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