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