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