Theory ValidPaths

section ‹Lemmas concerning paths to instantiate locale Postdomination›

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

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


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

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


declare One_nat_def [simp del]



subsubsection ‹From prog› to prog;;c2


lemma Proc_CFG_edge_SeqFirst_nodes_Label:
  "prog  Label l -etp Label l'  prog;;c2  Label l -etp Label l'"
proof(induct prog "Label l" et "Label l'" rule:Proc_CFG.induct)
  case (Proc_CFG_SeqSecond c2' n et n' c1)
  hence "(c1;; c2');; c2  n  #:c1 -etp n'  #:c1"
    by(fastforce intro:Proc_CFG_SeqFirst Proc_CFG.Proc_CFG_SeqSecond)
  with n  #:c1 = Label l n'  #:c1 = Label l' show ?case by fastforce
next
  case (Proc_CFG_CondThen c1 n et n' b c2')
  hence "if (b) c1 else c2';; c2  n  1 -etp 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 c1 n et n' b c2')
  hence "if (b) c2' else c1 ;; c2  n  #:c2' + 1 -etp n'  (#:c2' + 1)"   
    by(fastforce intro:Proc_CFG_SeqFirst Proc_CFG.Proc_CFG_CondElse)
  with n  #:c2' + 1 = Label l n'  #:c2' + 1 = Label l' show ?case by fastforce
next
  case (Proc_CFG_WhileBody c' n et n' b)
  hence "while (b) c';; c2  n  2 -etp 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';; c2  n  2 -etp 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 -etp n'"
  obtains nx where "prog;;c2  Label l -etp nx"
proof(atomize_elim)
  from prog  Label l -etp n' obtain n where "prog  n -etp n'" and "Label l = n"
    by simp
  thus "nx. prog;;c2  Label l -etp nx"
  proof(induct prog n et n' rule:Proc_CFG.induct)
    case (Proc_CFG_SeqSecond c2' n et n' c1)
    show ?case
    proof(cases "n' = Exit")
      case True
      with c2'  n -etp n' n  Entry have "c1;; c2'  n  #:c1 -etp Exit  #:c1"
        by(fastforce intro:Proc_CFG.Proc_CFG_SeqSecond)
      moreover from n  Entry have "n  #:c1  Entry" by(cases n) auto
      ultimately
      have "c1;; c2';; c2  n  #:c1 -etp Label (#:c1;; c2')"
        by(fastforce intro:Proc_CFG_SeqConnect)
      with Label l = n  #:c1 show ?thesis by fastforce
    next
      case False
      with Proc_CFG_SeqSecond
      have "(c1;; c2');; c2  n  #:c1 -etp n'  #:c1"
        by(fastforce intro:Proc_CFG_SeqFirst Proc_CFG.Proc_CFG_SeqSecond)
      with Label l = n  #:c1 show ?thesis by fastforce
    qed
  next
    case (Proc_CFG_CondThen c1 n et n' b c2')
    show ?case
    proof(cases "n' = Exit")
      case True
      with c1  n -etp n' n  Entry
      have "if (b) c1 else c2'  n  1 -etp 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) c1 else c2';; c2  n  1 -etp Label (#:if (b) c1 else c2')"
        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) c1 else c2';; c2  Label l -etp 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 c1 n et n' b c2')
    show ?case
    proof(cases "n' = Exit")
      case True
      with c1  n -etp n' n  Entry
      have "if (b) c2' else c1  n  (#:c2' + 1) -etp Exit  (#:c2' + 1)"
        by(fastforce intro:Proc_CFG.Proc_CFG_CondElse)
      moreover from n  Entry have "n  (#:c2' + 1)  Entry" by(cases n) auto
      ultimately
      have "if (b) c2' else c1;; c2  n  (#:c2' + 1) -etp 
        Label (#:if (b) c2' else c1)"
        by(fastforce intro:Proc_CFG_SeqConnect)
      with Label l = n  (#:c2' + 1) show ?thesis by fastforce
    next
      case False
      hence "n'  (#:c2' + 1)  Exit" by(cases n') auto
      with Proc_CFG_CondElse
      have  "if (b) c2' else c1 ;; c2  Label l -etp n'  (#:c2' + 1)"
        by(fastforce intro:Proc_CFG_SeqFirst Proc_CFG.Proc_CFG_CondElse)
      with Label l = n  (#:c2' + 1) show ?thesis by fastforce
    qed
  qed (auto intro:Proc_CFG.intros)
qed


lemma Proc_CFG_edge_SeqFirst_target_Label:
  "prog  n -etp n'; Label l' = n'  prog;;c2  n -etp Label l'"
proof(induct prog n et n' rule:Proc_CFG.induct)
  case (Proc_CFG_SeqSecond c2' n et n' c1)
  from Label l' = n'  #:c1 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 c1 n et n' b c2')
  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;;c2,procs  (p,Label l) -et (p',nx)"
proof(atomize_elim)
  from prog,procs  (p,Label l) -et (p',n')
  show "nx. prog;;c2,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 etp n'
    obtain nx' where "prog;;c2  Label l -IEdge etp 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;;c2) 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;;c2  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;;c2) 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;;c2  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;;c2) 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;;c2,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;;c2) 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;;c2) 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;;c2) ps p" by simp
  with ProcCallReturn show ?case by(fastforce dest!:PCFG.ProcCallReturn)
qed


lemma path_SeqFirst:
  assumes "Rep_wf_prog wfp = (prog,procs)" and "Rep_wf_prog wfp' = (prog;;c2,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;; c2, 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); aset 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;;c2,procs)
  from Rep_wf_prog wfp = (prog,procs) have wf:"well_formed procs" 
    by(fastforce intro:wf_wf_prog)
  from aset (a # as). intra_kind (kind a) have "intra_kind (kind a)"
    and "aset 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 aset 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 aset 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 c1;;prog›

lemma Proc_CFG_edge_SeqSecond_source_not_Entry:
  "prog  n -etp n'; n  Entry  c1;;prog  n  #:c1 -etp n'  #:c1"
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
   c1;;prog,procs  (Main,n  #:c1) -et (p',n'  #:c1)"
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 "c1;;prog  n  #:c1 -CEdge (p, es, rets)p n'  #:c1"
    by(rule Proc_CFG_edge_SeqSecond_source_not_Entry)
  with MainCallReturn show ?case by(fastforce intro:PCFG.MainCallReturn)
qed (auto simp:intra_kind_def)


lemma valid_node_Main_SeqSecond:
  assumes "CFG.valid_node sourcenode targetnode (valid_edge wfp) (Main,n)"
  and "n  Entry" and "Rep_wf_prog wfp = (prog,procs)" 
  and "Rep_wf_prog wfp' = (c1;;prog,procs)"
  shows "CFG.valid_node sourcenode targetnode (valid_edge wfp') (Main, n  #:c1)"
proof -
  note [simp] = Rep_wf_prog wfp = (prog,procs) Rep_wf_prog wfp' = (c1;;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 "c1;;prog  n  #:c1 -IEdge (kind a)p nx'  #:c1"
        by(fastforce intro:Proc_CFG_edge_SeqSecond_source_not_Entry)
      hence "c1;;prog,procs  (Main,n  #:c1) -kind a (Main,nx'  #:c1)"
        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 "c1  Label l -IEdge etxp Exit" and "l  #:c1"
            by(erule Proc_CFG_Exit_edge)
          hence "c1;;prog  Label l -IEdge etxp Label #:c1"
            by(fastforce intro:Proc_CFG_SeqConnect)
          with nx' = Label 0 
          have "c1;;prog,procs  (Main,Label l) -etx (Main,nx'#:c1)"
            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 "c1;;prog  nx  #:c1 -IEdge (kind a)p nx'  #:c1"
          by(fastforce intro:Proc_CFG_edge_SeqSecond_source_not_Entry)
        hence "c1;;prog,procs  (Main,nx  #:c1) -kind a (Main,nx'  #:c1)"
          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 "c1;;prog  Label l  #:c1 -CEdge (p, es, rets)p n'  #:c1"
      by -(rule Proc_CFG_edge_SeqSecond_source_not_Entry,auto)
    with (p, ins, outs, c)  set procs
    have "c1;;prog,procs  (Main,Label (l + #:c1)) 
      -(λs. True):(Main,n'  #:c1)↪⇘pmap (λ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 "c1;;prog  Label l  #:c1 -CEdge (p, es, rets)p Label l'  #:c1"
      by -(rule Proc_CFG_edge_SeqSecond_source_not_Entry,auto)
    with (p, ins, outs, c)  set procs
    have "c1;;prog,procs  (p,Exit) -(λcf. snd cf = (Main,Label l'  #:c1))↩⇘p(λcf cf'. cf'(rets [:=] map cf outs)) (Main,Label (l' + #:c1))"
      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 "c1;;prog  n  #:c1 -CEdge (p, es, rets)p nx'  #:c1"
        by(fastforce intro:Proc_CFG_edge_SeqSecond_source_not_Entry)
      hence "c1;;prog,procs  (Main,n  #:c1) -(λs. False) (Main,nx'  #:c1)"
        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 "c1;;prog  nx  #:c1 -CEdge (p, es, rets)p nx'  #:c1"
        by(fastforce intro:Proc_CFG_edge_SeqSecond_source_not_Entry)
      hence "c1;;prog,procs  (Main,nx  #:c1) -(λs. False) (Main,nx'  #:c1)"
        by -(rule PCFG.MainCallReturn)
      with (Main, n) = targetnode a (Main, nx') = targetnode a[THEN sym] 
      show ?thesis by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
    qed
  next
    case (ProcCallReturn p ins outs c nx p' es' rets' n' ps)
    from (p, nx) = sourcenode a[THEN sym] (p, n') = targetnode a[THEN sym]
      (p, ins, outs, c)  set procs well_formed procs
      (Main, n) = sourcenode a  (Main, n) = targetnode a
    have False by fastforce
    thus ?case by simp
  qed
qed


lemma path_Main_SeqSecond:
  assumes "Rep_wf_prog wfp = (prog,procs)" and "Rep_wf_prog wfp' = (c1;;prog,procs)"
  shows "wfp  (Main,n) -as→* (p',n'); a  set as. intra_kind (kind a); n  Entry
   wfp'  (Main,n  #:c1) -as ⊕s #:c1→* (p',n'  #:c1)"
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' = (c1;;prog,procs)
  have "CFG.valid_node sourcenode targetnode (valid_edge wfp') (Main, n'  #:c1)"
    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); aset as. intra_kind (kind a); n  Entry 
     wfp'  (Main, n  #:c1) -as ⊕s #:c1→* (p', n'  #:c1)
  note [simp] = Rep_wf_prog wfp = (prog,procs) Rep_wf_prog wfp' = (c1;;prog,procs)
  from Rep_wf_prog wfp = (prog,procs) have wf:"well_formed procs" 
    by(fastforce intro:wf_wf_prog)
  from aset (a # as). intra_kind (kind a) have "intra_kind (kind a)"
    and "aset 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'') aset as. intra_kind (kind a) nx''  Entry]
  have path:"wfp'  (Main, nx''  #:c1) -as ⊕s #:c1→* (p', n'  #:c1)" .
  from valid_edge wfp a sourcenode a = (Main, n) targetnode a = n''
    n'' = (Main,nx'') n  Entry intra_kind (kind a) wf
  have "c1;; prog,procs  (Main, n  #:c1) -kind a (Main, nx''  #:c1)"
    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 c2

lemma Proc_CFG_edge_CondTrue_source_not_Entry:
  "prog  n -etp n'; n  Entry  if (b) prog else c2  n  1 -etp 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 c2,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 c2  n  1 -CEdge (p, es, rets)p n'  1"
    by(rule Proc_CFG_edge_CondTrue_source_not_Entry)
  with MainCallReturn show ?case by(fastforce intro:PCFG.MainCallReturn)
qed (auto simp:intra_kind_def)


lemma valid_node_Main_CondTrue:
  assumes "CFG.valid_node sourcenode targetnode (valid_edge wfp) (Main,n)"
  and "n  Entry" and "Rep_wf_prog wfp = (prog,procs)" 
  and "Rep_wf_prog wfp' = (if (b) prog else c2,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 c2,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 c2  n  1 -IEdge (kind a)p nx'  1"
        by(fastforce intro:Proc_CFG_edge_CondTrue_source_not_Entry)
      hence "if (b) prog else c2,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 c2  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 c2,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 c2  nx  1 -IEdge (kind a)p nx'  1"
          by(fastforce intro:Proc_CFG_edge_CondTrue_source_not_Entry)
        hence "if (b) prog else c2,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 c2  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 c2,procs  (Main,Label (l + 1)) 
      -(λs. True):(Main,n'  1)↪⇘pmap (λ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 c2  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 c2,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 c2  n  1 -CEdge (p, es, rets)p nx'  1"
        by(fastforce intro:Proc_CFG_edge_CondTrue_source_not_Entry)
      hence "if (b) prog else c2,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 c2  nx  1 -CEdge (p, es, rets)p nx'  1"
        by(fastforce intro:Proc_CFG_edge_CondTrue_source_not_Entry)
      hence "if (b) prog else c2,procs  (Main,nx  1) -(λs. False) (Main,nx'  1)"
        by -(rule PCFG.MainCallReturn)
      with (Main, n) = targetnode a (Main, nx') = targetnode a[THEN sym]
      show ?thesis by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
    qed
  next
    case (ProcCallReturn p ins outs c nx p' es' rets' n' ps)
    from (p, nx) = sourcenode a[THEN sym] (p, n') = targetnode a[THEN sym]
      (p, ins, outs, c)  set procs well_formed procs
      (Main, n) = sourcenode a  (Main, n) = targetnode a
    have False by fastforce
    thus ?case by simp
  qed
qed


lemma path_Main_CondTrue:
  assumes "Rep_wf_prog wfp = (prog,procs)" 
  and "Rep_wf_prog wfp' = (if (b) prog else c2,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 c2,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); aset 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 c2,procs)
  from Rep_wf_prog wfp = (prog,procs) have wf:"well_formed procs" 
    by(fastforce intro:wf_wf_prog)
  from aset (a # as). intra_kind (kind a) have "intra_kind (kind a)"
    and "aset 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'') aset 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 c2,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) c1 else prog›

lemma Proc_CFG_edge_CondFalse_source_not_Entry:
  "prog  n -etp n'; n  Entry 
   if (b) c1 else prog  n  (#:c1 + 1) -etp n'  (#:c1 + 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) c1 else prog,procs  (Main,n  (#:c1 + 1)) -et (p',n'  (#:c1 + 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) c1 else prog  n  (#:c1 + 1) -CEdge (p, es, rets)p n'  (#:c1 + 1)"
    by(rule Proc_CFG_edge_CondFalse_source_not_Entry)
  with MainCallReturn show ?case by(fastforce intro:PCFG.MainCallReturn)
qed (auto simp:intra_kind_def)


lemma valid_node_Main_CondFalse:
  assumes "CFG.valid_node sourcenode targetnode (valid_edge wfp) (Main,n)"
  and "n  Entry" and "Rep_wf_prog wfp = (prog,procs)" 
  and "Rep_wf_prog wfp' = (if (b) c1 else prog,procs)"
  shows "CFG.valid_node sourcenode targetnode (valid_edge wfp') 
  (Main, n  (#:c1 + 1))"
proof -
  note [simp] = Rep_wf_prog wfp = (prog,procs) 
    Rep_wf_prog wfp' = (if (b) c1 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) c1 else prog  n  (#:c1 + 1) -IEdge (kind a)p nx'  (#:c1 + 1)"
        by(fastforce intro:Proc_CFG_edge_CondFalse_source_not_Entry)
      hence "if (b) c1 else prog,procs  (Main,n  (#:c1 + 1)) -kind a 
        (Main,nx'  (#:c1 + 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) c1 else prog  Label 0 
            -IEdge (λcf. state_check cf b (Some false))p Label (#:c1 + 1)"
            by(rule Proc_CFG_CondFalse)
          with nx' = Label 0 
          have "if (b) c1 else prog,procs  (Main,Label 0) 
            -(λcf. state_check cf b (Some false)) (Main,nx'  (#:c1 + 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) c1 else prog  nx  (#:c1 + 1) -IEdge (kind a)p nx'  (#:c1 + 1)"
          by(fastforce intro:Proc_CFG_edge_CondFalse_source_not_Entry)
        hence "if (b) c1 else prog,procs  (Main,nx  (#:c1 + 1)) -kind a 
          (Main,nx'  (#:c1 + 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) c1 else prog  Label l  (#:c1 + 1) -CEdge (p, es, rets)p 
      n'  (#:c1 + 1)" by -(rule Proc_CFG_edge_CondFalse_source_not_Entry,auto)
    with (p, ins, outs, c)  set procs
    have "if (b) c1 else prog,procs  (Main,Label (l + (#:c1 + 1))) 
      -(λs. True):(Main,n'  (#:c1 + 1))↪⇘pmap (λ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) c1 else prog  Label l  (#:c1 + 1) -CEdge (p, es, rets)p 
      Label l'  (#:c1 + 1)" by -(rule Proc_CFG_edge_CondFalse_source_not_Entry,auto)
    with (p, ins, outs, c)  set procs
    have "if (b) c1 else prog,procs  (p,Exit) 
      -(λcf. snd cf = (Main,Label l'  (#:c1 + 1)))↩⇘p(λcf cf'. cf'(rets [:=] map cf outs)) (Main,Label (l' + (#:c1 + 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) c1 else prog  n  (#:c1 + 1) -CEdge (p, es, rets)p 
        nx'  (#:c1 + 1)" by(fastforce intro:Proc_CFG_edge_CondFalse_source_not_Entry)
      hence "if (b) c1 else prog,procs  (Main,n  (#:c1 + 1)) 
        -(λs. False) (Main,nx'  (#:c1 + 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) c1 else prog  nx  (#:c1 + 1) -CEdge (p, es, rets)p 
        nx'  (#:c1 + 1)" by(fastforce intro:Proc_CFG_edge_CondFalse_source_not_Entry)
      hence "if (b) c1 else prog,procs  (Main,nx  (#:c1 + 1)) 
        -(λs. False) (Main,nx'  (#:c1 + 1))" by -(rule PCFG.MainCallReturn)
      with (Main, n) = targetnode a (Main, nx') = targetnode a[THEN sym]
      show ?thesis by(simp add:ProcCFG.valid_node_def)(fastforce simp:valid_edge_def)
    qed
  next
    case (ProcCallReturn p ins outs c nx p' es' rets' n' ps)
    from (p, nx) = sourcenode a[THEN sym] (p, n') = targetnode a[THEN sym]
      (p, ins, outs, c)  set procs well_formed procs
      (Main, n) = sourcenode a  (Main, n) = targetnode a
    have False by fastforce
    thus ?case by simp
  qed
qed


lemma path_Main_CondFalse:
  assumes "Rep_wf_prog wfp = (prog,procs)" 
  and "Rep_wf_prog wfp' = (if (b) c1 else prog,procs)"
  shows "wfp  (Main,n) -as→* (p',n'); a  set as. intra_kind (kind a); n  Entry
   wfp'  (Main,n  (#:c1 + 1)) -as ⊕s (#:c1 + 1)→* (p',n'  (#:c1 + 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) c1 else prog,procs)
  have "CFG.valid_node sourcenode targetnode (valid_edge wfp') (Main, n'  (#:c1 + 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); aset as. intra_kind (kind a); n  Entry
     wfp'  (Main, n  (#:c1 + 1)) -as ⊕s (#:c1 + 1)→* (p', n'  (#:c1 + 1))
  note [simp] = Rep_wf_prog wfp = (prog,procs) 
    Rep_wf_prog wfp' = (if (b) c1 else prog,procs)
  from Rep_wf_prog wfp = (prog,procs) have wf:"well_formed procs" 
    by(fastforce intro:wf_wf_prog)
  from aset (a # as). intra_kind (kind a) have "intra_kind (kind a)"
    and "aset 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'') aset as. intra_kind (kind a) nx''  Entry]
  have path:"wfp'  (Main, nx''  (#:c1 + 1)) -as ⊕s (#:c1 + 1)→* 
    (p', n'  (#:c1 + 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) c1 else prog,procs  (Main, n  (#:c1 + 1)) -kind a 
    (Main, nx''  (#:c1 + 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 -etp n'; n  Entry; n'  Exit 
   while (b) prog  n  2 -etp n'  2"
by(induct rule:Proc_CFG.induct)(fastforce intro:Proc_CFG_WhileBody Proc_CFG.intros)+


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


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


lemma path_Main_WhileBody:
  assumes "Rep_wf_prog wfp = (prog,procs)" 
  and "Rep_wf_prog wfp' = (while (b) prog,procs)"
  shows "wfp  (Main,n) -as→* (p',n'); a  set as. intra_kind (kind a); 
    n  Entry; n'  Exit  wfp'  (Main,n  2) -as ⊕s 2→* (p',n'  2)"
proof(induct "(Main,n)" as "(p',n')" arbitrary:n rule:ProcCFG.path.induct)
  case empty_path
  from CFG.valid_node sourcenode targetnode (valid_edge wfp) (Main, n')
    n'  Entry Rep_wf_prog wfp = (prog,procs)
    Rep_wf_prog wfp' = (while (b) prog,procs)
  have "CFG.valid_node sourcenode targetnode (valid_edge wfp') (Main, n'  2)" 
    by(fastforce intro:valid_node_Main_WhileBody)
  with Main = p' show ?case
    by(fastforce intro:ProcCFG.empty_path simp:label_incrs_def)
next
  case (Cons_path n'' as a n)
  note IH = n.  n'' = (Main, n); aset 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 aset (a # as). intra_kind (kind a) have "intra_kind (kind a)"
    and "aset as. intra_kind (kind a)" by simp_all
  from valid_edge wfp