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