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› (‹⟦_⟧›) where
  ‹⟦_⟧ ❙⊥ ⟷ False›
| ‹⟦I⟧ (❙‡P) ⟷ I P›
| ‹⟦I⟧ (p ❙⟶ q) ⟷ ⟦I⟧ p ⟶ ⟦I⟧ q›

section ‹Calculus›

inductive Calculus :: ‹'p fm list ⇒ 'p fm list ⇒ bool› (‹_ ⊢⇩S _› [50, 50] 50) where
  Axiom [intro]: ‹p # A ⊢⇩S p # B›
| FlsL [intro]: ‹❙⊥ # A ⊢⇩S B›
| FlsR [dest]: ‹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 [elim]: ‹A ⊢⇩S p # B ⟹ p # C ⊢⇩S D ⟹ A @ C ⊢⇩S B @ D›
| WeakenL: ‹A ⊢⇩S B ⟹ set A ⊆ set A' ⟹ A' ⊢⇩S B›
| WeakenR: ‹A ⊢⇩S B ⟹ set B ⊆ set B' ⟹ A ⊢⇩S B'›

lemma Boole: ‹❙¬ p # A ⊢⇩S [] ⟹ A ⊢⇩S [p]›
  by (metis Axiom Cut ImpR WeakenR append_self_conv2 self_append_conv set_subset_Cons)

section ‹Soundness›

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

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

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

section ‹Maximal Consistent Sets›

definition consistent :: ‹'p fm set ⇒ bool› where
  ‹consistent S ≡ ∄S'. set S' ⊆ S ∧ S' ⊢⇩S [❙⊥]›

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

interpretation Derivations_MCS_Cut ‹λA p. A ⊢⇩S [p]› consistent ‹❙⊥›
proof
  fix A B and p :: ‹'p fm›
  assume ‹A ⊢⇩S [p]› ‹set A ⊆ set B›
  then show ‹B ⊢⇩S [p]›
    using WeakenL by blast
next
  fix S :: ‹'p fm set›
  show ‹consistent S ⟷ (∄S'. set S' ⊆ S ∧ S' ⊢⇩S [❙⊥])›
    unfolding consistent_def ..
next
  fix A and p :: ‹'p fm›
  assume ‹p ∈ set A›
  then show ‹A ⊢⇩S [p]›
    by (metis Axiom WeakenL set_ConsD subsetI)
next
  fix A B and p q :: ‹'p fm›
  assume ‹A ⊢⇩S [p]› ‹p # B ⊢⇩S [q]›
  then show ‹A @ B ⊢⇩S [q]›
    using Cut by fastforce
qed

section ‹Truth Lemma›

abbreviation hmodel :: ‹'p fm set ⇒ 'p model› where
  ‹hmodel H ≡ λP. ❙‡P ∈ H›

fun semics :: ‹'p model ⇒ ('p model ⇒ 'p fm ⇒ bool) ⇒ 'p fm ⇒ bool› where
  ‹semics _ _ ❙⊥ ⟷ False›
| ‹semics I _ (❙‡P) ⟷ I P›
| ‹semics I rel (p ❙⟶ q) ⟷ rel I p ⟶ rel I q›

fun rel :: ‹'p fm set ⇒ 'p model ⇒ 'p fm ⇒ bool› where
  ‹rel H _ p = (p ∈ H)›

theorem Hintikka_model':
  assumes ‹⋀p. semics (hmodel H) (rel H) p ⟷ p ∈ H›
  shows ‹p ∈ H ⟷ ⟦hmodel H⟧ 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[of x] by (cases x) simp_all
qed

lemma Hintikka_Extend:
  assumes ‹consistent H› ‹maximal H›
  shows ‹semics (hmodel H) (rel H) p ⟷ p ∈ H›
proof (cases p)
  case Fls
  have ‹❙⊥ ∉ H›
    using assms MCS_derive consistent_def by blast
  then show ?thesis
    using Fls by simp
next
  case (Imp p q)
  have ‹A ⊢⇩S [q] ⟹ A ⊢⇩S [p ❙⟶ q]› for A
    by (meson ImpR WeakenL set_subset_Cons)
  moreover have ‹p # A ⊢⇩S [❙⊥] ⟹ A ⊢⇩S [p ❙⟶ q]› for A
    by (meson FlsR ImpR WeakenR set_subset_Cons)
  moreover have ‹A ⊢⇩S [p ❙⟶ q] ⟹ B ⊢⇩S [p] ⟹ A @ B ⊢⇩S [q]› for A B
    using Cut by (metis Axiom ImpL append_Nil append_Nil2)
  ultimately have ‹(p ∈ H ⟶ q ∈ H) ⟷ p ❙⟶ q ∈ H›
    using assms MCS_derive MCS_derive_fls Axiom
    by (metis append_Cons append_Nil insert_subset list.simps(15))
  then show ?thesis
    using Imp by simp
qed simp

interpretation Truth_No_Saturation consistent semics semantics ‹λH. {hmodel H}› rel
proof
  fix p and M :: ‹'p model›
  show ‹⟦M⟧ p ⟷ semics M semantics p›
    by (induct p) auto
next
  fix p and H :: ‹'p fm set› and M :: ‹'p model›
  assume ‹∀M ∈ {hmodel H}. ∀p. semics M (rel H) p ⟷ rel H M p› ‹M ∈ {hmodel H}›
  then show ‹⟦M⟧ p ⟷ rel H M p›
    using Hintikka_model' by auto
next
  fix H :: ‹'p fm set›
  assume ‹consistent H› ‹maximal H›
  then show ‹∀M ∈ {hmodel H}. ∀p. semics M (rel H) p ⟷ rel H M p›
    using Hintikka_Extend by auto
qed

section ‹Completeness›

theorem strong_completeness:
  assumes ‹∀M :: 'p model. (∀q ∈ X. ⟦M⟧ q) ⟶ ⟦M⟧ 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 ⊆ X ∧ ❙¬ p # A ⊢⇩S []›
    using Boole by blast
  then have ‹∄A. set A ⊆ X ∧ ❙¬ p # A ⊢⇩S [❙⊥]›
    by fast
  then have *: ‹∄A. set A ⊆ {❙¬ p} ∪ X ∧ A ⊢⇩S [❙⊥]›
    using derive_split1 by blast

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

  have ‹consistent ?S›
    unfolding consistent_def using * by blast
  then have ‹consistent ?H› ‹maximal ?H›
    using MCS_Extend' by blast+
  then have ‹p ∈ ?H ⟷ ⟦hmodel ?H⟧ p› for p
    using truth_lemma_no_saturation by fastforce
  then have ‹p ∈ ?S ⟶ ⟦hmodel ?H⟧ p› for p
    using Extend_subset by blast
  then have ‹⟦hmodel ?H⟧ (❙¬ p)› ‹∀q ∈ X. ⟦hmodel ?H⟧ q›
    by blast+
  moreover from this have ‹⟦hmodel ?H⟧ p›
    using assms(1) by blast
  ultimately show False
    by simp
qed

abbreviation valid :: ‹'p fm ⇒ bool› where
  ‹valid p ≡ ∀M. ⟦M⟧ 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