# Theory AuxLemmas

section ‹Auxiliary lemmas›

theory AuxLemmas imports Main begin

text ‹Lemma concerning maps and ‹@››

lemma map_append_append_maps:
assumes map:"map f xs = ys@zs"
obtains xs' xs'' where "map f xs' = ys" and "map f xs'' = zs" and "xs=xs'@xs''"
by (metis append_eq_conv_conj append_take_drop_id assms drop_map take_map that)

text ‹Lemma concerning splitting of @{term list}s›

lemma  path_split_general:
assumes all:"∀zs. xs ≠ ys@zs"
obtains j zs where "xs = (take j ys)@zs" and "j < length ys"
and "∀k > j. ∀zs'. xs ≠ (take k ys)@zs'"
proof(atomize_elim)
from ‹∀zs. xs ≠ ys@zs›
show "∃j zs. xs = take j ys @ zs ∧ j < length ys ∧
(∀k>j. ∀zs'. xs ≠ take k ys @ zs')"
proof(induct ys arbitrary:xs)
case Nil thus ?case by auto
next
case (Cons y' ys')
note IH = ‹⋀xs. ∀zs. xs ≠ ys' @ zs ⟹
∃j zs. xs = take j ys' @ zs ∧ j < length ys' ∧
(∀k. j < k ⟶ (∀zs'. xs ≠ take k ys' @ zs'))›
show ?case
proof(cases xs)
case Nil thus ?thesis by simp
next
case (Cons x' xs')
with ‹∀zs. xs ≠ (y' # ys') @ zs› have "x' ≠ y' ∨ (∀zs. xs' ≠ ys' @ zs)"
by simp
show ?thesis
proof(cases "x' = y'")
case True
with ‹x' ≠ y' ∨ (∀zs. xs' ≠ ys' @ zs)› have "∀zs. xs' ≠ ys' @ zs" by simp
from IH[OF this] have "∃j zs. xs' = take j ys' @ zs ∧ j < length ys' ∧
(∀k. j < k ⟶ (∀zs'. xs' ≠ take k ys' @ zs'))" .
then obtain j zs where "xs' = take j ys' @ zs"
and "j < length ys'"
and all_sub:"∀k. j < k ⟶ (∀zs'. xs' ≠ take k ys' @ zs')"
by blast
from ‹xs' = take j ys' @ zs› True
have "(x'#xs') = take (Suc j) (y' # ys') @ zs"
by simp
from all_sub True have all_imp:"∀k. j < k ⟶
(∀zs'. (x'#xs') ≠ take (Suc k) (y' # ys') @ zs')"
by auto
{ fix l assume "(Suc j) < l"
then obtain k where [simp]:"l = Suc k" by(cases l) auto
with ‹(Suc j) < l› have "j < k" by simp
with all_imp
have "∀zs'. (x'#xs') ≠ take (Suc k) (y' # ys') @ zs'"
by simp
hence "∀zs'. (x'#xs') ≠ take l (y' # ys') @ zs'"
by simp }
with ‹(x'#xs') = take (Suc j) (y' # ys') @ zs› ‹j < length ys'› Cons
show ?thesis by (metis Suc_length_conv less_Suc_eq_0_disj)
next
case False
with Cons have "∀i zs'. i > 0 ⟶ xs ≠ take i (y' # ys') @ zs'"
by auto(case_tac i,auto)
moreover
have "∃zs. xs = take 0 (y' # ys') @ zs" by simp
ultimately show ?thesis by(rule_tac x="0" in exI,auto)
qed
qed
qed
qed

end


# Theory BasicDefs

chapter ‹The Framework›

theory BasicDefs imports AuxLemmas begin

text ‹
As slicing is a program analysis that can be completely based on the
information given in the CFG, we want to provide a framework which
allows us to formalize and prove properties of slicing regardless of
the actual programming language. So the starting point for the formalization
is the definition of an abstract CFG, i.e.\ without considering features
specific for certain languages. By doing so we ensure that our framework
is as generic as possible since all proofs hold for every language whose
CFG conforms to this abstract CFG.

Static Slicing analyses a CFG prior to execution. Whereas dynamic
slicing can provide better results for certain inputs (i.e.\ trace and
initial state), static slicing is more conservative but provides
results independent of inputs.

Correctness for static slicing is defined using a weak
simulation between nodes and states when traversing the original and
the sliced graph. The weak simulation property demands that if a
(node,state) tuples $(n_1,s_1)$ simulates $(n_2,s_2)$
and making an observable move in the original graph leads from
$(n_1,s_1)$ to $(n_1',s_1')$, this tuple simulates a
tuple $(n_2,s_2)$ which is the result of making an
observable move in the sliced graph beginning in $(n_2',s_2')$.
›

section ‹Basic Definitions›

fun fun_upds :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list ⇒ ('a ⇒ 'b)"
where "fun_upds f [] ys = f"
| "fun_upds f xs [] = f"
| "fun_upds f (x#xs) (y#ys) = (fun_upds f xs ys)(x := y)"

notation fun_upds ("_'(_ /[:=]/ _')")

lemma fun_upds_nth:
"⟦i < length xs; length xs = length ys; distinct xs⟧
⟹ f(xs [:=] ys)(xs!i) = (ys!i)"
proof(induct xs arbitrary:ys i)
case Nil thus ?case by simp
next
case (Cons x' xs')
note IH = ‹⋀ys i. ⟦i < length xs'; length xs' = length ys; distinct xs'⟧
⟹ f(xs' [:=] ys) (xs'!i) = ys!i›
from ‹distinct (x'#xs')› have "distinct xs'" and "x' ∉ set xs'" by simp_all
from ‹length (x'#xs') = length ys› obtain y' ys' where [simp]:"ys = y'#ys'"
and "length xs' = length ys'"
by(cases ys) auto
show ?case
proof(cases i)
case 0 thus ?thesis by simp
next
case (Suc j)
with ‹i < length (x'#xs')› have "j < length xs'" by simp
from IH[OF this ‹length xs' = length ys'› ‹distinct xs'›]
have "f(xs' [:=] ys') (xs'!j) = ys'!j" .
with ‹x' ∉ set xs'› ‹j < length xs'›
have "f((x'#xs') [:=] ys) ((x'#xs')!(Suc j)) = ys!(Suc j)" by fastforce
with Suc show ?thesis by simp
qed
qed

lemma fun_upds_eq:
assumes "V ∈ set xs" and "length xs = length ys" and "distinct xs"
shows "f(xs [:=] ys) V = f'(xs [:=] ys) V"
proof -
from ‹V ∈ set xs› obtain i where "i < length xs" and "xs!i = V"
by(fastforce simp:in_set_conv_nth)
with ‹length xs = length ys› ‹distinct xs›
have "f(xs [:=] ys)(xs!i) = (ys!i)" by -(rule fun_upds_nth)
moreover
from ‹i < length xs› ‹xs!i = V› ‹length xs = length ys› ‹distinct xs›
have "f'(xs [:=] ys)(xs!i) = (ys!i)" by -(rule fun_upds_nth)
ultimately show ?thesis using ‹xs!i = V› by simp
qed

lemma fun_upds_notin:"x ∉ set xs ⟹ f(xs [:=] ys) x = f x"
by(induct xs arbitrary:ys,auto,case_tac ys,auto)

subsection ‹‹distinct_fst››

definition distinct_fst :: "('a × 'b) list ⇒ bool" where
"distinct_fst  ≡  distinct ∘ map fst"

lemma distinct_fst_Nil [simp]:
"distinct_fst []"

lemma distinct_fst_Cons [simp]:
"distinct_fst ((k,x)#kxs) = (distinct_fst kxs ∧ (∀y. (k,y) ∉ set kxs))"
by(auto simp:distinct_fst_def image_def)

lemma distinct_fst_isin_same_fst:
"⟦(x,y) ∈ set xs; (x,y') ∈ set xs; distinct_fst xs⟧
⟹ y = y'"
by(induct xs,auto simp:distinct_fst_def image_def)

subsection‹Edge kinds›

text ‹Every procedure has a unique name, e.g. in object oriented languages
‹pname› refers to class + procedure.›

text ‹A state is a call stack of tuples, which consists of:
\begin{enumerate}
\item data information, i.e.\ a mapping from the local variables in the call
frame to their values, and
\item control flow information, e.g.\ which node called the current procedure.
\end{enumerate}

Update and predicate edges check and manipulate only the data information
of the top call stack element. Call and return edges however may use the data and
control flow information present in the top stack element to state if this edge is
traversable. The call edge additionally has a list of functions to determine what
values the parameters have in a certain call frame and control flow information for
the return. The return edge is concerned with passing the values
of the return parameter values to the underlying stack frame. See the funtions
‹transfer› and ‹pred› in locale ‹CFG›.›

UpdateEdge "('var ⇀ 'val) ⇒ ('var ⇀ 'val)"                  ("⇑_")
| PredicateEdge "('var ⇀ 'val) ⇒ bool"                         ("'(_')⇩√")
| CallEdge "('var ⇀ 'val) × 'ret ⇒ bool" "'ret" "'pname"
"(('var ⇀ 'val) ⇀ 'val) list"                       ("_:_↪⇘_⇙_" 70)
| ReturnEdge "('var ⇀ 'val) × 'ret ⇒ bool" "'pname"
"('var ⇀ 'val) ⇒ ('var ⇀ 'val) ⇒ ('var ⇀ 'val)" ("_↩⇘_⇙_" 70)

definition intra_kind :: "('var,'val,'ret,'pname) edge_kind ⇒ bool"
where "intra_kind et ≡ (∃f. et = ⇑f) ∨ (∃Q. et = (Q)⇩√)"

lemma edge_kind_cases [case_names Intra Call Return]:
"⟦intra_kind et ⟹ P; ⋀Q r p fs. et = Q:r↪⇘p⇙fs ⟹ P;
⋀Q p f. et = Q↩⇘p⇙f ⟹ P⟧ ⟹ P"
by(cases et,auto simp:intra_kind_def)

end


# Theory CFG

section ‹CFG›

theory CFG imports BasicDefs begin

subsection ‹The abstract CFG›

subsubsection ‹Locale fixes and assumptions›

locale CFG =
fixes sourcenode :: "'edge ⇒ 'node"
fixes targetnode :: "'edge ⇒ 'node"
fixes kind :: "'edge ⇒ ('var,'val,'ret,'pname) edge_kind"
fixes valid_edge :: "'edge ⇒ bool"
fixes Entry::"'node" ("'('_Entry'_')")
fixes get_proc::"'node ⇒ 'pname"
fixes get_return_edges::"'edge ⇒ 'edge set"
fixes procs::"('pname × 'var list × 'var list) list"
fixes Main::"'pname"
assumes Entry_target [dest]: "⟦valid_edge a; targetnode a = (_Entry_)⟧ ⟹ False"
and get_proc_Entry:"get_proc (_Entry_) = Main"
and Entry_no_call_source:
"⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; sourcenode a = (_Entry_)⟧ ⟹ False"
and edge_det:
"⟦valid_edge a; valid_edge a'; sourcenode a = sourcenode a';
targetnode a = targetnode a'⟧ ⟹ a = a'"
and Main_no_call_target:"⟦valid_edge a; kind a = Q:r↪⇘Main⇙f⟧ ⟹ False"
and Main_no_return_source:"⟦valid_edge a; kind a = Q'↩⇘Main⇙f'⟧ ⟹ False"
and callee_in_procs:
"⟦valid_edge a; kind a = Q:r↪⇘p⇙fs⟧ ⟹ ∃ins outs. (p,ins,outs) ∈ set procs"
and get_proc_intra:"⟦valid_edge a; intra_kind(kind a)⟧
⟹ get_proc (sourcenode a) = get_proc (targetnode a)"
and get_proc_call:
"⟦valid_edge a; kind a = Q:r↪⇘p⇙fs⟧ ⟹ get_proc (targetnode a) = p"
and get_proc_return:
"⟦valid_edge a; kind a = Q'↩⇘p⇙f'⟧ ⟹ get_proc (sourcenode a) = p"
and call_edges_only:"⟦valid_edge a; kind a = Q:r↪⇘p⇙fs⟧
⟹ ∀a'. valid_edge a' ∧ targetnode a' = targetnode a ⟶
(∃Qx rx fsx. kind a' = Qx:rx↪⇘p⇙fsx)"
and return_edges_only:"⟦valid_edge a; kind a = Q'↩⇘p⇙f'⟧
⟹ ∀a'. valid_edge a' ∧ sourcenode a' = sourcenode a ⟶
(∃Qx fx. kind a' = Qx↩⇘p⇙fx)"
and get_return_edge_call:
"⟦valid_edge a; kind a = Q:r↪⇘p⇙fs⟧ ⟹ get_return_edges a ≠ {}"
and get_return_edges_valid:
"⟦valid_edge a; a' ∈ get_return_edges a⟧ ⟹ valid_edge a'"
and only_call_get_return_edges:
"⟦valid_edge a; a' ∈ get_return_edges a⟧ ⟹ ∃Q r p fs. kind a = Q:r↪⇘p⇙fs"
and call_return_edges:
"⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; a' ∈ get_return_edges a⟧
⟹ ∃Q' f'. kind a' = Q'↩⇘p⇙f'"
and return_needs_call: "⟦valid_edge a; kind a = Q'↩⇘p⇙f'⟧
⟹ ∃!a'. valid_edge a' ∧ (∃Q r fs. kind a' = Q:r↪⇘p⇙fs) ∧ a ∈ get_return_edges a'"
"⟦valid_edge a; a' ∈ get_return_edges a⟧
⟹ ∃a''. valid_edge a'' ∧ sourcenode a'' = targetnode a ∧
targetnode a'' = sourcenode a' ∧ kind a'' = (λcf. False)⇩√"
and call_return_node_edge:
"⟦valid_edge a; a' ∈ get_return_edges a⟧
⟹ ∃a''. valid_edge a'' ∧ sourcenode a'' = sourcenode a ∧
targetnode a'' = targetnode a' ∧ kind a'' = (λcf. False)⇩√"
and call_only_one_intra_edge:
"⟦valid_edge a; kind a = Q:r↪⇘p⇙fs⟧
⟹ ∃!a'. valid_edge a' ∧ sourcenode a' = sourcenode a ∧ intra_kind(kind a')"
and return_only_one_intra_edge:
"⟦valid_edge a; kind a = Q'↩⇘p⇙f'⟧
⟹ ∃!a'. valid_edge a' ∧ targetnode a' = targetnode a ∧ intra_kind(kind a')"
and same_proc_call_unique_target:
"⟦valid_edge a; valid_edge a'; kind a = Q⇩1:r⇩1↪⇘p⇙fs⇩1;  kind a' = Q⇩2:r⇩2↪⇘p⇙fs⇩2⟧
⟹ targetnode a = targetnode a'"
and unique_callers:"distinct_fst procs"
and distinct_formal_ins:"(p,ins,outs) ∈ set procs ⟹ distinct ins"
and distinct_formal_outs:"(p,ins,outs) ∈ set procs ⟹ distinct outs"

begin

lemma get_proc_get_return_edge:
assumes "valid_edge a" and "a' ∈ get_return_edges a"
shows "get_proc (sourcenode a) = get_proc (targetnode a')"
proof -
from assms obtain ax where "valid_edge ax" and "sourcenode a = sourcenode ax"
and "targetnode a' = targetnode ax" and "intra_kind(kind ax)"
by(auto dest:call_return_node_edge simp:intra_kind_def)
thus ?thesis by(fastforce intro:get_proc_intra)
qed

lemma call_intra_edge_False:
assumes "valid_edge a" and "kind a = Q:r↪⇘p⇙fs" and "valid_edge a'"
and "sourcenode a = sourcenode a'" and "intra_kind(kind a')"
shows "kind a' = (λcf. False)⇩√"
proof -
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› obtain ax where "ax ∈ get_return_edges a"
by(fastforce dest:get_return_edge_call)
with ‹valid_edge a› obtain a'' where "valid_edge a''"
and "sourcenode a'' = sourcenode a" and "kind a'' = (λcf. False)⇩√"
by(fastforce dest:call_return_node_edge)
from ‹kind a'' = (λcf. False)⇩√› have "intra_kind(kind a'')"
with assms ‹valid_edge a''› ‹sourcenode a'' = sourcenode a›
‹kind a'' = (λcf. False)⇩√›
show ?thesis by(fastforce dest:call_only_one_intra_edge)
qed

lemma formal_in_THE:
"⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; (p,ins,outs) ∈ set procs⟧
⟹ (THE ins. ∃outs. (p,ins,outs) ∈ set procs) = ins"
by(fastforce dest:distinct_fst_isin_same_fst intro:unique_callers)

lemma formal_out_THE:
"⟦valid_edge a; kind a = Q↩⇘p⇙f; (p,ins,outs) ∈ set procs⟧
⟹ (THE outs. ∃ins. (p,ins,outs) ∈ set procs) = outs"
by(fastforce dest:distinct_fst_isin_same_fst intro:unique_callers)

subsubsection ‹Transfer and predicate functions›

fun params :: "(('var ⇀ 'val) ⇀ 'val) list ⇒ ('var ⇀ 'val) ⇒ 'val option list"
where "params [] cf = []"
| "params (f#fs) cf = (f cf)#params fs cf"

lemma params_nth:
"i < length fs ⟹ (params fs cf)!i = (fs!i) cf"
by(induct fs arbitrary:i,auto,case_tac i,auto)

lemma [simp]:"length (params fs cf) = length fs"
by(induct fs) auto

fun transfer :: "('var,'val,'ret,'pname) edge_kind ⇒ (('var ⇀ 'val) × 'ret) list ⇒
(('var ⇀ 'val) × 'ret) list"
where "transfer (⇑f) (cf#cfs)    = (f (fst cf),snd cf)#cfs"
| "transfer (Q)⇩√ (cf#cfs)      = (cf#cfs)"
| "transfer (Q:r↪⇘p⇙fs) (cf#cfs) =
(let ins = THE ins. ∃outs. (p,ins,outs) ∈ set procs in
(Map.empty(ins [:=] params fs (fst cf)),r)#cf#cfs)"
| "transfer (Q↩⇘p⇙f )(cf#cfs)    = (case cfs of [] ⇒ []
| cf'#cfs' ⇒ (f (fst cf) (fst cf'),snd cf')#cfs')"
| "transfer et [] = []"

fun transfers :: "('var,'val,'ret,'pname) edge_kind list ⇒ (('var ⇀ 'val) × 'ret) list ⇒
(('var ⇀ 'val) × 'ret) list"
where "transfers [] s   = s"
| "transfers (et#ets) s = transfers ets (transfer et s)"

fun pred :: "('var,'val,'ret,'pname) edge_kind ⇒ (('var ⇀ 'val) × 'ret) list ⇒ bool"
where "pred (⇑f) (cf#cfs) = True"
| "pred (Q)⇩√ (cf#cfs)   = Q (fst cf)"
| "pred (Q:r↪⇘p⇙fs) (cf#cfs) = Q (fst cf,r)"
| "pred (Q↩⇘p⇙f) (cf#cfs) = (Q cf ∧ cfs ≠ [])"
| "pred et [] = False"

fun preds :: "('var,'val,'ret,'pname) edge_kind list ⇒ (('var ⇀ 'val) × 'ret) list ⇒ bool"
where "preds [] s   = True"
| "preds (et#ets) s = (pred et s ∧ preds ets (transfer et s))"

lemma transfers_split:
"(transfers (ets@ets') s) = (transfers ets' (transfers ets s))"
by(induct ets arbitrary:s) auto

lemma preds_split:
"(preds (ets@ets') s) = (preds ets s ∧ preds ets' (transfers ets s))"
by(induct ets arbitrary:s) auto

abbreviation state_val :: "(('var ⇀ 'val) × 'ret) list ⇒ 'var ⇀ 'val"
where "state_val s V ≡ (fst (hd s)) V"

subsubsection ‹‹valid_node››

definition valid_node :: "'node ⇒ bool"
where "valid_node n ≡
(∃a. valid_edge a ∧ (n = sourcenode a ∨ n = targetnode a))"

lemma [simp]: "valid_edge a ⟹ valid_node (sourcenode a)"
by(fastforce simp:valid_node_def)

lemma [simp]: "valid_edge a ⟹ valid_node (targetnode a)"
by(fastforce simp:valid_node_def)

subsection ‹CFG paths›

inductive path :: "'node ⇒ 'edge list ⇒ 'node ⇒ bool"
("_ -_→* _" [51,0,0] 80)
where
empty_path:"valid_node n ⟹ n -[]→* n"

| Cons_path:
"⟦n'' -as→* n'; valid_edge a; sourcenode a = n; targetnode a = n''⟧
⟹ n -a#as→* n'"

lemma path_valid_node:
assumes "n -as→* n'" shows "valid_node n" and "valid_node n'"
using ‹n -as→* n'›
by(induct rule:path.induct,auto)

lemma empty_path_nodes [dest]:"n -[]→* n' ⟹ n = n'"
by(fastforce elim:path.cases)

lemma path_valid_edges:"n -as→* n' ⟹ ∀a ∈ set as. valid_edge a"
by(induct rule:path.induct) auto

lemma path_edge:"valid_edge a ⟹ sourcenode a -[a]→* targetnode a"
by(fastforce intro:Cons_path empty_path)

lemma path_Append:"⟦n -as→* n''; n'' -as'→* n'⟧
⟹ n -as@as'→* n'"
by(induct rule:path.induct,auto intro:Cons_path)

lemma path_split:
assumes "n -as@a#as'→* n'"
shows "n -as→* sourcenode a" and "valid_edge a" and "targetnode a -as'→* n'"
using ‹n -as@a#as'→* n'›
proof(induct as arbitrary:n)
case Nil case 1
thus ?case by(fastforce elim:path.cases intro:empty_path)
next
case Nil case 2
thus ?case by(fastforce elim:path.cases intro:path_edge)
next
case Nil case 3
thus ?case by(fastforce elim:path.cases)
next
case (Cons ax asx)
note IH1 = ‹⋀n. n -asx@a#as'→* n' ⟹ n -asx→* sourcenode a›
note IH2 = ‹⋀n. n -asx@a#as'→* n' ⟹ valid_edge a›
note IH3 = ‹⋀n. n -asx@a#as'→* n' ⟹ targetnode a -as'→* n'›
{ case 1
hence "sourcenode ax = n" and "targetnode ax -asx@a#as'→* n'" and "valid_edge ax"
by(auto elim:path.cases)
from IH1[OF ‹ targetnode ax -asx@a#as'→* n'›]
have "targetnode ax -asx→* sourcenode a" .
with ‹sourcenode ax = n› ‹valid_edge ax› show ?case by(fastforce intro:Cons_path)
next
case 2 hence "targetnode ax -asx@a#as'→* n'" by(auto elim:path.cases)
from IH2[OF this] show ?case .
next
case 3 hence "targetnode ax -asx@a#as'→* n'" by(auto elim:path.cases)
from IH3[OF this] show ?case .
}
qed

lemma path_split_Cons:
assumes "n -as→* n'" and "as ≠ []"
obtains a' as' where "as = a'#as'" and "n = sourcenode a'"
and "valid_edge a'" and "targetnode a' -as'→* n'"
proof(atomize_elim)
from ‹as ≠ []› obtain a' as' where "as = a'#as'" by(cases as) auto
with ‹n -as→* n'› have "n -[]@a'#as'→* n'" by simp
hence "n -[]→* sourcenode a'" and "valid_edge a'" and "targetnode a' -as'→* n'"
by(rule path_split)+
from ‹n -[]→* sourcenode a'› have "n = sourcenode a'" by fast
with ‹as = a'#as'› ‹valid_edge a'› ‹targetnode a' -as'→* n'›
show "∃a' as'. as = a'#as' ∧ n = sourcenode a' ∧ valid_edge a' ∧
targetnode a' -as'→* n'"
by fastforce
qed

lemma path_split_snoc:
assumes "n -as→* n'" and "as ≠ []"
obtains a' as' where "as = as'@[a']" and "n -as'→* sourcenode a'"
and "valid_edge a'" and "n' = targetnode a'"
proof(atomize_elim)
from ‹as ≠ []› obtain a' as' where "as = as'@[a']" by(cases as rule:rev_cases) auto
with ‹n -as→* n'› have "n -as'@a'#[]→* n'" by simp
hence "n -as'→* sourcenode a'" and "valid_edge a'" and "targetnode a' -[]→* n'"
by(rule path_split)+
from ‹targetnode a' -[]→* n'› have "n' = targetnode a'" by fast
with ‹as = as'@[a']› ‹valid_edge a'› ‹n -as'→* sourcenode a'›
show "∃as' a'. as = as'@[a'] ∧ n -as'→* sourcenode a' ∧ valid_edge a' ∧
n' = targetnode a'"
by fastforce
qed

lemma path_split_second:
assumes "n -as@a#as'→* n'" shows "sourcenode a -a#as'→* n'"
proof -
from ‹n -as@a#as'→* n'› have "valid_edge a" and "targetnode a -as'→* n'"
by(auto intro:path_split)
thus ?thesis by(fastforce intro:Cons_path)
qed

lemma path_Entry_Cons:
assumes "(_Entry_) -as→* n'" and "n' ≠ (_Entry_)"
obtains n a where "sourcenode a = (_Entry_)" and "targetnode a = n"
and "n -tl as→* n'" and "valid_edge a" and "a = hd as"
proof(atomize_elim)
from ‹(_Entry_) -as→* n'› ‹n' ≠ (_Entry_)› have "as ≠ []"
by(cases as,auto elim:path.cases)
with ‹(_Entry_) -as→* n'› obtain a' as' where "as = a'#as'"
and "(_Entry_) = sourcenode a'" and "valid_edge a'" and "targetnode a' -as'→* n'"
by(erule path_split_Cons)
thus "∃a n. sourcenode a = (_Entry_) ∧ targetnode a = n ∧ n -tl as→* n' ∧
valid_edge a ∧ a = hd as"
by fastforce
qed

lemma path_det:
"⟦n -as→* n'; n -as→* n''⟧ ⟹ n' = n''"
proof(induct as arbitrary:n)
case Nil thus ?case by(auto elim:path.cases)
next
case (Cons a' as')
note IH = ‹⋀n. ⟦n -as'→* n'; n -as'→* n''⟧ ⟹ n' = n''›
from ‹n -a'#as'→* n'› have "targetnode a' -as'→* n'"
by(fastforce elim:path_split_Cons)
from ‹n -a'#as'→* n''› have "targetnode a' -as'→* n''"
by(fastforce elim:path_split_Cons)
from IH[OF ‹targetnode a' -as'→* n'› this] show ?thesis .
qed

definition
sourcenodes :: "'edge list ⇒ 'node list"
where "sourcenodes xs ≡ map sourcenode xs"

definition
kinds :: "'edge list ⇒ ('var,'val,'ret,'pname) edge_kind list"
where "kinds xs ≡ map kind xs"

definition
targetnodes :: "'edge list ⇒ 'node list"
where "targetnodes xs ≡ map targetnode xs"

lemma path_sourcenode:
"⟦n -as→* n'; as ≠ []⟧ ⟹ hd (sourcenodes as) = n"
by(fastforce elim:path_split_Cons simp:sourcenodes_def)

lemma path_targetnode:
"⟦n -as→* n'; as ≠ []⟧ ⟹ last (targetnodes as) = n'"
by(fastforce elim:path_split_snoc simp:targetnodes_def)

lemma sourcenodes_is_n_Cons_butlast_targetnodes:
"⟦n -as→* n'; as ≠ []⟧ ⟹
sourcenodes as = n#(butlast (targetnodes as))"
proof(induct as arbitrary:n)
case Nil thus ?case by simp
next
case (Cons a' as')
note IH = ‹⋀n. ⟦n -as'→* n'; as' ≠ []⟧
⟹ sourcenodes as' = n#(butlast (targetnodes as'))›
from ‹n -a'#as'→* n'› have "n = sourcenode a'" and "targetnode a' -as'→* n'"
by(auto elim:path_split_Cons)
show ?case
proof(cases "as' = []")
case True
with ‹targetnode a' -as'→* n'› have "targetnode a' = n'" by fast
with True ‹n = sourcenode a'› show ?thesis
next
case False
from IH[OF ‹targetnode a' -as'→* n'› this]
have "sourcenodes as' = targetnode a' # butlast (targetnodes as')" .
with ‹n = sourcenode a'› False show ?thesis
qed
qed

lemma targetnodes_is_tl_sourcenodes_App_n':
"⟦n -as→* n'; as ≠ []⟧ ⟹
targetnodes as = (tl (sourcenodes as))@[n']"
proof(induct as arbitrary:n' rule:rev_induct)
case Nil thus ?case by simp
next
case (snoc a' as')
note IH = ‹⋀n'. ⟦n -as'→* n'; as' ≠ []⟧
⟹ targetnodes as' = tl (sourcenodes as') @ [n']›
from ‹n -as'@[a']→* n'› have "n -as'→* sourcenode a'" and "n' = targetnode a'"
by(auto elim:path_split_snoc)
show ?case
proof(cases "as' = []")
case True
with ‹n -as'→* sourcenode a'› have "n = sourcenode a'" by fast
with True ‹n' = targetnode a'› show ?thesis
next
case False
from IH[OF ‹n -as'→* sourcenode a'› this]
have "targetnodes as' = tl (sourcenodes as')@[sourcenode a']" .
with ‹n' = targetnode a'› False show ?thesis
qed
qed

subsubsection ‹Intraprocedural paths›

definition intra_path :: "'node ⇒ 'edge list ⇒ 'node ⇒ bool"
("_ -_→⇩ι* _" [51,0,0] 80)
where "n -as→⇩ι* n' ≡ n -as→* n' ∧ (∀a ∈ set as. intra_kind(kind a))"

lemma intra_path_get_procs:
assumes "n -as→⇩ι* n'" shows "get_proc n = get_proc n'"
proof -
from ‹n -as→⇩ι* n'› have "n -as→* n'" and "∀a ∈ set as. intra_kind(kind a)"
thus ?thesis
proof(induct as arbitrary:n)
case Nil thus ?case by fastforce
next
case (Cons a' as')
note IH = ‹⋀n. ⟦n -as'→* n'; ∀a∈set as'. intra_kind (kind a)⟧
⟹ get_proc n = get_proc n'›
from ‹∀a∈set (a'#as'). intra_kind (kind a)›
have "intra_kind(kind a')" and "∀a∈set as'. intra_kind (kind a)" by simp_all
from ‹n -a'#as'→* n'› have "sourcenode a' = n" and "valid_edge a'"
and "targetnode a' -as'→* n'" by(auto elim:path.cases)
from IH[OF ‹targetnode a' -as'→* n'› ‹∀a∈set as'. intra_kind (kind a)›]
have "get_proc (targetnode a') = get_proc n'" .
from ‹valid_edge a'› ‹intra_kind(kind a')›
have "get_proc (sourcenode a') = get_proc (targetnode a')"
by(rule get_proc_intra)
with ‹sourcenode a' = n› ‹get_proc (targetnode a') = get_proc n'›
show ?case by simp
qed
qed

lemma intra_path_Append:
"⟦n -as→⇩ι* n''; n'' -as'→⇩ι* n'⟧ ⟹ n -as@as'→⇩ι* n'"
by(fastforce intro:path_Append simp:intra_path_def)

lemma get_proc_get_return_edges:
assumes "valid_edge a" and "a' ∈ get_return_edges a"
shows "get_proc(targetnode a) = get_proc(sourcenode a')"
proof -
from ‹valid_edge a› ‹a' ∈ get_return_edges a›
obtain a'' where "valid_edge a''" and "sourcenode a'' = targetnode a"
and "targetnode a'' = sourcenode a'" and "kind a'' = (λcf. False)⇩√"
from ‹valid_edge a''› ‹kind a'' = (λcf. False)⇩√›
have "get_proc(sourcenode a'') = get_proc(targetnode a'')"
by(fastforce intro:get_proc_intra simp:intra_kind_def)
with ‹sourcenode a'' = targetnode a› ‹targetnode a'' = sourcenode a'›
show ?thesis by simp
qed

subsubsection ‹Valid paths›

declare conj_cong[fundef_cong]

fun valid_path_aux :: "'edge list ⇒ 'edge list ⇒ bool"
where "valid_path_aux cs [] ⟷ True"
| "valid_path_aux cs (a#as) ⟷
(case (kind a) of Q:r↪⇘p⇙fs ⇒ valid_path_aux (a#cs) as
| Q↩⇘p⇙f ⇒ case cs of [] ⇒ valid_path_aux [] as
| c'#cs' ⇒ a ∈ get_return_edges c' ∧
valid_path_aux cs' as
|    _ ⇒ valid_path_aux cs as)"

lemma vpa_induct [consumes 1,case_names vpa_empty vpa_intra vpa_Call vpa_ReturnEmpty
vpa_ReturnCons]:
assumes major: "valid_path_aux xs ys"
and rules: "⋀cs. P cs []"
"⋀cs a as. ⟦intra_kind(kind a); valid_path_aux cs as; P cs as⟧ ⟹ P cs (a#as)"
"⋀cs a as Q r p fs. ⟦kind a = Q:r↪⇘p⇙fs; valid_path_aux (a#cs) as; P (a#cs) as⟧
⟹ P cs (a#as)"
"⋀cs a as Q p f. ⟦kind a = Q↩⇘p⇙f; cs = []; valid_path_aux [] as; P [] as⟧
⟹ P cs (a#as)"
"⋀cs a as Q p f c' cs' . ⟦kind a = Q↩⇘p⇙f; cs = c'#cs'; valid_path_aux cs' as;
a ∈ get_return_edges c'; P cs' as⟧
⟹ P cs (a#as)"
shows "P xs ys"
using major
apply(induct ys arbitrary: xs)
by(auto intro:rules split:edge_kind.split_asm list.split_asm simp:intra_kind_def)

lemma valid_path_aux_intra_path:
"∀a ∈ set as. intra_kind(kind a) ⟹ valid_path_aux cs as"
by(induct as,auto simp:intra_kind_def)

lemma valid_path_aux_callstack_prefix:
"valid_path_aux (cs@cs') as ⟹ valid_path_aux cs as"
proof(induct "cs@cs'" as arbitrary:cs cs' rule:vpa_induct)
case vpa_empty thus ?case by simp
next
case (vpa_intra a as)
hence "valid_path_aux cs as" by simp
with ‹intra_kind (kind a)› show ?case by(cases "kind a",auto simp:intra_kind_def)
next
case (vpa_Call a as Q r p fs cs'' cs')
note IH = ‹⋀xs ys. a#cs''@cs' = xs@ys ⟹ valid_path_aux xs as›
have "a#cs''@cs' = (a#cs'')@cs'" by simp
from IH[OF this] have "valid_path_aux (a#cs'') as" .
with ‹kind a = Q:r↪⇘p⇙fs› show ?case by simp
next
case (vpa_ReturnEmpty a as Q p f cs'' cs')
hence "valid_path_aux cs'' as" by simp
with ‹kind a = Q↩⇘p⇙f› ‹cs''@cs' = []› show ?case by simp
next
case (vpa_ReturnCons a as Q p f c' cs' csx csx')
note IH = ‹⋀xs ys. cs' = xs@ys ⟹ valid_path_aux xs as›
from ‹csx@csx' = c'#cs'›
have "csx = [] ∧ csx' = c'#cs' ∨ (∃zs. csx = c'#zs ∧ zs@csx' = cs')"
thus ?case
proof
assume "csx = [] ∧ csx' = c'#cs'"
hence "csx = []" and "csx' = c'#cs'" by simp_all
from ‹csx' = c'#cs'› have "cs' = []@tl csx'" by simp
from IH[OF this] have "valid_path_aux [] as" .
with ‹csx = []› ‹kind a = Q↩⇘p⇙f› show ?thesis by simp
next
assume "∃zs. csx = c'#zs ∧ zs@csx' = cs'"
then obtain zs where "csx = c'#zs" and "cs' = zs@csx'" by auto
from IH[OF ‹cs' = zs@csx'›] have "valid_path_aux zs as" .
with ‹csx = c'#zs› ‹kind a = Q↩⇘p⇙f› ‹a ∈ get_return_edges c'›
show ?thesis by simp
qed
qed

fun upd_cs :: "'edge list ⇒ 'edge list ⇒ 'edge list"
where "upd_cs cs [] = cs"
| "upd_cs cs (a#as) =
(case (kind a) of Q:r↪⇘p⇙fs ⇒ upd_cs (a#cs) as
| Q↩⇘p⇙f ⇒ case cs of [] ⇒ upd_cs cs as
| c'#cs' ⇒ upd_cs cs' as
|    _ ⇒ upd_cs cs as)"

lemma upd_cs_empty [dest]:
"upd_cs cs [] = [] ⟹ cs = []"
by(cases cs) auto

lemma upd_cs_intra_path:
"∀a ∈ set as. intra_kind(kind a) ⟹ upd_cs cs as = cs"
by(induct as,auto simp:intra_kind_def)

lemma upd_cs_Append:
"⟦upd_cs cs as = cs'; upd_cs cs' as' = cs''⟧ ⟹ upd_cs cs (as@as') = cs''"
by(induct as arbitrary:cs,auto split:edge_kind.split list.split)

lemma upd_cs_empty_split:
assumes "upd_cs cs as = []" and "cs ≠ []" and "as ≠ []"
obtains xs ys where "as = xs@ys" and "xs ≠ []" and "upd_cs cs xs = []"
and "∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []"
and "upd_cs [] ys = []"
proof(atomize_elim)
from ‹upd_cs cs as = []› ‹cs ≠ []› ‹as ≠ []›
show "∃xs ys. as = xs@ys ∧ xs ≠ [] ∧ upd_cs cs xs = [] ∧
(∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []) ∧
upd_cs [] ys = []"
proof(induct as arbitrary:cs)
case Nil thus ?case by simp
next
case (Cons a' as')
note IH = ‹⋀cs. ⟦upd_cs cs as' = []; cs ≠ []; as' ≠ []⟧
⟹ ∃xs ys. as' = xs@ys ∧ xs ≠ [] ∧ upd_cs cs xs = [] ∧
(∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []) ∧
upd_cs [] ys = []›
show ?case
proof(cases "kind a'" rule:edge_kind_cases)
case Intra
with ‹upd_cs cs (a'#as') = []› have "upd_cs cs as' = []"
by(fastforce simp:intra_kind_def)
with ‹cs ≠ []› have "as' ≠ []" by fastforce
from IH[OF ‹upd_cs cs as' = []› ‹cs ≠ []› this] obtain xs ys where "as' = xs@ys"
and "xs ≠ []" and "upd_cs cs xs = []" and "upd_cs [] ys = []"
and "∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []" by blast
from ‹upd_cs cs xs = []› Intra have "upd_cs cs (a'#xs) = []"
by(fastforce simp:intra_kind_def)
from ‹∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []› ‹xs ≠ []› Intra
have "∀xs' ys'. a'#xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []"
apply auto
apply(case_tac xs') apply(auto simp:intra_kind_def)
by(erule_tac x="[]" in allE,fastforce)+
with ‹as' = xs@ys› ‹upd_cs cs (a'#xs) = []› ‹upd_cs [] ys = []›
show ?thesis apply(rule_tac x="a'#xs" in exI) by fastforce
next
case (Call Q p f)
with ‹upd_cs cs (a'#as') = []› have "upd_cs (a'#cs) as' = []" by simp
with ‹cs ≠ []› have "as' ≠ []" by fastforce
from IH[OF ‹upd_cs (a'#cs) as' = []› _ this] obtain xs ys where "as' = xs@ys"
and "xs ≠ []" and "upd_cs (a'#cs) xs = []" and "upd_cs [] ys = []"
and "∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs (a'#cs) xs' ≠ []" by blast
from ‹upd_cs (a'#cs) xs = []› Call have "upd_cs cs (a'#xs) = []" by simp
from ‹∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs (a'#cs) xs' ≠ []›
‹xs ≠ []› ‹cs ≠ []› Call
have "∀xs' ys'. a'#xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []"
by auto(case_tac xs',auto)
with ‹as' = xs@ys› ‹upd_cs cs (a'#xs) = []› ‹upd_cs [] ys = []›
show ?thesis apply(rule_tac x="a'#xs" in exI) by fastforce
next
case (Return Q p f)
with ‹upd_cs cs (a'#as') = []› ‹cs ≠ []› obtain c' cs' where "cs = c'#cs'"
and "upd_cs cs' as' = []" by(cases cs) auto
show ?thesis
proof(cases "cs' = []")
case True
with ‹cs = c'#cs'› ‹upd_cs cs' as' = []› Return show ?thesis
apply(rule_tac x="[a']" in exI) apply clarsimp
by(case_tac xs') auto
next
case False
with ‹upd_cs cs' as' = []› have "as' ≠ []" by fastforce
from IH[OF ‹upd_cs cs' as' = []› False this] obtain xs ys where "as' = xs@ys"
and "xs ≠ []" and "upd_cs cs' xs = []" and "upd_cs [] ys = []"
and "∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs' xs' ≠ []" by blast
from ‹upd_cs cs' xs = []› ‹cs = c'#cs'› Return have "upd_cs cs (a'#xs) = []"
by simp
from ‹∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs' xs' ≠ []›
‹xs ≠ []› ‹cs = c'#cs'› Return
have "∀xs' ys'. a'#xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []"
by auto(case_tac xs',auto)
with ‹as' = xs@ys› ‹upd_cs cs (a'#xs) = []› ‹upd_cs [] ys = []›
show ?thesis apply(rule_tac x="a'#xs" in exI) by fastforce
qed
qed
qed
qed

lemma upd_cs_snoc_Return_Cons:
assumes "kind a = Q↩⇘p⇙f"
shows "upd_cs cs as = c'#cs' ⟹ upd_cs cs (as@[a]) = cs'"
proof(induct as arbitrary:cs)
case Nil
with ‹kind a = Q↩⇘p⇙f› have "upd_cs cs [a] = cs'" by simp
thus ?case by simp
next
case (Cons a' as')
note IH = ‹⋀cs. upd_cs cs as' = c'#cs' ⟹ upd_cs cs (as'@[a]) = cs'›
show ?case
proof(cases "kind a'" rule:edge_kind_cases)
case Intra
with ‹upd_cs cs (a'#as') = c'#cs'›
have "upd_cs cs as' = c'#cs'" by(fastforce simp:intra_kind_def)
from IH[OF this] have "upd_cs cs (as'@[a]) = cs'" .
with Intra show ?thesis by(fastforce simp:intra_kind_def)
next
case Call
with ‹upd_cs cs (a'#as') = c'#cs'›
have "upd_cs (a'#cs) as' = c'#cs'" by simp
from IH[OF this] have "upd_cs (a'#cs) (as'@[a]) = cs'" .
with Call show ?thesis by simp
next
case Return
show ?thesis
proof(cases cs)
case Nil
with ‹upd_cs cs (a'#as') = c'#cs'› Return
have "upd_cs cs as' = c'#cs'" by simp
from IH[OF this] have "upd_cs cs (as'@[a]) = cs'" .
with Nil Return show ?thesis by simp
next
case (Cons cx csx)
with ‹upd_cs cs (a'#as') = c'#cs'› Return
have "upd_cs csx as' = c'#cs'" by simp
from IH[OF this] have "upd_cs csx (as'@[a]) = cs'" .
with Cons Return show ?thesis by simp
qed
qed
qed

lemma upd_cs_snoc_Call:
assumes "kind a = Q:r↪⇘p⇙fs"
shows "upd_cs cs (as@[a]) = a#(upd_cs cs as)"
proof(induct as arbitrary:cs)
case Nil
with ‹kind a = Q:r↪⇘p⇙fs› show ?case by simp
next
case (Cons a' as')
note IH = ‹⋀cs. upd_cs cs (as'@[a]) = a#upd_cs cs as'›
show ?case
proof(cases "kind a'" rule:edge_kind_cases)
case Intra
with IH[of cs] show ?thesis by(fastforce simp:intra_kind_def)
next
case Call
with IH[of "a'#cs"] show ?thesis by simp
next
case Return
show ?thesis
proof(cases cs)
case Nil
with IH[of "[]"] Return show ?thesis by simp
next
case (Cons cx csx)
with IH[of csx] Return show ?thesis by simp
qed
qed
qed

lemma valid_path_aux_split:
assumes "valid_path_aux cs (as@as')"
shows "valid_path_aux cs as" and "valid_path_aux (upd_cs cs as) as'"
using ‹valid_path_aux cs (as@as')›
proof(induct cs "as@as'" arbitrary:as as' rule:vpa_induct)
case (vpa_intra cs a as as'')
note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux cs xs›
note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux (upd_cs cs xs) ys›
{ case 1
from vpa_intra
have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')"
thus ?case
proof
assume "as'' = [] ∧ a#as = as'"
thus ?thesis by simp
next
assume "∃xs. a#xs = as'' ∧ as = xs@as'"
then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
from IH1[OF ‹as = xs@as'›] have "valid_path_aux cs xs" .
with ‹a#xs = as''› ‹intra_kind (kind a)›
show ?thesis by(fastforce simp:intra_kind_def)
qed
next
case 2
from vpa_intra
have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')"
thus ?case
proof
assume "as'' = [] ∧ a#as = as'"
hence "as = []@tl as'" by(cases as') auto
from IH2[OF this] have "valid_path_aux (upd_cs cs []) (tl as')" by simp
with ‹as'' = [] ∧ a#as = as'› ‹intra_kind (kind a)›
show ?thesis by(fastforce simp:intra_kind_def)
next
assume "∃xs. a#xs = as'' ∧ as = xs@as'"
then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
from IH2[OF ‹as = xs@as'›] have "valid_path_aux (upd_cs cs xs) as'" .
from ‹a#xs = as''› ‹intra_kind (kind a)›
have "upd_cs cs xs = upd_cs cs as''" by(fastforce simp:intra_kind_def)
with ‹valid_path_aux (upd_cs cs xs) as'›
show ?thesis by simp
qed
}
next
case (vpa_Call cs a as Q r p fs as'')
note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux (a#cs) xs›
note IH2 = ‹⋀xs ys. as = xs@ys ⟹   valid_path_aux (upd_cs (a#cs) xs) ys›
{ case 1
from vpa_Call
have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')"
thus ?case
proof
assume "as'' = [] ∧ a#as = as'"
thus ?thesis by simp
next
assume "∃xs. a#xs = as'' ∧ as = xs@as'"
then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
from IH1[OF ‹as = xs@as'›] have "valid_path_aux (a#cs) xs" .
with ‹a#xs = as''›[THEN sym] ‹kind a = Q:r↪⇘p⇙fs›
show ?thesis by simp
qed
next
case 2
from vpa_Call
have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')"
thus ?case
proof
assume "as'' = [] ∧ a#as = as'"
hence "as = []@tl as'" by(cases as') auto
from IH2[OF this] have "valid_path_aux (upd_cs (a#cs) []) (tl as')" .
with ‹as'' = [] ∧ a#as = as'› ‹kind a = Q:r↪⇘p⇙fs›
show ?thesis by clarsimp
next
assume "∃xs. a#xs = as'' ∧ as = xs@as'"
then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
from IH2[OF ‹as = xs@as'›] have "valid_path_aux (upd_cs (a # cs) xs) as'" .
with ‹a#xs = as''›[THEN sym]  ‹kind a = Q:r↪⇘p⇙fs›
show ?thesis by simp
qed
}
next
case (vpa_ReturnEmpty cs a as Q p f as'')
note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux [] xs›
note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux (upd_cs [] xs) ys›
{ case 1
from vpa_ReturnEmpty
have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')"
thus ?case
proof
assume "as'' = [] ∧ a#as = as'"
thus ?thesis by simp
next
assume "∃xs. a#xs = as'' ∧ as = xs@as'"
then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
from IH1[OF ‹as = xs@as'›] have "valid_path_aux [] xs" .
with ‹a#xs = as''›[THEN sym] ‹kind a = Q↩⇘p⇙f› ‹cs = []›
show ?thesis by simp
qed
next
case 2
from vpa_ReturnEmpty
have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')"
thus ?case
proof
assume "as'' = [] ∧ a#as = as'"
hence "as = []@tl as'" by(cases as') auto
from IH2[OF this] have "valid_path_aux [] (tl as')" by simp
with ‹as'' = [] ∧ a#as = as'› ‹kind a = Q↩⇘p⇙f› ‹cs = []›
show ?thesis by fastforce
next
assume "∃xs. a#xs = as'' ∧ as = xs@as'"
then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
from IH2[OF ‹as = xs@as'›] have "valid_path_aux (upd_cs [] xs) as'" .
from ‹a#xs = as''›[THEN sym] ‹kind a = Q↩⇘p⇙f› ‹cs = []›
have "upd_cs [] xs = upd_cs cs as''" by simp
with ‹valid_path_aux (upd_cs [] xs) as'› show ?thesis by simp
qed
}
next
case (vpa_ReturnCons cs a as Q p f c' cs' as'')
note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux cs' xs›
note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux (upd_cs cs' xs) ys›
{ case 1
from vpa_ReturnCons
have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')"
thus ?case
proof
assume "as'' = [] ∧ a#as = as'"
thus ?thesis by simp
next
assume "∃xs. a#xs = as'' ∧ as = xs@as'"
then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
from IH1[OF ‹as = xs@as'›] have "valid_path_aux cs' xs" .
with ‹a#xs = as''›[THEN sym] ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'›
‹a ∈ get_return_edges c'›
show ?thesis by simp
qed
next
case 2
from vpa_ReturnCons
have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')"
thus ?case
proof
assume "as'' = [] ∧ a#as = as'"
hence "as = []@tl as'" by(cases as') auto
from IH2[OF this] have "valid_path_aux (upd_cs cs' []) (tl as')" .
with ‹as'' = [] ∧ a#as = as'› ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'›
‹a ∈ get_return_edges c'›
show ?thesis by fastforce
next
assume "∃xs. a#xs = as'' ∧ as = xs@as'"
then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
from IH2[OF ‹as = xs@as'›] have "valid_path_aux (upd_cs cs' xs) as'" .
from ‹a#xs = as''›[THEN sym] ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'›
have "upd_cs cs' xs = upd_cs cs as''" by simp
with ‹valid_path_aux (upd_cs cs' xs) as'› show ?thesis by simp
qed
}
qed simp_all

lemma valid_path_aux_Append:
"⟦valid_path_aux cs as; valid_path_aux (upd_cs cs as) as'⟧
⟹ valid_path_aux cs (as@as')"
by(induct rule:vpa_induct,auto simp:intra_kind_def)

lemma vpa_snoc_Call:
assumes "kind a = Q:r↪⇘p⇙fs"
shows "valid_path_aux cs as ⟹ valid_path_aux cs (as@[a])"
proof(induct rule:vpa_induct)
case (vpa_empty cs)
from ‹kind a = Q:r↪⇘p⇙fs› have "valid_path_aux cs [a]" by simp
thus ?case by simp
next
case (vpa_intra cs a' as')
from ‹valid_path_aux cs (as'@[a])› ‹intra_kind (kind a')›
have "valid_path_aux cs (a'#(as'@[a]))"
by(fastforce simp:intra_kind_def)
thus ?case by simp
next
case (vpa_Call cs a' as' Q' r' p' fs')
from ‹valid_path_aux (a'#cs) (as'@[a])› ‹kind a' = Q':r'↪⇘p'⇙fs'›
have "valid_path_aux cs (a'#(as'@[a]))" by simp
thus ?case by simp
next
case (vpa_ReturnEmpty cs a' as' Q' p' f')
from ‹valid_path_aux [] (as'@[a])› ‹kind a' = Q'↩⇘p'⇙f'› ‹cs = []›
have "valid_path_aux cs (a'#(as'@[a]))" by simp
thus ?case by simp
next
case (vpa_ReturnCons cs a' as' Q' p' f' c' cs')
from ‹valid_path_aux cs' (as'@[a])› ‹kind a' = Q'↩⇘p'⇙f'› ‹cs = c'#cs'›
‹a' ∈ get_return_edges c'›
have "valid_path_aux cs (a'#(as'@[a]))" by simp
thus ?case by simp
qed

definition valid_path :: "'edge list ⇒ bool"
where "valid_path as ≡ valid_path_aux [] as"

lemma valid_path_aux_valid_path:
"valid_path_aux cs as ⟹ valid_path as"
by(fastforce intro:valid_path_aux_callstack_prefix simp:valid_path_def)

lemma valid_path_split:
assumes "valid_path (as@as')" shows "valid_path as" and "valid_path as'"
using ‹valid_path (as@as')›
apply(auto simp:valid_path_def)
apply(erule valid_path_aux_split)
apply(drule valid_path_aux_split(2))
by(fastforce intro:valid_path_aux_callstack_prefix)

definition valid_path' :: "'node ⇒ 'edge list ⇒ 'node ⇒ bool"
("_ -_→⇩√* _" [51,0,0] 80)
where vp_def:"n -as→⇩√* n' ≡ n -as→* n' ∧ valid_path as"

lemma intra_path_vp:
assumes "n -as→⇩ι* n'" shows "n -as→⇩√* n'"
proof -
from ‹n -as→⇩ι* n'› have "n -as→* n'" and "∀a ∈ set as. intra_kind(kind a)"
from ‹∀a ∈ set as. intra_kind(kind a)› have "valid_path_aux [] as"
by(rule valid_path_aux_intra_path)
thus ?thesis using ‹n -as→* n'› by(simp add:vp_def valid_path_def)
qed

lemma vp_split_Cons:
assumes "n -as→⇩√* n'" and "as ≠ []"
obtains a' as' where "as = a'#as'" and "n = sourcenode a'"
and "valid_edge a'" and "targetnode a' -as'→⇩√* n'"
proof(atomize_elim)
from ‹n -as→⇩√* n'› ‹as ≠ []› obtain a' as' where "as = a'#as'"
and "n = sourcenode a'" and "valid_edge a'" and "targetnode a' -as'→* n'"
by(fastforce elim:path_split_Cons simp:vp_def)
from ‹n -as→⇩√* n'› have "valid_path as" by(simp add:vp_def)
from ‹as = a'#as'› have "as = [a']@as'" by simp
with ‹valid_path as› have "valid_path ([a']@as')" by simp
hence "valid_path as'" by(rule valid_path_split)
with ‹targetnode a' -as'→* n'› have "targetnode a' -as'→⇩√* n'" by(simp add:vp_def)
with ‹as = a'#as'› ‹n = sourcenode a'› ‹valid_edge a'›
show "∃a' as'. as = a'#as' ∧ n = sourcenode a' ∧ valid_edge a' ∧
targetnode a' -as'→⇩√* n'" by blast
qed

lemma vp_split_snoc:
assumes "n -as→⇩√* n'" and "as ≠ []"
obtains a' as' where "as = as'@[a']" and "n -as'→⇩√* sourcenode a'"
and "valid_edge a'" and "n' = targetnode a'"
proof(atomize_elim)
from ‹n -as→⇩√* n'› ‹as ≠ []› obtain a' as' where "as = as'@[a']"
and "n -as'→* sourcenode a'" and "valid_edge a'" and "n' = targetnode a'"
by(clarsimp simp:vp_def)(erule path_split_snoc,auto)
from ‹n -as→⇩√* n'› ‹as = as'@[a']› have "valid_path (as'@[a'])" by(simp add:vp_def)
hence "valid_path as'" by(rule valid_path_split)
with ‹n -as'→* sourcenode a'› have "n -as'→⇩√* sourcenode a'" by(simp add:vp_def)
with ‹as = as'@[a']› ‹valid_edge a'› ‹n' = targetnode a'›
show "∃as' a'. as = as'@[a'] ∧ n -as'→⇩√* sourcenode a' ∧ valid_edge a' ∧
n' = targetnode a'"
by blast
qed

lemma vp_split:
assumes "n -as@a#as'→⇩√* n'"
shows "n -as→⇩√* sourcenode a" and "valid_edge a" and "targetnode a -as'→⇩√* n'"
proof -
from ‹n -as@a#as'→⇩√* n'› have "n -as→* sourcenode a" and "valid_edge a"
and "targetnode a -as'→* n'"
by(auto intro:path_split simp:vp_def)
from ‹n -as@a#as'→⇩√* n'› have "valid_path (as@a#as')" by(simp add:vp_def)
hence "valid_path as" and "valid_path (a#as')" by(auto intro:valid_path_split)
from ‹valid_path (a#as')› have "valid_path ([a]@as')" by simp
hence "valid_path as'"  by(rule valid_path_split)
with ‹n -as→* sourcenode a› ‹valid_path as› ‹valid_edge a› ‹targetnode a -as'→* n'›
show "n -as→⇩√* sourcenode a" "valid_edge a" "targetnode a -as'→⇩√* n'"
by(auto simp:vp_def)
qed

lemma vp_split_second:
assumes "n -as@a#as'→⇩√* n'" shows "sourcenode a -a#as'→⇩√* n'"
proof -
from ‹n -as@a#as'→⇩√* n'› have "sourcenode a -a#as'→* n'"
by(fastforce elim:path_split_second simp:vp_def)
from ‹n -as@a#as'→⇩√* n'› have "valid_path (as@a#as')" by(simp add:vp_def)
hence "valid_path (a#as')" by(rule valid_path_split)
with ‹sourcenode a -a#as'→* n'› show ?thesis by(simp add:vp_def)
qed

function valid_path_rev_aux :: "'edge list ⇒ 'edge list ⇒ bool"
where "valid_path_rev_aux cs [] ⟷ True"
| "valid_path_rev_aux cs (as@[a]) ⟷
(case (kind a) of Q↩⇘p⇙f ⇒ valid_path_rev_aux (a#cs) as
| Q:r↪⇘p⇙fs ⇒ case cs of [] ⇒ valid_path_rev_aux [] as
| c'#cs' ⇒ c' ∈ get_return_edges a ∧
valid_path_rev_aux cs' as
|    _ ⇒ valid_path_rev_aux cs as)"
by auto(case_tac b rule:rev_cases,auto)
termination by lexicographic_order

lemma vpra_induct [consumes 1,case_names vpra_empty vpra_intra vpra_Return
vpra_CallEmpty vpra_CallCons]:
assumes major: "valid_path_rev_aux xs ys"
and rules: "⋀cs. P cs []"
"⋀cs a as. ⟦intra_kind(kind a); valid_path_rev_aux cs as; P cs as⟧
⟹ P cs (as@[a])"
"⋀cs a as Q p f. ⟦kind a = Q↩⇘p⇙f; valid_path_rev_aux (a#cs) as; P (a#cs) as⟧
⟹ P cs (as@[a])"
"⋀cs a as Q r p fs. ⟦kind a = Q:r↪⇘p⇙fs; cs = []; valid_path_rev_aux [] as;
P [] as⟧ ⟹ P cs (as@[a])"
"⋀cs a as Q r p fs c' cs'. ⟦kind a = Q:r↪⇘p⇙fs; cs = c'#cs';
valid_path_rev_aux cs' as; c' ∈ get_return_edges a; P cs' as⟧
⟹ P cs (as@[a])"
shows "P xs ys"
using major
apply(induct ys arbitrary:xs rule:rev_induct)
by(auto intro:rules split:edge_kind.split_asm list.split_asm simp:intra_kind_def)

lemma vpra_callstack_prefix:
"valid_path_rev_aux (cs@cs') as ⟹ valid_path_rev_aux cs as"
proof(induct "cs@cs'" as arbitrary:cs cs' rule:vpra_induct)
case vpra_empty thus ?case by simp
next
case (vpra_intra a as)
hence "valid_path_rev_aux cs as" by simp
with ‹intra_kind (kind a)› show ?case by(fastforce simp:intra_kind_def)
next
case (vpra_Return a as Q p f)
note IH = ‹⋀ds ds'. a#cs@cs' = ds@ds' ⟹ valid_path_rev_aux ds as›
have "a#cs@cs' = (a#cs)@cs'" by simp
from IH[OF this] have "valid_path_rev_aux (a#cs) as" .
with ‹kind a = Q↩⇘p⇙f› show ?case by simp
next
case (vpra_CallEmpty a as Q r p fs)
hence "valid_path_rev_aux cs as" by simp
with ‹kind a = Q:r↪⇘p⇙fs› ‹cs@cs' = []› show ?case by simp
next
case (vpra_CallCons a as Q r p fs c' csx)
note IH = ‹⋀cs cs'. csx = cs@cs' ⟹ valid_path_rev_aux cs as›
from ‹cs@cs' = c'#csx›
have "(cs = [] ∧ cs' = c'#csx) ∨ (∃zs. cs = c'#zs ∧ zs@cs' = csx)"
thus ?case
proof
assume "cs = [] ∧ cs' = c'#csx"
hence "cs = []" and "cs' = c'#csx" by simp_all
from ‹cs' = c'#csx› have "csx = []@tl cs'" by simp
from IH[OF this] have "valid_path_rev_aux [] as" .
with ‹cs = []› ‹kind a = Q:r↪⇘p⇙fs› show ?thesis by simp
next
assume "∃zs. cs = c'#zs ∧ zs@cs' = csx"
then obtain zs where "cs = c'#zs" and "csx = zs@cs'" by auto
from IH[OF ‹csx = zs@cs'›] have "valid_path_rev_aux zs as" .
with ‹cs = c'#zs› ‹kind a = Q:r↪⇘p⇙fs› ‹c' ∈ get_return_edges a› show ?thesis by simp
qed
qed

function upd_rev_cs :: "'edge list ⇒ 'edge list ⇒ 'edge list"
where "upd_rev_cs cs [] = cs"
| "upd_rev_cs cs (as@[a]) =
(case (kind a) of Q↩⇘p⇙f ⇒ upd_rev_cs (a#cs) as
| Q:r↪⇘p⇙fs ⇒ case cs of [] ⇒ upd_rev_cs cs as
| c'#cs' ⇒ upd_rev_cs cs' as
|    _ ⇒ upd_rev_cs cs as)"
by auto(case_tac b rule:rev_cases,auto)
termination by lexicographic_order

lemma upd_rev_cs_empty [dest]:
"upd_rev_cs cs [] = [] ⟹ cs = []"
by(cases cs) auto

lemma valid_path_rev_aux_split:
assumes "valid_path_rev_aux cs (as@as')"
shows "valid_path_rev_aux cs as'" and "valid_path_rev_aux (upd_rev_cs cs as') as"
using ‹valid_path_rev_aux cs (as@as')›
proof(induct cs "as@as'" arbitrary:as as' rule:vpra_induct)
case (vpra_intra cs a as as'')
note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux cs ys›
note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux (upd_rev_cs cs ys) xs›
{ case 1
from vpra_intra
have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')"
by(cases as' rule:rev_cases) auto
thus ?case
proof
assume "as' = [] ∧ as@[a] = as''"
thus ?thesis by simp
next
assume "∃xs. as = as''@xs ∧ xs@[a] = as'"
then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
from IH1[OF ‹as = as''@xs›] have "valid_path_rev_aux cs xs" .
with ‹xs@[a] = as'› ‹intra_kind (kind a)›
show ?thesis by(fastforce simp:intra_kind_def)
qed
next
case 2
from vpra_intra
have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')"
by(cases as' rule:rev_cases) auto
thus ?case
proof
assume "as' = [] ∧ as@[a] = as''"
hence "as = butlast as''@[]" by(cases as) auto
from IH2[OF this] have "valid_path_rev_aux (upd_rev_cs cs []) (butlast as'')" .
with ‹as' = [] ∧ as@[a] = as''› ‹intra_kind (kind a)›
show ?thesis by(fastforce simp:intra_kind_def)
next
assume "∃xs. as = as''@xs ∧ xs@[a] = as'"
then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
from IH2[OF ‹as = as''@xs›] have "valid_path_rev_aux (upd_rev_cs cs xs) as''" .
from ‹xs@[a] = as'› ‹intra_kind (kind a)›
have "upd_rev_cs cs xs = upd_rev_cs cs as'" by(fastforce simp:intra_kind_def)
with ‹valid_path_rev_aux (upd_rev_cs cs xs) as''›
show ?thesis by simp
qed
}
next
case (vpra_Return cs a as Q p f as'')
note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux (a#cs) ys›
note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux (upd_rev_cs (a#cs) ys) xs›
{ case 1
from vpra_Return
have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')"
by(cases as' rule:rev_cases) auto
thus ?case
proof
assume "as' = [] ∧ as@[a] = as''"
thus ?thesis by simp
next
assume "∃xs. as = as''@xs ∧ xs@[a] = as'"
then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
from IH1[OF ‹as = as''@xs›] have "valid_path_rev_aux (a#cs) xs" .
with ‹xs@[a] = as'› ‹kind a = Q↩⇘p⇙f›
show ?thesis by fastforce
qed
next
case 2
from vpra_Return
have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')"
by(cases as' rule:rev_cases) auto
thus ?case
proof
assume "as' = [] ∧ as@[a] = as''"
hence "as = butlast as''@[]" by(cases as) auto
from IH2[OF this]
have "valid_path_rev_aux (upd_rev_cs (a#cs) []) (butlast as'')" .
with ‹as' = [] ∧ as@[a] = as''› ‹kind a = Q↩⇘p⇙f›
show ?thesis by fastforce
next
assume "∃xs. as = as''@xs ∧ xs@[a] = as'"
then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
from IH2[OF ‹as = as''@xs›]
have "valid_path_rev_aux (upd_rev_cs (a#cs) xs) as''" .
from ‹xs@[a] = as'› ‹kind a = Q↩⇘p⇙f›
have "upd_rev_cs (a#cs) xs = upd_rev_cs cs as'" by fastforce
with ‹valid_path_rev_aux (upd_rev_cs (a#cs) xs) as''›
show ?thesis by simp
qed
}
next
case (vpra_CallEmpty cs a as Q r p fs as'')
note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux [] ys›
note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux (upd_rev_cs [] ys) xs›
{ case 1
from vpra_CallEmpty
have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')"
by(cases as' rule:rev_cases) auto
thus ?case
proof
assume "as' = [] ∧ as@[a] = as''"
thus ?thesis by simp
next
assume "∃xs. as = as''@xs ∧ xs@[a] = as'"
then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
from IH1[OF ‹as = as''@xs›] have "valid_path_rev_aux [] xs" .
with ‹xs@[a] = as'› ‹kind a = Q:r↪⇘p⇙fs› ‹cs = []›
show ?thesis by fastforce
qed
next
case 2
from vpra_CallEmpty
have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')"
by(cases as' rule:rev_cases) auto
thus ?case
proof
assume "as' = [] ∧ as@[a] = as''"
hence "as = butlast as''@[]" by(cases as) auto
from IH2[OF this]
have "valid_path_rev_aux (upd_rev_cs [] []) (butlast as'')" .
with ‹as' = [] ∧ as@[a] = as''› ‹kind a = Q:r↪⇘p⇙fs› ‹cs = []›
show ?thesis by fastforce
next
assume "∃xs. as = as''@xs ∧ xs@[a] = as'"
then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
from IH2[OF ‹as = as''@xs›]
have "valid_path_rev_aux (upd_rev_cs [] xs) as''" .
with ‹xs@[a] = as'› ‹kind a = Q:r↪⇘p⇙fs› ‹cs = []›
show ?thesis by fastforce
qed
}
next
case (vpra_CallCons cs a as Q r p fs c' cs' as'')
note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux cs' ys›
note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux (upd_rev_cs cs' ys) xs›
{ case 1
from vpra_CallCons
have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')"
by(cases as' rule:rev_cases) auto
thus ?case
proof
assume "as' = [] ∧ as@[a] = as''"
thus ?thesis by simp
next
assume "∃xs. as = as''@xs ∧ xs@[a] = as'"
then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
from IH1[OF ‹as = as''@xs›] have "valid_path_rev_aux cs' xs" .
with ‹xs@[a] = as'› ‹kind a = Q:r↪⇘p⇙fs› ‹cs = c' # cs'› ‹c' ∈ get_return_edges a›
show ?thesis by fastforce
qed
next
case 2
from vpra_CallCons
have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')"
by(cases as' rule:rev_cases) auto
thus ?case
proof
assume "as' = [] ∧ as@[a] = as''"
hence "as = butlast as''@[]" by(cases as) auto
from IH2[OF this]
have "valid_path_rev_aux (upd_rev_cs cs' []) (butlast as'')" .
with ‹as' = [] ∧ as@[a] = as''› ‹kind a = Q:r↪⇘p⇙fs› ‹cs = c' # cs'›
‹c' ∈ get_return_edges a› show ?thesis by fastforce
next
assume "∃xs. as = as''@xs ∧ xs@[a] = as'"
then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
from IH2[OF ‹as = as''@xs›]
have "valid_path_rev_aux (upd_rev_cs cs' xs) as''" .
with ‹xs@[a] = as'› ‹kind a = Q:r↪⇘p⇙fs› ‹cs = c' # cs'›
‹c' ∈ get_return_edges a›
show ?thesis by fastforce
qed
}
qed simp_all

lemma valid_path_rev_aux_Append:
"⟦valid_path_rev_aux cs as'; valid_path_rev_aux (upd_rev_cs cs as') as⟧
⟹ valid_path_rev_aux cs (as@as')"
by(induct rule:vpra_induct,
auto simp:intra_kind_def simp del:append_assoc simp:append_assoc[THEN sym])

lemma vpra_Cons_intra:
assumes "intra_kind(kind a)"
shows "valid_path_rev_aux cs as ⟹ valid_path_rev_aux cs (a#as)"
proof(induct rule:vpra_induct)
case (vpra_empty cs)
have "valid_path_rev_aux cs []" by simp
with ‹intra_kind(kind a)› have "valid_path_rev_aux cs ([]@[a])"
by(simp only:valid_path_rev_aux.simps intra_kind_def,fastforce)
thus ?case by simp
qed(simp only:append_Cons[THEN sym] valid_path_rev_aux.simps intra_kind_def,fastforce)+

lemma vpra_Cons_Return:
assumes "kind a = Q↩⇘p⇙f"
shows "valid_path_rev_aux cs as ⟹ valid_path_rev_aux cs (a#as)"
proof(induct rule:vpra_induct)
case (vpra_empty cs)
from ‹kind a = Q↩⇘p⇙f› have "valid_path_rev_aux cs ([]@[a])"
by(simp only:valid_path_rev_aux.simps,clarsimp)
thus ?case by simp
next
case (vpra_intra cs a' as')
from ‹valid_path_rev_aux cs (a#as')› ‹intra_kind (kind a')›
have "valid_path_rev_aux cs ((a#as')@[a'])"
by(simp only:valid_path_rev_aux.simps,fastforce simp:intra_kind_def)
thus ?case by simp
next
case (vpra_Return cs a' as' Q' p' f')
from ‹valid_path_rev_aux (a'#cs) (a#as')› ‹kind a' = Q'↩⇘p'⇙f'›
have "valid_path_rev_aux cs ((a#as')@[a'])"
by(simp only:valid_path_rev_aux.simps,clarsimp)
thus ?case by simp
next
case (vpra_CallEmpty cs a' as' Q' r' p' fs')
from ‹valid_path_rev_aux [] (a#as')› ‹kind a' = Q':r'↪⇘p'⇙fs'› ‹cs = []›
have "valid_path_rev_aux cs ((a#as')@[a'])"
by(simp only:valid_path_rev_aux.simps,clarsimp)
thus ?case by simp
next
case (vpra_CallCons cs a' as' Q' r' p' fs' c' cs')
from ‹valid_path_rev_aux cs' (a#as')› ‹kind a' = Q':r'↪⇘p'⇙fs'› ‹cs = c'#cs'›
‹c' ∈ get_return_edges a'›
have "valid_path_rev_aux cs ((a#as')@[a'])"
by(simp only:valid_path_rev_aux.simps,clarsimp)
thus ?case by simp
qed

(*<*)
lemmas append_Cons_rev = append_Cons[THEN sym]
declare append_Cons [simp del] append_Cons_rev [simp]
(*>*)

lemma upd_rev_cs_Cons_intra:
assumes "intra_kind(kind a)" shows "upd_rev_cs cs (a#as) = upd_rev_cs cs as"
proof(induct as arbitrary:cs rule:rev_induct)
case Nil
from ‹intra_kind (kind a)›
have "upd_rev_cs cs ([]@[a]) = upd_rev_cs cs []"
by(simp only:upd_rev_cs.simps,auto simp:intra_kind_def)
thus ?case by simp
next
case (snoc a' as')
note IH = ‹⋀cs. upd_rev_cs cs (a#as') = upd_rev_cs cs as'›
show ?case
proof(cases "kind a'" rule:edge_kind_cases)
case Intra
from IH have "upd_rev_cs cs (a#as') = upd_rev_cs cs as'" .
with Intra have "upd_rev_cs cs ((a#as')@[a']) = upd_rev_cs cs (as'@[a'])"
by(fastforce simp:intra_kind_def)
thus ?thesis by simp
next
case Return
from IH have "upd_rev_cs (a'#cs) (a#as') = upd_rev_cs (a'#cs) as'" .
with Return have "upd_rev_cs cs ((a#as')@[a']) = upd_rev_cs cs (as'@[a'])"
by(auto simp:intra_kind_def)
thus ?thesis by simp
next
case Call
show ?thesis
proof(cases cs)
case Nil
from IH have "upd_rev_cs [] (a#as') = upd_rev_cs [] as'" .
with Call Nil have "upd_rev_cs cs ((a#as')@[a']) = upd_rev_cs cs (as'@[a'])"
by(auto simp:intra_kind_def)
thus ?thesis by simp
next
case (Cons c' cs')
from IH have "upd_rev_cs cs' (a#as') = upd_rev_cs cs' as'" .
with Call Cons have "upd_rev_cs cs ((a#as')@[a']) = upd_rev_cs cs (as'@[a'])"
by(auto simp:intra_kind_def)
thus ?thesis by simp
qed
qed
qed

lemma upd_rev_cs_Cons_Return:
assumes "kind a = Q↩⇘p⇙f" shows "upd_rev_cs cs (a#as) = a#(upd_rev_cs cs as)"
proof(induct as arbitrary:cs rule:rev_induct)
case Nil
with ‹kind a = Q↩⇘p⇙f› have "upd_rev_cs cs ([]@[a]) = a#(upd_rev_cs cs [])"
by(simp only:upd_rev_cs.simps) clarsimp
thus ?case by simp
next
case (snoc a' as')
note IH = ‹⋀cs. upd_rev_cs cs (a#as') = a#upd_rev_cs cs as'›
show ?case
proof(cases "kind a'" rule:edge_kind_cases)
case Intra
from IH have "upd_rev_cs cs (a#as') = a#(upd_rev_cs cs as')" .
with Intra have "upd_rev_cs cs ((a#as')@[a']) = a#(upd_rev_cs cs (as'@[a']))"
by(fastforce simp:intra_kind_def)
thus ?thesis by simp
next
case Return
from IH have "upd_rev_cs (a'#cs) (a#as') = a#(upd_rev_cs (a'#cs) as')" .
with Return have "upd_rev_cs cs ((a#as')@[a']) = a#(upd_rev_cs cs (as'@[a']))"
by(auto simp:intra_kind_def)
thus ?thesis by simp
next
case Call
show ?thesis
proof(cases cs)
case Nil
from IH have "upd_rev_cs [] (a#as') = a#(upd_rev_cs [] as')" .
with Call Nil have "upd_rev_cs cs ((a#as')@[a']) = a#(upd_rev_cs cs (as'@[a']))"
by(auto simp:intra_kind_def)
thus ?thesis by simp
next
case (Cons c' cs')
from IH have "upd_rev_cs cs' (a#as') = a#(upd_rev_cs cs' as')" .
with Call Cons
have "upd_rev_cs cs ((a#as')@[a']) = a#(upd_rev_cs cs (as'@[a']))"
by(auto simp:intra_kind_def)
thus ?thesis by simp
qed
qed
qed

lemma upd_rev_cs_Cons_Call_Cons:
assumes "kind a = Q:r↪⇘p⇙fs"
shows "upd_rev_cs cs as = c'#cs' ⟹ upd_rev_cs cs (a#as) = cs'"
proof(induct as arbitrary:cs rule:rev_induct)
case Nil
with ‹kind a = Q:r↪⇘p⇙fs› have "upd_rev_cs cs ([]@[a]) = cs'"
by(simp only:upd_rev_cs.simps) clarsimp
thus ?case by simp
next
case (snoc a' as')
note IH = ‹⋀cs. upd_rev_cs cs as' = c'#cs' ⟹ upd_rev_cs cs (a#as') = cs'›
show ?case
proof(cases "kind a'" rule:edge_kind_cases)
case Intra
with ‹upd_rev_cs cs (as'@[a']) = c'#cs'›
have "upd_rev_cs cs as' = c'#cs'" by(fastforce simp:intra_kind_def)
from IH[OF this] have "upd_rev_cs cs (a#as') = cs'" .
with Intra show ?thesis by(fastforce simp:intra_kind_def)
next
case Return
with ‹upd_rev_cs cs (as'@[a']) = c'#cs'›
have "upd_rev_cs (a'#cs) as' = c'#cs'" by simp
from IH[OF this] have "upd_rev_cs (a'#cs) (a#as') = cs'" .
with Return show ?thesis by simp
next
case Call
show ?thesis
proof(cases cs)
case Nil
with ‹upd_rev_cs cs (as'@[a']) = c'#cs'› Call
have "upd_rev_cs cs as' = c'#cs'" by simp
from IH[OF this] have "upd_rev_cs cs (a#as') = cs'" .
with Nil Call show ?thesis by simp
next
case (Cons cx csx)
with ‹upd_rev_cs cs (as'@[a']) = c'#cs'› Call
have "upd_rev_cs csx as' = c'#cs'" by simp
from IH[OF this] have "upd_rev_cs csx (a#as') = cs'" .
with Cons Call show ?thesis by simp
qed
qed
qed

lemma upd_rev_cs_Cons_Call_Cons_Empty:
assumes "kind a = Q:r↪⇘p⇙fs"
shows "upd_rev_cs cs as = [] ⟹ upd_rev_cs cs (a#as) = []"
proof(induct as arbitrary:cs rule:rev_induct)
case Nil
with ‹kind a = Q:r↪⇘p⇙fs› have "upd_rev_cs cs ([]@[a]) = []"
by(simp only:upd_rev_cs.simps) clarsimp
thus ?case by simp
next
case (snoc a' as')
note IH = ‹⋀cs. upd_rev_cs cs as' = [] ⟹ upd_rev_cs cs (a#as') = []›
show ?case
proof(cases "kind a'" rule:edge_kind_cases)
case Intra
with ‹upd_rev_cs cs (as'@[a']) = []›
have "upd_rev_cs cs as' = []" by(fastforce simp:intra_kind_def)
from IH[OF this] have "upd_rev_cs cs (a#as') = []" .
with Intra show ?thesis by(fastforce simp:intra_kind_def)
next
case Return
with ‹upd_rev_cs cs (as'@[a']) = []›
have "upd_rev_cs (a'#cs) as' = []" by simp
from IH[OF this] have "upd_rev_cs (a'#cs) (a#as') = []" .
with Return show ?thesis by simp
next
case Call
show ?thesis
proof(cases cs)
case Nil
with ‹upd_rev_cs cs (as'@[a']) = []› Call
have "upd_rev_cs cs as' = []" by simp
from IH[OF this] have "upd_rev_cs cs (a#as') = []" .
with Nil Call show ?thesis by simp
next
case (Cons cx csx)
with ‹upd_rev_cs cs (as'@[a']) = []› Call
have "upd_rev_cs csx as' = []" by simp
from IH[OF this] have "upd_rev_cs csx (a#as') = []" .
with Cons Call show ?thesis by simp
qed
qed
qed

(*<*)declare append_Cons [simp] append_Cons_rev [simp del](*>*)

definition valid_call_list :: "'edge list ⇒ 'node ⇒ bool"
where "valid_call_list cs n ≡
∀cs' c cs''. cs = cs'@c#cs'' ⟶ (valid_edge c ∧ (∃Q r p fs. (kind c = Q:r↪⇘p⇙fs) ∧
p = get_proc (case cs' of [] ⇒ n | _ ⇒ last (sourcenodes cs'))))"

definition valid_return_list :: "'edge list ⇒ 'node ⇒ bool"
where "valid_return_list cs n ≡
∀cs' c cs''. cs = cs'@c#cs'' ⟶ (valid_edge c ∧ (∃Q p f. (kind c = Q↩⇘p⇙f) ∧
p = get_proc (case cs' of [] ⇒ n | _ ⇒ last (targetnodes cs'))))"

lemma valid_call_list_valid_edges:
assumes "valid_call_list cs n" shows "∀c ∈ set cs. valid_edge c"
proof -
from ‹valid_call_list cs n›
have "∀cs' c cs''. cs = cs'@c#cs'' ⟶ valid_edge c"
thus ?thesis
proof(induct cs)
case Nil thus ?case by simp
next
case (Cons cx csx)
note IH = ‹∀cs' c cs''. csx = cs'@c#cs'' ⟶ valid_edge c ⟹
∀a∈set csx. valid_edge a›
from ‹∀cs' c cs''. cx#csx = cs'@c#cs'' ⟶ valid_edge c›
have "valid_edge cx" by blast
from ‹∀cs' c cs''. cx#csx = cs'@c#cs'' ⟶ valid_edge c›
have "∀cs' c cs''. csx = cs'@c#cs'' ⟶ valid_edge c"
by auto(erule_tac x="cx#cs'" in allE,auto)
from IH[OF this] ‹valid_edge cx› show ?case by simp
qed
qed

lemma valid_return_list_valid_edges:
assumes "valid_return_list rs n" shows "∀r ∈ set rs. valid_edge r"
proof -
from ‹valid_return_list rs n›
have "∀rs' r rs''. rs = rs'@r#rs'' ⟶ valid_edge r"
thus ?thesis
proof(induct rs)
case Nil thus ?case by simp
next
case (Cons rx rsx)
note IH = ‹∀rs' r rs''. rsx = rs'@r#rs'' ⟶ valid_edge r ⟹
∀a∈set rsx. valid_edge a›
from ‹∀rs' r rs''. rx#rsx = rs'@r#rs'' ⟶ valid_edge r›
have "valid_edge rx" by blast
from ‹∀rs' r rs''. rx#rsx = rs'@r#rs'' ⟶ valid_edge r›
have "∀rs' r rs''. rsx = rs'@r#rs'' ⟶ valid_edge r"
by auto(erule_tac x="rx#rs'" in allE,auto)
from IH[OF this] ‹valid_edge rx› show ?case by simp
qed
qed

lemma vpra_empty_valid_call_list_rev:
"valid_call_list cs n ⟹ valid_path_rev_aux [] (rev cs)"
proof(induct cs arbitrary:n)
case Nil thus ?case by simp
next
case (Cons c' cs')
note IH = ‹⋀n. valid_call_list cs' n ⟹ valid_path_rev_aux [] (rev cs')›
from ‹valid_call_list (c'#cs') n› have "valid_call_list cs' (sourcenode c')"
apply(clarsimp simp:valid_call_list_def)
apply hypsubst_thin
apply(erule_tac x="c'#cs'" in allE)
apply clarsimp
by(case_tac cs',auto simp:sourcenodes_def)
from IH[OF this] have "valid_path_rev_aux [] (rev cs')" .
moreover
from ‹valid_call_list (c'#cs') n› obtain Q r p fs where "kind c' = Q:r↪⇘p⇙fs"
apply(clarsimp simp:valid_call_list_def)
by(erule_tac x="[]" in allE) fastforce
ultimately show ?case by simp
qed

lemma vpa_upd_cs_cases:
"⟦valid_path_aux cs as; valid_call_list cs n; n -as→* n'⟧
⟹ case (upd_cs cs as) of [] ⇒ (∀c ∈ set cs. ∃a ∈ set as. a ∈ get_return_edges c)
| cx#csx ⇒ valid_call_list (cx#csx) n'"
proof(induct arbitrary:n rule:vpa_induct)
case (vpa_empty cs)
from ‹n -[]→* n'› have "n = n'" by fastforce
with ‹valid_call_list cs n› show ?case by(cases cs) auto
next
case (vpa_intra cs a' as')
note IH = ‹⋀n. ⟦valid_call_list cs n; n -as'→* n'⟧
⟹ case (upd_cs cs as') of [] ⇒ ∀c∈set cs. ∃a∈set as'. a ∈ get_return_edges c
| cx#csx ⇒ valid_call_list (cx # csx) n'›
from ‹intra_kind (kind a')› have "upd_cs cs (a'#as') = upd_cs cs as'"
by(fastforce simp:intra_kind_def)
from ‹n -a'#as'→* n'› have [simp]:"n = sourcenode a'" and "valid_edge a'"
and "targetnode a' -as'→* n'" by(auto elim:path_split_Cons)
from ‹valid_edge a'› ‹intra_kind (kind a')›
have "get_proc (sourcenode a') = get_proc (targetnode a')" by(rule get_proc_intra)
with ‹valid_call_list cs n› have "valid_call_list cs (targetnode a')"
apply(clarsimp simp:valid_call_list_def)
apply(erule_tac x="cs'" in allE) apply clarsimp
by(case_tac cs') auto
from IH[OF this ‹targetnode a' -as'→* n'›] ‹upd_cs cs (a'#as') = upd_cs cs as'›
show ?case by(cases "upd_cs cs as'") auto
next
case (vpa_Call cs a' as' Q r p fs)
note IH = ‹⋀n. ⟦valid_call_list (a'#cs) n; n -as'→* n'⟧
⟹ case (upd_cs (a'#cs) as')
of [] ⇒ ∀c∈set (a'#cs). ∃a∈set as'. a ∈ get_return_edges c
| cx#csx ⇒ valid_call_list (cx # csx) n'›
from ‹kind a' = Q:r↪⇘p⇙fs› have "upd_cs (a'#cs) as' = upd_cs cs (a'#as')"
by simp
from ‹n -a'#as'→* n'› have [simp]:"n = sourcenode a'" and "valid_edge a'"
and "targetnode a' -as'→* n'" by(auto elim:path_split_Cons)
from ‹valid_edge a'› ‹kind a' = Q:r↪⇘p⇙fs›
have "get_proc (targetnode a') = p" by(rule get_proc_call)
with ‹valid_edge a'› ‹kind a' = Q:r↪⇘p⇙fs› ‹valid_call_list cs n›
have "valid_call_list (a'#cs) (targetnode a')"
apply(clarsimp simp:valid_call_list_def)
apply(case_tac cs') apply auto
apply(erule_tac x="list" in allE) apply clarsimp
by(case_tac list,auto simp:sourcenodes_def)
from IH[OF this ‹targetnode a' -as'→* n'›]
‹upd_cs (a'#cs) as' = upd_cs cs (a'#as')›
have "case upd_cs cs (a'#as')
of [] ⇒ ∀c∈set (a' # cs). ∃a∈set as'. a ∈ get_return_edges c
| cx # csx ⇒ valid_call_list (cx # csx) n'" by simp
thus ?case by(cases "upd_cs cs (a'#as')") simp+
next
case (vpa_ReturnEmpty cs a' as' Q p f)
note IH = ‹⋀n. ⟦valid_call_list [] n; n -as'→* n'⟧
⟹ case (upd_cs [] as')
of [] ⇒ ∀c∈set []. ∃a∈set as'. a ∈ get_return_edges c
| cx#csx ⇒ valid_call_list (cx # csx) n'›
from ‹kind a' = Q↩⇘p⇙f› ‹cs = []› have "upd_cs [] as' = upd_cs cs (a'#as')"
by simp
from ‹n -a'#as'→* n'› have [simp]:"n = sourcenode a'" and "valid_edge a'"
and "targetnode a' -as'→* n'" by(auto elim:path_split_Cons)
have "valid_call_list [] (targetnode a')" by(simp add:valid_call_list_def)
from IH[OF this ‹targetnode a' -as'→* n'›]
‹upd_cs [] as' = upd_cs cs (a'#as')›
have "case (upd_cs cs (a'#as'))
of [] ⇒ ∀c∈set []. ∃a∈set as'. a ∈ get_return_edges c
| cx#csx ⇒ valid_call_list (cx#csx) n'" by simp
with ‹cs = []› show ?case by(cases "upd_cs cs (a'#as')") simp+
next
case (vpa_ReturnCons cs a' as' Q p f c' cs')
note IH = ‹⋀n. ⟦valid_call_list cs' n; n -as'→* n'⟧
⟹ case (upd_cs cs' as')
of [] ⇒ ∀c∈set cs'. ∃a∈set as'. a ∈ get_return_edges c
| cx#csx ⇒ valid_call_list (cx # csx) n'›
from ‹kind a' = Q↩⇘p⇙f› ‹cs = c'#cs'› ‹a' ∈ get_return_edges c'›
have "upd_cs cs' as' = upd_cs cs (a'#as')" by simp
from ‹n -a'#as'→* n'› have [simp]:"n = sourcenode a'" and "valid_edge a'"
and "targetnode a' -as'→* n'" by(auto elim:path_split_Cons)
from ‹valid_call_list cs n› ‹cs = c'#cs'› have "valid_edge c'"
apply(clarsimp simp:valid_call_list_def)
by(erule_tac x="[]" in allE,auto)
with ‹a' ∈ get_return_edges c'› obtain ax where "valid_edge ax"
and sources:"sourcenode ax = sourcenode c'"
and targets:"targetnode ax = targetnode a'" and "kind ax = (λcf. False)⇩√"
by(fastforce dest:call_return_node_edge)
from ‹valid_edge ax› sources[THEN sym] targets[THEN sym] ‹kind ax = (λcf. False)⇩√›
have "get_proc (sourcenode c') = get_proc (targetnode a')"
by(fastforce intro:get_proc_intra simp:intra_kind_def)
with ‹valid_call_list cs n› ‹cs = c'#cs'›
have "valid_call_list cs' (targetnode a')"
apply(clarsimp simp:valid_call_list_def)
apply(hypsubst_thin)
apply(erule_tac x="c'#cs'" in allE)
by(case_tac cs',auto simp:sourcenodes_def)
from IH[OF this ‹targetnode a' -as'→* n'›]
‹upd_cs cs' as' = upd_cs cs (a'#as')›
have "case (upd_cs cs (a'#as'))
of [] ⇒ ∀c∈set cs'. ∃a∈set as'. a ∈ get_return_edges c
| cx#csx ⇒ valid_call_list (cx#csx) n'" by simp
with ‹cs = c' # cs'› ‹a' ∈ get_return_edges c'› show ?case
by(cases "upd_cs cs (a'#as')") simp+
qed

lemma vpa_valid_call_list_valid_return_list_vpra:
"⟦valid_path_aux cs cs'; valid_call_list cs n; valid_return_list cs' n'⟧
⟹ valid_path_rev_aux cs' (rev cs)"
proof(induct arbitrary:n n' rule:vpa_induct)
case (vpa_empty cs)
from ‹valid_call_list cs n› show ?case by(rule vpra_empty_valid_call_list_rev)
next
case (vpa_intra cs a as)
from ‹intra_kind (kind a)› ‹valid_return_list (a#as) n'›
have False apply(clarsimp simp:valid_return_list_def)
by(erule_tac x="[]" in allE,clarsimp simp:intra_kind_def)
thus ?case by simp
next
case (vpa_Call cs a as Q r p fs)
from ‹kind a = Q:r↪⇘p⇙fs› ‹valid_return_list (a#as) n'›
have False apply(clarsimp simp:valid_return_list_def)
by(erule_tac x="[]" in allE,clarsimp)
thus ?case by simp
next
case (vpa_ReturnEmpty cs a as Q p f)
from ‹cs = []› show ?case by simp
next
case (vpa_ReturnCons cs a as Q p f c' cs')
note IH = ‹⋀n n'. ⟦valid_call_list cs' n; valid_return_list as n'⟧
⟹ valid_path_rev_aux as (rev cs')›
from ‹valid_return_list (a#as) n'› have "valid_return_list as (targetnode a)"
apply(clarsimp simp:valid_return_list_def)
apply(erule_tac x="a#cs'" in allE)
by(case_tac cs',auto simp:targetnodes_def)
from ‹valid_call_list cs n› ‹cs = c'#cs'›
have "valid_call_list cs' (sourcenode c')"
apply(clarsimp simp:valid_call_list_def)
apply(erule_tac x="c'#cs'" in allE)
by(case_tac cs',auto simp:sourcenodes_def)
from ‹valid_call_list cs n› ‹cs = c'#cs'› have "valid_edge c'"
apply(clarsimp simp:valid_call_list_def)
by(erule_tac x="[]" in allE,auto)
with ‹a ∈ get_return_edges c'› obtain Q' r' p' f' where "kind c' = Q':r'↪⇘p'⇙f'"
apply(cases "kind c'" rule:edge_kind_cases)
by(auto dest:only_call_get_return_edges simp:intra_kind_def)
from IH[OF ‹valid_call_list cs' (sourcenode c')›
‹valid_return_list as (targetnode a)›]
have "valid_path_rev_aux as (rev cs')" .
with ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'› ‹a ∈ get_return_edges c'› ‹kind c' = Q':r'↪⇘p'⇙f'›
show ?case by simp
qed

lemma vpa_to_vpra:
"⟦valid_path_aux cs as; valid_path_aux (upd_cs cs as) cs';
n -as→* n'; valid_call_list cs n; valid_return_list cs' n''⟧
⟹ valid_path_rev_aux cs' as ∧ valid_path_rev_aux (upd_rev_cs cs' as) (rev cs)"
proof(induct arbitrary:n rule:vpa_induct)
case vpa_empty thus ?case
by(fastforce intro:vpa_valid_call_list_valid_return_list_vpra)
next
case (vpa_intra cs a as)
note IH = ‹⋀n. ⟦valid_path_aux (upd_cs cs as) cs'; n -as→* n';
valid_call_list cs n; valid_return_list cs' n''⟧
⟹ valid_path_rev_aux cs' as ∧
valid_path_rev_aux (upd_rev_cs cs' as) (rev cs)›
from ‹n -a#as→* n'› have "n = sourcenode a" and "valid_edge a"
and "targetnode a -as→* n'" by(auto intro:path_split_Cons)
from ‹valid_edge a› ‹intra_kind (kind a)›
have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
with ‹valid_call_list cs n› ‹n = sourcenode a›
have "valid_call_list cs (targetnode a)"
apply(clarsimp simp:valid_call_list_def)
apply(erule_tac x="cs'" in allE) apply clarsimp
by(case_tac cs') auto
from ‹valid_path_aux (upd_cs cs (a#as)) cs'› ‹intra_kind (kind a)›
have "valid_path_aux (upd_cs cs as) cs'"
by(fastforce simp:intra_kind_def)
from IH[OF this ‹targetnode a -as→* n'› ‹valid_call_list cs (targetnode a)›
‹valid_return_list cs' n''›]
have "valid_path_rev_aux cs' as"
and "valid_path_rev_aux (upd_rev_cs cs' as) (rev cs)" by simp_all
from  ‹intra_kind (kind a)› ‹valid_path_rev_aux cs' as›
have "valid_path_rev_aux cs' (a#as)" by(rule vpra_Cons_intra)
from ‹intra_kind (kind a)› have "upd_rev_cs cs' (a#as) = upd_rev_cs cs' as"
with ‹valid_path_rev_aux (upd_rev_cs cs' as) (rev cs)›
have "valid_path_rev_aux (upd_rev_cs cs' (a#as)) (rev cs)" by simp
with ‹valid_path_rev_aux cs' (a#as)› show ?case by simp
next
case (vpa_Call cs a as Q r p fs)
note IH = ‹⋀n. ⟦valid_path_aux (upd_cs (a#cs) as) cs'; n -as→* n';
valid_call_list (a#cs) n; valid_return_list cs' n''⟧
⟹ valid_path_rev_aux cs' as ∧
valid_path_rev_aux (upd_rev_cs cs' as) (rev (a#cs))›
from ‹n -a#as→* n'› have "n = sourcenode a" and "valid_edge a"
and "targetnode a -as→* n'" by(auto intro:path_split_Cons)
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "p = get_proc (targetnode a)"
by(rule get_proc_call[THEN sym])
from ‹valid_call_list cs n› ‹n = sourcenode a›
have "valid_call_list cs (sourcenode a)" by simp
with ‹kind a = Q:r↪⇘p⇙fs› ‹valid_edge a› ‹p = get_proc (targetnode a)›
have "valid_call_list (a#cs) (targetnode a)"
apply(clarsimp simp:valid_call_list_def)
apply(case_tac cs') apply auto
apply(erule_tac x="list" in allE) apply clarsimp
by(case_tac list,auto simp:sourcenodes_def)
from ‹kind a = Q:r↪⇘p⇙fs› have "upd_cs cs (a#as) = upd_cs (a#cs) as"
by simp
with ‹valid_path_aux (upd_cs cs (a#as)) cs'›
have "valid_path_aux (upd_cs (a#cs) as) cs'" by simp
from IH[OF this ‹targetnode a -as→* n'› ‹valid_call_list (a#cs) (targetnode a)›
‹valid_return_list cs' n''›]
have "valid_path_rev_aux cs' as"
and "valid_path_rev_aux (upd_rev_cs cs' as) (rev (a#cs))" by simp_all
show ?case
proof(cases "upd_rev_cs cs' as")
case Nil
with ‹kind a = Q:r↪⇘p⇙fs›
have "upd_rev_cs cs' (a#as) = []" by(rule upd_rev_cs_Cons_Call_Cons_Empty)
with ‹valid_path_rev_aux (upd_rev_cs cs' as) (rev (a#cs))› ‹kind a = Q:r↪⇘p⇙fs› Nil
have "valid_path_rev_aux (upd_rev_cs cs' (a#as)) (rev cs)" by simp
from Nil ‹kind a = Q:r↪⇘p⇙fs› have "valid_path_rev_aux (upd_rev_cs cs' as) ([]@[a])"
by(simp only:valid_path_rev_aux.simps) clarsimp
with ‹valid_path_rev_aux cs' as› have "valid_path_rev_aux cs' ([a]@as)"
by(fastforce intro:valid_path_rev_aux_Append)
with ‹valid_path_rev_aux (upd_rev_cs cs' (a#as)) (rev cs)›
show ?thesis by simp
next
case (Cons cx csx)
with ‹valid_path_rev_aux (upd_rev_cs cs' as) (rev (a#cs))› ‹kind a = Q:r↪⇘p⇙fs›
have match:"cx ∈ get_return_edges a" "valid_path_rev_aux csx (rev cs)" by auto
from ‹kind a = Q:r↪⇘p⇙fs› Cons have "upd_rev_cs cs' (a#as) = csx"
by(rule upd_rev_cs_Cons_Call_Cons)
with ‹valid_path_rev_aux (upd_rev_cs cs' as) (rev(a#cs))› ‹kind a = Q:r↪⇘p⇙fs› match
have "valid_path_rev_aux (upd_rev_cs cs' (a#as)) (rev cs)" by simp
from Cons ‹kind a = Q:r↪⇘p⇙fs› match
have "valid_path_rev_aux (upd_rev_cs cs' as) ([]@[a])"
by(simp only:valid_path_rev_aux.simps) clarsimp
with ‹valid_path_rev_aux cs' as› have "valid_path_rev_aux cs' ([a]@as)"
by(fastforce intro:valid_path_rev_aux_Append)
with ‹valid_path_rev_aux (upd_rev_cs cs' (a#as)) (rev cs)›
show ?thesis by simp
qed
next
case (vpa_ReturnEmpty cs a as Q p f)
note IH = ‹⋀n. ⟦valid_path_aux (upd_cs [] as) cs'; n -as→* n';
valid_call_list [] n; valid_return_list cs' n''⟧
⟹ valid_path_rev_aux cs' as ∧
valid_path_rev_aux (upd_rev_cs cs' as) (rev [])›
from ‹n -a#as→* n'› have "n = sourcenode a" and "valid_edge a"
and "targetnode a -as→* n'" by(auto intro:path_split_Cons)
from ‹cs = []› ‹kind a = Q↩⇘p⇙f› have "upd_cs cs (a#as) = upd_cs [] as"
by simp
with ‹valid_path_aux (upd_cs cs (a#as)) cs'›
have "valid_path_aux (upd_cs [] as) cs'" by simp
from IH[OF this ‹targetnode a -as→* n'› _ ‹valid_return_list cs' n''›]
have "valid_path_rev_aux cs' as"
and "valid_path_rev_aux (upd_rev_cs cs' as) (rev [])"
by(auto simp:valid_call_list_def)
from ‹kind a = Q↩⇘p⇙f› ‹valid_path_rev_aux cs' as›
have "valid_path_rev_aux cs' (a#as)" by(rule vpra_Cons_Return)
moreover
from ‹cs = []› have "valid_path_rev_aux (upd_rev_cs cs' (a#as)) (rev cs)"
by simp
ultimately show ?case by simp
next
case (vpa_ReturnCons cs a as Q p f cx csx)
note IH = ‹⋀n. ⟦valid_path_aux (upd_cs csx as) cs'; n -as→* n';
valid_call_list csx n; valid_return_list cs' n''⟧
⟹ valid_path_rev_aux cs' as ∧
valid_path_rev_aux (upd_rev_cs cs' as) (rev csx)›
note match = ‹cs = cx#csx› ‹a ∈ get_return_edges cx›
from ‹n -a#as→* n'› have "n = sourcenode a" and "valid_edge a"
and "targetnode a -as→* n'" by(auto intro:path_split_Cons)
from ‹cs = cx#csx› ‹valid_call_list cs n› have "valid_edge cx"
apply(clarsimp simp:valid_call_list_def)
by(erule_tac x="[]" in allE) clarsimp
with match have "get_proc (sourcenode cx) = get_proc (targetnode a)"
by(fastforce intro:get_proc_get_return_edge)
with ‹valid_call_list cs n› ‹cs = cx#csx›
have "valid_call_list csx (targetnode a)"
apply(clarsimp simp:valid_call_list_def)
apply(erule_tac x="cx#cs'" in allE) apply clarsimp
by(case_tac cs',auto simp:sourcenodes_def)
from ‹kind a = Q↩⇘p⇙f› match have "upd_cs cs (a#as) = upd_cs csx as" by simp
with ‹valid_path_aux (upd_cs cs (a#as)) cs'›
have "valid_path_aux (upd_cs csx as) cs'" by simp
from IH[OF this ‹targetnode a -as→* n'› ‹valid_call_list csx (targetnode a)›
‹valid_return_list cs' n''›]
have "valid_path_rev_aux cs' as"
and "valid_path_rev_aux (upd_rev_cs cs' as) (rev csx)" by simp_all
from ‹kind a = Q↩⇘p⇙f› ‹valid_path_rev_aux cs' as›
have "valid_path_rev_aux cs' (a#as)" by(rule vpra_Cons_Return)
from match ‹valid_edge cx› obtain Q' r' p' f' where "kind cx = Q':r'↪⇘p'⇙f'"
by(fastforce dest!:only_call_get_return_edges)
from ‹kind a = Q↩⇘p⇙f› have "upd_rev_cs cs' (a#as) = a#(upd_rev_cs cs' as)"
by(rule upd_rev_cs_Cons_Return)
with ‹valid_path_rev_aux (upd_rev_cs cs' as) (rev csx)› ‹kind a = Q↩⇘p⇙f›
‹kind cx = Q':r'↪⇘p'⇙f'› match
have "valid_path_rev_aux (upd_rev_cs cs' (a#as)) (rev cs)"
by simp
with ‹valid_path_rev_aux cs' (a#as)› show ?case by simp
qed

lemma vp_to_vpra:
"n -as→⇩√* n' ⟹ valid_path_rev_aux [] as"
by(fastforce elim:vpa_to_vpra[THEN conjunct1]
simp:vp_def valid_path_def valid_call_list_def valid_return_list_def)

subsubsection ‹Same level paths›

fun same_level_path_aux :: "'edge list ⇒ 'edge list ⇒ bool"
where "same_level_path_aux cs [] ⟷ True"
| "same_level_path_aux cs (a#as) ⟷
(case (kind a) of Q:r↪⇘p⇙fs ⇒ same_level_path_aux (a#cs) as
| Q↩⇘p⇙f ⇒ case cs of [] ⇒ False
| c'#cs' ⇒ a ∈ get_return_edges c' ∧
same_level_path_aux cs' as
|    _ ⇒ same_level_path_aux cs as)"

lemma slpa_induct [consumes 1,case_names slpa_empty slpa_intra slpa_Call
slpa_Return]:
assumes major: "same_level_path_aux xs ys"
and rules: "⋀cs. P cs []"
"⋀cs a as. ⟦intra_kind(kind a); same_level_path_aux cs as; P cs as⟧
⟹ P cs (a#as)"
"⋀cs a as Q r p fs. ⟦kind a = Q:r↪⇘p⇙fs; same_level_path_aux (a#cs) as; P (a#cs) as⟧
⟹ P cs (a#as)"
"⋀cs a as Q p f c' cs'. ⟦kind a = Q↩⇘p⇙f; cs = c'#cs'; same_level_path_aux cs' as;
a ∈ get_return_edges c'; P cs' as⟧
⟹ P cs (a#as)"
shows "P xs ys"
using major
apply(induct ys arbitrary: xs)
by(auto intro:rules split:edge_kind.split_asm list.split_asm simp:intra_kind_def)

lemma slpa_cases [consumes 4,case_names intra_path return_intra_path]:
assumes "same_level_path_aux cs as" and "upd_cs cs as = []"
and "∀c ∈ set cs. valid_edge c" and "∀a ∈ set as. valid_edge a"
obtains "∀a ∈ set as. intra_kind(kind a)"
| asx a asx' Q p f c' cs' where "as = asx@a#asx'" and "same_level_path_aux cs asx"
and "kind a = Q↩⇘p⇙f" and "upd_cs cs asx = c'#cs'" and "upd_cs cs (asx@[a]) = []"
and "a ∈ get_return_edges c'" and "valid_edge c'"
and "∀a ∈ set asx'. intra_kind(kind a)"
proof(atomize_elim)
from assms
show "(∀a∈set as. intra_kind (kind a)) ∨
(∃asx a asx' Q p f c' cs'. as = asx@a#asx' ∧ same_level_path_aux cs asx ∧
kind a = Q↩⇘p⇙f ∧ upd_cs cs asx = c'#cs' ∧ upd_cs cs (asx@[a]) = [] ∧
a ∈ get_return_edges c' ∧ valid_edge c' ∧ (∀a∈set asx'. intra_kind (kind a)))"
proof(induct rule:slpa_induct)
case (slpa_empty cs)
have "∀a∈set []. intra_kind (kind a)" by simp
thus ?case by simp
next
case (slpa_intra cs a as)
note IH = ‹⟦upd_cs cs as = []; ∀c∈set cs. valid_edge c; ∀a'∈set as. valid_edge a'⟧
⟹ (∀a∈set as. intra_kind (kind a)) ∨
(∃asx a asx' Q p f c' cs'. as = asx@a#asx' ∧ same_level_path_aux cs asx ∧
kind a = Q↩⇘p⇙f ∧  upd_cs cs asx = c' # cs' ∧ upd_cs cs (asx@[a]) = [] ∧
a ∈ get_return_edges c' ∧ valid_edge c' ∧ (∀a∈set asx'. intra_kind (kind a)))›
from ‹∀a'∈set (a#as). valid_edge a'› have "∀a'∈set as. valid_edge a'" by simp
from ‹intra_kind (kind a)› ‹upd_cs cs (a#as) = []›
have "upd_cs cs as = []" by(fastforce simp:intra_kind_def)
from IH[OF this ‹∀c∈set cs. valid_edge c› ‹∀a'∈set as. valid_edge a'›] show ?case
proof
assume "∀a∈set as. intra_kind (kind a)"
with ‹intra_kind (kind a)› have "∀a'∈set (a#as). intra_kind (kind a')"
by simp
thus ?case by simp
next
assume "∃asx a asx' Q p f c' cs'. as = asx@a#asx' ∧ same_level_path_aux cs asx ∧
kind a = Q↩⇘p⇙f ∧ upd_cs cs asx = c'#cs' ∧ upd_cs cs (asx@[a]) = [] ∧
a ∈ get_return_edges c' ∧ valid_edge c' ∧
(∀a∈set asx'. intra_kind (kind a))"
then obtain asx a' Q p f asx' c' cs' where "as = asx@a'#asx'"
and "same_level_path_aux cs asx" and "upd_cs cs (asx@[a']) = []"
and "upd_cs cs asx = c'#cs'" and assms:"a' ∈ get_return_edges c'"
"kind a' = Q↩⇘p⇙f" "valid_edge c'" "∀a∈set asx'. intra_kind (kind a)"
by blast
from ‹as = asx@a'#asx'› have "a#as = (a#asx)@a'#asx'" by simp
moreover
from ‹intra_kind (kind a)› ‹same_level_path_aux cs asx›
have "same_level_path_aux cs (a#asx)" by(fastforce simp:intra_kind_def)
moreover
from ‹upd_cs cs asx = c'#cs'› ‹intra_kind (kind a)›
have "upd_cs cs (a#asx) = c'#cs'" by(fastforce simp:intra_kind_def)
moreover
from ‹upd_cs cs (asx@[a']) = []› ‹intra_kind (kind a)›
have "upd_cs cs ((a#asx)@[a']) = []" by(fastforce simp:intra_kind_def)
ultimately show ?case using assms by blast
qed
next
case (slpa_Call cs a as Q r p fs)
note IH = ‹⟦upd_cs (a#cs) as = []; ∀c∈set (a#cs). valid_edge c;
∀a'∈set as. valid_edge a'⟧ ⟹
(∀a'∈set as. intra_kind (kind a')) ∨
(∃asx a' asx' Q' p' f' c' cs'. as = asx@a'#asx' ∧
same_level_path_aux (a#cs) asx ∧ kind a' = Q'↩⇘p'⇙f' ∧
upd_cs (a#cs) asx = c'#cs' ∧ upd_cs (a#cs) (asx@[a']) = [] ∧
a' ∈ get_return_edges c' ∧ valid_edge c' ∧
(∀a'∈set asx'. intra_kind (kind a')))›
from ‹∀a'∈set (a#as). valid_edge a'› have "valid_edge a"
and "∀a'∈set as. valid_edge a'" by simp_all
from ‹∀c∈set cs. valid_edge c› ‹valid_edge a› have "∀c∈set (a#cs). valid_edge c"
by simp
from ‹upd_cs cs (a#as) = []› ‹kind a = Q:r↪⇘p⇙fs›
have "upd_cs (a#cs) as = []" by simp
from IH[OF this ‹∀c∈set (a#cs). valid_edge c› ‹∀a'∈set as. valid_edge a'›]
show ?case
proof
assume "∀a'∈set as. intra_kind (kind a')"
with ‹kind a = Q:r↪⇘p⇙fs› have "upd_cs cs (a#as) = a#cs"
by(fastforce intro:upd_cs_intra_path)
with ‹upd_cs cs (a#as) = []› have False by simp
thus ?case by simp
next
assume "∃asx a' asx' Q p f c' cs'. as = asx@a'#asx' ∧
same_level_path_aux (a#cs) asx ∧ kind a' = Q↩⇘p⇙f ∧
upd_cs (a#cs) asx = c'#cs' ∧ upd_cs (a#cs) (asx@[a']) = [] ∧
a' ∈ get_return_edges c' ∧ valid_edge c' ∧
(∀a∈set asx'. intra_kind (kind a))"
then obtain asx a' Q' p' f' asx' c' cs' where "as = asx@a'#asx'"
and "same_level_path_aux (a#cs) asx" and "upd_cs (a#cs) (asx@[a']) = []"
and "upd_cs (a#cs) asx = c'#cs'" and assms:"a' ∈ get_return_edges c'"
"kind a' = Q'↩⇘p'⇙f'" "valid_edge c'" "∀a∈set asx'. intra_kind (kind a)"
by blast
from ‹as = asx@a'#asx'› have "a#as = (a#asx)@a'#asx'" by simp
moreover
from ‹kind a = Q:r↪⇘p⇙fs› ‹same_level_path_aux (a#cs) asx›
have "same_level_path_aux cs (a#asx)" by simp
moreover
from ‹kind a = Q:r↪⇘p⇙fs› ‹upd_cs (a#cs) asx = c'#cs'›
have "upd_cs cs (a#asx) = c'#cs'" by simp
moreover
from ‹kind a = Q:r↪⇘p⇙fs› ‹upd_cs (a#cs) (asx@[a']) = []›
have "upd_cs cs ((a#asx)@[a']) = []" by simp
ultimately show ?case using assms by blast
qed
next
case (slpa_Return cs a as Q p f c' cs')
note IH = ‹⟦upd_cs cs' as = []; ∀c∈set cs'. valid_edge c;
∀a'∈set as. valid_edge a'⟧ ⟹
(∀a'∈set as. intra_kind (kind a')) ∨
(∃asx a' asx' Q' p' f' c'' cs''. as = asx@a'#asx' ∧
same_level_path_aux cs' asx ∧ kind a' = Q'↩⇘p'⇙f' ∧ upd_cs cs' asx = c''#cs'' ∧
upd_cs cs' (asx@[a']) = [] ∧ a' ∈ get_return_edges c'' ∧ valid_edge c'' ∧
(∀a'∈set asx'. intra_kind (kind a')))›
from ‹∀a'∈set (a#as). valid_edge a'› have "valid_edge a"
and "∀a'∈set as. valid_edge a'" by simp_all
from ‹∀c∈set cs. valid_edge c› ‹cs = c' # cs'›
have "valid_edge c'" and "∀c∈set cs'. valid_edge c" by simp_all
from ‹upd_cs cs (a#as) = []› ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'›
‹a ∈ get_return_edges c'› have "upd_cs cs' as = []" by simp
from IH[OF this ‹∀c∈set cs'. valid_edge c› ‹∀a'∈set as. valid_edge a'›] show ?case
proof
assume "∀a'∈set as. intra_kind (kind a')"
hence "upd_cs cs' as = cs'" by(rule upd_cs_intra_path)
with ‹upd_cs cs' as = []› have "cs' = []" by simp
with ‹cs = c'#cs'› ‹a ∈ get_return_edges c'› ‹kind a = Q↩⇘p⇙f›
have "upd_cs cs [a] = []" by simp
moreover
from ‹cs = c'#cs'› have "upd_cs cs [] ≠ []" by simp
moreover
have "same_level_path_aux cs []" by simp
ultimately show ?case
using ‹kind a = Q↩⇘p⇙f› ‹∀a'∈set as. intra_kind (kind a')› ‹cs = c'#cs'›
‹a ∈ get_return_edges c'› ‹valid_edge c'›
by fastforce
next
assume "∃asx a' asx' Q' p' f' c'' cs''. as = asx@a'#asx' ∧
same_level_path_aux cs' asx ∧ kind a' = Q'↩⇘p'⇙f' ∧ upd_cs cs' asx = c''#cs'' ∧
upd_cs cs' (asx@[a']) = [] ∧ a' ∈ get_return_edges c'' ∧ valid_edge c'' ∧
(∀a'∈set asx'. intra_kind (kind a'))"
then obtain asx a' asx' Q' p' f' c'' cs'' where "as = asx@a'#asx'"
and "same_level_path_aux cs' asx" and "upd_cs cs' asx = c''#cs''"
and "upd_cs cs' (asx@[a']) = []" and assms:"a' ∈ get_return_edges c''"
"kind a' = Q'↩⇘p'⇙f'" "valid_edge c''" "∀a'∈set asx'. intra_kind (kind a')"
by blast
from ‹as = asx@a'#asx'› have "a#as = (a#asx)@a'#asx'" by simp
moreover
from ‹same_level_path_aux cs' asx› ‹cs = c'#cs'› ‹a ∈ get_return_edges c'›
‹kind a = Q↩⇘p⇙f›
have "same_level_path_aux cs (a#asx)" by simp
moreover
from ‹upd_cs cs' asx = c''#cs''› ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'›
have "upd_cs cs (a#asx) = c''#cs''" by simp
moreover
from ‹upd_cs cs' (asx@[a']) = []› ‹cs = c'#cs'› ‹a ∈ get_return_edges c'›
‹kind a = Q↩⇘p⇙f›
have "upd_cs cs ((a#asx)@[a']) = []" by simp
ultimately show ?case using assms by blast
qed
qed
qed

lemma same_level_path_aux_valid_path_aux:
"same_level_path_aux cs as ⟹ valid_path_aux cs as"
by(induct rule:slpa_induct,auto split:edge_kind.split simp:intra_kind_def)

lemma same_level_path_aux_Append:
"⟦same_level_path_aux cs as; same_level_path_aux (upd_cs cs as) as'⟧
⟹ same_level_path_aux cs (as@as')"
by(induct rule:slpa_induct,auto simp:intra_kind_def)

lemma same_level_path_aux_callstack_Append:
"same_level_path_aux cs as ⟹ same_level_path_aux (cs@cs') as"
by(induct rule:slpa_induct,auto simp:intra_kind_def)

lemma same_level_path_upd_cs_callstack_Append:
"⟦same_level_path_aux cs as; upd_cs cs as = cs'⟧
⟹ upd_cs (cs@cs'') as = (cs'@cs'')"
by(induct rule:slpa_induct,auto split:edge_kind.split simp:intra_kind_def)

lemma slpa_split:
assumes "same_level_path_aux cs as" and "as = xs@ys" and "upd_cs cs xs = []"
shows "same_level_path_aux cs xs" and "same_level_path_aux [] ys"
using assms
proof(induct arbitrary:xs ys rule:slpa_induct)
case (slpa_empty cs) case 1
from ‹[] = xs@ys› show ?case by simp
next
case (slpa_empty cs) case 2
from ‹[] = xs@ys› show ?case by simp
next
case (slpa_intra cs a as)
note IH1 = ‹⋀xs ys. ⟦as = xs@ys; upd_cs cs xs = []⟧ ⟹ same_level_path_aux cs xs›
note IH2 = ‹⋀xs ys. ⟦as = xs@ys; upd_cs cs xs = []⟧ ⟹ same_level_path_aux [] ys›
{ case 1
show ?case
proof(cases xs)
case Nil thus ?thesis by simp
next
case (Cons x' xs')
with ‹a#as = xs@ys› have "a = x'" and "as = xs'@ys" by simp_all
with ‹upd_cs cs xs = []› Cons ‹intra_kind (kind a)›
have "upd_cs cs xs' = []" by(fastforce simp:intra_kind_def)
from IH1[OF ‹as = xs'@ys› this] have "same_level_path_aux cs xs'" .
with ‹a = x'› ‹intra_kind (kind a)› Cons
show ?thesis by(fastforce simp:intra_kind_def)
qed
next
case 2
show ?case
proof(cases xs)
case Nil
with ‹upd_cs cs xs = []› have "cs = []" by fastforce
with Nil ‹a#as = xs@ys› ‹same_level_path_aux cs as› ‹intra_kind (kind a)›
show ?thesis by(cases ys,auto simp:intra_kind_def)
next
case (Cons x' xs')
with ‹a#as = xs@ys› have "a = x'" and "as = xs'@ys" by simp_all
with ‹upd_cs cs xs = []› Cons ‹intra_kind (kind a)›
have "upd_cs cs xs' = []" by(fastforce simp:intra_kind_def)
from IH2[OF ‹as = xs'@ys› this] show ?thesis .
qed
}
next
case (slpa_Call cs a as Q r p fs)
note IH1 = ‹⋀xs ys. ⟦as = xs@ys; upd_cs (a#cs) xs = []⟧
⟹ same_level_path_aux (a#cs) xs›
note IH2 = ‹⋀xs ys. ⟦as = xs@ys; upd_cs (a#cs) xs = []⟧
⟹ same_level_path_aux [] ys›
{ case 1
show ?case
proof(cases xs)
case Nil thus ?thesis by simp
next
case (Cons x' xs')
with ‹a#as = xs@ys› have "a = x'" and "as = xs'@ys" by simp_all
with ‹upd_cs cs xs = []› Cons ‹kind a = Q:r↪⇘p⇙fs›
have "upd_cs (a#cs) xs' = []" by simp
from IH1[OF ‹as = xs'@ys› this] have "same_level_path_aux (a#cs) xs'" .
with ‹a = x'› ‹kind a = Q:r↪⇘p⇙fs› Cons show ?thesis by simp
qed
next
case 2
show ?case
proof(cases xs)
case Nil
with ‹upd_cs cs xs = []› have "cs = []" by fastforce
with Nil ‹a#as = xs@ys› ‹same_level_path_aux (a#cs) as› ‹kind a = Q:r↪⇘p⇙fs›
show ?thesis by(cases ys) auto
next
case (Cons x' xs')
with ‹a#as = xs@ys› have "a = x'" and "as = xs'@ys" by simp_all
with ‹upd_cs cs xs = []› Cons ‹kind a = Q:r↪⇘p⇙fs›
have "upd_cs (a#cs) xs' = []" by simp
from IH2[OF ‹as = xs'@ys› this] show ?thesis .
qed
}
next
case (slpa_Return cs a as Q p f c' cs')
note IH1 = ‹⋀xs ys. ⟦as = xs@ys; upd_cs cs' xs = []⟧ ⟹ same_level_path_aux cs' xs›
note IH2 = ‹⋀xs ys. ⟦as = xs@ys; upd_cs cs' xs = []⟧ ⟹ same_level_path_aux [] ys›
{ case 1
show ?case
proof(cases xs)
case Nil thus ?thesis by simp
next
case (Cons x' xs')
with ‹a#as = xs@ys› have "a = x'" and "as = xs'@ys" by simp_all
with ‹upd_cs cs xs = []› Cons ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'›
have "upd_cs cs' xs' = []" by simp
from IH1[OF ‹as = xs'@ys› this] have "same_level_path_aux cs' xs'" .
with ‹a = x'› ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'› ‹a ∈ get_return_edges c'› Cons
show ?thesis by simp
qed
next
case 2
show ?case
proof(cases xs)
case Nil
with ‹upd_cs cs xs = []› have "cs = []" by fastforce
with ‹cs = c'#cs'› have False by simp
thus ?thesis by simp
next
case (Cons x' xs')
with ‹a#as = xs@ys› have "a = x'" and "as = xs'@ys" by simp_all
with ‹upd_cs cs xs = []› Cons ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'›
have "upd_cs cs' xs' = []" by simp
from IH2[OF ‹as = xs'@ys› this] show ?thesis .
qed
}
qed

lemma slpa_number_Calls_eq_number_Returns:
"⟦same_level_path_aux cs as; upd_cs cs as = [];
∀a ∈ set as. valid_edge a; ∀c ∈ set cs. valid_edge c⟧
⟹ length [a←as@cs. ∃Q r p fs. kind a = Q:r↪⇘p⇙fs] =
length [a←as. ∃Q p f. kind a = Q↩⇘p⇙f]"
apply(induct rule:slpa_induct)
by(auto split:list.split edge_kind.split intro:only_call_get_return_edges
simp:intra_kind_def)

lemma slpa_get_proc:
"⟦same_level_path_aux cs as; upd_cs cs as = []; n -as→* n';
∀c ∈ set cs. valid_edge c⟧
⟹ (if cs = [] then get_proc n else get_proc(last(sourcenodes cs))) = get_proc n'"
proof(induct arbitrary:n rule:slpa_induct)
case slpa_empty thus ?case by fastforce
next
case (slpa_intra cs a as)
note IH = ‹⋀n. ⟦upd_cs cs as = []; n -as→* n'; ∀a∈set cs. valid_edge a⟧
⟹ (if cs = [] then get_proc n else get_proc (last (sourcenodes cs))) =
get_proc n'›
from ‹intra_kind (kind a)› ‹upd_cs cs (a#as) = []›
have "upd_cs cs as = []" by(cases "kind a",auto simp:intra_kind_def)
from ‹n -a#as→* n'› have "n -[]@a#as→* n'" by simp
hence "valid_edge a" and "n = sourcenode a" and "targetnode a -as→* n'"
by(fastforce dest:path_split)+
from ‹valid_edge a› ‹intra_kind (kind a)› ‹ n = sourcenode a›
have "get_proc n = get_proc (targetnode a)"
by(fastforce intro:get_proc_intra)
from IH[OF ‹upd_cs cs as = []› ‹targetnode a -as→* n'› ‹∀a∈set cs. valid_edge a›]
have "(if cs = [] then get_proc (targetnode a)
else get_proc (last (sourcenodes cs))) = get_proc n'" .
with ‹get_proc n = get_proc (targetnode a)› show ?case by auto
next
case (slpa_Call cs a as Q r p fs)
note IH = ‹⋀n. ⟦upd_cs (a#cs) as = []; n -as→* n'; ∀a∈set (a#cs). valid_edge a⟧
⟹ (if a#cs = [] then get_proc n else get_proc (last (sourcenodes (a#cs)))) =
get_proc n'›
from ‹kind a = Q:r↪⇘p⇙fs› ‹upd_cs cs (a#as) = []›
have "upd_cs (a#cs) as = []" by simp
from ‹n -a#as→* n'› have "n -[]@a#as→* n'" by simp
hence "valid_edge a" and "n = sourcenode a" and "targetnode a -as→* n'"
by(fastforce dest:path_split)+
from ‹valid_edge a› ‹∀a∈set cs. valid_edge a› have "∀a∈set (a#cs). valid_edge a"
by simp
from IH[OF ‹upd_cs (a#cs) as = []› ‹targetnode a -as→* n'› this]
have "get_proc (last (sourcenodes (a#cs))) = get_proc n'" by simp
with ‹n = sourcenode a› show ?case by(cases cs,auto simp:sourcenodes_def)
next
case (slpa_Return cs a as Q p f c' cs')
note IH = ‹⋀n. ⟦upd_cs cs' as = []; n -as→* n'; ∀a∈set cs'. valid_edge a⟧
⟹ (if cs' = [] then get_proc n else get_proc (last (sourcenodes cs'))) =
get_proc n'›
from ‹∀a∈set cs. valid_edge a› ‹cs = c'#cs'›
have "valid_edge c'" and "∀a∈set cs'. valid_edge a" by simp_all
from ‹kind a = Q↩⇘p⇙f› ‹upd_cs cs (a#as) = []› ‹cs = c'#cs'›
have "upd_cs cs' as = []" by simp
from ‹n -a#as→* n'› have "n -[]@a#as→* n'" by simp
hence "n = sourcenode a" and "targetnode a -as→* n'"
by(fastforce dest:path_split)+
from ‹valid_edge c'› ‹a ∈ get_return_edges c'›
have "get_proc (sourcenode c') = get_proc (targetnode a)"
by(rule get_proc_get_return_edge)
from IH[OF ‹upd_cs cs' as = []› ‹targetnode a -as→* n'› ‹∀a∈set cs'. valid_edge a›]
have "(if cs' = [] then get_proc (targetnode a)
else get_proc (last (sourcenodes cs'))) = get_proc n'" .
with ‹cs = c'#cs'› ‹get_proc (sourcenode c') = get_proc (targetnode a)›
show ?case by(auto simp:sourcenodes_def)
qed

lemma slpa_get_return_edges:
"⟦same_level_path_aux cs as; cs ≠ []; upd_cs cs as = [];
∀xs ys. as = xs@ys ∧ ys ≠ [] ⟶ upd_cs cs xs ≠ []⟧
⟹ last as ∈ get_return_edges (last cs)"
proof(induct rule:slpa_induct)
case (slpa_empty cs)
from ‹cs ≠ []› ‹upd_cs cs [] = []› have False by fastforce
thus ?case by simp
next
case (slpa_intra cs a as)
note IH = ‹⟦cs ≠ []; upd_cs cs as = [];
∀xs ys. as = xs@ys ∧ ys ≠ [] ⟶ upd_cs cs xs ≠ []⟧
⟹ last as ∈ get_return_edges (last cs)›
show ?case
proof(cases "as = []")
case True
with ‹intra_kind (kind a)› ‹upd_cs cs (a#as) = []› have "cs = []"
by(fastforce simp:intra_kind_def)
with ‹cs ≠ []› have False by simp
thus ?thesis by simp
next
case False
from ‹intra_kind (kind a)› ‹upd_cs cs (a#as) = []› have "upd_cs cs as = []"
by(fastforce simp:intra_kind_def)
from ‹∀xs ys. a#as = xs@ys ∧ ys ≠ [] ⟶ upd_cs cs xs ≠ []› ‹intra_kind (kind a)›
have "∀xs ys. as = xs@ys ∧ ys ≠ [] ⟶ upd_cs cs xs ≠ []"
apply(clarsimp,erule_tac x="a#xs" in allE)
by(auto simp:intra_kind_def)
from IH[OF ‹cs ≠ []› ‹upd_cs cs as = []› this]
have "last as ∈ get_return_edges (last cs)" .
with False show ?thesis by simp
qed
next
case (slpa_Call cs a as Q r p fs)
note IH = ‹⟦a#cs ≠ []; upd_cs (a#cs) as = [];
∀xs ys. as = xs@ys ∧ ys ≠ [] ⟶ upd_cs (a#cs) xs ≠ []⟧
⟹ last as ∈ get_return_edges (last (a#cs))›
show ?case
proof(cases "as = []")
case True
with ‹kind a = Q:r↪⇘p⇙fs› ‹upd_cs cs (a#as) = []› have "a#cs = []" by simp
thus ?thesis by simp
next
case False
from ‹kind a = Q:r↪⇘p⇙fs› ‹upd_cs cs (a#as) = []› have "upd_cs (a#cs) as = []"
by simp
from ‹∀xs ys. a#as = xs@ys ∧ ys ≠ [] ⟶ upd_cs cs xs ≠ []› ‹kind a = Q:r↪⇘p⇙fs›
have "∀xs ys. as = xs@ys ∧ ys ≠ [] ⟶ upd_cs (a#cs) xs ≠ []"
by(clarsimp,erule_tac x="a#xs" in allE,simp)
from IH[OF _ ‹upd_cs (a#cs) as = []› this]
have "last as ∈ get_return_edges (last (a#cs))" by simp
with False ‹cs ≠ []› show ?thesis by(simp add:targetnodes_def)
qed
next
case (slpa_Return cs a as Q p f c' cs')
note IH = ‹⟦cs' ≠ []; upd_cs cs' as = [];
∀xs ys. as = xs@ys ∧ ys ≠ [] ⟶ upd_cs cs' xs ≠ []⟧
⟹ last as ∈ get_return_edges (last cs')›
show ?case
proof(cases "as = []")
case True
with ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'› ‹upd_cs cs (a#as) = []›
have "cs' = []" by simp
with ‹cs = c'#cs'› ‹a ∈ get_return_edges c'› True
show ?thesis by simp
next
case False
from ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'› ‹upd_cs cs (a#as) = []›
have "upd_cs cs' as = []" by simp
show ?thesis
proof(cases "cs' = []")
case True
with ‹cs = c'#cs'› ‹kind a = Q↩⇘p⇙f› have "upd_cs cs [a] = []" by simp
with ‹∀xs ys. a#as = xs@ys ∧ ys ≠ [] ⟶ upd_cs cs xs ≠ []› False have False
apply(erule_tac x="[a]" in allE) by fastforce
thus ?thesis by simp
next
case False
from ‹∀xs ys. a#as = xs@ys ∧ ys ≠ [] ⟶ upd_cs cs xs ≠ []›
‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'›
have "∀xs ys. as = xs@ys ∧ ys ≠ [] ⟶ upd_cs cs' xs ≠ []"
by(clarsimp,erule_tac x="a#xs" in allE,simp)
from IH[OF False ‹upd_cs cs' as = []› this]
have "last as ∈ get_return_edges (last cs')" .
with ‹as ≠ []› False ‹cs = c'#cs'› show ?thesis by(simp add:targetnodes_def)
qed
qed
qed

lemma slpa_callstack_length:
assumes "same_level_path_aux cs as" and "length cs = length cfsx"
obtains cfx cfsx' where "transfers (kinds as) (cfsx@cf#cfs) = cfsx'@cfx#cfs"
and "transfers (kinds as) (cfsx@cf#cfs') = cfsx'@cfx#cfs'"
and "length cfsx' = length (upd_cs cs as)"
proof(atomize_elim)
from assms show "∃cfsx' cfx. transfers (kinds as) (cfsx@cf#cfs) = cfsx'@cfx#cfs ∧
transfers (kinds as) (cfsx@cf#cfs') = cfsx'@cfx#cfs' ∧
length cfsx' = length (upd_cs cs as)"
proof(induct arbitrary:cfsx cf rule:slpa_induct)
case (slpa_empty cs) thus ?case by(simp add:kinds_def)
next
case (slpa_intra cs a as)
note IH = ‹⋀cfsx cf. length cs = length cfsx ⟹
∃cfsx' cfx. transfers (kinds as) (cfsx@cf#cfs) = cfsx'@cfx#cfs ∧
transfers (kinds as) (cfsx@cf#cfs') = cfsx'@cfx#cfs' ∧
length cfsx' = length (upd_cs cs as)›
from ‹intra_kind (kind a)›
have "length (upd_cs cs (a#as)) = length (upd_cs cs as)"
by(fastforce simp:intra_kind_def)
show ?case
proof(cases cfsx)
case Nil
with ‹length cs = length cfsx› have "length cs = length []" by simp
from Nil ‹intra_kind (kind a)›
obtain cfx where transfer:"transfer (kind a) (cfsx@cf#cfs) = []@cfx#cfs"
"transfer (kind a) (cfsx@cf#cfs') = []@cfx#cfs'"
by(cases "kind a",auto simp:kinds_def intra_kind_def)
from IH[OF ‹length cs = length []›] obtain cfsx' cfx'
where "transfers (kinds as) ([]@cfx#cfs) = cfsx'@cfx'#cfs"
and "transfers (kinds as) ([]@cfx#cfs') = cfsx'@cfx'#cfs'"
and "length cfsx' = length (upd_cs cs as)" by blast
with ‹length (upd_cs cs (a#as)) = length (upd_cs cs as)› transfer
show ?thesis by(fastforce simp:kinds_def)
next
case (Cons x xs)
with ‹intra_kind (kind a)› obtain cfx'
where transfer:"transfer (kind a) (cfsx@cf#cfs) = (cfx'#xs)@cf#cfs"
"transfer (kind a) (cfsx@cf#cfs') = (cfx'#xs)@cf#cfs'"
by(cases "kind a",auto simp:kinds_def intra_kind_def)
from ‹length cs = length cfsx› Cons have "length cs = length (cfx'#xs)"
by simp
from IH[OF this] obtain cfs'' cf''
where "transfers (kinds as) ((cfx'#xs)@cf#cfs) = cfs''@cf''#cfs"
and "transfers (kinds as) ((cfx'#xs)@cf#cfs') = cfs''@cf''#cfs'"
and "length cfs'' = length (upd_cs cs as)" by blast
with ‹length (upd_cs cs (a#as)) = length (upd_cs cs as)› transfer
show ?thesis by(fastforce simp:kinds_def)
qed
next
case (slpa_Call cs a as Q r p fs)
note IH = ‹⋀cfsx cf. length (a#cs) = length cfsx ⟹
∃cfsx' cfx. transfers (kinds as) (cfsx@cf#cfs) = cfsx'@cfx#cfs ∧
transfers (kinds as) (cfsx@cf#cfs') = cfsx'@cfx#cfs' ∧
length cfsx' = length (upd_cs (a#cs) as)›
from ‹kind a = Q:r↪⇘p⇙fs›
obtain cfx where transfer:"transfer (kind a) (cfsx@cf#cfs) = (cfx#cfsx)@cf#cfs"
"transfer (kind a) (cfsx@cf#cfs') = (cfx#cfsx)@cf#cfs'"
by(cases cfsx) auto
from ‹length cs = length cfsx› have "length (a#cs) = length (cfx#cfsx)"
by simp
from IH[OF this] obtain cfsx' cfx'
where "transfers (kinds as) ((cfx#cfsx)@cf#cfs) = cfsx'@cfx'#cfs"
and "transfers (kinds as) ((cfx#cfsx)@cf#cfs') = cfsx'@cfx'#cfs'"
and "length cfsx' = length (upd_cs (a#cs) as)" by blast
with ‹kind a = Q:r↪⇘p⇙fs› transfer show ?case by(fastforce simp:kinds_def)
next
case (slpa_Return cs a as Q p f c' cs')
note IH = ‹⋀cfsx cf. length cs' = length cfsx ⟹
∃cfsx' cfx. transfers (kinds as) (cfsx@cf#cfs) = cfsx'@cfx#cfs ∧
transfers (kinds as) (cfsx@cf#cfs') = cfsx'@cfx#cfs' ∧
length cfsx' = length (upd_cs cs' as)›
from ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'›
have "length (upd_cs cs (a#as)) = length (upd_cs cs' as)" by simp
show ?case
proof(cases cs')
case Nil
with ‹cs = c'#cs'› ‹length cs = length cfsx› obtain cfx
where [simp]:"cfsx = [cfx]" by(cases cfsx) auto
with ‹kind a = Q↩⇘p⇙f› obtain cf'
where transfer:"transfer (kind a) (cfsx@cf#cfs) = []@cf'#cfs"
"transfer (kind a) (cfsx@cf#cfs') = []@cf'#cfs'"
by fastforce
from Nil have "length cs' = length []" by simp
from IH[OF this] obtain cfsx' cfx'
where "transfers (kinds as) ([]@cf'#cfs) = cfsx'@cfx'#cfs"
and "transfers (kinds as) ([]@cf'#cfs') = cfsx'@cfx'#cfs'"
and "length cfsx' = length (upd_cs cs' as)" by blast
with ‹length (upd_cs cs (a#as)) = length (upd_cs cs' as)› transfer
show ?thesis by(fastforce simp:kinds_def)
next
case (Cons cx csx)
with ‹cs = c'#cs'› ‹length cs = length cfsx› obtain x x' xs
where [simp]:"cfsx = x#x'#xs" and "length xs = length csx"
by(cases cfsx,auto,case_tac list,fastforce+)
with ‹kind a = Q↩⇘p⇙f› obtain cf'
where transfer:"transfer (kind a) ((x#x'#xs)@cf#cfs) = (cf'#xs)@cf#cfs"
"transfer (kind a) ((x#x'#xs)@cf#cfs') = (cf'#xs)@cf#cfs'"
by fastforce
from ‹cs = c'#cs'› ‹length cs = length cfsx› have "length cs' = length (cf'#xs)"
by simp
from IH[OF this] obtain cfsx' cfx
where "transfers (kinds as) ((cf'#xs)@cf#cfs) = cfsx'@cfx#cfs"
and "transfers (kinds as) ((cf'#xs)@cf#cfs') = cfsx'@cfx#cfs'"
and "length cfsx' = length (upd_cs cs' as)" by blast
with ‹length (upd_cs cs (a#as)) = length (upd_cs cs' as)› transfer
show ?thesis by(fastforce simp:kinds_def)
qed
qed
qed

lemma slpa_snoc_intra:
"⟦same_level_path_aux cs as; intra_kind (kind a)⟧
⟹ same_level_path_aux cs (as@[a])"
by(induct rule:slpa_induct,auto simp:intra_kind_def)

lemma slpa_snoc_Call:
"⟦same_level_path_aux cs as; kind a = Q:r↪⇘p⇙fs⟧
⟹ same_level_path_aux cs (as@[a])"
by(induct rule:slpa_induct,auto simp:intra_kind_def)

lemma vpa_Main_slpa:
"⟦valid_path_aux cs as; m -as→* m'; as ≠ [];
valid_call_list cs m; get_proc m' = Main;
get_proc (case cs of [] ⇒ m | _ ⇒ sourcenode (last cs)) = Main⟧
⟹ same_level_path_aux cs as ∧ upd_cs cs as = []"
proof(induct arbitrary:m rule:vpa_induct)
case (vpa_empty cs) thus ?case by simp
next
case (vpa_intra cs a as)
note IH = ‹⋀m. ⟦m -as→* m'; as ≠ []; valid_call_list cs m; get_proc m' = Main;
get_proc (case cs of [] ⇒ m | a # list ⇒ sourcenode (last cs)) = Main⟧
⟹ same_level_path_aux cs as ∧ upd_cs cs as = []›
from ‹m -a # as→* m'› have "sourcenode a = m" and "valid_edge a"
and "targetnode a -as→* m'" by(auto elim:path_split_Cons)
from ‹valid_edge a› ‹intra_kind (kind a)›
have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
show ?case
proof(cases "as = []")
case True
with ‹targetnode a -as→* m'› have "targetnode a = m'" by fastforce
with ‹get_proc (sourcenode a) = get_proc (targetnode a)›
‹sourcenode a = m› ‹get_proc m' = Main›
have "get_proc m = Main" by simp
have "cs = []"
proof(cases cs)
case Cons
with ‹valid_call_list cs m›
obtain c Q r p fs where "valid_edge c" and "kind c = Q:r↪⇘get_proc m⇙fs"
by(auto simp:valid_call_list_def,erule_tac x="[]" in allE,
auto simp:sourcenodes_def)
with ‹get_proc m = Main› have "kind c = Q:r↪⇘Main⇙fs" by simp
with ‹valid_edge c› have False by(rule Main_no_call_target)
thus ?thesis by simp
qed simp
with True ‹intra_kind (kind a)› show ?thesis by(fastforce simp:intra_kind_def)
next
case False
from ‹valid_call_list cs m› ‹sourcenode a = m›
‹get_proc (sourcenode a) = get_proc (targetnode a)›
have "valid_call_list cs (targetnode a)"
apply(clarsimp simp:valid_call_list_def)
apply(erule_tac x="cs'" in allE)
apply(erule_tac x="c" in allE)
by(auto split:list.split)
from ‹get_proc (case cs of [] ⇒ m | _ ⇒ sourcenode (last cs)) = Main›
‹sourcenode a = m› ‹get_proc (sourcenode a) = get_proc (targetnode a)›
have "get_proc (case cs of [] ⇒ targetnode a | _ ⇒ sourcenode (last cs)) = Main"
by(cases cs) auto
from IH[OF ‹targetnode a -as→* m'› False ‹valid_call_list cs (targetnode a)›
‹get_proc m' = Main› this]
have "same_level_path_aux cs as ∧ upd_cs cs as = []" .
with ‹intra_kind (kind a)› show ?thesis by(fastforce simp:intra_kind_def)
qed
next
case (vpa_Call cs a as Q r p fs)
note IH = ‹⋀m. ⟦m -as→* m'; as ≠ []; valid_call_list (a # cs) m;
get_proc m' = Main;
get_proc (case a # cs of [] ⇒ m | _ ⇒ sourcenode (last (a # cs))) = Main⟧
⟹ same_level_path_aux (a # cs) as ∧ upd_cs (a # cs) as = []›
from ‹m -a # as→* m'› have "sourcenode a = m" and "valid_edge a"
and "targetnode a -as→* m'" by(auto elim:path_split_Cons)
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "get_proc (targetnode a) = p"
by(rule get_proc_call)
show ?case
proof(cases "as = []")
case True
with ‹targetnode a -as→* m'› have "targetnode a = m'" by fastforce
with ‹get_proc (targetnode a) = p› ‹get_proc m' = Main› ‹kind a = Q:r↪⇘p⇙fs›
have "kind a = Q:r↪⇘Main⇙fs" by simp
with ‹valid_edge a› have False by(rule Main_no_call_target)
thus ?thesis by simp
next
case False
from ‹get_proc (targetnode a) = p› ‹valid_call_list cs m› ‹valid_edge a›
‹kind a = Q:r↪⇘p⇙fs› ‹sourcenode a = m›
have "valid_call_list (a # cs) (targetnode a)"
apply(clarsimp simp:valid_call_list_def)
apply(case_tac cs') apply auto
apply(erule_tac x="list" in allE)
by(case_tac list)(auto simp:sourcenodes_def)
from ‹get_proc (case cs of [] ⇒ m | _ ⇒ sourcenode (last cs)) = Main›
‹sourcenode a = m›
have "get_proc (case a # cs of [] ⇒ targetnode a
| _ ⇒ sourcenode (last (a # cs))) = Main"
by(cases cs) auto
from IH[OF ‹targetnode a -as→* m'› False ‹valid_call_list (a#cs) (targetnode a)›
‹get_proc m' = Main› this]
have "same_level_path_aux (a # cs) as ∧ upd_cs (a # cs) as = []" .
with ‹kind a = Q:r↪⇘p⇙fs› show ?thesis by simp
qed
next
case (vpa_ReturnEmpty cs a as Q p f)
note IH = ‹⋀m. ⟦m -as→* m'; as ≠ []; valid_call_list [] m; get_proc m' = Main;
get_proc (case [] of [] ⇒ m | a # list ⇒ sourcenode (last [])) = Main⟧
⟹ same_level_path_aux [] as ∧ upd_cs [] as = []›
from ‹m -a # as→* m'› have "sourcenode a = m" and "valid_edge a"
and "targetnode a -as→* m'" by(auto elim:path_split_Cons)
from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› have "get_proc (sourcenode a) = p"
by(rule get_proc_return)
from ‹get_proc (case cs of [] ⇒ m | a # list ⇒ sourcenode (last cs)) = Main›
‹cs = []›
have "get_proc m = Main" by simp
with ‹sourcenode a = m› ‹get_proc (sourcenode a) = p› have "p = Main" by simp
with ‹kind a = Q↩⇘p⇙f› have "kind a = Q↩⇘Main⇙f" by simp
with ‹valid_edge a› have False by(rule Main_no_return_source)
thus ?case by simp
next
case (vpa_ReturnCons cs a as Q p f c' cs')
note IH = ‹⋀m. ⟦m -as→* m'; as ≠ []; valid_call_list cs' m; get_proc m' = Main;
get_proc (case cs' of [] ⇒ m | a # list ⇒ sourcenode (last cs')) = Main⟧
⟹ same_level_path_aux cs' as ∧ upd_cs cs' as = []›
from ‹m -a # as→* m'› have "sourcenode a = m" and "valid_edge a"
and "targetnode a -as→* m'" by(auto elim:path_split_Cons)
from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› have "get_proc (sourcenode a) = p"
by(rule get_proc_return)
from ‹valid_call_list cs m› ‹cs = c' # cs'›
have "valid_edge c'"
by(auto simp:valid_call_list_def,erule_tac x="[]" in allE,auto)
from ‹valid_edge c'› ‹a ∈ get_return_edges c'›
have "get_proc (sourcenode c') = get_proc (targetnode a)"
by(rule get_proc_get_return_edge)
show ?case
proof(cases "as = []")
case True
with ‹targetnode a -as→* m'› have "targetnode a = m'" by fastforce
with ‹get_proc m' = Main› have "get_proc (targetnode a) = Main" by simp
from ‹get_proc (sourcenode c') = get_proc (targetnode a)›
‹get_proc (targetnode a) = Main›
have "get_proc (sourcenode c') = Main" by simp
have "cs' = []"
proof(cases cs')
case (Cons cx csx)
with ‹cs = c' # cs'› ‹valid_call_list cs m›
obtain Qx rx fsx where "valid_edge cx"
and "kind cx = Qx:rx↪⇘get_proc (sourcenode c')⇙fsx"
by(auto simp:valid_call_list_def,erule_tac x="[c']" in allE,
auto simp:sourcenodes_def)
with ‹get_proc (sourcenode c') = Main› have "kind cx = Qx:rx↪⇘Main⇙fsx" by simp
with ‹valid_edge cx› have False by(rule Main_no_call_target)
thus ?thesis by simp
qed simp
with True ‹cs = c' # cs'› ‹a ∈ get_return_edges c'› ‹kind a = Q↩⇘p⇙f›
show ?thesis by simp
next
case False
from ‹valid_call_list cs m› ‹cs = c' # cs'›
‹get_proc (sourcenode c') = get_proc (targetnode a)›
have "valid_call_list cs' (targetnode a)"
apply(clarsimp simp:valid_call_list_def)
apply(hypsubst_thin)
apply(erule_tac x="c' # cs'" in allE)
by(case_tac cs')(auto simp:sourcenodes_def)
from ‹get_proc (case cs of [] ⇒ m | a # list ⇒ sourcenode (last cs)) = Main›
‹cs = c' # cs'› ‹get_proc (sourcenode c') = get_proc (targetnode a)›
have "get_proc (case cs' of [] ⇒ targetnode a
| _ ⇒ sourcenode (last cs')) = Main"
by(cases cs') auto
from IH[OF ‹targetnode a -as→* m'› False ‹valid_call_list cs' (targetnode a)›
‹get_proc m' = Main› this]
have "same_level_path_aux cs' as ∧ upd_cs cs' as = []" .
with ‹kind a = Q↩⇘p⇙f› ‹cs = c' # cs'› ‹a ∈ get_return_edges c'›
show ?thesis by simp
qed
qed

definition same_level_path :: "'edge list ⇒ bool"
where "same_level_path as ≡ same_level_path_aux [] as ∧ upd_cs [] as = []"

lemma same_level_path_valid_path:
"same_level_path as ⟹ valid_path as"
by(fastforce intro:same_level_path_aux_valid_path_aux
simp:same_level_path_def valid_path_def)

lemma same_level_path_Append:
"⟦same_level_path as; same_level_path as'⟧ ⟹ same_level_path (as@as')"
by(fastforce elim:same_level_path_aux_Append upd_cs_Append simp:same_level_path_def)

lemma same_level_path_number_Calls_eq_number_Returns:
"⟦same_level_path as; ∀a ∈ set as. valid_edge a⟧ ⟹
length [