# HG changeset patch # User paulson # Date 1035978258 -3600 # Node ID 22dce9134953726fc9b90664d4ce2b55f6903e88 # Parent bc63c3b2b3e78faa9138218942d83df5916f31fd simpler separation/replacement proofs diff -r bc63c3b2b3e7 -r 22dce9134953 src/ZF/Constructible/DPow_absolute.thy --- a/src/ZF/Constructible/DPow_absolute.thy Wed Oct 30 12:18:23 2002 +0100 +++ b/src/ZF/Constructible/DPow_absolute.thy Wed Oct 30 12:44:18 2002 +0100 @@ -181,7 +181,7 @@ done -subsection{*Additional Constraints on the Class Model @{term M}*} +subsection{*A Locale for Relativizing the Operator @{term DPow'}*} locale M_DPow = M_satisfies + assumes sep: @@ -242,12 +242,10 @@ lemma DPow_separation: "[| L(A); env \ list(A); p \ formula |] ==> separation(L, \x. is_DPow_body(L,A,env,p,x))" -apply (rule gen_separation [OF DPow_body_reflection, of "{A,env,p}"], - blast intro: transL) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule_tac env = "[x,A,env,p]" in DPow_body_iff_sats) -apply (rule sep_rules | simp)+ +apply (rule gen_separation_multi [OF DPow_body_reflection, of "{A,env,p}"], + auto intro: transL) +apply (rule_tac env="[A,env,p]" in DPow_LsetI) +apply (rule DPow_body_iff_sats sep_rules | simp)+ done @@ -276,14 +274,11 @@ pair(L,env,p,ep) & is_Collect(L, A, \x. is_DPow_body(L,A,env,p,x), z))" apply (rule strong_replacementI) -apply (rename_tac B) -apply (rule_tac u="{A,B}" in gen_separation [OF DPow_replacement_Reflects], - simp) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) +apply (rule_tac u="{A,B}" + in gen_separation_multi [OF DPow_replacement_Reflects], + auto) apply (unfold is_Collect_def) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[u,x,A,B]" in mem_iff_sats) +apply (rule_tac env="[A,B]" in DPow_LsetI) apply (rule sep_rules mem_formula_iff_sats mem_list_iff_sats DPow_body_iff_sats | simp)+ done @@ -452,13 +447,8 @@ mem_list_reflection Collect_reflection DPow_body_reflection) done -(*????????????????move up*) - - - - -subsection{*Additional Constraints on the Class Model @{term M}*} +subsection{*A Locale for Relativizing the Operator @{term Lset}*} constdefs transrec_body :: "[i=>o,i,i,i,i] => o" @@ -510,7 +500,7 @@ done - +text{*Relativization of the Operator @{term Lset}*} constdefs is_Lset :: "[i=>o, i, i] => o" @@ -534,7 +524,6 @@ subsection{*Instantiating the Locale @{text M_Lset}*} - subsubsection{*The First Instance of Replacement*} lemma strong_rep_Reflects: @@ -548,12 +537,9 @@ "[|L(x); L(g)|] ==> strong_replacement(L, \y z. transrec_body(L,g,x,y,z))" apply (unfold transrec_body_def) apply (rule strong_replacementI) -apply (rename_tac B) -apply (rule_tac u="{x,g,B}" in gen_separation [OF strong_rep_Reflects], simp) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[v,u,x,g,B]" in mem_iff_sats) +apply (rule_tac u="{x,g,B}" + in gen_separation_multi [OF strong_rep_Reflects], auto) +apply (rule_tac env="[x,g,B]" in DPow_LsetI) apply (rule sep_rules DPow'_iff_sats | simp)+ done @@ -590,13 +576,9 @@ apply (rule transrec_replacementI, assumption) apply (unfold transrec_body_def) apply (rule strong_replacementI) -apply (rename_tac B) apply (rule_tac u="{j,B,Memrel(eclose({j}))}" - in gen_separation [OF transrec_rep_Reflects], simp) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[v,x,j,B,Memrel(eclose({j}))]" in mem_iff_sats) + in gen_separation_multi [OF transrec_rep_Reflects], auto) +apply (rule_tac env="[j,B,Memrel(eclose({j}))]" in DPow_LsetI) apply (rule sep_rules is_wfrec_iff_sats Replace_iff_sats DPow'_iff_sats | simp)+ done diff -r bc63c3b2b3e7 -r 22dce9134953 src/ZF/Constructible/Datatype_absolute.thy --- a/src/ZF/Constructible/Datatype_absolute.thy Wed Oct 30 12:18:23 2002 +0100 +++ b/src/ZF/Constructible/Datatype_absolute.thy Wed Oct 30 12:44:18 2002 +0100 @@ -120,16 +120,16 @@ is_nat_case(M, v, \m u. \gm[M]. fun_apply(M,g,m,gm) & isF(gm,u), n, z)" + is_iterates :: "[i=>o, [i,i]=>o, i, i, i] => o" + "is_iterates(M,isF,v,n,Z) == + \sn[M]. \msn[M]. successor(M,n,sn) & membership(M,sn,msn) & + is_wfrec(M, iterates_MH(M,isF,v), msn, n, Z)" + iterates_replacement :: "[i=>o, [i,i]=>o, i] => o" "iterates_replacement(M,isF,v) == \n[M]. n\nat --> wfrec_replacement(M, iterates_MH(M,isF,v), Memrel(succ(n)))" - is_iterates :: "[i=>o, [i,i]=>o, i, i, i] => o" - "is_iterates(M,isF,v,n,Z) == - \sn[M]. \msn[M]. successor(M,n,sn) & membership(M,sn,msn) & - is_wfrec(M, iterates_MH(M,isF,v), msn, n, Z)" - lemma (in M_basic) iterates_MH_abs: "[| relation1(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)" diff -r bc63c3b2b3e7 -r 22dce9134953 src/ZF/Constructible/Formula.thy --- a/src/ZF/Constructible/Formula.thy Wed Oct 30 12:18:23 2002 +0100 +++ b/src/ZF/Constructible/Formula.thy Wed Oct 30 12:44:18 2002 +0100 @@ -246,12 +246,12 @@ subsection{*Renaming Some de Bruijn Variables*} constdefs incr_var :: "[i,i]=>i" - "incr_var(x,lev) == if x incr_var(x,lev) = x" +lemma incr_var_lt: "x incr_var(x,nq) = x" by (simp add: incr_var_def) -lemma incr_var_le: "lev\x ==> incr_var(x,lev) = succ(x)" +lemma incr_var_le: "nq\x ==> incr_var(x,nq) = succ(x)" apply (simp add: incr_var_def) apply (blast dest: lt_trans1) done @@ -259,19 +259,19 @@ consts incr_bv :: "i=>i" primrec "incr_bv(Member(x,y)) = - (\lev \ nat. Member (incr_var(x,lev), incr_var(y,lev)))" + (\nq \ nat. Member (incr_var(x,nq), incr_var(y,nq)))" "incr_bv(Equal(x,y)) = - (\lev \ nat. Equal (incr_var(x,lev), incr_var(y,lev)))" + (\nq \ nat. Equal (incr_var(x,nq), incr_var(y,nq)))" "incr_bv(Nand(p,q)) = - (\lev \ nat. Nand (incr_bv(p)`lev, incr_bv(q)`lev))" + (\nq \ nat. Nand (incr_bv(p)`nq, incr_bv(q)`nq))" "incr_bv(Forall(p)) = - (\lev \ nat. Forall (incr_bv(p) ` succ(lev)))" + (\nq \ nat. Forall (incr_bv(p) ` succ(nq)))" -lemma [TC]: "x \ nat ==> incr_var(x,lev) \ nat" +lemma [TC]: "x \ nat ==> incr_var(x,nq) \ nat" by (simp add: incr_var_def) lemma incr_bv_type [TC]: "p \ formula ==> incr_bv(p) \ nat -> formula" @@ -294,8 +294,8 @@ (*the following two lemmas prevent huge case splits in arity_incr_bv_lemma*) lemma incr_var_lemma: - "[| x \ nat; y \ nat; lev \ x |] - ==> succ(x) \ incr_var(y,lev) = succ(x \ y)" + "[| x \ nat; y \ nat; nq \ x |] + ==> succ(x) \ incr_var(y,nq) = succ(x \ y)" apply (simp add: incr_var_def Ord_Un_if, auto) apply (blast intro: leI) apply (simp add: not_lt_iff_le) @@ -757,7 +757,7 @@ subsubsection{* Unions *} lemma Union_in_Lset: - "X \ Lset(j) ==> Union(X) \ Lset(succ(j))" + "X \ Lset(i) ==> Union(X) \ Lset(succ(i))" apply (insert Transset_Lset) apply (rule LsetI [OF succI1]) apply (simp add: Transset_def DPow_def) @@ -769,17 +769,8 @@ apply (simp add: succ_Un_distrib [symmetric], blast) done -lemma Union_in_LLimit: - "[| X: Lset(i); Limit(i) |] ==> Union(X) : Lset(i)" -apply (rule Limit_LsetE, assumption+) -apply (blast intro: Limit_has_succ lt_LsetI Union_in_Lset) -done - theorem Union_in_L: "L(X) ==> L(Union(X))" -apply (simp add: L_def, clarify) -apply (drule Ord_imp_greater_Limit) -apply (blast intro: lt_LsetI Union_in_LLimit Limit_is_Ord) -done +by (simp add: L_def, blast dest: Union_in_Lset) subsubsection{* Finite sets and ordered pairs *} diff -r bc63c3b2b3e7 -r 22dce9134953 src/ZF/Constructible/Rank_Separation.thy --- a/src/ZF/Constructible/Rank_Separation.thy Wed Oct 30 12:18:23 2002 +0100 +++ b/src/ZF/Constructible/Rank_Separation.thy Wed Oct 30 12:44:18 2002 +0100 @@ -10,7 +10,8 @@ text{*This theory proves all instances needed for locales - @{text "M_ordertype"} and @{text "M_wfrank"}*} + @{text "M_ordertype"} and @{text "M_wfrank"}. But the material is not + needed for proving the relative consistency of AC.*} subsection{*The Locale @{text "M_ordertype"}*} @@ -27,11 +28,9 @@ "[| L(A); L(f); L(r) |] ==> separation (L, \x. x\A --> (\y[L]. (\p[L]. fun_apply(L,f,x,y) & pair(L,y,x,p) & p \ r)))" -apply (rule gen_separation [OF well_ord_iso_Reflects, of "{A,f,r}"], simp) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule imp_iff_sats) -apply (rule_tac env = "[x,A,f,r]" in mem_iff_sats) +apply (rule gen_separation_multi [OF well_ord_iso_Reflects, of "{A,f,r}"], + auto) +apply (rule_tac env="[A,f,r]" in DPow_LsetI) apply (rule sep_rules | simp)+ done @@ -53,12 +52,9 @@ ==> separation(L, \a. \x[L]. \g[L]. \mx[L]. \par[L]. ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))" -apply (rule gen_separation [OF obase_reflects, of "{A,r}"], simp) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[x,a,A,r]" in ordinal_iff_sats) -apply (rule sep_rules | simp)+ +apply (rule gen_separation_multi [OF obase_reflects, of "{A,r}"], auto) +apply (rule_tac env="[A,r]" in DPow_LsetI) +apply (rule ordinal_iff_sats sep_rules | simp)+ done @@ -81,11 +77,8 @@ ordinal(L,y) & (\my[L]. \pxr[L]. membership(L,y,my) & pred_set(L,A,x,r,pxr) & order_isomorphism(L,pxr,r,y,my,g))))" -apply (rule gen_separation [OF obase_equals_reflects, of "{A,r}"], simp) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule imp_iff_sats ball_iff_sats disj_iff_sats not_iff_sats)+ -apply (rule_tac env = "[x,A,r]" in mem_iff_sats) +apply (rule gen_separation_multi [OF obase_equals_reflects, of "{A,r}"], auto) +apply (rule_tac env="[A,r]" in DPow_LsetI) apply (rule sep_rules | simp)+ done @@ -110,12 +103,8 @@ ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) & pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))" apply (rule strong_replacementI) -apply (rename_tac B) -apply (rule_tac u="{A,r,B}" in gen_separation [OF omap_reflects], simp) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[a,z,A,B,r]" in mem_iff_sats) +apply (rule_tac u="{A,r,B}" in gen_separation_multi [OF omap_reflects], auto) +apply (rule_tac env="[A,B,r]" in DPow_LsetI) apply (rule sep_rules | simp)+ done @@ -157,10 +146,8 @@ separation (L, \x. \rplus[L]. tran_closure(L,r,rplus) --> ~ (\f[L]. M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f)))" apply (rule gen_separation [OF wfrank_Reflects], simp) -apply (rule DPow_LsetI) -apply (rule ball_iff_sats imp_iff_sats)+ -apply (rule_tac env="[rplus,x,r]" in tran_closure_iff_sats) -apply (rule sep_rules is_recfun_iff_sats | simp)+ +apply (rule_tac env="[r]" in DPow_LsetI) +apply (rule sep_rules tran_closure_iff_sats is_recfun_iff_sats | simp)+ done @@ -188,14 +175,11 @@ M_is_recfun(L, %x f y. is_range(L,f,y), rplus, x, f) & is_range(L,f,y)))" apply (rule strong_replacementI) -apply (rule_tac u="{r,A}" in gen_separation [OF wfrank_replacement_Reflects], - simp) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats ball_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[x,z,A,r]" in mem_iff_sats) -apply (rule sep_rules list.intros app_type tran_closure_iff_sats - is_recfun_iff_sats | simp)+ +apply (rule_tac u="{r,B}" + in gen_separation_multi [OF wfrank_replacement_Reflects], + auto) +apply (rule_tac env="[r,B]" in DPow_LsetI) +apply (rule sep_rules tran_closure_iff_sats is_recfun_iff_sats | simp)+ done @@ -225,10 +209,8 @@ M_is_recfun(L, \x f y. is_range(L,f,y), rplus, x, f) --> ordinal(L,rangef)))" apply (rule gen_separation [OF Ord_wfrank_Reflects], simp) -apply (rule DPow_LsetI) -apply (rule ball_iff_sats imp_iff_sats)+ -apply (rule_tac env="[rplus,x,r]" in tran_closure_iff_sats) -apply (rule sep_rules is_recfun_iff_sats | simp)+ +apply (rule_tac env="[r]" in DPow_LsetI) +apply (rule sep_rules tran_closure_iff_sats is_recfun_iff_sats | simp)+ done diff -r bc63c3b2b3e7 -r 22dce9134953 src/ZF/Constructible/Rec_Separation.thy --- a/src/ZF/Constructible/Rec_Separation.thy Wed Oct 30 12:18:23 2002 +0100 +++ b/src/ZF/Constructible/Rec_Separation.thy Wed Oct 30 12:44:18 2002 +0100 @@ -75,11 +75,10 @@ text{*Separation for @{term "rtrancl(r)"}.*} lemma rtrancl_separation: "[| L(r); L(A) |] ==> separation (L, rtran_closure_mem(L,A,r))" -apply (rule gen_separation [OF rtran_closure_mem_reflection, of "{r,A}"], simp) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule_tac env = "[x,r,A]" in rtran_closure_mem_iff_sats) -apply (rule sep_rules | simp)+ +apply (rule gen_separation_multi [OF rtran_closure_mem_reflection, of "{r,A}"], + auto) +apply (rule_tac env="[r,A]" in DPow_LsetI) +apply (rule rtran_closure_mem_iff_sats sep_rules | simp)+ done @@ -167,11 +166,9 @@ separation (L, \x. \w[L]. \wx[L]. \rp[L]. w \ Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \ rp)" -apply (rule gen_separation [OF wellfounded_trancl_reflects, of "{r,Z}"], simp) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[w,x,r,Z]" in mem_iff_sats) +apply (rule gen_separation_multi [OF wellfounded_trancl_reflects, of "{r,Z}"], + auto) +apply (rule_tac env="[r,Z]" in DPow_LsetI) apply (rule sep_rules tran_closure_iff_sats | simp)+ done @@ -214,14 +211,10 @@ "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 (rename_tac B) apply (rule_tac u="{B,A,n,0,Memrel(succ(n))}" - in gen_separation [OF list_replacement1_Reflects], - simp add: nonempty) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[u,x,A,n,B,0,Memrel(succ(n))]" in mem_iff_sats) + in gen_separation_multi [OF list_replacement1_Reflects], + auto simp add: nonempty) +apply (rule_tac env="[B,A,n,0,Memrel(succ(n))]" in DPow_LsetI) apply (rule sep_rules is_nat_case_iff_sats list_functor_iff_sats is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ done @@ -240,14 +233,10 @@ "L(A) ==> strong_replacement(L, \n y. n\nat & is_iterates(L, is_list_functor(L,A), 0, n, y))" apply (rule strong_replacementI) -apply (rename_tac B) apply (rule_tac u="{A,B,0,nat}" - in gen_separation [OF list_replacement2_Reflects], - simp add: L_nat nonempty) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[u,x,A,B,0,nat]" in mem_iff_sats) + in gen_separation_multi [OF list_replacement2_Reflects], + auto simp add: L_nat nonempty) +apply (rule_tac env="[A,B,0,nat]" in DPow_LsetI) apply (rule sep_rules list_functor_iff_sats is_iterates_iff_sats | simp)+ done @@ -273,14 +262,10 @@ "iterates_replacement(L, is_formula_functor(L), 0)" apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) apply (rule strong_replacementI) -apply (rename_tac B) apply (rule_tac u="{B,n,0,Memrel(succ(n))}" - in gen_separation [OF formula_replacement1_Reflects], - simp add: nonempty) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[u,x,n,B,0,Memrel(succ(n))]" in mem_iff_sats) + in gen_separation_multi [OF formula_replacement1_Reflects], + auto simp add: nonempty) +apply (rule_tac env="[n,B,0,Memrel(succ(n))]" in DPow_LsetI) apply (rule sep_rules is_nat_case_iff_sats formula_functor_iff_sats is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ done @@ -298,14 +283,10 @@ "strong_replacement(L, \n y. n\nat & is_iterates(L, is_formula_functor(L), 0, n, y))" apply (rule strong_replacementI) -apply (rename_tac B) apply (rule_tac u="{B,0,nat}" - in gen_separation [OF formula_replacement2_Reflects], - simp add: nonempty L_nat) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[u,x,B,0,nat]" in mem_iff_sats) + in gen_separation_multi [OF formula_replacement2_Reflects], + auto simp add: nonempty L_nat) +apply (rule_tac env="[B,0,nat]" in DPow_LsetI) apply (rule sep_rules formula_functor_iff_sats is_iterates_iff_sats | simp)+ done @@ -368,13 +349,10 @@ "L(w) ==> iterates_replacement(L, is_tl(L), w)" apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) apply (rule strong_replacementI) -apply (rule_tac u="{A,n,w,Memrel(succ(n))}" - in gen_separation [OF nth_replacement_Reflects], - simp add: nonempty) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[u,x,A,w,Memrel(succ(n))]" in mem_iff_sats) +apply (rule_tac u="{B,w,Memrel(succ(n))}" + in gen_separation_multi [OF nth_replacement_Reflects], + auto) +apply (rule_tac env="[B,w,Memrel(succ(n))]" in DPow_LsetI) apply (rule sep_rules is_nat_case_iff_sats tl_iff_sats is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+ done @@ -428,13 +406,9 @@ "L(A) ==> iterates_replacement(L, big_union(L), A)" apply (unfold iterates_replacement_def wfrec_replacement_def, clarify) apply (rule strong_replacementI) -apply (rename_tac B) apply (rule_tac u="{B,A,n,Memrel(succ(n))}" - in gen_separation [OF eclose_replacement1_Reflects], simp) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[u,x,A,n,B,Memrel(succ(n))]" in mem_iff_sats) + in gen_separation_multi [OF eclose_replacement1_Reflects], auto) +apply (rule_tac env="[B,A,n,Memrel(succ(n))]" in DPow_LsetI) apply (rule sep_rules iterates_MH_iff_sats is_nat_case_iff_sats is_wfrec_iff_sats big_union_iff_sats quasinat_iff_sats | simp)+ done @@ -452,13 +426,10 @@ "L(A) ==> strong_replacement(L, \n y. n\nat & is_iterates(L, big_union(L), A, n, y))" apply (rule strong_replacementI) -apply (rename_tac B) apply (rule_tac u="{A,B,nat}" - in gen_separation [OF eclose_replacement2_Reflects], simp add: L_nat) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[u,x,A,B,nat]" in mem_iff_sats) + in gen_separation_multi [OF eclose_replacement2_Reflects], + auto simp add: L_nat) +apply (rule_tac env="[A,B,nat]" in DPow_LsetI) apply (rule sep_rules is_iterates_iff_sats big_union_iff_sats | simp)+ done diff -r bc63c3b2b3e7 -r 22dce9134953 src/ZF/Constructible/Relative.thy --- a/src/ZF/Constructible/Relative.thy Wed Oct 30 12:18:23 2002 +0100 +++ b/src/ZF/Constructible/Relative.thy Wed Oct 30 12:44:18 2002 +0100 @@ -627,7 +627,7 @@ text{*Probably the premise and conclusion are equivalent*} lemma (in M_trivial) strong_replacementI [rule_format]: - "[| \A[M]. separation(M, %u. \x[M]. x\A & P(x,u)) |] + "[| \B[M]. separation(M, %u. \x[M]. x\B & P(x,u)) |] ==> strong_replacement(M,P)" apply (simp add: strong_replacement_def, clarify) apply (frule replacementD [OF replacement], assumption, clarify) diff -r bc63c3b2b3e7 -r 22dce9134953 src/ZF/Constructible/Satisfies_absolute.thy --- a/src/ZF/Constructible/Satisfies_absolute.thy Wed Oct 30 12:18:23 2002 +0100 +++ b/src/ZF/Constructible/Satisfies_absolute.thy Wed Oct 30 12:44:18 2002 +0100 @@ -8,6 +8,7 @@ theory Satisfies_absolute = Datatype_absolute + Rec_Separation: +subsection {*More Internalization*} subsubsection{*The Formula @{term is_depth}, Internalized*} @@ -823,14 +824,10 @@ is_bool_of_o(L, nx \ ny, bo) & pair(L, env, bo, z))" apply (rule strong_replacementI) -apply (rename_tac B) apply (rule_tac u="{list(A),B,x,y}" - in gen_separation [OF Member_Reflects], - simp add: nat_into_M list_closed) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[v,u,list(A),B,x,y]" in mem_iff_sats) + in gen_separation_multi [OF Member_Reflects], + auto simp add: nat_into_M list_closed) +apply (rule_tac env="[list(A),B,x,y]" in DPow_LsetI) apply (rule sep_rules nth_iff_sats is_bool_of_o_iff_sats | simp)+ done @@ -857,14 +854,10 @@ is_bool_of_o(L, nx = ny, bo) & pair(L, env, bo, z))" apply (rule strong_replacementI) -apply (rename_tac B) apply (rule_tac u="{list(A),B,x,y}" - in gen_separation [OF Equal_Reflects], - simp add: nat_into_M list_closed) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[v,u,list(A),B,x,y]" in mem_iff_sats) + in gen_separation_multi [OF Equal_Reflects], + auto simp add: nat_into_M list_closed) +apply (rule_tac env="[list(A),B,x,y]" in DPow_LsetI) apply (rule sep_rules nth_iff_sats is_bool_of_o_iff_sats | simp)+ done @@ -893,13 +886,10 @@ is_and(L,rpe,rqe,andpq) & is_not(L,andpq,notpq) & env \ list(A) & pair(L, env, notpq, z))" apply (rule strong_replacementI) -apply (rename_tac B) -apply (rule_tac u="{list(A),B,rp,rq}" in gen_separation [OF Nand_Reflects], - simp add: list_closed) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[u,x,list(A),B,rp,rq]" in mem_iff_sats) +apply (rule_tac u="{list(A),B,rp,rq}" + in gen_separation_multi [OF Nand_Reflects], + auto simp add: list_closed) +apply (rule_tac env="[list(A),B,rp,rq]" in DPow_LsetI) apply (rule sep_rules is_and_iff_sats is_not_iff_sats | simp)+ done @@ -935,13 +925,10 @@ bo) & pair(L,env,bo,z))" apply (rule strong_replacementI) -apply (rename_tac B) -apply (rule_tac u="{A,list(A),B,rp}" in gen_separation [OF Forall_Reflects], - simp add: list_closed) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[u,x,A,list(A),B,rp]" in mem_iff_sats) +apply (rule_tac u="{A,list(A),B,rp}" + in gen_separation_multi [OF Forall_Reflects], + auto simp add: list_closed) +apply (rule_tac env="[A,list(A),B,rp]" in DPow_LsetI) apply (rule sep_rules is_bool_of_o_iff_sats Cons_iff_sats | simp)+ done @@ -960,14 +947,10 @@ "[|n \ nat; L(A)|] ==> transrec_replacement(L, satisfies_MH(L,A), n)" apply (rule transrec_replacementI, simp add: nat_into_M) apply (rule strong_replacementI) -apply (rename_tac B) apply (rule_tac u="{B,A,n,Memrel(eclose({n}))}" - in gen_separation [OF formula_rec_replacement_Reflects], - simp add: nat_into_M) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[u,x,A,n,B,Memrel(eclose({n}))]" in mem_iff_sats) + in gen_separation_multi [OF formula_rec_replacement_Reflects], + auto simp add: nat_into_M) +apply (rule_tac env="[B,A,n,Memrel(eclose({n}))]" in DPow_LsetI) apply (rule sep_rules satisfies_MH_iff_sats is_wfrec_iff_sats | simp)+ done @@ -1006,13 +989,10 @@ satisfies_is_d(L,A,g), x, c) & pair(L, x, c, y)))" apply (rule strong_replacementI) -apply (rename_tac B) apply (rule_tac u="{B,A,g}" - in gen_separation [OF formula_rec_lambda_replacement_Reflects], simp) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[u,x,A,g,B]" in mem_iff_sats) + in gen_separation_multi [OF formula_rec_lambda_replacement_Reflects], + auto) +apply (rule_tac env="[A,g,B]" in DPow_LsetI) apply (rule sep_rules mem_formula_iff_sats formula_case_iff_sats satisfies_is_a_iff_sats satisfies_is_b_iff_sats satisfies_is_c_iff_sats diff -r bc63c3b2b3e7 -r 22dce9134953 src/ZF/Constructible/Separation.thy --- a/src/ZF/Constructible/Separation.thy Wed Oct 30 12:18:23 2002 +0100 +++ b/src/ZF/Constructible/Separation.thy Wed Oct 30 12:44:18 2002 +0100 @@ -51,7 +51,7 @@ done text{*Encapsulates the standard proof script for proving instances of -Separation. Typically @{term u} is a finite enumeration.*} + Separation.*} lemma gen_separation: assumes reflection: "REFLECTS [P,Q]" and Lu: "L(u)" @@ -65,7 +65,22 @@ apply (erule reflection_imp_L_separation) apply (simp_all add: lt_Ord2, clarify) apply (rule collI) -apply assumption; +apply assumption +done + +text{*As above, but typically @{term u} is a finite enumeration such as + @{term "{a,b}"}; thus the new subgoal gets the assumption + @{term "{a,b} \ Lset(i)"}, which is logically equivalent to + @{term "a \ Lset(i)"} and @{term "b \ Lset(i)"}.*} +lemma gen_separation_multi: + assumes reflection: "REFLECTS [P,Q]" + and Lu: "L(u)" + and collI: "!!j. u \ Lset(j) + \ Collect(Lset(j), Q(j)) \ DPow(Lset(j))" + shows "separation(L,P)" +apply (rule gen_separation [OF reflection Lu]) +apply (drule mem_Lset_imp_subset_Lset) +apply (erule collI) done @@ -80,6 +95,8 @@ "L(A) ==> separation(L, \x. \y[L]. y\A --> x\y)" apply (rule gen_separation [OF Inter_Reflects], simp) apply (rule DPow_LsetI) + txt{*I leave this one example of a manual proof. The tedium of manually + instantiating @{term i}, @{term j} and @{term env} is obvious. *} apply (rule ball_iff_sats) apply (rule imp_iff_sats) apply (rule_tac [2] i=1 and j=0 and env="[y,x,A]" in mem_iff_sats) @@ -96,9 +113,7 @@ lemma Diff_separation: "L(B) ==> separation(L, \x. x \ B)" apply (rule gen_separation [OF Diff_Reflects], simp) -apply (rule DPow_LsetI) -apply (rule not_iff_sats) -apply (rule_tac env="[x,B]" in mem_iff_sats) +apply (rule_tac env="[B]" in DPow_LsetI) apply (rule sep_rules | simp)+ done @@ -113,12 +128,8 @@ lemma cartprod_separation: "[| L(A); L(B) |] ==> separation(L, \z. \x[L]. x\A & (\y[L]. y\B & pair(L,x,y,z)))" -apply (rule gen_separation [OF cartprod_Reflects, of "{A,B}"], simp) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats) -apply (rule conj_iff_sats) -apply (rule_tac i=0 and j=2 and env="[x,z,A,B]" in mem_iff_sats, simp_all) +apply (rule gen_separation_multi [OF cartprod_Reflects, of "{A,B}"], auto) +apply (rule_tac env="[A,B]" in DPow_LsetI) apply (rule sep_rules | simp)+ done @@ -132,12 +143,8 @@ lemma image_separation: "[| L(A); L(r) |] ==> separation(L, \y. \p[L]. p\r & (\x[L]. x\A & pair(L,x,y,p)))" -apply (rule gen_separation [OF image_Reflects, of "{A,r}"], simp) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats) -apply (rule conj_iff_sats) -apply (rule_tac env="[p,y,A,r]" in mem_iff_sats) +apply (rule gen_separation_multi [OF image_Reflects, of "{A,r}"], auto) +apply (rule_tac env="[A,r]" in DPow_LsetI) apply (rule sep_rules | simp)+ done @@ -154,10 +161,7 @@ "L(r) ==> separation(L, \z. \p[L]. p\r & (\x[L]. \y[L]. pair(L,x,y,p) & pair(L,y,x,z)))" apply (rule gen_separation [OF converse_Reflects], simp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats) -apply (rule conj_iff_sats) -apply (rule_tac i=0 and j=2 and env="[p,z,r]" in mem_iff_sats, simp_all) +apply (rule_tac env="[r]" in DPow_LsetI) apply (rule sep_rules | simp)+ done @@ -172,10 +176,7 @@ lemma restrict_separation: "L(A) ==> separation(L, \z. \x[L]. x\A & (\y[L]. pair(L,x,y,z)))" apply (rule gen_separation [OF restrict_Reflects], simp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats) -apply (rule conj_iff_sats) -apply (rule_tac i=0 and j=2 and env="[x,z,A]" in mem_iff_sats, simp_all) +apply (rule_tac env="[A]" in DPow_LsetI) apply (rule sep_rules | simp)+ done @@ -196,15 +197,16 @@ ==> separation(L, \xz. \x[L]. \y[L]. \z[L]. \xy[L]. \yz[L]. pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) & xy\s & yz\r)" -apply (rule gen_separation [OF comp_Reflects, of "{r,s}"], simp) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats)+ -apply (rule conj_iff_sats) -apply (rule_tac env="[z,y,x,xz,r,s]" in pair_iff_sats) +apply (rule gen_separation_multi [OF comp_Reflects, of "{r,s}"], auto) +txt{*Subgoals after applying general ``separation'' rule: + @{subgoals[display,indent=0,margin=65]}*} +apply (rule_tac env="[r,s]" in DPow_LsetI) +txt{*Subgoals ready for automatic synthesis of a formula: + @{subgoals[display,indent=0,margin=65]}*} apply (rule sep_rules | simp)+ done + subsection{*Separation for Predecessors in an Order*} lemma pred_Reflects: @@ -214,12 +216,8 @@ lemma pred_separation: "[| L(r); L(x) |] ==> separation(L, \y. \p[L]. p\r & pair(L,y,x,p))" -apply (rule gen_separation [OF pred_Reflects, of "{r,x}"], simp) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats) -apply (rule conj_iff_sats) -apply (rule_tac env = "[p,y,r,x]" in mem_iff_sats) +apply (rule gen_separation_multi [OF pred_Reflects, of "{r,x}"], auto) +apply (rule_tac env="[r,x]" in DPow_LsetI) apply (rule sep_rules | simp)+ done @@ -234,9 +232,7 @@ lemma Memrel_separation: "separation(L, \z. \x[L]. \y[L]. pair(L,x,y,z) & x \ y)" apply (rule gen_separation [OF Memrel_Reflects nonempty]) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[y,x,z]" in pair_iff_sats) +apply (rule_tac env="[]" in DPow_LsetI) apply (rule sep_rules | simp)+ done @@ -259,12 +255,9 @@ pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) & upair(L,cnbf,cnbf,z))" apply (rule strong_replacementI) -apply (rule_tac u="{n,A}" in gen_separation [OF funspace_succ_Reflects], simp) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats) -apply (rule conj_iff_sats) -apply (rule_tac env = "[p,z,n,A]" in mem_iff_sats) +apply (rule_tac u="{n,B}" in gen_separation_multi [OF funspace_succ_Reflects], + auto) +apply (rule_tac env="[n,B]" in DPow_LsetI) apply (rule sep_rules | simp)+ done @@ -290,11 +283,9 @@ pair(L,x,a,xa) & xa \ r & pair(L,x,b,xb) & xb \ r & (\fx[L]. \gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) & fx \ gx))" -apply (rule gen_separation [OF is_recfun_reflects, of "{r,f,g,a,b}"], simp) -apply (drule mem_Lset_imp_subset_Lset, clarsimp) -apply (rule DPow_LsetI) -apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[xa,x,r,f,g,a,b]" in pair_iff_sats) +apply (rule gen_separation_multi [OF is_recfun_reflects, of "{r,f,g,a,b}"], + auto) +apply (rule_tac env="[r,f,g,a,b]" in DPow_LsetI) apply (rule sep_rules | simp)+ done