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. 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:
  fixes wfp
  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:
  fixes wfp
  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:
  fixes wfp
  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:
  fixes wfp
  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:
  fixes wfp
  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:
  fixes wfp
  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:
  fixes wfp
  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:
  fixes wfp
  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:
  fixes wfp
  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 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› ‹n' ≠ Exit›]
  have path:"wfp' ⊢ (Main, nx'' ⊕ 2) -as ⊕s 2→* (p', n' ⊕ 2)" .
  with ‹n' ≠ Exit› have "nx'' ≠ Exit" by(fastforce dest:ProcCFGExit.path_Exit_source)
  with ‹valid_edge wfp a› ‹sourcenode a = (Main, n)› ‹targetnode a = n''›
    ‹n'' = (Main,nx'')› ‹n ≠ Entry› ‹intra_kind (kind a)› wf
  have "while (b) prog,procs ⊢ (Main, n ⊕ 2) -kind a→ (Main, nx'' ⊕ 2)"
    by(fastforce intro:PCFG_Main_edge_WhileBody_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 ‹Existence of intraprodecural paths›

lemma Label_Proc_CFG_Entry_Exit_path_Main:
  fixes wfp
  assumes "Rep_wf_prog wfp = (prog,procs)" and "l < #:prog"
  obtains as as' where "wfp ⊢ (Main,Label l) -as→* (Main,Exit)"
  and "∀a ∈ set as. intra_kind (kind a)"
  and "wfp ⊢ (Main,Entry) -as'→* (Main,Label l)"
  and "∀a ∈ set as'. intra_kind (kind a)"
proof(atomize_elim)
  from ‹Rep_wf_prog wfp = (prog,procs)› have wf:"well_formed procs" 
    by(fastforce intro:wf_wf_prog)
  from ‹l < #:prog› ‹Rep_wf_prog wfp = (prog,procs)›
  show "∃as as'. wfp ⊢ (Main, Label l) -as→* (Main, Exit) ∧
    (∀a∈set as. intra_kind (kind a)) ∧
    wfp ⊢ (Main, Entry) -as'→* (Main, Label l) ∧ (∀a∈set as'. intra_kind (kind a))"
  proof(induct prog arbitrary:l wfp)
    case Skip
    note [simp] = ‹Rep_wf_prog wfp = (Skip, procs)›
    from ‹l < #:Skip› have [simp]:"l = 0" by simp
    have "wfp ⊢ (Main,Entry) -[((Main,Entry),(λs. True)⇩√,(Main,Label 0))]→* 
      (Main,Label 0)" 
      by(fastforce intro:ProcCFG.path.intros Main Proc_CFG_Entry
                   simp:valid_edge_def ProcCFG.valid_node_def)
    moreover
    have "wfp ⊢ (Main,Label l) -[((Main,Label l),⇑id,(Main,Exit))]→* (Main,Exit)" 
      by(fastforce intro:ProcCFG.path.intros Main Proc_CFG_Skip simp:valid_edge_def)
    ultimately show ?case by(fastforce simp:intra_kind_def)
  next
    case (LAss V e)
    note [simp] = ‹Rep_wf_prog wfp = (V:=e, procs)›
    from ‹l < #:V:=e› have "l = 0 ∨ l = 1" by auto
    thus ?case
    proof
      assume [simp]:"l = 0"
      have "wfp ⊢ (Main,Entry) -[((Main,Entry),(λs. True)⇩√,(Main,Label 0))]→*
        (Main,Label 0)" 
        by(fastforce intro:ProcCFG.path.intros Main Proc_CFG_Entry
                    simp:valid_edge_def ProcCFG.valid_node_def)
      moreover
      have "wfp ⊢ (Main,Label 0) 
        -((Main,Label 0),⇑(λcf. update cf V e),(Main,Label 1))#
        [((Main,Label 1),⇑id,(Main,Exit))]→* (Main,Exit)"
        by(fastforce intro:ProcCFG.Cons_path ProcCFG.path.intros Main Proc_CFG_LAss 
          Proc_CFG_LAssSkip simp:valid_edge_def ProcCFG.valid_node_def)
      ultimately show ?thesis by(fastforce simp:intra_kind_def)
    next
      assume [simp]:"l = 1"
      have "wfp ⊢ (Main,Entry) -((Main,Entry),(λs. True)⇩√,(Main,Label 0))#
        [((Main,Label 0),⇑(λcf. update cf V e),(Main,Label 1))]→* (Main,Label 1)"
        by(fastforce intro:ProcCFG.path.intros Main Proc_CFG_LAss ProcCFG.Cons_path 
          Main Proc_CFG_Entry simp:ProcCFG.valid_node_def valid_edge_def)
      moreover
      have "wfp ⊢ (Main,Label 1) -[((Main,Label 1),⇑id,(Main,Exit))]→* 
        (Main,Exit)" by(fastforce intro:ProcCFG.path.intros  Main Proc_CFG_LAssSkip
        simp:valid_edge_def ProcCFG.valid_node_def)
      ultimately show ?thesis by(fastforce simp:intra_kind_def)
    qed
  next
    case (Seq c⇩1 c⇩2)
    note IH1 = ‹⋀l wfp. ⟦l < #:c⇩1; Rep_wf_prog wfp = (c⇩1, procs)⟧ ⟹
      ∃as as'. wfp ⊢ (Main, Label l) -as→* (Main, Exit) ∧ 
      (∀a∈set as. intra_kind (kind a)) ∧
      wfp ⊢ (Main, Entry) -as'→* (Main, Label l) ∧ (∀a∈set as'. intra_kind (kind a))›
    note IH2 = ‹⋀l wfp. ⟦l < #:c⇩2; Rep_wf_prog wfp = (c⇩2, procs)⟧ ⟹
      ∃as as'. wfp ⊢ (Main, Label l) -as→* (Main, Exit) ∧ 
      (∀a∈set as. intra_kind (kind a)) ∧
      wfp ⊢ (Main, Entry) -as'→* (Main, Label l) ∧ (∀a∈set as'. intra_kind (kind a))›
    note [simp] = ‹Rep_wf_prog wfp = (c⇩1;; c⇩2, procs)›
    show ?case
    proof(cases "l < #:c⇩1")
      case True
      from ‹Rep_wf_prog wfp = (c⇩1;; c⇩2, procs)›
      obtain wfp' where [simp]:"Rep_wf_prog wfp' = (c⇩1, procs)" by(erule wfp_Seq1)
      from IH1[OF True this] obtain as as' 
        where path1:"wfp' ⊢ (Main, Label l) -as→* (Main, Exit)"
        and intra1:"∀a∈set as. intra_kind (kind a)"
        and path2:"wfp' ⊢ (Main, Entry) -as'→* (Main, Label l)"
        and intra2:"∀a∈set as'. intra_kind (kind a)" by blast
      from path1 have "as ≠ []" by(fastforce elim:ProcCFG.path.cases)
      then obtain ax asx where [simp]:"as = asx@[ax]"
        by(cases as rule:rev_cases) fastforce+
      with path1 have "wfp' ⊢ (Main, Label l) -asx→* sourcenode ax"
        and "valid_edge wfp' ax" and "targetnode ax = (Main, Exit)"
        by(auto elim:ProcCFG.path_split_snoc)
      from ‹valid_edge wfp' ax› ‹targetnode ax = (Main, Exit)›
      obtain nx where "sourcenode ax = (Main,nx)" 
        by(fastforce elim:PCFG.cases simp:valid_edge_def)
      with ‹wfp' ⊢ (Main, Label l) -asx→* sourcenode ax› have "nx ≠ Entry"
        by fastforce
      moreover
      from ‹valid_edge wfp' ax› ‹sourcenode ax = (Main,nx)› have "nx ≠ Exit"
        by(fastforce intro:ProcCFGExit.Exit_source)
      ultimately obtain lx where [simp]:"nx = Label lx" by(cases nx) auto
      with ‹wfp' ⊢ (Main, Label l) -asx→* sourcenode ax› 
        ‹sourcenode ax = (Main,nx)› intra1
      have path3:"wfp ⊢ (Main, Label l) -asx→* (Main, Label lx)"
        by -(rule path_SeqFirst,auto)
      from ‹valid_edge wfp' ax› ‹targetnode ax = (Main, Exit)›
        ‹sourcenode ax = (Main,nx)› wf
      obtain etx where "c⇩1 ⊢ Label lx -etx→⇩p Exit" 
        by(fastforce elim!:PCFG.cases simp:valid_edge_def)
      then obtain et where [simp]:"etx = IEdge et" 
        by(cases etx)(auto dest:Proc_CFG_Call_Labels)
      with ‹c⇩1 ⊢ Label lx -etx→⇩p Exit› have "intra_kind et"
        by(fastforce intro:Proc_CFG_IEdge_intra_kind)
      from ‹c⇩1 ⊢ Label lx -etx→⇩p Exit› path3
      have path4:"wfp ⊢ (Main, Label l) -asx@
        [((Main, Label lx),et,(Main,Label 0 ⊕ #:c⇩1))] →* (Main,Label 0 ⊕ #:c⇩1)"
        by(fastforce intro:ProcCFG.path_Append ProcCFG.path.intros Proc_CFG_SeqConnect
          Main simp:ProcCFG.valid_node_def valid_edge_def)
      from ‹Rep_wf_prog wfp = (c⇩1;; c⇩2, procs)›
      obtain wfp'' where [simp]:"Rep_wf_prog wfp'' = (c⇩2, procs)" by(erule wfp_Seq2)
      from IH2[OF _ this,of "0"] obtain asx' 
        where "wfp'' ⊢ (Main, Label 0) -asx'→* (Main, Exit)"
        and "∀a∈set asx'. intra_kind (kind a)" by blast
      with path4 intra1 ‹intra_kind et› have "wfp ⊢ (Main, Label l) 
        -(asx@[((Main, Label lx),et,(Main,Label 0 ⊕ #:c⇩1))])@(asx' ⊕s #:c⇩1)→*
        (Main, Exit ⊕ #:c⇩1)"
        by -(erule ProcCFG.path_Append,rule path_Main_SeqSecond,auto)
      moreover
      from intra1 ‹intra_kind et› ‹∀a∈set asx'. intra_kind (kind a)›
      have "∀a ∈ set ((asx@[((Main, Label lx),et,(Main,Label #:c⇩1))])@(asx' ⊕s #:c⇩1)).
        intra_kind (kind a)" by(auto simp:label_incrs_def)
      moreover
      from path2 intra2 have "wfp ⊢ (Main, Entry) -as'→* (Main, Label l)"
        by -(rule path_SeqFirst,auto)
      ultimately show ?thesis using ‹∀a∈set as'. intra_kind (kind a)› by fastforce
    next
      case False
      hence "#:c⇩1 ≤ l" by simp
      then obtain l' where [simp]:"l = l' + #:c⇩1" and "l' = l - #:c⇩1" by simp
      from ‹l < #:c⇩1;; c⇩2› have "l' < #:c⇩2" by simp
      from ‹Rep_wf_prog wfp = (c⇩1;; c⇩2, procs)›
      obtain wfp' where [simp]:"Rep_wf_prog wfp' = (c⇩2, procs)" by(erule wfp_Seq2)
      from IH2[OF ‹l' < #:c⇩2› this] obtain as as' 
        where path1:"wfp' ⊢ (Main, Label l') -as→* (Main, Exit)"
        and intra1:"∀a∈set as. intra_kind (kind a)"
        and path2:"wfp' ⊢ (Main, Entry) -as'→* (Main, Label l')"
        and intra2:"∀a∈set as'. intra_kind (kind a)" by blast
      from path1 intra1
      have "wfp ⊢ (Main, Label l' ⊕ #:c⇩1) -as ⊕s #:c⇩1→* (Main, Exit ⊕ #:c⇩1)"
        by -(rule path_Main_SeqSecond,auto)
      moreover
      from path2 have "as' ≠ []" by(fastforce elim:ProcCFG.path.cases)
      with path2 obtain ax' asx' where [simp]:"as' = ax'#asx'"
        and "sourcenode ax' = (Main, Entry)" and "valid_edge wfp' ax'" 
        and "wfp' ⊢ targetnode ax' -asx'→* (Main, Label l')"
        by -(erule ProcCFG.path_split_Cons,fastforce+)
      from ‹wfp' ⊢ targetnode ax' -asx'→* (Main, Label l')›
      have "targetnode ax' ≠ (Main,Exit)" by fastforce
      with ‹valid_edge wfp' ax'› ‹sourcenode ax' = (Main, Entry)› wf
      have "targetnode ax' = (Main,Label 0)"
        by(fastforce elim:PCFG.cases dest:Proc_CFG_EntryD simp:valid_edge_def)
      with ‹wfp' ⊢ targetnode ax' -asx'→* (Main, Label l')› intra2
      have path3:"wfp ⊢ (Main,Label 0 ⊕ #:c⇩1) -asx' ⊕s #:c⇩1→* 
        (Main, Label l' ⊕ #:c⇩1)" by -(rule path_Main_SeqSecond,auto)
      from ‹Rep_wf_prog wfp = (c⇩1;; c⇩2, procs)›
      obtain wfp'' where [simp]:"Rep_wf_prog wfp'' = (c⇩1, procs)" by(erule wfp_Seq1)
      from IH1[OF _ this,of "0"] obtain xs 
        where "wfp'' ⊢ (Main, Label 0) -xs→* (Main, Exit)"
        and "∀a∈set xs. intra_kind (kind a)" by blast
      from ‹wfp'' ⊢ (Main, Label 0) -xs→* (Main, Exit)› have "xs ≠ []"
        by(fastforce elim:ProcCFG.path.cases)
      then obtain x xs' where [simp]:"xs = xs'@[x]"
        by(cases xs rule:rev_cases) fastforce+
      with ‹wfp'' ⊢ (Main, Label 0) -xs→* (Main, Exit)›
      have "wfp'' ⊢ (Main, Label 0) -xs'→* sourcenode x"
        and "valid_edge wfp'' x" and "targetnode x = (Main, Exit)"
        by(auto elim:ProcCFG.path_split_snoc)
      from ‹valid_edge wfp'' x› ‹targetnode x = (Main, Exit)›
      obtain nx where "sourcenode x = (Main,nx)" 
        by(fastforce elim:PCFG.cases simp:valid_edge_def)
      with ‹wfp'' ⊢ (Main, Label 0) -xs'→* sourcenode x› have "nx ≠ Entry"
        by fastforce
      from ‹valid_edge wfp'' x› ‹sourcenode x = (Main,nx)› have "nx ≠ Exit"
        by(fastforce intro:ProcCFGExit.Exit_source)
      with ‹nx ≠ Entry› obtain lx where [simp]:"nx = Label lx" by(cases nx) auto
      from ‹wfp'' ⊢ (Main, Label 0) -xs'→* sourcenode x› 
        ‹sourcenode x = (Main,nx)› ‹∀a∈set xs. intra_kind (kind a)›
      have "wfp ⊢ (Main, Entry) 
        -((Main, Entry),(λs. True)⇩√,(Main, Label 0))#xs'→* sourcenode x"
        apply simp apply(rule path_SeqFirst[OF ‹Rep_wf_prog wfp'' = (c⇩1, procs)›])
        apply(auto intro!:ProcCFG.Cons_path)
        by(auto intro:Main Proc_CFG_Entry simp:valid_edge_def intra_kind_def)
      with ‹valid_edge wfp'' x› ‹targetnode x = (Main, Exit)› path3
        ‹sourcenode x = (Main,nx)› ‹nx ≠ Entry› ‹sourcenode x = (Main,nx)› wf
      have "wfp ⊢ (Main, Entry) -((((Main, Entry),(λs. True)⇩√,(Main, Label 0))#xs')@
        [(sourcenode x,kind x,(Main,Label #:c⇩1))])@(asx' ⊕s #:c⇩1)→* 
        (Main, Label l' ⊕ #:c⇩1)" 
        by(fastforce intro:ProcCFG.path_Append ProcCFG.path.intros Main 
          Proc_CFG_SeqConnect elim!:PCFG.cases dest:Proc_CFG_Call_Labels
          simp:ProcCFG.valid_node_def valid_edge_def)
      ultimately show ?thesis using intra1 intra2 ‹∀a∈set xs. intra_kind (kind a)›
        by(fastforce simp:label_incrs_def intra_kind_def)
    qed
  next
    case (Cond b c⇩1 c⇩2)
    note IH1 = ‹⋀l wfp. ⟦l < #:c⇩1; Rep_wf_prog wfp = (c⇩1, procs)⟧ ⟹
      ∃as as'. wfp ⊢ (Main, Label l) -as→* (Main, Exit) ∧ 
      (∀a∈set as. intra_kind (kind a)) ∧
      wfp ⊢ (Main, Entry) -as'→* (Main, Label l) ∧ (∀a∈set as'. intra_kind (kind a))›
    note IH2 = ‹⋀l wfp. ⟦l < #:c⇩2; Rep_wf_prog wfp = (c⇩2, procs)⟧ ⟹
      ∃as as'. wfp ⊢ (Main, Label l) -as→* (Main, Exit) ∧ 
      (∀a∈set as. intra_kind (kind a)) ∧
      wfp ⊢ (Main, Entry) -as'→* (Main, Label l) ∧ (∀a∈set as'. intra_kind (kind a))›
    note [simp] = ‹Rep_wf_prog wfp = (if (b) c⇩1 else c⇩2, procs)›
    show ?case
    proof(cases "l = 0")
      case True
      from ‹Rep_wf_prog wfp = (if (b) c⇩1 else c⇩2, procs)›
      obtain wfp' where [simp]:"Rep_wf_prog wfp' = (c⇩1, procs)" by(erule wfp_CondTrue)
      from IH1[OF _ this,of 0] obtain as 
        where path:"wfp' ⊢ (Main, Label 0) -as→* (Main, Exit)"
        and intra:"∀a∈set as. intra_kind (kind a)" by blast
      have "if (b) c⇩1 else c⇩2,procs ⊢ (Main,Label 0)
        -(λcf. state_check cf b (Some true))⇩√→ (Main,Label 0 ⊕ 1)"
        by(fastforce intro:Main Proc_CFG_CondTrue)
      with path intra have "wfp ⊢ (Main,Label 0)
        -[((Main,Label 0),(λcf. state_check cf b (Some true))⇩√,(Main,Label 0 ⊕ 1))]@
        (as ⊕s 1)→* (Main,Exit ⊕ 1)"
        apply - apply(rule ProcCFG.path_Append) apply(rule ProcCFG.path.intros)+
        prefer 5 apply(rule path_Main_CondTrue)
        apply(auto intro:ProcCFG.path.intros simp:valid_edge_def)
        by(fastforce simp:ProcCFG.valid_node_def valid_edge_def)
      moreover
      have "if (b) c⇩1 else c⇩2,procs ⊢ (Main,Entry) -(λs. True)⇩√→ 
        (Main,Label 0)" by(fastforce intro:Main Proc_CFG_Entry)
      hence "wfp ⊢ (Main,Entry) -[((Main,Entry),(λs. True)⇩√,(Main,Label 0))]→* 
        (Main,Label 0)"
        by(fastforce intro:ProcCFG.path.intros 
                    simp:ProcCFG.valid_node_def valid_edge_def)
      ultimately show ?thesis using ‹l = 0› ‹∀a∈set as. intra_kind (kind a)› 
        by(fastforce simp:label_incrs_def intra_kind_def)
    next
      case False
      hence "0 < l" by simp
      then obtain l' where [simp]:"l = l' + 1" and "l' = l - 1" by simp
      show ?thesis
      proof(cases "l' < #:c⇩1")
        case True
        from ‹Rep_wf_prog wfp = (if (b) c⇩1 else c⇩2, procs)›
        obtain wfp' where [simp]:"Rep_wf_prog wfp' = (c⇩1, procs)" 
          by(erule wfp_CondTrue)
        from IH1[OF True this] obtain as as' 
          where path1:"wfp' ⊢ (Main, Label l') -as→* (Main, Exit)"
          and intra1:"∀a∈set as. intra_kind (kind a)"
          and path2:"wfp' ⊢ (Main, Entry) -as'→* (Main, Label l')"
          and intra2:"∀a∈set as'. intra_kind (kind a)" by blast
        from path1 intra1
        have "wfp ⊢ (Main, Label l' ⊕ 1) -as ⊕s 1→* (Main, Exit ⊕ 1)"
          by -(rule path_Main_CondTrue,auto)
        moreover
        from path2 obtain ax' asx' where [simp]:"as' = ax'#asx'"
          and "sourcenode ax' = (Main,Entry)" and "valid_edge wfp' ax'"
          and "wfp' ⊢ targetnode ax' -asx'→* (Main, Label l')"
          by -(erule ProcCFG.path.cases,fastforce+)
        with wf have "targetnode ax' = (Main,Label 0)"
          by(fastforce elim:PCFG.cases dest:Proc_CFG_EntryD Proc_CFG_Call_Labels 
                      simp:valid_edge_def)
        with ‹wfp' ⊢ targetnode ax' -asx'→* (Main, Label l')› intra2
        have "wfp ⊢ (Main,Entry) -((Main,Entry),(λs. True)⇩√,(Main,Label 0))#
          ((Main,Label 0),(λcf. state_check cf b (Some true))⇩√,(Main,Label 0 ⊕ 1))#
          (asx' ⊕s 1)→* (Main,Label l' ⊕ 1)"
          apply - apply(rule ProcCFG.path.intros)+ apply(rule path_Main_CondTrue) 
          by(auto intro:Main Proc_CFG_Entry Proc_CFG_CondTrue simp:valid_edge_def)
        ultimately show ?thesis using intra1 intra2
          by(fastforce simp:label_incrs_def intra_kind_def)
      next
        case False
        hence "#:c⇩1 ≤ l'" by simp
        then obtain l'' where [simp]:"l' = l'' + #:c⇩1" and "l'' = l' - #:c⇩1" by simp
        from  ‹l < #:(if (b) c⇩1 else c⇩2)› have "l'' < #:c⇩2" by simp
        from ‹Rep_wf_prog wfp = (if (b) c⇩1 else c⇩2, procs)›
        obtain wfp'' where [simp]:"Rep_wf_prog wfp'' = (c⇩2, procs)" 
          by(erule wfp_CondFalse)
        from IH2[OF ‹l'' < #:c⇩2› this] obtain as as' 
          where path1:"wfp'' ⊢ (Main, Label l'') -as→* (Main, Exit)"
          and intra1:"∀a∈set as. intra_kind (kind a)"
          and path2:"wfp'' ⊢ (Main, Entry) -as'→* (Main, Label l'')"
          and intra2:"∀a∈set as'. intra_kind (kind a)" by blast
        from path1 intra1
        have "wfp ⊢ (Main, Label l'' ⊕ (#:c⇩1 + 1)) -as ⊕s (#:c⇩1 + 1)→* 
          (Main, Exit ⊕ (#:c⇩1 + 1))"
          by -(rule path_Main_CondFalse,auto simp:add.assoc)
        moreover
        from path2 obtain ax' asx' where [simp]:"as' = ax'#asx'"
          and "sourcenode ax' = (Main,Entry)" and "valid_edge wfp'' ax'"
          and "wfp'' ⊢ targetnode ax' -asx'→* (Main, Label l'')"
          by -(erule ProcCFG.path.cases,fastforce+)
        with wf have "targetnode ax' = (Main,Label 0)"
          by(fastforce elim:PCFG.cases dest:Proc_CFG_EntryD Proc_CFG_Call_Labels 
                      simp:valid_edge_def)
        with ‹wfp'' ⊢ targetnode ax' -asx'→* (Main, Label l'')› intra2
        have "wfp ⊢ (Main,Entry) -((Main,Entry),(λs. True)⇩√,(Main,Label 0))#
          ((Main,Label 0),(λcf. state_check cf b (Some false))⇩√,
          (Main,Label (#:c⇩1 + 1)))#(asx' ⊕s (#:c⇩1 + 1))→* 
          (Main,Label l'' ⊕ (#:c⇩1 + 1))"
          apply - apply(rule ProcCFG.path.intros)+ apply(rule path_Main_CondFalse)
          by(auto intro:Main Proc_CFG_Entry Proc_CFG_CondFalse simp:valid_edge_def)
        ultimately show ?thesis using intra1 intra2
          by(fastforce simp:label_incrs_def intra_kind_def add.assoc)
      qed
    qed
  next
    case (While b c')
    note IH = ‹⋀l wfp. ⟦l < #:c'; Rep_wf_prog wfp = (c', procs)⟧ ⟹
      ∃as as'. wfp ⊢ (Main, Label l) -as→* (Main, Exit) ∧
      (∀a∈set as. intra_kind (kind a)) ∧
      wfp ⊢ (Main, Entry) -as'→* (Main, Label l) ∧ (∀a∈set as'. intra_kind (kind a))›
    note [simp] = ‹Rep_wf_prog wfp = (while (b) c', procs)›
    show ?case
    proof(cases "l = 0")
      case True
      hence "wfp ⊢ (Main,Label l) - 
        ((Main,Label 0),(λcf. state_check cf b (Some false))⇩√,(Main,Label 1))#
        [((Main,Label 1),⇑id,(Main,Exit))]→* (Main,Exit)"
        by(fastforce intro:ProcCFG.path.intros Main Proc_CFG_WhileFalseSkip 
          Proc_CFG_WhileFalse simp:valid_edge_def)
      moreover
      have "while (b) c' ⊢ Entry -IEdge (λs. True)⇩√→⇩p Label 0" by(rule Proc_CFG_Entry)
      with ‹l = 0› have "wfp ⊢ (Main,Entry) 
        -[((Main,Entry),(λs. True)⇩√,(Main,Label 0))]→* (Main,Label l)"
        by(fastforce intro:ProcCFG.path.intros Main 
                     simp:ProcCFG.valid_node_def valid_edge_def)
      ultimately show ?thesis by(fastforce simp:intra_kind_def)
    next
      case False
      hence "1 ≤ l" by simp
      thus ?thesis
      proof(cases "l < 2")
        case True
        with ‹1 ≤ l› have [simp]:"l = 1" by simp
        have "wfp ⊢ (Main,Label l) -[((Main,Label 1),⇑id,(Main,Exit))]→* (Main,Exit)"
          by(fastforce intro:ProcCFG.path.intros Main Proc_CFG_WhileFalseSkip 
                      simp:valid_edge_def)
        moreover
        have "while (b) c' ⊢ Label 0 -IEdge (λcf. state_check cf b (Some false))⇩√→⇩p 
          Label 1" by(rule Proc_CFG_WhileFalse)
        hence "wfp ⊢ (Main,Entry) -((Main,Entry),(λs. True)⇩√,(Main,Label 0))#
          [((Main,Label 0),(λcf. state_check cf b (Some false))⇩√,(Main,Label 1))]→*
          (Main,Label l)"
          by(fastforce intro:ProcCFG.path.intros Main Proc_CFG_Entry 
                       simp:ProcCFG.valid_node_def valid_edge_def)
        ultimately show ?thesis by(fastforce simp:intra_kind_def)
      next
        case False
        with ‹1 ≤ l› have "2 ≤ l" by simp
        then obtain l' where [simp]:"l = l' + 2" and "l' = l - 2" 
          by(simp del:add_2_eq_Suc')
        from ‹l < #:while (b) c'› have "l' < #:c'" by simp
        from ‹Rep_wf_prog wfp = (while (b) c', procs)›
        obtain wfp' where [simp]:"Rep_wf_prog wfp' = (c', procs)" 
          by(erule wfp_WhileBody)
        from IH[OF ‹l' < #:c'› this] obtain as as' 
          where path1:"wfp' ⊢ (Main, Label l') -as→* (Main, Exit)"
          and intra1:"∀a∈set as. intra_kind (kind a)"
          and path2:"wfp' ⊢ (Main, Entry) -as'→* (Main, Label l')"
          and intra2:"∀a∈set as'. intra_kind (kind a)" by blast
        from path1 have "as ≠ []" by(fastforce elim:ProcCFG.path.cases)
        with path1 obtain ax asx where [simp]:"as = asx@[ax]"
          and "wfp' ⊢ (Main, Label l') -asx→* sourcenode ax"
          and "valid_edge wfp' ax" and "targetnode ax = (Main, Exit)"
          by -(erule ProcCFG.path_split_snoc,fastforce+)
        with wf obtain lx etx where "sourcenode ax = (Main,Label lx)"
          and "intra_kind (kind ax)"
          apply(auto elim!:PCFG.cases dest:Proc_CFG_Call_Labels simp:valid_edge_def)
          by(case_tac n)(auto dest:Proc_CFG_IEdge_intra_kind)
        with ‹wfp' ⊢ (Main, Label l') -asx→* sourcenode ax› intra1
        have "wfp ⊢ (Main, Label l' ⊕ 2) -asx ⊕s 2→* (Main,Label lx ⊕ 2)"
          by -(rule path_Main_WhileBody,auto)
        from ‹valid_edge wfp' ax› ‹sourcenode ax = (Main,Label lx)›
          ‹targetnode ax = (Main, Exit)› ‹intra_kind (kind ax)› wf
        have "while (b) c',procs ⊢ (Main,Label lx ⊕ 2) -kind ax→ 
          (Main,Label 0)"
          by(fastforce intro!:Main Proc_CFG_WhileBodyExit elim!:PCFG.cases 
                        dest:Proc_CFG_Call_Labels simp:valid_edge_def)
        hence "wfp ⊢ (Main,Label lx ⊕ 2) 
          -((Main,Label lx ⊕ 2),kind ax,(Main,Label 0))#
          ((Main,Label 0),(λcf. state_check cf b (Some false))⇩√,(Main,Label 1))#
          [((Main,Label 1),⇑id,(Main,Exit))]→* (Main,Exit)"
          by(fastforce intro:ProcCFG.path.intros Main Proc_CFG_WhileFalse 
            Proc_CFG_WhileFalseSkip simp:valid_edge_def)
        with ‹wfp ⊢ (Main, Label l' ⊕ 2) -asx ⊕s 2→* (Main,Label lx ⊕ 2)›
        have "wfp ⊢ (Main, Label l) -(asx ⊕s 2)@
          (((Main,Label lx ⊕ 2),kind ax,(Main,Label 0))#
          ((Main,Label 0),(λcf. state_check cf b (Some false))⇩√,(Main,Label 1))#
          [((Main,Label 1),⇑id,(Main,Exit))])→* (Main,Exit)"
          by(fastforce intro:ProcCFG.path_Append)
        moreover
        from path2 have "as' ≠ []" by(fastforce elim:ProcCFG.path.cases)
        with path2 obtain ax' asx' where [simp]:"as' = ax'#asx'"
          and "wfp' ⊢ targetnode ax' -asx'→* (Main,Label l')"
          and "valid_edge wfp' ax'" and "sourcenode ax' = (Main, Entry)"
          by -(erule ProcCFG.path_split_Cons,fastforce+)
        with wf have "targetnode ax' = (Main,Label 0)" and "intra_kind (kind ax')"
          by(fastforce elim!:PCFG.cases dest:Proc_CFG_Call_Labels 
            Proc_CFG_EntryD simp:intra_kind_def valid_edge_def)+
        with ‹wfp' ⊢ targetnode ax' -asx'→* (Main,Label l')› intra2
        have "wfp ⊢ (Main, Label 0 ⊕ 2) -asx' ⊕s 2→* (Main,Label l' ⊕ 2)"
          by -(rule path_Main_WhileBody,auto simp del:add_2_eq_Suc')
        hence "wfp ⊢ (Main,Entry) -((Main,Entry),(λs. True)⇩√,(Main,Label 0))#
          ((Main,Label 0),(λcf. state_check cf b (Some true))⇩√,(Main,Label 2))#
          (asx' ⊕s 2)→* (Main,Label l)"
          by(fastforce intro:ProcCFG.path.intros Main Proc_CFG_WhileTrue 
            Proc_CFG_Entry simp:valid_edge_def)
        ultimately show ?thesis using ‹intra_kind (kind ax)› intra1 intra2
          by(fastforce simp:label_incrs_def intra_kind_def)
      qed
    qed
  next
    case (Call p es rets)
    note Rep [simp] = ‹Rep_wf_prog wfp = (Call p es rets, procs)›
    have cC:"containsCall procs (Call p es rets) [] p" by simp
    show ?case
    proof(cases "l = 0")
      case True
      have "wfp ⊢ (Main,Label 0) -((Main,Label 0),(λs. False)⇩√,(Main,Label 1))#
        [((Main,Label 1),⇑id,(Main,Exit))]→* (Main,Exit)"
        by(fastforce intro:ProcCFG.path.intros Main Proc_CFG_CallSkip MainCallReturn
          Proc_CFG_Call simp:valid_edge_def)
      moreover
      have "Call p es rets,procs ⊢ (Main,Entry) -(λs. True)⇩√→ (Main,Label 0)"
        by(fastforce intro:Main Proc_CFG_Entry)
      hence "wfp ⊢ (Main,Entry) -[((Main,Entry),(λs. True)⇩√,(Main,Label 0))]→*
        (Main,Label 0)"
        by(fastforce intro:ProcCFG.path.intros 
          simp:ProcCFG.valid_node_def valid_edge_def)
      ultimately show ?thesis using ‹l = 0› by(fastforce simp:intra_kind_def)
    next
      case False
      with ‹l < #:Call p es rets› have "l = 1" by simp
      have "wfp ⊢ (Main,Label 1) -[((Main,Label 1),⇑id,(Main,Exit))]→* (Main,Exit)"
        by(fastforce intro:ProcCFG.path.intros Main Proc_CFG_CallSkip
                    simp:valid_edge_def)
      moreover
      have "Call p es rets,procs ⊢ (Main,Label 0) -(λs. False)⇩√→ (Main,Label 1)"
        by(fastforce intro:MainCallReturn Proc_CFG_Call)
      hence "wfp ⊢ (Main,Entry) -((Main,Entry),(λs. True)⇩√,(Main,Label 0))#
        [((Main,Label 0),(λs. False)⇩√,(Main,Label 1))]→* (Main,Label 1)"
        by(fastforce intro:ProcCFG.path.intros Main Proc_CFG_Entry 
                    simp:ProcCFG.valid_node_def valid_edge_def)
      ultimately show ?thesis using ‹l = 1› by(fastforce simp:intra_kind_def)
    qed
  qed
qed



subsection ‹Lifting from edges in procedure Main to arbitrary procedures›

lemma lift_edge_Main_Main:
  "⟦c,procs ⊢ (Main, n) -et→ (Main, n'); (p,ins,outs,c) ∈ set procs;
  containsCall procs prog ps p; well_formed procs⟧ 
  ⟹ prog,procs ⊢ (p, n) -et→ (p, n')"
proof(induct "(Main,n)" et "(Main,n')" rule:PCFG.induct)
  case Main thus ?case by(fastforce intro:Proc)
next
  case MainCallReturn thus ?case by(fastforce intro:ProcCallReturn)
qed auto

lemma lift_edge_Main_Proc:
  "⟦c,procs ⊢ (Main, n) -et→ (q, n'); q ≠ Main; (p,ins,outs,c) ∈ set procs;
  containsCall procs prog ps p; well_formed procs⟧ 
  ⟹ ∃et'. prog,procs ⊢ (p, n) -et'→ (q, n')"
proof(induct "(Main,n)" et "(q,n')" rule:PCFG.induct)
  case (MainCall l esx retsx n'x insx outsx cx)
  from ‹c ⊢ Label l -CEdge (q, esx, retsx)→⇩p n'x› 
  obtain l' where [simp]:"n'x = Label l'" by(fastforce dest:Proc_CFG_Call_Labels)
  with MainCall have "prog,procs ⊢ (p, n) 
    -(λs. True):(p,n'x)↪⇘q⇙map (λe cf. interpret e cf) esx→ (q, n')"
    by(fastforce intro:ProcCall)
  thus ?case by fastforce
qed auto

lemma lift_edge_Proc_Main:
  "⟦c,procs ⊢ (q, n) -et→ (Main, n'); q ≠ Main; (p,ins,outs,c) ∈ set procs;
  containsCall procs prog ps p; well_formed procs⟧ 
  ⟹ ∃et'. prog,procs ⊢ (q, n) -et'→ (p, n')"
proof(induct "(q,n)" et "(Main,n')" rule:PCFG.induct)
  case (MainReturn l esx retsx l' insx outsx cx)
  note [simp] = ‹Exit = n›[THEN sym] ‹Label l' = n'›[THEN sym]
  from MainReturn have "prog,procs ⊢ (q,Exit) -(λcf. snd cf = (p,Label l'))↩⇘q⇙
    (λcf cf'. cf'(retsx [:=] map cf outsx))→ (p,Label l')"
    by(fastforce intro!:ProcReturn)
  thus ?case by fastforce
qed auto


fun lift_edge :: "edge ⇒ pname ⇒ edge"
where "lift_edge a p = ((p,snd(sourcenode a)),kind a,(p,snd(targetnode a)))"

fun lift_path :: "edge list ⇒ pname ⇒ edge list"
  where "lift_path as p = map (λa. lift_edge a p) as"


lemma lift_path_Proc: 
  fixes wfp
  assumes "Rep_wf_prog wfp' = (c,procs)" and "Rep_wf_prog wfp = (prog,procs)"
  and "(p,ins,outs,c) ∈ set procs" and "containsCall procs prog ps p"
  shows "⟦wfp' ⊢ (Main,n) -as→* (Main,n'); ∀a ∈ set as. intra_kind (kind a)⟧
  ⟹ wfp ⊢ (p,n) -lift_path as p→* (p,n')"
proof(induct "(Main,n)" as "(Main,n')" arbitrary:n rule:ProcCFG.path.induct)
  case empty_path
  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')›
    assms wf
  have "CFG.valid_node sourcenode targetnode (valid_edge wfp) (p,n')"
    apply(auto simp:ProcCFG.valid_node_def valid_edge_def)
     apply(case_tac "ab = Main")
      apply(fastforce dest:lift_edge_Main_Main)
     apply(fastforce dest!:lift_edge_Main_Proc)
    apply(case_tac "a = Main")
     apply(fastforce dest:lift_edge_Main_Main)
    by(fastforce dest!:lift_edge_Proc_Main)
  thus ?case by(fastforce dest:ProcCFG.empty_path)
next
  case (Cons_path m'' as a n)
  note IH = ‹⋀n. ⟦m'' = (Main, n); ∀a∈set as. intra_kind (kind a)⟧
    ⟹ wfp ⊢ (p, n) -lift_path as p→* (p, n')›
  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› ‹intra_kind (kind a)› ‹sourcenode a = (Main, n)› 
    ‹targetnode a = m''› ‹Rep_wf_prog wfp' = (c,procs)›
  obtain n'' where "m'' = (Main, n'')"
    by(fastforce elim:PCFG.cases simp:valid_edge_def intra_kind_def)
  with ‹valid_edge wfp' a› ‹Rep_wf_prog wfp' = (c,procs)›
    ‹sourcenode a = (Main, n)› ‹targetnode a = m''›
    ‹(p,ins,outs,c) ∈ set procs› ‹containsCall procs prog ps p› 
    ‹Rep_wf_prog wfp = (prog,procs)› wf
  have "prog,procs ⊢ (p, n) -kind a→ (p, n'')"
    by(auto intro:lift_edge_Main_Main simp:valid_edge_def)  
  from IH[OF ‹m'' = (Main, n'')› ‹∀a∈set as. intra_kind (kind a)›]
  have "wfp ⊢ (p, n'') -lift_path as p→* (p, n')" .
  with ‹prog,procs ⊢ (p, n) -kind a→ (p, n'')› ‹Rep_wf_prog wfp = (prog,procs)›
    ‹sourcenode a = (Main, n)› ‹targetnode a = m''› ‹m'' = (Main, n'')›
  show ?case by simp (rule ProcCFG.Cons_path,auto simp:valid_edge_def)
qed


subsection ‹Existence of paths from Entry and to Exit›

lemma Label_Proc_CFG_Entry_Exit_path_Proc:
  fixes wfp
  assumes "Rep_wf_prog wfp = (prog,procs)" and "l < #:c"
  and "(p,ins,outs,c) ∈ set procs" and "containsCall procs prog ps p"
  obtains as as' where "wfp ⊢ (p,Label l) -as→* (p,Exit)"
  and "∀a ∈ set as. intra_kind (kind a)"
  and "wfp ⊢ (p,Entry) -as'→* (p,Label l)"
  and "∀a ∈ set as'. intra_kind (kind a)"
proof(atomize_elim)
  from ‹Rep_wf_prog wfp = (prog,procs)› ‹(p,ins,outs,c) ∈ set procs›
    ‹containsCall procs prog ps p›
  obtain wfp' where "Rep_wf_prog wfp' = (c,procs)" by(erule wfp_Call)
  from this ‹l < #:c› obtain as as' where "wfp' ⊢ (Main,Label l) -as→* (Main,Exit)"
    and "∀a ∈ set as. intra_kind (kind a)"
    and "wfp' ⊢ (Main,Entry) -as'→* (Main,Label l)"
    and "∀a ∈ set as'. intra_kind (kind a)" 
    by(erule Label_Proc_CFG_Entry_Exit_path_Main)
  from ‹Rep_wf_prog wfp' = (c,procs)› ‹Rep_wf_prog wfp = (prog,procs)›
    ‹(p,ins,outs,c) ∈ set procs› ‹containsCall procs prog ps p›
    ‹wfp' ⊢ (Main,Label l) -as→* (Main,Exit)› ‹∀a ∈ set as. intra_kind (kind a)›
  have "wfp ⊢ (p,Label l) -lift_path as p→* (p,Exit)"
    by(fastforce intro:lift_path_Proc)
  moreover
  from ‹Rep_wf_prog wfp' = (c,procs)› ‹Rep_wf_prog wfp = (prog,procs)›
    ‹(p,ins,outs,c) ∈ set procs› ‹containsCall procs prog ps p›
    ‹wfp' ⊢ (Main,Entry) -as'→* (Main,Label l)› ‹∀a ∈ set as'. intra_kind (kind a)›
  have "wfp ⊢ (p,Entry) -lift_path as' p→* (p,Label l)"
    by(fastforce intro:lift_path_Proc)
  moreover
  from ‹∀a ∈ set as. intra_kind (kind a)› ‹∀a ∈ set as'. intra_kind (kind a)›
  have "∀a ∈ set (lift_path as p). intra_kind (kind a)"
    and "∀a ∈ set (lift_path as' p). intra_kind (kind a)" by auto
  ultimately
  show "∃as as'. wfp ⊢ (p, Label l) -as→* (p, Exit) ∧
    (∀a∈set as. intra_kind (kind a)) ∧ wfp ⊢ (p, Entry) -as'→* (p, Label l) ∧
    (∀a∈set as'. intra_kind (kind a))" by fastforce
qed


lemma Entry_to_Entry_and_Exit_to_Exit: 
  fixes wfp
  assumes "Rep_wf_prog wfp = (prog,procs)"
  and "containsCall procs prog ps p" and "(p,ins,outs,c) ∈ set procs"
  obtains as as' where "CFG.valid_path' sourcenode targetnode kind
      (valid_edge wfp) (get_return_edges wfp) (Main,Entry) as (p,Entry)"
  and "CFG.valid_path' sourcenode targetnode kind
      (valid_edge wfp) (get_return_edges wfp) (p,Exit) as' (Main,Exit)"
proof(atomize_elim)
  from ‹containsCall procs prog ps p› ‹(p,ins,outs,c) ∈ set procs›
  show "∃as as'. CFG.valid_path' sourcenode targetnode kind (valid_edge wfp)
    (get_return_edges wfp) (Main, Entry) as (p, Entry) ∧
    CFG.valid_path' sourcenode targetnode kind (valid_edge wfp)
    (get_return_edges wfp) (p, Exit) as' (Main, Exit)"
  proof(induct ps arbitrary:p ins outs c rule:rev_induct)
    case Nil
    from ‹containsCall procs prog [] p›
    obtain lx es rets lx' where "prog ⊢ Label lx -CEdge (p,es,rets)→⇩p Label lx'"
      by(erule containsCall_empty_Proc_CFG_Call_edge)
    with ‹(p, ins, outs, c) ∈ set procs›
    have "prog,procs ⊢ (Main,Label lx) -(λs. True):(Main,Label lx')↪⇘p⇙
      map (λe cf. interpret e cf) es→  (p,Entry)" 
      and "prog,procs ⊢ (p,Exit) -(λcf. snd cf = (Main,Label lx'))↩⇘p⇙
      (λcf cf'. cf'(rets [:=] map cf outs))→ (Main,Label lx')"
      by -(rule MainCall,assumption+,rule MainReturn)
    with ‹Rep_wf_prog wfp = (prog,procs)›
    have "wfp ⊢ (Main,Label lx) -[((Main,Label lx),
      (λs. True):(Main,Label lx')↪⇘p⇙map (λe cf. interpret e cf) es,(p,Entry))]→* 
      (p,Entry)"
      and "wfp ⊢ (p,Exit) -[((p,Exit),(λcf. snd cf = (Main,Label lx'))↩⇘p⇙
      (λcf cf'. cf'(rets [:=] map cf outs)),(Main,Label lx'))]→* (Main,Label lx')"
      by(fastforce intro:ProcCFG.path.intros 
        simp:ProcCFG.valid_node_def valid_edge_def)+
    moreover
    from ‹prog ⊢ Label lx -CEdge (p,es,rets)→⇩p Label lx'›
    have "lx < #:prog" and "lx' < #:prog"
      by(auto intro:Proc_CFG_sourcelabel_less_num_nodes 
                    Proc_CFG_targetlabel_less_num_nodes)
    from ‹Rep_wf_prog wfp = (prog,procs)› ‹lx < #:prog› obtain as 
      where "wfp ⊢ (Main,Entry) -as→* (Main,Label lx)"
      and "∀a ∈ set as. intra_kind (kind a)"
      by -(erule Label_Proc_CFG_Entry_Exit_path_Main)
    moreover
    from ‹Rep_wf_prog wfp = (prog,procs)› ‹lx' < #:prog› obtain as' 
      where "wfp ⊢ (Main,Label lx') -as'→* (Main,Exit)"
      and "∀a ∈ set as'. intra_kind (kind a)"
      by -(erule Label_Proc_CFG_Entry_Exit_path_Main)
    moreover
    from ‹∀a ∈ set as. intra_kind (kind a)› 
    have "CFG.valid_path kind (get_return_edges wfp) 
      (as@[((Main,Label lx),(λs. True):(Main,Label lx')↪⇘p⇙
      map (λe cf. interpret e cf) es,(p,Entry))])"
      by(fastforce intro:ProcCFG.same_level_path_valid_path_Append 
        ProcCFG.intras_same_level_path simp:ProcCFG.valid_path_def)
    moreover
    from ‹∀a ∈ set as'. intra_kind (kind a)› 
    have "CFG.valid_path kind (get_return_edges wfp) 
      ([((p,Exit),(λcf. snd cf = (Main,Label lx'))↩⇘p⇙
      (λcf cf'. cf'(rets [:=] map cf outs)),(Main,Label lx'))]@as')"
      by(fastforce intro:ProcCFG.valid_path_same_level_path_Append 
        ProcCFG.intras_same_level_path simp:ProcCFG.valid_path_def)
    ultimately show ?case by(fastforce intro:ProcCFG.path_Append simp:ProcCFG.vp_def)
  next
    case (snoc p' ps')
    note IH = ‹⋀p ins outs c. 
      ⟦containsCall procs prog ps' p; (p,ins,outs,c) ∈ set procs⟧
      ⟹ ∃as as'. CFG.valid_path' sourcenode targetnode kind (valid_edge wfp)
      (get_return_edges wfp) (Main, Entry) as (p, Entry) ∧
      CFG.valid_path' sourcenode targetnode kind (valid_edge wfp)
      (get_return_edges wfp) (p, Exit) as' (Main, Exit)›
    from ‹containsCall procs prog (ps' @ [p']) p›
    obtain ins' outs' c' where "(p',ins',outs',c') ∈ set procs"
      and "containsCall procs c' [] p" 
      and "containsCall procs prog ps' p'" by(auto elim:containsCallE)
    from IH[OF ‹containsCall procs prog ps' p'› ‹(p',ins',outs',c') ∈ set procs›] 
    obtain as as' where pathE:"CFG.valid_path' sourcenode targetnode kind 
      (valid_edge wfp) (get_return_edges wfp) (Main, Entry) as (p', Entry)"
      and pathX:"CFG.valid_path' sourcenode targetnode kind (valid_edge wfp)
      (get_return_edges wfp) (p', Exit) as' (Main, Exit)" by blast
    from ‹containsCall procs c' [] p›
    obtain lx es rets lx' where edge:"c' ⊢ Label lx -CEdge (p,es,rets)→⇩p Label lx'"
      by(erule containsCall_empty_Proc_CFG_Call_edge)
    hence "lx < #:c'" and "lx' < #:c'"
      by(auto intro:Proc_CFG_sourcelabel_less_num_nodes 
                    Proc_CFG_targetlabel_less_num_nodes)
    from ‹lx < #:c'› ‹Rep_wf_prog wfp = (prog,procs)› ‹(p',ins',outs',c') ∈ set procs›
      ‹containsCall procs prog ps' p'› obtain asx 
      where "wfp ⊢ (p',Entry) -asx→* (p',Label lx)"
      and "∀a ∈ set asx. intra_kind (kind a)"
      by(fastforce elim:Label_Proc_CFG_Entry_Exit_path_Proc)
    with pathE have pathE2:"CFG.valid_path' sourcenode targetnode kind 
      (valid_edge wfp) (get_return_edges wfp) (Main, Entry) (as@asx) (p', Label lx)"
      by(fastforce intro:ProcCFG.path_Append ProcCFG.valid_path_same_level_path_Append
        ProcCFG.intras_same_level_path simp:ProcCFG.vp_def)
    from ‹lx' < #:c'› ‹Rep_wf_prog wfp = (prog,procs)›
      ‹(p',ins',outs',c') ∈ set procs› ‹containsCall procs prog ps' p'› 
    obtain asx' where "wfp ⊢ (p',Label lx') -asx'→* (p',Exit)"
      and "∀a ∈ set asx'. intra_kind (kind a)"
      by(fastforce elim:Label_Proc_CFG_Entry_Exit_path_Proc)
    with pathX have pathX2:"CFG.valid_path' sourcenode targetnode kind 
      (valid_edge wfp) (get_return_edges wfp) (p', Label lx') (asx'@as') (Main, Exit)"
      by(fastforce intro:ProcCFG.path_Append ProcCFG.same_level_path_valid_path_Append
        ProcCFG.intras_same_level_path simp:ProcCFG.vp_def)
    from edge ‹(p,ins,outs,c) ∈ set procs› ‹(p',ins',outs',c') ∈ set procs›
      ‹containsCall procs prog ps' p'›
    have "prog,procs ⊢ (p',Label lx) -(λs. True):(p',Label lx')↪⇘p⇙
      map (λe cf. interpret e cf) es→ (p,Entry)"
      and "prog,procs ⊢ (p,Exit) -(λcf. snd cf = (p',Label lx'))↩⇘p⇙
      (λcf cf'. cf'(rets [:=] map cf outs))→ (p',Label lx')"
      by(fastforce intro:ProcCall ProcReturn)+
    with ‹Rep_wf_prog wfp = (prog,procs)›
    have path:"wfp ⊢ (p',Label lx) -[((p',Label lx),(λs. True):(p',Label lx')↪⇘p⇙
      map (λe cf. interpret e cf) es,(p,Entry))]→* (p,Entry)"
      and path':"wfp ⊢ (p,Exit) -[((p,Exit),(λcf. snd cf = (p',Label lx'))↩⇘p⇙
      (λcf cf'. cf'(rets [:=] map cf outs)),(p',Label lx'))]→* 
      (p',Label lx')"
      by(fastforce intro:ProcCFG.path.intros 
                  simp:ProcCFG.valid_node_def valid_edge_def)+
    from path pathE2 have "CFG.valid_path' sourcenode targetnode kind (valid_edge wfp)
      (get_return_edges wfp) (Main, Entry) ((as@asx)@[((p',Label lx),
      (λs. True):(p',Label lx')↪⇘p⇙map (λe cf. interpret e cf) es,(p,Entry))])
      (p,Entry)"
      apply(unfold ProcCFG.vp_def) apply(rule conjI)
       apply(fastforce intro:ProcCFG.path_Append)
      by(unfold ProcCFG.valid_path_def,fastforce intro:ProcCFG.vpa_snoc_Call)
    moreover
    from path' pathX2 have "CFG.valid_path' sourcenode targetnode kind 
      (valid_edge wfp) (get_return_edges wfp) (p,Exit)
      ([((p,Exit),(λcf. snd cf = (p',Label lx'))↩⇘p⇙
      (λcf cf'. cf'(rets [:=] map cf outs)),(p',Label lx'))]@(asx'@as')) (Main, Exit)"
      apply(unfold ProcCFG.vp_def) apply(rule conjI)
       apply(fastforce intro:ProcCFG.path_Append)
      by(simp add:ProcCFG.valid_path_def ProcCFG.valid_path_def)
    ultimately show ?case by blast
  qed
qed


lemma edge_valid_paths:
  fixes wfp
  assumes "prog,procs ⊢ sourcenode a -kind a→ targetnode a"
  and disj:"(p,n) = sourcenode a ∨ (p,n) = targetnode a" 
  and [simp]:"Rep_wf_prog wfp = (prog,procs)"
  shows "∃as as'. CFG.valid_path' sourcenode targetnode kind (valid_edge wfp)
                (get_return_edges wfp) (Main,Entry) as (p,n) ∧
              CFG.valid_path' sourcenode targetnode kind (valid_edge wfp)
                (get_return_edges wfp) (p,n) as' (Main,Exit)"
proof -
  from ‹Rep_wf_prog wfp = (prog,procs)› have wf:"well_formed procs"
    by(fastforce intro:wf_wf_prog)
  from ‹prog,procs ⊢ sourcenode a -kind a→ targetnode a›
  show ?thesis
  proof(induct "sourcenode a" "kind a" "targetnode a" rule:PCFG.induct)
    case (Main nx nx')
    from ‹(Main, nx) = sourcenode a›[THEN sym] ‹(Main, nx') = targetnode a›[THEN sym]
      disj have [simp]:"p = Main" by auto
    have "prog,procs ⊢ (Main, Entry) -(λs. False)⇩√→ (Main, Exit)"
      by(fastforce intro:PCFG.Main Proc_CFG_Entry_Exit)
    hence EXpath:"wfp ⊢ (Main,Entry) -[((Main,Entry),(λs. False)⇩√,(Main,Exit))]→*
        (Main,Exit)"
      by(fastforce intro:ProcCFG.path.intros
        simp:valid_edge_def ProcCFG.valid_node_def)
    show ?case
    proof(cases n)
      case (Label l)
      with ‹prog ⊢ nx -IEdge (kind a)→⇩p nx'› ‹(Main, nx) = sourcenode a›[THEN sym]
        ‹(Main, nx') = targetnode a›[THEN sym] disj
      have "l < #:prog" by(auto intro:Proc_CFG_sourcelabel_less_num_nodes
        Proc_CFG_targetlabel_less_num_nodes)
      with ‹Rep_wf_prog wfp = (prog,procs)› 
      obtain as as' where "wfp ⊢ (Main,Entry) -as→* (Main,Label l)"
        and "∀a ∈ set as. intra_kind (kind a)"
        and "wfp ⊢ (Main,Label l) -as'→* (Main,Exit)"
        and "∀a ∈ set as'. intra_kind (kind a)"
        by -(erule Label_Proc_CFG_Entry_Exit_path_Main)+
      with Label show ?thesis
        apply(rule_tac x="as" in exI) apply(rule_tac x="as'" in exI) apply simp
        by(fastforce intro:ProcCFG.intra_path_vp simp:ProcCFG.intra_path_def)
    next
      case Entry
      hence "wfp ⊢ (Main,Entry) -[]→* (Main,n)" by(fastforce intro:ProcCFG.empty_path)
      with EXpath show ?thesis by(fastforce simp:ProcCFG.vp_def ProcCFG.valid_path_def)
    next
      case Exit
      hence "wfp ⊢ (Main,n) -[]→* (Main,Exit)" by(fastforce intro:ProcCFG.empty_path)
      with Exit EXpath show ?thesis using Exit
        apply(rule_tac x="[((Main,Entry),(λs. False)⇩√,(Main,Exit))]" in exI) 
        apply simp
        by(fastforce intro:ProcCFG.intra_path_vp 
          simp:ProcCFG.intra_path_def intra_kind_def)
    qed
  next
    case (Proc px ins outs c nx nx' ps)
    from ‹(px, ins, outs, c) ∈ set procs› wf have [simp]:"px ≠ Main" by auto
    from disj ‹(px, nx) = sourcenode a›[THEN sym] ‹(px, nx') = targetnode a›[THEN sym]
    have [simp]:"p = px" by auto
    from ‹Rep_wf_prog wfp = (prog,procs)› 
      ‹containsCall procs prog ps px› ‹(px, ins, outs, c) ∈ set procs›
    obtain asx asx' where path:"CFG.valid_path' sourcenode targetnode kind
      (valid_edge wfp) (get_return_edges wfp) (Main,Entry) asx (px,Entry)"
      and path':"CFG.valid_path' sourcenode targetnode kind
      (valid_edge wfp) (get_return_edges wfp) (px,Exit) asx' (Main,Exit)"
      by -(erule Entry_to_Entry_and_Exit_to_Exit)+
    from ‹containsCall procs prog ps px› ‹(px, ins, outs, c) ∈ set procs›
    have "prog,procs ⊢ (px, Entry) -(λs. False)⇩√→ (px, Exit)"
      by(fastforce intro:PCFG.Proc Proc_CFG_Entry_Exit)
    hence EXpath:"wfp ⊢ (px,Entry) -[((px,Entry),(λs. False)⇩√,(px,Exit))]→* 
      (px,Exit)" by(fastforce intro:ProcCFG.path.intros 
        simp:valid_edge_def ProcCFG.valid_node_def)
    show ?case
    proof(cases n)
      case (Label l)
      with ‹c ⊢ nx -IEdge (kind a)→⇩p nx'› disj ‹(px, nx) = sourcenode a›[THEN sym]
        ‹(px, nx') = targetnode a›[THEN sym]
      have "l < #:c" by(auto intro:Proc_CFG_sourcelabel_less_num_nodes
        Proc_CFG_targetlabel_less_num_nodes)
      with ‹Rep_wf_prog wfp = (prog,procs)› ‹(px, ins, outs, c) ∈ set procs› 
        ‹containsCall procs prog ps px›
      obtain as as' where "wfp ⊢ (px,Entry) -as→* (px,Label l)"
        and "∀a ∈ set as. intra_kind (kind a)"
        and "wfp ⊢ (px,Label l) -as'→* (px,Exit)"
        and "∀a ∈ set as'. intra_kind (kind a)"
        by -(erule Label_Proc_CFG_Entry_Exit_path_Proc)+
      with path path' show ?thesis using Label
        apply(rule_tac x="asx@as" in exI) apply(rule_tac x="as'@asx'" in exI)
        by(auto intro:ProcCFG.path_Append ProcCFG.valid_path_same_level_path_Append
          ProcCFG.same_level_path_valid_path_Append ProcCFG.intras_same_level_path
          simp:ProcCFG.vp_def)
    next
      case Entry
      from EXpath path' have "CFG.valid_path' sourcenode targetnode kind 
        (valid_edge wfp) (get_return_edges wfp) (px,Entry) 
        ([((px,Entry),(λs. False)⇩√,(px,Exit))]@asx') (Main, Exit)"
        apply(unfold ProcCFG.vp_def) apply(erule conjE) apply(rule conjI)
        by(fastforce intro:ProcCFG.path_Append 
          ProcCFG.same_level_path_valid_path_Append ProcCFG.intras_same_level_path
          simp:intra_kind_def)+
      with path Entry show ?thesis by simp blast
    next
      case Exit
      with path EXpath path' show ?thesis
        apply(rule_tac x="asx@[((px,Entry),(λs. False)⇩√,(px,Exit))]" in exI)
        apply simp
        by(fastforce intro:ProcCFG.path_Append 
          ProcCFG.valid_path_same_level_path_Append ProcCFG.intras_same_level_path
          simp:ProcCFG.vp_def ProcCFG.intra_path_def intra_kind_def)
    qed
  next
    case (MainCall l px es rets nx' ins outs c)
    from disj show ?case
    proof
      assume "(p,n) = sourcenode a"
      with ‹(Main, Label l) = sourcenode a›[THEN sym] 
      have [simp]:"n = Label l" "p = Main" by simp_all
      with ‹prog ⊢ Label l -CEdge (px, es, rets)→⇩p nx'› have "l < #:prog"
        by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
      with ‹Rep_wf_prog wfp = (prog,procs)› 
      obtain as as' where "wfp ⊢ (Main,Entry) -as→* (Main,Label l)"
        and "∀a ∈ set as. intra_kind (kind a)"
        and "wfp ⊢ (Main,Label l) -as'→* (Main,Exit)"
        and "∀a ∈ set as'. intra_kind (kind a)"
        by -(erule Label_Proc_CFG_Entry_Exit_path_Main)+
      thus ?thesis 
        by(fastforce intro:ProcCFG.intra_path_vp simp:ProcCFG.intra_path_def)
    next
      assume "(p,n) = targetnode a"
      with ‹(px, Entry) = targetnode a›[THEN sym] 
      have [simp]:"n = Entry" "p = px" by simp_all
      from ‹prog ⊢ Label l -CEdge (px, es, rets)→⇩p nx'›
      have "containsCall procs prog [] px" 
        by(rule Proc_CFG_Call_containsCall)
      with ‹Rep_wf_prog wfp = (prog,procs)› ‹(px, ins, outs, c) ∈ set procs›
      obtain as' where Xpath:"CFG.valid_path' sourcenode targetnode kind
        (valid_edge wfp) (get_return_edges wfp) (px,Exit) as' (Main,Exit)"
        by -(erule Entry_to_Entry_and_Exit_to_Exit)      
      from ‹containsCall procs prog [] px› ‹(px, ins, outs, c) ∈ set procs›
      have "prog,procs ⊢ (px, Entry) -(λs. False)⇩√→ (px, Exit)"
        by(fastforce intro:PCFG.Proc Proc_CFG_Entry_Exit)
      hence "wfp ⊢ (px,Entry) -[((px,Entry),(λs. False)⇩√,(px,Exit))]→* (px,Exit)"
        by(fastforce intro:ProcCFG.path.intros 
          simp:valid_edge_def ProcCFG.valid_node_def)
      with Xpath have "CFG.valid_path' sourcenode targetnode kind
        (valid_edge wfp) (get_return_edges wfp) (px,Entry) 
        ([((px,Entry),(λs. False)⇩√,(px,Exit))]@as') (Main,Exit)"
        apply(unfold ProcCFG.vp_def) apply(erule conjE) apply(rule conjI)
        by(fastforce intro:ProcCFG.path_Append 
          ProcCFG.same_level_path_valid_path_Append ProcCFG.intras_same_level_path
          simp:intra_kind_def)+
      with ‹containsCall procs prog [] px› ‹Rep_wf_prog wfp = (prog,procs)›
        ‹(px, ins, outs, c) ∈ set procs›
      show ?thesis by(fastforce elim:Entry_to_Entry_and_Exit_to_Exit)
    qed
  next
    case (ProcCall px ins outs c l p' es' rets' l' ins' outs' c' ps)
    from disj show ?case
    proof
      assume "(p,n) = sourcenode a"
      with ‹(px, Label l) = sourcenode a›[THEN sym] 
      have [simp]:"n = Label l" "p = px" by simp_all
      with ‹c ⊢ Label l -CEdge (p', es', rets')→⇩p Label l'› have "l < #:c"
        by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
      from ‹Rep_wf_prog wfp = (prog,procs)› ‹l < #:c› 
        ‹containsCall procs prog ps px› ‹(px, ins, outs, c) ∈ set procs›
      obtain as as' where "wfp ⊢ (px,Label l) -as→* (px,Exit)"
        and "∀a ∈ set as. intra_kind (kind a)"
        and "wfp ⊢ (px,Entry) -as'→* (px,Label l)"
        and "∀a ∈ set as'. intra_kind (kind a)"
        by -(erule Label_Proc_CFG_Entry_Exit_path_Proc)+
      moreover
      from ‹Rep_wf_prog wfp = (prog,procs)› ‹containsCall procs prog ps px›
        ‹(px, ins, outs, c) ∈ set procs› obtain asx asx' 
        where" CFG.valid_path' sourcenode targetnode kind
        (valid_edge wfp) (get_return_edges wfp) (Main,Entry) asx (px,Entry)"
        and "CFG.valid_path' sourcenode targetnode kind
        (valid_edge wfp) (get_return_edges wfp) (px,Exit) asx' (Main,Exit)"
        by -(erule Entry_to_Entry_and_Exit_to_Exit)+
      ultimately show ?thesis 
        apply(rule_tac x="asx@as'" in exI) apply(rule_tac x="as@asx'" in exI)
        by(auto intro:ProcCFG.path_Append ProcCFG.valid_path_same_level_path_Append
          ProcCFG.same_level_path_valid_path_Append ProcCFG.intras_same_level_path
          simp:ProcCFG.vp_def)
    next
      assume "(p,n) = targetnode a"
      with ‹(p', Entry) = targetnode a›[THEN sym] 
      have [simp]:"n = Entry" "p = p'" by simp_all
      from ‹c ⊢ Label l -CEdge (p', es', rets')→⇩p Label l'›
      have "containsCall procs c [] p'" by(rule Proc_CFG_Call_containsCall)
      with ‹containsCall procs prog ps px› ‹(px, ins, outs, c) ∈ set procs›
      have "containsCall procs prog (ps@[px]) p'"
        by(rule containsCall_in_proc)
      with ‹(p', ins', outs', c') ∈ set procs›
      have "prog,procs ⊢ (p', Entry) -(λs. False)⇩√→ (p', Exit)"
        by(fastforce intro:PCFG.Proc Proc_CFG_Entry_Exit)
      hence "wfp ⊢ (p',Entry) -[((p',Entry),(λs. False)⇩√,(p',Exit))]→* (p',Exit)"
        by(fastforce intro:ProcCFG.path.intros 
          simp:valid_edge_def ProcCFG.valid_node_def)
      moreover
      from ‹Rep_wf_prog wfp = (prog,procs)› ‹(p', ins', outs', c') ∈ set procs›
        ‹containsCall procs prog (ps@[px]) p'›
      obtain as as' where "CFG.valid_path' sourcenode targetnode kind
        (valid_edge wfp) (get_return_edges wfp) (Main,Entry) as (p',Entry)"
        and "CFG.valid_path' sourcenode targetnode kind
        (valid_edge wfp) (get_return_edges wfp) (p',Exit) as' (Main,Exit)"
        by -(erule Entry_to_Entry_and_Exit_to_Exit)+
      ultimately show ?thesis
        apply(rule_tac x="as" in exI)
        apply(rule_tac x="[((p',Entry),(λs. False)⇩√,(p',Exit))]@as'" in exI)
        apply(unfold ProcCFG.vp_def)
        by(fastforce intro:ProcCFG.path_Append 
          ProcCFG.same_level_path_valid_path_Append ProcCFG.intras_same_level_path
          simp:intra_kind_def)+
    qed
  next
    case (MainReturn l px es rets l' ins outs c)
    from disj show ?case
    proof
      assume "(p,n) = sourcenode a"
      with ‹(px, Exit) = sourcenode a›[THEN sym] 
      have [simp]:"n = Exit" "p = px" by simp_all
      from ‹prog ⊢ Label l -CEdge (px, es, rets)→⇩p Label l'›
      have "containsCall procs prog [] px" by(rule Proc_CFG_Call_containsCall)
      with ‹(px, ins, outs, c) ∈ set procs›
      have "prog,procs ⊢ (px, Entry) -(λs. False)⇩√→ (px, Exit)"
        by(fastforce intro:PCFG.Proc Proc_CFG_Entry_Exit)
      hence "wfp ⊢ (px,Entry) -[((px,Entry),(λs. False)⇩√,(px,Exit))]→* (px,Exit)"
        by(fastforce intro:ProcCFG.path.intros 
          simp:valid_edge_def ProcCFG.valid_node_def)
      moreover
      from ‹Rep_wf_prog wfp = (prog,procs)› ‹(px, ins, outs, c) ∈ set procs›
        ‹containsCall procs prog [] px›
      obtain as as' where "CFG.valid_path' sourcenode targetnode kind
        (valid_edge wfp) (get_return_edges wfp) (Main,Entry) as (px,Entry)"
        and "CFG.valid_path' sourcenode targetnode kind
        (valid_edge wfp) (get_return_edges wfp) (px,Exit) as' (Main,Exit)"
        by -(erule Entry_to_Entry_and_Exit_to_Exit)+
      ultimately show ?thesis
        apply(rule_tac x="as@[((px,Entry),(λs. False)⇩√,(px,Exit))]" in exI)
        apply(rule_tac x="as'" in exI)
        apply(unfold ProcCFG.vp_def)
        by(fastforce intro:ProcCFG.path_Append 
          ProcCFG.valid_path_same_level_path_Append ProcCFG.intras_same_level_path
          simp:intra_kind_def)+
    next
      assume "(p, n) = targetnode a"
      with ‹(Main, Label l') = targetnode a›[THEN sym] 
      have [simp]:"n = Label l'" "p = Main" by simp_all
      with ‹prog ⊢ Label l -CEdge (px, es, rets)→⇩p Label l'› have "l' < #:prog"
        by(fastforce intro:Proc_CFG_targetlabel_less_num_nodes)
      with ‹Rep_wf_prog wfp = (prog,procs)› 
      obtain as as' where "wfp ⊢ (Main,Entry) -as→* (Main,Label l')"
        and "∀a ∈ set as. intra_kind (kind a)"
        and "wfp ⊢ (Main,Label l') -as'→* (Main,Exit)"
        and "∀a ∈ set as'. intra_kind (kind a)"
        by -(erule Label_Proc_CFG_Entry_Exit_path_Main)+
      thus ?thesis 
        by(fastforce intro:ProcCFG.intra_path_vp simp:ProcCFG.intra_path_def)
    qed
  next
    case (ProcReturn px ins outs c l p' es' rets' l' ins' outs' c' ps)
    from disj show ?case
    proof
      assume "(p,n) = sourcenode a"
      with ‹(p', Exit) = sourcenode a›[THEN sym] 
      have [simp]:"n = Exit" "p = p'" by simp_all
      from ‹c ⊢ Label l -CEdge (p', es', rets')→⇩p Label l'›
      have "containsCall procs c [] p'" by(rule Proc_CFG_Call_containsCall)
      with ‹containsCall procs prog ps px› ‹(px, ins, outs, c) ∈ set procs›
      have "containsCall procs prog (ps@[px]) p'"
        by(rule containsCall_in_proc)
      with ‹(p', ins', outs', c') ∈ set procs›
      have "prog,procs ⊢ (p', Entry) -(λs. False)⇩√→ (p', Exit)"
        by(fastforce intro:PCFG.Proc Proc_CFG_Entry_Exit)
      hence "wfp ⊢ (p',Entry) -[((p',Entry),(λs. False)⇩√,(p',Exit))]→* (p',Exit)"
        by(fastforce intro:ProcCFG.path.intros 
          simp:valid_edge_def ProcCFG.valid_node_def)
      moreover
      from ‹Rep_wf_prog wfp = (prog,procs)› ‹(p', ins', outs', c') ∈ set procs›
        ‹containsCall procs prog (ps@[px]) p'›
      obtain as as' where "CFG.valid_path' sourcenode targetnode kind
        (valid_edge wfp) (get_return_edges wfp) (Main,Entry) as (p',Entry)"
        and "CFG.valid_path' sourcenode targetnode kind
        (valid_edge wfp) (get_return_edges wfp) (p',Exit) as' (Main,Exit)"
        by -(erule Entry_to_Entry_and_Exit_to_Exit)+
      ultimately show ?thesis
        apply(rule_tac x="as@[((p',Entry),(λs. False)⇩√,(p',Exit))]" in exI)
        apply(rule_tac x="as'" in exI)
        apply(unfold ProcCFG.vp_def)
        by(fastforce intro:ProcCFG.path_Append 
          ProcCFG.valid_path_same_level_path_Append ProcCFG.intras_same_level_path
          simp:intra_kind_def)+
    next
      assume "(p, n) = targetnode a"
      with ‹(px, Label l') = targetnode a›[THEN sym] 
      have [simp]:"n = Label l'" "p = px" by simp_all
      with ‹c ⊢ Label l -CEdge (p', es', rets')→⇩p Label l'› have "l' < #:c"
        by(fastforce intro:Proc_CFG_targetlabel_less_num_nodes)
      from ‹Rep_wf_prog wfp = (prog,procs)› ‹l' < #:c› 
        ‹containsCall procs prog ps px› ‹(px, ins, outs, c) ∈ set procs›
      obtain as as' where "wfp ⊢ (px,Label l') -as→* (px,Exit)"
        and "∀a ∈ set as. intra_kind (kind a)"
        and "wfp ⊢ (px,Entry) -as'→* (px,Label l')"
        and "∀a ∈ set as'. intra_kind (kind a)"
        by -(erule Label_Proc_CFG_Entry_Exit_path_Proc)+
      moreover
      from ‹Rep_wf_prog wfp = (prog,procs)› ‹containsCall procs prog ps px›
        ‹(px, ins, outs, c) ∈ set procs› obtain asx asx' 
        where" CFG.valid_path' sourcenode targetnode kind
        (valid_edge wfp) (get_return_edges wfp) (Main,Entry) asx (px,Entry)"
        and "CFG.valid_path' sourcenode targetnode kind
        (valid_edge wfp) (get_return_edges wfp) (px,Exit) asx' (Main,Exit)"
        by -(erule Entry_to_Entry_and_Exit_to_Exit)+
      ultimately show ?thesis 
        apply(rule_tac x="asx@as'" in exI) apply(rule_tac x="as@asx'" in exI)
        by(auto intro:ProcCFG.path_Append ProcCFG.valid_path_same_level_path_Append
          ProcCFG.same_level_path_valid_path_Append ProcCFG.intras_same_level_path
          simp:ProcCFG.vp_def)
    qed
  next
    case (MainCallReturn nx px es rets nx')
    from ‹prog ⊢ nx -CEdge (px, es, rets)→⇩p nx'› disj
      ‹(Main, nx) = sourcenode a›[THEN sym] ‹(Main, nx') = targetnode a›[THEN sym]
    obtain l where [simp]:"n = Label l" "p = Main"
      by(fastforce dest:Proc_CFG_Call_Labels)
    from ‹prog ⊢ nx -CEdge (px, es, rets)→⇩p nx'› disj
      ‹(Main, nx) = sourcenode a›[THEN sym] ‹(Main, nx') = targetnode a›[THEN sym]
    have "l < #:prog" by(auto intro:Proc_CFG_sourcelabel_less_num_nodes
      Proc_CFG_targetlabel_less_num_nodes)
    with ‹Rep_wf_prog wfp = (prog,procs)› 
    obtain as as' where "wfp ⊢ (Main,Entry) -as→* (Main,Label l)"
      and "∀a ∈ set as. intra_kind (kind a)"
      and "wfp ⊢ (Main,Label l) -as'→* (Main,Exit)"
      and "∀a ∈ set as'. intra_kind (kind a)"
      by -(erule Label_Proc_CFG_Entry_Exit_path_Main)+
    thus ?thesis
      apply(rule_tac x="as" in exI) apply(rule_tac x="as'" in exI) apply simp
      by(fastforce intro:ProcCFG.intra_path_vp simp:ProcCFG.intra_path_def)
  next
    case (ProcCallReturn px ins outs c nx p' es' rets' nx' ps)
    from ‹(px, ins, outs, c) ∈ set procs› wf have [simp]:"px ≠ Main" by auto
    from ‹c ⊢ nx -CEdge (p', es', rets')→⇩p nx'› disj 
      ‹(px, nx) = sourcenode a›[THEN sym] ‹(px, nx') = targetnode a›[THEN sym]
    obtain l where [simp]:"n = Label l" "p = px"
      by(fastforce dest:Proc_CFG_Call_Labels)
    from ‹c ⊢ nx -CEdge (p', es', rets')→⇩p nx'› disj 
    ‹(px, nx) = sourcenode a›[THEN sym] ‹(px, nx') = targetnode a›[THEN sym]
    have "l < #:c"
      by(auto intro:Proc_CFG_sourcelabel_less_num_nodes
        Proc_CFG_targetlabel_less_num_nodes)
    with ‹Rep_wf_prog wfp = (prog,procs)› ‹(px, ins, outs, c) ∈ set procs› 
      ‹containsCall procs prog ps px›
    obtain as as' where "wfp ⊢ (px,Entry) -as→* (px,Label l)"
      and "∀a ∈ set as. intra_kind (kind a)"
      and "wfp ⊢ (px,Label l) -as'→* (px,Exit)"
      and "∀a ∈ set as'. intra_kind (kind a)"
      by -(erule Label_Proc_CFG_Entry_Exit_path_Proc)+
    moreover
    from ‹Rep_wf_prog wfp = (prog,procs)› 
      ‹containsCall procs prog ps px› ‹(px, ins, outs, c) ∈ set procs›
    obtain asx asx' where "CFG.valid_path' sourcenode targetnode kind
      (valid_edge wfp) (get_return_edges wfp) (Main,Entry) asx (px,Entry)"
      and "CFG.valid_path' sourcenode targetnode kind
      (valid_edge wfp) (get_return_edges wfp) (px,Exit) asx' (Main,Exit)"
      by -(erule Entry_to_Entry_and_Exit_to_Exit)+
    ultimately show ?thesis
      apply(rule_tac x="asx@as" in exI) apply(rule_tac x="as'@asx'" in exI)
      by(auto intro:ProcCFG.path_Append ProcCFG.valid_path_same_level_path_Append
        ProcCFG.same_level_path_valid_path_Append ProcCFG.intras_same_level_path
        simp:ProcCFG.vp_def)
  qed
qed



subsection ‹Instantiating the ‹Postdomination› locale›

interpretation ProcPostdomination:
  Postdomination sourcenode targetnode kind "valid_edge wfp" "(Main,Entry)"
  get_proc "get_return_edges wfp" "lift_procs wfp" Main "(Main,Exit)"
  for wfp
proof -
  from Rep_wf_prog[of wfp]
  obtain prog procs where [simp]:"Rep_wf_prog wfp = (prog,procs)" 
    by(fastforce simp:wf_prog_def)
  hence wf:"well_formed procs" by(fastforce intro:wf_wf_prog)
  show "Postdomination sourcenode targetnode kind (valid_edge wfp)
    (Main, Entry) get_proc (get_return_edges wfp) (lift_procs wfp) Main (Main, Exit)"
  proof
    fix m
    assume "CFG.valid_node sourcenode targetnode (valid_edge wfp) m"
    then obtain a where "valid_edge wfp a"
      and "m = sourcenode a ∨ m = targetnode a"
      by(fastforce simp:ProcCFG.valid_node_def)
    obtain p n where [simp]:"m = (p,n)" by(cases m) auto
    from ‹valid_edge wfp a› ‹m = sourcenode a ∨ m = targetnode a› 
      ‹Rep_wf_prog wfp = (prog,procs)›
    show "∃as. CFG.valid_path' sourcenode targetnode kind (valid_edge wfp)
      (get_return_edges wfp) (Main, Entry) as m"
      by(auto dest!:edge_valid_paths simp:valid_edge_def)
  next
    fix m
    assume "CFG.valid_node sourcenode targetnode (valid_edge wfp) m"
    then obtain a where "valid_edge wfp a"
      and "m = sourcenode a ∨ m = targetnode a"
      by(fastforce simp:ProcCFG.valid_node_def)
    obtain p n where [simp]:"m = (p,n)" by(cases m) auto
    from ‹valid_edge wfp a› ‹m = sourcenode a ∨ m = targetnode a› 
      ‹Rep_wf_prog wfp = (prog,procs)›
    show "∃as. CFG.valid_path' sourcenode targetnode kind (valid_edge wfp)
      (get_return_edges wfp) m as (Main,Exit)"
      by(auto dest!:edge_valid_paths simp:valid_edge_def)
  next
    fix n n'
    assume mex1:"CFGExit.method_exit sourcenode kind (valid_edge wfp) (Main,Exit) n"
      and mex2:"CFGExit.method_exit sourcenode kind (valid_edge wfp) (Main,Exit) n'"
      and "get_proc n = get_proc n'"
    from mex1 
    have "n = (Main,Exit) ∨ (∃a Q p f. n = sourcenode a ∧ valid_edge wfp a ∧ 
      kind a = Q↩⇘p⇙f)" by(simp add:ProcCFGExit.method_exit_def)
    thus "n = n'"
    proof
      assume "n = (Main,Exit)"
      from mex2 have "n' = (Main,Exit) ∨ (∃a Q p f. n' = sourcenode a ∧ 
        valid_edge wfp a ∧ kind a = Q↩⇘p⇙f)" 
        by(simp add:ProcCFGExit.method_exit_def)
      thus ?thesis
      proof
        assume "n' = (Main,Exit)"
        with ‹n = (Main,Exit)› show ?thesis by simp
      next
        assume "∃a Q p f. n' = sourcenode a ∧ 
          valid_edge wfp a ∧ kind a = Q↩⇘p⇙f"
        then obtain a Q p f where "n' = sourcenode a"
          and "valid_edge wfp a" and "kind a = Q↩⇘p⇙f" by blast
        from ‹valid_edge wfp a› ‹kind a = Q↩⇘p⇙f›
        have "get_proc (sourcenode a) = p" by(rule ProcCFG.get_proc_return)
        with ‹get_proc n = get_proc n'› ‹n = (Main,Exit)› ‹n' = sourcenode a›
        have "get_proc (Main,Exit) = p" by simp
        hence "p = Main" by simp
        with ‹kind a = Q↩⇘p⇙f› have "kind a = Q↩⇘Main⇙f" by simp
        with ‹valid_edge wfp a› have False by(rule ProcCFG.Main_no_return_source)
        thus ?thesis by simp
      qed
    next
      assume "∃a Q p f. n = sourcenode a ∧ 
        valid_edge wfp a ∧ kind a = Q↩⇘p⇙f"
      then obtain a Q p f where "n = sourcenode a"
        and "valid_edge wfp a" and "kind a = Q↩⇘p⇙f" by blast
      from ‹valid_edge wfp a› ‹kind a = Q↩⇘p⇙f›
      have "get_proc (sourcenode a) = p" by(rule ProcCFG.get_proc_return)
      from mex2 have "n' = (Main,Exit) ∨ (∃a Q p f. n' = sourcenode a ∧ 
        valid_edge wfp a ∧ kind a = Q↩⇘p⇙f)" 
        by(simp add:ProcCFGExit.method_exit_def)
      thus ?thesis
      proof
        assume "n' = (Main,Exit)"
        from ‹get_proc (sourcenode a) = p› ‹get_proc n = get_proc n'›
          ‹n' = (Main,Exit)› ‹n = sourcenode a›
        have "get_proc (Main,Exit) = p" by simp
        hence "p = Main" by simp
        with ‹kind a = Q↩⇘p⇙f› have "kind a = Q↩⇘Main⇙f" by simp
        with ‹valid_edge wfp a› have False by(rule ProcCFG.Main_no_return_source)
        thus ?thesis by simp
      next
        assume "∃a Q p f. n' = sourcenode a ∧ 
          valid_edge wfp a ∧ kind a = Q↩⇘p⇙f"
        then obtain a' Q' p' f' where "n' = sourcenode a'"
          and "valid_edge wfp a'" and "kind a' = Q'↩⇘p'⇙f'" by blast
        from ‹valid_edge wfp a'› ‹kind a' = Q'↩⇘p'⇙f'›
        have "get_proc (sourcenode a') = p'" by(rule ProcCFG.get_proc_return)
        with ‹get_proc n = get_proc n'› ‹get_proc (sourcenode a) = p›
          ‹n = sourcenode a› ‹n' = sourcenode a'›
        have "p' = p" by simp
        from ‹valid_edge wfp a› ‹kind a = Q↩⇘p⇙f›
        have "sourcenode a = (p,Exit)" by(auto elim:PCFG.cases simp:valid_edge_def)
        from ‹valid_edge wfp a'› ‹kind a' = Q'↩⇘p'⇙f'›
        have "sourcenode a' = (p',Exit)" by(auto elim:PCFG.cases simp:valid_edge_def)
        with ‹n = sourcenode a› ‹n' = sourcenode a'› ‹p' = p›
          ‹sourcenode a = (p,Exit)› show ?thesis by simp
      qed
    qed
  qed
qed


end