1 (* |
1 (* Title: HOL/Word/Bits_Int.thy |
2 Author: Jeremy Dawson and Gerwin Klein, NICTA |
2 Author: Jeremy Dawson and Gerwin Klein, NICTA |
3 |
3 |
4 Definitions and basic theorems for bit-wise logical operations |
4 Definitions and basic theorems for bit-wise logical operations |
5 for integers expressed using Pls, Min, BIT, |
5 for integers expressed using Pls, Min, BIT, |
6 and converting them to and from lists of bools. |
6 and converting them to and from lists of bools. |
7 *) |
7 *) |
8 |
8 |
9 section \<open>Bitwise Operations on Binary Integers\<close> |
9 section \<open>Bitwise Operations on Binary Integers\<close> |
10 |
10 |
11 theory Bits_Int |
11 theory Bits_Int |
12 imports Bits Bit_Representation |
12 imports Bits Bit_Representation |
13 begin |
13 begin |
14 |
14 |
15 subsection \<open>Logical operations\<close> |
15 subsection \<open>Logical operations\<close> |
16 |
16 |
17 text "bit-wise logical operations on the int type" |
17 text "bit-wise logical operations on the int type" |
18 |
18 |
19 instantiation int :: bit |
19 instantiation int :: bit |
20 begin |
20 begin |
21 |
21 |
22 definition int_not_def: |
22 definition int_not_def: "bitNOT = (\<lambda>x::int. - x - 1)" |
23 "bitNOT = (\<lambda>x::int. - x - 1)" |
23 |
24 |
24 function bitAND_int |
25 function bitAND_int where |
25 where "bitAND_int x y = |
26 "bitAND_int x y = |
26 (if x = 0 then 0 else if x = -1 then y |
27 (if x = 0 then 0 else if x = -1 then y else |
27 else (bin_rest x AND bin_rest y) BIT (bin_last x \<and> bin_last y))" |
28 (bin_rest x AND bin_rest y) BIT (bin_last x \<and> bin_last y))" |
|
29 by pat_completeness simp |
28 by pat_completeness simp |
30 |
29 |
31 termination |
30 termination |
32 by (relation "measure (nat o abs o fst)", simp_all add: bin_rest_def) |
31 by (relation "measure (nat \<circ> abs \<circ> fst)", simp_all add: bin_rest_def) |
33 |
32 |
34 declare bitAND_int.simps [simp del] |
33 declare bitAND_int.simps [simp del] |
35 |
34 |
36 definition int_or_def: |
35 definition int_or_def: |
37 "bitOR = (\<lambda>x y::int. NOT (NOT x AND NOT y))" |
36 "bitOR = (\<lambda>x y::int. NOT (NOT x AND NOT y))" |
65 by (simp add: bitAND_int.simps) |
64 by (simp add: bitAND_int.simps) |
66 |
65 |
67 lemma int_and_m1 [simp]: "(-1::int) AND x = x" |
66 lemma int_and_m1 [simp]: "(-1::int) AND x = x" |
68 by (simp add: bitAND_int.simps) |
67 by (simp add: bitAND_int.simps) |
69 |
68 |
70 lemma int_and_Bits [simp]: |
69 lemma int_and_Bits [simp]: |
71 "(x BIT b) AND (y BIT c) = (x AND y) BIT (b \<and> c)" |
70 "(x BIT b) AND (y BIT c) = (x AND y) BIT (b \<and> c)" |
72 by (subst bitAND_int.simps, simp add: Bit_eq_0_iff Bit_eq_m1_iff) |
71 by (subst bitAND_int.simps, simp add: Bit_eq_0_iff Bit_eq_m1_iff) |
73 |
72 |
74 lemma int_or_zero [simp]: "(0::int) OR x = x" |
73 lemma int_or_zero [simp]: "(0::int) OR x = x" |
75 unfolding int_or_def by simp |
74 unfolding int_or_def by simp |
76 |
75 |
77 lemma int_or_minus1 [simp]: "(-1::int) OR x = -1" |
76 lemma int_or_minus1 [simp]: "(-1::int) OR x = -1" |
78 unfolding int_or_def by simp |
77 unfolding int_or_def by simp |
79 |
78 |
80 lemma int_or_Bits [simp]: |
79 lemma int_or_Bits [simp]: |
81 "(x BIT b) OR (y BIT c) = (x OR y) BIT (b \<or> c)" |
80 "(x BIT b) OR (y BIT c) = (x OR y) BIT (b \<or> c)" |
82 unfolding int_or_def by simp |
81 unfolding int_or_def by simp |
83 |
82 |
84 lemma int_xor_zero [simp]: "(0::int) XOR x = x" |
83 lemma int_xor_zero [simp]: "(0::int) XOR x = x" |
85 unfolding int_xor_def by simp |
84 unfolding int_xor_def by simp |
86 |
85 |
87 lemma int_xor_Bits [simp]: |
86 lemma int_xor_Bits [simp]: |
88 "(x BIT b) XOR (y BIT c) = (x XOR y) BIT ((b \<or> c) \<and> \<not> (b \<and> c))" |
87 "(x BIT b) XOR (y BIT c) = (x XOR y) BIT ((b \<or> c) \<and> \<not> (b \<and> c))" |
89 unfolding int_xor_def by auto |
88 unfolding int_xor_def by auto |
90 |
89 |
91 subsubsection \<open>Binary destructors\<close> |
90 subsubsection \<open>Binary destructors\<close> |
92 |
91 |
113 |
112 |
114 lemma bin_last_XOR [simp]: "bin_last (x XOR y) \<longleftrightarrow> (bin_last x \<or> bin_last y) \<and> \<not> (bin_last x \<and> bin_last y)" |
113 lemma bin_last_XOR [simp]: "bin_last (x XOR y) \<longleftrightarrow> (bin_last x \<or> bin_last y) \<and> \<not> (bin_last x \<and> bin_last y)" |
115 by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp) |
114 by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp) |
116 |
115 |
117 lemma bin_nth_ops: |
116 lemma bin_nth_ops: |
118 "!!x y. bin_nth (x AND y) n = (bin_nth x n & bin_nth y n)" |
117 "!!x y. bin_nth (x AND y) n = (bin_nth x n & bin_nth y n)" |
119 "!!x y. bin_nth (x OR y) n = (bin_nth x n | bin_nth y n)" |
118 "!!x y. bin_nth (x OR y) n = (bin_nth x n | bin_nth y n)" |
120 "!!x y. bin_nth (x XOR y) n = (bin_nth x n ~= bin_nth y n)" |
119 "!!x y. bin_nth (x XOR y) n = (bin_nth x n ~= bin_nth y n)" |
121 "!!x. bin_nth (NOT x) n = (~ bin_nth x n)" |
120 "!!x. bin_nth (NOT x) n = (~ bin_nth x n)" |
122 by (induct n) auto |
121 by (induct n) auto |
123 |
122 |
124 subsubsection \<open>Derived properties\<close> |
123 subsubsection \<open>Derived properties\<close> |
125 |
124 |
148 int_or_comm: "!!y::int. x OR y = y OR x" and |
147 int_or_comm: "!!y::int. x OR y = y OR x" and |
149 int_xor_comm: "!!y::int. x XOR y = y XOR x" |
148 int_xor_comm: "!!y::int. x XOR y = y XOR x" |
150 by (auto simp add: bin_eq_iff bin_nth_ops) |
149 by (auto simp add: bin_eq_iff bin_nth_ops) |
151 |
150 |
152 lemma bin_ops_same [simp]: |
151 lemma bin_ops_same [simp]: |
153 "(x::int) AND x = x" |
152 "(x::int) AND x = x" |
154 "(x::int) OR x = x" |
153 "(x::int) OR x = x" |
155 "(x::int) XOR x = 0" |
154 "(x::int) XOR x = 0" |
156 by (auto simp add: bin_eq_iff bin_nth_ops) |
155 by (auto simp add: bin_eq_iff bin_nth_ops) |
157 |
156 |
158 lemmas bin_log_esimps = |
157 lemmas bin_log_esimps = |
159 int_and_extra_simps int_or_extra_simps int_xor_extra_simps |
158 int_and_extra_simps int_or_extra_simps int_xor_extra_simps |
160 int_and_0 int_and_m1 int_or_zero int_or_minus1 int_xor_zero int_xor_minus1 |
159 int_and_0 int_and_m1 int_or_zero int_or_minus1 int_xor_zero int_xor_minus1 |
161 |
160 |
162 (* basic properties of logical (bit-wise) operations *) |
161 (* basic properties of logical (bit-wise) operations *) |
163 |
162 |
164 lemma bbw_ao_absorb: |
163 lemma bbw_ao_absorb: |
165 "!!y::int. x AND (y OR x) = x & x OR (y AND x) = x" |
164 "!!y::int. x AND (y OR x) = x & x OR (y AND x) = x" |
166 by (auto simp add: bin_eq_iff bin_nth_ops) |
165 by (auto simp add: bin_eq_iff bin_nth_ops) |
167 |
166 |
168 lemma bbw_ao_absorbs_other: |
167 lemma bbw_ao_absorbs_other: |
169 "x AND (x OR y) = x \<and> (y AND x) OR x = (x::int)" |
168 "x AND (x OR y) = x \<and> (y AND x) OR x = (x::int)" |
191 by (auto simp add: bin_eq_iff bin_nth_ops) |
190 by (auto simp add: bin_eq_iff bin_nth_ops) |
192 |
191 |
193 lemmas bbw_assocs = int_and_assoc int_or_assoc int_xor_assoc |
192 lemmas bbw_assocs = int_and_assoc int_or_assoc int_xor_assoc |
194 |
193 |
195 (* BH: Why are these declared as simp rules??? *) |
194 (* BH: Why are these declared as simp rules??? *) |
196 lemma bbw_lcs [simp]: |
195 lemma bbw_lcs [simp]: |
197 "(y::int) AND (x AND z) = x AND (y AND z)" |
196 "(y::int) AND (x AND z) = x AND (y AND z)" |
198 "(y::int) OR (x OR z) = x OR (y OR z)" |
197 "(y::int) OR (x OR z) = x OR (y OR z)" |
199 "(y::int) XOR (x XOR z) = x XOR (y XOR z)" |
198 "(y::int) XOR (x XOR z) = x XOR (y XOR z)" |
200 by (auto simp add: bin_eq_iff bin_nth_ops) |
199 by (auto simp add: bin_eq_iff bin_nth_ops) |
201 |
200 |
202 lemma bbw_not_dist: |
201 lemma bbw_not_dist: |
203 "!!y::int. NOT (x OR y) = (NOT x) AND (NOT y)" |
202 "!!y::int. NOT (x OR y) = (NOT x) AND (NOT y)" |
204 "!!y::int. NOT (x AND y) = (NOT x) OR (NOT y)" |
203 "!!y::int. NOT (x AND y) = (NOT x) OR (NOT y)" |
205 by (auto simp add: bin_eq_iff bin_nth_ops) |
204 by (auto simp add: bin_eq_iff bin_nth_ops) |
206 |
205 |
207 lemma bbw_oa_dist: |
206 lemma bbw_oa_dist: |
208 "!!y z::int. (x AND y) OR z = |
207 "!!y z::int. (x AND y) OR z = |
209 (x OR z) AND (y OR z)" |
208 (x OR z) AND (y OR z)" |
210 by (auto simp add: bin_eq_iff bin_nth_ops) |
209 by (auto simp add: bin_eq_iff bin_nth_ops) |
211 |
210 |
212 lemma bbw_ao_dist: |
211 lemma bbw_ao_dist: |
213 "!!y z::int. (x OR y) AND z = |
212 "!!y z::int. (x OR y) AND z = |
214 (x AND z) OR (y AND z)" |
213 (x AND z) OR (y AND z)" |
215 by (auto simp add: bin_eq_iff bin_nth_ops) |
214 by (auto simp add: bin_eq_iff bin_nth_ops) |
216 |
215 |
217 (* |
216 (* |
218 Why were these declared simp??? |
217 Why were these declared simp??? |
219 declare bin_ops_comm [simp] bbw_assocs [simp] |
218 declare bin_ops_comm [simp] bbw_assocs [simp] |
220 *) |
219 *) |
221 |
220 |
222 subsubsection \<open>Simplification with numerals\<close> |
221 subsubsection \<open>Simplification with numerals\<close> |
223 |
222 |
224 text \<open>Cases for \<open>0\<close> and \<open>-1\<close> are already covered by |
223 text \<open>Cases for \<open>0\<close> and \<open>-1\<close> are already covered by |
358 apply (case_tac bit, auto) |
357 apply (case_tac bit, auto) |
359 done |
358 done |
360 |
359 |
361 subsubsection \<open>Truncating results of bit-wise operations\<close> |
360 subsubsection \<open>Truncating results of bit-wise operations\<close> |
362 |
361 |
363 lemma bin_trunc_ao: |
362 lemma bin_trunc_ao: |
364 "!!x y. (bintrunc n x) AND (bintrunc n y) = bintrunc n (x AND y)" |
363 "!!x y. (bintrunc n x) AND (bintrunc n y) = bintrunc n (x AND y)" |
365 "!!x y. (bintrunc n x) OR (bintrunc n y) = bintrunc n (x OR y)" |
364 "!!x y. (bintrunc n x) OR (bintrunc n y) = bintrunc n (x OR y)" |
366 by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr) |
365 by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr) |
367 |
366 |
368 lemma bin_trunc_xor: |
367 lemma bin_trunc_xor: |
369 "!!x y. bintrunc n (bintrunc n x XOR bintrunc n y) = |
368 "!!x y. bintrunc n (bintrunc n x XOR bintrunc n y) = |
370 bintrunc n (x XOR y)" |
369 bintrunc n (x XOR y)" |
371 by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr) |
370 by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr) |
372 |
371 |
373 lemma bin_trunc_not: |
372 lemma bin_trunc_not: |
374 "!!x. bintrunc n (NOT (bintrunc n x)) = bintrunc n (NOT x)" |
373 "!!x. bintrunc n (NOT (bintrunc n x)) = bintrunc n (NOT x)" |
375 by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr) |
374 by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr) |
376 |
375 |
377 (* want theorems of the form of bin_trunc_xor *) |
376 (* want theorems of the form of bin_trunc_xor *) |
378 lemma bintr_bintr_i: |
377 lemma bintr_bintr_i: |
390 bin_sc :: "nat => bool => int => int" |
389 bin_sc :: "nat => bool => int => int" |
391 where |
390 where |
392 Z: "bin_sc 0 b w = bin_rest w BIT b" |
391 Z: "bin_sc 0 b w = bin_rest w BIT b" |
393 | Suc: "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w" |
392 | Suc: "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w" |
394 |
393 |
395 lemma bin_nth_sc [simp]: |
394 lemma bin_nth_sc [simp]: |
396 "bin_nth (bin_sc n b w) n \<longleftrightarrow> b" |
395 "bin_nth (bin_sc n b w) n \<longleftrightarrow> b" |
397 by (induct n arbitrary: w) auto |
396 by (induct n arbitrary: w) auto |
398 |
397 |
399 lemma bin_sc_sc_same [simp]: |
398 lemma bin_sc_sc_same [simp]: |
400 "bin_sc n c (bin_sc n b w) = bin_sc n c w" |
399 "bin_sc n c (bin_sc n b w) = bin_sc n c w" |
401 by (induct n arbitrary: w) auto |
400 by (induct n arbitrary: w) auto |
402 |
401 |
403 lemma bin_sc_sc_diff: |
402 lemma bin_sc_sc_diff: |
404 "m ~= n ==> |
403 "m ~= n ==> |
405 bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)" |
404 bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)" |
406 apply (induct n arbitrary: w m) |
405 apply (induct n arbitrary: w m) |
407 apply (case_tac [!] m) |
406 apply (case_tac [!] m) |
408 apply auto |
407 apply auto |
409 done |
408 done |
410 |
409 |
411 lemma bin_nth_sc_gen: |
410 lemma bin_nth_sc_gen: |
412 "bin_nth (bin_sc n b w) m = (if m = n then b else bin_nth w m)" |
411 "bin_nth (bin_sc n b w) m = (if m = n then b else bin_nth w m)" |
413 by (induct n arbitrary: w m) (case_tac [!] m, auto) |
412 by (induct n arbitrary: w m) (case_tac [!] m, auto) |
414 |
413 |
415 lemma bin_sc_nth [simp]: |
414 lemma bin_sc_nth [simp]: |
416 "(bin_sc n (bin_nth w n) w) = w" |
415 "(bin_sc n (bin_nth w n) w) = w" |
417 by (induct n arbitrary: w) auto |
416 by (induct n arbitrary: w) auto |
418 |
417 |
419 lemma bin_sign_sc [simp]: |
418 lemma bin_sign_sc [simp]: |
420 "bin_sign (bin_sc n b w) = bin_sign w" |
419 "bin_sign (bin_sc n b w) = bin_sign w" |
421 by (induct n arbitrary: w) auto |
420 by (induct n arbitrary: w) auto |
422 |
421 |
423 lemma bin_sc_bintr [simp]: |
422 lemma bin_sc_bintr [simp]: |
424 "bintrunc m (bin_sc n x (bintrunc m (w))) = bintrunc m (bin_sc n x w)" |
423 "bintrunc m (bin_sc n x (bintrunc m (w))) = bintrunc m (bin_sc n x w)" |
425 apply (induct n arbitrary: w m) |
424 apply (induct n arbitrary: w m) |
426 apply (case_tac [!] w rule: bin_exhaust) |
425 apply (case_tac [!] w rule: bin_exhaust) |
427 apply (case_tac [!] m, auto) |
426 apply (case_tac [!] m, auto) |
428 done |
427 done |
462 lemma bin_sc_FP [simp]: "bin_sc n False 0 = 0" |
461 lemma bin_sc_FP [simp]: "bin_sc n False 0 = 0" |
463 by (induct n) auto |
462 by (induct n) auto |
464 |
463 |
465 lemma bin_sc_TM [simp]: "bin_sc n True (- 1) = - 1" |
464 lemma bin_sc_TM [simp]: "bin_sc n True (- 1) = - 1" |
466 by (induct n) auto |
465 by (induct n) auto |
467 |
466 |
468 lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP |
467 lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP |
469 |
468 |
470 lemma bin_sc_minus: |
469 lemma bin_sc_minus: |
471 "0 < n ==> bin_sc (Suc (n - 1)) b w = bin_sc n b w" |
470 "0 < n ==> bin_sc (Suc (n - 1)) b w = bin_sc n b w" |
472 by auto |
471 by auto |
473 |
472 |
474 lemmas bin_sc_Suc_minus = |
473 lemmas bin_sc_Suc_minus = |
475 trans [OF bin_sc_minus [symmetric] bin_sc.Suc] |
474 trans [OF bin_sc_minus [symmetric] bin_sc.Suc] |
476 |
475 |
477 lemma bin_sc_numeral [simp]: |
476 lemma bin_sc_numeral [simp]: |
478 "bin_sc (numeral k) b w = |
477 "bin_sc (numeral k) b w = |
479 bin_sc (pred_numeral k) b (bin_rest w) BIT bin_last w" |
478 bin_sc (pred_numeral k) b (bin_rest w) BIT bin_last w" |
488 |
487 |
489 fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" |
488 fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" |
490 where |
489 where |
491 "bin_rsplit_aux n m c bs = |
490 "bin_rsplit_aux n m c bs = |
492 (if m = 0 | n = 0 then bs else |
491 (if m = 0 | n = 0 then bs else |
493 let (a, b) = bin_split n c |
492 let (a, b) = bin_split n c |
494 in bin_rsplit_aux n (m - n) a (b # bs))" |
493 in bin_rsplit_aux n (m - n) a (b # bs))" |
495 |
494 |
496 definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" |
495 definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" |
497 where |
496 where |
498 "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []" |
497 "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []" |
499 |
498 |
500 fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" |
499 fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" |
501 where |
500 where |
502 "bin_rsplitl_aux n m c bs = |
501 "bin_rsplitl_aux n m c bs = |
503 (if m = 0 | n = 0 then bs else |
502 (if m = 0 | n = 0 then bs else |
504 let (a, b) = bin_split (min m n) c |
503 let (a, b) = bin_split (min m n) c |
505 in bin_rsplitl_aux n (m - n) a (b # bs))" |
504 in bin_rsplitl_aux n (m - n) a (b # bs))" |
506 |
505 |
507 definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" |
506 definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" |
508 where |
507 where |
509 "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []" |
508 "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []" |
510 |
509 |
511 declare bin_rsplit_aux.simps [simp del] |
510 declare bin_rsplit_aux.simps [simp del] |
512 declare bin_rsplitl_aux.simps [simp del] |
511 declare bin_rsplitl_aux.simps [simp del] |
513 |
512 |
514 lemma bin_sign_cat: |
513 lemma bin_sign_cat: |
515 "bin_sign (bin_cat x n y) = bin_sign x" |
514 "bin_sign (bin_cat x n y) = bin_sign x" |
516 by (induct n arbitrary: y) auto |
515 by (induct n arbitrary: y) auto |
517 |
516 |
518 lemma bin_cat_Suc_Bit: |
517 lemma bin_cat_Suc_Bit: |
519 "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b" |
518 "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b" |
520 by auto |
519 by auto |
521 |
520 |
522 lemma bin_nth_cat: |
521 lemma bin_nth_cat: |
523 "bin_nth (bin_cat x k y) n = |
522 "bin_nth (bin_cat x k y) n = |
524 (if n < k then bin_nth y n else bin_nth x (n - k))" |
523 (if n < k then bin_nth y n else bin_nth x (n - k))" |
525 apply (induct k arbitrary: n y) |
524 apply (induct k arbitrary: n y) |
526 apply clarsimp |
525 apply clarsimp |
527 apply (case_tac n, auto) |
526 apply (case_tac n, auto) |
528 done |
527 done |
529 |
528 |
530 lemma bin_nth_split: |
529 lemma bin_nth_split: |
531 "bin_split n c = (a, b) ==> |
530 "bin_split n c = (a, b) ==> |
532 (ALL k. bin_nth a k = bin_nth c (n + k)) & |
531 (ALL k. bin_nth a k = bin_nth c (n + k)) & |
533 (ALL k. bin_nth b k = (k < n & bin_nth c k))" |
532 (ALL k. bin_nth b k = (k < n & bin_nth c k))" |
534 apply (induct n arbitrary: b c) |
533 apply (induct n arbitrary: b c) |
535 apply clarsimp |
534 apply clarsimp |
536 apply (clarsimp simp: Let_def split: prod.split_asm) |
535 apply (clarsimp simp: Let_def split: prod.split_asm) |
537 apply (case_tac k) |
536 apply (case_tac k) |
538 apply auto |
537 apply auto |
539 done |
538 done |
540 |
539 |
541 lemma bin_cat_assoc: |
540 lemma bin_cat_assoc: |
542 "bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)" |
541 "bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)" |
543 by (induct n arbitrary: z) auto |
542 by (induct n arbitrary: z) auto |
544 |
543 |
545 lemma bin_cat_assoc_sym: |
544 lemma bin_cat_assoc_sym: |
546 "bin_cat x m (bin_cat y n z) = bin_cat (bin_cat x (m - n) y) (min m n) z" |
545 "bin_cat x m (bin_cat y n z) = bin_cat (bin_cat x (m - n) y) (min m n) z" |
547 apply (induct n arbitrary: z m, clarsimp) |
546 apply (induct n arbitrary: z m, clarsimp) |
549 done |
548 done |
550 |
549 |
551 lemma bin_cat_zero [simp]: "bin_cat 0 n w = bintrunc n w" |
550 lemma bin_cat_zero [simp]: "bin_cat 0 n w = bintrunc n w" |
552 by (induct n arbitrary: w) auto |
551 by (induct n arbitrary: w) auto |
553 |
552 |
554 lemma bintr_cat1: |
553 lemma bintr_cat1: |
555 "bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b" |
554 "bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b" |
556 by (induct n arbitrary: b) auto |
555 by (induct n arbitrary: b) auto |
557 |
556 |
558 lemma bintr_cat: "bintrunc m (bin_cat a n b) = |
557 lemma bintr_cat: "bintrunc m (bin_cat a n b) = |
559 bin_cat (bintrunc (m - n) a) n (bintrunc (min m n) b)" |
558 bin_cat (bintrunc (m - n) a) n (bintrunc (min m n) b)" |
560 by (rule bin_eqI) (auto simp: bin_nth_cat nth_bintr) |
559 by (rule bin_eqI) (auto simp: bin_nth_cat nth_bintr) |
561 |
560 |
562 lemma bintr_cat_same [simp]: |
561 lemma bintr_cat_same [simp]: |
563 "bintrunc n (bin_cat a n b) = bintrunc n b" |
562 "bintrunc n (bin_cat a n b) = bintrunc n b" |
564 by (auto simp add : bintr_cat) |
563 by (auto simp add : bintr_cat) |
565 |
564 |
566 lemma cat_bintr [simp]: |
565 lemma cat_bintr [simp]: |
567 "bin_cat a n (bintrunc n b) = bin_cat a n b" |
566 "bin_cat a n (bintrunc n b) = bin_cat a n b" |
568 by (induct n arbitrary: b) auto |
567 by (induct n arbitrary: b) auto |
569 |
568 |
570 lemma split_bintrunc: |
569 lemma split_bintrunc: |
571 "bin_split n c = (a, b) ==> b = bintrunc n c" |
570 "bin_split n c = (a, b) ==> b = bintrunc n c" |
572 by (induct n arbitrary: b c) (auto simp: Let_def split: prod.split_asm) |
571 by (induct n arbitrary: b c) (auto simp: Let_def split: prod.split_asm) |
573 |
572 |
574 lemma bin_cat_split: |
573 lemma bin_cat_split: |
575 "bin_split n w = (u, v) ==> w = bin_cat u n v" |
574 "bin_split n w = (u, v) ==> w = bin_cat u n v" |
585 lemma bin_split_minus1 [simp]: |
584 lemma bin_split_minus1 [simp]: |
586 "bin_split n (- 1) = (- 1, bintrunc n (- 1))" |
585 "bin_split n (- 1) = (- 1, bintrunc n (- 1))" |
587 by (induct n) auto |
586 by (induct n) auto |
588 |
587 |
589 lemma bin_split_trunc: |
588 lemma bin_split_trunc: |
590 "bin_split (min m n) c = (a, b) ==> |
589 "bin_split (min m n) c = (a, b) ==> |
591 bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)" |
590 bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)" |
592 apply (induct n arbitrary: m b c, clarsimp) |
591 apply (induct n arbitrary: m b c, clarsimp) |
593 apply (simp add: bin_rest_trunc Let_def split: prod.split_asm) |
592 apply (simp add: bin_rest_trunc Let_def split: prod.split_asm) |
594 apply (case_tac m) |
593 apply (case_tac m) |
595 apply (auto simp: Let_def split: prod.split_asm) |
594 apply (auto simp: Let_def split: prod.split_asm) |
596 done |
595 done |
597 |
596 |
598 lemma bin_split_trunc1: |
597 lemma bin_split_trunc1: |
599 "bin_split n c = (a, b) ==> |
598 "bin_split n c = (a, b) ==> |
600 bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)" |
599 bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)" |
601 apply (induct n arbitrary: m b c, clarsimp) |
600 apply (induct n arbitrary: m b c, clarsimp) |
602 apply (simp add: bin_rest_trunc Let_def split: prod.split_asm) |
601 apply (simp add: bin_rest_trunc Let_def split: prod.split_asm) |
603 apply (case_tac m) |
602 apply (case_tac m) |
604 apply (auto simp: Let_def split: prod.split_asm) |
603 apply (auto simp: Let_def split: prod.split_asm) |