author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 21404  eb85850d3eb7 
child 27208  5fe899199f85 
permissions  rwrr 
17441  1 
(* Title: CTT/Arith.thy 
0  2 
ID: $Id$ 
1474  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1991 University of Cambridge 
5 
*) 

6 

19761  7 
header {* Elementary arithmetic *} 
17441  8 

9 
theory Arith 

10 
imports Bool 

11 
begin 

0  12 

19761  13 
subsection {* Arithmetic operators and their definitions *} 
17441  14 

19762  15 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

16 
add :: "[i,i]=>i" (infixr "#+" 65) where 
19762  17 
"a#+b == rec(a, b, %u v. succ(v))" 
0  18 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

19 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

20 
diff :: "[i,i]=>i" (infixr "" 65) where 
19762  21 
"ab == rec(b, a, %u v. rec(v, 0, %x y. x))" 
22 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

23 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

24 
absdiff :: "[i,i]=>i" (infixr "" 65) where 
19762  25 
"ab == (ab) #+ (ba)" 
26 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

27 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

28 
mult :: "[i,i]=>i" (infixr "#*" 70) where 
19762  29 
"a#*b == rec(a, 0, %u v. b #+ v)" 
10467
e6e7205e9e91
xsymbol support for Pi, Sigma, >, : (membership)
paulson
parents:
3837
diff
changeset

30 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

31 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

32 
mod :: "[i,i]=>i" (infixr "mod" 70) where 
19762  33 
"a mod b == rec(a, 0, %u v. rec(succ(v)  b, 0, %x y. succ(v)))" 
34 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

35 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

36 
div :: "[i,i]=>i" (infixr "div" 70) where 
19762  37 
"a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))" 
38 

10467
e6e7205e9e91
xsymbol support for Pi, Sigma, >, : (membership)
paulson
parents:
3837
diff
changeset

39 

21210  40 
notation (xsymbols) 
19762  41 
mult (infixr "#\<times>" 70) 
42 

21210  43 
notation (HTML output) 
19762  44 
mult (infixr "#\<times>" 70) 
45 

17441  46 

19761  47 
lemmas arith_defs = add_def diff_def absdiff_def mult_def mod_def div_def 
48 

49 

50 
subsection {* Proofs about elementary arithmetic: addition, multiplication, etc. *} 

51 

52 
(** Addition *) 

53 

54 
(*typing of add: short and long versions*) 

55 

56 
lemma add_typing: "[ a:N; b:N ] ==> a #+ b : N" 

57 
apply (unfold arith_defs) 

58 
apply (tactic "typechk_tac []") 

59 
done 

60 

61 
lemma add_typingL: "[ a=c:N; b=d:N ] ==> a #+ b = c #+ d : N" 

62 
apply (unfold arith_defs) 

63 
apply (tactic "equal_tac []") 

64 
done 

65 

66 

67 
(*computation for add: 0 and successor cases*) 

68 

69 
lemma addC0: "b:N ==> 0 #+ b = b : N" 

70 
apply (unfold arith_defs) 

71 
apply (tactic "rew_tac []") 

72 
done 

73 

74 
lemma addC_succ: "[ a:N; b:N ] ==> succ(a) #+ b = succ(a #+ b) : N" 

75 
apply (unfold arith_defs) 

76 
apply (tactic "rew_tac []") 

77 
done 

78 

79 

80 
(** Multiplication *) 

81 

82 
(*typing of mult: short and long versions*) 

83 

84 
lemma mult_typing: "[ a:N; b:N ] ==> a #* b : N" 

85 
apply (unfold arith_defs) 

86 
apply (tactic {* typechk_tac [thm "add_typing"] *}) 

87 
done 

88 

89 
lemma mult_typingL: "[ a=c:N; b=d:N ] ==> a #* b = c #* d : N" 

90 
apply (unfold arith_defs) 

91 
apply (tactic {* equal_tac [thm "add_typingL"] *}) 

92 
done 

93 

94 
(*computation for mult: 0 and successor cases*) 

95 

96 
lemma multC0: "b:N ==> 0 #* b = 0 : N" 

97 
apply (unfold arith_defs) 

98 
apply (tactic "rew_tac []") 

99 
done 

100 

101 
lemma multC_succ: "[ a:N; b:N ] ==> succ(a) #* b = b #+ (a #* b) : N" 

102 
apply (unfold arith_defs) 

103 
apply (tactic "rew_tac []") 

104 
done 

105 

106 

107 
(** Difference *) 

108 

109 
(*typing of difference*) 

110 

111 
lemma diff_typing: "[ a:N; b:N ] ==> a  b : N" 

112 
apply (unfold arith_defs) 

113 
apply (tactic "typechk_tac []") 

114 
done 

115 

116 
lemma diff_typingL: "[ a=c:N; b=d:N ] ==> a  b = c  d : N" 

117 
apply (unfold arith_defs) 

118 
apply (tactic "equal_tac []") 

119 
done 

120 

121 

122 
(*computation for difference: 0 and successor cases*) 

123 

124 
lemma diffC0: "a:N ==> a  0 = a : N" 

125 
apply (unfold arith_defs) 

126 
apply (tactic "rew_tac []") 

127 
done 

128 

129 
(*Note: rec(a, 0, %z w.z) is pred(a). *) 

130 

131 
lemma diff_0_eq_0: "b:N ==> 0  b = 0 : N" 

132 
apply (unfold arith_defs) 

133 
apply (tactic {* NE_tac "b" 1 *}) 

134 
apply (tactic "hyp_rew_tac []") 

135 
done 

136 

137 

138 
(*Essential to simplify FIRST!! (Else we get a critical pair) 

139 
succ(a)  succ(b) rewrites to pred(succ(a)  b) *) 

140 
lemma diff_succ_succ: "[ a:N; b:N ] ==> succ(a)  succ(b) = a  b : N" 

141 
apply (unfold arith_defs) 

142 
apply (tactic "hyp_rew_tac []") 

143 
apply (tactic {* NE_tac "b" 1 *}) 

144 
apply (tactic "hyp_rew_tac []") 

145 
done 

146 

147 

148 
subsection {* Simplification *} 

149 

150 
lemmas arith_typing_rls = add_typing mult_typing diff_typing 

151 
and arith_congr_rls = add_typingL mult_typingL diff_typingL 

152 
lemmas congr_rls = arith_congr_rls intrL2_rls elimL_rls 

153 

154 
lemmas arithC_rls = 

155 
addC0 addC_succ 

156 
multC0 multC_succ 

157 
diffC0 diff_0_eq_0 diff_succ_succ 

158 

159 
ML {* 

160 

161 
structure Arith_simp_data: TSIMP_DATA = 

162 
struct 

163 
val refl = thm "refl_elem" 

164 
val sym = thm "sym_elem" 

165 
val trans = thm "trans_elem" 

166 
val refl_red = thm "refl_red" 

167 
val trans_red = thm "trans_red" 

168 
val red_if_equal = thm "red_if_equal" 

169 
val default_rls = thms "arithC_rls" @ thms "comp_rls" 

170 
val routine_tac = routine_tac (thms "arith_typing_rls" @ thms "routine_rls") 

171 
end 

172 

173 
structure Arith_simp = TSimpFun (Arith_simp_data) 

174 

175 
local val congr_rls = thms "congr_rls" in 

176 

177 
fun arith_rew_tac prems = make_rew_tac 

178 
(Arith_simp.norm_tac(congr_rls, prems)) 

179 

180 
fun hyp_arith_rew_tac prems = make_rew_tac 

181 
(Arith_simp.cond_norm_tac(prove_cond_tac, congr_rls, prems)) 

17441  182 

0  183 
end 
19761  184 
*} 
185 

186 

187 
subsection {* Addition *} 

188 

189 
(*Associative law for addition*) 

190 
lemma add_assoc: "[ a:N; b:N; c:N ] ==> (a #+ b) #+ c = a #+ (b #+ c) : N" 

191 
apply (tactic {* NE_tac "a" 1 *}) 

192 
apply (tactic "hyp_arith_rew_tac []") 

193 
done 

194 

195 

196 
(*Commutative law for addition. Can be proved using three inductions. 

197 
Must simplify after first induction! Orientation of rewrites is delicate*) 

198 
lemma add_commute: "[ a:N; b:N ] ==> a #+ b = b #+ a : N" 

199 
apply (tactic {* NE_tac "a" 1 *}) 

200 
apply (tactic "hyp_arith_rew_tac []") 

201 
apply (tactic {* NE_tac "b" 2 *}) 

202 
apply (rule sym_elem) 

203 
apply (tactic {* NE_tac "b" 1 *}) 

204 
apply (tactic "hyp_arith_rew_tac []") 

205 
done 

206 

207 

208 
subsection {* Multiplication *} 

209 

210 
(*right annihilation in product*) 

211 
lemma mult_0_right: "a:N ==> a #* 0 = 0 : N" 

212 
apply (tactic {* NE_tac "a" 1 *}) 

213 
apply (tactic "hyp_arith_rew_tac []") 

214 
done 

215 

216 
(*right successor law for multiplication*) 

217 
lemma mult_succ_right: "[ a:N; b:N ] ==> a #* succ(b) = a #+ (a #* b) : N" 

218 
apply (tactic {* NE_tac "a" 1 *}) 

219 
apply (tactic {* hyp_arith_rew_tac [thm "add_assoc" RS thm "sym_elem"] *}) 

220 
apply (assumption  rule add_commute mult_typingL add_typingL intrL_rls refl_elem)+ 

221 
done 

222 

223 
(*Commutative law for multiplication*) 

224 
lemma mult_commute: "[ a:N; b:N ] ==> a #* b = b #* a : N" 

225 
apply (tactic {* NE_tac "a" 1 *}) 

226 
apply (tactic {* hyp_arith_rew_tac [thm "mult_0_right", thm "mult_succ_right"] *}) 

227 
done 

228 

229 
(*addition distributes over multiplication*) 

230 
lemma add_mult_distrib: "[ a:N; b:N; c:N ] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N" 

231 
apply (tactic {* NE_tac "a" 1 *}) 

232 
apply (tactic {* hyp_arith_rew_tac [thm "add_assoc" RS thm "sym_elem"] *}) 

233 
done 

234 

235 
(*Associative law for multiplication*) 

236 
lemma mult_assoc: "[ a:N; b:N; c:N ] ==> (a #* b) #* c = a #* (b #* c) : N" 

237 
apply (tactic {* NE_tac "a" 1 *}) 

238 
apply (tactic {* hyp_arith_rew_tac [thm "add_mult_distrib"] *}) 

239 
done 

240 

241 

242 
subsection {* Difference *} 

243 

244 
text {* 

245 
Difference on natural numbers, without negative numbers 

246 
a  b = 0 iff a<=b a  b = succ(c) iff a>b *} 

247 

248 
lemma diff_self_eq_0: "a:N ==> a  a = 0 : N" 

249 
apply (tactic {* NE_tac "a" 1 *}) 

250 
apply (tactic "hyp_arith_rew_tac []") 

251 
done 

252 

253 

254 
lemma add_0_right: "[ c : N; 0 : N; c : N ] ==> c #+ 0 = c : N" 

255 
by (rule addC0 [THEN [3] add_commute [THEN trans_elem]]) 

256 

257 
(*Addition is the inverse of subtraction: if b<=x then b#+(xb) = x. 

258 
An example of induction over a quantified formula (a product). 

259 
Uses rewriting with a quantified, implicative inductive hypothesis.*) 

260 
lemma add_diff_inverse_lemma: "b:N ==> ?a : PROD x:N. Eq(N, bx, 0) > Eq(N, b #+ (xb), x)" 

261 
apply (tactic {* NE_tac "b" 1 *}) 

262 
(*strip one "universal quantifier" but not the "implication"*) 

263 
apply (rule_tac [3] intr_rls) 

264 
(*case analysis on x in 

265 
(succ(u) <= x) > (succ(u)#+(xsucc(u)) = x) *) 

266 
apply (tactic {* NE_tac "x" 4 *}, tactic "assume_tac 4") 

267 
(*Prepare for simplification of types  the antecedent succ(u)<=x *) 

268 
apply (rule_tac [5] replace_type) 

269 
apply (rule_tac [4] replace_type) 

270 
apply (tactic "arith_rew_tac []") 

271 
(*Solves first 0 goal, simplifies others. Two sugbgoals remain. 

272 
Both follow by rewriting, (2) using quantified induction hyp*) 

273 
apply (tactic "intr_tac []") (*strips remaining PRODs*) 

274 
apply (tactic {* hyp_arith_rew_tac [thm "add_0_right"] *}) 

275 
apply assumption 

276 
done 

277 

278 

279 
(*Version of above with premise ba=0 i.e. a >= b. 

280 
Using ProdE does not work  for ?B(?a) is ambiguous. 

281 
Instead, add_diff_inverse_lemma states the desired induction scheme 

282 
the use of RS below instantiates Vars in ProdE automatically. *) 

283 
lemma add_diff_inverse: "[ a:N; b:N; ba = 0 : N ] ==> b #+ (ab) = a : N" 

284 
apply (rule EqE) 

285 
apply (rule add_diff_inverse_lemma [THEN ProdE, THEN ProdE]) 

286 
apply (assumption  rule EqI)+ 

287 
done 

288 

289 

290 
subsection {* Absolute difference *} 

291 

292 
(*typing of absolute difference: short and long versions*) 

293 

294 
lemma absdiff_typing: "[ a:N; b:N ] ==> a  b : N" 

295 
apply (unfold arith_defs) 

296 
apply (tactic "typechk_tac []") 

297 
done 

298 

299 
lemma absdiff_typingL: "[ a=c:N; b=d:N ] ==> a  b = c  d : N" 

300 
apply (unfold arith_defs) 

301 
apply (tactic "equal_tac []") 

302 
done 

303 

304 
lemma absdiff_self_eq_0: "a:N ==> a  a = 0 : N" 

305 
apply (unfold absdiff_def) 

306 
apply (tactic {* arith_rew_tac [thm "diff_self_eq_0"] *}) 

307 
done 

308 

309 
lemma absdiffC0: "a:N ==> 0  a = a : N" 

310 
apply (unfold absdiff_def) 

311 
apply (tactic "hyp_arith_rew_tac []") 

312 
done 

313 

314 

315 
lemma absdiff_succ_succ: "[ a:N; b:N ] ==> succ(a)  succ(b) = a  b : N" 

316 
apply (unfold absdiff_def) 

317 
apply (tactic "hyp_arith_rew_tac []") 

318 
done 

319 

320 
(*Note how easy using commutative laws can be? ...not always... *) 

321 
lemma absdiff_commute: "[ a:N; b:N ] ==> a  b = b  a : N" 

322 
apply (unfold absdiff_def) 

323 
apply (rule add_commute) 

324 
apply (tactic {* typechk_tac [thm "diff_typing"] *}) 

325 
done 

326 

327 
(*If a+b=0 then a=0. Surprisingly tedious*) 

328 
lemma add_eq0_lemma: "[ a:N; b:N ] ==> ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)" 

329 
apply (tactic {* NE_tac "a" 1 *}) 

330 
apply (rule_tac [3] replace_type) 

331 
apply (tactic "arith_rew_tac []") 

332 
apply (tactic "intr_tac []") (*strips remaining PRODs*) 

333 
apply (rule_tac [2] zero_ne_succ [THEN FE]) 

334 
apply (erule_tac [3] EqE [THEN sym_elem]) 

335 
apply (tactic {* typechk_tac [thm "add_typing"] *}) 

336 
done 

337 

338 
(*Version of above with the premise a+b=0. 

339 
Again, resolution instantiates variables in ProdE *) 

340 
lemma add_eq0: "[ a:N; b:N; a #+ b = 0 : N ] ==> a = 0 : N" 

341 
apply (rule EqE) 

342 
apply (rule add_eq0_lemma [THEN ProdE]) 

343 
apply (rule_tac [3] EqI) 

344 
apply (tactic "typechk_tac []") 

345 
done 

346 

347 
(*Here is a lemma to infer ab=0 and ba=0 from ab=0, below. *) 

348 
lemma absdiff_eq0_lem: 

349 
"[ a:N; b:N; a  b = 0 : N ] ==> 

350 
?a : SUM v: Eq(N, ab, 0) . Eq(N, ba, 0)" 

351 
apply (unfold absdiff_def) 

352 
apply (tactic "intr_tac []") 

353 
apply (tactic eqintr_tac) 

354 
apply (rule_tac [2] add_eq0) 

355 
apply (rule add_eq0) 

356 
apply (rule_tac [6] add_commute [THEN trans_elem]) 

357 
apply (tactic {* typechk_tac [thm "diff_typing"] *}) 

358 
done 

359 

360 
(*if a  b = 0 then a = b 

361 
proof: ab=0 and ba=0, so b = a+(ba) = a+0 = a*) 

362 
lemma absdiff_eq0: "[ a  b = 0 : N; a:N; b:N ] ==> a = b : N" 

363 
apply (rule EqE) 

364 
apply (rule absdiff_eq0_lem [THEN SumE]) 

365 
apply (tactic "TRYALL assume_tac") 

366 
apply (tactic eqintr_tac) 

367 
apply (rule add_diff_inverse [THEN sym_elem, THEN trans_elem]) 

368 
apply (rule_tac [3] EqE, tactic "assume_tac 3") 

369 
apply (tactic {* hyp_arith_rew_tac [thm "add_0_right"] *}) 

370 
done 

371 

372 

373 
subsection {* Remainder and Quotient *} 

374 

375 
(*typing of remainder: short and long versions*) 

376 

377 
lemma mod_typing: "[ a:N; b:N ] ==> a mod b : N" 

378 
apply (unfold mod_def) 

379 
apply (tactic {* typechk_tac [thm "absdiff_typing"] *}) 

380 
done 

381 

382 
lemma mod_typingL: "[ a=c:N; b=d:N ] ==> a mod b = c mod d : N" 

383 
apply (unfold mod_def) 

384 
apply (tactic {* equal_tac [thm "absdiff_typingL"] *}) 

385 
done 

386 

387 

388 
(*computation for mod : 0 and successor cases*) 

389 

390 
lemma modC0: "b:N ==> 0 mod b = 0 : N" 

391 
apply (unfold mod_def) 

392 
apply (tactic {* rew_tac [thm "absdiff_typing"] *}) 

393 
done 

394 

395 
lemma modC_succ: 

396 
"[ a:N; b:N ] ==> succ(a) mod b = rec(succ(a mod b)  b, 0, %x y. succ(a mod b)) : N" 

397 
apply (unfold mod_def) 

398 
apply (tactic {* rew_tac [thm "absdiff_typing"] *}) 

399 
done 

400 

401 

402 
(*typing of quotient: short and long versions*) 

403 

404 
lemma div_typing: "[ a:N; b:N ] ==> a div b : N" 

405 
apply (unfold div_def) 

406 
apply (tactic {* typechk_tac [thm "absdiff_typing", thm "mod_typing"] *}) 

407 
done 

408 

409 
lemma div_typingL: "[ a=c:N; b=d:N ] ==> a div b = c div d : N" 

410 
apply (unfold div_def) 

411 
apply (tactic {* equal_tac [thm "absdiff_typingL", thm "mod_typingL"] *}) 

412 
done 

413 

414 
lemmas div_typing_rls = mod_typing div_typing absdiff_typing 

415 

416 

417 
(*computation for quotient: 0 and successor cases*) 

418 

419 
lemma divC0: "b:N ==> 0 div b = 0 : N" 

420 
apply (unfold div_def) 

421 
apply (tactic {* rew_tac [thm "mod_typing", thm "absdiff_typing"] *}) 

422 
done 

423 

424 
lemma divC_succ: 

425 
"[ a:N; b:N ] ==> succ(a) div b = 

426 
rec(succ(a) mod b, succ(a div b), %x y. a div b) : N" 

427 
apply (unfold div_def) 

428 
apply (tactic {* rew_tac [thm "mod_typing"] *}) 

429 
done 

430 

431 

432 
(*Version of above with same condition as the mod one*) 

433 
lemma divC_succ2: "[ a:N; b:N ] ==> 

434 
succ(a) div b =rec(succ(a mod b)  b, succ(a div b), %x y. a div b) : N" 

435 
apply (rule divC_succ [THEN trans_elem]) 

436 
apply (tactic {* rew_tac (thms "div_typing_rls" @ [thm "modC_succ"]) *}) 

437 
apply (tactic {* NE_tac "succ (a mod b) b" 1 *}) 

438 
apply (tactic {* rew_tac [thm "mod_typing", thm "div_typing", thm "absdiff_typing"] *}) 

439 
done 

440 

441 
(*for case analysis on whether a number is 0 or a successor*) 

442 
lemma iszero_decidable: "a:N ==> rec(a, inl(eq), %ka kb. inr(<ka, eq>)) : 

443 
Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))" 

444 
apply (tactic {* NE_tac "a" 1 *}) 

445 
apply (rule_tac [3] PlusI_inr) 

446 
apply (rule_tac [2] PlusI_inl) 

447 
apply (tactic eqintr_tac) 

448 
apply (tactic "equal_tac []") 

449 
done 

450 

451 
(*Main Result. Holds when b is 0 since a mod 0 = a and a div 0 = 0 *) 

452 
lemma mod_div_equality: "[ a:N; b:N ] ==> a mod b #+ (a div b) #* b = a : N" 

453 
apply (tactic {* NE_tac "a" 1 *}) 

454 
apply (tactic {* arith_rew_tac (thms "div_typing_rls" @ 

455 
[thm "modC0", thm "modC_succ", thm "divC0", thm "divC_succ2"]) *}) 

456 
apply (rule EqE) 

457 
(*case analysis on succ(u mod b)b *) 

458 
apply (rule_tac a1 = "succ (u mod b)  b" in iszero_decidable [THEN PlusE]) 

459 
apply (erule_tac [3] SumE) 

460 
apply (tactic {* hyp_arith_rew_tac (thms "div_typing_rls" @ 

461 
[thm "modC0", thm "modC_succ", thm "divC0", thm "divC_succ2"]) *}) 

462 
(*Replace one occurence of b by succ(u mod b). Clumsy!*) 

463 
apply (rule add_typingL [THEN trans_elem]) 

464 
apply (erule EqE [THEN absdiff_eq0, THEN sym_elem]) 

465 
apply (rule_tac [3] refl_elem) 

466 
apply (tactic {* hyp_arith_rew_tac (thms "div_typing_rls") *}) 

467 
done 

468 

469 
end 