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: ‹'w set›) (R: ‹'i ⇒ 'w ⇒ 'w set›) (V: ‹'w ⇒ 'p ⇒ bool›)

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

fun semantics :: ‹('i, 'p, 'w) ctx ⇒ ('i, 'p) fm ⇒ bool› (infix ‹⊨⇩□› 50) where
  ‹_ ⊨⇩□ ❙⊥ ⟷ False›
| ‹(M, w) ⊨⇩□ ❙⋅P ⟷ V M w P›
| ‹(M, w) ⊨⇩□ p ❙⟶ q ⟷ (M, w) ⊨⇩□ p ⟶ (M, w) ⊨⇩□ q›
| ‹(M, w) ⊨⇩□ ❙□ i p ⟷ (∀v ∈ W M ∩ R 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 (infix ‹⊢⇩□› 50) where
  ‹A ⊢⇩□ p ≡ ⊢⇩□ A ❙↝ p›

section ‹Soundness›

lemma eval_semantics: ‹eval (g w) (λq. (Model Ws r g, w) ⊨⇩□ q) p = ((Model Ws 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 Ws r g, w) ⊨⇩□ q) p› for Ws g r
    by simp
  then have ‹(Model Ws r g, w) ⊨⇩□ p› for Ws g r
    using eval_semantics by fast
  then show ‹(M, w) ⊨⇩□ p›
    by (metis model.exhaust)
qed

theorem soundness: ‹⊢⇩□ p ⟹ w ∈ W M ⟹ (M, w) ⊨⇩□ p›
  by (induct p arbitrary: w rule: Calculus.induct) (auto simp: 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›
  using assms by (auto simp: A1 intro: R1)

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

section ‹Maximal Consistent Sets›

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

interpretation MCS_No_Witness_UNIV consistent
proof
  show ‹infinite (UNIV :: ('i, 'p) fm set)›
    using infinite_UNIV_size[of ‹λp. p ❙⟶ p›] by simp
qed (auto simp: consistent_def)

interpretation Derivations_Cut_MCS consistent 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
next
  fix S :: ‹('i, 'p) fm set›
  show ‹consistent S = (∀A. set A ⊆ S ⟶ (∃q. ¬ A ⊢⇩□ q))›
    unfolding consistent_def using K_Boole K_imply_Cons by blast
next
  fix A B and p q :: ‹('i, 'p) fm›
  assume ‹A ⊢⇩□ p› ‹p # B ⊢⇩□ q›
  then show ‹A @ B ⊢⇩□ q›
    by (metis K_right_mp add_imply imply.simps(2) imply_append)
qed simp

interpretation Derivations_Bot consistent Calculus_assms ‹❙⊥›
proof
  show ‹⋀A r. A ⊢⇩□ ❙⊥ ⟹ A ⊢⇩□ r›
    using K_Boole K_imply_Cons by blast
qed

interpretation Derivations_Imp consistent Calculus_assms ‹λp q. p ❙⟶ q›
proof
  show ‹⋀A p q. p # A ⊢⇩□ q ⟹ A ⊢⇩□ p ❙⟶ q›
    using K_ImpI by blast
  show ‹⋀A p q. A ⊢⇩□ p ⟹ A ⊢⇩□ p ❙⟶ q ⟹ A ⊢⇩□ q›
    using K_right_mp by blast
qed

theorem deriv_in_maximal:
  assumes ‹consistent S› ‹maximal S› ‹⊢⇩□ p›
  shows ‹p ∈ S›
  using assms MCS_derive by fastforce

section ‹Truth Lemma›

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

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

abbreviation canonical :: ‹('i, 'p) fm set ⇒ ('i, 'p, ('i, 'p) fm set) ctx› (‹ℳ⇩□›) where
  ‹ℳ⇩□(S) ≡ (Model {S. MCS S} reach (λS P. ❙⋅P ∈ S), S)›

fun semics ::
  ‹('i, 'p, 'w) ctx ⇒ (('i, 'p, 'w) ctx ⇒ ('i, 'p) fm ⇒ bool) ⇒ ('i, 'p) fm ⇒ bool›
  (‹(_ ⟦_⟧⇩□ _)› [55, 0, 55] 55) where
  ‹_ ⟦_⟧⇩□ ❙⊥ ⟷ False›
| ‹(M, w) ⟦_⟧⇩□ ❙⋅P ⟷ V M w P›
| ‹(M, w) ⟦ℛ⟧⇩□ p ❙⟶ q ⟷ ℛ (M, w) p ⟶ ℛ (M, w) q›
| ‹(M, w) ⟦ℛ⟧⇩□ ❙□ i p ⟷ (∀v ∈ W M ∩ R M i w. ℛ (M, v) p)›

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

theorem saturated_model:
  fixes S :: ‹('i, 'p) fm set›
  assumes ‹⋀(S :: ('i, 'p) fm set) p. MCS S ⟹ ℳ⇩□(S) ⟦ℛ⇩□(S')⟧⇩□ p ⟷ p ∈ S›
  shows ‹MCS S ⟹ ℳ⇩□(S) ⊨⇩□ p ⟷ p ∈ S›
proof (induct p arbitrary: S rule: wf_induct[where r=‹measure size›])
  case 1
  then show ?case ..
next
  case (2 x)
  then show ?case
    using assms[of S x] by (cases x) auto
qed

theorem saturated_MCS:
  assumes ‹MCS S›
  shows ‹ℳ⇩□(S) ⟦ℛ⇩□(S')⟧⇩□ p ⟷ ℛ⇩□(S')  (ℳ⇩□(S)) p›
proof (cases p)
  case Fls
  have ‹❙⊥ ∉ S›
    using assms MCS_derive unfolding consistent_def by blast
  then show ?thesis
    using Fls by simp
next
  case (Imp p q)
  then show ?thesis
    using assms by auto
next
  case (Box i p)
  have ‹(∀S' ∈ reach i S. p ∈ S') ⟷ ❙□ i p ∈ S›
  proof
    assume ‹❙□ i p ∈ S›
    then show ‹∀S' ∈ reach i S. p ∈ S'›
      by auto
  next
    assume *: ‹∀S' ∈ reach i S. p ∈ S'›
    have ‹¬ consistent ({❙¬ p} ∪ known S i)›
    proof
      assume ‹consistent ({❙¬ p} ∪ known S i)›
      then obtain S' where S': ‹{❙¬ p} ∪ known S i ⊆ S'› ‹MCS S'›
        using ‹MCS S› MCS_Extend' Extend_subset by metis
      then show False
        using * MCS_impE MCS_bot by force
    qed
    then obtain A where A: ‹❙¬ p # A ⊢⇩□ ❙⊥› ‹set A ⊆ known S i›
      unfolding consistent_def using derive_split1 K_imply_Cons
      by (metis (no_types, lifting) insert_is_Un subset_insert)
    then have ‹⊢⇩□ A ❙↝ p›
      using K_Boole by blast
    then have ‹⊢⇩□ ❙□ i (A ❙↝ p)›
      using R2 by fast
    then have ‹map (❙□ i) A ⊢⇩□ ❙□ i p›
      using K_distrib_K_imp by fast
    then have ‹(map (❙□ i) A ❙↝ ❙□ i p) ∈ S›
      using deriv_in_maximal ‹MCS S› by blast
    then show ‹❙□ i p ∈ S›
      using A(2)
    proof (induct A)
      case (Cons a L)
      then have ‹❙□ i a ∈ S›
        by auto
      then have ‹(map (❙□ i) L ❙↝ ❙□ i p) ∈ S›
        using Cons(2) ‹MCS S› MCS_impE by auto
      then show ?case
        using Cons by simp
    qed simp
  qed
  then show ?thesis
    using Box by auto
qed simp

interpretation Truth_No_Witness semics semantics ‹λ_. {ℳ⇩□(S) |S. MCS S}› rel consistent
proof
  fix p and M :: ‹('i, 'p, ('i, 'p) fm set) ctx›
  show ‹(M ⊨⇩□ p) = M ⟦semantics⟧⇩□ p›
    by (cases M, induct p) simp_all
next
  fix p and S :: ‹('i, 'p) fm set› and M :: ‹('i, 'p, ('i, 'p) fm set) ctx›
  assume ‹∀p. ∀M∈{ℳ⇩□(S) |S. MCS S}. M ⟦ℛ⇩□(S)⟧⇩□ p ⟷ ℛ⇩□(S) M p› ‹M ∈ {ℳ⇩□(S) |S. MCS S}›
  then show ‹M ⊨⇩□ p ⟷ ℛ⇩□(S) M p›
    using saturated_model[of S _ p] by auto
next
  fix S :: ‹('i, 'p) fm set› and M :: ‹('i, 'p, ('i, 'p) fm set) ctx›
  assume ‹MCS S›
  then show ‹∀p. ∀M∈{ℳ⇩□(S) |S. MCS S}. M ⟦ℛ⇩□(S)⟧⇩□ p ⟷ ℛ⇩□(S) M p›
    using saturated_MCS by blast
qed

lemma Truth_lemma:
  assumes ‹MCS S›
  shows ‹ℳ⇩□(S) ⊨⇩□ p ⟷ p ∈ S›
  using assms truth_lemma by fastforce

section ‹Completeness›

theorem strong_completeness:
  assumes ‹∀M :: ('i, 'p, ('i, 'p) fm set) model. ∀w ∈ 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 ⊆ {❙¬ p} ∪ X ⟶ ¬ A ⊢⇩□ ❙⊥›
    using K_Boole botE by (metis derive_split1 insert_is_Un subset_insert)

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

  have ‹consistent ?X›
    using * unfolding consistent_def .
  then have ‹MCS ?S›
    using MCS_Extend' by blast
  moreover have ‹❙¬ p ∈ ?S› ‹X ⊆ ?S›
    using Extend_subset by fast+
  ultimately have ‹ℳ⇩□ ?S ⊨⇩□ (❙¬ p)› ‹∀q ∈ X. ℳ⇩□ ?S ⊨⇩□ q›
    using assms Truth_lemma by fast+
  then have ‹ℳ⇩□ ?S ⊨⇩□ p›
    using assms ‹MCS ?S› by simp
  then show False
    using ‹ℳ⇩□ ?S ⊨⇩□ (❙¬ p)› by simp
qed

abbreviation valid :: ‹('i, 'p) fm ⇒ bool› where
  ‹valid p ≡ ∀(M :: ('i, 'p, ('i, 'p) fm set) model). ∀w ∈ 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