# HG changeset patch
# User paulson
# Date 1026916892 -7200
# Node ID f3e9e8b21aba2095d869e7631b40f5d46bacc126
# Parent  31df66ca0780ff40c66d19a6823db51e30820869
Formulas (and lists) in M (and L!)

diff -r 31df66ca0780 -r f3e9e8b21aba src/ZF/Constructible/Datatype_absolute.thy
--- a/src/ZF/Constructible/Datatype_absolute.thy	Wed Jul 17 15:48:54 2002 +0200
+++ b/src/ZF/Constructible/Datatype_absolute.thy	Wed Jul 17 16:41:32 2002 +0200
@@ -106,45 +106,6 @@
 
 
 
-subsection {*lists without univ*}
-
-lemmas datatype_univs = Inl_in_univ Inr_in_univ 
-                        Pair_in_univ nat_into_univ A_into_univ 
-
-lemma list_fun_bnd_mono: "bnd_mono(univ(A), \<lambda>X. {0} + A*X)"
-apply (rule bnd_monoI)
- apply (intro subset_refl zero_subset_univ A_subset_univ 
-	      sum_subset_univ Sigma_subset_univ) 
-apply (rule subset_refl sum_mono Sigma_mono | assumption)+
-done
-
-lemma list_fun_contin: "contin(\<lambda>X. {0} + A*X)"
-by (intro sum_contin prod_contin id_contin const_contin) 
-
-text{*Re-expresses lists using sum and product*}
-lemma list_eq_lfp2: "list(A) = lfp(univ(A), \<lambda>X. {0} + A*X)"
-apply (simp add: list_def) 
-apply (rule equalityI) 
- apply (rule lfp_lowerbound) 
-  prefer 2 apply (rule lfp_subset)
- apply (clarify, subst lfp_unfold [OF list_fun_bnd_mono])
- apply (simp add: Nil_def Cons_def)
- apply blast 
-txt{*Opposite inclusion*}
-apply (rule lfp_lowerbound) 
- prefer 2 apply (rule lfp_subset) 
-apply (clarify, subst lfp_unfold [OF list.bnd_mono]) 
-apply (simp add: Nil_def Cons_def)
-apply (blast intro: datatype_univs
-             dest: lfp_subset [THEN subsetD])
-done
-
-text{*Re-expresses lists using "iterates", no univ.*}
-lemma list_eq_Union:
-     "list(A) = (\<Union>n\<in>nat. (\<lambda>X. {0} + A*X) ^ n (0))"
-by (simp add: list_eq_lfp2 lfp_eq_Union list_fun_bnd_mono list_fun_contin)
-
-
 subsection {*Absoluteness for "Iterates"*}
 
 constdefs
@@ -198,6 +159,45 @@
 done
 
 
+subsection {*lists without univ*}
+
+lemmas datatype_univs = Inl_in_univ Inr_in_univ 
+                        Pair_in_univ nat_into_univ A_into_univ 
+
+lemma list_fun_bnd_mono: "bnd_mono(univ(A), \<lambda>X. {0} + A*X)"
+apply (rule bnd_monoI)
+ apply (intro subset_refl zero_subset_univ A_subset_univ 
+	      sum_subset_univ Sigma_subset_univ) 
+apply (rule subset_refl sum_mono Sigma_mono | assumption)+
+done
+
+lemma list_fun_contin: "contin(\<lambda>X. {0} + A*X)"
+by (intro sum_contin prod_contin id_contin const_contin) 
+
+text{*Re-expresses lists using sum and product*}
+lemma list_eq_lfp2: "list(A) = lfp(univ(A), \<lambda>X. {0} + A*X)"
+apply (simp add: list_def) 
+apply (rule equalityI) 
+ apply (rule lfp_lowerbound) 
+  prefer 2 apply (rule lfp_subset)
+ apply (clarify, subst lfp_unfold [OF list_fun_bnd_mono])
+ apply (simp add: Nil_def Cons_def)
+ apply blast 
+txt{*Opposite inclusion*}
+apply (rule lfp_lowerbound) 
+ prefer 2 apply (rule lfp_subset) 
+apply (clarify, subst lfp_unfold [OF list.bnd_mono]) 
+apply (simp add: Nil_def Cons_def)
+apply (blast intro: datatype_univs
+             dest: lfp_subset [THEN subsetD])
+done
+
+text{*Re-expresses lists using "iterates", no univ.*}
+lemma list_eq_Union:
+     "list(A) = (\<Union>n\<in>nat. (\<lambda>X. {0} + A*X) ^ n (0))"
+by (simp add: list_eq_lfp2 lfp_eq_Union list_fun_bnd_mono list_fun_contin)
+
+
 constdefs
   is_list_functor :: "[i=>o,i,i,i] => o"
     "is_list_functor(M,A,X,Z) == 
@@ -209,6 +209,65 @@
 by (simp add: is_list_functor_def singleton_0 nat_into_M)
 
 
+subsection {*formulas without univ*}
+
+lemma formula_fun_bnd_mono:
+     "bnd_mono(univ(0), \<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))"
+apply (rule bnd_monoI)
+ apply (intro subset_refl zero_subset_univ A_subset_univ 
+	      sum_subset_univ Sigma_subset_univ nat_subset_univ) 
+apply (rule subset_refl sum_mono Sigma_mono | assumption)+
+done
+
+lemma formula_fun_contin:
+     "contin(\<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))"
+by (intro sum_contin prod_contin id_contin const_contin) 
+
+
+text{*Re-expresses formulas using sum and product*}
+lemma formula_eq_lfp2:
+    "formula = lfp(univ(0), \<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X)))"
+apply (simp add: formula_def) 
+apply (rule equalityI) 
+ apply (rule lfp_lowerbound) 
+  prefer 2 apply (rule lfp_subset)
+ apply (clarify, subst lfp_unfold [OF formula_fun_bnd_mono])
+ apply (simp add: Member_def Equal_def Neg_def And_def Forall_def)
+ apply blast 
+txt{*Opposite inclusion*}
+apply (rule lfp_lowerbound) 
+ prefer 2 apply (rule lfp_subset, clarify) 
+apply (subst lfp_unfold [OF formula.bnd_mono, simplified]) 
+apply (simp add: Member_def Equal_def Neg_def And_def Forall_def)  
+apply (elim sumE SigmaE, simp_all) 
+apply (blast intro: datatype_univs dest: lfp_subset [THEN subsetD])+  
+done
+
+text{*Re-expresses formulas using "iterates", no univ.*}
+lemma formula_eq_Union:
+     "formula = 
+      (\<Union>n\<in>nat. (\<lambda>X. ((nat*nat) + (nat*nat)) + (X + (X*X + X))) ^ n (0))"
+by (simp add: formula_eq_lfp2 lfp_eq_Union formula_fun_bnd_mono 
+              formula_fun_contin)
+
+
+constdefs
+  is_formula_functor :: "[i=>o,i,i] => o"
+    "is_formula_functor(M,X,Z) == 
+        \<exists>nat'[M]. \<exists>natnat[M]. \<exists>natnatsum[M]. \<exists>XX[M]. \<exists>X3[M]. \<exists>X4[M]. 
+          omega(M,nat') & cartprod(M,nat',nat',natnat) & 
+          is_sum(M,natnat,natnat,natnatsum) &
+          cartprod(M,X,X,XX) & is_sum(M,XX,X,X3) & is_sum(M,X,X3,X4) &
+          is_sum(M,natnatsum,X4,Z)"
+
+lemma (in M_axioms) formula_functor_abs [simp]: 
+     "[| M(X); M(Z) |] 
+      ==> is_formula_functor(M,X,Z) <-> 
+          Z = ((nat*nat) + (nat*nat)) + (X + (X*X + X))"
+by (simp add: is_formula_functor_def) 
+
+
+subsection{*@{term M} Contains the List and Formula Datatypes*}
 locale (open) M_datatypes = M_wfrank +
  assumes list_replacement1: 
    "M(A) ==> iterates_replacement(M, is_list_functor(M,A), 0)"
@@ -218,6 +277,14 @@
                (\<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
                is_wfrec(M, iterates_MH(M,is_list_functor(M,A), 0), 
                         msn, n, y)))"
+  and formula_replacement1: 
+   "iterates_replacement(M, is_formula_functor(M), 0)"
+  and formula_replacement2: 
+   "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,is_formula_functor(M), 0), 
+                        msn, n, y)))"
 
 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))"
@@ -235,4 +302,20 @@
                iterates_closed [of "is_list_functor(M,A)"])
 
 
+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))"
+apply (insert formula_replacement2) 
+apply (rule strong_replacement_cong [THEN iffD1])  
+apply (rule conj_cong [OF iff_refl iterates_abs [of "is_formula_functor(M)"]]) 
+apply (simp_all add: formula_replacement1 relativize1_def) 
+done
+
+lemma (in M_datatypes) formula_closed [intro,simp]:
+     "M(formula)"
+apply (insert formula_replacement1)
+apply  (simp add: RepFun_closed2 formula_eq_Union 
+                  formula_replacement2' relativize1_def
+                  iterates_closed [of "is_formula_functor(M)"])
+done
+
 end
diff -r 31df66ca0780 -r f3e9e8b21aba src/ZF/Constructible/Rec_Separation.thy
--- a/src/ZF/Constructible/Rec_Separation.thy	Wed Jul 17 15:48:54 2002 +0200
+++ b/src/ZF/Constructible/Rec_Separation.thy	Wed Jul 17 16:41:32 2002 +0200
@@ -562,46 +562,6 @@
 done
 
 
-subsubsection{*The List Functor, Internalized*}
-
-constdefs list_functor_fm :: "[i,i,i]=>i"
-(* "is_list_functor(M,A,X,Z) == 
-        \<exists>n1[M]. \<exists>AX[M]. 
-         number1(M,n1) & cartprod(M,A,X,AX) & is_sum(M,n1,AX,Z)" *)
-    "list_functor_fm(A,X,Z) == 
-       Exists(Exists(
-	And(number1_fm(1),
-            And(cartprod_fm(A#+2,X#+2,0), sum_fm(1,0,Z#+2)))))"
-
-lemma list_functor_type [TC]:
-     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> list_functor_fm(x,y,z) \<in> formula"
-by (simp add: list_functor_fm_def) 
-
-lemma arity_list_functor_fm [simp]:
-     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
-      ==> arity(list_functor_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
-by (simp add: list_functor_fm_def succ_Un_distrib [symmetric] Un_ac) 
-
-lemma sats_list_functor_fm [simp]:
-   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
-    ==> sats(A, list_functor_fm(x,y,z), env) <-> 
-        is_list_functor(**A, nth(x,env), nth(y,env), nth(z,env))"
-by (simp add: list_functor_fm_def is_list_functor_def)
-
-lemma list_functor_iff_sats:
-  "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
-      i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
-   ==> is_list_functor(**A, x, y, z) <-> sats(A, list_functor_fm(i,j,k), env)"
-by simp
-
-theorem list_functor_reflection:
-     "REFLECTS[\<lambda>x. is_list_functor(L,f(x),g(x),h(x)), 
-               \<lambda>i x. is_list_functor(**Lset(i),f(x),g(x),h(x))]"
-apply (simp only: is_list_functor_def setclass_simps)
-apply (intro FOL_reflections number1_reflection
-             cartprod_reflection sum_reflection)  
-done
-
 subsubsection{*The Operator @{term quasinat}*}
 
 (* "is_quasinat(M,z) == empty(M,z) | (\<exists>m[M]. successor(M,m,z))" *)
@@ -785,6 +745,49 @@
 
 subsection{*@{term L} is Closed Under the Operator @{term list}*} 
 
+subsubsection{*The List Functor, Internalized*}
+
+constdefs list_functor_fm :: "[i,i,i]=>i"
+(* "is_list_functor(M,A,X,Z) == 
+        \<exists>n1[M]. \<exists>AX[M]. 
+         number1(M,n1) & cartprod(M,A,X,AX) & is_sum(M,n1,AX,Z)" *)
+    "list_functor_fm(A,X,Z) == 
+       Exists(Exists(
+	And(number1_fm(1),
+            And(cartprod_fm(A#+2,X#+2,0), sum_fm(1,0,Z#+2)))))"
+
+lemma list_functor_type [TC]:
+     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> list_functor_fm(x,y,z) \<in> formula"
+by (simp add: list_functor_fm_def) 
+
+lemma arity_list_functor_fm [simp]:
+     "[| x \<in> nat; y \<in> nat; z \<in> nat |] 
+      ==> arity(list_functor_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
+by (simp add: list_functor_fm_def succ_Un_distrib [symmetric] Un_ac) 
+
+lemma sats_list_functor_fm [simp]:
+   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
+    ==> sats(A, list_functor_fm(x,y,z), env) <-> 
+        is_list_functor(**A, nth(x,env), nth(y,env), nth(z,env))"
+by (simp add: list_functor_fm_def is_list_functor_def)
+
+lemma list_functor_iff_sats:
+  "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
+      i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
+   ==> is_list_functor(**A, x, y, z) <-> sats(A, list_functor_fm(i,j,k), env)"
+by simp
+
+theorem list_functor_reflection:
+     "REFLECTS[\<lambda>x. is_list_functor(L,f(x),g(x),h(x)), 
+               \<lambda>i x. is_list_functor(**Lset(i),f(x),g(x),h(x))]"
+apply (simp only: is_list_functor_def setclass_simps)
+apply (intro FOL_reflections number1_reflection
+             cartprod_reflection sum_reflection)  
+done
+
+
+subsubsection{*Instances of Replacement for Lists*}
+
 lemma list_replacement1_Reflects:
  "REFLECTS
    [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
@@ -809,7 +812,8 @@
 apply (rule ReflectsE [OF list_replacement1_Reflects], assumption)
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2)
+  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)+
@@ -818,7 +822,6 @@
 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 list_functor_iff_sats quasinat_iff_sats | simp)+
-apply (simp_all add: succ_Un_distrib [symmetric] Memrel_closed)
 done
 
 
@@ -864,4 +867,133 @@
 apply (rule sep_rules list_functor_iff_sats quasinat_iff_sats | simp)+
 done
 
+
+subsection{*@{term L} is Closed Under the Operator @{term formula}*} 
+
+subsubsection{*The Formula Functor, Internalized*}
+
+constdefs formula_functor_fm :: "[i,i]=>i"
+(*     "is_formula_functor(M,X,Z) == 
+        \<exists>nat'[M]. \<exists>natnat[M]. \<exists>natnatsum[M]. \<exists>XX[M]. \<exists>X3[M]. \<exists>X4[M]. 
+          5          4              3          2       1       0
+          omega(M,nat') & cartprod(M,nat',nat',natnat) & 
+          is_sum(M,natnat,natnat,natnatsum) &
+          cartprod(M,X,X,XX) & is_sum(M,XX,X,X3) & is_sum(M,X,X3,X4) &
+          is_sum(M,natnatsum,X4,Z)" *) 
+    "formula_functor_fm(X,Z) == 
+       Exists(Exists(Exists(Exists(Exists(Exists(
+	And(omega_fm(5),
+         And(cartprod_fm(5,5,4),
+          And(sum_fm(4,4,3),
+           And(cartprod_fm(X#+6,X#+6,2),
+            And(sum_fm(2,X#+6,1),
+             And(sum_fm(X#+6,1,0), sum_fm(3,0,Z#+6)))))))))))))"
+
+lemma formula_functor_type [TC]:
+     "[| x \<in> nat; y \<in> nat |] ==> formula_functor_fm(x,y) \<in> formula"
+by (simp add: formula_functor_fm_def) 
+
+lemma sats_formula_functor_fm [simp]:
+   "[| x \<in> nat; y \<in> nat; env \<in> list(A)|]
+    ==> sats(A, formula_functor_fm(x,y), env) <-> 
+        is_formula_functor(**A, nth(x,env), nth(y,env))"
+by (simp add: formula_functor_fm_def is_formula_functor_def)
+
+lemma formula_functor_iff_sats:
+  "[| nth(i,env) = x; nth(j,env) = y; 
+      i \<in> nat; j \<in> nat; env \<in> list(A)|]
+   ==> is_formula_functor(**A, x, y) <-> sats(A, formula_functor_fm(i,j), env)"
+by simp
+
+theorem formula_functor_reflection:
+     "REFLECTS[\<lambda>x. is_formula_functor(L,f(x),g(x)), 
+               \<lambda>i x. is_formula_functor(**Lset(i),f(x),g(x))]"
+apply (simp only: is_formula_functor_def setclass_simps)
+apply (intro FOL_reflections omega_reflection
+             cartprod_reflection sum_reflection)  
+done
+
+subsubsection{*Instances of Replacement for Formulas*}
+
+lemma formula_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, is_formula_functor(L), 0), 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), 
+                          is_formula_functor(**Lset(i)), 0), memsn, u, y))]"
+by (intro FOL_reflections function_reflections is_wfrec_reflection 
+          iterates_MH_reflection formula_functor_reflection) 
+
+lemma formula_replacement1: 
+   "iterates_replacement(L, is_formula_functor(L), 0)"
+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 (insert nonempty) 
+apply (subgoal_tac "L(Memrel(succ(n)))") 
+apply (rule_tac A="{B,n,z,0,Memrel(succ(n))}" in subset_LsetE, blast ) 
+apply (rule ReflectsE [OF formula_replacement1_Reflects], assumption)
+apply (drule subset_Lset_ltD, assumption) 
+apply (erule reflection_imp_L_separation)
+  apply (simp_all add: lt_Ord2 Memrel_closed)
+apply (rule DPow_LsetI)
+apply (rename_tac v) 
+apply (rule bex_iff_sats conj_iff_sats)+
+apply (rule_tac env = "[u,v,n,B,0,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 formula_functor_iff_sats quasinat_iff_sats | simp)+
+txt{*SLOW: like 40 seconds!*}
+done
+
+lemma formula_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, is_formula_functor(L), 0),
+                              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), is_formula_functor(**Lset(i)), 0),
+                     msn, u, x))]"
+by (intro FOL_reflections function_reflections is_wfrec_reflection 
+          iterates_MH_reflection formula_functor_reflection) 
+
+
+lemma formula_replacement2: 
+   "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,is_formula_functor(L), 0), 
+                        msn, n, y)))"
+apply (rule strong_replacementI) 
+apply (rule rallI)
+apply (rename_tac B)   
+apply (rule separation_CollectI) 
+apply (insert nonempty) 
+apply (rule_tac A="{B,z,0,nat}" in subset_LsetE) 
+apply (blast intro: L_nat) 
+apply (rule ReflectsE [OF formula_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,B,0,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 formula_functor_iff_sats quasinat_iff_sats | simp)+
+done
+
+text{*NB The proofs for type @{term formula} are virtually identical to those
+for @{term "list(A)"}.  It was a cut-and-paste job! *}
+
 end