Theory FOL_Seq_Calc1.Sequent

(*
    Author: Asta Halkjær From, DTU Compute, 2019-2021
    Contributors: Alexander Birch Jensen, Anders Schlichtkrull & Jørgen Villadsen

    See also the Natural Deduction Assistant (NaDeA) and the Sequent Calculus Verifier (SeCaV):

      https://nadea.compute.dtu.dk/
      https://secav.compute.dtu.dk/
*)

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
  by (simp add: Order)

lemma Swap:  B # A # G   A # B # G
  by (simp add: Order insert_commute)

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
qed (simp_all add: SC.intros)

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