src/HOL/Word/Bits_Int.thy
 author haftmann Fri Jun 19 07:53:35 2015 +0200 (2015-06-19) changeset 60517 f16e4fb20652 parent 58874 7172c7ffb047 child 61799 4cf66f21b764 permissions -rw-r--r--
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
```     1 (*
```
```     2   Author: Jeremy Dawson and Gerwin Klein, NICTA
```
```     3
```
```     4   Definitions 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 section {* Bitwise Operations on Binary Integers *}
```
```    10
```
```    11 theory Bits_Int
```
```    12 imports Bits Bit_Representation
```
```    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 int_not_def:
```
```    23   "bitNOT = (\<lambda>x::int. - x - 1)"
```
```    24
```
```    25 function bitAND_int where
```
```    26   "bitAND_int x y =
```
```    27     (if x = 0 then 0 else if x = -1 then y else
```
```    28       (bin_rest x AND bin_rest y) BIT (bin_last x \<and> bin_last y))"
```
```    29   by pat_completeness simp
```
```    30
```
```    31 termination
```
```    32   by (relation "measure (nat o abs o fst)", simp_all add: bin_rest_def)
```
```    33
```
```    34 declare bitAND_int.simps [simp del]
```
```    35
```
```    36 definition int_or_def:
```
```    37   "bitOR = (\<lambda>x y::int. NOT (NOT x AND NOT y))"
```
```    38
```
```    39 definition int_xor_def:
```
```    40   "bitXOR = (\<lambda>x y::int. (x AND NOT y) OR (NOT x AND y))"
```
```    41
```
```    42 instance ..
```
```    43
```
```    44 end
```
```    45
```
```    46 subsubsection {* Basic simplification rules *}
```
```    47
```
```    48 lemma int_not_BIT [simp]:
```
```    49   "NOT (w BIT b) = (NOT w) BIT (\<not> b)"
```
```    50   unfolding int_not_def Bit_def by (cases b, simp_all)
```
```    51
```
```    52 lemma int_not_simps [simp]:
```
```    53   "NOT (0::int) = -1"
```
```    54   "NOT (1::int) = -2"
```
```    55   "NOT (- 1::int) = 0"
```
```    56   "NOT (numeral w::int) = - numeral (w + Num.One)"
```
```    57   "NOT (- numeral (Num.Bit0 w)::int) = numeral (Num.BitM w)"
```
```    58   "NOT (- numeral (Num.Bit1 w)::int) = numeral (Num.Bit0 w)"
```
```    59   unfolding int_not_def by simp_all
```
```    60
```
```    61 lemma int_not_not [simp]: "NOT (NOT (x::int)) = x"
```
```    62   unfolding int_not_def by simp
```
```    63
```
```    64 lemma int_and_0 [simp]: "(0::int) AND x = 0"
```
```    65   by (simp add: bitAND_int.simps)
```
```    66
```
```    67 lemma int_and_m1 [simp]: "(-1::int) AND x = x"
```
```    68   by (simp add: bitAND_int.simps)
```
```    69
```
```    70 lemma int_and_Bits [simp]:
```
```    71   "(x BIT b) AND (y BIT c) = (x AND y) BIT (b \<and> c)"
```
```    72   by (subst bitAND_int.simps, simp add: Bit_eq_0_iff Bit_eq_m1_iff)
```
```    73
```
```    74 lemma int_or_zero [simp]: "(0::int) OR x = x"
```
```    75   unfolding int_or_def by simp
```
```    76
```
```    77 lemma int_or_minus1 [simp]: "(-1::int) OR x = -1"
```
```    78   unfolding int_or_def by simp
```
```    79
```
```    80 lemma int_or_Bits [simp]:
```
```    81   "(x BIT b) OR (y BIT c) = (x OR y) BIT (b \<or> c)"
```
```    82   unfolding int_or_def by simp
```
```    83
```
```    84 lemma int_xor_zero [simp]: "(0::int) XOR x = x"
```
```    85   unfolding int_xor_def by simp
```
```    86
```
```    87 lemma int_xor_Bits [simp]:
```
```    88   "(x BIT b) XOR (y BIT c) = (x XOR y) BIT ((b \<or> c) \<and> \<not> (b \<and> c))"
```
```    89   unfolding int_xor_def by auto
```
```    90
```
```    91 subsubsection {* Binary destructors *}
```
```    92
```
```    93 lemma bin_rest_NOT [simp]: "bin_rest (NOT x) = NOT (bin_rest x)"
```
```    94   by (cases x rule: bin_exhaust, simp)
```
```    95
```
```    96 lemma bin_last_NOT [simp]: "bin_last (NOT x) \<longleftrightarrow> \<not> bin_last x"
```
```    97   by (cases x rule: bin_exhaust, simp)
```
```    98
```
```    99 lemma bin_rest_AND [simp]: "bin_rest (x AND y) = bin_rest x AND bin_rest y"
```
```   100   by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
```
```   101
```
```   102 lemma bin_last_AND [simp]: "bin_last (x AND y) \<longleftrightarrow> bin_last x \<and> bin_last y"
```
```   103   by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
```
```   104
```
```   105 lemma bin_rest_OR [simp]: "bin_rest (x OR y) = bin_rest x OR bin_rest y"
```
```   106   by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
```
```   107
```
```   108 lemma bin_last_OR [simp]: "bin_last (x OR y) \<longleftrightarrow> bin_last x \<or> bin_last y"
```
```   109   by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
```
```   110
```
```   111 lemma bin_rest_XOR [simp]: "bin_rest (x XOR y) = bin_rest x XOR bin_rest y"
```
```   112   by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
```
```   113
```
```   114 lemma bin_last_XOR [simp]: "bin_last (x XOR y) \<longleftrightarrow> (bin_last x \<or> bin_last y) \<and> \<not> (bin_last x \<and> bin_last y)"
```
```   115   by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
```
```   116
```
```   117 lemma bin_nth_ops:
```
```   118   "!!x y. bin_nth (x AND y) n = (bin_nth x n & bin_nth y n)"
```
```   119   "!!x y. bin_nth (x OR y) n = (bin_nth x n | bin_nth y n)"
```
```   120   "!!x y. bin_nth (x XOR y) n = (bin_nth x n ~= bin_nth y n)"
```
```   121   "!!x. bin_nth (NOT x) n = (~ bin_nth x n)"
```
```   122   by (induct n) auto
```
```   123
```
```   124 subsubsection {* Derived properties *}
```
```   125
```
```   126 lemma int_xor_minus1 [simp]: "(-1::int) XOR x = NOT x"
```
```   127   by (auto simp add: bin_eq_iff bin_nth_ops)
```
```   128
```
```   129 lemma int_xor_extra_simps [simp]:
```
```   130   "w XOR (0::int) = w"
```
```   131   "w XOR (-1::int) = NOT w"
```
```   132   by (auto simp add: bin_eq_iff bin_nth_ops)
```
```   133
```
```   134 lemma int_or_extra_simps [simp]:
```
```   135   "w OR (0::int) = w"
```
```   136   "w OR (-1::int) = -1"
```
```   137   by (auto simp add: bin_eq_iff bin_nth_ops)
```
```   138
```
```   139 lemma int_and_extra_simps [simp]:
```
```   140   "w AND (0::int) = 0"
```
```   141   "w AND (-1::int) = w"
```
```   142   by (auto simp add: bin_eq_iff bin_nth_ops)
```
```   143
```
```   144 (* commutativity of the above *)
```
```   145 lemma bin_ops_comm:
```
```   146   shows
```
```   147   int_and_comm: "!!y::int. x AND y = y AND x" and
```
```   148   int_or_comm:  "!!y::int. x OR y = y OR x" and
```
```   149   int_xor_comm: "!!y::int. x XOR y = y XOR x"
```
```   150   by (auto simp add: bin_eq_iff bin_nth_ops)
```
```   151
```
```   152 lemma bin_ops_same [simp]:
```
```   153   "(x::int) AND x = x"
```
```   154   "(x::int) OR x = x"
```
```   155   "(x::int) XOR x = 0"
```
```   156   by (auto simp add: bin_eq_iff bin_nth_ops)
```
```   157
```
```   158 lemmas bin_log_esimps =
```
```   159   int_and_extra_simps  int_or_extra_simps  int_xor_extra_simps
```
```   160   int_and_0 int_and_m1 int_or_zero int_or_minus1 int_xor_zero int_xor_minus1
```
```   161
```
```   162 (* basic properties of logical (bit-wise) operations *)
```
```   163
```
```   164 lemma bbw_ao_absorb:
```
```   165   "!!y::int. x AND (y OR x) = x & x OR (y AND x) = x"
```
```   166   by (auto simp add: bin_eq_iff bin_nth_ops)
```
```   167
```
```   168 lemma bbw_ao_absorbs_other:
```
```   169   "x AND (x OR y) = x \<and> (y AND x) OR x = (x::int)"
```
```   170   "(y OR x) AND x = x \<and> x OR (x AND y) = (x::int)"
```
```   171   "(x OR y) AND x = x \<and> (x AND y) OR x = (x::int)"
```
```   172   by (auto simp add: bin_eq_iff bin_nth_ops)
```
```   173
```
```   174 lemmas bbw_ao_absorbs [simp] = bbw_ao_absorb bbw_ao_absorbs_other
```
```   175
```
```   176 lemma int_xor_not:
```
```   177   "!!y::int. (NOT x) XOR y = NOT (x XOR y) &
```
```   178         x XOR (NOT y) = NOT (x XOR y)"
```
```   179   by (auto simp add: bin_eq_iff bin_nth_ops)
```
```   180
```
```   181 lemma int_and_assoc:
```
```   182   "(x AND y) AND (z::int) = x AND (y AND z)"
```
```   183   by (auto simp add: bin_eq_iff bin_nth_ops)
```
```   184
```
```   185 lemma int_or_assoc:
```
```   186   "(x OR y) OR (z::int) = x OR (y OR z)"
```
```   187   by (auto simp add: bin_eq_iff bin_nth_ops)
```
```   188
```
```   189 lemma int_xor_assoc:
```
```   190   "(x XOR y) XOR (z::int) = x XOR (y XOR z)"
```
```   191   by (auto simp add: bin_eq_iff bin_nth_ops)
```
```   192
```
```   193 lemmas bbw_assocs = int_and_assoc int_or_assoc int_xor_assoc
```
```   194
```
```   195 (* BH: Why are these declared as simp rules??? *)
```
```   196 lemma bbw_lcs [simp]:
```
```   197   "(y::int) AND (x AND z) = x AND (y AND z)"
```
```   198   "(y::int) OR (x OR z) = x OR (y OR z)"
```
```   199   "(y::int) XOR (x XOR z) = x XOR (y XOR z)"
```
```   200   by (auto simp add: bin_eq_iff bin_nth_ops)
```
```   201
```
```   202 lemma bbw_not_dist:
```
```   203   "!!y::int. NOT (x OR y) = (NOT x) AND (NOT y)"
```
```   204   "!!y::int. NOT (x AND y) = (NOT x) OR (NOT y)"
```
```   205   by (auto simp add: bin_eq_iff bin_nth_ops)
```
```   206
```
```   207 lemma bbw_oa_dist:
```
```   208   "!!y z::int. (x AND y) OR z =
```
```   209           (x OR z) AND (y OR z)"
```
```   210   by (auto simp add: bin_eq_iff bin_nth_ops)
```
```   211
```
```   212 lemma bbw_ao_dist:
```
```   213   "!!y z::int. (x OR y) AND z =
```
```   214           (x AND z) OR (y AND z)"
```
```   215   by (auto simp add: bin_eq_iff bin_nth_ops)
```
```   216
```
```   217 (*
```
```   218 Why were these declared simp???
```
```   219 declare bin_ops_comm [simp] bbw_assocs [simp]
```
```   220 *)
```
```   221
```
```   222 subsubsection {* Simplification with numerals *}
```
```   223
```
```   224 text {* Cases for @{text "0"} and @{text "-1"} are already covered by
```
```   225   other simp rules. *}
```
```   226
```
```   227 lemma bin_rl_eqI: "\<lbrakk>bin_rest x = bin_rest y; bin_last x = bin_last y\<rbrakk> \<Longrightarrow> x = y"
```
```   228   by (metis (mono_tags) BIT_eq_iff bin_ex_rl bin_last_BIT bin_rest_BIT)
```
```   229
```
```   230 lemma bin_rest_neg_numeral_BitM [simp]:
```
```   231   "bin_rest (- numeral (Num.BitM w)) = - numeral w"
```
```   232   by (simp only: BIT_bin_simps [symmetric] bin_rest_BIT)
```
```   233
```
```   234 lemma bin_last_neg_numeral_BitM [simp]:
```
```   235   "bin_last (- numeral (Num.BitM w))"
```
```   236   by (simp only: BIT_bin_simps [symmetric] bin_last_BIT)
```
```   237
```
```   238 text {* FIXME: The rule sets below are very large (24 rules for each
```
```   239   operator). Is there a simpler way to do this? *}
```
```   240
```
```   241 lemma int_and_numerals [simp]:
```
```   242   "numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (numeral x AND numeral y) BIT False"
```
```   243   "numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (numeral x AND numeral y) BIT False"
```
```   244   "numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (numeral x AND numeral y) BIT False"
```
```   245   "numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = (numeral x AND numeral y) BIT True"
```
```   246   "numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (numeral x AND - numeral y) BIT False"
```
```   247   "numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (numeral x AND - numeral (y + Num.One)) BIT False"
```
```   248   "numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (numeral x AND - numeral y) BIT False"
```
```   249   "numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = (numeral x AND - numeral (y + Num.One)) BIT True"
```
```   250   "- numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (- numeral x AND numeral y) BIT False"
```
```   251   "- numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (- numeral x AND numeral y) BIT False"
```
```   252   "- numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (- numeral (x + Num.One) AND numeral y) BIT False"
```
```   253   "- numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = (- numeral (x + Num.One) AND numeral y) BIT True"
```
```   254   "- numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (- numeral x AND - numeral y) BIT False"
```
```   255   "- numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (- numeral x AND - numeral (y + Num.One)) BIT False"
```
```   256   "- numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (- numeral (x + Num.One) AND - numeral y) BIT False"
```
```   257   "- numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = (- numeral (x + Num.One) AND - numeral (y + Num.One)) BIT True"
```
```   258   "(1::int) AND numeral (Num.Bit0 y) = 0"
```
```   259   "(1::int) AND numeral (Num.Bit1 y) = 1"
```
```   260   "(1::int) AND - numeral (Num.Bit0 y) = 0"
```
```   261   "(1::int) AND - numeral (Num.Bit1 y) = 1"
```
```   262   "numeral (Num.Bit0 x) AND (1::int) = 0"
```
```   263   "numeral (Num.Bit1 x) AND (1::int) = 1"
```
```   264   "- numeral (Num.Bit0 x) AND (1::int) = 0"
```
```   265   "- numeral (Num.Bit1 x) AND (1::int) = 1"
```
```   266   by (rule bin_rl_eqI, simp, simp)+
```
```   267
```
```   268 lemma int_or_numerals [simp]:
```
```   269   "numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (numeral x OR numeral y) BIT False"
```
```   270   "numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = (numeral x OR numeral y) BIT True"
```
```   271   "numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = (numeral x OR numeral y) BIT True"
```
```   272   "numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = (numeral x OR numeral y) BIT True"
```
```   273   "numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (numeral x OR - numeral y) BIT False"
```
```   274   "numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = (numeral x OR - numeral (y + Num.One)) BIT True"
```
```   275   "numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = (numeral x OR - numeral y) BIT True"
```
```   276   "numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = (numeral x OR - numeral (y + Num.One)) BIT True"
```
```   277   "- numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (- numeral x OR numeral y) BIT False"
```
```   278   "- numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = (- numeral x OR numeral y) BIT True"
```
```   279   "- numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = (- numeral (x + Num.One) OR numeral y) BIT True"
```
```   280   "- numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = (- numeral (x + Num.One) OR numeral y) BIT True"
```
```   281   "- numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (- numeral x OR - numeral y) BIT False"
```
```   282   "- numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = (- numeral x OR - numeral (y + Num.One)) BIT True"
```
```   283   "- numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = (- numeral (x + Num.One) OR - numeral y) BIT True"
```
```   284   "- numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = (- numeral (x + Num.One) OR - numeral (y + Num.One)) BIT True"
```
```   285   "(1::int) OR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
```
```   286   "(1::int) OR numeral (Num.Bit1 y) = numeral (Num.Bit1 y)"
```
```   287   "(1::int) OR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)"
```
```   288   "(1::int) OR - numeral (Num.Bit1 y) = - numeral (Num.Bit1 y)"
```
```   289   "numeral (Num.Bit0 x) OR (1::int) = numeral (Num.Bit1 x)"
```
```   290   "numeral (Num.Bit1 x) OR (1::int) = numeral (Num.Bit1 x)"
```
```   291   "- numeral (Num.Bit0 x) OR (1::int) = - numeral (Num.BitM x)"
```
```   292   "- numeral (Num.Bit1 x) OR (1::int) = - numeral (Num.Bit1 x)"
```
```   293   by (rule bin_rl_eqI, simp, simp)+
```
```   294
```
```   295 lemma int_xor_numerals [simp]:
```
```   296   "numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (numeral x XOR numeral y) BIT False"
```
```   297   "numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = (numeral x XOR numeral y) BIT True"
```
```   298   "numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = (numeral x XOR numeral y) BIT True"
```
```   299   "numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (numeral x XOR numeral y) BIT False"
```
```   300   "numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (numeral x XOR - numeral y) BIT False"
```
```   301   "numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = (numeral x XOR - numeral (y + Num.One)) BIT True"
```
```   302   "numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = (numeral x XOR - numeral y) BIT True"
```
```   303   "numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (numeral x XOR - numeral (y + Num.One)) BIT False"
```
```   304   "- numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (- numeral x XOR numeral y) BIT False"
```
```   305   "- numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = (- numeral x XOR numeral y) BIT True"
```
```   306   "- numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = (- numeral (x + Num.One) XOR numeral y) BIT True"
```
```   307   "- numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (- numeral (x + Num.One) XOR numeral y) BIT False"
```
```   308   "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (- numeral x XOR - numeral y) BIT False"
```
```   309   "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = (- numeral x XOR - numeral (y + Num.One)) BIT True"
```
```   310   "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = (- numeral (x + Num.One) XOR - numeral y) BIT True"
```
```   311   "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (- numeral (x + Num.One) XOR - numeral (y + Num.One)) BIT False"
```
```   312   "(1::int) XOR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
```
```   313   "(1::int) XOR numeral (Num.Bit1 y) = numeral (Num.Bit0 y)"
```
```   314   "(1::int) XOR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)"
```
```   315   "(1::int) XOR - numeral (Num.Bit1 y) = - numeral (Num.Bit0 (y + Num.One))"
```
```   316   "numeral (Num.Bit0 x) XOR (1::int) = numeral (Num.Bit1 x)"
```
```   317   "numeral (Num.Bit1 x) XOR (1::int) = numeral (Num.Bit0 x)"
```
```   318   "- numeral (Num.Bit0 x) XOR (1::int) = - numeral (Num.BitM x)"
```
```   319   "- numeral (Num.Bit1 x) XOR (1::int) = - numeral (Num.Bit0 (x + Num.One))"
```
```   320   by (rule bin_rl_eqI, simp, simp)+
```
```   321
```
```   322 subsubsection {* Interactions with arithmetic *}
```
```   323
```
```   324 lemma plus_and_or [rule_format]:
```
```   325   "ALL y::int. (x AND y) + (x OR y) = x + y"
```
```   326   apply (induct x rule: bin_induct)
```
```   327     apply clarsimp
```
```   328    apply clarsimp
```
```   329   apply clarsimp
```
```   330   apply (case_tac y rule: bin_exhaust)
```
```   331   apply clarsimp
```
```   332   apply (unfold Bit_def)
```
```   333   apply clarsimp
```
```   334   apply (erule_tac x = "x" in allE)
```
```   335   apply simp
```
```   336   done
```
```   337
```
```   338 lemma le_int_or:
```
```   339   "bin_sign (y::int) = 0 ==> x <= x OR y"
```
```   340   apply (induct y arbitrary: x rule: bin_induct)
```
```   341     apply clarsimp
```
```   342    apply clarsimp
```
```   343   apply (case_tac x rule: bin_exhaust)
```
```   344   apply (case_tac b)
```
```   345    apply (case_tac [!] bit)
```
```   346      apply (auto simp: le_Bits)
```
```   347   done
```
```   348
```
```   349 lemmas int_and_le =
```
```   350   xtrans(3) [OF bbw_ao_absorbs (2) [THEN conjunct2, symmetric] le_int_or]
```
```   351
```
```   352 (* interaction between bit-wise and arithmetic *)
```
```   353 (* good example of bin_induction *)
```
```   354 lemma bin_add_not: "x + NOT x = (-1::int)"
```
```   355   apply (induct x rule: bin_induct)
```
```   356     apply clarsimp
```
```   357    apply clarsimp
```
```   358   apply (case_tac bit, auto)
```
```   359   done
```
```   360
```
```   361 subsubsection {* Truncating results of bit-wise operations *}
```
```   362
```
```   363 lemma bin_trunc_ao:
```
```   364   "!!x y. (bintrunc n x) AND (bintrunc n y) = bintrunc n (x AND y)"
```
```   365   "!!x y. (bintrunc n x) OR (bintrunc n y) = bintrunc n (x OR y)"
```
```   366   by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
```
```   367
```
```   368 lemma bin_trunc_xor:
```
```   369   "!!x y. bintrunc n (bintrunc n x XOR bintrunc n y) =
```
```   370           bintrunc n (x XOR y)"
```
```   371   by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
```
```   372
```
```   373 lemma bin_trunc_not:
```
```   374   "!!x. bintrunc n (NOT (bintrunc n x)) = bintrunc n (NOT x)"
```
```   375   by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
```
```   376
```
```   377 (* want theorems of the form of bin_trunc_xor *)
```
```   378 lemma bintr_bintr_i:
```
```   379   "x = bintrunc n y ==> bintrunc n x = bintrunc n y"
```
```   380   by auto
```
```   381
```
```   382 lemmas bin_trunc_and = bin_trunc_ao(1) [THEN bintr_bintr_i]
```
```   383 lemmas bin_trunc_or = bin_trunc_ao(2) [THEN bintr_bintr_i]
```
```   384
```
```   385 subsection {* Setting and clearing bits *}
```
```   386
```
```   387 (** nth bit, set/clear **)
```
```   388
```
```   389 primrec
```
```   390   bin_sc :: "nat => bool => int => int"
```
```   391 where
```
```   392   Z: "bin_sc 0 b w = bin_rest w BIT b"
```
```   393   | Suc: "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w"
```
```   394
```
```   395 lemma bin_nth_sc [simp]:
```
```   396   "bin_nth (bin_sc n b w) n \<longleftrightarrow> b"
```
```   397   by (induct n arbitrary: w) auto
```
```   398
```
```   399 lemma bin_sc_sc_same [simp]:
```
```   400   "bin_sc n c (bin_sc n b w) = bin_sc n c w"
```
```   401   by (induct n arbitrary: w) auto
```
```   402
```
```   403 lemma bin_sc_sc_diff:
```
```   404   "m ~= n ==>
```
```   405     bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)"
```
```   406   apply (induct n arbitrary: w m)
```
```   407    apply (case_tac [!] m)
```
```   408      apply auto
```
```   409   done
```
```   410
```
```   411 lemma bin_nth_sc_gen:
```
```   412   "bin_nth (bin_sc n b w) m = (if m = n then b else bin_nth w m)"
```
```   413   by (induct n arbitrary: w m) (case_tac [!] m, auto)
```
```   414
```
```   415 lemma bin_sc_nth [simp]:
```
```   416   "(bin_sc n (bin_nth w n) w) = w"
```
```   417   by (induct n arbitrary: w) auto
```
```   418
```
```   419 lemma bin_sign_sc [simp]:
```
```   420   "bin_sign (bin_sc n b w) = bin_sign w"
```
```   421   by (induct n arbitrary: w) auto
```
```   422
```
```   423 lemma bin_sc_bintr [simp]:
```
```   424   "bintrunc m (bin_sc n x (bintrunc m (w))) = bintrunc m (bin_sc n x w)"
```
```   425   apply (induct n arbitrary: w m)
```
```   426    apply (case_tac [!] w rule: bin_exhaust)
```
```   427    apply (case_tac [!] m, auto)
```
```   428   done
```
```   429
```
```   430 lemma bin_clr_le:
```
```   431   "bin_sc n False w <= w"
```
```   432   apply (induct n arbitrary: w)
```
```   433    apply (case_tac [!] w rule: bin_exhaust)
```
```   434    apply (auto simp: le_Bits)
```
```   435   done
```
```   436
```
```   437 lemma bin_set_ge:
```
```   438   "bin_sc n True w >= w"
```
```   439   apply (induct n arbitrary: w)
```
```   440    apply (case_tac [!] w rule: bin_exhaust)
```
```   441    apply (auto simp: le_Bits)
```
```   442   done
```
```   443
```
```   444 lemma bintr_bin_clr_le:
```
```   445   "bintrunc n (bin_sc m False w) <= bintrunc n w"
```
```   446   apply (induct n arbitrary: w m)
```
```   447    apply simp
```
```   448   apply (case_tac w rule: bin_exhaust)
```
```   449   apply (case_tac m)
```
```   450    apply (auto simp: le_Bits)
```
```   451   done
```
```   452
```
```   453 lemma bintr_bin_set_ge:
```
```   454   "bintrunc n (bin_sc m True w) >= bintrunc n w"
```
```   455   apply (induct n arbitrary: w m)
```
```   456    apply simp
```
```   457   apply (case_tac w rule: bin_exhaust)
```
```   458   apply (case_tac m)
```
```   459    apply (auto simp: le_Bits)
```
```   460   done
```
```   461
```
```   462 lemma bin_sc_FP [simp]: "bin_sc n False 0 = 0"
```
```   463   by (induct n) auto
```
```   464
```
```   465 lemma bin_sc_TM [simp]: "bin_sc n True (- 1) = - 1"
```
```   466   by (induct n) auto
```
```   467
```
```   468 lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP
```
```   469
```
```   470 lemma bin_sc_minus:
```
```   471   "0 < n ==> bin_sc (Suc (n - 1)) b w = bin_sc n b w"
```
```   472   by auto
```
```   473
```
```   474 lemmas bin_sc_Suc_minus =
```
```   475   trans [OF bin_sc_minus [symmetric] bin_sc.Suc]
```
```   476
```
```   477 lemma bin_sc_numeral [simp]:
```
```   478   "bin_sc (numeral k) b w =
```
```   479     bin_sc (pred_numeral k) b (bin_rest w) BIT bin_last w"
```
```   480   by (simp add: numeral_eq_Suc)
```
```   481
```
```   482
```
```   483 subsection {* Splitting and concatenation *}
```
```   484
```
```   485 definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int"
```
```   486 where
```
```   487   "bin_rcat n = foldl (\<lambda>u v. bin_cat u n v) 0"
```
```   488
```
```   489 fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
```
```   490 where
```
```   491   "bin_rsplit_aux n m c bs =
```
```   492     (if m = 0 | n = 0 then bs else
```
```   493       let (a, b) = bin_split n c
```
```   494       in bin_rsplit_aux n (m - n) a (b # bs))"
```
```   495
```
```   496 definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
```
```   497 where
```
```   498   "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
```
```   499
```
```   500 fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
```
```   501 where
```
```   502   "bin_rsplitl_aux n m c bs =
```
```   503     (if m = 0 | n = 0 then bs else
```
```   504       let (a, b) = bin_split (min m n) c
```
```   505       in bin_rsplitl_aux n (m - n) a (b # bs))"
```
```   506
```
```   507 definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
```
```   508 where
```
```   509   "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"
```
```   510
```
```   511 declare bin_rsplit_aux.simps [simp del]
```
```   512 declare bin_rsplitl_aux.simps [simp del]
```
```   513
```
```   514 lemma bin_sign_cat:
```
```   515   "bin_sign (bin_cat x n y) = bin_sign x"
```
```   516   by (induct n arbitrary: y) auto
```
```   517
```
```   518 lemma bin_cat_Suc_Bit:
```
```   519   "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b"
```
```   520   by auto
```
```   521
```
```   522 lemma bin_nth_cat:
```
```   523   "bin_nth (bin_cat x k y) n =
```
```   524     (if n < k then bin_nth y n else bin_nth x (n - k))"
```
```   525   apply (induct k arbitrary: n y)
```
```   526    apply clarsimp
```
```   527   apply (case_tac n, auto)
```
```   528   done
```
```   529
```
```   530 lemma bin_nth_split:
```
```   531   "bin_split n c = (a, b) ==>
```
```   532     (ALL k. bin_nth a k = bin_nth c (n + k)) &
```
```   533     (ALL k. bin_nth b k = (k < n & bin_nth c k))"
```
```   534   apply (induct n arbitrary: b c)
```
```   535    apply clarsimp
```
```   536   apply (clarsimp simp: Let_def split: prod.split_asm)
```
```   537   apply (case_tac k)
```
```   538   apply auto
```
```   539   done
```
```   540
```
```   541 lemma bin_cat_assoc:
```
```   542   "bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)"
```
```   543   by (induct n arbitrary: z) auto
```
```   544
```
```   545 lemma bin_cat_assoc_sym:
```
```   546   "bin_cat x m (bin_cat y n z) = bin_cat (bin_cat x (m - n) y) (min m n) z"
```
```   547   apply (induct n arbitrary: z m, clarsimp)
```
```   548   apply (case_tac m, auto)
```
```   549   done
```
```   550
```
```   551 lemma bin_cat_zero [simp]: "bin_cat 0 n w = bintrunc n w"
```
```   552   by (induct n arbitrary: w) auto
```
```   553
```
```   554 lemma bintr_cat1:
```
```   555   "bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b"
```
```   556   by (induct n arbitrary: b) auto
```
```   557
```
```   558 lemma bintr_cat: "bintrunc m (bin_cat a n b) =
```
```   559     bin_cat (bintrunc (m - n) a) n (bintrunc (min m n) b)"
```
```   560   by (rule bin_eqI) (auto simp: bin_nth_cat nth_bintr)
```
```   561
```
```   562 lemma bintr_cat_same [simp]:
```
```   563   "bintrunc n (bin_cat a n b) = bintrunc n b"
```
```   564   by (auto simp add : bintr_cat)
```
```   565
```
```   566 lemma cat_bintr [simp]:
```
```   567   "bin_cat a n (bintrunc n b) = bin_cat a n b"
```
```   568   by (induct n arbitrary: b) auto
```
```   569
```
```   570 lemma split_bintrunc:
```
```   571   "bin_split n c = (a, b) ==> b = bintrunc n c"
```
```   572   by (induct n arbitrary: b c) (auto simp: Let_def split: prod.split_asm)
```
```   573
```
```   574 lemma bin_cat_split:
```
```   575   "bin_split n w = (u, v) ==> w = bin_cat u n v"
```
```   576   by (induct n arbitrary: v w) (auto simp: Let_def split: prod.split_asm)
```
```   577
```
```   578 lemma bin_split_cat:
```
```   579   "bin_split n (bin_cat v n w) = (v, bintrunc n w)"
```
```   580   by (induct n arbitrary: w) auto
```
```   581
```
```   582 lemma bin_split_zero [simp]: "bin_split n 0 = (0, 0)"
```
```   583   by (induct n) auto
```
```   584
```
```   585 lemma bin_split_minus1 [simp]:
```
```   586   "bin_split n (- 1) = (- 1, bintrunc n (- 1))"
```
```   587   by (induct n) auto
```
```   588
```
```   589 lemma bin_split_trunc:
```
```   590   "bin_split (min m n) c = (a, b) ==>
```
```   591     bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)"
```
```   592   apply (induct n arbitrary: m b c, clarsimp)
```
```   593   apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
```
```   594   apply (case_tac m)
```
```   595    apply (auto simp: Let_def split: prod.split_asm)
```
```   596   done
```
```   597
```
```   598 lemma bin_split_trunc1:
```
```   599   "bin_split n c = (a, b) ==>
```
```   600     bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)"
```
```   601   apply (induct n arbitrary: m b c, clarsimp)
```
```   602   apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
```
```   603   apply (case_tac m)
```
```   604    apply (auto simp: Let_def split: prod.split_asm)
```
```   605   done
```
```   606
```
```   607 lemma bin_cat_num:
```
```   608   "bin_cat a n b = a * 2 ^ n + bintrunc n b"
```
```   609   apply (induct n arbitrary: b, clarsimp)
```
```   610   apply (simp add: Bit_def)
```
```   611   done
```
```   612
```
```   613 lemma bin_split_num:
```
```   614   "bin_split n b = (b div 2 ^ n, b mod 2 ^ n)"
```
```   615   apply (induct n arbitrary: b, simp)
```
```   616   apply (simp add: bin_rest_def zdiv_zmult2_eq)
```
```   617   apply (case_tac b rule: bin_exhaust)
```
```   618   apply simp
```
```   619   apply (simp add: Bit_def mod_mult_mult1 p1mod22k)
```
```   620   done
```
```   621
```
```   622 subsection {* Miscellaneous lemmas *}
```
```   623
```
```   624 lemma nth_2p_bin:
```
```   625   "bin_nth (2 ^ n) m = (m = n)"
```
```   626   apply (induct n arbitrary: m)
```
```   627    apply clarsimp
```
```   628    apply safe
```
```   629    apply (case_tac m)
```
```   630     apply (auto simp: Bit_B0_2t [symmetric])
```
```   631   done
```
```   632
```
```   633 (* for use when simplifying with bin_nth_Bit *)
```
```   634
```
```   635 lemma ex_eq_or:
```
```   636   "(EX m. n = Suc m & (m = k | P m)) = (n = Suc k | (EX m. n = Suc m & P m))"
```
```   637   by auto
```
```   638
```
```   639 lemma power_BIT: "2 ^ (Suc n) - 1 = (2 ^ n - 1) BIT True"
```
```   640   unfolding Bit_B1
```
```   641   by (induct n) simp_all
```
```   642
```
```   643 lemma mod_BIT:
```
```   644   "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit"
```
```   645 proof -
```
```   646   have "bin mod 2 ^ n < 2 ^ n" by simp
```
```   647   then have "bin mod 2 ^ n \<le> 2 ^ n - 1" by simp
```
```   648   then have "2 * (bin mod 2 ^ n) \<le> 2 * (2 ^ n - 1)"
```
```   649     by (rule mult_left_mono) simp
```
```   650   then have "2 * (bin mod 2 ^ n) + 1 < 2 * 2 ^ n" by simp
```
```   651   then show ?thesis
```
```   652     by (auto simp add: Bit_def mod_mult_mult1 mod_add_left_eq [of "2 * bin"]
```
```   653       mod_pos_pos_trivial)
```
```   654 qed
```
```   655
```
```   656 lemma AND_mod:
```
```   657   fixes x :: int
```
```   658   shows "x AND 2 ^ n - 1 = x mod 2 ^ n"
```
```   659 proof (induct x arbitrary: n rule: bin_induct)
```
```   660   case 1
```
```   661   then show ?case
```
```   662     by simp
```
```   663 next
```
```   664   case 2
```
```   665   then show ?case
```
```   666     by (simp, simp add: m1mod2k)
```
```   667 next
```
```   668   case (3 bin bit)
```
```   669   show ?case
```
```   670   proof (cases n)
```
```   671     case 0
```
```   672     then show ?thesis by simp
```
```   673   next
```
```   674     case (Suc m)
```
```   675     with 3 show ?thesis
```
```   676       by (simp only: power_BIT mod_BIT int_and_Bits) simp
```
```   677   qed
```
```   678 qed
```
```   679
```
```   680 end
```
```   681
```