(*
    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