992
|
1 |
(* Title: ZF/AC/Transrec2.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Krzysztof Gr`abczewski
|
|
4 |
|
|
5 |
Transfinite recursion introduced to handle definitions based on the three
|
|
6 |
cases of ordinals.
|
|
7 |
*)
|
|
8 |
|
|
9 |
open Transrec2;
|
|
10 |
|
|
11 |
val AC_cs = OrdQuant_cs;
|
|
12 |
val AC_ss = OrdQuant_ss;
|
|
13 |
|
|
14 |
goal thy "transrec2(0,a,b) = a";
|
|
15 |
by (rtac (transrec2_def RS def_transrec RS trans) 1);
|
|
16 |
by (simp_tac ZF_ss 1);
|
|
17 |
val transrec2_0 = result();
|
|
18 |
|
|
19 |
goal thy "(THE j. succ(i)=succ(j)) = i";
|
|
20 |
by (fast_tac (AC_cs addSIs [the_equality]) 1);
|
|
21 |
val THE_succ_eq = result();
|
|
22 |
|
|
23 |
goal thy "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))";
|
|
24 |
by (rtac (transrec2_def RS def_transrec RS trans) 1);
|
|
25 |
by (simp_tac (ZF_ss addsimps [succ_not_0, THE_succ_eq, if_P]
|
|
26 |
setsolver K (fast_tac FOL_cs)) 1);
|
|
27 |
val transrec2_succ = result();
|
|
28 |
|
|
29 |
goal thy "!!i. Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))";
|
|
30 |
by (rtac (transrec2_def RS def_transrec RS trans) 1);
|
|
31 |
by (resolve_tac [if_not_P RS trans] 1 THEN
|
|
32 |
fast_tac (AC_cs addSDs [Limit_has_0] addSEs [ltE]) 1);
|
|
33 |
by (resolve_tac [if_not_P RS trans] 1 THEN
|
|
34 |
fast_tac (AC_cs addSEs [succ_LimitE]) 1);
|
|
35 |
by (simp_tac AC_ss 1);
|
|
36 |
val transrec2_Limit = result();
|