100 (**** integ_of ****) |
100 (**** integ_of ****) |
101 |
101 |
102 qed_goal "integ_of_norm_Bcons" Bin.thy |
102 qed_goal "integ_of_norm_Bcons" Bin.thy |
103 "integ_of(norm_Bcons w b) = integ_of(Bcons w b)" |
103 "integ_of(norm_Bcons w b) = integ_of(Bcons w b)" |
104 (fn _ =>[(induct_tac "w" 1), |
104 (fn _ =>[(induct_tac "w" 1), |
105 (ALLGOALS (asm_simp_tac |
105 (ALLGOALS Asm_simp_tac) ]); |
106 (simpset() addsimps [zadd_zminus_inverse_nat]))) ]); |
106 |
107 |
107 Addsimps [integ_of_norm_Bcons]; |
108 val integ_of_norm_Cons_simps = |
|
109 [zadd_zminus_inverse_nat, integ_of_norm_Bcons] @ zadd_ac; |
|
110 |
108 |
111 qed_goal "integ_of_succ" Bin.thy |
109 qed_goal "integ_of_succ" Bin.thy |
112 "integ_of(bin_succ w) = $#1 + integ_of w" |
110 "integ_of(bin_succ w) = $#1 + integ_of w" |
113 (fn _ =>[(rtac bin.induct 1), |
111 (fn _ =>[(rtac bin.induct 1), |
114 (ALLGOALS(asm_simp_tac (simpset() addsimps integ_of_norm_Cons_simps))) ]); |
112 (ALLGOALS(asm_simp_tac (simpset() addsimps zadd_ac))) ]); |
115 |
113 |
116 qed_goal "integ_of_pred" Bin.thy |
114 qed_goal "integ_of_pred" Bin.thy |
117 "integ_of(bin_pred w) = - ($#1) + integ_of w" |
115 "integ_of(bin_pred w) = - ($#1) + integ_of w" |
118 (fn _ =>[(rtac bin.induct 1), |
116 (fn _ =>[(rtac bin.induct 1), |
119 (ALLGOALS(asm_simp_tac (simpset() addsimps integ_of_norm_Cons_simps))) ]); |
117 (ALLGOALS(asm_simp_tac (simpset() addsimps zadd_ac))) ]); |
120 |
118 |
121 Goal "integ_of(bin_minus w) = - (integ_of w)"; |
119 Goal "integ_of(bin_minus w) = - (integ_of w)"; |
122 by (rtac bin.induct 1); |
120 by (rtac bin.induct 1); |
123 by (Simp_tac 1); |
121 by (Simp_tac 1); |
124 by (Simp_tac 1); |
122 by (Simp_tac 1); |
127 addsimps [integ_of_succ,integ_of_pred, |
125 addsimps [integ_of_succ,integ_of_pred, |
128 zadd_assoc]) 1); |
126 zadd_assoc]) 1); |
129 qed "integ_of_minus"; |
127 qed "integ_of_minus"; |
130 |
128 |
131 |
129 |
132 val bin_add_simps = [zadd_zminus_inverse_nat, zadd_zminus_inverse_nat2, |
130 val bin_add_simps = [bin_add_Bcons_Bcons, |
133 bin_add_Bcons_Plus, |
131 integ_of_succ, integ_of_pred]; |
134 bin_add_Bcons_Minus,bin_add_Bcons_Bcons, |
|
135 integ_of_succ, integ_of_pred, |
|
136 integ_of_norm_Bcons]; |
|
137 |
132 |
138 Goal "! w. integ_of(bin_add v w) = integ_of v + integ_of w"; |
133 Goal "! w. integ_of(bin_add v w) = integ_of v + integ_of w"; |
139 by (induct_tac "v" 1); |
134 by (induct_tac "v" 1); |
140 by (simp_tac (simpset() addsimps bin_add_simps) 1); |
135 by (simp_tac (simpset() addsimps bin_add_simps) 1); |
141 by (simp_tac (simpset() addsimps bin_add_simps) 1); |
136 by (simp_tac (simpset() addsimps bin_add_simps) 1); |
142 by (rtac allI 1); |
137 by (rtac allI 1); |
143 by (induct_tac "w" 1); |
138 by (induct_tac "w" 1); |
144 by (ALLGOALS (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)))); |
139 by (ALLGOALS (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)))); |
145 qed_spec_mp "integ_of_add"; |
140 qed_spec_mp "integ_of_add"; |
146 |
141 |
147 val bin_mult_simps = [zmult_zminus, |
142 val bin_mult_simps = [zmult_zminus, integ_of_minus, integ_of_add, |
148 integ_of_minus, integ_of_add, |
|
149 integ_of_norm_Bcons]; |
143 integ_of_norm_Bcons]; |
150 |
144 |
151 |
145 |
152 Goal "integ_of(bin_mult v w) = integ_of v * integ_of w"; |
146 Goal "integ_of(bin_mult v w) = integ_of v * integ_of w"; |
153 by (induct_tac "v" 1); |
147 by (induct_tac "v" 1); |
179 Goal "z + #0 = z"; |
162 Goal "z + #0 = z"; |
180 by (Simp_tac 1); |
163 by (Simp_tac 1); |
181 qed "zadd_0_right"; |
164 qed "zadd_0_right"; |
182 |
165 |
183 Goal "z + (- z) = #0"; |
166 Goal "z + (- z) = #0"; |
184 by (simp_tac (simpset() addsimps [zadd_zminus_inverse_nat]) 1); |
167 by (Simp_tac 1); |
185 qed "zadd_zminus_inverse"; |
168 qed "zadd_zminus_inverse"; |
186 |
169 |
187 Goal "(- z) + z = #0"; |
170 Goal "(- z) + z = #0"; |
188 by (simp_tac (simpset() addsimps [zadd_zminus_inverse_nat2]) 1); |
171 by (Simp_tac 1); |
189 qed "zadd_zminus_inverse2"; |
172 qed "zadd_zminus_inverse2"; |
|
173 |
|
174 (*These rewrite to $# 0. Henceforth we should rewrite to #0 *) |
|
175 Delsimps [zadd_zminus_inverse_nat, zadd_zminus_inverse_nat2]; |
190 |
176 |
191 Addsimps [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2]; |
177 Addsimps [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2]; |
192 |
178 |
193 Goal "- (#0) = #0"; |
179 Goal "- (#0) = #0"; |
194 by (Simp_tac 1); |
180 by (Simp_tac 1); |
230 |
216 |
231 Goal "(w + #1 <= z) = (w<z)"; |
217 Goal "(w + #1 <= z) = (w<z)"; |
232 by (simp_tac (simpset() addsimps [add_nat1_zle_eq]) 1); |
218 by (simp_tac (simpset() addsimps [add_nat1_zle_eq]) 1); |
233 qed "add1_zle_eq"; |
219 qed "add1_zle_eq"; |
234 Addsimps [add1_zle_eq]; |
220 Addsimps [add1_zle_eq]; |
|
221 |
|
222 Goal "znegative x = (x < #0)"; |
|
223 by (simp_tac (simpset() addsimps [znegative_eq_less_nat0]) 1); |
|
224 qed "znegative_eq_less_0"; |
|
225 |
|
226 Goal "(~znegative x) = ($# 0 <= x)"; |
|
227 by (simp_tac (simpset() addsimps [not_znegative_eq_ge_nat0]) 1); |
|
228 qed "not_znegative_eq_ge_0"; |
|
229 |
235 |
230 |
236 |
231 |
237 (** Simplification rules for comparison of binary numbers (Norbert Voelker) **) |
232 (** Simplification rules for comparison of binary numbers (Norbert Voelker) **) |
238 |
233 |
239 (** Equals (=) **) |
234 (** Equals (=) **) |
282 |
277 |
283 Goal "znegative (integ_of (Bcons w x)) = znegative (integ_of w)"; |
278 Goal "znegative (integ_of (Bcons w x)) = znegative (integ_of w)"; |
284 by (Asm_simp_tac 1); |
279 by (Asm_simp_tac 1); |
285 by (int_case_tac "integ_of w" 1); |
280 by (int_case_tac "integ_of w" 1); |
286 by (ALLGOALS (asm_simp_tac |
281 by (ALLGOALS (asm_simp_tac |
287 (simpset() addsimps ([add_znat, znegative_eq_less_0, |
282 (simpset() addsimps ([add_znat, znegative_eq_less_nat0, |
288 symmetric zdiff_def] @ |
283 symmetric zdiff_def] @ |
289 zcompare_rls)))); |
284 zcompare_rls)))); |
290 qed "neg_integ_of_Bcons"; |
285 qed "neg_integ_of_Bcons"; |
291 |
286 |
292 |
287 |
304 |
299 |
305 (*Add simplification of arithmetic operations on integer constants*) |
300 (*Add simplification of arithmetic operations on integer constants*) |
306 Addsimps [integ_of_add RS sym, |
301 Addsimps [integ_of_add RS sym, |
307 integ_of_minus RS sym, |
302 integ_of_minus RS sym, |
308 integ_of_mult RS sym, |
303 integ_of_mult RS sym, |
309 bin_succ_Bcons1,bin_succ_Bcons0, |
304 bin_succ_Bcons1, bin_succ_Bcons0, |
310 bin_pred_Bcons1,bin_pred_Bcons0, |
305 bin_pred_Bcons1, bin_pred_Bcons0, |
311 bin_minus_Bcons1,bin_minus_Bcons0, |
306 bin_minus_Bcons1, bin_minus_Bcons0, |
312 bin_add_Bcons_Plus,bin_add_Bcons_Minus, |
307 bin_add_Bcons_Plus, bin_add_Bcons_Minus, |
313 bin_add_Bcons_Bcons0,bin_add_Bcons_Bcons10,bin_add_Bcons_Bcons11, |
308 bin_add_Bcons_Bcons0, bin_add_Bcons_Bcons10, bin_add_Bcons_Bcons11, |
314 bin_mult_Bcons1,bin_mult_Bcons0, |
309 bin_mult_Bcons1, bin_mult_Bcons0, |
315 norm_Bcons_Plus_0,norm_Bcons_Plus_1, |
310 norm_Bcons_Plus_0, norm_Bcons_Plus_1, |
316 norm_Bcons_Minus_0,norm_Bcons_Minus_1, |
311 norm_Bcons_Minus_0, norm_Bcons_Minus_1, |
317 norm_Bcons_Bcons]; |
312 norm_Bcons_Bcons]; |
318 |
313 |
319 (*... and simplification of relational operations*) |
314 (*... and simplification of relational operations*) |
320 Addsimps [eq_integ_of_eq, iszero_integ_of_Plus, nonzero_integ_of_Minus, |
315 Addsimps [eq_integ_of_eq, iszero_integ_of_Plus, nonzero_integ_of_Minus, |
321 iszero_integ_of_Bcons, |
316 iszero_integ_of_Bcons, |
328 by (Simp_tac 1); |
323 by (Simp_tac 1); |
329 qed "diff_integ_of_eq"; |
324 qed "diff_integ_of_eq"; |
330 |
325 |
331 (*... and finally subtraction*) |
326 (*... and finally subtraction*) |
332 Addsimps [diff_integ_of_eq]; |
327 Addsimps [diff_integ_of_eq]; |
|
328 |
|
329 |
|
330 (** Simplification of inequalities involving numerical constants **) |
|
331 |
|
332 Goal "(w <= z + #1) = (w<=z | w = z + #1)"; |
|
333 by (simp_tac (simpset() addsimps [zle_eq_zless_or_eq, zless_add1_eq]) 1); |
|
334 qed "zle_add1_eq"; |
|
335 |
|
336 Goal "(w <= z - #1) = (w<z)"; |
|
337 by (simp_tac (simpset() addsimps zcompare_rls) 1); |
|
338 qed "zle_diff1_eq"; |
|
339 Addsimps [zle_diff1_eq]; |
|
340 |
|
341 (*2nd premise can be proved automatically if v is a literal*) |
|
342 Goal "[| w <= z; #0 <= v |] ==> w <= z + v"; |
|
343 by (dtac zadd_zle_mono 1); |
|
344 by (assume_tac 1); |
|
345 by (Full_simp_tac 1); |
|
346 qed "zle_imp_zle_zadd"; |
|
347 |
|
348 Goal "w <= z ==> w <= z + #1"; |
|
349 by (asm_simp_tac (simpset() addsimps [zle_imp_zle_zadd]) 1); |
|
350 qed "zle_imp_zle_zadd1"; |
|
351 |
|
352 (*2nd premise can be proved automatically if v is a literal*) |
|
353 Goal "[| w < z; #0 <= v |] ==> w < z + v"; |
|
354 by (dtac zadd_zless_mono 1); |
|
355 by (assume_tac 1); |
|
356 by (Full_simp_tac 1); |
|
357 qed "zless_imp_zless_zadd"; |
|
358 |
|
359 Goal "w < z ==> w < z + #1"; |
|
360 by (asm_simp_tac (simpset() addsimps [zless_imp_zless_zadd]) 1); |
|
361 qed "zless_imp_zless_zadd1"; |
|
362 |
|
363 Goal "(w < z + #1) = (w<=z)"; |
|
364 by (simp_tac (simpset() addsimps [zless_add1_eq, zle_eq_zless_or_eq]) 1); |
|
365 qed "zle_add1_eq_le"; |
|
366 Addsimps [zle_add1_eq_le]; |
|
367 |
|
368 Goal "(z = z + w) = (w = #0)"; |
|
369 by (rtac trans 1); |
|
370 by (rtac zadd_left_cancel 2); |
|
371 by (simp_tac (simpset() addsimps [eq_sym_conv]) 1); |
|
372 qed "zadd_left_cancel0"; |
|
373 Addsimps [zadd_left_cancel0]; |
|
374 |
|
375 (*LOOPS as a simprule!*) |
|
376 Goal "[| w + v < z; #0 <= v |] ==> w < z"; |
|
377 by (dtac zadd_zless_mono 1); |
|
378 by (assume_tac 1); |
|
379 by (full_simp_tac (simpset() addsimps zadd_ac) 1); |
|
380 qed "zless_zadd_imp_zless"; |
|
381 |
|
382 (*LOOPS as a simprule!*) |
|
383 Goal "w + #1 < z ==> w < z"; |
|
384 bd zless_zadd_imp_zless 1; |
|
385 ba 2; |
|
386 by (Simp_tac 1); |
|
387 qed "zless_zadd1_imp_zless"; |
|
388 |
|
389 |