Theory Q0

section ‹Q0 abbreviations›

theory Q0
  imports Set_Theory 
  abbrevs "App" = "❙⋅"
    and "Abs" = "❙[❙λ_:_. _❙]"
    and "Eql" = "❙[_ ❙=_❙= _❙]"
    and "Con" = "❙∧"
    and "Forall" = "❙[❙∀_:_. _❙]"
    and "Imp" = "❙⟶"
    and "Fun" = "❙⇐"
begin

lemma arg_cong3: "a = b ⟹ c = d ⟹ e = f ⟹ h a c e = h b d f"
  by auto


section ‹Syntax and typing›

datatype type_sym =
  Ind | 
  Tv |
  Fun type_sym type_sym (infixl "❙⇐" 80)

type_synonym var_sym = string
type_synonym cst_sym = string

datatype trm =
  Var var_sym type_sym |
  Cst cst_sym type_sym |
  App trm trm (infixl "❙⋅" 80) |
  Abs var_sym type_sym trm ("❙[❙λ_:_. _❙]" [80,80,80])

fun vars :: "trm ⇒ (var_sym * type_sym) set" where
  "vars (Var x α) = {(x,α)}"
| "vars (Cst _ _) = {}"
| "vars (A ❙⋅ B) = vars A ∪ vars B"
| "vars (❙[❙λx:α. A❙]) = {(x,α)} ∪ vars A"

fun frees :: "trm ⇒ (var_sym * type_sym) set" where
  "frees (Var x α) = {(x,α)}"
| "frees (Cst _ _) = {}"
| "frees (A ❙⋅ B) = frees A ∪ frees B"
| "frees (❙[❙λx:α. A❙]) = frees A - {(x,α)}"

lemma frees_subset_vars:
  "frees A ⊆ vars A"
  by (induction A) auto

inductive wff :: "type_sym ⇒ trm ⇒ bool" where
  wff_Var: "wff α (Var _ α)"
| wff_Cst: "wff α (Cst _ α)"
| wff_App: "wff (α ❙⇐ β) A ⟹ wff β B ⟹ wff α (A ❙⋅ B)"
| wff_Abs: "wff α A ⟹ wff (α ❙⇐ β) ❙[❙λx:β. A❙]"

fun type_of :: "trm ⇒ type_sym" where
  "type_of (Var x α) = α"
| "type_of (Cst c α) = α"
| "type_of (A ❙⋅ B) =
     (case type_of A of β ❙⇐ α ⇒ β)"
| "type_of ❙[❙λx:α. A❙] = (type_of A) ❙⇐ α"

lemma type_of[simp]:
  "wff α A ⟹ type_of A = α"
  by (induction rule: wff.induct) auto

lemma wff_Var'[simp, code]: 
  "wff β (Var x α) ⟷ β = α"
  using wff.cases wff_Var by auto

lemma wff_Cst'[simp, code]:
  "wff β (Cst c α) ⟷ β = α"
  using wff.cases wff_Cst by auto

lemma wff_App'[simp]:
  "wff α (A ❙⋅ B) ⟷ (∃β. wff (α ❙⇐ β) A ∧ wff β B)"
proof
  assume "wff α (A ❙⋅ B)"
  then show "∃β. wff (α ❙⇐ β) A ∧ wff β B" 
    using wff.cases by fastforce
next
  assume "∃β. wff (α ❙⇐ β) A ∧ wff β B"
  then show "wff α (A ❙⋅ B)"
    using wff_App by auto
qed

lemma wff_Abs'[simp]:
  "wff γ (❙[❙λx:α. A❙]) ⟷ (∃β. wff β A ∧ γ = β ❙⇐ α)"
proof
  assume "wff γ ❙[❙λx:α. A❙]"
  then show "∃β. wff β A ∧ γ = β ❙⇐ α" 
    using wff.cases by blast
next
  assume "∃β. wff β A ∧ γ = β ❙⇐ α"
  then show "wff γ ❙[❙λx:α. A❙]" 
    using wff_Abs by auto     
qed

lemma wff_Abs_type_of[code]:
  "wff γ ❙[❙λx:α. A❙] ⟷ (wff (type_of A) A ∧ γ = (type_of A) ❙⇐ α)"
proof
  assume "wff γ ❙[❙λx:α. A❙]"
  then show "wff (type_of A) A ∧ γ = (type_of A) ❙⇐ α" 
    using wff.cases by auto
next
  assume "wff (type_of A) A ∧ γ = (type_of A) ❙⇐ α"
  then show "wff γ ❙[❙λx:α. A❙]" 
    using wff_Abs by auto
qed

lemma wff_App_type_of[code]:
  "wff γ ((A ❙⋅ B)) ⟷ (wff (type_of A) A ∧ wff (type_of B) B ∧ type_of A = γ ❙⇐ (type_of B))"
proof
  assume "wff γ (A ❙⋅ B)"
  then show "wff (type_of A) A ∧ wff (type_of B) B ∧ type_of A = γ ❙⇐ (type_of B)" 
    by auto
next
  assume "wff (type_of A) A ∧ wff (type_of B) B ∧ type_of A = γ ❙⇐ (type_of B)"
  then show "wff γ (A ❙⋅ B)"
    by (metis wff_App')
qed

lemma unique_type:
  "wff β A ⟹ wff α A ⟹ α = β"
proof (induction arbitrary: α rule: wff.induct)
  case (wff_Var α' y)
  then show ?case
    by simp
next
  case (wff_Cst α' c)
  then show ?case
    by simp 
next
  case (wff_App α' β A B)
  then show ?case
    using wff_App' by blast
next
  case (wff_Abs β A α x)
  then show ?case
    using wff_Abs_type_of by blast
qed


section ‹Replacement›

inductive replacement :: "trm ⇒ trm ⇒ trm ⇒ trm ⇒ bool" where
  replace: "replacement A B A B"
| replace_App_left: "replacement A B C E ⟹ replacement A B (C ❙⋅ D) (E ❙⋅ D)"
| replace_App_right: "replacement A B D E ⟹ replacement A B (C ❙⋅ D) (C ❙⋅ E)"
| replace_Abs: "replacement A B C D ⟹ replacement A B ❙[❙λx:α. C❙] ❙[❙λx:α. D❙]"

lemma replacement_preserves_type:
  assumes "replacement A B C D"
  assumes "wff α A"
  assumes "wff α B"
  assumes "wff β C"
  shows "wff β D"
  using assms
proof (induction arbitrary: α β rule: replacement.induct)
  case (replace A B)
  then show ?case
    using unique_type by auto
next
  case (replace_App_left A B C E D)
  then have "∃β'. wff (β ❙⇐ β') C"
    by auto
  then obtain β' where wff_C: "wff (β ❙⇐ β') C"
    by auto
  then have e: "wff (β ❙⇐ β') E"
    using replace_App_left by auto
  define α' where "α' = β ❙⇐ β'"
  have "wff β' D"
    using wff_C unique_type replace_App_left.prems(3) by auto
  then have "wff β (E ❙⋅ D)"
    using e by auto
  then show ?case
    by auto
next
  case (replace_App_right A B D E C)
  have "∃β'. wff (β ❙⇐ β') C"
    using replace_App_right.prems(3) by auto
  then obtain β' where wff_C: "wff (β ❙⇐ β') C"
    by auto
  have wff_E: "wff β' E"
    using wff_C unique_type replace_App_right by fastforce
  define α' where α': "α' = β ❙⇐ β'"
  have "wff β (C ❙⋅ E)"
    using wff_C wff_E by auto
  then show ?case
    using α' by auto
next
  case (replace_Abs A B C D x α')
  then have "∃β'. wff β' D"
    by auto
  then obtain β' where wff_D: "wff β' D"
    by auto
  have β: "β = β' ❙⇐ α'"
    using wff_D unique_type replace_Abs by auto
  have "wff (β' ❙⇐ α') (❙[❙λx:α'. D❙])"
    using wff_D by auto
  then show ?case
    using β by auto
qed

lemma replacement_preserved_type:
  assumes "replacement A B C D"
  assumes "wff α A"
  assumes "wff α B"
  assumes "wff β D"
  shows "wff β C"
  using assms
proof (induction arbitrary: α β rule: replacement.induct)
  case (replace A B)
  then show ?case 
    using unique_type by auto
next
  case (replace_App_left A B C E D)
  then obtain γ where γ: "wff (β ❙⇐ γ) E ∧ wff γ D"
    by auto
  then have "wff (β ❙⇐ γ) C"
    using replace_App_left by auto
  then show ?case
    using γ by auto 
next
  case (replace_App_right A B D E C)
  then obtain γ where γ: "wff (β ❙⇐ γ) C ∧ wff γ E"
    by auto
  then have "wff γ D"
    using replace_App_right by auto
  then show ?case
    using γ by auto 
next
  case (replace_Abs A B C D x α')
  then obtain γ where "wff γ D"
    by auto
  then show ?case
    using unique_type replace_Abs by auto
qed


section ‹Defined wffs›
  ― ‹This section formalizes most of the definitions and abbreviations from page 212.
    We formalize enough to define the Q0 proof system.›


subsection ‹Common expressions›

abbreviation (input) Var_yi ("y⇩i") where
  "y⇩i == Cst ''y'' Ind"

abbreviation (input) Var_xo ("x⇩o") where
  "x⇩o == Var ''x'' Tv"

abbreviation (input) Var_yo ("y⇩o") where
  "y⇩o == Var ''y'' Tv"

abbreviation (input) Fun_oo ("oo") where
  "oo == Tv ❙⇐ Tv"

abbreviation (input) Fun_ooo ("ooo") where
  "ooo == oo ❙⇐ Tv"

abbreviation (input) Var_goo ("g⇩o⇩o") where
  "g⇩o⇩o == Var ''g'' oo"

abbreviation (input) Var_gooo ("g⇩o⇩o⇩o") where
  "g⇩o⇩o⇩o == Var ''g'' ooo"


subsection ‹Equality symbol›

abbreviation QQ :: "type_sym ⇒ trm" ("❙Q") where
  "❙Q α ≡ Cst ''Q'' α"


subsection ‹Description or selection operator›

abbreviation ιι :: "trm" ("❙ι") where
  "❙ι ≡ Cst ''i'' (Ind ❙⇐ (Tv ❙⇐ Ind))"


subsection ‹Equality›

definition Eql :: "trm ⇒ trm ⇒ type_sym ⇒ trm" where
  "Eql A B α ≡ (❙Q (Tv ❙⇐ α ❙⇐ α)) ❙⋅ A ❙⋅ B"

abbreviation Eql' :: "trm ⇒ type_sym ⇒ trm ⇒ trm" ("❙[_ ❙=_❙= _❙]" [89]) where
  "❙[A ❙=α❙= B❙] ≡ Eql A B α"

definition LHS where
  "LHS EqlAB = (case EqlAB of (_ ❙⋅ A ❙⋅ _) ⇒ A)"

lemma LHS_def2[simp]: "LHS ❙[A ❙=α❙= B❙] = A"
  unfolding LHS_def Eql_def by auto

definition RHS where
  "RHS EqlAB = (case EqlAB of (_ ❙⋅ B ) ⇒ B)"

lemma RHS_def2[simp]: "RHS (❙[A ❙=α❙= B❙]) = B"
  unfolding RHS_def Eql_def by auto

lemma wff_Eql[simp]:
  "wff α A ⟹ wff α B ⟹ wff Tv ❙[A ❙=α❙= B❙]"
  unfolding Eql_def by force

lemma wff_Eql_iff[simp]:
  "wff β ❙[A ❙=α❙= B❙] ⟷ wff α A ∧ wff α B ∧ β = Tv"
  using Eql_def by auto


subsection ‹Truth›

definition T :: trm where
  "T ≡ ❙[(❙Q ooo) ❙=ooo❙= (❙Q ooo)❙]"

lemma wff_T[simp]: "wff Tv T"
  unfolding T_def by auto

lemma wff_T_iff[simp]: "wff α T ⟷ α = Tv"
  using unique_type wff_T by blast

subsection ‹Falsity›

abbreviation F :: trm where
  "F ≡ ❙[❙[❙λ''x'':Tv. T❙] ❙= oo❙= ❙[❙λ''x'':Tv. x⇩o❙]❙]"

lemma wff_F[simp]: "wff Tv F"
  by auto

lemma wff_F_iff[simp]: "wff α F ⟷ α = Tv"
  using unique_type wff_F by blast


subsection ‹Pi›

definition PI :: "type_sym ⇒ trm" where
  "PI α ≡ (❙Q (Tv ❙⇐ (Tv ❙⇐ α) ❙⇐ (Tv ❙⇐ α))) ❙⋅ ❙[❙λ ''x'':α. T❙]"

lemma wff_PI[simp]: "wff (Tv ❙⇐ (Tv ❙⇐ α)) (PI α)"
  unfolding PI_def by auto

lemma wff_PI_subterm[simp]: "wff (Tv ❙⇐ α) ❙[❙λ ''x'':α. T❙]"
  by auto

lemma wff_PI_subterm_iff[simp]:
  "wff β ❙[❙λ ''x'':α. T❙] ⟷ β = (Tv ❙⇐ α)"
  by auto


subsection ‹Forall›

definition Forall :: "string ⇒ type_sym ⇒ trm ⇒ trm" ("❙[❙∀_:_. _❙]" [80,80,80]) where 
  "❙[❙∀x:α. A❙] = (PI α) ❙⋅ ❙[❙λx:α. A❙]"

lemma wff_Forall[simp]: "wff Tv A ⟹ wff Tv ❙[❙∀x:α. A❙]"
  unfolding Forall_def by force

lemma wff_Forall_iff[simp]: "wff β ❙[❙∀x:α. A❙] ⟷ wff Tv A ∧ β = Tv"
proof 
  assume "wff β ❙[❙∀x:α. A❙]"
  then show "wff Tv A ∧ β = Tv"
    by (smt Forall_def unique_type type_sym.inject wff_Abs' wff_App' wff_PI)
next
  assume "wff Tv A ∧ β = Tv"
  then show "wff β ❙[❙∀x:α. A❙]" 
    unfolding Forall_def by force
qed


subsection ‹Conjunction symbol›

definition Con_sym :: trm where
  "Con_sym ≡
    ❙[❙λ''x'':Tv. ❙[❙λ''y'':Tv.
      ❙[❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙]  ❙=Tv ❙⇐ ooo❙=  ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]❙]
    ❙]❙]"

lemma wff_Con_sym[simp]: "wff ooo Con_sym"
  unfolding Con_sym_def by auto

lemma wff_Con_sym'[simp]: "wff α Con_sym ⟷ α = ooo"
  unfolding Con_sym_def by auto


lemma wff_Con_sym_subterm0[simp]:
  "wff Tv A ⟹ wff Tv B ⟹ wff (Tv ❙⇐ ooo) ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ A ❙⋅ B❙]"
  by force

lemma wff_Con_sym_subterm0_iff[simp]:
  "wff β ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ A ❙⋅ B❙] ⟷ wff Tv A ∧ wff Tv B ∧ β = (Tv ❙⇐ ooo)"
proof
  assume wff: "wff β ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ A ❙⋅ B❙]"
  then have "wff Tv A"
    by auto
  moreover
  from wff have "wff Tv B"
    by auto
  moreover
  from wff have "β = Tv ❙⇐ ooo"
    by auto
  ultimately show "wff Tv A ∧ wff Tv B ∧ β = Tv ❙⇐ ooo"
    by auto
next
  assume "wff Tv A ∧ wff Tv B ∧ β = Tv ❙⇐ ooo"
  then show "wff β ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ A ❙⋅ B❙]"
    by force
qed

lemma wff_Con_sym_subterm1[simp]:
  "wff Tv ❙[❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] ❙=(Tv ❙⇐ ooo)❙= ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]❙]"
  by auto

lemma wff_Con_sym_subterm1_iff[simp]:
  "wff α ❙[❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] ❙=(Tv ❙⇐ ooo)❙= ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]❙] ⟷ α = Tv"
  using unique_type wff_Con_sym_subterm1 by blast

lemma wff_Con_sym_subterm2[simp]:
  "wff oo ❙[❙λ ''y'':Tv. ❙[❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] ❙=(Tv ❙⇐ ooo)❙= ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]❙]❙]"
  by auto

lemma wff_Con_sym_subterm2_iff[simp]:
  "wff α ❙[❙λ ''y'':Tv. ❙[❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] ❙=(Tv ❙⇐ ooo)❙= ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅  x⇩o ❙⋅ y⇩o❙]❙]❙] ⟷ α = oo"
  by auto

subsection ‹Conjunction›

definition Con :: "trm ⇒ trm ⇒ trm" (infix "❙∧" 80) where
  "A ❙∧ B = Con_sym ❙⋅ A ❙⋅ B"

lemma wff_Con[simp]: "wff Tv A ⟹ wff Tv B ⟹ wff Tv (A ❙∧ B)"
  unfolding Con_def by auto

lemma wff_Con_iff[simp]: "wff α (A ❙∧ B) ⟷ wff Tv A ∧ wff Tv B ∧ α = Tv"
  unfolding Con_def by auto


subsection ‹Implication symbol›

definition Imp_sym :: trm where
  "Imp_sym ≡ ❙[❙λ''x'':Tv. ❙[❙λ''y'':Tv. ❙[x⇩o ❙=Tv❙= (x⇩o ❙∧ y⇩o)❙]❙]❙]"

lemma wff_Imp_sym[simp]:
  "wff ooo Imp_sym"
  unfolding Imp_sym_def by auto

lemma wff_Imp_sym_iff[simp]:
  "wff α Imp_sym ⟷ α = ooo"
  unfolding Imp_sym_def by auto

lemma wff_Imp_sym_subterm0[simp]:
  "wff Tv (x⇩o ❙∧ y⇩o)"
  by auto

lemma wff_Imp_sym_subterm0_iff[simp]:
  "wff α (x⇩o ❙∧ y⇩o) ⟷ α = Tv"
   by auto

lemma wff_Imp_sym_subterm1[simp]:
  "wff Tv ❙[x⇩o ❙=Tv❙= (x⇩o ❙∧ y⇩o)❙]"
  by auto

lemma wff_Imp_sym_subterm1_iff[simp]:
  "wff α ❙[x⇩o ❙=Tv❙= (x⇩o ❙∧ y⇩o)❙] ⟷ α = Tv"
  using unique_type wff_Imp_sym_subterm1 by blast

lemma wff_Imp_sym_subterm2[simp]:
  "wff oo ❙[❙λ ''y'':Tv. ❙[x⇩o ❙=Tv❙= (x⇩o ❙∧ y⇩o)❙]❙]"
  by auto

lemma wff_Imp_sym_subterm2_iff[simp]:
  "wff α ❙[❙λ ''y'':Tv. ❙[x⇩o ❙=Tv❙= (x⇩o ❙∧ y⇩o)❙]❙] ⟷ α = oo"
  by auto


subsection ‹Implication›

definition Imp :: "trm ⇒ trm ⇒ trm" (infix "❙⟶" 80) where
  "A ❙⟶ B = Imp_sym ❙⋅ A ❙⋅ B"

lemma wff_Imp[simp]: "wff Tv A ⟹ wff Tv B ⟹ wff Tv (A ❙⟶ B)"
  unfolding Imp_def by auto

lemma wff_Imp_iff[simp]: "wff α (A ❙⟶ B) ⟷ wff Tv A ∧ wff Tv B ∧ α = Tv"
  using Imp_def by auto


section ‹The Q0 proof system›

definition axiom_1 :: trm where
  "axiom_1 ≡ ❙[((g⇩o⇩o ❙⋅ T) ❙∧ (g⇩o⇩o ❙⋅ F)) ❙=Tv❙= ❙[❙∀''x'':Tv. g⇩o⇩o ❙⋅ x⇩o❙]❙]"

lemma wff_axiom_1[simp]: "wff Tv axiom_1"
  unfolding axiom_1_def by auto

definition axiom_2 :: "type_sym ⇒ trm" where
  "axiom_2 α ≡
       ❙[(Var ''x'' α) ❙=α❙= (Var ''y'' α)❙] ❙⟶
       ❙[((Var ''h'' (Tv ❙⇐ α)) ❙⋅ (Var ''x'' α)) ❙=Tv❙= ((Var ''h'' (Tv ❙⇐ α)) ❙⋅ (Var ''y'' α))❙]"

definition axiom_3 :: "type_sym ⇒ type_sym ⇒ trm" where
  "axiom_3 α β ≡
       ❙[❙[(Var ''f'' (α ❙⇐ β)) ❙=α ❙⇐ β❙= (Var ''g'' (α ❙⇐ β))❙] ❙=Tv❙=
       ❙[❙∀''x'':β. ❙[((Var ''f'' (α ❙⇐ β)) ❙⋅ (Var ''x'' β)) ❙=α❙= ((Var ''g'' (α ❙⇐ β)) ❙⋅ (Var ''x'' β))❙]❙]❙]"

definition axiom_4_1 :: "var_sym ⇒ type_sym ⇒ trm ⇒ type_sym ⇒ trm ⇒ trm" where
  "axiom_4_1 x α B β A ≡ ❙[(❙[❙λx:α. B❙] ❙⋅ A) ❙=β❙= B❙]"

definition axiom_4_1_side_condition :: "var_sym ⇒ type_sym ⇒ trm ⇒ type_sym ⇒ trm ⇒ bool" where
  "axiom_4_1_side_condition x α B β A ≡ (∃c. B = Cst c β) ∨ (∃y. B = Var y β ∧ (x ≠ y ∨ α ≠ β))"

definition axiom_4_2 :: "var_sym ⇒ type_sym ⇒ trm ⇒ trm" where
  "axiom_4_2 x α A = ❙[(❙[❙λx:α. Var x α❙] ❙⋅ A) ❙=α❙= A❙]"

definition axiom_4_3 :: "var_sym ⇒ type_sym ⇒ trm ⇒
                          type_sym ⇒ type_sym ⇒ trm ⇒ trm  ⇒ trm" where
  "axiom_4_3 x α B β γ C A = ❙[(❙[❙λx:α. B ❙⋅ C❙] ❙⋅ A) ❙=β❙= ((❙[❙λx:α. B❙] ❙⋅ A) ❙⋅ (❙[❙λx:α. C❙] ❙⋅ A))❙]"

definition axiom_4_4 :: "var_sym ⇒ type_sym ⇒ var_sym ⇒ type_sym ⇒ trm ⇒ type_sym ⇒ trm ⇒ trm" where
  "axiom_4_4 x α y γ B δ A = ❙[(❙[❙λx:α. ❙[❙λy:γ. B❙]❙] ❙⋅ A) ❙=δ ❙⇐ γ❙= ❙[❙λy:γ. ❙[❙λx:α. B❙] ❙⋅ A❙]❙]"

definition axiom_4_4_side_condition :: "var_sym ⇒ type_sym ⇒ var_sym ⇒ type_sym ⇒ trm ⇒ type_sym ⇒ trm ⇒ bool" where
  "axiom_4_4_side_condition x α y γ B δ A ≡ (x ≠ y ∨ α ≠ γ) ∧ (y, γ) ∉ vars A"

definition axiom_4_5 :: "var_sym ⇒ type_sym ⇒ trm ⇒ type_sym ⇒ trm ⇒ trm" where
  "axiom_4_5 x α B δ A = ❙[(❙[❙λx:α. ❙[❙λx:α. B❙]❙] ❙⋅ A) ❙=δ ❙⇐ α ❙= ❙[❙λx:α. B❙]❙]"

definition axiom_5 where
  "axiom_5 = ❙[(❙ι ❙⋅ ((❙Q (Tv ❙⇐ Ind ❙⇐ Ind)) ❙⋅ y⇩i)) ❙=Ind❙= y⇩i❙]"

inductive axiom :: "trm ⇒ bool" where
  by_axiom_1: 
  "axiom axiom_1"
| by_axiom_2: 
  "axiom (axiom_2 α)"
| by_axiom_3: 
  "axiom (axiom_3 α β)"
| by_axiom_4_1: 
  "wff α A ⟹
   wff β B ⟹
   axiom_4_1_side_condition x α B β A ⟹
   axiom (axiom_4_1 x α B β A)"
| by_axiom_4_2: 
  "wff α A ⟹
   axiom (axiom_4_2 x α A)"
| by_axiom_4_3: 
  "wff α A ⟹
   wff (β ❙⇐ γ) B ⟹
   wff γ C ⟹
   axiom (axiom_4_3 x α B β γ C A)"
| by_axiom_4_4: 
  "wff α A ⟹
   wff δ B ⟹
   axiom_4_4_side_condition x α y γ B δ A ⟹
   axiom (axiom_4_4 x α y γ B δ A)"
| by_axiom_4_5: 
  "wff α A ⟹
   wff δ B ⟹
   axiom (axiom_4_5 x α B δ A)"
| by_axiom_5: 
  "axiom (axiom_5)"

inductive rule_R :: "trm ⇒ trm ⇒ trm ⇒ bool" where
  "replacement A B C D ⟹ rule_R C (❙[A ❙=α❙= B❙]) D"

definition "proof" :: "trm ⇒ trm list ⇒ bool" where
  "proof A p ⟷ (p ≠ [] ∧ last p = A ∧
                    (∀i<length p. axiom (p ! i) 
                  ∨ (∃j<i. ∃k<i. rule_R (p ! j) (p ! k) (p ! i))))"

(* Peter Andrews defines theorems directly from "proof", here I instead define it as an inductive predicate based on rule_R *)
inductive "theorem" :: "trm ⇒ bool" where
  by_axiom: "axiom A ⟹ theorem A"
| by_rule_R: "theorem A ⟹ theorem B ⟹ rule_R A B C ⟹ theorem C"

(* Two variant formulations of axiom 4_1: *)
definition axiom_4_1_variant_cst :: "var_sym ⇒ type_sym ⇒ var_sym ⇒ type_sym ⇒ trm ⇒ trm" where
  "axiom_4_1_variant_cst x α c β A ≡ ❙[(❙[❙λx:α. Cst c β❙] ❙⋅ A) ❙=β❙= (Cst c β)❙]"

definition axiom_4_1_variant_var :: "var_sym ⇒ type_sym ⇒ var_sym ⇒ type_sym ⇒ trm ⇒ trm" where
  "axiom_4_1_variant_var x α y β A ≡  ❙[(❙[❙λx:α. Var y β❙] ❙⋅ A) ❙=β❙= Var y β❙]"

definition axiom_4_1_variant_var_side_condition :: "var_sym ⇒ type_sym ⇒ var_sym ⇒ type_sym ⇒ trm ⇒ bool" where
  "axiom_4_1_variant_var_side_condition x α y β A ≡ x ≠ y ∨ α ≠ β"


section ‹Semantics›

type_synonym 's frame = "type_sym ⇒ 's"

type_synonym 's denotation = "cst_sym ⇒ type_sym ⇒ 's"

type_synonym 's asg = "var_sym * type_sym ⇒ 's"

definition agree_off_asg :: "'s asg ⇒ 's asg ⇒ var_sym ⇒ type_sym ⇒ bool" where
  "agree_off_asg φ ψ x α ⟷ (∀y β. (y≠x ∨ β ≠ α) ⟶ φ (y,β) = ψ (y,β))"

lemma agree_off_asg_def2:
  "agree_off_asg ψ φ x α ⟷ (∃xa. φ((x, α) := xa) = ψ)"
  unfolding agree_off_asg_def by force

lemma agree_off_asg_disagree_var_sym[simp]:
  "agree_off_asg ψ φ x α ⟹ x ≠ y ⟹ ψ(y,β) = φ(y,β)"
  unfolding agree_off_asg_def by auto

lemma agree_off_asg_disagree_type_sym[simp]:
  "agree_off_asg ψ φ x α ⟹ α ≠ β ⟹ ψ(y,β) = φ(y,β)"
  unfolding agree_off_asg_def by auto


context set_theory
begin

definition wf_frame :: "'s frame ⇒ bool" where
  "wf_frame D ⟷ D Tv = boolset ∧ (∀α β. D (α ❙⇐ β) ⊆: funspace (D β) (D α)) ∧ (∀α. D α ≠ Ø)"

definition inds :: "'s frame ⇒ 's" where
  "inds Fr = Fr Ind"

inductive wf_interp :: "'s frame ⇒ 's denotation ⇒ bool" where
  "wf_frame D ⟹
   ∀c α. I c α ∈: D α ⟹
   ∀α. I ''Q'' (Tv ❙⇐ α ❙⇐ α) = iden (D α) ⟹
   (I ''i'' (Ind ❙⇐ (Tv ❙⇐ Ind))) ∈: funspace (D (Tv ❙⇐ Ind)) (D Ind) ⟹
   ∀x. x ∈: D Ind ⟶ (I ''i'' (Ind ❙⇐ (Tv ❙⇐ Ind))) ⋅ one_elem_fun x (D Ind) = x ⟹
   wf_interp D I"

definition asg_into_frame :: "'s asg ⇒ 's frame ⇒ bool" where
  "asg_into_frame φ D ⟷ (∀x α. φ (x, α) ∈: D α)"

abbreviation(input) asg_into_interp :: "'s asg ⇒ 's frame ⇒ 's denotation ⇒ bool" where
  "asg_into_interp φ D I ≡ asg_into_frame φ D"

(* Note that because Isabelle's HOL is total, val will also give values to trms that are not wffs *)
fun val :: "'s frame ⇒ 's denotation ⇒ 's asg ⇒ trm ⇒ 's" where
  "val D I φ (Var x α) = φ (x,α)"
| "val D I φ (Cst c α) = I c α"
| "val D I φ (A ❙⋅ B) = val D I φ A ⋅ val D I φ B"
| "val D I φ ❙[❙λx:α. B❙] = abstract (D α) (D (type_of B)) (λz. val D I (φ((x,α):=z)) B)"

fun general_model :: "'s frame ⇒ 's denotation ⇒ bool" where
  "general_model D I ⟷ wf_interp D I ∧ (∀φ A α. asg_into_interp φ D I ⟶ wff α A ⟶ val D I φ A ∈: D α)"

fun standard_model :: "'s frame ⇒ 's denotation ⇒ bool" where
  "standard_model D I ⟷ wf_interp D I ∧ (∀α β. D (α ❙⇐ β) = funspace (D β) (D α))"

lemma asg_into_frame_fun_upd:
  assumes "asg_into_frame φ D"
  assumes "xa ∈: D α"
  shows "asg_into_frame (φ((x, α) := xa)) D"
  using assms unfolding asg_into_frame_def by auto

lemma asg_into_interp_fun_upd:
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  assumes "wff α A"
  shows "asg_into_interp (φ((x, α) := val D I φ A)) D I"
  using assms asg_into_frame_fun_upd by auto

lemma standard_model_is_general_model: (* property mentioned on page 239 *)
  assumes "standard_model D I"
  shows "general_model D I" 
proof -
  have "wf_interp D I"
    using assms by auto
  moreover
  have "wff α A ⟹ asg_into_interp φ D I ⟹ val D I φ A ∈: D α" for φ α A
  proof (induction arbitrary: φ rule: wff.induct)
    case (wff_Var α uu)
    then show ?case
      unfolding asg_into_frame_def using assms by auto
  next
    case (wff_Cst α uv)
    then show ?case 
      using assms using wf_interp.simps by auto
  next
    case (wff_App α β A B)
    then show ?case
      using apply_in_rng assms by fastforce
  next
    case (wff_Abs β A α x)
    then show ?case 
      using assms abstract_in_funspace asg_into_frame_fun_upd by force
  qed
  ultimately
  have "general_model D I"
    unfolding general_model.simps by auto
  then show "general_model D I"
    by auto
qed

abbreviation agree_on_asg :: "'s asg ⇒ 's asg ⇒ var_sym ⇒ type_sym ⇒ bool" where
  "agree_on_asg φ ψ x α == (φ (x, α) = ψ (x, α))"

(* Corresponds to Andrews' proposition 5400 *)
proposition prop_5400:
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  assumes "asg_into_interp ψ D I"
  assumes "wff α A"
  assumes "∀(x,α) ∈ frees A. agree_on_asg φ ψ x α"
  shows "val D I φ A = val D I ψ A"
  using assms(4) assms(1-3,5)
proof (induction arbitrary: φ ψ rule: wff.induct)
  case (wff_Var α x)
  then show ?case by auto
next
  case (wff_Cst α c)
  then show ?case by auto
next
  case (wff_App α β A B)
  show ?case
    using wff_App(1,2,5,6,7,8) wff_App(3,4)[of φ ψ] by auto
next
  case (wff_Abs β A α x)
  have "abstract (D α) (D β) (λz. val D I (φ((x, α) := z)) A) = 
        abstract (D α) (D β) (λz. val D I (ψ((x, α) := z)) A)"
  proof (rule abstract_extensional, rule, rule)
    fix xa
    assume "xa ∈: D α"
    then have "val D I (φ((x, α) := xa)) A ∈: D β"
      using wff_Abs asg_into_frame_fun_upd by auto
    moreover
    {
      have "asg_into_frame (ψ((x, α) := xa)) D"
        using ‹xa ∈: D α› asg_into_frame_fun_upd wff_Abs by auto
      moreover
      have "asg_into_frame (φ((x, α) := xa)) D"
        using ‹xa ∈: D α› asg_into_frame_fun_upd wff_Abs by auto
      moreover
      have "(∀y∈frees A. (φ((x, α) := xa)) y = (ψ((x, α) := xa)) y)"
        using wff_Abs by auto
      ultimately
      have "val D I (φ((x, α) := xa)) A = val D I (ψ((x, α) := xa)) A"
        using assms wff_Abs by (smt case_prodI2) 
    }  
    ultimately
    show "val D I (φ((x, α) := xa)) A ∈: D β ∧ val D I (φ((x, α) := xa)) A = val D I (ψ((x, α) := xa)) A"
      by auto
  qed
  then show ?case
    using wff_Abs by auto 
qed

(* definitions on page 239 *)
abbreviation satisfies :: "'s frame ⇒ 's denotation ⇒ 's asg ⇒ trm ⇒ bool" where
  "satisfies D I φ A ≡ (val D I φ A = true)"

definition valid_in_model :: "'s frame ⇒ 's denotation ⇒ trm ⇒ bool" where
  "valid_in_model D I A ≡ (∀φ. asg_into_interp φ D I ⟶ val D I φ A = true)"

definition valid_general :: "trm ⇒ bool" where
  "valid_general A ≡ ∀D I. general_model D I ⟶ valid_in_model D I A"

definition valid_standard :: "trm ⇒ bool" where
  "valid_standard A ≡ ∀D I. standard_model D I ⟶ valid_in_model D I A"


section ‹Semantics of defined wffs›

(* Corresponds to Andrews' lemma 5401 a *)
lemma lemma_5401_a:
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  assumes "wff α A" "wff β B"
  shows "val D I φ (❙[❙λx:α. B❙] ❙⋅ A) = val D I (φ((x,α):=val D I φ A)) B"
proof -
  have val_A: "val D I φ A ∈: D α"
    using assms  by simp
  have "asg_into_interp (φ((x, α) := val D I φ A)) D I"
    using assms asg_into_frame_fun_upd  by force
  then have val_B: "val D I (φ((x, α) := val D I φ A)) B ∈: D β"
    using assms by simp

  have "val D I φ (❙[❙λx:α. B❙] ❙⋅ A) =
          (abstract (D α) (D β) (λz. val D I (φ((x, α) := z)) B)) ⋅ val D I φ A"
    using assms by auto
  also
  have "... = val D I (φ((x, α) := val D I φ A)) B"
    using apply_abstract val_A val_B by auto
  finally
  show ?thesis 
    by auto
qed

(* Corresponds to Andrews' lemma 5401 b *)
lemma lemma_5401_b_variant_1:
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  assumes "wff α A" "wff α B"
  shows "val D I φ (❙[A ❙=α❙= B❙]) = (boolean (val D I φ A = val D I φ B))"
proof -
  have "val D I φ (❙[A ❙=α❙= B❙]) = (I ''Q'' (Tv ❙⇐ α ❙⇐ α)) ⋅ val D I φ A ⋅ val D I φ B"
    unfolding Eql_def by auto
  have "... = (iden (D α)) ⋅ val D I φ A ⋅ val D I φ B"
    using assms general_model.simps wf_interp.simps by auto 
  also
  have "... = boolean (val D I φ A = val D I φ B)"
    using apply_id using assms general_model.simps by blast
  finally show ?thesis 
    unfolding Eql_def by simp
qed

(* Corresponds to Andrews' lemma 5401 b *)
lemma lemma_5401_b:
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  assumes "wff α A" "wff α B"
  shows "val D I φ (❙[A ❙=α❙= B❙]) = true ⟷ val D I φ A = val D I φ B"
  using lemma_5401_b_variant_1[OF assms] boolean_eq_true by auto

(* Corresponds to Andrews' lemma 5401 b *)
lemma lemma_5401_b_variant_2: ― ‹Just a reformulation of @{thm [source] lemma_5401_b}'s directions› 
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  assumes "wff α A" "wff α B"
  assumes "val D I φ A = val D I φ B"
  shows "val D I φ (❙[A ❙=α❙= B❙]) = true"
  using assms(5) lemma_5401_b[OF assms(1,2,3,4)] by auto 

(* Corresponds to Andrews' lemma 5401 b *)
lemma lemma_5401_b_variant_3: ― ‹Just a reformulation of @{thm [source] lemma_5401_b}'s directions› 
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  assumes "wff α A" "wff α B"
  assumes "val D I φ A ≠ val D I φ B"
  shows "val D I φ (❙[A ❙=α❙= B❙]) = false"
  using assms(5) lemma_5401_b_variant_1[OF assms(1,2,3,4)] by (simp add: boolean_def) 

(* Corresponds to Andrews' lemma 5401 c *)
lemma lemma_5401_c:
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  shows "val D I φ T = true"
  using assms lemma_5401_b[OF assms(1,2)] unfolding T_def by auto

(* Corresponds to Andrews' lemma 5401 d *)
lemma lemma_5401_d:
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  shows "val D I φ F = false"
proof -
  have "iden boolset ∈: D ooo"
    using assms general_model.simps wf_interp.simps wf_frame_def by metis
  then have "(val D I φ ❙[❙λ''x'':Tv. T❙]) ⋅ false ≠ (val D I φ ❙[❙λ''x'':Tv. x⇩o❙]) ⋅ false" 
    using assms wf_interp.simps wf_frame_def true_neq_false 
      apply_id[of "iden boolset" "(D ooo)" "iden boolset"]
    unfolding boolean_def Eql_def T_def by auto
  then have neqLR: "val D I φ ❙[❙λ''x'':Tv. T❙] ≠ val D I φ ❙[❙λ''x'':Tv. x⇩o❙]"
    by metis
  have "val D I φ F = boolean (val D I φ (❙[❙λ''x'':Tv. T❙]) = val D I φ ❙[❙λ''x'':Tv. x⇩o❙])"
    using lemma_5401_b_variant_1[OF assms(1,2), 
        of "oo" "(❙[❙λ''x'':Tv. T❙])" "❙[❙λ''x'':Tv. x⇩o❙]"] assms
    by auto
  also
  have "... = boolean False"
    using neqLR by auto
  also
  have "... = false"
    unfolding boolean_def by auto
  finally
  show ?thesis
    by auto
qed

lemma asg_into_interp_fun_upd_true:
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  shows "asg_into_interp (φ((x, Tv) := true)) D I"
  using asg_into_interp_fun_upd[OF assms wff_T, of x] lemma_5401_c[OF assms(1,2)] by auto

lemma asg_into_interp_fun_upd_false:
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  shows "asg_into_interp (φ((x, Tv) := false)) D I"
  using asg_into_interp_fun_upd[OF assms wff_F, of x] lemma_5401_d[OF assms] by auto

(* Corresponds to Andrews' lemma 5401 e_1 *)
lemma lemma_5401_e_1:
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  shows "(val D I φ Con_sym) ⋅ true ⋅ true = true"
proof -
  define φ' where "φ' ≡ φ((''x'',Tv) := val D I φ T)"
  define φ'' where "φ'' ≡ φ'((''y'',Tv) :=  val D I φ' T)"
  define φ''' where "φ''' ≡ λz. φ''((''g'', ooo) := z)"
  have φ'_asg_into: "asg_into_interp φ' D I"
    unfolding φ'_def using asg_into_interp_fun_upd[OF assms wff_T] by blast
  have φ''_asg_into: "asg_into_interp φ'' D I"
    unfolding φ''_def using asg_into_interp_fun_upd[OF assms(1) φ'_asg_into wff_T] by blast

  have "(val D I φ Con_sym) ⋅ true ⋅ true = val D I φ (Con_sym ❙⋅ T ❙⋅ T)"
    using lemma_5401_c[OF assms(1,2)] by auto
  also
  have "... = val D I φ (❙[❙λ''x'':Tv. ❙[❙λ''y'':Tv. ❙[❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] ❙=(Tv ❙⇐ ooo)❙= ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]❙]❙]❙] ❙⋅ T ❙⋅ T)"
    unfolding Con_sym_def by auto 
  also
  have "... = (val D I φ ((❙[❙λ''x'':Tv. ❙[❙λ''y'':Tv. ❙[❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] ❙=(Tv ❙⇐ ooo)❙= ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]❙]❙]❙] ❙⋅ T))) ⋅ val D I φ T"
    by simp
  also
  have "... = (val D I (φ((''x'',Tv) := val D I φ T)) ((❙[❙λ''y'':Tv. ❙[❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] ❙=(Tv ❙⇐ ooo)❙= ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]❙]❙]))) ⋅ val D I φ T"
    by (metis lemma_5401_a[OF assms(1,2)] wff_Con_sym_subterm2 wff_T)
  also
  have "... = (val D I φ' ((❙[❙λ''y'':Tv. ❙[❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] ❙=(Tv ❙⇐ ooo)❙= ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]❙]❙]))) ⋅ val D I φ T"
    unfolding φ'_def ..
  also
  have "... = (val D I φ' ((❙[❙λ''y'':Tv. ❙[❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] ❙=(Tv ❙⇐ ooo)❙= ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]❙]❙]))) ⋅ val D I φ' T"
    using φ'_asg_into assms(2) lemma_5401_c[OF assms(1)] by auto
  also
  have "... = (val D I φ' (❙[❙λ''y'':Tv. ❙[❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] ❙=(Tv ❙⇐ ooo)❙= ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]❙]❙] ❙⋅ T))"
    by simp
  also
  have "... = (val D I (φ'((''y'',Tv) :=  val D I φ' T)) (❙[❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] ❙=(Tv ❙⇐ ooo)❙= ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]❙]))"
    by (meson φ'_asg_into assms(1) lemma_5401_a[OF assms(1)] wff_Con_sym_subterm1 wff_T)
  also
  have "... = (val D I φ'' (❙[❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] ❙=(Tv ❙⇐ ooo)❙= ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]❙]))"
    unfolding φ''_def ..
  also
  have "... = true"
  proof (rule lemma_5401_b_variant_2[OF assms(1)])
    show "wff (Tv ❙⇐ ooo) ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙]"
      by auto
  next
    show "wff (Tv ❙⇐ ooo) ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]"
      by auto
  next
    show "asg_into_frame φ'' D"
      using φ''_asg_into by blast
  next
    have "val D I φ'' ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] = abstract (D ooo) (D Tv)
                  (λz. val D I (φ''((''g'', ooo) := z)) 
                     (g⇩o⇩o⇩o ❙⋅ T ❙⋅ T))"
      by (simp only: val.simps(4) type_of.simps type_sym.case)
    also
    have "... = abstract (D ooo) (D Tv) 
                  (λz. val D I (φ''' z) (g⇩o⇩o⇩o ❙⋅ T ❙⋅ T))"
      unfolding φ'''_def ..
    also
    have "... = abstract (D ooo) (D Tv) 
                  (λz. val D I (φ''' z) g⇩o⇩o⇩o ⋅ val D I (φ''' z) T
                     ⋅ val D I (φ''' z) T)"
      unfolding val.simps(3) ..
    also
    have "... = abstract (D ooo) (D Tv) 
                  (λz. val D I (φ''' z) g⇩o⇩o⇩o ⋅ true ⋅ true)"
    proof (rule abstract_extensional')
      fix x
      assume "x ∈: D ooo"
      then have "val D I (φ''' x) (g⇩o⇩o⇩o ❙⋅ T ❙⋅ T) ∈: D Tv"
        using φ'''_def φ''_asg_into asg_into_frame_fun_upd assms(1) 
          general_model.elims(2) type_sym.inject wff_Abs_type_of wff_Con_sym_subterm0 wff_T 
        by (metis wff_App wff_Var)
      then show "val D I (φ''' x) g⇩o⇩o⇩o ⋅ val D I (φ''' x) T ⋅
                   val D I (φ''' x) T
                 ∈: D Tv"
        by simp
    next
      fix x
      assume "x ∈: D ooo"
      then have "val D I (φ''' x) T = true"
        unfolding φ'''_def using  φ''_asg_into asg_into_frame_fun_upd 
          lemma_5401_c[OF assms(1)] by blast
      then show "val D I (φ''' x) g⇩o⇩o⇩o ⋅ val D I (φ''' x) T ⋅
                   val D I (φ''' x) T =
                 val D I (φ''' x) g⇩o⇩o⇩o ⋅ true ⋅ true" by auto
    qed
    also
    have "... = abstract (D ooo) (D Tv) 
                  (λz. val D I (φ''' z) g⇩o⇩o⇩o ⋅
                         val D I (φ''' z) x⇩o ⋅ val D I (φ''' z) y⇩o)"
    proof (rule abstract_extensional')
      fix x
      assume x_in_D: "x ∈: D ooo"
      then have "val D I (φ''' x) (g⇩o⇩o⇩o ❙⋅ T ❙⋅ T) ∈: D Tv"
        using φ'''_def φ''_asg_into asg_into_frame_fun_upd assms(1) 
          general_model.elims(2) type_sym.inject wff_Abs_type_of wff_Con_sym_subterm0 wff_T 
        by (metis wff_App wff_Var)
      then have "val D I (φ''' x) g⇩o⇩o⇩o ⋅ val D I (φ''' x) T ⋅
                   val D I (φ''' x) T ∈: D Tv"
        by simp
      then show "val D I (φ''' x) g⇩o⇩o⇩o ⋅ true ⋅ true ∈: D Tv"
        by (metis φ'''_def φ''_asg_into lemma_5401_c[OF assms(1)] asg_into_frame_fun_upd x_in_D)
    next
      fix x
      assume x_in_D: "x ∈: D ooo"
      then have "val D I (φ''' x) x⇩o = true"
        unfolding φ'''_def φ''_def φ'_def using lemma_5401_c[OF assms(1,2)] by auto
      moreover
      from x_in_D have "val D I (φ''' x) y⇩o = true"
        unfolding φ'''_def φ''_def using φ'_asg_into lemma_5401_c[OF assms(1)] by auto
      ultimately
      show "val D I (φ''' x) g⇩o⇩o⇩o ⋅ true ⋅ true =
        val D I (φ''' x)
          g⇩o⇩o⇩o ⋅
            val D I (φ''' x) x⇩o ⋅ val D I (φ''' x) y⇩o" 
        by auto
    qed
    also
    have "... = abstract (D ooo) (D Tv) (λz. val D I (φ''' z)
                  (g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o))"
      unfolding val.simps(3) ..
    also
    have "... = abstract (D ooo) (D Tv)
                  (λz. val D I (φ''((''g'', ooo) := z)) 
                         (g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o))"
      unfolding φ'''_def ..
    also
    have "... = val D I φ'' ❙[❙λ''g'':ooo.
                                g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]"
      by (simp only: val.simps(4) type_of.simps type_sym.case)
    finally
    show "val D I φ'' ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] = val D I φ'' ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]" 
      .
  qed
  finally show ?thesis .
qed

(* Corresponds to Andrews' lemma 5401 e_2 *)
lemma lemma_5401_e_2:
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  assumes "y = true ∨ y = false"
  shows "(val D I φ Con_sym) ⋅ false ⋅ y = false"
proof -
  define give_x :: trm where "give_x = ❙[❙λ''y'':Tv. x⇩o❙]"
  define give_fst :: trm where "give_fst = ❙[❙λ ''x'':Tv. give_x❙]"
  define val_give_fst :: 's where "val_give_fst = val D I φ give_fst"
  have wff_give_x: "wff oo give_x"
    unfolding give_x_def by auto

  have "⋀a b. a ∈: D Tv ⟹ 
               b ∈: D Tv ⟹ 
               val D I (φ((''x'', Tv) := a)) give_x ∈: D (type_of give_x)"
    using wff_give_x asg_into_frame_def assms(1,2) by auto
  moreover
  have "⋀a b. a ∈: D Tv ⟹ b ∈: D Tv ⟹ val D I (φ((''x'', Tv) := a)) give_x ⋅ b = a"
    unfolding give_x_def by auto
  ultimately
  have "⋀a b. a ∈: D Tv ⟹
               b ∈: D Tv ⟹ 
               abstract (D Tv) (D (type_of give_x)) (λz. val D I (φ((''x'', Tv) := z)) give_x) ⋅ a ⋅ b
               = a"
    by auto
  then have val_give_fst_simp: "⋀a b. a ∈: D Tv ⟹ b ∈: D Tv ⟹ val_give_fst ⋅ a ⋅ b = a"
    unfolding val_give_fst_def give_fst_def by auto

  have wff_give_fst: "wff ooo give_fst"
    unfolding give_fst_def give_x_def by auto
  then have val_give_fst_fun: "val_give_fst ∈: D ooo"
    unfolding val_give_fst_def using assms by auto

  have "val D I (φ((''x'', Tv) := false, 
                   (''y'', Tv) := y, 
                   (''g'', ooo) := val_give_fst)) T ∈: D Tv"
    by (smt Pair_inject wff_give_fst assms(1,2,3) fun_upd_twist general_model.simps
        asg_into_interp_fun_upd[OF assms(1,2)] asg_into_interp_fun_upd_true[OF assms(1)] 
        asg_into_interp_fun_upd_false[OF assms(1)] type_sym.distinct(5) val_give_fst_def wff_T)
  then have val_give_fst_D:
    "val_give_fst ⋅ val D I (φ((''x'', Tv) := false, 
                               (''y'', Tv) := y, 
                               (''g'', ooo) := val_give_fst)) T ⋅
                      val D I (φ((''x'', Tv) := false, 
                               (''y'', Tv) := y, 
                               (''g'', ooo) := val_give_fst)) T
       ∈: D Tv"
    using val_give_fst_simp[of
        "val D I (φ((''x'', Tv) := false, 
                    (''y'', Tv) := y, 
                    (''g'', ooo) := val_give_fst)) T" 
        "val D I (φ((''x'', Tv) := false, 
                     (''y'', Tv) := y, 
                     (''g'', ooo) := val_give_fst)) T" ]
    by auto

  have false_y_TV: "false ∈: D Tv ∧ y ∈: D Tv"
    using assms(1) assms(3) wf_frame_def wf_interp.simps by auto
  then have val_give_fst_in_D: "val_give_fst ⋅ false ⋅ y ∈: D Tv"
    using val_give_fst_simp by auto

  have "true ∈: D Tv"
    by (metis assms(1) assms(2) general_model.simps lemma_5401_c[OF assms(1,2)] wff_T)
  from this val_give_fst_in_D false_y_TV have "val_give_fst ⋅ true ⋅ true ≠ val_give_fst ⋅ false ⋅ y"
    using val_give_fst_simp true_neq_false by auto
  then have val_give_fst_not_false: 
    "val_give_fst ⋅ val D I (φ((''x'', Tv) := false, 
                             (''y'', Tv) := y, 
                             (''g'', ooo) := val_give_fst)) T
                  ⋅ val D I (φ((''x'', Tv) := false, 
                             (''y'', Tv) := y, 
                             (''g'', ooo) := val_give_fst)) T 
     ≠ val_give_fst ⋅ false ⋅ y"
    using asg_into_frame_fun_upd assms(1) assms(2) lemma_5401_c false_y_TV val_give_fst_fun by auto
  have Con_sym_subterm0TT_neq_Con_sym_subterm0xy: 
    "val D I (φ((''x'', Tv) := false, (''y'', Tv) := y)) ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] ≠ 
     val D I (φ((''x'', Tv) := false, (''y'', Tv) := y)) ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]"
    using abstract_cong_specific[of
        val_give_fst
        "(D ooo)" 
        "(λz. z ⋅ val D I (φ((''x'', Tv) := false, 
                           (''y'', Tv) := y, 
                           (''g'', ooo) := z)) T
                 ⋅ val D I (φ((''x'', Tv) := false, 
                            (''y'', Tv) := y, 
                            (''g'', ooo) := z)) T)" 
        "(D Tv)"
        "(λz. z ⋅ false ⋅ y)"]
    using val_give_fst_fun val_give_fst_D val_give_fst_in_D val_give_fst_not_false by auto

  have "asg_into_frame (φ((''x'', Tv) := false, (''y'', Tv) := y)) D"
    using asg_into_interp_fun_upd_false[OF assms(1)] general_model.simps[of D I] assms wff_Con_sym_subterm1
      asg_into_interp_fun_upd_true[OF assms(1)] by auto
  then have val_Con_sym_subterm1: "val D I (φ((''x'', Tv) := false, (''y'', Tv) := y)) ❙[❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] ❙=(Tv ❙⇐ ooo)❙= ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]❙] = false"
    using Con_sym_subterm0TT_neq_Con_sym_subterm0xy lemma_5401_b_variant_3[OF assms(1)] 
    by auto

  have "y ∈: D Tv"
    using general_model.simps lemma_5401_d[OF assms(1,2)] wff_F assms
    by (metis lemma_5401_c[OF assms(1,2)] wff_T) 
  moreover
  have "val D I (φ((''x'', Tv) := false, (''y'', Tv) := y)) ❙[❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] ❙=(Tv ❙⇐ ooo)❙= ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]❙] ∈: D Tv"
    using asg_into_interp_fun_upd_false[OF assms(1)] general_model.simps[of D I] assms wff_Con_sym_subterm1 
      asg_into_interp_fun_upd_true[OF assms(1)] by auto
  moreover
  have "val D I (φ((''x'', Tv) := false, (''y'', Tv) := y)) ❙[❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] ❙=(Tv ❙⇐ ooo)❙= ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]❙] = false"
    using val_Con_sym_subterm1 by auto
  ultimately
  have val_y: "(val D I (φ((''x'', Tv) := false)) ❙[❙λ ''y'':Tv. ❙[❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] ❙=(Tv ❙⇐ ooo)❙= ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]❙]❙]) ⋅ y = false"
    by simp

  have 11: "val D I (φ((''x'', Tv) := false)) ❙[❙λ ''y'':Tv. ❙[❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] ❙=(Tv ❙⇐ ooo)❙= ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]❙]❙] ∈: D oo"
    using asg_into_interp_fun_upd_false[OF assms(1,2)] general_model.simps[of D I] assms
      wff_Con_sym_subterm2 by blast 
  moreover
  have "val D I (φ((''x'', Tv) := false)) ❙[❙λ ''y'':Tv. ❙[❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] ❙=(Tv ❙⇐ ooo)❙= ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]❙]❙] ⋅ y = false"
    using val_y by auto
  ultimately
  have "(val D I φ ❙[❙λ''x'':Tv. ❙[❙λ ''y'':Tv. ❙[❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] ❙=(Tv ❙⇐ ooo)❙= ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]❙]❙]❙]) ⋅ false ⋅ y = false"
    using false_y_TV by simp
  then show "(val D I φ Con_sym) ⋅ false ⋅ y = false"
    unfolding Con_sym_def by auto
qed

(* Corresponds to Andrews' lemma 5401 e_3 *)
lemma lemma_5401_e_3:
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  assumes "x = true ∨ x = false"
  shows "(val D I φ Con_sym) ⋅ x ⋅ false = false"
proof -
  (* proof adapted from lemma_5401_e_2 *)
  define give_y :: trm where "give_y = (❙[❙λ ''y'':Tv. y⇩o❙])"
  define give_snd :: trm where "give_snd = ❙[❙λ ''x'':Tv. give_y❙]"
  define val_give_snd :: 's where "val_give_snd = val D I φ give_snd"
  have wff_give_y: "wff oo give_y"
    unfolding give_y_def by auto

  have  "⋀a b. a ∈: D Tv ⟹ b ∈: D Tv ⟹ a ∈: D Tv"
    by simp
  moreover
  have "⋀a b. a ∈: D Tv ⟹ b ∈: D Tv ⟹ val D I (φ((''x'', Tv) := a)) give_y ∈: D (type_of give_y)"
    using wff_give_y asg_into_frame_def assms(1) assms(2) by auto
  moreover
  have "⋀a b. a ∈: D Tv ⟹ b ∈: D Tv ⟹ val D I (φ((''x'', Tv) := a)) give_y ⋅ b = b"
    unfolding give_y_def by auto
  ultimately
  have val_give_snd_simp: "⋀a b. a ∈: D Tv ⟹ b ∈: D Tv ⟹ val_give_snd ⋅ a ⋅ b = b"
    unfolding val_give_snd_def give_snd_def by auto

  have wff_give_snd: "wff ooo give_snd"
    unfolding give_snd_def give_y_def by auto
  then have val_give_snd_in_D: "val_give_snd ∈: D ooo"
    unfolding val_give_snd_def using assms
    by auto

  then have "val D I (φ((''x'', Tv) := x, 
                   (''y'', Tv) := false, 
                   (''g'', ooo) := val_give_snd)) T ∈: D Tv"
    by (smt Pair_inject wff_give_snd assms(1,2,3) 
        fun_upd_twist general_model.simps asg_into_interp_fun_upd[OF assms(1,2)] 
        asg_into_interp_fun_upd_false[OF assms(1)] asg_into_interp_fun_upd_true[OF assms(1)] 
        type_sym.distinct(5) val_give_snd_def wff_T)
  then have val_give_snd_app_in_D: 
    "val_give_snd ⋅ val D I (φ((''x'', Tv) := x, 
                             (''y'', Tv) := false, 
                             (''g'', ooo) := val_give_snd)) T
                  ⋅ val D I (φ((''x'', Tv) := x, 
                             (''y'', Tv) := false, 
                             (''g'', ooo) := val_give_snd)) T
     ∈: D Tv"
    using val_give_snd_simp[of
        "val D I (φ((''x'', Tv) := x, 
                    (''y'', Tv) := false, 
                    (''g'', ooo) := val_give_snd)) T" 
        "val D I (φ((''x'', Tv) := x, 
                     (''y'', Tv) := false, 
                     (''g'', ooo) := val_give_snd)) T" ]
    by auto

  have false_and_x_in_D: "false ∈: D Tv ∧ x ∈: D Tv"
    using assms(1,3) wf_frame_def wf_interp.simps by auto
  then have val_give_snd_app_x_false_in_D: "val_give_snd ⋅ x ⋅ false ∈: D Tv"
    using val_give_snd_simp by auto

  have "true ∈: D Tv"
    by (metis assms(1) assms(2) general_model.simps lemma_5401_c[OF assms(1,2)] wff_T)
  then have "val_give_snd ⋅ true ⋅ true ≠ val_give_snd ⋅ x ⋅ false"
    using val_give_snd_simp true_neq_false val_give_snd_app_in_D false_and_x_in_D by auto
  then have
    "val_give_snd ⋅ val D I (φ((''x'', Tv) := x, 
                             (''y'', Tv) := false, 
                             (''g'', ooo) := val_give_snd)) T
                  ⋅ val D I (φ((''x'', Tv) := x, 
                             (''y'', Tv) := false, 
                             (''g'', ooo) := val_give_snd)) T ≠
     val_give_snd ⋅ x ⋅ false"
    using asg_into_frame_fun_upd assms(1) assms(2) lemma_5401_c false_and_x_in_D val_give_snd_in_D
    by auto
  then have "val D I (φ((''x'', Tv) := x, (''y'', Tv) := false)) ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] ≠ 
        val D I (φ((''x'', Tv) := x, (''y'', Tv) := false)) 
          ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]"
    using abstract_cong_specific[of 
        val_give_snd 
        "(D ooo)" 
        "(λz. z ⋅ val D I (φ((''x'', Tv) := x, (''y'', Tv) := false, (''g'', ooo) := z))
             T ⋅ val D I (φ((''x'', Tv) := x, (''y'', Tv) := false, (''g'', ooo) := z)) T)" 
        "(D Tv)"
        "(λz. z ⋅ x ⋅ false)"
        ]
    using val_give_snd_in_D val_give_snd_app_x_false_in_D val_give_snd_app_in_D by auto
  then have "val D I (φ((''x'', Tv) := x, (''y'', Tv) := false)) ❙[❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] ❙=(Tv ❙⇐ ooo)❙= ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]❙] = false"
    using asg_into_frame_fun_upd assms(1,2) lemma_5401_b_variant_3 false_and_x_in_D by auto
  then have val_Con_sym_subterm2_false: "(val D I (φ((''x'', Tv) := x)) ❙[❙λ ''y'':Tv. ❙[❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] ❙=(Tv ❙⇐ ooo)❙= ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]❙]❙]) ⋅ false = false"
    using false_and_x_in_D by simp

  have "x ∈: D Tv"
    by (simp add: false_and_x_in_D)
  moreover
  have "val D I (φ((''x'', Tv) := x)) ❙[❙λ ''y'':Tv. ❙[❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] ❙=(Tv ❙⇐ ooo)❙= ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]❙]❙] ∈: D oo"
    by (metis assms(1,3) general_model.simps lemma_5401_c[OF assms(1,2)] 
        asg_into_interp_fun_upd[OF assms(1,2)] asg_into_interp_fun_upd_false[OF assms(1,2)] 
        wff_Con_sym_subterm2 wff_T)
  moreover
  have "val D I (φ((''x'', Tv) := x)) ❙[❙λ ''y'':Tv. ❙[❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] ❙=(Tv ❙⇐ ooo)❙= ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]❙]❙] ⋅ false = false"
    using val_Con_sym_subterm2_false by auto
  ultimately
  have "(val D I φ ❙[❙λ''x'':Tv. ❙[❙λ ''y'':Tv. ❙[❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ T ❙⋅ T❙] ❙=(Tv ❙⇐ ooo)❙= ❙[❙λ''g'':ooo. g⇩o⇩o⇩o ❙⋅ x⇩o ❙⋅ y⇩o❙]❙]❙]❙]) ⋅ x ⋅ false = false"
    by auto
  then show "(val D I φ Con_sym) ⋅ x ⋅ false = false"
    unfolding Con_sym_def by auto
qed

(* Corresponds to Andrews' lemma 5401 e *)
lemma lemma_5401_e_variant_1:
  assumes "asg_into_interp φ D I"
  assumes "general_model D I"
  assumes "y = true ∨ y = false"
  assumes "x = true ∨ x = false"
  shows "(val D I φ Con_sym) ⋅ x ⋅ y = boolean (x = true ∧ y = true)"
proof (cases "y = true")
  case True
  note True_outer = this
  then show ?thesis
  proof (cases "x = true")
    case True
    then show ?thesis
      using True_outer assms lemma_5401_e_1 unfolding boolean_def by auto
  next
    case False
    then show ?thesis
      using True_outer assms  lemma_5401_e_2 unfolding boolean_def by auto
  qed
next
  case False
  note False_outer = this
  then show ?thesis 
  proof (cases "x = true")
    case True
    then show ?thesis
      using False_outer assms lemma_5401_e_3 unfolding boolean_def by auto
  next
    case False
    then show ?thesis
      using False_outer assms lemma_5401_e_2 unfolding boolean_def by auto
  qed
qed

lemma asg_into_interp_is_true_or_false:
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  shows "φ (x, Tv) = true ∨ φ (x, Tv) = false"
proof -
  have "wff Tv (Var x Tv)"
    by auto
  then have "val D I φ (Var x Tv) ∈: D Tv"
    using assms general_model.simps by blast
  then have "val D I φ (Var x Tv) ∈: boolset"
    using assms unfolding general_model.simps wf_interp.simps wf_frame_def by auto
  then show ?thesis
    using mem_boolset by simp 
qed

lemma wff_Tv_is_true_or_false:
  assumes "asg_into_interp φ D I"
  assumes "general_model D I"
  assumes "wff Tv A"
  shows "val D I φ A = true ∨ val D I φ A = false"
proof -
  have "val D I φ A ∈: D Tv"
    using assms by auto
  then have "val D I φ A ∈: boolset"
    using assms unfolding general_model.simps wf_interp.simps wf_frame_def by force
  then show ?thesis
    using mem_boolset by blast
qed

(* Corresponds to Andrews' lemma 5401 e *)
lemma lemma_5401_e_variant_2:
  assumes "asg_into_interp φ D I"
  assumes "general_model D I"
  assumes "wff Tv A"
  assumes "wff Tv B"
  shows "(val D I φ (A ❙∧ B)) = boolean (satisfies D I φ A ∧ satisfies D I φ B)"
  using assms wff_Tv_is_true_or_false[of φ D I] lemma_5401_e_variant_1 unfolding Con_def by auto

(* Corresponds to Andrews' lemma 5401 f_1 *)
lemma lemma_5401_f_1:
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  assumes "y = true ∨ y = false"
  shows "(val D I φ Imp_sym) ⋅ false ⋅ y = true"
proof -
  define Imp_subterm2 :: trm where
    "Imp_subterm2 ≡ ❙[❙λ ''y'':Tv. ❙[x⇩o ❙=Tv❙= (x⇩o ❙∧ y⇩o)❙]❙]"

  have val_Imp_subterm0_false: "val D I (φ((''x'', Tv) := false, (''y'', Tv) := y)) (x⇩o ❙∧ y⇩o) = false"
    using assms asg_into_interp_fun_upd_false[OF assms(1)] asg_into_interp_fun_upd_true[OF assms(1)] 
      boolean_def lemma_5401_e_variant_2 by auto

  have "asg_into_frame (φ((''x'', Tv) := false, (''y'', Tv) := y)) D"
    using assms(1, 2, 3) lemma_5401_c[OF assms(1)] asg_into_interp_fun_upd wff_T
      asg_into_interp_fun_upd_false by metis
  then have "val D I (φ((''x'', Tv) := false, (''y'', Tv) := y)) ❙[x⇩o ❙=Tv❙= (x⇩o ❙∧ y⇩o)❙] = true"
    using lemma_5401_b_variant_1[OF assms(1)] val_Imp_subterm0_false unfolding boolean_def by auto
  then have val_Imp_subterm2_true: "(val D I (φ((''x'', Tv) := false)) ❙[❙λ ''y'':Tv. ❙[x⇩o ❙=Tv❙= (x⇩o ❙∧ y⇩o)❙]❙]) ⋅ y = true"
    using assms(1,3) wf_frame_def wf_interp.simps by auto 

  have "val D I φ ❙[❙λ ''x'':Tv. ❙[❙λ ''y'':Tv. ❙[x⇩o ❙=Tv❙= (x⇩o ❙∧ y⇩o)❙]❙]❙] ⋅ false ⋅ y = true"
  proof -
    have "false ∈: D Tv"
      by (metis asg_into_frame_def asg_into_interp_fun_upd_false assms(1) assms(2) fun_upd_same)
    then have "val D I (φ((''x'', Tv) := false)) ❙[❙λ ''y'':Tv. ❙[x⇩o ❙=Tv❙= (x⇩o ❙∧ y⇩o)❙]❙] = val D I φ ❙[❙λ''x'':Tv. ❙[❙λ ''y'':Tv. ❙[x⇩o ❙=Tv❙= (x⇩o ❙∧ y⇩o)❙]❙]❙] ⋅ false"
      using asg_into_interp_fun_upd_false assms(1,2) Imp_subterm2_def[symmetric] wff_Imp_sym_subterm2_iff by force
    then show ?thesis
      by (metis val_Imp_subterm2_true)
  qed
  then show "(val D I φ Imp_sym) ⋅ false ⋅ y = true"
    unfolding Imp_sym_def Imp_subterm2_def by auto
qed

(* Corresponds to Andrews' lemma 5401 f_2 *)
lemma lemma_5401_f_2:
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  assumes "x = true ∨ x = false"
  shows "(val D I φ Imp_sym) ⋅ x ⋅ true = true"
proof -
  have asg: "asg_into_frame (φ((''x'', Tv) := x, (''y'', Tv) := true)) D"
    using assms(1,2,3) asg_into_interp_fun_upd_false asg_into_interp_fun_upd_true[OF assms(1)] by blast
  then have "val D I (φ((''x'', Tv) := x, (''y'', Tv) := true)) (x⇩o ❙∧ y⇩o) = x"
    using lemma_5401_e_variant_2 assms unfolding boolean_def by auto
  then have val_Imp_subterm1_true: "val D I (φ((''x'', Tv) := x, (''y'', Tv) := true)) ❙[x⇩o ❙=Tv❙= (x⇩o ❙∧ y⇩o)❙] = true"
    using asg lemma_5401_b_variant_1[OF assms(1)] boolean_eq_true  by auto 

  have val_Imp_subterm2_true: "val D I (φ((''x'', Tv) := x)) ❙[❙λ ''y'':Tv. ❙[x⇩o ❙=Tv❙= (x⇩o ❙∧ y⇩o)❙]❙] ⋅ true = true"
    using val_Imp_subterm1_true assms(1) wf_frame_def wf_interp.simps by auto 

  have "x ∈: D Tv"
    by (metis asg_into_frame_def assms(1) assms(3) fun_upd_same asg_into_interp_fun_upd_false 
        asg_into_interp_fun_upd_true[OF assms(1,2)])
  moreover
  have "val D I (φ((''x'', Tv) := x)) ❙[❙λ ''y'':Tv. ❙[x⇩o ❙=Tv❙= (x⇩o ❙∧ y⇩o)❙]❙] ∈: D oo"
    using wff_Imp_sym_subterm2
    by (metis assms(1,2,3) general_model.simps lemma_5401_c[OF assms(1,2)]
        asg_into_interp_fun_upd[OF assms(1,2)] asg_into_interp_fun_upd_false wff_T)
  ultimately
  have "(val D I φ ❙[❙λ''x'':Tv. ❙[❙λ ''y'':Tv. ❙[x⇩o ❙=Tv❙= (x⇩o ❙∧ y⇩o)❙]❙]❙]) ⋅ x ⋅ true = true"
    using val_Imp_subterm2_true by auto
  then show "(val D I φ Imp_sym) ⋅ x ⋅ true = true"
    unfolding Imp_sym_def by auto
qed

(* Corresponds to Andrews' lemma 5401 f_3 *)
lemma lemma_5401_f_3:
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  shows "(val D I φ Imp_sym) ⋅ true ⋅ false = false"
proof -
  have asg: "asg_into_frame (φ((''x'', Tv) := true, (''y'', Tv) := false)) D"
    by (meson assms(1,2) asg_into_interp_fun_upd_false asg_into_interp_fun_upd_true)
  moreover
  have "false = true ∨ false = false"
    unfolding boolean_def by auto
  moreover
  have "boolean (true = true ∧ false = true) = false"
    unfolding boolean_def by auto
  ultimately
  have 3: "val D I (φ((''x'', Tv) := true, (''y'', Tv) := false)) (x⇩o ❙∧ y⇩o) = false"
    using lemma_5401_e_variant_2 assms by auto
  then have Imp_subterm1_false: "val D I (φ((''x'', Tv) := true, (''y'', Tv) := false)) ❙[x⇩o ❙=Tv❙= (x⇩o ❙∧ y⇩o)❙] = false"
    using subst lemma_5401_b_variant_1[OF assms(1)] asg boolean_def by auto

  have asdff: "wff Tv ❙[x⇩o ❙=Tv❙= (x⇩o ❙∧ y⇩o)❙]"
    by auto

  have false_Tv: "false ∈: D Tv"
    using assms(1) wf_frame_def wf_interp.simps by auto
  moreover
  have "val D I (φ((''x'', Tv) := true, (''y'', Tv) := false)) ❙[x⇩o ❙=Tv❙= (x⇩o ❙∧ y⇩o)❙] ∈: D Tv"
    by (simp add: Imp_subterm1_false false_Tv)
  moreover
  have "val D I (φ((''x'', Tv) := true, (''y'', Tv) := false)) ❙[x⇩o ❙=Tv❙= (x⇩o ❙∧ y⇩o)❙] = false"
    using Imp_subterm1_false by auto
  ultimately 
  have Imp_subterm2_app_false: "val D I (φ((''x'', Tv) := true)) ❙[❙λ ''y'':Tv. ❙[x⇩o ❙=Tv❙= (x⇩o ❙∧ y⇩o)❙]❙] ⋅ false = false"
    by auto

  have wff_Imp_sym_subterm2: "wff oo ❙[❙λ ''y'':Tv. ❙[x⇩o ❙=Tv❙= (x⇩o ❙∧ y⇩o)❙]❙]"
    by auto

  have "(val D I φ ❙[❙λ ''x'':Tv. ❙[❙λ ''y'':Tv. ❙[x⇩o ❙=Tv❙= (x⇩o ❙∧ y⇩o)❙]❙]❙]) ⋅ true ⋅ false = false"
  proof -
    have "true ∈: D Tv"
      by (metis assms(1) assms(2) general_model.simps lemma_5401_c[OF assms(1,2)] wff_T)
    moreover
    have "val D I (φ((''x'', Tv) := true)) ❙[❙λ ''y'':Tv. ❙[x⇩o ❙=Tv❙= (x⇩o ❙∧ y⇩o)❙]❙] ∈: D oo"
      using wff_Imp_sym_subterm2 
      by (metis assms(1) general_model.simps asg_into_interp_fun_upd_true[OF assms(1,2)])
    moreover
    have "val D I (φ((''x'', Tv) := true)) ❙[❙λ ''y'':Tv. ❙[x⇩o ❙=Tv❙= (x⇩o ❙∧ y⇩o)❙]❙] ⋅ false = false"
      using Imp_subterm2_app_false by auto
    ultimately
    show ?thesis
      by auto
  qed
  then show "(val D I φ Imp_sym) ⋅ true ⋅ false = false"
    unfolding Imp_sym_def by auto
qed

(* Corresponds to Andrews' lemma 5401 f *)
lemma lemma_5401_f_variant_1:
  assumes "asg_into_interp φ D I"
  assumes "general_model D I"
  assumes "x = true ∨ x = false"
  assumes "y = true ∨ y = false"
  shows "(val D I φ Imp_sym) ⋅ x ⋅ y = boolean (x = true ⟶ y = true)"
proof (cases "y = true")
  case True
  note True_outer = this
  then show ?thesis
  proof (cases "x = true")
    case True
    then show ?thesis
      using True_outer assms lemma_5401_f_2 unfolding boolean_def by auto
  next
    case False
    then show ?thesis
      using True_outer assms  lemma_5401_f_2 unfolding boolean_def by auto
  qed
next
  case False
  note False_outer = this
  then show ?thesis 
  proof (cases "x = true")
    case True
    then show ?thesis
      using False_outer assms lemma_5401_f_3 unfolding boolean_def by auto
  next
    case False
    then show ?thesis
      using False_outer assms lemma_5401_f_1 unfolding boolean_def by auto
  qed
qed

(* Corresponds to Andrews' lemma 5401 f *)
lemma lemma_5401_f_variant_2:
  assumes "asg_into_interp φ D I"
  assumes "general_model D I"
  assumes "wff Tv A"
  assumes "wff Tv B"
  shows "(val D I φ (A ❙⟶ B)) = boolean (satisfies D I φ A ⟶ satisfies D I φ B)"
  using assms unfolding Imp_def
  by (simp add: lemma_5401_f_variant_1 wff_Tv_is_true_or_false)

(* Corresponds to Andrews' lemma 5401 g *)
lemma lemma_5401_g:
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  assumes "wff Tv A"
  shows "satisfies D I φ ❙[❙∀x:α. A❙] ⟷ 
        (∀ψ. asg_into_interp ψ D I ⟶ agree_off_asg ψ φ x α ⟶ satisfies D I ψ A)"
proof -
  have "wff (Tv ❙⇐ α) ❙[❙λ ''x'':α. T❙]"
    by auto
  then have PI_subterm_in_D: "val D I φ ❙[❙λ ''x'':α. T❙] ∈: D (Tv ❙⇐ α)"
    using assms(1,2) general_model.simps by blast

  have "wff (Tv ❙⇐ α) (❙[❙λx:α. A❙])"
    using assms by auto
  moreover
  have "∀φ. asg_into_frame φ D ⟶ (∀A α. wff α A ⟶ val D I φ A ∈: D α)"
    using assms(1) by auto
  then have "∀t cs. val D I φ ❙[❙λcs:t. A❙] ∈: D (Tv ❙⇐ t)"
    using wff_Abs assms(1,2,3) by presburger
  then have "abstract (D α) (D Tv) (λu. val D I (φ((x, α) := u)) A) ∈: D (Tv ❙⇐ α)"
    using assms(3) by simp
  ultimately
  have val_lambda_A: "val D I φ (❙[❙λx:α. A❙]) ∈: D (Tv ❙⇐ α)"
    using assms by auto

  have true_and_A_in_D: "∀z. z ∈: D α ⟶ true ∈: D Tv ∧ val D I (φ((x, α) := z)) A ∈: D Tv"
    by (metis assms(1,2,3) general_model.simps lemma_5401_c[OF assms(1,2)] asg_into_frame_fun_upd wff_T)

  have "satisfies D I φ ❙[❙∀ x: α. A❙] ⟷ val D I φ ❙[❙∀x: α. A❙] = true"
    by auto
  moreover have "... ⟷ val D I φ (PI α) ⋅ val D I φ ❙[❙λx:α. A❙] = true"
    unfolding Forall_def by simp
  moreover have "... ⟷ I ''Q'' ((Tv ❙⇐ (Tv ❙⇐ α)) ❙⇐ (Tv ❙⇐ α))
                            ⋅ val D I φ ❙[❙λ ''x'':α. T❙] ⋅ val D I φ ❙[❙λx:α. A❙] =
                         true"
    unfolding PI_def by simp
  moreover have "... ⟷ (iden (D (Tv ❙⇐ α))) ⋅ val D I φ ❙[❙λ ''x'':α. T❙] ⋅ val D I φ ❙[❙λx:α. A❙] =
                         true"
    unfolding PI_def using wf_interp.simps assms by simp
  moreover have "... ⟷ val D I φ ❙[❙λ''x'':α. T❙] = val D I φ ❙[❙λx:α. A❙]"
    using PI_subterm_in_D val_lambda_A apply_id_true by auto
  moreover have "... ⟷ abstract (D α) (D Tv) (λz. val D I (φ((''x'', α) := z)) T) = val D I φ ❙[❙λx:α. A❙]"
    using assms wff_T by simp
  moreover have "... ⟷ abstract (D α) (D Tv) (λz. true) = val D I φ ❙[❙λx:α. A❙]"
  proof -
    have "∀x. x ∈: D α ⟶ val D I (φ((''x'', α) := x)) T ∈: D Tv ∧ true ∈: D Tv"
      using true_and_A_in_D assms(1,2)  asg_into_frame_fun_upd by auto
    moreover
    have "∀x. x ∈: D α ⟶ val D I (φ((''x'', α) := x)) T ∈: D Tv ∧ satisfies D I (φ((''x'', α) := x)) T"
      using true_and_A_in_D assms(1) assms(2) lemma_5401_c[OF assms(1)] asg_into_frame_fun_upd by auto
    ultimately
    have "abstract (D α) (D Tv) (λz. val D I (φ((''x'', α) := z)) T) = abstract (D α) (D Tv) (λz. true)"
      using abstract_extensional by auto
    then show ?thesis
      by auto
  qed
  moreover have "... ⟷ abstract (D α) (D Tv) (λz. true) = val D I φ (❙[❙λx:α. A❙])"
    by auto
  moreover have "... ⟷ abstract (D α) (D Tv) (λz. true) = 
                         abstract (D α) (D Tv) (λz. val D I (φ((x, α) := z)) A)"
    using assms by simp
  moreover have "... ⟷ (∀z. z ∈: D α ⟶ true ∈: D Tv ∧ true = val D I (φ((x, α) := z)) A)"
  proof -
    have "∀z. z ∈: D α ⟶ true ∈: D Tv ∧ val D I (φ((x, α) := z)) A ∈: D Tv"
      using true_and_A_in_D by auto
    then show ?thesis
      using abstract_iff_extensional by auto
  qed
  moreover have "... ⟷ (∀z. z ∈: D α ⟶ true = val D I (φ((x, α) := z)) A)"
    by (metis assms(1,2) general_model.simps lemma_5401_c[OF assms(1,2)] wff_T)
  moreover have "... ⟷ (∀z. z ∈: D α ⟶ satisfies D I (φ((x, α) := z)) A)"
    by auto
  moreover have "... ⟷ (∀ψ. asg_into_interp ψ D I ⟶ agree_off_asg ψ φ x α ⟶ satisfies D I ψ A)"
  proof -
    show ?thesis
    proof
      assume A_sat: "∀z. z ∈: D α ⟶ satisfies D I (φ((x, α) := z)) A"
      show "∀ψ. asg_into_frame ψ D ⟶ agree_off_asg ψ φ x α ⟶ satisfies D I ψ A"
      proof (rule; rule; rule)
        fix ψ
        assume a1: "asg_into_frame ψ D"
        assume a2: "agree_off_asg ψ φ x α"
        have "∃xa. (φ((x, α) := xa)) = ψ"
          using a1 a2 agree_off_asg_def2 by blast
        then show "satisfies D I ψ A"
          using A_sat a1 a2 by (metis asg_into_frame_def fun_upd_same)
      qed
    next
      assume "∀ψ. asg_into_frame ψ D ⟶ agree_off_asg ψ φ x α ⟶ satisfies D I ψ A"
      then show "∀z. z ∈: D α ⟶ satisfies D I (φ((x, α) := z)) A"
        using asg_into_frame_fun_upd asg_into_interp_fun_upd[OF assms(1,2)] assms(2) fun_upd_other 
        unfolding agree_off_asg_def by auto
    qed
  qed
  ultimately show ?thesis
    by auto
qed

(* Corresponds to Andrews' lemma 5401 g *)
theorem lemma_5401_g_variant_1:
  assumes "asg_into_interp φ D I"
  assumes "general_model D I"
  assumes "wff Tv A"
  shows "val D I φ ❙[❙∀x:α. A❙] =
        boolean (∀ψ. asg_into_interp ψ D I ⟶ agree_off_asg ψ φ x α ⟶ satisfies D I ψ A)"
proof -
  have "val D I φ ❙[❙∀x:α. A❙] = (if satisfies D I φ ❙[❙∀x:α. A❙] then true else false)"
    using assms wff_Forall wff_Tv_is_true_or_false by metis
  then show ?thesis
    using assms lemma_5401_g[symmetric] unfolding boolean_def by auto
qed


section ‹Soundness›

lemma fun_sym_asg_to_funspace:
  assumes "asg_into_frame φ D"
  assumes "general_model D I"
  shows "φ (f, α ❙⇐ β) ∈: funspace (D β) (D α)"
proof -
  have "wff (α ❙⇐ β) (Var f (α ❙⇐ β))"
    by auto
  then have "val D I φ (Var f (α ❙⇐ β)) ∈: D (α ❙⇐ β)"
    using assms
    using general_model.simps by blast
  then show "φ (f, α ❙⇐ β) ∈: funspace (D β) (D α)"
    using assms unfolding general_model.simps wf_interp.simps wf_frame_def
    by (simp add: subs_def)
qed

lemma fun_sym_interp_to_funspace:
  assumes "asg_into_frame φ D"
  assumes "general_model D I"
  shows "I f (α ❙⇐ β) ∈: funspace (D β) (D α)"
proof -
  have "wff (α ❙⇐ β) (Cst f (α ❙⇐ β))"
    by auto
  then have "val D I φ (Cst f (α ❙⇐ β)) ∈: D (α ❙⇐ β)"
    using assms general_model.simps by blast
  then show "I f (α ❙⇐ β) ∈: funspace (D β) (D α)"
    using assms subs_def unfolding general_model.simps wf_interp.simps wf_frame_def by auto
qed

(* Corresponds to Andrews' theorem 5402 a for rule R *)
theorem theorem_5402_a_rule_R:
  assumes A_eql_B: "valid_general (❙[A ❙=α❙= B❙])"
  assumes "valid_general C"
  assumes "rule_R C (❙[A ❙=α❙= B❙]) C'"
  assumes "wff α A"
  assumes "wff α B"
  assumes "wff β C"
  shows "valid_general C'"
  unfolding valid_general_def 
proof (rule allI, rule allI, rule impI)
  fix D :: "type_sym ⇒ 's" and I :: "char list ⇒ type_sym ⇒ 's"
  assume DI: "general_model D I"
  then have "valid_in_model D I (❙[A ❙=α❙= B❙])"
    using A_eql_B unfolding valid_general_def by auto
  then have x: "∀φ. asg_into_frame φ D ⟶ (val D I φ A = val D I φ B)"
    unfolding valid_in_model_def using lemma_5401_b[OF DI, of _ α A B ] assms(4,5) by auto
  have r: "replacement A B C C'"
    using assms(3) using Eql_def rule_R.cases by fastforce 
  from r have "∀φ. asg_into_frame φ D ⟶ (val D I φ C = val D I φ C')"
    using x assms(4,5,6) 
  proof (induction arbitrary: β rule: replacement.induct)
    case (replace A B)
    then show ?case by auto
  next
    case (replace_App_left A B C E D')
    define α' where "α' = type_of C"
    define β' where "β' = type_of D'"
    show ?case
    proof (rule, rule)
      fix φ
      assume asg: "asg_into_frame φ D"
      have α': "α' = β ❙⇐ β'"
        using trm.distinct(11) trm.distinct(3,7) trm.inject(3) replace_App_left.prems(4) wff.simps
        by (metis α'_def β'_def wff_App_type_of)
      from asg have "wff α' C"
        using replace_App_left trm.distinct(3,7,11) trm.inject(3) wff.simps
        by (metis α' β'_def type_of wff_App')   
      then have "val D I φ C = val D I φ E"
        using asg replace_App_left by auto
      then show "val D I φ (C ❙⋅ D') = val D I φ (E ❙⋅ D')"
        using α' by auto
    qed
  next
    case (replace_App_right A B D' E C)
    define α' where "α' = type_of C"
    define β' where "β' = type_of D'"
    show ?case 
    proof (rule, rule)
      fix φ
      assume asg: "asg_into_frame φ D"
      have α': "α' = β ❙⇐ β'"
        using trm.distinct(11) trm.distinct(3) trm.distinct(7) trm.inject(3) 
          replace_App_right.prems(4) wff.simps by (metis α'_def β'_def type_of wff_App')
      from asg have "wff β' D'"
        using β'_def replace_App_right.prems(4) by fastforce
      then have "val D I φ D' = val D I φ E"
        using asg replace_App_right by auto
      then show "val D I φ (C ❙⋅ D') = val D I φ (C ❙⋅ E)"
        using α' by auto
    qed
  next
    case (replace_Abs A B C D' x α')
    define β' where "β' = type_of C"
    show ?case
    proof (rule, rule)
      fix φ
      assume asg: "asg_into_frame φ D"
      then have val_C_eql_val_D':
        "∀z. z ∈: D α' ⟶ val D I (φ((x, α') := z)) C = val D I (φ((x, α') := z)) D'"
        using asg replace_App_right
        by (metis trm.distinct(11) trm.distinct(5) trm.distinct(9) trm.inject(4) 
            asg_into_frame_fun_upd replace_Abs.IH replace_Abs.prems(1) replace_Abs.prems(2) 
            replace_Abs.prems(3) replace_Abs.prems(4) wff.cases)

      have val_C_eql_val_D'_type: 
        "∀z. z ∈: D α' ⟶
                val D I (φ((x, α') := z)) C ∈: D (type_of C) ∧
                  val D I (φ((x, α') := z)) C = val D I (φ((x, α') := z)) D'"
      proof (rule; rule)
        fix z 
        assume a2: "z ∈: D α'"
        have "val D I (φ((x, α') := z)) C ∈: D (type_of C)"
          using DI asg a2 asg_into_frame_fun_upd replace_Abs.prems(4) by auto
        moreover
        have "val D I (φ((x, α') := z)) C = val D I (φ((x, α') := z)) D'"
          using a2 val_C_eql_val_D' replace_Abs by auto
        ultimately
        show
          "val D I (φ((x, α') := z)) C ∈: D (type_of C) ∧
          val D I (φ((x, α') := z)) C = val D I (φ((x, α') := z)) D'"
          by auto
      qed
      have "wff (type_of C) D'"
        using replacement_preserves_type replace_Abs.hyps replace_Abs.prems(2) 
          replace_Abs.prems(3) replace_Abs.prems(4) wff_Abs_type_of by blast
      then have same_type: 
        "abstract (D α') (D (type_of C)) (λz. val D I (φ((x, α') := z)) D') =
         abstract (D α') (D (type_of D')) (λz. val D I (φ((x, α') := z)) D')"
        using type_of by presburger
      then show "val D I φ ❙[❙λx:α'. C❙] = val D I φ (❙[❙λx:α'. D'❙])"
        using val_C_eql_val_D'_type same_type 
          abstract_extensional[of _ _ _ "λxa. val D I (φ((x, α') := xa)) D'"]
        by (simp add: val_C_eql_val_D'_type same_type)
    qed
  qed
  then show "valid_in_model D I C'"
    using assms(2) DI unfolding valid_in_model_def valid_general_def by auto
qed

theorem Fun_Tv_Tv_frame_subs_funspace:
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  shows "D oo ⊆: funspace (boolset) (boolset)"
  by (metis assms(1) general_model.elims(2) wf_frame_def wf_interp.simps)

(* Corresponds to Andrews' theorem 5402 a for axiom 1 *)
theorem theorem_5402_a_axiom_1_variant:
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  shows "satisfies D I φ axiom_1"
proof (cases "(φ (''g'',oo)) ⋅ true = true ∧ (φ (''g'',oo)) ⋅ false = true")
  case True
  then have val: "val D I φ ((g⇩o⇩o ❙⋅ T) ❙∧ (g⇩o⇩o ❙⋅ F)) = true"
    using assms lemma_5401_e_variant_2
    by (auto simp add: boolean_eq_true lemma_5401_c[OF assms(1,2)] lemma_5401_d[OF assms(1,2)])
  have "∀ψ. asg_into_frame ψ D ⟶ 
            agree_off_asg ψ φ ''x'' Tv ⟶ 
            satisfies D I ψ (g⇩o⇩o ❙⋅ x⇩o)"
  proof (rule; rule; rule)
    fix ψ
    assume ψ: "asg_into_frame ψ D" "agree_off_asg ψ φ ''x'' Tv"
    then have "ψ (''x'', Tv) = true ∨ ψ (''x'', Tv) = false"
      using asg_into_interp_is_true_or_false assms
      by auto
    then show " satisfies D I ψ (g⇩o⇩o ❙⋅ x⇩o)"
      using True ψ unfolding agree_off_asg_def by auto
  qed
  then have  "val D I φ (❙[❙∀''x'':Tv. (g⇩o⇩o ❙⋅ x⇩o)❙]) = true"
    using lemma_5401_g using assms by auto
  then show ?thesis
    unfolding axiom_1_def
    using lemma_5401_b[OF assms(1,2)] val by auto
next
  case False
  have "φ (''g'', oo) ∈: D oo"
    using assms
    by (simp add: asg_into_frame_def) 
  then have 0: "φ (''g'', oo) ∈: funspace (D Tv) (D Tv)"
    using assms(1) assms(2) fun_sym_asg_to_funspace by blast

  from False have "(φ (''g'', oo) ⋅ true ≠ true ∨ φ (''g'', oo) ⋅ false ≠ true)"
    by auto
  then have "∃z. φ (''g'', oo) ⋅ z = false ∧ z ∈: D Tv"
  proof
    assume a: "φ (''g'', oo) ⋅ true ≠ true"
    have "φ (''g'', oo) ⋅ true ∈: boolset"
      by (metis "0" apply_abstract assms(1) boolset_def general_model.elims(2) in_funspace_abstract 
          mem_two true_def wf_frame_def wf_interp.simps)
    from this a have "φ (''g'', oo) ⋅ true = false ∧ true ∈: D Tv"
      using assms(1) wf_frame_def wf_interp.simps by auto  
    then show "∃z. φ (''g'', oo) ⋅ z = false ∧ z ∈: D Tv"
      by auto
  next
    assume a: "φ (''g'', oo) ⋅ false ≠ true"
    have "φ (''g'', oo) ⋅ false ∈: boolset"
      by (metis "0" apply_abstract assms(1) boolset_def general_model.elims(2) in_funspace_abstract 
          mem_two false_def wf_frame_def wf_interp.simps)
    from this a have "φ (''g'', oo) ⋅ false = false ∧ false ∈: D Tv" 
      using assms(1) wf_frame_def wf_interp.simps by auto
    then show "∃z. φ (''g'', oo) ⋅ z = false ∧ z ∈: D Tv"
      by auto
  qed
  then obtain z where z_p: "φ (''g'', oo) ⋅ z = false ∧ z ∈: D Tv"
    by auto
  have "boolean (satisfies D I φ (g⇩o⇩o ❙⋅ T)
          ∧ satisfies D I φ (g⇩o⇩o ❙⋅ F)) = false"
    using False
    by (smt boolean_def val.simps(1) val.simps(3) lemma_5401_c[OF assms(1,2)] 
        lemma_5401_d[OF assms(1,2)])
  then have 1: "val D I φ ( 
         (g⇩o⇩o ❙⋅ T) ❙∧
         (g⇩o⇩o ❙⋅ F)) = false"
    using lemma_5401_e_variant_2 assms by auto
  have 3: "asg_into_frame (φ((''x'', Tv) := z)) D ∧
    agree_off_asg (φ((''x'', Tv) := z)) φ ''x'' Tv ∧
    φ (''g'', oo) ⋅ (φ((''x'', Tv) := z)) (''x'', Tv) ≠ true"
    using z_p Pair_inject agree_off_asg_def2 asg_into_frame_fun_upd assms(2) true_neq_false by fastforce
  then have 2: "val D I φ (❙[❙∀''x'':Tv. (g⇩o⇩o ❙⋅ x⇩o)❙]) = false"
    using  lemma_5401_g_variant_1 assms boolean_def by auto
  then show ?thesis
    unfolding axiom_1_def using 1 2 lemma_5401_b_variant_2[OF assms(1,2)] by auto 
qed

(* Corresponds to Andrews' theorem 5402 a for axiom 1 *)
theorem theorem_5402_a_axiom_1: "valid_general axiom_1"
  using theorem_5402_a_axiom_1_variant unfolding valid_general_def valid_in_model_def by auto

(* Corresponds to Andrews' theorem 5402 a for axiom 2 *)
theorem theorem_5402_a_axiom_2_variant:
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  shows "satisfies D I φ (axiom_2 α)"
proof (cases "φ(''x'',α) = φ(''y'',α)")
  case True
  have "val D I φ ((Var ''h'' (Tv ❙⇐ α)) ❙⋅ (Var ''x'' α)) = 
           (φ (''h'', (Tv ❙⇐ α))) ⋅ φ (''x'', α)"
    using assms by auto
  also
  have "... = φ (''h'', (Tv ❙⇐ α)) ⋅ φ (''y'', α)"
    using True by auto
  also
  have "... = val D I φ ((Var ''h'' (Tv ❙⇐ α)) ❙⋅ (Var ''y'' α))"
    using assms by auto
  finally
  show ?thesis
    unfolding axiom_2_def 
    using lemma_5401_f_variant_2 assms lemma_5401_b_variant_1[OF assms(1,2)] boolean_def by auto
next
  case False
  have "asg_into_frame φ D"
    using assms(2) by blast
  moreover
  have "general_model D I"
    using assms(1) by blast
  ultimately
  have 
    "boolean (satisfies D I φ ❙[Var ''x'' α ❙=α❙= Var ''y'' α❙] ⟶
       satisfies D I φ
         ❙[(Var ''h'' (Tv ❙⇐ α) ❙⋅ Var ''x'' α) ❙=Tv❙= Var ''h'' (Tv ❙⇐ α) ❙⋅ Var ''y'' α❙]) =
       true"
    using boolean_eq_true lemma_5401_b by auto
  then
  show ?thesis
    using assms lemma_5401_f_variant_2 unfolding axiom_2_def by auto
qed                                   

(* Corresponds to Andrews' theorem 5402 a for axiom 2 *)
theorem theorem_5402_a_axiom_2: "valid_general (axiom_2 α)"
  using theorem_5402_a_axiom_2_variant unfolding valid_general_def valid_in_model_def by auto

(* Corresponds to Andrews' theorem 5402 a for axiom 3 *)
theorem theorem_5402_a_axiom_3_variant:
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  shows "satisfies D I φ (axiom_3 α β)"
proof (cases "φ (''f'',α ❙⇐ β) = φ (''g'',α ❙⇐ β)")
  case True
  {
    fix ψ
    assume agree: "agree_off_asg ψ φ ''x'' β"
    assume asg: "asg_into_interp ψ D I"
    have "val D I ψ ((Var ''f'' (α ❙⇐ β)) ❙⋅ (Var ''x'' β)) = ψ (''f'',α ❙⇐ β) ⋅ ψ (''x'', β)"
      by auto
    also
    have "... = φ (''f'',α ❙⇐ β) ⋅ ψ (''x'', β)"
      using agree by auto
    also
    have "... = φ (''g'',α ❙⇐ β) ⋅ ψ (''x'', β)"
      using True by auto
    also
    have "... = ψ (''g'',α ❙⇐ β) ⋅ ψ (''x'', β)"
      using agree by auto
    also
    have "... = val D I ψ ((Var ''g'' (α ❙⇐ β)) ❙⋅ (Var ''x'' β))"
      by auto
    finally
    have 
      "val D I ψ
            (❙[((Var ''f'' (α ❙⇐ β)) ❙⋅ (Var ''x'' β)) ❙=α❙= ((Var ''g'' (α ❙⇐ β)) ❙⋅ (Var ''x'' β))❙]) 
       = true"
      using lemma_5401_b_variant_1[OF assms(1)] assms agree asg boolean_eq_true by auto
  }
  then have "satisfies D I φ
        (❙[❙∀''x'':β. ❙[(Var ''f'' (α ❙⇐ β) ❙⋅ Var ''x'' β) ❙=α❙= Var ''g'' (α ❙⇐ β) ❙⋅ Var ''x'' β❙]❙])"
    using assms lemma_5401_g by force
  moreover
  have "satisfies D I φ ❙[Var ''f'' (α ❙⇐ β) ❙=α ❙⇐ β❙= Var ''g'' (α ❙⇐ β)❙]"
    using True assms using lemma_5401_b_variant_2 wff_Var by auto
  ultimately
  show ?thesis
    using axiom_3_def lemma_5401_b_variant_2 assms by auto
next
  case False
  then have "∃z. z ∈: D β ∧ φ (''f'', α ❙⇐ β) ⋅ z ≠ φ (''g'', α ❙⇐ β) ⋅ z"
    using funspace_difference_witness[of "φ (''f'', α ❙⇐ β)" "D β" "D α" "φ (''g'', α ❙⇐ β)"]
      assms(1,2) fun_sym_asg_to_funspace by blast
  then obtain z where
    zβ: "z ∈: D β" and
    z_neq: "φ (''f'', α ❙⇐ β) ⋅ z ≠ φ (''g'', α ❙⇐ β) ⋅ z"
    by auto
  define ψ where "ψ = (φ((''x'',β):= z))"
  have agree: "agree_off_asg ψ φ ''x'' β"
    using ψ_def agree_off_asg_def2 by blast
  have asg: "asg_into_interp ψ D I"
    using zβ ψ_def asg_into_frame_fun_upd assms(2) by blast
  have "val D I ψ ((Var ''f'' (α ❙⇐ β)) ❙⋅ (Var ''x'' β)) = ψ (''f'',α ❙⇐ β) ⋅ ψ (''x'', β)"
    by auto
  moreover
  have "... = φ (''f'',α ❙⇐ β) ⋅ z"
    by (simp add: ψ_def)
  moreover
  have "... ≠ φ (''g'',α ❙⇐ β) ⋅ z"
    using False z_neq by blast
  moreover
  have "φ (''g'',α ❙⇐ β) ⋅ z = ψ (''g'',α ❙⇐ β) ⋅ ψ (''x'', β)"
    by (simp add: ψ_def)
  moreover
  have "... = val D I ψ ((Var ''g'' (α ❙⇐ β)) ❙⋅ (Var ''x'' β))"
    by auto
  ultimately
  have 
    "val D I ψ
            (❙[((Var ''f'' (α ❙⇐ β)) ❙⋅ (Var ''x'' β)) ❙=α❙= ((Var ''g'' (α ❙⇐ β)) ❙⋅ (Var ''x'' β))❙]) 
       = false"
    by (metis asg assms(1) lemma_5401_b_variant_3 wff_App wff_Var)
  have "val D I φ
        (❙[❙∀''x'':β. ❙[(Var ''f'' (α ❙⇐ β) ❙⋅ Var ''x'' β) ❙=α❙= Var ''g'' (α ❙⇐ β) ❙⋅ Var ''x'' β❙]❙]) = false"
    by (smt (verit) ‹val D I ψ ❙[(Var ''f'' (α ❙⇐ β) ❙⋅ Var ''x'' β) ❙=α❙= Var ''g'' (α ❙⇐ β) ❙⋅ Var ''x'' β❙] = false› 
        agree asg assms(1,2) lemma_5401_g wff_App wff_Eql wff_Forall wff_Tv_is_true_or_false wff_Var)
  moreover
  have "val D I φ ❙[Var ''f'' (α ❙⇐ β) ❙=α ❙⇐ β❙= Var ''g'' (α ❙⇐ β)❙] = false"
    using False assms(1,2) lemma_5401_b_variant_3 wff_Var by auto
  ultimately show ?thesis
    using assms(1,2) axiom_3_def lemma_5401_b by auto
qed

(* Corresponds to Andrews' theorem 5402 a for axiom 3 *)
theorem theorem_5402_a_axiom_3: "valid_general (axiom_3 α β)"
  using theorem_5402_a_axiom_3_variant unfolding valid_general_def valid_in_model_def by auto

(* Corresponds to Andrews' theorem 5402 a for axiom 4_1 with a constant *)
theorem theorem_5402_a_axiom_4_1_variant_cst:
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  assumes "wff α A"
  shows "satisfies D I φ (axiom_4_1_variant_cst x α c β A)"
proof -
  let ?ψ = "φ((x,α):=val D I φ A)"
  have "val D I φ (❙[❙λx:α. (Cst c β)❙] ❙⋅ A) = val D I ?ψ (Cst c β)"
    by (rule lemma_5401_a[of _ _ _ _ _ β]; use assms in auto)
  then have "val D I φ (❙[❙λx:α. Cst c β❙] ❙⋅ A) = val D I φ (Cst c β)"
    by auto
  moreover
  have "wff β (❙[❙λx:α. Cst c β❙] ❙⋅ A)"
    using assms by auto
  ultimately
  show ?thesis
    unfolding axiom_4_1_variant_cst_def
    using lemma_5401_b_variant_2[OF assms(1,2)] by auto
qed

(* Corresponds to Andrews' theorem 5402 a for axiom 4_1 *)
theorem theorem_5402_a_axiom_4_1_variant_var:
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  assumes "wff α A"
  assumes "axiom_4_1_variant_var_side_condition x α y β A"
  shows "satisfies D I φ (axiom_4_1_variant_var x α y β A)"
proof -
  let ?ψ = "φ((x,α):=val D I φ A)"
  have  "val D I φ (❙[❙λx:α. (Var y β)❙] ❙⋅ A) = val D I ?ψ (Var y β)"
    by (rule lemma_5401_a[of _ _ _ _ _  β], use assms in auto)
  then have "val D I φ (❙[❙λx:α. Var y β❙] ❙⋅ A) = val D I φ (Var y β)"   
    using assms unfolding axiom_4_1_variant_var_side_condition_def by auto
  moreover
  have "wff β (❙[❙λx:α. Var y β❙] ❙⋅ A)"
    using assms by auto
  moreover
  have "wff β (Var y β)"
    using assms by auto
  ultimately
  show ?thesis
    unfolding axiom_4_1_variant_var_def
    using lemma_5401_b_variant_2[OF assms(1,2)] by auto
qed

(* Corresponds to Andrews' theorem 5402 a for axiom 4_1 *)
theorem theorem_5402_a_axiom_4_1:
  assumes "asg_into_interp φ D I"
  assumes "general_model D I"
  assumes "axiom_4_1_side_condition x α y β A"
  assumes "wff α A"
  shows "satisfies D I φ (axiom_4_1 x α y β A)"
  using assms theorem_5402_a_axiom_4_1_variant_cst theorem_5402_a_axiom_4_1_variant_var
  unfolding axiom_4_1_variant_cst_def axiom_4_1_variant_var_side_condition_def
    axiom_4_1_side_condition_def axiom_4_1_variant_var_def
    axiom_4_1_def by auto

(* Corresponds to Andrews' theorem 5402 a for axiom 4_2 *)
theorem theorem_5402_a_axiom_4_2: 
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  assumes "wff α A"
  shows "satisfies D I φ (axiom_4_2 x α A)"
proof -
  let ?ψ = "φ((x,α):=val D I φ A)"
  have "wff α (❙[❙λx:α. Var x α❙] ❙⋅ A)"
    using assms by auto
  moreover
  have "wff α A"
    using assms by auto
  moreover
  have "val D I φ (❙[❙λx:α. Var x α❙] ❙⋅ A) = val D I φ A"
    using lemma_5401_a[of _ _ _ _ _ α _ _] assms by auto
  ultimately
  show ?thesis
    unfolding axiom_4_2_def by (rule lemma_5401_b_variant_2[OF assms(1,2)])
qed

(* Corresponds to Andrews' theorem 5402 a for axiom 4_3 *)
theorem theorem_5402_a_axiom_4_3: 
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  assumes "wff α A"
  assumes "wff (β ❙⇐ γ) B"
  assumes "wff γ C"
  shows "satisfies D I φ (axiom_4_3 x α B β γ C A)"
proof -
  let ?ψ = "φ((x,α):=val D I φ A)"
  let ?E = "B ❙⋅ C"

  have "val D I φ (LHS (axiom_4_3 x α B β γ C A)) = val D I ?ψ ?E"
    by (metis LHS_def2 assms(3) assms(4) assms(5) axiom_4_3_def lemma_5401_a[OF assms(1,2)] wff_App)
  moreover
  have "... = val D I ?ψ (B ❙⋅ C)"
    by simp
  moreover
  have "... = (val D I ?ψ B) ⋅ val D I ?ψ C"
    by simp
  moreover
  have "... = (val D I φ (❙[❙λx:α. B❙] ❙⋅ A)) ⋅ val D I φ (App ❙[❙λx :α. C❙] A)"
    by (metis assms(3) assms(4) assms(5) lemma_5401_a[OF assms(1,2)])
  moreover
  have "... = val D I φ (RHS (axiom_4_3 x α B β γ C A))"
    unfolding axiom_4_3_def by auto
  ultimately
  have "val D I φ (LHS (axiom_4_3 x α B β γ C A)) = val D I φ (RHS (axiom_4_3 x α B β γ C A))"
    by auto
  then have "val D I φ (❙[❙λx:α. B ❙⋅ C❙] ❙⋅ A) = val D I φ (❙[❙λx:α. B❙] ❙⋅ A ❙⋅ (❙[❙λx:α. C❙] ❙⋅ A))"
    unfolding axiom_4_3_def by auto
  moreover
  have "wff β (❙[❙λx:α. B ❙⋅ C❙] ❙⋅ A)"
    using assms by auto
  moreover
  have "wff β (❙[❙λx:α. B❙] ❙⋅ A ❙⋅ (❙[❙λx:α. C❙] ❙⋅ A))"
    using assms by auto
  ultimately
  show ?thesis
    unfolding axiom_4_3_def using lemma_5401_b_variant_2[OF assms(1,2)] by auto
qed

lemma lemma_to_help_with_theorem_5402_a_axiom_4_4:
  assumes lambda_eql_lambda_lambda: 
    "⋀z. z ∈: D γ ⟹ val D I ψ ❙[❙λy:γ. B❙] ⋅ z = val D I φ ❙[❙λy:γ. ❙[❙λx:α. B❙] ❙⋅ A❙] ⋅ z" 
  assumes ψ_eql: "ψ = φ((x, α) := val D I φ A)" 
  assumes "asg_into_frame φ D" 
  assumes "general_model D I" 
  assumes "axiom_4_4_side_condition x α y γ B δ A" 
  assumes "wff α A" 
  assumes "wff δ B"
  shows "val D I ψ ❙[❙λy:γ. B❙] = val D I φ ❙[❙λy:γ. ❙[❙λx:α. B❙] ❙⋅ A❙]"
proof -
  {
    fix e
    assume e_in_D: "e ∈: D γ"
    then have "val D I (ψ((y, γ) := e)) B ∈: D (type_of B)"
      using asg_into_frame_fun_upd assms(3,4,6,7) ψ_eql by auto
    then have val_lambda_B: "val D I ψ ❙[❙λy:γ. B❙] ⋅ e = val D I (ψ((y, γ) := e)) B"
      using e_in_D by auto
    have
      "val D I φ ❙[❙λy:γ. ❙[❙λx:α. B❙] ❙⋅ A❙] ⋅ e = 
       abstract (D α) (D (type_of B))
         (λz. val D I (φ((y, γ) := e, (x, α) := z)) B) ⋅ val D I (φ((y, γ) := e)) A"
      using apply_abstract e_in_D asg_into_frame_fun_upd assms(3,4,6,7) by auto
    then have "val D I (ψ((y, γ) := e)) B =
        abstract (D α) (D (type_of B))
         (λz. val D I (φ((y, γ) := e, (x, α) := z)) B) ⋅ val D I (φ((y, γ) := e)) A" 
      using val_lambda_B lambda_eql_lambda_lambda e_in_D by metis
  }
  note val_eql_abstract = this

  have 
    "∀e. e ∈: D γ ⟶
            val D I (ψ((y, γ) := e)) B ∈: D (type_of B) ∧
            val D I (ψ((y, γ) := e)) B =
            abstract (D α) (D (type_of B))
              (λza. val D I (φ((y, γ) := e, (x, α) := za)) B) ⋅ val D I (φ((y, γ) := e)) A"
    using asg_into_frame_fun_upd assms(3,4,6,7) ψ_eql val_eql_abstract by auto
  then have 
    "abstract (D γ) (D (type_of B)) (λz. val D I (ψ((y, γ) := z)) B) =
     abstract (D γ) (D (type_of B))
       (λz. abstract (D α) (D (type_of B))
         (λza. val D I (φ((y, γ) := z, (x, α) := za)) B) ⋅ val D I (φ((y, γ) := z)) A)"
    by (rule abstract_extensional)
  then show ?thesis 
    by auto
qed

(* Corresponds to Andrews' theorem 5402 a for axiom 4_4 *)
theorem theorem_5402_a_axiom_4_4:
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  assumes "axiom_4_4_side_condition x α y γ B δ A"
  assumes "wff α A"
  assumes "wff δ B"
  shows "satisfies D I φ (axiom_4_4 x α y γ B δ A)"
proof -
  define ψ where "ψ = φ((x,α):=val D I φ A)"
  let ?E = "❙[❙λy:γ. B❙]"
  have fr: "(y, γ) ∉ vars A"
    using assms(3) axiom_4_4_side_condition_def by blast
  {
    fix z
    assume z_in_D: "z ∈: D γ"
    define φ' where "φ' = φ((y,γ) := z)"
    have "asg_into_frame φ' D"
      using assms z_in_D unfolding asg_into_frame_def φ'_def by auto
    moreover
    have "∀(x, α)∈vars A. agree_on_asg φ φ' x α"
      using fr unfolding φ'_def by auto
    ultimately
    have "val D I φ A = val D I φ' A"
      using prop_5400[OF assms(1), of _ _ α] assms(2) assms(4) frees_subset_vars by blast
    then have Az: "φ'((x,α):=(val D I φ' A)) = ψ((y,γ):=z)"
      using assms(3) unfolding axiom_4_4_side_condition_def
      by (simp add: fun_upd_twist φ'_def ψ_def) 
    then have "abstract (D γ) (D (type_of B)) (λz. val D I (ψ((y, γ) := z)) B) ⋅ z = 
               val D I (ψ((y, γ) := z)) B"
      using apply_abstract_matchable assms(1,2,4,5) type_of asg_into_frame_fun_upd 
        general_model.elims(2) z_in_D by (metis φ'_def)
    then have "(val D I ψ ?E) ⋅ z = (val D I (ψ((y,γ):=z)) B)"
      by auto
    moreover
    have "... = val D I φ' (❙[❙λx:α. B❙] ❙⋅ A)"
      using assms(1,2,4,5) asg_into_frame_fun_upd lemma_5401_a z_in_D
      by (metis Az φ'_def) 
    moreover
    have "... = val D I φ ❙[❙λy:γ. ❙[❙λx:α. B❙] ❙⋅ A❙] ⋅ z"
    proof -
      have valA: "val D I φ' A ∈: D α"
        using φ'_def asg_into_frame_fun_upd z_in_D assms by simp
      have valB: "val D I (φ'((x, α) := val D I φ' A)) B ∈: D (type_of B)" 
        using asg_into_frame_fun_upd z_in_D assms by (simp add: Az ψ_def) 
      have valA': "val D I (φ((y, γ) := z)) A ∈: D α"
        using z_in_D assms asg_into_frame_fun_upd valA unfolding ψ_def φ'_def 
        by blast
      have valB':
        "val D I (φ((y, γ) := z, (x, α) := val D I (φ((y, γ) := z)) A)) B 
         ∈: D (type_of B)"
        using asg_into_frame_fun_upd z_in_D assms valB φ'_def by blast 
      have
        "val D I (φ'((x, α) := val D I φ' A)) B =
         val D I (φ((y, γ) := z, (x, α) := val D I (φ((y, γ) := z)) A)) B"
        unfolding ψ_def φ'_def by (metis apply_abstract asg_into_frame_fun_upd)
      then have valB_eql_abs: 
        "val D I (φ'((x, α) := val D I φ' A)) B =
         abstract (D α) (D (type_of B))
           (λza. val D I (φ((y, γ) := z, (x, α) := za)) B) ⋅ val D I (φ((y, γ) := z)) A"
        using valA' valB' by auto
      then have "abstract (D α) (D (type_of B))
              (λza. val D I (φ((y, γ) := z, (x, α) := za)) B) ⋅ val D I (φ((y, γ) := z)) A 
            ∈: D (type_of B)"
        using valB assms z_in_D by auto
      then have 
        "val D I (φ'((x, α) := val D I φ' A)) B =
         abstract (D γ) (D (type_of B))
           (λz. abstract (D α) (D (type_of B))
             (λza. val D I (φ((y, γ) := z, (x, α) := za)) B) ⋅ val D I (φ((y, γ) := z)) A) ⋅ z"
        using z_in_D valB_eql_abs by auto
      then show "val D I φ' (❙[❙λx:α. B❙] ❙⋅ A) = val D I φ ❙[❙λy:γ. ❙[❙λx:α. B❙] ❙⋅ A❙] ⋅ z"
        using valA valB by auto
    qed
    ultimately
    have "val D I ψ ❙[❙λy:γ. B❙] ⋅ z = val D I φ ❙[❙λy:γ. ❙[❙λx:α. B❙] ❙⋅ A❙] ⋅ z"
      by simp
  }
  note lambda_eql_lambda_lambda = this
  have equal_funs: "val D I ψ ?E = val D I φ (❙[❙λy:γ. (❙[❙λx:α. B❙]) ❙⋅ A❙])"
    using lambda_eql_lambda_lambda ψ_def assms lemma_to_help_with_theorem_5402_a_axiom_4_4 by metis
  have "val D I φ (❙[❙λx:α. ❙[❙λy:γ. B❙]❙] ❙⋅ A) = val D I φ ❙[❙λy:γ. ❙[❙λx:α. B❙] ❙⋅ A❙]"
    using equal_funs by (metis ψ_def assms(1,2,4,5) lemma_5401_a wff_Abs) 
  then have "satisfies D I φ ❙[(❙[❙λx:α. ❙[❙λy:γ. B❙]❙] ❙⋅ A) ❙=δ ❙⇐ γ❙= ❙[❙λy:γ. ❙[❙λx:α. B❙] ❙⋅ A❙]❙]"
    using lemma_5401_b[OF assms(1,2)] assms by auto
  then show ?thesis
    unfolding axiom_4_4_def .
qed

(* Corresponds to Andrews' theorem 5402 a for axiom 4_5 *)
theorem theorem_5402_a_axiom_4_5:
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  assumes "wff α A"
  assumes "wff δ B"
  shows "satisfies D I φ (axiom_4_5 x α B δ A)"
proof -
  define ψ where "ψ = φ((x,α):=val D I φ A)"
  let ?E = "❙[❙λx:α. B❙]"

  {
    assume val: "∀φ. asg_into_frame φ D ⟶ (∀A α. wff α A ⟶ val D I φ A ∈: D α)"
    assume asg: "asg_into_frame φ D"
    assume wffA: "wff α A"
    assume wffB: "wff δ B"
    have valA: "val D I φ A ∈: D α"
      using val asg wffA by blast
    have "∀t cs. val D I φ ❙[❙λcs:t. B❙] ∈: D (δ ❙⇐ t)"
      using val asg wffB wff_Abs by blast
    then have "abstract (D α) (D (δ ❙⇐ α)) 
                 (λu. abstract (D α) (D δ) (λu. val D I (φ((x, α) := u)) B)) ⋅ val D I φ A =
               abstract (D α) (D δ) (λu. val D I (φ((x, α) := u)) B)"
      using valA wffB by simp
  }
  note abstract_eql = this

  have "val D I ψ ?E = val D I φ ?E"
    using prop_5400[OF assms(1), of _ _ "δ ❙⇐ α"] ψ_def assms(2) by auto
  then show ?thesis
    unfolding axiom_4_5_def using lemma_5401_b[OF assms(1,2)] assms abstract_eql by auto
qed

(* Corresponds to Andrews' theorem 5402 a for axiom 5 *)
theorem theorem_5402_a_axiom_5:
  assumes "general_model D I"
  assumes "asg_into_interp φ D I"
  shows "satisfies D I φ (axiom_5)"
proof -
  have iden_eql: "iden (D Ind) ⋅ I ''y'' Ind = one_elem_fun (I ''y'' Ind) (D Ind)"
  proof -
    have "I ''y'' Ind ∈: D Ind"
      using assms unfolding  general_model.simps wf_interp.simps[simplified] iden_def one_elem_fun_def
      by auto
    moreover
    have "abstract (D Ind) boolset (λy. boolean (I ''y'' Ind = y)) ∈: funspace (D Ind) boolset"
      using boolean_in_boolset by auto
    ultimately
    show ?thesis
      unfolding iden_def one_elem_fun_def by auto
  qed

  have "val D I φ (❙ι ❙⋅ ((❙Q (Tv ❙⇐ Ind ❙⇐ Ind)) ❙⋅ y⇩i)) = 
          val D I φ ❙ι ⋅ val D I φ ((❙Q (Tv ❙⇐ Ind ❙⇐ Ind)) ❙⋅ y⇩i)"
    by auto
  moreover
  have "... = val D I φ y⇩i"
    using assms iden_eql unfolding general_model.simps wf_interp.simps[simplified] by auto
  ultimately
  show ?thesis
    unfolding axiom_5_def using lemma_5401_b[OF assms(1,2)] by auto
qed

lemma theorem_isa_Tv:
  assumes "theorem A"
  shows "wff Tv A"
  using assms proof (induction)
  case (by_axiom A)
  then show ?case 
  proof (induction)
    case by_axiom_1
    then show ?case 
      unfolding axiom_1_def by auto
  next
    case (by_axiom_2 α)
    then show ?case 
      unfolding axiom_2_def by auto
  next
    case (by_axiom_3 α β)
    then show ?case 
      unfolding axiom_3_def by auto
  next
    case (by_axiom_4_1 α A β B x)
    then show ?case 
      unfolding axiom_4_1_def by auto
  next
    case (by_axiom_4_2 α A x)
    then show ?case 
      unfolding axiom_4_2_def by auto
  next
    case (by_axiom_4_3 α A β γ B C x)
    then show ?case 
      unfolding axiom_4_3_def by auto
  next
    case (by_axiom_4_4 α A δ B x y γ)
    then show ?case 
      unfolding axiom_4_4_def by auto
  next
    case (by_axiom_4_5 α A δ B x)
    then show ?case 
      unfolding axiom_4_5_def by auto
  next
    case by_axiom_5
    then show ?case 
      unfolding axiom_5_def by auto
  qed
next
  case (by_rule_R A B C)
  then show ?case
    by (smt replacement_preserves_type rule_R.cases wff_Eql_iff)
qed

(* Corresponds to Andrews' theorem 5402 a *)
theorem theorem_5402_a_general:
  assumes "theorem A"
  shows "valid_general A"
  using assms 
proof (induction)
  case (by_axiom A)
  then show ?case
  proof (induction)
    case by_axiom_1
    then show ?case 
      using theorem_5402_a_axiom_1 by auto
  next
    case (by_axiom_2 α)
    then show ?case 
      using theorem_5402_a_axiom_2 by auto
  next
    case (by_axiom_3 α β)
    then show ?case 
      using theorem_5402_a_axiom_3 by auto
  next
    case (by_axiom_4_1 α A β B x)
    then show ?case 
      using theorem_5402_a_axiom_4_1
      unfolding valid_general_def valid_in_model_def by auto
  next
    case (by_axiom_4_2 α A x)
    then show ?case 
      using theorem_5402_a_axiom_4_2 
      unfolding valid_general_def valid_in_model_def by auto
  next
    case (by_axiom_4_3 α A β γ B C x)
    then show ?case 
      using theorem_5402_a_axiom_4_3 
      unfolding valid_general_def valid_in_model_def by auto
  next
    case (by_axiom_4_4 α A δ B x y γ)
    then show ?case 
      using theorem_5402_a_axiom_4_4 
      unfolding valid_general_def valid_in_model_def by auto
  next
    case (by_axiom_4_5 α A δ B x)
    then show ?case 
      using theorem_5402_a_axiom_4_5 
      unfolding valid_general_def valid_in_model_def by auto
  next
    case by_axiom_5
    then show ?case
      using theorem_5402_a_axiom_5 
      unfolding valid_general_def valid_in_model_def by auto
  qed
next
  case (by_rule_R C AB C')
  then have C_isa_Tv: "wff Tv C"
    using theorem_isa_Tv by blast
  have "∃A B β. AB = ❙[A ❙=β❙= B❙] ∧ wff β A ∧ wff β B"
    using by_rule_R rule_R.simps theorem_isa_Tv by fastforce
  then obtain A B β where A_B_β_p: "AB = ❙[A ❙=β❙= B❙] ∧ wff β A ∧ wff β B"
    by blast
  then have R: "rule_R C ❙[A ❙=β❙= B❙] C'"
    using by_rule_R by auto
  then have "replacement A B C C'"
    using Eql_def rule_R.cases by fastforce
  show ?case
    using theorem_5402_a_rule_R[of A B β C C' Tv] by_rule_R.IH R
      A_B_β_p C_isa_Tv by auto
qed

(* Corresponds to Andrews' theorem 5402 a *)
theorem theorem_5402_a_standard:
  assumes "theorem A"
  shows "valid_standard A"
  using theorem_5402_a_general assms standard_model_is_general_model valid_general_def 
    valid_standard_def by blast

end

end