# Theory WellFormed

```section ‹Instantiate well-formedness locales with Proc CFG›

theory WellFormed imports Interpretation Labels "../StaticInter/CFGExit_wf" begin

subsection ‹Determining the first atomic command›

fun fst_cmd :: "cmd ⇒ cmd"
where "fst_cmd (c⇩1;;c⇩2) = fst_cmd c⇩1"
| "fst_cmd c = c"

lemma Proc_CFG_Call_target_fst_cmd_Skip:
"⟦labels prog l' c; prog ⊢ n -CEdge (p,es,rets)→⇩p Label l'⟧
⟹ fst_cmd c = Skip"
proof(induct arbitrary:n rule:labels.induct)
case (Labels_Seq1 c⇩1 l c c⇩2)
note IH = ‹⋀n. c⇩1 ⊢ n -CEdge (p, es, rets)→⇩p Label l ⟹ fst_cmd c = Skip›
from ‹c⇩1;; c⇩2 ⊢ n -CEdge (p, es, rets)→⇩p Label l› ‹labels c⇩1 l c›
have "c⇩1 ⊢ n -CEdge (p, es, rets)→⇩p Label l"
apply - apply(erule Proc_CFG.cases,auto dest:Proc_CFG_Call_Labels)
by(case_tac n')(auto dest:label_less_num_inner_nodes)
from IH[OF this] show ?case by simp
next
case (Labels_Seq2 c⇩2 l c c⇩1)
note IH = ‹⋀n. c⇩2 ⊢ n -CEdge (p, es, rets)→⇩p Label l ⟹ fst_cmd c = Skip›
from ‹c⇩1;; c⇩2 ⊢ n -CEdge (p, es, rets)→⇩p Label (l + #:c⇩1)› ‹labels c⇩2 l c›
obtain nx where "c⇩2 ⊢ nx -CEdge (p, es, rets)→⇩p Label l"
apply - apply(erule Proc_CFG.cases)
apply(auto dest:Proc_CFG_targetlabel_less_num_nodes Proc_CFG_Call_Labels)
by(case_tac n') auto
from IH[OF this] show ?case by simp
next
case (Labels_CondTrue c⇩1 l c b c⇩2)
note IH = ‹⋀n. c⇩1 ⊢ n -CEdge (p, es, rets)→⇩p Label l ⟹ fst_cmd c = Skip›
from ‹if (b) c⇩1 else c⇩2 ⊢ n -CEdge (p, es, rets)→⇩p Label (l + 1)› ‹labels c⇩1 l c›
obtain nx where "c⇩1 ⊢ nx -CEdge (p, es, rets)→⇩p Label l"
apply - apply(erule Proc_CFG.cases,auto)
apply(case_tac n') apply auto
by(case_tac n')(auto dest:label_less_num_inner_nodes)
from IH[OF this] show ?case by simp
next
case (Labels_CondFalse c⇩2 l c b c⇩1)
note IH = ‹⋀n. c⇩2 ⊢ n -CEdge (p, es, rets)→⇩p Label l ⟹ fst_cmd c = Skip›
from ‹if (b) c⇩1 else c⇩2 ⊢ n -CEdge (p, es, rets)→⇩p Label (l + #:c⇩1 + 1)›
‹labels c⇩2 l c›
obtain nx where "c⇩2 ⊢ nx -CEdge (p, es, rets)→⇩p Label l"
apply - apply(erule Proc_CFG.cases,auto)
apply(case_tac n') apply(auto dest:Proc_CFG_targetlabel_less_num_nodes)
by(case_tac n') auto
from IH[OF this] show ?case by simp
next
case (Labels_WhileBody c' l c b)
note IH = ‹⋀n. c' ⊢ n -CEdge (p, es, rets)→⇩p Label l ⟹ fst_cmd c = Skip›
from ‹while (b) c' ⊢ n -CEdge (p, es, rets)→⇩p Label (l + 2)› ‹labels c' l c›
obtain nx where "c' ⊢ nx -CEdge (p, es, rets)→⇩p Label l"
apply - apply(erule Proc_CFG.cases,auto)
by(case_tac n') auto
from IH[OF this] show ?case by simp
next
case (Labels_Call px esx retsx)
from ‹Call px esx retsx ⊢ n -CEdge (p, es, rets)→⇩p Label 1›
show ?case by(fastforce elim:Proc_CFG.cases)
qed(auto dest:Proc_CFG_Call_Labels)

lemma Proc_CFG_Call_source_fst_cmd_Call:
"⟦labels prog l c; prog ⊢ Label l -CEdge (p,es,rets)→⇩p n'⟧
⟹ ∃p es rets. fst_cmd c = Call p es rets"
proof(induct arbitrary:n' rule:labels.induct)
case (Labels_Base c n')
from ‹c ⊢ Label 0 -CEdge (p, es, rets)→⇩p n'› show ?case
by(induct c "Label 0" "CEdge (p, es, rets)" n' rule:Proc_CFG.induct) auto
next
case (Labels_LAss V e n')
from ‹V:=e ⊢ Label 1 -CEdge (p, es, rets)→⇩p n'› show ?case
by(fastforce elim:Proc_CFG.cases)
next
case (Labels_Seq1 c⇩1 l c c⇩2)
note IH = ‹⋀n'. c⇩1 ⊢ Label l -CEdge (p, es, rets)→⇩p n'
⟹ ∃p es rets. fst_cmd c = Call p es rets›
from ‹c⇩1;; c⇩2 ⊢ Label l -CEdge (p, es, rets)→⇩p n'› ‹labels c⇩1 l c›
have "c⇩1 ⊢ Label l -CEdge (p, es, rets)→⇩p n'"
apply - apply(erule Proc_CFG.cases,auto dest:Proc_CFG_Call_Labels)
by(case_tac n)(auto dest:label_less_num_inner_nodes)
from IH[OF this] show ?case by simp
next
case (Labels_Seq2 c⇩2 l c c⇩1)
note IH = ‹⋀n'. c⇩2 ⊢ Label l -CEdge (p, es, rets)→⇩p n'
⟹ ∃p es rets. fst_cmd c = Call p es rets›
from ‹c⇩1;; c⇩2 ⊢ Label (l + #:c⇩1) -CEdge (p, es, rets)→⇩p n'› ‹labels c⇩2 l c›
obtain nx where "c⇩2 ⊢ Label l -CEdge (p, es, rets)→⇩p nx"
apply - apply(erule Proc_CFG.cases)
apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes Proc_CFG_Call_Labels)
by(case_tac n) auto
from IH[OF this] show ?case by simp
next
case (Labels_CondTrue c⇩1 l c b c⇩2)
note IH = ‹⋀n'. c⇩1 ⊢ Label l -CEdge (p, es, rets)→⇩p n'
⟹ ∃p es rets. fst_cmd c = Call p es rets›
from ‹if (b) c⇩1 else c⇩2 ⊢ Label (l + 1) -CEdge (p, es, rets)→⇩p n'› ‹labels c⇩1 l c›
obtain nx where "c⇩1 ⊢ Label l -CEdge (p, es, rets)→⇩p nx"
apply - apply(erule Proc_CFG.cases,auto)
apply(case_tac n) apply auto
by(case_tac n)(auto dest:label_less_num_inner_nodes)
from IH[OF this] show ?case by simp
next
case (Labels_CondFalse c⇩2 l c b c⇩1)
note IH = ‹⋀n'. c⇩2 ⊢ Label l -CEdge (p, es, rets)→⇩p n'
⟹ ∃p es rets. fst_cmd c = Call p es rets›
from ‹if (b) c⇩1 else c⇩2 ⊢ Label  (l + #:c⇩1 + 1)-CEdge (p, es, rets)→⇩p n'›
‹labels c⇩2 l c›
obtain nx where "c⇩2 ⊢ Label l -CEdge (p, es, rets)→⇩p nx"
apply - apply(erule Proc_CFG.cases,auto)
apply(case_tac n) apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
by(case_tac n) auto
from IH[OF this] show ?case by simp
next
case (Labels_WhileBody c' l c b)
note IH = ‹⋀n'. c' ⊢ Label l -CEdge (p, es, rets)→⇩p n'
⟹ ∃p es rets. fst_cmd c = Call p es rets›
from ‹while (b) c' ⊢ Label (l + 2) -CEdge (p, es, rets)→⇩p n'› ‹labels c' l c›
obtain nx where "c' ⊢ Label l -CEdge (p, es, rets)→⇩p nx"
apply - apply(erule Proc_CFG.cases,auto dest:Proc_CFG_Call_Labels)
by(case_tac n) auto
from IH[OF this] show ?case by simp
next
case (Labels_WhileExit b c' n')
have "while (b) c' ⊢ Label 1 -IEdge ⇑id→⇩p Exit" by(rule Proc_CFG_WhileFalseSkip)
with ‹while (b) c' ⊢ Label 1 -CEdge (p, es, rets)→⇩p n'›
have False by(rule Proc_CFG_Call_Intra_edge_not_same_source)
thus ?case by simp
next
case (Labels_Call px esx retsx)
from ‹Call px esx retsx ⊢ Label 1 -CEdge (p, es, rets)→⇩p n'›
show ?case by(fastforce elim:Proc_CFG.cases)
qed

subsection ‹Definition of ‹Def› and ‹Use› sets›

subsubsection ‹‹ParamDefs››

lemma PCFG_CallEdge_THE_rets:
"prog ⊢ n -CEdge (p,es,rets)→⇩p n'
⟹ (THE rets'. ∃p' es' n. prog ⊢ n -CEdge(p',es',rets')→⇩p n') = rets"
by(fastforce intro:the_equality dest:Proc_CFG_Call_nodes_eq')

definition ParamDefs_proc :: "cmd ⇒ label ⇒ vname list"
where "ParamDefs_proc c n ≡
if (∃n' p' es' rets'. c ⊢ n' -CEdge(p',es',rets')→⇩p n) then
(THE rets'. ∃p' es' n'. c ⊢ n' -CEdge(p',es',rets')→⇩p n)
else []"

lemma in_procs_THE_in_procs_cmd:
"⟦well_formed procs; (p,ins,outs,c) ∈ set procs⟧
⟹ (THE c'. ∃ins' outs'. (p,ins',outs',c') ∈ set procs) = c"
by(fastforce intro:the_equality)

definition ParamDefs :: "wf_prog ⇒ node ⇒ vname list"
where "ParamDefs wfp n ≡ let (prog,procs) = Rep_wf_prog wfp; (p,l) = n in
(if (p = Main) then ParamDefs_proc prog l
else (if (∃ins outs c. (p,ins,outs,c) ∈ set procs)
then ParamDefs_proc (THE c'. ∃ins' outs'. (p,ins',outs',c') ∈ set procs) l
else []))"

lemma ParamDefs_Main_Return_target:
"⟦Rep_wf_prog wfp = (prog,procs); prog ⊢ n -CEdge(p',es,rets)→⇩p n'⟧
⟹ ParamDefs wfp (Main,n') = rets"
by(fastforce dest:PCFG_CallEdge_THE_rets simp:ParamDefs_def ParamDefs_proc_def)

lemma ParamDefs_Proc_Return_target:
assumes "Rep_wf_prog wfp = (prog,procs)"
and "(p,ins,outs,c) ∈ set procs" and "c ⊢ n -CEdge(p',es,rets)→⇩p n'"
shows "ParamDefs wfp (p,n') = rets"
proof -
from ‹Rep_wf_prog wfp = (prog,procs)› have "well_formed procs"
by(fastforce intro:wf_wf_prog)
with ‹(p,ins,outs,c) ∈ set procs› have "p ≠ Main" by fastforce
moreover
from ‹well_formed procs› ‹(p,ins,outs,c) ∈ set procs›
have "(THE c'. ∃ins' outs'. (p,ins',outs',c') ∈ set procs) = c"
by(rule in_procs_THE_in_procs_cmd)
ultimately show ?thesis using assms
by(fastforce dest:PCFG_CallEdge_THE_rets simp:ParamDefs_def ParamDefs_proc_def)
qed

lemma ParamDefs_Main_IEdge_Nil:
"⟦Rep_wf_prog wfp = (prog,procs); prog ⊢ n -IEdge et→⇩p n'⟧
⟹ ParamDefs wfp (Main,n') = []"
by(fastforce dest:Proc_CFG_Call_Intra_edge_not_same_target
simp:ParamDefs_def ParamDefs_proc_def)

lemma ParamDefs_Proc_IEdge_Nil:
assumes "Rep_wf_prog wfp = (prog,procs)"
and "(p,ins,outs,c) ∈ set procs" and "c ⊢ n -IEdge et→⇩p n'"
shows "ParamDefs wfp (p,n') = []"
proof -
from ‹Rep_wf_prog wfp = (prog,procs)› have "well_formed procs"
by(fastforce intro:wf_wf_prog)
with ‹(p,ins,outs,c) ∈ set procs› have "p ≠ Main" by fastforce
moreover
from ‹well_formed procs› ‹(p,ins,outs,c) ∈ set procs›
have "(THE c'. ∃ins' outs'. (p,ins',outs',c') ∈ set procs) = c"
by(rule in_procs_THE_in_procs_cmd)
ultimately show ?thesis using assms
by(fastforce dest:Proc_CFG_Call_Intra_edge_not_same_target
simp:ParamDefs_def ParamDefs_proc_def)
qed

lemma ParamDefs_Main_CEdge_Nil:
"⟦Rep_wf_prog wfp = (prog,procs); prog ⊢ n' -CEdge(p',es,rets)→⇩p n''⟧
⟹ ParamDefs wfp (Main,n') = []"
by(fastforce dest:Proc_CFG_Call_targetnode_no_Call_sourcenode
simp:ParamDefs_def ParamDefs_proc_def)

lemma ParamDefs_Proc_CEdge_Nil:
assumes "Rep_wf_prog wfp = (prog,procs)"
and "(p,ins,outs,c) ∈ set procs" and "c ⊢ n' -CEdge(p',es,rets)→⇩p n''"
shows "ParamDefs wfp (p,n') = []"
proof -
from ‹Rep_wf_prog wfp = (prog,procs)› have "well_formed procs"
by(fastforce intro:wf_wf_prog)
with ‹(p,ins,outs,c) ∈ set procs› have "p ≠ Main" by fastforce
moreover
from ‹well_formed procs› ‹(p,ins,outs,c) ∈ set procs›
have "(THE c'. ∃ins' outs'. (p,ins',outs',c') ∈ set procs) = c"
by(rule in_procs_THE_in_procs_cmd)
ultimately show ?thesis using assms
by(fastforce dest:Proc_CFG_Call_targetnode_no_Call_sourcenode
simp:ParamDefs_def ParamDefs_proc_def)
qed

lemma assumes "valid_edge wfp a" and "kind a = Q'↩⇘p⇙f'"
and "(p, ins, outs) ∈ set (lift_procs wfp)"
shows ParamDefs_length:"length (ParamDefs wfp (targetnode a)) = length outs"
(is ?length)
and Return_update:"f' cf cf' = cf'(ParamDefs wfp (targetnode a) [:=] map cf outs)"
(is ?update)
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 prog procs" by(rule wf_wf_prog)
hence wf:"well_formed procs" by fastforce
from assms have "prog,procs ⊢ sourcenode a -kind a→ targetnode a"
from this ‹kind a = Q'↩⇘p⇙f'› wf have "?length ∧ ?update"
proof(induct "sourcenode a" "kind a" "targetnode a" rule:PCFG.induct)
case (MainReturn l p' es rets l' insx outsx cx)
from ‹λcf. snd cf = (Main, Label l')↩⇘p'⇙λcf cf'. cf'(rets [:=] map cf outsx) =
kind a› ‹kind a = Q'↩⇘p⇙f'› have "p' = p"
and f':"f' = (λcf cf'. cf'(rets [:=] map cf outsx))" by simp_all
with ‹well_formed procs› ‹(p', insx, outsx, cx) ∈ set procs›
‹(p, ins, outs) ∈ set (lift_procs wfp)›
have [simp]:"outsx = outs" by fastforce
from ‹prog ⊢ Label l -CEdge (p', es, rets)→⇩p Label l'›
have "containsCall procs prog [] p'" by(rule Proc_CFG_Call_containsCall)
with ‹wf prog procs› ‹(p', insx, outsx, cx) ∈ set procs›
‹prog ⊢ Label l -CEdge (p', es, rets)→⇩p Label l'›
have "length rets = length outs" by fastforce
from ‹prog ⊢ Label l -CEdge (p', es, rets)→⇩p Label l'›
have "ParamDefs wfp (Main,Label l') = rets"
by(fastforce intro:ParamDefs_Main_Return_target)
with ‹(Main, Label l') = targetnode a› f' ‹length rets = length outs›
show ?thesis by simp
next
case (ProcReturn px insx outsx cx l p' es rets l' ins' outs' c' ps)
from ‹λcf. snd cf = (px, Label l')↩⇘p'⇙λcf cf'. cf'(rets [:=] map cf outs') =
kind a› ‹kind a = Q'↩⇘p⇙f'›
have "p' = p" and f':"f' = (λcf cf'. cf'(rets [:=] map cf outs'))"
by simp_all
with ‹well_formed procs› ‹(p', ins', outs', c') ∈ set procs›
‹(p, ins, outs) ∈ set (lift_procs wfp)›
have [simp]:"outs' = outs" by fastforce
from ‹cx ⊢ Label l -CEdge (p', es, rets)→⇩p Label l'›
have "containsCall procs cx [] p'" by(rule Proc_CFG_Call_containsCall)
with ‹containsCall procs prog ps px› ‹(px, insx, outsx, cx) ∈ set procs›
have "containsCall procs prog (ps@[px]) p'" by(rule containsCall_in_proc)
with ‹wf prog procs› ‹(p', ins', outs', c') ∈ set procs›
‹cx ⊢ Label l -CEdge (p', es, rets)→⇩p Label l'›
have "length rets = length outs" by fastforce
from ‹(px, insx, outsx, cx) ∈ set procs›
‹cx ⊢ Label l -CEdge (p', es, rets)→⇩p Label l'›
have "ParamDefs wfp (px,Label l') = rets"
by(fastforce intro:ParamDefs_Proc_Return_target simp:set_conv_nth)
with ‹(px, Label l') = targetnode a› f' ‹length rets = length outs›
show ?thesis by simp
qed auto
thus "?length" and "?update" by simp_all
qed

subsubsection ‹‹ParamUses››

fun fv :: "expr ⇒ vname set"
where
"fv (Val v)       = {}"
| "fv (Var V)       = {V}"
| "fv (e1 «bop» e2) = (fv e1 ∪ fv e2)"

lemma rhs_interpret_eq:
"⟦state_check cf e v'; ∀V ∈ fv e. cf V = cf' V⟧
⟹ state_check cf' e v'"
proof(induct e arbitrary:v')
case (Val v)
from ‹state_check cf (Val v) v'› have "v' = Some v"
by(fastforce elim:interpret.cases)
thus ?case by simp
next
case (Var V)
hence "cf' (V) = v'" by(fastforce elim:interpret.cases)
thus ?case by simp
next
case (BinOp b1 bop b2)
note IH1 = ‹⋀v'. ⟦state_check cf b1 v'; ∀V∈fv b1. cf V = cf' V⟧
⟹ state_check cf' b1 v'›
note IH2 = ‹⋀v'. ⟦state_check cf b2 v'; ∀V∈fv b2. cf V = cf' V⟧
⟹ state_check cf' b2 v'›
from ‹∀V ∈ fv (b1 «bop» b2). cf V = cf' V› have "∀V ∈ fv b1. cf V = cf' V"
and "∀V ∈ fv b2. cf V = cf' V" by simp_all
from ‹state_check cf (b1 «bop» b2) v'›
have "((state_check cf b1 None ∧ v' = None) ∨
(state_check cf b2 None ∧ v' = None)) ∨
(∃v⇩1 v⇩2. state_check cf b1 (Some v⇩1) ∧ state_check cf b2 (Some v⇩2) ∧
binop bop v⇩1 v⇩2 = v')"
apply(cases "interpret b1 cf",simp)
apply(cases "interpret b2 cf",simp)
by(case_tac "binop bop a aa",simp+)
thus ?case apply -
proof(erule disjE)+
assume "state_check cf b1 None ∧ v' = None"
hence check:"state_check cf b1 None" and "v' = None" by simp_all
from IH1[OF check ‹∀V ∈ fv b1. cf V = cf' V›] have "state_check cf' b1 None" .
with ‹v' = None› show ?case by simp
next
assume "state_check cf b2 None ∧ v' = None"
hence check:"state_check cf b2 None" and "v' = None" by simp_all
from IH2[OF check ‹∀V ∈ fv b2. cf V = cf' V›] have "state_check cf' b2 None" .
with ‹v' = None› show ?case by(cases "interpret b1 cf'") simp+
next
assume "∃v⇩1 v⇩2. state_check cf b1 (Some v⇩1) ∧
state_check cf b2 (Some v⇩2) ∧ binop bop v⇩1 v⇩2 = v'"
then obtain v⇩1 v⇩2 where "state_check cf b1 (Some v⇩1)"
and "state_check cf b2 (Some v⇩2)" and "binop bop v⇩1 v⇩2 = v'" by blast
from ‹∀V ∈ fv (b1 «bop» b2). cf V = cf' V› have "∀V ∈ fv b1. cf V = cf' V"
by simp
from IH1[OF ‹state_check cf b1 (Some v⇩1)› this]
have "interpret b1 cf' = Some v⇩1" .
from ‹∀V ∈ fv (b1 «bop» b2). cf V = cf' V› have "∀V ∈ fv b2. cf V = cf' V"
by simp
from IH2[OF ‹state_check cf b2 (Some v⇩2)› this]
have "interpret b2 cf' = Some v⇩2" .
with ‹interpret b1 cf' = Some v⇩1› ‹binop bop v⇩1 v⇩2 = v'›
show ?thesis by(cases v') simp+
qed
qed

lemma PCFG_CallEdge_THE_es:
"prog ⊢ n -CEdge(p,es,rets)→⇩p n'
⟹ (THE es'. ∃p' rets' n'. prog ⊢ n -CEdge(p',es',rets')→⇩p n') = es"
by(fastforce intro:the_equality dest:Proc_CFG_Call_nodes_eq)

definition ParamUses_proc :: "cmd ⇒ label ⇒ vname set list"
where "ParamUses_proc c n ≡
if (∃n' p' es' rets'. c ⊢ n -CEdge(p',es',rets')→⇩p n') then
(map fv (THE es'. ∃p' rets' n'. c ⊢ n -CEdge(p',es',rets')→⇩p n'))
else []"

definition ParamUses :: "wf_prog ⇒ node ⇒ vname set list"
where "ParamUses wfp n ≡ let (prog,procs) = Rep_wf_prog wfp; (p,l) = n in
(if (p = Main) then ParamUses_proc prog l
else (if (∃ins outs c. (p,ins,outs,c) ∈ set procs)
then ParamUses_proc (THE c'. ∃ins' outs'. (p,ins',outs',c') ∈ set procs) l
else []))"

lemma ParamUses_Main_Return_target:
"⟦Rep_wf_prog wfp = (prog,procs); prog ⊢ n -CEdge(p',es,rets)→⇩p n' ⟧
⟹ ParamUses wfp (Main,n) = map fv es"
by(fastforce dest:PCFG_CallEdge_THE_es simp:ParamUses_def ParamUses_proc_def)

lemma ParamUses_Proc_Return_target:
assumes "Rep_wf_prog wfp = (prog,procs)"
and "(p,ins,outs,c) ∈ set procs" and "c ⊢ n -CEdge(p',es,rets)→⇩p n'"
shows "ParamUses wfp (p,n) = map fv es"
proof -
from ‹Rep_wf_prog wfp = (prog,procs)› have "well_formed procs"
by(fastforce intro:wf_wf_prog)
with ‹(p,ins,outs,c) ∈ set procs› have "p ≠ Main" by fastforce
moreover
from ‹well_formed procs› ‹(p,ins,outs,c) ∈ set procs›
have "(THE c'. ∃ins' outs'. (p,ins',outs',c') ∈ set procs) = c"
by(rule in_procs_THE_in_procs_cmd)
ultimately show ?thesis using assms
by(fastforce dest:PCFG_CallEdge_THE_es simp:ParamUses_def ParamUses_proc_def)
qed

lemma ParamUses_Main_IEdge_Nil:
"⟦Rep_wf_prog wfp = (prog,procs); prog ⊢ n -IEdge et→⇩p n'⟧
⟹ ParamUses wfp (Main,n) = []"
by(fastforce dest:Proc_CFG_Call_Intra_edge_not_same_source
simp:ParamUses_def ParamUses_proc_def)

lemma ParamUses_Proc_IEdge_Nil:
assumes "Rep_wf_prog wfp = (prog,procs)"
and "(p,ins,outs,c) ∈ set procs" and "c ⊢ n -IEdge et→⇩p n'"
shows "ParamUses wfp (p,n) = []"
proof -
from ‹Rep_wf_prog wfp = (prog,procs)› have "well_formed procs"
by(fastforce intro:wf_wf_prog)
with ‹(p,ins,outs,c) ∈ set procs› have "p ≠ Main" by fastforce
moreover
from ‹well_formed procs› ‹(p,ins,outs,c) ∈ set procs›
have "(THE c'. ∃ins' outs'. (p,ins',outs',c') ∈ set procs) = c"
by(rule in_procs_THE_in_procs_cmd)
ultimately show ?thesis using assms
by(fastforce dest:Proc_CFG_Call_Intra_edge_not_same_source
simp:ParamUses_def ParamUses_proc_def)
qed

lemma ParamUses_Main_CEdge_Nil:
"⟦Rep_wf_prog wfp = (prog,procs); prog ⊢ n' -CEdge(p',es,rets)→⇩p n⟧
⟹ ParamUses wfp (Main,n) = []"
by(fastforce dest:Proc_CFG_Call_targetnode_no_Call_sourcenode
simp:ParamUses_def ParamUses_proc_def)

lemma ParamUses_Proc_CEdge_Nil:
assumes "Rep_wf_prog wfp = (prog,procs)"
and "(p,ins,outs,c) ∈ set procs" and "c ⊢ n' -CEdge(p',es,rets)→⇩p n"
shows "ParamUses wfp (p,n) = []"
proof -
from ‹Rep_wf_prog wfp = (prog,procs)› have "well_formed procs"
by(fastforce intro:wf_wf_prog)
with ‹(p,ins,outs,c) ∈ set procs› have "p ≠ Main" by fastforce
moreover
from ‹well_formed procs›
‹(p,ins,outs,c) ∈ set procs›
have "(THE c'. ∃ins' outs'. (p,ins',outs',c') ∈ set procs) = c"
by(rule in_procs_THE_in_procs_cmd)
ultimately show ?thesis using assms
by(fastforce dest:Proc_CFG_Call_targetnode_no_Call_sourcenode
simp:ParamUses_def ParamUses_proc_def)
qed

subsubsection ‹‹Def››

fun lhs :: "cmd ⇒ vname set"
where
"lhs Skip                = {}"
| "lhs (V:=e)              = {V}"
| "lhs (c⇩1;;c⇩2)            = lhs c⇩1"
| "lhs (if (b) c⇩1 else c⇩2) = {}"
| "lhs (while (b) c)       = {}"
| "lhs (Call p es rets)    = {}"

lemma lhs_fst_cmd:"lhs (fst_cmd c) = lhs c" by(induct c) auto

lemma Proc_CFG_Call_source_empty_lhs:
assumes "prog ⊢ Label l -CEdge (p,es,rets)→⇩p n'"
shows "lhs (label prog l) = {}"
proof -
from ‹prog ⊢ Label l -CEdge (p,es,rets)→⇩p n'› have "l < #:prog"
by(rule Proc_CFG_sourcelabel_less_num_nodes)
then obtain c' where "labels prog l c'"
by(erule less_num_inner_nodes_label)
hence "label prog l = c'" by(rule labels_label)
from ‹labels prog l c'› ‹prog ⊢ Label l -CEdge (p,es,rets)→⇩p n'›
have "∃p es rets. fst_cmd c' = Call p es rets"
by(rule Proc_CFG_Call_source_fst_cmd_Call)
with lhs_fst_cmd[of c'] have "lhs c' = {}" by auto
with ‹label prog l = c'› show ?thesis by simp
qed

lemma in_procs_THE_in_procs_ins:
"⟦well_formed procs; (p,ins,outs,c) ∈ set procs⟧
⟹ (THE ins'. ∃c' outs'. (p,ins',outs',c') ∈ set procs) = ins"
by(fastforce intro:the_equality)

definition Def :: "wf_prog ⇒ node ⇒ vname set"
where "Def wfp n ≡ (let (prog,procs) = Rep_wf_prog wfp; (p,l) = n in
(case l of Label lx ⇒
(if p = Main then lhs (label prog lx)
else (if (∃ins outs c. (p,ins,outs,c) ∈ set procs)
then
lhs (label (THE c'. ∃ins' outs'. (p,ins',outs',c') ∈ set procs) lx)
else {}))
| Entry ⇒ if (∃ins outs c. (p,ins,outs,c) ∈ set procs)
then (set
(THE ins'. ∃c' outs'. (p,ins',outs',c') ∈ set procs)) else {}
| Exit ⇒ {}))
∪ set (ParamDefs wfp n)"

lemma Entry_Def_empty:"Def wfp (Main, Entry) = {}"
proof -
obtain prog procs where [simp]:"Rep_wf_prog wfp = (prog,procs)"
by(cases "Rep_wf_prog wfp") auto
hence "well_formed procs" by(fastforce intro:wf_wf_prog)
thus ?thesis by(auto simp:Def_def ParamDefs_def ParamDefs_proc_def)
qed

lemma Exit_Def_empty:"Def wfp (Main, Exit) = {}"
proof -
obtain prog procs where [simp]:"Rep_wf_prog wfp = (prog,procs)"
by(cases "Rep_wf_prog wfp") auto
hence "well_formed procs" by(fastforce intro:wf_wf_prog)
thus ?thesis
by(auto dest:Proc_CFG_Call_Labels simp:Def_def ParamDefs_def ParamDefs_proc_def)
qed

subsubsection ‹‹Use››

fun rhs :: "cmd ⇒ vname set"
where
"rhs Skip                = {}"
| "rhs (V:=e)              = fv e"
| "rhs (c⇩1;;c⇩2)            = rhs c⇩1"
| "rhs (if (b) c⇩1 else c⇩2) = fv b"
| "rhs (while (b) c)       = fv b"
| "rhs (Call p es rets)    = {}"

lemma rhs_fst_cmd:"rhs (fst_cmd c) = rhs c" by(induct c) auto

lemma Proc_CFG_Call_target_empty_rhs:
assumes "prog ⊢ n -CEdge (p,es,rets)→⇩p Label l'"
shows "rhs (label prog l') = {}"
proof -
from ‹prog ⊢ n -CEdge (p,es,rets)→⇩p Label l'› have "l' < #:prog"
by(rule Proc_CFG_targetlabel_less_num_nodes)
then obtain c' where "labels prog l' c'"
by(erule less_num_inner_nodes_label)
hence "label prog l' = c'" by(rule labels_label)
from ‹labels prog l' c'› ‹prog ⊢ n -CEdge (p,es,rets)→⇩p Label l'›
have "fst_cmd c' = Skip" by(rule Proc_CFG_Call_target_fst_cmd_Skip)
with rhs_fst_cmd[of c'] have "rhs c' = {}" by simp
with ‹label prog l' = c'› show ?thesis by simp
qed

lemma in_procs_THE_in_procs_outs:
"⟦well_formed procs; (p,ins,outs,c) ∈ set procs⟧
⟹ (THE outs'. ∃c' ins'. (p,ins',outs',c') ∈ set procs) = outs"
by(fastforce intro:the_equality)

definition Use :: "wf_prog ⇒ node ⇒ vname set"
where "Use wfp n ≡ (let (prog,procs) = Rep_wf_prog wfp; (p,l) = n in
(case l of Label lx ⇒
(if p = Main then rhs (label prog lx)
else (if (∃ins outs c. (p,ins,outs,c) ∈ set procs)
then
rhs (label (THE c'. ∃ins' outs'. (p,ins',outs',c') ∈ set procs) lx)
else {}))
| Exit ⇒ if (∃ins outs c. (p,ins,outs,c) ∈ set procs)
then (set (THE outs'. ∃c' ins'. (p,ins',outs',c') ∈ set procs) )
else {}
| Entry ⇒ if (∃ins outs c. (p,ins,outs,c) ∈ set procs)
then (set (THE ins'. ∃c' outs'. (p,ins',outs',c') ∈ set procs))
else {}))
∪ Union (set (ParamUses wfp n)) ∪ set (ParamDefs wfp n)"

lemma Entry_Use_empty:"Use wfp (Main, Entry) = {}"
proof -
obtain prog procs where [simp]:"Rep_wf_prog wfp = (prog,procs)"
by(cases "Rep_wf_prog wfp") auto
hence "well_formed procs" by(fastforce intro:wf_wf_prog)
thus ?thesis by(auto dest:Proc_CFG_Call_Labels
simp:Use_def ParamUses_def ParamUses_proc_def ParamDefs_def ParamDefs_proc_def)
qed

lemma Exit_Use_empty:"Use wfp (Main, Exit) = {}"
proof -
obtain prog procs where [simp]:"Rep_wf_prog wfp = (prog,procs)"
by(cases "Rep_wf_prog wfp") auto
hence "well_formed procs" by(fastforce intro:wf_wf_prog)
thus ?thesis by(auto dest:Proc_CFG_Call_Labels
simp:Use_def ParamUses_def ParamUses_proc_def ParamDefs_def ParamDefs_proc_def)
qed

subsection ‹Lemmas about edges and call frames›

lemmas transfers_simps = ProcCFG.transfer.simps[simplified]
declare transfers_simps [simp]

abbreviation state_val :: "(('var ⇀ 'val) × 'ret) list ⇒ 'var ⇀ 'val"
where "state_val s V ≡ (fst (hd s)) V"

lemma Proc_CFG_edge_no_lhs_equal:
assumes "prog ⊢ Label l -IEdge et→⇩p n'" and "V ∉ lhs (label prog l)"
shows "state_val (CFG.transfer (lift_procs wfp) et (cf#cfs)) V = fst cf V"
proof -
from ‹prog ⊢ Label l -IEdge et→⇩p n'›
obtain x where "IEdge et = x" and "prog ⊢ Label l -x→⇩p n'" by simp_all
from ‹prog ⊢ Label l -x→⇩p n'› ‹IEdge et = x› ‹V ∉ lhs (label prog l)›
show ?thesis
proof(induct prog "Label l" x n' arbitrary:l rule:Proc_CFG.induct)
case (Proc_CFG_LAss V' e)
have "labels (V':=e) 0 (V':=e)" by(rule Labels_Base)
hence "label (V':=e) 0 = (V':=e)" by(rule labels_label)
have "V' ∈ lhs (V':=e)" by simp
with ‹V ∉ lhs (label (V':=e) 0)›
‹IEdge et = IEdge ⇑λcf. update cf V' e› ‹label (V':=e) 0 = (V':=e)›
show ?case by fastforce
next
case (Proc_CFG_SeqFirst c⇩1 et' n' c⇩2)
note IH = ‹⟦IEdge et = et'; V ∉ lhs (label c⇩1 l)⟧
⟹ state_val (CFG.transfer (lift_procs wfp) et (cf # cfs)) V = fst cf V›
from ‹c⇩1 ⊢ Label l -et'→⇩p n'› have "l < #:c⇩1"
by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
then obtain c' where "labels c⇩1 l c'" by(erule less_num_inner_nodes_label)
hence "labels (c⇩1;;c⇩2) l (c';;c⇩2)" by(rule Labels_Seq1)
hence "label (c⇩1;;c⇩2) l = c';;c⇩2" by(rule labels_label)
with ‹V ∉ lhs (label (c⇩1;; c⇩2) l)› ‹labels c⇩1 l c'›
have "V ∉ lhs (label c⇩1 l)" by(fastforce dest:labels_label)
with ‹IEdge et = et'› show ?case by (rule IH)
next
case (Proc_CFG_SeqConnect c⇩1 et' c⇩2)
note IH = ‹⟦IEdge et = et'; V ∉ lhs (label c⇩1 l)⟧
⟹ state_val (CFG.transfer (lift_procs wfp) et (cf # cfs)) V = fst cf V›
from ‹c⇩1 ⊢ Label l -et'→⇩p Exit› have "l < #:c⇩1"
by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
then obtain c' where "labels c⇩1 l c'" by(erule less_num_inner_nodes_label)
hence "labels (c⇩1;;c⇩2) l (c';;c⇩2)" by(rule Labels_Seq1)
hence "label (c⇩1;;c⇩2) l = c';;c⇩2" by(rule labels_label)
with ‹V ∉ lhs (label (c⇩1;; c⇩2) l)› ‹labels c⇩1 l c'›
have "V ∉ lhs (label c⇩1 l)" by(fastforce dest:labels_label)
with ‹IEdge et = et'› show ?case by (rule IH)
next
case (Proc_CFG_SeqSecond c⇩2 n et' n' c⇩1 l)
note IH = ‹⋀l. ⟦n = Label l; IEdge et = et'; V ∉ lhs (label c⇩2 l)⟧
⟹ state_val (CFG.transfer (lift_procs wfp) et (cf # cfs)) V = fst cf V›
from ‹n ⊕ #:c⇩1 = Label l› obtain l'
where "n = Label l'" and "l = l' + #:c⇩1" by(cases n) auto
from ‹n = Label l'› ‹c⇩2 ⊢ n -et'→⇩p n'› have "l' < #:c⇩2"
by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
then obtain c' where "labels c⇩2 l' c'" by(erule less_num_inner_nodes_label)
with ‹l = l' + #:c⇩1› have "labels (c⇩1;;c⇩2) l c'"
by(fastforce intro:Labels_Seq2)
hence "label (c⇩1;;c⇩2) l = c'" by(rule labels_label)
with ‹V ∉ lhs (label (c⇩1;;c⇩2) l)› ‹labels c⇩2 l' c'› ‹l = l' + #:c⇩1›
have "V ∉ lhs (label c⇩2 l')" by(fastforce dest:labels_label)
with ‹n = Label l'› ‹IEdge et = et'› show ?case by (rule IH)
next
case (Proc_CFG_CondThen c⇩1 n et' n' b c⇩2 l)
note IH = ‹⋀l. ⟦n = Label l; IEdge et = et'; V ∉ lhs (label c⇩1 l)⟧
⟹ state_val (CFG.transfer (lift_procs wfp) et (cf # cfs)) V = fst cf V›
from ‹n ⊕ 1 = Label l› obtain l'
where "n = Label l'" and "l = l' + 1" by(cases n) auto
from ‹n = Label l'› ‹c⇩1 ⊢ n -et'→⇩p n'› have "l' < #:c⇩1"
by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
then obtain c' where "labels c⇩1 l' c'" by(erule less_num_inner_nodes_label)
with ‹l = l' + 1› have "labels (if (b) c⇩1 else c⇩2) l c'"
by(fastforce intro:Labels_CondTrue)
hence "label (if (b) c⇩1 else c⇩2) l = c'" by(rule labels_label)
with ‹V ∉ lhs (label (if (b) c⇩1 else c⇩2) l)› ‹labels c⇩1 l' c'› ‹l = l' + 1›
have "V ∉ lhs (label c⇩1 l')" by(fastforce dest:labels_label)
with ‹n = Label l'› ‹IEdge et = et'› show ?case by (rule IH)
next
case (Proc_CFG_CondElse c⇩2 n et' n' b c⇩1 l)
note IH = ‹⋀l. ⟦n = Label l; IEdge et = et'; V ∉ lhs (label c⇩2 l)⟧
⟹ state_val (CFG.transfer (lift_procs wfp) et (cf # cfs)) V = fst cf V›
from ‹n ⊕ #:c⇩1 + 1 = Label l› obtain l'
where "n = Label l'" and "l = l' + #:c⇩1 + 1" by(cases n) auto
from ‹n = Label l'› ‹c⇩2 ⊢ n -et'→⇩p n'› have "l' < #:c⇩2"
by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
then obtain c' where "labels c⇩2 l' c'" by(erule less_num_inner_nodes_label)
with ‹l = l' + #:c⇩1 + 1› have "labels (if (b) c⇩1 else c⇩2) l c'"
by(fastforce intro:Labels_CondFalse)
hence "label (if (b) c⇩1 else c⇩2) l = c'" by(rule labels_label)
with ‹V ∉ lhs (label (if (b) c⇩1 else c⇩2) l)› ‹labels c⇩2 l' c'› ‹l = l' + #:c⇩1 + 1›
have "V ∉ lhs (label c⇩2 l')" by(fastforce dest:labels_label)
with ‹n = Label l'› ‹IEdge et = et'› show ?case by (rule IH)
next
case (Proc_CFG_WhileBody c' n et' n' b l)
note IH = ‹⋀l. ⟦n = Label l; IEdge et = et'; V ∉ lhs (label c' l)⟧
⟹ state_val (CFG.transfer (lift_procs wfp) et (cf # cfs)) V = fst cf V›
from ‹n ⊕ 2 = Label l› obtain l'
where "n = Label l'" and "l = l' + 2" by(cases n) auto
from ‹n = Label l'› ‹c' ⊢ n -et'→⇩p n'› have "l' < #:c'"
by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
then obtain cx where "labels c' l' cx" by(erule less_num_inner_nodes_label)
with ‹l = l' + 2› have "labels (while (b) c') l (cx;;while (b) c')"
by(fastforce intro:Labels_WhileBody)
hence "label (while (b) c') l = cx;;while (b) c'" by(rule labels_label)
with ‹V ∉ lhs (label (while (b) c') l)› ‹labels c' l' cx› ‹l = l' + 2›
have "V ∉ lhs (label c' l')" by(fastforce dest:labels_label)
with ‹n = Label l'› ‹IEdge et = et'› show ?case by (rule IH)
next
case (Proc_CFG_WhileBodyExit c' n et' b l)
note IH = ‹⋀l. ⟦n = Label l; IEdge et = et'; V ∉ lhs (label c' l)⟧
⟹ state_val (CFG.transfer (lift_procs wfp) et (cf # cfs)) V = fst cf V›
from ‹n ⊕ 2 = Label l› obtain l'
where "n = Label l'" and "l = l' + 2" by(cases n) auto
from ‹n = Label l'› ‹c' ⊢ n -et'→⇩p Exit› have "l' < #:c'"
by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
then obtain cx where "labels c' l' cx" by(erule less_num_inner_nodes_label)
with ‹l = l' + 2› have "labels (while (b) c') l (cx;;while (b) c')"
by(fastforce intro:Labels_WhileBody)
hence "label (while (b) c') l = cx;;while (b) c'" by(rule labels_label)
with ‹V ∉ lhs (label (while (b) c') l)› ‹labels c' l' cx› ‹l = l' + 2›
have "V ∉ lhs (label c' l')" by(fastforce dest:labels_label)
with ‹n = Label l'› ‹IEdge et = et'› show ?case by (rule IH)
qed auto
qed

lemma Proc_CFG_edge_uses_only_rhs:
assumes "prog ⊢ Label l -IEdge et→⇩p n'" and "CFG.pred et s"
and "CFG.pred et s'" and "∀V∈rhs (label prog l). state_val s V = state_val s' V"
shows "∀V∈lhs (label prog l).
state_val (CFG.transfer (lift_procs wfp) et s) V =
state_val (CFG.transfer (lift_procs wfp) et s') V"
proof -
from ‹prog ⊢ Label l -IEdge et→⇩p n'›
obtain x where "IEdge et = x" and "prog ⊢ Label l -x→⇩p n'" by simp_all
from ‹CFG.pred et s› obtain cf cfs where [simp]:"s = cf#cfs" by(cases s) auto
from ‹CFG.pred et s'› obtain cf' cfs' where [simp]:"s' = cf'#cfs'"
by(cases s') auto
from ‹prog ⊢ Label l -x→⇩p n'› ‹IEdge et = x›
‹∀V∈rhs (label prog l). state_val s V = state_val s' V›
show ?thesis
proof(induct prog "Label l" x n' arbitrary:l rule:Proc_CFG.induct)
case Proc_CFG_Skip
have "labels Skip 0 Skip" by(rule Labels_Base)
hence "label Skip 0 = Skip" by(rule labels_label)
hence "∀V. V ∉ lhs (label Skip 0)" by simp
then show ?case by fastforce
next
case (Proc_CFG_LAss V e)
have "labels (V:=e) 0 (V:=e)" by(rule Labels_Base)
hence "label (V:=e) 0 = V:=e" by(rule labels_label)
then have "lhs (label (V:=e) 0) = {V}"
and "rhs (label (V:=e) 0) = fv e" by auto
with ‹IEdge et = IEdge ⇑λcf. update cf V e›
‹∀V∈rhs (label (V:=e) 0). state_val s V = state_val s' V›
show ?case by(fastforce intro:rhs_interpret_eq)
next
case (Proc_CFG_LAssSkip V e)
have "labels (V:=e) 1 Skip" by(rule Labels_LAss)
hence "label (V:=e) 1 = Skip" by(rule labels_label)
hence "∀V'. V' ∉ lhs (label (V:=e) 1)" by simp
then show ?case by fastforce
next
case (Proc_CFG_SeqFirst c⇩1 et' n' c⇩2)
note IH = ‹⟦IEdge et = et';
∀V∈rhs (label c⇩1 l). state_val s V = state_val s' V⟧
⟹ ∀V∈lhs (label c⇩1 l). state_val (CFG.transfer (lift_procs wfp) et s) V =
state_val (CFG.transfer (lift_procs wfp) et s') V›
from ‹c⇩1 ⊢ Label l -et'→⇩p n'›
have "l < #:c⇩1" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
then obtain c' where "labels c⇩1 l c'" by(erule less_num_inner_nodes_label)
hence "labels (c⇩1;;c⇩2) l (c';;c⇩2)" by(rule Labels_Seq1)
with ‹labels c⇩1 l c'› ‹∀V∈rhs (label (c⇩1;; c⇩2) l). state_val s V = state_val s' V›
have "∀V∈rhs (label c⇩1 l). state_val s V = state_val s' V"
by(fastforce dest:labels_label)
with ‹IEdge et = et'›
have "∀V∈lhs (label c⇩1 l). state_val (CFG.transfer (lift_procs wfp) et s) V =
state_val (CFG.transfer (lift_procs wfp) et s') V" by (rule IH)
with ‹labels c⇩1 l c'› ‹labels (c⇩1;;c⇩2) l (c';;c⇩2)›
show ?case by(fastforce dest:labels_label)
next
case (Proc_CFG_SeqConnect c⇩1 et' c⇩2)
note IH = ‹⟦IEdge et = et';
∀V∈rhs (label c⇩1 l). state_val s V = state_val s' V⟧
⟹ ∀V∈lhs (label c⇩1 l). state_val (CFG.transfer (lift_procs wfp) et s) V =
state_val (CFG.transfer (lift_procs wfp) et s') V›
from ‹c⇩1 ⊢ Label l -et'→⇩p Exit›
have "l < #:c⇩1" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
then obtain c' where "labels c⇩1 l c'" by(erule less_num_inner_nodes_label)
hence "labels (c⇩1;;c⇩2) l (c';;c⇩2)" by(rule Labels_Seq1)
with ‹labels c⇩1 l c'› ‹∀V∈rhs (label (c⇩1;; c⇩2) l). state_val s V = state_val s' V›
have "∀V∈rhs (label c⇩1 l). state_val s V = state_val s' V"
by(fastforce dest:labels_label)
with ‹IEdge et = et'›
have "∀V∈lhs (label c⇩1 l). state_val (CFG.transfer (lift_procs wfp) et s) V =
state_val (CFG.transfer (lift_procs wfp) et s') V" by (rule IH)
with ‹labels c⇩1 l c'› ‹labels (c⇩1;;c⇩2) l (c';;c⇩2)›
show ?case by(fastforce dest:labels_label)
next
case (Proc_CFG_SeqSecond c⇩2 n et' n' c⇩1)
note IH = ‹⋀l. ⟦n = Label l; IEdge et = et';
∀V∈rhs (label c⇩2 l). state_val s V = state_val s' V⟧
⟹ ∀V∈lhs (label c⇩2 l). state_val (CFG.transfer (lift_procs wfp) et s) V =
state_val (CFG.transfer (lift_procs wfp) et s') V›
from ‹n ⊕ #:c⇩1 = Label l› obtain l' where "n = Label l'" and "l = l' + #:c⇩1"
by(cases n) auto
from ‹c⇩2 ⊢ n -et'→⇩p n'› ‹n = Label l'›
have "l' < #:c⇩2" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
then obtain c' where "labels c⇩2 l' c'" by(erule less_num_inner_nodes_label)
with ‹l = l' + #:c⇩1› have "labels (c⇩1;;c⇩2) l c'" by(fastforce intro:Labels_Seq2)
with ‹labels c⇩2 l' c'› ‹∀V∈rhs (label (c⇩1;;c⇩2) l). state_val s V = state_val s' V›
have "∀V∈rhs (label c⇩2 l'). state_val s V = state_val s' V"
by(fastforce dest:labels_label)
with ‹n = Label l'› ‹IEdge et = et'›
have "∀V∈lhs (label c⇩2 l'). state_val (CFG.transfer (lift_procs wfp) et s) V =
state_val (CFG.transfer (lift_procs wfp) et s') V" by (rule IH)
with ‹labels c⇩2 l' c'› ‹labels (c⇩1;;c⇩2) l c'›
show ?case by(fastforce dest:labels_label)
next
case (Proc_CFG_CondTrue b c⇩1 c⇩2)
have "labels (if (b) c⇩1 else c⇩2) 0 (if (b) c⇩1 else c⇩2)" by(rule Labels_Base)
hence "label (if (b) c⇩1 else c⇩2) 0 = if (b) c⇩1 else c⇩2" by(rule labels_label)
hence "∀V. V ∉ lhs (label (if (b) c⇩1 else c⇩2) 0)" by simp
then show ?case by fastforce
next
case (Proc_CFG_CondFalse b c⇩1 c⇩2)
have "labels (if (b) c⇩1 else c⇩2) 0 (if (b) c⇩1 else c⇩2)" by(rule Labels_Base)
hence "label (if (b) c⇩1 else c⇩2) 0 = if (b) c⇩1 else c⇩2" by(rule labels_label)
hence "∀V. V ∉ lhs (label (if (b) c⇩1 else c⇩2) 0)" by simp
then show ?case by fastforce
next
case (Proc_CFG_CondThen c⇩1 n et' n' b c⇩2)
note IH = ‹⋀l. ⟦n = Label l; IEdge et = et';
∀V∈rhs (label c⇩1 l). state_val s V = state_val s' V⟧
⟹ ∀V∈lhs (label c⇩1 l). state_val (CFG.transfer (lift_procs wfp) et s) V =
state_val (CFG.transfer (lift_procs wfp) et s') V›
from ‹n ⊕ 1 = Label l› obtain l' where "n = Label l'" and "l = l' + 1"
by(cases n) auto
from ‹c⇩1 ⊢ n -et'→⇩p n'› ‹n = Label l'›
have "l' < #:c⇩1" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
then obtain c' where "labels c⇩1 l' c'" by(erule less_num_inner_nodes_label)
with ‹l = l' + 1› have "labels (if (b) c⇩1 else c⇩2) l c'"
by(fastforce intro:Labels_CondTrue)
with ‹labels c⇩1 l' c'› ‹∀V∈rhs (label (if (b) c⇩1 else c⇩2) l). state_val s V = state_val s' V›
have "∀V∈rhs (label c⇩1 l'). state_val s V = state_val s' V"
by(fastforce dest:labels_label)
with ‹n = Label l'› ‹IEdge et = et'›
have "∀V∈lhs (label c⇩1 l'). state_val (CFG.transfer (lift_procs wfp) et s) V =
state_val (CFG.transfer (lift_procs wfp) et s') V" by (rule IH)
with ‹labels c⇩1 l' c'› ‹labels (if (b) c⇩1 else c⇩2) l c'›
show ?case by(fastforce dest:labels_label)
next
case (Proc_CFG_CondElse c⇩2 n et' n' b c⇩1)
note IH = ‹⋀l. ⟦n = Label l; IEdge et = et';
∀V∈rhs (label c⇩2 l). state_val s V = state_val s' V⟧
⟹ ∀V∈lhs (label c⇩2 l). state_val (CFG.transfer (lift_procs wfp) et s) V =
state_val (CFG.transfer (lift_procs wfp) et s') V›
from ‹n ⊕ #:c⇩1 + 1= Label l› obtain l' where "n = Label l'" and "l = l' + #:c⇩1+1"
by(cases n) auto
from ‹c⇩2 ⊢ n -et'→⇩p n'› ‹n = Label l'›
have "l' < #:c⇩2" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
then obtain c' where "labels c⇩2 l' c'" by(erule less_num_inner_nodes_label)
with ‹l = l' + #:c⇩1 + 1› have "labels (if (b) c⇩1 else c⇩2) l c'"
by(fastforce intro:Labels_CondFalse)
with ‹labels c⇩2 l' c'› ‹∀V∈rhs (label (if (b) c⇩1 else c⇩2) l).
state_val s V = state_val s' V›
have "∀V∈rhs (label c⇩2 l'). state_val s V = state_val s' V"
by(fastforce dest:labels_label)
with ‹n = Label l'› ‹IEdge et = et'›
have "∀V∈lhs (label c⇩2 l'). state_val (CFG.transfer (lift_procs wfp) et s) V =
state_val (CFG.transfer (lift_procs wfp) et s') V" by (rule IH)
with ‹labels c⇩2 l' c'› ‹labels (if (b) c⇩1 else c⇩2) l c'›
show ?case by(fastforce dest:labels_label)
next
case (Proc_CFG_WhileTrue b c')
have "labels (while (b) c') 0 (while (b) c')" by(rule Labels_Base)
hence "label (while (b) c') 0 = while (b) c'" by(rule labels_label)
hence "∀V. V ∉ lhs (label (while (b) c') 0)" by simp
then show ?case by fastforce
next
case (Proc_CFG_WhileFalse b c')
have "labels (while (b) c') 0 (while (b) c')" by(rule Labels_Base)
hence "label (while (b) c') 0 = while (b) c'" by(rule labels_label)
hence "∀V. V ∉ lhs (label (while (b) c') 0)" by simp
then show ?case by fastforce
next
case (Proc_CFG_WhileFalseSkip b c')
have "labels (while (b) c') 1 Skip" by(rule Labels_WhileExit)
hence "label (while (b) c') 1 = Skip" by(rule labels_label)
hence "∀V. V ∉ lhs (label (while (b) c') 1)" by simp
then show ?case by fastforce
next
case (Proc_CFG_WhileBody c' n et' n' b)
note IH = ‹⋀l. ⟦n = Label l; IEdge et = et';
∀V∈rhs (label c' l). state_val s V = state_val s' V⟧
⟹ ∀V∈lhs (label c' l). state_val (CFG.transfer (lift_procs wfp) et s) V =
state_val (CFG.transfer (lift_procs wfp) et s') V›
from ‹n ⊕ 2 = Label l› obtain l' where "n = Label l'" and "l = l' + 2"
by(cases n) auto
from ‹c' ⊢ n -et'→⇩p n'› ‹n = Label l'›
have "l' < #:c'" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
then obtain cx where "labels c' l' cx" by(erule less_num_inner_nodes_label)
with ‹l = l' + 2› have "labels (while (b) c') l (cx;;while (b) c')"
by(fastforce intro:Labels_WhileBody)
with ‹labels c' l' cx› ‹∀V∈rhs (label (while (b) c') l).
state_val s V = state_val s' V›
have "∀V∈rhs (label c' l'). state_val s V = state_val s' V"
by(fastforce dest:labels_label)
with ‹n = Label l'› ‹IEdge et = et'›
have "∀V∈lhs (label c' l'). state_val (CFG.transfer (lift_procs wfp) et s) V =
state_val (CFG.transfer (lift_procs wfp) et s') V" by (rule IH)
with ‹labels c' l' cx› ‹labels (while (b) c') l (cx;;while (b) c')›
show ?case by(fastforce dest:labels_label)
next
case (Proc_CFG_WhileBodyExit c' n et' b)
note IH = ‹⋀l. ⟦n = Label l; IEdge et = et';
∀V∈rhs (label c' l). state_val s V = state_val s' V⟧
⟹ ∀V∈lhs (label c' l). state_val (CFG.transfer (lift_procs wfp) et s) V =
state_val (CFG.transfer (lift_procs wfp) et s') V›
from ‹n ⊕ 2 = Label l› obtain l' where "n = Label l'" and "l = l' + 2"
by(cases n) auto
from ‹c' ⊢ n -et'→⇩p Exit› ‹n = Label l'›
have "l' < #:c'" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
then obtain cx where "labels c' l' cx" by(erule less_num_inner_nodes_label)
with ‹l = l' + 2› have "labels (while (b) c') l (cx;;while (b) c')"
by(fastforce intro:Labels_WhileBody)
with ‹labels c' l' cx› ‹∀V∈rhs (label (while (b) c') l).
state_val s V = state_val s' V›
have "∀V∈rhs (label c' l'). state_val s V = state_val s' V"
by(fastforce dest:labels_label)
with ‹n = Label l'› ‹IEdge et = et'›
have "∀V∈lhs (label c' l'). state_val (CFG.transfer (lift_procs wfp) et s) V =
state_val (CFG.transfer (lift_procs wfp) et s') V" by (rule IH)
with ‹labels c' l' cx› ‹labels (while (b) c') l (cx;;while (b) c')›
show ?case by(fastforce dest:labels_label)
next
case (Proc_CFG_CallSkip p es rets)
have "labels (Call p es rets) 1 Skip" by(rule Labels_Call)
hence "label (Call p es rets) 1 = Skip" by(rule labels_label)
hence "∀V. V ∉ lhs (label (Call p es rets) 1)" by simp
then show ?case by fastforce
qed auto
qed

lemma Proc_CFG_edge_rhs_pred_eq:
assumes "prog ⊢ Label l -IEdge et→⇩p n'" and "CFG.pred et s"
and "∀V∈rhs (label prog l). state_val s V = state_val s' V"
and "length s = length s'"
shows "CFG.pred et s'"
proof -
from ‹prog ⊢ Label l -IEdge et→⇩p n'›
obtain x where "IEdge et = x" and "prog ⊢ Label l -x→⇩p n'" by simp_all
from ‹CFG.pred et s› obtain cf cfs where [simp]:"s = cf#cfs" by(cases s) auto
from ‹length s = length s'› obtain cf' cfs' where [simp]:"s' = cf'#cfs'"
by(cases s') auto
from ‹prog ⊢ Label l -x→⇩p n'› ‹IEdge et = x›
‹∀V∈rhs (label prog l). state_val s V = state_val s' V›
show ?thesis
proof(induct prog "Label l" x n' arbitrary:l rule:Proc_CFG.induct)
case (Proc_CFG_SeqFirst c⇩1 et' n' c⇩2)
note IH = ‹⟦IEdge et = et'; ∀V∈rhs (label c⇩1 l).
state_val s V = state_val s' V⟧ ⟹ CFG.pred et s'›
from ‹c⇩1 ⊢ Label l -et'→⇩p n'›
have "l < #:c⇩1" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
then obtain c' where "labels c⇩1 l c'" by(erule less_num_inner_nodes_label)
hence "labels (c⇩1;;c⇩2) l (c';;c⇩2)" by(rule Labels_Seq1)
with ‹labels c⇩1 l c'› ‹∀V∈rhs (label (c⇩1;; c⇩2) l). state_val s V = state_val s' V›
have "∀V∈rhs (label c⇩1 l). state_val s V = state_val s' V"
by(fastforce dest:labels_label)
with ‹IEdge et = et'› show ?case by (rule IH)
next
case (Proc_CFG_SeqConnect c⇩1 et' c⇩2)
note IH = ‹⟦IEdge et = et';
∀V∈rhs (label c⇩1 l). state_val s V = state_val s' V⟧
⟹ CFG.pred et s'›
from ‹c⇩1 ⊢ Label l -et'→⇩p Exit›
have "l < #:c⇩1" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
then obtain c' where "labels c⇩1 l c'" by(erule less_num_inner_nodes_label)
hence "labels (c⇩1;;c⇩2) l (c';;c⇩2)" by(rule Labels_Seq1)
with ‹labels c⇩1 l c'› ‹∀V∈rhs (label (c⇩1;; c⇩2) l). state_val s V = state_val s' V›
have "∀V∈rhs (label c⇩1 l). state_val s V = state_val s' V"
by(fastforce dest:labels_label)
with ‹IEdge et = et'› show ?case by (rule IH)
next
case (Proc_CFG_SeqSecond c⇩2 n et' n' c⇩1)
note IH = ‹⋀l. ⟦n = Label l; IEdge et = et';
∀V∈rhs (label c⇩2 l). state_val s V = state_val s' V⟧
⟹ CFG.pred et s'›
from ‹n ⊕ #:c⇩1 = Label l› obtain l' where "n = Label l'" and "l = l' + #:c⇩1"
by(cases n) auto
from ‹c⇩2 ⊢ n -et'→⇩p n'› ‹n = Label l'›
have "l' < #:c⇩2" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
then obtain c' where "labels c⇩2 l' c'" by(erule less_num_inner_nodes_label)
with ‹l = l' + #:c⇩1› have "labels (c⇩1;;c⇩2) l c'" by(fastforce intro:Labels_Seq2)
with ‹labels c⇩2 l' c'› ‹∀V∈rhs (label (c⇩1;;c⇩2) l). state_val s V = state_val s' V›
have "∀V∈rhs (label c⇩2 l'). state_val s V = state_val s' V"
by(fastforce dest:labels_label)
with ‹n = Label l'› ‹IEdge et = et'› show ?case by (rule IH)
next
case (Proc_CFG_CondTrue b c⇩1 c⇩2)
from ‹CFG.pred et s› ‹IEdge et = IEdge (λcf. state_check cf b (Some true))⇩√›
have "state_check (fst cf) b (Some true)" by simp
moreover
have "labels (if (b) c⇩1 else c⇩2) 0 (if (b) c⇩1 else c⇩2)" by(rule Labels_Base)
hence "label (if (b) c⇩1 else c⇩2) 0 = if (b) c⇩1 else c⇩2" by(rule labels_label)
with ‹∀V∈rhs (label (if (b) c⇩1 else c⇩2) 0). state_val s V = state_val s' V›
have "∀V∈ fv b. state_val s V = state_val s' V" by fastforce
ultimately have "state_check (fst cf') b (Some true)"
by simp(rule rhs_interpret_eq)
with ‹IEdge et = IEdge (λcf. state_check cf b (Some true))⇩√›
show ?case by simp
next
case (Proc_CFG_CondFalse b c⇩1 c⇩2)
from ‹CFG.pred et s›
‹IEdge et = IEdge (λcf. state_check cf b (Some false))⇩√›
have "state_check (fst cf) b (Some false)" by simp
moreover
have "labels (if (b) c⇩1 else c⇩2) 0 (if (b) c⇩1 else c⇩2)" by(rule Labels_Base)
hence "label (if (b) c⇩1 else c⇩2) 0 = if (b) c⇩1 else c⇩2" by(rule labels_label)
with ‹∀V∈rhs (label (if (b) c⇩1 else c⇩2) 0). state_val s V = state_val s' V›
have "∀V∈ fv b. state_val s V = state_val s' V" by fastforce
ultimately have "state_check (fst cf') b (Some false)"
by simp(rule rhs_interpret_eq)
with ‹IEdge et = IEdge (λcf. state_check cf b (Some false))⇩√›
show ?case by simp
next
case (Proc_CFG_CondThen c⇩1 n et' n' b c⇩2)
note IH = ‹⋀l. ⟦n = Label l; IEdge et = et';
∀V∈rhs (label c⇩1 l). state_val s V = state_val s' V⟧
⟹ CFG.pred et s'›
from ‹n ⊕ 1 = Label l› obtain l' where "n = Label l'" and "l = l' + 1"
by(cases n) auto
from ‹c⇩1 ⊢ n -et'→⇩p n'› ‹n = Label l'›
have "l' < #:c⇩1" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
then obtain c' where "labels c⇩1 l' c'" by(erule less_num_inner_nodes_label)
with ‹l = l' + 1› have "labels (if (b) c⇩1 else c⇩2) l c'"
by(fastforce intro:Labels_CondTrue)
with ‹labels c⇩1 l' c'› ‹∀V∈rhs (label (if (b) c⇩1 else c⇩2) l).
state_val s V = state_val s' V›
have "∀V∈rhs (label c⇩1 l'). state_val s V = state_val s' V"
by(fastforce dest:labels_label)
with ‹n = Label l'› ‹IEdge et = et'› show ?case by (rule IH)
next
case (Proc_CFG_CondElse c⇩2 n et' n' b c⇩1)
note IH = ‹⋀l. ⟦n = Label l; IEdge et = et';
∀V∈rhs (label c⇩2 l). state_val s V = state_val s' V⟧
⟹ CFG.pred et s'›
from ‹n ⊕ #:c⇩1 + 1= Label l› obtain l' where "n = Label l'" and "l = l' + #:c⇩1+1"
by(cases n) auto
from ‹c⇩2 ⊢ n -et'→⇩p n'› ‹n = Label l'›
have "l' < #:c⇩2" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
then obtain c' where "labels c⇩2 l' c'" by(erule less_num_inner_nodes_label)
with ‹l = l' + #:c⇩1 + 1› have "labels (if (b) c⇩1 else c⇩2) l c'"
by(fastforce intro:Labels_CondFalse)
with ‹labels c⇩2 l' c'› ‹∀V∈rhs (label (if (b) c⇩1 else c⇩2) l).
state_val s V = state_val s' V›
have "∀V∈rhs (label c⇩2 l'). state_val s V = state_val s' V"
by(fastforce dest:labels_label)
with ‹n = Label l'› ‹IEdge et = et'› show ?case by (rule IH)
next
case (Proc_CFG_WhileTrue b c')
from ‹CFG.pred et s› ‹IEdge et = IEdge (λcf. state_check cf b (Some true))⇩√›
have "state_check (fst cf) b (Some true)" by simp
moreover
have "labels (while (b) c') 0 (while (b) c')" by(rule Labels_Base)
hence "label (while (b) c') 0 = while (b) c'" by(rule labels_label)
with ‹∀V∈rhs (label (while (b) c') 0). state_val s V = state_val s' V›
have "∀V∈ fv b. state_val s V = state_val s' V" by fastforce
ultimately have "state_check (fst cf') b (Some true)"
by simp(rule rhs_interpret_eq)
with ‹IEdge et = IEdge (λcf. state_check cf b (Some true))⇩√›
show ?case by simp
next
case (Proc_CFG_WhileFalse b c')
from ‹CFG.pred et s›
‹IEdge et = IEdge (λcf. state_check cf b (Some false))⇩√›
have "state_check (fst cf) b (Some false)" by simp
moreover
have "labels (while (b) c') 0 (while (b) c')" by(rule Labels_Base)
hence "label (while (b) c') 0 = while (b) c'" by(rule labels_label)
with ‹∀V∈rhs (label (while (b) c') 0). state_val s V = state_val s' V›
have "∀V∈ fv b. state_val s V = state_val s' V" by fastforce
ultimately have "state_check (fst cf') b (Some false)"
by simp(rule rhs_interpret_eq)
with ‹IEdge et = IEdge (λcf. state_check cf b (Some false))⇩√›
show ?case by simp
next
case (Proc_CFG_WhileBody c' n et' n' b)
note IH = ‹⋀l. ⟦n = Label l; IEdge et = et';
∀V∈rhs (label c' l). state_val s V = state_val s' V⟧
⟹ CFG.pred et s'›
from ‹n ⊕ 2 = Label l› obtain l' where "n = Label l'" and "l = l' + 2"
by(cases n) auto
from ‹c' ⊢ n -et'→⇩p n'› ‹n = Label l'›
have "l' < #:c'" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
then obtain cx where "labels c' l' cx" by(erule less_num_inner_nodes_label)
with ‹l = l' + 2› have "labels (while (b) c') l (cx;;while (b) c')"
by(fastforce intro:Labels_WhileBody)
with ‹labels c' l' cx› ‹∀V∈rhs (label (while (b) c') l).
state_val s V = state_val s' V›
have "∀V∈rhs (label c' l'). state_val s V = state_val s' V"
by(fastforce dest:labels_label)
with ‹n = Label l'› ‹IEdge et = et'› show ?case by (rule IH)
next
case (Proc_CFG_WhileBodyExit c' n et' b)
note IH = ‹⋀l. ⟦n = Label l; IEdge et = et';
∀V∈rhs (label c' l). state_val s V = state_val s' V⟧
⟹ CFG.pred et s'›
from ‹n ⊕ 2 = Label l› obtain l' where "n = Label l'" and "l = l' + 2"
by(cases n) auto
from ‹c' ⊢ n -et'→⇩p Exit› ‹n = Label l'›
have "l' < #:c'" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
then obtain cx where "labels c' l' cx" by(erule less_num_inner_nodes_label)
with ‹l = l' + 2› have "labels (while (b) c') l (cx;;while (b) c')"
by(fastforce intro:Labels_WhileBody)
with ‹labels c' l' cx› ‹∀V∈rhs (label (while (b) c') l).
state_val s V = state_val s' V›
have "∀V∈rhs (label c' l'). state_val s V = state_val s' V"
by(fastforce dest:labels_label)
with ‹n = Label l'› ‹IEdge et = et'› show ?case by (rule ```