Theory Example_Propositional_Tableau

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

chapter ‹Example: Propositional Tableau Calculus›

theory Example_Propositional_Tableau imports Refutations begin

section ‹Syntax›

datatype 'p fm
  = Pro 'p (‹❙‡›)
  | Neg ‹'p fm› (‹❙¬ _› [70] 70)
  | Imp ‹'p fm› ‹'p fm› (infixr ‹❙⟶› 55)

section ‹Semantics›

type_synonym 'p model = ‹'p ⇒ bool›

fun semantics :: ‹'p model ⇒ 'p fm ⇒ bool› (‹⟦_⟧›) where
  ‹⟦I⟧ (❙‡P) ⟷ I P›
| ‹⟦I⟧ (❙¬ p) ⟷ ¬ ⟦I⟧ p›
| ‹⟦I⟧ (p ❙⟶ q) ⟷ ⟦I⟧ p ⟶ ⟦I⟧ q›

section ‹Calculus›

inductive Calculus :: ‹'p fm list ⇒ bool› (‹⊢⇩T _› [50] 50) where
  Axiom [intro]: ‹⊢⇩T ❙‡P # ❙¬ ❙‡P # A›
| NegI [intro]: ‹⊢⇩T p # A ⟹ ⊢⇩T ❙¬ ❙¬ p # A›
| ImpP [intro]: ‹⊢⇩T ❙¬ p # A ⟹ ⊢⇩T q # A ⟹ ⊢⇩T (p ❙⟶ q) # A›
| ImpN [intro]: ‹⊢⇩T p # ❙¬ q # A ⟹ ⊢⇩T ❙¬ (p ❙⟶ q) # A›
| Weaken: ‹⊢⇩T A ⟹ set A ⊆ set B ⟹ ⊢⇩T B›

lemma Weaken2:
  assumes ‹⊢⇩T p # A› ‹⊢⇩T q # B›
  shows ‹⊢⇩T p # A @ B ∧ ⊢⇩T q # A @ B›
  using assms Weaken[where A=‹_ # _› and B=‹_ # A @ B›] by fastforce

section ‹Soundness›

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

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

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

section ‹Maximal Consistent Sets›

definition consistent :: ‹'p fm set ⇒ bool› where
  ‹consistent S ≡ ∄S'. set S' ⊆ S ∧ ⊢⇩T 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 Refutations_MCS Calculus consistent
proof
  fix A B :: ‹'p fm list›
  assume ‹⊢⇩T A› ‹set A ⊆ set B›
  then show ‹⊢⇩T B›
    using Weaken by meson
next
  fix S :: ‹'p fm set›
  show ‹consistent S ⟷ (∄S'. set S' ⊆ S ∧ ⊢⇩T S')›
    unfolding consistent_def ..
qed

section ‹Truth Lemma›

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

locale Hintikka =
  fixes H :: ‹'a fm set›
  assumes AxiomH: ‹⋀P. ❙‡P ∈ H ⟹ ❙¬ ❙‡P ∈ H ⟹ False›
    and NegIH: ‹⋀p. ❙¬ ❙¬ p ∈ H ⟹ p ∈ H›
    and ImpPH: ‹⋀p q. p ❙⟶ q ∈ H ⟹ ❙¬ p ∈ H ∨ q ∈ H›
    and ImpNH: ‹⋀p q. ❙¬ (p ❙⟶ q) ∈ H ⟹ p ∈ H ∧ ❙¬ q ∈ H›

lemma Hintikka_model:
  assumes ‹Hintikka H›
  shows ‹(p ∈ H ⟶ ⟦hmodel H⟧ p) ∧ (❙¬ p ∈ H ⟶ ¬ ⟦hmodel H⟧ p)›
  using assms by (induct p) (unfold Hintikka_def semantics.simps; blast)+

lemma MCS_Hintikka:
  assumes ‹consistent H› ‹maximal H›
  shows ‹Hintikka H›
proof
  fix P
  assume ‹❙‡P ∈ H› ‹❙¬ ❙‡P ∈ H›
  then have ‹set [❙‡P, ❙¬ ❙‡P] ⊆ H›
    by simp
  moreover have ‹⊢⇩T [❙‡P, ❙¬ ❙‡P]›
    by blast
  ultimately show False
    using assms unfolding consistent_def by blast
next
  fix p
  assume ‹❙¬ ❙¬ p ∈ H›
  then show ‹p ∈ H›
    using assms MCS_refute by blast
next
  fix p q
  assume *: ‹p ❙⟶ q ∈ H›
  show ‹❙¬ p ∈ H ∨ q ∈ H›
  proof (rule ccontr)
    assume ‹¬ (❙¬ p ∈ H ∨ q ∈ H)›
    then have ‹❙¬ p ∉ H› ‹q ∉ H›
      by blast+
    then have ‹∃A. set A ⊆ H ∧ ⊢⇩T ❙¬ p # A› ‹∃A. set A ⊆ H ∧ ⊢⇩T q # A›
      using assms MCS_refute by blast+
    then have ‹∃A. set A ⊆ H ∧ ⊢⇩T ❙¬ p # A ∧ ⊢⇩T q # A›
      using Weaken2[where p=‹❙¬ p› and q=q] by (metis Un_least set_append)
    then have ‹∃A. set A ⊆ H ∧ ⊢⇩T (p ❙⟶ q) # A›
      by blast
    then have ‹p ❙⟶ q ∉ H›
      using assms unfolding consistent_def by auto
    then show False
      using * ..
  qed
next
  fix p q
  assume *: ‹❙¬ (p ❙⟶ q) ∈ H›
  show ‹p ∈ H ∧ ❙¬ q ∈ H›
  proof (rule ccontr)
    assume ‹¬ (p ∈ H ∧ ❙¬ q ∈ H)›
    then consider ‹p ∉ H› | ‹❙¬ q ∉ H›
      by blast
    then show False
    proof cases
      case 1
      then have ‹∃A. set A ⊆ H ∧ ⊢⇩T p # A›
        using assms MCS_refute by blast
      then have ‹∃A. set A ⊆ H ∧ ⊢⇩T p # ❙¬ q # A›
        using Weaken[where B=‹p # ❙¬ q # _›] by fastforce
      then have ‹∃A. set A ⊆ H ∧ ⊢⇩T ❙¬ (p ❙⟶ q) # A›
        by fast
      then have ‹❙¬ (p ❙⟶ q) ∉ H›
        using assms unfolding consistent_def by auto
      then show False
        using * ..
    next
      case 2
      then have ‹∃A. set A ⊆ H ∧ ⊢⇩T ❙¬ q # A›
        using assms MCS_refute by blast
      then have ‹∃A. set A ⊆ H ∧ ⊢⇩T p # ❙¬ q # A›
        using Weaken by (metis set_subset_Cons)
      then have ‹∃A. set A ⊆ H ∧ ⊢⇩T ❙¬ (p ❙⟶ q) # A›
        by fast
      then have ‹❙¬ (p ❙⟶ q) ∉ H›
        using assms unfolding consistent_def by auto
      then show False
        using * ..
    qed
  qed
qed

lemma truth_lemma:
  assumes ‹consistent H› ‹maximal H› ‹p ∈ H›
  shows ‹⟦hmodel H⟧ p›
  using Hintikka_model MCS_Hintikka assms by blast

section ‹Completeness›

theorem strong_completeness:
  assumes ‹∀M :: 'p model. (∀q ∈ X. ⟦M⟧ q) ⟶ ⟦M⟧ p›
  shows ‹∃A. set A ⊆ X ∧ ⊢⇩T ❙¬ p # A›
proof (rule ccontr)
  assume ‹∄A. set A ⊆ X ∧ ⊢⇩T ❙¬ p # A›
  then have *: ‹∄A. set A ⊆ {❙¬ p} ∪ X ∧ ⊢⇩T A›
    using refute_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 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 ‹⊢⇩T [❙¬ p]›
  using assms strong_completeness[where X=‹{}›] by auto

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

end