src/HOL/Word/Bool_List_Representation.thy
author wenzelm
Sun Sep 18 20:33:48 2016 +0200 (2016-09-18)
changeset 63915 bab633745c7f
parent 63648 f9f3006a5579
child 64507 eace715f4988
permissions -rw-r--r--
tuned proofs;
kleing@24333
     1
(* 
kleing@24333
     2
  Author: Jeremy Dawson, NICTA
kleing@24333
     3
kleing@44939
     4
  Theorems to do with integers, expressed using Pls, Min, BIT,
kleing@24333
     5
  theorems linking them to lists of booleans, and repeated splitting 
kleing@24333
     6
  and concatenation.
kleing@24333
     7
*) 
kleing@24333
     8
wenzelm@58874
     9
section "Bool lists and integers"
kleing@24333
    10
haftmann@37658
    11
theory Bool_List_Representation
eberlm@63501
    12
imports Complex_Main Bits_Int
haftmann@26557
    13
begin
kleing@24333
    14
haftmann@53062
    15
definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
haftmann@53062
    16
where
haftmann@61424
    17
  "map2 f as bs = map (case_prod f) (zip as bs)"
haftmann@53062
    18
haftmann@53062
    19
lemma map2_Nil [simp, code]:
haftmann@53062
    20
  "map2 f [] ys = []"
haftmann@53062
    21
  unfolding map2_def by auto
haftmann@53062
    22
haftmann@53062
    23
lemma map2_Nil2 [simp, code]:
haftmann@53062
    24
  "map2 f xs [] = []"
haftmann@53062
    25
  unfolding map2_def by auto
haftmann@53062
    26
haftmann@53062
    27
lemma map2_Cons [simp, code]:
haftmann@53062
    28
  "map2 f (x # xs) (y # ys) = f x y # map2 f xs ys"
haftmann@53062
    29
  unfolding map2_def by auto
haftmann@53062
    30
haftmann@53062
    31
wenzelm@61799
    32
subsection \<open>Operations on lists of booleans\<close>
haftmann@37657
    33
haftmann@54848
    34
primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int"
haftmann@54848
    35
where
haftmann@37657
    36
  Nil: "bl_to_bin_aux [] w = w"
haftmann@37657
    37
  | Cons: "bl_to_bin_aux (b # bs) w = 
haftmann@54847
    38
      bl_to_bin_aux bs (w BIT b)"
haftmann@37657
    39
haftmann@54848
    40
definition bl_to_bin :: "bool list \<Rightarrow> int"
haftmann@54848
    41
where
huffman@46001
    42
  bl_to_bin_def: "bl_to_bin bs = bl_to_bin_aux bs 0"
haftmann@37667
    43
haftmann@54848
    44
primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list"
haftmann@54848
    45
where
haftmann@37657
    46
  Z: "bin_to_bl_aux 0 w bl = bl"
haftmann@37657
    47
  | Suc: "bin_to_bl_aux (Suc n) w bl =
haftmann@54847
    48
      bin_to_bl_aux n (bin_rest w) ((bin_last w) # bl)"
haftmann@37657
    49
haftmann@54848
    50
definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list"
haftmann@54848
    51
where
haftmann@37657
    52
  bin_to_bl_def : "bin_to_bl n w = bin_to_bl_aux n w []"
haftmann@37657
    53
haftmann@54848
    54
primrec bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool list"
haftmann@54848
    55
where
haftmann@37657
    56
  Suc: "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
haftmann@37657
    57
  | Z: "bl_of_nth 0 f = []"
haftmann@37657
    58
haftmann@54848
    59
primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
haftmann@54848
    60
where
haftmann@37657
    61
  Z: "takefill fill 0 xs = []"
haftmann@37657
    62
  | Suc: "takefill fill (Suc n) xs = (
haftmann@37657
    63
      case xs of [] => fill # takefill fill n xs
haftmann@37657
    64
        | y # ys => y # takefill fill n ys)"
haftmann@37657
    65
haftmann@37657
    66
huffman@24465
    67
subsection "Arithmetic in terms of bool lists"
huffman@24465
    68
wenzelm@61799
    69
text \<open>
kleing@44939
    70
  Arithmetic operations in terms of the reversed bool list,
kleing@44939
    71
  assuming input list(s) the same length, and don't extend them. 
wenzelm@61799
    72
\<close>
huffman@24465
    73
haftmann@54848
    74
primrec rbl_succ :: "bool list => bool list"
haftmann@54848
    75
where
huffman@24465
    76
  Nil: "rbl_succ Nil = Nil"
haftmann@26557
    77
  | Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)"
huffman@24465
    78
haftmann@54848
    79
primrec rbl_pred :: "bool list => bool list"
haftmann@54848
    80
where
haftmann@26557
    81
  Nil: "rbl_pred Nil = Nil"
haftmann@26557
    82
  | Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)"
huffman@24465
    83
haftmann@54848
    84
primrec rbl_add :: "bool list => bool list => bool list"
haftmann@54848
    85
where
wenzelm@61799
    86
  \<comment> "result is length of first arg, second arg may be longer"
haftmann@26557
    87
  Nil: "rbl_add Nil x = Nil"
haftmann@26557
    88
  | Cons: "rbl_add (y # ys) x = (let ws = rbl_add ys (tl x) in 
huffman@24465
    89
    (y ~= hd x) # (if hd x & y then rbl_succ ws else ws))"
huffman@24465
    90
haftmann@54848
    91
primrec rbl_mult :: "bool list => bool list => bool list"
haftmann@54848
    92
where
wenzelm@61799
    93
  \<comment> "result is length of first arg, second arg may be longer"
haftmann@26557
    94
  Nil: "rbl_mult Nil x = Nil"
haftmann@26557
    95
  | Cons: "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in 
huffman@24465
    96
    if y then rbl_add ws x else ws)"
kleing@24333
    97
kleing@24333
    98
lemma butlast_power:
haftmann@30971
    99
  "(butlast ^^ n) bl = take (length bl - n) bl"
kleing@24333
   100
  by (induct n) (auto simp: butlast_take)
kleing@24333
   101
huffman@46001
   102
lemma bin_to_bl_aux_zero_minus_simp [simp]:
huffman@46001
   103
  "0 < n \<Longrightarrow> bin_to_bl_aux n 0 bl = 
huffman@46001
   104
    bin_to_bl_aux (n - 1) 0 (False # bl)"
huffman@46001
   105
  by (cases n) auto
huffman@46001
   106
huffman@46617
   107
lemma bin_to_bl_aux_minus1_minus_simp [simp]:
haftmann@58410
   108
  "0 < n ==> bin_to_bl_aux n (- 1) bl = 
haftmann@58410
   109
    bin_to_bl_aux (n - 1) (- 1) (True # bl)"
kleing@24333
   110
  by (cases n) auto
kleing@24333
   111
huffman@46617
   112
lemma bin_to_bl_aux_one_minus_simp [simp]:
huffman@46617
   113
  "0 < n \<Longrightarrow> bin_to_bl_aux n 1 bl = 
huffman@46617
   114
    bin_to_bl_aux (n - 1) 0 (True # bl)"
kleing@24333
   115
  by (cases n) auto
kleing@24333
   116
huffman@26086
   117
lemma bin_to_bl_aux_Bit_minus_simp [simp]:
kleing@24333
   118
  "0 < n ==> bin_to_bl_aux n (w BIT b) bl = 
haftmann@54847
   119
    bin_to_bl_aux (n - 1) w (b # bl)"
kleing@24333
   120
  by (cases n) auto
kleing@24333
   121
huffman@26086
   122
lemma bin_to_bl_aux_Bit0_minus_simp [simp]:
huffman@47108
   123
  "0 < n ==> bin_to_bl_aux n (numeral (Num.Bit0 w)) bl = 
huffman@47108
   124
    bin_to_bl_aux (n - 1) (numeral w) (False # bl)"
huffman@26086
   125
  by (cases n) auto
huffman@26086
   126
huffman@26086
   127
lemma bin_to_bl_aux_Bit1_minus_simp [simp]:
huffman@47108
   128
  "0 < n ==> bin_to_bl_aux n (numeral (Num.Bit1 w)) bl = 
huffman@47108
   129
    bin_to_bl_aux (n - 1) (numeral w) (True # bl)"
huffman@26086
   130
  by (cases n) auto
kleing@24333
   131
wenzelm@61799
   132
text \<open>Link between bin and bool list.\<close>
huffman@24465
   133
haftmann@26557
   134
lemma bl_to_bin_aux_append: 
haftmann@26557
   135
  "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)"
haftmann@26557
   136
  by (induct bs arbitrary: w) auto
huffman@24465
   137
haftmann@26557
   138
lemma bin_to_bl_aux_append: 
haftmann@26557
   139
  "bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)"
haftmann@26557
   140
  by (induct n arbitrary: w bs) auto
kleing@24333
   141
huffman@24465
   142
lemma bl_to_bin_append: 
haftmann@26557
   143
  "bl_to_bin (bs @ cs) = bl_to_bin_aux cs (bl_to_bin bs)"
huffman@24465
   144
  unfolding bl_to_bin_def by (rule bl_to_bin_aux_append)
huffman@24465
   145
kleing@24333
   146
lemma bin_to_bl_aux_alt: 
kleing@24333
   147
  "bin_to_bl_aux n w bs = bin_to_bl n w @ bs" 
kleing@24333
   148
  unfolding bin_to_bl_def by (simp add : bin_to_bl_aux_append)
kleing@24333
   149
huffman@45996
   150
lemma bin_to_bl_0 [simp]: "bin_to_bl 0 bs = []"
kleing@24333
   151
  unfolding bin_to_bl_def by auto
kleing@24333
   152
haftmann@26557
   153
lemma size_bin_to_bl_aux: 
haftmann@26557
   154
  "size (bin_to_bl_aux n w bs) = n + length bs"
haftmann@26557
   155
  by (induct n arbitrary: w bs) auto
kleing@24333
   156
huffman@45996
   157
lemma size_bin_to_bl [simp]: "size (bin_to_bl n w) = n" 
kleing@24333
   158
  unfolding bin_to_bl_def by (simp add : size_bin_to_bl_aux)
kleing@24333
   159
haftmann@26557
   160
lemma bin_bl_bin': 
haftmann@26557
   161
  "bl_to_bin (bin_to_bl_aux n w bs) = 
haftmann@26557
   162
    bl_to_bin_aux bs (bintrunc n w)"
haftmann@26557
   163
  by (induct n arbitrary: w bs) (auto simp add : bl_to_bin_def)
huffman@24465
   164
huffman@45996
   165
lemma bin_bl_bin [simp]: "bl_to_bin (bin_to_bl n w) = bintrunc n w"
huffman@24465
   166
  unfolding bin_to_bl_def bin_bl_bin' by auto
huffman@24465
   167
haftmann@26557
   168
lemma bl_bin_bl':
haftmann@26557
   169
  "bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = 
huffman@24465
   170
    bin_to_bl_aux n w bs"
haftmann@26557
   171
  apply (induct bs arbitrary: w n)
huffman@24465
   172
   apply auto
huffman@24465
   173
    apply (simp_all only : add_Suc [symmetric])
huffman@24465
   174
    apply (auto simp add : bin_to_bl_def)
huffman@24465
   175
  done
huffman@24465
   176
huffman@45996
   177
lemma bl_bin_bl [simp]: "bin_to_bl (length bs) (bl_to_bin bs) = bs"
huffman@24465
   178
  unfolding bl_to_bin_def
huffman@24465
   179
  apply (rule box_equals)
huffman@24465
   180
    apply (rule bl_bin_bl')
huffman@24465
   181
   prefer 2
huffman@24465
   182
   apply (rule bin_to_bl_aux.Z)
huffman@24465
   183
  apply simp
huffman@24465
   184
  done
huffman@24465
   185
  
huffman@24465
   186
lemma bl_to_bin_inj:
huffman@24465
   187
  "bl_to_bin bs = bl_to_bin cs ==> length bs = length cs ==> bs = cs"
huffman@24465
   188
  apply (rule_tac box_equals)
huffman@24465
   189
    defer
huffman@24465
   190
    apply (rule bl_bin_bl)
huffman@24465
   191
   apply (rule bl_bin_bl)
huffman@24465
   192
  apply simp
huffman@24465
   193
  done
huffman@24465
   194
huffman@45996
   195
lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl"
huffman@46001
   196
  unfolding bl_to_bin_def by auto
huffman@45996
   197
huffman@46001
   198
lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = 0"
huffman@24465
   199
  unfolding bl_to_bin_def by auto
huffman@24465
   200
huffman@46001
   201
lemma bin_to_bl_zero_aux: 
huffman@46001
   202
  "bin_to_bl_aux n 0 bl = replicate n False @ bl"
huffman@46001
   203
  by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
huffman@46001
   204
huffman@46617
   205
lemma bin_to_bl_zero: "bin_to_bl n 0 = replicate n False"
huffman@46617
   206
  unfolding bin_to_bl_def by (simp add: bin_to_bl_zero_aux)
huffman@46617
   207
huffman@46617
   208
lemma bin_to_bl_minus1_aux:
haftmann@58410
   209
  "bin_to_bl_aux n (- 1) bl = replicate n True @ bl"
haftmann@26557
   210
  by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
kleing@24333
   211
haftmann@58410
   212
lemma bin_to_bl_minus1: "bin_to_bl n (- 1) = replicate n True"
huffman@46617
   213
  unfolding bin_to_bl_def by (simp add: bin_to_bl_minus1_aux)
kleing@24333
   214
huffman@24465
   215
lemma bl_to_bin_rep_F: 
huffman@24465
   216
  "bl_to_bin (replicate n False @ bl) = bl_to_bin bl"
huffman@46001
   217
  apply (simp add: bin_to_bl_zero_aux [symmetric] bin_bl_bin')
huffman@24465
   218
  apply (simp add: bl_to_bin_def)
huffman@24465
   219
  done
huffman@24465
   220
huffman@45996
   221
lemma bin_to_bl_trunc [simp]:
huffman@24465
   222
  "n <= m ==> bin_to_bl n (bintrunc m w) = bin_to_bl n w"
huffman@24465
   223
  by (auto intro: bl_to_bin_inj)
huffman@24465
   224
huffman@45997
   225
lemma bin_to_bl_aux_bintr:
huffman@45997
   226
  "bin_to_bl_aux n (bintrunc m bin) bl = 
kleing@24333
   227
    replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl"
huffman@45997
   228
  apply (induct n arbitrary: m bin bl)
kleing@24333
   229
   apply clarsimp
kleing@24333
   230
  apply clarsimp
kleing@24333
   231
  apply (case_tac "m")
huffman@46001
   232
   apply (clarsimp simp: bin_to_bl_zero_aux) 
kleing@24333
   233
   apply (erule thin_rl)
kleing@24333
   234
   apply (induct_tac n)   
kleing@24333
   235
    apply auto
kleing@24333
   236
  done
kleing@24333
   237
huffman@45854
   238
lemma bin_to_bl_bintr:
huffman@45854
   239
  "bin_to_bl n (bintrunc m bin) =
huffman@45854
   240
    replicate (n - m) False @ bin_to_bl (min n m) bin"
huffman@45854
   241
  unfolding bin_to_bl_def by (rule bin_to_bl_aux_bintr)
kleing@24333
   242
huffman@46001
   243
lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = 0"
huffman@24465
   244
  by (induct n) auto
huffman@24465
   245
haftmann@26557
   246
lemma len_bin_to_bl_aux: 
haftmann@26557
   247
  "length (bin_to_bl_aux n w bs) = n + length bs"
haftmann@54869
   248
  by (fact size_bin_to_bl_aux)
kleing@24333
   249
kleing@24333
   250
lemma len_bin_to_bl [simp]: "length (bin_to_bl n w) = n"
huffman@46617
   251
  by (fact size_bin_to_bl) (* FIXME: duplicate *)
kleing@24333
   252
  
haftmann@26557
   253
lemma sign_bl_bin': 
haftmann@26557
   254
  "bin_sign (bl_to_bin_aux bs w) = bin_sign w"
haftmann@26557
   255
  by (induct bs arbitrary: w) auto
kleing@24333
   256
  
huffman@46001
   257
lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = 0"
kleing@24333
   258
  unfolding bl_to_bin_def by (simp add : sign_bl_bin')
kleing@24333
   259
  
haftmann@26557
   260
lemma bl_sbin_sign_aux: 
haftmann@26557
   261
  "hd (bin_to_bl_aux (Suc n) w bs) = 
huffman@46001
   262
    (bin_sign (sbintrunc n w) = -1)"
haftmann@26557
   263
  apply (induct n arbitrary: w bs)
kleing@24333
   264
   apply clarsimp
haftmann@26557
   265
   apply (cases w rule: bin_exhaust)
haftmann@54847
   266
   apply simp
kleing@24333
   267
  done
kleing@24333
   268
    
kleing@24333
   269
lemma bl_sbin_sign: 
huffman@46001
   270
  "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)"
kleing@24333
   271
  unfolding bin_to_bl_def by (rule bl_sbin_sign_aux)
kleing@24333
   272
huffman@45997
   273
lemma bin_nth_of_bl_aux:
huffman@45997
   274
  "bin_nth (bl_to_bin_aux bl w) n = 
kleing@24333
   275
    (n < size bl & rev bl ! n | n >= length bl & bin_nth w (n - size bl))"
huffman@45997
   276
  apply (induct bl arbitrary: w)
kleing@24333
   277
   apply clarsimp
kleing@24333
   278
  apply clarsimp
huffman@45997
   279
  apply (cut_tac x=n and y="size bl" in linorder_less_linear)
kleing@24333
   280
  apply (erule disjE, simp add: nth_append)+
haftmann@26557
   281
  apply auto
kleing@24333
   282
  done
kleing@24333
   283
huffman@45475
   284
lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl & rev bl ! n)"
kleing@24333
   285
  unfolding bl_to_bin_def by (simp add : bin_nth_of_bl_aux)
kleing@24333
   286
huffman@45997
   287
lemma bin_nth_bl: "n < m \<Longrightarrow> bin_nth w n = nth (rev (bin_to_bl m w)) n"
huffman@45997
   288
  apply (induct n arbitrary: m w)
kleing@24333
   289
   apply clarsimp
kleing@24333
   290
   apply (case_tac m, clarsimp)
kleing@24333
   291
   apply (clarsimp simp: bin_to_bl_def)
kleing@24333
   292
   apply (simp add: bin_to_bl_aux_alt)
kleing@24333
   293
  apply clarsimp
kleing@24333
   294
  apply (case_tac m, clarsimp)
kleing@24333
   295
  apply (clarsimp simp: bin_to_bl_def)
kleing@24333
   296
  apply (simp add: bin_to_bl_aux_alt)
kleing@24333
   297
  done
kleing@24333
   298
huffman@45997
   299
lemma nth_rev:
huffman@45997
   300
  "n < length xs \<Longrightarrow> rev xs ! n = xs ! (length xs - 1 - n)"
huffman@45997
   301
  apply (induct xs)
huffman@24465
   302
   apply simp
nipkow@63648
   303
  apply (clarsimp simp add : nth_append nth.simps split: nat.split)
huffman@45997
   304
  apply (rule_tac f = "\<lambda>n. xs ! n" in arg_cong)
huffman@24465
   305
  apply arith
huffman@24465
   306
  done
huffman@24465
   307
huffman@45854
   308
lemma nth_rev_alt: "n < length ys \<Longrightarrow> ys ! n = rev ys ! (length ys - Suc n)"
huffman@45854
   309
  by (simp add: nth_rev)
huffman@24465
   310
huffman@45997
   311
lemma nth_bin_to_bl_aux:
huffman@45997
   312
  "n < m + length bl \<Longrightarrow> (bin_to_bl_aux m w bl) ! n = 
kleing@24333
   313
    (if n < m then bin_nth w (m - 1 - n) else bl ! (n - m))"
huffman@45997
   314
  apply (induct m arbitrary: w n bl)
kleing@24333
   315
   apply clarsimp
kleing@24333
   316
  apply clarsimp
kleing@24333
   317
  apply (case_tac w rule: bin_exhaust)
kleing@24333
   318
  apply simp
kleing@24333
   319
  done
huffman@45997
   320
kleing@24333
   321
lemma nth_bin_to_bl: "n < m ==> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)"
kleing@24333
   322
  unfolding bin_to_bl_def by (simp add : nth_bin_to_bl_aux)
kleing@24333
   323
huffman@45997
   324
lemma bl_to_bin_lt2p_aux:
huffman@45997
   325
  "bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)"
huffman@45997
   326
  apply (induct bs arbitrary: w)
kleing@24333
   327
   apply clarsimp
kleing@24333
   328
  apply clarsimp
haftmann@53062
   329
  apply (drule meta_spec, erule xtrans(8) [rotated], simp add: Bit_def)+
kleing@24333
   330
  done
kleing@24333
   331
kleing@62701
   332
lemma bl_to_bin_lt2p_drop:
kleing@62701
   333
  "bl_to_bin bs < 2 ^ length (dropWhile Not bs)"
kleing@62701
   334
proof (induct bs)
kleing@62701
   335
  case (Cons b bs) with bl_to_bin_lt2p_aux[where w=1]
kleing@62701
   336
  show ?case unfolding bl_to_bin_def by simp
kleing@62701
   337
qed simp
kleing@62701
   338
kleing@62701
   339
lemma bl_to_bin_lt2p: "bl_to_bin bs < 2 ^ length bs"
kleing@62701
   340
  by (metis bin_bl_bin bintr_lt2p bl_bin_bl)
kleing@24333
   341
huffman@45997
   342
lemma bl_to_bin_ge2p_aux:
huffman@45997
   343
  "bl_to_bin_aux bs w >= w * (2 ^ length bs)"
huffman@45997
   344
  apply (induct bs arbitrary: w)
kleing@24333
   345
   apply clarsimp
kleing@24333
   346
  apply clarsimp
huffman@46652
   347
   apply (drule meta_spec, erule order_trans [rotated],
huffman@46652
   348
          simp add: Bit_B0_2t Bit_B1_2t algebra_simps)+
haftmann@54847
   349
   apply (simp add: Bit_def)
kleing@24333
   350
  done
kleing@24333
   351
kleing@24333
   352
lemma bl_to_bin_ge0: "bl_to_bin bs >= 0"
kleing@24333
   353
  apply (unfold bl_to_bin_def)
haftmann@53062
   354
  apply (rule xtrans(4))
kleing@24333
   355
   apply (rule bl_to_bin_ge2p_aux)
huffman@46617
   356
  apply simp
kleing@24333
   357
  done
kleing@24333
   358
kleing@24333
   359
lemma butlast_rest_bin: 
kleing@24333
   360
  "butlast (bin_to_bl n w) = bin_to_bl (n - 1) (bin_rest w)"
kleing@24333
   361
  apply (unfold bin_to_bl_def)
kleing@24333
   362
  apply (cases w rule: bin_exhaust)
kleing@24333
   363
  apply (cases n, clarsimp)
kleing@24333
   364
  apply clarsimp
kleing@24333
   365
  apply (auto simp add: bin_to_bl_aux_alt)
kleing@24333
   366
  done
kleing@24333
   367
huffman@45854
   368
lemma butlast_bin_rest:
huffman@45854
   369
  "butlast bl = bin_to_bl (length bl - Suc 0) (bin_rest (bl_to_bin bl))"
huffman@45854
   370
  using butlast_rest_bin [where w="bl_to_bin bl" and n="length bl"] by simp
kleing@24333
   371
haftmann@26557
   372
lemma butlast_rest_bl2bin_aux:
haftmann@26557
   373
  "bl ~= [] \<Longrightarrow>
haftmann@26557
   374
    bl_to_bin_aux (butlast bl) w = bin_rest (bl_to_bin_aux bl w)"
haftmann@26557
   375
  by (induct bl arbitrary: w) auto
kleing@24333
   376
  
kleing@24333
   377
lemma butlast_rest_bl2bin: 
kleing@24333
   378
  "bl_to_bin (butlast bl) = bin_rest (bl_to_bin bl)"
kleing@24333
   379
  apply (unfold bl_to_bin_def)
kleing@24333
   380
  apply (cases bl)
kleing@24333
   381
   apply (auto simp add: butlast_rest_bl2bin_aux)
kleing@24333
   382
  done
kleing@24333
   383
huffman@45997
   384
lemma trunc_bl2bin_aux:
huffman@45997
   385
  "bintrunc m (bl_to_bin_aux bl w) = 
haftmann@26557
   386
    bl_to_bin_aux (drop (length bl - m) bl) (bintrunc (m - length bl) w)"
haftmann@53438
   387
proof (induct bl arbitrary: w)
haftmann@53438
   388
  case Nil show ?case by simp
haftmann@53438
   389
next
haftmann@53438
   390
  case (Cons b bl) show ?case
haftmann@53438
   391
  proof (cases "m - length bl")
haftmann@53438
   392
    case 0 then have "Suc (length bl) - m = Suc (length bl - m)" by simp
haftmann@53438
   393
    with Cons show ?thesis by simp
haftmann@53438
   394
  next
haftmann@53438
   395
    case (Suc n) then have *: "m - Suc (length bl) = n" by simp
haftmann@53438
   396
    with Suc Cons show ?thesis by simp
haftmann@53438
   397
  qed
haftmann@53438
   398
qed
kleing@24333
   399
kleing@24333
   400
lemma trunc_bl2bin: 
kleing@24333
   401
  "bintrunc m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)"
kleing@24333
   402
  unfolding bl_to_bin_def by (simp add : trunc_bl2bin_aux)
kleing@24333
   403
  
huffman@45854
   404
lemma trunc_bl2bin_len [simp]:
huffman@45854
   405
  "bintrunc (length bl) (bl_to_bin bl) = bl_to_bin bl"
huffman@45854
   406
  by (simp add: trunc_bl2bin)
kleing@24333
   407
kleing@24333
   408
lemma bl2bin_drop: 
kleing@24333
   409
  "bl_to_bin (drop k bl) = bintrunc (length bl - k) (bl_to_bin bl)"
kleing@24333
   410
  apply (rule trans)
kleing@24333
   411
   prefer 2
kleing@24333
   412
   apply (rule trunc_bl2bin [symmetric])
kleing@24333
   413
  apply (cases "k <= length bl")
kleing@24333
   414
   apply auto
kleing@24333
   415
  done
kleing@24333
   416
huffman@45997
   417
lemma nth_rest_power_bin:
huffman@45997
   418
  "bin_nth ((bin_rest ^^ k) w) n = bin_nth w (n + k)"
huffman@45997
   419
  apply (induct k arbitrary: n, clarsimp)
kleing@24333
   420
  apply clarsimp
kleing@24333
   421
  apply (simp only: bin_nth.Suc [symmetric] add_Suc)
kleing@24333
   422
  done
kleing@24333
   423
kleing@24333
   424
lemma take_rest_power_bin:
haftmann@30971
   425
  "m <= n ==> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest ^^ (n - m)) w)" 
kleing@24333
   426
  apply (rule nth_equalityI)
kleing@24333
   427
   apply simp
kleing@24333
   428
  apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin)
kleing@24333
   429
  done
kleing@24333
   430
huffman@24465
   431
lemma hd_butlast: "size xs > 1 ==> hd (butlast xs) = hd xs"
huffman@24465
   432
  by (cases xs) auto
kleing@24333
   433
haftmann@26557
   434
lemma last_bin_last': 
haftmann@54847
   435
  "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin_aux xs w)" 
haftmann@26557
   436
  by (induct xs arbitrary: w) auto
kleing@24333
   437
kleing@24333
   438
lemma last_bin_last: 
haftmann@54847
   439
  "size xs > 0 ==> last xs \<longleftrightarrow> bin_last (bl_to_bin xs)" 
kleing@24333
   440
  unfolding bl_to_bin_def by (erule last_bin_last')
kleing@24333
   441
  
kleing@24333
   442
lemma bin_last_last: 
haftmann@54847
   443
  "bin_last w \<longleftrightarrow> last (bin_to_bl (Suc n) w)" 
kleing@24333
   444
  apply (unfold bin_to_bl_def)
kleing@24333
   445
  apply simp
kleing@24333
   446
  apply (auto simp add: bin_to_bl_aux_alt)
kleing@24333
   447
  done
kleing@24333
   448
huffman@24465
   449
(** links between bit-wise operations and operations on bool lists **)
huffman@24465
   450
    
huffman@45997
   451
lemma bl_xor_aux_bin:
huffman@45997
   452
  "map2 (%x y. x ~= y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
haftmann@26557
   453
    bin_to_bl_aux n (v XOR w) (map2 (%x y. x ~= y) bs cs)"
huffman@45997
   454
  apply (induct n arbitrary: v w bs cs)
huffman@45997
   455
   apply simp
huffman@45997
   456
  apply (case_tac v rule: bin_exhaust)
huffman@45997
   457
  apply (case_tac w rule: bin_exhaust)
huffman@45997
   458
  apply clarsimp
huffman@45997
   459
  apply (case_tac b)
haftmann@54847
   460
  apply auto
huffman@45997
   461
  done
huffman@45997
   462
huffman@45997
   463
lemma bl_or_aux_bin:
huffman@45997
   464
  "map2 (op | ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
huffman@45997
   465
    bin_to_bl_aux n (v OR w) (map2 (op | ) bs cs)"
huffman@45997
   466
  apply (induct n arbitrary: v w bs cs)
kleing@24333
   467
   apply simp
kleing@24333
   468
  apply (case_tac v rule: bin_exhaust)
kleing@24333
   469
  apply (case_tac w rule: bin_exhaust)
kleing@24333
   470
  apply clarsimp
kleing@24333
   471
  done
kleing@24333
   472
    
huffman@45997
   473
lemma bl_and_aux_bin:
huffman@45997
   474
  "map2 (op & ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
haftmann@26557
   475
    bin_to_bl_aux n (v AND w) (map2 (op & ) bs cs)" 
huffman@45997
   476
  apply (induct n arbitrary: v w bs cs)
kleing@24333
   477
   apply simp
kleing@24333
   478
  apply (case_tac v rule: bin_exhaust)
kleing@24333
   479
  apply (case_tac w rule: bin_exhaust)
kleing@24333
   480
  apply clarsimp
kleing@24333
   481
  done
kleing@24333
   482
    
huffman@45997
   483
lemma bl_not_aux_bin:
huffman@45997
   484
  "map Not (bin_to_bl_aux n w cs) = 
huffman@24353
   485
    bin_to_bl_aux n (NOT w) (map Not cs)"
huffman@45997
   486
  apply (induct n arbitrary: w cs)
kleing@24333
   487
   apply clarsimp
kleing@24333
   488
  apply clarsimp
kleing@24333
   489
  done
kleing@24333
   490
huffman@45854
   491
lemma bl_not_bin: "map Not (bin_to_bl n w) = bin_to_bl n (NOT w)"
huffman@45854
   492
  unfolding bin_to_bl_def by (simp add: bl_not_aux_bin)
kleing@24333
   493
huffman@45854
   494
lemma bl_and_bin:
huffman@45854
   495
  "map2 (op \<and>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)"
huffman@45854
   496
  unfolding bin_to_bl_def by (simp add: bl_and_aux_bin)
kleing@24333
   497
huffman@45854
   498
lemma bl_or_bin:
huffman@45854
   499
  "map2 (op \<or>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)"
huffman@45854
   500
  unfolding bin_to_bl_def by (simp add: bl_or_aux_bin)
kleing@24333
   501
huffman@45854
   502
lemma bl_xor_bin:
huffman@45854
   503
  "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)"
huffman@45854
   504
  unfolding bin_to_bl_def by (simp only: bl_xor_aux_bin map2_Nil)
kleing@24333
   505
huffman@45997
   506
lemma drop_bin2bl_aux:
huffman@45997
   507
  "drop m (bin_to_bl_aux n bin bs) = 
kleing@24333
   508
    bin_to_bl_aux (n - m) bin (drop (m - n) bs)"
huffman@45997
   509
  apply (induct n arbitrary: m bin bs, clarsimp)
kleing@24333
   510
  apply clarsimp
kleing@24333
   511
  apply (case_tac bin rule: bin_exhaust)
kleing@24333
   512
  apply (case_tac "m <= n", simp)
kleing@24333
   513
  apply (case_tac "m - n", simp)
kleing@24333
   514
  apply simp
kleing@24333
   515
  apply (rule_tac f = "%nat. drop nat bs" in arg_cong) 
kleing@24333
   516
  apply simp
kleing@24333
   517
  done
kleing@24333
   518
kleing@24333
   519
lemma drop_bin2bl: "drop m (bin_to_bl n bin) = bin_to_bl (n - m) bin"
kleing@24333
   520
  unfolding bin_to_bl_def by (simp add : drop_bin2bl_aux)
kleing@24333
   521
huffman@45997
   522
lemma take_bin2bl_lem1:
huffman@45997
   523
  "take m (bin_to_bl_aux m w bs) = bin_to_bl m w"
huffman@45997
   524
  apply (induct m arbitrary: w bs, clarsimp)
kleing@24333
   525
  apply clarsimp
kleing@24333
   526
  apply (simp add: bin_to_bl_aux_alt)
kleing@24333
   527
  apply (simp add: bin_to_bl_def)
kleing@24333
   528
  apply (simp add: bin_to_bl_aux_alt)
kleing@24333
   529
  done
kleing@24333
   530
huffman@45997
   531
lemma take_bin2bl_lem:
huffman@45997
   532
  "take m (bin_to_bl_aux (m + n) w bs) = 
kleing@24333
   533
    take m (bin_to_bl (m + n) w)"
huffman@45997
   534
  apply (induct n arbitrary: w bs)
kleing@24333
   535
   apply (simp_all (no_asm) add: bin_to_bl_def take_bin2bl_lem1)
kleing@24333
   536
  apply simp
kleing@24333
   537
  done
kleing@24333
   538
huffman@45997
   539
lemma bin_split_take:
huffman@45997
   540
  "bin_split n c = (a, b) \<Longrightarrow>
kleing@24333
   541
    bin_to_bl m a = take m (bin_to_bl (m + n) c)"
huffman@45997
   542
  apply (induct n arbitrary: b c)
kleing@24333
   543
   apply clarsimp
haftmann@53062
   544
  apply (clarsimp simp: Let_def split: prod.split_asm)
kleing@24333
   545
  apply (simp add: bin_to_bl_def)
kleing@24333
   546
  apply (simp add: take_bin2bl_lem)
kleing@24333
   547
  done
kleing@24333
   548
kleing@24333
   549
lemma bin_split_take1: 
kleing@24333
   550
  "k = m + n ==> bin_split n c = (a, b) ==> 
kleing@24333
   551
    bin_to_bl m a = take m (bin_to_bl k c)"
kleing@24333
   552
  by (auto elim: bin_split_take)
kleing@24333
   553
  
huffman@45997
   554
lemma nth_takefill: "m < n \<Longrightarrow>
kleing@24333
   555
    takefill fill n l ! m = (if m < length l then l ! m else fill)"
huffman@45997
   556
  apply (induct n arbitrary: m l, clarsimp)
kleing@24333
   557
  apply clarsimp
kleing@24333
   558
  apply (case_tac m)
kleing@24333
   559
   apply (simp split: list.split)
kleing@24333
   560
  apply (simp split: list.split)
kleing@24333
   561
  done
kleing@24333
   562
huffman@45997
   563
lemma takefill_alt:
huffman@45997
   564
  "takefill fill n l = take n l @ replicate (n - length l) fill"
huffman@45997
   565
  by (induct n arbitrary: l) (auto split: list.split)
kleing@24333
   566
kleing@24333
   567
lemma takefill_replicate [simp]:
kleing@24333
   568
  "takefill fill n (replicate m fill) = replicate n fill"
kleing@24333
   569
  by (simp add : takefill_alt replicate_add [symmetric])
kleing@24333
   570
huffman@45997
   571
lemma takefill_le':
huffman@45997
   572
  "n = m + k \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
huffman@45997
   573
  by (induct m arbitrary: l n) (auto split: list.split)
kleing@24333
   574
kleing@24333
   575
lemma length_takefill [simp]: "length (takefill fill n l) = n"
kleing@24333
   576
  by (simp add : takefill_alt)
kleing@24333
   577
kleing@24333
   578
lemma take_takefill':
kleing@24333
   579
  "!!w n.  n = k + m ==> take k (takefill fill n w) = takefill fill k w"
nipkow@63648
   580
  by (induct k) (auto split: list.split) 
kleing@24333
   581
kleing@24333
   582
lemma drop_takefill:
kleing@24333
   583
  "!!w. drop k (takefill fill (m + k) w) = takefill fill m (drop k w)"
nipkow@63648
   584
  by (induct k) (auto split: list.split) 
kleing@24333
   585
kleing@24333
   586
lemma takefill_le [simp]:
kleing@24333
   587
  "m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
kleing@24333
   588
  by (auto simp: le_iff_add takefill_le')
kleing@24333
   589
kleing@24333
   590
lemma take_takefill [simp]:
kleing@24333
   591
  "m \<le> n \<Longrightarrow> take m (takefill fill n w) = takefill fill m w"
kleing@24333
   592
  by (auto simp: le_iff_add take_takefill')
kleing@24333
   593
 
kleing@24333
   594
lemma takefill_append:
kleing@24333
   595
  "takefill fill (m + length xs) (xs @ w) = xs @ (takefill fill m w)"
kleing@24333
   596
  by (induct xs) auto
kleing@24333
   597
kleing@24333
   598
lemma takefill_same': 
kleing@24333
   599
  "l = length xs ==> takefill fill l xs = xs"
thomas@57492
   600
  by (induct xs arbitrary: l, auto)
kleing@24333
   601
 
kleing@24333
   602
lemmas takefill_same [simp] = takefill_same' [OF refl]
kleing@24333
   603
kleing@24333
   604
lemma takefill_bintrunc:
kleing@24333
   605
  "takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))"
kleing@24333
   606
  apply (rule nth_equalityI)
kleing@24333
   607
   apply simp
kleing@24333
   608
  apply (clarsimp simp: nth_takefill nth_rev nth_bin_to_bl bin_nth_of_bl)
kleing@24333
   609
  done
kleing@24333
   610
kleing@24333
   611
lemma bl_bin_bl_rtf:
kleing@24333
   612
  "bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))"
kleing@24333
   613
  by (simp add : takefill_bintrunc)
huffman@45854
   614
huffman@45854
   615
lemma bl_bin_bl_rep_drop:
huffman@45854
   616
  "bin_to_bl n (bl_to_bin bl) =
huffman@45854
   617
    replicate (n - length bl) False @ drop (length bl - n) bl"
huffman@45854
   618
  by (simp add: bl_bin_bl_rtf takefill_alt rev_take)
kleing@24333
   619
kleing@24333
   620
lemma tf_rev:
kleing@24333
   621
  "n + k = m + length bl ==> takefill x m (rev (takefill y n bl)) = 
kleing@24333
   622
    rev (takefill y m (rev (takefill x k (rev bl))))"
kleing@24333
   623
  apply (rule nth_equalityI)
kleing@24333
   624
   apply (auto simp add: nth_takefill nth_rev)
kleing@24333
   625
  apply (rule_tac f = "%n. bl ! n" in arg_cong) 
kleing@24333
   626
  apply arith 
kleing@24333
   627
  done
kleing@24333
   628
kleing@24333
   629
lemma takefill_minus:
kleing@24333
   630
  "0 < n ==> takefill fill (Suc (n - 1)) w = takefill fill n w"
kleing@24333
   631
  by auto
kleing@24333
   632
kleing@24333
   633
lemmas takefill_Suc_cases = 
wenzelm@45604
   634
  list.cases [THEN takefill.Suc [THEN trans]]
kleing@24333
   635
kleing@24333
   636
lemmas takefill_Suc_Nil = takefill_Suc_cases (1)
kleing@24333
   637
lemmas takefill_Suc_Cons = takefill_Suc_cases (2)
kleing@24333
   638
kleing@24333
   639
lemmas takefill_minus_simps = takefill_Suc_cases [THEN [2] 
wenzelm@45604
   640
  takefill_minus [symmetric, THEN trans]]
kleing@24333
   641
huffman@47108
   642
lemma takefill_numeral_Nil [simp]:
huffman@47219
   643
  "takefill fill (numeral k) [] = fill # takefill fill (pred_numeral k) []"
huffman@47219
   644
  by (simp add: numeral_eq_Suc)
huffman@47108
   645
huffman@47108
   646
lemma takefill_numeral_Cons [simp]:
huffman@47219
   647
  "takefill fill (numeral k) (x # xs) = x # takefill fill (pred_numeral k) xs"
huffman@47219
   648
  by (simp add: numeral_eq_Suc)
kleing@24333
   649
kleing@24333
   650
(* links with function bl_to_bin *)
kleing@24333
   651
kleing@24333
   652
lemma bl_to_bin_aux_cat: 
haftmann@26557
   653
  "!!nv v. bl_to_bin_aux bs (bin_cat w nv v) = 
haftmann@26557
   654
    bin_cat w (nv + length bs) (bl_to_bin_aux bs v)"
kleing@24333
   655
  apply (induct bs)
kleing@24333
   656
   apply simp
kleing@24333
   657
  apply (simp add: bin_cat_Suc_Bit [symmetric] del: bin_cat.simps)
kleing@24333
   658
  done
kleing@24333
   659
kleing@24333
   660
lemma bin_to_bl_aux_cat: 
kleing@24333
   661
  "!!w bs. bin_to_bl_aux (nv + nw) (bin_cat v nw w) bs = 
kleing@24333
   662
    bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)"
kleing@24333
   663
  by (induct nw) auto 
kleing@24333
   664
huffman@45854
   665
lemma bl_to_bin_aux_alt:
huffman@45854
   666
  "bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)"
huffman@46001
   667
  using bl_to_bin_aux_cat [where nv = "0" and v = "0"]
huffman@45854
   668
  unfolding bl_to_bin_def [symmetric] by simp
kleing@24333
   669
huffman@45854
   670
lemma bin_to_bl_cat:
huffman@45854
   671
  "bin_to_bl (nv + nw) (bin_cat v nw w) =
huffman@45854
   672
    bin_to_bl_aux nv v (bin_to_bl nw w)"
huffman@45854
   673
  unfolding bin_to_bl_def by (simp add: bin_to_bl_aux_cat)
kleing@24333
   674
kleing@24333
   675
lemmas bl_to_bin_aux_app_cat = 
kleing@24333
   676
  trans [OF bl_to_bin_aux_append bl_to_bin_aux_alt]
kleing@24333
   677
kleing@24333
   678
lemmas bin_to_bl_aux_cat_app =
kleing@24333
   679
  trans [OF bin_to_bl_aux_cat bin_to_bl_aux_alt]
kleing@24333
   680
huffman@45854
   681
lemma bl_to_bin_app_cat:
huffman@45854
   682
  "bl_to_bin (bsa @ bs) = bin_cat (bl_to_bin bsa) (length bs) (bl_to_bin bs)"
huffman@45854
   683
  by (simp only: bl_to_bin_aux_app_cat bl_to_bin_def)
kleing@24333
   684
huffman@45854
   685
lemma bin_to_bl_cat_app:
huffman@45854
   686
  "bin_to_bl (n + nw) (bin_cat w nw wa) = bin_to_bl n w @ bin_to_bl nw wa"
huffman@45854
   687
  by (simp only: bin_to_bl_def bin_to_bl_aux_cat_app)
kleing@24333
   688
kleing@24333
   689
(* bl_to_bin_app_cat_alt and bl_to_bin_app_cat are easily interderivable *)
kleing@24333
   690
lemma bl_to_bin_app_cat_alt: 
kleing@24333
   691
  "bin_cat (bl_to_bin cs) n w = bl_to_bin (cs @ bin_to_bl n w)"
kleing@24333
   692
  by (simp add : bl_to_bin_app_cat)
kleing@24333
   693
kleing@24333
   694
lemma mask_lem: "(bl_to_bin (True # replicate n False)) = 
huffman@46645
   695
    (bl_to_bin (replicate n True)) + 1"
kleing@24333
   696
  apply (unfold bl_to_bin_def)
kleing@24333
   697
  apply (induct n)
huffman@46645
   698
   apply simp
nipkow@31790
   699
  apply (simp only: Suc_eq_plus1 replicate_add
kleing@24333
   700
                    append_Cons [symmetric] bl_to_bin_aux_append)
huffman@46645
   701
  apply (simp add: Bit_B0_2t Bit_B1_2t)
kleing@24333
   702
  done
kleing@24333
   703
huffman@24465
   704
(* function bl_of_nth *)
kleing@24333
   705
lemma length_bl_of_nth [simp]: "length (bl_of_nth n f) = n"
kleing@24333
   706
  by (induct n)  auto
kleing@24333
   707
kleing@24333
   708
lemma nth_bl_of_nth [simp]:
kleing@24333
   709
  "m < n \<Longrightarrow> rev (bl_of_nth n f) ! m = f m"
kleing@24333
   710
  apply (induct n)
kleing@24333
   711
   apply simp
kleing@24333
   712
  apply (clarsimp simp add : nth_append)
kleing@24333
   713
  apply (rule_tac f = "f" in arg_cong) 
kleing@24333
   714
  apply simp
kleing@24333
   715
  done
kleing@24333
   716
kleing@24333
   717
lemma bl_of_nth_inj: 
kleing@24333
   718
  "(!!k. k < n ==> f k = g k) ==> bl_of_nth n f = bl_of_nth n g"
kleing@24333
   719
  by (induct n)  auto
kleing@24333
   720
huffman@45997
   721
lemma bl_of_nth_nth_le:
huffman@45997
   722
  "n \<le> length xs \<Longrightarrow> bl_of_nth n (nth (rev xs)) = drop (length xs - n) xs"
huffman@45997
   723
  apply (induct n arbitrary: xs, clarsimp)
kleing@24333
   724
  apply clarsimp
kleing@24333
   725
  apply (rule trans [OF _ hd_Cons_tl])
kleing@24333
   726
   apply (frule Suc_le_lessD)
kleing@24333
   727
   apply (simp add: nth_rev trans [OF drop_Suc drop_tl, symmetric])
kleing@24333
   728
   apply (subst hd_drop_conv_nth)
kleing@24333
   729
     apply force
kleing@24333
   730
    apply simp_all
kleing@24333
   731
  apply (rule_tac f = "%n. drop n xs" in arg_cong) 
kleing@24333
   732
  apply simp
kleing@24333
   733
  done
kleing@24333
   734
huffman@45854
   735
lemma bl_of_nth_nth [simp]: "bl_of_nth (length xs) (op ! (rev xs)) = xs"
huffman@45854
   736
  by (simp add: bl_of_nth_nth_le)
kleing@24333
   737
kleing@24333
   738
lemma size_rbl_pred: "length (rbl_pred bl) = length bl"
kleing@24333
   739
  by (induct bl) auto
kleing@24333
   740
kleing@24333
   741
lemma size_rbl_succ: "length (rbl_succ bl) = length bl"
kleing@24333
   742
  by (induct bl) auto
kleing@24333
   743
kleing@24333
   744
lemma size_rbl_add:
kleing@24333
   745
  "!!cl. length (rbl_add bl cl) = length bl"
kleing@24333
   746
  by (induct bl) (auto simp: Let_def size_rbl_succ)
kleing@24333
   747
kleing@24333
   748
lemma size_rbl_mult: 
kleing@24333
   749
  "!!cl. length (rbl_mult bl cl) = length bl"
kleing@24333
   750
  by (induct bl) (auto simp add : Let_def size_rbl_add)
kleing@24333
   751
kleing@24333
   752
lemmas rbl_sizes [simp] = 
kleing@24333
   753
  size_rbl_pred size_rbl_succ size_rbl_add size_rbl_mult
kleing@24333
   754
kleing@24333
   755
lemmas rbl_Nils =
kleing@24333
   756
  rbl_pred.Nil rbl_succ.Nil rbl_add.Nil rbl_mult.Nil
kleing@24333
   757
huffman@46653
   758
lemma rbl_pred:
huffman@46653
   759
  "rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin - 1))"
huffman@46653
   760
  apply (induct n arbitrary: bin, simp)
kleing@24333
   761
  apply (unfold bin_to_bl_def)
kleing@24333
   762
  apply clarsimp
kleing@24333
   763
  apply (case_tac bin rule: bin_exhaust)
kleing@24333
   764
  apply (case_tac b)
huffman@46653
   765
   apply (clarsimp simp: bin_to_bl_aux_alt)+
kleing@24333
   766
  done
kleing@24333
   767
kleing@24333
   768
lemma rbl_succ: 
huffman@46653
   769
  "rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))"
huffman@46653
   770
  apply (induct n arbitrary: bin, simp)
kleing@24333
   771
  apply (unfold bin_to_bl_def)
kleing@24333
   772
  apply clarsimp
kleing@24333
   773
  apply (case_tac bin rule: bin_exhaust)
kleing@24333
   774
  apply (case_tac b)
huffman@46653
   775
   apply (clarsimp simp: bin_to_bl_aux_alt)+
kleing@24333
   776
  done
kleing@24333
   777
kleing@24333
   778
lemma rbl_add: 
kleing@24333
   779
  "!!bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = 
kleing@24333
   780
    rev (bin_to_bl n (bina + binb))"
kleing@24333
   781
  apply (induct n, simp)
kleing@24333
   782
  apply (unfold bin_to_bl_def)
kleing@24333
   783
  apply clarsimp
kleing@24333
   784
  apply (case_tac bina rule: bin_exhaust)
kleing@24333
   785
  apply (case_tac binb rule: bin_exhaust)
kleing@24333
   786
  apply (case_tac b)
kleing@24333
   787
   apply (case_tac [!] "ba")
haftmann@57514
   788
     apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def ac_simps)
kleing@24333
   789
  done
kleing@24333
   790
kleing@24333
   791
lemma rbl_add_app2: 
kleing@24333
   792
  "!!blb. length blb >= length bla ==> 
kleing@24333
   793
    rbl_add bla (blb @ blc) = rbl_add bla blb"
kleing@24333
   794
  apply (induct bla, simp)
kleing@24333
   795
  apply clarsimp
kleing@24333
   796
  apply (case_tac blb, clarsimp)
kleing@24333
   797
  apply (clarsimp simp: Let_def)
kleing@24333
   798
  done
kleing@24333
   799
kleing@24333
   800
lemma rbl_add_take2: 
kleing@24333
   801
  "!!blb. length blb >= length bla ==> 
kleing@24333
   802
    rbl_add bla (take (length bla) blb) = rbl_add bla blb"
kleing@24333
   803
  apply (induct bla, simp)
kleing@24333
   804
  apply clarsimp
kleing@24333
   805
  apply (case_tac blb, clarsimp)
kleing@24333
   806
  apply (clarsimp simp: Let_def)
kleing@24333
   807
  done
kleing@24333
   808
kleing@24333
   809
lemma rbl_add_long: 
kleing@24333
   810
  "m >= n ==> rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) = 
kleing@24333
   811
    rev (bin_to_bl n (bina + binb))"
kleing@24333
   812
  apply (rule box_equals [OF _ rbl_add_take2 rbl_add])
kleing@24333
   813
   apply (rule_tac f = "rbl_add (rev (bin_to_bl n bina))" in arg_cong) 
kleing@24333
   814
   apply (rule rev_swap [THEN iffD1])
kleing@24333
   815
   apply (simp add: rev_take drop_bin2bl)
kleing@24333
   816
  apply simp
kleing@24333
   817
  done
kleing@24333
   818
kleing@24333
   819
lemma rbl_mult_app2:
kleing@24333
   820
  "!!blb. length blb >= length bla ==> 
kleing@24333
   821
    rbl_mult bla (blb @ blc) = rbl_mult bla blb"
kleing@24333
   822
  apply (induct bla, simp)
kleing@24333
   823
  apply clarsimp
kleing@24333
   824
  apply (case_tac blb, clarsimp)
kleing@24333
   825
  apply (clarsimp simp: Let_def rbl_add_app2)
kleing@24333
   826
  done
kleing@24333
   827
kleing@24333
   828
lemma rbl_mult_take2: 
kleing@24333
   829
  "length blb >= length bla ==> 
kleing@24333
   830
    rbl_mult bla (take (length bla) blb) = rbl_mult bla blb"
kleing@24333
   831
  apply (rule trans)
kleing@24333
   832
   apply (rule rbl_mult_app2 [symmetric])
kleing@24333
   833
   apply simp
kleing@24333
   834
  apply (rule_tac f = "rbl_mult bla" in arg_cong) 
kleing@24333
   835
  apply (rule append_take_drop_id)
kleing@24333
   836
  done
kleing@24333
   837
    
kleing@24333
   838
lemma rbl_mult_gt1: 
kleing@24333
   839
  "m >= length bl ==> rbl_mult bl (rev (bin_to_bl m binb)) = 
kleing@24333
   840
    rbl_mult bl (rev (bin_to_bl (length bl) binb))"
kleing@24333
   841
  apply (rule trans)
kleing@24333
   842
   apply (rule rbl_mult_take2 [symmetric])
kleing@24333
   843
   apply simp_all
kleing@24333
   844
  apply (rule_tac f = "rbl_mult bl" in arg_cong) 
kleing@24333
   845
  apply (rule rev_swap [THEN iffD1])
kleing@24333
   846
  apply (simp add: rev_take drop_bin2bl)
kleing@24333
   847
  done
kleing@24333
   848
    
kleing@24333
   849
lemma rbl_mult_gt: 
kleing@24333
   850
  "m > n ==> rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) = 
kleing@24333
   851
    rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb))"
kleing@24333
   852
  by (auto intro: trans [OF rbl_mult_gt1])
kleing@24333
   853
  
kleing@24333
   854
lemmas rbl_mult_Suc = lessI [THEN rbl_mult_gt]
kleing@24333
   855
kleing@24333
   856
lemma rbbl_Cons: 
haftmann@54847
   857
  "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (x BIT b))"
kleing@24333
   858
  apply (unfold bin_to_bl_def)
kleing@24333
   859
  apply simp
kleing@24333
   860
  apply (simp add: bin_to_bl_aux_alt)
kleing@24333
   861
  done
huffman@46653
   862
kleing@24333
   863
lemma rbl_mult: "!!bina binb. 
kleing@24333
   864
    rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = 
kleing@24333
   865
    rev (bin_to_bl n (bina * binb))"
kleing@24333
   866
  apply (induct n)
kleing@24333
   867
   apply simp
kleing@24333
   868
  apply (unfold bin_to_bl_def)
kleing@24333
   869
  apply clarsimp
kleing@24333
   870
  apply (case_tac bina rule: bin_exhaust)
kleing@24333
   871
  apply (case_tac binb rule: bin_exhaust)
kleing@24333
   872
  apply (case_tac b)
kleing@24333
   873
   apply (case_tac [!] "ba")
huffman@46653
   874
     apply (auto simp: bin_to_bl_aux_alt Let_def)
huffman@46653
   875
     apply (auto simp: rbbl_Cons rbl_mult_Suc rbl_add)
kleing@24333
   876
  done
kleing@24333
   877
kleing@24333
   878
lemma rbl_add_split: 
kleing@24333
   879
  "P (rbl_add (y # ys) (x # xs)) = 
kleing@24333
   880
    (ALL ws. length ws = length ys --> ws = rbl_add ys xs --> 
wenzelm@26008
   881
    (y --> ((x --> P (False # rbl_succ ws)) & (~ x -->  P (True # ws)))) &
kleing@24333
   882
    (~ y --> P (x # ws)))"
kleing@24333
   883
  apply (auto simp add: Let_def)
kleing@24333
   884
   apply (case_tac [!] "y")
kleing@24333
   885
     apply auto
kleing@24333
   886
  done
kleing@24333
   887
kleing@24333
   888
lemma rbl_mult_split: 
kleing@24333
   889
  "P (rbl_mult (y # ys) xs) = 
kleing@24333
   890
    (ALL ws. length ws = Suc (length ys) --> ws = False # rbl_mult ys xs --> 
kleing@24333
   891
    (y --> P (rbl_add ws xs)) & (~ y -->  P ws))"
kleing@24333
   892
  by (clarsimp simp add : Let_def)
kleing@24333
   893
  
kleing@24333
   894
huffman@24350
   895
subsection "Repeated splitting or concatenation"
kleing@24333
   896
kleing@24333
   897
lemma sclem:
kleing@24333
   898
  "size (concat (map (bin_to_bl n) xs)) = length xs * n"
kleing@24333
   899
  by (induct xs) auto
kleing@24333
   900
huffman@45997
   901
lemma bin_cat_foldl_lem:
huffman@45997
   902
  "foldl (%u. bin_cat u n) x xs = 
kleing@24333
   903
    bin_cat x (size xs * n) (foldl (%u. bin_cat u n) y xs)"
huffman@45997
   904
  apply (induct xs arbitrary: x)
kleing@24333
   905
   apply simp
kleing@24333
   906
  apply (simp (no_asm))
kleing@24333
   907
  apply (frule asm_rl)
huffman@45997
   908
  apply (drule meta_spec)
kleing@24333
   909
  apply (erule trans)
huffman@45997
   910
  apply (drule_tac x = "bin_cat y n a" in meta_spec)
haftmann@54863
   911
  apply (simp add : bin_cat_assoc_sym min.absorb2)
kleing@24333
   912
  done
kleing@24333
   913
kleing@24333
   914
lemma bin_rcat_bl:
kleing@24333
   915
  "(bin_rcat n wl) = bl_to_bin (concat (map (bin_to_bl n) wl))"
kleing@24333
   916
  apply (unfold bin_rcat_def)
kleing@24333
   917
  apply (rule sym)
kleing@24333
   918
  apply (induct wl)
kleing@24333
   919
   apply (auto simp add : bl_to_bin_append)
kleing@24333
   920
  apply (simp add : bl_to_bin_aux_alt sclem)
kleing@24333
   921
  apply (simp add : bin_cat_foldl_lem [symmetric])
kleing@24333
   922
  done
kleing@24333
   923
kleing@24333
   924
lemmas bin_rsplit_aux_simps = bin_rsplit_aux.simps bin_rsplitl_aux.simps
kleing@24333
   925
lemmas rsplit_aux_simps = bin_rsplit_aux_simps
kleing@24333
   926
nipkow@62390
   927
lemmas th_if_simp1 = if_split [where P = "op = l", THEN iffD1, THEN conjunct1, THEN mp] for l
nipkow@62390
   928
lemmas th_if_simp2 = if_split [where P = "op = l", THEN iffD1, THEN conjunct2, THEN mp] for l
kleing@24333
   929
kleing@24333
   930
lemmas rsplit_aux_simp1s = rsplit_aux_simps [THEN th_if_simp1]
kleing@24333
   931
kleing@24333
   932
lemmas rsplit_aux_simp2ls = rsplit_aux_simps [THEN th_if_simp2]
kleing@24333
   933
(* these safe to [simp add] as require calculating m - n *)
kleing@24333
   934
lemmas bin_rsplit_aux_simp2s [simp] = rsplit_aux_simp2ls [unfolded Let_def]
kleing@24333
   935
lemmas rbscl = bin_rsplit_aux_simp2s (2)
kleing@24333
   936
kleing@24333
   937
lemmas rsplit_aux_0_simps [simp] = 
kleing@24333
   938
  rsplit_aux_simp1s [OF disjI1] rsplit_aux_simp1s [OF disjI2]
kleing@24333
   939
kleing@24333
   940
lemma bin_rsplit_aux_append:
haftmann@26557
   941
  "bin_rsplit_aux n m c (bs @ cs) = bin_rsplit_aux n m c bs @ cs"
haftmann@26557
   942
  apply (induct n m c bs rule: bin_rsplit_aux.induct)
kleing@24333
   943
  apply (subst bin_rsplit_aux.simps)
kleing@24333
   944
  apply (subst bin_rsplit_aux.simps)
haftmann@53062
   945
  apply (clarsimp split: prod.split)
kleing@24333
   946
  done
kleing@24333
   947
kleing@24333
   948
lemma bin_rsplitl_aux_append:
haftmann@26557
   949
  "bin_rsplitl_aux n m c (bs @ cs) = bin_rsplitl_aux n m c bs @ cs"
haftmann@26557
   950
  apply (induct n m c bs rule: bin_rsplitl_aux.induct)
kleing@24333
   951
  apply (subst bin_rsplitl_aux.simps)
kleing@24333
   952
  apply (subst bin_rsplitl_aux.simps)
haftmann@53062
   953
  apply (clarsimp split: prod.split)
kleing@24333
   954
  done
kleing@24333
   955
kleing@24333
   956
lemmas rsplit_aux_apps [where bs = "[]"] =
kleing@24333
   957
  bin_rsplit_aux_append bin_rsplitl_aux_append
kleing@24333
   958
kleing@24333
   959
lemmas rsplit_def_auxs = bin_rsplit_def bin_rsplitl_def
kleing@24333
   960
kleing@24333
   961
lemmas rsplit_aux_alts = rsplit_aux_apps 
kleing@24333
   962
  [unfolded append_Nil rsplit_def_auxs [symmetric]]
kleing@24333
   963
kleing@24333
   964
lemma bin_split_minus: "0 < n ==> bin_split (Suc (n - 1)) w = bin_split n w"
kleing@24333
   965
  by auto
kleing@24333
   966
kleing@24333
   967
lemmas bin_split_minus_simp =
wenzelm@45604
   968
  bin_split.Suc [THEN [2] bin_split_minus [symmetric, THEN trans]]
kleing@24333
   969
kleing@24333
   970
lemma bin_split_pred_simp [simp]: 
huffman@47108
   971
  "(0::nat) < numeral bin \<Longrightarrow>
huffman@47108
   972
  bin_split (numeral bin) w =
huffman@47108
   973
  (let (w1, w2) = bin_split (numeral bin - 1) (bin_rest w)
kleing@24333
   974
   in (w1, w2 BIT bin_last w))" 
huffman@47108
   975
  by (simp only: bin_split_minus_simp)
kleing@24333
   976
kleing@24333
   977
lemma bin_rsplit_aux_simp_alt:
haftmann@26557
   978
  "bin_rsplit_aux n m c bs =
kleing@24333
   979
   (if m = 0 \<or> n = 0 
kleing@24333
   980
   then bs
kleing@24333
   981
   else let (a, b) = bin_split n c in bin_rsplit n (m - n, a) @ b # bs)"
haftmann@26557
   982
  unfolding bin_rsplit_aux.simps [of n m c bs]
haftmann@26557
   983
  apply simp
haftmann@26557
   984
  apply (subst rsplit_aux_alts)
haftmann@26557
   985
  apply (simp add: bin_rsplit_def)
kleing@24333
   986
  done
kleing@24333
   987
kleing@24333
   988
lemmas bin_rsplit_simp_alt = 
wenzelm@45604
   989
  trans [OF bin_rsplit_def bin_rsplit_aux_simp_alt]
kleing@24333
   990
kleing@24333
   991
lemmas bthrs = bin_rsplit_simp_alt [THEN [2] trans]
kleing@24333
   992
kleing@24333
   993
lemma bin_rsplit_size_sign' [rule_format] : 
huffman@45997
   994
  "\<lbrakk>n > 0; rev sw = bin_rsplit n (nw, w)\<rbrakk> \<Longrightarrow> 
huffman@45997
   995
    (ALL v: set sw. bintrunc n v = v)"
wenzelm@62957
   996
  apply (induct sw arbitrary: nw w)
kleing@24333
   997
   apply clarsimp
kleing@24333
   998
  apply clarsimp
kleing@24333
   999
  apply (drule bthrs)
nipkow@62390
  1000
  apply (simp (no_asm_use) add: Let_def split: prod.split_asm if_split_asm)
kleing@24333
  1001
  apply clarify
kleing@24333
  1002
  apply (drule split_bintrunc)
kleing@24333
  1003
  apply simp
kleing@24333
  1004
  done
kleing@24333
  1005
kleing@24333
  1006
lemmas bin_rsplit_size_sign = bin_rsplit_size_sign' [OF asm_rl 
wenzelm@45604
  1007
  rev_rev_ident [THEN trans] set_rev [THEN equalityD2 [THEN subsetD]]]
kleing@24333
  1008
kleing@24333
  1009
lemma bin_nth_rsplit [rule_format] :
kleing@24333
  1010
  "n > 0 ==> m < n ==> (ALL w k nw. rev sw = bin_rsplit n (nw, w) --> 
kleing@24333
  1011
       k < size sw --> bin_nth (sw ! k) m = bin_nth w (k * n + m))"
kleing@24333
  1012
  apply (induct sw)
kleing@24333
  1013
   apply clarsimp
kleing@24333
  1014
  apply clarsimp
kleing@24333
  1015
  apply (drule bthrs)
nipkow@62390
  1016
  apply (simp (no_asm_use) add: Let_def split: prod.split_asm if_split_asm)
kleing@24333
  1017
  apply clarify
kleing@24333
  1018
  apply (erule allE, erule impE, erule exI)
kleing@24333
  1019
  apply (case_tac k)
kleing@24333
  1020
   apply clarsimp   
kleing@24333
  1021
   prefer 2
kleing@24333
  1022
   apply clarsimp
kleing@24333
  1023
   apply (erule allE)
kleing@24333
  1024
   apply (erule (1) impE)
kleing@24333
  1025
   apply (drule bin_nth_split, erule conjE, erule allE,
haftmann@57514
  1026
          erule trans, simp add : ac_simps)+
kleing@24333
  1027
  done
kleing@24333
  1028
kleing@24333
  1029
lemma bin_rsplit_all:
kleing@24333
  1030
  "0 < nw ==> nw <= n ==> bin_rsplit n (nw, w) = [bintrunc n w]"
kleing@24333
  1031
  unfolding bin_rsplit_def
haftmann@53062
  1032
  by (clarsimp dest!: split_bintrunc simp: rsplit_aux_simp2ls split: prod.split)
kleing@24333
  1033
kleing@24333
  1034
lemma bin_rsplit_l [rule_format] :
kleing@24333
  1035
  "ALL bin. bin_rsplitl n (m, bin) = bin_rsplit n (m, bintrunc m bin)"
kleing@24333
  1036
  apply (rule_tac a = "m" in wf_less_than [THEN wf_induct])
kleing@24333
  1037
  apply (simp (no_asm) add : bin_rsplitl_def bin_rsplit_def)
kleing@24333
  1038
  apply (rule allI)
kleing@24333
  1039
  apply (subst bin_rsplitl_aux.simps)
kleing@24333
  1040
  apply (subst bin_rsplit_aux.simps)
haftmann@53062
  1041
  apply (clarsimp simp: Let_def split: prod.split)
kleing@24333
  1042
  apply (drule bin_split_trunc)
kleing@24333
  1043
  apply (drule sym [THEN trans], assumption)
haftmann@26557
  1044
  apply (subst rsplit_aux_alts(1))
haftmann@26557
  1045
  apply (subst rsplit_aux_alts(2))
haftmann@26557
  1046
  apply clarsimp
haftmann@26557
  1047
  unfolding bin_rsplit_def bin_rsplitl_def
haftmann@26557
  1048
  apply simp
kleing@24333
  1049
  done
haftmann@26557
  1050
kleing@24333
  1051
lemma bin_rsplit_rcat [rule_format] :
kleing@24333
  1052
  "n > 0 --> bin_rsplit n (n * size ws, bin_rcat n ws) = map (bintrunc n) ws"
kleing@24333
  1053
  apply (unfold bin_rsplit_def bin_rcat_def)
kleing@24333
  1054
  apply (rule_tac xs = "ws" in rev_induct)
kleing@24333
  1055
   apply clarsimp
kleing@24333
  1056
  apply clarsimp
haftmann@26557
  1057
  apply (subst rsplit_aux_alts)
haftmann@26557
  1058
  unfolding bin_split_cat
haftmann@26557
  1059
  apply simp
kleing@24333
  1060
  done
kleing@24333
  1061
kleing@24333
  1062
lemma bin_rsplit_aux_len_le [rule_format] :
haftmann@26557
  1063
  "\<forall>ws m. n \<noteq> 0 \<longrightarrow> ws = bin_rsplit_aux n nw w bs \<longrightarrow>
haftmann@26557
  1064
    length ws \<le> m \<longleftrightarrow> nw + length bs * n \<le> m * n"
haftmann@54871
  1065
proof -
haftmann@54871
  1066
  { fix i j j' k k' m :: nat and R
haftmann@54871
  1067
    assume d: "(i::nat) \<le> j \<or> m < j'"
haftmann@54871
  1068
    assume R1: "i * k \<le> j * k \<Longrightarrow> R"
haftmann@54871
  1069
    assume R2: "Suc m * k' \<le> j' * k' \<Longrightarrow> R"
haftmann@54871
  1070
    have "R" using d
haftmann@54871
  1071
      apply safe
haftmann@54871
  1072
       apply (rule R1, erule mult_le_mono1)
haftmann@54871
  1073
      apply (rule R2, erule Suc_le_eq [THEN iffD2 [THEN mult_le_mono1]])
haftmann@54871
  1074
      done
haftmann@54871
  1075
  } note A = this
haftmann@54871
  1076
  { fix sc m n lb :: nat
haftmann@54871
  1077
    have "(0::nat) < sc \<Longrightarrow> sc - n + (n + lb * n) \<le> m * n \<longleftrightarrow> sc + lb * n \<le> m * n"
haftmann@54871
  1078
      apply safe
haftmann@54871
  1079
       apply arith
haftmann@54871
  1080
      apply (case_tac "sc >= n")
haftmann@54871
  1081
       apply arith
haftmann@54871
  1082
      apply (insert linorder_le_less_linear [of m lb])
haftmann@54871
  1083
      apply (erule_tac k2=n and k'2=n in A)
haftmann@54871
  1084
       apply arith
haftmann@54871
  1085
      apply simp
haftmann@54871
  1086
      done
haftmann@54871
  1087
  } note B = this
haftmann@54871
  1088
  show ?thesis
haftmann@54871
  1089
    apply (induct n nw w bs rule: bin_rsplit_aux.induct)
haftmann@54871
  1090
    apply (subst bin_rsplit_aux.simps)
haftmann@54871
  1091
    apply (simp add: B Let_def split: prod.split)
haftmann@54871
  1092
    done
haftmann@54871
  1093
qed
kleing@24333
  1094
kleing@24333
  1095
lemma bin_rsplit_len_le: 
nipkow@25134
  1096
  "n \<noteq> 0 --> ws = bin_rsplit n (nw, w) --> (length ws <= m) = (nw <= m * n)"
kleing@24333
  1097
  unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len_le)
kleing@24333
  1098
 
huffman@45997
  1099
lemma bin_rsplit_aux_len:
huffman@45997
  1100
  "n \<noteq> 0 \<Longrightarrow> length (bin_rsplit_aux n nw w cs) =
kleing@24333
  1101
    (nw + n - 1) div n + length cs"
haftmann@26557
  1102
  apply (induct n nw w cs rule: bin_rsplit_aux.induct)
kleing@24333
  1103
  apply (subst bin_rsplit_aux.simps)
haftmann@53062
  1104
  apply (clarsimp simp: Let_def split: prod.split)
kleing@24333
  1105
  apply (erule thin_rl)
haftmann@27651
  1106
  apply (case_tac m)
haftmann@27651
  1107
  apply simp
kleing@24333
  1108
  apply (case_tac "m <= n")
eberlm@63501
  1109
   apply auto
kleing@24333
  1110
  done
kleing@24333
  1111
kleing@24333
  1112
lemma bin_rsplit_len: 
nipkow@25134
  1113
  "n\<noteq>0 ==> length (bin_rsplit n (nw, w)) = (nw + n - 1) div n"
kleing@24333
  1114
  unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len)
kleing@24333
  1115
haftmann@26557
  1116
lemma bin_rsplit_aux_len_indep:
haftmann@26557
  1117
  "n \<noteq> 0 \<Longrightarrow> length bs = length cs \<Longrightarrow>
haftmann@26557
  1118
    length (bin_rsplit_aux n nw v bs) =
haftmann@26557
  1119
    length (bin_rsplit_aux n nw w cs)"
haftmann@26557
  1120
proof (induct n nw w cs arbitrary: v bs rule: bin_rsplit_aux.induct)
haftmann@26557
  1121
  case (1 n m w cs v bs) show ?case
haftmann@26557
  1122
  proof (cases "m = 0")
wenzelm@61799
  1123
    case True then show ?thesis using \<open>length bs = length cs\<close> by simp
haftmann@26557
  1124
  next
haftmann@26557
  1125
    case False
wenzelm@61799
  1126
    from "1.hyps" \<open>m \<noteq> 0\<close> \<open>n \<noteq> 0\<close> have hyp: "\<And>v bs. length bs = Suc (length cs) \<Longrightarrow>
haftmann@26557
  1127
      length (bin_rsplit_aux n (m - n) v bs) =
haftmann@26557
  1128
      length (bin_rsplit_aux n (m - n) (fst (bin_split n w)) (snd (bin_split n w) # cs))"
haftmann@26557
  1129
    by auto
wenzelm@61799
  1130
    show ?thesis using \<open>length bs = length cs\<close> \<open>n \<noteq> 0\<close>
haftmann@26557
  1131
      by (auto simp add: bin_rsplit_aux_simp_alt Let_def bin_rsplit_len
haftmann@53062
  1132
        split: prod.split)
haftmann@26557
  1133
  qed
haftmann@26557
  1134
qed
kleing@24333
  1135
kleing@24333
  1136
lemma bin_rsplit_len_indep: 
nipkow@25134
  1137
  "n\<noteq>0 ==> length (bin_rsplit n (nw, v)) = length (bin_rsplit n (nw, w))"
kleing@24333
  1138
  apply (unfold bin_rsplit_def)
haftmann@26557
  1139
  apply (simp (no_asm))
kleing@24333
  1140
  apply (erule bin_rsplit_aux_len_indep)
kleing@24333
  1141
  apply (rule refl)
kleing@24333
  1142
  done
kleing@24333
  1143
haftmann@54874
  1144
wenzelm@61799
  1145
text \<open>Even more bit operations\<close>
haftmann@54874
  1146
haftmann@54874
  1147
instantiation int :: bitss
haftmann@54874
  1148
begin
haftmann@54874
  1149
haftmann@54874
  1150
definition [iff]:
haftmann@54874
  1151
  "i !! n \<longleftrightarrow> bin_nth i n"
haftmann@54874
  1152
haftmann@54874
  1153
definition
haftmann@54874
  1154
  "lsb i = (i :: int) !! 0"
haftmann@54874
  1155
haftmann@54874
  1156
definition
haftmann@54874
  1157
  "set_bit i n b = bin_sc n b i"
haftmann@54874
  1158
haftmann@54874
  1159
definition
haftmann@54874
  1160
  "set_bits f =
haftmann@54874
  1161
  (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then 
haftmann@54874
  1162
     let n = LEAST n. \<forall>n'\<ge>n. \<not> f n'
haftmann@54874
  1163
     in bl_to_bin (rev (map f [0..<n]))
haftmann@54874
  1164
   else if \<exists>n. \<forall>n'\<ge>n. f n' then
haftmann@54874
  1165
     let n = LEAST n. \<forall>n'\<ge>n. f n'
haftmann@54874
  1166
     in sbintrunc n (bl_to_bin (True # rev (map f [0..<n])))
haftmann@54874
  1167
   else 0 :: int)"
haftmann@54874
  1168
haftmann@54874
  1169
definition
haftmann@54874
  1170
  "shiftl x n = (x :: int) * 2 ^ n"
haftmann@54874
  1171
haftmann@54874
  1172
definition
haftmann@54874
  1173
  "shiftr x n = (x :: int) div 2 ^ n"
haftmann@54874
  1174
haftmann@54874
  1175
definition
haftmann@54874
  1176
  "msb x \<longleftrightarrow> (x :: int) < 0"
haftmann@54874
  1177
haftmann@54874
  1178
instance ..
haftmann@54874
  1179
kleing@24333
  1180
end
haftmann@54874
  1181
haftmann@54874
  1182
end