136 bin_add_Bcons_Minus,bin_add_Bcons_Bcons, |
136 bin_add_Bcons_Minus,bin_add_Bcons_Bcons, |
137 integ_of_bin_succ, integ_of_bin_pred, |
137 integ_of_bin_succ, integ_of_bin_pred, |
138 integ_of_bin_norm_Bcons]; |
138 integ_of_bin_norm_Bcons]; |
139 val bin_simps = [iob_Plus,iob_Minus,iob_Bcons]; |
139 val bin_simps = [iob_Plus,iob_Minus,iob_Bcons]; |
140 |
140 |
141 Goal |
141 Goal "! w. integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w"; |
142 "! w. integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w"; |
|
143 by (induct_tac "v" 1); |
142 by (induct_tac "v" 1); |
144 by (simp_tac (simpset() addsimps bin_add_simps) 1); |
143 by (simp_tac (simpset() addsimps bin_add_simps) 1); |
145 by (simp_tac (simpset() addsimps bin_add_simps) 1); |
144 by (simp_tac (simpset() addsimps bin_add_simps) 1); |
146 by (rtac allI 1); |
145 by (rtac allI 1); |
147 by (induct_tac "w" 1); |
146 by (induct_tac "w" 1); |
149 by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1); |
148 by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1); |
150 by (cut_inst_tac [("P","bool")] True_or_False 1); |
149 by (cut_inst_tac [("P","bool")] True_or_False 1); |
151 by (etac disjE 1); |
150 by (etac disjE 1); |
152 by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1); |
151 by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1); |
153 by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1); |
152 by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1); |
154 val integ_of_bin_add_lemma = result(); |
153 qed_spec_mp "integ_of_bin_add"; |
155 |
|
156 Goal "integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w"; |
|
157 by (cut_facts_tac [integ_of_bin_add_lemma] 1); |
|
158 by (Fast_tac 1); |
|
159 qed "integ_of_bin_add"; |
|
160 |
154 |
161 val bin_mult_simps = [integ_of_bin_minus, integ_of_bin_add, |
155 val bin_mult_simps = [integ_of_bin_minus, integ_of_bin_add, |
162 integ_of_bin_norm_Bcons]; |
156 integ_of_bin_norm_Bcons]; |
163 |
157 |
164 Goal "integ_of_bin(bin_mult v w) = integ_of_bin v * integ_of_bin w"; |
158 Goal "integ_of_bin(bin_mult v w) = integ_of_bin v * integ_of_bin w"; |
193 |
187 |
194 (** Simplification rules for comparison of binary numbers (Norbert Voelker) **) |
188 (** Simplification rules for comparison of binary numbers (Norbert Voelker) **) |
195 |
189 |
196 Addsimps [zadd_assoc]; |
190 Addsimps [zadd_assoc]; |
197 |
191 |
198 Goal |
192 Goal "(integ_of_bin x = integ_of_bin y) \ |
199 "(integ_of_bin x = integ_of_bin y) \ |
|
200 \ = (integ_of_bin (bin_add x (bin_minus y)) = $# 0)"; |
193 \ = (integ_of_bin (bin_add x (bin_minus y)) = $# 0)"; |
201 by (simp_tac (HOL_ss addsimps |
194 by (simp_tac (HOL_ss addsimps |
202 [integ_of_bin_add, integ_of_bin_minus,zdiff_def]) 1); |
195 [integ_of_bin_add, integ_of_bin_minus,zdiff_def]) 1); |
203 by (rtac iffI 1); |
196 by (rtac iffI 1); |
204 by (etac ssubst 1); |
197 by (etac ssubst 1); |
216 Goal "(integ_of_bin MinusSign = $# 0) = False"; |
209 Goal "(integ_of_bin MinusSign = $# 0) = False"; |
217 by (stac iob_Minus 1); |
210 by (stac iob_Minus 1); |
218 by (Simp_tac 1); |
211 by (Simp_tac 1); |
219 val iob_Minus_not_eq_0 = result(); |
212 val iob_Minus_not_eq_0 = result(); |
220 |
213 |
221 Goal |
214 Goal "(integ_of_bin (Bcons w x) = $# 0) = (~x & integ_of_bin w = $# 0)"; |
222 "(integ_of_bin (Bcons w x) = $# 0) = (~x & integ_of_bin w = $# 0)"; |
|
223 by (stac iob_Bcons 1); |
215 by (stac iob_Bcons 1); |
224 by (case_tac "x" 1); |
216 by (case_tac "x" 1); |
225 by (ALLGOALS Asm_simp_tac); |
217 by (ALLGOALS Asm_simp_tac); |
226 by (ALLGOALS(asm_simp_tac (HOL_ss addsimps [integ_of_bin_add]))); |
218 by (ALLGOALS(asm_simp_tac (HOL_ss addsimps [integ_of_bin_add]))); |
227 by (ALLGOALS(int_case_tac "integ_of_bin w")); |
219 by (ALLGOALS(int_case_tac "integ_of_bin w")); |
228 by (ALLGOALS(asm_simp_tac |
220 by (ALLGOALS(asm_simp_tac |
229 (simpset() addsimps[zminus_zadd_distrib RS sym, |
221 (simpset() addsimps[zminus_zadd_distrib RS sym, |
230 znat_add RS sym]))); |
222 znat_add RS sym]))); |
231 by (rtac notI 1); |
223 by (rtac notI 1); |
|
224 (*Add Suc(Suc(n + n)) to both sides*) |
232 by (dres_inst_tac [("f","(% z. z + $# Suc (Suc (n + n)))")] arg_cong 1); |
225 by (dres_inst_tac [("f","(% z. z + $# Suc (Suc (n + n)))")] arg_cong 1); |
233 by (Asm_full_simp_tac 1); |
226 by (Asm_full_simp_tac 1); |
234 val iob_Bcons_eq_0 = result(); |
227 val iob_Bcons_eq_0 = result(); |
235 |
228 |
236 Goalw [zless_def,zdiff_def] |
229 Goalw [zless_def,zdiff_def] |
245 |
238 |
246 Goal "(integ_of_bin MinusSign < $# 0) = True"; |
239 Goal "(integ_of_bin MinusSign < $# 0) = True"; |
247 by (stac iob_Minus 1); by (Simp_tac 1); |
240 by (stac iob_Minus 1); by (Simp_tac 1); |
248 val iob_Minus_lt_0 = result(); |
241 val iob_Minus_lt_0 = result(); |
249 |
242 |
250 Goal |
243 Goal "(integ_of_bin (Bcons w x) < $# 0) = (integ_of_bin w < $# 0)"; |
251 "(integ_of_bin (Bcons w x) < $# 0) = (integ_of_bin w < $# 0)"; |
|
252 by (stac iob_Bcons 1); |
244 by (stac iob_Bcons 1); |
253 by (case_tac "x" 1); |
245 by (case_tac "x" 1); |
254 by (ALLGOALS Asm_simp_tac); |
246 by (ALLGOALS Asm_simp_tac); |
255 by (ALLGOALS(asm_simp_tac (HOL_ss addsimps [integ_of_bin_add]))); |
247 by (ALLGOALS(asm_simp_tac (HOL_ss addsimps [integ_of_bin_add]))); |
256 by (ALLGOALS(int_case_tac "integ_of_bin w")); |
248 by (ALLGOALS(int_case_tac "integ_of_bin w")); |
260 by (stac (zadd_zminus_inverse RS sym) 1); |
252 by (stac (zadd_zminus_inverse RS sym) 1); |
261 by (rtac zadd_zless_mono1 1); |
253 by (rtac zadd_zless_mono1 1); |
262 by (Simp_tac 1); |
254 by (Simp_tac 1); |
263 val iob_Bcons_lt_0 = result(); |
255 val iob_Bcons_lt_0 = result(); |
264 |
256 |
265 Goal |
257 Goal "integ_of_bin x <= integ_of_bin y \ |
266 "integ_of_bin x <= integ_of_bin y \ |
|
267 \ = ( integ_of_bin (bin_add x (bin_minus y)) < $# 0 \ |
258 \ = ( integ_of_bin (bin_add x (bin_minus y)) < $# 0 \ |
268 \ | integ_of_bin (bin_add x (bin_minus y)) = $# 0)"; |
259 \ | integ_of_bin (bin_add x (bin_minus y)) = $# 0)"; |
269 by (simp_tac (HOL_ss addsimps |
260 by (simp_tac (HOL_ss addsimps |
270 [zle_eq_zless_or_eq,iob_less_eq_diff_lt_0,zdiff_def |
261 [zle_eq_zless_or_eq,iob_less_eq_diff_lt_0,zdiff_def |
271 ,iob_eq_eq_diff_0,integ_of_bin_minus,integ_of_bin_add]) 1); |
262 ,iob_eq_eq_diff_0,integ_of_bin_minus,integ_of_bin_add]) 1); |