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