Theory Slicing.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