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