Changeset 273


Ignore:
Timestamp:
Nov 24, 2010, 2:28:34 PM (9 years ago)
Author:
mulligan
Message:

Some fault functions were rewritten.

Location:
Deliverables/D4.1/Matita
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Arithmetic.ma

    r272 r273  
    5959      ? (mk_Cartesian (BitVector n) ? (? (bitvector_of_nat n result))
    6060                          (cy_flag :: ac_flag :: ov_flag :: Empty Bool)).
    61     //.
     61    #H; nassumption;
    6262nqed.
    6363
     
    7171    let c_as_nat ≝ nat_of_bitvector eight c in
    7272    let carry_as_nat ≝ nat_of_bool carry in
    73     let result_old_1 ≝ minus (minus b_as_nat c_as_nat) carry_as_nat in
    74     let modulus_1 ≝ (modulus b_as_nat sixteen) - (modulus c_as_nat sixteen) in
    75       match less_than_b (modulus b_as_nat sixteen) (modulus c_as_nat sixteen) with
    76         [ true ⇒
    77           let ac_flag ≝ true in
    78           let result_old_2 ≝ (minus (modulus b_as_nat one_hundred_and_twenty_eight)
    79                                    (modulus c_as_nat one_hundred_and_twenty_eight)) in
    80             match less_than_b (modulus b_as_nat one_hundred_and_twenty_eight)
    81                               (modulus c_as_nat one_hundred_and_twenty_eight) with
    82             [ true ⇒
    83               let bit_six ≝ true in
    84               let result_carry ≝ mk_Cartesian … result_old_1 false in
    85               let ov_flag ≝ exclusive_disjunction cy_flag bit_six in
    86                 mk_Cartesian … (first … result_carry) (second … result_carry :: ac_flag :: ov_flag :: Empty Bool)
    87             | false ⇒ ?
    88             ]
    89         | false ⇒ ?
    90         ].
    91    
    9273   
    9374ndefinition add_8_with_carry ≝ add_n_with_carry eight.
    9475ndefinition add_16_with_carry ≝ add_n_with_carry sixteen.
    9576
    96 (*
    9777ndefinition increment ≝
    9878  λn: Nat.
     
    10181    let overflow ≝ b_as_nat ≥ (S (S Z))^n in
    10282      match overflow with
    103         [ False ⇒ bitvector_of_nat n b_as_nat
    104         | True ⇒ bitvector_of_nat n Z
     83        [ false ⇒ bitvector_of_nat n b_as_nat
     84        | true ⇒ zero n
    10585        ].
    10686       
     
    121101  λb: Bool.
    122102    ? (pad (n - (S Z)) (S Z) (Cons Bool ? b (Empty Bool))).
    123   //.
     103  nrewrite > (plus_minus_inverse_right n ?);
     104  #H;
     105  nassumption;
    124106nqed.
    125 
    126 *)
  • Deliverables/D4.1/Matita/BitVector.ma

    r271 r273  
    185185nqed.
    186186
    187 ndefinition bitvector_of_nat ≝
    188   λm, n: Nat.
    189     let biglist ≝ reverse Bool (bitvector_of_nat_aux m) in
    190     let size ≝ length Bool biglist in
    191     let bitvector ≝ bitvector_of_list biglist in
    192     let difference ≝ n - size in
    193       pad difference size bitvector.
     187naxiom plus_minus_inverse_left:
     188  ∀m, n: Nat.
     189    (m + n) - n = m.
     190   
     191naxiom plus_minus_inverse_right:
     192  ∀m, n: Nat.
     193    (m - n) + n = m.
     194
     195naxiom greater_than_b: Nat → Nat → Bool.
     196
     197nlet rec bitvector_of_nat (n: Nat) (m: Nat): BitVector n ≝
     198  let biglist ≝ reverse ? (bitvector_of_nat_aux m) in
     199  let size ≝ length ? biglist in
     200  let bitvector ≝ bitvector_of_list biglist in
     201  let difference ≝ n - size in
     202    match greater_than_b size n with
     203      [ true ⇒ max n
     204      | false ⇒ ? (pad difference size bitvector)
     205      ].
     206      nnormalize.
     207      nrewrite > (plus_minus_inverse_right n ?).
     208      #H.
     209      nassumption.
     210nqed.
     211
     212ncheck bitvector_of_nat.
    194213
    195214nlet rec nat_of_bitvector (n: Nat) (b: BitVector n) on b ≝
Note: See TracChangeset for help on using the changeset viewer.