author  haftmann 
Thu, 17 Sep 2020 09:57:31 +0000  
changeset 72262  a282abb07642 
parent 72261  5193570b739a 
child 72265  ff32ddc8165c 
permissions  rwrr 
29628  1 
(* Title: HOL/Word/Word.thy 
46124  2 
Author: Jeremy Dawson and Gerwin Klein, NICTA 
24333  3 
*) 
4 

61799  5 
section \<open>A type of finite bit strings\<close> 
24350  6 

29628  7 
theory Word 
41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
41060
diff
changeset

8 
imports 
66453
cc19f7ca2ed6
sessionqualified theory imports: isabelle imports U i d '~~/src/Benchmarks' a;
wenzelm
parents:
65363
diff
changeset

9 
"HOLLibrary.Type_Length" 
cc19f7ca2ed6
sessionqualified theory imports: isabelle imports U i d '~~/src/Benchmarks' a;
wenzelm
parents:
65363
diff
changeset

10 
"HOLLibrary.Boolean_Algebra" 
71957
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71955
diff
changeset

11 
"HOLLibrary.Bit_Operations" 
70190  12 
Bits_Int 
72128  13 
Traditional_Syntax 
70192  14 
Bit_Comprehension 
53062
3af1a6020014
some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory
haftmann
parents:
51717
diff
changeset

15 
Misc_Typedef 
37660  16 
begin 
17 

72243  18 
subsection \<open>Preliminaries\<close> 
19 

20 
lemma signed_take_bit_decr_length_iff: 

21 
\<open>signed_take_bit (LENGTH('a::len)  Suc 0) k = signed_take_bit (LENGTH('a)  Suc 0) l 

22 
\<longleftrightarrow> take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close> 

23 
by (cases \<open>LENGTH('a)\<close>) 

24 
(simp_all add: signed_take_bit_eq_iff_take_bit_eq) 

25 

26 

72244  27 
subsection \<open>Fundamentals\<close> 
28 

29 
subsubsection \<open>Type definition\<close> 

37660  30 

71954
13bb3f5cdc5b
pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
haftmann
parents:
71953
diff
changeset

31 
quotient_type (overloaded) 'a word = int / \<open>\<lambda>k l. take_bit LENGTH('a) k = take_bit LENGTH('a::len) l\<close> 
72243  32 
morphisms rep Word by (auto intro!: equivpI reflpI sympI transpI) 
33 

34 
hide_const (open) rep \<comment> \<open>only for foundational purpose\<close> 

72130
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72128
diff
changeset

35 
hide_const (open) Word \<comment> \<open>only for code generation\<close> 
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72128
diff
changeset

36 

72244  37 

38 
subsubsection \<open>Basic arithmetic\<close> 

39 

72243  40 
instantiation word :: (len) comm_ring_1 
41 
begin 

42 

43 
lift_definition zero_word :: \<open>'a word\<close> 

44 
is 0 . 

45 

46 
lift_definition one_word :: \<open>'a word\<close> 

47 
is 1 . 

48 

49 
lift_definition plus_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close> 

50 
is \<open>(+)\<close> 

51 
by (auto simp add: take_bit_eq_mod intro: mod_add_cong) 

52 

53 
lift_definition minus_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close> 

54 
is \<open>()\<close> 

55 
by (auto simp add: take_bit_eq_mod intro: mod_diff_cong) 

56 

57 
lift_definition uminus_word :: \<open>'a word \<Rightarrow> 'a word\<close> 

58 
is uminus 

59 
by (auto simp add: take_bit_eq_mod intro: mod_minus_cong) 

60 

61 
lift_definition times_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close> 

62 
is \<open>(*)\<close> 

63 
by (auto simp add: take_bit_eq_mod intro: mod_mult_cong) 

64 

65 
instance 

66 
by (standard; transfer) (simp_all add: algebra_simps) 

67 

68 
end 

69 

70 
context 

71 
includes lifting_syntax 

72244  72 
notes 
73 
power_transfer [transfer_rule] 

74 
transfer_rule_of_bool [transfer_rule] 

75 
transfer_rule_numeral [transfer_rule] 

76 
transfer_rule_of_nat [transfer_rule] 

77 
transfer_rule_of_int [transfer_rule] 

78 

72243  79 
begin 
80 

81 
lemma power_transfer_word [transfer_rule]: 

82 
\<open>(pcr_word ===> (=) ===> pcr_word) (^) (^)\<close> 

83 
by transfer_prover 

84 

72244  85 
lemma [transfer_rule]: 
86 
\<open>((=) ===> pcr_word) of_bool of_bool\<close> 

87 
by transfer_prover 

88 

89 
lemma [transfer_rule]: 

90 
\<open>((=) ===> pcr_word) numeral numeral\<close> 

91 
by transfer_prover 

92 

93 
lemma [transfer_rule]: 

94 
\<open>((=) ===> pcr_word) int of_nat\<close> 

95 
by transfer_prover 

96 

97 
lemma [transfer_rule]: 

98 
\<open>((=) ===> pcr_word) (\<lambda>k. k) of_int\<close> 

99 
proof  

100 
have \<open>((=) ===> pcr_word) of_int of_int\<close> 

101 
by transfer_prover 

102 
then show ?thesis by (simp add: id_def) 

103 
qed 

104 

105 
lemma [transfer_rule]: 

106 
\<open>(pcr_word ===> (\<longleftrightarrow>)) even ((dvd) 2 :: 'a::len word \<Rightarrow> bool)\<close> 

107 
proof  

108 
have even_word_unfold: "even k \<longleftrightarrow> (\<exists>l. take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l))" (is "?P \<longleftrightarrow> ?Q") 

109 
for k :: int 

110 
proof 

111 
assume ?P 

112 
then show ?Q 

113 
by auto 

114 
next 

115 
assume ?Q 

116 
then obtain l where "take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l)" .. 

117 
then have "even (take_bit LENGTH('a) k)" 

118 
by simp 

119 
then show ?P 

120 
by simp 

121 
qed 

122 
show ?thesis by (simp only: even_word_unfold [abs_def] dvd_def [where ?'a = "'a word", abs_def]) 

123 
transfer_prover 

124 
qed 

125 

72243  126 
end 
127 

72244  128 
lemma word_exp_length_eq_0 [simp]: 
129 
\<open>(2 :: 'a::len word) ^ LENGTH('a) = 0\<close> 

130 
by transfer simp 

131 

72262  132 
lemma exp_eq_zero_iff: 
133 
\<open>2 ^ n = (0 :: 'a::len word) \<longleftrightarrow> n \<ge> LENGTH('a)\<close> 

134 
by transfer simp 

135 

72244  136 

137 
subsubsection \<open>Basic code generation setup\<close> 

71948
6ede899d26d3
fundamental construction of word type following existing transfer rules
haftmann
parents:
71947
diff
changeset

138 

72262  139 
context 
140 
begin 

141 

142 
qualified lift_definition the_int :: \<open>'a::len word \<Rightarrow> int\<close> 

71948
6ede899d26d3
fundamental construction of word type following existing transfer rules
haftmann
parents:
71947
diff
changeset

143 
is \<open>take_bit LENGTH('a)\<close> . 
37660  144 

72262  145 
end 
146 

72243  147 
lemma [code abstype]: 
72262  148 
\<open>Word.Word (Word.the_int w) = w\<close> 
72243  149 
by transfer simp 
150 

72262  151 
lemma Word_eq_word_of_int [code_post, simp]: 
152 
\<open>Word.Word = of_int\<close> 

153 
by (rule; transfer) simp 

154 

72243  155 
quickcheck_generator word 
156 
constructors: 

157 
\<open>0 :: 'a::len word\<close>, 

158 
\<open>numeral :: num \<Rightarrow> 'a::len word\<close> 

159 

160 
instantiation word :: (len) equal 

161 
begin 

162 

163 
lift_definition equal_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> bool\<close> 

164 
is \<open>\<lambda>k l. take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close> 

165 
by simp 

166 

167 
instance 

168 
by (standard; transfer) rule 

169 

170 
end 

171 

172 
lemma [code]: 

72262  173 
\<open>HOL.equal v w \<longleftrightarrow> HOL.equal (Word.the_int v) (Word.the_int w)\<close> 
72243  174 
by transfer (simp add: equal) 
175 

176 
lemma [code]: 

72262  177 
\<open>Word.the_int 0 = 0\<close> 
72243  178 
by transfer simp 
179 

180 
lemma [code]: 

72262  181 
\<open>Word.the_int 1 = 1\<close> 
72243  182 
by transfer simp 
183 

184 
lemma [code]: 

72262  185 
\<open>Word.the_int (v + w) = take_bit LENGTH('a) (Word.the_int v + Word.the_int w)\<close> 
72243  186 
for v w :: \<open>'a::len word\<close> 
187 
by transfer (simp add: take_bit_add) 

188 

189 
lemma [code]: 

72262  190 
\<open>Word.the_int ( w) = (let k = Word.the_int w in if w = 0 then 0 else 2 ^ LENGTH('a)  k)\<close> 
72243  191 
for w :: \<open>'a::len word\<close> 
192 
by transfer (auto simp add: take_bit_eq_mod zmod_zminus1_eq_if) 

193 

194 
lemma [code]: 

72262  195 
\<open>Word.the_int (v  w) = take_bit LENGTH('a) (Word.the_int v  Word.the_int w)\<close> 
72243  196 
for v w :: \<open>'a::len word\<close> 
197 
by transfer (simp add: take_bit_diff) 

198 

199 
lemma [code]: 

72262  200 
\<open>Word.the_int (v * w) = take_bit LENGTH('a) (Word.the_int v * Word.the_int w)\<close> 
72243  201 
for v w :: \<open>'a::len word\<close> 
202 
by transfer (simp add: take_bit_mult) 

203 

204 

72244  205 
subsubsection \<open>Basic conversions\<close> 
70185  206 

72262  207 
abbreviation word_of_nat :: \<open>nat \<Rightarrow> 'a::len word\<close> 
208 
where \<open>word_of_nat \<equiv> of_nat\<close> 

209 

210 
abbreviation word_of_int :: \<open>int \<Rightarrow> 'a::len word\<close> 

211 
where \<open>word_of_int \<equiv> of_int\<close> 

212 

213 
lemma word_of_nat_eq_iff: 

214 
\<open>word_of_nat m = (word_of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m = take_bit LENGTH('a) n\<close> 

215 
by transfer (simp add: take_bit_of_nat) 

216 

217 
lemma word_of_int_eq_iff: 

218 
\<open>word_of_int k = (word_of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close> 

219 
by transfer rule 

220 

221 
lemma word_of_nat_eq_0_iff [simp]: 

222 
\<open>word_of_nat n = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd n\<close> 

223 
using word_of_nat_eq_iff [where ?'a = 'a, of n 0] by (simp add: take_bit_eq_0_iff) 

224 

225 
lemma word_of_int_eq_0_iff [simp]: 

226 
\<open>word_of_int k = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd k\<close> 

227 
using word_of_int_eq_iff [where ?'a = 'a, of k 0] by (simp add: take_bit_eq_0_iff) 

228 

229 
context semiring_1 

230 
begin 

231 

232 
lift_definition unsigned :: \<open>'b::len word \<Rightarrow> 'a\<close> 

233 
is \<open>of_nat \<circ> nat \<circ> take_bit LENGTH('b)\<close> 

72244  234 
by simp 
55816
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

235 

72262  236 
lemma unsigned_0 [simp]: 
237 
\<open>unsigned 0 = 0\<close> 

238 
by transfer simp 

239 

240 
lemma unsigned_1 [simp]: 

241 
\<open>unsigned 1 = 1\<close> 

242 
by transfer simp 

243 

244 
lemma unsigned_numeral [simp]: 

245 
\<open>unsigned (numeral n :: 'b::len word) = of_nat (take_bit LENGTH('b) (numeral n))\<close> 

246 
by transfer (simp add: nat_take_bit_eq) 

247 

248 
lemma unsigned_neg_numeral [simp]: 

249 
\<open>unsigned ( numeral n :: 'b::len word) = of_nat (nat (take_bit LENGTH('b) ( numeral n)))\<close> 

250 
by transfer simp 

251 

252 
end 

253 

254 
context semiring_1 

255 
begin 

256 

257 
lemma unsigned_of_nat [simp]: 

258 
\<open>unsigned (word_of_nat n :: 'b::len word) = of_nat (take_bit LENGTH('b) n)\<close> 

259 
by transfer (simp add: nat_eq_iff take_bit_of_nat) 

260 

261 
lemma unsigned_of_int [simp]: 

262 
\<open>unsigned (word_of_int k :: 'b::len word) = of_nat (nat (take_bit LENGTH('b) k))\<close> 

263 
by transfer simp 

264 

265 
end 

266 

267 
context semiring_char_0 

268 
begin 

269 

270 
lemma unsigned_word_eqI: 

271 
\<open>v = w\<close> if \<open>unsigned v = unsigned w\<close> 

272 
using that by transfer (simp add: eq_nat_nat_iff) 

273 

274 
lemma word_eq_iff_unsigned: 

275 
\<open>v = w \<longleftrightarrow> unsigned v = unsigned w\<close> 

276 
by (auto intro: unsigned_word_eqI) 

277 

278 
end 

279 

280 
context ring_1 

281 
begin 

282 

283 
lift_definition signed :: \<open>'b::len word \<Rightarrow> 'a\<close> 

284 
is \<open>of_int \<circ> signed_take_bit (LENGTH('b)  Suc 0)\<close> 

285 
by (simp flip: signed_take_bit_decr_length_iff) 

286 

287 
lemma signed_0 [simp]: 

288 
\<open>signed 0 = 0\<close> 

289 
by transfer simp 

290 

291 
lemma signed_1 [simp]: 

292 
\<open>signed (1 :: 'b::len word) = (if LENGTH('b) = 1 then  1 else 1)\<close> 

293 
by (transfer fixing: uminus; cases \<open>LENGTH('b)\<close>) 

294 
(simp_all add: sbintrunc_minus_simps) 

295 

296 
lemma signed_minus_1 [simp]: 

297 
\<open>signed ( 1 :: 'b::len word) =  1\<close> 

298 
by (transfer fixing: uminus) simp 

299 

300 
lemma signed_numeral [simp]: 

301 
\<open>signed (numeral n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b)  1) (numeral n))\<close> 

302 
by transfer simp 

303 

304 
lemma signed_neg_numeral [simp]: 

305 
\<open>signed ( numeral n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b)  1) ( numeral n))\<close> 

306 
by transfer simp 

307 

308 
lemma signed_of_nat [simp]: 

309 
\<open>signed (word_of_nat n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b)  Suc 0) (int n))\<close> 

310 
by transfer simp 

311 

312 
lemma signed_of_int [simp]: 

313 
\<open>signed (word_of_int n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b)  Suc 0) n)\<close> 

314 
by transfer simp 

315 

316 
end 

317 

318 
context ring_char_0 

319 
begin 

320 

321 
lemma signed_word_eqI: 

322 
\<open>v = w\<close> if \<open>signed v = signed w\<close> 

323 
using that by transfer (simp flip: signed_take_bit_decr_length_iff) 

324 

325 
lemma word_eq_iff_signed: 

326 
\<open>v = w \<longleftrightarrow> signed v = signed w\<close> 

327 
by (auto intro: signed_word_eqI) 

328 

329 
end 

330 

331 
abbreviation unat :: \<open>'a::len word \<Rightarrow> nat\<close> 

332 
where \<open>unat \<equiv> unsigned\<close> 

333 

334 
abbreviation uint :: \<open>'a::len word \<Rightarrow> int\<close> 

335 
where \<open>uint \<equiv> unsigned\<close> 

336 

337 
abbreviation sint :: \<open>'a::len word \<Rightarrow> int\<close> 

338 
where \<open>sint \<equiv> signed\<close> 

339 

340 
abbreviation ucast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close> 

341 
where \<open>ucast \<equiv> unsigned\<close> 

342 

343 
abbreviation scast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close> 

344 
where \<open>scast \<equiv> signed\<close> 

345 

346 
context 

347 
includes lifting_syntax 

348 
begin 

349 

350 
lemma [transfer_rule]: 

351 
\<open>(pcr_word ===> (=)) (nat \<circ> take_bit LENGTH('a)) (unat :: 'a::len word \<Rightarrow> nat)\<close> 

352 
using unsigned.transfer [where ?'a = nat] by simp 

353 

354 
lemma [transfer_rule]: 

355 
\<open>(pcr_word ===> (=)) (take_bit LENGTH('a)) (uint :: 'a::len word \<Rightarrow> int)\<close> 

356 
using unsigned.transfer [where ?'a = int] by (simp add: comp_def) 

357 

358 
lemma [transfer_rule]: 

359 
\<open>(pcr_word ===> (=)) (signed_take_bit (LENGTH('a)  Suc 0)) (sint :: 'a::len word \<Rightarrow> int)\<close> 

360 
using signed.transfer [where ?'a = int] by simp 

361 

362 
lemma [transfer_rule]: 

363 
\<open>(pcr_word ===> pcr_word) (take_bit LENGTH('a)) (ucast :: 'a::len word \<Rightarrow> 'b::len word)\<close> 

364 
proof (rule rel_funI) 

365 
fix k :: int and w :: \<open>'a word\<close> 

366 
assume \<open>pcr_word k w\<close> 

367 
then have \<open>w = word_of_int k\<close> 

368 
by (simp add: pcr_word_def cr_word_def relcompp_apply) 

369 
moreover have \<open>pcr_word (take_bit LENGTH('a) k) (ucast (word_of_int k :: 'a word))\<close> 

370 
by transfer (simp add: pcr_word_def cr_word_def relcompp_apply) 

371 
ultimately show \<open>pcr_word (take_bit LENGTH('a) k) (ucast w)\<close> 

372 
by simp 

373 
qed 

374 

375 
lemma [transfer_rule]: 

376 
\<open>(pcr_word ===> pcr_word) (signed_take_bit (LENGTH('a)  Suc 0)) (scast :: 'a::len word \<Rightarrow> 'b::len word)\<close> 

377 
proof (rule rel_funI) 

378 
fix k :: int and w :: \<open>'a word\<close> 

379 
assume \<open>pcr_word k w\<close> 

380 
then have \<open>w = word_of_int k\<close> 

381 
by (simp add: pcr_word_def cr_word_def relcompp_apply) 

382 
moreover have \<open>pcr_word (signed_take_bit (LENGTH('a)  Suc 0) k) (scast (word_of_int k :: 'a word))\<close> 

383 
by transfer (simp add: pcr_word_def cr_word_def relcompp_apply) 

384 
ultimately show \<open>pcr_word (signed_take_bit (LENGTH('a)  Suc 0) k) (scast w)\<close> 

385 
by simp 

386 
qed 

387 

388 
end 

389 

390 
lemma of_nat_unat [simp]: 

391 
\<open>of_nat (unat w) = unsigned w\<close> 

392 
by transfer simp 

393 

394 
lemma of_int_uint [simp]: 

395 
\<open>of_int (uint w) = unsigned w\<close> 

396 
by transfer simp 

397 

398 
lemma of_int_sint [simp]: 

399 
\<open>of_int (sint a) = signed a\<close> 

400 
by transfer (simp_all add: take_bit_signed_take_bit) 

72079  401 

402 
lemma nat_uint_eq [simp]: 

403 
\<open>nat (uint w) = unat w\<close> 

404 
by transfer simp 

405 

72262  406 
text \<open>Aliasses only for code generation\<close> 
407 

408 
context 

409 
begin 

410 

411 
qualified lift_definition of_int :: \<open>int \<Rightarrow> 'a::len word\<close> 

412 
is \<open>take_bit LENGTH('a)\<close> . 

413 

414 
qualified lift_definition of_nat :: \<open>nat \<Rightarrow> 'a::len word\<close> 

415 
is \<open>int \<circ> take_bit LENGTH('a)\<close> . 

416 

417 
qualified lift_definition the_nat :: \<open>'a::len word \<Rightarrow> nat\<close> 

418 
is \<open>nat \<circ> take_bit LENGTH('a)\<close> by simp 

419 

420 
qualified lift_definition the_signed_int :: \<open>'a::len word \<Rightarrow> int\<close> 

421 
is \<open>signed_take_bit (LENGTH('a)  Suc 0)\<close> by (simp add: signed_take_bit_decr_length_iff) 

422 

423 
qualified lift_definition cast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close> 

424 
is \<open>take_bit LENGTH('a)\<close> by simp 

425 

426 
qualified lift_definition signed_cast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close> 

427 
is \<open>signed_take_bit (LENGTH('a)  Suc 0)\<close> by (metis signed_take_bit_decr_length_iff) 

428 

429 
end 

430 

431 
lemma [code_abbrev, simp]: 

432 
\<open>Word.the_int = uint\<close> 

433 
by transfer rule 

434 

435 
lemma [code]: 

436 
\<open>Word.the_int (Word.of_int k :: 'a::len word) = take_bit LENGTH('a) k\<close> 

437 
by transfer simp 

438 

439 
lemma [code_abbrev, simp]: 

440 
\<open>Word.of_int = word_of_int\<close> 

441 
by (rule; transfer) simp 

442 

443 
lemma [code]: 

444 
\<open>Word.the_int (Word.of_nat n :: 'a::len word) = take_bit LENGTH('a) (int n)\<close> 

72244  445 
by transfer (simp add: take_bit_of_nat) 
446 

72262  447 
lemma [code_abbrev, simp]: 
448 
\<open>Word.of_nat = word_of_nat\<close> 

449 
by (rule; transfer) (simp add: take_bit_of_nat) 

450 

451 
lemma [code]: 

452 
\<open>Word.the_nat w = nat (Word.the_int w)\<close> 

453 
by transfer simp 

454 

455 
lemma [code_abbrev, simp]: 

456 
\<open>Word.the_nat = unat\<close> 

457 
by (rule; transfer) simp 

458 

459 
lemma [code]: 

460 
\<open>Word.the_signed_int w = signed_take_bit (LENGTH('a)  Suc 0) (Word.the_int w)\<close> 

461 
for w :: \<open>'a::len word\<close> 

462 
by transfer simp 

463 

464 
lemma [code_abbrev, simp]: 

465 
\<open>Word.the_signed_int = sint\<close> 

466 
by (rule; transfer) simp 

467 

468 
lemma [code]: 

469 
\<open>Word.the_int (Word.cast w :: 'b::len word) = take_bit LENGTH('b) (Word.the_int w)\<close> 

470 
for w :: \<open>'a::len word\<close> 

471 
by transfer simp 

472 

473 
lemma [code_abbrev, simp]: 

474 
\<open>Word.cast = ucast\<close> 

475 
by (rule; transfer) simp 

476 

477 
lemma [code]: 

478 
\<open>Word.the_int (Word.signed_cast w :: 'b::len word) = take_bit LENGTH('b) (Word.the_signed_int w)\<close> 

479 
for w :: \<open>'a::len word\<close> 

480 
by transfer simp 

481 

482 
lemma [code_abbrev, simp]: 

483 
\<open>Word.signed_cast = scast\<close> 

484 
by (rule; transfer) simp 

485 

486 
lemma [code]: 

487 
\<open>unsigned w = of_nat (nat (Word.the_int w))\<close> 

488 
by transfer simp 

489 

490 
lemma [code]: 

491 
\<open>signed w = of_int (Word.the_signed_int w)\<close> 

492 
by transfer simp 

72244  493 

494 

495 
subsubsection \<open>Basic ordering\<close> 

45547  496 

71954
13bb3f5cdc5b
pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
haftmann
parents:
71953
diff
changeset

497 
instantiation word :: (len) linorder 
45547  498 
begin 
499 

71950  500 
lift_definition less_eq_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" 
501 
is "\<lambda>a b. take_bit LENGTH('a) a \<le> take_bit LENGTH('a) b" 

502 
by simp 

503 

504 
lift_definition less_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" 

505 
is "\<lambda>a b. take_bit LENGTH('a) a < take_bit LENGTH('a) b" 

506 
by simp 

37660  507 

45547  508 
instance 
71950  509 
by (standard; transfer) auto 
45547  510 

511 
end 

512 

71957
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71955
diff
changeset

513 
interpretation word_order: ordering_top \<open>(\<le>)\<close> \<open>(<)\<close> \<open> 1 :: 'a::len word\<close> 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71955
diff
changeset

514 
by (standard; transfer) (simp add: take_bit_eq_mod zmod_minus1) 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71955
diff
changeset

515 

3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71955
diff
changeset

516 
interpretation word_coorder: ordering_top \<open>(\<ge>)\<close> \<open>(>)\<close> \<open>0 :: 'a::len word\<close> 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71955
diff
changeset

517 
by (standard; transfer) simp 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71955
diff
changeset

518 

72262  519 
lemma word_of_nat_less_eq_iff: 
520 
\<open>word_of_nat m \<le> (word_of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m \<le> take_bit LENGTH('a) n\<close> 

521 
by transfer (simp add: take_bit_of_nat) 

522 

523 
lemma word_of_int_less_eq_iff: 

524 
\<open>word_of_int k \<le> (word_of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k \<le> take_bit LENGTH('a) l\<close> 

525 
by transfer rule 

526 

527 
lemma word_of_nat_less_iff: 

528 
\<open>word_of_nat m < (word_of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m < take_bit LENGTH('a) n\<close> 

529 
by transfer (simp add: take_bit_of_nat) 

530 

531 
lemma word_of_int_less_iff: 

532 
\<open>word_of_int k < (word_of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k < take_bit LENGTH('a) l\<close> 

533 
by transfer rule 

534 

71950  535 
lemma word_le_def [code]: 
536 
"a \<le> b \<longleftrightarrow> uint a \<le> uint b" 

537 
by transfer rule 

538 

539 
lemma word_less_def [code]: 

540 
"a < b \<longleftrightarrow> uint a < uint b" 

541 
by transfer rule 

542 

71951  543 
lemma word_greater_zero_iff: 
71954
13bb3f5cdc5b
pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
haftmann
parents:
71953
diff
changeset

544 
\<open>a > 0 \<longleftrightarrow> a \<noteq> 0\<close> for a :: \<open>'a::len word\<close> 
71951  545 
by transfer (simp add: less_le) 
546 

547 
lemma of_nat_word_less_eq_iff: 

548 
\<open>of_nat m \<le> (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m \<le> take_bit LENGTH('a) n\<close> 

549 
by transfer (simp add: take_bit_of_nat) 

550 

551 
lemma of_nat_word_less_iff: 

552 
\<open>of_nat m < (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m < take_bit LENGTH('a) n\<close> 

553 
by transfer (simp add: take_bit_of_nat) 

554 

555 
lemma of_int_word_less_eq_iff: 

556 
\<open>of_int k \<le> (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k \<le> take_bit LENGTH('a) l\<close> 

557 
by transfer rule 

558 

559 
lemma of_int_word_less_iff: 

560 
\<open>of_int k < (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k < take_bit LENGTH('a) l\<close> 

561 
by transfer rule 

562 

37660  563 

61799  564 
subsection \<open>Bitwise operations\<close> 
37660  565 

72244  566 
instantiation word :: (len) semiring_modulo 
567 
begin 

568 

569 
lift_definition divide_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close> 

570 
is \<open>\<lambda>a b. take_bit LENGTH('a) a div take_bit LENGTH('a) b\<close> 

571 
by simp 

572 

573 
lift_definition modulo_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close> 

574 
is \<open>\<lambda>a b. take_bit LENGTH('a) a mod take_bit LENGTH('a) b\<close> 

575 
by simp 

576 

577 
instance proof 

578 
show "a div b * b + a mod b = a" for a b :: "'a word" 

579 
proof transfer 

580 
fix k l :: int 

581 
define r :: int where "r = 2 ^ LENGTH('a)" 

582 
then have r: "take_bit LENGTH('a) k = k mod r" for k 

583 
by (simp add: take_bit_eq_mod) 

584 
have "k mod r = ((k mod r) div (l mod r) * (l mod r) 

585 
+ (k mod r) mod (l mod r)) mod r" 

586 
by (simp add: div_mult_mod_eq) 

587 
also have "... = (((k mod r) div (l mod r) * (l mod r)) mod r 

588 
+ (k mod r) mod (l mod r)) mod r" 

589 
by (simp add: mod_add_left_eq) 

590 
also have "... = (((k mod r) div (l mod r) * l) mod r 

591 
+ (k mod r) mod (l mod r)) mod r" 

592 
by (simp add: mod_mult_right_eq) 

593 
finally have "k mod r = ((k mod r) div (l mod r) * l 

594 
+ (k mod r) mod (l mod r)) mod r" 

595 
by (simp add: mod_simps) 

596 
with r show "take_bit LENGTH('a) (take_bit LENGTH('a) k div take_bit LENGTH('a) l * l 

597 
+ take_bit LENGTH('a) k mod take_bit LENGTH('a) l) = take_bit LENGTH('a) k" 

598 
by simp 

599 
qed 

600 
qed 

601 

602 
end 

603 

604 
instance word :: (len) semiring_parity 

605 
proof 

606 
show "\<not> 2 dvd (1::'a word)" 

607 
by transfer simp 

608 
show even_iff_mod_2_eq_0: "2 dvd a \<longleftrightarrow> a mod 2 = 0" 

609 
for a :: "'a word" 

610 
by transfer (simp_all add: mod_2_eq_odd take_bit_Suc) 

611 
show "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1" 

612 
for a :: "'a word" 

613 
by transfer (simp_all add: mod_2_eq_odd take_bit_Suc) 

614 
qed 

615 

71951  616 
lemma word_bit_induct [case_names zero even odd]: 
617 
\<open>P a\<close> if word_zero: \<open>P 0\<close> 

72262  618 
and word_even: \<open>\<And>a. P a \<Longrightarrow> 0 < a \<Longrightarrow> a < 2 ^ (LENGTH('a)  Suc 0) \<Longrightarrow> P (2 * a)\<close> 
619 
and word_odd: \<open>\<And>a. P a \<Longrightarrow> a < 2 ^ (LENGTH('a)  Suc 0) \<Longrightarrow> P (1 + 2 * a)\<close> 

71951  620 
for P and a :: \<open>'a::len word\<close> 
621 
proof  

72262  622 
define m :: nat where \<open>m = LENGTH('a)  Suc 0\<close> 
71951  623 
then have l: \<open>LENGTH('a) = Suc m\<close> 
624 
by simp 

625 
define n :: nat where \<open>n = unat a\<close> 

626 
then have \<open>n < 2 ^ LENGTH('a)\<close> 

72262  627 
by transfer (simp add: take_bit_eq_mod) 
71951  628 
then have \<open>n < 2 * 2 ^ m\<close> 
629 
by (simp add: l) 

630 
then have \<open>P (of_nat n)\<close> 

631 
proof (induction n rule: nat_bit_induct) 

632 
case zero 

633 
show ?case 

634 
by simp (rule word_zero) 

635 
next 

636 
case (even n) 

637 
then have \<open>n < 2 ^ m\<close> 

638 
by simp 

639 
with even.IH have \<open>P (of_nat n)\<close> 

640 
by simp 

641 
moreover from \<open>n < 2 ^ m\<close> even.hyps have \<open>0 < (of_nat n :: 'a word)\<close> 

72262  642 
by (auto simp add: word_greater_zero_iff l) 
643 
moreover from \<open>n < 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a)  Suc 0)\<close> 

71951  644 
using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>] 
72261  645 
by (simp add: l take_bit_eq_mod) 
71951  646 
ultimately have \<open>P (2 * of_nat n)\<close> 
647 
by (rule word_even) 

648 
then show ?case 

649 
by simp 

650 
next 

651 
case (odd n) 

652 
then have \<open>Suc n \<le> 2 ^ m\<close> 

653 
by simp 

654 
with odd.IH have \<open>P (of_nat n)\<close> 

655 
by simp 

72262  656 
moreover from \<open>Suc n \<le> 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a)  Suc 0)\<close> 
71951  657 
using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>] 
72261  658 
by (simp add: l take_bit_eq_mod) 
71951  659 
ultimately have \<open>P (1 + 2 * of_nat n)\<close> 
660 
by (rule word_odd) 

661 
then show ?case 

662 
by simp 

663 
qed 

664 
moreover have \<open>of_nat (nat (uint a)) = a\<close> 

665 
by transfer simp 

666 
ultimately show ?thesis 

72079  667 
by (simp add: n_def) 
71951  668 
qed 
669 

670 
lemma bit_word_half_eq: 

671 
\<open>(of_bool b + a * 2) div 2 = a\<close> 

672 
if \<open>a < 2 ^ (LENGTH('a)  Suc 0)\<close> 

673 
for a :: \<open>'a::len word\<close> 

674 
proof (cases \<open>2 \<le> LENGTH('a::len)\<close>) 

675 
case False 

676 
have \<open>of_bool (odd k) < (1 :: int) \<longleftrightarrow> even k\<close> for k :: int 

677 
by auto 

678 
with False that show ?thesis 

679 
by transfer (simp add: eq_iff) 

680 
next 

681 
case True 

682 
obtain n where length: \<open>LENGTH('a) = Suc n\<close> 

683 
by (cases \<open>LENGTH('a)\<close>) simp_all 

684 
show ?thesis proof (cases b) 

685 
case False 

686 
moreover have \<open>a * 2 div 2 = a\<close> 

687 
using that proof transfer 

688 
fix k :: int 

689 
from length have \<open>k * 2 mod 2 ^ LENGTH('a) = (k mod 2 ^ n) * 2\<close> 

690 
by simp 

691 
moreover assume \<open>take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a)  Suc 0))\<close> 

692 
with \<open>LENGTH('a) = Suc n\<close> 

693 
have \<open>k mod 2 ^ LENGTH('a) = k mod 2 ^ n\<close> 

694 
by (simp add: take_bit_eq_mod divmod_digit_0) 

695 
ultimately have \<open>take_bit LENGTH('a) (k * 2) = take_bit LENGTH('a) k * 2\<close> 

696 
by (simp add: take_bit_eq_mod) 

697 
with True show \<open>take_bit LENGTH('a) (take_bit LENGTH('a) (k * 2) div take_bit LENGTH('a) 2) 

698 
= take_bit LENGTH('a) k\<close> 

699 
by simp 

700 
qed 

701 
ultimately show ?thesis 

702 
by simp 

703 
next 

704 
case True 

705 
moreover have \<open>(1 + a * 2) div 2 = a\<close> 

706 
using that proof transfer 

707 
fix k :: int 

708 
from length have \<open>(1 + k * 2) mod 2 ^ LENGTH('a) = 1 + (k mod 2 ^ n) * 2\<close> 

709 
using pos_zmod_mult_2 [of \<open>2 ^ n\<close> k] by (simp add: ac_simps) 

710 
moreover assume \<open>take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a)  Suc 0))\<close> 

711 
with \<open>LENGTH('a) = Suc n\<close> 

712 
have \<open>k mod 2 ^ LENGTH('a) = k mod 2 ^ n\<close> 

713 
by (simp add: take_bit_eq_mod divmod_digit_0) 

714 
ultimately have \<open>take_bit LENGTH('a) (1 + k * 2) = 1 + take_bit LENGTH('a) k * 2\<close> 

715 
by (simp add: take_bit_eq_mod) 

716 
with True show \<open>take_bit LENGTH('a) (take_bit LENGTH('a) (1 + k * 2) div take_bit LENGTH('a) 2) 

717 
= take_bit LENGTH('a) k\<close> 

718 
by (auto simp add: take_bit_Suc) 

719 
qed 

720 
ultimately show ?thesis 

721 
by simp 

722 
qed 

723 
qed 

724 

725 
lemma even_mult_exp_div_word_iff: 

726 
\<open>even (a * 2 ^ m div 2 ^ n) \<longleftrightarrow> \<not> ( 

727 
m \<le> n \<and> 

728 
n < LENGTH('a) \<and> odd (a div 2 ^ (n  m)))\<close> for a :: \<open>'a::len word\<close> 

729 
by transfer 

730 
(auto simp flip: drop_bit_eq_div simp add: even_drop_bit_iff_not_bit bit_take_bit_iff, 

731 
simp_all flip: push_bit_eq_mult add: bit_push_bit_iff_int) 

732 

71965
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

733 
instantiation word :: (len) semiring_bits 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

734 
begin 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

735 

d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

736 
lift_definition bit_word :: \<open>'a word \<Rightarrow> nat \<Rightarrow> bool\<close> 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

737 
is \<open>\<lambda>k n. n < LENGTH('a) \<and> bit k n\<close> 
71951  738 
proof 
71965
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

739 
fix k l :: int and n :: nat 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

740 
assume *: \<open>take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close> 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

741 
show \<open>n < LENGTH('a) \<and> bit k n \<longleftrightarrow> n < LENGTH('a) \<and> bit l n\<close> 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

742 
proof (cases \<open>n < LENGTH('a)\<close>) 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

743 
case True 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

744 
from * have \<open>bit (take_bit LENGTH('a) k) n \<longleftrightarrow> bit (take_bit LENGTH('a) l) n\<close> 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

745 
by simp 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

746 
then show ?thesis 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

747 
by (simp add: bit_take_bit_iff) 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

748 
next 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

749 
case False 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

750 
then show ?thesis 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

751 
by simp 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

752 
qed 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

753 
qed 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

754 

d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

755 
instance proof 
71951  756 
show \<open>P a\<close> if stable: \<open>\<And>a. a div 2 = a \<Longrightarrow> P a\<close> 
757 
and rec: \<open>\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a)\<close> 

758 
for P and a :: \<open>'a word\<close> 

759 
proof (induction a rule: word_bit_induct) 

760 
case zero 

761 
have \<open>0 div 2 = (0::'a word)\<close> 

762 
by transfer simp 

763 
with stable [of 0] show ?case 

764 
by simp 

765 
next 

766 
case (even a) 

767 
with rec [of a False] show ?case 

768 
using bit_word_half_eq [of a False] by (simp add: ac_simps) 

769 
next 

770 
case (odd a) 

771 
with rec [of a True] show ?case 

772 
using bit_word_half_eq [of a True] by (simp add: ac_simps) 

773 
qed 

71965
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

774 
show \<open>bit a n \<longleftrightarrow> odd (a div 2 ^ n)\<close> for a :: \<open>'a word\<close> and n 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

775 
by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit bit_iff_odd_drop_bit) 
71951  776 
show \<open>0 div a = 0\<close> 
777 
for a :: \<open>'a word\<close> 

778 
by transfer simp 

779 
show \<open>a div 1 = a\<close> 

780 
for a :: \<open>'a word\<close> 

781 
by transfer simp 

782 
show \<open>a mod b div b = 0\<close> 

783 
for a b :: \<open>'a word\<close> 

784 
apply transfer 

785 
apply (simp add: take_bit_eq_mod) 

786 
apply (subst (3) mod_pos_pos_trivial [of _ \<open>2 ^ LENGTH('a)\<close>]) 

787 
apply simp_all 

788 
apply (metis le_less mod_by_0 pos_mod_conj zero_less_numeral zero_less_power) 

789 
using pos_mod_bound [of \<open>2 ^ LENGTH('a)\<close>] apply simp 

790 
proof  

791 
fix aa :: int and ba :: int 

792 
have f1: "\<And>i n. (i::int) mod 2 ^ n = 0 \<or> 0 < i mod 2 ^ n" 

793 
by (metis le_less take_bit_eq_mod take_bit_nonnegative) 

794 
have "(0::int) < 2 ^ len_of (TYPE('a)::'a itself) \<and> ba mod 2 ^ len_of (TYPE('a)::'a itself) \<noteq> 0 \<or> aa mod 2 ^ len_of (TYPE('a)::'a itself) mod (ba mod 2 ^ len_of (TYPE('a)::'a itself)) < 2 ^ len_of (TYPE('a)::'a itself)" 

795 
by (metis (no_types) mod_by_0 unique_euclidean_semiring_numeral_class.pos_mod_bound zero_less_numeral zero_less_power) 

796 
then show "aa mod 2 ^ len_of (TYPE('a)::'a itself) mod (ba mod 2 ^ len_of (TYPE('a)::'a itself)) < 2 ^ len_of (TYPE('a)::'a itself)" 

797 
using f1 by (meson le_less less_le_trans unique_euclidean_semiring_numeral_class.pos_mod_bound) 

798 
qed 

799 
show \<open>(1 + a) div 2 = a div 2\<close> 

800 
if \<open>even a\<close> 

801 
for a :: \<open>'a word\<close> 

71953  802 
using that by transfer 
803 
(auto dest: le_Suc_ex simp add: mod_2_eq_odd take_bit_Suc elim!: evenE) 

71951  804 
show \<open>(2 :: 'a word) ^ m div 2 ^ n = of_bool ((2 :: 'a word) ^ m \<noteq> 0 \<and> n \<le> m) * 2 ^ (m  n)\<close> 
805 
for m n :: nat 

806 
by transfer (simp, simp add: exp_div_exp_eq) 

807 
show "a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)" 

808 
for a :: "'a word" and m n :: nat 

809 
apply transfer 

810 
apply (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: drop_bit_eq_div) 

811 
apply (simp add: drop_bit_take_bit) 

812 
done 

813 
show "a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n" 

814 
for a :: "'a word" and m n :: nat 

815 
by transfer (auto simp flip: take_bit_eq_mod simp add: ac_simps) 

816 
show \<open>a * 2 ^ m mod 2 ^ n = a mod 2 ^ (n  m) * 2 ^ m\<close> 

817 
if \<open>m \<le> n\<close> for a :: "'a word" and m n :: nat 

818 
using that apply transfer 

819 
apply (auto simp flip: take_bit_eq_mod) 

820 
apply (auto simp flip: push_bit_eq_mult simp add: push_bit_take_bit split: split_min_lin) 

821 
done 

822 
show \<open>a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\<close> 

823 
for a :: "'a word" and m n :: nat 

824 
by transfer (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: take_bit_eq_mod drop_bit_eq_div split: split_min_lin) 

825 
show \<open>even ((2 ^ m  1) div (2::'a word) ^ n) \<longleftrightarrow> 2 ^ n = (0::'a word) \<or> m \<le> n\<close> 

826 
for m n :: nat 

827 
by transfer (auto simp add: take_bit_of_mask even_mask_div_iff) 

828 
show \<open>even (a * 2 ^ m div 2 ^ n) \<longleftrightarrow> n < m \<or> (2::'a word) ^ n = 0 \<or> m \<le> n \<and> even (a div 2 ^ (n  m))\<close> 

829 
for a :: \<open>'a word\<close> and m n :: nat 

830 
proof transfer 

831 
show \<open>even (take_bit LENGTH('a) (k * 2 ^ m) div take_bit LENGTH('a) (2 ^ n)) \<longleftrightarrow> 

832 
n < m 

833 
\<or> take_bit LENGTH('a) ((2::int) ^ n) = take_bit LENGTH('a) 0 

834 
\<or> (m \<le> n \<and> even (take_bit LENGTH('a) k div take_bit LENGTH('a) (2 ^ (n  m))))\<close> 

835 
for m n :: nat and k l :: int 

836 
by (auto simp flip: take_bit_eq_mod drop_bit_eq_div push_bit_eq_mult 

837 
simp add: div_push_bit_of_1_eq_drop_bit drop_bit_take_bit drop_bit_push_bit_int [of n m]) 

838 
qed 

839 
qed 

840 

841 
end 

842 

72262  843 
lemma bit_word_eqI: 
844 
\<open>a = b\<close> if \<open>\<And>n. n < LENGTH('a) \<Longrightarrow> bit a n \<longleftrightarrow> bit b n\<close> 

845 
for a b :: \<open>'a::len word\<close> 

846 
using that by transfer (auto simp add: nat_less_le bit_eq_iff bit_take_bit_iff) 

847 

848 
lemma bit_imp_le_length: 

849 
\<open>n < LENGTH('a)\<close> if \<open>bit w n\<close> 

850 
for w :: \<open>'a::len word\<close> 

851 
using that by transfer simp 

852 

853 
lemma not_bit_length [simp]: 

854 
\<open>\<not> bit w LENGTH('a)\<close> for w :: \<open>'a::len word\<close> 

855 
by transfer simp 

856 

71952
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

857 
instantiation word :: (len) semiring_bit_shifts 
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

858 
begin 
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

859 

2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

860 
lift_definition push_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close> 
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

861 
is push_bit 
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

862 
proof  
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

863 
show \<open>take_bit LENGTH('a) (push_bit n k) = take_bit LENGTH('a) (push_bit n l)\<close> 
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

864 
if \<open>take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close> for k l :: int and n :: nat 
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

865 
proof  
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

866 
from that 
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

867 
have \<open>take_bit (LENGTH('a)  n) (take_bit LENGTH('a) k) 
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

868 
= take_bit (LENGTH('a)  n) (take_bit LENGTH('a) l)\<close> 
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

869 
by simp 
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

870 
moreover have \<open>min (LENGTH('a)  n) LENGTH('a) = LENGTH('a)  n\<close> 
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

871 
by simp 
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

872 
ultimately show ?thesis 
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

873 
by (simp add: take_bit_push_bit) 
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

874 
qed 
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

875 
qed 
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

876 

2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

877 
lift_definition drop_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close> 
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

878 
is \<open>\<lambda>n. drop_bit n \<circ> take_bit LENGTH('a)\<close> 
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

879 
by (simp add: take_bit_eq_mod) 
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

880 

71965
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

881 
lift_definition take_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close> 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

882 
is \<open>\<lambda>n. take_bit (min LENGTH('a) n)\<close> 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

883 
by (simp add: ac_simps) (simp only: flip: take_bit_take_bit) 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

884 

71952
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

885 
instance proof 
71965
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

886 
show \<open>push_bit n a = a * 2 ^ n\<close> for n :: nat and a :: \<open>'a word\<close> 
71952
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

887 
by transfer (simp add: push_bit_eq_mult) 
71965
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

888 
show \<open>drop_bit n a = a div 2 ^ n\<close> for n :: nat and a :: \<open>'a word\<close> 
71952
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

889 
by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit) 
71965
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

890 
show \<open>take_bit n a = a mod 2 ^ n\<close> for n :: nat and a :: \<open>'a word\<close> 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

891 
by transfer (auto simp flip: take_bit_eq_mod) 
71952
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

892 
qed 
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

893 

2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

894 
end 
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

895 

72262  896 
lemma [code]: 
897 
\<open>Word.the_int (take_bit n w) = (if n < LENGTH('a::len) then take_bit n (Word.the_int w) else Word.the_int w)\<close> 

898 
for w :: \<open>'a::len word\<close> 

899 
by transfer (simp add: not_le not_less ac_simps min_absorb2) 

900 

901 

902 
instantiation word :: (len) ring_bit_operations 

903 
begin 

904 

905 
lift_definition not_word :: \<open>'a word \<Rightarrow> 'a word\<close> 

906 
is not 

907 
by (simp add: take_bit_not_iff) 

908 

909 
lift_definition and_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close> 

910 
is \<open>and\<close> 

911 
by simp 

912 

913 
lift_definition or_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close> 

914 
is or 

915 
by simp 

916 

917 
lift_definition xor_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close> 

918 
is xor 

919 
by simp 

920 

921 
lift_definition mask_word :: \<open>nat \<Rightarrow> 'a word\<close> 

922 
is mask 

923 
. 

924 

925 
instance by (standard; transfer) 

926 
(auto simp add: minus_eq_not_minus_1 mask_eq_exp_minus_1 

927 
bit_not_iff bit_and_iff bit_or_iff bit_xor_iff) 

928 

929 
end 

930 

931 
lemma [code_abbrev]: 

932 
\<open>push_bit n 1 = (2 :: 'a::len word) ^ n\<close> 

933 
by (fact push_bit_of_1) 

934 

935 
lemma [code]: 

936 
\<open>NOT w = Word.of_int (NOT (Word.the_int w))\<close> 

937 
for w :: \<open>'a::len word\<close> 

938 
by transfer (simp add: take_bit_not_take_bit) 

939 

940 
lemma [code]: 

941 
\<open>Word.the_int (v AND w) = Word.the_int v AND Word.the_int w\<close> 

71990  942 
by transfer simp 
943 

72262  944 
lemma [code]: 
945 
\<open>Word.the_int (v OR w) = Word.the_int v OR Word.the_int w\<close> 

946 
by transfer simp 

947 

948 
lemma [code]: 

949 
\<open>Word.the_int (v XOR w) = Word.the_int v XOR Word.the_int w\<close> 

950 
by transfer simp 

951 

952 
lemma [code]: 

953 
\<open>Word.the_int (mask n :: 'a::len word) = mask (min LENGTH('a) n)\<close> 

954 
by transfer simp 

955 

956 
context 

957 
includes lifting_syntax 

958 
begin 

959 

960 
lemma set_bit_word_transfer [transfer_rule]: 

961 
\<open>((=) ===> pcr_word ===> pcr_word) set_bit set_bit\<close> 

962 
by (unfold set_bit_def) transfer_prover 

963 

964 
lemma unset_bit_word_transfer [transfer_rule]: 

965 
\<open>((=) ===> pcr_word ===> pcr_word) unset_bit unset_bit\<close> 

966 
by (unfold unset_bit_def) transfer_prover 

967 

968 
lemma flip_bit_word_transfer [transfer_rule]: 

969 
\<open>((=) ===> pcr_word ===> pcr_word) flip_bit flip_bit\<close> 

970 
by (unfold flip_bit_def) transfer_prover 

971 

972 
lemma signed_take_bit_word_transfer [transfer_rule]: 

973 
\<open>((=) ===> pcr_word ===> pcr_word) 

974 
(\<lambda>n k. signed_take_bit n (take_bit LENGTH('a::len) k)) 

975 
(signed_take_bit :: nat \<Rightarrow> 'a word \<Rightarrow> 'a word)\<close> 

976 
proof  

977 
let ?K = \<open>\<lambda>n (k :: int). take_bit (min LENGTH('a) n) k OR of_bool (n < LENGTH('a) \<and> bit k n) * NOT (mask n)\<close> 

978 
let ?W = \<open>\<lambda>n (w :: 'a word). take_bit n w OR of_bool (bit w n) * NOT (mask n)\<close> 

979 
have \<open>((=) ===> pcr_word ===> pcr_word) ?K ?W\<close> 

980 
by transfer_prover 

981 
also have \<open>?K = (\<lambda>n k. signed_take_bit n (take_bit LENGTH('a::len) k))\<close> 

982 
by (simp add: fun_eq_iff signed_take_bit_def bit_take_bit_iff ac_simps) 

983 
also have \<open>?W = signed_take_bit\<close> 

984 
by (simp add: fun_eq_iff signed_take_bit_def) 

985 
finally show ?thesis . 

986 
qed 

987 

988 
end 

989 

72244  990 

991 
subsection \<open>Conversions including casts\<close> 

992 

72262  993 
subsubsection \<open>Generic unsigned conversion\<close> 
994 

995 
context semiring_bits 

996 
begin 

997 

998 
lemma bit_unsigned_iff: 

999 
\<open>bit (unsigned w) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> bit w n\<close> 

1000 
for w :: \<open>'b::len word\<close> 

1001 
by (transfer fixing: bit) (simp add: bit_of_nat_iff bit_nat_iff bit_take_bit_iff) 

1002 

1003 
end 

1004 

1005 
context semiring_bit_shifts 

1006 
begin 

1007 

1008 
lemma unsigned_push_bit_eq: 

1009 
\<open>unsigned (push_bit n w) = take_bit LENGTH('b) (push_bit n (unsigned w))\<close> 

1010 
for w :: \<open>'b::len word\<close> 

1011 
proof (rule bit_eqI) 

1012 
fix m 

1013 
assume \<open>2 ^ m \<noteq> 0\<close> 

1014 
show \<open>bit (unsigned (push_bit n w)) m = bit (take_bit LENGTH('b) (push_bit n (unsigned w))) m\<close> 

1015 
proof (cases \<open>n \<le> m\<close>) 

1016 
case True 

1017 
with \<open>2 ^ m \<noteq> 0\<close> have \<open>2 ^ (m  n) \<noteq> 0\<close> 

1018 
by (metis (full_types) diff_add exp_add_not_zero_imp) 

1019 
with True show ?thesis 

1020 
by (simp add: bit_unsigned_iff bit_push_bit_iff Parity.bit_push_bit_iff bit_take_bit_iff not_le exp_eq_zero_iff ac_simps) 

1021 
next 

1022 
case False 

1023 
then show ?thesis 

1024 
by (simp add: not_le bit_unsigned_iff bit_push_bit_iff Parity.bit_push_bit_iff bit_take_bit_iff) 

1025 
qed 

1026 
qed 

1027 

1028 
lemma unsigned_take_bit_eq: 

1029 
\<open>unsigned (take_bit n w) = take_bit n (unsigned w)\<close> 

1030 
for w :: \<open>'b::len word\<close> 

1031 
by (rule bit_eqI) (simp add: bit_unsigned_iff bit_take_bit_iff Parity.bit_take_bit_iff) 

1032 

1033 
end 

1034 

1035 
context semiring_bit_operations 

1036 
begin 

1037 

1038 
lemma unsigned_and_eq: 

1039 
\<open>unsigned (v AND w) = unsigned v AND unsigned w\<close> 

1040 
for v w :: \<open>'b::len word\<close> 

1041 
by (rule bit_eqI) (simp add: bit_unsigned_iff bit_and_iff Bit_Operations.bit_and_iff) 

1042 

1043 
lemma unsigned_or_eq: 

1044 
\<open>unsigned (v OR w) = unsigned v OR unsigned w\<close> 

1045 
for v w :: \<open>'b::len word\<close> 

1046 
by (rule bit_eqI) (simp add: bit_unsigned_iff bit_or_iff Bit_Operations.bit_or_iff) 

1047 

1048 
lemma unsigned_xor_eq: 

1049 
\<open>unsigned (v XOR w) = unsigned v XOR unsigned w\<close> 

1050 
for v w :: \<open>'b::len word\<close> 

1051 
by (rule bit_eqI) (simp add: bit_unsigned_iff bit_xor_iff Bit_Operations.bit_xor_iff) 

1052 

1053 
end 

1054 

1055 
context ring_bit_operations 

1056 
begin 

1057 

1058 
lemma unsigned_not_eq: 

1059 
\<open>unsigned (NOT w) = take_bit LENGTH('b) (NOT (unsigned w))\<close> 

1060 
for w :: \<open>'b::len word\<close> 

1061 
by (rule bit_eqI) 

1062 
(simp add: bit_unsigned_iff bit_take_bit_iff bit_not_iff Bit_Operations.bit_not_iff exp_eq_zero_iff not_le) 

1063 

1064 
end 

1065 

1066 
context unique_euclidean_semiring_numeral 

1067 
begin 

1068 

1069 
lemma unsigned_greater_eq: 

1070 
\<open>0 \<le> unsigned w\<close> for w :: \<open>'b::len word\<close> 

1071 
by (transfer fixing: less_eq) simp 

1072 

1073 
lemma unsigned_less: 

1074 
\<open>unsigned w < 2 ^ LENGTH('b)\<close> for w :: \<open>'b::len word\<close> 

1075 
by (transfer fixing: less) simp 

1076 

1077 
end 

1078 

1079 
context linordered_semidom 

1080 
begin 

1081 

1082 
lemma word_less_eq_iff_unsigned: 

1083 
"a \<le> b \<longleftrightarrow> unsigned a \<le> unsigned b" 

1084 
by (transfer fixing: less_eq) (simp add: nat_le_eq_zle) 

1085 

1086 
lemma word_less_iff_unsigned: 

1087 
"a < b \<longleftrightarrow> unsigned a < unsigned b" 

1088 
by (transfer fixing: less) (auto dest: preorder_class.le_less_trans [OF take_bit_nonnegative]) 

1089 

1090 
end 

1091 

1092 

1093 
subsubsection \<open>Generic signed conversion\<close> 

1094 

1095 
context ring_bit_operations 

1096 
begin 

1097 

1098 
lemma bit_signed_iff: 

1099 
\<open>bit (signed w) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> bit w (min (LENGTH('b)  Suc 0) n)\<close> 

1100 
for w :: \<open>'b::len word\<close> 

1101 
by (transfer fixing: bit) 

1102 
(auto simp add: bit_of_int_iff Bit_Operations.bit_signed_take_bit_iff min_def) 

1103 

1104 
lemma signed_push_bit_eq: 

1105 
\<open>signed (push_bit n w) = signed_take_bit (LENGTH('b)  Suc 0) (push_bit n (signed w :: 'a))\<close> 

1106 
for w :: \<open>'b::len word\<close> 

1107 
proof (rule bit_eqI) 

1108 
fix m 

1109 
assume \<open>2 ^ m \<noteq> 0\<close> 

1110 
define q where \<open>q = LENGTH('b)  Suc 0\<close> 

1111 
then have *: \<open>LENGTH('b) = Suc q\<close> 

1112 
by simp 

1113 
show \<open>bit (signed (push_bit n w)) m \<longleftrightarrow> 

1114 
bit (signed_take_bit (LENGTH('b)  Suc 0) (push_bit n (signed w :: 'a))) m\<close> 

1115 
proof (cases \<open>q \<le> m\<close>) 

1116 
case True 

1117 
moreover define r where \<open>r = m  q\<close> 

1118 
ultimately have \<open>m = q + r\<close> 

1119 
by simp 

1120 
moreover from \<open>m = q + r\<close> \<open>2 ^ m \<noteq> 0\<close> have \<open>2 ^ q \<noteq> 0\<close> \<open>2 ^ r \<noteq> 0\<close> 

1121 
using exp_add_not_zero_imp_left [of q r] exp_add_not_zero_imp_right [of q r] 

1122 
by simp_all 

1123 
moreover from \<open>2 ^ q \<noteq> 0\<close> have \<open>2 ^ (q  n) \<noteq> 0\<close> 

1124 
by (rule exp_not_zero_imp_exp_diff_not_zero) 

1125 
ultimately show ?thesis 

1126 
by (auto simp add: bit_signed_iff bit_signed_take_bit_iff bit_push_bit_iff Parity.bit_push_bit_iff 

1127 
min_def * exp_eq_zero_iff le_diff_conv2) 

1128 
next 

1129 
case False 

1130 
then show ?thesis 

1131 
using exp_not_zero_imp_exp_diff_not_zero [of m n] 

1132 
by (auto simp add: bit_signed_iff bit_signed_take_bit_iff bit_push_bit_iff Parity.bit_push_bit_iff 

1133 
min_def not_le not_less * le_diff_conv2 less_diff_conv2 Parity.exp_eq_0_imp_not_bit exp_eq_0_imp_not_bit 

1134 
exp_eq_zero_iff) 

1135 
qed 

1136 
qed 

1137 

1138 
lemma signed_take_bit_eq: 

1139 
\<open>signed (take_bit n w) = (if n < LENGTH('b) then take_bit n (signed w) else signed w)\<close> 

1140 
for w :: \<open>'b::len word\<close> 

1141 
by (transfer fixing: take_bit; cases \<open>LENGTH('b)\<close>) 

1142 
(auto simp add: Bit_Operations.signed_take_bit_take_bit Bit_Operations.take_bit_signed_take_bit take_bit_of_int min_def less_Suc_eq) 

1143 

1144 
lemma signed_not_eq: 

1145 
\<open>signed (NOT w) = signed_take_bit LENGTH('b) (NOT (signed w))\<close> 

1146 
for w :: \<open>'b::len word\<close> 

1147 
proof (rule bit_eqI) 

1148 
fix n 

1149 
assume \<open>2 ^ n \<noteq> 0\<close> 

1150 
define q where \<open>q = LENGTH('b)  Suc 0\<close> 

1151 
then have *: \<open>LENGTH('b) = Suc q\<close> 

1152 
by simp 

1153 
show \<open>bit (signed (NOT w)) n \<longleftrightarrow> 

1154 
bit (signed_take_bit LENGTH('b) (NOT (signed w))) n\<close> 

1155 
proof (cases \<open>q < n\<close>) 

1156 
case True 

1157 
moreover define r where \<open>r = n  Suc q\<close> 

1158 
ultimately have \<open>n = r + Suc q\<close> 

1159 
by simp 

1160 
moreover from \<open>2 ^ n \<noteq> 0\<close> \<open>n = r + Suc q\<close> 

1161 
have \<open>2 ^ Suc q \<noteq> 0\<close> 

1162 
using exp_add_not_zero_imp_right by blast 

1163 
ultimately show ?thesis 

1164 
by (simp add: * bit_signed_iff bit_not_iff bit_signed_take_bit_iff Bit_Operations.bit_not_iff min_def 

1165 
exp_eq_zero_iff) 

1166 
next 

1167 
case False 

1168 
then show ?thesis 

1169 
by (auto simp add: * bit_signed_iff bit_not_iff bit_signed_take_bit_iff Bit_Operations.bit_not_iff min_def 

1170 
exp_eq_zero_iff) 

1171 
qed 

1172 
qed 

1173 

1174 
lemma signed_and_eq: 

1175 
\<open>signed (v AND w) = signed v AND signed w\<close> 

1176 
for v w :: \<open>'b::len word\<close> 

1177 
by (rule bit_eqI) (simp add: bit_signed_iff bit_and_iff Bit_Operations.bit_and_iff) 

1178 

1179 
lemma signed_or_eq: 

1180 
\<open>signed (v OR w) = signed v OR signed w\<close> 

1181 
for v w :: \<open>'b::len word\<close> 

1182 
by (rule bit_eqI) (simp add: bit_signed_iff bit_or_iff Bit_Operations.bit_or_iff) 

1183 

1184 
lemma signed_xor_eq: 

1185 
\<open>signed (v XOR w) = signed v XOR signed w\<close> 

1186 
for v w :: \<open>'b::len word\<close> 

1187 
by (rule bit_eqI) (simp add: bit_signed_iff bit_xor_iff Bit_Operations.bit_xor_iff) 

1188 

1189 
end 

1190 

1191 

1192 
subsubsection \<open>More\<close> 

1193 

1194 
lemma sint_greater_eq: 

1195 
\<open> (2 ^ (LENGTH('a)  Suc 0)) \<le> sint w\<close> for w :: \<open>'a::len word\<close> 

1196 
proof (cases \<open>bit w (LENGTH('a)  Suc 0)\<close>) 

1197 
case True 

1198 
then show ?thesis 

1199 
by transfer (simp add: signed_take_bit_eq_if_negative minus_exp_eq_not_mask or_greater_eq ac_simps) 

1200 
next 

1201 
have *: \<open> (2 ^ (LENGTH('a)  Suc 0)) \<le> (0::int)\<close> 

1202 
by simp 

1203 
case False 

1204 
then show ?thesis 

1205 
by transfer (auto simp add: signed_take_bit_eq intro: order_trans *) 

1206 
qed 

1207 

1208 
lemma sint_less: 

1209 
\<open>sint w < 2 ^ (LENGTH('a)  Suc 0)\<close> for w :: \<open>'a::len word\<close> 

1210 
by (cases \<open>bit w (LENGTH('a)  Suc 0)\<close>; transfer) 

1211 
(simp_all add: signed_take_bit_eq signed_take_bit_def not_eq_complement mask_eq_exp_minus_1 OR_upper) 

1212 

1213 
lemma unat_div_distrib: 

1214 
\<open>unat (v div w) = unat v div unat w\<close> 

1215 
proof transfer 

1216 
fix k l 

1217 
have \<open>nat (take_bit LENGTH('a) k) div nat (take_bit LENGTH('a) l) \<le> nat (take_bit LENGTH('a) k)\<close> 

1218 
by (rule div_le_dividend) 

1219 
also have \<open>nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\<close> 

1220 
by (simp add: nat_less_iff) 

1221 
finally show \<open>(nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) k div take_bit LENGTH('a) l) = 

1222 
(nat \<circ> take_bit LENGTH('a)) k div (nat \<circ> take_bit LENGTH('a)) l\<close> 

1223 
by (simp add: nat_take_bit_eq div_int_pos_iff nat_div_distrib take_bit_nat_eq_self_iff) 

1224 
qed 

1225 

1226 
lemma unat_mod_distrib: 

1227 
\<open>unat (v mod w) = unat v mod unat w\<close> 

1228 
proof transfer 

1229 
fix k l 

1230 
have \<open>nat (take_bit LENGTH('a) k) mod nat (take_bit LENGTH('a) l) \<le> nat (take_bit LENGTH('a) k)\<close> 

1231 
by (rule mod_less_eq_dividend) 

1232 
also have \<open>nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\<close> 

1233 
by (simp add: nat_less_iff) 

1234 
finally show \<open>(nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) k mod take_bit LENGTH('a) l) = 

1235 
(nat \<circ> take_bit LENGTH('a)) k mod (nat \<circ> take_bit LENGTH('a)) l\<close> 

1236 
by (simp add: nat_take_bit_eq mod_int_pos_iff less_le nat_mod_distrib take_bit_nat_eq_self_iff) 

1237 
qed 

1238 

1239 
lemma uint_div_distrib: 

1240 
\<open>uint (v div w) = uint v div uint w\<close> 

1241 
proof  

1242 
have \<open>int (unat (v div w)) = int (unat v div unat w)\<close> 

1243 
by (simp add: unat_div_distrib) 

1244 
then show ?thesis 

1245 
by (simp add: of_nat_div) 

1246 
qed 

1247 

1248 
lemma uint_mod_distrib: 

1249 
\<open>uint (v mod w) = uint v mod uint w\<close> 

1250 
proof  

1251 
have \<open>int (unat (v mod w)) = int (unat v mod unat w)\<close> 

1252 
by (simp add: unat_mod_distrib) 

1253 
then show ?thesis 

1254 
by (simp add: of_nat_mod) 

1255 
qed 

1256 

1257 
context semiring_bit_shifts 

1258 
begin 

1259 

1260 
lemma unsigned_ucast_eq: 

1261 
\<open>unsigned (ucast w :: 'c::len word) = take_bit LENGTH('c) (unsigned w)\<close> 

1262 
for w :: \<open>'b::len word\<close> 

1263 
by (rule bit_eqI) (simp add: bit_unsigned_iff Word.bit_unsigned_iff bit_take_bit_iff exp_eq_zero_iff not_le) 

1264 

1265 
end 

1266 

1267 
context ring_bit_operations 

1268 
begin 

1269 

1270 
lemma signed_ucast_eq: 

1271 
\<open>signed (ucast w :: 'c::len word) = signed_take_bit (LENGTH('c)  Suc 0) (unsigned w)\<close> 

1272 
for w :: \<open>'b::len word\<close> 

1273 
proof (rule bit_eqI) 

1274 
fix n 

1275 
assume \<open>2 ^ n \<noteq> 0\<close> 

1276 
then have \<open>2 ^ (min (LENGTH('c)  Suc 0) n) \<noteq> 0\<close> 

1277 
by (simp add: min_def) 

1278 
(metis (mono_tags) diff_diff_cancel exp_not_zero_imp_exp_diff_not_zero) 

1279 
then show \<open>bit (signed (ucast w :: 'c::len word)) n \<longleftrightarrow> bit (signed_take_bit (LENGTH('c)  Suc 0) (unsigned w)) n\<close> 

1280 
by (simp add: bit_signed_iff bit_unsigned_iff Word.bit_unsigned_iff bit_signed_take_bit_iff exp_eq_zero_iff not_le) 

1281 
qed 

1282 

1283 
lemma signed_scast_eq: 

1284 
\<open>signed (scast w :: 'c::len word) = signed_take_bit (LENGTH('c)  Suc 0) (signed w)\<close> 

1285 
for w :: \<open>'b::len word\<close> 

1286 
proof (rule bit_eqI) 

1287 
fix n 

1288 
assume \<open>2 ^ n \<noteq> 0\<close> 

1289 
then have \<open>2 ^ (min (LENGTH('c)  Suc 0) n) \<noteq> 0\<close> 

1290 
by (simp add: min_def) 

1291 
(metis (mono_tags) diff_diff_cancel exp_not_zero_imp_exp_diff_not_zero) 

1292 
then show \<open>bit (signed (scast w :: 'c::len word)) n \<longleftrightarrow> bit (signed_take_bit (LENGTH('c)  Suc 0) (signed w)) n\<close> 

1293 
by (simp add: bit_signed_iff bit_unsigned_iff Word.bit_signed_iff bit_signed_take_bit_iff exp_eq_zero_iff not_le) 

1294 
qed 

1295 

1296 
end 

1297 

72244  1298 
lemma uint_nonnegative: "0 \<le> uint w" 
72262  1299 
by (fact unsigned_greater_eq) 
72244  1300 

1301 
lemma uint_bounded: "uint w < 2 ^ LENGTH('a)" 

1302 
for w :: "'a::len word" 

72262  1303 
by (fact unsigned_less) 
72244  1304 

1305 
lemma uint_idem: "uint w mod 2 ^ LENGTH('a) = uint w" 

1306 
for w :: "'a::len word" 

72262  1307 
by transfer (simp add: take_bit_eq_mod) 
72244  1308 

1309 
lemma word_uint_eqI: "uint a = uint b \<Longrightarrow> a = b" 

72262  1310 
by (fact unsigned_word_eqI) 
72244  1311 

1312 
lemma word_uint_eq_iff: "a = b \<longleftrightarrow> uint a = uint b" 

72262  1313 
by (fact word_eq_iff_unsigned) 
1314 

1315 
lemma uint_word_of_int_eq: 

72244  1316 
\<open>uint (word_of_int k :: 'a::len word) = take_bit LENGTH('a) k\<close> 
1317 
by transfer rule 

1318 

1319 
lemma uint_word_of_int: "uint (word_of_int k :: 'a::len word) = k mod 2 ^ LENGTH('a)" 

1320 
by (simp add: uint_word_of_int_eq take_bit_eq_mod) 

1321 

1322 
lemma word_of_int_uint: "word_of_int (uint w) = w" 
