# HG changeset patch # User paulson # Date 1027587395 -7200 # Node ID af9bc8d87a75292e4ead9e38f203ecba027cd4c7 # Parent 8fcdf4a26468d4905d729ef75aab8f3bf3cef09b Added the assumption nth_replacement to locale M_datatypes. Moved up its proof to make it available for the instantiation of that locale. diff -r 8fcdf4a26468 -r af9bc8d87a75 src/ZF/Constructible/Datatype_absolute.thy --- a/src/ZF/Constructible/Datatype_absolute.thy Wed Jul 24 22:15:55 2002 +0200 +++ b/src/ZF/Constructible/Datatype_absolute.thy Thu Jul 25 10:56:35 2002 +0200 @@ -379,7 +379,9 @@ (\sn[M]. \msn[M]. successor(M,n,sn) & membership(M,sn,msn) & is_wfrec(M, iterates_MH(M,is_formula_functor(M), 0), msn, n, y)))" - + and nth_replacement: + "M(l) ==> iterates_replacement(M, %l t. is_tl(M,l,t), l)" + subsubsection{*Absoluteness of the List Construction*} @@ -649,14 +651,13 @@ is_hd(M,X,Z)" lemma (in M_datatypes) nth_abs [simp]: - "[|iterates_replacement(M, %l t. is_tl(M,l,t), l); - M(A); n \ nat; l \ list(A); M(Z)|] + "[|M(A); n \ nat; l \ list(A); M(Z)|] ==> is_nth(M,n,l,Z) <-> Z = nth(n,l)" apply (subgoal_tac "M(l)") prefer 2 apply (blast intro: transM) apply (simp add: is_nth_def nth_eq_hd_iterates_tl nat_into_M tl'_closed iterates_tl'_closed - iterates_abs [OF _ relativize1_tl]) + iterates_abs [OF _ relativize1_tl] nth_replacement) done diff -r 8fcdf4a26468 -r af9bc8d87a75 src/ZF/Constructible/Rec_Separation.thy --- a/src/ZF/Constructible/Rec_Separation.thy Wed Jul 24 22:15:55 2002 +0200 +++ b/src/ZF/Constructible/Rec_Separation.thy Thu Jul 25 10:56:35 2002 +0200 @@ -996,134 +996,6 @@ for @{term "list(A)"}. It was a cut-and-paste job! *} -subsubsection{*Instantiating the locale @{text M_datatypes}*} -ML -{* -val list_replacement1 = thm "list_replacement1"; -val list_replacement2 = thm "list_replacement2"; -val formula_replacement1 = thm "formula_replacement1"; -val formula_replacement2 = thm "formula_replacement2"; - -val m_datatypes = [list_replacement1, list_replacement2, - formula_replacement1, formula_replacement2]; - -fun datatypes_L th = - kill_flex_triv_prems (m_datatypes MRS (wfrank_L th)); - -bind_thm ("list_closed", datatypes_L (thm "M_datatypes.list_closed")); -bind_thm ("formula_closed", datatypes_L (thm "M_datatypes.formula_closed")); -bind_thm ("list_abs", datatypes_L (thm "M_datatypes.list_abs")); -bind_thm ("formula_abs", datatypes_L (thm "M_datatypes.formula_abs")); -*} - -declare list_closed [intro,simp] -declare formula_closed [intro,simp] -declare list_abs [intro,simp] -declare formula_abs [intro,simp] - - - -subsection{*@{term L} is Closed Under the Operator @{term eclose}*} - -subsubsection{*Instances of Replacement for @{term eclose}*} - -lemma eclose_replacement1_Reflects: - "REFLECTS - [\x. \u[L]. u \ B \ (\y[L]. pair(L,u,y,x) \ - is_wfrec(L, iterates_MH(L, big_union(L), A), 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), big_union(**Lset(i)), A), - memsn, u, y))]" -by (intro FOL_reflections function_reflections is_wfrec_reflection - iterates_MH_reflection) - -lemma eclose_replacement1: - "L(A) ==> iterates_replacement(L, big_union(L), A)" -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 (subgoal_tac "L(Memrel(succ(n)))") -apply (rule_tac A="{B,A,n,z,Memrel(succ(n))}" in subset_LsetE, blast ) -apply (rule ReflectsE [OF eclose_replacement1_Reflects], assumption) -apply (drule subset_Lset_ltD, assumption) -apply (erule reflection_imp_L_separation) - apply (simp_all add: lt_Ord2 Memrel_closed) -apply (elim conjE) -apply (rule DPow_LsetI) -apply (rename_tac v) -apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[u,v,A,n,B,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 big_union_iff_sats quasinat_iff_sats | simp)+ -done - - -lemma eclose_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, big_union(L), A), - 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), big_union(**Lset(i)), A), - msn, u, x))]" -by (intro FOL_reflections function_reflections is_wfrec_reflection - iterates_MH_reflection) - - -lemma eclose_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,big_union(L), A), - msn, n, y)))" -apply (rule strong_replacementI) -apply (rule rallI) -apply (rename_tac B) -apply (rule separation_CollectI) -apply (rule_tac A="{A,B,z,nat}" in subset_LsetE) -apply (blast intro: L_nat) -apply (rule ReflectsE [OF eclose_replacement2_Reflects], assumption) -apply (drule subset_Lset_ltD, assumption) -apply (erule reflection_imp_L_separation) - apply (simp_all add: lt_Ord2) -apply (rule DPow_LsetI) -apply (rename_tac v) -apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[u,v,A,B,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 big_union_iff_sats quasinat_iff_sats | simp)+ -done - - -subsubsection{*Instantiating the locale @{text M_eclose}*} -ML -{* -val eclose_replacement1 = thm "eclose_replacement1"; -val eclose_replacement2 = thm "eclose_replacement2"; - -val m_eclose = [eclose_replacement1, eclose_replacement2]; - -fun eclose_L th = - kill_flex_triv_prems (m_eclose MRS (datatypes_L th)); - -bind_thm ("eclose_closed", eclose_L (thm "M_eclose.eclose_closed")); -bind_thm ("eclose_abs", eclose_L (thm "M_eclose.eclose_abs")); -*} - -declare eclose_closed [intro,simp] -declare eclose_abs [intro,simp] - - subsection{*Internalized Forms of Data Structuring Operators*} subsubsection{*The Formula @{term is_Inl}, Internalized*} @@ -1212,7 +1084,7 @@ done -subsubsection{*The Formula @{term is_Nil}, Internalized*} +subsubsection{*The Formula @{term is_Cons}, Internalized*} (* "is_Cons(M,a,l,Z) == \p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)" *) @@ -1346,17 +1218,138 @@ apply (rule sep_rules quasinat_iff_sats tl_iff_sats | simp)+ done + + +subsubsection{*Instantiating the locale @{text M_datatypes}*} ML {* -bind_thm ("nth_abs_lemma", datatypes_L (thm "M_datatypes.nth_abs")); +val list_replacement1 = thm "list_replacement1"; +val list_replacement2 = thm "list_replacement2"; +val formula_replacement1 = thm "formula_replacement1"; +val formula_replacement2 = thm "formula_replacement2"; +val nth_replacement = thm "nth_replacement"; + +val m_datatypes = [list_replacement1, list_replacement2, + formula_replacement1, formula_replacement2, + nth_replacement]; + +fun datatypes_L th = + kill_flex_triv_prems (m_datatypes MRS (wfrank_L th)); + +bind_thm ("list_closed", datatypes_L (thm "M_datatypes.list_closed")); +bind_thm ("formula_closed", datatypes_L (thm "M_datatypes.formula_closed")); +bind_thm ("list_abs", datatypes_L (thm "M_datatypes.list_abs")); +bind_thm ("formula_abs", datatypes_L (thm "M_datatypes.formula_abs")); +bind_thm ("nth_abs", datatypes_L (thm "M_datatypes.nth_abs")); *} -text{*Instantiating theorem @{text nth_abs} for @{term L}*} -lemma nth_abs [simp]: - "[|L(A); n \ nat; l \ list(A); L(Z)|] - ==> is_nth(L,n,l,Z) <-> Z = nth(n,l)" -apply (rule nth_abs_lemma) -apply (blast intro: nth_replacement transL list_closed, assumption+) +declare list_closed [intro,simp] +declare formula_closed [intro,simp] +declare list_abs [simp] +declare formula_abs [simp] +declare nth_abs [simp] + + + +subsection{*@{term L} is Closed Under the Operator @{term eclose}*} + +subsubsection{*Instances of Replacement for @{term eclose}*} + +lemma eclose_replacement1_Reflects: + "REFLECTS + [\x. \u[L]. u \ B \ (\y[L]. pair(L,u,y,x) \ + is_wfrec(L, iterates_MH(L, big_union(L), A), 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), big_union(**Lset(i)), A), + memsn, u, y))]" +by (intro FOL_reflections function_reflections is_wfrec_reflection + iterates_MH_reflection) + +lemma eclose_replacement1: + "L(A) ==> iterates_replacement(L, big_union(L), A)" +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 (subgoal_tac "L(Memrel(succ(n)))") +apply (rule_tac A="{B,A,n,z,Memrel(succ(n))}" in subset_LsetE, blast ) +apply (rule ReflectsE [OF eclose_replacement1_Reflects], assumption) +apply (drule subset_Lset_ltD, assumption) +apply (erule reflection_imp_L_separation) + apply (simp_all add: lt_Ord2 Memrel_closed) +apply (elim conjE) +apply (rule DPow_LsetI) +apply (rename_tac v) +apply (rule bex_iff_sats conj_iff_sats)+ +apply (rule_tac env = "[u,v,A,n,B,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 big_union_iff_sats quasinat_iff_sats | simp)+ done + +lemma eclose_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, big_union(L), A), + 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), big_union(**Lset(i)), A), + msn, u, x))]" +by (intro FOL_reflections function_reflections is_wfrec_reflection + iterates_MH_reflection) + + +lemma eclose_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,big_union(L), A), + msn, n, y)))" +apply (rule strong_replacementI) +apply (rule rallI) +apply (rename_tac B) +apply (rule separation_CollectI) +apply (rule_tac A="{A,B,z,nat}" in subset_LsetE) +apply (blast intro: L_nat) +apply (rule ReflectsE [OF eclose_replacement2_Reflects], assumption) +apply (drule subset_Lset_ltD, assumption) +apply (erule reflection_imp_L_separation) + apply (simp_all add: lt_Ord2) +apply (rule DPow_LsetI) +apply (rename_tac v) +apply (rule bex_iff_sats conj_iff_sats)+ +apply (rule_tac env = "[u,v,A,B,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 big_union_iff_sats quasinat_iff_sats | simp)+ +done + + +subsubsection{*Instantiating the locale @{text M_eclose}*} +ML +{* +val eclose_replacement1 = thm "eclose_replacement1"; +val eclose_replacement2 = thm "eclose_replacement2"; + +val m_eclose = [eclose_replacement1, eclose_replacement2]; + +fun eclose_L th = + kill_flex_triv_prems (m_eclose MRS (datatypes_L th)); + +bind_thm ("eclose_closed", eclose_L (thm "M_eclose.eclose_closed")); +bind_thm ("eclose_abs", eclose_L (thm "M_eclose.eclose_abs")); +*} + +declare eclose_closed [intro,simp] +declare eclose_abs [intro,simp] + + end