redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
2 Author: Jeremy Dawson, NICTA
4 Theorems to do with integers, expressed using Pls, Min, BIT,
5 theorems linking them to lists of booleans, and repeated splitting
9 header "Bool lists and integers"
11 theory Bool_List_Representation
15 subsection {* Operations on lists of booleans *}
17 primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int" where
18 Nil: "bl_to_bin_aux [] w = w"
19 | Cons: "bl_to_bin_aux (b # bs) w =
20 bl_to_bin_aux bs (w BIT (if b then 1 else 0))"
22 definition bl_to_bin :: "bool list \<Rightarrow> int" where
23 bl_to_bin_def: "bl_to_bin bs = bl_to_bin_aux bs 0"
25 primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list" where
26 Z: "bin_to_bl_aux 0 w bl = bl"
27 | Suc: "bin_to_bl_aux (Suc n) w bl =
28 bin_to_bl_aux n (bin_rest w) ((bin_last w = 1) # bl)"
30 definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list" where
31 bin_to_bl_def : "bin_to_bl n w = bin_to_bl_aux n w []"
33 primrec bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool list" where
34 Suc: "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
35 | Z: "bl_of_nth 0 f = []"
37 primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
38 Z: "takefill fill 0 xs = []"
39 | Suc: "takefill fill (Suc n) xs = (
40 case xs of [] => fill # takefill fill n xs
41 | y # ys => y # takefill fill n ys)"
43 definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where
44 "map2 f as bs = map (split f) (zip as bs)"
46 lemma map2_Nil [simp]: "map2 f [] ys = []"
47 unfolding map2_def by auto
49 lemma map2_Nil2 [simp]: "map2 f xs [] = []"
50 unfolding map2_def by auto
52 lemma map2_Cons [simp]:
53 "map2 f (x # xs) (y # ys) = f x y # map2 f xs ys"
54 unfolding map2_def by auto
57 subsection "Arithmetic in terms of bool lists"
60 Arithmetic operations in terms of the reversed bool list,
61 assuming input list(s) the same length, and don't extend them.
64 primrec rbl_succ :: "bool list => bool list" where
65 Nil: "rbl_succ Nil = Nil"
66 | Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)"
68 primrec rbl_pred :: "bool list => bool list" where
69 Nil: "rbl_pred Nil = Nil"
70 | Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)"
72 primrec rbl_add :: "bool list => bool list => bool list" where
73 -- "result is length of first arg, second arg may be longer"
74 Nil: "rbl_add Nil x = Nil"
75 | Cons: "rbl_add (y # ys) x = (let ws = rbl_add ys (tl x) in
76 (y ~= hd x) # (if hd x & y then rbl_succ ws else ws))"
78 primrec rbl_mult :: "bool list => bool list => bool list" where
79 -- "result is length of first arg, second arg may be longer"
80 Nil: "rbl_mult Nil x = Nil"
81 | Cons: "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in
82 if y then rbl_add ws x else ws)"
85 "(butlast ^^ n) bl = take (length bl - n) bl"
86 by (induct n) (auto simp: butlast_take)
88 lemma bin_to_bl_aux_zero_minus_simp [simp]:
89 "0 < n \<Longrightarrow> bin_to_bl_aux n 0 bl =
90 bin_to_bl_aux (n - 1) 0 (False # bl)"
93 lemma bin_to_bl_aux_Pls_minus_simp [simp]:
94 "0 < n ==> bin_to_bl_aux n Int.Pls bl =
95 bin_to_bl_aux (n - 1) Int.Pls (False # bl)"
98 lemma bin_to_bl_aux_Min_minus_simp [simp]:
99 "0 < n ==> bin_to_bl_aux n Int.Min bl =
100 bin_to_bl_aux (n - 1) Int.Min (True # bl)"
103 lemma bin_to_bl_aux_Bit_minus_simp [simp]:
104 "0 < n ==> bin_to_bl_aux n (w BIT b) bl =
105 bin_to_bl_aux (n - 1) w ((b = 1) # bl)"
108 lemma bin_to_bl_aux_Bit0_minus_simp [simp]:
109 "0 < n ==> bin_to_bl_aux n (Int.Bit0 w) bl =
110 bin_to_bl_aux (n - 1) w (False # bl)"
113 lemma bin_to_bl_aux_Bit1_minus_simp [simp]:
114 "0 < n ==> bin_to_bl_aux n (Int.Bit1 w) bl =
115 bin_to_bl_aux (n - 1) w (True # bl)"
118 text {* Link between bin and bool list. *}
120 lemma bl_to_bin_aux_append:
121 "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)"
122 by (induct bs arbitrary: w) auto
124 lemma bin_to_bl_aux_append:
125 "bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)"
126 by (induct n arbitrary: w bs) auto
128 lemma bl_to_bin_append:
129 "bl_to_bin (bs @ cs) = bl_to_bin_aux cs (bl_to_bin bs)"
130 unfolding bl_to_bin_def by (rule bl_to_bin_aux_append)
132 lemma bin_to_bl_aux_alt:
133 "bin_to_bl_aux n w bs = bin_to_bl n w @ bs"
134 unfolding bin_to_bl_def by (simp add : bin_to_bl_aux_append)
136 lemma bin_to_bl_0 [simp]: "bin_to_bl 0 bs = []"
137 unfolding bin_to_bl_def by auto
139 lemma size_bin_to_bl_aux:
140 "size (bin_to_bl_aux n w bs) = n + length bs"
141 by (induct n arbitrary: w bs) auto
143 lemma size_bin_to_bl [simp]: "size (bin_to_bl n w) = n"
144 unfolding bin_to_bl_def by (simp add : size_bin_to_bl_aux)
147 "bl_to_bin (bin_to_bl_aux n w bs) =
148 bl_to_bin_aux bs (bintrunc n w)"
149 by (induct n arbitrary: w bs) (auto simp add : bl_to_bin_def)
151 lemma bin_bl_bin [simp]: "bl_to_bin (bin_to_bl n w) = bintrunc n w"
152 unfolding bin_to_bl_def bin_bl_bin' by auto
155 "bin_to_bl (n + length bs) (bl_to_bin_aux bs w) =
156 bin_to_bl_aux n w bs"
157 apply (induct bs arbitrary: w n)
159 apply (simp_all only : add_Suc [symmetric])
160 apply (auto simp add : bin_to_bl_def)
163 lemma bl_bin_bl [simp]: "bin_to_bl (length bs) (bl_to_bin bs) = bs"
164 unfolding bl_to_bin_def
165 apply (rule box_equals)
166 apply (rule bl_bin_bl')
168 apply (rule bin_to_bl_aux.Z)
173 "bl_to_bin bs = bl_to_bin cs ==> length bs = length cs ==> bs = cs"
174 apply (rule_tac box_equals)
176 apply (rule bl_bin_bl)
177 apply (rule bl_bin_bl)
181 lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl"
182 unfolding bl_to_bin_def by auto
184 lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = 0"
185 unfolding bl_to_bin_def by auto
187 lemma bin_to_bl_zero_aux:
188 "bin_to_bl_aux n 0 bl = replicate n False @ bl"
189 by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
191 lemma bin_to_bl_Pls_aux:
192 "bin_to_bl_aux n Int.Pls bl = replicate n False @ bl"
193 by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
195 lemma bin_to_bl_Pls: "bin_to_bl n Int.Pls = replicate n False"
196 unfolding bin_to_bl_def by (simp add : bin_to_bl_Pls_aux)
198 lemma bin_to_bl_Min_aux:
199 "bin_to_bl_aux n Int.Min bl = replicate n True @ bl"
200 by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
202 lemma bin_to_bl_Min: "bin_to_bl n Int.Min = replicate n True"
203 unfolding bin_to_bl_def by (simp add : bin_to_bl_Min_aux)
205 lemma bl_to_bin_rep_F:
206 "bl_to_bin (replicate n False @ bl) = bl_to_bin bl"
207 apply (simp add: bin_to_bl_zero_aux [symmetric] bin_bl_bin')
208 apply (simp add: bl_to_bin_def)
211 lemma bin_to_bl_trunc [simp]:
212 "n <= m ==> bin_to_bl n (bintrunc m w) = bin_to_bl n w"
213 by (auto intro: bl_to_bin_inj)
215 lemma bin_to_bl_aux_bintr:
216 "bin_to_bl_aux n (bintrunc m bin) bl =
217 replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl"
218 apply (induct n arbitrary: m bin bl)
222 apply (clarsimp simp: bin_to_bl_zero_aux)
223 apply (erule thin_rl)
228 lemma bin_to_bl_bintr:
229 "bin_to_bl n (bintrunc m bin) =
230 replicate (n - m) False @ bin_to_bl (min n m) bin"
231 unfolding bin_to_bl_def by (rule bin_to_bl_aux_bintr)
233 lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = 0"
236 lemma len_bin_to_bl_aux:
237 "length (bin_to_bl_aux n w bs) = n + length bs"
238 by (induct n arbitrary: w bs) auto
240 lemma len_bin_to_bl [simp]: "length (bin_to_bl n w) = n"
241 unfolding bin_to_bl_def len_bin_to_bl_aux by auto
244 "bin_sign (bl_to_bin_aux bs w) = bin_sign w"
245 by (induct bs arbitrary: w) auto
247 lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = 0"
248 unfolding bl_to_bin_def by (simp add : sign_bl_bin')
250 lemma bl_sbin_sign_aux:
251 "hd (bin_to_bl_aux (Suc n) w bs) =
252 (bin_sign (sbintrunc n w) = -1)"
253 apply (induct n arbitrary: w bs)
255 apply (cases w rule: bin_exhaust)
256 apply (simp split add : bit.split)
261 "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)"
262 unfolding bin_to_bl_def by (rule bl_sbin_sign_aux)
264 lemma bin_nth_of_bl_aux:
265 "bin_nth (bl_to_bin_aux bl w) n =
266 (n < size bl & rev bl ! n | n >= length bl & bin_nth w (n - size bl))"
267 apply (induct bl arbitrary: w)
270 apply (cut_tac x=n and y="size bl" in linorder_less_linear)
271 apply (erule disjE, simp add: nth_append)+
275 lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl & rev bl ! n)"
276 unfolding bl_to_bin_def by (simp add : bin_nth_of_bl_aux)
278 lemma bin_nth_bl: "n < m \<Longrightarrow> bin_nth w n = nth (rev (bin_to_bl m w)) n"
279 apply (induct n arbitrary: m w)
281 apply (case_tac m, clarsimp)
282 apply (clarsimp simp: bin_to_bl_def)
283 apply (simp add: bin_to_bl_aux_alt)
285 apply (case_tac m, clarsimp)
286 apply (clarsimp simp: bin_to_bl_def)
287 apply (simp add: bin_to_bl_aux_alt)
291 "n < length xs \<Longrightarrow> rev xs ! n = xs ! (length xs - 1 - n)"
294 apply (clarsimp simp add : nth_append nth.simps split add : nat.split)
295 apply (rule_tac f = "\<lambda>n. xs ! n" in arg_cong)
299 lemma nth_rev_alt: "n < length ys \<Longrightarrow> ys ! n = rev ys ! (length ys - Suc n)"
300 by (simp add: nth_rev)
302 lemma nth_bin_to_bl_aux:
303 "n < m + length bl \<Longrightarrow> (bin_to_bl_aux m w bl) ! n =
304 (if n < m then bin_nth w (m - 1 - n) else bl ! (n - m))"
305 apply (induct m arbitrary: w n bl)
308 apply (case_tac w rule: bin_exhaust)
312 lemma nth_bin_to_bl: "n < m ==> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)"
313 unfolding bin_to_bl_def by (simp add : nth_bin_to_bl_aux)
315 lemma bl_to_bin_lt2p_aux:
316 "bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)"
317 apply (induct bs arbitrary: w)
321 apply (drule meta_spec, erule xtr8 [rotated],
322 simp add: numeral_simps algebra_simps BIT_simps
323 cong add: number_of_False_cong)+
326 lemma bl_to_bin_lt2p: "bl_to_bin bs < (2 ^ length bs)"
327 apply (unfold bl_to_bin_def)
330 apply (rule bl_to_bin_lt2p_aux)
334 lemma bl_to_bin_ge2p_aux:
335 "bl_to_bin_aux bs w >= w * (2 ^ length bs)"
336 apply (induct bs arbitrary: w)
340 apply (drule meta_spec, erule preorder_class.order_trans [rotated],
341 simp add: numeral_simps algebra_simps BIT_simps
342 cong add: number_of_False_cong)+
345 lemma bl_to_bin_ge0: "bl_to_bin bs >= 0"
346 apply (unfold bl_to_bin_def)
348 apply (rule bl_to_bin_ge2p_aux)
349 apply (simp add: Pls_def)
352 lemma butlast_rest_bin:
353 "butlast (bin_to_bl n w) = bin_to_bl (n - 1) (bin_rest w)"
354 apply (unfold bin_to_bl_def)
355 apply (cases w rule: bin_exhaust)
356 apply (cases n, clarsimp)
358 apply (auto simp add: bin_to_bl_aux_alt)
361 lemma butlast_bin_rest:
362 "butlast bl = bin_to_bl (length bl - Suc 0) (bin_rest (bl_to_bin bl))"
363 using butlast_rest_bin [where w="bl_to_bin bl" and n="length bl"] by simp
365 lemma butlast_rest_bl2bin_aux:
366 "bl ~= [] \<Longrightarrow>
367 bl_to_bin_aux (butlast bl) w = bin_rest (bl_to_bin_aux bl w)"
368 by (induct bl arbitrary: w) auto
370 lemma butlast_rest_bl2bin:
371 "bl_to_bin (butlast bl) = bin_rest (bl_to_bin bl)"
372 apply (unfold bl_to_bin_def)
374 apply (auto simp add: butlast_rest_bl2bin_aux)
377 lemma trunc_bl2bin_aux:
378 "bintrunc m (bl_to_bin_aux bl w) =
379 bl_to_bin_aux (drop (length bl - m) bl) (bintrunc (m - length bl) w)"
380 apply (induct bl arbitrary: w)
384 apply (case_tac "m - size bl")
385 apply (simp add : diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
386 apply (simp add: BIT_simps)
387 apply (rule_tac f = "%nat. bl_to_bin_aux bl (Int.Bit1 (bintrunc nat w))"
390 apply (case_tac "m - size bl")
391 apply (simp add: diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
392 apply (simp add: BIT_simps)
393 apply (rule_tac f = "%nat. bl_to_bin_aux bl (Int.Bit0 (bintrunc nat w))"
399 "bintrunc m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)"
400 unfolding bl_to_bin_def by (simp add : trunc_bl2bin_aux)
402 lemma trunc_bl2bin_len [simp]:
403 "bintrunc (length bl) (bl_to_bin bl) = bl_to_bin bl"
404 by (simp add: trunc_bl2bin)
407 "bl_to_bin (drop k bl) = bintrunc (length bl - k) (bl_to_bin bl)"
410 apply (rule trunc_bl2bin [symmetric])
411 apply (cases "k <= length bl")
415 lemma nth_rest_power_bin:
416 "bin_nth ((bin_rest ^^ k) w) n = bin_nth w (n + k)"
417 apply (induct k arbitrary: n, clarsimp)
419 apply (simp only: bin_nth.Suc [symmetric] add_Suc)
422 lemma take_rest_power_bin:
423 "m <= n ==> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest ^^ (n - m)) w)"
424 apply (rule nth_equalityI)
426 apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin)
429 lemma hd_butlast: "size xs > 1 ==> hd (butlast xs) = hd xs"
432 lemma last_bin_last':
433 "size xs > 0 \<Longrightarrow> last xs = (bin_last (bl_to_bin_aux xs w) = 1)"
434 by (induct xs arbitrary: w) auto
437 "size xs > 0 ==> last xs = (bin_last (bl_to_bin xs) = 1)"
438 unfolding bl_to_bin_def by (erule last_bin_last')
441 "bin_last w = (if last (bin_to_bl (Suc n) w) then 1 else 0)"
442 apply (unfold bin_to_bl_def)
444 apply (auto simp add: bin_to_bl_aux_alt)
447 (** links between bit-wise operations and operations on bool lists **)
449 lemma bl_xor_aux_bin:
450 "map2 (%x y. x ~= y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
451 bin_to_bl_aux n (v XOR w) (map2 (%x y. x ~= y) bs cs)"
452 apply (induct n arbitrary: v w bs cs)
454 apply (case_tac v rule: bin_exhaust)
455 apply (case_tac w rule: bin_exhaust)
458 apply (case_tac ba, safe, simp_all)+
462 "map2 (op | ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
463 bin_to_bl_aux n (v OR w) (map2 (op | ) bs cs)"
464 apply (induct n arbitrary: v w bs cs)
466 apply (case_tac v rule: bin_exhaust)
467 apply (case_tac w rule: bin_exhaust)
470 apply (case_tac ba, safe, simp_all)+
473 lemma bl_and_aux_bin:
474 "map2 (op & ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) =
475 bin_to_bl_aux n (v AND w) (map2 (op & ) bs cs)"
476 apply (induct n arbitrary: v w bs cs)
478 apply (case_tac v rule: bin_exhaust)
479 apply (case_tac w rule: bin_exhaust)
483 lemma bl_not_aux_bin:
484 "map Not (bin_to_bl_aux n w cs) =
485 bin_to_bl_aux n (NOT w) (map Not cs)"
486 apply (induct n arbitrary: w cs)
491 lemma bl_not_bin: "map Not (bin_to_bl n w) = bin_to_bl n (NOT w)"
492 unfolding bin_to_bl_def by (simp add: bl_not_aux_bin)
495 "map2 (op \<and>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)"
496 unfolding bin_to_bl_def by (simp add: bl_and_aux_bin)
499 "map2 (op \<or>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)"
500 unfolding bin_to_bl_def by (simp add: bl_or_aux_bin)
503 "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)"
504 unfolding bin_to_bl_def by (simp only: bl_xor_aux_bin map2_Nil)
506 lemma drop_bin2bl_aux:
507 "drop m (bin_to_bl_aux n bin bs) =
508 bin_to_bl_aux (n - m) bin (drop (m - n) bs)"
509 apply (induct n arbitrary: m bin bs, clarsimp)
511 apply (case_tac bin rule: bin_exhaust)
512 apply (case_tac "m <= n", simp)
513 apply (case_tac "m - n", simp)
515 apply (rule_tac f = "%nat. drop nat bs" in arg_cong)
519 lemma drop_bin2bl: "drop m (bin_to_bl n bin) = bin_to_bl (n - m) bin"
520 unfolding bin_to_bl_def by (simp add : drop_bin2bl_aux)
522 lemma take_bin2bl_lem1:
523 "take m (bin_to_bl_aux m w bs) = bin_to_bl m w"
524 apply (induct m arbitrary: w bs, clarsimp)
526 apply (simp add: bin_to_bl_aux_alt)
527 apply (simp add: bin_to_bl_def)
528 apply (simp add: bin_to_bl_aux_alt)
531 lemma take_bin2bl_lem:
532 "take m (bin_to_bl_aux (m + n) w bs) =
533 take m (bin_to_bl (m + n) w)"
534 apply (induct n arbitrary: w bs)
535 apply (simp_all (no_asm) add: bin_to_bl_def take_bin2bl_lem1)
539 lemma bin_split_take:
540 "bin_split n c = (a, b) \<Longrightarrow>
541 bin_to_bl m a = take m (bin_to_bl (m + n) c)"
542 apply (induct n arbitrary: b c)
544 apply (clarsimp simp: Let_def split: ls_splits)
545 apply (simp add: bin_to_bl_def)
546 apply (simp add: take_bin2bl_lem)
549 lemma bin_split_take1:
550 "k = m + n ==> bin_split n c = (a, b) ==>
551 bin_to_bl m a = take m (bin_to_bl k c)"
552 by (auto elim: bin_split_take)
554 lemma nth_takefill: "m < n \<Longrightarrow>
555 takefill fill n l ! m = (if m < length l then l ! m else fill)"
556 apply (induct n arbitrary: m l, clarsimp)
559 apply (simp split: list.split)
560 apply (simp split: list.split)
564 "takefill fill n l = take n l @ replicate (n - length l) fill"
565 by (induct n arbitrary: l) (auto split: list.split)
567 lemma takefill_replicate [simp]:
568 "takefill fill n (replicate m fill) = replicate n fill"
569 by (simp add : takefill_alt replicate_add [symmetric])
572 "n = m + k \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
573 by (induct m arbitrary: l n) (auto split: list.split)
575 lemma length_takefill [simp]: "length (takefill fill n l) = n"
576 by (simp add : takefill_alt)
578 lemma take_takefill':
579 "!!w n. n = k + m ==> take k (takefill fill n w) = takefill fill k w"
580 by (induct k) (auto split add : list.split)
583 "!!w. drop k (takefill fill (m + k) w) = takefill fill m (drop k w)"
584 by (induct k) (auto split add : list.split)
586 lemma takefill_le [simp]:
587 "m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
588 by (auto simp: le_iff_add takefill_le')
590 lemma take_takefill [simp]:
591 "m \<le> n \<Longrightarrow> take m (takefill fill n w) = takefill fill m w"
592 by (auto simp: le_iff_add take_takefill')
594 lemma takefill_append:
595 "takefill fill (m + length xs) (xs @ w) = xs @ (takefill fill m w)"
598 lemma takefill_same':
599 "l = length xs ==> takefill fill l xs = xs"
600 by clarify (induct xs, auto)
602 lemmas takefill_same [simp] = takefill_same' [OF refl]
604 lemma takefill_bintrunc:
605 "takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))"
606 apply (rule nth_equalityI)
608 apply (clarsimp simp: nth_takefill nth_rev nth_bin_to_bl bin_nth_of_bl)
612 "bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))"
613 by (simp add : takefill_bintrunc)
615 lemma bl_bin_bl_rep_drop:
616 "bin_to_bl n (bl_to_bin bl) =
617 replicate (n - length bl) False @ drop (length bl - n) bl"
618 by (simp add: bl_bin_bl_rtf takefill_alt rev_take)
621 "n + k = m + length bl ==> takefill x m (rev (takefill y n bl)) =
622 rev (takefill y m (rev (takefill x k (rev bl))))"
623 apply (rule nth_equalityI)
624 apply (auto simp add: nth_takefill nth_rev)
625 apply (rule_tac f = "%n. bl ! n" in arg_cong)
629 lemma takefill_minus:
630 "0 < n ==> takefill fill (Suc (n - 1)) w = takefill fill n w"
633 lemmas takefill_Suc_cases =
634 list.cases [THEN takefill.Suc [THEN trans]]
636 lemmas takefill_Suc_Nil = takefill_Suc_cases (1)
637 lemmas takefill_Suc_Cons = takefill_Suc_cases (2)
639 lemmas takefill_minus_simps = takefill_Suc_cases [THEN [2]
640 takefill_minus [symmetric, THEN trans]]
642 lemmas takefill_pred_simps [simp] =
643 takefill_minus_simps [where n="number_of bin", simplified nobm1] for bin
645 (* links with function bl_to_bin *)
647 lemma bl_to_bin_aux_cat:
648 "!!nv v. bl_to_bin_aux bs (bin_cat w nv v) =
649 bin_cat w (nv + length bs) (bl_to_bin_aux bs v)"
652 apply (simp add: bin_cat_Suc_Bit [symmetric] del: bin_cat.simps)
655 lemma bin_to_bl_aux_cat:
656 "!!w bs. bin_to_bl_aux (nv + nw) (bin_cat v nw w) bs =
657 bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)"
660 lemma bl_to_bin_aux_alt:
661 "bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)"
662 using bl_to_bin_aux_cat [where nv = "0" and v = "0"]
663 unfolding bl_to_bin_def [symmetric] by simp
666 "bin_to_bl (nv + nw) (bin_cat v nw w) =
667 bin_to_bl_aux nv v (bin_to_bl nw w)"
668 unfolding bin_to_bl_def by (simp add: bin_to_bl_aux_cat)
670 lemmas bl_to_bin_aux_app_cat =
671 trans [OF bl_to_bin_aux_append bl_to_bin_aux_alt]
673 lemmas bin_to_bl_aux_cat_app =
674 trans [OF bin_to_bl_aux_cat bin_to_bl_aux_alt]
676 lemma bl_to_bin_app_cat:
677 "bl_to_bin (bsa @ bs) = bin_cat (bl_to_bin bsa) (length bs) (bl_to_bin bs)"
678 by (simp only: bl_to_bin_aux_app_cat bl_to_bin_def)
680 lemma bin_to_bl_cat_app:
681 "bin_to_bl (n + nw) (bin_cat w nw wa) = bin_to_bl n w @ bin_to_bl nw wa"
682 by (simp only: bin_to_bl_def bin_to_bl_aux_cat_app)
684 (* bl_to_bin_app_cat_alt and bl_to_bin_app_cat are easily interderivable *)
685 lemma bl_to_bin_app_cat_alt:
686 "bin_cat (bl_to_bin cs) n w = bl_to_bin (cs @ bin_to_bl n w)"
687 by (simp add : bl_to_bin_app_cat)
689 lemma mask_lem: "(bl_to_bin (True # replicate n False)) =
690 Int.succ (bl_to_bin (replicate n True))"
691 apply (unfold bl_to_bin_def)
693 apply (simp add: Int.succ_def)
694 apply (simp only: Suc_eq_plus1 replicate_add
695 append_Cons [symmetric] bl_to_bin_aux_append)
696 apply (simp add: BIT_simps)
699 (* function bl_of_nth *)
700 lemma length_bl_of_nth [simp]: "length (bl_of_nth n f) = n"
703 lemma nth_bl_of_nth [simp]:
704 "m < n \<Longrightarrow> rev (bl_of_nth n f) ! m = f m"
707 apply (clarsimp simp add : nth_append)
708 apply (rule_tac f = "f" in arg_cong)
713 "(!!k. k < n ==> f k = g k) ==> bl_of_nth n f = bl_of_nth n g"
716 lemma bl_of_nth_nth_le:
717 "n \<le> length xs \<Longrightarrow> bl_of_nth n (nth (rev xs)) = drop (length xs - n) xs"
718 apply (induct n arbitrary: xs, clarsimp)
720 apply (rule trans [OF _ hd_Cons_tl])
721 apply (frule Suc_le_lessD)
722 apply (simp add: nth_rev trans [OF drop_Suc drop_tl, symmetric])
723 apply (subst hd_drop_conv_nth)
726 apply (rule_tac f = "%n. drop n xs" in arg_cong)
730 lemma bl_of_nth_nth [simp]: "bl_of_nth (length xs) (op ! (rev xs)) = xs"
731 by (simp add: bl_of_nth_nth_le)
733 lemma size_rbl_pred: "length (rbl_pred bl) = length bl"
736 lemma size_rbl_succ: "length (rbl_succ bl) = length bl"
740 "!!cl. length (rbl_add bl cl) = length bl"
741 by (induct bl) (auto simp: Let_def size_rbl_succ)
744 "!!cl. length (rbl_mult bl cl) = length bl"
745 by (induct bl) (auto simp add : Let_def size_rbl_add)
747 lemmas rbl_sizes [simp] =
748 size_rbl_pred size_rbl_succ size_rbl_add size_rbl_mult
751 rbl_pred.Nil rbl_succ.Nil rbl_add.Nil rbl_mult.Nil
754 "!!bin. rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (Int.pred bin))"
755 apply (induct n, simp)
756 apply (unfold bin_to_bl_def)
758 apply (case_tac bin rule: bin_exhaust)
760 apply (clarsimp simp: bin_to_bl_aux_alt BIT_simps)+
764 "!!bin. rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (Int.succ bin))"
765 apply (induct n, simp)
766 apply (unfold bin_to_bl_def)
768 apply (case_tac bin rule: bin_exhaust)
770 apply (clarsimp simp: bin_to_bl_aux_alt BIT_simps)+
774 "!!bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
775 rev (bin_to_bl n (bina + binb))"
776 apply (induct n, simp)
777 apply (unfold bin_to_bl_def)
779 apply (case_tac bina rule: bin_exhaust)
780 apply (case_tac binb rule: bin_exhaust)
782 apply (case_tac [!] "ba")
783 apply (auto simp: rbl_succ succ_def bin_to_bl_aux_alt Let_def add_ac BIT_simps)
787 "!!blb. length blb >= length bla ==>
788 rbl_add bla (blb @ blc) = rbl_add bla blb"
789 apply (induct bla, simp)
791 apply (case_tac blb, clarsimp)
792 apply (clarsimp simp: Let_def)
796 "!!blb. length blb >= length bla ==>
797 rbl_add bla (take (length bla) blb) = rbl_add bla blb"
798 apply (induct bla, simp)
800 apply (case_tac blb, clarsimp)
801 apply (clarsimp simp: Let_def)
805 "m >= n ==> rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
806 rev (bin_to_bl n (bina + binb))"
807 apply (rule box_equals [OF _ rbl_add_take2 rbl_add])
808 apply (rule_tac f = "rbl_add (rev (bin_to_bl n bina))" in arg_cong)
809 apply (rule rev_swap [THEN iffD1])
810 apply (simp add: rev_take drop_bin2bl)
815 "!!blb. length blb >= length bla ==>
816 rbl_mult bla (blb @ blc) = rbl_mult bla blb"
817 apply (induct bla, simp)
819 apply (case_tac blb, clarsimp)
820 apply (clarsimp simp: Let_def rbl_add_app2)
823 lemma rbl_mult_take2:
824 "length blb >= length bla ==>
825 rbl_mult bla (take (length bla) blb) = rbl_mult bla blb"
827 apply (rule rbl_mult_app2 [symmetric])
829 apply (rule_tac f = "rbl_mult bla" in arg_cong)
830 apply (rule append_take_drop_id)
834 "m >= length bl ==> rbl_mult bl (rev (bin_to_bl m binb)) =
835 rbl_mult bl (rev (bin_to_bl (length bl) binb))"
837 apply (rule rbl_mult_take2 [symmetric])
839 apply (rule_tac f = "rbl_mult bl" in arg_cong)
840 apply (rule rev_swap [THEN iffD1])
841 apply (simp add: rev_take drop_bin2bl)
845 "m > n ==> rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) =
846 rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb))"
847 by (auto intro: trans [OF rbl_mult_gt1])
849 lemmas rbl_mult_Suc = lessI [THEN rbl_mult_gt]
852 "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (x BIT If b 1 0))"
853 apply (unfold bin_to_bl_def)
855 apply (simp add: bin_to_bl_aux_alt)
858 lemma rbl_mult: "!!bina binb.
859 rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) =
860 rev (bin_to_bl n (bina * binb))"
863 apply (unfold bin_to_bl_def)
865 apply (case_tac bina rule: bin_exhaust)
866 apply (case_tac binb rule: bin_exhaust)
868 apply (case_tac [!] "ba")
869 apply (auto simp: bin_to_bl_aux_alt Let_def BIT_simps)
870 apply (auto simp: rbbl_Cons rbl_mult_Suc rbl_add BIT_simps)
874 "P (rbl_add (y # ys) (x # xs)) =
875 (ALL ws. length ws = length ys --> ws = rbl_add ys xs -->
876 (y --> ((x --> P (False # rbl_succ ws)) & (~ x --> P (True # ws)))) &
877 (~ y --> P (x # ws)))"
878 apply (auto simp add: Let_def)
879 apply (case_tac [!] "y")
883 lemma rbl_mult_split:
884 "P (rbl_mult (y # ys) xs) =
885 (ALL ws. length ws = Suc (length ys) --> ws = False # rbl_mult ys xs -->
886 (y --> P (rbl_add ws xs)) & (~ y --> P ws))"
887 by (clarsimp simp add : Let_def)
889 lemma and_len: "xs = ys ==> xs = ys & length xs = length ys"
892 lemma size_if: "size (if p then xs else ys) = (if p then size xs else size ys)"
895 lemma tl_if: "tl (if p then xs else ys) = (if p then tl xs else tl ys)"
898 lemma hd_if: "hd (if p then xs else ys) = (if p then hd xs else hd ys)"
901 lemma if_Not_x: "(if p then ~ x else x) = (p = (~ x))"
904 lemma if_x_Not: "(if p then x else ~ x) = (p = x)"
907 lemma if_same_and: "(If p x y & If p u v) = (if p then x & u else y & v)"
910 lemma if_same_eq: "(If p x y = (If p u v)) = (if p then x = (u) else y = (v))"
913 lemma if_same_eq_not:
914 "(If p x y = (~ If p u v)) = (if p then x = (~u) else y = (~v))"
917 (* note - if_Cons can cause blowup in the size, if p is complex,
919 lemma if_Cons: "(if p then x # xs else y # ys) = If p x y # If p xs ys"
923 "(if xc then [xab] else [an]) = [if xc then xab else an]"
927 "If p True y = (p | y) & If p False y = (~p & y) &
928 If p y True = (p --> y) & If p y False = (p & y)"
931 lemmas if_simps = if_x_Not if_Not_x if_cancel if_True if_False if_bool_simps
933 lemmas seqr = eq_reflection [where x = "size w"] for w (* FIXME: delete *)
935 (* TODO: move name bindings to List.thy *)
936 lemmas tl_Nil = tl.simps (1)
937 lemmas tl_Cons = tl.simps (2)
940 subsection "Repeated splitting or concatenation"
943 "size (concat (map (bin_to_bl n) xs)) = length xs * n"
946 lemma bin_cat_foldl_lem:
947 "foldl (%u. bin_cat u n) x xs =
948 bin_cat x (size xs * n) (foldl (%u. bin_cat u n) y xs)"
949 apply (induct xs arbitrary: x)
951 apply (simp (no_asm))
953 apply (drule meta_spec)
955 apply (drule_tac x = "bin_cat y n a" in meta_spec)
956 apply (simp add : bin_cat_assoc_sym min_max.inf_absorb2)
960 "(bin_rcat n wl) = bl_to_bin (concat (map (bin_to_bl n) wl))"
961 apply (unfold bin_rcat_def)
964 apply (auto simp add : bl_to_bin_append)
965 apply (simp add : bl_to_bin_aux_alt sclem)
966 apply (simp add : bin_cat_foldl_lem [symmetric])
969 lemmas bin_rsplit_aux_simps = bin_rsplit_aux.simps bin_rsplitl_aux.simps
970 lemmas rsplit_aux_simps = bin_rsplit_aux_simps
972 lemmas th_if_simp1 = split_if [where P = "op = l", THEN iffD1, THEN conjunct1, THEN mp] for l
973 lemmas th_if_simp2 = split_if [where P = "op = l", THEN iffD1, THEN conjunct2, THEN mp] for l
975 lemmas rsplit_aux_simp1s = rsplit_aux_simps [THEN th_if_simp1]
977 lemmas rsplit_aux_simp2ls = rsplit_aux_simps [THEN th_if_simp2]
978 (* these safe to [simp add] as require calculating m - n *)
979 lemmas bin_rsplit_aux_simp2s [simp] = rsplit_aux_simp2ls [unfolded Let_def]
980 lemmas rbscl = bin_rsplit_aux_simp2s (2)
982 lemmas rsplit_aux_0_simps [simp] =
983 rsplit_aux_simp1s [OF disjI1] rsplit_aux_simp1s [OF disjI2]
985 lemma bin_rsplit_aux_append:
986 "bin_rsplit_aux n m c (bs @ cs) = bin_rsplit_aux n m c bs @ cs"
987 apply (induct n m c bs rule: bin_rsplit_aux.induct)
988 apply (subst bin_rsplit_aux.simps)
989 apply (subst bin_rsplit_aux.simps)
990 apply (clarsimp split: ls_splits)
994 lemma bin_rsplitl_aux_append:
995 "bin_rsplitl_aux n m c (bs @ cs) = bin_rsplitl_aux n m c bs @ cs"
996 apply (induct n m c bs rule: bin_rsplitl_aux.induct)
997 apply (subst bin_rsplitl_aux.simps)
998 apply (subst bin_rsplitl_aux.simps)
999 apply (clarsimp split: ls_splits)
1003 lemmas rsplit_aux_apps [where bs = "[]"] =
1004 bin_rsplit_aux_append bin_rsplitl_aux_append
1006 lemmas rsplit_def_auxs = bin_rsplit_def bin_rsplitl_def
1008 lemmas rsplit_aux_alts = rsplit_aux_apps
1009 [unfolded append_Nil rsplit_def_auxs [symmetric]]
1011 lemma bin_split_minus: "0 < n ==> bin_split (Suc (n - 1)) w = bin_split n w"
1014 lemmas bin_split_minus_simp =
1015 bin_split.Suc [THEN [2] bin_split_minus [symmetric, THEN trans]]
1017 lemma bin_split_pred_simp [simp]:
1018 "(0::nat) < number_of bin \<Longrightarrow>
1019 bin_split (number_of bin) w =
1020 (let (w1, w2) = bin_split (number_of (Int.pred bin)) (bin_rest w)
1021 in (w1, w2 BIT bin_last w))"
1022 by (simp only: nobm1 bin_split_minus_simp)
1024 lemma bin_rsplit_aux_simp_alt:
1025 "bin_rsplit_aux n m c bs =
1026 (if m = 0 \<or> n = 0
1028 else let (a, b) = bin_split n c in bin_rsplit n (m - n, a) @ b # bs)"
1029 unfolding bin_rsplit_aux.simps [of n m c bs]
1031 apply (subst rsplit_aux_alts)
1032 apply (simp add: bin_rsplit_def)
1035 lemmas bin_rsplit_simp_alt =
1036 trans [OF bin_rsplit_def bin_rsplit_aux_simp_alt]
1038 lemmas bthrs = bin_rsplit_simp_alt [THEN [2] trans]
1040 lemma bin_rsplit_size_sign' [rule_format] :
1041 "\<lbrakk>n > 0; rev sw = bin_rsplit n (nw, w)\<rbrakk> \<Longrightarrow>
1042 (ALL v: set sw. bintrunc n v = v)"
1043 apply (induct sw arbitrary: nw w v)
1047 apply (simp (no_asm_use) add: Let_def split: ls_splits)
1049 apply (drule split_bintrunc)
1053 lemmas bin_rsplit_size_sign = bin_rsplit_size_sign' [OF asm_rl
1054 rev_rev_ident [THEN trans] set_rev [THEN equalityD2 [THEN subsetD]]]
1056 lemma bin_nth_rsplit [rule_format] :
1057 "n > 0 ==> m < n ==> (ALL w k nw. rev sw = bin_rsplit n (nw, w) -->
1058 k < size sw --> bin_nth (sw ! k) m = bin_nth w (k * n + m))"
1063 apply (simp (no_asm_use) add: Let_def split: ls_splits)
1065 apply (erule allE, erule impE, erule exI)
1071 apply (erule (1) impE)
1072 apply (drule bin_nth_split, erule conjE, erule allE,
1073 erule trans, simp add : add_ac)+
1076 lemma bin_rsplit_all:
1077 "0 < nw ==> nw <= n ==> bin_rsplit n (nw, w) = [bintrunc n w]"
1078 unfolding bin_rsplit_def
1079 by (clarsimp dest!: split_bintrunc simp: rsplit_aux_simp2ls split: ls_splits)
1081 lemma bin_rsplit_l [rule_format] :
1082 "ALL bin. bin_rsplitl n (m, bin) = bin_rsplit n (m, bintrunc m bin)"
1083 apply (rule_tac a = "m" in wf_less_than [THEN wf_induct])
1084 apply (simp (no_asm) add : bin_rsplitl_def bin_rsplit_def)
1086 apply (subst bin_rsplitl_aux.simps)
1087 apply (subst bin_rsplit_aux.simps)
1088 apply (clarsimp simp: Let_def split: ls_splits)
1089 apply (drule bin_split_trunc)
1090 apply (drule sym [THEN trans], assumption)
1091 apply (subst rsplit_aux_alts(1))
1092 apply (subst rsplit_aux_alts(2))
1094 unfolding bin_rsplit_def bin_rsplitl_def
1098 lemma bin_rsplit_rcat [rule_format] :
1099 "n > 0 --> bin_rsplit n (n * size ws, bin_rcat n ws) = map (bintrunc n) ws"
1100 apply (unfold bin_rsplit_def bin_rcat_def)
1101 apply (rule_tac xs = "ws" in rev_induct)
1104 apply (subst rsplit_aux_alts)
1105 unfolding bin_split_cat
1109 lemma bin_rsplit_aux_len_le [rule_format] :
1110 "\<forall>ws m. n \<noteq> 0 \<longrightarrow> ws = bin_rsplit_aux n nw w bs \<longrightarrow>
1111 length ws \<le> m \<longleftrightarrow> nw + length bs * n \<le> m * n"
1112 apply (induct n nw w bs rule: bin_rsplit_aux.induct)
1113 apply (subst bin_rsplit_aux.simps)
1114 apply (simp add: lrlem Let_def split: ls_splits)
1117 lemma bin_rsplit_len_le:
1118 "n \<noteq> 0 --> ws = bin_rsplit n (nw, w) --> (length ws <= m) = (nw <= m * n)"
1119 unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len_le)
1121 lemma bin_rsplit_aux_len:
1122 "n \<noteq> 0 \<Longrightarrow> length (bin_rsplit_aux n nw w cs) =
1123 (nw + n - 1) div n + length cs"
1124 apply (induct n nw w cs rule: bin_rsplit_aux.induct)
1125 apply (subst bin_rsplit_aux.simps)
1126 apply (clarsimp simp: Let_def split: ls_splits)
1127 apply (erule thin_rl)
1130 apply (case_tac "m <= n")
1134 lemma bin_rsplit_len:
1135 "n\<noteq>0 ==> length (bin_rsplit n (nw, w)) = (nw + n - 1) div n"
1136 unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len)
1138 lemma bin_rsplit_aux_len_indep:
1139 "n \<noteq> 0 \<Longrightarrow> length bs = length cs \<Longrightarrow>
1140 length (bin_rsplit_aux n nw v bs) =
1141 length (bin_rsplit_aux n nw w cs)"
1142 proof (induct n nw w cs arbitrary: v bs rule: bin_rsplit_aux.induct)
1143 case (1 n m w cs v bs) show ?case
1144 proof (cases "m = 0")
1145 case True then show ?thesis using `length bs = length cs` by simp
1148 from "1.hyps" `m \<noteq> 0` `n \<noteq> 0` have hyp: "\<And>v bs. length bs = Suc (length cs) \<Longrightarrow>
1149 length (bin_rsplit_aux n (m - n) v bs) =
1150 length (bin_rsplit_aux n (m - n) (fst (bin_split n w)) (snd (bin_split n w) # cs))"
1152 show ?thesis using `length bs = length cs` `n \<noteq> 0`
1153 by (auto simp add: bin_rsplit_aux_simp_alt Let_def bin_rsplit_len
1158 lemma bin_rsplit_len_indep:
1159 "n\<noteq>0 ==> length (bin_rsplit n (nw, v)) = length (bin_rsplit n (nw, w))"
1160 apply (unfold bin_rsplit_def)
1161 apply (simp (no_asm))
1162 apply (erule bin_rsplit_aux_len_indep)