Theory Example_Modal_Logic

(*
  Title:  Example Completeness Proof for System K
  Author: Asta Halkjær From
*)

chapter ‹Example: Modal Logic›

theory Example_Modal_Logic imports Derivations begin

section ‹Syntax›

datatype ('i, 'p) fm
  = Fls (‹❙⊥›)
  | Pro 'p (‹❙‡›)
  | Imp ‹('i, 'p) fm› ‹('i, 'p) fm› (infixr ‹❙⟶› 55)
  | Box 'i ‹('i, 'p) fm› (‹❙□›)

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

section ‹Semantics›

datatype ('i, 'p, 'w) model =
  Model (𝒲: ‹'w set›) (ℛ: ‹'i ⇒ 'w ⇒ 'w set›) (𝒱: ‹'w ⇒ 'p ⇒ bool›)

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

fun semantics :: ‹('i, 'p, 'w) ctx ⇒ ('i, 'p) fm ⇒ bool› (‹_ ⊨ _› [50, 50] 50) where
  ‹_ ⊨ ❙⊥ ⟷ False›
| ‹(M, w) ⊨ ❙‡P ⟷ 𝒱 M w P›
| ‹(M, w) ⊨ p ❙⟶ q ⟷ (M, w) ⊨ p ⟶ (M, w) ⊨ q›
| ‹(M, w) ⊨ ❙□ i p ⟷ (∀v ∈ 𝒲 M ∩ ℛ M i w. (M, v) ⊨ p)›

section ‹Calculus›

primrec eval :: ‹('p ⇒ bool) ⇒ (('i, 'p) fm ⇒ bool) ⇒ ('i, 'p) fm ⇒ bool› where
  ‹eval _ _ ❙⊥ = False›
| ‹eval g _ (❙‡P) = g P›
| ‹eval g h (p ❙⟶ q) = (eval g h p ⟶ eval g h q)›
| ‹eval _ h (❙□ i p) = h (❙□ i p)›

abbreviation ‹tautology p ≡ ∀g h. eval g h p›

inductive Calculus :: ‹('i, 'p) fm ⇒ bool› (‹⊢⇩□ _› [50] 50) where
  A1: ‹tautology p ⟹ ⊢⇩□ p›
| A2: ‹⊢⇩□ ❙□ i (p ❙⟶ q) ❙⟶ ❙□ i p ❙⟶ ❙□ i q›
| R1: ‹⊢⇩□ p ⟹ ⊢⇩□ p ❙⟶ q ⟹ ⊢⇩□ q›
| R2: ‹⊢⇩□ p ⟹ ⊢⇩□ ❙□ i p›

primrec imply :: ‹('i, 'p) fm list ⇒ ('i, 'p) fm ⇒ ('i, 'p) fm› (infixr ‹❙↝› 56) where
  ‹([] ❙↝ p) = p›
| ‹(q # A ❙↝ p) = (q ❙⟶ A ❙↝ p)›

abbreviation Calculus_assms (‹_ ⊢⇩□ _› [50, 50] 50) where
  ‹A ⊢⇩□ p ≡ ⊢⇩□ A ❙↝ p›

section ‹Soundness›

lemma eval_semantics: ‹eval (g w) (λq. (Model W r g, w) ⊨ q) p = ((Model W r g, w) ⊨ p)›
  by (induct p) simp_all

lemma tautology:
  assumes ‹tautology p›
  shows ‹(M, w) ⊨ p›
proof -
  from assms have ‹eval (g w) (λq. (Model W r g, w) ⊨ q) p› for W g r
    by simp
  then have ‹(Model W r g, w) ⊨ p› for W g r
    using eval_semantics by fast
  then show ‹(M, w) ⊨ p›
    by (metis model.exhaust)
qed

theorem soundness:
  assumes ‹⋀M w p. A p ⟹ w ∈ 𝒲 M ⟹ (M, w) ⊨ p›
  shows ‹⊢⇩□ p ⟹ w ∈ 𝒲 M ⟹ (M, w) ⊨ p›
  by (induct p arbitrary: w rule: Calculus.induct) (auto simp: assms tautology)

section ‹Admissible rules›

lemma K_imply_head: ‹p # A ⊢⇩□ p›
proof -
  have ‹tautology (p # A ❙↝ p)›
    by (induct A) simp_all
  then show ?thesis
    using A1 by blast
qed

lemma K_imply_Cons:
  assumes ‹A ⊢⇩□ q›
  shows ‹p # A ⊢⇩□ q›
proof -
  have ‹⊢⇩□ (A ❙↝ q ❙⟶ p # A ❙↝ q)›
    by (simp add: A1)
  with R1 assms show ?thesis .
qed

lemma K_right_mp:
  assumes ‹A ⊢⇩□ p› ‹A ⊢⇩□ p ❙⟶ q›
  shows ‹A ⊢⇩□ q›
proof -
  have ‹tautology (A ❙↝ p ❙⟶ A ❙↝ (p ❙⟶ q) ❙⟶ A ❙↝ q)›
    by (induct A) simp_all
  with A1 have ‹⊢⇩□ A ❙↝ p ❙⟶ A ❙↝ (p ❙⟶ q) ❙⟶ A ❙↝ q› .
  then show ?thesis
    using assms R1 by blast
qed

lemma deduct1: ‹A ⊢⇩□ p ❙⟶ q ⟹ p # A ⊢⇩□ q›
  by (meson K_right_mp K_imply_Cons K_imply_head)

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

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

lemma K_ImpI: ‹p # A ⊢⇩□ q ⟹ A ⊢⇩□ p ❙⟶ q›
  by (metis imply.simps imply_append imply_swap_append)

lemma imply_mem [simp]: ‹p ∈ set A ⟹ A ⊢⇩□ p›
  using K_imply_head K_imply_Cons by (induct A) fastforce+

lemma add_imply [simp]: ‹⊢⇩□ q ⟹ A ⊢⇩□ q›
  using K_imply_head R1 by auto

lemma K_imply_weaken: ‹A ⊢⇩□ q ⟹ set A ⊆ set A' ⟹ A' ⊢⇩□ q›
  by (induct A arbitrary: q) (simp, metis K_right_mp K_ImpI imply_mem insert_subset list.set(2))

lemma K_Boole:
  assumes ‹(❙¬ p) # A ⊢⇩□ ❙⊥›
  shows ‹A ⊢⇩□ p›
proof -
  have ‹A ⊢⇩□ ❙¬ ❙¬ p›
    using assms K_ImpI by blast
  moreover have ‹tautology (A ❙↝ ❙¬ ❙¬ p ❙⟶ A ❙↝ p)›
    by (induct A) simp_all
  then have ‹⊢⇩□ (A ❙↝ ❙¬ ❙¬ p ❙⟶ A ❙↝ p)›
    using A1 by blast
  ultimately show ?thesis
    using R1 by blast
qed

lemma K_distrib_K_imp:
  assumes ‹⊢⇩□ ❙□ i (A ❙↝ q)›
  shows ‹map (❙□ i) A ⊢⇩□ ❙□ i q›
proof -
  have ‹⊢⇩□ ❙□ i (A ❙↝ q) ❙⟶ map (❙□ i) A ❙↝ ❙□ i q›
  proof (induct A)
    case Nil
    then show ?case
      by (simp add: A1)
  next
    case (Cons a A)
    have ‹⊢⇩□ ❙□ i (a # A ❙↝ q) ❙⟶ ❙□ i a ❙⟶ ❙□ i (A ❙↝ q)›
      by (simp add: A2)
    moreover have
      ‹⊢⇩□ ((❙□ i (a # A ❙↝ q) ❙⟶ ❙□ i a ❙⟶ ❙□ i (A ❙↝ q)) ❙⟶
        (❙□ i (A ❙↝ q) ❙⟶ map (❙□ i) A ❙↝ ❙□ i q) ❙⟶
        (❙□ i (a # A ❙↝ q) ❙⟶ ❙□ i a ❙⟶ map (❙□ i) A ❙↝ ❙□ i q))›
      by (simp add: A1)
    ultimately have ‹⊢⇩□ ❙□ i (a # A ❙↝ q) ❙⟶ ❙□ i a ❙⟶ map (❙□ i) A ❙↝ ❙□ i q›
      using Cons R1 by blast
    then show ?case
      by simp
  qed
  then show ?thesis
    using assms R1 by blast
qed

interpretation Derivations Calculus_assms
proof
  fix A B and p :: ‹('i, 'p) fm›
  assume ‹⊢⇩□ A ❙↝ p› ‹set A ⊆ set B›
  then show ‹⊢⇩□ B ❙↝ p›
    using K_imply_weaken by blast
qed

section ‹Maximal Consistent Sets›

definition consistent :: ‹('i, 'p) fm set ⇒ bool› where
  ‹consistent S ≡ ∄S'. set S' ⊆ S ∧ S' ⊢⇩□ ❙⊥›

interpretation MCS_No_Saturation consistent
proof
  fix S S' :: ‹('i, 'p) fm set›
  assume ‹consistent S› ‹S' ⊆ S›
  then show ‹consistent S'›
    unfolding consistent_def by fast
next
  fix S :: ‹('i, 'p) fm set›
  assume ‹¬ consistent S›
  then show ‹∃S' ⊆ S. finite S' ∧ ¬ consistent S'›
    unfolding consistent_def by blast
next
  show ‹infinite (UNIV :: ('i, 'p) fm set)›
    using infinite_UNIV_size[of ‹λp. p ❙⟶ p›] by simp
qed

interpretation Derivations_MCS_Cut Calculus_assms consistent ‹❙⊥›
proof
  fix S :: ‹('i, 'p) fm set›
  show ‹consistent S = (∄S'. set S' ⊆ S ∧ S' ⊢⇩□ ❙⊥)›
    unfolding consistent_def ..
next
  fix A and p :: ‹('i, 'p) fm›
  assume ‹p ∈ set A›
  then show ‹A ⊢⇩□ p›
    by (metis K_imply_head K_imply_weaken Un_upper2 set_append split_list_first)
next
  fix A B and p q :: ‹('i, 'p) fm›
  assume ‹A ⊢⇩□ p› ‹p # B ⊢⇩□ q›
  then show ‹A @ B ⊢⇩□ q›
    by (metis K_imply_head K_right_mp R1 imply.simps(2) imply_append)
qed

lemma exists_finite_inconsistent:
  assumes ‹¬ consistent ({❙¬ p} ∪ V)›
  obtains W where ‹{❙¬ p} ∪ W ⊆ {❙¬ p} ∪ V› ‹(❙¬ p) ∉ W› ‹finite W› ‹¬ consistent ({❙¬ p} ∪ W)›
proof -
  obtain W' where W': ‹set W' ⊆ {❙¬ p} ∪ V› ‹W' ⊢⇩□ ❙⊥›
    using assms unfolding consistent_def by blast
  let ?S = ‹removeAll (❙¬ p) W'›
  have ‹¬ consistent ({❙¬ p} ∪ set ?S)›
    unfolding consistent_def using W'(2) by auto
  moreover have ‹finite (set ?S)›
    by blast
  moreover have ‹{❙¬ p} ∪ set ?S ⊆ {❙¬ p} ∪ V›
    using W'(1) by auto
  moreover have ‹(❙¬ p) ∉ set ?S›
    by simp
  ultimately show ?thesis
    by (meson that)
qed

lemma MCS_consequent:
  assumes ‹consistent V› ‹maximal V› ‹p ❙⟶ q ∈ V› ‹p ∈ V›
  shows ‹q ∈ V›
  using assms MCS_derive
  by (metis (mono_tags, lifting) K_imply_Cons K_imply_head K_right_mp insert_subset list.simps(15))

theorem deriv_in_maximal:
  assumes ‹consistent V› ‹maximal V› ‹⊢⇩□ p›
  shows ‹p ∈ V›
  using assms R1 derive_split1 unfolding consistent_def maximal_def by (metis imply.simps(2))

theorem exactly_one_in_maximal:
  assumes ‹consistent V› ‹maximal V›
  shows ‹p ∈ V ⟷ (❙¬ p) ∉ V›
  using assms MCS_derive MCS_derive_fls by (metis K_Boole K_imply_Cons K_imply_head K_right_mp)

section ‹Truth Lemma›

abbreviation val :: ‹('i, 'p) fm set ⇒ 'p ⇒ bool› where
  ‹val V P ≡ ❙‡P ∈ V›

abbreviation known :: ‹('i, 'p) fm set ⇒ 'i ⇒ ('i, 'p) fm set› where
  ‹known V i ≡ {p. ❙□ i p ∈ V}›

abbreviation reach :: ‹'i ⇒ ('i, 'p) fm set ⇒ ('i, 'p) fm set set› where
  ‹reach i V ≡ {W. known V i ⊆ W}›

abbreviation mcss :: ‹('i, 'p) fm set set› where
  ‹mcss ≡ {W. consistent W ∧ maximal W}›

abbreviation canonical :: ‹('i, 'p, ('i, 'p) fm set) model› where
  ‹canonical ≡ Model mcss reach val›

fun semics ::
  ‹('i, 'p, 'w) ctx ⇒ (('i, 'p, 'w) ctx ⇒ ('i, 'p) fm ⇒ bool) ⇒ ('i, 'p) fm ⇒ bool› where
  ‹semics _ _ ❙⊥ ⟷ False›
| ‹semics (M, w) _ (❙‡P) ⟷ 𝒱 M w P›
| ‹semics (M, w) rel (p ❙⟶ q) ⟷ rel (M, w) p ⟶ rel (M, w) q›
| ‹semics (M, w) rel (❙□ i p) ⟷ (∀v ∈ 𝒲 M ∩ ℛ M i w. rel (M, v) p)›

fun rel :: ‹('i, 'p) fm set ⇒ ('i, 'p, ('i, 'p) fm set) ctx ⇒ ('i, 'p) fm ⇒ bool› where
  ‹rel _ (_, w) p = (p ∈ w)›

lemma Hintikka_model':
  fixes V :: ‹('i, 'p) fm set›
  assumes ‹⋀(V :: ('i, 'p) fm set) p. V ∈ mcss ⟹ semics (canonical, V) (rel H) p ⟷ p ∈ V›
  shows ‹V ∈ mcss ⟹ (canonical, V) ⊨ p ⟷ p ∈ V›
proof (induct p arbitrary: V rule: wf_induct[where r=‹measure size›])
  case 1
  then show ?case ..
next
  case (2 x)
  then show ?case
    using assms[of V x] by (cases x) auto
qed

lemma maximal_extension:
  assumes ‹consistent V›
  shows ‹∃W. V ⊆ W ∧ consistent W ∧ maximal W›
  using assms MCS_Extend' Extend_subset by meson

lemma Hintikka_canonical:
  assumes ‹V ∈ mcss›
  shows ‹semics (canonical, V) (rel H) p ⟷ rel H (canonical, V) p›
proof (cases p)
  case Fls
  have ‹❙⊥ ∉ V›
    using assms MCS_derive unfolding consistent_def by blast
  then show ?thesis
    using Fls by simp
next
  case (Imp p q)
  have ‹(p ∈ V ⟶ q ∈ V) ⟷ p ❙⟶ q ∈ V›
    using assms MCS_derive MCS_derive_fls MCS_consequent
    by (metis (no_types, lifting) CollectD K_Boole K_ImpI K_imply_Cons)
  then show ?thesis
    using Imp by simp
next
  case (Box i p)
  have ‹(∀v ∈ mcss ∩ reach i V. p ∈ v) = (❙□ i p ∈ V)›
  proof
    assume ‹❙□ i p ∈ V›
    then show ‹∀v ∈ mcss ∩ reach i V. p ∈ v›
      by auto
  next
    assume *: ‹∀v ∈ mcss ∩ reach i V. p ∈ v›

    have ‹consistent V› ‹maximal V›
      using ‹V ∈ mcss› by blast+

    have ‹¬ consistent ({❙¬ p} ∪ known V i)›
    proof
      assume ‹consistent ({❙¬ p} ∪ known V i)›
      then obtain W where W: ‹{❙¬ p} ∪ known V i ⊆ W› ‹consistent W› ‹maximal W›
        using ‹V ∈ mcss› maximal_extension by blast
      then have ‹(canonical, W) ⊨ ❙¬ p›
        using "*" exactly_one_in_maximal by auto
      moreover have ‹W ∈ reach i V› ‹W ∈ mcss›
        using W by simp_all
      ultimately have ‹(canonical, V) ⊨ ❙¬ ❙□ i p›
        by auto
      then show False
        using * W(1) ‹W ∈ mcss› exactly_one_in_maximal by auto
    qed

    then obtain W where W:
      ‹{❙¬ p} ∪ W ⊆ {❙¬ p} ∪ known V i› ‹(❙¬ p) ∉ W› ‹finite W› ‹¬ consistent ({❙¬ p} ∪ W)›
      using exists_finite_inconsistent by metis

    obtain L where L: ‹set L = W›
      using ‹finite W› finite_list by blast
    then have ‹⊢⇩□ L ❙↝ p›
      using W(4) derive_split1 unfolding consistent_def by (meson K_Boole K_imply_weaken)
    then have ‹⊢⇩□ ❙□ i (L ❙↝ p)›
      using R2 by fast
    then have ‹map (❙□ i) L ⊢⇩□ ❙□ i p›
      using K_distrib_K_imp by fast
    then have ‹(map (❙□ i) L ❙↝ ❙□ i p) ∈ V›
      using deriv_in_maximal ‹V ∈ mcss› by blast
    then show ‹❙□ i p ∈ V›
      using L W(1-2)
    proof (induct L arbitrary: W)
      case (Cons a L)
      then have ‹❙□ i a ∈ V›
        by auto
      then have ‹(map (❙□ i) L ❙↝ ❙□ i p) ∈ V›
        using Cons(2) ‹consistent V› ‹maximal V› MCS_consequent by auto
      then show ?case
        using Cons by auto
    qed simp
  qed
  then show ?thesis
    using Box by simp
qed simp

interpretation Truth_No_Saturation consistent semics semantics
  ‹λ_. {(canonical, V) |V. V ∈ mcss}› rel
proof
  fix p and M :: ‹('i, 'p, ('i, 'p) fm set) ctx›
  show ‹(M ⊨ p) = semics M semantics p›
    by (cases M, induct p) simp_all
next
  fix p and H :: ‹('i, 'p) fm set› and M :: ‹('i, 'p, ('i, 'p) fm set) ctx›
  assume ‹∀M∈{(canonical, V) |V. V ∈ mcss}. ∀p. semics M (rel H) p = rel H M p›
    ‹M ∈ {(canonical, V) |V. V ∈ mcss}›
  then show ‹(M ⊨ p) = rel H M p›
    using Hintikka_model'[of H _ p] by auto
next
  fix H :: ‹('i, 'p) fm set›
  assume ‹consistent H› ‹maximal H›
  then show ‹∀M∈{(canonical, V) |V. V ∈ mcss}. ∀p. semics M (rel H) p = rel H M p›
    using Hintikka_canonical by blast
qed

lemma Truth_lemma:
  assumes ‹consistent V› ‹maximal V›
  shows ‹(canonical, V) ⊨ p ⟷ p ∈ V›
  using assms truth_lemma_no_saturation by fastforce

lemma canonical_model:
  assumes ‹consistent S› ‹p ∈ S›
  defines ‹V ≡ Extend S› and ‹M ≡ canonical›
  shows ‹(M, V) ⊨ p› ‹consistent V› ‹maximal V›
proof -
  have ‹consistent V›
    using ‹consistent S› unfolding V_def using consistent_Extend by auto
  have ‹maximal V›
    unfolding V_def using maximal_Extend by blast
  { fix x
    assume ‹x ∈ S›
    then have ‹x ∈ V›
      unfolding V_def using Extend_subset by blast
    then have ‹(M, V) ⊨ x›
      unfolding M_def using Truth_lemma ‹consistent V› ‹maximal V› by blast }
  then show ‹(M, V) ⊨ p›
    using ‹p ∈ S› by blast+
  show ‹consistent V› ‹maximal V›
    by fact+
qed

section ‹Completeness›

theorem strong_completeness:
  assumes ‹∀M :: ('i, 'p, ('i, 'p) fm set) model. ∀w ∈ 𝒲 M.
    (∀q ∈ X. (M, w) ⊨ q) ⟶ (M, w) ⊨ p›
  shows ‹∃A. set A ⊆ X ∧ A ⊢⇩□ p›
proof (rule ccontr)
  assume ‹∄A. set A ⊆ X ∧ A ⊢⇩□ p›
  then have *: ‹∀A. set A ⊆ X ⟶ ¬ (❙¬ p) # A ⊢⇩□ ❙⊥›
    using K_Boole by blast

  let ?S = ‹{❙¬ p} ∪ X›
  let ?V = ‹Extend ?S›

  have ‹consistent ?S›
    using * derive_split1 unfolding consistent_def by meson
  then have ‹(canonical, ?V) ⊨ (❙¬ p)› ‹∀q ∈ X. (canonical, ?V) ⊨ q›
    using canonical_model by fastforce+
  moreover have ‹?V ∈ mcss›
    using ‹consistent ?S› maximal_Extend canonical_model(2) by blast
  ultimately have ‹(canonical, ?V) ⊨ p›
    using assms by simp
  then show False
    using ‹(canonical, ?V) ⊨ (❙¬ p)› by simp
qed

abbreviation valid :: ‹('i, 'p) fm ⇒ bool› where
  ‹valid p ≡ ∀(M :: ('i, 'p, ('i, 'p) fm set) model). ∀w ∈ 𝒲 M. (M, w) ⊨ p›

corollary completeness: ‹valid p ⟹ ⊢⇩□ p›
  using strong_completeness[where X=‹{}›] by simp

theorem main: ‹valid p ⟷ ⊢⇩□ p›
  using soundness completeness by meson

end