author  haftmann 
Tue, 04 Aug 2020 09:33:05 +0000  
changeset 72082  41393ecb57ac 
parent 72079  8c355e2dd7db 
permissions  rwrr 
64015  1 
(* Author: Florian Haftmann, TUM 
2 
*) 

3 

4 
section \<open>Proof of concept for algebraically founded bit word types\<close> 

5 

71042
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

6 
theory Word 
64015  7 
imports 
8 
Main 

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

9 
"HOLLibrary.Type_Length" 
71956  10 
"HOLLibrary.Bit_Operations" 
64015  11 
begin 
12 

13 
subsection \<open>Bit strings as quotient type\<close> 

14 

15 
subsubsection \<open>Basic properties\<close> 

16 

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

17 
quotient_type (overloaded) 'a word = int / "\<lambda>k l. take_bit LENGTH('a) k = take_bit LENGTH('a::len) l" 
64015  18 
by (auto intro!: equivpI reflpI sympI transpI) 
19 

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

20 
instantiation word :: (len) "{semiring_numeral, comm_semiring_0, comm_ring}" 
64015  21 
begin 
22 

23 
lift_definition zero_word :: "'a word" 

24 
is 0 

25 
. 

26 

27 
lift_definition one_word :: "'a word" 

28 
is 1 

29 
. 

30 

31 
lift_definition plus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" 

32 
is plus 

67961  33 
by (subst take_bit_add [symmetric]) (simp add: take_bit_add) 
64015  34 

35 
lift_definition uminus_word :: "'a word \<Rightarrow> 'a word" 

36 
is uminus 

71424  37 
by (subst take_bit_minus [symmetric]) (simp add: take_bit_minus) 
64015  38 

39 
lift_definition minus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" 

40 
is minus 

71424  41 
by (subst take_bit_diff [symmetric]) (simp add: take_bit_diff) 
64015  42 

43 
lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" 

44 
is times 

67907
02a14c1cb917
prefer convention to place operation name before type name
haftmann
parents:
67816
diff
changeset

45 
by (auto simp add: take_bit_eq_mod intro: mod_mult_cong) 
64015  46 

47 
instance 

48 
by standard (transfer; simp add: algebra_simps)+ 

49 

50 
end 

51 

52 
instance word :: (len) comm_ring_1 

53 
by standard (transfer; simp)+ 

54 

70903  55 
quickcheck_generator word 
56 
constructors: 

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

57 
"zero_class.zero :: ('a::len) word", 
13bb3f5cdc5b
pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
haftmann
parents:
71921
diff
changeset

58 
"numeral :: num \<Rightarrow> ('a::len) word", 
13bb3f5cdc5b
pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
haftmann
parents:
71921
diff
changeset

59 
"uminus :: ('a::len) word \<Rightarrow> ('a::len) word" 
70903  60 

70973  61 
context 
62 
includes lifting_syntax 

63 
notes power_transfer [transfer_rule] 

64 
begin 

65 

66 
lemma power_transfer_word [transfer_rule]: 

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

68 
by transfer_prover 

69 

70 
end 

71 

64015  72 

73 
subsubsection \<open>Conversions\<close> 

74 

70927  75 
context 
76 
includes lifting_syntax 

71182  77 
notes 
78 
transfer_rule_of_bool [transfer_rule] 

79 
transfer_rule_numeral [transfer_rule] 

70927  80 
transfer_rule_of_nat [transfer_rule] 
81 
transfer_rule_of_int [transfer_rule] 

82 
begin 

70348
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

83 

bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

84 
lemma [transfer_rule]: 
71182  85 
"((=) ===> (pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool)) of_bool of_bool" 
86 
by transfer_prover 

87 

88 
lemma [transfer_rule]: 

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

89 
"((=) ===> (pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool)) numeral numeral" 
70927  90 
by transfer_prover 
91 

92 
lemma [transfer_rule]: 

93 
"((=) ===> pcr_word) int of_nat" 

94 
by transfer_prover 

71042
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

95 

64015  96 
lemma [transfer_rule]: 
70927  97 
"((=) ===> pcr_word) (\<lambda>k. k) of_int" 
64015  98 
proof  
70927  99 
have "((=) ===> pcr_word) of_int of_int" 
64015  100 
by transfer_prover 
101 
then show ?thesis by (simp add: id_def) 

102 
qed 

103 

70927  104 
end 
105 

70973  106 
lemma abs_word_eq: 
107 
"abs_word = of_int" 

108 
by (rule ext) (transfer, rule) 

109 

64015  110 
context semiring_1 
111 
begin 

112 

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

113 
lift_definition unsigned :: "'b::len word \<Rightarrow> 'a" 
67907
02a14c1cb917
prefer convention to place operation name before type name
haftmann
parents:
67816
diff
changeset

114 
is "of_nat \<circ> nat \<circ> take_bit LENGTH('b)" 
64015  115 
by simp 
116 

117 
lemma unsigned_0 [simp]: 

118 
"unsigned 0 = 0" 

119 
by transfer simp 

120 

121 
end 

122 

123 
context semiring_char_0 

124 
begin 

125 

126 
lemma word_eq_iff_unsigned: 

127 
"a = b \<longleftrightarrow> unsigned a = unsigned b" 

128 
by safe (transfer; simp add: eq_nat_nat_iff) 

129 

130 
end 

131 

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

132 
instantiation word :: (len) equal 
70903  133 
begin 
134 

135 
definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" 

136 
where "equal_word a b \<longleftrightarrow> (unsigned a :: int) = unsigned b" 

137 

138 
instance proof 

139 
fix a b :: "'a word" 

140 
show "HOL.equal a b \<longleftrightarrow> a = b" 

141 
using word_eq_iff_unsigned [of a b] by (auto simp add: equal_word_def) 

142 
qed 

143 

144 
end 

145 

64015  146 
context ring_1 
147 
begin 

148 

149 
lift_definition signed :: "'b::len word \<Rightarrow> 'a" 

67907
02a14c1cb917
prefer convention to place operation name before type name
haftmann
parents:
67816
diff
changeset

150 
is "of_int \<circ> signed_take_bit (LENGTH('b)  1)" 
72010  151 
by (cases \<open>LENGTH('b)\<close>) 
152 
(simp_all add: signed_take_bit_eq_iff_take_bit_eq [symmetric]) 

64015  153 

154 
lemma signed_0 [simp]: 

155 
"signed 0 = 0" 

156 
by transfer simp 

157 

158 
end 

159 

160 
lemma unsigned_of_nat [simp]: 

67907
02a14c1cb917
prefer convention to place operation name before type name
haftmann
parents:
67816
diff
changeset

161 
"unsigned (of_nat n :: 'a word) = take_bit LENGTH('a::len) n" 
02a14c1cb917
prefer convention to place operation name before type name
haftmann
parents:
67816
diff
changeset

162 
by transfer (simp add: nat_eq_iff take_bit_eq_mod zmod_int) 
64015  163 

164 
lemma of_nat_unsigned [simp]: 

165 
"of_nat (unsigned a) = a" 

166 
by transfer simp 

167 

168 
lemma of_int_unsigned [simp]: 

169 
"of_int (unsigned a) = a" 

170 
by transfer simp 

171 

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

173 
\<open>unsigned a < (2 ^ LENGTH('a) :: nat)\<close> for a :: \<open>'a::len word\<close> 
70973  174 
by transfer (simp add: take_bit_eq_mod) 
175 

176 
lemma unsigned_int_less: 

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

177 
\<open>unsigned a < (2 ^ LENGTH('a) :: int)\<close> for a :: \<open>'a::len word\<close> 
70973  178 
by transfer (simp add: take_bit_eq_mod) 
179 

64015  180 
context ring_char_0 
181 
begin 

182 

183 
lemma word_eq_iff_signed: 

184 
"a = b \<longleftrightarrow> signed a = signed b" 

67907
02a14c1cb917
prefer convention to place operation name before type name
haftmann
parents:
67816
diff
changeset

185 
by safe (transfer; auto simp add: signed_take_bit_eq_iff_take_bit_eq) 
64015  186 

187 
end 

188 

189 
lemma signed_of_int [simp]: 

67907
02a14c1cb917
prefer convention to place operation name before type name
haftmann
parents:
67816
diff
changeset

190 
"signed (of_int k :: 'a word) = signed_take_bit (LENGTH('a::len)  1) k" 
64015  191 
by transfer simp 
192 

193 
lemma of_int_signed [simp]: 

194 
"of_int (signed a) = a" 

72079  195 
by transfer (simp_all add: take_bit_signed_take_bit) 
64015  196 

197 

198 
subsubsection \<open>Properties\<close> 

199 

71196  200 
lemma exp_eq_zero_iff: 
201 
\<open>(2 :: 'a::len word) ^ n = 0 \<longleftrightarrow> LENGTH('a) \<le> n\<close> 

202 
by transfer simp 

203 

64015  204 

205 
subsubsection \<open>Division\<close> 

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:
71921
diff
changeset

207 
instantiation word :: (len) modulo 
64015  208 
begin 
209 

210 
lift_definition divide_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" 

67907
02a14c1cb917
prefer convention to place operation name before type name
haftmann
parents:
67816
diff
changeset

211 
is "\<lambda>a b. take_bit LENGTH('a) a div take_bit LENGTH('a) b" 
64015  212 
by simp 
213 

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

67907
02a14c1cb917
prefer convention to place operation name before type name
haftmann
parents:
67816
diff
changeset

215 
is "\<lambda>a b. take_bit LENGTH('a) a mod take_bit LENGTH('a) b" 
64015  216 
by simp 
217 

218 
instance .. 

219 

220 
end 

221 

70973  222 
lemma zero_word_div_eq [simp]: 
71954
13bb3f5cdc5b
pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
haftmann
parents:
71921
diff
changeset

223 
\<open>0 div a = 0\<close> for a :: \<open>'a::len word\<close> 
70973  224 
by transfer simp 
225 

226 
lemma div_zero_word_eq [simp]: 

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

227 
\<open>a div 0 = 0\<close> for a :: \<open>'a::len word\<close> 
70973  228 
by transfer simp 
229 

70927  230 
context 
231 
includes lifting_syntax 

232 
begin 

233 

70348
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

234 
lemma [transfer_rule]: 
70927  235 
"(pcr_word ===> (\<longleftrightarrow>)) even ((dvd) 2 :: 'a::len word \<Rightarrow> bool)" 
70348
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

236 
proof  
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

237 
have even_word_unfold: "even k \<longleftrightarrow> (\<exists>l. take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l))" (is "?P \<longleftrightarrow> ?Q") 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

238 
for k :: int 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

239 
proof 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

240 
assume ?P 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

241 
then show ?Q 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

242 
by auto 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

243 
next 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

244 
assume ?Q 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

245 
then obtain l where "take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l)" .. 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

246 
then have "even (take_bit LENGTH('a) k)" 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

247 
by simp 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

248 
then show ?P 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

249 
by simp 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

250 
qed 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

251 
show ?thesis by (simp only: even_word_unfold [abs_def] dvd_def [where ?'a = "'a word", abs_def]) 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

252 
transfer_prover 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

253 
qed 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

254 

70927  255 
end 
256 

70348
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

257 
instance word :: (len) semiring_modulo 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

258 
proof 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

259 
show "a div b * b + a mod b = a" for a b :: "'a word" 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

260 
proof transfer 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

261 
fix k l :: int 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

262 
define r :: int where "r = 2 ^ LENGTH('a)" 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

263 
then have r: "take_bit LENGTH('a) k = k mod r" for k 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

264 
by (simp add: take_bit_eq_mod) 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

265 
have "k mod r = ((k mod r) div (l mod r) * (l mod r) 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

266 
+ (k mod r) mod (l mod r)) mod r" 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

267 
by (simp add: div_mult_mod_eq) 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

268 
also have "... = (((k mod r) div (l mod r) * (l mod r)) mod r 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

269 
+ (k mod r) mod (l mod r)) mod r" 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

270 
by (simp add: mod_add_left_eq) 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

271 
also have "... = (((k mod r) div (l mod r) * l) mod r 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

272 
+ (k mod r) mod (l mod r)) mod r" 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

273 
by (simp add: mod_mult_right_eq) 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

274 
finally have "k mod r = ((k mod r) div (l mod r) * l 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

275 
+ (k mod r) mod (l mod r)) mod r" 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

276 
by (simp add: mod_simps) 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

277 
with r show "take_bit LENGTH('a) (take_bit LENGTH('a) k div take_bit LENGTH('a) l * l 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

278 
+ take_bit LENGTH('a) k mod take_bit LENGTH('a) l) = take_bit LENGTH('a) k" 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

279 
by simp 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

280 
qed 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

281 
qed 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

282 

bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

283 
instance word :: (len) semiring_parity 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

284 
proof 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

285 
show "\<not> 2 dvd (1::'a word)" 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

286 
by transfer simp 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

287 
show even_iff_mod_2_eq_0: "2 dvd a \<longleftrightarrow> a mod 2 = 0" 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

288 
for a :: "'a word" 
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71443
diff
changeset

289 
by transfer (simp_all add: mod_2_eq_odd take_bit_Suc) 
70348
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

290 
show "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1" 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

291 
for a :: "'a word" 
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71443
diff
changeset

292 
by transfer (simp_all add: mod_2_eq_odd take_bit_Suc) 
70348
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

293 
qed 
bde161c740ca
more theorems for proof of concept for word type
haftmann
parents:
70171
diff
changeset

294 

64015  295 

296 
subsubsection \<open>Orderings\<close> 

297 

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

298 
instantiation word :: (len) linorder 
64015  299 
begin 
300 

301 
lift_definition less_eq_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" 

67907
02a14c1cb917
prefer convention to place operation name before type name
haftmann
parents:
67816
diff
changeset

302 
is "\<lambda>a b. take_bit LENGTH('a) a \<le> take_bit LENGTH('a) b" 
64015  303 
by simp 
304 

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

67907
02a14c1cb917
prefer convention to place operation name before type name
haftmann
parents:
67816
diff
changeset

306 
is "\<lambda>a b. take_bit LENGTH('a) a < take_bit LENGTH('a) b" 
64015  307 
by simp 
308 

309 
instance 

310 
by standard (transfer; auto)+ 

311 

312 
end 

313 

314 
context linordered_semidom 

315 
begin 

316 

317 
lemma word_less_eq_iff_unsigned: 

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

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

320 

321 
lemma word_less_iff_unsigned: 

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

67907
02a14c1cb917
prefer convention to place operation name before type name
haftmann
parents:
67816
diff
changeset

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

325 
end 

326 

70973  327 
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:
71921
diff
changeset

328 
\<open>a > 0 \<longleftrightarrow> a \<noteq> 0\<close> for a :: \<open>'a::len word\<close> 
70973  329 
by transfer (simp add: less_le) 
330 

331 
lemma of_nat_word_eq_iff: 

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

333 
by transfer (simp add: take_bit_of_nat) 

334 

335 
lemma of_nat_word_less_eq_iff: 

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

337 
by transfer (simp add: take_bit_of_nat) 

338 

339 
lemma of_nat_word_less_iff: 

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

341 
by transfer (simp add: take_bit_of_nat) 

342 

343 
lemma of_nat_word_eq_0_iff: 

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

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

346 

347 
lemma of_int_word_eq_iff: 

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

349 
by transfer rule 

350 

351 
lemma of_int_word_less_eq_iff: 

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

353 
by transfer rule 

354 

355 
lemma of_int_word_less_iff: 

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

357 
by transfer rule 

358 

359 
lemma of_int_word_eq_0_iff: 

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

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

362 

363 

364 
subsection \<open>Bit structure on \<^typ>\<open>'a word\<close>\<close> 

365 

366 
lemma word_bit_induct [case_names zero even odd]: 

367 
\<open>P a\<close> if word_zero: \<open>P 0\<close> 

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

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

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

371 
proof  

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

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

374 
by simp 

375 
define n :: nat where \<open>n = unsigned a\<close> 

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

377 
by (simp add: unsigned_nat_less) 

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

379 
by (simp add: l) 

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

381 
proof (induction n rule: nat_bit_induct) 

382 
case zero 

383 
show ?case 

384 
by simp (rule word_zero) 

385 
next 

386 
case (even n) 

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

388 
by simp 

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

390 
by simp 

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

392 
by (auto simp add: word_greater_zero_iff of_nat_word_eq_0_iff l) 

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

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

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

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

397 
by (rule word_even) 

398 
then show ?case 

399 
by simp 

400 
next 

401 
case (odd n) 

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

403 
by simp 

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

405 
by simp 

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

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

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

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

410 
by (rule word_odd) 

411 
then show ?case 

412 
by simp 

413 
qed 

414 
then show ?thesis 

415 
by (simp add: n_def) 

416 
qed 

417 

71042
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

418 
lemma bit_word_half_eq: 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

419 
\<open>(of_bool b + a * 2) div 2 = a\<close> 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

420 
if \<open>a < 2 ^ (LENGTH('a)  Suc 0)\<close> 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

421 
for a :: \<open>'a::len word\<close> 
71195  422 
proof (cases \<open>2 \<le> LENGTH('a::len)\<close>) 
423 
case False 

71042
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

424 
have \<open>of_bool (odd k) < (1 :: int) \<longleftrightarrow> even k\<close> for k :: int 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

425 
by auto 
71195  426 
with False that show ?thesis 
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71443
diff
changeset

427 
by transfer (simp add: eq_iff) 
71042
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

428 
next 
71195  429 
case True 
71042
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

430 
obtain n where length: \<open>LENGTH('a) = Suc n\<close> 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

431 
by (cases \<open>LENGTH('a)\<close>) simp_all 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

432 
show ?thesis proof (cases b) 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

433 
case False 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

434 
moreover have \<open>a * 2 div 2 = a\<close> 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

435 
using that proof transfer 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

436 
fix k :: int 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

437 
from length have \<open>k * 2 mod 2 ^ LENGTH('a) = (k mod 2 ^ n) * 2\<close> 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

438 
by simp 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

439 
moreover assume \<open>take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a)  Suc 0))\<close> 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

440 
with \<open>LENGTH('a) = Suc n\<close> 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

441 
have \<open>k mod 2 ^ LENGTH('a) = k mod 2 ^ n\<close> 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

442 
by (simp add: take_bit_eq_mod divmod_digit_0) 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

443 
ultimately have \<open>take_bit LENGTH('a) (k * 2) = take_bit LENGTH('a) k * 2\<close> 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

444 
by (simp add: take_bit_eq_mod) 
71195  445 
with True show \<open>take_bit LENGTH('a) (take_bit LENGTH('a) (k * 2) div take_bit LENGTH('a) 2) 
71042
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

446 
= take_bit LENGTH('a) k\<close> 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

447 
by simp 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

448 
qed 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

449 
ultimately show ?thesis 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

450 
by simp 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

451 
next 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

452 
case True 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

453 
moreover have \<open>(1 + a * 2) div 2 = a\<close> 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

454 
using that proof transfer 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

455 
fix k :: int 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

456 
from length have \<open>(1 + k * 2) mod 2 ^ LENGTH('a) = 1 + (k mod 2 ^ n) * 2\<close> 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

457 
using pos_zmod_mult_2 [of \<open>2 ^ n\<close> k] by (simp add: ac_simps) 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

458 
moreover assume \<open>take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a)  Suc 0))\<close> 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

459 
with \<open>LENGTH('a) = Suc n\<close> 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

460 
have \<open>k mod 2 ^ LENGTH('a) = k mod 2 ^ n\<close> 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

461 
by (simp add: take_bit_eq_mod divmod_digit_0) 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

462 
ultimately have \<open>take_bit LENGTH('a) (1 + k * 2) = 1 + take_bit LENGTH('a) k * 2\<close> 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

463 
by (simp add: take_bit_eq_mod) 
71195  464 
with True show \<open>take_bit LENGTH('a) (take_bit LENGTH('a) (1 + k * 2) div take_bit LENGTH('a) 2) 
71042
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

465 
= take_bit LENGTH('a) k\<close> 
71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71443
diff
changeset

466 
by (auto simp add: take_bit_Suc) 
71042
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

467 
qed 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

468 
ultimately show ?thesis 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70973
diff
changeset

469 
by simp 
70925  470 
qed 
471 
qed 

472 

71409  473 
lemma even_mult_exp_div_word_iff: 
474 
\<open>even (a * 2 ^ m div 2 ^ n) \<longleftrightarrow> \<not> ( 

475 
m \<le> n \<and> 

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

477 
by transfer 

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

71412  479 
simp_all flip: push_bit_eq_mult add: bit_push_bit_iff_int) 
71409  480 

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

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

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

483 

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

484 
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:
71956
diff
changeset

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

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

488 
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:
71956
diff
changeset

489 
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:
71956
diff
changeset

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

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

492 
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:
71956
diff
changeset

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

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

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

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

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

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

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

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

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

502 

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

503 
instance proof 
71094  504 
show \<open>P a\<close> if stable: \<open>\<And>a. a div 2 = a \<Longrightarrow> P a\<close> 
505 
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> 

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

507 
proof (induction a rule: word_bit_induct) 

508 
case zero 

509 
from stable [of 0] show ?case 

510 
by simp 

511 
next 

512 
case (even a) 

513 
with rec [of a False] show ?case 

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

515 
next 

516 
case (odd a) 

517 
with rec [of a True] show ?case 

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

519 
qed 

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

520 
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:
71956
diff
changeset

521 
by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit bit_iff_odd_drop_bit) 
71138  522 
show \<open>0 div a = 0\<close> 
523 
for a :: \<open>'a word\<close> 

524 
by transfer simp 

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

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

527 
by transfer simp 

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

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

530 
apply transfer 

531 
apply (simp add: take_bit_eq_mod) 

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

533 
apply simp_all 

534 
apply (metis le_less mod_by_0 pos_mod_conj zero_less_numeral zero_less_power) 

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

536 
proof  

537 
fix aa :: int and ba :: int 

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

539 
by (metis le_less take_bit_eq_mod take_bit_nonnegative) 

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

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

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

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

544 
qed 

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

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

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

71822  548 
using that by transfer 
549 
(auto dest: le_Suc_ex simp add: mod_2_eq_odd take_bit_Suc elim!: evenE) 

71182  550 
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> 
551 
for m n :: nat 

552 
by transfer (simp, simp add: exp_div_exp_eq) 

71138  553 
show "a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)" 
554 
for a :: "'a word" and m n :: nat 

555 
apply transfer 

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

557 
apply (simp add: drop_bit_take_bit) 

558 
done 

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

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

71195  561 
by transfer (auto simp flip: take_bit_eq_mod simp add: ac_simps) 
71138  562 
show \<open>a * 2 ^ m mod 2 ^ n = a mod 2 ^ (n  m) * 2 ^ m\<close> 
563 
if \<open>m \<le> n\<close> for a :: "'a word" and m n :: nat 

564 
using that apply transfer 

565 
apply (auto simp flip: take_bit_eq_mod) 

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

567 
done 

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

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

71195  570 
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) 
71413  571 
show \<open>even ((2 ^ m  1) div (2::'a word) ^ n) \<longleftrightarrow> 2 ^ n = (0::'a word) \<or> m \<le> n\<close> 
572 
for m n :: nat 

573 
by transfer (auto simp add: take_bit_of_mask even_mask_div_iff) 

71424  574 
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> 
575 
for a :: \<open>'a word\<close> and m n :: nat 

576 
proof transfer 

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

578 
n < m 

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

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

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

582 
by (auto simp flip: take_bit_eq_mod drop_bit_eq_div push_bit_eq_mult 

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

584 
qed 

71094  585 
qed 
586 

71183  587 
end 
588 

71094  589 
instantiation word :: (len) semiring_bit_shifts 
590 
begin 

591 

592 
lift_definition push_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close> 

593 
is push_bit 

594 
proof  

71195  595 
show \<open>take_bit LENGTH('a) (push_bit n k) = take_bit LENGTH('a) (push_bit n l)\<close> 
596 
if \<open>take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close> for k l :: int and n :: nat 

71094  597 
proof  
598 
from that 

71195  599 
have \<open>take_bit (LENGTH('a)  n) (take_bit LENGTH('a) k) 
600 
= take_bit (LENGTH('a)  n) (take_bit LENGTH('a) l)\<close> 

71094  601 
by simp 
602 
moreover have \<open>min (LENGTH('a)  n) LENGTH('a) = LENGTH('a)  n\<close> 

603 
by simp 

604 
ultimately show ?thesis 

605 
by (simp add: take_bit_push_bit) 

606 
qed 

607 
qed 

608 

609 
lift_definition drop_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close> 

610 
is \<open>\<lambda>n. drop_bit n \<circ> take_bit LENGTH('a)\<close> 

611 
by (simp add: take_bit_eq_mod) 

612 

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

613 
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:
71956
diff
changeset

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

615 
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:
71956
diff
changeset

616 

71094  617 
instance proof 
618 
show \<open>push_bit n a = a * 2 ^ n\<close> for n :: nat and a :: "'a word" 

619 
by transfer (simp add: push_bit_eq_mult) 

620 
show \<open>drop_bit n a = a div 2 ^ n\<close> for n :: nat and a :: "'a word" 

71195  621 
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:
71956
diff
changeset

622 
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:
71956
diff
changeset

623 
by transfer (auto simp flip: take_bit_eq_mod) 
71094  624 
qed 
625 

70925  626 
end 
71094  627 

71095  628 
instantiation word :: (len) ring_bit_operations 
629 
begin 

630 

631 
lift_definition not_word :: "'a word \<Rightarrow> 'a word" 

632 
is not 

71418  633 
by (simp add: take_bit_not_iff) 
71095  634 

635 
lift_definition and_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" 

71409  636 
is \<open>and\<close> 
71095  637 
by simp 
638 

639 
lift_definition or_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" 

640 
is or 

641 
by simp 

642 

643 
lift_definition xor_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" 

644 
is xor 

645 
by simp 

646 

72082  647 
lift_definition mask_word :: \<open>nat \<Rightarrow> 'a word\<close> 
648 
is mask . 

649 

650 
instance by (standard; transfer) 

651 
(auto simp add: minus_eq_not_minus_1 mask_eq_exp_minus_1 

652 
bit_not_iff bit_and_iff bit_or_iff bit_xor_iff) 

71095  653 

71094  654 
end 
71095  655 

71854  656 
definition even_word :: \<open>'a::len word \<Rightarrow> bool\<close> 
657 
where [code_abbrev]: \<open>even_word = even\<close> 

658 

659 
lemma even_word_iff [code]: 

660 
\<open>even_word a \<longleftrightarrow> a AND 1 = 0\<close> 

71921  661 
by (simp add: even_word_def and_one_eq even_iff_mod_2_eq_zero) 
71854  662 

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

663 
lemma bit_word_iff_drop_bit_and [code]: 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71956
diff
changeset

664 
\<open>bit a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close> for a :: \<open>'a::len word\<close> 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71956
diff
changeset

665 
by (simp add: bit_iff_odd_drop_bit odd_iff_mod_2_eq_one and_one_eq) 
71854  666 

71443  667 
lifting_update word.lifting 
668 
lifting_forget word.lifting 

669 

71095  670 
end 