# 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)
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›
then show ?thesis
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
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›
then show ?thesis
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›
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
```