Theory Example_PIL

(*
  File: Example_PIL.thy
  Title: Example Completeness Proof for a Natural Deduction Calculus for Prior's Ideal Language
  Author: Asta Halkjær Boserup, 2025-2026.
  Reference:
    Blackburn, P. R., Braüner, T., & Kofod, J. L. Prior's Ideal Language.
    Mathematical Structures in Computer Science.
*)

chapter ‹Example: Prior's Ideal Logic›

theory Example_PIL imports
  Abstract_Consistency_Property
  "HOL-Number_Theory.Number_Theory"
begin

no_syntax
  "_Pi" :: "pttrn ⇒ 'a set ⇒ 'b set ⇒ ('a ⇒ 'b) set"
    (‹(‹indent=3 notation=‹binder Π∈››Π _∈_./ _)› 10)

section ‹Syntax›

datatype (symbols_tm: 'x) tm
  = Var nat (‹❙#›)
  | Sym 'x (‹❙○›)

datatype (symbols_fm: 'x) fm
  = TmI ‹'x tm› (‹❙∙›)
  | TmP ‹'x tm› (‹❙⋅›)
  | Neg ‹'x fm› (‹❙¬ _› [70] 70)
  | Con ‹'x fm› ‹'x fm› (infixr ‹❙∧› 35)
  | Box ‹'x fm› (‹❙□›)
  | Sat ‹'x tm› ‹'x fm› (‹❙@›)
  | Glo ‹'x fm› (‹❙A›)
  | Dwn ‹'x fm› (‹❙↓›)
  | All ‹'x fm› (‹❙∀›)

abbreviation Fls :: ‹'x fm› (‹❙⊥›) where
  ‹❙⊥ ≡ undefined ❙∧ ❙¬ undefined›

abbreviation Imp :: ‹'x fm ⇒ 'x fm ⇒ 'x fm› (infixr ‹❙⟶› 55) where
  ‹p ❙⟶ q ≡ ❙¬ (p ❙∧ ❙¬ q)›

abbreviation Dia :: ‹'x fm ⇒ 'x fm› (‹❙◇›) where
  ‹❙◇ p ≡ ❙¬ (❙□ (❙¬ p))›

type_synonym 'x lbd = ‹'x tm × 'x fm›

section ‹Semantics›

record 'w frame =
  𝒲 :: ‹'w set›
  ℛ :: ‹'w ⇒ 'w set›

record 'w gframe = ‹'w frame› +
  Π :: ‹'w set set›

record ('x, 'w) model = ‹'w gframe› +
  𝒩 :: ‹'x ⇒ 'w›
  𝔑 :: ‹nat ⇒ 'w›
  𝒱 :: ‹'x ⇒ 'w set›
  𝔙 :: ‹nat ⇒ 'w set›

abbreviation ‹Model W R PI N e V f ≡ ⦇𝒲 = W, ℛ = R, Π = PI, 𝒩 = N, 𝔑 = e, 𝒱 = V, 𝔙 = f⦈›

definition admissible :: ‹'w frame ⇒ 'w set set ⇒ bool› where
  ‹admissible M PI ≡
    (∀X ∈ PI. 𝒲 M - X ∈ PI) ∧
    (∀X ∈ PI. ∀Y ∈ PI. X ∩ Y ∈ PI) ∧
    (∀X ∈ PI. {w ∈ 𝒲 M. ∀v ∈ ℛ M w. v ∈ X} ∈ PI)›

definition wf_frame :: ‹'w frame ⇒ bool› where
  ‹wf_frame M ≡ 𝒲 M ≠ {} ∧ ℛ M ` 𝒲 M ⊆ Pow (𝒲 M)›

definition wf_gframe :: ‹'w gframe ⇒ bool› where
  ‹wf_gframe M ≡ wf_frame (frame.truncate M) ∧ Π M ≠ {} ∧ Π M ⊆ Pow (𝒲 M) ∧ admissible (frame.truncate M) (Π M)›

definition wf_env :: ‹('x, 'w) model ⇒ bool› where
  ‹wf_env M ≡ range (𝒩 M) ⊆ 𝒲 M ∧ range (𝔑 M) ⊆ 𝒲 M ∧ range (𝒱 M) ⊆ Π M ∧ range (𝔙 M) ⊆ Π M›

definition wf_model :: ‹('x, 'w) model ⇒ bool› where
  ‹wf_model M ≡ wf_gframe (gframe.truncate M) ∧ wf_env M›

lemmas unfolds =
  model.defs gframe.defs frame.defs
  model.select_convs gframe.select_convs frame.select_convs

context
  fixes M :: ‹('x, 'w) model›
  assumes wf: ‹wf_model M›
begin

lemma wf_compl: ‹X ∈ Π M ⟹ 𝒲 M - X ∈ Π M›
  using wf unfolding wf_model_def wf_gframe_def admissible_def unfolds by blast

lemma wf_inter: ‹X ∈ Π M ⟹ Y ∈ Π M ⟹ X ∩ Y ∈ Π M›
  using wf unfolding wf_model_def wf_gframe_def admissible_def unfolds by blast

lemma wf_modal: ‹X ∈ Π M ⟹ {w ∈ 𝒲 M. ∀v ∈ ℛ M w. v ∈ X} ∈ Π M›
  using wf unfolding wf_model_def wf_gframe_def admissible_def unfolds by blast

lemma wf_empty: ‹{} ∈ Π M›
  using wf wf_compl wf_inter unfolding wf_model_def wf_gframe_def unfolds by force

lemma wf_univ: ‹𝒲 M ∈ Π M›  
  using wf wf_empty wf_compl by fastforce

lemma wf_Π: ‹P ∈ Π M ⟹ P ⊆ 𝒲 M›
  using wf unfolding wf_gframe_def wf_model_def unfolds by fast

lemma wf_𝒩: ‹𝒩 M i ∈ 𝒲 M›
  using wf unfolding wf_model_def wf_env_def by fast

lemma wf_𝔑: ‹𝔑 M n ∈ 𝒲 M›
  using wf unfolding wf_model_def wf_env_def by blast

lemma wf_𝒱: ‹𝒱 M P ∈ Π M›
  using wf unfolding wf_model_def wf_env_def by blast

lemma wf_𝒱': ‹𝒱 M n ⊆ 𝒲 M›
  using wf wf_𝒱 wf_Π by blast

lemma wf_𝔙: ‹𝔙 M n ∈ Π M›
  using wf unfolding wf_model_def wf_env_def by blast

lemma wf_𝔙': ‹𝔙 M n ⊆ 𝒲 M›
  using wf wf_𝔙 wf_Π by blast

end

type_synonym ('x, 'w) ctx = ‹('x, 'w) model × 'w›

primrec add_env :: ‹'a ⇒ (nat ⇒ 'a) ⇒ nat ⇒ 'a› (infixr ‹⪢› 0) where
  ‹(t ⪢ e) 0 = t›
| ‹(_ ⪢ e) (Suc n) = e n›

fun semantics :: ‹('x, 'w) ctx ⇒ 'x fm ⇒ bool› (infix ‹⊨› 50) where
  ‹((M, w) ⊨ ❙∙t) = (case_tm (𝔑 M) (𝒩 M) t = w)›
| ‹((M, w) ⊨ ❙⋅P) = (w ∈ case_tm (𝔙 M) (𝒱 M) P)›
| ‹((M, w) ⊨ (❙¬ p)) = (¬ (M, w) ⊨ p)›
| ‹((M, w) ⊨ (p ❙∧ q)) = ((M, w) ⊨ p ∧ (M, w) ⊨ q)›
| ‹((M, w) ⊨ ❙□ p) = (∀v ∈ ℛ M w. (M, v) ⊨ p)›
| ‹((M, _) ⊨ ❙@i p) = ((M, case_tm (𝔑 M) (𝒩 M) i) ⊨ p)›
| ‹((M, _) ⊨ ❙A p) = (∀v ∈ 𝒲 M. (M, v) ⊨ p)›
| ‹((M, w) ⊨ ❙↓ p) = ((M⦇𝔑 := (w ⪢ 𝔑 M)⦈, w) ⊨ p)›
| ‹((M, w) ⊨ ❙∀ p) = (∀P ∈ Π M. (M⦇𝔙 := (P ⪢ 𝔙 M)⦈, w) ⊨ p)›

lemma ‹(M, w) ⊨ p ❙⟶ q ⟷ (M, w) ⊨ p ⟶ (M, w) ⊨ q›
  by simp

lemma ‹(M, w) ⊨ ❙↓(❙∙(❙#0))›
  by (cases M) simp

lemma ‹(M, w) ⊨ ❙∀(❙@(❙○k) (❙⋅(❙#0))) ❙⟶ ❙@(❙○k) (❙∀(❙⋅(❙#0)))›
  by (cases M) auto

lemma ‹(M, w) ⊨ ❙@(❙○k) (❙∀(❙⋅(❙#0))) ❙⟶ ❙∀(❙@(❙○k) (❙⋅(❙#0)))›
  by (cases M) auto

lemma ‹wf_model M ⟹ (M, w) ⊨ ❙∀(❙⋅(❙#0)) ❙⟶ ❙⋅P›
  unfolding wf_model_def wf_env_def by (fastforce split: tm.splits)

lemma ‹wf_model M ⟹ (M, w) ⊨ ❙∀(❙@(❙○k) (❙⋅(❙#0))) ❙⟶ ❙↓(❙∙(❙○k) ❙⟶ ❙@(❙#0) (❙⋅P))›
  unfolding wf_model_def wf_env_def by (fastforce split: tm.splits)

section ‹Operations›

abbreviation map_lbd :: ‹('x ⇒ 'k) ⇒ 'x lbd ⇒ 'k lbd› where
  ‹map_lbd f ≡ map_prod (map_tm f) (map_fm f)›

primrec symbols_lbd :: ‹'x lbd ⇒ 'x set› where
  ‹symbols_lbd (i, p) = symbols_tm i ∪ symbols_fm p›

abbreviation symbols :: ‹'x lbd set ⇒ 'x set› where
  ‹symbols S ≡ ⋃ip ∈ S. symbols_lbd ip›

abbreviation lift_tm :: ‹nat ⇒ 'x tm ⇒ 'x tm› where
  ‹lift_tm m ≡ case_tm (λn. if n < m then ❙#n else ❙#(n + m + 1)) ❙○›

primrec vars_tm :: ‹nat ⇒ 'x tm ⇒ nat set› where
  ‹vars_tm m (❙#n) = (if n ≤ m then {} else {n})›
| ‹vars_tm _ (❙○_) = {}›

primrec vars_fm :: ‹nat ⇒ 'x fm ⇒ nat set› where
  ‹vars_fm m (❙∙t) = vars_tm m t›
| ‹vars_fm m (❙⋅P) = vars_tm m P›
| ‹vars_fm m (❙¬ p) = vars_fm m p›
| ‹vars_fm m (p ❙∧ q) = vars_fm m p ∪ vars_fm m q›
| ‹vars_fm m (❙□ p) = vars_fm m p›
| ‹vars_fm m (❙@i p) = vars_tm m i ∪ vars_fm m p›
| ‹vars_fm m (❙A p) = vars_fm m p›
| ‹vars_fm m (❙↓ p) = vars_fm (m + 1) p›
| ‹vars_fm m (❙∀ p) = vars_fm (m + 1) p›

subsubsection ‹Nominals›

primrec sub_tm :: ‹(nat ⇒ 'x tm) ⇒ 'x tm ⇒ 'x tm› where
  ‹sub_tm s (❙#n) = s n›
| ‹sub_tm _ (❙○k) = ❙○k›

primrec sub_nom :: ‹(nat ⇒ 'x tm) ⇒ 'x fm ⇒ 'x fm› where
  ‹sub_nom s (❙∙t) = ❙∙(sub_tm s t)›
| ‹sub_nom _ (❙⋅P) = ❙⋅P›
| ‹sub_nom s (❙¬ p) = ❙¬ sub_nom s p›
| ‹sub_nom s (p ❙∧ q) = (sub_nom s p ❙∧ sub_nom s q)›
| ‹sub_nom s (❙□ p) = ❙□(sub_nom s p)›
| ‹sub_nom s (❙@i p) = ❙@(sub_tm s i) (sub_nom s p)›
| ‹sub_nom s (❙A p) = ❙A (sub_nom s p)›
| ‹sub_nom s (❙↓ p) = ❙↓ (sub_nom (❙#0 ⪢ λn. lift_tm 0 (s n)) p)›
| ‹sub_nom s (❙∀ p) = ❙∀ (sub_nom s p)›

abbreviation inst_single_nom :: ‹'x tm ⇒ 'x fm ⇒ 'x fm› (‹⟨_⟩⇩_i›) where
  ‹⟨t⟩⇩_i ≡ sub_nom (t ⪢ ❙#)›

subsubsection ‹Propositions›

fun softqdf :: ‹'x fm ⇒ bool› where
  ‹softqdf (❙∙_) = False›
| ‹softqdf (❙⋅P) = True›
| ‹softqdf (❙¬ p) = softqdf p›
| ‹softqdf (p ❙∧ q) = (softqdf p ∧ softqdf q)›
| ‹softqdf (❙□ p) = softqdf p›
| ‹softqdf (❙@i p) = softqdf p›
| ‹softqdf (❙A p) = softqdf p›
| ‹softqdf (❙↓ p) = False›
| ‹softqdf (❙∀ p) = False›

abbreviation softqdf_sub :: ‹(nat ⇒ 'x fm) ⇒ bool› where
  ‹softqdf_sub s ≡ ∀n. softqdf (s n)›

primrec lift_fm_nom :: ‹nat ⇒ 'x fm ⇒ 'x fm› where
  ‹lift_fm_nom m (❙∙t) = ❙∙(lift_tm m t)›
| ‹lift_fm_nom _ (❙⋅P) = ❙⋅P›
| ‹lift_fm_nom m (❙¬ p) = ❙¬ lift_fm_nom m p›
| ‹lift_fm_nom m (p ❙∧ q) = (lift_fm_nom m p ❙∧ lift_fm_nom m q)›
| ‹lift_fm_nom m (❙□ p) = ❙□(lift_fm_nom m p)›
| ‹lift_fm_nom m (❙@i p) = ❙@(lift_tm m i) (lift_fm_nom m p)›
| ‹lift_fm_nom m (❙A p) = ❙A (lift_fm_nom m p)›
| ‹lift_fm_nom m (❙↓ p) = ❙↓ (lift_fm_nom (m + 1) p)›
| ‹lift_fm_nom m (❙∀ p) = ❙∀ (lift_fm_nom m p)›

primrec lift_fm_pro :: ‹nat ⇒ 'x fm ⇒ 'x fm› where
  ‹lift_fm_pro _ (❙∙t) = ❙∙t›
| ‹lift_fm_pro m (❙⋅P) = ❙⋅(lift_tm m P)›
| ‹lift_fm_pro m (❙¬ p) = ❙¬ lift_fm_pro m p›
| ‹lift_fm_pro m (p ❙∧ q) = (lift_fm_pro m p ❙∧ lift_fm_pro m q)›
| ‹lift_fm_pro m (❙□ p) = ❙□(lift_fm_pro m p)›
| ‹lift_fm_pro m (❙@i p) = ❙@i (lift_fm_pro m p)›
| ‹lift_fm_pro m (❙A p) = ❙A (lift_fm_pro m p)›
| ‹lift_fm_pro m (❙↓ p) = ❙↓ (lift_fm_pro m p)›
| ‹lift_fm_pro m (❙∀ p) = ❙∀ (lift_fm_pro (m + 1) p)›

primrec sub_pro :: ‹(nat ⇒ 'x fm) ⇒ 'x fm ⇒ 'x fm› where
  ‹sub_pro _ (❙∙t) = ❙∙t›
| ‹sub_pro s (❙⋅P) = case_tm s (❙⋅ o ❙○) P›
| ‹sub_pro s (❙¬ p) = ❙¬ sub_pro s p›
| ‹sub_pro s (p ❙∧ q) = (sub_pro s p ❙∧ sub_pro s q)›
| ‹sub_pro s (❙□ p) = ❙□(sub_pro s p)›
| ‹sub_pro s (❙@i p) = ❙@i (sub_pro s p)›
| ‹sub_pro s (❙A p) = ❙A (sub_pro s p)›
| ‹sub_pro s (❙↓ p) = ❙↓ (sub_pro (lift_fm_nom 0 o s) p)›
| ‹sub_pro s (❙∀ p) = ❙∀ (sub_pro (❙⋅(❙#0) ⪢ λn. lift_fm_pro 0 (s n)) p)›

abbreviation inst_single_pro :: ‹'x fm ⇒ 'x fm ⇒ 'x fm› (‹⟨_⟩⇩_p›) where
  ‹⟨q⟩⇩_p ≡ sub_pro (q ⪢ ❙⋅ o ❙#)›

primrec sz_fm :: ‹'x fm ⇒ nat› where
  ‹sz_fm (❙∙t) = 1›
| ‹sz_fm (❙⋅P) = 1›
| ‹sz_fm (❙¬ p) = sz_fm p + 1›
| ‹sz_fm (p ❙∧ q) = sz_fm p + sz_fm q + 1›
| ‹sz_fm (❙□ p) = sz_fm p + 1›
| ‹sz_fm (❙@i p) = sz_fm p + 1›
| ‹sz_fm (❙A p) = sz_fm p + 1›
| ‹sz_fm (❙↓ p) = sz_fm p + 1›
| ‹sz_fm (❙∀ p) = sz_fm p + 1›

primrec qs_fm :: ‹'x fm ⇒ nat› where
  ‹qs_fm (❙∙t) = 0›
| ‹qs_fm (❙⋅P) = 0›
| ‹qs_fm (❙¬ p) = qs_fm p›
| ‹qs_fm (p ❙∧ q) = max (qs_fm p) (qs_fm q)›
| ‹qs_fm (❙□ p) = qs_fm p›
| ‹qs_fm (❙@i p) = qs_fm p›
| ‹qs_fm (❙A p) = qs_fm p›
| ‹qs_fm (❙↓ p) = qs_fm p›
| ‹qs_fm (❙∀ p) = qs_fm p + 1›

subsection ‹Lemmas›

subsubsection ‹Finite›

lemma finite_symbols_tm [simp]: ‹finite (symbols_tm t)›
  by (induct t) simp_all

lemma finite_symbols_fm [simp]: ‹finite (symbols_fm p)›
  by (induct p) simp_all

lemma finite_symbols_lbd: ‹finite (symbols_lbd p)›
  by (cases p) simp

subsubsection ‹Terms›

lemma env [simp]: ‹P ((x ⪢ E) n) = (P x ⪢ λn. P (E n)) n›
  by (induct n) simp_all

lemma lift_lemma [simp]: ‹case_tm (x ⪢ e) s (lift_tm 0 t) = case_tm e s t›
  by (induct t) auto

lemma sub_tm_semantics [simp]: ‹case_tm e g (sub_tm s t) = case_tm (λn. case_tm e g (s n)) g t›
  by (induct t) (auto split: tm.splits)

lemma semantics_tm_id [simp]: ‹case_tm ❙# ❙○ t = t›
  by (induct t) auto

lemma semantics_tm_id_map [simp]: ‹map (case_tm ❙# ❙○) ts = ts›
  by (auto cong: map_cong)

lemma map_tm_sub_tm [simp]: ‹map_tm f (sub_tm g t) = sub_tm (map_tm f o g) (map_tm f t)›
  by (induct t) simp_all

lemma map_tm_lift_tm [simp]: ‹map_tm f (lift_tm m t) = lift_tm m (map_tm f t)›
  by (induct t) simp_all

lemma semantics_tm_fresh [simp]: ‹x ∉ symbols_tm t ⟹ case_tm e (g(x := a)) t = case_tm e g t›
  by (induct t) auto

lemma map_tm_inst_single: ‹(map_tm f o (u ⪢ ❙#)) t = (map_tm f u ⪢ ❙#) t›
  by (induct t) auto

subsubsection ‹Nominals›

lemma size_sub_nom [simp]: ‹sz_fm (sub_nom s p) = sz_fm p›
  by (induct p arbitrary: s) simp_all

lemma semantics_symbols_cong_nom:
  assumes ‹∀i ∈ symbols_fm p. N i = N' i›
  shows ‹(Model W R PI N e V f, w) ⊨ p ⟷ (Model W R PI N' e V f, w) ⊨ p›
  using assms by (induct p arbitrary: e f w) (simp_all split: tm.splits)

corollary semantics_symbols_other_nom [simp]:
  assumes ‹i ∉ symbols_fm p›
  shows ‹(Model W R PI (N(i := x)) e V f, w) ⊨ p ⟷ (Model W R PI N e V f, w) ⊨ p›
  using assms by (simp add: semantics_symbols_cong_nom)

lemma sub_nom_semantics [simp]:
  ‹(Model W R PI N e V f, w) ⊨ sub_nom s p ⟷ (Model W R PI N (λn. case_tm e N (s n)) V f, w) ⊨ p›
  by (induct p arbitrary: e f s w) (simp_all split: tm.splits)

lemma map_fm_sub_nom: ‹map_fm f (sub_nom s p) = sub_nom (map_tm f o s) (map_fm f p)›
  by (induct p arbitrary: s) (simp_all add: comp_def)

lemma map_fm_inst_single_nom [simp]: ‹map_fm f (⟨t⟩⇩_i p) = ⟨map_tm f t⟩⇩_i (map_fm f p)›
  unfolding map_fm_sub_nom map_tm_inst_single ..

subsubsection ‹Propositions›

lemma semantics_symbols_cong_pro:
  ‹∀P ∈ symbols_fm p. V P = V' P ⟹
  (Model W R PI N e V f, w) ⊨ p ⟷ (Model W R PI N e V' f, w) ⊨ p›
  by (induct p arbitrary: e f w) (simp_all split: tm.splits)

corollary semantics_symbols_other_pro [simp]:
  assumes ‹P ∉ symbols_fm p›
  shows ‹(Model W R PI N e (V(P := x)) f, w) ⊨ p ⟷ (Model W R PI N e V f, w) ⊨ p›
  using assms by (simp add: semantics_symbols_cong_pro)

lemma semantics_symbols_lbd_cong_pro:
  ‹∀P ∈ symbols_lbd (i, p). V P = V' P ⟹
  (Model W R PI N e V f, w) ⊨ p ⟷ (Model W R PI N e V' f, w) ⊨ p›
  by (simp add: semantics_symbols_cong_pro)

lemma map_lift_fm_pro [simp]: ‹map_fm f (lift_fm_pro m p) = lift_fm_pro m (map_fm f p)›
  by (induct p arbitrary: m) simp_all

lemma map_lift_fm_nom [simp]: ‹map_fm f (lift_fm_nom m p) = lift_fm_nom m (map_fm f p)›
  by (induct p arbitrary: m) simp_all

lemma map_fm_sub_pro: ‹map_fm f (sub_pro s p) = sub_pro (map_fm f o s) (map_fm f p)›
  by (induct p arbitrary: s) (simp_all add: comp_def split: tm.splits)

lemma map_fm_inst_single: ‹(map_fm f o (q ⪢ ❙⋅ o ❙#)) p = (map_fm f q ⪢ ❙⋅ o ❙#) p›
  by (induct p) auto

lemma map_fm_inst_single_pro [simp]: ‹map_fm f (⟨q⟩⇩_p p) = ⟨map_fm f q⟩⇩_p (map_fm f p)›
  unfolding map_fm_sub_pro map_fm_inst_single ..

subsection ‹softqdf›

lemma softqdf_map_fm [simp]: ‹softqdf (map_fm f p) ⟷ softqdf p›
  by (induct p) auto

lemma softqdf_lift_fm_nom [simp]: ‹softqdf (lift_fm_nom m q) ⟷ softqdf q›
  by (induct q arbitrary: m) auto

lemma softqdf_lift_fm_pro [simp]: ‹softqdf (lift_fm_pro m q) ⟷ softqdf q›
  by (induct q) auto

subsection ‹Add env›

lemma range_add_env:
  assumes ‹range f ⊆ A› ‹a ∈ A›
  shows ‹range (a ⪢ f) ⊆ A›
proof safe
  fix x n
  show ‹(a ⪢ f) n ∈ A›
    using assms by (induct n) auto
qed

lemma softqdf_add_env: ‹softqdf q ⟹ softqdf_sub (q ⪢ ❙⋅ o ❙#)›
  by (metis add_env.simps comp_apply not0_implies_Suc softqdf.simps(2))

lemma wf_env_add_nom: ‹wf_env (Model W R PI N e V f) ⟹ w ∈ W ⟹
    wf_env (⦇𝒲 = W, ℛ = R, Π = PI, 𝒩 = N, 𝔑 = w ⪢ e, 𝒱 = V, 𝔙 = f⦈)›
  unfolding wf_env_def unfolds using range_add_env by meson
  
lemma wf_model_add_nom: ‹wf_model (Model W R PI N e V f) ⟹ w ∈ W ⟹
    wf_model (⦇𝒲 = W, ℛ = R, Π = PI, 𝒩 = N, 𝔑 = w ⪢ e, 𝒱 = V, 𝔙 = f⦈)›
  using wf_env_add_nom unfolding wf_model_def wf_env_def wf_frame_def wf_gframe_def admissible_def unfolds by meson

lemma wf_env_add_pro: ‹wf_env (Model W R PI N e V f) ⟹ P ∈ PI ⟹
    wf_env (⦇𝒲 = W, ℛ = R, Π = PI, 𝒩 = N, 𝔑 = e, 𝒱 = V, 𝔙 = P ⪢ f⦈)›
  unfolding wf_env_def unfolds using range_add_env by meson

lemma wf_model_add_pro:
  ‹wf_model (Model W R PI N e V f) ⟹ P ∈ PI ⟹ wf_model (Model W R PI N e V (P ⪢ f))›
  using wf_env_add_pro unfolding wf_model_def wf_env_def wf_frame_def wf_gframe_def admissible_def unfolds by meson

lemma softqdf_lift_fm_nom_add_env [simp]:
  ‹softqdf p ⟹ (Model W R PI N (v ⪢ e) V f, w) ⊨ lift_fm_nom 0 p ⟷ (Model W R PI N e V f, w) ⊨ p›
  by (induct p arbitrary: e w) (simp_all split: tm.splits)

lemma softqdf_lift_fm_pro_add_env [simp]:
  ‹softqdf p ⟹ (Model W R PI N e V (P ⪢ f), w) ⊨ lift_fm_pro 0 p ⟷ (Model W R PI N e V f, w) ⊨ p›
  by (induct p arbitrary: e w) (simp_all split: tm.splits)

subsection ‹Sizes›

lemma qs_fm_sub_nom [simp]: ‹qs_fm (sub_nom s p) = qs_fm p›
  by (induct p arbitrary: s) auto

lemma softqdf_qs_fm [simp]: ‹softqdf q ⟹ qs_fm q = 0›
  by (induct q) simp_all

lemma softqdf_sub_pro: ‹softqdf_sub s ⟹ softqdf_sub (❙⋅(❙#0) ⪢ λn. lift_fm_pro 0 (s n))›
  by (metis add_env.simps not0_implies_Suc softqdf.simps(2) softqdf_lift_fm_pro)

lemma qs_fm_sub_pro [simp]: ‹softqdf_sub s ⟹ qs_fm (sub_pro s p) = qs_fm p›
proof (induct p arbitrary: s)
  case (All p)
  then show ?case
    using softqdf_sub_pro by force
qed (auto split: tm.splits)

section ‹Propositional Quantification›

definition worlds :: ‹('x, 'w) model ⇒ 'x fm ⇒ 'w set› where
  ‹worlds M p ≡ { w ∈ 𝒲 M. (M, w) ⊨ p }›

lemma worlds_op [simp]:
  assumes ‹wf_model M›
  shows
    ‹worlds M (❙¬ p) = 𝒲 M - worlds M p›
    ‹worlds M (p ❙∧ q) = worlds M p ∩ worlds M q›
    ‹worlds M (❙□ p) = {w ∈ 𝒲 M. ∀v ∈ ℛ M w. v ∈ worlds M p}›
  using assms unfolding worlds_def wf_model_def wf_frame_def wf_gframe_def unfolds by auto

lemma softqdf_worlds:
  assumes ‹wf_model M› ‹softqdf p›
  shows ‹worlds M p ∈ Π M›
  using assms
proof (induct p)
  case (TmI x)
  then show ?case
    by simp
next
  case (TmP x)
  then have ‹𝒱 M P ∈ Π M› ‹𝔙 M n ∈ Π M› for P n
    using wf_𝒱 wf_𝔙 by fastforce+
  moreover have ‹𝒲 M ∈ Π M›
    using TmP wf_univ by fastforce
  ultimately have ‹𝒱 M P ∩ 𝒲 M ∈ Π M› ‹𝔙 M n ∩ 𝒲 M ∈ Π M› for P n
    using TmP wf_inter by fastforce+
  then have ‹{w ∈ 𝒲 M. w ∈ 𝒱 M P} ∈ Π M› ‹{w ∈ 𝒲 M. w ∈ 𝔙 M n} ∈ Π M› for P n
    by (metis Int_def inf_commute)+
  then show ?case
    unfolding worlds_def
    by (auto split: tm.splits)
next
  case (Neg p)
  then show ?case
    by (simp add: wf_compl)
next
  case (Con p q)
  then show ?case
    by (simp add: wf_inter)
next
  case (Box p)
  then show ?case
    by (simp add: wf_modal)
next
  case (Sat k p)
  then have ‹(∀w. (M, w) ⊨ ❙@k p) ∨ (∄w. (M, w) ⊨ ❙@k p)›
    by (auto split: tm.splits)
  then have ‹worlds M (❙@k p) = {} ∨ worlds M (❙@k p) = 𝒲 M›
    unfolding worlds_def by blast
  then show ?case
    using Sat(2) wf_univ wf_empty by fastforce
next
  case (Glo p)
  then have ‹(∀w. (M, w) ⊨ ❙A p) ∨ (∄w. (M, w) ⊨ ❙A p)›
    by auto
  then have ‹worlds M (❙A p) = {} ∨ worlds M (❙A p) = 𝒲 M›
    unfolding worlds_def by blast
  then show ?case
    using Glo(2) wf_univ wf_empty by fastforce
next
  case (Dwn p)
  then show ?case
    by simp
next
  case (All p)
  then show ?case
    by simp
qed

definition sqdfs :: ‹('x, 'w) model ⇒ 'w set set› where
  ‹sqdfs M ≡ { worlds M p |p. softqdf p }›

lemma sqdfs:
  assumes ‹wf_model M›
  shows ‹sqdfs M ⊆ Π M›
  unfolding sqdfs_def using assms softqdf_worlds by blast

lemma sqdfs_admissible:
  assumes ‹wf_model M›
  shows ‹admissible (frame.truncate M) (sqdfs M)›
  unfolding admissible_def
proof safe
  fix X
  assume ‹X ∈ sqdfs M›
  then obtain p where ‹X = worlds M p› ‹softqdf p›
    unfolding sqdfs_def by fast
  moreover from this have ‹worlds M (❙¬ p) ∈ sqdfs M›
    unfolding sqdfs_def by auto
  ultimately show ‹𝒲 (frame.truncate M) - X ∈ sqdfs M›
    unfolding sqdfs_def unfolds using assms by simp
next
  fix X Y
  assume ‹X ∈ sqdfs M› ‹Y ∈ sqdfs M›
  then obtain p q where ‹X = worlds M p› ‹softqdf p› ‹Y = worlds M q› ‹softqdf q›
    unfolding sqdfs_def by fast
  moreover from this have ‹worlds M (p ❙∧ q) ∈ sqdfs M›
    unfolding sqdfs_def by auto
  ultimately show ‹X ∩ Y ∈ sqdfs M›
    unfolding sqdfs_def using assms by simp
next
  fix X
  assume ‹X ∈ sqdfs M›
  then obtain p where ‹X = worlds M p› ‹softqdf p›
    unfolding sqdfs_def by fast
  moreover from this have ‹worlds M (❙□ p) ∈ sqdfs M›
    unfolding sqdfs_def by auto
  ultimately show ‹{w ∈ 𝒲 (frame.truncate M). ∀v ∈ ℛ (frame.truncate M) w. v ∈ X} ∈ sqdfs M›
    unfolding sqdfs_def unfolds using assms by simp
qed

definition with_worlds :: ‹('x, 'w) model ⇒ (nat ⇒ 'x fm)  ⇒ ('x, 'w) model› where
  ‹with_worlds M s ≡ M⦇𝔙 := worlds M o s⦈›

lemma sub_pro_with_worlds:
  assumes ‹wf_model (Model W R PI N e V f)› ‹w ∈ W› ‹softqdf_sub s›
  shows ‹(Model W R PI N e V f, w) ⊨ sub_pro s p ⟷ (with_worlds (Model W R PI N e V f) s, w) ⊨ p›
  using assms
proof (induct p arbitrary: s e f w)
  case (Box p)
  moreover from this have ‹v ∈ R w ⟹ v ∈ W› for v
    unfolding wf_model_def wf_gframe_def wf_frame_def unfolds by auto
  ultimately show ?case
    unfolding with_worlds_def by simp
next
  case (Sat x p)
  moreover from this have ‹case_tm e N x ∈ W›
    unfolding wf_model_def wf_env_def
    by (auto split: tm.splits)
  ultimately show ?case
    unfolding with_worlds_def
    by (simp split: tm.splits)
next
  case (Dwn p)
  let ?s = ‹lift_fm_nom 0 o s›

  have ‹wf_model (Model W R PI N (w ⪢ e) V f)›
    using Dwn by (simp add: wf_model_add_nom)
  moreover have ‹softqdf_sub ?s›
    using Dwn by simp
  ultimately have ‹(Model W R PI N (w ⪢ e) V f, w) ⊨ sub_pro ?s p ⟷
      (with_worlds (Model W R PI N (w ⪢ e) V f) ?s, w) ⊨ p›
    using Dwn by fastforce
  moreover have ‹worlds (Model W R PI N (w ⪢ e) V f) o ?s = worlds (Model W R PI N e V f) o s›
    unfolding worlds_def comp_def using Dwn(4) by simp
  ultimately have *: ‹(Model W R PI N (w ⪢ e) V f, w) ⊨ sub_pro ?s p ⟷
      (Model W R PI N (w ⪢ e) V (worlds (Model W R PI N e V f) ∘ s), w) ⊨ p›
    unfolding with_worlds_def by simp

  moreover have ‹(with_worlds (Model W R PI N e V f) ?s, w) ⊨ ❙↓ p ⟷
      (Model W R PI N (w ⪢ e) V (worlds (Model W R PI N e V f) o ?s), w) ⊨ p›
    unfolding with_worlds_def by simp
  then have ** :‹(with_worlds (Model W R PI N e V f) ?s, w) ⊨ ❙↓ p ⟷
      (Model W R PI N (w ⪢ e) V (worlds (Model W R PI N e V f) o ?s), w) ⊨ p›
    by metis

  ultimately show ?case
    unfolding with_worlds_def by simp
next
  case (All p)
  let ?s = ‹❙⋅(❙#0) ⪢ λn. lift_fm_pro 0 (s n)›

  have ‹softqdf (?s n)›  for n
    using All(4) by (induct n) auto
  then have ‹softqdf_sub ?s›
    by blast
  moreover have ‹∀P ∈ PI. wf_model (Model W R PI N e V (P ⪢ f))›
    using All(2) wf_model_add_pro by blast
  ultimately have ‹(∀P ∈ PI. (Model W R PI N e V (P ⪢ f), w) ⊨ sub_pro ?s p) ⟷
    (∀P ∈ PI. (with_worlds (Model W R PI N e V (P ⪢ f)) ?s, w) ⊨ p)›
    using All by blast

  moreover have ‹∀P ∈ PI. P ⊆ W›
    using All(2) unfolding wf_model_def wf_gframe_def unfolds by blast
  then have ‹P ∈ PI ⟹
    (worlds (Model W R PI N e V (P ⪢ f)) o ?s) n = (P ⪢ worlds (Model W R PI N e V f) o s) n› for P n
    unfolding worlds_def using All(4) by (induct n) auto
  then have ‹P ∈ PI ⟹
      (worlds (Model W R PI N e V (P ⪢ f)) o ?s) = (P ⪢ worlds (Model W R PI N e V f) o s)› for P
    by blast

  ultimately show ?case
    unfolding with_worlds_def by simp
qed (simp_all add: worlds_def with_worlds_def split: tm.splits)

lemma worlds_id_sub:
 assumes ‹wf_model (Model W R PI N e V f)›
 shows ‹worlds (Model W R PI N e V f) (❙⋅ (❙# n)) = f n›
  using wf_𝔙'[OF assms] unfolding worlds_def unfolds by auto

lemma worlds_inst_single_pro:
  assumes ‹wf_model (Model W R PI N e V f)›
  shows ‹worlds (Model W R PI N e V f) o (q ⪢ ❙⋅ o ❙#) = (worlds (Model W R PI N e V f) q ⪢ f)›
  unfolding comp_def env worlds_id_sub[OF assms] ..

corollary inst_single_worlds:
  assumes ‹wf_model (Model W R PI N e V f)› ‹w ∈ W› ‹softqdf q›
  shows
    ‹(Model W R PI N e V f, w) ⊨ ⟨q⟩⇩_p p ⟷
     (Model W R PI N e V (worlds (Model W R PI N e V f) q ⪢ f), w) ⊨ p›
proof -
  have
    ‹(Model W R PI N e V f, w) ⊨ ⟨q⟩⇩_p p ⟷
     (Model W R PI N e V (worlds (Model W R PI N e V f) o (q ⪢ ❙⋅ o ❙#)), w) ⊨ p›
    using sub_pro_with_worlds[OF assms(1-2)] assms(3) unfolding with_worlds_def
    by (metis model.update_convs(4) softqdf_add_env)
  then show ?thesis
    using assms worlds_inst_single_pro by metis
qed

section ‹Model Existence›

inductive confl_class :: ‹'x lbd list ⇒ 'x lbd list ⇒ bool› (infix ‹↝⇩_✗› 50) where
  CNegP: ‹[ (i, ❙¬ ❙⋅P) ] ↝⇩_✗ [(i, ❙⋅P)]›
| CNegI: ‹[ (i, ❙¬ ❙∙k) ] ↝⇩_✗ [(i, ❙∙k)]›

inductive alpha_class :: ‹'x lbd list ⇒ 'x lbd list ⇒ bool› (infix ‹↝⇩_α› 50) where
  CSym: ‹[ (i, ❙∙k) ] ↝⇩_α [(k, ❙∙i)]›
| CNom: ‹[ (i, ❙∙k), (i, p) ] ↝⇩_α [(k, p)]›
| CNegN: ‹[ (i, ❙¬ ❙¬ p) ] ↝⇩_α [(i, p)]›
| CConP: ‹[ (i, p ❙∧ q) ] ↝⇩_α [(i, p), (i, q)]›
| CSatP: ‹[ (i, ❙@k p) ] ↝⇩_α [(k, p)]›
| CSatN: ‹[ (i, ❙¬ ❙@k p) ] ↝⇩_α [(k, ❙¬ p)]›
| CBoxP: ‹[ (i, ❙□p), (i, ❙◇(❙∙k)) ] ↝⇩_α [(k, p)]›
| CDwnP: ‹[ (i, ❙↓ p) ] ↝⇩_α [ (i, ⟨i⟩⇩_i p) ]›
| CDwnN: ‹[ (i, ❙¬ ❙↓ p) ] ↝⇩_α [ (i, ❙¬ ⟨i⟩⇩_i p) ]›

inductive beta_class :: ‹'x lbd list ⇒ 'x lbd list ⇒ bool› (infix ‹↝⇩_β› 50) where
  CConN: ‹[ (i, ❙¬ (p ❙∧ q)) ] ↝⇩_β [(i, ❙¬ p), (i, ❙¬ q)]›

inductive gamma_class_nom :: ‹'x lbd list ⇒ ('x tm ⇒ _) ⇒ bool› (infix ‹↝⇩_γ⇩_i› 50) where
  CRefl: ‹[] ↝⇩_γ⇩_i (λi. [ (i, ❙∙i) ])›
| CGloP: ‹[ (i, ❙A p) ] ↝⇩_γ⇩_i (λk. [ (k, p) ])›
  
inductive gamma_class_fm :: ‹'x lbd list ⇒ ('x lbd set ⇒ 'x fm set) × ('x fm ⇒ _) ⇒ bool› (infix ‹↝⇩_γ⇩_p› 50) where
  CAllP: ‹[ (i, ❙∀ p) ] ↝⇩_γ⇩_p (λ_. {q. softqdf q}, λq. [ (i, ⟨q⟩⇩_p p) ])›

fun δ :: ‹'x lbd ⇒ 'x ⇒ 'x lbd list› where
  CBoxN: ‹δ (i, ❙¬ ❙□p) k = [(❙○k, ❙¬ p), (i, ❙◇ (❙∙ (❙○ k)))]›
| CGloN: ‹δ (i, ❙¬ ❙A p) k = [ (❙○k, ❙¬ p) ]›
| CAllN: ‹δ (i, ❙¬ ❙∀ p) P = [ (i, ❙¬ ⟨❙⋅(❙○P)⟩⇩_p p) ]›
| ‹δ _ _ = []›

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

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

interpretation A: Alpha map_lbd symbols_lbd ‹λ_. 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_lbd symbols_lbd ‹λ_. True› beta_class
  by unfold_locales (auto simp: fm.map_id0 cong: fm.map_cong0 elim!: beta_class.cases intro: beta_class.intros)

interpretation GI: Gamma_UNIV map_tm map_lbd symbols_lbd ‹λ_. True› gamma_class_nom
  by unfold_locales (fastforce elim: gamma_class_nom.cases intro: gamma_class_nom.intros)+

interpretation GP: Gamma map_fm map_lbd symbols_lbd ‹λ_. True› gamma_class_fm
  by unfold_locales (fastforce elim: gamma_class_fm.cases intro: gamma_class_fm.intros)+

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

abbreviation Kinds :: ‹('x, 'x lbd) kind list› where
  ‹Kinds ≡ [C.kind, A.kind, B.kind, GI.kind, GP.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 GI.kind C› ‹P.sat⇩_E GP.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_lbd symbols_lbd ‹λ_. True› Kinds
  using P.Params_axioms C.Consistency_Kind_axioms A.Consistency_Kind_axioms B.Consistency_Kind_axioms
    GI.Consistency_Kind_axioms GP.Consistency_Kind_axioms D.Consistency_Kind_axioms
  by (auto intro: Consistency_Kinds.intro simp: Consistency_Kinds_axioms_def)

interpretation Maximal_Consistency map_lbd symbols_lbd ‹λ_. True› Kinds
proof
 have ‹infinite (UNIV :: 'x fm set)›
    using infinite_UNIV_size[of ‹λp. p ❙⟶ p›] by simp
  then show ‹infinite (UNIV :: 'x lbd set)›
    using finite_prod by blast
qed simp

context begin

lemma ‹P.prop⇩_E Kinds C ⟹ S ∈ C ⟹ (i, ❙⋅P) ∉ S ∨ (i, ❙¬ ❙⋅P) ∉ S›
  using sat⇩_E[of C.kind] by (force intro: CNegP)

lemma ‹P.prop⇩_E Kinds C ⟹ S ∈ C ⟹ (i, p ❙∧ q) ∈ S ⟹ {(i, p), (i, q)} ∪ S ∈ C›
  using sat⇩_E[of A.kind] by (force intro: CConP)

lemma ‹P.prop⇩_E Kinds C ⟹ S ∈ C ⟹ (i, ❙¬ (p ❙∧ q)) ∈ S ⟹ {(i, ❙¬ p)} ∪ S ∈ C ∨ {(i, ❙¬ q)} ∪ S ∈ C›
  using sat⇩_E[of B.kind] by (force intro: CConN)
  
lemma ‹P.prop⇩_E Kinds C ⟹ S ∈ C ⟹ (i, ❙□ p) ∈ S ⟹ (i, ❙◇(❙∙k)) ∈ S ⟹ {(k, p)} ∪ S ∈ C›
  using sat⇩_E[of A.kind] by (force intro: CBoxP)

lemma ‹P.prop⇩_E Kinds C ⟹ S ∈ C ⟹ (i, ❙¬ ❙□p) ∈ S ⟹ ∃k. {(k, ❙¬ p), (i, ❙◇ (❙∙k))} ∪ S ∈ C›
  using sat⇩_E[of D.kind] by fastforce
  
lemma ‹P.prop⇩_E Kinds C ⟹ S ∈ C ⟹ { (i, ❙∙i) } ∪ S ∈ C›
  using sat⇩_E[of GI.kind] by (force intro: CRefl)

lemma ‹P.prop⇩_E Kinds C ⟹ S ∈ C ⟹ (i, ❙A p) ∈ S ⟹ { (k, p) } ∪ S ∈ C›
  using sat⇩_E[of GI.kind] by (force intro: CGloP)
 
lemma ‹P.prop⇩_E Kinds C ⟹ S ∈ C ⟹ (i, ❙¬ ❙A p) ∈ S ⟹ ∃k. { (k, ❙¬ p) } ∪ S ∈ C›
  using sat⇩_E[of D.kind] by fastforce

lemma ‹P.prop⇩_E Kinds C ⟹ S ∈ C ⟹ (i, ❙∀ p) ∈ S ⟹ softqdf q ⟹ { (i, ⟨q⟩⇩_p p) } ∪ S ∈ C›
  using sat⇩_E[of GP.kind] by (force intro: CAllP)

lemma ‹P.prop⇩_E Kinds C ⟹ S ∈ C ⟹ (i, ❙¬ ❙∀ p) ∈ S ⟹ ∃P. { (i, ❙¬ ⟨❙⋅(❙○P)⟩⇩_p p) } ∪ S ∈ C›
  using sat⇩_E[of D.kind] by fastforce

end

definition equiv_nom :: ‹'x lbd set ⇒ 'x tm ⇒ 'x tm ⇒ bool› where
  ‹equiv_nom S i k ≡ (i, ❙∙k) ∈ S›

definition assign :: ‹'x tm ⇒ 'x lbd set ⇒ 'x tm› (‹[_]⇩_› [0, 100] 100) where
  ‹[i]⇩S ≡ wo_rel.minim ( |UNIV| ) {k. equiv_nom S i k}›

definition reach :: ‹'x lbd set ⇒ 'x tm ⇒ 'x tm set› where
  ‹reach S i ≡ {[k]⇩S |k. (i, ❙◇ (❙∙k)) ∈ S}›

definition val :: ‹'x lbd set ⇒ 'x tm ⇒ 'x tm set› where
  ‹val S P ≡ {[i]⇩S |i. (i, ❙⋅P) ∈ S}›

lemma range_val_ne: ‹range (val S) ≠ {}›
  unfolding val_def by blast

lemma admissible_Pow: ‹admissible F (Pow (𝒲 F))›
  unfolding admissible_def by blast

definition admits :: ‹'w frame ⇒ 'w set set ⇒ 'w set set ⇒ bool› where
  ‹admits F B PI ≡ PI ≠ {} ∧ PI ⊆ Pow (𝒲 F) ∧ B ⊆ PI ∧ admissible F PI›

definition adm_δ :: ‹'w frame ⇒ 'w set set ⇒ 'w set set› where
  ‹adm_δ M PI ≡
    { 𝒲 M - X | X. X ∈ PI } ∪
    { X ∩ Y | X Y. X ∈ PI ∧ Y ∈ PI } ∪
    { {w ∈ 𝒲 M. ∀v ∈ ℛ M w. v ∈ X} | X. X ∈ PI }›

abbreviation ‹grow F B ≡ λPI. B ∪ PI ∪ adm_δ F (B ∪ PI)›

definition admit :: ‹'w frame ⇒ 'w set set ⇒ 'w set set› where
  ‹admit F B ≡ lfp (grow F B)›

lemma mono_grow: ‹mono (grow F B)›
  unfolding adm_δ_def mono_def by (auto simp: subset_eq)

lemma admissible_δ: ‹admissible F B ⟷ adm_δ F B ⊆ B›
  unfolding admissible_def adm_δ_def by auto

lemma admit_B: ‹B ⊆ admit F B›
  unfolding admit_def by (meson le_sup_iff lfp_greatest)

lemma admit_Pow: ‹B ⊆ Pow (𝒲 F) ⟹ admit F B ⊆ Pow (𝒲 F)›
  unfolding admit_def using admissible_Pow admissible_δ lfp_lowerbound 
  by (metis (no_types, lifting) order_class.order_eq_iff subset_Un_eq sup.absorb_iff1)

lemma admissible_grow: ‹admissible F B ⟷ grow F B B = B›
  using admissible_δ by auto

lemma lfp_grow: ‹grow F B (lfp (grow F B)) = lfp (grow F B)›
  using lfp_unfold mono_grow by blast

lemma admit_admissible: ‹admissible F (admit F B)›
  unfolding admit_def
proof -
  have "B ∪ lfp (grow F B) = lfp (grow F B)"
    using lfp_grow by blast
  then show "admissible F (lfp (grow F B))"
    using lfp_grow[of B F] by (simp add: admissible_δ sup.order_iff)
qed

lemma admits_admit: ‹B ≠ {} ⟹ B ⊆ Pow (𝒲 F) ⟹ admits F B (admit F B)›
  by (metis admit_B admit_Pow admit_admissible admits_def subset_empty)

lemma admissible_admit:
  assumes ‹B ≠ {}› ‹B ⊆ Pow (𝒲 F)›
  shows
    ‹admit F B ≠ {}›
    ‹admit F B ⊆ Pow (𝒲 F)›
    ‹admissible F (admit F B)›
  using assms admits_admit unfolding admits_def by metis+

abbreviation canonical_frame :: ‹'x lbd set ⇒ ('x tm) frame› where
  ‹canonical_frame S ≡ ⦇ 𝒲 = {[k]⇩S | k. True}, ℛ = reach S ⦈›

abbreviation canonical_gframe :: ‹'x lbd set ⇒ ('x tm) gframe› where
  ‹canonical_gframe S ≡ frame.extend (canonical_frame S)
    ⦇ Π = admit (canonical_frame S) (range (val S)) ⦈›

definition canonical :: ‹'x lbd set ⇒ ('x, 'x tm) model› where
  ‹canonical S ≡
    gframe.extend (canonical_gframe S)
     ⦇ 𝒩 = λi. [❙○i]⇩S,
       𝔑 = λi. [❙#i]⇩S,
       𝒱 = val S o ❙○,
       𝔙 = val S o ❙#
     ⦈›

lemma wf_canonical_frame: ‹wf_frame (canonical_frame S)›
  unfolding wf_frame_def unfolds reach_def by auto

lemma val_Pow: ‹range (val S) ⊆ Pow (𝒲 (canonical_frame S))›
  unfolding val_def by auto

lemma wf_cannonical_gframe: ‹wf_gframe (canonical_gframe S)›
  unfolding wf_gframe_def unfolds using wf_canonical_frame admissible_admit(2) admit_B admit_admissible
  by (metis (mono_tags, lifting) frame.select_convs(1) range_val_ne subset_empty val_Pow)

lemma admits_val: ‹admits (canonical_frame S) (range (val S)) PI ⟹ val S P ∈ PI›
  unfolding admits_def by blast 

lemma admit_val: ‹val S P ∈ admit (canonical_frame S) (range (val S))›
  using admits_val admits_admit val_Pow by (simp add: admit_B range_subsetD)
 
lemma wf_canonical_env: ‹wf_env (canonical S)›
  unfolding wf_env_def canonical_def unfolds using admit_val by auto

lemma wf_gframe_canonical: ‹wf_gframe (gframe.truncate (canonical S))›
  using wf_cannonical_gframe unfolding canonical_def unfolds .
 
lemma wf_canonical: ‹wf_model (canonical S)›
  unfolding wf_model_def using wf_gframe_canonical wf_canonical_env by blast  

lemma admissible_sqdfs: ‹admissible (canonical_frame S) (sqdfs (canonical S))›
  using sqdfs_admissible[OF wf_canonical[of S]]
  unfolding canonical_def unfolds .

lemma sqdfs_Pow: ‹sqdfs (canonical S) ⊆ Pow (𝒲 (canonical_frame S))›
  unfolding sqdfs_def canonical_def unfolds worlds_def by blast

lemma val_sqdfs: ‹val S P ∈ sqdfs (canonical S)›
  unfolding val_def sqdfs_def canonical_def unfolds worlds_def
  by (auto split: tm.splits intro!: exI[of _ ‹❙⋅ P›])

lemma admits_canonical_sqdfs: ‹admits (canonical_frame S) (range (val S)) (sqdfs (canonical S))›
  unfolding admits_def using admissible_sqdfs sqdfs_Pow val_sqdfs by blast

definition canonical_ctx :: ‹'x lbd set ⇒ 'x tm ⇒ ('x, 'x tm) ctx› (‹⟦_, _⟧›) where
  ‹⟦S, i⟧ ≡ (canonical S, [i]⇩S)›

lemma sqdfs_canonical: ‹sqdfs (canonical S) = Π (canonical S)›
proof
  show ‹sqdfs (canonical S) ⊆ Π (canonical S)›
    using sqdfs wf_canonical by blast
next
  have ‹grow (canonical_frame S) (range (val S)) (sqdfs (canonical S)) ⊆ sqdfs (canonical S)›
    using admissible_grow[of ‹canonical_frame S› ‹sqdfs _›] admits_canonical_sqdfs[of S] unfolding admits_def 
    by (metis (no_types, lifting) equalityE le_iff_sup)
  then have ‹admit (canonical_frame S) (range (val S)) ⊆ sqdfs (canonical S)›
    by (simp add: admit_def lfp_lowerbound)
  then show ‹Π (canonical S) ⊆ sqdfs (canonical S)›
    unfolding canonical_def unfolds .
qed

lemma canonical_tm_eta [simp]: ‹case_tm (λi. [❙# i]⇩S) (λn. [❙○ n]⇩S) k = [k]⇩S›
  by (cases k) simp_all

corollary canonical_tm_eta' [simp]: ‹case_tm (𝔑 (canonical S)) (𝒩 (canonical S)) k = [k]⇩S›
  unfolding canonical_def unfolds by simp

locale MyHintikka = Hintikka map_lbd symbols_lbd ‹λ_. True› Kinds S
  for S :: ‹'x lbd set›
begin

lemmas
  confl = sat⇩_H[of C.kind] and
  alpha = sat⇩_H[of A.kind] and
  beta = sat⇩_H[of B.kind] and
  gammaI = sat⇩_H[of GI.kind] and
  gammaP = sat⇩_H[of GP.kind] and
  δ = sat⇩_H[of D.kind]

lemma Nom_refl: ‹(i, ❙∙i) ∈ S›
  using gammaI by (fastforce intro: CRefl)

lemma Nom_sym:
  assumes ‹(i, ❙∙k) ∈ S›
  shows ‹(k, ❙∙i) ∈ S›
  using assms alpha by (fastforce intro: CSym)

lemma Nom_trans:
  assumes ‹(i, ❙∙j) ∈ S› ‹(j, ❙∙k) ∈ S›
  shows ‹(i, ❙∙k) ∈ S›
  using assms 
proof -
  have ‹(j, ❙∙i) ∈ S›
    using assms Nom_sym by blast
  then show ?thesis
    using assms(2) alpha by (fastforce intro: CNom)
qed

lemma equiv_nom_ne: ‹{k. equiv_nom S i k} ≠ {}›
  unfolding equiv_nom_def using Nom_refl by blast

lemma equiv_nom_assign: ‹equiv_nom S i ([i]⇩S)›
  unfolding assign_def using equiv_nom_ne 
  by (metis Field_card_of card_of_well_order_on mem_Collect_eq top.extremum wo_rel_def wo_rel.minim_in)

lemma equiv_nom_Nom:
  assumes ‹equiv_nom S i k› ‹(i, p) ∈ S›
  shows ‹(k, p) ∈ S›
proof -
  have ‹(i, ❙∙k) ∈ S›
    using assms unfolding equiv_nom_def by blast
  then show ?thesis
    using assms alpha by (fastforce intro: CNom)
qed

lemma assign_in_W: ‹[i]⇩S ∈ 𝒲 (canonical S)›
  unfolding canonical_def gframe.defs frame.defs unfolds by blast

theorem model: ‹((i, p) ∈ S ⟶ ⟦S, i⟧ ⊨ p) ∧ ((i, ❙¬ p) ∈ S ⟶ ¬ ⟦S, i⟧ ⊨ p)›
proof (induct p arbitrary: i rule: wf_induct[where r=‹measures [qs_fm, sz_fm]›])
  case 1
  then show ?case
    by simp
next
  case (2 x)
  then show ?case
  proof (cases x)
    case (TmI k)
    then show ?thesis
    proof (safe del: notI)
      assume ‹x = ❙∙k› ‹(i, ❙∙k) ∈ S›
      moreover from this have ‹(k, ❙∙i) ∈ S›
        using Nom_sym by fast
      ultimately have ‹[i]⇩S = [k]⇩S›
        using Nom_trans unfolding assign_def equiv_nom_def by metis
      then show ‹⟦S, i⟧ ⊨ ❙∙k›
        unfolding canonical_ctx_def canonical_def gframe.defs
        by (simp split: tm.splits)
    next
      assume ‹x = ❙∙k› ‹(i, ❙¬ ❙∙k) ∈ S›
      then have ‹(i, ❙∙k) ∉ S›
        using confl by (fastforce intro: CNegI)
      then have ‹¬ equiv_nom S i k›
        unfolding equiv_nom_def by blast
      moreover have ‹(i, ❙∙k) ∉ S›
        using ‹(i, ❙¬ ❙∙k) ∈ S› using confl by (fastforce intro: CNegI)
      ultimately have ‹[i]⇩S ≠ [k]⇩S›
        using Nom_sym Nom_trans equiv_nom_assign unfolding equiv_nom_def by metis
      then show ‹¬ ⟦S, i⟧ ⊨ ❙∙k›
        unfolding canonical_ctx_def canonical_def gframe.defs
        by (auto split: tm.splits)
    qed
  next
    case (TmP P)
    then show ?thesis
    proof (safe del: notI)
      assume ‹x = ❙⋅P› ‹(i, ❙⋅P) ∈ S›
      then show ‹⟦S, i⟧ ⊨ ❙⋅P›
        unfolding canonical_ctx_def canonical_def val_def gframe.defs
        by (auto split: tm.splits)
    next
      assume ‹x = ❙⋅P› ‹(i, ❙¬ ❙⋅P) ∈ S›
      then have ‹(i, ❙⋅P) ∉ S›
        using confl by (fastforce intro: CNegP)
      then have ‹⋀k. [k]⇩S = [i]⇩S ⟹ (k, ❙⋅P) ∉ S›
        by (metis Nom_refl equiv_nom_Nom equiv_nom_assign equiv_nom_def)
      then show ‹¬ ⟦S, i⟧ ⊨ ❙⋅P›
        unfolding canonical_ctx_def canonical_def val_def gframe.defs
        by (auto split: tm.splits)
    qed
  next
    case (Neg p)
    then show ?thesis
    proof (safe del: notI)
      assume ‹x = ❙¬ p› ‹(i, ❙¬ p) ∈ S›
      then show ‹⟦S, i⟧ ⊨ ❙¬ p›
        using 2 unfolding canonical_ctx_def by simp
    next
      assume ‹x = ❙¬ p› ‹(i, ❙¬ ❙¬ p) ∈ S›
      then have ‹(i, p) ∈ S›
        using alpha by (fastforce intro: CNegN)
      then show ‹¬ ⟦S, i⟧ ⊨ ❙¬ p›
        using 2 Neg unfolding canonical_ctx_def by auto
    qed
  next
    case (Con p q)
    then show ?thesis
    proof (safe del: notI)
      assume ‹x = (p ❙∧ q)› ‹(i, p ❙∧ q) ∈ S›
      then have ‹(i, p) ∈ S ∧ (i, q) ∈ S›
        using alpha by (fastforce intro: CConP)
      moreover have
        ‹(p, x) ∈ measures [qs_fm, sz_fm]›
        ‹(q, x) ∈ measures [qs_fm, sz_fm]›
        using Con by auto
      ultimately show ‹⟦S, i⟧ ⊨ (p ❙∧ q)›
        using 2 unfolding canonical_ctx_def by auto
    next
      assume ‹x = (p ❙∧ q)› ‹(i, ❙¬ (p ❙∧ q)) ∈ S›
      then have ‹(i, ❙¬ p) ∈ S ∨ (i, ❙¬ q) ∈ S›
        using beta by (fastforce intro: CConN)
      moreover have
        ‹(❙¬ p, ❙¬ x) ∈ measures [qs_fm, sz_fm]›
        ‹(❙¬ q, ❙¬ x) ∈ measures [qs_fm, sz_fm]›
        using Con by auto
      ultimately show ‹¬ ⟦S, i⟧ ⊨ (p ❙∧ q)›
        using 2 unfolding canonical_ctx_def by auto
    qed
  next
    case (Box p)
    then show ?thesis
    proof (safe del: notI)
      assume ‹x = ❙□ p› ‹(i, ❙□ p) ∈ S›
      {
        fix k
        assume ‹[k]⇩S ∈ reach S ([i]⇩S)›
        then obtain k' where ‹([i]⇩S, ❙◇ (❙∙k')) ∈ S› ‹[k']⇩S = [k]⇩S›
          unfolding reach_def by auto
        then have ‹(i, ❙◇ (❙∙k')) ∈ S›
          using Nom_sym equiv_nom_Nom equiv_nom_assign equiv_nom_def by blast
        then have ‹(k', p) ∈ S›
          using ‹(i, ❙□ p) ∈ S› alpha by (fastforce intro: CBoxP)
        then have ‹⟦S, k'⟧ ⊨ p›
          using 2 Box by simp
        then have ‹⟦S, k⟧ ⊨ p›
          unfolding canonical_ctx_def canonical_def using ‹[k']⇩S = [k]⇩S› by simp
      }
      then show ‹⟦S, i⟧ ⊨ ❙□ p›
        unfolding canonical_ctx_def canonical_def reach_def gframe.defs frame.defs
        by auto
    next
      assume ‹x = ❙□ p› ‹(i, ❙¬ (❙□ p)) ∈ S›
      then obtain k where k: ‹(k, ❙¬ p) ∈ S› ‹(i, ❙◇ (❙∙ k)) ∈ S›
        using δ by force
      then have ‹¬ ⟦S, k⟧ ⊨ p›
        using 2 Box by simp
      moreover have ‹([i]⇩S, ❙◇ (❙∙k)) ∈ S›
        using k(2) equiv_nom_Nom equiv_nom_assign by fastforce
      then have ‹[k]⇩S ∈ reach S ([i]⇩S)›
        unfolding reach_def by blast
      ultimately show ‹¬ ⟦S, i⟧ ⊨ ❙□ p›
        unfolding canonical_ctx_def canonical_def gframe.defs frame.defs
        by auto
    qed
  next
    case (Sat k p)
    then show ?thesis
    proof (safe del: notI)
      assume ‹x = ❙@k p› ‹(i, ❙@k p) ∈ S›
      then have ‹(k, p) ∈ S›
        using alpha by (fastforce intro: CSatP)
      then have ‹⟦S, k⟧ ⊨ p›
        using 2 Sat by simp
      then show ‹⟦S, i⟧ ⊨ ❙@k p›
        unfolding canonical_ctx_def canonical_def gframe.defs
        by (auto split: tm.splits)
    next
      assume ‹x = ❙@k p› ‹(i, ❙¬ ❙@k p) ∈ S›
      then have ‹(k, ❙¬ p) ∈ S›
        using alpha by (fastforce intro: CSatN)
      then have ‹¬ ⟦S, k⟧ ⊨ p›
        using 2 Sat by simp
      then show ‹¬ ⟦S, i⟧ ⊨ ❙@k p›
        unfolding canonical_ctx_def canonical_def gframe.defs
        by (auto split: tm.splits)
    qed
  next
    case (Glo p)
    then show ?thesis
    proof (safe del: notI)
      assume ‹x = ❙A p› ‹(i, ❙A p) ∈ S›
      then have ‹(k, p) ∈ S› for k
        using gammaI by (fastforce intro: CGloP)
      then have ‹⟦S, k⟧ ⊨ p› for k
        using 2 Glo by simp
      then show ‹⟦S, i⟧ ⊨ ❙A p›
        unfolding canonical_ctx_def canonical_def gframe.defs frame.defs
        by auto
    next
      assume ‹x = ❙A p› ‹(i, ❙¬ ❙A p) ∈ S›
      then have ‹∃k. (k, ❙¬ p) ∈ S›
        using δ by fastforce
      then have ‹∃k. ¬ ⟦S, k⟧ ⊨ p›
        using 2 Glo by auto
      then show ‹¬ ⟦S, i⟧ ⊨ ❙A p›
        unfolding canonical_ctx_def canonical_def gframe.defs frame.defs
        by auto
    qed
  next
    case (Dwn p)
   then show ?thesis
    proof (safe del: notI)
      assume ‹x = ❙↓ p› ‹(i, ❙↓ p) ∈ S›
      then have ‹(i, ⟨i⟩⇩_i p) ∈ S›
        using alpha by (fastforce intro: CDwnP)
      moreover have ‹(⟨i⟩⇩_i p, x) ∈ measures [qs_fm, sz_fm]›
        using Dwn by simp
      ultimately have ‹⟦S, i⟧ ⊨ ⟨i⟩⇩_i p›
        using 2 by (meson in_measure)
      then show ‹⟦S, i⟧ ⊨ ❙↓ p›
        unfolding canonical_ctx_def canonical_def gframe.defs
        by simp
    next
      assume ‹x = ❙↓ p› ‹(i, ❙¬ ❙↓ p) ∈ S›
      then have ‹(i, ❙¬ ⟨i⟩⇩_i p) ∈ S›
        using alpha by (fastforce intro: CDwnN)
      moreover have ‹(⟨i⟩⇩_i p, x) ∈ measures [qs_fm, sz_fm]›
        using Dwn by simp
      ultimately have ‹¬ ⟦S, i⟧ ⊨ ⟨i⟩⇩_i p›
        using 2 by (meson in_measure)
      then show ‹¬ ⟦S, i⟧ ⊨ ❙↓ p›
        unfolding canonical_ctx_def canonical_def gframe.defs
        by simp
    qed
  next
    case (All p)
    then show ?thesis
    proof (safe del: notI)
      assume ‹x = ❙∀ p› ‹(i, ❙∀ p) ∈ S›
      then have ‹softqdf q ⟹ (i, ⟨q⟩⇩_p p) ∈ S› for q
        using gammaP by (fastforce intro: CAllP)
      moreover have ‹softqdf q ⟹ (⟨q⟩⇩_p p, x) ∈ measures [qs_fm, sz_fm]› for q
        using All by (metis less_add_one measures_less qs_fm.simps(9) qs_fm_sub_pro softqdf_add_env)
      ultimately have *: ‹softqdf q ⟹ ⟦S, i⟧ ⊨ ⟨q⟩⇩_p p› for q
        using 2 by (meson in_measure)
      
      moreover note wf_canonical[of S] assign_in_W[of i]
      ultimately have ‹softqdf q ⟹
        ((canonical S)⦇𝔙 := (worlds (canonical S) q ⪢ 𝔙 (canonical S))⦈, [i]⇩S) ⊨ p› for q
        using inst_single_worlds[where W=‹𝒲 (canonical S)› and q=q] unfolding canonical_ctx_def canonical_def unfolds by fastforce
      then have ‹(∀P ∈ sqdfs (canonical S). ((canonical S)⦇𝔙 := (P ⪢ 𝔙 (canonical S))⦈, [i]⇩S) ⊨ p)›
        unfolding sqdfs_def by blast
      then have ‹(∀P ∈ Π (canonical S). ((canonical S)⦇𝔙 := (P ⪢ 𝔙 (canonical S))⦈, [i]⇩S) ⊨ p)›
        using sqdfs_canonical by blast
      then show ‹⟦S, i⟧ ⊨ ❙∀ p›
        unfolding canonical_ctx_def by simp
    next
      assume ‹x = ❙∀ p› ‹(i, ❙¬ ❙∀ p) ∈ S›
      then obtain P where ‹(i, ❙¬ ⟨❙⋅ (❙○ P)⟩⇩_p p) ∈ S›
        using δ by auto
      moreover have ‹(❙¬ ⟨❙⋅ (❙○ P)⟩⇩_p p, x) ∈ measures [qs_fm, sz_fm]›
        using All
        by (metis less_add_one measures_less qs_fm.simps(3) qs_fm.simps(9) qs_fm_sub_pro softqdf.simps(2) softqdf_add_env)
      ultimately have ‹¬ ⟦S, i⟧ ⊨ ⟨❙⋅ (❙○ P)⟩⇩_p p›
        using 2 unfolding canonical_ctx_def by auto
      moreover have ‹softqdf (❙⋅ (❙○ P))›
        by simp
      moreover note wf_canonical[of S] assign_in_W[of i]
      ultimately have ‹softqdf (❙⋅ (❙○ P)) ∧
        ¬ ((canonical S)⦇𝔙 := (worlds (canonical S) (❙⋅ (❙○ P)) ⪢ 𝔙 (canonical S))⦈, [i]⇩S) ⊨ p›
        using inst_single_worlds[where W=‹𝒲 (canonical S)›] unfolding canonical_ctx_def canonical_def unfolds
        by fastforce
      then have ‹(∃P ∈ sqdfs (canonical S). ¬ ((canonical S)⦇𝔙 := (P ⪢ 𝔙 (canonical S))⦈, [i]⇩S) ⊨ p)›
        unfolding sqdfs_def by blast
      then have ‹(∃P ∈ Π (canonical S). ¬ ((canonical S)⦇𝔙 := (P ⪢ 𝔙 (canonical S))⦈, [i]⇩S) ⊨ p)›
        using sqdfs_canonical by blast
      then show ‹¬ ⟦S, i⟧ ⊨ ❙∀ p›
        unfolding canonical_ctx_def by simp
    qed
  qed
qed

end

theorem model_existence:
  fixes S :: ‹'x lbd set›
  assumes ‹P.prop⇩_E Kinds C›
    and ‹S ∈ C›
    and ‹P.enough_new S›
    and ‹(i, p) ∈ S›
  shows ‹⟦mk_mcs C S, i⟧ ⊨ 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 ‹(i, p) ∈ mk_mcs C S›
    using assms(4) Extend_subset by blast
  ultimately show ?thesis
    using MyHintikka.model by blast
qed

section ‹Natural Deduction›

inductive Calculus_Set :: ‹'x lbd set ⇒ 'x lbd ⇒ bool› (‹_ ⊩ _› [50, 50] 50) where
  Assm [dest]: ‹(i, p) ∈ A ⟹ A ⊩ (i, p)›
| Ref [simp]: ‹A ⊩ (i, ❙∙i)›
| Nom [dest]: ‹A ⊩ (i, ❙∙k) ⟹ A ⊩ (i, p) ⟹ A ⊩ (k, p)›
| NotI [intro]: ‹{(i, p)} ∪ A ⊩ (i, ❙⊥) ⟹ A ⊩ (i, ❙¬ p)›
| NotE [elim]: ‹A ⊩ (i, ❙¬ p) ⟹ A ⊩ (i, p) ⟹ A ⊩ (k, q)›
| AndI [intro]: ‹A ⊩ (i, p) ⟹ A ⊩ (i, q) ⟹ A ⊩ (i, p ❙∧ q)›
| AndD1 [dest]: ‹A ⊩ (i, p ❙∧ q) ⟹ A ⊩ (i, p)›
| AndD2 [dest]: ‹A ⊩ (i, p ❙∧ q) ⟹ A ⊩ (i, q)›
| SatI [intro]: ‹A ⊩ (i, p) ⟹ A ⊩ (k, ❙@i p)›
| SatE [dest]: ‹A ⊩ (i, ❙@k p) ⟹ A ⊩ (k, p)›
| BoxI [intro]: ‹{(i, ❙◇ (❙∙ (❙○k)))} ∪ A ⊩ (❙○k, p) ⟹ k ∉ symbols ({(i, p)} ∪ A) ⟹ A ⊩ (i, ❙□ p)›
| BoxE [elim]: ‹A ⊩ (i, ❙□ p) ⟹ A ⊩ (i, ❙◇ (❙∙k)) ⟹ A ⊩ (k, p)›
| GloI [intro]: ‹A ⊩ (❙○k, p) ⟹ k ∉ symbols ({(i, p)} ∪ A) ⟹ A ⊩ (i, ❙A p)›
| GloE [dest]: ‹A ⊩ (i, ❙A p) ⟹ A ⊩ (k, p)›
| DwnI [intro]: ‹A ⊩ (i, ⟨i⟩⇩_i p) ⟹ A ⊩ (i, ❙↓ p)›
| DwnE [dest]: ‹A ⊩ (i, ❙↓ p) ⟹ A ⊩ (i, ⟨i⟩⇩_i p)›
| AllI [intro]: ‹A ⊩ (i, ⟨❙⋅(❙○P)⟩⇩_p p) ⟹ P ∉ symbols ({(i, p)} ∪ A) ⟹ A ⊩ (i, ❙∀ p)›
| AllE [dest]: ‹A ⊩ (i, ❙∀ p) ⟹ softqdf q ⟹ A ⊩ (i, ⟨q⟩⇩_p p)›
| Clas: ‹{(i, ❙¬ p)} ∪ A ⊩ (i, p) ⟹ A ⊩ (i, p)›

subsection ‹Soundness›

theorem soundness:
  assumes ‹A ⊩ (i, p)› ‹∀(k, q) ∈ A. (Model W R PI N e V f, case_tm e N k) ⊨ q›
    ‹wf_model (Model W R PI N e V f)›
  shows ‹(Model W R PI N e V f, case_tm e N i) ⊨ p›
  using assms
proof (induct A ‹(i, p)› arbitrary: i p N V pred: Calculus_Set)
  case (Ref A i)
  then show ?case
    by (auto split: tm.splits)
next
  case (Nom A i k p)
  then show ?case
    by (auto split: tm.splits)
next
  case (SatI A i p k)
  then show ?case
    by (auto split: tm.splits)
next
  case (SatE A i k p)
  then show ?case
    by (auto split: tm.splits)
next
  case (BoxI i k A p)
  {
    fix v
    assume v: ‹v ∈ R (case_tm e N i)›
    moreover have ‹case_tm e N i ∈ W›
      using BoxI(5) unfolding wf_env_def wf_model_def unfolds by (auto split: tm.splits)
    ultimately have ‹v ∈ W›
      using BoxI(5) unfolding wf_model_def wf_gframe_def wf_frame_def unfolds by blast
 
    let ?N = ‹N(k := v)›
    have ‹∀(i, p) ∈ A. (Model W R PI ?N e V f, case_tm e ?N i) ⊨ p›
      using BoxI by fastforce
    moreover have ‹(Model W R PI ?N e V f, case_tm e ?N i) ⊨ ❙◇ (❙∙ (❙○ k))›
      using v BoxI.hyps(3) by (simp split: tm.splits)
    moreover have ‹wf_model (Model W R PI ?N e V f)›
      using BoxI.prems(2) ‹v ∈ W› unfolding wf_env_def wf_model_def unfolds by auto
    ultimately have ‹(Model W R PI ?N e V f, ?N k) ⊨ p›
      using BoxI.hyps(2) by fastforce
  }
  then have ‹∀v ∈ R (case_tm e N i). (Model W R PI (N(k := v)) e V f, v) ⊨ p›
    by simp
  then have ‹∀v ∈ R (case_tm e N i). (Model W R PI N e V f, v) ⊨ p›
    using BoxI.hyps(3) by simp
  then show ?case
    by simp
next
  case (BoxE A i p k)
  then show ?case
    by (auto split: tm.splits)
next
  case (GloI A k p i)
  {
    fix v
    assume ‹v ∈ W›
    let ?N = ‹N(k := v)›
    have ‹∀v. ∀(i, p) ∈ A. (Model W R PI ?N e V f, case_tm e ?N i) ⊨ p›
      using GloI.prems(1) GloI.hyps(3) by fastforce
    moreover have ‹wf_model (Model W R PI ?N e V f)›
      using GloI.prems(2)  ‹v ∈ W› unfolding wf_env_def wf_model_def unfolds by auto
    ultimately have ‹(Model W R PI ?N e V f, ?N k) ⊨ p›
      using GloI.hyps(2) by fastforce
  }
  then have ‹∀v ∈ W. (Model W R PI (N(k := v)) e V f, v) ⊨ p›
    by simp
  then have ‹∀v ∈ W. (Model W R PI N e V f, v) ⊨ p›
    using GloI.hyps(3) by simp
  then show ?case
    by simp
next
  case (GloE A i p k)
  then show ?case
    using wf_𝔑 wf_𝒩
    by (cases k) fastforce+
next
  case (AllI A i P p)
  {
    fix X
    assume ‹X ∈ PI›
    let ?V = ‹V(P := X)›
    have ‹∀v. ∀(i, p) ∈ A. (Model W R PI N e ?V f, case_tm e N i) ⊨ p›
      using AllI.prems(1) AllI.hyps(3) by fastforce
    moreover have *: ‹wf_model (Model W R PI N e ?V f)›
      using AllI.prems(2) ‹X ∈ PI› unfolding wf_env_def wf_model_def unfolds by auto
    ultimately have ‹(Model W R PI N e ?V f, case_tm e N i) ⊨ ⟨❙⋅ (❙○ P)⟩⇩_p p›
      using AllI.hyps(2) by fast
    moreover have ‹case_tm e N i ∈ W›
      using AllI.prems(2) unfolding wf_model_def wf_env_def unfolds by (auto split: tm.splits) 
    ultimately have ‹(Model W R PI N e ?V (worlds (Model W R PI N e ?V f) (❙⋅ (❙○ P)) ⪢ f), case_tm e N i) ⊨ p›
      using inst_single_worlds * by fastforce
    then have ‹(Model W R PI N e ?V ({ w ∈ W. w ∈ X } ⪢ f), case_tm e N i) ⊨ p›
      unfolding worlds_def by simp
    moreover have ‹X ∈ Pow W›
      using AllI.prems(2) ‹X ∈ PI› unfolding wf_model_def wf_gframe_def unfolds by auto
    then have ‹{ w ∈ W. w ∈ X } = X›
      by blast
    ultimately have ‹(Model W R PI N e ?V (X ⪢ f), case_tm e N i) ⊨ p›
      by simp
  }
  then have ‹∀X ∈ PI. (Model W R PI N e (V(P := X)) (X ⪢ f), case_tm e N i) ⊨ p›
    by simp
  then have ‹∀X ∈ PI. (Model W R PI N e V (X ⪢ f), case_tm e N i) ⊨ p›
    using AllI.hyps(3) by simp
  then show ?case
    by simp
next
  case (AllE A i p q)
  then show ?case
  proof (cases i)
    case (Var x1)
    then show ?thesis
      using AllE(2-) inst_single_worlds softqdf_worlds wf_𝔑 by fastforce
  next
    case (Sym x2)
    then show ?thesis
      using AllE(2-) inst_single_worlds softqdf_worlds wf_𝒩 by fastforce
  qed
qed auto

corollary soundness':
  assumes ‹{} ⊩ (❙○i, p)› ‹i ∉ symbols_fm p›
    and ‹wf_model M› ‹w ∈ 𝒲 M›
  shows ‹(M, w) ⊨ p›
proof (cases M)
  case (fields W R PI N e V f)
  let ?N = ‹N(i := w)›
  have ‹wf_model (Model W R PI ?N e V f)›
    using fields assms(3-4) unfolding wf_env_def wf_model_def unfolds by auto
  then have ‹(Model W R PI ?N e V f, case_tm e ?N (❙○i)) ⊨ p›
    using assms(1) soundness by blast
  then have ‹(Model W R PI ?N e V f, w) ⊨ p›
    by simp
  then show ?thesis
    using assms(2) fields by simp
qed

lemma no_bot: ‹¬ (M, w) ⊨ ❙⊥›
  by simp

corollary ‹¬ ({} ⊩ (❙○i, ❙⊥))›
  using soundness no_bot wf_canonical unfolding canonical_def unfolds
  by (metis (no_types, lifting) emptyE)

subsection ‹Derived Rules›

lemma Assm_head [simp]: ‹{(p, i)} ∪ A ⊩ (p, i)›
  using Assm by blast

lemma Boole: ‹{(i, ❙¬ p)} ∪ A ⊩ (i, ❙⊥) ⟹ A ⊩ (i, p)›
  using Clas AndD1 AndD2 NotE by meson

lemma FlsE [dest]: ‹A ⊩ (i, ❙⊥) ⟹ A ⊩ (k, p)›
  by (meson Assm_head NotE NotI)

subsection ‹Derivational Consistency›

lemma calculus_confl:
  assumes ‹ps ↝⇩_✗ qs› ‹set ps ⊆ A› ‹q ∈ set qs› ‹q ∈ A› 
  shows ‹A ⊩ (i, ❙⊥)›
  using assms
proof cases
  case (CNegP i p)
  then show ?thesis
    using assms(2-)
    by (metis Assm NotE empty_set equals0D list.set_intros(1) set_ConsD subset_eq)
next
  case (CNegI i k)
  then show ?thesis
    using assms(2-) by fastforce
qed

lemma calculus_alpha:
  assumes ‹ps ↝⇩_α qs› ‹set ps ⊆ A› ‹set qs ∪ A ⊩ (i, ❙⊥)›
  shows ‹A ⊩ (i, ❙⊥)›
  using assms
proof cases
  case (CSym i k)
  then show ?thesis
    using assms(2-)
    by (metis Assm_head Diff_partition Nom NotE NotI Ref list.set(1) list.simps(15))
next
  case (CNom i k p)
  then show ?thesis
    using assms(2-)
    by (metis AndD1 AndD2 Assm Nom NotE NotI empty_set insert_subset list.simps(15))
next
  case (CNegN i p)
  then show ?thesis
    using assms(2-)
    by (metis Assm_head Diff_partition NotE NotI empty_set list.simps(15))
next
  case (CConP k p q)
  then have ‹A ⊩ (k, p)› ‹A ⊩ (k, q)›
    using assms(2-) by (meson AndD1 AndD2 Assm list.set_intros(1) subset_eq)+
  moreover have ‹{(k, p), (k, q)} ∪ A ⊩ (k, ❙⊥)›
    using CConP assms(2-) by auto
  then have ‹{(k, q)} ∪ A ⊩ (k, ❙¬ p)›
    using NotI by auto
  ultimately have ‹A ⊩ (k, ❙⊥)›
    using CConP(1) assms(2)
    by (metis AndD1 Assm NotE NotI list.set_intros(1) subset_code(1) sup.coboundedI2)
  then show ?thesis
    by blast
next
  case (CSatP i k p)
  then show ?thesis
    using assms(2-) SatE[of A i k p]
    by (metis Assm_head NotE NotI empty_set le_iff_sup list.simps(15))
next
  case (CSatN i k p)
  then show ?thesis
    using assms(2-) SatI[of A k p]
    by (metis Assm_head Boole FlsE NotE empty_set le_iff_sup list.simps(15))
next
  case (CBoxP i p k)
  then show ?thesis
    using assms(2-) BoxE[of A i p]
    by (metis AndD1 AndD2 Assm NotE NotI empty_set insert_subset list.simps(15))
next
  case (CDwnP i p)
  then show ?thesis
    using assms(2-) DwnE[of A i p]
    by (metis Assm_head Diff_partition NotE NotI empty_set list.simps(15))
next
  case (CDwnN i p)
  then show ?thesis
    using assms(2-) DwnI[of A i p]
    by (metis AndD1 AndD2 Assm_head Clas NotE empty_set le_iff_sup list.simps(15))
qed

lemma calculus_beta:
  assumes ‹ps ↝⇩_β qs› ‹set ps ⊆ A› ‹∀q ∈ set qs. {q} ∪ A ⊩ (i, ❙⊥)›
  shows ‹A ⊩ (i, ❙⊥)›
  using assms
proof cases
  case (CConN i p q)
  then show ?thesis
    using assms(2-) AndI[of A i p q]
    by (metis Assm Clas FlsE NotE UnI2 insert_is_Un list.set_intros(1) list.simps(15) subset_iff)
qed

lemma calculus_gammaI:
  assumes ‹ps ↝⇩_γ⇩_i qs› ‹set ps ⊆ A› ‹set (qs k) ∪ A ⊩ (i, ❙⊥)›
  shows ‹A ⊩ (i, ❙⊥)›
  using assms
proof cases
  case CRefl
  then show ?thesis
    using CRefl assms(2-) Ref[of A k] 
    by (metis (mono_tags, lifting) AndD1 AndD2 NotE NotI empty_set list.simps(15))
next
  case (CGloP i p)
  then show ?thesis
    using CGloP assms(2-) GloE[of A i p k]
    by (metis (no_types, lifting) Assm_head NotE NotI empty_set le_iff_sup list.simps(15))
qed

lemma calculus_gammaP:
  assumes ‹ps ↝⇩_γ⇩_p (F, qs)› ‹set ps ⊆ A› ‹k ∈ F A› ‹set (qs k) ∪ A ⊩ (i, ❙⊥)›
  shows ‹A ⊩ (i, ❙⊥)›
  using assms
proof cases
  case (CAllP i p)
  then show ?thesis
    using assms(2-) AllE[of A i p]
    by (metis (no_types, lifting) Assm_head NotE NotI le_iff_sup list.set(1) list.simps(15) mem_Collect_eq)
qed

lemma calculus_δ:
  assumes ‹p ∈ A› ‹k ∉ symbols A› ‹set (δ p k) ∪ A ⊩ (a, ❙⊥)›
  shows ‹A ⊩ (a, ❙⊥)›
  using assms
proof (induct p k rule: δ.induct)
  case (1 i p k)
  then have ‹{(❙○k, ❙¬ p), (i, ❙◇ (❙∙(❙○k)))} ∪ A ⊩ (a, ❙⊥)› ‹(i, ❙¬ ❙□ p) ∈ A›
    by simp_all
  then have ‹{(i, ❙◇ (❙∙(❙○k)))} ∪ A ⊩ (❙○k, p)›
    using Boole by auto
  moreover have ‹k ∉ symbols ({(i, p)} ∪ A)›
    using 1 by auto
  ultimately have ‹A ⊩ (i, ❙□ p)›
    using BoxI by blast
  then show ?thesis
    using ‹(i, ❙¬ ❙□ p) ∈ A› by (meson Assm NotE)
next
  case (2 i p k)
  then have ‹{(❙○k, ❙¬ p)} ∪ A ⊩ (a, ❙⊥)› ‹(i, ❙¬ ❙A p) ∈ A›
    by simp_all
  then have ‹{(❙○k, ❙¬ p)} ∪ A ⊩ (❙○k, ❙⊥)›
    by fast
  then have ‹A ⊩ (❙○k, p)›
    by (meson Boole)
  moreover have ‹k ∉ symbols ({(i, p)} ∪ A)›
    using 2 CGloN by auto
  ultimately have ‹A ⊩ (i, ❙A p)›
    by blast
  then show ?thesis
    using ‹(i, ❙¬ ❙A p) ∈ A› Assm NotE by meson
next
  case (3 i p P)
  then have ‹{(i, ❙¬ ⟨❙⋅ (❙○ P)⟩⇩_p p)} ∪ A ⊩ (a, ❙⊥)› ‹(i, ❙¬ ❙∀ p) ∈ A›
    by simp_all
  then have ‹A ⊩ (i, ⟨❙⋅ (❙○ P)⟩⇩_p p)›
    using Clas by blast
  moreover have ‹P ∉ symbols ({(i, p)} ∪ A)›
    using 3 by auto
  ultimately have ‹A ⊩ (i, ❙∀ p)›
    by blast
  then show ?thesis
    using ‹(i, ❙¬ ❙∀ p) ∈ A› Assm NotE by meson
qed simp_all

interpretation DC: Derivational_Confl map_lbd symbols_lbd ‹λ_. True› confl_class ‹λA. ¬ A ⊩ (a, ❙⊥)›
  using calculus_confl by unfold_locales blast

interpretation DA: Derivational_Alpha map_lbd symbols_lbd ‹λ_. True› alpha_class ‹λA. ¬ A ⊩ (a, ❙⊥)›
  using calculus_alpha by unfold_locales blast

interpretation DB: Derivational_Beta map_lbd symbols_lbd ‹λ_. True› beta_class ‹λA. ¬ A ⊩ (a, ❙⊥)›
  using calculus_beta by unfold_locales blast

interpretation DGI: Derivational_Gamma map_tm map_lbd symbols_lbd ‹λ_. True› GI.classify_UNIV ‹λA. ¬ A ⊩ (a, ❙⊥)›
  using calculus_gammaI by unfold_locales blast

interpretation DGP: Derivational_Gamma map_fm map_lbd symbols_lbd ‹λ_. True› gamma_class_fm ‹λA. ¬ A ⊩ (a, ❙⊥)›
  using calculus_gammaP by unfold_locales blast

interpretation DD: Derivational_Delta map_lbd symbols_lbd ‹λ_. True› δ ‹λA. ¬ A ⊩ (a, ❙⊥)›
  by unfold_locales (meson calculus_δ)
  
interpretation Derivational_Consistency map_lbd symbols_lbd ‹λ_. True› Kinds ‹λA. ¬ A ⊩ (a, ❙⊥)›
  using prop⇩_E_Kinds[OF DC.kind DA.kind DB.kind DGI.kind DGP.kind DD.kind] by unfold_locales

subsection ‹Strong Completeness›

theorem strong_completeness:
  fixes p :: ‹'x fm›
  assumes mod: ‹⋀(M :: ('x, 'x tm) model) w. wf_model M ⟹ w ∈ 𝒲 M ⟹
      ∀(k, q) ∈ A. (M, case_tm (𝔑 M) (𝒩 M) k) ⊨ q ⟹
      (M, w) ⊨ p›
    and ‹P.enough_new A›
  shows ‹A ⊩ (i, p)›
proof (rule ccontr)
  assume ‹¬ A ⊩ (i, p)›
  then have *: ‹¬ {(i, ❙¬ p)} ∪ A ⊩ (i, ❙⊥)›
    using Boole by blast

  let ?S = ‹{(i, ❙¬ p)} ∪ A›
  let ?C = ‹{A. P.enough_new A ∧ ¬ A ⊩ (undefined, ❙⊥)}›
  let ?H = ‹mk_mcs ?C ?S›
  let ?M = ‹canonical ?H›

  have ‹P.prop⇩_E Kinds ?C›
    using Consistency by fast
  moreover have ‹?S ∈ ?C›
    using * FlsE params_left assms(2)
    by (metis (no_types, lifting) ext List.set_insert empty_set mem_Collect_eq )
  moreover from this have ‹P.enough_new ?S›
    by blast
  ultimately have **: ‹∀(k, q) ∈ ?S. ⟦?H, k⟧ ⊨ q›
    using model_existence[of ?C ?S] by blast
  then have ‹∀(k, q) ∈ ?S. (?M, case_tm (𝔑 ?M) (𝒩 ?M) k) ⊨ q›
    unfolding canonical_tm_eta' canonical_ctx_def by blast

  moreover have ‹wf_model ?M›
    using wf_canonical by blast
  moreover have ‹assign i ?H ∈ 𝒲 ?M›
    unfolding canonical_def unfolds by auto

  ultimately have ‹⟦?H, i⟧ ⊨ p›
    using mod unfolding canonical_ctx_def by auto

  moreover have ‹¬ ⟦?H, i⟧ ⊨ p›
    using ** unfolding canonical_ctx_def by simp
  ultimately show False
    by simp
qed

section ‹Natural Deduction with Lists›

inductive Calculus :: ‹'x lbd list ⇒ 'x lbd ⇒ bool› (infix ‹⊢› 50) where
  Assm [dest]: ‹(i, p) ∈ set A ⟹ A ⊢ (i, p)›
| Ref [simp]: ‹A ⊢ (i, ❙∙i)›
| Nom [dest]: ‹A ⊢ (i, ❙∙k) ⟹ A ⊢ (i, p) ⟹ A ⊢ (k, p)›
| NotI [intro]: ‹(i, p) # A ⊢ (i, ❙⊥) ⟹ A ⊢ (i, ❙¬ p)›
| NotE [elim]: ‹A ⊢ (i, ❙¬ p) ⟹ A ⊢ (i, p) ⟹ A ⊢ (k, q)›
| AndI [intro]: ‹A ⊢ (i, p) ⟹ A ⊢ (i, q) ⟹ A ⊢ (i, p ❙∧ q)›
| AndD1 [dest]: ‹A ⊢ (i, p ❙∧ q) ⟹ A ⊢ (i, p)›
| AndD2 [dest]: ‹A ⊢ (i, p ❙∧ q) ⟹ A ⊢ (i, q)›
| SatI [intro]: ‹A ⊢ (i, p) ⟹ A ⊢ (k, ❙@i p)›
| SatE [dest]: ‹A ⊢ (i, ❙@k p) ⟹ A ⊢ (k, p)›
| BoxI [intro]: ‹(i, ❙◇ (❙∙ (❙○k))) # A ⊢ (❙○k, p) ⟹ k ∉ symbols ({(i, p)} ∪ set A) ⟹ A ⊢ (i, ❙□ p)›
| BoxE [elim]: ‹A ⊢ (i, ❙□ p) ⟹ A ⊢ (i, ❙◇ (❙∙k)) ⟹ A ⊢ (k, p)›
| GloI [intro]: ‹A ⊢ (❙○k, p) ⟹ k ∉ symbols ({(i, p)} ∪ set A) ⟹ A ⊢ (i, ❙A p)›
| GloE [dest]: ‹A ⊢ (i, ❙A p) ⟹ A ⊢ (k, p)›
| DwnI [intro]: ‹A ⊢ (i, ⟨i⟩⇩_i p) ⟹ A ⊢ (i, ❙↓ p)›
| DwnE [dest]: ‹A ⊢ (i, ❙↓ p) ⟹ A ⊢ (i, ⟨i⟩⇩_i p)›
| AllI [intro]: ‹A ⊢ (i, ⟨❙⋅(❙○P)⟩⇩_p p) ⟹ P ∉ symbols ({(i, p)} ∪ set A) ⟹ A ⊢ (i, ❙∀ p)›
| AllE [dest]: ‹A ⊢ (i, ❙∀ p) ⟹ softqdf q ⟹ A ⊢ (i, ⟨q⟩⇩_p p)›
| Clas: ‹(i, ❙¬ p) # A ⊢ (i, p) ⟹ A ⊢ (i, p)›

definition bounded :: ‹'a list ⇒ 'a set ⇒ ('a list ⇒ bool) ⇒ bool› where
  ‹bounded K A P ≡ set K ⊆ A ∧ (∀B. set K ⊆ set B ⟶ set B ⊆ A ⟶ P B)›

lemma bounded_one [elim]:
  assumes ‹bounded K A P› ‹⋀A. P A ⟹ Q A›
  shows ‹bounded K A Q›
  using assms unfolding bounded_def by simp

lemma bounded_two [elim]:
  assumes ‹bounded K A P› ‹bounded K' A Q› ‹⋀A. P A ⟹ Q A ⟹ R A›
  shows ‹bounded (K @ K') A R›
  using assms unfolding bounded_def by simp

lemma bounded_removeAll [dest]:
  assumes ‹bounded K ({p} ∪ A) P›
  shows ‹bounded (removeAll p K) A (λB. P (p # B))›
  using assms unfolding bounded_def
  by (metis Diff_subset_conv insert_is_Un insert_mono list.simps(15) set_removeAll)

lemma bounded_params:
  assumes ‹a ∉ P.params ({p} ∪ A)› ‹bounded K A P›
  shows ‹bounded K A (λB. a ∉ P.params (set (p # B)))›
  using assms unfolding bounded_def by auto

lemma finite_kernel: ‹A ⊩ (i, p) ⟹ ∃K. bounded K A (λB. B ⊢ (i, p))›
proof (induct A ‹(i, p)› arbitrary: i p pred: Calculus_Set)
  case (Assm i p A)
  then show ?case
    unfolding bounded_def using Calculus.Assm
    by (metis empty_subsetI insert_subset set_replicate_Suc)
next
  case (Ref A i)
  then show ?case
    unfolding bounded_def using Calculus.Ref
    by (metis empty_set empty_subsetI)
next
  case (Nom A i k p)
  then show ?case
    by force
next
  case (NotI i p A)
  then have ‹∃K. bounded K A (λB. (i, p) # B ⊢ (i, ❙⊥))›
    by blast
  then show ?case
    by fast
next
  case (BoxI i k A p)
  then have ‹∃K. bounded K A (λB. (i, ❙◇ (❙∙ (❙○ k))) # B ⊢ (❙○ k, p))›
    by blast
  moreover from this have ‹∃K. bounded K A (λB. k ∉ P.params ({(i, p)} ∪ set B))›
    using BoxI(2-3) bounded_params by fastforce
  ultimately show ?case
    by fastforce
next
  case (GloI A k p i)
  then have ‹∃K. bounded K A (λB. B ⊢ (❙○ k, p))›
    by blast
  moreover from this have ‹∃K. bounded K A (λB. k ∉ P.params ({(i, p)} ∪ set B))›
    using GloI(3) bounded_params by fastforce
  ultimately show ?case
    by fastforce
next
  case (AllI A i P p)
  then have ‹∃K. bounded K A (λB. B ⊢ (i, ⟨❙⋅ (❙○ P)⟩⇩_p p))›
    by blast
  moreover from this have ‹∃K. bounded K A (λB. P ∉ P.params ({(i, p)} ∪ set B))›
    using AllI(3) bounded_params by fastforce
  ultimately show ?case
    by fastforce
next
  case (Clas i p A)
  then have ‹∃K. bounded K A (λB. (i, ❙¬ p) # B ⊢ (i, p))›
    by fast
  then show ?case
    using Calculus.Clas by force
qed fast+

corollary finite_assumptions: ‹A ⊩ (i, p) ⟹ ∃B. set B ⊆ A ∧ B ⊢ (i, p)›
  using finite_kernel unfolding bounded_def by blast

lemma calculus_set: ‹A ⊢ (i, p) ⟹ set A ⊩ (i, p)›
proof (induct A ‹(i, p)› arbitrary: i p pred: Calculus)
  case (Clas p q A)
  then show ?case
    using Calculus_Set.Clas by auto
qed auto

corollary soundness_list:
  assumes ‹A ⊢ (i, p)› ‹∀(k, q) ∈ set A. (M, case_tm (𝔑 M) (𝒩 M) k) ⊨ q›
    and ‹wf_model M›
  shows ‹(M, case_tm (𝔑 M) (𝒩 M) i) ⊨ p›
  using assms soundness calculus_set
  by (metis (mono_tags, lifting) model.surjective unit.exhaust split_cong)

corollary soundness_nil:
  ‹[] ⊢ (❙○i, p) ⟹ i ∉ symbols_fm p ⟹ wf_model M ⟹ w ∈ 𝒲 M ⟹ (M, w) ⊨ p›
  by (metis calculus_set empty_set soundness')
  
corollary ‹¬ ([] ⊢ (i, ❙⊥))›
  by (metis equals0D no_bot set_empty2 soundness_list wf_canonical)

corollary strong_completeness_list:
  fixes p :: ‹'x fm›
  assumes ‹⋀(M :: ('x, 'x tm) model) w. wf_model M ⟹ w ∈ 𝒲 M ⟹
      ∀(k, q) ∈ A. (M, case_tm (𝔑 M) (𝒩 M) k) ⊨ q ⟹ (M, w) ⊨ p›
    and ‹P.enough_new A›
  shows ‹∃B. set B ⊆ A ∧ B ⊢ (i, p)›
  using assms strong_completeness finite_assumptions by blast

theorem main:
  fixes p :: ‹'x fm›
  assumes ‹i ∉ symbols_fm p› ‹|UNIV :: 'x lbd set| ≤o  |UNIV :: 'x set|›
  shows ‹[] ⊢ (❙○i, p) ⟷ (∀(M :: ('x, 'x tm) model). ∀w ∈ 𝒲 M. wf_model M ⟶ (M, w) ⊨ p)›
  using assms strong_completeness_list[where A=‹{}›] soundness_nil unfolding P.enough_new_def by fastforce

section ‹The Need for SQDFs›

subsection ‹Finite Unions of Arithmetic Progressions›

subsubsection ‹From Manuel Eberl's Furstenberg-Topology AFP entry›

definition arith_prog :: "int ⇒ nat ⇒ int set" where
  "arith_prog a b = {x. [x = a] (mod int b)}"

lemma arith_prog_0_right [simp]: "arith_prog a 0 = {a}"
  by (simp add: arith_prog_def)

lemma arith_prog_Suc_0_right [simp]: "arith_prog a (Suc 0) = UNIV"
  by (auto simp: arith_prog_def)

lemma in_arith_progI [intro]: "[x = a] (mod b) ⟹ x ∈ arith_prog a b"
  by (auto simp: arith_prog_def)

lemma arith_prog_disjoint:
  assumes "[a ≠ a'] (mod int b)" and "b > 0"
  shows   "arith_prog a b ∩ arith_prog a' b = {}"
  using assms by (auto simp: arith_prog_def cong_def)

lemma arith_prog_dvd_mono: "b dvd b' ⟹ arith_prog a b' ⊆ arith_prog a b"
  by (auto simp: arith_prog_def cong_dvd_modulus)

lemma bij_betw_arith_prog:
  assumes "b > 0"
  shows   "bij_betw (λn. a + int b * n) UNIV (arith_prog a b)"
proof (rule bij_betwI[of _ _ _ "λx. (x - a) div int b"], goal_cases)
  case 1
  thus ?case 
    by (auto simp: arith_prog_def cong_add_lcancel_0 cong_mult_self_right mult_of_nat_commute)
next
  case 4
  thus ?case
    by (auto simp: arith_prog_def cong_iff_lin)
qed (use ‹b > 0› in ‹auto simp: arith_prog_def›)

lemma arith_prog_altdef: "arith_prog a b = range (λn. a + int b * n)"
proof (cases "b = 0")
  case False
  thus ?thesis
    using bij_betw_arith_prog[of b] by (auto simp: bij_betw_def)
qed auto

lemma infinite_arith_prog: "b > 0 ⟹ infinite (arith_prog a b)"
  using bij_betw_finite[OF bij_betw_arith_prog[of b]] by simp

(* from the lemma closed_arith_prog_fb *)
lemma arith_prog_complement:
  assumes ‹b > 0›
  shows "-arith_prog a b = (⋃i∈{1..<b}. arith_prog (a + int i) b)"
proof -
  have disjoint: "x ∉ arith_prog a b" if "x ∈ arith_prog (a + int i) b" "i ∈ {1..<b}" for x i
  proof -
    have "[a ≠ a + int i] (mod int b)"
    proof
      assume "[a = a + int i] (mod int b)"
      hence "[a + 0 = a + int i] (mod int b)" by simp
      hence "[0 = int i] (mod int b)" by (subst (asm) cong_add_lcancel) auto
      with that show False by (auto simp: cong_def)
    qed
    thus ?thesis using arith_prog_disjoint[of a "a + int i" b] ‹b > 0› that by auto
  qed

  have covering: "x ∈ arith_prog a b ∨ x ∈ (⋃i∈{1..<b}. arith_prog (a + int i) b)" for x
  proof -
    define i where "i = nat ((x - a) mod (int b))"
    have "[a + int i = a + (x - a) mod int b] (mod int b)"
      unfolding i_def using ‹b > 0› by simp
    also have "[a + (x - a) mod int b = a + (x - a)] (mod int b)"
      by (intro cong_add) auto
    finally have "[x = a + int i] (mod int b)"
      by (simp add: cong_sym_eq)
    hence "x ∈ arith_prog (a + int i) b"
      using ‹b > 0› by (auto simp: arith_prog_def)
    moreover have "i < b" using ‹b > 0› 
      by (auto simp: i_def nat_less_iff)
    ultimately show ?thesis using ‹b > 0›
      by (cases "i = 0") auto
  qed

  from disjoint and covering show ?thesis
    by blast
qed

(* from instance t2_space *)
lemma arith_prog_distinguish:
  assumes "x ≠ y"
  shows "∃a c b. b > 0 ∧ x ∈ arith_prog a b ∧ y ∈ arith_prog c b ∧ arith_prog a b ∩ arith_prog c b = {}"
proof -
  define d where "d = nat ¦x - y¦ + 1"
  from ‹x ≠ y› have "d > 0"
    unfolding d_def by auto
  define U where "U = arith_prog x d"
  define V where "V = arith_prog y d"

  have "U ∩ V = {}" unfolding U_def V_def d_def
  proof (use ‹x ≠ y› in transfer, rule arith_prog_disjoint)
    fix x y :: int
    assume "x ≠ y"
    show "[x ≠ y] (mod int (nat ¦x - y¦ + 1))"
    proof
      assume "[x = y] (mod int (nat ¦x - y¦ + 1))"
      hence "¦x - y¦ + 1 dvd ¦x - y¦"
        by (auto simp: cong_iff_dvd_diff algebra_simps)
      hence "¦x - y¦ + 1 ≤ ¦x - y¦"
        by (rule zdvd_imp_le) (use ‹x ≠ y› in auto)
      thus False by simp
    qed
  qed auto
  moreover have "x ∈ U" "y ∈ V"
    unfolding U_def V_def by (use ‹d > 0› in transfer, fastforce)+
  ultimately show ?thesis
    using U_def V_def ‹0 < d› by blast
qed

subsubsection ‹Unions of Arithmetic Progressions›

lemma arith_prog_offset_in: ‹k ∈ arith_prog a b ⟹ arith_prog k b = arith_prog a b›
  unfolding arith_prog_def by (simp add: cong_def)

lemma arith_prog_mod: ‹arith_prog (a mod int b) b = arith_prog a b›
  unfolding arith_prog_def by auto                   

lemma mod_bounds: ‹b > 0 ⟹ a mod int b ≥ 0 ∧ a mod int b < b›
  by simp

lemma mod_range: ‹{a mod int b |a. b > 0} ⊆ {0..<int b}›
  using mod_bounds by auto

lemma finite_mod_range: ‹finite {a mod int b |a. b > 0}›
  using mod_range by (meson finite_atLeastLessThan_int finite_subset)

definition arith :: ‹nat set ⇒ int set ⇒ bool› where
  ‹arith B U ≡ ∀a ∈ U. ∃b ∈ B. b > 0 ∧ arith_prog a b ⊆ U›

lemma arith_mono: ‹arith B U ⟹ B ⊆ C ⟹ arith C U›
  unfolding arith_def by blast

lemma arith_empty_steps: ‹arith B U ⟹ B = {} ⟹ U = {}›
  unfolding arith_def by blast

lemma arith_ne_steps: ‹arith B U ⟹ U ≠ {} ⟹ B ≠ {}›
  using arith_empty_steps by blast

lemma arith_decomp:
  assumes ‹arith B U›
  obtains abs where
    ‹finite B ⟹ finite abs›
    ‹⋀a b. (a, b) ∈ abs ⟹ b > 0 ∧ b ∈ B›
    ‹U = (⋃(a, b) ∈ abs. arith_prog a b)›
proof -
  have ‹∀a∈U. ∃b ∈ B. b > 0 ∧ arith_prog (a mod int b) b ⊆ U›
    using ‹arith B U› unfolding arith_def using arith_prog_mod by simp
  then obtain f where f: ‹∀a ∈ U. ∃b ∈ B. f a = b ∧ b > 0 ∧ arith_prog (a mod int b) b ⊆ U›
    by metis

  let ?abs = ‹{(a mod int (f a), f a) |a. a ∈ U}›

  have abs: ‹U = (⋃(a, b) ∈ ?abs. arith_prog a b)›
    using f by fastforce

  have ‹{a mod int (f a) |a. a ∈ U} ⊆ (⋃b ∈ B. {a mod int b |a. b > 0})›
    using f by blast
  moreover have ‹finite (⋃b ∈ B. {a mod int b |a. b > 0})› if ‹finite B›
    using that finite_mod_range by fast
  ultimately have ‹finite {a mod int (f a) |a. a ∈ U}› if ‹finite B›
    using that by (meson finite_subset)

  moreover have ‹?abs ⊆ {a mod int (f a) |a. a ∈ U} × f ` U›
    by blast
  moreover have fin_f: ‹finite (f ` U)› if ‹finite B›
    using that f by (meson finite_subset image_subsetI)
  ultimately have fin_abs: ‹finite ?abs› if ‹finite B›
    using that fin_f by (meson finite_SigmaI finite_subset)

  have pos: ‹⋀a b. (a, b) ∈ ?abs ⟹ b > 0 ∧ b ∈ B›
    using f by blast

  show ?thesis
    using fin_abs pos abs that by meson
qed

lemma arith_UNIV: ‹arith {1} UNIV›
  unfolding arith_def by blast

lemma arith_empty: "arith B {}"
  unfolding arith_def by blast

lemma finite_case_prod_lcm: ‹finite B ⟹ finite C ⟹ finite (case_prod lcm ` (B × C))›
  by blast

lemma arith_inter:
  assumes U: ‹arith B U› and V: ‹arith C V›
  shows ‹arith (case_prod lcm ` (B × C)) (U ∩ V)›
  unfolding arith_def
proof safe
  fix a
  assume a: ‹a ∈ U› ‹a ∈ V›
  
  from a U obtain b where b: ‹b ∈ B› ‹b > 0› ‹arith_prog a b ⊆ U›
    unfolding arith_def by auto
  from a V obtain c where c: ‹c ∈ C› ‹c > 0› ‹arith_prog a c ⊆ V›
    unfolding arith_def by auto

  with a b c U V have ‹arith_prog a (lcm b c) ⊆ U ∩ V›
    using arith_prog_dvd_mono[of b ‹lcm b c› a] arith_prog_dvd_mono[of c ‹lcm b c› a] by blast
  moreover from b c have ‹lcm b c > 0›
    using lcm_pos_nat by blast
  ultimately show ‹∃b∈(λ(x, y). lcm x y) ` (B × C). 0 < b ∧ arith_prog a b ⊆ U ∩ V›
    using b c by blast
qed

lemma arith_Inter:
  assumes ‹finite X› and X: ‹∀U ∈ X. arith B U› ‹X ≠ {}›
  shows ‹∃B'. (finite B ⟶ finite B') ∧ arith B' (⋂X)›
  using assms
proof (induct X rule: finite_induct)
  case empty
  then show ?case
    by simp
next
  case (insert U X)
  then show ?case
    using arith_inter finite_case_prod_lcm
    by (metis Inf_insert cInf_singleton insertCI)
qed

lemma arith_union:
  assumes ‹arith B U› ‹arith C V›
  shows ‹arith (B ∪ C) (U ∪ V)›
  using assms unfolding arith_def by (metis Un_iff subset_trans sup_ge1 sup_ge2)

lemma arith_ne_infinite:
  assumes ‹arith B U› ‹U ≠ {}›
  shows ‹infinite U›
  using assms unfolding arith_def
  by (meson equals0I infinite_arith_prog rev_finite_subset)

lemma arith_prog_arith [intro]:
  assumes ‹b > 0›
  shows ‹arith {b} (arith_prog a b)›
  unfolding arith_def using assms arith_prog_offset_in by blast

lemma arith_prog_complement_arith [intro]:
  assumes ‹b > 0›
  shows ‹arith {b} (- arith_prog a b)›
proof -
  have "-arith_prog a b = (⋃i∈{1..<b}. arith_prog (a + int i) b)"
    using assms arith_prog_complement by blast
  also from assms have "arith {b} …"
    unfolding arith_def using arith_prog_offset_in by blast
  finally show ?thesis .
qed

lemma arith_complement_arith [intro]:
  assumes ‹arith B U› ‹finite B›
  shows ‹∃B'. finite B' ∧ arith B' (- U)›
proof -
  obtain abs where
    abs: ‹⋀a b. (a, b) ∈ abs ⟹ b > 0 ∧ b ∈ B› ‹finite abs› and
    U: ‹U = (⋃(a, b) ∈ abs. arith_prog a b)›
    using assms arith_decomp by metis
  then have *: ‹⋀a b. (a, b) ∈ abs ⟹ - arith_prog a b = (⋃i∈{1..<b}. arith_prog (a + int i) b)›
    using arith_prog_complement by simp

  have ‹- U = (⋂(a, b) ∈ abs. - arith_prog a b)›
    using U by blast
  also have ‹… = (⋂(a, b) ∈ abs. (⋃i∈{1..<b}. arith_prog (a + int i) b))›
    using * by blast
  finally have **: ‹- U = (⋂(a, b) ∈ abs. (⋃i∈{1..<b}. arith_prog (a + int i) b))› .

  have ‹⋀a b. (a, b) ∈ abs ⟹ arith {b} (⋃i∈{1..<b}. arith_prog (a + int i) b)›
    using abs * by (metis arith_prog_complement_arith)
  then have ***: ‹⋀a b. (a, b) ∈ abs ⟹ arith B (⋃i∈{1..<b}. arith_prog (a + int i) b)›
    using arith_mono abs by fast

  define X where X: ‹X ≡ (λ(a, b). ⋃i∈{1..<b}. arith_prog (a + int i) b) ` abs›

  from X have ‹finite X›
    using abs(2) by simp
  moreover have ‹∀U∈X. arith B U›
    using X *** by fast
  ultimately have ‹∃B'. finite B' ∧ arith B' (⋂ X)›
    using arith_Inter[of X] ‹finite B› arith_UNIV by fastforce

  moreover from X have ‹- U = ⋂X›
    using ** by simp
  ultimately show ?thesis
    by simp
qed

lemma arith_distinguish:
  assumes ‹x ≠ y›
  shows ‹∃B U V. finite B ∧ arith B U ∧ arith B V ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = {}›
proof -
  obtain a b c where
    b: ‹0 < b› and x: ‹x ∈ arith_prog a b› and y: ‹y ∈ arith_prog c b› and
    *: ‹arith_prog a b ∩ arith_prog c b = {}›
    using assms arith_prog_distinguish by meson

  let ?B = ‹{b}›
  let ?U = ‹arith_prog a b›
  let ?V = ‹arith_prog c b›
  have ‹finite ?B ∧ arith ?B ?U ∧ arith ?B ?V ∧ x ∈ ?U ∧ y ∈ ?V ∧ ?U ∩ ?V = {}›
    using b x y *
    by blast
  then show ?thesis
    by blast
qed

subsubsection ‹Finite Unions of Arithmetic Progressions›

definition fin_arith :: ‹int set ⇒ bool› where
  ‹fin_arith U ≡ ∃B. finite B ∧ arith B U›

lemma fin_arith_UNIV [intro]: ‹fin_arith UNIV›
  unfolding fin_arith_def using arith_UNIV by force

lemma fin_arith_empty [intro]: ‹fin_arith {}›
  unfolding fin_arith_def using arith_empty by blast

lemma fin_arith_inter [intro]: ‹fin_arith U ⟹ fin_arith V ⟹ fin_arith (U ∩ V)›
  unfolding fin_arith_def using arith_inter finite_case_prod_lcm by metis

lemma fin_arith_union [intro]: ‹fin_arith U ⟹ fin_arith V ⟹ fin_arith (U ∪ V)›
  unfolding fin_arith_def using arith_union by blast

lemma fin_arith_compl [intro]: ‹fin_arith U ⟹ fin_arith (- U)›
  unfolding fin_arith_def by blast

lemma fin_arith_distinguish:
  assumes ‹x ≠ y›
  shows ‹∃U V. fin_arith U ∧ fin_arith V ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = {}›
  using assms arith_distinguish unfolding fin_arith_def by meson

subsubsection ‹Singletons›

lemma arith_prog_singleton: ‹⋂{arith_prog a b |a b. b > 0 ∧ x ∈ arith_prog a b} = {x}›
proof
  show ‹⋂ {arith_prog a b |a b. 0 < b ∧ x ∈ arith_prog a b} ⊆ {x}›
    using arith_prog_distinguish by fast
qed fast

lemma fin_arith_Inter_singleton: ‹⋂{U |U. fin_arith U ∧ x ∈ U} = {x}›
proof -
  have ‹{arith_prog a b |a b. b > 0 ∧ x ∈ arith_prog a b} ⊆ {U |U b. arith {b} U ∧ x ∈ U}›
    using arith_prog_arith by blast
  also have ‹… ⊆ {U |U B. finite B ∧ arith B U ∧ x ∈ U}›
    by force
  finally have ‹{arith_prog a b |a b. b > 0 ∧ x ∈ arith_prog a b} ⊆ {U |U. fin_arith U ∧ x ∈ U}›
    unfolding fin_arith_def by auto
  then have ‹⋂{U |U. fin_arith U ∧ x ∈ U} ⊆ ⋂{arith_prog a b |a b. b > 0 ∧ x ∈ arith_prog a b}›
    by blast
  then show ?thesis
    using arith_prog_singleton by auto
qed

lemma singleton_not_finarith: ‹¬ fin_arith {x}›
  unfolding fin_arith_def using arith_ne_infinite by blast

subsection ‹Counterexample›

definition Pss :: ‹int set set› where
  ‹Pss ≡ {U. fin_arith U}›

lemma Pss_empty: ‹{} ∈ Pss›
  unfolding Pss_def by blast

lemma Pss_UNIV: ‹UNIV ∈ Pss›
  unfolding Pss_def by blast

lemma Pss_union: ‹X ∈ Pss ⟹ Y ∈ Pss ⟹ X ∪ Y ∈ Pss›
  unfolding Pss_def by blast

lemma Pss_inter: ‹X ∈ Pss ⟹ Y ∈ Pss ⟹ X ∩ Y ∈ Pss›
  unfolding Pss_def by blast
  
lemma Pss_compl: ‹X ∈ Pss ⟹ - X ∈ Pss›
  unfolding Pss_def by blast

definition my_gframe :: ‹int gframe› where
  ‹my_gframe ≡ ⦇ 𝒲 = UNIV, ℛ = λx. UNIV, Π = Pss ⦈›

lemma wf_frame_mygframe: ‹wf_frame (frame.truncate my_gframe)›
  unfolding wf_frame_def unfolds my_gframe_def by blast  

lemma admissible_mygframe: ‹admissible (frame.truncate my_gframe) (Π my_gframe)›
  unfolding admissible_def unfolds my_gframe_def Pss_def
  by (auto simp: Compl_eq_Diff_UNIV[symmetric])

lemma wf_mygframe: ‹wf_gframe my_gframe›
  using wf_frame_mygframe admissible_mygframe
  unfolding wf_gframe_def unfolds my_gframe_def Pss_def by fast

definition my_model :: ‹(int, int) model› where
  ‹my_model ≡ gframe.extend my_gframe ⦇𝒩 = λi. i, 𝔑 = λi. int i, 𝒱 = λn. {}, 𝔙 = λn. {}⦈›

lemma wf_mymodel: ‹wf_model my_model›
  using wf_mygframe unfolding wf_model_def wf_env_def unfolds my_model_def my_gframe_def Pss_def
  by blast

abbreviation GloE :: ‹'x fm ⇒ 'x fm› (‹❙E›) where
  ‹❙E p ≡ ❙¬ (❙A (❙¬ p))›

text ‹Nowhere-or-twice says that if formula p holds somewhere, then it holds in at least two distinct worlds.›
text ‹(We ignore de Bruijn complications and only instantiate with closed formulas.)›

abbreviation ‹nowhere_or_twice p ≡
  (❙◇ p) ❙⟶
  (❙◇ (❙↓ (❙◇ (❙↓ (
    (❙@ (❙#1) p) ❙∧
    (❙@ (❙#0) p) ❙∧
    ❙¬ (❙@ (❙#0) (❙∙(❙#1))))))))›

text ‹Finite unions of arithmetic progressions are either empty or infinite.›

lemma fin_arith_nowhere_or_twice:
  assumes ‹fin_arith U›
  shows ‹U = {} ∨ (∃x y. x ∈ U ∧ y ∈ U ∧ x ≠ y)›
  using assms arith_ne_infinite unfolding fin_arith_def
  by (metis infinite_int_iff_unbounded less_le_not_le)

text ‹So nowhere-or-twice holds for all admissible propositions.›

lemma nowhere_or_twice_admissible: ‹(my_model, x) ⊨ ❙∀ (nowhere_or_twice (❙⋅(❙#0)))›
  unfolding my_model_def my_gframe_def unfolds Pss_def
  using fin_arith_nowhere_or_twice by simp

text ‹However, propositional quantification lets us form a singleton.›

abbreviation ‹singleton x ≡ ❙∀( ❙@(❙○x) (❙⋅(❙#0)) ❙⟶ ❙⋅(❙#0) )›

lemma singleton: ‹((my_model, x) ⊨ singleton y) ⟷ x = y›
  unfolding my_model_def my_gframe_def unfolds Pss_def
  using fin_arith_Inter_singleton by auto

lemma fin_arith_distinguish':
  ‹∀P. fin_arith P ⟶ y ∈ P ⟶ v ∈ P ⟹ v ≠ w ⟹ ∃P. y ∈ P ∧ fin_arith P ∧ w ∉ P›
  by (metis disjoint_iff fin_arith_distinguish)

text ‹The singleton does not hold nowhere-or-twice.›

lemma not_nowhere_or_twice_singleton: ‹¬ (my_model, x) ⊨ nowhere_or_twice (singleton y)›
  unfolding my_model_def my_gframe_def unfolds Pss_def
  using fin_arith_distinguish' by auto

text ‹So we cannot always eliminate a quantifier with a non-quantifier-free formula.›
  
theorem counter:
  shows ‹¬ (my_model, x) ⊨ ❙∀ (nowhere_or_twice (❙⋅(❙#0))) ❙⟶ nowhere_or_twice (singleton y)›
  using nowhere_or_twice_admissible not_nowhere_or_twice_singleton
  by (meson semantics.simps(3,4))

end