Theory Example_SOL

(*
  File:      Example_SOL.thy
  Author:    Anders Schlichtkrull
  Author:    Asta Halkjær Boserup

*)

chapter ‹Example: Second-Order Logic›

text ‹Generalizes \<^cite>‹"FOL-Axiomatic-AFP"› and \<^cite>‹"From21-TYPES"›
      from first-order logic to second-order logic›

theory Example_SOL imports
  Abstract_Consistency_Property
begin

section ‹Syntax›

datatype (params_sym:'f) sym
  = VarS nat (‹❙#⇩2›)
  | SymS 'f (‹❙○⇩2›)

datatype (params_tm: 'f) tm
  = Var nat (‹❙#›)
  | Fun ‹'f sym› ‹'f tm list› (‹❙○›)
  | Cst 'f (‹❙⋆›) 

datatype (params_fm: 'f) fm
  = Falsity (‹❙⊥›)
  | is_Pre: Pre ‹'f sym› ‹'f tm list› (‹❙⋅›)
  | Imp ‹'f fm› ‹'f fm› (infixr ‹❙⟶› 55)
  | Uni ‹'f fm› (‹❙∀›)
  | UniP ‹'f fm› (‹❙∀⇩P›)
  | UniF ‹'f fm› (‹❙∀⇩F›)

abbreviation Neg (‹❙¬ _› [70] 70) where ‹❙¬ p ≡ p ❙⟶ ❙⊥›

abbreviation And (infix ‹❙∧› 50) where ‹p ❙∧ q ≡ ❙¬ (p ❙⟶ ❙¬ q)›

abbreviation Iff (infix ‹❙⟷› 50) where ‹p ❙⟷ q ≡ (p ❙⟶ q) ❙∧ (q ❙⟶ p)›

abbreviation Eql (‹_ ❙= _›) where ‹t1 ❙= t2 ≡ (❙∀⇩P ((❙⋅(❙#⇩2 0) [t1]) ❙⟷ (❙⋅(❙#⇩2 0) [t2])))›

abbreviation ExiF (‹❙∃⇩F›) where ‹❙∃⇩F p ≡ ❙¬(❙∀⇩F(❙¬p))›

abbreviation ExiP (‹❙∃⇩P›) where ‹❙∃⇩P p ≡ ❙¬(❙∀⇩P(❙¬p))›

term ‹❙∀(❙⊥ ❙⟶ (❙⋅(❙○⇩2 ''P'') [❙○(❙○⇩2 ''f'') [❙#0]]))›

section ‹Semantics›

definition shift (‹_⟨_:_⟩›) where
  ‹E⟨n:x⟩ m ≡ if m < n then E m else if m = n then x else E (m-1)›

primrec semantics_fn (‹⦉_, _⦊⇩2›) where
  ‹⦉E⇩F, F⦊⇩2 (❙#⇩2 n) = E⇩F n›
| ‹⦉E⇩F, F⦊⇩2 (❙○⇩2 f) = F f›

primrec semantics_tm (‹⦉_,_, _, _⦊›) where
  ‹⦉E, E⇩F, C, F⦊ (❙#n) = E n›
| ‹⦉E, E⇩F, C, F⦊ (❙○f ts) = (⦉E⇩F, F⦊⇩2 f) (map ⦉E, E⇩F, C, F⦊ ts)›
| ‹⦉E, E⇩F, C, F⦊ (❙⋆ c) = C c›

fun semantics_fm (infix ‹⊨› 50) where
  ‹((_, _, _, _, _, _, _, _) ⊨ ❙⊥) = False›
| ‹((E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ ❙⋅P ts) = ⦉E⇩P, G⦊⇩2 P (map ⦉E, E⇩F, C, F⦊ ts)›
| ‹((E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ p ❙⟶ q) = ((E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ p ⟶ (E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ q)›
| ‹((E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ ❙∀p) = (∀x. (E⟨0:x⟩, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ p)›
| ‹((E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ ❙∀⇩Pp) = (∀x ∈ PS. (E, E⇩F, E⇩P⟨0:x⟩, C, F, G, PS, FS) ⊨ p)›
| ‹((E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ ❙∀⇩Fp) = (∀x ∈ FS. (E, E⇩F⟨0:x⟩, E⇩P, C, F, G, PS, FS) ⊨ p)›

proposition ‹(E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ (❙∀(❙⋅P [❙# 0]) ❙⟶ ❙⋅P [❙⋆a])›
  by (simp add: shift_def)

section ‹Operations›

subsection ‹Shift›

context fixes n m :: nat begin

lemma shift_eq [simp]: ‹n = m ⟹ E⟨n:x⟩ m = x›
  by (simp add: shift_def)

lemma shift_gt [simp]: ‹m < n ⟹ E⟨n:x⟩ m = E m›
  by (simp add: shift_def)

lemma shift_lt [simp]: ‹n < m ⟹ E⟨n:x⟩ m = E (m-1)›
  by (simp add: shift_def)

lemma shift_commute [simp]: ‹(E⟨n:y⟩⟨0:x⟩) = (E⟨0:x⟩⟨n+1:y⟩)›
proof
  fix m
  show ‹(E⟨n:y⟩⟨0:x⟩) m = (E⟨0:x⟩⟨n+1:y⟩) m›
    unfolding shift_def by (cases m) simp_all
qed

end

subsection ‹Parameters›

abbreviation ‹params S ≡ ⋃p ∈ S. params_fm p›

lemma upd_params_sym [simp]: ‹f ∉ params_sym fn ⟹ ⦉E⇩F, F(f := x)⦊⇩2 fn = ⦉E⇩F, F⦊⇩2 fn›
  by (induct fn) (auto cong: map_cong)

lemma upd_params_tm [simp]: ‹f ∉ params_tm t ⟹ ⦉E, E⇩F, C, F(f := x)⦊ t = ⦉E, E⇩F, C, F⦊ t›
  by (induct t) (auto cong: map_cong)

lemma upd_params_tm_c [simp]: ‹c ∉ params_tm t ⟹ ⦉E, E⇩F, C(c := x), F⦊ t = ⦉E, E⇩F, C, F⦊ t›
  by (induct t) (auto cong: map_cong)

lemma upd_params_fm [simp]: ‹f ∉ params_fm p ⟹ (E, E⇩F, E⇩P, C, F(f := x), G, PS, FS) ⊨ p ⟷ (E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ p›
  by (induct p arbitrary: E E⇩P E⇩F) (auto cong: map_cong)

lemma upd_params_fm_c [simp]: ‹c ∉ params_fm p ⟹ (E, E⇩F, E⇩P, C(c := x), F, G, PS, FS) ⊨ p ⟷ (E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ p›
  by (induct p arbitrary: E E⇩P E⇩F) (auto cong: map_cong)

lemma upd_params_fm_G [simp]: ‹P ∉ params_fm p ⟹ (E, E⇩F, E⇩P, C, F, G(P := x), PS, FS) ⊨ p ⟷ (E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ p›
  by (induct p arbitrary: E E⇩F E⇩P) (auto cong: map_cong)

lemma finite_params_sym [simp]: ‹finite (params_sym fn)›
  by (induct fn) simp_all

lemma finite_params_tm [simp]: ‹finite (params_tm t)›
  by (induct t) simp_all

lemma finite_params_fm [simp]: ‹finite (params_fm p)›
  by (induct p) simp_all


subsection ‹Instantiation›

primrec lift_tm (‹❙↑›) where
  ‹❙↑(❙#n) = ❙#(n+1)›
| ‹❙↑(❙○f ts) = ❙○f (map ❙↑ ts)›
| ‹❙↑(❙⋆c) = ❙⋆ c›

primrec lift_sym (‹❙↑⇩2›) where
  ‹❙↑⇩2(❙#⇩2 n) = ❙#⇩2 (n+1)›
| ‹❙↑⇩2(❙○⇩2 p) = ❙○⇩2 p›

primrec lift_fn (‹❙↑⇩F›) where
  ‹❙↑⇩F(❙#n) = ❙#n›
| ‹❙↑⇩F(❙○f ts) = ❙○(❙↑⇩2 f) (map ❙↑⇩F ts)›
| ‹❙↑⇩F(❙⋆ c) = ❙⋆ c›

primrec inst_tm (‹⟪_'/_⟫›) where
  ‹⟪s/m⟫(❙#n) = (if n < m then ❙#n else if n = m then s else ❙#(n-1))›
| ‹⟪s/m⟫(❙○f ts) = ❙○f (map ⟪s/m⟫ ts)›
| ‹⟪s/m⟫(❙⋆c) = ❙⋆c›

primrec inst_sym (‹⟪_'/_⟫⇩2›) where
  ‹⟪s/m⟫⇩2 (❙#⇩2 n) = (if n < m then ❙#⇩2 n else if n = m then s else ❙#⇩2 (n-1))›
| ‹⟪s/m⟫⇩2 (❙○⇩2 p) = ❙○⇩2 p›

primrec inst_fn (‹⟪_'/_⟫⇩F›) where
  ‹⟪s/m⟫⇩F(❙#n) = (❙#n)›
| ‹⟪s/m⟫⇩F(❙○f ts) = ❙○(⟪s/m⟫⇩2 f) (map ⟪s/m⟫⇩F ts)›
| ‹⟪s/m⟫⇩F(❙⋆c) = (❙⋆c)›

primrec inst_fm (‹⟨_'/_⟩›) where
  ‹⟨_/_⟩❙⊥ = ❙⊥›
| ‹⟨s/m⟩(❙⋅P ts) = ❙⋅P (map ⟪s/m⟫ ts)›
| ‹⟨s/m⟩(p ❙⟶ q) = ⟨s/m⟩p ❙⟶ ⟨s/m⟩q›
| ‹⟨s/m⟩(❙∀p) = ❙∀(⟨❙↑s/m+1⟩p)›
| ‹⟨s/m⟩(❙∀⇩Pp) = ❙∀⇩P(⟨s/m⟩p)›
| ‹⟨s/m⟩(❙∀⇩Fp) = ❙∀⇩F(⟨❙↑⇩F s/m⟩p)›

primrec inst_fm_P (‹⟨_'/_⟩⇩P›) where
  ‹⟨_/_⟩⇩P❙⊥ = ❙⊥›
| ‹⟨s/m⟩⇩P(❙⋅P ts) = ❙⋅(⟪s/m⟫⇩2 P) ts›
| ‹⟨s/m⟩⇩P(p ❙⟶ q) = ⟨s/m⟩⇩Pp ❙⟶ ⟨s/m⟩⇩Pq›
| ‹⟨s/m⟩⇩P(❙∀p) = ❙∀(⟨s/m⟩⇩Pp)›
| ‹⟨s/m⟩⇩P(❙∀⇩Pp) = ❙∀⇩P(⟨❙↑⇩2 s/m+1⟩⇩Pp)›
| ‹⟨s/m⟩⇩P(❙∀⇩Fp) = ❙∀⇩F(⟨s/m⟩⇩Pp)›

primrec inst_fm_F (‹⟨_'/_⟩⇩F›) where
  ‹⟨_/_⟩⇩F❙⊥ = ❙⊥›
| ‹⟨s/m⟩⇩F(❙⋅P ts) = ❙⋅P (map ⟪s/m⟫⇩F ts)›
| ‹⟨s/m⟩⇩F(p ❙⟶ q) = ⟨s/m⟩⇩Fp ❙⟶ ⟨s/m⟩⇩Fq›
| ‹⟨s/m⟩⇩F(❙∀p) = ❙∀(⟨s/m⟩⇩Fp)›
| ‹⟨s/m⟩⇩F(❙∀⇩Pp) = ❙∀⇩P(⟨s/m⟩⇩Fp)›
| ‹⟨s/m⟩⇩F(❙∀⇩Fp) = ❙∀⇩F(⟨❙↑⇩2 s/m+1⟩⇩Fp)›

lemma lift_lemma [simp]: ‹⦉E⟨0:x⟩, E⇩F, C, F⦊ (❙↑t) = ⦉E, E⇩F, C, F⦊ t›
  by (induct t) (auto cong: map_cong)

lemma lift_lemma_P [simp]: ‹⦉E⇩P⟨0:x⟩, G⦊⇩2 (❙↑⇩2 P) = ⦉E⇩P, G⦊⇩2 P›
  by (induct P) (auto cong: map_cong)

lemma lift_lemma_F [simp]: ‹⦉E, E⇩F⟨0:x⟩, C, F⦊ (❙↑⇩F tm) = ⦉E, E⇩F, C, F⦊ tm›
  by (induct tm) (auto cong: map_cong)

lemma inst_tm_semantics [simp]: ‹⦉E, E⇩F, C, F⦊ (⟪s/m⟫t) = ⦉E⟨m:⦉E, E⇩F, C, F⦊ s⟩, E⇩F, C, F⦊ t›
  by (induct t) (auto cong: map_cong)

lemma inst_sym_semantics [simp]: ‹⦉E⇩F, G⦊⇩2 (⟪s/m⟫⇩2 fn) = ⦉E⇩F⟨m:⦉E⇩F, G⦊⇩2 s⟩, G⦊⇩2 fn›
  by (induct fn) (auto cong: map_cong)

lemma inst_tm_semantics_F [simp]: ‹⦉E, E⇩F, C, F⦊ (⟪s/m⟫⇩F t) = ⦉E, E⇩F⟨m:⦉E⇩F, F⦊⇩2 s⟩, C, F⦊ t›
  by (induct t) (auto cong: map_cong)

lemma inst_fm_semantics_F [simp]:
   ‹(E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ (⟨t/m⟩⇩F p) ⟷ (E, E⇩F⟨m:⦉E⇩F, F⦊⇩2 t⟩, E⇩P, C, F, G, PS, FS) ⊨ p›
  by (induct p arbitrary: E E⇩P E⇩F m t) (auto cong: map_cong)

lemma inst_fm_semantics [simp]:
   ‹(E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ (⟨t/m⟩p) ⟷ (E⟨m:⦉E, E⇩F, C, F⦊ t⟩, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ p›
  by (induct p arbitrary: E E⇩P E⇩F m t) (auto cong: map_cong)

lemma inst_fm_semantics_P [simp]: ‹(E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ (⟨P/m⟩⇩Pp) ⟷ (E, E⇩F, E⇩P⟨m:⦉E⇩P, G⦊⇩2 P⟩, C, F, G, PS, FS) ⊨ p›
  by (induct p arbitrary: E E⇩F E⇩P m P) (auto cong: map_cong)

subsection ‹Size›

text ‹The built-in ‹size› is not invariant under substitution.›

primrec size_fm where
  ‹size_fm ❙⊥ = 1›
| ‹size_fm (❙⋅_ _) = 1›
| ‹size_fm (p ❙⟶ q) = 1 + size_fm p + size_fm q›
| ‹size_fm (❙∀p) = 1 + size_fm p›
| ‹size_fm (❙∀⇩Pp) = 1 + size_fm p›
| ‹size_fm (❙∀⇩Fp) = 1 + size_fm p›

lemma size_inst_fm [simp]: ‹size_fm (⟨t/m⟩p) = size_fm p›
  by (induct p arbitrary: m t) simp_all

lemma size_inst_fm_P [simp]: ‹size_fm (⟨t/m⟩⇩Pp) = size_fm p›
  by (induct p arbitrary: m t) simp_all

lemma size_inst_fm_F [simp]: ‹size_fm (⟨t/m⟩⇩Fp) = size_fm p›
  by (induct p arbitrary: m t) simp_all


section ‹Model Existence›

inductive confl_class :: ‹'f fm list ⇒ 'f fm list ⇒ bool› (infix ‹↝⇩✗› 50) where
  CFls: ‹[ ❙⊥ ] ↝⇩✗ [ ❙⊥ ]›
| CNeg: ‹[ ❙¬ (❙⋅P ts) ] ↝⇩✗ [ ❙⋅P ts ]›

inductive alpha_class :: ‹'f fm list ⇒ 'f fm list ⇒ bool› (infix ‹↝⇩α› 50) where
  CImpN: ‹[ ❙¬ (p ❙⟶ q) ] ↝⇩α [ p, ❙¬ q ]›

inductive beta_class :: ‹'f fm list ⇒ 'f fm list ⇒ bool› (infix ‹↝⇩β› 50) where
  CImpP: ‹[ p ❙⟶ q ] ↝⇩β [ ❙¬ p, q ]›

inductive gamma_class :: ‹'f fm list ⇒  ('f tm ⇒ 'f fm list) ⇒ bool› (infix ‹↝⇩γ› 50) where
  CAllP: ‹[ ❙∀p ] ↝⇩γ (λt. [ ⟨t/0⟩p ])›

inductive gamma_class_P :: ‹'f fm list ⇒ ('f sym ⇒ 'f fm list) ⇒ bool› (infix ‹↝⇩γ⇩P› 50) where
  CAllPP: ‹[ ❙∀⇩P p ] ↝⇩γ⇩P (λs. [ ⟨s/0⟩⇩P p ])›

inductive gamma_class_F :: ‹'f fm list ⇒ ('f sym ⇒ 'f fm list) ⇒ bool› (infix ‹↝⇩γ⇩F› 50) where
  CAllFP: ‹[ ❙∀⇩F p ] ↝⇩γ⇩F (λs. [ ⟨s/0⟩⇩F p ])›

fun δ :: ‹'f fm ⇒ 'f ⇒ 'f fm list› where
  CAllN:   ‹δ (❙¬ ❙∀p) x = [ ❙¬ ⟨❙⋆x/0⟩ p ]› 
| CAll2PN: ‹δ (❙¬ ❙∀⇩P p) x = [ ❙¬ ⟨❙○⇩2 x/0⟩⇩P p ]›
| CAll2FN: ‹δ ( ❙¬ ❙∀⇩F p ) x = [ ❙¬ ⟨❙○⇩2 x/0⟩⇩F p ]›
| NOMATCH: ‹δ _ _ = []›

interpretation P: Params map_fm params_fm ‹λ_. True›
  by unfold_locales (auto simp: tm.map_id0 fm.map_id0 cong: tm.map_cong0 fm.map_cong0)

interpretation C: Confl map_fm params_fm ‹λ_. True› confl_class
  by unfold_locales (auto elim!: confl_class.cases intro: confl_class.intros)

interpretation A: Alpha map_fm params_fm ‹λ_. True› alpha_class
  by unfold_locales (auto simp: fm.map_id0 cong: fm.map_cong0 elim!: alpha_class.cases intro: alpha_class.intros)

interpretation B: Beta map_fm params_fm ‹λ_. True› beta_class
  by unfold_locales (auto simp: fm.map_id0 cong: fm.map_cong0 elim!: beta_class.cases intro: beta_class.intros)

lemma map_tm_inst_tm [simp]:
  "map_tm f (⟪t/n⟫ x) = ⟪map_tm f t/n⟫ (map_tm f x)"
  by (induct x) simp_all

lemma map_tm_lift_tm [simp]: "map_tm f (❙↑ t) = ❙↑ (map_tm f t)"
  by (induct t) simp_all

lemma map_sym_lift_fn [simp]: ‹map_sym f (❙↑⇩2 t) = ❙↑⇩2 (map_sym f t)›
  by (induct t) auto

lemma map_tm_lift_fn [simp]: "map_tm f (❙↑⇩F t) = ❙↑⇩F (map_tm f t)"
  by (induct t) simp_all

lemma map_fm_inst_single [simp]: ‹map_fm f (⟨t/m⟩p) = ⟨map_tm f t/m⟩(map_fm f p)›
  by (induct p arbitrary: t m) simp_all

lemma map_sym_inst_sym [simp]: ‹map_sym f (⟪t/m⟫⇩2 p) = ⟪map_sym f t/m⟫⇩2 (map_sym f p)›
  by (induct p arbitrary: t m) simp_all

lemma psub_inst_single' [simp]: ‹map_fm f (⟨t/m⟩⇩P p) = ⟨map_sym f t/m⟩⇩P(map_fm f p)›
  by (induct p arbitrary: t m) simp_all

lemma map_tm_inst_fn [simp]: ‹map_tm f (⟪t/m⟫⇩F s) = ⟪map_sym f t/m⟫⇩F (map_tm f s)›
  by (induct s) auto

lemma psub_inst_single'' [simp]: ‹map_fm f (⟨t/m⟩⇩F p) = ⟨map_sym f t/m⟩⇩F(map_fm f p)›
  by (induct p arbitrary: t m) simp_all

interpretation G: Gamma_UNIV map_tm map_fm params_fm ‹λ_. True› gamma_class
  by unfold_locales (fastforce elim: gamma_class.cases intro: gamma_class.intros)+

interpretation G⇩P: Gamma_UNIV map_sym map_fm params_fm ‹λ_. True› gamma_class_P
  by unfold_locales (fastforce elim: gamma_class_P.cases intro: gamma_class_P.intros)+

interpretation G⇩F: Gamma_UNIV map_sym map_fm params_fm ‹λ_. True› gamma_class_F
  by unfold_locales (fastforce elim: gamma_class_F.cases intro: gamma_class_F.intros)+

interpretation D: Delta map_fm params_fm ‹λ_. True› δ
proof
  show ‹⋀f. δ (map_fm f p) (f x) = map (map_fm f) (δ p x)› for p :: ‹'x fm› and x
    by (induct p x rule: δ.induct) simp_all
qed

abbreviation Kinds :: ‹('x, 'x fm) kind list› where
  ‹Kinds ≡ [C.kind, A.kind, B.kind, G.kind, G⇩P.kind, G⇩F.kind, D.kind]›

lemma prop⇩E_Kinds:
  assumes ‹P.sat⇩E C.kind C› ‹P.sat⇩E A.kind C› ‹P.sat⇩E B.kind C› ‹P.sat⇩E G.kind C› ‹P.sat⇩E G⇩P.kind C›
    ‹P.sat⇩E G⇩F.kind C› ‹P.sat⇩E D.kind C›
  shows ‹P.prop⇩E Kinds C›
  unfolding P.prop⇩E_def using assms by simp

interpretation Consistency_Kinds map_fm params_fm ‹λ_. True› Kinds
  using P.Params_axioms C.Consistency_Kind_axioms A.Consistency_Kind_axioms B.Consistency_Kind_axioms
    G.Consistency_Kind_axioms G⇩P.Consistency_Kind_axioms G⇩F.Consistency_Kind_axioms
    D.Consistency_Kind_axioms
  by (auto intro: Consistency_Kinds.intro simp: Consistency_Kinds_axioms_def)

interpretation Maximal_Consistency map_fm params_fm ‹λ_. True› Kinds
proof
  show ‹infinite (UNIV :: 'x fm set)›
    using infinite_UNIV_size[of ‹λp. p ❙⟶ p›] by simp
qed simp

abbreviation henv⇩P where "henv⇩P H == λn ts. ❙⋅(❙#⇩2 n) ts ∈ H"

abbreviation hpred where "hpred H == λP ts. ❙⋅(❙○⇩2 P) ts ∈ H"

abbreviation hdom⇩P where "hdom⇩P H == range (henv⇩P H) ∪ range (hpred H)"

abbreviation henv⇩F where "henv⇩F == λf. ❙○ (❙#⇩2 f)"

abbreviation hfun where "hfun ==  λf. ❙○ (❙○⇩2 f)"

definition hdom⇩F where "hdom⇩F == range henv⇩F ∪ range hfun"

abbreviation (input) hmodel (‹⟦_⟧›) where ‹⟦H⟧ ≡ (❙#, henv⇩F, henv⇩P H, ❙⋆, hfun, hpred H, hdom⇩P H, hdom⇩F)›

lemma semantics_tm_id [simp]: ‹⦉❙#, henv⇩F , ❙⋆ , λf. ❙○ (❙○⇩2 f) ⦊ t = t›
proof (induct t)
  case (Var x)
  then show ?case 
    by (auto cong: map_cong)
next
  case (Fun x1a x2)
  then show ?case
    by (cases x1a) (auto cong: map_cong)
next
  case (Cst c)
  then show ?case
    by auto
qed

lemma semantics_tm_id_map [simp]: ‹map ⦉❙#, λf. ❙○ (❙#⇩2 f) , ❙⋆, λf. ❙○ (❙○⇩2 f) ⦊ ts = ts›
  by (auto cong: map_cong)

lemma semantics_fn_h [simp]: ‹⦉henv⇩P S, hpred S⦊⇩2 P ts ⟷ ❙⋅P ts ∈ S›
  by (cases P) simp_all

lemma canonical_henv⇩P:
  ‹∀t. (❙#, henv⇩F, (henv⇩P S)⟨0:⦉henv⇩P S, hpred S⦊⇩2 t⟩, ❙⋆, hfun, hpred S, hdom⇩P S, hdom⇩F) ⊨ p ⟹
       (❙#, henv⇩F, (henv⇩P S)⟨0:henv⇩P S n⟩, ❙⋆, hfun, hpred S, hdom⇩P S, hdom⇩F) ⊨ p›
  by (metis semantics_fn.simps(1))

lemma canonical_hpred:
  ‹∀t. (❙#, henv⇩F, (henv⇩P S)⟨0:⦉henv⇩P S, hpred S⦊⇩2 t⟩, ❙⋆, hfun, hpred S, hdom⇩P S, hdom⇩F) ⊨ p ⟹
       (❙#, henv⇩F, (henv⇩P S)⟨0:hpred S P⟩, ❙⋆, hfun, hpred S, hdom⇩P S, hdom⇩F) ⊨ p›
  by (metis semantics_fn.simps(2))

lemma canonical_henv⇩F:
  ‹∀t. (❙#, henv⇩F⟨0:⦉henv⇩F, hfun⦊⇩2 t⟩, henv⇩P S, ❙⋆, hfun, hpred S, hdom⇩P S, hdom⇩F) ⊨ p ⟹
       (❙#, henv⇩F⟨0:henv⇩F f⟩, henv⇩P S, ❙⋆, hfun, hpred S, hdom⇩P S, hdom⇩F) ⊨ p›
  by (metis semantics_fn.simps(1))

lemma canonical_hfun:
  ‹∀t. (❙#, henv⇩F⟨0:⦉henv⇩F, hfun⦊⇩2 t⟩, henv⇩P S, ❙⋆, hfun, hpred S, hdom⇩P S, hdom⇩F) ⊨ p ⟹
       (❙#, henv⇩F⟨0:hfun f⟩, henv⇩P S, ❙⋆, hfun, hpred S, hdom⇩P S, hdom⇩F) ⊨ p›
  by (metis semantics_fn.simps(2))

locale MyHintikka = Hintikka map_fm params_fm ‹λ_. True› Kinds S for S :: ‹'x fm set›
begin

lemmas
  confl = sat⇩H[of C.kind] and
  alpha = sat⇩H[of A.kind] and
  beta = sat⇩H[of B.kind] and
  gammaFO = sat⇩H[of G.kind] and
  gamma2P = sat⇩H[of G⇩P.kind] and
  gamma2F = sat⇩H[of G⇩F.kind] and
  delta = sat⇩H[of D.kind]

theorem model: ‹(p ∈ S ⟶ ⟦S⟧ ⊨ p) ∧ (❙¬ p ∈ S ⟶ ¬ ⟦S⟧ ⊨ p)›
proof (induct p rule: wf_induct[where r=‹measure size_fm›])
  case 1
  then show ?case
    by simp
next
  case (2 x)
  then show ?case
  proof (cases x)
    case Falsity
    then show ?thesis
      using confl by (force intro: CFls)
  next
    case (Pre P ts)
    then show ?thesis
    proof (safe del: notI)
      assume ‹x = ❙⋅P ts› ‹❙⋅P ts ∈ S›
      then show ‹⟦S⟧ ⊨ (❙⋅P ts)›
        by simp
    next
      assume ‹x = ❙⋅P ts› ‹❙¬ ❙⋅P ts ∈ S›
      then have ‹❙⋅P ts ∉ S›
        using confl by (force intro: CNeg)
      then show ‹¬ ⟦S⟧ ⊨ (❙⋅P ts)›
        by simp
    qed
  next
    case (Imp p q)
    then show ?thesis
    proof (safe del: notI)
      assume ‹x = p ❙⟶ q› ‹p ❙⟶ q ∈ S›
      then have ‹❙¬ p ∈ S ∨ q ∈ S›
        using beta by (force intro: CImpP)
      then show ‹⟦S⟧ ⊨ (p ❙⟶ q)›
        using 2 Imp by auto
    next
      assume ‹x = p ❙⟶ q› ‹❙¬ (p ❙⟶ q) ∈ S›
      then have ‹p ∈ S ∧ ❙¬ q ∈ S›
        using alpha by (force intro: CImpN)
      then show ‹¬ ⟦S⟧ ⊨ (p ❙⟶ q)›
        using 2 Imp by auto
    qed
  next
    case (Uni p)
    then show ?thesis
    proof (safe del: notI)
      assume ‹x = ❙∀p› ‹❙∀p ∈ S›
      then have ‹∀t. ⟨t/0⟩p ∈ S›
        using gammaFO by (fastforce intro: CAllP)
      moreover have ‹∀t. (⟨t/0⟩p, ❙∀p) ∈ measure size_fm›
        by simp
      ultimately have ‹∀t. ⟦S⟧ ⊨ (⟨t/0⟩p)›
        using 2 ‹x = ❙∀p› by blast
      then show ‹⟦S⟧ ⊨ (❙∀p)›
        by simp
    next
      assume ‹x = ❙∀p› ‹❙¬ ❙∀p ∈ S›
      then obtain a where ‹❙¬ ⟨❙⋆a/0⟩p ∈ S›
        using delta by auto
      moreover have ‹(⟨❙⋆a/0⟩p, ❙∀p) ∈ measure size_fm›
        by simp
      ultimately have ‹¬ ⟦S⟧ ⊨ (⟨❙⋆a/0⟩p)›
        using 2 ‹x = ❙∀p› by blast
      then show ‹¬ ⟦S⟧ ⊨ (❙∀p)›
        by auto
    qed
  next
    case (UniP p)
    then show ?thesis
    proof (safe del: notI)
      assume ‹x = ❙∀⇩P p› ‹❙∀⇩P p ∈ S›
      then have ‹∀t. ⟨t/0⟩⇩P p ∈ S›
        using gamma2P by (fastforce intro: CAllPP)
      moreover have *: ‹∀t. (⟨t/0⟩⇩P p, ❙∀⇩P p) ∈ measure size_fm›
        by simp
      ultimately have ‹∀t. ⟦S⟧ ⊨ (⟨t/0⟩⇩P p)›
        using 2 ‹x = ❙∀⇩P p› by blast
      then show ‹⟦S⟧ ⊨ ❙∀⇩P p›
        using canonical_henv⇩P canonical_hpred by auto
    next
      assume ‹x = ❙∀⇩P p› ‹❙¬ ❙∀⇩P p ∈ S›
      then obtain a where ‹❙¬ ⟨❙○⇩2 a/0⟩⇩P p ∈ S›
        using delta by auto
      moreover have ‹(⟨❙○⇩2 a/0⟩⇩P p, ❙∀⇩P p) ∈ measure size_fm›
        by simp
      ultimately have ‹¬ ⟦S⟧ ⊨ (⟨❙○⇩2a/0⟩⇩P p)›
        using 2 ‹x = ❙∀⇩P p› by blast
      then show ‹¬ ⟦S⟧ ⊨ (❙∀⇩P p)›
        by auto
    qed
  next
    case (UniF p)
    then show ?thesis
    proof (safe del: notI)
      assume ‹x = ❙∀⇩F p› ‹❙∀⇩F p ∈ S›
      then have ‹∀t. ⟨t/0⟩⇩F p ∈ S›
        using gamma2F by (fastforce intro: CAllFP)
      moreover have ‹∀t. (⟨t/0⟩⇩F p, ❙∀⇩F p) ∈ measure size_fm›
        by simp
      ultimately have ‹∀t. ⟦S⟧ ⊨ (⟨t/0⟩⇩F p)›
        using 2 ‹x = ❙∀⇩F p› by blast
      then show ‹⟦S⟧ ⊨ (❙∀⇩F p)›
        using canonical_henv⇩F canonical_hfun unfolding hdom⇩F_def by auto
    next
      assume ‹x = ❙∀⇩F p› ‹❙¬ ❙∀⇩F p ∈ S›
      then obtain a where ‹❙¬ ⟨❙○⇩2 a/0⟩⇩F p ∈ S›
        using delta by auto
      moreover have ‹(⟨❙○⇩2 a/0⟩⇩F p, ❙∀⇩F p) ∈ measure size_fm›
        by simp
      ultimately have ‹¬ ⟦S⟧ ⊨ (⟨❙○⇩2a/0⟩⇩F p)›
        using 2 ‹x = ❙∀⇩F p› by blast
      then show ‹¬ ⟦S⟧ ⊨ (❙∀⇩F p)›
        by (auto simp: hdom⇩F_def)
    qed
  qed
qed

end

theorem model_existence:
  fixes S :: ‹'x fm set›
  assumes ‹P.prop⇩E Kinds C›
    and ‹S ∈ C›
    and ‹P.enough_new S›
    and ‹p ∈ S›
  shows ‹⟦mk_mcs C S⟧ ⊨ p›
proof -
  have *: ‹MyHintikka (mk_mcs C S)›
  proof
    show ‹P.prop⇩H Kinds (mk_mcs C S)›
      using mk_mcs_Hintikka[OF assms(1-3)] Hintikka.hintikka by blast
  qed
  moreover have ‹p ∈ mk_mcs C S›
    using assms(4) Extend_subset by blast
  ultimately show ?thesis
    using MyHintikka.model by blast
qed


section ‹Propositional Semantics›

primrec boolean where
  ‹boolean _ _ ❙⊥ = False›
| ‹boolean G _ (❙⋅P ts) = G P ts›
| ‹boolean G A (p ❙⟶ q) = (boolean G A p ⟶ boolean G A q)›
| ‹boolean _ A (❙∀p) = A (❙∀p)›
| ‹boolean _ A (❙∀⇩Pp) = A (❙∀⇩Pp)›
| ‹boolean _ A (❙∀⇩Fp) = A (❙∀⇩Fp)›

abbreviation ‹tautology p ≡ ∀G A. boolean G A p›

proposition ‹tautology (❙∀(❙⋅P [❙#0]) ❙⟶ ❙∀(❙⋅P [❙#0]))›
  by simp

lemma boolean_semantics: ‹boolean (λa. ⦉E⇩P,G⦊⇩2 a ∘ map ⦉E, E⇩F, C, F⦊) (λp. (E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ p) = (λp. (E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ p)›
proof
  fix p
  show ‹boolean (λa. ⦉E⇩P, G⦊⇩2 a ∘ map ⦉E,E⇩F, C, F⦊) ((⊨) (E, E⇩F, E⇩P, C, F, G, PS, FS)) p = ((E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ p)›
    by (induct p) simp_all
qed

lemma tautology[simp]: ‹tautology p ⟹ (E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ p›
  using boolean_semantics by metis

proposition ‹∃p. (∀E E⇩F E⇩P C F G PS FS. (E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ p) ∧ ¬ tautology p›
  by (metis boolean.simps(4) fun_upd_same semantics_fm.simps(3) semantics_fm.simps(4) tautology)


section ‹Calculus›

text ‹Adapted from System Q1 by Smullyan in First-Order Logic (1968).›

inductive Axiomatic (‹⊢ _› [50] 50) where
  TA: ‹tautology p ⟹ ⊢ p›
| IA: ‹⊢ ❙∀p ❙⟶ ⟨t/0⟩p› 
| IA⇩P: ‹⊢ ❙∀⇩Pp ❙⟶ ⟨s/0⟩⇩Pp› 
| IA⇩F: ‹⊢ ❙∀⇩Fp ❙⟶ ⟨s/0⟩⇩Fp› 
| MP: ‹⊢ p ❙⟶ q ⟹ ⊢ p ⟹ ⊢ q› 
| GR: ‹⊢ q ❙⟶ ⟨❙⋆a/0⟩p ⟹ a ∉ params {p, q} ⟹ ⊢ q ❙⟶ ❙∀p› 
| GR⇩P: ‹⊢ q ❙⟶ ⟨❙○⇩2 a/0⟩⇩Pp ⟹ a ∉ params {p, q} ⟹ ⊢ q ❙⟶ ❙∀⇩Pp›
| GR⇩F: ‹⊢ q ❙⟶ ⟨❙○⇩2 a/0⟩⇩Fp ⟹ a ∉ params {p, q} ⟹ ⊢ q ❙⟶ ❙∀⇩Fp›

text ‹We simulate assumptions on the lhs of ‹⊢› with a chain of implications on the rhs.›

primrec imply (infixr ‹❙↝› 56) where
  ‹([] ❙↝ q) = q›
| ‹(p # ps ❙↝ q) = (p ❙⟶ ps ❙↝ q)›

abbreviation Axiomatic_assms (‹_ ⊢ _› [50, 50] 50) where
  ‹ps ⊢ q ≡ ⊢ ps ❙↝ q›

section ‹Soundness›

fun wf_model where
  ‹wf_model (E, E⇩F, E⇩P, C, F, G, PS, FS) ⟷ range G ⊆ PS ∧ range E⇩P ⊆ PS ∧ range F ⊆ FS ∧ range E⇩F ⊆ FS›

theorem soundness:
  shows ‹⊢ p ⟹ wf_model (E, E⇩F, E⇩P, C, F, G, PS, FS) ⟹ (E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ p›
proof (induct p arbitrary: C F G PS FS rule: Axiomatic.induct)
  case (TA p)
  then show ?case
    by simp 
next
  case (IA p t)
  then show ?case
    by auto
next
  case (IA⇩P p s)
  then show ?case
    by (cases s) (fastforce intro!: rangeI)+
next
  case (IA⇩F p s)
  then show ?case
    by (cases s) (fastforce intro!: rangeI)+
next
  case (MP p q)
  then show ?case
    by auto
next
  case (GR q a p)
  moreover from this have ‹(E, E⇩F, E⇩P, C(a := x), F, G, PS, FS) ⊨ (q ❙⟶ ⟨❙⋆a/0⟩p)› for x
    unfolding wf_model.simps by meson
  ultimately show ?case
    by fastforce
next
  case (GR⇩P q a p)
  moreover from this have ‹∀x. x ∈ PS ⟶ (E, E⇩F, E⇩P, C, F, G(a := x), PS,FS) ⊨ (q ❙⟶ ⟨❙○⇩2a/0⟩⇩Pp)›
    unfolding wf_model.simps
    by (metis (no_types, opaque_lifting) fun_upd_other fun_upd_same image_subset_iff)
  ultimately show ?case
    by fastforce
next
  case (GR⇩F q a p)
  moreover from this have ‹∀x. x ∈ FS ⟶ (E, E⇩F, E⇩P, C, F(a := x), G, PS,FS) ⊨ (q ❙⟶ ⟨❙○⇩2a/0⟩⇩Fp)›
    unfolding wf_model.simps
    by (metis (no_types, opaque_lifting) fun_upd_other fun_upd_same image_subset_iff)
  ultimately show ?case
    by fastforce
qed

corollary ‹¬ (⊢ ❙⊥)›
  using soundness[where p="❙⊥" and G="λp cs. True" and PS="{λcs. True}" and E⇩P="λn cs. True" and F="λp cs. ()"] by fastforce

section ‹Derived Rules›

lemma Imp1: ‹⊢ q ❙⟶ p ❙⟶ q›
  and Imp2: ‹⊢ (p ❙⟶ q ❙⟶ r) ❙⟶ (p ❙⟶ q) ❙⟶ p ❙⟶ r›
  and Neg: ‹⊢ ❙¬ ❙¬ p ❙⟶ p›
  by (auto intro: TA)

text ‹The tautology axiom TA is not used directly beyond this point.›

lemma Tran': ‹⊢ (q ❙⟶ r) ❙⟶ (p ❙⟶ q) ❙⟶ p ❙⟶ r›
  by (meson Imp1 Imp2 MP)

lemma Swap: ‹⊢ (p ❙⟶ q ❙⟶ r) ❙⟶ q ❙⟶ p ❙⟶ r›
  by (meson Imp1 Imp2 Tran' MP)

lemma Tran: ‹⊢ (p ❙⟶ q) ❙⟶ (q ❙⟶ r) ❙⟶ p ❙⟶ r›
  by (meson Swap Tran' MP)

text ‹Note that contraposition in the other direction is an instance of the lemma Tran.›

lemma contraposition: ‹⊢ (❙¬ q ❙⟶ ❙¬ p) ❙⟶ p ❙⟶ q›
  by (meson Neg Swap Tran MP)

lemma GR': ‹⊢ ❙¬ ⟨❙⋆a/0⟩p ❙⟶ q ⟹ a ∉ params {p, q} ⟹ ⊢ ❙¬ (❙∀p) ❙⟶ q›
proof -
  assume *: ‹⊢ ❙¬ ⟨❙⋆a/0⟩p ❙⟶ q› and a: ‹a ∉ params {p, q}›
  have ‹⊢ ❙¬ q ❙⟶ ❙¬ ❙¬ ⟨❙⋆a/0⟩p›
    using * Tran MP by metis
  then have ‹⊢ ❙¬ q ❙⟶ ⟨❙⋆a/0⟩p›
    using Neg Tran MP by metis
  then have ‹⊢ ❙¬ q ❙⟶ ❙∀p›
    using a by (auto intro: GR)
  then have ‹⊢ ❙¬ (❙∀p) ❙⟶ ❙¬ ❙¬ q›
    using Tran MP by metis
  then show ?thesis
    using Neg Tran MP by metis
qed

lemma GR⇩P': ‹⊢ ❙¬ ⟨❙○⇩2P/0⟩⇩Pp ❙⟶ q ⟹ P ∉ params {p, q} ⟹ ⊢ ❙¬ (❙∀⇩Pp) ❙⟶ q›
proof -
  assume *: ‹⊢ ❙¬ ⟨❙○⇩2P/0⟩⇩Pp ❙⟶ q› and a: ‹P ∉ params {p, q}›
  have ‹⊢ ❙¬ q ❙⟶ ❙¬ ❙¬ ⟨❙○⇩2P/0⟩⇩Pp›
    using * Tran MP by metis
  then have ‹⊢ ❙¬ q ❙⟶ ⟨❙○⇩2P/0⟩⇩Pp›
    using Neg Tran MP by metis
  then have ‹⊢ ❙¬ q ❙⟶ ❙∀⇩Pp›
    using a by (auto intro: GR⇩P)
  then have ‹⊢ ❙¬ (❙∀⇩Pp) ❙⟶ ❙¬ ❙¬ q›
    using Tran MP by metis
  then show ?thesis
    using Neg Tran MP by metis
qed

lemma GR⇩F': ‹⊢ ❙¬ ⟨❙○⇩2F/0⟩⇩Fp ❙⟶ q ⟹ F ∉ params {p, q} ⟹ ⊢ ❙¬ (❙∀⇩Fp) ❙⟶ q›
proof -
  assume *: ‹⊢ ❙¬ ⟨❙○⇩2F/0⟩⇩Fp ❙⟶ q› and a: ‹F ∉ params {p, q}›
  have ‹⊢ ❙¬ q ❙⟶ ❙¬ ❙¬ ⟨❙○⇩2F/0⟩⇩Fp›
    using * Tran MP by metis
  then have ‹⊢ ❙¬ q ❙⟶ ⟨❙○⇩2F/0⟩⇩Fp›
    using Neg Tran MP by metis
  then have ‹⊢ ❙¬ q ❙⟶ ❙∀⇩Fp›
    using a by (auto intro: GR⇩F)
  then have ‹⊢ ❙¬ (❙∀⇩Fp) ❙⟶ ❙¬ ❙¬ q›
    using Tran MP by metis
  then show ?thesis
    using Neg Tran MP by metis
qed

lemma imply_ImpE: ‹⊢ ps ❙↝ p ❙⟶ ps ❙↝ (p ❙⟶ q) ❙⟶ ps ❙↝ q›
proof (induct ps)
  case Nil
  then show ?case
    by (metis Imp1 Swap MP imply.simps(1))
next
  case (Cons r ps)
  have ‹⊢ (r ❙⟶ ps ❙↝ p) ❙⟶ r ❙⟶ ps ❙↝ (p ❙⟶ q) ❙⟶ ps ❙↝ q›
    by (meson Cons.hyps Imp1 Imp2 MP)
  then have ‹⊢ (r ❙⟶ ps ❙↝ p) ❙⟶ (r ❙⟶ ps ❙↝ (p ❙⟶ q)) ❙⟶ r ❙⟶ ps ❙↝ q›
    by (meson Imp1 Imp2 MP)
  then show ?case
    by simp
qed

lemma MP': ‹ps ⊢ p ❙⟶ q ⟹ ps ⊢ p ⟹ ps ⊢ q›
  using imply_ImpE MP by metis

lemma imply_Cons [intro]: ‹ps ⊢ q ⟹ p # ps ⊢ q›
  by (auto intro: MP Imp1)

lemma imply_head [intro]: ‹p # ps ⊢ p›
  by (induct ps) (metis Imp1 Imp2 MP imply.simps, metis Imp1 Imp2 MP imply.simps(2))

lemma add_imply [simp]: ‹⊢ q ⟹ ps ⊢ q›
  using imply_head by (metis MP imply.simps(2))

lemma imply_mem [simp]: ‹p ∈ set ps ⟹ ps ⊢ p›
  using imply_head imply_Cons by (induct ps) fastforce+

lemma deduct1: ‹ps ⊢ p ❙⟶ q ⟹ p # ps ⊢ q›
  by (meson MP' imply_Cons imply_head)

lemma imply_append [iff]: ‹(ps @ qs ❙↝ r) = (ps ❙↝ qs ❙↝ r)›
  by (induct ps) simp_all

lemma imply_swap_append: ‹ps @ qs ⊢ r ⟹ qs @ ps ⊢ r›
proof (induct qs arbitrary: ps)
  case Cons
  then show ?case
    by (metis deduct1 imply.simps(2) imply_append)
qed simp

lemma deduct2: ‹p # ps ⊢ q ⟹ ps ⊢ p ❙⟶ q›
  by (metis imply.simps imply_append imply_swap_append)

lemmas deduct [iff] = deduct1 deduct2

lemma cut: ‹p # ps ⊢ r ⟹ q # ps ⊢ p ⟹ q # ps ⊢ r›
  by (meson MP' deduct(2) imply_Cons)

lemma Boole: ‹(❙¬ p) # ps ⊢ ❙⊥ ⟹ ps ⊢ p›
  by (meson MP' Neg add_imply deduct(2))

lemma imply_weaken: ‹ps ⊢ q ⟹ set ps ⊆ set ps' ⟹ ps' ⊢ q›
  by (induct ps arbitrary: q) (simp, metis MP' deduct(2) imply_mem insert_subset list.simps(15))


section ‹Derivational Consistency›

interpretation DC: Weak_Derivational_Confl map_fm params_fm ‹λ_. True› confl_class ‹λA. ¬ A ⊢ ❙⊥›
proof
  fix A ps qs and q :: ‹'x fm›
  assume ‹ps ↝⇩✗ qs› ‹set ps ⊆ set A› ‹q ∈ set qs› ‹q ∈ set A›
  then show ‹¬ ¬ A ⊢ ❙⊥›
    by cases (simp, metis MP' empty_set equals0D imply_head imply_mem imply_weaken set_ConsD)
qed

interpretation DA: Weak_Derivational_Alpha map_fm params_fm ‹λ_. True› alpha_class ‹λA. ¬ A ⊢ ❙⊥›
proof (standard; safe)
  fix A and ps qs :: ‹'x fm list›
  assume ‹ps ↝⇩α qs› and *: ‹set ps ⊆ set A› ‹¬ A ⊢ ❙⊥› ‹qs @ A ⊢ ❙⊥›
  then show False
  proof cases
    case (CImpN p q)
    then have ‹A ⊢ ❙¬ (p ❙⟶ q)›
      using *(1) by simp
    moreover have ‹A ⊢ p ❙⟶ q›
      using CImpN(2) * Boole[of q]
      by (metis deduct2 imply.simps(1) imply.simps(2) imply_append)
    ultimately show ?thesis
      using MP' * by blast
  qed
qed

interpretation DB: Weak_Derivational_Beta map_fm params_fm ‹λ_. True› beta_class ‹λA. ¬ A ⊢ ❙⊥›
proof
  fix A and ps qs :: ‹'x fm list›
  assume ‹ps ↝⇩β qs› and *: ‹set ps ⊆ set A› ‹¬ A ⊢ ❙⊥›
  then show ‹∃q ∈ set qs. ¬ q # A ⊢ ❙⊥›
  proof cases
    case (CImpP p q)
    then show ?thesis
      using * Boole[of p A]
      by (metis MP' deduct2 imply_head imply_weaken insertI2 list.set_intros(1) list.simps(15))
  qed
qed

interpretation DG: Weak_Derivational_Gamma map_tm map_fm params_fm ‹λ_. True› G.classify_UNIV ‹λA. ¬ A ⊢ ❙⊥›
proof (unfold_locales; safe)
  fix A qs t and ps :: ‹'x fm list›
  assume ‹ps ↝⇩γ qs› and *: ‹set ps ⊆ set A› ‹¬ A ⊢ ❙⊥› ‹qs t @ A ⊢ ❙⊥›
  then show False
  proof cases
    case (CAllP p)
    then show ?thesis
      using * IA[of p t] MP'
      by (metis (mono_tags, lifting) imply.simps(1-2) imply_append imply_swap_append imply_weaken)
  qed
qed

interpretation DG⇩P: Weak_Derivational_Gamma map_sym map_fm params_fm ‹λ_. True› G⇩P.classify_UNIV ‹λA. ¬ A ⊢ ❙⊥›
proof (unfold_locales; safe)
  fix A qs t and ps :: ‹'x fm list›
  assume ‹ps ↝⇩γ⇩P qs› and *: ‹set ps ⊆ set A› ‹¬ A ⊢ ❙⊥› ‹qs t @ A ⊢ ❙⊥›
  then show False
  proof cases
    case (CAllPP p)
    then show ?thesis
      using * IA⇩P[of p t] MP'
      by (metis (mono_tags, lifting) imply.simps(1-2) imply_append imply_swap_append imply_weaken)
  qed
qed

interpretation DG⇩F: Weak_Derivational_Gamma map_sym map_fm params_fm ‹λ_. True› G⇩F.classify_UNIV ‹λA. ¬ A ⊢ ❙⊥›
proof (unfold_locales; safe)
  fix A qs t and ps :: ‹'x fm list›
  assume ‹ps ↝⇩γ⇩F qs› and *: ‹set ps ⊆ set A› ‹¬ A ⊢ ❙⊥› ‹qs t @ A ⊢ ❙⊥›
  then show False
  proof cases
    case (CAllFP p)
    then show ?thesis
      using * IA⇩F[of p t] MP'
      by (metis (mono_tags, lifting) imply.simps(1-2) imply_append imply_swap_append imply_weaken)
  qed
qed

lemma imply_params_fm: ‹params_fm (ps ❙↝ q) = params_fm q ∪ (⋃p ∈ set ps. params_fm p)›
  by (induct ps) auto

interpretation DD: Weak_Derivational_Delta map_fm params_fm ‹λ_. True› δ ‹λA. ¬ A ⊢ ❙⊥›
proof (standard; safe)
  fix A a and p :: ‹'x fm›
  assume ‹p ∈ set A› ‹a ∉ P.params (set A)› ‹¬ A ⊢ ❙⊥› ‹δ p a @ A ⊢ ❙⊥›
  then show False
  proof (induct p a rule: δ.induct)
    case (1 p x)
    have ‹x ∉ P.params {p, A ❙↝ ❙⊥}›
      using 1(1-2) imply_params_fm[of A ‹❙⊥›] by auto
    moreover have ‹❙¬ ⟨❙⋆x/0⟩p # A ⊢ ❙⊥›
      using 1(4) by simp
    ultimately have ‹❙¬ ❙∀p # A ⊢ ❙⊥›
      using GR'[of x p] by simp
    then show ?thesis
      using 1 by (meson Boole MP' imply_mem)
  next
    case (2 p x)
    have ‹x ∉ P.params {p, A ❙↝ ❙⊥}›
      using 2(1-2) imply_params_fm[of A ‹❙⊥›] by auto
    moreover have ‹❙¬ ⟨❙○⇩2 x/0⟩⇩P p # A ⊢ ❙⊥›
      using 2(4) by simp
    ultimately have ‹❙¬ ❙∀⇩P p # A ⊢ ❙⊥›
      using GR⇩P'[of x p] by simp
    then show ?thesis
      using 2 by (meson Boole MP' imply_mem)
  next
    case (3 p x)
    have ‹x ∉ P.params {p, A ❙↝ ❙⊥}›
      using 3(1-2) imply_params_fm[of A ‹❙⊥›] by auto
    moreover have ‹❙¬ ⟨❙○⇩2 x/0⟩⇩F p # A ⊢ ❙⊥›
      using 3(4) by simp
    ultimately have ‹❙¬ ❙∀⇩F p # A ⊢ ❙⊥›
      using GR⇩F'[of x p] by simp
    then show ?thesis
      using 3 by (meson Boole MP' imply_mem)
  qed simp_all
qed

term P.params

interpretation Weak_Derivational_Consistency map_fm params_fm ‹λ_. True› Kinds ‹λA. ¬ A ⊢ ❙⊥›
proof
  assume ‹infinite (UNIV :: 'x set)›
  then have inf: ‹infinite (Collect (λ_. True) :: 'x set)›
    by simp
  then show ‹P.prop⇩E Kinds {S :: 'x fm set. ∃A. set A = S ∧ ¬ A ⊢ ❙⊥}›
    using prop⇩E_Kinds[OF DC.kind[OF inf] DA.kind DB.kind DG.kind DG⇩P.kind DG⇩F.kind DD.kind]
    by blast
qed

theorem weak_completeness:
  fixes p :: ‹'x fm›
  assumes mod: ‹∀(E :: _ ⇒ 'x tm) E⇩F E⇩P C F G PS FS. wf_model (E, E⇩F, E⇩P, C, F, G, PS, FS) ⟶ (∀q ∈ set ps. (E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ q) ⟶ (E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ p›
    and ‹P.enough_new (set ps)›
  shows ‹ps ⊢ p›
proof (rule ccontr)
  assume ‹¬ ps ⊢ p›
  then have *: ‹¬ (❙¬ p) # ps ⊢ ❙⊥›
    using Boole by blast

  let ?S = ‹set (❙¬ p # ps)›
  let ?C = ‹{S :: 'x fm set. ∃A. set A = S ∧ ¬ A ⊢ ❙⊥}›
  let ?M = ‹⟦mk_mcs ?C ?S⟧›

  have ‹infinite (UNIV :: 'x set)›
    using assms(2) card_of_ordLeq_infinite finite_subset inf_univ subset_UNIV
    unfolding P.enough_new_def by blast
  then have ‹P.prop⇩E Kinds ?C›
    using Consistency by blast
  moreover have ‹?S ∈ ?C›
    using * by blast
  moreover have ‹P.enough_new ?S›
    using assms(2) P.infinite_params_left unfolding P.enough_new_def
    by (metis Set_Diff_Un UN_Un card_of_diff inf_univ ordLeq_transitive)
  ultimately have *: ‹∀p ∈ ?S. ?M ⊨ p›
    using model_existence by blast 
  then have ‹?M ⊨ p›
    using mod unfolding hdom⇩F_def by auto
  then show False
    using * by simp
qed

theorem completeness:
  fixes p :: ‹'x fm›
  assumes ‹∀(E :: nat ⇒ 'x tm) E⇩P E⇩F C F G PS FS.  wf_model (E, E⇩F, E⇩P, C, F, G, PS, FS) ⟶ (E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ p›
    and ‹|UNIV :: 'x fm set| ≤o  |UNIV :: 'x set|›
  shows ‹⊢ p›
  using assms weak_completeness[where ps=‹[]›, of p] unfolding P.enough_new_def by simp

section ‹Natural Deduction›

locale Natural_Deduction
begin

inductive ND_Set :: ‹'x fm set ⇒ 'x fm ⇒ bool› (infix ‹⊩› 50) where
  Assm [dest]: ‹p ∈ A ⟹ A ⊩ p›
| FlsE [elim]: ‹A ⊩ ❙⊥ ⟹ A ⊩ p›
| ImpI [intro]: ‹{p} ∪ A ⊩ q ⟹ A ⊩ p ❙⟶ q›
| ImpE [dest]: ‹A ⊩ p ❙⟶ q ⟹ A ⊩ p ⟹ A ⊩ q›
| UniI [intro]: ‹A ⊩ ⟨❙⋆a/0⟩p ⟹ a ∉ P.params ({p} ∪ A) ⟹ A ⊩ ❙∀p›
| UniE [dest]: ‹A ⊩ ❙∀p ⟹ A ⊩ ⟨t/0⟩p›
| UniI⇩P [intro]: ‹A ⊩ ⟨❙○⇩2 a/0⟩⇩P p ⟹ a ∉ P.params ({p} ∪ A) ⟹ A ⊩ ❙∀⇩P p›
| UniE⇩P [dest]: ‹A ⊩ ❙∀⇩P p ⟹ A ⊩ ⟨s/0⟩⇩P p›
| UniI⇩F [intro]: ‹A ⊩ ⟨❙○⇩2 a/0⟩⇩F p ⟹ a ∉ P.params ({p} ∪ A) ⟹ A ⊩ ❙∀⇩F p›
| UniE⇩F [dest]: ‹A ⊩ ❙∀⇩F p ⟹ A ⊩ ⟨s/0⟩⇩F p›
| Clas: ‹{p ❙⟶ q} ∪ A ⊩ p ⟹ A ⊩ p›

subsection ‹Soundness›

theorem soundness_set:
  assumes ‹A ⊩ p› ‹wf_model (E, E⇩F, E⇩P, C, F, G, PS, FS)›
  shows ‹∀q ∈ A. (E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ q ⟹ (E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ p›
  using assms
proof (induct A p arbitrary: C F G pred: ND_Set)
  case (UniI A a p)
  have ‹∀q ∈ A. (E, E⇩F, E⇩P, C(a := x), F, G, PS, FS) ⊨ q› for x
    using UniI(3-) by simp
  moreover have ‹wf_model (E, E⇩F, E⇩P, C(a := x), F, G, PS, FS)› for x
    using UniI(5) by simp
  ultimately have ‹(E, E⇩F, E⇩P, C(a := x), F, G, PS, FS) ⊨ ⟨❙⋆a/0⟩p› for x
    using UniI by meson
  then show ?case
    using UniI by simp
next
  case (UniI⇩P A a p)
  have ‹∀x ∈ PS. ∀q ∈ A. (E, E⇩F, E⇩P, C, F, G(a := x), PS, FS) ⊨ q›
    using UniI⇩P(3-) by simp
  moreover have ‹∀x ∈ PS. wf_model (E, E⇩F, E⇩P, C, F, G(a := x), PS, FS)›
    using UniI⇩P(5) by auto
  ultimately have ‹∀x ∈ PS. (E, E⇩F, E⇩P, C, F, G(a := x), PS, FS) ⊨ ⟨❙○⇩2 a/0⟩⇩P p›
    using UniI⇩P by meson
  then show ?case
    using UniI⇩P by simp
next
  case (UniE⇩P A p s)
  then show ?case
    by (cases s) (fastforce intro!: rangeI)+
next
  case (UniI⇩F A a p)
  have ‹∀x ∈ FS. ∀q ∈ A. (E, E⇩F, E⇩P, C, F(a := x), G, PS, FS) ⊨ q›
    using UniI⇩F(3-) by simp
  moreover have ‹∀x ∈ FS. wf_model (E, E⇩F, E⇩P, C, F(a := x), G, PS, FS)›
    using UniI⇩F(5) by auto
  ultimately have ‹∀x ∈ FS. (E, E⇩F, E⇩P, C, F(a := x), G, PS, FS) ⊨ ⟨❙○⇩2 a/0⟩⇩F p›
    using UniI⇩F by meson
  then show ?case
    using UniI⇩F by simp
next
  case (UniE⇩F A p s)
  then show ?case
    by (cases s) (fastforce intro!: rangeI)+
qed auto

subsection ‹Derivational Consistency›

lemma Boole: ‹{❙¬ p} ∪ A ⊩ ❙⊥ ⟹ A ⊩ p›
  using Clas FlsE by blast

sublocale DC: Derivational_Confl map_fm params_fm ‹λ_. True› confl_class ‹λA. ¬ A ⊩ ❙⊥›
proof
  fix A ps qs and q :: ‹'x fm›
  assume ‹ps ↝⇩✗ qs› ‹set ps ⊆ A› ‹q ∈ set qs› ‹q ∈ A›
  then show ‹¬ ¬ A ⊩ ❙⊥›
    by cases auto
qed

sublocale DA: Derivational_Alpha map_fm params_fm ‹λ_. True› alpha_class ‹λA. ¬ A ⊩ ❙⊥›
proof (standard; safe)
  fix A and ps qs :: ‹'x fm list›
  assume ‹ps ↝⇩α qs› and *: ‹set ps ⊆ A› ‹¬ A ⊩ ❙⊥› ‹set qs ∪ A ⊩ ❙⊥›
  then show False
  proof cases
    case (CImpN p q)
    then have ‹A ⊩ ❙¬ (p ❙⟶ q)›
      using *(1) by auto
    moreover have ‹A ⊩ p ❙⟶ q›
      using CImpN(2) * Boole[of q ‹{p} ∪ A›] by auto
    ultimately show ?thesis
      using * by blast
  qed
qed

sublocale DB: Derivational_Beta map_fm params_fm ‹λ_. True› beta_class ‹λA. ¬ A ⊩ ❙⊥›
proof
  fix A and ps qs :: ‹'x fm list›
  assume ‹ps ↝⇩β qs› and *: ‹set ps ⊆ A› ‹¬ A ⊩ ❙⊥›
  then show ‹∃q ∈ set qs. ¬ {q} ∪ A ⊩ ❙⊥›
  proof cases
    case (CImpP p q)
    then show ?thesis
      using * Boole[of p A]
      by (metis Assm ImpE ImpI list.set_intros(1) set_subset_Cons subset_iff)
  qed
qed

sublocale DG: Derivational_Gamma map_tm map_fm params_fm ‹λ_. True› G.classify_UNIV ‹λA. ¬ A ⊩ ❙⊥›
proof (unfold_locales; safe)
  fix A qs t and ps :: ‹'x fm list›
  assume ‹ps ↝⇩γ qs› and *: ‹set ps ⊆ A› ‹¬ A ⊩ ❙⊥› ‹set (qs t) ∪ A ⊩ ❙⊥›
  then show False
  proof cases
    case (CAllP p)
    then show ?thesis
      using * UniE[of A p t] ImpI by auto
  qed
qed

sublocale DGP: Derivational_Gamma map_sym map_fm params_fm ‹λ_. True› G⇩P.classify_UNIV ‹λA. ¬ A ⊩ ❙⊥›
proof (unfold_locales; safe)
  fix A qs t and ps :: ‹'x fm list›
  assume ‹ps ↝⇩γ⇩P qs› and *: ‹set ps ⊆ A› ‹¬ A ⊩ ❙⊥› ‹set (qs t) ∪ A ⊩ ❙⊥›
  then show False
  proof cases
    case (CAllPP p)
    then show ?thesis
      using * UniE⇩P[of A p t] ImpI by auto
  qed
qed

sublocale DGF: Derivational_Gamma map_sym map_fm params_fm ‹λ_. True› G⇩F.classify_UNIV ‹λA. ¬ A ⊩ ❙⊥›
proof (unfold_locales; safe)
  fix A qs t and ps :: ‹'x fm list›
  assume ‹ps ↝⇩γ⇩F qs› and *: ‹set ps ⊆ A› ‹¬ A ⊩ ❙⊥› ‹set (qs t) ∪ A ⊩ ❙⊥›
  then show False
  proof cases
    case (CAllFP p)
    then show ?thesis
      using * UniE⇩F[of A p t] ImpI by auto
  qed
qed

sublocale DD: Derivational_Delta map_fm params_fm ‹λ_. True› δ ‹λA. ¬ A ⊩ ❙⊥›
proof (standard; safe)
  fix A a and p :: ‹'x fm›
  assume ‹p ∈ A› ‹a ∉ P.params A› ‹¬ A ⊩ ❙⊥›  ‹set (δ p a) ∪ A ⊩ ❙⊥›
  then show False
  proof (induct p a rule: δ.induct)
    case (1 p x)
    then have ‹x ∉ P.params ({p} ∪ A)›
      by auto
    moreover have ‹A ⊩ ⟨❙⋆x/0⟩ p›
      using 1(4) Boole by auto
    ultimately show ?case
      using 1 UniI by blast
  next
    case (2 p x)
    then have ‹x ∉ P.params ({p} ∪ A)›
      by auto
    moreover have ‹A ⊩ ⟨❙○⇩2 x/0⟩⇩P p›
      using 2(4) Boole by auto
    ultimately show ?case
      using 2 UniI⇩P by blast
  next
    case (3 p x)
    then have ‹x ∉ P.params ({p} ∪ A)›
      by auto
    moreover have ‹A ⊩ ⟨❙○⇩2 x/0⟩⇩F p›
      using 3(4) Boole by auto
    ultimately show ?case
      using 3 UniI⇩F by blast
  qed simp_all
qed

sublocale Derivational_Consistency map_fm params_fm ‹λ_. True› Kinds ‹λA. ¬ A ⊩ ❙⊥›
  using prop⇩E_Kinds[OF DC.kind DA.kind DB.kind DG.kind DGP.kind DGF.kind DD.kind] by unfold_locales

subsection ‹Strong Completeness›

theorem strong_completeness:
  fixes p :: ‹'x fm›
  assumes mod: ‹⋀(E :: nat ⇒ 'x tm) E⇩F E⇩P C F G PS FS. wf_model (E, E⇩F, E⇩P, C, F, G, PS, FS) ⟹
      (∀q ∈ A. (E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ q) ⟹ (E, E⇩F, E⇩P, C, F, G, PS, FS) ⊨ p›
    and ‹P.enough_new A›
  shows ‹A ⊩ p›
proof (rule ccontr)
  assume ‹¬ A ⊩ p›
  then have *: ‹¬ {❙¬ p} ∪ A ⊩ ❙⊥›
    using Boole by (metis insert_is_Un)

  let ?S = ‹set [❙¬ p] ∪ A›
  let ?C = ‹{A. P.enough_new A ∧ ¬ A ⊩ ❙⊥}›
  let ?M = ‹⟦mk_mcs ?C ?S⟧›

  have wf: ‹wf_model ?M›
    unfolding hdom⇩F_def by simp

  have ‹P.prop⇩E Kinds ?C›
    using Consistency by blast
  moreover have ‹P.enough_new ?S›
    using assms(2) params_left by blast
  moreover from this have ‹?S ∈ ?C›
    using * by simp
  ultimately have *: ‹∀p ∈ ?S. ?M ⊨ p›
    using model_existence by blast
  then have ‹?M ⊨ p›
    using mod[OF wf] by fast 
  then show False
    using * by simp
qed

proposition ‹∃M. wf_model M›
  by (meson sup.cobounded2 sup_ge1 wf_model.simps)

end

end