# Theory Soundness

```section ‹Soundness›

theory Soundness imports "Abstract_Soundness.Finite_Proof_Soundness" Prover Semantics begin

lemma eff_sound:
assumes ‹eff r (A, B) = Some ss› ‹∀A B. (A, B) |∈| ss ⟶ (∀(E :: _ ⇒ 'a). sc (E, F, G) (A, B))›
shows ‹sc (E, F, G) (A, B)›
using assms
proof (induct r ‹(A, B)› rule: eff.induct)
case (5 p q)
then have ‹sc (E, F, G) (A [÷] (p ❙⟶ q), p # B)› ‹sc (E, F, G) (q # A [÷] (p ❙⟶ q), B)›
by (metis eff.simps(5) finsertCI option.inject option.simps(3))+
then show ?case
using "5.prems"(1) by (force split: if_splits)
next
case (7 t p)
then have ‹sc (E, F, G) (⟨t⟩p # A, B)›
by (metis eff.simps(7) finsert_iff option.inject option.simps(3))
then show ?case
using "7.prems"(1) by (fastforce split: if_splits)
next
case (8 p)
let ?n = ‹fresh (A @ B)›
have A: ‹∀p [∈] A. max_list (vars_fm p) < ?n› and B: ‹∀p [∈] B. max_list (vars_fm p) < ?n›
unfolding fresh_def using max_list_vars_fms max_list_mono vars_fms_member
by (metis Un_iff le_imp_less_Suc set_append)+
from 8 have ‹sc (E(?n := x), F, G) (A, ⟨❙#?n⟩p # B [÷] ❙∀p)› for x
by (metis eff.simps(8) finsert_iff option.inject option.simps(3))
then have ‹(∀p [∈] A. ⟦E, F, G⟧ p) ⟶
(∀x. ⟦(x ⨟ λm. (E(?n := x)) m), F, G⟧ p) ∨ (∃q [∈] B [÷] ❙∀p. ⟦E, F, G⟧ q)›
using A B upd_vars_fm by fastforce
then have ‹(∀p [∈] A. ⟦E, F, G⟧ p) ⟶
(∀x. ⟦((x ⨟ E)(Suc ?n := x)), F, G⟧ p) ∨ (∃q [∈] B [÷] ❙∀p. ⟦E, F, G⟧ q)›
unfolding add_upd_commute by blast
moreover have ‹max_list (vars_fm p) < ?n›
using B "8.prems"(1) by (metis eff.simps(8) option.distinct(1) vars_fm.simps(4))
ultimately have ‹sc (E, F, G) (A, ❙∀p # (B [÷] ❙∀p))›
by auto
moreover have ‹❙∀p [∈] B›
using "8.prems"(1) by (simp split: if_splits)
ultimately show ?case
by (metis (full_types) Diff_iff sc.simps set_ConsD set_removeAll)
qed (fastforce split: if_splits)+

interpretation Soundness ‹λr s ss. eff r s = Some ss› rules UNIV sc
unfolding Soundness_def using eff_sound by fast

theorem prover_soundness:
assumes ‹tfinite t› and ‹wf t›
shows ‹sc (E, F, G) (fst (root t))›
using assms soundness by fast

end
```