|
1 (* |
|
2 Author: Jeremy Dawson, NICTA |
|
3 |
|
4 contains basic definition to do with integers |
|
5 expressed using Pls, Min, BIT and important resulting theorems, |
|
6 in particular, bin_rec and related work |
|
7 *) |
|
8 |
|
9 header {* Basic Definitions for Binary Integers *} |
|
10 |
|
11 theory Bit_Representation |
|
12 imports Misc_Numeric Bit |
|
13 begin |
|
14 |
|
15 subsection {* Further properties of numerals *} |
|
16 |
|
17 definition Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where |
|
18 "k BIT b = bit_case 0 1 b + k + k" |
|
19 |
|
20 lemma BIT_B0_eq_Bit0 [simp]: "w BIT 0 = Int.Bit0 w" |
|
21 unfolding Bit_def Bit0_def by simp |
|
22 |
|
23 lemma BIT_B1_eq_Bit1 [simp]: "w BIT 1 = Int.Bit1 w" |
|
24 unfolding Bit_def Bit1_def by simp |
|
25 |
|
26 lemmas BIT_simps = BIT_B0_eq_Bit0 BIT_B1_eq_Bit1 |
|
27 |
|
28 lemma Min_ne_Pls [iff]: |
|
29 "Int.Min ~= Int.Pls" |
|
30 unfolding Min_def Pls_def by auto |
|
31 |
|
32 lemmas Pls_ne_Min [iff] = Min_ne_Pls [symmetric] |
|
33 |
|
34 lemmas PlsMin_defs [intro!] = |
|
35 Pls_def Min_def Pls_def [symmetric] Min_def [symmetric] |
|
36 |
|
37 lemmas PlsMin_simps [simp] = PlsMin_defs [THEN Eq_TrueI] |
|
38 |
|
39 lemma number_of_False_cong: |
|
40 "False \<Longrightarrow> number_of x = number_of y" |
|
41 by (rule FalseE) |
|
42 |
|
43 (** ways in which type Bin resembles a datatype **) |
|
44 |
|
45 lemma BIT_eq: "u BIT b = v BIT c ==> u = v & b = c" |
|
46 apply (unfold Bit_def) |
|
47 apply (simp (no_asm_use) split: bit.split_asm) |
|
48 apply simp_all |
|
49 apply (drule_tac f=even in arg_cong, clarsimp)+ |
|
50 done |
|
51 |
|
52 lemmas BIT_eqE [elim!] = BIT_eq [THEN conjE, standard] |
|
53 |
|
54 lemma BIT_eq_iff [simp]: |
|
55 "(u BIT b = v BIT c) = (u = v \<and> b = c)" |
|
56 by (rule iffI) auto |
|
57 |
|
58 lemmas BIT_eqI [intro!] = conjI [THEN BIT_eq_iff [THEN iffD2]] |
|
59 |
|
60 lemma less_Bits: |
|
61 "(v BIT b < w BIT c) = (v < w | v <= w & b = (0::bit) & c = (1::bit))" |
|
62 unfolding Bit_def by (auto split: bit.split) |
|
63 |
|
64 lemma le_Bits: |
|
65 "(v BIT b <= w BIT c) = (v < w | v <= w & (b ~= (1::bit) | c ~= (0::bit)))" |
|
66 unfolding Bit_def by (auto split: bit.split) |
|
67 |
|
68 lemma no_no [simp]: "number_of (number_of i) = i" |
|
69 unfolding number_of_eq by simp |
|
70 |
|
71 lemma Bit_B0: |
|
72 "k BIT (0::bit) = k + k" |
|
73 by (unfold Bit_def) simp |
|
74 |
|
75 lemma Bit_B1: |
|
76 "k BIT (1::bit) = k + k + 1" |
|
77 by (unfold Bit_def) simp |
|
78 |
|
79 lemma Bit_B0_2t: "k BIT (0::bit) = 2 * k" |
|
80 by (rule trans, rule Bit_B0) simp |
|
81 |
|
82 lemma Bit_B1_2t: "k BIT (1::bit) = 2 * k + 1" |
|
83 by (rule trans, rule Bit_B1) simp |
|
84 |
|
85 lemma B_mod_2': |
|
86 "X = 2 ==> (w BIT (1::bit)) mod X = 1 & (w BIT (0::bit)) mod X = 0" |
|
87 apply (simp (no_asm) only: Bit_B0 Bit_B1) |
|
88 apply (simp add: z1pmod2) |
|
89 done |
|
90 |
|
91 lemma B1_mod_2 [simp]: "(Int.Bit1 w) mod 2 = 1" |
|
92 unfolding numeral_simps number_of_is_id by (simp add: z1pmod2) |
|
93 |
|
94 lemma B0_mod_2 [simp]: "(Int.Bit0 w) mod 2 = 0" |
|
95 unfolding numeral_simps number_of_is_id by simp |
|
96 |
|
97 lemma neB1E [elim!]: |
|
98 assumes ne: "y \<noteq> (1::bit)" |
|
99 assumes y: "y = (0::bit) \<Longrightarrow> P" |
|
100 shows "P" |
|
101 apply (rule y) |
|
102 apply (cases y rule: bit.exhaust, simp) |
|
103 apply (simp add: ne) |
|
104 done |
|
105 |
|
106 lemma bin_ex_rl: "EX w b. w BIT b = bin" |
|
107 apply (unfold Bit_def) |
|
108 apply (cases "even bin") |
|
109 apply (clarsimp simp: even_equiv_def) |
|
110 apply (auto simp: odd_equiv_def split: bit.split) |
|
111 done |
|
112 |
|
113 lemma bin_exhaust: |
|
114 assumes Q: "\<And>x b. bin = x BIT b \<Longrightarrow> Q" |
|
115 shows "Q" |
|
116 apply (insert bin_ex_rl [of bin]) |
|
117 apply (erule exE)+ |
|
118 apply (rule Q) |
|
119 apply force |
|
120 done |
|
121 |
|
122 |
|
123 subsection {* Destructors for binary integers *} |
|
124 |
|
125 definition bin_last :: "int \<Rightarrow> bit" where |
|
126 "bin_last w = (if w mod 2 = 0 then (0::bit) else (1::bit))" |
|
127 |
|
128 definition bin_rest :: "int \<Rightarrow> int" where |
|
129 "bin_rest w = w div 2" |
|
130 |
|
131 definition bin_rl :: "int \<Rightarrow> int \<times> bit" where |
|
132 "bin_rl w = (bin_rest w, bin_last w)" |
|
133 |
|
134 lemma bin_rl_char: "bin_rl w = (r, l) \<longleftrightarrow> r BIT l = w" |
|
135 apply (cases l) |
|
136 apply (auto simp add: bin_rl_def bin_last_def bin_rest_def) |
|
137 unfolding Pls_def Min_def Bit0_def Bit1_def number_of_is_id |
|
138 apply arith+ |
|
139 done |
|
140 |
|
141 primrec bin_nth where |
|
142 Z: "bin_nth w 0 = (bin_last w = (1::bit))" |
|
143 | Suc: "bin_nth w (Suc n) = bin_nth (bin_rest w) n" |
|
144 |
|
145 lemma bin_rl_simps [simp]: |
|
146 "bin_rl Int.Pls = (Int.Pls, (0::bit))" |
|
147 "bin_rl Int.Min = (Int.Min, (1::bit))" |
|
148 "bin_rl (Int.Bit0 r) = (r, (0::bit))" |
|
149 "bin_rl (Int.Bit1 r) = (r, (1::bit))" |
|
150 "bin_rl (r BIT b) = (r, b)" |
|
151 unfolding bin_rl_char by simp_all |
|
152 |
|
153 lemma bin_rl_simp [simp]: |
|
154 "bin_rest w BIT bin_last w = w" |
|
155 by (simp add: iffD1 [OF bin_rl_char bin_rl_def]) |
|
156 |
|
157 lemma bin_abs_lem: |
|
158 "bin = (w BIT b) ==> ~ bin = Int.Min --> ~ bin = Int.Pls --> |
|
159 nat (abs w) < nat (abs bin)" |
|
160 apply (clarsimp simp add: bin_rl_char) |
|
161 apply (unfold Pls_def Min_def Bit_def) |
|
162 apply (cases b) |
|
163 apply (clarsimp, arith) |
|
164 apply (clarsimp, arith) |
|
165 done |
|
166 |
|
167 lemma bin_induct: |
|
168 assumes PPls: "P Int.Pls" |
|
169 and PMin: "P Int.Min" |
|
170 and PBit: "!!bin bit. P bin ==> P (bin BIT bit)" |
|
171 shows "P bin" |
|
172 apply (rule_tac P=P and a=bin and f1="nat o abs" |
|
173 in wf_measure [THEN wf_induct]) |
|
174 apply (simp add: measure_def inv_image_def) |
|
175 apply (case_tac x rule: bin_exhaust) |
|
176 apply (frule bin_abs_lem) |
|
177 apply (auto simp add : PPls PMin PBit) |
|
178 done |
|
179 |
|
180 lemma numeral_induct: |
|
181 assumes Pls: "P Int.Pls" |
|
182 assumes Min: "P Int.Min" |
|
183 assumes Bit0: "\<And>w. \<lbrakk>P w; w \<noteq> Int.Pls\<rbrakk> \<Longrightarrow> P (Int.Bit0 w)" |
|
184 assumes Bit1: "\<And>w. \<lbrakk>P w; w \<noteq> Int.Min\<rbrakk> \<Longrightarrow> P (Int.Bit1 w)" |
|
185 shows "P x" |
|
186 apply (induct x rule: bin_induct) |
|
187 apply (rule Pls) |
|
188 apply (rule Min) |
|
189 apply (case_tac bit) |
|
190 apply (case_tac "bin = Int.Pls") |
|
191 apply simp |
|
192 apply (simp add: Bit0) |
|
193 apply (case_tac "bin = Int.Min") |
|
194 apply simp |
|
195 apply (simp add: Bit1) |
|
196 done |
|
197 |
|
198 lemma bin_rest_simps [simp]: |
|
199 "bin_rest Int.Pls = Int.Pls" |
|
200 "bin_rest Int.Min = Int.Min" |
|
201 "bin_rest (Int.Bit0 w) = w" |
|
202 "bin_rest (Int.Bit1 w) = w" |
|
203 "bin_rest (w BIT b) = w" |
|
204 using bin_rl_simps bin_rl_def by auto |
|
205 |
|
206 lemma bin_last_simps [simp]: |
|
207 "bin_last Int.Pls = (0::bit)" |
|
208 "bin_last Int.Min = (1::bit)" |
|
209 "bin_last (Int.Bit0 w) = (0::bit)" |
|
210 "bin_last (Int.Bit1 w) = (1::bit)" |
|
211 "bin_last (w BIT b) = b" |
|
212 using bin_rl_simps bin_rl_def by auto |
|
213 |
|
214 lemma bin_r_l_extras [simp]: |
|
215 "bin_last 0 = (0::bit)" |
|
216 "bin_last (- 1) = (1::bit)" |
|
217 "bin_last -1 = (1::bit)" |
|
218 "bin_last 1 = (1::bit)" |
|
219 "bin_rest 1 = 0" |
|
220 "bin_rest 0 = 0" |
|
221 "bin_rest (- 1) = - 1" |
|
222 "bin_rest -1 = -1" |
|
223 by (simp_all add: bin_last_def bin_rest_def) |
|
224 |
|
225 lemma bin_last_mod: |
|
226 "bin_last w = (if w mod 2 = 0 then (0::bit) else (1::bit))" |
|
227 apply (case_tac w rule: bin_exhaust) |
|
228 apply (case_tac b) |
|
229 apply auto |
|
230 done |
|
231 |
|
232 lemma bin_rest_div: |
|
233 "bin_rest w = w div 2" |
|
234 apply (case_tac w rule: bin_exhaust) |
|
235 apply (rule trans) |
|
236 apply clarsimp |
|
237 apply (rule refl) |
|
238 apply (drule trans) |
|
239 apply (rule Bit_def) |
|
240 apply (simp add: z1pdiv2 split: bit.split) |
|
241 done |
|
242 |
|
243 lemma Bit_div2 [simp]: "(w BIT b) div 2 = w" |
|
244 unfolding bin_rest_div [symmetric] by auto |
|
245 |
|
246 lemma Bit0_div2 [simp]: "(Int.Bit0 w) div 2 = w" |
|
247 using Bit_div2 [where b="(0::bit)"] by simp |
|
248 |
|
249 lemma Bit1_div2 [simp]: "(Int.Bit1 w) div 2 = w" |
|
250 using Bit_div2 [where b="(1::bit)"] by simp |
|
251 |
|
252 lemma bin_nth_lem [rule_format]: |
|
253 "ALL y. bin_nth x = bin_nth y --> x = y" |
|
254 apply (induct x rule: bin_induct) |
|
255 apply safe |
|
256 apply (erule rev_mp) |
|
257 apply (induct_tac y rule: bin_induct) |
|
258 apply (safe del: subset_antisym) |
|
259 apply (drule_tac x=0 in fun_cong, force) |
|
260 apply (erule notE, rule ext, |
|
261 drule_tac x="Suc x" in fun_cong, force) |
|
262 apply (drule_tac x=0 in fun_cong, force) |
|
263 apply (erule rev_mp) |
|
264 apply (induct_tac y rule: bin_induct) |
|
265 apply (safe del: subset_antisym) |
|
266 apply (drule_tac x=0 in fun_cong, force) |
|
267 apply (erule notE, rule ext, |
|
268 drule_tac x="Suc x" in fun_cong, force) |
|
269 apply (drule_tac x=0 in fun_cong, force) |
|
270 apply (case_tac y rule: bin_exhaust) |
|
271 apply clarify |
|
272 apply (erule allE) |
|
273 apply (erule impE) |
|
274 prefer 2 |
|
275 apply (erule BIT_eqI) |
|
276 apply (drule_tac x=0 in fun_cong, force) |
|
277 apply (rule ext) |
|
278 apply (drule_tac x="Suc ?x" in fun_cong, force) |
|
279 done |
|
280 |
|
281 lemma bin_nth_eq_iff: "(bin_nth x = bin_nth y) = (x = y)" |
|
282 by (auto elim: bin_nth_lem) |
|
283 |
|
284 lemmas bin_eqI = ext [THEN bin_nth_eq_iff [THEN iffD1], standard] |
|
285 |
|
286 lemma bin_nth_Pls [simp]: "~ bin_nth Int.Pls n" |
|
287 by (induct n) auto |
|
288 |
|
289 lemma bin_nth_Min [simp]: "bin_nth Int.Min n" |
|
290 by (induct n) auto |
|
291 |
|
292 lemma bin_nth_0_BIT: "bin_nth (w BIT b) 0 = (b = (1::bit))" |
|
293 by auto |
|
294 |
|
295 lemma bin_nth_Suc_BIT: "bin_nth (w BIT b) (Suc n) = bin_nth w n" |
|
296 by auto |
|
297 |
|
298 lemma bin_nth_minus [simp]: "0 < n ==> bin_nth (w BIT b) n = bin_nth w (n - 1)" |
|
299 by (cases n) auto |
|
300 |
|
301 lemma bin_nth_minus_Bit0 [simp]: |
|
302 "0 < n ==> bin_nth (Int.Bit0 w) n = bin_nth w (n - 1)" |
|
303 using bin_nth_minus [where b="(0::bit)"] by simp |
|
304 |
|
305 lemma bin_nth_minus_Bit1 [simp]: |
|
306 "0 < n ==> bin_nth (Int.Bit1 w) n = bin_nth w (n - 1)" |
|
307 using bin_nth_minus [where b="(1::bit)"] by simp |
|
308 |
|
309 lemmas bin_nth_0 = bin_nth.simps(1) |
|
310 lemmas bin_nth_Suc = bin_nth.simps(2) |
|
311 |
|
312 lemmas bin_nth_simps = |
|
313 bin_nth_0 bin_nth_Suc bin_nth_Pls bin_nth_Min bin_nth_minus |
|
314 bin_nth_minus_Bit0 bin_nth_minus_Bit1 |
|
315 |
|
316 |
|
317 subsection {* Recursion combinator for binary integers *} |
|
318 |
|
319 lemma brlem: "(bin = Int.Min) = (- bin + Int.pred 0 = 0)" |
|
320 unfolding Min_def pred_def by arith |
|
321 |
|
322 function |
|
323 bin_rec :: "'a \<Rightarrow> 'a \<Rightarrow> (int \<Rightarrow> bit \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> int \<Rightarrow> 'a" |
|
324 where |
|
325 "bin_rec f1 f2 f3 bin = (if bin = Int.Pls then f1 |
|
326 else if bin = Int.Min then f2 |
|
327 else case bin_rl bin of (w, b) => f3 w b (bin_rec f1 f2 f3 w))" |
|
328 by pat_completeness auto |
|
329 |
|
330 termination |
|
331 apply (relation "measure (nat o abs o snd o snd o snd)") |
|
332 apply (auto simp add: bin_rl_def bin_last_def bin_rest_def) |
|
333 unfolding Pls_def Min_def Bit0_def Bit1_def number_of_is_id |
|
334 apply auto |
|
335 done |
|
336 |
|
337 declare bin_rec.simps [simp del] |
|
338 |
|
339 lemma bin_rec_PM: |
|
340 "f = bin_rec f1 f2 f3 ==> f Int.Pls = f1 & f Int.Min = f2" |
|
341 by (auto simp add: bin_rec.simps) |
|
342 |
|
343 lemma bin_rec_Pls: "bin_rec f1 f2 f3 Int.Pls = f1" |
|
344 by (simp add: bin_rec.simps) |
|
345 |
|
346 lemma bin_rec_Min: "bin_rec f1 f2 f3 Int.Min = f2" |
|
347 by (simp add: bin_rec.simps) |
|
348 |
|
349 lemma bin_rec_Bit0: |
|
350 "f3 Int.Pls (0::bit) f1 = f1 \<Longrightarrow> |
|
351 bin_rec f1 f2 f3 (Int.Bit0 w) = f3 w (0::bit) (bin_rec f1 f2 f3 w)" |
|
352 by (simp add: bin_rec_Pls bin_rec.simps [of _ _ _ "Int.Bit0 w"]) |
|
353 |
|
354 lemma bin_rec_Bit1: |
|
355 "f3 Int.Min (1::bit) f2 = f2 \<Longrightarrow> |
|
356 bin_rec f1 f2 f3 (Int.Bit1 w) = f3 w (1::bit) (bin_rec f1 f2 f3 w)" |
|
357 by (simp add: bin_rec_Min bin_rec.simps [of _ _ _ "Int.Bit1 w"]) |
|
358 |
|
359 lemma bin_rec_Bit: |
|
360 "f = bin_rec f1 f2 f3 ==> f3 Int.Pls (0::bit) f1 = f1 ==> |
|
361 f3 Int.Min (1::bit) f2 = f2 ==> f (w BIT b) = f3 w b (f w)" |
|
362 by (cases b, simp add: bin_rec_Bit0, simp add: bin_rec_Bit1) |
|
363 |
|
364 lemmas bin_rec_simps = refl [THEN bin_rec_Bit] bin_rec_Pls bin_rec_Min |
|
365 bin_rec_Bit0 bin_rec_Bit1 |
|
366 |
|
367 |
|
368 subsection {* Truncating binary integers *} |
|
369 |
|
370 definition |
|
371 bin_sign_def [code del] : "bin_sign = bin_rec Int.Pls Int.Min (%w b s. s)" |
|
372 |
|
373 lemma bin_sign_simps [simp]: |
|
374 "bin_sign Int.Pls = Int.Pls" |
|
375 "bin_sign Int.Min = Int.Min" |
|
376 "bin_sign (Int.Bit0 w) = bin_sign w" |
|
377 "bin_sign (Int.Bit1 w) = bin_sign w" |
|
378 "bin_sign (w BIT b) = bin_sign w" |
|
379 unfolding bin_sign_def by (auto simp: bin_rec_simps) |
|
380 |
|
381 declare bin_sign_simps(1-4) [code] |
|
382 |
|
383 lemma bin_sign_rest [simp]: |
|
384 "bin_sign (bin_rest w) = (bin_sign w)" |
|
385 by (cases w rule: bin_exhaust) auto |
|
386 |
|
387 consts |
|
388 bintrunc :: "nat => int => int" |
|
389 primrec |
|
390 Z : "bintrunc 0 bin = Int.Pls" |
|
391 Suc : "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT (bin_last bin)" |
|
392 |
|
393 consts |
|
394 sbintrunc :: "nat => int => int" |
|
395 primrec |
|
396 Z : "sbintrunc 0 bin = |
|
397 (case bin_last bin of (1::bit) => Int.Min | (0::bit) => Int.Pls)" |
|
398 Suc : "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)" |
|
399 |
|
400 lemma sign_bintr: |
|
401 "!!w. bin_sign (bintrunc n w) = Int.Pls" |
|
402 by (induct n) auto |
|
403 |
|
404 lemma bintrunc_mod2p: |
|
405 "!!w. bintrunc n w = (w mod 2 ^ n :: int)" |
|
406 apply (induct n, clarsimp) |
|
407 apply (simp add: bin_last_mod bin_rest_div Bit_def zmod_zmult2_eq |
|
408 cong: number_of_False_cong) |
|
409 done |
|
410 |
|
411 lemma sbintrunc_mod2p: |
|
412 "!!w. sbintrunc n w = ((w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n :: int)" |
|
413 apply (induct n) |
|
414 apply clarsimp |
|
415 apply (subst mod_add_left_eq) |
|
416 apply (simp add: bin_last_mod) |
|
417 apply (simp add: number_of_eq) |
|
418 apply clarsimp |
|
419 apply (simp add: bin_last_mod bin_rest_div Bit_def |
|
420 cong: number_of_False_cong) |
|
421 apply (clarsimp simp: mod_mult_mult1 [symmetric] |
|
422 zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]]) |
|
423 apply (rule trans [symmetric, OF _ emep1]) |
|
424 apply auto |
|
425 apply (auto simp: even_def) |
|
426 done |
|
427 |
|
428 subsection "Simplifications for (s)bintrunc" |
|
429 |
|
430 lemma bit_bool: |
|
431 "(b = (b' = (1::bit))) = (b' = (if b then (1::bit) else (0::bit)))" |
|
432 by (cases b') auto |
|
433 |
|
434 lemmas bit_bool1 [simp] = refl [THEN bit_bool [THEN iffD1], symmetric] |
|
435 |
|
436 lemma bin_sign_lem: |
|
437 "!!bin. (bin_sign (sbintrunc n bin) = Int.Min) = bin_nth bin n" |
|
438 apply (induct n) |
|
439 apply (case_tac bin rule: bin_exhaust, case_tac b, auto)+ |
|
440 done |
|
441 |
|
442 lemma nth_bintr: |
|
443 "!!w m. bin_nth (bintrunc m w) n = (n < m & bin_nth w n)" |
|
444 apply (induct n) |
|
445 apply (case_tac m, auto)[1] |
|
446 apply (case_tac m, auto)[1] |
|
447 done |
|
448 |
|
449 lemma nth_sbintr: |
|
450 "!!w m. bin_nth (sbintrunc m w) n = |
|
451 (if n < m then bin_nth w n else bin_nth w m)" |
|
452 apply (induct n) |
|
453 apply (case_tac m, simp_all split: bit.splits)[1] |
|
454 apply (case_tac m, simp_all split: bit.splits)[1] |
|
455 done |
|
456 |
|
457 lemma bin_nth_Bit: |
|
458 "bin_nth (w BIT b) n = (n = 0 & b = (1::bit) | (EX m. n = Suc m & bin_nth w m))" |
|
459 by (cases n) auto |
|
460 |
|
461 lemma bin_nth_Bit0: |
|
462 "bin_nth (Int.Bit0 w) n = (EX m. n = Suc m & bin_nth w m)" |
|
463 using bin_nth_Bit [where b="(0::bit)"] by simp |
|
464 |
|
465 lemma bin_nth_Bit1: |
|
466 "bin_nth (Int.Bit1 w) n = (n = 0 | (EX m. n = Suc m & bin_nth w m))" |
|
467 using bin_nth_Bit [where b="(1::bit)"] by simp |
|
468 |
|
469 lemma bintrunc_bintrunc_l: |
|
470 "n <= m ==> (bintrunc m (bintrunc n w) = bintrunc n w)" |
|
471 by (rule bin_eqI) (auto simp add : nth_bintr) |
|
472 |
|
473 lemma sbintrunc_sbintrunc_l: |
|
474 "n <= m ==> (sbintrunc m (sbintrunc n w) = sbintrunc n w)" |
|
475 by (rule bin_eqI) (auto simp: nth_sbintr) |
|
476 |
|
477 lemma bintrunc_bintrunc_ge: |
|
478 "n <= m ==> (bintrunc n (bintrunc m w) = bintrunc n w)" |
|
479 by (rule bin_eqI) (auto simp: nth_bintr) |
|
480 |
|
481 lemma bintrunc_bintrunc_min [simp]: |
|
482 "bintrunc m (bintrunc n w) = bintrunc (min m n) w" |
|
483 apply (rule bin_eqI) |
|
484 apply (auto simp: nth_bintr) |
|
485 done |
|
486 |
|
487 lemma sbintrunc_sbintrunc_min [simp]: |
|
488 "sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w" |
|
489 apply (rule bin_eqI) |
|
490 apply (auto simp: nth_sbintr min_max.inf_absorb1 min_max.inf_absorb2) |
|
491 done |
|
492 |
|
493 lemmas bintrunc_Pls = |
|
494 bintrunc.Suc [where bin="Int.Pls", simplified bin_last_simps bin_rest_simps, standard] |
|
495 |
|
496 lemmas bintrunc_Min [simp] = |
|
497 bintrunc.Suc [where bin="Int.Min", simplified bin_last_simps bin_rest_simps, standard] |
|
498 |
|
499 lemmas bintrunc_BIT [simp] = |
|
500 bintrunc.Suc [where bin="w BIT b", simplified bin_last_simps bin_rest_simps, standard] |
|
501 |
|
502 lemma bintrunc_Bit0 [simp]: |
|
503 "bintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (bintrunc n w)" |
|
504 using bintrunc_BIT [where b="(0::bit)"] by simp |
|
505 |
|
506 lemma bintrunc_Bit1 [simp]: |
|
507 "bintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (bintrunc n w)" |
|
508 using bintrunc_BIT [where b="(1::bit)"] by simp |
|
509 |
|
510 lemmas bintrunc_Sucs = bintrunc_Pls bintrunc_Min bintrunc_BIT |
|
511 bintrunc_Bit0 bintrunc_Bit1 |
|
512 |
|
513 lemmas sbintrunc_Suc_Pls = |
|
514 sbintrunc.Suc [where bin="Int.Pls", simplified bin_last_simps bin_rest_simps, standard] |
|
515 |
|
516 lemmas sbintrunc_Suc_Min = |
|
517 sbintrunc.Suc [where bin="Int.Min", simplified bin_last_simps bin_rest_simps, standard] |
|
518 |
|
519 lemmas sbintrunc_Suc_BIT [simp] = |
|
520 sbintrunc.Suc [where bin="w BIT b", simplified bin_last_simps bin_rest_simps, standard] |
|
521 |
|
522 lemma sbintrunc_Suc_Bit0 [simp]: |
|
523 "sbintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (sbintrunc n w)" |
|
524 using sbintrunc_Suc_BIT [where b="(0::bit)"] by simp |
|
525 |
|
526 lemma sbintrunc_Suc_Bit1 [simp]: |
|
527 "sbintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (sbintrunc n w)" |
|
528 using sbintrunc_Suc_BIT [where b="(1::bit)"] by simp |
|
529 |
|
530 lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min sbintrunc_Suc_BIT |
|
531 sbintrunc_Suc_Bit0 sbintrunc_Suc_Bit1 |
|
532 |
|
533 lemmas sbintrunc_Pls = |
|
534 sbintrunc.Z [where bin="Int.Pls", |
|
535 simplified bin_last_simps bin_rest_simps bit.simps, standard] |
|
536 |
|
537 lemmas sbintrunc_Min = |
|
538 sbintrunc.Z [where bin="Int.Min", |
|
539 simplified bin_last_simps bin_rest_simps bit.simps, standard] |
|
540 |
|
541 lemmas sbintrunc_0_BIT_B0 [simp] = |
|
542 sbintrunc.Z [where bin="w BIT (0::bit)", |
|
543 simplified bin_last_simps bin_rest_simps bit.simps, standard] |
|
544 |
|
545 lemmas sbintrunc_0_BIT_B1 [simp] = |
|
546 sbintrunc.Z [where bin="w BIT (1::bit)", |
|
547 simplified bin_last_simps bin_rest_simps bit.simps, standard] |
|
548 |
|
549 lemma sbintrunc_0_Bit0 [simp]: "sbintrunc 0 (Int.Bit0 w) = Int.Pls" |
|
550 using sbintrunc_0_BIT_B0 by simp |
|
551 |
|
552 lemma sbintrunc_0_Bit1 [simp]: "sbintrunc 0 (Int.Bit1 w) = Int.Min" |
|
553 using sbintrunc_0_BIT_B1 by simp |
|
554 |
|
555 lemmas sbintrunc_0_simps = |
|
556 sbintrunc_Pls sbintrunc_Min sbintrunc_0_BIT_B0 sbintrunc_0_BIT_B1 |
|
557 sbintrunc_0_Bit0 sbintrunc_0_Bit1 |
|
558 |
|
559 lemmas bintrunc_simps = bintrunc.Z bintrunc_Sucs |
|
560 lemmas sbintrunc_simps = sbintrunc_0_simps sbintrunc_Sucs |
|
561 |
|
562 lemma bintrunc_minus: |
|
563 "0 < n ==> bintrunc (Suc (n - 1)) w = bintrunc n w" |
|
564 by auto |
|
565 |
|
566 lemma sbintrunc_minus: |
|
567 "0 < n ==> sbintrunc (Suc (n - 1)) w = sbintrunc n w" |
|
568 by auto |
|
569 |
|
570 lemmas bintrunc_minus_simps = |
|
571 bintrunc_Sucs [THEN [2] bintrunc_minus [symmetric, THEN trans], standard] |
|
572 lemmas sbintrunc_minus_simps = |
|
573 sbintrunc_Sucs [THEN [2] sbintrunc_minus [symmetric, THEN trans], standard] |
|
574 |
|
575 lemma bintrunc_n_Pls [simp]: |
|
576 "bintrunc n Int.Pls = Int.Pls" |
|
577 by (induct n) auto |
|
578 |
|
579 lemma sbintrunc_n_PM [simp]: |
|
580 "sbintrunc n Int.Pls = Int.Pls" |
|
581 "sbintrunc n Int.Min = Int.Min" |
|
582 by (induct n) auto |
|
583 |
|
584 lemmas thobini1 = arg_cong [where f = "%w. w BIT b", standard] |
|
585 |
|
586 lemmas bintrunc_BIT_I = trans [OF bintrunc_BIT thobini1] |
|
587 lemmas bintrunc_Min_I = trans [OF bintrunc_Min thobini1] |
|
588 |
|
589 lemmas bmsts = bintrunc_minus_simps(1-3) [THEN thobini1 [THEN [2] trans], standard] |
|
590 lemmas bintrunc_Pls_minus_I = bmsts(1) |
|
591 lemmas bintrunc_Min_minus_I = bmsts(2) |
|
592 lemmas bintrunc_BIT_minus_I = bmsts(3) |
|
593 |
|
594 lemma bintrunc_0_Min: "bintrunc 0 Int.Min = Int.Pls" |
|
595 by auto |
|
596 lemma bintrunc_0_BIT: "bintrunc 0 (w BIT b) = Int.Pls" |
|
597 by auto |
|
598 |
|
599 lemma bintrunc_Suc_lem: |
|
600 "bintrunc (Suc n) x = y ==> m = Suc n ==> bintrunc m x = y" |
|
601 by auto |
|
602 |
|
603 lemmas bintrunc_Suc_Ialts = |
|
604 bintrunc_Min_I [THEN bintrunc_Suc_lem, standard] |
|
605 bintrunc_BIT_I [THEN bintrunc_Suc_lem, standard] |
|
606 |
|
607 lemmas sbintrunc_BIT_I = trans [OF sbintrunc_Suc_BIT thobini1] |
|
608 |
|
609 lemmas sbintrunc_Suc_Is = |
|
610 sbintrunc_Sucs(1-3) [THEN thobini1 [THEN [2] trans], standard] |
|
611 |
|
612 lemmas sbintrunc_Suc_minus_Is = |
|
613 sbintrunc_minus_simps(1-3) [THEN thobini1 [THEN [2] trans], standard] |
|
614 |
|
615 lemma sbintrunc_Suc_lem: |
|
616 "sbintrunc (Suc n) x = y ==> m = Suc n ==> sbintrunc m x = y" |
|
617 by auto |
|
618 |
|
619 lemmas sbintrunc_Suc_Ialts = |
|
620 sbintrunc_Suc_Is [THEN sbintrunc_Suc_lem, standard] |
|
621 |
|
622 lemma sbintrunc_bintrunc_lt: |
|
623 "m > n ==> sbintrunc n (bintrunc m w) = sbintrunc n w" |
|
624 by (rule bin_eqI) (auto simp: nth_sbintr nth_bintr) |
|
625 |
|
626 lemma bintrunc_sbintrunc_le: |
|
627 "m <= Suc n ==> bintrunc m (sbintrunc n w) = bintrunc m w" |
|
628 apply (rule bin_eqI) |
|
629 apply (auto simp: nth_sbintr nth_bintr) |
|
630 apply (subgoal_tac "x=n", safe, arith+)[1] |
|
631 apply (subgoal_tac "x=n", safe, arith+)[1] |
|
632 done |
|
633 |
|
634 lemmas bintrunc_sbintrunc [simp] = order_refl [THEN bintrunc_sbintrunc_le] |
|
635 lemmas sbintrunc_bintrunc [simp] = lessI [THEN sbintrunc_bintrunc_lt] |
|
636 lemmas bintrunc_bintrunc [simp] = order_refl [THEN bintrunc_bintrunc_l] |
|
637 lemmas sbintrunc_sbintrunc [simp] = order_refl [THEN sbintrunc_sbintrunc_l] |
|
638 |
|
639 lemma bintrunc_sbintrunc' [simp]: |
|
640 "0 < n \<Longrightarrow> bintrunc n (sbintrunc (n - 1) w) = bintrunc n w" |
|
641 by (cases n) (auto simp del: bintrunc.Suc) |
|
642 |
|
643 lemma sbintrunc_bintrunc' [simp]: |
|
644 "0 < n \<Longrightarrow> sbintrunc (n - 1) (bintrunc n w) = sbintrunc (n - 1) w" |
|
645 by (cases n) (auto simp del: bintrunc.Suc) |
|
646 |
|
647 lemma bin_sbin_eq_iff: |
|
648 "bintrunc (Suc n) x = bintrunc (Suc n) y <-> |
|
649 sbintrunc n x = sbintrunc n y" |
|
650 apply (rule iffI) |
|
651 apply (rule box_equals [OF _ sbintrunc_bintrunc sbintrunc_bintrunc]) |
|
652 apply simp |
|
653 apply (rule box_equals [OF _ bintrunc_sbintrunc bintrunc_sbintrunc]) |
|
654 apply simp |
|
655 done |
|
656 |
|
657 lemma bin_sbin_eq_iff': |
|
658 "0 < n \<Longrightarrow> bintrunc n x = bintrunc n y <-> |
|
659 sbintrunc (n - 1) x = sbintrunc (n - 1) y" |
|
660 by (cases n) (simp_all add: bin_sbin_eq_iff del: bintrunc.Suc) |
|
661 |
|
662 lemmas bintrunc_sbintruncS0 [simp] = bintrunc_sbintrunc' [unfolded One_nat_def] |
|
663 lemmas sbintrunc_bintruncS0 [simp] = sbintrunc_bintrunc' [unfolded One_nat_def] |
|
664 |
|
665 lemmas bintrunc_bintrunc_l' = le_add1 [THEN bintrunc_bintrunc_l] |
|
666 lemmas sbintrunc_sbintrunc_l' = le_add1 [THEN sbintrunc_sbintrunc_l] |
|
667 |
|
668 (* although bintrunc_minus_simps, if added to default simpset, |
|
669 tends to get applied where it's not wanted in developing the theories, |
|
670 we get a version for when the word length is given literally *) |
|
671 |
|
672 lemmas nat_non0_gr = |
|
673 trans [OF iszero_def [THEN Not_eq_iff [THEN iffD2]] refl, standard] |
|
674 |
|
675 lemmas bintrunc_pred_simps [simp] = |
|
676 bintrunc_minus_simps [of "number_of bin", simplified nobm1, standard] |
|
677 |
|
678 lemmas sbintrunc_pred_simps [simp] = |
|
679 sbintrunc_minus_simps [of "number_of bin", simplified nobm1, standard] |
|
680 |
|
681 lemma no_bintr_alt: |
|
682 "number_of (bintrunc n w) = w mod 2 ^ n" |
|
683 by (simp add: number_of_eq bintrunc_mod2p) |
|
684 |
|
685 lemma no_bintr_alt1: "bintrunc n = (%w. w mod 2 ^ n :: int)" |
|
686 by (rule ext) (rule bintrunc_mod2p) |
|
687 |
|
688 lemma range_bintrunc: "range (bintrunc n) = {i. 0 <= i & i < 2 ^ n}" |
|
689 apply (unfold no_bintr_alt1) |
|
690 apply (auto simp add: image_iff) |
|
691 apply (rule exI) |
|
692 apply (auto intro: int_mod_lem [THEN iffD1, symmetric]) |
|
693 done |
|
694 |
|
695 lemma no_bintr: |
|
696 "number_of (bintrunc n w) = (number_of w mod 2 ^ n :: int)" |
|
697 by (simp add : bintrunc_mod2p number_of_eq) |
|
698 |
|
699 lemma no_sbintr_alt2: |
|
700 "sbintrunc n = (%w. (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n :: int)" |
|
701 by (rule ext) (simp add : sbintrunc_mod2p) |
|
702 |
|
703 lemma no_sbintr: |
|
704 "number_of (sbintrunc n w) = |
|
705 ((number_of w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n :: int)" |
|
706 by (simp add : no_sbintr_alt2 number_of_eq) |
|
707 |
|
708 lemma range_sbintrunc: |
|
709 "range (sbintrunc n) = {i. - (2 ^ n) <= i & i < 2 ^ n}" |
|
710 apply (unfold no_sbintr_alt2) |
|
711 apply (auto simp add: image_iff eq_diff_eq) |
|
712 apply (rule exI) |
|
713 apply (auto intro: int_mod_lem [THEN iffD1, symmetric]) |
|
714 done |
|
715 |
|
716 lemma sb_inc_lem: |
|
717 "(a::int) + 2^k < 0 \<Longrightarrow> a + 2^k + 2^(Suc k) <= (a + 2^k) mod 2^(Suc k)" |
|
718 apply (erule int_mod_ge' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k", simplified zless2p]) |
|
719 apply (rule TrueI) |
|
720 done |
|
721 |
|
722 lemma sb_inc_lem': |
|
723 "(a::int) < - (2^k) \<Longrightarrow> a + 2^k + 2^(Suc k) <= (a + 2^k) mod 2^(Suc k)" |
|
724 by (rule sb_inc_lem) simp |
|
725 |
|
726 lemma sbintrunc_inc: |
|
727 "x < - (2^n) ==> x + 2^(Suc n) <= sbintrunc n x" |
|
728 unfolding no_sbintr_alt2 by (drule sb_inc_lem') simp |
|
729 |
|
730 lemma sb_dec_lem: |
|
731 "(0::int) <= - (2^k) + a ==> (a + 2^k) mod (2 * 2 ^ k) <= - (2 ^ k) + a" |
|
732 by (rule int_mod_le' [where n = "2 ^ (Suc k)" and b = "a + 2 ^ k", |
|
733 simplified zless2p, OF _ TrueI, simplified]) |
|
734 |
|
735 lemma sb_dec_lem': |
|
736 "(2::int) ^ k <= a ==> (a + 2 ^ k) mod (2 * 2 ^ k) <= - (2 ^ k) + a" |
|
737 by (rule iffD1 [OF diff_le_eq', THEN sb_dec_lem, simplified]) |
|
738 |
|
739 lemma sbintrunc_dec: |
|
740 "x >= (2 ^ n) ==> x - 2 ^ (Suc n) >= sbintrunc n x" |
|
741 unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp |
|
742 |
|
743 lemmas zmod_uminus' = zmod_uminus [where b="c", standard] |
|
744 lemmas zpower_zmod' = zpower_zmod [where m="c" and y="k", standard] |
|
745 |
|
746 lemmas brdmod1s' [symmetric] = |
|
747 mod_add_left_eq mod_add_right_eq |
|
748 zmod_zsub_left_eq zmod_zsub_right_eq |
|
749 zmod_zmult1_eq zmod_zmult1_eq_rev |
|
750 |
|
751 lemmas brdmods' [symmetric] = |
|
752 zpower_zmod' [symmetric] |
|
753 trans [OF mod_add_left_eq mod_add_right_eq] |
|
754 trans [OF zmod_zsub_left_eq zmod_zsub_right_eq] |
|
755 trans [OF zmod_zmult1_eq zmod_zmult1_eq_rev] |
|
756 zmod_uminus' [symmetric] |
|
757 mod_add_left_eq [where b = "1::int"] |
|
758 zmod_zsub_left_eq [where b = "1"] |
|
759 |
|
760 lemmas bintr_arith1s = |
|
761 brdmod1s' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p, standard] |
|
762 lemmas bintr_ariths = |
|
763 brdmods' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p, standard] |
|
764 |
|
765 lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p, standard] |
|
766 |
|
767 lemma bintr_ge0: "(0 :: int) <= number_of (bintrunc n w)" |
|
768 by (simp add : no_bintr m2pths) |
|
769 |
|
770 lemma bintr_lt2p: "number_of (bintrunc n w) < (2 ^ n :: int)" |
|
771 by (simp add : no_bintr m2pths) |
|
772 |
|
773 lemma bintr_Min: |
|
774 "number_of (bintrunc n Int.Min) = (2 ^ n :: int) - 1" |
|
775 by (simp add : no_bintr m1mod2k) |
|
776 |
|
777 lemma sbintr_ge: "(- (2 ^ n) :: int) <= number_of (sbintrunc n w)" |
|
778 by (simp add : no_sbintr m2pths) |
|
779 |
|
780 lemma sbintr_lt: "number_of (sbintrunc n w) < (2 ^ n :: int)" |
|
781 by (simp add : no_sbintr m2pths) |
|
782 |
|
783 lemma bintrunc_Suc: |
|
784 "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT bin_last bin" |
|
785 by (case_tac bin rule: bin_exhaust) auto |
|
786 |
|
787 lemma sign_Pls_ge_0: |
|
788 "(bin_sign bin = Int.Pls) = (number_of bin >= (0 :: int))" |
|
789 by (induct bin rule: numeral_induct) auto |
|
790 |
|
791 lemma sign_Min_lt_0: |
|
792 "(bin_sign bin = Int.Min) = (number_of bin < (0 :: int))" |
|
793 by (induct bin rule: numeral_induct) auto |
|
794 |
|
795 lemmas sign_Min_neg = trans [OF sign_Min_lt_0 neg_def [symmetric]] |
|
796 |
|
797 lemma bin_rest_trunc: |
|
798 "!!bin. (bin_rest (bintrunc n bin)) = bintrunc (n - 1) (bin_rest bin)" |
|
799 by (induct n) auto |
|
800 |
|
801 lemma bin_rest_power_trunc [rule_format] : |
|
802 "(bin_rest ^^ k) (bintrunc n bin) = |
|
803 bintrunc (n - k) ((bin_rest ^^ k) bin)" |
|
804 by (induct k) (auto simp: bin_rest_trunc) |
|
805 |
|
806 lemma bin_rest_trunc_i: |
|
807 "bintrunc n (bin_rest bin) = bin_rest (bintrunc (Suc n) bin)" |
|
808 by auto |
|
809 |
|
810 lemma bin_rest_strunc: |
|
811 "!!bin. bin_rest (sbintrunc (Suc n) bin) = sbintrunc n (bin_rest bin)" |
|
812 by (induct n) auto |
|
813 |
|
814 lemma bintrunc_rest [simp]: |
|
815 "!!bin. bintrunc n (bin_rest (bintrunc n bin)) = bin_rest (bintrunc n bin)" |
|
816 apply (induct n, simp) |
|
817 apply (case_tac bin rule: bin_exhaust) |
|
818 apply (auto simp: bintrunc_bintrunc_l) |
|
819 done |
|
820 |
|
821 lemma sbintrunc_rest [simp]: |
|
822 "!!bin. sbintrunc n (bin_rest (sbintrunc n bin)) = bin_rest (sbintrunc n bin)" |
|
823 apply (induct n, simp) |
|
824 apply (case_tac bin rule: bin_exhaust) |
|
825 apply (auto simp: bintrunc_bintrunc_l split: bit.splits) |
|
826 done |
|
827 |
|
828 lemma bintrunc_rest': |
|
829 "bintrunc n o bin_rest o bintrunc n = bin_rest o bintrunc n" |
|
830 by (rule ext) auto |
|
831 |
|
832 lemma sbintrunc_rest' : |
|
833 "sbintrunc n o bin_rest o sbintrunc n = bin_rest o sbintrunc n" |
|
834 by (rule ext) auto |
|
835 |
|
836 lemma rco_lem: |
|
837 "f o g o f = g o f ==> f o (g o f) ^^ n = g ^^ n o f" |
|
838 apply (rule ext) |
|
839 apply (induct_tac n) |
|
840 apply (simp_all (no_asm)) |
|
841 apply (drule fun_cong) |
|
842 apply (unfold o_def) |
|
843 apply (erule trans) |
|
844 apply simp |
|
845 done |
|
846 |
|
847 lemma rco_alt: "(f o g) ^^ n o f = f o (g o f) ^^ n" |
|
848 apply (rule ext) |
|
849 apply (induct n) |
|
850 apply (simp_all add: o_def) |
|
851 done |
|
852 |
|
853 lemmas rco_bintr = bintrunc_rest' |
|
854 [THEN rco_lem [THEN fun_cong], unfolded o_def] |
|
855 lemmas rco_sbintr = sbintrunc_rest' |
|
856 [THEN rco_lem [THEN fun_cong], unfolded o_def] |
|
857 |
|
858 subsection {* Splitting and concatenation *} |
|
859 |
|
860 primrec bin_split :: "nat \<Rightarrow> int \<Rightarrow> int \<times> int" where |
|
861 Z: "bin_split 0 w = (w, Int.Pls)" |
|
862 | Suc: "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w) |
|
863 in (w1, w2 BIT bin_last w))" |
|
864 |
|
865 primrec bin_cat :: "int \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int" where |
|
866 Z: "bin_cat w 0 v = w" |
|
867 | Suc: "bin_cat w (Suc n) v = bin_cat w n (bin_rest v) BIT bin_last v" |
|
868 |
|
869 subsection {* Miscellaneous lemmas *} |
|
870 |
|
871 lemma funpow_minus_simp: |
|
872 "0 < n \<Longrightarrow> f ^^ n = f \<circ> f ^^ (n - 1)" |
|
873 by (cases n) simp_all |
|
874 |
|
875 lemmas funpow_pred_simp [simp] = |
|
876 funpow_minus_simp [of "number_of bin", simplified nobm1, standard] |
|
877 |
|
878 lemmas replicate_minus_simp = |
|
879 trans [OF gen_minus [where f = "%n. replicate n x"] replicate.replicate_Suc, |
|
880 standard] |
|
881 |
|
882 lemmas replicate_pred_simp [simp] = |
|
883 replicate_minus_simp [of "number_of bin", simplified nobm1, standard] |
|
884 |
|
885 lemmas power_Suc_no [simp] = power_Suc [of "number_of a", standard] |
|
886 |
|
887 lemmas power_minus_simp = |
|
888 trans [OF gen_minus [where f = "power f"] power_Suc, standard] |
|
889 |
|
890 lemmas power_pred_simp = |
|
891 power_minus_simp [of "number_of bin", simplified nobm1, standard] |
|
892 lemmas power_pred_simp_no [simp] = power_pred_simp [where f= "number_of f", standard] |
|
893 |
|
894 lemma list_exhaust_size_gt0: |
|
895 assumes y: "\<And>a list. y = a # list \<Longrightarrow> P" |
|
896 shows "0 < length y \<Longrightarrow> P" |
|
897 apply (cases y, simp) |
|
898 apply (rule y) |
|
899 apply fastsimp |
|
900 done |
|
901 |
|
902 lemma list_exhaust_size_eq0: |
|
903 assumes y: "y = [] \<Longrightarrow> P" |
|
904 shows "length y = 0 \<Longrightarrow> P" |
|
905 apply (cases y) |
|
906 apply (rule y, simp) |
|
907 apply simp |
|
908 done |
|
909 |
|
910 lemma size_Cons_lem_eq: |
|
911 "y = xa # list ==> size y = Suc k ==> size list = k" |
|
912 by auto |
|
913 |
|
914 lemma size_Cons_lem_eq_bin: |
|
915 "y = xa # list ==> size y = number_of (Int.succ k) ==> |
|
916 size list = number_of k" |
|
917 by (auto simp: pred_def succ_def split add : split_if_asm) |
|
918 |
|
919 lemmas ls_splits = |
|
920 prod.split split_split prod.split_asm split_split_asm split_if_asm |
|
921 |
|
922 lemma not_B1_is_B0: "y \<noteq> (1::bit) \<Longrightarrow> y = (0::bit)" |
|
923 by (cases y) auto |
|
924 |
|
925 lemma B1_ass_B0: |
|
926 assumes y: "y = (0::bit) \<Longrightarrow> y = (1::bit)" |
|
927 shows "y = (1::bit)" |
|
928 apply (rule classical) |
|
929 apply (drule not_B1_is_B0) |
|
930 apply (erule y) |
|
931 done |
|
932 |
|
933 -- "simplifications for specific word lengths" |
|
934 lemmas n2s_ths [THEN eq_reflection] = add_2_eq_Suc add_2_eq_Suc' |
|
935 |
|
936 lemmas s2n_ths = n2s_ths [symmetric] |
|
937 |
|
938 end |