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