|
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 header {* 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 primrec |
|
388 bin_sc :: "nat => bool => int => int" |
|
389 where |
|
390 Z: "bin_sc 0 b w = bin_rest w BIT b" |
|
391 | Suc: "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w" |
|
392 |
|
393 (** nth bit, set/clear **) |
|
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 |