prefer "Bits" as theory name for abstract bit operations, similar to "Orderings", "Lattices", "Groups" etc.
1.1 --- a/src/HOL/Word/Bit_Bit.thy Mon Dec 23 16:29:43 2013 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,73 +0,0 @@
1.4 -(* Title: HOL/Word/Bit_Bit.thy
1.5 - Author: Author: Brian Huffman, PSU and Gerwin Klein, NICTA
1.6 -*)
1.7 -
1.8 -header {* Bit operations in $\cal Z_2$ *}
1.9 -
1.10 -theory Bit_Bit
1.11 -imports Bit_Operations "~~/src/HOL/Library/Bit"
1.12 -begin
1.13 -
1.14 -instantiation bit :: bit
1.15 -begin
1.16 -
1.17 -primrec bitNOT_bit where
1.18 - "NOT 0 = (1::bit)"
1.19 - | "NOT 1 = (0::bit)"
1.20 -
1.21 -primrec bitAND_bit where
1.22 - "0 AND y = (0::bit)"
1.23 - | "1 AND y = (y::bit)"
1.24 -
1.25 -primrec bitOR_bit where
1.26 - "0 OR y = (y::bit)"
1.27 - | "1 OR y = (1::bit)"
1.28 -
1.29 -primrec bitXOR_bit where
1.30 - "0 XOR y = (y::bit)"
1.31 - | "1 XOR y = (NOT y :: bit)"
1.32 -
1.33 -instance ..
1.34 -
1.35 -end
1.36 -
1.37 -lemmas bit_simps =
1.38 - bitNOT_bit.simps bitAND_bit.simps bitOR_bit.simps bitXOR_bit.simps
1.39 -
1.40 -lemma bit_extra_simps [simp]:
1.41 - "x AND 0 = (0::bit)"
1.42 - "x AND 1 = (x::bit)"
1.43 - "x OR 1 = (1::bit)"
1.44 - "x OR 0 = (x::bit)"
1.45 - "x XOR 1 = NOT (x::bit)"
1.46 - "x XOR 0 = (x::bit)"
1.47 - by (cases x, auto)+
1.48 -
1.49 -lemma bit_ops_comm:
1.50 - "(x::bit) AND y = y AND x"
1.51 - "(x::bit) OR y = y OR x"
1.52 - "(x::bit) XOR y = y XOR x"
1.53 - by (cases y, auto)+
1.54 -
1.55 -lemma bit_ops_same [simp]:
1.56 - "(x::bit) AND x = x"
1.57 - "(x::bit) OR x = x"
1.58 - "(x::bit) XOR x = 0"
1.59 - by (cases x, auto)+
1.60 -
1.61 -lemma bit_not_not [simp]: "NOT (NOT (x::bit)) = x"
1.62 - by (cases x) auto
1.63 -
1.64 -lemma bit_or_def: "(b::bit) OR c = NOT (NOT b AND NOT c)"
1.65 - by (induct b, simp_all)
1.66 -
1.67 -lemma bit_xor_def: "(b::bit) XOR c = (b AND NOT c) OR (NOT b AND c)"
1.68 - by (induct b, simp_all)
1.69 -
1.70 -lemma bit_NOT_eq_1_iff [simp]: "NOT (b::bit) = 1 \<longleftrightarrow> b = 0"
1.71 - by (induct b, simp_all)
1.72 -
1.73 -lemma bit_AND_eq_1_iff [simp]: "(a::bit) AND b = 1 \<longleftrightarrow> a = 1 \<and> b = 1"
1.74 - by (induct a, simp_all)
1.75 -
1.76 -end
2.1 --- a/src/HOL/Word/Bit_Comparison.thy Mon Dec 23 16:29:43 2013 +0100
2.2 +++ b/src/HOL/Word/Bit_Comparison.thy Mon Dec 23 18:37:51 2013 +0100
2.3 @@ -6,7 +6,7 @@
2.4 *)
2.5
2.6 theory Bit_Comparison
2.7 -imports Type_Length Bit_Operations Bit_Int
2.8 +imports Bits_Int
2.9 begin
2.10
2.11 lemma AND_lower [simp]:
3.1 --- a/src/HOL/Word/Bit_Int.thy Mon Dec 23 16:29:43 2013 +0100
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,681 +0,0 @@
3.4 -(*
3.5 - Author: Jeremy Dawson and Gerwin Klein, NICTA
3.6 -
3.7 - Definitions and basic theorems for bit-wise logical operations
3.8 - for integers expressed using Pls, Min, BIT,
3.9 - and converting them to and from lists of bools.
3.10 -*)
3.11 -
3.12 -header {* Bitwise Operations on Binary Integers *}
3.13 -
3.14 -theory Bit_Int
3.15 -imports Bit_Representation Bit_Operations
3.16 -begin
3.17 -
3.18 -subsection {* Logical operations *}
3.19 -
3.20 -text "bit-wise logical operations on the int type"
3.21 -
3.22 -instantiation int :: bit
3.23 -begin
3.24 -
3.25 -definition int_not_def:
3.26 - "bitNOT = (\<lambda>x::int. - x - 1)"
3.27 -
3.28 -function bitAND_int where
3.29 - "bitAND_int x y =
3.30 - (if x = 0 then 0 else if x = -1 then y else
3.31 - (bin_rest x AND bin_rest y) BIT (bin_last x \<and> bin_last y))"
3.32 - by pat_completeness simp
3.33 -
3.34 -termination
3.35 - by (relation "measure (nat o abs o fst)", simp_all add: bin_rest_def)
3.36 -
3.37 -declare bitAND_int.simps [simp del]
3.38 -
3.39 -definition int_or_def:
3.40 - "bitOR = (\<lambda>x y::int. NOT (NOT x AND NOT y))"
3.41 -
3.42 -definition int_xor_def:
3.43 - "bitXOR = (\<lambda>x y::int. (x AND NOT y) OR (NOT x AND y))"
3.44 -
3.45 -instance ..
3.46 -
3.47 -end
3.48 -
3.49 -subsubsection {* Basic simplification rules *}
3.50 -
3.51 -lemma int_not_BIT [simp]:
3.52 - "NOT (w BIT b) = (NOT w) BIT (\<not> b)"
3.53 - unfolding int_not_def Bit_def by (cases b, simp_all)
3.54 -
3.55 -lemma int_not_simps [simp]:
3.56 - "NOT (0::int) = -1"
3.57 - "NOT (1::int) = -2"
3.58 - "NOT (- 1::int) = 0"
3.59 - "NOT (numeral w::int) = - numeral (w + Num.One)"
3.60 - "NOT (- numeral (Num.Bit0 w)::int) = numeral (Num.BitM w)"
3.61 - "NOT (- numeral (Num.Bit1 w)::int) = numeral (Num.Bit0 w)"
3.62 - unfolding int_not_def by simp_all
3.63 -
3.64 -lemma int_not_not [simp]: "NOT (NOT (x::int)) = x"
3.65 - unfolding int_not_def by simp
3.66 -
3.67 -lemma int_and_0 [simp]: "(0::int) AND x = 0"
3.68 - by (simp add: bitAND_int.simps)
3.69 -
3.70 -lemma int_and_m1 [simp]: "(-1::int) AND x = x"
3.71 - by (simp add: bitAND_int.simps)
3.72 -
3.73 -lemma int_and_Bits [simp]:
3.74 - "(x BIT b) AND (y BIT c) = (x AND y) BIT (b \<and> c)"
3.75 - by (subst bitAND_int.simps, simp add: Bit_eq_0_iff Bit_eq_m1_iff)
3.76 -
3.77 -lemma int_or_zero [simp]: "(0::int) OR x = x"
3.78 - unfolding int_or_def by simp
3.79 -
3.80 -lemma int_or_minus1 [simp]: "(-1::int) OR x = -1"
3.81 - unfolding int_or_def by simp
3.82 -
3.83 -lemma int_or_Bits [simp]:
3.84 - "(x BIT b) OR (y BIT c) = (x OR y) BIT (b \<or> c)"
3.85 - unfolding int_or_def by simp
3.86 -
3.87 -lemma int_xor_zero [simp]: "(0::int) XOR x = x"
3.88 - unfolding int_xor_def by simp
3.89 -
3.90 -lemma int_xor_Bits [simp]:
3.91 - "(x BIT b) XOR (y BIT c) = (x XOR y) BIT ((b \<or> c) \<and> \<not> (b \<and> c))"
3.92 - unfolding int_xor_def by auto
3.93 -
3.94 -subsubsection {* Binary destructors *}
3.95 -
3.96 -lemma bin_rest_NOT [simp]: "bin_rest (NOT x) = NOT (bin_rest x)"
3.97 - by (cases x rule: bin_exhaust, simp)
3.98 -
3.99 -lemma bin_last_NOT [simp]: "bin_last (NOT x) \<longleftrightarrow> \<not> bin_last x"
3.100 - by (cases x rule: bin_exhaust, simp)
3.101 -
3.102 -lemma bin_rest_AND [simp]: "bin_rest (x AND y) = bin_rest x AND bin_rest y"
3.103 - by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
3.104 -
3.105 -lemma bin_last_AND [simp]: "bin_last (x AND y) \<longleftrightarrow> bin_last x \<and> bin_last y"
3.106 - by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
3.107 -
3.108 -lemma bin_rest_OR [simp]: "bin_rest (x OR y) = bin_rest x OR bin_rest y"
3.109 - by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
3.110 -
3.111 -lemma bin_last_OR [simp]: "bin_last (x OR y) \<longleftrightarrow> bin_last x \<or> bin_last y"
3.112 - by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
3.113 -
3.114 -lemma bin_rest_XOR [simp]: "bin_rest (x XOR y) = bin_rest x XOR bin_rest y"
3.115 - by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
3.116 -
3.117 -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)"
3.118 - by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
3.119 -
3.120 -lemma bin_nth_ops:
3.121 - "!!x y. bin_nth (x AND y) n = (bin_nth x n & bin_nth y n)"
3.122 - "!!x y. bin_nth (x OR y) n = (bin_nth x n | bin_nth y n)"
3.123 - "!!x y. bin_nth (x XOR y) n = (bin_nth x n ~= bin_nth y n)"
3.124 - "!!x. bin_nth (NOT x) n = (~ bin_nth x n)"
3.125 - by (induct n) auto
3.126 -
3.127 -subsubsection {* Derived properties *}
3.128 -
3.129 -lemma int_xor_minus1 [simp]: "(-1::int) XOR x = NOT x"
3.130 - by (auto simp add: bin_eq_iff bin_nth_ops)
3.131 -
3.132 -lemma int_xor_extra_simps [simp]:
3.133 - "w XOR (0::int) = w"
3.134 - "w XOR (-1::int) = NOT w"
3.135 - by (auto simp add: bin_eq_iff bin_nth_ops)
3.136 -
3.137 -lemma int_or_extra_simps [simp]:
3.138 - "w OR (0::int) = w"
3.139 - "w OR (-1::int) = -1"
3.140 - by (auto simp add: bin_eq_iff bin_nth_ops)
3.141 -
3.142 -lemma int_and_extra_simps [simp]:
3.143 - "w AND (0::int) = 0"
3.144 - "w AND (-1::int) = w"
3.145 - by (auto simp add: bin_eq_iff bin_nth_ops)
3.146 -
3.147 -(* commutativity of the above *)
3.148 -lemma bin_ops_comm:
3.149 - shows
3.150 - int_and_comm: "!!y::int. x AND y = y AND x" and
3.151 - int_or_comm: "!!y::int. x OR y = y OR x" and
3.152 - int_xor_comm: "!!y::int. x XOR y = y XOR x"
3.153 - by (auto simp add: bin_eq_iff bin_nth_ops)
3.154 -
3.155 -lemma bin_ops_same [simp]:
3.156 - "(x::int) AND x = x"
3.157 - "(x::int) OR x = x"
3.158 - "(x::int) XOR x = 0"
3.159 - by (auto simp add: bin_eq_iff bin_nth_ops)
3.160 -
3.161 -lemmas bin_log_esimps =
3.162 - int_and_extra_simps int_or_extra_simps int_xor_extra_simps
3.163 - int_and_0 int_and_m1 int_or_zero int_or_minus1 int_xor_zero int_xor_minus1
3.164 -
3.165 -(* basic properties of logical (bit-wise) operations *)
3.166 -
3.167 -lemma bbw_ao_absorb:
3.168 - "!!y::int. x AND (y OR x) = x & x OR (y AND x) = x"
3.169 - by (auto simp add: bin_eq_iff bin_nth_ops)
3.170 -
3.171 -lemma bbw_ao_absorbs_other:
3.172 - "x AND (x OR y) = x \<and> (y AND x) OR x = (x::int)"
3.173 - "(y OR x) AND x = x \<and> x OR (x AND y) = (x::int)"
3.174 - "(x OR y) AND x = x \<and> (x AND y) OR x = (x::int)"
3.175 - by (auto simp add: bin_eq_iff bin_nth_ops)
3.176 -
3.177 -lemmas bbw_ao_absorbs [simp] = bbw_ao_absorb bbw_ao_absorbs_other
3.178 -
3.179 -lemma int_xor_not:
3.180 - "!!y::int. (NOT x) XOR y = NOT (x XOR y) &
3.181 - x XOR (NOT y) = NOT (x XOR y)"
3.182 - by (auto simp add: bin_eq_iff bin_nth_ops)
3.183 -
3.184 -lemma int_and_assoc:
3.185 - "(x AND y) AND (z::int) = x AND (y AND z)"
3.186 - by (auto simp add: bin_eq_iff bin_nth_ops)
3.187 -
3.188 -lemma int_or_assoc:
3.189 - "(x OR y) OR (z::int) = x OR (y OR z)"
3.190 - by (auto simp add: bin_eq_iff bin_nth_ops)
3.191 -
3.192 -lemma int_xor_assoc:
3.193 - "(x XOR y) XOR (z::int) = x XOR (y XOR z)"
3.194 - by (auto simp add: bin_eq_iff bin_nth_ops)
3.195 -
3.196 -lemmas bbw_assocs = int_and_assoc int_or_assoc int_xor_assoc
3.197 -
3.198 -(* BH: Why are these declared as simp rules??? *)
3.199 -lemma bbw_lcs [simp]:
3.200 - "(y::int) AND (x AND z) = x AND (y AND z)"
3.201 - "(y::int) OR (x OR z) = x OR (y OR z)"
3.202 - "(y::int) XOR (x XOR z) = x XOR (y XOR z)"
3.203 - by (auto simp add: bin_eq_iff bin_nth_ops)
3.204 -
3.205 -lemma bbw_not_dist:
3.206 - "!!y::int. NOT (x OR y) = (NOT x) AND (NOT y)"
3.207 - "!!y::int. NOT (x AND y) = (NOT x) OR (NOT y)"
3.208 - by (auto simp add: bin_eq_iff bin_nth_ops)
3.209 -
3.210 -lemma bbw_oa_dist:
3.211 - "!!y z::int. (x AND y) OR z =
3.212 - (x OR z) AND (y OR z)"
3.213 - by (auto simp add: bin_eq_iff bin_nth_ops)
3.214 -
3.215 -lemma bbw_ao_dist:
3.216 - "!!y z::int. (x OR y) AND z =
3.217 - (x AND z) OR (y AND z)"
3.218 - by (auto simp add: bin_eq_iff bin_nth_ops)
3.219 -
3.220 -(*
3.221 -Why were these declared simp???
3.222 -declare bin_ops_comm [simp] bbw_assocs [simp]
3.223 -*)
3.224 -
3.225 -subsubsection {* Simplification with numerals *}
3.226 -
3.227 -text {* Cases for @{text "0"} and @{text "-1"} are already covered by
3.228 - other simp rules. *}
3.229 -
3.230 -lemma bin_rl_eqI: "\<lbrakk>bin_rest x = bin_rest y; bin_last x = bin_last y\<rbrakk> \<Longrightarrow> x = y"
3.231 - by (metis (mono_tags) BIT_eq_iff bin_ex_rl bin_last_BIT bin_rest_BIT)
3.232 -
3.233 -lemma bin_rest_neg_numeral_BitM [simp]:
3.234 - "bin_rest (- numeral (Num.BitM w)) = - numeral w"
3.235 - by (simp only: BIT_bin_simps [symmetric] bin_rest_BIT)
3.236 -
3.237 -lemma bin_last_neg_numeral_BitM [simp]:
3.238 - "bin_last (- numeral (Num.BitM w))"
3.239 - by (simp only: BIT_bin_simps [symmetric] bin_last_BIT)
3.240 -
3.241 -text {* FIXME: The rule sets below are very large (24 rules for each
3.242 - operator). Is there a simpler way to do this? *}
3.243 -
3.244 -lemma int_and_numerals [simp]:
3.245 - "numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (numeral x AND numeral y) BIT False"
3.246 - "numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (numeral x AND numeral y) BIT False"
3.247 - "numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (numeral x AND numeral y) BIT False"
3.248 - "numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = (numeral x AND numeral y) BIT True"
3.249 - "numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (numeral x AND - numeral y) BIT False"
3.250 - "numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (numeral x AND - numeral (y + Num.One)) BIT False"
3.251 - "numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (numeral x AND - numeral y) BIT False"
3.252 - "numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = (numeral x AND - numeral (y + Num.One)) BIT True"
3.253 - "- numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (- numeral x AND numeral y) BIT False"
3.254 - "- numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (- numeral x AND numeral y) BIT False"
3.255 - "- numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (- numeral (x + Num.One) AND numeral y) BIT False"
3.256 - "- numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = (- numeral (x + Num.One) AND numeral y) BIT True"
3.257 - "- numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (- numeral x AND - numeral y) BIT False"
3.258 - "- numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (- numeral x AND - numeral (y + Num.One)) BIT False"
3.259 - "- numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (- numeral (x + Num.One) AND - numeral y) BIT False"
3.260 - "- numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = (- numeral (x + Num.One) AND - numeral (y + Num.One)) BIT True"
3.261 - "(1::int) AND numeral (Num.Bit0 y) = 0"
3.262 - "(1::int) AND numeral (Num.Bit1 y) = 1"
3.263 - "(1::int) AND - numeral (Num.Bit0 y) = 0"
3.264 - "(1::int) AND - numeral (Num.Bit1 y) = 1"
3.265 - "numeral (Num.Bit0 x) AND (1::int) = 0"
3.266 - "numeral (Num.Bit1 x) AND (1::int) = 1"
3.267 - "- numeral (Num.Bit0 x) AND (1::int) = 0"
3.268 - "- numeral (Num.Bit1 x) AND (1::int) = 1"
3.269 - by (rule bin_rl_eqI, simp, simp)+
3.270 -
3.271 -lemma int_or_numerals [simp]:
3.272 - "numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (numeral x OR numeral y) BIT False"
3.273 - "numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = (numeral x OR numeral y) BIT True"
3.274 - "numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = (numeral x OR numeral y) BIT True"
3.275 - "numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = (numeral x OR numeral y) BIT True"
3.276 - "numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (numeral x OR - numeral y) BIT False"
3.277 - "numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = (numeral x OR - numeral (y + Num.One)) BIT True"
3.278 - "numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = (numeral x OR - numeral y) BIT True"
3.279 - "numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = (numeral x OR - numeral (y + Num.One)) BIT True"
3.280 - "- numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (- numeral x OR numeral y) BIT False"
3.281 - "- numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = (- numeral x OR numeral y) BIT True"
3.282 - "- numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = (- numeral (x + Num.One) OR numeral y) BIT True"
3.283 - "- numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = (- numeral (x + Num.One) OR numeral y) BIT True"
3.284 - "- numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (- numeral x OR - numeral y) BIT False"
3.285 - "- numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = (- numeral x OR - numeral (y + Num.One)) BIT True"
3.286 - "- numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = (- numeral (x + Num.One) OR - numeral y) BIT True"
3.287 - "- numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = (- numeral (x + Num.One) OR - numeral (y + Num.One)) BIT True"
3.288 - "(1::int) OR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
3.289 - "(1::int) OR numeral (Num.Bit1 y) = numeral (Num.Bit1 y)"
3.290 - "(1::int) OR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)"
3.291 - "(1::int) OR - numeral (Num.Bit1 y) = - numeral (Num.Bit1 y)"
3.292 - "numeral (Num.Bit0 x) OR (1::int) = numeral (Num.Bit1 x)"
3.293 - "numeral (Num.Bit1 x) OR (1::int) = numeral (Num.Bit1 x)"
3.294 - "- numeral (Num.Bit0 x) OR (1::int) = - numeral (Num.BitM x)"
3.295 - "- numeral (Num.Bit1 x) OR (1::int) = - numeral (Num.Bit1 x)"
3.296 - by (rule bin_rl_eqI, simp, simp)+
3.297 -
3.298 -lemma int_xor_numerals [simp]:
3.299 - "numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (numeral x XOR numeral y) BIT False"
3.300 - "numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = (numeral x XOR numeral y) BIT True"
3.301 - "numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = (numeral x XOR numeral y) BIT True"
3.302 - "numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (numeral x XOR numeral y) BIT False"
3.303 - "numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (numeral x XOR - numeral y) BIT False"
3.304 - "numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = (numeral x XOR - numeral (y + Num.One)) BIT True"
3.305 - "numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = (numeral x XOR - numeral y) BIT True"
3.306 - "numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (numeral x XOR - numeral (y + Num.One)) BIT False"
3.307 - "- numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (- numeral x XOR numeral y) BIT False"
3.308 - "- numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = (- numeral x XOR numeral y) BIT True"
3.309 - "- numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = (- numeral (x + Num.One) XOR numeral y) BIT True"
3.310 - "- numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (- numeral (x + Num.One) XOR numeral y) BIT False"
3.311 - "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (- numeral x XOR - numeral y) BIT False"
3.312 - "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = (- numeral x XOR - numeral (y + Num.One)) BIT True"
3.313 - "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = (- numeral (x + Num.One) XOR - numeral y) BIT True"
3.314 - "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (- numeral (x + Num.One) XOR - numeral (y + Num.One)) BIT False"
3.315 - "(1::int) XOR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
3.316 - "(1::int) XOR numeral (Num.Bit1 y) = numeral (Num.Bit0 y)"
3.317 - "(1::int) XOR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)"
3.318 - "(1::int) XOR - numeral (Num.Bit1 y) = - numeral (Num.Bit0 (y + Num.One))"
3.319 - "numeral (Num.Bit0 x) XOR (1::int) = numeral (Num.Bit1 x)"
3.320 - "numeral (Num.Bit1 x) XOR (1::int) = numeral (Num.Bit0 x)"
3.321 - "- numeral (Num.Bit0 x) XOR (1::int) = - numeral (Num.BitM x)"
3.322 - "- numeral (Num.Bit1 x) XOR (1::int) = - numeral (Num.Bit0 (x + Num.One))"
3.323 - by (rule bin_rl_eqI, simp, simp)+
3.324 -
3.325 -subsubsection {* Interactions with arithmetic *}
3.326 -
3.327 -lemma plus_and_or [rule_format]:
3.328 - "ALL y::int. (x AND y) + (x OR y) = x + y"
3.329 - apply (induct x rule: bin_induct)
3.330 - apply clarsimp
3.331 - apply clarsimp
3.332 - apply clarsimp
3.333 - apply (case_tac y rule: bin_exhaust)
3.334 - apply clarsimp
3.335 - apply (unfold Bit_def)
3.336 - apply clarsimp
3.337 - apply (erule_tac x = "x" in allE)
3.338 - apply simp
3.339 - done
3.340 -
3.341 -lemma le_int_or:
3.342 - "bin_sign (y::int) = 0 ==> x <= x OR y"
3.343 - apply (induct y arbitrary: x rule: bin_induct)
3.344 - apply clarsimp
3.345 - apply clarsimp
3.346 - apply (case_tac x rule: bin_exhaust)
3.347 - apply (case_tac b)
3.348 - apply (case_tac [!] bit)
3.349 - apply (auto simp: le_Bits)
3.350 - done
3.351 -
3.352 -lemmas int_and_le =
3.353 - xtrans(3) [OF bbw_ao_absorbs (2) [THEN conjunct2, symmetric] le_int_or]
3.354 -
3.355 -(* interaction between bit-wise and arithmetic *)
3.356 -(* good example of bin_induction *)
3.357 -lemma bin_add_not: "x + NOT x = (-1::int)"
3.358 - apply (induct x rule: bin_induct)
3.359 - apply clarsimp
3.360 - apply clarsimp
3.361 - apply (case_tac bit, auto)
3.362 - done
3.363 -
3.364 -subsubsection {* Truncating results of bit-wise operations *}
3.365 -
3.366 -lemma bin_trunc_ao:
3.367 - "!!x y. (bintrunc n x) AND (bintrunc n y) = bintrunc n (x AND y)"
3.368 - "!!x y. (bintrunc n x) OR (bintrunc n y) = bintrunc n (x OR y)"
3.369 - by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
3.370 -
3.371 -lemma bin_trunc_xor:
3.372 - "!!x y. bintrunc n (bintrunc n x XOR bintrunc n y) =
3.373 - bintrunc n (x XOR y)"
3.374 - by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
3.375 -
3.376 -lemma bin_trunc_not:
3.377 - "!!x. bintrunc n (NOT (bintrunc n x)) = bintrunc n (NOT x)"
3.378 - by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
3.379 -
3.380 -(* want theorems of the form of bin_trunc_xor *)
3.381 -lemma bintr_bintr_i:
3.382 - "x = bintrunc n y ==> bintrunc n x = bintrunc n y"
3.383 - by auto
3.384 -
3.385 -lemmas bin_trunc_and = bin_trunc_ao(1) [THEN bintr_bintr_i]
3.386 -lemmas bin_trunc_or = bin_trunc_ao(2) [THEN bintr_bintr_i]
3.387 -
3.388 -subsection {* Setting and clearing bits *}
3.389 -
3.390 -primrec
3.391 - bin_sc :: "nat => bool => int => int"
3.392 -where
3.393 - Z: "bin_sc 0 b w = bin_rest w BIT b"
3.394 - | Suc: "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w"
3.395 -
3.396 -(** nth bit, set/clear **)
3.397 -
3.398 -lemma bin_nth_sc [simp]:
3.399 - "bin_nth (bin_sc n b w) n \<longleftrightarrow> b"
3.400 - by (induct n arbitrary: w) auto
3.401 -
3.402 -lemma bin_sc_sc_same [simp]:
3.403 - "bin_sc n c (bin_sc n b w) = bin_sc n c w"
3.404 - by (induct n arbitrary: w) auto
3.405 -
3.406 -lemma bin_sc_sc_diff:
3.407 - "m ~= n ==>
3.408 - bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)"
3.409 - apply (induct n arbitrary: w m)
3.410 - apply (case_tac [!] m)
3.411 - apply auto
3.412 - done
3.413 -
3.414 -lemma bin_nth_sc_gen:
3.415 - "bin_nth (bin_sc n b w) m = (if m = n then b else bin_nth w m)"
3.416 - by (induct n arbitrary: w m) (case_tac [!] m, auto)
3.417 -
3.418 -lemma bin_sc_nth [simp]:
3.419 - "(bin_sc n (bin_nth w n) w) = w"
3.420 - by (induct n arbitrary: w) auto
3.421 -
3.422 -lemma bin_sign_sc [simp]:
3.423 - "bin_sign (bin_sc n b w) = bin_sign w"
3.424 - by (induct n arbitrary: w) auto
3.425 -
3.426 -lemma bin_sc_bintr [simp]:
3.427 - "bintrunc m (bin_sc n x (bintrunc m (w))) = bintrunc m (bin_sc n x w)"
3.428 - apply (induct n arbitrary: w m)
3.429 - apply (case_tac [!] w rule: bin_exhaust)
3.430 - apply (case_tac [!] m, auto)
3.431 - done
3.432 -
3.433 -lemma bin_clr_le:
3.434 - "bin_sc n False w <= w"
3.435 - apply (induct n arbitrary: w)
3.436 - apply (case_tac [!] w rule: bin_exhaust)
3.437 - apply (auto simp: le_Bits)
3.438 - done
3.439 -
3.440 -lemma bin_set_ge:
3.441 - "bin_sc n True w >= w"
3.442 - apply (induct n arbitrary: w)
3.443 - apply (case_tac [!] w rule: bin_exhaust)
3.444 - apply (auto simp: le_Bits)
3.445 - done
3.446 -
3.447 -lemma bintr_bin_clr_le:
3.448 - "bintrunc n (bin_sc m False w) <= bintrunc n w"
3.449 - apply (induct n arbitrary: w m)
3.450 - apply simp
3.451 - apply (case_tac w rule: bin_exhaust)
3.452 - apply (case_tac m)
3.453 - apply (auto simp: le_Bits)
3.454 - done
3.455 -
3.456 -lemma bintr_bin_set_ge:
3.457 - "bintrunc n (bin_sc m True w) >= bintrunc n w"
3.458 - apply (induct n arbitrary: w m)
3.459 - apply simp
3.460 - apply (case_tac w rule: bin_exhaust)
3.461 - apply (case_tac m)
3.462 - apply (auto simp: le_Bits)
3.463 - done
3.464 -
3.465 -lemma bin_sc_FP [simp]: "bin_sc n False 0 = 0"
3.466 - by (induct n) auto
3.467 -
3.468 -lemma bin_sc_TM [simp]: "bin_sc n True -1 = -1"
3.469 - by (induct n) auto
3.470 -
3.471 -lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP
3.472 -
3.473 -lemma bin_sc_minus:
3.474 - "0 < n ==> bin_sc (Suc (n - 1)) b w = bin_sc n b w"
3.475 - by auto
3.476 -
3.477 -lemmas bin_sc_Suc_minus =
3.478 - trans [OF bin_sc_minus [symmetric] bin_sc.Suc]
3.479 -
3.480 -lemma bin_sc_numeral [simp]:
3.481 - "bin_sc (numeral k) b w =
3.482 - bin_sc (pred_numeral k) b (bin_rest w) BIT bin_last w"
3.483 - by (simp add: numeral_eq_Suc)
3.484 -
3.485 -
3.486 -subsection {* Splitting and concatenation *}
3.487 -
3.488 -definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int"
3.489 -where
3.490 - "bin_rcat n = foldl (\<lambda>u v. bin_cat u n v) 0"
3.491 -
3.492 -fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
3.493 -where
3.494 - "bin_rsplit_aux n m c bs =
3.495 - (if m = 0 | n = 0 then bs else
3.496 - let (a, b) = bin_split n c
3.497 - in bin_rsplit_aux n (m - n) a (b # bs))"
3.498 -
3.499 -definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
3.500 -where
3.501 - "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
3.502 -
3.503 -fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
3.504 -where
3.505 - "bin_rsplitl_aux n m c bs =
3.506 - (if m = 0 | n = 0 then bs else
3.507 - let (a, b) = bin_split (min m n) c
3.508 - in bin_rsplitl_aux n (m - n) a (b # bs))"
3.509 -
3.510 -definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
3.511 -where
3.512 - "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"
3.513 -
3.514 -declare bin_rsplit_aux.simps [simp del]
3.515 -declare bin_rsplitl_aux.simps [simp del]
3.516 -
3.517 -lemma bin_sign_cat:
3.518 - "bin_sign (bin_cat x n y) = bin_sign x"
3.519 - by (induct n arbitrary: y) auto
3.520 -
3.521 -lemma bin_cat_Suc_Bit:
3.522 - "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b"
3.523 - by auto
3.524 -
3.525 -lemma bin_nth_cat:
3.526 - "bin_nth (bin_cat x k y) n =
3.527 - (if n < k then bin_nth y n else bin_nth x (n - k))"
3.528 - apply (induct k arbitrary: n y)
3.529 - apply clarsimp
3.530 - apply (case_tac n, auto)
3.531 - done
3.532 -
3.533 -lemma bin_nth_split:
3.534 - "bin_split n c = (a, b) ==>
3.535 - (ALL k. bin_nth a k = bin_nth c (n + k)) &
3.536 - (ALL k. bin_nth b k = (k < n & bin_nth c k))"
3.537 - apply (induct n arbitrary: b c)
3.538 - apply clarsimp
3.539 - apply (clarsimp simp: Let_def split: prod.split_asm)
3.540 - apply (case_tac k)
3.541 - apply auto
3.542 - done
3.543 -
3.544 -lemma bin_cat_assoc:
3.545 - "bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)"
3.546 - by (induct n arbitrary: z) auto
3.547 -
3.548 -lemma bin_cat_assoc_sym:
3.549 - "bin_cat x m (bin_cat y n z) = bin_cat (bin_cat x (m - n) y) (min m n) z"
3.550 - apply (induct n arbitrary: z m, clarsimp)
3.551 - apply (case_tac m, auto)
3.552 - done
3.553 -
3.554 -lemma bin_cat_zero [simp]: "bin_cat 0 n w = bintrunc n w"
3.555 - by (induct n arbitrary: w) auto
3.556 -
3.557 -lemma bintr_cat1:
3.558 - "bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b"
3.559 - by (induct n arbitrary: b) auto
3.560 -
3.561 -lemma bintr_cat: "bintrunc m (bin_cat a n b) =
3.562 - bin_cat (bintrunc (m - n) a) n (bintrunc (min m n) b)"
3.563 - by (rule bin_eqI) (auto simp: bin_nth_cat nth_bintr)
3.564 -
3.565 -lemma bintr_cat_same [simp]:
3.566 - "bintrunc n (bin_cat a n b) = bintrunc n b"
3.567 - by (auto simp add : bintr_cat)
3.568 -
3.569 -lemma cat_bintr [simp]:
3.570 - "bin_cat a n (bintrunc n b) = bin_cat a n b"
3.571 - by (induct n arbitrary: b) auto
3.572 -
3.573 -lemma split_bintrunc:
3.574 - "bin_split n c = (a, b) ==> b = bintrunc n c"
3.575 - by (induct n arbitrary: b c) (auto simp: Let_def split: prod.split_asm)
3.576 -
3.577 -lemma bin_cat_split:
3.578 - "bin_split n w = (u, v) ==> w = bin_cat u n v"
3.579 - by (induct n arbitrary: v w) (auto simp: Let_def split: prod.split_asm)
3.580 -
3.581 -lemma bin_split_cat:
3.582 - "bin_split n (bin_cat v n w) = (v, bintrunc n w)"
3.583 - by (induct n arbitrary: w) auto
3.584 -
3.585 -lemma bin_split_zero [simp]: "bin_split n 0 = (0, 0)"
3.586 - by (induct n) auto
3.587 -
3.588 -lemma bin_split_minus1 [simp]:
3.589 - "bin_split n -1 = (-1, bintrunc n -1)"
3.590 - by (induct n) auto
3.591 -
3.592 -lemma bin_split_trunc:
3.593 - "bin_split (min m n) c = (a, b) ==>
3.594 - bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)"
3.595 - apply (induct n arbitrary: m b c, clarsimp)
3.596 - apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
3.597 - apply (case_tac m)
3.598 - apply (auto simp: Let_def split: prod.split_asm)
3.599 - done
3.600 -
3.601 -lemma bin_split_trunc1:
3.602 - "bin_split n c = (a, b) ==>
3.603 - bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)"
3.604 - apply (induct n arbitrary: m b c, clarsimp)
3.605 - apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
3.606 - apply (case_tac m)
3.607 - apply (auto simp: Let_def split: prod.split_asm)
3.608 - done
3.609 -
3.610 -lemma bin_cat_num:
3.611 - "bin_cat a n b = a * 2 ^ n + bintrunc n b"
3.612 - apply (induct n arbitrary: b, clarsimp)
3.613 - apply (simp add: Bit_def)
3.614 - done
3.615 -
3.616 -lemma bin_split_num:
3.617 - "bin_split n b = (b div 2 ^ n, b mod 2 ^ n)"
3.618 - apply (induct n arbitrary: b, simp)
3.619 - apply (simp add: bin_rest_def zdiv_zmult2_eq)
3.620 - apply (case_tac b rule: bin_exhaust)
3.621 - apply simp
3.622 - apply (simp add: Bit_def mod_mult_mult1 p1mod22k)
3.623 - done
3.624 -
3.625 -subsection {* Miscellaneous lemmas *}
3.626 -
3.627 -lemma nth_2p_bin:
3.628 - "bin_nth (2 ^ n) m = (m = n)"
3.629 - apply (induct n arbitrary: m)
3.630 - apply clarsimp
3.631 - apply safe
3.632 - apply (case_tac m)
3.633 - apply (auto simp: Bit_B0_2t [symmetric])
3.634 - done
3.635 -
3.636 -(* for use when simplifying with bin_nth_Bit *)
3.637 -
3.638 -lemma ex_eq_or:
3.639 - "(EX m. n = Suc m & (m = k | P m)) = (n = Suc k | (EX m. n = Suc m & P m))"
3.640 - by auto
3.641 -
3.642 -lemma power_BIT: "2 ^ (Suc n) - 1 = (2 ^ n - 1) BIT True"
3.643 - unfolding Bit_B1
3.644 - by (induct n) simp_all
3.645 -
3.646 -lemma mod_BIT:
3.647 - "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit"
3.648 -proof -
3.649 - have "bin mod 2 ^ n < 2 ^ n" by simp
3.650 - then have "bin mod 2 ^ n \<le> 2 ^ n - 1" by simp
3.651 - then have "2 * (bin mod 2 ^ n) \<le> 2 * (2 ^ n - 1)"
3.652 - by (rule mult_left_mono) simp
3.653 - then have "2 * (bin mod 2 ^ n) + 1 < 2 * 2 ^ n" by simp
3.654 - then show ?thesis
3.655 - by (auto simp add: Bit_def mod_mult_mult1 mod_add_left_eq [of "2 * bin"]
3.656 - mod_pos_pos_trivial)
3.657 -qed
3.658 -
3.659 -lemma AND_mod:
3.660 - fixes x :: int
3.661 - shows "x AND 2 ^ n - 1 = x mod 2 ^ n"
3.662 -proof (induct x arbitrary: n rule: bin_induct)
3.663 - case 1
3.664 - then show ?case
3.665 - by simp
3.666 -next
3.667 - case 2
3.668 - then show ?case
3.669 - by (simp, simp add: m1mod2k)
3.670 -next
3.671 - case (3 bin bit)
3.672 - show ?case
3.673 - proof (cases n)
3.674 - case 0
3.675 - then show ?thesis by simp
3.676 - next
3.677 - case (Suc m)
3.678 - with 3 show ?thesis
3.679 - by (simp only: power_BIT mod_BIT int_and_Bits) simp
3.680 - qed
3.681 -qed
3.682 -
3.683 -end
3.684 -
4.1 --- a/src/HOL/Word/Bit_Operations.thy Mon Dec 23 16:29:43 2013 +0100
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,39 +0,0 @@
4.4 -(* Title: HOL/Word/Bit_Operations.thy
4.5 - Author: Author: Brian Huffman, PSU and Gerwin Klein, NICTA
4.6 -*)
4.7 -
4.8 -header {* Syntactic classes for bitwise operations *}
4.9 -
4.10 -theory Bit_Operations
4.11 -imports Main
4.12 -begin
4.13 -
4.14 -class bit =
4.15 - fixes bitNOT :: "'a \<Rightarrow> 'a" ("NOT _" [70] 71)
4.16 - and bitAND :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "AND" 64)
4.17 - and bitOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "OR" 59)
4.18 - and bitXOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "XOR" 59)
4.19 -
4.20 -text {*
4.21 - We want the bitwise operations to bind slightly weaker
4.22 - than @{text "+"} and @{text "-"}, but @{text "~~"} to
4.23 - bind slightly stronger than @{text "*"}.
4.24 -*}
4.25 -
4.26 -text {*
4.27 - Testing and shifting operations.
4.28 -*}
4.29 -
4.30 -class bits = bit +
4.31 - fixes test_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool" (infixl "!!" 100)
4.32 - and lsb :: "'a \<Rightarrow> bool"
4.33 - and set_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a"
4.34 - and set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> 'a" (binder "BITS " 10)
4.35 - and shiftl :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl "<<" 55)
4.36 - and shiftr :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl ">>" 55)
4.37 -
4.38 -class bitss = bits +
4.39 - fixes msb :: "'a \<Rightarrow> bool"
4.40 -
4.41 -end
4.42 -
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/Word/Bits.thy Mon Dec 23 18:37:51 2013 +0100
5.3 @@ -0,0 +1,39 @@
5.4 +(* Title: HOL/Word/Bit_Operations.thy
5.5 + Author: Author: Brian Huffman, PSU and Gerwin Klein, NICTA
5.6 +*)
5.7 +
5.8 +header {* Syntactic classes for bitwise operations *}
5.9 +
5.10 +theory Bits
5.11 +imports Main
5.12 +begin
5.13 +
5.14 +class bit =
5.15 + fixes bitNOT :: "'a \<Rightarrow> 'a" ("NOT _" [70] 71)
5.16 + and bitAND :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "AND" 64)
5.17 + and bitOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "OR" 59)
5.18 + and bitXOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "XOR" 59)
5.19 +
5.20 +text {*
5.21 + We want the bitwise operations to bind slightly weaker
5.22 + than @{text "+"} and @{text "-"}, but @{text "~~"} to
5.23 + bind slightly stronger than @{text "*"}.
5.24 +*}
5.25 +
5.26 +text {*
5.27 + Testing and shifting operations.
5.28 +*}
5.29 +
5.30 +class bits = bit +
5.31 + fixes test_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool" (infixl "!!" 100)
5.32 + and lsb :: "'a \<Rightarrow> bool"
5.33 + and set_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a"
5.34 + and set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> 'a" (binder "BITS " 10)
5.35 + and shiftl :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl "<<" 55)
5.36 + and shiftr :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl ">>" 55)
5.37 +
5.38 +class bitss = bits +
5.39 + fixes msb :: "'a \<Rightarrow> bool"
5.40 +
5.41 +end
5.42 +
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/HOL/Word/Bits_Bit.thy Mon Dec 23 18:37:51 2013 +0100
6.3 @@ -0,0 +1,73 @@
6.4 +(* Title: HOL/Word/Bit_Bit.thy
6.5 + Author: Author: Brian Huffman, PSU and Gerwin Klein, NICTA
6.6 +*)
6.7 +
6.8 +header {* Bit operations in $\cal Z_2$ *}
6.9 +
6.10 +theory Bits_Bit
6.11 +imports Bits "~~/src/HOL/Library/Bit"
6.12 +begin
6.13 +
6.14 +instantiation bit :: bit
6.15 +begin
6.16 +
6.17 +primrec bitNOT_bit where
6.18 + "NOT 0 = (1::bit)"
6.19 + | "NOT 1 = (0::bit)"
6.20 +
6.21 +primrec bitAND_bit where
6.22 + "0 AND y = (0::bit)"
6.23 + | "1 AND y = (y::bit)"
6.24 +
6.25 +primrec bitOR_bit where
6.26 + "0 OR y = (y::bit)"
6.27 + | "1 OR y = (1::bit)"
6.28 +
6.29 +primrec bitXOR_bit where
6.30 + "0 XOR y = (y::bit)"
6.31 + | "1 XOR y = (NOT y :: bit)"
6.32 +
6.33 +instance ..
6.34 +
6.35 +end
6.36 +
6.37 +lemmas bit_simps =
6.38 + bitNOT_bit.simps bitAND_bit.simps bitOR_bit.simps bitXOR_bit.simps
6.39 +
6.40 +lemma bit_extra_simps [simp]:
6.41 + "x AND 0 = (0::bit)"
6.42 + "x AND 1 = (x::bit)"
6.43 + "x OR 1 = (1::bit)"
6.44 + "x OR 0 = (x::bit)"
6.45 + "x XOR 1 = NOT (x::bit)"
6.46 + "x XOR 0 = (x::bit)"
6.47 + by (cases x, auto)+
6.48 +
6.49 +lemma bit_ops_comm:
6.50 + "(x::bit) AND y = y AND x"
6.51 + "(x::bit) OR y = y OR x"
6.52 + "(x::bit) XOR y = y XOR x"
6.53 + by (cases y, auto)+
6.54 +
6.55 +lemma bit_ops_same [simp]:
6.56 + "(x::bit) AND x = x"
6.57 + "(x::bit) OR x = x"
6.58 + "(x::bit) XOR x = 0"
6.59 + by (cases x, auto)+
6.60 +
6.61 +lemma bit_not_not [simp]: "NOT (NOT (x::bit)) = x"
6.62 + by (cases x) auto
6.63 +
6.64 +lemma bit_or_def: "(b::bit) OR c = NOT (NOT b AND NOT c)"
6.65 + by (induct b, simp_all)
6.66 +
6.67 +lemma bit_xor_def: "(b::bit) XOR c = (b AND NOT c) OR (NOT b AND c)"
6.68 + by (induct b, simp_all)
6.69 +
6.70 +lemma bit_NOT_eq_1_iff [simp]: "NOT (b::bit) = 1 \<longleftrightarrow> b = 0"
6.71 + by (induct b, simp_all)
6.72 +
6.73 +lemma bit_AND_eq_1_iff [simp]: "(a::bit) AND b = 1 \<longleftrightarrow> a = 1 \<and> b = 1"
6.74 + by (induct a, simp_all)
6.75 +
6.76 +end
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/HOL/Word/Bits_Int.thy Mon Dec 23 18:37:51 2013 +0100
7.3 @@ -0,0 +1,681 @@
7.4 +(*
7.5 + Author: Jeremy Dawson and Gerwin Klein, NICTA
7.6 +
7.7 + Definitions and basic theorems for bit-wise logical operations
7.8 + for integers expressed using Pls, Min, BIT,
7.9 + and converting them to and from lists of bools.
7.10 +*)
7.11 +
7.12 +header {* Bitwise Operations on Binary Integers *}
7.13 +
7.14 +theory Bits_Int
7.15 +imports Bits Bit_Representation
7.16 +begin
7.17 +
7.18 +subsection {* Logical operations *}
7.19 +
7.20 +text "bit-wise logical operations on the int type"
7.21 +
7.22 +instantiation int :: bit
7.23 +begin
7.24 +
7.25 +definition int_not_def:
7.26 + "bitNOT = (\<lambda>x::int. - x - 1)"
7.27 +
7.28 +function bitAND_int where
7.29 + "bitAND_int x y =
7.30 + (if x = 0 then 0 else if x = -1 then y else
7.31 + (bin_rest x AND bin_rest y) BIT (bin_last x \<and> bin_last y))"
7.32 + by pat_completeness simp
7.33 +
7.34 +termination
7.35 + by (relation "measure (nat o abs o fst)", simp_all add: bin_rest_def)
7.36 +
7.37 +declare bitAND_int.simps [simp del]
7.38 +
7.39 +definition int_or_def:
7.40 + "bitOR = (\<lambda>x y::int. NOT (NOT x AND NOT y))"
7.41 +
7.42 +definition int_xor_def:
7.43 + "bitXOR = (\<lambda>x y::int. (x AND NOT y) OR (NOT x AND y))"
7.44 +
7.45 +instance ..
7.46 +
7.47 +end
7.48 +
7.49 +subsubsection {* Basic simplification rules *}
7.50 +
7.51 +lemma int_not_BIT [simp]:
7.52 + "NOT (w BIT b) = (NOT w) BIT (\<not> b)"
7.53 + unfolding int_not_def Bit_def by (cases b, simp_all)
7.54 +
7.55 +lemma int_not_simps [simp]:
7.56 + "NOT (0::int) = -1"
7.57 + "NOT (1::int) = -2"
7.58 + "NOT (- 1::int) = 0"
7.59 + "NOT (numeral w::int) = - numeral (w + Num.One)"
7.60 + "NOT (- numeral (Num.Bit0 w)::int) = numeral (Num.BitM w)"
7.61 + "NOT (- numeral (Num.Bit1 w)::int) = numeral (Num.Bit0 w)"
7.62 + unfolding int_not_def by simp_all
7.63 +
7.64 +lemma int_not_not [simp]: "NOT (NOT (x::int)) = x"
7.65 + unfolding int_not_def by simp
7.66 +
7.67 +lemma int_and_0 [simp]: "(0::int) AND x = 0"
7.68 + by (simp add: bitAND_int.simps)
7.69 +
7.70 +lemma int_and_m1 [simp]: "(-1::int) AND x = x"
7.71 + by (simp add: bitAND_int.simps)
7.72 +
7.73 +lemma int_and_Bits [simp]:
7.74 + "(x BIT b) AND (y BIT c) = (x AND y) BIT (b \<and> c)"
7.75 + by (subst bitAND_int.simps, simp add: Bit_eq_0_iff Bit_eq_m1_iff)
7.76 +
7.77 +lemma int_or_zero [simp]: "(0::int) OR x = x"
7.78 + unfolding int_or_def by simp
7.79 +
7.80 +lemma int_or_minus1 [simp]: "(-1::int) OR x = -1"
7.81 + unfolding int_or_def by simp
7.82 +
7.83 +lemma int_or_Bits [simp]:
7.84 + "(x BIT b) OR (y BIT c) = (x OR y) BIT (b \<or> c)"
7.85 + unfolding int_or_def by simp
7.86 +
7.87 +lemma int_xor_zero [simp]: "(0::int) XOR x = x"
7.88 + unfolding int_xor_def by simp
7.89 +
7.90 +lemma int_xor_Bits [simp]:
7.91 + "(x BIT b) XOR (y BIT c) = (x XOR y) BIT ((b \<or> c) \<and> \<not> (b \<and> c))"
7.92 + unfolding int_xor_def by auto
7.93 +
7.94 +subsubsection {* Binary destructors *}
7.95 +
7.96 +lemma bin_rest_NOT [simp]: "bin_rest (NOT x) = NOT (bin_rest x)"
7.97 + by (cases x rule: bin_exhaust, simp)
7.98 +
7.99 +lemma bin_last_NOT [simp]: "bin_last (NOT x) \<longleftrightarrow> \<not> bin_last x"
7.100 + by (cases x rule: bin_exhaust, simp)
7.101 +
7.102 +lemma bin_rest_AND [simp]: "bin_rest (x AND y) = bin_rest x AND bin_rest y"
7.103 + by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
7.104 +
7.105 +lemma bin_last_AND [simp]: "bin_last (x AND y) \<longleftrightarrow> bin_last x \<and> bin_last y"
7.106 + by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
7.107 +
7.108 +lemma bin_rest_OR [simp]: "bin_rest (x OR y) = bin_rest x OR bin_rest y"
7.109 + by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
7.110 +
7.111 +lemma bin_last_OR [simp]: "bin_last (x OR y) \<longleftrightarrow> bin_last x \<or> bin_last y"
7.112 + by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
7.113 +
7.114 +lemma bin_rest_XOR [simp]: "bin_rest (x XOR y) = bin_rest x XOR bin_rest y"
7.115 + by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
7.116 +
7.117 +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)"
7.118 + by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
7.119 +
7.120 +lemma bin_nth_ops:
7.121 + "!!x y. bin_nth (x AND y) n = (bin_nth x n & bin_nth y n)"
7.122 + "!!x y. bin_nth (x OR y) n = (bin_nth x n | bin_nth y n)"
7.123 + "!!x y. bin_nth (x XOR y) n = (bin_nth x n ~= bin_nth y n)"
7.124 + "!!x. bin_nth (NOT x) n = (~ bin_nth x n)"
7.125 + by (induct n) auto
7.126 +
7.127 +subsubsection {* Derived properties *}
7.128 +
7.129 +lemma int_xor_minus1 [simp]: "(-1::int) XOR x = NOT x"
7.130 + by (auto simp add: bin_eq_iff bin_nth_ops)
7.131 +
7.132 +lemma int_xor_extra_simps [simp]:
7.133 + "w XOR (0::int) = w"
7.134 + "w XOR (-1::int) = NOT w"
7.135 + by (auto simp add: bin_eq_iff bin_nth_ops)
7.136 +
7.137 +lemma int_or_extra_simps [simp]:
7.138 + "w OR (0::int) = w"
7.139 + "w OR (-1::int) = -1"
7.140 + by (auto simp add: bin_eq_iff bin_nth_ops)
7.141 +
7.142 +lemma int_and_extra_simps [simp]:
7.143 + "w AND (0::int) = 0"
7.144 + "w AND (-1::int) = w"
7.145 + by (auto simp add: bin_eq_iff bin_nth_ops)
7.146 +
7.147 +(* commutativity of the above *)
7.148 +lemma bin_ops_comm:
7.149 + shows
7.150 + int_and_comm: "!!y::int. x AND y = y AND x" and
7.151 + int_or_comm: "!!y::int. x OR y = y OR x" and
7.152 + int_xor_comm: "!!y::int. x XOR y = y XOR x"
7.153 + by (auto simp add: bin_eq_iff bin_nth_ops)
7.154 +
7.155 +lemma bin_ops_same [simp]:
7.156 + "(x::int) AND x = x"
7.157 + "(x::int) OR x = x"
7.158 + "(x::int) XOR x = 0"
7.159 + by (auto simp add: bin_eq_iff bin_nth_ops)
7.160 +
7.161 +lemmas bin_log_esimps =
7.162 + int_and_extra_simps int_or_extra_simps int_xor_extra_simps
7.163 + int_and_0 int_and_m1 int_or_zero int_or_minus1 int_xor_zero int_xor_minus1
7.164 +
7.165 +(* basic properties of logical (bit-wise) operations *)
7.166 +
7.167 +lemma bbw_ao_absorb:
7.168 + "!!y::int. x AND (y OR x) = x & x OR (y AND x) = x"
7.169 + by (auto simp add: bin_eq_iff bin_nth_ops)
7.170 +
7.171 +lemma bbw_ao_absorbs_other:
7.172 + "x AND (x OR y) = x \<and> (y AND x) OR x = (x::int)"
7.173 + "(y OR x) AND x = x \<and> x OR (x AND y) = (x::int)"
7.174 + "(x OR y) AND x = x \<and> (x AND y) OR x = (x::int)"
7.175 + by (auto simp add: bin_eq_iff bin_nth_ops)
7.176 +
7.177 +lemmas bbw_ao_absorbs [simp] = bbw_ao_absorb bbw_ao_absorbs_other
7.178 +
7.179 +lemma int_xor_not:
7.180 + "!!y::int. (NOT x) XOR y = NOT (x XOR y) &
7.181 + x XOR (NOT y) = NOT (x XOR y)"
7.182 + by (auto simp add: bin_eq_iff bin_nth_ops)
7.183 +
7.184 +lemma int_and_assoc:
7.185 + "(x AND y) AND (z::int) = x AND (y AND z)"
7.186 + by (auto simp add: bin_eq_iff bin_nth_ops)
7.187 +
7.188 +lemma int_or_assoc:
7.189 + "(x OR y) OR (z::int) = x OR (y OR z)"
7.190 + by (auto simp add: bin_eq_iff bin_nth_ops)
7.191 +
7.192 +lemma int_xor_assoc:
7.193 + "(x XOR y) XOR (z::int) = x XOR (y XOR z)"
7.194 + by (auto simp add: bin_eq_iff bin_nth_ops)
7.195 +
7.196 +lemmas bbw_assocs = int_and_assoc int_or_assoc int_xor_assoc
7.197 +
7.198 +(* BH: Why are these declared as simp rules??? *)
7.199 +lemma bbw_lcs [simp]:
7.200 + "(y::int) AND (x AND z) = x AND (y AND z)"
7.201 + "(y::int) OR (x OR z) = x OR (y OR z)"
7.202 + "(y::int) XOR (x XOR z) = x XOR (y XOR z)"
7.203 + by (auto simp add: bin_eq_iff bin_nth_ops)
7.204 +
7.205 +lemma bbw_not_dist:
7.206 + "!!y::int. NOT (x OR y) = (NOT x) AND (NOT y)"
7.207 + "!!y::int. NOT (x AND y) = (NOT x) OR (NOT y)"
7.208 + by (auto simp add: bin_eq_iff bin_nth_ops)
7.209 +
7.210 +lemma bbw_oa_dist:
7.211 + "!!y z::int. (x AND y) OR z =
7.212 + (x OR z) AND (y OR z)"
7.213 + by (auto simp add: bin_eq_iff bin_nth_ops)
7.214 +
7.215 +lemma bbw_ao_dist:
7.216 + "!!y z::int. (x OR y) AND z =
7.217 + (x AND z) OR (y AND z)"
7.218 + by (auto simp add: bin_eq_iff bin_nth_ops)
7.219 +
7.220 +(*
7.221 +Why were these declared simp???
7.222 +declare bin_ops_comm [simp] bbw_assocs [simp]
7.223 +*)
7.224 +
7.225 +subsubsection {* Simplification with numerals *}
7.226 +
7.227 +text {* Cases for @{text "0"} and @{text "-1"} are already covered by
7.228 + other simp rules. *}
7.229 +
7.230 +lemma bin_rl_eqI: "\<lbrakk>bin_rest x = bin_rest y; bin_last x = bin_last y\<rbrakk> \<Longrightarrow> x = y"
7.231 + by (metis (mono_tags) BIT_eq_iff bin_ex_rl bin_last_BIT bin_rest_BIT)
7.232 +
7.233 +lemma bin_rest_neg_numeral_BitM [simp]:
7.234 + "bin_rest (- numeral (Num.BitM w)) = - numeral w"
7.235 + by (simp only: BIT_bin_simps [symmetric] bin_rest_BIT)
7.236 +
7.237 +lemma bin_last_neg_numeral_BitM [simp]:
7.238 + "bin_last (- numeral (Num.BitM w))"
7.239 + by (simp only: BIT_bin_simps [symmetric] bin_last_BIT)
7.240 +
7.241 +text {* FIXME: The rule sets below are very large (24 rules for each
7.242 + operator). Is there a simpler way to do this? *}
7.243 +
7.244 +lemma int_and_numerals [simp]:
7.245 + "numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (numeral x AND numeral y) BIT False"
7.246 + "numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (numeral x AND numeral y) BIT False"
7.247 + "numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (numeral x AND numeral y) BIT False"
7.248 + "numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = (numeral x AND numeral y) BIT True"
7.249 + "numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (numeral x AND - numeral y) BIT False"
7.250 + "numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (numeral x AND - numeral (y + Num.One)) BIT False"
7.251 + "numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (numeral x AND - numeral y) BIT False"
7.252 + "numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = (numeral x AND - numeral (y + Num.One)) BIT True"
7.253 + "- numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (- numeral x AND numeral y) BIT False"
7.254 + "- numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (- numeral x AND numeral y) BIT False"
7.255 + "- numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (- numeral (x + Num.One) AND numeral y) BIT False"
7.256 + "- numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = (- numeral (x + Num.One) AND numeral y) BIT True"
7.257 + "- numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (- numeral x AND - numeral y) BIT False"
7.258 + "- numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (- numeral x AND - numeral (y + Num.One)) BIT False"
7.259 + "- numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (- numeral (x + Num.One) AND - numeral y) BIT False"
7.260 + "- numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = (- numeral (x + Num.One) AND - numeral (y + Num.One)) BIT True"
7.261 + "(1::int) AND numeral (Num.Bit0 y) = 0"
7.262 + "(1::int) AND numeral (Num.Bit1 y) = 1"
7.263 + "(1::int) AND - numeral (Num.Bit0 y) = 0"
7.264 + "(1::int) AND - numeral (Num.Bit1 y) = 1"
7.265 + "numeral (Num.Bit0 x) AND (1::int) = 0"
7.266 + "numeral (Num.Bit1 x) AND (1::int) = 1"
7.267 + "- numeral (Num.Bit0 x) AND (1::int) = 0"
7.268 + "- numeral (Num.Bit1 x) AND (1::int) = 1"
7.269 + by (rule bin_rl_eqI, simp, simp)+
7.270 +
7.271 +lemma int_or_numerals [simp]:
7.272 + "numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (numeral x OR numeral y) BIT False"
7.273 + "numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = (numeral x OR numeral y) BIT True"
7.274 + "numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = (numeral x OR numeral y) BIT True"
7.275 + "numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = (numeral x OR numeral y) BIT True"
7.276 + "numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (numeral x OR - numeral y) BIT False"
7.277 + "numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = (numeral x OR - numeral (y + Num.One)) BIT True"
7.278 + "numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = (numeral x OR - numeral y) BIT True"
7.279 + "numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = (numeral x OR - numeral (y + Num.One)) BIT True"
7.280 + "- numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (- numeral x OR numeral y) BIT False"
7.281 + "- numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = (- numeral x OR numeral y) BIT True"
7.282 + "- numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = (- numeral (x + Num.One) OR numeral y) BIT True"
7.283 + "- numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = (- numeral (x + Num.One) OR numeral y) BIT True"
7.284 + "- numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (- numeral x OR - numeral y) BIT False"
7.285 + "- numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = (- numeral x OR - numeral (y + Num.One)) BIT True"
7.286 + "- numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = (- numeral (x + Num.One) OR - numeral y) BIT True"
7.287 + "- numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = (- numeral (x + Num.One) OR - numeral (y + Num.One)) BIT True"
7.288 + "(1::int) OR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
7.289 + "(1::int) OR numeral (Num.Bit1 y) = numeral (Num.Bit1 y)"
7.290 + "(1::int) OR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)"
7.291 + "(1::int) OR - numeral (Num.Bit1 y) = - numeral (Num.Bit1 y)"
7.292 + "numeral (Num.Bit0 x) OR (1::int) = numeral (Num.Bit1 x)"
7.293 + "numeral (Num.Bit1 x) OR (1::int) = numeral (Num.Bit1 x)"
7.294 + "- numeral (Num.Bit0 x) OR (1::int) = - numeral (Num.BitM x)"
7.295 + "- numeral (Num.Bit1 x) OR (1::int) = - numeral (Num.Bit1 x)"
7.296 + by (rule bin_rl_eqI, simp, simp)+
7.297 +
7.298 +lemma int_xor_numerals [simp]:
7.299 + "numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (numeral x XOR numeral y) BIT False"
7.300 + "numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = (numeral x XOR numeral y) BIT True"
7.301 + "numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = (numeral x XOR numeral y) BIT True"
7.302 + "numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (numeral x XOR numeral y) BIT False"
7.303 + "numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (numeral x XOR - numeral y) BIT False"
7.304 + "numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = (numeral x XOR - numeral (y + Num.One)) BIT True"
7.305 + "numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = (numeral x XOR - numeral y) BIT True"
7.306 + "numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (numeral x XOR - numeral (y + Num.One)) BIT False"
7.307 + "- numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (- numeral x XOR numeral y) BIT False"
7.308 + "- numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = (- numeral x XOR numeral y) BIT True"
7.309 + "- numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = (- numeral (x + Num.One) XOR numeral y) BIT True"
7.310 + "- numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (- numeral (x + Num.One) XOR numeral y) BIT False"
7.311 + "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (- numeral x XOR - numeral y) BIT False"
7.312 + "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = (- numeral x XOR - numeral (y + Num.One)) BIT True"
7.313 + "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = (- numeral (x + Num.One) XOR - numeral y) BIT True"
7.314 + "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (- numeral (x + Num.One) XOR - numeral (y + Num.One)) BIT False"
7.315 + "(1::int) XOR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
7.316 + "(1::int) XOR numeral (Num.Bit1 y) = numeral (Num.Bit0 y)"
7.317 + "(1::int) XOR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)"
7.318 + "(1::int) XOR - numeral (Num.Bit1 y) = - numeral (Num.Bit0 (y + Num.One))"
7.319 + "numeral (Num.Bit0 x) XOR (1::int) = numeral (Num.Bit1 x)"
7.320 + "numeral (Num.Bit1 x) XOR (1::int) = numeral (Num.Bit0 x)"
7.321 + "- numeral (Num.Bit0 x) XOR (1::int) = - numeral (Num.BitM x)"
7.322 + "- numeral (Num.Bit1 x) XOR (1::int) = - numeral (Num.Bit0 (x + Num.One))"
7.323 + by (rule bin_rl_eqI, simp, simp)+
7.324 +
7.325 +subsubsection {* Interactions with arithmetic *}
7.326 +
7.327 +lemma plus_and_or [rule_format]:
7.328 + "ALL y::int. (x AND y) + (x OR y) = x + y"
7.329 + apply (induct x rule: bin_induct)
7.330 + apply clarsimp
7.331 + apply clarsimp
7.332 + apply clarsimp
7.333 + apply (case_tac y rule: bin_exhaust)
7.334 + apply clarsimp
7.335 + apply (unfold Bit_def)
7.336 + apply clarsimp
7.337 + apply (erule_tac x = "x" in allE)
7.338 + apply simp
7.339 + done
7.340 +
7.341 +lemma le_int_or:
7.342 + "bin_sign (y::int) = 0 ==> x <= x OR y"
7.343 + apply (induct y arbitrary: x rule: bin_induct)
7.344 + apply clarsimp
7.345 + apply clarsimp
7.346 + apply (case_tac x rule: bin_exhaust)
7.347 + apply (case_tac b)
7.348 + apply (case_tac [!] bit)
7.349 + apply (auto simp: le_Bits)
7.350 + done
7.351 +
7.352 +lemmas int_and_le =
7.353 + xtrans(3) [OF bbw_ao_absorbs (2) [THEN conjunct2, symmetric] le_int_or]
7.354 +
7.355 +(* interaction between bit-wise and arithmetic *)
7.356 +(* good example of bin_induction *)
7.357 +lemma bin_add_not: "x + NOT x = (-1::int)"
7.358 + apply (induct x rule: bin_induct)
7.359 + apply clarsimp
7.360 + apply clarsimp
7.361 + apply (case_tac bit, auto)
7.362 + done
7.363 +
7.364 +subsubsection {* Truncating results of bit-wise operations *}
7.365 +
7.366 +lemma bin_trunc_ao:
7.367 + "!!x y. (bintrunc n x) AND (bintrunc n y) = bintrunc n (x AND y)"
7.368 + "!!x y. (bintrunc n x) OR (bintrunc n y) = bintrunc n (x OR y)"
7.369 + by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
7.370 +
7.371 +lemma bin_trunc_xor:
7.372 + "!!x y. bintrunc n (bintrunc n x XOR bintrunc n y) =
7.373 + bintrunc n (x XOR y)"
7.374 + by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
7.375 +
7.376 +lemma bin_trunc_not:
7.377 + "!!x. bintrunc n (NOT (bintrunc n x)) = bintrunc n (NOT x)"
7.378 + by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
7.379 +
7.380 +(* want theorems of the form of bin_trunc_xor *)
7.381 +lemma bintr_bintr_i:
7.382 + "x = bintrunc n y ==> bintrunc n x = bintrunc n y"
7.383 + by auto
7.384 +
7.385 +lemmas bin_trunc_and = bin_trunc_ao(1) [THEN bintr_bintr_i]
7.386 +lemmas bin_trunc_or = bin_trunc_ao(2) [THEN bintr_bintr_i]
7.387 +
7.388 +subsection {* Setting and clearing bits *}
7.389 +
7.390 +primrec
7.391 + bin_sc :: "nat => bool => int => int"
7.392 +where
7.393 + Z: "bin_sc 0 b w = bin_rest w BIT b"
7.394 + | Suc: "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w"
7.395 +
7.396 +(** nth bit, set/clear **)
7.397 +
7.398 +lemma bin_nth_sc [simp]:
7.399 + "bin_nth (bin_sc n b w) n \<longleftrightarrow> b"
7.400 + by (induct n arbitrary: w) auto
7.401 +
7.402 +lemma bin_sc_sc_same [simp]:
7.403 + "bin_sc n c (bin_sc n b w) = bin_sc n c w"
7.404 + by (induct n arbitrary: w) auto
7.405 +
7.406 +lemma bin_sc_sc_diff:
7.407 + "m ~= n ==>
7.408 + bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)"
7.409 + apply (induct n arbitrary: w m)
7.410 + apply (case_tac [!] m)
7.411 + apply auto
7.412 + done
7.413 +
7.414 +lemma bin_nth_sc_gen:
7.415 + "bin_nth (bin_sc n b w) m = (if m = n then b else bin_nth w m)"
7.416 + by (induct n arbitrary: w m) (case_tac [!] m, auto)
7.417 +
7.418 +lemma bin_sc_nth [simp]:
7.419 + "(bin_sc n (bin_nth w n) w) = w"
7.420 + by (induct n arbitrary: w) auto
7.421 +
7.422 +lemma bin_sign_sc [simp]:
7.423 + "bin_sign (bin_sc n b w) = bin_sign w"
7.424 + by (induct n arbitrary: w) auto
7.425 +
7.426 +lemma bin_sc_bintr [simp]:
7.427 + "bintrunc m (bin_sc n x (bintrunc m (w))) = bintrunc m (bin_sc n x w)"
7.428 + apply (induct n arbitrary: w m)
7.429 + apply (case_tac [!] w rule: bin_exhaust)
7.430 + apply (case_tac [!] m, auto)
7.431 + done
7.432 +
7.433 +lemma bin_clr_le:
7.434 + "bin_sc n False w <= w"
7.435 + apply (induct n arbitrary: w)
7.436 + apply (case_tac [!] w rule: bin_exhaust)
7.437 + apply (auto simp: le_Bits)
7.438 + done
7.439 +
7.440 +lemma bin_set_ge:
7.441 + "bin_sc n True w >= w"
7.442 + apply (induct n arbitrary: w)
7.443 + apply (case_tac [!] w rule: bin_exhaust)
7.444 + apply (auto simp: le_Bits)
7.445 + done
7.446 +
7.447 +lemma bintr_bin_clr_le:
7.448 + "bintrunc n (bin_sc m False w) <= bintrunc n w"
7.449 + apply (induct n arbitrary: w m)
7.450 + apply simp
7.451 + apply (case_tac w rule: bin_exhaust)
7.452 + apply (case_tac m)
7.453 + apply (auto simp: le_Bits)
7.454 + done
7.455 +
7.456 +lemma bintr_bin_set_ge:
7.457 + "bintrunc n (bin_sc m True w) >= bintrunc n w"
7.458 + apply (induct n arbitrary: w m)
7.459 + apply simp
7.460 + apply (case_tac w rule: bin_exhaust)
7.461 + apply (case_tac m)
7.462 + apply (auto simp: le_Bits)
7.463 + done
7.464 +
7.465 +lemma bin_sc_FP [simp]: "bin_sc n False 0 = 0"
7.466 + by (induct n) auto
7.467 +
7.468 +lemma bin_sc_TM [simp]: "bin_sc n True -1 = -1"
7.469 + by (induct n) auto
7.470 +
7.471 +lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP
7.472 +
7.473 +lemma bin_sc_minus:
7.474 + "0 < n ==> bin_sc (Suc (n - 1)) b w = bin_sc n b w"
7.475 + by auto
7.476 +
7.477 +lemmas bin_sc_Suc_minus =
7.478 + trans [OF bin_sc_minus [symmetric] bin_sc.Suc]
7.479 +
7.480 +lemma bin_sc_numeral [simp]:
7.481 + "bin_sc (numeral k) b w =
7.482 + bin_sc (pred_numeral k) b (bin_rest w) BIT bin_last w"
7.483 + by (simp add: numeral_eq_Suc)
7.484 +
7.485 +
7.486 +subsection {* Splitting and concatenation *}
7.487 +
7.488 +definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int"
7.489 +where
7.490 + "bin_rcat n = foldl (\<lambda>u v. bin_cat u n v) 0"
7.491 +
7.492 +fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
7.493 +where
7.494 + "bin_rsplit_aux n m c bs =
7.495 + (if m = 0 | n = 0 then bs else
7.496 + let (a, b) = bin_split n c
7.497 + in bin_rsplit_aux n (m - n) a (b # bs))"
7.498 +
7.499 +definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
7.500 +where
7.501 + "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
7.502 +
7.503 +fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list"
7.504 +where
7.505 + "bin_rsplitl_aux n m c bs =
7.506 + (if m = 0 | n = 0 then bs else
7.507 + let (a, b) = bin_split (min m n) c
7.508 + in bin_rsplitl_aux n (m - n) a (b # bs))"
7.509 +
7.510 +definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list"
7.511 +where
7.512 + "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"
7.513 +
7.514 +declare bin_rsplit_aux.simps [simp del]
7.515 +declare bin_rsplitl_aux.simps [simp del]
7.516 +
7.517 +lemma bin_sign_cat:
7.518 + "bin_sign (bin_cat x n y) = bin_sign x"
7.519 + by (induct n arbitrary: y) auto
7.520 +
7.521 +lemma bin_cat_Suc_Bit:
7.522 + "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b"
7.523 + by auto
7.524 +
7.525 +lemma bin_nth_cat:
7.526 + "bin_nth (bin_cat x k y) n =
7.527 + (if n < k then bin_nth y n else bin_nth x (n - k))"
7.528 + apply (induct k arbitrary: n y)
7.529 + apply clarsimp
7.530 + apply (case_tac n, auto)
7.531 + done
7.532 +
7.533 +lemma bin_nth_split:
7.534 + "bin_split n c = (a, b) ==>
7.535 + (ALL k. bin_nth a k = bin_nth c (n + k)) &
7.536 + (ALL k. bin_nth b k = (k < n & bin_nth c k))"
7.537 + apply (induct n arbitrary: b c)
7.538 + apply clarsimp
7.539 + apply (clarsimp simp: Let_def split: prod.split_asm)
7.540 + apply (case_tac k)
7.541 + apply auto
7.542 + done
7.543 +
7.544 +lemma bin_cat_assoc:
7.545 + "bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)"
7.546 + by (induct n arbitrary: z) auto
7.547 +
7.548 +lemma bin_cat_assoc_sym:
7.549 + "bin_cat x m (bin_cat y n z) = bin_cat (bin_cat x (m - n) y) (min m n) z"
7.550 + apply (induct n arbitrary: z m, clarsimp)
7.551 + apply (case_tac m, auto)
7.552 + done
7.553 +
7.554 +lemma bin_cat_zero [simp]: "bin_cat 0 n w = bintrunc n w"
7.555 + by (induct n arbitrary: w) auto
7.556 +
7.557 +lemma bintr_cat1:
7.558 + "bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b"
7.559 + by (induct n arbitrary: b) auto
7.560 +
7.561 +lemma bintr_cat: "bintrunc m (bin_cat a n b) =
7.562 + bin_cat (bintrunc (m - n) a) n (bintrunc (min m n) b)"
7.563 + by (rule bin_eqI) (auto simp: bin_nth_cat nth_bintr)
7.564 +
7.565 +lemma bintr_cat_same [simp]:
7.566 + "bintrunc n (bin_cat a n b) = bintrunc n b"
7.567 + by (auto simp add : bintr_cat)
7.568 +
7.569 +lemma cat_bintr [simp]:
7.570 + "bin_cat a n (bintrunc n b) = bin_cat a n b"
7.571 + by (induct n arbitrary: b) auto
7.572 +
7.573 +lemma split_bintrunc:
7.574 + "bin_split n c = (a, b) ==> b = bintrunc n c"
7.575 + by (induct n arbitrary: b c) (auto simp: Let_def split: prod.split_asm)
7.576 +
7.577 +lemma bin_cat_split:
7.578 + "bin_split n w = (u, v) ==> w = bin_cat u n v"
7.579 + by (induct n arbitrary: v w) (auto simp: Let_def split: prod.split_asm)
7.580 +
7.581 +lemma bin_split_cat:
7.582 + "bin_split n (bin_cat v n w) = (v, bintrunc n w)"
7.583 + by (induct n arbitrary: w) auto
7.584 +
7.585 +lemma bin_split_zero [simp]: "bin_split n 0 = (0, 0)"
7.586 + by (induct n) auto
7.587 +
7.588 +lemma bin_split_minus1 [simp]:
7.589 + "bin_split n -1 = (-1, bintrunc n -1)"
7.590 + by (induct n) auto
7.591 +
7.592 +lemma bin_split_trunc:
7.593 + "bin_split (min m n) c = (a, b) ==>
7.594 + bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)"
7.595 + apply (induct n arbitrary: m b c, clarsimp)
7.596 + apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
7.597 + apply (case_tac m)
7.598 + apply (auto simp: Let_def split: prod.split_asm)
7.599 + done
7.600 +
7.601 +lemma bin_split_trunc1:
7.602 + "bin_split n c = (a, b) ==>
7.603 + bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)"
7.604 + apply (induct n arbitrary: m b c, clarsimp)
7.605 + apply (simp add: bin_rest_trunc Let_def split: prod.split_asm)
7.606 + apply (case_tac m)
7.607 + apply (auto simp: Let_def split: prod.split_asm)
7.608 + done
7.609 +
7.610 +lemma bin_cat_num:
7.611 + "bin_cat a n b = a * 2 ^ n + bintrunc n b"
7.612 + apply (induct n arbitrary: b, clarsimp)
7.613 + apply (simp add: Bit_def)
7.614 + done
7.615 +
7.616 +lemma bin_split_num:
7.617 + "bin_split n b = (b div 2 ^ n, b mod 2 ^ n)"
7.618 + apply (induct n arbitrary: b, simp)
7.619 + apply (simp add: bin_rest_def zdiv_zmult2_eq)
7.620 + apply (case_tac b rule: bin_exhaust)
7.621 + apply simp
7.622 + apply (simp add: Bit_def mod_mult_mult1 p1mod22k)
7.623 + done
7.624 +
7.625 +subsection {* Miscellaneous lemmas *}
7.626 +
7.627 +lemma nth_2p_bin:
7.628 + "bin_nth (2 ^ n) m = (m = n)"
7.629 + apply (induct n arbitrary: m)
7.630 + apply clarsimp
7.631 + apply safe
7.632 + apply (case_tac m)
7.633 + apply (auto simp: Bit_B0_2t [symmetric])
7.634 + done
7.635 +
7.636 +(* for use when simplifying with bin_nth_Bit *)
7.637 +
7.638 +lemma ex_eq_or:
7.639 + "(EX m. n = Suc m & (m = k | P m)) = (n = Suc k | (EX m. n = Suc m & P m))"
7.640 + by auto
7.641 +
7.642 +lemma power_BIT: "2 ^ (Suc n) - 1 = (2 ^ n - 1) BIT True"
7.643 + unfolding Bit_B1
7.644 + by (induct n) simp_all
7.645 +
7.646 +lemma mod_BIT:
7.647 + "bin BIT bit mod 2 ^ Suc n = (bin mod 2 ^ n) BIT bit"
7.648 +proof -
7.649 + have "bin mod 2 ^ n < 2 ^ n" by simp
7.650 + then have "bin mod 2 ^ n \<le> 2 ^ n - 1" by simp
7.651 + then have "2 * (bin mod 2 ^ n) \<le> 2 * (2 ^ n - 1)"
7.652 + by (rule mult_left_mono) simp
7.653 + then have "2 * (bin mod 2 ^ n) + 1 < 2 * 2 ^ n" by simp
7.654 + then show ?thesis
7.655 + by (auto simp add: Bit_def mod_mult_mult1 mod_add_left_eq [of "2 * bin"]
7.656 + mod_pos_pos_trivial)
7.657 +qed
7.658 +
7.659 +lemma AND_mod:
7.660 + fixes x :: int
7.661 + shows "x AND 2 ^ n - 1 = x mod 2 ^ n"
7.662 +proof (induct x arbitrary: n rule: bin_induct)
7.663 + case 1
7.664 + then show ?case
7.665 + by simp
7.666 +next
7.667 + case 2
7.668 + then show ?case
7.669 + by (simp, simp add: m1mod2k)
7.670 +next
7.671 + case (3 bin bit)
7.672 + show ?case
7.673 + proof (cases n)
7.674 + case 0
7.675 + then show ?thesis by simp
7.676 + next
7.677 + case (Suc m)
7.678 + with 3 show ?thesis
7.679 + by (simp only: power_BIT mod_BIT int_and_Bits) simp
7.680 + qed
7.681 +qed
7.682 +
7.683 +end
7.684 +
8.1 --- a/src/HOL/Word/Bool_List_Representation.thy Mon Dec 23 16:29:43 2013 +0100
8.2 +++ b/src/HOL/Word/Bool_List_Representation.thy Mon Dec 23 18:37:51 2013 +0100
8.3 @@ -9,7 +9,7 @@
8.4 header "Bool lists and integers"
8.5
8.6 theory Bool_List_Representation
8.7 -imports Bit_Int
8.8 +imports Bits_Int
8.9 begin
8.10
8.11 definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
9.1 --- a/src/HOL/Word/Word.thy Mon Dec 23 16:29:43 2013 +0100
9.2 +++ b/src/HOL/Word/Word.thy Mon Dec 23 18:37:51 2013 +0100
9.3 @@ -8,7 +8,7 @@
9.4 imports
9.5 Type_Length
9.6 "~~/src/HOL/Library/Boolean_Algebra"
9.7 - Bit_Bit
9.8 + Bits_Bit
9.9 Bool_List_Representation
9.10 Misc_Typedef
9.11 Word_Miscellaneous