author  oheimb 
Fri, 02 Jun 2000 17:46:32 +0200  
changeset 9020  1056cbbaeb29 
parent 3837  d7f033c74b38 
child 9249  c71db8c28727 
permissions  rwrr 
1459  1 
(* Title: CTT/arith 
0  2 
ID: $Id$ 
1459  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1991 University of Cambridge 
5 

6 
Theorems for arith.thy (Arithmetic operators) 

7 

8 
Proofs about elementary arithmetic: addition, multiplication, etc. 

9 
Tests definitions and simplifier. 

10 
*) 

11 

12 
open Arith; 

13 
val arith_defs = [add_def, diff_def, absdiff_def, mult_def, mod_def, div_def]; 

14 

15 

16 
(** Addition *) 

17 

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

19 

1294  20 
qed_goalw "add_typing" Arith.thy arith_defs 
0  21 
"[ a:N; b:N ] ==> a #+ b : N" 
354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

22 
(fn prems=> [ (typechk_tac prems) ]); 
0  23 

1294  24 
qed_goalw "add_typingL" Arith.thy arith_defs 
0  25 
"[ a=c:N; b=d:N ] ==> a #+ b = c #+ d : N" 
354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

26 
(fn prems=> [ (equal_tac prems) ]); 
0  27 

28 

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

30 

1294  31 
qed_goalw "addC0" Arith.thy arith_defs 
0  32 
"b:N ==> 0 #+ b = b : N" 
354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

33 
(fn prems=> [ (rew_tac prems) ]); 
0  34 

1294  35 
qed_goalw "addC_succ" Arith.thy arith_defs 
0  36 
"[ a:N; b:N ] ==> succ(a) #+ b = succ(a #+ b) : N" 
354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

37 
(fn prems=> [ (rew_tac prems) ]); 
0  38 

39 

40 
(** Multiplication *) 

41 

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

43 

1294  44 
qed_goalw "mult_typing" Arith.thy arith_defs 
0  45 
"[ a:N; b:N ] ==> a #* b : N" 
46 
(fn prems=> 

354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

47 
[ (typechk_tac([add_typing]@prems)) ]); 
0  48 

1294  49 
qed_goalw "mult_typingL" Arith.thy arith_defs 
0  50 
"[ a=c:N; b=d:N ] ==> a #* b = c #* d : N" 
51 
(fn prems=> 

354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

52 
[ (equal_tac (prems@[add_typingL])) ]); 
0  53 

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

55 

1294  56 
qed_goalw "multC0" Arith.thy arith_defs 
0  57 
"b:N ==> 0 #* b = 0 : N" 
354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

58 
(fn prems=> [ (rew_tac prems) ]); 
0  59 

1294  60 
qed_goalw "multC_succ" Arith.thy arith_defs 
0  61 
"[ a:N; b:N ] ==> succ(a) #* b = b #+ (a #* b) : N" 
354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

62 
(fn prems=> [ (rew_tac prems) ]); 
0  63 

64 

65 
(** Difference *) 

66 

67 
(*typing of difference*) 

68 

1294  69 
qed_goalw "diff_typing" Arith.thy arith_defs 
0  70 
"[ a:N; b:N ] ==> a  b : N" 
354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

71 
(fn prems=> [ (typechk_tac prems) ]); 
0  72 

1294  73 
qed_goalw "diff_typingL" Arith.thy arith_defs 
0  74 
"[ a=c:N; b=d:N ] ==> a  b = c  d : N" 
354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

75 
(fn prems=> [ (equal_tac prems) ]); 
0  76 

77 

78 

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

80 

1294  81 
qed_goalw "diffC0" Arith.thy arith_defs 
0  82 
"a:N ==> a  0 = a : N" 
354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

83 
(fn prems=> [ (rew_tac prems) ]); 
0  84 

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

86 

1294  87 
qed_goalw "diff_0_eq_0" Arith.thy arith_defs 
0  88 
"b:N ==> 0  b = 0 : N" 
89 
(fn prems=> 

90 
[ (NE_tac "b" 1), 

91 
(hyp_rew_tac prems) ]); 

92 

93 

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

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

1294  96 
qed_goalw "diff_succ_succ" Arith.thy arith_defs 
0  97 
"[ a:N; b:N ] ==> succ(a)  succ(b) = a  b : N" 
98 
(fn prems=> 

354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

99 
[ (hyp_rew_tac prems), 
0  100 
(NE_tac "b" 1), 
101 
(hyp_rew_tac prems) ]); 

102 

103 

104 

105 
(*** Simplification *) 

106 

107 
val arith_typing_rls = 

108 
[add_typing, mult_typing, diff_typing]; 

109 

110 
val arith_congr_rls = 

111 
[add_typingL, mult_typingL, diff_typingL]; 

112 

113 
val congr_rls = arith_congr_rls@standard_congr_rls; 

114 

115 
val arithC_rls = 

116 
[addC0, addC_succ, 

117 
multC0, multC_succ, 

118 
diffC0, diff_0_eq_0, diff_succ_succ]; 

119 

120 

121 
structure Arith_simp_data: TSIMP_DATA = 

122 
struct 

1459  123 
val refl = refl_elem 
124 
val sym = sym_elem 

125 
val trans = trans_elem 

126 
val refl_red = refl_red 

127 
val trans_red = trans_red 

128 
val red_if_equal = red_if_equal 

129 
val default_rls = arithC_rls @ comp_rls 

130 
val routine_tac = routine_tac (arith_typing_rls @ routine_rls) 

0  131 
end; 
132 

133 
structure Arith_simp = TSimpFun (Arith_simp_data); 

134 

135 
fun arith_rew_tac prems = make_rew_tac 

136 
(Arith_simp.norm_tac(congr_rls, prems)); 

137 

138 
fun hyp_arith_rew_tac prems = make_rew_tac 

139 
(Arith_simp.cond_norm_tac(prove_cond_tac, congr_rls, prems)); 

140 

141 

142 
(********** 

143 
Addition 

144 
**********) 

145 

146 
(*Associative law for addition*) 

1294  147 
qed_goal "add_assoc" Arith.thy 
0  148 
"[ a:N; b:N; c:N ] ==> (a #+ b) #+ c = a #+ (b #+ c) : N" 
149 
(fn prems=> 

150 
[ (NE_tac "a" 1), 

151 
(hyp_arith_rew_tac prems) ]); 

152 

153 

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

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

1294  156 
qed_goal "add_commute" Arith.thy 
0  157 
"[ a:N; b:N ] ==> a #+ b = b #+ a : N" 
158 
(fn prems=> 

159 
[ (NE_tac "a" 1), 

160 
(hyp_arith_rew_tac prems), 

161 
(NE_tac "b" 2), 

1459  162 
(rtac sym_elem 1), 
0  163 
(NE_tac "b" 1), 
164 
(hyp_arith_rew_tac prems) ]); 

165 

166 

167 
(**************** 

168 
Multiplication 

169 
****************) 

170 

171 
(*Commutative law for multiplication 

1294  172 
qed_goal "mult_commute" Arith.thy 
0  173 
"[ a:N; b:N ] ==> a #* b = b #* a : N" 
174 
(fn prems=> 

175 
[ (NE_tac "a" 1), 

176 
(hyp_arith_rew_tac prems), 

177 
(NE_tac "b" 2), 

1459  178 
(rtac sym_elem 1), 
0  179 
(NE_tac "b" 1), 
180 
(hyp_arith_rew_tac prems) ]); NEEDS COMMUTATIVE MATCHING 

181 
***************) 

182 

183 
(*right annihilation in product*) 

1294  184 
qed_goal "mult_0_right" Arith.thy 
0  185 
"a:N ==> a #* 0 = 0 : N" 
186 
(fn prems=> 

187 
[ (NE_tac "a" 1), 

188 
(hyp_arith_rew_tac prems) ]); 

189 

190 
(*right successor law for multiplication*) 

1294  191 
qed_goal "mult_succ_right" Arith.thy 
0  192 
"[ a:N; b:N ] ==> a #* succ(b) = a #+ (a #* b) : N" 
193 
(fn prems=> 

194 
[ (NE_tac "a" 1), 

195 
(*swap round the associative law of addition*) 

196 
(hyp_arith_rew_tac (prems @ [add_assoc RS sym_elem])), 

197 
(*leaves a goal involving a commutative law*) 

198 
(REPEAT (assume_tac 1 ORELSE 

199 
resolve_tac 

200 
(prems@[add_commute,mult_typingL,add_typingL]@ 

1459  201 
intrL_rls@[refl_elem]) 1)) ]); 
0  202 

203 
(*Commutative law for multiplication*) 

1294  204 
qed_goal "mult_commute" Arith.thy 
0  205 
"[ a:N; b:N ] ==> a #* b = b #* a : N" 
206 
(fn prems=> 

207 
[ (NE_tac "a" 1), 

208 
(hyp_arith_rew_tac (prems @ [mult_0_right, mult_succ_right])) ]); 

209 

210 
(*addition distributes over multiplication*) 

1294  211 
qed_goal "add_mult_distrib" Arith.thy 
0  212 
"[ a:N; b:N; c:N ] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N" 
213 
(fn prems=> 

214 
[ (NE_tac "a" 1), 

215 
(*swap round the associative law of addition*) 

216 
(hyp_arith_rew_tac (prems @ [add_assoc RS sym_elem])) ]); 

217 

218 

219 
(*Associative law for multiplication*) 

1294  220 
qed_goal "mult_assoc" Arith.thy 
0  221 
"[ a:N; b:N; c:N ] ==> (a #* b) #* c = a #* (b #* c) : N" 
222 
(fn prems=> 

223 
[ (NE_tac "a" 1), 

224 
(hyp_arith_rew_tac (prems @ [add_mult_distrib])) ]); 

225 

226 

227 
(************ 

228 
Difference 

229 
************ 

230 

231 
Difference on natural numbers, without negative numbers 

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

233 

1294  234 
qed_goal "diff_self_eq_0" Arith.thy 
0  235 
"a:N ==> a  a = 0 : N" 
236 
(fn prems=> 

237 
[ (NE_tac "a" 1), 

238 
(hyp_arith_rew_tac prems) ]); 

239 

240 

241 
(* [ c : N; 0 : N; c : N ] ==> c #+ 0 = c : N *) 

242 
val add_0_right = addC0 RSN (3, add_commute RS trans_elem); 

243 

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

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

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

247 
val prems = 

248 
goal Arith.thy 

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

250 
by (NE_tac "b" 1); 

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

252 
by (resolve_tac intr_rls 3); 

253 
(*case analysis on x in 

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

255 
by (NE_tac "x" 4 THEN assume_tac 4); 

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

1459  257 
by (rtac replace_type 5); 
258 
by (rtac replace_type 4); 

0  259 
by (arith_rew_tac prems); 
260 
(*Solves first 0 goal, simplifies others. Two sugbgoals remain. 

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

262 
by (intr_tac[]); (*strips remaining PRODs*) 

263 
by (hyp_arith_rew_tac (prems@[add_0_right])); 

264 
by (assume_tac 1); 

1294  265 
qed "add_diff_inverse_lemma"; 
0  266 

267 

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

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

270 
Instead, add_diff_inverse_lemma states the desired induction scheme; 

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

272 
val prems = 

273 
goal Arith.thy "[ a:N; b:N; ba = 0 : N ] ==> b #+ (ab) = a : N"; 

1459  274 
by (rtac EqE 1); 
0  275 
by (resolve_tac [ add_diff_inverse_lemma RS ProdE RS ProdE ] 1); 
276 
by (REPEAT (resolve_tac (prems@[EqI]) 1)); 

1294  277 
qed "add_diff_inverse"; 
0  278 

279 

280 
(******************** 

281 
Absolute difference 

282 
********************) 

283 

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

285 

1294  286 
qed_goalw "absdiff_typing" Arith.thy arith_defs 
0  287 
"[ a:N; b:N ] ==> a  b : N" 
354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

288 
(fn prems=> [ (typechk_tac prems) ]); 
0  289 

1294  290 
qed_goalw "absdiff_typingL" Arith.thy arith_defs 
0  291 
"[ a=c:N; b=d:N ] ==> a  b = c  d : N" 
354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

292 
(fn prems=> [ (equal_tac prems) ]); 
0  293 

1294  294 
qed_goalw "absdiff_self_eq_0" Arith.thy [absdiff_def] 
0  295 
"a:N ==> a  a = 0 : N" 
296 
(fn prems=> 

354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

297 
[ (arith_rew_tac (prems@[diff_self_eq_0])) ]); 
0  298 

1294  299 
qed_goalw "absdiffC0" Arith.thy [absdiff_def] 
0  300 
"a:N ==> 0  a = a : N" 
301 
(fn prems=> 

354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

302 
[ (hyp_arith_rew_tac prems) ]); 
0  303 

304 

1294  305 
qed_goalw "absdiff_succ_succ" Arith.thy [absdiff_def] 
0  306 
"[ a:N; b:N ] ==> succ(a)  succ(b) = a  b : N" 
307 
(fn prems=> 

354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

308 
[ (hyp_arith_rew_tac prems) ]); 
0  309 

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

354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

311 
val prems = goalw Arith.thy [absdiff_def] 
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

312 
"[ a:N; b:N ] ==> a  b = b  a : N"; 
1459  313 
by (rtac add_commute 1); 
0  314 
by (typechk_tac ([diff_typing]@prems)); 
1294  315 
qed "absdiff_commute"; 
0  316 

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

318 
val prems = 

319 
goal Arith.thy "[ a:N; b:N ] ==> ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)"; 

320 
by (NE_tac "a" 1); 

1459  321 
by (rtac replace_type 3); 
0  322 
by (arith_rew_tac prems); 
323 
by (intr_tac[]); (*strips remaining PRODs*) 

324 
by (resolve_tac [ zero_ne_succ RS FE ] 2); 

325 
by (etac (EqE RS sym_elem) 3); 

326 
by (typechk_tac ([add_typing] @prems)); 

1294  327 
qed "add_eq0_lemma"; 
0  328 

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

330 
Again, resolution instantiates variables in ProdE *) 

331 
val prems = 

332 
goal Arith.thy "[ a:N; b:N; a #+ b = 0 : N ] ==> a = 0 : N"; 

1459  333 
by (rtac EqE 1); 
0  334 
by (resolve_tac [add_eq0_lemma RS ProdE] 1); 
1459  335 
by (rtac EqI 3); 
0  336 
by (ALLGOALS (resolve_tac prems)); 
1294  337 
qed "add_eq0"; 
0  338 

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

354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

340 
val prems = goalw Arith.thy [absdiff_def] 
0  341 
"[ a:N; b:N; a  b = 0 : N ] ==> \ 
342 
\ ?a : SUM v: Eq(N, ab, 0) . Eq(N, ba, 0)"; 

343 
by (intr_tac[]); 

344 
by eqintr_tac; 

1459  345 
by (rtac add_eq0 2); 
346 
by (rtac add_eq0 1); 

0  347 
by (resolve_tac [add_commute RS trans_elem] 6); 
354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

348 
by (typechk_tac (diff_typing::prems)); 
1294  349 
qed "absdiff_eq0_lem"; 
0  350 

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

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

353 
val prems = 

354 
goal Arith.thy "[ a  b = 0 : N; a:N; b:N ] ==> a = b : N"; 

1459  355 
by (rtac EqE 1); 
0  356 
by (resolve_tac [absdiff_eq0_lem RS SumE] 1); 
357 
by (TRYALL (resolve_tac prems)); 

358 
by eqintr_tac; 

359 
by (resolve_tac [add_diff_inverse RS sym_elem RS trans_elem] 1); 

1459  360 
by (rtac EqE 3 THEN assume_tac 3); 
0  361 
by (hyp_arith_rew_tac (prems@[add_0_right])); 
1294  362 
qed "absdiff_eq0"; 
0  363 

364 
(*********************** 

365 
Remainder and Quotient 

366 
***********************) 

367 

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

369 

1294  370 
qed_goalw "mod_typing" Arith.thy [mod_def] 
0  371 
"[ a:N; b:N ] ==> a mod b : N" 
372 
(fn prems=> 

354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

373 
[ (typechk_tac (absdiff_typing::prems)) ]); 
0  374 

1294  375 
qed_goalw "mod_typingL" Arith.thy [mod_def] 
0  376 
"[ a=c:N; b=d:N ] ==> a mod b = c mod d : N" 
377 
(fn prems=> 

354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

378 
[ (equal_tac (prems@[absdiff_typingL])) ]); 
0  379 

380 

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

382 

1294  383 
qed_goalw "modC0" Arith.thy [mod_def] "b:N ==> 0 mod b = 0 : N" 
0  384 
(fn prems=> 
354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

385 
[ (rew_tac(absdiff_typing::prems)) ]); 
0  386 

1294  387 
qed_goalw "modC_succ" Arith.thy [mod_def] 
3837  388 
"[ a:N; b:N ] ==> succ(a) mod b = rec(succ(a mod b)  b, 0, %x y. succ(a mod b)) : N" 
0  389 
(fn prems=> 
354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

390 
[ (rew_tac(absdiff_typing::prems)) ]); 
0  391 

392 

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

394 

1294  395 
qed_goalw "div_typing" Arith.thy [div_def] "[ a:N; b:N ] ==> a div b : N" 
0  396 
(fn prems=> 
354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

397 
[ (typechk_tac ([absdiff_typing,mod_typing]@prems)) ]); 
0  398 

1294  399 
qed_goalw "div_typingL" Arith.thy [div_def] 
0  400 
"[ a=c:N; b=d:N ] ==> a div b = c div d : N" 
401 
(fn prems=> 

354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

402 
[ (equal_tac (prems @ [absdiff_typingL, mod_typingL])) ]); 
0  403 

404 
val div_typing_rls = [mod_typing, div_typing, absdiff_typing]; 

405 

406 

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

408 

1294  409 
qed_goalw "divC0" Arith.thy [div_def] "b:N ==> 0 div b = 0 : N" 
0  410 
(fn prems=> 
354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

411 
[ (rew_tac([mod_typing, absdiff_typing] @ prems)) ]); 
0  412 

413 
val divC_succ = 

354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

414 
prove_goalw Arith.thy [div_def] "[ a:N; b:N ] ==> succ(a) div b = \ 
0  415 
\ rec(succ(a) mod b, succ(a div b), %x y. a div b) : N" 
416 
(fn prems=> 

354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset

417 
[ (rew_tac([mod_typing]@prems)) ]); 
0  418 

419 

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

1294  421 
qed_goal "divC_succ2" Arith.thy 
0  422 
"[ a:N; b:N ] ==> \ 
423 
\ succ(a) div b =rec(succ(a mod b)  b, succ(a div b), %x y. a div b) : N" 

424 
(fn prems=> 

425 
[ (resolve_tac [ divC_succ RS trans_elem ] 1), 

426 
(rew_tac(div_typing_rls @ prems @ [modC_succ])), 

427 
(NE_tac "succ(a mod b)b" 1), 

428 
(rew_tac ([mod_typing, div_typing, absdiff_typing] @prems)) ]); 

429 

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

1294  431 
qed_goal "iszero_decidable" Arith.thy 
3837  432 
"a:N ==> rec(a, inl(eq), %ka kb. inr(<ka, eq>)) : \ 
1459  433 
\ Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))" 
0  434 
(fn prems=> 
435 
[ (NE_tac "a" 1), 

1459  436 
(rtac PlusI_inr 3), 
437 
(rtac PlusI_inl 2), 

0  438 
eqintr_tac, 
439 
(equal_tac prems) ]); 

440 

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

442 
val prems = 

443 
goal Arith.thy "[ a:N; b:N ] ==> a mod b #+ (a div b) #* b = a : N"; 

444 
by (NE_tac "a" 1); 

445 
by (arith_rew_tac (div_typing_rls@prems@[modC0,modC_succ,divC0,divC_succ2])); 

1459  446 
by (rtac EqE 1); 
0  447 
(*case analysis on succ(u mod b)b *) 
448 
by (res_inst_tac [("a1", "succ(u mod b)  b")] 

449 
(iszero_decidable RS PlusE) 1); 

450 
by (etac SumE 3); 

451 
by (hyp_arith_rew_tac (prems @ div_typing_rls @ 

1459  452 
[modC0,modC_succ, divC0, divC_succ2])); 
0  453 
(*Replace one occurence of b by succ(u mod b). Clumsy!*) 
454 
by (resolve_tac [ add_typingL RS trans_elem ] 1); 

455 
by (eresolve_tac [EqE RS absdiff_eq0 RS sym_elem] 1); 

1459  456 
by (rtac refl_elem 3); 
0  457 
by (hyp_arith_rew_tac (prems @ div_typing_rls)); 
1294  458 
qed "mod_div_equality"; 
0  459 

460 
writeln"Reached end of file."; 