src/HOL/Word/BinOperations.thy
 author nipkow Fri Mar 06 17:38:47 2009 +0100 (2009-03-06) changeset 30313 b2441b0c8d38 parent 29631 3aa049e5f156 child 30943 eb3dbbe971f6 permissions -rw-r--r--
 kleing@24333 ` 1` ```(* ``` kleing@24333 ` 2` ``` Author: Jeremy Dawson and Gerwin Klein, NICTA ``` kleing@24333 ` 3` kleing@24333 ` 4` ``` definition and basic theorems for bit-wise logical operations ``` kleing@24333 ` 5` ``` for integers expressed using Pls, Min, BIT, ``` kleing@24333 ` 6` ``` and converting them to and from lists of bools ``` kleing@24333 ` 7` ```*) ``` kleing@24333 ` 8` huffman@24350 ` 9` ```header {* Bitwise Operations on Binary Integers *} ``` huffman@24350 ` 10` haftmann@26558 ` 11` ```theory BinOperations ``` haftmann@26558 ` 12` ```imports BinGeneral BitSyntax ``` kleing@24333 ` 13` ```begin ``` kleing@24333 ` 14` huffman@24364 ` 15` ```subsection {* Logical operations *} ``` huffman@24353 ` 16` huffman@24353 ` 17` ```text "bit-wise logical operations on the int type" ``` huffman@24353 ` 18` haftmann@25762 ` 19` ```instantiation int :: bit ``` haftmann@25762 ` 20` ```begin ``` haftmann@25762 ` 21` haftmann@25762 ` 22` ```definition ``` haftmann@28562 ` 23` ``` int_not_def [code del]: "bitNOT = bin_rec Int.Min Int.Pls ``` huffman@24353 ` 24` ``` (\w b s. s BIT (NOT b))" ``` haftmann@25762 ` 25` haftmann@25762 ` 26` ```definition ``` haftmann@28562 ` 27` ``` int_and_def [code del]: "bitAND = bin_rec (\x. Int.Pls) (\y. y) ``` huffman@24353 ` 28` ``` (\w b s y. s (bin_rest y) BIT (b AND bin_last y))" ``` haftmann@25762 ` 29` haftmann@25762 ` 30` ```definition ``` haftmann@28562 ` 31` ``` int_or_def [code del]: "bitOR = bin_rec (\x. x) (\y. Int.Min) ``` huffman@24353 ` 32` ``` (\w b s y. s (bin_rest y) BIT (b OR bin_last y))" ``` haftmann@25762 ` 33` haftmann@25762 ` 34` ```definition ``` haftmann@28562 ` 35` ``` int_xor_def [code del]: "bitXOR = bin_rec (\x. x) bitNOT ``` huffman@24353 ` 36` ``` (\w b s y. s (bin_rest y) BIT (b XOR bin_last y))" ``` haftmann@25762 ` 37` haftmann@25762 ` 38` ```instance .. ``` haftmann@25762 ` 39` haftmann@25762 ` 40` ```end ``` huffman@24353 ` 41` kleing@24333 ` 42` ```lemma int_not_simps [simp]: ``` haftmann@25919 ` 43` ``` "NOT Int.Pls = Int.Min" ``` haftmann@25919 ` 44` ``` "NOT Int.Min = Int.Pls" ``` huffman@26086 ` 45` ``` "NOT (Int.Bit0 w) = Int.Bit1 (NOT w)" ``` huffman@26086 ` 46` ``` "NOT (Int.Bit1 w) = Int.Bit0 (NOT w)" ``` haftmann@26558 ` 47` ``` "NOT (w BIT b) = (NOT w) BIT (NOT b)" ``` huffman@26086 ` 48` ``` unfolding int_not_def by (simp_all add: bin_rec_simps) ``` kleing@24333 ` 49` haftmann@28562 ` 50` ```declare int_not_simps(1-4) [code] ``` haftmann@26558 ` 51` haftmann@28562 ` 52` ```lemma int_xor_Pls [simp, code]: ``` haftmann@25919 ` 53` ``` "Int.Pls XOR x = x" ``` huffman@24465 ` 54` ``` unfolding int_xor_def by (simp add: bin_rec_PM) ``` kleing@24333 ` 55` haftmann@28562 ` 56` ```lemma int_xor_Min [simp, code]: ``` haftmann@25919 ` 57` ``` "Int.Min XOR x = NOT x" ``` huffman@24465 ` 58` ``` unfolding int_xor_def by (simp add: bin_rec_PM) ``` kleing@24333 ` 59` kleing@24333 ` 60` ```lemma int_xor_Bits [simp]: ``` huffman@24353 ` 61` ``` "(x BIT b) XOR (y BIT c) = (x XOR y) BIT (b XOR c)" ``` kleing@24333 ` 62` ``` apply (unfold int_xor_def) ``` kleing@24333 ` 63` ``` apply (rule bin_rec_simps (1) [THEN fun_cong, THEN trans]) ``` kleing@24333 ` 64` ``` apply (rule ext, simp) ``` kleing@24333 ` 65` ``` prefer 2 ``` kleing@24333 ` 66` ``` apply simp ``` kleing@24333 ` 67` ``` apply (rule ext) ``` kleing@24333 ` 68` ``` apply (simp add: int_not_simps [symmetric]) ``` kleing@24333 ` 69` ``` done ``` kleing@24333 ` 70` haftmann@28562 ` 71` ```lemma int_xor_Bits2 [simp, code]: ``` huffman@26086 ` 72` ``` "(Int.Bit0 x) XOR (Int.Bit0 y) = Int.Bit0 (x XOR y)" ``` huffman@26086 ` 73` ``` "(Int.Bit0 x) XOR (Int.Bit1 y) = Int.Bit1 (x XOR y)" ``` huffman@26086 ` 74` ``` "(Int.Bit1 x) XOR (Int.Bit0 y) = Int.Bit1 (x XOR y)" ``` huffman@26086 ` 75` ``` "(Int.Bit1 x) XOR (Int.Bit1 y) = Int.Bit0 (x XOR y)" ``` huffman@26086 ` 76` ``` unfolding BIT_simps [symmetric] int_xor_Bits by simp_all ``` huffman@26086 ` 77` kleing@24333 ` 78` ```lemma int_xor_x_simps': ``` haftmann@25919 ` 79` ``` "w XOR (Int.Pls BIT bit.B0) = w" ``` haftmann@25919 ` 80` ``` "w XOR (Int.Min BIT bit.B1) = NOT w" ``` kleing@24333 ` 81` ``` apply (induct w rule: bin_induct) ``` kleing@24333 ` 82` ``` apply simp_all[4] ``` kleing@24333 ` 83` ``` apply (unfold int_xor_Bits) ``` kleing@24333 ` 84` ``` apply clarsimp+ ``` kleing@24333 ` 85` ``` done ``` kleing@24333 ` 86` haftmann@28562 ` 87` ```lemma int_xor_extra_simps [simp, code]: ``` huffman@26086 ` 88` ``` "w XOR Int.Pls = w" ``` huffman@26086 ` 89` ``` "w XOR Int.Min = NOT w" ``` huffman@26086 ` 90` ``` using int_xor_x_simps' by simp_all ``` kleing@24333 ` 91` haftmann@28562 ` 92` ```lemma int_or_Pls [simp, code]: ``` haftmann@25919 ` 93` ``` "Int.Pls OR x = x" ``` huffman@24465 ` 94` ``` by (unfold int_or_def) (simp add: bin_rec_PM) ``` kleing@24333 ` 95` ``` ``` haftmann@28562 ` 96` ```lemma int_or_Min [simp, code]: ``` haftmann@25919 ` 97` ``` "Int.Min OR x = Int.Min" ``` huffman@24465 ` 98` ``` by (unfold int_or_def) (simp add: bin_rec_PM) ``` kleing@24333 ` 99` kleing@24333 ` 100` ```lemma int_or_Bits [simp]: ``` huffman@24353 ` 101` ``` "(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)" ``` kleing@24333 ` 102` ``` unfolding int_or_def by (simp add: bin_rec_simps) ``` kleing@24333 ` 103` haftmann@28562 ` 104` ```lemma int_or_Bits2 [simp, code]: ``` huffman@26086 ` 105` ``` "(Int.Bit0 x) OR (Int.Bit0 y) = Int.Bit0 (x OR y)" ``` huffman@26086 ` 106` ``` "(Int.Bit0 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)" ``` huffman@26086 ` 107` ``` "(Int.Bit1 x) OR (Int.Bit0 y) = Int.Bit1 (x OR y)" ``` huffman@26086 ` 108` ``` "(Int.Bit1 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)" ``` huffman@26086 ` 109` ``` unfolding BIT_simps [symmetric] int_or_Bits by simp_all ``` huffman@26086 ` 110` kleing@24333 ` 111` ```lemma int_or_x_simps': ``` haftmann@25919 ` 112` ``` "w OR (Int.Pls BIT bit.B0) = w" ``` haftmann@25919 ` 113` ``` "w OR (Int.Min BIT bit.B1) = Int.Min" ``` kleing@24333 ` 114` ``` apply (induct w rule: bin_induct) ``` kleing@24333 ` 115` ``` apply simp_all[4] ``` kleing@24333 ` 116` ``` apply (unfold int_or_Bits) ``` kleing@24333 ` 117` ``` apply clarsimp+ ``` kleing@24333 ` 118` ``` done ``` kleing@24333 ` 119` haftmann@28562 ` 120` ```lemma int_or_extra_simps [simp, code]: ``` huffman@26086 ` 121` ``` "w OR Int.Pls = w" ``` huffman@26086 ` 122` ``` "w OR Int.Min = Int.Min" ``` huffman@26086 ` 123` ``` using int_or_x_simps' by simp_all ``` kleing@24333 ` 124` haftmann@28562 ` 125` ```lemma int_and_Pls [simp, code]: ``` haftmann@25919 ` 126` ``` "Int.Pls AND x = Int.Pls" ``` huffman@24465 ` 127` ``` unfolding int_and_def by (simp add: bin_rec_PM) ``` kleing@24333 ` 128` haftmann@28562 ` 129` ```lemma int_and_Min [simp, code]: ``` haftmann@25919 ` 130` ``` "Int.Min AND x = x" ``` huffman@24465 ` 131` ``` unfolding int_and_def by (simp add: bin_rec_PM) ``` kleing@24333 ` 132` kleing@24333 ` 133` ```lemma int_and_Bits [simp]: ``` huffman@24353 ` 134` ``` "(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)" ``` kleing@24333 ` 135` ``` unfolding int_and_def by (simp add: bin_rec_simps) ``` kleing@24333 ` 136` haftmann@28562 ` 137` ```lemma int_and_Bits2 [simp, code]: ``` huffman@26086 ` 138` ``` "(Int.Bit0 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)" ``` huffman@26086 ` 139` ``` "(Int.Bit0 x) AND (Int.Bit1 y) = Int.Bit0 (x AND y)" ``` huffman@26086 ` 140` ``` "(Int.Bit1 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)" ``` huffman@26086 ` 141` ``` "(Int.Bit1 x) AND (Int.Bit1 y) = Int.Bit1 (x AND y)" ``` huffman@26086 ` 142` ``` unfolding BIT_simps [symmetric] int_and_Bits by simp_all ``` huffman@26086 ` 143` kleing@24333 ` 144` ```lemma int_and_x_simps': ``` haftmann@25919 ` 145` ``` "w AND (Int.Pls BIT bit.B0) = Int.Pls" ``` haftmann@25919 ` 146` ``` "w AND (Int.Min BIT bit.B1) = w" ``` kleing@24333 ` 147` ``` apply (induct w rule: bin_induct) ``` kleing@24333 ` 148` ``` apply simp_all[4] ``` kleing@24333 ` 149` ``` apply (unfold int_and_Bits) ``` kleing@24333 ` 150` ``` apply clarsimp+ ``` kleing@24333 ` 151` ``` done ``` kleing@24333 ` 152` haftmann@28562 ` 153` ```lemma int_and_extra_simps [simp, code]: ``` huffman@26086 ` 154` ``` "w AND Int.Pls = Int.Pls" ``` huffman@26086 ` 155` ``` "w AND Int.Min = w" ``` huffman@26086 ` 156` ``` using int_and_x_simps' by simp_all ``` kleing@24333 ` 157` kleing@24333 ` 158` ```(* commutativity of the above *) ``` kleing@24333 ` 159` ```lemma bin_ops_comm: ``` kleing@24333 ` 160` ``` shows ``` huffman@24353 ` 161` ``` int_and_comm: "!!y::int. x AND y = y AND x" and ``` huffman@24353 ` 162` ``` int_or_comm: "!!y::int. x OR y = y OR x" and ``` huffman@24353 ` 163` ``` int_xor_comm: "!!y::int. x XOR y = y XOR x" ``` kleing@24333 ` 164` ``` apply (induct x rule: bin_induct) ``` kleing@24333 ` 165` ``` apply simp_all[6] ``` kleing@24333 ` 166` ``` apply (case_tac y rule: bin_exhaust, simp add: bit_ops_comm)+ ``` kleing@24333 ` 167` ``` done ``` kleing@24333 ` 168` kleing@24333 ` 169` ```lemma bin_ops_same [simp]: ``` huffman@24353 ` 170` ``` "(x::int) AND x = x" ``` huffman@24353 ` 171` ``` "(x::int) OR x = x" ``` haftmann@25919 ` 172` ``` "(x::int) XOR x = Int.Pls" ``` kleing@24333 ` 173` ``` by (induct x rule: bin_induct) auto ``` kleing@24333 ` 174` huffman@24353 ` 175` ```lemma int_not_not [simp]: "NOT (NOT (x::int)) = x" ``` kleing@24333 ` 176` ``` by (induct x rule: bin_induct) auto ``` kleing@24333 ` 177` kleing@24333 ` 178` ```lemmas bin_log_esimps = ``` kleing@24333 ` 179` ``` int_and_extra_simps int_or_extra_simps int_xor_extra_simps ``` kleing@24333 ` 180` ``` int_and_Pls int_and_Min int_or_Pls int_or_Min int_xor_Pls int_xor_Min ``` kleing@24333 ` 181` kleing@24333 ` 182` ```(* basic properties of logical (bit-wise) operations *) ``` kleing@24333 ` 183` kleing@24333 ` 184` ```lemma bbw_ao_absorb: ``` huffman@24353 ` 185` ``` "!!y::int. x AND (y OR x) = x & x OR (y AND x) = x" ``` kleing@24333 ` 186` ``` apply (induct x rule: bin_induct) ``` kleing@24333 ` 187` ``` apply auto ``` kleing@24333 ` 188` ``` apply (case_tac [!] y rule: bin_exhaust) ``` kleing@24333 ` 189` ``` apply auto ``` kleing@24333 ` 190` ``` apply (case_tac [!] bit) ``` kleing@24333 ` 191` ``` apply auto ``` kleing@24333 ` 192` ``` done ``` kleing@24333 ` 193` kleing@24333 ` 194` ```lemma bbw_ao_absorbs_other: ``` huffman@24353 ` 195` ``` "x AND (x OR y) = x \ (y AND x) OR x = (x::int)" ``` huffman@24353 ` 196` ``` "(y OR x) AND x = x \ x OR (x AND y) = (x::int)" ``` huffman@24353 ` 197` ``` "(x OR y) AND x = x \ (x AND y) OR x = (x::int)" ``` kleing@24333 ` 198` ``` apply (auto simp: bbw_ao_absorb int_or_comm) ``` kleing@24333 ` 199` ``` apply (subst int_or_comm) ``` kleing@24333 ` 200` ``` apply (simp add: bbw_ao_absorb) ``` kleing@24333 ` 201` ``` apply (subst int_and_comm) ``` kleing@24333 ` 202` ``` apply (subst int_or_comm) ``` kleing@24333 ` 203` ``` apply (simp add: bbw_ao_absorb) ``` kleing@24333 ` 204` ``` apply (subst int_and_comm) ``` kleing@24333 ` 205` ``` apply (simp add: bbw_ao_absorb) ``` kleing@24333 ` 206` ``` done ``` huffman@24353 ` 207` kleing@24333 ` 208` ```lemmas bbw_ao_absorbs [simp] = bbw_ao_absorb bbw_ao_absorbs_other ``` kleing@24333 ` 209` kleing@24333 ` 210` ```lemma int_xor_not: ``` huffman@24353 ` 211` ``` "!!y::int. (NOT x) XOR y = NOT (x XOR y) & ``` huffman@24353 ` 212` ``` x XOR (NOT y) = NOT (x XOR y)" ``` kleing@24333 ` 213` ``` apply (induct x rule: bin_induct) ``` kleing@24333 ` 214` ``` apply auto ``` kleing@24333 ` 215` ``` apply (case_tac y rule: bin_exhaust, auto, ``` kleing@24333 ` 216` ``` case_tac b, auto)+ ``` kleing@24333 ` 217` ``` done ``` kleing@24333 ` 218` kleing@24333 ` 219` ```lemma bbw_assocs': ``` huffman@24353 ` 220` ``` "!!y z::int. (x AND y) AND z = x AND (y AND z) & ``` huffman@24353 ` 221` ``` (x OR y) OR z = x OR (y OR z) & ``` huffman@24353 ` 222` ``` (x XOR y) XOR z = x XOR (y XOR z)" ``` kleing@24333 ` 223` ``` apply (induct x rule: bin_induct) ``` kleing@24333 ` 224` ``` apply (auto simp: int_xor_not) ``` kleing@24333 ` 225` ``` apply (case_tac [!] y rule: bin_exhaust) ``` kleing@24333 ` 226` ``` apply (case_tac [!] z rule: bin_exhaust) ``` kleing@24333 ` 227` ``` apply (case_tac [!] bit) ``` kleing@24333 ` 228` ``` apply (case_tac [!] b) ``` huffman@26086 ` 229` ``` apply (auto simp del: BIT_simps) ``` kleing@24333 ` 230` ``` done ``` kleing@24333 ` 231` kleing@24333 ` 232` ```lemma int_and_assoc: ``` huffman@24353 ` 233` ``` "(x AND y) AND (z::int) = x AND (y AND z)" ``` kleing@24333 ` 234` ``` by (simp add: bbw_assocs') ``` kleing@24333 ` 235` kleing@24333 ` 236` ```lemma int_or_assoc: ``` huffman@24353 ` 237` ``` "(x OR y) OR (z::int) = x OR (y OR z)" ``` kleing@24333 ` 238` ``` by (simp add: bbw_assocs') ``` kleing@24333 ` 239` kleing@24333 ` 240` ```lemma int_xor_assoc: ``` huffman@24353 ` 241` ``` "(x XOR y) XOR (z::int) = x XOR (y XOR z)" ``` kleing@24333 ` 242` ``` by (simp add: bbw_assocs') ``` kleing@24333 ` 243` kleing@24333 ` 244` ```lemmas bbw_assocs = int_and_assoc int_or_assoc int_xor_assoc ``` kleing@24333 ` 245` kleing@24333 ` 246` ```lemma bbw_lcs [simp]: ``` huffman@24353 ` 247` ``` "(y::int) AND (x AND z) = x AND (y AND z)" ``` huffman@24353 ` 248` ``` "(y::int) OR (x OR z) = x OR (y OR z)" ``` huffman@24353 ` 249` ``` "(y::int) XOR (x XOR z) = x XOR (y XOR z)" ``` kleing@24333 ` 250` ``` apply (auto simp: bbw_assocs [symmetric]) ``` kleing@24333 ` 251` ``` apply (auto simp: bin_ops_comm) ``` kleing@24333 ` 252` ``` done ``` kleing@24333 ` 253` kleing@24333 ` 254` ```lemma bbw_not_dist: ``` huffman@24353 ` 255` ``` "!!y::int. NOT (x OR y) = (NOT x) AND (NOT y)" ``` huffman@24353 ` 256` ``` "!!y::int. NOT (x AND y) = (NOT x) OR (NOT y)" ``` kleing@24333 ` 257` ``` apply (induct x rule: bin_induct) ``` kleing@24333 ` 258` ``` apply auto ``` kleing@24333 ` 259` ``` apply (case_tac [!] y rule: bin_exhaust) ``` huffman@26086 ` 260` ``` apply (case_tac [!] bit, auto simp del: BIT_simps) ``` kleing@24333 ` 261` ``` done ``` kleing@24333 ` 262` kleing@24333 ` 263` ```lemma bbw_oa_dist: ``` huffman@24353 ` 264` ``` "!!y z::int. (x AND y) OR z = ``` huffman@24353 ` 265` ``` (x OR z) AND (y OR z)" ``` kleing@24333 ` 266` ``` apply (induct x rule: bin_induct) ``` kleing@24333 ` 267` ``` apply auto ``` kleing@24333 ` 268` ``` apply (case_tac y rule: bin_exhaust) ``` kleing@24333 ` 269` ``` apply (case_tac z rule: bin_exhaust) ``` huffman@26086 ` 270` ``` apply (case_tac ba, auto simp del: BIT_simps) ``` kleing@24333 ` 271` ``` done ``` kleing@24333 ` 272` kleing@24333 ` 273` ```lemma bbw_ao_dist: ``` huffman@24353 ` 274` ``` "!!y z::int. (x OR y) AND z = ``` huffman@24353 ` 275` ``` (x AND z) OR (y AND z)" ``` kleing@24333 ` 276` ``` apply (induct x rule: bin_induct) ``` kleing@24333 ` 277` ``` apply auto ``` kleing@24333 ` 278` ``` apply (case_tac y rule: bin_exhaust) ``` kleing@24333 ` 279` ``` apply (case_tac z rule: bin_exhaust) ``` huffman@26086 ` 280` ``` apply (case_tac ba, auto simp del: BIT_simps) ``` kleing@24333 ` 281` ``` done ``` kleing@24333 ` 282` huffman@24367 ` 283` ```(* ``` huffman@24367 ` 284` ```Why were these declared simp??? ``` kleing@24333 ` 285` ```declare bin_ops_comm [simp] bbw_assocs [simp] ``` huffman@24367 ` 286` ```*) ``` kleing@24333 ` 287` kleing@24333 ` 288` ```lemma plus_and_or [rule_format]: ``` huffman@24353 ` 289` ``` "ALL y::int. (x AND y) + (x OR y) = x + y" ``` kleing@24333 ` 290` ``` apply (induct x rule: bin_induct) ``` kleing@24333 ` 291` ``` apply clarsimp ``` kleing@24333 ` 292` ``` apply clarsimp ``` kleing@24333 ` 293` ``` apply clarsimp ``` kleing@24333 ` 294` ``` apply (case_tac y rule: bin_exhaust) ``` kleing@24333 ` 295` ``` apply clarsimp ``` kleing@24333 ` 296` ``` apply (unfold Bit_def) ``` kleing@24333 ` 297` ``` apply clarsimp ``` kleing@24333 ` 298` ``` apply (erule_tac x = "x" in allE) ``` kleing@24333 ` 299` ``` apply (simp split: bit.split) ``` kleing@24333 ` 300` ``` done ``` kleing@24333 ` 301` kleing@24333 ` 302` ```lemma le_int_or: ``` haftmann@25919 ` 303` ``` "!!x. bin_sign y = Int.Pls ==> x <= x OR y" ``` kleing@24333 ` 304` ``` apply (induct y rule: bin_induct) ``` kleing@24333 ` 305` ``` apply clarsimp ``` kleing@24333 ` 306` ``` apply clarsimp ``` kleing@24333 ` 307` ``` apply (case_tac x rule: bin_exhaust) ``` kleing@24333 ` 308` ``` apply (case_tac b) ``` kleing@24333 ` 309` ``` apply (case_tac [!] bit) ``` haftmann@26514 ` 310` ``` apply (auto simp: less_eq_int_code) ``` kleing@24333 ` 311` ``` done ``` kleing@24333 ` 312` kleing@24333 ` 313` ```lemmas int_and_le = ``` kleing@24333 ` 314` ``` xtr3 [OF bbw_ao_absorbs (2) [THEN conjunct2, symmetric] le_int_or] ; ``` kleing@24333 ` 315` huffman@24364 ` 316` ```lemma bin_nth_ops: ``` huffman@24364 ` 317` ``` "!!x y. bin_nth (x AND y) n = (bin_nth x n & bin_nth y n)" ``` huffman@24364 ` 318` ``` "!!x y. bin_nth (x OR y) n = (bin_nth x n | bin_nth y n)" ``` huffman@24364 ` 319` ``` "!!x y. bin_nth (x XOR y) n = (bin_nth x n ~= bin_nth y n)" ``` huffman@24364 ` 320` ``` "!!x. bin_nth (NOT x) n = (~ bin_nth x n)" ``` huffman@24364 ` 321` ``` apply (induct n) ``` huffman@24364 ` 322` ``` apply safe ``` huffman@24364 ` 323` ``` apply (case_tac [!] x rule: bin_exhaust) ``` huffman@26086 ` 324` ``` apply (simp_all del: BIT_simps) ``` huffman@24364 ` 325` ``` apply (case_tac [!] y rule: bin_exhaust) ``` huffman@26086 ` 326` ``` apply (simp_all del: BIT_simps) ``` huffman@24364 ` 327` ``` apply (auto dest: not_B1_is_B0 intro: B1_ass_B0) ``` huffman@24364 ` 328` ``` done ``` huffman@24364 ` 329` huffman@24364 ` 330` ```(* interaction between bit-wise and arithmetic *) ``` huffman@24364 ` 331` ```(* good example of bin_induction *) ``` haftmann@25919 ` 332` ```lemma bin_add_not: "x + NOT x = Int.Min" ``` huffman@24364 ` 333` ``` apply (induct x rule: bin_induct) ``` huffman@24364 ` 334` ``` apply clarsimp ``` huffman@24364 ` 335` ``` apply clarsimp ``` huffman@24364 ` 336` ``` apply (case_tac bit, auto) ``` huffman@24364 ` 337` ``` done ``` huffman@24364 ` 338` huffman@24364 ` 339` ```(* truncating results of bit-wise operations *) ``` huffman@24364 ` 340` ```lemma bin_trunc_ao: ``` huffman@24364 ` 341` ``` "!!x y. (bintrunc n x) AND (bintrunc n y) = bintrunc n (x AND y)" ``` huffman@24364 ` 342` ``` "!!x y. (bintrunc n x) OR (bintrunc n y) = bintrunc n (x OR y)" ``` huffman@24364 ` 343` ``` apply (induct n) ``` huffman@24364 ` 344` ``` apply auto ``` huffman@24364 ` 345` ``` apply (case_tac [!] x rule: bin_exhaust) ``` huffman@24364 ` 346` ``` apply (case_tac [!] y rule: bin_exhaust) ``` huffman@24364 ` 347` ``` apply auto ``` huffman@24364 ` 348` ``` done ``` huffman@24364 ` 349` huffman@24364 ` 350` ```lemma bin_trunc_xor: ``` huffman@24364 ` 351` ``` "!!x y. bintrunc n (bintrunc n x XOR bintrunc n y) = ``` huffman@24364 ` 352` ``` bintrunc n (x XOR y)" ``` huffman@24364 ` 353` ``` apply (induct n) ``` huffman@24364 ` 354` ``` apply auto ``` huffman@24364 ` 355` ``` apply (case_tac [!] x rule: bin_exhaust) ``` huffman@24364 ` 356` ``` apply (case_tac [!] y rule: bin_exhaust) ``` huffman@24364 ` 357` ``` apply auto ``` huffman@24364 ` 358` ``` done ``` huffman@24364 ` 359` huffman@24364 ` 360` ```lemma bin_trunc_not: ``` huffman@24364 ` 361` ``` "!!x. bintrunc n (NOT (bintrunc n x)) = bintrunc n (NOT x)" ``` huffman@24364 ` 362` ``` apply (induct n) ``` huffman@24364 ` 363` ``` apply auto ``` huffman@24364 ` 364` ``` apply (case_tac [!] x rule: bin_exhaust) ``` huffman@24364 ` 365` ``` apply auto ``` huffman@24364 ` 366` ``` done ``` huffman@24364 ` 367` huffman@24364 ` 368` ```(* want theorems of the form of bin_trunc_xor *) ``` huffman@24364 ` 369` ```lemma bintr_bintr_i: ``` huffman@24364 ` 370` ``` "x = bintrunc n y ==> bintrunc n x = bintrunc n y" ``` huffman@24364 ` 371` ``` by auto ``` huffman@24364 ` 372` huffman@24364 ` 373` ```lemmas bin_trunc_and = bin_trunc_ao(1) [THEN bintr_bintr_i] ``` huffman@24364 ` 374` ```lemmas bin_trunc_or = bin_trunc_ao(2) [THEN bintr_bintr_i] ``` huffman@24364 ` 375` huffman@24364 ` 376` ```subsection {* Setting and clearing bits *} ``` huffman@24364 ` 377` haftmann@26558 ` 378` ```primrec ``` huffman@24364 ` 379` ``` bin_sc :: "nat => bit => int => int" ``` haftmann@26558 ` 380` ```where ``` haftmann@26558 ` 381` ``` Z: "bin_sc 0 b w = bin_rest w BIT b" ``` haftmann@26558 ` 382` ``` | Suc: "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w" ``` huffman@24364 ` 383` kleing@24333 ` 384` ```(** nth bit, set/clear **) ``` kleing@24333 ` 385` kleing@24333 ` 386` ```lemma bin_nth_sc [simp]: ``` kleing@24333 ` 387` ``` "!!w. bin_nth (bin_sc n b w) n = (b = bit.B1)" ``` kleing@24333 ` 388` ``` by (induct n) auto ``` kleing@24333 ` 389` kleing@24333 ` 390` ```lemma bin_sc_sc_same [simp]: ``` kleing@24333 ` 391` ``` "!!w. bin_sc n c (bin_sc n b w) = bin_sc n c w" ``` kleing@24333 ` 392` ``` by (induct n) auto ``` kleing@24333 ` 393` kleing@24333 ` 394` ```lemma bin_sc_sc_diff: ``` kleing@24333 ` 395` ``` "!!w m. m ~= n ==> ``` kleing@24333 ` 396` ``` bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)" ``` kleing@24333 ` 397` ``` apply (induct n) ``` kleing@24333 ` 398` ``` apply (case_tac [!] m) ``` kleing@24333 ` 399` ``` apply auto ``` kleing@24333 ` 400` ``` done ``` kleing@24333 ` 401` kleing@24333 ` 402` ```lemma bin_nth_sc_gen: ``` kleing@24333 ` 403` ``` "!!w m. bin_nth (bin_sc n b w) m = (if m = n then b = bit.B1 else bin_nth w m)" ``` kleing@24333 ` 404` ``` by (induct n) (case_tac [!] m, auto) ``` kleing@24333 ` 405` ``` ``` kleing@24333 ` 406` ```lemma bin_sc_nth [simp]: ``` kleing@24333 ` 407` ``` "!!w. (bin_sc n (If (bin_nth w n) bit.B1 bit.B0) w) = w" ``` huffman@24465 ` 408` ``` by (induct n) auto ``` kleing@24333 ` 409` kleing@24333 ` 410` ```lemma bin_sign_sc [simp]: ``` kleing@24333 ` 411` ``` "!!w. bin_sign (bin_sc n b w) = bin_sign w" ``` kleing@24333 ` 412` ``` by (induct n) auto ``` kleing@24333 ` 413` ``` ``` kleing@24333 ` 414` ```lemma bin_sc_bintr [simp]: ``` kleing@24333 ` 415` ``` "!!w m. bintrunc m (bin_sc n x (bintrunc m (w))) = bintrunc m (bin_sc n x w)" ``` kleing@24333 ` 416` ``` apply (induct n) ``` kleing@24333 ` 417` ``` apply (case_tac [!] w rule: bin_exhaust) ``` kleing@24333 ` 418` ``` apply (case_tac [!] m, auto) ``` kleing@24333 ` 419` ``` done ``` kleing@24333 ` 420` kleing@24333 ` 421` ```lemma bin_clr_le: ``` kleing@24333 ` 422` ``` "!!w. bin_sc n bit.B0 w <= w" ``` kleing@24333 ` 423` ``` apply (induct n) ``` kleing@24333 ` 424` ``` apply (case_tac [!] w rule: bin_exhaust) ``` huffman@26086 ` 425` ``` apply (auto simp del: BIT_simps) ``` kleing@24333 ` 426` ``` apply (unfold Bit_def) ``` kleing@24333 ` 427` ``` apply (simp_all split: bit.split) ``` kleing@24333 ` 428` ``` done ``` kleing@24333 ` 429` kleing@24333 ` 430` ```lemma bin_set_ge: ``` kleing@24333 ` 431` ``` "!!w. bin_sc n bit.B1 w >= w" ``` kleing@24333 ` 432` ``` apply (induct n) ``` kleing@24333 ` 433` ``` apply (case_tac [!] w rule: bin_exhaust) ``` huffman@26086 ` 434` ``` apply (auto simp del: BIT_simps) ``` kleing@24333 ` 435` ``` apply (unfold Bit_def) ``` kleing@24333 ` 436` ``` apply (simp_all split: bit.split) ``` kleing@24333 ` 437` ``` done ``` kleing@24333 ` 438` kleing@24333 ` 439` ```lemma bintr_bin_clr_le: ``` kleing@24333 ` 440` ``` "!!w m. bintrunc n (bin_sc m bit.B0 w) <= bintrunc n w" ``` kleing@24333 ` 441` ``` apply (induct n) ``` kleing@24333 ` 442` ``` apply simp ``` kleing@24333 ` 443` ``` apply (case_tac w rule: bin_exhaust) ``` kleing@24333 ` 444` ``` apply (case_tac m) ``` huffman@26086 ` 445` ``` apply (auto simp del: BIT_simps) ``` kleing@24333 ` 446` ``` apply (unfold Bit_def) ``` kleing@24333 ` 447` ``` apply (simp_all split: bit.split) ``` kleing@24333 ` 448` ``` done ``` kleing@24333 ` 449` kleing@24333 ` 450` ```lemma bintr_bin_set_ge: ``` kleing@24333 ` 451` ``` "!!w m. bintrunc n (bin_sc m bit.B1 w) >= bintrunc n w" ``` kleing@24333 ` 452` ``` apply (induct n) ``` kleing@24333 ` 453` ``` apply simp ``` kleing@24333 ` 454` ``` apply (case_tac w rule: bin_exhaust) ``` kleing@24333 ` 455` ``` apply (case_tac m) ``` huffman@26086 ` 456` ``` apply (auto simp del: BIT_simps) ``` kleing@24333 ` 457` ``` apply (unfold Bit_def) ``` kleing@24333 ` 458` ``` apply (simp_all split: bit.split) ``` kleing@24333 ` 459` ``` done ``` kleing@24333 ` 460` haftmann@25919 ` 461` ```lemma bin_sc_FP [simp]: "bin_sc n bit.B0 Int.Pls = Int.Pls" ``` kleing@24333 ` 462` ``` by (induct n) auto ``` kleing@24333 ` 463` haftmann@25919 ` 464` ```lemma bin_sc_TM [simp]: "bin_sc n bit.B1 Int.Min = Int.Min" ``` kleing@24333 ` 465` ``` by (induct n) auto ``` kleing@24333 ` 466` ``` ``` kleing@24333 ` 467` ```lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP ``` kleing@24333 ` 468` kleing@24333 ` 469` ```lemma bin_sc_minus: ``` kleing@24333 ` 470` ``` "0 < n ==> bin_sc (Suc (n - 1)) b w = bin_sc n b w" ``` kleing@24333 ` 471` ``` by auto ``` kleing@24333 ` 472` kleing@24333 ` 473` ```lemmas bin_sc_Suc_minus = ``` kleing@24333 ` 474` ``` trans [OF bin_sc_minus [symmetric] bin_sc.Suc, standard] ``` kleing@24333 ` 475` kleing@24333 ` 476` ```lemmas bin_sc_Suc_pred [simp] = ``` kleing@24333 ` 477` ``` bin_sc_Suc_minus [of "number_of bin", simplified nobm1, standard] ``` kleing@24333 ` 478` huffman@24465 ` 479` ```subsection {* Operations on lists of booleans *} ``` huffman@24465 ` 480` haftmann@26558 ` 481` ```primrec bl_to_bin_aux :: "bool list \ int \ int" where ``` haftmann@26558 ` 482` ``` Nil: "bl_to_bin_aux [] w = w" ``` haftmann@26558 ` 483` ``` | Cons: "bl_to_bin_aux (b # bs) w = ``` haftmann@26558 ` 484` ``` bl_to_bin_aux bs (w BIT (if b then bit.B1 else bit.B0))" ``` huffman@24465 ` 485` haftmann@26558 ` 486` ```definition bl_to_bin :: "bool list \ int" where ``` haftmann@26558 ` 487` ``` bl_to_bin_def : "bl_to_bin bs = bl_to_bin_aux bs Int.Pls" ``` huffman@24465 ` 488` haftmann@26558 ` 489` ```primrec bin_to_bl_aux :: "nat \ int \ bool list \ bool list" where ``` haftmann@26558 ` 490` ``` Z: "bin_to_bl_aux 0 w bl = bl" ``` haftmann@26558 ` 491` ``` | Suc: "bin_to_bl_aux (Suc n) w bl = ``` haftmann@26558 ` 492` ``` bin_to_bl_aux n (bin_rest w) ((bin_last w = bit.B1) # bl)" ``` huffman@24465 ` 493` haftmann@26558 ` 494` ```definition bin_to_bl :: "nat \ int \ bool list" where ``` haftmann@26558 ` 495` ``` bin_to_bl_def : "bin_to_bl n w = bin_to_bl_aux n w []" ``` huffman@24465 ` 496` haftmann@26558 ` 497` ```primrec bl_of_nth :: "nat \ (nat \ bool) \ bool list" where ``` haftmann@26558 ` 498` ``` Suc: "bl_of_nth (Suc n) f = f n # bl_of_nth n f" ``` haftmann@26558 ` 499` ``` | Z: "bl_of_nth 0 f = []" ``` huffman@24465 ` 500` haftmann@26558 ` 501` ```primrec takefill :: "'a \ nat \ 'a list \ 'a list" where ``` haftmann@26558 ` 502` ``` Z: "takefill fill 0 xs = []" ``` haftmann@26558 ` 503` ``` | Suc: "takefill fill (Suc n) xs = ( ``` haftmann@26558 ` 504` ``` case xs of [] => fill # takefill fill n xs ``` haftmann@26558 ` 505` ``` | y # ys => y # takefill fill n ys)" ``` huffman@24465 ` 506` haftmann@26558 ` 507` ```definition map2 :: "('a \ 'b \ 'c) \ 'a list \ 'b list \ 'c list" where ``` haftmann@26558 ` 508` ``` "map2 f as bs = map (split f) (zip as bs)" ``` huffman@24465 ` 509` huffman@24465 ` 510` huffman@24364 ` 511` ```subsection {* Splitting and concatenation *} ``` kleing@24333 ` 512` haftmann@26558 ` 513` ```definition bin_rcat :: "nat \ int list \ int" where ``` haftmann@26558 ` 514` ``` "bin_rcat n = foldl (%u v. bin_cat u n v) Int.Pls" ``` haftmann@26558 ` 515` krauss@28042 ` 516` ```fun bin_rsplit_aux :: "nat \ nat \ int \ int list \ int list" where ``` haftmann@26558 ` 517` ``` "bin_rsplit_aux n m c bs = ``` huffman@24364 ` 518` ``` (if m = 0 | n = 0 then bs else ``` huffman@24364 ` 519` ``` let (a, b) = bin_split n c ``` haftmann@26558 ` 520` ``` in bin_rsplit_aux n (m - n) a (b # bs))" ``` huffman@24364 ` 521` haftmann@26558 ` 522` ```definition bin_rsplit :: "nat \ nat \ int \ int list" where ``` haftmann@26558 ` 523` ``` "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []" ``` haftmann@26558 ` 524` krauss@28042 ` 525` ```fun bin_rsplitl_aux :: "nat \ nat \ int \ int list \ int list" where ``` haftmann@26558 ` 526` ``` "bin_rsplitl_aux n m c bs = ``` huffman@24364 ` 527` ``` (if m = 0 | n = 0 then bs else ``` huffman@24364 ` 528` ``` let (a, b) = bin_split (min m n) c ``` haftmann@26558 ` 529` ``` in bin_rsplitl_aux n (m - n) a (b # bs))" ``` huffman@24364 ` 530` haftmann@26558 ` 531` ```definition bin_rsplitl :: "nat \ nat \ int \ int list" where ``` haftmann@26558 ` 532` ``` "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []" ``` haftmann@26558 ` 533` huffman@24364 ` 534` ```declare bin_rsplit_aux.simps [simp del] ``` huffman@24364 ` 535` ```declare bin_rsplitl_aux.simps [simp del] ``` huffman@24364 ` 536` huffman@24364 ` 537` ```lemma bin_sign_cat: ``` huffman@24364 ` 538` ``` "!!y. bin_sign (bin_cat x n y) = bin_sign x" ``` huffman@24364 ` 539` ``` by (induct n) auto ``` huffman@24364 ` 540` huffman@24364 ` 541` ```lemma bin_cat_Suc_Bit: ``` huffman@24364 ` 542` ``` "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b" ``` huffman@24364 ` 543` ``` by auto ``` huffman@24364 ` 544` huffman@24364 ` 545` ```lemma bin_nth_cat: ``` huffman@24364 ` 546` ``` "!!n y. bin_nth (bin_cat x k y) n = ``` huffman@24364 ` 547` ``` (if n < k then bin_nth y n else bin_nth x (n - k))" ``` huffman@24364 ` 548` ``` apply (induct k) ``` huffman@24364 ` 549` ``` apply clarsimp ``` huffman@24364 ` 550` ``` apply (case_tac n, auto) ``` kleing@24333 ` 551` ``` done ``` kleing@24333 ` 552` huffman@24364 ` 553` ```lemma bin_nth_split: ``` huffman@24364 ` 554` ``` "!!b c. bin_split n c = (a, b) ==> ``` huffman@24364 ` 555` ``` (ALL k. bin_nth a k = bin_nth c (n + k)) & ``` huffman@24364 ` 556` ``` (ALL k. bin_nth b k = (k < n & bin_nth c k))" ``` kleing@24333 ` 557` ``` apply (induct n) ``` huffman@24364 ` 558` ``` apply clarsimp ``` huffman@24364 ` 559` ``` apply (clarsimp simp: Let_def split: ls_splits) ``` huffman@24364 ` 560` ``` apply (case_tac k) ``` huffman@24364 ` 561` ``` apply auto ``` huffman@24364 ` 562` ``` done ``` huffman@24364 ` 563` huffman@24364 ` 564` ```lemma bin_cat_assoc: ``` huffman@24364 ` 565` ``` "!!z. bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)" ``` huffman@24364 ` 566` ``` by (induct n) auto ``` huffman@24364 ` 567` huffman@24364 ` 568` ```lemma bin_cat_assoc_sym: "!!z m. ``` huffman@24364 ` 569` ``` bin_cat x m (bin_cat y n z) = bin_cat (bin_cat x (m - n) y) (min m n) z" ``` huffman@24364 ` 570` ``` apply (induct n, clarsimp) ``` huffman@24364 ` 571` ``` apply (case_tac m, auto) ``` kleing@24333 ` 572` ``` done ``` kleing@24333 ` 573` huffman@24364 ` 574` ```lemma bin_cat_Pls [simp]: ``` haftmann@25919 ` 575` ``` "!!w. bin_cat Int.Pls n w = bintrunc n w" ``` huffman@24364 ` 576` ``` by (induct n) auto ``` huffman@24364 ` 577` huffman@24364 ` 578` ```lemma bintr_cat1: ``` huffman@24364 ` 579` ``` "!!b. bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b" ``` huffman@24364 ` 580` ``` by (induct n) auto ``` huffman@24364 ` 581` ``` ``` huffman@24364 ` 582` ```lemma bintr_cat: "bintrunc m (bin_cat a n b) = ``` huffman@24364 ` 583` ``` bin_cat (bintrunc (m - n) a) n (bintrunc (min m n) b)" ``` huffman@24364 ` 584` ``` by (rule bin_eqI) (auto simp: bin_nth_cat nth_bintr) ``` huffman@24364 ` 585` ``` ``` huffman@24364 ` 586` ```lemma bintr_cat_same [simp]: ``` huffman@24364 ` 587` ``` "bintrunc n (bin_cat a n b) = bintrunc n b" ``` huffman@24364 ` 588` ``` by (auto simp add : bintr_cat) ``` huffman@24364 ` 589` huffman@24364 ` 590` ```lemma cat_bintr [simp]: ``` huffman@24364 ` 591` ``` "!!b. bin_cat a n (bintrunc n b) = bin_cat a n b" ``` huffman@24364 ` 592` ``` by (induct n) auto ``` huffman@24364 ` 593` huffman@24364 ` 594` ```lemma split_bintrunc: ``` huffman@24364 ` 595` ``` "!!b c. bin_split n c = (a, b) ==> b = bintrunc n c" ``` huffman@24364 ` 596` ``` by (induct n) (auto simp: Let_def split: ls_splits) ``` huffman@24364 ` 597` huffman@24364 ` 598` ```lemma bin_cat_split: ``` huffman@24364 ` 599` ``` "!!v w. bin_split n w = (u, v) ==> w = bin_cat u n v" ``` huffman@24364 ` 600` ``` by (induct n) (auto simp: Let_def split: ls_splits) ``` huffman@24364 ` 601` huffman@24364 ` 602` ```lemma bin_split_cat: ``` huffman@24364 ` 603` ``` "!!w. bin_split n (bin_cat v n w) = (v, bintrunc n w)" ``` huffman@24364 ` 604` ``` by (induct n) auto ``` huffman@24364 ` 605` huffman@24364 ` 606` ```lemma bin_split_Pls [simp]: ``` haftmann@25919 ` 607` ``` "bin_split n Int.Pls = (Int.Pls, Int.Pls)" ``` huffman@24364 ` 608` ``` by (induct n) (auto simp: Let_def split: ls_splits) ``` huffman@24364 ` 609` huffman@24364 ` 610` ```lemma bin_split_Min [simp]: ``` haftmann@25919 ` 611` ``` "bin_split n Int.Min = (Int.Min, bintrunc n Int.Min)" ``` huffman@24364 ` 612` ``` by (induct n) (auto simp: Let_def split: ls_splits) ``` huffman@24364 ` 613` huffman@24364 ` 614` ```lemma bin_split_trunc: ``` huffman@24364 ` 615` ``` "!!m b c. bin_split (min m n) c = (a, b) ==> ``` huffman@24364 ` 616` ``` bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)" ``` huffman@24364 ` 617` ``` apply (induct n, clarsimp) ``` huffman@24364 ` 618` ``` apply (simp add: bin_rest_trunc Let_def split: ls_splits) ``` huffman@24364 ` 619` ``` apply (case_tac m) ``` huffman@24364 ` 620` ``` apply (auto simp: Let_def split: ls_splits) ``` kleing@24333 ` 621` ``` done ``` kleing@24333 ` 622` huffman@24364 ` 623` ```lemma bin_split_trunc1: ``` huffman@24364 ` 624` ``` "!!m b c. bin_split n c = (a, b) ==> ``` huffman@24364 ` 625` ``` bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)" ``` huffman@24364 ` 626` ``` apply (induct n, clarsimp) ``` huffman@24364 ` 627` ``` apply (simp add: bin_rest_trunc Let_def split: ls_splits) ``` huffman@24364 ` 628` ``` apply (case_tac m) ``` huffman@24364 ` 629` ``` apply (auto simp: Let_def split: ls_splits) ``` huffman@24364 ` 630` ``` done ``` kleing@24333 ` 631` huffman@24364 ` 632` ```lemma bin_cat_num: ``` huffman@24364 ` 633` ``` "!!b. bin_cat a n b = a * 2 ^ n + bintrunc n b" ``` huffman@24364 ` 634` ``` apply (induct n, clarsimp) ``` huffman@24364 ` 635` ``` apply (simp add: Bit_def cong: number_of_False_cong) ``` huffman@24364 ` 636` ``` done ``` huffman@24364 ` 637` huffman@24364 ` 638` ```lemma bin_split_num: ``` huffman@24364 ` 639` ``` "!!b. bin_split n b = (b div 2 ^ n, b mod 2 ^ n)" ``` huffman@24364 ` 640` ``` apply (induct n, clarsimp) ``` huffman@24364 ` 641` ``` apply (simp add: bin_rest_div zdiv_zmult2_eq) ``` huffman@24364 ` 642` ``` apply (case_tac b rule: bin_exhaust) ``` huffman@24364 ` 643` ``` apply simp ``` huffman@24364 ` 644` ``` apply (simp add: Bit_def zmod_zmult_zmult1 p1mod22k ``` huffman@24364 ` 645` ``` split: bit.split ``` huffman@24364 ` 646` ``` cong: number_of_False_cong) ``` huffman@24364 ` 647` ``` done ``` huffman@24364 ` 648` huffman@24364 ` 649` ```subsection {* Miscellaneous lemmas *} ``` kleing@24333 ` 650` kleing@24333 ` 651` ```lemma nth_2p_bin: ``` kleing@24333 ` 652` ``` "!!m. bin_nth (2 ^ n) m = (m = n)" ``` kleing@24333 ` 653` ``` apply (induct n) ``` kleing@24333 ` 654` ``` apply clarsimp ``` kleing@24333 ` 655` ``` apply safe ``` kleing@24333 ` 656` ``` apply (case_tac m) ``` kleing@24333 ` 657` ``` apply (auto simp: trans [OF numeral_1_eq_1 [symmetric] number_of_eq]) ``` kleing@24333 ` 658` ``` apply (case_tac m) ``` kleing@24333 ` 659` ``` apply (auto simp: Bit_B0_2t [symmetric]) ``` kleing@24333 ` 660` ``` done ``` kleing@24333 ` 661` kleing@24333 ` 662` ```(* for use when simplifying with bin_nth_Bit *) ``` kleing@24333 ` 663` kleing@24333 ` 664` ```lemma ex_eq_or: ``` kleing@24333 ` 665` ``` "(EX m. n = Suc m & (m = k | P m)) = (n = Suc k | (EX m. n = Suc m & P m))" ``` kleing@24333 ` 666` ``` by auto ``` kleing@24333 ` 667` kleing@24333 ` 668` ```end ``` kleing@24333 ` 669`