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