Theory SemanticsCFG

section ‹CFG and semantics conform›

theory SemanticsCFG imports CFG begin

locale CFG_semantics_wf = CFG sourcenode targetnode kind valid_edge Entry
  for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
  and kind :: "'edge ⇒ 'state edge_kind" and valid_edge :: "'edge ⇒ bool"
  and Entry :: "'node" ("'('_Entry'_')") +
  fixes sem::"'com ⇒ 'state ⇒ 'com ⇒ 'state ⇒ bool" 
    ("((1⟨_,/_⟩) ⇒/ (1⟨_,/_⟩))" [0,0,0,0] 81)
  fixes identifies::"'node ⇒ 'com ⇒ bool" ("_ ≜ _" [51,0] 80)
  assumes fundamental_property:
    "⟦n ≜ c; ⟨c,s⟩ ⇒ ⟨c',s'⟩⟧ ⟹
      ∃n' as. n -as→* n' ∧ transfers (kinds as) s = s' ∧ preds (kinds as) s ∧
               n' ≜ c'"


end