author | paulson |
Tue, 15 Sep 1998 15:06:29 +0200 | |
changeset 5491 | 22f8331cdf47 |
parent 5224 | 8d132a14e722 |
child 5510 | ad120f7c52ad |
permissions | -rw-r--r-- |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
1 |
(* Title: HOL/Integ/Bin.ML |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
2 |
Authors: Lawrence C Paulson, Cambridge University Computer Laboratory |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
3 |
David Spelt, University of Twente |
1632 | 4 |
Copyright 1994 University of Cambridge |
5 |
Copyright 1996 University of Twente |
|
6 |
||
7 |
Arithmetic on binary integers. |
|
8 |
*) |
|
9 |
||
10 |
(** extra rules for bin_succ, bin_pred, bin_add, bin_mult **) |
|
11 |
||
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
12 |
qed_goal "norm_Bcons_Plus_0" Bin.thy |
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
2224
diff
changeset
|
13 |
"norm_Bcons PlusSign False = PlusSign" |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
14 |
(fn _ => [(Simp_tac 1)]); |
1632 | 15 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
16 |
qed_goal "norm_Bcons_Plus_1" Bin.thy |
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
2224
diff
changeset
|
17 |
"norm_Bcons PlusSign True = Bcons PlusSign True" |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
18 |
(fn _ => [(Simp_tac 1)]); |
1632 | 19 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
20 |
qed_goal "norm_Bcons_Minus_0" Bin.thy |
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
2224
diff
changeset
|
21 |
"norm_Bcons MinusSign False = Bcons MinusSign False" |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
22 |
(fn _ => [(Simp_tac 1)]); |
1632 | 23 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
24 |
qed_goal "norm_Bcons_Minus_1" Bin.thy |
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
2224
diff
changeset
|
25 |
"norm_Bcons MinusSign True = MinusSign" |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
26 |
(fn _ => [(Simp_tac 1)]); |
1632 | 27 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
28 |
qed_goal "norm_Bcons_Bcons" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
29 |
"norm_Bcons (Bcons w x) b = Bcons (Bcons w x) b" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
30 |
(fn _ => [(Simp_tac 1)]); |
1632 | 31 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
32 |
qed_goal "bin_succ_Bcons1" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
33 |
"bin_succ(Bcons w True) = Bcons (bin_succ w) False" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
34 |
(fn _ => [(Simp_tac 1)]); |
1632 | 35 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
36 |
qed_goal "bin_succ_Bcons0" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
37 |
"bin_succ(Bcons w False) = norm_Bcons w True" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
38 |
(fn _ => [(Simp_tac 1)]); |
1632 | 39 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
40 |
qed_goal "bin_pred_Bcons1" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
41 |
"bin_pred(Bcons w True) = norm_Bcons w False" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
42 |
(fn _ => [(Simp_tac 1)]); |
1632 | 43 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
44 |
qed_goal "bin_pred_Bcons0" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
45 |
"bin_pred(Bcons w False) = Bcons (bin_pred w) True" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
46 |
(fn _ => [(Simp_tac 1)]); |
1632 | 47 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
48 |
qed_goal "bin_minus_Bcons1" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
49 |
"bin_minus(Bcons w True) = bin_pred (Bcons(bin_minus w) False)" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
50 |
(fn _ => [(Simp_tac 1)]); |
1632 | 51 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
52 |
qed_goal "bin_minus_Bcons0" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
53 |
"bin_minus(Bcons w False) = Bcons (bin_minus w) False" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
54 |
(fn _ => [(Simp_tac 1)]); |
1632 | 55 |
|
5491 | 56 |
|
1632 | 57 |
(*** bin_add: binary addition ***) |
58 |
||
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
59 |
qed_goal "bin_add_Bcons_Bcons11" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
60 |
"bin_add (Bcons v True) (Bcons w True) = \ |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
61 |
\ norm_Bcons (bin_add v (bin_succ w)) False" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
62 |
(fn _ => [(Simp_tac 1)]); |
1632 | 63 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
64 |
qed_goal "bin_add_Bcons_Bcons10" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
65 |
"bin_add (Bcons v True) (Bcons w False) = norm_Bcons (bin_add v w) True" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
66 |
(fn _ => [(Simp_tac 1)]); |
1632 | 67 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
68 |
qed_goal "bin_add_Bcons_Bcons0" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
69 |
"bin_add (Bcons v False) (Bcons w y) = norm_Bcons (bin_add v w) y" |
5491 | 70 |
(fn _ => [Auto_tac]); |
1632 | 71 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
72 |
qed_goal "bin_add_Bcons_Plus" Bin.thy |
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
2224
diff
changeset
|
73 |
"bin_add (Bcons v x) PlusSign = Bcons v x" |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
74 |
(fn _ => [(Simp_tac 1)]); |
1632 | 75 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
76 |
qed_goal "bin_add_Bcons_Minus" Bin.thy |
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
2224
diff
changeset
|
77 |
"bin_add (Bcons v x) MinusSign = bin_pred (Bcons v x)" |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
78 |
(fn _ => [(Simp_tac 1)]); |
1632 | 79 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
80 |
qed_goal "bin_add_Bcons_Bcons" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
81 |
"bin_add (Bcons v x) (Bcons w y) = \ |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
82 |
\ norm_Bcons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
83 |
(fn _ => [(Simp_tac 1)]); |
1632 | 84 |
|
85 |
||
86 |
(*** bin_add: binary multiplication ***) |
|
87 |
||
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
88 |
qed_goal "bin_mult_Bcons1" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
89 |
"bin_mult (Bcons v True) w = bin_add (norm_Bcons (bin_mult v w) False) w" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
90 |
(fn _ => [(Simp_tac 1)]); |
1632 | 91 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
92 |
qed_goal "bin_mult_Bcons0" Bin.thy |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
93 |
"bin_mult (Bcons v False) w = norm_Bcons (bin_mult v w) False" |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
94 |
(fn _ => [(Simp_tac 1)]); |
1632 | 95 |
|
96 |
||
97 |
(**** The carry/borrow functions, bin_succ and bin_pred ****) |
|
98 |
||
99 |
||
5491 | 100 |
(**** integ_of ****) |
1632 | 101 |
|
5491 | 102 |
qed_goal "integ_of_norm_Bcons" Bin.thy |
103 |
"integ_of(norm_Bcons w b) = integ_of(Bcons w b)" |
|
5184 | 104 |
(fn _ =>[(induct_tac "w" 1), |
5491 | 105 |
(ALLGOALS (asm_simp_tac |
106 |
(simpset() addsimps [zadd_zminus_inverse_nat]))) ]); |
|
1632 | 107 |
|
5491 | 108 |
val integ_of_norm_Cons_simps = |
109 |
[zadd_zminus_inverse_nat, integ_of_norm_Bcons] @ zadd_ac; |
|
1632 | 110 |
|
5491 | 111 |
qed_goal "integ_of_succ" Bin.thy |
112 |
"integ_of(bin_succ w) = $#1 + integ_of w" |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
113 |
(fn _ =>[(rtac bin.induct 1), |
5491 | 114 |
(ALLGOALS(asm_simp_tac (simpset() addsimps integ_of_norm_Cons_simps))) ]); |
115 |
||
116 |
qed_goal "integ_of_pred" Bin.thy |
|
117 |
"integ_of(bin_pred w) = - ($#1) + integ_of w" |
|
118 |
(fn _ =>[(rtac bin.induct 1), |
|
119 |
(ALLGOALS(asm_simp_tac (simpset() addsimps integ_of_norm_Cons_simps))) ]); |
|
1632 | 120 |
|
5491 | 121 |
Goal "integ_of(bin_minus w) = - (integ_of w)"; |
122 |
by (rtac bin.induct 1); |
|
123 |
by (Simp_tac 1); |
|
124 |
by (Simp_tac 1); |
|
125 |
by (asm_simp_tac (simpset() |
|
126 |
delsimps [pred_Plus,pred_Minus,pred_Bcons] |
|
127 |
addsimps [integ_of_succ,integ_of_pred, |
|
128 |
zadd_assoc]) 1); |
|
129 |
qed "integ_of_minus"; |
|
1632 | 130 |
|
131 |
||
5491 | 132 |
val bin_add_simps = [zadd_zminus_inverse_nat, zadd_zminus_inverse_nat2, |
133 |
bin_add_Bcons_Plus, |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
134 |
bin_add_Bcons_Minus,bin_add_Bcons_Bcons, |
5491 | 135 |
integ_of_succ, integ_of_pred, |
136 |
integ_of_norm_Bcons]; |
|
1632 | 137 |
|
5491 | 138 |
Goal "! w. integ_of(bin_add v w) = integ_of v + integ_of w"; |
5184 | 139 |
by (induct_tac "v" 1); |
4686 | 140 |
by (simp_tac (simpset() addsimps bin_add_simps) 1); |
141 |
by (simp_tac (simpset() addsimps bin_add_simps) 1); |
|
1632 | 142 |
by (rtac allI 1); |
5184 | 143 |
by (induct_tac "w" 1); |
5491 | 144 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)))); |
145 |
qed_spec_mp "integ_of_add"; |
|
1632 | 146 |
|
5491 | 147 |
val bin_mult_simps = [zmult_zminus, |
148 |
integ_of_minus, integ_of_add, |
|
149 |
integ_of_norm_Bcons]; |
|
1632 | 150 |
|
5491 | 151 |
|
152 |
Goal "integ_of(bin_mult v w) = integ_of v * integ_of w"; |
|
5184 | 153 |
by (induct_tac "v" 1); |
4686 | 154 |
by (simp_tac (simpset() addsimps bin_mult_simps) 1); |
155 |
by (simp_tac (simpset() addsimps bin_mult_simps) 1); |
|
5491 | 156 |
by (asm_simp_tac |
157 |
(simpset() addsimps (bin_mult_simps @ [zadd_zmult_distrib] @ |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
158 |
zadd_ac)) 1); |
5491 | 159 |
qed "integ_of_mult"; |
160 |
||
161 |
(* #0 = $# 0 *) |
|
162 |
bind_thm ("int_eq_nat0", integ_of_Plus); |
|
163 |
||
164 |
Goal "$# 1 = #1"; |
|
165 |
by (Simp_tac 1); |
|
166 |
qed "int_eq_nat1"; |
|
167 |
||
168 |
Goal "$# 2 = #2"; |
|
169 |
by (simp_tac (simpset() addsimps [add_znat]) 1); |
|
170 |
qed "int_eq_nat2"; |
|
1632 | 171 |
|
172 |
||
5491 | 173 |
(** Simplification rules with integer constants **) |
174 |
||
175 |
Goal "#0 + z = z"; |
|
176 |
by (Simp_tac 1); |
|
177 |
qed "zadd_0"; |
|
178 |
||
179 |
Goal "z + #0 = z"; |
|
180 |
by (Simp_tac 1); |
|
181 |
qed "zadd_0_right"; |
|
182 |
||
183 |
Goal "z + (- z) = #0"; |
|
184 |
by (simp_tac (simpset() addsimps [zadd_zminus_inverse_nat]) 1); |
|
185 |
qed "zadd_zminus_inverse"; |
|
186 |
||
187 |
Goal "(- z) + z = #0"; |
|
188 |
by (simp_tac (simpset() addsimps [zadd_zminus_inverse_nat2]) 1); |
|
189 |
qed "zadd_zminus_inverse2"; |
|
190 |
||
191 |
Addsimps [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2]; |
|
192 |
||
193 |
Goal "- (#0) = #0"; |
|
194 |
by (Simp_tac 1); |
|
195 |
qed "zminus_0"; |
|
196 |
||
197 |
Addsimps [zminus_0]; |
|
198 |
||
199 |
Goal "#0 * z = #0"; |
|
200 |
by (Simp_tac 1); |
|
201 |
qed "zmult_0"; |
|
202 |
||
203 |
Goal "#1 * z = z"; |
|
204 |
by (Simp_tac 1); |
|
205 |
qed "zmult_1"; |
|
206 |
||
207 |
Goal "#2 * z = z+z"; |
|
208 |
by (simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1); |
|
209 |
qed "zmult_2"; |
|
210 |
||
211 |
Goal "z * #0 = #0"; |
|
212 |
by (Simp_tac 1); |
|
213 |
qed "zmult_0_right"; |
|
214 |
||
215 |
Goal "z * #1 = z"; |
|
216 |
by (Simp_tac 1); |
|
217 |
qed "zmult_1_right"; |
|
218 |
||
219 |
Goal "z * #2 = z+z"; |
|
220 |
by (simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1); |
|
221 |
qed "zmult_2_right"; |
|
222 |
||
223 |
Addsimps [zmult_0, zmult_0_right, |
|
224 |
zmult_1, zmult_1_right, |
|
225 |
zmult_2, zmult_2_right]; |
|
226 |
||
227 |
Goal "(w < z + #1) = (w<z | w=z)"; |
|
228 |
by (simp_tac (simpset() addsimps [zless_add_nat1_eq]) 1); |
|
229 |
qed "zless_add1_eq"; |
|
230 |
||
231 |
Goal "(w + #1 <= z) = (w<z)"; |
|
232 |
by (simp_tac (simpset() addsimps [add_nat1_zle_eq]) 1); |
|
233 |
qed "add1_zle_eq"; |
|
234 |
Addsimps [add1_zle_eq]; |
|
235 |
||
236 |
||
237 |
(** Simplification rules for comparison of binary numbers (Norbert Voelker) **) |
|
238 |
||
239 |
(** Equals (=) **) |
|
1632 | 240 |
|
5491 | 241 |
Goalw [iszero_def] |
242 |
"(integ_of x = integ_of y) \ |
|
243 |
\ = iszero(integ_of (bin_add x (bin_minus y)))"; |
|
244 |
by (simp_tac (simpset() addsimps |
|
245 |
(zcompare_rls @ [integ_of_add, integ_of_minus])) 1); |
|
246 |
qed "eq_integ_of_eq"; |
|
247 |
||
248 |
Goalw [iszero_def] "iszero (integ_of PlusSign)"; |
|
249 |
by (Simp_tac 1); |
|
250 |
qed "iszero_integ_of_Plus"; |
|
251 |
||
252 |
Goalw [iszero_def] "~ iszero(integ_of MinusSign)"; |
|
253 |
by (Simp_tac 1); |
|
254 |
qed "nonzero_integ_of_Minus"; |
|
255 |
||
256 |
Goalw [iszero_def] |
|
257 |
"iszero (integ_of (Bcons w x)) = (~x & iszero (integ_of w))"; |
|
258 |
by (Simp_tac 1); |
|
259 |
by (int_case_tac "integ_of w" 1); |
|
260 |
by (ALLGOALS (asm_simp_tac |
|
261 |
(simpset() addsimps (zcompare_rls @ |
|
262 |
[zminus_zadd_distrib RS sym, |
|
263 |
add_znat])))); |
|
264 |
qed "iszero_integ_of_Bcons"; |
|
265 |
||
266 |
||
267 |
(** Less-than (<) **) |
|
268 |
||
269 |
Goalw [zless_def,zdiff_def] |
|
270 |
"integ_of x < integ_of y \ |
|
271 |
\ = znegative (integ_of (bin_add x (bin_minus y)))"; |
|
272 |
by (simp_tac (simpset() addsimps bin_mult_simps) 1); |
|
273 |
qed "less_integ_of_eq_zneg"; |
|
274 |
||
275 |
Goal "~ znegative (integ_of PlusSign)"; |
|
276 |
by (Simp_tac 1); |
|
277 |
qed "not_neg_integ_of_Plus"; |
|
278 |
||
279 |
Goal "znegative (integ_of MinusSign)"; |
|
280 |
by (Simp_tac 1); |
|
281 |
qed "neg_integ_of_Minus"; |
|
282 |
||
283 |
Goal "znegative (integ_of (Bcons w x)) = znegative (integ_of w)"; |
|
284 |
by (Asm_simp_tac 1); |
|
285 |
by (int_case_tac "integ_of w" 1); |
|
286 |
by (ALLGOALS (asm_simp_tac |
|
287 |
(simpset() addsimps ([add_znat, znegative_eq_less_0, |
|
288 |
symmetric zdiff_def] @ |
|
289 |
zcompare_rls)))); |
|
290 |
qed "neg_integ_of_Bcons"; |
|
291 |
||
292 |
||
293 |
(** Less-than-or-equals (<=) **) |
|
294 |
||
295 |
Goal "(integ_of x <= integ_of y) = (~ integ_of y < integ_of x)"; |
|
296 |
by (simp_tac (simpset() addsimps [zle_def]) 1); |
|
297 |
qed "le_integ_of_eq_not_less"; |
|
298 |
||
299 |
||
300 |
(*Hide the binary representation of integer constants*) |
|
301 |
Delsimps [succ_Bcons, pred_Bcons, min_Bcons, add_Bcons, mult_Bcons, |
|
302 |
integ_of_Plus, integ_of_Minus, integ_of_Bcons, |
|
303 |
norm_Plus, norm_Minus, norm_Bcons]; |
|
304 |
||
305 |
(*Add simplification of arithmetic operations on integer constants*) |
|
306 |
Addsimps [integ_of_add RS sym, |
|
307 |
integ_of_minus RS sym, |
|
308 |
integ_of_mult RS sym, |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
309 |
bin_succ_Bcons1,bin_succ_Bcons0, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
310 |
bin_pred_Bcons1,bin_pred_Bcons0, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
311 |
bin_minus_Bcons1,bin_minus_Bcons0, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
312 |
bin_add_Bcons_Plus,bin_add_Bcons_Minus, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
313 |
bin_add_Bcons_Bcons0,bin_add_Bcons_Bcons10,bin_add_Bcons_Bcons11, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
314 |
bin_mult_Bcons1,bin_mult_Bcons0, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
315 |
norm_Bcons_Plus_0,norm_Bcons_Plus_1, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
316 |
norm_Bcons_Minus_0,norm_Bcons_Minus_1, |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
317 |
norm_Bcons_Bcons]; |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
318 |
|
5491 | 319 |
(*... and simplification of relational operations*) |
320 |
Addsimps [eq_integ_of_eq, iszero_integ_of_Plus, nonzero_integ_of_Minus, |
|
321 |
iszero_integ_of_Bcons, |
|
322 |
less_integ_of_eq_zneg, |
|
323 |
not_neg_integ_of_Plus, neg_integ_of_Minus, neg_integ_of_Bcons, |
|
324 |
le_integ_of_eq_not_less]; |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
325 |
|
5491 | 326 |
Goalw [zdiff_def] |
327 |
"integ_of v - integ_of w = integ_of(bin_add v (bin_minus w))"; |
|
328 |
by (Simp_tac 1); |
|
329 |
qed "diff_integ_of_eq"; |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
330 |
|
5491 | 331 |
(*... and finally subtraction*) |
332 |
Addsimps [diff_integ_of_eq]; |