src/ZF/Constructible/Rec_Separation.thy
changeset 13395 4eb948d1eb4e
parent 13387 b7464ca2ebbb
child 13398 1cadd412da48
     1.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Thu Jul 18 12:10:24 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Thu Jul 18 15:21:42 2002 +0200
     1.3 @@ -1013,9 +1013,118 @@
     1.4  
     1.5  bind_thm ("list_closed", datatypes_L (thm "M_datatypes.list_closed"));
     1.6  bind_thm ("formula_closed", datatypes_L (thm "M_datatypes.formula_closed"));
     1.7 +bind_thm ("list_abs", datatypes_L (thm "M_datatypes.list_abs"));
     1.8 +bind_thm ("formula_abs", datatypes_L (thm "M_datatypes.formula_abs"));
     1.9  *}
    1.10  
    1.11  declare list_closed [intro,simp]
    1.12  declare formula_closed [intro,simp]
    1.13 +declare list_abs [intro,simp]
    1.14 +declare formula_abs [intro,simp]
    1.15 +
    1.16 +
    1.17 +
    1.18 +subsection{*@{term L} is Closed Under the Operator @{term eclose}*} 
    1.19 +
    1.20 +subsubsection{*Instances of Replacement for @{term eclose}*}
    1.21 +
    1.22 +lemma eclose_replacement1_Reflects:
    1.23 + "REFLECTS
    1.24 +   [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
    1.25 +         is_wfrec(L, iterates_MH(L, big_union(L), A), memsn, u, y)),
    1.26 +    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
    1.27 +         is_wfrec(**Lset(i), 
    1.28 +                  iterates_MH(**Lset(i), big_union(**Lset(i)), A), 
    1.29 +                  memsn, u, y))]"
    1.30 +by (intro FOL_reflections function_reflections is_wfrec_reflection 
    1.31 +          iterates_MH_reflection) 
    1.32 +
    1.33 +lemma eclose_replacement1: 
    1.34 +   "L(A) ==> iterates_replacement(L, big_union(L), A)"
    1.35 +apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
    1.36 +apply (rule strong_replacementI) 
    1.37 +apply (rule rallI)
    1.38 +apply (rename_tac B)   
    1.39 +apply (rule separation_CollectI) 
    1.40 +apply (subgoal_tac "L(Memrel(succ(n)))") 
    1.41 +apply (rule_tac A="{B,A,n,z,Memrel(succ(n))}" in subset_LsetE, blast ) 
    1.42 +apply (rule ReflectsE [OF eclose_replacement1_Reflects], assumption)
    1.43 +apply (drule subset_Lset_ltD, assumption) 
    1.44 +apply (erule reflection_imp_L_separation)
    1.45 +  apply (simp_all add: lt_Ord2 Memrel_closed)
    1.46 +apply (elim conjE) 
    1.47 +apply (rule DPow_LsetI)
    1.48 +apply (rename_tac v) 
    1.49 +apply (rule bex_iff_sats conj_iff_sats)+
    1.50 +apply (rule_tac env = "[u,v,A,n,B,Memrel(succ(n))]" in mem_iff_sats)
    1.51 +apply (rule sep_rules | simp)+
    1.52 +txt{*Can't get sat rules to work for higher-order operators, so just expand them!*}
    1.53 +apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
    1.54 +apply (rule sep_rules big_union_iff_sats quasinat_iff_sats | simp)+
    1.55 +done
    1.56 +
    1.57 +
    1.58 +lemma eclose_replacement2_Reflects:
    1.59 + "REFLECTS
    1.60 +   [\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and>
    1.61 +         (\<exists>sn[L]. \<exists>msn[L]. successor(L, u, sn) \<and> membership(L, sn, msn) \<and>
    1.62 +           is_wfrec (L, iterates_MH (L, big_union(L), A),
    1.63 +                              msn, u, x)),
    1.64 +    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and>
    1.65 +         (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i). 
    1.66 +          successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and>
    1.67 +           is_wfrec (**Lset(i), 
    1.68 +                 iterates_MH (**Lset(i), big_union(**Lset(i)), A),
    1.69 +                     msn, u, x))]"
    1.70 +by (intro FOL_reflections function_reflections is_wfrec_reflection 
    1.71 +          iterates_MH_reflection) 
    1.72 +
    1.73 +
    1.74 +lemma eclose_replacement2: 
    1.75 +   "L(A) ==> strong_replacement(L, 
    1.76 +         \<lambda>n y. n\<in>nat & 
    1.77 +               (\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) &
    1.78 +               is_wfrec(L, iterates_MH(L,big_union(L), A), 
    1.79 +                        msn, n, y)))"
    1.80 +apply (rule strong_replacementI) 
    1.81 +apply (rule rallI)
    1.82 +apply (rename_tac B)   
    1.83 +apply (rule separation_CollectI) 
    1.84 +apply (rule_tac A="{A,B,z,nat}" in subset_LsetE) 
    1.85 +apply (blast intro: L_nat) 
    1.86 +apply (rule ReflectsE [OF eclose_replacement2_Reflects], assumption)
    1.87 +apply (drule subset_Lset_ltD, assumption) 
    1.88 +apply (erule reflection_imp_L_separation)
    1.89 +  apply (simp_all add: lt_Ord2)
    1.90 +apply (rule DPow_LsetI)
    1.91 +apply (rename_tac v) 
    1.92 +apply (rule bex_iff_sats conj_iff_sats)+
    1.93 +apply (rule_tac env = "[u,v,A,B,nat]" in mem_iff_sats)
    1.94 +apply (rule sep_rules | simp)+
    1.95 +apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
    1.96 +apply (rule sep_rules big_union_iff_sats quasinat_iff_sats | simp)+
    1.97 +done
    1.98 +
    1.99 +
   1.100 +subsubsection{*Instantiating the locale @{text M_eclose}*}
   1.101 +ML
   1.102 +{*
   1.103 +val eclose_replacement1 = thm "eclose_replacement1"; 
   1.104 +val eclose_replacement2 = thm "eclose_replacement2";
   1.105 +
   1.106 +val m_eclose = [eclose_replacement1, eclose_replacement2];
   1.107 +
   1.108 +fun eclose_L th =
   1.109 +    kill_flex_triv_prems (m_eclose MRS (wfrank_L th));
   1.110 +
   1.111 +bind_thm ("eclose_closed", eclose_L (thm "M_eclose.eclose_closed"));
   1.112 +bind_thm ("eclose_abs", eclose_L (thm "M_eclose.eclose_abs"));
   1.113 +*}
   1.114 +
   1.115 +declare eclose_closed [intro,simp]
   1.116 +declare eclose_abs [intro,simp]
   1.117 +
   1.118 +
   1.119 +
   1.120  
   1.121  end