author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 48891  c0eafbd55de3 
child 58022  464c1815fde9 
permissions  rwrr 
23146  1 
(* Title: ZF/Bin.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

3 
Copyright 1994 University of Cambridge 

4 

5 
The sign Pls stands for an infinite string of leading 0's. 

6 
The sign Min stands for an infinite string of leading 1's. 

7 

8 
A number can have multiple representations, namely leading 0's with sign 

9 
Pls and leading 1's with sign Min. See twoscompl.ML/int_of_binary for 

10 
the numerical interpretation. 

11 

12 
The representation expects that (m mod 2) is 0 or 1, even if m is negative; 

13 
For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1 

14 
*) 

15 

16 
header{*Arithmetic on Binary Integers*} 

17 

18 
theory Bin 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
24893
diff
changeset

19 
imports Int_ZF Datatype_ZF 
23146  20 
begin 
21 

22 
consts bin :: i 

23 
datatype 

24 
"bin" = Pls 

25 
 Min 

46953  26 
 Bit ("w \<in> bin", "b \<in> bool") (infixl "BIT" 90) 
23146  27 

28 
consts 

29 
integ_of :: "i=>i" 

30 
NCons :: "[i,i]=>i" 

31 
bin_succ :: "i=>i" 

32 
bin_pred :: "i=>i" 

33 
bin_minus :: "i=>i" 

34 
bin_adder :: "i=>i" 

35 
bin_mult :: "[i,i]=>i" 

36 

37 
primrec 

38 
integ_of_Pls: "integ_of (Pls) = $# 0" 

39 
integ_of_Min: "integ_of (Min) = $($#1)" 

40 
integ_of_BIT: "integ_of (w BIT b) = $#b $+ integ_of(w) $+ integ_of(w)" 

41 

42 
(** recall that cond(1,b,c)=b and cond(0,b,c)=0 **) 

43 

44 
primrec (*NCons adds a bit, suppressing leading 0s and 1s*) 

45 
NCons_Pls: "NCons (Pls,b) = cond(b,Pls BIT b,Pls)" 

46 
NCons_Min: "NCons (Min,b) = cond(b,Min,Min BIT b)" 

47 
NCons_BIT: "NCons (w BIT c,b) = w BIT c BIT b" 

48 

49 
primrec (*successor. If a BIT, can change a 0 to a 1 without recursion.*) 

50 
bin_succ_Pls: "bin_succ (Pls) = Pls BIT 1" 

51 
bin_succ_Min: "bin_succ (Min) = Pls" 

52 
bin_succ_BIT: "bin_succ (w BIT b) = cond(b, bin_succ(w) BIT 0, NCons(w,1))" 

53 

54 
primrec (*predecessor*) 

55 
bin_pred_Pls: "bin_pred (Pls) = Min" 

56 
bin_pred_Min: "bin_pred (Min) = Min BIT 0" 

57 
bin_pred_BIT: "bin_pred (w BIT b) = cond(b, NCons(w,0), bin_pred(w) BIT 1)" 

58 

59 
primrec (*unary negation*) 

60 
bin_minus_Pls: 

61 
"bin_minus (Pls) = Pls" 

62 
bin_minus_Min: 

63 
"bin_minus (Min) = Pls BIT 1" 

64 
bin_minus_BIT: 

65 
"bin_minus (w BIT b) = cond(b, bin_pred(NCons(bin_minus(w),0)), 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26190
diff
changeset

66 
bin_minus(w) BIT 0)" 
23146  67 

68 
primrec (*sum*) 

69 
bin_adder_Pls: 

46820  70 
"bin_adder (Pls) = (\<lambda>w\<in>bin. w)" 
23146  71 
bin_adder_Min: 
46820  72 
"bin_adder (Min) = (\<lambda>w\<in>bin. bin_pred(w))" 
23146  73 
bin_adder_BIT: 
46820  74 
"bin_adder (v BIT x) = 
75 
(\<lambda>w\<in>bin. 

76 
bin_case (v BIT x, bin_pred(v BIT x), 

77 
%w y. NCons(bin_adder (v) ` cond(x and y, bin_succ(w), w), 

23146  78 
x xor y), 
79 
w))" 

80 

81 
(*The bin_case above replaces the following mutually recursive function: 

82 
primrec 

83 
"adding (v,x,Pls) = v BIT x" 

84 
"adding (v,x,Min) = bin_pred(v BIT x)" 

46820  85 
"adding (v,x,w BIT y) = NCons(bin_adder (v, cond(x and y, bin_succ(w), w)), 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26190
diff
changeset

86 
x xor y)" 
23146  87 
*) 
88 

24893  89 
definition 
90 
bin_add :: "[i,i]=>i" where 

23146  91 
"bin_add(v,w) == bin_adder(v)`w" 
92 

93 

94 
primrec 

95 
bin_mult_Pls: 

96 
"bin_mult (Pls,w) = Pls" 

97 
bin_mult_Min: 

98 
"bin_mult (Min,w) = bin_minus(w)" 

99 
bin_mult_BIT: 

100 
"bin_mult (v BIT b,w) = cond(b, bin_add(NCons(bin_mult(v,w),0),w), 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26190
diff
changeset

101 
NCons(bin_mult(v,w),0))" 
23146  102 

35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset

103 
syntax 
45703
c7a13ce60161
renamed inner syntax categories "num" to "num_token" and "xnum" to "xnum_token";
wenzelm
parents:
35123
diff
changeset

104 
"_Int" :: "xnum_token => i" ("_") 
35112
ff6f60e6ab85
numeral syntax: clarify parse trees vs. actual terms;
wenzelm
parents:
32960
diff
changeset

105 

48891  106 
ML_file "Tools/numeral_syntax.ML" 
35123  107 
setup Numeral_Syntax.setup 
23146  108 

109 

110 
declare bin.intros [simp,TC] 

111 

112 
lemma NCons_Pls_0: "NCons(Pls,0) = Pls" 

113 
by simp 

114 

115 
lemma NCons_Pls_1: "NCons(Pls,1) = Pls BIT 1" 

116 
by simp 

117 

118 
lemma NCons_Min_0: "NCons(Min,0) = Min BIT 0" 

119 
by simp 

120 

121 
lemma NCons_Min_1: "NCons(Min,1) = Min" 

122 
by simp 

123 

124 
lemma NCons_BIT: "NCons(w BIT x,b) = w BIT x BIT b" 

125 
by (simp add: bin.case_eqns) 

126 

46820  127 
lemmas NCons_simps [simp] = 
23146  128 
NCons_Pls_0 NCons_Pls_1 NCons_Min_0 NCons_Min_1 NCons_BIT 
129 

130 

131 

132 
(** Type checking **) 

133 

46953  134 
lemma integ_of_type [TC]: "w \<in> bin ==> integ_of(w) \<in> int" 
23146  135 
apply (induct_tac "w") 
136 
apply (simp_all add: bool_into_nat) 

137 
done 

138 

46953  139 
lemma NCons_type [TC]: "[ w \<in> bin; b \<in> bool ] ==> NCons(w,b) \<in> bin" 
23146  140 
by (induct_tac "w", auto) 
141 

46953  142 
lemma bin_succ_type [TC]: "w \<in> bin ==> bin_succ(w) \<in> bin" 
23146  143 
by (induct_tac "w", auto) 
144 

46953  145 
lemma bin_pred_type [TC]: "w \<in> bin ==> bin_pred(w) \<in> bin" 
23146  146 
by (induct_tac "w", auto) 
147 

46953  148 
lemma bin_minus_type [TC]: "w \<in> bin ==> bin_minus(w) \<in> bin" 
23146  149 
by (induct_tac "w", auto) 
150 

151 
(*This proof is complicated by the mutual recursion*) 

152 
lemma bin_add_type [rule_format,TC]: 

46953  153 
"v \<in> bin ==> \<forall>w\<in>bin. bin_add(v,w) \<in> bin" 
23146  154 
apply (unfold bin_add_def) 
155 
apply (induct_tac "v") 

156 
apply (rule_tac [3] ballI) 

157 
apply (rename_tac [3] "w'") 

158 
apply (induct_tac [3] "w'") 

159 
apply (simp_all add: NCons_type) 

160 
done 

161 

46953  162 
lemma bin_mult_type [TC]: "[ v \<in> bin; w \<in> bin ] ==> bin_mult(v,w) \<in> bin" 
23146  163 
by (induct_tac "v", auto) 
164 

165 

46820  166 
subsubsection{*The Carry and Borrow Functions, 
23146  167 
@{term bin_succ} and @{term bin_pred}*} 
168 

169 
(*NCons preserves the integer value of its argument*) 

170 
lemma integ_of_NCons [simp]: 

46953  171 
"[ w \<in> bin; b \<in> bool ] ==> integ_of(NCons(w,b)) = integ_of(w BIT b)" 
23146  172 
apply (erule bin.cases) 
46820  173 
apply (auto elim!: boolE) 
23146  174 
done 
175 

176 
lemma integ_of_succ [simp]: 

46953  177 
"w \<in> bin ==> integ_of(bin_succ(w)) = $#1 $+ integ_of(w)" 
23146  178 
apply (erule bin.induct) 
46820  179 
apply (auto simp add: zadd_ac elim!: boolE) 
23146  180 
done 
181 

182 
lemma integ_of_pred [simp]: 

46953  183 
"w \<in> bin ==> integ_of(bin_pred(w)) = $ ($#1) $+ integ_of(w)" 
23146  184 
apply (erule bin.induct) 
46820  185 
apply (auto simp add: zadd_ac elim!: boolE) 
23146  186 
done 
187 

188 

189 
subsubsection{*@{term bin_minus}: Unary Negation of Binary Integers*} 

190 

46953  191 
lemma integ_of_minus: "w \<in> bin ==> integ_of(bin_minus(w)) = $ integ_of(w)" 
23146  192 
apply (erule bin.induct) 
46820  193 
apply (auto simp add: zadd_ac zminus_zadd_distrib elim!: boolE) 
23146  194 
done 
195 

196 

197 
subsubsection{*@{term bin_add}: Binary Addition*} 

198 

46953  199 
lemma bin_add_Pls [simp]: "w \<in> bin ==> bin_add(Pls,w) = w" 
23146  200 
by (unfold bin_add_def, simp) 
201 

46953  202 
lemma bin_add_Pls_right: "w \<in> bin ==> bin_add(w,Pls) = w" 
23146  203 
apply (unfold bin_add_def) 
204 
apply (erule bin.induct, auto) 

205 
done 

206 

46953  207 
lemma bin_add_Min [simp]: "w \<in> bin ==> bin_add(Min,w) = bin_pred(w)" 
23146  208 
by (unfold bin_add_def, simp) 
209 

46953  210 
lemma bin_add_Min_right: "w \<in> bin ==> bin_add(w,Min) = bin_pred(w)" 
23146  211 
apply (unfold bin_add_def) 
212 
apply (erule bin.induct, auto) 

213 
done 

214 

215 
lemma bin_add_BIT_Pls [simp]: "bin_add(v BIT x,Pls) = v BIT x" 

216 
by (unfold bin_add_def, simp) 

217 

218 
lemma bin_add_BIT_Min [simp]: "bin_add(v BIT x,Min) = bin_pred(v BIT x)" 

219 
by (unfold bin_add_def, simp) 

220 

221 
lemma bin_add_BIT_BIT [simp]: 

46953  222 
"[ w \<in> bin; y \<in> bool ] 
46820  223 
==> bin_add(v BIT x, w BIT y) = 
23146  224 
NCons(bin_add(v, cond(x and y, bin_succ(w), w)), x xor y)" 
225 
by (unfold bin_add_def, simp) 

226 

227 
lemma integ_of_add [rule_format]: 

46953  228 
"v \<in> bin ==> 
46820  229 
\<forall>w\<in>bin. integ_of(bin_add(v,w)) = integ_of(v) $+ integ_of(w)" 
23146  230 
apply (erule bin.induct, simp, simp) 
231 
apply (rule ballI) 

232 
apply (induct_tac "wa") 

46820  233 
apply (auto simp add: zadd_ac elim!: boolE) 
23146  234 
done 
235 

236 
(*Subtraction*) 

46820  237 
lemma diff_integ_of_eq: 
46953  238 
"[ v \<in> bin; w \<in> bin ] 
23146  239 
==> integ_of(v) $ integ_of(w) = integ_of(bin_add (v, bin_minus(w)))" 
240 
apply (unfold zdiff_def) 

241 
apply (simp add: integ_of_add integ_of_minus) 

242 
done 

243 

244 

245 
subsubsection{*@{term bin_mult}: Binary Multiplication*} 

246 

247 
lemma integ_of_mult: 

46953  248 
"[ v \<in> bin; w \<in> bin ] 
23146  249 
==> integ_of(bin_mult(v,w)) = integ_of(v) $* integ_of(w)" 
250 
apply (induct_tac "v", simp) 

251 
apply (simp add: integ_of_minus) 

46820  252 
apply (auto simp add: zadd_ac integ_of_add zadd_zmult_distrib elim!: boolE) 
23146  253 
done 
254 

255 

256 
subsection{*Computations*} 

257 

258 
(** extra rules for bin_succ, bin_pred **) 

259 

260 
lemma bin_succ_1: "bin_succ(w BIT 1) = bin_succ(w) BIT 0" 

261 
by simp 

262 

263 
lemma bin_succ_0: "bin_succ(w BIT 0) = NCons(w,1)" 

264 
by simp 

265 

266 
lemma bin_pred_1: "bin_pred(w BIT 1) = NCons(w,0)" 

267 
by simp 

268 

269 
lemma bin_pred_0: "bin_pred(w BIT 0) = bin_pred(w) BIT 1" 

270 
by simp 

271 

272 
(** extra rules for bin_minus **) 

273 

274 
lemma bin_minus_1: "bin_minus(w BIT 1) = bin_pred(NCons(bin_minus(w), 0))" 

275 
by simp 

276 

277 
lemma bin_minus_0: "bin_minus(w BIT 0) = bin_minus(w) BIT 0" 

278 
by simp 

279 

280 
(** extra rules for bin_add **) 

281 

46953  282 
lemma bin_add_BIT_11: "w \<in> bin ==> bin_add(v BIT 1, w BIT 1) = 
23146  283 
NCons(bin_add(v, bin_succ(w)), 0)" 
284 
by simp 

285 

46953  286 
lemma bin_add_BIT_10: "w \<in> bin ==> bin_add(v BIT 1, w BIT 0) = 
23146  287 
NCons(bin_add(v,w), 1)" 
288 
by simp 

289 

46953  290 
lemma bin_add_BIT_0: "[ w \<in> bin; y \<in> bool ] 
23146  291 
==> bin_add(v BIT 0, w BIT y) = NCons(bin_add(v,w), y)" 
292 
by simp 

293 

294 
(** extra rules for bin_mult **) 

295 

296 
lemma bin_mult_1: "bin_mult(v BIT 1, w) = bin_add(NCons(bin_mult(v,w),0), w)" 

297 
by simp 

298 

299 
lemma bin_mult_0: "bin_mult(v BIT 0, w) = NCons(bin_mult(v,w),0)" 

300 
by simp 

301 

302 

303 
(** Simplification rules with integer constants **) 

304 

305 
lemma int_of_0: "$#0 = #0" 

306 
by simp 

307 

308 
lemma int_of_succ: "$# succ(n) = #1 $+ $#n" 

309 
by (simp add: int_of_add [symmetric] natify_succ) 

310 

311 
lemma zminus_0 [simp]: "$ #0 = #0" 

312 
by simp 

313 

314 
lemma zadd_0_intify [simp]: "#0 $+ z = intify(z)" 

315 
by simp 

316 

317 
lemma zadd_0_right_intify [simp]: "z $+ #0 = intify(z)" 

318 
by simp 

319 

320 
lemma zmult_1_intify [simp]: "#1 $* z = intify(z)" 

321 
by simp 

322 

323 
lemma zmult_1_right_intify [simp]: "z $* #1 = intify(z)" 

324 
by (subst zmult_commute, simp) 

325 

326 
lemma zmult_0 [simp]: "#0 $* z = #0" 

327 
by simp 

328 

329 
lemma zmult_0_right [simp]: "z $* #0 = #0" 

330 
by (subst zmult_commute, simp) 

331 

332 
lemma zmult_minus1 [simp]: "#1 $* z = $z" 

333 
by (simp add: zcompare_rls) 

334 

335 
lemma zmult_minus1_right [simp]: "z $* #1 = $z" 

336 
apply (subst zmult_commute) 

337 
apply (rule zmult_minus1) 

338 
done 

339 

340 

341 
subsection{*Simplification Rules for Comparison of Binary Numbers*} 

342 
text{*Thanks to Norbert Voelker*} 

343 

344 
(** Equals (=) **) 

345 

46820  346 
lemma eq_integ_of_eq: 
46953  347 
"[ v \<in> bin; w \<in> bin ] 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

348 
==> ((integ_of(v)) = integ_of(w)) \<longleftrightarrow> 
23146  349 
iszero (integ_of (bin_add (v, bin_minus(w))))" 
350 
apply (unfold iszero_def) 

351 
apply (simp add: zcompare_rls integ_of_add integ_of_minus) 

352 
done 

353 

354 
lemma iszero_integ_of_Pls: "iszero (integ_of(Pls))" 

355 
by (unfold iszero_def, simp) 

356 

357 

358 
lemma nonzero_integ_of_Min: "~ iszero (integ_of(Min))" 

359 
apply (unfold iszero_def) 

360 
apply (simp add: zminus_equation) 

361 
done 

362 

46820  363 
lemma iszero_integ_of_BIT: 
46953  364 
"[ w \<in> bin; x \<in> bool ] 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

365 
==> iszero (integ_of (w BIT x)) \<longleftrightarrow> (x=0 & iszero (integ_of(w)))" 
23146  366 
apply (unfold iszero_def, simp) 
46820  367 
apply (subgoal_tac "integ_of (w) \<in> int") 
23146  368 
apply typecheck 
369 
apply (drule int_cases) 

370 
apply (safe elim!: boolE) 

371 
apply (simp_all (asm_lr) add: zcompare_rls zminus_zadd_distrib [symmetric] 

372 
int_of_add [symmetric]) 

373 
done 

374 

375 
lemma iszero_integ_of_0: 

46953  376 
"w \<in> bin ==> iszero (integ_of (w BIT 0)) \<longleftrightarrow> iszero (integ_of(w))" 
46820  377 
by (simp only: iszero_integ_of_BIT, blast) 
23146  378 

46953  379 
lemma iszero_integ_of_1: "w \<in> bin ==> ~ iszero (integ_of (w BIT 1))" 
23146  380 
by (simp only: iszero_integ_of_BIT, blast) 
381 

382 

383 

384 
(** Lessthan (<) **) 

385 

46820  386 
lemma less_integ_of_eq_neg: 
46953  387 
"[ v \<in> bin; w \<in> bin ] 
46820  388 
==> integ_of(v) $< integ_of(w) 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

389 
\<longleftrightarrow> znegative (integ_of (bin_add (v, bin_minus(w))))" 
23146  390 
apply (unfold zless_def zdiff_def) 
391 
apply (simp add: integ_of_minus integ_of_add) 

392 
done 

393 

394 
lemma not_neg_integ_of_Pls: "~ znegative (integ_of(Pls))" 

395 
by simp 

396 

397 
lemma neg_integ_of_Min: "znegative (integ_of(Min))" 

398 
by simp 

399 

400 
lemma neg_integ_of_BIT: 

46953  401 
"[ w \<in> bin; x \<in> bool ] 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

402 
==> znegative (integ_of (w BIT x)) \<longleftrightarrow> znegative (integ_of(w))" 
23146  403 
apply simp 
46820  404 
apply (subgoal_tac "integ_of (w) \<in> int") 
23146  405 
apply typecheck 
406 
apply (drule int_cases) 

407 
apply (auto elim!: boolE simp add: int_of_add [symmetric] zcompare_rls) 

46820  408 
apply (simp_all add: zminus_zadd_distrib [symmetric] zdiff_def 
23146  409 
int_of_add [symmetric]) 
410 
apply (subgoal_tac "$#1 $ $# succ (succ (n #+ n)) = $ $# succ (n #+ n) ") 

411 
apply (simp add: zdiff_def) 

412 
apply (simp add: equation_zminus int_of_diff [symmetric]) 

413 
done 

414 

415 
(** Lessthanorequals (<=) **) 

416 

417 
lemma le_integ_of_eq_not_less: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

418 
"(integ_of(x) $<= (integ_of(w))) \<longleftrightarrow> ~ (integ_of(w) $< (integ_of(x)))" 
23146  419 
by (simp add: not_zless_iff_zle [THEN iff_sym]) 
420 

421 

422 
(*Delete the original rewrites, with their clumsy conditional expressions*) 

46820  423 
declare bin_succ_BIT [simp del] 
424 
bin_pred_BIT [simp del] 

23146  425 
bin_minus_BIT [simp del] 
426 
NCons_Pls [simp del] 

427 
NCons_Min [simp del] 

428 
bin_adder_BIT [simp del] 

429 
bin_mult_BIT [simp del] 

430 

431 
(*Hide the binary representation of integer constants*) 

432 
declare integ_of_Pls [simp del] integ_of_Min [simp del] integ_of_BIT [simp del] 

433 

434 

435 
lemmas bin_arith_extra_simps = 

46820  436 
integ_of_add [symmetric] 
437 
integ_of_minus [symmetric] 

438 
integ_of_mult [symmetric] 

439 
bin_succ_1 bin_succ_0 

440 
bin_pred_1 bin_pred_0 

441 
bin_minus_1 bin_minus_0 

23146  442 
bin_add_Pls_right bin_add_Min_right 
443 
bin_add_BIT_0 bin_add_BIT_10 bin_add_BIT_11 

444 
diff_integ_of_eq 

445 
bin_mult_1 bin_mult_0 NCons_simps 

446 

447 

448 
(*For making a minimal simpset, one must include these default simprules 

449 
of thy. Also include simp_thms, or at least (~False)=True*) 

450 
lemmas bin_arith_simps = 

451 
bin_pred_Pls bin_pred_Min 

452 
bin_succ_Pls bin_succ_Min 

453 
bin_add_Pls bin_add_Min 

454 
bin_minus_Pls bin_minus_Min 

46820  455 
bin_mult_Pls bin_mult_Min 
23146  456 
bin_arith_extra_simps 
457 

458 
(*Simplification of relational operations*) 

459 
lemmas bin_rel_simps = 

460 
eq_integ_of_eq iszero_integ_of_Pls nonzero_integ_of_Min 

461 
iszero_integ_of_0 iszero_integ_of_1 

462 
less_integ_of_eq_neg 

463 
not_neg_integ_of_Pls neg_integ_of_Min neg_integ_of_BIT 

464 
le_integ_of_eq_not_less 

465 

466 
declare bin_arith_simps [simp] 

467 
declare bin_rel_simps [simp] 

468 

469 

470 
(** Simplification of arithmetic when nested to the right **) 

471 

472 
lemma add_integ_of_left [simp]: 

46953  473 
"[ v \<in> bin; w \<in> bin ] 
23146  474 
==> integ_of(v) $+ (integ_of(w) $+ z) = (integ_of(bin_add(v,w)) $+ z)" 
475 
by (simp add: zadd_assoc [symmetric]) 

476 

477 
lemma mult_integ_of_left [simp]: 

46953  478 
"[ v \<in> bin; w \<in> bin ] 
23146  479 
==> integ_of(v) $* (integ_of(w) $* z) = (integ_of(bin_mult(v,w)) $* z)" 
480 
by (simp add: zmult_assoc [symmetric]) 

481 

46820  482 
lemma add_integ_of_diff1 [simp]: 
46953  483 
"[ v \<in> bin; w \<in> bin ] 
23146  484 
==> integ_of(v) $+ (integ_of(w) $ c) = integ_of(bin_add(v,w)) $ (c)" 
485 
apply (unfold zdiff_def) 

486 
apply (rule add_integ_of_left, auto) 

487 
done 

488 

489 
lemma add_integ_of_diff2 [simp]: 

46953  490 
"[ v \<in> bin; w \<in> bin ] 
46820  491 
==> integ_of(v) $+ (c $ integ_of(w)) = 
23146  492 
integ_of (bin_add (v, bin_minus(w))) $+ (c)" 
493 
apply (subst diff_integ_of_eq [symmetric]) 

494 
apply (simp_all add: zdiff_def zadd_ac) 

495 
done 

496 

497 

498 
(** More for integer constants **) 

499 

500 
declare int_of_0 [simp] int_of_succ [simp] 

501 

502 
lemma zdiff0 [simp]: "#0 $ x = $x" 

503 
by (simp add: zdiff_def) 

504 

505 
lemma zdiff0_right [simp]: "x $ #0 = intify(x)" 

506 
by (simp add: zdiff_def) 

507 

508 
lemma zdiff_self [simp]: "x $ x = #0" 

509 
by (simp add: zdiff_def) 

510 

46953  511 
lemma znegative_iff_zless_0: "k \<in> int ==> znegative(k) \<longleftrightarrow> k $< #0" 
23146  512 
by (simp add: zless_def) 
513 

46953  514 
lemma zero_zless_imp_znegative_zminus: "[#0 $< k; k \<in> int] ==> znegative($k)" 
23146  515 
by (simp add: zless_def) 
516 

517 
lemma zero_zle_int_of [simp]: "#0 $<= $# n" 

518 
by (simp add: not_zless_iff_zle [THEN iff_sym] znegative_iff_zless_0 [THEN iff_sym]) 

519 

520 
lemma nat_of_0 [simp]: "nat_of(#0) = 0" 

521 
by (simp only: natify_0 int_of_0 [symmetric] nat_of_int_of) 

522 

46953  523 
lemma nat_le_int0_lemma: "[ z $<= $#0; z \<in> int ] ==> nat_of(z) = 0" 
23146  524 
by (auto simp add: znegative_iff_zless_0 [THEN iff_sym] zle_def zneg_nat_of) 
525 

526 
lemma nat_le_int0: "z $<= $#0 ==> nat_of(z) = 0" 

527 
apply (subgoal_tac "nat_of (intify (z)) = 0") 

528 
apply (rule_tac [2] nat_le_int0_lemma, auto) 

529 
done 

530 

531 
lemma int_of_eq_0_imp_natify_eq_0: "$# n = #0 ==> natify(n) = 0" 

532 
by (rule not_znegative_imp_zero, auto) 

533 

534 
lemma nat_of_zminus_int_of: "nat_of($ $# n) = 0" 

535 
by (simp add: nat_of_def int_of_def raw_nat_of zminus image_intrel_int) 

536 

537 
lemma int_of_nat_of: "#0 $<= z ==> $# nat_of(z) = intify(z)" 

538 
apply (rule not_zneg_nat_of_intify) 

539 
apply (simp add: znegative_iff_zless_0 not_zless_iff_zle) 

540 
done 

541 

542 
declare int_of_nat_of [simp] nat_of_zminus_int_of [simp] 

543 

544 
lemma int_of_nat_of_if: "$# nat_of(z) = (if #0 $<= z then intify(z) else #0)" 

545 
by (simp add: int_of_nat_of znegative_iff_zless_0 not_zle_iff_zless) 

546 

46953  547 
lemma zless_nat_iff_int_zless: "[ m \<in> nat; z \<in> int ] ==> (m < nat_of(z)) \<longleftrightarrow> ($#m $< z)" 
23146  548 
apply (case_tac "znegative (z) ") 
549 
apply (erule_tac [2] not_zneg_nat_of [THEN subst]) 

550 
apply (auto dest: zless_trans dest!: zero_zle_int_of [THEN zle_zless_trans] 

551 
simp add: znegative_iff_zless_0) 

552 
done 

553 

554 

555 
(** nat_of and zless **) 

556 

46820  557 
(*An alternative condition is @{term"$#0 \<subseteq> w"} *) 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

558 
lemma zless_nat_conj_lemma: "$#0 $< z ==> (nat_of(w) < nat_of(z)) \<longleftrightarrow> (w $< z)" 
23146  559 
apply (rule iff_trans) 
560 
apply (rule zless_int_of [THEN iff_sym]) 

561 
apply (auto simp add: int_of_nat_of_if simp del: zless_int_of) 

562 
apply (auto elim: zless_asym simp add: not_zle_iff_zless) 

563 
apply (blast intro: zless_zle_trans) 

564 
done 

565 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

566 
lemma zless_nat_conj: "(nat_of(w) < nat_of(z)) \<longleftrightarrow> ($#0 $< z & w $< z)" 
23146  567 
apply (case_tac "$#0 $< z") 
568 
apply (auto simp add: zless_nat_conj_lemma nat_le_int0 not_zless_iff_zle) 

569 
done 

570 

571 
(*This simprule cannot be added unless we can find a way to make eq_integ_of_eq 

572 
unconditional! 

573 
[The condition "True" is a hack to prevent looping. 

574 
Conditional rewrite rules are tried after unconditional ones, so a rule 

575 
like eq_nat_number_of will be tried first to eliminate #mm=#nn.] 

576 
lemma integ_of_reorient [simp]: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

577 
"True ==> (integ_of(w) = x) \<longleftrightarrow> (x = integ_of(w))" 
23146  578 
by auto 
579 
*) 

580 

581 
lemma integ_of_minus_reorient [simp]: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

582 
"(integ_of(w) = $ x) \<longleftrightarrow> ($ x = integ_of(w))" 
23146  583 
by auto 
584 

585 
lemma integ_of_add_reorient [simp]: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

586 
"(integ_of(w) = x $+ y) \<longleftrightarrow> (x $+ y = integ_of(w))" 
23146  587 
by auto 
588 

589 
lemma integ_of_diff_reorient [simp]: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

590 
"(integ_of(w) = x $ y) \<longleftrightarrow> (x $ y = integ_of(w))" 
23146  591 
by auto 
592 

593 
lemma integ_of_mult_reorient [simp]: 

46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

594 
"(integ_of(w) = x $* y) \<longleftrightarrow> (x $* y = integ_of(w))" 
23146  595 
by auto 
596 

597 
end 