Theory Example_Propositional_SC

(*
  Title:  Example Completeness Proof for a Propositional Sequent Calculus
  Author: Asta Halkjær From
*)

chapter ‹Example: Propositional Sequent Calculus›

theory Example_Propositional_SC imports Derivations begin

section ‹Syntax›

datatype 'p fm
  = Fls (‹❙⊥›)
  | Pro 'p (‹❙⋅›)
  | Imp ‹'p fm› ‹'p fm› (infixr ‹❙⟶› 55)

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

section ‹Semantics›

type_synonym 'p model = ‹'p ⇒ bool›

fun semantics :: ‹'p model ⇒ 'p fm ⇒ bool› (infix ‹⊨⇩S› 50) where
  ‹_ ⊨⇩S ❙⊥ ⟷ False›
| ‹I ⊨⇩S ❙⋅P ⟷ I P›
| ‹I ⊨⇩S p ❙⟶ q ⟷ I ⊨⇩S p ⟶ I ⊨⇩S q›

section ‹Calculus›

inductive Calculus :: ‹'p fm list ⇒ 'p fm list ⇒ bool› (infix ‹⊢⇩S› 50) where
  Axiom [simp]: ‹p # A ⊢⇩S p # B›
| FlsL [simp]: ‹❙⊥ # A ⊢⇩S B›
| FlsR [elim]: ‹A ⊢⇩S ❙⊥ # B ⟹ A ⊢⇩S B›
| ImpL [intro]: ‹A ⊢⇩S p # B ⟹ q # A ⊢⇩S B ⟹ (p ❙⟶ q) # A ⊢⇩S B›
| ImpR [intro]: ‹p # A ⊢⇩S q # B ⟹ A ⊢⇩S (p ❙⟶ q) # B›
| Cut: ‹A ⊢⇩S [p] ⟹ p # A ⊢⇩S B ⟹ A ⊢⇩S B›
| WeakL: ‹A ⊢⇩S B ⟹ set A ⊆ set A' ⟹ A' ⊢⇩S B›
| WeakR: ‹A ⊢⇩S B ⟹ set B ⊆ set B' ⟹ A ⊢⇩S B'›

lemma Boole: ‹❙¬ p # A ⊢⇩S [] ⟹ A ⊢⇩S [p]›
  by (meson Axiom Cut ImpL ImpR WeakR set_subset_Cons)

section ‹Soundness›

theorem soundness: ‹A ⊢⇩S B ⟹ ∀q ∈ set A. I ⊨⇩S q ⟹ ∃p ∈ set B. I ⊨⇩S p›
  by (induct A B rule: Calculus.induct) auto

corollary soundness': ‹[] ⊢⇩S [p] ⟹ I ⊨⇩S p›
  using soundness by fastforce

corollary ‹¬ [] ⊢⇩S []›
  using soundness by fastforce

section ‹Maximal Consistent Sets›

definition consistent :: ‹'p fm set ⇒ bool› where
  ‹consistent S ≡ ∀A. set A ⊆ S ⟶ ¬ A ⊢⇩S [❙⊥]›

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

interpretation Derivations_Cut_MCS consistent ‹λA p. A ⊢⇩S [p]›
proof
  fix A B and p :: ‹'p fm›
  assume ‹A ⊢⇩S [p]› ‹set A = set B›
  then show ‹B ⊢⇩S [p]›
    using WeakL by blast
next
  fix S :: ‹'p fm set›
  show ‹consistent S ⟷ (∀A. set A ⊆ S ⟶ (∃q. ¬ A ⊢⇩S [q]))›
    unfolding consistent_def using Cut FlsL by blast
next
  fix A and p :: ‹'p fm›
  assume ‹p ∈ set A›
  then show ‹A ⊢⇩S [p]›
    by (metis Axiom WeakL set_ConsD subsetI)
next
  fix A B and p q :: ‹'p fm›
  assume ‹A ⊢⇩S [p]› ‹p # B ⊢⇩S [q]›
  then have ‹A @ B ⊢⇩S [p]› ‹p # A @ B ⊢⇩S [q]›
    by (fastforce intro: WeakL)+
  then show ‹A @ B ⊢⇩S [q]›
    using Cut by blast
qed

interpretation Derivations_Bot consistent ‹λA p. A ⊢⇩S [p]› ‹❙⊥›
proof
  show ‹⋀A r. A ⊢⇩S [❙⊥] ⟹ A ⊢⇩S [r]›
    using Cut FlsL by blast
qed

interpretation Derivations_Imp consistent ‹λA p. A ⊢⇩S [p]› ‹λp q. p ❙⟶ q›
proof
  show ‹⋀A p q. A ⊢⇩S [p] ⟹ A ⊢⇩S [p ❙⟶ q] ⟹ A ⊢⇩S [q]›
    by (meson Axiom Cut ImpL)
qed fast+

section ‹Truth Lemma›

abbreviation canonical :: ‹'p fm set ⇒ 'p model› (‹ℳ⇩S›) where
  ‹ℳ⇩S(S) ≡ λP. ❙⋅P ∈ S›

fun semics :: ‹'p model ⇒ ('p model ⇒ 'p fm ⇒ bool) ⇒ 'p fm ⇒ bool›
  (‹_ ⟦_⟧⇩S _› [55, 0, 55] 55) where
  ‹_ ⟦_⟧⇩S ❙⊥ ⟷ False›
| ‹I ⟦_⟧⇩S ❙⋅P ⟷ I P›
| ‹I ⟦ℛ⟧⇩S p ❙⟶ q ⟷ ℛ I p ⟶ ℛ I q›

fun rel :: ‹'p fm set ⇒ 'p model ⇒ 'p fm ⇒ bool› (‹ℛ⇩S›) where
  ‹ℛ⇩S(S) _ p ⟷ p ∈ S›

theorem saturated_model:
  assumes ‹⋀p. ∀M∈{ℳ⇩S(S)}. M ⟦ℛ⇩S(S)⟧⇩S p = ℛ⇩S(S) M p› ‹M ∈ {ℳ⇩S(S)}›
  shows ‹ℛ⇩S(S) M p ⟷ M ⊨⇩S p›
proof (induct p rule: wf_induct[where r=‹measure size›])
  case 1
  then show ?case ..
next
  case (2 x)
  then show ?case
    using assms(1)[of x] assms(2) by (cases x) simp_all
qed

theorem saturated_MCS:
  assumes ‹MCS S› ‹M ∈ {ℳ⇩S(S)}›
  shows ‹M ⟦ℛ⇩S(S)⟧⇩S p ⟷ ℛ⇩S(S) M p›
  using assms by (cases p) auto

interpretation Truth_No_Witness semics semantics ‹λS. {ℳ⇩S(S)}› rel consistent
proof
  fix p and M :: ‹'p model›
  show ‹(M ⊨⇩S p) = M ⟦(⊨⇩S)⟧⇩S p›
    by (induct p) auto
qed (use saturated_model saturated_MCS in blast)+

section ‹Completeness›

theorem strong_completeness:
  assumes ‹∀M. (∀q ∈ X. M ⊨⇩S q) ⟶ M ⊨⇩S p›
  shows ‹∃A. set A ⊆ X ∧ A ⊢⇩S [p]›
proof (rule ccontr)
  assume ‹∄A. set A ⊆ X ∧ A ⊢⇩S [p]›
  then have *: ‹∀A. set A ⊆ {❙¬ p} ∪ X ⟶ ¬ A ⊢⇩S [❙⊥]›
    using derive_split1 botE Boole FlsR by (metis (full_types) insert_is_Un subset_insert_iff)

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

  have ‹consistent ?X›
    unfolding consistent_def using * .
  then have ‹MCS ?S›
    using MCS_Extend' by blast
  then have ‹p ∈ ?S ⟷ ℳ⇩S ?S ⊨⇩S p› for p
    using truth_lemma by fastforce
  then have ‹p ∈ ?X ⟶ ℳ⇩S ?S ⊨⇩S p› for p
    using Extend_subset by blast
  then have ‹ℳ⇩S ?S ⊨⇩S ❙¬ p› ‹∀q ∈ X. ℳ⇩S ?S ⊨⇩S q›
    by blast+
  moreover from this have ‹ℳ⇩S ?S ⊨⇩S p›
    using assms(1) by blast
  ultimately show False
    by simp
qed

abbreviation valid :: ‹'p fm ⇒ bool› where
  ‹valid p ≡ ∀M. M ⊨⇩S p›

theorem completeness:
  assumes ‹valid p›
  shows ‹[] ⊢⇩S [p]›
  using assms strong_completeness[where X=‹{}›] by auto

theorem main: ‹valid p ⟷ [] ⊢⇩S [p]›
  using completeness soundness' by blast

end