# Theory SeCaV

```chapter SeCaV

(*
Author: Jørgen Villadsen, DTU Compute, 2020
Contributors: Stefan Berghofer, Asta Halkjær From, Alexander Birch Jensen & Anders Schlichtkrull
*)

section ‹Sequent Calculus Verifier (SeCaV)›

theory SeCaV imports Main begin

section ‹Syntax: Terms / Formulas›

datatype tm = Fun nat ‹tm list› | Var nat

datatype fm = Pre nat ‹tm list› | Imp fm fm | Dis fm fm | Con fm fm | Exi fm | Uni fm | Neg fm

section ‹Semantics: Terms / Formulas›

definition ‹shift e v x ≡ λn. if n < v then e n else if n = v then x else e (n - 1)›

primrec semantics_term and semantics_list where
‹semantics_term e f (Var n) = e n› |
‹semantics_term e f (Fun i l) = f i (semantics_list e f l)› |
‹semantics_list e f [] = []› |
‹semantics_list e f (t # l) = semantics_term e f t # semantics_list e f l›

primrec semantics where
‹semantics e f g (Pre i l) = g i (semantics_list e f l)› |
‹semantics e f g (Imp p q) = (semantics e f g p ⟶ semantics e f g q)› |
‹semantics e f g (Dis p q) = (semantics e f g p ∨ semantics e f g q)› |
‹semantics e f g (Con p q) = (semantics e f g p ∧ semantics e f g q)› |
‹semantics e f g (Exi p) = (∃x. semantics (shift e 0 x) f g p)› |
‹semantics e f g (Uni p) = (∀x. semantics (shift e 0 x) f g p)› |
‹semantics e f g (Neg p) = (¬ semantics e f g p)›

― ‹Test›

corollary ‹semantics e f g (Imp (Pre 0 []) (Pre 0 []))›
by simp

lemma ‹¬ semantics e f g (Neg (Imp (Pre 0 []) (Pre 0 [])))›
by simp

section ‹Auxiliary Functions›

primrec new_term and new_list where
‹new_term c (Var n) = True› |
‹new_term c (Fun i l) = (if i = c then False else new_list c l)› |
‹new_list c [] = True› |
‹new_list c (t # l) = (if new_term c t then new_list c l else False)›

primrec new where
‹new c (Pre i l) = new_list c l› |
‹new c (Imp p q) = (if new c p then new c q else False)› |
‹new c (Dis p q) = (if new c p then new c q else False)› |
‹new c (Con p q) = (if new c p then new c q else False)› |
‹new c (Exi p) = new c p› |
‹new c (Uni p) = new c p› |
‹new c (Neg p) = new c p›

primrec news where
‹news c [] = True› |
‹news c (p # z) = (if new c p then news c z else False)›

primrec inc_term and inc_list where
‹inc_term (Var n) = Var (n + 1)› |
‹inc_term (Fun i l) = Fun i (inc_list l)› |
‹inc_list [] = []› |
‹inc_list (t # l) = inc_term t # inc_list l›

primrec sub_term and sub_list where
‹sub_term v s (Var n) = (if n < v then Var n else if n = v then s else Var (n - 1))› |
‹sub_term v s (Fun i l) = Fun i (sub_list v s l)› |
‹sub_list v s [] = []› |
‹sub_list v s (t # l) = sub_term v s t # sub_list v s l›

primrec sub where
‹sub v s (Pre i l) = Pre i (sub_list v s l)› |
‹sub v s (Imp p q) = Imp (sub v s p) (sub v s q)› |
‹sub v s (Dis p q) = Dis (sub v s p) (sub v s q)› |
‹sub v s (Con p q) = Con (sub v s p) (sub v s q)› |
‹sub v s (Exi p) = Exi (sub (v + 1) (inc_term s) p)› |
‹sub v s (Uni p) = Uni (sub (v + 1) (inc_term s) p)› |
‹sub v s (Neg p) = Neg (sub v s p)›

primrec member where
‹member p [] = False› |
‹member p (q # z) = (if p = q then True else member p z)›

primrec ext where
‹ext y [] = True› |
‹ext y (p # z) = (if member p y then ext y z else False)›

― ‹Simplifications›

lemma member [iff]: ‹member p z ⟷ p ∈ set z›
by (induct z) simp_all

lemma ext [iff]: ‹ext y z ⟷ set z ⊆ set y›
by (induct z) simp_all

section ‹Sequent Calculus›

inductive sequent_calculus (‹⊩ _› 0) where
‹⊩ p # z› if ‹member (Neg p) z› |
‹⊩ Dis p q # z› if ‹⊩ p # q # z› |
‹⊩ Imp p q # z› if ‹⊩ Neg p # q # z› |
‹⊩ Neg (Con p q) # z› if ‹⊩ Neg p # Neg q # z› |
‹⊩ Con p q # z› if ‹⊩ p # z› and ‹⊩ q # z› |
‹⊩ Neg (Imp p q) # z› if ‹⊩ p # z› and ‹⊩ Neg q # z› |
‹⊩ Neg (Dis p q) # z› if ‹⊩ Neg p # z› and ‹⊩ Neg q # z› |
‹⊩ Exi p # z› if ‹⊩ sub 0 t p # z› |
‹⊩ Neg (Uni p) # z› if ‹⊩ Neg (sub 0 t p) # z› |
‹⊩ Uni p # z› if ‹⊩ sub 0 (Fun i []) p # z› and ‹news i (p # z)› |
‹⊩ Neg (Exi p) # z› if ‹⊩ Neg (sub 0 (Fun i []) p) # z› and ‹news i (p # z)› |
‹⊩ Neg (Neg p) # z› if ‹⊩ p # z› |
‹⊩ y› if ‹⊩ z› and ‹ext y z›

― ‹Test›

corollary ‹⊩ [Imp (Pre 0 []) (Pre 0 [])]›
using sequent_calculus.intros(1,3,13) ext.simps member.simps(2) by metis

section ‹Shorthands›

lemmas Basic = sequent_calculus.intros(1)

lemmas AlphaDis = sequent_calculus.intros(2)
lemmas AlphaImp = sequent_calculus.intros(3)
lemmas AlphaCon = sequent_calculus.intros(4)

lemmas BetaCon = sequent_calculus.intros(5)
lemmas BetaImp = sequent_calculus.intros(6)
lemmas BetaDis = sequent_calculus.intros(7)

lemmas GammaExi = sequent_calculus.intros(8)
lemmas GammaUni = sequent_calculus.intros(9)

lemmas DeltaUni = sequent_calculus.intros(10)
lemmas DeltaExi = sequent_calculus.intros(11)

lemmas Neg = sequent_calculus.intros(12)

lemmas Ext = sequent_calculus.intros(13)

― ‹Test›

lemma ‹⊩
[
Imp (Pre 0 []) (Pre 0 [])
]
›
proof -
from AlphaImp have ?thesis if ‹⊩
[
Neg (Pre 0 []),
Pre 0 []
]
›
using that by simp
with Ext have ?thesis if ‹⊩
[
Pre 0 [],
Neg (Pre 0 [])
]
›
using that by simp
with Basic show ?thesis
by simp
qed

section ‹Appendix: Soundness›

subsection ‹Increment Function›

primrec liftt :: ‹tm ⇒ tm› and liftts :: ‹tm list ⇒ tm list› where
‹liftt (Var i) = Var (Suc i)› |
‹liftt (Fun a ts) = Fun a (liftts ts)› |
‹liftts [] = []› |
‹liftts (t # ts) = liftt t # liftts ts›

subsection ‹Parameters: Terms›

primrec paramst :: ‹tm ⇒ nat set› and paramsts :: ‹tm list ⇒ nat set› where
‹paramst (Var n) = {}› |
‹paramst (Fun a ts) = {a} ∪ paramsts ts› |
‹paramsts [] = {}› |
‹paramsts (t # ts) = (paramst t ∪ paramsts ts)›

lemma p0 [simp]: ‹paramsts ts = ⋃(set (map paramst ts))›
by (induct ts) simp_all

primrec paramst' :: ‹tm ⇒ nat set› where
‹paramst' (Var n) = {}› |
‹paramst' (Fun a ts) = {a} ∪ ⋃(set (map paramst' ts))›

lemma p1 [simp]: ‹paramst' t = paramst t›
by (induct t) simp_all

subsection ‹Parameters: Formulas›

primrec params :: ‹fm ⇒ nat set› where
‹params (Pre b ts) = paramsts ts› |
‹params (Imp p q) = params p ∪ params q› |
‹params (Dis p q) = params p ∪ params q› |
‹params (Con p q) = params p ∪ params q› |
‹params (Exi p) = params p› |
‹params (Uni p) = params p› |
‹params (Neg p) = params p›

primrec params' :: ‹fm ⇒ nat set› where
‹params' (Pre b ts) = ⋃(set (map paramst' ts))› |
‹params' (Imp p q) = params' p ∪ params' q› |
‹params' (Dis p q) = params' p ∪ params' q› |
‹params' (Con p q) = params' p ∪ params' q› |
‹params' (Exi p) = params' p› |
‹params' (Uni p) = params' p› |
‹params' (Neg p) = params' p›

lemma p2 [simp]: ‹params' p = params p›
by (induct p) simp_all

fun paramst'' :: ‹tm ⇒ nat set› where
‹paramst'' (Var n) = {}› |
‹paramst'' (Fun a ts) = {a} ∪ (⋃t ∈ set ts. paramst'' t)›

lemma p1' [simp]: ‹paramst'' t = paramst t›
by (induct t) simp_all

fun params'' :: ‹fm ⇒ nat set› where
‹params'' (Pre b ts) = (⋃t ∈ set ts. paramst'' t)› |
‹params'' (Imp p q) = params'' p ∪ params'' q› |
‹params'' (Dis p q) = params'' p ∪ params'' q› |
‹params'' (Con p q) = params'' p ∪ params'' q› |
‹params'' (Exi p) = params'' p› |
‹params'' (Uni p) = params'' p› |
‹params'' (Neg p) = params'' p›

lemma p2' [simp]: ‹params'' p = params p›
by (induct p) simp_all

subsection ‹Update Lemmas›

lemma upd_lemma' [simp]:
‹n ∉ paramst t ⟹ semantics_term e (f(n := z)) t = semantics_term e f t›
‹n ∉ paramsts ts ⟹ semantics_list e (f(n := z)) ts = semantics_list e f ts›
by (induct t and ts rule: paramst.induct paramsts.induct) auto

lemma upd_lemma [iff]: ‹n ∉ params p ⟹ semantics e (f(n := z)) g p ⟷ semantics e f g p›
by (induct p arbitrary: e) simp_all

subsection ‹Substitution›

primrec substt :: ‹tm ⇒ tm ⇒ nat ⇒ tm› and substts :: ‹tm list ⇒ tm ⇒ nat ⇒ tm list› where
‹substt (Var i) s k = (if k < i then Var (i - 1) else if i = k then s else Var i)› |
‹substt (Fun a ts) s k = Fun a (substts ts s k)› |
‹substts [] s k = []› |
‹substts (t # ts) s k = substt t s k # substts ts s k›

primrec subst :: ‹fm ⇒ tm ⇒ nat ⇒ fm› where
‹subst (Pre b ts) s k = Pre b (substts ts s k)› |
‹subst (Imp p q) s k = Imp (subst p s k) (subst q s k)› |
‹subst (Dis p q) s k = Dis (subst p s k) (subst q s k)› |
‹subst (Con p q) s k = Con (subst p s k) (subst q s k)› |
‹subst (Exi p) s k = Exi (subst p (liftt s) (Suc k))› |
‹subst (Uni p) s k = Uni (subst p (liftt s) (Suc k))› |
‹subst (Neg p) s k = Neg (subst p s k)›

lemma shift_eq [simp]: ‹i = j ⟹ (shift e i T) j = T› for i :: nat
unfolding shift_def by simp

lemma shift_gt [simp]: ‹j < i ⟹ (shift e i T) j = e j› for i :: nat
unfolding shift_def by simp

lemma shift_lt [simp]: ‹i < j ⟹ (shift e i T) j = e (j - 1)› for i :: nat
unfolding shift_def by simp

lemma shift_commute [simp]: ‹shift (shift e i U) 0 T = shift (shift e 0 T) (Suc i) U›
unfolding shift_def by force

lemma subst_lemma' [simp]:
‹semantics_term e f (substt t u i) = semantics_term (shift e i (semantics_term e f u)) f t›
‹semantics_list e f (substts ts u i) = semantics_list (shift e i (semantics_term e f u)) f ts›
by (induct t and ts rule: substt.induct substts.induct) simp_all

lemma lift_lemma [simp]:
‹semantics_term (shift e 0 x) f (liftt t) = semantics_term e f t›
‹semantics_list (shift e 0 x) f (liftts ts) = semantics_list e f ts›
by (induct t and ts rule: liftt.induct liftts.induct) simp_all

lemma subst_lemma [iff]:
‹semantics e f g (subst a t i) ⟷ semantics (shift e i (semantics_term e f t)) f g a›
by (induct a arbitrary: e i t) simp_all

subsection ‹Auxiliary Lemmas›

lemma s1 [iff]: ‹new_term c t ⟷ (c ∉ paramst t)› ‹new_list c l ⟷ (c ∉ paramsts l)›
by (induct t and l rule: new_term.induct new_list.induct) simp_all

lemma s2 [iff]: ‹new c p ⟷ (c ∉ params p)›
by (induct p) simp_all

lemma s3 [iff]: ‹news c z ⟷ list_all (λp. c ∉ params p) z›
by (induct z) simp_all

lemma s4 [simp]: ‹inc_term t = liftt t› ‹inc_list l = liftts l›
by (induct t and l rule: inc_term.induct inc_list.induct) simp_all

lemma s5 [simp]: ‹sub_term v s t = substt t s v› ‹sub_list v s l = substts l s v›
by (induct t and l rule: inc_term.induct inc_list.induct) simp_all

lemma s6 [simp]: ‹sub v s p = subst p s v›
by (induct p arbitrary: v s) simp_all

subsection ‹Soundness›

theorem sound: ‹⊩ z ⟹ ∃p ∈ set z. semantics e f g p›
proof (induct arbitrary: f rule: sequent_calculus.induct)
case (10 i p z)
then show ?case
proof (cases ‹∀x. semantics e (f(i := λ_. x)) g (sub 0 (Fun i []) p)›)
case False
moreover have ‹list_all (λp. i ∉ params p) z›
using 10 by simp
ultimately show ?thesis
using 10 Ball_set insert_iff list.set(2) upd_lemma by metis
qed simp
next
case (11 i p z)
then show ?case
proof (cases ‹∀x. semantics e (f(i := λ_. x)) g (Neg (sub 0 (Fun i []) p))›)
case False
moreover have ‹list_all (λp. i ∉ params p) z›
using 11 by simp
ultimately show ?thesis
using 11 Ball_set insert_iff list.set(2) upd_lemma by metis
qed simp
qed force+

corollary ‹⊩ z ⟹ ∃p. member p z ∧ semantics e f g p›
using sound by force

corollary ‹⊩ [p] ⟹ semantics e f g p›
using sound by force

corollary ‹¬ (⊩ [])›
using sound by force

section ‹Reference›

text ‹Mordechai Ben-Ari (Springer 2012): Mathematical Logic for Computer Science (Third Edition)›

end
```