Up to index of Isabelle/HOL/Jinja/HRB-Slicing
theory Interpretationheader {* \isaheader{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 "valid_edge wfp a ≡ let (prog,procs) = Rep_wf_prog wfp in
prog,procs \<turnstile> sourcenode a -kind a-> targetnode a"
definition get_return_edges :: "wf_prog => edge => edge set"
where "get_return_edges wfp a ≡
case kind a of Q:r\<hookrightarrow>⇘p⇙fs => {a'. valid_edge wfp a' ∧ (∃Q' f'. kind a' = Q'\<hookleftarrow>⇘p⇙f') ∧
targetnode a' = r}
| _ => {}"
lemma get_return_edges_non_call_empty:
"∀Q r p fs. kind a ≠ Q:r\<hookrightarrow>⇘p⇙fs ==> get_return_edges wfp a = {}"
by(cases "kind a",auto simp:get_return_edges_def)
lemma call_has_return_edge:
assumes "valid_edge wfp a" and "kind a = Q:r\<hookrightarrow>⇘p⇙fs"
obtains a' where "valid_edge wfp a'" and "∃Q' f'. kind a' = Q'\<hookleftarrow>⇘p⇙f'"
and "targetnode a' = r"
proof(atomize_elim)
from `valid_edge wfp a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
obtain prog procs where "Rep_wf_prog wfp = (prog,procs)"
and "prog,procs \<turnstile> sourcenode a -Q:r\<hookrightarrow>⇘p⇙fs-> targetnode a"
by(fastforce simp:valid_edge_def)
from `prog,procs \<turnstile> sourcenode a -Q:r\<hookrightarrow>⇘p⇙fs-> targetnode a`
show "∃a'. valid_edge wfp a' ∧ (∃Q' f'. kind a' = Q'\<hookleftarrow>⇘p⇙f') ∧ targetnode a' = r"
proof(induct "sourcenode a" "Q:r\<hookrightarrow>⇘p⇙fs" "targetnode a" rule:PCFG.induct)
case (MainCall l es rets n' ins outs c)
from `prog \<turnstile> 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 \<turnstile> (p,Exit) -(λcf. snd cf = (Main,Label l'))\<hookleftarrow>⇘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 \<turnstile> (p,Exit) -(λcf. snd cf = (px,Label l'))\<hookleftarrow>⇘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:
"[|valid_edge wfp a; kind a = Q:r\<hookrightarrow>⇘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:
"[|valid_edge wfp a; kind a = Q:r\<hookrightarrow>⇘p⇙fs; a' ∈ get_return_edges wfp a|]
==> ∃Q' f'. kind a' = Q'\<hookleftarrow>⇘p⇙f'"
by(cases "kind a",auto simp:get_return_edges_def)
abbreviation lift_procs :: "wf_prog => (pname × vname list × vname list) list"
where "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 @{text CFG} locale *}
interpretation ProcCFG:
CFG sourcenode targetnode kind "valid_edge wfp" "(Main,Entry)"
get_proc "get_return_edges wfp" "lift_procs wfp" Main
for wfp
proof -
from Rep_wf_prog[of wfp]
obtain prog procs where [simp]:"Rep_wf_prog wfp = (prog,procs)"
by(fastforce simp:wf_prog_def)
hence wf:"well_formed procs" by(fastforce intro:wf_wf_prog)
show "CFG sourcenode targetnode kind (valid_edge wfp) (Main, Entry)
get_proc (get_return_edges wfp) (lift_procs wfp) Main"
proof
fix a assume "valid_edge wfp a" and "targetnode a = (Main, Entry)"
from this wf show False by(auto elim:PCFG.cases simp:valid_edge_def)
next
show "get_proc (Main, Entry) = Main" by simp
next
fix a Q r p fs
assume "valid_edge wfp a" and "kind a = Q:r\<hookrightarrow>⇘p⇙fs"
and "sourcenode a = (Main, Entry)"
thus False by(auto elim:PCFG.cases simp:valid_edge_def)
next
fix a a'
assume "valid_edge wfp a" and "valid_edge wfp a'"
and "sourcenode a = sourcenode a'" and "targetnode a = targetnode a'"
with wf show "a = a'"
by(cases a,cases a',auto dest:Proc_CFG_edge_det simp:valid_edge_def)
next
fix a Q r f
assume "valid_edge wfp a" and "kind a = Q:r\<hookrightarrow>⇘Main⇙f"
from this wf show False by(auto elim:PCFG.cases simp:valid_edge_def)
next
fix a Q' f'
assume "valid_edge wfp a" and "kind a = Q'\<hookleftarrow>⇘Main⇙f'"
from this wf show False by(auto elim:PCFG.cases simp:valid_edge_def)
next
fix a Q r p fs
assume "valid_edge wfp a" and "kind a = Q:r\<hookrightarrow>⇘p⇙fs"
thus "∃ins outs. (p, ins, outs) ∈ set (lift_procs wfp)"
apply(auto simp:valid_edge_def) apply(erule PCFG.cases) apply auto
apply(fastforce dest:Proc_CFG_IEdge_intra_kind simp:intra_kind_def)
apply(fastforce dest:Proc_CFG_IEdge_intra_kind simp:intra_kind_def)
apply(rule_tac x="ins" in exI) apply(rule_tac x="outs" in exI)
apply(rule_tac x="(p,ins,outs,c)" in image_eqI) apply auto
apply(rule_tac x="ins'" in exI) apply(rule_tac x="outs'" in exI)
apply(rule_tac x="(p,ins',outs',c')" in image_eqI) by(auto simp:set_conv_nth)
next
fix a assume "valid_edge wfp a" and "intra_kind (kind a)"
thus "get_proc (sourcenode a) = get_proc (targetnode a)"
by(auto elim:PCFG.cases simp:valid_edge_def intra_kind_def)
next
fix a Q r p fs
assume "valid_edge wfp a" and "kind a = Q:r\<hookrightarrow>⇘p⇙fs"
thus "get_proc (targetnode a) = p" by(auto elim:PCFG.cases simp:valid_edge_def)
next
fix a Q' p f'
assume "valid_edge wfp a" and "kind a = Q'\<hookleftarrow>⇘p⇙f'"
thus "get_proc (sourcenode a) = p" by(auto elim:PCFG.cases simp:valid_edge_def)
next
fix a Q r p fs
assume "valid_edge wfp a" and "kind a = Q:r\<hookrightarrow>⇘p⇙fs"
hence "prog,procs \<turnstile> sourcenode a -kind a-> targetnode a"
by(simp add:valid_edge_def)
from this `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
show "∀a'. valid_edge wfp a' ∧ targetnode a' = targetnode a -->
(∃Qx rx fsx. kind a' = Qx:rx\<hookrightarrow>⇘p⇙fsx)"
proof(induct "sourcenode a" "kind a" "targetnode a" rule:PCFG.induct)
case (MainCall l p' es rets n' ins outs c)
from `λs. True:(Main, n')\<hookrightarrow>⇘p'⇙map interpret es = kind a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
have [simp]:"p' = p" by simp
{ fix a' assume "valid_edge wfp a'" and "targetnode a' = (p', Entry)"
hence "∃Qx rx fsx. kind a' = Qx:rx\<hookrightarrow>⇘p⇙fsx"
by(auto elim:PCFG.cases simp:valid_edge_def) }
with `(p',Entry) = targetnode a` show ?case by simp
next
case (ProcCall px ins outs c l p' es rets l' ins' outs' c' ps)
from `λs. True:(px, Label l')\<hookrightarrow>⇘p'⇙map interpret es = kind a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
have [simp]:"p' = p" by simp
{ fix a' assume "valid_edge wfp a'" and "targetnode a' = (p', Entry)"
hence "∃Qx rx fsx. kind a' = Qx:rx\<hookrightarrow>⇘p⇙fsx"
by(auto elim:PCFG.cases simp:valid_edge_def) }
with `(p', Entry) = targetnode a` show ?case by simp
qed auto
next
fix a Q' p f'
assume "valid_edge wfp a" and "kind a = Q'\<hookleftarrow>⇘p⇙f'"
hence "prog,procs \<turnstile> sourcenode a -kind a-> targetnode a"
by(simp add:valid_edge_def)
from this `kind a = Q'\<hookleftarrow>⇘p⇙f'`
show "∀a'. valid_edge wfp a' ∧ sourcenode a' = sourcenode a -->
(∃Qx fx. kind a' = Qx\<hookleftarrow>⇘p⇙fx)"
proof(induct "sourcenode a" "kind a" "targetnode a" rule:PCFG.induct)
case (MainReturn l p' es rets l' ins outs c)
from `λcf. snd cf = (Main, Label l')\<hookleftarrow>⇘p'⇙λcf cf'. cf'(rets [:=] map cf outs) =
kind a` `kind a = Q'\<hookleftarrow>⇘p⇙f'` have [simp]:"p' = p" by simp
{ fix a' assume "valid_edge wfp a'" and "sourcenode a' = (p', Exit)"
hence "∃Qx fx. kind a' = Qx\<hookleftarrow>⇘p⇙fx"
by(auto elim:PCFG.cases simp:valid_edge_def) }
with `(p', Exit) = sourcenode a` show ?case by simp
next
case (ProcReturn px ins outs c l p' es rets l' ins' outs' c' ps)
from `λcf. snd cf = (px, Label l')\<hookleftarrow>⇘p'⇙λcf cf'. cf'(rets [:=] map cf outs') =
kind a` `kind a = Q'\<hookleftarrow>⇘p⇙f'` have [simp]:"p' = p" by simp
{ fix a' assume "valid_edge wfp a'" and "sourcenode a' = (p', Exit)"
hence "∃Qx fx. kind a' = Qx\<hookleftarrow>⇘p⇙fx"
by(auto elim:PCFG.cases simp:valid_edge_def) }
with `(p', Exit) = sourcenode a` show ?case by simp
qed auto
next
fix a Q r p fs
assume "valid_edge wfp a" and "kind a = Q:r\<hookrightarrow>⇘p⇙fs"
thus "get_return_edges wfp a ≠ {}" by(rule get_return_edges_call_nonempty)
next
fix a a'
assume "valid_edge wfp a" and "a' ∈ get_return_edges wfp a"
thus "valid_edge wfp a'"
by(cases "kind a",auto simp:get_return_edges_def)
next
fix a a'
assume "valid_edge wfp a" and "a' ∈ get_return_edges wfp a"
thus "∃Q r p fs. kind a = Q:r\<hookrightarrow>⇘p⇙fs"
by(cases "kind a")(auto simp:get_return_edges_def)
next
fix a Q r p fs a'
assume "valid_edge wfp a" and "kind a = Q:r\<hookrightarrow>⇘p⇙fs"
and "a' ∈ get_return_edges wfp a"
thus "∃Q' f'. kind a' = Q'\<hookleftarrow>⇘p⇙f'" by(rule only_return_edges_in_get_return_edges)
next
fix a Q' p f'
assume "valid_edge wfp a" and "kind a = Q'\<hookleftarrow>⇘p⇙f'"
hence "prog,procs \<turnstile> sourcenode a -kind a-> targetnode a"
by(simp add:valid_edge_def)
from this `kind a = Q'\<hookleftarrow>⇘p⇙f'`
show "∃!a'. valid_edge wfp a' ∧ (∃Q r fs. kind a' = Q:r\<hookrightarrow>⇘p⇙fs) ∧
a ∈ get_return_edges wfp a'"
proof(induct "sourcenode a" "kind a" "targetnode a" rule:PCFG.induct)
case (MainReturn l px es rets l' ins outs c)
from `λcf. snd cf = (Main, Label l')\<hookleftarrow>⇘px⇙λcf cf'. cf'(rets [:=] map cf outs) =
kind a` `kind a = Q'\<hookleftarrow>⇘p⇙f'` have [simp]:"px = p" by simp
from `prog \<turnstile> Label l -CEdge (px, es, rets)->⇣p Label l'` have "l' = Suc l"
by(fastforce dest:Proc_CFG_Call_Labels)
from `prog \<turnstile> Label l -CEdge (px, es, rets)->⇣p Label l'`
have "containsCall procs prog [] px" by(rule Proc_CFG_Call_containsCall)
with `prog \<turnstile> Label l -CEdge (px, es, rets)->⇣p Label l'`
`(px, ins, outs, c) ∈ set procs`
have "prog,procs \<turnstile> (p,Exit) -(λcf. snd cf = (Main,Label l'))\<hookleftarrow>⇘p⇙
(λcf cf'. cf'(rets [:=] map cf outs))-> (Main,Label l')"
by(fastforce intro:PCFG.MainReturn)
with `(px, Exit) = sourcenode a` `(Main, Label l') = targetnode a`
`λcf. snd cf = (Main, Label l')\<hookleftarrow>⇘px⇙λcf cf'. cf'(rets [:=] map cf outs) =
kind a`
have edge:"prog,procs \<turnstile> sourcenode a -kind a-> targetnode a" by simp
from `prog \<turnstile> Label l -CEdge (px, es, rets)->⇣p Label l'`
`(px, ins, outs, c) ∈ set procs`
have edge':"prog,procs \<turnstile> (Main,Label l)
-(λs. True):(Main,Label l')\<hookrightarrow>⇘p⇙map (λe cf. interpret e cf) es-> (p,Entry)"
by(fastforce intro:MainCall)
show ?case
proof(rule ex_ex1I)
from edge edge' `(Main, Label l') = targetnode a`
`l' = Suc l` `kind a = Q'\<hookleftarrow>⇘p⇙f'`
show "∃a'. valid_edge wfp a' ∧
(∃Q r fs. kind a' = Q:r\<hookrightarrow>⇘p⇙fs) ∧ a ∈ get_return_edges wfp a'"
by(fastforce simp:valid_edge_def get_return_edges_def)
next
fix a' a''
assume "valid_edge wfp a' ∧
(∃Q r fs. kind a' = Q:r\<hookrightarrow>⇘p⇙fs) ∧ a ∈ get_return_edges wfp a'"
and "valid_edge wfp a'' ∧
(∃Q r fs. kind a'' = Q:r\<hookrightarrow>⇘p⇙fs) ∧ a ∈ get_return_edges wfp a''"
then obtain Q r fs Q' r' fs' where "valid_edge wfp a'"
and "kind a' = Q:r\<hookrightarrow>⇘p⇙fs" and "a ∈ get_return_edges wfp a'"
and "valid_edge wfp a''" and "kind a'' = Q':r'\<hookrightarrow>⇘p⇙fs'"
and "a ∈ get_return_edges wfp a''" by blast
from `valid_edge wfp a'` `kind a' = Q:r\<hookrightarrow>⇘p⇙fs`[THEN sym] edge wf `l' = Suc l`
`a ∈ get_return_edges wfp a'` `(Main, Label l') = targetnode a`
have nodes:"sourcenode a' = (Main,Label l) ∧ targetnode a' = (p,Entry)"
apply(auto simp:valid_edge_def get_return_edges_def)
by(erule PCFG.cases,auto dest:Proc_CFG_Call_Labels)+
from `valid_edge wfp a''` `kind a'' = Q':r'\<hookrightarrow>⇘p⇙fs'`[THEN sym] `l' = Suc l`
`a ∈ get_return_edges wfp a''` `(Main, Label l') = targetnode a` wf edge'
have nodes':"sourcenode a'' = (Main,Label l) ∧ targetnode a'' = (p,Entry)"
apply(auto simp:valid_edge_def get_return_edges_def)
by(erule PCFG.cases,auto dest:Proc_CFG_Call_Labels)+
with nodes `valid_edge wfp a'` `valid_edge wfp a''` wf
have "kind a' = kind a''"
by(fastforce dest:Proc_CFG_edge_det simp:valid_edge_def)
with nodes nodes' show "a' = a''" by(cases a',cases a'',auto)
qed
next
case (ProcReturn p' ins outs c l px esx retsx l' ins' outs' c' ps)
from `λcf. snd cf = (p', Label l')\<hookleftarrow>⇘px⇙λcf cf'. cf'(retsx [:=] map cf outs') =
kind a` `kind a = Q'\<hookleftarrow>⇘p⇙f'` have [simp]:"px = p" by simp
from `c \<turnstile> Label l -CEdge (px, esx, retsx)->⇣p Label l'` have "l' = Suc l"
by(fastforce dest:Proc_CFG_Call_Labels)
from `(p',ins,outs,c) ∈ set procs`
`c \<turnstile> Label l -CEdge (px, esx, retsx)->⇣p Label l'`
`(px, ins', outs', c') ∈ set procs` `containsCall procs prog ps p'`
have "prog,procs \<turnstile> (p,Exit) -(λcf. snd cf = (p',Label l'))\<hookleftarrow>⇘p⇙
(λcf cf'. cf'(retsx [:=] map cf outs'))-> (p',Label l')"
by(fastforce intro:PCFG.ProcReturn)
with `(px, Exit) = sourcenode a` `(p', Label l') = targetnode a`
`λcf. snd cf = (p', Label l')\<hookleftarrow>⇘px⇙λcf cf'. cf'(retsx [:=] map cf outs') =
kind a` have edge:"prog,procs \<turnstile> sourcenode a -kind a-> targetnode a" by simp
from `(p',ins,outs,c) ∈ set procs`
`c \<turnstile> Label l -CEdge (px, esx, retsx)->⇣p Label l'`
`(px, ins', outs', c') ∈ set procs` `containsCall procs prog ps p'`
have edge':"prog,procs \<turnstile> (p',Label l)
-(λs. True):(p',Label l')\<hookrightarrow>⇘p⇙map (λe cf. interpret e cf) esx-> (p,Entry)"
by(fastforce intro:ProcCall)
show ?case
proof(rule ex_ex1I)
from edge edge' `(p', Label l') = targetnode a` `l' = Suc l`
`(p', ins, outs, c) ∈ set procs` `kind a = Q'\<hookleftarrow>⇘p⇙f'`
show "∃a'. valid_edge wfp a' ∧
(∃Q r fs. kind a' = Q:r\<hookrightarrow>⇘p⇙fs) ∧ a ∈ get_return_edges wfp a'"
by(fastforce simp:valid_edge_def get_return_edges_def)
next
fix a' a''
assume "valid_edge wfp a' ∧
(∃Q r fs. kind a' = Q:r\<hookrightarrow>⇘p⇙fs) ∧ a ∈ get_return_edges wfp a'"
and "valid_edge wfp a'' ∧
(∃Q r fs. kind a'' = Q:r\<hookrightarrow>⇘p⇙fs) ∧ a ∈ get_return_edges wfp a''"
then obtain Q r fs Q' r' fs' where "valid_edge wfp a'"
and "kind a' = Q:r\<hookrightarrow>⇘p⇙fs" and "a ∈ get_return_edges wfp a'"
and "valid_edge wfp a''" and "kind a'' = Q':r'\<hookrightarrow>⇘p⇙fs'"
and "a ∈ get_return_edges wfp a''" by blast
from `valid_edge wfp a'` `kind a' = Q:r\<hookrightarrow>⇘p⇙fs`[THEN sym]
`a ∈ get_return_edges wfp a'` edge `(p', Label l') = targetnode a` wf
`(p', ins, outs, c) ∈ set procs` `l' = Suc l`
have nodes:"sourcenode a' = (p',Label l) ∧ targetnode a' = (p,Entry)"
apply(auto simp:valid_edge_def get_return_edges_def)
by(erule PCFG.cases,auto dest:Proc_CFG_Call_Labels)+
from `valid_edge wfp a''` `kind a'' = Q':r'\<hookrightarrow>⇘p⇙fs'`[THEN sym]
`a ∈ get_return_edges wfp a''` edge `(p', Label l') = targetnode a` wf
`(p', ins, outs, c) ∈ set procs` `l' = Suc l`
have nodes':"sourcenode a'' = (p',Label l) ∧ targetnode a'' = (p,Entry)"
apply(auto simp:valid_edge_def get_return_edges_def)
by(erule PCFG.cases,auto dest:Proc_CFG_Call_Labels)+
with nodes `valid_edge wfp a'` `valid_edge wfp a''` wf
have "kind a' = kind a''"
by(fastforce dest:Proc_CFG_edge_det simp:valid_edge_def)
with nodes nodes' show "a' = a''" by(cases a',cases a'',auto)
qed
qed auto
next
fix a a'
assume "valid_edge wfp a" and "a' ∈ get_return_edges wfp a"
then obtain Q r p fs l'
where "kind a = Q:r\<hookrightarrow>⇘p⇙fs" and "valid_edge wfp a'"
by(cases "kind a")(fastforce simp:valid_edge_def get_return_edges_def)+
from `valid_edge wfp a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs` `a' ∈ get_return_edges wfp a`
obtain Q' f' where "kind a' = Q'\<hookleftarrow>⇘p⇙f'"
by(fastforce dest!:only_return_edges_in_get_return_edges)
with `valid_edge wfp a'` have "sourcenode a' = (p,Exit)"
by(auto elim:PCFG.cases simp:valid_edge_def)
from `valid_edge wfp a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
have "prog,procs \<turnstile> sourcenode a -Q:r\<hookrightarrow>⇘p⇙fs-> targetnode a"
by(simp add:valid_edge_def)
thus "∃a''. valid_edge wfp a'' ∧ sourcenode a'' = targetnode a ∧
targetnode a'' = sourcenode a' ∧ kind a'' = (λcf. False)⇣\<surd>"
proof(induct "sourcenode a" "Q:r\<hookrightarrow>⇘p⇙fs" "targetnode a" rule:PCFG.induct)
case (MainCall l es rets n' ins outs c)
have "c \<turnstile> Entry -IEdge (λs. False)⇣\<surd>->⇣p Exit" by(rule Proc_CFG_Entry_Exit)
moreover
from `prog \<turnstile> Label l -CEdge (p, es, rets)->⇣p n'`
have "containsCall procs prog [] p" by(rule Proc_CFG_Call_containsCall)
ultimately have "prog,procs \<turnstile> (p,Entry) -(λs. False)⇣\<surd>-> (p,Exit)"
using `(p, ins, outs, c) ∈ set procs` by(fastforce intro:Proc)
with `sourcenode a' = (p,Exit)` `(p, Entry) = targetnode a`[THEN sym]
show ?case by(fastforce simp:valid_edge_def)
next
case (ProcCall px ins outs c l es' rets' l' ins' outs' c' ps)
have "c' \<turnstile> Entry -IEdge (λs. False)⇣\<surd>->⇣p Exit" by(rule Proc_CFG_Entry_Exit)
moreover
from `c \<turnstile> Label l -CEdge (p, es', rets')->⇣p Label l'`
have "containsCall procs c [] p" by(rule Proc_CFG_Call_containsCall)
with `containsCall procs prog ps px` `(px,ins,outs,c) ∈ set procs`
have "containsCall procs prog (ps@[px]) p"
by(rule containsCall_in_proc)
ultimately have "prog,procs \<turnstile> (p,Entry) -(λs. False)⇣\<surd>-> (p,Exit)"
using `(p, ins', outs', c') ∈ set procs` by(fastforce intro:Proc)
with `sourcenode a' = (p,Exit)` `(p, Entry) = targetnode a`[THEN sym]
show ?case by(fastforce simp:valid_edge_def)
qed auto
next
fix a a'
assume "valid_edge wfp a" and "a' ∈ get_return_edges wfp a"
then obtain Q r p fs l'
where "kind a = Q:r\<hookrightarrow>⇘p⇙fs" and "valid_edge wfp a'"
by(cases "kind a")(fastforce simp:valid_edge_def get_return_edges_def)+
from `valid_edge wfp a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs` `a' ∈ get_return_edges wfp a`
obtain Q' f' where "kind a' = Q'\<hookleftarrow>⇘p⇙f'" and "targetnode a' = r"
by(auto simp:get_return_edges_def)
from `valid_edge wfp a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
have "prog,procs \<turnstile> sourcenode a -Q:r\<hookrightarrow>⇘p⇙fs-> targetnode a"
by(simp add:valid_edge_def)
thus "∃a''. valid_edge wfp a'' ∧ sourcenode a'' = sourcenode a ∧
targetnode a'' = targetnode a' ∧ kind a'' = (λcf. False)⇣\<surd>"
proof(induct "sourcenode a" "Q:r\<hookrightarrow>⇘p⇙fs" "targetnode a" rule:PCFG.induct)
case (MainCall l es rets n' ins outs c)
from `prog \<turnstile> Label l -CEdge (p, es, rets)->⇣p n'`
have "prog,procs \<turnstile> (Main,Label l) -(λs. False)⇣\<surd>-> (Main,n')"
by(rule MainCallReturn)
with `(Main, Label l) = sourcenode a`[THEN sym] `targetnode a' = r`
`(Main, n') = r`[THEN sym]
show ?case by(auto simp:valid_edge_def)
next
case (ProcCall px ins outs c l es' rets' l' ins' outs' c' ps)
from `(px,ins,outs,c) ∈ set procs` `containsCall procs prog ps px`
`c \<turnstile> Label l -CEdge (p, es', rets')->⇣p Label l'`
have "prog,procs \<turnstile> (px,Label l) -(λs. False)⇣\<surd>-> (px,Label l')"
by(fastforce intro:ProcCallReturn)
with `(px, Label l) = sourcenode a`[THEN sym] `targetnode a' = r`
`(px, Label l') = r`[THEN sym]
show ?case by(auto simp:valid_edge_def)
qed auto
next
fix a Q r p fs
assume "valid_edge wfp a" and "kind a = Q:r\<hookrightarrow>⇘p⇙fs"
hence "prog,procs \<turnstile> sourcenode a -kind a-> targetnode a"
by(simp add:valid_edge_def)
from this `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
show "∃!a'. valid_edge wfp a' ∧
sourcenode a' = sourcenode a ∧ intra_kind (kind a')"
proof(induct "sourcenode a" "kind a" "targetnode a" rule:PCFG.induct)
case (MainCall l p' es rets n' ins outs c)
show ?thesis
proof(rule ex_ex1I)
from `prog \<turnstile> Label l -CEdge (p', es, rets)->⇣p n'`
have "prog,procs \<turnstile> (Main,Label l) -(λs. False)⇣\<surd>-> (Main,n')"
by(rule MainCallReturn)
with `(Main, Label l) = sourcenode a`[THEN sym]
show "∃a'. valid_edge wfp a' ∧
sourcenode a' = sourcenode a ∧ intra_kind (kind a')"
by(fastforce simp:valid_edge_def intra_kind_def)
next
fix a' a''
assume "valid_edge wfp a' ∧ sourcenode a' = sourcenode a ∧
intra_kind (kind a')" and "valid_edge wfp a'' ∧
sourcenode a'' = sourcenode a ∧ intra_kind (kind a'')"
hence "valid_edge wfp a'" and "sourcenode a' = sourcenode a"
and "intra_kind (kind a')" and "valid_edge wfp a''"
and "sourcenode a'' = sourcenode a" and "intra_kind (kind a'')" by simp_all
from `valid_edge wfp a'` `sourcenode a' = sourcenode a`
`intra_kind (kind a')` `prog \<turnstile> Label l -CEdge (p', es, rets)->⇣p n'`
`(Main, Label l) = sourcenode a` wf
have "targetnode a' = (Main,Label (Suc l))"
by(auto elim!:PCFG.cases dest:Proc_CFG_Call_Intra_edge_not_same_source
Proc_CFG_Call_Labels simp:intra_kind_def valid_edge_def)
from `valid_edge wfp a''` `sourcenode a'' = sourcenode a`
`intra_kind (kind a'')` `prog \<turnstile> Label l -CEdge (p', es, rets)->⇣p n'`
`(Main, Label l) = sourcenode a` wf
have "targetnode a'' = (Main,Label (Suc l))"
by(auto elim!:PCFG.cases dest:Proc_CFG_Call_Intra_edge_not_same_source
Proc_CFG_Call_Labels simp:intra_kind_def valid_edge_def)
with `valid_edge wfp a'` `sourcenode a' = sourcenode a`
`valid_edge wfp a''` `sourcenode a'' = sourcenode a`
`targetnode a' = (Main,Label (Suc l))` wf
show "a' = a''" by(cases a',cases a'')
(auto dest:Proc_CFG_edge_det simp:valid_edge_def)
qed
next
case (ProcCall px ins outs c l p' es' rets' l' ins' outs' c' ps)
show ?thesis
proof(rule ex_ex1I)
from `(px, ins, outs, c) ∈ set procs` `containsCall procs prog ps px`
`c \<turnstile> Label l -CEdge (p', es', rets')->⇣p Label l'`
have "prog,procs \<turnstile> (px,Label l) -(λs. False)⇣\<surd>-> (px,Label l')"
by -(rule ProcCallReturn)
with `(px, Label l) = sourcenode a`[THEN sym]
show "∃a'. valid_edge wfp a' ∧ sourcenode a' = sourcenode a ∧
intra_kind (kind a')"
by(fastforce simp:valid_edge_def intra_kind_def)
next
fix a' a''
assume "valid_edge wfp a' ∧ sourcenode a' = sourcenode a ∧
intra_kind (kind a')" and "valid_edge wfp a'' ∧
sourcenode a'' = sourcenode a ∧ intra_kind (kind a'')"
hence "valid_edge wfp a'" and "sourcenode a' = sourcenode a"
and "intra_kind (kind a')" and "valid_edge wfp a''"
and "sourcenode a'' = sourcenode a" and "intra_kind (kind a'')" by simp_all
from `valid_edge wfp a'` `sourcenode a' = sourcenode a`
`intra_kind (kind a')` `(px, ins, outs, c) ∈ set procs`
`c \<turnstile> Label l -CEdge (p', es', rets')->⇣p Label l'`
`(p', ins', outs', c') ∈ set procs` wf
`containsCall procs prog ps px` `(px, Label l) = sourcenode a`
have "targetnode a' = (px,Label (Suc l))"
apply(auto simp:valid_edge_def) apply(erule PCFG.cases)
by(auto dest:Proc_CFG_Call_Intra_edge_not_same_source
Proc_CFG_Call_nodes_eq Proc_CFG_Call_Labels simp:intra_kind_def)
from `valid_edge wfp a''` `sourcenode a'' = sourcenode a`
`intra_kind (kind a'')` `(px, ins, outs, c) ∈ set procs`
`c \<turnstile> Label l -CEdge (p', es', rets')->⇣p Label l'`
`(p', ins', outs', c') ∈ set procs` wf
`containsCall procs prog ps px` `(px, Label l) = sourcenode a`
have "targetnode a'' = (px,Label (Suc l))"
apply(auto simp:valid_edge_def) apply(erule PCFG.cases)
by(auto dest:Proc_CFG_Call_Intra_edge_not_same_source
Proc_CFG_Call_nodes_eq Proc_CFG_Call_Labels simp:intra_kind_def)
with `valid_edge wfp a'` `sourcenode a' = sourcenode a`
`valid_edge wfp a''` `sourcenode a'' = sourcenode a`
`targetnode a' = (px,Label (Suc l))` wf
show "a' = a''" by(cases a',cases a'')
(auto dest:Proc_CFG_edge_det simp:valid_edge_def)
qed
qed auto
next
fix a Q' p f'
assume "valid_edge wfp a" and "kind a = Q'\<hookleftarrow>⇘p⇙f'"
hence "prog,procs \<turnstile> sourcenode a -kind a-> targetnode a"
by(simp add:valid_edge_def)
from this `kind a = Q'\<hookleftarrow>⇘p⇙f'`
show "∃!a'. valid_edge wfp a' ∧
targetnode a' = targetnode a ∧ intra_kind (kind a')"
proof(induct "sourcenode a" "kind a" "targetnode a" rule:PCFG.induct)
case (MainReturn l p' es rets l' ins outs c)
show ?thesis
proof(rule ex_ex1I)
from `prog \<turnstile> Label l -CEdge (p', es, rets)->⇣p Label l'`
have "prog,procs \<turnstile> (Main,Label l) -(λs. False)⇣\<surd>->
(Main,Label l')" by(rule MainCallReturn)
with `(Main, Label l') = targetnode a`[THEN sym]
show "∃a'. valid_edge wfp a' ∧
targetnode a' = targetnode a ∧ intra_kind (kind a')"
by(fastforce simp:valid_edge_def intra_kind_def)
next
fix a' a''
assume "valid_edge wfp a' ∧ targetnode a' = targetnode a ∧
intra_kind (kind a')" and "valid_edge wfp a'' ∧
targetnode a'' = targetnode a ∧ intra_kind (kind a'')"
hence "valid_edge wfp a'" and "targetnode a' = targetnode a"
and "intra_kind (kind a')" and "valid_edge wfp a''"
and "targetnode a'' = targetnode a" and "intra_kind (kind a'')" by simp_all
from `valid_edge wfp a'` `targetnode a' = targetnode a`
`intra_kind (kind a')` `prog \<turnstile> Label l -CEdge (p', es, rets)->⇣p Label l'`
`(Main, Label l') = targetnode a` wf
have "sourcenode a' = (Main,Label l)"
apply(auto elim!:PCFG.cases dest:Proc_CFG_Call_Intra_edge_not_same_target
simp:valid_edge_def intra_kind_def)
by(fastforce dest:Proc_CFG_Call_nodes_eq' Proc_CFG_Call_Labels)
from `valid_edge wfp a''` `targetnode a'' = targetnode a`
`intra_kind (kind a'')` `prog \<turnstile> Label l -CEdge (p', es, rets)->⇣p Label l'`
`(Main, Label l') = targetnode a` wf
have "sourcenode a'' = (Main,Label l)"
apply(auto elim!:PCFG.cases dest:Proc_CFG_Call_Intra_edge_not_same_target
simp:valid_edge_def intra_kind_def)
by(fastforce dest:Proc_CFG_Call_nodes_eq' Proc_CFG_Call_Labels)
with `valid_edge wfp a'` `targetnode a' = targetnode a`
`valid_edge wfp a''` `targetnode a'' = targetnode a`
`sourcenode a' = (Main,Label l)` wf
show "a' = a''" by(cases a',cases a'')
(auto dest:Proc_CFG_edge_det simp:valid_edge_def)
qed
next
case (ProcReturn px ins outs c l p' es' rets' l' ins' outs' c' ps)
show ?thesis
proof(rule ex_ex1I)
from `(px, ins, outs, c) ∈ set procs` `containsCall procs prog ps px`
`c \<turnstile> Label l -CEdge (p', es', rets')->⇣p Label l'`
have "prog,procs \<turnstile> (px,Label l) -(λs. False)⇣\<surd>-> (px,Label l')"
by -(rule ProcCallReturn)
with `(px, Label l') = targetnode a`[THEN sym]
show "∃a'. valid_edge wfp a' ∧
targetnode a' = targetnode a ∧ intra_kind (kind a')"
by(fastforce simp:valid_edge_def intra_kind_def)
next
fix a' a''
assume "valid_edge wfp a' ∧ targetnode a' = targetnode a ∧
intra_kind (kind a')" and "valid_edge wfp a'' ∧
targetnode a'' = targetnode a ∧ intra_kind (kind a'')"
hence "valid_edge wfp a'" and "targetnode a' = targetnode a"
and "intra_kind (kind a')" and "valid_edge wfp a''"
and "targetnode a'' = targetnode a" and "intra_kind (kind a'')" by simp_all
from `valid_edge wfp a'` `targetnode a' = targetnode a`
`intra_kind (kind a')` `(px, ins, outs, c) ∈ set procs`
`(p', ins', outs', c') ∈ set procs` wf
`c \<turnstile> Label l -CEdge (p', es', rets')->⇣p Label l'`
`containsCall procs prog ps px` `(px, Label l') = targetnode a`
have "sourcenode a' = (px,Label l)"
apply(auto simp:valid_edge_def) apply(erule PCFG.cases)
by(auto dest:Proc_CFG_Call_Intra_edge_not_same_target
Proc_CFG_Call_nodes_eq' simp:intra_kind_def)
from `valid_edge wfp a''` `targetnode a'' = targetnode a`
`intra_kind (kind a'')` `(px, ins, outs, c) ∈ set procs`
`(p', ins', outs', c') ∈ set procs` wf
`c \<turnstile> Label l -CEdge (p', es', rets')->⇣p Label l'`
`containsCall procs prog ps px` `(px, Label l') = targetnode a`
have "sourcenode a'' = (px,Label l)"
apply(auto simp:valid_edge_def) apply(erule PCFG.cases)
by(auto dest:Proc_CFG_Call_Intra_edge_not_same_target
Proc_CFG_Call_nodes_eq' simp:intra_kind_def)
with `valid_edge wfp a'` `targetnode a' = targetnode a`
`valid_edge wfp a''` `targetnode a'' = targetnode a`
`sourcenode a' = (px,Label l)` wf
show "a' = a''" by(cases a',cases a'')
(auto dest:Proc_CFG_edge_det simp:valid_edge_def)
qed
qed auto
next
fix a a' Q⇣1 r⇣1 p fs⇣1 Q⇣2 r⇣2 fs⇣2
assume "valid_edge wfp a" and "valid_edge wfp a'"
and "kind a = Q⇣1:r⇣1\<hookrightarrow>⇘p⇙fs⇣1" and "kind a' = Q⇣2:r⇣2\<hookrightarrow>⇘p⇙fs⇣2"
thus "targetnode a = targetnode a'" by(auto elim!:PCFG.cases simp:valid_edge_def)
next
from wf show "distinct_fst (lift_procs wfp)"
by(fastforce simp:well_formed_def distinct_fst_def o_def)
next
fix p ins outs assume "(p, ins, outs) ∈ set (lift_procs wfp)"
from `(p, ins, outs) ∈ set (lift_procs wfp)` wf
show "distinct ins" by(fastforce simp:well_formed_def wf_proc_def)
next
fix p ins outs assume "(p, ins, outs) ∈ set (lift_procs wfp)"
from `(p, ins, outs) ∈ set (lift_procs wfp)` wf
show "distinct outs" by(fastforce simp:well_formed_def wf_proc_def)
qed
qed
subsection {* Instatiation of the @{text CFGExit} locale *}
interpretation ProcCFGExit:
CFGExit sourcenode targetnode kind "valid_edge wfp" "(Main,Entry)"
get_proc "get_return_edges wfp" "lift_procs wfp" Main "(Main,Exit)"
for wfp
proof -
from Rep_wf_prog[of wfp]
obtain prog procs where [simp]:"Rep_wf_prog wfp = (prog,procs)"
by(fastforce simp:wf_prog_def)
hence wf:"well_formed procs" by(fastforce intro:wf_wf_prog)
show "CFGExit sourcenode targetnode kind (valid_edge wfp) (Main, Entry)
get_proc (get_return_edges wfp) (lift_procs wfp) Main (Main, Exit)"
proof
fix a assume "valid_edge wfp a" and "sourcenode a = (Main, Exit)"
with wf show False by(auto elim:PCFG.cases simp:valid_edge_def)
next
show "get_proc (Main, Exit) = Main" by simp
next
fix a Q p f
assume "valid_edge wfp a" and "kind a = Q\<hookleftarrow>⇘p⇙f"
and "targetnode a = (Main, Exit)"
thus False by(auto elim:PCFG.cases simp:valid_edge_def)
next
have "prog,procs \<turnstile> (Main,Entry) -(λs. False)⇣\<surd>-> (Main,Exit)"
by(fastforce intro:Main Proc_CFG_Entry_Exit)
thus "∃a. valid_edge wfp a ∧
sourcenode a = (Main, Entry) ∧
targetnode a = (Main, Exit) ∧ kind a = (λs. False)⇣\<surd>"
by(fastforce simp:valid_edge_def)
qed
qed
end