src/HOL/Word/BinOperations.thy
author wenzelm
Wed Sep 17 21:27:14 2008 +0200 (2008-09-17)
changeset 28263 69eaa97e7e96
parent 28042 1471f2974eb1
child 28562 4e74209f113e
permissions -rw-r--r--
moved global ML bindings to global place;
     1 (* 
     2   ID:     $Id$
     3   Author: Jeremy Dawson and Gerwin Klein, NICTA
     4 
     5   definition and basic theorems for bit-wise logical operations 
     6   for integers expressed using Pls, Min, BIT,
     7   and converting them to and from lists of bools
     8 *) 
     9 
    10 header {* Bitwise Operations on Binary Integers *}
    11 
    12 theory BinOperations
    13 imports BinGeneral BitSyntax
    14 begin
    15 
    16 subsection {* Logical operations *}
    17 
    18 text "bit-wise logical operations on the int type"
    19 
    20 instantiation int :: bit
    21 begin
    22 
    23 definition
    24   int_not_def [code func del]: "bitNOT = bin_rec Int.Min Int.Pls 
    25     (\<lambda>w b s. s BIT (NOT b))"
    26 
    27 definition
    28   int_and_def [code func del]: "bitAND = bin_rec (\<lambda>x. Int.Pls) (\<lambda>y. y) 
    29     (\<lambda>w b s y. s (bin_rest y) BIT (b AND bin_last y))"
    30 
    31 definition
    32   int_or_def [code func del]: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. Int.Min) 
    33     (\<lambda>w b s y. s (bin_rest y) BIT (b OR bin_last y))"
    34 
    35 definition
    36   int_xor_def [code func del]: "bitXOR = bin_rec (\<lambda>x. x) bitNOT 
    37     (\<lambda>w b s y. s (bin_rest y) BIT (b XOR bin_last y))"
    38 
    39 instance ..
    40 
    41 end
    42 
    43 lemma int_not_simps [simp]:
    44   "NOT Int.Pls = Int.Min"
    45   "NOT Int.Min = Int.Pls"
    46   "NOT (Int.Bit0 w) = Int.Bit1 (NOT w)"
    47   "NOT (Int.Bit1 w) = Int.Bit0 (NOT w)"
    48   "NOT (w BIT b) = (NOT w) BIT (NOT b)"
    49   unfolding int_not_def by (simp_all add: bin_rec_simps)
    50 
    51 declare int_not_simps(1-4) [code func]
    52 
    53 lemma int_xor_Pls [simp, code func]: 
    54   "Int.Pls XOR x = x"
    55   unfolding int_xor_def by (simp add: bin_rec_PM)
    56 
    57 lemma int_xor_Min [simp, code func]: 
    58   "Int.Min XOR x = NOT x"
    59   unfolding int_xor_def by (simp add: bin_rec_PM)
    60 
    61 lemma int_xor_Bits [simp]: 
    62   "(x BIT b) XOR (y BIT c) = (x XOR y) BIT (b XOR c)"
    63   apply (unfold int_xor_def)
    64   apply (rule bin_rec_simps (1) [THEN fun_cong, THEN trans])
    65     apply (rule ext, simp)
    66    prefer 2
    67    apply simp
    68   apply (rule ext)
    69   apply (simp add: int_not_simps [symmetric])
    70   done
    71 
    72 lemma int_xor_Bits2 [simp, code func]: 
    73   "(Int.Bit0 x) XOR (Int.Bit0 y) = Int.Bit0 (x XOR y)"
    74   "(Int.Bit0 x) XOR (Int.Bit1 y) = Int.Bit1 (x XOR y)"
    75   "(Int.Bit1 x) XOR (Int.Bit0 y) = Int.Bit1 (x XOR y)"
    76   "(Int.Bit1 x) XOR (Int.Bit1 y) = Int.Bit0 (x XOR y)"
    77   unfolding BIT_simps [symmetric] int_xor_Bits by simp_all
    78 
    79 lemma int_xor_x_simps':
    80   "w XOR (Int.Pls BIT bit.B0) = w"
    81   "w XOR (Int.Min BIT bit.B1) = NOT w"
    82   apply (induct w rule: bin_induct)
    83        apply simp_all[4]
    84    apply (unfold int_xor_Bits)
    85    apply clarsimp+
    86   done
    87 
    88 lemma int_xor_extra_simps [simp, code func]:
    89   "w XOR Int.Pls = w"
    90   "w XOR Int.Min = NOT w"
    91   using int_xor_x_simps' by simp_all
    92 
    93 lemma int_or_Pls [simp, code func]: 
    94   "Int.Pls OR x = x"
    95   by (unfold int_or_def) (simp add: bin_rec_PM)
    96   
    97 lemma int_or_Min [simp, code func]:
    98   "Int.Min OR x = Int.Min"
    99   by (unfold int_or_def) (simp add: bin_rec_PM)
   100 
   101 lemma int_or_Bits [simp]: 
   102   "(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
   103   unfolding int_or_def by (simp add: bin_rec_simps)
   104 
   105 lemma int_or_Bits2 [simp, code func]: 
   106   "(Int.Bit0 x) OR (Int.Bit0 y) = Int.Bit0 (x OR y)"
   107   "(Int.Bit0 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
   108   "(Int.Bit1 x) OR (Int.Bit0 y) = Int.Bit1 (x OR y)"
   109   "(Int.Bit1 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
   110   unfolding BIT_simps [symmetric] int_or_Bits by simp_all
   111 
   112 lemma int_or_x_simps': 
   113   "w OR (Int.Pls BIT bit.B0) = w"
   114   "w OR (Int.Min BIT bit.B1) = Int.Min"
   115   apply (induct w rule: bin_induct)
   116        apply simp_all[4]
   117    apply (unfold int_or_Bits)
   118    apply clarsimp+
   119   done
   120 
   121 lemma int_or_extra_simps [simp, code func]:
   122   "w OR Int.Pls = w"
   123   "w OR Int.Min = Int.Min"
   124   using int_or_x_simps' by simp_all
   125 
   126 lemma int_and_Pls [simp, code func]:
   127   "Int.Pls AND x = Int.Pls"
   128   unfolding int_and_def by (simp add: bin_rec_PM)
   129 
   130 lemma int_and_Min [simp, code func]:
   131   "Int.Min AND x = x"
   132   unfolding int_and_def by (simp add: bin_rec_PM)
   133 
   134 lemma int_and_Bits [simp]: 
   135   "(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)" 
   136   unfolding int_and_def by (simp add: bin_rec_simps)
   137 
   138 lemma int_and_Bits2 [simp, code func]: 
   139   "(Int.Bit0 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
   140   "(Int.Bit0 x) AND (Int.Bit1 y) = Int.Bit0 (x AND y)"
   141   "(Int.Bit1 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
   142   "(Int.Bit1 x) AND (Int.Bit1 y) = Int.Bit1 (x AND y)"
   143   unfolding BIT_simps [symmetric] int_and_Bits by simp_all
   144 
   145 lemma int_and_x_simps': 
   146   "w AND (Int.Pls BIT bit.B0) = Int.Pls"
   147   "w AND (Int.Min BIT bit.B1) = w"
   148   apply (induct w rule: bin_induct)
   149        apply simp_all[4]
   150    apply (unfold int_and_Bits)
   151    apply clarsimp+
   152   done
   153 
   154 lemma int_and_extra_simps [simp, code func]:
   155   "w AND Int.Pls = Int.Pls"
   156   "w AND Int.Min = w"
   157   using int_and_x_simps' by simp_all
   158 
   159 (* commutativity of the above *)
   160 lemma bin_ops_comm:
   161   shows
   162   int_and_comm: "!!y::int. x AND y = y AND x" and
   163   int_or_comm:  "!!y::int. x OR y = y OR x" and
   164   int_xor_comm: "!!y::int. x XOR y = y XOR x"
   165   apply (induct x rule: bin_induct)
   166           apply simp_all[6]
   167     apply (case_tac y rule: bin_exhaust, simp add: bit_ops_comm)+
   168   done
   169 
   170 lemma bin_ops_same [simp]:
   171   "(x::int) AND x = x" 
   172   "(x::int) OR x = x" 
   173   "(x::int) XOR x = Int.Pls"
   174   by (induct x rule: bin_induct) auto
   175 
   176 lemma int_not_not [simp]: "NOT (NOT (x::int)) = x"
   177   by (induct x rule: bin_induct) auto
   178 
   179 lemmas bin_log_esimps = 
   180   int_and_extra_simps  int_or_extra_simps  int_xor_extra_simps
   181   int_and_Pls int_and_Min  int_or_Pls int_or_Min  int_xor_Pls int_xor_Min
   182 
   183 (* basic properties of logical (bit-wise) operations *)
   184 
   185 lemma bbw_ao_absorb: 
   186   "!!y::int. x AND (y OR x) = x & x OR (y AND x) = x"
   187   apply (induct x rule: bin_induct)
   188     apply auto 
   189    apply (case_tac [!] y rule: bin_exhaust)
   190    apply auto
   191    apply (case_tac [!] bit)
   192      apply auto
   193   done
   194 
   195 lemma bbw_ao_absorbs_other:
   196   "x AND (x OR y) = x \<and> (y AND x) OR x = (x::int)"
   197   "(y OR x) AND x = x \<and> x OR (x AND y) = (x::int)"
   198   "(x OR y) AND x = x \<and> (x AND y) OR x = (x::int)"
   199   apply (auto simp: bbw_ao_absorb int_or_comm)  
   200       apply (subst int_or_comm)
   201     apply (simp add: bbw_ao_absorb)
   202    apply (subst int_and_comm)
   203    apply (subst int_or_comm)
   204    apply (simp add: bbw_ao_absorb)
   205   apply (subst int_and_comm)
   206   apply (simp add: bbw_ao_absorb)
   207   done
   208 
   209 lemmas bbw_ao_absorbs [simp] = bbw_ao_absorb bbw_ao_absorbs_other
   210 
   211 lemma int_xor_not:
   212   "!!y::int. (NOT x) XOR y = NOT (x XOR y) & 
   213         x XOR (NOT y) = NOT (x XOR y)"
   214   apply (induct x rule: bin_induct)
   215     apply auto
   216    apply (case_tac y rule: bin_exhaust, auto, 
   217           case_tac b, auto)+
   218   done
   219 
   220 lemma bbw_assocs': 
   221   "!!y z::int. (x AND y) AND z = x AND (y AND z) & 
   222           (x OR y) OR z = x OR (y OR z) & 
   223           (x XOR y) XOR z = x XOR (y XOR z)"
   224   apply (induct x rule: bin_induct)
   225     apply (auto simp: int_xor_not)
   226     apply (case_tac [!] y rule: bin_exhaust)
   227     apply (case_tac [!] z rule: bin_exhaust)
   228     apply (case_tac [!] bit)
   229        apply (case_tac [!] b)
   230              apply (auto simp del: BIT_simps)
   231   done
   232 
   233 lemma int_and_assoc:
   234   "(x AND y) AND (z::int) = x AND (y AND z)"
   235   by (simp add: bbw_assocs')
   236 
   237 lemma int_or_assoc:
   238   "(x OR y) OR (z::int) = x OR (y OR z)"
   239   by (simp add: bbw_assocs')
   240 
   241 lemma int_xor_assoc:
   242   "(x XOR y) XOR (z::int) = x XOR (y XOR z)"
   243   by (simp add: bbw_assocs')
   244 
   245 lemmas bbw_assocs = int_and_assoc int_or_assoc int_xor_assoc
   246 
   247 lemma bbw_lcs [simp]: 
   248   "(y::int) AND (x AND z) = x AND (y AND z)"
   249   "(y::int) OR (x OR z) = x OR (y OR z)"
   250   "(y::int) XOR (x XOR z) = x XOR (y XOR z)" 
   251   apply (auto simp: bbw_assocs [symmetric])
   252   apply (auto simp: bin_ops_comm)
   253   done
   254 
   255 lemma bbw_not_dist: 
   256   "!!y::int. NOT (x OR y) = (NOT x) AND (NOT y)" 
   257   "!!y::int. NOT (x AND y) = (NOT x) OR (NOT y)"
   258   apply (induct x rule: bin_induct)
   259        apply auto
   260    apply (case_tac [!] y rule: bin_exhaust)
   261    apply (case_tac [!] bit, auto simp del: BIT_simps)
   262   done
   263 
   264 lemma bbw_oa_dist: 
   265   "!!y z::int. (x AND y) OR z = 
   266           (x OR z) AND (y OR z)"
   267   apply (induct x rule: bin_induct)
   268     apply auto
   269   apply (case_tac y rule: bin_exhaust)
   270   apply (case_tac z rule: bin_exhaust)
   271   apply (case_tac ba, auto simp del: BIT_simps)
   272   done
   273 
   274 lemma bbw_ao_dist: 
   275   "!!y z::int. (x OR y) AND z = 
   276           (x AND z) OR (y AND z)"
   277    apply (induct x rule: bin_induct)
   278     apply auto
   279   apply (case_tac y rule: bin_exhaust)
   280   apply (case_tac z rule: bin_exhaust)
   281   apply (case_tac ba, auto simp del: BIT_simps)
   282   done
   283 
   284 (*
   285 Why were these declared simp???
   286 declare bin_ops_comm [simp] bbw_assocs [simp] 
   287 *)
   288 
   289 lemma plus_and_or [rule_format]:
   290   "ALL y::int. (x AND y) + (x OR y) = x + y"
   291   apply (induct x rule: bin_induct)
   292     apply clarsimp
   293    apply clarsimp
   294   apply clarsimp
   295   apply (case_tac y rule: bin_exhaust)
   296   apply clarsimp
   297   apply (unfold Bit_def)
   298   apply clarsimp
   299   apply (erule_tac x = "x" in allE)
   300   apply (simp split: bit.split)
   301   done
   302 
   303 lemma le_int_or:
   304   "!!x.  bin_sign y = Int.Pls ==> x <= x OR y"
   305   apply (induct y rule: bin_induct)
   306     apply clarsimp
   307    apply clarsimp
   308   apply (case_tac x rule: bin_exhaust)
   309   apply (case_tac b)
   310    apply (case_tac [!] bit)
   311      apply (auto simp: less_eq_int_code)
   312   done
   313 
   314 lemmas int_and_le =
   315   xtr3 [OF bbw_ao_absorbs (2) [THEN conjunct2, symmetric] le_int_or] ;
   316 
   317 lemma bin_nth_ops:
   318   "!!x y. bin_nth (x AND y) n = (bin_nth x n & bin_nth y n)" 
   319   "!!x y. bin_nth (x OR y) n = (bin_nth x n | bin_nth y n)"
   320   "!!x y. bin_nth (x XOR y) n = (bin_nth x n ~= bin_nth y n)" 
   321   "!!x. bin_nth (NOT x) n = (~ bin_nth x n)"
   322   apply (induct n)
   323          apply safe
   324                          apply (case_tac [!] x rule: bin_exhaust)
   325                          apply (simp_all del: BIT_simps)
   326                       apply (case_tac [!] y rule: bin_exhaust)
   327                       apply (simp_all del: BIT_simps)
   328         apply (auto dest: not_B1_is_B0 intro: B1_ass_B0)
   329   done
   330 
   331 (* interaction between bit-wise and arithmetic *)
   332 (* good example of bin_induction *)
   333 lemma bin_add_not: "x + NOT x = Int.Min"
   334   apply (induct x rule: bin_induct)
   335     apply clarsimp
   336    apply clarsimp
   337   apply (case_tac bit, auto)
   338   done
   339 
   340 (* truncating results of bit-wise operations *)
   341 lemma bin_trunc_ao: 
   342   "!!x y. (bintrunc n x) AND (bintrunc n y) = bintrunc n (x AND y)" 
   343   "!!x y. (bintrunc n x) OR (bintrunc n y) = bintrunc n (x OR y)"
   344   apply (induct n)
   345       apply auto
   346       apply (case_tac [!] x rule: bin_exhaust)
   347       apply (case_tac [!] y rule: bin_exhaust)
   348       apply auto
   349   done
   350 
   351 lemma bin_trunc_xor: 
   352   "!!x y. bintrunc n (bintrunc n x XOR bintrunc n y) = 
   353           bintrunc n (x XOR y)"
   354   apply (induct n)
   355    apply auto
   356    apply (case_tac [!] x rule: bin_exhaust)
   357    apply (case_tac [!] y rule: bin_exhaust)
   358    apply auto
   359   done
   360 
   361 lemma bin_trunc_not: 
   362   "!!x. bintrunc n (NOT (bintrunc n x)) = bintrunc n (NOT x)"
   363   apply (induct n)
   364    apply auto
   365    apply (case_tac [!] x rule: bin_exhaust)
   366    apply auto
   367   done
   368 
   369 (* want theorems of the form of bin_trunc_xor *)
   370 lemma bintr_bintr_i:
   371   "x = bintrunc n y ==> bintrunc n x = bintrunc n y"
   372   by auto
   373 
   374 lemmas bin_trunc_and = bin_trunc_ao(1) [THEN bintr_bintr_i]
   375 lemmas bin_trunc_or = bin_trunc_ao(2) [THEN bintr_bintr_i]
   376 
   377 subsection {* Setting and clearing bits *}
   378 
   379 primrec
   380   bin_sc :: "nat => bit => int => int"
   381 where
   382   Z: "bin_sc 0 b w = bin_rest w BIT b"
   383   | Suc: "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w"
   384 
   385 (** nth bit, set/clear **)
   386 
   387 lemma bin_nth_sc [simp]: 
   388   "!!w. bin_nth (bin_sc n b w) n = (b = bit.B1)"
   389   by (induct n)  auto
   390 
   391 lemma bin_sc_sc_same [simp]: 
   392   "!!w. bin_sc n c (bin_sc n b w) = bin_sc n c w"
   393   by (induct n) auto
   394 
   395 lemma bin_sc_sc_diff:
   396   "!!w m. m ~= n ==> 
   397     bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)"
   398   apply (induct n)
   399    apply (case_tac [!] m)
   400      apply auto
   401   done
   402 
   403 lemma bin_nth_sc_gen: 
   404   "!!w m. bin_nth (bin_sc n b w) m = (if m = n then b = bit.B1 else bin_nth w m)"
   405   by (induct n) (case_tac [!] m, auto)
   406   
   407 lemma bin_sc_nth [simp]:
   408   "!!w. (bin_sc n (If (bin_nth w n) bit.B1 bit.B0) w) = w"
   409   by (induct n) auto
   410 
   411 lemma bin_sign_sc [simp]:
   412   "!!w. bin_sign (bin_sc n b w) = bin_sign w"
   413   by (induct n) auto
   414   
   415 lemma bin_sc_bintr [simp]: 
   416   "!!w m. bintrunc m (bin_sc n x (bintrunc m (w))) = bintrunc m (bin_sc n x w)"
   417   apply (induct n)
   418    apply (case_tac [!] w rule: bin_exhaust)
   419    apply (case_tac [!] m, auto)
   420   done
   421 
   422 lemma bin_clr_le:
   423   "!!w. bin_sc n bit.B0 w <= w"
   424   apply (induct n) 
   425    apply (case_tac [!] w rule: bin_exhaust)
   426    apply (auto simp del: BIT_simps)
   427    apply (unfold Bit_def)
   428    apply (simp_all split: bit.split)
   429   done
   430 
   431 lemma bin_set_ge:
   432   "!!w. bin_sc n bit.B1 w >= w"
   433   apply (induct n) 
   434    apply (case_tac [!] w rule: bin_exhaust)
   435    apply (auto simp del: BIT_simps)
   436    apply (unfold Bit_def)
   437    apply (simp_all split: bit.split)
   438   done
   439 
   440 lemma bintr_bin_clr_le:
   441   "!!w m. bintrunc n (bin_sc m bit.B0 w) <= bintrunc n w"
   442   apply (induct n)
   443    apply simp
   444   apply (case_tac w rule: bin_exhaust)
   445   apply (case_tac m)
   446    apply (auto simp del: BIT_simps)
   447    apply (unfold Bit_def)
   448    apply (simp_all split: bit.split)
   449   done
   450 
   451 lemma bintr_bin_set_ge:
   452   "!!w m. bintrunc n (bin_sc m bit.B1 w) >= bintrunc n w"
   453   apply (induct n)
   454    apply simp
   455   apply (case_tac w rule: bin_exhaust)
   456   apply (case_tac m)
   457    apply (auto simp del: BIT_simps)
   458    apply (unfold Bit_def)
   459    apply (simp_all split: bit.split)
   460   done
   461 
   462 lemma bin_sc_FP [simp]: "bin_sc n bit.B0 Int.Pls = Int.Pls"
   463   by (induct n) auto
   464 
   465 lemma bin_sc_TM [simp]: "bin_sc n bit.B1 Int.Min = Int.Min"
   466   by (induct n) auto
   467   
   468 lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP
   469 
   470 lemma bin_sc_minus:
   471   "0 < n ==> bin_sc (Suc (n - 1)) b w = bin_sc n b w"
   472   by auto
   473 
   474 lemmas bin_sc_Suc_minus = 
   475   trans [OF bin_sc_minus [symmetric] bin_sc.Suc, standard]
   476 
   477 lemmas bin_sc_Suc_pred [simp] = 
   478   bin_sc_Suc_minus [of "number_of bin", simplified nobm1, standard]
   479 
   480 subsection {* Operations on lists of booleans *}
   481 
   482 primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int" where
   483   Nil: "bl_to_bin_aux [] w = w"
   484   | Cons: "bl_to_bin_aux (b # bs) w = 
   485       bl_to_bin_aux bs (w BIT (if b then bit.B1 else bit.B0))"
   486 
   487 definition bl_to_bin :: "bool list \<Rightarrow> int" where
   488   bl_to_bin_def : "bl_to_bin bs = bl_to_bin_aux bs Int.Pls"
   489 
   490 primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list" where
   491   Z: "bin_to_bl_aux 0 w bl = bl"
   492   | Suc: "bin_to_bl_aux (Suc n) w bl =
   493       bin_to_bl_aux n (bin_rest w) ((bin_last w = bit.B1) # bl)"
   494 
   495 definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list" where
   496   bin_to_bl_def : "bin_to_bl n w = bin_to_bl_aux n w []"
   497 
   498 primrec bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool list" where
   499   Suc: "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
   500   | Z: "bl_of_nth 0 f = []"
   501 
   502 primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   503   Z: "takefill fill 0 xs = []"
   504   | Suc: "takefill fill (Suc n) xs = (
   505       case xs of [] => fill # takefill fill n xs
   506         | y # ys => y # takefill fill n ys)"
   507 
   508 definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where
   509   "map2 f as bs = map (split f) (zip as bs)"
   510 
   511 
   512 subsection {* Splitting and concatenation *}
   513 
   514 definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int" where
   515   "bin_rcat n = foldl (%u v. bin_cat u n v) Int.Pls"
   516 
   517 fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
   518   "bin_rsplit_aux n m c bs =
   519     (if m = 0 | n = 0 then bs else
   520       let (a, b) = bin_split n c 
   521       in bin_rsplit_aux n (m - n) a (b # bs))"
   522 
   523 definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
   524   "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
   525 
   526 fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
   527   "bin_rsplitl_aux n m c bs =
   528     (if m = 0 | n = 0 then bs else
   529       let (a, b) = bin_split (min m n) c 
   530       in bin_rsplitl_aux n (m - n) a (b # bs))"
   531 
   532 definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
   533   "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"
   534 
   535 declare bin_rsplit_aux.simps [simp del]
   536 declare bin_rsplitl_aux.simps [simp del]
   537 
   538 lemma bin_sign_cat: 
   539   "!!y. bin_sign (bin_cat x n y) = bin_sign x"
   540   by (induct n) auto
   541 
   542 lemma bin_cat_Suc_Bit:
   543   "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b"
   544   by auto
   545 
   546 lemma bin_nth_cat: 
   547   "!!n y. bin_nth (bin_cat x k y) n = 
   548     (if n < k then bin_nth y n else bin_nth x (n - k))"
   549   apply (induct k)
   550    apply clarsimp
   551   apply (case_tac n, auto)
   552   done
   553 
   554 lemma bin_nth_split:
   555   "!!b c. bin_split n c = (a, b) ==> 
   556     (ALL k. bin_nth a k = bin_nth c (n + k)) & 
   557     (ALL k. bin_nth b k = (k < n & bin_nth c k))"
   558   apply (induct n)
   559    apply clarsimp
   560   apply (clarsimp simp: Let_def split: ls_splits)
   561   apply (case_tac k)
   562   apply auto
   563   done
   564 
   565 lemma bin_cat_assoc: 
   566   "!!z. bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)" 
   567   by (induct n) auto
   568 
   569 lemma bin_cat_assoc_sym: "!!z m. 
   570   bin_cat x m (bin_cat y n z) = bin_cat (bin_cat x (m - n) y) (min m n) z"
   571   apply (induct n, clarsimp)
   572   apply (case_tac m, auto)
   573   done
   574 
   575 lemma bin_cat_Pls [simp]: 
   576   "!!w. bin_cat Int.Pls n w = bintrunc n w"
   577   by (induct n) auto
   578 
   579 lemma bintr_cat1: 
   580   "!!b. bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b"
   581   by (induct n) auto
   582     
   583 lemma bintr_cat: "bintrunc m (bin_cat a n b) = 
   584     bin_cat (bintrunc (m - n) a) n (bintrunc (min m n) b)"
   585   by (rule bin_eqI) (auto simp: bin_nth_cat nth_bintr)
   586     
   587 lemma bintr_cat_same [simp]: 
   588   "bintrunc n (bin_cat a n b) = bintrunc n b"
   589   by (auto simp add : bintr_cat)
   590 
   591 lemma cat_bintr [simp]: 
   592   "!!b. bin_cat a n (bintrunc n b) = bin_cat a n b"
   593   by (induct n) auto
   594 
   595 lemma split_bintrunc: 
   596   "!!b c. bin_split n c = (a, b) ==> b = bintrunc n c"
   597   by (induct n) (auto simp: Let_def split: ls_splits)
   598 
   599 lemma bin_cat_split:
   600   "!!v w. bin_split n w = (u, v) ==> w = bin_cat u n v"
   601   by (induct n) (auto simp: Let_def split: ls_splits)
   602 
   603 lemma bin_split_cat:
   604   "!!w. bin_split n (bin_cat v n w) = (v, bintrunc n w)"
   605   by (induct n) auto
   606 
   607 lemma bin_split_Pls [simp]:
   608   "bin_split n Int.Pls = (Int.Pls, Int.Pls)"
   609   by (induct n) (auto simp: Let_def split: ls_splits)
   610 
   611 lemma bin_split_Min [simp]:
   612   "bin_split n Int.Min = (Int.Min, bintrunc n Int.Min)"
   613   by (induct n) (auto simp: Let_def split: ls_splits)
   614 
   615 lemma bin_split_trunc:
   616   "!!m b c. bin_split (min m n) c = (a, b) ==> 
   617     bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)"
   618   apply (induct n, clarsimp)
   619   apply (simp add: bin_rest_trunc Let_def split: ls_splits)
   620   apply (case_tac m)
   621    apply (auto simp: Let_def split: ls_splits)
   622   done
   623 
   624 lemma bin_split_trunc1:
   625   "!!m b c. bin_split n c = (a, b) ==> 
   626     bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)"
   627   apply (induct n, clarsimp)
   628   apply (simp add: bin_rest_trunc Let_def split: ls_splits)
   629   apply (case_tac m)
   630    apply (auto simp: Let_def split: ls_splits)
   631   done
   632 
   633 lemma bin_cat_num:
   634   "!!b. bin_cat a n b = a * 2 ^ n + bintrunc n b"
   635   apply (induct n, clarsimp)
   636   apply (simp add: Bit_def cong: number_of_False_cong)
   637   done
   638 
   639 lemma bin_split_num:
   640   "!!b. bin_split n b = (b div 2 ^ n, b mod 2 ^ n)"
   641   apply (induct n, clarsimp)
   642   apply (simp add: bin_rest_div zdiv_zmult2_eq)
   643   apply (case_tac b rule: bin_exhaust)
   644   apply simp
   645   apply (simp add: Bit_def zmod_zmult_zmult1 p1mod22k
   646               split: bit.split 
   647               cong: number_of_False_cong)
   648   done 
   649 
   650 subsection {* Miscellaneous lemmas *}
   651 
   652 lemma nth_2p_bin: 
   653   "!!m. bin_nth (2 ^ n) m = (m = n)"
   654   apply (induct n)
   655    apply clarsimp
   656    apply safe
   657      apply (case_tac m) 
   658       apply (auto simp: trans [OF numeral_1_eq_1 [symmetric] number_of_eq])
   659    apply (case_tac m) 
   660     apply (auto simp: Bit_B0_2t [symmetric])
   661   done
   662 
   663 (* for use when simplifying with bin_nth_Bit *)
   664 
   665 lemma ex_eq_or:
   666   "(EX m. n = Suc m & (m = k | P m)) = (n = Suc k | (EX m. n = Suc m & P m))"
   667   by auto
   668 
   669 end
   670