author  haftmann 
Tue, 04 Aug 2020 09:33:05 +0000  
changeset 72082  41393ecb57ac 
parent 72079  8c355e2dd7db 
child 72083  3ec876181527 
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 
70192  13 
Bit_Comprehension 
71997  14 
Bit_Lists 
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 

61799  18 
subsection \<open>Type definition\<close> 
37660  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:
71953
diff
changeset

20 
quotient_type (overloaded) 'a word = int / \<open>\<lambda>k l. take_bit LENGTH('a) k = take_bit LENGTH('a::len) l\<close> 
71948
6ede899d26d3
fundamental construction of word type following existing transfer rules
haftmann
parents:
71947
diff
changeset

21 
morphisms rep_word word_of_int by (auto intro!: equivpI reflpI sympI transpI) 
6ede899d26d3
fundamental construction of word type following existing transfer rules
haftmann
parents:
71947
diff
changeset

22 

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

23 
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

24 
is \<open>take_bit LENGTH('a)\<close> . 
37660  25 

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

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

28 

70185  29 
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

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

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

32 

70185  33 
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

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

35 
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

36 

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

37 
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

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

39 

65268  40 
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

41 
using word_uint_eqI by auto 
70185  42 

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

43 
lemma uint_word_of_int: "uint (word_of_int k :: 'a::len word) = k mod 2 ^ LENGTH('a)" 
71948
6ede899d26d3
fundamental construction of word type following existing transfer rules
haftmann
parents:
71947
diff
changeset

44 
by transfer (simp add: take_bit_eq_mod) 
6ede899d26d3
fundamental construction of word type following existing transfer rules
haftmann
parents:
71947
diff
changeset

45 

65268  46 
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

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

48 

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

49 
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

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

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

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

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

54 
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

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

56 

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

57 

61799  58 
subsection \<open>Type conversions and casting\<close> 
55816
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

59 

72079  60 
lemma signed_take_bit_decr_length_iff: 
61 
\<open>signed_take_bit (LENGTH('a::len)  Suc 0) k = signed_take_bit (LENGTH('a)  Suc 0) l 

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

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

64 
(simp_all add: signed_take_bit_eq_iff_take_bit_eq) 

65 

66 
lift_definition sint :: \<open>'a::len word \<Rightarrow> int\<close> 

67 
\<comment> \<open>treats the mostsignificant bit as a sign bit\<close> 

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

69 
by (simp add: signed_take_bit_decr_length_iff) 

70 

71 
lemma sint_uint [code]: 

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

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

74 
by transfer simp 

75 

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

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

78 
by transfer simp 

79 

80 
lemma nat_uint_eq [simp]: 

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

82 
by transfer simp 

83 

84 
lemma unat_eq_nat_uint [code]: 

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

86 
by simp 

87 

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

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

90 
by simp 

91 

92 
lemma ucast_eq [code]: 

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

94 
by transfer simp 

95 

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

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

98 
by (simp flip: signed_take_bit_decr_length_iff) 

99 

100 
lemma scast_eq [code]: 

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

102 
by transfer simp 

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

103 

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

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

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

106 

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

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

109 

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

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

111 

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

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

113 

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

116 
by (fact size_word.rep_eq) 

117 

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

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

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

121 

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

122 
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

123 

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

124 
lemma lens_not_0 [iff]: 
71942  125 
\<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

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

127 

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

130 

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

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

133 

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

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

136 

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

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

139 

140 
lemma is_up_eq: 

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

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

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

144 

145 
lemma is_down_eq: 

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

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

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

149 

150 
lift_definition of_bl :: \<open>bool list \<Rightarrow> 'a::len word\<close> 

151 
is bl_to_bin . 

152 

153 
lift_definition to_bl :: \<open>'a::len word \<Rightarrow> bool list\<close> 

154 
is \<open>bin_to_bl LENGTH('a)\<close> 

155 
by (simp add: bl_to_bin_inj) 

156 

157 
lemma to_bl_eq: 

158 
\<open>to_bl w = bin_to_bl (LENGTH('a)) (uint w)\<close> 

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

160 
by transfer simp 

161 

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

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

164 

165 
lemma word_int_case_eq_uint [code]: 

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

167 
by transfer simp 

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

168 

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

169 
translations 
65268  170 
"case x of XCONST of_int y \<Rightarrow> b" \<rightleftharpoons> "CONST word_int_case (\<lambda>y. b) x" 
171 
"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

172 

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

173 

61799  174 
subsection \<open>Basic code generation setup\<close> 
55817
0bc0217387a5
earlier setup of transfer, without dependency on psychodelic interpretations
haftmann
parents:
55816
diff
changeset

175 

72079  176 
lift_definition Word :: \<open>int \<Rightarrow> 'a::len word\<close> 
177 
is id . 

178 

179 
lemma Word_eq_word_of_int [code_post]: 

180 
\<open>Word = word_of_int\<close> 

181 
by (simp add: fun_eq_iff Word.abs_eq) 

182 

183 
lemma [code abstype]: 

184 
\<open>Word (uint w) = w\<close> 

185 
by transfer simp 

186 

187 
lemma [code abstract]: 

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

189 
by (fact uint.abs_eq) 

55817
0bc0217387a5
earlier setup of transfer, without dependency on psychodelic interpretations
haftmann
parents:
55816
diff
changeset

190 

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

191 
instantiation word :: (len) equal 
55817
0bc0217387a5
earlier setup of transfer, without dependency on psychodelic interpretations
haftmann
parents:
55816
diff
changeset

192 
begin 
0bc0217387a5
earlier setup of transfer, without dependency on psychodelic interpretations
haftmann
parents:
55816
diff
changeset

193 

72079  194 
lift_definition equal_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> bool\<close> 
195 
is \<open>\<lambda>k l. take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close> 

196 
by simp 

65268  197 

198 
instance 

72079  199 
by (standard; transfer) rule 
55817
0bc0217387a5
earlier setup of transfer, without dependency on psychodelic interpretations
haftmann
parents:
55816
diff
changeset

200 

0bc0217387a5
earlier setup of transfer, without dependency on psychodelic interpretations
haftmann
parents:
55816
diff
changeset

201 
end 
0bc0217387a5
earlier setup of transfer, without dependency on psychodelic interpretations
haftmann
parents:
55816
diff
changeset

202 

72079  203 
lemma [code]: 
204 
\<open>HOL.equal k l \<longleftrightarrow> HOL.equal (uint k) (uint l)\<close> 

205 
by transfer (simp add: equal) 

206 

55817
0bc0217387a5
earlier setup of transfer, without dependency on psychodelic interpretations
haftmann
parents:
55816
diff
changeset

207 
notation fcomp (infixl "\<circ>>" 60) 
0bc0217387a5
earlier setup of transfer, without dependency on psychodelic interpretations
haftmann
parents:
55816
diff
changeset

208 
notation scomp (infixl "\<circ>\<rightarrow>" 60) 
0bc0217387a5
earlier setup of transfer, without dependency on psychodelic interpretations
haftmann
parents:
55816
diff
changeset

209 

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

210 
instantiation word :: ("{len, typerep}") random 
55817
0bc0217387a5
earlier setup of transfer, without dependency on psychodelic interpretations
haftmann
parents:
55816
diff
changeset

211 
begin 
0bc0217387a5
earlier setup of transfer, without dependency on psychodelic interpretations
haftmann
parents:
55816
diff
changeset

212 

0bc0217387a5
earlier setup of transfer, without dependency on psychodelic interpretations
haftmann
parents:
55816
diff
changeset

213 
definition 
0bc0217387a5
earlier setup of transfer, without dependency on psychodelic interpretations
haftmann
parents:
55816
diff
changeset

214 
"random_word i = Random.range i \<circ>\<rightarrow> (\<lambda>k. Pair ( 
0bc0217387a5
earlier setup of transfer, without dependency on psychodelic interpretations
haftmann
parents:
55816
diff
changeset

215 
let j = word_of_int (int_of_integer (integer_of_natural k)) :: 'a word 
0bc0217387a5
earlier setup of transfer, without dependency on psychodelic interpretations
haftmann
parents:
55816
diff
changeset

216 
in (j, \<lambda>_::unit. Code_Evaluation.term_of j)))" 
0bc0217387a5
earlier setup of transfer, without dependency on psychodelic interpretations
haftmann
parents:
55816
diff
changeset

217 

0bc0217387a5
earlier setup of transfer, without dependency on psychodelic interpretations
haftmann
parents:
55816
diff
changeset

218 
instance .. 
0bc0217387a5
earlier setup of transfer, without dependency on psychodelic interpretations
haftmann
parents:
55816
diff
changeset

219 

0bc0217387a5
earlier setup of transfer, without dependency on psychodelic interpretations
haftmann
parents:
55816
diff
changeset

220 
end 
0bc0217387a5
earlier setup of transfer, without dependency on psychodelic interpretations
haftmann
parents:
55816
diff
changeset

221 

0bc0217387a5
earlier setup of transfer, without dependency on psychodelic interpretations
haftmann
parents:
55816
diff
changeset

222 
no_notation fcomp (infixl "\<circ>>" 60) 
0bc0217387a5
earlier setup of transfer, without dependency on psychodelic interpretations
haftmann
parents:
55816
diff
changeset

223 
no_notation scomp (infixl "\<circ>\<rightarrow>" 60) 
0bc0217387a5
earlier setup of transfer, without dependency on psychodelic interpretations
haftmann
parents:
55816
diff
changeset

224 

0bc0217387a5
earlier setup of transfer, without dependency on psychodelic interpretations
haftmann
parents:
55816
diff
changeset

225 

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

227 

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

228 
lemmas uint_0 = uint_nonnegative (* FIXME duplicate *) 
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

229 
lemmas uint_lt = uint_bounded (* FIXME duplicate *) 
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

230 
lemmas uint_mod_same = uint_idem (* FIXME duplicate *) 
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

231 

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

234 
where "uints n = range (bintrunc n)" 

235 

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

237 
where "sints n = range (sbintrunc (n  1))" 

238 

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

240 
by (simp add: uints_def range_bintrunc) 

241 

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

243 
by (simp add: sints_def range_sbintrunc) 

244 

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

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

247 

248 
\<comment> \<open>naturals\<close> 

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

250 
apply (unfold unats_def uints_num) 

251 
apply safe 

252 
apply (rule_tac image_eqI) 

253 
apply (erule_tac nat_0_le [symmetric]) 

254 
by auto 

255 

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

257 
by (auto simp: uints_unats image_iff) 

258 

65268  259 
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

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

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

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

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

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

266 

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

267 
interpretation word_uint: 
65268  268 
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

269 
"uint::'a::len word \<Rightarrow> int" 
65268  270 
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

271 
"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

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

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

274 

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

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

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

277 

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

278 
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

279 
"td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (LENGTH('a::len))) 
70185  280 
(bintrunc (LENGTH('a)))" 
55816
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

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

282 

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

283 
interpretation word_ubin: 
65268  284 
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

285 
"uint::'a::len word \<Rightarrow> int" 
65268  286 
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

287 
"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

288 
"bintrunc (LENGTH('a::len))" 
55816
e8dd03241e86
cursory polishing: tuned proofs, tuned symbols, tuned headings
haftmann
parents:
55415
diff
changeset

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

290 

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

291 

61799  292 
subsection \<open>Arithmetic operations\<close> 
37660  293 

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

294 
lift_definition word_succ :: "'a::len word \<Rightarrow> 'a word" is "\<lambda>x. x + 1" 
64593
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64243
diff
changeset

295 
by (auto simp add: bintrunc_mod2p intro: mod_add_cong) 
47374
9475d524bafb
set up and use lift_definition for word operations
huffman
parents:
47372
diff
changeset

296 

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

297 
lift_definition word_pred :: "'a::len word \<Rightarrow> 'a word" is "\<lambda>x. x  1" 
64593
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64243
diff
changeset

298 
by (auto simp add: bintrunc_mod2p intro: mod_diff_cong) 
45545
26aebb8ac9c1
Word.thy: rearrange to instantiate arithmetic classes together with arithmetic operations
huffman
parents:
45544
diff
changeset

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) "{neg_numeral, modulo, comm_monoid_mult, comm_ring}" 
37660  301 
begin 
302 

47387
a0f257197741
remove nowunnecessary type annotations from lift_definition commands
huffman
parents:
47377
diff
changeset

303 
lift_definition zero_word :: "'a word" is "0" . 
a0f257197741
remove nowunnecessary type annotations from lift_definition commands
huffman
parents:
47377
diff
changeset

304 

a0f257197741
remove nowunnecessary type annotations from lift_definition commands
huffman
parents:
47377
diff
changeset

305 
lift_definition one_word :: "'a word" is "1" . 
a0f257197741
remove nowunnecessary type annotations from lift_definition commands
huffman
parents:
47377
diff
changeset

306 

67399  307 
lift_definition plus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "(+)" 
64593
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64243
diff
changeset

308 
by (auto simp add: bintrunc_mod2p intro: mod_add_cong) 
47374
9475d524bafb
set up and use lift_definition for word operations
huffman
parents:
47372
diff
changeset

309 

67399  310 
lift_definition minus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "()" 
64593
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64243
diff
changeset

311 
by (auto simp add: bintrunc_mod2p intro: mod_diff_cong) 
47374
9475d524bafb
set up and use lift_definition for word operations
huffman
parents:
47372
diff
changeset

312 

47387
a0f257197741
remove nowunnecessary type annotations from lift_definition commands
huffman
parents:
47377
diff
changeset

313 
lift_definition uminus_word :: "'a word \<Rightarrow> 'a word" is uminus 
64593
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64243
diff
changeset

314 
by (auto simp add: bintrunc_mod2p intro: mod_minus_cong) 
47374
9475d524bafb
set up and use lift_definition for word operations
huffman
parents:
47372
diff
changeset

315 

69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68157
diff
changeset

316 
lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "(*)" 
64593
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64243
diff
changeset

317 
by (auto simp add: bintrunc_mod2p intro: mod_mult_cong) 
37660  318 

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

321 
by simp 

322 

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

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

325 
by simp 

37660  326 

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

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

329 

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

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

331 

72079  332 
lemma uint_0_eq [simp, code]: 
333 
\<open>uint 0 = 0\<close> 

334 
by transfer simp 

335 

336 
quickcheck_generator word 

337 
constructors: 

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

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

340 
\<open>uminus :: 'a word \<Rightarrow> 'a::len word\<close> 

341 

342 
lemma uint_1_eq [simp, code]: 

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

344 
by transfer simp 

345 

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

348 
by transfer rule 

349 

350 
lemma word_mod_def [code]: 

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

352 
by transfer rule 

353 

354 
context 

355 
includes lifting_syntax 

356 
notes power_transfer [transfer_rule] 

357 
begin 

358 

359 
lemma power_transfer_word [transfer_rule]: 

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

361 
by transfer_prover 

362 

363 
end 

364 

365 

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

367 

72079  368 
lemma word_arith_wis: 
369 
shows word_add_def [code]: "a + b = word_of_int (uint a + uint b)" 

370 
and word_sub_wi [code]: "a  b = word_of_int (uint a  uint b)" 

371 
and word_mult_def [code]: "a * b = word_of_int (uint a * uint b)" 

372 
and word_minus_def [code]: " a = word_of_int ( uint a)" 

373 
and word_succ_alt [code]: "word_succ a = word_of_int (uint a + 1)" 

374 
and word_pred_alt [code]: "word_pred a = word_of_int (uint a  1)" 

65268  375 
and word_0_wi: "0 = word_of_int 0" 
376 
and word_1_wi: "1 = word_of_int 1" 

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

377 
apply (simp_all flip: plus_word.abs_eq minus_word.abs_eq 
6ede899d26d3
fundamental construction of word type following existing transfer rules
haftmann
parents:
71947
diff
changeset

378 
times_word.abs_eq uminus_word.abs_eq 
6ede899d26d3
fundamental construction of word type following existing transfer rules
haftmann
parents:
71947
diff
changeset

379 
zero_word.abs_eq one_word.abs_eq) 
6ede899d26d3
fundamental construction of word type following existing transfer rules
haftmann
parents:
71947
diff
changeset

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

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

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

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

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

385 

65268  386 
lemma wi_homs: 
387 
shows wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)" 

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

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

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

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

392 
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

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

394 

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

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

396 

46013  397 
lemmas word_of_int_homs = wi_homs word_0_wi word_1_wi 
46009  398 

399 
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

400 

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

401 
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

402 

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

403 
instance word :: (len) semiring_numeral .. 
71950  404 

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

405 
instance word :: (len) comm_ring_1 
45810  406 
proof 
70185  407 
have *: "0 < LENGTH('a)" by (rule len_gt_0) 
65268  408 
show "(0::'a word) \<noteq> 1" 
409 
by transfer (use * in \<open>auto simp add: gr0_conv_Suc\<close>) 

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

411 

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

412 
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

413 
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

414 

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

415 
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

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

417 
apply (case_tac x rule: int_diff_cases) 
46013  418 
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

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

420 

71950  421 
context 
422 
includes lifting_syntax 

423 
notes 

424 
transfer_rule_of_bool [transfer_rule] 

425 
transfer_rule_numeral [transfer_rule] 

426 
transfer_rule_of_nat [transfer_rule] 

427 
transfer_rule_of_int [transfer_rule] 

428 
begin 

429 

430 
lemma [transfer_rule]: 

431 
"((=) ===> (pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool)) of_bool of_bool" 

432 
by transfer_prover 

433 

434 
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:
71953
diff
changeset

435 
"((=) ===> (pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool)) numeral numeral" 
71950  436 
by transfer_prover 
437 

438 
lemma [transfer_rule]: 

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

440 
by transfer_prover 

441 

442 
lemma [transfer_rule]: 

443 
"((=) ===> pcr_word) (\<lambda>k. k) of_int" 

444 
proof  

445 
have "((=) ===> pcr_word) of_int of_int" 

446 
by transfer_prover 

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

448 
qed 

449 

450 
end 

451 

452 
lemma word_of_int_eq: 

453 
"word_of_int = of_int" 

454 
by (rule ext) (transfer, rule) 

455 

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

37660  458 

71950  459 
context 
460 
includes lifting_syntax 

461 
begin 

462 

463 
lemma [transfer_rule]: 

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

467 
for k :: int 

468 
proof 

469 
assume ?P 

470 
then show ?Q 

471 
by auto 

472 
next 

473 
assume ?Q 

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

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

476 
by simp 

477 
then show ?P 

478 
by simp 

479 
qed 

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

481 
transfer_prover 

482 
qed 

483 

484 
end 

485 

71951  486 
instance word :: (len) semiring_modulo 
487 
proof 

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

489 
proof transfer 

490 
fix k l :: int 

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

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

493 
by (simp add: take_bit_eq_mod) 

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

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

496 
by (simp add: div_mult_mod_eq) 

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

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

499 
by (simp add: mod_add_left_eq) 

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

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

502 
by (simp add: mod_mult_right_eq) 

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

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

505 
by (simp add: mod_simps) 

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

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

508 
by simp 

509 
qed 

510 
qed 

511 

512 
instance word :: (len) semiring_parity 

513 
proof 

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

515 
by transfer simp 

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

517 
for a :: "'a word" 

518 
by transfer (simp_all add: mod_2_eq_odd take_bit_Suc) 

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

520 
for a :: "'a word" 

521 
by transfer (simp_all add: mod_2_eq_odd take_bit_Suc) 

522 
qed 

523 

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

526 
by transfer simp 

527 

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

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

531 
proof  

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

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

534 
by simp 

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

536 
using that by transfer 

537 
(auto simp add: take_bit_eq_0_iff take_bit_eq_mod *) 

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

539 
by transfer simp 

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

541 
by (simp add: *) 

542 
ultimately show ?thesis 

543 
by auto 

544 
qed 

545 

45547  546 

61799  547 
subsection \<open>Ordering\<close> 
45547  548 

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

549 
instantiation word :: (len) linorder 
45547  550 
begin 
551 

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

554 
by simp 

555 

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

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

558 
by simp 

37660  559 

45547  560 
instance 
71950  561 
by (standard; transfer) auto 
45547  562 

563 
end 

564 

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

565 
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

566 
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

567 

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

568 
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

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

570 

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

573 
by transfer rule 

574 

575 
lemma word_less_def [code]: 

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

577 
by transfer rule 

578 

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

580 
\<open>a > 0 \<longleftrightarrow> a \<noteq> 0\<close> for a :: \<open>'a::len word\<close> 
71951  581 
by transfer (simp add: less_le) 
582 

583 
lemma of_nat_word_eq_iff: 

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

585 
by transfer (simp add: take_bit_of_nat) 

586 

587 
lemma of_nat_word_less_eq_iff: 

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

589 
by transfer (simp add: take_bit_of_nat) 

590 

591 
lemma of_nat_word_less_iff: 

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

593 
by transfer (simp add: take_bit_of_nat) 

594 

595 
lemma of_nat_word_eq_0_iff: 

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

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

598 

599 
lemma of_int_word_eq_iff: 

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

601 
by transfer rule 

602 

603 
lemma of_int_word_less_eq_iff: 

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

605 
by transfer rule 

606 

607 
lemma of_int_word_less_iff: 

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

609 
by transfer rule 

610 

611 
lemma of_int_word_eq_0_iff: 

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

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

614 

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

617 
by (simp flip: signed_take_bit_decr_length_iff) 

618 

619 
lemma word_sle_eq [code]: 

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

621 
by transfer simp 

622 

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

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

625 
by (simp flip: signed_take_bit_decr_length_iff) 

626 

627 
lemma word_sless_eq: 

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

629 
by transfer (simp add: signed_take_bit_decr_length_iff less_le) 

630 

631 
lemma [code]: 

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

633 
by transfer simp 

37660  634 

635 

61799  636 
subsection \<open>Bitwise operations\<close> 
37660  637 

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

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

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

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

643 
proof  

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

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

646 
by simp 

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

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

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

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

651 
by (simp add: l) 

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

653 
proof (induction n rule: nat_bit_induct) 

654 
case zero 

655 
show ?case 

656 
by simp (rule word_zero) 

657 
next 

658 
case (even n) 

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

660 
by simp 

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

662 
by simp 

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

664 
by (auto simp add: word_greater_zero_iff of_nat_word_eq_0_iff l) 

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

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

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

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

669 
by (rule word_even) 

670 
then show ?case 

671 
by simp 

672 
next 

673 
case (odd n) 

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

675 
by simp 

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

677 
by simp 

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

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

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

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

682 
by (rule word_odd) 

683 
then show ?case 

684 
by simp 

685 
qed 

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

687 
by transfer simp 

688 
ultimately show ?thesis 

72079  689 
by (simp add: n_def) 
71951  690 
qed 
691 

692 
lemma bit_word_half_eq: 

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

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

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

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

697 
case False 

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

699 
by auto 

700 
with False that show ?thesis 

701 
by transfer (simp add: eq_iff) 

702 
next 

703 
case True 

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

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

706 
show ?thesis proof (cases b) 

707 
case False 

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

709 
using that proof transfer 

710 
fix k :: int 

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

712 
by simp 

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

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

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

716 
by (simp add: take_bit_eq_mod divmod_digit_0) 

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

718 
by (simp add: take_bit_eq_mod) 

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

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

721 
by simp 

722 
qed 

723 
ultimately show ?thesis 

724 
by simp 

725 
next 

726 
case True 

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

728 
using that proof transfer 

729 
fix k :: int 

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

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

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

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

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

735 
by (simp add: take_bit_eq_mod divmod_digit_0) 

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

737 
by (simp add: take_bit_eq_mod) 

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

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

740 
by (auto simp add: take_bit_Suc) 

741 
qed 

742 
ultimately show ?thesis 

743 
by simp 

744 
qed 

745 
qed 

746 

747 
lemma even_mult_exp_div_word_iff: 

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

749 
m \<le> n \<and> 

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

751 
by transfer 

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

753 
simp_all flip: push_bit_eq_mult add: bit_push_bit_iff_int) 

754 

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

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

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

757 

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

758 
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

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

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

762 
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

763 
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

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

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

766 
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

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

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

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

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

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

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

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

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

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

776 

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

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

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

781 
proof (induction a rule: word_bit_induct) 

782 
case zero 

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

784 
by transfer simp 

785 
with stable [of 0] show ?case 

786 
by simp 

787 
next 

788 
case (even a) 

789 
with rec [of a False] show ?case 

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

791 
next 

792 
case (odd a) 

793 
with rec [of a True] show ?case 

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

795 
qed 

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

796 
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

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

800 
by transfer simp 

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

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

803 
by transfer simp 

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

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

806 
apply transfer 

807 
apply (simp add: take_bit_eq_mod) 

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

809 
apply simp_all 

810 
apply (metis le_less mod_by_0 pos_mod_conj zero_less_numeral zero_less_power) 

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

812 
proof  

813 
fix aa :: int and ba :: int 

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

815 
by (metis le_less take_bit_eq_mod take_bit_nonnegative) 

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

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

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

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

820 
qed 

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

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

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

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

71951  826 
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> 
827 
for m n :: nat 

828 
by transfer (simp, simp add: exp_div_exp_eq) 

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

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

831 
apply transfer 

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

833 
apply (simp add: drop_bit_take_bit) 

834 
done 

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

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

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

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

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

840 
using that apply transfer 

841 
apply (auto simp flip: take_bit_eq_mod) 

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

843 
done 

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

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

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

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

848 
for m n :: nat 

849 
by transfer (auto simp add: take_bit_of_mask even_mask_div_iff) 

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

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

852 
proof transfer 

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

854 
n < m 

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

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

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

858 
by (auto simp flip: take_bit_eq_mod drop_bit_eq_div push_bit_eq_mult 

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

860 
qed 

861 
qed 

862 

863 
end 

864 

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

865 
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

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

867 

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

868 
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

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

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

871 
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

872 
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

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

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

875 
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

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

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

878 
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

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

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

881 
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

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

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

884 

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

885 
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

886 
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

887 
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

888 

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

889 
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

890 
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

891 
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

892 

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

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

894 
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

895 
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

896 
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

897 
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

898 
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

899 
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

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

901 

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

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

903 

71958  904 
lemma bit_word_eqI: 
905 
\<open>a = b\<close> if \<open>\<And>n. n \<le> LENGTH('a) \<Longrightarrow> bit a n \<longleftrightarrow> bit b n\<close> 

71990  906 
for a b :: \<open>'a::len word\<close> 
907 
using that by transfer (auto simp add: nat_less_le bit_eq_iff bit_take_bit_iff) 

908 

909 
lemma bit_imp_le_length: 

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

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

912 
using that by transfer simp 

913 

914 
lemma not_bit_length [simp]: 

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

916 
by transfer simp 

917 

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

920 
by transfer (simp add: ac_simps) 

921 

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

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

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

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

925 

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

928 
by transfer rule 

929 

930 
lemma bit_uint_iff: 

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

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

933 
by transfer (simp add: bit_take_bit_iff) 

934 

935 
lemma bit_sint_iff: 

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

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

72079  938 
by transfer (auto simp add: bit_signed_take_bit_iff min_def le_less not_less) 
71990  939 

940 
lemma bit_word_ucast_iff: 

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

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

72079  943 
by transfer (simp add: bit_take_bit_iff ac_simps) 
71990  944 

945 
lemma bit_word_scast_iff: 

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

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

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

72079  949 
by transfer (auto simp add: bit_signed_take_bit_iff le_less min_def) 
950 

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

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

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

954 

955 
lemma shiftl1_eq: 

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

957 
by transfer (simp add: take_bit_eq_mod mod_simps) 

70191  958 

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

959 
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

960 
\<open>shiftl1 = (*) 2\<close> 
72079  961 
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

962 

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

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

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

967 

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

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

972 
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

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

975 

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

72079  978 
by transfer (auto simp flip: bit_Suc simp add: bit_take_bit_iff) 
979 

980 
lemma shiftr1_eq: 

981 
\<open>shiftr1 w = word_of_int (bin_rest (uint w))\<close> 

982 
by transfer simp 

71990  983 

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

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

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

986 

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

987 
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

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

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

990 

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

991 
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

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

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

994 

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

995 
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

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

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

998 

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

999 
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

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

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

1002 

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

1005 
. 

1006 

1007 
instance by (standard; transfer) 

1008 
(auto simp add: minus_eq_not_minus_1 mask_eq_exp_minus_1 

1009 
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

1010 

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

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

1012 

72009  1013 
context 
1014 
includes lifting_syntax 

1015 
begin 

1016 

72079  1017 
lemma set_bit_word_transfer [transfer_rule]: 
72009  1018 
\<open>((=) ===> pcr_word ===> pcr_word) set_bit set_bit\<close> 
1019 
by (unfold set_bit_def) transfer_prover 

1020 

72079  1021 
lemma unset_bit_word_transfer [transfer_rule]: 
72009  1022 
\<open>((=) ===> pcr_word ===> pcr_word) unset_bit unset_bit\<close> 
1023 
by (unfold unset_bit_def) transfer_prover 

1024 

72079  1025 
lemma flip_bit_word_transfer [transfer_rule]: 
72009  1026 
\<open>((=) ===> pcr_word ===> pcr_word) flip_bit flip_bit\<close> 
1027 
by (unfold flip_bit_def) transfer_prover 

1028 

1029 
end 

1030 

72000  1031 
instantiation word :: (len) semiring_bit_syntax 
37660  1032 
begin 
1033 

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

1036 
proof 

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

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

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

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

1041 
case True 

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

1043 
by simp 

1044 
then show ?thesis 

1045 
by (simp add: bit_take_bit_iff) 

1046 
next 

1047 
case False 

1048 
then show ?thesis 

1049 
by simp 

1050 
qed 

1051 
qed 

37660  1052 

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

1053 
lemma test_bit_word_eq: 
72079  1054 
\<open>test_bit = (bit :: 'a word \<Rightarrow> _)\<close> 
1055 
by transfer simp 

1056 

1057 
lemma [code]: 

1058 
\<open>bit w n \<longleftrightarrow> w AND push_bit n 1 \<noteq> 0\<close> 

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

1060 
apply (simp add: bit_eq_iff) 

1061 
apply (auto simp add: bit_and_iff bit_push_bit_iff bit_1_iff exp_eq_0_imp_not_bit) 

1062 
done 

1063 

1064 
lemma [code]: 

1065 
\<open>test_bit w n \<longleftrightarrow> w AND push_bit n 1 \<noteq> 0\<close> 

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

1067 
apply (simp add: test_bit_word_eq bit_eq_iff) 

1068 
apply (auto simp add: bit_and_iff bit_push_bit_iff bit_1_iff exp_eq_0_imp_not_bit) 

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

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

1070 

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

1073 
proof  

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

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

1076 
proof  

1077 
from that 

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

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

1080 
by simp 

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

1082 
by simp 

1083 
ultimately show ?thesis 

1084 
by (simp add: take_bit_push_bit) 

1085 
qed 

1086 
qed 

1087 

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

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

1089 
\<open>w << n = push_bit n w\<close> for w :: \<open>'a::len word\<close> 
72079  1090 
by transfer rule 
1091 

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

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

1094 

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

72079  1097 
by transfer simp 
1098 

1099 
instance 

1100 
by (standard; transfer) simp_all 

72000  1101 

1102 
end 

1103 

72079  1104 
lemma shiftl_code [code]: 
1105 
\<open>w << n = w * 2 ^ n\<close> 

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

1107 
by transfer (simp add: push_bit_eq_mult) 

1108 

1109 
lemma shiftl1_code [code]: 

1110 
\<open>shiftl1 w = w << 1\<close> 

1111 
by transfer (simp add: push_bit_eq_mult ac_simps) 

1112 

1113 
lemma uint_shiftr_eq [code]: 

1114 
\<open>uint (w >> n) = uint w div 2 ^ n\<close> 

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

1116 
by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit min_def le_less less_diff_conv) 

1117 

1118 
lemma shiftr1_code [code]: 

1119 
\<open>shiftr1 w = w >> 1\<close> 

1120 
by transfer (simp add: drop_bit_Suc) 

1121 

1122 
lemma word_test_bit_def: 

1123 
\<open>test_bit a = bin_nth (uint a)\<close> 

1124 
by transfer (simp add: fun_eq_iff bit_take_bit_iff) 

1125 

1126 
lemma shiftl_def: 

1127 
\<open>w << n = (shiftl1 ^^ n) w\<close> 

1128 
proof  

1129 
have \<open>push_bit n = (((*) 2 ^^ n) :: int \<Rightarrow> int)\<close> for n 

1130 
by (induction n) (simp_all add: fun_eq_iff funpow_swap1, simp add: ac_simps) 

1131 
then show ?thesis 

1132 
by transfer simp 

1133 
qed 

1134 

1135 
lemma shiftr_def: 

1136 
\<open>w >> n = (shiftr1 ^^ n) w\<close> 

1137 
proof  

1138 
have \<open>drop_bit n = (((\<lambda>k::int. k div 2) ^^ n))\<close> for n 

1139 
by (rule sym, induction n) 

1140 
(simp_all add: fun_eq_iff drop_bit_Suc flip: drop_bit_half) 

1141 
then show ?thesis 

1142 
apply transfer 

1143 
apply simp 

1144 
apply (metis bintrunc_bintrunc rco_bintr) 

1145 
done 

1146 
qed 

1147 

71990  1148 
lemma bit_shiftl_word_iff: 
1149 
\<open>bit (w << m) n \<longleftrightarrow> m \<le> n \<and> n < LENGTH('a) \<and> bit w (n  m)\<close> 

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

1151 
by (simp add: shiftl_word_eq bit_push_bit_iff exp_eq_zero_iff not_le) 

1152 

71955  1153 
lemma [code]: 
1154 
\<open>push_bit n w = w << n\<close> for w :: \<open>'a::len word\<close> 

1155 
by (simp add: shiftl_word_eq) 

1156 

71990  1157 
lemma bit_shiftr_word_iff: 
1158 
\<open>bit (w >> m) n \<longleftrightarrow> bit w (m + n)\<close> 

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

1160 
by (simp add: shiftr_word_eq bit_drop_bit_eq) 

1161 

71955  1162 
lemma [code]: 
1163 
\<open>drop_bit n w = w >> n\<close> for w :: \<open>'a::len word\<close> 

1164 
by (simp add: shiftr_word_eq) 

1165 

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

1166 
lemma [code]: 
72079  1167 
\<open>take_bit n a = a AND mask n\<close> for a :: \<open>'a::len word\<close> 
71965
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

1168 
by (fact take_bit_eq_mask) 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71958
diff
changeset

1169 

72082  1170 
lemma [code]: 
1171 
\<open>mask (Suc n) = push_bit n (1 :: 'a word) OR mask n\<close> 

1172 
\<open>mask 0 = (0 :: 'a::len word)\<close> 

1173 
by (simp_all add: mask_Suc_exp push_bit_of_1) 

1174 

71955  1175 
lemma [code_abbrev]: 
1176 
\<open>push_bit n 1 = (2 :: 'a::len word) ^ n\<close> 

1177 
by (fact push_bit_of_1) 

1178 

72079  1179 
lemma 
1180 
word_not_def [code]: "NOT (a::'a::len word) = word_of_int (NOT (uint a))" 

65268  1181 
and word_and_def: "(a::'a word) AND b = word_of_int (uint a AND uint b)" 
1182 
and word_or_def: "(a::'a word) OR b = word_of_int (uint a OR uint b)" 

1183 
and word_xor_def: "(a::'a word) XOR b = word_of_int (uint a XOR uint b)" 

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

1184 
by (transfer, simp add: take_bit_not_take_bit)+ 
47374
9475d524bafb
set up and use lift_definition for word operations
huffman
parents:
47372
diff
changeset

1185 

72079  1186 
lemma [code abstract]: 
1187 
\<open>uint (v AND w) = uint v AND uint w\<close> 

1188 
by transfer simp 

1189 

1190 
lemma [code abstract]: 

1191 
\<open>uint (v OR w) = uint v OR uint w\<close> 

1192 
by transfer simp 

1193 

1194 
lemma [code abstract]: 

1195 
\<open>uint (v XOR w) = uint v XOR uint w\<close> 

1196 
by transfer simp 

1197 

1198 
lift_definition setBit :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> 'a word\<close> 

1199 
is \<open>\<lambda>k n. set_bit n k\<close> 

1200 
by (simp add: take_bit_set_bit_eq) 

1201 

1202 
lemma set_Bit_eq: 

1203 
\<open>setBit w n = set_bit n w\<close> 

1204 
by transfer simp 

71990  1205 

1206 
lemma bit_setBit_iff: 

1207 
\<open>bit (setBit w m) n \<longleftrightarrow> (m = n \<and> n < LENGTH('a) \<or> bit w n)\<close> 

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

72079  1209 
by transfer (auto simp add: bit_set_bit_iff) 
1210 

1211 
lift_definition clearBit :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> 'a word\<close> 

1212 
is \<open>\<lambda>k n. unset_bit n k\<close> 

1213 
by (simp add: take_bit_unset_bit_eq) 

1214 

1215 
lemma clear_Bit_eq: 

1216 
\<open>clearBit w n = unset_bit n w\<close> 

1217 
by transfer simp 

71990  1218 

1219 
lemma bit_clearBit_iff: 

1220 
\<open>bit (clearBit w m) n \<longleftrightarrow> m \<noteq> n \<and> bit w n\<close> 

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

72079  1222 
by transfer (auto simp add: bit_unset_bit_iff) 
71990  1223 

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

1224 
definition even_word :: \<open>'a::len word \<Rightarrow> bool\<close> 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71955
diff
changeset

1225 
where [code_abbrev]: \<open>even_word = even\<close> 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71955
diff
changeset

1226 

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

1227 
lemma even_word_iff [code]: 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71955
diff
changeset

1228 
\<open>even_word a \<longleftrightarrow> a AND 1 = 0\<close> 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71955
diff
changeset

1229 
by (simp add: and_one_eq even_iff_mod_2_eq_zero even_word_def) 
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71955
diff
changeset

1230 

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

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

1232 
\<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:
71958
diff
changeset

1233 
by (simp add: bit_iff_odd_drop_bit odd_iff_mod_2_eq_one and_one_eq) 
71957
3e162c63371a
build bit operations on word on library theory on bit operations
haftmann
parents:
71955
diff
changeset

1234 

72079  1235 
lemma map_bit_range_eq_if_take_bit_eq: 
1236 
\<open>map (bit k) [0..<n] = map (bit l) [0..<n]\<close> 

1237 
if \<open>take_bit n k = take_bit n l\<close> for k l :: int 

1238 
using that proof (induction n arbitrary: k l) 

1239 
case 0 

1240 
then show ?case 

1241 
by simp 

1242 
next 

1243 
case (Suc n) 

1244 
from Suc.prems have \<open>take_bit n (k div 2) = take_bit n (l div 2)\<close> 

1245 
by (simp add: take_bit_Suc) 

1246 
then have \<open>map (bit (k div 2)) [0..<n] = map (bit (l div 2)) [0..<n]\<close> 

1247 
by (rule Suc.IH) 

1248 
moreover have \<open>bit (r div 2) = bit r \<circ> Suc\<close> for r :: int 

1249 
by (simp add: fun_eq_iff bit_Suc) 

1250 
moreover from Suc.prems have \<open>even k \<longleftrightarrow> even l\<close> 

1251 
by (auto simp add: take_bit_Suc elim!: evenE oddE) arith+ 

1252 
ultimately show ?case 

1253 
by (simp only: map_Suc_upt upt_conv_Cons flip: list.map_comp) simp 

1254 
qed 

1255 

1256 
lemma bit_of_bl_iff: 

1257 
\<open>bit (of_bl bs :: 'a word) n \<longleftrightarrow> rev bs ! n \<and> n < LENGTH('a::len) \<and> n < length bs\<close> 

1258 
by (auto simp add: of_bl_def bit_word_of_int_iff bin_nth_of_bl) 

1259 

1260 
lemma rev_to_bl_eq: 

1261 
\<open>rev (to_bl w) = map (bit w) [0..<LENGTH('a)]\<close> 

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

1263 
apply (rule nth_equalityI) 

1264 
apply (simp add: to_bl.rep_eq) 

1265 
apply (simp add: bin_nth_bl bit_word.rep_eq to_bl.rep_eq) 

1266 
done 

1267 

1268 
lemma of_bl_rev_eq: 

1269 
\<open>of_bl (rev bs) = horner_sum of_bool 2 bs\<close> 

1270 
apply (rule bit_word_eqI) 

1271 
apply (simp add: bit_of_bl_iff) 

1272 
apply transfer 

1273 
apply (simp add: bit_horner_sum_bit_iff ac_simps) 

1274 
done 

1275 

1276 

1277 
subsection \<open>More shift operations\<close> 

1278 

1279 
lift_definition sshiftr1 :: \<open>'a::len word \<Rightarrow> 'a word\<close> 

1280 
is \<open>\<lambda>k. take_bit LENGTH('a) (signed_take_bit (LENGTH('a)  1) k div 2)\<close> 

1281 
by (simp flip: signed_take_bit_decr_length_iff) 

1282 

1283 
lift_definition sshiftr :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> 'a word\<close> (infixl \<open>>>>\<close> 55) 

1284 
is \<open>\<lambda>k n. take_bit LENGTH('a) (drop_bit n (signed_take_bit (LENGTH('a)  1) k))\<close> 

1285 
by (simp flip: signed_take_bit_decr_length_iff) 

1286 

1287 
lift_definition bshiftr1 :: \<open>bool \<Rightarrow> 'a::len word \<Rightarrow> 'a word\<close> 

1288 
is \<open>\<lambda>b k. take_bit LENGTH('a) k div 2 + of_bool b * 2 ^ (LENGTH('a)  Suc 0)\<close> 

1289 
by (fact arg_cong) 

1290 

1291 
lemma sshiftr1_eq: 

1292 
\<open>sshiftr1 w = word_of_int (bin_rest (sint w))\<close> 

1293 
by transfer simp 

1294 

1295 
lemma bshiftr1_eq: 

1296 
\<open>bshiftr1 b w = of_bl (b # butlast (to_bl w))\<close> 

1297 
apply transfer 

1298 
apply auto 

1299 
apply (subst bl_to_bin_app_cat [of \<open>[True]\<close>, simplified]) 

1300 
apply simp 

1301 
apply (metis One_nat_def add.commute bin_bl_bin bin_last_bl_to_bin bin_rest_bl_to_bin butlast_bin_rest concat_bit_eq last.simps list.distinct(1) list.size(3) list.size(4) odd_iff_mod_2_eq_one plus_1_eq_Suc power_Suc0_right push_bit_of_1 size_bin_to_bl take_bit_eq_mod trunc_bl2bin_len) 

1302 
apply (simp add: butlast_rest_bl2bin) 

1303 
done 

1304 

1305 
lemma sshiftr_eq: 

1306 
\<open>w >>> n = (sshiftr1 ^^ n) w\<close> 

1307 
proof  

1308 
have *: \<open>(\<lambda>k. take_bit LENGTH('a) (signed_take_bit (LENGTH('a)  Suc 0) k div 2)) ^^ Suc n = 

1309 
take_bit LENGTH('a) \<circ> drop_bit (Suc n) \<circ> signed_take_bit (LENGTH('a)  Suc 0)\<close> 

1310 
for n 

1311 
apply (induction n) 

1312 
apply (auto simp add: fun_eq_iff drop_bit_Suc) 

1313 
apply (metis (no_types, lifting) Suc_pred funpow_swap1 len_gt_0 sbintrunc_bintrunc sbintrunc_rest) 

1314 
done 

1315 
show ?thesis 

1316 
apply transfer 