SSL Satisfies_absolute.thy

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

section ‹Absoluteness for the Satisfies Relation on Formulas›

theory Satisfies_absolute imports Datatype_absolute Rec_Separation begin 


subsection ‹More Internalization›

subsubsection‹The Formula 🍋‹is_depth›, Internalized›

(*    "is_depth(M,p,n) \<equiv> 
  ∃sn[M]. ∃formula_n[M]. ∃formula_sn[M].
  2 1 0
  is_formula_N(M,n,formula_n) ∧ p ∉ formula_n ∧
        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)]
    ==> sats(A, depth_fm(x,y), env) ⟷
        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 ∈ nat; j < length(env); env ∈ list(A)]
       ==> is_depth(##A, x, y) ⟷ sats(A, depth_fm(i,j), env)"
by (simp)

theorem depth_reflection:
     "REFLECTS[λx. is_depth(L, f(x), g(x)),
               λ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‹The Operator 🍋‹is_formula_case›\›

text‹The arguments of 🍋‹is_a› are always 2, 1, 0, and the formula
  will be enclosed by three quantifiers.›

(* is_formula_case :: 
  "[i==>o, [i,i,i]==>o, [i,i,i]==>o, [i,i,i]==>o, [i,i]==>o, i, i] ==> o"
  "is_formula_case(M, is_a, is_b, is_c, is_d, v, z) ≡
  (∀x[M]. ∀y[M]. x∈nat ⟶ y∈nat ⟶ is_Member(M,x,y,v) ⟶ is_a(x,y,z)) ∧
  (∀x[M]. ∀y[M]. x∈nat ⟶ y∈nat ⟶ is_Equal(M,x,y,v) ⟶ is_b(x,y,z)) ∧
  (∀x[M]. ∀y[M]. x∈formula ⟶ y∈formula ⟶
  is_Nand(M,x,y,v) ⟶ is_c(x,y,z)) ∧
      (\<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 ∈ nat; y ∈ nat]
      ==> formula_case_fm(is_a, is_b, is_c, is_d, x, y) ∈ formula"
by (simp add: formula_case_fm_def)

lemma sats_formula_case_fm:
  assumes is_a_iff_sats: 
      "∧a0 a1 a2.
        [a0∈A; a1∈A; a2∈A]
        ==> ISA(a2, a1, a0) ⟷ sats(A, is_a, Cons(a0,Cons(a1,Cons(a2,env))))"
  and is_b_iff_sats: 
      "∧a0 a1 a2.
        [a0∈A; a1∈A; a2∈A]
        ==> ISB(a2, a1, a0) ⟷ sats(A, is_b, Cons(a0,Cons(a1,Cons(a2,env))))"
  and is_c_iff_sats: 
      "∧a0 a1 a2.
        [a0∈A; a1∈A; a2∈A]
        ==> ISC(a2, a1, a0) ⟷ sats(A, is_c, Cons(a0,Cons(a1,Cons(a2,env))))"
  and is_d_iff_sats: 
      "∧a0 a1.
        [a0∈A; a1∈A]
        ==> ISD(a1, a0) ⟷ sats(A, is_d, Cons(a0,Cons(a1,env)))"
  shows 
      "[x ∈ nat; y < length(env); env ∈ list(A)]
       ==> sats(A, formula_case_fm(is_a,is_b,is_c,is_d,x,y), env) ⟷
           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.
        [a0∈A; a1∈A; a2∈A]
        ==> ISA(a2, a1, a0) ⟷ sats(A, is_a, Cons(a0,Cons(a1,Cons(a2,env))))"
  and is_b_iff_sats: 
      "∧a0 a1 a2.
        [a0∈A; a1∈A; a2∈A]
        ==> ISB(a2, a1, a0) ⟷ sats(A, is_b, Cons(a0,Cons(a1,Cons(a2,env))))"
  and is_c_iff_sats: 
      "∧a0 a1 a2.
        [a0∈A; a1∈A; a2∈A]
        ==> ISC(a2, a1, a0) ⟷ sats(A, is_c, Cons(a0,Cons(a1,Cons(a2,env))))"
  and is_d_iff_sats: 
      "∧a0 a1.
        [a0∈A; a1∈A]
        ==> ISD(a1, a0) ⟷ sats(A, is_d, Cons(a0,Cons(a1,env)))"
  shows 
      "[nth(i,env) = x; nth(j,env) = y;
      i ∈ nat; j < length(env); env ∈ list(A)]
       ==> is_formula_case(##A, ISA, ISB, ISC, ISD, x, y) ⟷
           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‹The second argument of 🍋‹is_a› gives it direct access to 🍋‹x›,
  which is essential for handling free variable references. Treatment is
  based on that of ‹is_nat_case_reflection›.›
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)),
                     λ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)),
                     λ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)),
                     λ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)),
                     λ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)),
               λ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 ‹Absoluteness for the Function 🍋‹satisfies›\›

definition
  is_depth_apply :: "[i==>o,i,i,i] ==> o" where
   🍋 ‹Merely a useful abbreviation for the sequel.›
  "is_depth_apply(M,h,p,z) ≡
    ∃dp[M]. ∃sdp[M]. ∃hsdp[M].
        finite_ordinal(M,dp) ∧ is_depth(M,p,dp) ∧ successor(M,dp,sdp) ∧
        fun_apply(M,h,sdp,hsdp) ∧ fun_apply(M,hsdp,p,z)"

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



text‹There is at present some redundancy between the relativizations in
  e.g. ‹satisfies_is_a› and those in e.g. ‹Member_replacement›.›

text‹These constants let us instantiate the parameters 🍋‹a›, 🍋‹b›,
  🍋‹c›, 🍋‹d›, etc., of the locale ‹Formula_Rec›.›
definition
  satisfies_a :: "[i,i,i]==>i" where
   "satisfies_a(A) ≡
    λx y. λenv ∈ list(A). bool_of_o (nth(x,env) ∈ nth(y,env))"

definition
  satisfies_is_a :: "[i==>o,i,i,i,i]==>o" where
   "satisfies_is_a(M,A) ≡
    λx y zz. ∀lA[M]. is_list(M,A,lA) ⟶
             is_lambda(M, lA,
                λenv z. is_bool_of_o(M,
                      ∃nx[M]. ∃ny[M].
                       is_nth(M,x,env,nx) ∧ is_nth(M,y,env,ny) ∧ nx ∈ ny, z),
                zz)"

definition
  satisfies_b :: "[i,i,i]==>i" where
   "satisfies_b(A) ≡
    λx y. λenv ∈ list(A). bool_of_o (nth(x,env) = nth(y,env))"

definition
  satisfies_is_b :: "[i==>o,i,i,i,i]==>o" where
   🍋 ‹We simplify the formula to have just 🍋‹nx› rather than
  introducing 🍋‹ny› with 🍋‹nx=ny›\›
  "satisfies_is_b(M,A) ≡
    λx y zz. ∀lA[M]. is_list(M,A,lA) ⟶
             is_lambda(M, lA,
                λenv z. is_bool_of_o(M,
                      ∃nx[M]. is_nth(M,x,env,nx) ∧ 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) ≡
    λp q zz. ∀lA[M]. is_list(M,A,lA) ⟶
             is_lambda(M, lA, λenv z. ∃hp[M]. ∃hq[M].
                 (∃rp[M]. is_depth_apply(M,h,p,rp) ∧ fun_apply(M,rp,env,hp)) ∧
                 (∃rq[M]. is_depth_apply(M,h,q,rq) ∧ fun_apply(M,rq,env,hq)) ∧
                 (∃pq[M]. is_and(M,hp,hq,pq) ∧ is_not(M,pq,z)),
                zz)"

definition
  satisfies_d :: "[i,i,i]==>i" where
   "satisfies_d(A)
    ≡ λp rp. λenv ∈ list(A). bool_of_o (∀x∈A. rp ` (Cons(x,env)) = 1)"

definition
  satisfies_is_d :: "[i==>o,i,i,i,i]==>o" where
   "satisfies_is_d(M,A,h) ≡
    λp zz. ∀lA[M]. is_list(M,A,lA) ⟶
             is_lambda(M, lA,
                λenv z. ∃rp[M]. is_depth_apply(M,h,p,rp) ∧
                    is_bool_of_o(M,
                           ∀x[M]. ∀xenv[M]. ∀hp[M].
                              x∈A ⟶ is_Cons(M,x,env,xenv) ⟶
                              fun_apply(M,rp,xenv,hp) ⟶ number1(M,hp),
                  z),
               zz)"

definition
  satisfies_MH :: "[i==>o,i,i,i,i]==>o" where
    🍋 ‹The variable 🍋‹u› is unused, but gives 🍋‹satisfies_MH›
  the correct arity.›
  "satisfies_MH ≡
    λM A u f z.
         ∀fml[M]. is_formula(M,fml) ⟶
             is_lambda (M, fml,
               is_formula_case (M, satisfies_is_a(M,A),
                                satisfies_is_b(M,A),
                                satisfies_is_c(M,A,f), satisfies_is_d(M,A,f)),
               z)"

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


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

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


lemma (in M_satisfies) Member_replacement':
    "[M(A); x ∈ nat; y ∈ nat]
     ==> strong_replacement
         (M, λenv z. env ∈ list(A) ∧
                     z = ⟨env, bool_of_o(nth(x, env) ∈ nth(y, env))⟩)"
by (insert Member_replacement, simp) 

lemma (in M_satisfies) Equal_replacement':
    "[M(A); x ∈ nat; y ∈ nat]
     ==> strong_replacement
         (M, λenv z. env ∈ list(A) ∧
                     z = ⟨env, bool_of_o(nth(x, env) = nth(y, env))⟩)"
by (insert Equal_replacement, simp) 

lemma (in M_satisfies) Nand_replacement':
    "[M(A); M(rp); M(rq)]
     ==> strong_replacement
         (M, λenv z. env ∈ list(A) ∧ z = ⟨env, not(rp`env and rq`env)⟩)"
by (insert Nand_replacement, simp) 

lemma (in M_satisfies) Forall_replacement':
   "[M(A); M(rp)]
    ==> strong_replacement
        (M, λenv z.
               env ∈ list(A) ∧
               z = ⟨env, bool_of_o (∀a∈A. rp ` Cons(a,env) = 1)⟩)"
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)]
      ==> 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),
               λ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),
     λ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),
       λu v. satisfies_c(A, u, v,
                         g ` succ(depth(u)) ` u, g ` succ(depth(v)) ` v),
       λ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, λx y. x ∈ formula ∧
            y = ⟨x,
                 formula_rec_case(satisfies_a(A),
                                  satisfies_b(A),
                                  satisfies_c(A),
                                  satisfies_d(A), g, x)⟩)"
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‹Instantiate locale ‹Formula_Rec› for the
  Function 🍋‹satisfies›\›

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]
   ==> is_satisfies(M,A,p,z) ⟷ 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‹Internalizations Needed to Instantiate ‹M_satisfies›\›

subsubsection‹The Operator 🍋‹is_depth_apply›, Internalized›

(* is_depth_apply(M,h,p,z) \<equiv>
  ∃dp[M]. ∃sdp[M]. ∃hsdp[M].
  2 1 0
  finite_ordinal(M,dp) ∧ is_depth(M,p,dp) ∧ successor(M,dp,sdp) ∧
        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)]
    ==> sats(A, depth_apply_fm(x,y,z), env) ⟷
        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 ∈ nat; j ∈ nat; k ∈ nat; env ∈ list(A)]
     ==> is_depth_apply(##A, x, y, z) ⟷ 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)),
               λ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‹The Operator 🍋‹satisfies_is_a›, Internalized›

(* satisfies_is_a(M,A) \<equiv> 
  λx y zz. ∀lA[M]. is_list(M,A,lA) ⟶
  is_lambda(M, lA,
  λenv z. is_bool_of_o(M,
  ∃nx[M]. ∃ny[M].
  is_nth(M,x,env,nx) ∧ is_nth(M,y,env,ny) ∧ nx ∈ 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]
      ==> satisfies_is_a_fm(A,x,y,z) ∈ 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)]
    ==> sats(A, satisfies_is_a_fm(u,x,y,z), env) ⟷
        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 ∈ nat; x < length(env); y < length(env); z ∈ nat; env ∈ list(A)]
   ==> satisfies_is_a(##A,nu,nx,ny,nz) ⟷
       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)),
               λ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‹The Operator 🍋‹satisfies_is_b›, Internalized›

(* satisfies_is_b(M,A) \<equiv> 
  λx y zz. ∀lA[M]. is_list(M,A,lA) ⟶
  is_lambda(M, lA,
  λenv z. is_bool_of_o(M,
  ∃nx[M]. is_nth(M,x,env,nx) ∧ 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]
      ==> satisfies_is_b_fm(A,x,y,z) ∈ 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)]
    ==> sats(A, satisfies_is_b_fm(u,x,y,z), env) ⟷
        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 ∈ nat; x < length(env); y < length(env); z ∈ nat; env ∈ list(A)]
   ==> satisfies_is_b(##A,nu,nx,ny,nz) ⟷
       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)),
               λ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‹The Operator 🍋‹satisfies_is_c›, Internalized›

(* satisfies_is_c(M,A,h) \<equiv> 
  λp q zz. ∀lA[M]. is_list(M,A,lA) ⟶
  is_lambda(M, lA, λenv z. ∃hp[M]. ∃hq[M].
  (∃rp[M]. is_depth_apply(M,h,p,rp) ∧ fun_apply(M,rp,env,hp)) ∧
  (∃rq[M]. is_depth_apply(M,h,q,rq) ∧ fun_apply(M,rq,env,hq)) ∧
  (∃pq[M]. is_and(M,hp,hq,pq) ∧ 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]
      ==> satisfies_is_c_fm(A,h,x,y,z) ∈ 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)]
    ==> sats(A, satisfies_is_c_fm(u,v,x,y,z), env) ⟷
        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 ∈ nat; v ∈ nat; x ∈ nat; y ∈ nat; z ∈ nat; env ∈ list(A)]
   ==> satisfies_is_c(##A,nu,nv,nx,ny,nz) ⟷
       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)),
               λ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‹The Operator 🍋‹satisfies_is_d›, Internalized›

(* satisfies_is_d(M,A,h) \<equiv> 
  λp zz. ∀lA[M]. is_list(M,A,lA) ⟶
  is_lambda(M, lA,
  λenv z. ∃rp[M]. is_depth_apply(M,h,p,rp) ∧
  is_bool_of_o(M,
  ∀x[M]. ∀xenv[M]. ∀hp[M].
  x∈A ⟶ is_Cons(M,x,env,xenv) ⟶
  fun_apply(M,rp,xenv,hp) ⟶ 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]
      ==> satisfies_is_d_fm(A,h,x,z) ∈ 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)]
    ==> sats(A, satisfies_is_d_fm(u,x,y,z), env) ⟷
        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 ∈ nat; x ∈ nat; y ∈ nat; z ∈ nat; env ∈ list(A)]
   ==> satisfies_is_d(##A,nu,nx,ny,nz) ⟷
       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)),
               λ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‹The Operator 🍋‹satisfies_MH›, Internalized›

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

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]
      ==> satisfies_MH_fm(A,u,x,z) ∈ 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)]
    ==> sats(A, satisfies_MH_fm(u,x,y,z), env) ⟷
        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 ∈ nat; x ∈ nat; y ∈ nat; z ∈ nat; env ∈ list(A)]
   ==> satisfies_MH(##A,nu,nx,ny,nz) ⟷
       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)),
               λ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‹Lemmas for Instantiating the Locale ‹M_satisfies›\›


subsubsection‹The 🍋‹Member› Case›

lemma Member_Reflects:
 "REFLECTS[λu. ∃v[L]. v ∈ B ∧ (∃bo[L]. ∃nx[L]. ∃ny[L].
          v ∈ lstA ∧ is_nth(L,x,v,nx) ∧ is_nth(L,y,v,ny) ∧
          is_bool_of_o(L, nx ∈ ny, bo) ∧ pair(L,v,bo,u)),
   λi u. ∃v ∈ Lset(i). v ∈ B ∧ (∃bo ∈ Lset(i). ∃nx ∈ Lset(i). ∃ny ∈ Lset(i).
             v ∈ lstA ∧ is_nth(##Lset(i), x, v, nx) ∧
             is_nth(##Lset(i), y, v, ny) ∧
          is_bool_of_o(##Lset(i), nx ∈ ny, bo) ∧ 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]
     ==> strong_replacement
         (L, λenv z. ∃bo[L]. ∃nx[L]. ∃ny[L].
              env ∈ list(A) ∧ is_nth(L,x,env,nx) ∧ is_nth(L,y,env,ny) ∧
              is_bool_of_o(L, nx ∈ ny, bo) ∧
              pair(L, env, bo, z))"
apply (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‹The 🍋‹Equal› Case›

lemma Equal_Reflects:
 "REFLECTS[λu. ∃v[L]. v ∈ B ∧ (∃bo[L]. ∃nx[L]. ∃ny[L].
          v ∈ lstA ∧ is_nth(L, x, v, nx) ∧ is_nth(L, y, v, ny) ∧
          is_bool_of_o(L, nx = ny, bo) ∧ pair(L, v, bo, u)),
   λi u. ∃v ∈ Lset(i). v ∈ B ∧ (∃bo ∈ Lset(i). ∃nx ∈ Lset(i). ∃ny ∈ Lset(i).
             v ∈ lstA ∧ is_nth(##Lset(i), x, v, nx) ∧
             is_nth(##Lset(i), y, v, ny) ∧
          is_bool_of_o(##Lset(i), nx = ny, bo) ∧ 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]
     ==> strong_replacement
         (L, λenv z. ∃bo[L]. ∃nx[L]. ∃ny[L].
              env ∈ list(A) ∧ is_nth(L,x,env,nx) ∧ is_nth(L,y,env,ny) ∧
              is_bool_of_o(L, nx = ny, bo) ∧
              pair(L, env, bo, z))"
apply (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‹The 🍋‹Nand› Case›

lemma Nand_Reflects:
    "REFLECTS [λx. ∃u[L]. u ∈ B ∧
               (∃rpe[L]. ∃rqe[L]. ∃andpq[L]. ∃notpq[L].
                 fun_apply(L, rp, u, rpe) ∧ fun_apply(L, rq, u, rqe) ∧
                 is_and(L, rpe, rqe, andpq) ∧ is_not(L, andpq, notpq) ∧
                 u ∈ list(A) ∧ pair(L, u, notpq, x)),
    λi x. ∃u ∈ Lset(i). u ∈ B ∧
     (∃rpe ∈ Lset(i). ∃rqe ∈ Lset(i). ∃andpq ∈ Lset(i). ∃notpq ∈ Lset(i).
       fun_apply(##Lset(i), rp, u, rpe) ∧ fun_apply(##Lset(i), rq, u, rqe) ∧
       is_and(##Lset(i), rpe, rqe, andpq) ∧ is_not(##Lset(i), andpq, notpq) ∧
       u ∈ list(A) ∧ 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)]
     ==> strong_replacement
         (L, λenv z. ∃rpe[L]. ∃rqe[L]. ∃andpq[L]. ∃notpq[L].
               fun_apply(L,rp,env,rpe) ∧ fun_apply(L,rq,env,rqe) ∧
               is_and(L,rpe,rqe,andpq) ∧ is_not(L,andpq,notpq) ∧
               env ∈ list(A) ∧ 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‹The 🍋‹Forall› Case›

lemma Forall_Reflects:
 "REFLECTS [λx. ∃u[L]. u ∈ B ∧ (∃bo[L]. u ∈ list(A) ∧
                 is_bool_of_o (L,
     ∀a[L]. ∀co[L]. ∀rpco[L]. a ∈ A ⟶
                is_Cons(L,a,u,co) ⟶ fun_apply(L,rp,co,rpco) ⟶
                number1(L,rpco),
                           bo) ∧ pair(L,u,bo,x)),
 λi x. ∃u ∈ Lset(i). u ∈ B ∧ (∃bo ∈ Lset(i). u ∈ list(A) ∧
        is_bool_of_o (##Lset(i),
 ∀a ∈ Lset(i). ∀co ∈ Lset(i). ∀rpco ∈ Lset(i). a ∈ A ⟶
            is_Cons(##Lset(i),a,u,co) ⟶ fun_apply(##Lset(i),rp,co,rpco) ⟶
            number1(##Lset(i),rpco),
                       bo) ∧ 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)]
    ==> strong_replacement
        (L, λenv z. ∃bo[L].
              env ∈ list(A) ∧
              is_bool_of_o (L,
                            ∀a[L]. ∀co[L]. ∀rpco[L].
                               a∈A ⟶ is_Cons(L,a,env,co) ⟶
                               fun_apply(L,rp,co,rpco) ⟶ number1(L, rpco),
                            bo) ∧
              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‹The 🍋‹transrec_replacement› Case›

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)),
    λi x. ∃u ∈ Lset(i). u ∈ B ∧ (∃y ∈ Lset(i). pair(##Lset(i), u, y, x) ∧
             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: 
      🍋 ‹For the 🍋‹transrec›\›
   "[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‹The Lambda Replacement Case›

lemma formula_rec_lambda_replacement_Reflects:
 "REFLECTS [λx. ∃u[L]. u ∈ B ∧
     mem_formula(L,u) ∧
     (∃c[L].
         is_formula_case
          (L, satisfies_is_a(L,A), satisfies_is_b(L,A),
           satisfies_is_c(L,A,g), satisfies_is_d(L,A,g),
           u, c) ∧
         pair(L,u,c,x)),
  λi x. ∃u ∈ Lset(i). u ∈ B ∧ mem_formula(##Lset(i),u) ∧
     (∃c ∈ Lset(i).
         is_formula_case
          (##Lset(i), satisfies_is_a(##Lset(i),A), satisfies_is_b(##Lset(i),A),
           satisfies_is_c(##Lset(i),A,g), satisfies_is_d(##Lset(i),A,g),
           u, c) ∧
         pair(##Lset(i),u,c,x))]"
by (intro FOL_reflections function_reflections mem_formula_reflection
          is_formula_case_reflection satisfies_is_a_reflection
          satisfies_is_b_reflection satisfies_is_c_reflection
          satisfies_is_d_reflection)  

lemma formula_rec_lambda_replacement: 
      🍋 ‹For the 🍋‹transrec›\›
   "[L(g); L(A)] ==>
    strong_replacement (L,
       λx y. mem_formula(L,x) ∧
             (∃c[L]. is_formula_case(L, satisfies_is_a(L,A),
                                  satisfies_is_b(L,A),
                                  satisfies_is_c(L,A,g),
                                  satisfies_is_d(L,A,g), x, c) ∧
             pair(L, x, c, y)))" 
apply (rule strong_replacementI)
apply (rule_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‹Instantiating ‹M_satisfies›\›

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

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

text‹Finally: the point of the whole theory!›
lemmas satisfies_closed = M_satisfies.satisfies_closed [OF M_satisfies_L]
   and satisfies_abs = M_satisfies.satisfies_abs [OF M_satisfies_L]

end