# HG changeset patch # User paulson # Date 1026829776 -7200 # Node ID c26eeb000470e5e33533a4a4c5d021e7aa551246 # Parent cd7f9ea583388fc3492fcff665cae5ed8d0ce78b instantiation of locales M_trancl and M_wfrank; proofs of list_replacement{1,2} diff -r cd7f9ea58338 -r c26eeb000470 src/ZF/Constructible/Datatype_absolute.thy --- a/src/ZF/Constructible/Datatype_absolute.thy Tue Jul 16 16:28:49 2002 +0200 +++ b/src/ZF/Constructible/Datatype_absolute.thy Tue Jul 16 16:29:36 2002 +0200 @@ -101,17 +101,14 @@ iterates_replacement :: "[i=>o, [i,i]=>o, i] => o" "iterates_replacement(M,isF,v) == - \n[M]. n\nat --> + \n[M]. n\nat --> wfrec_replacement(M, iterates_MH(M,isF,v), Memrel(succ(n)))" lemma (in M_axioms) iterates_MH_abs: "[| relativize1(M,isF,F); M(n); M(g); M(z) |] ==> iterates_MH(M,isF,v,n,g,z) <-> z = nat_case(v, \m. F(g`m), n)" -apply (simp add: iterates_MH_def) -apply (rule nat_case_abs) -apply (simp_all add: relativize1_def) -done - +by (simp add: nat_case_abs [of _ "\m. F(g ` m)"] + relativize1_def iterates_MH_def) lemma (in M_axioms) iterates_imp_wfrec_replacement: "[|relativize1(M,isF,F); n \ nat; iterates_replacement(M,isF,v)|] @@ -159,28 +156,20 @@ locale M_datatypes = M_wfrank + assumes list_replacement1: - "M(A) ==> \zero[M]. empty(M,zero) & - iterates_replacement(M, is_list_functor(M,A), zero)" + "M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)" and list_replacement2: - "M(A) ==> - \zero[M]. empty(M,zero) & - strong_replacement(M, + "M(A) ==> strong_replacement(M, \n y. n\nat & (\sn[M]. \msn[M]. successor(M,n,sn) & membership(M,sn,msn) & - is_wfrec(M, iterates_MH(M,is_list_functor(M,A), zero), + is_wfrec(M, iterates_MH(M,is_list_functor(M,A), 0), msn, n, y)))" -lemma (in M_datatypes) list_replacement1': - "M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)" -apply (insert list_replacement1, simp) -done - lemma (in M_datatypes) list_replacement2': "M(A) ==> strong_replacement(M, \n y. n\nat & y = (\X. {0} + A * X)^n (0))" apply (insert list_replacement2 [of A]) apply (rule strong_replacement_cong [THEN iffD1]) apply (rule conj_cong [OF iff_refl iterates_abs [of "is_list_functor(M,A)"]]) -apply (simp_all add: list_replacement1' relativize1_def) +apply (simp_all add: list_replacement1 relativize1_def) done lemma (in M_datatypes) list_closed [intro,simp]: diff -r cd7f9ea58338 -r c26eeb000470 src/ZF/Constructible/L_axioms.thy --- a/src/ZF/Constructible/L_axioms.thy Tue Jul 16 16:28:49 2002 +0200 +++ b/src/ZF/Constructible/L_axioms.thy Tue Jul 16 16:29:36 2002 +0200 @@ -66,7 +66,8 @@ apply (simp_all add: Replace_iff univalent_def, blast) done -subsection{*Instantiation of the locale @{text M_triv_axioms}*} +subsection{*Instantiating the locale @{text M_triv_axioms}*} +text{*No instances of Separation yet.*} lemma Lset_mono_le: "mono_le_subset(Lset)" by (simp add: mono_le_subset_def le_imp_subset Lset_mono) @@ -90,57 +91,57 @@ fun kill_flex_triv_prems st = Seq.hd ((REPEAT_FIRST assume_tac) st); -fun trivaxL th = +fun triv_axioms_L th = kill_flex_triv_prems ([transL, nonempty, upair_ax, Union_ax, power_ax, replacement, L_nat] MRS (inst "M" "L" th)); -bind_thm ("ball_abs", trivaxL (thm "M_triv_axioms.ball_abs")); -bind_thm ("rall_abs", trivaxL (thm "M_triv_axioms.rall_abs")); -bind_thm ("bex_abs", trivaxL (thm "M_triv_axioms.bex_abs")); -bind_thm ("rex_abs", trivaxL (thm "M_triv_axioms.rex_abs")); -bind_thm ("ball_iff_equiv", trivaxL (thm "M_triv_axioms.ball_iff_equiv")); -bind_thm ("M_equalityI", trivaxL (thm "M_triv_axioms.M_equalityI")); -bind_thm ("empty_abs", trivaxL (thm "M_triv_axioms.empty_abs")); -bind_thm ("subset_abs", trivaxL (thm "M_triv_axioms.subset_abs")); -bind_thm ("upair_abs", trivaxL (thm "M_triv_axioms.upair_abs")); -bind_thm ("upair_in_M_iff", trivaxL (thm "M_triv_axioms.upair_in_M_iff")); -bind_thm ("singleton_in_M_iff", trivaxL (thm "M_triv_axioms.singleton_in_M_iff")); -bind_thm ("pair_abs", trivaxL (thm "M_triv_axioms.pair_abs")); -bind_thm ("pair_in_M_iff", trivaxL (thm "M_triv_axioms.pair_in_M_iff")); -bind_thm ("pair_components_in_M", trivaxL (thm "M_triv_axioms.pair_components_in_M")); -bind_thm ("cartprod_abs", trivaxL (thm "M_triv_axioms.cartprod_abs")); -bind_thm ("union_abs", trivaxL (thm "M_triv_axioms.union_abs")); -bind_thm ("inter_abs", trivaxL (thm "M_triv_axioms.inter_abs")); -bind_thm ("setdiff_abs", trivaxL (thm "M_triv_axioms.setdiff_abs")); -bind_thm ("Union_abs", trivaxL (thm "M_triv_axioms.Union_abs")); -bind_thm ("Union_closed", trivaxL (thm "M_triv_axioms.Union_closed")); -bind_thm ("Un_closed", trivaxL (thm "M_triv_axioms.Un_closed")); -bind_thm ("cons_closed", trivaxL (thm "M_triv_axioms.cons_closed")); -bind_thm ("successor_abs", trivaxL (thm "M_triv_axioms.successor_abs")); -bind_thm ("succ_in_M_iff", trivaxL (thm "M_triv_axioms.succ_in_M_iff")); -bind_thm ("separation_closed", trivaxL (thm "M_triv_axioms.separation_closed")); -bind_thm ("strong_replacementI", trivaxL (thm "M_triv_axioms.strong_replacementI")); -bind_thm ("strong_replacement_closed", trivaxL (thm "M_triv_axioms.strong_replacement_closed")); -bind_thm ("RepFun_closed", trivaxL (thm "M_triv_axioms.RepFun_closed")); -bind_thm ("lam_closed", trivaxL (thm "M_triv_axioms.lam_closed")); -bind_thm ("image_abs", trivaxL (thm "M_triv_axioms.image_abs")); -bind_thm ("powerset_Pow", trivaxL (thm "M_triv_axioms.powerset_Pow")); -bind_thm ("powerset_imp_subset_Pow", trivaxL (thm "M_triv_axioms.powerset_imp_subset_Pow")); -bind_thm ("nat_into_M", trivaxL (thm "M_triv_axioms.nat_into_M")); -bind_thm ("nat_case_closed", trivaxL (thm "M_triv_axioms.nat_case_closed")); -bind_thm ("Inl_in_M_iff", trivaxL (thm "M_triv_axioms.Inl_in_M_iff")); -bind_thm ("Inr_in_M_iff", trivaxL (thm "M_triv_axioms.Inr_in_M_iff")); -bind_thm ("lt_closed", trivaxL (thm "M_triv_axioms.lt_closed")); -bind_thm ("transitive_set_abs", trivaxL (thm "M_triv_axioms.transitive_set_abs")); -bind_thm ("ordinal_abs", trivaxL (thm "M_triv_axioms.ordinal_abs")); -bind_thm ("limit_ordinal_abs", trivaxL (thm "M_triv_axioms.limit_ordinal_abs")); -bind_thm ("successor_ordinal_abs", trivaxL (thm "M_triv_axioms.successor_ordinal_abs")); -bind_thm ("finite_ordinal_abs", trivaxL (thm "M_triv_axioms.finite_ordinal_abs")); -bind_thm ("omega_abs", trivaxL (thm "M_triv_axioms.omega_abs")); -bind_thm ("number1_abs", trivaxL (thm "M_triv_axioms.number1_abs")); -bind_thm ("number1_abs", trivaxL (thm "M_triv_axioms.number1_abs")); -bind_thm ("number3_abs", trivaxL (thm "M_triv_axioms.number3_abs")); +bind_thm ("ball_abs", triv_axioms_L (thm "M_triv_axioms.ball_abs")); +bind_thm ("rall_abs", triv_axioms_L (thm "M_triv_axioms.rall_abs")); +bind_thm ("bex_abs", triv_axioms_L (thm "M_triv_axioms.bex_abs")); +bind_thm ("rex_abs", triv_axioms_L (thm "M_triv_axioms.rex_abs")); +bind_thm ("ball_iff_equiv", triv_axioms_L (thm "M_triv_axioms.ball_iff_equiv")); +bind_thm ("M_equalityI", triv_axioms_L (thm "M_triv_axioms.M_equalityI")); +bind_thm ("empty_abs", triv_axioms_L (thm "M_triv_axioms.empty_abs")); +bind_thm ("subset_abs", triv_axioms_L (thm "M_triv_axioms.subset_abs")); +bind_thm ("upair_abs", triv_axioms_L (thm "M_triv_axioms.upair_abs")); +bind_thm ("upair_in_M_iff", triv_axioms_L (thm "M_triv_axioms.upair_in_M_iff")); +bind_thm ("singleton_in_M_iff", triv_axioms_L (thm "M_triv_axioms.singleton_in_M_iff")); +bind_thm ("pair_abs", triv_axioms_L (thm "M_triv_axioms.pair_abs")); +bind_thm ("pair_in_M_iff", triv_axioms_L (thm "M_triv_axioms.pair_in_M_iff")); +bind_thm ("pair_components_in_M", triv_axioms_L (thm "M_triv_axioms.pair_components_in_M")); +bind_thm ("cartprod_abs", triv_axioms_L (thm "M_triv_axioms.cartprod_abs")); +bind_thm ("union_abs", triv_axioms_L (thm "M_triv_axioms.union_abs")); +bind_thm ("inter_abs", triv_axioms_L (thm "M_triv_axioms.inter_abs")); +bind_thm ("setdiff_abs", triv_axioms_L (thm "M_triv_axioms.setdiff_abs")); +bind_thm ("Union_abs", triv_axioms_L (thm "M_triv_axioms.Union_abs")); +bind_thm ("Union_closed", triv_axioms_L (thm "M_triv_axioms.Union_closed")); +bind_thm ("Un_closed", triv_axioms_L (thm "M_triv_axioms.Un_closed")); +bind_thm ("cons_closed", triv_axioms_L (thm "M_triv_axioms.cons_closed")); +bind_thm ("successor_abs", triv_axioms_L (thm "M_triv_axioms.successor_abs")); +bind_thm ("succ_in_M_iff", triv_axioms_L (thm "M_triv_axioms.succ_in_M_iff")); +bind_thm ("separation_closed", triv_axioms_L (thm "M_triv_axioms.separation_closed")); +bind_thm ("strong_replacementI", triv_axioms_L (thm "M_triv_axioms.strong_replacementI")); +bind_thm ("strong_replacement_closed", triv_axioms_L (thm "M_triv_axioms.strong_replacement_closed")); +bind_thm ("RepFun_closed", triv_axioms_L (thm "M_triv_axioms.RepFun_closed")); +bind_thm ("lam_closed", triv_axioms_L (thm "M_triv_axioms.lam_closed")); +bind_thm ("image_abs", triv_axioms_L (thm "M_triv_axioms.image_abs")); +bind_thm ("powerset_Pow", triv_axioms_L (thm "M_triv_axioms.powerset_Pow")); +bind_thm ("powerset_imp_subset_Pow", triv_axioms_L (thm "M_triv_axioms.powerset_imp_subset_Pow")); +bind_thm ("nat_into_M", triv_axioms_L (thm "M_triv_axioms.nat_into_M")); +bind_thm ("nat_case_closed", triv_axioms_L (thm "M_triv_axioms.nat_case_closed")); +bind_thm ("Inl_in_M_iff", triv_axioms_L (thm "M_triv_axioms.Inl_in_M_iff")); +bind_thm ("Inr_in_M_iff", triv_axioms_L (thm "M_triv_axioms.Inr_in_M_iff")); +bind_thm ("lt_closed", triv_axioms_L (thm "M_triv_axioms.lt_closed")); +bind_thm ("transitive_set_abs", triv_axioms_L (thm "M_triv_axioms.transitive_set_abs")); +bind_thm ("ordinal_abs", triv_axioms_L (thm "M_triv_axioms.ordinal_abs")); +bind_thm ("limit_ordinal_abs", triv_axioms_L (thm "M_triv_axioms.limit_ordinal_abs")); +bind_thm ("successor_ordinal_abs", triv_axioms_L (thm "M_triv_axioms.successor_ordinal_abs")); +bind_thm ("finite_ordinal_abs", triv_axioms_L (thm "M_triv_axioms.finite_ordinal_abs")); +bind_thm ("omega_abs", triv_axioms_L (thm "M_triv_axioms.omega_abs")); +bind_thm ("number1_abs", triv_axioms_L (thm "M_triv_axioms.number1_abs")); +bind_thm ("number1_abs", triv_axioms_L (thm "M_triv_axioms.number1_abs")); +bind_thm ("number3_abs", triv_axioms_L (thm "M_triv_axioms.number3_abs")); *} declare ball_abs [simp] @@ -563,6 +564,39 @@ done +subsubsection{*The Number 1, Internalized*} + +(* "number1(M,a) == (\x[M]. empty(M,x) & successor(M,x,a))" *) +constdefs number1_fm :: "i=>i" + "number1_fm(a) == Exists(And(empty_fm(0), succ_fm(0,succ(a))))" + +lemma number1_type [TC]: + "x \ nat ==> number1_fm(x) \ formula" +by (simp add: number1_fm_def) + +lemma arity_number1_fm [simp]: + "x \ nat ==> arity(number1_fm(x)) = succ(x)" +by (simp add: number1_fm_def succ_Un_distrib [symmetric] Un_ac) + +lemma sats_number1_fm [simp]: + "[| x \ nat; env \ list(A)|] + ==> sats(A, number1_fm(x), env) <-> number1(**A, nth(x,env))" +by (simp add: number1_fm_def number1_def) + +lemma number1_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; + i \ nat; env \ list(A)|] + ==> number1(**A, x) <-> sats(A, number1_fm(i), env)" +by simp + +theorem number1_reflection: + "REFLECTS[\x. number1(L,f(x)), + \i x. number1(**Lset(i),f(x))]" +apply (simp only: number1_def setclass_simps) +apply (intro FOL_reflections empty_reflection successor_reflection) +done + + subsubsection{*Big Union, Internalized*} (* "big_union(M,A,z) == \x[M]. x \ z <-> (\y[M]. y\A & x \ y)" *) @@ -1076,7 +1110,8 @@ by simp lemmas function_reflections = - empty_reflection upair_reflection pair_reflection union_reflection + empty_reflection number1_reflection + upair_reflection pair_reflection union_reflection big_union_reflection cons_reflection successor_reflection fun_apply_reflection subset_reflection transitive_set_reflection membership_reflection @@ -1085,7 +1120,8 @@ is_relation_reflection is_function_reflection lemmas function_iff_sats = - empty_iff_sats upair_iff_sats pair_iff_sats union_iff_sats + empty_iff_sats number1_iff_sats + upair_iff_sats pair_iff_sats union_iff_sats cons_iff_sats successor_iff_sats fun_apply_iff_sats Memrel_iff_sats pred_set_iff_sats domain_iff_sats range_iff_sats field_iff_sats diff -r cd7f9ea58338 -r c26eeb000470 src/ZF/Constructible/Rec_Separation.thy --- a/src/ZF/Constructible/Rec_Separation.thy Tue Jul 16 16:28:49 2002 +0200 +++ b/src/ZF/Constructible/Rec_Separation.thy Tue Jul 16 16:29:36 2002 +0200 @@ -1,10 +1,13 @@ -header{*Separation for the Absoluteness of Recursion*} +header{*Separation for Facts About Recursion*} -theory Rec_Separation = Separation: +theory Rec_Separation = Separation + Datatype_absolute: text{*This theory proves all instances needed for locales @{text "M_trancl"}, @{text "M_wfrank"} and @{text "M_datatypes"}*} +lemma eq_succ_imp_lt: "[|i = succ(j); Ord(i)|] ==> jo, [i,i,i]=>o, i, i, i] => o" @@ -275,7 +312,22 @@ restriction_reflection MH_reflection) done -subsection{*Separation for @{term "wfrank"}*} +text{*Currently, @{text sats}-theorems for higher-order operators don't seem +useful. Reflection theorems do work, though. This one avoids the repetition +of the @{text MH}-term.*} +theorem is_wfrec_reflection: + assumes MH_reflection: + "!!f g h. REFLECTS[\x. MH(L, f(x), g(x), h(x)), + \i x. MH(**Lset(i), f(x), g(x), h(x))]" + shows "REFLECTS[\x. is_wfrec(L, MH(L), f(x), g(x), h(x)), + \i x. is_wfrec(**Lset(i), MH(**Lset(i)), f(x), g(x), h(x))]" +apply (simp (no_asm_use) only: is_wfrec_def setclass_simps) +apply (intro FOL_reflections MH_reflection is_recfun_reflection) +done + +subsection{*The Locale @{text "M_wfrank"}*} + +subsubsection{*Separation for @{term "wfrank"}*} lemma wfrank_Reflects: "REFLECTS[\x. \rplus[L]. tran_closure(L,r,rplus) --> @@ -305,7 +357,7 @@ done -subsection{*Replacement for @{term "wfrank"}*} +subsubsection{*Replacement for @{term "wfrank"}*} lemma wfrank_replacement_Reflects: "REFLECTS[\z. \x[L]. x \ A & @@ -347,7 +399,7 @@ done -subsection{*Separation for @{term "wfrank"}*} +subsubsection{*Separation for Proving @{text Ord_wfrank_range}*} lemma Ord_wfrank_Reflects: "REFLECTS[\x. \rplus[L]. tran_closure(L,r,rplus) --> @@ -387,4 +439,438 @@ done +subsubsection{*Instantiating the locale @{text M_wfrank}*} +ML +{* +val wfrank_separation = thm "wfrank_separation"; +val wfrank_strong_replacement = thm "wfrank_strong_replacement"; +val Ord_wfrank_separation = thm "Ord_wfrank_separation"; + +val m_wfrank = + [wfrank_separation, wfrank_strong_replacement, Ord_wfrank_separation]; + +fun wfrank_L th = + kill_flex_triv_prems (m_wfrank MRS (trancl_L th)); + + + +bind_thm ("iterates_closed", wfrank_L (thm "M_wfrank.iterates_closed")); +bind_thm ("exists_wfrank", wfrank_L (thm "M_wfrank.exists_wfrank")); +bind_thm ("M_wellfoundedrank", wfrank_L (thm "M_wfrank.M_wellfoundedrank")); +bind_thm ("Ord_wfrank_range", wfrank_L (thm "M_wfrank.Ord_wfrank_range")); +bind_thm ("Ord_range_wellfoundedrank", wfrank_L (thm "M_wfrank.Ord_range_wellfoundedrank")); +bind_thm ("function_wellfoundedrank", wfrank_L (thm "M_wfrank.function_wellfoundedrank")); +bind_thm ("domain_wellfoundedrank", wfrank_L (thm "M_wfrank.domain_wellfoundedrank")); +bind_thm ("wellfoundedrank_type", wfrank_L (thm "M_wfrank.wellfoundedrank_type")); +bind_thm ("Ord_wellfoundedrank", wfrank_L (thm "M_wfrank.Ord_wellfoundedrank")); +bind_thm ("wellfoundedrank_eq", wfrank_L (thm "M_wfrank.wellfoundedrank_eq")); +bind_thm ("wellfoundedrank_lt", wfrank_L (thm "M_wfrank.wellfoundedrank_lt")); +bind_thm ("wellfounded_imp_subset_rvimage", wfrank_L (thm "M_wfrank.wellfounded_imp_subset_rvimage")); +bind_thm ("wellfounded_imp_wf", wfrank_L (thm "M_wfrank.wellfounded_imp_wf")); +bind_thm ("wellfounded_on_imp_wf_on", wfrank_L (thm "M_wfrank.wellfounded_on_imp_wf_on")); +bind_thm ("wf_abs", wfrank_L (thm "M_wfrank.wf_abs")); +bind_thm ("wf_on_abs", wfrank_L (thm "M_wfrank.wf_on_abs")); +bind_thm ("wfrec_replacement_iff", wfrank_L (thm "M_wfrank.wfrec_replacement_iff")); +bind_thm ("trans_wfrec_closed", wfrank_L (thm "M_wfrank.trans_wfrec_closed")); +bind_thm ("wfrec_closed", wfrank_L (thm "M_wfrank.wfrec_closed")); +*} + +declare iterates_closed [intro,simp] +declare Ord_wfrank_range [rule_format] +declare wf_abs [simp] +declare wf_on_abs [simp] + + +subsection{*For Datatypes*} + +subsubsection{*Binary Products, Internalized*} + +constdefs cartprod_fm :: "[i,i,i]=>i" +(* "cartprod(M,A,B,z) == + \u[M]. u \ z <-> (\x[M]. x\A & (\y[M]. y\B & pair(M,x,y,u)))" *) + "cartprod_fm(A,B,z) == + Forall(Iff(Member(0,succ(z)), + Exists(And(Member(0,succ(succ(A))), + Exists(And(Member(0,succ(succ(succ(B)))), + pair_fm(1,0,2)))))))" + +lemma cartprod_type [TC]: + "[| x \ nat; y \ nat; z \ nat |] ==> cartprod_fm(x,y,z) \ formula" +by (simp add: cartprod_fm_def) + +lemma arity_cartprod_fm [simp]: + "[| x \ nat; y \ nat; z \ nat |] + ==> arity(cartprod_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" +by (simp add: cartprod_fm_def succ_Un_distrib [symmetric] Un_ac) + +lemma sats_cartprod_fm [simp]: + "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] + ==> sats(A, cartprod_fm(x,y,z), env) <-> + cartprod(**A, nth(x,env), nth(y,env), nth(z,env))" +by (simp add: cartprod_fm_def cartprod_def) + +lemma cartprod_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; + i \ nat; j \ nat; k \ nat; env \ list(A)|] + ==> cartprod(**A, x, y, z) <-> sats(A, cartprod_fm(i,j,k), env)" +by (simp add: sats_cartprod_fm) + +theorem cartprod_reflection: + "REFLECTS[\x. cartprod(L,f(x),g(x),h(x)), + \i x. cartprod(**Lset(i),f(x),g(x),h(x))]" +apply (simp only: cartprod_def setclass_simps) +apply (intro FOL_reflections pair_reflection) +done + + +subsubsection{*Binary Sums, Internalized*} + +(* "is_sum(M,A,B,Z) == + \A0[M]. \n1[M]. \s1[M]. \B1[M]. + 3 2 1 0 + number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) & + cartprod(M,s1,B,B1) & union(M,A0,B1,Z)" *) +constdefs sum_fm :: "[i,i,i]=>i" + "sum_fm(A,B,Z) == + Exists(Exists(Exists(Exists( + And(number1_fm(2), + And(cartprod_fm(2,A#+4,3), + And(upair_fm(2,2,1), + And(cartprod_fm(1,B#+4,0), union_fm(3,0,Z#+4)))))))))" + +lemma sum_type [TC]: + "[| x \ nat; y \ nat; z \ nat |] ==> sum_fm(x,y,z) \ formula" +by (simp add: sum_fm_def) + +lemma arity_sum_fm [simp]: + "[| x \ nat; y \ nat; z \ nat |] + ==> arity(sum_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" +by (simp add: sum_fm_def succ_Un_distrib [symmetric] Un_ac) + +lemma sats_sum_fm [simp]: + "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] + ==> sats(A, sum_fm(x,y,z), env) <-> + is_sum(**A, nth(x,env), nth(y,env), nth(z,env))" +by (simp add: sum_fm_def is_sum_def) + +lemma sum_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; + i \ nat; j \ nat; k \ nat; env \ list(A)|] + ==> is_sum(**A, x, y, z) <-> sats(A, sum_fm(i,j,k), env)" +by simp + +theorem sum_reflection: + "REFLECTS[\x. is_sum(L,f(x),g(x),h(x)), + \i x. is_sum(**Lset(i),f(x),g(x),h(x))]" +apply (simp only: is_sum_def setclass_simps) +apply (intro FOL_reflections function_reflections cartprod_reflection) +done + + +subsubsection{*The List Functor, Internalized*} + +constdefs list_functor_fm :: "[i,i,i]=>i" +(* "is_list_functor(M,A,X,Z) == + \n1[M]. \AX[M]. + number1(M,n1) & cartprod(M,A,X,AX) & is_sum(M,n1,AX,Z)" *) + "list_functor_fm(A,X,Z) == + Exists(Exists( + And(number1_fm(1), + And(cartprod_fm(A#+2,X#+2,0), sum_fm(1,0,Z#+2)))))" + +lemma list_functor_type [TC]: + "[| x \ nat; y \ nat; z \ nat |] ==> list_functor_fm(x,y,z) \ formula" +by (simp add: list_functor_fm_def) + +lemma arity_list_functor_fm [simp]: + "[| x \ nat; y \ nat; z \ nat |] + ==> arity(list_functor_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" +by (simp add: list_functor_fm_def succ_Un_distrib [symmetric] Un_ac) + +lemma sats_list_functor_fm [simp]: + "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] + ==> sats(A, list_functor_fm(x,y,z), env) <-> + is_list_functor(**A, nth(x,env), nth(y,env), nth(z,env))" +by (simp add: list_functor_fm_def is_list_functor_def) + +lemma list_functor_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; + i \ nat; j \ nat; k \ nat; env \ list(A)|] + ==> is_list_functor(**A, x, y, z) <-> sats(A, list_functor_fm(i,j,k), env)" +by simp + +theorem list_functor_reflection: + "REFLECTS[\x. is_list_functor(L,f(x),g(x),h(x)), + \i x. is_list_functor(**Lset(i),f(x),g(x),h(x))]" +apply (simp only: is_list_functor_def setclass_simps) +apply (intro FOL_reflections number1_reflection + cartprod_reflection sum_reflection) +done + +subsubsection{*The Operator @{term quasinat}*} + +(* "is_quasinat(M,z) == empty(M,z) | (\m[M]. successor(M,m,z))" *) +constdefs quasinat_fm :: "i=>i" + "quasinat_fm(z) == Or(empty_fm(z), Exists(succ_fm(0,succ(z))))" + +lemma quasinat_type [TC]: + "x \ nat ==> quasinat_fm(x) \ formula" +by (simp add: quasinat_fm_def) + +lemma arity_quasinat_fm [simp]: + "x \ nat ==> arity(quasinat_fm(x)) = succ(x)" +by (simp add: quasinat_fm_def succ_Un_distrib [symmetric] Un_ac) + +lemma sats_quasinat_fm [simp]: + "[| x \ nat; env \ list(A)|] + ==> sats(A, quasinat_fm(x), env) <-> is_quasinat(**A, nth(x,env))" +by (simp add: quasinat_fm_def is_quasinat_def) + +lemma quasinat_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; + i \ nat; env \ list(A)|] + ==> is_quasinat(**A, x) <-> sats(A, quasinat_fm(i), env)" +by simp + +theorem quasinat_reflection: + "REFLECTS[\x. is_quasinat(L,f(x)), + \i x. is_quasinat(**Lset(i),f(x))]" +apply (simp only: is_quasinat_def setclass_simps) +apply (intro FOL_reflections function_reflections) +done + + +subsubsection{*The Operator @{term is_nat_case}*} + +(* is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o" + "is_nat_case(M, a, is_b, k, z) == + (empty(M,k) --> z=a) & + (\m[M]. successor(M,m,k) --> is_b(m,z)) & + (is_quasinat(M,k) | empty(M,z))" *) +text{*The formula @{term is_b} has free variables 1 and 0.*} +constdefs is_nat_case_fm :: "[i, [i,i]=>i, i, i]=>i" + "is_nat_case_fm(a,is_b,k,z) == + And(Implies(empty_fm(k), Equal(z,a)), + And(Forall(Implies(succ_fm(0,succ(k)), + Forall(Implies(Equal(0,succ(succ(z))), is_b(1,0))))), + Or(quasinat_fm(k), empty_fm(z))))" + +lemma is_nat_case_type [TC]: + "[| is_b(1,0) \ formula; + x \ nat; y \ nat; z \ nat |] + ==> is_nat_case_fm(x,is_b,y,z) \ formula" +by (simp add: is_nat_case_fm_def) + +lemma arity_is_nat_case_fm [simp]: + "[| is_b(1,0) \ formula; x \ nat; y \ nat; z \ nat |] + ==> arity(is_nat_case_fm(x,is_b,y,z)) = + succ(x) \ succ(y) \ succ(z) \ (arity(is_b(1,0)) #- 2)" +apply (subgoal_tac "arity(is_b(1,0)) \ nat") +apply typecheck +(*FIXME: could nat_diff_split work?*) +apply (auto simp add: diff_def raw_diff_succ is_nat_case_fm_def nat_imp_quasinat + succ_Un_distrib [symmetric] Un_ac + split: split_nat_case) +done + +lemma sats_is_nat_case_fm: + assumes is_b_iff_sats: + "!!a b. [| a \ A; b \ A|] + ==> is_b(a,b) <-> sats(A, p(1,0), Cons(b, Cons(a,env)))" + shows + "[|x \ nat; y \ nat; z < length(env); env \ list(A)|] + ==> sats(A, is_nat_case_fm(x,p,y,z), env) <-> + is_nat_case(**A, nth(x,env), is_b, nth(y,env), nth(z,env))" +apply (frule lt_length_in_nat, assumption) +apply (simp add: is_nat_case_fm_def is_nat_case_def is_b_iff_sats [THEN iff_sym]) +done + +lemma is_nat_case_iff_sats: + "[| (!!a b. [| a \ A; b \ A|] + ==> is_b(a,b) <-> sats(A, p(1,0), Cons(b, Cons(a,env)))); + nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; + i \ nat; j \ nat; k < length(env); env \ list(A)|] + ==> is_nat_case(**A, x, is_b, y, z) <-> sats(A, is_nat_case_fm(i,p,j,k), env)" +by (simp add: sats_is_nat_case_fm [of A is_b]) + + +text{*The second argument of @{term is_b} gives it direct access to @{term x}, + which is essential for handling free variable references. Without this + argument, we cannot prove reflection for @{term iterates_MH}.*} +theorem is_nat_case_reflection: + assumes is_b_reflection: + "!!h f g. REFLECTS[\x. is_b(L, h(x), f(x), g(x)), + \i x. is_b(**Lset(i), h(x), f(x), g(x))]" + shows "REFLECTS[\x. is_nat_case(L, f(x), is_b(L,x), g(x), h(x)), + \i x. is_nat_case(**Lset(i), f(x), is_b(**Lset(i), x), g(x), h(x))]" +apply (simp (no_asm_use) only: is_nat_case_def setclass_simps) +apply (intro FOL_reflections function_reflections + restriction_reflection is_b_reflection quasinat_reflection) +done + + + +subsection{*The Operator @{term iterates_MH}, Needed for Iteration*} + +(* iterates_MH :: "[i=>o, [i,i]=>o, i, i, i, i] => o" + "iterates_MH(M,isF,v,n,g,z) == + is_nat_case(M, v, \m u. \gm[M]. fun_apply(M,g,m,gm) & isF(gm,u), + n, z)" *) +constdefs iterates_MH_fm :: "[[i,i]=>i, i, i, i, i]=>i" + "iterates_MH_fm(isF,v,n,g,z) == + is_nat_case_fm(v, + \m u. Exists(And(fun_apply_fm(succ(succ(succ(g))),succ(m),0), + Forall(Implies(Equal(0,succ(succ(u))), isF(1,0))))), + n, z)" + +lemma iterates_MH_type [TC]: + "[| p(1,0) \ formula; + v \ nat; x \ nat; y \ nat; z \ nat |] + ==> iterates_MH_fm(p,v,x,y,z) \ formula" +by (simp add: iterates_MH_fm_def) + + +lemma arity_iterates_MH_fm [simp]: + "[| p(1,0) \ formula; + v \ nat; x \ nat; y \ nat; z \ nat |] + ==> arity(iterates_MH_fm(p,v,x,y,z)) = + succ(v) \ succ(x) \ succ(y) \ succ(z) \ (arity(p(1,0)) #- 4)" +apply (subgoal_tac "arity(p(1,0)) \ nat") +apply typecheck +apply (simp add: nat_imp_quasinat iterates_MH_fm_def Un_ac + split: split_nat_case, clarify) +apply (rename_tac i j) +apply (drule eq_succ_imp_eq_m1, simp) +apply (drule eq_succ_imp_eq_m1, simp) +apply (simp add: diff_Un_distrib succ_Un_distrib Un_ac diff_diff_left) +done + +lemma sats_iterates_MH_fm: + assumes is_F_iff_sats: + "!!a b c d. [| a \ A; b \ A; c \ A; d \ A|] + ==> is_F(a,b) <-> + sats(A, p(1,0), Cons(b, Cons(a, Cons(c, Cons(d,env)))))" + shows + "[|v \ nat; x \ nat; y \ nat; z < length(env); env \ list(A)|] + ==> sats(A, iterates_MH_fm(p,v,x,y,z), env) <-> + iterates_MH(**A, is_F, nth(v,env), nth(x,env), nth(y,env), nth(z,env))" +by (simp add: iterates_MH_fm_def iterates_MH_def sats_is_nat_case_fm + is_F_iff_sats [symmetric]) + +lemma iterates_MH_iff_sats: + "[| (!!a b c d. [| a \ A; b \ A; c \ A; d \ A|] + ==> is_F(a,b) <-> + sats(A, p(1,0), Cons(b, Cons(a, Cons(c, Cons(d,env)))))); + nth(i',env) = v; nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; + i' \ nat; i \ nat; j \ nat; k < length(env); env \ list(A)|] + ==> iterates_MH(**A, is_F, v, x, y, z) <-> + sats(A, iterates_MH_fm(p,i',i,j,k), env)" +apply (rule iff_sym) +apply (rule iff_trans) +apply (rule sats_iterates_MH_fm [of A is_F], blast, simp_all) +done + +theorem iterates_MH_reflection: + assumes p_reflection: + "!!f g h. REFLECTS[\x. p(L, f(x), g(x)), + \i x. p(**Lset(i), f(x), g(x))]" + shows "REFLECTS[\x. iterates_MH(L, p(L), e(x), f(x), g(x), h(x)), + \i x. iterates_MH(**Lset(i), p(**Lset(i)), e(x), f(x), g(x), h(x))]" +apply (simp (no_asm_use) only: iterates_MH_def) +txt{*Must be careful: simplifying with @{text setclass_simps} above would + change @{text "\gm[**Lset(i)]"} into @{text "\gm \ Lset(i)"}, when + it would no longer match rule @{text is_nat_case_reflection}. *} +apply (rule is_nat_case_reflection) +apply (simp (no_asm_use) only: setclass_simps) +apply (intro FOL_reflections function_reflections is_nat_case_reflection + restriction_reflection p_reflection) +done + + + +subsection{*@{term L} is Closed Under the Operator @{term list}*} + + +lemma list_replacement1_Reflects: + "REFLECTS + [\x. \u[L]. u \ B \ (\y[L]. pair(L,u,y,x) \ + is_wfrec(L, iterates_MH(L, is_list_functor(L,A), 0), memsn, u, y)), + \i x. \u \ Lset(i). u \ B \ (\y \ Lset(i). pair(**Lset(i), u, y, x) \ + is_wfrec(**Lset(i), + iterates_MH(**Lset(i), + is_list_functor(**Lset(i), A), 0), memsn, u, y))]" +by (intro FOL_reflections function_reflections is_wfrec_reflection + iterates_MH_reflection list_functor_reflection) + +lemma list_replacement1: + "L(A) ==> iterates_replacement(L, is_list_functor(L,A), 0)" +apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) +apply (rule strong_replacementI) +apply (rule rallI) +apply (rename_tac B) +apply (rule separation_CollectI) +apply (insert nonempty) +apply (subgoal_tac "L(Memrel(succ(n)))") +apply (rule_tac A="{B,A,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast ) +apply (rule ReflectsE [OF list_replacement1_Reflects], assumption) +apply (drule subset_Lset_ltD, assumption) +apply (erule reflection_imp_L_separation) + apply (simp_all add: lt_Ord2) +apply (rule DPowI2) +apply (rename_tac v) +apply (rule bex_iff_sats conj_iff_sats)+ +apply (rule_tac env = "[u,v,A,n,B,0,Memrel(succ(n))]" in mem_iff_sats) +apply (rule sep_rules | simp)+ +txt{*Can't get sat rules to work for higher-order operators, so just expand them!*} +apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def) +apply (rule sep_rules list_functor_iff_sats quasinat_iff_sats | simp)+ +apply (simp_all add: succ_Un_distrib [symmetric] Memrel_closed) +done + + +lemma list_replacement2_Reflects: + "REFLECTS + [\x. \u[L]. u \ B \ u \ nat \ + (\sn[L]. \msn[L]. successor(L, u, sn) \ membership(L, sn, msn) \ + is_wfrec (L, iterates_MH (L, is_list_functor(L, A), 0), + msn, u, x)), + \i x. \u \ Lset(i). u \ B \ u \ nat \ + (\sn \ Lset(i). \msn \ Lset(i). + successor(**Lset(i), u, sn) \ membership(**Lset(i), sn, msn) \ + is_wfrec (**Lset(i), + iterates_MH (**Lset(i), is_list_functor(**Lset(i), A), 0), + msn, u, x))]" +by (intro FOL_reflections function_reflections is_wfrec_reflection + iterates_MH_reflection list_functor_reflection) + + +lemma list_replacement2: + "L(A) ==> strong_replacement(L, + \n y. n\nat & + (\sn[L]. \msn[L]. successor(L,n,sn) & membership(L,sn,msn) & + is_wfrec(L, iterates_MH(L,is_list_functor(L,A), 0), + msn, n, y)))" +apply (rule strong_replacementI) +apply (rule rallI) +apply (rename_tac B) +apply (rule separation_CollectI) +apply (insert nonempty) +apply (rule_tac A="{A,B,z,0,nat}" in subset_LsetE) +apply (blast intro: L_nat) +apply (rule ReflectsE [OF list_replacement2_Reflects], assumption) +apply (drule subset_Lset_ltD, assumption) +apply (erule reflection_imp_L_separation) + apply (simp_all add: lt_Ord2) +apply (rule DPowI2) +apply (rename_tac v) +apply (rule bex_iff_sats conj_iff_sats)+ +apply (rule_tac env = "[u,v,A,B,0,nat]" in mem_iff_sats) +apply (rule sep_rules | simp)+ +apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def) +apply (rule sep_rules list_functor_iff_sats quasinat_iff_sats | simp)+ +apply (simp_all add: succ_Un_distrib [symmetric] Memrel_closed) +done + + + end diff -r cd7f9ea58338 -r c26eeb000470 src/ZF/Constructible/Relative.thy --- a/src/ZF/Constructible/Relative.thy Tue Jul 16 16:28:49 2002 +0200 +++ b/src/ZF/Constructible/Relative.thy Tue Jul 16 16:29:36 2002 +0200 @@ -28,6 +28,15 @@ successor :: "[i=>o,i,i] => o" "successor(M,a,z) == is_cons(M,a,a,z)" + number1 :: "[i=>o,i] => o" + "number1(M,a) == (\x[M]. empty(M,x) & successor(M,x,a))" + + number2 :: "[i=>o,i] => o" + "number2(M,a) == (\x[M]. number1(M,x) & successor(M,x,a))" + + number3 :: "[i=>o,i] => o" + "number3(M,a) == (\x[M]. number2(M,x) & successor(M,x,a))" + powerset :: "[i=>o,i,i] => o" "powerset(M,A,z) == \x[M]. x \ z <-> subset(M,x,A)" @@ -161,15 +170,6 @@ --{*omega is a limit ordinal none of whose elements are limit*} "omega(M,a) == limit_ordinal(M,a) & (\x[M]. x\a --> ~ limit_ordinal(M,x))" - number1 :: "[i=>o,i] => o" - "number1(M,a) == (\x[M]. empty(M,x) & successor(M,x,a))" - - number2 :: "[i=>o,i] => o" - "number2(M,a) == (\x[M]. number1(M,x) & successor(M,x,a))" - - number3 :: "[i=>o,i] => o" - "number3(M,a) == (\x[M]. number2(M,x) & successor(M,x,a))" - is_quasinat :: "[i=>o,i] => o" "is_quasinat(M,z) == empty(M,z) | (\m[M]. successor(M,m,z))" @@ -177,7 +177,7 @@ "is_nat_case(M, a, is_b, k, z) == (empty(M,k) --> z=a) & (\m[M]. successor(M,m,k) --> is_b(m,z)) & - (is_quasinat(M,k) | z=0)" + (is_quasinat(M,k) | empty(M,z))" relativize1 :: "[i=>o, [i,i]=>o, i=>i] => o" "relativize1(M,is_f,f) == \x[M]. \y[M]. is_f(x,y) <-> y = f(x)" @@ -669,8 +669,10 @@ apply (simp_all add: relativize1_def) done -(*Needed? surely better to replace is_nat_case by nat_case?*) -lemma (in M_triv_axioms) is_nat_case_cong [cong]: +(*NOT for the simplifier. The assumption M(z') is apparently necessary, but + causes the error "Failed congruence proof!" It may be better to replace + is_nat_case by nat_case before attempting congruence reasoning.*) +lemma (in M_triv_axioms) is_nat_case_cong: "[| a = a'; k = k'; z = z'; M(z'); !!x y. [| M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |] ==> is_nat_case(M, a, is_b, k, z) <-> is_nat_case(M, a', is_b', k', z')" diff -r cd7f9ea58338 -r c26eeb000470 src/ZF/Constructible/Separation.thy --- a/src/ZF/Constructible/Separation.thy Tue Jul 16 16:28:49 2002 +0200 +++ b/src/ZF/Constructible/Separation.thy Tue Jul 16 16:29:36 2002 +0200 @@ -457,6 +457,10 @@ done +subsection{*Instantiating the locale @{text M_axioms}*} +text{*Separation (and Strong Replacement) for basic set-theoretic constructions +such as intersection, Cartesian Product and image.*} + ML {* val Inter_separation = thm "Inter_separation"; @@ -481,119 +485,119 @@ well_ord_iso_separation, obase_separation, obase_equals_separation, omap_replacement, is_recfun_separation] -fun axiomsL th = - kill_flex_triv_prems (m_axioms MRS (trivaxL th)); +fun axioms_L th = + kill_flex_triv_prems (m_axioms MRS (triv_axioms_L th)); -bind_thm ("cartprod_iff", axiomsL (thm "M_axioms.cartprod_iff")); -bind_thm ("cartprod_closed", axiomsL (thm "M_axioms.cartprod_closed")); -bind_thm ("sum_closed", axiomsL (thm "M_axioms.sum_closed")); -bind_thm ("M_converse_iff", axiomsL (thm "M_axioms.M_converse_iff")); -bind_thm ("converse_closed", axiomsL (thm "M_axioms.converse_closed")); -bind_thm ("converse_abs", axiomsL (thm "M_axioms.converse_abs")); -bind_thm ("image_closed", axiomsL (thm "M_axioms.image_closed")); -bind_thm ("vimage_abs", axiomsL (thm "M_axioms.vimage_abs")); -bind_thm ("vimage_closed", axiomsL (thm "M_axioms.vimage_closed")); -bind_thm ("domain_abs", axiomsL (thm "M_axioms.domain_abs")); -bind_thm ("domain_closed", axiomsL (thm "M_axioms.domain_closed")); -bind_thm ("range_abs", axiomsL (thm "M_axioms.range_abs")); -bind_thm ("range_closed", axiomsL (thm "M_axioms.range_closed")); -bind_thm ("field_abs", axiomsL (thm "M_axioms.field_abs")); -bind_thm ("field_closed", axiomsL (thm "M_axioms.field_closed")); -bind_thm ("relation_abs", axiomsL (thm "M_axioms.relation_abs")); -bind_thm ("function_abs", axiomsL (thm "M_axioms.function_abs")); -bind_thm ("apply_closed", axiomsL (thm "M_axioms.apply_closed")); -bind_thm ("apply_abs", axiomsL (thm "M_axioms.apply_abs")); -bind_thm ("typed_function_abs", axiomsL (thm "M_axioms.typed_function_abs")); -bind_thm ("injection_abs", axiomsL (thm "M_axioms.injection_abs")); -bind_thm ("surjection_abs", axiomsL (thm "M_axioms.surjection_abs")); -bind_thm ("bijection_abs", axiomsL (thm "M_axioms.bijection_abs")); -bind_thm ("M_comp_iff", axiomsL (thm "M_axioms.M_comp_iff")); -bind_thm ("comp_closed", axiomsL (thm "M_axioms.comp_closed")); -bind_thm ("composition_abs", axiomsL (thm "M_axioms.composition_abs")); -bind_thm ("restriction_is_function", axiomsL (thm "M_axioms.restriction_is_function")); -bind_thm ("restriction_abs", axiomsL (thm "M_axioms.restriction_abs")); -bind_thm ("M_restrict_iff", axiomsL (thm "M_axioms.M_restrict_iff")); -bind_thm ("restrict_closed", axiomsL (thm "M_axioms.restrict_closed")); -bind_thm ("Inter_abs", axiomsL (thm "M_axioms.Inter_abs")); -bind_thm ("Inter_closed", axiomsL (thm "M_axioms.Inter_closed")); -bind_thm ("Int_closed", axiomsL (thm "M_axioms.Int_closed")); -bind_thm ("finite_fun_closed", axiomsL (thm "M_axioms.finite_fun_closed")); -bind_thm ("is_funspace_abs", axiomsL (thm "M_axioms.is_funspace_abs")); -bind_thm ("succ_fun_eq2", axiomsL (thm "M_axioms.succ_fun_eq2")); -bind_thm ("funspace_succ", axiomsL (thm "M_axioms.funspace_succ")); -bind_thm ("finite_funspace_closed", axiomsL (thm "M_axioms.finite_funspace_closed")); +bind_thm ("cartprod_iff", axioms_L (thm "M_axioms.cartprod_iff")); +bind_thm ("cartprod_closed", axioms_L (thm "M_axioms.cartprod_closed")); +bind_thm ("sum_closed", axioms_L (thm "M_axioms.sum_closed")); +bind_thm ("M_converse_iff", axioms_L (thm "M_axioms.M_converse_iff")); +bind_thm ("converse_closed", axioms_L (thm "M_axioms.converse_closed")); +bind_thm ("converse_abs", axioms_L (thm "M_axioms.converse_abs")); +bind_thm ("image_closed", axioms_L (thm "M_axioms.image_closed")); +bind_thm ("vimage_abs", axioms_L (thm "M_axioms.vimage_abs")); +bind_thm ("vimage_closed", axioms_L (thm "M_axioms.vimage_closed")); +bind_thm ("domain_abs", axioms_L (thm "M_axioms.domain_abs")); +bind_thm ("domain_closed", axioms_L (thm "M_axioms.domain_closed")); +bind_thm ("range_abs", axioms_L (thm "M_axioms.range_abs")); +bind_thm ("range_closed", axioms_L (thm "M_axioms.range_closed")); +bind_thm ("field_abs", axioms_L (thm "M_axioms.field_abs")); +bind_thm ("field_closed", axioms_L (thm "M_axioms.field_closed")); +bind_thm ("relation_abs", axioms_L (thm "M_axioms.relation_abs")); +bind_thm ("function_abs", axioms_L (thm "M_axioms.function_abs")); +bind_thm ("apply_closed", axioms_L (thm "M_axioms.apply_closed")); +bind_thm ("apply_abs", axioms_L (thm "M_axioms.apply_abs")); +bind_thm ("typed_function_abs", axioms_L (thm "M_axioms.typed_function_abs")); +bind_thm ("injection_abs", axioms_L (thm "M_axioms.injection_abs")); +bind_thm ("surjection_abs", axioms_L (thm "M_axioms.surjection_abs")); +bind_thm ("bijection_abs", axioms_L (thm "M_axioms.bijection_abs")); +bind_thm ("M_comp_iff", axioms_L (thm "M_axioms.M_comp_iff")); +bind_thm ("comp_closed", axioms_L (thm "M_axioms.comp_closed")); +bind_thm ("composition_abs", axioms_L (thm "M_axioms.composition_abs")); +bind_thm ("restriction_is_function", axioms_L (thm "M_axioms.restriction_is_function")); +bind_thm ("restriction_abs", axioms_L (thm "M_axioms.restriction_abs")); +bind_thm ("M_restrict_iff", axioms_L (thm "M_axioms.M_restrict_iff")); +bind_thm ("restrict_closed", axioms_L (thm "M_axioms.restrict_closed")); +bind_thm ("Inter_abs", axioms_L (thm "M_axioms.Inter_abs")); +bind_thm ("Inter_closed", axioms_L (thm "M_axioms.Inter_closed")); +bind_thm ("Int_closed", axioms_L (thm "M_axioms.Int_closed")); +bind_thm ("finite_fun_closed", axioms_L (thm "M_axioms.finite_fun_closed")); +bind_thm ("is_funspace_abs", axioms_L (thm "M_axioms.is_funspace_abs")); +bind_thm ("succ_fun_eq2", axioms_L (thm "M_axioms.succ_fun_eq2")); +bind_thm ("funspace_succ", axioms_L (thm "M_axioms.funspace_succ")); +bind_thm ("finite_funspace_closed", axioms_L (thm "M_axioms.finite_funspace_closed")); *} ML {* -bind_thm ("is_recfun_equal", axiomsL (thm "M_axioms.is_recfun_equal")); -bind_thm ("is_recfun_cut", axiomsL (thm "M_axioms.is_recfun_cut")); -bind_thm ("is_recfun_functional", axiomsL (thm "M_axioms.is_recfun_functional")); -bind_thm ("is_recfun_relativize", axiomsL (thm "M_axioms.is_recfun_relativize")); -bind_thm ("is_recfun_restrict", axiomsL (thm "M_axioms.is_recfun_restrict")); -bind_thm ("univalent_is_recfun", axiomsL (thm "M_axioms.univalent_is_recfun")); -bind_thm ("exists_is_recfun_indstep", axiomsL (thm "M_axioms.exists_is_recfun_indstep")); -bind_thm ("wellfounded_exists_is_recfun", axiomsL (thm "M_axioms.wellfounded_exists_is_recfun")); -bind_thm ("wf_exists_is_recfun", axiomsL (thm "M_axioms.wf_exists_is_recfun")); -bind_thm ("is_recfun_abs", axiomsL (thm "M_axioms.is_recfun_abs")); -bind_thm ("irreflexive_abs", axiomsL (thm "M_axioms.irreflexive_abs")); -bind_thm ("transitive_rel_abs", axiomsL (thm "M_axioms.transitive_rel_abs")); -bind_thm ("linear_rel_abs", axiomsL (thm "M_axioms.linear_rel_abs")); -bind_thm ("wellordered_is_trans_on", axiomsL (thm "M_axioms.wellordered_is_trans_on")); -bind_thm ("wellordered_is_linear", axiomsL (thm "M_axioms.wellordered_is_linear")); -bind_thm ("wellordered_is_wellfounded_on", axiomsL (thm "M_axioms.wellordered_is_wellfounded_on")); -bind_thm ("wellfounded_imp_wellfounded_on", axiomsL (thm "M_axioms.wellfounded_imp_wellfounded_on")); -bind_thm ("wellfounded_on_subset_A", axiomsL (thm "M_axioms.wellfounded_on_subset_A")); -bind_thm ("wellfounded_on_iff_wellfounded", axiomsL (thm "M_axioms.wellfounded_on_iff_wellfounded")); -bind_thm ("wellfounded_on_imp_wellfounded", axiomsL (thm "M_axioms.wellfounded_on_imp_wellfounded")); -bind_thm ("wellfounded_on_field_imp_wellfounded", axiomsL (thm "M_axioms.wellfounded_on_field_imp_wellfounded")); -bind_thm ("wellfounded_iff_wellfounded_on_field", axiomsL (thm "M_axioms.wellfounded_iff_wellfounded_on_field")); -bind_thm ("wellfounded_induct", axiomsL (thm "M_axioms.wellfounded_induct")); -bind_thm ("wellfounded_on_induct", axiomsL (thm "M_axioms.wellfounded_on_induct")); -bind_thm ("wellfounded_on_induct2", axiomsL (thm "M_axioms.wellfounded_on_induct2")); -bind_thm ("linear_imp_relativized", axiomsL (thm "M_axioms.linear_imp_relativized")); -bind_thm ("trans_on_imp_relativized", axiomsL (thm "M_axioms.trans_on_imp_relativized")); -bind_thm ("wf_on_imp_relativized", axiomsL (thm "M_axioms.wf_on_imp_relativized")); -bind_thm ("wf_imp_relativized", axiomsL (thm "M_axioms.wf_imp_relativized")); -bind_thm ("well_ord_imp_relativized", axiomsL (thm "M_axioms.well_ord_imp_relativized")); -bind_thm ("order_isomorphism_abs", axiomsL (thm "M_axioms.order_isomorphism_abs")); -bind_thm ("pred_set_abs", axiomsL (thm "M_axioms.pred_set_abs")); +bind_thm ("is_recfun_equal", axioms_L (thm "M_axioms.is_recfun_equal")); +bind_thm ("is_recfun_cut", axioms_L (thm "M_axioms.is_recfun_cut")); +bind_thm ("is_recfun_functional", axioms_L (thm "M_axioms.is_recfun_functional")); +bind_thm ("is_recfun_relativize", axioms_L (thm "M_axioms.is_recfun_relativize")); +bind_thm ("is_recfun_restrict", axioms_L (thm "M_axioms.is_recfun_restrict")); +bind_thm ("univalent_is_recfun", axioms_L (thm "M_axioms.univalent_is_recfun")); +bind_thm ("exists_is_recfun_indstep", axioms_L (thm "M_axioms.exists_is_recfun_indstep")); +bind_thm ("wellfounded_exists_is_recfun", axioms_L (thm "M_axioms.wellfounded_exists_is_recfun")); +bind_thm ("wf_exists_is_recfun", axioms_L (thm "M_axioms.wf_exists_is_recfun")); +bind_thm ("is_recfun_abs", axioms_L (thm "M_axioms.is_recfun_abs")); +bind_thm ("irreflexive_abs", axioms_L (thm "M_axioms.irreflexive_abs")); +bind_thm ("transitive_rel_abs", axioms_L (thm "M_axioms.transitive_rel_abs")); +bind_thm ("linear_rel_abs", axioms_L (thm "M_axioms.linear_rel_abs")); +bind_thm ("wellordered_is_trans_on", axioms_L (thm "M_axioms.wellordered_is_trans_on")); +bind_thm ("wellordered_is_linear", axioms_L (thm "M_axioms.wellordered_is_linear")); +bind_thm ("wellordered_is_wellfounded_on", axioms_L (thm "M_axioms.wellordered_is_wellfounded_on")); +bind_thm ("wellfounded_imp_wellfounded_on", axioms_L (thm "M_axioms.wellfounded_imp_wellfounded_on")); +bind_thm ("wellfounded_on_subset_A", axioms_L (thm "M_axioms.wellfounded_on_subset_A")); +bind_thm ("wellfounded_on_iff_wellfounded", axioms_L (thm "M_axioms.wellfounded_on_iff_wellfounded")); +bind_thm ("wellfounded_on_imp_wellfounded", axioms_L (thm "M_axioms.wellfounded_on_imp_wellfounded")); +bind_thm ("wellfounded_on_field_imp_wellfounded", axioms_L (thm "M_axioms.wellfounded_on_field_imp_wellfounded")); +bind_thm ("wellfounded_iff_wellfounded_on_field", axioms_L (thm "M_axioms.wellfounded_iff_wellfounded_on_field")); +bind_thm ("wellfounded_induct", axioms_L (thm "M_axioms.wellfounded_induct")); +bind_thm ("wellfounded_on_induct", axioms_L (thm "M_axioms.wellfounded_on_induct")); +bind_thm ("wellfounded_on_induct2", axioms_L (thm "M_axioms.wellfounded_on_induct2")); +bind_thm ("linear_imp_relativized", axioms_L (thm "M_axioms.linear_imp_relativized")); +bind_thm ("trans_on_imp_relativized", axioms_L (thm "M_axioms.trans_on_imp_relativized")); +bind_thm ("wf_on_imp_relativized", axioms_L (thm "M_axioms.wf_on_imp_relativized")); +bind_thm ("wf_imp_relativized", axioms_L (thm "M_axioms.wf_imp_relativized")); +bind_thm ("well_ord_imp_relativized", axioms_L (thm "M_axioms.well_ord_imp_relativized")); +bind_thm ("order_isomorphism_abs", axioms_L (thm "M_axioms.order_isomorphism_abs")); +bind_thm ("pred_set_abs", axioms_L (thm "M_axioms.pred_set_abs")); *} ML {* -bind_thm ("pred_closed", axiomsL (thm "M_axioms.pred_closed")); -bind_thm ("membership_abs", axiomsL (thm "M_axioms.membership_abs")); -bind_thm ("M_Memrel_iff", axiomsL (thm "M_axioms.M_Memrel_iff")); -bind_thm ("Memrel_closed", axiomsL (thm "M_axioms.Memrel_closed")); -bind_thm ("wellordered_iso_predD", axiomsL (thm "M_axioms.wellordered_iso_predD")); -bind_thm ("wellordered_iso_pred_eq", axiomsL (thm "M_axioms.wellordered_iso_pred_eq")); -bind_thm ("wellfounded_on_asym", axiomsL (thm "M_axioms.wellfounded_on_asym")); -bind_thm ("wellordered_asym", axiomsL (thm "M_axioms.wellordered_asym")); -bind_thm ("ord_iso_pred_imp_lt", axiomsL (thm "M_axioms.ord_iso_pred_imp_lt")); -bind_thm ("obase_iff", axiomsL (thm "M_axioms.obase_iff")); -bind_thm ("omap_iff", axiomsL (thm "M_axioms.omap_iff")); -bind_thm ("omap_unique", axiomsL (thm "M_axioms.omap_unique")); -bind_thm ("omap_yields_Ord", axiomsL (thm "M_axioms.omap_yields_Ord")); -bind_thm ("otype_iff", axiomsL (thm "M_axioms.otype_iff")); -bind_thm ("otype_eq_range", axiomsL (thm "M_axioms.otype_eq_range")); -bind_thm ("Ord_otype", axiomsL (thm "M_axioms.Ord_otype")); -bind_thm ("domain_omap", axiomsL (thm "M_axioms.domain_omap")); -bind_thm ("omap_subset", axiomsL (thm "M_axioms.omap_subset")); -bind_thm ("omap_funtype", axiomsL (thm "M_axioms.omap_funtype")); -bind_thm ("wellordered_omap_bij", axiomsL (thm "M_axioms.wellordered_omap_bij")); -bind_thm ("omap_ord_iso", axiomsL (thm "M_axioms.omap_ord_iso")); -bind_thm ("Ord_omap_image_pred", axiomsL (thm "M_axioms.Ord_omap_image_pred")); -bind_thm ("restrict_omap_ord_iso", axiomsL (thm "M_axioms.restrict_omap_ord_iso")); -bind_thm ("obase_equals", axiomsL (thm "M_axioms.obase_equals")); -bind_thm ("omap_ord_iso_otype", axiomsL (thm "M_axioms.omap_ord_iso_otype")); -bind_thm ("obase_exists", axiomsL (thm "M_axioms.obase_exists")); -bind_thm ("omap_exists", axiomsL (thm "M_axioms.omap_exists")); -bind_thm ("otype_exists", axiomsL (thm "M_axioms.otype_exists")); -bind_thm ("omap_ord_iso_otype", axiomsL (thm "M_axioms.omap_ord_iso_otype")); -bind_thm ("ordertype_exists", axiomsL (thm "M_axioms.ordertype_exists")); -bind_thm ("relativized_imp_well_ord", axiomsL (thm "M_axioms.relativized_imp_well_ord")); -bind_thm ("well_ord_abs", axiomsL (thm "M_axioms.well_ord_abs")); +bind_thm ("pred_closed", axioms_L (thm "M_axioms.pred_closed")); +bind_thm ("membership_abs", axioms_L (thm "M_axioms.membership_abs")); +bind_thm ("M_Memrel_iff", axioms_L (thm "M_axioms.M_Memrel_iff")); +bind_thm ("Memrel_closed", axioms_L (thm "M_axioms.Memrel_closed")); +bind_thm ("wellordered_iso_predD", axioms_L (thm "M_axioms.wellordered_iso_predD")); +bind_thm ("wellordered_iso_pred_eq", axioms_L (thm "M_axioms.wellordered_iso_pred_eq")); +bind_thm ("wellfounded_on_asym", axioms_L (thm "M_axioms.wellfounded_on_asym")); +bind_thm ("wellordered_asym", axioms_L (thm "M_axioms.wellordered_asym")); +bind_thm ("ord_iso_pred_imp_lt", axioms_L (thm "M_axioms.ord_iso_pred_imp_lt")); +bind_thm ("obase_iff", axioms_L (thm "M_axioms.obase_iff")); +bind_thm ("omap_iff", axioms_L (thm "M_axioms.omap_iff")); +bind_thm ("omap_unique", axioms_L (thm "M_axioms.omap_unique")); +bind_thm ("omap_yields_Ord", axioms_L (thm "M_axioms.omap_yields_Ord")); +bind_thm ("otype_iff", axioms_L (thm "M_axioms.otype_iff")); +bind_thm ("otype_eq_range", axioms_L (thm "M_axioms.otype_eq_range")); +bind_thm ("Ord_otype", axioms_L (thm "M_axioms.Ord_otype")); +bind_thm ("domain_omap", axioms_L (thm "M_axioms.domain_omap")); +bind_thm ("omap_subset", axioms_L (thm "M_axioms.omap_subset")); +bind_thm ("omap_funtype", axioms_L (thm "M_axioms.omap_funtype")); +bind_thm ("wellordered_omap_bij", axioms_L (thm "M_axioms.wellordered_omap_bij")); +bind_thm ("omap_ord_iso", axioms_L (thm "M_axioms.omap_ord_iso")); +bind_thm ("Ord_omap_image_pred", axioms_L (thm "M_axioms.Ord_omap_image_pred")); +bind_thm ("restrict_omap_ord_iso", axioms_L (thm "M_axioms.restrict_omap_ord_iso")); +bind_thm ("obase_equals", axioms_L (thm "M_axioms.obase_equals")); +bind_thm ("omap_ord_iso_otype", axioms_L (thm "M_axioms.omap_ord_iso_otype")); +bind_thm ("obase_exists", axioms_L (thm "M_axioms.obase_exists")); +bind_thm ("omap_exists", axioms_L (thm "M_axioms.omap_exists")); +bind_thm ("otype_exists", axioms_L (thm "M_axioms.otype_exists")); +bind_thm ("omap_ord_iso_otype", axioms_L (thm "M_axioms.omap_ord_iso_otype")); +bind_thm ("ordertype_exists", axioms_L (thm "M_axioms.ordertype_exists")); +bind_thm ("relativized_imp_well_ord", axioms_L (thm "M_axioms.relativized_imp_well_ord")); +bind_thm ("well_ord_abs", axioms_L (thm "M_axioms.well_ord_abs")); *} declare cartprod_closed [intro,simp] diff -r cd7f9ea58338 -r c26eeb000470 src/ZF/Constructible/WF_absolute.thy --- a/src/ZF/Constructible/WF_absolute.thy Tue Jul 16 16:28:49 2002 +0200 +++ b/src/ZF/Constructible/WF_absolute.thy Tue Jul 16 16:29:36 2002 +0200 @@ -611,19 +611,6 @@ apply (simp add: wfrec_relativize, blast) done -lemma (in M_wfrank) wfrec_closed_lemma [rule_format]: - "[|wf(r); M(r); - strong_replacement(M, \x y. y = \x, wfrec(r, x, H)\); - \x[M]. \g[M]. function(g) --> M(H(x,g)) |] - ==> M(a) --> M(wfrec(r,a,H))" -apply (rule_tac a=a in wf_induct, assumption+) -apply (subst wfrec, assumption, clarify) -apply (drule_tac x1=x and x="\x\r -`` {x}. wfrec(r, x, H)" - in rspec [THEN rspec]) -apply (simp_all add: function_lam) -apply (blast intro: dest: pair_components_in_M ) -done - text{*Full version not assuming transitivity, but maybe not very useful.*} theorem (in M_wfrank) wfrec_closed: "[|wf(r); M(r); M(a);