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--
added lemmas
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
  "\<lbrakk>\<And>n. \<lbrakk>(x ::'a::len0 word) = word_of_int n; 0 \<le> n; n < 2^len_of TYPE('a)\<rbrakk> \<Longrightarrow> P\<rbrakk>
kleing@24333
    18
   \<Longrightarrow> 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
  "\<lbrakk>\<And>n. \<lbrakk>(x ::'a::len word) = of_nat n; n < 2^len_of TYPE('a)\<rbrakk> \<Longrightarrow> P\<rbrakk>
kleing@24333
    23
   \<Longrightarrow> 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 \<le> 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 \<Longrightarrow> 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 (\<lambda>(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 (\<lambda>(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' \<equiv> 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 & \<dots> (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 \<le> 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 \<noteq> 0) = (0 < w)"
kleing@24333
   222
proof -
kleing@24333
   223
  have "0 \<le> 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 \<le> 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 \<le> 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 \<noteq> 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 \<noteq> 0 ==> 1 \<le> x = (0 \<le> 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) \<le> y = (x = y \<or> 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 "\<dots> = (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
  "\<lbrakk>P (0::'a::len word); \<And>n. \<lbrakk>n < m; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> 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
  "\<lbrakk>P (0::'a::len word); \<And>n. P n \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> 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
  "\<lbrakk>P 0; \<And>n. \<lbrakk>1 + n \<noteq> 0; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> 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 \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a"
kleing@24333
   349
  "word_rec forZero forSuc n \<equiv> nat_rec forZero (forSuc \<circ> 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 \<noteq> (0::'a::len word) \<Longrightarrow> 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 \<noteq> 0 \<Longrightarrow> 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 (\<lambda>_. f) n) = word_rec (f z) (\<lambda>_. 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 \<circ> 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 \<le> n \<Longrightarrow> word_rec z f n = word_rec (word_rec z f (n - m)) (f \<circ> 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 \<circ> 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="\<lambda>a. x (1 + (n - m + a))" and s="\<lambda>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 (\<lambda>_. 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: "\<forall>m < n. f m = id \<Longrightarrow> 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
  "\<forall>m\<ge>n. m \<noteq> -1 \<longrightarrow> f m = id \<Longrightarrow> 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="\<lambda>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 \<noteq> (0::'a::len word) \<Longrightarrow> 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