Theory Interpretation
section ‹Instantiate CFG locales with Proc CFG›
theory Interpretation imports WellFormProgs "../StaticInter/CFGExit" begin
subsection ‹Lifting of the basic definitions›
abbreviation sourcenode :: "edge ⇒ node"
where "sourcenode e ≡ fst e"
abbreviation targetnode :: "edge ⇒ node"
where "targetnode e ≡ snd(snd e)"
abbreviation kind :: "edge ⇒ (vname,val,node,pname) edge_kind"
where "kind e ≡ fst(snd e)"
definition valid_edge :: "wf_prog ⇒ edge ⇒ bool"
where "⋀wfp. valid_edge wfp a ≡ let (prog,procs) = Rep_wf_prog wfp in
prog,procs ⊢ sourcenode a -kind a→ targetnode a"
definition get_return_edges :: "wf_prog ⇒ edge ⇒ edge set"
where "⋀wfp. get_return_edges wfp a ≡
case kind a of Q:r↪⇘p⇙fs ⇒ {a'. valid_edge wfp a' ∧ (∃Q' f'. kind a' = Q'↩⇘p⇙f') ∧
targetnode a' = r}
| _ ⇒ {}"
lemma get_return_edges_non_call_empty:
fixes wfp
shows "∀Q r p fs. kind a ≠ Q:r↪⇘p⇙fs ⟹ get_return_edges wfp a = {}"
by(cases "kind a",auto simp:get_return_edges_def)
lemma call_has_return_edge:
fixes wfp
assumes "valid_edge wfp a" and "kind a = Q:r↪⇘p⇙fs"
obtains a' where "valid_edge wfp a'" and "∃Q' f'. kind a' = Q'↩⇘p⇙f'"
and "targetnode a' = r"
proof(atomize_elim)
from ‹valid_edge wfp a› ‹kind a = Q:r↪⇘p⇙fs›
obtain prog procs where "Rep_wf_prog wfp = (prog,procs)"
and "prog,procs ⊢ sourcenode a -Q:r↪⇘p⇙fs→ targetnode a"
by(fastforce simp:valid_edge_def)
from ‹prog,procs ⊢ sourcenode a -Q:r↪⇘p⇙fs→ targetnode a›
show "∃a'. valid_edge wfp a' ∧ (∃Q' f'. kind a' = Q'↩⇘p⇙f') ∧ targetnode a' = r"
proof(induct "sourcenode a" "Q:r↪⇘p⇙fs" "targetnode a" rule:PCFG.induct)
case (MainCall l es rets n' ins outs c)
from ‹prog ⊢ Label l -CEdge (p, es, rets)→⇩p n'› obtain l'
where [simp]:"n' = Label l'"
by(fastforce dest:Proc_CFG_Call_Labels)
from MainCall
have "prog,procs ⊢ (p,Exit) -(λcf. snd cf = (Main,Label l'))↩⇘p⇙
(λcf cf'. cf'(rets [:=] map cf outs))→ (Main,Label l')"
by(fastforce intro:MainReturn)
with ‹Rep_wf_prog wfp = (prog,procs)› ‹(Main, n') = r› show ?thesis
by(fastforce simp:valid_edge_def)
next
case (ProcCall px ins outs c l es' rets' l' ins' outs' c' ps)
from ProcCall have "prog,procs ⊢ (p,Exit) -(λcf. snd cf = (px,Label l'))↩⇘p⇙
(λcf cf'. cf'(rets' [:=] map cf outs'))→ (px,Label l')"
by(fastforce intro:ProcReturn)
with ‹Rep_wf_prog wfp = (prog,procs)› ‹(px, Label l') = r› show ?thesis
by(fastforce simp:valid_edge_def)
qed auto
qed
lemma get_return_edges_call_nonempty:
fixes wfp
shows "⟦valid_edge wfp a; kind a = Q:r↪⇘p⇙fs⟧ ⟹ get_return_edges wfp a ≠ {}"
by -(erule call_has_return_edge,(fastforce simp:get_return_edges_def)+)
lemma only_return_edges_in_get_return_edges:
fixes wfp
shows "⟦valid_edge wfp a; kind a = Q:r↪⇘p⇙fs; a' ∈ get_return_edges wfp a⟧
⟹ ∃Q' f'. kind a' = Q'↩⇘p⇙f'"
by(cases "kind a",auto simp:get_return_edges_def)
abbreviation lift_procs :: "wf_prog ⇒ (pname × vname list × vname list) list"
where "⋀wfp. lift_procs wfp ≡ let (prog,procs) = Rep_wf_prog wfp in
map (λx. (fst x,fst(snd x),fst(snd(snd x)))) procs"
subsection ‹Instatiation of the ‹CFG› locale›