1 (* |
1 (* Title: HOL/Word/Bit_Representation.thy |
2 Author: Jeremy Dawson, NICTA |
2 Author: Jeremy Dawson, NICTA |
3 *) |
3 *) |
4 |
4 |
5 section \<open>Integers as implict bit strings\<close> |
5 section \<open>Integers as implict bit strings\<close> |
6 |
6 |
7 theory Bit_Representation |
7 theory Bit_Representation |
8 imports Misc_Numeric |
8 imports Misc_Numeric |
9 begin |
9 begin |
10 |
10 |
11 subsection \<open>Constructors and destructors for binary integers\<close> |
11 subsection \<open>Constructors and destructors for binary integers\<close> |
12 |
12 |
13 definition Bit :: "int \<Rightarrow> bool \<Rightarrow> int" (infixl "BIT" 90) |
13 definition Bit :: "int \<Rightarrow> bool \<Rightarrow> int" (infixl "BIT" 90) |
14 where |
14 where "k BIT b = (if b then 1 else 0) + k + k" |
15 "k BIT b = (if b then 1 else 0) + k + k" |
15 |
16 |
16 lemma Bit_B0: "k BIT False = k + k" |
17 lemma Bit_B0: |
17 by (simp add: Bit_def) |
18 "k BIT False = k + k" |
18 |
19 by (unfold Bit_def) simp |
19 lemma Bit_B1: "k BIT True = k + k + 1" |
20 |
20 by (simp add: Bit_def) |
21 lemma Bit_B1: |
21 |
22 "k BIT True = k + k + 1" |
|
23 by (unfold Bit_def) simp |
|
24 |
|
25 lemma Bit_B0_2t: "k BIT False = 2 * k" |
22 lemma Bit_B0_2t: "k BIT False = 2 * k" |
26 by (rule trans, rule Bit_B0) simp |
23 by (rule trans, rule Bit_B0) simp |
27 |
24 |
28 lemma Bit_B1_2t: "k BIT True = 2 * k + 1" |
25 lemma Bit_B1_2t: "k BIT True = 2 * k + 1" |
29 by (rule trans, rule Bit_B1) simp |
26 by (rule trans, rule Bit_B1) simp |
30 |
27 |
31 definition bin_last :: "int \<Rightarrow> bool" |
28 definition bin_last :: "int \<Rightarrow> bool" |
32 where |
29 where "bin_last w \<longleftrightarrow> w mod 2 = 1" |
33 "bin_last w \<longleftrightarrow> w mod 2 = 1" |
30 |
34 |
31 lemma bin_last_odd: "bin_last = odd" |
35 lemma bin_last_odd: |
|
36 "bin_last = odd" |
|
37 by (rule ext) (simp add: bin_last_def even_iff_mod_2_eq_zero) |
32 by (rule ext) (simp add: bin_last_def even_iff_mod_2_eq_zero) |
38 |
33 |
39 definition bin_rest :: "int \<Rightarrow> int" |
34 definition bin_rest :: "int \<Rightarrow> int" |
40 where |
35 where "bin_rest w = w div 2" |
41 "bin_rest w = w div 2" |
36 |
42 |
37 lemma bin_rl_simp [simp]: "bin_rest w BIT bin_last w = w" |
43 lemma bin_rl_simp [simp]: |
|
44 "bin_rest w BIT bin_last w = w" |
|
45 unfolding bin_rest_def bin_last_def Bit_def |
38 unfolding bin_rest_def bin_last_def Bit_def |
46 using div_mult_mod_eq [of w 2] |
39 by (cases "w mod 2 = 0") (use div_mult_mod_eq [of w 2] in simp_all) |
47 by (cases "w mod 2 = 0", simp_all) |
|
48 |
40 |
49 lemma bin_rest_BIT [simp]: "bin_rest (x BIT b) = x" |
41 lemma bin_rest_BIT [simp]: "bin_rest (x BIT b) = x" |
50 unfolding bin_rest_def Bit_def |
42 unfolding bin_rest_def Bit_def |
51 by (cases b, simp_all) |
43 by (cases b) simp_all |
52 |
44 |
53 lemma bin_last_BIT [simp]: "bin_last (x BIT b) = b" |
45 lemma bin_last_BIT [simp]: "bin_last (x BIT b) = b" |
54 unfolding bin_last_def Bit_def |
46 unfolding bin_last_def Bit_def |
55 by (cases b) simp_all |
47 by (cases b) simp_all |
56 |
48 |
57 lemma BIT_eq_iff [iff]: "u BIT b = v BIT c \<longleftrightarrow> u = v \<and> b = c" |
49 lemma BIT_eq_iff [iff]: "u BIT b = v BIT c \<longleftrightarrow> u = v \<and> b = c" |
58 apply (auto simp add: Bit_def) |
50 by (auto simp: Bit_def) arith+ |
59 apply arith |
|
60 apply arith |
|
61 done |
|
62 |
51 |
63 lemma BIT_bin_simps [simp]: |
52 lemma BIT_bin_simps [simp]: |
64 "numeral k BIT False = numeral (Num.Bit0 k)" |
53 "numeral k BIT False = numeral (Num.Bit0 k)" |
65 "numeral k BIT True = numeral (Num.Bit1 k)" |
54 "numeral k BIT True = numeral (Num.Bit1 k)" |
66 "(- numeral k) BIT False = - numeral (Num.Bit0 k)" |
55 "(- numeral k) BIT False = - numeral (Num.Bit0 k)" |
67 "(- numeral k) BIT True = - numeral (Num.BitM k)" |
56 "(- numeral k) BIT True = - numeral (Num.BitM k)" |
68 unfolding numeral.simps numeral_BitM |
57 unfolding numeral.simps numeral_BitM |
69 unfolding Bit_def |
58 by (simp_all add: Bit_def del: arith_simps add_numeral_special diff_numeral_special) |
70 by (simp_all del: arith_simps add_numeral_special diff_numeral_special) |
|
71 |
59 |
72 lemma BIT_special_simps [simp]: |
60 lemma BIT_special_simps [simp]: |
73 shows "0 BIT False = 0" and "0 BIT True = 1" |
61 shows "0 BIT False = 0" |
74 and "1 BIT False = 2" and "1 BIT True = 3" |
62 and "0 BIT True = 1" |
75 and "(- 1) BIT False = - 2" and "(- 1) BIT True = - 1" |
63 and "1 BIT False = 2" |
76 unfolding Bit_def by simp_all |
64 and "1 BIT True = 3" |
|
65 and "(- 1) BIT False = - 2" |
|
66 and "(- 1) BIT True = - 1" |
|
67 by (simp_all add: Bit_def) |
77 |
68 |
78 lemma Bit_eq_0_iff: "w BIT b = 0 \<longleftrightarrow> w = 0 \<and> \<not> b" |
69 lemma Bit_eq_0_iff: "w BIT b = 0 \<longleftrightarrow> w = 0 \<and> \<not> b" |
79 apply (auto simp add: Bit_def) |
70 by (auto simp: Bit_def) arith |
80 apply arith |
|
81 done |
|
82 |
71 |
83 lemma Bit_eq_m1_iff: "w BIT b = -1 \<longleftrightarrow> w = -1 \<and> b" |
72 lemma Bit_eq_m1_iff: "w BIT b = -1 \<longleftrightarrow> w = -1 \<and> b" |
84 apply (auto simp add: Bit_def) |
73 by (auto simp: Bit_def) arith |
85 apply arith |
|
86 done |
|
87 |
74 |
88 lemma BitM_inc: "Num.BitM (Num.inc w) = Num.Bit1 w" |
75 lemma BitM_inc: "Num.BitM (Num.inc w) = Num.Bit1 w" |
89 by (induct w, simp_all) |
76 by (induct w) simp_all |
90 |
77 |
91 lemma expand_BIT: |
78 lemma expand_BIT: |
92 "numeral (Num.Bit0 w) = numeral w BIT False" |
79 "numeral (Num.Bit0 w) = numeral w BIT False" |
93 "numeral (Num.Bit1 w) = numeral w BIT True" |
80 "numeral (Num.Bit1 w) = numeral w BIT True" |
94 "- numeral (Num.Bit0 w) = (- numeral w) BIT False" |
81 "- numeral (Num.Bit0 w) = (- numeral w) BIT False" |
95 "- numeral (Num.Bit1 w) = (- numeral (w + Num.One)) BIT True" |
82 "- numeral (Num.Bit1 w) = (- numeral (w + Num.One)) BIT True" |
96 unfolding add_One by (simp_all add: BitM_inc) |
83 by (simp_all add: add_One BitM_inc) |
97 |
84 |
98 lemma bin_last_numeral_simps [simp]: |
85 lemma bin_last_numeral_simps [simp]: |
99 "\<not> bin_last 0" |
86 "\<not> bin_last 0" |
100 "bin_last 1" |
87 "bin_last 1" |
101 "bin_last (- 1)" |
88 "bin_last (- 1)" |
146 "x BIT False * y = (x * y) BIT False" |
131 "x BIT False * y = (x * y) BIT False" |
147 "x * y BIT False = (x * y) BIT False" |
132 "x * y BIT False = (x * y) BIT False" |
148 "x BIT True * y = (x * y) BIT False + y" |
133 "x BIT True * y = (x * y) BIT False + y" |
149 by (simp_all add: Bit_B0_2t Bit_B1_2t algebra_simps) |
134 by (simp_all add: Bit_B0_2t Bit_B1_2t algebra_simps) |
150 |
135 |
151 lemma B_mod_2': |
136 lemma B_mod_2': "X = 2 \<Longrightarrow> (w BIT True) mod X = 1 \<and> (w BIT False) mod X = 0" |
152 "X = 2 ==> (w BIT True) mod X = 1 & (w BIT False) mod X = 0" |
137 by (simp add: Bit_B0 Bit_B1) |
153 apply (simp (no_asm) only: Bit_B0 Bit_B1) |
138 |
154 apply simp |
139 lemma bin_ex_rl: "\<exists>w b. w BIT b = bin" |
155 done |
|
156 |
|
157 lemma bin_ex_rl: "EX w b. w BIT b = bin" |
|
158 by (metis bin_rl_simp) |
140 by (metis bin_rl_simp) |
159 |
141 |
160 lemma bin_exhaust: |
142 lemma bin_exhaust: |
161 assumes Q: "\<And>x b. bin = x BIT b \<Longrightarrow> Q" |
143 assumes that: "\<And>x b. bin = x BIT b \<Longrightarrow> Q" |
162 shows "Q" |
144 shows "Q" |
163 apply (insert bin_ex_rl [of bin]) |
145 apply (insert bin_ex_rl [of bin]) |
164 apply (erule exE)+ |
146 apply (erule exE)+ |
165 apply (rule Q) |
147 apply (rule that) |
166 apply force |
148 apply force |
167 done |
149 done |
168 |
150 |
169 primrec bin_nth where |
151 primrec bin_nth |
170 Z: "bin_nth w 0 \<longleftrightarrow> bin_last w" |
152 where |
|
153 Z: "bin_nth w 0 \<longleftrightarrow> bin_last w" |
171 | Suc: "bin_nth w (Suc n) \<longleftrightarrow> bin_nth (bin_rest w) n" |
154 | Suc: "bin_nth w (Suc n) \<longleftrightarrow> bin_nth (bin_rest w) n" |
172 |
155 |
173 lemma bin_abs_lem: |
156 lemma bin_abs_lem: "bin = (w BIT b) \<Longrightarrow> bin \<noteq> -1 \<longrightarrow> bin \<noteq> 0 \<longrightarrow> nat \<bar>w\<bar> < nat \<bar>bin\<bar>" |
174 "bin = (w BIT b) ==> bin ~= -1 --> bin ~= 0 --> |
|
175 nat \<bar>w\<bar> < nat \<bar>bin\<bar>" |
|
176 apply clarsimp |
157 apply clarsimp |
177 apply (unfold Bit_def) |
158 apply (unfold Bit_def) |
178 apply (cases b) |
159 apply (cases b) |
179 apply (clarsimp, arith) |
160 apply (clarsimp, arith) |
180 apply (clarsimp, arith) |
161 apply (clarsimp, arith) |
181 done |
162 done |
182 |
163 |
183 lemma bin_induct: |
164 lemma bin_induct: |
184 assumes PPls: "P 0" |
165 assumes PPls: "P 0" |
185 and PMin: "P (- 1)" |
166 and PMin: "P (- 1)" |
186 and PBit: "!!bin bit. P bin ==> P (bin BIT bit)" |
167 and PBit: "\<And>bin bit. P bin \<Longrightarrow> P (bin BIT bit)" |
187 shows "P bin" |
168 shows "P bin" |
188 apply (rule_tac P=P and a=bin and f1="nat o abs" |
169 apply (rule_tac P=P and a=bin and f1="nat \<circ> abs" in wf_measure [THEN wf_induct]) |
189 in wf_measure [THEN wf_induct]) |
|
190 apply (simp add: measure_def inv_image_def) |
170 apply (simp add: measure_def inv_image_def) |
191 apply (case_tac x rule: bin_exhaust) |
171 apply (case_tac x rule: bin_exhaust) |
192 apply (frule bin_abs_lem) |
172 apply (frule bin_abs_lem) |
193 apply (auto simp add : PPls PMin PBit) |
173 apply (auto simp add : PPls PMin PBit) |
194 done |
174 done |
195 |
175 |
196 lemma Bit_div2 [simp]: "(w BIT b) div 2 = w" |
176 lemma Bit_div2 [simp]: "(w BIT b) div 2 = w" |
197 unfolding bin_rest_def [symmetric] by (rule bin_rest_BIT) |
177 unfolding bin_rest_def [symmetric] by (rule bin_rest_BIT) |
198 |
178 |
199 lemma bin_nth_eq_iff: |
179 lemma bin_nth_eq_iff: "bin_nth x = bin_nth y \<longleftrightarrow> x = y" |
200 "bin_nth x = bin_nth y \<longleftrightarrow> x = y" |
|
201 proof - |
180 proof - |
202 have bin_nth_lem [rule_format]: "ALL y. bin_nth x = bin_nth y --> x = y" |
181 have bin_nth_lem [rule_format]: "\<forall>y. bin_nth x = bin_nth y \<longrightarrow> x = y" |
203 apply (induct x rule: bin_induct) |
182 apply (induct x rule: bin_induct) |
204 apply safe |
183 apply safe |
205 apply (erule rev_mp) |
184 apply (erule rev_mp) |
206 apply (induct_tac y rule: bin_induct) |
185 apply (induct_tac y rule: bin_induct) |
207 apply safe |
186 apply safe |
208 apply (drule_tac x=0 in fun_cong, force) |
187 apply (drule_tac x=0 in fun_cong, force) |
209 apply (erule notE, rule ext, |
188 apply (erule notE, rule ext, drule_tac x="Suc x" in fun_cong, force) |
210 drule_tac x="Suc x" in fun_cong, force) |
|
211 apply (drule_tac x=0 in fun_cong, force) |
189 apply (drule_tac x=0 in fun_cong, force) |
212 apply (erule rev_mp) |
190 apply (erule rev_mp) |
213 apply (induct_tac y rule: bin_induct) |
191 apply (induct_tac y rule: bin_induct) |
214 apply safe |
192 apply safe |
215 apply (drule_tac x=0 in fun_cong, force) |
193 apply (drule_tac x=0 in fun_cong, force) |
216 apply (erule notE, rule ext, |
194 apply (erule notE, rule ext, drule_tac x="Suc x" in fun_cong, force) |
217 drule_tac x="Suc x" in fun_cong, force) |
195 apply (metis Bit_eq_m1_iff Z bin_last_BIT) |
218 apply (metis Bit_eq_m1_iff Z bin_last_BIT) |
|
219 apply (case_tac y rule: bin_exhaust) |
196 apply (case_tac y rule: bin_exhaust) |
220 apply clarify |
197 apply clarify |
221 apply (erule allE) |
198 apply (erule allE) |
222 apply (erule impE) |
199 apply (erule impE) |
223 prefer 2 |
200 prefer 2 |
249 by auto |
225 by auto |
250 |
226 |
251 lemma bin_nth_Suc_BIT: "bin_nth (w BIT b) (Suc n) = bin_nth w n" |
227 lemma bin_nth_Suc_BIT: "bin_nth (w BIT b) (Suc n) = bin_nth w n" |
252 by auto |
228 by auto |
253 |
229 |
254 lemma bin_nth_minus [simp]: "0 < n ==> bin_nth (w BIT b) n = bin_nth w (n - 1)" |
230 lemma bin_nth_minus [simp]: "0 < n \<Longrightarrow> bin_nth (w BIT b) n = bin_nth w (n - 1)" |
255 by (cases n) auto |
231 by (cases n) auto |
256 |
232 |
257 lemma bin_nth_numeral: |
233 lemma bin_nth_numeral: "bin_rest x = y \<Longrightarrow> bin_nth x (numeral n) = bin_nth y (pred_numeral n)" |
258 "bin_rest x = y \<Longrightarrow> bin_nth x (numeral n) = bin_nth y (pred_numeral n)" |
|
259 by (simp add: numeral_eq_Suc) |
234 by (simp add: numeral_eq_Suc) |
260 |
235 |
261 lemmas bin_nth_numeral_simps [simp] = |
236 lemmas bin_nth_numeral_simps [simp] = |
262 bin_nth_numeral [OF bin_rest_numeral_simps(2)] |
237 bin_nth_numeral [OF bin_rest_numeral_simps(2)] |
263 bin_nth_numeral [OF bin_rest_numeral_simps(5)] |
238 bin_nth_numeral [OF bin_rest_numeral_simps(5)] |
264 bin_nth_numeral [OF bin_rest_numeral_simps(6)] |
239 bin_nth_numeral [OF bin_rest_numeral_simps(6)] |
265 bin_nth_numeral [OF bin_rest_numeral_simps(7)] |
240 bin_nth_numeral [OF bin_rest_numeral_simps(7)] |
266 bin_nth_numeral [OF bin_rest_numeral_simps(8)] |
241 bin_nth_numeral [OF bin_rest_numeral_simps(8)] |
267 |
242 |
268 lemmas bin_nth_simps = |
243 lemmas bin_nth_simps = |
269 bin_nth.Z bin_nth.Suc bin_nth_zero bin_nth_minus1 |
244 bin_nth.Z bin_nth.Suc bin_nth_zero bin_nth_minus1 |
270 bin_nth_numeral_simps |
245 bin_nth_numeral_simps |
271 |
246 |
272 |
247 |
273 subsection \<open>Truncating binary integers\<close> |
248 subsection \<open>Truncating binary integers\<close> |
274 |
249 |
275 definition bin_sign :: "int \<Rightarrow> int" |
250 definition bin_sign :: "int \<Rightarrow> int" |
276 where |
251 where "bin_sign k = (if k \<ge> 0 then 0 else - 1)" |
277 bin_sign_def: "bin_sign k = (if k \<ge> 0 then 0 else - 1)" |
|
278 |
252 |
279 lemma bin_sign_simps [simp]: |
253 lemma bin_sign_simps [simp]: |
280 "bin_sign 0 = 0" |
254 "bin_sign 0 = 0" |
281 "bin_sign 1 = 0" |
255 "bin_sign 1 = 0" |
282 "bin_sign (- 1) = - 1" |
256 "bin_sign (- 1) = - 1" |
283 "bin_sign (numeral k) = 0" |
257 "bin_sign (numeral k) = 0" |
284 "bin_sign (- numeral k) = -1" |
258 "bin_sign (- numeral k) = -1" |
285 "bin_sign (w BIT b) = bin_sign w" |
259 "bin_sign (w BIT b) = bin_sign w" |
286 unfolding bin_sign_def Bit_def |
260 by (simp_all add: bin_sign_def Bit_def) |
287 by simp_all |
261 |
288 |
262 lemma bin_sign_rest [simp]: "bin_sign (bin_rest w) = bin_sign w" |
289 lemma bin_sign_rest [simp]: |
|
290 "bin_sign (bin_rest w) = bin_sign w" |
|
291 by (cases w rule: bin_exhaust) auto |
263 by (cases w rule: bin_exhaust) auto |
292 |
264 |
293 primrec bintrunc :: "nat \<Rightarrow> int \<Rightarrow> int" where |
265 primrec bintrunc :: "nat \<Rightarrow> int \<Rightarrow> int" |
294 Z : "bintrunc 0 bin = 0" |
266 where |
295 | Suc : "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT (bin_last bin)" |
267 Z : "bintrunc 0 bin = 0" |
296 |
268 | Suc : "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT (bin_last bin)" |
297 primrec sbintrunc :: "nat => int => int" where |
269 |
298 Z : "sbintrunc 0 bin = (if bin_last bin then -1 else 0)" |
270 primrec sbintrunc :: "nat \<Rightarrow> int \<Rightarrow> int" |
299 | Suc : "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)" |
271 where |
|
272 Z : "sbintrunc 0 bin = (if bin_last bin then -1 else 0)" |
|
273 | Suc : "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)" |
300 |
274 |
301 lemma sign_bintr: "bin_sign (bintrunc n w) = 0" |
275 lemma sign_bintr: "bin_sign (bintrunc n w) = 0" |
302 by (induct n arbitrary: w) auto |
276 by (induct n arbitrary: w) auto |
303 |
277 |
304 lemma bintrunc_mod2p: "bintrunc n w = (w mod 2 ^ n)" |
278 lemma bintrunc_mod2p: "bintrunc n w = w mod 2 ^ n" |
305 apply (induct n arbitrary: w, clarsimp) |
279 by (induct n arbitrary: w) (auto simp add: bin_last_def bin_rest_def Bit_def zmod_zmult2_eq) |
306 apply (simp add: bin_last_def bin_rest_def Bit_def zmod_zmult2_eq) |
|
307 done |
|
308 |
280 |
309 lemma sbintrunc_mod2p: "sbintrunc n w = (w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n" |
281 lemma sbintrunc_mod2p: "sbintrunc n w = (w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n" |
310 apply (induct n arbitrary: w) |
282 apply (induct n arbitrary: w) |
311 apply (auto simp add: bin_last_odd bin_rest_def Bit_def elim!: evenE oddE) |
283 apply (auto simp add: bin_last_odd bin_rest_def Bit_def elim!: evenE oddE) |
312 apply (smt pos_zmod_mult_2 zle2p) |
284 apply (smt pos_zmod_mult_2 zle2p) |
344 "sbintrunc 0 (- numeral (Num.Bit1 w)) = -1" |
314 "sbintrunc 0 (- numeral (Num.Bit1 w)) = -1" |
345 by simp_all |
315 by simp_all |
346 |
316 |
347 lemma sbintrunc_Suc_numeral: |
317 lemma sbintrunc_Suc_numeral: |
348 "sbintrunc (Suc n) 1 = 1" |
318 "sbintrunc (Suc n) 1 = 1" |
349 "sbintrunc (Suc n) (numeral (Num.Bit0 w)) = |
319 "sbintrunc (Suc n) (numeral (Num.Bit0 w)) = sbintrunc n (numeral w) BIT False" |
350 sbintrunc n (numeral w) BIT False" |
320 "sbintrunc (Suc n) (numeral (Num.Bit1 w)) = sbintrunc n (numeral w) BIT True" |
351 "sbintrunc (Suc n) (numeral (Num.Bit1 w)) = |
321 "sbintrunc (Suc n) (- numeral (Num.Bit0 w)) = sbintrunc n (- numeral w) BIT False" |
352 sbintrunc n (numeral w) BIT True" |
322 "sbintrunc (Suc n) (- numeral (Num.Bit1 w)) = sbintrunc n (- numeral (w + Num.One)) BIT True" |
353 "sbintrunc (Suc n) (- numeral (Num.Bit0 w)) = |
|
354 sbintrunc n (- numeral w) BIT False" |
|
355 "sbintrunc (Suc n) (- numeral (Num.Bit1 w)) = |
|
356 sbintrunc n (- numeral (w + Num.One)) BIT True" |
|
357 by simp_all |
323 by simp_all |
358 |
324 |
359 lemma bin_sign_lem: "(bin_sign (sbintrunc n bin) = -1) = bin_nth bin n" |
325 lemma bin_sign_lem: "(bin_sign (sbintrunc n bin) = -1) = bin_nth bin n" |
360 apply (induct n arbitrary: bin) |
326 apply (induct n arbitrary: bin) |
361 apply (case_tac bin rule: bin_exhaust, case_tac b, auto) |
327 apply (case_tac bin rule: bin_exhaust, case_tac b, auto) |
362 done |
328 done |
363 |
329 |
364 lemma nth_bintr: "bin_nth (bintrunc m w) n = (n < m & bin_nth w n)" |
330 lemma nth_bintr: "bin_nth (bintrunc m w) n \<longleftrightarrow> n < m \<and> bin_nth w n" |
365 apply (induct n arbitrary: w m) |
331 apply (induct n arbitrary: w m) |
366 apply (case_tac m, auto)[1] |
332 apply (case_tac m, auto)[1] |
367 apply (case_tac m, auto)[1] |
333 apply (case_tac m, auto)[1] |
368 done |
334 done |
369 |
335 |
370 lemma nth_sbintr: |
336 lemma nth_sbintr: "bin_nth (sbintrunc m w) n = (if n < m then bin_nth w n else bin_nth w m)" |
371 "bin_nth (sbintrunc m w) n = |
|
372 (if n < m then bin_nth w n else bin_nth w m)" |
|
373 apply (induct n arbitrary: w m) |
337 apply (induct n arbitrary: w m) |
|
338 apply (case_tac m) |
|
339 apply simp_all |
374 apply (case_tac m) |
340 apply (case_tac m) |
375 apply simp_all |
341 apply simp_all |
376 apply (case_tac m) |
342 done |
377 apply simp_all |
343 |
378 done |
344 lemma bin_nth_Bit: "bin_nth (w BIT b) n \<longleftrightarrow> n = 0 \<and> b \<or> (\<exists>m. n = Suc m \<and> bin_nth w m)" |
379 |
|
380 lemma bin_nth_Bit: |
|
381 "bin_nth (w BIT b) n = (n = 0 & b | (EX m. n = Suc m & bin_nth w m))" |
|
382 by (cases n) auto |
345 by (cases n) auto |
383 |
346 |
384 lemma bin_nth_Bit0: |
347 lemma bin_nth_Bit0: |
385 "bin_nth (numeral (Num.Bit0 w)) n \<longleftrightarrow> |
348 "bin_nth (numeral (Num.Bit0 w)) n \<longleftrightarrow> |
386 (\<exists>m. n = Suc m \<and> bin_nth (numeral w) m)" |
349 (\<exists>m. n = Suc m \<and> bin_nth (numeral w) m)" |
389 lemma bin_nth_Bit1: |
352 lemma bin_nth_Bit1: |
390 "bin_nth (numeral (Num.Bit1 w)) n \<longleftrightarrow> |
353 "bin_nth (numeral (Num.Bit1 w)) n \<longleftrightarrow> |
391 n = 0 \<or> (\<exists>m. n = Suc m \<and> bin_nth (numeral w) m)" |
354 n = 0 \<or> (\<exists>m. n = Suc m \<and> bin_nth (numeral w) m)" |
392 using bin_nth_Bit [where w="numeral w" and b="True"] by simp |
355 using bin_nth_Bit [where w="numeral w" and b="True"] by simp |
393 |
356 |
394 lemma bintrunc_bintrunc_l: |
357 lemma bintrunc_bintrunc_l: "n \<le> m \<Longrightarrow> bintrunc m (bintrunc n w) = bintrunc n w" |
395 "n <= m ==> (bintrunc m (bintrunc n w) = bintrunc n w)" |
358 by (rule bin_eqI) (auto simp: nth_bintr) |
396 by (rule bin_eqI) (auto simp add : nth_bintr) |
359 |
397 |
360 lemma sbintrunc_sbintrunc_l: "n \<le> m \<Longrightarrow> sbintrunc m (sbintrunc n w) = sbintrunc n w" |
398 lemma sbintrunc_sbintrunc_l: |
|
399 "n <= m ==> (sbintrunc m (sbintrunc n w) = sbintrunc n w)" |
|
400 by (rule bin_eqI) (auto simp: nth_sbintr) |
361 by (rule bin_eqI) (auto simp: nth_sbintr) |
401 |
362 |
402 lemma bintrunc_bintrunc_ge: |
363 lemma bintrunc_bintrunc_ge: "n \<le> m \<Longrightarrow> bintrunc n (bintrunc m w) = bintrunc n w" |
403 "n <= m ==> (bintrunc n (bintrunc m w) = bintrunc n w)" |
|
404 by (rule bin_eqI) (auto simp: nth_bintr) |
364 by (rule bin_eqI) (auto simp: nth_bintr) |
405 |
365 |
406 lemma bintrunc_bintrunc_min [simp]: |
366 lemma bintrunc_bintrunc_min [simp]: "bintrunc m (bintrunc n w) = bintrunc (min m n) w" |
407 "bintrunc m (bintrunc n w) = bintrunc (min m n) w" |
367 by (rule bin_eqI) (auto simp: nth_bintr) |
408 apply (rule bin_eqI) |
368 |
409 apply (auto simp: nth_bintr) |
369 lemma sbintrunc_sbintrunc_min [simp]: "sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w" |
410 done |
370 by (rule bin_eqI) (auto simp: nth_sbintr min.absorb1 min.absorb2) |
411 |
371 |
412 lemma sbintrunc_sbintrunc_min [simp]: |
372 lemmas bintrunc_Pls = |
413 "sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w" |
|
414 apply (rule bin_eqI) |
|
415 apply (auto simp: nth_sbintr min.absorb1 min.absorb2) |
|
416 done |
|
417 |
|
418 lemmas bintrunc_Pls = |
|
419 bintrunc.Suc [where bin="0", simplified bin_last_numeral_simps bin_rest_numeral_simps] |
373 bintrunc.Suc [where bin="0", simplified bin_last_numeral_simps bin_rest_numeral_simps] |
420 |
374 |
421 lemmas bintrunc_Min [simp] = |
375 lemmas bintrunc_Min [simp] = |
422 bintrunc.Suc [where bin="-1", simplified bin_last_numeral_simps bin_rest_numeral_simps] |
376 bintrunc.Suc [where bin="-1", simplified bin_last_numeral_simps bin_rest_numeral_simps] |
423 |
377 |
424 lemmas bintrunc_BIT [simp] = |
378 lemmas bintrunc_BIT [simp] = |
425 bintrunc.Suc [where bin="w BIT b", simplified bin_last_BIT bin_rest_BIT] for w b |
379 bintrunc.Suc [where bin="w BIT b", simplified bin_last_BIT bin_rest_BIT] for w b |
426 |
380 |
427 lemmas bintrunc_Sucs = bintrunc_Pls bintrunc_Min bintrunc_BIT |
381 lemmas bintrunc_Sucs = bintrunc_Pls bintrunc_Min bintrunc_BIT |
428 bintrunc_Suc_numeral |
382 bintrunc_Suc_numeral |
429 |
383 |
430 lemmas sbintrunc_Suc_Pls = |
384 lemmas sbintrunc_Suc_Pls = |
431 sbintrunc.Suc [where bin="0", simplified bin_last_numeral_simps bin_rest_numeral_simps] |
385 sbintrunc.Suc [where bin="0", simplified bin_last_numeral_simps bin_rest_numeral_simps] |
432 |
386 |
433 lemmas sbintrunc_Suc_Min = |
387 lemmas sbintrunc_Suc_Min = |
434 sbintrunc.Suc [where bin="-1", simplified bin_last_numeral_simps bin_rest_numeral_simps] |
388 sbintrunc.Suc [where bin="-1", simplified bin_last_numeral_simps bin_rest_numeral_simps] |
435 |
389 |
436 lemmas sbintrunc_Suc_BIT [simp] = |
390 lemmas sbintrunc_Suc_BIT [simp] = |
437 sbintrunc.Suc [where bin="w BIT b", simplified bin_last_BIT bin_rest_BIT] for w b |
391 sbintrunc.Suc [where bin="w BIT b", simplified bin_last_BIT bin_rest_BIT] for w b |
438 |
392 |
439 lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min sbintrunc_Suc_BIT |
393 lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min sbintrunc_Suc_BIT |
440 sbintrunc_Suc_numeral |
394 sbintrunc_Suc_numeral |
441 |
395 |
442 lemmas sbintrunc_Pls = |
396 lemmas sbintrunc_Pls = |
443 sbintrunc.Z [where bin="0", |
397 sbintrunc.Z [where bin="0", simplified bin_last_numeral_simps bin_rest_numeral_simps] |
444 simplified bin_last_numeral_simps bin_rest_numeral_simps] |
398 |
445 |
399 lemmas sbintrunc_Min = |
446 lemmas sbintrunc_Min = |
400 sbintrunc.Z [where bin="-1", simplified bin_last_numeral_simps bin_rest_numeral_simps] |
447 sbintrunc.Z [where bin="-1", |
401 |
448 simplified bin_last_numeral_simps bin_rest_numeral_simps] |
402 lemmas sbintrunc_0_BIT_B0 [simp] = |
449 |
403 sbintrunc.Z [where bin="w BIT False", simplified bin_last_numeral_simps bin_rest_numeral_simps] |
450 lemmas sbintrunc_0_BIT_B0 [simp] = |
404 for w |
451 sbintrunc.Z [where bin="w BIT False", |
405 |
452 simplified bin_last_numeral_simps bin_rest_numeral_simps] for w |
406 lemmas sbintrunc_0_BIT_B1 [simp] = |
453 |
407 sbintrunc.Z [where bin="w BIT True", simplified bin_last_BIT bin_rest_numeral_simps] |
454 lemmas sbintrunc_0_BIT_B1 [simp] = |
408 for w |
455 sbintrunc.Z [where bin="w BIT True", |
|
456 simplified bin_last_BIT bin_rest_numeral_simps] for w |
|
457 |
409 |
458 lemmas sbintrunc_0_simps = |
410 lemmas sbintrunc_0_simps = |
459 sbintrunc_Pls sbintrunc_Min sbintrunc_0_BIT_B0 sbintrunc_0_BIT_B1 |
411 sbintrunc_Pls sbintrunc_Min sbintrunc_0_BIT_B0 sbintrunc_0_BIT_B1 |
460 |
412 |
461 lemmas bintrunc_simps = bintrunc.Z bintrunc_Sucs |
413 lemmas bintrunc_simps = bintrunc.Z bintrunc_Sucs |
462 lemmas sbintrunc_simps = sbintrunc_0_simps sbintrunc_Sucs |
414 lemmas sbintrunc_simps = sbintrunc_0_simps sbintrunc_Sucs |
463 |
415 |
464 lemma bintrunc_minus: |
416 lemma bintrunc_minus: "0 < n \<Longrightarrow> bintrunc (Suc (n - 1)) w = bintrunc n w" |
465 "0 < n ==> bintrunc (Suc (n - 1)) w = bintrunc n w" |
|
466 by auto |
417 by auto |
467 |
418 |
468 lemma sbintrunc_minus: |
419 lemma sbintrunc_minus: "0 < n \<Longrightarrow> sbintrunc (Suc (n - 1)) w = sbintrunc n w" |
469 "0 < n ==> sbintrunc (Suc (n - 1)) w = sbintrunc n w" |
|
470 by auto |
420 by auto |
471 |
421 |
472 lemmas bintrunc_minus_simps = |
422 lemmas bintrunc_minus_simps = |
473 bintrunc_Sucs [THEN [2] bintrunc_minus [symmetric, THEN trans]] |
423 bintrunc_Sucs [THEN [2] bintrunc_minus [symmetric, THEN trans]] |
474 lemmas sbintrunc_minus_simps = |
424 lemmas sbintrunc_minus_simps = |
475 sbintrunc_Sucs [THEN [2] sbintrunc_minus [symmetric, THEN trans]] |
425 sbintrunc_Sucs [THEN [2] sbintrunc_minus [symmetric, THEN trans]] |
476 |
426 |
477 lemmas thobini1 = arg_cong [where f = "%w. w BIT b"] for b |
427 lemmas thobini1 = arg_cong [where f = "\<lambda>w. w BIT b"] for b |
478 |
428 |
479 lemmas bintrunc_BIT_I = trans [OF bintrunc_BIT thobini1] |
429 lemmas bintrunc_BIT_I = trans [OF bintrunc_BIT thobini1] |
480 lemmas bintrunc_Min_I = trans [OF bintrunc_Min thobini1] |
430 lemmas bintrunc_Min_I = trans [OF bintrunc_Min thobini1] |
481 |
431 |
482 lemmas bmsts = bintrunc_minus_simps(1-3) [THEN thobini1 [THEN [2] trans]] |
432 lemmas bmsts = bintrunc_minus_simps(1-3) [THEN thobini1 [THEN [2] trans]] |
483 lemmas bintrunc_Pls_minus_I = bmsts(1) |
433 lemmas bintrunc_Pls_minus_I = bmsts(1) |
484 lemmas bintrunc_Min_minus_I = bmsts(2) |
434 lemmas bintrunc_Min_minus_I = bmsts(2) |
485 lemmas bintrunc_BIT_minus_I = bmsts(3) |
435 lemmas bintrunc_BIT_minus_I = bmsts(3) |
486 |
436 |
487 lemma bintrunc_Suc_lem: |
437 lemma bintrunc_Suc_lem: "bintrunc (Suc n) x = y \<Longrightarrow> m = Suc n \<Longrightarrow> bintrunc m x = y" |
488 "bintrunc (Suc n) x = y ==> m = Suc n ==> bintrunc m x = y" |
|
489 by auto |
438 by auto |
490 |
439 |
491 lemmas bintrunc_Suc_Ialts = |
440 lemmas bintrunc_Suc_Ialts = |
492 bintrunc_Min_I [THEN bintrunc_Suc_lem] |
441 bintrunc_Min_I [THEN bintrunc_Suc_lem] |
493 bintrunc_BIT_I [THEN bintrunc_Suc_lem] |
442 bintrunc_BIT_I [THEN bintrunc_Suc_lem] |
494 |
443 |
495 lemmas sbintrunc_BIT_I = trans [OF sbintrunc_Suc_BIT thobini1] |
444 lemmas sbintrunc_BIT_I = trans [OF sbintrunc_Suc_BIT thobini1] |
496 |
445 |
497 lemmas sbintrunc_Suc_Is = |
446 lemmas sbintrunc_Suc_Is = |
498 sbintrunc_Sucs(1-3) [THEN thobini1 [THEN [2] trans]] |
447 sbintrunc_Sucs(1-3) [THEN thobini1 [THEN [2] trans]] |
499 |
448 |
500 lemmas sbintrunc_Suc_minus_Is = |
449 lemmas sbintrunc_Suc_minus_Is = |
501 sbintrunc_minus_simps(1-3) [THEN thobini1 [THEN [2] trans]] |
450 sbintrunc_minus_simps(1-3) [THEN thobini1 [THEN [2] trans]] |
502 |
451 |
503 lemma sbintrunc_Suc_lem: |
452 lemma sbintrunc_Suc_lem: "sbintrunc (Suc n) x = y \<Longrightarrow> m = Suc n \<Longrightarrow> sbintrunc m x = y" |
504 "sbintrunc (Suc n) x = y ==> m = Suc n ==> sbintrunc m x = y" |
|
505 by auto |
453 by auto |
506 |
454 |
507 lemmas sbintrunc_Suc_Ialts = |
455 lemmas sbintrunc_Suc_Ialts = |
508 sbintrunc_Suc_Is [THEN sbintrunc_Suc_lem] |
456 sbintrunc_Suc_Is [THEN sbintrunc_Suc_lem] |
509 |
457 |
510 lemma sbintrunc_bintrunc_lt: |
458 lemma sbintrunc_bintrunc_lt: "m > n \<Longrightarrow> sbintrunc n (bintrunc m w) = sbintrunc n w" |
511 "m > n ==> sbintrunc n (bintrunc m w) = sbintrunc n w" |
|
512 by (rule bin_eqI) (auto simp: nth_sbintr nth_bintr) |
459 by (rule bin_eqI) (auto simp: nth_sbintr nth_bintr) |
513 |
460 |
514 lemma bintrunc_sbintrunc_le: |
461 lemma bintrunc_sbintrunc_le: "m \<le> Suc n \<Longrightarrow> bintrunc m (sbintrunc n w) = bintrunc m w" |
515 "m <= Suc n ==> bintrunc m (sbintrunc n w) = bintrunc m w" |
|
516 apply (rule bin_eqI) |
462 apply (rule bin_eqI) |
517 apply (auto simp: nth_sbintr nth_bintr) |
463 apply (auto simp: nth_sbintr nth_bintr) |
518 apply (subgoal_tac "x=n", safe, arith+)[1] |
464 apply (subgoal_tac "x=n", safe, arith+)[1] |
519 apply (subgoal_tac "x=n", safe, arith+)[1] |
465 apply (subgoal_tac "x=n", safe, arith+)[1] |
520 done |
466 done |
521 |
467 |
522 lemmas bintrunc_sbintrunc [simp] = order_refl [THEN bintrunc_sbintrunc_le] |
468 lemmas bintrunc_sbintrunc [simp] = order_refl [THEN bintrunc_sbintrunc_le] |
523 lemmas sbintrunc_bintrunc [simp] = lessI [THEN sbintrunc_bintrunc_lt] |
469 lemmas sbintrunc_bintrunc [simp] = lessI [THEN sbintrunc_bintrunc_lt] |
524 lemmas bintrunc_bintrunc [simp] = order_refl [THEN bintrunc_bintrunc_l] |
470 lemmas bintrunc_bintrunc [simp] = order_refl [THEN bintrunc_bintrunc_l] |
525 lemmas sbintrunc_sbintrunc [simp] = order_refl [THEN sbintrunc_sbintrunc_l] |
471 lemmas sbintrunc_sbintrunc [simp] = order_refl [THEN sbintrunc_sbintrunc_l] |
526 |
472 |
527 lemma bintrunc_sbintrunc' [simp]: |
473 lemma bintrunc_sbintrunc' [simp]: "0 < n \<Longrightarrow> bintrunc n (sbintrunc (n - 1) w) = bintrunc n w" |
528 "0 < n \<Longrightarrow> bintrunc n (sbintrunc (n - 1) w) = bintrunc n w" |
|
529 by (cases n) (auto simp del: bintrunc.Suc) |
474 by (cases n) (auto simp del: bintrunc.Suc) |
530 |
475 |
531 lemma sbintrunc_bintrunc' [simp]: |
476 lemma sbintrunc_bintrunc' [simp]: "0 < n \<Longrightarrow> sbintrunc (n - 1) (bintrunc n w) = sbintrunc (n - 1) w" |
532 "0 < n \<Longrightarrow> sbintrunc (n - 1) (bintrunc n w) = sbintrunc (n - 1) w" |
|
533 by (cases n) (auto simp del: bintrunc.Suc) |
477 by (cases n) (auto simp del: bintrunc.Suc) |
534 |
478 |
535 lemma bin_sbin_eq_iff: |
479 lemma bin_sbin_eq_iff: "bintrunc (Suc n) x = bintrunc (Suc n) y \<longleftrightarrow> sbintrunc n x = sbintrunc n y" |
536 "bintrunc (Suc n) x = bintrunc (Suc n) y \<longleftrightarrow> |
|
537 sbintrunc n x = sbintrunc n y" |
|
538 apply (rule iffI) |
480 apply (rule iffI) |
539 apply (rule box_equals [OF _ sbintrunc_bintrunc sbintrunc_bintrunc]) |
481 apply (rule box_equals [OF _ sbintrunc_bintrunc sbintrunc_bintrunc]) |
540 apply simp |
482 apply simp |
541 apply (rule box_equals [OF _ bintrunc_sbintrunc bintrunc_sbintrunc]) |
483 apply (rule box_equals [OF _ bintrunc_sbintrunc bintrunc_sbintrunc]) |
542 apply simp |
484 apply simp |
543 done |
485 done |
544 |
486 |
545 lemma bin_sbin_eq_iff': |
487 lemma bin_sbin_eq_iff': |
546 "0 < n \<Longrightarrow> bintrunc n x = bintrunc n y \<longleftrightarrow> |
488 "0 < n \<Longrightarrow> bintrunc n x = bintrunc n y \<longleftrightarrow> sbintrunc (n - 1) x = sbintrunc (n - 1) y" |
547 sbintrunc (n - 1) x = sbintrunc (n - 1) y" |
|
548 by (cases n) (simp_all add: bin_sbin_eq_iff del: bintrunc.Suc) |
489 by (cases n) (simp_all add: bin_sbin_eq_iff del: bintrunc.Suc) |
549 |
490 |
550 lemmas bintrunc_sbintruncS0 [simp] = bintrunc_sbintrunc' [unfolded One_nat_def] |
491 lemmas bintrunc_sbintruncS0 [simp] = bintrunc_sbintrunc' [unfolded One_nat_def] |
551 lemmas sbintrunc_bintruncS0 [simp] = sbintrunc_bintrunc' [unfolded One_nat_def] |
492 lemmas sbintrunc_bintruncS0 [simp] = sbintrunc_bintrunc' [unfolded One_nat_def] |
552 |
493 |
555 |
496 |
556 (* although bintrunc_minus_simps, if added to default simpset, |
497 (* although bintrunc_minus_simps, if added to default simpset, |
557 tends to get applied where it's not wanted in developing the theories, |
498 tends to get applied where it's not wanted in developing the theories, |
558 we get a version for when the word length is given literally *) |
499 we get a version for when the word length is given literally *) |
559 |
500 |
560 lemmas nat_non0_gr = |
501 lemmas nat_non0_gr = |
561 trans [OF iszero_def [THEN Not_eq_iff [THEN iffD2]] refl] |
502 trans [OF iszero_def [THEN Not_eq_iff [THEN iffD2]] refl] |
562 |
503 |
563 lemma bintrunc_numeral: |
504 lemma bintrunc_numeral: |
564 "bintrunc (numeral k) x = |
505 "bintrunc (numeral k) x = bintrunc (pred_numeral k) (bin_rest x) BIT bin_last x" |
565 bintrunc (pred_numeral k) (bin_rest x) BIT bin_last x" |
|
566 by (simp add: numeral_eq_Suc) |
506 by (simp add: numeral_eq_Suc) |
567 |
507 |
568 lemma sbintrunc_numeral: |
508 lemma sbintrunc_numeral: |
569 "sbintrunc (numeral k) x = |
509 "sbintrunc (numeral k) x = sbintrunc (pred_numeral k) (bin_rest x) BIT bin_last x" |
570 sbintrunc (pred_numeral k) (bin_rest x) BIT bin_last x" |
|
571 by (simp add: numeral_eq_Suc) |
510 by (simp add: numeral_eq_Suc) |
572 |
511 |
573 lemma bintrunc_numeral_simps [simp]: |
512 lemma bintrunc_numeral_simps [simp]: |
574 "bintrunc (numeral k) (numeral (Num.Bit0 w)) = |
513 "bintrunc (numeral k) (numeral (Num.Bit0 w)) = bintrunc (pred_numeral k) (numeral w) BIT False" |
575 bintrunc (pred_numeral k) (numeral w) BIT False" |
514 "bintrunc (numeral k) (numeral (Num.Bit1 w)) = bintrunc (pred_numeral k) (numeral w) BIT True" |
576 "bintrunc (numeral k) (numeral (Num.Bit1 w)) = |
515 "bintrunc (numeral k) (- numeral (Num.Bit0 w)) = bintrunc (pred_numeral k) (- numeral w) BIT False" |
577 bintrunc (pred_numeral k) (numeral w) BIT True" |
|
578 "bintrunc (numeral k) (- numeral (Num.Bit0 w)) = |
|
579 bintrunc (pred_numeral k) (- numeral w) BIT False" |
|
580 "bintrunc (numeral k) (- numeral (Num.Bit1 w)) = |
516 "bintrunc (numeral k) (- numeral (Num.Bit1 w)) = |
581 bintrunc (pred_numeral k) (- numeral (w + Num.One)) BIT True" |
517 bintrunc (pred_numeral k) (- numeral (w + Num.One)) BIT True" |
582 "bintrunc (numeral k) 1 = 1" |
518 "bintrunc (numeral k) 1 = 1" |
583 by (simp_all add: bintrunc_numeral) |
519 by (simp_all add: bintrunc_numeral) |
584 |
520 |
585 lemma sbintrunc_numeral_simps [simp]: |
521 lemma sbintrunc_numeral_simps [simp]: |
586 "sbintrunc (numeral k) (numeral (Num.Bit0 w)) = |
522 "sbintrunc (numeral k) (numeral (Num.Bit0 w)) = sbintrunc (pred_numeral k) (numeral w) BIT False" |
587 sbintrunc (pred_numeral k) (numeral w) BIT False" |
523 "sbintrunc (numeral k) (numeral (Num.Bit1 w)) = sbintrunc (pred_numeral k) (numeral w) BIT True" |
588 "sbintrunc (numeral k) (numeral (Num.Bit1 w)) = |
|
589 sbintrunc (pred_numeral k) (numeral w) BIT True" |
|
590 "sbintrunc (numeral k) (- numeral (Num.Bit0 w)) = |
524 "sbintrunc (numeral k) (- numeral (Num.Bit0 w)) = |
591 sbintrunc (pred_numeral k) (- numeral w) BIT False" |
525 sbintrunc (pred_numeral k) (- numeral w) BIT False" |
592 "sbintrunc (numeral k) (- numeral (Num.Bit1 w)) = |
526 "sbintrunc (numeral k) (- numeral (Num.Bit1 w)) = |
593 sbintrunc (pred_numeral k) (- numeral (w + Num.One)) BIT True" |
527 sbintrunc (pred_numeral k) (- numeral (w + Num.One)) BIT True" |
594 "sbintrunc (numeral k) 1 = 1" |
528 "sbintrunc (numeral k) 1 = 1" |
595 by (simp_all add: sbintrunc_numeral) |
529 by (simp_all add: sbintrunc_numeral) |
596 |
530 |
597 lemma no_bintr_alt1: "bintrunc n = (\<lambda>w. w mod 2 ^ n :: int)" |
531 lemma no_bintr_alt1: "bintrunc n = (\<lambda>w. w mod 2 ^ n :: int)" |
598 by (rule ext) (rule bintrunc_mod2p) |
532 by (rule ext) (rule bintrunc_mod2p) |
599 |
533 |
600 lemma range_bintrunc: "range (bintrunc n) = {i. 0 <= i & i < 2 ^ n}" |
534 lemma range_bintrunc: "range (bintrunc n) = {i. 0 \<le> i \<and> i < 2 ^ n}" |
601 apply (unfold no_bintr_alt1) |
535 apply (unfold no_bintr_alt1) |
602 apply (auto simp add: image_iff) |
536 apply (auto simp add: image_iff) |
603 apply (rule exI) |
537 apply (rule exI) |
604 apply (auto intro: int_mod_lem [THEN iffD1, symmetric]) |
538 apply (auto intro: int_mod_lem [THEN iffD1, symmetric]) |
605 done |
539 done |
606 |
540 |
607 lemma no_sbintr_alt2: |
541 lemma no_sbintr_alt2: "sbintrunc n = (\<lambda>w. (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n :: int)" |
608 "sbintrunc n = (%w. (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n :: int)" |
|
609 by (rule ext) (simp add : sbintrunc_mod2p) |
542 by (rule ext) (simp add : sbintrunc_mod2p) |
610 |
543 |
611 lemma range_sbintrunc: |
544 lemma range_sbintrunc: "range (sbintrunc n) = {i. - (2 ^ n) \<le> i \<and> i < 2 ^ n}" |
612 "range (sbintrunc n) = {i. - (2 ^ n) <= i & i < 2 ^ n}" |
|
613 apply (unfold no_sbintr_alt2) |
545 apply (unfold no_sbintr_alt2) |
614 apply (auto simp add: image_iff eq_diff_eq) |
546 apply (auto simp add: image_iff eq_diff_eq) |
615 apply (rule exI) |
547 apply (rule exI) |
616 apply (auto intro: int_mod_lem [THEN iffD1, symmetric]) |
548 apply (auto intro: int_mod_lem [THEN iffD1, symmetric]) |
617 done |
549 done |
618 |
550 |
619 lemma sb_inc_lem: |
551 lemma sb_inc_lem: "a + 2^k < 0 \<Longrightarrow> a + 2^k + 2^(Suc k) \<le> (a + 2^k) mod 2^(Suc k)" |
620 "(a::int) + 2^k < 0 \<Longrightarrow> a + 2^k + 2^(Suc k) <= (a + 2^k) mod 2^(Suc k)" |
552 for a :: int |
621 apply (erule int_mod_ge' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k", simplified zless2p]) |
553 apply (erule int_mod_ge' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k", simplified zless2p]) |
622 apply (rule TrueI) |
554 apply (rule TrueI) |
623 done |
555 done |
624 |
556 |
625 lemma sb_inc_lem': |
557 lemma sb_inc_lem': "a < - (2^k) \<Longrightarrow> a + 2^k + 2^(Suc k) \<le> (a + 2^k) mod 2^(Suc k)" |
626 "(a::int) < - (2^k) \<Longrightarrow> a + 2^k + 2^(Suc k) <= (a + 2^k) mod 2^(Suc k)" |
558 for a :: int |
627 by (rule sb_inc_lem) simp |
559 by (rule sb_inc_lem) simp |
628 |
560 |
629 lemma sbintrunc_inc: |
561 lemma sbintrunc_inc: "x < - (2^n) \<Longrightarrow> x + 2^(Suc n) \<le> sbintrunc n x" |
630 "x < - (2^n) ==> x + 2^(Suc n) <= sbintrunc n x" |
|
631 unfolding no_sbintr_alt2 by (drule sb_inc_lem') simp |
562 unfolding no_sbintr_alt2 by (drule sb_inc_lem') simp |
632 |
563 |
633 lemma sb_dec_lem: |
564 lemma sb_dec_lem: "0 \<le> - (2 ^ k) + a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a" |
634 "(0::int) \<le> - (2 ^ k) + a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a" |
565 for a :: int |
635 using int_mod_le'[where n = "2 ^ (Suc k)" and b = "a + 2 ^ k"] by simp |
566 using int_mod_le'[where n = "2 ^ (Suc k)" and b = "a + 2 ^ k"] by simp |
636 |
567 |
637 lemma sb_dec_lem': |
568 lemma sb_dec_lem': "2 ^ k \<le> a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a" |
638 "(2::int) ^ k \<le> a \<Longrightarrow> (a + 2 ^ k) mod (2 * 2 ^ k) \<le> - (2 ^ k) + a" |
569 for a :: int |
639 by (rule sb_dec_lem) simp |
570 by (rule sb_dec_lem) simp |
640 |
571 |
641 lemma sbintrunc_dec: |
572 lemma sbintrunc_dec: "x \<ge> (2 ^ n) \<Longrightarrow> x - 2 ^ (Suc n) >= sbintrunc n x" |
642 "x >= (2 ^ n) ==> x - 2 ^ (Suc n) >= sbintrunc n x" |
|
643 unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp |
573 unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp |
644 |
574 |
645 lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p] |
575 lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p] |
646 |
576 |
647 lemma bintr_ge0: "0 \<le> bintrunc n w" |
577 lemma bintr_ge0: "0 \<le> bintrunc n w" |
657 by (simp add: sbintrunc_mod2p) |
587 by (simp add: sbintrunc_mod2p) |
658 |
588 |
659 lemma sbintr_lt: "sbintrunc n w < 2 ^ n" |
589 lemma sbintr_lt: "sbintrunc n w < 2 ^ n" |
660 by (simp add: sbintrunc_mod2p) |
590 by (simp add: sbintrunc_mod2p) |
661 |
591 |
662 lemma sign_Pls_ge_0: |
592 lemma sign_Pls_ge_0: "bin_sign bin = 0 \<longleftrightarrow> bin \<ge> 0" |
663 "(bin_sign bin = 0) = (bin >= (0 :: int))" |
593 for bin :: int |
664 unfolding bin_sign_def by simp |
594 by (simp add: bin_sign_def) |
665 |
595 |
666 lemma sign_Min_lt_0: |
596 lemma sign_Min_lt_0: "bin_sign bin = -1 \<longleftrightarrow> bin < 0" |
667 "(bin_sign bin = -1) = (bin < (0 :: int))" |
597 for bin :: int |
668 unfolding bin_sign_def by simp |
598 by (simp add: bin_sign_def) |
669 |
599 |
670 lemma bin_rest_trunc: |
600 lemma bin_rest_trunc: "bin_rest (bintrunc n bin) = bintrunc (n - 1) (bin_rest bin)" |
671 "(bin_rest (bintrunc n bin)) = bintrunc (n - 1) (bin_rest bin)" |
|
672 by (induct n arbitrary: bin) auto |
601 by (induct n arbitrary: bin) auto |
673 |
602 |
674 lemma bin_rest_power_trunc: |
603 lemma bin_rest_power_trunc: |
675 "(bin_rest ^^ k) (bintrunc n bin) = |
604 "(bin_rest ^^ k) (bintrunc n bin) = bintrunc (n - k) ((bin_rest ^^ k) bin)" |
676 bintrunc (n - k) ((bin_rest ^^ k) bin)" |
|
677 by (induct k) (auto simp: bin_rest_trunc) |
605 by (induct k) (auto simp: bin_rest_trunc) |
678 |
606 |
679 lemma bin_rest_trunc_i: |
607 lemma bin_rest_trunc_i: "bintrunc n (bin_rest bin) = bin_rest (bintrunc (Suc n) bin)" |
680 "bintrunc n (bin_rest bin) = bin_rest (bintrunc (Suc n) bin)" |
|
681 by auto |
608 by auto |
682 |
609 |
683 lemma bin_rest_strunc: |
610 lemma bin_rest_strunc: "bin_rest (sbintrunc (Suc n) bin) = sbintrunc n (bin_rest bin)" |
684 "bin_rest (sbintrunc (Suc n) bin) = sbintrunc n (bin_rest bin)" |
|
685 by (induct n arbitrary: bin) auto |
611 by (induct n arbitrary: bin) auto |
686 |
612 |
687 lemma bintrunc_rest [simp]: |
613 lemma bintrunc_rest [simp]: "bintrunc n (bin_rest (bintrunc n bin)) = bin_rest (bintrunc n bin)" |
688 "bintrunc n (bin_rest (bintrunc n bin)) = bin_rest (bintrunc n bin)" |
614 apply (induct n arbitrary: bin) |
689 apply (induct n arbitrary: bin, simp) |
615 apply simp |
690 apply (case_tac bin rule: bin_exhaust) |
616 apply (case_tac bin rule: bin_exhaust) |
691 apply (auto simp: bintrunc_bintrunc_l) |
617 apply (auto simp: bintrunc_bintrunc_l) |
692 done |
618 done |
693 |
619 |
694 lemma sbintrunc_rest [simp]: |
620 lemma sbintrunc_rest [simp]: "sbintrunc n (bin_rest (sbintrunc n bin)) = bin_rest (sbintrunc n bin)" |
695 "sbintrunc n (bin_rest (sbintrunc n bin)) = bin_rest (sbintrunc n bin)" |
621 apply (induct n arbitrary: bin) |
696 apply (induct n arbitrary: bin, simp) |
622 apply simp |
697 apply (case_tac bin rule: bin_exhaust) |
623 apply (case_tac bin rule: bin_exhaust) |
698 apply (auto simp: bintrunc_bintrunc_l split: bool.splits) |
624 apply (auto simp: bintrunc_bintrunc_l split: bool.splits) |
699 done |
625 done |
700 |
626 |
701 lemma bintrunc_rest': |
627 lemma bintrunc_rest': "bintrunc n \<circ> bin_rest \<circ> bintrunc n = bin_rest \<circ> bintrunc n" |
702 "bintrunc n o bin_rest o bintrunc n = bin_rest o bintrunc n" |
|
703 by (rule ext) auto |
628 by (rule ext) auto |
704 |
629 |
705 lemma sbintrunc_rest' : |
630 lemma sbintrunc_rest': "sbintrunc n \<circ> bin_rest \<circ> sbintrunc n = bin_rest \<circ> sbintrunc n" |
706 "sbintrunc n o bin_rest o sbintrunc n = bin_rest o sbintrunc n" |
|
707 by (rule ext) auto |
631 by (rule ext) auto |
708 |
632 |
709 lemma rco_lem: |
633 lemma rco_lem: "f \<circ> g \<circ> f = g \<circ> f \<Longrightarrow> f \<circ> (g \<circ> f) ^^ n = g ^^ n \<circ> f" |
710 "f o g o f = g o f ==> f o (g o f) ^^ n = g ^^ n o f" |
|
711 apply (rule ext) |
634 apply (rule ext) |
712 apply (induct_tac n) |
635 apply (induct_tac n) |
713 apply (simp_all (no_asm)) |
636 apply (simp_all (no_asm)) |
714 apply (drule fun_cong) |
637 apply (drule fun_cong) |
715 apply (unfold o_def) |
638 apply (unfold o_def) |
716 apply (erule trans) |
639 apply (erule trans) |
717 apply simp |
640 apply simp |
718 done |
641 done |
719 |
642 |
720 lemmas rco_bintr = bintrunc_rest' |
643 lemmas rco_bintr = bintrunc_rest' |
721 [THEN rco_lem [THEN fun_cong], unfolded o_def] |
644 [THEN rco_lem [THEN fun_cong], unfolded o_def] |
722 lemmas rco_sbintr = sbintrunc_rest' |
645 lemmas rco_sbintr = sbintrunc_rest' |
723 [THEN rco_lem [THEN fun_cong], unfolded o_def] |
646 [THEN rco_lem [THEN fun_cong], unfolded o_def] |
724 |
647 |
725 |
648 |
726 subsection \<open>Splitting and concatenation\<close> |
649 subsection \<open>Splitting and concatenation\<close> |
727 |
650 |
728 primrec bin_split :: "nat \<Rightarrow> int \<Rightarrow> int \<times> int" where |
651 primrec bin_split :: "nat \<Rightarrow> int \<Rightarrow> int \<times> int" |
729 Z: "bin_split 0 w = (w, 0)" |
652 where |
730 | Suc: "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w) |
653 Z: "bin_split 0 w = (w, 0)" |
731 in (w1, w2 BIT bin_last w))" |
654 | Suc: "bin_split (Suc n) w = |
|
655 (let (w1, w2) = bin_split n (bin_rest w) |
|
656 in (w1, w2 BIT bin_last w))" |
732 |
657 |
733 lemma [code]: |
658 lemma [code]: |
734 "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w) in (w1, w2 BIT bin_last w))" |
659 "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w) in (w1, w2 BIT bin_last w))" |
735 "bin_split 0 w = (w, 0)" |
660 "bin_split 0 w = (w, 0)" |
736 by simp_all |
661 by simp_all |
737 |
662 |
738 primrec bin_cat :: "int \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int" where |
663 primrec bin_cat :: "int \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int" |
739 Z: "bin_cat w 0 v = w" |
664 where |
|
665 Z: "bin_cat w 0 v = w" |
740 | Suc: "bin_cat w (Suc n) v = bin_cat w n (bin_rest v) BIT bin_last v" |
666 | Suc: "bin_cat w (Suc n) v = bin_cat w n (bin_rest v) BIT bin_last v" |
741 |
667 |
742 end |
668 end |
743 |
|