Theory DPN_Setup

theory DPN_Setup
imports "Program-Conflict-Analysis.LTS" "Automatic_Refinement.Misc"
begin

section ‹Additions to LTS›

lemma trcl_struct: "⋀s. ⟦(s,w,s')∈trcl D; D⊆S×A×S'⟧ ⟹ (s=s' ∧ w=[]) ∨ (s∈S ∧ s'∈S' ∧ w∈lists A)" 
proof (induct w)
  case Nil
  then show ?case by simp
next
  case (Cons e w)
  then obtain sh where SPLIT: "(s,e,sh)∈D ∧ (sh,w,s')∈trcl D" by (blast dest: trcl_uncons)
  from SPLIT Cons.prems have "s∈S ∧ e∈A ∧ sh∈S'" by auto
  moreover from SPLIT Cons have "(sh=s' ∧ w=[]) ∨ (s'∈S' ∧ w∈lists A)" by blast
  ultimately show ?case by auto
qed


lemma trcl_structE: 
  assumes "(s,w,s')∈trcl D" "D⊆S×A×S'"
  obtains (empty) "s=s'" "w=[]" | (nonempty) "s∈S" "s'∈S'" "w∈lists A"
  using assms
  by (blast dest: trcl_struct)


end