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