author | huffman |
Wed, 22 Aug 2007 21:09:21 +0200 | |
changeset 24408 | 058c5613a86f |
parent 24397 | eaf37b780683 |
child 24415 | 640b85390ba0 |
permissions | -rw-r--r-- |
24333 | 1 |
(* |
2 |
ID: $Id$ |
|
3 |
Author: Jeremy Dawson and Gerwin Klein, NICTA |
|
4 |
||
5 |
contains arithmetic theorems for word, instantiations to |
|
6 |
arithmetic type classes and tactics for reducing word arithmetic |
|
7 |
to linear arithmetic on int or nat |
|
8 |
*) |
|
9 |
||
24350 | 10 |
header {* Word Arithmetic *} |
11 |
||
24333 | 12 |
theory WordArith imports WordDefinition begin |
13 |
||
14 |
lemmas word_arith_wis [THEN meta_eq_to_obj_eq] = |
|
15 |
word_add_def word_mult_def word_minus_def |
|
16 |
word_succ_def word_pred_def word_0_wi word_1_wi |
|
17 |
||
18 |
(* following two are available in class number_ring, |
|
19 |
but convenient to have them here here; |
|
20 |
note - the number_ring versions, numeral_0_eq_0 and numeral_1_eq_1 |
|
21 |
are in the default simpset, so to use the automatic simplifications for |
|
22 |
(eg) sint (number_of bin) on sint 1, must do |
|
23 |
(simp add: word_1_no del: numeral_1_eq_1) |
|
24 |
*) |
|
25 |
lemmas word_0_wi_Pls = word_0_wi [folded Pls_def] |
|
26 |
lemmas word_0_no = word_0_wi_Pls [folded word_no_wi] |
|
27 |
||
28 |
lemma int_one_bin: "(1 :: int) == (Numeral.Pls BIT bit.B1)" |
|
29 |
unfolding Pls_def Bit_def by auto |
|
30 |
||
31 |
lemma word_1_no: |
|
24408 | 32 |
"(1 :: 'a word) == number_of (Numeral.Pls BIT bit.B1)" |
24333 | 33 |
unfolding word_1_wi word_number_of_def int_one_bin by auto |
34 |
||
35 |
lemma word_m1_wi: "-1 == word_of_int -1" |
|
36 |
by (rule word_number_of_alt) |
|
37 |
||
38 |
lemma word_m1_wi_Min: "-1 = word_of_int Numeral.Min" |
|
39 |
by (simp add: word_m1_wi number_of_eq) |
|
40 |
||
41 |
lemma uint_0 [simp] : "(uint 0 = 0)" |
|
42 |
unfolding word_0_wi |
|
43 |
by (simp add: word_ubin.eq_norm Pls_def [symmetric]) |
|
44 |
||
45 |
lemma uint_0_iff: "(uint x = 0) = (x = 0)" |
|
46 |
by (auto intro!: word_uint.Rep_eqD) |
|
47 |
||
48 |
lemma unat_0_iff: "(unat x = 0) = (x = 0)" |
|
49 |
unfolding unat_def by (auto simp add : nat_eq_iff uint_0_iff) |
|
50 |
||
51 |
lemma unat_0 [simp]: "unat 0 = 0" |
|
52 |
unfolding unat_def by auto |
|
53 |
||
24408 | 54 |
lemma size_0_same': "size w = 0 ==> w = (v :: 'a word)" |
24333 | 55 |
apply (unfold word_size) |
56 |
apply (rule box_equals) |
|
57 |
defer |
|
58 |
apply (rule word_uint.Rep_inverse)+ |
|
59 |
apply (rule word_ubin.norm_eq_iff [THEN iffD1]) |
|
60 |
apply simp |
|
61 |
done |
|
62 |
||
63 |
lemmas size_0_same = size_0_same' [folded word_size] |
|
64 |
||
65 |
lemmas unat_eq_0 = unat_0_iff |
|
66 |
lemmas unat_eq_zero = unat_0_iff |
|
67 |
||
68 |
lemma unat_gt_0: "(0 < unat x) = (x ~= 0)" |
|
69 |
by (simp add : unat_0_iff [symmetric]) |
|
70 |
||
71 |
lemma ucast_0 [simp] : "ucast 0 = 0" |
|
72 |
unfolding ucast_def |
|
73 |
by simp (simp add: word_0_wi) |
|
74 |
||
75 |
lemma sint_0 [simp] : "sint 0 = 0" |
|
76 |
unfolding sint_uint |
|
77 |
by (simp add: Pls_def [symmetric]) |
|
78 |
||
79 |
lemma scast_0 [simp] : "scast 0 = 0" |
|
80 |
apply (unfold scast_def) |
|
81 |
apply simp |
|
82 |
apply (simp add: word_0_wi) |
|
83 |
done |
|
84 |
||
85 |
lemma sint_n1 [simp] : "sint -1 = -1" |
|
86 |
apply (unfold word_m1_wi_Min) |
|
87 |
apply (simp add: word_sbin.eq_norm) |
|
88 |
apply (unfold Min_def number_of_eq) |
|
89 |
apply simp |
|
90 |
done |
|
91 |
||
92 |
lemma scast_n1 [simp] : "scast -1 = -1" |
|
93 |
apply (unfold scast_def sint_n1) |
|
94 |
apply (unfold word_number_of_alt) |
|
95 |
apply (rule refl) |
|
96 |
done |
|
97 |
||
24408 | 98 |
lemma uint_1 [simp] : "uint (1 :: 'a :: finite word) = 1" |
24333 | 99 |
unfolding word_1_wi |
100 |
by (simp add: word_ubin.eq_norm int_one_bin bintrunc_minus_simps) |
|
101 |
||
24408 | 102 |
lemma unat_1 [simp] : "unat (1 :: 'a :: finite word) = 1" |
24333 | 103 |
by (unfold unat_def uint_1) auto |
104 |
||
24408 | 105 |
lemma ucast_1 [simp] : "ucast (1 :: 'a :: finite word) = 1" |
24333 | 106 |
unfolding ucast_def word_1_wi |
107 |
by (simp add: word_ubin.eq_norm int_one_bin bintrunc_minus_simps) |
|
108 |
||
109 |
(* abstraction preserves the operations |
|
110 |
(the definitions tell this for bins in range uint) *) |
|
111 |
||
112 |
lemmas arths = |
|
113 |
bintr_ariths [THEN word_ubin.norm_eq_iff [THEN iffD1], |
|
114 |
folded word_ubin.eq_norm, standard] |
|
115 |
||
116 |
lemma wi_homs: |
|
117 |
shows |
|
118 |
wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)" and |
|
119 |
wi_hom_mult: "word_of_int a * word_of_int b = word_of_int (a * b)" and |
|
120 |
wi_hom_neg: "- word_of_int a = word_of_int (- a)" and |
|
121 |
wi_hom_succ: "word_succ (word_of_int a) = word_of_int (Numeral.succ a)" and |
|
122 |
wi_hom_pred: "word_pred (word_of_int a) = word_of_int (Numeral.pred a)" |
|
123 |
by (auto simp: word_arith_wis arths) |
|
124 |
||
125 |
lemmas wi_hom_syms = wi_homs [symmetric] |
|
126 |
||
24408 | 127 |
lemma word_sub_def: "a - b == a + - (b :: 'a word)" |
24333 | 128 |
unfolding word_sub_wi diff_def |
129 |
by (simp only : word_uint.Rep_inverse wi_hom_syms) |
|
130 |
||
131 |
lemmas word_diff_minus = word_sub_def [THEN meta_eq_to_obj_eq, standard] |
|
132 |
||
133 |
lemma word_of_int_sub_hom: |
|
134 |
"(word_of_int a) - word_of_int b = word_of_int (a - b)" |
|
135 |
unfolding word_sub_def diff_def by (simp only : wi_homs) |
|
136 |
||
137 |
lemmas new_word_of_int_homs = |
|
138 |
word_of_int_sub_hom wi_homs word_0_wi word_1_wi |
|
139 |
||
140 |
lemmas new_word_of_int_hom_syms = new_word_of_int_homs [symmetric, standard] |
|
141 |
||
142 |
lemmas word_of_int_hom_syms = |
|
143 |
new_word_of_int_hom_syms [unfolded succ_def pred_def] |
|
144 |
||
145 |
lemmas word_of_int_homs = |
|
146 |
new_word_of_int_homs [unfolded succ_def pred_def] |
|
147 |
||
148 |
lemmas word_of_int_add_hom = word_of_int_homs (2) |
|
149 |
lemmas word_of_int_mult_hom = word_of_int_homs (3) |
|
150 |
lemmas word_of_int_minus_hom = word_of_int_homs (4) |
|
151 |
lemmas word_of_int_succ_hom = word_of_int_homs (5) |
|
152 |
lemmas word_of_int_pred_hom = word_of_int_homs (6) |
|
153 |
lemmas word_of_int_0_hom = word_of_int_homs (7) |
|
154 |
lemmas word_of_int_1_hom = word_of_int_homs (8) |
|
155 |
||
156 |
(* now, to get the weaker results analogous to word_div/mod_def *) |
|
157 |
||
158 |
lemmas word_arith_alts = |
|
159 |
word_sub_wi [unfolded succ_def pred_def, THEN meta_eq_to_obj_eq, standard] |
|
160 |
word_arith_wis [unfolded succ_def pred_def, standard] |
|
161 |
||
162 |
lemmas word_sub_alt = word_arith_alts (1) |
|
163 |
lemmas word_add_alt = word_arith_alts (2) |
|
164 |
lemmas word_mult_alt = word_arith_alts (3) |
|
165 |
lemmas word_minus_alt = word_arith_alts (4) |
|
166 |
lemmas word_succ_alt = word_arith_alts (5) |
|
167 |
lemmas word_pred_alt = word_arith_alts (6) |
|
168 |
lemmas word_0_alt = word_arith_alts (7) |
|
169 |
lemmas word_1_alt = word_arith_alts (8) |
|
170 |
||
24350 | 171 |
subsection "Transferring goals from words to ints" |
24333 | 172 |
|
173 |
lemma word_ths: |
|
174 |
shows |
|
175 |
word_succ_p1: "word_succ a = a + 1" and |
|
176 |
word_pred_m1: "word_pred a = a - 1" and |
|
177 |
word_pred_succ: "word_pred (word_succ a) = a" and |
|
178 |
word_succ_pred: "word_succ (word_pred a) = a" and |
|
179 |
word_mult_succ: "word_succ a * b = b + a * b" |
|
180 |
by (rule word_uint.Abs_cases [of b], |
|
181 |
rule word_uint.Abs_cases [of a], |
|
182 |
simp add: pred_def succ_def add_commute mult_commute |
|
183 |
ring_distribs new_word_of_int_homs)+ |
|
184 |
||
185 |
lemmas uint_cong = arg_cong [where f = uint] |
|
186 |
||
187 |
lemmas uint_word_ariths = |
|
188 |
word_arith_alts [THEN trans [OF uint_cong int_word_uint], standard] |
|
189 |
||
190 |
lemmas uint_word_arith_bintrs = uint_word_ariths [folded bintrunc_mod2p] |
|
191 |
||
192 |
(* similar expressions for sint (arith operations) *) |
|
193 |
lemmas sint_word_ariths = uint_word_arith_bintrs |
|
194 |
[THEN uint_sint [symmetric, THEN trans], |
|
195 |
unfolded uint_sint bintr_arith1s bintr_ariths |
|
24408 | 196 |
zero_less_card_finite [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep, standard] |
24333 | 197 |
|
198 |
lemma word_pred_0_n1: "word_pred 0 = word_of_int -1" |
|
199 |
unfolding word_pred_def number_of_eq |
|
200 |
by (simp add : pred_def word_no_wi) |
|
201 |
||
202 |
lemma word_pred_0_Min: "word_pred 0 = word_of_int Numeral.Min" |
|
203 |
by (simp add: word_pred_0_n1 number_of_eq) |
|
204 |
||
205 |
lemma word_m1_Min: "- 1 = word_of_int Numeral.Min" |
|
206 |
unfolding Min_def by (simp only: word_of_int_hom_syms) |
|
207 |
||
208 |
lemma succ_pred_no [simp]: |
|
209 |
"word_succ (number_of bin) = number_of (Numeral.succ bin) & |
|
210 |
word_pred (number_of bin) = number_of (Numeral.pred bin)" |
|
211 |
unfolding word_number_of_def by (simp add : new_word_of_int_homs) |
|
212 |
||
213 |
lemma word_sp_01 [simp] : |
|
214 |
"word_succ -1 = 0 & word_succ 0 = 1 & word_pred 0 = -1 & word_pred 1 = 0" |
|
215 |
by (unfold word_0_no word_1_no) auto |
|
216 |
||
217 |
(* alternative approach to lifting arithmetic equalities *) |
|
218 |
lemma word_of_int_Ex: |
|
219 |
"\<exists>y. x = word_of_int y" |
|
220 |
by (rule_tac x="uint x" in exI) simp |
|
221 |
||
222 |
lemma word_arith_eqs: |
|
24408 | 223 |
fixes a :: "'a word" |
224 |
fixes b :: "'a word" |
|
24333 | 225 |
shows |
226 |
word_add_0: "0 + a = a" and |
|
227 |
word_add_0_right: "a + 0 = a" and |
|
228 |
word_mult_1: "1 * a = a" and |
|
229 |
word_mult_1_right: "a * 1 = a" and |
|
230 |
word_add_commute: "a + b = b + a" and |
|
231 |
word_add_assoc: "a + b + c = a + (b + c)" and |
|
232 |
word_add_left_commute: "a + (b + c) = b + (a + c)" and |
|
233 |
word_mult_commute: "a * b = b * a" and |
|
234 |
word_mult_assoc: "a * b * c = a * (b * c)" and |
|
235 |
word_mult_left_commute: "a * (b * c) = b * (a * c)" and |
|
236 |
word_left_distrib: "(a + b) * c = a * c + b * c" and |
|
237 |
word_right_distrib: "a * (b + c) = a * b + a * c" and |
|
238 |
word_left_minus: "- a + a = 0" and |
|
239 |
word_diff_0_right: "a - 0 = a" and |
|
240 |
word_diff_self: "a - a = 0" |
|
241 |
using word_of_int_Ex [of a] |
|
242 |
word_of_int_Ex [of b] |
|
243 |
word_of_int_Ex [of c] |
|
244 |
by (auto simp: word_of_int_hom_syms [symmetric] |
|
245 |
zadd_0_right add_commute add_assoc add_left_commute |
|
246 |
mult_commute mult_assoc mult_left_commute |
|
247 |
plus_times.left_distrib plus_times.right_distrib) |
|
248 |
||
249 |
lemmas word_add_ac = word_add_commute word_add_assoc word_add_left_commute |
|
250 |
lemmas word_mult_ac = word_mult_commute word_mult_assoc word_mult_left_commute |
|
251 |
||
252 |
lemmas word_plus_ac0 = word_add_0 word_add_0_right word_add_ac |
|
253 |
lemmas word_times_ac1 = word_mult_1 word_mult_1_right word_mult_ac |
|
254 |
||
24408 | 255 |
instance word :: (type) semigroup_add |
24377
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
256 |
by intro_classes (simp add: word_add_assoc) |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
257 |
|
24408 | 258 |
instance word :: (type) ring |
24377
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
259 |
by intro_classes |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
260 |
(auto simp: word_arith_eqs word_diff_minus |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
261 |
word_diff_self [unfolded word_diff_minus]) |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
262 |
|
24333 | 263 |
|
24350 | 264 |
subsection "Order on fixed-length words" |
24333 | 265 |
|
24408 | 266 |
instance word :: (type) ord |
24377
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
267 |
word_le_def: "a <= b == uint a <= uint b" |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
268 |
word_less_def: "x < y == x <= y & x ~= y" |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
269 |
.. |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
270 |
|
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
271 |
constdefs |
24408 | 272 |
word_sle :: "'a :: finite word => 'a word => bool" ("(_/ <=s _)" [50, 51] 50) |
24377
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
273 |
"a <=s b == sint a <= sint b" |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
274 |
|
24408 | 275 |
word_sless :: "'a :: finite word => 'a word => bool" ("(_/ <s _)" [50, 51] 50) |
24377
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
276 |
"(x <s y) == (x <=s y & x ~= y)" |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
277 |
|
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
278 |
lemma word_less_alt: "(a < b) = (uint a < uint b)" |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
279 |
unfolding word_less_def word_le_def |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
280 |
by (auto simp del: word_uint.Rep_inject |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
281 |
simp: word_uint.Rep_inject [symmetric]) |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
282 |
|
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
283 |
lemma signed_linorder: "linorder word_sle word_sless" |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
284 |
apply unfold_locales |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
285 |
apply (unfold word_sle_def word_sless_def) |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
286 |
by auto |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
287 |
|
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
288 |
interpretation signed: linorder ["word_sle" "word_sless"] |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
289 |
by (rule signed_linorder) |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
290 |
|
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
291 |
lemmas word_less_no [simp] = |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
292 |
word_less_def [of "number_of ?a" "number_of ?b"] |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
293 |
|
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
294 |
lemmas word_le_no [simp] = |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
295 |
word_le_def [of "number_of ?a" "number_of ?b"] |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
296 |
|
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
297 |
lemmas word_sless_no [simp] = |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
298 |
word_sless_def [of "number_of ?a" "number_of ?b"] |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
299 |
|
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
300 |
lemmas word_sle_no [simp] = |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
301 |
word_sle_def [of "number_of ?a" "number_of ?b"] |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
302 |
|
24408 | 303 |
lemma word_order_trans: "x <= y ==> y <= z ==> x <= (z :: 'a word)" |
24333 | 304 |
unfolding word_le_def by auto |
305 |
||
24408 | 306 |
lemma word_order_refl: "z <= (z :: 'a word)" |
24333 | 307 |
unfolding word_le_def by auto |
308 |
||
24408 | 309 |
lemma word_order_antisym: "x <= y ==> y <= x ==> x = (y :: 'a word)" |
24333 | 310 |
unfolding word_le_def by (auto intro!: word_uint.Rep_eqD) |
311 |
||
312 |
lemma word_order_linear: |
|
24408 | 313 |
"y <= x | x <= (y :: 'a word)" |
24333 | 314 |
unfolding word_le_def by auto |
315 |
||
316 |
lemma word_zero_le [simp] : |
|
24408 | 317 |
"0 <= (y :: 'a word)" |
24333 | 318 |
unfolding word_le_def by auto |
319 |
||
24408 | 320 |
instance word :: (type) linorder |
24333 | 321 |
by intro_classes (auto simp: word_less_def word_le_def) |
322 |
||
323 |
lemma word_m1_ge [simp] : "word_pred 0 >= y" |
|
324 |
unfolding word_le_def |
|
325 |
by (simp only : word_pred_0_n1 word_uint.eq_norm m1mod2k) auto |
|
326 |
||
327 |
lemmas word_n1_ge [simp] = word_m1_ge [simplified word_sp_01] |
|
328 |
||
329 |
lemmas word_not_simps [simp] = |
|
330 |
word_zero_le [THEN leD] word_m1_ge [THEN leD] word_n1_ge [THEN leD] |
|
331 |
||
24408 | 332 |
lemma word_gt_0: "0 < y = (0 ~= (y :: 'a word))" |
24333 | 333 |
unfolding word_less_def by auto |
334 |
||
335 |
lemmas word_gt_0_no [simp] = word_gt_0 [of "number_of ?y"] |
|
336 |
||
337 |
lemma word_sless_alt: "(a <s b) == (sint a < sint b)" |
|
338 |
unfolding word_sle_def word_sless_def |
|
339 |
by (auto simp add : less_eq_less.less_le) |
|
340 |
||
341 |
lemma word_le_nat_alt: "(a <= b) = (unat a <= unat b)" |
|
342 |
unfolding unat_def word_le_def |
|
343 |
by (rule nat_le_eq_zle [symmetric]) simp |
|
344 |
||
345 |
lemma word_less_nat_alt: "(a < b) = (unat a < unat b)" |
|
346 |
unfolding unat_def word_less_alt |
|
347 |
by (rule nat_less_eq_zless [symmetric]) simp |
|
348 |
||
349 |
lemma wi_less: |
|
24408 | 350 |
"(word_of_int n < (word_of_int m :: 'a word)) = |
351 |
(n mod 2 ^ CARD('a) < m mod 2 ^ CARD('a))" |
|
24333 | 352 |
unfolding word_less_alt by (simp add: word_uint.eq_norm) |
353 |
||
354 |
lemma wi_le: |
|
24408 | 355 |
"(word_of_int n <= (word_of_int m :: 'a word)) = |
356 |
(n mod 2 ^ CARD('a) <= m mod 2 ^ CARD('a))" |
|
24333 | 357 |
unfolding word_le_def by (simp add: word_uint.eq_norm) |
358 |
||
24377
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
359 |
lemmas unat_mono = word_less_nat_alt [THEN iffD1, standard] |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
360 |
|
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
361 |
|
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
362 |
subsection "Divisibility" |
223622422d7b
move order-related stuff from WordDefinition to WordArith
huffman
parents:
24368
diff
changeset
|
363 |
|
24378
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset
|
364 |
definition |
24408 | 365 |
udvd :: "'a::finite word \<Rightarrow> 'a word \<Rightarrow> bool" (infixl "udvd" 50) where |
24378
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset
|
366 |
"a udvd b \<equiv> \<exists>n\<ge>0. uint b = n * uint a" |
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset
|
367 |
|
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset
|
368 |
lemma udvdI: |
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset
|
369 |
"0 \<le> n ==> uint b = n * uint a ==> a udvd b" |
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset
|
370 |
by (auto simp: udvd_def) |
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset
|
371 |
|
24333 | 372 |
lemma udvd_nat_alt: "a udvd b = (EX n>=0. unat b = n * unat a)" |
373 |
apply (unfold udvd_def) |
|
374 |
apply safe |
|
375 |
apply (simp add: unat_def nat_mult_distrib) |
|
376 |
apply (simp add: uint_nat int_mult) |
|
377 |
apply (rule exI) |
|
378 |
apply safe |
|
379 |
prefer 2 |
|
380 |
apply (erule notE) |
|
381 |
apply (rule refl) |
|
382 |
apply force |
|
383 |
done |
|
384 |
||
385 |
lemma udvd_iff_dvd: "x udvd y <-> unat x dvd unat y" |
|
386 |
unfolding dvd_def udvd_nat_alt by force |
|
387 |
||
24378
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset
|
388 |
|
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset
|
389 |
subsection "Division with remainder" |
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset
|
390 |
|
24408 | 391 |
instance word :: (type) Divides.div |
24378
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset
|
392 |
word_div_def: "a div b == word_of_int (uint a div uint b)" |
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset
|
393 |
word_mod_def: "a mod b == word_of_int (uint a mod uint b)" |
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset
|
394 |
.. |
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset
|
395 |
|
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset
|
396 |
lemmas word_div_no [simp] = |
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset
|
397 |
word_div_def [of "number_of ?a" "number_of ?b"] |
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset
|
398 |
|
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset
|
399 |
lemmas word_mod_no [simp] = |
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset
|
400 |
word_mod_def [of "number_of ?a" "number_of ?b"] |
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset
|
401 |
|
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset
|
402 |
lemmas uint_div_alt = word_div_def |
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset
|
403 |
[THEN meta_eq_to_obj_eq [THEN trans [OF uint_cong int_word_uint]], standard] |
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset
|
404 |
lemmas uint_mod_alt = word_mod_def |
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset
|
405 |
[THEN meta_eq_to_obj_eq [THEN trans [OF uint_cong int_word_uint]], standard] |
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset
|
406 |
|
af83eeb4a702
move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents:
24377
diff
changeset
|
407 |
|
24408 | 408 |
lemma word_zero_neq_one: "0 < CARD('a) ==> (0 :: 'a word) ~= 1"; |
24333 | 409 |
unfolding word_arith_wis |
410 |
by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc) |
|
411 |
||
24408 | 412 |
lemmas lenw1_zero_neq_one = zero_less_card_finite [THEN word_zero_neq_one] |
24333 | 413 |
|
414 |
lemma no_no [simp] : "number_of (number_of b) = number_of b" |
|
415 |
by (simp add: number_of_eq) |
|
416 |
||
417 |
lemma unat_minus_one: "x ~= 0 ==> unat (x - 1) = unat x - 1" |
|
418 |
apply (unfold unat_def) |
|
419 |
apply (simp only: int_word_uint word_arith_alts rdmods) |
|
420 |
apply (subgoal_tac "uint x >= 1") |
|
421 |
prefer 2 |
|
422 |
apply (drule contrapos_nn) |
|
423 |
apply (erule word_uint.Rep_inverse' [symmetric]) |
|
424 |
apply (insert uint_ge_0 [of x])[1] |
|
425 |
apply arith |
|
426 |
apply (rule box_equals) |
|
427 |
apply (rule nat_diff_distrib) |
|
428 |
prefer 2 |
|
429 |
apply assumption |
|
430 |
apply simp |
|
431 |
apply (subst mod_pos_pos_trivial) |
|
432 |
apply arith |
|
433 |
apply (insert uint_lt2p [of x])[1] |
|
434 |
apply arith |
|
435 |
apply (rule refl) |
|
436 |
apply simp |
|
437 |
done |
|
438 |
||
439 |
lemma measure_unat: "p ~= 0 ==> unat (p - 1) < unat p" |
|
440 |
by (simp add: unat_minus_one) (simp add: unat_0_iff [symmetric]) |
|
441 |
||
442 |
lemmas uint_add_ge0 [simp] = |
|
443 |
add_nonneg_nonneg [OF uint_ge_0 uint_ge_0, standard] |
|
444 |
lemmas uint_mult_ge0 [simp] = |
|
445 |
mult_nonneg_nonneg [OF uint_ge_0 uint_ge_0, standard] |
|
446 |
||
447 |
lemma uint_sub_lt2p [simp]: |
|
24408 | 448 |
"uint (x :: 'a word) - uint (y :: 'b word) < |
449 |
2 ^ CARD('a)" |
|
24333 | 450 |
using uint_ge_0 [of y] uint_lt2p [of x] by arith |
451 |
||
452 |
||
24350 | 453 |
subsection "Conditions for the addition (etc) of two words to overflow" |
24333 | 454 |
|
455 |
lemma uint_add_lem: |
|
24408 | 456 |
"(uint x + uint y < 2 ^ CARD('a)) = |
457 |
(uint (x + y :: 'a word) = uint x + uint y)" |
|
24333 | 458 |
by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem]) |
459 |
||
460 |
lemma uint_mult_lem: |
|
24408 | 461 |
"(uint x * uint y < 2 ^ CARD('a)) = |
462 |
(uint (x * y :: 'a word) = uint x * uint y)" |
|
24333 | 463 |
by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem]) |
464 |
||
465 |
lemma uint_sub_lem: |
|
466 |
"(uint x >= uint y) = (uint (x - y) = uint x - uint y)" |
|
467 |
by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem]) |
|
468 |
||
469 |
lemma uint_add_le: "uint (x + y) <= uint x + uint y" |
|
470 |
unfolding uint_word_ariths by (auto simp: mod_add_if_z) |
|
471 |
||
472 |
lemma uint_sub_ge: "uint (x - y) >= uint x - uint y" |
|
473 |
unfolding uint_word_ariths by (auto simp: mod_sub_if_z) |
|
474 |
||
475 |
lemmas uint_sub_if' = |
|
476 |
trans [OF uint_word_ariths(1) mod_sub_if_z, simplified, standard] |
|
477 |
lemmas uint_plus_if' = |
|
478 |
trans [OF uint_word_ariths(2) mod_add_if_z, simplified, standard] |
|
479 |
||
480 |
||
24350 | 481 |
subsection {* Definition of uint\_arith *} |
24333 | 482 |
|
483 |
lemma word_of_int_inverse: |
|
24408 | 484 |
"word_of_int r = a ==> 0 <= r ==> r < 2 ^ CARD('a) ==> |
485 |
uint (a::'a word) = r" |
|
24333 | 486 |
apply (erule word_uint.Abs_inverse' [rotated]) |
487 |
apply (simp add: uints_num) |
|
488 |
done |
|
489 |
||
490 |
lemma uint_split: |
|
24408 | 491 |
fixes x::"'a word" |
24333 | 492 |
shows "P (uint x) = |
24408 | 493 |
(ALL i. word_of_int i = x & 0 <= i & i < 2^CARD('a) --> P i)" |
24333 | 494 |
apply (fold word_int_case_def) |
495 |
apply (auto dest!: word_of_int_inverse simp: int_word_uint int_mod_eq' |
|
496 |
split: word_int_split) |
|
497 |
done |
|
498 |
||
499 |
lemma uint_split_asm: |
|
24408 | 500 |
fixes x::"'a word" |
24333 | 501 |
shows "P (uint x) = |
24408 | 502 |
(~(EX i. word_of_int i = x & 0 <= i & i < 2^CARD('a) & ~ P i))" |
24333 | 503 |
by (auto dest!: word_of_int_inverse |
504 |
simp: int_word_uint int_mod_eq' |
|
505 |
split: uint_split) |
|
506 |
||
507 |
lemmas uint_splits = uint_split uint_split_asm |
|
508 |
||
509 |
lemmas uint_arith_simps = |
|
510 |
word_le_def word_less_alt |
|
511 |
word_uint.Rep_inject [symmetric] |
|
512 |
uint_sub_if' uint_plus_if' |
|
513 |
||
24408 | 514 |
(* use this to stop, eg, 2 ^ CARD(32) being simplified *) |
24333 | 515 |
lemma power_False_cong: "False ==> a ^ b = c ^ d" |
516 |
by auto |
|
517 |
||
518 |
(* uint_arith_tac: reduce to arithmetic on int, try to solve by arith *) |
|
519 |
ML {* |
|
520 |
fun uint_arith_ss_of ss = |
|
521 |
ss addsimps @{thms uint_arith_simps} |
|
522 |
delsimps @{thms word_uint.Rep_inject} |
|
523 |
addsplits @{thms split_if_asm} |
|
524 |
addcongs @{thms power_False_cong} |
|
525 |
||
526 |
fun uint_arith_tacs ctxt = |
|
527 |
let fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty |
|
528 |
in |
|
529 |
[ CLASET' clarify_tac 1, |
|
530 |
SIMPSET' (full_simp_tac o uint_arith_ss_of) 1, |
|
531 |
ALLGOALS (full_simp_tac (HOL_ss addsplits @{thms uint_splits} |
|
532 |
addcongs @{thms power_False_cong})), |
|
533 |
rewrite_goals_tac @{thms word_size}, |
|
534 |
ALLGOALS (fn n => REPEAT (resolve_tac [allI, impI] n) THEN |
|
535 |
REPEAT (etac conjE n) THEN |
|
536 |
REPEAT (dtac @{thm word_of_int_inverse} n |
|
537 |
THEN atac n |
|
538 |
THEN atac n)), |
|
539 |
TRYALL arith_tac' ] |
|
540 |
end |
|
541 |
||
542 |
fun uint_arith_tac ctxt = SELECT_GOAL (EVERY (uint_arith_tacs ctxt)) |
|
543 |
*} |
|
544 |
||
545 |
method_setup uint_arith = |
|
546 |
"Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (uint_arith_tac ctxt 1))" |
|
547 |
"solving word arithmetic via integers and arith" |
|
548 |
||
549 |
||
24350 | 550 |
subsection "More on overflows and monotonicity" |
24333 | 551 |
|
552 |
lemma no_plus_overflow_uint_size: |
|
24408 | 553 |
"((x :: 'a word) <= x + y) = (uint x + uint y < 2 ^ size x)" |
24333 | 554 |
unfolding word_size by uint_arith |
555 |
||
556 |
lemmas no_olen_add = no_plus_overflow_uint_size [unfolded word_size] |
|
557 |
||
24408 | 558 |
lemma no_ulen_sub: "((x :: 'a word) >= x - y) = (uint y <= uint x)" |
24333 | 559 |
by uint_arith |
560 |
||
561 |
lemma no_olen_add': |
|
24408 | 562 |
fixes x :: "'a word" |
563 |
shows "(x \<le> y + x) = (uint y + uint x < 2 ^ CARD('a))" |
|
24333 | 564 |
by (simp add: word_add_ac add_ac no_olen_add) |
565 |
||
566 |
lemmas olen_add_eqv = trans [OF no_olen_add no_olen_add' [symmetric], standard] |
|
567 |
||
568 |
lemmas uint_plus_simple_iff = trans [OF no_olen_add uint_add_lem, standard] |
|
569 |
lemmas uint_plus_simple = uint_plus_simple_iff [THEN iffD1, standard] |
|
570 |
lemmas uint_minus_simple_iff = trans [OF no_ulen_sub uint_sub_lem, standard] |
|
571 |
lemmas uint_minus_simple_alt = uint_sub_lem [folded word_le_def] |
|
572 |
lemmas word_sub_le_iff = no_ulen_sub [folded word_le_def] |
|
573 |
lemmas word_sub_le = word_sub_le_iff [THEN iffD2, standard] |
|
574 |
||
575 |
lemma word_less_sub1: |
|
24408 | 576 |
"(x :: 'a :: finite word) ~= 0 ==> (1 < x) = (0 < x - 1)" |
24333 | 577 |
by uint_arith |
578 |
||
579 |
lemma word_le_sub1: |
|
24408 | 580 |
"(x :: 'a :: finite word) ~= 0 ==> (1 <= x) = (0 <= x - 1)" |
24333 | 581 |
by uint_arith |
582 |
||
583 |
lemma sub_wrap_lt: |
|
24408 | 584 |
"((x :: 'a word) < x - z) = (x < z)" |
24333 | 585 |
by uint_arith |
586 |
||
587 |
lemma sub_wrap: |
|
24408 | 588 |
"((x :: 'a word) <= x - z) = (z = 0 | x < z)" |
24333 | 589 |
by uint_arith |
590 |
||
591 |
lemma plus_minus_not_NULL_ab: |
|
24408 | 592 |
"(x :: 'a word) <= ab - c ==> c <= ab ==> c ~= 0 ==> x + c ~= 0" |
24333 | 593 |
by uint_arith |
594 |
||
595 |
lemma plus_minus_no_overflow_ab: |
|
24408 | 596 |
"(x :: 'a word) <= ab - c ==> c <= ab ==> x <= x + c" |
24333 | 597 |
by uint_arith |
598 |
||
599 |
lemma le_minus': |
|
24408 | 600 |
"(a :: 'a word) + c <= b ==> a <= a + c ==> c <= b - a" |
24333 | 601 |
by uint_arith |
602 |
||
603 |
lemma le_plus': |
|
24408 | 604 |
"(a :: 'a word) <= b ==> c <= b - a ==> a + c <= b" |
24333 | 605 |
by uint_arith |
606 |
||
607 |
lemmas le_plus = le_plus' [rotated] |
|
608 |
||
609 |
lemmas le_minus = leD [THEN thin_rl, THEN le_minus', standard] |
|
610 |
||
611 |
lemma word_plus_mono_right: |
|
24408 | 612 |
"(y :: 'a word) <= z ==> x <= x + z ==> x + y <= x + z" |
24333 | 613 |
by uint_arith |
614 |
||
615 |
lemma word_less_minus_cancel: |
|
24408 | 616 |
"y - x < z - x ==> x <= z ==> (y :: 'a word) < z" |
24333 | 617 |
by uint_arith |
618 |
||
619 |
lemma word_less_minus_mono_left: |
|
24408 | 620 |
"(y :: 'a word) < z ==> x <= y ==> y - x < z - x" |
24333 | 621 |
by uint_arith |
622 |
||
623 |
lemma word_less_minus_mono: |
|
624 |
"a < c ==> d < b ==> a - b < a ==> c - d < c |
|
24408 | 625 |
==> a - b < c - (d::'a::finite word)" |
24333 | 626 |
by uint_arith |
627 |
||
628 |
lemma word_le_minus_cancel: |
|
24408 | 629 |
"y - x <= z - x ==> x <= z ==> (y :: 'a word) <= z" |
24333 | 630 |
by uint_arith |
631 |
||
632 |
lemma word_le_minus_mono_left: |
|
24408 | 633 |
"(y :: 'a word) <= z ==> x <= y ==> y - x <= z - x" |
24333 | 634 |
by uint_arith |
635 |
||
636 |
lemma word_le_minus_mono: |
|
637 |
"a <= c ==> d <= b ==> a - b <= a ==> c - d <= c |
|
24408 | 638 |
==> a - b <= c - (d::'a::finite word)" |
24333 | 639 |
by uint_arith |
640 |
||
641 |
lemma plus_le_left_cancel_wrap: |
|
24408 | 642 |
"(x :: 'a word) + y' < x ==> x + y < x ==> (x + y' < x + y) = (y' < y)" |
24333 | 643 |
by uint_arith |
644 |
||
645 |
lemma plus_le_left_cancel_nowrap: |
|
24408 | 646 |
"(x :: 'a word) <= x + y' ==> x <= x + y ==> |
24333 | 647 |
(x + y' < x + y) = (y' < y)" |
648 |
by uint_arith |
|
649 |
||
650 |
lemma word_plus_mono_right2: |
|
24408 | 651 |
"(a :: 'a word) <= a + b ==> c <= b ==> a <= a + c" |
24333 | 652 |
by uint_arith |
653 |
||
654 |
lemma word_less_add_right: |
|
24408 | 655 |
"(x :: 'a word) < y - z ==> z <= y ==> x + z < y" |
24333 | 656 |
by uint_arith |
657 |
||
658 |
lemma word_less_sub_right: |
|
24408 | 659 |
"(x :: 'a word) < y + z ==> y <= x ==> x - y < z" |
24333 | 660 |
by uint_arith |
661 |
||
662 |
lemma word_le_plus_either: |
|
24408 | 663 |
"(x :: 'a word) <= y | x <= z ==> y <= y + z ==> x <= y + z" |
24333 | 664 |
by uint_arith |
665 |
||
666 |
lemma word_less_nowrapI: |
|
24408 | 667 |
"(x :: 'a word) < z - k ==> k <= z ==> 0 < k ==> x < x + k" |
24333 | 668 |
by uint_arith |
669 |
||
24408 | 670 |
lemma inc_le: "(i :: 'a :: finite word) < m ==> i + 1 <= m" |
24333 | 671 |
by uint_arith |
672 |
||
673 |
lemma inc_i: |
|
24408 | 674 |
"(1 :: 'a :: finite word) <= i ==> i < m ==> 1 <= (i + 1) & i + 1 <= m" |
24333 | 675 |
by uint_arith |
676 |
||
677 |
lemma udvd_incr_lem: |
|
678 |
"up < uq ==> up = ua + n * uint K ==> |
|
679 |
uq = ua + n' * uint K ==> up + uint K <= uq" |
|
680 |
apply clarsimp |
|
681 |
apply (drule less_le_mult) |
|
682 |
apply safe |
|
683 |
done |
|
684 |
||
685 |
lemma udvd_incr': |
|
686 |
"p < q ==> uint p = ua + n * uint K ==> |
|
687 |
uint q = ua + n' * uint K ==> p + K <= q" |
|
688 |
apply (unfold word_less_alt word_le_def) |
|
689 |
apply (drule (2) udvd_incr_lem) |
|
690 |
apply (erule uint_add_le [THEN order_trans]) |
|
691 |
done |
|
692 |
||
693 |
lemma udvd_decr': |
|
694 |
"p < q ==> uint p = ua + n * uint K ==> |
|
695 |
uint q = ua + n' * uint K ==> p <= q - K" |
|
696 |
apply (unfold word_less_alt word_le_def) |
|
697 |
apply (drule (2) udvd_incr_lem) |
|
698 |
apply (drule le_diff_eq [THEN iffD2]) |
|
699 |
apply (erule order_trans) |
|
700 |
apply (rule uint_sub_ge) |
|
701 |
done |
|
702 |
||
703 |
lemmas udvd_incr_lem0 = udvd_incr_lem [where ua=0, simplified] |
|
704 |
lemmas udvd_incr0 = udvd_incr' [where ua=0, simplified] |
|
705 |
lemmas udvd_decr0 = udvd_decr' [where ua=0, simplified] |
|
706 |
||
707 |
lemma udvd_minus_le': |
|
708 |
"xy < k ==> z udvd xy ==> z udvd k ==> xy <= k - z" |
|
709 |
apply (unfold udvd_def) |
|
710 |
apply clarify |
|
711 |
apply (erule (2) udvd_decr0) |
|
712 |
done |
|
713 |
||
714 |
lemma udvd_incr2_K: |
|
715 |
"p < a + s ==> a <= a + s ==> K udvd s ==> K udvd p - a ==> a <= p ==> |
|
716 |
0 < K ==> p <= p + K & p + K <= a + s" |
|
717 |
apply (unfold udvd_def) |
|
718 |
apply clarify |
|
719 |
apply (simp add: uint_arith_simps split: split_if_asm) |
|
720 |
prefer 2 |
|
721 |
apply (insert uint_range' [of s])[1] |
|
722 |
apply arith |
|
723 |
apply (drule add_commute [THEN xtr1]) |
|
724 |
apply (simp add: diff_less_eq [symmetric]) |
|
725 |
apply (drule less_le_mult) |
|
726 |
apply arith |
|
727 |
apply simp |
|
728 |
done |
|
729 |
||
24350 | 730 |
subsection "Arithmetic type class instantiations" |
24333 | 731 |
|
24408 | 732 |
instance word :: (type) comm_monoid_add .. |
24333 | 733 |
|
24408 | 734 |
instance word :: (type) comm_monoid_mult |
24333 | 735 |
apply (intro_classes) |
736 |
apply (simp add: word_mult_commute) |
|
737 |
apply (simp add: word_mult_1) |
|
738 |
done |
|
739 |
||
24408 | 740 |
instance word :: (type) comm_semiring |
24333 | 741 |
by (intro_classes) (simp add : word_left_distrib) |
742 |
||
24408 | 743 |
instance word :: (type) ab_group_add .. |
24333 | 744 |
|
24408 | 745 |
instance word :: (type) comm_ring .. |
24333 | 746 |
|
24408 | 747 |
instance word :: (finite) comm_semiring_1 |
24333 | 748 |
by (intro_classes) (simp add: lenw1_zero_neq_one) |
749 |
||
24408 | 750 |
instance word :: (finite) comm_ring_1 .. |
24333 | 751 |
|
24408 | 752 |
instance word :: (type) comm_semiring_0 .. |
24333 | 753 |
|
24408 | 754 |
instance word :: (finite) recpower |
24333 | 755 |
by (intro_classes) (simp_all add: word_pow) |
756 |
||
757 |
(* note that iszero_def is only for class comm_semiring_1_cancel, |
|
24408 | 758 |
which requires word length >= 1, ie 'a :: finite word *) |
24333 | 759 |
lemma zero_bintrunc: |
24408 | 760 |
"iszero (number_of x :: 'a :: finite word) = |
761 |
(bintrunc CARD('a) x = Numeral.Pls)" |
|
24333 | 762 |
apply (unfold iszero_def word_0_wi word_no_wi) |
763 |
apply (rule word_ubin.norm_eq_iff [symmetric, THEN trans]) |
|
764 |
apply (simp add : Pls_def [symmetric]) |
|
765 |
done |
|
766 |
||
767 |
lemmas word_le_0_iff [simp] = |
|
768 |
word_zero_le [THEN leD, THEN linorder_antisym_conv1] |
|
769 |
||
770 |
lemma word_of_nat: "of_nat n = word_of_int (int n)" |
|
771 |
by (induct n) (auto simp add : word_of_int_hom_syms) |
|
772 |
||
773 |
lemma word_of_int: "of_int = word_of_int" |
|
774 |
apply (rule ext) |
|
24382 | 775 |
apply (case_tac x rule: int_diff_cases) |
776 |
apply (simp add: word_of_nat word_of_int_sub_hom) |
|
24333 | 777 |
done |
778 |
||
779 |
lemma word_of_int_nat: |
|
780 |
"0 <= x ==> word_of_int x = of_nat (nat x)" |
|
781 |
by (simp add: of_nat_nat word_of_int) |
|
782 |
||
783 |
lemma word_number_of_eq: |
|
24408 | 784 |
"number_of w = (of_int w :: 'a :: finite word)" |
24333 | 785 |
unfolding word_number_of_def word_of_int by auto |
786 |
||
24408 | 787 |
instance word :: (finite) number_ring |
24333 | 788 |
by (intro_classes) (simp add : word_number_of_eq) |
789 |
||
790 |
lemma iszero_word_no [simp] : |
|
24408 | 791 |
"iszero (number_of bin :: 'a :: finite word) = |
792 |
iszero (number_of (bintrunc CARD('a) bin) :: int)" |
|
24368 | 793 |
apply (simp add: zero_bintrunc number_of_is_id) |
24333 | 794 |
apply (unfold iszero_def Pls_def) |
795 |
apply (rule refl) |
|
796 |
done |
|
797 |
||
798 |
||
24350 | 799 |
subsection "Word and nat" |
24333 | 800 |
|
801 |
lemma td_ext_unat': |
|
24408 | 802 |
"n = CARD('a :: finite) ==> |
24333 | 803 |
td_ext (unat :: 'a word => nat) of_nat |
804 |
(unats n) (%i. i mod 2 ^ n)" |
|
805 |
apply (unfold td_ext_def' unat_def word_of_nat unats_uints) |
|
806 |
apply (auto intro!: imageI simp add : word_of_int_hom_syms) |
|
807 |
apply (erule word_uint.Abs_inverse [THEN arg_cong]) |
|
808 |
apply (simp add: int_word_uint nat_mod_distrib nat_power_eq) |
|
809 |
done |
|
810 |
||
811 |
lemmas td_ext_unat = refl [THEN td_ext_unat'] |
|
812 |
lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm, standard] |
|
813 |
||
814 |
interpretation word_unat: |
|
24408 | 815 |
td_ext ["unat::'a::finite word => nat" |
24333 | 816 |
of_nat |
24408 | 817 |
"unats CARD('a::finite)" |
818 |
"%i. i mod 2 ^ CARD('a::finite)"] |
|
24333 | 819 |
by (rule td_ext_unat) |
820 |
||
821 |
lemmas td_unat = word_unat.td_thm |
|
822 |
||
823 |
lemmas unat_lt2p [iff] = word_unat.Rep [unfolded unats_def mem_Collect_eq] |
|
824 |
||
24408 | 825 |
lemma unat_le: "y <= unat (z :: 'a :: finite word) ==> y : unats CARD('a)" |
24333 | 826 |
apply (unfold unats_def) |
827 |
apply clarsimp |
|
828 |
apply (rule xtrans, rule unat_lt2p, assumption) |
|
829 |
done |
|
830 |
||
831 |
lemma word_nchotomy: |
|
24408 | 832 |
"ALL w. EX n. (w :: 'a :: finite word) = of_nat n & n < 2 ^ CARD('a)" |
24333 | 833 |
apply (rule allI) |
834 |
apply (rule word_unat.Abs_cases) |
|
835 |
apply (unfold unats_def) |
|
836 |
apply auto |
|
837 |
done |
|
838 |
||
839 |
lemma of_nat_eq: |
|
24408 | 840 |
fixes w :: "'a::finite word" |
841 |
shows "(of_nat n = w) = (\<exists>q. n = unat w + q * 2 ^ CARD('a))" |
|
24333 | 842 |
apply (rule trans) |
843 |
apply (rule word_unat.inverse_norm) |
|
844 |
apply (rule iffI) |
|
845 |
apply (rule mod_eqD) |
|
846 |
apply simp |
|
847 |
apply clarsimp |
|
848 |
done |
|
849 |
||
850 |
lemma of_nat_eq_size: |
|
851 |
"(of_nat n = w) = (EX q. n = unat w + q * 2 ^ size w)" |
|
852 |
unfolding word_size by (rule of_nat_eq) |
|
853 |
||
854 |
lemma of_nat_0: |
|
24408 | 855 |
"(of_nat m = (0::'a::finite word)) = (\<exists>q. m = q * 2 ^ CARD('a))" |
24333 | 856 |
by (simp add: of_nat_eq) |
857 |
||
858 |
lemmas of_nat_2p = mult_1 [symmetric, THEN iffD2 [OF of_nat_0 exI]] |
|
859 |
||
860 |
lemma of_nat_gt_0: "of_nat k ~= 0 ==> 0 < k" |
|
861 |
by (cases k) auto |
|
862 |
||
863 |
lemma of_nat_neq_0: |
|
24408 | 864 |
"0 < k ==> k < 2 ^ CARD('a :: finite) ==> of_nat k ~= (0 :: 'a word)" |
24333 | 865 |
by (clarsimp simp add : of_nat_0) |
866 |
||
867 |
lemma Abs_fnat_hom_add: |
|
868 |
"of_nat a + of_nat b = of_nat (a + b)" |
|
869 |
by simp |
|
870 |
||
871 |
lemma Abs_fnat_hom_mult: |
|
24408 | 872 |
"of_nat a * of_nat b = (of_nat (a * b) :: 'a :: finite word)" |
24333 | 873 |
by (simp add: word_of_nat word_of_int_mult_hom zmult_int) |
874 |
||
875 |
lemma Abs_fnat_hom_Suc: |
|
876 |
"word_succ (of_nat a) = of_nat (Suc a)" |
|
877 |
by (simp add: word_of_nat word_of_int_succ_hom add_ac) |
|
878 |
||
24408 | 879 |
lemma Abs_fnat_hom_0: "(0::'a::finite word) = of_nat 0" |
24333 | 880 |
by (simp add: word_of_nat word_0_wi) |
881 |
||
24408 | 882 |
lemma Abs_fnat_hom_1: "(1::'a::finite word) = of_nat (Suc 0)" |
24333 | 883 |
by (simp add: word_of_nat word_1_wi) |
884 |
||
885 |
lemmas Abs_fnat_homs = |
|
886 |
Abs_fnat_hom_add Abs_fnat_hom_mult Abs_fnat_hom_Suc |
|
887 |
Abs_fnat_hom_0 Abs_fnat_hom_1 |
|
888 |
||
889 |
lemma word_arith_nat_add: |
|
890 |
"a + b = of_nat (unat a + unat b)" |
|
891 |
by simp |
|
892 |
||
893 |
lemma word_arith_nat_mult: |
|
894 |
"a * b = of_nat (unat a * unat b)" |
|
895 |
by (simp add: Abs_fnat_hom_mult [symmetric]) |
|
896 |
||
897 |
lemma word_arith_nat_Suc: |
|
898 |
"word_succ a = of_nat (Suc (unat a))" |
|
899 |
by (subst Abs_fnat_hom_Suc [symmetric]) simp |
|
900 |
||
901 |
lemma word_arith_nat_div: |
|
902 |
"a div b = of_nat (unat a div unat b)" |
|
903 |
by (simp add: word_div_def word_of_nat zdiv_int uint_nat) |
|
904 |
||
905 |
lemma word_arith_nat_mod: |
|
906 |
"a mod b = of_nat (unat a mod unat b)" |
|
907 |
by (simp add: word_mod_def word_of_nat zmod_int uint_nat) |
|
908 |
||
909 |
lemmas word_arith_nat_defs = |
|
910 |
word_arith_nat_add word_arith_nat_mult |
|
911 |
word_arith_nat_Suc Abs_fnat_hom_0 |
|
912 |
Abs_fnat_hom_1 word_arith_nat_div |
|
913 |
word_arith_nat_mod |
|
914 |
||
915 |
lemmas unat_cong = arg_cong [where f = "unat"] |
|
916 |
||
917 |
lemmas unat_word_ariths = word_arith_nat_defs |
|
918 |
[THEN trans [OF unat_cong unat_of_nat], standard] |
|
919 |
||
920 |
lemmas word_sub_less_iff = word_sub_le_iff |
|
921 |
[simplified linorder_not_less [symmetric], simplified] |
|
922 |
||
923 |
lemma unat_add_lem: |
|
24408 | 924 |
"(unat x + unat y < 2 ^ CARD('a)) = |
925 |
(unat (x + y :: 'a :: finite word) = unat x + unat y)" |
|
24333 | 926 |
unfolding unat_word_ariths |
927 |
by (auto intro!: trans [OF _ nat_mod_lem]) |
|
928 |
||
929 |
lemma unat_mult_lem: |
|
24408 | 930 |
"(unat x * unat y < 2 ^ CARD('a)) = |
931 |
(unat (x * y :: 'a :: finite word) = unat x * unat y)" |
|
24333 | 932 |
unfolding unat_word_ariths |
933 |
by (auto intro!: trans [OF _ nat_mod_lem]) |
|
934 |
||
935 |
lemmas unat_plus_if' = |
|
936 |
trans [OF unat_word_ariths(1) mod_nat_add, simplified, standard] |
|
937 |
||
938 |
lemma le_no_overflow: |
|
24408 | 939 |
"x <= b ==> a <= a + b ==> x <= a + (b :: 'a word)" |
24333 | 940 |
apply (erule order_trans) |
941 |
apply (erule olen_add_eqv [THEN iffD1]) |
|
942 |
done |
|
943 |
||
944 |
lemmas un_ui_le = trans |
|
945 |
[OF word_le_nat_alt [symmetric] |
|
946 |
word_le_def [THEN meta_eq_to_obj_eq], |
|
947 |
standard] |
|
948 |
||
949 |
lemma unat_sub_if_size: |
|
950 |
"unat (x - y) = (if unat y <= unat x |
|
951 |
then unat x - unat y |
|
952 |
else unat x + 2 ^ size x - unat y)" |
|
953 |
apply (unfold word_size) |
|
954 |
apply (simp add: un_ui_le) |
|
955 |
apply (auto simp add: unat_def uint_sub_if') |
|
956 |
apply (rule nat_diff_distrib) |
|
957 |
prefer 3 |
|
958 |
apply (simp add: group_simps) |
|
959 |
apply (rule nat_diff_distrib [THEN trans]) |
|
960 |
prefer 3 |
|
961 |
apply (subst nat_add_distrib) |
|
962 |
prefer 3 |
|
963 |
apply (simp add: nat_power_eq) |
|
964 |
apply auto |
|
965 |
apply uint_arith |
|
966 |
done |
|
967 |
||
968 |
lemmas unat_sub_if' = unat_sub_if_size [unfolded word_size] |
|
969 |
||
24408 | 970 |
lemma unat_div: "unat ((x :: 'a :: finite word) div y) = unat x div unat y" |
24333 | 971 |
apply (simp add : unat_word_ariths) |
972 |
apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq']) |
|
973 |
apply (rule div_le_dividend) |
|
974 |
done |
|
975 |
||
24408 | 976 |
lemma unat_mod: "unat ((x :: 'a :: finite word) mod y) = unat x mod unat y" |
24333 | 977 |
apply (clarsimp simp add : unat_word_ariths) |
978 |
apply (cases "unat y") |
|
979 |
prefer 2 |
|
980 |
apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq']) |
|
981 |
apply (rule mod_le_divisor) |
|
982 |
apply auto |
|
983 |
done |
|
984 |
||
24408 | 985 |
lemma uint_div: "uint ((x :: 'a :: finite word) div y) = uint x div uint y" |
24333 | 986 |
unfolding uint_nat by (simp add : unat_div zdiv_int) |
987 |
||
24408 | 988 |
lemma uint_mod: "uint ((x :: 'a :: finite word) mod y) = uint x mod uint y" |
24333 | 989 |
unfolding uint_nat by (simp add : unat_mod zmod_int) |
990 |
||
991 |
||
24350 | 992 |
subsection {* Definition of unat\_arith tactic *} |
24333 | 993 |
|
994 |
lemma unat_split: |
|
24408 | 995 |
fixes x::"'a::finite word" |
24333 | 996 |
shows "P (unat x) = |
24408 | 997 |
(ALL n. of_nat n = x & n < 2^CARD('a) --> P n)" |
24333 | 998 |
by (auto simp: unat_of_nat) |
999 |
||
1000 |
lemma unat_split_asm: |
|
24408 | 1001 |
fixes x::"'a::finite word" |
24333 | 1002 |
shows "P (unat x) = |
24408 | 1003 |
(~(EX n. of_nat n = x & n < 2^CARD('a) & ~ P n))" |
24333 | 1004 |
by (auto simp: unat_of_nat) |
1005 |
||
1006 |
lemmas of_nat_inverse = |
|
1007 |
word_unat.Abs_inverse' [rotated, unfolded unats_def, simplified] |
|
1008 |
||
1009 |
lemmas unat_splits = unat_split unat_split_asm |
|
1010 |
||
1011 |
lemmas unat_arith_simps = |
|
1012 |
word_le_nat_alt word_less_nat_alt |
|
1013 |
word_unat.Rep_inject [symmetric] |
|
1014 |
unat_sub_if' unat_plus_if' unat_div unat_mod |
|
1015 |
||
1016 |
(* unat_arith_tac: tactic to reduce word arithmetic to nat, |
|
1017 |
try to solve via arith *) |
|
1018 |
ML {* |
|
1019 |
fun unat_arith_ss_of ss = |
|
1020 |
ss addsimps @{thms unat_arith_simps} |
|
1021 |
delsimps @{thms word_unat.Rep_inject} |
|
1022 |
addsplits @{thms split_if_asm} |
|
1023 |
addcongs @{thms power_False_cong} |
|
1024 |
||
1025 |
fun unat_arith_tacs ctxt = |
|
1026 |
let fun arith_tac' n t = arith_tac ctxt n t handle COOPER => Seq.empty |
|
1027 |
in |
|
1028 |
[ CLASET' clarify_tac 1, |
|
1029 |
SIMPSET' (full_simp_tac o unat_arith_ss_of) 1, |
|
1030 |
ALLGOALS (full_simp_tac (HOL_ss addsplits @{thms unat_splits} |
|
1031 |
addcongs @{thms power_False_cong})), |
|
1032 |
rewrite_goals_tac @{thms word_size}, |
|
1033 |
ALLGOALS (fn n => REPEAT (resolve_tac [allI, impI] n) THEN |
|
1034 |
REPEAT (etac conjE n) THEN |
|
1035 |
REPEAT (dtac @{thm of_nat_inverse} n THEN atac n)), |
|
1036 |
TRYALL arith_tac' ] |
|
1037 |
end |
|
1038 |
||
1039 |
fun unat_arith_tac ctxt = SELECT_GOAL (EVERY (unat_arith_tacs ctxt)) |
|
1040 |
*} |
|
1041 |
||
1042 |
method_setup unat_arith = |
|
1043 |
"Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (unat_arith_tac ctxt 1))" |
|
1044 |
"solving word arithmetic via natural numbers and arith" |
|
1045 |
||
1046 |
lemma no_plus_overflow_unat_size: |
|
24408 | 1047 |
"((x :: 'a :: finite word) <= x + y) = (unat x + unat y < 2 ^ size x)" |
24333 | 1048 |
unfolding word_size by unat_arith |
1049 |
||
24408 | 1050 |
lemma unat_sub: "b <= a ==> unat (a - b) = unat a - unat (b :: 'a :: finite word)" |
24333 | 1051 |
by unat_arith |
1052 |
||
1053 |
lemmas no_olen_add_nat = no_plus_overflow_unat_size [unfolded word_size] |
|
1054 |
||
1055 |
lemmas unat_plus_simple = trans [OF no_olen_add_nat unat_add_lem, standard] |
|
1056 |
||
1057 |
lemma word_div_mult: |
|
24408 | 1058 |
"(0 :: 'a :: finite word) < y ==> unat x * unat y < 2 ^ CARD('a) ==> |
24333 | 1059 |
x * y div y = x" |
1060 |
apply unat_arith |
|
1061 |
apply clarsimp |
|
1062 |
apply (subst unat_mult_lem [THEN iffD1]) |
|
1063 |
apply auto |
|
1064 |
done |
|
1065 |
||
24408 | 1066 |
lemma div_lt': "(i :: 'a :: finite word) <= k div x ==> |
1067 |
unat i * unat x < 2 ^ CARD('a)" |
|
24333 | 1068 |
apply unat_arith |
1069 |
apply clarsimp |
|
1070 |
apply (drule mult_le_mono1) |
|
1071 |
apply (erule order_le_less_trans) |
|
1072 |
apply (rule xtr7 [OF unat_lt2p div_mult_le]) |
|
1073 |
done |
|
1074 |
||
1075 |
lemmas div_lt'' = order_less_imp_le [THEN div_lt'] |
|
1076 |
||
24408 | 1077 |
lemma div_lt_mult: "(i :: 'a :: finite word) < k div x ==> 0 < x ==> i * x < k" |
24333 | 1078 |
apply (frule div_lt'' [THEN unat_mult_lem [THEN iffD1]]) |
1079 |
apply (simp add: unat_arith_simps) |
|
1080 |
apply (drule (1) mult_less_mono1) |
|
1081 |
apply (erule order_less_le_trans) |
|
1082 |
apply (rule div_mult_le) |
|
1083 |
done |
|
1084 |
||
1085 |
lemma div_le_mult: |
|
24408 | 1086 |
"(i :: 'a :: finite word) <= k div x ==> 0 < x ==> i * x <= k" |
24333 | 1087 |
apply (frule div_lt' [THEN unat_mult_lem [THEN iffD1]]) |
1088 |
apply (simp add: unat_arith_simps) |
|
1089 |
apply (drule mult_le_mono1) |
|
1090 |
apply (erule order_trans) |
|
1091 |
apply (rule div_mult_le) |
|
1092 |
done |
|
1093 |
||
1094 |
lemma div_lt_uint': |
|
24408 | 1095 |
"(i :: 'a :: finite word) <= k div x ==> uint i * uint x < 2 ^ CARD('a)" |
24333 | 1096 |
apply (unfold uint_nat) |
1097 |
apply (drule div_lt') |
|
1098 |
apply (simp add: zmult_int zless_nat_eq_int_zless [symmetric] |
|
1099 |
nat_power_eq) |
|
1100 |
done |
|
1101 |
||
1102 |
lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint'] |
|
1103 |
||
1104 |
lemma word_le_exists': |
|
24408 | 1105 |
"(x :: 'a word) <= y ==> |
1106 |
(EX z. y = x + z & uint x + uint z < 2 ^ CARD('a))" |
|
24333 | 1107 |
apply (rule exI) |
1108 |
apply (rule conjI) |
|
1109 |
apply (rule zadd_diff_inverse) |
|
1110 |
apply uint_arith |
|
1111 |
done |
|
1112 |
||
1113 |
lemmas plus_minus_not_NULL = order_less_imp_le [THEN plus_minus_not_NULL_ab] |
|
1114 |
||
1115 |
lemmas plus_minus_no_overflow = |
|
1116 |
order_less_imp_le [THEN plus_minus_no_overflow_ab] |
|
1117 |
||
1118 |
lemmas mcs = word_less_minus_cancel word_less_minus_mono_left |
|
1119 |
word_le_minus_cancel word_le_minus_mono_left |
|
1120 |
||
1121 |
lemmas word_l_diffs = mcs [where y = "?w + ?x", unfolded add_diff_cancel] |
|
1122 |
lemmas word_diff_ls = mcs [where z = "?w + ?x", unfolded add_diff_cancel] |
|
1123 |
lemmas word_plus_mcs = word_diff_ls |
|
1124 |
[where y = "?v + ?x", unfolded add_diff_cancel] |
|
1125 |
||
1126 |
lemmas le_unat_uoi = unat_le [THEN word_unat.Abs_inverse] |
|
1127 |
||
1128 |
lemmas thd = refl [THEN [2] split_div_lemma [THEN iffD2], THEN conjunct1] |
|
1129 |
||
1130 |
lemma thd1: |
|
1131 |
"a div b * b \<le> (a::nat)" |
|
1132 |
using gt_or_eq_0 [of b] |
|
1133 |
apply (rule disjE) |
|
1134 |
apply (erule xtr4 [OF thd mult_commute]) |
|
1135 |
apply clarsimp |
|
1136 |
done |
|
1137 |
||
1138 |
lemmas uno_simps [THEN le_unat_uoi, standard] = |
|
1139 |
mod_le_divisor div_le_dividend thd1 |
|
1140 |
||
1141 |
lemma word_mod_div_equality: |
|
24408 | 1142 |
"(n div b) * b + (n mod b) = (n :: 'a :: finite word)" |
24333 | 1143 |
apply (unfold word_less_nat_alt word_arith_nat_defs) |
1144 |
apply (cut_tac y="unat b" in gt_or_eq_0) |
|
1145 |
apply (erule disjE) |
|
1146 |
apply (simp add: mod_div_equality uno_simps) |
|
1147 |
apply simp |
|
1148 |
done |
|
1149 |
||
24408 | 1150 |
lemma word_div_mult_le: "a div b * b <= (a::'a::finite word)" |
24333 | 1151 |
apply (unfold word_le_nat_alt word_arith_nat_defs) |
1152 |
apply (cut_tac y="unat b" in gt_or_eq_0) |
|
1153 |
apply (erule disjE) |
|
1154 |
apply (simp add: div_mult_le uno_simps) |
|
1155 |
apply simp |
|
1156 |
done |
|
1157 |
||
24408 | 1158 |
lemma word_mod_less_divisor: "0 < n ==> m mod n < (n :: 'a :: finite word)" |
24333 | 1159 |
apply (simp only: word_less_nat_alt word_arith_nat_defs) |
1160 |
apply (clarsimp simp add : uno_simps) |
|
1161 |
done |
|
1162 |
||
1163 |
lemma word_of_int_power_hom: |
|
24408 | 1164 |
"word_of_int a ^ n = (word_of_int (a ^ n) :: 'a :: finite word)" |
24333 | 1165 |
by (induct n) (simp_all add : word_of_int_hom_syms power_Suc) |
1166 |
||
1167 |
lemma word_arith_power_alt: |
|
24408 | 1168 |
"a ^ n = (word_of_int (uint a ^ n) :: 'a :: finite word)" |
24333 | 1169 |
by (simp add : word_of_int_power_hom [symmetric]) |
1170 |
||
1171 |
||
24350 | 1172 |
subsection "Cardinality, finiteness of set of words" |
24333 | 1173 |
|
1174 |
lemmas card_lessThan' = card_lessThan [unfolded lessThan_def] |
|
1175 |
||
1176 |
lemmas card_eq = word_unat.Abs_inj_on [THEN card_image, |
|
1177 |
unfolded word_unat.image, unfolded unats_def, standard] |
|
1178 |
||
1179 |
lemmas card_word = trans [OF card_eq card_lessThan', standard] |
|
1180 |
||
24408 | 1181 |
lemma finite_word_UNIV: "finite (UNIV :: 'a :: finite word set)" |
24333 | 1182 |
apply (rule contrapos_np) |
1183 |
prefer 2 |
|
1184 |
apply (erule card_infinite) |
|
1185 |
apply (simp add : card_word) |
|
1186 |
done |
|
1187 |
||
1188 |
lemma card_word_size: |
|
24408 | 1189 |
"card (UNIV :: 'a :: finite word set) = (2 ^ size (x :: 'a word))" |
24333 | 1190 |
unfolding word_size by (rule card_word) |
1191 |
||
1192 |
end |
|
1193 |