Changeset 277


Ignore:
Timestamp:
Nov 24, 2010, 5:06:16 PM (9 years ago)
Author:
sacerdot
Message:

Bugs fixed in definition of sub8_with_carrier.

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

Legend:

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

    r275 r277  
    6969    let c_as_nat ≝ nat_of_bitvector eight c in
    7070    let carry_as_nat ≝ nat_of_bool carry in
    71     let temporary ≝ minus (modulus b_as_nat sixteen) (modulus c_as_nat sixteen) in
    72     let ac_flag ≝ inclusive_disjunction
    73                     (negation (conjunction (less_than_or_equal_b (modulus b_as_nat sixteen) (modulus c_as_nat sixteen)) (less_than_or_equal_b temporary carry_as_nat)))
    74                     (conjunction (conjunction (decidable_equality b_as_nat Z) (decidable_equality c_as_nat Z)) (decidable_equality carry_as_nat Z)) in
    75     let bit_six ≝ inclusive_disjunction
    76                     (negation (conjunction (less_than_or_equal_b (modulus b_as_nat one_hundred_and_twenty_eight) (modulus c_as_nat one_hundred_and_twenty_eight)) (less_than_or_equal_b temporary carry_as_nat)))
    77                     (conjunction (conjunction (decidable_equality b_as_nat Z) (decidable_equality c_as_nat Z)) (decidable_equality carry_as_nat Z)) in
     71    let temporary ≝ b_as_nat mod sixteen - c_as_nat mod sixteen in
     72    let ac_flag ≝ negation (conjunction ((b_as_nat mod sixteen) ≤ (c_as_nat mod sixteen)) (temporary ≤ carry_as_nat)) in
     73    let bit_six ≝ negation (conjunction ((b_as_nat mod one_hundred_and_twenty_eight) ≤ (c_as_nat mod one_hundred_and_twenty_eight)) (temporary ≤ carry_as_nat)) in
    7874    let old_result_1 ≝ b_as_nat - c_as_nat in
    7975    let old_result_2 ≝ old_result_1 - carry_as_nat in
    8076    let ov_flag ≝ exclusive_disjunction carry bit_six in
    81       match less_than_or_equal_b b_as_nat c_as_nat with
    82         [ true ⇒
    83           match less_than_or_equal_b old_result_1 carry_as_nat with
    84             [ true ⇒
    85               let cy_flag ≝ false in
    86                 mk_Cartesian … (bitvector_of_nat eight old_result_2) (cy_flag :: ac_flag :: ov_flag :: (Empty Bool))
    87             | false ⇒
    88               let cy_flag ≝ true in
    89               let new_result ≝ b_as_nat + two_hundred_and_fifty_six - c_as_nat - carry_as_nat in
    90                 mk_Cartesian … (bitvector_of_nat eight new_result) (cy_flag :: ac_flag :: ov_flag :: (Empty Bool))
    91             ]
    92         | false ⇒
    93             let cy_flag ≝ true in
    94             let new_result ≝ b_as_nat + two_hundred_and_fifty_six - c_as_nat - carry_as_nat in
    95               mk_Cartesian … (bitvector_of_nat eight new_result) (cy_flag :: ac_flag :: ov_flag :: (Empty Bool))
     77      match conjunction (b_as_nat ≤ c_as_nat) (old_result_1 ≤ carry_as_nat) with
     78        [ false ⇒
     79           let cy_flag ≝ false in
     80            〈 bitvector_of_nat eight old_result_2, [cy_flag ; ac_flag ; ov_flag ] 〉
     81        | true ⇒
     82           let cy_flag ≝ true in
     83           let new_result ≝ b_as_nat + two_hundred_and_fifty_six - c_as_nat - carry_as_nat in
     84            〈 bitvector_of_nat eight new_result, [ cy_flag ; ac_flag ; ov_flag ] 〉
    9685        ].
    97    
     86         
    9887ndefinition add_8_with_carry ≝ add_n_with_carry eight.
    9988ndefinition add_16_with_carry ≝ add_n_with_carry sixteen.
  • Deliverables/D4.1/Matita/Nat.ma

    r275 r277  
    164164      ].
    165165   
    166 notation "hvbox(n break % m)"
     166notation "hvbox(n break 'mod' m)"
    167167  right associative with precedence 47
    168168  for @{ 'modulus $n $m }.
Note: See TracChangeset for help on using the changeset viewer.