author | paulson |
Thu, 07 Sep 2000 17:36:37 +0200 | |
changeset 9883 | c1c8647af477 |
parent 9578 | ab26d6c8ebfe |
child 9909 | 111ccda5009b |
permissions | -rw-r--r-- |
5528 | 1 |
(* Title: ZF/ex/Bin.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1994 University of Cambridge |
|
5 |
||
6 |
Arithmetic on binary integers. |
|
7 |
*) |
|
8 |
||
6046 | 9 |
|
6153 | 10 |
AddTCs bin.intrs; |
5528 | 11 |
|
6046 | 12 |
Goal "NCons(Pls,0) = Pls"; |
5528 | 13 |
by (Asm_simp_tac 1); |
14 |
qed "NCons_Pls_0"; |
|
15 |
||
6153 | 16 |
Goal "NCons(Pls,1) = Pls BIT 1"; |
5528 | 17 |
by (Asm_simp_tac 1); |
18 |
qed "NCons_Pls_1"; |
|
19 |
||
6153 | 20 |
Goal "NCons(Min,0) = Min BIT 0"; |
5528 | 21 |
by (Asm_simp_tac 1); |
22 |
qed "NCons_Min_0"; |
|
23 |
||
6046 | 24 |
Goal "NCons(Min,1) = Min"; |
5528 | 25 |
by (Asm_simp_tac 1); |
26 |
qed "NCons_Min_1"; |
|
27 |
||
6153 | 28 |
Goal "NCons(w BIT x,b) = w BIT x BIT b"; |
5528 | 29 |
by (asm_simp_tac (simpset() addsimps bin.case_eqns) 1); |
6153 | 30 |
qed "NCons_BIT"; |
5528 | 31 |
|
32 |
val NCons_simps = [NCons_Pls_0, NCons_Pls_1, |
|
33 |
NCons_Min_0, NCons_Min_1, |
|
6153 | 34 |
NCons_BIT]; |
6046 | 35 |
Addsimps NCons_simps; |
36 |
||
5528 | 37 |
|
38 |
(** Type checking **) |
|
39 |
||
6046 | 40 |
Goal "w: bin ==> integ_of(w) : int"; |
6065 | 41 |
by (induct_tac "w" 1); |
6153 | 42 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [bool_into_nat]))); |
5528 | 43 |
qed "integ_of_type"; |
6153 | 44 |
AddTCs [integ_of_type]; |
5528 | 45 |
|
6046 | 46 |
Goal "[| w: bin; b: bool |] ==> NCons(w,b) : bin"; |
6065 | 47 |
by (induct_tac "w" 1); |
6046 | 48 |
by Auto_tac; |
5528 | 49 |
qed "NCons_type"; |
6153 | 50 |
AddTCs [NCons_type]; |
5528 | 51 |
|
6046 | 52 |
Goal "w: bin ==> bin_succ(w) : bin"; |
6065 | 53 |
by (induct_tac "w" 1); |
6046 | 54 |
by Auto_tac; |
5528 | 55 |
qed "bin_succ_type"; |
6153 | 56 |
AddTCs [bin_succ_type]; |
5528 | 57 |
|
6046 | 58 |
Goal "w: bin ==> bin_pred(w) : bin"; |
6065 | 59 |
by (induct_tac "w" 1); |
6046 | 60 |
by Auto_tac; |
61 |
qed "bin_pred_type"; |
|
6153 | 62 |
AddTCs [bin_pred_type]; |
5528 | 63 |
|
6046 | 64 |
Goal "w: bin ==> bin_minus(w) : bin"; |
6065 | 65 |
by (induct_tac "w" 1); |
6046 | 66 |
by Auto_tac; |
67 |
qed "bin_minus_type"; |
|
6153 | 68 |
AddTCs [bin_minus_type]; |
5528 | 69 |
|
6046 | 70 |
(*This proof is complicated by the mutual recursion*) |
9207 | 71 |
Goalw [bin_add_def] "v: bin ==> ALL w: bin. bin_add(v,w) : bin"; |
6065 | 72 |
by (induct_tac "v" 1); |
6046 | 73 |
by (rtac ballI 3); |
6065 | 74 |
by (rename_tac "w'" 3); |
75 |
by (induct_tac "w'" 3); |
|
6153 | 76 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [NCons_type]))); |
6112 | 77 |
qed_spec_mp "bin_add_type"; |
6153 | 78 |
AddTCs [bin_add_type]; |
5528 | 79 |
|
6046 | 80 |
Goal "[| v: bin; w: bin |] ==> bin_mult(v,w) : bin"; |
6065 | 81 |
by (induct_tac "v" 1); |
6046 | 82 |
by Auto_tac; |
83 |
qed "bin_mult_type"; |
|
6153 | 84 |
AddTCs [bin_mult_type]; |
5528 | 85 |
|
86 |
||
87 |
(**** The carry/borrow functions, bin_succ and bin_pred ****) |
|
88 |
||
89 |
(*NCons preserves the integer value of its argument*) |
|
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
90 |
Goal "[| w: bin; b: bool |] ==> integ_of(NCons(w,b)) = integ_of(w BIT b)"; |
5528 | 91 |
by (etac bin.elim 1); |
6046 | 92 |
by (Asm_simp_tac 3); |
5528 | 93 |
by (ALLGOALS (etac boolE)); |
6046 | 94 |
by (ALLGOALS Asm_simp_tac); |
5528 | 95 |
qed "integ_of_NCons"; |
96 |
||
97 |
Addsimps [integ_of_NCons]; |
|
98 |
||
99 |
Goal "w: bin ==> integ_of(bin_succ(w)) = $#1 $+ integ_of(w)"; |
|
100 |
by (etac bin.induct 1); |
|
101 |
by (Simp_tac 1); |
|
102 |
by (Simp_tac 1); |
|
103 |
by (etac boolE 1); |
|
104 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac))); |
|
105 |
qed "integ_of_succ"; |
|
106 |
||
9548 | 107 |
Goal "w: bin ==> integ_of(bin_pred(w)) = $- ($#1) $+ integ_of(w)"; |
5528 | 108 |
by (etac bin.induct 1); |
109 |
by (Simp_tac 1); |
|
110 |
by (Simp_tac 1); |
|
111 |
by (etac boolE 1); |
|
112 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac))); |
|
113 |
qed "integ_of_pred"; |
|
114 |
||
6046 | 115 |
Addsimps [integ_of_succ, integ_of_pred]; |
5528 | 116 |
|
117 |
||
118 |
(*** bin_minus: (unary!) negation of binary integers ***) |
|
119 |
||
9548 | 120 |
Goal "w: bin ==> integ_of(bin_minus(w)) = $- integ_of(w)"; |
5528 | 121 |
by (etac bin.induct 1); |
122 |
by (Simp_tac 1); |
|
123 |
by (Simp_tac 1); |
|
124 |
by (etac boolE 1); |
|
125 |
by (ALLGOALS |
|
126 |
(asm_simp_tac (simpset() addsimps zadd_ac@[zminus_zadd_distrib]))); |
|
127 |
qed "integ_of_minus"; |
|
128 |
||
129 |
||
130 |
(*** bin_add: binary addition ***) |
|
131 |
||
9207 | 132 |
Goalw [bin_add_def] "w: bin ==> bin_add(Pls,w) = w"; |
5528 | 133 |
by (Asm_simp_tac 1); |
134 |
qed "bin_add_Pls"; |
|
135 |
||
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
136 |
Goalw [bin_add_def] "w: bin ==> bin_add(w,Pls) = w"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
137 |
by (etac bin.induct 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
138 |
by Auto_tac; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
139 |
qed "bin_add_Pls_right"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
140 |
|
9207 | 141 |
Goalw [bin_add_def] "w: bin ==> bin_add(Min,w) = bin_pred(w)"; |
5528 | 142 |
by (Asm_simp_tac 1); |
143 |
qed "bin_add_Min"; |
|
144 |
||
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
145 |
Goalw [bin_add_def] "w: bin ==> bin_add(w,Min) = bin_pred(w)"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
146 |
by (etac bin.induct 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
147 |
by Auto_tac; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
148 |
qed "bin_add_Min_right"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
149 |
|
9207 | 150 |
Goalw [bin_add_def] "bin_add(v BIT x,Pls) = v BIT x"; |
5528 | 151 |
by (Simp_tac 1); |
6153 | 152 |
qed "bin_add_BIT_Pls"; |
5528 | 153 |
|
9207 | 154 |
Goalw [bin_add_def] "bin_add(v BIT x,Min) = bin_pred(v BIT x)"; |
5528 | 155 |
by (Simp_tac 1); |
6153 | 156 |
qed "bin_add_BIT_Min"; |
5528 | 157 |
|
9207 | 158 |
Goalw [bin_add_def] "[| w: bin; y: bool |] \ |
6153 | 159 |
\ ==> bin_add(v BIT x, w BIT y) = \ |
6046 | 160 |
\ NCons(bin_add(v, cond(x and y, bin_succ(w), w)), x xor y)"; |
5528 | 161 |
by (Asm_simp_tac 1); |
6153 | 162 |
qed "bin_add_BIT_BIT"; |
5528 | 163 |
|
6153 | 164 |
Addsimps [bin_add_Pls, bin_add_Min, bin_add_BIT_Pls, |
165 |
bin_add_BIT_Min, bin_add_BIT_BIT, |
|
5528 | 166 |
integ_of_succ, integ_of_pred]; |
167 |
||
168 |
Goal "v: bin ==> \ |
|
6046 | 169 |
\ ALL w: bin. integ_of(bin_add(v,w)) = integ_of(v) $+ integ_of(w)"; |
5528 | 170 |
by (etac bin.induct 1); |
171 |
by (Simp_tac 1); |
|
172 |
by (Simp_tac 1); |
|
173 |
by (rtac ballI 1); |
|
6065 | 174 |
by (induct_tac "wa" 1); |
5528 | 175 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac setloop (etac boolE)))); |
6112 | 176 |
qed_spec_mp "integ_of_add"; |
5528 | 177 |
|
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
178 |
(*Subtraction*) |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
179 |
Goalw [zdiff_def] |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
180 |
"[| v: bin; w: bin |] \ |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
181 |
\ ==> integ_of(v) $- integ_of(w) = integ_of(bin_add (v, bin_minus(w)))"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
182 |
by (asm_simp_tac (simpset() addsimps [integ_of_add, integ_of_minus]) 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
183 |
qed "diff_integ_of_eq"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
184 |
|
5528 | 185 |
|
9207 | 186 |
(*** bin_mult: binary multiplication ***) |
5528 | 187 |
|
6046 | 188 |
Goal "[| v: bin; w: bin |] \ |
189 |
\ ==> integ_of(bin_mult(v,w)) = integ_of(v) $* integ_of(w)"; |
|
6065 | 190 |
by (induct_tac "v" 1); |
5528 | 191 |
by (Asm_simp_tac 1); |
6153 | 192 |
by (asm_simp_tac (simpset() addsimps [integ_of_minus]) 1); |
5528 | 193 |
by (etac boolE 1); |
194 |
by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib]) 2); |
|
6153 | 195 |
by (asm_simp_tac (simpset() addsimps [integ_of_add, |
196 |
zadd_zmult_distrib] @ zadd_ac) 1); |
|
5528 | 197 |
qed "integ_of_mult"; |
198 |
||
199 |
(**** Computations ****) |
|
200 |
||
201 |
(** extra rules for bin_succ, bin_pred **) |
|
202 |
||
6153 | 203 |
Goal "bin_succ(w BIT 1) = bin_succ(w) BIT 0"; |
5528 | 204 |
by (Simp_tac 1); |
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
205 |
qed "bin_succ_1"; |
5528 | 206 |
|
6153 | 207 |
Goal "bin_succ(w BIT 0) = NCons(w,1)"; |
5528 | 208 |
by (Simp_tac 1); |
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
209 |
qed "bin_succ_0"; |
5528 | 210 |
|
6153 | 211 |
Goal "bin_pred(w BIT 1) = NCons(w,0)"; |
5528 | 212 |
by (Simp_tac 1); |
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
213 |
qed "bin_pred_1"; |
5528 | 214 |
|
6153 | 215 |
Goal "bin_pred(w BIT 0) = bin_pred(w) BIT 1"; |
5528 | 216 |
by (Simp_tac 1); |
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
217 |
qed "bin_pred_0"; |
5528 | 218 |
|
219 |
(** extra rules for bin_minus **) |
|
220 |
||
6153 | 221 |
Goal "bin_minus(w BIT 1) = bin_pred(NCons(bin_minus(w), 0))"; |
5528 | 222 |
by (Simp_tac 1); |
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
223 |
qed "bin_minus_1"; |
5528 | 224 |
|
6153 | 225 |
Goal "bin_minus(w BIT 0) = bin_minus(w) BIT 0"; |
5528 | 226 |
by (Simp_tac 1); |
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
227 |
qed "bin_minus_0"; |
5528 | 228 |
|
229 |
(** extra rules for bin_add **) |
|
230 |
||
6153 | 231 |
Goal "w: bin ==> bin_add(v BIT 1, w BIT 1) = \ |
5528 | 232 |
\ NCons(bin_add(v, bin_succ(w)), 0)"; |
233 |
by (Asm_simp_tac 1); |
|
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
234 |
qed "bin_add_BIT_11"; |
5528 | 235 |
|
6153 | 236 |
Goal "w: bin ==> bin_add(v BIT 1, w BIT 0) = \ |
5528 | 237 |
\ NCons(bin_add(v,w), 1)"; |
238 |
by (Asm_simp_tac 1); |
|
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
239 |
qed "bin_add_BIT_10"; |
5528 | 240 |
|
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
241 |
Goal "[| w: bin; y: bool |] \ |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
242 |
\ ==> bin_add(v BIT 0, w BIT y) = NCons(bin_add(v,w), y)"; |
5528 | 243 |
by (Asm_simp_tac 1); |
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
244 |
qed "bin_add_BIT_0"; |
5528 | 245 |
|
246 |
(** extra rules for bin_mult **) |
|
247 |
||
6153 | 248 |
Goal "bin_mult(v BIT 1, w) = bin_add(NCons(bin_mult(v,w),0), w)"; |
5528 | 249 |
by (Simp_tac 1); |
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
250 |
qed "bin_mult_1"; |
5528 | 251 |
|
6153 | 252 |
Goal "bin_mult(v BIT 0, w) = NCons(bin_mult(v,w),0)"; |
5528 | 253 |
by (Simp_tac 1); |
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
254 |
qed "bin_mult_0"; |
5528 | 255 |
|
256 |
||
9548 | 257 |
(** Simplification rules with integer constants **) |
258 |
||
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
259 |
Goal "$#0 = #0"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
260 |
by (Simp_tac 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
261 |
qed "int_of_0"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
262 |
|
9576
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
263 |
Goal "$# succ(n) = #1 $+ $#n"; |
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
264 |
by (simp_tac (simpset() addsimps [int_of_add RS sym, natify_succ]) 1); |
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
265 |
qed "int_of_succ"; |
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
266 |
|
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
267 |
Goal "$- #0 = #0"; |
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
268 |
by (Simp_tac 1); |
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
269 |
qed "zminus_0"; |
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
270 |
|
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
271 |
Addsimps [zminus_0]; |
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
272 |
|
9548 | 273 |
Goal "#0 $+ z = intify(z)"; |
274 |
by (Simp_tac 1); |
|
275 |
qed "zadd_0_intify"; |
|
276 |
||
277 |
Goal "z $+ #0 = intify(z)"; |
|
278 |
by (Simp_tac 1); |
|
279 |
qed "zadd_0_right_intify"; |
|
280 |
||
281 |
Addsimps [zadd_0_intify, zadd_0_right_intify]; |
|
282 |
||
283 |
Goal "#1 $* z = intify(z)"; |
|
284 |
by (Simp_tac 1); |
|
285 |
qed "zmult_1_intify"; |
|
286 |
||
287 |
Goal "z $* #1 = intify(z)"; |
|
288 |
by (stac zmult_commute 1); |
|
289 |
by (Simp_tac 1); |
|
290 |
qed "zmult_1_right_intify"; |
|
291 |
||
292 |
Addsimps [zmult_1_intify, zmult_1_right_intify]; |
|
293 |
||
294 |
Goal "#0 $* z = #0"; |
|
295 |
by (Simp_tac 1); |
|
296 |
qed "zmult_0"; |
|
297 |
||
298 |
Goal "z $* #0 = #0"; |
|
299 |
by (stac zmult_commute 1); |
|
300 |
by (Simp_tac 1); |
|
301 |
qed "zmult_0_right"; |
|
302 |
||
303 |
Addsimps [zmult_0, zmult_0_right]; |
|
304 |
||
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
305 |
Goal "#-1 $* z = $-z"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
306 |
by (simp_tac (simpset() addsimps zcompare_rls) 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
307 |
qed "zmult_minus1"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
308 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
309 |
Goal "z $* #-1 = $-z"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
310 |
by (stac zmult_commute 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
311 |
by (rtac zmult_minus1 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
312 |
qed "zmult_minus1_right"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
313 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
314 |
Addsimps [zmult_minus1, zmult_minus1_right]; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
315 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
316 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
317 |
(*** Simplification rules for comparison of binary numbers (N Voelker) ***) |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
318 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
319 |
(** Equals (=) **) |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
320 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
321 |
Goalw [iszero_def] |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
322 |
"[| v: bin; w: bin |] \ |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
323 |
\ ==> ((integ_of(v)) = integ_of(w)) <-> \ |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
324 |
\ iszero (integ_of (bin_add (v, bin_minus(w))))"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
325 |
by (asm_simp_tac (simpset() addsimps |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
326 |
(zcompare_rls @ [integ_of_add, integ_of_minus])) 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
327 |
qed "eq_integ_of_eq"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
328 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
329 |
Goalw [iszero_def] "iszero (integ_of(Pls))"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
330 |
by (Simp_tac 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
331 |
qed "iszero_integ_of_Pls"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
332 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
333 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
334 |
Goalw [iszero_def] "~ iszero (integ_of(Min))"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
335 |
by (simp_tac (simpset() addsimps [zminus_equation]) 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
336 |
qed "nonzero_integ_of_Min"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
337 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
338 |
Goalw [iszero_def] |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
339 |
"[| w: bin; x: bool |] \ |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
340 |
\ ==> iszero (integ_of (w BIT x)) <-> (x=0 & iszero (integ_of(w)))"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
341 |
by (Simp_tac 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
342 |
by (subgoal_tac "integ_of(w) : int" 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
343 |
by (Asm_simp_tac 2); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
344 |
by (dtac int_cases 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
345 |
by (auto_tac (claset() addSEs [boolE], |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
346 |
simpset() addsimps [int_of_add RS sym])); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
347 |
by (ALLGOALS (asm_full_simp_tac |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
348 |
(simpset() addsimps zcompare_rls @ |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
349 |
[zminus_zadd_distrib RS sym, int_of_add RS sym]))); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
350 |
by (subgoal_tac "znegative ($- $# succ(x)) <-> znegative ($# succ(x))" 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
351 |
by (Asm_simp_tac 2); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
352 |
by (Full_simp_tac 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
353 |
qed "iszero_integ_of_BIT"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
354 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
355 |
Goal "w: bin ==> iszero (integ_of (w BIT 0)) <-> iszero (integ_of(w))"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
356 |
by (asm_simp_tac (ZF_ss addsimps [iszero_integ_of_BIT]) 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
357 |
qed "iszero_integ_of_0"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
358 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
359 |
Goal "w: bin ==> ~ iszero (integ_of (w BIT 1))"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
360 |
by (asm_simp_tac (ZF_ss addsimps [iszero_integ_of_BIT]) 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
361 |
qed "iszero_integ_of_1"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
362 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
363 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
364 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
365 |
(** Less-than (<) **) |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
366 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
367 |
Goalw [zless_def,zdiff_def] |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
368 |
"[| v: bin; w: bin |] \ |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
369 |
\ ==> integ_of(v) $< integ_of(w) \ |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
370 |
\ <-> znegative (integ_of (bin_add (v, bin_minus(w))))"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
371 |
by (asm_simp_tac (simpset() addsimps [integ_of_minus, integ_of_add]) 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
372 |
qed "less_integ_of_eq_neg"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
373 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
374 |
Goal "~ znegative (integ_of(Pls))"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
375 |
by (Simp_tac 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
376 |
qed "not_neg_integ_of_Pls"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
377 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
378 |
Goal "znegative (integ_of(Min))"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
379 |
by (Simp_tac 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
380 |
qed "neg_integ_of_Min"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
381 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
382 |
Goal "[| w: bin; x: bool |] \ |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
383 |
\ ==> znegative (integ_of (w BIT x)) <-> znegative (integ_of(w))"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
384 |
by (Asm_simp_tac 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
385 |
by (subgoal_tac "integ_of(w) : int" 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
386 |
by (Asm_simp_tac 2); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
387 |
by (dtac int_cases 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
388 |
by (auto_tac (claset() addSEs [boolE], |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
389 |
simpset() addsimps [int_of_add RS sym] @ zcompare_rls)); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
390 |
by (ALLGOALS (asm_full_simp_tac |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
391 |
(simpset() addsimps [zminus_zadd_distrib RS sym, zdiff_def, |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
392 |
int_of_add RS sym]))); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
393 |
by (subgoal_tac "$#1 $- $# succ(succ(x #+ x)) = $- $# succ(x #+ x)" 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
394 |
by (asm_full_simp_tac (simpset() addsimps [zdiff_def])1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
395 |
by (asm_simp_tac (simpset() addsimps [equation_zminus, int_of_diff RS sym])1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
396 |
qed "neg_integ_of_BIT"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
397 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
398 |
Goal "w: bin ==> iszero (integ_of (w BIT 0)) <-> iszero (integ_of(w))"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
399 |
by (asm_simp_tac (ZF_ss addsimps [iszero_integ_of_BIT]) 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
400 |
qed "iszero_integ_of_0"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
401 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
402 |
(** Less-than-or-equals (<=) **) |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
403 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
404 |
Goal "(integ_of(x) $<= (integ_of(w))) <-> ~ (integ_of(w) $< (integ_of(x)))"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
405 |
by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
406 |
qed "le_integ_of_eq_not_less"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
407 |
|
9548 | 408 |
|
6153 | 409 |
(*Delete the original rewrites, with their clumsy conditional expressions*) |
410 |
Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT, |
|
9207 | 411 |
NCons_Pls, NCons_Min, bin_adder_BIT, bin_mult_BIT]; |
6153 | 412 |
|
413 |
(*Hide the binary representation of integer constants*) |
|
414 |
Delsimps [integ_of_Pls, integ_of_Min, integ_of_BIT]; |
|
415 |
||
5528 | 416 |
|
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
417 |
bind_thms ("NCons_simps", |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
418 |
[NCons_Pls_0, NCons_Pls_1, NCons_Min_0, NCons_Min_1, NCons_BIT]); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
419 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
420 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
421 |
bind_thms ("bin_arith_extra_simps", |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
422 |
[integ_of_add RS sym, (*invoke bin_add*) |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
423 |
integ_of_minus RS sym, (*invoke bin_minus*) |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
424 |
integ_of_mult RS sym, (*invoke bin_mult*) |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
425 |
bin_succ_1, bin_succ_0, |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
426 |
bin_pred_1, bin_pred_0, |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
427 |
bin_minus_1, bin_minus_0, |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
428 |
bin_add_Pls_right, bin_add_Min_right, |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
429 |
bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11, |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
430 |
diff_integ_of_eq, |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
431 |
bin_mult_1, bin_mult_0] @ NCons_simps); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
432 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
433 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
434 |
(*For making a minimal simpset, one must include these default simprules |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
435 |
of thy. Also include simp_thms, or at least (~False)=True*) |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
436 |
bind_thms ("bin_arith_simps", |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
437 |
[bin_pred_Pls, bin_pred_Min, |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
438 |
bin_succ_Pls, bin_succ_Min, |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
439 |
bin_add_Pls, bin_add_Min, |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
440 |
bin_minus_Pls, bin_minus_Min, |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
441 |
bin_mult_Pls, bin_mult_Min] @ bin_arith_extra_simps); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
442 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
443 |
(*Simplification of relational operations*) |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
444 |
bind_thms ("bin_rel_simps", |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
445 |
[eq_integ_of_eq, iszero_integ_of_Pls, nonzero_integ_of_Min, |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
446 |
iszero_integ_of_0, iszero_integ_of_1, |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
447 |
less_integ_of_eq_neg, |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
448 |
not_neg_integ_of_Pls, neg_integ_of_Min, neg_integ_of_BIT, |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
449 |
le_integ_of_eq_not_less]); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
450 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
451 |
Addsimps bin_arith_simps; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
452 |
Addsimps bin_rel_simps; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
453 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
454 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
455 |
(** Simplification of arithmetic when nested to the right **) |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
456 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
457 |
Goal "[| v: bin; w: bin |] \ |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
458 |
\ ==> integ_of(v) $+ (integ_of(w) $+ z) = (integ_of(bin_add(v,w)) $+ z)"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
459 |
by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
460 |
qed "add_integ_of_left"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
461 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
462 |
Goal "[| v: bin; w: bin |] \ |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
463 |
\ ==> integ_of(v) $* (integ_of(w) $* z) = (integ_of(bin_mult(v,w)) $* z)"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
464 |
by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
465 |
qed "mult_integ_of_left"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
466 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
467 |
Goalw [zdiff_def] |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
468 |
"[| v: bin; w: bin |] \ |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
469 |
\ ==> integ_of(v) $+ (integ_of(w) $- c) = integ_of(bin_add(v,w)) $- (c)"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
470 |
by (rtac add_integ_of_left 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
471 |
by Auto_tac; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
472 |
qed "add_integ_of_diff1"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
473 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
474 |
Goal "[| v: bin; w: bin |] \ |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
475 |
\ ==> integ_of(v) $+ (c $- integ_of(w)) = \ |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
476 |
\ integ_of (bin_add (v, bin_minus(w))) $+ (c)"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
477 |
by (stac (diff_integ_of_eq RS sym) 1); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
478 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps zdiff_def::zadd_ac))); |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
479 |
qed "add_integ_of_diff2"; |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
480 |
|
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
481 |
Addsimps [add_integ_of_left, mult_integ_of_left, |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
482 |
add_integ_of_diff1, add_integ_of_diff2]; |
9576
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
483 |
|
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
484 |
|
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
485 |
(** More for integer constants **) |
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
486 |
|
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
487 |
Addsimps [int_of_0, int_of_succ]; |
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
488 |
|
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
489 |
Goal "#0 $- x = $-x"; |
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
490 |
by (simp_tac (simpset() addsimps [zdiff_def]) 1); |
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
491 |
qed "zdiff0"; |
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
492 |
|
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
493 |
Goal "x $- #0 = intify(x)"; |
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
494 |
by (simp_tac (simpset() addsimps [zdiff_def]) 1); |
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
495 |
qed "zdiff0_right"; |
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
496 |
|
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
497 |
Goal "x $- x = #0"; |
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
498 |
by (simp_tac (simpset() addsimps [zdiff_def]) 1); |
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
499 |
qed "zdiff_self"; |
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
500 |
|
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
501 |
Addsimps [zdiff0, zdiff0_right, zdiff_self]; |
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
502 |
|
9883 | 503 |
Goal "k: int ==> znegative(k) <-> k $< #0"; |
9576
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
504 |
by (asm_simp_tac (simpset() addsimps [zless_def]) 1); |
9883 | 505 |
qed "znegative_iff_zless_0"; |
9576
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
506 |
|
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
507 |
Goal "[| #0 $< k; k: int |] ==> znegative($-k)"; |
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
508 |
by (asm_full_simp_tac (simpset() addsimps [zless_def]) 1); |
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
509 |
qed "zero_zless_imp_znegative_zminus"; |
3df14e0a3a51
interim working version: more improvements to the integers
paulson
parents:
9570
diff
changeset
|
510 |
|
9883 | 511 |
Goal "#0 $<= $# n"; |
512 |
by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym, |
|
513 |
znegative_iff_zless_0 RS iff_sym]) 1); |
|
514 |
qed "zero_zle_int_of"; |
|
515 |
AddIffs [zero_zle_int_of]; |
|
516 |
||
517 |
Goal "nat_of(#0) = 0"; |
|
518 |
by (simp_tac (ZF_ss addsimps [natify_0, int_of_0 RS sym, nat_of_int_of]) 1); |
|
519 |
qed "nat_of_0"; |
|
520 |
Addsimps [nat_of_0]; |
|
521 |
||
522 |
Goal "[| z $<= $#0; z: int |] ==> nat_of(z) = 0"; |
|
523 |
by (auto_tac (claset(), |
|
524 |
simpset() addsimps [znegative_iff_zless_0 RS iff_sym, |
|
525 |
zle_def, zneg_nat_of])); |
|
526 |
val lemma = result(); |
|
527 |
||
528 |
Goal "z $<= $#0 ==> nat_of(z) = 0"; |
|
529 |
by (subgoal_tac "nat_of(intify(z)) = 0" 1); |
|
530 |
by (rtac lemma 2); |
|
531 |
by Auto_tac; |
|
532 |
qed "nat_le_int0"; |
|
533 |
||
534 |
Goal "$# n = #0 \\<Longrightarrow> natify(n) = 0"; |
|
535 |
by (rtac not_znegative_imp_zero 1); |
|
536 |
by Auto_tac; |
|
537 |
qed "int_of_eq_0_imp_natify_eq_0"; |
|
538 |
||
539 |
Goalw [nat_of_def, raw_nat_of_def] "nat_of($- $# n) = 0"; |
|
540 |
by (auto_tac((claset() addSDs [not_znegative_imp_zero, natify_int_of_eq], |
|
541 |
simpset()) delIffs [int_of_eq])); |
|
542 |
by (rtac the_equality 1); |
|
543 |
by Auto_tac; |
|
544 |
by (blast_tac (claset() addIs [int_of_eq_0_imp_natify_eq_0, sym]) 1); |
|
545 |
qed "nat_of_zminus_int_of"; |
|
546 |
||
547 |
Goal "#0 $<= z \\<Longrightarrow> $# nat_of(z) = intify(z)"; |
|
548 |
by (rtac not_zneg_nat_of_intify 1); |
|
549 |
by (asm_simp_tac (simpset() addsimps [znegative_iff_zless_0, |
|
550 |
not_zless_iff_zle]) 1); |
|
551 |
qed "int_of_nat_of"; |
|
552 |
||
553 |
Addsimps [int_of_nat_of, nat_of_zminus_int_of]; |
|
554 |
||
555 |
Goal "$# nat_of(z) = (if #0 $<= z then intify(z) else #0)"; |
|
556 |
by (simp_tac (simpset() addsimps [int_of_nat_of, |
|
557 |
znegative_iff_zless_0, not_zle_iff_zless]) 1); |
|
558 |
qed "int_of_nat_of_if"; |
|
559 |
||
560 |
Goal "[| m: nat; z: int |] ==> (m < nat_of(z)) <-> ($#m $< z)"; |
|
561 |
by (case_tac "znegative(z)" 1); |
|
562 |
by (etac (not_zneg_nat_of RS subst) 2); |
|
563 |
by (auto_tac (claset() addDs [zless_trans] |
|
564 |
addSDs [zero_zle_int_of RS zle_zless_trans], |
|
565 |
simpset() addsimps [znegative_iff_zless_0])); |
|
566 |
qed "zless_nat_iff_int_zless"; |
|
567 |
||
568 |
||
569 |
(** nat_of and zless **) |
|
570 |
||
571 |
(*An alternative condition is $#0 <= w *) |
|
572 |
Goal "$#0 $< z ==> (nat_of(w) < nat_of(z)) <-> (w $< z)"; |
|
573 |
by (rtac iff_trans 1); |
|
574 |
by (rtac (zless_int_of RS iff_sym) 1); |
|
575 |
by (auto_tac (claset(), |
|
576 |
simpset() addsimps [int_of_nat_of_if] delsimps [zless_int_of])); |
|
577 |
by (auto_tac (claset() addEs [zless_asym], |
|
578 |
simpset() addsimps [not_zle_iff_zless])); |
|
579 |
by (blast_tac (claset() addIs [zless_zle_trans]) 1); |
|
580 |
val lemma = result(); |
|
581 |
||
582 |
Goal "(nat_of(w) < nat_of(z)) <-> ($#0 $< z & w $< z)"; |
|
583 |
by (case_tac "$#0 $< z" 1); |
|
584 |
by (auto_tac (claset(), |
|
585 |
simpset() addsimps [lemma, nat_le_int0, not_zless_iff_zle])); |
|
586 |
qed "zless_nat_conj"; |
|
587 |