Theory CFG
section ‹CFG›
theory CFG imports BasicDefs begin
subsection ‹The abstract CFG›
subsubsection ‹Locale fixes and assumptions›
locale CFG =
fixes sourcenode :: "'edge ⇒ 'node"
fixes targetnode :: "'edge ⇒ 'node"
fixes kind :: "'edge ⇒ ('var,'val,'ret,'pname) edge_kind"
fixes valid_edge :: "'edge ⇒ bool"
fixes Entry::"'node" ("'('_Entry'_')")
fixes get_proc::"'node ⇒ 'pname"
fixes get_return_edges::"'edge ⇒ 'edge set"
fixes procs::"('pname × 'var list × 'var list) list"
fixes Main::"'pname"
assumes Entry_target [dest]: "⟦valid_edge a; targetnode a = (_Entry_)⟧ ⟹ False"
and get_proc_Entry:"get_proc (_Entry_) = Main"
and Entry_no_call_source:
"⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; sourcenode a = (_Entry_)⟧ ⟹ False"
and edge_det:
"⟦valid_edge a; valid_edge a'; sourcenode a = sourcenode a';
targetnode a = targetnode a'⟧ ⟹ a = a'"
and Main_no_call_target:"⟦valid_edge a; kind a = Q:r↪⇘Main⇙f⟧ ⟹ False"
and Main_no_return_source:"⟦valid_edge a; kind a = Q'↩⇘Main⇙f'⟧ ⟹ False"
and callee_in_procs:
"⟦valid_edge a; kind a = Q:r↪⇘p⇙fs⟧ ⟹ ∃ins outs. (p,ins,outs) ∈ set procs"
and get_proc_intra:"⟦valid_edge a; intra_kind(kind a)⟧
⟹ get_proc (sourcenode a) = get_proc (targetnode a)"
and get_proc_call:
"⟦valid_edge a; kind a = Q:r↪⇘p⇙fs⟧ ⟹ get_proc (targetnode a) = p"
and get_proc_return:
"⟦valid_edge a; kind a = Q'↩⇘p⇙f'⟧ ⟹ get_proc (sourcenode a) = p"
and call_edges_only:"⟦valid_edge a; kind a = Q:r↪⇘p⇙fs⟧
⟹ ∀a'. valid_edge a' ∧ targetnode a' = targetnode a ⟶
(∃Qx rx fsx. kind a' = Qx:rx↪⇘p⇙fsx)"
and return_edges_only:"⟦valid_edge a; kind a = Q'↩⇘p⇙f'⟧
⟹ ∀a'. valid_edge a' ∧ sourcenode a' = sourcenode a ⟶
(∃Qx fx. kind a' = Qx↩⇘p⇙fx)"
and get_return_edge_call:
"⟦valid_edge a; kind a = Q:r↪⇘p⇙fs⟧ ⟹ get_return_edges a ≠ {}"
and get_return_edges_valid:
"⟦valid_edge a; a' ∈ get_return_edges a⟧ ⟹ valid_edge a'"
and only_call_get_return_edges:
"⟦valid_edge a; a' ∈ get_return_edges a⟧ ⟹ ∃Q r p fs. kind a = Q:r↪⇘p⇙fs"
and call_return_edges:
"⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; a' ∈ get_return_edges a⟧
⟹ ∃Q' f'. kind a' = Q'↩⇘p⇙f'"
and return_needs_call: "⟦valid_edge a; kind a = Q'↩⇘p⇙f'⟧
⟹ ∃!a'. valid_edge a' ∧ (∃Q r fs. kind a' = Q:r↪⇘p⇙fs) ∧ a ∈ get_return_edges a'"
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)⇩√"
and call_return_node_edge:
"⟦valid_edge a; a' ∈ get_return_edges a⟧
⟹ ∃a''. valid_edge a'' ∧ sourcenode a'' = sourcenode a ∧
targetnode a'' = targetnode a' ∧ kind a'' = (λcf. False)⇩√"
and call_only_one_intra_edge:
"⟦valid_edge a; kind a = Q:r↪⇘p⇙fs⟧
⟹ ∃!a'. valid_edge a' ∧ sourcenode a' = sourcenode a ∧ intra_kind(kind a')"
and return_only_one_intra_edge:
"⟦valid_edge a; kind a = Q'↩⇘p⇙f'⟧
⟹ ∃!a'. valid_edge a' ∧ targetnode a' = targetnode a ∧ intra_kind(kind a')"
and same_proc_call_unique_target:
"⟦valid_edge a; valid_edge a'; kind a = Q⇩1:r⇩1↪⇘p⇙fs⇩1; kind a' = Q⇩2:r⇩2↪⇘p⇙fs⇩2⟧
⟹ targetnode a = targetnode a'"
and unique_callers:"distinct_fst procs"
and distinct_formal_ins:"(p,ins,outs) ∈ set procs ⟹ distinct ins"
and distinct_formal_outs:"(p,ins,outs) ∈ set procs ⟹ distinct outs"
begin
lemma get_proc_get_return_edge:
assumes "valid_edge a" and "a' ∈ get_return_edges a"
shows "get_proc (sourcenode a) = get_proc (targetnode a')"
proof -
from assms obtain ax where "valid_edge ax" and "sourcenode a = sourcenode ax"
and "targetnode a' = targetnode ax" and "intra_kind(kind ax)"
by(auto dest:call_return_node_edge simp:intra_kind_def)
thus ?thesis by(fastforce intro:get_proc_intra)
qed
lemma call_intra_edge_False:
assumes "valid_edge a" and "kind a = Q:r↪⇘p⇙fs" and "valid_edge a'"
and "sourcenode a = sourcenode a'" and "intra_kind(kind a')"
shows "kind a' = (λcf. False)⇩√"
proof -
from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› obtain ax where "ax ∈ get_return_edges a"
by(fastforce dest:get_return_edge_call)
with ‹valid_edge a› obtain a'' where "valid_edge a''"
and "sourcenode a'' = sourcenode a" and "kind a'' = (λcf. False)⇩√"
by(fastforce dest:call_return_node_edge)
from ‹kind a'' = (λcf. False)⇩√› have "intra_kind(kind a'')"
by(simp add:intra_kind_def)
with assms ‹valid_edge a''› ‹sourcenode a'' = sourcenode a›
‹kind a'' = (λcf. False)⇩√›
show ?thesis by(fastforce dest:call_only_one_intra_edge)
qed
lemma formal_in_THE:
"⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; (p,ins,outs) ∈ set procs⟧
⟹ (THE ins. ∃outs. (p,ins,outs) ∈ set procs) = ins"
by(fastforce dest:distinct_fst_isin_same_fst intro:unique_callers)
lemma formal_out_THE:
"⟦valid_edge a; kind a = Q↩⇘p⇙f; (p,ins,outs) ∈ set procs⟧
⟹ (THE outs. ∃ins. (p,ins,outs) ∈ set procs) = outs"
by(fastforce dest:distinct_fst_isin_same_fst intro:unique_callers)
subsubsection ‹Transfer and predicate functions›
fun params :: "(('var ⇀ 'val) ⇀ 'val) list ⇒ ('var ⇀ 'val) ⇒ 'val option list"
where "params [] cf = []"
| "params (f#fs) cf = (f cf)#params fs cf"
lemma params_nth:
"i < length fs ⟹ (params fs cf)!i = (fs!i) cf"
by(induct fs arbitrary:i,auto,case_tac i,auto)
lemma [simp]:"length (params fs cf) = length fs"
by(induct fs) auto
fun transfer :: "('var,'val,'ret,'pname) edge_kind ⇒ (('var ⇀ 'val) × 'ret) list ⇒
(('var ⇀ 'val) × 'ret) list"
where "transfer (⇑f) (cf#cfs) = (f (fst cf),snd cf)#cfs"
| "transfer (Q)⇩√ (cf#cfs) = (cf#cfs)"
| "transfer (Q:r↪⇘p⇙fs) (cf#cfs) =
(let ins = THE ins. ∃outs. (p,ins,outs) ∈ set procs in
(Map.empty(ins [:=] params fs (fst cf)),r)#cf#cfs)"
| "transfer (Q↩⇘p⇙f )(cf#cfs) = (case cfs of [] ⇒ []
| cf'#cfs' ⇒ (f (fst cf) (fst cf'),snd cf')#cfs')"
| "transfer et [] = []"
fun transfers :: "('var,'val,'ret,'pname) edge_kind list ⇒ (('var ⇀ 'val) × 'ret) list ⇒
(('var ⇀ 'val) × 'ret) list"
where "transfers [] s = s"
| "transfers (et#ets) s = transfers ets (transfer et s)"
fun pred :: "('var,'val,'ret,'pname) edge_kind ⇒ (('var ⇀ 'val) × 'ret) list ⇒ bool"
where "pred (⇑f) (cf#cfs) = True"
| "pred (Q)⇩√ (cf#cfs) = Q (fst cf)"
| "pred (Q:r↪⇘p⇙fs) (cf#cfs) = Q (fst cf,r)"
| "pred (Q↩⇘p⇙f) (cf#cfs) = (Q cf ∧ cfs ≠ [])"
| "pred et [] = False"
fun preds :: "('var,'val,'ret,'pname) edge_kind list ⇒ (('var ⇀ 'val) × 'ret) list ⇒ bool"
where "preds [] s = True"
| "preds (et#ets) s = (pred et s ∧ preds ets (transfer et s))"
lemma transfers_split:
"(transfers (ets@ets') s) = (transfers ets' (transfers ets s))"
by(induct ets arbitrary:s) auto
lemma preds_split:
"(preds (ets@ets') s) = (preds ets s ∧ preds ets' (transfers ets s))"
by(induct ets arbitrary:s) auto
abbreviation state_val :: "(('var ⇀ 'val) × 'ret) list ⇒ 'var ⇀ 'val"
where "state_val s V ≡ (fst (hd s)) V"
subsubsection ‹‹valid_node››
definition valid_node :: "'node ⇒ bool"
where "valid_node n ≡
(∃a. valid_edge a ∧ (n = sourcenode a ∨ n = targetnode a))"
lemma [simp]: "valid_edge a ⟹ valid_node (sourcenode a)"
by(fastforce simp:valid_node_def)
lemma [simp]: "valid_edge a ⟹ valid_node (targetnode a)"
by(fastforce simp:valid_node_def)
subsection ‹CFG paths›
inductive path :: "'node ⇒ 'edge list ⇒ 'node ⇒ bool"
("_ -_→* _" [51,0,0] 80)
where
empty_path:"valid_node n ⟹ n -[]→* n"
| Cons_path:
"⟦n'' -as→* n'; valid_edge a; sourcenode a = n; targetnode a = n''⟧
⟹ n -a#as→* n'"
lemma path_valid_node:
assumes "n -as→* n'" shows "valid_node n" and "valid_node n'"
using ‹n -as→* n'›
by(induct rule:path.induct,auto)
lemma empty_path_nodes [dest]:"n -[]→* n' ⟹ n = n'"
by(fastforce elim:path.cases)
lemma path_valid_edges:"n -as→* n' ⟹ ∀a ∈ set as. valid_edge a"
by(induct rule:path.induct) auto
lemma path_edge:"valid_edge a ⟹ sourcenode a -[a]→* targetnode a"
by(fastforce intro:Cons_path empty_path)
lemma path_Append:"⟦n -as→* n''; n'' -as'→* n'⟧
⟹ n -as@as'→* n'"
by(induct rule:path.induct,auto intro:Cons_path)
lemma path_split:
assumes "n -as@a#as'→* n'"
shows "n -as→* sourcenode a" and "valid_edge a" and "targetnode a -as'→* n'"
using ‹n -as@a#as'→* n'›
proof(induct as arbitrary:n)
case Nil case 1
thus ?case by(fastforce elim:path.cases intro:empty_path)
next
case Nil case 2
thus ?case by(fastforce elim:path.cases intro:path_edge)
next
case Nil case 3
thus ?case by(fastforce elim:path.cases)
next
case (Cons ax asx)
note IH1 = ‹⋀n. n -asx@a#as'→* n' ⟹ n -asx→* sourcenode a›
note IH2 = ‹⋀n. n -asx@a#as'→* n' ⟹ valid_edge a›
note IH3 = ‹⋀n. n -asx@a#as'→* n' ⟹ targetnode a -as'→* n'›
{ case 1
hence "sourcenode ax = n" and "targetnode ax -asx@a#as'→* n'" and "valid_edge ax"
by(auto elim:path.cases)
from IH1[OF ‹ targetnode ax -asx@a#as'→* n'›]
have "targetnode ax -asx→* sourcenode a" .
with ‹sourcenode ax = n› ‹valid_edge ax› show ?case by(fastforce intro:Cons_path)
next
case 2 hence "targetnode ax -asx@a#as'→* n'" by(auto elim:path.cases)
from IH2[OF this] show ?case .
next
case 3 hence "targetnode ax -asx@a#as'→* n'" by(auto elim:path.cases)
from IH3[OF this] show ?case .
}
qed
lemma path_split_Cons:
assumes "n -as→* n'" and "as ≠ []"
obtains a' as' where "as = a'#as'" and "n = sourcenode a'"
and "valid_edge a'" and "targetnode a' -as'→* n'"
proof(atomize_elim)
from ‹as ≠ []› obtain a' as' where "as = a'#as'" by(cases as) auto
with ‹n -as→* n'› have "n -[]@a'#as'→* n'" by simp
hence "n -[]→* sourcenode a'" and "valid_edge a'" and "targetnode a' -as'→* n'"
by(rule path_split)+
from ‹n -[]→* sourcenode a'› have "n = sourcenode a'" by fast
with ‹as = a'#as'› ‹valid_edge a'› ‹targetnode a' -as'→* n'›
show "∃a' as'. as = a'#as' ∧ n = sourcenode a' ∧ valid_edge a' ∧
targetnode a' -as'→* n'"
by fastforce
qed
lemma path_split_snoc:
assumes "n -as→* n'" and "as ≠ []"
obtains a' as' where "as = as'@[a']" and "n -as'→* sourcenode a'"
and "valid_edge a'" and "n' = targetnode a'"
proof(atomize_elim)
from ‹as ≠ []› obtain a' as' where "as = as'@[a']" by(cases as rule:rev_cases) auto
with ‹n -as→* n'› have "n -as'@a'#[]→* n'" by simp
hence "n -as'→* sourcenode a'" and "valid_edge a'" and "targetnode a' -[]→* n'"
by(rule path_split)+
from ‹targetnode a' -[]→* n'› have "n' = targetnode a'" by fast
with ‹as = as'@[a']› ‹valid_edge a'› ‹n -as'→* sourcenode a'›
show "∃as' a'. as = as'@[a'] ∧ n -as'→* sourcenode a' ∧ valid_edge a' ∧
n' = targetnode a'"
by fastforce
qed
lemma path_split_second:
assumes "n -as@a#as'→* n'" shows "sourcenode a -a#as'→* n'"
proof -
from ‹n -as@a#as'→* n'› have "valid_edge a" and "targetnode a -as'→* n'"
by(auto intro:path_split)
thus ?thesis by(fastforce intro:Cons_path)
qed
lemma path_Entry_Cons:
assumes "(_Entry_) -as→* n'" and "n' ≠ (_Entry_)"
obtains n a where "sourcenode a = (_Entry_)" and "targetnode a = n"
and "n -tl as→* n'" and "valid_edge a" and "a = hd as"
proof(atomize_elim)
from ‹(_Entry_) -as→* n'› ‹n' ≠ (_Entry_)› have "as ≠ []"
by(cases as,auto elim:path.cases)
with ‹(_Entry_) -as→* n'› obtain a' as' where "as = a'#as'"
and "(_Entry_) = sourcenode a'" and "valid_edge a'" and "targetnode a' -as'→* n'"
by(erule path_split_Cons)
thus "∃a n. sourcenode a = (_Entry_) ∧ targetnode a = n ∧ n -tl as→* n' ∧
valid_edge a ∧ a = hd as"
by fastforce
qed
lemma path_det:
"⟦n -as→* n'; n -as→* n''⟧ ⟹ n' = n''"
proof(induct as arbitrary:n)
case Nil thus ?case by(auto elim:path.cases)
next
case (Cons a' as')
note IH = ‹⋀n. ⟦n -as'→* n'; n -as'→* n''⟧ ⟹ n' = n''›
from ‹n -a'#as'→* n'› have "targetnode a' -as'→* n'"
by(fastforce elim:path_split_Cons)
from ‹n -a'#as'→* n''› have "targetnode a' -as'→* n''"
by(fastforce elim:path_split_Cons)
from IH[OF ‹targetnode a' -as'→* n'› this] show ?thesis .
qed
definition
sourcenodes :: "'edge list ⇒ 'node list"
where "sourcenodes xs ≡ map sourcenode xs"
definition
kinds :: "'edge list ⇒ ('var,'val,'ret,'pname) edge_kind list"
where "kinds xs ≡ map kind xs"
definition
targetnodes :: "'edge list ⇒ 'node list"
where "targetnodes xs ≡ map targetnode xs"
lemma path_sourcenode:
"⟦n -as→* n'; as ≠ []⟧ ⟹ hd (sourcenodes as) = n"
by(fastforce elim:path_split_Cons simp:sourcenodes_def)
lemma path_targetnode:
"⟦n -as→* n'; as ≠ []⟧ ⟹ last (targetnodes as) = n'"
by(fastforce elim:path_split_snoc simp:targetnodes_def)
lemma sourcenodes_is_n_Cons_butlast_targetnodes:
"⟦n -as→* n'; as ≠ []⟧ ⟹
sourcenodes as = n#(butlast (targetnodes as))"
proof(induct as arbitrary:n)
case Nil thus ?case by simp
next
case (Cons a' as')
note IH = ‹⋀n. ⟦n -as'→* n'; as' ≠ []⟧
⟹ sourcenodes as' = n#(butlast (targetnodes as'))›
from ‹n -a'#as'→* n'› have "n = sourcenode a'" and "targetnode a' -as'→* n'"
by(auto elim:path_split_Cons)
show ?case
proof(cases "as' = []")
case True
with ‹targetnode a' -as'→* n'› have "targetnode a' = n'" by fast
with True ‹n = sourcenode a'› show ?thesis
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)⇩√"
by(fastforce dest:intra_proc_additional_edge)
from ‹valid_edge a''› ‹kind a'' = (λcf. False)⇩√›
have "get_proc(sourcenode a'') = get_proc(targetnode a'')"
by(fastforce intro:get_proc_intra simp:intra_kind_def)
with ‹sourcenode a'' = targetnode a› ‹targetnode a'' = sourcenode a'›
show ?thesis by simp
qed
subsubsection ‹Valid paths›
declare conj_cong[fundef_cong]
fun valid_path_aux :: "'edge list ⇒ 'edge list ⇒ bool"
where "valid_path_aux cs [] ⟷ True"
| "valid_path_aux cs (a#as) ⟷
(case (kind a) of Q:r↪⇘p⇙fs ⇒ valid_path_aux (a#cs) as
| Q↩⇘p⇙f ⇒ case cs of [] ⇒ valid_path_aux [] as
| c'#cs' ⇒ a ∈ get_return_edges c' ∧
valid_path_aux cs' as
| _ ⇒ valid_path_aux cs as)"
lemma vpa_induct [consumes 1,case_names vpa_empty vpa_intra vpa_Call vpa_ReturnEmpty
vpa_ReturnCons]:
assumes major: "valid_path_aux xs ys"
and rules: "⋀cs. P cs []"
"⋀cs a as. ⟦intra_kind(kind a); valid_path_aux cs as; P cs as⟧ ⟹ P cs (a#as)"
"⋀cs a as Q r p fs. ⟦kind a = Q:r↪⇘p⇙fs; valid_path_aux (a#cs) as; P (a#cs) as⟧
⟹ P cs (a#as)"
"⋀cs a as Q p f. ⟦kind a = Q↩⇘p⇙f; cs = []; valid_path_aux [] as; P [] as⟧
⟹ P cs (a#as)"
"⋀cs a as Q p f c' cs' . ⟦kind a = Q↩⇘p⇙f; cs = c'#cs'; valid_path_aux cs' as;
a ∈ get_return_edges c'; P cs' as⟧
⟹ P cs (a#as)"
shows "P xs ys"
using major
apply(induct ys arbitrary: xs)
by(auto intro:rules split:edge_kind.split_asm list.split_asm simp:intra_kind_def)
lemma valid_path_aux_intra_path:
"∀a ∈ set as. intra_kind(kind a) ⟹ valid_path_aux cs as"
by(induct as,auto simp:intra_kind_def)
lemma valid_path_aux_callstack_prefix:
"valid_path_aux (cs@cs') as ⟹ valid_path_aux cs as"
proof(induct "cs@cs'" as arbitrary:cs cs' rule:vpa_induct)
case vpa_empty thus ?case by simp
next
case (vpa_intra a as)
hence "valid_path_aux cs as" by simp
with ‹intra_kind (kind a)› show ?case by(cases "kind a",auto simp:intra_kind_def)
next
case (vpa_Call a as Q r p fs cs'' cs')
note IH = ‹⋀xs ys. a#cs''@cs' = xs@ys ⟹ valid_path_aux xs as›
have "a#cs''@cs' = (a#cs'')@cs'" by simp
from IH[OF this] have "valid_path_aux (a#cs'') as" .
with ‹kind a = Q:r↪⇘p⇙fs› show ?case by simp
next
case (vpa_ReturnEmpty a as Q p f cs'' cs')
hence "valid_path_aux cs'' as" by simp
with ‹kind a = Q↩⇘p⇙f› ‹cs''@cs' = []› show ?case by simp
next
case (vpa_ReturnCons a as Q p f c' cs' csx csx')
note IH = ‹⋀xs ys. cs' = xs@ys ⟹ valid_path_aux xs as›
from ‹csx@csx' = c'#cs'›
have "csx = [] ∧ csx' = c'#cs' ∨ (∃zs. csx = c'#zs ∧ zs@csx' = cs')"
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↩⇘p⇙f› show ?thesis by simp
next
assume "∃zs. csx = c'#zs ∧ zs@csx' = cs'"
then obtain zs where "csx = c'#zs" and "cs' = zs@csx'" by auto
from IH[OF ‹cs' = zs@csx'›] have "valid_path_aux zs as" .
with ‹csx = c'#zs› ‹kind a = Q↩⇘p⇙f› ‹a ∈ get_return_edges c'›
show ?thesis by simp
qed
qed
fun upd_cs :: "'edge list ⇒ 'edge list ⇒ 'edge list"
where "upd_cs cs [] = cs"
| "upd_cs cs (a#as) =
(case (kind a) of Q:r↪⇘p⇙fs ⇒ upd_cs (a#cs) as
| Q↩⇘p⇙f ⇒ case cs of [] ⇒ upd_cs cs as
| c'#cs' ⇒ upd_cs cs' as
| _ ⇒ upd_cs cs as)"
lemma upd_cs_empty [dest]:
"upd_cs cs [] = [] ⟹ cs = []"
by(cases cs) auto
lemma upd_cs_intra_path:
"∀a ∈ set as. intra_kind(kind a) ⟹ upd_cs cs as = cs"
by(induct as,auto simp:intra_kind_def)
lemma upd_cs_Append:
"⟦upd_cs cs as = cs'; upd_cs cs' as' = cs''⟧ ⟹ upd_cs cs (as@as') = cs''"
by(induct as arbitrary:cs,auto split:edge_kind.split list.split)
lemma upd_cs_empty_split:
assumes "upd_cs cs as = []" and "cs ≠ []" and "as ≠ []"
obtains xs ys where "as = xs@ys" and "xs ≠ []" and "upd_cs cs xs = []"
and "∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []"
and "upd_cs [] ys = []"
proof(atomize_elim)
from ‹upd_cs cs as = []› ‹cs ≠ []› ‹as ≠ []›
show "∃xs ys. as = xs@ys ∧ xs ≠ [] ∧ upd_cs cs xs = [] ∧
(∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []) ∧
upd_cs [] ys = []"
proof(induct as arbitrary:cs)
case Nil thus ?case by simp
next
case (Cons a' as')
note IH = ‹⋀cs. ⟦upd_cs cs as' = []; cs ≠ []; as' ≠ []⟧
⟹ ∃xs ys. as' = xs@ys ∧ xs ≠ [] ∧ upd_cs cs xs = [] ∧
(∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []) ∧
upd_cs [] ys = []›
show ?case
proof(cases "kind a'" rule:edge_kind_cases)
case Intra
with ‹upd_cs cs (a'#as') = []› have "upd_cs cs as' = []"
by(fastforce simp:intra_kind_def)
with ‹cs ≠ []› have "as' ≠ []" by fastforce
from IH[OF ‹upd_cs cs as' = []› ‹cs ≠ []› this] obtain xs ys where "as' = xs@ys"
and "xs ≠ []" and "upd_cs cs xs = []" and "upd_cs [] ys = []"
and "∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []" by blast
from ‹upd_cs cs xs = []› Intra have "upd_cs cs (a'#xs) = []"
by(fastforce simp:intra_kind_def)
from ‹∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []› ‹xs ≠ []› Intra
have "∀xs' ys'. a'#xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []"
apply auto
apply(case_tac xs') apply(auto simp:intra_kind_def)
by(erule_tac x="[]" in allE,fastforce)+
with ‹as' = xs@ys› ‹upd_cs cs (a'#xs) = []› ‹upd_cs [] ys = []›
show ?thesis apply(rule_tac x="a'#xs" in exI) by fastforce
next
case (Call Q p f)
with ‹upd_cs cs (a'#as') = []› have "upd_cs (a'#cs) as' = []" by simp
with ‹cs ≠ []› have "as' ≠ []" by fastforce
from IH[OF ‹upd_cs (a'#cs) as' = []› _ this] obtain xs ys where "as' = xs@ys"
and "xs ≠ []" and "upd_cs (a'#cs) xs = []" and "upd_cs [] ys = []"
and "∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs (a'#cs) xs' ≠ []" by blast
from ‹upd_cs (a'#cs) xs = []› Call have "upd_cs cs (a'#xs) = []" by simp
from ‹∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs (a'#cs) xs' ≠ []›
‹xs ≠ []› ‹cs ≠ []› Call
have "∀xs' ys'. a'#xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []"
by auto(case_tac xs',auto)
with ‹as' = xs@ys› ‹upd_cs cs (a'#xs) = []› ‹upd_cs [] ys = []›
show ?thesis apply(rule_tac x="a'#xs" in exI) by fastforce
next
case (Return Q p f)
with ‹upd_cs cs (a'#as') = []› ‹cs ≠ []› obtain c' cs' where "cs = c'#cs'"
and "upd_cs cs' as' = []" by(cases cs) auto
show ?thesis
proof(cases "cs' = []")
case True
with ‹cs = c'#cs'› ‹upd_cs cs' as' = []› Return show ?thesis
apply(rule_tac x="[a']" in exI) apply clarsimp
by(case_tac xs') auto
next
case False
with ‹upd_cs cs' as' = []› have "as' ≠ []" by fastforce
from IH[OF ‹upd_cs cs' as' = []› False this] obtain xs ys where "as' = xs@ys"
and "xs ≠ []" and "upd_cs cs' xs = []" and "upd_cs [] ys = []"
and "∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs' xs' ≠ []" by blast
from ‹upd_cs cs' xs = []› ‹cs = c'#cs'› Return have "upd_cs cs (a'#xs) = []"
by simp
from ‹∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs' xs' ≠ []›
‹xs ≠ []› ‹cs = c'#cs'› Return
have "∀xs' ys'. a'#xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs cs xs' ≠ []"
by auto(case_tac xs',auto)
with ‹as' = xs@ys› ‹upd_cs cs (a'#xs) = []› ‹upd_cs [] ys = []›
show ?thesis apply(rule_tac x="a'#xs" in exI) by fastforce
qed
qed
qed
qed
lemma upd_cs_snoc_Return_Cons:
assumes "kind a = Q↩⇘p⇙f"
shows "upd_cs cs as = c'#cs' ⟹ upd_cs cs (as@[a]) = cs'"
proof(induct as arbitrary:cs)
case Nil
with ‹kind a = Q↩⇘p⇙f› have "upd_cs cs [a] = cs'" by simp
thus ?case by simp
next
case (Cons a' as')
note IH = ‹⋀cs. upd_cs cs as' = c'#cs' ⟹ upd_cs cs (as'@[a]) = cs'›
show ?case
proof(cases "kind a'" rule:edge_kind_cases)
case Intra
with ‹upd_cs cs (a'#as') = c'#cs'›
have "upd_cs cs as' = c'#cs'" by(fastforce simp:intra_kind_def)
from IH[OF this] have "upd_cs cs (as'@[a]) = cs'" .
with Intra show ?thesis by(fastforce simp:intra_kind_def)
next
case Call
with ‹upd_cs cs (a'#as') = c'#cs'›
have "upd_cs (a'#cs) as' = c'#cs'" by simp
from IH[OF this] have "upd_cs (a'#cs) (as'@[a]) = cs'" .
with Call show ?thesis by simp
next
case Return
show ?thesis
proof(cases cs)
case Nil
with ‹upd_cs cs (a'#as') = c'#cs'› Return
have "upd_cs cs as' = c'#cs'" by simp
from IH[OF this] have "upd_cs cs (as'@[a]) = cs'" .
with Nil Return show ?thesis by simp
next
case (Cons cx csx)
with ‹upd_cs cs (a'#as') = c'#cs'› Return
have "upd_cs csx as' = c'#cs'" by simp
from IH[OF this] have "upd_cs csx (as'@[a]) = cs'" .
with Cons Return show ?thesis by simp
qed
qed
qed
lemma upd_cs_snoc_Call:
assumes "kind a = Q:r↪⇘p⇙fs"
shows "upd_cs cs (as@[a]) = a#(upd_cs cs as)"
proof(induct as arbitrary:cs)
case Nil
with ‹kind a = Q:r↪⇘p⇙fs› show ?case by simp
next
case (Cons a' as')
note IH = ‹⋀cs. upd_cs cs (as'@[a]) = a#upd_cs cs as'›
show ?case
proof(cases "kind a'" rule:edge_kind_cases)
case Intra
with IH[of cs] show ?thesis by(fastforce simp:intra_kind_def)
next
case Call
with IH[of "a'#cs"] show ?thesis by simp
next
case Return
show ?thesis
proof(cases cs)
case Nil
with IH[of "[]"] Return show ?thesis by simp
next
case (Cons cx csx)
with IH[of csx] Return show ?thesis by simp
qed
qed
qed
lemma valid_path_aux_split:
assumes "valid_path_aux cs (as@as')"
shows "valid_path_aux cs as" and "valid_path_aux (upd_cs cs as) as'"
using ‹valid_path_aux cs (as@as')›
proof(induct cs "as@as'" arbitrary:as as' rule:vpa_induct)
case (vpa_intra cs a as as'')
note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux cs xs›
note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux (upd_cs cs xs) ys›
{ case 1
from vpa_intra
have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')"
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↪⇘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↪⇘p⇙fs›
show ?thesis by clarsimp
next
assume "∃xs. a#xs = as'' ∧ as = xs@as'"
then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
from IH2[OF ‹as = xs@as'›] have "valid_path_aux (upd_cs (a # cs) xs) as'" .
with ‹a#xs = as''›[THEN sym] ‹kind a = Q:r↪⇘p⇙fs›
show ?thesis by simp
qed
}
next
case (vpa_ReturnEmpty cs a as Q p f as'')
note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux [] xs›
note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux (upd_cs [] xs) ys›
{ case 1
from vpa_ReturnEmpty
have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')"
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↩⇘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↩⇘p⇙f› ‹cs = []›
show ?thesis by fastforce
next
assume "∃xs. a#xs = as'' ∧ as = xs@as'"
then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
from IH2[OF ‹as = xs@as'›] have "valid_path_aux (upd_cs [] xs) as'" .
from ‹a#xs = as''›[THEN sym] ‹kind a = Q↩⇘p⇙f› ‹cs = []›
have "upd_cs [] xs = upd_cs cs as''" by simp
with ‹valid_path_aux (upd_cs [] xs) as'› show ?thesis by simp
qed
}
next
case (vpa_ReturnCons cs a as Q p f c' cs' as'')
note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux cs' xs›
note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_aux (upd_cs cs' xs) ys›
{ case 1
from vpa_ReturnCons
have "as'' = [] ∧ a#as = as' ∨ (∃xs. a#xs = as'' ∧ as = xs@as')"
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↩⇘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↩⇘p⇙f› ‹cs = c'#cs'›
‹a ∈ get_return_edges c'›
show ?thesis by fastforce
next
assume "∃xs. a#xs = as'' ∧ as = xs@as'"
then obtain xs where "a#xs = as''" and "as = xs@as'" by auto
from IH2[OF ‹as = xs@as'›] have "valid_path_aux (upd_cs cs' xs) as'" .
from ‹a#xs = as''›[THEN sym] ‹kind a = Q↩⇘p⇙f› ‹cs = c'#cs'›
have "upd_cs cs' xs = upd_cs cs as''" by simp
with ‹valid_path_aux (upd_cs cs' xs) as'› show ?thesis by simp
qed
}
qed simp_all
lemma valid_path_aux_Append:
"⟦valid_path_aux cs as; valid_path_aux (upd_cs cs as) as'⟧
⟹ valid_path_aux cs (as@as')"
by(induct rule:vpa_induct,auto simp:intra_kind_def)
lemma vpa_snoc_Call:
assumes "kind a = Q:r↪⇘p⇙fs"
shows "valid_path_aux cs as ⟹ valid_path_aux cs (as@[a])"
proof(induct rule:vpa_induct)
case (vpa_empty cs)
from ‹kind a = Q:r↪⇘p⇙fs› have "valid_path_aux cs [a]" by simp
thus ?case by simp
next
case (vpa_intra cs a' as')
from ‹valid_path_aux cs (as'@[a])› ‹intra_kind (kind a')›
have "valid_path_aux cs (a'#(as'@[a]))"
by(fastforce simp:intra_kind_def)
thus ?case by simp
next
case (vpa_Call cs a' as' Q' r' p' fs')
from ‹valid_path_aux (a'#cs) (as'@[a])› ‹kind a' = Q':r'↪⇘p'⇙fs'›
have "valid_path_aux cs (a'#(as'@[a]))" by simp
thus ?case by simp
next
case (vpa_ReturnEmpty cs a' as' Q' p' f')
from ‹valid_path_aux [] (as'@[a])› ‹kind a' = Q'↩⇘p'⇙f'› ‹cs = []›
have "valid_path_aux cs (a'#(as'@[a]))" by simp
thus ?case by simp
next
case (vpa_ReturnCons cs a' as' Q' p' f' c' cs')
from ‹valid_path_aux cs' (as'@[a])› ‹kind a' = Q'↩⇘p'⇙f'› ‹cs = c'#cs'›
‹a' ∈ get_return_edges c'›
have "valid_path_aux cs (a'#(as'@[a]))" by simp
thus ?case by simp
qed
definition valid_path :: "'edge list ⇒ bool"
where "valid_path as ≡ valid_path_aux [] as"
lemma valid_path_aux_valid_path:
"valid_path_aux cs as ⟹ valid_path as"
by(fastforce intro:valid_path_aux_callstack_prefix simp:valid_path_def)
lemma valid_path_split:
assumes "valid_path (as@as')" shows "valid_path as" and "valid_path as'"
using ‹valid_path (as@as')›
apply(auto simp:valid_path_def)
apply(erule valid_path_aux_split)
apply(drule valid_path_aux_split(2))
by(fastforce intro:valid_path_aux_callstack_prefix)
definition valid_path' :: "'node ⇒ 'edge list ⇒ 'node ⇒ bool"
("_ -_→⇩√* _" [51,0,0] 80)
where vp_def:"n -as→⇩√* n' ≡ n -as→* n' ∧ valid_path as"
lemma intra_path_vp:
assumes "n -as→⇩ι* n'" shows "n -as→⇩√* n'"
proof -
from ‹n -as→⇩ι* n'› have "n -as→* n'" and "∀a ∈ set as. intra_kind(kind a)"
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→⇩√* n'" and "as ≠ []"
obtains a' as' where "as = a'#as'" and "n = sourcenode a'"
and "valid_edge a'" and "targetnode a' -as'→⇩√* n'"
proof(atomize_elim)
from ‹n -as→⇩√* n'› ‹as ≠ []› obtain a' as' where "as = a'#as'"
and "n = sourcenode a'" and "valid_edge a'" and "targetnode a' -as'→* n'"
by(fastforce elim:path_split_Cons simp:vp_def)
from ‹n -as→⇩√* n'› have "valid_path as" by(simp add:vp_def)
from ‹as = a'#as'› have "as = [a']@as'" by simp
with ‹valid_path as› have "valid_path ([a']@as')" by simp
hence "valid_path as'" by(rule valid_path_split)
with ‹targetnode a' -as'→* n'› have "targetnode a' -as'→⇩√* n'" by(simp add:vp_def)
with ‹as = a'#as'› ‹n = sourcenode a'› ‹valid_edge a'›
show "∃a' as'. as = a'#as' ∧ n = sourcenode a' ∧ valid_edge a' ∧
targetnode a' -as'→⇩√* n'" by blast
qed
lemma vp_split_snoc:
assumes "n -as→⇩√* n'" and "as ≠ []"
obtains a' as' where "as = as'@[a']" and "n -as'→⇩√* sourcenode a'"
and "valid_edge a'" and "n' = targetnode a'"
proof(atomize_elim)
from ‹n -as→⇩√* n'› ‹as ≠ []› obtain a' as' where "as = as'@[a']"
and "n -as'→* sourcenode a'" and "valid_edge a'" and "n' = targetnode a'"
by(clarsimp simp:vp_def)(erule path_split_snoc,auto)
from ‹n -as→⇩√* n'› ‹as = as'@[a']› have "valid_path (as'@[a'])" by(simp add:vp_def)
hence "valid_path as'" by(rule valid_path_split)
with ‹n -as'→* sourcenode a'› have "n -as'→⇩√* sourcenode a'" by(simp add:vp_def)
with ‹as = as'@[a']› ‹valid_edge a'› ‹n' = targetnode a'›
show "∃as' a'. as = as'@[a'] ∧ n -as'→⇩√* sourcenode a' ∧ valid_edge a' ∧
n' = targetnode a'"
by blast
qed
lemma vp_split:
assumes "n -as@a#as'→⇩√* n'"
shows "n -as→⇩√* sourcenode a" and "valid_edge a" and "targetnode a -as'→⇩√* n'"
proof -
from ‹n -as@a#as'→⇩√* n'› have "n -as→* sourcenode a" and "valid_edge a"
and "targetnode a -as'→* n'"
by(auto intro:path_split simp:vp_def)
from ‹n -as@a#as'→⇩√* n'› have "valid_path (as@a#as')" by(simp add:vp_def)
hence "valid_path as" and "valid_path (a#as')" by(auto intro:valid_path_split)
from ‹valid_path (a#as')› have "valid_path ([a]@as')" by simp
hence "valid_path as'" by(rule valid_path_split)
with ‹n -as→* sourcenode a› ‹valid_path as› ‹valid_edge a› ‹targetnode a -as'→* n'›
show "n -as→⇩√* sourcenode a" "valid_edge a" "targetnode a -as'→⇩√* n'"
by(auto simp:vp_def)
qed
lemma vp_split_second:
assumes "n -as@a#as'→⇩√* n'" shows "sourcenode a -a#as'→⇩√* n'"
proof -
from ‹n -as@a#as'→⇩√* n'› have "sourcenode a -a#as'→* n'"
by(fastforce elim:path_split_second simp:vp_def)
from ‹n -as@a#as'→⇩√* n'› have "valid_path (as@a#as')" by(simp add:vp_def)
hence "valid_path (a#as')" by(rule valid_path_split)
with ‹sourcenode a -a#as'→* n'› show ?thesis by(simp add:vp_def)
qed
function valid_path_rev_aux :: "'edge list ⇒ 'edge list ⇒ bool"
where "valid_path_rev_aux cs [] ⟷ True"
| "valid_path_rev_aux cs (as@[a]) ⟷
(case (kind a) of Q↩⇘p⇙f ⇒ valid_path_rev_aux (a#cs) as
| Q:r↪⇘p⇙fs ⇒ case cs of [] ⇒ valid_path_rev_aux [] as
| c'#cs' ⇒ c' ∈ get_return_edges a ∧
valid_path_rev_aux cs' as
| _ ⇒ valid_path_rev_aux cs as)"
by auto(case_tac b rule:rev_cases,auto)
termination by lexicographic_order
lemma vpra_induct [consumes 1,case_names vpra_empty vpra_intra vpra_Return
vpra_CallEmpty vpra_CallCons]:
assumes major: "valid_path_rev_aux xs ys"
and rules: "⋀cs. P cs []"
"⋀cs a as. ⟦intra_kind(kind a); valid_path_rev_aux cs as; P cs as⟧
⟹ P cs (as@[a])"
"⋀cs a as Q p f. ⟦kind a = Q↩⇘p⇙f; valid_path_rev_aux (a#cs) as; P (a#cs) as⟧
⟹ P cs (as@[a])"
"⋀cs a as Q r p fs. ⟦kind a = Q:r↪⇘p⇙fs; cs = []; valid_path_rev_aux [] as;
P [] as⟧ ⟹ P cs (as@[a])"
"⋀cs a as Q r p fs c' cs'. ⟦kind a = Q:r↪⇘p⇙fs; cs = c'#cs';
valid_path_rev_aux cs' as; c' ∈ get_return_edges a; P cs' as⟧
⟹ P cs (as@[a])"
shows "P xs ys"
using major
apply(induct ys arbitrary:xs rule:rev_induct)
by(auto intro:rules split:edge_kind.split_asm list.split_asm simp:intra_kind_def)
lemma vpra_callstack_prefix:
"valid_path_rev_aux (cs@cs') as ⟹ valid_path_rev_aux cs as"
proof(induct "cs@cs'" as arbitrary:cs cs' rule:vpra_induct)
case vpra_empty thus ?case by simp
next
case (vpra_intra a as)
hence "valid_path_rev_aux cs as" by simp
with ‹intra_kind (kind a)› show ?case by(fastforce simp:intra_kind_def)
next
case (vpra_Return a as Q p f)
note IH = ‹⋀ds ds'. a#cs@cs' = ds@ds' ⟹ valid_path_rev_aux ds as›
have "a#cs@cs' = (a#cs)@cs'" by simp
from IH[OF this] have "valid_path_rev_aux (a#cs) as" .
with ‹kind a = Q↩⇘p⇙f› show ?case by simp
next
case (vpra_CallEmpty a as Q r p fs)
hence "valid_path_rev_aux cs as" by simp
with ‹kind a = Q:r↪⇘p⇙fs› ‹cs@cs' = []› show ?case by simp
next
case (vpra_CallCons a as Q r p fs c' csx)
note IH = ‹⋀cs cs'. csx = cs@cs' ⟹ valid_path_rev_aux cs as›
from ‹cs@cs' = c'#csx›
have "(cs = [] ∧ cs' = c'#csx) ∨ (∃zs. cs = c'#zs ∧ zs@cs' = csx)"
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↪⇘p⇙fs› show ?thesis by simp
next
assume "∃zs. cs = c'#zs ∧ zs@cs' = csx"
then obtain zs where "cs = c'#zs" and "csx = zs@cs'" by auto
from IH[OF ‹csx = zs@cs'›] have "valid_path_rev_aux zs as" .
with ‹cs = c'#zs› ‹kind a = Q:r↪⇘p⇙fs› ‹c' ∈ get_return_edges a› show ?thesis by simp
qed
qed
function upd_rev_cs :: "'edge list ⇒ 'edge list ⇒ 'edge list"
where "upd_rev_cs cs [] = cs"
| "upd_rev_cs cs (as@[a]) =
(case (kind a) of Q↩⇘p⇙f ⇒ upd_rev_cs (a#cs) as
| Q:r↪⇘p⇙fs ⇒ case cs of [] ⇒ upd_rev_cs cs as
| c'#cs' ⇒ upd_rev_cs cs' as
| _ ⇒ upd_rev_cs cs as)"
by auto(case_tac b rule:rev_cases,auto)
termination by lexicographic_order
lemma upd_rev_cs_empty [dest]:
"upd_rev_cs cs [] = [] ⟹ cs = []"
by(cases cs) auto
lemma valid_path_rev_aux_split:
assumes "valid_path_rev_aux cs (as@as')"
shows "valid_path_rev_aux cs as'" and "valid_path_rev_aux (upd_rev_cs cs as') as"
using ‹valid_path_rev_aux cs (as@as')›
proof(induct cs "as@as'" arbitrary:as as' rule:vpra_induct)
case (vpra_intra cs a as as'')
note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux cs ys›
note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux (upd_rev_cs cs ys) xs›
{ case 1
from vpra_intra
have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')"
by(cases as' rule:rev_cases) auto
thus ?case
proof
assume "as' = [] ∧ as@[a] = as''"
thus ?thesis by simp
next
assume "∃xs. as = as''@xs ∧ xs@[a] = as'"
then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
from IH1[OF ‹as = as''@xs›] have "valid_path_rev_aux cs xs" .
with ‹xs@[a] = as'› ‹intra_kind (kind a)›
show ?thesis by(fastforce simp:intra_kind_def)
qed
next
case 2
from vpra_intra
have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')"
by(cases as' rule:rev_cases) auto
thus ?case
proof
assume "as' = [] ∧ as@[a] = as''"
hence "as = butlast as''@[]" by(cases as) auto
from IH2[OF this] have "valid_path_rev_aux (upd_rev_cs cs []) (butlast as'')" .
with ‹as' = [] ∧ as@[a] = as''› ‹intra_kind (kind a)›
show ?thesis by(fastforce simp:intra_kind_def)
next
assume "∃xs. as = as''@xs ∧ xs@[a] = as'"
then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
from IH2[OF ‹as = as''@xs›] have "valid_path_rev_aux (upd_rev_cs cs xs) as''" .
from ‹xs@[a] = as'› ‹intra_kind (kind a)›
have "upd_rev_cs cs xs = upd_rev_cs cs as'" by(fastforce simp:intra_kind_def)
with ‹valid_path_rev_aux (upd_rev_cs cs xs) as''›
show ?thesis by simp
qed
}
next
case (vpra_Return cs a as Q p f as'')
note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux (a#cs) ys›
note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux (upd_rev_cs (a#cs) ys) xs›
{ case 1
from vpra_Return
have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')"
by(cases as' rule:rev_cases) auto
thus ?case
proof
assume "as' = [] ∧ as@[a] = as''"
thus ?thesis by simp
next
assume "∃xs. as = as''@xs ∧ xs@[a] = as'"
then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
from IH1[OF ‹as = as''@xs›] have "valid_path_rev_aux (a#cs) xs" .
with ‹xs@[a] = as'› ‹kind a = Q↩⇘p⇙f›
show ?thesis by fastforce
qed
next
case 2
from vpra_Return
have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')"
by(cases as' rule:rev_cases) auto
thus ?case
proof
assume "as' = [] ∧ as@[a] = as''"
hence "as = butlast as''@[]" by(cases as) auto
from IH2[OF this]
have "valid_path_rev_aux (upd_rev_cs (a#cs) []) (butlast as'')" .
with ‹as' = [] ∧ as@[a] = as''› ‹kind a = Q↩⇘p⇙f›
show ?thesis by fastforce
next
assume "∃xs. as = as''@xs ∧ xs@[a] = as'"
then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
from IH2[OF ‹as = as''@xs›]
have "valid_path_rev_aux (upd_rev_cs (a#cs) xs) as''" .
from ‹xs@[a] = as'› ‹kind a = Q↩⇘p⇙f›
have "upd_rev_cs (a#cs) xs = upd_rev_cs cs as'" by fastforce
with ‹valid_path_rev_aux (upd_rev_cs (a#cs) xs) as''›
show ?thesis by simp
qed
}
next
case (vpra_CallEmpty cs a as Q r p fs as'')
note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux [] ys›
note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux (upd_rev_cs [] ys) xs›
{ case 1
from vpra_CallEmpty
have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')"
by(cases as' rule:rev_cases) auto
thus ?case
proof
assume "as' = [] ∧ as@[a] = as''"
thus ?thesis by simp
next
assume "∃xs. as = as''@xs ∧ xs@[a] = as'"
then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
from IH1[OF ‹as = as''@xs›] have "valid_path_rev_aux [] xs" .
with ‹xs@[a] = as'› ‹kind a = Q:r↪⇘p⇙fs› ‹cs = []›
show ?thesis by fastforce
qed
next
case 2
from vpra_CallEmpty
have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')"
by(cases as' rule:rev_cases) auto
thus ?case
proof
assume "as' = [] ∧ as@[a] = as''"
hence "as = butlast as''@[]" by(cases as) auto
from IH2[OF this]
have "valid_path_rev_aux (upd_rev_cs [] []) (butlast as'')" .
with ‹as' = [] ∧ as@[a] = as''› ‹kind a = Q:r↪⇘p⇙fs› ‹cs = []›
show ?thesis by fastforce
next
assume "∃xs. as = as''@xs ∧ xs@[a] = as'"
then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
from IH2[OF ‹as = as''@xs›]
have "valid_path_rev_aux (upd_rev_cs [] xs) as''" .
with ‹xs@[a] = as'› ‹kind a = Q:r↪⇘p⇙fs› ‹cs = []›
show ?thesis by fastforce
qed
}
next
case (vpra_CallCons cs a as Q r p fs c' cs' as'')
note IH1 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux cs' ys›
note IH2 = ‹⋀xs ys. as = xs@ys ⟹ valid_path_rev_aux (upd_rev_cs cs' ys) xs›
{ case 1
from vpra_CallCons
have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')"
by(cases as' rule:rev_cases) auto
thus ?case
proof
assume "as' = [] ∧ as@[a] = as''"
thus ?thesis by simp
next
assume "∃xs. as = as''@xs ∧ xs@[a] = as'"
then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
from IH1[OF ‹as = as''@xs›] have "valid_path_rev_aux cs' xs" .
with ‹xs@[a] = as'› ‹kind a = Q:r↪⇘p⇙fs› ‹cs = c' # cs'› ‹c' ∈ get_return_edges a›
show ?thesis by fastforce
qed
next
case 2
from vpra_CallCons
have "as' = [] ∧ as@[a] = as'' ∨ (∃xs. as = as''@xs ∧ xs@[a] = as')"
by(cases as' rule:rev_cases) auto
thus ?case
proof
assume "as' = [] ∧ as@[a] = as''"
hence "as = butlast as''@[]" by(cases as) auto
from IH2[OF this]
have "valid_path_rev_aux (upd_rev_cs cs' []) (butlast as'')" .
with ‹as' = [] ∧ as@[a] = as''› ‹kind a = Q:r↪⇘p⇙fs› ‹cs = c' # cs'›
‹c' ∈ get_return_edges a› show ?thesis by fastforce
next
assume "∃xs. as = as''@xs ∧ xs@[a] = as'"
then obtain xs where "as = as''@xs" and "xs@[a] = as'" by auto
from IH2[OF ‹as = as''@xs›]
have "valid_path_rev_aux (upd_rev_cs cs' xs) as''" .
with ‹xs@[a] = as'› ‹kind a = Q:r↪⇘p⇙fs› ‹cs = c' # cs'›
‹c' ∈ get_return_edges a›
show ?thesis by fastforce
qed
}
qed simp_all
lemma valid_path_rev_aux_Append:
"⟦valid_path_rev_aux cs as'; valid_path_rev_aux (upd_rev_cs cs as') as⟧
⟹ valid_path_rev_aux cs (as@as')"
by(induct rule:vpra_induct,
auto simp:intra_kind_def simp del:append_assoc simp:append_assoc[THEN sym])
lemma vpra_Cons_intra:
assumes "intra_kind(kind a)"
shows "valid_path_rev_aux cs as ⟹ valid_path_rev_aux cs (a#as)"
proof(induct rule:vpra_induct)
case (vpra_empty cs)
have "valid_path_rev_aux cs []" by simp
with ‹intra_kind(kind a)› have "valid_path_rev_aux cs ([]@[a])"
by(simp only:valid_path_rev_aux.simps intra_kind_def,fastforce)
thus ?case by simp
qed(simp only:append_Cons[THEN sym] valid_path_rev_aux.simps intra_kind_def,fastforce)+
lemma vpra_Cons_Return:
assumes "kind a = Q↩⇘p⇙f"
shows "valid_path_rev_aux cs as ⟹ valid_path_rev_aux cs (a#as)"
proof(induct rule:vpra_induct)
case (vpra_empty cs)
from ‹kind a = Q↩⇘p⇙f› have "valid_path_rev_aux cs ([]@[a])"
by(simp only:valid_path_rev_aux.simps,clarsimp)
thus ?case by simp
next
case (vpra_intra cs a' as')
from ‹valid_path_rev_aux cs (a#as')› ‹intra_kind (kind a')›
have "valid_path_rev_aux cs ((a#as')@[a'])"
by(simp only:valid_path_rev_aux.simps,fastforce simp:intra_kind_def)
thus ?case by simp
next
case (vpra_Return cs a' as' Q' p' f')
from ‹valid_path_rev_aux (a'#cs) (a#as')› ‹kind a' = Q'↩⇘p'⇙f'›
have "valid_path_rev_aux cs ((a#as')@[a'])"
by(simp only:valid_path_rev_aux.simps,clarsimp)
thus ?case by simp
next
case (vpra_CallEmpty cs a' as' Q' r' p' fs')
from ‹valid_path_rev_aux [] (a#as')› ‹kind a' = Q':r'↪⇘p'⇙fs'› ‹cs = []›
have "valid_path_rev_aux cs ((a#as')@[a'])"
by(simp only:valid_path_rev_aux.simps,clarsimp)
thus ?case by simp
next
case (vpra_CallCons cs a' as' Q' r' p' fs' c' cs')
from ‹valid_path_rev_aux cs' (a#as')› ‹kind a' = Q':r'↪⇘p'⇙fs'› ‹cs = c'#cs'›
‹c' ∈ get_return_edges a'›
have "valid_path_rev_aux cs ((a#as')@[a'])"
by(simp only:valid_path_rev_aux.simps,clarsimp)
thus ?case by simp
qed
lemmas append_Cons_rev = append_Cons[THEN sym]
declare append_Cons [simp del] append_Cons_rev [simp]
lemma upd_rev_cs_Cons_intra:
assumes "intra_kind(kind a)" shows "upd_rev_cs cs (a#as) = upd_rev_cs cs as"
proof(induct as arbitrary:cs rule:rev_induct)
case Nil
from ‹intra_kind (kind a)›
have "upd_rev_cs cs ([]@[a]) = upd_rev_cs cs []"
by(simp only:upd_rev_cs.simps,auto simp:intra_kind_def)
thus ?case by simp
next
case (snoc a' as')
note IH = ‹⋀cs. upd_rev_cs cs (a#as') = upd_rev_cs cs as'›
show ?case
proof(cases "kind a'" rule:edge_kind_cases)
case Intra
from IH have "upd_rev_cs cs (a#as') = upd_rev_cs cs as'" .
with Intra have "upd_rev_cs cs ((a#as')@[a']) = upd_rev_cs cs (as'@[a'])"
by(fastforce simp:intra_kind_def)
thus ?thesis by simp
next
case Return
from IH have "upd_rev_cs (a'#cs) (a#as') = upd_rev_cs (a'#cs) as'" .