Theory Finite_Proof_Soundness

(*<*)
theory Finite_Proof_Soundness
imports Abstract_Completeness.Abstract_Completeness
begin
(*>*)

section ‹Abstract Soundness›

locale Soundness = RuleSystem_Defs eff rules for
  eff :: "'rule ⇒ 'sequent ⇒ 'sequent fset ⇒ bool"
  and rules :: "'rule stream" +
  fixes "structure" :: "'structure set"
    and sat :: "'structure ⇒ 'sequent ⇒ bool"
  assumes local_soundness:
    "⋀r s sl.
      ⟦r ∈ R; eff r s sl; ⋀s'. s' |∈| sl ⟹ ∀S ∈ structure. sat S s'⟧
      ⟹
      ∀S ∈ structure. sat S s"
begin

abbreviation "ssat s ≡ ∀S ∈ structure. sat S s"

lemma epath_shift:
  assumes "epath (srs @- steps)"
  shows "epath steps"
  using assms by (induction srs arbitrary: steps) (auto elim: epath.cases)

theorem soundness:
  assumes f: "tfinite t" and w: "wf t"
  shows "ssat (fst (root t))"
  using f w proof (induction t rule: tfinite.induct)
  case (tfinite t)
  show ?case
    by (rule local_soundness[of "snd (root t)" _ "fimage (fst o root) (cont t)"], insert tfinite)
      (fastforce elim!: wf.cases)+
qed

end (* context Soundness *)

(*<*)
end
(*>*)