1 (* Title: HOL/Integ/Bin.ML |
1 (* Title: HOL/Integ/Bin.ML |
2 Authors: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Authors: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 David Spelt, University of Twente |
3 David Spelt, University of Twente |
4 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 Copyright 1996 University of Twente |
5 Copyright 1996 University of Twente |
6 |
6 |
7 Arithmetic on binary integers. |
7 Arithmetic on binary integers. |
8 *) |
8 *) |
9 |
9 |
10 open Bin; |
10 open Bin; |
11 |
11 |
12 (** extra rules for bin_succ, bin_pred, bin_add, bin_mult **) |
12 (** extra rules for bin_succ, bin_pred, bin_add, bin_mult **) |
13 |
13 |
14 qed_goal "norm_Bcons_Plus_0" Bin.thy "norm_Bcons Plus False = Plus" |
14 qed_goal "norm_Bcons_Plus_0" Bin.thy |
15 (fn prem => [(Simp_tac 1)]); |
15 "norm_Bcons Plus False = Plus" |
16 |
16 (fn _ => [(Simp_tac 1)]); |
17 qed_goal "norm_Bcons_Plus_1" Bin.thy "norm_Bcons Plus True = Bcons Plus True" |
17 |
18 (fn prem => [(Simp_tac 1)]); |
18 qed_goal "norm_Bcons_Plus_1" Bin.thy |
19 |
19 "norm_Bcons Plus True = Bcons Plus True" |
20 qed_goal "norm_Bcons_Minus_0" Bin.thy "norm_Bcons Minus False = Bcons Minus False" |
20 (fn _ => [(Simp_tac 1)]); |
21 (fn prem => [(Simp_tac 1)]); |
21 |
22 |
22 qed_goal "norm_Bcons_Minus_0" Bin.thy |
23 qed_goal "norm_Bcons_Minus_1" Bin.thy "norm_Bcons Minus True = Minus" |
23 "norm_Bcons Minus False = Bcons Minus False" |
24 (fn prem => [(Simp_tac 1)]); |
24 (fn _ => [(Simp_tac 1)]); |
25 |
25 |
26 qed_goal "norm_Bcons_Bcons" Bin.thy "norm_Bcons (Bcons w x) b = Bcons (Bcons w x) b" |
26 qed_goal "norm_Bcons_Minus_1" Bin.thy |
27 (fn prem => [(Simp_tac 1)]); |
27 "norm_Bcons Minus True = Minus" |
28 |
28 (fn _ => [(Simp_tac 1)]); |
29 qed_goal "bin_succ_Bcons1" Bin.thy "bin_succ(Bcons w True) = Bcons (bin_succ w) False" |
29 |
30 (fn prem => [(Simp_tac 1)]); |
30 qed_goal "norm_Bcons_Bcons" Bin.thy |
31 |
31 "norm_Bcons (Bcons w x) b = Bcons (Bcons w x) b" |
32 qed_goal "bin_succ_Bcons0" Bin.thy "bin_succ(Bcons w False) = norm_Bcons w True" |
32 (fn _ => [(Simp_tac 1)]); |
33 (fn prem => [(Simp_tac 1)]); |
33 |
34 |
34 qed_goal "bin_succ_Bcons1" Bin.thy |
35 qed_goal "bin_pred_Bcons1" Bin.thy "bin_pred(Bcons w True) = norm_Bcons w False" |
35 "bin_succ(Bcons w True) = Bcons (bin_succ w) False" |
36 (fn prem => [(Simp_tac 1)]); |
36 (fn _ => [(Simp_tac 1)]); |
37 |
37 |
38 qed_goal "bin_pred_Bcons0" Bin.thy "bin_pred(Bcons w False) = Bcons (bin_pred w) True" |
38 qed_goal "bin_succ_Bcons0" Bin.thy |
39 (fn prem => [(Simp_tac 1)]); |
39 "bin_succ(Bcons w False) = norm_Bcons w True" |
40 |
40 (fn _ => [(Simp_tac 1)]); |
41 qed_goal "bin_minus_Bcons1" Bin.thy "bin_minus(Bcons w True) = bin_pred (Bcons(bin_minus w) False)" |
41 |
42 (fn prem => [(Simp_tac 1)]); |
42 qed_goal "bin_pred_Bcons1" Bin.thy |
43 |
43 "bin_pred(Bcons w True) = norm_Bcons w False" |
44 qed_goal "bin_minus_Bcons0" Bin.thy "bin_minus(Bcons w False) = Bcons (bin_minus w) False" |
44 (fn _ => [(Simp_tac 1)]); |
45 (fn prem => [(Simp_tac 1)]); |
45 |
|
46 qed_goal "bin_pred_Bcons0" Bin.thy |
|
47 "bin_pred(Bcons w False) = Bcons (bin_pred w) True" |
|
48 (fn _ => [(Simp_tac 1)]); |
|
49 |
|
50 qed_goal "bin_minus_Bcons1" Bin.thy |
|
51 "bin_minus(Bcons w True) = bin_pred (Bcons(bin_minus w) False)" |
|
52 (fn _ => [(Simp_tac 1)]); |
|
53 |
|
54 qed_goal "bin_minus_Bcons0" Bin.thy |
|
55 "bin_minus(Bcons w False) = Bcons (bin_minus w) False" |
|
56 (fn _ => [(Simp_tac 1)]); |
46 |
57 |
47 (*** bin_add: binary addition ***) |
58 (*** bin_add: binary addition ***) |
48 |
59 |
49 qed_goal "bin_add_Bcons_Bcons11" Bin.thy "bin_add (Bcons v True) (Bcons w True) = norm_Bcons (bin_add v (bin_succ w)) False" |
60 qed_goal "bin_add_Bcons_Bcons11" Bin.thy |
50 (fn prem => [(Simp_tac 1)]); |
61 "bin_add (Bcons v True) (Bcons w True) = \ |
51 |
62 \ norm_Bcons (bin_add v (bin_succ w)) False" |
52 qed_goal "bin_add_Bcons_Bcons10" Bin.thy "bin_add (Bcons v True) (Bcons w False) = norm_Bcons (bin_add v w) True" |
63 (fn _ => [(Simp_tac 1)]); |
53 (fn prem => [(Simp_tac 1)]); |
64 |
54 |
65 qed_goal "bin_add_Bcons_Bcons10" Bin.thy |
55 (* SHOULD THIS THEOREM BE ADDED TO HOL_SS ? *) |
66 "bin_add (Bcons v True) (Bcons w False) = norm_Bcons (bin_add v w) True" |
56 val my = prove_goal HOL.thy "(False = (~P)) = P" |
67 (fn _ => [(Simp_tac 1)]); |
57 (fn prem => [(Fast_tac 1)]); |
68 |
58 |
69 val lemma = prove_goal HOL.thy "(False = (~P)) = P" |
59 qed_goal "bin_add_Bcons_Bcons0" Bin.thy "bin_add (Bcons v False) (Bcons w y) = norm_Bcons (bin_add v w) y" |
70 (fn _ => [(Fast_tac 1)]); |
60 (fn prem => [(simp_tac (!simpset addsimps [my]) 1)]); |
71 |
61 |
72 qed_goal "bin_add_Bcons_Bcons0" Bin.thy |
62 qed_goal "bin_add_Bcons_Plus" Bin.thy "bin_add (Bcons v x) Plus = Bcons v x" |
73 "bin_add (Bcons v False) (Bcons w y) = norm_Bcons (bin_add v w) y" |
63 (fn prems => [(Simp_tac 1)]); |
74 (fn _ => [(simp_tac (!simpset addsimps [lemma]) 1)]); |
64 |
75 |
65 qed_goal "bin_add_Bcons_Minus" Bin.thy "bin_add (Bcons v x) Minus = bin_pred (Bcons v x)" |
76 qed_goal "bin_add_Bcons_Plus" Bin.thy |
66 (fn prems => [(Simp_tac 1)]); |
77 "bin_add (Bcons v x) Plus = Bcons v x" |
67 |
78 (fn _ => [(Simp_tac 1)]); |
68 qed_goal "bin_add_Bcons_Bcons" Bin.thy "bin_add (Bcons v x) (Bcons w y) = norm_Bcons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)" |
79 |
69 (fn prems => [(Simp_tac 1)]); |
80 qed_goal "bin_add_Bcons_Minus" Bin.thy |
|
81 "bin_add (Bcons v x) Minus = bin_pred (Bcons v x)" |
|
82 (fn _ => [(Simp_tac 1)]); |
|
83 |
|
84 qed_goal "bin_add_Bcons_Bcons" Bin.thy |
|
85 "bin_add (Bcons v x) (Bcons w y) = \ |
|
86 \ norm_Bcons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)" |
|
87 (fn _ => [(Simp_tac 1)]); |
70 |
88 |
71 |
89 |
72 (*** bin_add: binary multiplication ***) |
90 (*** bin_add: binary multiplication ***) |
73 |
91 |
74 qed_goal "bin_mult_Bcons1" Bin.thy "bin_mult (Bcons v True) w = bin_add (norm_Bcons (bin_mult v w) False) w" |
92 qed_goal "bin_mult_Bcons1" Bin.thy |
75 (fn prem => [(Simp_tac 1)]); |
93 "bin_mult (Bcons v True) w = bin_add (norm_Bcons (bin_mult v w) False) w" |
76 |
94 (fn _ => [(Simp_tac 1)]); |
77 qed_goal "bin_mult_Bcons0" Bin.thy "bin_mult (Bcons v False) w = norm_Bcons (bin_mult v w) False" |
95 |
78 (fn prem => [(Simp_tac 1)]); |
96 qed_goal "bin_mult_Bcons0" Bin.thy |
|
97 "bin_mult (Bcons v False) w = norm_Bcons (bin_mult v w) False" |
|
98 (fn _ => [(Simp_tac 1)]); |
79 |
99 |
80 |
100 |
81 (**** The carry/borrow functions, bin_succ and bin_pred ****) |
101 (**** The carry/borrow functions, bin_succ and bin_pred ****) |
82 |
102 |
83 (** Lemmas **) |
103 val if_ss = !simpset setloop (split_tac [expand_if]) ; |
84 |
|
85 qed_goal "zadd_assoc_cong" Integ.thy "(z::int) + v = z' + v' ==> z + (v + w) = z' + (v' + w)" |
|
86 (fn prems => [(asm_simp_tac (!simpset addsimps (prems @ [zadd_assoc RS sym])) 1)]); |
|
87 |
|
88 qed_goal "zadd_assoc_swap" Integ.thy "(z::int) + (v + w) = v + (z + w)" |
|
89 (fn prems => [(REPEAT (ares_tac [zadd_commute RS zadd_assoc_cong] 1))]); |
|
90 |
|
91 |
|
92 val my_ss = !simpset setloop (split_tac [expand_if]) ; |
|
93 |
104 |
94 |
105 |
95 (**** integ_of_bin ****) |
106 (**** integ_of_bin ****) |
96 |
107 |
97 |
108 |
98 qed_goal "integ_of_bin_norm_Bcons" Bin.thy "integ_of_bin(norm_Bcons w b) = integ_of_bin(Bcons w b)" |
109 qed_goal "integ_of_bin_norm_Bcons" Bin.thy |
99 (fn prems=>[ (bin.induct_tac "w" 1), |
110 "integ_of_bin(norm_Bcons w b) = integ_of_bin(Bcons w b)" |
100 (REPEAT(simp_tac (!simpset setloop (split_tac [expand_if])) 1)) ]); |
111 (fn _ =>[(bin.induct_tac "w" 1), |
101 |
112 (ALLGOALS(simp_tac if_ss)) ]); |
102 qed_goal "integ_of_bin_succ" Bin.thy "integ_of_bin(bin_succ w) = $#1 + integ_of_bin w" |
113 |
103 (fn prems=>[ (rtac bin.induct 1), |
114 qed_goal "integ_of_bin_succ" Bin.thy |
104 (REPEAT(asm_simp_tac (!simpset addsimps (integ_of_bin_norm_Bcons::zadd_ac) |
115 "integ_of_bin(bin_succ w) = $#1 + integ_of_bin w" |
105 setloop (split_tac [expand_if])) 1)) ]); |
116 (fn _ =>[(rtac bin.induct 1), |
106 |
117 (ALLGOALS(asm_simp_tac |
107 qed_goal "integ_of_bin_pred" Bin.thy "integ_of_bin(bin_pred w) = $~ ($#1) + integ_of_bin w" |
118 (if_ss addsimps (integ_of_bin_norm_Bcons::zadd_ac)))) ]); |
108 (fn prems=>[ (rtac bin.induct 1), |
119 |
109 (REPEAT(asm_simp_tac (!simpset addsimps (integ_of_bin_norm_Bcons::zadd_ac) |
120 qed_goal "integ_of_bin_pred" Bin.thy |
110 setloop (split_tac [expand_if])) 1)) ]); |
121 "integ_of_bin(bin_pred w) = $~ ($#1) + integ_of_bin w" |
111 |
122 (fn _ =>[(rtac bin.induct 1), |
112 qed_goal "integ_of_bin_minus" Bin.thy "integ_of_bin(bin_minus w) = $~ (integ_of_bin w)" |
123 (ALLGOALS(asm_simp_tac |
113 (fn prems=>[ (rtac bin.induct 1), |
124 (if_ss addsimps (integ_of_bin_norm_Bcons::zadd_ac)))) ]); |
114 (Simp_tac 1), |
125 |
115 (Simp_tac 1), |
126 qed_goal "integ_of_bin_minus" Bin.thy |
116 (asm_simp_tac (!simpset |
127 "integ_of_bin(bin_minus w) = $~ (integ_of_bin w)" |
117 delsimps [pred_Plus,pred_Minus,pred_Bcons] |
128 (fn _ =>[(rtac bin.induct 1), |
118 addsimps [integ_of_bin_succ,integ_of_bin_pred, |
129 (Simp_tac 1), |
119 zadd_assoc] |
130 (Simp_tac 1), |
120 setloop (split_tac [expand_if])) 1)]); |
131 (asm_simp_tac (if_ss |
|
132 delsimps [pred_Plus,pred_Minus,pred_Bcons] |
|
133 addsimps [integ_of_bin_succ,integ_of_bin_pred, |
|
134 zadd_assoc]) 1)]); |
121 |
135 |
122 |
136 |
123 val bin_add_simps = [add_Plus,add_Minus,bin_add_Bcons_Plus,bin_add_Bcons_Minus,bin_add_Bcons_Bcons, |
137 val bin_add_simps = [add_Plus,add_Minus,bin_add_Bcons_Plus, |
124 integ_of_bin_succ, integ_of_bin_pred, |
138 bin_add_Bcons_Minus,bin_add_Bcons_Bcons, |
125 integ_of_bin_norm_Bcons]; |
139 integ_of_bin_succ, integ_of_bin_pred, |
|
140 integ_of_bin_norm_Bcons]; |
126 val bin_simps = [iob_Plus,iob_Minus,iob_Bcons]; |
141 val bin_simps = [iob_Plus,iob_Minus,iob_Bcons]; |
127 |
142 |
128 goal Bin.thy "! w. integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w"; |
143 goal Bin.thy |
|
144 "! w. integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w"; |
129 by (bin.induct_tac "v" 1); |
145 by (bin.induct_tac "v" 1); |
130 by (simp_tac (my_ss addsimps bin_add_simps) 1); |
146 by (simp_tac (if_ss addsimps bin_add_simps) 1); |
131 by (simp_tac (my_ss addsimps bin_add_simps) 1); |
147 by (simp_tac (if_ss addsimps bin_add_simps) 1); |
132 by (rtac allI 1); |
148 by (rtac allI 1); |
133 by (bin.induct_tac "w" 1); |
149 by (bin.induct_tac "w" 1); |
134 by (asm_simp_tac (my_ss addsimps (bin_add_simps)) 1); |
150 by (asm_simp_tac (if_ss addsimps (bin_add_simps)) 1); |
135 by (asm_simp_tac (my_ss addsimps (bin_add_simps @ zadd_ac)) 1); |
151 by (asm_simp_tac (if_ss addsimps (bin_add_simps @ zadd_ac)) 1); |
136 by (cut_inst_tac [("P","bool")] True_or_False 1); |
152 by (cut_inst_tac [("P","bool")] True_or_False 1); |
137 by (etac disjE 1); |
153 by (etac disjE 1); |
138 by (asm_simp_tac (my_ss addsimps (bin_add_simps @ zadd_ac)) 1); |
154 by (asm_simp_tac (if_ss addsimps (bin_add_simps @ zadd_ac)) 1); |
139 by (asm_simp_tac (my_ss addsimps (bin_add_simps @ zadd_ac)) 1); |
155 by (asm_simp_tac (if_ss addsimps (bin_add_simps @ zadd_ac)) 1); |
140 val integ_of_bin_add_lemma = result(); |
156 val integ_of_bin_add_lemma = result(); |
141 |
157 |
142 goal Bin.thy "integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w"; |
158 goal Bin.thy "integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w"; |
143 by (cut_facts_tac [integ_of_bin_add_lemma] 1); |
159 by (cut_facts_tac [integ_of_bin_add_lemma] 1); |
144 by (Fast_tac 1); |
160 by (Fast_tac 1); |
145 qed "integ_of_bin_add"; |
161 qed "integ_of_bin_add"; |
146 |
162 |
147 val bin_mult_simps = [integ_of_bin_minus, integ_of_bin_add,integ_of_bin_norm_Bcons]; |
163 val bin_mult_simps = [integ_of_bin_minus, integ_of_bin_add, |
|
164 integ_of_bin_norm_Bcons]; |
148 |
165 |
149 goal Bin.thy "integ_of_bin(bin_mult v w) = integ_of_bin v * integ_of_bin w"; |
166 goal Bin.thy "integ_of_bin(bin_mult v w) = integ_of_bin v * integ_of_bin w"; |
150 by (bin.induct_tac "v" 1); |
167 by (bin.induct_tac "v" 1); |
151 by (simp_tac (my_ss addsimps bin_mult_simps) 1); |
168 by (simp_tac (if_ss addsimps bin_mult_simps) 1); |
152 by (simp_tac (my_ss addsimps bin_mult_simps) 1); |
169 by (simp_tac (if_ss addsimps bin_mult_simps) 1); |
153 by (cut_inst_tac [("P","bool")] True_or_False 1); |
170 by (cut_inst_tac [("P","bool")] True_or_False 1); |
154 by (etac disjE 1); |
171 by (etac disjE 1); |
155 by (asm_simp_tac (my_ss addsimps (bin_mult_simps @ [zadd_zmult_distrib])) 2); |
172 by (asm_simp_tac (if_ss addsimps (bin_mult_simps @ [zadd_zmult_distrib])) 2); |
156 by (asm_simp_tac (my_ss addsimps (bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac)) 1); |
173 by (asm_simp_tac (if_ss addsimps (bin_mult_simps @ [zadd_zmult_distrib] @ |
|
174 zadd_ac)) 1); |
157 qed "integ_of_bin_mult"; |
175 qed "integ_of_bin_mult"; |
158 |
176 |
159 |
177 |
160 Delsimps [succ_Bcons,pred_Bcons,min_Bcons,add_Bcons,mult_Bcons, |
178 Delsimps [succ_Bcons,pred_Bcons,min_Bcons,add_Bcons,mult_Bcons, |
161 iob_Plus,iob_Minus,iob_Bcons, |
179 iob_Plus,iob_Minus,iob_Bcons, |
162 norm_Plus,norm_Minus,norm_Bcons]; |
180 norm_Plus,norm_Minus,norm_Bcons]; |
163 |
181 |
164 Addsimps [integ_of_bin_add RS sym, |
182 Addsimps [integ_of_bin_add RS sym, |
165 integ_of_bin_minus RS sym, |
183 integ_of_bin_minus RS sym, |
166 integ_of_bin_mult RS sym, |
184 integ_of_bin_mult RS sym, |
167 bin_succ_Bcons1,bin_succ_Bcons0, |
185 bin_succ_Bcons1,bin_succ_Bcons0, |
168 bin_pred_Bcons1,bin_pred_Bcons0, |
186 bin_pred_Bcons1,bin_pred_Bcons0, |
169 bin_minus_Bcons1,bin_minus_Bcons0, |
187 bin_minus_Bcons1,bin_minus_Bcons0, |
170 bin_add_Bcons_Plus,bin_add_Bcons_Minus, |
188 bin_add_Bcons_Plus,bin_add_Bcons_Minus, |
171 bin_add_Bcons_Bcons0,bin_add_Bcons_Bcons10,bin_add_Bcons_Bcons11, |
189 bin_add_Bcons_Bcons0,bin_add_Bcons_Bcons10,bin_add_Bcons_Bcons11, |
172 bin_mult_Bcons1,bin_mult_Bcons0, |
190 bin_mult_Bcons1,bin_mult_Bcons0, |
173 norm_Bcons_Plus_0,norm_Bcons_Plus_1, |
191 norm_Bcons_Plus_0,norm_Bcons_Plus_1, |
174 norm_Bcons_Minus_0,norm_Bcons_Minus_1, |
192 norm_Bcons_Minus_0,norm_Bcons_Minus_1, |
175 norm_Bcons_Bcons]; |
193 norm_Bcons_Bcons]; |
|
194 |
|
195 |
|
196 (** Simplification rules for comparison of binary numbers (Norbert Völker) **) |
|
197 |
|
198 Addsimps [zadd_assoc]; |
|
199 |
|
200 goal Bin.thy |
|
201 "(integ_of_bin x = integ_of_bin y) \ |
|
202 \ = (integ_of_bin (bin_add x (bin_minus y)) = $# 0)"; |
|
203 by (simp_tac (HOL_ss addsimps |
|
204 [integ_of_bin_add, integ_of_bin_minus,zdiff_def]) 1); |
|
205 by (rtac iffI 1); |
|
206 by (etac ssubst 1); |
|
207 by (rtac zadd_zminus_inverse 1); |
|
208 by (dres_inst_tac [("f","(% z. z + integ_of_bin y)")] arg_cong 1); |
|
209 by (asm_full_simp_tac |
|
210 (HOL_ss addsimps[zadd_assoc,zadd_0,zadd_0_right, |
|
211 zadd_zminus_inverse2]) 1); |
|
212 val iob_eq_eq_diff_0 = result(); |
|
213 |
|
214 goal Bin.thy "(integ_of_bin Plus = $# 0) = True"; |
|
215 by (stac iob_Plus 1); by (Simp_tac 1); |
|
216 val iob_Plus_eq_0 = result(); |
|
217 |
|
218 goal Bin.thy "(integ_of_bin Minus = $# 0) = False"; |
|
219 by (stac iob_Minus 1); |
|
220 by (Simp_tac 1); |
|
221 val iob_Minus_not_eq_0 = result(); |
|
222 |
|
223 goal Bin.thy |
|
224 "(integ_of_bin (Bcons w x) = $# 0) = (~x & integ_of_bin w = $# 0)"; |
|
225 by (stac iob_Bcons 1); |
|
226 by (case_tac "x" 1); |
|
227 by (ALLGOALS Asm_simp_tac); |
|
228 by (ALLGOALS(asm_simp_tac (HOL_ss addsimps [integ_of_bin_add]))); |
|
229 by (ALLGOALS(int_case_tac "integ_of_bin w")); |
|
230 by (ALLGOALS(asm_simp_tac |
|
231 (!simpset addsimps[zminus_zadd_distrib RS sym, |
|
232 znat_add RS sym]))); |
|
233 by (stac eq_False_conv 1); |
|
234 by (rtac notI 1); |
|
235 by (dres_inst_tac [("f","(% z. z + $# Suc (Suc (n + n)))")] arg_cong 1); |
|
236 by (Asm_full_simp_tac 1); |
|
237 val iob_Bcons_eq_0 = result(); |
|
238 |
|
239 goalw Bin.thy [zless_def,zdiff_def] |
|
240 "integ_of_bin x < integ_of_bin y \ |
|
241 \ = (integ_of_bin (bin_add x (bin_minus y)) < $# 0)"; |
|
242 by (Simp_tac 1); |
|
243 val iob_less_eq_diff_lt_0 = result(); |
|
244 |
|
245 goal Bin.thy "(integ_of_bin Plus < $# 0) = False"; |
|
246 by (stac iob_Plus 1); by (Simp_tac 1); |
|
247 val iob_Plus_not_lt_0 = result(); |
|
248 |
|
249 goal Bin.thy "(integ_of_bin Minus < $# 0) = True"; |
|
250 by (stac iob_Minus 1); by (Simp_tac 1); |
|
251 val iob_Minus_lt_0 = result(); |
|
252 |
|
253 goal Bin.thy |
|
254 "(integ_of_bin (Bcons w x) < $# 0) = (integ_of_bin w < $# 0)"; |
|
255 by (stac iob_Bcons 1); |
|
256 by (case_tac "x" 1); |
|
257 by (ALLGOALS Asm_simp_tac); |
|
258 by (ALLGOALS(asm_simp_tac (HOL_ss addsimps [integ_of_bin_add]))); |
|
259 by (ALLGOALS(int_case_tac "integ_of_bin w")); |
|
260 by (ALLGOALS(asm_simp_tac |
|
261 (!simpset addsimps[zminus_zadd_distrib RS sym, |
|
262 znat_add RS sym]))); |
|
263 by (stac (zadd_zminus_inverse RS sym) 1); |
|
264 by (rtac zadd_zless_mono1 1); |
|
265 by (Simp_tac 1); |
|
266 val iob_Bcons_lt_0 = result(); |
|
267 |
|
268 goal Bin.thy |
|
269 "integ_of_bin x <= integ_of_bin y \ |
|
270 \ = ( integ_of_bin (bin_add x (bin_minus y)) < $# 0 \ |
|
271 \ | integ_of_bin (bin_add x (bin_minus y)) = $# 0)"; |
|
272 by (simp_tac (HOL_ss addsimps |
|
273 [zle_eq_zless_or_eq,iob_less_eq_diff_lt_0,zdiff_def |
|
274 ,iob_eq_eq_diff_0,integ_of_bin_minus,integ_of_bin_add]) 1); |
|
275 val iob_le_diff_lt_0_or_eq_0 = result(); |
|
276 |
|
277 Delsimps [zless_eq_less, zle_eq_le, zadd_assoc, znegative_zminus_znat, |
|
278 not_znegative_znat, zero_zless_Suc_pos, negative_zless_0, |
|
279 negative_zle_0, not_zle_0_negative, not_znat_zless_negative, |
|
280 zminus_zless_zminus, zminus_zle_zminus, negative_eq_positive]; |
|
281 |
|
282 Addsimps [zdiff_def, iob_eq_eq_diff_0, iob_less_eq_diff_lt_0, |
|
283 iob_le_diff_lt_0_or_eq_0, iob_Plus_eq_0, iob_Minus_not_eq_0, |
|
284 iob_Bcons_eq_0, iob_Plus_not_lt_0, iob_Minus_lt_0, iob_Bcons_lt_0]; |
|
285 |
176 |
286 |
177 (*** Examples of performing binary arithmetic by simplification ***) |
287 (*** Examples of performing binary arithmetic by simplification ***) |
178 |
288 |
179 goal Bin.thy "#13 + #19 = #32"; |
289 goal Bin.thy "#13 + #19 = #32"; |
180 by (Simp_tac 1); |
290 by (Simp_tac 1); |