1 (* Title: ZF/AC/recfunAC16.ML |
1 (* Title: ZF/AC/recfunAC16.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Krzysztof Grabczewski |
3 Author: Krzysztof Grabczewski |
4 |
4 |
5 Properties of the recursive definition used in the proof of WO2 ==> AC16 |
5 Properties of the recursive definition used in the proof of WO2 ==> AC16 |
6 *) |
6 *) |
7 |
7 |
8 open recfunAC16; |
8 open recfunAC16; |
9 |
9 |
10 (* ********************************************************************** *) |
10 (* ********************************************************************** *) |
11 (* Basic properties of recfunAC16 *) |
11 (* Basic properties of recfunAC16 *) |
12 (* ********************************************************************** *) |
12 (* ********************************************************************** *) |
13 |
13 |
14 goalw thy [recfunAC16_def] "recfunAC16(f,fa,0,a) = 0"; |
14 goalw thy [recfunAC16_def] "recfunAC16(f,fa,0,a) = 0"; |
15 by (rtac transrec2_0 1); |
15 by (rtac transrec2_0 1); |
16 val recfunAC16_0 = result(); |
16 val recfunAC16_0 = result(); |
17 |
17 |
18 goalw thy [recfunAC16_def] "recfunAC16(f,fa,succ(i),a) = \ |
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), \ |
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 & \ |
20 \ recfunAC16(f,fa,i,a) Un {f ` (LEAST j. fa ` i <= f ` j & \ |
21 \ (ALL b<a. (fa`b <= f`j \ |
21 \ (ALL b<a. (fa`b <= f`j \ |
22 \ --> (ALL t:recfunAC16(f,fa,i,a). ~ fa`b <= t))))})"; |
22 \ --> (ALL t:recfunAC16(f,fa,i,a). ~ fa`b <= t))))})"; |
23 by (rtac transrec2_succ 1); |
23 by (rtac transrec2_succ 1); |
24 val recfunAC16_succ = result(); |
24 val recfunAC16_succ = result(); |
25 |
25 |
26 goalw thy [recfunAC16_def] "!!i. Limit(i) \ |
26 goalw thy [recfunAC16_def] "!!i. Limit(i) \ |
27 \ ==> recfunAC16(f,fa,i,a) = (UN j<i. recfunAC16(f,fa,j,a))"; |
27 \ ==> recfunAC16(f,fa,i,a) = (UN j<i. recfunAC16(f,fa,j,a))"; |
28 by (etac transrec2_Limit 1); |
28 by (etac transrec2_Limit 1); |
29 val recfunAC16_Limit = result(); |
29 val recfunAC16_Limit = result(); |
30 |
30 |
31 (* ********************************************************************** *) |
31 (* ********************************************************************** *) |
32 (* Monotonicity of transrec2 *) |
32 (* Monotonicity of transrec2 *) |
33 (* ********************************************************************** *) |
33 (* ********************************************************************** *) |
34 |
34 |
35 val [prem1, prem2] = goal thy |
35 val [prem1, prem2] = goal thy |
36 "[| !!g r. r <= B(g,r); Ord(i) |] \ |
36 "[| !!g r. r <= B(g,r); Ord(i) |] \ |
37 \ ==> j<i --> transrec2(j, 0, B) <= transrec2(i, 0, B)"; |
37 \ ==> j<i --> transrec2(j, 0, B) <= transrec2(i, 0, B)"; |
38 by (resolve_tac [prem2 RS trans_induct] 1); |
38 by (resolve_tac [prem2 RS trans_induct] 1); |
39 by (rtac Ord_cases 1 THEN (REPEAT (assume_tac 1))); |
39 by (rtac Ord_cases 1 THEN (REPEAT (assume_tac 1))); |
40 by (fast_tac lt_cs 1); |
40 by (fast_tac lt_cs 1); |
41 by (asm_simp_tac (AC_ss addsimps [transrec2_succ]) 1); |
41 by (asm_simp_tac (AC_ss addsimps [transrec2_succ]) 1); |
42 by (fast_tac (FOL_cs addSIs [succI1, prem1] |
42 by (fast_tac (FOL_cs addSIs [succI1, prem1] |
43 addSEs [ballE, leE, prem1 RSN (2, subset_trans)]) 1); |
43 addSEs [ballE, leE, prem1 RSN (2, subset_trans)]) 1); |
44 by (fast_tac (AC_cs addIs [OUN_I, ltI] |
44 by (fast_tac (AC_cs addIs [OUN_I, ltI] |
45 addSEs [Limit_has_succ RS ltE, succI1 RSN (2, Ord_in_Ord) RS le_refl, |
45 addSEs [Limit_has_succ RS ltE, succI1 RSN (2, Ord_in_Ord) RS le_refl, |
46 transrec2_Limit RS ssubst]) 1); |
46 transrec2_Limit RS ssubst]) 1); |
47 val transrec2_mono_lemma = result(); |
47 val transrec2_mono_lemma = result(); |
48 |
48 |
49 val [prem1, prem2] = goal thy "[| !!g r. r <= B(g,r); j le i |] \ |
49 val [prem1, prem2] = goal thy "[| !!g r. r <= B(g,r); j le i |] \ |
50 \ ==> transrec2(j, 0, B) <= transrec2(i, 0, B)"; |
50 \ ==> transrec2(j, 0, B) <= transrec2(i, 0, B)"; |
51 by (resolve_tac [prem2 RS leE] 1); |
51 by (resolve_tac [prem2 RS leE] 1); |
52 by (resolve_tac [transrec2_mono_lemma RS impE] 1); |
52 by (resolve_tac [transrec2_mono_lemma RS impE] 1); |
53 by (TRYALL (fast_tac (AC_cs addSIs [prem1, prem2, lt_Ord2]))); |
53 by (TRYALL (fast_tac (AC_cs addSIs [prem1, prem2, lt_Ord2]))); |
54 val transrec2_mono = result(); |
54 val transrec2_mono = result(); |
55 |
55 |
56 (* ********************************************************************** *) |
56 (* ********************************************************************** *) |
57 (* Monotonicity of recfunAC16 *) |
57 (* Monotonicity of recfunAC16 *) |
58 (* ********************************************************************** *) |
58 (* ********************************************************************** *) |
59 |
59 |
60 goalw thy [recfunAC16_def] |
60 goalw thy [recfunAC16_def] |
61 "!!i. i le j ==> recfunAC16(f, g, i, a) <= recfunAC16(f, g, j, a)"; |
61 "!!i. i le j ==> recfunAC16(f, g, i, a) <= recfunAC16(f, g, j, a)"; |
62 by (rtac transrec2_mono 1); |
62 by (rtac transrec2_mono 1); |
63 by (REPEAT (fast_tac (AC_cs addIs [expand_if RS iffD2]) 1)); |
63 by (REPEAT (fast_tac (AC_cs addIs [expand_if RS iffD2]) 1)); |
64 val recfunAC16_mono = result(); |
64 val recfunAC16_mono = result(); |
65 |
65 |