author | paulson |
Wed, 05 Jul 2000 17:42:06 +0200 | |
changeset 9249 | c71db8c28727 |
parent 3837 | d7f033c74b38 |
child 9251 | bd57acd44fc1 |
permissions | -rw-r--r-- |
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 |
val arith_defs = [add_def, diff_def, absdiff_def, mult_def, mod_def, div_def]; |
|
13 |
||
14 |
||
15 |
(** Addition *) |
|
16 |
||
17 |
(*typing of add: short and long versions*) |
|
18 |
||
9249 | 19 |
val prems= goalw Arith.thy arith_defs |
20 |
"[| a:N; b:N |] ==> a #+ b : N"; |
|
21 |
by (typechk_tac prems) ; |
|
22 |
qed "add_typing"; |
|
0 | 23 |
|
9249 | 24 |
val prems= goalw Arith.thy arith_defs |
25 |
"[| a=c:N; b=d:N |] ==> a #+ b = c #+ d : N"; |
|
26 |
by (equal_tac prems) ; |
|
27 |
qed "add_typingL"; |
|
0 | 28 |
|
29 |
||
30 |
(*computation for add: 0 and successor cases*) |
|
31 |
||
9249 | 32 |
val prems= goalw Arith.thy arith_defs |
33 |
"b:N ==> 0 #+ b = b : N"; |
|
34 |
by (rew_tac prems) ; |
|
35 |
qed "addC0"; |
|
0 | 36 |
|
9249 | 37 |
val prems= goalw Arith.thy arith_defs |
38 |
"[| a:N; b:N |] ==> succ(a) #+ b = succ(a #+ b) : N"; |
|
39 |
by (rew_tac prems) ; |
|
40 |
qed "addC_succ"; |
|
0 | 41 |
|
42 |
||
43 |
(** Multiplication *) |
|
44 |
||
45 |
(*typing of mult: short and long versions*) |
|
46 |
||
9249 | 47 |
val prems= goalw Arith.thy arith_defs |
48 |
"[| a:N; b:N |] ==> a #* b : N"; |
|
49 |
by (typechk_tac([add_typing]@prems)) ; |
|
50 |
qed "mult_typing"; |
|
0 | 51 |
|
9249 | 52 |
val prems= goalw Arith.thy arith_defs |
53 |
"[| a=c:N; b=d:N |] ==> a #* b = c #* d : N"; |
|
54 |
by (equal_tac (prems@[add_typingL])) ; |
|
55 |
qed "mult_typingL"; |
|
0 | 56 |
|
57 |
(*computation for mult: 0 and successor cases*) |
|
58 |
||
9249 | 59 |
val prems= goalw Arith.thy arith_defs |
60 |
"b:N ==> 0 #* b = 0 : N"; |
|
61 |
by (rew_tac prems) ; |
|
62 |
qed "multC0"; |
|
0 | 63 |
|
9249 | 64 |
val prems= goalw Arith.thy arith_defs |
65 |
"[| a:N; b:N |] ==> succ(a) #* b = b #+ (a #* b) : N"; |
|
66 |
by (rew_tac prems) ; |
|
67 |
qed "multC_succ"; |
|
0 | 68 |
|
69 |
||
70 |
(** Difference *) |
|
71 |
||
72 |
(*typing of difference*) |
|
73 |
||
9249 | 74 |
val prems= goalw Arith.thy arith_defs |
75 |
"[| a:N; b:N |] ==> a - b : N"; |
|
76 |
by (typechk_tac prems) ; |
|
77 |
qed "diff_typing"; |
|
0 | 78 |
|
9249 | 79 |
val prems= goalw Arith.thy arith_defs |
80 |
"[| a=c:N; b=d:N |] ==> a - b = c - d : N"; |
|
81 |
by (equal_tac prems) ; |
|
82 |
qed "diff_typingL"; |
|
0 | 83 |
|
84 |
||
85 |
||
86 |
(*computation for difference: 0 and successor cases*) |
|
87 |
||
9249 | 88 |
val prems= goalw Arith.thy arith_defs |
89 |
"a:N ==> a - 0 = a : N"; |
|
90 |
by (rew_tac prems) ; |
|
91 |
qed "diffC0"; |
|
0 | 92 |
|
93 |
(*Note: rec(a, 0, %z w.z) is pred(a). *) |
|
94 |
||
9249 | 95 |
val prems= goalw Arith.thy arith_defs |
96 |
"b:N ==> 0 - b = 0 : N"; |
|
97 |
by (NE_tac "b" 1); |
|
98 |
by (hyp_rew_tac prems) ; |
|
99 |
qed "diff_0_eq_0"; |
|
0 | 100 |
|
101 |
||
102 |
(*Essential to simplify FIRST!! (Else we get a critical pair) |
|
103 |
succ(a) - succ(b) rewrites to pred(succ(a) - b) *) |
|
9249 | 104 |
val prems= goalw Arith.thy arith_defs |
105 |
"[| a:N; b:N |] ==> succ(a) - succ(b) = a - b : N"; |
|
106 |
by (hyp_rew_tac prems); |
|
107 |
by (NE_tac "b" 1); |
|
108 |
by (hyp_rew_tac prems) ; |
|
109 |
qed "diff_succ_succ"; |
|
0 | 110 |
|
111 |
||
112 |
||
113 |
(*** Simplification *) |
|
114 |
||
115 |
val arith_typing_rls = |
|
116 |
[add_typing, mult_typing, diff_typing]; |
|
117 |
||
118 |
val arith_congr_rls = |
|
119 |
[add_typingL, mult_typingL, diff_typingL]; |
|
120 |
||
121 |
val congr_rls = arith_congr_rls@standard_congr_rls; |
|
122 |
||
123 |
val arithC_rls = |
|
124 |
[addC0, addC_succ, |
|
125 |
multC0, multC_succ, |
|
126 |
diffC0, diff_0_eq_0, diff_succ_succ]; |
|
127 |
||
128 |
||
129 |
structure Arith_simp_data: TSIMP_DATA = |
|
130 |
struct |
|
1459 | 131 |
val refl = refl_elem |
132 |
val sym = sym_elem |
|
133 |
val trans = trans_elem |
|
134 |
val refl_red = refl_red |
|
135 |
val trans_red = trans_red |
|
136 |
val red_if_equal = red_if_equal |
|
137 |
val default_rls = arithC_rls @ comp_rls |
|
138 |
val routine_tac = routine_tac (arith_typing_rls @ routine_rls) |
|
0 | 139 |
end; |
140 |
||
141 |
structure Arith_simp = TSimpFun (Arith_simp_data); |
|
142 |
||
143 |
fun arith_rew_tac prems = make_rew_tac |
|
144 |
(Arith_simp.norm_tac(congr_rls, prems)); |
|
145 |
||
146 |
fun hyp_arith_rew_tac prems = make_rew_tac |
|
147 |
(Arith_simp.cond_norm_tac(prove_cond_tac, congr_rls, prems)); |
|
148 |
||
149 |
||
150 |
(********** |
|
151 |
Addition |
|
152 |
**********) |
|
153 |
||
154 |
(*Associative law for addition*) |
|
9249 | 155 |
val prems= goal Arith.thy |
156 |
"[| a:N; b:N; c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N"; |
|
157 |
by (NE_tac "a" 1); |
|
158 |
by (hyp_arith_rew_tac prems) ; |
|
159 |
qed "add_assoc"; |
|
0 | 160 |
|
161 |
||
162 |
(*Commutative law for addition. Can be proved using three inductions. |
|
163 |
Must simplify after first induction! Orientation of rewrites is delicate*) |
|
9249 | 164 |
val prems= goal Arith.thy |
165 |
"[| a:N; b:N |] ==> a #+ b = b #+ a : N"; |
|
166 |
by (NE_tac "a" 1); |
|
167 |
by (hyp_arith_rew_tac prems); |
|
168 |
by (NE_tac "b" 2); |
|
169 |
by (rtac sym_elem 1); |
|
170 |
by (NE_tac "b" 1); |
|
171 |
by (hyp_arith_rew_tac prems) ; |
|
172 |
qed "add_commute"; |
|
0 | 173 |
|
174 |
||
175 |
(**************** |
|
176 |
Multiplication |
|
177 |
****************) |
|
178 |
||
179 |
(*Commutative law for multiplication |
|
9249 | 180 |
val prems= goal Arith.thy |
181 |
"[| a:N; b:N |] ==> a #* b = b #* a : N"; |
|
182 |
by (NE_tac "a" 1); |
|
183 |
by (hyp_arith_rew_tac prems); |
|
184 |
by (NE_tac "b" 2); |
|
185 |
by (rtac sym_elem 1); |
|
186 |
by (NE_tac "b" 1); |
|
187 |
by (hyp_arith_rew_tac prems) ; |
|
188 |
qed "mult_commute"; NEEDS COMMUTATIVE MATCHING |
|
0 | 189 |
***************) |
190 |
||
191 |
(*right annihilation in product*) |
|
9249 | 192 |
val prems= goal Arith.thy |
193 |
"a:N ==> a #* 0 = 0 : N"; |
|
194 |
by (NE_tac "a" 1); |
|
195 |
by (hyp_arith_rew_tac prems) ; |
|
196 |
qed "mult_0_right"; |
|
0 | 197 |
|
198 |
(*right successor law for multiplication*) |
|
9249 | 199 |
val prems= goal Arith.thy |
200 |
"[| a:N; b:N |] ==> a #* succ(b) = a #+ (a #* b) : N"; |
|
201 |
by (NE_tac "a" 1); |
|
202 |
by (hyp_arith_rew_tac (prems @ [add_assoc RS sym_elem])); |
|
203 |
by (REPEAT (assume_tac 1 ORELSE resolve_tac (prems@[add_commute,mult_typingL,add_typingL]@ intrL_rls@[refl_elem]) 1)) ; |
|
204 |
qed "mult_succ_right"; |
|
0 | 205 |
|
206 |
(*Commutative law for multiplication*) |
|
9249 | 207 |
val prems= goal Arith.thy |
208 |
"[| a:N; b:N |] ==> a #* b = b #* a : N"; |
|
209 |
by (NE_tac "a" 1); |
|
210 |
by (hyp_arith_rew_tac (prems @ [mult_0_right, mult_succ_right])) ; |
|
211 |
qed "mult_commute"; |
|
0 | 212 |
|
213 |
(*addition distributes over multiplication*) |
|
9249 | 214 |
val prems= goal Arith.thy |
215 |
"[| a:N; b:N; c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N"; |
|
216 |
by (NE_tac "a" 1); |
|
217 |
by (hyp_arith_rew_tac (prems @ [add_assoc RS sym_elem])) ; |
|
218 |
qed "add_mult_distrib"; |
|
0 | 219 |
|
220 |
||
221 |
(*Associative law for multiplication*) |
|
9249 | 222 |
val prems= goal Arith.thy |
223 |
"[| a:N; b:N; c:N |] ==> (a #* b) #* c = a #* (b #* c) : N"; |
|
224 |
by (NE_tac "a" 1); |
|
225 |
by (hyp_arith_rew_tac (prems @ [add_mult_distrib])) ; |
|
226 |
qed "mult_assoc"; |
|
0 | 227 |
|
228 |
||
229 |
(************ |
|
230 |
Difference |
|
231 |
************ |
|
232 |
||
233 |
Difference on natural numbers, without negative numbers |
|
234 |
a - b = 0 iff a<=b a - b = succ(c) iff a>b *) |
|
235 |
||
9249 | 236 |
val prems= goal Arith.thy |
237 |
"a:N ==> a - a = 0 : N"; |
|
238 |
by (NE_tac "a" 1); |
|
239 |
by (hyp_arith_rew_tac prems) ; |
|
240 |
qed "diff_self_eq_0"; |
|
0 | 241 |
|
242 |
||
243 |
(* [| c : N; 0 : N; c : N |] ==> c #+ 0 = c : N *) |
|
244 |
val add_0_right = addC0 RSN (3, add_commute RS trans_elem); |
|
245 |
||
246 |
(*Addition is the inverse of subtraction: if b<=x then b#+(x-b) = x. |
|
247 |
An example of induction over a quantified formula (a product). |
|
248 |
Uses rewriting with a quantified, implicative inductive hypothesis.*) |
|
249 |
val prems = |
|
250 |
goal Arith.thy |
|
251 |
"b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)"; |
|
252 |
by (NE_tac "b" 1); |
|
253 |
(*strip one "universal quantifier" but not the "implication"*) |
|
254 |
by (resolve_tac intr_rls 3); |
|
255 |
(*case analysis on x in |
|
256 |
(succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *) |
|
257 |
by (NE_tac "x" 4 THEN assume_tac 4); |
|
258 |
(*Prepare for simplification of types -- the antecedent succ(u)<=x *) |
|
1459 | 259 |
by (rtac replace_type 5); |
260 |
by (rtac replace_type 4); |
|
0 | 261 |
by (arith_rew_tac prems); |
262 |
(*Solves first 0 goal, simplifies others. Two sugbgoals remain. |
|
263 |
Both follow by rewriting, (2) using quantified induction hyp*) |
|
264 |
by (intr_tac[]); (*strips remaining PRODs*) |
|
265 |
by (hyp_arith_rew_tac (prems@[add_0_right])); |
|
266 |
by (assume_tac 1); |
|
1294 | 267 |
qed "add_diff_inverse_lemma"; |
0 | 268 |
|
269 |
||
270 |
(*Version of above with premise b-a=0 i.e. a >= b. |
|
271 |
Using ProdE does not work -- for ?B(?a) is ambiguous. |
|
272 |
Instead, add_diff_inverse_lemma states the desired induction scheme; |
|
273 |
the use of RS below instantiates Vars in ProdE automatically. *) |
|
274 |
val prems = |
|
275 |
goal Arith.thy "[| a:N; b:N; b-a = 0 : N |] ==> b #+ (a-b) = a : N"; |
|
1459 | 276 |
by (rtac EqE 1); |
0 | 277 |
by (resolve_tac [ add_diff_inverse_lemma RS ProdE RS ProdE ] 1); |
278 |
by (REPEAT (resolve_tac (prems@[EqI]) 1)); |
|
1294 | 279 |
qed "add_diff_inverse"; |
0 | 280 |
|
281 |
||
282 |
(******************** |
|
283 |
Absolute difference |
|
284 |
********************) |
|
285 |
||
286 |
(*typing of absolute difference: short and long versions*) |
|
287 |
||
9249 | 288 |
val prems= goalw Arith.thy arith_defs |
289 |
"[| a:N; b:N |] ==> a |-| b : N"; |
|
290 |
by (typechk_tac prems) ; |
|
291 |
qed "absdiff_typing"; |
|
0 | 292 |
|
9249 | 293 |
val prems= goalw Arith.thy arith_defs |
294 |
"[| a=c:N; b=d:N |] ==> a |-| b = c |-| d : N"; |
|
295 |
by (equal_tac prems) ; |
|
296 |
qed "absdiff_typingL"; |
|
0 | 297 |
|
9249 | 298 |
Goalw [absdiff_def] |
299 |
"a:N ==> a |-| a = 0 : N"; |
|
300 |
by (arith_rew_tac (prems@[diff_self_eq_0])) ; |
|
301 |
qed "absdiff_self_eq_0"; |
|
0 | 302 |
|
9249 | 303 |
Goalw [absdiff_def] |
304 |
"a:N ==> 0 |-| a = a : N"; |
|
305 |
by (hyp_arith_rew_tac []); |
|
306 |
qed "absdiffC0"; |
|
0 | 307 |
|
308 |
||
9249 | 309 |
Goalw [absdiff_def] |
310 |
"[| a:N; b:N |] ==> succ(a) |-| succ(b) = a |-| b : N"; |
|
311 |
by (hyp_arith_rew_tac []) ; |
|
312 |
qed "absdiff_succ_succ"; |
|
0 | 313 |
|
314 |
(*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
|
315 |
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
|
316 |
"[| a:N; b:N |] ==> a |-| b = b |-| a : N"; |
1459 | 317 |
by (rtac add_commute 1); |
0 | 318 |
by (typechk_tac ([diff_typing]@prems)); |
1294 | 319 |
qed "absdiff_commute"; |
0 | 320 |
|
321 |
(*If a+b=0 then a=0. Surprisingly tedious*) |
|
322 |
val prems = |
|
323 |
goal Arith.thy "[| a:N; b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)"; |
|
324 |
by (NE_tac "a" 1); |
|
1459 | 325 |
by (rtac replace_type 3); |
0 | 326 |
by (arith_rew_tac prems); |
327 |
by (intr_tac[]); (*strips remaining PRODs*) |
|
328 |
by (resolve_tac [ zero_ne_succ RS FE ] 2); |
|
329 |
by (etac (EqE RS sym_elem) 3); |
|
330 |
by (typechk_tac ([add_typing] @prems)); |
|
1294 | 331 |
qed "add_eq0_lemma"; |
0 | 332 |
|
333 |
(*Version of above with the premise a+b=0. |
|
334 |
Again, resolution instantiates variables in ProdE *) |
|
335 |
val prems = |
|
336 |
goal Arith.thy "[| a:N; b:N; a #+ b = 0 : N |] ==> a = 0 : N"; |
|
1459 | 337 |
by (rtac EqE 1); |
0 | 338 |
by (resolve_tac [add_eq0_lemma RS ProdE] 1); |
1459 | 339 |
by (rtac EqI 3); |
0 | 340 |
by (ALLGOALS (resolve_tac prems)); |
1294 | 341 |
qed "add_eq0"; |
0 | 342 |
|
343 |
(*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *) |
|
354
edf1ffedf139
CTT/Arith.ML: replaced many rewrite_goals_tac calls by prove_goalw
lcp
parents:
0
diff
changeset
|
344 |
val prems = goalw Arith.thy [absdiff_def] |
0 | 345 |
"[| a:N; b:N; a |-| b = 0 : N |] ==> \ |
346 |
\ ?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)"; |
|
347 |
by (intr_tac[]); |
|
348 |
by eqintr_tac; |
|
1459 | 349 |
by (rtac add_eq0 2); |
350 |
by (rtac add_eq0 1); |
|
0 | 351 |
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
|
352 |
by (typechk_tac (diff_typing::prems)); |
1294 | 353 |
qed "absdiff_eq0_lem"; |
0 | 354 |
|
355 |
(*if a |-| b = 0 then a = b |
|
356 |
proof: a-b=0 and b-a=0, so b = a+(b-a) = a+0 = a*) |
|
357 |
val prems = |
|
358 |
goal Arith.thy "[| a |-| b = 0 : N; a:N; b:N |] ==> a = b : N"; |
|
1459 | 359 |
by (rtac EqE 1); |
0 | 360 |
by (resolve_tac [absdiff_eq0_lem RS SumE] 1); |
361 |
by (TRYALL (resolve_tac prems)); |
|
362 |
by eqintr_tac; |
|
363 |
by (resolve_tac [add_diff_inverse RS sym_elem RS trans_elem] 1); |
|
1459 | 364 |
by (rtac EqE 3 THEN assume_tac 3); |
0 | 365 |
by (hyp_arith_rew_tac (prems@[add_0_right])); |
1294 | 366 |
qed "absdiff_eq0"; |
0 | 367 |
|
368 |
(*********************** |
|
369 |
Remainder and Quotient |
|
370 |
***********************) |
|
371 |
||
372 |
(*typing of remainder: short and long versions*) |
|
373 |
||
9249 | 374 |
Goalw [mod_def] |
375 |
"[| a:N; b:N |] ==> a mod b : N"; |
|
376 |
by (typechk_tac (absdiff_typing::prems)) ; |
|
377 |
qed "mod_typing"; |
|
0 | 378 |
|
9249 | 379 |
Goalw [mod_def] |
380 |
"[| a=c:N; b=d:N |] ==> a mod b = c mod d : N"; |
|
381 |
by (equal_tac [absdiff_typingL]) ; |
|
382 |
by (ALLGOALS assume_tac); |
|
383 |
qed "mod_typingL"; |
|
0 | 384 |
|
385 |
||
386 |
(*computation for mod : 0 and successor cases*) |
|
387 |
||
9249 | 388 |
Goalw [mod_def] "b:N ==> 0 mod b = 0 : N"; |
389 |
by (rew_tac(absdiff_typing::prems)) ; |
|
390 |
qed "modC0"; |
|
0 | 391 |
|
9249 | 392 |
Goalw [mod_def] |
393 |
"[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y. succ(a mod b)) : N"; |
|
394 |
by (rew_tac(absdiff_typing::prems)) ; |
|
395 |
qed "modC_succ"; |
|
0 | 396 |
|
397 |
||
398 |
(*typing of quotient: short and long versions*) |
|
399 |
||
9249 | 400 |
Goalw [div_def] "[| a:N; b:N |] ==> a div b : N"; |
401 |
by (typechk_tac ([absdiff_typing,mod_typing]@prems)) ; |
|
402 |
qed "div_typing"; |
|
0 | 403 |
|
9249 | 404 |
Goalw [div_def] |
405 |
"[| a=c:N; b=d:N |] ==> a div b = c div d : N"; |
|
406 |
by (equal_tac [absdiff_typingL, mod_typingL]); |
|
407 |
by (ALLGOALS assume_tac); |
|
408 |
qed "div_typingL"; |
|
0 | 409 |
|
410 |
val div_typing_rls = [mod_typing, div_typing, absdiff_typing]; |
|
411 |
||
412 |
||
413 |
(*computation for quotient: 0 and successor cases*) |
|
414 |
||
9249 | 415 |
Goalw [div_def] "b:N ==> 0 div b = 0 : N"; |
416 |
by (rew_tac([mod_typing, absdiff_typing] @ prems)) ; |
|
417 |
qed "divC0"; |
|
0 | 418 |
|
9249 | 419 |
Goalw [div_def] |
420 |
"[| a:N; b:N |] ==> succ(a) div b = \ |
|
421 |
\ rec(succ(a) mod b, succ(a div b), %x y. a div b) : N"; |
|
422 |
by (rew_tac([mod_typing]@prems)) ; |
|
423 |
qed "divC_succ"; |
|
0 | 424 |
|
425 |
||
426 |
(*Version of above with same condition as the mod one*) |
|
9249 | 427 |
val prems= goal Arith.thy |
0 | 428 |
"[| a:N; b:N |] ==> \ |
9249 | 429 |
\ succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N"; |
430 |
by (resolve_tac [ divC_succ RS trans_elem ] 1); |
|
431 |
by (rew_tac(div_typing_rls @ prems @ [modC_succ])); |
|
432 |
by (NE_tac "succ(a mod b)|-|b" 1); |
|
433 |
by (rew_tac ([mod_typing, div_typing, absdiff_typing] @prems)) ; |
|
434 |
qed "divC_succ2"; |
|
0 | 435 |
|
436 |
(*for case analysis on whether a number is 0 or a successor*) |
|
9249 | 437 |
val prems= goal Arith.thy |
3837 | 438 |
"a:N ==> rec(a, inl(eq), %ka kb. inr(<ka, eq>)) : \ |
9249 | 439 |
\ Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))"; |
440 |
by (NE_tac "a" 1); |
|
441 |
by (rtac PlusI_inr 3); |
|
442 |
by (rtac PlusI_inl 2); |
|
443 |
by eqintr_tac; |
|
444 |
by (equal_tac prems) ; |
|
445 |
qed "iszero_decidable"; |
|
0 | 446 |
|
447 |
(*Main Result. Holds when b is 0 since a mod 0 = a and a div 0 = 0 *) |
|
448 |
val prems = |
|
449 |
goal Arith.thy "[| a:N; b:N |] ==> a mod b #+ (a div b) #* b = a : N"; |
|
450 |
by (NE_tac "a" 1); |
|
451 |
by (arith_rew_tac (div_typing_rls@prems@[modC0,modC_succ,divC0,divC_succ2])); |
|
1459 | 452 |
by (rtac EqE 1); |
0 | 453 |
(*case analysis on succ(u mod b)|-|b *) |
454 |
by (res_inst_tac [("a1", "succ(u mod b) |-| b")] |
|
455 |
(iszero_decidable RS PlusE) 1); |
|
456 |
by (etac SumE 3); |
|
457 |
by (hyp_arith_rew_tac (prems @ div_typing_rls @ |
|
1459 | 458 |
[modC0,modC_succ, divC0, divC_succ2])); |
0 | 459 |
(*Replace one occurence of b by succ(u mod b). Clumsy!*) |
460 |
by (resolve_tac [ add_typingL RS trans_elem ] 1); |
|
461 |
by (eresolve_tac [EqE RS absdiff_eq0 RS sym_elem] 1); |
|
1459 | 462 |
by (rtac refl_elem 3); |
0 | 463 |
by (hyp_arith_rew_tac (prems @ div_typing_rls)); |
1294 | 464 |
qed "mod_div_equality"; |
0 | 465 |
|
466 |
writeln"Reached end of file."; |