Finished absoluteness of "satisfies"!!
authorpaulson
Wed, 14 Aug 2002 14:33:26 +0200
changeset 13502 da43ebc02f17
parent 13501 79242cccaddc
child 13503 d93f41fe35d2
Finished absoluteness of "satisfies"!!
src/ZF/Constructible/Satisfies_absolute.thy
--- a/src/ZF/Constructible/Satisfies_absolute.thy	Tue Aug 13 22:01:53 2002 +0200
+++ b/src/ZF/Constructible/Satisfies_absolute.thy	Wed Aug 14 14:33:26 2002 +0200
@@ -403,11 +403,9 @@
                               h ` succ(depth(v)) ` v),
                 \<lambda>u. d(u, h ` succ(depth(u)) ` u))"
 
-  is_formula_rec :: "[i=>o, [i,i,i]=>o, 
-                      [i,i]=>i, [i,i]=>i, [i,i,i,i]=>i, [i,i]=>i, 
-                      i, i] => o"
+  is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o"
     --{* predicate to relative the functional @{term formula_rec}*}
-   "is_formula_rec(M,MH,a,b,c,d,p,z)  ==
+   "is_formula_rec(M,MH,p,z)  ==
     \<exists>i[M]. \<exists>f[M]. i = succ(depth(p)) & fun_apply(M,f,p,z) &
                   is_transrec(M,MH,i,f)"
 
@@ -445,8 +443,9 @@
   fixes a and is_a and b and is_b and c and is_c and d and is_d and MH
   defines
       "MH(u::i,f,z) ==
-	is_lambda
-	 (M, formula, is_formula_case (M, is_a, is_b, is_c(f), is_d(f)), z)"
+	\<forall>fml[M]. is_formula(M,fml) -->
+             is_lambda
+	 (M, fml, is_formula_case (M, is_a, is_b, is_c(f), is_d(f)), z)"
 
   assumes a_closed: "[|x\<in>nat; y\<in>nat|] ==> M(a(x,y))"
       and a_rel:    "Relativize2(M, nat, nat, is_a, a)"
@@ -502,7 +501,7 @@
 
 theorem (in M_formula_rec) formula_rec_abs:
   "[| p \<in> formula; M(z)|] 
-   ==> is_formula_rec(M,MH,a,b,c,d,p,z) <-> z = formula_rec(a,b,c,d,p)" 
+   ==> is_formula_rec(M,MH,p,z) <-> z = formula_rec(a,b,c,d,p)" 
 by (simp add: is_formula_rec_def formula_rec_eq2 transM [OF _ formula_closed]
               transrec_abs [OF fr_replace MH_rel2] 
               fr_transrec_closed formula_rec_lam_closed eq_commute)
@@ -559,7 +558,7 @@
                 zz)"
  
   satisfies_c :: "[i,i,i,i,i]=>i"
-   "satisfies_c(A,p,q,rp,rq) == \<lambda>env \<in> list(A). not(rp ` env and rq ` env)"
+   "satisfies_c(A) == \<lambda>p q rp rq. \<lambda>env \<in> list(A). not(rp ` env and rq ` env)"
 
   satisfies_is_c :: "[i=>o,i,i,i,i,i]=>o"
    "satisfies_is_c(M,A,h) == 
@@ -590,19 +589,40 @@
     --{*The variable @{term u} is unused, but gives @{term satisfies_MH} 
         the correct arity.*}
    "satisfies_MH == 
-    \<lambda>M A u f zz. 
+    \<lambda>M A u f z. 
          \<forall>fml[M]. is_formula(M,fml) -->
              is_lambda (M, fml, 
                is_formula_case (M, satisfies_is_a(M,A), 
                                 satisfies_is_b(M,A), 
                                 satisfies_is_c(M,A,f), satisfies_is_d(M,A,f)),
-               zz)"
+               z)"
 
+  is_satisfies :: "[i=>o,i,i,i]=>o"
+   "is_satisfies(M,A) == 
+      is_formula_rec (M, \<lambda>u f z.
+        \<forall>fml[M].
+           is_formula(M,fml) \<longrightarrow>
+           is_lambda
+            (M, fml,
+             is_formula_case
+              (M, satisfies_is_a(M,A), satisfies_is_b(M,A),
+               satisfies_is_c(M,A,f), satisfies_is_d(M,A,f)), z))"
+
+
+text{*This lemma relates the fragments defined above to the original primitive
+      recursion in @{term satisfies}.
+      Induction is not required: the definitions are directly equal!*}
+lemma satisfies_eq:
+  "satisfies(A,p) = 
+   formula_rec (satisfies_a(A), satisfies_b(A), 
+                satisfies_c(A), satisfies_d(A), p)"
+by (simp add: satisfies_formula_def satisfies_a_def satisfies_b_def 
+              satisfies_c_def satisfies_d_def) 
 
 text{*Further constraints on the class @{term M} in order to prove
       absoluteness for the constants defined above.  The ultimate goal
       is the absoluteness of the function @{term satisfies}. *}
-locale M_satisfies = M_datatypes +
+locale M_satisfies = M_eclose +
  assumes 
    Member_replacement:
     "[|M(A); x \<in> nat; y \<in> nat|]
@@ -643,17 +663,17 @@
   formula_rec_replacement: 
       --{*For the @{term transrec}*}
    "[|n \<in> nat; M(A)|] ==> transrec_replacement(M, satisfies_MH(M,A), n)"
-(*NEEDS RELATIVIZATION?*)
  and
   formula_rec_lambda_replacement:  
       --{*For the @{text "\<lambda>-abstraction"} in the @{term transrec} body*}
-   "M(g) ==>
-    strong_replacement (M, \<lambda>x y. x \<in> formula &
-            y = \<langle>x, 
-                 formula_rec_case(satisfies_a(A),
-                                  satisfies_b(A),
-                                  satisfies_c(A),
-                                  satisfies_d(A), g, x)\<rangle>)"
+   "[|M(g); M(A)|] ==>
+    strong_replacement (M, 
+       \<lambda>x y. mem_formula(M,x) &
+             (\<exists>c[M]. is_formula_case(M, satisfies_is_a(M,A),
+                                  satisfies_is_b(M,A),
+                                  satisfies_is_c(M,A,g),
+                                  satisfies_is_d(M,A,g), x, c) &
+             pair(M, x, c, y)))"
 
 
 lemma (in M_satisfies) Member_replacement':
@@ -751,198 +771,76 @@
       "[|n \<in> nat; M(A)|] ==> transrec_replacement(M,satisfies_MH(M,A),n)" 
 by (blast intro: formula_rec_replacement) 
 
+lemma (in M_satisfies) formula_case_satisfies_closed:
+ "[|M(g); M(A); x \<in> formula|] ==>
+  M(formula_case (satisfies_a(A), satisfies_b(A),
+       \<lambda>u v. satisfies_c(A, u, v, 
+                         g ` succ(depth(u)) ` u, g ` succ(depth(v)) ` v),
+       \<lambda>u. satisfies_d (A, u, g ` succ(depth(u)) ` u),
+       x))"
+by (blast intro: formula_case_closed a_closed b_closed c_closed d_closed) 
+
 lemma (in M_satisfies) fr_lam_replace:
-   "M(g) ==>
+   "[|M(g); M(A)|] ==>
     strong_replacement (M, \<lambda>x y. x \<in> formula &
             y = \<langle>x, 
                  formula_rec_case(satisfies_a(A),
                                   satisfies_b(A),
                                   satisfies_c(A),
                                   satisfies_d(A), g, x)\<rangle>)"
-by (blast intro: formula_rec_lambda_replacement)
+apply (insert formula_rec_lambda_replacement) 
+apply (simp add: formula_rec_case_def formula_case_satisfies_closed
+                 formula_case_abs [OF a_rel b_rel c_rel d_rel]) 
+done
 
 
 
-subsection{*Instantiating the Locale @{text "M_satisfies"}*}
-
-
-subsubsection{*The @{term "Member"} Case*}
-
-lemma Member_Reflects:
- "REFLECTS[\<lambda>u. \<exists>v[L]. v \<in> B \<and> (\<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L].
-          v \<in> lstA \<and> is_nth(L,x,v,nx) \<and> is_nth(L,y,v,ny) \<and>
-          is_bool_of_o(L, nx \<in> ny, bo) \<and> pair(L,v,bo,u)),
-   \<lambda>i u. \<exists>v \<in> Lset(i). v \<in> B \<and> (\<exists>bo \<in> Lset(i). \<exists>nx \<in> Lset(i). \<exists>ny \<in> Lset(i).
-             v \<in> lstA \<and> is_nth(**Lset(i), x, v, nx) \<and> 
-             is_nth(**Lset(i), y, v, ny) \<and>
-          is_bool_of_o(**Lset(i), nx \<in> ny, bo) \<and> pair(**Lset(i), v, bo, u))]"
-by (intro FOL_reflections function_reflections nth_reflection 
-          bool_of_o_reflection)
-
+text{*Instantiate locale @{text M_formula_rec} for the 
+      Function @{term satisfies}*}
 
-lemma Member_replacement:
-    "[|L(A); x \<in> nat; y \<in> nat|]
-     ==> strong_replacement
-	 (L, \<lambda>env z. \<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L]. 
-              env \<in> list(A) & is_nth(L,x,env,nx) & is_nth(L,y,env,ny) & 
-              is_bool_of_o(L, nx \<in> ny, bo) &
-              pair(L, env, bo, z))"
-apply (frule list_closed) 
-apply (rule strong_replacementI) 
-apply (rule rallI)
-apply (rename_tac B)  
-apply (rule separation_CollectI) 
-apply (rule_tac A="{list(A),B,x,y,z}" in subset_LsetE, blast ) 
-apply (rule ReflectsE [OF Member_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption) 
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2)
-apply (simp add: is_nth_def is_wfrec_def is_bool_of_o_def)
-apply (rule DPow_LsetI)
-apply (rename_tac u) 
-apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[v,u,list(A),B,x,y,z]" in mem_iff_sats) 
-apply (rule sep_rules is_nat_case_iff_sats iterates_MH_iff_sats
-            is_recfun_iff_sats hd_iff_sats tl_iff_sats quasinat_iff_sats
-     | simp)+
+lemma (in M_satisfies) M_formula_rec_axioms_M:
+   "M(A) ==>
+    M_formula_rec_axioms(M, satisfies_a(A), satisfies_is_a(M,A), 
+                            satisfies_b(A), satisfies_is_b(M,A), 
+                            satisfies_c(A), satisfies_is_c(M,A), 
+                            satisfies_d(A), satisfies_is_d(M,A))"
+apply (rule M_formula_rec_axioms.intro)
+apply (assumption | 
+       rule a_closed a_rel b_closed b_rel c_closed c_rel d_closed d_rel
+       fr_replace [unfolded satisfies_MH_def]
+       fr_lam_replace) +
 done
 
 
-subsubsection{*The @{term "Equal"} Case*}
-
-lemma Equal_Reflects:
- "REFLECTS[\<lambda>u. \<exists>v[L]. v \<in> B \<and> (\<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L].
-          v \<in> lstA \<and> is_nth(L, x, v, nx) \<and> is_nth(L, y, v, ny) \<and>
-          is_bool_of_o(L, nx = ny, bo) \<and> pair(L, v, bo, u)),
-   \<lambda>i u. \<exists>v \<in> Lset(i). v \<in> B \<and> (\<exists>bo \<in> Lset(i). \<exists>nx \<in> Lset(i). \<exists>ny \<in> Lset(i).
-             v \<in> lstA \<and> is_nth(**Lset(i), x, v, nx) \<and> 
-             is_nth(**Lset(i), y, v, ny) \<and>
-          is_bool_of_o(**Lset(i), nx = ny, bo) \<and> pair(**Lset(i), v, bo, u))]"
-by (intro FOL_reflections function_reflections nth_reflection 
-          bool_of_o_reflection)
-
-
-lemma Equal_replacement:
-    "[|L(A); x \<in> nat; y \<in> nat|]
-     ==> strong_replacement
-	 (L, \<lambda>env z. \<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L]. 
-              env \<in> list(A) & is_nth(L,x,env,nx) & is_nth(L,y,env,ny) & 
-              is_bool_of_o(L, nx = ny, bo) &
-              pair(L, env, bo, z))"
-apply (frule list_closed) 
-apply (rule strong_replacementI) 
-apply (rule rallI)
-apply (rename_tac B)  
-apply (rule separation_CollectI) 
-apply (rule_tac A="{list(A),B,x,y,z}" in subset_LsetE, blast ) 
-apply (rule ReflectsE [OF Equal_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption) 
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2)
-apply (simp add: is_nth_def is_wfrec_def is_bool_of_o_def)
-apply (rule DPow_LsetI)
-apply (rename_tac u) 
-apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[v,u,list(A),B,x,y,z]" in mem_iff_sats) 
-apply (rule sep_rules is_nat_case_iff_sats iterates_MH_iff_sats
-            is_recfun_iff_sats hd_iff_sats tl_iff_sats quasinat_iff_sats
-     | simp)+
-done
-
-subsubsection{*The @{term "Nand"} Case*}
-
-lemma Nand_Reflects:
-    "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B \<and>
-	       (\<exists>rpe[L]. \<exists>rqe[L]. \<exists>andpq[L]. \<exists>notpq[L].
-		 fun_apply(L, rp, u, rpe) \<and> fun_apply(L, rq, u, rqe) \<and>
-		 is_and(L, rpe, rqe, andpq) \<and> is_not(L, andpq, notpq) \<and>
-		 u \<in> list(A) \<and> pair(L, u, notpq, x)),
-    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and>
-     (\<exists>rpe \<in> Lset(i). \<exists>rqe \<in> Lset(i). \<exists>andpq \<in> Lset(i). \<exists>notpq \<in> Lset(i).
-       fun_apply(**Lset(i), rp, u, rpe) \<and> fun_apply(**Lset(i), rq, u, rqe) \<and>
-       is_and(**Lset(i), rpe, rqe, andpq) \<and> is_not(**Lset(i), andpq, notpq) \<and>
-       u \<in> list(A) \<and> pair(**Lset(i), u, notpq, x))]"
-apply (unfold is_and_def is_not_def) 
-apply (intro FOL_reflections function_reflections)
+theorem (in M_satisfies) M_formula_rec_M: 
+    "M(A) ==>
+     PROP M_formula_rec(M, satisfies_a(A), satisfies_is_a(M,A), 
+                            satisfies_b(A), satisfies_is_b(M,A), 
+                            satisfies_c(A), satisfies_is_c(M,A), 
+                            satisfies_d(A), satisfies_is_d(M,A))"
+apply (rule M_formula_rec.intro, assumption+)
+apply (erule M_formula_rec_axioms_M) 
 done
 
-lemma Nand_replacement:
-    "[|L(A); L(rp); L(rq)|]
-     ==> strong_replacement
-	 (L, \<lambda>env z. \<exists>rpe[L]. \<exists>rqe[L]. \<exists>andpq[L]. \<exists>notpq[L]. 
-               fun_apply(L,rp,env,rpe) & fun_apply(L,rq,env,rqe) & 
-               is_and(L,rpe,rqe,andpq) & is_not(L,andpq,notpq) & 
-               env \<in> list(A) & pair(L, env, notpq, z))"
-apply (frule list_closed) 
-apply (rule strong_replacementI) 
-apply (rule rallI)
-apply (rename_tac B)  
-apply (rule separation_CollectI) 
-apply (rule_tac A="{list(A),B,rp,rq,z}" in subset_LsetE, blast ) 
-apply (rule ReflectsE [OF Nand_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption) 
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2)
-apply (simp add: is_and_def is_not_def)
-apply (rule DPow_LsetI)
-apply (rename_tac v) 
-apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[u,v,list(A),B,rp,rq,z]" in mem_iff_sats) 
-apply (rule sep_rules | simp)+
-done
+lemmas (in M_satisfies) 
+   satisfies_closed = M_formula_rec.formula_rec_closed [OF M_formula_rec_M]
+and
+   satisfies_abs = M_formula_rec.formula_rec_abs [OF M_formula_rec_M];
 
 
-subsubsection{*The @{term "Forall"} Case*}
-
-lemma Forall_Reflects:
- "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>bo[L]. u \<in> list(A) \<and>
-                 is_bool_of_o (L,
-     \<forall>a[L]. \<forall>co[L]. \<forall>rpco[L]. a \<in> A \<longrightarrow>
-                is_Cons(L,a,u,co) \<longrightarrow> fun_apply(L,rp,co,rpco) \<longrightarrow> 
-                number1(L,rpco),
-                           bo) \<and> pair(L,u,bo,x)),
- \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>bo \<in> Lset(i). u \<in> list(A) \<and>
-        is_bool_of_o (**Lset(i),
- \<forall>a \<in> Lset(i). \<forall>co \<in> Lset(i). \<forall>rpco \<in> Lset(i). a \<in> A \<longrightarrow>
-	    is_Cons(**Lset(i),a,u,co) \<longrightarrow> fun_apply(**Lset(i),rp,co,rpco) \<longrightarrow> 
-	    number1(**Lset(i),rpco),
-		       bo) \<and> pair(**Lset(i),u,bo,x))]"
-apply (unfold is_bool_of_o_def) 
-apply (intro FOL_reflections function_reflections Cons_reflection)
-done
+lemma (in M_satisfies) satisfies_closed:
+  "[|M(A); p \<in> formula|] ==> M(satisfies(A,p))"
+by (simp add: M_formula_rec.formula_rec_closed [OF M_formula_rec_M]  
+              satisfies_eq) 
 
-lemma Forall_replacement:
-   "[|L(A); L(rp)|]
-    ==> strong_replacement
-	(L, \<lambda>env z. \<exists>bo[L]. 
-	      env \<in> list(A) & 
-	      is_bool_of_o (L, 
-			    \<forall>a[L]. \<forall>co[L]. \<forall>rpco[L]. 
-			       a\<in>A --> is_Cons(L,a,env,co) -->
-			       fun_apply(L,rp,co,rpco) --> number1(L, rpco), 
-                            bo) &
-	      pair(L,env,bo,z))"
-apply (frule list_closed) 
-apply (rule strong_replacementI) 
-apply (rule rallI)
-apply (rename_tac B)  
-apply (rule separation_CollectI) 
-apply (rule_tac A="{A,list(A),B,rp,z}" in subset_LsetE, blast ) 
-apply (rule ReflectsE [OF Forall_Reflects], assumption)
-apply (drule subset_Lset_ltD, assumption) 
-apply (erule reflection_imp_L_separation)
-  apply (simp_all add: lt_Ord2)
-apply (simp add: is_bool_of_o_def)
-apply (rule DPow_LsetI)
-apply (rename_tac v) 
-apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[u,v,A,list(A),B,rp,z]" in mem_iff_sats)
-apply (rule sep_rules Cons_iff_sats | simp)+
-done
-
-subsubsection{*The @{term "transrec_replacement"} Case*}
+lemma (in M_satisfies) satisfies_abs:
+  "[|M(A); M(z); p \<in> formula|] 
+   ==> is_satisfies(M,A,p,z) <-> z = satisfies(A,p)"
+by (simp only: M_formula_rec.formula_rec_abs [OF M_formula_rec_M]  
+               satisfies_eq is_satisfies_def)
 
 
+subsection{*Internalizations Needed to Instantiate @{text "M_satisfies"}*}
 
 subsubsection{*The Operator @{term is_depth_apply}, Internalized*}
 
@@ -1246,6 +1144,185 @@
 done
 
 
+subsection{*Lemmas for Instantiating the Locale @{text "M_satisfies"}*}
+
+
+subsubsection{*The @{term "Member"} Case*}
+
+lemma Member_Reflects:
+ "REFLECTS[\<lambda>u. \<exists>v[L]. v \<in> B \<and> (\<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L].
+          v \<in> lstA \<and> is_nth(L,x,v,nx) \<and> is_nth(L,y,v,ny) \<and>
+          is_bool_of_o(L, nx \<in> ny, bo) \<and> pair(L,v,bo,u)),
+   \<lambda>i u. \<exists>v \<in> Lset(i). v \<in> B \<and> (\<exists>bo \<in> Lset(i). \<exists>nx \<in> Lset(i). \<exists>ny \<in> Lset(i).
+             v \<in> lstA \<and> is_nth(**Lset(i), x, v, nx) \<and> 
+             is_nth(**Lset(i), y, v, ny) \<and>
+          is_bool_of_o(**Lset(i), nx \<in> ny, bo) \<and> pair(**Lset(i), v, bo, u))]"
+by (intro FOL_reflections function_reflections nth_reflection 
+          bool_of_o_reflection)
+
+
+lemma Member_replacement:
+    "[|L(A); x \<in> nat; y \<in> nat|]
+     ==> strong_replacement
+	 (L, \<lambda>env z. \<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L]. 
+              env \<in> list(A) & is_nth(L,x,env,nx) & is_nth(L,y,env,ny) & 
+              is_bool_of_o(L, nx \<in> ny, bo) &
+              pair(L, env, bo, z))"
+apply (frule list_closed) 
+apply (rule strong_replacementI) 
+apply (rule rallI)
+apply (rename_tac B)  
+apply (rule separation_CollectI) 
+apply (rule_tac A="{list(A),B,x,y,z}" in subset_LsetE, blast ) 
+apply (rule ReflectsE [OF Member_Reflects], assumption)
+apply (drule subset_Lset_ltD, assumption) 
+apply (erule reflection_imp_L_separation)
+  apply (simp_all add: lt_Ord2)
+apply (simp add: is_nth_def is_wfrec_def is_bool_of_o_def)
+apply (rule DPow_LsetI)
+apply (rename_tac u) 
+apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+
+apply (rule_tac env = "[v,u,list(A),B,x,y,z]" in mem_iff_sats) 
+apply (rule sep_rules is_nat_case_iff_sats iterates_MH_iff_sats
+            is_recfun_iff_sats hd_iff_sats tl_iff_sats quasinat_iff_sats
+     | simp)+
+done
+
+
+subsubsection{*The @{term "Equal"} Case*}
+
+lemma Equal_Reflects:
+ "REFLECTS[\<lambda>u. \<exists>v[L]. v \<in> B \<and> (\<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L].
+          v \<in> lstA \<and> is_nth(L, x, v, nx) \<and> is_nth(L, y, v, ny) \<and>
+          is_bool_of_o(L, nx = ny, bo) \<and> pair(L, v, bo, u)),
+   \<lambda>i u. \<exists>v \<in> Lset(i). v \<in> B \<and> (\<exists>bo \<in> Lset(i). \<exists>nx \<in> Lset(i). \<exists>ny \<in> Lset(i).
+             v \<in> lstA \<and> is_nth(**Lset(i), x, v, nx) \<and> 
+             is_nth(**Lset(i), y, v, ny) \<and>
+          is_bool_of_o(**Lset(i), nx = ny, bo) \<and> pair(**Lset(i), v, bo, u))]"
+by (intro FOL_reflections function_reflections nth_reflection 
+          bool_of_o_reflection)
+
+
+lemma Equal_replacement:
+    "[|L(A); x \<in> nat; y \<in> nat|]
+     ==> strong_replacement
+	 (L, \<lambda>env z. \<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L]. 
+              env \<in> list(A) & is_nth(L,x,env,nx) & is_nth(L,y,env,ny) & 
+              is_bool_of_o(L, nx = ny, bo) &
+              pair(L, env, bo, z))"
+apply (frule list_closed) 
+apply (rule strong_replacementI) 
+apply (rule rallI)
+apply (rename_tac B)  
+apply (rule separation_CollectI) 
+apply (rule_tac A="{list(A),B,x,y,z}" in subset_LsetE, blast ) 
+apply (rule ReflectsE [OF Equal_Reflects], assumption)
+apply (drule subset_Lset_ltD, assumption) 
+apply (erule reflection_imp_L_separation)
+  apply (simp_all add: lt_Ord2)
+apply (simp add: is_nth_def is_wfrec_def is_bool_of_o_def)
+apply (rule DPow_LsetI)
+apply (rename_tac u) 
+apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+
+apply (rule_tac env = "[v,u,list(A),B,x,y,z]" in mem_iff_sats) 
+apply (rule sep_rules is_nat_case_iff_sats iterates_MH_iff_sats
+            is_recfun_iff_sats hd_iff_sats tl_iff_sats quasinat_iff_sats
+     | simp)+
+done
+
+subsubsection{*The @{term "Nand"} Case*}
+
+lemma Nand_Reflects:
+    "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B \<and>
+	       (\<exists>rpe[L]. \<exists>rqe[L]. \<exists>andpq[L]. \<exists>notpq[L].
+		 fun_apply(L, rp, u, rpe) \<and> fun_apply(L, rq, u, rqe) \<and>
+		 is_and(L, rpe, rqe, andpq) \<and> is_not(L, andpq, notpq) \<and>
+		 u \<in> list(A) \<and> pair(L, u, notpq, x)),
+    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and>
+     (\<exists>rpe \<in> Lset(i). \<exists>rqe \<in> Lset(i). \<exists>andpq \<in> Lset(i). \<exists>notpq \<in> Lset(i).
+       fun_apply(**Lset(i), rp, u, rpe) \<and> fun_apply(**Lset(i), rq, u, rqe) \<and>
+       is_and(**Lset(i), rpe, rqe, andpq) \<and> is_not(**Lset(i), andpq, notpq) \<and>
+       u \<in> list(A) \<and> pair(**Lset(i), u, notpq, x))]"
+apply (unfold is_and_def is_not_def) 
+apply (intro FOL_reflections function_reflections)
+done
+
+lemma Nand_replacement:
+    "[|L(A); L(rp); L(rq)|]
+     ==> strong_replacement
+	 (L, \<lambda>env z. \<exists>rpe[L]. \<exists>rqe[L]. \<exists>andpq[L]. \<exists>notpq[L]. 
+               fun_apply(L,rp,env,rpe) & fun_apply(L,rq,env,rqe) & 
+               is_and(L,rpe,rqe,andpq) & is_not(L,andpq,notpq) & 
+               env \<in> list(A) & pair(L, env, notpq, z))"
+apply (frule list_closed) 
+apply (rule strong_replacementI) 
+apply (rule rallI)
+apply (rename_tac B)  
+apply (rule separation_CollectI) 
+apply (rule_tac A="{list(A),B,rp,rq,z}" in subset_LsetE, blast ) 
+apply (rule ReflectsE [OF Nand_Reflects], assumption)
+apply (drule subset_Lset_ltD, assumption) 
+apply (erule reflection_imp_L_separation)
+  apply (simp_all add: lt_Ord2)
+apply (simp add: is_and_def is_not_def)
+apply (rule DPow_LsetI)
+apply (rename_tac v) 
+apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+
+apply (rule_tac env = "[u,v,list(A),B,rp,rq,z]" in mem_iff_sats) 
+apply (rule sep_rules | simp)+
+done
+
+
+subsubsection{*The @{term "Forall"} Case*}
+
+lemma Forall_Reflects:
+ "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>bo[L]. u \<in> list(A) \<and>
+                 is_bool_of_o (L,
+     \<forall>a[L]. \<forall>co[L]. \<forall>rpco[L]. a \<in> A \<longrightarrow>
+                is_Cons(L,a,u,co) \<longrightarrow> fun_apply(L,rp,co,rpco) \<longrightarrow> 
+                number1(L,rpco),
+                           bo) \<and> pair(L,u,bo,x)),
+ \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>bo \<in> Lset(i). u \<in> list(A) \<and>
+        is_bool_of_o (**Lset(i),
+ \<forall>a \<in> Lset(i). \<forall>co \<in> Lset(i). \<forall>rpco \<in> Lset(i). a \<in> A \<longrightarrow>
+	    is_Cons(**Lset(i),a,u,co) \<longrightarrow> fun_apply(**Lset(i),rp,co,rpco) \<longrightarrow> 
+	    number1(**Lset(i),rpco),
+		       bo) \<and> pair(**Lset(i),u,bo,x))]"
+apply (unfold is_bool_of_o_def) 
+apply (intro FOL_reflections function_reflections Cons_reflection)
+done
+
+lemma Forall_replacement:
+   "[|L(A); L(rp)|]
+    ==> strong_replacement
+	(L, \<lambda>env z. \<exists>bo[L]. 
+	      env \<in> list(A) & 
+	      is_bool_of_o (L, 
+			    \<forall>a[L]. \<forall>co[L]. \<forall>rpco[L]. 
+			       a\<in>A --> is_Cons(L,a,env,co) -->
+			       fun_apply(L,rp,co,rpco) --> number1(L, rpco), 
+                            bo) &
+	      pair(L,env,bo,z))"
+apply (frule list_closed) 
+apply (rule strong_replacementI) 
+apply (rule rallI)
+apply (rename_tac B)  
+apply (rule separation_CollectI) 
+apply (rule_tac A="{A,list(A),B,rp,z}" in subset_LsetE, blast ) 
+apply (rule ReflectsE [OF Forall_Reflects], assumption)
+apply (drule subset_Lset_ltD, assumption) 
+apply (erule reflection_imp_L_separation)
+  apply (simp_all add: lt_Ord2)
+apply (simp add: is_bool_of_o_def)
+apply (rule DPow_LsetI)
+apply (rename_tac v) 
+apply (rule bex_iff_sats conj_iff_sats conj_iff_sats)+
+apply (rule_tac env = "[u,v,A,list(A),B,rp,z]" in mem_iff_sats)
+apply (rule sep_rules Cons_iff_sats | simp)+
+done
+
+subsubsection{*The @{term "transrec_replacement"} Case*}
+
 lemma formula_rec_replacement_Reflects:
  "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L, u, y, x) \<and>
              is_wfrec (L, satisfies_MH(L,A), mesa, u, y)),
@@ -1275,8 +1352,78 @@
 apply (rename_tac v)
 apply (rule bex_iff_sats conj_iff_sats)+
 apply (rule_tac env = "[u,v,A,n,B,Memrel(eclose({n}))]" in mem_iff_sats)
-apply (rule sep_rules | simp)+
 apply (rule sep_rules satisfies_MH_iff_sats is_wfrec_iff_sats | simp)+
 done
 
+
+subsubsection{*The Lambda Replacement Case*}
+
+lemma formula_rec_lambda_replacement_Reflects:
+ "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B &
+     mem_formula(L,u) &
+     (\<exists>c[L].
+	 is_formula_case
+	  (L, satisfies_is_a(L,A), satisfies_is_b(L,A),
+	   satisfies_is_c(L,A,g), satisfies_is_d(L,A,g),
+	   u, c) &
+	 pair(L,u,c,x)),
+  \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & mem_formula(**Lset(i),u) &
+     (\<exists>c \<in> Lset(i).
+	 is_formula_case
+	  (**Lset(i), satisfies_is_a(**Lset(i),A), satisfies_is_b(**Lset(i),A),
+	   satisfies_is_c(**Lset(i),A,g), satisfies_is_d(**Lset(i),A,g),
+	   u, c) &
+	 pair(**Lset(i),u,c,x))]"
+by (intro FOL_reflections function_reflections mem_formula_reflection
+          is_formula_case_reflection satisfies_is_a_reflection
+          satisfies_is_b_reflection satisfies_is_c_reflection
+          satisfies_is_d_reflection)  
+
+lemma formula_rec_lambda_replacement: 
+      --{*For the @{term transrec}*}
+   "[|L(g); L(A)|] ==>
+    strong_replacement (L, 
+       \<lambda>x y. mem_formula(L,x) &
+             (\<exists>c[L]. is_formula_case(L, satisfies_is_a(L,A),
+                                  satisfies_is_b(L,A),
+                                  satisfies_is_c(L,A,g),
+                                  satisfies_is_d(L,A,g), x, c) &
+             pair(L, x, c, y)))" 
+apply (rule strong_replacementI)
+apply (rule rallI)
+apply (rename_tac B)
+apply (rule separation_CollectI)
+apply (rule_tac A="{B,A,g,z}" in subset_LsetE, blast)
+apply (rule ReflectsE [OF formula_rec_lambda_replacement_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,g,B]" in mem_iff_sats)
+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
+          satisfies_is_d_iff_sats | simp)+
+done
+
+
+subsection{*Instantiating @{text M_satisfies}*}
+
+lemma M_satisfies_axioms_L: "M_satisfies_axioms(L)"
+  apply (rule M_satisfies_axioms.intro)
+       apply (assumption | rule
+	 Member_replacement Equal_replacement 
+         Nand_replacement Forall_replacement
+         formula_rec_replacement formula_rec_lambda_replacement)+
+  done
+
+theorem M_satisfies_L: "PROP M_satisfies(L)"
+apply (rule M_satisfies.intro) 
+     apply (rule M_eclose.axioms [OF M_eclose_L])+
+apply (rule M_satisfies_axioms_L) 
+done
+
 end