Changeset 462 for Deliverables/D4.1/Matita/Arithmetic.ma
 Timestamp:
 Jan 20, 2011, 1:32:32 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Arithmetic.ma
r374 r462 31 31 ([[ cy_flag ; ac_flag ; ov_flag ]]). 32 32 33 ndefinition sub_8_with_carry: ∀b,c: BitVector eight. ∀carry: Bool. Cartesian (BitVector eight) (BitVector three) ≝ 34 λb: BitVector eight. 35 λc: BitVector eight. 33 ndefinition sub_n_with_carry: ∀n: Nat. ∀b,c: BitVector n. ∀carry: Bool. Cartesian (BitVector n) (BitVector three) ≝ 34 λn: Nat. 35 λb: BitVector n. 36 λc: BitVector n. 36 37 λcarry: Bool. 37 let b_as_nat ≝ nat_of_bitvector eight b in 38 let c_as_nat ≝ nat_of_bitvector eight c in 39 let carry_as_nat ≝ nat_of_bool carry in 40 let temporary ≝ b_as_nat mod sixteen  c_as_nat mod sixteen in 41 let ac_flag ≝ negation (conjunction ((b_as_nat mod sixteen) ≲ (c_as_nat mod sixteen)) (temporary ≲ carry_as_nat)) in 42 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 43 let old_result_1 ≝ b_as_nat  c_as_nat in 44 let old_result_2 ≝ old_result_1  carry_as_nat in 45 let ov_flag ≝ exclusive_disjunction carry bit_six in 46 match conjunction (b_as_nat ≲ c_as_nat) (old_result_1 ≲ carry_as_nat) with 47 [ false ⇒ 48 let cy_flag ≝ false in 49 〈 bitvector_of_nat eight old_result_2, [[ cy_flag ; ac_flag ; ov_flag ]]〉 50  true ⇒ 51 let cy_flag ≝ true in 52 let new_result ≝ b_as_nat + two_hundred_and_fifty_six  c_as_nat  carry_as_nat in 53 〈 bitvector_of_nat eight new_result, [[ cy_flag ; ac_flag ; ov_flag ]]〉 54 ]. 38 let b_as_nat ≝ nat_of_bitvector n b in 39 let c_as_nat ≝ nat_of_bitvector n c in 40 let carry_as_nat ≝ nat_of_bool carry in 41 let temporary ≝ (b_as_nat mod (two * n))  (c_as_nat mod (two * n)) in 42 let ac_flag ≝ less_than_b (b_as_nat mod (two * n)) ((c_as_nat mod (two * n)) + carry_as_nat) in 43 let bit_six ≝ less_than_b (b_as_nat mod (two^(n  one))) ((c_as_nat mod (two^(n  one))) + carry_as_nat) in 44 let 〈b',cy_flag〉 ≝ 45 if greater_than_or_equal_b b_as_nat (c_as_nat + carry_as_nat) then 46 〈b_as_nat, false〉 47 else 48 〈b_as_nat + (two^n), true〉 49 in 50 let ov_flag ≝ exclusive_disjunction cy_flag bit_six in 51 〈bitvector_of_nat n ((b'  c_as_nat)  carry_as_nat), [[ cy_flag; ac_flag; ov_flag ]]〉. 55 52 56 53 ndefinition add_8_with_carry ≝ add_n_with_carry eight. 57 54 ndefinition add_16_with_carry ≝ add_n_with_carry sixteen. 55 ndefinition sub_8_with_carry ≝ sub_n_with_carry eight. 56 ndefinition sub_16_with_carry ≝ sub_n_with_carry sixteen. 58 57 59 58 ndefinition increment ≝ … … 75 74  S o ⇒ bitvector_of_nat n o 76 75 ]. 77 76 77 ndefinition two_complement_negation ≝ 78 λn: Nat. 79 λb: BitVector n. 80 let new_b ≝ negation_bv n b in 81 increment n new_b. 82 83 ndefinition addition_n ≝ 84 λn: Nat. 85 λb, c: BitVector n. 86 let 〈res,flags〉 ≝ add_n_with_carry n b c false in 87 res. 88 89 ndefinition subtraction ≝ 90 λn: Nat. 91 λb, c: BitVector n. 92 addition_n n b (two_complement_negation n c). 93 94 ndefinition multiplication ≝ 95 λn: Nat. 96 λb, c: BitVector n. 97 let b_nat ≝ nat_of_bitvector ? b in 98 let c_nat ≝ nat_of_bitvector ? c in 99 let result ≝ b_nat * c_nat in 100 bitvector_of_nat (n + n) result. 101 102 ndefinition division_u ≝ 103 λn: Nat. 104 λb, c: BitVector n. 105 let b_nat ≝ nat_of_bitvector ? b in 106 let c_nat ≝ nat_of_bitvector ? c in 107 match c_nat with 108 [ Z ⇒ Nothing ? 109  _ ⇒ 110 let result ≝ b_nat ÷ c_nat in 111 Just ? (bitvector_of_nat n result) 112 ]. 113 114 ndefinition division_s: ∀n. ∀b, c: BitVector n. Maybe (BitVector n) ≝ 115 λn. 116 match n with 117 [ Z ⇒ λb, c. Nothing ? 118  S p ⇒ λb, c: BitVector (S p). 119 let b_sign_bit ≝ get_index_v ? ? b Z ? in 120 let c_sign_bit ≝ get_index_v ? ? c Z ? in 121 let b_as_nat ≝ nat_of_bitvector ? b in 122 let c_as_nat ≝ nat_of_bitvector ? c in 123 match c_as_nat with 124 [ Z ⇒ Nothing ? 125  S o ⇒ 126 match b_sign_bit with 127 [ true ⇒ 128 let temp_b ≝ (b_as_nat  (two^((S p)one))) in 129 match c_sign_bit with 130 [ true ⇒ 131 let temp_c ≝ (c_as_nat  (two^((S p)one))) in 132 Just ? (bitvector_of_nat ? (temp_b ÷ temp_c)) 133  false ⇒ 134 let result ≝ (temp_b ÷ c_as_nat) + (two^((S p)one)) in 135 Just ? (bitvector_of_nat ? result) 136 ] 137  false ⇒ 138 match c_sign_bit with 139 [ true ⇒ 140 let temp_c ≝ (c_as_nat  (two^((S p)one))) in 141 let result ≝ (b_as_nat ÷ temp_c) + (two^((S p)one)) in 142 Just ? (bitvector_of_nat ? result) 143  false ⇒ Just ? (bitvector_of_nat ? (b_as_nat ÷ c_as_nat)) 144 ] 145 ] 146 ] 147 ]. 148 //; 149 nqed. 150 151 ndefinition modulus_u ≝ 152 λn. 153 λb, c: BitVector n. 154 let b_nat ≝ nat_of_bitvector ? b in 155 let c_nat ≝ nat_of_bitvector ? c in 156 let result ≝ modulus b_nat c_nat in 157 bitvector_of_nat (n + n) result. 158 159 ndefinition modulus_s ≝ 160 λn. 161 λb, c: BitVector n. 162 match division_s n b c with 163 [ Nothing ⇒ Nothing ? 164  Just result ⇒ 165 let 〈high_bits, low_bits〉 ≝ split Bool ? n (multiplication n result c) in 166 Just ? (subtraction n b low_bits) 167 ]. 168 169 ndefinition lt_u ≝ 170 λn. 171 λb, c: BitVector n. 172 let b_nat ≝ nat_of_bitvector ? b in 173 let c_nat ≝ nat_of_bitvector ? c in 174 less_than_b b_nat c_nat. 175 176 ndefinition gt_u ≝ λn, b, c. lt_u n c b. 177 178 ndefinition lte_u ≝ λn, b, c. negation (gt_u n b c). 179 180 ndefinition gte_u ≝ λn, b, c. negation (lt_u n b c). 181 182 ndefinition lt_s ≝ 183 λn. 184 λb, c: BitVector n. 185 let 〈result, flags〉 ≝ sub_n_with_carry n b c false in 186 let ov_flag ≝ get_index_v ? ? flags two ? in 187 if ov_flag then 188 true 189 else 190 ((match n return λn'.BitVector n' → Bool with 191 [ Z ⇒ λ_.false 192  S o ⇒ 193 λresult'.(get_index_v ? ? result' Z ?) 194 ]) result). 195 //; 196 nqed. 197 198 ndefinition gt_s ≝ λn,b,c. lt_s n c b. 199 200 ndefinition lte_s ≝ λn,b,c. negation (gt_s n b c). 201 202 ndefinition gte_s ≝ λn. λb, c. 203 negation (lt_s n b c). 204 78 205 alias symbol "greater_than_or_equal" (instance 1) = "Nat greater than or equal prop". 79 206
Note: See TracChangeset
for help on using the changeset viewer.