author | paulson |
Tue, 29 Sep 1998 15:57:42 +0200 | |
changeset 5582 | a356fb49e69e |
parent 5562 | 02261e6880d1 |
child 5592 | 64697e426048 |
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 |
||
5512 | 12 |
qed_goal "NCons_Pls_0" Bin.thy |
13 |
"NCons Pls False = Pls" |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
14 |
(fn _ => [(Simp_tac 1)]); |
1632 | 15 |
|
5512 | 16 |
qed_goal "NCons_Pls_1" Bin.thy |
17 |
"NCons Pls True = Pls BIT True" |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
18 |
(fn _ => [(Simp_tac 1)]); |
1632 | 19 |
|
5512 | 20 |
qed_goal "NCons_Min_0" Bin.thy |
21 |
"NCons Min False = Min BIT False" |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
22 |
(fn _ => [(Simp_tac 1)]); |
1632 | 23 |
|
5512 | 24 |
qed_goal "NCons_Min_1" Bin.thy |
25 |
"NCons Min True = Min" |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
26 |
(fn _ => [(Simp_tac 1)]); |
1632 | 27 |
|
5512 | 28 |
qed_goal "bin_succ_1" Bin.thy |
29 |
"bin_succ(w BIT True) = (bin_succ w) BIT False" |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
30 |
(fn _ => [(Simp_tac 1)]); |
1632 | 31 |
|
5512 | 32 |
qed_goal "bin_succ_0" Bin.thy |
33 |
"bin_succ(w BIT False) = NCons w True" |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
34 |
(fn _ => [(Simp_tac 1)]); |
1632 | 35 |
|
5512 | 36 |
qed_goal "bin_pred_1" Bin.thy |
37 |
"bin_pred(w BIT True) = NCons w False" |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
38 |
(fn _ => [(Simp_tac 1)]); |
1632 | 39 |
|
5512 | 40 |
qed_goal "bin_pred_0" Bin.thy |
41 |
"bin_pred(w BIT False) = (bin_pred w) BIT True" |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
42 |
(fn _ => [(Simp_tac 1)]); |
1632 | 43 |
|
5512 | 44 |
qed_goal "bin_minus_1" Bin.thy |
45 |
"bin_minus(w BIT True) = bin_pred (NCons (bin_minus w) False)" |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
46 |
(fn _ => [(Simp_tac 1)]); |
1632 | 47 |
|
5512 | 48 |
qed_goal "bin_minus_0" Bin.thy |
49 |
"bin_minus(w BIT False) = (bin_minus w) BIT False" |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
50 |
(fn _ => [(Simp_tac 1)]); |
1632 | 51 |
|
5491 | 52 |
|
1632 | 53 |
(*** bin_add: binary addition ***) |
54 |
||
5512 | 55 |
qed_goal "bin_add_BIT_11" Bin.thy |
56 |
"bin_add (v BIT True) (w BIT True) = \ |
|
57 |
\ NCons (bin_add v (bin_succ w)) False" |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
58 |
(fn _ => [(Simp_tac 1)]); |
1632 | 59 |
|
5512 | 60 |
qed_goal "bin_add_BIT_10" Bin.thy |
61 |
"bin_add (v BIT True) (w BIT False) = NCons (bin_add v w) True" |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
62 |
(fn _ => [(Simp_tac 1)]); |
1632 | 63 |
|
5512 | 64 |
qed_goal "bin_add_BIT_0" Bin.thy |
65 |
"bin_add (v BIT False) (w BIT y) = NCons (bin_add v w) y" |
|
5491 | 66 |
(fn _ => [Auto_tac]); |
1632 | 67 |
|
5551 | 68 |
Goal "bin_add w Pls = w"; |
69 |
by (induct_tac "w" 1); |
|
70 |
by Auto_tac; |
|
71 |
qed "bin_add_Pls_right"; |
|
1632 | 72 |
|
5512 | 73 |
qed_goal "bin_add_BIT_Min" Bin.thy |
74 |
"bin_add (v BIT x) Min = bin_pred (v BIT x)" |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
75 |
(fn _ => [(Simp_tac 1)]); |
1632 | 76 |
|
5512 | 77 |
qed_goal "bin_add_BIT_BIT" Bin.thy |
78 |
"bin_add (v BIT x) (w BIT y) = \ |
|
79 |
\ NCons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)" |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
80 |
(fn _ => [(Simp_tac 1)]); |
1632 | 81 |
|
82 |
||
83 |
(*** bin_add: binary multiplication ***) |
|
84 |
||
5512 | 85 |
qed_goal "bin_mult_1" Bin.thy |
86 |
"bin_mult (v BIT True) w = bin_add (NCons (bin_mult v w) False) w" |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
87 |
(fn _ => [(Simp_tac 1)]); |
1632 | 88 |
|
5512 | 89 |
qed_goal "bin_mult_0" Bin.thy |
90 |
"bin_mult (v BIT False) w = NCons (bin_mult v w) False" |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
91 |
(fn _ => [(Simp_tac 1)]); |
1632 | 92 |
|
93 |
||
94 |
(**** The carry/borrow functions, bin_succ and bin_pred ****) |
|
95 |
||
96 |
||
5491 | 97 |
(**** integ_of ****) |
1632 | 98 |
|
5512 | 99 |
qed_goal "integ_of_NCons" Bin.thy |
100 |
"integ_of(NCons w b) = integ_of(w BIT b)" |
|
5184 | 101 |
(fn _ =>[(induct_tac "w" 1), |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
102 |
(ALLGOALS Asm_simp_tac) ]); |
1632 | 103 |
|
5512 | 104 |
Addsimps [integ_of_NCons]; |
1632 | 105 |
|
5491 | 106 |
qed_goal "integ_of_succ" Bin.thy |
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
107 |
"integ_of(bin_succ w) = int 1 + integ_of w" |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
108 |
(fn _ =>[(rtac bin.induct 1), |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
109 |
(ALLGOALS(asm_simp_tac (simpset() addsimps zadd_ac))) ]); |
5491 | 110 |
|
111 |
qed_goal "integ_of_pred" Bin.thy |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
112 |
"integ_of(bin_pred w) = - (int 1) + integ_of w" |
5491 | 113 |
(fn _ =>[(rtac bin.induct 1), |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
114 |
(ALLGOALS(asm_simp_tac (simpset() addsimps zadd_ac))) ]); |
1632 | 115 |
|
5491 | 116 |
Goal "integ_of(bin_minus w) = - (integ_of w)"; |
117 |
by (rtac bin.induct 1); |
|
118 |
by (Simp_tac 1); |
|
119 |
by (Simp_tac 1); |
|
120 |
by (asm_simp_tac (simpset() |
|
5551 | 121 |
delsimps [bin_pred_Pls, bin_pred_Min, bin_pred_BIT] |
5491 | 122 |
addsimps [integ_of_succ,integ_of_pred, |
123 |
zadd_assoc]) 1); |
|
124 |
qed "integ_of_minus"; |
|
1632 | 125 |
|
126 |
||
5512 | 127 |
val bin_add_simps = [bin_add_BIT_BIT, |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
128 |
integ_of_succ, integ_of_pred]; |
1632 | 129 |
|
5491 | 130 |
Goal "! w. integ_of(bin_add v w) = integ_of v + integ_of w"; |
5184 | 131 |
by (induct_tac "v" 1); |
4686 | 132 |
by (simp_tac (simpset() addsimps bin_add_simps) 1); |
133 |
by (simp_tac (simpset() addsimps bin_add_simps) 1); |
|
1632 | 134 |
by (rtac allI 1); |
5184 | 135 |
by (induct_tac "w" 1); |
5540 | 136 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps bin_add_simps @ zadd_ac))); |
5491 | 137 |
qed_spec_mp "integ_of_add"; |
1632 | 138 |
|
5512 | 139 |
val bin_mult_simps = [zmult_zminus, integ_of_minus, integ_of_add]; |
1632 | 140 |
|
5491 | 141 |
|
142 |
Goal "integ_of(bin_mult v w) = integ_of v * integ_of w"; |
|
5184 | 143 |
by (induct_tac "v" 1); |
4686 | 144 |
by (simp_tac (simpset() addsimps bin_mult_simps) 1); |
145 |
by (simp_tac (simpset() addsimps bin_mult_simps) 1); |
|
5491 | 146 |
by (asm_simp_tac |
5540 | 147 |
(simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac) 1); |
5491 | 148 |
qed "integ_of_mult"; |
149 |
||
1632 | 150 |
|
5491 | 151 |
(** Simplification rules with integer constants **) |
152 |
||
153 |
Goal "#0 + z = z"; |
|
154 |
by (Simp_tac 1); |
|
155 |
qed "zadd_0"; |
|
156 |
||
157 |
Goal "z + #0 = z"; |
|
158 |
by (Simp_tac 1); |
|
159 |
qed "zadd_0_right"; |
|
160 |
||
161 |
Goal "z + (- z) = #0"; |
|
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
162 |
by (Simp_tac 1); |
5491 | 163 |
qed "zadd_zminus_inverse"; |
164 |
||
165 |
Goal "(- z) + z = #0"; |
|
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
166 |
by (Simp_tac 1); |
5491 | 167 |
qed "zadd_zminus_inverse2"; |
168 |
||
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
169 |
(*These rewrite to int 0. Henceforth we should rewrite to #0 *) |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
170 |
Delsimps [zadd_zminus_inverse_nat, zadd_zminus_inverse_nat2]; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
171 |
|
5491 | 172 |
Addsimps [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2]; |
173 |
||
174 |
Goal "- (#0) = #0"; |
|
175 |
by (Simp_tac 1); |
|
176 |
qed "zminus_0"; |
|
177 |
||
178 |
Addsimps [zminus_0]; |
|
179 |
||
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
180 |
|
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
181 |
Goal "#0 - x = -x"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
182 |
by (simp_tac (simpset() addsimps [zdiff_def]) 1); |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
183 |
qed "zdiff0"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
184 |
|
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
185 |
Goal "x - #0 = x"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
186 |
by (simp_tac (simpset() addsimps [zdiff_def]) 1); |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
187 |
qed "zdiff0_right"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
188 |
|
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
189 |
Goal "x - x = #0"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
190 |
by (simp_tac (simpset() addsimps [zdiff_def]) 1); |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
191 |
qed "zdiff_self"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
192 |
|
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
193 |
Addsimps [zdiff0, zdiff0_right, zdiff_self]; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
194 |
|
5491 | 195 |
Goal "#0 * z = #0"; |
196 |
by (Simp_tac 1); |
|
197 |
qed "zmult_0"; |
|
198 |
||
199 |
Goal "#1 * z = z"; |
|
200 |
by (Simp_tac 1); |
|
201 |
qed "zmult_1"; |
|
202 |
||
203 |
Goal "#2 * z = z+z"; |
|
204 |
by (simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1); |
|
205 |
qed "zmult_2"; |
|
206 |
||
207 |
Goal "z * #0 = #0"; |
|
208 |
by (Simp_tac 1); |
|
209 |
qed "zmult_0_right"; |
|
210 |
||
211 |
Goal "z * #1 = z"; |
|
212 |
by (Simp_tac 1); |
|
213 |
qed "zmult_1_right"; |
|
214 |
||
215 |
Goal "z * #2 = z+z"; |
|
216 |
by (simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1); |
|
217 |
qed "zmult_2_right"; |
|
218 |
||
219 |
Addsimps [zmult_0, zmult_0_right, |
|
220 |
zmult_1, zmult_1_right, |
|
221 |
zmult_2, zmult_2_right]; |
|
222 |
||
223 |
Goal "(w < z + #1) = (w<z | w=z)"; |
|
224 |
by (simp_tac (simpset() addsimps [zless_add_nat1_eq]) 1); |
|
225 |
qed "zless_add1_eq"; |
|
226 |
||
227 |
Goal "(w + #1 <= z) = (w<z)"; |
|
228 |
by (simp_tac (simpset() addsimps [add_nat1_zle_eq]) 1); |
|
229 |
qed "add1_zle_eq"; |
|
230 |
Addsimps [add1_zle_eq]; |
|
231 |
||
5540 | 232 |
Goal "neg x = (x < #0)"; |
233 |
by (simp_tac (simpset() addsimps [neg_eq_less_nat0]) 1); |
|
234 |
qed "neg_eq_less_0"; |
|
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
235 |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
236 |
Goal "(~neg x) = (int 0 <= x)"; |
5540 | 237 |
by (simp_tac (simpset() addsimps [not_neg_eq_ge_nat0]) 1); |
238 |
qed "not_neg_eq_ge_0"; |
|
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
239 |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
240 |
Goal "#0 <= int m"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
241 |
by (Simp_tac 1); |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
242 |
qed "zero_zle_int"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
243 |
AddIffs [zero_zle_int]; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
244 |
|
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
245 |
|
5491 | 246 |
|
247 |
(** Simplification rules for comparison of binary numbers (Norbert Voelker) **) |
|
248 |
||
249 |
(** Equals (=) **) |
|
1632 | 250 |
|
5491 | 251 |
Goalw [iszero_def] |
252 |
"(integ_of x = integ_of y) \ |
|
253 |
\ = iszero(integ_of (bin_add x (bin_minus y)))"; |
|
254 |
by (simp_tac (simpset() addsimps |
|
255 |
(zcompare_rls @ [integ_of_add, integ_of_minus])) 1); |
|
256 |
qed "eq_integ_of_eq"; |
|
257 |
||
5512 | 258 |
Goalw [iszero_def] "iszero (integ_of Pls)"; |
5491 | 259 |
by (Simp_tac 1); |
5512 | 260 |
qed "iszero_integ_of_Pls"; |
5491 | 261 |
|
5512 | 262 |
Goalw [iszero_def] "~ iszero(integ_of Min)"; |
5491 | 263 |
by (Simp_tac 1); |
5512 | 264 |
qed "nonzero_integ_of_Min"; |
5491 | 265 |
|
266 |
Goalw [iszero_def] |
|
5512 | 267 |
"iszero (integ_of (w BIT x)) = (~x & iszero (integ_of w))"; |
5491 | 268 |
by (Simp_tac 1); |
269 |
by (int_case_tac "integ_of w" 1); |
|
270 |
by (ALLGOALS (asm_simp_tac |
|
5540 | 271 |
(simpset() addsimps zcompare_rls @ |
272 |
[zminus_zadd_distrib RS sym, |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
273 |
zadd_int]))); |
5512 | 274 |
qed "iszero_integ_of_BIT"; |
5491 | 275 |
|
276 |
||
277 |
(** Less-than (<) **) |
|
278 |
||
279 |
Goalw [zless_def,zdiff_def] |
|
280 |
"integ_of x < integ_of y \ |
|
5540 | 281 |
\ = neg (integ_of (bin_add x (bin_minus y)))"; |
5491 | 282 |
by (simp_tac (simpset() addsimps bin_mult_simps) 1); |
5540 | 283 |
qed "less_integ_of_eq_neg"; |
5491 | 284 |
|
5540 | 285 |
Goal "~ neg (integ_of Pls)"; |
5491 | 286 |
by (Simp_tac 1); |
5512 | 287 |
qed "not_neg_integ_of_Pls"; |
5491 | 288 |
|
5540 | 289 |
Goal "neg (integ_of Min)"; |
5491 | 290 |
by (Simp_tac 1); |
5512 | 291 |
qed "neg_integ_of_Min"; |
5491 | 292 |
|
5540 | 293 |
Goal "neg (integ_of (w BIT x)) = neg (integ_of w)"; |
5491 | 294 |
by (Asm_simp_tac 1); |
295 |
by (int_case_tac "integ_of w" 1); |
|
296 |
by (ALLGOALS (asm_simp_tac |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
297 |
(simpset() addsimps [zadd_int, neg_eq_less_nat0, |
5540 | 298 |
symmetric zdiff_def] @ zcompare_rls))); |
5512 | 299 |
qed "neg_integ_of_BIT"; |
5491 | 300 |
|
301 |
||
302 |
(** Less-than-or-equals (<=) **) |
|
303 |
||
304 |
Goal "(integ_of x <= integ_of y) = (~ integ_of y < integ_of x)"; |
|
305 |
by (simp_tac (simpset() addsimps [zle_def]) 1); |
|
306 |
qed "le_integ_of_eq_not_less"; |
|
307 |
||
5540 | 308 |
(*Delete the original rewrites, with their clumsy conditional expressions*) |
5551 | 309 |
Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT, |
310 |
NCons_Pls, NCons_Min, bin_add_BIT, bin_mult_BIT]; |
|
5491 | 311 |
|
312 |
(*Hide the binary representation of integer constants*) |
|
5540 | 313 |
Delsimps [integ_of_Pls, integ_of_Min, integ_of_BIT]; |
5491 | 314 |
|
315 |
(*Add simplification of arithmetic operations on integer constants*) |
|
316 |
Addsimps [integ_of_add RS sym, |
|
317 |
integ_of_minus RS sym, |
|
318 |
integ_of_mult RS sym, |
|
5512 | 319 |
bin_succ_1, bin_succ_0, |
320 |
bin_pred_1, bin_pred_0, |
|
321 |
bin_minus_1, bin_minus_0, |
|
5551 | 322 |
bin_add_Pls_right, bin_add_BIT_Min, |
5512 | 323 |
bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11, |
324 |
bin_mult_1, bin_mult_0, |
|
325 |
NCons_Pls_0, NCons_Pls_1, |
|
326 |
NCons_Min_0, NCons_Min_1, |
|
327 |
NCons_BIT]; |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
328 |
|
5491 | 329 |
(*... and simplification of relational operations*) |
5512 | 330 |
Addsimps [eq_integ_of_eq, iszero_integ_of_Pls, nonzero_integ_of_Min, |
331 |
iszero_integ_of_BIT, |
|
5540 | 332 |
less_integ_of_eq_neg, |
5512 | 333 |
not_neg_integ_of_Pls, neg_integ_of_Min, neg_integ_of_BIT, |
5491 | 334 |
le_integ_of_eq_not_less]; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
335 |
|
5491 | 336 |
Goalw [zdiff_def] |
337 |
"integ_of v - integ_of w = integ_of(bin_add v (bin_minus w))"; |
|
338 |
by (Simp_tac 1); |
|
339 |
qed "diff_integ_of_eq"; |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
340 |
|
5491 | 341 |
(*... and finally subtraction*) |
342 |
Addsimps [diff_integ_of_eq]; |
|
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
343 |
|
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
344 |
|
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
345 |
(** Simplification of inequalities involving numerical constants **) |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
346 |
|
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
347 |
Goal "(w <= z + #1) = (w<=z | w = z + #1)"; |
5540 | 348 |
by (simp_tac (simpset() addsimps [integ_le_less, zless_add1_eq]) 1); |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
349 |
qed "zle_add1_eq"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
350 |
|
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
351 |
Goal "(w <= z - #1) = (w<z)"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
352 |
by (simp_tac (simpset() addsimps zcompare_rls) 1); |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
353 |
qed "zle_diff1_eq"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
354 |
Addsimps [zle_diff1_eq]; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
355 |
|
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
356 |
(*2nd premise can be proved automatically if v is a literal*) |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
357 |
Goal "[| w <= z; #0 <= v |] ==> w <= z + v"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
358 |
by (dtac zadd_zle_mono 1); |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
359 |
by (assume_tac 1); |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
360 |
by (Full_simp_tac 1); |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
361 |
qed "zle_imp_zle_zadd"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
362 |
|
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
363 |
Goal "w <= z ==> w <= z + #1"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
364 |
by (asm_simp_tac (simpset() addsimps [zle_imp_zle_zadd]) 1); |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
365 |
qed "zle_imp_zle_zadd1"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
366 |
|
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
367 |
(*2nd premise can be proved automatically if v is a literal*) |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
368 |
Goal "[| w < z; #0 <= v |] ==> w < z + v"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
369 |
by (dtac zadd_zless_mono 1); |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
370 |
by (assume_tac 1); |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
371 |
by (Full_simp_tac 1); |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
372 |
qed "zless_imp_zless_zadd"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
373 |
|
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
374 |
Goal "w < z ==> w < z + #1"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
375 |
by (asm_simp_tac (simpset() addsimps [zless_imp_zless_zadd]) 1); |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
376 |
qed "zless_imp_zless_zadd1"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
377 |
|
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
378 |
Goal "(w < z + #1) = (w<=z)"; |
5540 | 379 |
by (simp_tac (simpset() addsimps [zless_add1_eq, integ_le_less]) 1); |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
380 |
qed "zle_add1_eq_le"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
381 |
Addsimps [zle_add1_eq_le]; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
382 |
|
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
383 |
Goal "(z = z + w) = (w = #0)"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
384 |
by (rtac trans 1); |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
385 |
by (rtac zadd_left_cancel 2); |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
386 |
by (simp_tac (simpset() addsimps [eq_sym_conv]) 1); |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
387 |
qed "zadd_left_cancel0"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
388 |
Addsimps [zadd_left_cancel0]; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
389 |
|
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
390 |
(*LOOPS as a simprule!*) |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
391 |
Goal "[| w + v < z; #0 <= v |] ==> w < z"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
392 |
by (dtac zadd_zless_mono 1); |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
393 |
by (assume_tac 1); |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
394 |
by (full_simp_tac (simpset() addsimps zadd_ac) 1); |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
395 |
qed "zless_zadd_imp_zless"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
396 |
|
5540 | 397 |
(*LOOPS as a simprule! Analogous to Suc_lessD*) |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
398 |
Goal "w + #1 < z ==> w < z"; |
5540 | 399 |
by (dtac zless_zadd_imp_zless 1); |
400 |
by (assume_tac 2); |
|
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
401 |
by (Simp_tac 1); |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
402 |
qed "zless_zadd1_imp_zless"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
403 |
|
5551 | 404 |
Goal "w + #-1 = w - #1"; |
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
405 |
by (Simp_tac 1); |
5551 | 406 |
qed "zplus_minus1_conv"; |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
407 |
|
5551 | 408 |
|
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
409 |
(*** nat ***) |
5551 | 410 |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
411 |
Goal "#0 <= z ==> int (nat z) = z"; |
5551 | 412 |
by (asm_full_simp_tac |
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
413 |
(simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1); |
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
414 |
qed "nat_0_le"; |
5551 | 415 |
|
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
416 |
Goal "z < #0 ==> nat z = 0"; |
5551 | 417 |
by (asm_full_simp_tac |
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
418 |
(simpset() addsimps [neg_eq_less_0, zle_def, neg_nat]) 1); |
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
419 |
qed "nat_less_0"; |
5551 | 420 |
|
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
421 |
Addsimps [nat_0_le, nat_less_0]; |
5551 | 422 |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
423 |
Goal "#0 <= w ==> (nat w = m) = (w = int m)"; |
5551 | 424 |
by Auto_tac; |
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
425 |
qed "nat_eq_iff"; |
5551 | 426 |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
427 |
Goal "#0 <= w ==> (nat w < m) = (w < int m)"; |
5551 | 428 |
by (rtac iffI 1); |
429 |
by (asm_full_simp_tac |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
430 |
(simpset() delsimps [zless_int] addsimps [zless_int RS sym]) 2); |
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
431 |
by (etac (nat_0_le RS subst) 1); |
5551 | 432 |
by (Simp_tac 1); |
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
433 |
qed "nat_less_iff"; |
5551 | 434 |
|
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
435 |
Goal "#0 <= w ==> (nat w < nat z) = (w<z)"; |
5551 | 436 |
by (case_tac "neg z" 1); |
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
437 |
by (auto_tac (claset(), simpset() addsimps [nat_less_iff])); |
5551 | 438 |
by (auto_tac (claset() addIs [zless_trans], |
439 |
simpset() addsimps [neg_eq_less_0, integ_of_Pls, zle_def])); |
|
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
440 |
qed "nat_less_eq_zless"; |
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
441 |
|
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
442 |
Goal "#0 <= w ==> (nat w < nat z) = (w<z)"; |
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
443 |
by (stac nat_less_iff 1); |
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
444 |
by (assume_tac 1); |
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
445 |
by (case_tac "neg z" 1); |
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
446 |
by (auto_tac (claset(), simpset() addsimps [not_neg_nat, neg_nat])); |
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
447 |
by (auto_tac (claset(), |
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
448 |
simpset() addsimps [neg_eq_less_0, integ_of_Pls, zle_def])); |
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
449 |
by (blast_tac (claset() addIs [zless_trans]) 1); |
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
450 |
qed "nat_less_eq_zless"; |
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
451 |
|
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
452 |
|
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
453 |
(**Can these be generalized without evaluating large numbers?**) |
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
454 |
Goal "(int k = #0) = (k=0)"; |
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
455 |
by (simp_tac (simpset() addsimps [integ_of_Pls]) 1); |
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
456 |
qed "nat_eq_0_conv"; |
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
457 |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
458 |
Goal "(#0 = int k) = (k=0)"; |
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
459 |
by (auto_tac (claset(), simpset() addsimps [integ_of_Pls])); |
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
460 |
qed "nat_eq_0_conv'"; |
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
461 |
|
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
462 |
Addsimps [nat_eq_0_conv, nat_eq_0_conv']; |
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
463 |
|
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
464 |