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
```