author  huffman 
Sat, 12 Nov 2011 13:01:56 +0100  
changeset 45475  b2b087c20e45 
parent 44939  5930d35c976d 
child 45529  0e1037d4e049 
permissions  rwrr 
24333  1 
(* 
2 
Author: Jeremy Dawson and Gerwin Klein, NICTA 

3 

44939
5930d35c976d
removed unused legacy lemma names, some comment cleanup.
kleing
parents:
37667
diff
changeset

4 
Definitions and basic theorems for bitwise logical operations 
24333  5 
for integers expressed using Pls, Min, BIT, 
44939
5930d35c976d
removed unused legacy lemma names, some comment cleanup.
kleing
parents:
37667
diff
changeset

6 
and converting them to and from lists of bools. 
24333  7 
*) 
8 

24350  9 
header {* Bitwise Operations on Binary Integers *} 
10 

37658  11 
theory Bit_Int 
12 
imports Bit_Representation Bit_Operations 

24333  13 
begin 
14 

37667  15 
subsection {* Recursion combinators for bitstrings *} 
16 

17 
function bin_rec :: "'a \<Rightarrow> 'a \<Rightarrow> (int \<Rightarrow> bit \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> int \<Rightarrow> 'a" where 

18 
"bin_rec f1 f2 f3 bin = (if bin = 0 then f1 

19 
else if bin =  1 then f2 

20 
else f3 (bin_rest bin) (bin_last bin) (bin_rec f1 f2 f3 (bin_rest bin)))" 

21 
by pat_completeness auto 

22 

23 
termination by (relation "measure (nat o abs o snd o snd o snd)") 

24 
(simp_all add: bin_last_def bin_rest_def) 

25 

26 
declare bin_rec.simps [simp del] 

27 

28 
lemma bin_rec_PM: 

29 
"f = bin_rec f1 f2 f3 ==> f Int.Pls = f1 & f Int.Min = f2" 

30 
by (unfold Pls_def Min_def) (simp add: bin_rec.simps) 

31 

32 
lemma bin_rec_Pls: "bin_rec f1 f2 f3 Int.Pls = f1" 

33 
by (unfold Pls_def Min_def) (simp add: bin_rec.simps) 

34 

35 
lemma bin_rec_Min: "bin_rec f1 f2 f3 Int.Min = f2" 

36 
by (unfold Pls_def Min_def) (simp add: bin_rec.simps) 

37 

38 
lemma bin_rec_Bit0: 

39 
"f3 Int.Pls (0::bit) f1 = f1 \<Longrightarrow> 

40 
bin_rec f1 f2 f3 (Int.Bit0 w) = f3 w (0::bit) (bin_rec f1 f2 f3 w)" 

41 
by (unfold Pls_def Min_def Bit0_def Bit1_def) (simp add: bin_rec.simps bin_last_def bin_rest_def) 

42 

43 
lemma bin_rec_Bit1: 

44 
"f3 Int.Min (1::bit) f2 = f2 \<Longrightarrow> 

45 
bin_rec f1 f2 f3 (Int.Bit1 w) = f3 w (1::bit) (bin_rec f1 f2 f3 w)" 

46 
apply (cases "w = Int.Min") 

47 
apply (simp add: bin_rec_Min) 

48 
apply (cases "w = Int.Pls") 

49 
apply (simp add: bin_rec_Pls number_of_is_id Pls_def [symmetric] bin_rec.simps) 

50 
apply (subst bin_rec.simps) 

51 
apply auto unfolding Pls_def Min_def Bit0_def Bit1_def number_of_is_id apply auto 

52 
done 

53 

54 
lemma bin_rec_Bit: 

55 
"f = bin_rec f1 f2 f3 ==> f3 Int.Pls (0::bit) f1 = f1 ==> 

56 
f3 Int.Min (1::bit) f2 = f2 ==> f (w BIT b) = f3 w b (f w)" 

57 
by (cases b, simp add: bin_rec_Bit0, simp add: bin_rec_Bit1) 

58 

59 
lemmas bin_rec_simps = refl [THEN bin_rec_Bit] bin_rec_Pls bin_rec_Min 

60 
bin_rec_Bit0 bin_rec_Bit1 

61 

62 

24364  63 
subsection {* Logical operations *} 
24353  64 

65 
text "bitwise logical operations on the int type" 

66 

25762  67 
instantiation int :: bit 
68 
begin 

69 

70 
definition 

37667  71 
int_not_def: "bitNOT = bin_rec ( 1) 0 
24353  72 
(\<lambda>w b s. s BIT (NOT b))" 
25762  73 

74 
definition 

37667  75 
int_and_def: "bitAND = bin_rec (\<lambda>x. 0) (\<lambda>y. y) 
24353  76 
(\<lambda>w b s y. s (bin_rest y) BIT (b AND bin_last y))" 
25762  77 

78 
definition 

37667  79 
int_or_def: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y.  1) 
24353  80 
(\<lambda>w b s y. s (bin_rest y) BIT (b OR bin_last y))" 
25762  81 

82 
definition 

37667  83 
int_xor_def: "bitXOR = bin_rec (\<lambda>x. x) bitNOT 
24353  84 
(\<lambda>w b s y. s (bin_rest y) BIT (b XOR bin_last y))" 
25762  85 

86 
instance .. 

87 

88 
end 

24353  89 

24333  90 
lemma int_not_simps [simp]: 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25762
diff
changeset

91 
"NOT Int.Pls = Int.Min" 
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25762
diff
changeset

92 
"NOT Int.Min = Int.Pls" 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

93 
"NOT (Int.Bit0 w) = Int.Bit1 (NOT w)" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

94 
"NOT (Int.Bit1 w) = Int.Bit0 (NOT w)" 
26558  95 
"NOT (w BIT b) = (NOT w) BIT (NOT b)" 
37667  96 
unfolding int_not_def Pls_def [symmetric] Min_def [symmetric] by (simp_all add: bin_rec_simps) 
24333  97 

37667  98 
lemma int_xor_Pls [simp]: 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25762
diff
changeset

99 
"Int.Pls XOR x = x" 
37667  100 
unfolding int_xor_def Pls_def [symmetric] Min_def [symmetric] by (simp add: bin_rec_PM) 
24333  101 

37667  102 
lemma int_xor_Min [simp]: 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25762
diff
changeset

103 
"Int.Min XOR x = NOT x" 
37667  104 
unfolding int_xor_def Pls_def [symmetric] Min_def [symmetric] by (simp add: bin_rec_PM) 
24333  105 

106 
lemma int_xor_Bits [simp]: 

24353  107 
"(x BIT b) XOR (y BIT c) = (x XOR y) BIT (b XOR c)" 
37667  108 
apply (unfold int_xor_def Pls_def [symmetric] Min_def [symmetric]) 
24333  109 
apply (rule bin_rec_simps (1) [THEN fun_cong, THEN trans]) 
110 
apply (rule ext, simp) 

111 
prefer 2 

112 
apply simp 

113 
apply (rule ext) 

114 
apply (simp add: int_not_simps [symmetric]) 

115 
done 

116 

37667  117 
lemma int_xor_Bits2 [simp]: 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

118 
"(Int.Bit0 x) XOR (Int.Bit0 y) = Int.Bit0 (x XOR y)" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

119 
"(Int.Bit0 x) XOR (Int.Bit1 y) = Int.Bit1 (x XOR y)" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

120 
"(Int.Bit1 x) XOR (Int.Bit0 y) = Int.Bit1 (x XOR y)" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

121 
"(Int.Bit1 x) XOR (Int.Bit1 y) = Int.Bit0 (x XOR y)" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

122 
unfolding BIT_simps [symmetric] int_xor_Bits by simp_all 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

123 

24333  124 
lemma int_xor_x_simps': 
37654  125 
"w XOR (Int.Pls BIT 0) = w" 
126 
"w XOR (Int.Min BIT 1) = NOT w" 

24333  127 
apply (induct w rule: bin_induct) 
128 
apply simp_all[4] 

129 
apply (unfold int_xor_Bits) 

130 
apply clarsimp+ 

131 
done 

132 

37667  133 
lemma int_xor_extra_simps [simp]: 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

134 
"w XOR Int.Pls = w" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

135 
"w XOR Int.Min = NOT w" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

136 
using int_xor_x_simps' by simp_all 
24333  137 

37667  138 
lemma int_or_Pls [simp]: 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25762
diff
changeset

139 
"Int.Pls OR x = x" 
24465  140 
by (unfold int_or_def) (simp add: bin_rec_PM) 
24333  141 

37667  142 
lemma int_or_Min [simp]: 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25762
diff
changeset

143 
"Int.Min OR x = Int.Min" 
37667  144 
by (unfold int_or_def Pls_def [symmetric] Min_def [symmetric]) (simp add: bin_rec_PM) 
24333  145 

146 
lemma int_or_Bits [simp]: 

24353  147 
"(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)" 
37667  148 
unfolding int_or_def Pls_def [symmetric] Min_def [symmetric] by (simp add: bin_rec_simps) 
24333  149 

37667  150 
lemma int_or_Bits2 [simp]: 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

151 
"(Int.Bit0 x) OR (Int.Bit0 y) = Int.Bit0 (x OR y)" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

152 
"(Int.Bit0 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

153 
"(Int.Bit1 x) OR (Int.Bit0 y) = Int.Bit1 (x OR y)" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

154 
"(Int.Bit1 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

155 
unfolding BIT_simps [symmetric] int_or_Bits by simp_all 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

156 

24333  157 
lemma int_or_x_simps': 
37654  158 
"w OR (Int.Pls BIT 0) = w" 
159 
"w OR (Int.Min BIT 1) = Int.Min" 

24333  160 
apply (induct w rule: bin_induct) 
161 
apply simp_all[4] 

162 
apply (unfold int_or_Bits) 

163 
apply clarsimp+ 

164 
done 

165 

37667  166 
lemma int_or_extra_simps [simp]: 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

167 
"w OR Int.Pls = w" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

168 
"w OR Int.Min = Int.Min" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

169 
using int_or_x_simps' by simp_all 
24333  170 

37667  171 
lemma int_and_Pls [simp]: 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25762
diff
changeset

172 
"Int.Pls AND x = Int.Pls" 
24465  173 
unfolding int_and_def by (simp add: bin_rec_PM) 
24333  174 

37667  175 
lemma int_and_Min [simp]: 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25762
diff
changeset

176 
"Int.Min AND x = x" 
24465  177 
unfolding int_and_def by (simp add: bin_rec_PM) 
24333  178 

179 
lemma int_and_Bits [simp]: 

24353  180 
"(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)" 
37667  181 
unfolding int_and_def Pls_def [symmetric] Min_def [symmetric] by (simp add: bin_rec_simps) 
24333  182 

37667  183 
lemma int_and_Bits2 [simp]: 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

184 
"(Int.Bit0 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

185 
"(Int.Bit0 x) AND (Int.Bit1 y) = Int.Bit0 (x AND y)" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

186 
"(Int.Bit1 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

187 
"(Int.Bit1 x) AND (Int.Bit1 y) = Int.Bit1 (x AND y)" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

188 
unfolding BIT_simps [symmetric] int_and_Bits by simp_all 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

189 

24333  190 
lemma int_and_x_simps': 
37654  191 
"w AND (Int.Pls BIT 0) = Int.Pls" 
192 
"w AND (Int.Min BIT 1) = w" 

24333  193 
apply (induct w rule: bin_induct) 
194 
apply simp_all[4] 

195 
apply (unfold int_and_Bits) 

196 
apply clarsimp+ 

197 
done 

198 

37667  199 
lemma int_and_extra_simps [simp]: 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

200 
"w AND Int.Pls = Int.Pls" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

201 
"w AND Int.Min = w" 
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

202 
using int_and_x_simps' by simp_all 
24333  203 

204 
(* commutativity of the above *) 

205 
lemma bin_ops_comm: 

206 
shows 

24353  207 
int_and_comm: "!!y::int. x AND y = y AND x" and 
208 
int_or_comm: "!!y::int. x OR y = y OR x" and 

209 
int_xor_comm: "!!y::int. x XOR y = y XOR x" 

24333  210 
apply (induct x rule: bin_induct) 
211 
apply simp_all[6] 

212 
apply (case_tac y rule: bin_exhaust, simp add: bit_ops_comm)+ 

213 
done 

214 

215 
lemma bin_ops_same [simp]: 

24353  216 
"(x::int) AND x = x" 
217 
"(x::int) OR x = x" 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25762
diff
changeset

218 
"(x::int) XOR x = Int.Pls" 
24333  219 
by (induct x rule: bin_induct) auto 
220 

24353  221 
lemma int_not_not [simp]: "NOT (NOT (x::int)) = x" 
24333  222 
by (induct x rule: bin_induct) auto 
223 

224 
lemmas bin_log_esimps = 

225 
int_and_extra_simps int_or_extra_simps int_xor_extra_simps 

226 
int_and_Pls int_and_Min int_or_Pls int_or_Min int_xor_Pls int_xor_Min 

227 

228 
(* basic properties of logical (bitwise) operations *) 

229 

230 
lemma bbw_ao_absorb: 

24353  231 
"!!y::int. x AND (y OR x) = x & x OR (y AND x) = x" 
24333  232 
apply (induct x rule: bin_induct) 
233 
apply auto 

234 
apply (case_tac [!] y rule: bin_exhaust) 

235 
apply auto 

236 
apply (case_tac [!] bit) 

237 
apply auto 

238 
done 

239 

240 
lemma bbw_ao_absorbs_other: 

24353  241 
"x AND (x OR y) = x \<and> (y AND x) OR x = (x::int)" 
242 
"(y OR x) AND x = x \<and> x OR (x AND y) = (x::int)" 

243 
"(x OR y) AND x = x \<and> (x AND y) OR x = (x::int)" 

24333  244 
apply (auto simp: bbw_ao_absorb int_or_comm) 
245 
apply (subst int_or_comm) 

246 
apply (simp add: bbw_ao_absorb) 

247 
apply (subst int_and_comm) 

248 
apply (subst int_or_comm) 

249 
apply (simp add: bbw_ao_absorb) 

250 
apply (subst int_and_comm) 

251 
apply (simp add: bbw_ao_absorb) 

252 
done 

24353  253 

24333  254 
lemmas bbw_ao_absorbs [simp] = bbw_ao_absorb bbw_ao_absorbs_other 
255 

256 
lemma int_xor_not: 

24353  257 
"!!y::int. (NOT x) XOR y = NOT (x XOR y) & 
258 
x XOR (NOT y) = NOT (x XOR y)" 

24333  259 
apply (induct x rule: bin_induct) 
260 
apply auto 

261 
apply (case_tac y rule: bin_exhaust, auto, 

262 
case_tac b, auto)+ 

263 
done 

264 

265 
lemma bbw_assocs': 

24353  266 
"!!y z::int. (x AND y) AND z = x AND (y AND z) & 
267 
(x OR y) OR z = x OR (y OR z) & 

268 
(x XOR y) XOR z = x XOR (y XOR z)" 

24333  269 
apply (induct x rule: bin_induct) 
270 
apply (auto simp: int_xor_not) 

271 
apply (case_tac [!] y rule: bin_exhaust) 

272 
apply (case_tac [!] z rule: bin_exhaust) 

273 
apply (case_tac [!] bit) 

274 
apply (case_tac [!] b) 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

275 
apply (auto simp del: BIT_simps) 
24333  276 
done 
277 

278 
lemma int_and_assoc: 

24353  279 
"(x AND y) AND (z::int) = x AND (y AND z)" 
24333  280 
by (simp add: bbw_assocs') 
281 

282 
lemma int_or_assoc: 

24353  283 
"(x OR y) OR (z::int) = x OR (y OR z)" 
24333  284 
by (simp add: bbw_assocs') 
285 

286 
lemma int_xor_assoc: 

24353  287 
"(x XOR y) XOR (z::int) = x XOR (y XOR z)" 
24333  288 
by (simp add: bbw_assocs') 
289 

290 
lemmas bbw_assocs = int_and_assoc int_or_assoc int_xor_assoc 

291 

292 
lemma bbw_lcs [simp]: 

24353  293 
"(y::int) AND (x AND z) = x AND (y AND z)" 
294 
"(y::int) OR (x OR z) = x OR (y OR z)" 

295 
"(y::int) XOR (x XOR z) = x XOR (y XOR z)" 

24333  296 
apply (auto simp: bbw_assocs [symmetric]) 
297 
apply (auto simp: bin_ops_comm) 

298 
done 

299 

300 
lemma bbw_not_dist: 

24353  301 
"!!y::int. NOT (x OR y) = (NOT x) AND (NOT y)" 
302 
"!!y::int. NOT (x AND y) = (NOT x) OR (NOT y)" 

24333  303 
apply (induct x rule: bin_induct) 
304 
apply auto 

305 
apply (case_tac [!] y rule: bin_exhaust) 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

306 
apply (case_tac [!] bit, auto simp del: BIT_simps) 
24333  307 
done 
308 

309 
lemma bbw_oa_dist: 

24353  310 
"!!y z::int. (x AND y) OR z = 
311 
(x OR z) AND (y OR z)" 

24333  312 
apply (induct x rule: bin_induct) 
313 
apply auto 

314 
apply (case_tac y rule: bin_exhaust) 

315 
apply (case_tac z rule: bin_exhaust) 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

316 
apply (case_tac ba, auto simp del: BIT_simps) 
24333  317 
done 
318 

319 
lemma bbw_ao_dist: 

24353  320 
"!!y z::int. (x OR y) AND z = 
321 
(x AND z) OR (y AND z)" 

24333  322 
apply (induct x rule: bin_induct) 
323 
apply auto 

324 
apply (case_tac y rule: bin_exhaust) 

325 
apply (case_tac z rule: bin_exhaust) 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

326 
apply (case_tac ba, auto simp del: BIT_simps) 
24333  327 
done 
328 

24367
3e29eafabe16
AC rules for bitwise logical operators no longer declared simp
huffman
parents:
24366
diff
changeset

329 
(* 
3e29eafabe16
AC rules for bitwise logical operators no longer declared simp
huffman
parents:
24366
diff
changeset

330 
Why were these declared simp??? 
24333  331 
declare bin_ops_comm [simp] bbw_assocs [simp] 
24367
3e29eafabe16
AC rules for bitwise logical operators no longer declared simp
huffman
parents:
24366
diff
changeset

332 
*) 
24333  333 

334 
lemma plus_and_or [rule_format]: 

24353  335 
"ALL y::int. (x AND y) + (x OR y) = x + y" 
24333  336 
apply (induct x rule: bin_induct) 
337 
apply clarsimp 

338 
apply clarsimp 

339 
apply clarsimp 

340 
apply (case_tac y rule: bin_exhaust) 

341 
apply clarsimp 

342 
apply (unfold Bit_def) 

343 
apply clarsimp 

344 
apply (erule_tac x = "x" in allE) 

37667  345 
apply (simp add: bitval_def split: bit.split) 
24333  346 
done 
347 

348 
lemma le_int_or: 

37667  349 
"bin_sign (y::int) = Int.Pls ==> x <= x OR y" 
350 
apply (induct y arbitrary: x rule: bin_induct) 

24333  351 
apply clarsimp 
352 
apply clarsimp 

353 
apply (case_tac x rule: bin_exhaust) 

354 
apply (case_tac b) 

355 
apply (case_tac [!] bit) 

26514  356 
apply (auto simp: less_eq_int_code) 
24333  357 
done 
358 

359 
lemmas int_and_le = 

45475  360 
xtr3 [OF bbw_ao_absorbs (2) [THEN conjunct2, symmetric] le_int_or] 
24333  361 

24364  362 
lemma bin_nth_ops: 
363 
"!!x y. bin_nth (x AND y) n = (bin_nth x n & bin_nth y n)" 

364 
"!!x y. bin_nth (x OR y) n = (bin_nth x n  bin_nth y n)" 

365 
"!!x y. bin_nth (x XOR y) n = (bin_nth x n ~= bin_nth y n)" 

366 
"!!x. bin_nth (NOT x) n = (~ bin_nth x n)" 

367 
apply (induct n) 

368 
apply safe 

369 
apply (case_tac [!] x rule: bin_exhaust) 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

370 
apply (simp_all del: BIT_simps) 
24364  371 
apply (case_tac [!] y rule: bin_exhaust) 
26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

372 
apply (simp_all del: BIT_simps) 
24364  373 
apply (auto dest: not_B1_is_B0 intro: B1_ass_B0) 
374 
done 

375 

376 
(* interaction between bitwise and arithmetic *) 

377 
(* good example of bin_induction *) 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25762
diff
changeset

378 
lemma bin_add_not: "x + NOT x = Int.Min" 
24364  379 
apply (induct x rule: bin_induct) 
380 
apply clarsimp 

381 
apply clarsimp 

382 
apply (case_tac bit, auto) 

383 
done 

384 

385 
(* truncating results of bitwise operations *) 

386 
lemma bin_trunc_ao: 

387 
"!!x y. (bintrunc n x) AND (bintrunc n y) = bintrunc n (x AND y)" 

388 
"!!x y. (bintrunc n x) OR (bintrunc n y) = bintrunc n (x OR y)" 

389 
apply (induct n) 

390 
apply auto 

391 
apply (case_tac [!] x rule: bin_exhaust) 

392 
apply (case_tac [!] y rule: bin_exhaust) 

393 
apply auto 

394 
done 

395 

396 
lemma bin_trunc_xor: 

397 
"!!x y. bintrunc n (bintrunc n x XOR bintrunc n y) = 

398 
bintrunc n (x XOR y)" 

399 
apply (induct n) 

400 
apply auto 

401 
apply (case_tac [!] x rule: bin_exhaust) 

402 
apply (case_tac [!] y rule: bin_exhaust) 

403 
apply auto 

404 
done 

405 

406 
lemma bin_trunc_not: 

407 
"!!x. bintrunc n (NOT (bintrunc n x)) = bintrunc n (NOT x)" 

408 
apply (induct n) 

409 
apply auto 

410 
apply (case_tac [!] x rule: bin_exhaust) 

411 
apply auto 

412 
done 

413 

414 
(* want theorems of the form of bin_trunc_xor *) 

415 
lemma bintr_bintr_i: 

416 
"x = bintrunc n y ==> bintrunc n x = bintrunc n y" 

417 
by auto 

418 

419 
lemmas bin_trunc_and = bin_trunc_ao(1) [THEN bintr_bintr_i] 

420 
lemmas bin_trunc_or = bin_trunc_ao(2) [THEN bintr_bintr_i] 

421 

422 
subsection {* Setting and clearing bits *} 

423 

26558  424 
primrec 
24364  425 
bin_sc :: "nat => bit => int => int" 
26558  426 
where 
427 
Z: "bin_sc 0 b w = bin_rest w BIT b" 

428 
 Suc: "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w" 

24364  429 

24333  430 
(** nth bit, set/clear **) 
431 

432 
lemma bin_nth_sc [simp]: 

37654  433 
"!!w. bin_nth (bin_sc n b w) n = (b = 1)" 
24333  434 
by (induct n) auto 
435 

436 
lemma bin_sc_sc_same [simp]: 

437 
"!!w. bin_sc n c (bin_sc n b w) = bin_sc n c w" 

438 
by (induct n) auto 

439 

440 
lemma bin_sc_sc_diff: 

441 
"!!w m. m ~= n ==> 

442 
bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)" 

443 
apply (induct n) 

444 
apply (case_tac [!] m) 

445 
apply auto 

446 
done 

447 

448 
lemma bin_nth_sc_gen: 

37654  449 
"!!w m. bin_nth (bin_sc n b w) m = (if m = n then b = 1 else bin_nth w m)" 
24333  450 
by (induct n) (case_tac [!] m, auto) 
451 

452 
lemma bin_sc_nth [simp]: 

37654  453 
"!!w. (bin_sc n (If (bin_nth w n) 1 0) w) = w" 
24465  454 
by (induct n) auto 
24333  455 

456 
lemma bin_sign_sc [simp]: 

457 
"!!w. bin_sign (bin_sc n b w) = bin_sign w" 

458 
by (induct n) auto 

459 

460 
lemma bin_sc_bintr [simp]: 

461 
"!!w m. bintrunc m (bin_sc n x (bintrunc m (w))) = bintrunc m (bin_sc n x w)" 

462 
apply (induct n) 

463 
apply (case_tac [!] w rule: bin_exhaust) 

464 
apply (case_tac [!] m, auto) 

465 
done 

466 

467 
lemma bin_clr_le: 

37654  468 
"!!w. bin_sc n 0 w <= w" 
24333  469 
apply (induct n) 
470 
apply (case_tac [!] w rule: bin_exhaust) 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

471 
apply (auto simp del: BIT_simps) 
24333  472 
apply (unfold Bit_def) 
37667  473 
apply (simp_all add: bitval_def split: bit.split) 
24333  474 
done 
475 

476 
lemma bin_set_ge: 

37654  477 
"!!w. bin_sc n 1 w >= w" 
24333  478 
apply (induct n) 
479 
apply (case_tac [!] w rule: bin_exhaust) 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

480 
apply (auto simp del: BIT_simps) 
24333  481 
apply (unfold Bit_def) 
37667  482 
apply (simp_all add: bitval_def split: bit.split) 
24333  483 
done 
484 

485 
lemma bintr_bin_clr_le: 

37654  486 
"!!w m. bintrunc n (bin_sc m 0 w) <= bintrunc n w" 
24333  487 
apply (induct n) 
488 
apply simp 

489 
apply (case_tac w rule: bin_exhaust) 

490 
apply (case_tac m) 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

491 
apply (auto simp del: BIT_simps) 
24333  492 
apply (unfold Bit_def) 
37667  493 
apply (simp_all add: bitval_def split: bit.split) 
24333  494 
done 
495 

496 
lemma bintr_bin_set_ge: 

37654  497 
"!!w m. bintrunc n (bin_sc m 1 w) >= bintrunc n w" 
24333  498 
apply (induct n) 
499 
apply simp 

500 
apply (case_tac w rule: bin_exhaust) 

501 
apply (case_tac m) 

26086
3c243098b64a
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents:
25919
diff
changeset

502 
apply (auto simp del: BIT_simps) 
24333  503 
apply (unfold Bit_def) 
37667  504 
apply (simp_all add: bitval_def split: bit.split) 
24333  505 
done 
506 

37654  507 
lemma bin_sc_FP [simp]: "bin_sc n 0 Int.Pls = Int.Pls" 
24333  508 
by (induct n) auto 
509 

37654  510 
lemma bin_sc_TM [simp]: "bin_sc n 1 Int.Min = Int.Min" 
24333  511 
by (induct n) auto 
512 

513 
lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP 

514 

515 
lemma bin_sc_minus: 

516 
"0 < n ==> bin_sc (Suc (n  1)) b w = bin_sc n b w" 

517 
by auto 

518 

519 
lemmas bin_sc_Suc_minus = 

520 
trans [OF bin_sc_minus [symmetric] bin_sc.Suc, standard] 

521 

522 
lemmas bin_sc_Suc_pred [simp] = 

523 
bin_sc_Suc_minus [of "number_of bin", simplified nobm1, standard] 

524 

24465  525 

24364  526 
subsection {* Splitting and concatenation *} 
24333  527 

26558  528 
definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int" where 
529 
"bin_rcat n = foldl (%u v. bin_cat u n v) Int.Pls" 

530 

37667  531 
lemma [code]: 
532 
"bin_rcat n = foldl (\<lambda>u v. bin_cat u n v) 0" 

533 
by (simp add: bin_rcat_def Pls_def) 

534 

28042  535 
fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where 
26558  536 
"bin_rsplit_aux n m c bs = 
24364  537 
(if m = 0  n = 0 then bs else 
538 
let (a, b) = bin_split n c 

26558  539 
in bin_rsplit_aux n (m  n) a (b # bs))" 
24364  540 

26558  541 
definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where 
542 
"bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []" 

543 

28042  544 
fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where 
26558  545 
"bin_rsplitl_aux n m c bs = 
24364  546 
(if m = 0  n = 0 then bs else 
547 
let (a, b) = bin_split (min m n) c 

26558  548 
in bin_rsplitl_aux n (m  n) a (b # bs))" 
24364  549 

26558  550 
definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where 
551 
"bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []" 

552 

24364  553 
declare bin_rsplit_aux.simps [simp del] 
554 
declare bin_rsplitl_aux.simps [simp del] 

555 

556 
lemma bin_sign_cat: 

557 
"!!y. bin_sign (bin_cat x n y) = bin_sign x" 

558 
by (induct n) auto 

559 

560 
lemma bin_cat_Suc_Bit: 

561 
"bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b" 

562 
by auto 

563 

564 
lemma bin_nth_cat: 

565 
"!!n y. bin_nth (bin_cat x k y) n = 

566 
(if n < k then bin_nth y n else bin_nth x (n  k))" 

567 
apply (induct k) 

568 
apply clarsimp 

569 
apply (case_tac n, auto) 

24333  570 
done 
571 

24364  572 
lemma bin_nth_split: 
573 
"!!b c. bin_split n c = (a, b) ==> 

574 
(ALL k. bin_nth a k = bin_nth c (n + k)) & 

575 
(ALL k. bin_nth b k = (k < n & bin_nth c k))" 

24333  576 
apply (induct n) 
24364  577 
apply clarsimp 
578 
apply (clarsimp simp: Let_def split: ls_splits) 

579 
apply (case_tac k) 

580 
apply auto 

581 
done 

582 

583 
lemma bin_cat_assoc: 

584 
"!!z. bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)" 

585 
by (induct n) auto 

586 

587 
lemma bin_cat_assoc_sym: "!!z m. 

588 
bin_cat x m (bin_cat y n z) = bin_cat (bin_cat x (m  n) y) (min m n) z" 

589 
apply (induct n, clarsimp) 

590 
apply (case_tac m, auto) 

24333  591 
done 
592 

24364  593 
lemma bin_cat_Pls [simp]: 
25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25762
diff
changeset

594 
"!!w. bin_cat Int.Pls n w = bintrunc n w" 
24364  595 
by (induct n) auto 
596 

597 
lemma bintr_cat1: 

598 
"!!b. bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b" 

599 
by (induct n) auto 

600 

601 
lemma bintr_cat: "bintrunc m (bin_cat a n b) = 

602 
bin_cat (bintrunc (m  n) a) n (bintrunc (min m n) b)" 

603 
by (rule bin_eqI) (auto simp: bin_nth_cat nth_bintr) 

604 

605 
lemma bintr_cat_same [simp]: 

606 
"bintrunc n (bin_cat a n b) = bintrunc n b" 

607 
by (auto simp add : bintr_cat) 

608 

609 
lemma cat_bintr [simp]: 

610 
"!!b. bin_cat a n (bintrunc n b) = bin_cat a n b" 

611 
by (induct n) auto 

612 

613 
lemma split_bintrunc: 

614 
"!!b c. bin_split n c = (a, b) ==> b = bintrunc n c" 

615 
by (induct n) (auto simp: Let_def split: ls_splits) 

616 

617 
lemma bin_cat_split: 

618 
"!!v w. bin_split n w = (u, v) ==> w = bin_cat u n v" 

619 
by (induct n) (auto simp: Let_def split: ls_splits) 

620 

621 
lemma bin_split_cat: 

622 
"!!w. bin_split n (bin_cat v n w) = (v, bintrunc n w)" 

623 
by (induct n) auto 

624 

625 
lemma bin_split_Pls [simp]: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25762
diff
changeset

626 
"bin_split n Int.Pls = (Int.Pls, Int.Pls)" 
24364  627 
by (induct n) (auto simp: Let_def split: ls_splits) 
628 

629 
lemma bin_split_Min [simp]: 

25919
8b1c0d434824
joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents:
25762
diff
changeset

630 
"bin_split n Int.Min = (Int.Min, bintrunc n Int.Min)" 
24364  631 
by (induct n) (auto simp: Let_def split: ls_splits) 
632 

633 
lemma bin_split_trunc: 

634 
"!!m b c. bin_split (min m n) c = (a, b) ==> 

635 
bin_split n (bintrunc m c) = (bintrunc (m  n) a, b)" 

636 
apply (induct n, clarsimp) 

637 
apply (simp add: bin_rest_trunc Let_def split: ls_splits) 

638 
apply (case_tac m) 

639 
apply (auto simp: Let_def split: ls_splits) 

24333  640 
done 
641 

24364  642 
lemma bin_split_trunc1: 
643 
"!!m b c. bin_split n c = (a, b) ==> 

644 
bin_split n (bintrunc m c) = (bintrunc (m  n) a, bintrunc m b)" 

645 
apply (induct n, clarsimp) 

646 
apply (simp add: bin_rest_trunc Let_def split: ls_splits) 

647 
apply (case_tac m) 

648 
apply (auto simp: Let_def split: ls_splits) 

649 
done 

24333  650 

24364  651 
lemma bin_cat_num: 
652 
"!!b. bin_cat a n b = a * 2 ^ n + bintrunc n b" 

653 
apply (induct n, clarsimp) 

654 
apply (simp add: Bit_def cong: number_of_False_cong) 

655 
done 

656 

657 
lemma bin_split_num: 

658 
"!!b. bin_split n b = (b div 2 ^ n, b mod 2 ^ n)" 

659 
apply (induct n, clarsimp) 

660 
apply (simp add: bin_rest_div zdiv_zmult2_eq) 

661 
apply (case_tac b rule: bin_exhaust) 

662 
apply simp 

37667  663 
apply (simp add: Bit_def mod_mult_mult1 p1mod22k bitval_def 
24364  664 
split: bit.split 
665 
cong: number_of_False_cong) 

666 
done 

667 

668 
subsection {* Miscellaneous lemmas *} 

24333  669 

670 
lemma nth_2p_bin: 

671 
"!!m. bin_nth (2 ^ n) m = (m = n)" 

672 
apply (induct n) 

673 
apply clarsimp 

674 
apply safe 

675 
apply (case_tac m) 

676 
apply (auto simp: trans [OF numeral_1_eq_1 [symmetric] number_of_eq]) 

677 
apply (case_tac m) 

678 
apply (auto simp: Bit_B0_2t [symmetric]) 

679 
done 

680 

681 
(* for use when simplifying with bin_nth_Bit *) 

682 

683 
lemma ex_eq_or: 

684 
"(EX m. n = Suc m & (m = k  P m)) = (n = Suc k  (EX m. n = Suc m & P m))" 

685 
by auto 

686 

687 
end 

688 