absoluteness for "formula" and "eclose"
authorpaulson
Thu Jul 18 15:21:42 2002 +0200 (2002-07-18)
changeset 133954eb948d1eb4e
parent 13394 b39347206719
child 13396 11219ca224ab
absoluteness for "formula" and "eclose"
src/ZF/Constructible/Datatype_absolute.thy
src/ZF/Constructible/Rec_Separation.thy
     1.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Thu Jul 18 12:10:24 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Thu Jul 18 15:21:42 2002 +0200
     1.3 @@ -268,6 +268,39 @@
     1.4  
     1.5  
     1.6  subsection{*@{term M} Contains the List and Formula Datatypes*}
     1.7 +
     1.8 +constdefs
     1.9 +  is_list_n :: "[i=>o,i,i,i] => o"
    1.10 +    "is_list_n(M,A,n,Z) == 
    1.11 +      \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M]. 
    1.12 +       empty(M,zero) & 
    1.13 +       successor(M,n,sn) & membership(M,sn,msn) &
    1.14 +       is_wfrec(M, iterates_MH(M, is_list_functor(M,A),zero), msn, n, Z)"
    1.15 +  
    1.16 +  mem_list :: "[i=>o,i,i] => o"
    1.17 +    "mem_list(M,A,l) == 
    1.18 +      \<exists>n[M]. \<exists>listn[M]. 
    1.19 +       finite_ordinal(M,n) & is_list_n(M,A,n,listn) & l \<in> listn"
    1.20 +
    1.21 +  is_list :: "[i=>o,i,i] => o"
    1.22 +    "is_list(M,A,Z) == \<forall>l[M]. l \<in> Z <-> mem_list(M,A,l)"
    1.23 +
    1.24 +constdefs
    1.25 +  is_formula_n :: "[i=>o,i,i] => o"
    1.26 +    "is_formula_n(M,n,Z) == 
    1.27 +      \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M]. 
    1.28 +       empty(M,zero) & 
    1.29 +       successor(M,n,sn) & membership(M,sn,msn) &
    1.30 +       is_wfrec(M, iterates_MH(M, is_formula_functor(M),zero), msn, n, Z)"
    1.31 +  
    1.32 +  mem_formula :: "[i=>o,i] => o"
    1.33 +    "mem_formula(M,p) == 
    1.34 +      \<exists>n[M]. \<exists>formn[M]. 
    1.35 +       finite_ordinal(M,n) & is_formula_n(M,n,formn) & p \<in> formn"
    1.36 +
    1.37 +  is_formula :: "[i=>o,i] => o"
    1.38 +    "is_formula(M,Z) == \<forall>p[M]. p \<in> Z <-> mem_formula(M,p)"
    1.39 +
    1.40  locale (open) M_datatypes = M_wfrank +
    1.41   assumes list_replacement1: 
    1.42     "M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)"
    1.43 @@ -286,6 +319,9 @@
    1.44                 is_wfrec(M, iterates_MH(M,is_formula_functor(M), 0), 
    1.45                          msn, n, y)))"
    1.46  
    1.47 +
    1.48 +subsubsection{*Absoluteness of the List Construction*}
    1.49 +
    1.50  lemma (in M_datatypes) list_replacement2': 
    1.51    "M(A) ==> strong_replacement(M, \<lambda>n y. n\<in>nat & y = (\<lambda>X. {0} + A * X)^n (0))"
    1.52  apply (insert list_replacement2 [of A]) 
    1.53 @@ -300,7 +336,28 @@
    1.54  by  (simp add: RepFun_closed2 list_eq_Union 
    1.55                 list_replacement2' relativize1_def
    1.56                 iterates_closed [of "is_list_functor(M,A)"])
    1.57 +lemma (in M_datatypes) is_list_n_abs [simp]:
    1.58 +     "[|M(A); n\<in>nat; M(Z)|] 
    1.59 +      ==> is_list_n(M,A,n,Z) <-> Z = (\<lambda>X. {0} + A * X)^n (0)"
    1.60 +apply (insert list_replacement1)
    1.61 +apply (simp add: is_list_n_def relativize1_def nat_into_M
    1.62 +                 iterates_abs [of "is_list_functor(M,A)" _ "\<lambda>X. {0} + A*X"])
    1.63 +done
    1.64  
    1.65 +lemma (in M_datatypes) mem_list_abs [simp]:
    1.66 +     "M(A) ==> mem_list(M,A,l) <-> l \<in> list(A)"
    1.67 +apply (insert list_replacement1)
    1.68 +apply (simp add: mem_list_def relativize1_def list_eq_Union
    1.69 +                 iterates_closed [of "is_list_functor(M,A)"]) 
    1.70 +done
    1.71 +
    1.72 +lemma (in M_datatypes) list_abs [simp]:
    1.73 +     "[|M(A); M(Z)|] ==> is_list(M,A,Z) <-> Z = list(A)"
    1.74 +apply (simp add: is_list_def, safe)
    1.75 +apply (rule M_equalityI, simp_all)
    1.76 +done
    1.77 +
    1.78 +subsubsection{*Absoluteness of Formulas*}
    1.79  
    1.80  lemma (in M_datatypes) formula_replacement2': 
    1.81    "strong_replacement(M, \<lambda>n y. n\<in>nat & y = (\<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))^n (0))"
    1.82 @@ -318,4 +375,151 @@
    1.83                    iterates_closed [of "is_formula_functor(M)"])
    1.84  done
    1.85  
    1.86 +lemma (in M_datatypes) is_formula_n_abs [simp]:
    1.87 +     "[|n\<in>nat; M(Z)|] 
    1.88 +      ==> is_formula_n(M,n,Z) <-> 
    1.89 +          Z = (\<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))^n (0)"
    1.90 +apply (insert formula_replacement1)
    1.91 +apply (simp add: is_formula_n_def relativize1_def nat_into_M
    1.92 +                 iterates_abs [of "is_formula_functor(M)" _ 
    1.93 +                        "\<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X))"])
    1.94 +done
    1.95 +
    1.96 +lemma (in M_datatypes) mem_formula_abs [simp]:
    1.97 +     "mem_formula(M,l) <-> l \<in> formula"
    1.98 +apply (insert formula_replacement1)
    1.99 +apply (simp add: mem_formula_def relativize1_def formula_eq_Union
   1.100 +                 iterates_closed [of "is_formula_functor(M)"]) 
   1.101 +done
   1.102 +
   1.103 +lemma (in M_datatypes) formula_abs [simp]:
   1.104 +     "[|M(Z)|] ==> is_formula(M,Z) <-> Z = formula"
   1.105 +apply (simp add: is_formula_def, safe)
   1.106 +apply (rule M_equalityI, simp_all)
   1.107 +done
   1.108 +
   1.109 +
   1.110 +subsection{*Absoluteness for @{text \<epsilon>}-Closure: the @{term eclose} Operator*}
   1.111 +
   1.112 +text{*Re-expresses eclose using "iterates"*}
   1.113 +lemma eclose_eq_Union:
   1.114 +     "eclose(A) = (\<Union>n\<in>nat. Union^n (A))"
   1.115 +apply (simp add: eclose_def) 
   1.116 +apply (rule UN_cong) 
   1.117 +apply (rule refl)
   1.118 +apply (induct_tac n)
   1.119 +apply (simp add: nat_rec_0)  
   1.120 +apply (simp add: nat_rec_succ) 
   1.121 +done
   1.122 +
   1.123 +constdefs
   1.124 +  is_eclose_n :: "[i=>o,i,i,i] => o"
   1.125 +    "is_eclose_n(M,A,n,Z) == 
   1.126 +      \<exists>sn[M]. \<exists>msn[M]. 
   1.127 +       successor(M,n,sn) & membership(M,sn,msn) &
   1.128 +       is_wfrec(M, iterates_MH(M, big_union(M), A), msn, n, Z)"
   1.129 +  
   1.130 +  mem_eclose :: "[i=>o,i,i] => o"
   1.131 +    "mem_eclose(M,A,l) == 
   1.132 +      \<exists>n[M]. \<exists>eclosen[M]. 
   1.133 +       finite_ordinal(M,n) & is_eclose_n(M,A,n,eclosen) & l \<in> eclosen"
   1.134 +
   1.135 +  is_eclose :: "[i=>o,i,i] => o"
   1.136 +    "is_eclose(M,A,Z) == \<forall>u[M]. u \<in> Z <-> mem_eclose(M,A,u)"
   1.137 +
   1.138 +
   1.139 +locale (open) M_eclose = M_wfrank +
   1.140 + assumes eclose_replacement1: 
   1.141 +   "M(A) ==> iterates_replacement(M, big_union(M), A)"
   1.142 +  and eclose_replacement2: 
   1.143 +   "M(A) ==> strong_replacement(M, 
   1.144 +         \<lambda>n y. n\<in>nat & 
   1.145 +               (\<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
   1.146 +               is_wfrec(M, iterates_MH(M,big_union(M), A), 
   1.147 +                        msn, n, y)))"
   1.148 +
   1.149 +lemma (in M_eclose) eclose_replacement2': 
   1.150 +  "M(A) ==> strong_replacement(M, \<lambda>n y. n\<in>nat & y = Union^n (A))"
   1.151 +apply (insert eclose_replacement2 [of A]) 
   1.152 +apply (rule strong_replacement_cong [THEN iffD1])  
   1.153 +apply (rule conj_cong [OF iff_refl iterates_abs [of "big_union(M)"]]) 
   1.154 +apply (simp_all add: eclose_replacement1 relativize1_def) 
   1.155 +done
   1.156 +
   1.157 +lemma (in M_eclose) eclose_closed [intro,simp]:
   1.158 +     "M(A) ==> M(eclose(A))"
   1.159 +apply (insert eclose_replacement1)
   1.160 +by  (simp add: RepFun_closed2 eclose_eq_Union 
   1.161 +               eclose_replacement2' relativize1_def
   1.162 +               iterates_closed [of "big_union(M)"])
   1.163 +
   1.164 +lemma (in M_eclose) is_eclose_n_abs [simp]:
   1.165 +     "[|M(A); n\<in>nat; M(Z)|] ==> is_eclose_n(M,A,n,Z) <-> Z = Union^n (A)"
   1.166 +apply (insert eclose_replacement1)
   1.167 +apply (simp add: is_eclose_n_def relativize1_def nat_into_M
   1.168 +                 iterates_abs [of "big_union(M)" _ "Union"])
   1.169 +done
   1.170 +
   1.171 +lemma (in M_eclose) mem_eclose_abs [simp]:
   1.172 +     "M(A) ==> mem_eclose(M,A,l) <-> l \<in> eclose(A)"
   1.173 +apply (insert eclose_replacement1)
   1.174 +apply (simp add: mem_eclose_def relativize1_def eclose_eq_Union
   1.175 +                 iterates_closed [of "big_union(M)"]) 
   1.176 +done
   1.177 +
   1.178 +lemma (in M_eclose) eclose_abs [simp]:
   1.179 +     "[|M(A); M(Z)|] ==> is_eclose(M,A,Z) <-> Z = eclose(A)"
   1.180 +apply (simp add: is_eclose_def, safe)
   1.181 +apply (rule M_equalityI, simp_all)
   1.182 +done
   1.183 +
   1.184 +
   1.185 +
   1.186 +
   1.187 +subsection {*Absoluteness for @{term transrec}*}
   1.188 +
   1.189 +
   1.190 +text{* @{term "transrec(a,H) \<equiv> wfrec(Memrel(eclose({a})), a, H)"} *}
   1.191 +constdefs
   1.192 +
   1.193 +  is_transrec :: "[i=>o, [i,i,i]=>o, i, i] => o"
   1.194 +   "is_transrec(M,MH,a,z) == 
   1.195 +      \<exists>sa[M]. \<exists>esa[M]. \<exists>mesa[M]. 
   1.196 +       upair(M,a,a,sa) & is_eclose(M,sa,esa) & membership(M,esa,mesa) &
   1.197 +       is_wfrec(M,MH,mesa,a,z)"
   1.198 +
   1.199 +  transrec_replacement :: "[i=>o, [i,i,i]=>o, i] => o"
   1.200 +   "transrec_replacement(M,MH,a) ==
   1.201 +      \<exists>sa[M]. \<exists>esa[M]. \<exists>mesa[M]. 
   1.202 +       upair(M,a,a,sa) & is_eclose(M,sa,esa) & membership(M,esa,mesa) &
   1.203 +       wfrec_replacement(M,MH,mesa)"
   1.204 +
   1.205 +(*????????????????Ordinal.thy*)
   1.206 +lemma Transset_trans_Memrel: 
   1.207 +    "\<forall>j\<in>i. Transset(j) ==> trans(Memrel(i))"
   1.208 +by (unfold Transset_def trans_def, blast)
   1.209 +
   1.210 +text{*The condition @{term "Ord(i)"} lets us use the simpler 
   1.211 +  @{text "trans_wfrec_abs"} rather than @{text "trans_wfrec_abs"},
   1.212 +  which I haven't even proved yet. *}
   1.213 +theorem (in M_eclose) transrec_abs:
   1.214 +  "[|Ord(i);  M(i);  M(z);
   1.215 +     transrec_replacement(M,MH,i);  relativize2(M,MH,H);
   1.216 +     \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   1.217 +   ==> is_transrec(M,MH,i,z) <-> z = transrec(i,H)" 
   1.218 +by (simp add: trans_wfrec_abs transrec_replacement_def is_transrec_def
   1.219 +       transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
   1.220 +
   1.221 +
   1.222 +theorem (in M_eclose) transrec_closed:
   1.223 +     "[|Ord(i);  M(i);  M(z);
   1.224 +	transrec_replacement(M,MH,i);  relativize2(M,MH,H);
   1.225 +	\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
   1.226 +      ==> M(transrec(i,H))"
   1.227 +by (simp add: trans_wfrec_closed transrec_replacement_def is_transrec_def
   1.228 +       transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
   1.229 +
   1.230 +
   1.231 +
   1.232 +
   1.233  end
     2.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Thu Jul 18 12:10:24 2002 +0200
     2.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Thu Jul 18 15:21:42 2002 +0200
     2.3 @@ -1013,9 +1013,118 @@
     2.4  
     2.5  bind_thm ("list_closed", datatypes_L (thm "M_datatypes.list_closed"));
     2.6  bind_thm ("formula_closed", datatypes_L (thm "M_datatypes.formula_closed"));
     2.7 +bind_thm ("list_abs", datatypes_L (thm "M_datatypes.list_abs"));
     2.8 +bind_thm ("formula_abs", datatypes_L (thm "M_datatypes.formula_abs"));
     2.9  *}
    2.10  
    2.11  declare list_closed [intro,simp]
    2.12  declare formula_closed [intro,simp]
    2.13 +declare list_abs [intro,simp]
    2.14 +declare formula_abs [intro,simp]
    2.15 +
    2.16 +
    2.17 +
    2.18 +subsection{*@{term L} is Closed Under the Operator @{term eclose}*} 
    2.19 +
    2.20 +subsubsection{*Instances of Replacement for @{term eclose}*}
    2.21 +
    2.22 +lemma eclose_replacement1_Reflects:
    2.23 + "REFLECTS
    2.24 +   [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
    2.25 +         is_wfrec(L, iterates_MH(L, big_union(L), A), memsn, u, y)),
    2.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>
    2.27 +         is_wfrec(**Lset(i), 
    2.28 +                  iterates_MH(**Lset(i), big_union(**Lset(i)), A), 
    2.29 +                  memsn, u, y))]"
    2.30 +by (intro FOL_reflections function_reflections is_wfrec_reflection 
    2.31 +          iterates_MH_reflection) 
    2.32 +
    2.33 +lemma eclose_replacement1: 
    2.34 +   "L(A) ==> iterates_replacement(L, big_union(L), A)"
    2.35 +apply (unfold iterates_replacement_def wfrec_replacement_def, clarify)
    2.36 +apply (rule strong_replacementI) 
    2.37 +apply (rule rallI)
    2.38 +apply (rename_tac B)   
    2.39 +apply (rule separation_CollectI) 
    2.40 +apply (subgoal_tac "L(Memrel(succ(n)))") 
    2.41 +apply (rule_tac A="{B,A,n,z,Memrel(succ(n))}" in subset_LsetE, blast ) 
    2.42 +apply (rule ReflectsE [OF eclose_replacement1_Reflects], assumption)
    2.43 +apply (drule subset_Lset_ltD, assumption) 
    2.44 +apply (erule reflection_imp_L_separation)
    2.45 +  apply (simp_all add: lt_Ord2 Memrel_closed)
    2.46 +apply (elim conjE) 
    2.47 +apply (rule DPow_LsetI)
    2.48 +apply (rename_tac v) 
    2.49 +apply (rule bex_iff_sats conj_iff_sats)+
    2.50 +apply (rule_tac env = "[u,v,A,n,B,Memrel(succ(n))]" in mem_iff_sats)
    2.51 +apply (rule sep_rules | simp)+
    2.52 +txt{*Can't get sat rules to work for higher-order operators, so just expand them!*}
    2.53 +apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
    2.54 +apply (rule sep_rules big_union_iff_sats quasinat_iff_sats | simp)+
    2.55 +done
    2.56 +
    2.57 +
    2.58 +lemma eclose_replacement2_Reflects:
    2.59 + "REFLECTS
    2.60 +   [\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and>
    2.61 +         (\<exists>sn[L]. \<exists>msn[L]. successor(L, u, sn) \<and> membership(L, sn, msn) \<and>
    2.62 +           is_wfrec (L, iterates_MH (L, big_union(L), A),
    2.63 +                              msn, u, x)),
    2.64 +    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and>
    2.65 +         (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i). 
    2.66 +          successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and>
    2.67 +           is_wfrec (**Lset(i), 
    2.68 +                 iterates_MH (**Lset(i), big_union(**Lset(i)), A),
    2.69 +                     msn, u, x))]"
    2.70 +by (intro FOL_reflections function_reflections is_wfrec_reflection 
    2.71 +          iterates_MH_reflection) 
    2.72 +
    2.73 +
    2.74 +lemma eclose_replacement2: 
    2.75 +   "L(A) ==> strong_replacement(L, 
    2.76 +         \<lambda>n y. n\<in>nat & 
    2.77 +               (\<exists>sn[L]. \<exists>msn[L]. successor(L,n,sn) & membership(L,sn,msn) &
    2.78 +               is_wfrec(L, iterates_MH(L,big_union(L), A), 
    2.79 +                        msn, n, y)))"
    2.80 +apply (rule strong_replacementI) 
    2.81 +apply (rule rallI)
    2.82 +apply (rename_tac B)   
    2.83 +apply (rule separation_CollectI) 
    2.84 +apply (rule_tac A="{A,B,z,nat}" in subset_LsetE) 
    2.85 +apply (blast intro: L_nat) 
    2.86 +apply (rule ReflectsE [OF eclose_replacement2_Reflects], assumption)
    2.87 +apply (drule subset_Lset_ltD, assumption) 
    2.88 +apply (erule reflection_imp_L_separation)
    2.89 +  apply (simp_all add: lt_Ord2)
    2.90 +apply (rule DPow_LsetI)
    2.91 +apply (rename_tac v) 
    2.92 +apply (rule bex_iff_sats conj_iff_sats)+
    2.93 +apply (rule_tac env = "[u,v,A,B,nat]" in mem_iff_sats)
    2.94 +apply (rule sep_rules | simp)+
    2.95 +apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
    2.96 +apply (rule sep_rules big_union_iff_sats quasinat_iff_sats | simp)+
    2.97 +done
    2.98 +
    2.99 +
   2.100 +subsubsection{*Instantiating the locale @{text M_eclose}*}
   2.101 +ML
   2.102 +{*
   2.103 +val eclose_replacement1 = thm "eclose_replacement1"; 
   2.104 +val eclose_replacement2 = thm "eclose_replacement2";
   2.105 +
   2.106 +val m_eclose = [eclose_replacement1, eclose_replacement2];
   2.107 +
   2.108 +fun eclose_L th =
   2.109 +    kill_flex_triv_prems (m_eclose MRS (wfrank_L th));
   2.110 +
   2.111 +bind_thm ("eclose_closed", eclose_L (thm "M_eclose.eclose_closed"));
   2.112 +bind_thm ("eclose_abs", eclose_L (thm "M_eclose.eclose_abs"));
   2.113 +*}
   2.114 +
   2.115 +declare eclose_closed [intro,simp]
   2.116 +declare eclose_abs [intro,simp]
   2.117 +
   2.118 +
   2.119 +
   2.120  
   2.121  end