header {* \isaheader{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" ("_ \<triangleq> _" [51,0] 80)
assumes fundamental_property:
"[|n \<triangleq> c; ⟨c,s⟩ => ⟨c',s'⟩|] ==>
∃n' as. n -as->* n' ∧ transfers (kinds as) s = s' ∧ preds (kinds as) s ∧
n' \<triangleq> c'"
end