absoluteness for "formula" and "eclose"

--- a/src/ZF/Constructible/Datatype_absolute.thy	Thu Jul 18 12:10:24 2002 +0200
+++ b/src/ZF/Constructible/Datatype_absolute.thy	Thu Jul 18 15:21:42 2002 +0200
@@ -268,6 +268,39 @@
 
 
 subsection{*@{term M} Contains the List and Formula Datatypes*}
+
+constdefs
+  is_list_n :: "[i=>o,i,i,i] => o"
+    "is_list_n(M,A,n,Z) == 
+      \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M]. 
+       empty(M,zero) & 
+       successor(M,n,sn) & membership(M,sn,msn) &
+       is_wfrec(M, iterates_MH(M, is_list_functor(M,A),zero), msn, n, Z)"
+  
+  mem_list :: "[i=>o,i,i] => o"
+    "mem_list(M,A,l) == 
+      \<exists>n[M]. \<exists>listn[M]. 
+       finite_ordinal(M,n) & is_list_n(M,A,n,listn) & l \<in> listn"
+
+  is_list :: "[i=>o,i,i] => o"
+    "is_list(M,A,Z) == \<forall>l[M]. l \<in> Z <-> mem_list(M,A,l)"
+
+constdefs
+  is_formula_n :: "[i=>o,i,i] => o"
+    "is_formula_n(M,n,Z) == 
+      \<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M]. 
+       empty(M,zero) & 
+       successor(M,n,sn) & membership(M,sn,msn) &
+       is_wfrec(M, iterates_MH(M, is_formula_functor(M),zero), msn, n, Z)"
+  
+  mem_formula :: "[i=>o,i] => o"
+    "mem_formula(M,p) == 
+      \<exists>n[M]. \<exists>formn[M]. 
+       finite_ordinal(M,n) & is_formula_n(M,n,formn) & p \<in> formn"
+
+  is_formula :: "[i=>o,i] => o"
+    "is_formula(M,Z) == \<forall>p[M]. p \<in> Z <-> mem_formula(M,p)"
+
 locale (open) M_datatypes = M_wfrank +
  assumes list_replacement1: 
    "M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)"
@@ -286,6 +319,9 @@
                is_wfrec(M, iterates_MH(M,is_formula_functor(M), 0), 
                         msn, n, y)))"
 
+
+subsubsection{*Absoluteness of the List Construction*}
+
 lemma (in M_datatypes) list_replacement2': 
   "M(A) ==> strong_replacement(M, \<lambda>n y. n\<in>nat & y = (\<lambda>X. {0} + A * X)^n (0))"
 apply (insert list_replacement2 [of A]) 
@@ -300,7 +336,28 @@
 by  (simp add: RepFun_closed2 list_eq_Union 
                list_replacement2' relativize1_def
                iterates_closed [of "is_list_functor(M,A)"])
+lemma (in M_datatypes) is_list_n_abs [simp]:
+     "[|M(A); n\<in>nat; M(Z)|] 
+      ==> is_list_n(M,A,n,Z) <-> Z = (\<lambda>X. {0} + A * X)^n (0)"
+apply (insert list_replacement1)
+apply (simp add: is_list_n_def relativize1_def nat_into_M
+                 iterates_abs [of "is_list_functor(M,A)" _ "\<lambda>X. {0} + A*X"])
+done
 
+lemma (in M_datatypes) mem_list_abs [simp]:
+     "M(A) ==> mem_list(M,A,l) <-> l \<in> list(A)"
+apply (insert list_replacement1)
+apply (simp add: mem_list_def relativize1_def list_eq_Union
+                 iterates_closed [of "is_list_functor(M,A)"]) 
+done
+
+lemma (in M_datatypes) list_abs [simp]:
+     "[|M(A); M(Z)|] ==> is_list(M,A,Z) <-> Z = list(A)"
+apply (simp add: is_list_def, safe)
+apply (rule M_equalityI, simp_all)
+done
+
+subsubsection{*Absoluteness of Formulas*}
 
 lemma (in M_datatypes) formula_replacement2': 
   "strong_replacement(M, \<lambda>n y. n\<in>nat & y = (\<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))^n (0))"
@@ -318,4 +375,151 @@
                   iterates_closed [of "is_formula_functor(M)"])
 done
 
+lemma (in M_datatypes) is_formula_n_abs [simp]:
+     "[|n\<in>nat; M(Z)|] 
+      ==> is_formula_n(M,n,Z) <-> 
+          Z = (\<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))^n (0)"
+apply (insert formula_replacement1)
+apply (simp add: is_formula_n_def relativize1_def nat_into_M
+                 iterates_abs [of "is_formula_functor(M)" _ 
+                        "\<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X))"])
+done
+
+lemma (in M_datatypes) mem_formula_abs [simp]:
+     "mem_formula(M,l) <-> l \<in> formula"
+apply (insert formula_replacement1)
+apply (simp add: mem_formula_def relativize1_def formula_eq_Union
+                 iterates_closed [of "is_formula_functor(M)"]) 
+done
+
+lemma (in M_datatypes) formula_abs [simp]:
+     "[|M(Z)|] ==> is_formula(M,Z) <-> Z = formula"
+apply (simp add: is_formula_def, safe)
+apply (rule M_equalityI, simp_all)
+done
+
+
+subsection{*Absoluteness for @{text \<epsilon>}-Closure: the @{term eclose} Operator*}
+
+text{*Re-expresses eclose using "iterates"*}
+lemma eclose_eq_Union:
+     "eclose(A) = (\<Union>n\<in>nat. Union^n (A))"
+apply (simp add: eclose_def) 
+apply (rule UN_cong) 
+apply (rule refl)
+apply (induct_tac n)
+apply (simp add: nat_rec_0)  
+apply (simp add: nat_rec_succ) 
+done
+
+constdefs
+  is_eclose_n :: "[i=>o,i,i,i] => o"
+    "is_eclose_n(M,A,n,Z) == 
+      \<exists>sn[M]. \<exists>msn[M]. 
+       successor(M,n,sn) & membership(M,sn,msn) &
+       is_wfrec(M, iterates_MH(M, big_union(M), A), msn, n, Z)"
+  
+  mem_eclose :: "[i=>o,i,i] => o"
+    "mem_eclose(M,A,l) == 
+      \<exists>n[M]. \<exists>eclosen[M]. 
+       finite_ordinal(M,n) & is_eclose_n(M,A,n,eclosen) & l \<in> eclosen"
+
+  is_eclose :: "[i=>o,i,i] => o"
+    "is_eclose(M,A,Z) == \<forall>u[M]. u \<in> Z <-> mem_eclose(M,A,u)"
+
+
+locale (open) M_eclose = M_wfrank +
+ assumes eclose_replacement1: 
+   "M(A) ==> iterates_replacement(M, big_union(M), A)"
+  and eclose_replacement2: 
+   "M(A) ==> strong_replacement(M, 
+         \<lambda>n y. n\<in>nat & 
+               (\<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
+               is_wfrec(M, iterates_MH(M,big_union(M), A), 
+                        msn, n, y)))"
+
+lemma (in M_eclose) eclose_replacement2': 
+  "M(A) ==> strong_replacement(M, \<lambda>n y. n\<in>nat & y = Union^n (A))"
+apply (insert eclose_replacement2 [of A]) 
+apply (rule strong_replacement_cong [THEN iffD1])  
+apply (rule conj_cong [OF iff_refl iterates_abs [of "big_union(M)"]]) 
+apply (simp_all add: eclose_replacement1 relativize1_def) 
+done
+
+lemma (in M_eclose) eclose_closed [intro,simp]:
+     "M(A) ==> M(eclose(A))"
+apply (insert eclose_replacement1)
+by  (simp add: RepFun_closed2 eclose_eq_Union 
+               eclose_replacement2' relativize1_def
+               iterates_closed [of "big_union(M)"])
+
+lemma (in M_eclose) is_eclose_n_abs [simp]:
+     "[|M(A); n\<in>nat; M(Z)|] ==> is_eclose_n(M,A,n,Z) <-> Z = Union^n (A)"
+apply (insert eclose_replacement1)
+apply (simp add: is_eclose_n_def relativize1_def nat_into_M
+                 iterates_abs [of "big_union(M)" _ "Union"])
+done
+
+lemma (in M_eclose) mem_eclose_abs [simp]:
+     "M(A) ==> mem_eclose(M,A,l) <-> l \<in> eclose(A)"
+apply (insert eclose_replacement1)
+apply (simp add: mem_eclose_def relativize1_def eclose_eq_Union
+                 iterates_closed [of "big_union(M)"]) 
+done
+
+lemma (in M_eclose) eclose_abs [simp]:
+     "[|M(A); M(Z)|] ==> is_eclose(M,A,Z) <-> Z = eclose(A)"
+apply (simp add: is_eclose_def, safe)
+apply (rule M_equalityI, simp_all)
+done
+
+
+
+
+subsection {*Absoluteness for @{term transrec}*}
+
+
+text{* @{term "transrec(a,H) \<equiv> wfrec(Memrel(eclose({a})), a, H)"} *}
+constdefs
+
+  is_transrec :: "[i=>o, [i,i,i]=>o, i, i] => o"
+   "is_transrec(M,MH,a,z) == 
+      \<exists>sa[M]. \<exists>esa[M]. \<exists>mesa[M]. 
+       upair(M,a,a,sa) & is_eclose(M,sa,esa) & membership(M,esa,mesa) &
+       is_wfrec(M,MH,mesa,a,z)"
+
+  transrec_replacement :: "[i=>o, [i,i,i]=>o, i] => o"
+   "transrec_replacement(M,MH,a) ==
+      \<exists>sa[M]. \<exists>esa[M]. \<exists>mesa[M]. 
+       upair(M,a,a,sa) & is_eclose(M,sa,esa) & membership(M,esa,mesa) &
+       wfrec_replacement(M,MH,mesa)"
+
+(*????????????????Ordinal.thy*)
+lemma Transset_trans_Memrel: 
+    "\<forall>j\<in>i. Transset(j) ==> trans(Memrel(i))"
+by (unfold Transset_def trans_def, blast)
+
+text{*The condition @{term "Ord(i)"} lets us use the simpler 
+  @{text "trans_wfrec_abs"} rather than @{text "trans_wfrec_abs"},
+  which I haven't even proved yet. *}
+theorem (in M_eclose) transrec_abs:
+  "[|Ord(i);  M(i);  M(z);
+     transrec_replacement(M,MH,i);  relativize2(M,MH,H);
+     \<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
+   ==> is_transrec(M,MH,i,z) <-> z = transrec(i,H)" 
+by (simp add: trans_wfrec_abs transrec_replacement_def is_transrec_def
+       transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
+
+
+theorem (in M_eclose) transrec_closed:
+     "[|Ord(i);  M(i);  M(z);
+	transrec_replacement(M,MH,i);  relativize2(M,MH,H);
+	\<forall>x[M]. \<forall>g[M]. function(g) --> M(H(x,g))|] 
+      ==> M(transrec(i,H))"
+by (simp add: trans_wfrec_closed transrec_replacement_def is_transrec_def
+       transrec_def eclose_sing_Ord_eq wf_Memrel trans_Memrel relation_Memrel)
+
+
+
+
 end

--- a/src/ZF/Constructible/Rec_Separation.thy	Thu Jul 18 12:10:24 2002 +0200
+++ b/src/ZF/Constructible/Rec_Separation.thy	Thu Jul 18 15:21:42 2002 +0200
@@ -1013,9 +1013,118 @@
 
 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
+   [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
+         is_wfrec(L, iterates_MH(L, big_union(L), A), memsn, u, y)),
+    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(**Lset(i), u, y, x) \<and>
+         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
+   [\<lambda>x. \<exists>u[L]. u \<in> B \<and> u \<in> nat \<and>
+         (\<exists>sn[L]. \<exists>msn[L]. successor(L, u, sn) \<and> membership(L, sn, msn) \<and>
+           is_wfrec (L, iterates_MH (L, big_union(L), A),
+                              msn, u, x)),
+    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> u \<in> nat \<and>
+         (\<exists>sn \<in> Lset(i). \<exists>msn \<in> Lset(i). 
+          successor(**Lset(i), u, sn) \<and> membership(**Lset(i), sn, msn) \<and>
+           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, 
+         \<lambda>n y. n\<in>nat & 
+               (\<exists>sn[L]. \<exists>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 (wfrank_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