Theory PCFG

section ‹Definition of the CFG›

theory PCFG imports ProcState begin

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

datatype label = Label nat | Entry | Exit

subsection‹The CFG for every procedure›

subsubsection ‹Definition of ⊕›

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


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

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

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

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

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

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

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

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

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


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

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

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

subsubsection ‹The edges of the procedure CFG›

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

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


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

inductive Proc_CFG :: "cmd  label  p_edge_kind  label  bool"
("_  _ -_p _")
where

  Proc_CFG_Entry_Exit:
  "prog  Entry -IEdge (λs. False)p Exit"

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

| Proc_CFG_Skip: 
  "Skip  Label 0 -IEdge idp Exit"

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

| Proc_CFG_LAssSkip:
  "V:=e  Label 1 -IEdge idp Exit"

| Proc_CFG_SeqFirst:
  "c1  n -etp n'; n'  Exit  c1;;c2  n -etp n'"

| Proc_CFG_SeqConnect: 
  "c1  n -etp Exit; n  Entry  c1;;c2  n -etp Label #:c1"

| Proc_CFG_SeqSecond: 
  "c2  n -etp n'; n  Entry  c1;;c2  n  #:c1 -etp n'  #:c1"

| Proc_CFG_CondTrue:
    "if (b) c1 else c2  Label 0 
  -IEdge (λcf. state_check cf b (Some true))p Label 1"

| Proc_CFG_CondFalse:
    "if (b) c1 else c2  Label 0 -IEdge (λcf. state_check cf b (Some false))p 
                        Label (#:c1 + 1)"

| Proc_CFG_CondThen:
  "c1  n -etp n'; n  Entry  if (b) c1 else c2  n  1 -etp n'  1"

| Proc_CFG_CondElse:
  "c2  n -etp n'; n  Entry 
   if (b) c1 else c2  n  (#:c1 + 1) -etp n'  (#:c1 + 1)"

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

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

| Proc_CFG_WhileFalseSkip:
  "while (b) c'  Label 1 -IEdge idp Exit"

| Proc_CFG_WhileBody:
  "c'  n -etp n'; n  Entry; n'  Exit 
   while (b) c'  n  2 -etp n'  2"

| Proc_CFG_WhileBodyExit:
  "c'  n -etp Exit; n  Entry  while (b) c'  n  2 -etp Label 0"

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

| Proc_CFG_CallSkip:
  "Call p es rets  Label 1 -IEdge idp Exit"


subsubsection‹Some lemmas about the procedure CFG›

lemma Proc_CFG_Exit_no_sourcenode [dest]:
  "prog  Exit -etp n'  False"
by(induct prog n"Exit" et n' rule:Proc_CFG.induct,auto)


lemma Proc_CFG_Entry_no_targetnode [dest]:
  "prog  n -etp Entry  False"
by(induct prog n et n'"Entry" rule:Proc_CFG.induct,auto)


lemma Proc_CFG_IEdge_intra_kind:
  "prog  n -IEdge etp n'  intra_kind et"
by(induct prog n x"IEdge et" n' rule:Proc_CFG.induct,auto simp:intra_kind_def)


lemma [dest]:"prog  n -IEdge (Q:r↪⇘pfs)p n'  False"
by(fastforce dest:Proc_CFG_IEdge_intra_kind simp:intra_kind_def)

lemma [dest]:"prog  n -IEdge (Q↩⇘pf)p n'  False"
by(fastforce dest:Proc_CFG_IEdge_intra_kind simp:intra_kind_def)


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


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


lemma Proc_CFG_EntryD:
  "prog  Entry -etp n' 
   (n' = Exit  et = IEdge(λs. False))  (n' = Label 0  et = IEdge (λs. True))"
by(induct prog n"Entry" et n' rule:Proc_CFG.induct,auto)


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


text ‹Lots of lemmas for call edges …›

lemma Proc_CFG_Call_Labels:
  "prog  n -CEdge (p,es,rets)p n'  l. n = Label l  n' = Label (Suc l)"
by(induct prog n et"CEdge (p,es,rets)" n' rule:Proc_CFG.induct,auto)


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


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


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


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


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


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


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


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


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


subsection ‹And now: the interprocedural CFG›

subsubsection ‹Statements containing calls›

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

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


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

declare conj_cong[fundef_cong]

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


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


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



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