author | nipkow |
Sat, 09 Jan 1999 15:24:11 +0100 | |
changeset 6073 | fba734ba6894 |
parent 6060 | d30d1dd2082d |
child 6079 | 4f7975c74cdf |
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 |
6060 | 4 |
Tobias Nipkow, Technical University Munich |
1632 | 5 |
Copyright 1994 University of Cambridge |
6060 | 6 |
Copyright 1996 University of Twente |
7 |
Copyright 1999 TU Munich |
|
1632 | 8 |
|
6060 | 9 |
Arithmetic on binary integers; |
10 |
decision procedure for linear arithmetic. |
|
1632 | 11 |
*) |
12 |
||
13 |
(** extra rules for bin_succ, bin_pred, bin_add, bin_mult **) |
|
14 |
||
5512 | 15 |
qed_goal "NCons_Pls_0" Bin.thy |
16 |
"NCons Pls False = Pls" |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
17 |
(fn _ => [(Simp_tac 1)]); |
1632 | 18 |
|
5512 | 19 |
qed_goal "NCons_Pls_1" Bin.thy |
20 |
"NCons Pls True = Pls BIT True" |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
21 |
(fn _ => [(Simp_tac 1)]); |
1632 | 22 |
|
5512 | 23 |
qed_goal "NCons_Min_0" Bin.thy |
24 |
"NCons Min False = Min BIT False" |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
25 |
(fn _ => [(Simp_tac 1)]); |
1632 | 26 |
|
5512 | 27 |
qed_goal "NCons_Min_1" Bin.thy |
28 |
"NCons Min True = Min" |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
29 |
(fn _ => [(Simp_tac 1)]); |
1632 | 30 |
|
5512 | 31 |
qed_goal "bin_succ_1" Bin.thy |
32 |
"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
|
33 |
(fn _ => [(Simp_tac 1)]); |
1632 | 34 |
|
5512 | 35 |
qed_goal "bin_succ_0" Bin.thy |
36 |
"bin_succ(w BIT False) = NCons w True" |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
37 |
(fn _ => [(Simp_tac 1)]); |
1632 | 38 |
|
5512 | 39 |
qed_goal "bin_pred_1" Bin.thy |
40 |
"bin_pred(w BIT True) = NCons w False" |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
41 |
(fn _ => [(Simp_tac 1)]); |
1632 | 42 |
|
5512 | 43 |
qed_goal "bin_pred_0" Bin.thy |
44 |
"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
|
45 |
(fn _ => [(Simp_tac 1)]); |
1632 | 46 |
|
5512 | 47 |
qed_goal "bin_minus_1" Bin.thy |
48 |
"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
|
49 |
(fn _ => [(Simp_tac 1)]); |
1632 | 50 |
|
5512 | 51 |
qed_goal "bin_minus_0" Bin.thy |
52 |
"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
|
53 |
(fn _ => [(Simp_tac 1)]); |
1632 | 54 |
|
5491 | 55 |
|
1632 | 56 |
(*** bin_add: binary addition ***) |
57 |
||
5512 | 58 |
qed_goal "bin_add_BIT_11" Bin.thy |
59 |
"bin_add (v BIT True) (w BIT True) = \ |
|
60 |
\ NCons (bin_add v (bin_succ w)) False" |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
61 |
(fn _ => [(Simp_tac 1)]); |
1632 | 62 |
|
5512 | 63 |
qed_goal "bin_add_BIT_10" Bin.thy |
64 |
"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
|
65 |
(fn _ => [(Simp_tac 1)]); |
1632 | 66 |
|
5512 | 67 |
qed_goal "bin_add_BIT_0" Bin.thy |
68 |
"bin_add (v BIT False) (w BIT y) = NCons (bin_add v w) y" |
|
5491 | 69 |
(fn _ => [Auto_tac]); |
1632 | 70 |
|
5551 | 71 |
Goal "bin_add w Pls = w"; |
72 |
by (induct_tac "w" 1); |
|
73 |
by Auto_tac; |
|
74 |
qed "bin_add_Pls_right"; |
|
1632 | 75 |
|
5512 | 76 |
qed_goal "bin_add_BIT_Min" Bin.thy |
77 |
"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
|
78 |
(fn _ => [(Simp_tac 1)]); |
1632 | 79 |
|
5512 | 80 |
qed_goal "bin_add_BIT_BIT" Bin.thy |
81 |
"bin_add (v BIT x) (w BIT y) = \ |
|
82 |
\ 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
|
83 |
(fn _ => [(Simp_tac 1)]); |
1632 | 84 |
|
85 |
||
6036 | 86 |
(*** bin_mult: binary multiplication ***) |
1632 | 87 |
|
5512 | 88 |
qed_goal "bin_mult_1" Bin.thy |
89 |
"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
|
90 |
(fn _ => [(Simp_tac 1)]); |
1632 | 91 |
|
5512 | 92 |
qed_goal "bin_mult_0" Bin.thy |
93 |
"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
|
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 |
|
5512 | 102 |
qed_goal "integ_of_NCons" Bin.thy |
103 |
"integ_of(NCons w b) = integ_of(w BIT b)" |
|
5184 | 104 |
(fn _ =>[(induct_tac "w" 1), |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
105 |
(ALLGOALS Asm_simp_tac) ]); |
1632 | 106 |
|
5512 | 107 |
Addsimps [integ_of_NCons]; |
1632 | 108 |
|
5491 | 109 |
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
|
110 |
"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
|
111 |
(fn _ =>[(rtac bin.induct 1), |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
112 |
(ALLGOALS(asm_simp_tac (simpset() addsimps zadd_ac))) ]); |
5491 | 113 |
|
114 |
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
|
115 |
"integ_of(bin_pred w) = - (int 1) + integ_of w" |
5491 | 116 |
(fn _ =>[(rtac bin.induct 1), |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
117 |
(ALLGOALS(asm_simp_tac (simpset() addsimps zadd_ac))) ]); |
1632 | 118 |
|
5491 | 119 |
Goal "integ_of(bin_minus w) = - (integ_of w)"; |
120 |
by (rtac bin.induct 1); |
|
121 |
by (Simp_tac 1); |
|
122 |
by (Simp_tac 1); |
|
123 |
by (asm_simp_tac (simpset() |
|
5551 | 124 |
delsimps [bin_pred_Pls, bin_pred_Min, bin_pred_BIT] |
5491 | 125 |
addsimps [integ_of_succ,integ_of_pred, |
126 |
zadd_assoc]) 1); |
|
127 |
qed "integ_of_minus"; |
|
1632 | 128 |
|
129 |
||
6036 | 130 |
val bin_add_simps = [bin_add_BIT_BIT, integ_of_succ, integ_of_pred]; |
1632 | 131 |
|
6036 | 132 |
(*This proof is complicated by the mutual recursion*) |
5491 | 133 |
Goal "! w. integ_of(bin_add v w) = integ_of v + integ_of w"; |
5184 | 134 |
by (induct_tac "v" 1); |
4686 | 135 |
by (simp_tac (simpset() addsimps bin_add_simps) 1); |
136 |
by (simp_tac (simpset() addsimps bin_add_simps) 1); |
|
1632 | 137 |
by (rtac allI 1); |
5184 | 138 |
by (induct_tac "w" 1); |
5540 | 139 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps bin_add_simps @ zadd_ac))); |
5491 | 140 |
qed_spec_mp "integ_of_add"; |
1632 | 141 |
|
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
142 |
|
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
143 |
(*Subtraction*) |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
144 |
Goalw [zdiff_def] |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
145 |
"integ_of v - integ_of w = integ_of(bin_add v (bin_minus w))"; |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
146 |
by (simp_tac (simpset() addsimps [integ_of_add, integ_of_minus]) 1); |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
147 |
qed "diff_integ_of_eq"; |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
148 |
|
5512 | 149 |
val bin_mult_simps = [zmult_zminus, integ_of_minus, integ_of_add]; |
1632 | 150 |
|
5491 | 151 |
Goal "integ_of(bin_mult v w) = integ_of v * integ_of w"; |
5184 | 152 |
by (induct_tac "v" 1); |
4686 | 153 |
by (simp_tac (simpset() addsimps bin_mult_simps) 1); |
154 |
by (simp_tac (simpset() addsimps bin_mult_simps) 1); |
|
5491 | 155 |
by (asm_simp_tac |
5540 | 156 |
(simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac) 1); |
5491 | 157 |
qed "integ_of_mult"; |
158 |
||
1632 | 159 |
|
5491 | 160 |
(** Simplification rules with integer constants **) |
161 |
||
162 |
Goal "#0 + z = z"; |
|
163 |
by (Simp_tac 1); |
|
164 |
qed "zadd_0"; |
|
165 |
||
166 |
Goal "z + #0 = z"; |
|
167 |
by (Simp_tac 1); |
|
168 |
qed "zadd_0_right"; |
|
169 |
||
5592 | 170 |
Addsimps [zadd_0, zadd_0_right]; |
171 |
||
172 |
||
173 |
(** Converting simple cases of (int n) to numerals **) |
|
5491 | 174 |
|
5592 | 175 |
(*int 0 = #0 *) |
176 |
bind_thm ("int_0", integ_of_Pls RS sym); |
|
5491 | 177 |
|
5592 | 178 |
Goal "int (Suc n) = #1 + int n"; |
179 |
by (simp_tac (simpset() addsimps [zadd_int]) 1); |
|
180 |
qed "int_Suc"; |
|
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
181 |
|
5592 | 182 |
val int_simps = [int_0, int_Suc]; |
5491 | 183 |
|
184 |
Goal "- (#0) = #0"; |
|
185 |
by (Simp_tac 1); |
|
186 |
qed "zminus_0"; |
|
187 |
||
188 |
Addsimps [zminus_0]; |
|
189 |
||
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
190 |
|
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
191 |
Goal "#0 - x = -x"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
192 |
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
|
193 |
qed "zdiff0"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
194 |
|
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
195 |
Goal "x - #0 = x"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
196 |
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
|
197 |
qed "zdiff0_right"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
198 |
|
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
199 |
Goal "x - x = #0"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
200 |
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
|
201 |
qed "zdiff_self"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
202 |
|
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
203 |
Addsimps [zdiff0, zdiff0_right, zdiff_self]; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
204 |
|
5491 | 205 |
Goal "#0 * z = #0"; |
206 |
by (Simp_tac 1); |
|
207 |
qed "zmult_0"; |
|
208 |
||
209 |
Goal "#1 * z = z"; |
|
210 |
by (Simp_tac 1); |
|
211 |
qed "zmult_1"; |
|
212 |
||
213 |
Goal "#2 * z = z+z"; |
|
214 |
by (simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1); |
|
215 |
qed "zmult_2"; |
|
216 |
||
217 |
Goal "z * #0 = #0"; |
|
218 |
by (Simp_tac 1); |
|
219 |
qed "zmult_0_right"; |
|
220 |
||
221 |
Goal "z * #1 = z"; |
|
222 |
by (Simp_tac 1); |
|
223 |
qed "zmult_1_right"; |
|
224 |
||
225 |
Goal "z * #2 = z+z"; |
|
226 |
by (simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1); |
|
227 |
qed "zmult_2_right"; |
|
228 |
||
229 |
Addsimps [zmult_0, zmult_0_right, |
|
230 |
zmult_1, zmult_1_right, |
|
231 |
zmult_2, zmult_2_right]; |
|
232 |
||
233 |
Goal "(w < z + #1) = (w<z | w=z)"; |
|
5592 | 234 |
by (simp_tac (simpset() addsimps [zless_add_int_Suc_eq]) 1); |
5491 | 235 |
qed "zless_add1_eq"; |
236 |
||
237 |
Goal "(w + #1 <= z) = (w<z)"; |
|
5592 | 238 |
by (simp_tac (simpset() addsimps [add_int_Suc_zle_eq]) 1); |
5491 | 239 |
qed "add1_zle_eq"; |
240 |
Addsimps [add1_zle_eq]; |
|
241 |
||
5540 | 242 |
Goal "neg x = (x < #0)"; |
243 |
by (simp_tac (simpset() addsimps [neg_eq_less_nat0]) 1); |
|
244 |
qed "neg_eq_less_0"; |
|
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
245 |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
246 |
Goal "(~neg x) = (int 0 <= x)"; |
5540 | 247 |
by (simp_tac (simpset() addsimps [not_neg_eq_ge_nat0]) 1); |
248 |
qed "not_neg_eq_ge_0"; |
|
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
249 |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
250 |
Goal "#0 <= int m"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
251 |
by (Simp_tac 1); |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
252 |
qed "zero_zle_int"; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
253 |
AddIffs [zero_zle_int]; |
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
254 |
|
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
255 |
|
5747 | 256 |
(** Needed because (int 0) rewrites to #0. |
257 |
Can these be generalized without evaluating large numbers?**) |
|
258 |
||
259 |
Goal "~ (int k < #0)"; |
|
260 |
by (Simp_tac 1); |
|
261 |
qed "int_less_0_conv"; |
|
262 |
||
263 |
Goal "(int k <= #0) = (k=0)"; |
|
264 |
by (Simp_tac 1); |
|
265 |
qed "int_le_0_conv"; |
|
266 |
||
267 |
Goal "(int k = #0) = (k=0)"; |
|
268 |
by (Simp_tac 1); |
|
269 |
qed "int_eq_0_conv"; |
|
270 |
||
271 |
Goal "(#0 = int k) = (k=0)"; |
|
272 |
by Auto_tac; |
|
273 |
qed "int_eq_0_conv'"; |
|
274 |
||
275 |
Addsimps [int_less_0_conv, int_le_0_conv, int_eq_0_conv, int_eq_0_conv']; |
|
276 |
||
277 |
||
5491 | 278 |
(** Simplification rules for comparison of binary numbers (Norbert Voelker) **) |
279 |
||
280 |
(** Equals (=) **) |
|
1632 | 281 |
|
5491 | 282 |
Goalw [iszero_def] |
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
283 |
"(integ_of x = integ_of y) = iszero(integ_of (bin_add x (bin_minus y)))"; |
5491 | 284 |
by (simp_tac (simpset() addsimps |
285 |
(zcompare_rls @ [integ_of_add, integ_of_minus])) 1); |
|
286 |
qed "eq_integ_of_eq"; |
|
287 |
||
5512 | 288 |
Goalw [iszero_def] "iszero (integ_of Pls)"; |
5491 | 289 |
by (Simp_tac 1); |
5512 | 290 |
qed "iszero_integ_of_Pls"; |
5491 | 291 |
|
5512 | 292 |
Goalw [iszero_def] "~ iszero(integ_of Min)"; |
5491 | 293 |
by (Simp_tac 1); |
5512 | 294 |
qed "nonzero_integ_of_Min"; |
5491 | 295 |
|
296 |
Goalw [iszero_def] |
|
5512 | 297 |
"iszero (integ_of (w BIT x)) = (~x & iszero (integ_of w))"; |
5491 | 298 |
by (Simp_tac 1); |
299 |
by (int_case_tac "integ_of w" 1); |
|
300 |
by (ALLGOALS (asm_simp_tac |
|
5540 | 301 |
(simpset() addsimps zcompare_rls @ |
302 |
[zminus_zadd_distrib RS sym, |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
303 |
zadd_int]))); |
5512 | 304 |
qed "iszero_integ_of_BIT"; |
5491 | 305 |
|
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
306 |
Goal "iszero (integ_of (w BIT False)) = iszero (integ_of w)"; |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
307 |
by (simp_tac (HOL_ss addsimps [iszero_integ_of_BIT]) 1); |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
308 |
qed "iszero_integ_of_0"; |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
309 |
|
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
310 |
Goal "~ iszero (integ_of (w BIT True))"; |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
311 |
by (simp_tac (HOL_ss addsimps [iszero_integ_of_BIT]) 1); |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
312 |
qed "iszero_integ_of_1"; |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
313 |
|
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
314 |
|
5491 | 315 |
|
316 |
(** Less-than (<) **) |
|
317 |
||
318 |
Goalw [zless_def,zdiff_def] |
|
319 |
"integ_of x < integ_of y \ |
|
5540 | 320 |
\ = neg (integ_of (bin_add x (bin_minus y)))"; |
5491 | 321 |
by (simp_tac (simpset() addsimps bin_mult_simps) 1); |
5540 | 322 |
qed "less_integ_of_eq_neg"; |
5491 | 323 |
|
5540 | 324 |
Goal "~ neg (integ_of Pls)"; |
5491 | 325 |
by (Simp_tac 1); |
5512 | 326 |
qed "not_neg_integ_of_Pls"; |
5491 | 327 |
|
5540 | 328 |
Goal "neg (integ_of Min)"; |
5491 | 329 |
by (Simp_tac 1); |
5512 | 330 |
qed "neg_integ_of_Min"; |
5491 | 331 |
|
5540 | 332 |
Goal "neg (integ_of (w BIT x)) = neg (integ_of w)"; |
5491 | 333 |
by (Asm_simp_tac 1); |
334 |
by (int_case_tac "integ_of w" 1); |
|
335 |
by (ALLGOALS (asm_simp_tac |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
336 |
(simpset() addsimps [zadd_int, neg_eq_less_nat0, |
5540 | 337 |
symmetric zdiff_def] @ zcompare_rls))); |
5512 | 338 |
qed "neg_integ_of_BIT"; |
5491 | 339 |
|
340 |
||
341 |
(** Less-than-or-equals (<=) **) |
|
342 |
||
343 |
Goal "(integ_of x <= integ_of y) = (~ integ_of y < integ_of x)"; |
|
344 |
by (simp_tac (simpset() addsimps [zle_def]) 1); |
|
345 |
qed "le_integ_of_eq_not_less"; |
|
346 |
||
5540 | 347 |
(*Delete the original rewrites, with their clumsy conditional expressions*) |
5551 | 348 |
Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT, |
349 |
NCons_Pls, NCons_Min, bin_add_BIT, bin_mult_BIT]; |
|
5491 | 350 |
|
351 |
(*Hide the binary representation of integer constants*) |
|
5540 | 352 |
Delsimps [integ_of_Pls, integ_of_Min, integ_of_BIT]; |
5491 | 353 |
|
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
354 |
(*simplification of arithmetic operations on integer constants*) |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
355 |
val bin_arith_extra_simps = |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
356 |
[integ_of_add RS sym, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
357 |
integ_of_minus RS sym, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
358 |
integ_of_mult RS sym, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
359 |
bin_succ_1, bin_succ_0, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
360 |
bin_pred_1, bin_pred_0, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
361 |
bin_minus_1, bin_minus_0, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
362 |
bin_add_Pls_right, bin_add_BIT_Min, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
363 |
bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
364 |
diff_integ_of_eq, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
365 |
bin_mult_1, bin_mult_0, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
366 |
NCons_Pls_0, NCons_Pls_1, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
367 |
NCons_Min_0, NCons_Min_1, NCons_BIT]; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
368 |
|
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
369 |
(*For making a minimal simpset, one must include these default simprules |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
370 |
of Bin.thy. Also include simp_thms, or at least (~False)=True*) |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
371 |
val bin_arith_simps = |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
372 |
[bin_pred_Pls, bin_pred_Min, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
373 |
bin_succ_Pls, bin_succ_Min, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
374 |
bin_add_Pls, bin_add_Min, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
375 |
bin_minus_Pls, bin_minus_Min, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
376 |
bin_mult_Pls, bin_mult_Min] @ bin_arith_extra_simps; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
377 |
|
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
378 |
(*Simplification of relational operations*) |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
379 |
val bin_rel_simps = |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
380 |
[eq_integ_of_eq, iszero_integ_of_Pls, nonzero_integ_of_Min, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
381 |
iszero_integ_of_0, iszero_integ_of_1, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
382 |
less_integ_of_eq_neg, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
383 |
not_neg_integ_of_Pls, neg_integ_of_Min, neg_integ_of_BIT, |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
384 |
le_integ_of_eq_not_less]; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
1894
diff
changeset
|
385 |
|
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
386 |
Addsimps bin_arith_extra_simps; |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
387 |
Addsimps bin_rel_simps; |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
388 |
|
6060 | 389 |
(*---------------------------------------------------------------------------*) |
390 |
(* Linear arithmetic *) |
|
391 |
(*---------------------------------------------------------------------------*) |
|
392 |
||
393 |
(* |
|
394 |
Instantiation of the generic linear arithmetic package for int. |
|
395 |
FIXME: multiplication with constants (eg #2 * i) does not work yet. |
|
396 |
Solution: the cancellation simprocs in Int_Cancel should be able to deal with |
|
397 |
it (eg simplify #3 * i <= 2 * i to i <= #0) or `add_rules' below should |
|
398 |
include rules for turning multiplication with constants into addition. |
|
399 |
(The latter option is very inefficient!) |
|
400 |
*) |
|
401 |
||
402 |
structure Int_LA_Data: LIN_ARITH_DATA = |
|
403 |
struct |
|
404 |
val ccontr = ccontr; |
|
405 |
val conjI = conjI; |
|
406 |
val lessD = add1_zle_eq RS iffD2; |
|
407 |
val neqE = int_neqE; |
|
408 |
val notI = notI; |
|
409 |
val not_leD = not_zleE RS lessD; |
|
410 |
val not_lessD = zleI; |
|
411 |
val sym = sym; |
|
412 |
||
6073 | 413 |
val mk_Trueprop = Nat_LA_Data.mk_Trueprop; |
414 |
val neg_prop = Nat_LA_Data.neg_prop; |
|
415 |
val mkEqTrue = Nat_LA_Data.mkEqTrue; |
|
416 |
||
6060 | 417 |
val intT = Type("IntDef.int",[]); |
418 |
||
419 |
(* borrowed from Bin.thy: *) |
|
420 |
fun dest_bit (Const ("False", _)) = 0 |
|
421 |
| dest_bit (Const ("True", _)) = 1 |
|
422 |
| dest_bit _ = raise Match; |
|
423 |
||
424 |
fun dest_bin tm = |
|
425 |
let |
|
426 |
fun bin_of (Const ("Bin.bin.Pls", _)) = [] |
|
427 |
| bin_of (Const ("Bin.bin.Min", _)) = [~1] |
|
428 |
| bin_of (Const ("Bin.bin.op BIT", _) $ bs $ b) = dest_bit b :: bin_of bs |
|
429 |
| bin_of _ = raise Match; |
|
430 |
||
431 |
fun int_of [] = 0 |
|
432 |
| int_of (b :: bs) = b + 2 * int_of bs; |
|
433 |
||
434 |
in int_of(bin_of tm) end; |
|
435 |
||
436 |
fun add_atom(t,m,(p,i)) = (case assoc(p,t) of None => ((t,m)::p,i) |
|
437 |
| Some n => (overwrite(p,(t,n+m:int)), i)); |
|
438 |
||
439 |
(* Turn term into list of summand * multiplicity plus a constant *) |
|
440 |
fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi)) |
|
441 |
| poly(Const("op -",_) $ s $ t, m, pi) = poly(s,m,poly(t,~1*m,pi)) |
|
442 |
| poly(Const("uminus",_) $ t, m, pi) = poly(t,~1*m,pi) |
|
443 |
| poly(all as Const("op *",_) $ (Const("Bin.integ_of",_)$c) $ t, m, pi) = |
|
444 |
(poly(t,m*dest_bin c,pi) handle Match => add_atom(all,m,pi)) |
|
445 |
| poly(all as Const("Bin.integ_of",_)$t,m,(p,i)) = |
|
446 |
((p,i + m*dest_bin t) handle Match => add_atom(all,m,(p,i))) |
|
447 |
| poly x = add_atom x; |
|
448 |
||
449 |
fun iib T = T = ([intT,intT] ---> HOLogic.boolT); |
|
450 |
||
451 |
fun decomp2(rel,T,lhs,rhs) = |
|
452 |
if not(iib T) then None else |
|
453 |
let val (p,i) = poly(lhs,1,([],0)) and (q,j) = poly(rhs,1,([],0)) |
|
454 |
in case rel of |
|
455 |
"op <" => Some(p,i,"<",q,j) |
|
456 |
| "op <=" => Some(p,i,"<=",q,j) |
|
457 |
| "op =" => Some(p,i,"=",q,j) |
|
458 |
| _ => None |
|
459 |
end; |
|
460 |
||
461 |
fun negate(Some(x,i,rel,y,j)) = Some(x,i,"~"^rel,y,j) |
|
462 |
| negate None = None; |
|
463 |
||
464 |
fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp2(rel,T,lhs,rhs) |
|
465 |
| decomp(_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) = |
|
466 |
negate(decomp2(rel,T,lhs,rhs)) |
|
467 |
| decomp _ = None |
|
468 |
||
469 |
(* reduce contradictory <= to False *) |
|
470 |
val add_rules = simp_thms@bin_arith_simps@bin_rel_simps@[int_0]; |
|
471 |
||
472 |
val cancel_sums_ss = HOL_basic_ss addsimps add_rules |
|
473 |
addsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv]; |
|
474 |
||
475 |
val simp = simplify cancel_sums_ss; |
|
476 |
||
477 |
val add_mono_thms = map (fn s => prove_goal Int.thy s |
|
478 |
(fn prems => [cut_facts_tac prems 1, |
|
479 |
asm_simp_tac (simpset() addsimps [zadd_zle_mono]) 1])) |
|
480 |
["(i <= j) & (k <= l) ==> i + k <= j + (l::int)", |
|
481 |
"(i = j) & (k <= l) ==> i + k <= j + (l::int)", |
|
482 |
"(i <= j) & (k = l) ==> i + k <= j + (l::int)", |
|
483 |
"(i = j) & (k = l) ==> i + k = j + (l::int)" |
|
484 |
]; |
|
485 |
||
486 |
fun is_False thm = |
|
487 |
let val _ $ t = #prop(rep_thm thm) |
|
488 |
in t = Const("False",HOLogic.boolT) end; |
|
489 |
||
490 |
fun is_nat(t) = false; |
|
491 |
||
492 |
fun mk_nat_thm sg t = sys_error "Int/mk_nat_thm"; |
|
493 |
||
494 |
end; |
|
495 |
||
496 |
structure Fast_Int_Arith = Fast_Lin_Arith(Int_LA_Data); |
|
497 |
||
498 |
val fast_int_arith_tac = Fast_Int_Arith.lin_arith_tac; |
|
499 |
||
500 |
simpset_ref () := (simpset() addSolver Fast_Int_Arith.cut_lin_arith_tac); |
|
501 |
||
502 |
(* FIXME: K true should be replaced by a sensible test to speed things up |
|
503 |
in case there are lots of irrelevant terms involved. |
|
504 |
*) |
|
505 |
val int_arith_tac = |
|
506 |
refute_tac (K true) (K all_tac) |
|
507 |
((REPEAT o etac int_neqE) THEN' fast_int_arith_tac); |
|
508 |
||
509 |
(* Some test data |
|
510 |
Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d"; |
|
511 |
by(fast_int_arith_tac 1); |
|
512 |
Goal "!!a::int. [| a < b; c < d |] ==> a-d+ #2 <= b+(-c)"; |
|
513 |
by(fast_int_arith_tac 1); |
|
514 |
Goal "!!a::int. [| a < b; c < d |] ==> a+c+ #1 < b+d"; |
|
515 |
by(fast_int_arith_tac 1); |
|
516 |
Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c"; |
|
517 |
by(fast_int_arith_tac 1); |
|
518 |
Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \ |
|
519 |
\ ==> a+a <= j+j"; |
|
520 |
by(fast_int_arith_tac 1); |
|
521 |
Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \ |
|
522 |
\ ==> a+a - - #-1 < j+j - #3"; |
|
523 |
by(fast_int_arith_tac 1); |
|
524 |
Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"; |
|
525 |
by(int_arith_tac 1); |
|
526 |
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
|
527 |
\ ==> a <= l"; |
|
528 |
by(fast_int_arith_tac 1); |
|
529 |
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
|
530 |
\ ==> a+a+a+a <= l+l+l+l"; |
|
531 |
by(fast_int_arith_tac 1); |
|
532 |
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
|
533 |
\ ==> a+a+a+a+a <= l+l+l+l+i"; |
|
534 |
by(fast_int_arith_tac 1); |
|
535 |
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
|
536 |
\ ==> a+a+a+a+a+a <= l+l+l+l+i+l"; |
|
537 |
by(fast_int_arith_tac 1); |
|
538 |
*) |
|
539 |
||
540 |
(*---------------------------------------------------------------------------*) |
|
541 |
(* End of linear arithmetic *) |
|
542 |
(*---------------------------------------------------------------------------*) |
|
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
543 |
|
5592 | 544 |
(** Simplification of arithmetic when nested to the right **) |
545 |
||
546 |
Goal "integ_of v + (integ_of w + z) = integ_of(bin_add v w) + z"; |
|
547 |
by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1); |
|
548 |
qed "add_integ_of_left"; |
|
549 |
||
550 |
Goal "integ_of v * (integ_of w * z) = integ_of(bin_mult v w) * z"; |
|
551 |
by (simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1); |
|
552 |
qed "mult_integ_of_left"; |
|
553 |
||
554 |
Addsimps [add_integ_of_left, mult_integ_of_left]; |
|
555 |
||
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
556 |
(** Simplification of inequalities involving numerical constants **) |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
557 |
|
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
558 |
Goal "(w <= z + #1) = (w<=z | w = z + #1)"; |
6060 | 559 |
by(int_arith_tac 1); |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
560 |
qed "zle_add1_eq"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
561 |
|
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
562 |
Goal "(w <= z - #1) = (w<z)"; |
6060 | 563 |
by(int_arith_tac 1); |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
564 |
qed "zle_diff1_eq"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
565 |
Addsimps [zle_diff1_eq]; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
566 |
|
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
567 |
(*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
|
568 |
Goal "[| w <= z; #0 <= v |] ==> w <= z + v"; |
6060 | 569 |
by(fast_int_arith_tac 1); |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
570 |
qed "zle_imp_zle_zadd"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
571 |
|
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
572 |
Goal "w <= z ==> w <= z + #1"; |
6060 | 573 |
by(fast_int_arith_tac 1); |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
574 |
qed "zle_imp_zle_zadd1"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
575 |
|
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
576 |
(*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
|
577 |
Goal "[| w < z; #0 <= v |] ==> w < z + v"; |
6060 | 578 |
by(fast_int_arith_tac 1); |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
579 |
qed "zless_imp_zless_zadd"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
580 |
|
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
581 |
Goal "w < z ==> w < z + #1"; |
6060 | 582 |
by(fast_int_arith_tac 1); |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
583 |
qed "zless_imp_zless_zadd1"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
584 |
|
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
585 |
Goal "(w < z + #1) = (w<=z)"; |
6060 | 586 |
by(int_arith_tac 1); |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
587 |
qed "zle_add1_eq_le"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
588 |
Addsimps [zle_add1_eq_le]; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
589 |
|
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
590 |
Goal "(z = z + w) = (w = #0)"; |
6060 | 591 |
by(int_arith_tac 1); |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
592 |
qed "zadd_left_cancel0"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
593 |
Addsimps [zadd_left_cancel0]; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
594 |
|
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
595 |
(*LOOPS as a simprule!*) |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
596 |
Goal "[| w + v < z; #0 <= v |] ==> w < z"; |
6060 | 597 |
by(fast_int_arith_tac 1); |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
598 |
qed "zless_zadd_imp_zless"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
599 |
|
5540 | 600 |
(*LOOPS as a simprule! Analogous to Suc_lessD*) |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
601 |
Goal "w + #1 < z ==> w < z"; |
6060 | 602 |
by(fast_int_arith_tac 1); |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
603 |
qed "zless_zadd1_imp_zless"; |
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
604 |
|
5551 | 605 |
Goal "w + #-1 = w - #1"; |
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
606 |
by (Simp_tac 1); |
5551 | 607 |
qed "zplus_minus1_conv"; |
5510
ad120f7c52ad
improved (but still flawed) treatment of binary arithmetic
paulson
parents:
5491
diff
changeset
|
608 |
|
5551 | 609 |
|
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
610 |
(*** nat ***) |
5551 | 611 |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
612 |
Goal "#0 <= z ==> int (nat z) = z"; |
5551 | 613 |
by (asm_full_simp_tac |
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
614 |
(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
|
615 |
qed "nat_0_le"; |
5551 | 616 |
|
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
617 |
Goal "z < #0 ==> nat z = 0"; |
5551 | 618 |
by (asm_full_simp_tac |
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
619 |
(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
|
620 |
qed "nat_less_0"; |
5551 | 621 |
|
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
622 |
Addsimps [nat_0_le, nat_less_0]; |
5551 | 623 |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
624 |
Goal "#0 <= w ==> (nat w = m) = (w = int m)"; |
5551 | 625 |
by Auto_tac; |
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
626 |
qed "nat_eq_iff"; |
5551 | 627 |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
628 |
Goal "#0 <= w ==> (nat w < m) = (w < int m)"; |
5551 | 629 |
by (rtac iffI 1); |
630 |
by (asm_full_simp_tac |
|
5582
a356fb49e69e
many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents:
5562
diff
changeset
|
631 |
(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
|
632 |
by (etac (nat_0_le RS subst) 1); |
5551 | 633 |
by (Simp_tac 1); |
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
634 |
qed "nat_less_iff"; |
5551 | 635 |
|
5747 | 636 |
|
5779
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
637 |
(*Users don't want to see (int 0) or w + - z*) |
5c74f003a68e
Explicit (and improved) simprules for binary arithmetic.
paulson
parents:
5747
diff
changeset
|
638 |
Addsimps [int_0, symmetric zdiff_def]; |
5747 | 639 |
|
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
640 |
Goal "#0 <= w ==> (nat w < nat z) = (w<z)"; |
5551 | 641 |
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
|
642 |
by (auto_tac (claset(), simpset() addsimps [nat_less_iff])); |
5551 | 643 |
by (auto_tac (claset() addIs [zless_trans], |
5747 | 644 |
simpset() addsimps [neg_eq_less_0, zle_def])); |
5562
02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
5551
diff
changeset
|
645 |
qed "nat_less_eq_zless"; |
5747 | 646 |