# HG changeset patch # User paulson # Date 1021753343 -7200 # Node ID dfc399c684e498594bf0f197f7ea6b687e9dc2f3 # Parent e320a52ff71121198c576afc98850a29f390f8eb converted Epsilon to Isar diff -r e320a52ff711 -r dfc399c684e4 src/ZF/Epsilon.ML --- 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()"; -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()"; -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 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"; - diff -r e320a52ff711 -r dfc399c684e4 src/ZF/Epsilon.thy --- 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 ji, 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()" +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()" +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 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 diff -r e320a52ff711 -r dfc399c684e4 src/ZF/IsaMakefile --- a/src/ZF/IsaMakefile Sat May 18 20:08:17 2002 +0200 +++ b/src/ZF/IsaMakefile Sat May 18 22:22:23 2002 +0200 @@ -31,7 +31,7 @@ $(OUT)/ZF: $(OUT)/FOL AC.thy Arith.thy ArithSimp.ML \ ArithSimp.thy Bool.ML Bool.thy Cardinal.ML Cardinal.thy \ CardinalArith.ML CardinalArith.thy Cardinal_AC.thy \ - Datatype.ML Datatype.thy Epsilon.ML Epsilon.thy Finite.ML Finite.thy \ + Datatype.ML Datatype.thy Epsilon.thy Finite.ML Finite.thy \ Fixedpt.ML Fixedpt.thy Inductive.ML Inductive.thy \ InfDatatype.thy Integ/Bin.ML Integ/Bin.thy Integ/EquivClass.ML \ Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy Integ/IntArith.thy \ @@ -39,8 +39,7 @@ Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy Main.ML Main.thy \ Main_ZFC.ML Main_ZFC.thy \ Nat.ML Nat.thy Order.thy OrderArith.thy \ - OrderType.thy Ordinal.thy OrdQuant.ML OrdQuant.thy \ - Perm.ML Perm.thy \ + OrderType.thy Ordinal.thy OrdQuant.ML OrdQuant.thy Perm.ML Perm.thy \ QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML Rel.thy Sum.ML \ Sum.thy Tools/cartprod.ML Tools/datatype_package.ML \ Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML \