--- a/src/ZF/Epsilon.ML Sat May 18 20:08:17 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,363 +0,0 @@
-(* Title: ZF/epsilon.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-Epsilon induction and recursion
-*)
-
-(*** Basic closure properties ***)
-
-Goalw [eclose_def] "A <= eclose(A)";
-by (rtac (nat_rec_0 RS equalityD2 RS subset_trans) 1);
-by (rtac (nat_0I RS UN_upper) 1);
-qed "arg_subset_eclose";
-
-bind_thm ("arg_into_eclose", arg_subset_eclose RS subsetD);
-
-Goalw [eclose_def,Transset_def] "Transset(eclose(A))";
-by (rtac (subsetI RS ballI) 1);
-by (etac UN_E 1);
-by (rtac (nat_succI RS UN_I) 1);
-by (assume_tac 1);
-by (etac (nat_rec_succ RS ssubst) 1);
-by (etac UnionI 1);
-by (assume_tac 1);
-qed "Transset_eclose";
-
-(* x : eclose(A) ==> x <= eclose(A) *)
-bind_thm ("eclose_subset",
- rewrite_rule [Transset_def] Transset_eclose RS bspec);
-
-(* [| A : eclose(B); c : A |] ==> c : eclose(B) *)
-bind_thm ("ecloseD", eclose_subset RS subsetD);
-
-bind_thm ("arg_in_eclose_sing", arg_subset_eclose RS singleton_subsetD);
-bind_thm ("arg_into_eclose_sing", arg_in_eclose_sing RS ecloseD);
-
-(* This is epsilon-induction for eclose(A); see also eclose_induct_down...
- [| a: eclose(A); !!x. [| x: eclose(A); ALL y:x. P(y) |] ==> P(x)
- |] ==> P(a)
-*)
-bind_thm ("eclose_induct", Transset_eclose RSN (2, Transset_induct));
-
-(*Epsilon induction*)
-val prems = Goal
- "[| !!x. ALL y:x. P(y) ==> P(x) |] ==> P(a)";
-by (rtac (arg_in_eclose_sing RS eclose_induct) 1);
-by (eresolve_tac prems 1);
-qed "eps_induct";
-
-(*Perform epsilon-induction on i. *)
-fun eps_ind_tac a =
- EVERY' [res_inst_tac [("a",a)] eps_induct,
- rename_last_tac a ["1"]];
-
-
-(*** Leastness of eclose ***)
-
-(** eclose(A) is the least transitive set including A as a subset. **)
-
-Goalw [Transset_def]
- "[| Transset(X); A<=X; n: nat |] ==> \
-\ nat_rec(n, A, %m r. Union(r)) <= X";
-by (etac nat_induct 1);
-by (asm_simp_tac (simpset() addsimps [nat_rec_0]) 1);
-by (asm_simp_tac (simpset() addsimps [nat_rec_succ]) 1);
-by (Blast_tac 1);
-qed "eclose_least_lemma";
-
-Goalw [eclose_def]
- "[| Transset(X); A<=X |] ==> eclose(A) <= X";
-by (rtac (eclose_least_lemma RS UN_least) 1);
-by (REPEAT (assume_tac 1));
-qed "eclose_least";
-
-(*COMPLETELY DIFFERENT induction principle from eclose_induct!!*)
-val [major,base,step] = Goal
- "[| a: eclose(b); \
-\ !!y. [| y: b |] ==> P(y); \
-\ !!y z. [| y: eclose(b); P(y); z: y |] ==> P(z) \
-\ |] ==> P(a)";
-by (rtac (major RSN (3, eclose_least RS subsetD RS CollectD2)) 1);
-by (rtac (CollectI RS subsetI) 2);
-by (etac (arg_subset_eclose RS subsetD) 2);
-by (etac base 2);
-by (rewtac Transset_def);
-by (blast_tac (claset() addIs [step,ecloseD]) 1);
-qed "eclose_induct_down";
-
-Goal "Transset(X) ==> eclose(X) = X";
-by (etac ([eclose_least, arg_subset_eclose] MRS equalityI) 1);
-by (rtac subset_refl 1);
-qed "Transset_eclose_eq_arg";
-
-
-(*** Epsilon recursion ***)
-
-(*Unused...*)
-Goal "[| A: eclose(B); B: eclose(C) |] ==> A: eclose(C)";
-by (rtac ([Transset_eclose, eclose_subset] MRS eclose_least RS subsetD) 1);
-by (REPEAT (assume_tac 1));
-qed "mem_eclose_trans";
-
-(*Variant of the previous lemma in a useable form for the sequel*)
-Goal "[| A: eclose({B}); B: eclose({C}) |] ==> A: eclose({C})";
-by (rtac ([Transset_eclose, singleton_subsetI] MRS eclose_least RS subsetD) 1);
-by (REPEAT (assume_tac 1));
-qed "mem_eclose_sing_trans";
-
-Goalw [Transset_def] "[| Transset(i); j:i |] ==> Memrel(i)-``{j} = j";
-by (Blast_tac 1);
-qed "under_Memrel";
-
-(* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)
-bind_thm ("under_Memrel_eclose", Transset_eclose RS under_Memrel);
-
-bind_thm ("wfrec_ssubst", standard (wf_Memrel RS wfrec RS ssubst));
-
-val [kmemj,jmemi] = goal (the_context ())
- "[| k:eclose({j}); j:eclose({i}) |] ==> \
-\ wfrec(Memrel(eclose({i})), k, H) = wfrec(Memrel(eclose({j})), k, H)";
-by (rtac (kmemj RS eclose_induct) 1);
-by (rtac wfrec_ssubst 1);
-by (rtac wfrec_ssubst 1);
-by (asm_simp_tac (simpset() addsimps [under_Memrel_eclose,
- jmemi RSN (2,mem_eclose_sing_trans)]) 1);
-qed "wfrec_eclose_eq";
-
-Goal
- "k: i ==> wfrec(Memrel(eclose({i})),k,H) = wfrec(Memrel(eclose({k})),k,H)";
-by (rtac (arg_in_eclose_sing RS wfrec_eclose_eq) 1);
-by (etac arg_into_eclose_sing 1);
-qed "wfrec_eclose_eq2";
-
-Goalw [transrec_def]
- "transrec(a,H) = H(a, lam x:a. transrec(x,H))";
-by (rtac wfrec_ssubst 1);
-by (simp_tac (simpset() addsimps [wfrec_eclose_eq2, arg_in_eclose_sing,
- under_Memrel_eclose]) 1);
-qed "transrec";
-
-(*Avoids explosions in proofs; resolve it with a meta-level definition.*)
-val rew::prems = Goal
- "[| !!x. f(x)==transrec(x,H) |] ==> f(a) = H(a, lam x:a. f(x))";
-by (rewtac rew);
-by (REPEAT (resolve_tac (prems@[transrec]) 1));
-qed "def_transrec";
-
-val prems = Goal
- "[| !!x u. [| x:eclose({a}); u: Pi(x,B) |] ==> H(x,u) : B(x) \
-\ |] ==> transrec(a,H) : B(a)";
-by (res_inst_tac [("i", "a")] (arg_in_eclose_sing RS eclose_induct) 1);
-by (stac transrec 1);
-by (REPEAT (ares_tac (prems @ [lam_type]) 1 ORELSE etac bspec 1));
-qed "transrec_type";
-
-Goal "Ord(i) ==> eclose({i}) <= succ(i)";
-by (etac (Ord_is_Transset RS Transset_succ RS eclose_least) 1);
-by (rtac (succI1 RS singleton_subsetI) 1);
-qed "eclose_sing_Ord";
-
-val prems = Goal
- "[| j: i; Ord(i); \
-\ !!x u. [| x: i; u: Pi(x,B) |] ==> H(x,u) : B(x) \
-\ |] ==> transrec(j,H) : B(j)";
-by (rtac transrec_type 1);
-by (resolve_tac prems 1);
-by (rtac (Ord_in_Ord RS eclose_sing_Ord RS subsetD RS succE) 1);
-by (DEPTH_SOLVE (ares_tac prems 1 ORELSE eresolve_tac [ssubst,Ord_trans] 1));
-qed "Ord_transrec_type";
-
-(*** Rank ***)
-
-(*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
-Goal "rank(a) = (UN y:a. succ(rank(y)))";
-by (stac (rank_def RS def_transrec) 1);
-by (Simp_tac 1);
-qed "rank";
-
-Goal "Ord(rank(a))";
-by (eps_ind_tac "a" 1);
-by (stac rank 1);
-by (rtac (Ord_succ RS Ord_UN) 1);
-by (etac bspec 1);
-by (assume_tac 1);
-qed "Ord_rank";
-Addsimps [Ord_rank];
-
-Goal "Ord(i) ==> rank(i) = i";
-by (etac trans_induct 1);
-by (stac rank 1);
-by (asm_simp_tac (simpset() addsimps [Ord_equality]) 1);
-qed "rank_of_Ord";
-
-Goal "a:b ==> rank(a) < rank(b)";
-by (res_inst_tac [("a1","b")] (rank RS ssubst) 1);
-by (etac (UN_I RS ltI) 1);
-by (rtac Ord_UN 2);
-by Auto_tac;
-qed "rank_lt";
-
-Goal "a: eclose(b) ==> rank(a) < rank(b)";
-by (etac eclose_induct_down 1);
-by (etac rank_lt 1);
-by (etac (rank_lt RS lt_trans) 1);
-by (assume_tac 1);
-qed "eclose_rank_lt";
-
-Goal "a<=b ==> rank(a) le rank(b)";
-by (rtac subset_imp_le 1);
-by (stac rank 1);
-by (stac rank 1);
-by Auto_tac;
-qed "rank_mono";
-
-Goal "rank(Pow(a)) = succ(rank(a))";
-by (rtac (rank RS trans) 1);
-by (rtac le_anti_sym 1);
-by (rtac UN_upper_le 2);
-by (rtac UN_least_le 1);
-by (auto_tac (claset() addIs [rank_mono], simpset() addsimps [Ord_UN]));
-qed "rank_Pow";
-
-Goal "rank(0) = 0";
-by (rtac (rank RS trans) 1);
-by (Blast_tac 1);
-qed "rank_0";
-
-Goal "rank(succ(x)) = succ(rank(x))";
-by (rtac (rank RS trans) 1);
-by (rtac ([UN_least, succI1 RS UN_upper] MRS equalityI) 1);
-by (etac succE 1);
-by (Blast_tac 1);
-by (etac (rank_lt RS leI RS succ_leI RS le_imp_subset) 1);
-qed "rank_succ";
-Addsimps [rank_0, rank_succ];
-
-Goal "rank(Union(A)) = (UN x:A. rank(x))";
-by (rtac equalityI 1);
-by (rtac (rank_mono RS le_imp_subset RS UN_least) 2);
-by (etac Union_upper 2);
-by (stac rank 1);
-by (rtac UN_least 1);
-by (etac UnionE 1);
-by (rtac subset_trans 1);
-by (etac (RepFunI RS Union_upper) 2);
-by (etac (rank_lt RS succ_leI RS le_imp_subset) 1);
-qed "rank_Union";
-
-Goal "rank(eclose(a)) = rank(a)";
-by (rtac le_anti_sym 1);
-by (rtac (arg_subset_eclose RS rank_mono) 2);
-by (res_inst_tac [("a1","eclose(a)")] (rank RS ssubst) 1);
-by (rtac (Ord_rank RS UN_least_le) 1);
-by (etac (eclose_rank_lt RS succ_leI) 1);
-qed "rank_eclose";
-
-Goalw [Pair_def] "rank(a) < rank(<a,b>)";
-by (rtac (consI1 RS rank_lt RS lt_trans) 1);
-by (rtac (consI1 RS consI2 RS rank_lt) 1);
-qed "rank_pair1";
-
-Goalw [Pair_def] "rank(b) < rank(<a,b>)";
-by (rtac (consI1 RS consI2 RS rank_lt RS lt_trans) 1);
-by (rtac (consI1 RS consI2 RS rank_lt) 1);
-qed "rank_pair2";
-
-(*Not clear how to remove the P(a) condition, since the "then" part
- must refer to "a"*)
-Goal "P(a) ==> (THE x. P(x)) = (if (EX!x. P(x)) then a else 0)";
-by (asm_simp_tac (simpset() addsimps [the_0, the_equality2]) 1);
-qed "the_equality_if";
-
-(*The premise is needed not just to fix i but to ensure f~=0*)
-Goalw [apply_def] "i : domain(f) ==> rank(f`i) < rank(f)";
-by (Clarify_tac 1);
-by (subgoal_tac "rank(y) < rank(f)" 1);
-by (blast_tac (claset() addIs [lt_trans, rank_lt, rank_pair2]) 2);
-by (subgoal_tac "0 < rank(f)" 1);
-by (etac (Ord_rank RS Ord_0_le RS lt_trans1) 2);
-by (asm_simp_tac (simpset() addsimps [the_equality_if]) 1);
-qed "rank_apply";
-
-
-(*** Corollaries of leastness ***)
-
-Goal "A:B ==> eclose(A)<=eclose(B)";
-by (rtac (Transset_eclose RS eclose_least) 1);
-by (etac (arg_into_eclose RS eclose_subset) 1);
-qed "mem_eclose_subset";
-
-Goal "A<=B ==> eclose(A) <= eclose(B)";
-by (rtac (Transset_eclose RS eclose_least) 1);
-by (etac subset_trans 1);
-by (rtac arg_subset_eclose 1);
-qed "eclose_mono";
-
-(** Idempotence of eclose **)
-
-Goal "eclose(eclose(A)) = eclose(A)";
-by (rtac equalityI 1);
-by (rtac ([Transset_eclose, subset_refl] MRS eclose_least) 1);
-by (rtac arg_subset_eclose 1);
-qed "eclose_idem";
-
-(** Transfinite recursion for definitions based on the
- three cases of ordinals **)
-
-Goal "transrec2(0,a,b) = a";
-by (rtac (transrec2_def RS def_transrec RS trans) 1);
-by (Simp_tac 1);
-qed "transrec2_0";
-
-Goal "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))";
-by (rtac (transrec2_def RS def_transrec RS trans) 1);
-by (simp_tac (simpset() addsimps [the_equality, if_P]) 1);
-qed "transrec2_succ";
-
-Goal "Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))";
-by (rtac (transrec2_def RS def_transrec RS trans) 1);
-by (Simp_tac 1);
-by (blast_tac (claset() addSDs [Limit_has_0] addSEs [succ_LimitE]) 1);
-qed "transrec2_Limit";
-
-Addsimps [transrec2_0, transrec2_succ];
-
-
-(** recursor -- better than nat_rec; the succ case has no type requirement! **)
-
-(*NOT suitable for rewriting*)
-val lemma = recursor_def RS def_transrec RS trans;
-
-Goal "recursor(a,b,0) = a";
-by (rtac (nat_case_0 RS lemma) 1);
-qed "recursor_0";
-
-Goal "recursor(a,b,succ(m)) = b(m, recursor(a,b,m))";
-by (rtac lemma 1);
-by (Simp_tac 1);
-qed "recursor_succ";
-
-
-(** rec: old version for compatibility **)
-
-Goalw [rec_def] "rec(0,a,b) = a";
-by (rtac recursor_0 1);
-qed "rec_0";
-
-Goalw [rec_def] "rec(succ(m),a,b) = b(m, rec(m,a,b))";
-by (rtac recursor_succ 1);
-qed "rec_succ";
-
-Addsimps [rec_0, rec_succ];
-
-val major::prems = Goal
- "[| n: nat; \
-\ a: C(0); \
-\ !!m z. [| m: nat; z: C(m) |] ==> b(m,z): C(succ(m)) \
-\ |] ==> rec(n,a,b) : C(n)";
-by (rtac (major RS nat_induct) 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
-qed "rec_type";
-
--- a/src/ZF/Epsilon.thy Sat May 18 20:08:17 2002 +0200
+++ b/src/ZF/Epsilon.thy Sat May 18 22:22:23 2002 +0200
@@ -6,18 +6,19 @@
Epsilon induction and recursion
*)
-Epsilon = Nat + mono +
+theory Epsilon = Nat + mono:
+
constdefs
- eclose :: i=>i
+ eclose :: "i=>i"
"eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"
- transrec :: [i, [i,i]=>i] =>i
+ transrec :: "[i, [i,i]=>i] =>i"
"transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)"
- rank :: i=>i
+ rank :: "i=>i"
"rank(a) == transrec(a, %x f. UN y:x. succ(f`y))"
- transrec2 :: [i, i, [i,i]=>i] =>i
+ transrec2 :: "[i, i, [i,i]=>i] =>i"
"transrec2(k, a, b) ==
transrec(k,
%i r. if(i=0, a,
@@ -25,10 +26,394 @@
b(THE j. i=succ(j), r`(THE j. i=succ(j))),
UN j<i. r`j)))"
- recursor :: [i, [i,i]=>i, i]=>i
- "recursor(a,b,k) == transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
+ recursor :: "[i, [i,i]=>i, i]=>i"
+ "recursor(a,b,k) == transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
+
+ rec :: "[i, i, [i,i]=>i]=>i"
+ "rec(k,a,b) == recursor(a,b,k)"
+
+
+(*** Basic closure properties ***)
+
+lemma arg_subset_eclose: "A <= eclose(A)"
+apply (unfold eclose_def)
+apply (rule nat_rec_0 [THEN equalityD2, THEN subset_trans])
+apply (rule nat_0I [THEN UN_upper])
+done
+
+lemmas arg_into_eclose = arg_subset_eclose [THEN subsetD, standard]
+
+lemma Transset_eclose: "Transset(eclose(A))"
+apply (unfold eclose_def Transset_def)
+apply (rule subsetI [THEN ballI])
+apply (erule UN_E)
+apply (rule nat_succI [THEN UN_I], assumption)
+apply (erule nat_rec_succ [THEN ssubst])
+apply (erule UnionI, assumption)
+done
+
+(* x : eclose(A) ==> x <= eclose(A) *)
+lemmas eclose_subset =
+ Transset_eclose [unfolded Transset_def, THEN bspec, standard]
+
+(* [| A : eclose(B); c : A |] ==> c : eclose(B) *)
+lemmas ecloseD = eclose_subset [THEN subsetD, standard]
+
+lemmas arg_in_eclose_sing = arg_subset_eclose [THEN singleton_subsetD]
+lemmas arg_into_eclose_sing = arg_in_eclose_sing [THEN ecloseD, standard]
+
+(* This is epsilon-induction for eclose(A); see also eclose_induct_down...
+ [| a: eclose(A); !!x. [| x: eclose(A); ALL y:x. P(y) |] ==> P(x)
+ |] ==> P(a)
+*)
+lemmas eclose_induct = Transset_induct [OF _ Transset_eclose]
+
+(*Epsilon induction*)
+lemma eps_induct:
+ "[| !!x. ALL y:x. P(y) ==> P(x) |] ==> P(a)"
+by (rule arg_in_eclose_sing [THEN eclose_induct], blast)
+
+
+(*** Leastness of eclose ***)
+
+(** eclose(A) is the least transitive set including A as a subset. **)
+
+lemma eclose_least_lemma:
+ "[| Transset(X); A<=X; n: nat |] ==> nat_rec(n, A, %m r. Union(r)) <= X"
+apply (unfold Transset_def)
+apply (erule nat_induct)
+apply (simp add: nat_rec_0)
+apply (simp add: nat_rec_succ, blast)
+done
+
+lemma eclose_least:
+ "[| Transset(X); A<=X |] ==> eclose(A) <= X"
+apply (unfold eclose_def)
+apply (rule eclose_least_lemma [THEN UN_least], assumption+)
+done
+
+(*COMPLETELY DIFFERENT induction principle from eclose_induct!!*)
+lemma eclose_induct_down:
+ "[| a: eclose(b);
+ !!y. [| y: b |] ==> P(y);
+ !!y z. [| y: eclose(b); P(y); z: y |] ==> P(z)
+ |] ==> P(a)"
+apply (rule eclose_least [THEN subsetD, THEN CollectD2, of "eclose(b)"])
+ prefer 3 apply assumption
+ apply (unfold Transset_def)
+ apply (blast intro: ecloseD)
+apply (blast intro: arg_subset_eclose [THEN subsetD])
+done
+
+lemma Transset_eclose_eq_arg: "Transset(X) ==> eclose(X) = X"
+apply (erule equalityI [OF eclose_least arg_subset_eclose])
+apply (rule subset_refl)
+done
+
+
+(*** Epsilon recursion ***)
+
+(*Unused...*)
+lemma mem_eclose_trans: "[| A: eclose(B); B: eclose(C) |] ==> A: eclose(C)"
+by (rule eclose_least [OF Transset_eclose eclose_subset, THEN subsetD],
+ assumption+)
+
+(*Variant of the previous lemma in a useable form for the sequel*)
+lemma mem_eclose_sing_trans:
+ "[| A: eclose({B}); B: eclose({C}) |] ==> A: eclose({C})"
+by (rule eclose_least [OF Transset_eclose singleton_subsetI, THEN subsetD],
+ assumption+)
+
+lemma under_Memrel: "[| Transset(i); j:i |] ==> Memrel(i)-``{j} = j"
+by (unfold Transset_def, blast)
+
+(* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)
+lemmas under_Memrel_eclose = Transset_eclose [THEN under_Memrel, standard]
+
+lemmas wfrec_ssubst = wf_Memrel [THEN wfrec, THEN ssubst]
+
+lemma wfrec_eclose_eq:
+ "[| k:eclose({j}); j:eclose({i}) |] ==>
+ wfrec(Memrel(eclose({i})), k, H) = wfrec(Memrel(eclose({j})), k, H)"
+apply (erule eclose_induct)
+apply (rule wfrec_ssubst)
+apply (rule wfrec_ssubst)
+apply (simp add: under_Memrel_eclose mem_eclose_sing_trans [of _ j i])
+done
+
+lemma wfrec_eclose_eq2:
+ "k: i ==> wfrec(Memrel(eclose({i})),k,H) = wfrec(Memrel(eclose({k})),k,H)"
+apply (rule arg_in_eclose_sing [THEN wfrec_eclose_eq])
+apply (erule arg_into_eclose_sing)
+done
+
+lemma transrec: "transrec(a,H) = H(a, lam x:a. transrec(x,H))"
+apply (unfold transrec_def)
+apply (rule wfrec_ssubst)
+apply (simp add: wfrec_eclose_eq2 arg_in_eclose_sing under_Memrel_eclose)
+done
+
+(*Avoids explosions in proofs; resolve it with a meta-level definition.*)
+lemma def_transrec:
+ "[| !!x. f(x)==transrec(x,H) |] ==> f(a) = H(a, lam x:a. f(x))"
+apply simp
+apply (rule transrec)
+done
+
+lemma transrec_type:
+ "[| !!x u. [| x:eclose({a}); u: Pi(x,B) |] ==> H(x,u) : B(x) |]
+ ==> transrec(a,H) : B(a)"
+apply (rule_tac i = "a" in arg_in_eclose_sing [THEN eclose_induct])
+apply (subst transrec)
+apply (simp add: lam_type)
+done
+
+lemma eclose_sing_Ord: "Ord(i) ==> eclose({i}) <= succ(i)"
+apply (erule Ord_is_Transset [THEN Transset_succ, THEN eclose_least])
+apply (rule succI1 [THEN singleton_subsetI])
+done
+
+lemma Ord_transrec_type:
+ assumes jini: "j: i"
+ and ordi: "Ord(i)"
+ and minor: " !!x u. [| x: i; u: Pi(x,B) |] ==> H(x,u) : B(x)"
+ shows "transrec(j,H) : B(j)"
+apply (rule transrec_type)
+apply (insert jini ordi)
+apply (blast intro!: minor
+ intro: Ord_trans
+ dest: Ord_in_Ord [THEN eclose_sing_Ord, THEN subsetD])
+done
+
+(*** Rank ***)
+
+(*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
+lemma rank: "rank(a) = (UN y:a. succ(rank(y)))"
+by (subst rank_def [THEN def_transrec], simp)
+
+lemma Ord_rank [simp]: "Ord(rank(a))"
+apply (rule_tac a="a" in eps_induct)
+apply (subst rank)
+apply (rule Ord_succ [THEN Ord_UN])
+apply (erule bspec, assumption)
+done
+
+lemma rank_of_Ord: "Ord(i) ==> rank(i) = i"
+apply (erule trans_induct)
+apply (subst rank)
+apply (simp add: Ord_equality)
+done
+
+lemma rank_lt: "a:b ==> rank(a) < rank(b)"
+apply (rule_tac a1 = "b" in rank [THEN ssubst])
+apply (erule UN_I [THEN ltI])
+apply (rule_tac [2] Ord_UN, auto)
+done
+
+lemma eclose_rank_lt: "a: eclose(b) ==> rank(a) < rank(b)"
+apply (erule eclose_induct_down)
+apply (erule rank_lt)
+apply (erule rank_lt [THEN lt_trans], assumption)
+done
- rec :: [i, i, [i,i]=>i]=>i
- "rec(k,a,b) == recursor(a,b,k)"
+lemma rank_mono: "a<=b ==> rank(a) le rank(b)"
+apply (rule subset_imp_le)
+apply (subst rank)
+apply (subst rank, auto)
+done
+
+lemma rank_Pow: "rank(Pow(a)) = succ(rank(a))"
+apply (rule rank [THEN trans])
+apply (rule le_anti_sym)
+apply (rule_tac [2] UN_upper_le)
+apply (rule UN_least_le)
+apply (auto intro: rank_mono simp add: Ord_UN)
+done
+
+lemma rank_0 [simp]: "rank(0) = 0"
+by (rule rank [THEN trans], blast)
+
+lemma rank_succ [simp]: "rank(succ(x)) = succ(rank(x))"
+apply (rule rank [THEN trans])
+apply (rule equalityI [OF UN_least succI1 [THEN UN_upper]])
+apply (erule succE, blast)
+apply (erule rank_lt [THEN leI, THEN succ_leI, THEN le_imp_subset])
+done
+
+lemma rank_Union: "rank(Union(A)) = (UN x:A. rank(x))"
+apply (rule equalityI)
+apply (rule_tac [2] rank_mono [THEN le_imp_subset, THEN UN_least])
+apply (erule_tac [2] Union_upper)
+apply (subst rank)
+apply (rule UN_least)
+apply (erule UnionE)
+apply (rule subset_trans)
+apply (erule_tac [2] RepFunI [THEN Union_upper])
+apply (erule rank_lt [THEN succ_leI, THEN le_imp_subset])
+done
+
+lemma rank_eclose: "rank(eclose(a)) = rank(a)"
+apply (rule le_anti_sym)
+apply (rule_tac [2] arg_subset_eclose [THEN rank_mono])
+apply (rule_tac a1 = "eclose (a) " in rank [THEN ssubst])
+apply (rule Ord_rank [THEN UN_least_le])
+apply (erule eclose_rank_lt [THEN succ_leI])
+done
+
+lemma rank_pair1: "rank(a) < rank(<a,b>)"
+apply (unfold Pair_def)
+apply (rule consI1 [THEN rank_lt, THEN lt_trans])
+apply (rule consI1 [THEN consI2, THEN rank_lt])
+done
+
+lemma rank_pair2: "rank(b) < rank(<a,b>)"
+apply (unfold Pair_def)
+apply (rule consI1 [THEN consI2, THEN rank_lt, THEN lt_trans])
+apply (rule consI1 [THEN consI2, THEN rank_lt])
+done
+
+(*Not clear how to remove the P(a) condition, since the "then" part
+ must refer to "a"*)
+lemma the_equality_if:
+ "P(a) ==> (THE x. P(x)) = (if (EX!x. P(x)) then a else 0)"
+by (simp add: the_0 the_equality2)
+
+(*The premise is needed not just to fix i but to ensure f~=0*)
+lemma rank_apply: "i : domain(f) ==> rank(f`i) < rank(f)"
+apply (unfold apply_def, clarify)
+apply (subgoal_tac "rank (y) < rank (f) ")
+prefer 2 apply (blast intro: lt_trans rank_lt rank_pair2)
+apply (subgoal_tac "0 < rank (f) ")
+apply (erule_tac [2] Ord_rank [THEN Ord_0_le, THEN lt_trans1])
+apply (simp add: the_equality_if)
+done
+
+
+(*** Corollaries of leastness ***)
+
+lemma mem_eclose_subset: "A:B ==> eclose(A)<=eclose(B)"
+apply (rule Transset_eclose [THEN eclose_least])
+apply (erule arg_into_eclose [THEN eclose_subset])
+done
+
+lemma eclose_mono: "A<=B ==> eclose(A) <= eclose(B)"
+apply (rule Transset_eclose [THEN eclose_least])
+apply (erule subset_trans)
+apply (rule arg_subset_eclose)
+done
+
+(** Idempotence of eclose **)
+
+lemma eclose_idem: "eclose(eclose(A)) = eclose(A)"
+apply (rule equalityI)
+apply (rule eclose_least [OF Transset_eclose subset_refl])
+apply (rule arg_subset_eclose)
+done
+
+(** Transfinite recursion for definitions based on the
+ three cases of ordinals **)
+
+lemma transrec2_0 [simp]: "transrec2(0,a,b) = a"
+by (rule transrec2_def [THEN def_transrec, THEN trans], simp)
+
+lemma transrec2_succ [simp]: "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))"
+apply (rule transrec2_def [THEN def_transrec, THEN trans])
+apply (simp add: the_equality if_P)
+done
+
+lemma transrec2_Limit:
+ "Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))"
+apply (rule transrec2_def [THEN def_transrec, THEN trans], simp)
+apply (blast dest!: Limit_has_0 elim!: succ_LimitE)
+done
+
+
+(** recursor -- better than nat_rec; the succ case has no type requirement! **)
+
+(*NOT suitable for rewriting*)
+lemmas recursor_lemma = recursor_def [THEN def_transrec, THEN trans]
+
+lemma recursor_0: "recursor(a,b,0) = a"
+by (rule nat_case_0 [THEN recursor_lemma])
+
+lemma recursor_succ: "recursor(a,b,succ(m)) = b(m, recursor(a,b,m))"
+by (rule recursor_lemma, simp)
+
+
+(** rec: old version for compatibility **)
+
+lemma rec_0 [simp]: "rec(0,a,b) = a"
+apply (unfold rec_def)
+apply (rule recursor_0)
+done
+
+lemma rec_succ [simp]: "rec(succ(m),a,b) = b(m, rec(m,a,b))"
+apply (unfold rec_def)
+apply (rule recursor_succ)
+done
+
+lemma rec_type:
+ "[| n: nat;
+ a: C(0);
+ !!m z. [| m: nat; z: C(m) |] ==> b(m,z): C(succ(m)) |]
+ ==> rec(n,a,b) : C(n)"
+apply (erule nat_induct, auto)
+done
+
+ML
+{*
+val arg_subset_eclose = thm "arg_subset_eclose";
+val arg_into_eclose = thm "arg_into_eclose";
+val Transset_eclose = thm "Transset_eclose";
+val eclose_subset = thm "eclose_subset";
+val ecloseD = thm "ecloseD";
+val arg_in_eclose_sing = thm "arg_in_eclose_sing";
+val arg_into_eclose_sing = thm "arg_into_eclose_sing";
+val eclose_induct = thm "eclose_induct";
+val eps_induct = thm "eps_induct";
+val eclose_least_lemma = thm "eclose_least_lemma";
+val eclose_least = thm "eclose_least";
+val eclose_induct_down = thm "eclose_induct_down";
+val Transset_eclose_eq_arg = thm "Transset_eclose_eq_arg";
+val mem_eclose_trans = thm "mem_eclose_trans";
+val mem_eclose_sing_trans = thm "mem_eclose_sing_trans";
+val under_Memrel = thm "under_Memrel";
+val under_Memrel_eclose = thm "under_Memrel_eclose";
+val wfrec_ssubst = thm "wfrec_ssubst";
+val wfrec_eclose_eq = thm "wfrec_eclose_eq";
+val wfrec_eclose_eq2 = thm "wfrec_eclose_eq2";
+val transrec = thm "transrec";
+val def_transrec = thm "def_transrec";
+val transrec_type = thm "transrec_type";
+val eclose_sing_Ord = thm "eclose_sing_Ord";
+val Ord_transrec_type = thm "Ord_transrec_type";
+val rank = thm "rank";
+val Ord_rank = thm "Ord_rank";
+val rank_of_Ord = thm "rank_of_Ord";
+val rank_lt = thm "rank_lt";
+val eclose_rank_lt = thm "eclose_rank_lt";
+val rank_mono = thm "rank_mono";
+val rank_Pow = thm "rank_Pow";
+val rank_0 = thm "rank_0";
+val rank_succ = thm "rank_succ";
+val rank_Union = thm "rank_Union";
+val rank_eclose = thm "rank_eclose";
+val rank_pair1 = thm "rank_pair1";
+val rank_pair2 = thm "rank_pair2";
+val the_equality_if = thm "the_equality_if";
+val rank_apply = thm "rank_apply";
+val mem_eclose_subset = thm "mem_eclose_subset";
+val eclose_mono = thm "eclose_mono";
+val eclose_idem = thm "eclose_idem";
+val transrec2_0 = thm "transrec2_0";
+val transrec2_succ = thm "transrec2_succ";
+val transrec2_Limit = thm "transrec2_Limit";
+val recursor_lemma = thm "recursor_lemma";
+val recursor_0 = thm "recursor_0";
+val recursor_succ = thm "recursor_succ";
+val rec_0 = thm "rec_0";
+val rec_succ = thm "rec_succ";
+val rec_type = thm "rec_type";
+*}
end