author | haftmann |
Fri, 04 Apr 2008 13:40:25 +0200 | |
changeset 26558 | 7fcc10088e72 |
parent 25349 | 0d46bea01741 |
child 27133 | e26ed41cc8ea |
permissions | -rw-r--r-- |
24333 | 1 |
(* Author: Gerwin Klein, Jeremy Dawson |
2 |
$Id$ |
|
3 |
||
4 |
Miscellaneous additional library definitions and lemmas for |
|
5 |
the word type. Instantiation to boolean algebras, definition |
|
6 |
of recursion and induction patterns for words. |
|
7 |
*) |
|
8 |
||
24350 | 9 |
header {* Miscellaneous Library for Words *} |
10 |
||
26558 | 11 |
theory WordGenLib |
12 |
imports WordShift Boolean_Algebra |
|
24333 | 13 |
begin |
14 |
||
15 |
declare of_nat_2p [simp] |
|
16 |
||
17 |
lemma word_int_cases: |
|
24465 | 18 |
"\<lbrakk>\<And>n. \<lbrakk>(x ::'a::len0 word) = word_of_int n; 0 \<le> n; n < 2^len_of TYPE('a)\<rbrakk> \<Longrightarrow> P\<rbrakk> |
24333 | 19 |
\<Longrightarrow> P" |
20 |
by (cases x rule: word_uint.Abs_cases) (simp add: uints_num) |
|
21 |
||
22 |
lemma word_nat_cases [cases type: word]: |
|
24465 | 23 |
"\<lbrakk>\<And>n. \<lbrakk>(x ::'a::len word) = of_nat n; n < 2^len_of TYPE('a)\<rbrakk> \<Longrightarrow> P\<rbrakk> |
24333 | 24 |
\<Longrightarrow> P" |
25 |
by (cases x rule: word_unat.Abs_cases) (simp add: unats_def) |
|
26 |
||
27 |
lemma max_word_eq: |
|
24465 | 28 |
"(max_word::'a::len word) = 2^len_of TYPE('a) - 1" |
24333 | 29 |
by (simp add: max_word_def word_of_int_hom_syms word_of_int_2p) |
30 |
||
31 |
lemma max_word_max [simp,intro!]: |
|
32 |
"n \<le> max_word" |
|
33 |
by (cases n rule: word_int_cases) |
|
34 |
(simp add: max_word_def word_le_def int_word_uint int_mod_eq') |
|
35 |
||
36 |
lemma word_of_int_2p_len: |
|
24465 | 37 |
"word_of_int (2 ^ len_of TYPE('a)) = (0::'a::len0 word)" |
24333 | 38 |
by (subst word_uint.Abs_norm [symmetric]) |
39 |
(simp add: word_of_int_hom_syms) |
|
40 |
||
41 |
lemma word_pow_0: |
|
24465 | 42 |
"(2::'a::len word) ^ len_of TYPE('a) = 0" |
24333 | 43 |
proof - |
24465 | 44 |
have "word_of_int (2 ^ len_of TYPE('a)) = (0::'a word)" |
24333 | 45 |
by (rule word_of_int_2p_len) |
46 |
thus ?thesis by (simp add: word_of_int_2p) |
|
47 |
qed |
|
48 |
||
49 |
lemma max_word_wrap: "x + 1 = 0 \<Longrightarrow> x = max_word" |
|
50 |
apply (simp add: max_word_eq) |
|
51 |
apply uint_arith |
|
52 |
apply auto |
|
53 |
apply (simp add: word_pow_0) |
|
54 |
done |
|
55 |
||
56 |
lemma max_word_minus: |
|
24465 | 57 |
"max_word = (-1::'a::len word)" |
24333 | 58 |
proof - |
59 |
have "-1 + 1 = (0::'a word)" by simp |
|
60 |
thus ?thesis by (rule max_word_wrap [symmetric]) |
|
61 |
qed |
|
62 |
||
63 |
lemma max_word_bl [simp]: |
|
24465 | 64 |
"to_bl (max_word::'a::len word) = replicate (len_of TYPE('a)) True" |
24333 | 65 |
by (subst max_word_minus to_bl_n1)+ simp |
66 |
||
67 |
lemma max_test_bit [simp]: |
|
24465 | 68 |
"(max_word::'a::len word) !! n = (n < len_of TYPE('a))" |
24333 | 69 |
by (auto simp add: test_bit_bl word_size) |
70 |
||
71 |
lemma word_and_max [simp]: |
|
72 |
"x AND max_word = x" |
|
73 |
by (rule word_eqI) (simp add: word_ops_nth_size word_size) |
|
74 |
||
75 |
lemma word_or_max [simp]: |
|
76 |
"x OR max_word = max_word" |
|
77 |
by (rule word_eqI) (simp add: word_ops_nth_size word_size) |
|
78 |
||
79 |
lemma word_ao_dist2: |
|
24465 | 80 |
"x AND (y OR z) = x AND y OR x AND (z::'a::len0 word)" |
24333 | 81 |
by (rule word_eqI) (auto simp add: word_ops_nth_size word_size) |
82 |
||
83 |
lemma word_oa_dist2: |
|
24465 | 84 |
"x OR y AND z = (x OR y) AND (x OR (z::'a::len0 word))" |
24333 | 85 |
by (rule word_eqI) (auto simp add: word_ops_nth_size word_size) |
86 |
||
87 |
lemma word_and_not [simp]: |
|
24465 | 88 |
"x AND NOT x = (0::'a::len0 word)" |
24333 | 89 |
by (rule word_eqI) (auto simp add: word_ops_nth_size word_size) |
90 |
||
91 |
lemma word_or_not [simp]: |
|
92 |
"x OR NOT x = max_word" |
|
93 |
by (rule word_eqI) (auto simp add: word_ops_nth_size word_size) |
|
94 |
||
95 |
lemma word_boolean: |
|
96 |
"boolean (op AND) (op OR) bitNOT 0 max_word" |
|
97 |
apply (rule boolean.intro) |
|
98 |
apply (rule word_bw_assocs) |
|
99 |
apply (rule word_bw_assocs) |
|
100 |
apply (rule word_bw_comms) |
|
101 |
apply (rule word_bw_comms) |
|
102 |
apply (rule word_ao_dist2) |
|
103 |
apply (rule word_oa_dist2) |
|
104 |
apply (rule word_and_max) |
|
105 |
apply (rule word_log_esimps) |
|
106 |
apply (rule word_and_not) |
|
107 |
apply (rule word_or_not) |
|
108 |
done |
|
109 |
||
110 |
interpretation word_bool_alg: |
|
111 |
boolean ["op AND" "op OR" bitNOT 0 max_word] |
|
112 |
by (rule word_boolean) |
|
113 |
||
114 |
lemma word_xor_and_or: |
|
24465 | 115 |
"x XOR y = x AND NOT y OR NOT x AND (y::'a::len0 word)" |
24333 | 116 |
by (rule word_eqI) (auto simp add: word_ops_nth_size word_size) |
117 |
||
118 |
interpretation word_bool_alg: |
|
119 |
boolean_xor ["op AND" "op OR" bitNOT 0 max_word "op XOR"] |
|
120 |
apply (rule boolean_xor.intro) |
|
121 |
apply (rule word_boolean) |
|
122 |
apply (rule boolean_xor_axioms.intro) |
|
123 |
apply (rule word_xor_and_or) |
|
124 |
done |
|
125 |
||
126 |
lemma shiftr_0 [iff]: |
|
24465 | 127 |
"(x::'a::len0 word) >> 0 = x" |
24333 | 128 |
by (simp add: shiftr_bl) |
129 |
||
130 |
lemma shiftl_0 [simp]: |
|
24465 | 131 |
"(x :: 'a :: len word) << 0 = x" |
24333 | 132 |
by (simp add: shiftl_t2n) |
133 |
||
134 |
lemma shiftl_1 [simp]: |
|
24465 | 135 |
"(1::'a::len word) << n = 2^n" |
24333 | 136 |
by (simp add: shiftl_t2n) |
137 |
||
138 |
lemma uint_lt_0 [simp]: |
|
139 |
"uint x < 0 = False" |
|
140 |
by (simp add: linorder_not_less) |
|
141 |
||
142 |
lemma shiftr1_1 [simp]: |
|
24465 | 143 |
"shiftr1 (1::'a::len word) = 0" |
24333 | 144 |
by (simp add: shiftr1_def word_0_alt) |
145 |
||
146 |
lemma shiftr_1[simp]: |
|
24465 | 147 |
"(1::'a::len word) >> n = (if n = 0 then 1 else 0)" |
24333 | 148 |
by (induct n) (auto simp: shiftr_def) |
149 |
||
150 |
lemma word_less_1 [simp]: |
|
24465 | 151 |
"((x::'a::len word) < 1) = (x = 0)" |
24333 | 152 |
by (simp add: word_less_nat_alt unat_0_iff) |
153 |
||
154 |
lemma to_bl_mask: |
|
24465 | 155 |
"to_bl (mask n :: 'a::len word) = |
156 |
replicate (len_of TYPE('a) - n) False @ |
|
157 |
replicate (min (len_of TYPE('a)) n) True" |
|
24333 | 158 |
by (simp add: mask_bl word_rep_drop min_def) |
159 |
||
160 |
lemma map_replicate_True: |
|
161 |
"n = length xs ==> |
|
162 |
map (\<lambda>(x,y). x & y) (zip xs (replicate n True)) = xs" |
|
163 |
by (induct xs arbitrary: n) auto |
|
164 |
||
165 |
lemma map_replicate_False: |
|
166 |
"n = length xs ==> map (\<lambda>(x,y). x & y) |
|
167 |
(zip xs (replicate n False)) = replicate n False" |
|
168 |
by (induct xs arbitrary: n) auto |
|
169 |
||
170 |
lemma bl_and_mask: |
|
24465 | 171 |
fixes w :: "'a::len word" |
24333 | 172 |
fixes n |
24465 | 173 |
defines "n' \<equiv> len_of TYPE('a) - n" |
24333 | 174 |
shows "to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)" |
175 |
proof - |
|
176 |
note [simp] = map_replicate_True map_replicate_False |
|
177 |
have "to_bl (w AND mask n) = |
|
26558 | 178 |
map2 op & (to_bl w) (to_bl (mask n::'a::len word))" |
24333 | 179 |
by (simp add: bl_word_and) |
180 |
also |
|
181 |
have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)" by simp |
|
182 |
also |
|
26558 | 183 |
have "map2 op & \<dots> (to_bl (mask n::'a::len word)) = |
24333 | 184 |
replicate n' False @ drop n' (to_bl w)" |
26558 | 185 |
unfolding to_bl_mask n'_def map2_def |
24333 | 186 |
by (subst zip_append) auto |
187 |
finally |
|
188 |
show ?thesis . |
|
189 |
qed |
|
190 |
||
191 |
lemma drop_rev_takefill: |
|
192 |
"length xs \<le> n ==> |
|
193 |
drop (n - length xs) (rev (takefill False n (rev xs))) = xs" |
|
194 |
by (simp add: takefill_alt rev_take) |
|
195 |
||
196 |
lemma map_nth_0 [simp]: |
|
24465 | 197 |
"map (op !! (0::'a::len0 word)) xs = replicate (length xs) False" |
24333 | 198 |
by (induct xs) auto |
199 |
||
200 |
lemma uint_plus_if_size: |
|
201 |
"uint (x + y) = |
|
202 |
(if uint x + uint y < 2^size x then |
|
203 |
uint x + uint y |
|
204 |
else |
|
205 |
uint x + uint y - 2^size x)" |
|
206 |
by (simp add: word_arith_alts int_word_uint mod_add_if_z |
|
207 |
word_size) |
|
208 |
||
209 |
lemma unat_plus_if_size: |
|
24465 | 210 |
"unat (x + (y::'a::len word)) = |
24333 | 211 |
(if unat x + unat y < 2^size x then |
212 |
unat x + unat y |
|
213 |
else |
|
214 |
unat x + unat y - 2^size x)" |
|
215 |
apply (subst word_arith_nat_defs) |
|
216 |
apply (subst unat_of_nat) |
|
217 |
apply (simp add: mod_nat_add word_size) |
|
218 |
done |
|
219 |
||
220 |
lemma word_neq_0_conv [simp]: |
|
24465 | 221 |
fixes w :: "'a :: len word" |
24333 | 222 |
shows "(w \<noteq> 0) = (0 < w)" |
223 |
proof - |
|
224 |
have "0 \<le> w" by (rule word_zero_le) |
|
225 |
thus ?thesis by (auto simp add: word_less_def) |
|
226 |
qed |
|
227 |
||
228 |
lemma max_lt: |
|
24465 | 229 |
"unat (max a b div c) = unat (max a b) div unat (c:: 'a :: len word)" |
24333 | 230 |
apply (subst word_arith_nat_defs) |
231 |
apply (subst word_unat.eq_norm) |
|
232 |
apply (subst mod_if) |
|
233 |
apply clarsimp |
|
234 |
apply (erule notE) |
|
235 |
apply (insert div_le_dividend [of "unat (max a b)" "unat c"]) |
|
236 |
apply (erule order_le_less_trans) |
|
237 |
apply (insert unat_lt2p [of "max a b"]) |
|
238 |
apply simp |
|
239 |
done |
|
240 |
||
241 |
lemma uint_sub_if_size: |
|
242 |
"uint (x - y) = |
|
243 |
(if uint y \<le> uint x then |
|
244 |
uint x - uint y |
|
245 |
else |
|
246 |
uint x - uint y + 2^size x)" |
|
247 |
by (simp add: word_arith_alts int_word_uint mod_sub_if_z |
|
248 |
word_size) |
|
249 |
||
250 |
lemma unat_sub_simple: |
|
251 |
"x \<le> y ==> unat (y - x) = unat y - unat x" |
|
252 |
by (simp add: unat_def uint_sub_if_size word_le_def nat_diff_distrib) |
|
253 |
||
254 |
lemmas unat_sub = unat_sub_simple |
|
255 |
||
256 |
lemma word_less_sub1: |
|
24465 | 257 |
fixes x :: "'a :: len word" |
24333 | 258 |
shows "x \<noteq> 0 ==> 1 < x = (0 < x - 1)" |
259 |
by (simp add: unat_sub_if_size word_less_nat_alt) |
|
260 |
||
261 |
lemma word_le_sub1: |
|
24465 | 262 |
fixes x :: "'a :: len word" |
24333 | 263 |
shows "x \<noteq> 0 ==> 1 \<le> x = (0 \<le> x - 1)" |
264 |
by (simp add: unat_sub_if_size order_le_less word_less_nat_alt) |
|
265 |
||
266 |
lemmas word_less_sub1_numberof [simp] = |
|
25349
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
24465
diff
changeset
|
267 |
word_less_sub1 [of "number_of w", standard] |
24333 | 268 |
lemmas word_le_sub1_numberof [simp] = |
25349
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
24465
diff
changeset
|
269 |
word_le_sub1 [of "number_of w", standard] |
24333 | 270 |
|
271 |
lemma word_of_int_minus: |
|
24465 | 272 |
"word_of_int (2^len_of TYPE('a) - i) = (word_of_int (-i)::'a::len word)" |
24333 | 273 |
proof - |
24465 | 274 |
have x: "2^len_of TYPE('a) - i = -i + 2^len_of TYPE('a)" by simp |
24333 | 275 |
show ?thesis |
276 |
apply (subst x) |
|
277 |
apply (subst word_uint.Abs_norm [symmetric], subst zmod_zadd_self2) |
|
278 |
apply simp |
|
279 |
done |
|
280 |
qed |
|
281 |
||
282 |
lemmas word_of_int_inj = |
|
283 |
word_uint.Abs_inject [unfolded uints_num, simplified] |
|
284 |
||
285 |
lemma word_le_less_eq: |
|
24465 | 286 |
"(x ::'z::len word) \<le> y = (x = y \<or> x < y)" |
24333 | 287 |
by (auto simp add: word_less_def) |
288 |
||
289 |
lemma mod_plus_cong: |
|
290 |
assumes 1: "(b::int) = b'" |
|
291 |
and 2: "x mod b' = x' mod b'" |
|
292 |
and 3: "y mod b' = y' mod b'" |
|
293 |
and 4: "x' + y' = z'" |
|
294 |
shows "(x + y) mod b = z' mod b'" |
|
295 |
proof - |
|
296 |
from 1 2[symmetric] 3[symmetric] have "(x + y) mod b = (x' mod b' + y' mod b') mod b'" |
|
297 |
by (simp add: zmod_zadd1_eq[symmetric]) |
|
298 |
also have "\<dots> = (x' + y') mod b'" |
|
299 |
by (simp add: zmod_zadd1_eq[symmetric]) |
|
300 |
finally show ?thesis by (simp add: 4) |
|
301 |
qed |
|
302 |
||
303 |
lemma mod_minus_cong: |
|
304 |
assumes 1: "(b::int) = b'" |
|
305 |
and 2: "x mod b' = x' mod b'" |
|
306 |
and 3: "y mod b' = y' mod b'" |
|
307 |
and 4: "x' - y' = z'" |
|
308 |
shows "(x - y) mod b = z' mod b'" |
|
309 |
using assms |
|
310 |
apply (subst zmod_zsub_left_eq) |
|
311 |
apply (subst zmod_zsub_right_eq) |
|
312 |
apply (simp add: zmod_zsub_left_eq [symmetric] zmod_zsub_right_eq [symmetric]) |
|
313 |
done |
|
314 |
||
315 |
lemma word_induct_less: |
|
24465 | 316 |
"\<lbrakk>P (0::'a::len word); \<And>n. \<lbrakk>n < m; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m" |
24333 | 317 |
apply (cases m) |
318 |
apply atomize |
|
319 |
apply (erule rev_mp)+ |
|
320 |
apply (rule_tac x=m in spec) |
|
321 |
apply (induct_tac n) |
|
322 |
apply simp |
|
323 |
apply clarsimp |
|
324 |
apply (erule impE) |
|
325 |
apply clarsimp |
|
326 |
apply (erule_tac x=n in allE) |
|
327 |
apply (erule impE) |
|
328 |
apply (simp add: unat_arith_simps) |
|
329 |
apply (clarsimp simp: unat_of_nat) |
|
330 |
apply simp |
|
331 |
apply (erule_tac x="of_nat na" in allE) |
|
332 |
apply (erule impE) |
|
333 |
apply (simp add: unat_arith_simps) |
|
334 |
apply (clarsimp simp: unat_of_nat) |
|
335 |
apply simp |
|
336 |
done |
|
337 |
||
338 |
lemma word_induct: |
|
24465 | 339 |
"\<lbrakk>P (0::'a::len word); \<And>n. P n \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m" |
24333 | 340 |
by (erule word_induct_less, simp) |
341 |
||
342 |
lemma word_induct2 [induct type]: |
|
24465 | 343 |
"\<lbrakk>P 0; \<And>n. \<lbrakk>1 + n \<noteq> 0; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P (n::'b::len word)" |
24333 | 344 |
apply (rule word_induct, simp) |
345 |
apply (case_tac "1+n = 0", auto) |
|
346 |
done |
|
347 |
||
348 |
constdefs |
|
24465 | 349 |
word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a" |
24333 | 350 |
"word_rec forZero forSuc n \<equiv> nat_rec forZero (forSuc \<circ> of_nat) (unat n)" |
351 |
||
352 |
lemma word_rec_0: "word_rec z s 0 = z" |
|
353 |
by (simp add: word_rec_def) |
|
354 |
||
355 |
lemma word_rec_Suc: |
|
24465 | 356 |
"1 + n \<noteq> (0::'a::len word) \<Longrightarrow> word_rec z s (1 + n) = s n (word_rec z s n)" |
24333 | 357 |
apply (simp add: word_rec_def unat_word_ariths) |
358 |
apply (subst nat_mod_eq') |
|
359 |
apply (cut_tac x=n in unat_lt2p) |
|
360 |
apply (drule Suc_mono) |
|
361 |
apply (simp add: less_Suc_eq_le) |
|
362 |
apply (simp only: order_less_le, simp) |
|
363 |
apply (erule contrapos_pn, simp) |
|
364 |
apply (drule arg_cong[where f=of_nat]) |
|
365 |
apply simp |
|
366 |
apply (subst (asm) word_unat.Rep_Abs_A.Rep_inverse[of n]) |
|
367 |
apply simp |
|
368 |
apply simp |
|
369 |
done |
|
370 |
||
371 |
lemma word_rec_Pred: |
|
372 |
"n \<noteq> 0 \<Longrightarrow> word_rec z s n = s (n - 1) (word_rec z s (n - 1))" |
|
373 |
apply (rule subst[where t="n" and s="1 + (n - 1)"]) |
|
374 |
apply simp |
|
375 |
apply (subst word_rec_Suc) |
|
376 |
apply simp |
|
377 |
apply simp |
|
378 |
done |
|
379 |
||
380 |
lemma word_rec_in: |
|
381 |
"f (word_rec z (\<lambda>_. f) n) = word_rec (f z) (\<lambda>_. f) n" |
|
382 |
by (induct n) (simp_all add: word_rec_0 word_rec_Suc) |
|
383 |
||
384 |
lemma word_rec_in2: |
|
385 |
"f n (word_rec z f n) = word_rec (f 0 z) (f \<circ> op + 1) n" |
|
386 |
by (induct n) (simp_all add: word_rec_0 word_rec_Suc) |
|
387 |
||
388 |
lemma word_rec_twice: |
|
389 |
"m \<le> n \<Longrightarrow> word_rec z f n = word_rec (word_rec z f (n - m)) (f \<circ> op + (n - m)) m" |
|
390 |
apply (erule rev_mp) |
|
391 |
apply (rule_tac x=z in spec) |
|
392 |
apply (rule_tac x=f in spec) |
|
393 |
apply (induct n) |
|
394 |
apply (simp add: word_rec_0) |
|
395 |
apply clarsimp |
|
396 |
apply (rule_tac t="1 + n - m" and s="1 + (n - m)" in subst) |
|
397 |
apply simp |
|
398 |
apply (case_tac "1 + (n - m) = 0") |
|
399 |
apply (simp add: word_rec_0) |
|
25349
0d46bea01741
eliminated illegal schematic variables in where/of;
wenzelm
parents:
24465
diff
changeset
|
400 |
apply (rule_tac f = "word_rec ?a ?b" in arg_cong) |
24333 | 401 |
apply (rule_tac t="m" and s="m + (1 + (n - m))" in subst) |
402 |
apply simp |
|
403 |
apply (simp (no_asm_use)) |
|
404 |
apply (simp add: word_rec_Suc word_rec_in2) |
|
405 |
apply (erule impE) |
|
406 |
apply uint_arith |
|
407 |
apply (drule_tac x="x \<circ> op + 1" in spec) |
|
408 |
apply (drule_tac x="x 0 xa" in spec) |
|
409 |
apply simp |
|
410 |
apply (rule_tac t="\<lambda>a. x (1 + (n - m + a))" and s="\<lambda>a. x (1 + (n - m) + a)" |
|
411 |
in subst) |
|
412 |
apply (clarsimp simp add: expand_fun_eq) |
|
413 |
apply (rule_tac t="(1 + (n - m + xb))" and s="1 + (n - m) + xb" in subst) |
|
414 |
apply simp |
|
415 |
apply (rule refl) |
|
416 |
apply (rule refl) |
|
417 |
done |
|
418 |
||
419 |
lemma word_rec_id: "word_rec z (\<lambda>_. id) n = z" |
|
420 |
by (induct n) (auto simp add: word_rec_0 word_rec_Suc) |
|
421 |
||
422 |
lemma word_rec_id_eq: "\<forall>m < n. f m = id \<Longrightarrow> word_rec z f n = z" |
|
423 |
apply (erule rev_mp) |
|
424 |
apply (induct n) |
|
425 |
apply (auto simp add: word_rec_0 word_rec_Suc) |
|
426 |
apply (drule spec, erule mp) |
|
427 |
apply uint_arith |
|
428 |
apply (drule_tac x=n in spec, erule impE) |
|
429 |
apply uint_arith |
|
430 |
apply simp |
|
431 |
done |
|
432 |
||
433 |
lemma word_rec_max: |
|
434 |
"\<forall>m\<ge>n. m \<noteq> -1 \<longrightarrow> f m = id \<Longrightarrow> word_rec z f -1 = word_rec z f n" |
|
435 |
apply (subst word_rec_twice[where n="-1" and m="-1 - n"]) |
|
436 |
apply simp |
|
437 |
apply simp |
|
438 |
apply (rule word_rec_id_eq) |
|
439 |
apply clarsimp |
|
440 |
apply (drule spec, rule mp, erule mp) |
|
441 |
apply (rule word_plus_mono_right2[OF _ order_less_imp_le]) |
|
442 |
prefer 2 |
|
443 |
apply assumption |
|
444 |
apply simp |
|
445 |
apply (erule contrapos_pn) |
|
446 |
apply simp |
|
447 |
apply (drule arg_cong[where f="\<lambda>x. x - n"]) |
|
448 |
apply simp |
|
449 |
done |
|
450 |
||
451 |
lemma unatSuc: |
|
24465 | 452 |
"1 + n \<noteq> (0::'a::len word) \<Longrightarrow> unat (1 + n) = Suc (unat n)" |
24333 | 453 |
by unat_arith |
454 |
||
455 |
end |