Theory Satisfies_absolute

(*  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 termis_depth, Internalized›

(*    "is_depth(M,p,n) ≡ 
       ∃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) ∧ is_formula_N(M,sn,formula_sn) ∧ p ∈ 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 termis_formula_case

text‹The arguments of termis_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)) ∧
      (∀x[M]. x∈formula ⟶ is_Forall(M,x,v) ⟶ 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. 
        a0A; a1A; a2A  
         ISA(a2, a1, a0)  sats(A, is_a, Cons(a0,Cons(a1,Cons(a2,env))))"
  and is_b_iff_sats: 
      "a0 a1 a2. 
        a0A; a1A; a2A  
         ISB(a2, a1, a0)  sats(A, is_b, Cons(a0,Cons(a1,Cons(a2,env))))"
  and is_c_iff_sats: 
      "a0 a1 a2. 
        a0A; a1A; a2A  
         ISC(a2, a1, a0)  sats(A, is_c, Cons(a0,Cons(a1,Cons(a2,env))))"
  and is_d_iff_sats: 
      "a0 a1. 
        a0A; a1A  
         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. 
        a0A; a1A; a2A  
         ISA(a2, a1, a0)  sats(A, is_a, Cons(a0,Cons(a1,Cons(a2,env))))"
  and is_b_iff_sats: 
      "a0 a1 a2. 
        a0A; a1A; a2A  
         ISB(a2, a1, a0)  sats(A, is_b, Cons(a0,Cons(a1,Cons(a2,env))))"
  and is_c_iff_sats: 
      "a0 a1 a2. 
        a0A; a1A; a2A  
         ISC(a2, a1, a0)  sats(A, is_c, Cons(a0,Cons(a1,Cons(a2,env))))"
  and is_d_iff_sats: 
      "a0 a1. 
        a0A; a1A  
         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 termis_a gives it direct access to termx,
  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 termsatisfies

definition
  is_depth_apply :: "[io,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 terma, termb,
      termc, termd, 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 :: "[io,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 :: "[io,i,i,i,i]o" where
   ― ‹We simplify the formula to have just termnx rather than 
       introducing termny with  termnx=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 :: "[io,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 (xA. rp ` (Cons(x,env)) = 1)"

definition
  satisfies_is_d :: "[io,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]. 
                              xA  is_Cons(M,x,env,xenv)  
                              fun_apply(M,rp,xenv,hp)  number1(M,hp),
                  z),
               zz)"

definition
  satisfies_MH :: "[io,i,i,i,i]o" where
    ― ‹The variable termu is unused, but gives termsatisfies_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 :: "[io,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 termsatisfies.
      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 termM in order to prove
      absoluteness for the constants defined above.  The ultimate goal
      is the absoluteness of the function termsatisfies.›
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]. 
                               aA  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 termtransrec
   "n  nat; M(A)  transrec_replacement(M, satisfies_MH(M,A), n)"
 and
  formula_rec_lambda_replacement:  
      ― ‹For the λ-abstraction› in the termtransrec 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 (aA. rp ` Cons(a,env) = 1))"
by (insert Forall_replacement, simp) 

lemma (in M_satisfies) a_closed:
     "M(A); xnat; ynat  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); xnat; ynat  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 termsatisfies

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 termis_depth_apply, Internalized›

(* is_depth_apply(M,h,p,z) ≡
    ∃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) ∧ 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 termsatisfies_is_a, Internalized›

(* 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_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 termsatisfies_is_b, Internalized›

(* 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_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 termsatisfies_is_c, Internalized›

(* 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_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 termsatisfies_is_d, Internalized›

(* 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_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 termsatisfies_MH, Internalized›

(* satisfies_MH ≡ 
    λ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 termMember 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 termEqual 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 termNand 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 termForall 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]. 
                               aA  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 termtransrec_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 termtransrec
   "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 termtransrec
   "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