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--
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
```