Theory ValidPaths

```section ‹Lemmas concerning paths to instantiate locale Postdomination›

theory ValidPaths imports WellFormed "../StaticInter/Postdomination" begin

subsection ‹Intraprocedural paths from method entry and to method exit›

abbreviation path :: "wf_prog ⇒ node ⇒ edge list ⇒ node ⇒ bool" ("_ ⊢ _ -_→* _")
where "wfp ⊢ n -as→* n' ≡ CFG.path sourcenode targetnode (valid_edge wfp) n as n'"

definition label_incrs :: "edge list ⇒ nat ⇒ edge list" ("_ ⊕s _" 60)
where "as ⊕s i ≡ map (λ((p,n),et,(p',n')). ((p,n ⊕ i),et,(p',n' ⊕ i))) as"

declare One_nat_def [simp del]

subsubsection ‹From ‹prog› to ‹prog;;c⇩2››

lemma Proc_CFG_edge_SeqFirst_nodes_Label:
"prog ⊢ Label l -et→⇩p Label l' ⟹ prog;;c⇩2 ⊢ Label l -et→⇩p Label l'"
proof(induct prog "Label l" et "Label l'" rule:Proc_CFG.induct)
case (Proc_CFG_SeqSecond c⇩2' n et n' c⇩1)
hence "(c⇩1;; c⇩2');; c⇩2 ⊢ n ⊕ #:c⇩1 -et→⇩p n' ⊕ #:c⇩1"
by(fastforce intro:Proc_CFG_SeqFirst Proc_CFG.Proc_CFG_SeqSecond)
with ‹n ⊕ #:c⇩1 = Label l› ‹n' ⊕ #:c⇩1 = Label l'› show ?case by fastforce
next
case (Proc_CFG_CondThen c⇩1 n et n' b c⇩2')
hence "if (b) c⇩1 else c⇩2';; c⇩2 ⊢ n ⊕ 1 -et→⇩p n' ⊕ 1"
by(fastforce intro:Proc_CFG_SeqFirst Proc_CFG.Proc_CFG_CondThen)
with ‹n ⊕ 1 = Label l› ‹n' ⊕ 1 = Label l'› show ?case by fastforce
next
case (Proc_CFG_CondElse c⇩1 n et n' b c⇩2')
hence "if (b) c⇩2' else c⇩1 ;; c⇩2 ⊢ n ⊕ #:c⇩2' + 1 -et→⇩p n' ⊕ (#:c⇩2' + 1)"
by(fastforce intro:Proc_CFG_SeqFirst Proc_CFG.Proc_CFG_CondElse)
with ‹n ⊕ #:c⇩2' + 1 = Label l› ‹n' ⊕ #:c⇩2' + 1 = Label l'› show ?case by fastforce
next
case (Proc_CFG_WhileBody c' n et n' b)
hence "while (b) c';; c⇩2 ⊢ n ⊕ 2 -et→⇩p n' ⊕ 2"
by(fastforce intro:Proc_CFG_SeqFirst Proc_CFG.Proc_CFG_WhileBody)
with ‹n ⊕ 2 = Label l› ‹n' ⊕ 2 = Label l'› show ?case by fastforce
next
case (Proc_CFG_WhileBodyExit c' n et b)
hence "while (b) c';; c⇩2 ⊢ n ⊕ 2 -et→⇩p Label 0"
by(fastforce intro:Proc_CFG_SeqFirst Proc_CFG.Proc_CFG_WhileBodyExit)
with ‹n ⊕ 2 = Label l› ‹0 = l'› show ?case by fastforce
qed (auto intro:Proc_CFG.intros)

lemma Proc_CFG_edge_SeqFirst_source_Label:
assumes "prog ⊢ Label l -et→⇩p n'"
obtains nx where "prog;;c⇩2 ⊢ Label l -et→⇩p nx"
proof(atomize_elim)
from ‹prog ⊢ Label l -et→⇩p n'› obtain n where "prog ⊢ n -et→⇩p n'" and "Label l = n"
by simp
thus "∃nx. prog;;c⇩2 ⊢ Label l -et→⇩p nx"
proof(induct prog n et n' rule:Proc_CFG.induct)
case (Proc_CFG_SeqSecond c⇩2' n et n' c⇩1)
show ?case
proof(cases "n' = Exit")
case True
with ‹c⇩2' ⊢ n -et→⇩p n'› ‹n ≠ Entry› have "c⇩1;; c⇩2' ⊢ n ⊕ #:c⇩1 -et→⇩p Exit ⊕ #:c⇩1"
by(fastforce intro:Proc_CFG.Proc_CFG_SeqSecond)
moreover from ‹n ≠ Entry› have "n ⊕ #:c⇩1 ≠ Entry" by(cases n) auto
ultimately
have "c⇩1;; c⇩2';; c⇩2 ⊢ n ⊕ #:c⇩1 -et→⇩p Label (#:c⇩1;; c⇩2')"
by(fastforce intro:Proc_CFG_SeqConnect)
with ‹Label l = n ⊕ #:c⇩1› show ?thesis by fastforce
next
case False
with Proc_CFG_SeqSecond
have "(c⇩1;; c⇩2');; c⇩2 ⊢ n ⊕ #:c⇩1 -et→⇩p n' ⊕ #:c⇩1"
by(fastforce intro:Proc_CFG_SeqFirst Proc_CFG.Proc_CFG_SeqSecond)
with ‹Label l = n ⊕ #:c⇩1› show ?thesis by fastforce
qed
next
case (Proc_CFG_CondThen c⇩1 n et n' b c⇩2')
show ?case
proof(cases "n' = Exit")
case True
with ‹c⇩1 ⊢ n -et→⇩p n'› ‹n ≠ Entry›
have "if (b) c⇩1 else c⇩2' ⊢ n ⊕ 1 -et→⇩p Exit ⊕ 1"
by(fastforce intro:Proc_CFG.Proc_CFG_CondThen)
moreover from ‹n ≠ Entry› have "n ⊕ 1 ≠ Entry" by(cases n) auto
ultimately
have "if (b) c⇩1 else c⇩2';; c⇩2 ⊢ n ⊕ 1 -et→⇩p Label (#:if (b) c⇩1 else c⇩2')"
by(fastforce intro:Proc_CFG_SeqConnect)
with ‹Label l = n ⊕ 1› show ?thesis by fastforce
next
case False
hence "n' ⊕ 1 ≠ Exit" by(cases n') auto
with Proc_CFG_CondThen
have  "if (b) c⇩1 else c⇩2';; c⇩2 ⊢ Label l -et→⇩p n' ⊕ 1"
by(fastforce intro:Proc_CFG_SeqFirst Proc_CFG.Proc_CFG_CondThen)
with ‹Label l = n ⊕ 1› show ?thesis by fastforce
qed
next
case (Proc_CFG_CondElse c⇩1 n et n' b c⇩2')
show ?case
proof(cases "n' = Exit")
case True
with ‹c⇩1 ⊢ n -et→⇩p n'› ‹n ≠ Entry›
have "if (b) c⇩2' else c⇩1 ⊢ n ⊕ (#:c⇩2' + 1) -et→⇩p Exit ⊕ (#:c⇩2' + 1)"
by(fastforce intro:Proc_CFG.Proc_CFG_CondElse)
moreover from ‹n ≠ Entry› have "n ⊕ (#:c⇩2' + 1) ≠ Entry" by(cases n) auto
ultimately
have "if (b) c⇩2' else c⇩1;; c⇩2 ⊢ n ⊕ (#:c⇩2' + 1) -et→⇩p
Label (#:if (b) c⇩2' else c⇩1)"
by(fastforce intro:Proc_CFG_SeqConnect)
with ‹Label l = n ⊕ (#:c⇩2' + 1)› show ?thesis by fastforce
next
case False
hence "n' ⊕ (#:c⇩2' + 1) ≠ Exit" by(cases n') auto
with Proc_CFG_CondElse
have  "if (b) c⇩2' else c⇩1 ;; c⇩2 ⊢ Label l -et→⇩p n' ⊕ (#:c⇩2' + 1)"
by(fastforce intro:Proc_CFG_SeqFirst Proc_CFG.Proc_CFG_CondElse)
with ‹Label l = n ⊕ (#:c⇩2' + 1)› show ?thesis by fastforce
qed
qed (auto intro:Proc_CFG.intros)
qed

lemma Proc_CFG_edge_SeqFirst_target_Label:
"⟦prog ⊢ n -et→⇩p n'; Label l' = n'⟧ ⟹ prog;;c⇩2 ⊢ n -et→⇩p Label l'"
proof(induct prog n et n' rule:Proc_CFG.induct)
case (Proc_CFG_SeqSecond c⇩2' n et n' c⇩1)
from ‹Label l' = n' ⊕ #:c⇩1› have "n' ≠ Exit" by(cases n') auto
with Proc_CFG_SeqSecond
show ?case by(fastforce intro:Proc_CFG_SeqFirst intro:Proc_CFG.Proc_CFG_SeqSecond)
next
case (Proc_CFG_CondThen c⇩1 n et n' b c⇩2')
from ‹Label l' = n' ⊕ 1› have "n' ≠ Exit" by(cases n') auto
with Proc_CFG_CondThen
show ?case by(fastforce intro:Proc_CFG_SeqFirst Proc_CFG.Proc_CFG_CondThen)
qed (auto intro:Proc_CFG.intros)

lemma PCFG_edge_SeqFirst_source_Label:
assumes "prog,procs ⊢ (p,Label l) -et→ (p',n')"
obtains nx where "prog;;c⇩2,procs ⊢ (p,Label l) -et→ (p',nx)"
proof(atomize_elim)
from ‹prog,procs ⊢ (p,Label l) -et→ (p',n')›
show "∃nx. prog;;c⇩2,procs ⊢ (p,Label l) -et→ (p',nx)"
proof(induct "(p,Label l)" et "(p',n')" rule:PCFG.induct)
case (Main et)
from ‹prog ⊢ Label l -IEdge et→⇩p n'›
obtain nx' where "prog;;c⇩2 ⊢ Label l -IEdge et→⇩p nx'"
by(auto elim:Proc_CFG_edge_SeqFirst_source_Label)
with ‹Main = p› ‹Main = p'› show ?case
by(fastforce dest:PCFG.Main)
next
case (Proc ins outs c et ps)
from ‹containsCall procs prog ps p›
have "containsCall procs (prog;;c⇩2) ps p" by simp
with Proc show ?case by(fastforce dest:PCFG.Proc)
next
case (MainCall es rets nx ins outs c)
from ‹prog ⊢ Label l -CEdge (p', es, rets)→⇩p nx›
obtain lx where [simp]:"nx = Label lx" by(fastforce dest:Proc_CFG_Call_Labels)
with ‹prog ⊢ Label l -CEdge (p', es, rets)→⇩p nx›
have "prog;;c⇩2 ⊢ Label l -CEdge (p', es, rets)→⇩p Label lx"
by(auto intro:Proc_CFG_edge_SeqFirst_nodes_Label)
with MainCall show ?case by(fastforce dest:PCFG.MainCall)
next
case (ProcCall ins outs c es' rets' l' ins' outs' c' ps)
from ‹containsCall procs prog ps p›
have "containsCall procs (prog;;c⇩2) ps p" by simp
with ProcCall show ?case by(fastforce intro:PCFG.ProcCall)
next
case (MainCallReturn px es rets)
from ‹prog ⊢ Label l -CEdge (px, es, rets)→⇩p n'› ‹Main = p›
obtain nx'' where "prog;;c⇩2 ⊢ Label l -CEdge (px, es, rets)→⇩p nx''"
by(auto elim:Proc_CFG_edge_SeqFirst_source_Label)
with MainCallReturn show ?case by(fastforce dest:PCFG.MainCallReturn)
next
case (ProcCallReturn ins outs c px' es' rets' ps)
from ‹containsCall procs prog ps p›
have "containsCall procs (prog;;c⇩2) ps p" by simp
with ProcCallReturn show ?case by(fastforce dest!:PCFG.ProcCallReturn)
qed
qed

lemma PCFG_edge_SeqFirst_target_Label:
"prog,procs ⊢ (p,n) -et→ (p',Label l')
⟹ prog;;c⇩2,procs ⊢ (p,n) -et→ (p',Label l')"
proof(induct "(p,n)" et "(p',Label l')" rule:PCFG.induct)
case Main
thus ?case by(fastforce dest:Proc_CFG_edge_SeqFirst_target_Label intro:PCFG.Main)
next
case (Proc ins outs c et ps)
from ‹containsCall procs prog ps p›
have "containsCall procs (prog;;c⇩2) ps p" by simp
with Proc show ?case by(fastforce dest:PCFG.Proc)
next
case MainReturn thus ?case
by(fastforce dest:Proc_CFG_edge_SeqFirst_target_Label
intro!:PCFG.MainReturn[simplified])
next
case (ProcReturn ins outs c lx es' rets' ins' outs' c' ps)
from ‹containsCall procs prog ps p'›
have "containsCall procs (prog;;c⇩2) ps p'" by simp
with ProcReturn show ?case by(fastforce intro:PCFG.ProcReturn)
next
case MainCallReturn thus ?case
by(fastforce dest:Proc_CFG_edge_SeqFirst_target_Label intro:PCFG.MainCallReturn)
next
case (ProcCallReturn ins outs c px' es' rets' ps)
from ‹containsCall procs prog ps p›
have "containsCall procs (prog;;c⇩2) ps p" by simp
with ProcCallReturn show ?case by(fastforce dest!:PCFG.ProcCallReturn)
qed

lemma path_SeqFirst:
assumes "Rep_wf_prog wfp = (prog,procs)" and "Rep_wf_prog wfp' = (prog;;c⇩2,procs)"
shows "⟦wfp ⊢ (p,n) -as→* (p,Label l); ∀a ∈ set as. intra_kind (kind a)⟧
⟹ wfp' ⊢ (p,n) -as→* (p,Label l)"
proof(induct "(p,n)" as "(p,Label l)" arbitrary:n rule:ProcCFG.path.induct)
case empty_path
from ‹CFG.valid_node sourcenode targetnode (valid_edge wfp) (p, Label l)›
‹Rep_wf_prog wfp = (prog, procs)› ‹Rep_wf_prog wfp' = (prog;; c⇩2, procs)›
have "CFG.valid_node sourcenode targetnode (valid_edge wfp') (p, Label l)"
apply(auto simp:ProcCFG.valid_node_def valid_edge_def)
apply(erule PCFG_edge_SeqFirst_source_Label,fastforce)
by(drule PCFG_edge_SeqFirst_target_Label,fastforce)
thus ?case by(fastforce intro:ProcCFG.empty_path)
next
case (Cons_path n'' as a nx)
note IH = ‹⋀n. ⟦n'' = (p, n); ∀a∈set as. intra_kind (kind a)⟧
⟹ wfp' ⊢ (p, n) -as→* (p, Label l)›
note [simp] = ‹Rep_wf_prog wfp = (prog,procs)› ‹Rep_wf_prog wfp' = (prog;;c⇩2,procs)›
from ‹Rep_wf_prog wfp = (prog,procs)› have wf:"well_formed procs"
by(fastforce intro:wf_wf_prog)
from ‹∀a∈set (a # as). intra_kind (kind a)› have "intra_kind (kind a)"
and "∀a∈set as. intra_kind (kind a)" by simp_all
from ‹valid_edge wfp a› ‹sourcenode a = (p, nx)› ‹targetnode a = n''›
‹intra_kind (kind a)› wf
obtain nx' where "n'' = (p,nx')"
by(auto elim:PCFG.cases simp:valid_edge_def intra_kind_def)
from IH[OF this ‹∀a∈set as. intra_kind (kind a)›]
have path:"wfp' ⊢ (p, nx') -as→* (p, Label l)" .
have "valid_edge wfp' a"
proof(cases nx')
case (Label lx)
with ‹valid_edge wfp a› ‹sourcenode a = (p, nx)› ‹targetnode a = n''›
‹n'' = (p,nx')› show ?thesis
by(fastforce intro:PCFG_edge_SeqFirst_target_Label
simp:intra_kind_def valid_edge_def)
next
case Entry
with ‹valid_edge wfp a› ‹targetnode a = n''› ‹n'' = (p,nx')›
‹intra_kind (kind a)› have False
by(auto elim:PCFG.cases simp:valid_edge_def intra_kind_def)
thus ?thesis by simp
next
case Exit
with path ‹∀a∈set as. intra_kind (kind a)› have False
by(induct "(p,nx')" as "(p,Label l)" rule:ProcCFG.path.induct)
(auto elim!:PCFG.cases simp:valid_edge_def intra_kind_def)
thus ?thesis by simp
qed
with ‹sourcenode a = (p, nx)› ‹targetnode a = n''› ‹n'' = (p,nx')› path
show ?case by(fastforce intro:ProcCFG.Cons_path)
qed

subsubsection ‹From ‹prog› to ‹c⇩1;;prog››

lemma Proc_CFG_edge_SeqSecond_source_not_Entry:
"⟦prog ⊢ n -et→⇩p n'; n ≠ Entry⟧ ⟹ c⇩1;;prog ⊢ n ⊕ #:c⇩1 -et→⇩p n' ⊕ #:c⇩1"
by(induct rule:Proc_CFG.induct)(fastforce intro:Proc_CFG_SeqSecond Proc_CFG.intros)+

lemma PCFG_Main_edge_SeqSecond_source_not_Entry:
"⟦prog,procs ⊢ (Main,n) -et→ (p',n'); n ≠ Entry; intra_kind et; well_formed procs⟧
⟹ c⇩1;;prog,procs ⊢ (Main,n ⊕ #:c⇩1) -et→ (p',n' ⊕ #:c⇩1)"
proof(induct "(Main,n)" et "(p',n')" rule:PCFG.induct)
case Main
thus ?case
by(fastforce dest:Proc_CFG_edge_SeqSecond_source_not_Entry intro:PCFG.Main)
next
case (MainCallReturn p es rets)
from ‹prog ⊢ n -CEdge (p, es, rets)→⇩p n'› ‹n ≠ Entry›
have "c⇩1;;prog ⊢ n ⊕ #:c⇩1 -CEdge (p, es, rets)→⇩p n' ⊕ #:c⇩1"
by(rule Proc_CFG_edge_SeqSecond_source_not_Entry)
with MainCallReturn show ?case by(fastforce intro:PCFG.MainCallReturn)
qed (auto simp:intra_kind_def)

lemma valid_node_Main_SeqSecond:
assumes "CFG.valid_node sourcenode targetnode (valid_edge wfp) (Main,n)"
and "n ≠ Entry" and "Rep_wf_prog wfp = (prog,procs)"
and "Rep_wf_prog wfp' = (c⇩1;;prog,procs)"
shows "CFG.valid_node sourcenode targetnode (valid_edge wfp') (Main, n ⊕ #:c⇩1)"
proof -
note [simp] = ‹Rep_wf_prog wfp = (prog,procs)› ‹Rep_wf_prog wfp' = (c⇩1;;prog,procs)›
from ‹Rep_wf_prog wfp = (prog,procs)› have wf:"well_formed procs"
by(fastforce intro:wf_wf_prog)
from ‹CFG.valid_node sourcenode targetnode (valid_edge wfp) (Main,n)›
obtain a where "prog,procs ⊢ sourcenode a -kind a→ targetnode a"
and "(Main,n) = sourcenode a ∨ (Main,n) = targetnode a"
by(fastforce simp:ProcCFG.valid_node_def valid_edge_def)
from this ‹n ≠ Entry› wf show ?thesis
proof(induct "sourcenode a" "kind a" "targetnode a" rule:PCFG.induct)
case (Main nx nx')
from ‹(Main,n) = sourcenode a ∨ (Main,n) = targetnode a› show ?case
proof
assume "(Main,n) = sourcenode a"
with ‹(Main, nx) = sourcenode a›[THEN sym] have [simp]:"nx = n" by simp
from ‹n ≠ Entry› ‹prog ⊢ nx -IEdge (kind a)→⇩p nx'›
have "c⇩1;;prog ⊢ n ⊕ #:c⇩1 -IEdge (kind a)→⇩p nx' ⊕ #:c⇩1"
by(fastforce intro:Proc_CFG_edge_SeqSecond_source_not_Entry)
hence "c⇩1;;prog,procs ⊢ (Main,n ⊕ #:c⇩1) -kind a→ (Main,nx' ⊕ #:c⇩1)"
by(rule PCFG.Main)
thus ?thesis by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
next
assume "(Main, n) = targetnode a"
show ?thesis
proof(cases "nx = Entry")
case True
with ‹prog ⊢ nx -IEdge (kind a)→⇩p nx'›
have "nx' = Exit ∨ nx' = Label 0" by(fastforce dest:Proc_CFG_EntryD)
thus ?thesis
proof
assume "nx' = Exit"
with ‹(Main, n) = targetnode a› ‹(Main, nx') = targetnode a›[THEN sym]
show ?thesis by simp
next
assume "nx' = Label 0"
obtain l etx where "c⇩1 ⊢ Label l -IEdge etx→⇩p Exit" and "l ≤ #:c⇩1"
by(erule Proc_CFG_Exit_edge)
hence "c⇩1;;prog ⊢ Label l -IEdge etx→⇩p Label #:c⇩1"
by(fastforce intro:Proc_CFG_SeqConnect)
with ‹nx' = Label 0›
have "c⇩1;;prog,procs ⊢ (Main,Label l) -etx→ (Main,nx'⊕#:c⇩1)"
by(fastforce intro:PCFG.Main)
with ‹(Main, n) = targetnode a› ‹(Main, nx') = targetnode a›[THEN sym]
show ?thesis
by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
qed
next
case False
with ‹prog ⊢ nx -IEdge (kind a)→⇩p nx'›
have "c⇩1;;prog ⊢ nx ⊕ #:c⇩1 -IEdge (kind a)→⇩p nx' ⊕ #:c⇩1"
by(fastforce intro:Proc_CFG_edge_SeqSecond_source_not_Entry)
hence "c⇩1;;prog,procs ⊢ (Main,nx ⊕ #:c⇩1) -kind a→ (Main,nx' ⊕ #:c⇩1)"
by(rule PCFG.Main)
with ‹(Main, n) = targetnode a› ‹(Main, nx') = targetnode a›[THEN sym]
show ?thesis by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
qed
qed
next
case (Proc p ins outs c nx n' ps)
from ‹(p, nx) = sourcenode a›[THEN sym] ‹(p, n') = targetnode a›[THEN sym]
‹(Main, n) = sourcenode a ∨ (Main, n) = targetnode a›
‹(p, ins, outs, c) ∈ set procs› ‹well_formed procs› have False by fastforce
thus ?case by simp
next
case (MainCall l p es rets n' ins outs c)
from ‹(p, ins, outs, c) ∈ set procs› wf ‹(p, Entry) = targetnode a›[THEN sym]
‹(Main, Label l) = sourcenode a›[THEN sym]
‹(Main, n) = sourcenode a ∨ (Main, n) = targetnode a›
have [simp]:"n = Label l" by fastforce
from ‹prog ⊢ Label l -CEdge (p, es, rets)→⇩p n'›
have "c⇩1;;prog ⊢ Label l ⊕ #:c⇩1 -CEdge (p, es, rets)→⇩p n' ⊕ #:c⇩1"
by -(rule Proc_CFG_edge_SeqSecond_source_not_Entry,auto)
with ‹(p, ins, outs, c) ∈ set procs›
have "c⇩1;;prog,procs ⊢ (Main,Label (l + #:c⇩1))
-(λs. True):(Main,n' ⊕ #:c⇩1)↪⇘p⇙map (λe cf. interpret e cf) es→ (p,Entry)"
by(fastforce intro:PCFG.MainCall)
thus ?case by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
next
case (ProcCall p ins outs c l p' es' rets' l' ins' outs' c')
from ‹(p, Label l) = sourcenode a›[THEN sym]
‹(p', Entry) = targetnode a›[THEN sym]  ‹well_formed procs›
‹(p, ins, outs, c) ∈ set procs› ‹(p', ins', outs', c') ∈ set procs›
‹(Main, n) = sourcenode a ∨ (Main, n) = targetnode a›
have False by fastforce
thus ?case by simp
next
case (MainReturn l p es rets l' ins outs c)
from ‹(p, ins, outs, c) ∈ set procs› wf ‹(p, Exit) = sourcenode a›[THEN sym]
‹(Main, Label l') = targetnode a›[THEN sym]
‹(Main, n) = sourcenode a ∨ (Main, n) = targetnode a›
have [simp]:"n = Label l'" by fastforce
from ‹prog ⊢ Label l -CEdge (p, es, rets)→⇩p Label l'›
have "c⇩1;;prog ⊢ Label l ⊕ #:c⇩1 -CEdge (p, es, rets)→⇩p Label l' ⊕ #:c⇩1"
by -(rule Proc_CFG_edge_SeqSecond_source_not_Entry,auto)
with ‹(p, ins, outs, c) ∈ set procs›
have "c⇩1;;prog,procs ⊢ (p,Exit) -(λcf. snd cf = (Main,Label l' ⊕ #:c⇩1))↩⇘p⇙
(λcf cf'. cf'(rets [:=] map cf outs))→ (Main,Label (l' + #:c⇩1))"
by(fastforce intro:PCFG.MainReturn)
thus ?case by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
next
case (ProcReturn p ins outs c l p' es' rets' l' ins' outs' c' ps)
from ‹(p', Exit) = sourcenode a›[THEN sym]
‹(p, Label l') = targetnode a›[THEN sym] ‹well_formed procs›
‹(p, ins, outs, c) ∈ set procs› ‹(p', ins', outs', c') ∈ set procs›
‹(Main, n) = sourcenode a ∨ (Main, n) = targetnode a›
have False by fastforce
thus ?case by simp
next
case (MainCallReturn nx p es rets nx')
from ‹(Main,n) = sourcenode a ∨ (Main,n) = targetnode a› show ?case
proof
assume "(Main,n) = sourcenode a"
with ‹(Main, nx) = sourcenode a›[THEN sym] have [simp]:"nx = n" by simp
from ‹n ≠ Entry› ‹prog ⊢ nx -CEdge (p, es, rets)→⇩p nx'›
have "c⇩1;;prog ⊢ n ⊕ #:c⇩1 -CEdge (p, es, rets)→⇩p nx' ⊕ #:c⇩1"
by(fastforce intro:Proc_CFG_edge_SeqSecond_source_not_Entry)
hence "c⇩1;;prog,procs ⊢ (Main,n ⊕ #:c⇩1) -(λs. False)⇩√→ (Main,nx' ⊕ #:c⇩1)"
by -(rule PCFG.MainCallReturn)
thus ?thesis by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
next
assume "(Main, n) = targetnode a"
from ‹prog ⊢ nx -CEdge (p, es, rets)→⇩p nx'›
have "nx ≠ Entry" by(fastforce dest:Proc_CFG_Call_Labels)
with ‹prog ⊢ nx -CEdge (p, es, rets)→⇩p nx'›
have "c⇩1;;prog ⊢ nx ⊕ #:c⇩1 -CEdge (p, es, rets)→⇩p nx' ⊕ #:c⇩1"
by(fastforce intro:Proc_CFG_edge_SeqSecond_source_not_Entry)
hence "c⇩1;;prog,procs ⊢ (Main,nx ⊕ #:c⇩1) -(λs. False)⇩√→ (Main,nx' ⊕ #:c⇩1)"
by -(rule PCFG.MainCallReturn)
with ‹(Main, n) = targetnode a› ‹(Main, nx') = targetnode a›[THEN sym]
show ?thesis by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
qed
next
case (ProcCallReturn p ins outs c nx p' es' rets' n' ps)
from ‹(p, nx) = sourcenode a›[THEN sym] ‹(p, n') = targetnode a›[THEN sym]
‹(p, ins, outs, c) ∈ set procs› ‹well_formed procs›
‹(Main, n) = sourcenode a ∨ (Main, n) = targetnode a›
have False by fastforce
thus ?case by simp
qed
qed

lemma path_Main_SeqSecond:
assumes "Rep_wf_prog wfp = (prog,procs)" and "Rep_wf_prog wfp' = (c⇩1;;prog,procs)"
shows "⟦wfp ⊢ (Main,n) -as→* (p',n'); ∀a ∈ set as. intra_kind (kind a); n ≠ Entry⟧
⟹ wfp' ⊢ (Main,n ⊕ #:c⇩1) -as ⊕s #:c⇩1→* (p',n' ⊕ #:c⇩1)"
proof(induct "(Main,n)" as "(p',n')" arbitrary:n rule:ProcCFG.path.induct)
case empty_path
from ‹CFG.valid_node sourcenode targetnode (valid_edge wfp) (Main, n')›
‹n' ≠ Entry› ‹Rep_wf_prog wfp = (prog,procs)›
‹Rep_wf_prog wfp' = (c⇩1;;prog,procs)›
have "CFG.valid_node sourcenode targetnode (valid_edge wfp') (Main, n' ⊕ #:c⇩1)"
by(fastforce intro:valid_node_Main_SeqSecond)
with ‹Main = p'› show ?case
by(fastforce intro:ProcCFG.empty_path simp:label_incrs_def)
next
case (Cons_path n'' as a n)
note IH = ‹⋀n.  ⟦n'' = (Main, n); ∀a∈set as. intra_kind (kind a); n ≠ Entry⟧
⟹ wfp' ⊢ (Main, n ⊕ #:c⇩1) -as ⊕s #:c⇩1→* (p', n' ⊕ #:c⇩1)›
note [simp] = ‹Rep_wf_prog wfp = (prog,procs)› ‹Rep_wf_prog wfp' = (c⇩1;;prog,procs)›
from ‹Rep_wf_prog wfp = (prog,procs)› have wf:"well_formed procs"
by(fastforce intro:wf_wf_prog)
from ‹∀a∈set (a # as). intra_kind (kind a)› have "intra_kind (kind a)"
and "∀a∈set as. intra_kind (kind a)" by simp_all
from ‹valid_edge wfp a› ‹sourcenode a = (Main, n)› ‹targetnode a = n''›
‹intra_kind (kind a)› wf
obtain nx'' where "n'' = (Main,nx'')" and "nx'' ≠ Entry"
by(auto elim!:PCFG.cases simp:valid_edge_def intra_kind_def)
from IH[OF ‹n'' = (Main,nx'')› ‹∀a∈set as. intra_kind (kind a)› ‹nx'' ≠ Entry›]
have path:"wfp' ⊢ (Main, nx'' ⊕ #:c⇩1) -as ⊕s #:c⇩1→* (p', n' ⊕ #:c⇩1)" .
from ‹valid_edge wfp a› ‹sourcenode a = (Main, n)› ‹targetnode a = n''›
‹n'' = (Main,nx'')› ‹n ≠ Entry› ‹intra_kind (kind a)› wf
have "c⇩1;; prog,procs ⊢ (Main, n ⊕ #:c⇩1) -kind a→ (Main, nx'' ⊕ #:c⇩1)"
by(fastforce intro:PCFG_Main_edge_SeqSecond_source_not_Entry simp:valid_edge_def)
with path ‹sourcenode a = (Main, n)› ‹targetnode a = n''› ‹n'' = (Main,nx'')›
show ?case apply(cases a) apply(clarsimp simp:label_incrs_def)
by(auto intro:ProcCFG.Cons_path simp:valid_edge_def)
qed

subsubsection ‹From ‹prog› to ‹if (b) prog else c⇩2››

lemma Proc_CFG_edge_CondTrue_source_not_Entry:
"⟦prog ⊢ n -et→⇩p n'; n ≠ Entry⟧ ⟹ if (b) prog else c⇩2 ⊢ n ⊕ 1 -et→⇩p n' ⊕ 1"
by(induct rule:Proc_CFG.induct)(fastforce intro:Proc_CFG_CondThen Proc_CFG.intros)+

lemma PCFG_Main_edge_CondTrue_source_not_Entry:
"⟦prog,procs ⊢ (Main,n) -et→ (p',n'); n ≠ Entry; intra_kind et; well_formed procs⟧
⟹ if (b) prog else c⇩2,procs ⊢ (Main,n ⊕ 1) -et→ (p',n' ⊕ 1)"
proof(induct "(Main,n)" et "(p',n')" rule:PCFG.induct)
case Main
thus ?case by(fastforce dest:Proc_CFG_edge_CondTrue_source_not_Entry intro:PCFG.Main)
next
case (MainCallReturn p es rets)
from ‹prog ⊢ n -CEdge (p, es, rets)→⇩p n'› ‹n ≠ Entry›
have "if (b) prog else c⇩2 ⊢ n ⊕ 1 -CEdge (p, es, rets)→⇩p n' ⊕ 1"
by(rule Proc_CFG_edge_CondTrue_source_not_Entry)
with MainCallReturn show ?case by(fastforce intro:PCFG.MainCallReturn)
qed (auto simp:intra_kind_def)

lemma valid_node_Main_CondTrue:
assumes "CFG.valid_node sourcenode targetnode (valid_edge wfp) (Main,n)"
and "n ≠ Entry" and "Rep_wf_prog wfp = (prog,procs)"
and "Rep_wf_prog wfp' = (if (b) prog else c⇩2,procs)"
shows "CFG.valid_node sourcenode targetnode (valid_edge wfp') (Main, n ⊕ 1)"
proof -
note [simp] = ‹Rep_wf_prog wfp = (prog,procs)›
‹Rep_wf_prog wfp' = (if (b) prog else c⇩2,procs)›
from ‹Rep_wf_prog wfp = (prog,procs)› have wf:"well_formed procs"
by(fastforce intro:wf_wf_prog)
from ‹CFG.valid_node sourcenode targetnode (valid_edge wfp) (Main,n)›
obtain a where "prog,procs ⊢ sourcenode a -kind a→ targetnode a"
and "(Main,n) = sourcenode a ∨ (Main,n) = targetnode a"
by(fastforce simp:ProcCFG.valid_node_def valid_edge_def)
from this ‹n ≠ Entry› wf show ?thesis
proof(induct "sourcenode a" "kind a" "targetnode a" rule:PCFG.induct)
case (Main nx nx')
from ‹(Main,n) = sourcenode a ∨ (Main,n) = targetnode a› show ?case
proof
assume "(Main,n) = sourcenode a"
with ‹(Main, nx) = sourcenode a›[THEN sym] have [simp]:"nx = n" by simp
from ‹n ≠ Entry› ‹prog ⊢ nx -IEdge (kind a)→⇩p nx'›
have "if (b) prog else c⇩2 ⊢ n ⊕ 1 -IEdge (kind a)→⇩p nx' ⊕ 1"
by(fastforce intro:Proc_CFG_edge_CondTrue_source_not_Entry)
hence "if (b) prog else c⇩2,procs ⊢ (Main,n ⊕ 1) -kind a→ (Main,nx' ⊕ 1)"
by(rule PCFG.Main)
thus ?thesis by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
next
assume "(Main, n) = targetnode a"
show ?thesis
proof(cases "nx = Entry")
case True
with ‹prog ⊢ nx -IEdge (kind a)→⇩p nx'›
have "nx' = Exit ∨ nx' = Label 0" by(fastforce dest:Proc_CFG_EntryD)
thus ?thesis
proof
assume "nx' = Exit"
with ‹(Main, n) = targetnode a› ‹(Main, nx') = targetnode a›[THEN sym]
show ?thesis by simp
next
assume "nx' = Label 0"
have "if (b) prog else c⇩2 ⊢ Label 0
-IEdge (λcf. state_check cf b (Some true))⇩√→⇩p Label 1"
by(rule Proc_CFG_CondTrue)
with ‹nx' = Label 0›
have "if (b) prog else c⇩2,procs ⊢ (Main,Label 0)
-(λcf. state_check cf b (Some true))⇩√→ (Main,nx' ⊕ 1)"
by(fastforce intro:PCFG.Main)
with ‹(Main, n) = targetnode a› ‹(Main, nx') = targetnode a›[THEN sym]
show ?thesis
by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
qed
next
case False
with ‹prog ⊢ nx -IEdge (kind a)→⇩p nx'›
have "if (b) prog else c⇩2 ⊢ nx ⊕ 1 -IEdge (kind a)→⇩p nx' ⊕ 1"
by(fastforce intro:Proc_CFG_edge_CondTrue_source_not_Entry)
hence "if (b) prog else c⇩2,procs ⊢ (Main,nx ⊕ 1) -kind a→
(Main,nx' ⊕ 1)" by(rule PCFG.Main)
with ‹(Main, n) = targetnode a› ‹(Main, nx') = targetnode a›[THEN sym]
show ?thesis by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
qed
qed
next
case (Proc p ins outs c nx n' ps)
from ‹(p, nx) = sourcenode a›[THEN sym] ‹(p, n') = targetnode a›[THEN sym]
‹(p, ins, outs, c) ∈ set procs› ‹well_formed procs›
‹(Main, n) = sourcenode a ∨ (Main, n) = targetnode a›
have False by fastforce
thus ?case by simp
next
case (MainCall l p es rets n' ins outs c)
from ‹(p, ins, outs, c) ∈ set procs› ‹(p, Entry) = targetnode a›[THEN sym]
‹(Main, Label l) = sourcenode a›[THEN sym] wf
‹(Main, n) = sourcenode a ∨ (Main, n) = targetnode a›
have [simp]:"n = Label l" by fastforce
from ‹prog ⊢ Label l -CEdge (p, es, rets)→⇩p n'›
have "if (b) prog else c⇩2 ⊢ Label l ⊕ 1 -CEdge (p, es, rets)→⇩p n' ⊕ 1"
by -(rule Proc_CFG_edge_CondTrue_source_not_Entry,auto)
with ‹(p, ins, outs, c) ∈ set procs›
have "if (b) prog else c⇩2,procs ⊢ (Main,Label (l + 1))
-(λs. True):(Main,n' ⊕ 1)↪⇘p⇙map (λe cf. interpret e cf) es→ (p,Entry)"
by(fastforce intro:PCFG.MainCall)
thus ?case by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
next
case (ProcCall p ins outs c l p' es' rets' l' ins' outs' c' ps)
from ‹(p, Label l) = sourcenode a›[THEN sym]
‹(p', Entry) = targetnode a›[THEN sym] ‹well_formed procs›
‹(p, ins, outs, c) ∈ set procs› ‹(p', ins', outs', c') ∈ set procs›
‹(Main, n) = sourcenode a ∨ (Main, n) = targetnode a›
have False by fastforce
thus ?case by simp
next
case (MainReturn l p es rets l' ins outs c)
from ‹(p, ins, outs, c) ∈ set procs› ‹(p, Exit) = sourcenode a›[THEN sym]
‹(Main, Label l') = targetnode a›[THEN sym] wf
‹(Main, n) = sourcenode a ∨ (Main, n) = targetnode a›
have [simp]:"n = Label l'" by fastforce
from ‹prog ⊢ Label l -CEdge (p, es, rets)→⇩p Label l'›
have "if (b) prog else c⇩2 ⊢ Label l ⊕ 1 -CEdge (p, es, rets)→⇩p Label l' ⊕ 1"
by -(rule Proc_CFG_edge_CondTrue_source_not_Entry,auto)
with ‹(p, ins, outs, c) ∈ set procs›
have "if (b) prog else c⇩2,procs ⊢ (p,Exit) -(λcf. snd cf = (Main,Label l' ⊕ 1))↩⇘p⇙
(λcf cf'. cf'(rets [:=] map cf outs))→ (Main,Label (l' + 1))"
by(fastforce intro:PCFG.MainReturn)
thus ?case by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
next
case (ProcReturn p ins outs c l p' es' rets' l' ins' outs' c' ps)
from ‹(p', Exit) = sourcenode a›[THEN sym]
‹(p, Label l') = targetnode a›[THEN sym] ‹well_formed procs›
‹(p, ins, outs, c) ∈ set procs› ‹(p', ins', outs', c') ∈ set procs›
‹(Main, n) = sourcenode a ∨ (Main, n) = targetnode a›
have False by fastforce
thus ?case by simp
next
case (MainCallReturn nx p es rets nx')
from ‹(Main,n) = sourcenode a ∨ (Main,n) = targetnode a› show ?case
proof
assume "(Main,n) = sourcenode a"
with ‹(Main, nx) = sourcenode a›[THEN sym] have [simp]:"nx = n" by simp
from ‹n ≠ Entry› ‹prog ⊢ nx -CEdge (p, es, rets)→⇩p nx'›
have "if (b) prog else c⇩2 ⊢ n ⊕ 1 -CEdge (p, es, rets)→⇩p nx' ⊕ 1"
by(fastforce intro:Proc_CFG_edge_CondTrue_source_not_Entry)
hence "if (b) prog else c⇩2,procs ⊢ (Main,n ⊕ 1) -(λs. False)⇩√→
(Main,nx' ⊕ 1)" by -(rule PCFG.MainCallReturn)
thus ?thesis by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
next
assume "(Main, n) = targetnode a"
from ‹prog ⊢ nx -CEdge (p, es, rets)→⇩p nx'›
have "nx ≠ Entry" by(fastforce dest:Proc_CFG_Call_Labels)
with ‹prog ⊢ nx -CEdge (p, es, rets)→⇩p nx'›
have "if (b) prog else c⇩2 ⊢ nx ⊕ 1 -CEdge (p, es, rets)→⇩p nx' ⊕ 1"
by(fastforce intro:Proc_CFG_edge_CondTrue_source_not_Entry)
hence "if (b) prog else c⇩2,procs ⊢ (Main,nx ⊕ 1) -(λs. False)⇩√→ (Main,nx' ⊕ 1)"
by -(rule PCFG.MainCallReturn)
with ‹(Main, n) = targetnode a› ‹(Main, nx') = targetnode a›[THEN sym]
show ?thesis by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
qed
next
case (ProcCallReturn p ins outs c nx p' es' rets' n' ps)
from ‹(p, nx) = sourcenode a›[THEN sym] ‹(p, n') = targetnode a›[THEN sym]
‹(p, ins, outs, c) ∈ set procs› ‹well_formed procs›
‹(Main, n) = sourcenode a ∨ (Main, n) = targetnode a›
have False by fastforce
thus ?case by simp
qed
qed

lemma path_Main_CondTrue:
assumes "Rep_wf_prog wfp = (prog,procs)"
and "Rep_wf_prog wfp' = (if (b) prog else c⇩2,procs)"
shows "⟦wfp ⊢ (Main,n) -as→* (p',n'); ∀a ∈ set as. intra_kind (kind a); n ≠ Entry⟧
⟹ wfp' ⊢ (Main,n ⊕ 1) -as ⊕s 1→* (p',n' ⊕ 1)"
proof(induct "(Main,n)" as "(p',n')" arbitrary:n rule:ProcCFG.path.induct)
case empty_path
from ‹CFG.valid_node sourcenode targetnode (valid_edge wfp) (Main, n')›
‹n' ≠ Entry› ‹Rep_wf_prog wfp = (prog,procs)›
‹Rep_wf_prog wfp' = (if (b) prog else c⇩2,procs)›
have "CFG.valid_node sourcenode targetnode (valid_edge wfp') (Main, n' ⊕ 1)"
by(fastforce intro:valid_node_Main_CondTrue)
with ‹Main = p'› show ?case
by(fastforce intro:ProcCFG.empty_path simp:label_incrs_def)
next
case (Cons_path n'' as a n)
note IH = ‹⋀n.  ⟦n'' = (Main, n); ∀a∈set as. intra_kind (kind a); n ≠ Entry⟧
⟹ wfp' ⊢ (Main, n ⊕ 1) -as ⊕s 1→* (p', n' ⊕ 1)›
note [simp] = ‹Rep_wf_prog wfp = (prog,procs)›
‹Rep_wf_prog wfp' = (if (b) prog else c⇩2,procs)›
from ‹Rep_wf_prog wfp = (prog,procs)› have wf:"well_formed procs"
by(fastforce intro:wf_wf_prog)
from ‹∀a∈set (a # as). intra_kind (kind a)› have "intra_kind (kind a)"
and "∀a∈set as. intra_kind (kind a)" by simp_all
from ‹valid_edge wfp a› ‹sourcenode a = (Main, n)› ‹targetnode a = n''›
‹intra_kind (kind a)› wf
obtain nx'' where "n'' = (Main,nx'')" and "nx'' ≠ Entry"
by(auto elim!:PCFG.cases simp:valid_edge_def intra_kind_def)
from IH[OF ‹n'' = (Main,nx'')› ‹∀a∈set as. intra_kind (kind a)› ‹nx'' ≠ Entry›]
have path:"wfp' ⊢ (Main, nx'' ⊕ 1) -as ⊕s 1→* (p', n' ⊕ 1)" .
from ‹valid_edge wfp a› ‹sourcenode a = (Main, n)› ‹targetnode a = n''›
‹n'' = (Main,nx'')› ‹n ≠ Entry› ‹intra_kind (kind a)› wf
have "if (b) prog else c⇩2,procs ⊢ (Main, n ⊕ 1) -kind a→ (Main, nx'' ⊕ 1)"
by(fastforce intro:PCFG_Main_edge_CondTrue_source_not_Entry simp:valid_edge_def)
with path ‹sourcenode a = (Main, n)› ‹targetnode a = n''› ‹n'' = (Main,nx'')›
show ?case
apply(cases a) apply(clarsimp simp:label_incrs_def)
by(auto intro:ProcCFG.Cons_path simp:valid_edge_def)
qed

subsubsection ‹From ‹prog› to ‹if (b) c⇩1 else prog››

lemma Proc_CFG_edge_CondFalse_source_not_Entry:
"⟦prog ⊢ n -et→⇩p n'; n ≠ Entry⟧
⟹ if (b) c⇩1 else prog ⊢ n ⊕ (#:c⇩1 + 1) -et→⇩p n' ⊕ (#:c⇩1 + 1)"
by(induct rule:Proc_CFG.induct)(fastforce intro:Proc_CFG_CondElse Proc_CFG.intros)+

lemma PCFG_Main_edge_CondFalse_source_not_Entry:
"⟦prog,procs ⊢ (Main,n) -et→ (p',n'); n ≠ Entry; intra_kind et; well_formed procs⟧
⟹ if (b) c⇩1 else prog,procs ⊢ (Main,n ⊕ (#:c⇩1 + 1)) -et→ (p',n' ⊕ (#:c⇩1 + 1))"
proof(induct "(Main,n)" et "(p',n')" rule:PCFG.induct)
case Main
thus ?case
by(fastforce dest:Proc_CFG_edge_CondFalse_source_not_Entry intro:PCFG.Main)
next
case (MainCallReturn p es rets)
from ‹prog ⊢ n -CEdge (p, es, rets)→⇩p n'› ‹n ≠ Entry›
have "if (b) c⇩1 else prog ⊢ n ⊕ (#:c⇩1 + 1) -CEdge (p, es, rets)→⇩p n' ⊕ (#:c⇩1 + 1)"
by(rule Proc_CFG_edge_CondFalse_source_not_Entry)
with MainCallReturn show ?case by(fastforce intro:PCFG.MainCallReturn)
qed (auto simp:intra_kind_def)

lemma valid_node_Main_CondFalse:
assumes "CFG.valid_node sourcenode targetnode (valid_edge wfp) (Main,n)"
and "n ≠ Entry" and "Rep_wf_prog wfp = (prog,procs)"
and "Rep_wf_prog wfp' = (if (b) c⇩1 else prog,procs)"
shows "CFG.valid_node sourcenode targetnode (valid_edge wfp')
(Main, n ⊕ (#:c⇩1 + 1))"
proof -
note [simp] = ‹Rep_wf_prog wfp = (prog,procs)›
‹Rep_wf_prog wfp' = (if (b) c⇩1 else prog,procs)›
from ‹Rep_wf_prog wfp = (prog,procs)› have wf:"well_formed procs"
by(fastforce intro:wf_wf_prog)
from ‹CFG.valid_node sourcenode targetnode (valid_edge wfp) (Main,n)›
obtain a where "prog,procs ⊢ sourcenode a -kind a→ targetnode a"
and "(Main,n) = sourcenode a ∨ (Main,n) = targetnode a"
by(fastforce simp:ProcCFG.valid_node_def valid_edge_def)
from this ‹n ≠ Entry› wf show ?thesis
proof(induct "sourcenode a" "kind a" "targetnode a" rule:PCFG.induct)
case (Main nx nx')
from ‹(Main,n) = sourcenode a ∨ (Main,n) = targetnode a› show ?case
proof
assume "(Main,n) = sourcenode a"
with ‹(Main, nx) = sourcenode a›[THEN sym] have [simp]:"nx = n" by simp
from ‹n ≠ Entry› ‹prog ⊢ nx -IEdge (kind a)→⇩p nx'›
have "if (b) c⇩1 else prog ⊢ n ⊕ (#:c⇩1 + 1) -IEdge (kind a)→⇩p nx' ⊕ (#:c⇩1 + 1)"
by(fastforce intro:Proc_CFG_edge_CondFalse_source_not_Entry)
hence "if (b) c⇩1 else prog,procs ⊢ (Main,n ⊕ (#:c⇩1 + 1)) -kind a→
(Main,nx' ⊕ (#:c⇩1 + 1))" by(rule PCFG.Main)
thus ?thesis by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
next
assume "(Main, n) = targetnode a"
show ?thesis
proof(cases "nx = Entry")
case True
with ‹prog ⊢ nx -IEdge (kind a)→⇩p nx'›
have "nx' = Exit ∨ nx' = Label 0" by(fastforce dest:Proc_CFG_EntryD)
thus ?thesis
proof
assume "nx' = Exit"
with ‹(Main, n) = targetnode a› ‹(Main, nx') = targetnode a›[THEN sym]
show ?thesis by simp
next
assume "nx' = Label 0"
have "if (b) c⇩1 else prog ⊢ Label 0
-IEdge (λcf. state_check cf b (Some false))⇩√→⇩p Label (#:c⇩1 + 1)"
by(rule Proc_CFG_CondFalse)
with ‹nx' = Label 0›
have "if (b) c⇩1 else prog,procs ⊢ (Main,Label 0)
-(λcf. state_check cf b (Some false))⇩√→ (Main,nx' ⊕ (#:c⇩1 + 1))"
by(fastforce intro:PCFG.Main)
with ‹(Main, n) = targetnode a› ‹(Main, nx') = targetnode a›[THEN sym]
show ?thesis
by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
qed
next
case False
with ‹prog ⊢ nx -IEdge (kind a)→⇩p nx'›
have "if (b) c⇩1 else prog ⊢ nx ⊕ (#:c⇩1 + 1) -IEdge (kind a)→⇩p nx' ⊕ (#:c⇩1 + 1)"
by(fastforce intro:Proc_CFG_edge_CondFalse_source_not_Entry)
hence "if (b) c⇩1 else prog,procs ⊢ (Main,nx ⊕ (#:c⇩1 + 1)) -kind a→
(Main,nx' ⊕ (#:c⇩1 + 1))" by(rule PCFG.Main)
with ‹(Main, n) = targetnode a› ‹(Main, nx') = targetnode a›[THEN sym]
show ?thesis by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
qed
qed
next
case (Proc p ins outs c nx n' ps)
from ‹(p, nx) = sourcenode a›[THEN sym] ‹(p, n') = targetnode a›[THEN sym]
‹(p, ins, outs, c) ∈ set procs› ‹well_formed procs›
‹(Main, n) = sourcenode a ∨ (Main, n) = targetnode a›
have False by fastforce
thus ?case by simp
next
case (MainCall l p es rets n' ins outs c)
from ‹(p, ins, outs, c) ∈ set procs› ‹(p, Entry) = targetnode a›[THEN sym]
‹(Main, Label l) = sourcenode a›[THEN sym] wf
‹(Main, n) = sourcenode a ∨ (Main, n) = targetnode a›
have [simp]:"n = Label l" by fastforce
from ‹prog ⊢ Label l -CEdge (p, es, rets)→⇩p n'›
have "if (b) c⇩1 else prog ⊢ Label l ⊕ (#:c⇩1 + 1) -CEdge (p, es, rets)→⇩p
n' ⊕ (#:c⇩1 + 1)" by -(rule Proc_CFG_edge_CondFalse_source_not_Entry,auto)
with ‹(p, ins, outs, c) ∈ set procs›
have "if (b) c⇩1 else prog,procs ⊢ (Main,Label (l + (#:c⇩1 + 1)))
-(λs. True):(Main,n' ⊕ (#:c⇩1 + 1))↪⇘p⇙map (λe cf. interpret e cf) es→ (p,Entry)"
by(fastforce intro:PCFG.MainCall)
thus ?case by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
next
case (ProcCall p ins outs c l p' es' rets' l' ins' outs' c' ps)
from ‹(p, Label l) = sourcenode a›[THEN sym]
‹(p', Entry) = targetnode a›[THEN sym]  ‹well_formed procs›
‹(p, ins, outs, c) ∈ set procs› ‹(p', ins', outs', c') ∈ set procs›
‹(Main, n) = sourcenode a ∨ (Main, n) = targetnode a›
have False by fastforce
thus ?case by simp
next
case (MainReturn l p es rets l' ins outs c)
from ‹(p, ins, outs, c) ∈ set procs› ‹(p, Exit) = sourcenode a›[THEN sym]
‹(Main, Label l') = targetnode a›[THEN sym] wf
‹(Main, n) = sourcenode a ∨ (Main, n) = targetnode a›
have [simp]:"n = Label l'" by fastforce
from ‹prog ⊢ Label l -CEdge (p, es, rets)→⇩p Label l'›
have "if (b) c⇩1 else prog ⊢ Label l ⊕ (#:c⇩1 + 1) -CEdge (p, es, rets)→⇩p
Label l' ⊕ (#:c⇩1 + 1)" by -(rule Proc_CFG_edge_CondFalse_source_not_Entry,auto)
with ‹(p, ins, outs, c) ∈ set procs›
have "if (b) c⇩1 else prog,procs ⊢ (p,Exit)
-(λcf. snd cf = (Main,Label l' ⊕ (#:c⇩1 + 1)))↩⇘p⇙
(λcf cf'. cf'(rets [:=] map cf outs))→ (Main,Label (l' + (#:c⇩1 + 1)))"
by(fastforce intro:PCFG.MainReturn)
thus ?case by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
next
case (ProcReturn p ins outs c l p' es' rets' l' ins' outs' c' ps)
from ‹(p', Exit) = sourcenode a›[THEN sym]
‹(p, Label l') = targetnode a›[THEN sym] ‹well_formed procs›
‹(p, ins, outs, c) ∈ set procs› ‹(p', ins', outs', c') ∈ set procs›
‹(Main, n) = sourcenode a ∨ (Main, n) = targetnode a›
have False by fastforce
thus ?case by simp
next
case (MainCallReturn nx p es rets nx')
from ‹(Main,n) = sourcenode a ∨ (Main,n) = targetnode a› show ?case
proof
assume "(Main,n) = sourcenode a"
with ‹(Main, nx) = sourcenode a›[THEN sym] have [simp]:"nx = n" by simp
from ‹n ≠ Entry› ‹prog ⊢ nx -CEdge (p, es, rets)→⇩p nx'›
have "if (b) c⇩1 else prog ⊢ n ⊕ (#:c⇩1 + 1) -CEdge (p, es, rets)→⇩p
nx' ⊕ (#:c⇩1 + 1)" by(fastforce intro:Proc_CFG_edge_CondFalse_source_not_Entry)
hence "if (b) c⇩1 else prog,procs ⊢ (Main,n ⊕ (#:c⇩1 + 1))
-(λs. False)⇩√→ (Main,nx' ⊕ (#:c⇩1 + 1))" by -(rule PCFG.MainCallReturn)
thus ?thesis by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
next
assume "(Main, n) = targetnode a"
from ‹prog ⊢ nx -CEdge (p, es, rets)→⇩p nx'›
have "nx ≠ Entry" by(fastforce dest:Proc_CFG_Call_Labels)
with ‹prog ⊢ nx -CEdge (p, es, rets)→⇩p nx'›
have "if (b) c⇩1 else prog ⊢ nx ⊕ (#:c⇩1 + 1) -CEdge (p, es, rets)→⇩p
nx' ⊕ (#:c⇩1 + 1)" by(fastforce intro:Proc_CFG_edge_CondFalse_source_not_Entry)
hence "if (b) c⇩1 else prog,procs ⊢ (Main,nx ⊕ (#:c⇩1 + 1))
-(λs. False)⇩√→ (Main,nx' ⊕ (#:c⇩1 + 1))" by -(rule PCFG.MainCallReturn)
with ‹(Main, n) = targetnode a› ‹(Main, nx') = targetnode a›[THEN sym]
show ?thesis by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
qed
next
case (ProcCallReturn p ins outs c nx p' es' rets' n' ps)
from ‹(p, nx) = sourcenode a›[THEN sym] ‹(p, n') = targetnode a›[THEN sym]
‹(p, ins, outs, c) ∈ set procs› ‹well_formed procs›
‹(Main, n) = sourcenode a ∨ (Main, n) = targetnode a›
have False by fastforce
thus ?case by simp
qed
qed

lemma path_Main_CondFalse:
assumes "Rep_wf_prog wfp = (prog,procs)"
and "Rep_wf_prog wfp' = (if (b) c⇩1 else prog,procs)"
shows "⟦wfp ⊢ (Main,n) -as→* (p',n'); ∀a ∈ set as. intra_kind (kind a); n ≠ Entry⟧
⟹ wfp' ⊢ (Main,n ⊕ (#:c⇩1 + 1)) -as ⊕s (#:c⇩1 + 1)→* (p',n' ⊕ (#:c⇩1 + 1))"
proof(induct "(Main,n)" as "(p',n')" arbitrary:n rule:ProcCFG.path.induct)
case empty_path
from ‹CFG.valid_node sourcenode targetnode (valid_edge wfp) (Main, n')›
‹n' ≠ Entry› ‹Rep_wf_prog wfp = (prog,procs)›
‹Rep_wf_prog wfp' = (if (b) c⇩1 else prog,procs)›
have "CFG.valid_node sourcenode targetnode (valid_edge wfp') (Main, n' ⊕ (#:c⇩1 + 1))"
by(fastforce intro:valid_node_Main_CondFalse)
with ‹Main = p'› show ?case
by(fastforce intro:ProcCFG.empty_path simp:label_incrs_def)
next
case (Cons_path n'' as a n)
note IH = ‹⋀n. ⋀n.  ⟦n'' = (Main, n); ∀a∈set as. intra_kind (kind a); n ≠ Entry⟧
⟹ wfp' ⊢ (Main, n ⊕ (#:c⇩1 + 1)) -as ⊕s (#:c⇩1 + 1)→* (p', n' ⊕ (#:c⇩1 + 1))›
note [simp] = ‹Rep_wf_prog wfp = (prog,procs)›
‹Rep_wf_prog wfp' = (if (b) c⇩1 else prog,procs)›
from ‹Rep_wf_prog wfp = (prog,procs)› have wf:"well_formed procs"
by(fastforce intro:wf_wf_prog)
from ‹∀a∈set (a # as). intra_kind (kind a)› have "intra_kind (kind a)"
and "∀a∈set as. intra_kind (kind a)" by simp_all
from ‹valid_edge wfp a› ‹sourcenode a = (Main, n)› ‹targetnode a = n''›
‹intra_kind (kind a)› wf
obtain nx'' where "n'' = (Main,nx'')" and "nx'' ≠ Entry"
by(auto elim!:PCFG.cases simp:valid_edge_def intra_kind_def)
from IH[OF ‹n'' = (Main,nx'')› ‹∀a∈set as. intra_kind (kind a)› ‹nx'' ≠ Entry›]
have path:"wfp' ⊢ (Main, nx'' ⊕ (#:c⇩1 + 1)) -as ⊕s (#:c⇩1 + 1)→*
(p', n' ⊕ (#:c⇩1 + 1))" .
from ‹valid_edge wfp a› ‹sourcenode a = (Main, n)› ‹targetnode a = n''›
‹n'' = (Main,nx'')› ‹n ≠ Entry› ‹intra_kind (kind a)› wf
have "if (b) c⇩1 else prog,procs ⊢ (Main, n ⊕ (#:c⇩1 + 1)) -kind a→
(Main, nx'' ⊕ (#:c⇩1 + 1))"
by(fastforce intro:PCFG_Main_edge_CondFalse_source_not_Entry simp:valid_edge_def)
with path ‹sourcenode a = (Main, n)› ‹targetnode a = n''› ‹n'' = (Main,nx'')›
show ?case
apply(cases a) apply(clarsimp simp:label_incrs_def)
by(auto intro:ProcCFG.Cons_path simp:valid_edge_def)
qed

subsubsection ‹From ‹prog› to ‹while (b) prog››

lemma Proc_CFG_edge_WhileBody_source_not_Entry:
"⟦prog ⊢ n -et→⇩p n'; n ≠ Entry; n' ≠ Exit⟧
⟹ while (b) prog ⊢ n ⊕ 2 -et→⇩p n' ⊕ 2"
by(induct rule:Proc_CFG.induct)(fastforce intro:Proc_CFG_WhileBody Proc_CFG.intros)+

lemma PCFG_Main_edge_WhileBody_source_not_Entry:
"⟦prog,procs ⊢ (Main,n) -et→ (p',n'); n ≠ Entry; n' ≠ Exit; intra_kind et;
well_formed procs⟧ ⟹ while (b) prog,procs ⊢ (Main,n ⊕ 2) -et→ (p',n' ⊕ 2)"
proof(induct "(Main,n)" et "(p',n')" rule:PCFG.induct)
case Main
thus ?case
by(fastforce dest:Proc_CFG_edge_WhileBody_source_not_Entry intro:PCFG.Main)
next
case (MainCallReturn p es rets)
from ‹prog ⊢ n -CEdge (p, es, rets)→⇩p n'› ‹n ≠ Entry› ‹n' ≠ Exit›
have "while (b) prog ⊢ n ⊕ 2 -CEdge (p, es, rets)→⇩p n' ⊕ 2"
by(rule Proc_CFG_edge_WhileBody_source_not_Entry)
with MainCallReturn show ?case by(fastforce intro:PCFG.MainCallReturn)
qed (auto simp:intra_kind_def)

lemma valid_node_Main_WhileBody:
assumes "CFG.valid_node sourcenode targetnode (valid_edge wfp) (Main,n)"
and "n ≠ Entry" and "Rep_wf_prog wfp = (prog,procs)"
and "Rep_wf_prog wfp' = (while (b) prog,procs)"
shows "CFG.valid_node sourcenode targetnode (valid_edge wfp') (Main, n ⊕ 2)"
proof -
note [simp] = ‹Rep_wf_prog wfp = (prog,procs)›
‹Rep_wf_prog wfp' = (while (b) prog,procs)›
from ‹Rep_wf_prog wfp = (prog,procs)› have wf:"well_formed procs"
by(fastforce intro:wf_wf_prog)
from ‹CFG.valid_node sourcenode targetnode (valid_edge wfp) (Main,n)›
obtain a where "prog,procs ⊢ sourcenode a -kind a→ targetnode a"
and "(Main,n) = sourcenode a ∨ (Main,n) = targetnode a"
by(fastforce simp:ProcCFG.valid_node_def valid_edge_def)
from this ‹n ≠ Entry› wf show ?thesis
proof(induct "sourcenode a" "kind a" "targetnode a" rule:PCFG.induct)
case (Main nx nx')
from ‹(Main,n) = sourcenode a ∨ (Main,n) = targetnode a› show ?case
proof
assume "(Main,n) = sourcenode a"
with ‹(Main, nx) = sourcenode a›[THEN sym] have [simp]:"nx = n" by simp
show ?thesis
proof(cases "nx' = Exit")
case True
with ‹n ≠ Entry› ‹prog ⊢ nx -IEdge (kind a)→⇩p nx'›
have "while (b) prog ⊢ n ⊕ 2 -IEdge (kind a)→⇩p Label 0"
by(fastforce intro:Proc_CFG_WhileBodyExit)
hence "while (b) prog,procs ⊢ (Main,n ⊕ 2) -kind a→ (Main,Label 0)"
by(rule PCFG.Main)
thus ?thesis by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
next
case False
with ‹n ≠ Entry› ‹prog ⊢ nx -IEdge (kind a)→⇩p nx'›
have "while (b) prog ⊢ n ⊕ 2 -IEdge (kind a)→⇩p nx' ⊕ 2"
by(fastforce intro:Proc_CFG_edge_WhileBody_source_not_Entry)
hence "while (b) prog,procs ⊢ (Main,n ⊕ 2) -kind a→ (Main,nx' ⊕ 2)"
by(rule PCFG.Main)
thus ?thesis by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
qed
next
assume "(Main, n) = targetnode a"
show ?thesis
proof(cases "nx = Entry")
case True
with ‹prog ⊢ nx -IEdge (kind a)→⇩p nx'›
have "nx' = Exit ∨ nx' = Label 0" by(fastforce dest:Proc_CFG_EntryD)
thus ?thesis
proof
assume "nx' = Exit"
with ‹(Main, n) = targetnode a› ‹(Main, nx') = targetnode a›[THEN sym]
show ?thesis by simp
next
assume "nx' = Label 0"
have "while (b) prog ⊢ Label 0
-IEdge (λcf. state_check cf b (Some true))⇩√→⇩p Label 2"
by(rule Proc_CFG_WhileTrue)
hence "while (b) prog,procs ⊢ (Main,Label 0)
-(λcf. state_check cf b (Some true))⇩√→ (Main,Label 2)"
by(fastforce intro:PCFG.Main)
with ‹(Main, n) = targetnode a› ‹(Main, nx') = targetnode a›[THEN sym]
‹nx' = Label 0› show ?thesis
by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
qed
next
case False
show ?thesis
proof(cases "nx' = Exit")
case True
with ‹(Main, n) = targetnode a› ‹(Main, nx') = targetnode a›[THEN sym]
show ?thesis by simp
next
case False
with ‹prog ⊢ nx -IEdge (kind a)→⇩p nx'› ‹nx ≠ Entry›
have "while (b) prog ⊢ nx ⊕ 2 -IEdge (kind a)→⇩p nx' ⊕ 2"
by(fastforce intro:Proc_CFG_edge_WhileBody_source_not_Entry)
hence "while (b) prog,procs ⊢ (Main,nx ⊕ 2)  -kind a→
(Main,nx' ⊕ 2)" by(rule PCFG.Main)
with ‹(Main, n) = targetnode a› ‹(Main, nx') = targetnode a›[THEN sym]
show ?thesis
by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
qed
qed
qed
next
case (Proc p ins outs c nx n' ps)
from ‹(p, nx) = sourcenode a›[THEN sym] ‹(p, n') = targetnode a›[THEN sym]
‹(Main, n) = sourcenode a ∨ (Main, n) = targetnode a›
‹(p, ins, outs, c) ∈ set procs› ‹well_formed procs›
have False by fastforce
thus ?case by simp
next
case (MainCall l p es rets n' ins outs c)
from ‹(p, ins, outs, c) ∈ set procs› ‹(p, Entry) = targetnode a›[THEN sym]
‹(Main, Label l) = sourcenode a›[THEN sym] wf
‹(Main, n) = sourcenode a ∨ (Main, n) = targetnode a›
have [simp]:"n = Label l" by fastforce
from ‹prog ⊢ Label l -CEdge (p, es, rets)→⇩p n'› have "n' ≠ Exit"
by(fastforce dest:Proc_CFG_Call_Labels)
with ‹prog ⊢ Label l -CEdge (p, es, rets)→⇩p n'›
have "while (b) prog ⊢ Label l ⊕ 2 -CEdge (p, es, rets)→⇩p
n' ⊕ 2" by -(rule Proc_CFG_edge_WhileBody_source_not_Entry,auto)
with ‹(p, ins, outs, c) ∈ set procs›
have "while (b) prog,procs ⊢ (Main,Label l ⊕ 2)
-(λs. True):(Main,n' ⊕ 2)↪⇘p⇙map (λe cf. interpret e cf) es→ (p,Entry)"
by(fastforce intro:PCFG.MainCall)
thus ?case by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
next
case (ProcCall p ins outs c l p' es' rets' l' ins' outs' c')
from ‹(p, Label l) = sourcenode a›[THEN sym]
‹(p', Entry) = targetnode a›[THEN sym]  ‹well_formed procs›
‹(p, ins, outs, c) ∈ set procs› ‹(p', ins', outs', c') ∈ set procs›
‹(Main, n) = sourcenode a ∨ (Main, n) = targetnode a›
have False by fastforce
thus ?case by simp
next
case (MainReturn l p es rets l' ins outs c)
from ‹(p, ins, outs, c) ∈ set procs› ‹(p, Exit) = sourcenode a›[THEN sym]
‹(Main, Label l') = targetnode a›[THEN sym] wf
‹(Main, n) = sourcenode a ∨ (Main, n) = targetnode a›
have [simp]:"n = Label l'" by fastforce
from ‹prog ⊢ Label l -CEdge (p, es, rets)→⇩p Label l'›
have "while (b) prog ⊢ Label l ⊕ 2 -CEdge (p, es, rets)→⇩p
Label l' ⊕ 2" by -(rule Proc_CFG_edge_WhileBody_source_not_Entry,auto)
with ‹(p, ins, outs, c) ∈ set procs›
have "while (b) prog,procs ⊢ (p,Exit) -(λcf. snd cf = (Main,Label l' ⊕ 2))↩⇘p⇙
(λcf cf'. cf'(rets [:=] map cf outs))→ (Main,Label l' ⊕ 2)"
by(fastforce intro:PCFG.MainReturn)
thus ?case by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
next
case (ProcReturn p ins outs c l p' es' rets' l' ins' outs' c' ps)
from ‹(p', Exit) = sourcenode a›[THEN sym]
‹(p, Label l') = targetnode a›[THEN sym] ‹well_formed procs›
‹(p, ins, outs, c) ∈ set procs› ‹(p', ins', outs', c') ∈ set procs›
‹(Main, n) = sourcenode a ∨ (Main, n) = targetnode a›
have False by fastforce
thus ?case by simp
next
case (MainCallReturn nx p es rets nx')
from ‹(Main,n) = sourcenode a ∨ (Main,n) = targetnode a› show ?case
proof
assume "(Main,n) = sourcenode a"
with ‹(Main, nx) = sourcenode a›[THEN sym] have [simp]:"nx = n" by simp
from ‹prog ⊢ nx -CEdge (p, es, rets)→⇩p nx'› have "nx' ≠ Exit"
by(fastforce dest:Proc_CFG_Call_Labels)
with ‹n ≠ Entry› ‹prog ⊢ nx -CEdge (p, es, rets)→⇩p nx'›
have "while (b) prog ⊢ n ⊕ 2 -CEdge (p, es, rets)→⇩p
nx' ⊕ 2" by(fastforce intro:Proc_CFG_edge_WhileBody_source_not_Entry)
hence "while (b) prog,procs ⊢ (Main,n ⊕ 2) -(λs. False)⇩√→ (Main,nx' ⊕ 2)"
by -(rule PCFG.MainCallReturn)
thus ?thesis by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
next
assume "(Main, n) = targetnode a"
from ‹prog ⊢ nx -CEdge (p, es, rets)→⇩p nx'›
have "nx ≠ Entry" and "nx' ≠ Exit" by(auto dest:Proc_CFG_Call_Labels)
with ‹prog ⊢ nx -CEdge (p, es, rets)→⇩p nx'›
have "while (b) prog ⊢ nx ⊕ 2 -CEdge (p, es, rets)→⇩p
nx' ⊕ 2" by(fastforce intro:Proc_CFG_edge_WhileBody_source_not_Entry)
hence "while (b) prog,procs ⊢ (Main,nx ⊕ 2) -(λs. False)⇩√→ (Main,nx' ⊕ 2)"
by -(rule PCFG.MainCallReturn)
with ‹(Main, n) = targetnode a› ‹(Main, nx') = targetnode a›[THEN sym]
show ?thesis by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
qed
next
case (ProcCallReturn p ins outs c nx p' es' rets' n' ps)
from ‹(p, nx) = sourcenode a›[THEN sym] ‹(p, n') = targetnode a›[THEN sym]
‹(p, ins, outs, c) ∈ set procs› ‹well_formed procs›
‹(Main, n) = sourcenode a ∨ (Main, n) = targetnode a›
have False by fastforce
thus ?case by simp
qed
qed

lemma path_Main_WhileBody:
assumes "Rep_wf_prog wfp = (prog,procs)"
and "Rep_wf_prog wfp' = (while (b) prog,procs)"
shows "⟦wfp ⊢ (Main,n) -as→* (p',n'); ∀a ∈ set as. intra_kind (kind a);
n ≠ Entry; n' ≠ Exit⟧ ⟹ wfp' ⊢ (Main,n ⊕ 2) -as ⊕s 2→* (p',n' ⊕ 2)"
proof(induct "(Main,n)" as "(p',n')" arbitrary:n rule:ProcCFG.path.induct)
case empty_path
from ‹CFG.valid_node sourcenode targetnode (valid_edge wfp) (Main, n')›
‹n' ≠ Entry› ‹Rep_wf_prog wfp = (prog,procs)›
‹Rep_wf_prog wfp' = (while (b) prog,procs)›
have "CFG.valid_node sourcenode targetnode (valid_edge wfp') (Main, n' ⊕ 2)"
by(fastforce intro:valid_node_Main_WhileBody)
with ‹Main = p'› show ?case
by(fastforce intro:ProcCFG.empty_path simp:label_incrs_def)
next
case (Cons_path n'' as a n)
note IH = ‹⋀n.  ⟦n'' = (Main, n); ∀a∈set as. intra_kind (kind a); n ≠ Entry;
n' ≠ Exit⟧ ⟹ wfp' ⊢ (Main, n ⊕ 2) -as ⊕s 2→* (p', n' ⊕ 2)›
note [simp] = ‹Rep_wf_prog wfp = (prog,procs)›
‹Rep_wf_prog wfp' = (while (b) prog,procs)›
from ‹Rep_wf_prog wfp = (prog,procs)› have wf:"well_formed procs"
by(fastforce intro:wf_wf_prog)
from ‹∀a∈set (a # as). intra_kind (kind a)› have "intra_kind (kind a)"
and "∀a∈set as. intra_kind (kind a)" by simp_all
from ‹valid_edge wfp```