src/HOL/Word/WordGenLib.thy
 author nipkow Fri Mar 06 17:38:47 2009 +0100 (2009-03-06) changeset 30313 b2441b0c8d38 parent 30034 60f64f112174 child 30729 461ee3e49ad3 permissions -rw-r--r--
 kleing@24333 ` 1` ```(* Author: Gerwin Klein, Jeremy Dawson ``` kleing@24333 ` 2` kleing@24333 ` 3` ``` Miscellaneous additional library definitions and lemmas for ``` kleing@24333 ` 4` ``` the word type. Instantiation to boolean algebras, definition ``` kleing@24333 ` 5` ``` of recursion and induction patterns for words. ``` kleing@24333 ` 6` ```*) ``` kleing@24333 ` 7` huffman@24350 ` 8` ```header {* Miscellaneous Library for Words *} ``` huffman@24350 ` 9` haftmann@26558 ` 10` ```theory WordGenLib ``` haftmann@26558 ` 11` ```imports WordShift Boolean_Algebra ``` kleing@24333 ` 12` ```begin ``` kleing@24333 ` 13` kleing@24333 ` 14` ```declare of_nat_2p [simp] ``` kleing@24333 ` 15` kleing@24333 ` 16` ```lemma word_int_cases: ``` huffman@24465 ` 17` ``` "\\n. \(x ::'a::len0 word) = word_of_int n; 0 \ n; n < 2^len_of TYPE('a)\ \ P\ ``` kleing@24333 ` 18` ``` \ P" ``` kleing@24333 ` 19` ``` by (cases x rule: word_uint.Abs_cases) (simp add: uints_num) ``` kleing@24333 ` 20` kleing@24333 ` 21` ```lemma word_nat_cases [cases type: word]: ``` huffman@24465 ` 22` ``` "\\n. \(x ::'a::len word) = of_nat n; n < 2^len_of TYPE('a)\ \ P\ ``` kleing@24333 ` 23` ``` \ P" ``` kleing@24333 ` 24` ``` by (cases x rule: word_unat.Abs_cases) (simp add: unats_def) ``` kleing@24333 ` 25` kleing@24333 ` 26` ```lemma max_word_eq: ``` huffman@24465 ` 27` ``` "(max_word::'a::len word) = 2^len_of TYPE('a) - 1" ``` kleing@24333 ` 28` ``` by (simp add: max_word_def word_of_int_hom_syms word_of_int_2p) ``` kleing@24333 ` 29` kleing@24333 ` 30` ```lemma max_word_max [simp,intro!]: ``` kleing@24333 ` 31` ``` "n \ max_word" ``` kleing@24333 ` 32` ``` by (cases n rule: word_int_cases) ``` kleing@24333 ` 33` ``` (simp add: max_word_def word_le_def int_word_uint int_mod_eq') ``` kleing@24333 ` 34` ``` ``` kleing@24333 ` 35` ```lemma word_of_int_2p_len: ``` huffman@24465 ` 36` ``` "word_of_int (2 ^ len_of TYPE('a)) = (0::'a::len0 word)" ``` kleing@24333 ` 37` ``` by (subst word_uint.Abs_norm [symmetric]) ``` kleing@24333 ` 38` ``` (simp add: word_of_int_hom_syms) ``` kleing@24333 ` 39` kleing@24333 ` 40` ```lemma word_pow_0: ``` huffman@24465 ` 41` ``` "(2::'a::len word) ^ len_of TYPE('a) = 0" ``` kleing@24333 ` 42` ```proof - ``` huffman@24465 ` 43` ``` have "word_of_int (2 ^ len_of TYPE('a)) = (0::'a word)" ``` kleing@24333 ` 44` ``` by (rule word_of_int_2p_len) ``` kleing@24333 ` 45` ``` thus ?thesis by (simp add: word_of_int_2p) ``` kleing@24333 ` 46` ```qed ``` kleing@24333 ` 47` kleing@24333 ` 48` ```lemma max_word_wrap: "x + 1 = 0 \ x = max_word" ``` kleing@24333 ` 49` ``` apply (simp add: max_word_eq) ``` kleing@24333 ` 50` ``` apply uint_arith ``` kleing@24333 ` 51` ``` apply auto ``` kleing@24333 ` 52` ``` apply (simp add: word_pow_0) ``` kleing@24333 ` 53` ``` done ``` kleing@24333 ` 54` kleing@24333 ` 55` ```lemma max_word_minus: ``` huffman@24465 ` 56` ``` "max_word = (-1::'a::len word)" ``` kleing@24333 ` 57` ```proof - ``` kleing@24333 ` 58` ``` have "-1 + 1 = (0::'a word)" by simp ``` kleing@24333 ` 59` ``` thus ?thesis by (rule max_word_wrap [symmetric]) ``` kleing@24333 ` 60` ```qed ``` kleing@24333 ` 61` kleing@24333 ` 62` ```lemma max_word_bl [simp]: ``` huffman@24465 ` 63` ``` "to_bl (max_word::'a::len word) = replicate (len_of TYPE('a)) True" ``` kleing@24333 ` 64` ``` by (subst max_word_minus to_bl_n1)+ simp ``` kleing@24333 ` 65` kleing@24333 ` 66` ```lemma max_test_bit [simp]: ``` huffman@24465 ` 67` ``` "(max_word::'a::len word) !! n = (n < len_of TYPE('a))" ``` kleing@24333 ` 68` ``` by (auto simp add: test_bit_bl word_size) ``` kleing@24333 ` 69` kleing@24333 ` 70` ```lemma word_and_max [simp]: ``` kleing@24333 ` 71` ``` "x AND max_word = x" ``` kleing@24333 ` 72` ``` by (rule word_eqI) (simp add: word_ops_nth_size word_size) ``` kleing@24333 ` 73` kleing@24333 ` 74` ```lemma word_or_max [simp]: ``` kleing@24333 ` 75` ``` "x OR max_word = max_word" ``` kleing@24333 ` 76` ``` by (rule word_eqI) (simp add: word_ops_nth_size word_size) ``` kleing@24333 ` 77` kleing@24333 ` 78` ```lemma word_ao_dist2: ``` huffman@24465 ` 79` ``` "x AND (y OR z) = x AND y OR x AND (z::'a::len0 word)" ``` kleing@24333 ` 80` ``` by (rule word_eqI) (auto simp add: word_ops_nth_size word_size) ``` kleing@24333 ` 81` kleing@24333 ` 82` ```lemma word_oa_dist2: ``` huffman@24465 ` 83` ``` "x OR y AND z = (x OR y) AND (x OR (z::'a::len0 word))" ``` kleing@24333 ` 84` ``` by (rule word_eqI) (auto simp add: word_ops_nth_size word_size) ``` kleing@24333 ` 85` kleing@24333 ` 86` ```lemma word_and_not [simp]: ``` huffman@24465 ` 87` ``` "x AND NOT x = (0::'a::len0 word)" ``` kleing@24333 ` 88` ``` by (rule word_eqI) (auto simp add: word_ops_nth_size word_size) ``` kleing@24333 ` 89` kleing@24333 ` 90` ```lemma word_or_not [simp]: ``` kleing@24333 ` 91` ``` "x OR NOT x = max_word" ``` kleing@24333 ` 92` ``` by (rule word_eqI) (auto simp add: word_ops_nth_size word_size) ``` kleing@24333 ` 93` kleing@24333 ` 94` ```lemma word_boolean: ``` kleing@24333 ` 95` ``` "boolean (op AND) (op OR) bitNOT 0 max_word" ``` kleing@24333 ` 96` ``` apply (rule boolean.intro) ``` kleing@24333 ` 97` ``` apply (rule word_bw_assocs) ``` kleing@24333 ` 98` ``` apply (rule word_bw_assocs) ``` kleing@24333 ` 99` ``` apply (rule word_bw_comms) ``` kleing@24333 ` 100` ``` apply (rule word_bw_comms) ``` kleing@24333 ` 101` ``` apply (rule word_ao_dist2) ``` kleing@24333 ` 102` ``` apply (rule word_oa_dist2) ``` kleing@24333 ` 103` ``` apply (rule word_and_max) ``` kleing@24333 ` 104` ``` apply (rule word_log_esimps) ``` kleing@24333 ` 105` ``` apply (rule word_and_not) ``` kleing@24333 ` 106` ``` apply (rule word_or_not) ``` kleing@24333 ` 107` ``` done ``` kleing@24333 ` 108` ballarin@29235 ` 109` ```interpretation word_bool_alg!: ``` ballarin@29235 ` 110` ``` boolean "op AND" "op OR" bitNOT 0 max_word ``` kleing@24333 ` 111` ``` by (rule word_boolean) ``` kleing@24333 ` 112` kleing@24333 ` 113` ```lemma word_xor_and_or: ``` huffman@24465 ` 114` ``` "x XOR y = x AND NOT y OR NOT x AND (y::'a::len0 word)" ``` kleing@24333 ` 115` ``` by (rule word_eqI) (auto simp add: word_ops_nth_size word_size) ``` kleing@24333 ` 116` ballarin@29235 ` 117` ```interpretation word_bool_alg!: ``` ballarin@29235 ` 118` ``` boolean_xor "op AND" "op OR" bitNOT 0 max_word "op XOR" ``` kleing@24333 ` 119` ``` apply (rule boolean_xor.intro) ``` kleing@24333 ` 120` ``` apply (rule word_boolean) ``` kleing@24333 ` 121` ``` apply (rule boolean_xor_axioms.intro) ``` kleing@24333 ` 122` ``` apply (rule word_xor_and_or) ``` kleing@24333 ` 123` ``` done ``` kleing@24333 ` 124` kleing@24333 ` 125` ```lemma shiftr_0 [iff]: ``` huffman@24465 ` 126` ``` "(x::'a::len0 word) >> 0 = x" ``` kleing@24333 ` 127` ``` by (simp add: shiftr_bl) ``` kleing@24333 ` 128` kleing@24333 ` 129` ```lemma shiftl_0 [simp]: ``` huffman@24465 ` 130` ``` "(x :: 'a :: len word) << 0 = x" ``` kleing@24333 ` 131` ``` by (simp add: shiftl_t2n) ``` kleing@24333 ` 132` kleing@24333 ` 133` ```lemma shiftl_1 [simp]: ``` huffman@24465 ` 134` ``` "(1::'a::len word) << n = 2^n" ``` kleing@24333 ` 135` ``` by (simp add: shiftl_t2n) ``` kleing@24333 ` 136` kleing@24333 ` 137` ```lemma uint_lt_0 [simp]: ``` kleing@24333 ` 138` ``` "uint x < 0 = False" ``` kleing@24333 ` 139` ``` by (simp add: linorder_not_less) ``` kleing@24333 ` 140` kleing@24333 ` 141` ```lemma shiftr1_1 [simp]: ``` huffman@24465 ` 142` ``` "shiftr1 (1::'a::len word) = 0" ``` kleing@24333 ` 143` ``` by (simp add: shiftr1_def word_0_alt) ``` kleing@24333 ` 144` kleing@24333 ` 145` ```lemma shiftr_1[simp]: ``` huffman@24465 ` 146` ``` "(1::'a::len word) >> n = (if n = 0 then 1 else 0)" ``` kleing@24333 ` 147` ``` by (induct n) (auto simp: shiftr_def) ``` kleing@24333 ` 148` kleing@24333 ` 149` ```lemma word_less_1 [simp]: ``` huffman@24465 ` 150` ``` "((x::'a::len word) < 1) = (x = 0)" ``` kleing@24333 ` 151` ``` by (simp add: word_less_nat_alt unat_0_iff) ``` kleing@24333 ` 152` kleing@24333 ` 153` ```lemma to_bl_mask: ``` huffman@24465 ` 154` ``` "to_bl (mask n :: 'a::len word) = ``` huffman@24465 ` 155` ``` replicate (len_of TYPE('a) - n) False @ ``` huffman@24465 ` 156` ``` replicate (min (len_of TYPE('a)) n) True" ``` kleing@24333 ` 157` ``` by (simp add: mask_bl word_rep_drop min_def) ``` kleing@24333 ` 158` kleing@24333 ` 159` ```lemma map_replicate_True: ``` kleing@24333 ` 160` ``` "n = length xs ==> ``` kleing@24333 ` 161` ``` map (\(x,y). x & y) (zip xs (replicate n True)) = xs" ``` kleing@24333 ` 162` ``` by (induct xs arbitrary: n) auto ``` kleing@24333 ` 163` kleing@24333 ` 164` ```lemma map_replicate_False: ``` kleing@24333 ` 165` ``` "n = length xs ==> map (\(x,y). x & y) ``` kleing@24333 ` 166` ``` (zip xs (replicate n False)) = replicate n False" ``` kleing@24333 ` 167` ``` by (induct xs arbitrary: n) auto ``` kleing@24333 ` 168` kleing@24333 ` 169` ```lemma bl_and_mask: ``` huffman@24465 ` 170` ``` fixes w :: "'a::len word" ``` kleing@24333 ` 171` ``` fixes n ``` huffman@24465 ` 172` ``` defines "n' \ len_of TYPE('a) - n" ``` kleing@24333 ` 173` ``` shows "to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)" ``` kleing@24333 ` 174` ```proof - ``` kleing@24333 ` 175` ``` note [simp] = map_replicate_True map_replicate_False ``` kleing@24333 ` 176` ``` have "to_bl (w AND mask n) = ``` haftmann@26558 ` 177` ``` map2 op & (to_bl w) (to_bl (mask n::'a::len word))" ``` kleing@24333 ` 178` ``` by (simp add: bl_word_and) ``` kleing@24333 ` 179` ``` also ``` kleing@24333 ` 180` ``` have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)" by simp ``` kleing@24333 ` 181` ``` also ``` haftmann@26558 ` 182` ``` have "map2 op & \ (to_bl (mask n::'a::len word)) = ``` kleing@24333 ` 183` ``` replicate n' False @ drop n' (to_bl w)" ``` haftmann@26558 ` 184` ``` unfolding to_bl_mask n'_def map2_def ``` kleing@24333 ` 185` ``` by (subst zip_append) auto ``` kleing@24333 ` 186` ``` finally ``` kleing@24333 ` 187` ``` show ?thesis . ``` kleing@24333 ` 188` ```qed ``` kleing@24333 ` 189` kleing@24333 ` 190` ```lemma drop_rev_takefill: ``` kleing@24333 ` 191` ``` "length xs \ n ==> ``` kleing@24333 ` 192` ``` drop (n - length xs) (rev (takefill False n (rev xs))) = xs" ``` kleing@24333 ` 193` ``` by (simp add: takefill_alt rev_take) ``` kleing@24333 ` 194` kleing@24333 ` 195` ```lemma map_nth_0 [simp]: ``` huffman@24465 ` 196` ``` "map (op !! (0::'a::len0 word)) xs = replicate (length xs) False" ``` kleing@24333 ` 197` ``` by (induct xs) auto ``` kleing@24333 ` 198` kleing@24333 ` 199` ```lemma uint_plus_if_size: ``` kleing@24333 ` 200` ``` "uint (x + y) = ``` kleing@24333 ` 201` ``` (if uint x + uint y < 2^size x then ``` kleing@24333 ` 202` ``` uint x + uint y ``` kleing@24333 ` 203` ``` else ``` kleing@24333 ` 204` ``` uint x + uint y - 2^size x)" ``` kleing@24333 ` 205` ``` by (simp add: word_arith_alts int_word_uint mod_add_if_z ``` kleing@24333 ` 206` ``` word_size) ``` kleing@24333 ` 207` kleing@24333 ` 208` ```lemma unat_plus_if_size: ``` huffman@24465 ` 209` ``` "unat (x + (y::'a::len word)) = ``` kleing@24333 ` 210` ``` (if unat x + unat y < 2^size x then ``` kleing@24333 ` 211` ``` unat x + unat y ``` kleing@24333 ` 212` ``` else ``` kleing@24333 ` 213` ``` unat x + unat y - 2^size x)" ``` kleing@24333 ` 214` ``` apply (subst word_arith_nat_defs) ``` kleing@24333 ` 215` ``` apply (subst unat_of_nat) ``` kleing@24333 ` 216` ``` apply (simp add: mod_nat_add word_size) ``` kleing@24333 ` 217` ``` done ``` kleing@24333 ` 218` kleing@24333 ` 219` ```lemma word_neq_0_conv [simp]: ``` huffman@24465 ` 220` ``` fixes w :: "'a :: len word" ``` kleing@24333 ` 221` ``` shows "(w \ 0) = (0 < w)" ``` kleing@24333 ` 222` ```proof - ``` kleing@24333 ` 223` ``` have "0 \ w" by (rule word_zero_le) ``` kleing@24333 ` 224` ``` thus ?thesis by (auto simp add: word_less_def) ``` kleing@24333 ` 225` ```qed ``` kleing@24333 ` 226` kleing@24333 ` 227` ```lemma max_lt: ``` huffman@24465 ` 228` ``` "unat (max a b div c) = unat (max a b) div unat (c:: 'a :: len word)" ``` kleing@24333 ` 229` ``` apply (subst word_arith_nat_defs) ``` kleing@24333 ` 230` ``` apply (subst word_unat.eq_norm) ``` kleing@24333 ` 231` ``` apply (subst mod_if) ``` kleing@24333 ` 232` ``` apply clarsimp ``` kleing@24333 ` 233` ``` apply (erule notE) ``` kleing@24333 ` 234` ``` apply (insert div_le_dividend [of "unat (max a b)" "unat c"]) ``` kleing@24333 ` 235` ``` apply (erule order_le_less_trans) ``` kleing@24333 ` 236` ``` apply (insert unat_lt2p [of "max a b"]) ``` kleing@24333 ` 237` ``` apply simp ``` kleing@24333 ` 238` ``` done ``` kleing@24333 ` 239` kleing@24333 ` 240` ```lemma uint_sub_if_size: ``` kleing@24333 ` 241` ``` "uint (x - y) = ``` kleing@24333 ` 242` ``` (if uint y \ uint x then ``` kleing@24333 ` 243` ``` uint x - uint y ``` kleing@24333 ` 244` ``` else ``` kleing@24333 ` 245` ``` uint x - uint y + 2^size x)" ``` kleing@24333 ` 246` ``` by (simp add: word_arith_alts int_word_uint mod_sub_if_z ``` kleing@24333 ` 247` ``` word_size) ``` kleing@24333 ` 248` kleing@24333 ` 249` ```lemma unat_sub_simple: ``` kleing@24333 ` 250` ``` "x \ y ==> unat (y - x) = unat y - unat x" ``` kleing@24333 ` 251` ``` by (simp add: unat_def uint_sub_if_size word_le_def nat_diff_distrib) ``` kleing@24333 ` 252` kleing@24333 ` 253` ```lemmas unat_sub = unat_sub_simple ``` kleing@24333 ` 254` kleing@24333 ` 255` ```lemma word_less_sub1: ``` huffman@24465 ` 256` ``` fixes x :: "'a :: len word" ``` kleing@24333 ` 257` ``` shows "x \ 0 ==> 1 < x = (0 < x - 1)" ``` kleing@24333 ` 258` ``` by (simp add: unat_sub_if_size word_less_nat_alt) ``` kleing@24333 ` 259` kleing@24333 ` 260` ```lemma word_le_sub1: ``` huffman@24465 ` 261` ``` fixes x :: "'a :: len word" ``` kleing@24333 ` 262` ``` shows "x \ 0 ==> 1 \ x = (0 \ x - 1)" ``` kleing@24333 ` 263` ``` by (simp add: unat_sub_if_size order_le_less word_less_nat_alt) ``` kleing@24333 ` 264` kleing@24333 ` 265` ```lemmas word_less_sub1_numberof [simp] = ``` wenzelm@25349 ` 266` ``` word_less_sub1 [of "number_of w", standard] ``` kleing@24333 ` 267` ```lemmas word_le_sub1_numberof [simp] = ``` wenzelm@25349 ` 268` ``` word_le_sub1 [of "number_of w", standard] ``` kleing@24333 ` 269` ``` ``` kleing@24333 ` 270` ```lemma word_of_int_minus: ``` huffman@24465 ` 271` ``` "word_of_int (2^len_of TYPE('a) - i) = (word_of_int (-i)::'a::len word)" ``` kleing@24333 ` 272` ```proof - ``` huffman@24465 ` 273` ``` have x: "2^len_of TYPE('a) - i = -i + 2^len_of TYPE('a)" by simp ``` kleing@24333 ` 274` ``` show ?thesis ``` kleing@24333 ` 275` ``` apply (subst x) ``` nipkow@30034 ` 276` ``` apply (subst word_uint.Abs_norm [symmetric], subst mod_add_self2) ``` kleing@24333 ` 277` ``` apply simp ``` kleing@24333 ` 278` ``` done ``` kleing@24333 ` 279` ```qed ``` kleing@24333 ` 280` ``` ``` kleing@24333 ` 281` ```lemmas word_of_int_inj = ``` kleing@24333 ` 282` ``` word_uint.Abs_inject [unfolded uints_num, simplified] ``` kleing@24333 ` 283` kleing@24333 ` 284` ```lemma word_le_less_eq: ``` huffman@24465 ` 285` ``` "(x ::'z::len word) \ y = (x = y \ x < y)" ``` kleing@24333 ` 286` ``` by (auto simp add: word_less_def) ``` kleing@24333 ` 287` kleing@24333 ` 288` ```lemma mod_plus_cong: ``` kleing@24333 ` 289` ``` assumes 1: "(b::int) = b'" ``` kleing@24333 ` 290` ``` and 2: "x mod b' = x' mod b'" ``` kleing@24333 ` 291` ``` and 3: "y mod b' = y' mod b'" ``` kleing@24333 ` 292` ``` and 4: "x' + y' = z'" ``` kleing@24333 ` 293` ``` shows "(x + y) mod b = z' mod b'" ``` kleing@24333 ` 294` ```proof - ``` kleing@24333 ` 295` ``` from 1 2[symmetric] 3[symmetric] have "(x + y) mod b = (x' mod b' + y' mod b') mod b'" ``` nipkow@29948 ` 296` ``` by (simp add: mod_add_eq[symmetric]) ``` kleing@24333 ` 297` ``` also have "\ = (x' + y') mod b'" ``` nipkow@29948 ` 298` ``` by (simp add: mod_add_eq[symmetric]) ``` kleing@24333 ` 299` ``` finally show ?thesis by (simp add: 4) ``` kleing@24333 ` 300` ```qed ``` kleing@24333 ` 301` kleing@24333 ` 302` ```lemma mod_minus_cong: ``` kleing@24333 ` 303` ``` assumes 1: "(b::int) = b'" ``` kleing@24333 ` 304` ``` and 2: "x mod b' = x' mod b'" ``` kleing@24333 ` 305` ``` and 3: "y mod b' = y' mod b'" ``` kleing@24333 ` 306` ``` and 4: "x' - y' = z'" ``` kleing@24333 ` 307` ``` shows "(x - y) mod b = z' mod b'" ``` kleing@24333 ` 308` ``` using assms ``` kleing@24333 ` 309` ``` apply (subst zmod_zsub_left_eq) ``` kleing@24333 ` 310` ``` apply (subst zmod_zsub_right_eq) ``` kleing@24333 ` 311` ``` apply (simp add: zmod_zsub_left_eq [symmetric] zmod_zsub_right_eq [symmetric]) ``` kleing@24333 ` 312` ``` done ``` kleing@24333 ` 313` kleing@24333 ` 314` ```lemma word_induct_less: ``` huffman@24465 ` 315` ``` "\P (0::'a::len word); \n. \n < m; P n\ \ P (1 + n)\ \ P m" ``` kleing@24333 ` 316` ``` apply (cases m) ``` kleing@24333 ` 317` ``` apply atomize ``` kleing@24333 ` 318` ``` apply (erule rev_mp)+ ``` kleing@24333 ` 319` ``` apply (rule_tac x=m in spec) ``` wenzelm@27136 ` 320` ``` apply (induct_tac n) ``` kleing@24333 ` 321` ``` apply simp ``` kleing@24333 ` 322` ``` apply clarsimp ``` kleing@24333 ` 323` ``` apply (erule impE) ``` kleing@24333 ` 324` ``` apply clarsimp ``` kleing@24333 ` 325` ``` apply (erule_tac x=n in allE) ``` kleing@24333 ` 326` ``` apply (erule impE) ``` kleing@24333 ` 327` ``` apply (simp add: unat_arith_simps) ``` kleing@24333 ` 328` ``` apply (clarsimp simp: unat_of_nat) ``` kleing@24333 ` 329` ``` apply simp ``` kleing@24333 ` 330` ``` apply (erule_tac x="of_nat na" in allE) ``` kleing@24333 ` 331` ``` apply (erule impE) ``` kleing@24333 ` 332` ``` apply (simp add: unat_arith_simps) ``` kleing@24333 ` 333` ``` apply (clarsimp simp: unat_of_nat) ``` kleing@24333 ` 334` ``` apply simp ``` kleing@24333 ` 335` ``` done ``` kleing@24333 ` 336` ``` ``` kleing@24333 ` 337` ```lemma word_induct: ``` huffman@24465 ` 338` ``` "\P (0::'a::len word); \n. P n \ P (1 + n)\ \ P m" ``` kleing@24333 ` 339` ``` by (erule word_induct_less, simp) ``` kleing@24333 ` 340` kleing@24333 ` 341` ```lemma word_induct2 [induct type]: ``` huffman@24465 ` 342` ``` "\P 0; \n. \1 + n \ 0; P n\ \ P (1 + n)\ \ P (n::'b::len word)" ``` kleing@24333 ` 343` ``` apply (rule word_induct, simp) ``` kleing@24333 ` 344` ``` apply (case_tac "1+n = 0", auto) ``` kleing@24333 ` 345` ``` done ``` kleing@24333 ` 346` kleing@24333 ` 347` ```constdefs ``` huffman@24465 ` 348` ``` word_rec :: "'a \ ('b::len word \ 'a \ 'a) \ 'b word \ 'a" ``` kleing@24333 ` 349` ``` "word_rec forZero forSuc n \ nat_rec forZero (forSuc \ of_nat) (unat n)" ``` kleing@24333 ` 350` kleing@24333 ` 351` ```lemma word_rec_0: "word_rec z s 0 = z" ``` kleing@24333 ` 352` ``` by (simp add: word_rec_def) ``` kleing@24333 ` 353` kleing@24333 ` 354` ```lemma word_rec_Suc: ``` huffman@24465 ` 355` ``` "1 + n \ (0::'a::len word) \ word_rec z s (1 + n) = s n (word_rec z s n)" ``` kleing@24333 ` 356` ``` apply (simp add: word_rec_def unat_word_ariths) ``` kleing@24333 ` 357` ``` apply (subst nat_mod_eq') ``` kleing@24333 ` 358` ``` apply (cut_tac x=n in unat_lt2p) ``` kleing@24333 ` 359` ``` apply (drule Suc_mono) ``` kleing@24333 ` 360` ``` apply (simp add: less_Suc_eq_le) ``` kleing@24333 ` 361` ``` apply (simp only: order_less_le, simp) ``` kleing@24333 ` 362` ``` apply (erule contrapos_pn, simp) ``` kleing@24333 ` 363` ``` apply (drule arg_cong[where f=of_nat]) ``` kleing@24333 ` 364` ``` apply simp ``` ballarin@29235 ` 365` ``` apply (subst (asm) word_unat.Rep_inverse[of n]) ``` kleing@24333 ` 366` ``` apply simp ``` kleing@24333 ` 367` ``` apply simp ``` kleing@24333 ` 368` ``` done ``` kleing@24333 ` 369` kleing@24333 ` 370` ```lemma word_rec_Pred: ``` kleing@24333 ` 371` ``` "n \ 0 \ word_rec z s n = s (n - 1) (word_rec z s (n - 1))" ``` kleing@24333 ` 372` ``` apply (rule subst[where t="n" and s="1 + (n - 1)"]) ``` kleing@24333 ` 373` ``` apply simp ``` kleing@24333 ` 374` ``` apply (subst word_rec_Suc) ``` kleing@24333 ` 375` ``` apply simp ``` kleing@24333 ` 376` ``` apply simp ``` kleing@24333 ` 377` ``` done ``` kleing@24333 ` 378` kleing@24333 ` 379` ```lemma word_rec_in: ``` kleing@24333 ` 380` ``` "f (word_rec z (\_. f) n) = word_rec (f z) (\_. f) n" ``` kleing@24333 ` 381` ``` by (induct n) (simp_all add: word_rec_0 word_rec_Suc) ``` kleing@24333 ` 382` kleing@24333 ` 383` ```lemma word_rec_in2: ``` kleing@24333 ` 384` ``` "f n (word_rec z f n) = word_rec (f 0 z) (f \ op + 1) n" ``` kleing@24333 ` 385` ``` by (induct n) (simp_all add: word_rec_0 word_rec_Suc) ``` kleing@24333 ` 386` kleing@24333 ` 387` ```lemma word_rec_twice: ``` kleing@24333 ` 388` ``` "m \ n \ word_rec z f n = word_rec (word_rec z f (n - m)) (f \ op + (n - m)) m" ``` kleing@24333 ` 389` ```apply (erule rev_mp) ``` kleing@24333 ` 390` ```apply (rule_tac x=z in spec) ``` kleing@24333 ` 391` ```apply (rule_tac x=f in spec) ``` kleing@24333 ` 392` ```apply (induct n) ``` kleing@24333 ` 393` ``` apply (simp add: word_rec_0) ``` kleing@24333 ` 394` ```apply clarsimp ``` kleing@24333 ` 395` ```apply (rule_tac t="1 + n - m" and s="1 + (n - m)" in subst) ``` kleing@24333 ` 396` ``` apply simp ``` kleing@24333 ` 397` ```apply (case_tac "1 + (n - m) = 0") ``` kleing@24333 ` 398` ``` apply (simp add: word_rec_0) ``` wenzelm@25349 ` 399` ``` apply (rule_tac f = "word_rec ?a ?b" in arg_cong) ``` kleing@24333 ` 400` ``` apply (rule_tac t="m" and s="m + (1 + (n - m))" in subst) ``` kleing@24333 ` 401` ``` apply simp ``` kleing@24333 ` 402` ``` apply (simp (no_asm_use)) ``` kleing@24333 ` 403` ```apply (simp add: word_rec_Suc word_rec_in2) ``` kleing@24333 ` 404` ```apply (erule impE) ``` kleing@24333 ` 405` ``` apply uint_arith ``` kleing@24333 ` 406` ```apply (drule_tac x="x \ op + 1" in spec) ``` kleing@24333 ` 407` ```apply (drule_tac x="x 0 xa" in spec) ``` kleing@24333 ` 408` ```apply simp ``` kleing@24333 ` 409` ```apply (rule_tac t="\a. x (1 + (n - m + a))" and s="\a. x (1 + (n - m) + a)" ``` kleing@24333 ` 410` ``` in subst) ``` kleing@24333 ` 411` ``` apply (clarsimp simp add: expand_fun_eq) ``` kleing@24333 ` 412` ``` apply (rule_tac t="(1 + (n - m + xb))" and s="1 + (n - m) + xb" in subst) ``` kleing@24333 ` 413` ``` apply simp ``` kleing@24333 ` 414` ``` apply (rule refl) ``` kleing@24333 ` 415` ```apply (rule refl) ``` kleing@24333 ` 416` ```done ``` kleing@24333 ` 417` kleing@24333 ` 418` ```lemma word_rec_id: "word_rec z (\_. id) n = z" ``` kleing@24333 ` 419` ``` by (induct n) (auto simp add: word_rec_0 word_rec_Suc) ``` kleing@24333 ` 420` kleing@24333 ` 421` ```lemma word_rec_id_eq: "\m < n. f m = id \ word_rec z f n = z" ``` kleing@24333 ` 422` ```apply (erule rev_mp) ``` kleing@24333 ` 423` ```apply (induct n) ``` kleing@24333 ` 424` ``` apply (auto simp add: word_rec_0 word_rec_Suc) ``` kleing@24333 ` 425` ``` apply (drule spec, erule mp) ``` kleing@24333 ` 426` ``` apply uint_arith ``` kleing@24333 ` 427` ```apply (drule_tac x=n in spec, erule impE) ``` kleing@24333 ` 428` ``` apply uint_arith ``` kleing@24333 ` 429` ```apply simp ``` kleing@24333 ` 430` ```done ``` kleing@24333 ` 431` kleing@24333 ` 432` ```lemma word_rec_max: ``` kleing@24333 ` 433` ``` "\m\n. m \ -1 \ f m = id \ word_rec z f -1 = word_rec z f n" ``` kleing@24333 ` 434` ```apply (subst word_rec_twice[where n="-1" and m="-1 - n"]) ``` kleing@24333 ` 435` ``` apply simp ``` kleing@24333 ` 436` ```apply simp ``` kleing@24333 ` 437` ```apply (rule word_rec_id_eq) ``` kleing@24333 ` 438` ```apply clarsimp ``` kleing@24333 ` 439` ```apply (drule spec, rule mp, erule mp) ``` kleing@24333 ` 440` ``` apply (rule word_plus_mono_right2[OF _ order_less_imp_le]) ``` kleing@24333 ` 441` ``` prefer 2 ``` kleing@24333 ` 442` ``` apply assumption ``` kleing@24333 ` 443` ``` apply simp ``` kleing@24333 ` 444` ```apply (erule contrapos_pn) ``` kleing@24333 ` 445` ```apply simp ``` kleing@24333 ` 446` ```apply (drule arg_cong[where f="\x. x - n"]) ``` kleing@24333 ` 447` ```apply simp ``` kleing@24333 ` 448` ```done ``` kleing@24333 ` 449` kleing@24333 ` 450` ```lemma unatSuc: ``` huffman@24465 ` 451` ``` "1 + n \ (0::'a::len word) \ unat (1 + n) = Suc (unat n)" ``` kleing@24333 ` 452` ``` by unat_arith ``` kleing@24333 ` 453` haftmann@29628 ` 454` haftmann@29628 ` 455` ```lemmas word_no_1 [simp] = word_1_no [symmetric, unfolded BIT_simps] ``` haftmann@29628 ` 456` ```lemmas word_no_0 [simp] = word_0_no [symmetric] ``` haftmann@29628 ` 457` haftmann@29628 ` 458` ```declare word_0_bl [simp] ``` haftmann@29628 ` 459` ```declare bin_to_bl_def [simp] ``` haftmann@29628 ` 460` ```declare to_bl_0 [simp] ``` haftmann@29628 ` 461` ```declare of_bl_True [simp] ``` haftmann@29628 ` 462` kleing@24333 ` 463` ```end ```