# Theory Sequent

theory Sequent
imports Tableau
```(*
Author: Asta Halkjær From, DTU Compute, 2019
Contributors: Alexander Birch Jensen, Anders Schlichtkrull & Jørgen Villadsen
*)

section ‹Sequent Calculus›

theory Sequent imports Tableau begin

inductive SC :: ‹('a, 'b) form list ⇒ bool› (‹⊢ _› 0) where
Basic: ‹⊢ Pred i l # Neg (Pred i l) # G›
| BasicNegFF: ‹⊢ Neg ⊥ # G›
| BasicTT: ‹⊢ ⊤ # G›
| AlphaNegNeg: ‹⊢ A # G ⟹ ⊢ Neg (Neg A) # G›
| AlphaNegAnd: ‹⊢ Neg A # Neg B # G ⟹ ⊢ Neg (And A B) # G›
| AlphaOr: ‹⊢ A # B # G ⟹ ⊢ Or A B # G›
| AlphaImpl: ‹⊢ Neg A # B # G ⟹ ⊢ Impl A B # G›
| BetaAnd: ‹⊢ A # G ⟹ ⊢ B # G ⟹ ⊢ And A B # G›
| BetaNegOr: ‹⊢ Neg A # G ⟹ ⊢ Neg B # G ⟹ ⊢ Neg (Or A B) # G›
| BetaNegImpl: ‹⊢ A # G ⟹ ⊢ Neg B # G ⟹ ⊢ Neg (Impl A B) # G›
| GammaExists: ‹⊢ subst A t 0 # G ⟹ ⊢ Exists A # G›
| GammaNegForall: ‹⊢ Neg (subst A t 0) # G ⟹ ⊢ Neg (Forall A) # G›
| DeltaForall: ‹⊢ subst A (App n []) 0 # G ⟹ news n (A # G) ⟹ ⊢ Forall A # G›
| DeltaNegExists: ‹⊢ Neg (subst A (App n []) 0) # G ⟹ news n (A # G) ⟹ ⊢ Neg (Exists A) # G›
| Order: ‹⊢ G ⟹ set G = set G' ⟹ ⊢ G'›

lemma Shift: ‹⊢ rotate1 G ⟹ ⊢ G›

lemma Swap: ‹⊢ B # A # G ⟹ ⊢ A # B # G›

lemma ‹⊢ [Neg (Pred ''A'' []), Pred ''A'' []]›
by (rule Shift, simp) (rule Basic)

lemma ‹⊢ [And (Pred ''A'' []) (Pred ''B'' []), Neg (And (Pred ''B'' []) (Pred ''A'' []))]›
apply (rule BetaAnd)
apply (rule Swap)
apply (rule AlphaNegAnd)
apply (rule Shift, simp, rule Swap)
apply (rule Basic)
apply (rule Swap)
apply (rule AlphaNegAnd)
apply (rule Shift, rule Shift, simp)
apply (rule Basic)
done

subsection ‹Soundness›

lemma SC_soundness: ‹⊢ G ⟹ ∃p ∈ set G. eval e f g p›
proof (induct G arbitrary: f rule: SC.induct)
case (DeltaForall A n G)
then consider
‹∀x. eval e (f(n := λw. x)) g (subst A (App n []) 0)› |
‹∃x. ∃p ∈ set G. eval e (f(n := λw. x)) g p›
by fastforce
then show ?case
proof cases
case 1
then have ‹∀x. eval (shift e 0 x) (f(n := λw. x)) g A›
by simp
then have ‹∀x. eval (shift e 0 x) f g A›
using ‹news n (A # G)› by simp
then show ?thesis
by simp
next
case 2
then have ‹∃p ∈ set G. eval e f g p›
using ‹news n (A # G)› using Ball_set insert_iff list.set(2) upd_lemma by metis
then show ?thesis
by simp
qed
next
case (DeltaNegExists A n G)
then consider
‹∀x. eval e (f(n := λw. x)) g (Neg (subst A (App n []) 0))› |
‹∃x. ∃p ∈ set G. eval e (f(n := λw. x)) g p›
by fastforce
then show ?case
proof cases
case 1
then have ‹∀x. eval (shift e 0 x) (f(n := λw. x)) g (Neg A)›
by simp
then have ‹∀x. eval (shift e 0 x) f g (Neg A)›
using ‹news n (A # G)› by simp
then show ?thesis
by simp
next
case 2
then have ‹∃p ∈ set G. eval e f g p›
using ‹news n (A # G)› using Ball_set insert_iff list.set(2) upd_lemma by metis
then show ?thesis
by simp
qed
qed auto

subsection ‹Tableau Calculus Equivalence›

fun compl :: ‹('a, 'b) form ⇒ ('a, 'b) form› where
‹compl (Neg p) = p›
| ‹compl p = Neg p›

lemma compl: ‹compl p = Neg p ∨ (∃q. compl p = q ∧ p = Neg q)›
by (cases p rule: compl.cases) simp_all

lemma new_compl: ‹new n p ⟹ new n (compl p)›
by (cases p rule: compl.cases) simp_all

lemma news_compl: ‹news n G ⟹ news n (map compl G)›
using new_compl by (induct G) fastforce+

theorem TC_SC: ‹⊣ G ⟹ ⊢ map compl G›
proof (induct G rule: TC.induct)
case (Basic i l G)
then show ?case
using SC.Basic Swap by fastforce
next
case (AlphaNegNeg A G)
then show ?case
using SC.AlphaNegNeg compl by (metis compl.simps(1) list.simps(9))
next
case (AlphaAnd A B G)
then have *: ‹⊢ compl A # compl B # map compl G›
by simp
then have ‹⊢ Neg A # Neg B # map compl G›
using compl AlphaNegNeg Swap by metis
then show ?case
using AlphaNegAnd by simp
next
case (AlphaNegImpl A B G)
then have ‹⊢ compl A # B # map compl G›
by simp
then have ‹⊢ Neg A # B # map compl G›
using compl AlphaNegNeg by metis
then show ?case
using AlphaImpl by simp
next
case (BetaOr A G B)
then have ‹⊢ compl A # map compl G› ‹⊢ compl B # map compl G›
by simp_all
then have ‹⊢ Neg A # map compl G› ‹⊢ Neg B # map compl G›
using compl AlphaNegNeg by metis+
then show ?case
using BetaNegOr by simp
next
case (BetaImpl A G B)
then have ‹⊢ A # map compl G› ‹⊢ compl B # map compl G›
by simp_all
then have ‹⊢ A # map compl G› ‹⊢ Neg B # map compl G›
by - (assumption, metis compl AlphaNegNeg)
then have ‹⊢ Neg (Impl A B) # map compl G›
using BetaNegImpl by blast
then have ‹⊢ compl (Impl A B) # map compl G›
using ‹⊢ A # map compl G› compl by simp
then show ?case
by simp
next
case (GammaForall A t G)
then have ‹⊢ compl (subst A t 0) # map compl G›
by simp
then have ‹⊢ Neg (subst A t 0) # map compl G›
using compl AlphaNegNeg by metis
then show ?case
using GammaNegForall by simp
next
case (DeltaExists A n G)
then have ‹⊢ compl (subst A (App n []) 0) # map compl G›
by simp
then have ‹⊢ Neg (subst A (App n []) 0) # map compl G›
using compl AlphaNegNeg by metis
moreover have ‹news n (A # map compl G)›
using DeltaExists news_compl by fastforce
ultimately show ?case
using DeltaNegExists by simp
next
case (DeltaNegForall A n G)
then have ‹⊢ subst A (App n []) 0 # map compl G›
by simp
moreover have ‹news n (A # map compl G)›
using DeltaNegForall news_compl by fastforce
ultimately show ?case
using DeltaForall by simp

subsection ‹Completeness›

theorem SC_completeness:
fixes p :: ‹(nat, nat) form›
assumes ‹∀(e :: nat ⇒ nat hterm) f g. list_all (eval e f g) ps ⟶ eval e f g p›
shows ‹⊢ p # map compl ps›
proof -
have ‹⊣ Neg p # ps›
using assms tableau_completeness unfolding tableauproof_def by simp
then show ?thesis
using TC_SC by fastforce
qed

corollary
fixes p :: ‹(nat, nat) form›
assumes ‹∀(e :: nat ⇒ nat hterm) f g. eval e f g p›
shows ‹⊢ [p]›
using assms SC_completeness list.map(1) by metis

end
```