src/HOL/Word/WordShift.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 30042 31039ee583fa
child 30952 7ab2716dd93b
permissions -rw-r--r--
added lemmas
kleing@24333
     1
(* 
kleing@24333
     2
    Author:     Jeremy Dawson and Gerwin Klein, NICTA
kleing@24333
     3
kleing@24333
     4
  contains theorems to do with shifting, rotating, splitting words
kleing@24333
     5
*)
kleing@24333
     6
huffman@24350
     7
header {* Shifting, Rotating, and Splitting Words *}
huffman@24465
     8
haftmann@26558
     9
theory WordShift
haftmann@26558
    10
imports WordBitwise
haftmann@26558
    11
begin
kleing@24333
    12
huffman@24350
    13
subsection "Bit shifting"
kleing@24333
    14
kleing@24333
    15
lemma shiftl1_number [simp] :
kleing@24333
    16
  "shiftl1 (number_of w) = number_of (w BIT bit.B0)"
kleing@24333
    17
  apply (unfold shiftl1_def word_number_of_def)
huffman@26086
    18
  apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm
huffman@26086
    19
              del: BIT_simps)
kleing@24333
    20
  apply (subst refl [THEN bintrunc_BIT_I, symmetric])
kleing@24333
    21
  apply (subst bintrunc_bintrunc_min)
kleing@24333
    22
  apply simp
kleing@24333
    23
  done
kleing@24333
    24
kleing@24333
    25
lemma shiftl1_0 [simp] : "shiftl1 0 = 0"
kleing@24333
    26
  unfolding word_0_no shiftl1_number by auto
kleing@24333
    27
kleing@24333
    28
lemmas shiftl1_def_u = shiftl1_def [folded word_number_of_def]
kleing@24333
    29
kleing@24333
    30
lemma shiftl1_def_s: "shiftl1 w = number_of (sint w BIT bit.B0)"
kleing@24333
    31
  by (rule trans [OF _ shiftl1_number]) simp
kleing@24333
    32
kleing@24333
    33
lemma shiftr1_0 [simp] : "shiftr1 0 = 0"
kleing@24333
    34
  unfolding shiftr1_def 
kleing@24333
    35
  by simp (simp add: word_0_wi)
kleing@24333
    36
kleing@24333
    37
lemma sshiftr1_0 [simp] : "sshiftr1 0 = 0"
kleing@24333
    38
  apply (unfold sshiftr1_def)
kleing@24333
    39
  apply simp
kleing@24333
    40
  apply (simp add : word_0_wi)
kleing@24333
    41
  done
kleing@24333
    42
kleing@24333
    43
lemma sshiftr1_n1 [simp] : "sshiftr1 -1 = -1"
kleing@24333
    44
  unfolding sshiftr1_def by auto
kleing@24333
    45
huffman@24465
    46
lemma shiftl_0 [simp] : "(0::'a::len0 word) << n = 0"
kleing@24333
    47
  unfolding shiftl_def by (induct n) auto
kleing@24333
    48
huffman@24465
    49
lemma shiftr_0 [simp] : "(0::'a::len0 word) >> n = 0"
kleing@24333
    50
  unfolding shiftr_def by (induct n) auto
kleing@24333
    51
kleing@24333
    52
lemma sshiftr_0 [simp] : "0 >>> n = 0"
kleing@24333
    53
  unfolding sshiftr_def by (induct n) auto
kleing@24333
    54
kleing@24333
    55
lemma sshiftr_n1 [simp] : "-1 >>> n = -1"
kleing@24333
    56
  unfolding sshiftr_def by (induct n) auto
kleing@24333
    57
kleing@24333
    58
lemma nth_shiftl1: "shiftl1 w !! n = (n < size w & n > 0 & w !! (n - 1))"
kleing@24333
    59
  apply (unfold shiftl1_def word_test_bit_def)
kleing@24333
    60
  apply (simp add: nth_bintr word_ubin.eq_norm word_size)
kleing@24333
    61
  apply (cases n)
kleing@24333
    62
   apply auto
kleing@24333
    63
  done
kleing@24333
    64
kleing@24333
    65
lemma nth_shiftl' [rule_format]:
huffman@24465
    66
  "ALL n. ((w::'a::len0 word) << m) !! n = (n < size w & n >= m & w !! (n - m))"
kleing@24333
    67
  apply (unfold shiftl_def)
kleing@24333
    68
  apply (induct "m")
kleing@24333
    69
   apply (force elim!: test_bit_size)
kleing@24333
    70
  apply (clarsimp simp add : nth_shiftl1 word_size)
kleing@24333
    71
  apply arith
kleing@24333
    72
  done
kleing@24333
    73
kleing@24333
    74
lemmas nth_shiftl = nth_shiftl' [unfolded word_size] 
kleing@24333
    75
kleing@24333
    76
lemma nth_shiftr1: "shiftr1 w !! n = w !! Suc n"
kleing@24333
    77
  apply (unfold shiftr1_def word_test_bit_def)
kleing@24333
    78
  apply (simp add: nth_bintr word_ubin.eq_norm)
kleing@24333
    79
  apply safe
kleing@24333
    80
  apply (drule bin_nth.Suc [THEN iffD2, THEN bin_nth_uint_imp])
kleing@24333
    81
  apply simp
kleing@24333
    82
  done
kleing@24333
    83
kleing@24333
    84
lemma nth_shiftr: 
huffman@24465
    85
  "\<And>n. ((w::'a::len0 word) >> m) !! n = w !! (n + m)"
kleing@24333
    86
  apply (unfold shiftr_def)
kleing@24333
    87
  apply (induct "m")
kleing@24333
    88
   apply (auto simp add : nth_shiftr1)
kleing@24333
    89
  done
kleing@24333
    90
   
kleing@24333
    91
(* see paper page 10, (1), (2), shiftr1_def is of the form of (1),
kleing@24333
    92
  where f (ie bin_rest) takes normal arguments to normal results,
kleing@24333
    93
  thus we get (2) from (1) *)
kleing@24333
    94
kleing@24333
    95
lemma uint_shiftr1: "uint (shiftr1 w) = bin_rest (uint w)" 
kleing@24333
    96
  apply (unfold shiftr1_def word_ubin.eq_norm bin_rest_trunc_i)
kleing@24333
    97
  apply (subst bintr_uint [symmetric, OF order_refl])
kleing@24333
    98
  apply (simp only : bintrunc_bintrunc_l)
kleing@24333
    99
  apply simp 
kleing@24333
   100
  done
kleing@24333
   101
kleing@24333
   102
lemma nth_sshiftr1: 
kleing@24333
   103
  "sshiftr1 w !! n = (if n = size w - 1 then w !! n else w !! Suc n)"
kleing@24333
   104
  apply (unfold sshiftr1_def word_test_bit_def)
kleing@24333
   105
  apply (simp add: nth_bintr word_ubin.eq_norm
kleing@24333
   106
                   bin_nth.Suc [symmetric] word_size 
kleing@24333
   107
             del: bin_nth.simps)
kleing@24333
   108
  apply (simp add: nth_bintr uint_sint del : bin_nth.simps)
kleing@24333
   109
  apply (auto simp add: bin_nth_sint)
kleing@24333
   110
  done
kleing@24333
   111
kleing@24333
   112
lemma nth_sshiftr [rule_format] : 
kleing@24333
   113
  "ALL n. sshiftr w m !! n = (n < size w & 
kleing@24333
   114
    (if n + m >= size w then w !! (size w - 1) else w !! (n + m)))"
kleing@24333
   115
  apply (unfold sshiftr_def)
kleing@24333
   116
  apply (induct_tac "m")
kleing@24333
   117
   apply (simp add: test_bit_bl)
kleing@24333
   118
  apply (clarsimp simp add: nth_sshiftr1 word_size)
kleing@24333
   119
  apply safe
kleing@24333
   120
       apply arith
kleing@24333
   121
      apply arith
kleing@24333
   122
     apply (erule thin_rl)
wenzelm@27136
   123
     apply (case_tac n)
kleing@24333
   124
      apply safe
kleing@24333
   125
      apply simp
kleing@24333
   126
     apply simp
kleing@24333
   127
    apply (erule thin_rl)
wenzelm@27136
   128
    apply (case_tac n)
kleing@24333
   129
     apply safe
kleing@24333
   130
     apply simp
kleing@24333
   131
    apply simp
kleing@24333
   132
   apply arith+
kleing@24333
   133
  done
kleing@24333
   134
    
kleing@24333
   135
lemma shiftr1_div_2: "uint (shiftr1 w) = uint w div 2"
kleing@24333
   136
  apply (unfold shiftr1_def bin_rest_div)
kleing@24333
   137
  apply (rule word_uint.Abs_inverse)
kleing@24333
   138
  apply (simp add: uints_num pos_imp_zdiv_nonneg_iff)
kleing@24333
   139
  apply (rule xtr7)
kleing@24333
   140
   prefer 2
kleing@24333
   141
   apply (rule zdiv_le_dividend)
kleing@24333
   142
    apply auto
kleing@24333
   143
  done
kleing@24333
   144
kleing@24333
   145
lemma sshiftr1_div_2: "sint (sshiftr1 w) = sint w div 2"
kleing@24333
   146
  apply (unfold sshiftr1_def bin_rest_div [symmetric])
kleing@24333
   147
  apply (simp add: word_sbin.eq_norm)
kleing@24333
   148
  apply (rule trans)
kleing@24333
   149
   defer
kleing@24333
   150
   apply (subst word_sbin.norm_Rep [symmetric])
kleing@24333
   151
   apply (rule refl)
kleing@24333
   152
  apply (subst word_sbin.norm_Rep [symmetric])
kleing@24333
   153
  apply (unfold One_nat_def)
kleing@24333
   154
  apply (rule sbintrunc_rest)
kleing@24333
   155
  done
kleing@24333
   156
kleing@24333
   157
lemma shiftr_div_2n: "uint (shiftr w n) = uint w div 2 ^ n"
kleing@24333
   158
  apply (unfold shiftr_def)
kleing@24333
   159
  apply (induct "n")
kleing@24333
   160
   apply simp
kleing@24333
   161
  apply (simp add: shiftr1_div_2 mult_commute
kleing@24333
   162
                   zdiv_zmult2_eq [symmetric])
kleing@24333
   163
  done
kleing@24333
   164
kleing@24333
   165
lemma sshiftr_div_2n: "sint (sshiftr w n) = sint w div 2 ^ n"
kleing@24333
   166
  apply (unfold sshiftr_def)
kleing@24333
   167
  apply (induct "n")
kleing@24333
   168
   apply simp
kleing@24333
   169
  apply (simp add: sshiftr1_div_2 mult_commute
kleing@24333
   170
                   zdiv_zmult2_eq [symmetric])
kleing@24333
   171
  done
kleing@24333
   172
huffman@24350
   173
subsubsection "shift functions in terms of lists of bools"
kleing@24333
   174
kleing@24333
   175
lemmas bshiftr1_no_bin [simp] = 
wenzelm@25350
   176
  bshiftr1_def [where w="number_of w", unfolded to_bl_no_bin, standard]
kleing@24333
   177
kleing@24333
   178
lemma bshiftr1_bl: "to_bl (bshiftr1 b w) = b # butlast (to_bl w)"
kleing@24333
   179
  unfolding bshiftr1_def by (rule word_bl.Abs_inverse) simp
kleing@24333
   180
kleing@24333
   181
lemma shiftl1_of_bl: "shiftl1 (of_bl bl) = of_bl (bl @ [False])"
kleing@24333
   182
  unfolding uint_bl of_bl_no 
kleing@24333
   183
  by (simp add: bl_to_bin_aux_append bl_to_bin_def)
kleing@24333
   184
wenzelm@25350
   185
lemma shiftl1_bl: "shiftl1 (w::'a::len0 word) = of_bl (to_bl w @ [False])"
wenzelm@25350
   186
proof -
wenzelm@25350
   187
  have "shiftl1 w = shiftl1 (of_bl (to_bl w))" by simp
wenzelm@25350
   188
  also have "\<dots> = of_bl (to_bl w @ [False])" by (rule shiftl1_of_bl)
wenzelm@25350
   189
  finally show ?thesis .
wenzelm@25350
   190
qed
kleing@24333
   191
kleing@24333
   192
lemma bl_shiftl1:
huffman@24465
   193
  "to_bl (shiftl1 (w :: 'a :: len word)) = tl (to_bl w) @ [False]"
huffman@24465
   194
  apply (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons')
huffman@24465
   195
  apply (fast intro!: Suc_leI)
huffman@24465
   196
  done
kleing@24333
   197
kleing@24333
   198
lemma shiftr1_bl: "shiftr1 w = of_bl (butlast (to_bl w))"
kleing@24333
   199
  apply (unfold shiftr1_def uint_bl of_bl_def)
kleing@24333
   200
  apply (simp add: butlast_rest_bin word_size)
kleing@24333
   201
  apply (simp add: bin_rest_trunc [symmetric, unfolded One_nat_def])
kleing@24333
   202
  done
kleing@24333
   203
kleing@24333
   204
lemma bl_shiftr1: 
huffman@24465
   205
  "to_bl (shiftr1 (w :: 'a :: len word)) = False # butlast (to_bl w)"
kleing@24333
   206
  unfolding shiftr1_bl
huffman@24465
   207
  by (simp add : word_rep_drop len_gt_0 [THEN Suc_leI])
kleing@24333
   208
kleing@24333
   209
huffman@24465
   210
(* relate the two above : TODO - remove the :: len restriction on
kleing@24333
   211
  this theorem and others depending on it *)
kleing@24333
   212
lemma shiftl1_rev: 
huffman@24465
   213
  "shiftl1 (w :: 'a :: len word) = word_reverse (shiftr1 (word_reverse w))"
kleing@24333
   214
  apply (unfold word_reverse_def)
kleing@24333
   215
  apply (rule word_bl.Rep_inverse' [symmetric])
kleing@24333
   216
  apply (simp add: bl_shiftl1 bl_shiftr1 word_bl.Abs_inverse)
kleing@24333
   217
  apply (cases "to_bl w")
kleing@24333
   218
   apply auto
kleing@24333
   219
  done
kleing@24333
   220
kleing@24333
   221
lemma shiftl_rev: 
huffman@24465
   222
  "shiftl (w :: 'a :: len word) n = word_reverse (shiftr (word_reverse w) n)"
kleing@24333
   223
  apply (unfold shiftl_def shiftr_def)
kleing@24333
   224
  apply (induct "n")
kleing@24333
   225
   apply (auto simp add : shiftl1_rev)
kleing@24333
   226
  done
kleing@24333
   227
kleing@24333
   228
lemmas rev_shiftl =
wenzelm@25350
   229
  shiftl_rev [where w = "word_reverse w", simplified, standard]
kleing@24333
   230
kleing@24333
   231
lemmas shiftr_rev = rev_shiftl [THEN word_rev_gal', standard]
kleing@24333
   232
lemmas rev_shiftr = shiftl_rev [THEN word_rev_gal', standard]
kleing@24333
   233
kleing@24333
   234
lemma bl_sshiftr1:
huffman@24465
   235
  "to_bl (sshiftr1 (w :: 'a :: len word)) = hd (to_bl w) # butlast (to_bl w)"
kleing@24333
   236
  apply (unfold sshiftr1_def uint_bl word_size)
kleing@24333
   237
  apply (simp add: butlast_rest_bin word_ubin.eq_norm)
kleing@24333
   238
  apply (simp add: sint_uint)
kleing@24333
   239
  apply (rule nth_equalityI)
kleing@24333
   240
   apply clarsimp
kleing@24333
   241
  apply clarsimp
kleing@24333
   242
  apply (case_tac i)
kleing@24333
   243
   apply (simp_all add: hd_conv_nth length_0_conv [symmetric]
kleing@24333
   244
                        nth_bin_to_bl bin_nth.Suc [symmetric] 
kleing@24333
   245
                        nth_sbintr 
kleing@24333
   246
                   del: bin_nth.Suc)
huffman@24465
   247
   apply force
kleing@24333
   248
  apply (rule impI)
kleing@24333
   249
  apply (rule_tac f = "bin_nth (uint w)" in arg_cong)
kleing@24333
   250
  apply simp
kleing@24333
   251
  done
kleing@24333
   252
kleing@24333
   253
lemma drop_shiftr: 
huffman@24465
   254
  "drop n (to_bl ((w :: 'a :: len word) >> n)) = take (size w - n) (to_bl w)" 
kleing@24333
   255
  apply (unfold shiftr_def)
kleing@24333
   256
  apply (induct n)
kleing@24333
   257
   prefer 2
kleing@24333
   258
   apply (simp add: drop_Suc bl_shiftr1 butlast_drop [symmetric])
kleing@24333
   259
   apply (rule butlast_take [THEN trans])
kleing@24333
   260
  apply (auto simp: word_size)
kleing@24333
   261
  done
kleing@24333
   262
kleing@24333
   263
lemma drop_sshiftr: 
huffman@24465
   264
  "drop n (to_bl ((w :: 'a :: len word) >>> n)) = take (size w - n) (to_bl w)"
kleing@24333
   265
  apply (unfold sshiftr_def)
kleing@24333
   266
  apply (induct n)
kleing@24333
   267
   prefer 2
kleing@24333
   268
   apply (simp add: drop_Suc bl_sshiftr1 butlast_drop [symmetric])
kleing@24333
   269
   apply (rule butlast_take [THEN trans])
kleing@24333
   270
  apply (auto simp: word_size)
kleing@24333
   271
  done
kleing@24333
   272
kleing@24333
   273
lemma take_shiftr [rule_format] :
huffman@24465
   274
  "n <= size (w :: 'a :: len word) --> take n (to_bl (w >> n)) = 
kleing@24333
   275
    replicate n False" 
kleing@24333
   276
  apply (unfold shiftr_def)
kleing@24333
   277
  apply (induct n)
kleing@24333
   278
   prefer 2
kleing@24333
   279
   apply (simp add: bl_shiftr1)
kleing@24333
   280
   apply (rule impI)
kleing@24333
   281
   apply (rule take_butlast [THEN trans])
kleing@24333
   282
  apply (auto simp: word_size)
kleing@24333
   283
  done
kleing@24333
   284
kleing@24333
   285
lemma take_sshiftr' [rule_format] :
huffman@24465
   286
  "n <= size (w :: 'a :: len word) --> hd (to_bl (w >>> n)) = hd (to_bl w) & 
kleing@24333
   287
    take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))" 
kleing@24333
   288
  apply (unfold sshiftr_def)
kleing@24333
   289
  apply (induct n)
kleing@24333
   290
   prefer 2
kleing@24333
   291
   apply (simp add: bl_sshiftr1)
kleing@24333
   292
   apply (rule impI)
kleing@24333
   293
   apply (rule take_butlast [THEN trans])
kleing@24333
   294
  apply (auto simp: word_size)
kleing@24333
   295
  done
kleing@24333
   296
kleing@24333
   297
lemmas hd_sshiftr = take_sshiftr' [THEN conjunct1, standard]
kleing@24333
   298
lemmas take_sshiftr = take_sshiftr' [THEN conjunct2, standard]
kleing@24333
   299
kleing@24333
   300
lemma atd_lem: "take n xs = t ==> drop n xs = d ==> xs = t @ d"
kleing@24333
   301
  by (auto intro: append_take_drop_id [symmetric])
kleing@24333
   302
kleing@24333
   303
lemmas bl_shiftr = atd_lem [OF take_shiftr drop_shiftr]
kleing@24333
   304
lemmas bl_sshiftr = atd_lem [OF take_sshiftr drop_sshiftr]
kleing@24333
   305
kleing@24333
   306
lemma shiftl_of_bl: "of_bl bl << n = of_bl (bl @ replicate n False)"
kleing@24333
   307
  unfolding shiftl_def
kleing@24333
   308
  by (induct n) (auto simp: shiftl1_of_bl replicate_app_Cons_same)
kleing@24333
   309
wenzelm@25350
   310
lemma shiftl_bl:
wenzelm@25350
   311
  "(w::'a::len0 word) << (n::nat) = of_bl (to_bl w @ replicate n False)"
wenzelm@25350
   312
proof -
wenzelm@25350
   313
  have "w << n = of_bl (to_bl w) << n" by simp
wenzelm@25350
   314
  also have "\<dots> = of_bl (to_bl w @ replicate n False)" by (rule shiftl_of_bl)
wenzelm@25350
   315
  finally show ?thesis .
wenzelm@25350
   316
qed
kleing@24333
   317
wenzelm@25350
   318
lemmas shiftl_number [simp] = shiftl_def [where w="number_of w", standard]
kleing@24333
   319
kleing@24333
   320
lemma bl_shiftl:
kleing@24333
   321
  "to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False"
kleing@24333
   322
  by (simp add: shiftl_bl word_rep_drop word_size min_def)
kleing@24333
   323
kleing@24333
   324
lemma shiftl_zero_size: 
huffman@24465
   325
  fixes x :: "'a::len0 word"
kleing@24333
   326
  shows "size x <= n ==> x << n = 0"
kleing@24333
   327
  apply (unfold word_size)
kleing@24333
   328
  apply (rule word_eqI)
kleing@24333
   329
  apply (clarsimp simp add: shiftl_bl word_size test_bit_of_bl nth_append)
kleing@24333
   330
  done
kleing@24333
   331
huffman@24465
   332
(* note - the following results use 'a :: len word < number_ring *)
kleing@24333
   333
huffman@24465
   334
lemma shiftl1_2t: "shiftl1 (w :: 'a :: len word) = 2 * w"
kleing@24333
   335
  apply (simp add: shiftl1_def_u)
huffman@26086
   336
  apply (simp only:  double_number_of_Bit0 [symmetric])
kleing@24333
   337
  apply simp
kleing@24333
   338
  done
kleing@24333
   339
huffman@24465
   340
lemma shiftl1_p: "shiftl1 (w :: 'a :: len word) = w + w"
kleing@24333
   341
  apply (simp add: shiftl1_def_u)
huffman@26086
   342
  apply (simp only: double_number_of_Bit0 [symmetric])
kleing@24333
   343
  apply simp
kleing@24333
   344
  done
kleing@24333
   345
huffman@24465
   346
lemma shiftl_t2n: "shiftl (w :: 'a :: len word) n = 2 ^ n * w"
kleing@24333
   347
  unfolding shiftl_def 
kleing@24333
   348
  by (induct n) (auto simp: shiftl1_2t power_Suc)
kleing@24333
   349
kleing@24333
   350
lemma shiftr1_bintr [simp]:
huffman@24465
   351
  "(shiftr1 (number_of w) :: 'a :: len0 word) = 
huffman@24465
   352
    number_of (bin_rest (bintrunc (len_of TYPE ('a)) w))" 
kleing@24333
   353
  unfolding shiftr1_def word_number_of_def
kleing@24333
   354
  by (simp add : word_ubin.eq_norm)
kleing@24333
   355
kleing@24333
   356
lemma sshiftr1_sbintr [simp] :
huffman@24465
   357
  "(sshiftr1 (number_of w) :: 'a :: len word) = 
huffman@24465
   358
    number_of (bin_rest (sbintrunc (len_of TYPE ('a) - 1) w))" 
kleing@24333
   359
  unfolding sshiftr1_def word_number_of_def
kleing@24333
   360
  by (simp add : word_sbin.eq_norm)
kleing@24333
   361
kleing@24333
   362
lemma shiftr_no': 
kleing@24333
   363
  "w = number_of bin ==> 
huffman@24465
   364
  (w::'a::len0 word) >> n = number_of ((bin_rest ^ n) (bintrunc (size w) bin))"
kleing@24333
   365
  apply clarsimp
kleing@24333
   366
  apply (rule word_eqI)
kleing@24333
   367
  apply (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size)
kleing@24333
   368
  done
kleing@24333
   369
kleing@24333
   370
lemma sshiftr_no': 
kleing@24333
   371
  "w = number_of bin ==> w >>> n = number_of ((bin_rest ^ n) 
kleing@24333
   372
    (sbintrunc (size w - 1) bin))"
kleing@24333
   373
  apply clarsimp
kleing@24333
   374
  apply (rule word_eqI)
kleing@24333
   375
  apply (auto simp: nth_sshiftr nth_rest_power_bin nth_sbintr word_size)
huffman@24465
   376
   apply (subgoal_tac "na + n = len_of TYPE('a) - Suc 0", simp, simp)+
kleing@24333
   377
  done
kleing@24333
   378
kleing@24333
   379
lemmas sshiftr_no [simp] = 
wenzelm@25350
   380
  sshiftr_no' [where w = "number_of w", OF refl, unfolded word_size, standard]
kleing@24333
   381
kleing@24333
   382
lemmas shiftr_no [simp] = 
wenzelm@25350
   383
  shiftr_no' [where w = "number_of w", OF refl, unfolded word_size, standard]
kleing@24333
   384
kleing@24333
   385
lemma shiftr1_bl_of': 
kleing@24333
   386
  "us = shiftr1 (of_bl bl) ==> length bl <= size us ==> 
kleing@24333
   387
    us = of_bl (butlast bl)"
kleing@24333
   388
  by (clarsimp simp: shiftr1_def of_bl_def word_size butlast_rest_bl2bin 
kleing@24333
   389
                     word_ubin.eq_norm trunc_bl2bin)
kleing@24333
   390
kleing@24333
   391
lemmas shiftr1_bl_of = refl [THEN shiftr1_bl_of', unfolded word_size]
kleing@24333
   392
kleing@24333
   393
lemma shiftr_bl_of' [rule_format]: 
kleing@24333
   394
  "us = of_bl bl >> n ==> length bl <= size us --> 
kleing@24333
   395
   us = of_bl (take (length bl - n) bl)"
kleing@24333
   396
  apply (unfold shiftr_def)
kleing@24333
   397
  apply hypsubst
kleing@24333
   398
  apply (unfold word_size)
kleing@24333
   399
  apply (induct n)
kleing@24333
   400
   apply clarsimp
kleing@24333
   401
  apply clarsimp
kleing@24333
   402
  apply (subst shiftr1_bl_of)
kleing@24333
   403
   apply simp
kleing@24333
   404
  apply (simp add: butlast_take)
kleing@24333
   405
  done
kleing@24333
   406
kleing@24333
   407
lemmas shiftr_bl_of = refl [THEN shiftr_bl_of', unfolded word_size]
kleing@24333
   408
kleing@24333
   409
lemmas shiftr_bl = word_bl.Rep' [THEN eq_imp_le, THEN shiftr_bl_of,
kleing@24333
   410
  simplified word_size, simplified, THEN eq_reflection, standard]
kleing@24333
   411
huffman@24465
   412
lemma msb_shift': "msb (w::'a::len word) <-> (w >> (size w - 1)) ~= 0"
kleing@24333
   413
  apply (unfold shiftr_bl word_msb_alt)
kleing@24333
   414
  apply (simp add: word_size Suc_le_eq take_Suc)
kleing@24333
   415
  apply (cases "hd (to_bl w)")
kleing@24333
   416
   apply (auto simp: word_1_bl word_0_bl 
kleing@24333
   417
                     of_bl_rep_False [where n=1 and bs="[]", simplified])
kleing@24333
   418
  done
kleing@24333
   419
kleing@24333
   420
lemmas msb_shift = msb_shift' [unfolded word_size]
kleing@24333
   421
kleing@24333
   422
lemma align_lem_or [rule_format] :
kleing@24333
   423
  "ALL x m. length x = n + m --> length y = n + m --> 
kleing@24333
   424
    drop m x = replicate n False --> take m y = replicate m False --> 
haftmann@26558
   425
    map2 op | x y = take m x @ drop m y"
kleing@24333
   426
  apply (induct_tac y)
kleing@24333
   427
   apply force
kleing@24333
   428
  apply clarsimp
kleing@24333
   429
  apply (case_tac x, force)
kleing@24333
   430
  apply (case_tac m, auto)
kleing@24333
   431
  apply (drule sym)
kleing@24333
   432
  apply auto
kleing@24333
   433
  apply (induct_tac list, auto)
kleing@24333
   434
  done
kleing@24333
   435
kleing@24333
   436
lemma align_lem_and [rule_format] :
kleing@24333
   437
  "ALL x m. length x = n + m --> length y = n + m --> 
kleing@24333
   438
    drop m x = replicate n False --> take m y = replicate m False --> 
haftmann@26558
   439
    map2 op & x y = replicate (n + m) False"
kleing@24333
   440
  apply (induct_tac y)
kleing@24333
   441
   apply force
kleing@24333
   442
  apply clarsimp
kleing@24333
   443
  apply (case_tac x, force)
kleing@24333
   444
  apply (case_tac m, auto)
kleing@24333
   445
  apply (drule sym)
kleing@24333
   446
  apply auto
kleing@24333
   447
  apply (induct_tac list, auto)
kleing@24333
   448
  done
kleing@24333
   449
kleing@24333
   450
lemma aligned_bl_add_size':
kleing@24333
   451
  "size x - n = m ==> n <= size x ==> drop m (to_bl x) = replicate n False ==>
kleing@24333
   452
    take m (to_bl y) = replicate m False ==> 
kleing@24333
   453
    to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)"
kleing@24333
   454
  apply (subgoal_tac "x AND y = 0")
kleing@24333
   455
   prefer 2
kleing@24333
   456
   apply (rule word_bl.Rep_eqD)
kleing@24333
   457
   apply (simp add: bl_word_and to_bl_0)
kleing@24333
   458
   apply (rule align_lem_and [THEN trans])
kleing@24333
   459
       apply (simp_all add: word_size)[5]
kleing@24333
   460
   apply simp
kleing@24333
   461
  apply (subst word_plus_and_or [symmetric])
kleing@24333
   462
  apply (simp add : bl_word_or)
kleing@24333
   463
  apply (rule align_lem_or)
kleing@24333
   464
     apply (simp_all add: word_size)
kleing@24333
   465
  done
kleing@24333
   466
kleing@24333
   467
lemmas aligned_bl_add_size = refl [THEN aligned_bl_add_size']
kleing@24333
   468
huffman@24350
   469
subsubsection "Mask"
kleing@24333
   470
kleing@24333
   471
lemma nth_mask': "m = mask n ==> test_bit m i = (i < n & i < size m)"
kleing@24333
   472
  apply (unfold mask_def test_bit_bl)
kleing@24333
   473
  apply (simp only: word_1_bl [symmetric] shiftl_of_bl)
kleing@24333
   474
  apply (clarsimp simp add: word_size)
kleing@24333
   475
  apply (simp only: of_bl_no mask_lem number_of_succ add_diff_cancel2)
kleing@24333
   476
  apply (fold of_bl_no)
kleing@24333
   477
  apply (simp add: word_1_bl)
kleing@24333
   478
  apply (rule test_bit_of_bl [THEN trans, unfolded test_bit_bl word_size])
kleing@24333
   479
  apply auto
kleing@24333
   480
  done
kleing@24333
   481
kleing@24333
   482
lemmas nth_mask [simp] = refl [THEN nth_mask']
kleing@24333
   483
kleing@24333
   484
lemma mask_bl: "mask n = of_bl (replicate n True)"
kleing@24333
   485
  by (auto simp add : test_bit_of_bl word_size intro: word_eqI)
kleing@24333
   486
haftmann@25919
   487
lemma mask_bin: "mask n = number_of (bintrunc n Int.Min)"
kleing@24333
   488
  by (auto simp add: nth_bintr word_size intro: word_eqI)
kleing@24333
   489
kleing@24333
   490
lemma and_mask_bintr: "w AND mask n = number_of (bintrunc n (uint w))"
kleing@24333
   491
  apply (rule word_eqI)
kleing@24333
   492
  apply (simp add: nth_bintr word_size word_ops_nth_size)
kleing@24333
   493
  apply (auto simp add: test_bit_bin)
kleing@24333
   494
  done
kleing@24333
   495
kleing@24333
   496
lemma and_mask_no: "number_of i AND mask n = number_of (bintrunc n i)" 
kleing@24333
   497
  by (auto simp add : nth_bintr word_size word_ops_nth_size intro: word_eqI)
kleing@24333
   498
kleing@24333
   499
lemmas and_mask_wi = and_mask_no [unfolded word_number_of_def] 
kleing@24333
   500
kleing@24333
   501
lemma bl_and_mask:
huffman@24465
   502
  "to_bl (w AND mask n :: 'a :: len word) = 
huffman@24465
   503
    replicate (len_of TYPE('a) - n) False @ 
huffman@24465
   504
    drop (len_of TYPE('a) - n) (to_bl w)"
kleing@24333
   505
  apply (rule nth_equalityI)
kleing@24333
   506
   apply simp
kleing@24333
   507
  apply (clarsimp simp add: to_bl_nth word_size)
kleing@24333
   508
  apply (simp add: word_size word_ops_nth_size)
kleing@24333
   509
  apply (auto simp add: word_size test_bit_bl nth_append nth_rev)
kleing@24333
   510
  done
kleing@24333
   511
kleing@24333
   512
lemmas and_mask_mod_2p = 
kleing@24333
   513
  and_mask_bintr [unfolded word_number_of_alt no_bintr_alt]
kleing@24333
   514
kleing@24333
   515
lemma and_mask_lt_2p: "uint (w AND mask n) < 2 ^ n"
kleing@24333
   516
  apply (simp add : and_mask_bintr no_bintr_alt)
kleing@24333
   517
  apply (rule xtr8)
kleing@24333
   518
   prefer 2
kleing@24333
   519
   apply (rule pos_mod_bound)
kleing@24333
   520
  apply auto
kleing@24333
   521
  done
kleing@24333
   522
kleing@24333
   523
lemmas eq_mod_iff = trans [symmetric, OF int_mod_lem eq_sym_conv]
kleing@24333
   524
kleing@24333
   525
lemma mask_eq_iff: "(w AND mask n) = w <-> uint w < 2 ^ n"
kleing@24333
   526
  apply (simp add: and_mask_bintr word_number_of_def)
kleing@24333
   527
  apply (simp add: word_ubin.inverse_norm)
kleing@24333
   528
  apply (simp add: eq_mod_iff bintrunc_mod2p min_def)
kleing@24333
   529
  apply (fast intro!: lt2p_lem)
kleing@24333
   530
  done
kleing@24333
   531
kleing@24333
   532
lemma and_mask_dvd: "2 ^ n dvd uint w = (w AND mask n = 0)"
nipkow@30042
   533
  apply (simp add: dvd_eq_mod_eq_0 and_mask_mod_2p)
kleing@24333
   534
  apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs)
kleing@24333
   535
  apply (subst word_uint.norm_Rep [symmetric])
kleing@24333
   536
  apply (simp only: bintrunc_bintrunc_min bintrunc_mod2p [symmetric] min_def)
kleing@24333
   537
  apply auto
kleing@24333
   538
  done
kleing@24333
   539
kleing@24333
   540
lemma and_mask_dvd_nat: "2 ^ n dvd unat w = (w AND mask n = 0)"
kleing@24333
   541
  apply (unfold unat_def)
kleing@24333
   542
  apply (rule trans [OF _ and_mask_dvd])
kleing@24333
   543
  apply (unfold dvd_def) 
kleing@24333
   544
  apply auto 
kleing@24333
   545
  apply (drule uint_ge_0 [THEN nat_int.Abs_inverse' [simplified], symmetric])
kleing@24333
   546
  apply (simp add : int_mult int_power)
kleing@24333
   547
  apply (simp add : nat_mult_distrib nat_power_eq)
kleing@24333
   548
  done
kleing@24333
   549
kleing@24333
   550
lemma word_2p_lem: 
huffman@24465
   551
  "n < size w ==> w < 2 ^ n = (uint (w :: 'a :: len word) < 2 ^ n)"
kleing@24333
   552
  apply (unfold word_size word_less_alt word_number_of_alt)
kleing@24333
   553
  apply (clarsimp simp add: word_of_int_power_hom word_uint.eq_norm 
kleing@24333
   554
                            int_mod_eq'
kleing@24333
   555
                  simp del: word_of_int_bin)
kleing@24333
   556
  done
kleing@24333
   557
huffman@24465
   558
lemma less_mask_eq: "x < 2 ^ n ==> x AND mask n = (x :: 'a :: len word)"
kleing@24333
   559
  apply (unfold word_less_alt word_number_of_alt)
kleing@24333
   560
  apply (clarsimp simp add: and_mask_mod_2p word_of_int_power_hom 
kleing@24333
   561
                            word_uint.eq_norm
kleing@24333
   562
                  simp del: word_of_int_bin)
kleing@24333
   563
  apply (drule xtr8 [rotated])
kleing@24333
   564
  apply (rule int_mod_le)
kleing@24333
   565
  apply (auto simp add : mod_pos_pos_trivial)
kleing@24333
   566
  done
kleing@24333
   567
kleing@24333
   568
lemmas mask_eq_iff_w2p =
kleing@24333
   569
  trans [OF mask_eq_iff word_2p_lem [symmetric], standard]
kleing@24333
   570
kleing@24333
   571
lemmas and_mask_less' = 
kleing@24333
   572
  iffD2 [OF word_2p_lem and_mask_lt_2p, simplified word_size, standard]
kleing@24333
   573
kleing@24333
   574
lemma and_mask_less_size: "n < size x ==> x AND mask n < 2^n"
kleing@24333
   575
  unfolding word_size by (erule and_mask_less')
kleing@24333
   576
kleing@24333
   577
lemma word_mod_2p_is_mask':
huffman@24465
   578
  "c = 2 ^ n ==> c > 0 ==> x mod c = (x :: 'a :: len word) AND mask n" 
kleing@24333
   579
  by (clarsimp simp add: word_mod_def uint_2p and_mask_mod_2p) 
kleing@24333
   580
kleing@24333
   581
lemmas word_mod_2p_is_mask = refl [THEN word_mod_2p_is_mask'] 
kleing@24333
   582
kleing@24333
   583
lemma mask_eqs:
kleing@24333
   584
  "(a AND mask n) + b AND mask n = a + b AND mask n"
kleing@24333
   585
  "a + (b AND mask n) AND mask n = a + b AND mask n"
kleing@24333
   586
  "(a AND mask n) - b AND mask n = a - b AND mask n"
kleing@24333
   587
  "a - (b AND mask n) AND mask n = a - b AND mask n"
kleing@24333
   588
  "a * (b AND mask n) AND mask n = a * b AND mask n"
kleing@24333
   589
  "(b AND mask n) * a AND mask n = b * a AND mask n"
kleing@24333
   590
  "(a AND mask n) + (b AND mask n) AND mask n = a + b AND mask n"
kleing@24333
   591
  "(a AND mask n) - (b AND mask n) AND mask n = a - b AND mask n"
kleing@24333
   592
  "(a AND mask n) * (b AND mask n) AND mask n = a * b AND mask n"
kleing@24333
   593
  "- (a AND mask n) AND mask n = - a AND mask n"
kleing@24333
   594
  "word_succ (a AND mask n) AND mask n = word_succ a AND mask n"
kleing@24333
   595
  "word_pred (a AND mask n) AND mask n = word_pred a AND mask n"
kleing@24333
   596
  using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b]
kleing@24333
   597
  by (auto simp: and_mask_wi bintr_ariths bintr_arith1s new_word_of_int_homs)
kleing@24333
   598
kleing@24333
   599
lemma mask_power_eq:
kleing@24333
   600
  "(x AND mask n) ^ k AND mask n = x ^ k AND mask n"
kleing@24333
   601
  using word_of_int_Ex [where x=x]
kleing@24333
   602
  by (clarsimp simp: and_mask_wi word_of_int_power_hom bintr_ariths)
kleing@24333
   603
kleing@24333
   604
huffman@24350
   605
subsubsection "Revcast"
kleing@24333
   606
kleing@24333
   607
lemmas revcast_def' = revcast_def [simplified]
kleing@24333
   608
lemmas revcast_def'' = revcast_def' [simplified word_size]
kleing@24333
   609
lemmas revcast_no_def [simp] =
wenzelm@25350
   610
  revcast_def' [where w="number_of w", unfolded word_size, standard]
kleing@24333
   611
kleing@24333
   612
lemma to_bl_revcast: 
huffman@24465
   613
  "to_bl (revcast w :: 'a :: len0 word) = 
huffman@24465
   614
   takefill False (len_of TYPE ('a)) (to_bl w)"
kleing@24333
   615
  apply (unfold revcast_def' word_size)
kleing@24333
   616
  apply (rule word_bl.Abs_inverse)
kleing@24333
   617
  apply simp
kleing@24333
   618
  done
kleing@24333
   619
kleing@24333
   620
lemma revcast_rev_ucast': 
kleing@24333
   621
  "cs = [rc, uc] ==> rc = revcast (word_reverse w) ==> uc = ucast w ==> 
kleing@24333
   622
    rc = word_reverse uc"
kleing@24333
   623
  apply (unfold ucast_def revcast_def' Let_def word_reverse_def)
kleing@24333
   624
  apply (clarsimp simp add : to_bl_of_bin takefill_bintrunc)
kleing@24333
   625
  apply (simp add : word_bl.Abs_inverse word_size)
kleing@24333
   626
  done
kleing@24333
   627
kleing@24333
   628
lemmas revcast_rev_ucast = revcast_rev_ucast' [OF refl refl refl]
kleing@24333
   629
kleing@24333
   630
lemmas revcast_ucast = revcast_rev_ucast
wenzelm@25350
   631
  [where w = "word_reverse w", simplified word_rev_rev, standard]
kleing@24333
   632
kleing@24333
   633
lemmas ucast_revcast = revcast_rev_ucast [THEN word_rev_gal', standard]
kleing@24333
   634
lemmas ucast_rev_revcast = revcast_ucast [THEN word_rev_gal', standard]
kleing@24333
   635
kleing@24333
   636
kleing@24333
   637
-- "linking revcast and cast via shift"
kleing@24333
   638
kleing@24333
   639
lemmas wsst_TYs = source_size target_size word_size
kleing@24333
   640
kleing@24333
   641
lemma revcast_down_uu': 
kleing@24333
   642
  "rc = revcast ==> source_size rc = target_size rc + n ==> 
huffman@24465
   643
    rc (w :: 'a :: len word) = ucast (w >> n)"
kleing@24333
   644
  apply (simp add: revcast_def')
kleing@24333
   645
  apply (rule word_bl.Rep_inverse')
kleing@24333
   646
  apply (rule trans, rule ucast_down_drop)
kleing@24333
   647
   prefer 2
kleing@24333
   648
   apply (rule trans, rule drop_shiftr)
kleing@24333
   649
   apply (auto simp: takefill_alt wsst_TYs)
kleing@24333
   650
  done
kleing@24333
   651
kleing@24333
   652
lemma revcast_down_us': 
kleing@24333
   653
  "rc = revcast ==> source_size rc = target_size rc + n ==> 
huffman@24465
   654
    rc (w :: 'a :: len word) = ucast (w >>> n)"
kleing@24333
   655
  apply (simp add: revcast_def')
kleing@24333
   656
  apply (rule word_bl.Rep_inverse')
kleing@24333
   657
  apply (rule trans, rule ucast_down_drop)
kleing@24333
   658
   prefer 2
kleing@24333
   659
   apply (rule trans, rule drop_sshiftr)
kleing@24333
   660
   apply (auto simp: takefill_alt wsst_TYs)
kleing@24333
   661
  done
kleing@24333
   662
kleing@24333
   663
lemma revcast_down_su': 
kleing@24333
   664
  "rc = revcast ==> source_size rc = target_size rc + n ==> 
huffman@24465
   665
    rc (w :: 'a :: len word) = scast (w >> n)"
kleing@24333
   666
  apply (simp add: revcast_def')
kleing@24333
   667
  apply (rule word_bl.Rep_inverse')
kleing@24333
   668
  apply (rule trans, rule scast_down_drop)
kleing@24333
   669
   prefer 2
kleing@24333
   670
   apply (rule trans, rule drop_shiftr)
kleing@24333
   671
   apply (auto simp: takefill_alt wsst_TYs)
kleing@24333
   672
  done
kleing@24333
   673
kleing@24333
   674
lemma revcast_down_ss': 
kleing@24333
   675
  "rc = revcast ==> source_size rc = target_size rc + n ==> 
huffman@24465
   676
    rc (w :: 'a :: len word) = scast (w >>> n)"
kleing@24333
   677
  apply (simp add: revcast_def')
kleing@24333
   678
  apply (rule word_bl.Rep_inverse')
kleing@24333
   679
  apply (rule trans, rule scast_down_drop)
kleing@24333
   680
   prefer 2
kleing@24333
   681
   apply (rule trans, rule drop_sshiftr)
kleing@24333
   682
   apply (auto simp: takefill_alt wsst_TYs)
kleing@24333
   683
  done
kleing@24333
   684
kleing@24333
   685
lemmas revcast_down_uu = refl [THEN revcast_down_uu']
kleing@24333
   686
lemmas revcast_down_us = refl [THEN revcast_down_us']
kleing@24333
   687
lemmas revcast_down_su = refl [THEN revcast_down_su']
kleing@24333
   688
lemmas revcast_down_ss = refl [THEN revcast_down_ss']
kleing@24333
   689
kleing@24333
   690
lemma cast_down_rev: 
kleing@24333
   691
  "uc = ucast ==> source_size uc = target_size uc + n ==> 
huffman@24465
   692
    uc w = revcast ((w :: 'a :: len word) << n)"
kleing@24333
   693
  apply (unfold shiftl_rev)
kleing@24333
   694
  apply clarify
kleing@24333
   695
  apply (simp add: revcast_rev_ucast)
kleing@24333
   696
  apply (rule word_rev_gal')
kleing@24333
   697
  apply (rule trans [OF _ revcast_rev_ucast])
kleing@24333
   698
  apply (rule revcast_down_uu [symmetric])
kleing@24333
   699
  apply (auto simp add: wsst_TYs)
kleing@24333
   700
  done
kleing@24333
   701
kleing@24333
   702
lemma revcast_up': 
kleing@24333
   703
  "rc = revcast ==> source_size rc + n = target_size rc ==> 
huffman@24465
   704
    rc w = (ucast w :: 'a :: len word) << n" 
kleing@24333
   705
  apply (simp add: revcast_def')
kleing@24333
   706
  apply (rule word_bl.Rep_inverse')
kleing@24333
   707
  apply (simp add: takefill_alt)
kleing@24333
   708
  apply (rule bl_shiftl [THEN trans])
kleing@24333
   709
  apply (subst ucast_up_app)
kleing@24333
   710
  apply (auto simp add: wsst_TYs)
kleing@24333
   711
  done
kleing@24333
   712
kleing@24333
   713
lemmas revcast_up = refl [THEN revcast_up']
kleing@24333
   714
kleing@24333
   715
lemmas rc1 = revcast_up [THEN 
kleing@24333
   716
  revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
kleing@24333
   717
lemmas rc2 = revcast_down_uu [THEN 
kleing@24333
   718
  revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
kleing@24333
   719
kleing@24333
   720
lemmas ucast_up =
kleing@24333
   721
 rc1 [simplified rev_shiftr [symmetric] revcast_ucast [symmetric]]
kleing@24333
   722
lemmas ucast_down = 
kleing@24333
   723
  rc2 [simplified rev_shiftr revcast_ucast [symmetric]]
kleing@24333
   724
kleing@24333
   725
huffman@24350
   726
subsubsection "Slices"
kleing@24333
   727
kleing@24333
   728
lemmas slice1_no_bin [simp] =
wenzelm@25350
   729
  slice1_def [where w="number_of w", unfolded to_bl_no_bin, standard]
kleing@24333
   730
kleing@24333
   731
lemmas slice_no_bin [simp] = 
kleing@24333
   732
   trans [OF slice_def [THEN meta_eq_to_obj_eq] 
kleing@24333
   733
             slice1_no_bin [THEN meta_eq_to_obj_eq], 
kleing@24333
   734
          unfolded word_size, standard]
kleing@24333
   735
kleing@24333
   736
lemma slice1_0 [simp] : "slice1 n 0 = 0"
kleing@24333
   737
  unfolding slice1_def by (simp add : to_bl_0)
kleing@24333
   738
kleing@24333
   739
lemma slice_0 [simp] : "slice n 0 = 0"
kleing@24333
   740
  unfolding slice_def by auto
kleing@24333
   741
kleing@24333
   742
lemma slice_take': "slice n w = of_bl (take (size w - n) (to_bl w))"
kleing@24333
   743
  unfolding slice_def' slice1_def
kleing@24333
   744
  by (simp add : takefill_alt word_size)
kleing@24333
   745
kleing@24333
   746
lemmas slice_take = slice_take' [unfolded word_size]
kleing@24333
   747
kleing@24333
   748
-- "shiftr to a word of the same size is just slice, 
kleing@24333
   749
    slice is just shiftr then ucast"
kleing@24333
   750
lemmas shiftr_slice = trans
kleing@24333
   751
  [OF shiftr_bl [THEN meta_eq_to_obj_eq] slice_take [symmetric], standard]
kleing@24333
   752
kleing@24333
   753
lemma slice_shiftr: "slice n w = ucast (w >> n)"
kleing@24333
   754
  apply (unfold slice_take shiftr_bl)
kleing@24333
   755
  apply (rule ucast_of_bl_up [symmetric])
kleing@24333
   756
  apply (simp add: word_size)
kleing@24333
   757
  done
kleing@24333
   758
kleing@24333
   759
lemma nth_slice: 
huffman@24465
   760
  "(slice n w :: 'a :: len0 word) !! m = 
huffman@24465
   761
   (w !! (m + n) & m < len_of TYPE ('a))"
kleing@24333
   762
  unfolding slice_shiftr 
kleing@24333
   763
  by (simp add : nth_ucast nth_shiftr)
kleing@24333
   764
kleing@24333
   765
lemma slice1_down_alt': 
kleing@24333
   766
  "sl = slice1 n w ==> fs = size sl ==> fs + k = n ==> 
kleing@24333
   767
    to_bl sl = takefill False fs (drop k (to_bl w))"
kleing@24333
   768
  unfolding slice1_def word_size of_bl_def uint_bl
kleing@24333
   769
  by (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop drop_takefill)
kleing@24333
   770
kleing@24333
   771
lemma slice1_up_alt': 
kleing@24333
   772
  "sl = slice1 n w ==> fs = size sl ==> fs = n + k ==> 
kleing@24333
   773
    to_bl sl = takefill False fs (replicate k False @ (to_bl w))"
kleing@24333
   774
  apply (unfold slice1_def word_size of_bl_def uint_bl)
kleing@24333
   775
  apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop 
kleing@24333
   776
                        takefill_append [symmetric])
huffman@24465
   777
  apply (rule_tac f = "%k. takefill False (len_of TYPE('a))
huffman@24465
   778
    (replicate k False @ bin_to_bl (len_of TYPE('b)) (uint w))" in arg_cong)
kleing@24333
   779
  apply arith
kleing@24333
   780
  done
kleing@24333
   781
    
kleing@24333
   782
lemmas sd1 = slice1_down_alt' [OF refl refl, unfolded word_size]
kleing@24333
   783
lemmas su1 = slice1_up_alt' [OF refl refl, unfolded word_size]
kleing@24333
   784
lemmas slice1_down_alt = le_add_diff_inverse [THEN sd1]
kleing@24333
   785
lemmas slice1_up_alts = 
kleing@24333
   786
  le_add_diff_inverse [symmetric, THEN su1] 
kleing@24333
   787
  le_add_diff_inverse2 [symmetric, THEN su1]
kleing@24333
   788
kleing@24333
   789
lemma ucast_slice1: "ucast w = slice1 (size w) w"
kleing@24333
   790
  unfolding slice1_def ucast_bl
kleing@24333
   791
  by (simp add : takefill_same' word_size)
kleing@24333
   792
kleing@24333
   793
lemma ucast_slice: "ucast w = slice 0 w"
kleing@24333
   794
  unfolding slice_def by (simp add : ucast_slice1)
kleing@24333
   795
kleing@24333
   796
lemmas slice_id = trans [OF ucast_slice [symmetric] ucast_id]
kleing@24333
   797
kleing@24333
   798
lemma revcast_slice1': 
kleing@24333
   799
  "rc = revcast w ==> slice1 (size rc) w = rc"
kleing@24333
   800
  unfolding slice1_def revcast_def' by (simp add : word_size)
kleing@24333
   801
kleing@24333
   802
lemmas revcast_slice1 = refl [THEN revcast_slice1']
kleing@24333
   803
kleing@24333
   804
lemma slice1_tf_tf': 
huffman@24465
   805
  "to_bl (slice1 n w :: 'a :: len0 word) = 
huffman@24465
   806
   rev (takefill False (len_of TYPE('a)) (rev (takefill False n (to_bl w))))"
kleing@24333
   807
  unfolding slice1_def by (rule word_rev_tf)
kleing@24333
   808
kleing@24333
   809
lemmas slice1_tf_tf = slice1_tf_tf'
kleing@24333
   810
  [THEN word_bl.Rep_inverse', symmetric, standard]
kleing@24333
   811
kleing@24333
   812
lemma rev_slice1:
huffman@24465
   813
  "n + k = len_of TYPE('a) + len_of TYPE('b) \<Longrightarrow> 
huffman@24465
   814
  slice1 n (word_reverse w :: 'b :: len0 word) = 
huffman@24465
   815
  word_reverse (slice1 k w :: 'a :: len0 word)"
kleing@24333
   816
  apply (unfold word_reverse_def slice1_tf_tf)
kleing@24333
   817
  apply (rule word_bl.Rep_inverse')
kleing@24333
   818
  apply (rule rev_swap [THEN iffD1])
kleing@24333
   819
  apply (rule trans [symmetric])
kleing@24333
   820
  apply (rule tf_rev)
kleing@24333
   821
   apply (simp add: word_bl.Abs_inverse)
kleing@24333
   822
  apply (simp add: word_bl.Abs_inverse)
kleing@24333
   823
  done
kleing@24333
   824
kleing@24333
   825
lemma rev_slice': 
kleing@24333
   826
  "res = slice n (word_reverse w) ==> n + k + size res = size w ==> 
kleing@24333
   827
    res = word_reverse (slice k w)"
kleing@24333
   828
  apply (unfold slice_def word_size)
kleing@24333
   829
  apply clarify
kleing@24333
   830
  apply (rule rev_slice1)
kleing@24333
   831
  apply arith
kleing@24333
   832
  done
kleing@24333
   833
kleing@24333
   834
lemmas rev_slice = refl [THEN rev_slice', unfolded word_size]
kleing@24333
   835
kleing@24333
   836
lemmas sym_notr = 
kleing@24333
   837
  not_iff [THEN iffD2, THEN not_sym, THEN not_iff [THEN iffD1]]
kleing@24333
   838
kleing@24333
   839
-- {* problem posed by TPHOLs referee:
kleing@24333
   840
      criterion for overflow of addition of signed integers *}
kleing@24333
   841
kleing@24333
   842
lemma sofl_test:
huffman@24465
   843
  "(sint (x :: 'a :: len word) + sint y = sint (x + y)) = 
kleing@24333
   844
     ((((x+y) XOR x) AND ((x+y) XOR y)) >> (size x - 1) = 0)"
kleing@24333
   845
  apply (unfold word_size)
huffman@24465
   846
  apply (cases "len_of TYPE('a)", simp) 
kleing@24333
   847
  apply (subst msb_shift [THEN sym_notr])
kleing@24333
   848
  apply (simp add: word_ops_msb)
kleing@24333
   849
  apply (simp add: word_msb_sint)
kleing@24333
   850
  apply safe
kleing@24333
   851
       apply simp_all
kleing@24333
   852
     apply (unfold sint_word_ariths)
kleing@24333
   853
     apply (unfold word_sbin.set_iff_norm [symmetric] sints_num)
kleing@24333
   854
     apply safe
kleing@24333
   855
        apply (insert sint_range' [where x=x])
kleing@24333
   856
        apply (insert sint_range' [where x=y])
kleing@24333
   857
        defer 
kleing@24333
   858
        apply (simp (no_asm), arith)
kleing@24333
   859
       apply (simp (no_asm), arith)
kleing@24333
   860
      defer
kleing@24333
   861
      defer
kleing@24333
   862
      apply (simp (no_asm), arith)
kleing@24333
   863
     apply (simp (no_asm), arith)
kleing@24333
   864
    apply (rule notI [THEN notnotD],
kleing@24333
   865
           drule leI not_leE,
kleing@24333
   866
           drule sbintrunc_inc sbintrunc_dec,      
kleing@24333
   867
           simp)+
kleing@24333
   868
  done
kleing@24333
   869
kleing@24333
   870
huffman@24350
   871
subsection "Split and cat"
kleing@24333
   872
kleing@24333
   873
lemmas word_split_bin' = word_split_def [THEN meta_eq_to_obj_eq, standard]
kleing@24333
   874
lemmas word_cat_bin' = word_cat_def [THEN meta_eq_to_obj_eq, standard]
kleing@24333
   875
kleing@24333
   876
lemma word_rsplit_no:
huffman@24465
   877
  "(word_rsplit (number_of bin :: 'b :: len0 word) :: 'a word list) = 
huffman@24465
   878
    map number_of (bin_rsplit (len_of TYPE('a :: len)) 
huffman@24465
   879
      (len_of TYPE('b), bintrunc (len_of TYPE('b)) bin))"
kleing@24333
   880
  apply (unfold word_rsplit_def word_no_wi)
kleing@24333
   881
  apply (simp add: word_ubin.eq_norm)
kleing@24333
   882
  done
kleing@24333
   883
kleing@24333
   884
lemmas word_rsplit_no_cl [simp] = word_rsplit_no
kleing@24333
   885
  [unfolded bin_rsplitl_def bin_rsplit_l [symmetric]]
kleing@24333
   886
kleing@24333
   887
lemma test_bit_cat:
kleing@24333
   888
  "wc = word_cat a b ==> wc !! n = (n < size wc & 
kleing@24333
   889
    (if n < size b then b !! n else a !! (n - size b)))"
kleing@24333
   890
  apply (unfold word_cat_bin' test_bit_bin)
kleing@24333
   891
  apply (auto simp add : word_ubin.eq_norm nth_bintr bin_nth_cat word_size)
kleing@24333
   892
  apply (erule bin_nth_uint_imp)
kleing@24333
   893
  done
kleing@24333
   894
kleing@24333
   895
lemma word_cat_bl: "word_cat a b = of_bl (to_bl a @ to_bl b)"
kleing@24333
   896
  apply (unfold of_bl_def to_bl_def word_cat_bin')
kleing@24333
   897
  apply (simp add: bl_to_bin_app_cat)
kleing@24333
   898
  done
kleing@24333
   899
kleing@24333
   900
lemma of_bl_append:
huffman@24465
   901
  "(of_bl (xs @ ys) :: 'a :: len word) = of_bl xs * 2^(length ys) + of_bl ys"
kleing@24333
   902
  apply (unfold of_bl_def)
kleing@24333
   903
  apply (simp add: bl_to_bin_app_cat bin_cat_num)
kleing@24333
   904
  apply (simp add: word_of_int_power_hom [symmetric] new_word_of_int_hom_syms)
kleing@24333
   905
  done
kleing@24333
   906
kleing@24333
   907
lemma of_bl_False [simp]:
kleing@24333
   908
  "of_bl (False#xs) = of_bl xs"
kleing@24333
   909
  by (rule word_eqI)
kleing@24333
   910
     (auto simp add: test_bit_of_bl nth_append)
kleing@24333
   911
kleing@24333
   912
lemma of_bl_True: 
huffman@24465
   913
  "(of_bl (True#xs)::'a::len word) = 2^length xs + of_bl xs"
kleing@24333
   914
  by (subst of_bl_append [where xs="[True]", simplified])
kleing@24333
   915
     (simp add: word_1_bl)
kleing@24333
   916
kleing@24333
   917
lemma of_bl_Cons:
kleing@24333
   918
  "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
kleing@24333
   919
  by (cases x) (simp_all add: of_bl_True)
kleing@24333
   920
huffman@24465
   921
lemma split_uint_lem: "bin_split n (uint (w :: 'a :: len0 word)) = (a, b) ==> 
huffman@24465
   922
  a = bintrunc (len_of TYPE('a) - n) a & b = bintrunc (len_of TYPE('a)) b"
kleing@24333
   923
  apply (frule word_ubin.norm_Rep [THEN ssubst])
kleing@24333
   924
  apply (drule bin_split_trunc1)
kleing@24333
   925
  apply (drule sym [THEN trans])
kleing@24333
   926
  apply assumption
kleing@24333
   927
  apply safe
kleing@24333
   928
  done
kleing@24333
   929
kleing@24333
   930
lemma word_split_bl': 
kleing@24333
   931
  "std = size c - size b ==> (word_split c = (a, b)) ==> 
kleing@24333
   932
    (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c)))"
kleing@24333
   933
  apply (unfold word_split_bin')
kleing@24333
   934
  apply safe
kleing@24333
   935
   defer
kleing@24333
   936
   apply (clarsimp split: prod.splits)
kleing@24333
   937
   apply (drule word_ubin.norm_Rep [THEN ssubst])
kleing@24333
   938
   apply (drule split_bintrunc)
kleing@24333
   939
   apply (simp add : of_bl_def bl2bin_drop word_size
kleing@24333
   940
       word_ubin.norm_eq_iff [symmetric] min_def del : word_ubin.norm_Rep)    
kleing@24333
   941
  apply (clarsimp split: prod.splits)
kleing@24333
   942
  apply (frule split_uint_lem [THEN conjunct1])
kleing@24333
   943
  apply (unfold word_size)
huffman@24465
   944
  apply (cases "len_of TYPE('a) >= len_of TYPE('b)")
kleing@24333
   945
   defer
kleing@24333
   946
   apply (simp add: word_0_bl word_0_wi_Pls)
kleing@24333
   947
  apply (simp add : of_bl_def to_bl_def)
kleing@24333
   948
  apply (subst bin_split_take1 [symmetric])
kleing@24333
   949
    prefer 2
kleing@24333
   950
    apply assumption
kleing@24333
   951
   apply simp
kleing@24333
   952
  apply (erule thin_rl)
kleing@24333
   953
  apply (erule arg_cong [THEN trans])
kleing@24333
   954
  apply (simp add : word_ubin.norm_eq_iff [symmetric])
kleing@24333
   955
  done
kleing@24333
   956
kleing@24333
   957
lemma word_split_bl: "std = size c - size b ==> 
kleing@24333
   958
    (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c))) <-> 
kleing@24333
   959
    word_split c = (a, b)"
kleing@24333
   960
  apply (rule iffI)
kleing@24333
   961
   defer
kleing@24333
   962
   apply (erule (1) word_split_bl')
kleing@24333
   963
  apply (case_tac "word_split c")
kleing@24333
   964
  apply (auto simp add : word_size)
kleing@24333
   965
  apply (frule word_split_bl' [rotated])
kleing@24333
   966
  apply (auto simp add : word_size)
kleing@24333
   967
  done
kleing@24333
   968
kleing@24333
   969
lemma word_split_bl_eq:
huffman@24465
   970
   "(word_split (c::'a::len word) :: ('c :: len0 word * 'd :: len0 word)) =
huffman@24465
   971
      (of_bl (take (len_of TYPE('a::len) - len_of TYPE('d::len0)) (to_bl c)),
huffman@24465
   972
       of_bl (drop (len_of TYPE('a) - len_of TYPE('d)) (to_bl c)))"
kleing@24333
   973
  apply (rule word_split_bl [THEN iffD1])
kleing@24333
   974
  apply (unfold word_size)
kleing@24333
   975
  apply (rule refl conjI)+
kleing@24333
   976
  done
kleing@24333
   977
kleing@24333
   978
-- "keep quantifiers for use in simplification"
kleing@24333
   979
lemma test_bit_split':
kleing@24333
   980
  "word_split c = (a, b) --> (ALL n m. b !! n = (n < size b & c !! n) & 
kleing@24333
   981
    a !! m = (m < size a & c !! (m + size b)))"
kleing@24333
   982
  apply (unfold word_split_bin' test_bit_bin)
kleing@24333
   983
  apply (clarify)
kleing@24333
   984
  apply (clarsimp simp: word_ubin.eq_norm nth_bintr word_size split: prod.splits)
kleing@24333
   985
  apply (drule bin_nth_split)
kleing@24333
   986
  apply safe
kleing@24333
   987
       apply (simp_all add: add_commute)
kleing@24333
   988
   apply (erule bin_nth_uint_imp)+
kleing@24333
   989
  done
kleing@24333
   990
kleing@24333
   991
lemmas test_bit_split = 
kleing@24333
   992
  test_bit_split' [THEN mp, simplified all_simps, standard]
kleing@24333
   993
kleing@24333
   994
lemma test_bit_split_eq: "word_split c = (a, b) <-> 
kleing@24333
   995
  ((ALL n::nat. b !! n = (n < size b & c !! n)) &
kleing@24333
   996
    (ALL m::nat. a !! m = (m < size a & c !! (m + size b))))"
kleing@24333
   997
  apply (rule_tac iffI)
kleing@24333
   998
   apply (rule_tac conjI)
kleing@24333
   999
    apply (erule test_bit_split [THEN conjunct1])
kleing@24333
  1000
   apply (erule test_bit_split [THEN conjunct2])
kleing@24333
  1001
  apply (case_tac "word_split c")
kleing@24333
  1002
  apply (frule test_bit_split)
kleing@24333
  1003
  apply (erule trans)
kleing@24333
  1004
  apply (fastsimp intro ! : word_eqI simp add : word_size)
kleing@24333
  1005
  done
kleing@24333
  1006
wenzelm@26008
  1007
-- {* this odd result is analogous to @{text "ucast_id"}, 
kleing@24333
  1008
      result to the length given by the result type *}
kleing@24333
  1009
kleing@24333
  1010
lemma word_cat_id: "word_cat a b = b"
kleing@24333
  1011
  unfolding word_cat_bin' by (simp add: word_ubin.inverse_norm)
kleing@24333
  1012
kleing@24333
  1013
-- "limited hom result"
kleing@24333
  1014
lemma word_cat_hom:
huffman@24465
  1015
  "len_of TYPE('a::len0) <= len_of TYPE('b::len0) + len_of TYPE ('c::len0)
kleing@24333
  1016
  ==>
kleing@24333
  1017
  (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) = 
kleing@24333
  1018
  word_of_int (bin_cat w (size b) (uint b))"
kleing@24333
  1019
  apply (unfold word_cat_def word_size) 
kleing@24333
  1020
  apply (clarsimp simp add : word_ubin.norm_eq_iff [symmetric]
kleing@24333
  1021
      word_ubin.eq_norm bintr_cat min_def)
huffman@24465
  1022
  apply arith
kleing@24333
  1023
  done
kleing@24333
  1024
kleing@24333
  1025
lemma word_cat_split_alt:
kleing@24333
  1026
  "size w <= size u + size v ==> word_split w = (u, v) ==> word_cat u v = w"
kleing@24333
  1027
  apply (rule word_eqI)
kleing@24333
  1028
  apply (drule test_bit_split)
kleing@24333
  1029
  apply (clarsimp simp add : test_bit_cat word_size)
kleing@24333
  1030
  apply safe
kleing@24333
  1031
  apply arith
kleing@24333
  1032
  done
kleing@24333
  1033
kleing@24333
  1034
lemmas word_cat_split_size = 
kleing@24333
  1035
  sym [THEN [2] word_cat_split_alt [symmetric], standard]
kleing@24333
  1036
kleing@24333
  1037
huffman@24350
  1038
subsubsection "Split and slice"
kleing@24333
  1039
kleing@24333
  1040
lemma split_slices: 
kleing@24333
  1041
  "word_split w = (u, v) ==> u = slice (size v) w & v = slice 0 w"
kleing@24333
  1042
  apply (drule test_bit_split)
kleing@24333
  1043
  apply (rule conjI)
kleing@24333
  1044
   apply (rule word_eqI, clarsimp simp: nth_slice word_size)+
kleing@24333
  1045
  done
kleing@24333
  1046
kleing@24333
  1047
lemma slice_cat1':
kleing@24333
  1048
  "wc = word_cat a b ==> size wc >= size a + size b ==> slice (size b) wc = a"
kleing@24333
  1049
  apply safe
kleing@24333
  1050
  apply (rule word_eqI)
kleing@24333
  1051
  apply (simp add: nth_slice test_bit_cat word_size)
kleing@24333
  1052
  done
kleing@24333
  1053
kleing@24333
  1054
lemmas slice_cat1 = refl [THEN slice_cat1']
kleing@24333
  1055
lemmas slice_cat2 = trans [OF slice_id word_cat_id]
kleing@24333
  1056
kleing@24333
  1057
lemma cat_slices:
wenzelm@26008
  1058
  "a = slice n c ==> b = slice 0 c ==> n = size b ==>
kleing@24333
  1059
    size a + size b >= size c ==> word_cat a b = c"
kleing@24333
  1060
  apply safe
kleing@24333
  1061
  apply (rule word_eqI)
kleing@24333
  1062
  apply (simp add: nth_slice test_bit_cat word_size)
kleing@24333
  1063
  apply safe
kleing@24333
  1064
  apply arith
kleing@24333
  1065
  done
kleing@24333
  1066
kleing@24333
  1067
lemma word_split_cat_alt:
kleing@24333
  1068
  "w = word_cat u v ==> size u + size v <= size w ==> word_split w = (u, v)"
kleing@24333
  1069
  apply (case_tac "word_split ?w")
kleing@24333
  1070
  apply (rule trans, assumption)
kleing@24333
  1071
  apply (drule test_bit_split)
kleing@24333
  1072
  apply safe
kleing@24333
  1073
   apply (rule word_eqI, clarsimp simp: test_bit_cat word_size)+
kleing@24333
  1074
  done
kleing@24333
  1075
kleing@24333
  1076
lemmas word_cat_bl_no_bin [simp] =
wenzelm@25350
  1077
  word_cat_bl [where a="number_of a" 
wenzelm@25350
  1078
                 and b="number_of b", 
wenzelm@25350
  1079
               unfolded to_bl_no_bin, standard]
kleing@24333
  1080
kleing@24333
  1081
lemmas word_split_bl_no_bin [simp] =
wenzelm@25350
  1082
  word_split_bl_eq [where c="number_of c", unfolded to_bl_no_bin, standard]
kleing@24333
  1083
kleing@24333
  1084
-- {* this odd result arises from the fact that the statement of the
kleing@24333
  1085
      result implies that the decoded words are of the same type, 
kleing@24333
  1086
      and therefore of the same length, as the original word *}
kleing@24333
  1087
kleing@24333
  1088
lemma word_rsplit_same: "word_rsplit w = [w]"
kleing@24333
  1089
  unfolding word_rsplit_def by (simp add : bin_rsplit_all)
kleing@24333
  1090
kleing@24333
  1091
lemma word_rsplit_empty_iff_size:
kleing@24333
  1092
  "(word_rsplit w = []) = (size w = 0)" 
kleing@24333
  1093
  unfolding word_rsplit_def bin_rsplit_def word_size
wenzelm@26289
  1094
  by (simp add: bin_rsplit_aux_simp_alt Let_def split: Product_Type.split_split)
kleing@24333
  1095
kleing@24333
  1096
lemma test_bit_rsplit:
huffman@24465
  1097
  "sw = word_rsplit w ==> m < size (hd sw :: 'a :: len word) ==> 
kleing@24333
  1098
    k < length sw ==> (rev sw ! k) !! m = (w !! (k * size (hd sw) + m))"
kleing@24333
  1099
  apply (unfold word_rsplit_def word_test_bit_def)
kleing@24333
  1100
  apply (rule trans)
kleing@24333
  1101
   apply (rule_tac f = "%x. bin_nth x m" in arg_cong)
kleing@24333
  1102
   apply (rule nth_map [symmetric])
kleing@24333
  1103
   apply simp
kleing@24333
  1104
  apply (rule bin_nth_rsplit)
kleing@24333
  1105
     apply simp_all
kleing@24333
  1106
  apply (simp add : word_size rev_map map_compose [symmetric])
kleing@24333
  1107
  apply (rule trans)
kleing@24333
  1108
   defer
kleing@24333
  1109
   apply (rule map_ident [THEN fun_cong])
kleing@24333
  1110
  apply (rule refl [THEN map_cong])
kleing@24333
  1111
  apply (simp add : word_ubin.eq_norm)
huffman@24465
  1112
  apply (erule bin_rsplit_size_sign [OF len_gt_0 refl])
kleing@24333
  1113
  done
kleing@24333
  1114
kleing@24333
  1115
lemma word_rcat_bl: "word_rcat wl == of_bl (concat (map to_bl wl))"
kleing@24333
  1116
  unfolding word_rcat_def to_bl_def' of_bl_def
kleing@24333
  1117
  by (clarsimp simp add : bin_rcat_bl map_compose)
kleing@24333
  1118
kleing@24333
  1119
lemma size_rcat_lem':
kleing@24333
  1120
  "size (concat (map to_bl wl)) = length wl * size (hd wl)"
kleing@24333
  1121
  unfolding word_size by (induct wl) auto
kleing@24333
  1122
kleing@24333
  1123
lemmas size_rcat_lem = size_rcat_lem' [unfolded word_size]
kleing@24333
  1124
huffman@24465
  1125
lemmas td_gal_lt_len = len_gt_0 [THEN td_gal_lt, standard]
kleing@24333
  1126
kleing@24333
  1127
lemma nth_rcat_lem' [rule_format] :
huffman@24465
  1128
  "sw = size (hd wl  :: 'a :: len word) ==> (ALL n. n < size wl * sw --> 
kleing@24333
  1129
    rev (concat (map to_bl wl)) ! n = 
kleing@24333
  1130
    rev (to_bl (rev wl ! (n div sw))) ! (n mod sw))"
kleing@24333
  1131
  apply (unfold word_size)
kleing@24333
  1132
  apply (induct "wl")
kleing@24333
  1133
   apply clarsimp
kleing@24333
  1134
  apply (clarsimp simp add : nth_append size_rcat_lem)
kleing@24333
  1135
  apply (simp (no_asm_use) only:  mult_Suc [symmetric] 
kleing@24333
  1136
         td_gal_lt_len less_Suc_eq_le mod_div_equality')
kleing@24333
  1137
  apply clarsimp
kleing@24333
  1138
  done
kleing@24333
  1139
kleing@24333
  1140
lemmas nth_rcat_lem = refl [THEN nth_rcat_lem', unfolded word_size]
kleing@24333
  1141
kleing@24333
  1142
lemma test_bit_rcat:
huffman@24465
  1143
  "sw = size (hd wl :: 'a :: len word) ==> rc = word_rcat wl ==> rc !! n = 
kleing@24333
  1144
    (n < size rc & n div sw < size wl & (rev wl) ! (n div sw) !! (n mod sw))"
kleing@24333
  1145
  apply (unfold word_rcat_bl word_size)
kleing@24333
  1146
  apply (clarsimp simp add : 
kleing@24333
  1147
    test_bit_of_bl size_rcat_lem word_size td_gal_lt_len)
kleing@24333
  1148
  apply safe
kleing@24333
  1149
   apply (auto simp add : 
kleing@24333
  1150
    test_bit_bl word_size td_gal_lt_len [THEN iffD2, THEN nth_rcat_lem])
kleing@24333
  1151
  done
kleing@24333
  1152
kleing@24333
  1153
lemma foldl_eq_foldr [rule_format] :
kleing@24333
  1154
  "ALL x. foldl op + x xs = foldr op + (x # xs) (0 :: 'a :: comm_monoid_add)" 
kleing@24333
  1155
  by (induct xs) (auto simp add : add_assoc)
kleing@24333
  1156
kleing@24333
  1157
lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong]
kleing@24333
  1158
kleing@24333