header {* \isaheader{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\<hookrightarrow>⇘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\<hookrightarrow>⇘Main⇙f|] ==> False"
and Main_no_return_source:"[|valid_edge a; kind a = Q'\<hookleftarrow>⇘Main⇙f'|] ==> False"
and callee_in_procs:
"[|valid_edge a; kind a = Q:r\<hookrightarrow>⇘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\<hookrightarrow>⇘p⇙fs|] ==> get_proc (targetnode a) = p"
and get_proc_return:
"[|valid_edge a; kind a = Q'\<hookleftarrow>⇘p⇙f'|] ==> get_proc (sourcenode a) = p"
and call_edges_only:"[|valid_edge a; kind a = Q:r\<hookrightarrow>⇘p⇙fs|]
==> ∀a'. valid_edge a' ∧ targetnode a' = targetnode a -->
(∃Qx rx fsx. kind a' = Qx:rx\<hookrightarrow>⇘p⇙fsx)"
and return_edges_only:"[|valid_edge a; kind a = Q'\<hookleftarrow>⇘p⇙f'|]
==> ∀a'. valid_edge a' ∧ sourcenode a' = sourcenode a -->
(∃Qx fx. kind a' = Qx\<hookleftarrow>⇘p⇙fx)"
and get_return_edge_call:
"[|valid_edge a; kind a = Q:r\<hookrightarrow>⇘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\<hookrightarrow>⇘p⇙fs"
and call_return_edges:
"[|valid_edge a; kind a = Q:r\<hookrightarrow>⇘p⇙fs; a' ∈ get_return_edges a|]
==> ∃Q' f'. kind a' = Q'\<hookleftarrow>⇘p⇙f'"
and return_needs_call: "[|valid_edge a; kind a = Q'\<hookleftarrow>⇘p⇙f'|]
==> ∃!a'. valid_edge a' ∧ (∃Q r fs. kind a' = Q:r\<hookrightarrow>⇘p⇙fs) ∧ a ∈ get_return_edges a'"
and intra_proc_additional_edge:
"[|valid_edge a; a' ∈ get_return_edges a|]
==> ∃a''. valid_edge a'' ∧ sourcenode a'' = targetnode a ∧
targetnode a'' = sourcenode a' ∧ kind a'' = (λcf. False)⇣\<surd>"
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)⇣\<surd>"
and call_only_one_intra_edge:
"[|valid_edge a; kind a = Q:r\<hookrightarrow>⇘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'\<hookleftarrow>⇘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\<hookrightarrow>⇘p⇙fs⇣1; kind a' = Q⇣2:r⇣2\<hookrightarrow>⇘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\<hookrightarrow>⇘p⇙fs" and "valid_edge a'"
and "sourcenode a = sourcenode a'" and "intra_kind(kind a')"
shows "kind a' = (λcf. False)⇣\<surd>"
proof -
from `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘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)⇣\<surd>"
by(fastforce dest:call_return_node_edge)
from `kind a'' = (λcf. False)⇣\<surd>` have "intra_kind(kind a'')"
by(simp add:intra_kind_def)
with assms `valid_edge a''` `sourcenode a'' = sourcenode a`
`kind a'' = (λcf. False)⇣\<surd>`
show ?thesis by(fastforce dest:call_only_one_intra_edge)
qed
lemma formal_in_THE:
"[|valid_edge a; kind a = Q:r\<hookrightarrow>⇘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\<hookleftarrow>⇘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 \<rightharpoonup> 'val) \<rightharpoonup> 'val) list => ('var \<rightharpoonup> '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 \<rightharpoonup> 'val) × 'ret) list =>
(('var \<rightharpoonup> 'val) × 'ret) list"
where "transfer (\<Up>f) (cf#cfs) = (f (fst cf),snd cf)#cfs"
| "transfer (Q)⇣\<surd> (cf#cfs) = (cf#cfs)"
| "transfer (Q:r\<hookrightarrow>⇘p⇙fs) (cf#cfs) =
(let ins = THE ins. ∃outs. (p,ins,outs) ∈ set procs in
(empty(ins [:=] params fs (fst cf)),r)#cf#cfs)"
| "transfer (Q\<hookleftarrow>⇘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 \<rightharpoonup> 'val) × 'ret) list =>
(('var \<rightharpoonup> '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 \<rightharpoonup> 'val) × 'ret) list => bool"
where "pred (\<Up>f) (cf#cfs) = True"
| "pred (Q)⇣\<surd> (cf#cfs) = Q (fst cf)"
| "pred (Q:r\<hookrightarrow>⇘p⇙fs) (cf#cfs) = Q (fst cf,r)"
| "pred (Q\<hookleftarrow>⇘p⇙f) (cf#cfs) = (Q cf ∧ cfs ≠ [])"
| "pred et [] = False"
fun preds :: "('var,'val,'ret,'pname) edge_kind list => (('var \<rightharpoonup> '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 \<rightharpoonup> 'val) × 'ret) list => 'var \<rightharpoonup> 'val"
where "state_val s V ≡ (fst (hd s)) V"
subsubsection {* @{text "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
by(simp add:sourcenodes_def targetnodes_def)
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
by(simp add:sourcenodes_def targetnodes_def)
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
by(simp add:sourcenodes_def targetnodes_def)
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
by(simp add:sourcenodes_def targetnodes_def)
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)"
by(simp_all add:intra_path_def)
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)⇣\<surd>"
by(fastforce dest:intra_proc_additional_edge)
from `valid_edge a''` `kind a'' = (λcf. False)⇣\<surd>`
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\<hookrightarrow>⇘p⇙fs => valid_path_aux (a#cs) as
| Q\<hookleftarrow>⇘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\<hookrightarrow>⇘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\<hookleftarrow>⇘p⇙f; cs = []; valid_path_aux [] as; P [] as|]
==> P cs (a#as)"
"!!cs a as Q p f c' cs' . [|kind a = Q\<hookleftarrow>⇘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\<hookrightarrow>⇘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\<hookleftarrow>⇘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')"
by(simp add:append_eq_Cons_conv)
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\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<hookrightarrow>⇘p⇙fs => upd_cs (a#cs) as
| Q\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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')"
by(simp add:Cons_eq_append_conv)
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')"
by(simp add:Cons_eq_append_conv)
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')"
by(simp add:Cons_eq_append_conv)
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\<hookrightarrow>⇘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')"
by(simp add:Cons_eq_append_conv)
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\<hookrightarrow>⇘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\<hookrightarrow>⇘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')"
by(simp add:Cons_eq_append_conv)
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\<hookleftarrow>⇘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')"
by(simp add:Cons_eq_append_conv)
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\<hookleftarrow>⇘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\<hookleftarrow>⇘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')"
by(simp add:Cons_eq_append_conv)
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\<hookleftarrow>⇘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')"
by(simp add:Cons_eq_append_conv)
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\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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'\<hookrightarrow>⇘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'\<hookleftarrow>⇘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'\<hookleftarrow>⇘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"
("_ -_->⇣\<surd>* _" [51,0,0] 80)
where vp_def:"n -as->⇣\<surd>* n' ≡ n -as->* n' ∧ valid_path as"
lemma intra_path_vp:
assumes "n -as->⇣ι* n'" shows "n -as->⇣\<surd>* n'"
proof -
from `n -as->⇣ι* n'` have "n -as->* n'" and "∀a ∈ set as. intra_kind(kind a)"
by(simp_all add:intra_path_def)
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->⇣\<surd>* n'" and "as ≠ []"
obtains a' as' where "as = a'#as'" and "n = sourcenode a'"
and "valid_edge a'" and "targetnode a' -as'->⇣\<surd>* n'"
proof(atomize_elim)
from `n -as->⇣\<surd>* 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->⇣\<surd>* 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'->⇣\<surd>* 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'->⇣\<surd>* n'" by blast
qed
lemma vp_split_snoc:
assumes "n -as->⇣\<surd>* n'" and "as ≠ []"
obtains a' as' where "as = as'@[a']" and "n -as'->⇣\<surd>* sourcenode a'"
and "valid_edge a'" and "n' = targetnode a'"
proof(atomize_elim)
from `n -as->⇣\<surd>* 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->⇣\<surd>* 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'->⇣\<surd>* 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'->⇣\<surd>* sourcenode a' ∧ valid_edge a' ∧
n' = targetnode a'"
by blast
qed
lemma vp_split:
assumes "n -as@a#as'->⇣\<surd>* n'"
shows "n -as->⇣\<surd>* sourcenode a" and "valid_edge a" and "targetnode a -as'->⇣\<surd>* n'"
proof -
from `n -as@a#as'->⇣\<surd>* 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'->⇣\<surd>* 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->⇣\<surd>* sourcenode a" "valid_edge a" "targetnode a -as'->⇣\<surd>* n'"
by(auto simp:vp_def)
qed
lemma vp_split_second:
assumes "n -as@a#as'->⇣\<surd>* n'" shows "sourcenode a -a#as'->⇣\<surd>* n'"
proof -
from `n -as@a#as'->⇣\<surd>* n'` have "sourcenode a -a#as'->* n'"
by(fastforce elim:path_split_second simp:vp_def)
from `n -as@a#as'->⇣\<surd>* 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\<hookleftarrow>⇘p⇙f => valid_path_rev_aux (a#cs) as
| Q:r\<hookrightarrow>⇘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\<hookleftarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookleftarrow>⇘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\<hookrightarrow>⇘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)"
by(simp add:append_eq_Cons_conv)
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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookleftarrow>⇘p⇙f => upd_rev_cs (a#cs) as
| Q:r\<hookrightarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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'\<hookleftarrow>⇘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'\<hookrightarrow>⇘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'\<hookrightarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookleftarrow>⇘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"
by(simp add:valid_call_list_def)
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"
by(simp add:valid_return_list_def)
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(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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘p⇙fs`
have "get_proc (targetnode a') = p" by(rule get_proc_call)
with `valid_edge a'` `kind a' = Q:r\<hookrightarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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)⇣\<surd>"
by(fastforce dest:call_return_node_edge)
from `valid_edge ax` sources[THEN sym] targets[THEN sym] `kind ax = (λcf. False)⇣\<surd>`
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(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\<hookrightarrow>⇘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'\<hookrightarrow>⇘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\<hookleftarrow>⇘p⇙f` `cs = c'#cs'` `a ∈ get_return_edges c'` `kind c' = Q':r'\<hookrightarrow>⇘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"
by(simp add:upd_rev_cs_Cons_intra)
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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘p⇙fs` Nil
have "valid_path_rev_aux (upd_rev_cs cs' (a#as)) (rev cs)" by simp
from Nil `kind a = Q:r\<hookrightarrow>⇘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\<hookrightarrow>⇘p⇙fs`
have match:"cx ∈ get_return_edges a" "valid_path_rev_aux csx (rev cs)" by auto
from `kind a = Q:r\<hookrightarrow>⇘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\<hookrightarrow>⇘p⇙fs` match
have "valid_path_rev_aux (upd_rev_cs cs' (a#as)) (rev cs)" by simp
from Cons `kind a = Q:r\<hookrightarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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'\<hookrightarrow>⇘p'⇙f'"
by(fastforce dest!:only_call_get_return_edges)
from `kind a = Q\<hookleftarrow>⇘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\<hookleftarrow>⇘p⇙f`
`kind cx = Q':r'\<hookrightarrow>⇘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->⇣\<surd>* 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\<hookrightarrow>⇘p⇙fs => same_level_path_aux (a#cs) as
| Q\<hookleftarrow>⇘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\<hookrightarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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'\<hookleftarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookleftarrow>⇘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'\<hookleftarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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'\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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'\<hookleftarrow>⇘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'\<hookleftarrow>⇘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\<hookleftarrow>⇘p⇙f`
have "same_level_path_aux cs (a#asx)" by simp
moreover
from `upd_cs cs' asx = c''#cs''` `kind a = Q\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<leftarrow>as@cs. ∃Q r p fs. kind a = Q:r\<hookrightarrow>⇘p⇙fs] =
length [a\<leftarrow>as. ∃Q p f. kind a = Q\<hookleftarrow>⇘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\<hookrightarrow>⇘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\<hookleftarrow>⇘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\<hookrightarrow>⇘p⇙fs` `upd_cs cs (a#as) = []` have "a#cs = []" by simp
thus ?thesis by simp
next
case False
from `kind a = Q:r\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘p⇙fs`
have "kind a = Q:r\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘p⇙f` have "kind a = Q\<hookleftarrow>⇘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\<hookleftarrow>⇘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\<hookrightarrow>⇘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\<hookrightarrow>⇘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\<hookleftarrow>⇘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(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\<hookleftarrow>⇘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 [a\<leftarrow>as. ∃Q r p fs. kind a = Q:r\<hookrightarrow>⇘p⇙fs] = length [a\<leftarrow>as. ∃Q p f. kind a = Q\<hookleftarrow>⇘p⇙f]"
by(fastforce dest:slpa_number_Calls_eq_number_Returns simp:same_level_path_def)
lemma same_level_path_valid_path_Append:
"[|same_level_path as; valid_path as'|] ==> valid_path (as@as')"
by(fastforce intro:valid_path_aux_Append elim:same_level_path_aux_valid_path_aux
simp:valid_path_def same_level_path_def)
lemma valid_path_same_level_path_Append:
"[|valid_path as; same_level_path as'|] ==> valid_path (as@as')"
apply(auto simp:valid_path_def same_level_path_def)
apply(erule valid_path_aux_Append)
by(fastforce intro!:same_level_path_aux_valid_path_aux
dest:same_level_path_aux_callstack_Append)
lemma intras_same_level_path:
assumes "∀a ∈ set as. intra_kind(kind a)" shows "same_level_path as"
proof -
from `∀a ∈ set as. intra_kind(kind a)` have "same_level_path_aux [] as"
by(induct as)(auto simp:intra_kind_def)
moreover
from `∀a ∈ set as. intra_kind(kind a)` have "upd_cs [] as = []"
by(induct as)(auto simp:intra_kind_def)
ultimately show ?thesis by(simp add:same_level_path_def)
qed
definition same_level_path' :: "'node => 'edge list => 'node => bool"
("_ -_->⇘sl⇙* _" [51,0,0] 80)
where slp_def:"n -as->⇘sl⇙* n' ≡ n -as->* n' ∧ same_level_path as"
lemma slp_vp: "n -as->⇘sl⇙* n' ==> n -as->⇣\<surd>* n'"
by(fastforce intro:same_level_path_valid_path simp:slp_def vp_def)
lemma intra_path_slp: "n -as->⇣ι* n' ==> n -as->⇘sl⇙* n'"
by(fastforce intro:intras_same_level_path simp:slp_def intra_path_def)
lemma slp_Append:
"[|n -as->⇘sl⇙* n''; n'' -as'->⇘sl⇙* n'|] ==> n -as@as'->⇘sl⇙* n'"
by(fastforce simp:slp_def intro:path_Append same_level_path_Append)
lemma slp_vp_Append:
"[|n -as->⇘sl⇙* n''; n'' -as'->⇣\<surd>* n'|] ==> n -as@as'->⇣\<surd>* n'"
by(fastforce simp:slp_def vp_def intro:path_Append same_level_path_valid_path_Append)
lemma vp_slp_Append:
"[|n -as->⇣\<surd>* n''; n'' -as'->⇘sl⇙* n'|] ==> n -as@as'->⇣\<surd>* n'"
by(fastforce simp:slp_def vp_def intro:path_Append valid_path_same_level_path_Append)
lemma slp_get_proc:
"n -as->⇘sl⇙* n' ==> get_proc n = get_proc n'"
by(fastforce dest:slpa_get_proc simp:same_level_path_def slp_def)
lemma same_level_path_inner_path:
assumes "n -as->⇘sl⇙* n'"
obtains as' where "n -as'->⇣ι* n'" and "set(sourcenodes as') ⊆ set(sourcenodes as)"
proof(atomize_elim)
from `n -as->⇘sl⇙* n'` have "n -as->* n'" and "same_level_path as"
by(simp_all add:slp_def)
from `same_level_path as` have "same_level_path_aux [] as" and "upd_cs [] as = []"
by(simp_all add:same_level_path_def)
from `n -as->* n'` `same_level_path_aux [] as` `upd_cs [] as = []`
show "∃as'. n -as'->⇣ι* n' ∧ set(sourcenodes as') ⊆ set(sourcenodes as)"
proof(induct as arbitrary:n rule:length_induct)
fix as n
assume IH:"∀as''. length as'' < length as -->
(∀n''. n'' -as''->* n' --> same_level_path_aux [] as'' -->
upd_cs [] as'' = [] -->
(∃as'. n'' -as'->⇣ι* n' ∧ set (sourcenodes as') ⊆ set (sourcenodes as'')))"
and "n -as->* n'" and "same_level_path_aux [] as" and "upd_cs [] as = []"
show "∃as'. n -as'->⇣ι* n' ∧ set (sourcenodes as') ⊆ set (sourcenodes as)"
proof(cases as)
case Nil
with `n -as->* n'` show ?thesis by(fastforce simp:intra_path_def)
next
case (Cons a' as')
with `n -as->* n'` Cons have "n = sourcenode a'" and "valid_edge a'"
and "targetnode a' -as'->* n'"
by(auto intro:path_split_Cons)
show ?thesis
proof(cases "kind a'" rule:edge_kind_cases)
case Intra
with Cons `same_level_path_aux [] as` have "same_level_path_aux [] as'"
by(fastforce simp:intra_kind_def)
moreover
from Intra Cons `upd_cs [] as = []` have "upd_cs [] as' = []"
by(fastforce simp:intra_kind_def)
ultimately obtain as'' where "targetnode a' -as''->⇣ι* n'"
and "set (sourcenodes as'') ⊆ set (sourcenodes as')"
using IH Cons `targetnode a' -as'->* n'`
by(erule_tac x="as'" in allE) auto
from `n = sourcenode a'` `valid_edge a'` Intra `targetnode a' -as''->⇣ι* n'`
have "n -a'#as''->⇣ι* n'" by(fastforce intro:Cons_path simp:intra_path_def)
with `set (sourcenodes as'') ⊆ set (sourcenodes as')` Cons show ?thesis
by(rule_tac x="a'#as''" in exI,auto simp:sourcenodes_def)
next
case (Call Q p f)
with Cons `same_level_path_aux [] as`
have "same_level_path_aux [a'] as'" by simp
from Call Cons `upd_cs [] as = []` have "upd_cs [a'] as' = []" by simp
hence "as' ≠ []" by fastforce
with `upd_cs [a'] as' = []` obtain xs ys where "as' = xs@ys" and "xs ≠ []"
and "upd_cs [a'] xs = []" and "upd_cs [] ys = []"
and "∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] --> upd_cs [a'] xs' ≠ []"
by -(erule upd_cs_empty_split,auto)
from `same_level_path_aux [a'] as'` `as' = xs@ys` `upd_cs [a'] xs = []`
have "same_level_path_aux [a'] xs" and "same_level_path_aux [] ys"
by(auto intro:slpa_split)
from `same_level_path_aux [a'] xs` `upd_cs [a'] xs = []`
`∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] --> upd_cs [a'] xs' ≠ []`
have "last xs ∈ get_return_edges (last [a'])"
by(fastforce intro!:slpa_get_return_edges)
with `valid_edge a'` Call
obtain a where "valid_edge a" and "sourcenode a = sourcenode a'"
and "targetnode a = targetnode (last xs)" and "kind a = (λcf. False)⇣\<surd>"
by -(drule call_return_node_edge,auto)
from `targetnode a = targetnode (last xs)` `xs ≠ []`
have "targetnode a = targetnode (last (a'#xs))" by simp
from `as' = xs@ys` `xs ≠ []` Cons have "length ys < length as" by simp
from `targetnode a' -as'->* n'` `as' = xs@ys` `xs ≠ []`
have "targetnode (last (a'#xs)) -ys->* n'"
by(cases xs rule:rev_cases,auto dest:path_split)
with IH `length ys < length as` `same_level_path_aux [] ys`
`upd_cs [] ys = []`
obtain as'' where "targetnode (last (a'#xs)) -as''->⇣ι* n'"
and "set(sourcenodes as'') ⊆ set(sourcenodes ys)"
apply(erule_tac x="ys" in allE) apply clarsimp
apply(erule_tac x="targetnode (last (a'#xs))" in allE)
by clarsimp
from `sourcenode a = sourcenode a'` `n = sourcenode a'`
`targetnode a = targetnode (last (a'#xs))` `valid_edge a`
`kind a = (λcf. False)⇣\<surd>` `targetnode (last (a'#xs)) -as''->⇣ι* n'`
have "n -a#as''->⇣ι* n'"
by(fastforce intro:Cons_path simp:intra_path_def intra_kind_def)
moreover
from `set(sourcenodes as'') ⊆ set(sourcenodes ys)` Cons `as' = xs@ys`
`sourcenode a = sourcenode a'`
have "set(sourcenodes (a#as'')) ⊆ set(sourcenodes as)"
by(auto simp:sourcenodes_def)
ultimately show ?thesis by blast
next
case (Return Q p f)
with Cons `same_level_path_aux [] as` have False by simp
thus ?thesis by simp
qed
qed
qed
qed
lemma slp_callstack_length_equal:
assumes "n -as->⇘sl⇙* n'" obtains cf' where "transfers (kinds as) (cf#cfs) = cf'#cfs"
and "transfers (kinds as) (cf#cfs') = cf'#cfs'"
proof(atomize_elim)
from `n -as->⇘sl⇙* n'` have "same_level_path_aux [] as" and "upd_cs [] as = []"
by(simp_all add:slp_def same_level_path_def)
then obtain cfx cfsx where "transfers (kinds as) (cf#cfs) = cfsx@cfx#cfs"
and "transfers (kinds as) (cf#cfs') = cfsx@cfx#cfs'"
and "length cfsx = length (upd_cs [] as)"
by(fastforce elim:slpa_callstack_length)
with `upd_cs [] as = []` have "cfsx = []" by(cases cfsx) auto
with `transfers (kinds as) (cf#cfs) = cfsx@cfx#cfs`
`transfers (kinds as) (cf#cfs') = cfsx@cfx#cfs'`
show "∃cf'. transfers (kinds as) (cf#cfs) = cf'#cfs ∧
transfers (kinds as) (cf#cfs') = cf'#cfs'" by fastforce
qed
lemma slp_cases [consumes 1,case_names intra_path return_intra_path]:
assumes "m -as->⇘sl⇙* m'"
obtains "m -as->⇣ι* m'"
| as' a as'' Q p f where "as = as'@a#as''" and "kind a = Q\<hookleftarrow>⇘p⇙f"
and "m -as'@[a]->⇘sl⇙* targetnode a" and "targetnode a -as''->⇣ι* m'"
proof(atomize_elim)
from `m -as->⇘sl⇙* m'` have "m -as->* m'" and "same_level_path_aux [] as"
and "upd_cs [] as = []" by(simp_all add:slp_def same_level_path_def)
from `m -as->* m'` have "∀a ∈ set as. valid_edge a" by(rule path_valid_edges)
have "∀a ∈ set []. valid_edge a" by simp
with `same_level_path_aux [] as` `upd_cs [] as = []` `∀a ∈ set []. valid_edge a`
`∀a ∈ set as. valid_edge a`
show "m -as->⇣ι* m' ∨
(∃as' a as'' Q p f. as = as' @ a # as'' ∧ kind a = Q\<hookleftarrow>⇘p⇙f ∧
m -as' @ [a]->⇘sl⇙* targetnode a ∧ targetnode a -as''->⇣ι* m')"
proof(cases rule:slpa_cases)
case intra_path
with `m -as->* m'` have "m -as->⇣ι* m'" by(simp add:intra_path_def)
thus ?thesis by blast
next
case (return_intra_path as' a as'' Q p f c' cs')
from `m -as->* m'` `as = as' @ a # as''`
have "m -as'->* sourcenode a" and "valid_edge a" and "targetnode a -as''->* m'"
by(auto intro:path_split)
from `m -as'->* sourcenode a` `valid_edge a`
have "m -as'@[a]->* targetnode a" by(fastforce intro:path_Append path_edge)
with `same_level_path_aux [] as'` `upd_cs [] as' = c' # cs'` `kind a = Q\<hookleftarrow>⇘p⇙f`
`a ∈ get_return_edges c'`
have "same_level_path_aux [] (as'@[a])"
by(fastforce intro:same_level_path_aux_Append)
with `upd_cs [] (as' @ [a]) = []` `m -as'@[a]->* targetnode a`
have "m -as'@[a]->⇘sl⇙* targetnode a" by(simp add:slp_def same_level_path_def)
moreover
from `∀a∈set as''. intra_kind (kind a)` `targetnode a -as''->* m'`
have "targetnode a -as''->⇣ι* m'" by(simp add:intra_path_def)
ultimately show ?thesis using `as = as' @ a # as''` `kind a = Q\<hookleftarrow>⇘p⇙f` by blast
qed
qed
function same_level_path_rev_aux :: "'edge list => 'edge list => bool"
where "same_level_path_rev_aux cs [] <-> True"
| "same_level_path_rev_aux cs (as@[a]) <->
(case (kind a) of Q\<hookleftarrow>⇘p⇙f => same_level_path_rev_aux (a#cs) as
| Q:r\<hookrightarrow>⇘p⇙fs => case cs of [] => False
| c'#cs' => c' ∈ get_return_edges a ∧
same_level_path_rev_aux cs' as
| _ => same_level_path_rev_aux cs as)"
by auto(case_tac b rule:rev_cases,auto)
termination by lexicographic_order
lemma slpra_induct [consumes 1,case_names slpra_empty slpra_intra slpra_Return
slpra_Call]:
assumes major: "same_level_path_rev_aux xs ys"
and rules: "!!cs. P cs []"
"!!cs a as. [|intra_kind(kind a); same_level_path_rev_aux cs as; P cs as|]
==> P cs (as@[a])"
"!!cs a as Q p f. [|kind a = Q\<hookleftarrow>⇘p⇙f; same_level_path_rev_aux (a#cs) as; P (a#cs) as|]
==> P cs (as@[a])"
"!!cs a as Q r p fs c' cs'. [|kind a = Q:r\<hookrightarrow>⇘p⇙fs; cs = c'#cs';
same_level_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 same_level_path_rev_aux_Append:
"[|same_level_path_rev_aux cs as'; same_level_path_rev_aux (upd_rev_cs cs as') as|]
==> same_level_path_rev_aux cs (as@as')"
by(induct rule:slpra_induct,
auto simp:intra_kind_def simp del:append_assoc simp:append_assoc[THEN sym])
lemma slpra_to_slpa:
"[|same_level_path_rev_aux cs as; upd_rev_cs cs as = []; n -as->* n';
valid_return_list cs n'|]
==> same_level_path_aux [] as ∧ same_level_path_aux (upd_cs [] as) cs ∧
upd_cs (upd_cs [] as) cs = []"
proof(induct arbitrary:n' rule:slpra_induct)
case slpra_empty thus ?case by simp
next
case (slpra_intra cs a as)
note IH = `!!n'. [|upd_rev_cs cs as = []; n -as->* n'; valid_return_list cs n'|]
==> same_level_path_aux [] as ∧ same_level_path_aux (upd_cs [] as) cs ∧
upd_cs (upd_cs [] as) cs = []`
from `n -as@[a]->* n'` have "n -as->* sourcenode a" and "valid_edge a"
and "n' = targetnode a" by(auto intro:path_split_snoc)
from `valid_edge a` `intra_kind (kind a)`
have "get_proc (sourcenode a) = get_proc (targetnode a)"
by(rule get_proc_intra)
with `valid_return_list cs n'` `n' = targetnode a`
have "valid_return_list cs (sourcenode a)"
apply(clarsimp simp:valid_return_list_def)
apply(erule_tac x="cs'" in allE) apply clarsimp
by(case_tac cs')(auto simp:targetnodes_def)
from `upd_rev_cs cs (as@[a]) = []` `intra_kind (kind a)`
have "upd_rev_cs cs as = []" by(fastforce simp:intra_kind_def)
from `valid_edge a` `intra_kind (kind a)`
have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
from IH[OF `upd_rev_cs cs as = []` `n -as->* sourcenode a`
`valid_return_list cs (sourcenode a)`]
have "same_level_path_aux [] as"
and "same_level_path_aux (upd_cs [] as) cs"
and "upd_cs (upd_cs [] as) cs = []" by simp_all
from `same_level_path_aux [] as` `intra_kind (kind a)`
have "same_level_path_aux [] (as@[a])" by(rule slpa_snoc_intra)
from `intra_kind (kind a)`
have "upd_cs [] (as@[a]) = upd_cs [] as"
by(fastforce simp:upd_cs_Append intra_kind_def)
moreover
from `same_level_path_aux [] as` `intra_kind (kind a)`
have "same_level_path_aux [] (as@[a])" by(rule slpa_snoc_intra)
ultimately show ?case using `same_level_path_aux (upd_cs [] as) cs`
`upd_cs (upd_cs [] as) cs = []`
by simp
next
case (slpra_Return cs a as Q p f)
note IH = `!!n' n''. [|upd_rev_cs (a#cs) as = []; n -as->* n';
valid_return_list (a#cs) n'|]
==> same_level_path_aux [] as ∧
same_level_path_aux (upd_cs [] as) (a#cs) ∧
upd_cs (upd_cs [] as) (a#cs) = []`
from `n -as@[a]->* n'` have "n -as->* sourcenode a" and "valid_edge a"
and "n' = targetnode a" by(auto intro:path_split_snoc)
from `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f` have "p = get_proc (sourcenode a)"
by(rule get_proc_return[THEN sym])
from `valid_return_list cs n'` `n' = targetnode a`
have "valid_return_list cs (targetnode a)" by simp
with `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f` `p = get_proc (sourcenode a)`
have "valid_return_list (a#cs) (sourcenode a)"
apply(clarsimp simp:valid_return_list_def)
apply(case_tac cs') apply auto
apply(erule_tac x="list" in allE) apply clarsimp
by(case_tac list,auto simp:targetnodes_def)
from `upd_rev_cs cs (as@[a]) = []` `kind a = Q\<hookleftarrow>⇘p⇙f`
have "upd_rev_cs (a#cs) as = []" by simp
from IH[OF this `n -as->* sourcenode a` `valid_return_list (a#cs) (sourcenode a)`]
have "same_level_path_aux [] as"
and "same_level_path_aux (upd_cs [] as) (a#cs)"
and "upd_cs (upd_cs [] as) (a#cs) = []" by simp_all
show ?case
proof(cases "upd_cs [] as")
case Nil
with `kind a = Q\<hookleftarrow>⇘p⇙f` `same_level_path_aux (upd_cs [] as) (a#cs)`
have False by simp
thus ?thesis by simp
next
case (Cons cx csx)
with `kind a = Q\<hookleftarrow>⇘p⇙f` `same_level_path_aux (upd_cs [] as) (a#cs)`
obtain Qx fx
where match:"a ∈ get_return_edges cx" "same_level_path_aux csx cs" by auto
from `kind a = Q\<hookleftarrow>⇘p⇙f` Cons have "upd_cs [] (as@[a]) = csx"
by(rule upd_cs_snoc_Return_Cons)
with `same_level_path_aux (upd_cs [] as) (a#cs)`
`kind a = Q\<hookleftarrow>⇘p⇙f` match
have "same_level_path_aux (upd_cs [] (as@[a])) cs" by simp
from `upd_cs [] (as@[a]) = csx` `kind a = Q\<hookleftarrow>⇘p⇙f` Cons
`upd_cs (upd_cs [] as) (a#cs) = []`
have "upd_cs (upd_cs [] (as@[a])) cs = []" by simp
from Cons `kind a = Q\<hookleftarrow>⇘p⇙f` match
have "same_level_path_aux (upd_cs [] as) [a]" by simp
with `same_level_path_aux [] as` have "same_level_path_aux [] (as@[a])"
by(rule same_level_path_aux_Append)
with `same_level_path_aux (upd_cs [] (as@[a])) cs`
`upd_cs (upd_cs [] (as@[a])) cs = []`
show ?thesis by simp
qed
next
case (slpra_Call cs a as Q r p fs cx csx)
note IH = `!!n'. [|upd_rev_cs csx as = []; n -as->* n'; valid_return_list csx n'|]
==> same_level_path_aux [] as ∧
same_level_path_aux (upd_cs [] as) csx ∧ upd_cs (upd_cs [] as) csx = []`
note match = `cs = cx#csx` `cx ∈ get_return_edges a`
from `n -as@[a]->* n'` have "n -as->* sourcenode a" and "valid_edge a"
and "n' = targetnode a" by(auto intro:path_split_snoc)
from `valid_edge a` match
have "get_proc (sourcenode a) = get_proc (targetnode cx)"
by(fastforce intro:get_proc_get_return_edge)
with `valid_return_list cs n'` `cs = cx#csx`
have "valid_return_list csx (sourcenode a)"
apply(clarsimp simp:valid_return_list_def)
apply(erule_tac x="cx#cs'" in allE) apply clarsimp
by(case_tac cs',auto simp:targetnodes_def)
from `kind a = Q:r\<hookrightarrow>⇘p⇙fs` match `upd_rev_cs cs (as@[a]) = []`
have "upd_rev_cs csx as = []" by simp
from IH[OF this `n -as->* sourcenode a` `valid_return_list csx (sourcenode a)`]
have "same_level_path_aux [] as"
and "same_level_path_aux (upd_cs [] as) csx" and "upd_cs (upd_cs [] as) csx = []"
by simp_all
from `same_level_path_aux [] as` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
have "same_level_path_aux [] (as@[a])" by(rule slpa_snoc_Call)
from `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs` match obtain Q' f' where "kind cx = Q'\<hookleftarrow>⇘p⇙f'"
by(fastforce dest!:call_return_edges)
from `kind a = Q:r\<hookrightarrow>⇘p⇙fs` have "upd_cs [] (as@[a]) = a#(upd_cs [] as)"
by(rule upd_cs_snoc_Call)
with `same_level_path_aux (upd_cs [] as) csx` `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
`kind cx = Q'\<hookleftarrow>⇘p⇙f'` match
have "same_level_path_aux (upd_cs [] (as@[a])) cs" by simp
from `upd_cs (upd_cs [] as) csx = []` `upd_cs [] (as@[a]) = a#(upd_cs [] as)`
`kind a = Q:r\<hookrightarrow>⇘p⇙fs` `kind cx = Q'\<hookleftarrow>⇘p⇙f'` match
have "upd_cs (upd_cs [] (as@[a])) cs = []" by simp
with `same_level_path_aux [] (as@[a])`
`same_level_path_aux (upd_cs [] (as@[a])) cs` show ?case by simp
qed
subsubsection {* Lemmas on paths with @{text "(_Entry_)"} *}
lemma path_Entry_target [dest]:
assumes "n -as->* (_Entry_)"
shows "n = (_Entry_)" and "as = []"
using `n -as->* (_Entry_)`
proof(induct n as n'≡"(_Entry_)" rule:path.induct)
case (Cons_path n'' as a n)
from `n'' = (_Entry_)` `targetnode a = n''` `valid_edge a` have False
by -(rule Entry_target,simp_all)
{ case 1
from `False` show ?case ..
next
case 2
from `False` show ?case ..
}
qed simp_all
lemma Entry_sourcenode_hd:
assumes "n -as->* n'" and "(_Entry_) ∈ set (sourcenodes as)"
shows "n = (_Entry_)" and "(_Entry_) ∉ set (sourcenodes (tl as))"
using `n -as->* n'` `(_Entry_) ∈ set (sourcenodes as)`
proof(induct rule:path.induct)
case (empty_path n) case 1
thus ?case by(simp add:sourcenodes_def)
next
case (empty_path n) case 2
thus ?case by(simp add:sourcenodes_def)
next
case (Cons_path n'' as n' a n)
note IH1 = `(_Entry_) ∈ set(sourcenodes as) ==> n'' = (_Entry_)`
note IH2 = `(_Entry_) ∈ set(sourcenodes as) ==> (_Entry_) ∉ set(sourcenodes(tl as))`
have "(_Entry_) ∉ set (sourcenodes(tl(a#as)))"
proof(rule ccontr)
assume "¬ (_Entry_) ∉ set (sourcenodes (tl (a#as)))"
hence "(_Entry_) ∈ set (sourcenodes as)" by simp
from IH1[OF this] have "n'' = (_Entry_)" by simp
with `targetnode a = n''` `valid_edge a` show False by -(erule Entry_target,simp)
qed
hence "(_Entry_) ∉ set (sourcenodes(tl(a#as)))" by fastforce
{ case 1
with `(_Entry_) ∉ set (sourcenodes(tl(a#as)))` `sourcenode a = n`
show ?case by(simp add:sourcenodes_def)
next
case 2
with `(_Entry_) ∉ set (sourcenodes(tl(a#as)))` `sourcenode a = n`
show ?case by(simp add:sourcenodes_def)
}
qed
lemma Entry_no_inner_return_path:
assumes "(_Entry_) -as@[a]->* n" and "∀a ∈ set as. intra_kind(kind a)"
and "kind a = Q\<hookleftarrow>⇘p⇙f"
shows "False"
proof -
from `(_Entry_) -as@[a]->* n` have "(_Entry_) -as->* sourcenode a"
and "valid_edge a" and "targetnode a = n" by(auto intro:path_split_snoc)
from `(_Entry_) -as->* sourcenode a` `∀a ∈ set as. intra_kind(kind a)`
have "(_Entry_) -as->⇣ι* sourcenode a" by(simp add:intra_path_def)
hence "get_proc (sourcenode a) = Main"
by(fastforce dest:intra_path_get_procs simp:get_proc_Entry)
with `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f` have "p = Main"
by(fastforce dest:get_proc_return)
with `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f` show ?thesis
by(fastforce intro:Main_no_return_source)
qed
lemma vpra_no_slpra:
"[|valid_path_rev_aux cs as; n -as->* n'; valid_return_list cs n'; cs ≠ [];
∀xs ys. as = xs@ys --> (¬ same_level_path_rev_aux cs ys ∨ upd_rev_cs cs ys ≠ [])|]
==> ∃a Q f. valid_edge a ∧ kind a = Q\<hookleftarrow>⇘get_proc n⇙f"
proof(induct arbitrary:n' rule:vpra_induct)
case (vpra_empty cs)
from `valid_return_list cs n'` `cs ≠ []` obtain Q f where "valid_edge (hd cs)"
and "kind (hd cs) = Q\<hookleftarrow>⇘get_proc n'⇙f"
apply(unfold valid_return_list_def)
apply(drule hd_Cons_tl[THEN sym])
apply(erule_tac x="[]" in allE)
apply(erule_tac x="hd cs" in allE)
by auto
from `n -[]->* n'` have "n = n'" by fastforce
with `valid_edge (hd cs)` `kind (hd cs) = Q\<hookleftarrow>⇘get_proc n'⇙f` show ?case by blast
next
case (vpra_intra cs a as)
note IH = `!!n'. [|n -as->* n'; valid_return_list cs n'; cs ≠ [];
∀xs ys. as = xs@ys --> ¬ same_level_path_rev_aux cs ys ∨ upd_rev_cs cs ys ≠ []|]
==> ∃a Q f. valid_edge a ∧ kind a = Q\<hookleftarrow>⇘get_proc n⇙f`
note all = `∀xs ys. as@[a] = xs@ys
--> ¬ same_level_path_rev_aux cs ys ∨ upd_rev_cs cs ys ≠ []`
from `n -as@[a]->* n'` have "n -as->* sourcenode a" and "valid_edge a"
and "targetnode a = n'" by(auto intro:path_split_snoc)
from `valid_return_list cs n'` `cs ≠ []` obtain Q f where "valid_edge (hd cs)"
and "kind (hd cs) = Q\<hookleftarrow>⇘get_proc n'⇙f"
apply(unfold valid_return_list_def)
apply(drule hd_Cons_tl[THEN sym])
apply(erule_tac x="[]" in allE)
apply(erule_tac x="hd cs" in allE)
by auto
from `valid_edge a` `intra_kind (kind a)`
have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
with `kind (hd cs) = Q\<hookleftarrow>⇘get_proc n'⇙f` `targetnode a = n'`
have "kind (hd cs) = Q\<hookleftarrow>⇘get_proc (sourcenode a)⇙f" by simp
from `valid_return_list cs n'` `targetnode a = n'`
`get_proc (sourcenode a) = get_proc (targetnode a)`
have "valid_return_list cs (sourcenode a)"
apply(clarsimp simp:valid_return_list_def)
apply(erule_tac x="cs'" in allE)
apply(erule_tac x="c" in allE)
by(auto split:list.split)
from all `intra_kind (kind a)`
have "∀xs ys. as = xs@ys
--> ¬ same_level_path_rev_aux cs ys ∨ upd_rev_cs cs ys ≠ []"
apply clarsimp apply(erule_tac x="xs" in allE)
by(auto simp:intra_kind_def)
from IH[OF `n -as->* sourcenode a` `valid_return_list cs (sourcenode a)`
`cs ≠ []` this] show ?case .
next
case (vpra_Return cs a as Q p f)
note IH = `!!n'. [|n -as->* n'; valid_return_list (a#cs) n'; a#cs ≠ [];
∀xs ys. as = xs @ ys -->
¬ same_level_path_rev_aux (a#cs) ys ∨ upd_rev_cs (a#cs) ys ≠ []|]
==> ∃a Q f. valid_edge a ∧ kind a = Q\<hookleftarrow>⇘get_proc n⇙f`
from `n -as@[a]->* n'` have "n -as->* sourcenode a" and "valid_edge a"
and "targetnode a = n'" by(auto intro:path_split_snoc)
from `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f` have "get_proc (sourcenode a) = p"
by(rule get_proc_return)
with `kind a = Q\<hookleftarrow>⇘p⇙f` `valid_return_list cs n'` `valid_edge a` `targetnode a = n'`
have "valid_return_list (a#cs) (sourcenode a)"
apply(clarsimp simp:valid_return_list_def)
apply(case_tac cs') apply auto
apply(erule_tac x="list" in allE)
apply(erule_tac x="c" in allE)
by(auto split:list.split simp:targetnodes_def)
from `∀xs ys. as@[a] = xs@ys -->
¬ same_level_path_rev_aux cs ys ∨ upd_rev_cs cs ys ≠ []` `kind a = Q\<hookleftarrow>⇘p⇙f`
have "∀xs ys. as = xs@ys -->
¬ same_level_path_rev_aux (a#cs) ys ∨ upd_rev_cs (a#cs) ys ≠ []"
apply clarsimp apply(erule_tac x="xs" in allE)
by auto
from IH[OF `n -as->* sourcenode a` `valid_return_list (a#cs) (sourcenode a)`
_ this] show ?case by simp
next
case (vpra_CallEmpty cs a as Q p fs)
from `cs = []` `cs ≠ []` have False by simp
thus ?case by simp
next
case (vpra_CallCons cs a as Q r p fs c' cs')
note IH = `!!n'. [|n -as->* n'; valid_return_list cs' n'; cs' ≠ [];
∀xs ys. as = xs@ys -->
¬ same_level_path_rev_aux cs' ys ∨ upd_rev_cs cs' ys ≠ []|]
==> ∃a Q f. valid_edge a ∧ kind a = Q\<hookleftarrow>⇘get_proc n⇙f`
note all = `∀xs ys. as@[a] = xs@ys -->
¬ same_level_path_rev_aux cs ys ∨ upd_rev_cs cs ys ≠ []`
from `n -as@[a]->* n'` have "n -as->* sourcenode a" and "valid_edge a"
and "targetnode a = n'" by(auto intro:path_split_snoc)
from `valid_return_list cs n'` `cs = c'#cs'` have "valid_edge c'"
apply(clarsimp simp:valid_return_list_def)
apply(erule_tac x="[]" in allE)
by auto
show ?case
proof(cases "cs' = []")
case True
with `cs = c'#cs'` `kind a = Q:r\<hookrightarrow>⇘p⇙fs` `c' ∈ get_return_edges a`
have "same_level_path_rev_aux cs ([]@[a])"
and "upd_rev_cs cs ([]@[a]) = []"
by(simp only:same_level_path_rev_aux.simps upd_rev_cs.simps,clarsimp)+
with all have False by(erule_tac x="as" in allE) fastforce
thus ?thesis by simp
next
case False
with `valid_return_list cs n'` `cs = c'#cs'`
have "valid_return_list cs' (targetnode c')"
apply(clarsimp simp:valid_return_list_def)
apply(erule_tac x="c'#cs'" in allE)
apply(auto simp:targetnodes_def)
apply(case_tac cs') apply auto
apply(case_tac list) apply(auto simp:targetnodes_def)
done
from `valid_edge a` `c' ∈ get_return_edges a`
have "get_proc (sourcenode a) = get_proc (targetnode c')"
by(rule get_proc_get_return_edge)
with `valid_return_list cs' (targetnode c')`
have "valid_return_list cs' (sourcenode a)"
apply(clarsimp simp:valid_return_list_def)
apply(erule_tac x="cs'" in allE)
apply(erule_tac x="c" in allE)
by(auto split:list.split)
from all `kind a = Q:r\<hookrightarrow>⇘p⇙fs` `cs = c'#cs'` `c' ∈ get_return_edges a`
have "∀xs ys. as = xs@ys
--> ¬ same_level_path_rev_aux cs' ys ∨ upd_rev_cs cs' ys ≠ []"
apply clarsimp apply(erule_tac x="xs" in allE)
by auto
from IH[OF `n -as->* sourcenode a` `valid_return_list cs' (sourcenode a)`
False this] show ?thesis .
qed
qed
lemma valid_Entry_path_cases:
assumes "(_Entry_) -as->⇣\<surd>* n" and "as ≠ []"
shows "(∃a' as'. as = as'@[a'] ∧ intra_kind(kind a')) ∨
(∃a' as' Q r p fs. as = as'@[a'] ∧ kind a' = Q:r\<hookrightarrow>⇘p⇙fs) ∨
(∃as' as'' n'. as = as'@as'' ∧ as'' ≠ [] ∧ n' -as''->⇘sl⇙* n)"
proof -
from `as ≠ []` obtain a' as' where "as = as'@[a']" by(cases as rule:rev_cases) auto
thus ?thesis
proof(cases "kind a'" rule:edge_kind_cases)
case Intra with `as = as'@[a']` show ?thesis by simp
next
case Call with `as = as'@[a']` show ?thesis by simp
next
case (Return Q p f)
from `(_Entry_) -as->⇣\<surd>* n` have "(_Entry_) -as->* n" and "valid_path_rev_aux [] as"
by(auto intro:vp_to_vpra simp:vp_def valid_path_def)
from `(_Entry_) -as->* n` `as = as'@[a']`
have "(_Entry_) -as'->* sourcenode a'" and "valid_edge a'"
and "targetnode a' = n"
by(auto intro:path_split_snoc)
from `valid_path_rev_aux [] as` `as = as'@[a']` Return
have "valid_path_rev_aux [a'] as'" by simp
from `valid_edge a'` Return
have "valid_return_list [a'] (sourcenode a')"
apply(clarsimp simp:valid_return_list_def)
apply(case_tac cs')
by(auto intro:get_proc_return[THEN sym])
show ?thesis
proof(cases "∀xs ys. as' = xs@ys -->
(¬ same_level_path_rev_aux [a'] ys ∨ upd_rev_cs [a'] ys ≠ [])")
case True
with `valid_path_rev_aux [a'] as'` `(_Entry_) -as'->* sourcenode a'`
`valid_return_list [a'] (sourcenode a')`
obtain ax Qx fx where "valid_edge ax" and "kind ax = Qx\<hookleftarrow>⇘get_proc (_Entry_)⇙fx"
by(fastforce dest!:vpra_no_slpra)
hence False by(fastforce intro:Main_no_return_source simp:get_proc_Entry)
thus ?thesis by simp
next
case False
then obtain xs ys where "as' = xs@ys" and "same_level_path_rev_aux [a'] ys"
and "upd_rev_cs [a'] ys = []" by auto
with Return have "same_level_path_rev_aux [] (ys@[a'])"
and "upd_rev_cs [] (ys@[a']) = []" by simp_all
from `upd_rev_cs [a'] ys = []` have "ys ≠ []" by auto
with `(_Entry_) -as'->* sourcenode a'` `as' = xs@ys`
have "hd(sourcenodes ys) -ys->* sourcenode a'"
by(cases ys)(auto dest:path_split_second simp:sourcenodes_def)
with `targetnode a' = n` `valid_edge a'`
have "hd(sourcenodes ys) -ys@[a']->* n"
by(fastforce intro:path_Append path_edge)
with `same_level_path_rev_aux [] (ys@[a'])` `upd_rev_cs [] (ys@[a']) = []`
have "same_level_path (ys@[a'])"
by(fastforce dest:slpra_to_slpa simp:same_level_path_def valid_return_list_def)
with `hd(sourcenodes ys) -ys@[a']->* n` have "hd(sourcenodes ys) -ys@[a']->⇘sl⇙* n"
by(simp add:slp_def)
with `as = as'@[a']` `as' = xs@ys` Return
have "∃as' as'' n'. as = as'@as'' ∧ as'' ≠ [] ∧ n' -as''->⇘sl⇙* n"
by(rule_tac x="xs" in exI) auto
thus ?thesis by simp
qed
qed
qed
lemma valid_Entry_path_ascending_path:
assumes "(_Entry_) -as->⇣\<surd>* n"
obtains as' where "(_Entry_) -as'->⇣\<surd>* n"
and "set(sourcenodes as') ⊆ set(sourcenodes as)"
and "∀a' ∈ set as'. intra_kind(kind a') ∨ (∃Q r p fs. kind a' = Q:r\<hookrightarrow>⇘p⇙fs)"
proof(atomize_elim)
from `(_Entry_) -as->⇣\<surd>* n`
show "∃as'. (_Entry_) -as'->⇣\<surd>* n ∧ set(sourcenodes as') ⊆ set(sourcenodes as)∧
(∀a' ∈ set as'. intra_kind(kind a') ∨ (∃Q r p fs. kind a' = Q:r\<hookrightarrow>⇘p⇙fs))"
proof(induct as arbitrary:n rule:length_induct)
fix as n
assume IH:"∀as''. length as'' < length as -->
(∀n'. (_Entry_) -as''->⇣\<surd>* n' -->
(∃as'. (_Entry_) -as'->⇣\<surd>* n' ∧ set (sourcenodes as') ⊆ set (sourcenodes as'') ∧
(∀a'∈set as'. intra_kind (kind a') ∨ (∃Q r p fs. kind a' = Q:r\<hookrightarrow>⇘p⇙fs))))"
and "(_Entry_) -as->⇣\<surd>* n"
show "∃as'. (_Entry_) -as'->⇣\<surd>* n ∧ set(sourcenodes as') ⊆ set(sourcenodes as)∧
(∀a' ∈ set as'. intra_kind(kind a') ∨ (∃Q r p fs. kind a' = Q:r\<hookrightarrow>⇘p⇙fs))"
proof(cases "as = []")
case True
with `(_Entry_) -as->⇣\<surd>* n` show ?thesis by(fastforce simp:sourcenodes_def vp_def)
next
case False
with `(_Entry_) -as->⇣\<surd>* n`
have "((∃a' as'. as = as'@[a'] ∧ intra_kind(kind a')) ∨
(∃a' as' Q r p fs. as = as'@[a'] ∧ kind a' = Q:r\<hookrightarrow>⇘p⇙fs)) ∨
(∃as' as'' n'. as = as'@as'' ∧ as'' ≠ [] ∧ n' -as''->⇘sl⇙* n)"
by(fastforce dest!:valid_Entry_path_cases)
thus ?thesis apply -
proof(erule disjE)+
assume "∃a' as'. as = as'@[a'] ∧ intra_kind(kind a')"
then obtain a' as' where "as = as'@[a']" and "intra_kind(kind a')" by blast
from `(_Entry_) -as->⇣\<surd>* n` `as = as'@[a']`
have "(_Entry_) -as'->⇣\<surd>* sourcenode a'" and "valid_edge a'"
and "targetnode a' = n"
by(auto intro:vp_split_snoc)
from `valid_edge a'` `intra_kind(kind a')`
have "sourcenode a' -[a']->⇘sl⇙* targetnode a'"
by(fastforce intro:path_edge intras_same_level_path simp:slp_def)
from IH `(_Entry_) -as'->⇣\<surd>* sourcenode a'` `as = as'@[a']`
obtain xs where "(_Entry_) -xs->⇣\<surd>* sourcenode a'"
and "set (sourcenodes xs) ⊆ set (sourcenodes as')"
and "∀a'∈set xs. intra_kind (kind a') ∨ (∃Q r p fs. kind a' = Q:r\<hookrightarrow>⇘p⇙fs)"
apply(erule_tac x="as'" in allE) by auto
from `(_Entry_) -xs->⇣\<surd>* sourcenode a'` `sourcenode a' -[a']->⇘sl⇙* targetnode a'`
have "(_Entry_) -xs@[a']->⇣\<surd>* targetnode a'" by(rule vp_slp_Append)
with `targetnode a' = n` have "(_Entry_) -xs@[a']->⇣\<surd>* n" by simp
moreover
from `set (sourcenodes xs) ⊆ set (sourcenodes as')` `as = as'@[a']`
have "set (sourcenodes (xs@[a'])) ⊆ set (sourcenodes as)"
by(auto simp:sourcenodes_def)
moreover
from `∀a'∈set xs. intra_kind (kind a') ∨ (∃Q r p fs. kind a' = Q:r\<hookrightarrow>⇘p⇙fs)`
`intra_kind(kind a')`
have "∀a'∈set (xs@[a']). intra_kind (kind a') ∨
(∃Q r p fs. kind a' = Q:r\<hookrightarrow>⇘p⇙fs)"
by fastforce
ultimately show ?thesis by blast
next
assume "∃a' as' Q r p fs. as = as'@[a'] ∧ kind a' = Q:r\<hookrightarrow>⇘p⇙fs"
then obtain a' as' Q r p fs where "as = as'@[a']" and "kind a' = Q:r\<hookrightarrow>⇘p⇙fs"
by blast
from `(_Entry_) -as->⇣\<surd>* n` `as = as'@[a']`
have "(_Entry_) -as'->⇣\<surd>* sourcenode a'" and "valid_edge a'"
and "targetnode a' = n"
by(auto intro:vp_split_snoc)
from IH `(_Entry_) -as'->⇣\<surd>* sourcenode a'` `as = as'@[a']`
obtain xs where "(_Entry_) -xs->⇣\<surd>* sourcenode a'"
and "set (sourcenodes xs) ⊆ set (sourcenodes as')"
and "∀a'∈set xs. intra_kind (kind a') ∨ (∃Q r p fs. kind a' = Q:r\<hookrightarrow>⇘p⇙fs)"
apply(erule_tac x="as'" in allE) by auto
from `targetnode a' = n` `valid_edge a'` `kind a' = Q:r\<hookrightarrow>⇘p⇙fs`
`(_Entry_) -xs->⇣\<surd>* sourcenode a'`
have "(_Entry_) -xs@[a']->⇣\<surd>* n"
by(fastforce intro:path_Append path_edge vpa_snoc_Call
simp:vp_def valid_path_def)
moreover
from `set (sourcenodes xs) ⊆ set (sourcenodes as')` `as = as'@[a']`
have "set (sourcenodes (xs@[a'])) ⊆ set (sourcenodes as)"
by(auto simp:sourcenodes_def)
moreover
from `∀a'∈set xs. intra_kind (kind a') ∨ (∃Q r p fs. kind a' = Q:r\<hookrightarrow>⇘p⇙fs)`
`kind a' = Q:r\<hookrightarrow>⇘p⇙fs`
have "∀a'∈set (xs@[a']). intra_kind (kind a') ∨
(∃Q r p fs. kind a' = Q:r\<hookrightarrow>⇘p⇙fs)"
by fastforce
ultimately show ?thesis by blast
next
assume "∃as' as'' n'. as = as'@as'' ∧ as'' ≠ [] ∧ n' -as''->⇘sl⇙* n"
then obtain as' as'' n' where "as = as'@as''" and "as'' ≠ []"
and "n' -as''->⇘sl⇙* n" by blast
from `(_Entry_) -as->⇣\<surd>* n` `as = as'@as''` `as'' ≠ []`
have "(_Entry_) -as'->⇣\<surd>* hd(sourcenodes as'')"
by(cases as'',auto intro:vp_split simp:sourcenodes_def)
from `n' -as''->⇘sl⇙* n` `as'' ≠ []` have "hd(sourcenodes as'') = n'"
by(fastforce intro:path_sourcenode simp:slp_def)
from `as = as'@as''` `as'' ≠ []` have "length as' < length as" by simp
with IH `(_Entry_) -as'->⇣\<surd>* hd(sourcenodes as'')`
`hd(sourcenodes as'') = n'`
obtain xs where "(_Entry_) -xs->⇣\<surd>* n'"
and "set (sourcenodes xs) ⊆ set (sourcenodes as')"
and "∀a'∈set xs. intra_kind (kind a') ∨ (∃Q r p fs. kind a' = Q:r\<hookrightarrow>⇘p⇙fs)"
apply(erule_tac x="as'" in allE) by auto
from `n' -as''->⇘sl⇙* n` obtain ys where "n' -ys->⇣ι* n"
and "set(sourcenodes ys) ⊆ set(sourcenodes as'')"
by(erule same_level_path_inner_path)
from `(_Entry_) -xs->⇣\<surd>* n'` `n' -ys->⇣ι* n` have "(_Entry_) -xs@ys->⇣\<surd>* n"
by(fastforce intro:vp_slp_Append intra_path_slp)
moreover
from `set (sourcenodes xs) ⊆ set (sourcenodes as')`
`set(sourcenodes ys) ⊆ set(sourcenodes as'')` `as = as'@as''`
have "set (sourcenodes (xs@ys)) ⊆ set(sourcenodes as)"
by(auto simp:sourcenodes_def)
moreover
from `∀a'∈set xs. intra_kind (kind a') ∨ (∃Q r p fs. kind a' = Q:r\<hookrightarrow>⇘p⇙fs)`
`n' -ys->⇣ι* n`
have "∀a'∈set (xs@ys). intra_kind (kind a') ∨ (∃Q r p fs. kind a' = Q:r\<hookrightarrow>⇘p⇙fs)"
by(fastforce simp:intra_path_def)
ultimately show ?thesis by blast
qed
qed
qed
qed
end
end