Impressum Satisfies_absolute.thy Interaktion und
PortierbarkeitIsabelle

(*  Title:      ZF/Constructible/Satisfies_absolute.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
*)

section \<open>Absoluteness for the Satisfies Relation on Formulas\<close>

theory Satisfies_absolute imports Datatype_absolute Rec_Separation begin

subsection \<open>More Internalization\<close>

subsubsection\<open>The Formula \<^term>\<open>is_depth\<close>, Internalized\<close>

(*    "is_depth(M,p,n) \<equiv>
       \<exists>sn[M]. \<exists>formula_n[M]. \<exists>formula_sn[M].
         2          1                0
        is_formula_N(M,n,formula_n) \<and> p \<notin> formula_n \<and>
        successor(M,n,sn) \<and> is_formula_N(M,sn,formula_sn) \<and> p \<in> formula_sn" *)
definition
  depth_fm :: "[i,i]\i" where
  "depth_fm(p,n) \
     Exists(Exists(Exists(
       And(formula_N_fm(n#+3,1),
         And(Neg(Member(p#+3,1)),
          And(succ_fm(n#+3,2),
           And(formula_N_fm(2,0), Member(p#+3,0))))))))"

lemma depth_fm_type [TC]:
"\x \ nat; y \ nat\ \ depth_fm(x,y) \ formula"
by (simp add: depth_fm_def)

lemma sats_depth_fm [simp]:
   "\x \ nat; y < length(env); env \ list(A)\
    \<Longrightarrow> sats(A, depth_fm(x,y), env) \<longleftrightarrow>
        is_depth(##A, nth(x,env), nth(y,env))"
apply (frule_tac x=y in lt_length_in_nat, assumption)
apply (simp add: depth_fm_def is_depth_def)
done

lemma depth_iff_sats:
      "\nth(i,env) = x; nth(j,env) = y;
          i \<in> nat; j < length(env); env \<in> list(A)\<rbrakk>
       \<Longrightarrow> is_depth(##A, x, y) \<longleftrightarrow> sats(A, depth_fm(i,j), env)"
by (simp)

theorem depth_reflection:
     "REFLECTS[\x. is_depth(L, f(x), g(x)),
               \<lambda>i x. is_depth(##Lset(i), f(x), g(x))]"
apply (simp only: is_depth_def)
apply (intro FOL_reflections function_reflections formula_N_reflection)
done

subsubsection\<open>The Operator \<^term>\<open>is_formula_case\<close>\<close>

text\<open>The arguments of \<^term>\<open>is_a\<close> are always 2, 1, 0, and the formula
      will be enclosed by three quantifiers.\<close>

(* is_formula_case ::
    "[i\<Rightarrow>o, [i,i,i]\<Rightarrow>o, [i,i,i]\<Rightarrow>o, [i,i,i]\<Rightarrow>o, [i,i]\<Rightarrow>o, i, i] \<Rightarrow> o"
  "is_formula_case(M, is_a, is_b, is_c, is_d, v, z) \<equiv>
      (\<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)) \<and>
      (\<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)) \<and>
      (\<forall>x[M]. \<forall>y[M]. x\<in>formula \<longrightarrow> y\<in>formula \<longrightarrow>
                     is_Nand(M,x,y,v) \<longrightarrow> is_c(x,y,z)) \<and>
      (\<forall>x[M]. x\<in>formula \<longrightarrow> is_Forall(M,x,v) \<longrightarrow> is_d(x,z))" *)

definition
  formula_case_fm :: "[i, i, i, i, i, i]\i" where
  "formula_case_fm(is_a, is_b, is_c, is_d, v, z) \
        And(Forall(Forall(Implies(finite_ordinal_fm(1),
                           Implies(finite_ordinal_fm(0),
                            Implies(Member_fm(1,0,v#+2),
                             Forall(Implies(Equal(0,z#+3), is_a))))))),
        And(Forall(Forall(Implies(finite_ordinal_fm(1),
                           Implies(finite_ordinal_fm(0),
                            Implies(Equal_fm(1,0,v#+2),
                             Forall(Implies(Equal(0,z#+3), is_b))))))),
        And(Forall(Forall(Implies(mem_formula_fm(1),
                           Implies(mem_formula_fm(0),
                            Implies(Nand_fm(1,0,v#+2),
                             Forall(Implies(Equal(0,z#+3), is_c))))))),
        Forall(Implies(mem_formula_fm(0),
                       Implies(Forall_fm(0,succ(v)),
                             Forall(Implies(Equal(0,z#+2), is_d))))))))"

lemma is_formula_case_type [TC]:
     "\is_a \ formula; is_b \ formula; is_c \ formula; is_d \ formula;
         x \<in> nat; y \<in> nat\<rbrakk>
      \<Longrightarrow> formula_case_fm(is_a, is_b, is_c, is_d, x, y) \<in> formula"
by (simp add: formula_case_fm_def)

lemma sats_formula_case_fm:
  assumes is_a_iff_sats:
      "\a0 a1 a2.
        \<lbrakk>a0\<in>A; a1\<in>A; a2\<in>A\<rbrakk>
        \<Longrightarrow> ISA(a2, a1, a0) \<longleftrightarrow> sats(A, is_a, Cons(a0,Cons(a1,Cons(a2,env))))"
  and is_b_iff_sats:
      "\a0 a1 a2.
        \<lbrakk>a0\<in>A; a1\<in>A; a2\<in>A\<rbrakk>
        \<Longrightarrow> ISB(a2, a1, a0) \<longleftrightarrow> sats(A, is_b, Cons(a0,Cons(a1,Cons(a2,env))))"
  and is_c_iff_sats:
      "\a0 a1 a2.
        \<lbrakk>a0\<in>A; a1\<in>A; a2\<in>A\<rbrakk>
        \<Longrightarrow> ISC(a2, a1, a0) \<longleftrightarrow> sats(A, is_c, Cons(a0,Cons(a1,Cons(a2,env))))"
  and is_d_iff_sats:
      "\a0 a1.
        \<lbrakk>a0\<in>A; a1\<in>A\<rbrakk>
        \<Longrightarrow> ISD(a1, a0) \<longleftrightarrow> sats(A, is_d, Cons(a0,Cons(a1,env)))"
  shows
      "\x \ nat; y < length(env); env \ list(A)\
       \<Longrightarrow> sats(A, formula_case_fm(is_a,is_b,is_c,is_d,x,y), env) \<longleftrightarrow>
           is_formula_case(##A, ISA, ISB, ISC, ISD, nth(x,env), nth(y,env))"
apply (frule_tac x=y in lt_length_in_nat, assumption)
apply (simp add: formula_case_fm_def is_formula_case_def
                 is_a_iff_sats [THEN iff_sym] is_b_iff_sats [THEN iff_sym]
                 is_c_iff_sats [THEN iff_sym] is_d_iff_sats [THEN iff_sym])
done

lemma formula_case_iff_sats:
  assumes is_a_iff_sats:
      "\a0 a1 a2.
        \<lbrakk>a0\<in>A; a1\<in>A; a2\<in>A\<rbrakk>
        \<Longrightarrow> ISA(a2, a1, a0) \<longleftrightarrow> sats(A, is_a, Cons(a0,Cons(a1,Cons(a2,env))))"
  and is_b_iff_sats:
      "\a0 a1 a2.
        \<lbrakk>a0\<in>A; a1\<in>A; a2\<in>A\<rbrakk>
        \<Longrightarrow> ISB(a2, a1, a0) \<longleftrightarrow> sats(A, is_b, Cons(a0,Cons(a1,Cons(a2,env))))"
  and is_c_iff_sats:
      "\a0 a1 a2.
        \<lbrakk>a0\<in>A; a1\<in>A; a2\<in>A\<rbrakk>
        \<Longrightarrow> ISC(a2, a1, a0) \<longleftrightarrow> sats(A, is_c, Cons(a0,Cons(a1,Cons(a2,env))))"
  and is_d_iff_sats:
      "\a0 a1.
        \<lbrakk>a0\<in>A; a1\<in>A\<rbrakk>
        \<Longrightarrow> ISD(a1, a0) \<longleftrightarrow> sats(A, is_d, Cons(a0,Cons(a1,env)))"
  shows
      "\nth(i,env) = x; nth(j,env) = y;
      i \<in> nat; j < length(env); env \<in> list(A)\<rbrakk>
       \<Longrightarrow> is_formula_case(##A, ISA, ISB, ISC, ISD, x, y) \<longleftrightarrow>
           sats(A, formula_case_fm(is_a,is_b,is_c,is_d,i,j), env)"
by (simp add: sats_formula_case_fm [OF is_a_iff_sats is_b_iff_sats
                                       is_c_iff_sats is_d_iff_sats])

text\<open>The second argument of \<^term>\<open>is_a\<close> gives it direct access to \<^term>\<open>x\<close>,
  which is essential for handling free variable references.  Treatment is
  based on that of \<open>is_nat_case_reflection\<close>.\<close>
theorem is_formula_case_reflection:
  assumes is_a_reflection:
    "\h f g g'. REFLECTS[\x. is_a(L, h(x), f(x), g(x), g'(x)),
                     \<lambda>i x. is_a(##Lset(i), h(x), f(x), g(x), g'(x))]"
  and is_b_reflection:
    "\h f g g'. REFLECTS[\x. is_b(L, h(x), f(x), g(x), g'(x)),
                     \<lambda>i x. is_b(##Lset(i), h(x), f(x), g(x), g'(x))]"
  and is_c_reflection:
    "\h f g g'. REFLECTS[\x. is_c(L, h(x), f(x), g(x), g'(x)),
                     \<lambda>i x. is_c(##Lset(i), h(x), f(x), g(x), g'(x))]"
  and is_d_reflection:
    "\h f g g'. REFLECTS[\x. is_d(L, h(x), f(x), g(x)),
                     \<lambda>i x. is_d(##Lset(i), h(x), f(x), g(x))]"
  shows "REFLECTS[\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)),
               \<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))]"
apply (simp (no_asm_use) only: is_formula_case_def)
apply (intro FOL_reflections function_reflections finite_ordinal_reflection
         mem_formula_reflection
         Member_reflection Equal_reflection Nand_reflection Forall_reflection
         is_a_reflection is_b_reflection is_c_reflection is_d_reflection)
done

subsection \<open>Absoluteness for the Function \<^term>\<open>satisfies\<close>\<close>

definition
  is_depth_apply :: "[i\o,i,i,i] \ o" where
   \<comment> \<open>Merely a useful abbreviation for the sequel.\<close>
  "is_depth_apply(M,h,p,z) \
    \<exists>dp[M]. \<exists>sdp[M]. \<exists>hsdp[M].
        finite_ordinal(M,dp) \<and> is_depth(M,p,dp) \<and> successor(M,dp,sdp) \<and>
        fun_apply(M,h,sdp,hsdp) \<and> fun_apply(M,hsdp,p,z)"

lemma (in M_datatypes) is_depth_apply_abs [simp]:
     "\M(h); p \ formula; M(z)\
      \<Longrightarrow> is_depth_apply(M,h,p,z) \<longleftrightarrow> z = h ` succ(depth(p)) ` p"
by (simp add: is_depth_apply_def formula_into_M depth_type eq_commute)

text\<open>There is at present some redundancy between the relativizations in
e.g. \<open>satisfies_is_a\<close> and those in e.g. \<open>Member_replacement\<close>.\<close>

text\<open>These constants let us instantiate the parameters \<^term>\<open>a\<close>, \<^term>\<open>b\<close>,
      \<^term>\<open>c\<close>, \<^term>\<open>d\<close>, etc., of the locale \<open>Formula_Rec\<close>.\<close>
definition
  satisfies_a :: "[i,i,i]\i" where
   "satisfies_a(A) \
    \<lambda>x y. \<lambda>env \<in> list(A). bool_of_o (nth(x,env) \<in> nth(y,env))"

definition
  satisfies_is_a :: "[i\o,i,i,i,i]\o" where
   "satisfies_is_a(M,A) \
    \<lambda>x y zz. \<forall>lA[M]. is_list(M,A,lA) \<longrightarrow>
             is_lambda(M, lA,
                \<lambda>env z. is_bool_of_o(M,
                      \<exists>nx[M]. \<exists>ny[M].
                       is_nth(M,x,env,nx) \<and> is_nth(M,y,env,ny) \<and> nx \<in> ny, z),
                zz)"

definition
  satisfies_b :: "[i,i,i]\i" where
   "satisfies_b(A) \
    \<lambda>x y. \<lambda>env \<in> list(A). bool_of_o (nth(x,env) = nth(y,env))"

definition
  satisfies_is_b :: "[i\o,i,i,i,i]\o" where
   \<comment> \<open>We simplify the formula to have just \<^term>\<open>nx\<close> rather than
       introducing \<^term>\<open>ny\<close> with  \<^term>\<open>nx=ny\<close>\<close>
  "satisfies_is_b(M,A) \
    \<lambda>x y zz. \<forall>lA[M]. is_list(M,A,lA) \<longrightarrow>
             is_lambda(M, lA,
                \<lambda>env z. is_bool_of_o(M,
                      \<exists>nx[M]. is_nth(M,x,env,nx) \<and> is_nth(M,y,env,nx), z),
                zz)"

definition
  satisfies_c :: "[i,i,i,i,i]\i" where
   "satisfies_c(A) \ \p q rp rq. \env \ list(A). not(rp ` env and rq ` env)"

definition
  satisfies_is_c :: "[i\o,i,i,i,i,i]\o" where
   "satisfies_is_c(M,A,h) \
    \<lambda>p q zz. \<forall>lA[M]. is_list(M,A,lA) \<longrightarrow>
             is_lambda(M, lA, \<lambda>env z. \<exists>hp[M]. \<exists>hq[M].
                 (\<exists>rp[M]. is_depth_apply(M,h,p,rp) \<and> fun_apply(M,rp,env,hp)) \<and>
                 (\<exists>rq[M]. is_depth_apply(M,h,q,rq) \<and> fun_apply(M,rq,env,hq)) \<and>
                 (\<exists>pq[M]. is_and(M,hp,hq,pq) \<and> is_not(M,pq,z)),
                zz)"

definition
  satisfies_d :: "[i,i,i]\i" where
   "satisfies_d(A)
    \<equiv> \<lambda>p rp. \<lambda>env \<in> list(A). bool_of_o (\<forall>x\<in>A. rp ` (Cons(x,env)) = 1)"

definition
  satisfies_is_d :: "[i\o,i,i,i,i]\o" where
   "satisfies_is_d(M,A,h) \
    \<lambda>p zz. \<forall>lA[M]. is_list(M,A,lA) \<longrightarrow>
             is_lambda(M, lA,
                \<lambda>env z. \<exists>rp[M]. is_depth_apply(M,h,p,rp) \<and>
                    is_bool_of_o(M,
                           \<forall>x[M]. \<forall>xenv[M]. \<forall>hp[M].
                              x\<in>A \<longrightarrow> is_Cons(M,x,env,xenv) \<longrightarrow>
                              fun_apply(M,rp,xenv,hp) \<longrightarrow> number1(M,hp),
                  z),
               zz)"

definition
  satisfies_MH :: "[i\o,i,i,i,i]\o" where
    \<comment> \<open>The variable \<^term>\<open>u\<close> is unused, but gives \<^term>\<open>satisfies_MH\<close>
        the correct arity.\<close>
  "satisfies_MH \
    \<lambda>M A u f z.
         \<forall>fml[M]. is_formula(M,fml) \<longrightarrow>
             is_lambda (M, fml,
               is_formula_case (M, satisfies_is_a(M,A),
                                satisfies_is_b(M,A),
                                satisfies_is_c(M,A,f), satisfies_is_d(M,A,f)),
               z)"

definition
  is_satisfies :: "[i\o,i,i,i]\o" where
  "is_satisfies(M,A) \ is_formula_rec (M, satisfies_MH(M,A))"

text\<open>This lemma relates the fragments defined above to the original primitive
      recursion in \<^term>\<open>satisfies\<close>.
      Induction is not required: the definitions are directly equal!\<close>
lemma satisfies_eq:
  "satisfies(A,p) =
   formula_rec (satisfies_a(A), satisfies_b(A),
                satisfies_c(A), satisfies_d(A), p)"
by (simp add: satisfies_formula_def satisfies_a_def satisfies_b_def
              satisfies_c_def satisfies_d_def)

text\<open>Further constraints on the class \<^term>\<open>M\<close> in order to prove
      absoluteness for the constants defined above.  The ultimate goal
      is the absoluteness of the function \<^term>\<open>satisfies\<close>.\<close>
locale M_satisfies = M_eclose +
assumes
   Member_replacement:
    "\M(A); x \ nat; y \ nat\
     \<Longrightarrow> strong_replacement
         (M, \<lambda>env z. \<exists>bo[M]. \<exists>nx[M]. \<exists>ny[M].
              env \<in> list(A) \<and> is_nth(M,x,env,nx) \<and> is_nth(M,y,env,ny) \<and>
              is_bool_of_o(M, nx \<in> ny, bo) \<and>
              pair(M, env, bo, z))"
and
   Equal_replacement:
    "\M(A); x \ nat; y \ nat\
     \<Longrightarrow> strong_replacement
         (M, \<lambda>env z. \<exists>bo[M]. \<exists>nx[M]. \<exists>ny[M].
              env \<in> list(A) \<and> is_nth(M,x,env,nx) \<and> is_nth(M,y,env,ny) \<and>
              is_bool_of_o(M, nx = ny, bo) \<and>
              pair(M, env, bo, z))"
and
   Nand_replacement:
    "\M(A); M(rp); M(rq)\
     \<Longrightarrow> strong_replacement
         (M, \<lambda>env z. \<exists>rpe[M]. \<exists>rqe[M]. \<exists>andpq[M]. \<exists>notpq[M].
               fun_apply(M,rp,env,rpe) \<and> fun_apply(M,rq,env,rqe) \<and>
               is_and(M,rpe,rqe,andpq) \<and> is_not(M,andpq,notpq) \<and>
               env \<in> list(A) \<and> pair(M, env, notpq, z))"
and
  Forall_replacement:
   "\M(A); M(rp)\
    \<Longrightarrow> strong_replacement
        (M, \<lambda>env z. \<exists>bo[M].
              env \<in> list(A) \<and>
              is_bool_of_o (M,
                            \<forall>a[M]. \<forall>co[M]. \<forall>rpco[M].
                               a\<in>A \<longrightarrow> is_Cons(M,a,env,co) \<longrightarrow>
                               fun_apply(M,rp,co,rpco) \<longrightarrow> number1(M, rpco),
                            bo) \<and>
              pair(M,env,bo,z))"
and
  formula_rec_replacement:
      \<comment> \<open>For the \<^term>\<open>transrec\<close>\<close>
   "\n \ nat; M(A)\ \ transrec_replacement(M, satisfies_MH(M,A), n)"
and
  formula_rec_lambda_replacement:
      \<comment> \<open>For the \<open>\<lambda>-abstraction\<close> in the \<^term>\<open>transrec\<close> body\<close>
   "\M(g); M(A)\ \
    strong_replacement (M,
       \<lambda>x y. mem_formula(M,x) \<and>
             (\<exists>c[M]. is_formula_case(M, satisfies_is_a(M,A),
                                  satisfies_is_b(M,A),
                                  satisfies_is_c(M,A,g),
                                  satisfies_is_d(M,A,g), x, c) \<and>
             pair(M, x, c, y)))"

lemma (in M_satisfies) Member_replacement':
    "\M(A); x \ nat; y \ nat\
     \<Longrightarrow> strong_replacement
         (M, \<lambda>env z. env \<in> list(A) \<and>
                     z = \<langle>env, bool_of_o(nth(x, env) \<in> nth(y, env))\<rangle>)"
by (insert Member_replacement, simp)

lemma (in M_satisfies) Equal_replacement':
    "\M(A); x \ nat; y \ nat\
     \<Longrightarrow> strong_replacement
         (M, \<lambda>env z. env \<in> list(A) \<and>
                     z = \<langle>env, bool_of_o(nth(x, env) = nth(y, env))\<rangle>)"
by (insert Equal_replacement, simp)

lemma (in M_satisfies) Nand_replacement':
    "\M(A); M(rp); M(rq)\
     \<Longrightarrow> strong_replacement
         (M, \<lambda>env z. env \<in> list(A) \<and> z = \<langle>env, not(rp`env and rq`env)\<rangle>)"
by (insert Nand_replacement, simp)

lemma (in M_satisfies) Forall_replacement':
   "\M(A); M(rp)\
    \<Longrightarrow> strong_replacement
        (M, \<lambda>env z.
               env \<in> list(A) \<and>
               z = \<langle>env, bool_of_o (\<forall>a\<in>A. rp ` Cons(a,env) = 1)\<rangle>)"
by (insert Forall_replacement, simp)

lemma (in M_satisfies) a_closed:
     "\M(A); x\nat; y\nat\ \ M(satisfies_a(A,x,y))"
apply (simp add: satisfies_a_def)
apply (blast intro: lam_closed2 Member_replacement')
done

lemma (in M_satisfies) a_rel:
     "M(A) \ Relation2(M, nat, nat, satisfies_is_a(M,A), satisfies_a(A))"
apply (simp add: Relation2_def satisfies_is_a_def satisfies_a_def)
apply (auto del: iffI intro!: lambda_abs2 simp add: Relation1_def)
done

lemma (in M_satisfies) b_closed:
     "\M(A); x\nat; y\nat\ \ M(satisfies_b(A,x,y))"
apply (simp add: satisfies_b_def)
apply (blast intro: lam_closed2 Equal_replacement')
done

lemma (in M_satisfies) b_rel:
     "M(A) \ Relation2(M, nat, nat, satisfies_is_b(M,A), satisfies_b(A))"
apply (simp add: Relation2_def satisfies_is_b_def satisfies_b_def)
apply (auto del: iffI intro!: lambda_abs2 simp add: Relation1_def)
done

lemma (in M_satisfies) c_closed:
     "\M(A); x \ formula; y \ formula; M(rx); M(ry)\
      \<Longrightarrow> M(satisfies_c(A,x,y,rx,ry))"
apply (simp add: satisfies_c_def)
apply (rule lam_closed2)
apply (rule Nand_replacement')
apply (simp_all add: formula_into_M list_into_M [of _ A])
done

lemma (in M_satisfies) c_rel:
"\M(A); M(f)\ \
  Relation2 (M, formula, formula,
               satisfies_is_c(M,A,f),
               \<lambda>u v. satisfies_c(A, u, v, f ` succ(depth(u)) ` u,
                                          f ` succ(depth(v)) ` v))"
apply (simp add: Relation2_def satisfies_is_c_def satisfies_c_def)
apply (auto del: iffI intro!: lambda_abs2
            simp add: Relation1_def formula_into_M)
done

lemma (in M_satisfies) d_closed:
     "\M(A); x \ formula; M(rx)\ \ M(satisfies_d(A,x,rx))"
apply (simp add: satisfies_d_def)
apply (rule lam_closed2)
apply (rule Forall_replacement')
apply (simp_all add: formula_into_M list_into_M [of _ A])
done

lemma (in M_satisfies) d_rel:
"\M(A); M(f)\ \
  Relation1(M, formula, satisfies_is_d(M,A,f),
     \<lambda>u. satisfies_d(A, u, f ` succ(depth(u)) ` u))"
apply (simp del: rall_abs
            add: Relation1_def satisfies_is_d_def satisfies_d_def)
apply (auto del: iffI intro!: lambda_abs2 simp add: Relation1_def)
done

lemma (in M_satisfies) fr_replace:
      "\n \ nat; M(A)\ \ transrec_replacement(M,satisfies_MH(M,A),n)"
by (blast intro: formula_rec_replacement)

lemma (in M_satisfies) formula_case_satisfies_closed:
"\M(g); M(A); x \ formula\ \
  M(formula_case (satisfies_a(A), satisfies_b(A),
       \<lambda>u v. satisfies_c(A, u, v,
                         g ` succ(depth(u)) ` u, g ` succ(depth(v)) ` v),
       \<lambda>u. satisfies_d (A, u, g ` succ(depth(u)) ` u),
       x))"
by (blast intro: a_closed b_closed c_closed d_closed)

lemma (in M_satisfies) fr_lam_replace:
   "\M(g); M(A)\ \
    strong_replacement (M, \<lambda>x y. x \<in> formula \<and>
            y = \<langle>x,
                 formula_rec_case(satisfies_a(A),
                                  satisfies_b(A),
                                  satisfies_c(A),
                                  satisfies_d(A), g, x)\<rangle>)"
apply (insert formula_rec_lambda_replacement)
apply (simp add: formula_rec_case_def formula_case_satisfies_closed
                 formula_case_abs [OF a_rel b_rel c_rel d_rel])
done

text\<open>Instantiate locale \<open>Formula_Rec\<close> for the
      Function \<^term>\<open>satisfies\<close>\<close>

lemma (in M_satisfies) Formula_Rec_axioms_M:
   "M(A) \
    Formula_Rec_axioms(M, satisfies_a(A), satisfies_is_a(M,A),
                          satisfies_b(A), satisfies_is_b(M,A),
                          satisfies_c(A), satisfies_is_c(M,A),
                          satisfies_d(A), satisfies_is_d(M,A))"
apply (rule Formula_Rec_axioms.intro)
apply (assumption |
       rule a_closed a_rel b_closed b_rel c_closed c_rel d_closed d_rel
       fr_replace [unfolded satisfies_MH_def]
       fr_lam_replace) +
done

theorem (in M_satisfies) Formula_Rec_M:
    "M(A) \
     Formula_Rec(M, satisfies_a(A), satisfies_is_a(M,A),
                         satisfies_b(A), satisfies_is_b(M,A),
                         satisfies_c(A), satisfies_is_c(M,A),
                         satisfies_d(A), satisfies_is_d(M,A))"
  apply (rule Formula_Rec.intro)
   apply (rule M_satisfies.axioms, rule M_satisfies_axioms)
  apply (erule Formula_Rec_axioms_M)
  done

lemmas (in M_satisfies)
    satisfies_closed' = Formula_Rec.formula_rec_closed [OF Formula_Rec_M]
and satisfies_abs' = Formula_Rec.formula_rec_abs [OF Formula_Rec_M]

lemma (in M_satisfies) satisfies_closed:
  "\M(A); p \ formula\ \ M(satisfies(A,p))"
by (simp add: Formula_Rec.formula_rec_closed [OF Formula_Rec_M]
              satisfies_eq)

lemma (in M_satisfies) satisfies_abs:
  "\M(A); M(z); p \ formula\
   \<Longrightarrow> is_satisfies(M,A,p,z) \<longleftrightarrow> z = satisfies(A,p)"
by (simp only: Formula_Rec.formula_rec_abs [OF Formula_Rec_M]
               satisfies_eq is_satisfies_def satisfies_MH_def)

subsection\<open>Internalizations Needed to Instantiate \<open>M_satisfies\<close>\<close>

subsubsection\<open>The Operator \<^term>\<open>is_depth_apply\<close>, Internalized\<close>

(* is_depth_apply(M,h,p,z) \<equiv>
    \<exists>dp[M]. \<exists>sdp[M]. \<exists>hsdp[M].
      2        1         0
        finite_ordinal(M,dp) \<and> is_depth(M,p,dp) \<and> successor(M,dp,sdp) \<and>
        fun_apply(M,h,sdp,hsdp) \<and> fun_apply(M,hsdp,p,z) *)
definition
  depth_apply_fm :: "[i,i,i]\i" where
    "depth_apply_fm(h,p,z) \
       Exists(Exists(Exists(
        And(finite_ordinal_fm(2),
         And(depth_fm(p#+3,2),
          And(succ_fm(2,1),
           And(fun_apply_fm(h#+3,1,0), fun_apply_fm(0,p#+3,z#+3))))))))"

lemma depth_apply_type [TC]:
     "\x \ nat; y \ nat; z \ nat\ \ depth_apply_fm(x,y,z) \ formula"
by (simp add: depth_apply_fm_def)

lemma sats_depth_apply_fm [simp]:
   "\x \ nat; y \ nat; z \ nat; env \ list(A)\
    \<Longrightarrow> sats(A, depth_apply_fm(x,y,z), env) \<longleftrightarrow>
        is_depth_apply(##A, nth(x,env), nth(y,env), nth(z,env))"
by (simp add: depth_apply_fm_def is_depth_apply_def)

lemma depth_apply_iff_sats:
    "\nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
        i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)\<rbrakk>
     \<Longrightarrow> is_depth_apply(##A, x, y, z) \<longleftrightarrow> sats(A, depth_apply_fm(i,j,k), env)"
by simp

lemma depth_apply_reflection:
     "REFLECTS[\x. is_depth_apply(L,f(x),g(x),h(x)),
               \<lambda>i x. is_depth_apply(##Lset(i),f(x),g(x),h(x))]"
apply (simp only: is_depth_apply_def)
apply (intro FOL_reflections function_reflections depth_reflection
             finite_ordinal_reflection)
done

subsubsection\<open>The Operator \<^term>\<open>satisfies_is_a\<close>, Internalized\<close>

(* satisfies_is_a(M,A) \<equiv>
    \<lambda>x y zz. \<forall>lA[M]. is_list(M,A,lA) \<longrightarrow>
             is_lambda(M, lA,
                \<lambda>env z. is_bool_of_o(M,
                      \<exists>nx[M]. \<exists>ny[M].
                       is_nth(M,x,env,nx) \<and> is_nth(M,y,env,ny) \<and> nx \<in> ny, z),
                zz)  *)

definition
  satisfies_is_a_fm :: "[i,i,i,i]\i" where
  "satisfies_is_a_fm(A,x,y,z) \
   Forall(
     Implies(is_list_fm(succ(A),0),
       lambda_fm(
         bool_of_o_fm(Exists(
                       Exists(And(nth_fm(x#+6,3,1),
                               And(nth_fm(y#+6,3,0),
                                   Member(1,0))))), 0),
         0, succ(z))))"

lemma satisfies_is_a_type [TC]:
     "\A \ nat; x \ nat; y \ nat; z \ nat\
      \<Longrightarrow> satisfies_is_a_fm(A,x,y,z) \<in> formula"
by (simp add: satisfies_is_a_fm_def)

lemma sats_satisfies_is_a_fm [simp]:
   "\u \ nat; x < length(env); y < length(env); z \ nat; env \ list(A)\
    \<Longrightarrow> sats(A, satisfies_is_a_fm(u,x,y,z), env) \<longleftrightarrow>
        satisfies_is_a(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
apply (frule_tac x=x in lt_length_in_nat, assumption)
apply (frule_tac x=y in lt_length_in_nat, assumption)
apply (simp add: satisfies_is_a_fm_def satisfies_is_a_def sats_lambda_fm
                 sats_bool_of_o_fm)
done

lemma satisfies_is_a_iff_sats:
  "\nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
      u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)\<rbrakk>
   \<Longrightarrow> satisfies_is_a(##A,nu,nx,ny,nz) \<longleftrightarrow>
       sats(A, satisfies_is_a_fm(u,x,y,z), env)"
by simp

theorem satisfies_is_a_reflection:
     "REFLECTS[\x. satisfies_is_a(L,f(x),g(x),h(x),g'(x)),
               \<lambda>i x. satisfies_is_a(##Lset(i),f(x),g(x),h(x),g'(x))]"
  unfolding satisfies_is_a_def
apply (intro FOL_reflections is_lambda_reflection bool_of_o_reflection
             nth_reflection is_list_reflection)
done

subsubsection\<open>The Operator \<^term>\<open>satisfies_is_b\<close>, Internalized\<close>

(* satisfies_is_b(M,A) \<equiv>
    \<lambda>x y zz. \<forall>lA[M]. is_list(M,A,lA) \<longrightarrow>
             is_lambda(M, lA,
                \<lambda>env z. is_bool_of_o(M,
                      \<exists>nx[M]. is_nth(M,x,env,nx) \<and> is_nth(M,y,env,nx), z),
                zz) *)

definition
  satisfies_is_b_fm :: "[i,i,i,i]\i" where
"satisfies_is_b_fm(A,x,y,z) \
   Forall(
     Implies(is_list_fm(succ(A),0),
       lambda_fm(
         bool_of_o_fm(Exists(And(nth_fm(x#+5,2,0), nth_fm(y#+5,2,0))), 0),
         0, succ(z))))"

lemma satisfies_is_b_type [TC]:
     "\A \ nat; x \ nat; y \ nat; z \ nat\
      \<Longrightarrow> satisfies_is_b_fm(A,x,y,z) \<in> formula"
by (simp add: satisfies_is_b_fm_def)

lemma sats_satisfies_is_b_fm [simp]:
   "\u \ nat; x < length(env); y < length(env); z \ nat; env \ list(A)\
    \<Longrightarrow> sats(A, satisfies_is_b_fm(u,x,y,z), env) \<longleftrightarrow>
        satisfies_is_b(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
apply (frule_tac x=x in lt_length_in_nat, assumption)
apply (frule_tac x=y in lt_length_in_nat, assumption)
apply (simp add: satisfies_is_b_fm_def satisfies_is_b_def sats_lambda_fm
                 sats_bool_of_o_fm)
done

lemma satisfies_is_b_iff_sats:
  "\nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
      u \<in> nat; x < length(env); y < length(env); z \<in> nat; env \<in> list(A)\<rbrakk>
   \<Longrightarrow> satisfies_is_b(##A,nu,nx,ny,nz) \<longleftrightarrow>
       sats(A, satisfies_is_b_fm(u,x,y,z), env)"
by simp

theorem satisfies_is_b_reflection:
     "REFLECTS[\x. satisfies_is_b(L,f(x),g(x),h(x),g'(x)),
               \<lambda>i x. satisfies_is_b(##Lset(i),f(x),g(x),h(x),g'(x))]"
  unfolding satisfies_is_b_def
apply (intro FOL_reflections is_lambda_reflection bool_of_o_reflection
             nth_reflection is_list_reflection)
done

subsubsection\<open>The Operator \<^term>\<open>satisfies_is_c\<close>, Internalized\<close>

(* satisfies_is_c(M,A,h) \<equiv>
    \<lambda>p q zz. \<forall>lA[M]. is_list(M,A,lA) \<longrightarrow>
             is_lambda(M, lA, \<lambda>env z. \<exists>hp[M]. \<exists>hq[M].
                 (\<exists>rp[M]. is_depth_apply(M,h,p,rp) \<and> fun_apply(M,rp,env,hp)) \<and>
                 (\<exists>rq[M]. is_depth_apply(M,h,q,rq) \<and> fun_apply(M,rq,env,hq)) \<and>
                 (\<exists>pq[M]. is_and(M,hp,hq,pq) \<and> is_not(M,pq,z)),
                zz) *)

definition
  satisfies_is_c_fm :: "[i,i,i,i,i]\i" where
"satisfies_is_c_fm(A,h,p,q,zz) \
   Forall(
     Implies(is_list_fm(succ(A),0),
       lambda_fm(
         Exists(Exists(
          And(Exists(And(depth_apply_fm(h#+7,p#+7,0), fun_apply_fm(0,4,2))),
          And(Exists(And(depth_apply_fm(h#+7,q#+7,0), fun_apply_fm(0,4,1))),
              Exists(And(and_fm(2,1,0), not_fm(0,3))))))),
         0, succ(zz))))"

lemma satisfies_is_c_type [TC]:
     "\A \ nat; h \ nat; x \ nat; y \ nat; z \ nat\
      \<Longrightarrow> satisfies_is_c_fm(A,h,x,y,z) \<in> formula"
by (simp add: satisfies_is_c_fm_def)

lemma sats_satisfies_is_c_fm [simp]:
   "\u \ nat; v \ nat; x \ nat; y \ nat; z \ nat; env \ list(A)\
    \<Longrightarrow> sats(A, satisfies_is_c_fm(u,v,x,y,z), env) \<longleftrightarrow>
        satisfies_is_c(##A, nth(u,env), nth(v,env), nth(x,env),
                            nth(y,env), nth(z,env))"
by (simp add: satisfies_is_c_fm_def satisfies_is_c_def sats_lambda_fm)

lemma satisfies_is_c_iff_sats:
  "\nth(u,env) = nu; nth(v,env) = nv; nth(x,env) = nx; nth(y,env) = ny;
      nth(z,env) = nz;
      u \<in> nat; v \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)\<rbrakk>
   \<Longrightarrow> satisfies_is_c(##A,nu,nv,nx,ny,nz) \<longleftrightarrow>
       sats(A, satisfies_is_c_fm(u,v,x,y,z), env)"
by simp

theorem satisfies_is_c_reflection:
     "REFLECTS[\x. satisfies_is_c(L,f(x),g(x),h(x),g'(x),h'(x)),
               \<lambda>i x. satisfies_is_c(##Lset(i),f(x),g(x),h(x),g'(x),h'(x))]"
  unfolding satisfies_is_c_def
apply (intro FOL_reflections function_reflections is_lambda_reflection
             extra_reflections nth_reflection depth_apply_reflection
             is_list_reflection)
done

subsubsection\<open>The Operator \<^term>\<open>satisfies_is_d\<close>, Internalized\<close>

(* satisfies_is_d(M,A,h) \<equiv>
    \<lambda>p zz. \<forall>lA[M]. is_list(M,A,lA) \<longrightarrow>
             is_lambda(M, lA,
                \<lambda>env z. \<exists>rp[M]. is_depth_apply(M,h,p,rp) \<and>
                    is_bool_of_o(M,
                           \<forall>x[M]. \<forall>xenv[M]. \<forall>hp[M].
                              x\<in>A \<longrightarrow> is_Cons(M,x,env,xenv) \<longrightarrow>
                              fun_apply(M,rp,xenv,hp) \<longrightarrow> number1(M,hp),
                  z),
               zz) *)

definition
  satisfies_is_d_fm :: "[i,i,i,i]\i" where
"satisfies_is_d_fm(A,h,p,zz) \
   Forall(
     Implies(is_list_fm(succ(A),0),
       lambda_fm(
         Exists(
           And(depth_apply_fm(h#+5,p#+5,0),
               bool_of_o_fm(
                Forall(Forall(Forall(
                 Implies(Member(2,A#+8),
                  Implies(Cons_fm(2,5,1),
                   Implies(fun_apply_fm(3,1,0), number1_fm(0))))))), 1))),
         0, succ(zz))))"

lemma satisfies_is_d_type [TC]:
     "\A \ nat; h \ nat; x \ nat; z \ nat\
      \<Longrightarrow> satisfies_is_d_fm(A,h,x,z) \<in> formula"
by (simp add: satisfies_is_d_fm_def)

lemma sats_satisfies_is_d_fm [simp]:
   "\u \ nat; x \ nat; y \ nat; z \ nat; env \ list(A)\
    \<Longrightarrow> sats(A, satisfies_is_d_fm(u,x,y,z), env) \<longleftrightarrow>
        satisfies_is_d(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
by (simp add: satisfies_is_d_fm_def satisfies_is_d_def sats_lambda_fm
              sats_bool_of_o_fm)

lemma satisfies_is_d_iff_sats:
  "\nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
      u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)\<rbrakk>
   \<Longrightarrow> satisfies_is_d(##A,nu,nx,ny,nz) \<longleftrightarrow>
       sats(A, satisfies_is_d_fm(u,x,y,z), env)"
by simp

theorem satisfies_is_d_reflection:
     "REFLECTS[\x. satisfies_is_d(L,f(x),g(x),h(x),g'(x)),
               \<lambda>i x. satisfies_is_d(##Lset(i),f(x),g(x),h(x),g'(x))]"
  unfolding satisfies_is_d_def
apply (intro FOL_reflections function_reflections is_lambda_reflection
             extra_reflections nth_reflection depth_apply_reflection
             is_list_reflection)
done

subsubsection\<open>The Operator \<^term>\<open>satisfies_MH\<close>, Internalized\<close>

(* satisfies_MH \<equiv>
    \<lambda>M A u f zz.
         \<forall>fml[M]. is_formula(M,fml) \<longrightarrow>
             is_lambda (M, fml,
               is_formula_case (M, satisfies_is_a(M,A),
                                satisfies_is_b(M,A),
                                satisfies_is_c(M,A,f), satisfies_is_d(M,A,f)),
               zz) *)

definition
  satisfies_MH_fm :: "[i,i,i,i]\i" where
"satisfies_MH_fm(A,u,f,zz) \
   Forall(
     Implies(is_formula_fm(0),
       lambda_fm(
         formula_case_fm(satisfies_is_a_fm(A#+7,2,1,0),
                         satisfies_is_b_fm(A#+7,2,1,0),
                         satisfies_is_c_fm(A#+7,f#+7,2,1,0),
                         satisfies_is_d_fm(A#+6,f#+6,1,0),
                         1, 0),
         0, succ(zz))))"

lemma satisfies_MH_type [TC]:
     "\A \ nat; u \ nat; x \ nat; z \ nat\
      \<Longrightarrow> satisfies_MH_fm(A,u,x,z) \<in> formula"
by (simp add: satisfies_MH_fm_def)

lemma sats_satisfies_MH_fm [simp]:
   "\u \ nat; x \ nat; y \ nat; z \ nat; env \ list(A)\
    \<Longrightarrow> sats(A, satisfies_MH_fm(u,x,y,z), env) \<longleftrightarrow>
        satisfies_MH(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
by (simp add: satisfies_MH_fm_def satisfies_MH_def sats_lambda_fm
              sats_formula_case_fm)

lemma satisfies_MH_iff_sats:
  "\nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
      u \<in> nat; x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)\<rbrakk>
   \<Longrightarrow> satisfies_MH(##A,nu,nx,ny,nz) \<longleftrightarrow>
       sats(A, satisfies_MH_fm(u,x,y,z), env)"
by simp

lemmas satisfies_reflections =
       is_lambda_reflection is_formula_reflection
       is_formula_case_reflection
       satisfies_is_a_reflection satisfies_is_b_reflection
       satisfies_is_c_reflection satisfies_is_d_reflection

theorem satisfies_MH_reflection:
     "REFLECTS[\x. satisfies_MH(L,f(x),g(x),h(x),g'(x)),
               \<lambda>i x. satisfies_MH(##Lset(i),f(x),g(x),h(x),g'(x))]"
  unfolding satisfies_MH_def
apply (intro FOL_reflections satisfies_reflections)
done

subsection\<open>Lemmas for Instantiating the Locale \<open>M_satisfies\<close>\<close>

subsubsection\<open>The \<^term>\<open>Member\<close> Case\<close>

lemma Member_Reflects:
"REFLECTS[\u. \v[L]. v \ B \ (\bo[L]. \nx[L]. \ny[L].
          v \<in> lstA \<and> is_nth(L,x,v,nx) \<and> is_nth(L,y,v,ny) \<and>
          is_bool_of_o(L, nx \<in> ny, bo) \<and> pair(L,v,bo,u)),
   \<lambda>i u. \<exists>v \<in> Lset(i). v \<in> B \<and> (\<exists>bo \<in> Lset(i). \<exists>nx \<in> Lset(i). \<exists>ny \<in> Lset(i).
             v \<in> lstA \<and> is_nth(##Lset(i), x, v, nx) \<and>
             is_nth(##Lset(i), y, v, ny) \<and>
          is_bool_of_o(##Lset(i), nx \<in> ny, bo) \<and> pair(##Lset(i), v, bo, u))]"
by (intro FOL_reflections function_reflections nth_reflection
          bool_of_o_reflection)

lemma Member_replacement:
    "\L(A); x \ nat; y \ nat\
     \<Longrightarrow> strong_replacement
         (L, \<lambda>env z. \<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L].
              env \<in> list(A) \<and> is_nth(L,x,env,nx) \<and> is_nth(L,y,env,ny) \<and>
              is_bool_of_o(L, nx \<in> ny, bo) \<and>
              pair(L, env, bo, z))"
apply (rule strong_replacementI)
apply (rule_tac u="{list(A),B,x,y}"
         in gen_separation_multi [OF Member_Reflects],
       auto)
apply (rule_tac env="[list(A),B,x,y]" in DPow_LsetI)
apply (rule sep_rules nth_iff_sats is_bool_of_o_iff_sats | simp)+
done

subsubsection\<open>The \<^term>\<open>Equal\<close> Case\<close>

lemma Equal_Reflects:
"REFLECTS[\u. \v[L]. v \ B \ (\bo[L]. \nx[L]. \ny[L].
          v \<in> lstA \<and> is_nth(L, x, v, nx) \<and> is_nth(L, y, v, ny) \<and>
          is_bool_of_o(L, nx = ny, bo) \<and> pair(L, v, bo, u)),
   \<lambda>i u. \<exists>v \<in> Lset(i). v \<in> B \<and> (\<exists>bo \<in> Lset(i). \<exists>nx \<in> Lset(i). \<exists>ny \<in> Lset(i).
             v \<in> lstA \<and> is_nth(##Lset(i), x, v, nx) \<and>
             is_nth(##Lset(i), y, v, ny) \<and>
          is_bool_of_o(##Lset(i), nx = ny, bo) \<and> pair(##Lset(i), v, bo, u))]"
by (intro FOL_reflections function_reflections nth_reflection
          bool_of_o_reflection)

lemma Equal_replacement:
    "\L(A); x \ nat; y \ nat\
     \<Longrightarrow> strong_replacement
         (L, \<lambda>env z. \<exists>bo[L]. \<exists>nx[L]. \<exists>ny[L].
              env \<in> list(A) \<and> is_nth(L,x,env,nx) \<and> is_nth(L,y,env,ny) \<and>
              is_bool_of_o(L, nx = ny, bo) \<and>
              pair(L, env, bo, z))"
apply (rule strong_replacementI)
apply (rule_tac u="{list(A),B,x,y}"
         in gen_separation_multi [OF Equal_Reflects],
       auto)
apply (rule_tac env="[list(A),B,x,y]" in DPow_LsetI)
apply (rule sep_rules nth_iff_sats is_bool_of_o_iff_sats | simp)+
done

subsubsection\<open>The \<^term>\<open>Nand\<close> Case\<close>

lemma Nand_Reflects:
    "REFLECTS [\x. \u[L]. u \ B \
               (\<exists>rpe[L]. \<exists>rqe[L]. \<exists>andpq[L]. \<exists>notpq[L].
                 fun_apply(L, rp, u, rpe) \<and> fun_apply(L, rq, u, rqe) \<and>
                 is_and(L, rpe, rqe, andpq) \<and> is_not(L, andpq, notpq) \<and>
                 u \<in> list(A) \<and> pair(L, u, notpq, x)),
    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and>
     (\<exists>rpe \<in> Lset(i). \<exists>rqe \<in> Lset(i). \<exists>andpq \<in> Lset(i). \<exists>notpq \<in> Lset(i).
       fun_apply(##Lset(i), rp, u, rpe) \<and> fun_apply(##Lset(i), rq, u, rqe) \<and>
       is_and(##Lset(i), rpe, rqe, andpq) \<and> is_not(##Lset(i), andpq, notpq) \<and>
       u \<in> list(A) \<and> pair(##Lset(i), u, notpq, x))]"
  unfolding is_and_def is_not_def
apply (intro FOL_reflections function_reflections)
done

lemma Nand_replacement:
    "\L(A); L(rp); L(rq)\
     \<Longrightarrow> strong_replacement
         (L, \<lambda>env z. \<exists>rpe[L]. \<exists>rqe[L]. \<exists>andpq[L]. \<exists>notpq[L].
               fun_apply(L,rp,env,rpe) \<and> fun_apply(L,rq,env,rqe) \<and>
               is_and(L,rpe,rqe,andpq) \<and> is_not(L,andpq,notpq) \<and>
               env \<in> list(A) \<and> pair(L, env, notpq, z))"
apply (rule strong_replacementI)
apply (rule_tac u="{list(A),B,rp,rq}"
         in gen_separation_multi [OF Nand_Reflects],
       auto)
apply (rule_tac env="[list(A),B,rp,rq]" in DPow_LsetI)
apply (rule sep_rules is_and_iff_sats is_not_iff_sats | simp)+
done

subsubsection\<open>The \<^term>\<open>Forall\<close> Case\<close>

lemma Forall_Reflects:
"REFLECTS [\x. \u[L]. u \ B \ (\bo[L]. u \ list(A) \
                 is_bool_of_o (L,
     \<forall>a[L]. \<forall>co[L]. \<forall>rpco[L]. a \<in> A \<longrightarrow>
                is_Cons(L,a,u,co) \<longrightarrow> fun_apply(L,rp,co,rpco) \<longrightarrow>
                number1(L,rpco),
                           bo) \<and> pair(L,u,bo,x)),
\<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>bo \<in> Lset(i). u \<in> list(A) \<and>
        is_bool_of_o (##Lset(i),
\<forall>a \<in> Lset(i). \<forall>co \<in> Lset(i). \<forall>rpco \<in> Lset(i). a \<in> A \<longrightarrow>
            is_Cons(##Lset(i),a,u,co) \<longrightarrow> fun_apply(##Lset(i),rp,co,rpco) \<longrightarrow>
            number1(##Lset(i),rpco),
                       bo) \<and> pair(##Lset(i),u,bo,x))]"
  unfolding is_bool_of_o_def
apply (intro FOL_reflections function_reflections Cons_reflection)
done

lemma Forall_replacement:
   "\L(A); L(rp)\
    \<Longrightarrow> strong_replacement
        (L, \<lambda>env z. \<exists>bo[L].
              env \<in> list(A) \<and>
              is_bool_of_o (L,
                            \<forall>a[L]. \<forall>co[L]. \<forall>rpco[L].
                               a\<in>A \<longrightarrow> is_Cons(L,a,env,co) \<longrightarrow>
                               fun_apply(L,rp,co,rpco) \<longrightarrow> number1(L, rpco),
                            bo) \<and>
              pair(L,env,bo,z))"
apply (rule strong_replacementI)
apply (rule_tac u="{A,list(A),B,rp}"
         in gen_separation_multi [OF Forall_Reflects],
       auto)
apply (rule_tac env="[A,list(A),B,rp]" in DPow_LsetI)
apply (rule sep_rules is_bool_of_o_iff_sats Cons_iff_sats | simp)+
done

subsubsection\<open>The \<^term>\<open>transrec_replacement\<close> Case\<close>

lemma formula_rec_replacement_Reflects:
"REFLECTS [\x. \u[L]. u \ B \ (\y[L]. pair(L, u, y, x) \
             is_wfrec (L, satisfies_MH(L,A), mesa, u, y)),
    \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> (\<exists>y \<in> Lset(i). pair(##Lset(i), u, y, x) \<and>
             is_wfrec (##Lset(i), satisfies_MH(##Lset(i),A), mesa, u, y))]"
by (intro FOL_reflections function_reflections satisfies_MH_reflection
          is_wfrec_reflection)

lemma formula_rec_replacement:
      \<comment> \<open>For the \<^term>\<open>transrec\<close>\<close>
   "\n \ nat; L(A)\ \ transrec_replacement(L, satisfies_MH(L,A), n)"
apply (rule L.transrec_replacementI, simp add: L.nat_into_M)
apply (rule strong_replacementI)
apply (rule_tac u="{B,A,n,Memrel(eclose({n}))}"
         in gen_separation_multi [OF formula_rec_replacement_Reflects],
       auto simp add: L.nat_into_M)
apply (rule_tac env="[B,A,n,Memrel(eclose({n}))]" in DPow_LsetI)
apply (rule sep_rules satisfies_MH_iff_sats is_wfrec_iff_sats | simp)+
done

subsubsection\<open>The Lambda Replacement Case\<close>

lemma formula_rec_lambda_replacement_Reflects:
"REFLECTS [\x. \u[L]. u \ B \
     mem_formula(L,u) \<and>
     (\<exists>c[L].
         is_formula_case
          (L, satisfies_is_a(L,A), satisfies_is_b(L,A),
           satisfies_is_c(L,A,g), satisfies_is_d(L,A,g),
           u, c) \<and>
         pair(L,u,c,x)),
  \<lambda>i x. \<exists>u \<in> Lset(i). u \<in> B \<and> mem_formula(##Lset(i),u) \<and>
     (\<exists>c \<in> Lset(i).
         is_formula_case
          (##Lset(i), satisfies_is_a(##Lset(i),A), satisfies_is_b(##Lset(i),A),
           satisfies_is_c(##Lset(i),A,g), satisfies_is_d(##Lset(i),A,g),
           u, c) \<and>
         pair(##Lset(i),u,c,x))]"
by (intro FOL_reflections function_reflections mem_formula_reflection
          is_formula_case_reflection satisfies_is_a_reflection
          satisfies_is_b_reflection satisfies_is_c_reflection
          satisfies_is_d_reflection)

lemma formula_rec_lambda_replacement:
      \<comment> \<open>For the \<^term>\<open>transrec\<close>\<close>
   "\L(g); L(A)\ \
    strong_replacement (L,
       \<lambda>x y. mem_formula(L,x) \<and>
             (\<exists>c[L]. is_formula_case(L, satisfies_is_a(L,A),
                                  satisfies_is_b(L,A),
                                  satisfies_is_c(L,A,g),
                                  satisfies_is_d(L,A,g), x, c) \<and>
             pair(L, x, c, y)))"
apply (rule strong_replacementI)
apply (rule_tac u="{B,A,g}"
         in gen_separation_multi [OF formula_rec_lambda_replacement_Reflects],
       auto)
apply (rule_tac env="[A,g,B]" in DPow_LsetI)
apply (rule sep_rules mem_formula_iff_sats
          formula_case_iff_sats satisfies_is_a_iff_sats
          satisfies_is_b_iff_sats satisfies_is_c_iff_sats
          satisfies_is_d_iff_sats | simp)+
done

subsection\<open>Instantiating \<open>M_satisfies\<close>\<close>

lemma M_satisfies_axioms_L: "M_satisfies_axioms(L)"
  apply (rule M_satisfies_axioms.intro)
       apply (assumption | rule
         Member_replacement Equal_replacement
         Nand_replacement Forall_replacement
         formula_rec_replacement formula_rec_lambda_replacement)+
  done

theorem M_satisfies_L: "M_satisfies(L)"
  apply (rule M_satisfies.intro)
   apply (rule M_eclose_L)
  apply (rule M_satisfies_axioms_L)
  done

text\<open>Finally: the point of the whole theory!\<close>
lemmas satisfies_closed = M_satisfies.satisfies_closed [OF M_satisfies_L]
   and satisfies_abs = M_satisfies.satisfies_abs [OF M_satisfies_L]

end

quality100%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.34Bemerkung: Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Eine klare Vorstellung vom Zielzustand

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.

Impressum Satisfies_absolute.thy Interaktion und PortierbarkeitIsabelle

Haftungshinweis

Bemerkung:

Impressum Satisfies_absolute.thy Interaktion und
PortierbarkeitIsabelle