Theory PCFG

```section ‹Definition of the CFG›

theory PCFG imports ProcState begin

definition Main :: "pname"
where "Main = ''Main''"

datatype label = Label nat | Entry | Exit

subsection‹The CFG for every procedure›

subsubsection ‹Definition of ‹⊕››

fun label_incr :: "label ⇒ nat ⇒ label" ("_ ⊕ _" 60)
where "(Label l) ⊕ i = Label (l + i)"
| "Entry ⊕ i       = Entry"
| "Exit ⊕ i        = Exit"

lemma Exit_label_incr [dest]: "Exit = n ⊕ i ⟹ n = Exit"
by(cases n,auto)

lemma label_incr_Exit [dest]: "n ⊕ i = Exit ⟹ n = Exit"
by(cases n,auto)

lemma Entry_label_incr [dest]: "Entry = n ⊕ i ⟹ n = Entry"
by(cases n,auto)

lemma label_incr_Entry [dest]: "n ⊕ i = Entry ⟹ n = Entry"
by(cases n,auto)

lemma label_incr_inj:
"n ⊕ c = n' ⊕ c ⟹ n = n'"
by(cases n)(cases n',auto)+

lemma label_incr_simp:"n ⊕ i = m ⊕ (i + j) ⟹ n = m ⊕ j"
by(cases n,auto,cases m,auto)

lemma label_incr_simp_rev:"m ⊕ (j + i) = n ⊕ i ⟹ m ⊕ j = n"
by(cases n,auto,cases m,auto)

lemma label_incr_start_Node_smaller:
"Label l = n ⊕ i ⟹ n = Label (l - i)"
by(cases n,auto)

lemma label_incr_start_Node_smaller_rev:
"n ⊕ i = Label l ⟹ n = Label (l - i)"
by(cases n,auto)

lemma label_incr_ge:"Label l = n ⊕ i ⟹ l ≥ i"
by(cases n) auto

lemma label_incr_0 [dest]:
"⟦Label 0 = n ⊕ i; i > 0⟧ ⟹ False"
by(cases n) auto

lemma label_incr_0_rev [dest]:
"⟦n ⊕ i = Label 0; i > 0⟧ ⟹ False"
by(cases n) auto

subsubsection ‹The edges of the procedure CFG›

text ‹Control flow information in this language is the node, to which we return
after the calles procedure is finished.›

datatype p_edge_kind =
IEdge "(vname,val,pname × label,pname) edge_kind"
| CEdge "pname × expr list × vname list"

type_synonym p_edge = "(label × p_edge_kind × label)"

inductive Proc_CFG :: "cmd ⇒ label ⇒ p_edge_kind ⇒ label ⇒ bool"
("_ ⊢ _ -_→⇩p _")
where

Proc_CFG_Entry_Exit:
"prog ⊢ Entry -IEdge (λs. False)⇩√→⇩p Exit"

| Proc_CFG_Entry:
"prog ⊢ Entry -IEdge (λs. True)⇩√→⇩p Label 0"

| Proc_CFG_Skip:
"Skip ⊢ Label 0 -IEdge ⇑id→⇩p Exit"

| Proc_CFG_LAss:
"V:=e ⊢ Label 0 -IEdge ⇑(λcf. update cf V e)→⇩p Label 1"

| Proc_CFG_LAssSkip:
"V:=e ⊢ Label 1 -IEdge ⇑id→⇩p Exit"

| Proc_CFG_SeqFirst:
"⟦c⇩1 ⊢ n -et→⇩p n'; n' ≠ Exit⟧ ⟹ c⇩1;;c⇩2 ⊢ n -et→⇩p n'"

| Proc_CFG_SeqConnect:
"⟦c⇩1 ⊢ n -et→⇩p Exit; n ≠ Entry⟧ ⟹ c⇩1;;c⇩2 ⊢ n -et→⇩p Label #:c⇩1"

| Proc_CFG_SeqSecond:
"⟦c⇩2 ⊢ n -et→⇩p n'; n ≠ Entry⟧ ⟹ c⇩1;;c⇩2 ⊢ n ⊕ #:c⇩1 -et→⇩p n' ⊕ #:c⇩1"

| Proc_CFG_CondTrue:
"if (b) c⇩1 else c⇩2 ⊢ Label 0
-IEdge (λcf. state_check cf b (Some true))⇩√→⇩p Label 1"

| Proc_CFG_CondFalse:
"if (b) c⇩1 else c⇩2 ⊢ Label 0 -IEdge (λcf. state_check cf b (Some false))⇩√→⇩p
Label (#:c⇩1 + 1)"

| Proc_CFG_CondThen:
"⟦c⇩1 ⊢ n -et→⇩p n'; n ≠ Entry⟧ ⟹ if (b) c⇩1 else c⇩2 ⊢ n ⊕ 1 -et→⇩p n' ⊕ 1"

| Proc_CFG_CondElse:
"⟦c⇩2 ⊢ n -et→⇩p n'; n ≠ Entry⟧
⟹ if (b) c⇩1 else c⇩2 ⊢ n ⊕ (#:c⇩1 + 1) -et→⇩p n' ⊕ (#:c⇩1 + 1)"

| Proc_CFG_WhileTrue:
"while (b) c' ⊢ Label 0 -IEdge (λcf. state_check cf b (Some true))⇩√→⇩p Label 2"

| Proc_CFG_WhileFalse:
"while (b) c' ⊢ Label 0 -IEdge (λcf. state_check cf b (Some false))⇩√→⇩p Label 1"

| Proc_CFG_WhileFalseSkip:
"while (b) c' ⊢ Label 1 -IEdge ⇑id→⇩p Exit"

| Proc_CFG_WhileBody:
"⟦c' ⊢ n -et→⇩p n'; n ≠ Entry; n' ≠ Exit⟧
⟹ while (b) c' ⊢ n ⊕ 2 -et→⇩p n' ⊕ 2"

| Proc_CFG_WhileBodyExit:
"⟦c' ⊢ n -et→⇩p Exit; n ≠ Entry⟧ ⟹ while (b) c' ⊢ n ⊕ 2 -et→⇩p Label 0"

| Proc_CFG_Call:
"Call p es rets ⊢ Label 0 -CEdge (p,es,rets)→⇩p Label 1"

| Proc_CFG_CallSkip:
"Call p es rets ⊢ Label 1 -IEdge ⇑id→⇩p Exit"

subsubsection‹Some lemmas about the procedure CFG›

lemma Proc_CFG_Exit_no_sourcenode [dest]:
"prog ⊢ Exit -et→⇩p n' ⟹ False"
by(induct prog n≡"Exit" et n' rule:Proc_CFG.induct,auto)

lemma Proc_CFG_Entry_no_targetnode [dest]:
"prog ⊢ n -et→⇩p Entry ⟹ False"
by(induct prog n et n'≡"Entry" rule:Proc_CFG.induct,auto)

lemma Proc_CFG_IEdge_intra_kind:
"prog ⊢ n -IEdge et→⇩p n' ⟹ intra_kind et"
by(induct prog n x≡"IEdge et" n' rule:Proc_CFG.induct,auto simp:intra_kind_def)

lemma [dest]:"prog ⊢ n -IEdge (Q:r↪⇘p⇙fs)→⇩p n' ⟹ False"
by(fastforce dest:Proc_CFG_IEdge_intra_kind simp:intra_kind_def)

lemma [dest]:"prog ⊢ n -IEdge (Q↩⇘p⇙f)→⇩p n' ⟹ False"
by(fastforce dest:Proc_CFG_IEdge_intra_kind simp:intra_kind_def)

lemma Proc_CFG_sourcelabel_less_num_nodes:
"prog ⊢ Label l -et→⇩p n' ⟹ l < #:prog"
proof(induct prog "Label l" et n' arbitrary:l rule:Proc_CFG.induct)
case (Proc_CFG_SeqFirst c⇩1 et n' c⇩2 l)
thus ?case by simp
next
case (Proc_CFG_SeqConnect c⇩1 et c⇩2 l)
thus ?case by simp
next
case (Proc_CFG_SeqSecond c⇩2 n et n' c⇩1 l)
note n = ‹n ⊕ #:c⇩1 = Label l›
note IH = ‹⋀l. n = Label l ⟹ l < #:c⇩2›
from n obtain l' where l':"n = Label l'" by(cases n) auto
from IH[OF this] have "l' < #:c⇩2" .
with n l' show ?case by simp
next
case (Proc_CFG_CondThen c⇩1 n et n' b c⇩2 l)
note n = ‹n ⊕ 1 = Label l›
note IH = ‹⋀l. n = Label l ⟹ l < #:c⇩1›
from n obtain l' where l':"n = Label l'" by(cases n) auto
from IH[OF this] have "l' < #:c⇩1" .
with n l' show ?case by simp
next
case (Proc_CFG_CondElse c⇩2 n et n' b c⇩1 l)
note n = ‹n ⊕ (#:c⇩1 + 1) = Label l›
note IH = ‹⋀l. n = Label l ⟹ l < #:c⇩2›
from n obtain l' where l':"n = Label l'" by(cases n) auto
from IH[OF this] have "l' < #:c⇩2" .
with n l' show ?case by simp
next
case (Proc_CFG_WhileBody c' n et n' b l)
note n = ‹n ⊕ 2 = Label l›
note IH = ‹⋀l. n = Label l ⟹ l < #:c'›
from n obtain l' where l':"n = Label l'" by(cases n) auto
from IH[OF this] have "l' < #:c'" .
with n l' show ?case by simp
next
case (Proc_CFG_WhileBodyExit c' n et b l)
note n = ‹n ⊕ 2 = Label l›
note IH = ‹⋀l. n = Label l ⟹ l < #:c'›
from n obtain l' where l':"n = Label l'" by(cases n) auto
from IH[OF this] have "l' < #:c'" .
with n l' show ?case by simp
qed (auto simp:num_inner_nodes_gr_0)

lemma Proc_CFG_targetlabel_less_num_nodes:
"prog ⊢ n -et→⇩p Label l ⟹ l < #:prog"
proof(induct prog n et "Label l" arbitrary:l rule:Proc_CFG.induct)
case (Proc_CFG_SeqFirst c⇩1 n et c⇩2 l)
thus ?case by simp
next
case (Proc_CFG_SeqSecond c⇩2 n et n' c⇩1 l)
note n' = ‹n' ⊕ #:c⇩1 = Label l›
note IH = ‹⋀l. n' = Label l ⟹ l < #:c⇩2›
from n' obtain l' where l':"n' = Label l'" by(cases n') auto
from IH[OF this] have "l' < #:c⇩2" .
with n' l' show ?case by simp
next
case (Proc_CFG_CondThen c⇩1 n et n' b c⇩2 l)
note n' = ‹n' ⊕ 1 = Label l›
note IH = ‹⋀l. n' = Label l ⟹ l < #:c⇩1›
from n' obtain l' where l':"n' = Label l'" by(cases n') auto
from IH[OF this] have "l' < #:c⇩1" .
with n' l' show ?case by simp
next
case (Proc_CFG_CondElse c⇩2 n et n' b c⇩1 l)
note n' = ‹n' ⊕ (#:c⇩1 + 1) = Label l›
note IH = ‹⋀l. n' = Label l ⟹ l < #:c⇩2›
from n' obtain l' where l':"n' = Label l'" by(cases n') auto
from IH[OF this] have "l' < #:c⇩2" .
with n' l' show ?case by simp
next
case (Proc_CFG_WhileBody c' n et n' b l)
note n' = ‹n' ⊕ 2 = Label l›
note IH = ‹⋀l. n' = Label l ⟹ l < #:c'›
from n' obtain l' where l':"n' = Label l'" by(cases n') auto
from IH[OF this] have "l' < #:c'" .
with n' l' show ?case by simp
qed (auto simp:num_inner_nodes_gr_0)

lemma Proc_CFG_EntryD:
"prog ⊢ Entry -et→⇩p n'
⟹ (n' = Exit ∧ et = IEdge(λs. False)⇩√) ∨ (n' = Label 0 ∧ et = IEdge (λs. True)⇩√)"
by(induct prog n≡"Entry" et n' rule:Proc_CFG.induct,auto)

lemma Proc_CFG_Exit_edge:
obtains l et where "prog ⊢ Label l -IEdge et→⇩p Exit" and "l ≤ #:prog"
proof(atomize_elim)
show "∃l et. prog ⊢ Label l -IEdge et→⇩p Exit ∧ l ≤ #:prog"
proof(induct prog)
case Skip
have "Skip ⊢ Label 0 -IEdge ⇑id→⇩p Exit" by(rule Proc_CFG_Skip)
thus ?case by fastforce
next
case (LAss V e)
have "V:=e ⊢ Label 1 -IEdge ⇑id→⇩p Exit" by(rule Proc_CFG_LAssSkip)
thus ?case by fastforce
next
case (Seq c⇩1 c⇩2)
from ‹∃l et. c⇩2 ⊢ Label l -IEdge et→⇩p Exit ∧ l ≤ #:c⇩2›
obtain l et where "c⇩2 ⊢ Label l -IEdge et→⇩p Exit" and "l ≤ #:c⇩2" by blast
hence "c⇩1;;c⇩2 ⊢ Label l ⊕ #:c⇩1 -IEdge et→⇩p Exit ⊕ #:c⇩1"
by(fastforce intro:Proc_CFG_SeqSecond)
with ‹l ≤ #:c⇩2› show ?case by fastforce
next
case (Cond b c⇩1 c⇩2)
from ‹∃l et. c⇩1 ⊢ Label l -IEdge et→⇩p Exit ∧ l ≤ #:c⇩1›
obtain l et where "c⇩1 ⊢ Label l -IEdge et→⇩p Exit" and "l ≤ #:c⇩1" by blast
hence "if (b) c⇩1 else c⇩2 ⊢ Label l ⊕ 1 -IEdge et→⇩p Exit ⊕ 1"
by(fastforce intro:Proc_CFG_CondThen)
with ‹l ≤ #:c⇩1› show ?case by fastforce
next
case (While b c')
have "while (b) c' ⊢ Label 1 -IEdge ⇑id→⇩p Exit" by(rule Proc_CFG_WhileFalseSkip)
thus ?case by fastforce
next
case (Call p es rets)
have "Call p es rets ⊢ Label 1 -IEdge ⇑id→⇩p Exit" by(rule Proc_CFG_CallSkip)
thus ?case by fastforce
qed
qed

text ‹Lots of lemmas for call edges ‹…››

lemma Proc_CFG_Call_Labels:
"prog ⊢ n -CEdge (p,es,rets)→⇩p n' ⟹ ∃l. n = Label l ∧ n' = Label (Suc l)"
by(induct prog n et≡"CEdge (p,es,rets)" n' rule:Proc_CFG.induct,auto)

lemma Proc_CFG_Call_target_0:
"prog ⊢ n -CEdge (p,es,rets)→⇩p Label 0 ⟹ n = Entry"
by(induct prog n et≡"CEdge (p,es,rets)" n'≡"Label 0" rule:Proc_CFG.induct)
(auto dest:Proc_CFG_Call_Labels)

lemma Proc_CFG_Call_Intra_edge_not_same_source:
"⟦prog ⊢ n -CEdge (p,es,rets)→⇩p n'; prog ⊢ n -IEdge et→⇩p n''⟧ ⟹ False"
proof(induct prog n "CEdge (p,es,rets)" n' arbitrary:n'' rule:Proc_CFG.induct)
case (Proc_CFG_SeqFirst c⇩1 n n' c⇩2)
note IH = ‹⋀n''. c⇩1 ⊢ n -IEdge et→⇩p n'' ⟹ False›
from ‹c⇩1;;c⇩2 ⊢ n -IEdge et→⇩p n''› ‹c⇩1 ⊢ n -CEdge (p, es, rets)→⇩p n'›
‹n' ≠ Exit›
obtain nx where "c⇩1 ⊢ n -IEdge et→⇩p nx"
apply - apply(erule Proc_CFG.cases)
apply(auto intro:Proc_CFG_Entry_Exit Proc_CFG_Entry)
by(case_tac n)(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
then show ?case by (rule IH)
next
case (Proc_CFG_SeqConnect c⇩1 n c⇩2)
from ‹c⇩1 ⊢ n -CEdge (p, es, rets)→⇩p Exit›
show ?case by(fastforce dest:Proc_CFG_Call_Labels)
next
case (Proc_CFG_SeqSecond c⇩2 n n' c⇩1)
note IH = ‹⋀n''. c⇩2 ⊢ n -IEdge et→⇩p n'' ⟹ False›
from ‹c⇩1;;c⇩2 ⊢ n ⊕ #:c⇩1 -IEdge et→⇩p n''› ‹c⇩2 ⊢ n -CEdge (p, es, rets)→⇩p n'›
‹n ≠ Entry›
obtain nx where "c⇩2 ⊢ n -IEdge et→⇩p nx"
apply - apply(erule Proc_CFG.cases,auto)
apply(cases n) apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
apply(cases n) apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
by(cases n,auto,case_tac n,auto)
then show ?case by (rule IH)
next
case (Proc_CFG_CondThen c⇩1 n n' b c⇩2)
note IH = ‹⋀n''. c⇩1 ⊢ n -IEdge et→⇩p n'' ⟹ False›
from ‹if (b) c⇩1 else c⇩2 ⊢ n ⊕ 1 -IEdge et→⇩p n''› ‹c⇩1 ⊢ n -CEdge (p, es, rets)→⇩p n'›
‹n ≠ Entry›
obtain nx where "c⇩1 ⊢ n -IEdge et→⇩p nx"
apply - apply(erule Proc_CFG.cases,auto)
apply(cases n) apply auto apply(case_tac n) apply auto
apply(cases n) apply auto
by(case_tac n)(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
then show ?case by (rule IH)
next
case (Proc_CFG_CondElse c⇩2 n n' b c⇩1)
note IH = ‹⋀n''. c⇩2 ⊢ n -IEdge et→⇩p n'' ⟹ False›
from ‹if (b) c⇩1 else c⇩2 ⊢ n ⊕ #:c⇩1 + 1 -IEdge et→⇩p n''› ‹c⇩2 ⊢ n -CEdge (p, es, rets)→⇩p n'›
‹n ≠ Entry›
obtain nx where "c⇩2 ⊢ n -IEdge et→⇩p nx"
apply - apply(erule Proc_CFG.cases,auto)
apply(cases n) apply auto
apply(case_tac n) apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
by(cases n,auto,case_tac n,auto)
then show ?case by (rule IH)
next
case (Proc_CFG_WhileBody c' n n' b)
note IH = ‹⋀n''. c' ⊢ n -IEdge et→⇩p n'' ⟹ False›
from ‹while (b) c' ⊢ n ⊕ 2 -IEdge et→⇩p n''› ‹c' ⊢ n -CEdge (p, es, rets)→⇩p n'›
‹n ≠ Entry› ‹n' ≠ Exit›
obtain nx where "c' ⊢ n -IEdge et→⇩p nx"
apply - apply(erule Proc_CFG.cases,auto)
apply(drule label_incr_ge[OF sym]) apply simp
apply(cases n) apply auto apply(case_tac n) apply auto
by(cases n,auto,case_tac n,auto)
then show ?case by (rule IH)
next
case (Proc_CFG_WhileBodyExit c' n b)
from ‹c' ⊢ n -CEdge (p, es, rets)→⇩p Exit›
show ?case by(fastforce dest:Proc_CFG_Call_Labels)
next
case Proc_CFG_Call
from ‹Call p es rets ⊢ Label 0 -IEdge et→⇩p n''›
show ?case by(fastforce elim:Proc_CFG.cases)
qed

lemma Proc_CFG_Call_Intra_edge_not_same_target:
"⟦prog ⊢ n -CEdge (p,es,rets)→⇩p n'; prog ⊢ n'' -IEdge et→⇩p n'⟧ ⟹ False"
proof(induct prog n "CEdge (p,es,rets)" n' arbitrary:n'' rule:Proc_CFG.induct)
case (Proc_CFG_SeqFirst c⇩1 n n' c⇩2)
note IH = ‹⋀n''. c⇩1 ⊢ n'' -IEdge et→⇩p n' ⟹ False›
from ‹c⇩1;;c⇩2 ⊢ n'' -IEdge et→⇩p n'› ‹c⇩1 ⊢ n -CEdge (p, es, rets)→⇩p n'›
‹n' ≠ Exit›
have "c⇩1 ⊢ n'' -IEdge et→⇩p n'"
apply - apply(erule Proc_CFG.cases)
apply(auto intro:Proc_CFG_Entry dest:Proc_CFG_targetlabel_less_num_nodes)
by(case_tac n')(auto dest:Proc_CFG_targetlabel_less_num_nodes)
then show ?case by (rule IH)
next
case (Proc_CFG_SeqConnect c⇩1 n c⇩2)
from ‹c⇩1 ⊢ n -CEdge (p, es, rets)→⇩p Exit›
show ?case by(fastforce dest:Proc_CFG_Call_Labels)
next
case (Proc_CFG_SeqSecond c⇩2 n n' c⇩1)
note IH = ‹⋀n''. c⇩2 ⊢ n'' -IEdge et→⇩p n' ⟹ False›
from ‹c⇩1;;c⇩2 ⊢ n'' -IEdge et→⇩p n' ⊕ #:c⇩1› ‹c⇩2 ⊢ n -CEdge (p, es, rets)→⇩p n'›
‹n ≠ Entry›
obtain nx where "c⇩2 ⊢ nx -IEdge et→⇩p n'"
apply - apply(erule Proc_CFG.cases,auto)
apply(fastforce intro:Proc_CFG_Entry_Exit)
apply(cases n') apply(auto dest:Proc_CFG_targetlabel_less_num_nodes)
apply(cases n') apply(auto dest:Proc_CFG_Call_target_0)
apply(cases n') apply(auto dest:Proc_CFG_Call_Labels)
by(case_tac n') auto
then show ?case by (rule IH)
next
case (Proc_CFG_CondThen c⇩1 n n' b c⇩2)
note IH = ‹⋀n''. c⇩1 ⊢ n'' -IEdge et→⇩p n' ⟹ False›
from ‹if (b) c⇩1 else c⇩2 ⊢ n'' -IEdge et→⇩p n' ⊕ 1› ‹c⇩1 ⊢ n -CEdge (p, es, rets)→⇩p n'›
‹n ≠ Entry›
obtain nx where "c⇩1 ⊢ nx -IEdge et→⇩p n'"
apply - apply(erule Proc_CFG.cases,auto)
apply(cases n') apply(auto intro:Proc_CFG_Entry_Exit)
apply(cases n') apply(auto dest:Proc_CFG_Call_target_0)
apply(cases n') apply(auto dest:Proc_CFG_targetlabel_less_num_nodes)
apply(cases n') apply auto apply(case_tac n') apply auto
apply(cases n') apply auto
apply(case_tac n') apply(auto dest:Proc_CFG_targetlabel_less_num_nodes)
by(case_tac n')(auto dest:Proc_CFG_Call_Labels)
then show ?case by (rule IH)
next
case (Proc_CFG_CondElse c⇩2 n n' b c⇩1)
note IH = ‹⋀n''. c⇩2 ⊢ n'' -IEdge et→⇩p n' ⟹ False›
from ‹if (b) c⇩1 else c⇩2 ⊢ n'' -IEdge et→⇩p n' ⊕ #:c⇩1 + 1› ‹c⇩2 ⊢ n -CEdge (p, es, rets)→⇩p n'›
‹n ≠ Entry›
obtain nx where "c⇩2 ⊢ nx -IEdge et→⇩p n'"
apply - apply(erule Proc_CFG.cases,auto)
apply(cases n') apply(auto intro:Proc_CFG_Entry_Exit)
apply(cases n') apply(auto dest:Proc_CFG_Call_target_0)
apply(cases n') apply(auto dest:Proc_CFG_Call_target_0)
apply(cases n') apply auto
apply(case_tac n') apply(auto dest:Proc_CFG_targetlabel_less_num_nodes)
apply(case_tac n') apply(auto dest:Proc_CFG_Call_Labels)
by(cases n',auto,case_tac n',auto)
then show ?case by (rule IH)
next
case (Proc_CFG_WhileBody c' n n' b)
note IH = ‹⋀n''. c' ⊢ n'' -IEdge et→⇩p n' ⟹ False›
from ‹while (b) c' ⊢ n'' -IEdge et→⇩p n' ⊕ 2› ‹c' ⊢ n -CEdge (p, es, rets)→⇩p n'›
‹n ≠ Entry› ‹n' ≠ Exit›
obtain nx where "c' ⊢ nx -IEdge et→⇩p n'"
apply - apply(erule Proc_CFG.cases,auto)
apply(cases n') apply(auto dest:Proc_CFG_Call_target_0)
apply(cases n') apply auto
by(cases n',auto,case_tac n',auto)
then show ?case by (rule IH)
next
case (Proc_CFG_WhileBodyExit c' n b)
from ‹c' ⊢ n -CEdge (p, es, rets)→⇩p Exit›
show ?case by(fastforce dest:Proc_CFG_Call_Labels)
next
case Proc_CFG_Call
from ‹Call p es rets ⊢ n'' -IEdge et→⇩p Label 1›
show ?case by(fastforce elim:Proc_CFG.cases)
qed

lemma Proc_CFG_Call_nodes_eq:
"⟦prog ⊢ n -CEdge (p,es,rets)→⇩p n'; prog ⊢ n -CEdge (p',es',rets')→⇩p n''⟧
⟹ n' = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'"
proof(induct prog n "CEdge (p,es,rets)" n' arbitrary:n'' rule:Proc_CFG.induct)
case (Proc_CFG_SeqFirst c⇩1 n n' c⇩2)
note IH = ‹⋀n''. c⇩1 ⊢ n -CEdge (p',es',rets')→⇩p n''
⟹ n' = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'›
from ‹c⇩1;; c⇩2 ⊢ n -CEdge (p',es',rets')→⇩p n''› ‹c⇩1 ⊢ n -CEdge (p,es,rets)→⇩p n'›
have "c⇩1 ⊢ n -CEdge (p',es',rets')→⇩p n''"
apply - apply(erule Proc_CFG.cases,auto)
apply(fastforce dest:Proc_CFG_Call_Labels)
by(case_tac n,(fastforce dest:Proc_CFG_sourcelabel_less_num_nodes)+)
then show ?case by (rule IH)
next
case (Proc_CFG_SeqConnect c⇩1 n c⇩2)
from ‹c⇩1 ⊢ n -CEdge (p,es,rets)→⇩p Exit› have False
by(fastforce dest:Proc_CFG_Call_Labels)
thus ?case by simp
next
case (Proc_CFG_SeqSecond c⇩2 n n' c⇩1)
note IH = ‹⋀n''. c⇩2 ⊢ n -CEdge (p',es',rets')→⇩p n''
⟹ n' = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'›
from ‹c⇩1;;c⇩2 ⊢ n ⊕ #:c⇩1 -CEdge (p',es',rets')→⇩p n''› ‹n ≠ Entry›
obtain nx where edge:"c⇩2 ⊢ n -CEdge (p',es',rets')→⇩p nx" and nx:"nx ⊕ #:c⇩1 = n''"
apply - apply(erule Proc_CFG.cases,auto)
by(cases n,auto dest:Proc_CFG_sourcelabel_less_num_nodes label_incr_inj)+
from edge have "n' = nx ∧ p = p' ∧ es = es' ∧ rets = rets'" by (rule IH)
with nx show ?case by auto
next
case (Proc_CFG_CondThen c⇩1 n n' b c⇩2)
note IH = ‹⋀n''. c⇩1 ⊢ n -CEdge (p',es',rets')→⇩p n''
⟹ n' = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'›
from ‹if (b) c⇩1 else c⇩2 ⊢ n ⊕ 1 -CEdge (p',es',rets')→⇩p n''›
obtain nx where "c⇩1 ⊢ n -CEdge (p',es',rets')→⇩p nx ∧ nx ⊕ 1 = n''"
proof(rule Proc_CFG.cases)
fix c⇩2' nx etx nx' bx c⇩1'
assume "if (b) c⇩1 else c⇩2 = if (bx) c⇩1' else c⇩2'"
and "n ⊕ 1 = nx ⊕ #:c⇩1' + 1" and "nx ≠ Entry"
with ‹c⇩1 ⊢ n -CEdge (p,es,rets)→⇩p n'› obtain l where "n = Label l" and "l ≥ #:c⇩1"
by(cases n,auto,cases nx,auto)
with ‹c⇩1 ⊢ n -CEdge (p,es,rets)→⇩p n'› have False
by(fastforce dest:Proc_CFG_sourcelabel_less_num_nodes)
thus ?thesis by simp
qed (auto dest:label_incr_inj)
then obtain nx where edge:"c⇩1 ⊢ n -CEdge (p',es',rets')→⇩p nx"
and nx:"nx ⊕ 1 = n''" by blast
from IH[OF edge] nx show ?case by simp
next
case (Proc_CFG_CondElse c⇩2 n n' b c⇩1)
note IH = ‹⋀n''. c⇩2 ⊢ n -CEdge (p',es',rets')→⇩p n''
⟹ n' = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'›
from ‹if (b) c⇩1 else c⇩2 ⊢ n ⊕ #:c⇩1 + 1 -CEdge (p',es',rets')→⇩p n''›
obtain nx where "c⇩2 ⊢ n -CEdge (p',es',rets')→⇩p nx ∧ nx ⊕ #:c⇩1 + 1 = n''"
proof(rule Proc_CFG.cases)
fix c⇩1' nx etx nx' bx c⇩2'
assume ifs:"if (b) c⇩1 else c⇩2 = if (bx) c⇩1' else c⇩2'"
and "n ⊕ #:c⇩1 + 1 = nx ⊕ 1" and "nx ≠ Entry"
and edge:"c⇩1' ⊢ nx -etx→⇩p nx'"
then obtain l where "nx = Label l" and "l ≥ #:c⇩1"
by(cases n,auto,cases nx,auto)
with edge ifs have False
by(fastforce dest:Proc_CFG_sourcelabel_less_num_nodes)
thus ?thesis by simp
qed (auto dest:label_incr_inj)
then obtain nx where edge:"c⇩2 ⊢ n -CEdge (p',es',rets')→⇩p nx"
and nx:"nx ⊕ #:c⇩1 + 1 = n''"
by blast
from IH[OF edge] nx show ?case by simp
next
case (Proc_CFG_WhileBody c' n n' b)
note IH = ‹⋀n''. c' ⊢ n -CEdge (p',es',rets')→⇩p n''
⟹ n' = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'›
from ‹while (b) c' ⊢ n ⊕ 2 -CEdge (p',es',rets')→⇩p n''›
obtain nx where "c' ⊢ n -CEdge (p',es',rets')→⇩p nx ∧ nx ⊕ 2 = n''"
by(rule Proc_CFG.cases,auto dest:label_incr_inj Proc_CFG_Call_Labels)
then obtain nx where edge:"c' ⊢ n -CEdge (p',es',rets')→⇩p nx"
and nx:"nx ⊕ 2 = n''" by blast
from IH[OF edge] nx show ?case by simp
next
case (Proc_CFG_WhileBodyExit c' n b)
from ‹c' ⊢ n -CEdge (p,es,rets)→⇩p Exit› have False
by(fastforce dest:Proc_CFG_Call_Labels)
thus ?case by simp
next
case Proc_CFG_Call
from ‹Call p es rets ⊢ Label 0 -CEdge (p',es',rets')→⇩p n''›
have "p = p' ∧ es = es' ∧ rets = rets' ∧ n'' = Label 1"
by(auto elim:Proc_CFG.cases)
then show ?case by simp
qed

lemma Proc_CFG_Call_nodes_eq':
"⟦prog ⊢ n -CEdge (p,es,rets)→⇩p n'; prog ⊢ n'' -CEdge (p',es',rets')→⇩p n'⟧
⟹ n = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'"
proof(induct prog n "CEdge (p,es,rets)" n' arbitrary:n'' rule:Proc_CFG.induct)
case (Proc_CFG_SeqFirst c⇩1 n n' c⇩2)
note IH = ‹⋀n''. c⇩1 ⊢ n'' -CEdge (p',es',rets')→⇩p n'
⟹ n = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'›
from ‹c⇩1;;c⇩2 ⊢ n'' -CEdge (p',es',rets')→⇩p n'› ‹c⇩1 ⊢ n -CEdge (p,es,rets)→⇩p n'›
have "c⇩1 ⊢ n'' -CEdge (p',es',rets')→⇩p n'"
apply - apply(erule Proc_CFG.cases,auto)
apply(fastforce dest:Proc_CFG_Call_Labels)
by(case_tac n',auto dest:Proc_CFG_targetlabel_less_num_nodes Proc_CFG_Call_Labels)
then show ?case by (rule IH)
next
case (Proc_CFG_SeqConnect c⇩1 n c⇩2)
from ‹c⇩1 ⊢ n -CEdge (p,es,rets)→⇩p Exit› have False
by(fastforce dest:Proc_CFG_Call_Labels)
thus ?case by simp
next
case (Proc_CFG_SeqSecond c⇩2 n n' c⇩1)
note IH = ‹⋀n''. c⇩2 ⊢ n'' -CEdge (p',es',rets')→⇩p n'
⟹ n = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'›
from ‹c⇩1;;c⇩2 ⊢ n'' -CEdge (p',es',rets')→⇩p n' ⊕ #:c⇩1›
obtain nx where edge:"c⇩2 ⊢ nx -CEdge (p',es',rets')→⇩p n'" and nx:"nx ⊕ #:c⇩1 = n''"
apply - apply(erule Proc_CFG.cases,auto)
by(cases n',
auto dest:Proc_CFG_targetlabel_less_num_nodes Proc_CFG_Call_Labels
label_incr_inj)
from edge have "n = nx ∧ p = p' ∧ es = es' ∧ rets = rets'" by (rule IH)
with nx show ?case by auto
next
case (Proc_CFG_CondThen c⇩1 n n' b c⇩2)
note IH = ‹⋀n''. c⇩1 ⊢ n'' -CEdge (p',es',rets')→⇩p n'
⟹ n = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'›
from ‹if (b) c⇩1 else c⇩2 ⊢ n'' -CEdge (p',es',rets')→⇩p n' ⊕ 1›
obtain nx where "c⇩1 ⊢ nx -CEdge (p',es',rets')→⇩p n' ∧ nx ⊕ 1 = n''"
proof(cases)
case (Proc_CFG_CondElse nx nx')
from ‹n' ⊕ 1 = nx' ⊕ #:c⇩1 + 1›
‹c⇩1 ⊢ n -CEdge (p,es,rets)→⇩p n'›
obtain l where "n' = Label l" and "l ≥ #:c⇩1"
by(cases n', auto dest:Proc_CFG_Call_Labels,cases nx',auto)
with ‹c⇩1 ⊢ n -CEdge (p,es,rets)→⇩p n'› have False
by(fastforce dest:Proc_CFG_targetlabel_less_num_nodes)
thus ?thesis by simp
qed (auto dest:label_incr_inj)
then obtain nx where edge:"c⇩1 ⊢ nx -CEdge (p',es',rets')→⇩p n'"
and nx:"nx ⊕ 1 = n''"
by blast
from IH[OF edge] nx show ?case by simp
next
case (Proc_CFG_CondElse c⇩2 n n' b c⇩1)
note IH = ‹⋀n''. c⇩2 ⊢ n'' -CEdge (p',es',rets')→⇩p n'
⟹ n = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'›
from ‹if (b) c⇩1 else c⇩2 ⊢ n'' -CEdge (p',es',rets')→⇩p n' ⊕ #:c⇩1 + 1›
obtain nx where "c⇩2 ⊢ nx -CEdge (p',es',rets')→⇩p n' ∧ nx ⊕ #:c⇩1 + 1 = n''"
proof(cases)
case (Proc_CFG_CondThen nx nx')
from ‹n' ⊕ #:c⇩1 + 1 = nx' ⊕ 1›
‹c⇩1 ⊢ nx -CEdge (p',es',rets')→⇩p nx'›
obtain l where "nx' = Label l" and "l ≥ #:c⇩1"
by(cases n',auto,cases nx',auto dest:Proc_CFG_Call_Labels)
with ‹c⇩1 ⊢ nx -CEdge (p',es',rets')→⇩p nx'›
have False by(fastforce dest:Proc_CFG_targetlabel_less_num_nodes)
thus ?thesis by simp
qed (auto dest:label_incr_inj)
then obtain nx where edge:"c⇩2 ⊢ nx -CEdge (p',es',rets')→⇩p n'"
and nx:"nx ⊕ #:c⇩1 + 1 = n''"
by blast
from IH[OF edge] nx show ?case by simp
next
case (Proc_CFG_WhileBody c' n n' b)
note IH = ‹⋀n''. c' ⊢ n'' -CEdge (p',es',rets')→⇩p n'
⟹ n = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'›
from ‹while (b) c' ⊢ n'' -CEdge (p',es',rets')→⇩p n' ⊕ 2›
obtain nx where edge:"c' ⊢ nx -CEdge (p',es',rets')→⇩p n'" and nx:"nx ⊕ 2 = n''"
by(rule Proc_CFG.cases,auto dest:label_incr_inj)
from IH[OF edge] nx show ?case by simp
next
case (Proc_CFG_WhileBodyExit c' n b)
from ‹c' ⊢ n -CEdge (p,es,rets)→⇩p Exit›
have False by(fastforce dest:Proc_CFG_Call_Labels)
thus ?case by simp
next
case Proc_CFG_Call
from ‹Call p es rets ⊢ n'' -CEdge (p',es',rets')→⇩p Label 1›
have "p = p' ∧ es = es' ∧ rets = rets' ∧ n'' = Label 0"
by(auto elim:Proc_CFG.cases)
then show ?case by simp
qed

lemma Proc_CFG_Call_targetnode_no_Call_sourcenode:
"⟦prog ⊢ n -CEdge (p,es,rets)→⇩p n'; prog ⊢ n' -CEdge (p',es',rets')→⇩p n''⟧
⟹ False"
proof(induct prog n "CEdge (p,es,rets)" n' arbitrary:n'' rule:Proc_CFG.induct)
case (Proc_CFG_SeqFirst c⇩1 n n' c⇩2)
note IH = ‹⋀n''. c⇩1 ⊢ n' -CEdge (p', es', rets')→⇩p n'' ⟹ False›
from ‹c⇩1;; c⇩2 ⊢ n' -CEdge (p',es',rets')→⇩p n''› ‹c⇩1 ⊢ n -CEdge (p,es,rets)→⇩p n'›
have "c⇩1 ⊢ n' -CEdge (p',es',rets')→⇩p n''"
apply - apply(erule Proc_CFG.cases,auto)
apply(fastforce dest:Proc_CFG_Call_Labels)
by(case_tac n)(auto dest:Proc_CFG_targetlabel_less_num_nodes)
then show ?case by (rule IH)
next
case (Proc_CFG_SeqConnect c⇩1 n c⇩2)
from ‹c⇩1 ⊢ n -CEdge (p,es,rets)→⇩p Exit› have False
by(fastforce dest:Proc_CFG_Call_Labels)
thus ?case by simp
next
case (Proc_CFG_SeqSecond c⇩2 n n' c⇩1)
note IH = ‹⋀n''. c⇩2 ⊢ n' -CEdge (p', es', rets')→⇩p n'' ⟹ False›
from ‹c⇩1;; c⇩2 ⊢ n' ⊕ #:c⇩1 -CEdge (p', es', rets')→⇩p n''› ‹c⇩2 ⊢ n -CEdge (p,es,rets)→⇩p n'›
obtain nx where "c⇩2 ⊢ n' -CEdge (p',es',rets')→⇩p nx"
apply - apply(erule Proc_CFG.cases,auto)
apply(cases n') apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
apply(fastforce dest:Proc_CFG_Call_Labels)
by(cases n',auto,case_tac n,auto)
then show ?case by (rule IH)
next
case (Proc_CFG_CondThen c⇩1 n n' b c⇩2)
note IH = ‹⋀n''. c⇩1 ⊢ n' -CEdge (p',es',rets')→⇩p n'' ⟹ False›
from ‹if (b) c⇩1 else c⇩2 ⊢ n' ⊕ 1 -CEdge (p', es', rets')→⇩p n''› ‹c⇩1 ⊢ n -CEdge (p,es,rets)→⇩p n'›
obtain nx where "c⇩1 ⊢ n' -CEdge (p',es',rets')→⇩p nx"
apply - apply(erule Proc_CFG.cases,auto)
apply(cases n') apply auto apply(case_tac n) apply auto
apply(cases n') apply auto
by(case_tac n)(auto dest:Proc_CFG_targetlabel_less_num_nodes)
then show ?case by (rule IH)
next
case (Proc_CFG_CondElse c⇩2 n n' b c⇩1)
note IH = ‹⋀n''. c⇩2 ⊢ n' -CEdge (p',es',rets')→⇩p n'' ⟹ False›
from ‹if (b) c⇩1 else c⇩2 ⊢ n' ⊕ #:c⇩1 + 1 -CEdge (p', es', rets')→⇩p n''›
‹c⇩2 ⊢ n -CEdge (p,es,rets)→⇩p n'›
obtain nx where "c⇩2 ⊢ n' -CEdge (p',es',rets')→⇩p nx"
apply - apply(erule Proc_CFG.cases,auto)
apply(cases n') apply auto
apply(case_tac n) apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
by(cases n',auto,case_tac n,auto)
then show ?case by (rule IH)
next
case (Proc_CFG_WhileBody c' n n' b)
note IH = ‹⋀n''. c' ⊢ n' -CEdge (p',es',rets')→⇩p n'' ⟹ False›
from ‹while (b) c' ⊢ n' ⊕ 2 -CEdge (p', es', rets')→⇩p n''› ‹c' ⊢ n -CEdge (p,es,rets)→⇩p n'›
obtain nx where "c' ⊢ n' -CEdge (p',es',rets')→⇩p nx"
apply - apply(erule Proc_CFG.cases,auto)
by(cases n',auto,case_tac n,auto)+
then show ?case by (rule IH)
next
case (Proc_CFG_WhileBodyExit c' n b)
from ‹c' ⊢ n -CEdge (p, es, rets)→⇩p Exit›
show ?case by(fastforce dest:Proc_CFG_Call_Labels)
next
case Proc_CFG_Call
from ‹Call p es rets ⊢ Label 1 -CEdge (p', es', rets')→⇩p n''›
show ?case by(fastforce elim:Proc_CFG.cases)
qed

lemma Proc_CFG_Call_follows_id_edge:
"⟦prog ⊢ n -CEdge (p,es,rets)→⇩p n'; prog ⊢ n' -IEdge et→⇩p n''⟧ ⟹ et = ⇑id"
proof(induct prog n "CEdge (p,es,rets)" n' arbitrary:n'' rule:Proc_CFG.induct)
case (Proc_CFG_SeqFirst c⇩1 n n' c⇩2)
note IH = ‹⋀n''. c⇩1 ⊢ n' -IEdge et→⇩p n'' ⟹ et = ⇑id›
from ‹c⇩1;;c⇩2 ⊢ n' -IEdge et→⇩p n''› ‹c⇩1 ⊢ n -CEdge (p,es,rets)→⇩p n'› ‹n' ≠ Exit›
obtain nx where "c⇩1 ⊢ n' -IEdge et→⇩p nx"
apply - apply(erule Proc_CFG.cases,auto)
by(case_tac n)(auto dest:Proc_CFG_targetlabel_less_num_nodes)
then show ?case by (rule IH)
next
case (Proc_CFG_SeqConnect c⇩1 n c⇩2)
from ‹c⇩1 ⊢ n -CEdge (p, es, rets)→⇩p Exit›
show ?case by(fastforce dest:Proc_CFG_Call_Labels)
next
case (Proc_CFG_SeqSecond c⇩2 n n' c⇩1)
note IH = ‹⋀n''. c⇩2 ⊢ n' -IEdge et→⇩p n'' ⟹ et = ⇑id›
from ‹c⇩1;;c⇩2 ⊢ n' ⊕ #:c⇩1 -IEdge et→⇩p n''› ‹c⇩2 ⊢ n -CEdge (p,es,rets)→⇩p n'›
obtain nx where "c⇩2 ⊢ n' -IEdge et→⇩p nx"
apply - apply(erule Proc_CFG.cases,auto)
apply(cases n') apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
apply(cases n') apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
by(cases n',auto,case_tac n,auto)
then show ?case by (rule IH)
next
case (Proc_CFG_CondThen c⇩1 n n' b c⇩2)
note IH = ‹⋀n''. c⇩1 ⊢ n' -IEdge et→⇩p n'' ⟹ et = ⇑id›
from ‹if (b) c⇩1 else c⇩2 ⊢ n' ⊕ 1 -IEdge et→⇩p n''› ‹c⇩1 ⊢ n -CEdge (p,es,rets)→⇩p n'›
‹n ≠ Entry›
obtain nx where "c⇩1 ⊢ n' -IEdge et→⇩p nx"
apply - apply(erule Proc_CFG.cases,auto)
apply(cases n') apply auto apply(case_tac n) apply auto
apply(cases n') apply auto
by(case_tac n)(auto dest:Proc_CFG_targetlabel_less_num_nodes)
then show ?case by (rule IH)
next
case (Proc_CFG_CondElse c⇩2 n n' b c⇩1)
note IH = ‹⋀n''. c⇩2 ⊢ n' -IEdge et→⇩p n'' ⟹ et = ⇑id›
from ‹if (b) c⇩1 else c⇩2 ⊢ n' ⊕ #:c⇩1 + 1 -IEdge et→⇩p n''› ‹c⇩2 ⊢ n -CEdge (p,es,rets)→⇩p n'›
obtain nx where "c⇩2 ⊢ n' -IEdge et→⇩p nx"
apply - apply(erule Proc_CFG.cases,auto)
apply(cases n') apply auto
apply(case_tac n) apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
by(cases n',auto,case_tac n,auto)
then show ?case by (rule IH)
next
case (Proc_CFG_WhileBody c' n n' b)
note IH = ‹⋀n''. c' ⊢ n' -IEdge et→⇩p n'' ⟹ et = ⇑id›
from ‹while (b) c' ⊢ n' ⊕ 2 -IEdge et→⇩p n''› ‹c' ⊢ n -CEdge (p,es,rets)→⇩p n'›
obtain nx where "c' ⊢ n' -IEdge et→⇩p nx"
apply - apply(erule Proc_CFG.cases,auto)
apply(cases n') apply auto
apply(cases n') apply auto apply(case_tac n) apply auto
by(cases n',auto,case_tac n,auto)
then show ?case by (rule IH)
next
case (Proc_CFG_WhileBodyExit c' n et' b)
from ‹c' ⊢ n -CEdge (p, es, rets)→⇩p Exit›
show ?case by(fastforce dest:Proc_CFG_Call_Labels)
next
case Proc_CFG_Call
from ‹Call p es rets ⊢ Label 1 -IEdge et→⇩p n''› show ?case
by(fastforce elim:Proc_CFG.cases)
qed

lemma Proc_CFG_edge_det:
"⟦prog ⊢ n -et→⇩p n'; prog ⊢ n -et'→⇩p n'⟧ ⟹ et = et'"
proof(induct rule:Proc_CFG.induct)
case Proc_CFG_Entry_Exit thus ?case by(fastforce dest:Proc_CFG_EntryD)
next
case Proc_CFG_Entry thus ?case by(fastforce dest:Proc_CFG_EntryD)
next
case Proc_CFG_Skip thus ?case by(fastforce elim:Proc_CFG.cases)
next
case Proc_CFG_LAss thus ?case by(fastforce elim:Proc_CFG.cases)
next
case Proc_CFG_LAssSkip thus ?case by(fastforce elim:Proc_CFG.cases)
next
case (Proc_CFG_SeqFirst c⇩1 n et n' c⇩2)
note edge = ‹c⇩1 ⊢ n -et→⇩p n'›
note IH = ‹c⇩1 ⊢ n -et'→⇩p n' ⟹ et = et'›
from edge ‹n' ≠ Exit› obtain l where l:"n' = Label l" by (cases n') auto
with edge have "l < #:c⇩1" by(fastforce intro:Proc_CFG_targetlabel_less_num_nodes)
with ‹c⇩1;;c⇩2 ⊢ n -et'→⇩p n'› l have "c⇩1 ⊢ n -et'→⇩p n'"
by(fastforce elim:Proc_CFG.cases intro:Proc_CFG.intros dest:label_incr_ge)
from IH[OF this] show ?case .
next
case (Proc_CFG_SeqConnect c⇩1 n et c⇩2)
note edge = ‹c⇩1 ⊢ n -et→⇩p Exit›
note IH = ‹c⇩1 ⊢ n -et'→⇩p Exit ⟹ et = et'›
from edge ‹n ≠ Entry› obtain l where l:"n = Label l" by (cases n) auto
with edge have "l < #:c⇩1" by(fastforce intro: Proc_CFG_sourcelabel_less_num_nodes)
with ‹c⇩1;;c⇩2 ⊢ n -et'→⇩p Label #:c⇩1› l have "c⇩1 ⊢ n -et'→⇩p Exit"
by(fastforce elim:Proc_CFG.cases
dest:Proc_CFG_targetlabel_less_num_nodes label_incr_ge)
from IH[OF this] show ?case .
next
case (Proc_CFG_SeqSecond c⇩2 n et n' c⇩1)
note edge = ‹c⇩2 ⊢ n -et→⇩p n'›
note IH = ‹c⇩2 ⊢ n -et'→⇩p n' ⟹ et = et'›
from edge ‹n ≠ Entry› obtain l where l:"n = Label l" by (cases n) auto
with edge have "l < #:c⇩2" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
with ‹c⇩1;;c⇩2 ⊢ n ⊕ #:c⇩1 -et'→⇩p n' ⊕ #:c⇩1› l have "c⇩2 ⊢ n -et'→⇩p n'"
by -(erule Proc_CFG.cases,
(fastforce dest:Proc_CFG_sourcelabel_less_num_nodes label_incr_ge
dest!:label_incr_inj)+)
from IH[OF this] show ?case .
next
case Proc_CFG_CondTrue thus ?case by(fastforce elim:Proc_CFG.cases)
next
case Proc_CFG_CondFalse thus ?case by(fastforce elim:Proc_CFG.cases)
next
case (Proc_CFG_CondThen c⇩1 n et n' b c⇩2)
note edge = ‹c⇩1 ⊢ n -et→⇩p n'›
note IH = ‹c⇩1 ⊢ n -et'→⇩p n' ⟹ et = et'›
from edge ‹n ≠ Entry› obtain l where l:"n = Label l" by (cases n) auto
with edge have "l < #:c⇩1" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
with ‹if (b) c⇩1 else c⇩2 ⊢ n ⊕ 1 -et'→⇩p n' ⊕ 1› l have "c⇩1 ⊢ n -et'→⇩p n'"
by -(erule Proc_CFG.cases,(fastforce dest:label_incr_ge label_incr_inj)+)
from IH[OF this] show ?case .
next
case (Proc_CFG_CondElse c⇩2 n et n' b c⇩1)
note edge = ‹c⇩2 ⊢ n -et→⇩p n'›
note IH = ‹c⇩2 ⊢ n -et'→⇩p n' ⟹ et = et'›
from edge ‹n ≠ Entry› obtain l where l:"n = Label l" by (cases n) auto
with edge have "l < #:c⇩2" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
with ‹if (b) c⇩1 else c⇩2 ⊢ n ⊕ (#:c⇩1 + 1) -et'→⇩p n' ⊕ (#:c⇩1 + 1)› l
have "c⇩2 ⊢ n -et'→⇩p n'"
by -(erule Proc_CFG.cases,(fastforce dest:Proc_CFG_sourcelabel_less_num_nodes
label_incr_inj label_incr_ge label_incr_simp_rev)+)
from IH[OF this] show ?case .
next
case Proc_CFG_WhileTrue thus ?case by(fastforce elim:Proc_CFG.cases)
next
case Proc_CFG_WhileFalse thus ?case by(fastforce elim:Proc_CFG.cases)
next
case Proc_CFG_WhileFalseSkip thus ?case by(fastforce elim:Proc_CFG.cases)
next
case (Proc_CFG_WhileBody c' n et n' b)
note edge = ‹c' ⊢ n -et→⇩p n'›
note IH = ‹c' ⊢ n -et'→⇩p n' ⟹ et = et'›
from edge ‹n ≠ Entry› obtain l where l:"n = Label l" by (cases n) auto
with edge have less:"l < #:c'"
by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
from edge ‹n' ≠ Exit› obtain l' where l':"n' = Label l'" by (cases n') auto
with edge have "l' < #:c'" by(fastforce intro:Proc_CFG_targetlabel_less_num_nodes)
with ‹while (b) c' ⊢ n ⊕ 2 -et'→⇩p n' ⊕ 2› l less l' have "c' ⊢ n -et'→⇩p n'"
by(fastforce elim:Proc_CFG.cases dest:label_incr_start_Node_smaller)
from IH[OF this] show ?case .
next
case (Proc_CFG_WhileBodyExit c' n et b)
note edge = ‹c' ⊢ n -et→⇩p Exit›
note IH = ‹c' ⊢ n -et'→⇩p Exit ⟹ et = et'›
from edge ‹n ≠ Entry› obtain l where l:"n = Label l" by (cases n) auto
with edge have "l < #:c'" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
with ‹while (b) c' ⊢ n ⊕ 2 -et'→⇩p Label 0› l have "c' ⊢ n -et'→⇩p Exit"
by -(erule Proc_CFG.cases,auto dest:label_incr_start_Node_smaller)
from IH[OF this] show ?case .
next
case Proc_CFG_Call thus ?case by(fastforce elim:Proc_CFG.cases)
next
case Proc_CFG_CallSkip thus ?case by(fastforce elim:Proc_CFG.cases)
qed

lemma WCFG_deterministic:
"⟦prog ⊢ n⇩1 -et⇩1→⇩p n⇩1'; prog ⊢ n⇩2 -et⇩2→⇩p n⇩2'; n⇩1 = n⇩2; n⇩1' ≠ n⇩2'⟧
⟹ ∃Q Q'. et⇩1 = IEdge (Q)⇩√ ∧ et⇩2 = IEdge (Q')⇩√ ∧
(∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))"
proof(induct arbitrary:n⇩2 n⇩2' rule:Proc_CFG.induct)
case (Proc_CFG_Entry_Exit prog)
from ‹prog ⊢ n⇩2 -et⇩2→⇩p n⇩2'› ‹Entry = n⇩2› ‹Exit ≠ n⇩2'›
have "et⇩2 = IEdge (λs. True)⇩√" by(fastforce dest:Proc_CFG_EntryD)
thus ?case by simp
next
case (Proc_CFG_Entry prog)
from ‹prog ⊢ n⇩2 -et⇩2→⇩p n⇩2'› ‹Entry = n⇩2› ‹Label 0 ≠ n⇩2'›
have "et⇩2 = IEdge (λs. False)⇩√" by(fastforce dest:Proc_CFG_EntryD)
thus ?case by simp
next
case Proc_CFG_Skip
from ‹Skip ⊢ n⇩2 -et⇩2→⇩p n⇩2'› ‹Label 0 = n⇩2› ‹Exit ≠ n⇩2'›
have False by(fastforce elim:Proc_CFG.cases)
thus ?case by simp
next
case (Proc_CFG_LAss V e)
from ‹V:=e ⊢ n⇩2 -et⇩2→⇩p n⇩2'› ‹Label 0 = n⇩2› ‹Label 1 ≠ n⇩2'›
have False by -(erule Proc_CFG.cases,auto)
thus ?case by simp
next
case (Proc_CFG_LAssSkip V e)
from ‹V:=e ⊢ n⇩2 -et⇩2→⇩p n⇩2'› ‹Label 1 = n⇩2› ‹Exit ≠ n⇩2'›
have False by -(erule Proc_CFG.cases,auto)
thus ?case by simp
next
case (Proc_CFG_SeqFirst c⇩1 n et n' c⇩2)
note IH = ‹⋀n⇩2 n⇩2'. ⟦c⇩1 ⊢ n⇩2 -et⇩2→⇩p n⇩2'; n = n⇩2; n' ≠ n⇩2'⟧
⟹ ∃Q Q'. et = IEdge (Q)⇩√ ∧ et⇩2 = IEdge (Q')⇩√ ∧
(∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
from ‹c⇩1;;c⇩2 ⊢ n⇩2 -et⇩2→⇩p n⇩2'› ‹c⇩1 ⊢ n -et→⇩p n'› ‹n = n⇩2› ‹n' ≠ n⇩2'›
have "c⇩1 ⊢ n⇩2 -et⇩2→⇩p n⇩2' ∨ (c⇩1 ⊢ n⇩2 -et⇩2→⇩p Exit ∧ n⇩2' = Label #:c⇩1)"
apply hypsubst_thin apply(erule Proc_CFG.cases)
apply(auto intro:Proc_CFG.intros)
by(case_tac n,auto dest:Proc_CFG_sourcelabel_less_num_nodes)+
thus ?case
proof
assume "c⇩1 ⊢ n⇩2 -et⇩2→⇩p n⇩2'"
from IH[OF this ‹n = n⇩2› ‹n' ≠ n⇩2'›] show ?case .
next
assume "c⇩1 ⊢ n⇩2 -et⇩2→⇩p Exit ∧ n⇩2' = Label #:c⇩1"
hence edge:"c⇩1 ⊢ n⇩2 -et⇩2→⇩p Exit" and n2':"n⇩2' = Label #:c⇩1" by simp_all
from IH[OF edge ‹n = n⇩2› ‹n' ≠ Exit›] show ?case .
qed
next
case (Proc_CFG_SeqConnect c⇩1 n et c⇩2)
note IH = ‹⋀n⇩2 n⇩2'. ⟦c⇩1 ⊢ n⇩2 -et⇩2→⇩p n⇩2'; n = n⇩2; Exit ≠ n⇩2'⟧
⟹ ∃Q Q'. et = IEdge (Q)⇩√ ∧ et⇩2 = IEdge (Q')⇩√ ∧
(∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
from ‹c⇩1;;c⇩2 ⊢ n⇩2 -et⇩2→⇩p n⇩2'› ‹c⇩1 ⊢ n -et→⇩p Exit› ‹n = n⇩2› ‹n ≠ Entry›
‹Label #:c⇩1 ≠ n⇩2'› have "c⇩1 ⊢ n⇩2 -et⇩2→⇩p n⇩2' ∧ Exit ≠ n⇩2'"
apply hypsubst_thin apply(erule Proc_CFG.cases)
apply(auto intro:Proc_CFG.intros)
by(case_tac n,auto dest:Proc_CFG_sourcelabel_less_num_nodes)+
from IH[OF this[THEN conjunct1] ‹n = n⇩2› this[THEN conjunct2]]
show ?case .
next
case (Proc_CFG_SeqSecond c⇩2 n et n' c⇩1)
note IH = ‹⋀n⇩2 n⇩2'. ⟦c⇩2 ⊢ n⇩2 -et⇩2→⇩p n⇩2'; n = n⇩2; n' ≠ n⇩2'⟧
⟹ ∃Q Q'. et = IEdge (Q)⇩√ ∧ et⇩2 = IEdge (Q')⇩√ ∧
(∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
from ‹c⇩1;;c⇩2 ⊢ n⇩2 -et⇩2→⇩p n⇩2'› ‹c⇩2 ⊢ n -et→⇩p n'› ‹n ⊕ #:c⇩1 = n⇩2›
‹n' ⊕ #:c⇩1 ≠ n⇩2'› ‹n ≠ Entry›
obtain nx where "c⇩2 ⊢ n -et⇩2→⇩p nx ∧ nx ⊕ #:c⇩1 = n⇩2'"
apply - apply(erule Proc_CFG.cases)
apply(auto intro:Proc_CFG.intros)
apply(cases n,auto dest:Proc_CFG_sourcelabel_less_num_nodes)
apply(cases n,auto dest:Proc_CFG_sourcelabel_less_num_nodes)
by(fastforce dest:label_incr_inj)
with ‹n' ⊕ #:c⇩1 ≠ n⇩2'› have edge:"c⇩2 ⊢ n -et⇩2→⇩p nx" and neq:"n' ≠ nx"
by auto
from IH[OF edge _ neq] show ?case by simp
next
case (Proc_CFG_CondTrue b c⇩1 c⇩2)
from ‹if (b) c⇩1 else c⇩2 ⊢ n⇩2 -et⇩2→⇩p n⇩2'› ‹Label 0 = n⇩2› ‹Label 1 ≠ n⇩2'›
show ?case by -(erule Proc_CFG.cases,auto)
next
case (Proc_CFG_CondFalse b c⇩1 c⇩2)
from ‹if (b) c⇩1 else c⇩2 ⊢ n⇩2 -et⇩2→⇩p n⇩2'› ‹Label 0 = n⇩2› ‹Label (#:c⇩1 + 1) ≠ n⇩2'›
show ?case by -(erule Proc_CFG.cases,auto)
next
case (Proc_CFG_CondThen c⇩1 n et n' b c⇩2)
note IH = ‹⋀n⇩2 n⇩2'. ⟦c⇩1 ⊢ n⇩2 -et⇩2→⇩p n⇩2'; n = n⇩2; n' ≠ n⇩2'⟧
⟹ ∃Q Q'. et = IEdge (Q)⇩√ ∧ et⇩2 = IEdge (Q')⇩√ ∧
(∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
from ‹if (b) c⇩1 else c⇩2 ⊢ n⇩2 -et⇩2→⇩p n⇩2'› ‹c⇩1 ⊢ n -et→⇩p n'› ‹n ≠ Entry›
‹n ⊕ 1 = n⇩2› ‹n' ⊕ 1 ≠ n⇩2'›
obtain nx where "c⇩1 ⊢ n -et⇩2→⇩p nx ∧ n' ≠ nx"
apply - apply(erule Proc_CFG.cases)
apply(auto intro:Proc_CFG.intros simp del:One_nat_def)
apply(drule label_incr_inj) apply(auto simp del:One_nat_def)
apply(drule label_incr_simp_rev[OF sym])
by(case_tac na,auto dest:Proc_CFG_sourcelabel_less_num_nodes)
from IH[OF this[THEN conjunct1] _ this[THEN conjunct2]] show ?case by simp
next
case (Proc_CFG_CondElse c⇩2 n et n' b c⇩1)
note IH = ‹⋀n⇩2 n⇩2'. ⟦c⇩2 ⊢ n⇩2 -et⇩2→⇩p n⇩2'; n = n⇩2; n' ≠ n⇩2'⟧
⟹ ∃Q Q'. et = IEdge (Q)⇩√ ∧ et⇩2 = IEdge (Q')⇩√ ∧
(∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
from ‹if (b) c⇩1 else c⇩2 ⊢ n⇩2 -et⇩2→⇩p n⇩2'› ‹c⇩2 ⊢ n -et→⇩p n'› ‹n ≠ Entry›
‹n ⊕ #:c⇩1 + 1 = n⇩2› ‹n' ⊕ #:c⇩1 + 1 ≠ n⇩2'›
obtain nx where "c⇩2 ⊢ n -et⇩2→⇩p nx ∧ n' ≠ nx"
apply - apply(erule Proc_CFG.cases)
apply(auto intro:Proc_CFG.intros simp del:One_nat_def)
apply(drule label_incr_simp_rev)
apply(case_tac na,auto,cases n,auto dest:Proc_CFG_sourcelabel_less_num_nodes)
by(fastforce dest:label_incr_inj)
from IH[OF this[THEN conjunct1] _ this[THEN conjunct2]] show ?case by simp
next
case (Proc_CFG_WhileTrue b c')
from ‹while (b) c' ⊢ n⇩2 -et⇩2→⇩p n⇩2'› ‹Label 0 = n⇩2› ‹Label 2 ≠ n⇩2'›
show ?case by -(erule Proc_CFG.cases,auto)
next
case (Proc_CFG_WhileFalse b c')
from ‹while (b) c' ⊢ n⇩2 -et⇩2→⇩p n⇩2'› ‹Label 0 = n⇩2› ‹Label 1 ≠ n⇩2'›
show ?case by -(erule Proc_CFG.cases,auto)
next
case (Proc_CFG_WhileFalseSkip b c')
from ‹while (b) c' ⊢ n⇩2 -et⇩2→⇩p n⇩2'› ‹Label 1 = n⇩2› ‹Exit ≠ n⇩2'›
show ?case by -(erule Proc_CFG.cases,auto dest:label_incr_ge)
next
case (Proc_CFG_WhileBody c' n et n' b)
note IH = ‹⋀n⇩2 n⇩2'. ⟦c' ⊢ n⇩2 -et⇩2→⇩p n⇩2'; n = n⇩2; n' ≠ n⇩2'⟧
⟹ ∃Q Q'. et = IEdge (Q)⇩√ ∧ et⇩2 = IEdge (Q')⇩√ ∧
(∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
from ‹while (b) c' ⊢ n⇩2 -et⇩2→⇩p n⇩2'› ‹c' ⊢ n -et→⇩p n'› ‹n ≠ Entry›
‹n' ≠ Exit› ‹n ⊕ 2 = n⇩2› ‹n' ⊕ 2 ≠ n⇩2'›
obtain nx where "c' ⊢ n -et⇩2→⇩p nx ∧ n' ≠ nx"
apply - apply(erule Proc_CFG.cases)
apply(auto intro:Proc_CFG.intros)
apply(fastforce dest:label_incr_ge[OF sym])
apply(fastforce dest:label_incr_inj)
by(fastforce dest:label_incr_inj)
from IH[OF this[THEN conjunct1] _ this[THEN conjunct2]] show ?case by simp
next
case (Proc_CFG_WhileBodyExit c' n et b)
note IH = ‹⋀n⇩2 n⇩2'. ⟦c' ⊢ n⇩2 -et⇩2→⇩p n⇩2'; n = n⇩2; Exit ≠ n⇩2'⟧
⟹ ∃Q Q'. et = IEdge (Q)⇩√ ∧ et⇩2 = IEdge (Q')⇩√ ∧
(∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
from ‹while (b) c' ⊢ n⇩2 -et⇩2→⇩p n⇩2'› ‹c' ⊢ n -et→⇩p Exit› ‹n ≠ Entry›
‹n ⊕ 2 = n⇩2› ‹Label 0 ≠ n⇩2'›
obtain nx where "c' ⊢ n -et⇩2→⇩p nx ∧ Exit ≠ nx"
apply - apply(erule Proc_CFG.cases)
apply(auto intro:Proc_CFG.intros)
apply(fastforce dest:label_incr_ge[OF sym])
by(fastforce dest:label_incr_inj)
from IH[OF this[THEN conjunct1] _ this[THEN conjunct2]] show ?case by simp
next
case Proc_CFG_Call thus ?case by -(erule Proc_CFG.cases,auto)
next
case Proc_CFG_CallSkip thus ?case by -(erule Proc_CFG.cases,auto)
qed

subsection ‹And now: the interprocedural CFG›

subsubsection ‹Statements containing calls›

text ‹A procedure is a tuple composed of its name, its input and output variables
and its method body›

type_synonym proc = "(pname × vname list × vname list × cmd)"
type_synonym procs = "proc list"

text ‹‹containsCall› guarantees that a call to procedure p is in
a certain statement.›

declare conj_cong[fundef_cong]

function containsCall ::
"procs ⇒ cmd ⇒ pname list ⇒ pname ⇒ bool"
where "containsCall procs Skip ps p ⟷ False"
| "containsCall procs (V:=e) ps p ⟷ False"
| "containsCall procs (c⇩1;;c⇩2) ps p ⟷
containsCall procs c⇩1 ps p ∨ containsCall procs c⇩2 ps p"
| "containsCall procs (if (b) c⇩1 else c⇩2) ps p ⟷
containsCall procs c⇩1 ps p ∨ containsCall procs c⇩2 ps p"
| "containsCall procs (while (b) c) ps p ⟷
containsCall procs c ps p"
| "containsCall procs (Call q es' rets') ps p ⟷ p = q ∧ ps = [] ∨
(∃ins outs c ps'. ps = q#ps' ∧ (q,ins,outs,c) ∈ set procs ∧
containsCall procs c ps' p)"
by pat_completeness auto
termination containsCall
by(relation "measures [λ(procs,c,ps,p). length ps,
λ(procs,c,ps,p). size c]") auto

lemmas containsCall_induct[case_names Skip LAss Seq Cond While Call] =
containsCall.induct

lemma containsCallcases:
"containsCall procs prog ps p
⟹ ps = [] ∧ containsCall procs prog ps p ∨
(∃q ins outs c ps'. ps = ps'@[q] ∧ (q,ins,outs,c) ∈ set procs ∧
containsCall procs c [] p ∧ containsCall procs prog ps' q)"
proof(induct procs prog ps p rule:containsCall_induct)
case (Call procs q es' rets' ps p)
note IH = ‹⋀x y z ps'. ⟦ps = q#ps'; (q,x,y,z) ∈ set procs;
containsCall procs z ps' p⟧
⟹ ps' = [] ∧ containsCall procs z ps' p ∨
(∃qx ins outs c psx. ps' = psx@[qx] ∧ (qx,ins,outs,c) ∈ set procs ∧
containsCall procs c [] p ∧
containsCall procs z psx qx)›
from ‹containsCall procs (Call q es' rets') ps p›
have "p = q ∧ ps = [] ∨
(∃ins outs c ps'. ps = q#ps' ∧ (q,ins,outs,c) ∈ set procs ∧
containsCall procs c ps' p)" by simp
thus ?case
proof
assume assms:"p = q ∧ ps = []"
hence "containsCall procs (Call q es' rets') ps p" by simp
with assms show ?thesis by simp
next
assume "∃ins outs c ps'. ps = q#ps' ∧ (q,ins,outs,c) ∈ set procs ∧
containsCall procs c ps' p"
then obtain ins outs c ps' where "ps = q#ps'" and "(q,ins,outs,c) ∈ set procs"
and "containsCall procs c ps' p" by blast
from IH[OF this] have "ps' = [] ∧ containsCall procs c ps' p ∨
(∃qx insx outsx cx psx.
ps' = psx @ [qx] ∧ (qx,insx,outsx,cx) ∈ set procs ∧
containsCall procs cx [] p ∧ containsCall procs c psx qx)" .
thus ?thesis
proof
assume assms:"ps' = [] ∧ containsCall procs c ps' p"
have "containsCall procs (Call q es' rets') [] q" by simp
with assms ‹ps = q#ps'› ‹(q,ins,outs,c) ∈ set procs› show ?thesis by fastforce
next
assume "∃qx insx outsx cx psx.
ps' = psx@[qx] ∧ (qx,insx,outsx,cx) ∈ set procs ∧
containsCall procs cx [] p ∧ containsCall procs c psx qx"
then obtain qx insx outsx cx psx
where "ps' = psx@[qx]" and "(qx,insx,outsx,cx) ∈ set procs"
and "containsCall procs cx [] p"
and "containsCall procs c psx qx" by blast
from ‹(q,ins,outs,c) ∈ set procs› ‹containsCall procs c psx qx›
have "containsCall procs (Call q es' rets') (q#psx) qx" by fastforce
with ‹ps' = psx@[qx]› ‹ps = q#ps'› ‹(qx,insx,outsx,cx) ∈ set procs›
‹containsCall procs cx [] p› show ?thesis by fastforce
qed
qed
qed auto

lemma containsCallE:
"⟦containsCall procs prog ps p;
⟦ps = []; containsCall procs prog ps p⟧ ⟹ P procs prog ps p;
⋀q ins outs c es' rets' ps'. ⟦ps = ps'@[q]; (q,ins,outs,c) ∈ set procs;
containsCall procs c [] p; containsCall procs prog ```