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