|
1 (* Title: HOL/Word/Word_Bitwise.thy |
|
2 Authors: Thomas Sewell, NICTA and Sascha Boehme, TU Muenchen |
|
3 *) |
|
4 |
|
5 theory Word_Bitwise |
|
6 imports Word |
|
7 begin |
|
8 |
|
9 text \<open>Helper constants used in defining addition\<close> |
|
10 |
|
11 definition xor3 :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool" |
|
12 where "xor3 a b c = (a = (b = c))" |
|
13 |
|
14 definition carry :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool" |
|
15 where "carry a b c = ((a \<and> (b \<or> c)) \<or> (b \<and> c))" |
|
16 |
|
17 lemma carry_simps: |
|
18 "carry True a b = (a \<or> b)" |
|
19 "carry a True b = (a \<or> b)" |
|
20 "carry a b True = (a \<or> b)" |
|
21 "carry False a b = (a \<and> b)" |
|
22 "carry a False b = (a \<and> b)" |
|
23 "carry a b False = (a \<and> b)" |
|
24 by (auto simp add: carry_def) |
|
25 |
|
26 lemma xor3_simps: |
|
27 "xor3 True a b = (a = b)" |
|
28 "xor3 a True b = (a = b)" |
|
29 "xor3 a b True = (a = b)" |
|
30 "xor3 False a b = (a \<noteq> b)" |
|
31 "xor3 a False b = (a \<noteq> b)" |
|
32 "xor3 a b False = (a \<noteq> b)" |
|
33 by (simp_all add: xor3_def) |
|
34 |
|
35 text \<open>Breaking up word equalities into equalities on their |
|
36 bit lists. Equalities are generated and manipulated in the |
|
37 reverse order to \<^const>\<open>to_bl\<close>.\<close> |
|
38 |
|
39 lemma word_eq_rbl_eq: "x = y \<longleftrightarrow> rev (to_bl x) = rev (to_bl y)" |
|
40 by simp |
|
41 |
|
42 lemma rbl_word_or: "rev (to_bl (x OR y)) = map2 (\<or>) (rev (to_bl x)) (rev (to_bl y))" |
|
43 by (simp add: map2_def zip_rev bl_word_or rev_map) |
|
44 |
|
45 lemma rbl_word_and: "rev (to_bl (x AND y)) = map2 (\<and>) (rev (to_bl x)) (rev (to_bl y))" |
|
46 by (simp add: map2_def zip_rev bl_word_and rev_map) |
|
47 |
|
48 lemma rbl_word_xor: "rev (to_bl (x XOR y)) = map2 (\<noteq>) (rev (to_bl x)) (rev (to_bl y))" |
|
49 by (simp add: map2_def zip_rev bl_word_xor rev_map) |
|
50 |
|
51 lemma rbl_word_not: "rev (to_bl (NOT x)) = map Not (rev (to_bl x))" |
|
52 by (simp add: bl_word_not rev_map) |
|
53 |
|
54 lemma bl_word_sub: "to_bl (x - y) = to_bl (x + (- y))" |
|
55 by simp |
|
56 |
|
57 lemma rbl_word_1: "rev (to_bl (1 :: 'a::len0 word)) = takefill False (len_of TYPE('a)) [True]" |
|
58 apply (rule_tac s="rev (to_bl (word_succ (0 :: 'a word)))" in trans) |
|
59 apply simp |
|
60 apply (simp only: rtb_rbl_ariths(1)[OF refl]) |
|
61 apply simp |
|
62 apply (case_tac "len_of TYPE('a)") |
|
63 apply simp |
|
64 apply (simp add: takefill_alt) |
|
65 done |
|
66 |
|
67 lemma rbl_word_if: "rev (to_bl (if P then x else y)) = map2 (If P) (rev (to_bl x)) (rev (to_bl y))" |
|
68 by (simp add: map2_def split_def) |
|
69 |
|
70 lemma rbl_add_carry_Cons: |
|
71 "(if car then rbl_succ else id) (rbl_add (x # xs) (y # ys)) = |
|
72 xor3 x y car # (if carry x y car then rbl_succ else id) (rbl_add xs ys)" |
|
73 by (simp add: carry_def xor3_def) |
|
74 |
|
75 lemma rbl_add_suc_carry_fold: |
|
76 "length xs = length ys \<Longrightarrow> |
|
77 \<forall>car. (if car then rbl_succ else id) (rbl_add xs ys) = |
|
78 (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (zip xs ys) (\<lambda>_. [])) car" |
|
79 apply (erule list_induct2) |
|
80 apply simp |
|
81 apply (simp only: rbl_add_carry_Cons) |
|
82 apply simp |
|
83 done |
|
84 |
|
85 lemma to_bl_plus_carry: |
|
86 "to_bl (x + y) = |
|
87 rev (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) |
|
88 (rev (zip (to_bl x) (to_bl y))) (\<lambda>_. []) False)" |
|
89 using rbl_add_suc_carry_fold[where xs="rev (to_bl x)" and ys="rev (to_bl y)"] |
|
90 apply (simp add: word_add_rbl[OF refl refl]) |
|
91 apply (drule_tac x=False in spec) |
|
92 apply (simp add: zip_rev) |
|
93 done |
|
94 |
|
95 definition "rbl_plus cin xs ys = |
|
96 foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car)) (zip xs ys) (\<lambda>_. []) cin" |
|
97 |
|
98 lemma rbl_plus_simps: |
|
99 "rbl_plus cin (x # xs) (y # ys) = xor3 x y cin # rbl_plus (carry x y cin) xs ys" |
|
100 "rbl_plus cin [] ys = []" |
|
101 "rbl_plus cin xs [] = []" |
|
102 by (simp_all add: rbl_plus_def) |
|
103 |
|
104 lemma rbl_word_plus: "rev (to_bl (x + y)) = rbl_plus False (rev (to_bl x)) (rev (to_bl y))" |
|
105 by (simp add: rbl_plus_def to_bl_plus_carry zip_rev) |
|
106 |
|
107 definition "rbl_succ2 b xs = (if b then rbl_succ xs else xs)" |
|
108 |
|
109 lemma rbl_succ2_simps: |
|
110 "rbl_succ2 b [] = []" |
|
111 "rbl_succ2 b (x # xs) = (b \<noteq> x) # rbl_succ2 (x \<and> b) xs" |
|
112 by (simp_all add: rbl_succ2_def) |
|
113 |
|
114 lemma twos_complement: "- x = word_succ (NOT x)" |
|
115 using arg_cong[OF word_add_not[where x=x], where f="\<lambda>a. a - x + 1"] |
|
116 by (simp add: word_succ_p1 word_sp_01[unfolded word_succ_p1] del: word_add_not) |
|
117 |
|
118 lemma rbl_word_neg: "rev (to_bl (- x)) = rbl_succ2 True (map Not (rev (to_bl x)))" |
|
119 by (simp add: twos_complement word_succ_rbl[OF refl] bl_word_not rev_map rbl_succ2_def) |
|
120 |
|
121 lemma rbl_word_cat: |
|
122 "rev (to_bl (word_cat x y :: 'a::len0 word)) = |
|
123 takefill False (len_of TYPE('a)) (rev (to_bl y) @ rev (to_bl x))" |
|
124 by (simp add: word_cat_bl word_rev_tf) |
|
125 |
|
126 lemma rbl_word_slice: |
|
127 "rev (to_bl (slice n w :: 'a::len0 word)) = |
|
128 takefill False (len_of TYPE('a)) (drop n (rev (to_bl w)))" |
|
129 apply (simp add: slice_take word_rev_tf rev_take) |
|
130 apply (cases "n < len_of TYPE('b)", simp_all) |
|
131 done |
|
132 |
|
133 lemma rbl_word_ucast: |
|
134 "rev (to_bl (ucast x :: 'a::len0 word)) = takefill False (len_of TYPE('a)) (rev (to_bl x))" |
|
135 apply (simp add: to_bl_ucast takefill_alt) |
|
136 apply (simp add: rev_drop) |
|
137 apply (cases "len_of TYPE('a) < len_of TYPE('b)") |
|
138 apply simp_all |
|
139 done |
|
140 |
|
141 lemma rbl_shiftl: |
|
142 "rev (to_bl (w << n)) = takefill False (size w) (replicate n False @ rev (to_bl w))" |
|
143 by (simp add: bl_shiftl takefill_alt word_size rev_drop) |
|
144 |
|
145 lemma rbl_shiftr: |
|
146 "rev (to_bl (w >> n)) = takefill False (size w) (drop n (rev (to_bl w)))" |
|
147 by (simp add: shiftr_slice rbl_word_slice word_size) |
|
148 |
|
149 definition "drop_nonempty v n xs = (if n < length xs then drop n xs else [last (v # xs)])" |
|
150 |
|
151 lemma drop_nonempty_simps: |
|
152 "drop_nonempty v (Suc n) (x # xs) = drop_nonempty x n xs" |
|
153 "drop_nonempty v 0 (x # xs) = (x # xs)" |
|
154 "drop_nonempty v n [] = [v]" |
|
155 by (simp_all add: drop_nonempty_def) |
|
156 |
|
157 definition "takefill_last x n xs = takefill (last (x # xs)) n xs" |
|
158 |
|
159 lemma takefill_last_simps: |
|
160 "takefill_last z (Suc n) (x # xs) = x # takefill_last x n xs" |
|
161 "takefill_last z 0 xs = []" |
|
162 "takefill_last z n [] = replicate n z" |
|
163 by (simp_all add: takefill_last_def) (simp_all add: takefill_alt) |
|
164 |
|
165 lemma rbl_sshiftr: |
|
166 "rev (to_bl (w >>> n)) = takefill_last False (size w) (drop_nonempty False n (rev (to_bl w)))" |
|
167 apply (cases "n < size w") |
|
168 apply (simp add: bl_sshiftr takefill_last_def word_size |
|
169 takefill_alt rev_take last_rev |
|
170 drop_nonempty_def) |
|
171 apply (subgoal_tac "(w >>> n) = of_bl (replicate (size w) (msb w))") |
|
172 apply (simp add: word_size takefill_last_def takefill_alt |
|
173 last_rev word_msb_alt word_rev_tf |
|
174 drop_nonempty_def take_Cons') |
|
175 apply (case_tac "len_of TYPE('a)", simp_all) |
|
176 apply (rule word_eqI) |
|
177 apply (simp add: nth_sshiftr word_size test_bit_of_bl |
|
178 msb_nth) |
|
179 done |
|
180 |
|
181 lemma nth_word_of_int: |
|
182 "(word_of_int x :: 'a::len0 word) !! n = (n < len_of TYPE('a) \<and> bin_nth x n)" |
|
183 apply (simp add: test_bit_bl word_size to_bl_of_bin) |
|
184 apply (subst conj_cong[OF refl], erule bin_nth_bl) |
|
185 apply auto |
|
186 done |
|
187 |
|
188 lemma nth_scast: |
|
189 "(scast (x :: 'a::len word) :: 'b::len word) !! n = |
|
190 (n < len_of TYPE('b) \<and> |
|
191 (if n < len_of TYPE('a) - 1 then x !! n |
|
192 else x !! (len_of TYPE('a) - 1)))" |
|
193 by (simp add: scast_def nth_sint) |
|
194 |
|
195 lemma rbl_word_scast: |
|
196 "rev (to_bl (scast x :: 'a::len word)) = takefill_last False (len_of TYPE('a)) (rev (to_bl x))" |
|
197 apply (rule nth_equalityI) |
|
198 apply (simp add: word_size takefill_last_def) |
|
199 apply (clarsimp simp: nth_scast takefill_last_def |
|
200 nth_takefill word_size nth_rev to_bl_nth) |
|
201 apply (cases "len_of TYPE('b)") |
|
202 apply simp |
|
203 apply (clarsimp simp: less_Suc_eq_le linorder_not_less |
|
204 last_rev word_msb_alt[symmetric] |
|
205 msb_nth) |
|
206 done |
|
207 |
|
208 definition rbl_mul :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list" |
|
209 where "rbl_mul xs ys = foldr (\<lambda>x sm. rbl_plus False (map ((\<and>) x) ys) (False # sm)) xs []" |
|
210 |
|
211 lemma rbl_mul_simps: |
|
212 "rbl_mul (x # xs) ys = rbl_plus False (map ((\<and>) x) ys) (False # rbl_mul xs ys)" |
|
213 "rbl_mul [] ys = []" |
|
214 by (simp_all add: rbl_mul_def) |
|
215 |
|
216 lemma takefill_le2: "length xs \<le> n \<Longrightarrow> takefill x m (takefill x n xs) = takefill x m xs" |
|
217 by (simp add: takefill_alt replicate_add[symmetric]) |
|
218 |
|
219 lemma take_rbl_plus: "\<forall>n b. take n (rbl_plus b xs ys) = rbl_plus b (take n xs) (take n ys)" |
|
220 apply (simp add: rbl_plus_def take_zip[symmetric]) |
|
221 apply (rule_tac list="zip xs ys" in list.induct) |
|
222 apply simp |
|
223 apply (clarsimp simp: split_def) |
|
224 apply (case_tac n, simp_all) |
|
225 done |
|
226 |
|
227 lemma word_rbl_mul_induct: |
|
228 "length xs \<le> size y \<Longrightarrow> |
|
229 rbl_mul xs (rev (to_bl y)) = take (length xs) (rev (to_bl (of_bl (rev xs) * y)))" |
|
230 for y :: "'a::len word" |
|
231 proof (induct xs) |
|
232 case Nil |
|
233 show ?case by (simp add: rbl_mul_simps) |
|
234 next |
|
235 case (Cons z zs) |
|
236 |
|
237 have rbl_word_plus': "to_bl (x + y) = rev (rbl_plus False (rev (to_bl x)) (rev (to_bl y)))" |
|
238 for x y :: "'a word" |
|
239 by (simp add: rbl_word_plus[symmetric]) |
|
240 |
|
241 have mult_bit: "to_bl (of_bl [z] * y) = map ((\<and>) z) (to_bl y)" |
|
242 by (cases z) (simp cong: map_cong, simp add: map_replicate_const cong: map_cong) |
|
243 |
|
244 have shiftl: "of_bl xs * 2 * y = (of_bl xs * y) << 1" for xs |
|
245 by (simp add: shiftl_t2n) |
|
246 |
|
247 have zip_take_triv: "\<And>xs ys n. n = length ys \<Longrightarrow> zip (take n xs) ys = zip xs ys" |
|
248 by (rule nth_equalityI) simp_all |
|
249 |
|
250 from Cons show ?case |
|
251 apply (simp add: trans [OF of_bl_append add.commute] |
|
252 rbl_mul_simps rbl_word_plus' distrib_right mult_bit shiftl rbl_shiftl) |
|
253 apply (simp add: takefill_alt word_size rev_map take_rbl_plus min_def) |
|
254 apply (simp add: rbl_plus_def zip_take_triv) |
|
255 done |
|
256 qed |
|
257 |
|
258 lemma rbl_word_mul: "rev (to_bl (x * y)) = rbl_mul (rev (to_bl x)) (rev (to_bl y))" |
|
259 for x :: "'a::len word" |
|
260 using word_rbl_mul_induct[where xs="rev (to_bl x)" and y=y] by (simp add: word_size) |
|
261 |
|
262 text \<open>Breaking up inequalities into bitlist properties.\<close> |
|
263 |
|
264 definition |
|
265 "rev_bl_order F xs ys = |
|
266 (length xs = length ys \<and> |
|
267 ((xs = ys \<and> F) |
|
268 \<or> (\<exists>n < length xs. drop (Suc n) xs = drop (Suc n) ys |
|
269 \<and> \<not> xs ! n \<and> ys ! n)))" |
|
270 |
|
271 lemma rev_bl_order_simps: |
|
272 "rev_bl_order F [] [] = F" |
|
273 "rev_bl_order F (x # xs) (y # ys) = rev_bl_order ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> F)) xs ys" |
|
274 apply (simp_all add: rev_bl_order_def) |
|
275 apply (rule conj_cong[OF refl]) |
|
276 apply (cases "xs = ys") |
|
277 apply (simp add: nth_Cons') |
|
278 apply blast |
|
279 apply (simp add: nth_Cons') |
|
280 apply safe |
|
281 apply (rule_tac x="n - 1" in exI) |
|
282 apply simp |
|
283 apply (rule_tac x="Suc n" in exI) |
|
284 apply simp |
|
285 done |
|
286 |
|
287 lemma rev_bl_order_rev_simp: |
|
288 "length xs = length ys \<Longrightarrow> |
|
289 rev_bl_order F (xs @ [x]) (ys @ [y]) = ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> rev_bl_order F xs ys))" |
|
290 by (induct arbitrary: F rule: list_induct2) (auto simp: rev_bl_order_simps) |
|
291 |
|
292 lemma rev_bl_order_bl_to_bin: |
|
293 "length xs = length ys \<Longrightarrow> |
|
294 rev_bl_order True xs ys = (bl_to_bin (rev xs) \<le> bl_to_bin (rev ys)) \<and> |
|
295 rev_bl_order False xs ys = (bl_to_bin (rev xs) < bl_to_bin (rev ys))" |
|
296 apply (induct xs ys rule: list_induct2) |
|
297 apply (simp_all add: rev_bl_order_simps bl_to_bin_app_cat) |
|
298 apply (auto simp add: bl_to_bin_def Bit_B0 Bit_B1 add1_zle_eq Bit_def) |
|
299 done |
|
300 |
|
301 lemma word_le_rbl: "x \<le> y \<longleftrightarrow> rev_bl_order True (rev (to_bl x)) (rev (to_bl y))" |
|
302 for x y :: "'a::len0 word" |
|
303 by (simp add: rev_bl_order_bl_to_bin word_le_def) |
|
304 |
|
305 lemma word_less_rbl: "x < y \<longleftrightarrow> rev_bl_order False (rev (to_bl x)) (rev (to_bl y))" |
|
306 for x y :: "'a::len0 word" |
|
307 by (simp add: word_less_alt rev_bl_order_bl_to_bin) |
|
308 |
|
309 lemma word_sint_msb_eq: "sint x = uint x - (if msb x then 2 ^ size x else 0)" |
|
310 apply (cases "msb x") |
|
311 apply (rule word_sint.Abs_eqD[where 'a='a], simp_all) |
|
312 apply (simp add: word_size wi_hom_syms word_of_int_2p_len) |
|
313 apply (simp add: sints_num word_size) |
|
314 apply (rule conjI) |
|
315 apply (simp add: le_diff_eq') |
|
316 apply (rule order_trans[where y="2 ^ (len_of TYPE('a) - 1)"]) |
|
317 apply (simp add: power_Suc[symmetric]) |
|
318 apply (simp add: linorder_not_less[symmetric] mask_eq_iff[symmetric]) |
|
319 apply (rule notI, drule word_eqD[where x="size x - 1"]) |
|
320 apply (simp add: msb_nth word_ops_nth_size word_size) |
|
321 apply (simp add: order_less_le_trans[where y=0]) |
|
322 apply (rule word_uint.Abs_eqD[where 'a='a], simp_all) |
|
323 apply (simp add: linorder_not_less uints_num word_msb_sint) |
|
324 apply (rule order_less_le_trans[OF sint_lt]) |
|
325 apply simp |
|
326 done |
|
327 |
|
328 lemma word_sle_msb_le: "x <=s y \<longleftrightarrow> (msb y \<longrightarrow> msb x) \<and> ((msb x \<and> \<not> msb y) \<or> x \<le> y)" |
|
329 apply (simp add: word_sle_def word_sint_msb_eq word_size word_le_def) |
|
330 apply safe |
|
331 apply (rule order_trans[OF _ uint_ge_0]) |
|
332 apply (simp add: order_less_imp_le) |
|
333 apply (erule notE[OF leD]) |
|
334 apply (rule order_less_le_trans[OF _ uint_ge_0]) |
|
335 apply simp |
|
336 done |
|
337 |
|
338 lemma word_sless_msb_less: "x <s y \<longleftrightarrow> (msb y \<longrightarrow> msb x) \<and> ((msb x \<and> \<not> msb y) \<or> x < y)" |
|
339 by (auto simp add: word_sless_def word_sle_msb_le) |
|
340 |
|
341 definition "map_last f xs = (if xs = [] then [] else butlast xs @ [f (last xs)])" |
|
342 |
|
343 lemma map_last_simps: |
|
344 "map_last f [] = []" |
|
345 "map_last f [x] = [f x]" |
|
346 "map_last f (x # y # zs) = x # map_last f (y # zs)" |
|
347 by (simp_all add: map_last_def) |
|
348 |
|
349 lemma word_sle_rbl: |
|
350 "x <=s y \<longleftrightarrow> rev_bl_order True (map_last Not (rev (to_bl x))) (map_last Not (rev (to_bl y)))" |
|
351 using word_msb_alt[where w=x] word_msb_alt[where w=y] |
|
352 apply (simp add: word_sle_msb_le word_le_rbl) |
|
353 apply (subgoal_tac "length (to_bl x) = length (to_bl y)") |
|
354 apply (cases "to_bl x", simp) |
|
355 apply (cases "to_bl y", simp) |
|
356 apply (clarsimp simp: map_last_def rev_bl_order_rev_simp) |
|
357 apply auto |
|
358 done |
|
359 |
|
360 lemma word_sless_rbl: |
|
361 "x <s y \<longleftrightarrow> rev_bl_order False (map_last Not (rev (to_bl x))) (map_last Not (rev (to_bl y)))" |
|
362 using word_msb_alt[where w=x] word_msb_alt[where w=y] |
|
363 apply (simp add: word_sless_msb_less word_less_rbl) |
|
364 apply (subgoal_tac "length (to_bl x) = length (to_bl y)") |
|
365 apply (cases "to_bl x", simp) |
|
366 apply (cases "to_bl y", simp) |
|
367 apply (clarsimp simp: map_last_def rev_bl_order_rev_simp) |
|
368 apply auto |
|
369 done |
|
370 |
|
371 text \<open>Lemmas for unpacking \<^term>\<open>rev (to_bl n)\<close> for numerals n and also |
|
372 for irreducible values and expressions.\<close> |
|
373 |
|
374 lemma rev_bin_to_bl_simps: |
|
375 "rev (bin_to_bl 0 x) = []" |
|
376 "rev (bin_to_bl (Suc n) (numeral (num.Bit0 nm))) = False # rev (bin_to_bl n (numeral nm))" |
|
377 "rev (bin_to_bl (Suc n) (numeral (num.Bit1 nm))) = True # rev (bin_to_bl n (numeral nm))" |
|
378 "rev (bin_to_bl (Suc n) (numeral (num.One))) = True # replicate n False" |
|
379 "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm))) = False # rev (bin_to_bl n (- numeral nm))" |
|
380 "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm))) = |
|
381 True # rev (bin_to_bl n (- numeral (nm + num.One)))" |
|
382 "rev (bin_to_bl (Suc n) (- numeral (num.One))) = True # replicate n True" |
|
383 "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm + num.One))) = |
|
384 True # rev (bin_to_bl n (- numeral (nm + num.One)))" |
|
385 "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm + num.One))) = |
|
386 False # rev (bin_to_bl n (- numeral (nm + num.One)))" |
|
387 "rev (bin_to_bl (Suc n) (- numeral (num.One + num.One))) = |
|
388 False # rev (bin_to_bl n (- numeral num.One))" |
|
389 apply simp_all |
|
390 apply (simp_all only: bin_to_bl_aux_alt) |
|
391 apply (simp_all) |
|
392 apply (simp_all add: bin_to_bl_zero_aux bin_to_bl_minus1_aux) |
|
393 done |
|
394 |
|
395 lemma to_bl_upt: "to_bl x = rev (map ((!!) x) [0 ..< size x])" |
|
396 apply (rule nth_equalityI) |
|
397 apply (simp add: word_size) |
|
398 apply (auto simp: to_bl_nth word_size nth_rev) |
|
399 done |
|
400 |
|
401 lemma rev_to_bl_upt: "rev (to_bl x) = map ((!!) x) [0 ..< size x]" |
|
402 by (simp add: to_bl_upt) |
|
403 |
|
404 lemma upt_eq_list_intros: |
|
405 "j \<le> i \<Longrightarrow> [i ..< j] = []" |
|
406 "i = x \<Longrightarrow> x < j \<Longrightarrow> [x + 1 ..< j] = xs \<Longrightarrow> [i ..< j] = (x # xs)" |
|
407 by (simp_all add: upt_eq_Cons_conv) |
|
408 |
|
409 |
|
410 subsection \<open>Tactic definition\<close> |
|
411 |
|
412 ML \<open> |
|
413 structure Word_Bitwise_Tac = |
|
414 struct |
|
415 |
|
416 val word_ss = simpset_of \<^theory_context>\<open>Word\<close>; |
|
417 |
|
418 fun mk_nat_clist ns = |
|
419 fold_rev (Thm.mk_binop \<^cterm>\<open>Cons :: nat \<Rightarrow> _\<close>) |
|
420 ns \<^cterm>\<open>[] :: nat list\<close>; |
|
421 |
|
422 fun upt_conv ctxt ct = |
|
423 case Thm.term_of ct of |
|
424 (\<^const>\<open>upt\<close> $ n $ m) => |
|
425 let |
|
426 val (i, j) = apply2 (snd o HOLogic.dest_number) (n, m); |
|
427 val ns = map (Numeral.mk_cnumber \<^ctyp>\<open>nat\<close>) (i upto (j - 1)) |
|
428 |> mk_nat_clist; |
|
429 val prop = |
|
430 Thm.mk_binop \<^cterm>\<open>(=) :: nat list \<Rightarrow> _\<close> ct ns |
|
431 |> Thm.apply \<^cterm>\<open>Trueprop\<close>; |
|
432 in |
|
433 try (fn () => |
|
434 Goal.prove_internal ctxt [] prop |
|
435 (K (REPEAT_DETERM (resolve_tac ctxt @{thms upt_eq_list_intros} 1 |
|
436 ORELSE simp_tac (put_simpset word_ss ctxt) 1))) |> mk_meta_eq) () |
|
437 end |
|
438 | _ => NONE; |
|
439 |
|
440 val expand_upt_simproc = |
|
441 Simplifier.make_simproc \<^context> "expand_upt" |
|
442 {lhss = [\<^term>\<open>upt x y\<close>], proc = K upt_conv}; |
|
443 |
|
444 fun word_len_simproc_fn ctxt ct = |
|
445 (case Thm.term_of ct of |
|
446 Const (\<^const_name>\<open>len_of\<close>, _) $ t => |
|
447 (let |
|
448 val T = fastype_of t |> dest_Type |> snd |> the_single |
|
449 val n = Numeral.mk_cnumber \<^ctyp>\<open>nat\<close> (Word_Lib.dest_binT T); |
|
450 val prop = |
|
451 Thm.mk_binop \<^cterm>\<open>(=) :: nat \<Rightarrow> _\<close> ct n |
|
452 |> Thm.apply \<^cterm>\<open>Trueprop\<close>; |
|
453 in |
|
454 Goal.prove_internal ctxt [] prop (K (simp_tac (put_simpset word_ss ctxt) 1)) |
|
455 |> mk_meta_eq |> SOME |
|
456 end handle TERM _ => NONE | TYPE _ => NONE) |
|
457 | _ => NONE); |
|
458 |
|
459 val word_len_simproc = |
|
460 Simplifier.make_simproc \<^context> "word_len" |
|
461 {lhss = [\<^term>\<open>len_of x\<close>], proc = K word_len_simproc_fn}; |
|
462 |
|
463 (* convert 5 or nat 5 to Suc 4 when n_sucs = 1, Suc (Suc 4) when n_sucs = 2, |
|
464 or just 5 (discarding nat) when n_sucs = 0 *) |
|
465 |
|
466 fun nat_get_Suc_simproc_fn n_sucs ctxt ct = |
|
467 let |
|
468 val (f $ arg) = Thm.term_of ct; |
|
469 val n = |
|
470 (case arg of \<^term>\<open>nat\<close> $ n => n | n => n) |
|
471 |> HOLogic.dest_number |> snd; |
|
472 val (i, j) = if n > n_sucs then (n_sucs, n - n_sucs) else (n, 0); |
|
473 val arg' = funpow i HOLogic.mk_Suc (HOLogic.mk_number \<^typ>\<open>nat\<close> j); |
|
474 val _ = if arg = arg' then raise TERM ("", []) else (); |
|
475 fun propfn g = |
|
476 HOLogic.mk_eq (g arg, g arg') |
|
477 |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt; |
|
478 val eq1 = |
|
479 Goal.prove_internal ctxt [] (propfn I) |
|
480 (K (simp_tac (put_simpset word_ss ctxt) 1)); |
|
481 in |
|
482 Goal.prove_internal ctxt [] (propfn (curry (op $) f)) |
|
483 (K (simp_tac (put_simpset HOL_ss ctxt addsimps [eq1]) 1)) |
|
484 |> mk_meta_eq |> SOME |
|
485 end handle TERM _ => NONE; |
|
486 |
|
487 fun nat_get_Suc_simproc n_sucs ts = |
|
488 Simplifier.make_simproc \<^context> "nat_get_Suc" |
|
489 {lhss = map (fn t => t $ \<^term>\<open>n :: nat\<close>) ts, |
|
490 proc = K (nat_get_Suc_simproc_fn n_sucs)}; |
|
491 |
|
492 val no_split_ss = |
|
493 simpset_of (put_simpset HOL_ss \<^context> |
|
494 |> Splitter.del_split @{thm if_split}); |
|
495 |
|
496 val expand_word_eq_sss = |
|
497 (simpset_of (put_simpset HOL_basic_ss \<^context> addsimps |
|
498 @{thms word_eq_rbl_eq word_le_rbl word_less_rbl word_sle_rbl word_sless_rbl}), |
|
499 map simpset_of [ |
|
500 put_simpset no_split_ss \<^context> addsimps |
|
501 @{thms rbl_word_plus rbl_word_and rbl_word_or rbl_word_not |
|
502 rbl_word_neg bl_word_sub rbl_word_xor |
|
503 rbl_word_cat rbl_word_slice rbl_word_scast |
|
504 rbl_word_ucast rbl_shiftl rbl_shiftr rbl_sshiftr |
|
505 rbl_word_if}, |
|
506 put_simpset no_split_ss \<^context> addsimps |
|
507 @{thms to_bl_numeral to_bl_neg_numeral to_bl_0 rbl_word_1}, |
|
508 put_simpset no_split_ss \<^context> addsimps |
|
509 @{thms rev_rev_ident rev_replicate rev_map to_bl_upt word_size} |
|
510 addsimprocs [word_len_simproc], |
|
511 put_simpset no_split_ss \<^context> addsimps |
|
512 @{thms list.simps split_conv replicate.simps list.map |
|
513 zip_Cons_Cons zip_Nil drop_Suc_Cons drop_0 drop_Nil |
|
514 foldr.simps map2_Cons map2_Nil takefill_Suc_Cons |
|
515 takefill_Suc_Nil takefill.Z rbl_succ2_simps |
|
516 rbl_plus_simps rev_bin_to_bl_simps append.simps |
|
517 takefill_last_simps drop_nonempty_simps |
|
518 rev_bl_order_simps} |
|
519 addsimprocs [expand_upt_simproc, |
|
520 nat_get_Suc_simproc 4 |
|
521 [\<^term>\<open>replicate\<close>, \<^term>\<open>takefill x\<close>, |
|
522 \<^term>\<open>drop\<close>, \<^term>\<open>bin_to_bl\<close>, |
|
523 \<^term>\<open>takefill_last x\<close>, |
|
524 \<^term>\<open>drop_nonempty x\<close>]], |
|
525 put_simpset no_split_ss \<^context> addsimps @{thms xor3_simps carry_simps if_bool_simps} |
|
526 ]) |
|
527 |
|
528 fun tac ctxt = |
|
529 let |
|
530 val (ss, sss) = expand_word_eq_sss; |
|
531 in |
|
532 foldr1 (op THEN_ALL_NEW) |
|
533 ((CHANGED o safe_full_simp_tac (put_simpset ss ctxt)) :: |
|
534 map (fn ss => safe_full_simp_tac (put_simpset ss ctxt)) sss) |
|
535 end; |
|
536 |
|
537 end |
|
538 \<close> |
|
539 |
|
540 method_setup word_bitwise = |
|
541 \<open>Scan.succeed (fn ctxt => Method.SIMPLE_METHOD (Word_Bitwise_Tac.tac ctxt 1))\<close> |
|
542 "decomposer for word equalities and inequalities into bit propositions" |
|
543 |
|
544 end |