author  wenzelm 
Tue, 10 Jun 2008 19:45:53 +0200  
changeset 27133  e26ed41cc8ea 
parent 26558  7fcc10088e72 
child 27136  06a8f65e32f6 
permissions  rwrr 
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) 

27133  321 
apply (induct_tac n rule: nat_induct) 
24333  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 