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