Context Navigation

Arithmetic.ma @ 302

Last change on this file since 302 was 286, checked in by mulligan, 10 years ago
Added bit address lookup for registers.
File size: 6.3 KB

Line
1	include "Universes.ma".
2	include "Plogic/equality.ma".
3	include "Connectives.ma".
4	include "Nat.ma".
5	include "Exponential.ma".
6	include "Bool.ma".
7	include "BitVector.ma".
8	include "List.ma".
9
10	ndefinition one ≝ S Z.
11	ndefinition two ≝ (S(S(Z))).
12	ndefinition three ≝ two + one.
13	ndefinition four ≝ two + two.
14	ndefinition five ≝ three + two.
15	ndefinition six ≝ three + three.
16	ndefinition seven ≝ three + four.
17	ndefinition eight ≝ four + four.
18	ndefinition nine ≝ five + four.
19	ndefinition ten ≝ five + five.
20	ndefinition eleven ≝ six + five.
21	ndefinition twelve ≝ six + six.
22	ndefinition thirteen ≝ seven + six.
23	ndefinition fourteen ≝ seven + seven.
24	ndefinition fifteen ≝ eight + seven.
25	ndefinition sixteen ≝ eight + eight.
26	ndefinition seventeen ≝ nine + eight.
27	ndefinition eighteen ≝ nine + nine.
28	ndefinition nineteen ≝ ten + nine.
29	ndefinition twenty_four ≝ sixteen + eight.
30	ndefinition one_hundred ≝ ten * ten.
31	ndefinition one_hundred_and_twenty_eight ≝ sixteen * eight.
32	ndefinition one_hundred_and_twenty_nine ≝ one_hundred_and_twenty_eight + one.
33	ndefinition one_hundred_and_thirty ≝ one_hundred_and_twenty_nine + one.
34	ndefinition one_hundred_and_thirty_one ≝ one_hundred_and_thirty + one.
35	ndefinition one_hundred_and_thirty_five ≝ one_hundred_and_twenty_eight + seven.
36	ndefinition one_hundred_and_thirty_six ≝ one_hundred_and_thirty_five + one.
37	ndefinition one_hundred_and_thirty_seven ≝ one_hundred_and_thirty_six + one.
38	ndefinition one_hundred_and_thirty_eight ≝ one_hundred_and_twenty_eight + ten.
39	ndefinition one_hundred_and_thirty_nine ≝ one_hundred_and_thirty_eight + one.
40	ndefinition one_hundred_and_forty ≝ one_hundred_and_thirty_nine + one.
41	ndefinition one_hundred_and_forty_one ≝ one_hundred_and_forty + one.
42	ndefinition one_hundred_and_forty_four ≝ one_hundred_and_twenty_eight + sixteen.
43	ndefinition one_hundred_and_fifty_two ≝ one_hundred_and_forty_four + eight.
44	ndefinition one_hundred_and_fifty_three ≝ one_hundred_and_forty_four + nine.
45	ndefinition one_hundred_and_sixty ≝ one_hundred_and_forty_four + sixteen.
46	ndefinition one_hundred_and_sixty_eight ≝ one_hundred_and_sixty + eight.
47	ndefinition one_hundred_and_seventy_six ≝ one_hundred_and_sixty + sixteen.
48	ndefinition one_hundred_and_eighty_four ≝ one_hundred_and_seventy_six + eight.
49	ndefinition two_hundred ≝ one_hundred + one_hundred.
50	ndefinition two_hundred_and_two ≝ two_hundred + two.
51	ndefinition two_hundred_and_three ≝ two_hundred_and_two + one.
52	ndefinition two_hundred_and_four ≝ two_hundred_and_three + one.
53	ndefinition two_hundred_and_five ≝ two_hundred_and_four + one.
54	ndefinition two_hundred_and_eight ≝ two_hundred_and_five + three.
55	ndefinition two_hundred_and_twenty_four ≝ two_hundred_and_eight + sixteen.
56	ndefinition two_hundred_and_forty ≝ two_hundred_and_twenty_four + sixteen.
57	ndefinition two_hundred_and_fifty_six ≝
58	one_hundred_and_twenty_eight + one_hundred_and_twenty_eight.
59
60	ndefinition nat_of_bool ≝
61	λb: Bool.
62	match b with
63	[ false ⇒ Z
64	\| true ⇒ S Z
65	].
66
67	ndefinition 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;
89	nqed.
90
91	ndefinition 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
114	ndefinition add_8_with_carry ≝ add_n_with_carry eight.
115	ndefinition add_16_with_carry ≝ add_n_with_carry sixteen.
116
117	ndefinition 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
127	ndefinition 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
136	alias symbol "greater_than_or_equal" (instance 1) = "Nat greater than or equal prop".
137
138	ndefinition 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;
146	nqed.

Note: See TracBrowser for help on using the repository browser.

Download in other formats:

Original Format