header {* \isaheader{CFG and semantics conform} *}
theory SemanticsCFG imports CFG begin
locale CFG_semantics_wf = CFG sourcenode targetnode kind valid_edge Entry
get_proc get_return_edges procs Main
for sourcenode :: "'edge => 'node" and targetnode :: "'edge => 'node"
and kind :: "'edge => ('var,'val,'ret,'pname) edge_kind"
and valid_edge :: "'edge => bool"
and Entry :: "'node" ("'('_Entry'_')") and get_proc :: "'node => 'pname"
and get_return_edges :: "'edge => 'edge set"
and procs :: "('pname × 'var list × 'var list) list" and Main :: "'pname" +
fixes sem::"'com => ('var \<rightharpoonup> 'val) list => 'com => ('var \<rightharpoonup> 'val) list => bool"
("((1⟨_,/_⟩) =>/ (1⟨_,/_⟩))" [0,0,0,0] 81)
fixes identifies::"'node => 'com => bool" ("_ \<triangleq> _" [51,0] 80)
assumes fundamental_property:
"[|n \<triangleq> c; ⟨c,[cf]⟩ => ⟨c',s'⟩|] ==>
∃n' as. n -as->⇣\<surd>* n' ∧ n' \<triangleq> c' ∧ preds (kinds as) [(cf,undefined)] ∧
transfers (kinds as) [(cf,undefined)] = cfs' ∧ map fst cfs' = s'"
end