6 the definition of the word type |
6 the definition of the word type |
7 *) |
7 *) |
8 |
8 |
9 header {* Definition of Word Type *} |
9 header {* Definition of Word Type *} |
10 |
10 |
11 theory WordDefinition imports Size BinOperations TdThs begin |
11 theory WordDefinition |
|
12 imports Numeral_Type BinOperations TdThs begin |
12 |
13 |
13 typedef (open word) 'a word |
14 typedef (open word) 'a word |
14 = "{(0::int) ..< 2^len_of TYPE('a::len0)}" by auto |
15 = "{(0::int) ..< 2^CARD('a)}" by auto |
15 |
16 |
16 instance word :: (len0) number .. |
17 instance word :: (type) number .. |
17 instance word :: (type) minus .. |
18 instance word :: (type) minus .. |
18 instance word :: (type) plus .. |
19 instance word :: (type) plus .. |
19 instance word :: (type) one .. |
20 instance word :: (type) one .. |
20 instance word :: (type) zero .. |
21 instance word :: (type) zero .. |
21 instance word :: (type) times .. |
22 instance word :: (type) times .. |
28 subsection "Type conversions and casting" |
29 subsection "Type conversions and casting" |
29 |
30 |
30 constdefs |
31 constdefs |
31 -- {* representation of words using unsigned or signed bins, |
32 -- {* representation of words using unsigned or signed bins, |
32 only difference in these is the type class *} |
33 only difference in these is the type class *} |
33 word_of_int :: "int => 'a :: len0 word" |
34 word_of_int :: "int => 'a word" |
34 "word_of_int w == Abs_word (bintrunc (len_of TYPE ('a)) w)" |
35 "word_of_int w == Abs_word (bintrunc CARD('a) w)" |
35 |
36 |
36 -- {* uint and sint cast a word to an integer, |
37 -- {* uint and sint cast a word to an integer, |
37 uint treats the word as unsigned, |
38 uint treats the word as unsigned, |
38 sint treats the most-significant-bit as a sign bit *} |
39 sint treats the most-significant-bit as a sign bit *} |
39 uint :: "'a :: len0 word => int" |
40 uint :: "'a word => int" |
40 "uint w == Rep_word w" |
41 "uint w == Rep_word w" |
41 sint :: "'a :: len word => int" |
42 sint :: "'a :: finite word => int" |
42 sint_uint: "sint w == sbintrunc (len_of TYPE ('a) - 1) (uint w)" |
43 sint_uint: "sint w == sbintrunc (CARD('a) - 1) (uint w)" |
43 unat :: "'a :: len0 word => nat" |
44 unat :: "'a word => nat" |
44 "unat w == nat (uint w)" |
45 "unat w == nat (uint w)" |
45 |
46 |
46 -- "the sets of integers representing the words" |
47 -- "the sets of integers representing the words" |
47 uints :: "nat => int set" |
48 uints :: "nat => int set" |
48 "uints n == range (bintrunc n)" |
49 "uints n == range (bintrunc n)" |
96 |
97 |
97 subsection "Bit-wise operations" |
98 subsection "Bit-wise operations" |
98 |
99 |
99 defs (overloaded) |
100 defs (overloaded) |
100 word_and_def: |
101 word_and_def: |
101 "(a::'a::len0 word) AND b == word_of_int (uint a AND uint b)" |
102 "(a::'a word) AND b == word_of_int (uint a AND uint b)" |
102 |
103 |
103 word_or_def: |
104 word_or_def: |
104 "(a::'a::len0 word) OR b == word_of_int (uint a OR uint b)" |
105 "(a::'a word) OR b == word_of_int (uint a OR uint b)" |
105 |
106 |
106 word_xor_def: |
107 word_xor_def: |
107 "(a::'a::len0 word) XOR b == word_of_int (uint a XOR uint b)" |
108 "(a::'a word) XOR b == word_of_int (uint a XOR uint b)" |
108 |
109 |
109 word_not_def: |
110 word_not_def: |
110 "NOT (a::'a::len0 word) == word_of_int (NOT (uint a))" |
111 "NOT (a::'a word) == word_of_int (NOT (uint a))" |
111 |
112 |
112 word_test_bit_def: |
113 word_test_bit_def: |
113 "test_bit (a::'a::len0 word) == bin_nth (uint a)" |
114 "test_bit (a::'a word) == bin_nth (uint a)" |
114 |
115 |
115 word_set_bit_def: |
116 word_set_bit_def: |
116 "set_bit (a::'a::len0 word) n x == |
117 "set_bit (a::'a word) n x == |
117 word_of_int (bin_sc n (If x bit.B1 bit.B0) (uint a))" |
118 word_of_int (bin_sc n (If x bit.B1 bit.B0) (uint a))" |
118 |
119 |
119 word_lsb_def: |
120 word_lsb_def: |
120 "lsb (a::'a::len0 word) == bin_last (uint a) = bit.B1" |
121 "lsb (a::'a word) == bin_last (uint a) = bit.B1" |
121 |
122 |
122 word_msb_def: |
123 word_msb_def: |
123 "msb (a::'a::len word) == bin_sign (sint a) = Numeral.Min" |
124 "msb (a::'a::finite word) == bin_sign (sint a) = Numeral.Min" |
124 |
125 |
125 |
126 |
126 constdefs |
127 constdefs |
127 setBit :: "'a :: len0 word => nat => 'a word" |
128 setBit :: "'a word => nat => 'a word" |
128 "setBit w n == set_bit w n True" |
129 "setBit w n == set_bit w n True" |
129 |
130 |
130 clearBit :: "'a :: len0 word => nat => 'a word" |
131 clearBit :: "'a word => nat => 'a word" |
131 "clearBit w n == set_bit w n False" |
132 "clearBit w n == set_bit w n False" |
132 |
133 |
133 |
134 |
134 constdefs |
135 constdefs |
135 -- "Largest representable machine integer." |
136 -- "Largest representable machine integer." |
136 max_word :: "'a::len word" |
137 max_word :: "'a::finite word" |
137 "max_word \<equiv> word_of_int (2^len_of TYPE('a) - 1)" |
138 "max_word \<equiv> word_of_int (2^CARD('a) - 1)" |
138 |
139 |
139 consts |
140 consts |
140 of_bool :: "bool \<Rightarrow> 'a::len word" |
141 of_bool :: "bool \<Rightarrow> 'a::finite word" |
141 primrec |
142 primrec |
142 "of_bool False = 0" |
143 "of_bool False = 0" |
143 "of_bool True = 1" |
144 "of_bool True = 1" |
144 |
145 |
145 |
146 |
146 |
147 |
147 lemmas word_size_gt_0 [iff] = |
148 lemmas word_size_gt_0 [iff] = |
148 xtr1 [OF word_size [THEN meta_eq_to_obj_eq] len_gt_0, standard] |
149 xtr1 [OF word_size [THEN meta_eq_to_obj_eq] zero_less_card_finite, standard] |
149 lemmas lens_gt_0 = word_size_gt_0 len_gt_0 |
150 lemmas lens_gt_0 = word_size_gt_0 zero_less_card_finite |
150 lemmas lens_not_0 [iff] = lens_gt_0 [THEN gr_implies_not0, standard] |
151 lemmas lens_not_0 [iff] = lens_gt_0 [THEN gr_implies_not0, standard] |
151 |
152 |
152 lemma uints_num: "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}" |
153 lemma uints_num: "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}" |
153 by (simp add: uints_def range_bintrunc) |
154 by (simp add: uints_def range_bintrunc) |
154 |
155 |
161 lemma mod_in_reps: "m > 0 ==> y mod m : {0::int ..< m}" |
162 lemma mod_in_reps: "m > 0 ==> y mod m : {0::int ..< m}" |
162 unfolding atLeastLessThan_alt by auto |
163 unfolding atLeastLessThan_alt by auto |
163 |
164 |
164 lemma |
165 lemma |
165 Rep_word_0:"0 <= Rep_word x" and |
166 Rep_word_0:"0 <= Rep_word x" and |
166 Rep_word_lt: "Rep_word (x::'a::len0 word) < 2 ^ len_of TYPE('a)" |
167 Rep_word_lt: "Rep_word (x::'a word) < 2 ^ CARD('a)" |
167 by (auto simp: Rep_word [simplified]) |
168 by (auto simp: Rep_word [simplified]) |
168 |
169 |
169 lemma Rep_word_mod_same: |
170 lemma Rep_word_mod_same: |
170 "Rep_word x mod 2 ^ len_of TYPE('a) = Rep_word (x::'a::len0 word)" |
171 "Rep_word x mod 2 ^ CARD('a) = Rep_word (x::'a word)" |
171 by (simp add: int_mod_eq Rep_word_lt Rep_word_0) |
172 by (simp add: int_mod_eq Rep_word_lt Rep_word_0) |
172 |
173 |
173 lemma td_ext_uint: |
174 lemma td_ext_uint: |
174 "td_ext (uint :: 'a word => int) word_of_int (uints (len_of TYPE('a::len0))) |
175 "td_ext (uint :: 'a word => int) word_of_int (uints CARD('a)) |
175 (%w::int. w mod 2 ^ len_of TYPE('a))" |
176 (%w::int. w mod 2 ^ CARD('a))" |
176 apply (unfold td_ext_def') |
177 apply (unfold td_ext_def') |
177 apply (simp add: uints_num uint_def word_of_int_def bintrunc_mod2p) |
178 apply (simp add: uints_num uint_def word_of_int_def bintrunc_mod2p) |
178 apply (simp add: Rep_word_mod_same Rep_word_0 Rep_word_lt |
179 apply (simp add: Rep_word_mod_same Rep_word_0 Rep_word_lt |
179 word.Rep_word_inverse word.Abs_word_inverse int_mod_lem) |
180 word.Rep_word_inverse word.Abs_word_inverse int_mod_lem) |
180 done |
181 done |
181 |
182 |
182 lemmas int_word_uint = td_ext_uint [THEN td_ext.eq_norm, standard] |
183 lemmas int_word_uint = td_ext_uint [THEN td_ext.eq_norm, standard] |
183 |
184 |
184 interpretation word_uint: |
185 interpretation word_uint: |
185 td_ext ["uint::'a::len0 word \<Rightarrow> int" |
186 td_ext ["uint::'a word \<Rightarrow> int" |
186 word_of_int |
187 word_of_int |
187 "uints (len_of TYPE('a::len0))" |
188 "uints CARD('a)" |
188 "\<lambda>w. w mod 2 ^ len_of TYPE('a::len0)"] |
189 "\<lambda>w. w mod 2 ^ CARD('a)"] |
189 by (rule td_ext_uint) |
190 by (rule td_ext_uint) |
190 |
191 |
191 lemmas td_uint = word_uint.td_thm |
192 lemmas td_uint = word_uint.td_thm |
192 |
193 |
193 lemmas td_ext_ubin = td_ext_uint |
194 lemmas td_ext_ubin = td_ext_uint |
194 [simplified len_gt_0 no_bintr_alt1 [symmetric]] |
195 [simplified zero_less_card_finite no_bintr_alt1 [symmetric]] |
195 |
196 |
196 interpretation word_ubin: |
197 interpretation word_ubin: |
197 td_ext ["uint::'a::len0 word \<Rightarrow> int" |
198 td_ext ["uint::'a word \<Rightarrow> int" |
198 word_of_int |
199 word_of_int |
199 "uints (len_of TYPE('a::len0))" |
200 "uints CARD('a)" |
200 "bintrunc (len_of TYPE('a::len0))"] |
201 "bintrunc CARD('a)"] |
201 by (rule td_ext_ubin) |
202 by (rule td_ext_ubin) |
202 |
203 |
203 lemma sint_sbintrunc': |
204 lemma sint_sbintrunc': |
204 "sint (word_of_int bin :: 'a word) = |
205 "sint (word_of_int bin :: 'a word) = |
205 (sbintrunc (len_of TYPE ('a :: len) - 1) bin)" |
206 (sbintrunc (CARD('a :: finite) - 1) bin)" |
206 unfolding sint_uint |
207 unfolding sint_uint |
207 by (auto simp: word_ubin.eq_norm sbintrunc_bintrunc_lt) |
208 by (auto simp: word_ubin.eq_norm sbintrunc_bintrunc_lt) |
208 |
209 |
209 lemma uint_sint: |
210 lemma uint_sint: |
210 "uint w = bintrunc (len_of TYPE('a)) (sint (w :: 'a :: len word))" |
211 "uint w = bintrunc CARD('a) (sint (w :: 'a :: finite word))" |
211 unfolding sint_uint by (auto simp: bintrunc_sbintrunc_le) |
212 unfolding sint_uint by (auto simp: bintrunc_sbintrunc_le) |
|
213 |
212 |
214 |
213 lemma bintr_uint': |
215 lemma bintr_uint': |
214 "n >= size w ==> bintrunc n (uint w) = uint w" |
216 "n >= size w ==> bintrunc n (uint w) = uint w" |
215 apply (unfold word_size) |
217 apply (unfold word_size) |
216 apply (subst word_ubin.norm_Rep [symmetric]) |
218 apply (subst word_ubin.norm_Rep [symmetric]) |
226 |
228 |
227 lemmas bintr_uint = bintr_uint' [unfolded word_size] |
229 lemmas bintr_uint = bintr_uint' [unfolded word_size] |
228 lemmas wi_bintr = wi_bintr' [unfolded word_size] |
230 lemmas wi_bintr = wi_bintr' [unfolded word_size] |
229 |
231 |
230 lemma td_ext_sbin: |
232 lemma td_ext_sbin: |
231 "td_ext (sint :: 'a word => int) word_of_int (sints (len_of TYPE('a::len))) |
233 "td_ext (sint :: 'a word => int) word_of_int (sints CARD('a::finite)) |
232 (sbintrunc (len_of TYPE('a) - 1))" |
234 (sbintrunc (CARD('a) - 1))" |
233 apply (unfold td_ext_def' sint_uint) |
235 apply (unfold td_ext_def' sint_uint) |
234 apply (simp add : word_ubin.eq_norm) |
236 apply (simp add : word_ubin.eq_norm) |
235 apply (cases "len_of TYPE('a)") |
237 apply (cases "CARD('a)") |
236 apply (auto simp add : sints_def) |
238 apply (auto simp add : sints_def) |
237 apply (rule sym [THEN trans]) |
239 apply (rule sym [THEN trans]) |
238 apply (rule word_ubin.Abs_norm) |
240 apply (rule word_ubin.Abs_norm) |
239 apply (simp only: bintrunc_sbintrunc) |
241 apply (simp only: bintrunc_sbintrunc) |
240 apply (drule sym) |
242 apply (drule sym) |
241 apply simp |
243 apply simp |
242 done |
244 done |
243 |
245 |
244 lemmas td_ext_sint = td_ext_sbin |
246 lemmas td_ext_sint = td_ext_sbin |
245 [simplified len_gt_0 no_sbintr_alt2 Suc_pred' [symmetric]] |
247 [simplified zero_less_card_finite no_sbintr_alt2 Suc_pred' [symmetric]] |
246 |
248 |
247 (* We do sint before sbin, before sint is the user version |
249 (* We do sint before sbin, before sint is the user version |
248 and interpretations do not produce thm duplicates. I.e. |
250 and interpretations do not produce thm duplicates. I.e. |
249 we get the name word_sint.Rep_eqD, but not word_sbin.Req_eqD, |
251 we get the name word_sint.Rep_eqD, but not word_sbin.Req_eqD, |
250 because the latter is the same thm as the former *) |
252 because the latter is the same thm as the former *) |
251 interpretation word_sint: |
253 interpretation word_sint: |
252 td_ext ["sint ::'a::len word => int" |
254 td_ext ["sint ::'a::finite word => int" |
253 word_of_int |
255 word_of_int |
254 "sints (len_of TYPE('a::len))" |
256 "sints CARD('a::finite)" |
255 "%w. (w + 2^(len_of TYPE('a::len) - 1)) mod 2^len_of TYPE('a::len) - |
257 "%w. (w + 2^(CARD('a::finite) - 1)) mod 2^CARD('a::finite) - |
256 2 ^ (len_of TYPE('a::len) - 1)"] |
258 2 ^ (CARD('a::finite) - 1)"] |
257 by (rule td_ext_sint) |
259 by (rule td_ext_sint) |
258 |
260 |
259 interpretation word_sbin: |
261 interpretation word_sbin: |
260 td_ext ["sint ::'a::len word => int" |
262 td_ext ["sint ::'a::finite word => int" |
261 word_of_int |
263 word_of_int |
262 "sints (len_of TYPE('a::len))" |
264 "sints CARD('a::finite)" |
263 "sbintrunc (len_of TYPE('a::len) - 1)"] |
265 "sbintrunc (CARD('a::finite) - 1)"] |
264 by (rule td_ext_sbin) |
266 by (rule td_ext_sbin) |
265 |
267 |
266 lemmas int_word_sint = td_ext_sint [THEN td_ext.eq_norm, standard] |
268 lemmas int_word_sint = td_ext_sint [THEN td_ext.eq_norm, standard] |
267 |
269 |
268 lemmas td_sint = word_sint.td |
270 lemmas td_sint = word_sint.td |
274 by (auto simp: word_number_of_def intro: ext) |
276 by (auto simp: word_number_of_def intro: ext) |
275 |
277 |
276 lemmas uints_mod = uints_def [unfolded no_bintr_alt1] |
278 lemmas uints_mod = uints_def [unfolded no_bintr_alt1] |
277 |
279 |
278 lemma uint_bintrunc: "uint (number_of bin :: 'a word) = |
280 lemma uint_bintrunc: "uint (number_of bin :: 'a word) = |
279 number_of (bintrunc (len_of TYPE ('a :: len0)) bin)" |
281 number_of (bintrunc CARD('a) bin)" |
280 unfolding word_number_of_def number_of_eq |
282 unfolding word_number_of_def number_of_eq |
281 by (auto intro: word_ubin.eq_norm) |
283 by (auto intro: word_ubin.eq_norm) |
282 |
284 |
283 lemma sint_sbintrunc: "sint (number_of bin :: 'a word) = |
285 lemma sint_sbintrunc: "sint (number_of bin :: 'a word) = |
284 number_of (sbintrunc (len_of TYPE ('a :: len) - 1) bin)" |
286 number_of (sbintrunc (CARD('a :: finite) - 1) bin)" |
285 unfolding word_number_of_def number_of_eq |
287 unfolding word_number_of_def number_of_eq |
286 by (auto intro!: word_sbin.eq_norm simp del: one_is_Suc_zero) |
288 by (auto intro!: word_sbin.eq_norm simp del: one_is_Suc_zero) |
287 |
289 |
288 lemma unat_bintrunc: |
290 lemma unat_bintrunc: |
289 "unat (number_of bin :: 'a :: len0 word) = |
291 "unat (number_of bin :: 'a word) = |
290 number_of (bintrunc (len_of TYPE('a)) bin)" |
292 number_of (bintrunc CARD('a) bin)" |
291 unfolding unat_def nat_number_of_def |
293 unfolding unat_def nat_number_of_def |
292 by (simp only: uint_bintrunc) |
294 by (simp only: uint_bintrunc) |
293 |
295 |
294 (* WARNING - these may not always be helpful *) |
296 (* WARNING - these may not always be helpful *) |
295 declare |
297 declare |
296 uint_bintrunc [simp] |
298 uint_bintrunc [simp] |
297 sint_sbintrunc [simp] |
299 sint_sbintrunc [simp] |
298 unat_bintrunc [simp] |
300 unat_bintrunc [simp] |
299 |
301 |
300 lemma size_0_eq: "size (w :: 'a :: len0 word) = 0 ==> v = w" |
302 lemma size_0_eq: "size (w :: 'a word) = 0 ==> v = w" |
301 apply (unfold word_size) |
303 apply (unfold word_size) |
302 apply (rule word_uint.Rep_eqD) |
304 apply (rule word_uint.Rep_eqD) |
303 apply (rule box_equals) |
305 apply (rule box_equals) |
304 defer |
306 defer |
305 apply (rule word_ubin.norm_Rep)+ |
307 apply (rule word_ubin.norm_Rep)+ |
320 lemmas uint_m2p_neg = iffD2 [OF diff_less_0_iff_less uint_lt2p, standard] |
322 lemmas uint_m2p_neg = iffD2 [OF diff_less_0_iff_less uint_lt2p, standard] |
321 lemmas uint_m2p_not_non_neg = |
323 lemmas uint_m2p_not_non_neg = |
322 iffD2 [OF linorder_not_le uint_m2p_neg, standard] |
324 iffD2 [OF linorder_not_le uint_m2p_neg, standard] |
323 |
325 |
324 lemma lt2p_lem: |
326 lemma lt2p_lem: |
325 "len_of TYPE('a) <= n ==> uint (w :: 'a :: len0 word) < 2 ^ n" |
327 "CARD('a) <= n ==> uint (w :: 'a word) < 2 ^ n" |
326 by (rule xtr8 [OF _ uint_lt2p]) simp |
328 by (rule xtr8 [OF _ uint_lt2p]) simp |
327 |
329 |
328 lemmas uint_le_0_iff [simp] = |
330 lemmas uint_le_0_iff [simp] = |
329 uint_ge_0 [THEN leD, THEN linorder_antisym_conv1, standard] |
331 uint_ge_0 [THEN leD, THEN linorder_antisym_conv1, standard] |
330 |
332 |
331 lemma uint_nat: "uint w == int (unat w)" |
333 lemma uint_nat: "uint w == int (unat w)" |
332 unfolding unat_def by auto |
334 unfolding unat_def by auto |
333 |
335 |
334 lemma uint_number_of: |
336 lemma uint_number_of: |
335 "uint (number_of b :: 'a :: len0 word) = number_of b mod 2 ^ len_of TYPE('a)" |
337 "uint (number_of b :: 'a word) = number_of b mod 2 ^ CARD('a)" |
336 unfolding word_number_of_alt |
338 unfolding word_number_of_alt |
337 by (simp only: int_word_uint) |
339 by (simp only: int_word_uint) |
338 |
340 |
339 lemma unat_number_of: |
341 lemma unat_number_of: |
340 "bin_sign b = Numeral.Pls ==> |
342 "bin_sign b = Numeral.Pls ==> |
341 unat (number_of b::'a::len0 word) = number_of b mod 2 ^ len_of TYPE ('a)" |
343 unat (number_of b::'a word) = number_of b mod 2 ^ CARD('a)" |
342 apply (unfold unat_def) |
344 apply (unfold unat_def) |
343 apply (clarsimp simp only: uint_number_of) |
345 apply (clarsimp simp only: uint_number_of) |
344 apply (rule nat_mod_distrib [THEN trans]) |
346 apply (rule nat_mod_distrib [THEN trans]) |
345 apply (erule sign_Pls_ge_0 [THEN iffD1]) |
347 apply (erule sign_Pls_ge_0 [THEN iffD1]) |
346 apply (simp_all add: nat_power_eq) |
348 apply (simp_all add: nat_power_eq) |
347 done |
349 done |
348 |
350 |
349 lemma sint_number_of: "sint (number_of b :: 'a :: len word) = (number_of b + |
351 lemma sint_number_of: "sint (number_of b :: 'a :: finite word) = (number_of b + |
350 2 ^ (len_of TYPE('a) - 1)) mod 2 ^ len_of TYPE('a) - |
352 2 ^ (CARD('a) - 1)) mod 2 ^ CARD('a) - |
351 2 ^ (len_of TYPE('a) - 1)" |
353 2 ^ (CARD('a) - 1)" |
352 unfolding word_number_of_alt by (rule int_word_sint) |
354 unfolding word_number_of_alt by (rule int_word_sint) |
353 |
355 |
354 lemma word_of_int_bin [simp] : |
356 lemma word_of_int_bin [simp] : |
355 "(word_of_int (number_of bin) :: 'a :: len0 word) = (number_of bin)" |
357 "(word_of_int (number_of bin) :: 'a word) = (number_of bin)" |
356 unfolding word_number_of_alt by auto |
358 unfolding word_number_of_alt by auto |
357 |
359 |
358 lemma word_int_case_wi: |
360 lemma word_int_case_wi: |
359 "word_int_case f (word_of_int i :: 'b word) = |
361 "word_int_case f (word_of_int i :: 'b word) = |
360 f (i mod 2 ^ len_of TYPE('b::len0))" |
362 f (i mod 2 ^ CARD('b))" |
361 unfolding word_int_case_def by (simp add: word_uint.eq_norm) |
363 unfolding word_int_case_def by (simp add: word_uint.eq_norm) |
362 |
364 |
363 lemma word_int_split: |
365 lemma word_int_split: |
364 "P (word_int_case f x) = |
366 "P (word_int_case f x) = |
365 (ALL i. x = (word_of_int i :: 'b :: len0 word) & |
367 (ALL i. x = (word_of_int i :: 'b word) & |
366 0 <= i & i < 2 ^ len_of TYPE('b) --> P (f i))" |
368 0 <= i & i < 2 ^ CARD('b) --> P (f i))" |
367 unfolding word_int_case_def |
369 unfolding word_int_case_def |
368 by (auto simp: word_uint.eq_norm int_mod_eq') |
370 by (auto simp: word_uint.eq_norm int_mod_eq') |
369 |
371 |
370 lemma word_int_split_asm: |
372 lemma word_int_split_asm: |
371 "P (word_int_case f x) = |
373 "P (word_int_case f x) = |
372 (~ (EX n. x = (word_of_int n :: 'b::len0 word) & |
374 (~ (EX n. x = (word_of_int n :: 'b word) & |
373 0 <= n & n < 2 ^ len_of TYPE('b::len0) & ~ P (f n)))" |
375 0 <= n & n < 2 ^ CARD('b) & ~ P (f n)))" |
374 unfolding word_int_case_def |
376 unfolding word_int_case_def |
375 by (auto simp: word_uint.eq_norm int_mod_eq') |
377 by (auto simp: word_uint.eq_norm int_mod_eq') |
376 |
378 |
377 lemmas uint_range' = |
379 lemmas uint_range' = |
378 word_uint.Rep [unfolded uints_num mem_Collect_eq, standard] |
380 word_uint.Rep [unfolded uints_num mem_Collect_eq, standard] |
390 [THEN conjunct2, THEN [2] xtr8, folded One_nat_def, standard] |
392 [THEN conjunct2, THEN [2] xtr8, folded One_nat_def, standard] |
391 |
393 |
392 lemmas sint_below_size = sint_range_size |
394 lemmas sint_below_size = sint_range_size |
393 [THEN conjunct1, THEN [2] order_trans, folded One_nat_def, standard] |
395 [THEN conjunct1, THEN [2] order_trans, folded One_nat_def, standard] |
394 |
396 |
395 lemma test_bit_eq_iff: "(test_bit (u::'a::len0 word) = test_bit v) = (u = v)" |
397 lemma test_bit_eq_iff: "(test_bit (u::'a word) = test_bit v) = (u = v)" |
396 unfolding word_test_bit_def by (simp add: bin_nth_eq_iff) |
398 unfolding word_test_bit_def by (simp add: bin_nth_eq_iff) |
397 |
399 |
398 lemma test_bit_size [rule_format] : "(w::'a::len0 word) !! n --> n < size w" |
400 lemma test_bit_size [rule_format] : "(w::'a word) !! n --> n < size w" |
399 apply (unfold word_test_bit_def) |
401 apply (unfold word_test_bit_def) |
400 apply (subst word_ubin.norm_Rep [symmetric]) |
402 apply (subst word_ubin.norm_Rep [symmetric]) |
401 apply (simp only: nth_bintr word_size) |
403 apply (simp only: nth_bintr word_size) |
402 apply fast |
404 apply fast |
403 done |
405 done |
404 |
406 |
405 lemma word_eqI [rule_format] : |
407 lemma word_eqI [rule_format] : |
406 fixes u :: "'a::len0 word" |
408 fixes u :: "'a word" |
407 shows "(ALL n. n < size u --> u !! n = v !! n) ==> u = v" |
409 shows "(ALL n. n < size u --> u !! n = v !! n) ==> u = v" |
408 apply (rule test_bit_eq_iff [THEN iffD1]) |
410 apply (rule test_bit_eq_iff [THEN iffD1]) |
409 apply (rule ext) |
411 apply (rule ext) |
410 apply (erule allE) |
412 apply (erule allE) |
411 apply (erule impCE) |
413 apply (erule impCE) |
473 |
475 |
474 (* don't add these to simpset, since may want bintrunc n w to be simplified; |
476 (* don't add these to simpset, since may want bintrunc n w to be simplified; |
475 may want these in reverse, but loop as simp rules, so use following *) |
477 may want these in reverse, but loop as simp rules, so use following *) |
476 |
478 |
477 lemma num_of_bintr': |
479 lemma num_of_bintr': |
478 "bintrunc (len_of TYPE('a :: len0)) a = b ==> |
480 "bintrunc CARD('a) a = b ==> |
479 number_of a = (number_of b :: 'a word)" |
481 number_of a = (number_of b :: 'a word)" |
480 apply safe |
482 apply safe |
481 apply (rule_tac num_of_bintr [symmetric]) |
483 apply (rule_tac num_of_bintr [symmetric]) |
482 done |
484 done |
483 |
485 |
484 lemma num_of_sbintr': |
486 lemma num_of_sbintr': |
485 "sbintrunc (len_of TYPE('a :: len) - 1) a = b ==> |
487 "sbintrunc (CARD('a :: finite) - 1) a = b ==> |
486 number_of a = (number_of b :: 'a word)" |
488 number_of a = (number_of b :: 'a word)" |
487 apply safe |
489 apply safe |
488 apply (rule_tac num_of_sbintr [symmetric]) |
490 apply (rule_tac num_of_sbintr [symmetric]) |
489 done |
491 done |
490 |
492 |
501 |
503 |
502 subsection {* Casting words to different lengths *} |
504 subsection {* Casting words to different lengths *} |
503 |
505 |
504 constdefs |
506 constdefs |
505 -- "cast a word to a different length" |
507 -- "cast a word to a different length" |
506 scast :: "'a :: len word => 'b :: len word" |
508 scast :: "'a :: finite word => 'b :: finite word" |
507 "scast w == word_of_int (sint w)" |
509 "scast w == word_of_int (sint w)" |
508 ucast :: "'a :: len0 word => 'b :: len0 word" |
510 ucast :: "'a word => 'b word" |
509 "ucast w == word_of_int (uint w)" |
511 "ucast w == word_of_int (uint w)" |
510 |
512 |
511 -- "whether a cast (or other) function is to a longer or shorter length" |
513 -- "whether a cast (or other) function is to a longer or shorter length" |
512 source_size :: "('a :: len0 word => 'b) => nat" |
514 source_size :: "('a word => 'b) => nat" |
513 "source_size c == let arb = arbitrary ; x = c arb in size arb" |
515 "source_size c == let arb = arbitrary ; x = c arb in size arb" |
514 target_size :: "('a => 'b :: len0 word) => nat" |
516 target_size :: "('a => 'b word) => nat" |
515 "target_size c == size (c arbitrary)" |
517 "target_size c == size (c arbitrary)" |
516 is_up :: "('a :: len0 word => 'b :: len0 word) => bool" |
518 is_up :: "('a word => 'b word) => bool" |
517 "is_up c == source_size c <= target_size c" |
519 "is_up c == source_size c <= target_size c" |
518 is_down :: "('a :: len0 word => 'b :: len0 word) => bool" |
520 is_down :: "('a word => 'b word) => bool" |
519 "is_down c == target_size c <= source_size c" |
521 "is_down c == target_size c <= source_size c" |
520 |
522 |
521 (** cast - note, no arg for new length, as it's determined by type of result, |
523 (** cast - note, no arg for new length, as it's determined by type of result, |
522 thus in "cast w = w, the type means cast to length of w! **) |
524 thus in "cast w = w, the type means cast to length of w! **) |
523 |
525 |
526 |
528 |
527 lemma scast_id: "scast w = w" |
529 lemma scast_id: "scast w = w" |
528 unfolding scast_def by auto |
530 unfolding scast_def by auto |
529 |
531 |
530 lemma nth_ucast: |
532 lemma nth_ucast: |
531 "(ucast w::'a::len0 word) !! n = (w !! n & n < len_of TYPE('a))" |
533 "(ucast w::'a word) !! n = (w !! n & n < CARD('a))" |
532 apply (unfold ucast_def test_bit_bin) |
534 apply (unfold ucast_def test_bit_bin) |
533 apply (simp add: word_ubin.eq_norm nth_bintr word_size) |
535 apply (simp add: word_ubin.eq_norm nth_bintr word_size) |
534 apply (fast elim!: bin_nth_uint_imp) |
536 apply (fast elim!: bin_nth_uint_imp) |
535 done |
537 done |
536 |
538 |
537 (* for literal u(s)cast *) |
539 (* for literal u(s)cast *) |
538 |
540 |
539 lemma ucast_bintr [simp]: |
541 lemma ucast_bintr [simp]: |
540 "ucast (number_of w ::'a::len0 word) = |
542 "ucast (number_of w ::'a word) = |
541 number_of (bintrunc (len_of TYPE('a)) w)" |
543 number_of (bintrunc CARD('a) w)" |
542 unfolding ucast_def by simp |
544 unfolding ucast_def by simp |
543 |
545 |
544 lemma scast_sbintr [simp]: |
546 lemma scast_sbintr [simp]: |
545 "scast (number_of w ::'a::len word) = |
547 "scast (number_of w ::'a::finite word) = |
546 number_of (sbintrunc (len_of TYPE('a) - Suc 0) w)" |
548 number_of (sbintrunc (CARD('a) - Suc 0) w)" |
547 unfolding scast_def by simp |
549 unfolding scast_def by simp |
548 |
550 |
549 lemmas source_size = source_size_def [unfolded Let_def word_size] |
551 lemmas source_size = source_size_def [unfolded Let_def word_size] |
550 lemmas target_size = target_size_def [unfolded Let_def word_size] |
552 lemmas target_size = target_size_def [unfolded Let_def word_size] |
551 lemmas is_down = is_down_def [unfolded source_size target_size] |
553 lemmas is_down = is_down_def [unfolded source_size target_size] |
614 lemmas isdus = is_up_down [where c = "scast", THEN iffD2] |
616 lemmas isdus = is_up_down [where c = "scast", THEN iffD2] |
615 lemmas ucast_down_ucast_id = isduu [THEN ucast_up_ucast_id] |
617 lemmas ucast_down_ucast_id = isduu [THEN ucast_up_ucast_id] |
616 lemmas scast_down_scast_id = isdus [THEN ucast_up_ucast_id] |
618 lemmas scast_down_scast_id = isdus [THEN ucast_up_ucast_id] |
617 |
619 |
618 lemma up_ucast_surj: |
620 lemma up_ucast_surj: |
619 "is_up (ucast :: 'b::len0 word => 'a::len0 word) ==> |
621 "is_up (ucast :: 'b word => 'a word) ==> |
620 surj (ucast :: 'a word => 'b word)" |
622 surj (ucast :: 'a word => 'b word)" |
621 by (rule surjI, erule ucast_up_ucast_id) |
623 by (rule surjI, erule ucast_up_ucast_id) |
622 |
624 |
623 lemma up_scast_surj: |
625 lemma up_scast_surj: |
624 "is_up (scast :: 'b::len word => 'a::len word) ==> |
626 "is_up (scast :: 'b::finite word => 'a::finite word) ==> |
625 surj (scast :: 'a word => 'b word)" |
627 surj (scast :: 'a word => 'b word)" |
626 by (rule surjI, erule scast_up_scast_id) |
628 by (rule surjI, erule scast_up_scast_id) |
627 |
629 |
628 lemma down_scast_inj: |
630 lemma down_scast_inj: |
629 "is_down (scast :: 'b::len word => 'a::len word) ==> |
631 "is_down (scast :: 'b::finite word => 'a::finite word) ==> |
630 inj_on (ucast :: 'a word => 'b word) A" |
632 inj_on (ucast :: 'a word => 'b word) A" |
631 by (rule inj_on_inverseI, erule scast_down_scast_id) |
633 by (rule inj_on_inverseI, erule scast_down_scast_id) |
632 |
634 |
633 lemma down_ucast_inj: |
635 lemma down_ucast_inj: |
634 "is_down (ucast :: 'b::len0 word => 'a::len0 word) ==> |
636 "is_down (ucast :: 'b word => 'a word) ==> |
635 inj_on (ucast :: 'a word => 'b word) A" |
637 inj_on (ucast :: 'a word => 'b word) A" |
636 by (rule inj_on_inverseI, erule ucast_down_ucast_id) |
638 by (rule inj_on_inverseI, erule ucast_down_ucast_id) |
637 |
639 |
638 |
640 |
639 lemma ucast_down_no': |
641 lemma ucast_down_no': |