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