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› (infix ‹⊨⇩T› 50) where
  ‹I ⊨⇩T ❙⋅P ⟷ I P›
| ‹I ⊨⇩T ❙¬ p ⟷ ¬ I ⊨⇩T p›
| ‹I ⊨⇩T p ❙⟶ q ⟷ I ⊨⇩T p ⟶ I ⊨⇩T q›

section ‹Calculus›

inductive Calculus :: ‹'p fm list ⇒ bool› (‹⊢⇩T _› [50] 50) where
  Axiom [simp]: ‹⊢⇩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›
| Weak: ‹⊢⇩T A ⟹ set A ⊆ set B ⟹ ⊢⇩T B›

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

section ‹Soundness›

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

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

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

section ‹Maximal Consistent Sets›

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

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 Refutations_MCS consistent Calculus
proof
  fix A B :: ‹'p fm list›
  assume ‹⊢⇩T A› ‹set A = set B›
  then show ‹⊢⇩T B›
    using Weak by blast
next
  fix S :: ‹'p fm set›
  show ‹consistent S ⟷ (∀A. set A ⊆ S ⟶ ¬ ⊢⇩T A)›
    unfolding consistent_def ..
qed

section ‹Truth Lemma›

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

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 ⟶ ℳ⇩T(H) ⊨⇩T p) ∧ (❙¬ p ∈ H ⟶ ¬ ℳ⇩T(H) ⊨⇩T p)›
  using assms by (induct p) (unfold Hintikka_def semantics.simps; blast)+

lemma MCS_Hintikka:
  assumes ‹MCS 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 simp
  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 Weak2[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 Weak[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 Weak 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 ‹MCS H› ‹p ∈ H›
  shows ‹ℳ⇩T(H) ⊨⇩T p›
  using Hintikka_model MCS_Hintikka assms by blast

section ‹Completeness›

theorem strong_completeness:
  assumes ‹∀M. (∀q ∈ X. M ⊨⇩T q) ⟶ M ⊨⇩T 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 (metis Weak insert_is_Un set_subset_Cons subset_insert)

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

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

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