Theory Abstract_Soundness.Finite_Proof_Soundness

theory Finite_Proof_Soundness
imports Abstract_Completeness.Abstract_Completeness

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"

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)+

end (* context Soundness *)