src/HOL/Word/BinBoolList.thy
 author nipkow Fri Mar 06 17:38:47 2009 +0100 (2009-03-06) changeset 30313 b2441b0c8d38 parent 29668 33ba3faeaa0e child 30952 7ab2716dd93b permissions -rw-r--r--
```     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_add_numeral_1 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
```