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