source: Deliverables/D4.1/Matita/Arithmetic.ma @ 433

Last change on this file since 433 was 374, checked in by sacerdot, 10 years ago

1) notation for cast fixed
2) ambiguity reduced: Empty => VEmpty, Cons => VCons
3) DoTest? modified to pretty-print the execution trace.

This should make debugging easier.

File size: 3.9 KB
RevLine 
[248]1include "Exponential.ma".
2include "BitVector.ma".
[257]3
[248]4ndefinition nat_of_bool ≝
5  λb: Bool.
6    match b with
[260]7      [ false ⇒ Z
8      | true ⇒ S Z
[248]9      ].
10   
[246]11ndefinition add_n_with_carry:
[359]12      ∀n: Nat. ∀b, c: BitVector n. ∀carry: Bool. Cartesian (BitVector n) (BitVector three) ≝
[246]13  λn: Nat.
14  λb: BitVector n.
15  λc: BitVector n.
16  λcarry: Bool.
17    let b_as_nat ≝ nat_of_bitvector n b in
18    let c_as_nat ≝ nat_of_bitvector n c in
19    let carry_as_nat ≝ nat_of_bool carry in
20    let result_old ≝ b_as_nat + c_as_nat + carry_as_nat in
[248]21    let ac_flag ≝ ((modulus b_as_nat ((S (S Z)) * n)) +
22                  (modulus c_as_nat ((S (S Z)) * n)) +
[351]23                  c_as_nat) ≳ ((S (S Z)) * n) in
[246]24    let bit_xxx ≝ (((modulus b_as_nat ((S (S Z))^(n - (S Z)))) +
25                  (modulus c_as_nat ((S (S Z))^(n - (S Z)))) +
[351]26                  c_as_nat) ≳ ((S (S Z))^(n - (S Z)))) in
[246]27    let result ≝ modulus result_old ((S (S Z))^n) in
[351]28    let cy_flag ≝ (result_old ≳ ((S (S Z))^n)) in
[246]29    let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in
[359]30      mk_Cartesian ? ? (bitvector_of_nat n result)
31                       ([[ cy_flag ; ac_flag ; ov_flag ]]).
[246]32
[359]33ndefinition sub_8_with_carry: ∀b,c: BitVector eight. ∀carry: Bool. Cartesian (BitVector eight) (BitVector three) ≝
[246]34  λb: BitVector eight.
35  λc: BitVector eight.
36  λ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
[277]40    let temporary ≝ b_as_nat mod sixteen - c_as_nat mod sixteen in
[351]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
[274]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
[351]46      match conjunction (b_as_nat ≲ c_as_nat) (old_result_1 ≲ carry_as_nat) with
[277]47        [ false ⇒
48           let cy_flag ≝ false in
[359]49            〈 bitvector_of_nat eight old_result_2, [[ cy_flag ; ac_flag ; ov_flag ]]〉
[277]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
[359]53            〈 bitvector_of_nat eight new_result, [[ cy_flag ; ac_flag ; ov_flag ]]〉
[274]54        ].
[277]55         
[246]56ndefinition add_8_with_carry ≝ add_n_with_carry eight.
57ndefinition add_16_with_carry ≝ add_n_with_carry sixteen.
58
59ndefinition increment ≝
60  λn: Nat.
61  λb: BitVector n.
62    let b_as_nat ≝ (nat_of_bitvector n b) + (S Z) in
[351]63    let overflow ≝ b_as_nat ≳ (S (S Z))^n in
[246]64      match overflow with
[273]65        [ false ⇒ bitvector_of_nat n b_as_nat
66        | true ⇒ zero n
[246]67        ].
68       
69ndefinition decrement ≝
70  λn: Nat.
71  λb: BitVector n.
72    let b_as_nat ≝ nat_of_bitvector n b in
73      match b_as_nat with
74        [ Z ⇒ max n
75        | S o ⇒ bitvector_of_nat n o
76        ].
77       
78alias symbol "greater_than_or_equal" (instance 1) = "Nat greater than or equal prop".
79
80ndefinition bitvector_of_bool:
[351]81      ∀n: Nat. ∀b: Bool. BitVector (S n) ≝
[246]82  λn: Nat.
83  λb: Bool.
[374]84   (pad (S n - (S Z)) (S Z) [[b]])⌈(S n - (S Z)) + S Z ↦ S n⌉.
85 /2/.
[248]86nqed.
[349]87
[350]88ndefinition full_add ≝
89  λn: Nat.
90  λb, c: BitVector n.
91  λd: Bit.
92    fold_right2_i ? ? ? (
93      λn.
94       λb1, b2: Bool.
95        λd: Bit × (BitVector n).
[349]96        let 〈c1,r〉 ≝ d in
97          〈inclusive_disjunction (conjunction b1 b2)
98                                 (conjunction c1 (inclusive_disjunction b1 b2)),
[350]99           (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉)
100     〈d, [[ ]]〉 ? b c.
[349]101   
102ndefinition half_add ≝
103  λn: Nat.
104  λb, c: BitVector n.
[374]105    full_add n b c false.
Note: See TracBrowser for help on using the repository browser.