Theory Model_Existence

theory Model_Existence imports
  Consistency_Property
  "Q0_Metatheory.Soundness"
begin

section ‹Prelude›

instance type :: countable
  by countable_datatype

instance form :: countable
  by countable_datatype

instance type :: small ..
instance type :: embeddable ..
instance form :: small ..
instance form :: embeddable ..

definition is_frugal :: ‹model_structure ⇒ bool› where
  ‹is_frugal ℳ ≡ case ℳ of (𝒟, 𝒥, 𝒱) ⇒ ∀α. |elts (𝒟 α)| ≤o |UNIV :: form set|›

lemma is_frugal_countable: ‹is_frugal (𝒟, 𝒥, 𝒱) ⟷ ( ∀α. |elts (𝒟 α)| ≤o |UNIV :: nat set| )›
  unfolding is_frugal_def case_prod_conv
  by (meson UNIV_I card_of_ordLeqI  countable_class.ex_inj inf_univ
      infinite_iff_card_of_nat ordLeq_transitive)

definition extensionally_complete_membership :: ‹form set ⇒ bool› where
  ‹extensionally_complete_membership H ⟷
    (∀A B α β. is_closed_wff_of_type A (β → α) ⟶
               is_closed_wff_of_type B (β → α) ⟶
               (∃C. is_closed_wff_of_type C β ∧
                    ((A · C) =⇘α⇙ (B · C) ∈ H ⟶ (A =⇘β → α⇙ B) ∈ H)))›

lemma substitute_cong:
  assumes ‹A ∈ wffs⇘α⇙›
    and ‹∀x ∈ free_vars A. F $$ x = G $$ x›
  shows ‹substitute F A = substitute G A›
  using assms
proof (induct A arbitrary: F G rule: wffs_of_type_induct)
  case (abs_is_wff β A α x)
  show ?case
  proof (cases ‹(x, α) ∉ fmdom' G ∧ (x, α) ∉ fmdom' F›)
    case True
    then show ?thesis 
      using abs_is_wff
      by (metis fmdom'_notD free_vars_form.simps(4) 
          insert_Diff_single insert_iff substitute.simps(4))
  next
    case False
    then show ?thesis
      using abs_is_wff by auto
  qed
qed simp_all

lemma fmran'_fmdrop_subset: ‹fmran' (fmdrop (x, α) θ) ⊆ fmran' θ›
  by (induct θ) (simp_all add: fmdrop_fmupd subset_iff)

lemma free_vars_substitute: ‹free_vars (substitute φ A) 
  ⊆ (free_vars A - fmdom' φ) ∪ ⋃(free_vars ` fmran' φ)›
proof (induct φ A rule: substitute.induct)
  case (1 θ x α)
  then show ?case
    by (cases ‹θ $$ (x, α)›) (auto simp: fmran'I fmdom'_notI)
next
  case (2 θ c α)
  then show ?case
    by simp
next
  case (3 θ A B)
  then show ?case
    by auto
next
  case (4 θ x α A)
  then show ?case
  proof (cases ‹(x, α) ∈ fmdom' θ›)
    case True
    then have ind: ‹free_vars (❙S (fmdrop (x, α) θ) A) ⊆
                      free_vars A - fmdom' (fmdrop (x, α) θ)
                       ∪ ⋃ (free_vars ` fmran' (fmdrop (x, α) θ))›
      using 4 by auto
    {
      fix y β
      assume yβ_free: ‹(y,β) ∈ free_vars (❙S (fmdrop (x, α) θ) A) - {(x, α)}›
      then have yβ_free': ‹(y,β) ∈ free_vars (❙S (fmdrop (x, α) θ) A)›
        by auto
      have not: ‹(y,β) ≠ (x,α)›
        using yβ_free by auto
      from yβ_free' have ‹(y,β) ∈ free_vars A - fmdom' (fmdrop (x, α) θ)
                                   ∪ ⋃ (free_vars ` fmran' (fmdrop (x, α) θ))›
        using ind by auto
      then have ‹(y,β) ∈ ((free_vars A - {(x, α)}) - fmdom' θ) ∪ ⋃ (free_vars ` fmran' θ)›
      proof
        assume ind_l: ‹(y, β) ∈ free_vars A - fmdom' (fmdrop (x, α) θ)›
        then have fv: ‹(y, β) ∈ (free_vars A - {(x, α)})›
          using not by blast
        then have ‹(y, β) ∉ fmdom' θ›
          using ind_l by force
        then show ‹(y,β) ∈ ((free_vars A - {(x, α)}) - fmdom' θ) ∪ ⋃ (free_vars ` fmran' θ)›
          using fv by auto
      next
        assume ‹(y, β) ∈ ⋃ (free_vars ` fmran' (fmdrop (x, α) θ))›
        then have ‹(y,β) ∈  ⋃ (free_vars ` fmran' θ)›
          by (meson Union_mono fmran'_fmdrop_subset image_mono subsetD)
        then show ‹(y, β) ∈ ((free_vars A - {(x, α)}) - fmdom' θ) ∪ ⋃ (free_vars ` fmran' θ)›
          by blast
      qed
    }
    then have ‹free_vars (❙S (fmdrop (x, α) θ) A) - {(x, α)}
                ⊆ free_vars A - {(x, α)} - fmdom' θ ∪ ⋃ (free_vars ` fmran' θ)›
      by (metis subsetI surj_pair)
    then show ?thesis
      using True by auto
  next
    case False
    then show ?thesis
      using 4 by auto
  qed
qed

section ‹Hintikka›

locale MyHintikka = Hintikka map_con cons_form is_param Kinds H
  for H :: ‹form set›
begin

lemmas confl = sat⇩H[of C.kind]
  and alpha = sat⇩H[of A.kind] 
  and beta = sat⇩H[of B.kind] 
  and gamma = sat⇩H[of G.kind]
  and delta = sat⇩H[of D.kind]

(*
  With CNot at complete formulas, not just atoms, this is free.
  Notably, this does not necessarily imply derivational consistency: ‹¬ (H ⊢ A ∧ H ⊢ ∼⇧𝒬 A)›
*)
theorem consistent:
  assumes ‹A ∈ wffs⇘o⇙›
  shows ‹A ∉ H ∨ ∼⇧𝒬 A ∉ H›
  using assms confl by (force intro: CNot[of A])

lemma cFalse: ‹F⇘o⇙ ∉ H›
  using confl by (force intro: CFalse)

lemma cBool:
  assumes ‹A ∈ wffs⇘o⇙›
    and ‹A ∈ H›
  shows ‹A =⇘o⇙ T⇘o⇙ ∈ H›
  using assms alpha by (fastforce intro!: CBool[of A])

lemma cTrans:
  assumes ‹A ∈ wffs⇘α⇙› ‹B ∈ wffs⇘α⇙› ‹C ∈ wffs⇘α⇙›
    and ‹A =⇘α⇙ B ∈ H› ‹B =⇘α⇙ C ∈ H›
  shows ‹A =⇘α⇙ C ∈ H›
  using assms alpha by (force intro: CTrans[of A α B])

lemma cCong:
  assumes ‹A ∈ wffs⇘α⇙› ‹B ∈ wffs⇘α⇙› ‹C ∈ wffs⇘α → β⇙›
    and ‹A =⇘α⇙ B ∈ H›
  shows ‹C · A =⇘β⇙ C · B ∈ H›
  using assms alpha by (force intro: CCong[of A α B C β])

lemma cIota:
  assumes ‹A ∈ wffs⇘i⇙›
  shows ‹(ι · (Q⇘i⇙ · A) =⇘i⇙ A) ∈ H›
  using assms alpha by (force intro: CIota[of A])

lemma cSubst:
  assumes ‹A ∈ wffs⇘α⇙› ‹B ∈ wffs⇘β⇙›
    and ‹free_vars A = {}›
  shows ‹(λx⇘α⇙. B) · A =⇘β⇙ substitute {(x, α) ↣ A} B ∈ H›
  using assms alpha by (fastforce intro!: CSubst[of A α B β x])

lemma cExt:
  assumes ‹A ∈ wffs⇘α → β⇙› ‹B ∈ wffs⇘α → β⇙› ‹C ∈ wffs⇘α⇙›
    and ‹(A =⇘α → β⇙ B) ∈ H›
  shows ‹(A · C =⇘β⇙ B · C) ∈ H›
  using assms gamma by (force intro: CExt[of A α])

lemma cIneq:
  assumes ‹A ∈ wffs⇘α → β⇙› ‹B ∈ wffs⇘α → β⇙›
    and ‹∼⇧𝒬 (A =⇘α → β⇙ B) ∈ H›
  shows ‹∃c. is_param c ∧ ∼⇧𝒬 (A · ⦃c⦄⇘α⇙ =⇘β⇙ B · ⦃c⦄⇘α⇙) ∈ H›
proof -
  have ‹∼⇧𝒬 (A =⇘α → β⇙ B) ∈ wffs⇘o⇙ ∧ ineq_match (∼⇧𝒬 (A =⇘α → β⇙ B)) (α, β, A, B)›
    using assms(1-2) by blast
  then have ‹delta (∼⇧𝒬 (A =⇘α → β⇙ B)) c = [ ∼⇧𝒬 (A · ⦃c⦄⇘α⇙ =⇘β⇙ B · ⦃c⦄⇘α⇙) ]› for c
    using ineq_match_delta by fast
  then show ?thesis
    using delta assms(3) by (metis list.set_intros(1,2) sat⇩H_WitsE subset_code(1))
qed

lemma complete:
  assumes ‹A ∈ wffs⇘o⇙›
  shows ‹A ∈ H ∨ ∼⇧𝒬 A ∈ H›
  using assms beta by (fastforce intro!: CLEM[of A])

lemma cRefl:
  assumes ‹A ∈ wffs⇘α⇙›
  shows ‹A =⇘α⇙ A ∈ H›
  using assms alpha by (force intro: CRefl[of A α])

lemma cIrr:
  assumes ‹A ∈ wffs⇘α⇙›
  shows ‹∼⇧𝒬 (A =⇘α⇙ A) ∉ H›
  using assms by (metis consistent cRefl equality_wff)

lemma cTop: ‹T⇘o⇙ ∈ H›
  using cRefl by auto

lemma cSym:
  assumes ‹A ∈ wffs⇘α⇙› ‹B ∈ wffs⇘α⇙›
    and ‹A =⇘α⇙ B ∈ H›
  shows ‹B =⇘α⇙ A ∈ H›
  using assms cCong[of A α B _ o] cIrr[of B α] cTrans[of ‹F⇘o⇙› o] complete false_wff Q_wff
  by (metis neg_def equality_of_type_def wffs_of_type_intros(3))

lemma cEqv:
  assumes ‹A ∈ wffs⇘o⇙› ‹B ∈ wffs⇘o⇙›
    and ‹A ∈ H› ‹B ∈ H›
  shows ‹A ≡⇧𝒬 B ∈ H›
  using assms cBool cSym cTrans consistent complete unfolding equivalence_def
  by (metis true_wff)

lemma extensionally_complete_membership: ‹extensionally_complete_membership H›
  unfolding extensionally_complete_membership_def
proof (intro allI impI)
  fix A B α β
  assume *: ‹is_closed_wff_of_type A (β → α)› ‹is_closed_wff_of_type B (β → α)›
  then consider (pos) ‹A =⇘β → α⇙ B ∈ H› | (neg) ‹∼⇧𝒬 (A =⇘β → α⇙ B) ∈ H›
    using complete by blast
  then show ‹∃C. is_closed_wff_of_type C β ∧ ((A · C =⇘α⇙ B · C) ∈ H ⟶ (A =⇘β → α⇙ B) ∈ H)›
  proof cases
    case pos
    then show ?thesis
      by force
  next
    case neg
    then obtain c where ‹is_param c› ‹∼⇧𝒬 (A · ⦃c⦄⇘β⇙ =⇘α⇙ B · ⦃c⦄⇘β⇙) ∈ H›
      using * cIneq unfolding is_closed_wff_of_type_def by meson
    then show ?thesis
      using * consistent unfolding is_closed_wff_of_type_def
      by (metis equality_wff free_vars_form.simps(2) wffs_of_type_intros(2,3))
  qed
qed

section ‹The universe of Sets›

definition V_of_form :: ‹form ⇒ V› where
  ‹V_of_form ≡ SOME V_of. inj V_of›

definition V_of_form_set :: ‹form set ⇒ V› where
  ‹V_of_form_set As ≡ set (V_of_form ` As)›

fun
  𝒟 :: ‹type ⇒ V› and
  𝒱 :: ‹form ⇒ type ⇒ V› and
  get_rep :: ‹V ⇒ type ⇒ form› where
  ‹𝒟 o = 𝔹›
| ‹𝒟 i = set {𝒱 A i | A. is_closed_wff_of_type A i}›
| ‹𝒟 (β → α) = set {𝒱 A (β → α) | A. is_closed_wff_of_type A (β → α)}›
| ‹𝒱 A o = (if A ∈ H then ❙T else ❙F)›
| ‹𝒱 A i = V_of_form_set {B. is_closed_wff_of_type B i ∧ A =⇘i⇙ B ∈ H}›
| ‹𝒱 A (β → α) = (❙λVCβ ❙: 𝒟 β❙. (let C = get_rep VCβ β in 𝒱 (A · C) α))›
| ‹get_rep VCβ β = (SOME C. 𝒱 C β = VCβ ∧ is_closed_wff_of_type C β)›

lemma one_o: ‹𝒟 o = set {𝒱 A o| A. is_closed_wff_of_type A o}›
proof -
  have ‹{bool_to_V True, bool_to_V False} ⊆ {𝒱 A o |A. is_closed_wff_of_type A o}›
    using cFalse cTop false_wff true_wff by fastforce
  moreover have ‹{bool_to_V True, bool_to_V False} ⊇ {𝒱 A o |A. is_closed_wff_of_type A o}›
    by auto
  ultimately show ?thesis
    by (metis (lifting) 𝒟.simps(1) bottom_def set_eq_subset top_def
        two_valued_boolean_algebra_universe_def)
qed

lemma bool_to_V_distinct: ‹bool_to_V False ≠ bool_to_V True›
  by (simp add: inj_eq)

lemma two_o:
  assumes ‹A ∈ wffs⇘o⇙› ‹B ∈ wffs⇘o⇙›
  shows ‹𝒱 A o = 𝒱 B o ⟷ A ≡⇧𝒬 B ∈ H›
proof
  show ‹𝒱 A o = 𝒱 B o ⟹ A ≡⇧𝒬 B ∈ H›
    using assms cEqv cSym cTrans complete
  by (metis 𝒱.simps(1) bool_to_V_distinct bottom_def equality_of_type_def
      equivalence_def false_wff neg_def top_def)
next
  show ‹A ≡⇧𝒬 B ∈ H ⟹ 𝒱 A o = 𝒱 B o›
    unfolding equivalence_def 𝒱.simps 
    using assms consistent cSym cTrans complete 
    by (metis equality_of_type_def false_wff neg_def)
qed

lemma one_i: ‹𝒟 i = set {𝒱 A i| A. is_closed_wff_of_type A i}›
  by simp (* Holds directly by definition *)

lemma inj_V_of_form: ‹inj V_of_form›
  by (metis V_of_form_def embeddable_class.ex_inj someI_ex)

lemma V_of_form_set_inj:
  assumes ‹V_of_form_set As = V_of_form_set Bs›
  shows ‹As = Bs›
proof -
  have ‹small (V_of_form ` As)›
    by simp
  have ‹small (V_of_form ` Bs)›
    by simp
  show ?thesis
    using V_of_form_set_def inj_V_of_form assms inj_image_eq_iff by fastforce
qed

lemma two_i:
  assumes ‹is_closed_wff_of_type A i›
    and ‹is_closed_wff_of_type B i›
  shows ‹𝒱 A i = 𝒱 B i ⟷ A =⇘i⇙ B ∈ H›
proof -
  have A: ‹small {A. is_closed_wff_of_type A i ∧ A =⇘i⇙ B ∈ H}›
    by (simp add: setcompr_eq_image)
  have B: ‹small {B. is_closed_wff_of_type B i ∧ A =⇘i⇙ B ∈ H}›
    by (simp add: setcompr_eq_image)

  show ?thesis
  proof
    assume ‹𝒱 A i = 𝒱 B i›
    then have ‹{B'. is_closed_wff_of_type B' i ∧ A =⇘i⇙ B' ∈ H} = {A'. is_closed_wff_of_type A' i ∧ B =⇘i⇙ A' ∈ H}›
      using V_of_form_set_inj by simp
    then have ‹{B'. is_closed_wff_of_type B' i ∧ A =⇘i⇙ B' ∈ H} = {A'. is_closed_wff_of_type A' i ∧ A' =⇘i⇙ B ∈ H}›
      using assms cSym by auto
    then have ‹∀C. is_closed_wff_of_type C i ⟶ A =⇘i⇙ C ∈ H ⟷ C =⇘i⇙ B ∈ H›
      by blast
    moreover have ‹B =⇘i⇙ B ∈ H›
      using assms cRefl by blast+
    ultimately show ‹A =⇘i⇙ B ∈ H›
      using assms cTrans by blast
  next
    assume ‹A =⇘i⇙ B ∈ H›
    then have ‹∀C. is_closed_wff_of_type C i ⟶ A =⇘i⇙ C ∈ H ⟷ B =⇘i⇙ C ∈ H›
      using assms cSym cTrans unfolding is_closed_wff_of_type_def by meson
    then show ‹𝒱 A i = 𝒱 B i›
      using assms by (metis (mono_tags, lifting) Collect_cong 𝒱.simps(2))
  qed
qed

lemma one_fun:
  ‹𝒟 (β → α) = set {𝒱 A (β → α)| A. is_closed_wff_of_type A (β → α)}›
  by simp (* Holds directly by definition *)

lemma fun_ext_vfuncset:
  assumes ‹f ∈ elts (A ⟼ B)› ‹g ∈ elts (A ⟼ B)›
    and ‹⋀x. x ∈ elts A ⟹ app f x = app g x›
  shows ‹f = g›
  using assms ZFC_Cardinals.fun_ext by auto

lemma well_typed:
  assumes ‹is_closed_wff_of_type A γ›
  shows ‹𝒱 A γ ∈ elts (𝒟 γ)›
  using assms by (induct γ) (auto simp: setcompr_eq_image)

subsection ‹1‹γ››

lemma one_gamma: ‹𝒟 γ = set {𝒱 A γ| A. is_closed_wff_of_type A γ}›
  using one_i one_o one_fun by (cases γ) auto

lemma wff_for_elts:
  assumes ‹x ∈ elts (𝒟 α)›
  shows ‹∃A. is_closed_wff_of_type A α ∧ 𝒱 A α = x›
proof -
  have ‹∀x ∈ elts (𝒟 α). ∃C. 𝒱 C α = x ∧ is_closed_wff_of_type C α›
    using one_gamma by auto
  then show ?thesis
    using assms by fast
qed

lemma fun_typed:
  shows ‹elts (𝒟 (β → α)) ⊆ elts (𝒟 β ⟼ 𝒟 α)›
proof
  fix f
  assume f: ‹f ∈ elts (𝒟 (β → α))›
  have sma: ‹small {❙λVCβ❙:𝒟 β ❙. 𝒱 (A · (SOME C. 𝒱 C β = VCβ ∧ is_closed_wff_of_type C β)) α |A. is_closed_wff_of_type A (β → α)}›
    by (simp add: setcompr_eq_image)

  from f obtain A where A:
    ‹f = (❙λVCβ❙:𝒟 β ❙. 𝒱 (A · (SOME C. 𝒱 C β = VCβ ∧ is_closed_wff_of_type C β)) α)›
    ‹is_closed_wff_of_type A (β → α)›
    using sma by auto

  {
    fix VCβ
    assume ‹VCβ ∈ elts (𝒟 β)›
    then have ‹∃C. 𝒱 C β = VCβ ∧ is_closed_wff_of_type C β›
      using wff_for_elts by blast
    then obtain C where C: ‹(SOME C. 𝒱 C β = VCβ ∧ is_closed_wff_of_type C β) = C› ‹𝒱 C β = VCβ› ‹is_closed_wff_of_type C β›
      by (metis (mono_tags, lifting) someI)
    have ‹is_closed_wff_of_type (A · C) α›
      using A(2) C(3) by auto
    then have ‹𝒱 (A · C) α ∈ elts (𝒟 α)›
      using well_typed by blast
    then have ‹𝒱 (A · (SOME C. 𝒱 C β = VCβ ∧ is_closed_wff_of_type C β)) α ∈ elts (𝒟 α)›
      using C by meson
  }
  then show ‹f ∈ elts (𝒟 β ⟼ 𝒟 α)›
    unfolding A(1) is_closed_wff_of_type_def by (simp add: VPi_I)
qed

subsection ‹2‹γ››

lemma two_gamma:
  assumes ‹is_closed_wff_of_type A γ›
    and ‹is_closed_wff_of_type B γ›
  shows ‹𝒱 A γ = 𝒱 B γ ⟷ A =⇘γ⇙ B ∈ H›
  using assms
proof (induction γ arbitrary: A B)
  case TInd
  then show ?case
    using two_i by blast
next
  case TBool
  then show ?case
    using two_o by simp
next
  case (TFun β α)

  {
    fix A B C
    assume ‹is_closed_wff_of_type A (β → α)›
      ‹is_closed_wff_of_type B β›
      ‹is_closed_wff_of_type C β›
      ‹𝒱 B β = 𝒱 C β›
    then have ‹𝒱 (A · B) α = 𝒱 (A · C) α›
      using cCong wffs_of_type_intros(3) TFun.IH(1,2)
      by auto
  }
  note unambiguity = this

  show ‹𝒱 A (β → α) = 𝒱 B (β → α) ⟷ A =⇘β → α⇙ B ∈ H›
  proof
    assume ‹A =⇘β → α⇙ B ∈ H›
    then have nice: ‹⋀C. is_closed_wff_of_type C β ⟹ A · C =⇘α⇙ B · C ∈ H›
      using ‹is_closed_wff_of_type A (β → α)› 
        ‹is_closed_wff_of_type B (β → α)› cExt 
      by blast
    {
      fix C
      assume C: ‹is_closed_wff_of_type C β›
      then have rep: ‹𝒱 (get_rep (𝒱 C β) β) β = 𝒱 C β›
        by (metis (mono_tags, lifting) get_rep.simps some_eq_ex)
      moreover have 𝒱C: ‹𝒱 C β ∈ elts (𝒟 β)›
        using C by (simp add: well_typed)
      moreover have ‹𝒱 (A · (SOME Ca. 𝒱 Ca β = 𝒱 C β ∧ is_closed_wff_of_type Ca β)) α = 𝒱 (A · C) α›
        using TFun(3) C unambiguity by (metis (mono_tags, lifting) tfl_some)
      ultimately have ‹(𝒱 A (β → α)) ∙ (𝒱 C β) = 𝒱 (A · C) α›
        by simp
      moreover have ‹is_closed_wff_of_type (B · C) α›
        using TFun(4) C by auto
      then have ‹𝒱 (A · C) α = 𝒱 (B · C) α›
        using nice[OF C] TFun(3) C TFun(2)[of ‹A · C› ‹B · C›] by auto
      moreover have ‹𝒱 (B · C) α = 𝒱 (B · (SOME Ca. 𝒱 Ca β = 𝒱 C β ∧ is_closed_wff_of_type Ca β)) α›
        using TFun(4) C unambiguity by (metis (mono_tags, lifting) tfl_some)
      then have ‹𝒱 (B · C) α = (𝒱 B (β → α)) ∙ (𝒱 C β)›
        using rep 𝒱C by simp
      ultimately have ‹(𝒱 A (β → α)) ∙ (𝒱 C β) = (𝒱 B (β → α)) ∙ (𝒱 C β)›
        by simp
    }
    note C_application = this

    show ‹𝒱 A (β → α) = 𝒱 B (β → α)›
    proof (rule fun_ext_vfuncset[of _ ‹𝒟 β› ‹𝒟 α›])
      show ‹𝒱 A (β → α) ∈ elts (𝒟 β ⟼ 𝒟 α)›
        using fun_typed well_typed TFun(3) unambiguity by (metis subsetD)
    next
      show ‹𝒱 B (β → α) ∈ elts (𝒟 β ⟼ 𝒟 α)›
        using fun_typed well_typed TFun(4) unambiguity by (metis subsetD)
    next
      fix VCβ
      assume ‹VCβ ∈ elts (𝒟 β)›
      then obtain C where ‹𝒱 C β = VCβ ∧ is_closed_wff_of_type C β›
        using wff_for_elts by blast
      then show ‹𝒱 A (β → α) ∙ VCβ = 𝒱 B (β → α) ∙ VCβ›
        using C_application by blast
    qed
  next
    assume ‹𝒱 A (β → α) = 𝒱 B (β → α)›
    {
      fix C
      assume C: ‹is_closed_wff_of_type C β›
      then have rep: ‹𝒱 (get_rep (𝒱 C β) β) β = 𝒱 C β›
        by (metis (mono_tags, lifting) get_rep.simps some_eq_ex)
      moreover have 𝒱C: ‹𝒱 C β ∈ elts (𝒟 β)›
        using C by (simp add: well_typed)
      moreover have ‹𝒱 (A · (SOME Ca. 𝒱 Ca β = 𝒱 C β ∧ is_closed_wff_of_type Ca β)) α = 𝒱 (A · C) α›
        using TFun(3) C unambiguity by (metis (mono_tags, lifting) tfl_some)
      ultimately have ‹𝒱 (A · C) α = (𝒱 A (β → α)) ∙ (𝒱 C β)›
        by simp
      then have ‹𝒱 (A · C) α = (𝒱 B (β → α)) ∙ (𝒱 C β)›
        using ‹𝒱 A (β → α) = 𝒱 B (β → α)› by presburger

      moreover have ‹𝒱 (B · C) α = 𝒱 (B · (SOME Ca. 𝒱 Ca β = 𝒱 C β ∧ is_closed_wff_of_type Ca β)) α›
        using TFun(4) C unambiguity by (metis (mono_tags, lifting) tfl_some)
      then have ‹𝒱 (B · C) α = (𝒱 B (β → α)) ∙ (𝒱 C β)›
        using rep 𝒱C by simp
      ultimately have ‹𝒱 (A · C) α = 𝒱 (B · C) α›
        by simp
      then have ‹A · C =⇘α⇙ B · C ∈ H›
        using TFun.IH(2) TFun(3,4) C wffs_of_type_intros(3) by force
    }
    then show ‹A =⇘β → α⇙ B ∈ H›
      using TFun(3,4) extensionally_complete_membership
      unfolding extensionally_complete_membership_def is_closed_wff_of_type_def
      by meson
  qed
qed

lemma unambiguity:
  assumes ‹is_closed_wff_of_type A (β → α)›
    and ‹is_closed_wff_of_type B β›
    and ‹is_closed_wff_of_type C β›
    and ‹𝒱 B β = 𝒱 C β›
    shows ‹𝒱 (A · B) α = 𝒱 (A · C) α›
  using assms cCong wffs_of_type_intros(3) two_gamma by auto


subsection ‹M is interpretation›

fun 𝒥 :: ‹nat × Syntax.type ⇒ V› where
  ‹𝒥 (c,τ) = 𝒱 (FCon (c,τ)) τ›

(* Mapping primitive constants into 𝒟⇩α*)
lemma non_logical_constant_denotation_𝒱:
  assumes ‹¬ is_logical_constant (c, α)›
  shows ‹𝒱 (FCon (c, α)) α ∈ elts (𝒟 α)›
  using assms well_typed 
  by fastforce

lemma non_logical_constant_denotation_𝒥:
  assumes ‹¬ is_logical_constant (c, α)›
  shows ‹𝒥 (c, α) ∈ elts (𝒟 α)›
  using assms non_logical_constant_denotation_𝒱 
  unfolding 𝒥.simps by auto

lemma function_domain: ‹𝒟 (α → β) ≤ 𝒟 α ⟼ 𝒟 β›
  using fun_typed by blast

lemma domain_nonemptiness: ‹𝒟 α ≠ 0›
  by (metis wffs_of_type_intros(2) well_typed 
      is_closed_wff_of_type_def elts_0 all_not_in_conv free_vars_form.simps(2))

lemma domain_frame: ‹frame 𝒟›
  using 𝒟.simps(1) domain_nonemptiness frame.intro function_domain by blast

lemma distrib_𝒱_app:
  assumes ‹is_closed_wff_of_type A (α → β)› ‹is_closed_wff_of_type B α›
  shows ‹𝒱 (A · B) β = 𝒱 A (α → β) ∙ 𝒱 B α›
proof -
 have *: ‹VLambda (𝒟 α) b ∙ 𝒱 B α = b (𝒱 B α)› for b
   using assms(2) well_typed ZFC_Cardinals.beta by meson
 
  have ‹𝒱 B α = 𝒱 C α ⟹ 𝒱 (A · B) β = 𝒱 (A · C) β›
    if ‹is_closed_wff_of_type C α› for C
    using assms that unambiguity by blast
  moreover have ‹∃C. 𝒱 C α = 𝒱 B α ∧ is_closed_wff_of_type C α›
    using assms(2) by blast
  ultimately show ?thesis
    using assms(2) unfolding 𝒱.simps get_rep.simps Let_def *
    by (metis (mono_tags, lifting) someI_ex)
qed

lemma Q_denotation_𝒱_two:
  assumes ‹x ∈ elts (𝒟 α)› ‹y ∈ elts (𝒟 α)›
  shows ‹𝒱 (Q⇘α⇙) (α→α→o) ∙ x ∙ y = (q⇘α⇙⇗𝒟⇖) ∙ x ∙ y›
proof -
  obtain A B where A: ‹is_closed_wff_of_type A α› ‹𝒱 A α = x›
    and B: ‹is_closed_wff_of_type B α› ‹𝒱 B α = y›
    using wff_for_elts assms by meson

  have Q:
    ‹is_closed_wff_of_type (Q⇘α⇙) (α→α→o)›
    ‹is_closed_wff_of_type (Q⇘α⇙ · A) (α→o)›
    using A unfolding is_closed_wff_of_type_def by auto

  have ‹𝒱 A α = 𝒱 B α ⟷ A =⇘α⇙ B ∈ H›
    using A B two_gamma by blast
  also have ‹… ⟷ 𝒱 (Q⇘α⇙ · A · B) o = ❙T›
    by (simp add: bool_to_V_distinct)
  also have ‹… ⟷ 𝒱 (Q⇘α⇙) (α→α→o) ∙ 𝒱 A α ∙ 𝒱 B α = ❙T›
    using distrib_𝒱_app A B Q by metis
  finally have ‹𝒱 (Q⇘α⇙) (α→α→o) ∙ 𝒱 A α ∙ 𝒱 B α = ❙T ⟷ 𝒱 A α = 𝒱 B α› ..
  then show ?thesis
    using A(2) B(2) assms(1,2) domain_frame frame.identity_relation_def 
      frame.one_element_function_def 
    by fastforce
qed

lemma Q_denotation_𝒱_one:
  assumes ‹x ∈ elts (𝒟 α)›
  shows ‹𝒱 (Q⇘α⇙) (α→α→o) ∙ x = (q⇘α⇙⇗𝒟⇖) ∙ x›
proof (rule fun_ext)
  show ‹𝒱 Q⇘α⇙ (α → α → o) ∙ x ∈ elts (VPi (𝒟 α) (λ_. 𝒟 o))›
    using assms by (simp add: VPi_I)
next
  show ‹(q⇘α⇙⇗𝒟⇖) ∙ x ∈ elts (VPi (𝒟 α) (λ_. 𝒟 o))›
    using assms 
    by (metis VPi_D domain_frame frame.identity_relation_is_domain_respecting)
next
  show ‹⋀y. y ∈ elts (𝒟 α) ⟹ 𝒱 Q⇘α⇙ (α → α → o) ∙ x ∙ y = (q⇘α⇙⇗𝒟⇖) ∙ x ∙ y›
    using Q_denotation_𝒱_two assms .
qed

(* Q is identity relation*)
lemma Q_denotation_𝒱: ‹𝒱 (Q⇘α⇙) (α→α→o) = q⇘α⇙⇗𝒟⇖›
proof (rule fun_ext)
  show ‹𝒱 Q⇘α⇙ (α → α → o) ∈ elts (VPi (𝒟 α) (λ_. VPi (𝒟 α) (λ_. 𝒟 o)))›
    by (simp add: VPi_I)
next
  show ‹q⇘α⇙⇗𝒟⇖ ∈ elts (VPi (𝒟 α) (λ_. VPi (𝒟 α) (λ_. 𝒟 o)))›
    using domain_frame frame.identity_relation_is_domain_respecting by blast
next
  show ‹⋀x. x ∈ elts (𝒟 α) ⟹ 𝒱 Q⇘α⇙ (α → α → o) ∙ x = (q⇘α⇙⇗𝒟⇖) ∙ x›
    using Q_denotation_𝒱_one .
qed

lemma Q_denotation_𝒥: ‹𝒥 (Q_constant_of_type α) = q⇘α⇙⇗𝒟⇖›
  using Q_denotation_𝒱 by auto

(* ι is one element set*)
lemma ι_denotation_𝒱: ‹frame.is_unique_member_selector 𝒟 (𝒱 ι ((i→o)→i))›
  unfolding frame.is_unique_member_selector_def[OF domain_frame]
proof safe
  fix x
  assume *: ‹x ∈ elts (𝒟 i)›
  then obtain A where A: ‹is_closed_wff_of_type A i› ‹𝒱 A i = x›
    by (meson wff_for_elts)
  then have ‹ι · (Q⇘i⇙ · A) =⇘i⇙ A ∈ H›
    using cIota by blast
  moreover have ‹is_closed_wff_of_type ι ((i → o) → i)›
    by auto
  moreover have ‹is_closed_wff_of_type (Q⇘i⇙) (i→i→o)›
    by auto
  moreover have ‹is_closed_wff_of_type (Q⇘i⇙ · A) (i→o)›
    using A by auto
  moreover have ‹is_closed_wff_of_type (ι · (Q⇘i⇙ · A)) i›
    using A by auto
  ultimately show ‹𝒱 ι ((i → o) → i) ∙ {x}⇘i⇙⇗𝒟⇖ = x›
    using A * two_gamma
    by (metis distrib_𝒱_app Q_denotation_𝒱 ZFC_Cardinals.beta 
        domain_frame frame.identity_relation_def)
qed

lemma ι_denotation_𝒥: ‹frame.is_unique_member_selector 𝒟 (𝒥 iota_constant)›
  by (metis 𝒥.simps ι_denotation_𝒱 iota_constant_def iota_def)

(* M constitutes an interpretation (premodel) *)
sublocale premodel 𝒟 𝒥
  using function_domain domain_nonemptiness Q_denotation_𝒥 ι_denotation_𝒥
    non_logical_constant_denotation_𝒥
  by unfold_locales auto

subsection ‹M is general model›

(* Andrews asks for "the first formula such that". But SOME formula is sufficient. *)
definition fun_E :: ‹(var ⇒ V) ⇒ (var ⇒ form)› 
  where ‹fun_E φ ≡ λ(x,δ). (SOME A. φ (x,δ) = 𝒱 A δ ∧ is_closed_wff_of_type A δ)›

definition map_E :: ‹var set ⇒ (var ⇒ V) ⇒ (var ⇀ form)›
  where ‹map_E xs φ ≡ map_restrict_set xs (Some ∘ fun_E φ)›

definition subst_E :: ‹var set ⇒ (var ⇒ V) ⇒ substitution›
  where ‹subst_E xs φ ≡ Abs_fmap (map_E xs φ)›

definition θ⇩E :: ‹(var ⇒ V) ⇒ form ⇒ substitution›
  where ‹θ⇩E φ C ≡ subst_E (free_vars C) φ›

definition close_E :: ‹form ⇒ (var ⇒ V) ⇒ form›
  where ‹close_E C φ ≡ ❙S (θ⇩E φ C) C›

definition type_of :: ‹form ⇒ type› 
  where ‹type_of A ≡ (SOME γ. A ∈ wffs⇘γ⇙)›

definition 𝒱φ :: ‹(var ⇒ V) ⇒ form ⇒ V› (‹𝒱⇘_⇙›)
  where ‹𝒱⇘φ⇙ C ≡ 𝒱 (close_E C φ) (type_of C)›

lemma fmdom'_map_restrict_set:
  assumes ‹finite xs›
    and ‹x ∈ fmdom' (Abs_fmap (map_restrict_set xs (Some ∘ f)))›
  shows ‹x ∈ xs›
  using assms
proof (induction)
  case empty
  have None: ‹⋀g. (map_filter (λa. False) (λa. Some (g a))) = (λa. None)›
    by (simp add: Finite_Map.map_filter_def)
  from empty show ?case
    unfolding map_restrict_set_def None
    by (metis (no_types, lifting) HOL.ext Finite_Map.map_filter_def empty_iff fmdom'_empty fmempty_def)
next
  case (insert y F)
  have None: ‹⋀g. (map_filter (λa. False) (λa. Some (g a))) = (λa. None)›
    by (simp add: Finite_Map.map_filter_def)
  show ?case
  proof (cases ‹x = y›)
    case True
    then show ?thesis
      by auto
  next
    case False
    have ‹finite (dom (map_restrict_set F (Some ∘ f)))›
      by (metis Finite_Map.map_filter_def domIff finite_subset 
          insert.hyps(1) map_restrict_set_def subsetI)
    have finite_dom_mapr_insert: ‹finite (dom (map_restrict_set (insert y F) (Some ∘ f)))›
      by (metis Finite_Map.map_filter_def domIff finite_insert 
          finite_subset insert.hyps(1) map_restrict_set_def subsetI)
    from insert(4) have ‹x ∈ dom (map_restrict_set (insert y F) (Some ∘ f))›
      by (metis finite_dom_mapr_insert eq_onp_same_args fmdom'.abs_eq)
    then have ‹x ∈ dom (map_restrict_set F (Some ∘ f))›
      by (simp add: False Finite_Map.map_filter_def domIff map_restrict_set_def)
    then have ‹x ∈ fmdom' (Abs_fmap (map_restrict_set F (Some ∘ f)))›
      by (simp add: ‹finite (dom (map_restrict_set F (Some ∘ f)))› eq_onp_same_args fmdom'.abs_eq)
    then show ?thesis
      using insert by blast
  qed
qed

lemma θ⇩E_is_substitution:
  assumes ‹φ ↝ 𝒟›
  shows ‹is_substitution (θ⇩E φ C)›
proof safe
  fix x β
  assume a: ‹(x, β) ∈ fmdom' (θ⇩E φ C)›

  have *: ‹∃A. φ (x,β) = 𝒱 A β ∧ is_closed_wff_of_type A β›
    using assms by (metis wff_for_elts frame.is_assignment_def frame_axioms)

  have fc: ‹finite (free_vars C)›
    by (simp add: free_vars_form_finiteness)

  have ‹dom (map_E (free_vars C) φ) = free_vars C›
    unfolding map_E_def by (auto simp: Finite_Map.map_filter_def map_restrict_set_def split: if_splits)

  from a have b: ‹(x, β) ∈ free_vars C›
    unfolding θ⇩E_def subst_E_def map_E_def
    by (metis fmdom'_map_restrict_set free_vars_form_finiteness)

  have ‹fun_E φ (x, β) ∈ wffs⇘β⇙›
    using * unfolding case_prod_conv fun_E_def is_closed_wff_of_type_def
    by (metis (mono_tags, lifting) tfl_some)
  then have ‹(map_E (free_vars C) φ) (x, β) ∈ Some ` wffs⇘β⇙›
    using b unfolding fun_E_def map_E_def
    by (simp add: Finite_Map.map_filter_def map_restrict_set_def)
  then have
    ‹∃xa. xa ∈ wffs⇘β⇙ ∧ map_E (free_vars C) φ (x, β) = Some xa›
    by blast
  then have
    ‹∃xa. subst_E (free_vars C) φ $$ (x, β) = Some xa ∧ xa ∈ wffs⇘β⇙›
    unfolding image_def subst_E_def using ‹dom (map_E (free_vars C) φ) = free_vars C›
    by (metis Abs_fmap_inverse  free_vars_form_finiteness mem_Collect_eq)
  then have
    ‹∃xa. subst_E (free_vars C) φ $$ (x, β) = Some xa ∧ xa ∈ wffs⇘β⇙›
    unfolding subst_E_def by auto
  then have ‹subst_E (free_vars C) φ $$! (x, β) ∈ wffs⇘β⇙›
    by auto
  then show ‹((θ⇩E φ C) $$! (x, β)) ∈ wffs⇘β⇙›
    using θ⇩E_def by auto
qed

lemma assignment_some_wff:
  assumes φ: ‹φ ↝ 𝒟›
  obtains E where
    ‹(SOME A. φ (x, α) = 𝒱 A α ∧ is_closed_wff_of_type A α) = E›
    ‹is_closed_wff_of_type E α› ‹φ (x,α) = 𝒱 E α›
proof -
  have ‹∃A. φ (x, α) = 𝒱 A α ∧ is_closed_wff_of_type A α›
    using assms unfolding is_assignment_def by (metis wff_for_elts)
  then show ?thesis
    using that by (metis (mono_tags, lifting) someI_ex)
qed

(* Removing because Sledgehammer seems to struggle with this notation. *)
no_notation substitute (‹❙S _ _› [51, 51])

lemma finite_dom_map_E:
  assumes ‹finite xs›
  shows ‹finite (dom (map_E xs φ))›
  using assms unfolding map_E_def fun_E_def
  by (metis (no_types, lifting) Finite_Map.map_filter_def 
      map_restrict_set_def domIff rev_finite_subset subsetI)

lemma finite_dom_map_E_free_vars:
  fixes C :: form
  shows ‹finite (dom (map_E (free_vars C) φ))›
  using finite_dom_map_E free_vars_form_finiteness 
  by simp

lemma θ⇩E_lookup: ‹θ⇩E φ C $$ x = map_E (free_vars C) φ x›
  by (simp add: Abs_fmap_inverse θ⇩E_def finite_dom_map_E_free_vars subst_E_def)

lemma subst_E_Some:
  assumes ‹finite xs›
    and ‹subst_E xs φ $$ (x, α) = Some A›
  shows ‹A = fun_E φ (x, α)›
  using assms
  by (metis (mono_tags, lifting) Abs_fmap_inverse Finite_Map.map_filter_def 
      comp_apply finite_dom_map_E map_E_def map_restrict_set_def mem_Collect_eq 
      option.distinct(1) option.inject subst_E_def)

lemma closed_fmran'_subst_E:
  assumes ‹A ∈ fmran' (subst_E xs φ)›
    and ‹finite xs›
    and ‹φ ↝ 𝒟›
  shows ‹free_vars A = {}›
  using assms(1)
proof
  fix xα
  assume *: ‹subst_E xs φ $$ xα = Some A›
  moreover obtain x α where ‹xα = (x, α)›
    by fastforce
  ultimately have ‹A = (SOME A. φ (x, α) = 𝒱 A α ∧ is_closed_wff_of_type A α)›
    using * assms(2) subst_E_Some unfolding fun_E_def by simp
  then show ?thesis
    using assignment_some_wff assms(3) by blast
qed

lemma dom_map_restrict_set: ‹dom (map_restrict_set xs (Some ∘ f)) = xs›
  unfolding map_restrict_set_def map_filter_def using domIff by fastforce

lemma fmdom'_θ⇩E: ‹fmdom' (θ⇩E φ A) = free_vars A›
  using dom_map_restrict_set finite_dom_map_E_free_vars
  unfolding θ⇩E_def map_E_def subst_E_def
  by (metis Abs_fmap_inverse dom_fmlookup mem_Collect_eq )

lemma close_E_closes:
  assumes φ: ‹φ ↝ 𝒟›
  shows ‹free_vars (close_E A φ) = {}›
proof -
  have ‹free_vars (close_E A φ) ⊆ (free_vars A - fmdom' (θ⇩E φ A)) ∪ ⋃(free_vars ` fmran' (θ⇩E φ A))›
    unfolding close_E_def using assms free_vars_substitute by meson
  moreover have ‹⋃(free_vars ` fmran' (θ⇩E φ A)) = {}›
    unfolding θ⇩E_def using assms closed_fmran'_subst_E free_vars_form_finiteness by auto
  moreover have ‹fmdom' (θ⇩E φ A) = free_vars A›
    using fmdom'_θ⇩E .
  ultimately show ?thesis
    by blast
qed

lemma close_E_wff:
  assumes φ: ‹φ ↝ 𝒟›
    and A: ‹A ∈ wffs⇘α⇙›
  shows ‹close_E A φ ∈ wffs⇘α⇙›
  unfolding close_E_def
  using φ A substitution_preserves_typing θ⇩E_is_substitution by simp

(* Andrews writes "Clearly close_E A φ is a cwff (of the same type)". Here it took a bit of work. *)
lemma close_E_closes_wff:
  assumes φ: ‹φ ↝ 𝒟›
    and A: ‹A ∈ wffs⇘α⇙›
  shows ‹is_closed_wff_of_type (close_E A φ) α›
  using assms close_E_closes close_E_wff by fast

lemma g:
  assumes φ: ‹φ ↝ 𝒟›
    and A: ‹A ∈ wffs⇘α⇙›
  shows ‹𝒱⇘φ⇙ A ∈ elts (𝒟 α)›
  unfolding 𝒱φ_def using A close_E_closes_wff
  by (metis φ someI_ex type_of_def well_typed wff_has_unique_type)

(* For any variable *)
lemma denotation_function_a:
  assumes φ: ‹φ ↝ 𝒟›
  shows ‹𝒱⇘φ⇙ (x⇘α⇙) = φ (x, α)›
proof -
  obtain E where E: ‹(SOME A. φ (x, α) = 𝒱 A α ∧ is_closed_wff_of_type A α) = E›
    ‹E ∈ wffs⇘α⇙› ‹φ (x,α) = 𝒱 E α›
    using assms assignment_some_wff by blast

  have ‹map_E (free_vars (x⇘α⇙)) φ (x, α) = Some E›
    unfolding map_E_def fun_E_def map_restrict_set_def Finite_Map.map_filter_def using E(1) by simp
  then have ‹close_E (x⇘α⇙) φ = E›
    unfolding close_E_def using θ⇩E_lookup by simp
  moreover have ‹𝒱⇘φ⇙ (x⇘α⇙) = 𝒱 (close_E (x⇘α⇙) φ) α›
    unfolding 𝒱φ_def type_of_def by (metis someI_ex wff_has_unique_type wffs_of_type_intros(1))
  ultimately show ?thesis
    using E(3) by simp
qed

(* For any primitive constant *)
lemma denotation_function_b: ‹𝒱⇘φ⇙ (⦃c⦄⇘α⇙) = 𝒥 (c, α)›
proof -
  have ‹map_E (free_vars (⦃c⦄⇘α⇙)) φ (c, α) = None›
    unfolding map_E_def fun_E_def map_restrict_set_def map_filter_def by simp
  then have ‹close_E (⦃c⦄⇘α⇙) φ = ⦃c⦄⇘α⇙›
    using θ⇩E_lookup unfolding close_E_def by simp
  moreover have ‹𝒱⇘φ⇙ (⦃c⦄⇘α⇙) = 𝒱 (close_E (⦃c⦄⇘α⇙) φ) α›
    unfolding 𝒱φ_def type_of_def
    by (metis wff_has_unique_type wffs_of_type_intros(2) someI_ex)
  ultimately show ?thesis
    by simp
qed

(* Application *)
lemma denotation_function_c:
  assumes φ: ‹φ ↝ 𝒟›
    and A: ‹A ∈ wffs⇘β → α⇙›
    and B: ‹B ∈ wffs⇘β⇙›
  shows ‹𝒱⇘φ⇙ (A · B) = 𝒱⇘φ⇙ A ∙ 𝒱⇘φ⇙ B›
proof -
  have ‹close_E (A · B) φ = (substitute (θ⇩E φ (A · B)) A) · (substitute (θ⇩E φ (A · B)) B)›
    unfolding close_E_def by simp
  also have ‹… = (substitute (θ⇩E φ A) A) · (substitute (θ⇩E φ B) B)›
    using substitute_cong θ⇩E_lookup A B
    by (simp add: map_filter_def map_E_def map_restrict_set_def)
  also have ‹… = (close_E A φ) · (close_E B φ)›
    unfolding close_E_def by simp
      (* Andrews does not justify this step, even though it requires an induction. *)
  finally have ‹close_E (A · B) φ = (close_E A φ) · (close_E B φ)› .

  moreover have ‹𝒱⇘φ⇙ (A · B) = 𝒱 (close_E (A · B) φ) α›
    using A B unfolding 𝒱φ_def
    by (metis someI_ex type_of_def wff_has_unique_type wffs_of_type_intros(3))

  ultimately have ‹𝒱⇘φ⇙ (A · B) = 𝒱 ((close_E A φ) · (close_E B φ)) α›
    by simp
  moreover have ‹is_closed_wff_of_type (close_E A φ) (β → α)› ‹is_closed_wff_of_type (close_E B φ) β›
    using A B φ close_E_closes_wff by blast+
  ultimately have ‹𝒱⇘φ⇙ (A · B) = 𝒱 (close_E A φ) (β → α) ∙ 𝒱 (close_E B φ) β›
    using A B distrib_𝒱_app by metis
  then show ?thesis
    unfolding 𝒱φ_def by (metis A B someI_ex type_of_def wff_has_unique_type)
qed

lemma fmdom'_θ⇩E_lam: ‹(x, α) ∉ fmdom' (θ⇩E φ (λx⇘α⇙. B))›
  by (simp add: fmdom'_θ⇩E)

lemma empty_subst_E:
  assumes ‹free_vars C = {}›
  shows ‹subst_E (free_vars C) φ = {$$}›
  using assms unfolding map_E_def subst_E_def
  by (metis emptyE finite.emptyI fmap_ext fmdom'_empty fmdom'_map_restrict_set fmdom'_notD)

lemma empty_close_E:
  assumes ‹free_vars A = {}›
  shows ‹close_E A φ = A›
  using assms unfolding close_E_def θ⇩E_def using empty_subst_E empty_substitution_neutrality by metis

lemma close_E_lam: ‹close_E (λx⇘α⇙. B) φ = λx⇘α⇙. substitute (subst_E (free_vars B - {(x, α)}) φ) B›
  using fmdom'_θ⇩E_lam unfolding close_E_def θ⇩E_def by (simp add: fmdom'_θ⇩E_lam)

lemma substitute_id_disjoint:
  assumes ‹free_vars A ∩ fmdom' φ = {}›
  shows ‹substitute φ A = A›
  using assms by (induct φ A rule: substitute.induct) auto

corollary substitute_id_closed:
  assumes ‹free_vars A = {}›
  shows ‹substitute φ A = A›
  using assms substitute_id_disjoint by simp

lemma map_E_fun_upd:
  assumes ‹(x, α) ∈ xs›
    and ‹fun_E (φ((x, α) := A)) (x, α) = E›
  shows ‹map_E xs (φ((x, α) := A)) = ((map_E (xs - {(x, α)}) φ)((x, α) ↦ E))›
  using assms unfolding map_E_def map_restrict_set_def map_filter_def fun_E_def by auto

lemma substitute_fm_upd:
  assumes B: ‹B ∈ wffs⇘β⇙›
    and E: ‹E ∈ wffs⇘α⇙› ‹free_vars E = {}› ‹fun_E (φ((x, α) := 𝒱 E α)) (x, α) = E›
    and φ: ‹φ ↝ 𝒟›
  shows ‹substitute ((subst_E (free_vars B - {(x, α)}) φ)((x, α) ↣ E)) B =
         substitute (subst_E (free_vars B) (φ((x, α) := 𝒱 E α))) B›
  using B
proof (rule substitute_cong)
  show ‹∀xa∈free_vars B. subst_E (free_vars B - {(x, α)}) φ((x, α) ↣ E) $$ xa = subst_E (free_vars B) (φ((x, α) := 𝒱 E α)) $$ xa›
  proof safe
    fix y β
    assume ‹(y, β) ∈ free_vars B›
    then have ‹((map_E (free_vars B - {(x, α)}) φ)((x, α) ↦ E)) (y, β) = (map_E (free_vars B) (φ((x, α) := 𝒱 E α))) (y, β)›
      using assms(4) map_E_fun_upd unfolding fun_E_def map_filter_def map_restrict_set_def map_E_def by simp
    moreover have ‹finite (dom (map_E (free_vars B - {(x, α)}) φ))› ‹finite (dom (map_E (free_vars B) (φ((x, α) := 𝒱 E α))))›
      by (simp_all add: finite_dom_map_E free_vars_form_finiteness)
    ultimately show ‹(subst_E (free_vars B - {(x, α)}) φ)((x, α) ↣ E) $$ (y, β) = subst_E (free_vars B) (φ((x, α) := 𝒱 E α)) $$ (y, β)›
      by (metis θ⇩E_def θ⇩E_lookup exists_fv fmupd_lookup fun_upd_apply)
  qed
qed

lemma cSubst_close_E:
  assumes B: ‹B ∈ wffs⇘β⇙›
    and E: ‹E ∈ wffs⇘α⇙› ‹free_vars E = {}› ‹fun_E (φ((x, α) := 𝒱 E α)) (x, α) = E›
    and φ: ‹φ ↝ 𝒟›
  shows ‹close_E (λx⇘α⇙. B) φ · E =⇘β⇙ close_E B (φ((x, α) := 𝒱 E α)) ∈ H›
proof -
  let ?v = ‹subst_E (free_vars B - {(x, α)}) φ›
  let ?B = ‹substitute ?v B›

  have v: ‹is_substitution ?v›
    using φ θ⇩E_is_substitution unfolding θ⇩E_def by (metis free_vars_form.simps(4))

  have ‹substitute {(x, α) ↣ E} ?B = substitute ({(x, α) ↣ E} ++⇩f fmmap (substitute {(x, α) ↣ E}) ?v) B›
  proof (rule substitution_consolidation)
    show ‹(x, α) ∉ fmdom' ?v›
      using θ⇩E_def fmdom'_θ⇩E_lam by auto
  next
    show ‹∀v'∈fmdom' ?v. is_free_for (?v $$! v') v' B›
      by (metis φ closed_fmran'_subst_E closed_is_free_for exists_fv fmlookup_dom'_iff 
          fmran'I free_vars_form_finiteness option.sel)
  qed
  moreover have ‹fmmap (substitute {(x, α) ↣ E}) ?v = ?v›
    using substitute_id_closed
    by (meson Diff_subset closed_fmran'_subst_E φ finite_subset 
        fmap.map_ident_strong free_vars_form_finiteness)
  moreover have ‹{(x, α) ↣ E} ++⇩f ?v = ?v((x, α) ↣ E)›
    by (metis θ⇩E_def fmadd_empty(2) fmadd_fmupd fmap_singleton_comm fmdom'_θ⇩E_lam fmdom'_notD
        free_vars_form.simps(4))
  ultimately have ‹substitute {(x, α) ↣ E} ?B = substitute (?v((x, α) ↣ E)) B›
    by simp

  moreover have ‹(λx⇘α⇙. ?B) · E =⇘β⇙ substitute {(x, α) ↣ E} ?B ∈ H›
    using B E φ cSubst
    by (metis θ⇩E_def θ⇩E_is_substitution exists_fv substitution_preserves_typing)
  then have ‹close_E (λx⇘α⇙. B) φ · E =⇘β⇙ substitute {(x, α) ↣ E} ?B ∈ H›
    unfolding close_E_lam .
  ultimately have ‹close_E (λx⇘α⇙. B) φ · E =⇘β⇙ substitute (?v((x, α) ↣ E)) B ∈ H›
    by simp

  moreover have ‹substitute (?v((x, α) ↣ E)) B =
      substitute (subst_E (free_vars B) (φ((x, α) := 𝒱 E α))) B›
    using assms substitute_fm_upd by blast

  ultimately show ?thesis
    unfolding close_E_def θ⇩E_def by simp
qed

(* Abstraction *)
lemma denotation_function_d:
  assumes φ: ‹φ ↝ 𝒟›
    and B: ‹B ∈ wffs⇘β⇙›
  shows ‹𝒱⇘φ⇙ (λx⇘α⇙. B) = (❙λz❙:𝒟 α ❙. 𝒱⇘φ((x, α) := z)⇙ B)›
proof -
  have *: ‹𝒱⇘φ⇙ (λx⇘α⇙. B) = 𝒱 (close_E (λx⇘α⇙. B) φ) (α → β)›
    using B unfolding 𝒱φ_def is_closed_wff_of_type_def
    by (metis someI_ex type_of_def wff_has_unique_type wffs_of_type_intros(4))

  {
    fix y
    assume ‹y ∈ elts (𝒟 α)›
    then obtain E where E: ‹is_closed_wff_of_type E α› ‹𝒱 E α = y›
      (*
        Andrews defines fun_E to give him the "first" E that represents 𝒱 E α.
        In his proof of 5501 (d), he assumes that his representative E of 𝒱 E α is also the "first".
        We need the property below to make sure close_E behaves.
      *)
      ‹fun_E (φ((x, α) := 𝒱 E α)) (x, α) = E›
      using wff_for_elts fun_E_def fun_upd_apply using φ unfolding is_assignment_def
      by (smt (verit, del_insts) fun_E_def fun_upd_apply mem_Collect_eq prod.case someI_ex)

    have B': ‹is_closed_wff_of_type (close_E (λx⇘α⇙. B) φ) (α → β)›
      using φ B close_E_closes_wff by blast
    
    have ‹close_E (λx⇘α⇙. B) φ · E =⇘β⇙ close_E B (φ((x, α) := 𝒱 E α)) ∈ H›
      using cSubst_close_E assms E by blast
    moreover have ‹is_closed_wff_of_type (close_E (λx⇘α⇙. B) φ · E) β›
      using B' E by auto
    moreover have ‹is_closed_wff_of_type (close_E B (φ((x, α) := 𝒱 E α))) β›
      using B E close_E_closes_wff ‹y ∈ elts (𝒟 α)› φ by auto
    ultimately have ‹𝒱 (close_E (λx⇘α⇙. B) φ · E) β = 𝒱 (close_E B (φ((x, α) := 𝒱 E α))) β›
      using two_gamma by blast

    moreover have ‹𝒱 (close_E (λx⇘α⇙. B) φ) (α → β) ∙ 𝒱 E α = 𝒱 (close_E (λx⇘α⇙. B) φ · E) β›
      using B' distrib_𝒱_app E by metis

    ultimately have ‹𝒱⇘φ⇙ (λx⇘α⇙. B) ∙ y = 𝒱⇘φ((x, α) := y)⇙ B›
      using B E * unfolding 𝒱φ_def is_closed_wff_of_type_def
      by (metis someI_ex type_of_def wff_has_unique_type)
  }

  then show ?thesis
    using * vlambda_extensionality by fastforce
qed

lemma denotation_function: ‹is_wff_denotation_function 𝒱φ›
  unfolding is_wff_denotation_function_def
  using g denotation_function_a denotation_function_b denotation_function_c denotation_function_d
  by auto

sublocale M: general_model 𝒟 𝒥 𝒱φ
  using denotation_function
  by unfold_locales auto

lemma sat_closed_formulas:
  assumes A: ‹A ∈ wffs⇘o⇙› ‹free_vars A = {}›
    and H: ‹A ∈ H›
  shows ‹𝒱⇘φ⇙ A = ❙T›
proof -
  have ‹𝒱⇘φ⇙ A = 𝒱 (close_E A φ) o›
    using A by (metis 𝒱φ_def someI_ex type_of_def wff_has_unique_type)
  also have ‹𝒱 (close_E A φ) o = 𝒱 A o›
    using H A empty_close_E by simp
  also have ‹…  = ❙T ⟷ A ∈ H›
    by (simp add: bool_to_V_distinct)
  finally show ?thesis
    using H by meson
qed

lemma canon_model_for: ‹is_model_for (𝒟,𝒥,𝒱φ) {A ∈ H. A ∈ wffs⇘o⇙ ∧ free_vars A = {}}›
  using sat_closed_formulas by blast+

lemmas is_general_model = M.general_model_axioms

lemma 𝒱φ_consistent:
  assumes A: ‹A ∈ wffs⇘o⇙› ‹free_vars A = {}›
  shows ‹¬ (𝒱⇘φ⇙ A = ❙T ∧ 𝒱⇘φ⇙ (∼⇧𝒬 A) = ❙T)›
proof -
  have ‹𝒱⇘φ⇙ A = 𝒱 A o›
    using A empty_close_E by (metis 𝒱φ_def someI_ex type_of_def wff_has_unique_type)
  moreover have ‹𝒱⇘φ⇙ (∼⇧𝒬 A) = 𝒱 (∼⇧𝒬 A) o›
    using A empty_close_E
    by (metis 𝒱φ_def type_of_def neg_wff someI_ex neg_fv diff_types_implies_diff_wffs)
  ultimately show ?thesis
    by (metis 𝒱.simps(1) A(1) bool_to_V_distinct bottom_def consistent top_def)
qed

lemma model_consistent:
  assumes A: ‹A ∈ wffs⇘o⇙› ‹free_vars A = {}›
  shows ‹¬ ((𝒟,𝒥,𝒱φ) ⊨ A ∧ (𝒟,𝒥,𝒱φ) ⊨ ∼⇧𝒬 A)›
  using 𝒱φ_consistent[OF assms]
  by (metis (mono_tags, lifting) 𝒥.simps well_typed free_vars_form.simps(2)
      is_assignment_def is_closed_wff_of_type_def old.prod.case wffs_of_type_intros(2))

lemma elts_in_wffs: ‹elts (𝒟 α) ⊆ (λA. 𝒱 A α) ` wffs⇘α⇙›
proof (induct α)
  case TBool
  then show ?case
    using cTop cFalse by auto
qed auto

lemma frugal_wffs: ‹|elts (𝒟 α)| ≤o |wffs⇘α⇙|›
  using elts_in_wffs by (meson surj_imp_ordLeq)

theorem is_frugal: ‹is_frugal (𝒟,𝒥,𝒱φ)›
  unfolding is_frugal_def
  using frugal_wffs card_of_UNIV ordLeq_transitive by blast

end

section ‹Model Existence›

theorem model_existence:
  fixes S :: ‹form set›
  assumes cprop: ‹P.prop⇩E Kinds C›
    and S: ‹S ∈ C› ‹P.enough_new S›
  shows ‹∃M. is_general_model M ∧ is_frugal M ∧
    (∀A ∈ S. is_sentence A ⟶ M ⊨ A) ∧
    (∀A. is_sentence A ⟶ ¬ (M ⊨ A ∧ M ⊨ ∼⇧𝒬 A))›
proof -
  have *: ‹MyHintikka (mk_mcs C S)›
  proof
    show ‹P.prop⇩H Kinds (mk_mcs C S)›
      using mk_mcs_Hintikka[OF cprop S] Hintikka.hintikka by blast
  qed
  then show ?thesis
    using MyHintikka.canon_model_for[OF *] MyHintikka.is_general_model[OF *] 
      MyHintikka.model_consistent[OF *] MyHintikka.is_frugal[OF *]
      Extend_subset by blast
qed

end