src/HOL/Word/Bool_List_Representation.thy
 author wenzelm Sun Sep 18 20:33:48 2016 +0200 (2016-09-18) changeset 63915 bab633745c7f parent 63648 f9f3006a5579 child 64507 eace715f4988 permissions -rw-r--r--
tuned proofs;
 kleing@24333 ` 1` ```(* ``` kleing@24333 ` 2` ``` Author: Jeremy Dawson, NICTA ``` kleing@24333 ` 3` kleing@44939 ` 4` ``` Theorems to do with integers, expressed using Pls, Min, BIT, ``` kleing@24333 ` 5` ``` theorems linking them to lists of booleans, and repeated splitting ``` kleing@24333 ` 6` ``` and concatenation. ``` kleing@24333 ` 7` ```*) ``` kleing@24333 ` 8` wenzelm@58874 ` 9` ```section "Bool lists and integers" ``` kleing@24333 ` 10` haftmann@37658 ` 11` ```theory Bool_List_Representation ``` eberlm@63501 ` 12` ```imports Complex_Main Bits_Int ``` haftmann@26557 ` 13` ```begin ``` kleing@24333 ` 14` haftmann@53062 ` 15` ```definition map2 :: "('a \ 'b \ 'c) \ 'a list \ 'b list \ 'c list" ``` haftmann@53062 ` 16` ```where ``` haftmann@61424 ` 17` ``` "map2 f as bs = map (case_prod f) (zip as bs)" ``` haftmann@53062 ` 18` haftmann@53062 ` 19` ```lemma map2_Nil [simp, code]: ``` haftmann@53062 ` 20` ``` "map2 f [] ys = []" ``` haftmann@53062 ` 21` ``` unfolding map2_def by auto ``` haftmann@53062 ` 22` haftmann@53062 ` 23` ```lemma map2_Nil2 [simp, code]: ``` haftmann@53062 ` 24` ``` "map2 f xs [] = []" ``` haftmann@53062 ` 25` ``` unfolding map2_def by auto ``` haftmann@53062 ` 26` haftmann@53062 ` 27` ```lemma map2_Cons [simp, code]: ``` haftmann@53062 ` 28` ``` "map2 f (x # xs) (y # ys) = f x y # map2 f xs ys" ``` haftmann@53062 ` 29` ``` unfolding map2_def by auto ``` haftmann@53062 ` 30` haftmann@53062 ` 31` wenzelm@61799 ` 32` ```subsection \Operations on lists of booleans\ ``` haftmann@37657 ` 33` haftmann@54848 ` 34` ```primrec bl_to_bin_aux :: "bool list \ int \ int" ``` haftmann@54848 ` 35` ```where ``` haftmann@37657 ` 36` ``` Nil: "bl_to_bin_aux [] w = w" ``` haftmann@37657 ` 37` ``` | Cons: "bl_to_bin_aux (b # bs) w = ``` haftmann@54847 ` 38` ``` bl_to_bin_aux bs (w BIT b)" ``` haftmann@37657 ` 39` haftmann@54848 ` 40` ```definition bl_to_bin :: "bool list \ int" ``` haftmann@54848 ` 41` ```where ``` huffman@46001 ` 42` ``` bl_to_bin_def: "bl_to_bin bs = bl_to_bin_aux bs 0" ``` haftmann@37667 ` 43` haftmann@54848 ` 44` ```primrec bin_to_bl_aux :: "nat \ int \ bool list \ bool list" ``` haftmann@54848 ` 45` ```where ``` haftmann@37657 ` 46` ``` Z: "bin_to_bl_aux 0 w bl = bl" ``` haftmann@37657 ` 47` ``` | Suc: "bin_to_bl_aux (Suc n) w bl = ``` haftmann@54847 ` 48` ``` bin_to_bl_aux n (bin_rest w) ((bin_last w) # bl)" ``` haftmann@37657 ` 49` haftmann@54848 ` 50` ```definition bin_to_bl :: "nat \ int \ bool list" ``` haftmann@54848 ` 51` ```where ``` haftmann@37657 ` 52` ``` bin_to_bl_def : "bin_to_bl n w = bin_to_bl_aux n w []" ``` haftmann@37657 ` 53` haftmann@54848 ` 54` ```primrec bl_of_nth :: "nat \ (nat \ bool) \ bool list" ``` haftmann@54848 ` 55` ```where ``` haftmann@37657 ` 56` ``` Suc: "bl_of_nth (Suc n) f = f n # bl_of_nth n f" ``` haftmann@37657 ` 57` ``` | Z: "bl_of_nth 0 f = []" ``` haftmann@37657 ` 58` haftmann@54848 ` 59` ```primrec takefill :: "'a \ nat \ 'a list \ 'a list" ``` haftmann@54848 ` 60` ```where ``` haftmann@37657 ` 61` ``` Z: "takefill fill 0 xs = []" ``` haftmann@37657 ` 62` ``` | Suc: "takefill fill (Suc n) xs = ( ``` haftmann@37657 ` 63` ``` case xs of [] => fill # takefill fill n xs ``` haftmann@37657 ` 64` ``` | y # ys => y # takefill fill n ys)" ``` haftmann@37657 ` 65` haftmann@37657 ` 66` huffman@24465 ` 67` ```subsection "Arithmetic in terms of bool lists" ``` huffman@24465 ` 68` wenzelm@61799 ` 69` ```text \ ``` kleing@44939 ` 70` ``` Arithmetic operations in terms of the reversed bool list, ``` kleing@44939 ` 71` ``` assuming input list(s) the same length, and don't extend them. ``` wenzelm@61799 ` 72` ```\ ``` huffman@24465 ` 73` haftmann@54848 ` 74` ```primrec rbl_succ :: "bool list => bool list" ``` haftmann@54848 ` 75` ```where ``` huffman@24465 ` 76` ``` Nil: "rbl_succ Nil = Nil" ``` haftmann@26557 ` 77` ``` | Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)" ``` huffman@24465 ` 78` haftmann@54848 ` 79` ```primrec rbl_pred :: "bool list => bool list" ``` haftmann@54848 ` 80` ```where ``` haftmann@26557 ` 81` ``` Nil: "rbl_pred Nil = Nil" ``` haftmann@26557 ` 82` ``` | Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)" ``` huffman@24465 ` 83` haftmann@54848 ` 84` ```primrec rbl_add :: "bool list => bool list => bool list" ``` haftmann@54848 ` 85` ```where ``` wenzelm@61799 ` 86` ``` \ "result is length of first arg, second arg may be longer" ``` haftmann@26557 ` 87` ``` Nil: "rbl_add Nil x = Nil" ``` haftmann@26557 ` 88` ``` | Cons: "rbl_add (y # ys) x = (let ws = rbl_add ys (tl x) in ``` huffman@24465 ` 89` ``` (y ~= hd x) # (if hd x & y then rbl_succ ws else ws))" ``` huffman@24465 ` 90` haftmann@54848 ` 91` ```primrec rbl_mult :: "bool list => bool list => bool list" ``` haftmann@54848 ` 92` ```where ``` wenzelm@61799 ` 93` ``` \ "result is length of first arg, second arg may be longer" ``` haftmann@26557 ` 94` ``` Nil: "rbl_mult Nil x = Nil" ``` haftmann@26557 ` 95` ``` | Cons: "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in ``` huffman@24465 ` 96` ``` if y then rbl_add ws x else ws)" ``` kleing@24333 ` 97` kleing@24333 ` 98` ```lemma butlast_power: ``` haftmann@30971 ` 99` ``` "(butlast ^^ n) bl = take (length bl - n) bl" ``` kleing@24333 ` 100` ``` by (induct n) (auto simp: butlast_take) ``` kleing@24333 ` 101` huffman@46001 ` 102` ```lemma bin_to_bl_aux_zero_minus_simp [simp]: ``` huffman@46001 ` 103` ``` "0 < n \ bin_to_bl_aux n 0 bl = ``` huffman@46001 ` 104` ``` bin_to_bl_aux (n - 1) 0 (False # bl)" ``` huffman@46001 ` 105` ``` by (cases n) auto ``` huffman@46001 ` 106` huffman@46617 ` 107` ```lemma bin_to_bl_aux_minus1_minus_simp [simp]: ``` haftmann@58410 ` 108` ``` "0 < n ==> bin_to_bl_aux n (- 1) bl = ``` haftmann@58410 ` 109` ``` bin_to_bl_aux (n - 1) (- 1) (True # bl)" ``` kleing@24333 ` 110` ``` by (cases n) auto ``` kleing@24333 ` 111` huffman@46617 ` 112` ```lemma bin_to_bl_aux_one_minus_simp [simp]: ``` huffman@46617 ` 113` ``` "0 < n \ bin_to_bl_aux n 1 bl = ``` huffman@46617 ` 114` ``` bin_to_bl_aux (n - 1) 0 (True # bl)" ``` kleing@24333 ` 115` ``` by (cases n) auto ``` kleing@24333 ` 116` huffman@26086 ` 117` ```lemma bin_to_bl_aux_Bit_minus_simp [simp]: ``` kleing@24333 ` 118` ``` "0 < n ==> bin_to_bl_aux n (w BIT b) bl = ``` haftmann@54847 ` 119` ``` bin_to_bl_aux (n - 1) w (b # bl)" ``` kleing@24333 ` 120` ``` by (cases n) auto ``` kleing@24333 ` 121` huffman@26086 ` 122` ```lemma bin_to_bl_aux_Bit0_minus_simp [simp]: ``` huffman@47108 ` 123` ``` "0 < n ==> bin_to_bl_aux n (numeral (Num.Bit0 w)) bl = ``` huffman@47108 ` 124` ``` bin_to_bl_aux (n - 1) (numeral w) (False # bl)" ``` huffman@26086 ` 125` ``` by (cases n) auto ``` huffman@26086 ` 126` huffman@26086 ` 127` ```lemma bin_to_bl_aux_Bit1_minus_simp [simp]: ``` huffman@47108 ` 128` ``` "0 < n ==> bin_to_bl_aux n (numeral (Num.Bit1 w)) bl = ``` huffman@47108 ` 129` ``` bin_to_bl_aux (n - 1) (numeral w) (True # bl)" ``` huffman@26086 ` 130` ``` by (cases n) auto ``` kleing@24333 ` 131` wenzelm@61799 ` 132` ```text \Link between bin and bool list.\ ``` huffman@24465 ` 133` haftmann@26557 ` 134` ```lemma bl_to_bin_aux_append: ``` haftmann@26557 ` 135` ``` "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)" ``` haftmann@26557 ` 136` ``` by (induct bs arbitrary: w) auto ``` huffman@24465 ` 137` haftmann@26557 ` 138` ```lemma bin_to_bl_aux_append: ``` haftmann@26557 ` 139` ``` "bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)" ``` haftmann@26557 ` 140` ``` by (induct n arbitrary: w bs) auto ``` kleing@24333 ` 141` huffman@24465 ` 142` ```lemma bl_to_bin_append: ``` haftmann@26557 ` 143` ``` "bl_to_bin (bs @ cs) = bl_to_bin_aux cs (bl_to_bin bs)" ``` huffman@24465 ` 144` ``` unfolding bl_to_bin_def by (rule bl_to_bin_aux_append) ``` huffman@24465 ` 145` kleing@24333 ` 146` ```lemma bin_to_bl_aux_alt: ``` kleing@24333 ` 147` ``` "bin_to_bl_aux n w bs = bin_to_bl n w @ bs" ``` kleing@24333 ` 148` ``` unfolding bin_to_bl_def by (simp add : bin_to_bl_aux_append) ``` kleing@24333 ` 149` huffman@45996 ` 150` ```lemma bin_to_bl_0 [simp]: "bin_to_bl 0 bs = []" ``` kleing@24333 ` 151` ``` unfolding bin_to_bl_def by auto ``` kleing@24333 ` 152` haftmann@26557 ` 153` ```lemma size_bin_to_bl_aux: ``` haftmann@26557 ` 154` ``` "size (bin_to_bl_aux n w bs) = n + length bs" ``` haftmann@26557 ` 155` ``` by (induct n arbitrary: w bs) auto ``` kleing@24333 ` 156` huffman@45996 ` 157` ```lemma size_bin_to_bl [simp]: "size (bin_to_bl n w) = n" ``` kleing@24333 ` 158` ``` unfolding bin_to_bl_def by (simp add : size_bin_to_bl_aux) ``` kleing@24333 ` 159` haftmann@26557 ` 160` ```lemma bin_bl_bin': ``` haftmann@26557 ` 161` ``` "bl_to_bin (bin_to_bl_aux n w bs) = ``` haftmann@26557 ` 162` ``` bl_to_bin_aux bs (bintrunc n w)" ``` haftmann@26557 ` 163` ``` by (induct n arbitrary: w bs) (auto simp add : bl_to_bin_def) ``` huffman@24465 ` 164` huffman@45996 ` 165` ```lemma bin_bl_bin [simp]: "bl_to_bin (bin_to_bl n w) = bintrunc n w" ``` huffman@24465 ` 166` ``` unfolding bin_to_bl_def bin_bl_bin' by auto ``` huffman@24465 ` 167` haftmann@26557 ` 168` ```lemma bl_bin_bl': ``` haftmann@26557 ` 169` ``` "bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = ``` huffman@24465 ` 170` ``` bin_to_bl_aux n w bs" ``` haftmann@26557 ` 171` ``` apply (induct bs arbitrary: w n) ``` huffman@24465 ` 172` ``` apply auto ``` huffman@24465 ` 173` ``` apply (simp_all only : add_Suc [symmetric]) ``` huffman@24465 ` 174` ``` apply (auto simp add : bin_to_bl_def) ``` huffman@24465 ` 175` ``` done ``` huffman@24465 ` 176` huffman@45996 ` 177` ```lemma bl_bin_bl [simp]: "bin_to_bl (length bs) (bl_to_bin bs) = bs" ``` huffman@24465 ` 178` ``` unfolding bl_to_bin_def ``` huffman@24465 ` 179` ``` apply (rule box_equals) ``` huffman@24465 ` 180` ``` apply (rule bl_bin_bl') ``` huffman@24465 ` 181` ``` prefer 2 ``` huffman@24465 ` 182` ``` apply (rule bin_to_bl_aux.Z) ``` huffman@24465 ` 183` ``` apply simp ``` huffman@24465 ` 184` ``` done ``` huffman@24465 ` 185` ``` ``` huffman@24465 ` 186` ```lemma bl_to_bin_inj: ``` huffman@24465 ` 187` ``` "bl_to_bin bs = bl_to_bin cs ==> length bs = length cs ==> bs = cs" ``` huffman@24465 ` 188` ``` apply (rule_tac box_equals) ``` huffman@24465 ` 189` ``` defer ``` huffman@24465 ` 190` ``` apply (rule bl_bin_bl) ``` huffman@24465 ` 191` ``` apply (rule bl_bin_bl) ``` huffman@24465 ` 192` ``` apply simp ``` huffman@24465 ` 193` ``` done ``` huffman@24465 ` 194` huffman@45996 ` 195` ```lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl" ``` huffman@46001 ` 196` ``` unfolding bl_to_bin_def by auto ``` huffman@45996 ` 197` huffman@46001 ` 198` ```lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = 0" ``` huffman@24465 ` 199` ``` unfolding bl_to_bin_def by auto ``` huffman@24465 ` 200` huffman@46001 ` 201` ```lemma bin_to_bl_zero_aux: ``` huffman@46001 ` 202` ``` "bin_to_bl_aux n 0 bl = replicate n False @ bl" ``` huffman@46001 ` 203` ``` by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same) ``` huffman@46001 ` 204` huffman@46617 ` 205` ```lemma bin_to_bl_zero: "bin_to_bl n 0 = replicate n False" ``` huffman@46617 ` 206` ``` unfolding bin_to_bl_def by (simp add: bin_to_bl_zero_aux) ``` huffman@46617 ` 207` huffman@46617 ` 208` ```lemma bin_to_bl_minus1_aux: ``` haftmann@58410 ` 209` ``` "bin_to_bl_aux n (- 1) bl = replicate n True @ bl" ``` haftmann@26557 ` 210` ``` by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same) ``` kleing@24333 ` 211` haftmann@58410 ` 212` ```lemma bin_to_bl_minus1: "bin_to_bl n (- 1) = replicate n True" ``` huffman@46617 ` 213` ``` unfolding bin_to_bl_def by (simp add: bin_to_bl_minus1_aux) ``` kleing@24333 ` 214` huffman@24465 ` 215` ```lemma bl_to_bin_rep_F: ``` huffman@24465 ` 216` ``` "bl_to_bin (replicate n False @ bl) = bl_to_bin bl" ``` huffman@46001 ` 217` ``` apply (simp add: bin_to_bl_zero_aux [symmetric] bin_bl_bin') ``` huffman@24465 ` 218` ``` apply (simp add: bl_to_bin_def) ``` huffman@24465 ` 219` ``` done ``` huffman@24465 ` 220` huffman@45996 ` 221` ```lemma bin_to_bl_trunc [simp]: ``` huffman@24465 ` 222` ``` "n <= m ==> bin_to_bl n (bintrunc m w) = bin_to_bl n w" ``` huffman@24465 ` 223` ``` by (auto intro: bl_to_bin_inj) ``` huffman@24465 ` 224` huffman@45997 ` 225` ```lemma bin_to_bl_aux_bintr: ``` huffman@45997 ` 226` ``` "bin_to_bl_aux n (bintrunc m bin) bl = ``` kleing@24333 ` 227` ``` replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl" ``` huffman@45997 ` 228` ``` apply (induct n arbitrary: m bin bl) ``` kleing@24333 ` 229` ``` apply clarsimp ``` kleing@24333 ` 230` ``` apply clarsimp ``` kleing@24333 ` 231` ``` apply (case_tac "m") ``` huffman@46001 ` 232` ``` apply (clarsimp simp: bin_to_bl_zero_aux) ``` kleing@24333 ` 233` ``` apply (erule thin_rl) ``` kleing@24333 ` 234` ``` apply (induct_tac n) ``` kleing@24333 ` 235` ``` apply auto ``` kleing@24333 ` 236` ``` done ``` kleing@24333 ` 237` huffman@45854 ` 238` ```lemma bin_to_bl_bintr: ``` huffman@45854 ` 239` ``` "bin_to_bl n (bintrunc m bin) = ``` huffman@45854 ` 240` ``` replicate (n - m) False @ bin_to_bl (min n m) bin" ``` huffman@45854 ` 241` ``` unfolding bin_to_bl_def by (rule bin_to_bl_aux_bintr) ``` kleing@24333 ` 242` huffman@46001 ` 243` ```lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = 0" ``` huffman@24465 ` 244` ``` by (induct n) auto ``` huffman@24465 ` 245` haftmann@26557 ` 246` ```lemma len_bin_to_bl_aux: ``` haftmann@26557 ` 247` ``` "length (bin_to_bl_aux n w bs) = n + length bs" ``` haftmann@54869 ` 248` ``` by (fact size_bin_to_bl_aux) ``` kleing@24333 ` 249` kleing@24333 ` 250` ```lemma len_bin_to_bl [simp]: "length (bin_to_bl n w) = n" ``` huffman@46617 ` 251` ``` by (fact size_bin_to_bl) (* FIXME: duplicate *) ``` kleing@24333 ` 252` ``` ``` haftmann@26557 ` 253` ```lemma sign_bl_bin': ``` haftmann@26557 ` 254` ``` "bin_sign (bl_to_bin_aux bs w) = bin_sign w" ``` haftmann@26557 ` 255` ``` by (induct bs arbitrary: w) auto ``` kleing@24333 ` 256` ``` ``` huffman@46001 ` 257` ```lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = 0" ``` kleing@24333 ` 258` ``` unfolding bl_to_bin_def by (simp add : sign_bl_bin') ``` kleing@24333 ` 259` ``` ``` haftmann@26557 ` 260` ```lemma bl_sbin_sign_aux: ``` haftmann@26557 ` 261` ``` "hd (bin_to_bl_aux (Suc n) w bs) = ``` huffman@46001 ` 262` ``` (bin_sign (sbintrunc n w) = -1)" ``` haftmann@26557 ` 263` ``` apply (induct n arbitrary: w bs) ``` kleing@24333 ` 264` ``` apply clarsimp ``` haftmann@26557 ` 265` ``` apply (cases w rule: bin_exhaust) ``` haftmann@54847 ` 266` ``` apply simp ``` kleing@24333 ` 267` ``` done ``` kleing@24333 ` 268` ``` ``` kleing@24333 ` 269` ```lemma bl_sbin_sign: ``` huffman@46001 ` 270` ``` "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)" ``` kleing@24333 ` 271` ``` unfolding bin_to_bl_def by (rule bl_sbin_sign_aux) ``` kleing@24333 ` 272` huffman@45997 ` 273` ```lemma bin_nth_of_bl_aux: ``` huffman@45997 ` 274` ``` "bin_nth (bl_to_bin_aux bl w) n = ``` kleing@24333 ` 275` ``` (n < size bl & rev bl ! n | n >= length bl & bin_nth w (n - size bl))" ``` huffman@45997 ` 276` ``` apply (induct bl arbitrary: w) ``` kleing@24333 ` 277` ``` apply clarsimp ``` kleing@24333 ` 278` ``` apply clarsimp ``` huffman@45997 ` 279` ``` apply (cut_tac x=n and y="size bl" in linorder_less_linear) ``` kleing@24333 ` 280` ``` apply (erule disjE, simp add: nth_append)+ ``` haftmann@26557 ` 281` ``` apply auto ``` kleing@24333 ` 282` ``` done ``` kleing@24333 ` 283` huffman@45475 ` 284` ```lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl & rev bl ! n)" ``` kleing@24333 ` 285` ``` unfolding bl_to_bin_def by (simp add : bin_nth_of_bl_aux) ``` kleing@24333 ` 286` huffman@45997 ` 287` ```lemma bin_nth_bl: "n < m \ bin_nth w n = nth (rev (bin_to_bl m w)) n" ``` huffman@45997 ` 288` ``` apply (induct n arbitrary: m w) ``` kleing@24333 ` 289` ``` apply clarsimp ``` kleing@24333 ` 290` ``` apply (case_tac m, clarsimp) ``` kleing@24333 ` 291` ``` apply (clarsimp simp: bin_to_bl_def) ``` kleing@24333 ` 292` ``` apply (simp add: bin_to_bl_aux_alt) ``` kleing@24333 ` 293` ``` apply clarsimp ``` kleing@24333 ` 294` ``` apply (case_tac m, clarsimp) ``` kleing@24333 ` 295` ``` apply (clarsimp simp: bin_to_bl_def) ``` kleing@24333 ` 296` ``` apply (simp add: bin_to_bl_aux_alt) ``` kleing@24333 ` 297` ``` done ``` kleing@24333 ` 298` huffman@45997 ` 299` ```lemma nth_rev: ``` huffman@45997 ` 300` ``` "n < length xs \ rev xs ! n = xs ! (length xs - 1 - n)" ``` huffman@45997 ` 301` ``` apply (induct xs) ``` huffman@24465 ` 302` ``` apply simp ``` nipkow@63648 ` 303` ``` apply (clarsimp simp add : nth_append nth.simps split: nat.split) ``` huffman@45997 ` 304` ``` apply (rule_tac f = "\n. xs ! n" in arg_cong) ``` huffman@24465 ` 305` ``` apply arith ``` huffman@24465 ` 306` ``` done ``` huffman@24465 ` 307` huffman@45854 ` 308` ```lemma nth_rev_alt: "n < length ys \ ys ! n = rev ys ! (length ys - Suc n)" ``` huffman@45854 ` 309` ``` by (simp add: nth_rev) ``` huffman@24465 ` 310` huffman@45997 ` 311` ```lemma nth_bin_to_bl_aux: ``` huffman@45997 ` 312` ``` "n < m + length bl \ (bin_to_bl_aux m w bl) ! n = ``` kleing@24333 ` 313` ``` (if n < m then bin_nth w (m - 1 - n) else bl ! (n - m))" ``` huffman@45997 ` 314` ``` apply (induct m arbitrary: w n bl) ``` kleing@24333 ` 315` ``` apply clarsimp ``` kleing@24333 ` 316` ``` apply clarsimp ``` kleing@24333 ` 317` ``` apply (case_tac w rule: bin_exhaust) ``` kleing@24333 ` 318` ``` apply simp ``` kleing@24333 ` 319` ``` done ``` huffman@45997 ` 320` kleing@24333 ` 321` ```lemma nth_bin_to_bl: "n < m ==> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)" ``` kleing@24333 ` 322` ``` unfolding bin_to_bl_def by (simp add : nth_bin_to_bl_aux) ``` kleing@24333 ` 323` huffman@45997 ` 324` ```lemma bl_to_bin_lt2p_aux: ``` huffman@45997 ` 325` ``` "bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)" ``` huffman@45997 ` 326` ``` apply (induct bs arbitrary: w) ``` kleing@24333 ` 327` ``` apply clarsimp ``` kleing@24333 ` 328` ``` apply clarsimp ``` haftmann@53062 ` 329` ``` apply (drule meta_spec, erule xtrans(8) [rotated], simp add: Bit_def)+ ``` kleing@24333 ` 330` ``` done ``` kleing@24333 ` 331` kleing@62701 ` 332` ```lemma bl_to_bin_lt2p_drop: ``` kleing@62701 ` 333` ``` "bl_to_bin bs < 2 ^ length (dropWhile Not bs)" ``` kleing@62701 ` 334` ```proof (induct bs) ``` kleing@62701 ` 335` ``` case (Cons b bs) with bl_to_bin_lt2p_aux[where w=1] ``` kleing@62701 ` 336` ``` show ?case unfolding bl_to_bin_def by simp ``` kleing@62701 ` 337` ```qed simp ``` kleing@62701 ` 338` kleing@62701 ` 339` ```lemma bl_to_bin_lt2p: "bl_to_bin bs < 2 ^ length bs" ``` kleing@62701 ` 340` ``` by (metis bin_bl_bin bintr_lt2p bl_bin_bl) ``` kleing@24333 ` 341` huffman@45997 ` 342` ```lemma bl_to_bin_ge2p_aux: ``` huffman@45997 ` 343` ``` "bl_to_bin_aux bs w >= w * (2 ^ length bs)" ``` huffman@45997 ` 344` ``` apply (induct bs arbitrary: w) ``` kleing@24333 ` 345` ``` apply clarsimp ``` kleing@24333 ` 346` ``` apply clarsimp ``` huffman@46652 ` 347` ``` apply (drule meta_spec, erule order_trans [rotated], ``` huffman@46652 ` 348` ``` simp add: Bit_B0_2t Bit_B1_2t algebra_simps)+ ``` haftmann@54847 ` 349` ``` apply (simp add: Bit_def) ``` kleing@24333 ` 350` ``` done ``` kleing@24333 ` 351` kleing@24333 ` 352` ```lemma bl_to_bin_ge0: "bl_to_bin bs >= 0" ``` kleing@24333 ` 353` ``` apply (unfold bl_to_bin_def) ``` haftmann@53062 ` 354` ``` apply (rule xtrans(4)) ``` kleing@24333 ` 355` ``` apply (rule bl_to_bin_ge2p_aux) ``` huffman@46617 ` 356` ``` apply simp ``` kleing@24333 ` 357` ``` done ``` kleing@24333 ` 358` kleing@24333 ` 359` ```lemma butlast_rest_bin: ``` kleing@24333 ` 360` ``` "butlast (bin_to_bl n w) = bin_to_bl (n - 1) (bin_rest w)" ``` kleing@24333 ` 361` ``` apply (unfold bin_to_bl_def) ``` kleing@24333 ` 362` ``` apply (cases w rule: bin_exhaust) ``` kleing@24333 ` 363` ``` apply (cases n, clarsimp) ``` kleing@24333 ` 364` ``` apply clarsimp ``` kleing@24333 ` 365` ``` apply (auto simp add: bin_to_bl_aux_alt) ``` kleing@24333 ` 366` ``` done ``` kleing@24333 ` 367` huffman@45854 ` 368` ```lemma butlast_bin_rest: ``` huffman@45854 ` 369` ``` "butlast bl = bin_to_bl (length bl - Suc 0) (bin_rest (bl_to_bin bl))" ``` huffman@45854 ` 370` ``` using butlast_rest_bin [where w="bl_to_bin bl" and n="length bl"] by simp ``` kleing@24333 ` 371` haftmann@26557 ` 372` ```lemma butlast_rest_bl2bin_aux: ``` haftmann@26557 ` 373` ``` "bl ~= [] \ ``` haftmann@26557 ` 374` ``` bl_to_bin_aux (butlast bl) w = bin_rest (bl_to_bin_aux bl w)" ``` haftmann@26557 ` 375` ``` by (induct bl arbitrary: w) auto ``` kleing@24333 ` 376` ``` ``` kleing@24333 ` 377` ```lemma butlast_rest_bl2bin: ``` kleing@24333 ` 378` ``` "bl_to_bin (butlast bl) = bin_rest (bl_to_bin bl)" ``` kleing@24333 ` 379` ``` apply (unfold bl_to_bin_def) ``` kleing@24333 ` 380` ``` apply (cases bl) ``` kleing@24333 ` 381` ``` apply (auto simp add: butlast_rest_bl2bin_aux) ``` kleing@24333 ` 382` ``` done ``` kleing@24333 ` 383` huffman@45997 ` 384` ```lemma trunc_bl2bin_aux: ``` huffman@45997 ` 385` ``` "bintrunc m (bl_to_bin_aux bl w) = ``` haftmann@26557 ` 386` ``` bl_to_bin_aux (drop (length bl - m) bl) (bintrunc (m - length bl) w)" ``` haftmann@53438 ` 387` ```proof (induct bl arbitrary: w) ``` haftmann@53438 ` 388` ``` case Nil show ?case by simp ``` haftmann@53438 ` 389` ```next ``` haftmann@53438 ` 390` ``` case (Cons b bl) show ?case ``` haftmann@53438 ` 391` ``` proof (cases "m - length bl") ``` haftmann@53438 ` 392` ``` case 0 then have "Suc (length bl) - m = Suc (length bl - m)" by simp ``` haftmann@53438 ` 393` ``` with Cons show ?thesis by simp ``` haftmann@53438 ` 394` ``` next ``` haftmann@53438 ` 395` ``` case (Suc n) then have *: "m - Suc (length bl) = n" by simp ``` haftmann@53438 ` 396` ``` with Suc Cons show ?thesis by simp ``` haftmann@53438 ` 397` ``` qed ``` haftmann@53438 ` 398` ```qed ``` kleing@24333 ` 399` kleing@24333 ` 400` ```lemma trunc_bl2bin: ``` kleing@24333 ` 401` ``` "bintrunc m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)" ``` kleing@24333 ` 402` ``` unfolding bl_to_bin_def by (simp add : trunc_bl2bin_aux) ``` kleing@24333 ` 403` ``` ``` huffman@45854 ` 404` ```lemma trunc_bl2bin_len [simp]: ``` huffman@45854 ` 405` ``` "bintrunc (length bl) (bl_to_bin bl) = bl_to_bin bl" ``` huffman@45854 ` 406` ``` by (simp add: trunc_bl2bin) ``` kleing@24333 ` 407` kleing@24333 ` 408` ```lemma bl2bin_drop: ``` kleing@24333 ` 409` ``` "bl_to_bin (drop k bl) = bintrunc (length bl - k) (bl_to_bin bl)" ``` kleing@24333 ` 410` ``` apply (rule trans) ``` kleing@24333 ` 411` ``` prefer 2 ``` kleing@24333 ` 412` ``` apply (rule trunc_bl2bin [symmetric]) ``` kleing@24333 ` 413` ``` apply (cases "k <= length bl") ``` kleing@24333 ` 414` ``` apply auto ``` kleing@24333 ` 415` ``` done ``` kleing@24333 ` 416` huffman@45997 ` 417` ```lemma nth_rest_power_bin: ``` huffman@45997 ` 418` ``` "bin_nth ((bin_rest ^^ k) w) n = bin_nth w (n + k)" ``` huffman@45997 ` 419` ``` apply (induct k arbitrary: n, clarsimp) ``` kleing@24333 ` 420` ``` apply clarsimp ``` kleing@24333 ` 421` ``` apply (simp only: bin_nth.Suc [symmetric] add_Suc) ``` kleing@24333 ` 422` ``` done ``` kleing@24333 ` 423` kleing@24333 ` 424` ```lemma take_rest_power_bin: ``` haftmann@30971 ` 425` ``` "m <= n ==> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest ^^ (n - m)) w)" ``` kleing@24333 ` 426` ``` apply (rule nth_equalityI) ``` kleing@24333 ` 427` ``` apply simp ``` kleing@24333 ` 428` ``` apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin) ``` kleing@24333 ` 429` ``` done ``` kleing@24333 ` 430` huffman@24465 ` 431` ```lemma hd_butlast: "size xs > 1 ==> hd (butlast xs) = hd xs" ``` huffman@24465 ` 432` ``` by (cases xs) auto ``` kleing@24333 ` 433` haftmann@26557 ` 434` ```lemma last_bin_last': ``` haftmann@54847 ` 435` ``` "size xs > 0 \ last xs \ bin_last (bl_to_bin_aux xs w)" ``` haftmann@26557 ` 436` ``` by (induct xs arbitrary: w) auto ``` kleing@24333 ` 437` kleing@24333 ` 438` ```lemma last_bin_last: ``` haftmann@54847 ` 439` ``` "size xs > 0 ==> last xs \ bin_last (bl_to_bin xs)" ``` kleing@24333 ` 440` ``` unfolding bl_to_bin_def by (erule last_bin_last') ``` kleing@24333 ` 441` ``` ``` kleing@24333 ` 442` ```lemma bin_last_last: ``` haftmann@54847 ` 443` ``` "bin_last w \ last (bin_to_bl (Suc n) w)" ``` kleing@24333 ` 444` ``` apply (unfold bin_to_bl_def) ``` kleing@24333 ` 445` ``` apply simp ``` kleing@24333 ` 446` ``` apply (auto simp add: bin_to_bl_aux_alt) ``` kleing@24333 ` 447` ``` done ``` kleing@24333 ` 448` huffman@24465 ` 449` ```(** links between bit-wise operations and operations on bool lists **) ``` huffman@24465 ` 450` ``` ``` huffman@45997 ` 451` ```lemma bl_xor_aux_bin: ``` huffman@45997 ` 452` ``` "map2 (%x y. x ~= y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = ``` haftmann@26557 ` 453` ``` bin_to_bl_aux n (v XOR w) (map2 (%x y. x ~= y) bs cs)" ``` huffman@45997 ` 454` ``` apply (induct n arbitrary: v w bs cs) ``` huffman@45997 ` 455` ``` apply simp ``` huffman@45997 ` 456` ``` apply (case_tac v rule: bin_exhaust) ``` huffman@45997 ` 457` ``` apply (case_tac w rule: bin_exhaust) ``` huffman@45997 ` 458` ``` apply clarsimp ``` huffman@45997 ` 459` ``` apply (case_tac b) ``` haftmann@54847 ` 460` ``` apply auto ``` huffman@45997 ` 461` ``` done ``` huffman@45997 ` 462` huffman@45997 ` 463` ```lemma bl_or_aux_bin: ``` huffman@45997 ` 464` ``` "map2 (op | ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = ``` huffman@45997 ` 465` ``` bin_to_bl_aux n (v OR w) (map2 (op | ) bs cs)" ``` huffman@45997 ` 466` ``` apply (induct n arbitrary: v w bs cs) ``` kleing@24333 ` 467` ``` apply simp ``` kleing@24333 ` 468` ``` apply (case_tac v rule: bin_exhaust) ``` kleing@24333 ` 469` ``` apply (case_tac w rule: bin_exhaust) ``` kleing@24333 ` 470` ``` apply clarsimp ``` kleing@24333 ` 471` ``` done ``` kleing@24333 ` 472` ``` ``` huffman@45997 ` 473` ```lemma bl_and_aux_bin: ``` huffman@45997 ` 474` ``` "map2 (op & ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = ``` haftmann@26557 ` 475` ``` bin_to_bl_aux n (v AND w) (map2 (op & ) bs cs)" ``` huffman@45997 ` 476` ``` apply (induct n arbitrary: v w bs cs) ``` kleing@24333 ` 477` ``` apply simp ``` kleing@24333 ` 478` ``` apply (case_tac v rule: bin_exhaust) ``` kleing@24333 ` 479` ``` apply (case_tac w rule: bin_exhaust) ``` kleing@24333 ` 480` ``` apply clarsimp ``` kleing@24333 ` 481` ``` done ``` kleing@24333 ` 482` ``` ``` huffman@45997 ` 483` ```lemma bl_not_aux_bin: ``` huffman@45997 ` 484` ``` "map Not (bin_to_bl_aux n w cs) = ``` huffman@24353 ` 485` ``` bin_to_bl_aux n (NOT w) (map Not cs)" ``` huffman@45997 ` 486` ``` apply (induct n arbitrary: w cs) ``` kleing@24333 ` 487` ``` apply clarsimp ``` kleing@24333 ` 488` ``` apply clarsimp ``` kleing@24333 ` 489` ``` done ``` kleing@24333 ` 490` huffman@45854 ` 491` ```lemma bl_not_bin: "map Not (bin_to_bl n w) = bin_to_bl n (NOT w)" ``` huffman@45854 ` 492` ``` unfolding bin_to_bl_def by (simp add: bl_not_aux_bin) ``` kleing@24333 ` 493` huffman@45854 ` 494` ```lemma bl_and_bin: ``` huffman@45854 ` 495` ``` "map2 (op \) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)" ``` huffman@45854 ` 496` ``` unfolding bin_to_bl_def by (simp add: bl_and_aux_bin) ``` kleing@24333 ` 497` huffman@45854 ` 498` ```lemma bl_or_bin: ``` huffman@45854 ` 499` ``` "map2 (op \) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)" ``` huffman@45854 ` 500` ``` unfolding bin_to_bl_def by (simp add: bl_or_aux_bin) ``` kleing@24333 ` 501` huffman@45854 ` 502` ```lemma bl_xor_bin: ``` huffman@45854 ` 503` ``` "map2 (\x y. x \ y) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)" ``` huffman@45854 ` 504` ``` unfolding bin_to_bl_def by (simp only: bl_xor_aux_bin map2_Nil) ``` kleing@24333 ` 505` huffman@45997 ` 506` ```lemma drop_bin2bl_aux: ``` huffman@45997 ` 507` ``` "drop m (bin_to_bl_aux n bin bs) = ``` kleing@24333 ` 508` ``` bin_to_bl_aux (n - m) bin (drop (m - n) bs)" ``` huffman@45997 ` 509` ``` apply (induct n arbitrary: m bin bs, clarsimp) ``` kleing@24333 ` 510` ``` apply clarsimp ``` kleing@24333 ` 511` ``` apply (case_tac bin rule: bin_exhaust) ``` kleing@24333 ` 512` ``` apply (case_tac "m <= n", simp) ``` kleing@24333 ` 513` ``` apply (case_tac "m - n", simp) ``` kleing@24333 ` 514` ``` apply simp ``` kleing@24333 ` 515` ``` apply (rule_tac f = "%nat. drop nat bs" in arg_cong) ``` kleing@24333 ` 516` ``` apply simp ``` kleing@24333 ` 517` ``` done ``` kleing@24333 ` 518` kleing@24333 ` 519` ```lemma drop_bin2bl: "drop m (bin_to_bl n bin) = bin_to_bl (n - m) bin" ``` kleing@24333 ` 520` ``` unfolding bin_to_bl_def by (simp add : drop_bin2bl_aux) ``` kleing@24333 ` 521` huffman@45997 ` 522` ```lemma take_bin2bl_lem1: ``` huffman@45997 ` 523` ``` "take m (bin_to_bl_aux m w bs) = bin_to_bl m w" ``` huffman@45997 ` 524` ``` apply (induct m arbitrary: w bs, clarsimp) ``` kleing@24333 ` 525` ``` apply clarsimp ``` kleing@24333 ` 526` ``` apply (simp add: bin_to_bl_aux_alt) ``` kleing@24333 ` 527` ``` apply (simp add: bin_to_bl_def) ``` kleing@24333 ` 528` ``` apply (simp add: bin_to_bl_aux_alt) ``` kleing@24333 ` 529` ``` done ``` kleing@24333 ` 530` huffman@45997 ` 531` ```lemma take_bin2bl_lem: ``` huffman@45997 ` 532` ``` "take m (bin_to_bl_aux (m + n) w bs) = ``` kleing@24333 ` 533` ``` take m (bin_to_bl (m + n) w)" ``` huffman@45997 ` 534` ``` apply (induct n arbitrary: w bs) ``` kleing@24333 ` 535` ``` apply (simp_all (no_asm) add: bin_to_bl_def take_bin2bl_lem1) ``` kleing@24333 ` 536` ``` apply simp ``` kleing@24333 ` 537` ``` done ``` kleing@24333 ` 538` huffman@45997 ` 539` ```lemma bin_split_take: ``` huffman@45997 ` 540` ``` "bin_split n c = (a, b) \ ``` kleing@24333 ` 541` ``` bin_to_bl m a = take m (bin_to_bl (m + n) c)" ``` huffman@45997 ` 542` ``` apply (induct n arbitrary: b c) ``` kleing@24333 ` 543` ``` apply clarsimp ``` haftmann@53062 ` 544` ``` apply (clarsimp simp: Let_def split: prod.split_asm) ``` kleing@24333 ` 545` ``` apply (simp add: bin_to_bl_def) ``` kleing@24333 ` 546` ``` apply (simp add: take_bin2bl_lem) ``` kleing@24333 ` 547` ``` done ``` kleing@24333 ` 548` kleing@24333 ` 549` ```lemma bin_split_take1: ``` kleing@24333 ` 550` ``` "k = m + n ==> bin_split n c = (a, b) ==> ``` kleing@24333 ` 551` ``` bin_to_bl m a = take m (bin_to_bl k c)" ``` kleing@24333 ` 552` ``` by (auto elim: bin_split_take) ``` kleing@24333 ` 553` ``` ``` huffman@45997 ` 554` ```lemma nth_takefill: "m < n \ ``` kleing@24333 ` 555` ``` takefill fill n l ! m = (if m < length l then l ! m else fill)" ``` huffman@45997 ` 556` ``` apply (induct n arbitrary: m l, clarsimp) ``` kleing@24333 ` 557` ``` apply clarsimp ``` kleing@24333 ` 558` ``` apply (case_tac m) ``` kleing@24333 ` 559` ``` apply (simp split: list.split) ``` kleing@24333 ` 560` ``` apply (simp split: list.split) ``` kleing@24333 ` 561` ``` done ``` kleing@24333 ` 562` huffman@45997 ` 563` ```lemma takefill_alt: ``` huffman@45997 ` 564` ``` "takefill fill n l = take n l @ replicate (n - length l) fill" ``` huffman@45997 ` 565` ``` by (induct n arbitrary: l) (auto split: list.split) ``` kleing@24333 ` 566` kleing@24333 ` 567` ```lemma takefill_replicate [simp]: ``` kleing@24333 ` 568` ``` "takefill fill n (replicate m fill) = replicate n fill" ``` kleing@24333 ` 569` ``` by (simp add : takefill_alt replicate_add [symmetric]) ``` kleing@24333 ` 570` huffman@45997 ` 571` ```lemma takefill_le': ``` huffman@45997 ` 572` ``` "n = m + k \ takefill x m (takefill x n l) = takefill x m l" ``` huffman@45997 ` 573` ``` by (induct m arbitrary: l n) (auto split: list.split) ``` kleing@24333 ` 574` kleing@24333 ` 575` ```lemma length_takefill [simp]: "length (takefill fill n l) = n" ``` kleing@24333 ` 576` ``` by (simp add : takefill_alt) ``` kleing@24333 ` 577` kleing@24333 ` 578` ```lemma take_takefill': ``` kleing@24333 ` 579` ``` "!!w n. n = k + m ==> take k (takefill fill n w) = takefill fill k w" ``` nipkow@63648 ` 580` ``` by (induct k) (auto split: list.split) ``` kleing@24333 ` 581` kleing@24333 ` 582` ```lemma drop_takefill: ``` kleing@24333 ` 583` ``` "!!w. drop k (takefill fill (m + k) w) = takefill fill m (drop k w)" ``` nipkow@63648 ` 584` ``` by (induct k) (auto split: list.split) ``` kleing@24333 ` 585` kleing@24333 ` 586` ```lemma takefill_le [simp]: ``` kleing@24333 ` 587` ``` "m \ n \ takefill x m (takefill x n l) = takefill x m l" ``` kleing@24333 ` 588` ``` by (auto simp: le_iff_add takefill_le') ``` kleing@24333 ` 589` kleing@24333 ` 590` ```lemma take_takefill [simp]: ``` kleing@24333 ` 591` ``` "m \ n \ take m (takefill fill n w) = takefill fill m w" ``` kleing@24333 ` 592` ``` by (auto simp: le_iff_add take_takefill') ``` kleing@24333 ` 593` ``` ``` kleing@24333 ` 594` ```lemma takefill_append: ``` kleing@24333 ` 595` ``` "takefill fill (m + length xs) (xs @ w) = xs @ (takefill fill m w)" ``` kleing@24333 ` 596` ``` by (induct xs) auto ``` kleing@24333 ` 597` kleing@24333 ` 598` ```lemma takefill_same': ``` kleing@24333 ` 599` ``` "l = length xs ==> takefill fill l xs = xs" ``` thomas@57492 ` 600` ``` by (induct xs arbitrary: l, auto) ``` kleing@24333 ` 601` ``` ``` kleing@24333 ` 602` ```lemmas takefill_same [simp] = takefill_same' [OF refl] ``` kleing@24333 ` 603` kleing@24333 ` 604` ```lemma takefill_bintrunc: ``` kleing@24333 ` 605` ``` "takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))" ``` kleing@24333 ` 606` ``` apply (rule nth_equalityI) ``` kleing@24333 ` 607` ``` apply simp ``` kleing@24333 ` 608` ``` apply (clarsimp simp: nth_takefill nth_rev nth_bin_to_bl bin_nth_of_bl) ``` kleing@24333 ` 609` ``` done ``` kleing@24333 ` 610` kleing@24333 ` 611` ```lemma bl_bin_bl_rtf: ``` kleing@24333 ` 612` ``` "bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))" ``` kleing@24333 ` 613` ``` by (simp add : takefill_bintrunc) ``` huffman@45854 ` 614` huffman@45854 ` 615` ```lemma bl_bin_bl_rep_drop: ``` huffman@45854 ` 616` ``` "bin_to_bl n (bl_to_bin bl) = ``` huffman@45854 ` 617` ``` replicate (n - length bl) False @ drop (length bl - n) bl" ``` huffman@45854 ` 618` ``` by (simp add: bl_bin_bl_rtf takefill_alt rev_take) ``` kleing@24333 ` 619` kleing@24333 ` 620` ```lemma tf_rev: ``` kleing@24333 ` 621` ``` "n + k = m + length bl ==> takefill x m (rev (takefill y n bl)) = ``` kleing@24333 ` 622` ``` rev (takefill y m (rev (takefill x k (rev bl))))" ``` kleing@24333 ` 623` ``` apply (rule nth_equalityI) ``` kleing@24333 ` 624` ``` apply (auto simp add: nth_takefill nth_rev) ``` kleing@24333 ` 625` ``` apply (rule_tac f = "%n. bl ! n" in arg_cong) ``` kleing@24333 ` 626` ``` apply arith ``` kleing@24333 ` 627` ``` done ``` kleing@24333 ` 628` kleing@24333 ` 629` ```lemma takefill_minus: ``` kleing@24333 ` 630` ``` "0 < n ==> takefill fill (Suc (n - 1)) w = takefill fill n w" ``` kleing@24333 ` 631` ``` by auto ``` kleing@24333 ` 632` kleing@24333 ` 633` ```lemmas takefill_Suc_cases = ``` wenzelm@45604 ` 634` ``` list.cases [THEN takefill.Suc [THEN trans]] ``` kleing@24333 ` 635` kleing@24333 ` 636` ```lemmas takefill_Suc_Nil = takefill_Suc_cases (1) ``` kleing@24333 ` 637` ```lemmas takefill_Suc_Cons = takefill_Suc_cases (2) ``` kleing@24333 ` 638` kleing@24333 ` 639` ```lemmas takefill_minus_simps = takefill_Suc_cases [THEN [2] ``` wenzelm@45604 ` 640` ``` takefill_minus [symmetric, THEN trans]] ``` kleing@24333 ` 641` huffman@47108 ` 642` ```lemma takefill_numeral_Nil [simp]: ``` huffman@47219 ` 643` ``` "takefill fill (numeral k) [] = fill # takefill fill (pred_numeral k) []" ``` huffman@47219 ` 644` ``` by (simp add: numeral_eq_Suc) ``` huffman@47108 ` 645` huffman@47108 ` 646` ```lemma takefill_numeral_Cons [simp]: ``` huffman@47219 ` 647` ``` "takefill fill (numeral k) (x # xs) = x # takefill fill (pred_numeral k) xs" ``` huffman@47219 ` 648` ``` by (simp add: numeral_eq_Suc) ``` kleing@24333 ` 649` kleing@24333 ` 650` ```(* links with function bl_to_bin *) ``` kleing@24333 ` 651` kleing@24333 ` 652` ```lemma bl_to_bin_aux_cat: ``` haftmann@26557 ` 653` ``` "!!nv v. bl_to_bin_aux bs (bin_cat w nv v) = ``` haftmann@26557 ` 654` ``` bin_cat w (nv + length bs) (bl_to_bin_aux bs v)" ``` kleing@24333 ` 655` ``` apply (induct bs) ``` kleing@24333 ` 656` ``` apply simp ``` kleing@24333 ` 657` ``` apply (simp add: bin_cat_Suc_Bit [symmetric] del: bin_cat.simps) ``` kleing@24333 ` 658` ``` done ``` kleing@24333 ` 659` kleing@24333 ` 660` ```lemma bin_to_bl_aux_cat: ``` kleing@24333 ` 661` ``` "!!w bs. bin_to_bl_aux (nv + nw) (bin_cat v nw w) bs = ``` kleing@24333 ` 662` ``` bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)" ``` kleing@24333 ` 663` ``` by (induct nw) auto ``` kleing@24333 ` 664` huffman@45854 ` 665` ```lemma bl_to_bin_aux_alt: ``` huffman@45854 ` 666` ``` "bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)" ``` huffman@46001 ` 667` ``` using bl_to_bin_aux_cat [where nv = "0" and v = "0"] ``` huffman@45854 ` 668` ``` unfolding bl_to_bin_def [symmetric] by simp ``` kleing@24333 ` 669` huffman@45854 ` 670` ```lemma bin_to_bl_cat: ``` huffman@45854 ` 671` ``` "bin_to_bl (nv + nw) (bin_cat v nw w) = ``` huffman@45854 ` 672` ``` bin_to_bl_aux nv v (bin_to_bl nw w)" ``` huffman@45854 ` 673` ``` unfolding bin_to_bl_def by (simp add: bin_to_bl_aux_cat) ``` kleing@24333 ` 674` kleing@24333 ` 675` ```lemmas bl_to_bin_aux_app_cat = ``` kleing@24333 ` 676` ``` trans [OF bl_to_bin_aux_append bl_to_bin_aux_alt] ``` kleing@24333 ` 677` kleing@24333 ` 678` ```lemmas bin_to_bl_aux_cat_app = ``` kleing@24333 ` 679` ``` trans [OF bin_to_bl_aux_cat bin_to_bl_aux_alt] ``` kleing@24333 ` 680` huffman@45854 ` 681` ```lemma bl_to_bin_app_cat: ``` huffman@45854 ` 682` ``` "bl_to_bin (bsa @ bs) = bin_cat (bl_to_bin bsa) (length bs) (bl_to_bin bs)" ``` huffman@45854 ` 683` ``` by (simp only: bl_to_bin_aux_app_cat bl_to_bin_def) ``` kleing@24333 ` 684` huffman@45854 ` 685` ```lemma bin_to_bl_cat_app: ``` huffman@45854 ` 686` ``` "bin_to_bl (n + nw) (bin_cat w nw wa) = bin_to_bl n w @ bin_to_bl nw wa" ``` huffman@45854 ` 687` ``` by (simp only: bin_to_bl_def bin_to_bl_aux_cat_app) ``` kleing@24333 ` 688` kleing@24333 ` 689` ```(* bl_to_bin_app_cat_alt and bl_to_bin_app_cat are easily interderivable *) ``` kleing@24333 ` 690` ```lemma bl_to_bin_app_cat_alt: ``` kleing@24333 ` 691` ``` "bin_cat (bl_to_bin cs) n w = bl_to_bin (cs @ bin_to_bl n w)" ``` kleing@24333 ` 692` ``` by (simp add : bl_to_bin_app_cat) ``` kleing@24333 ` 693` kleing@24333 ` 694` ```lemma mask_lem: "(bl_to_bin (True # replicate n False)) = ``` huffman@46645 ` 695` ``` (bl_to_bin (replicate n True)) + 1" ``` kleing@24333 ` 696` ``` apply (unfold bl_to_bin_def) ``` kleing@24333 ` 697` ``` apply (induct n) ``` huffman@46645 ` 698` ``` apply simp ``` nipkow@31790 ` 699` ``` apply (simp only: Suc_eq_plus1 replicate_add ``` kleing@24333 ` 700` ``` append_Cons [symmetric] bl_to_bin_aux_append) ``` huffman@46645 ` 701` ``` apply (simp add: Bit_B0_2t Bit_B1_2t) ``` kleing@24333 ` 702` ``` done ``` kleing@24333 ` 703` huffman@24465 ` 704` ```(* function bl_of_nth *) ``` kleing@24333 ` 705` ```lemma length_bl_of_nth [simp]: "length (bl_of_nth n f) = n" ``` kleing@24333 ` 706` ``` by (induct n) auto ``` kleing@24333 ` 707` kleing@24333 ` 708` ```lemma nth_bl_of_nth [simp]: ``` kleing@24333 ` 709` ``` "m < n \ rev (bl_of_nth n f) ! m = f m" ``` kleing@24333 ` 710` ``` apply (induct n) ``` kleing@24333 ` 711` ``` apply simp ``` kleing@24333 ` 712` ``` apply (clarsimp simp add : nth_append) ``` kleing@24333 ` 713` ``` apply (rule_tac f = "f" in arg_cong) ``` kleing@24333 ` 714` ``` apply simp ``` kleing@24333 ` 715` ``` done ``` kleing@24333 ` 716` kleing@24333 ` 717` ```lemma bl_of_nth_inj: ``` kleing@24333 ` 718` ``` "(!!k. k < n ==> f k = g k) ==> bl_of_nth n f = bl_of_nth n g" ``` kleing@24333 ` 719` ``` by (induct n) auto ``` kleing@24333 ` 720` huffman@45997 ` 721` ```lemma bl_of_nth_nth_le: ``` huffman@45997 ` 722` ``` "n \ length xs \ bl_of_nth n (nth (rev xs)) = drop (length xs - n) xs" ``` huffman@45997 ` 723` ``` apply (induct n arbitrary: xs, clarsimp) ``` kleing@24333 ` 724` ``` apply clarsimp ``` kleing@24333 ` 725` ``` apply (rule trans [OF _ hd_Cons_tl]) ``` kleing@24333 ` 726` ``` apply (frule Suc_le_lessD) ``` kleing@24333 ` 727` ``` apply (simp add: nth_rev trans [OF drop_Suc drop_tl, symmetric]) ``` kleing@24333 ` 728` ``` apply (subst hd_drop_conv_nth) ``` kleing@24333 ` 729` ``` apply force ``` kleing@24333 ` 730` ``` apply simp_all ``` kleing@24333 ` 731` ``` apply (rule_tac f = "%n. drop n xs" in arg_cong) ``` kleing@24333 ` 732` ``` apply simp ``` kleing@24333 ` 733` ``` done ``` kleing@24333 ` 734` huffman@45854 ` 735` ```lemma bl_of_nth_nth [simp]: "bl_of_nth (length xs) (op ! (rev xs)) = xs" ``` huffman@45854 ` 736` ``` by (simp add: bl_of_nth_nth_le) ``` kleing@24333 ` 737` kleing@24333 ` 738` ```lemma size_rbl_pred: "length (rbl_pred bl) = length bl" ``` kleing@24333 ` 739` ``` by (induct bl) auto ``` kleing@24333 ` 740` kleing@24333 ` 741` ```lemma size_rbl_succ: "length (rbl_succ bl) = length bl" ``` kleing@24333 ` 742` ``` by (induct bl) auto ``` kleing@24333 ` 743` kleing@24333 ` 744` ```lemma size_rbl_add: ``` kleing@24333 ` 745` ``` "!!cl. length (rbl_add bl cl) = length bl" ``` kleing@24333 ` 746` ``` by (induct bl) (auto simp: Let_def size_rbl_succ) ``` kleing@24333 ` 747` kleing@24333 ` 748` ```lemma size_rbl_mult: ``` kleing@24333 ` 749` ``` "!!cl. length (rbl_mult bl cl) = length bl" ``` kleing@24333 ` 750` ``` by (induct bl) (auto simp add : Let_def size_rbl_add) ``` kleing@24333 ` 751` kleing@24333 ` 752` ```lemmas rbl_sizes [simp] = ``` kleing@24333 ` 753` ``` size_rbl_pred size_rbl_succ size_rbl_add size_rbl_mult ``` kleing@24333 ` 754` kleing@24333 ` 755` ```lemmas rbl_Nils = ``` kleing@24333 ` 756` ``` rbl_pred.Nil rbl_succ.Nil rbl_add.Nil rbl_mult.Nil ``` kleing@24333 ` 757` huffman@46653 ` 758` ```lemma rbl_pred: ``` huffman@46653 ` 759` ``` "rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin - 1))" ``` huffman@46653 ` 760` ``` apply (induct n arbitrary: bin, simp) ``` kleing@24333 ` 761` ``` apply (unfold bin_to_bl_def) ``` kleing@24333 ` 762` ``` apply clarsimp ``` kleing@24333 ` 763` ``` apply (case_tac bin rule: bin_exhaust) ``` kleing@24333 ` 764` ``` apply (case_tac b) ``` huffman@46653 ` 765` ``` apply (clarsimp simp: bin_to_bl_aux_alt)+ ``` kleing@24333 ` 766` ``` done ``` kleing@24333 ` 767` kleing@24333 ` 768` ```lemma rbl_succ: ``` huffman@46653 ` 769` ``` "rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))" ``` huffman@46653 ` 770` ``` apply (induct n arbitrary: bin, simp) ``` kleing@24333 ` 771` ``` apply (unfold bin_to_bl_def) ``` kleing@24333 ` 772` ``` apply clarsimp ``` kleing@24333 ` 773` ``` apply (case_tac bin rule: bin_exhaust) ``` kleing@24333 ` 774` ``` apply (case_tac b) ``` huffman@46653 ` 775` ``` apply (clarsimp simp: bin_to_bl_aux_alt)+ ``` kleing@24333 ` 776` ``` done ``` kleing@24333 ` 777` kleing@24333 ` 778` ```lemma rbl_add: ``` kleing@24333 ` 779` ``` "!!bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = ``` kleing@24333 ` 780` ``` rev (bin_to_bl n (bina + binb))" ``` kleing@24333 ` 781` ``` apply (induct n, simp) ``` kleing@24333 ` 782` ``` apply (unfold bin_to_bl_def) ``` kleing@24333 ` 783` ``` apply clarsimp ``` kleing@24333 ` 784` ``` apply (case_tac bina rule: bin_exhaust) ``` kleing@24333 ` 785` ``` apply (case_tac binb rule: bin_exhaust) ``` kleing@24333 ` 786` ``` apply (case_tac b) ``` kleing@24333 ` 787` ``` apply (case_tac [!] "ba") ``` haftmann@57514 ` 788` ``` apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def ac_simps) ``` kleing@24333 ` 789` ``` done ``` kleing@24333 ` 790` kleing@24333 ` 791` ```lemma rbl_add_app2: ``` kleing@24333 ` 792` ``` "!!blb. length blb >= length bla ==> ``` kleing@24333 ` 793` ``` rbl_add bla (blb @ blc) = rbl_add bla blb" ``` kleing@24333 ` 794` ``` apply (induct bla, simp) ``` kleing@24333 ` 795` ``` apply clarsimp ``` kleing@24333 ` 796` ``` apply (case_tac blb, clarsimp) ``` kleing@24333 ` 797` ``` apply (clarsimp simp: Let_def) ``` kleing@24333 ` 798` ``` done ``` kleing@24333 ` 799` kleing@24333 ` 800` ```lemma rbl_add_take2: ``` kleing@24333 ` 801` ``` "!!blb. length blb >= length bla ==> ``` kleing@24333 ` 802` ``` rbl_add bla (take (length bla) blb) = rbl_add bla blb" ``` kleing@24333 ` 803` ``` apply (induct bla, simp) ``` kleing@24333 ` 804` ``` apply clarsimp ``` kleing@24333 ` 805` ``` apply (case_tac blb, clarsimp) ``` kleing@24333 ` 806` ``` apply (clarsimp simp: Let_def) ``` kleing@24333 ` 807` ``` done ``` kleing@24333 ` 808` kleing@24333 ` 809` ```lemma rbl_add_long: ``` kleing@24333 ` 810` ``` "m >= n ==> rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) = ``` kleing@24333 ` 811` ``` rev (bin_to_bl n (bina + binb))" ``` kleing@24333 ` 812` ``` apply (rule box_equals [OF _ rbl_add_take2 rbl_add]) ``` kleing@24333 ` 813` ``` apply (rule_tac f = "rbl_add (rev (bin_to_bl n bina))" in arg_cong) ``` kleing@24333 ` 814` ``` apply (rule rev_swap [THEN iffD1]) ``` kleing@24333 ` 815` ``` apply (simp add: rev_take drop_bin2bl) ``` kleing@24333 ` 816` ``` apply simp ``` kleing@24333 ` 817` ``` done ``` kleing@24333 ` 818` kleing@24333 ` 819` ```lemma rbl_mult_app2: ``` kleing@24333 ` 820` ``` "!!blb. length blb >= length bla ==> ``` kleing@24333 ` 821` ``` rbl_mult bla (blb @ blc) = rbl_mult bla blb" ``` kleing@24333 ` 822` ``` apply (induct bla, simp) ``` kleing@24333 ` 823` ``` apply clarsimp ``` kleing@24333 ` 824` ``` apply (case_tac blb, clarsimp) ``` kleing@24333 ` 825` ``` apply (clarsimp simp: Let_def rbl_add_app2) ``` kleing@24333 ` 826` ``` done ``` kleing@24333 ` 827` kleing@24333 ` 828` ```lemma rbl_mult_take2: ``` kleing@24333 ` 829` ``` "length blb >= length bla ==> ``` kleing@24333 ` 830` ``` rbl_mult bla (take (length bla) blb) = rbl_mult bla blb" ``` kleing@24333 ` 831` ``` apply (rule trans) ``` kleing@24333 ` 832` ``` apply (rule rbl_mult_app2 [symmetric]) ``` kleing@24333 ` 833` ``` apply simp ``` kleing@24333 ` 834` ``` apply (rule_tac f = "rbl_mult bla" in arg_cong) ``` kleing@24333 ` 835` ``` apply (rule append_take_drop_id) ``` kleing@24333 ` 836` ``` done ``` kleing@24333 ` 837` ``` ``` kleing@24333 ` 838` ```lemma rbl_mult_gt1: ``` kleing@24333 ` 839` ``` "m >= length bl ==> rbl_mult bl (rev (bin_to_bl m binb)) = ``` kleing@24333 ` 840` ``` rbl_mult bl (rev (bin_to_bl (length bl) binb))" ``` kleing@24333 ` 841` ``` apply (rule trans) ``` kleing@24333 ` 842` ``` apply (rule rbl_mult_take2 [symmetric]) ``` kleing@24333 ` 843` ``` apply simp_all ``` kleing@24333 ` 844` ``` apply (rule_tac f = "rbl_mult bl" in arg_cong) ``` kleing@24333 ` 845` ``` apply (rule rev_swap [THEN iffD1]) ``` kleing@24333 ` 846` ``` apply (simp add: rev_take drop_bin2bl) ``` kleing@24333 ` 847` ``` done ``` kleing@24333 ` 848` ``` ``` kleing@24333 ` 849` ```lemma rbl_mult_gt: ``` kleing@24333 ` 850` ``` "m > n ==> rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) = ``` kleing@24333 ` 851` ``` rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb))" ``` kleing@24333 ` 852` ``` by (auto intro: trans [OF rbl_mult_gt1]) ``` kleing@24333 ` 853` ``` ``` kleing@24333 ` 854` ```lemmas rbl_mult_Suc = lessI [THEN rbl_mult_gt] ``` kleing@24333 ` 855` kleing@24333 ` 856` ```lemma rbbl_Cons: ``` haftmann@54847 ` 857` ``` "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (x BIT b))" ``` kleing@24333 ` 858` ``` apply (unfold bin_to_bl_def) ``` kleing@24333 ` 859` ``` apply simp ``` kleing@24333 ` 860` ``` apply (simp add: bin_to_bl_aux_alt) ``` kleing@24333 ` 861` ``` done ``` huffman@46653 ` 862` kleing@24333 ` 863` ```lemma rbl_mult: "!!bina binb. ``` kleing@24333 ` 864` ``` rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = ``` kleing@24333 ` 865` ``` rev (bin_to_bl n (bina * binb))" ``` kleing@24333 ` 866` ``` apply (induct n) ``` kleing@24333 ` 867` ``` apply simp ``` kleing@24333 ` 868` ``` apply (unfold bin_to_bl_def) ``` kleing@24333 ` 869` ``` apply clarsimp ``` kleing@24333 ` 870` ``` apply (case_tac bina rule: bin_exhaust) ``` kleing@24333 ` 871` ``` apply (case_tac binb rule: bin_exhaust) ``` kleing@24333 ` 872` ``` apply (case_tac b) ``` kleing@24333 ` 873` ``` apply (case_tac [!] "ba") ``` huffman@46653 ` 874` ``` apply (auto simp: bin_to_bl_aux_alt Let_def) ``` huffman@46653 ` 875` ``` apply (auto simp: rbbl_Cons rbl_mult_Suc rbl_add) ``` kleing@24333 ` 876` ``` done ``` kleing@24333 ` 877` kleing@24333 ` 878` ```lemma rbl_add_split: ``` kleing@24333 ` 879` ``` "P (rbl_add (y # ys) (x # xs)) = ``` kleing@24333 ` 880` ``` (ALL ws. length ws = length ys --> ws = rbl_add ys xs --> ``` wenzelm@26008 ` 881` ``` (y --> ((x --> P (False # rbl_succ ws)) & (~ x --> P (True # ws)))) & ``` kleing@24333 ` 882` ``` (~ y --> P (x # ws)))" ``` kleing@24333 ` 883` ``` apply (auto simp add: Let_def) ``` kleing@24333 ` 884` ``` apply (case_tac [!] "y") ``` kleing@24333 ` 885` ``` apply auto ``` kleing@24333 ` 886` ``` done ``` kleing@24333 ` 887` kleing@24333 ` 888` ```lemma rbl_mult_split: ``` kleing@24333 ` 889` ``` "P (rbl_mult (y # ys) xs) = ``` kleing@24333 ` 890` ``` (ALL ws. length ws = Suc (length ys) --> ws = False # rbl_mult ys xs --> ``` kleing@24333 ` 891` ``` (y --> P (rbl_add ws xs)) & (~ y --> P ws))" ``` kleing@24333 ` 892` ``` by (clarsimp simp add : Let_def) ``` kleing@24333 ` 893` ``` ``` kleing@24333 ` 894` huffman@24350 ` 895` ```subsection "Repeated splitting or concatenation" ``` kleing@24333 ` 896` kleing@24333 ` 897` ```lemma sclem: ``` kleing@24333 ` 898` ``` "size (concat (map (bin_to_bl n) xs)) = length xs * n" ``` kleing@24333 ` 899` ``` by (induct xs) auto ``` kleing@24333 ` 900` huffman@45997 ` 901` ```lemma bin_cat_foldl_lem: ``` huffman@45997 ` 902` ``` "foldl (%u. bin_cat u n) x xs = ``` kleing@24333 ` 903` ``` bin_cat x (size xs * n) (foldl (%u. bin_cat u n) y xs)" ``` huffman@45997 ` 904` ``` apply (induct xs arbitrary: x) ``` kleing@24333 ` 905` ``` apply simp ``` kleing@24333 ` 906` ``` apply (simp (no_asm)) ``` kleing@24333 ` 907` ``` apply (frule asm_rl) ``` huffman@45997 ` 908` ``` apply (drule meta_spec) ``` kleing@24333 ` 909` ``` apply (erule trans) ``` huffman@45997 ` 910` ``` apply (drule_tac x = "bin_cat y n a" in meta_spec) ``` haftmann@54863 ` 911` ``` apply (simp add : bin_cat_assoc_sym min.absorb2) ``` kleing@24333 ` 912` ``` done ``` kleing@24333 ` 913` kleing@24333 ` 914` ```lemma bin_rcat_bl: ``` kleing@24333 ` 915` ``` "(bin_rcat n wl) = bl_to_bin (concat (map (bin_to_bl n) wl))" ``` kleing@24333 ` 916` ``` apply (unfold bin_rcat_def) ``` kleing@24333 ` 917` ``` apply (rule sym) ``` kleing@24333 ` 918` ``` apply (induct wl) ``` kleing@24333 ` 919` ``` apply (auto simp add : bl_to_bin_append) ``` kleing@24333 ` 920` ``` apply (simp add : bl_to_bin_aux_alt sclem) ``` kleing@24333 ` 921` ``` apply (simp add : bin_cat_foldl_lem [symmetric]) ``` kleing@24333 ` 922` ``` done ``` kleing@24333 ` 923` kleing@24333 ` 924` ```lemmas bin_rsplit_aux_simps = bin_rsplit_aux.simps bin_rsplitl_aux.simps ``` kleing@24333 ` 925` ```lemmas rsplit_aux_simps = bin_rsplit_aux_simps ``` kleing@24333 ` 926` nipkow@62390 ` 927` ```lemmas th_if_simp1 = if_split [where P = "op = l", THEN iffD1, THEN conjunct1, THEN mp] for l ``` nipkow@62390 ` 928` ```lemmas th_if_simp2 = if_split [where P = "op = l", THEN iffD1, THEN conjunct2, THEN mp] for l ``` kleing@24333 ` 929` kleing@24333 ` 930` ```lemmas rsplit_aux_simp1s = rsplit_aux_simps [THEN th_if_simp1] ``` kleing@24333 ` 931` kleing@24333 ` 932` ```lemmas rsplit_aux_simp2ls = rsplit_aux_simps [THEN th_if_simp2] ``` kleing@24333 ` 933` ```(* these safe to [simp add] as require calculating m - n *) ``` kleing@24333 ` 934` ```lemmas bin_rsplit_aux_simp2s [simp] = rsplit_aux_simp2ls [unfolded Let_def] ``` kleing@24333 ` 935` ```lemmas rbscl = bin_rsplit_aux_simp2s (2) ``` kleing@24333 ` 936` kleing@24333 ` 937` ```lemmas rsplit_aux_0_simps [simp] = ``` kleing@24333 ` 938` ``` rsplit_aux_simp1s [OF disjI1] rsplit_aux_simp1s [OF disjI2] ``` kleing@24333 ` 939` kleing@24333 ` 940` ```lemma bin_rsplit_aux_append: ``` haftmann@26557 ` 941` ``` "bin_rsplit_aux n m c (bs @ cs) = bin_rsplit_aux n m c bs @ cs" ``` haftmann@26557 ` 942` ``` apply (induct n m c bs rule: bin_rsplit_aux.induct) ``` kleing@24333 ` 943` ``` apply (subst bin_rsplit_aux.simps) ``` kleing@24333 ` 944` ``` apply (subst bin_rsplit_aux.simps) ``` haftmann@53062 ` 945` ``` apply (clarsimp split: prod.split) ``` kleing@24333 ` 946` ``` done ``` kleing@24333 ` 947` kleing@24333 ` 948` ```lemma bin_rsplitl_aux_append: ``` haftmann@26557 ` 949` ``` "bin_rsplitl_aux n m c (bs @ cs) = bin_rsplitl_aux n m c bs @ cs" ``` haftmann@26557 ` 950` ``` apply (induct n m c bs rule: bin_rsplitl_aux.induct) ``` kleing@24333 ` 951` ``` apply (subst bin_rsplitl_aux.simps) ``` kleing@24333 ` 952` ``` apply (subst bin_rsplitl_aux.simps) ``` haftmann@53062 ` 953` ``` apply (clarsimp split: prod.split) ``` kleing@24333 ` 954` ``` done ``` kleing@24333 ` 955` kleing@24333 ` 956` ```lemmas rsplit_aux_apps [where bs = "[]"] = ``` kleing@24333 ` 957` ``` bin_rsplit_aux_append bin_rsplitl_aux_append ``` kleing@24333 ` 958` kleing@24333 ` 959` ```lemmas rsplit_def_auxs = bin_rsplit_def bin_rsplitl_def ``` kleing@24333 ` 960` kleing@24333 ` 961` ```lemmas rsplit_aux_alts = rsplit_aux_apps ``` kleing@24333 ` 962` ``` [unfolded append_Nil rsplit_def_auxs [symmetric]] ``` kleing@24333 ` 963` kleing@24333 ` 964` ```lemma bin_split_minus: "0 < n ==> bin_split (Suc (n - 1)) w = bin_split n w" ``` kleing@24333 ` 965` ``` by auto ``` kleing@24333 ` 966` kleing@24333 ` 967` ```lemmas bin_split_minus_simp = ``` wenzelm@45604 ` 968` ``` bin_split.Suc [THEN [2] bin_split_minus [symmetric, THEN trans]] ``` kleing@24333 ` 969` kleing@24333 ` 970` ```lemma bin_split_pred_simp [simp]: ``` huffman@47108 ` 971` ``` "(0::nat) < numeral bin \ ``` huffman@47108 ` 972` ``` bin_split (numeral bin) w = ``` huffman@47108 ` 973` ``` (let (w1, w2) = bin_split (numeral bin - 1) (bin_rest w) ``` kleing@24333 ` 974` ``` in (w1, w2 BIT bin_last w))" ``` huffman@47108 ` 975` ``` by (simp only: bin_split_minus_simp) ``` kleing@24333 ` 976` kleing@24333 ` 977` ```lemma bin_rsplit_aux_simp_alt: ``` haftmann@26557 ` 978` ``` "bin_rsplit_aux n m c bs = ``` kleing@24333 ` 979` ``` (if m = 0 \ n = 0 ``` kleing@24333 ` 980` ``` then bs ``` kleing@24333 ` 981` ``` else let (a, b) = bin_split n c in bin_rsplit n (m - n, a) @ b # bs)" ``` haftmann@26557 ` 982` ``` unfolding bin_rsplit_aux.simps [of n m c bs] ``` haftmann@26557 ` 983` ``` apply simp ``` haftmann@26557 ` 984` ``` apply (subst rsplit_aux_alts) ``` haftmann@26557 ` 985` ``` apply (simp add: bin_rsplit_def) ``` kleing@24333 ` 986` ``` done ``` kleing@24333 ` 987` kleing@24333 ` 988` ```lemmas bin_rsplit_simp_alt = ``` wenzelm@45604 ` 989` ``` trans [OF bin_rsplit_def bin_rsplit_aux_simp_alt] ``` kleing@24333 ` 990` kleing@24333 ` 991` ```lemmas bthrs = bin_rsplit_simp_alt [THEN [2] trans] ``` kleing@24333 ` 992` kleing@24333 ` 993` ```lemma bin_rsplit_size_sign' [rule_format] : ``` huffman@45997 ` 994` ``` "\n > 0; rev sw = bin_rsplit n (nw, w)\ \ ``` huffman@45997 ` 995` ``` (ALL v: set sw. bintrunc n v = v)" ``` wenzelm@62957 ` 996` ``` apply (induct sw arbitrary: nw w) ``` kleing@24333 ` 997` ``` apply clarsimp ``` kleing@24333 ` 998` ``` apply clarsimp ``` kleing@24333 ` 999` ``` apply (drule bthrs) ``` nipkow@62390 ` 1000` ``` apply (simp (no_asm_use) add: Let_def split: prod.split_asm if_split_asm) ``` kleing@24333 ` 1001` ``` apply clarify ``` kleing@24333 ` 1002` ``` apply (drule split_bintrunc) ``` kleing@24333 ` 1003` ``` apply simp ``` kleing@24333 ` 1004` ``` done ``` kleing@24333 ` 1005` kleing@24333 ` 1006` ```lemmas bin_rsplit_size_sign = bin_rsplit_size_sign' [OF asm_rl ``` wenzelm@45604 ` 1007` ``` rev_rev_ident [THEN trans] set_rev [THEN equalityD2 [THEN subsetD]]] ``` kleing@24333 ` 1008` kleing@24333 ` 1009` ```lemma bin_nth_rsplit [rule_format] : ``` kleing@24333 ` 1010` ``` "n > 0 ==> m < n ==> (ALL w k nw. rev sw = bin_rsplit n (nw, w) --> ``` kleing@24333 ` 1011` ``` k < size sw --> bin_nth (sw ! k) m = bin_nth w (k * n + m))" ``` kleing@24333 ` 1012` ``` apply (induct sw) ``` kleing@24333 ` 1013` ``` apply clarsimp ``` kleing@24333 ` 1014` ``` apply clarsimp ``` kleing@24333 ` 1015` ``` apply (drule bthrs) ``` nipkow@62390 ` 1016` ``` apply (simp (no_asm_use) add: Let_def split: prod.split_asm if_split_asm) ``` kleing@24333 ` 1017` ``` apply clarify ``` kleing@24333 ` 1018` ``` apply (erule allE, erule impE, erule exI) ``` kleing@24333 ` 1019` ``` apply (case_tac k) ``` kleing@24333 ` 1020` ``` apply clarsimp ``` kleing@24333 ` 1021` ``` prefer 2 ``` kleing@24333 ` 1022` ``` apply clarsimp ``` kleing@24333 ` 1023` ``` apply (erule allE) ``` kleing@24333 ` 1024` ``` apply (erule (1) impE) ``` kleing@24333 ` 1025` ``` apply (drule bin_nth_split, erule conjE, erule allE, ``` haftmann@57514 ` 1026` ``` erule trans, simp add : ac_simps)+ ``` kleing@24333 ` 1027` ``` done ``` kleing@24333 ` 1028` kleing@24333 ` 1029` ```lemma bin_rsplit_all: ``` kleing@24333 ` 1030` ``` "0 < nw ==> nw <= n ==> bin_rsplit n (nw, w) = [bintrunc n w]" ``` kleing@24333 ` 1031` ``` unfolding bin_rsplit_def ``` haftmann@53062 ` 1032` ``` by (clarsimp dest!: split_bintrunc simp: rsplit_aux_simp2ls split: prod.split) ``` kleing@24333 ` 1033` kleing@24333 ` 1034` ```lemma bin_rsplit_l [rule_format] : ``` kleing@24333 ` 1035` ``` "ALL bin. bin_rsplitl n (m, bin) = bin_rsplit n (m, bintrunc m bin)" ``` kleing@24333 ` 1036` ``` apply (rule_tac a = "m" in wf_less_than [THEN wf_induct]) ``` kleing@24333 ` 1037` ``` apply (simp (no_asm) add : bin_rsplitl_def bin_rsplit_def) ``` kleing@24333 ` 1038` ``` apply (rule allI) ``` kleing@24333 ` 1039` ``` apply (subst bin_rsplitl_aux.simps) ``` kleing@24333 ` 1040` ``` apply (subst bin_rsplit_aux.simps) ``` haftmann@53062 ` 1041` ``` apply (clarsimp simp: Let_def split: prod.split) ``` kleing@24333 ` 1042` ``` apply (drule bin_split_trunc) ``` kleing@24333 ` 1043` ``` apply (drule sym [THEN trans], assumption) ``` haftmann@26557 ` 1044` ``` apply (subst rsplit_aux_alts(1)) ``` haftmann@26557 ` 1045` ``` apply (subst rsplit_aux_alts(2)) ``` haftmann@26557 ` 1046` ``` apply clarsimp ``` haftmann@26557 ` 1047` ``` unfolding bin_rsplit_def bin_rsplitl_def ``` haftmann@26557 ` 1048` ``` apply simp ``` kleing@24333 ` 1049` ``` done ``` haftmann@26557 ` 1050` kleing@24333 ` 1051` ```lemma bin_rsplit_rcat [rule_format] : ``` kleing@24333 ` 1052` ``` "n > 0 --> bin_rsplit n (n * size ws, bin_rcat n ws) = map (bintrunc n) ws" ``` kleing@24333 ` 1053` ``` apply (unfold bin_rsplit_def bin_rcat_def) ``` kleing@24333 ` 1054` ``` apply (rule_tac xs = "ws" in rev_induct) ``` kleing@24333 ` 1055` ``` apply clarsimp ``` kleing@24333 ` 1056` ``` apply clarsimp ``` haftmann@26557 ` 1057` ``` apply (subst rsplit_aux_alts) ``` haftmann@26557 ` 1058` ``` unfolding bin_split_cat ``` haftmann@26557 ` 1059` ``` apply simp ``` kleing@24333 ` 1060` ``` done ``` kleing@24333 ` 1061` kleing@24333 ` 1062` ```lemma bin_rsplit_aux_len_le [rule_format] : ``` haftmann@26557 ` 1063` ``` "\ws m. n \ 0 \ ws = bin_rsplit_aux n nw w bs \ ``` haftmann@26557 ` 1064` ``` length ws \ m \ nw + length bs * n \ m * n" ``` haftmann@54871 ` 1065` ```proof - ``` haftmann@54871 ` 1066` ``` { fix i j j' k k' m :: nat and R ``` haftmann@54871 ` 1067` ``` assume d: "(i::nat) \ j \ m < j'" ``` haftmann@54871 ` 1068` ``` assume R1: "i * k \ j * k \ R" ``` haftmann@54871 ` 1069` ``` assume R2: "Suc m * k' \ j' * k' \ R" ``` haftmann@54871 ` 1070` ``` have "R" using d ``` haftmann@54871 ` 1071` ``` apply safe ``` haftmann@54871 ` 1072` ``` apply (rule R1, erule mult_le_mono1) ``` haftmann@54871 ` 1073` ``` apply (rule R2, erule Suc_le_eq [THEN iffD2 [THEN mult_le_mono1]]) ``` haftmann@54871 ` 1074` ``` done ``` haftmann@54871 ` 1075` ``` } note A = this ``` haftmann@54871 ` 1076` ``` { fix sc m n lb :: nat ``` haftmann@54871 ` 1077` ``` have "(0::nat) < sc \ sc - n + (n + lb * n) \ m * n \ sc + lb * n \ m * n" ``` haftmann@54871 ` 1078` ``` apply safe ``` haftmann@54871 ` 1079` ``` apply arith ``` haftmann@54871 ` 1080` ``` apply (case_tac "sc >= n") ``` haftmann@54871 ` 1081` ``` apply arith ``` haftmann@54871 ` 1082` ``` apply (insert linorder_le_less_linear [of m lb]) ``` haftmann@54871 ` 1083` ``` apply (erule_tac k2=n and k'2=n in A) ``` haftmann@54871 ` 1084` ``` apply arith ``` haftmann@54871 ` 1085` ``` apply simp ``` haftmann@54871 ` 1086` ``` done ``` haftmann@54871 ` 1087` ``` } note B = this ``` haftmann@54871 ` 1088` ``` show ?thesis ``` haftmann@54871 ` 1089` ``` apply (induct n nw w bs rule: bin_rsplit_aux.induct) ``` haftmann@54871 ` 1090` ``` apply (subst bin_rsplit_aux.simps) ``` haftmann@54871 ` 1091` ``` apply (simp add: B Let_def split: prod.split) ``` haftmann@54871 ` 1092` ``` done ``` haftmann@54871 ` 1093` ```qed ``` kleing@24333 ` 1094` kleing@24333 ` 1095` ```lemma bin_rsplit_len_le: ``` nipkow@25134 ` 1096` ``` "n \ 0 --> ws = bin_rsplit n (nw, w) --> (length ws <= m) = (nw <= m * n)" ``` kleing@24333 ` 1097` ``` unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len_le) ``` kleing@24333 ` 1098` ``` ``` huffman@45997 ` 1099` ```lemma bin_rsplit_aux_len: ``` huffman@45997 ` 1100` ``` "n \ 0 \ length (bin_rsplit_aux n nw w cs) = ``` kleing@24333 ` 1101` ``` (nw + n - 1) div n + length cs" ``` haftmann@26557 ` 1102` ``` apply (induct n nw w cs rule: bin_rsplit_aux.induct) ``` kleing@24333 ` 1103` ``` apply (subst bin_rsplit_aux.simps) ``` haftmann@53062 ` 1104` ``` apply (clarsimp simp: Let_def split: prod.split) ``` kleing@24333 ` 1105` ``` apply (erule thin_rl) ``` haftmann@27651 ` 1106` ``` apply (case_tac m) ``` haftmann@27651 ` 1107` ``` apply simp ``` kleing@24333 ` 1108` ``` apply (case_tac "m <= n") ``` eberlm@63501 ` 1109` ``` apply auto ``` kleing@24333 ` 1110` ``` done ``` kleing@24333 ` 1111` kleing@24333 ` 1112` ```lemma bin_rsplit_len: ``` nipkow@25134 ` 1113` ``` "n\0 ==> length (bin_rsplit n (nw, w)) = (nw + n - 1) div n" ``` kleing@24333 ` 1114` ``` unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len) ``` kleing@24333 ` 1115` haftmann@26557 ` 1116` ```lemma bin_rsplit_aux_len_indep: ``` haftmann@26557 ` 1117` ``` "n \ 0 \ length bs = length cs \ ``` haftmann@26557 ` 1118` ``` length (bin_rsplit_aux n nw v bs) = ``` haftmann@26557 ` 1119` ``` length (bin_rsplit_aux n nw w cs)" ``` haftmann@26557 ` 1120` ```proof (induct n nw w cs arbitrary: v bs rule: bin_rsplit_aux.induct) ``` haftmann@26557 ` 1121` ``` case (1 n m w cs v bs) show ?case ``` haftmann@26557 ` 1122` ``` proof (cases "m = 0") ``` wenzelm@61799 ` 1123` ``` case True then show ?thesis using \length bs = length cs\ by simp ``` haftmann@26557 ` 1124` ``` next ``` haftmann@26557 ` 1125` ``` case False ``` wenzelm@61799 ` 1126` ``` from "1.hyps" \m \ 0\ \n \ 0\ have hyp: "\v bs. length bs = Suc (length cs) \ ``` haftmann@26557 ` 1127` ``` length (bin_rsplit_aux n (m - n) v bs) = ``` haftmann@26557 ` 1128` ``` length (bin_rsplit_aux n (m - n) (fst (bin_split n w)) (snd (bin_split n w) # cs))" ``` haftmann@26557 ` 1129` ``` by auto ``` wenzelm@61799 ` 1130` ``` show ?thesis using \length bs = length cs\ \n \ 0\ ``` haftmann@26557 ` 1131` ``` by (auto simp add: bin_rsplit_aux_simp_alt Let_def bin_rsplit_len ``` haftmann@53062 ` 1132` ``` split: prod.split) ``` haftmann@26557 ` 1133` ``` qed ``` haftmann@26557 ` 1134` ```qed ``` kleing@24333 ` 1135` kleing@24333 ` 1136` ```lemma bin_rsplit_len_indep: ``` nipkow@25134 ` 1137` ``` "n\0 ==> length (bin_rsplit n (nw, v)) = length (bin_rsplit n (nw, w))" ``` kleing@24333 ` 1138` ``` apply (unfold bin_rsplit_def) ``` haftmann@26557 ` 1139` ``` apply (simp (no_asm)) ``` kleing@24333 ` 1140` ``` apply (erule bin_rsplit_aux_len_indep) ``` kleing@24333 ` 1141` ``` apply (rule refl) ``` kleing@24333 ` 1142` ``` done ``` kleing@24333 ` 1143` haftmann@54874 ` 1144` wenzelm@61799 ` 1145` ```text \Even more bit operations\ ``` haftmann@54874 ` 1146` haftmann@54874 ` 1147` ```instantiation int :: bitss ``` haftmann@54874 ` 1148` ```begin ``` haftmann@54874 ` 1149` haftmann@54874 ` 1150` ```definition [iff]: ``` haftmann@54874 ` 1151` ``` "i !! n \ bin_nth i n" ``` haftmann@54874 ` 1152` haftmann@54874 ` 1153` ```definition ``` haftmann@54874 ` 1154` ``` "lsb i = (i :: int) !! 0" ``` haftmann@54874 ` 1155` haftmann@54874 ` 1156` ```definition ``` haftmann@54874 ` 1157` ``` "set_bit i n b = bin_sc n b i" ``` haftmann@54874 ` 1158` haftmann@54874 ` 1159` ```definition ``` haftmann@54874 ` 1160` ``` "set_bits f = ``` haftmann@54874 ` 1161` ``` (if \n. \n'\n. \ f n' then ``` haftmann@54874 ` 1162` ``` let n = LEAST n. \n'\n. \ f n' ``` haftmann@54874 ` 1163` ``` in bl_to_bin (rev (map f [0..n. \n'\n. f n' then ``` haftmann@54874 ` 1165` ``` let n = LEAST n. \n'\n. f n' ``` haftmann@54874 ` 1166` ``` in sbintrunc n (bl_to_bin (True # rev (map f [0.. (x :: int) < 0" ``` haftmann@54874 ` 1177` haftmann@54874 ` 1178` ```instance .. ``` haftmann@54874 ` 1179` kleing@24333 ` 1180` ```end ``` haftmann@54874 ` 1181` haftmann@54874 ` 1182` ```end ```