author  haftmann 
Mon, 07 Sep 2020 16:14:32 +0000  
changeset 72243  eaac77208cf9 
parent 72242  bb002df3e82e 
child 72244  4b011fa5e83b 
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 

27 
subsection \<open>Type definition and fundamental arithmetic\<close> 

37660  28 

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

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

32 
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

33 
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

34 

72243  35 
instantiation word :: (len) comm_ring_1 
36 
begin 

37 

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

39 
is 0 . 

40 

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

42 
is 1 . 

43 

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

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

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

47 

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

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

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

51 

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

53 
is uminus 

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

55 

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

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

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

59 

60 
instance 

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

62 

63 
end 

64 

65 
context 

66 
includes lifting_syntax 

67 
notes power_transfer [transfer_rule] 

68 
begin 

69 

70 
lemma power_transfer_word [transfer_rule]: 

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

72 
by transfer_prover 

73 

74 
end 

75 

76 

77 
subsection \<open>Basic code generation setup\<close> 

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

78 

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

79 
lift_definition uint :: \<open>'a::len word \<Rightarrow> int\<close> 
71948
6ede899d26d3
fundamental construction of word type following existing transfer rules
haftmann
parents:
71947
diff
changeset

80 
is \<open>take_bit LENGTH('a)\<close> . 
37660  81 

72243  82 
lemma [code abstype]: 
83 
\<open>Word.Word (uint w) = w\<close> 

84 
by transfer simp 

85 

86 
quickcheck_generator word 

87 
constructors: 

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

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

90 

91 
instantiation word :: (len) equal 

92 
begin 

93 

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

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

96 
by simp 

97 

98 
instance 

99 
by (standard; transfer) rule 

100 

101 
end 

102 

103 
lemma [code]: 

104 
\<open>HOL.equal v w \<longleftrightarrow> HOL.equal (uint v) (uint w)\<close> 

105 
by transfer (simp add: equal) 

106 

107 
lemma [code]: 

108 
\<open>uint 0 = 0\<close> 

109 
by transfer simp 

110 

111 
lemma [code]: 

112 
\<open>uint 1 = 1\<close> 

113 
by transfer simp 

114 

115 
lemma [code]: 

116 
\<open>uint (v + w) = take_bit LENGTH('a) (uint v + uint w)\<close> 

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

118 
by transfer (simp add: take_bit_add) 

119 

120 
lemma [code]: 

121 
\<open>uint ( w) = (let k = uint w in if w = 0 then 0 else 2 ^ LENGTH('a)  k)\<close> 

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

123 
by transfer (auto simp add: take_bit_eq_mod zmod_zminus1_eq_if) 

124 

125 
lemma [code]: 

126 
\<open>uint (v  w) = take_bit LENGTH('a) (uint v  uint w)\<close> 

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

128 
by transfer (simp add: take_bit_diff) 

129 

130 
lemma [code]: 

131 
\<open>uint (v * w) = take_bit LENGTH('a) (uint v * uint w)\<close> 

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

133 
by transfer (simp add: take_bit_mult) 

134 

135 

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

137 

138 
context 

139 
includes lifting_syntax 

140 
notes 

141 
transfer_rule_of_bool [transfer_rule] 

142 
transfer_rule_numeral [transfer_rule] 

143 
transfer_rule_of_nat [transfer_rule] 

144 
transfer_rule_of_int [transfer_rule] 

145 
begin 

146 

147 
lemma [transfer_rule]: 

148 
\<open>((=) ===> pcr_word) of_bool of_bool\<close> 

149 
by transfer_prover 

150 

151 
lemma [transfer_rule]: 

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

153 
by transfer_prover 

154 

155 
lemma [transfer_rule]: 

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

157 
by transfer_prover 

158 

159 
lemma [transfer_rule]: 

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

161 
proof  

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

163 
by transfer_prover 

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

165 
qed 

166 

167 
end 

168 

169 
lemma word_exp_length_eq_0 [simp]: 

170 
\<open>(2 :: 'a::len word) ^ LENGTH('a) = 0\<close> 

171 
by transfer simp 

172 

65268  173 
lemma uint_nonnegative: "0 \<le> uint w" 
71948
6ede899d26d3
fundamental construction of word type following existing transfer rules
haftmann
parents:
71947
diff
changeset

174 
by transfer simp 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46962
diff
changeset

175 

70185  176 
lemma uint_bounded: "uint w < 2 ^ LENGTH('a)" 
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

177 
for w :: "'a::len word" 
71948
6ede899d26d3
fundamental construction of word type following existing transfer rules
haftmann
parents:
71947
diff
changeset

178 
by transfer (simp add: take_bit_eq_mod) 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46962
diff
changeset

179 

70185  180 
lemma uint_idem: "uint w mod 2 ^ LENGTH('a) = uint w" 
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

181 
for w :: "'a::len word" 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46962
diff
changeset

182 
using uint_nonnegative uint_bounded by (rule mod_pos_pos_trivial) 
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46962
diff
changeset

183 

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

184 
lemma word_uint_eqI: "uint a = uint b \<Longrightarrow> a = b" 
6ede899d26d3
fundamental construction of word type following existing transfer rules
haftmann
parents:
71947
diff
changeset

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

186 

65268  187 
lemma word_uint_eq_iff: "a = b \<longleftrightarrow> uint a = uint b" 
71948
6ede899d26d3
fundamental construction of word type following existing transfer rules
haftmann
parents:
71947
diff
changeset

188 
using word_uint_eqI by auto 
70185  189 

72243  190 
lift_definition word_of_int :: \<open>int \<Rightarrow> 'a::len word\<close> 
191 
is \<open>\<lambda>k. k\<close> . 

192 

193 
lemma Word_eq_word_of_int [code_post]: 

194 
\<open>Word.Word = word_of_int\<close> 

195 
by rule (transfer, rule) 

196 

197 
lemma uint_word_of_int_eq [code]: 

198 
\<open>uint (word_of_int k :: 'a::len word) = take_bit LENGTH('a) k\<close> 

199 
by transfer rule 

200 

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

201 
lemma uint_word_of_int: "uint (word_of_int k :: 'a::len word) = k mod 2 ^ LENGTH('a)" 
72243  202 
by (simp add: uint_word_of_int_eq take_bit_eq_mod) 
71948
6ede899d26d3
fundamental construction of word type following existing transfer rules
haftmann
parents:
71947
diff
changeset

203 

65268  204 
lemma word_of_int_uint: "word_of_int (uint w) = w" 
71948
6ede899d26d3
fundamental construction of word type following existing transfer rules
haftmann
parents:
71947
diff
changeset

205 
by transfer simp 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46962
diff
changeset

206 

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

207 
lemma split_word_all: "(\<And>x::'a::len word. PROP P x) \<equiv> (\<And>x. PROP P (word_of_int x))" 
55816
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

208 
proof 
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

209 
fix x :: "'a word" 
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

210 
assume "\<And>x. PROP P (word_of_int x)" 
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

211 
then have "PROP P (word_of_int (uint x))" . 
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

212 
then show "PROP P x" by (simp add: word_of_int_uint) 
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

213 
qed 
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

214 

72079  215 
lift_definition sint :: \<open>'a::len word \<Rightarrow> int\<close> 
216 
\<comment> \<open>treats the mostsignificant bit as a sign bit\<close> 

217 
is \<open>signed_take_bit (LENGTH('a)  1)\<close> 

218 
by (simp add: signed_take_bit_decr_length_iff) 

219 

220 
lemma sint_uint [code]: 

221 
\<open>sint w = signed_take_bit (LENGTH('a)  1) (uint w)\<close> 

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

72128  223 
by (cases \<open>LENGTH('a)\<close>; transfer) (simp_all add: signed_take_bit_take_bit) 
72079  224 

225 
lift_definition unat :: \<open>'a::len word \<Rightarrow> nat\<close> 

226 
is \<open>nat \<circ> take_bit LENGTH('a)\<close> 

227 
by transfer simp 

228 

229 
lemma nat_uint_eq [simp]: 

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

231 
by transfer simp 

232 

233 
lemma unat_eq_nat_uint [code]: 

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

235 
by simp 

236 

237 
lift_definition ucast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close> 

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

239 
by simp 

240 

241 
lemma ucast_eq [code]: 

242 
\<open>ucast w = word_of_int (uint w)\<close> 

243 
by transfer simp 

244 

245 
lift_definition scast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close> 

246 
is \<open>signed_take_bit (LENGTH('a)  1)\<close> 

247 
by (simp flip: signed_take_bit_decr_length_iff) 

248 

249 
lemma scast_eq [code]: 

250 
\<open>scast w = word_of_int (sint w)\<close> 

251 
by transfer simp 

55816
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

252 

72243  253 
lemma uint_0_eq [simp]: 
254 
\<open>uint 0 = 0\<close> 

255 
by transfer simp 

256 

257 
lemma uint_1_eq [simp]: 

258 
\<open>uint 1 = 1\<close> 

259 
by transfer simp 

260 

261 
lemma word_m1_wi: " 1 = word_of_int ( 1)" 

262 
by transfer rule 

263 

264 
lemma uint_0_iff: "uint x = 0 \<longleftrightarrow> x = 0" 

265 
by (simp add: word_uint_eq_iff) 

266 

267 
lemma unat_0_iff: "unat x = 0 \<longleftrightarrow> x = 0" 

268 
by transfer (auto intro: antisym) 

269 

270 
lemma unat_0 [simp]: "unat 0 = 0" 

271 
by transfer simp 

272 

273 
lemma unat_gt_0: "0 < unat x \<longleftrightarrow> x \<noteq> 0" 

274 
by (auto simp: unat_0_iff [symmetric]) 

275 

276 
lemma ucast_0 [simp]: "ucast 0 = 0" 

277 
by transfer simp 

278 

279 
lemma sint_0 [simp]: "sint 0 = 0" 

280 
by (simp add: sint_uint) 

281 

282 
lemma scast_0 [simp]: "scast 0 = 0" 

283 
by transfer simp 

284 

285 
lemma sint_n1 [simp] : "sint ( 1) =  1" 

286 
by transfer simp 

287 

288 
lemma scast_n1 [simp]: "scast ( 1) =  1" 

289 
by transfer simp 

290 

291 
lemma uint_1: "uint (1::'a::len word) = 1" 

292 
by (fact uint_1_eq) 

293 

294 
lemma unat_1 [simp]: "unat (1::'a::len word) = 1" 

295 
by transfer simp 

296 

297 
lemma ucast_1 [simp]: "ucast (1::'a::len word) = 1" 

298 
by transfer simp 

299 

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

300 
instantiation word :: (len) size 
55816
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

301 
begin 
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

302 

72079  303 
lift_definition size_word :: \<open>'a word \<Rightarrow> nat\<close> 
304 
is \<open>\<lambda>_. LENGTH('a)\<close> .. 

55816
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

305 

e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

306 
instance .. 
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

307 

e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

308 
end 
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

309 

72079  310 
lemma word_size [code]: 
311 
\<open>size w = LENGTH('a)\<close> for w :: \<open>'a::len word\<close> 

312 
by (fact size_word.rep_eq) 

313 

65268  314 
lemma word_size_gt_0 [iff]: "0 < size w" 
315 
for w :: "'a::len word" 

55816
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

316 
by (simp add: word_size) 
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

317 

e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

318 
lemmas lens_gt_0 = word_size_gt_0 len_gt_0 
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

319 

e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

320 
lemma lens_not_0 [iff]: 
71942  321 
\<open>size w \<noteq> 0\<close> for w :: \<open>'a::len word\<close> 
55816
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

322 
by auto 
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

323 

72079  324 
lift_definition source_size :: \<open>('a::len word \<Rightarrow> 'b) \<Rightarrow> nat\<close> 
325 
is \<open>\<lambda>_. LENGTH('a)\<close> . 

326 

327 
lift_definition target_size :: \<open>('a \<Rightarrow> 'b::len word) \<Rightarrow> nat\<close> 

328 
is \<open>\<lambda>_. LENGTH('b)\<close> .. 

329 

330 
lift_definition is_up :: \<open>('a::len word \<Rightarrow> 'b::len word) \<Rightarrow> bool\<close> 

331 
is \<open>\<lambda>_. LENGTH('a) \<le> LENGTH('b)\<close> .. 

332 

333 
lift_definition is_down :: \<open>('a::len word \<Rightarrow> 'b::len word) \<Rightarrow> bool\<close> 

334 
is \<open>\<lambda>_. LENGTH('a) \<ge> LENGTH('b)\<close> .. 

335 

336 
lemma is_up_eq: 

337 
\<open>is_up f \<longleftrightarrow> source_size f \<le> target_size f\<close> 

338 
for f :: \<open>'a::len word \<Rightarrow> 'b::len word\<close> 

339 
by (simp add: source_size.rep_eq target_size.rep_eq is_up.rep_eq) 

340 

341 
lemma is_down_eq: 

342 
\<open>is_down f \<longleftrightarrow> target_size f \<le> source_size f\<close> 

343 
for f :: \<open>'a::len word \<Rightarrow> 'b::len word\<close> 

344 
by (simp add: source_size.rep_eq target_size.rep_eq is_down.rep_eq) 

345 

346 
lift_definition word_int_case :: \<open>(int \<Rightarrow> 'b) \<Rightarrow> 'a::len word \<Rightarrow> 'b\<close> 

347 
is \<open>\<lambda>f. f \<circ> take_bit LENGTH('a)\<close> by simp 

348 

349 
lemma word_int_case_eq_uint [code]: 

350 
\<open>word_int_case f w = f (uint w)\<close> 

351 
by transfer simp 

55816
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

352 

e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

353 
translations 
65268  354 
"case x of XCONST of_int y \<Rightarrow> b" \<rightleftharpoons> "CONST word_int_case (\<lambda>y. b) x" 
355 
"case x of (XCONST of_int :: 'a) y \<Rightarrow> b" \<rightharpoonup> "CONST word_int_case (\<lambda>y. b) x" 

55816
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

356 

e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

357 

61799  358 
subsection \<open>Typedefinition locale instantiations\<close> 
55816
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

359 

72043  360 
definition uints :: "nat \<Rightarrow> int set" 
361 
\<comment> \<open>the sets of integers representing the words\<close> 

72128  362 
where "uints n = range (take_bit n)" 
72043  363 

364 
definition sints :: "nat \<Rightarrow> int set" 

72128  365 
where "sints n = range (signed_take_bit (n  1))" 
72043  366 

367 
lemma uints_num: "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}" 

368 
by (simp add: uints_def range_bintrunc) 

369 

370 
lemma sints_num: "sints n = {i.  (2 ^ (n  1)) \<le> i \<and> i < 2 ^ (n  1)}" 

371 
by (simp add: sints_def range_sbintrunc) 

372 

373 
definition unats :: "nat \<Rightarrow> nat set" 

374 
where "unats n = {i. i < 2 ^ n}" 

375 

376 
\<comment> \<open>naturals\<close> 

377 
lemma uints_unats: "uints n = int ` unats n" 

378 
apply (unfold unats_def uints_num) 

379 
apply safe 

380 
apply (rule_tac image_eqI) 

381 
apply (erule_tac nat_0_le [symmetric]) 

382 
by auto 

383 

384 
lemma unats_uints: "unats n = nat ` uints n" 

385 
by (auto simp: uints_unats image_iff) 

386 

65268  387 
lemma td_ext_uint: 
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

388 
"td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (LENGTH('a::len))) 
70185  389 
(\<lambda>w::int. w mod 2 ^ LENGTH('a))" 
55816
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

390 
apply (unfold td_ext_def') 
71948
6ede899d26d3
fundamental construction of word type following existing transfer rules
haftmann
parents:
71947
diff
changeset

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

392 
apply (simp add: uints_num take_bit_eq_mod) 
55816
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

393 
done 
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

394 

e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

395 
interpretation word_uint: 
65268  396 
td_ext 
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

397 
"uint::'a::len word \<Rightarrow> int" 
65268  398 
word_of_int 
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

399 
"uints (LENGTH('a::len))" 
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

400 
"\<lambda>w. w mod 2 ^ LENGTH('a::len)" 
55816
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

401 
by (fact td_ext_uint) 
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

402 

e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

403 
lemmas td_uint = word_uint.td_thm 
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

404 
lemmas int_word_uint = word_uint.eq_norm 
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

405 

e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

406 
lemma td_ext_ubin: 
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

407 
"td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (LENGTH('a::len))) 
72128  408 
(take_bit (LENGTH('a)))" 
409 
apply standard 

410 
apply transfer 

411 
apply simp 

412 
done 

55816
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

413 

e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

414 
interpretation word_ubin: 
65268  415 
td_ext 
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

416 
"uint::'a::len word \<Rightarrow> int" 
65268  417 
word_of_int 
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

418 
"uints (LENGTH('a::len))" 
72128  419 
"take_bit (LENGTH('a::len))" 
55816
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

420 
by (fact td_ext_ubin) 
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

421 

72243  422 
lemma td_ext_unat [OF refl]: 
423 
"n = LENGTH('a::len) \<Longrightarrow> 

424 
td_ext (unat :: 'a word \<Rightarrow> nat) of_nat (unats n) (\<lambda>i. i mod 2 ^ n)" 

425 
apply (standard; transfer) 

426 
apply (simp_all add: unats_def take_bit_int_less_exp take_bit_of_nat take_bit_eq_self) 

427 
apply (simp add: take_bit_eq_mod) 

428 
done 

429 

430 
lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm] 

431 

432 
interpretation word_unat: 

433 
td_ext 

434 
"unat::'a::len word \<Rightarrow> nat" 

435 
of_nat 

436 
"unats (LENGTH('a::len))" 

437 
"\<lambda>i. i mod 2 ^ LENGTH('a::len)" 

438 
by (rule td_ext_unat) 

439 

440 
lemmas td_unat = word_unat.td_thm 

441 

442 
lemmas unat_lt2p [iff] = word_unat.Rep [unfolded unats_def mem_Collect_eq] 

443 

444 
lemma unat_le: "y \<le> unat z \<Longrightarrow> y \<in> unats (LENGTH('a))" 

445 
for z :: "'a::len word" 

446 
apply (unfold unats_def) 

447 
apply clarsimp 

448 
apply (rule xtrans, rule unat_lt2p, assumption) 

449 
done 

450 

451 
lemma td_ext_sbin: 

452 
"td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (LENGTH('a::len))) 

453 
(signed_take_bit (LENGTH('a)  1))" 

454 
apply (unfold td_ext_def' sint_uint) 

455 
apply (simp add : word_ubin.eq_norm) 

456 
apply (cases "LENGTH('a)") 

457 
apply (auto simp add : sints_def) 

458 
apply (rule sym [THEN trans]) 

459 
apply (rule word_ubin.Abs_norm) 

460 
apply (simp only: bintrunc_sbintrunc) 

461 
apply (drule sym) 

462 
apply simp 

463 
done 

464 

465 
lemma td_ext_sint: 

466 
"td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (LENGTH('a::len))) 

467 
(\<lambda>w. (w + 2 ^ (LENGTH('a)  1)) mod 2 ^ LENGTH('a)  

468 
2 ^ (LENGTH('a)  1))" 

469 
using td_ext_sbin [where ?'a = 'a] by (simp add: no_sbintr_alt2) 

470 

471 
text \<open> 

472 
We do \<open>sint\<close> before \<open>sbin\<close>, before \<open>sint\<close> is the user version 

473 
and interpretations do not produce thm duplicates. I.e. 

474 
we get the name \<open>word_sint.Rep_eqD\<close>, but not \<open>word_sbin.Req_eqD\<close>, 

475 
because the latter is the same thm as the former. 

476 
\<close> 

477 
interpretation word_sint: 

478 
td_ext 

479 
"sint ::'a::len word \<Rightarrow> int" 

480 
word_of_int 

481 
"sints (LENGTH('a::len))" 

482 
"\<lambda>w. (w + 2^(LENGTH('a::len)  1)) mod 2^LENGTH('a::len)  

483 
2 ^ (LENGTH('a::len)  1)" 

484 
by (rule td_ext_sint) 

485 

486 
interpretation word_sbin: 

487 
td_ext 

488 
"sint ::'a::len word \<Rightarrow> int" 

489 
word_of_int 

490 
"sints (LENGTH('a::len))" 

491 
"signed_take_bit (LENGTH('a::len)  1)" 

492 
by (rule td_ext_sbin) 

493 

494 
lemmas int_word_sint = td_ext_sint [THEN td_ext.eq_norm] 

495 

496 
lemmas td_sint = word_sint.td 

497 

55816
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

498 

61799  499 
subsection \<open>Arithmetic operations\<close> 
37660  500 

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

501 
instantiation word :: (len) "{neg_numeral, modulo, comm_monoid_mult, comm_ring}" 
37660  502 
begin 
503 

71950  504 
lift_definition divide_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" 
505 
is "\<lambda>a b. take_bit LENGTH('a) a div take_bit LENGTH('a) b" 

506 
by simp 

507 

508 
lift_definition modulo_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" 

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

510 
by simp 

37660  511 

47374
9475d524bafb
set up and use lift_definition for word operations
huffman
parents:
47372
diff
changeset

512 
instance 
61169  513 
by standard (transfer, simp add: algebra_simps)+ 
47374
9475d524bafb
set up and use lift_definition for word operations
huffman
parents:
47372
diff
changeset

514 

9475d524bafb
set up and use lift_definition for word operations
huffman
parents:
47372
diff
changeset

515 
end 
9475d524bafb
set up and use lift_definition for word operations
huffman
parents:
47372
diff
changeset

516 

71950  517 
lemma word_div_def [code]: 
518 
"a div b = word_of_int (uint a div uint b)" 

519 
by transfer rule 

520 

521 
lemma word_mod_def [code]: 

522 
"a mod b = word_of_int (uint a mod uint b)" 

523 
by transfer rule 

524 

525 

526 

61799  527 
text \<open>Legacy theorems:\<close> 
47374
9475d524bafb
set up and use lift_definition for word operations
huffman
parents:
47372
diff
changeset

528 

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

529 
lemma word_add_def [code]: 
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72128
diff
changeset

530 
"a + b = word_of_int (uint a + uint b)" 
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72128
diff
changeset

531 
by transfer (simp add: take_bit_add) 
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72128
diff
changeset

532 

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

533 
lemma word_sub_wi [code]: 
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72128
diff
changeset

534 
"a  b = word_of_int (uint a  uint b)" 
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72128
diff
changeset

535 
by transfer (simp add: take_bit_diff) 
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72128
diff
changeset

536 

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

537 
lemma word_mult_def [code]: 
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72128
diff
changeset

538 
"a * b = word_of_int (uint a * uint b)" 
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72128
diff
changeset

539 
by transfer (simp add: take_bit_eq_mod mod_simps) 
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72128
diff
changeset

540 

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

541 
lemma word_minus_def [code]: 
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72128
diff
changeset

542 
" a = word_of_int ( uint a)" 
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72128
diff
changeset

543 
by transfer (simp add: take_bit_minus) 
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72128
diff
changeset

544 

72243  545 
lemma word_0_wi: 
546 
"0 = word_of_int 0" 

547 
by transfer simp 

548 

549 
lemma word_1_wi: 

550 
"1 = word_of_int 1" 

551 
by transfer simp 

552 

553 
lift_definition word_succ :: "'a::len word \<Rightarrow> 'a word" is "\<lambda>x. x + 1" 

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

555 

556 
lift_definition word_pred :: "'a::len word \<Rightarrow> 'a word" is "\<lambda>x. x  1" 

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

558 

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

559 
lemma word_succ_alt [code]: 
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72128
diff
changeset

560 
"word_succ a = word_of_int (uint a + 1)" 
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72128
diff
changeset

561 
by transfer (simp add: take_bit_eq_mod mod_simps) 
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72128
diff
changeset

562 

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

563 
lemma word_pred_alt [code]: 
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72128
diff
changeset

564 
"word_pred a = word_of_int (uint a  1)" 
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72128
diff
changeset

565 
by transfer (simp add: take_bit_eq_mod mod_simps) 
9e5862223442
dedicated symbols for code generation, to pave way for generic conversions from and to word
haftmann
parents:
72128
diff
changeset

566 

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

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

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

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

570 
word_0_wi word_1_wi 
45545
26aebb8ac9c1
Word.thy: rearrange to instantiate arithmetic classes together with arithmetic operations
huffman
parents:
45544
diff
changeset

571 

65268  572 
lemma wi_homs: 
573 
shows wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)" 

574 
and wi_hom_sub: "word_of_int a  word_of_int b = word_of_int (a  b)" 

575 
and wi_hom_mult: "word_of_int a * word_of_int b = word_of_int (a * b)" 

576 
and wi_hom_neg: " word_of_int a = word_of_int ( a)" 

577 
and wi_hom_succ: "word_succ (word_of_int a) = word_of_int (a + 1)" 

578 
and wi_hom_pred: "word_pred (word_of_int a) = word_of_int (a  1)" 

47374
9475d524bafb
set up and use lift_definition for word operations
huffman
parents:
47372
diff
changeset

579 
by (transfer, simp)+ 
45545
26aebb8ac9c1
Word.thy: rearrange to instantiate arithmetic classes together with arithmetic operations
huffman
parents:
45544
diff
changeset

580 

26aebb8ac9c1
Word.thy: rearrange to instantiate arithmetic classes together with arithmetic operations
huffman
parents:
45544
diff
changeset

581 
lemmas wi_hom_syms = wi_homs [symmetric] 
26aebb8ac9c1
Word.thy: rearrange to instantiate arithmetic classes together with arithmetic operations
huffman
parents:
45544
diff
changeset

582 

46013  583 
lemmas word_of_int_homs = wi_homs word_0_wi word_1_wi 
46009  584 

585 
lemmas word_of_int_hom_syms = word_of_int_homs [symmetric] 

45545
26aebb8ac9c1
Word.thy: rearrange to instantiate arithmetic classes together with arithmetic operations
huffman
parents:
45544
diff
changeset

586 

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

587 
instance word :: (len) comm_monoid_add .. 
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

588 

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

589 
instance word :: (len) semiring_numeral .. 
71950  590 

45545
26aebb8ac9c1
Word.thy: rearrange to instantiate arithmetic classes together with arithmetic operations
huffman
parents:
45544
diff
changeset

591 
lemma word_of_nat: "of_nat n = word_of_int (int n)" 
26aebb8ac9c1
Word.thy: rearrange to instantiate arithmetic classes together with arithmetic operations
huffman
parents:
45544
diff
changeset

592 
by (induct n) (auto simp add : word_of_int_hom_syms) 
26aebb8ac9c1
Word.thy: rearrange to instantiate arithmetic classes together with arithmetic operations
huffman
parents:
45544
diff
changeset

593 

26aebb8ac9c1
Word.thy: rearrange to instantiate arithmetic classes together with arithmetic operations
huffman
parents:
45544
diff
changeset

594 
lemma word_of_int: "of_int = word_of_int" 
26aebb8ac9c1
Word.thy: rearrange to instantiate arithmetic classes together with arithmetic operations
huffman
parents:
45544
diff
changeset

595 
apply (rule ext) 
26aebb8ac9c1
Word.thy: rearrange to instantiate arithmetic classes together with arithmetic operations
huffman
parents:
45544
diff
changeset

596 
apply (case_tac x rule: int_diff_cases) 
46013  597 
apply (simp add: word_of_nat wi_hom_sub) 
45545
26aebb8ac9c1
Word.thy: rearrange to instantiate arithmetic classes together with arithmetic operations
huffman
parents:
45544
diff
changeset

598 
done 
26aebb8ac9c1
Word.thy: rearrange to instantiate arithmetic classes together with arithmetic operations
huffman
parents:
45544
diff
changeset

599 

71950  600 
lemma word_of_int_eq: 
601 
"word_of_int = of_int" 

602 
by (rule ext) (transfer, rule) 

603 

65268  604 
definition udvd :: "'a::len word \<Rightarrow> 'a::len word \<Rightarrow> bool" (infixl "udvd" 50) 
605 
where "a udvd b = (\<exists>n\<ge>0. uint b = n * uint a)" 

37660  606 

71950  607 
context 
608 
includes lifting_syntax 

609 
begin 

610 

611 
lemma [transfer_rule]: 

71958  612 
\<open>(pcr_word ===> (\<longleftrightarrow>)) even ((dvd) 2 :: 'a::len word \<Rightarrow> bool)\<close> 
71950  613 
proof  
614 
have even_word_unfold: "even k \<longleftrightarrow> (\<exists>l. take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l))" (is "?P \<longleftrightarrow> ?Q") 

615 
for k :: int 

616 
proof 

617 
assume ?P 

618 
then show ?Q 

619 
by auto 

620 
next 

621 
assume ?Q 

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

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

624 
by simp 

625 
then show ?P 

626 
by simp 

627 
qed 

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

629 
transfer_prover 

630 
qed 

631 

632 
end 

633 

71951  634 
instance word :: (len) semiring_modulo 
635 
proof 

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

637 
proof transfer 

638 
fix k l :: int 

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

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

641 
by (simp add: take_bit_eq_mod) 

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

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

644 
by (simp add: div_mult_mod_eq) 

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

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

647 
by (simp add: mod_add_left_eq) 

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

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

650 
by (simp add: mod_mult_right_eq) 

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

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

653 
by (simp add: mod_simps) 

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

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

656 
by simp 

657 
qed 

658 
qed 

659 

660 
instance word :: (len) semiring_parity 

661 
proof 

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

663 
by transfer simp 

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

665 
for a :: "'a word" 

666 
by transfer (simp_all add: mod_2_eq_odd take_bit_Suc) 

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

668 
for a :: "'a word" 

669 
by transfer (simp_all add: mod_2_eq_odd take_bit_Suc) 

670 
qed 

671 

71953  672 
lemma exp_eq_zero_iff: 
673 
\<open>2 ^ n = (0 :: 'a::len word) \<longleftrightarrow> n \<ge> LENGTH('a)\<close> 

674 
by transfer simp 

675 

71958  676 
lemma double_eq_zero_iff: 
677 
\<open>2 * a = 0 \<longleftrightarrow> a = 0 \<or> a = 2 ^ (LENGTH('a)  Suc 0)\<close> 

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

679 
proof  

680 
define n where \<open>n = LENGTH('a)  Suc 0\<close> 

681 
then have *: \<open>LENGTH('a) = Suc n\<close> 

682 
by simp 

683 
have \<open>a = 0\<close> if \<open>2 * a = 0\<close> and \<open>a \<noteq> 2 ^ (LENGTH('a)  Suc 0)\<close> 

684 
using that by transfer 

685 
(auto simp add: take_bit_eq_0_iff take_bit_eq_mod *) 

686 
moreover have \<open>2 ^ LENGTH('a) = (0 :: 'a word)\<close> 

687 
by transfer simp 

688 
then have \<open>2 * 2 ^ (LENGTH('a)  Suc 0) = (0 :: 'a word)\<close> 

689 
by (simp add: *) 

690 
ultimately show ?thesis 

691 
by auto 

692 
qed 

693 

45547  694 

61799  695 
subsection \<open>Ordering\<close> 
45547  696 

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

697 
instantiation word :: (len) linorder 
45547  698 
begin 
699 

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

702 
by simp 

703 

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

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

706 
by simp 

37660  707 

45547  708 
instance 
71950  709 
by (standard; transfer) auto 
45547  710 

711 
end 

712 

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

713 
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

714 
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

715 

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

716 
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

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

718 

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

721 
by transfer rule 

722 

723 
lemma word_less_def [code]: 

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

725 
by transfer rule 

726 

71951  727 
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

728 
\<open>a > 0 \<longleftrightarrow> a \<noteq> 0\<close> for a :: \<open>'a::len word\<close> 
71951  729 
by transfer (simp add: less_le) 
730 

731 
lemma of_nat_word_eq_iff: 

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

733 
by transfer (simp add: take_bit_of_nat) 

734 

735 
lemma of_nat_word_less_eq_iff: 

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

737 
by transfer (simp add: take_bit_of_nat) 

738 

739 
lemma of_nat_word_less_iff: 

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

741 
by transfer (simp add: take_bit_of_nat) 

742 

743 
lemma of_nat_word_eq_0_iff: 

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

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

746 

747 
lemma of_int_word_eq_iff: 

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

749 
by transfer rule 

750 

751 
lemma of_int_word_less_eq_iff: 

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

753 
by transfer rule 

754 

755 
lemma of_int_word_less_iff: 

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

757 
by transfer rule 

758 

759 
lemma of_int_word_eq_0_iff: 

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

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

762 

72079  763 
lift_definition word_sle :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> bool\<close> (\<open>(_/ <=s _)\<close> [50, 51] 50) 
764 
is \<open>\<lambda>k l. signed_take_bit (LENGTH('a)  1) k \<le> signed_take_bit (LENGTH('a)  1) l\<close> 

765 
by (simp flip: signed_take_bit_decr_length_iff) 

766 

767 
lemma word_sle_eq [code]: 

768 
\<open>a <=s b \<longleftrightarrow> sint a \<le> sint b\<close> 

769 
by transfer simp 

770 

771 
lift_definition word_sless :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> bool\<close> (\<open>(_/ <s _)\<close> [50, 51] 50) 

772 
is \<open>\<lambda>k l. signed_take_bit (LENGTH('a)  1) k < signed_take_bit (LENGTH('a)  1) l\<close> 

773 
by (simp flip: signed_take_bit_decr_length_iff) 

774 

775 
lemma word_sless_eq: 

776 
\<open>x <s y \<longleftrightarrow> x <=s y \<and> x \<noteq> y\<close> 

777 
by transfer (simp add: signed_take_bit_decr_length_iff less_le) 

778 

779 
lemma [code]: 

780 
\<open>a <s b \<longleftrightarrow> sint a < sint b\<close> 

781 
by transfer simp 

37660  782 

72243  783 
lemma word_less_alt: "a < b \<longleftrightarrow> uint a < uint b" 
784 
by (fact word_less_def) 

785 

786 
lemma signed_linorder: "class.linorder word_sle word_sless" 

787 
by (standard; transfer) (auto simp add: signed_take_bit_decr_length_iff) 

788 

789 
interpretation signed: linorder "word_sle" "word_sless" 

790 
by (rule signed_linorder) 

791 

792 
lemma word_zero_le [simp]: "0 \<le> y" 

793 
for y :: "'a::len word" 

794 
by transfer simp 

795 

796 
lemma word_m1_ge [simp] : "word_pred 0 \<ge> y" (* FIXME: delete *) 

797 
by transfer (simp add: take_bit_minus_one_eq_mask mask_eq_exp_minus_1 bintr_lt2p) 

798 

799 
lemma word_n1_ge [simp]: "y \<le> 1" 

800 
for y :: "'a::len word" 

801 
by (fact word_order.extremum) 

802 

803 
lemmas word_not_simps [simp] = 

804 
word_zero_le [THEN leD] word_m1_ge [THEN leD] word_n1_ge [THEN leD] 

805 

806 
lemma word_gt_0: "0 < y \<longleftrightarrow> 0 \<noteq> y" 

807 
for y :: "'a::len word" 

808 
by (simp add: less_le) 

809 

810 
lemmas word_gt_0_no [simp] = word_gt_0 [of "numeral y"] for y 

811 

812 
lemma word_sless_alt: "a <s b \<longleftrightarrow> sint a < sint b" 

813 
by (auto simp add: word_sle_eq word_sless_eq less_le) 

814 

815 
lemma word_le_nat_alt: "a \<le> b \<longleftrightarrow> unat a \<le> unat b" 

816 
by transfer (simp add: nat_le_eq_zle) 

817 

818 
lemma word_less_nat_alt: "a < b \<longleftrightarrow> unat a < unat b" 

819 
by transfer (auto simp add: less_le [of 0]) 

820 

821 
lemmas unat_mono = word_less_nat_alt [THEN iffD1] 

822 

823 
instance word :: (len) wellorder 

824 
proof 

825 
fix P :: "'a word \<Rightarrow> bool" and a 

826 
assume *: "(\<And>b. (\<And>a. a < b \<Longrightarrow> P a) \<Longrightarrow> P b)" 

827 
have "wf (measure unat)" .. 

828 
moreover have "{(a, b :: ('a::len) word). a < b} \<subseteq> measure unat" 

829 
by (auto simp add: word_less_nat_alt) 

830 
ultimately have "wf {(a, b :: ('a::len) word). a < b}" 

831 
by (rule wf_subset) 

832 
then show "P a" using * 

833 
by induction blast 

834 
qed 

835 

836 
lemma wi_less: 

837 
"(word_of_int n < (word_of_int m :: 'a::len word)) = 

838 
(n mod 2 ^ LENGTH('a) < m mod 2 ^ LENGTH('a))" 

839 
unfolding word_less_alt by (simp add: word_uint.eq_norm) 

840 

841 
lemma wi_le: 

842 
"(word_of_int n \<le> (word_of_int m :: 'a::len word)) = 

843 
(n mod 2 ^ LENGTH('a) \<le> m mod 2 ^ LENGTH('a))" 

844 
unfolding word_le_def by (simp add: word_uint.eq_norm) 

845 

37660  846 

61799  847 
subsection \<open>Bitwise operations\<close> 
37660  848 

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

851 
and word_even: \<open>\<And>a. P a \<Longrightarrow> 0 < a \<Longrightarrow> a < 2 ^ (LENGTH('a)  1) \<Longrightarrow> P (2 * a)\<close> 

852 
and word_odd: \<open>\<And>a. P a \<Longrightarrow> a < 2 ^ (LENGTH('a)  1) \<Longrightarrow> P (1 + 2 * a)\<close> 

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

854 
proof  

855 
define m :: nat where \<open>m = LENGTH('a)  1\<close> 

856 
then have l: \<open>LENGTH('a) = Suc m\<close> 

857 
by simp 

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

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

860 
by (unfold unat_def) (transfer, simp add: take_bit_eq_mod) 

861 
then have \<open>n < 2 * 2 ^ m\<close> 

862 
by (simp add: l) 

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

864 
proof (induction n rule: nat_bit_induct) 

865 
case zero 

866 
show ?case 

867 
by simp (rule word_zero) 

868 
next 

869 
case (even n) 

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

871 
by simp 

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

873 
by simp 

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

875 
by (auto simp add: word_greater_zero_iff of_nat_word_eq_0_iff l) 

876 
moreover from \<open>n < 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a)  1)\<close> 

877 
using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>] 

878 
by (cases \<open>m = 0\<close>) (simp_all add: not_less take_bit_eq_self ac_simps l) 

879 
ultimately have \<open>P (2 * of_nat n)\<close> 

880 
by (rule word_even) 

881 
then show ?case 

882 
by simp 

883 
next 

884 
case (odd n) 

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

886 
by simp 

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

888 
by simp 

889 
moreover from \<open>Suc n \<le> 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a)  1)\<close> 

890 
using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>] 

891 
by (cases \<open>m = 0\<close>) (simp_all add: not_less take_bit_eq_self ac_simps l) 

892 
ultimately have \<open>P (1 + 2 * of_nat n)\<close> 

893 
by (rule word_odd) 

894 
then show ?case 

895 
by simp 

896 
qed 

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

898 
by transfer simp 

899 
ultimately show ?thesis 

72079  900 
by (simp add: n_def) 
71951  901 
qed 
902 

903 
lemma bit_word_half_eq: 

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

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

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

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

908 
case False 

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

910 
by auto 

911 
with False that show ?thesis 

912 
by transfer (simp add: eq_iff) 

913 
next 

914 
case True 

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

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

917 
show ?thesis proof (cases b) 

918 
case False 

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

920 
using that proof transfer 

921 
fix k :: int 

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

923 
by simp 

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

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

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

927 
by (simp add: take_bit_eq_mod divmod_digit_0) 

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

929 
by (simp add: take_bit_eq_mod) 

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

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

932 
by simp 

933 
qed 

934 
ultimately show ?thesis 

935 
by simp 

936 
next 

937 
case True 

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

939 
using that proof transfer 

940 
fix k :: int 

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

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

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

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

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

946 
by (simp add: take_bit_eq_mod divmod_digit_0) 

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

948 
by (simp add: take_bit_eq_mod) 

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

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

951 
by (auto simp add: take_bit_Suc) 

952 
qed 

953 
ultimately show ?thesis 

954 
by simp 

955 
qed 

956 
qed 

957 

958 
lemma even_mult_exp_div_word_iff: 

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

960 
m \<le> n \<and> 

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

962 
by transfer 

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

964 
simp_all flip: push_bit_eq_mult add: bit_push_bit_iff_int) 

965 

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

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

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

968 

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

969 
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

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

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

973 
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

974 
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

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

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

977 
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

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

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

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

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

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

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

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

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

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

987 

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

988 
instance proof 
71951  989 
show \<open>P a\<close> if stable: \<open>\<And>a. a div 2 = a \<Longrightarrow> P a\<close> 
990 
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> 

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

992 
proof (induction a rule: word_bit_induct) 

993 
case zero 

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

995 
by transfer simp 

996 
with stable [of 0] show ?case 

997 
by simp 

998 
next 

999 
case (even a) 

1000 
with rec [of a False] show ?case 

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

1002 
next 

1003 
case (odd a) 

1004 
with rec [of a True] show ?case 

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

1006 
qed 

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

1007 
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

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

1011 
by transfer simp 

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

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

1014 
by transfer simp 

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

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

1017 
apply transfer 

1018 
apply (simp add: take_bit_eq_mod) 

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

1020 
apply simp_all 

1021 
apply (metis le_less mod_by_0 pos_mod_conj zero_less_numeral zero_less_power) 

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

1023 
proof  

1024 
fix aa :: int and ba :: int 

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

1026 
by (metis le_less take_bit_eq_mod take_bit_nonnegative) 

1027 
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)" 

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

1029 
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)" 

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

1031 
qed 

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

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

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

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

71951  1037 
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> 
1038 
for m n :: nat 

1039 
by transfer (simp, simp add: exp_div_exp_eq) 

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

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

1042 
apply transfer 

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

1044 
apply (simp add: drop_bit_take_bit) 

1045 
done 

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

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

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

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

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

1051 
using that apply transfer 

1052 
apply (auto simp flip: take_bit_eq_mod) 

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

1054 
done 

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

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

1057 
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) 

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

1059 
for m n :: nat 

1060 
by transfer (auto simp add: take_bit_of_mask even_mask_div_iff) 

1061 
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> 

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

1063 
proof transfer 

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

1065 
n < m 

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

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

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

1069 
by (auto simp flip: take_bit_eq_mod drop_bit_eq_div push_bit_eq_mult 

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

1071 
qed 

1072 
qed 

1073 

1074 
end 

1075 

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

1076 
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

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

1078 

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

1079 
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

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

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

1082 
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

1083 
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

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

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

1086 
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

1087 
= 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

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

1089 
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

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

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

1092 
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

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

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

1095 

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

1096 
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

1097 
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

1098 
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

1099 

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

1100 
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

1101 
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

1102 
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

1103 

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

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

1105 
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

1106 
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

1107 
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

1108 
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

1109 
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

1110 
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

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

1112 

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

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

1114 

71958  1115 
lemma bit_word_eqI: 
72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72083
diff
changeset

1116 
\<open>a = b\<close> if \<open>\<And>n. n < LENGTH('a) \<Longrightarrow> bit a n \<longleftrightarrow> bit b n\<close> 
71990  1117 
for a b :: \<open>'a::len word\<close> 
1118 
using that by transfer (auto simp add: nat_less_le bit_eq_iff bit_take_bit_iff) 

1119 

1120 
lemma bit_imp_le_length: 

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

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

1123 
using that by transfer simp 

1124 

1125 
lemma not_bit_length [simp]: 

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

1127 
by transfer simp 

1128 

72079  1129 
lemma uint_take_bit_eq [code]: 
1130 
\<open>uint (take_bit n w) = take_bit n (uint w)\<close> 

1131 
by transfer (simp add: ac_simps) 

1132 

72227  1133 
lemma take_bit_word_eq_self: 
1134 
\<open>take_bit n w = w\<close> if \<open>LENGTH('a) \<le> n\<close> for w :: \<open>'a::len word\<close> 

1135 
using that by transfer simp 

1136 

72027
759532ef0885
prefer canonically oriented lists of bits and more direct characterizations in definitions
haftmann
parents:
72010
diff
changeset

1137 
lemma take_bit_length_eq [simp]: 
759532ef0885
prefer canonically oriented lists of bits and more direct characterizations in definitions
haftmann
parents:
72010
diff
changeset

1138 
\<open>take_bit LENGTH('a) w = w\<close> for w :: \<open>'a::len word\<close> 
72227  1139 
by (rule take_bit_word_eq_self) simp 
72027
759532ef0885
prefer canonically oriented lists of bits and more direct characterizations in definitions
haftmann
parents:
72010
diff
changeset

1140 

71990  1141 
lemma bit_word_of_int_iff: 
1142 
\<open>bit (word_of_int k :: 'a::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> bit k n\<close> 

1143 
by transfer rule 

1144 

1145 
lemma bit_uint_iff: 

1146 
\<open>bit (uint w) n \<longleftrightarrow> n < LENGTH('a) \<and> bit w n\<close> 

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

1148 
by transfer (simp add: bit_take_bit_iff) 

1149 

1150 
lemma bit_sint_iff: 

1151 
\<open>bit (sint w) n \<longleftrightarrow> n \<ge> LENGTH('a) \<and> bit w (LENGTH('a)  1) \<or> bit w n\<close> 

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

72079  1153 
by transfer (auto simp add: bit_signed_take_bit_iff min_def le_less not_less) 
71990  1154 

1155 
lemma bit_word_ucast_iff: 

1156 
\<open>bit (ucast w :: 'b::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> n < LENGTH('b) \<and> bit w n\<close> 

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

72079  1158 
by transfer (simp add: bit_take_bit_iff ac_simps) 
71990  1159 

1160 
lemma bit_word_scast_iff: 

1161 
\<open>bit (scast w :: 'b::len word) n \<longleftrightarrow> 

1162 
n < LENGTH('b) \<and> (bit w n \<or> LENGTH('a) \<le> n \<and> bit w (LENGTH('a)  Suc 0))\<close> 

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

72079  1164 
by transfer (auto simp add: bit_signed_take_bit_iff le_less min_def) 
1165 

1166 
lift_definition shiftl1 :: \<open>'a::len word \<Rightarrow> 'a word\<close> 

1167 
is \<open>(*) 2\<close> 

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

1169 

1170 
lemma shiftl1_eq: 

1171 
\<open>shiftl1 w = word_of_int (2 * uint w)\<close> 

1172 
by transfer (simp add: take_bit_eq_mod mod_simps) 

70191  1173 

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

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

1175 
\<open>shiftl1 = (*) 2\<close> 
72079  1176 
by (rule ext, transfer) simp 
71952
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

1177 

71990  1178 
lemma bit_shiftl1_iff: 
1179 
\<open>bit (shiftl1 w) n \<longleftrightarrow> 0 < n \<and> n < LENGTH('a) \<and> bit w (n  1)\<close> 

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

1181 
by (simp add: shiftl1_eq_mult_2 bit_double_iff exp_eq_zero_iff not_le) (simp add: ac_simps) 

1182 

72079  1183 
lift_definition shiftr1 :: \<open>'a::len word \<Rightarrow> 'a word\<close> 
70191  1184 
\<comment> \<open>shift right as unsigned or as signed, ie logical or arithmetic\<close> 
72079  1185 
is \<open>\<lambda>k. take_bit LENGTH('a) k div 2\<close> by simp 
70191  1186 

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

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

1188 
\<open>shiftr1 w = w div 2\<close> 
72079  1189 
by transfer simp 
71952
2efc5b8c7456
canonical bit shifts for word type, leaving duplicates as they are at the moment
haftmann
parents:
71951
diff
changeset

1190 

71990  1191 
lemma bit_shiftr1_iff: 
1192 
\<open>bit (shiftr1 w) n \<longleftrightarrow> bit w (Suc n)\<close> 

72079  1193 
by transfer (auto simp flip: bit_Suc simp add: bit_take_bit_iff) 
1194 

1195 
lemma shiftr1_eq: 

72128  1196 
\<open>shiftr1 w = word_of_int (uint w div 2)\<close> 
72079  1197 
by transfer simp 
71990  1198 

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

1199 
instantiation word :: (len) ring_bit_operations 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71955
diff
changeset

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

1201 

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

1202 
lift_definition not_word :: \<open>'a word \<Rightarrow> 'a word\<close> 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71955
diff
changeset

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

1204 
by (simp add: take_bit_not_iff) 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71955
diff
changeset

1205 

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

1206 
lift_definition and_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close> 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71955
diff
changeset

1207 
is \<open>and\<close> 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71955
diff
changeset

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

1209 

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

1210 
lift_definition or_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close> 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71955
diff
changeset

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

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

1213 

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

1214 
lift_definition xor_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close> 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71955
diff
changeset

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

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

1217 

72082  1218 
lift_definition mask_word :: \<open>nat \<Rightarrow> 'a word\<close> 
1219 
is mask 

1220 
. 

1221 

1222 
instance by (standard; transfer) 

1223 
(auto simp add: minus_eq_not_minus_1 mask_eq_exp_minus_1 

1224 
bit_not_iff bit_and_iff bit_or_iff bit_xor_iff) 

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

1225 

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

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

1227 

72009  1228 
context 
1229 
includes lifting_syntax 

1230 
begin 

1231 

72079  1232 
lemma set_bit_word_transfer [transfer_rule]: 
72009  1233 
\<open>((=) ===> pcr_word ===> pcr_word) set_bit set_bit\<close> 
1234 
by (unfold set_bit_def) transfer_prover 

1235 

72079  1236 
lemma unset_bit_word_transfer [transfer_rule]: 
72009  1237 
\<open>((=) ===> pcr_word ===> pcr_word) unset_bit unset_bit\<close> 
1238 
by (unfold unset_bit_def) transfer_prover 

1239 

72079  1240 
lemma flip_bit_word_transfer [transfer_rule]: 
72009  1241 
\<open>((=) ===> pcr_word ===> pcr_word) flip_bit flip_bit\<close> 
1242 
by (unfold flip_bit_def) transfer_prover 

1243 

72242  1244 
lemma signed_take_bit_word_transfer [transfer_rule]: 
1245 
\<open>((=) ===> pcr_word ===> pcr_word) 

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

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

1248 
proof  

1249 
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> 

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

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

1252 
by transfer_prover 

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

1254 
by (simp add: fun_eq_iff signed_take_bit_def bit_take_bit_iff ac_simps) 

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

1256 
by (simp add: fun_eq_iff signed_take_bit_def) 

1257 
finally show ?thesis . 

1258 
qed 

1259 

72009  1260 
end 
1261 

72000  1262 
instantiation word :: (len) semiring_bit_syntax 
37660  1263 
begin 
1264 

72079  1265 
lift_definition test_bit_word :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> bool\<close> 
1266 
is \<open>\<lambda>k n. n < LENGTH('a) \<and> bit k n\<close> 

1267 
proof 

1268 
fix k l :: int and n :: nat 

1269 
assume *: \<open>take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close> 

1270 
show \<open>n < LENGTH('a) \<and> bit k n \<longleftrightarrow> n < LENGTH('a) \<and> bit l n\<close> 

1271 
proof (cases \<open>n < LENGTH('a)\<close>) 

1272 
case True 

1273 
from * have \<open>bit (take_bit LENGTH('a) k) n \<longleftrightarrow> bit (take_bit LENGTH('a) l) n\<close> 

1274 
by simp 

1275 
then show ?thesis 

1276 
by (simp add: bit_take_bit_iff) 

1277 
next 

1278 
case False 

1279 
then show ?thesis 

1280 
by simp 

1281 
qed 

1282 
qed 

37660  1283 

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

1284 
lemma test_bit_word_eq: 
72079  1285 
\<open>test_bit = (bit :: 'a word \<Rightarrow> _)\<close> 
1286 
by transfer simp 

1287 

72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72083
diff
changeset

1288 
lemma bit_word_iff_drop_bit_and [code]: 
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72083
diff
changeset

1289 
\<open>bit a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close> for a :: \<open>'a::len word\<close> 
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72083
diff
changeset

1290 
by (simp add: bit_iff_odd_drop_bit odd_iff_mod_2_eq_one and_one_eq) 
72079  1291 

1292 
lemma [code]: 

72088
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72083
diff
changeset

1293 
\<open>test_bit a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close> for a :: \<open>'a::len word\<close> 
a36db1c8238e
separation of reversed bit lists from other material
haftmann
parents:
72083
diff
changeset

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

1295 

72079  1296 
lift_definition shiftl_word :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> 'a word\<close> 
1297 
is \<open>\<lambda>k n. push_bit n k\<close> 

1298 
proof  

1299 
show \<open>take_bit LENGTH('a) (push_bit n k) = take_bit LENGTH('a) (push_bit n l)\<close> 

1300 
if \<open>take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close> for k l :: int and n :: nat 

1301 
proof  

1302 
from that 

1303 
have \<open>take_bit (LENGTH('a)  n) (take_bit LENGTH('a) k) 

1304 
= take_bit (LENGTH('a)  n) (take_bit LENGTH('a) l)\<close> 

1305 
by simp 

1306 
moreover have \<open>min (LENGTH('a)  n) LENGTH('a) = LENGTH('a)  n\<close> 

1307 
by simp 

1308 
ultimately show ?thesis 

1309 
by (simp add: take_bit_push_bit) 

1310 
qed 

1311 
qed 

1312 

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

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

1314 
\<open>w << n = push_bit n w\<close> for w :: \<open>'a::len word\<close> 
72079  1315 
by transfer rule 
1316 

1317 
lift_definition shiftr_word :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> 'a word\<close> 

1318 
is \<open>\<lambda>k n. drop_bit n (take_bit LENGTH('a) k)\<close> by simp 

1319 

72000  1320 
lemma shiftr_word_eq: 
1321 
\<open>w >> n = drop_bit n w\<close> for w :: \<open>'a::len word\<close> 

72079  1322 
by transfer simp 
1323 

1324 
instance 
