author  haftmann 
Tue, 04 Aug 2020 09:33:05 +0000  
changeset 72082  41393ecb57ac 
parent 72079  8c355e2dd7db 
child 72083  3ec876181527 
permissions  rwrr 
71042
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
diff
changeset

1 
(* Author: Florian Haftmann, TUM 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
diff
changeset

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

3 

71956  4 
section \<open>Bit operations in suitable algebraic structures\<close> 
71042
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
diff
changeset

5 

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

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

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

8 
"HOLLibrary.Boolean_Algebra" 
71095  9 
Main 
71042
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
diff
changeset

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

11 

71956  12 
subsection \<open>Bit operations\<close> 
71042
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
diff
changeset

13 

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

14 
class semiring_bit_operations = semiring_bit_shifts + 
71426  15 
fixes "and" :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixr \<open>AND\<close> 64) 
16 
and or :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixr \<open>OR\<close> 59) 

17 
and xor :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixr \<open>XOR\<close> 59) 

72082  18 
and mask :: \<open>nat \<Rightarrow> 'a\<close> 
71186  19 
assumes bit_and_iff: \<open>\<And>n. bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close> 
20 
and bit_or_iff: \<open>\<And>n. bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close> 

21 
and bit_xor_iff: \<open>\<And>n. bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close> 

72082  22 
and mask_eq_exp_minus_1: \<open>mask n = 2 ^ n  1\<close> 
71042
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
diff
changeset

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

24 

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

25 
text \<open> 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
diff
changeset

26 
We want the bitwise operations to bind slightly weaker 
71094  27 
than \<open>+\<close> and \<open>\<close>. 
71042
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
diff
changeset

28 
For the sake of code generation 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
diff
changeset

29 
the operations \<^const>\<open>and\<close>, \<^const>\<open>or\<close> and \<^const>\<open>xor\<close> 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
diff
changeset

30 
are specified as definitional class operations. 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
diff
changeset

31 
\<close> 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
diff
changeset

32 

71418  33 
sublocale "and": semilattice \<open>(AND)\<close> 
34 
by standard (auto simp add: bit_eq_iff bit_and_iff) 

35 

36 
sublocale or: semilattice_neutr \<open>(OR)\<close> 0 

37 
by standard (auto simp add: bit_eq_iff bit_or_iff) 

38 

39 
sublocale xor: comm_monoid \<open>(XOR)\<close> 0 

40 
by standard (auto simp add: bit_eq_iff bit_xor_iff) 

41 

71823  42 
lemma even_and_iff: 
43 
\<open>even (a AND b) \<longleftrightarrow> even a \<or> even b\<close> 

44 
using bit_and_iff [of a b 0] by auto 

45 

46 
lemma even_or_iff: 

47 
\<open>even (a OR b) \<longleftrightarrow> even a \<and> even b\<close> 

48 
using bit_or_iff [of a b 0] by auto 

49 

50 
lemma even_xor_iff: 

51 
\<open>even (a XOR b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)\<close> 

52 
using bit_xor_iff [of a b 0] by auto 

53 

71412  54 
lemma zero_and_eq [simp]: 
55 
"0 AND a = 0" 

56 
by (simp add: bit_eq_iff bit_and_iff) 

57 

58 
lemma and_zero_eq [simp]: 

59 
"a AND 0 = 0" 

60 
by (simp add: bit_eq_iff bit_and_iff) 

61 

71921  62 
lemma one_and_eq: 
71822  63 
"1 AND a = a mod 2" 
71418  64 
by (simp add: bit_eq_iff bit_and_iff) (auto simp add: bit_1_iff) 
71412  65 

71921  66 
lemma and_one_eq: 
71822  67 
"a AND 1 = a mod 2" 
71418  68 
using one_and_eq [of a] by (simp add: ac_simps) 
69 

71822  70 
lemma one_or_eq: 
71418  71 
"1 OR a = a + of_bool (even a)" 
72 
by (simp add: bit_eq_iff bit_or_iff add.commute [of _ 1] even_bit_succ_iff) (auto simp add: bit_1_iff) 

71412  73 

71822  74 
lemma or_one_eq: 
71418  75 
"a OR 1 = a + of_bool (even a)" 
76 
using one_or_eq [of a] by (simp add: ac_simps) 

71412  77 

71822  78 
lemma one_xor_eq: 
71418  79 
"1 XOR a = a + of_bool (even a)  of_bool (odd a)" 
80 
by (simp add: bit_eq_iff bit_xor_iff add.commute [of _ 1] even_bit_succ_iff) (auto simp add: bit_1_iff odd_bit_iff_bit_pred elim: oddE) 

81 

71822  82 
lemma xor_one_eq: 
71418  83 
"a XOR 1 = a + of_bool (even a)  of_bool (odd a)" 
84 
using one_xor_eq [of a] by (simp add: ac_simps) 

71412  85 

71409  86 
lemma take_bit_and [simp]: 
87 
\<open>take_bit n (a AND b) = take_bit n a AND take_bit n b\<close> 

88 
by (auto simp add: bit_eq_iff bit_take_bit_iff bit_and_iff) 

89 

90 
lemma take_bit_or [simp]: 

91 
\<open>take_bit n (a OR b) = take_bit n a OR take_bit n b\<close> 

92 
by (auto simp add: bit_eq_iff bit_take_bit_iff bit_or_iff) 

93 

94 
lemma take_bit_xor [simp]: 

95 
\<open>take_bit n (a XOR b) = take_bit n a XOR take_bit n b\<close> 

96 
by (auto simp add: bit_eq_iff bit_take_bit_iff bit_xor_iff) 

97 

71823  98 
lemma bit_mask_iff: 
99 
\<open>bit (mask m) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n < m\<close> 

100 
by (simp add: mask_eq_exp_minus_1 bit_mask_iff) 

101 

102 
lemma even_mask_iff: 

103 
\<open>even (mask n) \<longleftrightarrow> n = 0\<close> 

104 
using bit_mask_iff [of n 0] by auto 

105 

72082  106 
lemma mask_0 [simp]: 
71823  107 
\<open>mask 0 = 0\<close> 
108 
by (simp add: mask_eq_exp_minus_1) 

109 

72082  110 
lemma mask_Suc_0 [simp]: 
111 
\<open>mask (Suc 0) = 1\<close> 

112 
by (simp add: mask_eq_exp_minus_1 add_implies_diff sym) 

113 

114 
lemma mask_Suc_exp: 

71823  115 
\<open>mask (Suc n) = 2 ^ n OR mask n\<close> 
116 
by (rule bit_eqI) 

117 
(auto simp add: bit_or_iff bit_mask_iff bit_exp_iff not_less le_less_Suc_eq) 

118 

119 
lemma mask_Suc_double: 

72082  120 
\<open>mask (Suc n) = 1 OR 2 * mask n\<close> 
71823  121 
proof (rule bit_eqI) 
122 
fix q 

123 
assume \<open>2 ^ q \<noteq> 0\<close> 

72082  124 
show \<open>bit (mask (Suc n)) q \<longleftrightarrow> bit (1 OR 2 * mask n) q\<close> 
71823  125 
by (cases q) 
126 
(simp_all add: even_mask_iff even_or_iff bit_or_iff bit_mask_iff bit_exp_iff bit_double_iff not_less le_less_Suc_eq bit_1_iff, auto simp add: mult_2) 

127 
qed 

128 

72082  129 
lemma mask_numeral: 
130 
\<open>mask (numeral n) = 1 + 2 * mask (pred_numeral n)\<close> 

131 
by (simp add: numeral_eq_Suc mask_Suc_double one_or_eq ac_simps) 

132 

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

133 
lemma take_bit_eq_mask: 
71823  134 
\<open>take_bit n a = a AND mask n\<close> 
135 
by (rule bit_eqI) 

136 
(auto simp add: bit_take_bit_iff bit_and_iff bit_mask_iff) 

137 

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

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

139 

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

140 
class ring_bit_operations = semiring_bit_operations + ring_parity + 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
diff
changeset

141 
fixes not :: \<open>'a \<Rightarrow> 'a\<close> (\<open>NOT\<close>) 
71186  142 
assumes bit_not_iff: \<open>\<And>n. bit (NOT a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> \<not> bit a n\<close> 
71409  143 
assumes minus_eq_not_minus_1: \<open> a = NOT (a  1)\<close> 
71042
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
diff
changeset

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

145 

71409  146 
text \<open> 
147 
For the sake of code generation \<^const>\<open>not\<close> is specified as 

148 
definitional class operation. Note that \<^const>\<open>not\<close> has no 

149 
sensible definition for unlimited but only positive bit strings 

150 
(type \<^typ>\<open>nat\<close>). 

151 
\<close> 

152 

71186  153 
lemma bits_minus_1_mod_2_eq [simp]: 
154 
\<open>( 1) mod 2 = 1\<close> 

155 
by (simp add: mod_2_eq_odd) 

156 

71409  157 
lemma not_eq_complement: 
158 
\<open>NOT a =  a  1\<close> 

159 
using minus_eq_not_minus_1 [of \<open>a + 1\<close>] by simp 

160 

161 
lemma minus_eq_not_plus_1: 

162 
\<open> a = NOT a + 1\<close> 

163 
using not_eq_complement [of a] by simp 

164 

165 
lemma bit_minus_iff: 

166 
\<open>bit ( a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> \<not> bit (a  1) n\<close> 

167 
by (simp add: minus_eq_not_minus_1 bit_not_iff) 

168 

71418  169 
lemma even_not_iff [simp]: 
170 
"even (NOT a) \<longleftrightarrow> odd a" 

171 
using bit_not_iff [of a 0] by auto 

172 

71409  173 
lemma bit_not_exp_iff: 
174 
\<open>bit (NOT (2 ^ m)) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n \<noteq> m\<close> 

175 
by (auto simp add: bit_not_iff bit_exp_iff) 

176 

71186  177 
lemma bit_minus_1_iff [simp]: 
178 
\<open>bit ( 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0\<close> 

71409  179 
by (simp add: bit_minus_iff) 
180 

181 
lemma bit_minus_exp_iff: 

182 
\<open>bit ( (2 ^ m)) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n \<ge> m\<close> 

183 
oops 

184 

185 
lemma bit_minus_2_iff [simp]: 

186 
\<open>bit ( 2) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n > 0\<close> 

187 
by (simp add: bit_minus_iff bit_1_iff) 

71186  188 

71418  189 
lemma not_one [simp]: 
190 
"NOT 1 =  2" 

191 
by (simp add: bit_eq_iff bit_not_iff) (simp add: bit_1_iff) 

192 

193 
sublocale "and": semilattice_neutr \<open>(AND)\<close> \<open> 1\<close> 

194 
apply standard 

71426  195 
apply (simp add: bit_eq_iff bit_and_iff) 
196 
apply (auto simp add: exp_eq_0_imp_not_bit bit_exp_iff) 

71418  197 
done 
198 

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

199 
sublocale bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open> 1\<close> 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
diff
changeset

200 
rewrites \<open>bit.xor = (XOR)\<close> 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
diff
changeset

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

202 
interpret bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open> 1\<close> 
71186  203 
apply standard 
71965
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71956
diff
changeset

204 
apply (simp_all add: bit_eq_iff) 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71956
diff
changeset

205 
apply (auto simp add: bit_and_iff bit_or_iff bit_not_iff bit_exp_iff exp_eq_0_imp_not_bit) 
71186  206 
done 
71042
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
diff
changeset

207 
show \<open>boolean_algebra (AND) (OR) NOT 0 ( 1)\<close> 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
diff
changeset

208 
by standard 
71426  209 
show \<open>boolean_algebra.xor (AND) (OR) NOT = (XOR)\<close> 
71965
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71956
diff
changeset

210 
apply (simp add: fun_eq_iff bit_eq_iff bit.xor_def) 
d45f5d4c41bd
more class operations for the sake of efficient generated code
haftmann
parents:
71956
diff
changeset

211 
apply (auto simp add: bit_and_iff bit_or_iff bit_not_iff bit_xor_iff exp_eq_0_imp_not_bit) 
71186  212 
done 
71042
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
diff
changeset

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

214 

71802  215 
lemma and_eq_not_not_or: 
216 
\<open>a AND b = NOT (NOT a OR NOT b)\<close> 

217 
by simp 

218 

219 
lemma or_eq_not_not_and: 

220 
\<open>a OR b = NOT (NOT a AND NOT b)\<close> 

221 
by simp 

222 

72009  223 
lemma not_add_distrib: 
224 
\<open>NOT (a + b) = NOT a  b\<close> 

225 
by (simp add: not_eq_complement algebra_simps) 

226 

227 
lemma not_diff_distrib: 

228 
\<open>NOT (a  b) = NOT a + b\<close> 

229 
using not_add_distrib [of a \<open> b\<close>] by simp 

230 

71412  231 
lemma push_bit_minus: 
232 
\<open>push_bit n ( a) =  push_bit n a\<close> 

233 
by (simp add: push_bit_eq_mult) 

234 

71409  235 
lemma take_bit_not_take_bit: 
236 
\<open>take_bit n (NOT (take_bit n a)) = take_bit n (NOT a)\<close> 

237 
by (auto simp add: bit_eq_iff bit_take_bit_iff bit_not_iff) 

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

238 

71418  239 
lemma take_bit_not_iff: 
240 
"take_bit n (NOT a) = take_bit n (NOT b) \<longleftrightarrow> take_bit n a = take_bit n b" 

241 
apply (simp add: bit_eq_iff bit_not_iff bit_take_bit_iff) 

242 
apply (simp add: bit_exp_iff) 

243 
apply (use local.exp_eq_0_imp_not_bit in blast) 

244 
done 

245 

72079  246 
lemma mask_eq_take_bit_minus_one: 
247 
\<open>mask n = take_bit n ( 1)\<close> 

248 
by (simp add: bit_eq_iff bit_mask_iff bit_take_bit_iff conj_commute) 

249 

71922  250 
lemma take_bit_minus_one_eq_mask: 
251 
\<open>take_bit n ( 1) = mask n\<close> 

72079  252 
by (simp add: mask_eq_take_bit_minus_one) 
71922  253 

72010  254 
lemma minus_exp_eq_not_mask: 
255 
\<open> (2 ^ n) = NOT (mask n)\<close> 

256 
by (rule bit_eqI) (simp add: bit_minus_iff bit_not_iff flip: mask_eq_exp_minus_1) 

257 

71922  258 
lemma push_bit_minus_one_eq_not_mask: 
259 
\<open>push_bit n ( 1) = NOT (mask n)\<close> 

72010  260 
by (simp add: push_bit_eq_mult minus_exp_eq_not_mask) 
261 

262 
lemma take_bit_not_mask_eq_0: 

263 
\<open>take_bit m (NOT (mask n)) = 0\<close> if \<open>n \<ge> m\<close> 

264 
by (rule bit_eqI) (use that in \<open>simp add: bit_take_bit_iff bit_not_iff bit_mask_iff\<close>) 

71922  265 

72079  266 
lemma take_bit_mask [simp]: 
267 
\<open>take_bit m (mask n) = mask (min m n)\<close> 

268 
by (simp add: mask_eq_take_bit_minus_one) 

269 

71426  270 
definition set_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close> 
71991  271 
where \<open>set_bit n a = a OR push_bit n 1\<close> 
71426  272 

273 
definition unset_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close> 

71991  274 
where \<open>unset_bit n a = a AND NOT (push_bit n 1)\<close> 
71426  275 

276 
definition flip_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close> 

71991  277 
where \<open>flip_bit n a = a XOR push_bit n 1\<close> 
71426  278 

279 
lemma bit_set_bit_iff: 

280 
\<open>bit (set_bit m a) n \<longleftrightarrow> bit a n \<or> (m = n \<and> 2 ^ n \<noteq> 0)\<close> 

71991  281 
by (auto simp add: set_bit_def push_bit_of_1 bit_or_iff bit_exp_iff) 
71426  282 

283 
lemma even_set_bit_iff: 

284 
\<open>even (set_bit m a) \<longleftrightarrow> even a \<and> m \<noteq> 0\<close> 

285 
using bit_set_bit_iff [of m a 0] by auto 

286 

287 
lemma bit_unset_bit_iff: 

288 
\<open>bit (unset_bit m a) n \<longleftrightarrow> bit a n \<and> m \<noteq> n\<close> 

71991  289 
by (auto simp add: unset_bit_def push_bit_of_1 bit_and_iff bit_not_iff bit_exp_iff exp_eq_0_imp_not_bit) 
71426  290 

291 
lemma even_unset_bit_iff: 

292 
\<open>even (unset_bit m a) \<longleftrightarrow> even a \<or> m = 0\<close> 

293 
using bit_unset_bit_iff [of m a 0] by auto 

294 

295 
lemma bit_flip_bit_iff: 

296 
\<open>bit (flip_bit m a) n \<longleftrightarrow> (m = n \<longleftrightarrow> \<not> bit a n) \<and> 2 ^ n \<noteq> 0\<close> 

71991  297 
by (auto simp add: flip_bit_def push_bit_of_1 bit_xor_iff bit_exp_iff exp_eq_0_imp_not_bit) 
71426  298 

299 
lemma even_flip_bit_iff: 

300 
\<open>even (flip_bit m a) \<longleftrightarrow> \<not> (even a \<longleftrightarrow> m = 0)\<close> 

301 
using bit_flip_bit_iff [of m a 0] by auto 

302 

303 
lemma set_bit_0 [simp]: 

304 
\<open>set_bit 0 a = 1 + 2 * (a div 2)\<close> 

305 
proof (rule bit_eqI) 

306 
fix m 

307 
assume *: \<open>2 ^ m \<noteq> 0\<close> 

308 
then show \<open>bit (set_bit 0 a) m = bit (1 + 2 * (a div 2)) m\<close> 

309 
by (simp add: bit_set_bit_iff bit_double_iff even_bit_succ_iff) 

71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71442
diff
changeset

310 
(cases m, simp_all add: bit_Suc) 
71426  311 
qed 
312 

71821  313 
lemma set_bit_Suc: 
71426  314 
\<open>set_bit (Suc n) a = a mod 2 + 2 * set_bit n (a div 2)\<close> 
315 
proof (rule bit_eqI) 

316 
fix m 

317 
assume *: \<open>2 ^ m \<noteq> 0\<close> 

318 
show \<open>bit (set_bit (Suc n) a) m \<longleftrightarrow> bit (a mod 2 + 2 * set_bit n (a div 2)) m\<close> 

319 
proof (cases m) 

320 
case 0 

321 
then show ?thesis 

322 
by (simp add: even_set_bit_iff) 

323 
next 

324 
case (Suc m) 

325 
with * have \<open>2 ^ m \<noteq> 0\<close> 

326 
using mult_2 by auto 

327 
show ?thesis 

328 
by (cases a rule: parity_cases) 

329 
(simp_all add: bit_set_bit_iff bit_double_iff even_bit_succ_iff *, 

71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71442
diff
changeset

330 
simp_all add: Suc \<open>2 ^ m \<noteq> 0\<close> bit_Suc) 
71426  331 
qed 
332 
qed 

333 

334 
lemma unset_bit_0 [simp]: 

335 
\<open>unset_bit 0 a = 2 * (a div 2)\<close> 

336 
proof (rule bit_eqI) 

337 
fix m 

338 
assume *: \<open>2 ^ m \<noteq> 0\<close> 

339 
then show \<open>bit (unset_bit 0 a) m = bit (2 * (a div 2)) m\<close> 

340 
by (simp add: bit_unset_bit_iff bit_double_iff) 

71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71442
diff
changeset

341 
(cases m, simp_all add: bit_Suc) 
71426  342 
qed 
343 

71821  344 
lemma unset_bit_Suc: 
71426  345 
\<open>unset_bit (Suc n) a = a mod 2 + 2 * unset_bit n (a div 2)\<close> 
346 
proof (rule bit_eqI) 

347 
fix m 

348 
assume *: \<open>2 ^ m \<noteq> 0\<close> 

349 
then show \<open>bit (unset_bit (Suc n) a) m \<longleftrightarrow> bit (a mod 2 + 2 * unset_bit n (a div 2)) m\<close> 

350 
proof (cases m) 

351 
case 0 

352 
then show ?thesis 

353 
by (simp add: even_unset_bit_iff) 

354 
next 

355 
case (Suc m) 

356 
show ?thesis 

357 
by (cases a rule: parity_cases) 

358 
(simp_all add: bit_unset_bit_iff bit_double_iff even_bit_succ_iff *, 

71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71442
diff
changeset

359 
simp_all add: Suc bit_Suc) 
71426  360 
qed 
361 
qed 

362 

363 
lemma flip_bit_0 [simp]: 

364 
\<open>flip_bit 0 a = of_bool (even a) + 2 * (a div 2)\<close> 

365 
proof (rule bit_eqI) 

366 
fix m 

367 
assume *: \<open>2 ^ m \<noteq> 0\<close> 

368 
then show \<open>bit (flip_bit 0 a) m = bit (of_bool (even a) + 2 * (a div 2)) m\<close> 

369 
by (simp add: bit_flip_bit_iff bit_double_iff even_bit_succ_iff) 

71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71442
diff
changeset

370 
(cases m, simp_all add: bit_Suc) 
71426  371 
qed 
372 

71821  373 
lemma flip_bit_Suc: 
71426  374 
\<open>flip_bit (Suc n) a = a mod 2 + 2 * flip_bit n (a div 2)\<close> 
375 
proof (rule bit_eqI) 

376 
fix m 

377 
assume *: \<open>2 ^ m \<noteq> 0\<close> 

378 
show \<open>bit (flip_bit (Suc n) a) m \<longleftrightarrow> bit (a mod 2 + 2 * flip_bit n (a div 2)) m\<close> 

379 
proof (cases m) 

380 
case 0 

381 
then show ?thesis 

382 
by (simp add: even_flip_bit_iff) 

383 
next 

384 
case (Suc m) 

385 
with * have \<open>2 ^ m \<noteq> 0\<close> 

386 
using mult_2 by auto 

387 
show ?thesis 

388 
by (cases a rule: parity_cases) 

389 
(simp_all add: bit_flip_bit_iff bit_double_iff even_bit_succ_iff, 

71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71442
diff
changeset

390 
simp_all add: Suc \<open>2 ^ m \<noteq> 0\<close> bit_Suc) 
71426  391 
qed 
392 
qed 

393 

72009  394 
lemma flip_bit_eq_if: 
395 
\<open>flip_bit n a = (if bit a n then unset_bit else set_bit) n a\<close> 

396 
by (rule bit_eqI) (auto simp add: bit_set_bit_iff bit_unset_bit_iff bit_flip_bit_iff) 

397 

71986  398 
lemma take_bit_set_bit_eq: 
72009  399 
\<open>take_bit n (set_bit m a) = (if n \<le> m then take_bit n a else set_bit m (take_bit n a))\<close> 
71986  400 
by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_set_bit_iff) 
401 

402 
lemma take_bit_unset_bit_eq: 

72009  403 
\<open>take_bit n (unset_bit m a) = (if n \<le> m then take_bit n a else unset_bit m (take_bit n a))\<close> 
71986  404 
by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_unset_bit_iff) 
405 

406 
lemma take_bit_flip_bit_eq: 

72009  407 
\<open>take_bit n (flip_bit m a) = (if n \<le> m then take_bit n a else flip_bit m (take_bit n a))\<close> 
71986  408 
by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_flip_bit_iff) 
409 

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

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

411 

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

412 

71956  413 
subsection \<open>Instance \<^typ>\<open>int\<close>\<close> 
71042
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
diff
changeset

414 

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

415 
instantiation int :: ring_bit_operations 
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
diff
changeset

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

417 

71420  418 
definition not_int :: \<open>int \<Rightarrow> int\<close> 
419 
where \<open>not_int k =  k  1\<close> 

420 

421 
lemma not_int_rec: 

422 
"NOT k = of_bool (even k) + 2 * NOT (k div 2)" for k :: int 

423 
by (auto simp add: not_int_def elim: oddE) 

424 

425 
lemma even_not_iff_int: 

426 
\<open>even (NOT k) \<longleftrightarrow> odd k\<close> for k :: int 

427 
by (simp add: not_int_def) 

428 

429 
lemma not_int_div_2: 

430 
\<open>NOT k div 2 = NOT (k div 2)\<close> for k :: int 

431 
by (simp add: not_int_def) 

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

432 

71804
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

433 
lemma bit_not_int_iff: 
71186  434 
\<open>bit (NOT k) n \<longleftrightarrow> \<not> bit k n\<close> 
435 
for k :: int 

71535
b612edee9b0c
more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents:
71442
diff
changeset

436 
by (induction n arbitrary: k) (simp_all add: not_int_div_2 even_not_iff_int bit_Suc) 
71186  437 

71804
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

438 
function and_int :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close> 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

439 
where \<open>(k::int) AND l = (if k \<in> {0,  1} \<and> l \<in> {0,  1} 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

440 
then  of_bool (odd k \<and> odd l) 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

441 
else of_bool (odd k \<and> odd l) + 2 * ((k div 2) AND (l div 2)))\<close> 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

442 
by auto 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

443 

6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

444 
termination 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

445 
by (relation \<open>measure (\<lambda>(k, l). nat (\<bar>k\<bar> + \<bar>l\<bar>))\<close>) auto 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

446 

6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

447 
declare and_int.simps [simp del] 
71802  448 

71804
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

449 
lemma and_int_rec: 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

450 
\<open>k AND l = of_bool (odd k \<and> odd l) + 2 * ((k div 2) AND (l div 2))\<close> 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

451 
for k l :: int 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

452 
proof (cases \<open>k \<in> {0,  1} \<and> l \<in> {0,  1}\<close>) 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

453 
case True 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

454 
then show ?thesis 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

455 
by auto (simp_all add: and_int.simps) 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

456 
next 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

457 
case False 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

458 
then show ?thesis 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

459 
by (auto simp add: ac_simps and_int.simps [of k l]) 
71802  460 
qed 
461 

71804
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

462 
lemma bit_and_int_iff: 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

463 
\<open>bit (k AND l) n \<longleftrightarrow> bit k n \<and> bit l n\<close> for k l :: int 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

464 
proof (induction n arbitrary: k l) 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

465 
case 0 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

466 
then show ?case 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

467 
by (simp add: and_int_rec [of k l]) 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

468 
next 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

469 
case (Suc n) 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

470 
then show ?case 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

471 
by (simp add: and_int_rec [of k l] bit_Suc) 
71802  472 
qed 
473 

71804
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

474 
lemma even_and_iff_int: 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

475 
\<open>even (k AND l) \<longleftrightarrow> even k \<or> even l\<close> for k l :: int 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

476 
using bit_and_int_iff [of k l 0] by auto 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

477 

6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

478 
definition or_int :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close> 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

479 
where \<open>k OR l = NOT (NOT k AND NOT l)\<close> for k l :: int 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

480 

6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

481 
lemma or_int_rec: 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

482 
\<open>k OR l = of_bool (odd k \<or> odd l) + 2 * ((k div 2) OR (l div 2))\<close> 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

483 
for k l :: int 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

484 
using and_int_rec [of \<open>NOT k\<close> \<open>NOT l\<close>] 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

485 
by (simp add: or_int_def even_not_iff_int not_int_div_2) 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

486 
(simp add: not_int_def) 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

487 

6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

488 
lemma bit_or_int_iff: 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

489 
\<open>bit (k OR l) n \<longleftrightarrow> bit k n \<or> bit l n\<close> for k l :: int 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

490 
by (simp add: or_int_def bit_not_int_iff bit_and_int_iff) 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

491 

6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

492 
definition xor_int :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close> 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

493 
where \<open>k XOR l = k AND NOT l OR NOT k AND l\<close> for k l :: int 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

494 

6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

495 
lemma xor_int_rec: 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

496 
\<open>k XOR l = of_bool (odd k \<noteq> odd l) + 2 * ((k div 2) XOR (l div 2))\<close> 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

497 
for k l :: int 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

498 
by (simp add: xor_int_def or_int_rec [of \<open>k AND NOT l\<close> \<open>NOT k AND l\<close>] even_and_iff_int even_not_iff_int) 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

499 
(simp add: and_int_rec [of \<open>NOT k\<close> \<open>l\<close>] and_int_rec [of \<open>k\<close> \<open>NOT l\<close>] not_int_div_2) 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

500 

6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

501 
lemma bit_xor_int_iff: 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

502 
\<open>bit (k XOR l) n \<longleftrightarrow> bit k n \<noteq> bit l n\<close> for k l :: int 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

503 
by (auto simp add: xor_int_def bit_or_int_iff bit_and_int_iff bit_not_int_iff) 
71802  504 

72082  505 
definition mask_int :: \<open>nat \<Rightarrow> int\<close> 
506 
where \<open>mask n = (2 :: int) ^ n  1\<close> 

507 

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

508 
instance proof 
71186  509 
fix k l :: int and n :: nat 
71409  510 
show \<open> k = NOT (k  1)\<close> 
511 
by (simp add: not_int_def) 

71186  512 
show \<open>bit (k AND l) n \<longleftrightarrow> bit k n \<and> bit l n\<close> 
71804
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

513 
by (fact bit_and_int_iff) 
71186  514 
show \<open>bit (k OR l) n \<longleftrightarrow> bit k n \<or> bit l n\<close> 
71804
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

515 
by (fact bit_or_int_iff) 
71186  516 
show \<open>bit (k XOR l) n \<longleftrightarrow> bit k n \<noteq> bit l n\<close> 
71804
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

517 
by (fact bit_xor_int_iff) 
72082  518 
qed (simp_all add: bit_not_int_iff mask_int_def) 
71042
400e9512f1d3
proofofconcept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
diff
changeset

519 

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

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

521 

72009  522 
lemma disjunctive_add: 
523 
\<open>k + l = k OR l\<close> if \<open>\<And>n. \<not> bit k n \<or> \<not> bit l n\<close> for k l :: int 

524 
\<comment> \<open>TODO: may integrate (indirectly) into \<^class>\<open>semiring_bits\<close> premises\<close> 

525 
proof (rule bit_eqI) 

526 
fix n 

527 
from that have \<open>bit (k + l) n \<longleftrightarrow> bit k n \<or> bit l n\<close> 

528 
proof (induction n arbitrary: k l) 

529 
case 0 

530 
from this [of 0] show ?case 

531 
by auto 

532 
next 

533 
case (Suc n) 

534 
have \<open>bit ((k + l) div 2) n \<longleftrightarrow> bit (k div 2 + l div 2) n\<close> 

535 
using Suc.prems [of 0] div_add1_eq [of k l] by auto 

536 
also have \<open>bit (k div 2 + l div 2) n \<longleftrightarrow> bit (k div 2) n \<or> bit (l div 2) n\<close> 

537 
by (rule Suc.IH) (use Suc.prems in \<open>simp flip: bit_Suc\<close>) 

538 
finally show ?case 

539 
by (simp add: bit_Suc) 

540 
qed 

541 
also have \<open>\<dots> \<longleftrightarrow> bit (k OR l) n\<close> 

542 
by (simp add: bit_or_iff) 

543 
finally show \<open>bit (k + l) n \<longleftrightarrow> bit (k OR l) n\<close> . 

544 
qed 

545 

546 
lemma disjunctive_diff: 

547 
\<open>k  l = k AND NOT l\<close> if \<open>\<And>n. bit l n \<Longrightarrow> bit k n\<close> for k l :: int 

548 
proof  

549 
have \<open>NOT k + l = NOT k OR l\<close> 

550 
by (rule disjunctive_add) (auto simp add: bit_not_iff dest: that) 

551 
then have \<open>NOT (NOT k + l) = NOT (NOT k OR l)\<close> 

552 
by simp 

553 
then show ?thesis 

554 
by (simp add: not_add_distrib) 

555 
qed 

556 

72028  557 
lemma mask_nonnegative_int [simp]: 
558 
\<open>mask n \<ge> (0::int)\<close> 

559 
by (simp add: mask_eq_exp_minus_1) 

560 

561 
lemma not_mask_negative_int [simp]: 

562 
\<open>\<not> mask n < (0::int)\<close> 

563 
by (simp add: not_less) 

564 

71802  565 
lemma not_nonnegative_int_iff [simp]: 
566 
\<open>NOT k \<ge> 0 \<longleftrightarrow> k < 0\<close> for k :: int 

567 
by (simp add: not_int_def) 

568 

569 
lemma not_negative_int_iff [simp]: 

570 
\<open>NOT k < 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int 

571 
by (subst Not_eq_iff [symmetric]) (simp add: not_less not_le) 

572 

573 
lemma and_nonnegative_int_iff [simp]: 

574 
\<open>k AND l \<ge> 0 \<longleftrightarrow> k \<ge> 0 \<or> l \<ge> 0\<close> for k l :: int 

575 
proof (induction k arbitrary: l rule: int_bit_induct) 

576 
case zero 

577 
then show ?case 

578 
by simp 

579 
next 

580 
case minus 

581 
then show ?case 

582 
by simp 

583 
next 

584 
case (even k) 

585 
then show ?case 

71804
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

586 
using and_int_rec [of \<open>k * 2\<close> l] by (simp add: pos_imp_zdiv_nonneg_iff) 
71802  587 
next 
588 
case (odd k) 

589 
from odd have \<open>0 \<le> k AND l div 2 \<longleftrightarrow> 0 \<le> k \<or> 0 \<le> l div 2\<close> 

590 
by simp 

591 
then have \<open>0 \<le> (1 + k * 2) div 2 AND l div 2 \<longleftrightarrow> 0 \<le> (1 + k * 2) div 2\<or> 0 \<le> l div 2\<close> 

592 
by simp 

71804
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

593 
with and_int_rec [of \<open>1 + k * 2\<close> l] 
71802  594 
show ?case 
595 
by auto 

596 
qed 

597 

598 
lemma and_negative_int_iff [simp]: 

599 
\<open>k AND l < 0 \<longleftrightarrow> k < 0 \<and> l < 0\<close> for k l :: int 

600 
by (subst Not_eq_iff [symmetric]) (simp add: not_less) 

601 

72009  602 
lemma and_less_eq: 
603 
\<open>k AND l \<le> k\<close> if \<open>l < 0\<close> for k l :: int 

604 
using that proof (induction k arbitrary: l rule: int_bit_induct) 

605 
case zero 

606 
then show ?case 

607 
by simp 

608 
next 

609 
case minus 

610 
then show ?case 

611 
by simp 

612 
next 

613 
case (even k) 

614 
from even.IH [of \<open>l div 2\<close>] even.hyps even.prems 

615 
show ?case 

616 
by (simp add: and_int_rec [of _ l]) 

617 
next 

618 
case (odd k) 

619 
from odd.IH [of \<open>l div 2\<close>] odd.hyps odd.prems 

620 
show ?case 

621 
by (simp add: and_int_rec [of _ l]) 

622 
qed 

623 

71802  624 
lemma or_nonnegative_int_iff [simp]: 
625 
\<open>k OR l \<ge> 0 \<longleftrightarrow> k \<ge> 0 \<and> l \<ge> 0\<close> for k l :: int 

626 
by (simp only: or_eq_not_not_and not_nonnegative_int_iff) simp 

627 

628 
lemma or_negative_int_iff [simp]: 

629 
\<open>k OR l < 0 \<longleftrightarrow> k < 0 \<or> l < 0\<close> for k l :: int 

630 
by (subst Not_eq_iff [symmetric]) (simp add: not_less) 

631 

72009  632 
lemma or_greater_eq: 
633 
\<open>k OR l \<ge> k\<close> if \<open>l \<ge> 0\<close> for k l :: int 

634 
using that proof (induction k arbitrary: l rule: int_bit_induct) 

635 
case zero 

636 
then show ?case 

637 
by simp 

638 
next 

639 
case minus 

640 
then show ?case 

641 
by simp 

642 
next 

643 
case (even k) 

644 
from even.IH [of \<open>l div 2\<close>] even.hyps even.prems 

645 
show ?case 

646 
by (simp add: or_int_rec [of _ l]) 

647 
next 

648 
case (odd k) 

649 
from odd.IH [of \<open>l div 2\<close>] odd.hyps odd.prems 

650 
show ?case 

651 
by (simp add: or_int_rec [of _ l]) 

652 
qed 

653 

71802  654 
lemma xor_nonnegative_int_iff [simp]: 
655 
\<open>k XOR l \<ge> 0 \<longleftrightarrow> (k \<ge> 0 \<longleftrightarrow> l \<ge> 0)\<close> for k l :: int 

656 
by (simp only: bit.xor_def or_nonnegative_int_iff) auto 

657 

658 
lemma xor_negative_int_iff [simp]: 

659 
\<open>k XOR l < 0 \<longleftrightarrow> (k < 0) \<noteq> (l < 0)\<close> for k l :: int 

660 
by (subst Not_eq_iff [symmetric]) (auto simp add: not_less) 

661 

662 
lemma set_bit_nonnegative_int_iff [simp]: 

663 
\<open>set_bit n k \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int 

664 
by (simp add: set_bit_def) 

665 

666 
lemma set_bit_negative_int_iff [simp]: 

667 
\<open>set_bit n k < 0 \<longleftrightarrow> k < 0\<close> for k :: int 

668 
by (simp add: set_bit_def) 

669 

670 
lemma unset_bit_nonnegative_int_iff [simp]: 

671 
\<open>unset_bit n k \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int 

672 
by (simp add: unset_bit_def) 

673 

674 
lemma unset_bit_negative_int_iff [simp]: 

675 
\<open>unset_bit n k < 0 \<longleftrightarrow> k < 0\<close> for k :: int 

676 
by (simp add: unset_bit_def) 

677 

678 
lemma flip_bit_nonnegative_int_iff [simp]: 

679 
\<open>flip_bit n k \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int 

680 
by (simp add: flip_bit_def) 

681 

682 
lemma flip_bit_negative_int_iff [simp]: 

683 
\<open>flip_bit n k < 0 \<longleftrightarrow> k < 0\<close> for k :: int 

684 
by (simp add: flip_bit_def) 

685 

71986  686 
lemma set_bit_greater_eq: 
687 
\<open>set_bit n k \<ge> k\<close> for k :: int 

688 
by (simp add: set_bit_def or_greater_eq) 

689 

690 
lemma unset_bit_less_eq: 

691 
\<open>unset_bit n k \<le> k\<close> for k :: int 

692 
by (simp add: unset_bit_def and_less_eq) 

693 

72009  694 
lemma set_bit_eq: 
695 
\<open>set_bit n k = k + of_bool (\<not> bit k n) * 2 ^ n\<close> for k :: int 

696 
proof (rule bit_eqI) 

697 
fix m 

698 
show \<open>bit (set_bit n k) m \<longleftrightarrow> bit (k + of_bool (\<not> bit k n) * 2 ^ n) m\<close> 

699 
proof (cases \<open>m = n\<close>) 

700 
case True 

701 
then show ?thesis 

702 
apply (simp add: bit_set_bit_iff) 

703 
apply (simp add: bit_iff_odd div_plus_div_distrib_dvd_right) 

704 
done 

705 
next 

706 
case False 

707 
then show ?thesis 

708 
apply (clarsimp simp add: bit_set_bit_iff) 

709 
apply (subst disjunctive_add) 

710 
apply (clarsimp simp add: bit_exp_iff) 

711 
apply (clarsimp simp add: bit_or_iff bit_exp_iff) 

712 
done 

713 
qed 

714 
qed 

715 

716 
lemma unset_bit_eq: 

717 
\<open>unset_bit n k = k  of_bool (bit k n) * 2 ^ n\<close> for k :: int 

718 
proof (rule bit_eqI) 

719 
fix m 

720 
show \<open>bit (unset_bit n k) m \<longleftrightarrow> bit (k  of_bool (bit k n) * 2 ^ n) m\<close> 

721 
proof (cases \<open>m = n\<close>) 

722 
case True 

723 
then show ?thesis 

724 
apply (simp add: bit_unset_bit_iff) 

725 
apply (simp add: bit_iff_odd) 

726 
using div_plus_div_distrib_dvd_right [of \<open>2 ^ n\<close> \<open> (2 ^ n)\<close> k] 

727 
apply (simp add: dvd_neg_div) 

728 
done 

729 
next 

730 
case False 

731 
then show ?thesis 

732 
apply (clarsimp simp add: bit_unset_bit_iff) 

733 
apply (subst disjunctive_diff) 

734 
apply (clarsimp simp add: bit_exp_iff) 

735 
apply (clarsimp simp add: bit_and_iff bit_not_iff bit_exp_iff) 

736 
done 

737 
qed 

738 
qed 

739 

71442  740 

72028  741 
subsection \<open>Bit concatenation\<close> 
742 

743 
definition concat_bit :: \<open>nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int\<close> 

744 
where \<open>concat_bit n k l = (k AND mask n) OR push_bit n l\<close> 

745 

746 
lemma bit_concat_bit_iff: 

747 
\<open>bit (concat_bit m k l) n \<longleftrightarrow> n < m \<and> bit k n \<or> m \<le> n \<and> bit l (n  m)\<close> 

748 
by (simp add: concat_bit_def bit_or_iff bit_and_iff bit_mask_iff bit_push_bit_iff ac_simps) 

749 

750 
lemma concat_bit_eq: 

751 
\<open>concat_bit n k l = take_bit n k + push_bit n l\<close> 

752 
by (simp add: concat_bit_def take_bit_eq_mask 

753 
bit_and_iff bit_mask_iff bit_push_bit_iff disjunctive_add) 

754 

755 
lemma concat_bit_0 [simp]: 

756 
\<open>concat_bit 0 k l = l\<close> 

757 
by (simp add: concat_bit_def) 

758 

759 
lemma concat_bit_Suc: 

760 
\<open>concat_bit (Suc n) k l = k mod 2 + 2 * concat_bit n (k div 2) l\<close> 

761 
by (simp add: concat_bit_eq take_bit_Suc push_bit_double) 

762 

763 
lemma concat_bit_of_zero_1 [simp]: 

764 
\<open>concat_bit n 0 l = push_bit n l\<close> 

765 
by (simp add: concat_bit_def) 

766 

767 
lemma concat_bit_of_zero_2 [simp]: 

768 
\<open>concat_bit n k 0 = take_bit n k\<close> 

769 
by (simp add: concat_bit_def take_bit_eq_mask) 

770 

771 
lemma concat_bit_nonnegative_iff [simp]: 

772 
\<open>concat_bit n k l \<ge> 0 \<longleftrightarrow> l \<ge> 0\<close> 

773 
by (simp add: concat_bit_def) 

774 

775 
lemma concat_bit_negative_iff [simp]: 

776 
\<open>concat_bit n k l < 0 \<longleftrightarrow> l < 0\<close> 

777 
by (simp add: concat_bit_def) 

778 

779 
lemma concat_bit_assoc: 

780 
\<open>concat_bit n k (concat_bit m l r) = concat_bit (m + n) (concat_bit n k l) r\<close> 

781 
by (rule bit_eqI) (auto simp add: bit_concat_bit_iff ac_simps) 

782 

783 
lemma concat_bit_assoc_sym: 

784 
\<open>concat_bit m (concat_bit n k l) r = concat_bit (min m n) k (concat_bit (m  n) l r)\<close> 

785 
by (rule bit_eqI) (auto simp add: bit_concat_bit_iff ac_simps min_def) 

786 

787 

72010  788 
subsection \<open>Taking bit with sign propagation\<close> 
789 

72028  790 
definition signed_take_bit :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close> 
791 
where \<open>signed_take_bit n k = concat_bit n k ( of_bool (bit k n))\<close> 

72010  792 

793 
lemma signed_take_bit_eq: 

794 
\<open>signed_take_bit n k = take_bit n k\<close> if \<open>\<not> bit k n\<close> 

795 
using that by (simp add: signed_take_bit_def) 

796 

797 
lemma signed_take_bit_eq_or: 

798 
\<open>signed_take_bit n k = take_bit n k OR NOT (mask n)\<close> if \<open>bit k n\<close> 

72028  799 
using that by (simp add: signed_take_bit_def concat_bit_def take_bit_eq_mask push_bit_minus_one_eq_not_mask) 
72010  800 

801 
lemma signed_take_bit_0 [simp]: 

802 
\<open>signed_take_bit 0 k =  (k mod 2)\<close> 

803 
by (simp add: signed_take_bit_def odd_iff_mod_2_eq_one) 

804 

805 
lemma mask_half_int: 

806 
\<open>mask n div 2 = (mask (n  1) :: int)\<close> 

807 
by (cases n) (simp_all add: mask_eq_exp_minus_1 algebra_simps) 

808 

809 
lemma signed_take_bit_Suc: 

810 
\<open>signed_take_bit (Suc n) k = k mod 2 + 2 * signed_take_bit n (k div 2)\<close> 

811 
by (unfold signed_take_bit_def or_int_rec [of \<open>take_bit (Suc n) k\<close>]) 

72028  812 
(simp add: bit_Suc concat_bit_Suc even_or_iff even_mask_iff odd_iff_mod_2_eq_one not_int_div_2 mask_half_int) 
72010  813 

814 
lemma signed_take_bit_rec: 

815 
\<open>signed_take_bit n k = (if n = 0 then  (k mod 2) else k mod 2 + 2 * signed_take_bit (n  1) (k div 2))\<close> 

816 
by (cases n) (simp_all add: signed_take_bit_Suc) 

817 

818 
lemma bit_signed_take_bit_iff: 

819 
\<open>bit (signed_take_bit m k) n = bit k (min m n)\<close> 

72028  820 
by (simp add: signed_take_bit_def bit_or_iff bit_concat_bit_iff bit_not_iff bit_mask_iff min_def) 
72010  821 

822 
text \<open>Modulus centered around 0\<close> 

823 

824 
lemma signed_take_bit_eq_take_bit_minus: 

825 
\<open>signed_take_bit n k = take_bit (Suc n) k  2 ^ Suc n * of_bool (bit k n)\<close> 

826 
proof (cases \<open>bit k n\<close>) 

827 
case True 

828 
have \<open>signed_take_bit n k = take_bit (Suc n) k OR NOT (mask (Suc n))\<close> 

829 
by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_take_bit_iff bit_or_iff bit_not_iff bit_mask_iff less_Suc_eq True) 

830 
then have \<open>signed_take_bit n k = take_bit (Suc n) k + NOT (mask (Suc n))\<close> 

831 
by (simp add: disjunctive_add bit_take_bit_iff bit_not_iff bit_mask_iff) 

832 
with True show ?thesis 

833 
by (simp flip: minus_exp_eq_not_mask) 

834 
next 

835 
case False 

836 
then show ?thesis 

837 
by (simp add: bit_eq_iff bit_take_bit_iff bit_signed_take_bit_iff min_def) 

838 
(auto intro: bit_eqI simp add: less_Suc_eq) 

839 
qed 

840 

841 
lemma signed_take_bit_eq_take_bit_shift: 

842 
\<open>signed_take_bit n k = take_bit (Suc n) (k + 2 ^ n)  2 ^ n\<close> 

843 
proof  

844 
have *: \<open>take_bit n k OR 2 ^ n = take_bit n k + 2 ^ n\<close> 

845 
by (simp add: disjunctive_add bit_exp_iff bit_take_bit_iff) 

846 
have \<open>take_bit n k  2 ^ n = take_bit n k + NOT (mask n)\<close> 

847 
by (simp add: minus_exp_eq_not_mask) 

848 
also have \<open>\<dots> = take_bit n k OR NOT (mask n)\<close> 

849 
by (rule disjunctive_add) 

850 
(simp add: bit_exp_iff bit_take_bit_iff bit_not_iff bit_mask_iff) 

851 
finally have **: \<open>take_bit n k  2 ^ n = take_bit n k OR NOT (mask n)\<close> . 

852 
have \<open>take_bit (Suc n) (k + 2 ^ n) = take_bit (Suc n) (take_bit (Suc n) k + take_bit (Suc n) (2 ^ n))\<close> 

853 
by (simp only: take_bit_add) 

854 
also have \<open>take_bit (Suc n) k = 2 ^ n * of_bool (bit k n) + take_bit n k\<close> 

855 
by (simp add: take_bit_Suc_from_most) 

856 
finally have \<open>take_bit (Suc n) (k + 2 ^ n) = take_bit (Suc n) (2 ^ (n + of_bool (bit k n)) + take_bit n k)\<close> 

857 
by (simp add: ac_simps) 

858 
also have \<open>2 ^ (n + of_bool (bit k n)) + take_bit n k = 2 ^ (n + of_bool (bit k n)) OR take_bit n k\<close> 

859 
by (rule disjunctive_add) 

860 
(auto simp add: disjunctive_add bit_take_bit_iff bit_double_iff bit_exp_iff) 

861 
finally show ?thesis 

72028  862 
using * ** 
863 
by (simp add: signed_take_bit_def concat_bit_Suc min_def ac_simps) 

864 
(simp add: concat_bit_def take_bit_eq_mask push_bit_minus_one_eq_not_mask ac_simps) 

72010  865 
qed 
866 

867 
lemma signed_take_bit_of_0 [simp]: 

868 
\<open>signed_take_bit n 0 = 0\<close> 

869 
by (simp add: signed_take_bit_def) 

870 

871 
lemma signed_take_bit_of_minus_1 [simp]: 

872 
\<open>signed_take_bit n ( 1) =  1\<close> 

72028  873 
by (simp add: signed_take_bit_def concat_bit_def push_bit_minus_one_eq_not_mask take_bit_minus_one_eq_mask) 
72010  874 

875 
lemma signed_take_bit_eq_iff_take_bit_eq: 

876 
\<open>signed_take_bit n k = signed_take_bit n l \<longleftrightarrow> take_bit (Suc n) k = take_bit (Suc n) l\<close> 

877 
proof (cases \<open>bit k n \<longleftrightarrow> bit l n\<close>) 

878 
case True 

879 
moreover have \<open>take_bit n k OR NOT (mask n) = take_bit n k  2 ^ n\<close> 

880 
for k :: int 

881 
by (auto simp add: disjunctive_add [symmetric] bit_not_iff bit_mask_iff bit_take_bit_iff minus_exp_eq_not_mask) 

882 
ultimately show ?thesis 

72028  883 
by (simp add: signed_take_bit_def take_bit_Suc_from_most concat_bit_eq) 
72010  884 
next 
885 
case False 

886 
then have \<open>signed_take_bit n k \<noteq> signed_take_bit n l\<close> and \<open>take_bit (Suc n) k \<noteq> take_bit (Suc n) l\<close> 

887 
by (auto simp add: bit_eq_iff bit_take_bit_iff bit_signed_take_bit_iff min_def) 

888 
then show ?thesis 

889 
by simp 

890 
qed 

891 

892 
lemma signed_take_bit_signed_take_bit [simp]: 

893 
\<open>signed_take_bit m (signed_take_bit n k) = signed_take_bit (min m n) k\<close> 

894 
by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_or_iff bit_not_iff bit_mask_iff bit_take_bit_iff) 

895 

896 
lemma take_bit_signed_take_bit: 

72079  897 
\<open>take_bit m (signed_take_bit n k) = take_bit m k\<close> if \<open>m \<le> Suc n\<close> 
898 
using that by (rule le_SucE; intro bit_eqI) 

899 
(auto simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def less_Suc_eq) 

72010  900 

901 
lemma signed_take_bit_take_bit: 

902 
\<open>signed_take_bit m (take_bit n k) = (if n \<le> m then take_bit n else signed_take_bit m) k\<close> 

903 
by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_take_bit_iff) 

904 

905 
lemma signed_take_bit_nonnegative_iff [simp]: 

906 
\<open>0 \<le> signed_take_bit n k \<longleftrightarrow> \<not> bit k n\<close> 

72028  907 
by (simp add: signed_take_bit_def not_less concat_bit_def) 
72010  908 

909 
lemma signed_take_bit_negative_iff [simp]: 

910 
\<open>signed_take_bit n k < 0 \<longleftrightarrow> bit k n\<close> 

72028  911 
by (simp add: signed_take_bit_def not_less concat_bit_def) 
72010  912 

913 
lemma signed_take_bit_greater_eq: 

914 
\<open>k + 2 ^ Suc n \<le> signed_take_bit n k\<close> if \<open>k <  (2 ^ n)\<close> 

915 
using that take_bit_greater_eq [of \<open>k + 2 ^ n\<close> \<open>Suc n\<close>] 

916 
by (simp add: signed_take_bit_eq_take_bit_shift) 

917 

918 
lemma signed_take_bit_less_eq: 

919 
\<open>signed_take_bit n k \<le> k  2 ^ Suc n\<close> if \<open>k \<ge> 2 ^ n\<close> 

920 
using that take_bit_less_eq [of \<open>Suc n\<close> \<open>k + 2 ^ n\<close>] 

921 
by (simp add: signed_take_bit_eq_take_bit_shift) 

922 

923 
lemma signed_take_bit_Suc_1 [simp]: 

924 
\<open>signed_take_bit (Suc n) 1 = 1\<close> 

925 
by (simp add: signed_take_bit_Suc) 

926 

927 
lemma signed_take_bit_Suc_bit0 [simp]: 

928 
\<open>signed_take_bit (Suc n) (numeral (Num.Bit0 k)) = signed_take_bit n (numeral k) * 2\<close> 

929 
by (simp add: signed_take_bit_Suc) 

930 

931 
lemma signed_take_bit_Suc_bit1 [simp]: 

932 
\<open>signed_take_bit (Suc n) (numeral (Num.Bit1 k)) = signed_take_bit n (numeral k) * 2 + 1\<close> 

933 
by (simp add: signed_take_bit_Suc) 

934 

935 
lemma signed_take_bit_Suc_minus_bit0 [simp]: 

936 
\<open>signed_take_bit (Suc n) ( numeral (Num.Bit0 k)) = signed_take_bit n ( numeral k) * 2\<close> 

937 
by (simp add: signed_take_bit_Suc) 

938 

939 
lemma signed_take_bit_Suc_minus_bit1 [simp]: 

940 
\<open>signed_take_bit (Suc n) ( numeral (Num.Bit1 k)) = signed_take_bit n ( numeral k  1) * 2 + 1\<close> 

941 
by (simp add: signed_take_bit_Suc) 

942 

943 
lemma signed_take_bit_numeral_bit0 [simp]: 

944 
\<open>signed_take_bit (numeral l) (numeral (Num.Bit0 k)) = signed_take_bit (pred_numeral l) (numeral k) * 2\<close> 

945 
by (simp add: signed_take_bit_rec) 

946 

947 
lemma signed_take_bit_numeral_bit1 [simp]: 

948 
\<open>signed_take_bit (numeral l) (numeral (Num.Bit1 k)) = signed_take_bit (pred_numeral l) (numeral k) * 2 + 1\<close> 

949 
by (simp add: signed_take_bit_rec) 

950 

951 
lemma signed_take_bit_numeral_minus_bit0 [simp]: 

952 
\<open>signed_take_bit (numeral l) ( numeral (Num.Bit0 k)) = signed_take_bit (pred_numeral l) ( numeral k) * 2\<close> 

953 
by (simp add: signed_take_bit_rec) 

954 

955 
lemma signed_take_bit_numeral_minus_bit1 [simp]: 

956 
\<open>signed_take_bit (numeral l) ( numeral (Num.Bit1 k)) = signed_take_bit (pred_numeral l) ( numeral k  1) * 2 + 1\<close> 

957 
by (simp add: signed_take_bit_rec) 

958 

959 
lemma signed_take_bit_code [code]: 

960 
\<open>signed_take_bit n k = 

961 
(let l = k AND mask (Suc n) 

962 
in if bit l n then l  (push_bit n 2) else l)\<close> 

963 
proof  

964 
have *: \<open>(k AND mask (Suc n))  2 * 2 ^ n = k AND mask (Suc n) OR NOT (mask (Suc n))\<close> 

965 
apply (subst disjunctive_add [symmetric]) 

966 
apply (simp_all add: bit_and_iff bit_mask_iff bit_not_iff) 

967 
apply (simp flip: minus_exp_eq_not_mask) 

968 
done 

969 
show ?thesis 

970 
by (rule bit_eqI) 

971 
(auto simp add: Let_def bit_and_iff bit_signed_take_bit_iff push_bit_eq_mult min_def not_le bit_mask_iff bit_exp_iff less_Suc_eq * bit_or_iff bit_not_iff) 

972 
qed 

973 

974 

71956  975 
subsection \<open>Instance \<^typ>\<open>nat\<close>\<close> 
71804
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

976 

6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

977 
instantiation nat :: semiring_bit_operations 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

978 
begin 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

979 

6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

980 
definition and_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close> 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

981 
where \<open>m AND n = nat (int m AND int n)\<close> for m n :: nat 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

982 

6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

983 
definition or_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close> 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

984 
where \<open>m OR n = nat (int m OR int n)\<close> for m n :: nat 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

985 

6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

986 
definition xor_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close> 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

987 
where \<open>m XOR n = nat (int m XOR int n)\<close> for m n :: nat 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

988 

72082  989 
definition mask_nat :: \<open>nat \<Rightarrow> nat\<close> 
990 
where \<open>mask n = (2 :: nat) ^ n  1\<close> 

991 

71804
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

992 
instance proof 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

993 
fix m n q :: nat 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

994 
show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close> 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

995 
by (auto simp add: and_nat_def bit_and_iff less_le bit_eq_iff) 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

996 
show \<open>bit (m OR n) q \<longleftrightarrow> bit m q \<or> bit n q\<close> 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

997 
by (auto simp add: or_nat_def bit_or_iff less_le bit_eq_iff) 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

998 
show \<open>bit (m XOR n) q \<longleftrightarrow> bit m q \<noteq> bit n q\<close> 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

999 
by (auto simp add: xor_nat_def bit_xor_iff less_le bit_eq_iff) 
72082  1000 
qed (simp add: mask_nat_def) 
71804
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1001 

6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1002 
end 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1003 

6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1004 
lemma and_nat_rec: 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1005 
\<open>m AND n = of_bool (odd m \<and> odd n) + 2 * ((m div 2) AND (n div 2))\<close> for m n :: nat 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1006 
by (simp add: and_nat_def and_int_rec [of \<open>int m\<close> \<open>int n\<close>] zdiv_int nat_add_distrib nat_mult_distrib) 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1007 

6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1008 
lemma or_nat_rec: 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1009 
\<open>m OR n = of_bool (odd m \<or> odd n) + 2 * ((m div 2) OR (n div 2))\<close> for m n :: nat 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1010 
by (simp add: or_nat_def or_int_rec [of \<open>int m\<close> \<open>int n\<close>] zdiv_int nat_add_distrib nat_mult_distrib) 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1011 

6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1012 
lemma xor_nat_rec: 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1013 
\<open>m XOR n = of_bool (odd m \<noteq> odd n) + 2 * ((m div 2) XOR (n div 2))\<close> for m n :: nat 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1014 
by (simp add: xor_nat_def xor_int_rec [of \<open>int m\<close> \<open>int n\<close>] zdiv_int nat_add_distrib nat_mult_distrib) 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1015 

6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1016 
lemma Suc_0_and_eq [simp]: 
71822  1017 
\<open>Suc 0 AND n = n mod 2\<close> 
71804
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1018 
using one_and_eq [of n] by simp 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1019 

6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1020 
lemma and_Suc_0_eq [simp]: 
71822  1021 
\<open>n AND Suc 0 = n mod 2\<close> 
71804
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1022 
using and_one_eq [of n] by simp 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1023 

71822  1024 
lemma Suc_0_or_eq: 
71804
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1025 
\<open>Suc 0 OR n = n + of_bool (even n)\<close> 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1026 
using one_or_eq [of n] by simp 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1027 

71822  1028 
lemma or_Suc_0_eq: 
71804
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1029 
\<open>n OR Suc 0 = n + of_bool (even n)\<close> 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1030 
using or_one_eq [of n] by simp 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1031 

71822  1032 
lemma Suc_0_xor_eq: 
71804
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1033 
\<open>Suc 0 XOR n = n + of_bool (even n)  of_bool (odd n)\<close> 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1034 
using one_xor_eq [of n] by simp 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1035 

71822  1036 
lemma xor_Suc_0_eq: 
71804
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1037 
\<open>n XOR Suc 0 = n + of_bool (even n)  of_bool (odd n)\<close> 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1038 
using xor_one_eq [of n] by simp 
6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1039 

6fd70ed18199
simplified construction of binary bit operations
haftmann
parents:
71802
diff
changeset

1040 

71956  1041 
subsection \<open>Instances for \<^typ>\<open>integer\<close> and \<^typ>\<open>natural\<close>\<close> 
71442  1042 

1043 
unbundle integer.lifting natural.lifting 

1044 

1045 
instantiation integer :: ring_bit_operations 

1046 
begin 

1047 

1048 
lift_definition not_integer :: \<open>integer \<Rightarrow> integer\<close> 

1049 
is not . 

1050 

1051 
lift_definition and_integer :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close> 

1052 
is \<open>and\<close> . 

1053 

1054 
lift_definition or_integer :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close> 

1055 
is or . 

1056 

1057 
lift_definition xor_integer :: \<open>integer \<Rightarrow> integer \<Rightarrow> integer\<close> 

1058 
is xor . 

1059 

72082  1060 
lift_definition mask_integer :: \<open>nat \<Rightarrow> integer\<close> 
1061 
is mask . 

1062 

1063 
instance by (standard; transfer) 

1064 
(simp_all add: minus_eq_not_minus_1 mask_eq_exp_minus_1 

1065 
bit_not_iff bit_and_iff bit_or_iff bit_xor_iff) 

71442  1066 

1067 
end 

1068 

1069 
instantiation natural :: semiring_bit_operations 

1070 
begin 

1071 

1072 
lift_definition and_natural :: \<open>natural \<Rightarrow> natural \<Rightarrow> natural\<close> 

1073 
is \<open>and\<close> . 

1074 

1075 
lift_definition or_natural :: \<open>natural \<Rightarrow> natural \<Rightarrow> natural\<close> 

1076 
is or . 

1077 

1078 
lift_definition xor_natural :: \<open>natural \<Rightarrow> natural \<Rightarrow> natural\<close> 

1079 
is xor . 

1080 

72082  1081 
lift_definition mask_natural :: \<open>nat \<Rightarrow> natural\<close> 
1082 
is mask . 

1083 

1084 
instance by (standard; transfer) 

1085 
(simp_all add: mask_eq_exp_minus_1 bit_and_iff bit_or_iff bit_xor_iff) 

71442  1086 

1087 
end 

1088 

1089 
lifting_update integer.lifting 

1090 
lifting_forget integer.lifting 

1091 

1092 
lifting_update natural.lifting 

1093 
lifting_forget natural.lifting 

1094 

71800  1095 

1096 
subsection \<open>Key ideas of bit operations\<close> 

1097 

1098 
text \<open> 

1099 
When formalizing bit operations, it is tempting to represent 

1100 
bit values as explicit lists over a binary type. This however 

1101 
is a bad idea, mainly due to the inherent ambiguities in 

1102 
representation concerning repeating leading bits. 

1103 

1104 
Hence this approach avoids such explicit lists altogether 

1105 
following an algebraic path: 

1106 

1107 
\<^item> Bit values are represented by numeric types: idealized 

1108 
unbounded bit values can be represented by type \<^typ>\<open>int\<close>, 

1109 
bounded bit values by quotient types over \<^typ>\<open>int\<close>. 

1110 

1111 
\<^item> (A special case are idealized unbounded bit values ending 

1112 
in @{term [source] 0} which can be represented by type \<^typ>\<open>nat\<close> but 

1113 
only support a restricted set of operations). 

1114 

1115 
\<^item> From this idea follows that 

1116 

1117 
\<^item> multiplication by \<^term>\<open>2 :: int\<close> is a bit shift to the left and 

1118 

1119 
\<^item> division by \<^term>\<open>2 :: int\<close> is a bit shift to the right. 

1120 

1121 
\<^item> Concerning bounded bit values, iterated shifts to the left 

1122 
may result in eliminating all bits by shifting them all 

1123 
beyond the boundary. The property \<^prop>\<open>(2 :: int) ^ n \<noteq> 0\<close> 

1124 
represents that \<^term>\<open>n\<close> is \<^emph>\<open>not\<close> beyond that boundary. 

1125 

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

1126 
\<^item> The projection on a single bit is then @{thm bit_iff_odd [where ?'a = int, no_vars]}. 
71800  1127 

1128 
\<^item> This leads to the most fundamental properties of bit values: 

1129 

1130 
\<^item> Equality rule: @{thm bit_eqI [where ?'a = int, no_vars]} 

1131 

1132 
\<^item> Induction rule: @{thm bits_induct [where ?'a = int, no_vars]} 

1133 

1134 
\<^item> Typical operations are characterized as follows: 

1135 

1136 
\<^item> Singleton \<^term>\<open>n\<close>th bit: \<^term>\<open>(2 :: int) ^ n\<close> 

1137 

71956  1138 
\<^item> Bit mask upto bit \<^term>\<open>n\<close>: @{thm mask_eq_exp_minus_1 [where ?'a = int, no_vars]} 
71800  1139 

1140 
\<^item> Left shift: @{thm push_bit_eq_mult [where ?'a = int, no_vars]} 

1141 

1142 
\<^item> Right shift: @{thm drop_bit_eq_div [where ?'a = int, no_vars]} 

1143 

1144 
\<^item> Truncation: @{thm take_bit_eq_mod [where ?'a = int, no_vars]} 

1145 

1146 
\<^item> Negation: @{thm bit_not_iff [where ?'a = int, no_vars]} 

1147 

1148 
\<^item> And: @{thm bit_and_iff [where ?'a = int, no_vars]} 

1149 

1150 
\<^item> Or: @{thm bit_or_iff [where ?'a = int, no_vars]} 

1151 

1152 
\<^item> Xor: @{thm bit_xor_iff [where ?'a = int, no_vars]} 

1153 

1154 
\<^item> Set a single bit: @{thm set_bit_def [where ?'a = int, no_vars]} 

1155 

1156 
\<^item> Unset a single bit: @{thm unset_bit_def [where ?'a = int, no_vars]} 

1157 

1158 
\<^item> Flip a single bit: @{thm flip_bit_def [where ?'a = int, no_vars]} 

72028  1159 

1160 
\<^item> Bit concatenation: @{thm concat_bit_def [no_vars]} 

1161 

1162 
\<^item> Truncation centered towards \<^term>\<open>0::int\<close>: @{thm signed_take_bit_def [no_vars]} 

1163 

1164 
\<^item> (Bounded) conversion from and to a list of bits: @{thm horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]} 

71800  1165 
\<close> 
1166 

71442  1167 
end 