src/ZF/Constructible/Satisfies_absolute.thy
author ballarin
Thu Dec 11 18:30:26 2008 +0100 (2008-12-11)
changeset 29223 e09c53289830
parent 23464 bc2563c37b1a
child 32960 69916a850301
permissions -rw-r--r--
Conversion of HOL-Main and ZF to new locales.
     1 (*  Title:      ZF/Constructible/Satisfies_absolute.thy
     2     ID:  $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4 *)
     5 
     6 header {*Absoluteness for the Satisfies Relation on Formulas*}
     7 
     8 theory Satisfies_absolute imports Datatype_absolute Rec_Separation begin 
     9 
    10 
    11 subsection {*More Internalization*}
    12 
    13 subsubsection{*The Formula @{term is_depth}, Internalized*}
    14 
    15 (*    "is_depth(M,p,n) == 
    16        \<exists>sn[M]. \<exists>formula_n[M]. \<exists>formula_sn[M]. 
    17          2          1                0
    18         is_formula_N(M,n,formula_n) & p \<notin> formula_n &
    19         successor(M,n,sn) & is_formula_N(M,sn,formula_sn) & p \<in> formula_sn" *)
    20 definition
    21   depth_fm :: "[i,i]=>i" where
    22   "depth_fm(p,n) == 
    23      Exists(Exists(Exists(
    24        And(formula_N_fm(n#+3,1),
    25          And(Neg(Member(p#+3,1)),
    26           And(succ_fm(n#+3,2),
    27            And(formula_N_fm(2,0), Member(p#+3,0))))))))"
    28 
    29 lemma depth_fm_type [TC]:
    30  "[| x \<in> nat; y \<in> nat |] ==> depth_fm(x,y) \<in> formula"
    31 by (simp add: depth_fm_def)
    32 
    33 lemma sats_depth_fm [simp]:
    34    "[| x \<in> nat; y < length(env); env \<in> list(A)|]
    35     ==> sats(A, depth_fm(x,y), env) <->
    36         is_depth(##A, nth(x,env), nth(y,env))"
    37 apply (frule_tac x=y in lt_length_in_nat, assumption)  
    38 apply (simp add: depth_fm_def is_depth_def) 
    39 done
    40 
    41 lemma depth_iff_sats:
    42       "[| nth(i,env) = x; nth(j,env) = y; 
    43           i \<in> nat; j < length(env); env \<in> list(A)|]
    44        ==> is_depth(##A, x, y) <-> sats(A, depth_fm(i,j), env)"
    45 by (simp add: sats_depth_fm)
    46 
    47 theorem depth_reflection:
    48      "REFLECTS[\<lambda>x. is_depth(L, f(x), g(x)),  
    49                \<lambda>i x. is_depth(##Lset(i), f(x), g(x))]"
    50 apply (simp only: is_depth_def)
    51 apply (intro FOL_reflections function_reflections formula_N_reflection) 
    52 done
    53 
    54 
    55 
    56 subsubsection{*The Operator @{term is_formula_case}*}
    57 
    58 text{*The arguments of @{term is_a} are always 2, 1, 0, and the formula
    59       will be enclosed by three quantifiers.*}
    60 
    61 (* is_formula_case :: 
    62     "[i=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i]=>o, i, i] => o"
    63   "is_formula_case(M, is_a, is_b, is_c, is_d, v, z) == 
    64       (\<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> is_Member(M,x,y,v) --> is_a(x,y,z)) &
    65       (\<forall>x[M]. \<forall>y[M]. x\<in>nat --> y\<in>nat --> is_Equal(M,x,y,v) --> is_b(x,y,z)) &
    66       (\<forall>x[M]. \<forall>y[M]. x\<in>formula --> y\<in>formula --> 
    67                      is_Nand(M,x,y,v) --> is_c(x,y,z)) &
    68       (\<forall>x[M]. x\<in>formula --> is_Forall(M,x,v) --> is_d(x,z))" *)
    69 
    70 definition
    71   formula_case_fm :: "[i, i, i, i, i, i]=>i" where
    72   "formula_case_fm(is_a, is_b, is_c, is_d, v, z) == 
    73         And(Forall(Forall(Implies(finite_ordinal_fm(1), 
    74                            Implies(finite_ordinal_fm(0), 
    75                             Implies(Member_fm(1,0,v#+2), 
    76                              Forall(Implies(Equal(0,z#+3), is_a))))))),
    77         And(Forall(Forall(Implies(finite_ordinal_fm(1), 
    78                            Implies(finite_ordinal_fm(0), 
    79                             Implies(Equal_fm(1,0,v#+2), 
    80                              Forall(Implies(Equal(0,z#+3), is_b))))))),
    81         And(Forall(Forall(Implies(mem_formula_fm(1), 
    82                            Implies(mem_formula_fm(0), 
    83                             Implies(Nand_fm(1,0,v#+2), 
    84                              Forall(Implies(Equal(0,z#+3), is_c))))))),
    85         Forall(Implies(mem_formula_fm(0), 
    86                        Implies(Forall_fm(0,succ(v)), 
    87                              Forall(Implies(Equal(0,z#+2), is_d))))))))"
    88 
    89 
    90 lemma is_formula_case_type [TC]:
    91      "[| is_a \<in> formula;  is_b \<in> formula;  is_c \<in> formula;  is_d \<in> formula;  
    92          x \<in> nat; y \<in> nat |] 
    93       ==> formula_case_fm(is_a, is_b, is_c, is_d, x, y) \<in> formula"
    94 by (simp add: formula_case_fm_def)
    95 
    96 lemma sats_formula_case_fm:
    97   assumes is_a_iff_sats: 
    98       "!!a0 a1 a2. 
    99         [|a0\<in>A; a1\<in>A; a2\<in>A|]  
   100         ==> ISA(a2, a1, a0) <-> sats(A, is_a, Cons(a0,Cons(a1,Cons(a2,env))))"
   101   and is_b_iff_sats: 
   102       "!!a0 a1 a2. 
   103         [|a0\<in>A; a1\<in>A; a2\<in>A|]  
   104         ==> ISB(a2, a1, a0) <-> sats(A, is_b, Cons(a0,Cons(a1,Cons(a2,env))))"
   105   and is_c_iff_sats: 
   106       "!!a0 a1 a2. 
   107         [|a0\<in>A; a1\<in>A; a2\<in>A|]  
   108         ==> ISC(a2, a1, a0) <-> sats(A, is_c, Cons(a0,Cons(a1,Cons(a2,env))))"
   109   and is_d_iff_sats: 
   110       "!!a0 a1. 
   111         [|a0\<in>A; a1\<in>A|]  
   112         ==> ISD(a1, a0) <-> sats(A, is_d, Cons(a0,Cons(a1,env)))"
   113   shows 
   114       "[|x \<in> nat; y < length(env); env \<in> list(A)|]
   115        ==> sats(A, formula_case_fm(is_a,is_b,is_c,is_d,x,y), env) <->
   116            is_formula_case(##A, ISA, ISB, ISC, ISD, nth(x,env), nth(y,env))"
   117 apply (frule_tac x=y in lt_length_in_nat, assumption)  
   118 apply (simp add: formula_case_fm_def is_formula_case_def 
   119                  is_a_iff_sats [THEN iff_sym] is_b_iff_sats [THEN iff_sym]
   120                  is_c_iff_sats [THEN iff_sym] is_d_iff_sats [THEN iff_sym])
   121 done
   122 
   123 lemma formula_case_iff_sats:
   124   assumes is_a_iff_sats: 
   125       "!!a0 a1 a2. 
   126         [|a0\<in>A; a1\<in>A; a2\<in>A|]  
   127         ==> ISA(a2, a1, a0) <-> sats(A, is_a, Cons(a0,Cons(a1,Cons(a2,env))))"
   128   and is_b_iff_sats: 
   129       "!!a0 a1 a2. 
   130         [|a0\<in>A; a1\<in>A; a2\<in>A|]  
   131         ==> ISB(a2, a1, a0) <-> sats(A, is_b, Cons(a0,Cons(a1,Cons(a2,env))))"
   132   and is_c_iff_sats: 
   133       "!!a0 a1 a2. 
   134         [|a0\<in>A; a1\<in>A; a2\<in>A|]  
   135         ==> ISC(a2, a1, a0) <-> sats(A, is_c, Cons(a0,Cons(a1,Cons(a2,env))))"
   136   and is_d_iff_sats: 
   137       "!!a0 a1. 
   138         [|a0\<in>A; a1\<in>A|]  
   139         ==> ISD(a1, a0) <-> sats(A, is_d, Cons(a0,Cons(a1,env)))"
   140   shows 
   141       "[|nth(i,env) = x; nth(j,env) = y; 
   142       i \<in> nat; j < length(env); env \<in> list(A)|]
   143        ==> is_formula_case(##A, ISA, ISB, ISC, ISD, x, y) <->
   144            sats(A, formula_case_fm(is_a,is_b,is_c,is_d,i,j), env)"
   145 by (simp add: sats_formula_case_fm [OF is_a_iff_sats is_b_iff_sats 
   146                                        is_c_iff_sats is_d_iff_sats])
   147 
   148 
   149 text{*The second argument of @{term is_a} gives it direct access to @{term x},
   150   which is essential for handling free variable references.  Treatment is
   151   based on that of @{text is_nat_case_reflection}.*}
   152 theorem is_formula_case_reflection:
   153   assumes is_a_reflection:
   154     "!!h f g g'. REFLECTS[\<lambda>x. is_a(L, h(x), f(x), g(x), g'(x)),
   155                      \<lambda>i x. is_a(##Lset(i), h(x), f(x), g(x), g'(x))]"
   156   and is_b_reflection:
   157     "!!h f g g'. REFLECTS[\<lambda>x. is_b(L, h(x), f(x), g(x), g'(x)),
   158                      \<lambda>i x. is_b(##Lset(i), h(x), f(x), g(x), g'(x))]"
   159   and is_c_reflection:
   160     "!!h f g g'. REFLECTS[\<lambda>x. is_c(L, h(x), f(x), g(x), g'(x)),
   161                      \<lambda>i x. is_c(##Lset(i), h(x), f(x), g(x), g'(x))]"
   162   and is_d_reflection:
   163     "!!h f g g'. REFLECTS[\<lambda>x. is_d(L, h(x), f(x), g(x)),
   164                      \<lambda>i x. is_d(##Lset(i), h(x), f(x), g(x))]"
   165   shows "REFLECTS[\<lambda>x. is_formula_case(L, is_a(L,x), is_b(L,x), is_c(L,x), is_d(L,x), g(x), h(x)),
   166                \<lambda>i x. is_formula_case(##Lset(i), is_a(##Lset(i), x), is_b(##Lset(i), x), is_c(##Lset(i), x), is_d(##Lset(i), x), g(x), h(x))]"
   167 apply (simp (no_asm_use) only: is_formula_case_def)
   168 apply (intro FOL_reflections function_reflections finite_ordinal_reflection
   169          mem_formula_reflection
   170          Member_reflection Equal_reflection Nand_reflection Forall_reflection
   171          is_a_reflection is_b_reflection is_c_reflection is_d_reflection)
   172 done
   173 
   174 
   175 
   176 subsection {*Absoluteness for the Function @{term satisfies}*}
   177 
   178 definition
   179   is_depth_apply :: "[i=>o,i,i,i] => o" where
   180    --{*Merely a useful abbreviation for the sequel.*}
   181   "is_depth_apply(M,h,p,z) ==
   182     \<exists>dp[M]. \<exists>sdp[M]. \<exists>hsdp[M]. 
   183 	finite_ordinal(M,dp) & is_depth(M,p,dp) & successor(M,dp,sdp) &
   184 	fun_apply(M,h,sdp,hsdp) & fun_apply(M,hsdp,p,z)"
   185 
   186 lemma (in M_datatypes) is_depth_apply_abs [simp]:
   187      "[|M(h); p \<in> formula; M(z)|] 
   188       ==> is_depth_apply(M,h,p,z) <-> z = h ` succ(depth(p)) ` p"
   189 by (simp add: is_depth_apply_def formula_into_M depth_type eq_commute)
   190 
   191 
   192 
   193 text{*There is at present some redundancy between the relativizations in
   194  e.g. @{text satisfies_is_a} and those in e.g. @{text Member_replacement}.*}
   195 
   196 text{*These constants let us instantiate the parameters @{term a}, @{term b},
   197       @{term c}, @{term d}, etc., of the locale @{text Formula_Rec}.*}
   198 definition
   199   satisfies_a :: "[i,i,i]=>i" where
   200    "satisfies_a(A) == 
   201     \<lambda>x y. \<lambda>env \<in> list(A). bool_of_o (nth(x,env) \<in> nth(y,env))"
   202 
   203 definition
   204   satisfies_is_a :: "[i=>o,i,i,i,i]=>o" where
   205    "satisfies_is_a(M,A) == 
   206     \<lambda>x y zz. \<forall>lA[M]. is_list(M,A,lA) -->
   207              is_lambda(M, lA, 
   208 		\<lambda>env z. is_bool_of_o(M, 
   209                       \<exists>nx[M]. \<exists>ny[M]. 
   210  		       is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & nx \<in> ny, z),
   211                 zz)"
   212 
   213 definition
   214   satisfies_b :: "[i,i,i]=>i" where
   215    "satisfies_b(A) ==
   216     \<lambda>x y. \<lambda>env \<in> list(A). bool_of_o (nth(x,env) = nth(y,env))"
   217 
   218 definition
   219   satisfies_is_b :: "[i=>o,i,i,i,i]=>o" where
   220    --{*We simplify the formula to have just @{term nx} rather than 
   221        introducing @{term ny} with  @{term "nx=ny"} *}
   222   "satisfies_is_b(M,A) == 
   223     \<lambda>x y zz. \<forall>lA[M]. is_list(M,A,lA) -->
   224              is_lambda(M, lA, 
   225                 \<lambda>env z. is_bool_of_o(M, 
   226                       \<exists>nx[M]. is_nth(M,x,env,nx) & is_nth(M,y,env,nx), z),
   227                 zz)"
   228 
   229 definition 
   230   satisfies_c :: "[i,i,i,i,i]=>i" where
   231    "satisfies_c(A) == \<lambda>p q rp rq. \<lambda>env \<in> list(A). not(rp ` env and rq ` env)"
   232 
   233 definition
   234   satisfies_is_c :: "[i=>o,i,i,i,i,i]=>o" where
   235    "satisfies_is_c(M,A,h) == 
   236     \<lambda>p q zz. \<forall>lA[M]. is_list(M,A,lA) -->
   237              is_lambda(M, lA, \<lambda>env z. \<exists>hp[M]. \<exists>hq[M]. 
   238 		 (\<exists>rp[M]. is_depth_apply(M,h,p,rp) & fun_apply(M,rp,env,hp)) & 
   239 		 (\<exists>rq[M]. is_depth_apply(M,h,q,rq) & fun_apply(M,rq,env,hq)) & 
   240                  (\<exists>pq[M]. is_and(M,hp,hq,pq) & is_not(M,pq,z)),
   241                 zz)"
   242 
   243 definition
   244   satisfies_d :: "[i,i,i]=>i" where
   245    "satisfies_d(A) 
   246     == \<lambda>p rp. \<lambda>env \<in> list(A). bool_of_o (\<forall>x\<in>A. rp ` (Cons(x,env)) = 1)"
   247 
   248 definition
   249   satisfies_is_d :: "[i=>o,i,i,i,i]=>o" where
   250    "satisfies_is_d(M,A,h) == 
   251     \<lambda>p zz. \<forall>lA[M]. is_list(M,A,lA) -->
   252              is_lambda(M, lA, 
   253                 \<lambda>env z. \<exists>rp[M]. is_depth_apply(M,h,p,rp) & 
   254                     is_bool_of_o(M, 
   255                            \<forall>x[M]. \<forall>xenv[M]. \<forall>hp[M]. 
   256                               x\<in>A --> is_Cons(M,x,env,xenv) --> 
   257                               fun_apply(M,rp,xenv,hp) --> number1(M,hp),
   258                   z),
   259                zz)"
   260 
   261 definition
   262   satisfies_MH :: "[i=>o,i,i,i,i]=>o" where
   263     --{*The variable @{term u} is unused, but gives @{term satisfies_MH} 
   264         the correct arity.*}
   265   "satisfies_MH == 
   266     \<lambda>M A u f z. 
   267          \<forall>fml[M]. is_formula(M,fml) -->
   268              is_lambda (M, fml, 
   269                is_formula_case (M, satisfies_is_a(M,A), 
   270                                 satisfies_is_b(M,A), 
   271                                 satisfies_is_c(M,A,f), satisfies_is_d(M,A,f)),
   272                z)"
   273 
   274 definition
   275   is_satisfies :: "[i=>o,i,i,i]=>o" where
   276   "is_satisfies(M,A) == is_formula_rec (M, satisfies_MH(M,A))"
   277 
   278 
   279 text{*This lemma relates the fragments defined above to the original primitive
   280       recursion in @{term satisfies}.
   281       Induction is not required: the definitions are directly equal!*}
   282 lemma satisfies_eq:
   283   "satisfies(A,p) = 
   284    formula_rec (satisfies_a(A), satisfies_b(A), 
   285                 satisfies_c(A), satisfies_d(A), p)"
   286 by (simp add: satisfies_formula_def satisfies_a_def satisfies_b_def 
   287               satisfies_c_def satisfies_d_def) 
   288 
   289 text{*Further constraints on the class @{term M} in order to prove
   290       absoluteness for the constants defined above.  The ultimate goal
   291       is the absoluteness of the function @{term satisfies}. *}
   292 locale M_satisfies = M_eclose +
   293  assumes 
   294    Member_replacement:
   295     "[|M(A); x \<in> nat; y \<in> nat|]
   296      ==> strong_replacement
   297 	 (M, \<lambda>env z. \<exists>bo[M]. \<exists>nx[M]. \<exists>ny[M]. 
   298               env \<in> list(A) & is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & 
   299               is_bool_of_o(M, nx \<in> ny, bo) &
   300               pair(M, env, bo, z))"
   301  and
   302    Equal_replacement:
   303     "[|M(A); x \<in> nat; y \<in> nat|]
   304      ==> strong_replacement
   305 	 (M, \<lambda>env z. \<exists>bo[M]. \<exists>nx[M]. \<exists>ny[M]. 
   306               env \<in> list(A) & is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & 
   307               is_bool_of_o(M, nx = ny, bo) &
   308               pair(M, env, bo, z))"
   309  and
   310    Nand_replacement:
   311     "[|M(A); M(rp); M(rq)|]
   312      ==> strong_replacement
   313 	 (M, \<lambda>env z. \<exists>rpe[M]. \<exists>rqe[M]. \<exists>andpq[M]. \<exists>notpq[M]. 
   314                fun_apply(M,rp,env,rpe) & fun_apply(M,rq,env,rqe) & 
   315                is_and(M,rpe,rqe,andpq) & is_not(M,andpq,notpq) & 
   316                env \<in> list(A) & pair(M, env, notpq, z))"
   317  and
   318   Forall_replacement:
   319    "[|M(A); M(rp)|]
   320     ==> strong_replacement
   321 	(M, \<lambda>env z. \<exists>bo[M]. 
   322 	      env \<in> list(A) & 
   323 	      is_bool_of_o (M, 
   324 			    \<forall>a[M]. \<forall>co[M]. \<forall>rpco[M]. 
   325 			       a\<in>A --> is_Cons(M,a,env,co) -->
   326 			       fun_apply(M,rp,co,rpco) --> number1(M, rpco), 
   327                             bo) &
   328 	      pair(M,env,bo,z))"
   329  and
   330   formula_rec_replacement: 
   331       --{*For the @{term transrec}*}
   332    "[|n \<in> nat; M(A)|] ==> transrec_replacement(M, satisfies_MH(M,A), n)"
   333  and
   334   formula_rec_lambda_replacement:  
   335       --{*For the @{text "\<lambda>-abstraction"} in the @{term transrec} body*}
   336    "[|M(g); M(A)|] ==>
   337     strong_replacement (M, 
   338        \<lambda>x y. mem_formula(M,x) &
   339              (\<exists>c[M]. is_formula_case(M, satisfies_is_a(M,A),
   340                                   satisfies_is_b(M,A),
   341                                   satisfies_is_c(M,A,g),
   342                                   satisfies_is_d(M,A,g), x, c) &
   343              pair(M, x, c, y)))"
   344 
   345 
   346 lemma (in M_satisfies) Member_replacement':
   347     "[|M(A); x \<in> nat; y \<in> nat|]
   348      ==> strong_replacement
   349 	 (M, \<lambda>env z. env \<in> list(A) &
   350 		     z = \<langle>env, bool_of_o(nth(x, env) \<in> nth(y, env))\<rangle>)"
   351 by (insert Member_replacement, simp) 
   352 
   353 lemma (in M_satisfies) Equal_replacement':
   354     "[|M(A); x \<in> nat; y \<in> nat|]
   355      ==> strong_replacement
   356 	 (M, \<lambda>env z. env \<in> list(A) &
   357 		     z = \<langle>env, bool_of_o(nth(x, env) = nth(y, env))\<rangle>)"
   358 by (insert Equal_replacement, simp) 
   359 
   360 lemma (in M_satisfies) Nand_replacement':
   361     "[|M(A); M(rp); M(rq)|]
   362      ==> strong_replacement
   363 	 (M, \<lambda>env z. env \<in> list(A) & z = \<langle>env, not(rp`env and rq`env)\<rangle>)"
   364 by (insert Nand_replacement, simp) 
   365 
   366 lemma (in M_satisfies) Forall_replacement':
   367    "[|M(A); M(rp)|]
   368     ==> strong_replacement
   369 	(M, \<lambda>env z.
   370 	       env \<in> list(A) &
   371 	       z = \<langle>env, bool_of_o (\<forall>a\<in>A. rp ` Cons(a,env) = 1)\<rangle>)"
   372 by (insert Forall_replacement, simp) 
   373 
   374 lemma (in M_satisfies) a_closed:
   375      "[|M(A); x\<in>nat; y\<in>nat|] ==> M(satisfies_a(A,x,y))"
   376 apply (simp add: satisfies_a_def) 
   377 apply (blast intro: lam_closed2 Member_replacement') 
   378 done
   379 
   380 lemma (in M_satisfies) a_rel:
   381      "M(A) ==> Relation2(M, nat, nat, satisfies_is_a(M,A), satisfies_a(A))"
   382 apply (simp add: Relation2_def satisfies_is_a_def satisfies_a_def)
   383 apply (auto del: iffI intro!: lambda_abs2 simp add: Relation1_def) 
   384 done
   385 
   386 lemma (in M_satisfies) b_closed:
   387      "[|M(A); x\<in>nat; y\<in>nat|] ==> M(satisfies_b(A,x,y))"
   388 apply (simp add: satisfies_b_def) 
   389 apply (blast intro: lam_closed2 Equal_replacement') 
   390 done
   391 
   392 lemma (in M_satisfies) b_rel:
   393      "M(A) ==> Relation2(M, nat, nat, satisfies_is_b(M,A), satisfies_b(A))"
   394 apply (simp add: Relation2_def satisfies_is_b_def satisfies_b_def)
   395 apply (auto del: iffI intro!: lambda_abs2 simp add: Relation1_def) 
   396 done
   397 
   398 lemma (in M_satisfies) c_closed:
   399      "[|M(A); x \<in> formula; y \<in> formula; M(rx); M(ry)|] 
   400       ==> M(satisfies_c(A,x,y,rx,ry))"
   401 apply (simp add: satisfies_c_def) 
   402 apply (rule lam_closed2) 
   403 apply (rule Nand_replacement') 
   404 apply (simp_all add: formula_into_M list_into_M [of _ A])
   405 done
   406 
   407 lemma (in M_satisfies) c_rel:
   408  "[|M(A); M(f)|] ==> 
   409   Relation2 (M, formula, formula, 
   410                satisfies_is_c(M,A,f),
   411 	       \<lambda>u v. satisfies_c(A, u, v, f ` succ(depth(u)) ` u, 
   412 					  f ` succ(depth(v)) ` v))"
   413 apply (simp add: Relation2_def satisfies_is_c_def satisfies_c_def)
   414 apply (auto del: iffI intro!: lambda_abs2 
   415             simp add: Relation1_def formula_into_M) 
   416 done
   417 
   418 lemma (in M_satisfies) d_closed:
   419      "[|M(A); x \<in> formula; M(rx)|] ==> M(satisfies_d(A,x,rx))"
   420 apply (simp add: satisfies_d_def) 
   421 apply (rule lam_closed2) 
   422 apply (rule Forall_replacement') 
   423 apply (simp_all add: formula_into_M list_into_M [of _ A])
   424 done
   425 
   426 lemma (in M_satisfies) d_rel:
   427  "[|M(A); M(f)|] ==> 
   428   Relation1(M, formula, satisfies_is_d(M,A,f), 
   429      \<lambda>u. satisfies_d(A, u, f ` succ(depth(u)) ` u))"
   430 apply (simp del: rall_abs 
   431             add: Relation1_def satisfies_is_d_def satisfies_d_def)
   432 apply (auto del: iffI intro!: lambda_abs2 simp add: Relation1_def) 
   433 done
   434 
   435 
   436 lemma (in M_satisfies) fr_replace:
   437       "[|n \<in> nat; M(A)|] ==> transrec_replacement(M,satisfies_MH(M,A),n)" 
   438 by (blast intro: formula_rec_replacement) 
   439 
   440 lemma (in M_satisfies) formula_case_satisfies_closed:
   441  "[|M(g); M(A); x \<in> formula|] ==>
   442   M(formula_case (satisfies_a(A), satisfies_b(A),
   443        \<lambda>u v. satisfies_c(A, u, v, 
   444                          g ` succ(depth(u)) ` u, g ` succ(depth(v)) ` v),
   445        \<lambda>u. satisfies_d (A, u, g ` succ(depth(u)) ` u),
   446        x))"
   447 by (blast intro: formula_case_closed a_closed b_closed c_closed d_closed) 
   448 
   449 lemma (in M_satisfies) fr_lam_replace:
   450    "[|M(g); M(A)|] ==>
   451     strong_replacement (M, \<lambda>x y. x \<in> formula &
   452             y = \<langle>x, 
   453                  formula_rec_case(satisfies_a(A),
   454                                   satisfies_b(A),
   455                                   satisfies_c(A),
   456                                   satisfies_d(A), g, x)\<rangle>)"
   457 apply (insert formula_rec_lambda_replacement) 
   458 apply (simp add: formula_rec_case_def formula_case_satisfies_closed
   459                  formula_case_abs [OF a_rel b_rel c_rel d_rel]) 
   460 done
   461 
   462 
   463 
   464 text{*Instantiate locale @{text Formula_Rec} for the 
   465       Function @{term satisfies}*}
   466 
   467 lemma (in M_satisfies) Formula_Rec_axioms_M:
   468    "M(A) ==>
   469     Formula_Rec_axioms(M, satisfies_a(A), satisfies_is_a(M,A), 
   470 			  satisfies_b(A), satisfies_is_b(M,A), 
   471 			  satisfies_c(A), satisfies_is_c(M,A), 
   472 			  satisfies_d(A), satisfies_is_d(M,A))"
   473 apply (rule Formula_Rec_axioms.intro)
   474 apply (assumption | 
   475        rule a_closed a_rel b_closed b_rel c_closed c_rel d_closed d_rel
   476        fr_replace [unfolded satisfies_MH_def]
   477        fr_lam_replace) +
   478 done
   479 
   480 
   481 theorem (in M_satisfies) Formula_Rec_M: 
   482     "M(A) ==>
   483      PROP Formula_Rec(M, satisfies_a(A), satisfies_is_a(M,A), 
   484 			 satisfies_b(A), satisfies_is_b(M,A), 
   485 			 satisfies_c(A), satisfies_is_c(M,A), 
   486 			 satisfies_d(A), satisfies_is_d(M,A))"
   487   apply (rule Formula_Rec.intro)
   488    apply (rule M_satisfies.axioms, rule M_satisfies_axioms)
   489   apply (erule Formula_Rec_axioms_M) 
   490   done
   491 
   492 lemmas (in M_satisfies) 
   493     satisfies_closed' = Formula_Rec.formula_rec_closed [OF Formula_Rec_M]
   494 and satisfies_abs'    = Formula_Rec.formula_rec_abs [OF Formula_Rec_M]
   495 
   496 
   497 lemma (in M_satisfies) satisfies_closed:
   498   "[|M(A); p \<in> formula|] ==> M(satisfies(A,p))"
   499 by (simp add: Formula_Rec.formula_rec_closed [OF Formula_Rec_M]  
   500               satisfies_eq) 
   501 
   502 lemma (in M_satisfies) satisfies_abs:
   503   "[|M(A); M(z); p \<in> formula|] 
   504    ==> is_satisfies(M,A,p,z) <-> z = satisfies(A,p)"
   505 by (simp only: Formula_Rec.formula_rec_abs [OF Formula_Rec_M]  
   506                satisfies_eq is_satisfies_def satisfies_MH_def)
   507 
   508 
   509 subsection{*Internalizations Needed to Instantiate @{text "M_satisfies"}*}
   510 
   511 subsubsection{*The Operator @{term is_depth_apply}, Internalized*}
   512 
   513 (* is_depth_apply(M,h,p,z) ==
   514     \<exists>dp[M]. \<exists>sdp[M]. \<exists>hsdp[M]. 
   515       2        1         0
   516 	finite_ordinal(M,dp) & is_depth(M,p,dp) & successor(M,dp,sdp) &
   517 	fun_apply(M,h,sdp,hsdp) & fun_apply(M,hsdp,p,z) *)
   518 definition
   519   depth_apply_fm :: "[i,i,i]=>i" where
   520     "depth_apply_fm(h,p,z) ==
   521        Exists(Exists(Exists(
   522         And(finite_ordinal_fm(2),
   523          And(depth_fm(p#+3,2),
   524           And(succ_fm(2,1),
   525            And(fun_apply_fm(h#+3,1,0), fun_apply_fm(0,p#+3,z#+3))))))))"
   526 
   527 lemma depth_apply_type [TC]:
   528      "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> depth_apply_fm(x,y,z) \<in> formula"
   529 by (simp add: depth_apply_fm_def)
   530 
   531 lemma sats_depth_apply_fm [simp]:
   532    "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   533     ==> sats(A, depth_apply_fm(x,y,z), env) <->
   534         is_depth_apply(##A, nth(x,env), nth(y,env), nth(z,env))"
   535 by (simp add: depth_apply_fm_def is_depth_apply_def)
   536 
   537 lemma depth_apply_iff_sats:
   538     "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
   539         i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
   540      ==> is_depth_apply(##A, x, y, z) <-> sats(A, depth_apply_fm(i,j,k), env)"
   541 by simp
   542 
   543 lemma depth_apply_reflection:
   544      "REFLECTS[\<lambda>x. is_depth_apply(L,f(x),g(x),h(x)),
   545                \<lambda>i x. is_depth_apply(##Lset(i),f(x),g(x),h(x))]"
   546 apply (simp only: is_depth_apply_def)
   547 apply (intro FOL_reflections function_reflections depth_reflection 
   548              finite_ordinal_reflection)
   549 done
   550 
   551 
   552 subsubsection{*The Operator @{term satisfies_is_a}, Internalized*}
   553 
   554 (* satisfies_is_a(M,A) == 
   555     \<lambda>x y zz. \<forall>lA[M]. is_list(M,A,lA) -->
   556              is_lambda(M, lA, 
   557 		\<lambda>env z. is_bool_of_o(M, 
   558                       \<exists>nx[M]. \<exists>ny[M]. 
   559  		       is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & nx \<in> ny, z),
   560                 zz)  *)
   561 
   562 definition
   563   satisfies_is_a_fm :: "[i,i,i,i]=>i" where
   564   "satisfies_is_a_fm(A,x,y,z) ==
   565    Forall(
   566      Implies(is_list_fm(succ(A),0),
   567        lambda_fm(
   568          bool_of_o_fm(Exists(
   569                        Exists(And(nth_fm(x#+6,3,1), 
   570                                And(nth_fm(y#+6,3,0), 
   571                                    Member(1,0))))), 0), 
   572          0, succ(z))))"
   573 
   574 lemma satisfies_is_a_type [TC]:
   575      "[| A \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
   576       ==> satisfies_is_a_fm(A,x,y,z) \<in> formula"
   577 by (simp add: satisfies_is_a_fm_def)
   578 
   579 lemma sats_satisfies_is_a_fm [simp]:
   580    "[| u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)|]
   581     ==> sats(A, satisfies_is_a_fm(u,x,y,z), env) <->
   582         satisfies_is_a(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
   583 apply (frule_tac x=x in lt_length_in_nat, assumption)  
   584 apply (frule_tac x=y in lt_length_in_nat, assumption)  
   585 apply (simp add: satisfies_is_a_fm_def satisfies_is_a_def sats_lambda_fm 
   586                  sats_bool_of_o_fm)
   587 done
   588 
   589 lemma satisfies_is_a_iff_sats:
   590   "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
   591       u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)|]
   592    ==> satisfies_is_a(##A,nu,nx,ny,nz) <->
   593        sats(A, satisfies_is_a_fm(u,x,y,z), env)"
   594 by simp
   595 
   596 theorem satisfies_is_a_reflection:
   597      "REFLECTS[\<lambda>x. satisfies_is_a(L,f(x),g(x),h(x),g'(x)),
   598                \<lambda>i x. satisfies_is_a(##Lset(i),f(x),g(x),h(x),g'(x))]"
   599 apply (unfold satisfies_is_a_def) 
   600 apply (intro FOL_reflections is_lambda_reflection bool_of_o_reflection 
   601              nth_reflection is_list_reflection)
   602 done
   603 
   604 
   605 subsubsection{*The Operator @{term satisfies_is_b}, Internalized*}
   606 
   607 (* satisfies_is_b(M,A) == 
   608     \<lambda>x y zz. \<forall>lA[M]. is_list(M,A,lA) -->
   609              is_lambda(M, lA, 
   610                 \<lambda>env z. is_bool_of_o(M, 
   611                       \<exists>nx[M]. is_nth(M,x,env,nx) & is_nth(M,y,env,nx), z),
   612                 zz) *)
   613 
   614 definition
   615   satisfies_is_b_fm :: "[i,i,i,i]=>i" where
   616  "satisfies_is_b_fm(A,x,y,z) ==
   617    Forall(
   618      Implies(is_list_fm(succ(A),0),
   619        lambda_fm(
   620          bool_of_o_fm(Exists(And(nth_fm(x#+5,2,0), nth_fm(y#+5,2,0))), 0), 
   621          0, succ(z))))"
   622 
   623 lemma satisfies_is_b_type [TC]:
   624      "[| A \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
   625       ==> satisfies_is_b_fm(A,x,y,z) \<in> formula"
   626 by (simp add: satisfies_is_b_fm_def)
   627 
   628 lemma sats_satisfies_is_b_fm [simp]:
   629    "[| u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)|]
   630     ==> sats(A, satisfies_is_b_fm(u,x,y,z), env) <->
   631         satisfies_is_b(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
   632 apply (frule_tac x=x in lt_length_in_nat, assumption)  
   633 apply (frule_tac x=y in lt_length_in_nat, assumption)  
   634 apply (simp add: satisfies_is_b_fm_def satisfies_is_b_def sats_lambda_fm 
   635                  sats_bool_of_o_fm)
   636 done
   637 
   638 lemma satisfies_is_b_iff_sats:
   639   "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
   640       u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)|]
   641    ==> satisfies_is_b(##A,nu,nx,ny,nz) <->
   642        sats(A, satisfies_is_b_fm(u,x,y,z), env)"
   643 by simp
   644 
   645 theorem satisfies_is_b_reflection:
   646      "REFLECTS[\<lambda>x. satisfies_is_b(L,f(x),g(x),h(x),g'(x)),
   647                \<lambda>i x. satisfies_is_b(##Lset(i),f(x),g(x),h(x),g'(x))]"
   648 apply (unfold satisfies_is_b_def) 
   649 apply (intro FOL_reflections is_lambda_reflection bool_of_o_reflection 
   650              nth_reflection is_list_reflection)
   651 done
   652 
   653 
   654 subsubsection{*The Operator @{term satisfies_is_c}, Internalized*}
   655 
   656 (* satisfies_is_c(M,A,h) == 
   657     \<lambda>p q zz. \<forall>lA[M]. is_list(M,A,lA) -->
   658              is_lambda(M, lA, \<lambda>env z. \<exists>hp[M]. \<exists>hq[M]. 
   659 		 (\<exists>rp[M]. is_depth_apply(M,h,p,rp) & fun_apply(M,rp,env,hp)) & 
   660 		 (\<exists>rq[M]. is_depth_apply(M,h,q,rq) & fun_apply(M,rq,env,hq)) & 
   661                  (\<exists>pq[M]. is_and(M,hp,hq,pq) & is_not(M,pq,z)),
   662                 zz) *)
   663 
   664 definition
   665   satisfies_is_c_fm :: "[i,i,i,i,i]=>i" where
   666  "satisfies_is_c_fm(A,h,p,q,zz) ==
   667    Forall(
   668      Implies(is_list_fm(succ(A),0),
   669        lambda_fm(
   670          Exists(Exists(
   671           And(Exists(And(depth_apply_fm(h#+7,p#+7,0), fun_apply_fm(0,4,2))),
   672           And(Exists(And(depth_apply_fm(h#+7,q#+7,0), fun_apply_fm(0,4,1))),
   673               Exists(And(and_fm(2,1,0), not_fm(0,3))))))),
   674          0, succ(zz))))"
   675 
   676 lemma satisfies_is_c_type [TC]:
   677      "[| A \<in> nat; h \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat |]
   678       ==> satisfies_is_c_fm(A,h,x,y,z) \<in> formula"
   679 by (simp add: satisfies_is_c_fm_def)
   680 
   681 lemma sats_satisfies_is_c_fm [simp]:
   682    "[| u \<in> nat; v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   683     ==> sats(A, satisfies_is_c_fm(u,v,x,y,z), env) <->
   684         satisfies_is_c(##A, nth(u,env), nth(v,env), nth(x,env), 
   685                             nth(y,env), nth(z,env))"  
   686 by (simp add: satisfies_is_c_fm_def satisfies_is_c_def sats_lambda_fm)
   687 
   688 lemma satisfies_is_c_iff_sats:
   689   "[| nth(u,env) = nu; nth(v,env) = nv; nth(x,env) = nx; nth(y,env) = ny; 
   690       nth(z,env) = nz;
   691       u \<in> nat; v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   692    ==> satisfies_is_c(##A,nu,nv,nx,ny,nz) <->
   693        sats(A, satisfies_is_c_fm(u,v,x,y,z), env)"
   694 by simp
   695 
   696 theorem satisfies_is_c_reflection:
   697      "REFLECTS[\<lambda>x. satisfies_is_c(L,f(x),g(x),h(x),g'(x),h'(x)),
   698                \<lambda>i x. satisfies_is_c(##Lset(i),f(x),g(x),h(x),g'(x),h'(x))]"
   699 apply (unfold satisfies_is_c_def) 
   700 apply (intro FOL_reflections function_reflections is_lambda_reflection
   701              extra_reflections nth_reflection depth_apply_reflection 
   702              is_list_reflection)
   703 done
   704 
   705 subsubsection{*The Operator @{term satisfies_is_d}, Internalized*}
   706 
   707 (* satisfies_is_d(M,A,h) == 
   708     \<lambda>p zz. \<forall>lA[M]. is_list(M,A,lA) -->
   709              is_lambda(M, lA, 
   710                 \<lambda>env z. \<exists>rp[M]. is_depth_apply(M,h,p,rp) & 
   711                     is_bool_of_o(M, 
   712                            \<forall>x[M]. \<forall>xenv[M]. \<forall>hp[M]. 
   713                               x\<in>A --> is_Cons(M,x,env,xenv) --> 
   714                               fun_apply(M,rp,xenv,hp) --> number1(M,hp),
   715                   z),
   716                zz) *)
   717 
   718 definition
   719   satisfies_is_d_fm :: "[i,i,i,i]=>i" where
   720  "satisfies_is_d_fm(A,h,p,zz) ==
   721    Forall(
   722      Implies(is_list_fm(succ(A),0),
   723        lambda_fm(
   724          Exists(
   725            And(depth_apply_fm(h#+5,p#+5,0),
   726                bool_of_o_fm(
   727                 Forall(Forall(Forall(
   728                  Implies(Member(2,A#+8),
   729                   Implies(Cons_fm(2,5,1),
   730                    Implies(fun_apply_fm(3,1,0), number1_fm(0))))))), 1))),
   731          0, succ(zz))))"
   732 
   733 lemma satisfies_is_d_type [TC]:
   734      "[| A \<in> nat; h \<in> nat; x \<in> nat; z \<in> nat |]
   735       ==> satisfies_is_d_fm(A,h,x,z) \<in> formula"
   736 by (simp add: satisfies_is_d_fm_def)
   737 
   738 lemma sats_satisfies_is_d_fm [simp]:
   739    "[| u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   740     ==> sats(A, satisfies_is_d_fm(u,x,y,z), env) <->
   741         satisfies_is_d(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"  
   742 by (simp add: satisfies_is_d_fm_def satisfies_is_d_def sats_lambda_fm
   743               sats_bool_of_o_fm)
   744 
   745 lemma satisfies_is_d_iff_sats:
   746   "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
   747       u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   748    ==> satisfies_is_d(##A,nu,nx,ny,nz) <->
   749        sats(A, satisfies_is_d_fm(u,x,y,z), env)"
   750 by simp
   751 
   752 theorem satisfies_is_d_reflection:
   753      "REFLECTS[\<lambda>x. satisfies_is_d(L,f(x),g(x),h(x),g'(x)),
   754                \<lambda>i x. satisfies_is_d(##Lset(i),f(x),g(x),h(x),g'(x))]"
   755 apply (unfold satisfies_is_d_def) 
   756 apply (intro FOL_reflections function_reflections is_lambda_reflection
   757              extra_reflections nth_reflection depth_apply_reflection 
   758              is_list_reflection)
   759 done
   760 
   761 
   762 subsubsection{*The Operator @{term satisfies_MH}, Internalized*}
   763 
   764 (* satisfies_MH == 
   765     \<lambda>M A u f zz. 
   766          \<forall>fml[M]. is_formula(M,fml) -->
   767              is_lambda (M, fml, 
   768                is_formula_case (M, satisfies_is_a(M,A), 
   769                                 satisfies_is_b(M,A), 
   770                                 satisfies_is_c(M,A,f), satisfies_is_d(M,A,f)),
   771                zz) *)
   772 
   773 definition
   774   satisfies_MH_fm :: "[i,i,i,i]=>i" where
   775  "satisfies_MH_fm(A,u,f,zz) ==
   776    Forall(
   777      Implies(is_formula_fm(0),
   778        lambda_fm(
   779          formula_case_fm(satisfies_is_a_fm(A#+7,2,1,0), 
   780                          satisfies_is_b_fm(A#+7,2,1,0), 
   781                          satisfies_is_c_fm(A#+7,f#+7,2,1,0), 
   782                          satisfies_is_d_fm(A#+6,f#+6,1,0), 
   783                          1, 0),
   784          0, succ(zz))))"
   785 
   786 lemma satisfies_MH_type [TC]:
   787      "[| A \<in> nat; u \<in> nat; x \<in> nat; z \<in> nat |]
   788       ==> satisfies_MH_fm(A,u,x,z) \<in> formula"
   789 by (simp add: satisfies_MH_fm_def)
   790 
   791 lemma sats_satisfies_MH_fm [simp]:
   792    "[| u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   793     ==> sats(A, satisfies_MH_fm(u,x,y,z), env) <->
   794         satisfies_MH(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"  
   795 by (simp add: satisfies_MH_fm_def satisfies_MH_def sats_lambda_fm
   796               sats_formula_case_fm)
   797 
   798 lemma satisfies_MH_iff_sats:
   799   "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
   800       u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
   801    ==> satisfies_MH(##A,nu,nx,ny,nz) <->
   802        sats(A, satisfies_MH_fm(u,x,y,z), env)"
   803 by simp 
   804 
   805 lemmas satisfies_reflections =
   806        is_lambda_reflection is_formula_reflection 
   807        is_formula_case_reflection
   808        satisfies_is_a_reflection satisfies_is_b_reflection 
   809        satisfies_is_c_reflection satisfies_is_d_reflection
   810 
   811 theorem satisfies_MH_reflection:
   812      "REFLECTS[\<lambda>x. satisfies_MH(L,f(x),g(x),h(x),g'(x)),
   813                \<lambda>i x. satisfies_MH(##Lset(i),f(x),g(x),h(x),g'(x))]"
   814 apply (unfold satisfies_MH_def) 
   815 apply (intro FOL_reflections satisfies_reflections)
   816 done
   817 
   818 
   819 subsection{*Lemmas for Instantiating the Locale @{text "M_satisfies"}*}
   820 
   821 
   822 subsubsection{*The @{term "Member"} Case*}
   823 
   824 lemma Member_Reflects:
   825  "REFLECTS[\<lambda>u. \<exists>v[L]. v \<in> B \<and> (\<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L].
   826           v \<in> lstA \<and> is_nth(L,x,v,nx) \<and> is_nth(L,y,v,ny) \<and>
   827           is_bool_of_o(L, nx \<in> ny, bo) \<and> pair(L,v,bo,u)),
   828    \<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).
   829              v \<in> lstA \<and> is_nth(##Lset(i), x, v, nx) \<and> 
   830              is_nth(##Lset(i), y, v, ny) \<and>
   831           is_bool_of_o(##Lset(i), nx \<in> ny, bo) \<and> pair(##Lset(i), v, bo, u))]"
   832 by (intro FOL_reflections function_reflections nth_reflection 
   833           bool_of_o_reflection)
   834 
   835 
   836 lemma Member_replacement:
   837     "[|L(A); x \<in> nat; y \<in> nat|]
   838      ==> strong_replacement
   839 	 (L, \<lambda>env z. \<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L]. 
   840               env \<in> list(A) & is_nth(L,x,env,nx) & is_nth(L,y,env,ny) & 
   841               is_bool_of_o(L, nx \<in> ny, bo) &
   842               pair(L, env, bo, z))"
   843 apply (rule strong_replacementI)
   844 apply (rule_tac u="{list(A),B,x,y}" 
   845          in gen_separation_multi [OF Member_Reflects], 
   846        auto simp add: nat_into_M list_closed)
   847 apply (rule_tac env="[list(A),B,x,y]" in DPow_LsetI)
   848 apply (rule sep_rules nth_iff_sats is_bool_of_o_iff_sats | simp)+
   849 done
   850 
   851 
   852 subsubsection{*The @{term "Equal"} Case*}
   853 
   854 lemma Equal_Reflects:
   855  "REFLECTS[\<lambda>u. \<exists>v[L]. v \<in> B \<and> (\<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L].
   856           v \<in> lstA \<and> is_nth(L, x, v, nx) \<and> is_nth(L, y, v, ny) \<and>
   857           is_bool_of_o(L, nx = ny, bo) \<and> pair(L, v, bo, u)),
   858    \<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).
   859              v \<in> lstA \<and> is_nth(##Lset(i), x, v, nx) \<and> 
   860              is_nth(##Lset(i), y, v, ny) \<and>
   861           is_bool_of_o(##Lset(i), nx = ny, bo) \<and> pair(##Lset(i), v, bo, u))]"
   862 by (intro FOL_reflections function_reflections nth_reflection 
   863           bool_of_o_reflection)
   864 
   865 
   866 lemma Equal_replacement:
   867     "[|L(A); x \<in> nat; y \<in> nat|]
   868      ==> strong_replacement
   869 	 (L, \<lambda>env z. \<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L]. 
   870               env \<in> list(A) & is_nth(L,x,env,nx) & is_nth(L,y,env,ny) & 
   871               is_bool_of_o(L, nx = ny, bo) &
   872               pair(L, env, bo, z))"
   873 apply (rule strong_replacementI)
   874 apply (rule_tac u="{list(A),B,x,y}" 
   875          in gen_separation_multi [OF Equal_Reflects], 
   876        auto simp add: nat_into_M list_closed)
   877 apply (rule_tac env="[list(A),B,x,y]" in DPow_LsetI)
   878 apply (rule sep_rules nth_iff_sats is_bool_of_o_iff_sats | simp)+
   879 done
   880 
   881 subsubsection{*The @{term "Nand"} Case*}
   882 
   883 lemma Nand_Reflects:
   884     "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B \<and>
   885 	       (\<exists>rpe[L]. \<exists>rqe[L]. \<exists>andpq[L]. \<exists>notpq[L].
   886 		 fun_apply(L, rp, u, rpe) \<and> fun_apply(L, rq, u, rqe) \<and>
   887 		 is_and(L, rpe, rqe, andpq) \<and> is_not(L, andpq, notpq) \<and>
   888 		 u \<in> list(A) \<and> pair(L, u, notpq, x)),
   889     \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and>
   890      (\<exists>rpe \<in> Lset(i). \<exists>rqe \<in> Lset(i). \<exists>andpq \<in> Lset(i). \<exists>notpq \<in> Lset(i).
   891        fun_apply(##Lset(i), rp, u, rpe) \<and> fun_apply(##Lset(i), rq, u, rqe) \<and>
   892        is_and(##Lset(i), rpe, rqe, andpq) \<and> is_not(##Lset(i), andpq, notpq) \<and>
   893        u \<in> list(A) \<and> pair(##Lset(i), u, notpq, x))]"
   894 apply (unfold is_and_def is_not_def) 
   895 apply (intro FOL_reflections function_reflections)
   896 done
   897 
   898 lemma Nand_replacement:
   899     "[|L(A); L(rp); L(rq)|]
   900      ==> strong_replacement
   901 	 (L, \<lambda>env z. \<exists>rpe[L]. \<exists>rqe[L]. \<exists>andpq[L]. \<exists>notpq[L]. 
   902                fun_apply(L,rp,env,rpe) & fun_apply(L,rq,env,rqe) & 
   903                is_and(L,rpe,rqe,andpq) & is_not(L,andpq,notpq) & 
   904                env \<in> list(A) & pair(L, env, notpq, z))"
   905 apply (rule strong_replacementI)
   906 apply (rule_tac u="{list(A),B,rp,rq}" 
   907          in gen_separation_multi [OF Nand_Reflects],
   908        auto simp add: list_closed)
   909 apply (rule_tac env="[list(A),B,rp,rq]" in DPow_LsetI)
   910 apply (rule sep_rules is_and_iff_sats is_not_iff_sats | simp)+
   911 done
   912 
   913 
   914 subsubsection{*The @{term "Forall"} Case*}
   915 
   916 lemma Forall_Reflects:
   917  "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>bo[L]. u \<in> list(A) \<and>
   918                  is_bool_of_o (L,
   919      \<forall>a[L]. \<forall>co[L]. \<forall>rpco[L]. a \<in> A \<longrightarrow>
   920                 is_Cons(L,a,u,co) \<longrightarrow> fun_apply(L,rp,co,rpco) \<longrightarrow> 
   921                 number1(L,rpco),
   922                            bo) \<and> pair(L,u,bo,x)),
   923  \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>bo \<in> Lset(i). u \<in> list(A) \<and>
   924         is_bool_of_o (##Lset(i),
   925  \<forall>a \<in> Lset(i). \<forall>co \<in> Lset(i). \<forall>rpco \<in> Lset(i). a \<in> A \<longrightarrow>
   926 	    is_Cons(##Lset(i),a,u,co) \<longrightarrow> fun_apply(##Lset(i),rp,co,rpco) \<longrightarrow> 
   927 	    number1(##Lset(i),rpco),
   928 		       bo) \<and> pair(##Lset(i),u,bo,x))]"
   929 apply (unfold is_bool_of_o_def) 
   930 apply (intro FOL_reflections function_reflections Cons_reflection)
   931 done
   932 
   933 lemma Forall_replacement:
   934    "[|L(A); L(rp)|]
   935     ==> strong_replacement
   936 	(L, \<lambda>env z. \<exists>bo[L]. 
   937 	      env \<in> list(A) & 
   938 	      is_bool_of_o (L, 
   939 			    \<forall>a[L]. \<forall>co[L]. \<forall>rpco[L]. 
   940 			       a\<in>A --> is_Cons(L,a,env,co) -->
   941 			       fun_apply(L,rp,co,rpco) --> number1(L, rpco), 
   942                             bo) &
   943 	      pair(L,env,bo,z))"
   944 apply (rule strong_replacementI)
   945 apply (rule_tac u="{A,list(A),B,rp}" 
   946          in gen_separation_multi [OF Forall_Reflects],
   947        auto simp add: list_closed)
   948 apply (rule_tac env="[A,list(A),B,rp]" in DPow_LsetI)
   949 apply (rule sep_rules is_bool_of_o_iff_sats Cons_iff_sats | simp)+
   950 done
   951 
   952 subsubsection{*The @{term "transrec_replacement"} Case*}
   953 
   954 lemma formula_rec_replacement_Reflects:
   955  "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L, u, y, x) \<and>
   956              is_wfrec (L, satisfies_MH(L,A), mesa, u, y)),
   957     \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) \<and>
   958              is_wfrec (##Lset(i), satisfies_MH(##Lset(i),A), mesa, u, y))]"
   959 by (intro FOL_reflections function_reflections satisfies_MH_reflection 
   960           is_wfrec_reflection) 
   961 
   962 lemma formula_rec_replacement: 
   963       --{*For the @{term transrec}*}
   964    "[|n \<in> nat; L(A)|] ==> transrec_replacement(L, satisfies_MH(L,A), n)"
   965 apply (rule transrec_replacementI, simp add: nat_into_M) 
   966 apply (rule strong_replacementI)
   967 apply (rule_tac u="{B,A,n,Memrel(eclose({n}))}"
   968          in gen_separation_multi [OF formula_rec_replacement_Reflects],
   969        auto simp add: nat_into_M)
   970 apply (rule_tac env="[B,A,n,Memrel(eclose({n}))]" in DPow_LsetI)
   971 apply (rule sep_rules satisfies_MH_iff_sats is_wfrec_iff_sats | simp)+
   972 done
   973 
   974 
   975 subsubsection{*The Lambda Replacement Case*}
   976 
   977 lemma formula_rec_lambda_replacement_Reflects:
   978  "REFLECTS [\<lambda>x. \<exists>u[L]. u \<in> B &
   979      mem_formula(L,u) &
   980      (\<exists>c[L].
   981 	 is_formula_case
   982 	  (L, satisfies_is_a(L,A), satisfies_is_b(L,A),
   983 	   satisfies_is_c(L,A,g), satisfies_is_d(L,A,g),
   984 	   u, c) &
   985 	 pair(L,u,c,x)),
   986   \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B & mem_formula(##Lset(i),u) &
   987      (\<exists>c \<in> Lset(i).
   988 	 is_formula_case
   989 	  (##Lset(i), satisfies_is_a(##Lset(i),A), satisfies_is_b(##Lset(i),A),
   990 	   satisfies_is_c(##Lset(i),A,g), satisfies_is_d(##Lset(i),A,g),
   991 	   u, c) &
   992 	 pair(##Lset(i),u,c,x))]"
   993 by (intro FOL_reflections function_reflections mem_formula_reflection
   994           is_formula_case_reflection satisfies_is_a_reflection
   995           satisfies_is_b_reflection satisfies_is_c_reflection
   996           satisfies_is_d_reflection)  
   997 
   998 lemma formula_rec_lambda_replacement: 
   999       --{*For the @{term transrec}*}
  1000    "[|L(g); L(A)|] ==>
  1001     strong_replacement (L, 
  1002        \<lambda>x y. mem_formula(L,x) &
  1003              (\<exists>c[L]. is_formula_case(L, satisfies_is_a(L,A),
  1004                                   satisfies_is_b(L,A),
  1005                                   satisfies_is_c(L,A,g),
  1006                                   satisfies_is_d(L,A,g), x, c) &
  1007              pair(L, x, c, y)))" 
  1008 apply (rule strong_replacementI)
  1009 apply (rule_tac u="{B,A,g}"
  1010          in gen_separation_multi [OF formula_rec_lambda_replacement_Reflects], 
  1011        auto)
  1012 apply (rule_tac env="[A,g,B]" in DPow_LsetI)
  1013 apply (rule sep_rules mem_formula_iff_sats
  1014           formula_case_iff_sats satisfies_is_a_iff_sats
  1015           satisfies_is_b_iff_sats satisfies_is_c_iff_sats
  1016           satisfies_is_d_iff_sats | simp)+
  1017 done
  1018 
  1019 
  1020 subsection{*Instantiating @{text M_satisfies}*}
  1021 
  1022 lemma M_satisfies_axioms_L: "M_satisfies_axioms(L)"
  1023   apply (rule M_satisfies_axioms.intro)
  1024        apply (assumption | rule
  1025 	 Member_replacement Equal_replacement 
  1026          Nand_replacement Forall_replacement
  1027          formula_rec_replacement formula_rec_lambda_replacement)+
  1028   done
  1029 
  1030 theorem M_satisfies_L: "PROP M_satisfies(L)"
  1031   apply (rule M_satisfies.intro)
  1032    apply (rule M_eclose_L)
  1033   apply (rule M_satisfies_axioms_L)
  1034   done
  1035 
  1036 text{*Finally: the point of the whole theory!*}
  1037 lemmas satisfies_closed = M_satisfies.satisfies_closed [OF M_satisfies_L]
  1038    and satisfies_abs = M_satisfies.satisfies_abs [OF M_satisfies_L]
  1039 
  1040 end