Theory Soundness

section ‹Soundness›

theory Soundness
  imports ProverLemmas
begin

text ‹In this theory, we prove that the prover is sound with regards to the SeCaV proof system 
  using the abstract soundness framework.›

text ‹If some suffix of the sequents in all of the children of a state are provable, so is some
  suffix of the sequent in the current state, with the prefix in each sequent being the same.
  (As a side condition, the lists of terms need to be compatible.)›
lemma SeCaV_children_pre:
  assumes ‹∀z' ∈ set (children A r z). (⊩ pre @ z')›
    and ‹paramss (pre @ z) ⊆ paramsts A› 
  shows ‹⊩ pre @ z›
  using assms
proof (induct z arbitrary: pre A)
  case Nil
  then show ?case
    by simp
next
  case (Cons p z)
  then have ih: ‹∀z' ∈ set (children A r z). (⊩ pre @ z') ⟹ (⊩ pre @ z)›
    if ‹paramss (pre @ z) ⊆ paramsts A› for pre A
    using that by simp

  let ?A = ‹remdups (A @ subtermFms (concat (parts A r p)))›

  have A: ‹paramss (pre @ p # z) ⊆ paramsts ?A›
    using paramsts_subset Cons.prems(2) by fastforce

  have ‹∀z' ∈ set (list_prod (parts A r p) (children ?A r z)). (⊩ pre @ z')›
    using Cons.prems by (metis children.simps(2))
  then have ‹∀z' ∈ {hs @ ts |hs ts. hs ∈ set (parts A r p) ∧ ts ∈ set (children ?A r z)}.
      (⊩ pre @ z')›
    using list_prod_is_cartesian by blast
  then have *:
    ‹∀hs ∈ set (parts A r p). ∀ts ∈ set (children ?A r z). (⊩ pre @ hs @ ts)›
    by blast
  then show ?case
  proof (cases r p rule: parts_exhaust)
    case (AlphaDis p q)
    then have ‹∀z' ∈ set (children ?A r z). (⊩ pre @ p # q # z')›
      using * unfolding parts_def by simp
    then have ‹∀z' ∈ set (children ?A r z). (⊩ (pre @ [p, q]) @ z')›
      by simp
    then have ‹⊩ pre @ p # q # z›
      using AlphaDis ih[where pre=‹pre @ [p, q]› and A=‹?A›] A by simp
    then have ‹⊩ p # q # pre @ z›
      using Ext by simp
    then have ‹⊩ Dis p q # pre @ z›
      using SeCaV.AlphaDis by blast
    then show ?thesis
      using AlphaDis Ext by simp
  next
    case (AlphaImp p q)
    then have ‹∀z' ∈ set (children ?A r z). (⊩ pre @ Neg p # q # z')›
      using * unfolding parts_def by simp
    then have ‹∀z' ∈ set (children ?A r z). (⊩ (pre @ [Neg p, q]) @ z')›
      by simp
    then have ‹⊩ pre @ Neg p # q # z›
      using AlphaImp ih[where pre=‹pre @ [Neg p, q]› and A=‹?A›] A by simp
    then have ‹⊩ Neg p # q # pre @ z›
      using Ext by simp
    then have ‹⊩ Imp p q # pre @ z›
      using SeCaV.AlphaImp by blast
    then show ?thesis
      using AlphaImp Ext by simp
  next
    case (AlphaCon p q)
    then have ‹∀z' ∈ set (children ?A r z). (⊩ pre @ Neg p # Neg q # z')›
      using * unfolding parts_def by simp
    then have ‹∀z' ∈ set (children ?A r z). (⊩ (pre @ [Neg p, Neg q]) @ z')›
      by simp
    then have ‹⊩ pre @ Neg p # Neg q # z›
      using AlphaCon ih[where pre=‹pre @ [Neg p, Neg q]› and A=‹?A›] A by simp
    then have ‹⊩ Neg p # Neg q # pre @ z›
      using Ext by simp
    then have ‹⊩ Neg (Con p q) # pre @ z›
      using SeCaV.AlphaCon by blast
    then show ?thesis
      using AlphaCon Ext by simp
  next
    case (BetaCon p q)
    then have
      ‹∀z' ∈ set (children ?A r z). (⊩ pre @ p # z')›
      ‹∀z' ∈ set (children ?A r z). (⊩ pre @ q # z')›
      using * unfolding parts_def by simp_all
    then have
      ‹∀z' ∈ set (children ?A r z). (⊩ (pre @ [p]) @ z')›
      ‹∀z' ∈ set (children ?A r z). (⊩ (pre @ [q]) @ z')›
      by simp_all
    then have ‹⊩ pre @ p # z› ‹⊩ pre @ q # z›
      using BetaCon ih[where pre=‹pre @ [_]› and A=‹?A›] A by simp_all
    then have ‹⊩ p # pre @ z› ‹⊩ q # pre @ z›
      using Ext by simp_all
    then have ‹⊩ Con p q # pre @ z›
      using SeCaV.BetaCon by blast
    then show ?thesis
      using BetaCon Ext by simp
  next
    case (BetaImp p q)
    then have
      ‹∀z' ∈ set (children ?A r z). (⊩ pre @ p # z')›
      ‹∀z' ∈ set (children ?A r z). (⊩ pre @ Neg q # z')›
      using * unfolding parts_def by simp_all
    then have
      ‹∀z' ∈ set (children ?A r z). (⊩ (pre @ [p]) @ z')›
      ‹∀z' ∈ set (children ?A r z). (⊩ (pre @ [Neg q]) @ z')›
      by simp_all
    then have ‹⊩ pre @ p # z› ‹⊩ pre @ Neg q # z›
      using BetaImp ih ih[where pre=‹pre @ [_]› and A=‹?A›] A by simp_all
    then have ‹⊩ p # pre @ z› ‹⊩ Neg q # pre @ z›
      using Ext by simp_all
    then have ‹⊩ Neg (Imp p q) # pre @ z›
      using SeCaV.BetaImp by blast
    then show ?thesis
      using BetaImp Ext by simp
  next
    case (BetaDis p q)
    then have
      ‹∀z' ∈ set (children ?A r z). (⊩ pre @ Neg p # z')›
      ‹∀z' ∈ set (children ?A r z). (⊩ pre @ Neg q # z')›
      using * unfolding parts_def by simp_all
    then have
      ‹∀z' ∈ set (children ?A r z). (⊩ (pre @ [Neg p]) @ z')›
      ‹∀z' ∈ set (children ?A r z). (⊩ (pre @ [Neg q]) @ z')›
      by simp_all
    then have ‹⊩ pre @ Neg p # z› ‹⊩ pre @ Neg q # z›
      using BetaDis ih[where pre=‹pre @ [_]› and A=‹?A›] A by simp_all
    then have ‹⊩ Neg p # pre @ z› ‹⊩ Neg q # pre @ z›
      using Ext by simp_all
    then have ‹⊩ Neg (Dis p q) # pre @ z›
      using SeCaV.BetaDis by blast
    then show ?thesis
      using BetaDis Ext by simp
  next
    case (DeltaUni p)
    let ?i = ‹generateNew A›
    have ‹∀z' ∈ set (children ?A r z). (⊩ pre @ sub 0 (Fun ?i []) p # z')›
      using DeltaUni * unfolding parts_def by simp
    then have ‹∀z' ∈ set (children ?A r z). (⊩ (pre @ [sub 0 (Fun ?i []) p]) @ z')›
      by simp
    moreover have ‹set (subtermFm (sub 0 (Fun ?i []) p)) ⊆ set ?A›
      using DeltaUni unfolding parts_def by simp
    then have ‹params (sub 0 (Fun ?i []) p) ⊆ paramsts ?A›
      using subtermFm_subset_params by blast
    ultimately have ‹⊩ pre @ sub 0 (Fun ?i []) p # z›
      using DeltaUni ih[where pre=‹pre @ [_]› and A=‹?A›] A by simp 
    then have ‹⊩ sub 0 (Fun ?i []) p # pre @ z›
      using Ext by simp
    moreover have ‹?i ∉ paramsts A›
      by (induct A) (metis Suc_max_new generateNew_def listFunTm_paramst(2) plus_1_eq_Suc)+
    then have ‹news ?i (p # pre @ z)›
      using DeltaUni Cons.prems(2) news_paramss by auto
    ultimately have ‹⊩ Uni p # pre @ z›
      using SeCaV.DeltaUni by blast
    then show ?thesis
      using DeltaUni Ext by simp
  next
    case (DeltaExi p)
    let ?i = ‹generateNew A›
    have ‹∀z' ∈ set (children ?A r z). (⊩ pre @ Neg (sub 0 (Fun ?i []) p) # z')›
      using DeltaExi * unfolding parts_def by simp
    then have ‹∀z' ∈ set (children ?A r z). (⊩ (pre @ [Neg (sub 0 (Fun ?i []) p)]) @ z')›
      by simp
    moreover have ‹set (subtermFm (sub 0 (Fun ?i []) p)) ⊆ set ?A›
      using DeltaExi unfolding parts_def by simp
    then have ‹params (sub 0 (Fun ?i []) p) ⊆ paramsts ?A›
      using subtermFm_subset_params by blast
    ultimately have ‹⊩ pre @ Neg (sub 0 (Fun ?i []) p) # z›
      using DeltaExi ih[where pre=‹pre @ [_]› and A=‹?A›] A by simp
    then have ‹⊩ Neg (sub 0 (Fun ?i []) p) # pre @ z›
      using Ext by simp
    moreover have ‹?i ∉ paramsts A›
      by (induct A) (metis Suc_max_new generateNew_def listFunTm_paramst(2) plus_1_eq_Suc)+
    then have ‹news ?i (p # pre @ z)›
      using DeltaExi Cons.prems(2) news_paramss by auto
   ultimately have ‹⊩ Neg (Exi p) # pre @ z›
      using SeCaV.DeltaExi by blast
    then show ?thesis
      using DeltaExi Ext by simp
  next
    case (NegNeg p)
    then have ‹∀z' ∈ set (children ?A r z). (⊩ pre @ p # z')›
      using * unfolding parts_def by simp
    then have ‹∀z' ∈ set (children ?A r z). (⊩ (pre @ [p]) @ z')›
      by simp
    then have ‹⊩ pre @ p # z›
      using NegNeg ih[where pre=‹pre @ [_]› and A=‹?A›] A by simp
    then have ‹⊩ p # pre @ z›
      using Ext by simp
    then have ‹⊩ Neg (Neg p) # pre @ z›
      using SeCaV.Neg by blast
    then show ?thesis
      using NegNeg Ext by simp
  next
    case (GammaExi p)
    then have ‹∀z' ∈ set (children ?A r z). (⊩ pre @ Exi p # map (λt. sub 0 t p) A @ z')›
      using * unfolding parts_def by simp
    then have ‹∀z' ∈ set (children ?A r z). (⊩ ((pre @ Exi p # map (λt. sub 0 t p) A) @ z'))›
      by simp
    moreover have ‹∀t ∈ set A. params (sub 0 t p) ⊆ paramsts A ∪ params p›
      using params_sub by fastforce
    then have ‹∀t ∈ set A. params (sub 0 t p) ⊆ paramsts ?A›
        using GammaExi A by fastforce
    then have ‹paramss (map (λt. sub 0 t p) A) ⊆ paramsts ?A›
      by auto
    ultimately have ‹⊩ pre @ Exi p # map (λt. sub 0 t p) A @ z›
      using GammaExi ih[where pre=‹pre @ Exi p # map _ A› and A=‹?A›] A by simp
    moreover have ‹ext (map (λt. sub 0 t p) A @ Exi p # pre @ z)
          (pre @ Exi p # map (λt. sub 0 t p) A @ z)›
      by auto
    ultimately have ‹⊩ map (λt. sub 0 t p) A @ Exi p # pre @ z›
      using Ext by blast
    then have ‹⊩ Exi p # pre @ z›
    proof (induct A)
      case Nil
      then show ?case
        by simp
    next
      case (Cons a A)
      then have ‹⊩ Exi p # map (λt. sub 0 t p) A @ Exi p # pre @ z›
        using SeCaV.GammaExi by simp
      then have ‹⊩ map (λt. sub 0 t p) A @ Exi p # pre @ z›
        using Ext by simp
      then show ?case
        using Cons.hyps by blast
    qed
    then show ?thesis
      using GammaExi Ext by simp
  next
    case (GammaUni p)
    then have ‹∀z' ∈ set (children ?A r z). (⊩ pre @ Neg (Uni p) # map (λt. Neg (sub 0 t p)) A @ z')›
      using * unfolding parts_def by simp
    then have ‹∀z' ∈ set (children ?A r z). (⊩ ((pre @ Neg (Uni p) # map (λt. Neg (sub 0 t p)) A) @ z'))›
      by simp
    moreover have ‹∀t ∈ set A. params (sub 0 t p) ⊆ paramsts A ∪ params p›
      using params_sub by fastforce
    then have ‹∀t ∈ set A. params (sub 0 t p) ⊆ paramsts ?A›
        using GammaUni A by fastforce
    then have ‹paramss (map (λt. sub 0 t p) A) ⊆ paramsts ?A›
      by auto
    ultimately have ‹⊩ pre @ Neg (Uni p) # map (λt. Neg (sub 0 t p)) A @ z›
      using GammaUni ih[where pre=‹pre @ Neg (Uni p) # map _ A› and A=‹?A›] A by simp
    moreover have ‹ext (map (λt. Neg (sub 0 t p)) A @ Neg (Uni p) # pre @ z)
          (pre @ Neg (Uni p) # map (λt. Neg (sub 0 t p)) A @ z)›
      by auto
    ultimately have ‹⊩ map (λt. Neg (sub 0 t p)) A @ Neg (Uni p) # pre @ z›
      using Ext by blast
    then have ‹⊩ Neg (Uni p) # pre @ z›
    proof (induct A)
      case Nil
      then show ?case
        by simp
    next
      case (Cons a A)
      then have ‹⊩ Neg (Uni p) # map (λt. Neg (sub 0 t p)) A @ Neg (Uni p) # pre @ z›
        using SeCaV.GammaUni by simp
      then have ‹⊩ map (λt. Neg (sub 0 t p)) A @ Neg (Uni p) # pre @ z›
        using Ext by simp
      then show ?case
        using Cons.hyps by blast
    qed
    then show ?thesis
      using GammaUni Ext by simp
  next
    case Other
    then have ‹∀z' ∈ set (children ?A r z). (⊩ (pre @ [p]) @ z')›
      using * by simp
    then show ?thesis
      using ih[where pre=‹pre @ [p]› and A=‹?A›] A by simp
  qed
qed

text ‹As a special case, the prefix can be empty.›
corollary SeCaV_children:
  assumes ‹∀z' ∈ set (children A r z). (⊩ z')› and ‹paramss z ⊆ paramsts A›
  shows ‹⊩ z›
  using SeCaV_children_pre assms by (metis append_Nil)

text ‹Using this lemma, we can instantiate the abstract soundness framework.›
interpretation Soundness eff rules UNIV ‹λ_ (A, z). (⊩ z)›
  unfolding Soundness_def
proof safe
  fix r A z ss S
  assume r_enabled: ‹eff r (A, z) ss›

  assume ‹∀s'. s' |∈| ss ⟶ (∀S ∈ UNIV. case s' of (A, z) ⇒ ⊩ z)›
  then have next_sound: ‹∀B z. (B, z) |∈| ss ⟶ (⊩ z)›
    by simp

  show ‹⊩ z›
  proof (cases ‹branchDone z›)
    case True
    then obtain p where ‹p ∈ set z› ‹Neg p ∈ set z›
      using branchDone_contradiction by blast
    then show ?thesis
      using Ext Basic by fastforce
  next
    case False
    let ?A = ‹remdups (A @ subtermFms z)›
    have ‹∀z' ∈ set (children ?A r z). (⊩ z')›
      using False r_enabled eff_children next_sound by blast
    moreover have ‹set (subtermFms z) ⊆ set ?A›
      by simp
    then have ‹paramss z ⊆ paramsts ?A›
      using subtermFm_subset_params by fastforce
    ultimately show ‹⊩ z›
      using SeCaV_children by blast
  qed
qed

text ‹Using the result from the abstract soundness framework, we can finally state our soundness
  result: for a finite, well-formed proof tree, the sequent at the root of the tree is provable in
  the SeCaV proof system.›
theorem prover_soundness_SeCaV:
  assumes ‹tfinite t› and ‹wf t›
  shows ‹⊩ rootSequent t›
  using assms soundness by fastforce

end