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