author | paulson |
Mon, 29 Sep 1997 11:48:48 +0200 | |
changeset 3731 | 71366483323b |
parent 2469 | b50b8c0eec01 |
child 4091 | 771b1f6422a8 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/AC/recfunAC16.ML |
1196 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Krzysztof Grabczewski |
1196 | 4 |
|
5 |
Properties of the recursive definition used in the proof of WO2 ==> AC16 |
|
6 |
*) |
|
7 |
||
8 |
open recfunAC16; |
|
9 |
||
10 |
(* ********************************************************************** *) |
|
1461 | 11 |
(* Basic properties of recfunAC16 *) |
1196 | 12 |
(* ********************************************************************** *) |
13 |
||
14 |
goalw thy [recfunAC16_def] "recfunAC16(f,fa,0,a) = 0"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1196
diff
changeset
|
15 |
by (rtac transrec2_0 1); |
3731 | 16 |
qed "recfunAC16_0"; |
1196 | 17 |
|
18 |
goalw thy [recfunAC16_def] "recfunAC16(f,fa,succ(i),a) = \ |
|
19 |
\ if (EX y:recfunAC16(f,fa,i,a). fa ` i <= y, recfunAC16(f,fa,i,a), \ |
|
20 |
\ recfunAC16(f,fa,i,a) Un {f ` (LEAST j. fa ` i <= f ` j & \ |
|
1461 | 21 |
\ (ALL b<a. (fa`b <= f`j \ |
22 |
\ --> (ALL t:recfunAC16(f,fa,i,a). ~ fa`b <= t))))})"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1196
diff
changeset
|
23 |
by (rtac transrec2_succ 1); |
3731 | 24 |
qed "recfunAC16_succ"; |
1196 | 25 |
|
26 |
goalw thy [recfunAC16_def] "!!i. Limit(i) \ |
|
1461 | 27 |
\ ==> recfunAC16(f,fa,i,a) = (UN j<i. recfunAC16(f,fa,j,a))"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1196
diff
changeset
|
28 |
by (etac transrec2_Limit 1); |
3731 | 29 |
qed "recfunAC16_Limit"; |
1196 | 30 |
|
31 |
(* ********************************************************************** *) |
|
1461 | 32 |
(* Monotonicity of transrec2 *) |
1196 | 33 |
(* ********************************************************************** *) |
34 |
||
35 |
val [prem1, prem2] = goal thy |
|
2469 | 36 |
"[| !!g r. r <= B(g,r); Ord(i) |] \ |
1461 | 37 |
\ ==> j<i --> transrec2(j, 0, B) <= transrec2(i, 0, B)"; |
1196 | 38 |
by (resolve_tac [prem2 RS trans_induct] 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1196
diff
changeset
|
39 |
by (rtac Ord_cases 1 THEN (REPEAT (assume_tac 1))); |
2469 | 40 |
by (Fast_tac 1); |
41 |
by (Asm_simp_tac 1); |
|
1196 | 42 |
by (fast_tac (FOL_cs addSIs [succI1, prem1] |
1461 | 43 |
addSEs [ballE, leE, prem1 RSN (2, subset_trans)]) 1); |
2469 | 44 |
by (fast_tac (!claset addIs [OUN_I, ltI] |
1461 | 45 |
addSEs [Limit_has_succ RS ltE, succI1 RSN (2, Ord_in_Ord) RS le_refl, |
46 |
transrec2_Limit RS ssubst]) 1); |
|
3731 | 47 |
qed "transrec2_mono_lemma"; |
1196 | 48 |
|
49 |
val [prem1, prem2] = goal thy "[| !!g r. r <= B(g,r); j le i |] \ |
|
1461 | 50 |
\ ==> transrec2(j, 0, B) <= transrec2(i, 0, B)"; |
1196 | 51 |
by (resolve_tac [prem2 RS leE] 1); |
52 |
by (resolve_tac [transrec2_mono_lemma RS impE] 1); |
|
2469 | 53 |
by (TRYALL (fast_tac (!claset addSIs [prem1, prem2, lt_Ord2]))); |
3731 | 54 |
qed "transrec2_mono"; |
1196 | 55 |
|
56 |
(* ********************************************************************** *) |
|
1461 | 57 |
(* Monotonicity of recfunAC16 *) |
1196 | 58 |
(* ********************************************************************** *) |
59 |
||
60 |
goalw thy [recfunAC16_def] |
|
1461 | 61 |
"!!i. i le j ==> recfunAC16(f, g, i, a) <= recfunAC16(f, g, j, a)"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1196
diff
changeset
|
62 |
by (rtac transrec2_mono 1); |
2469 | 63 |
by (REPEAT (fast_tac (!claset addIs [expand_if RS iffD2]) 1)); |
3731 | 64 |
qed "recfunAC16_mono"; |
1196 | 65 |