author  wenzelm 
Tue, 11 Nov 2014 11:41:58 +0100  
changeset 58972  5b026cfc5f04 
parent 58963  26bf09b95dda 
child 58976  b38a54bbfbd6 
permissions  rwrr 
17441  1 
(* Title: CTT/Arith.thy 
1474  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  3 
Copyright 1991 University of Cambridge 
4 
*) 

5 

58889  6 
section {* Elementary arithmetic *} 
17441  7 

8 
theory Arith 

9 
imports Bool 

10 
begin 

0  11 

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

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

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

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

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

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

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

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

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

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

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

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

29 

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

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

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

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

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

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

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

38 

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

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

17441  45 

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

48 

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

50 

51 
(** Addition *) 

52 

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

54 

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

56 
apply (unfold arith_defs) 

58972  57 
apply typechk 
19761  58 
done 
59 

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

61 
apply (unfold arith_defs) 

58972  62 
apply equal 
19761  63 
done 
64 

65 

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

67 

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

69 
apply (unfold arith_defs) 

58972  70 
apply rew 
19761  71 
done 
72 

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

74 
apply (unfold arith_defs) 

58972  75 
apply rew 
19761  76 
done 
77 

78 

79 
(** Multiplication *) 

80 

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

82 

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

84 
apply (unfold arith_defs) 

58972  85 
apply (typechk add_typing) 
19761  86 
done 
87 

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

89 
apply (unfold arith_defs) 

58972  90 
apply (equal add_typingL) 
19761  91 
done 
92 

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

94 

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

96 
apply (unfold arith_defs) 

58972  97 
apply rew 
19761  98 
done 
99 

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

101 
apply (unfold arith_defs) 

58972  102 
apply rew 
19761  103 
done 
104 

105 

106 
(** Difference *) 

107 

108 
(*typing of difference*) 

109 

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

111 
apply (unfold arith_defs) 

58972  112 
apply typechk 
19761  113 
done 
114 

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

116 
apply (unfold arith_defs) 

58972  117 
apply equal 
19761  118 
done 
119 

120 

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

122 

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

124 
apply (unfold arith_defs) 

58972  125 
apply rew 
19761  126 
done 
127 

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

129 

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

131 
apply (unfold arith_defs) 

58972  132 
apply (NE b) 
133 
apply hyp_rew 

19761  134 
done 
135 

136 

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

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

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

140 
apply (unfold arith_defs) 

58972  141 
apply hyp_rew 
142 
apply (NE b) 

143 
apply hyp_rew 

19761  144 
done 
145 

146 

147 
subsection {* Simplification *} 

148 

149 
lemmas arith_typing_rls = add_typing mult_typing diff_typing 

150 
and arith_congr_rls = add_typingL mult_typingL diff_typingL 

151 
lemmas congr_rls = arith_congr_rls intrL2_rls elimL_rls 

152 

153 
lemmas arithC_rls = 

154 
addC0 addC_succ 

155 
multC0 multC_succ 

156 
diffC0 diff_0_eq_0 diff_succ_succ 

157 

158 
ML {* 

159 

160 
structure Arith_simp_data: TSIMP_DATA = 

161 
struct 

39159  162 
val refl = @{thm refl_elem} 
163 
val sym = @{thm sym_elem} 

164 
val trans = @{thm trans_elem} 

165 
val refl_red = @{thm refl_red} 

166 
val trans_red = @{thm trans_red} 

167 
val red_if_equal = @{thm red_if_equal} 

168 
val default_rls = @{thms arithC_rls} @ @{thms comp_rls} 

169 
val routine_tac = routine_tac (@{thms arith_typing_rls} @ @{thms routine_rls}) 

19761  170 
end 
171 

172 
structure Arith_simp = TSimpFun (Arith_simp_data) 

173 

39159  174 
local val congr_rls = @{thms congr_rls} in 
19761  175 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

176 
fun arith_rew_tac ctxt prems = make_rew_tac ctxt 
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

177 
(Arith_simp.norm_tac ctxt (congr_rls, prems)) 
19761  178 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

179 
fun hyp_arith_rew_tac ctxt prems = make_rew_tac ctxt 
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

180 
(Arith_simp.cond_norm_tac ctxt (prove_cond_tac, congr_rls, prems)) 
17441  181 

0  182 
end 
19761  183 
*} 
184 

58972  185 
method_setup arith_rew = {* 
186 
Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (arith_rew_tac ctxt ths)) 

187 
*} 

188 

189 
method_setup hyp_arith_rew = {* 

190 
Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (hyp_arith_rew_tac ctxt ths)) 

191 
*} 

192 

19761  193 

194 
subsection {* Addition *} 

195 

196 
(*Associative law for addition*) 

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

58972  198 
apply (NE a) 
199 
apply hyp_arith_rew 

19761  200 
done 
201 

202 

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

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

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

58972  206 
apply (NE a) 
207 
apply hyp_arith_rew 

19761  208 
apply (rule sym_elem) 
58972  209 
prefer 2 
210 
apply (NE b) 

211 
prefer 4 

212 
apply (NE b) 

213 
apply hyp_arith_rew 

19761  214 
done 
215 

216 

217 
subsection {* Multiplication *} 

218 

219 
(*right annihilation in product*) 

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

58972  221 
apply (NE a) 
222 
apply hyp_arith_rew 

19761  223 
done 
224 

225 
(*right successor law for multiplication*) 

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

58972  227 
apply (NE a) 
228 
apply (hyp_arith_rew add_assoc [THEN sym_elem]) 

19761  229 
apply (assumption  rule add_commute mult_typingL add_typingL intrL_rls refl_elem)+ 
230 
done 

231 

232 
(*Commutative law for multiplication*) 

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

58972  234 
apply (NE a) 
235 
apply (hyp_arith_rew mult_0_right mult_succ_right) 

19761  236 
done 
237 

238 
(*addition distributes over multiplication*) 

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

58972  240 
apply (NE a) 
241 
apply (hyp_arith_rew add_assoc [THEN sym_elem]) 

19761  242 
done 
243 

244 
(*Associative law for multiplication*) 

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

58972  246 
apply (NE a) 
247 
apply (hyp_arith_rew add_mult_distrib) 

19761  248 
done 
249 

250 

251 
subsection {* Difference *} 

252 

253 
text {* 

254 
Difference on natural numbers, without negative numbers 

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

256 

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

58972  258 
apply (NE a) 
259 
apply hyp_arith_rew 

19761  260 
done 
261 

262 

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

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

265 

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

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

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

36319  269 
schematic_lemma add_diff_inverse_lemma: 
270 
"b:N ==> ?a : PROD x:N. Eq(N, bx, 0) > Eq(N, b #+ (xb), x)" 

58972  271 
apply (NE b) 
19761  272 
(*strip one "universal quantifier" but not the "implication"*) 
273 
apply (rule_tac [3] intr_rls) 

274 
(*case analysis on x in 

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

58972  276 
prefer 4 
277 
apply (NE x) 

278 
apply assumption 

19761  279 
(*Prepare for simplification of types  the antecedent succ(u)<=x *) 
58972  280 
apply (rule_tac [2] replace_type) 
281 
apply (rule_tac [1] replace_type) 

282 
apply arith_rew 

19761  283 
(*Solves first 0 goal, simplifies others. Two sugbgoals remain. 
284 
Both follow by rewriting, (2) using quantified induction hyp*) 

58972  285 
apply intr (*strips remaining PRODs*) 
286 
apply (hyp_arith_rew add_0_right) 

19761  287 
apply assumption 
288 
done 

289 

290 

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

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

293 
Instead, add_diff_inverse_lemma states the desired induction scheme 

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

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

296 
apply (rule EqE) 

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

298 
apply (assumption  rule EqI)+ 

299 
done 

300 

301 

302 
subsection {* Absolute difference *} 

303 

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

305 

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

307 
apply (unfold arith_defs) 

58972  308 
apply typechk 
19761  309 
done 
310 

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

312 
apply (unfold arith_defs) 

58972  313 
apply equal 
19761  314 
done 
315 

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

317 
apply (unfold absdiff_def) 

58972  318 
apply (arith_rew diff_self_eq_0) 
19761  319 
done 
320 

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

322 
apply (unfold absdiff_def) 

58972  323 
apply hyp_arith_rew 
19761  324 
done 
325 

326 

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

328 
apply (unfold absdiff_def) 

58972  329 
apply hyp_arith_rew 
19761  330 
done 
331 

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

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

334 
apply (unfold absdiff_def) 

335 
apply (rule add_commute) 

58972  336 
apply (typechk diff_typing) 
19761  337 
done 
338 

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

36319  340 
schematic_lemma add_eq0_lemma: "[ a:N; b:N ] ==> ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)" 
58972  341 
apply (NE a) 
19761  342 
apply (rule_tac [3] replace_type) 
58972  343 
apply arith_rew 
344 
apply intr (*strips remaining PRODs*) 

19761  345 
apply (rule_tac [2] zero_ne_succ [THEN FE]) 
346 
apply (erule_tac [3] EqE [THEN sym_elem]) 

58972  347 
apply (typechk add_typing) 
19761  348 
done 
349 

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

351 
Again, resolution instantiates variables in ProdE *) 

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

353 
apply (rule EqE) 

354 
apply (rule add_eq0_lemma [THEN ProdE]) 

355 
apply (rule_tac [3] EqI) 

58972  356 
apply typechk 
19761  357 
done 
358 

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

36319  360 
schematic_lemma absdiff_eq0_lem: 
19761  361 
"[ a:N; b:N; a  b = 0 : N ] ==> 
362 
?a : SUM v: Eq(N, ab, 0) . Eq(N, ba, 0)" 

363 
apply (unfold absdiff_def) 

58972  364 
apply intr 
365 
apply eqintr 

19761  366 
apply (rule_tac [2] add_eq0) 
367 
apply (rule add_eq0) 

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

58972  369 
apply (typechk diff_typing) 
19761  370 
done 
371 

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

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

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

375 
apply (rule EqE) 

376 
apply (rule absdiff_eq0_lem [THEN SumE]) 

58972  377 
apply eqintr 
19761  378 
apply (rule add_diff_inverse [THEN sym_elem, THEN trans_elem]) 
58972  379 
apply (erule_tac [3] EqE) 
380 
apply (hyp_arith_rew add_0_right) 

19761  381 
done 
382 

383 

384 
subsection {* Remainder and Quotient *} 

385 

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

387 

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

389 
apply (unfold mod_def) 

58972  390 
apply (typechk absdiff_typing) 
19761  391 
done 
392 

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

394 
apply (unfold mod_def) 

58972  395 
apply (equal absdiff_typingL) 
19761  396 
done 
397 

398 

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

400 

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

402 
apply (unfold mod_def) 

58972  403 
apply (rew absdiff_typing) 
19761  404 
done 
405 

406 
lemma modC_succ: 

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

408 
apply (unfold mod_def) 

58972  409 
apply (rew absdiff_typing) 
19761  410 
done 
411 

412 

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

414 

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

416 
apply (unfold div_def) 

58972  417 
apply (typechk absdiff_typing mod_typing) 
19761  418 
done 
419 

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

421 
apply (unfold div_def) 

58972  422 
apply (equal absdiff_typingL mod_typingL) 
19761  423 
done 
424 

425 
lemmas div_typing_rls = mod_typing div_typing absdiff_typing 

426 

427 

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

429 

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

431 
apply (unfold div_def) 

58972  432 
apply (rew mod_typing absdiff_typing) 
19761  433 
done 
434 

435 
lemma divC_succ: 

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

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

438 
apply (unfold div_def) 

58972  439 
apply (rew mod_typing) 
19761  440 
done 
441 

442 

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

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

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

446 
apply (rule divC_succ [THEN trans_elem]) 

58972  447 
apply (rew div_typing_rls modC_succ) 
448 
apply (NE "succ (a mod b) b") 

449 
apply (rew mod_typing div_typing absdiff_typing) 

19761  450 
done 
451 

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

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

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

58972  455 
apply (NE a) 
19761  456 
apply (rule_tac [3] PlusI_inr) 
457 
apply (rule_tac [2] PlusI_inl) 

58972  458 
apply eqintr 
459 
apply equal 

19761  460 
done 
461 

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

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

58972  464 
apply (NE a) 
465 
apply (arith_rew div_typing_rls modC0 modC_succ divC0 divC_succ2) 

19761  466 
apply (rule EqE) 
467 
(*case analysis on succ(u mod b)b *) 

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

469 
apply (erule_tac [3] SumE) 

58972  470 
apply (hyp_arith_rew div_typing_rls modC0 modC_succ divC0 divC_succ2) 
58318  471 
(*Replace one occurrence of b by succ(u mod b). Clumsy!*) 
19761  472 
apply (rule add_typingL [THEN trans_elem]) 
473 
apply (erule EqE [THEN absdiff_eq0, THEN sym_elem]) 

474 
apply (rule_tac [3] refl_elem) 

58972  475 
apply (hyp_arith_rew div_typing_rls) 
19761  476 
done 
477 

478 
end 