source: Deliverables/D4.1/Demo-March-2011/matita/Arithmetic.ma @ 664

Last change on this file since 664 was 664, checked in by mulligan, 9 years ago

Changed output of Intel HEX files so we no longer have those gargantuan blocks of zeroes at the end.

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