# 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)

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)›
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›

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›

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
next
case (Cons a A)
have ‹⊢⇩□ ❙□ i (a # A ❙↝ q) ❙⟶ ❙□ i a ❙⟶ ❙□ i (A ❙↝ q)›
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))›
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
```