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

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

Added bit address lookup for registers.

File size: 6.3 KB
Line 
1include "Universes.ma".
2include "Plogic/equality.ma".
3include "Connectives.ma".
4include "Nat.ma".
5include "Exponential.ma".
6include "Bool.ma".
7include "BitVector.ma".
8include "List.ma".
9
10ndefinition one ≝ S Z.
11ndefinition two ≝ (S(S(Z))).
12ndefinition three ≝ two + one.
13ndefinition four ≝ two + two.
14ndefinition five ≝ three + two.
15ndefinition six ≝ three + three.
16ndefinition seven ≝ three + four.
17ndefinition eight ≝ four + four.
18ndefinition nine ≝ five + four.
19ndefinition ten ≝ five + five.
20ndefinition eleven ≝ six + five.
21ndefinition twelve ≝ six + six.
22ndefinition thirteen ≝ seven + six.
23ndefinition fourteen ≝ seven + seven.
24ndefinition fifteen ≝ eight + seven.
25ndefinition sixteen ≝ eight + eight.
26ndefinition seventeen ≝ nine + eight.
27ndefinition eighteen ≝ nine + nine.
28ndefinition nineteen ≝ ten + nine.
29ndefinition twenty_four ≝ sixteen + eight.
30ndefinition one_hundred ≝ ten * ten.
31ndefinition one_hundred_and_twenty_eight ≝ sixteen * eight.
32ndefinition one_hundred_and_twenty_nine ≝ one_hundred_and_twenty_eight + one.
33ndefinition one_hundred_and_thirty ≝ one_hundred_and_twenty_nine + one.
34ndefinition one_hundred_and_thirty_one ≝ one_hundred_and_thirty + one.
35ndefinition one_hundred_and_thirty_five ≝ one_hundred_and_twenty_eight + seven.
36ndefinition one_hundred_and_thirty_six ≝ one_hundred_and_thirty_five + one.
37ndefinition one_hundred_and_thirty_seven ≝ one_hundred_and_thirty_six + one.
38ndefinition one_hundred_and_thirty_eight ≝ one_hundred_and_twenty_eight + ten.
39ndefinition one_hundred_and_thirty_nine ≝ one_hundred_and_thirty_eight + one.
40ndefinition one_hundred_and_forty ≝ one_hundred_and_thirty_nine + one.
41ndefinition one_hundred_and_forty_one ≝ one_hundred_and_forty + one.
42ndefinition one_hundred_and_forty_four ≝ one_hundred_and_twenty_eight + sixteen.
43ndefinition one_hundred_and_fifty_two ≝ one_hundred_and_forty_four + eight.
44ndefinition one_hundred_and_fifty_three ≝ one_hundred_and_forty_four + nine.
45ndefinition one_hundred_and_sixty ≝ one_hundred_and_forty_four + sixteen.
46ndefinition one_hundred_and_sixty_eight ≝ one_hundred_and_sixty + eight.
47ndefinition one_hundred_and_seventy_six ≝ one_hundred_and_sixty + sixteen.
48ndefinition one_hundred_and_eighty_four ≝ one_hundred_and_seventy_six + eight.
49ndefinition two_hundred ≝ one_hundred + one_hundred.
50ndefinition two_hundred_and_two ≝ two_hundred + two.
51ndefinition two_hundred_and_three ≝ two_hundred_and_two + one.
52ndefinition two_hundred_and_four ≝ two_hundred_and_three + one.
53ndefinition two_hundred_and_five ≝ two_hundred_and_four + one.
54ndefinition two_hundred_and_eight ≝ two_hundred_and_five + three.
55ndefinition two_hundred_and_twenty_four ≝ two_hundred_and_eight + sixteen.
56ndefinition two_hundred_and_forty ≝ two_hundred_and_twenty_four + sixteen.
57ndefinition two_hundred_and_fifty_six ≝
58  one_hundred_and_twenty_eight + one_hundred_and_twenty_eight.                                       
59   
60ndefinition nat_of_bool ≝
61  λb: Bool.
62    match b with
63      [ false ⇒ Z
64      | true ⇒ S Z
65      ].
66   
67ndefinition add_n_with_carry:
68      ∀n: Nat. ∀b, c: BitVector n. ∀carry: Bool. Cartesian (BitVector n) (List Bool) ≝
69  λn: Nat.
70  λb: BitVector n.
71  λc: BitVector n.
72  λcarry: Bool.
73    let b_as_nat ≝ nat_of_bitvector n b in
74    let c_as_nat ≝ nat_of_bitvector n c in
75    let carry_as_nat ≝ nat_of_bool carry in
76    let result_old ≝ b_as_nat + c_as_nat + carry_as_nat in
77    let ac_flag ≝ ((modulus b_as_nat ((S (S Z)) * n)) +
78                  (modulus c_as_nat ((S (S Z)) * n)) +
79                  c_as_nat) ≥ ((S (S Z)) * n) in
80    let bit_xxx ≝ (((modulus b_as_nat ((S (S Z))^(n - (S Z)))) +
81                  (modulus c_as_nat ((S (S Z))^(n - (S Z)))) +
82                  c_as_nat) ≥ ((S (S Z))^(n - (S Z)))) in
83    let result ≝ modulus result_old ((S (S Z))^n) in
84    let cy_flag ≝ (result_old ≥ ((S (S Z))^n)) in
85    let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in
86      ? (mk_Cartesian (BitVector n) ? (? (bitvector_of_nat n result))
87                          (cy_flag :: ac_flag :: ov_flag :: Empty Bool)).
88    #H; nassumption;
89nqed.
90
91ndefinition sub_8_with_carry: ∀b,c: BitVector eight. ∀carry: Bool. Cartesian (BitVector eight) (List Bool) ≝
92  λb: BitVector eight.
93  λc: BitVector eight.
94  λcarry: Bool.
95    let b_as_nat ≝ nat_of_bitvector eight b in
96    let c_as_nat ≝ nat_of_bitvector eight c in
97    let carry_as_nat ≝ nat_of_bool carry in
98    let temporary ≝ b_as_nat mod sixteen - c_as_nat mod sixteen in
99    let ac_flag ≝ negation (conjunction ((b_as_nat mod sixteen) ≤ (c_as_nat mod sixteen)) (temporary ≤ carry_as_nat)) in
100    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
101    let old_result_1 ≝ b_as_nat - c_as_nat in
102    let old_result_2 ≝ old_result_1 - carry_as_nat in
103    let ov_flag ≝ exclusive_disjunction carry bit_six in
104      match conjunction (b_as_nat ≤ c_as_nat) (old_result_1 ≤ carry_as_nat) with
105        [ false ⇒
106           let cy_flag ≝ false in
107            〈 bitvector_of_nat eight old_result_2, [cy_flag ; ac_flag ; ov_flag ] 〉
108        | true ⇒
109           let cy_flag ≝ true in
110           let new_result ≝ b_as_nat + two_hundred_and_fifty_six - c_as_nat - carry_as_nat in
111            〈 bitvector_of_nat eight new_result, [ cy_flag ; ac_flag ; ov_flag ] 〉
112        ].
113         
114ndefinition add_8_with_carry ≝ add_n_with_carry eight.
115ndefinition add_16_with_carry ≝ add_n_with_carry sixteen.
116
117ndefinition increment ≝
118  λn: Nat.
119  λb: BitVector n.
120    let b_as_nat ≝ (nat_of_bitvector n b) + (S Z) in
121    let overflow ≝ b_as_nat ≥ (S (S Z))^n in
122      match overflow with
123        [ false ⇒ bitvector_of_nat n b_as_nat
124        | true ⇒ zero n
125        ].
126       
127ndefinition decrement ≝
128  λn: Nat.
129  λb: BitVector n.
130    let b_as_nat ≝ nat_of_bitvector n b in
131      match b_as_nat with
132        [ Z ⇒ max n
133        | S o ⇒ bitvector_of_nat n o
134        ].
135       
136alias symbol "greater_than_or_equal" (instance 1) = "Nat greater than or equal prop".
137
138ndefinition bitvector_of_bool:
139      ∀n: Nat. ∀b: Bool. BitVector n ≝
140  λn: Nat.
141  λb: Bool.
142    ? (pad (n - (S Z)) (S Z) (Cons Bool ? b (Empty Bool))).
143  nrewrite > (plus_minus_inverse_right n ?);
144  #H;
145  nassumption;
146nqed.
Note: See TracBrowser for help on using the repository browser.