Theory PCFG

header {* \isaheader{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 @{text "⊕"} *}

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"
("_ \<turnstile> _ -_->⇣p _")
where

  Proc_CFG_Entry_Exit:
  "prog \<turnstile> Entry -IEdge (λs. False)⇣\<surd>->⇣p Exit"

| Proc_CFG_Entry:
  "prog \<turnstile> Entry -IEdge (λs. True)⇣\<surd>->⇣p Label 0"

| Proc_CFG_Skip: 
  "Skip \<turnstile> Label 0 -IEdge \<Up>id->⇣p Exit"

| Proc_CFG_LAss: 
  "V:=e \<turnstile> Label 0 -IEdge \<Up>(λcf. update cf V e)->⇣p Label 1"

| Proc_CFG_LAssSkip:
  "V:=e \<turnstile> Label 1 -IEdge \<Up>id->⇣p Exit"

| Proc_CFG_SeqFirst:
  "[|c⇣1 \<turnstile> n -et->⇣p n'; n' ≠ Exit|] ==> c⇣1;;c⇣2 \<turnstile> n -et->⇣p n'"

| Proc_CFG_SeqConnect: 
  "[|c⇣1 \<turnstile> n -et->⇣p Exit; n ≠ Entry|] ==> c⇣1;;c⇣2 \<turnstile> n -et->⇣p Label #:c⇣1"

| Proc_CFG_SeqSecond: 
  "[|c⇣2 \<turnstile> n -et->⇣p n'; n ≠ Entry|] ==> c⇣1;;c⇣2 \<turnstile> n ⊕ #:c⇣1 -et->⇣p n' ⊕ #:c⇣1"

| Proc_CFG_CondTrue:
    "if (b) c⇣1 else c⇣2 \<turnstile> Label 0 
  -IEdge (λcf. state_check cf b (Some true))⇣\<surd>->⇣p Label 1"

| Proc_CFG_CondFalse:
    "if (b) c⇣1 else c⇣2 \<turnstile> Label 0 -IEdge (λcf. state_check cf b (Some false))⇣\<surd>->⇣p 
                        Label (#:c⇣1 + 1)"

| Proc_CFG_CondThen:
  "[|c⇣1 \<turnstile> n -et->⇣p n'; n ≠ Entry|] ==> if (b) c⇣1 else c⇣2 \<turnstile> n ⊕ 1 -et->⇣p n' ⊕ 1"

| Proc_CFG_CondElse:
  "[|c⇣2 \<turnstile> n -et->⇣p n'; n ≠ Entry|] 
  ==> if (b) c⇣1 else c⇣2 \<turnstile> n ⊕ (#:c⇣1 + 1) -et->⇣p n' ⊕ (#:c⇣1 + 1)"

| Proc_CFG_WhileTrue:
    "while (b) c' \<turnstile> Label 0 -IEdge (λcf. state_check cf b (Some true))⇣\<surd>->⇣p Label 2"

| Proc_CFG_WhileFalse:
    "while (b) c' \<turnstile> Label 0 -IEdge (λcf. state_check cf b (Some false))⇣\<surd>->⇣p Label 1"

| Proc_CFG_WhileFalseSkip:
  "while (b) c' \<turnstile> Label 1 -IEdge \<Up>id->⇣p Exit"

| Proc_CFG_WhileBody:
  "[|c' \<turnstile> n -et->⇣p n'; n ≠ Entry; n' ≠ Exit|] 
  ==> while (b) c' \<turnstile> n ⊕ 2 -et->⇣p n' ⊕ 2"

| Proc_CFG_WhileBodyExit:
  "[|c' \<turnstile> n -et->⇣p Exit; n ≠ Entry|] ==> while (b) c' \<turnstile> n ⊕ 2 -et->⇣p Label 0"

| Proc_CFG_Call:
  "Call p es rets \<turnstile> Label 0 -CEdge (p,es,rets)->⇣p Label 1"

| Proc_CFG_CallSkip:
  "Call p es rets \<turnstile> Label 1 -IEdge \<Up>id->⇣p Exit"


subsubsection{* Some lemmas about the procedure CFG *}

lemma Proc_CFG_Exit_no_sourcenode [dest]:
  "prog \<turnstile> Exit -et->⇣p n' ==> False"
by(induct prog n≡"Exit" et n' rule:Proc_CFG.induct,auto)


lemma Proc_CFG_Entry_no_targetnode [dest]:
  "prog \<turnstile> n -et->⇣p Entry ==> False"
by(induct prog n et n'≡"Entry" rule:Proc_CFG.induct,auto)


lemma Proc_CFG_IEdge_intra_kind:
  "prog \<turnstile> n -IEdge et->⇣p n' ==> intra_kind et"
by(induct prog n x≡"IEdge et" n' rule:Proc_CFG.induct,auto simp:intra_kind_def)


lemma [dest]:"prog \<turnstile> n -IEdge (Q:r\<hookrightarrow>⇘p⇙fs)->⇣p n' ==> False"
by(fastforce dest:Proc_CFG_IEdge_intra_kind simp:intra_kind_def)

lemma [dest]:"prog \<turnstile> n -IEdge (Q\<hookleftarrow>⇘p⇙f)->⇣p n' ==> False"
by(fastforce dest:Proc_CFG_IEdge_intra_kind simp:intra_kind_def)


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


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


lemma Proc_CFG_EntryD:
  "prog \<turnstile> Entry -et->⇣p n' 
  ==> (n' = Exit ∧ et = IEdge(λs. False)⇣\<surd>) ∨ (n' = Label 0 ∧ et = IEdge (λs. True)⇣\<surd>)"
by(induct prog n≡"Entry" et n' rule:Proc_CFG.induct,auto)


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


text {* Lots of lemmas for call edges @{text "…"} *}

lemma Proc_CFG_Call_Labels:
  "prog \<turnstile> 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 \<turnstile> 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 \<turnstile> n -CEdge (p,es,rets)->⇣p n'; prog \<turnstile> n -IEdge et->⇣p n''|] ==> False"
proof(induct prog n "CEdge (p,es,rets)" n' arbitrary:n'' rule:Proc_CFG.induct)
  case (Proc_CFG_SeqFirst c⇣1 n n' c⇣2)
  note IH = `!!n''. c⇣1 \<turnstile> n -IEdge et->⇣p n'' ==> False`
  from `c⇣1;;c⇣2 \<turnstile> n -IEdge et->⇣p n''` `c⇣1 \<turnstile> n -CEdge (p, es, rets)->⇣p n'` 
    `n' ≠ Exit`
  obtain nx where "c⇣1 \<turnstile> n -IEdge et->⇣p nx"
    apply - apply(erule Proc_CFG.cases)
    apply(auto intro:Proc_CFG_Entry_Exit Proc_CFG_Entry)
    by(case_tac n)(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
  then show ?case by (rule IH)
next
  case (Proc_CFG_SeqConnect c⇣1 n c⇣2)
  from `c⇣1 \<turnstile> n -CEdge (p, es, rets)->⇣p Exit`
  show ?case by(fastforce dest:Proc_CFG_Call_Labels)
next
  case (Proc_CFG_SeqSecond c⇣2 n n' c⇣1)
  note IH = `!!n''. c⇣2 \<turnstile> n -IEdge et->⇣p n'' ==> False`
  from `c⇣1;;c⇣2 \<turnstile> n ⊕ #:c⇣1 -IEdge et->⇣p n''` `c⇣2 \<turnstile> n -CEdge (p, es, rets)->⇣p n'` 
    `n ≠ Entry`
  obtain nx where "c⇣2 \<turnstile> n -IEdge et->⇣p nx"
    apply - apply(erule Proc_CFG.cases,auto)
      apply(cases n) apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
     apply(cases n) apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
    by(cases n,auto,case_tac n,auto)
  then show ?case by (rule IH)
next
  case (Proc_CFG_CondThen c⇣1 n n' b c⇣2)
  note IH = `!!n''. c⇣1 \<turnstile> n -IEdge et->⇣p n'' ==> False`
  from `if (b) c⇣1 else c⇣2 \<turnstile> n ⊕ 1 -IEdge et->⇣p n''` `c⇣1 \<turnstile> n -CEdge (p, es, rets)->⇣p n'`
    `n ≠ Entry`
  obtain nx where "c⇣1 \<turnstile> n -IEdge et->⇣p nx"
    apply - apply(erule Proc_CFG.cases,auto)
     apply(cases n) apply auto apply(case_tac n) apply auto
    apply(cases n) apply auto
    by(case_tac n)(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
  then show ?case by (rule IH)
next
  case (Proc_CFG_CondElse c⇣2 n n' b c⇣1)
  note IH = `!!n''. c⇣2 \<turnstile> n -IEdge et->⇣p n'' ==> False`
  from `if (b) c⇣1 else c⇣2 \<turnstile> n ⊕ #:c⇣1 + 1 -IEdge et->⇣p n''` `c⇣2 \<turnstile> n -CEdge (p, es, rets)->⇣p n'`
    `n ≠ Entry`
  obtain nx where "c⇣2 \<turnstile> n -IEdge et->⇣p nx"
    apply - apply(erule Proc_CFG.cases,auto)
     apply(cases n) apply auto
     apply(case_tac n) apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
    by(cases n,auto,case_tac n,auto)
  then show ?case by (rule IH)
next
  case (Proc_CFG_WhileBody c' n n' b)
  note IH = `!!n''. c' \<turnstile> n -IEdge et->⇣p n'' ==> False`
  from `while (b) c' \<turnstile> n ⊕ 2 -IEdge et->⇣p n''` `c' \<turnstile> n -CEdge (p, es, rets)->⇣p n'`
    `n ≠ Entry` `n' ≠ Exit`
  obtain nx where "c' \<turnstile> n -IEdge et->⇣p nx"
    apply - apply(erule Proc_CFG.cases,auto)
      apply(drule label_incr_ge[OF sym]) apply simp
     apply(cases n) apply auto apply(case_tac n) apply auto
    by(cases n,auto,case_tac n,auto)
  then show ?case by (rule IH)
next
  case (Proc_CFG_WhileBodyExit c' n b)
  from `c' \<turnstile> 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 \<turnstile> Label 0 -IEdge et->⇣p n''`
  show ?case by(fastforce elim:Proc_CFG.cases)
qed


lemma Proc_CFG_Call_Intra_edge_not_same_target:
  "[|prog \<turnstile> n -CEdge (p,es,rets)->⇣p n'; prog \<turnstile> n'' -IEdge et->⇣p n'|] ==> False"
proof(induct prog n "CEdge (p,es,rets)" n' arbitrary:n'' rule:Proc_CFG.induct)
  case (Proc_CFG_SeqFirst c⇣1 n n' c⇣2)
  note IH = `!!n''. c⇣1 \<turnstile> n'' -IEdge et->⇣p n' ==> False`
  from `c⇣1;;c⇣2 \<turnstile> n'' -IEdge et->⇣p n'` `c⇣1 \<turnstile> n -CEdge (p, es, rets)->⇣p n'` 
    `n' ≠ Exit`
  have "c⇣1 \<turnstile> n'' -IEdge et->⇣p n'"
    apply - apply(erule Proc_CFG.cases)
    apply(auto intro:Proc_CFG_Entry dest:Proc_CFG_targetlabel_less_num_nodes) 
    by(case_tac n')(auto dest:Proc_CFG_targetlabel_less_num_nodes)
  then show ?case by (rule IH)
next
  case (Proc_CFG_SeqConnect c⇣1 n c⇣2)
  from `c⇣1 \<turnstile> n -CEdge (p, es, rets)->⇣p Exit`
  show ?case by(fastforce dest:Proc_CFG_Call_Labels)
next
  case (Proc_CFG_SeqSecond c⇣2 n n' c⇣1)
  note IH = `!!n''. c⇣2 \<turnstile> n'' -IEdge et->⇣p n' ==> False`
  from `c⇣1;;c⇣2 \<turnstile> n'' -IEdge et->⇣p n' ⊕ #:c⇣1` `c⇣2 \<turnstile> n -CEdge (p, es, rets)->⇣p n'` 
    `n ≠ Entry`
  obtain nx where "c⇣2 \<turnstile> nx -IEdge et->⇣p n'"
    apply - apply(erule Proc_CFG.cases,auto)
       apply(fastforce intro:Proc_CFG_Entry_Exit)
      apply(cases n') apply(auto dest:Proc_CFG_targetlabel_less_num_nodes)
     apply(cases n') apply(auto dest:Proc_CFG_Call_target_0)
    apply(cases n') apply(auto dest:Proc_CFG_Call_Labels)
    by(case_tac n') auto
  then show ?case by (rule IH)
next
  case (Proc_CFG_CondThen c⇣1 n n' b c⇣2)
  note IH = `!!n''. c⇣1 \<turnstile> n'' -IEdge et->⇣p n' ==> False`
  from `if (b) c⇣1 else c⇣2 \<turnstile> n'' -IEdge et->⇣p n' ⊕ 1` `c⇣1 \<turnstile> n -CEdge (p, es, rets)->⇣p n'`
    `n ≠ Entry`
  obtain nx where "c⇣1 \<turnstile> nx -IEdge et->⇣p n'"
    apply - apply(erule Proc_CFG.cases,auto)
        apply(cases n') apply(auto intro:Proc_CFG_Entry_Exit)
       apply(cases n') apply(auto dest:Proc_CFG_Call_target_0)
      apply(cases n') apply(auto dest:Proc_CFG_targetlabel_less_num_nodes)
     apply(cases n') apply auto apply(case_tac n') apply auto
    apply(cases n') apply auto
    apply(case_tac n') apply(auto dest:Proc_CFG_targetlabel_less_num_nodes)
    by(case_tac n')(auto dest:Proc_CFG_Call_Labels)
  then show ?case by (rule IH)
next
  case (Proc_CFG_CondElse c⇣2 n n' b c⇣1)
  note IH = `!!n''. c⇣2 \<turnstile> n'' -IEdge et->⇣p n' ==> False`
  from `if (b) c⇣1 else c⇣2 \<turnstile> n'' -IEdge et->⇣p n' ⊕ #:c⇣1 + 1` `c⇣2 \<turnstile> n -CEdge (p, es, rets)->⇣p n'`
    `n ≠ Entry`
  obtain nx where "c⇣2 \<turnstile> nx -IEdge et->⇣p n'"
    apply - apply(erule Proc_CFG.cases,auto)
        apply(cases n') apply(auto intro:Proc_CFG_Entry_Exit)
       apply(cases n') apply(auto dest:Proc_CFG_Call_target_0)
      apply(cases n') apply(auto dest:Proc_CFG_Call_target_0)
     apply(cases n') apply auto
      apply(case_tac n') apply(auto dest:Proc_CFG_targetlabel_less_num_nodes)
     apply(case_tac n') apply(auto dest:Proc_CFG_Call_Labels)
    by(cases n',auto,case_tac n',auto)
  then show ?case by (rule IH)
next
  case (Proc_CFG_WhileBody c' n n' b)
  note IH = `!!n''. c' \<turnstile> n'' -IEdge et->⇣p n' ==> False`
  from `while (b) c' \<turnstile> n'' -IEdge et->⇣p n' ⊕ 2` `c' \<turnstile> n -CEdge (p, es, rets)->⇣p n'`
    `n ≠ Entry` `n' ≠ Exit`
  obtain nx where "c' \<turnstile> nx -IEdge et->⇣p n'"
    apply - apply(erule Proc_CFG.cases,auto)
      apply(cases n') apply(auto dest:Proc_CFG_Call_target_0)
     apply(cases n') apply auto
    by(cases n',auto,case_tac n',auto)
  then show ?case by (rule IH)
next
  case (Proc_CFG_WhileBodyExit c' n b)
  from `c' \<turnstile> 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 \<turnstile> n'' -IEdge et->⇣p Label 1`
  show ?case by(fastforce elim:Proc_CFG.cases)
qed


lemma Proc_CFG_Call_nodes_eq:
  "[|prog \<turnstile> n -CEdge (p,es,rets)->⇣p n'; prog \<turnstile> n -CEdge (p',es',rets')->⇣p n''|]
  ==> n' = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'"
proof(induct prog n "CEdge (p,es,rets)" n' arbitrary:n'' rule:Proc_CFG.induct)
  case (Proc_CFG_SeqFirst c⇣1 n n' c⇣2)
  note IH = `!!n''. c⇣1 \<turnstile> n -CEdge (p',es',rets')->⇣p n''
    ==> n' = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'`
  from `c⇣1;; c⇣2 \<turnstile> n -CEdge (p',es',rets')->⇣p n''` `c⇣1 \<turnstile> n -CEdge (p,es,rets)->⇣p n'`
  have "c⇣1 \<turnstile> n -CEdge (p',es',rets')->⇣p n''"
    apply - apply(erule Proc_CFG.cases,auto)
     apply(fastforce dest:Proc_CFG_Call_Labels)
    by(case_tac n,(fastforce dest:Proc_CFG_sourcelabel_less_num_nodes)+)
  then show ?case by (rule IH)
next
  case (Proc_CFG_SeqConnect c⇣1 n c⇣2)
  from `c⇣1 \<turnstile> n -CEdge (p,es,rets)->⇣p Exit` have False
    by(fastforce dest:Proc_CFG_Call_Labels)
  thus ?case by simp
next
  case (Proc_CFG_SeqSecond c⇣2 n n' c⇣1)
  note IH = `!!n''. c⇣2 \<turnstile> n -CEdge (p',es',rets')->⇣p n''
    ==> n' = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'`
  from `c⇣1;;c⇣2 \<turnstile> n ⊕ #:c⇣1 -CEdge (p',es',rets')->⇣p n''` `n ≠ Entry`
  obtain nx where edge:"c⇣2 \<turnstile> n -CEdge (p',es',rets')->⇣p nx" and nx:"nx ⊕ #:c⇣1 = n''"
    apply - apply(erule Proc_CFG.cases,auto)
    by(cases n,auto dest:Proc_CFG_sourcelabel_less_num_nodes label_incr_inj)+
  from edge have "n' = nx ∧ p = p' ∧ es = es' ∧ rets = rets'" by (rule IH)
  with nx show ?case by auto
next
  case (Proc_CFG_CondThen c⇣1 n n' b c⇣2)
  note IH = `!!n''. c⇣1 \<turnstile> n -CEdge (p',es',rets')->⇣p n''
    ==> n' = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'`
  from `if (b) c⇣1 else c⇣2 \<turnstile> n ⊕ 1 -CEdge (p',es',rets')->⇣p n''`
  obtain nx where "c⇣1 \<turnstile> n -CEdge (p',es',rets')->⇣p nx ∧ nx ⊕ 1 = n''"
  proof(rule Proc_CFG.cases)
    fix c⇣2' nx etx nx' bx c⇣1'
    assume "if (b) c⇣1 else c⇣2 = if (bx) c⇣1' else c⇣2'"
      and "n ⊕ 1 = nx ⊕ #:c⇣1' + 1" and "nx ≠ Entry"
    with `c⇣1 \<turnstile> n -CEdge (p,es,rets)->⇣p n'` obtain l where "n = Label l" and "l ≥ #:c⇣1"
      by(cases n,auto,cases nx,auto)
    with `c⇣1 \<turnstile> n -CEdge (p,es,rets)->⇣p n'` have False
      by(fastforce dest:Proc_CFG_sourcelabel_less_num_nodes)
    thus ?thesis by simp
  qed (auto dest:label_incr_inj)
  then obtain nx where edge:"c⇣1 \<turnstile> n -CEdge (p',es',rets')->⇣p nx" 
    and nx:"nx ⊕ 1 = n''" by blast
  from IH[OF edge] nx show ?case by simp
next
  case (Proc_CFG_CondElse c⇣2 n n' b c⇣1)
  note IH = `!!n''. c⇣2 \<turnstile> n -CEdge (p',es',rets')->⇣p n''
    ==> n' = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'`
  from `if (b) c⇣1 else c⇣2 \<turnstile> n ⊕ #:c⇣1 + 1 -CEdge (p',es',rets')->⇣p n''`
  obtain nx where "c⇣2 \<turnstile> n -CEdge (p',es',rets')->⇣p nx ∧ nx ⊕ #:c⇣1 + 1 = n''"
  proof(rule Proc_CFG.cases)
    fix c⇣1' nx etx nx' bx c⇣2'
    assume ifs:"if (b) c⇣1 else c⇣2 = if (bx) c⇣1' else c⇣2'"
      and "n ⊕ #:c⇣1 + 1 = nx ⊕ 1" and "nx ≠ Entry"
      and edge:"c⇣1' \<turnstile> nx -etx->⇣p nx'"
    then obtain l where "nx = Label l" and "l ≥ #:c⇣1"
      by(cases n,auto,cases nx,auto)
    with edge ifs have False
      by(fastforce dest:Proc_CFG_sourcelabel_less_num_nodes)
    thus ?thesis by simp
  qed (auto dest:label_incr_inj)
  then obtain nx where edge:"c⇣2 \<turnstile> n -CEdge (p',es',rets')->⇣p nx"
    and nx:"nx ⊕ #:c⇣1 + 1 = n''"
    by blast
  from IH[OF edge] nx show ?case by simp
next
  case (Proc_CFG_WhileBody c' n n' b)
  note IH = `!!n''. c' \<turnstile> n -CEdge (p',es',rets')->⇣p n''
    ==> n' = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'`
  from `while (b) c' \<turnstile> n ⊕ 2 -CEdge (p',es',rets')->⇣p n''`
  obtain nx where "c' \<turnstile> 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' \<turnstile> 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' \<turnstile> 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 \<turnstile> 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 \<turnstile> n -CEdge (p,es,rets)->⇣p n'; prog \<turnstile> n'' -CEdge (p',es',rets')->⇣p n'|]
  ==> n = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'"
proof(induct prog n "CEdge (p,es,rets)" n' arbitrary:n'' rule:Proc_CFG.induct)
  case (Proc_CFG_SeqFirst c⇣1 n n' c⇣2)
  note IH = `!!n''. c⇣1 \<turnstile> n'' -CEdge (p',es',rets')->⇣p n'
    ==> n = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'`
  from `c⇣1;;c⇣2 \<turnstile> n'' -CEdge (p',es',rets')->⇣p n'` `c⇣1 \<turnstile> n -CEdge (p,es,rets)->⇣p n'`
  have "c⇣1 \<turnstile> n'' -CEdge (p',es',rets')->⇣p n'"
    apply - apply(erule Proc_CFG.cases,auto)
     apply(fastforce dest:Proc_CFG_Call_Labels)
    by(case_tac n',auto dest:Proc_CFG_targetlabel_less_num_nodes Proc_CFG_Call_Labels)
  then show ?case by (rule IH)
next
  case (Proc_CFG_SeqConnect c⇣1 n c⇣2)
  from `c⇣1 \<turnstile> n -CEdge (p,es,rets)->⇣p Exit` have False
    by(fastforce dest:Proc_CFG_Call_Labels)
  thus ?case by simp
next
  case (Proc_CFG_SeqSecond c⇣2 n n' c⇣1)
  note IH = `!!n''. c⇣2 \<turnstile> n'' -CEdge (p',es',rets')->⇣p n'
    ==> n = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'`
  from `c⇣1;;c⇣2 \<turnstile> n'' -CEdge (p',es',rets')->⇣p n' ⊕ #:c⇣1`
  obtain nx where edge:"c⇣2 \<turnstile> nx -CEdge (p',es',rets')->⇣p n'" and nx:"nx ⊕ #:c⇣1 = n''"
    apply - apply(erule Proc_CFG.cases,auto)
    by(cases n',
       auto dest:Proc_CFG_targetlabel_less_num_nodes Proc_CFG_Call_Labels 
                 label_incr_inj)
  from edge have "n = nx ∧ p = p' ∧ es = es' ∧ rets = rets'" by (rule IH)
  with nx show ?case by auto
next
  case (Proc_CFG_CondThen c⇣1 n n' b c⇣2)
  note IH = `!!n''. c⇣1 \<turnstile> n'' -CEdge (p',es',rets')->⇣p n'
    ==> n = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'`
  from `if (b) c⇣1 else c⇣2 \<turnstile> n'' -CEdge (p',es',rets')->⇣p n' ⊕ 1`
  obtain nx where "c⇣1 \<turnstile> nx -CEdge (p',es',rets')->⇣p n' ∧ nx ⊕ 1 = n''"
  proof(cases)
    case (Proc_CFG_CondElse nx nx')
    from `n' ⊕ 1 = nx' ⊕ #:c⇣1 + 1`
      `c⇣1 \<turnstile> n -CEdge (p,es,rets)->⇣p n'`
    obtain l where "n' = Label l" and "l ≥ #:c⇣1"
      by(cases n', auto dest:Proc_CFG_Call_Labels,cases nx',auto)
    with `c⇣1 \<turnstile> n -CEdge (p,es,rets)->⇣p n'` have False
      by(fastforce dest:Proc_CFG_targetlabel_less_num_nodes)
    thus ?thesis by simp
  qed (auto dest:label_incr_inj)
  then obtain nx where edge:"c⇣1 \<turnstile> nx -CEdge (p',es',rets')->⇣p n'" 
    and nx:"nx ⊕ 1 = n''"
    by blast
  from IH[OF edge] nx show ?case by simp
next
  case (Proc_CFG_CondElse c⇣2 n n' b c⇣1)
  note IH = `!!n''. c⇣2 \<turnstile> n'' -CEdge (p',es',rets')->⇣p n'
    ==> n = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'`
  from `if (b) c⇣1 else c⇣2 \<turnstile> n'' -CEdge (p',es',rets')->⇣p n' ⊕ #:c⇣1 + 1`
  obtain nx where "c⇣2 \<turnstile> nx -CEdge (p',es',rets')->⇣p n' ∧ nx ⊕ #:c⇣1 + 1 = n''"
  proof(cases)
    case (Proc_CFG_CondThen nx nx')
    from `n' ⊕ #:c⇣1 + 1 = nx' ⊕ 1`
      `c⇣1 \<turnstile> nx -CEdge (p',es',rets')->⇣p nx'`
    obtain l where "nx' = Label l" and "l ≥ #:c⇣1"
      by(cases n',auto,cases nx',auto dest:Proc_CFG_Call_Labels)
    with `c⇣1 \<turnstile> nx -CEdge (p',es',rets')->⇣p nx'`
    have False by(fastforce dest:Proc_CFG_targetlabel_less_num_nodes)
    thus ?thesis by simp
  qed (auto dest:label_incr_inj)
  then obtain nx where edge:"c⇣2 \<turnstile> nx -CEdge (p',es',rets')->⇣p n'" 
    and nx:"nx ⊕ #:c⇣1 + 1 = n''"
    by blast
  from IH[OF edge] nx show ?case by simp
next
  case (Proc_CFG_WhileBody c' n n' b)
  note IH = `!!n''. c' \<turnstile> n'' -CEdge (p',es',rets')->⇣p n'
    ==> n = n'' ∧ p = p' ∧ es = es' ∧ rets = rets'`
  from `while (b) c' \<turnstile> n'' -CEdge (p',es',rets')->⇣p n' ⊕ 2`
  obtain nx where edge:"c' \<turnstile> 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' \<turnstile> 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 \<turnstile> 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 \<turnstile> n -CEdge (p,es,rets)->⇣p n'; prog \<turnstile> n' -CEdge (p',es',rets')->⇣p n''|] 
  ==> False"
proof(induct prog n "CEdge (p,es,rets)" n' arbitrary:n'' rule:Proc_CFG.induct)
  case (Proc_CFG_SeqFirst c⇣1 n n' c⇣2)
  note IH = `!!n''. c⇣1 \<turnstile> n' -CEdge (p', es', rets')->⇣p n'' ==> False`
  from `c⇣1;; c⇣2 \<turnstile> n' -CEdge (p',es',rets')->⇣p n''` `c⇣1 \<turnstile> n -CEdge (p,es,rets)->⇣p n'`
  have "c⇣1 \<turnstile> n' -CEdge (p',es',rets')->⇣p n''"
    apply - apply(erule Proc_CFG.cases,auto)
     apply(fastforce dest:Proc_CFG_Call_Labels)
    by(case_tac n)(auto dest:Proc_CFG_targetlabel_less_num_nodes)
  then show ?case by (rule IH)
next
  case (Proc_CFG_SeqConnect c⇣1 n c⇣2)
  from `c⇣1 \<turnstile> n -CEdge (p,es,rets)->⇣p Exit` have False
    by(fastforce dest:Proc_CFG_Call_Labels)
  thus ?case by simp
next
  case (Proc_CFG_SeqSecond c⇣2 n n' c⇣1)
  note IH = `!!n''. c⇣2 \<turnstile> n' -CEdge (p', es', rets')->⇣p n'' ==> False`
  from `c⇣1;; c⇣2 \<turnstile> n' ⊕ #:c⇣1 -CEdge (p', es', rets')->⇣p n''` `c⇣2 \<turnstile> n -CEdge (p,es,rets)->⇣p n'`
  obtain nx where "c⇣2 \<turnstile> n' -CEdge (p',es',rets')->⇣p nx"
    apply - apply(erule Proc_CFG.cases,auto)
      apply(cases n') apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
     apply(fastforce dest:Proc_CFG_Call_Labels)
    by(cases n',auto,case_tac n,auto)
  then show ?case by (rule IH)
next
  case (Proc_CFG_CondThen c⇣1 n n' b c⇣2)
  note IH = `!!n''. c⇣1 \<turnstile> n' -CEdge (p',es',rets')->⇣p n'' ==> False`
  from `if (b) c⇣1 else c⇣2 \<turnstile> n' ⊕ 1 -CEdge (p', es', rets')->⇣p n''` `c⇣1 \<turnstile> n -CEdge (p,es,rets)->⇣p n'`
  obtain nx where "c⇣1 \<turnstile> n' -CEdge (p',es',rets')->⇣p nx"
    apply - apply(erule Proc_CFG.cases,auto)
     apply(cases n') apply auto apply(case_tac n) apply auto
    apply(cases n') apply auto
    by(case_tac n)(auto dest:Proc_CFG_targetlabel_less_num_nodes)
  then show ?case by (rule IH)
next
  case (Proc_CFG_CondElse c⇣2 n n' b c⇣1)
  note IH = `!!n''. c⇣2 \<turnstile> n' -CEdge (p',es',rets')->⇣p n'' ==> False`
  from `if (b) c⇣1 else c⇣2 \<turnstile> n' ⊕ #:c⇣1 + 1 -CEdge (p', es', rets')->⇣p n''` 
    `c⇣2 \<turnstile> n -CEdge (p,es,rets)->⇣p n'`
  obtain nx where "c⇣2 \<turnstile> 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' \<turnstile> n' -CEdge (p',es',rets')->⇣p n'' ==> False`
  from `while (b) c' \<turnstile> n' ⊕ 2 -CEdge (p', es', rets')->⇣p n''` `c' \<turnstile> n -CEdge (p,es,rets)->⇣p n'`
  obtain nx where "c' \<turnstile> 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' \<turnstile> 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 \<turnstile> 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 \<turnstile> n -CEdge (p,es,rets)->⇣p n'; prog \<turnstile> n' -IEdge et->⇣p n''|] ==> et = \<Up>id"
proof(induct prog n "CEdge (p,es,rets)" n' arbitrary:n'' rule:Proc_CFG.induct)
  case (Proc_CFG_SeqFirst c⇣1 n n' c⇣2)
  note IH = `!!n''. c⇣1 \<turnstile> n' -IEdge et->⇣p n'' ==> et = \<Up>id`
  from `c⇣1;;c⇣2 \<turnstile> n' -IEdge et->⇣p n''` `c⇣1 \<turnstile> n -CEdge (p,es,rets)->⇣p n'` `n' ≠ Exit`
  obtain nx where "c⇣1 \<turnstile> n' -IEdge et->⇣p nx"
    apply - apply(erule Proc_CFG.cases,auto)
    by(case_tac n)(auto dest:Proc_CFG_targetlabel_less_num_nodes)
  then show ?case by (rule IH)
next
  case (Proc_CFG_SeqConnect c⇣1 n c⇣2)
  from `c⇣1 \<turnstile> n -CEdge (p, es, rets)->⇣p Exit`
  show ?case by(fastforce dest:Proc_CFG_Call_Labels)
next
  case (Proc_CFG_SeqSecond c⇣2 n n' c⇣1)
  note IH = `!!n''. c⇣2 \<turnstile> n' -IEdge et->⇣p n'' ==> et = \<Up>id`
  from `c⇣1;;c⇣2 \<turnstile> n' ⊕ #:c⇣1 -IEdge et->⇣p n''` `c⇣2 \<turnstile> n -CEdge (p,es,rets)->⇣p n'`
  obtain nx where "c⇣2 \<turnstile> n' -IEdge et->⇣p nx"
    apply - apply(erule Proc_CFG.cases,auto)
      apply(cases n') apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
     apply(cases n') apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
    by(cases n',auto,case_tac n,auto)
  then show ?case by (rule IH)
next
  case (Proc_CFG_CondThen c⇣1 n n' b c⇣2)
  note IH = `!!n''. c⇣1 \<turnstile> n' -IEdge et->⇣p n'' ==> et = \<Up>id`
  from `if (b) c⇣1 else c⇣2 \<turnstile> n' ⊕ 1 -IEdge et->⇣p n''` `c⇣1 \<turnstile> n -CEdge (p,es,rets)->⇣p n'`
    `n ≠ Entry`
  obtain nx where "c⇣1 \<turnstile> n' -IEdge et->⇣p nx"
    apply - apply(erule Proc_CFG.cases,auto)
     apply(cases n') apply auto apply(case_tac n) apply auto
    apply(cases n') apply auto
    by(case_tac n)(auto dest:Proc_CFG_targetlabel_less_num_nodes)
  then show ?case by (rule IH)
next
  case (Proc_CFG_CondElse c⇣2 n n' b c⇣1)
  note IH = `!!n''. c⇣2 \<turnstile> n' -IEdge et->⇣p n'' ==> et = \<Up>id`
  from `if (b) c⇣1 else c⇣2 \<turnstile> n' ⊕ #:c⇣1 + 1 -IEdge et->⇣p n''` `c⇣2 \<turnstile> n -CEdge (p,es,rets)->⇣p n'`
  obtain nx where "c⇣2 \<turnstile> n' -IEdge et->⇣p nx"
    apply - apply(erule Proc_CFG.cases,auto)
     apply(cases n') apply auto
     apply(case_tac n) apply(auto dest:Proc_CFG_sourcelabel_less_num_nodes)
    by(cases n',auto,case_tac n,auto)
  then show ?case by (rule IH)
next
  case (Proc_CFG_WhileBody c' n n' b)
  note IH = `!!n''. c' \<turnstile> n' -IEdge et->⇣p n'' ==> et = \<Up>id`
  from `while (b) c' \<turnstile> n' ⊕ 2 -IEdge et->⇣p n''` `c' \<turnstile> n -CEdge (p,es,rets)->⇣p n'`
  obtain nx where "c' \<turnstile> n' -IEdge et->⇣p nx"
    apply - apply(erule Proc_CFG.cases,auto)
      apply(cases n') apply auto
     apply(cases n') apply auto apply(case_tac n) apply auto
    by(cases n',auto,case_tac n,auto)
  then show ?case by (rule IH)
next
  case (Proc_CFG_WhileBodyExit c' n et' b)
  from `c' \<turnstile> 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 \<turnstile> Label 1 -IEdge et->⇣p n''` show ?case
    by(fastforce elim:Proc_CFG.cases)
qed


lemma Proc_CFG_edge_det:
  "[|prog \<turnstile> n -et->⇣p n'; prog \<turnstile> n -et'->⇣p n'|] ==> et = et'"
proof(induct rule:Proc_CFG.induct)
  case Proc_CFG_Entry_Exit thus ?case by(fastforce dest:Proc_CFG_EntryD)
next
  case Proc_CFG_Entry thus ?case by(fastforce dest:Proc_CFG_EntryD)
next
  case Proc_CFG_Skip thus ?case by(fastforce elim:Proc_CFG.cases)
next
  case Proc_CFG_LAss thus ?case by(fastforce elim:Proc_CFG.cases)
next
  case Proc_CFG_LAssSkip thus ?case by(fastforce elim:Proc_CFG.cases)
next
  case (Proc_CFG_SeqFirst c⇣1 n et n' c⇣2)
  note edge = `c⇣1 \<turnstile> n -et->⇣p n'` 
  note IH = `c⇣1 \<turnstile> n -et'->⇣p n' ==> et = et'`
  from edge `n' ≠ Exit` obtain l where l:"n' = Label l" by (cases n') auto
  with edge have "l < #:c⇣1" by(fastforce intro:Proc_CFG_targetlabel_less_num_nodes)
  with `c⇣1;;c⇣2 \<turnstile> n -et'->⇣p n'` l have "c⇣1 \<turnstile> n -et'->⇣p n'"
    by(fastforce elim:Proc_CFG.cases intro:Proc_CFG.intros dest:label_incr_ge)
  from IH[OF this] show ?case .
next
  case (Proc_CFG_SeqConnect c⇣1 n et c⇣2)
  note edge = `c⇣1 \<turnstile> n -et->⇣p Exit`
  note IH = `c⇣1 \<turnstile> n -et'->⇣p Exit ==> et = et'`
  from edge `n ≠ Entry` obtain l where l:"n = Label l" by (cases n) auto
  with edge have "l < #:c⇣1" by(fastforce intro: Proc_CFG_sourcelabel_less_num_nodes)
  with `c⇣1;;c⇣2 \<turnstile> n -et'->⇣p Label #:c⇣1` l have "c⇣1 \<turnstile> n -et'->⇣p Exit"
    by(fastforce elim:Proc_CFG.cases 
                dest:Proc_CFG_targetlabel_less_num_nodes label_incr_ge)
  from IH[OF this] show ?case .
next
  case (Proc_CFG_SeqSecond c⇣2 n et n' c⇣1)
  note edge = `c⇣2 \<turnstile> n -et->⇣p n'` 
  note IH = `c⇣2 \<turnstile> n -et'->⇣p n' ==> et = et'`
  from edge `n ≠ Entry` obtain l where l:"n = Label l" by (cases n) auto
  with edge have "l < #:c⇣2" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
  with `c⇣1;;c⇣2 \<turnstile> n ⊕ #:c⇣1 -et'->⇣p n' ⊕ #:c⇣1` l have "c⇣2 \<turnstile> n -et'->⇣p n'"
    by -(erule Proc_CFG.cases,
    (fastforce dest:Proc_CFG_sourcelabel_less_num_nodes label_incr_ge
              dest!:label_incr_inj)+)
  from IH[OF this] show ?case .
next
  case Proc_CFG_CondTrue thus ?case by(fastforce elim:Proc_CFG.cases)
next
  case Proc_CFG_CondFalse thus ?case by(fastforce elim:Proc_CFG.cases)
next
  case (Proc_CFG_CondThen c⇣1 n et n' b c⇣2)
  note edge = `c⇣1 \<turnstile> n -et->⇣p n'`
  note IH = `c⇣1 \<turnstile> n -et'->⇣p n' ==> et = et'`
  from edge `n ≠ Entry` obtain l where l:"n = Label l" by (cases n) auto
  with edge have "l < #:c⇣1" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
  with `if (b) c⇣1 else c⇣2 \<turnstile> n ⊕ 1 -et'->⇣p n' ⊕ 1` l have "c⇣1 \<turnstile> n -et'->⇣p n'"
    by -(erule Proc_CFG.cases,(fastforce dest:label_incr_ge label_incr_inj)+)
  from IH[OF this] show ?case .
next
  case (Proc_CFG_CondElse c⇣2 n et n' b c⇣1)
  note edge = `c⇣2 \<turnstile> n -et->⇣p n'`
  note IH = `c⇣2 \<turnstile> n -et'->⇣p n' ==> et = et'`
  from edge `n ≠ Entry` obtain l where l:"n = Label l" by (cases n) auto
  with edge have "l < #:c⇣2" by(fastforce intro:Proc_CFG_sourcelabel_less_num_nodes)
  with `if (b) c⇣1 else c⇣2 \<turnstile> n ⊕ (#:c⇣1 + 1) -et'->⇣p n' ⊕ (#:c⇣1 + 1)` l 
  have "c⇣2 \<turnstile> 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' \<turnstile> n -et->⇣p n'`
  note IH = `c' \<turnstile> 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' \<turnstile> n ⊕ 2 -et'->⇣p n' ⊕ 2` l less l' have "c' \<turnstile> 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' \<turnstile> n -et->⇣p Exit`
  note IH = `c' \<turnstile> 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' \<turnstile> n ⊕ 2 -et'->⇣p Label 0` l have "c' \<turnstile> 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 \<turnstile> n⇣1 -et⇣1->⇣p n⇣1'; prog \<turnstile> n⇣2 -et⇣2->⇣p n⇣2'; n⇣1 = n⇣2; n⇣1' ≠ n⇣2'|]
  ==> ∃Q Q'. et⇣1 = IEdge (Q)⇣\<surd> ∧ et⇣2 = IEdge (Q')⇣\<surd> ∧ 
            (∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s))"
proof(induct arbitrary:n⇣2 n⇣2' rule:Proc_CFG.induct)
  case (Proc_CFG_Entry_Exit prog)
  from `prog \<turnstile> n⇣2 -et⇣2->⇣p n⇣2'` `Entry = n⇣2` `Exit ≠ n⇣2'`
  have "et⇣2 = IEdge (λs. True)⇣\<surd>" by(fastforce dest:Proc_CFG_EntryD)
  thus ?case by simp
next
  case (Proc_CFG_Entry prog)
  from `prog \<turnstile> n⇣2 -et⇣2->⇣p n⇣2'` `Entry = n⇣2` `Label 0 ≠ n⇣2'`
  have "et⇣2 = IEdge (λs. False)⇣\<surd>" by(fastforce dest:Proc_CFG_EntryD)
  thus ?case by simp
next
  case Proc_CFG_Skip
  from `Skip \<turnstile> n⇣2 -et⇣2->⇣p n⇣2'` `Label 0 = n⇣2` `Exit ≠ n⇣2'`
  have False by(fastforce elim:Proc_CFG.cases)
  thus ?case by simp
next
  case (Proc_CFG_LAss V e)
  from `V:=e \<turnstile> n⇣2 -et⇣2->⇣p n⇣2'` `Label 0 = n⇣2` `Label 1 ≠ n⇣2'`
  have False by -(erule Proc_CFG.cases,auto)
  thus ?case by simp
next
  case (Proc_CFG_LAssSkip V e)
  from `V:=e \<turnstile> n⇣2 -et⇣2->⇣p n⇣2'` `Label 1 = n⇣2` `Exit ≠ n⇣2'`
  have False by -(erule Proc_CFG.cases,auto)
  thus ?case by simp
next
  case (Proc_CFG_SeqFirst c⇣1 n et n' c⇣2)
  note IH = `!!n⇣2 n⇣2'. [|c⇣1 \<turnstile> n⇣2 -et⇣2->⇣p n⇣2'; n = n⇣2; n' ≠ n⇣2'|]
  ==> ∃Q Q'. et = IEdge (Q)⇣\<surd> ∧ et⇣2 = IEdge (Q')⇣\<surd> ∧ 
            (∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s))`
  from `c⇣1;;c⇣2 \<turnstile> n⇣2 -et⇣2->⇣p n⇣2'` `c⇣1 \<turnstile> n -et->⇣p n'` `n = n⇣2` `n' ≠ n⇣2'`
  have "c⇣1 \<turnstile> n⇣2 -et⇣2->⇣p n⇣2' ∨ (c⇣1 \<turnstile> n⇣2 -et⇣2->⇣p Exit ∧ n⇣2' = Label #:c⇣1)"
    apply - apply(erule Proc_CFG.cases)
    apply(auto intro:Proc_CFG.intros)
    by(case_tac n,auto dest:Proc_CFG_sourcelabel_less_num_nodes)+
  thus ?case
  proof
    assume "c⇣1 \<turnstile> n⇣2 -et⇣2->⇣p n⇣2'"
    from IH[OF this `n = n⇣2` `n' ≠ n⇣2'`] show ?case .
  next
    assume "c⇣1 \<turnstile> n⇣2 -et⇣2->⇣p Exit ∧ n⇣2' = Label #:c⇣1"
    hence edge:"c⇣1 \<turnstile> n⇣2 -et⇣2->⇣p Exit" and n2':"n⇣2' = Label #:c⇣1" by simp_all
    from IH[OF edge `n = n⇣2` `n' ≠ Exit`] show ?case .
  qed
next
  case (Proc_CFG_SeqConnect c⇣1 n et c⇣2)
  note IH = `!!n⇣2 n⇣2'. [|c⇣1 \<turnstile> n⇣2 -et⇣2->⇣p n⇣2'; n = n⇣2; Exit ≠ n⇣2'|]
  ==> ∃Q Q'. et = IEdge (Q)⇣\<surd> ∧ et⇣2 = IEdge (Q')⇣\<surd> ∧ 
            (∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s))`
  from `c⇣1;;c⇣2 \<turnstile> n⇣2 -et⇣2->⇣p n⇣2'` `c⇣1 \<turnstile> n -et->⇣p Exit` `n = n⇣2` `n ≠ Entry`
    `Label #:c⇣1 ≠ n⇣2'` have "c⇣1 \<turnstile> n⇣2 -et⇣2->⇣p n⇣2' ∧ Exit ≠ n⇣2'"
    apply - apply(erule Proc_CFG.cases)
    apply(auto intro:Proc_CFG.intros)
    by(case_tac n,auto dest:Proc_CFG_sourcelabel_less_num_nodes)+
  from IH[OF this[THEN conjunct1] `n = n⇣2` this[THEN conjunct2]]
  show ?case .
next
  case (Proc_CFG_SeqSecond c⇣2 n et n' c⇣1)
  note IH = `!!n⇣2 n⇣2'. [|c⇣2 \<turnstile> n⇣2 -et⇣2->⇣p n⇣2'; n = n⇣2; n' ≠ n⇣2'|]
  ==> ∃Q Q'. et = IEdge (Q)⇣\<surd> ∧ et⇣2 = IEdge (Q')⇣\<surd> ∧ 
            (∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s))`
  from `c⇣1;;c⇣2 \<turnstile> n⇣2 -et⇣2->⇣p n⇣2'` `c⇣2 \<turnstile> n -et->⇣p n'` `n ⊕ #:c⇣1 = n⇣2`
    `n' ⊕ #:c⇣1 ≠ n⇣2'` `n ≠ Entry`
  obtain nx where "c⇣2 \<turnstile> n -et⇣2->⇣p nx ∧ nx ⊕ #:c⇣1 = n⇣2'"
    apply - apply(erule Proc_CFG.cases)
    apply(auto intro:Proc_CFG.intros)
      apply(cases n,auto dest:Proc_CFG_sourcelabel_less_num_nodes)
     apply(cases n,auto dest:Proc_CFG_sourcelabel_less_num_nodes)
    by(fastforce dest:label_incr_inj)
  with `n' ⊕ #:c⇣1 ≠ n⇣2'` have edge:"c⇣2 \<turnstile> n -et⇣2->⇣p nx" and neq:"n' ≠ nx"
    by auto
  from IH[OF edge _ neq] show ?case by simp
next
  case (Proc_CFG_CondTrue b c⇣1 c⇣2)
  from `if (b) c⇣1 else c⇣2 \<turnstile> n⇣2 -et⇣2->⇣p n⇣2'` `Label 0 = n⇣2` `Label 1 ≠ n⇣2'`
  show ?case by -(erule Proc_CFG.cases,auto)
next
  case (Proc_CFG_CondFalse b c⇣1 c⇣2)
  from `if (b) c⇣1 else c⇣2 \<turnstile> n⇣2 -et⇣2->⇣p n⇣2'` `Label 0 = n⇣2` `Label (#:c⇣1 + 1) ≠ n⇣2'`
  show ?case by -(erule Proc_CFG.cases,auto)
next
  case (Proc_CFG_CondThen c⇣1 n et n' b c⇣2)
  note IH = `!!n⇣2 n⇣2'. [|c⇣1 \<turnstile> n⇣2 -et⇣2->⇣p n⇣2'; n = n⇣2; n' ≠ n⇣2'|]
    ==> ∃Q Q'. et = IEdge (Q)⇣\<surd> ∧ et⇣2 = IEdge (Q')⇣\<surd> ∧ 
              (∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s))`
  from `if (b) c⇣1 else c⇣2 \<turnstile> n⇣2 -et⇣2->⇣p n⇣2'` `c⇣1 \<turnstile> n -et->⇣p n'` `n ≠ Entry` 
    `n ⊕ 1 = n⇣2` `n' ⊕ 1 ≠ n⇣2'`
  obtain nx where "c⇣1 \<turnstile> n -et⇣2->⇣p nx ∧ n' ≠ nx"
    apply - apply(erule Proc_CFG.cases)
    apply(auto intro:Proc_CFG.intros simp del:One_nat_def)
     apply(drule label_incr_inj) apply(auto simp del:One_nat_def)
    apply(drule label_incr_simp_rev[OF sym])
    by(case_tac na,auto dest:Proc_CFG_sourcelabel_less_num_nodes)
  from IH[OF this[THEN conjunct1] _ this[THEN conjunct2]] show ?case by simp
next
  case (Proc_CFG_CondElse c⇣2 n et n' b c⇣1)
  note IH = `!!n⇣2 n⇣2'. [|c⇣2 \<turnstile> n⇣2 -et⇣2->⇣p n⇣2'; n = n⇣2; n' ≠ n⇣2'|]
    ==> ∃Q Q'. et = IEdge (Q)⇣\<surd> ∧ et⇣2 = IEdge (Q')⇣\<surd> ∧ 
              (∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s))`
  from `if (b) c⇣1 else c⇣2 \<turnstile> n⇣2 -et⇣2->⇣p n⇣2'` `c⇣2 \<turnstile> n -et->⇣p n'` `n ≠ Entry` 
    `n ⊕ #:c⇣1 + 1 = n⇣2` `n' ⊕ #:c⇣1 + 1 ≠ n⇣2'`
  obtain nx where "c⇣2 \<turnstile> n -et⇣2->⇣p nx ∧ n' ≠ nx"
    apply - apply(erule Proc_CFG.cases)
    apply(auto intro:Proc_CFG.intros simp del:One_nat_def)
     apply(drule label_incr_simp_rev)
     apply(case_tac na,auto,cases n,auto dest:Proc_CFG_sourcelabel_less_num_nodes)
    by(fastforce dest:label_incr_inj)
  from IH[OF this[THEN conjunct1] _ this[THEN conjunct2]] show ?case by simp
next
  case (Proc_CFG_WhileTrue b c')
  from `while (b) c' \<turnstile> n⇣2 -et⇣2->⇣p n⇣2'` `Label 0 = n⇣2` `Label 2 ≠ n⇣2'`
  show ?case by -(erule Proc_CFG.cases,auto)
next
  case (Proc_CFG_WhileFalse b c')
  from `while (b) c' \<turnstile> n⇣2 -et⇣2->⇣p n⇣2'` `Label 0 = n⇣2` `Label 1 ≠ n⇣2'`
  show ?case by -(erule Proc_CFG.cases,auto)
next
  case (Proc_CFG_WhileFalseSkip b c')
  from `while (b) c' \<turnstile> n⇣2 -et⇣2->⇣p n⇣2'` `Label 1 = n⇣2` `Exit ≠ n⇣2'`
  show ?case by -(erule Proc_CFG.cases,auto dest:label_incr_ge)
next
  case (Proc_CFG_WhileBody c' n et n' b)
  note IH = `!!n⇣2 n⇣2'. [|c' \<turnstile> n⇣2 -et⇣2->⇣p n⇣2'; n = n⇣2; n' ≠ n⇣2'|]
    ==> ∃Q Q'. et = IEdge (Q)⇣\<surd> ∧ et⇣2 = IEdge (Q')⇣\<surd> ∧ 
              (∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s))`
  from `while (b) c' \<turnstile> n⇣2 -et⇣2->⇣p n⇣2'` `c' \<turnstile> n -et->⇣p n'` `n ≠ Entry`
    `n' ≠ Exit` `n ⊕ 2 = n⇣2` `n' ⊕ 2 ≠ n⇣2'`
  obtain nx where "c' \<turnstile> n -et⇣2->⇣p nx ∧ n' ≠ nx"
    apply - apply(erule Proc_CFG.cases)
    apply(auto intro:Proc_CFG.intros)
      apply(fastforce dest:label_incr_ge[OF sym])
     apply(fastforce dest:label_incr_inj)
    by(fastforce dest:label_incr_inj)
  from IH[OF this[THEN conjunct1] _ this[THEN conjunct2]] show ?case by simp
next
  case (Proc_CFG_WhileBodyExit c' n et b)
  note IH = `!!n⇣2 n⇣2'. [|c' \<turnstile> n⇣2 -et⇣2->⇣p n⇣2'; n = n⇣2; Exit ≠ n⇣2'|]
    ==> ∃Q Q'. et = IEdge (Q)⇣\<surd> ∧ et⇣2 = IEdge (Q')⇣\<surd> ∧ 
              (∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s))`
  from `while (b) c' \<turnstile> n⇣2 -et⇣2->⇣p n⇣2'` `c' \<turnstile> n -et->⇣p Exit` `n ≠ Entry`
    `n ⊕ 2 = n⇣2` `Label 0 ≠ n⇣2'`
  obtain nx where "c' \<turnstile> n -et⇣2->⇣p nx ∧ Exit ≠ nx"
    apply - apply(erule Proc_CFG.cases)
    apply(auto intro:Proc_CFG.intros)
     apply(fastforce dest:label_incr_ge[OF sym])
    by(fastforce dest:label_incr_inj)
  from IH[OF this[THEN conjunct1] _ this[THEN conjunct2]] show ?case by simp
next
  case Proc_CFG_Call thus ?case by -(erule Proc_CFG.cases,auto)
next
  case Proc_CFG_CallSkip thus ?case by -(erule Proc_CFG.cases,auto)
qed


subsection {* And now: the interprocedural CFG *}

subsubsection {* Statements containing calls *}

text {* A procedure is a tuple composed of its name, its input and output variables
  and its method body *}

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


text {* @{text "containsCall"} guarantees that a call to procedure p is in
  a certain statement. *}

declare conj_cong[fundef_cong]

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


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


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



lemma containsCallE:
  "[|containsCall procs prog ps p; 
    [|ps = []; containsCall procs prog ps p|] ==> P procs prog ps p;
    !!q ins outs c es' rets' ps'. [|ps = ps'@[q]; (q,ins,outs,c) ∈ set procs; 
      containsCall procs c [] p; containsCall procs prog ps' q|] 
     ==> P procs prog ps p|] ==> P procs prog ps p"
  by(auto dest:containsCallcases)


lemma containsCall_in_proc: 
  "[|containsCall procs prog qs q; (q,ins,outs,c) ∈ set procs; 
  containsCall procs c [] p|]
  ==> containsCall procs prog (qs@[q]) p"
proof(induct procs prog qs q rule:containsCall_induct)
  case (Call procs qx esx retsx ps p')
  note IH = `!!x y z psx. [|ps = qx#psx; (qx,x,y,z) ∈ set procs;
    containsCall procs z psx p'; (p',ins,outs,c) ∈ set procs; 
    containsCall procs c [] p|] ==> containsCall procs z (psx@[p']) p`
  from `containsCall procs (Call qx esx retsx) ps p'`
  have "p' = qx ∧ ps = [] ∨
    (∃insx outsx cx psx. ps = qx#psx ∧ (qx,insx,outsx,cx) ∈ set procs ∧
    containsCall procs cx psx p')" by simp
  thus ?case
  proof
    assume assms:"p' = qx ∧ ps = []"
    with `(p', ins, outs, c) ∈ set procs` `containsCall procs c [] p`
    have "containsCall procs (Call qx esx retsx) [p'] p" by fastforce
    with assms show ?thesis by simp
  next
    assume "∃insx outsx cx psx. ps = qx#psx ∧ (qx,insx,outsx,cx) ∈ set procs ∧
      containsCall procs cx psx p'"
    then obtain insx outsx cx psx where "ps = qx#psx" 
      and "(qx,insx,outsx,cx) ∈ set procs"
      and "containsCall procs cx psx p'" by blast
    from IH[OF this `(p', ins, outs, c) ∈ set procs` 
      `containsCall procs c [] p`] 
    have "containsCall procs cx (psx @ [p']) p" .
    with `ps = qx#psx` `(qx,insx,outsx,cx) ∈ set procs`
    show ?thesis by fastforce
  qed
qed auto
    

lemma containsCall_indirection:
  "[|containsCall procs prog qs q; containsCall procs c ps p;
  (q,ins,outs,c) ∈ set procs|]
  ==> containsCall procs prog (qs@q#ps) p"
proof(induct procs prog qs q rule:containsCall_induct)
  case (Call procs px esx retsx ps' p')
  note IH = `!!x y z psx. [|ps' = px # psx; (px, x, y, z) ∈ set procs;
    containsCall procs z psx p'; containsCall procs c ps p;
    (p', ins, outs, c) ∈ set procs|]
    ==> containsCall procs z (psx @ p' # ps) p`
  from `containsCall procs (Call px esx retsx) ps' p'`
  have "p' = px ∧ ps' = [] ∨
    (∃insx outsx cx psx. ps' = px#psx ∧ (px,insx,outsx,cx) ∈ set procs ∧
    containsCall procs cx psx p')" by simp
  thus ?case
  proof
    assume "p' = px ∧ ps' = []"
    with `containsCall procs c ps p` `(p', ins, outs, c) ∈ set procs`
    show ?thesis by fastforce
  next
    assume "∃insx outsx cx psx. ps' = px#psx ∧ (px,insx,outsx,cx) ∈ set procs ∧
      containsCall procs cx psx p'"
    then obtain insx outsx cx psx where "ps' = px#psx" 
      and "(px,insx,outsx,cx) ∈ set procs"
      and "containsCall procs cx psx p'" by blast
    from IH[OF this `containsCall procs c ps p`
      `(p', ins, outs, c) ∈ set procs`] 
    have "containsCall procs cx (psx @ p' # ps) p" .
    with `ps' = px#psx` `(px,insx,outsx,cx) ∈ set procs`
    show ?thesis by fastforce
  qed
qed auto


lemma Proc_CFG_Call_containsCall:
  "prog \<turnstile> n -CEdge (p,es,rets)->⇣p n' ==> containsCall procs prog [] p"
by(induct prog n et≡"CEdge (p,es,rets)" n' rule:Proc_CFG.induct,auto)


lemma containsCall_empty_Proc_CFG_Call_edge: 
  assumes "containsCall procs prog [] p"
  obtains l es rets l' where "prog \<turnstile> Label l -CEdge (p,es,rets)->⇣p Label l'"
proof(atomize_elim)
  from `containsCall procs prog [] p`
  show "∃l es rets l'. prog \<turnstile> Label l -CEdge (p,es,rets)->⇣p Label l'"
  proof(induct procs prog ps≡"[]::pname list" p rule:containsCall_induct)
    case Seq thus ?case
      by auto(fastforce dest:Proc_CFG_SeqFirst,fastforce dest:Proc_CFG_SeqSecond)
  next
    case Cond thus ?case
      by auto(fastforce dest:Proc_CFG_CondThen,fastforce dest:Proc_CFG_CondElse)
  next
    case While thus ?case by(fastforce dest:Proc_CFG_WhileBody)
  next
    case Call thus ?case by(fastforce intro:Proc_CFG_Call)
  qed auto
qed


subsubsection{* The edges of the combined CFG *}

type_synonym node = "(pname × label)"
type_synonym edge = "(node × (vname,val,node,pname) edge_kind × node)"

fun get_proc :: "node => pname"
  where "get_proc (p,l) = p"


inductive PCFG :: 
  "cmd => procs => node => (vname,val,node,pname) edge_kind => node => bool" 
("_,_ \<turnstile> _ -_-> _" [51,51,0,0,0] 81)
for prog::cmd and procs::procs
where

  Main:
  "prog \<turnstile> n -IEdge et->⇣p n' ==> prog,procs \<turnstile> (Main,n) -et-> (Main,n')"

| Proc:
  "[|(p,ins,outs,c) ∈ set procs; c \<turnstile> n -IEdge et->⇣p n'; 
    containsCall procs prog ps p|] 
  ==> prog,procs \<turnstile> (p,n) -et-> (p,n')"


| MainCall:
  "[|prog \<turnstile> Label l -CEdge (p,es,rets)->⇣p n'; (p,ins,outs,c) ∈ set procs|]
  ==> prog,procs \<turnstile> (Main,Label l) 
                  -(λs. True):(Main,n')\<hookrightarrow>⇘p⇙map (λe cf. interpret e cf) es-> (p,Entry)"

| ProcCall:
  "[|(p,ins,outs,c) ∈ set procs; c \<turnstile> Label l -CEdge (p',es',rets')->⇣p Label l';
    (p',ins',outs',c') ∈ set procs; containsCall procs prog ps p|]
  ==> prog,procs \<turnstile> (p,Label l) 
               -(λs. True):(p,Label l')\<hookrightarrow>⇘p'⇙map (λe cf. interpret e cf) es'-> (p',Entry)"

| MainReturn:
  "[|prog \<turnstile> Label l -CEdge (p,es,rets)->⇣p Label l'; (p,ins,outs,c) ∈ set procs|]
  ==> prog,procs \<turnstile> (p,Exit) -(λcf. snd cf = (Main,Label l'))\<hookleftarrow>⇘p⇙
       (λcf cf'. cf'(rets [:=] map cf outs))-> (Main,Label l')"

| ProcReturn:
  "[|(p,ins,outs,c) ∈ set procs; c \<turnstile> Label l -CEdge (p',es',rets')->⇣p Label l'; 
   (p',ins',outs',c') ∈ set procs; containsCall procs prog ps p|]
  ==> prog,procs \<turnstile> (p',Exit) -(λcf. snd cf = (p,Label l'))\<hookleftarrow>⇘p'⇙
       (λcf cf'. cf'(rets' [:=] map cf outs'))-> (p,Label l')"

| MainCallReturn:
  "prog \<turnstile> n -CEdge (p,es,rets)->⇣p n'
  ==> prog,procs \<turnstile> (Main,n) -(λs. False)⇣\<surd>-> (Main,n')"

| ProcCallReturn:
  "[|(p,ins,outs,c) ∈ set procs; c \<turnstile> n -CEdge (p',es',rets')->⇣p n'; 
    containsCall procs prog ps p|] 
  ==> prog,procs \<turnstile> (p,n) -(λs. False)⇣\<surd>-> (p,n')"


end