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