# Theory AuxLemmas

section ‹Auxiliary lemmas›

theory AuxLemmas imports Main begin

abbreviation "arbitrary == undefined"

text ‹Lemmas about left- and rightmost elements in lists›

lemma leftmost_element_property:
assumes "∃x ∈ set xs. P x"
obtains zs x' ys where "xs = zs@x'#ys" and "P x'" and "∀z ∈ set zs. ¬ P z"
proof(atomize_elim)
from ‹∃x ∈ set xs. P x›
show "∃zs x' ys. xs = zs @ x' # ys ∧ P x' ∧ (∀z∈set zs. ¬ P z)"
proof(induct xs)
case Nil thus ?case by simp
next
case (Cons x' xs')
note IH = ‹∃a∈set xs'. P a
⟹ ∃zs x' ys. xs' = zs@x'#ys ∧ P x' ∧ (∀z∈set zs. ¬ P z)›
show ?case
proof (cases "P x'")
case True
then have "(∃ys. x' # xs' = [] @ x' # ys) ∧ P x' ∧ (∀x∈set []. ¬ P x)" by simp
then show ?thesis by blast
next
case False
with ‹∃y∈set (x'#xs'). P y› have "∃y∈set xs'. P y" by simp
from IH[OF this] obtain y ys zs where "xs' = zs@y#ys"
and "P y" and "∀z∈set zs. ¬ P z" by blast
from ‹∀z∈set zs. ¬ P z› False have "∀z∈set (x'#zs). ¬ P z" by simp
with ‹xs' = zs@y#ys› ‹P y› show ?thesis by (metis Cons_eq_append_conv)
qed
qed
qed

lemma rightmost_element_property:
assumes "∃x ∈ set xs. P x"
obtains ys x' zs where "xs = ys@x'#zs" and "P x'" and "∀z ∈ set zs. ¬ P z"
proof(atomize_elim)
from ‹∃x ∈ set xs. P x›
show "∃ys x' zs. xs = ys @ x' # zs ∧ P x' ∧ (∀z∈set zs. ¬ P z)"
proof(induct xs)
case Nil thus ?case by simp
next
case (Cons x' xs')
note IH = ‹∃a∈set xs'. P a
⟹ ∃ys x' zs. xs' = ys @ x' # zs ∧ P x' ∧ (∀z∈set zs. ¬ P z)›
show ?case
proof(cases "∃y∈set xs'. P y")
case True
from IH[OF this] obtain y ys zs where "xs' = ys @ y # zs"
and "P y" and "∀z∈set zs. ¬ P z" by blast
thus ?thesis by (metis Cons_eq_append_conv)
next
case False
with ‹∃y∈set (x'#xs'). P y› have "P x'" by simp
with False show ?thesis by (metis eq_Nil_appendI)
qed
qed
qed

text ‹Lemma concerning maps and ‹@››

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

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

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

end


# Theory BasicDefs

chapter ‹The Framework›

theory BasicDefs imports AuxLemmas begin

text ‹
As slicing is a program analysis that can be completely based on the
information given in the CFG, we want to provide a framework which
allows us to formalize and prove properties of slicing regardless of
the actual programming language. So the starting point for the formalization
is the definition of an abstract CFG, i.e.\ without considering features
specific for certain languages. By doing so we ensure that our framework
is as generic as possible since all proofs hold for every language whose
CFG conforms to this abstract CFG.  This abstract CFG can be used as a
basis for static intraprocedural slicing as well as for dynamic slicing,
if in the dynamic case all method calls are inlined (i.e., abstract CFG
paths conform to traces).
›

section ‹Basic Definitions›

subsection‹Edge kinds›

datatype 'state edge_kind = Update "'state ⇒ 'state"           ("⇑_")
| Predicate "'state ⇒ bool"      ("'(_')⇩√")

subsection ‹Transfer and predicate functions›

fun transfer :: "'state edge_kind ⇒ 'state ⇒ 'state"
where "transfer (⇑f) s = f s"
| "transfer (P)⇩√ s   = s"

fun transfers :: "'state edge_kind list ⇒ 'state ⇒ 'state"
where "transfers [] s   = s"
| "transfers (e#es) s = transfers es (transfer e s)"

fun pred :: "'state edge_kind ⇒ 'state ⇒ bool"
where "pred (⇑f) s = True"
| "pred (P)⇩√ s   = (P s)"

fun preds :: "'state edge_kind list ⇒ 'state ⇒ bool"
where "preds [] s   = True"
| "preds (e#es) s = (pred e s ∧ preds es (transfer e 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

lemma transfers_id_no_influence:
"transfers [et ← ets. et ≠ ⇑id] s = transfers ets s"
by(induct ets arbitrary:s,auto)

lemma preds_True_no_influence:
"preds [et ← ets. et ≠ (λs. True)⇩√] s = preds ets s"
by(induct ets arbitrary:s,auto)

end


# Theory CFG

section ‹CFG›

theory CFG imports BasicDefs begin

subsection ‹The abstract CFG›

locale CFG =
fixes sourcenode :: "'edge ⇒ 'node"
fixes targetnode :: "'edge ⇒ 'node"
fixes kind :: "'edge ⇒ 'state edge_kind"
fixes valid_edge :: "'edge ⇒ bool"
fixes Entry::"'node" ("'('_Entry'_')")
assumes Entry_target [dest]: "⟦valid_edge a; targetnode a = (_Entry_)⟧ ⟹ False"
and edge_det:
"⟦valid_edge a; valid_edge a'; sourcenode a = sourcenode a';
targetnode a = targetnode a'⟧ ⟹ a = a'"

begin

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 and lemmas›

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_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 ‹targetnode a = n''› ‹valid_edge a› ‹n'' = (_Entry_)› have False
by -(rule Entry_target,simp_all)
{ case 1
with ‹False› show ?case ..
next
case 2
with ‹False› show ?case ..
}
qed simp_all

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 -
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'› that show ?thesis
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 -
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'› that show ?thesis
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 -
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)
with that show ?thesis 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 ⇒ 'state edge_kind list"
where "kinds xs ≡ map kind xs"

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

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

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

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

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

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
next
case (empty_path n) case 2
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
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›
next
case 2
with ‹(_Entry_) ∉ set (sourcenodes(tl(a#as)))› ‹sourcenode a = n›
}
qed

end

end


# Theory CFGExit

theory CFGExit imports CFG begin

subsection ‹Adds an exit node to the abstract CFG›

locale CFGExit = CFG sourcenode targetnode kind valid_edge Entry
for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
and kind :: "'edge ⇒ 'state edge_kind" and valid_edge :: "'edge ⇒ bool"
and Entry :: "'node" ("'('_Entry'_')") +
fixes Exit::"'node"  ("'('_Exit'_')")
assumes Exit_source [dest]: "⟦valid_edge a; sourcenode a = (_Exit_)⟧ ⟹ False"
and Entry_Exit_edge: "∃a. valid_edge a ∧ sourcenode a = (_Entry_) ∧
targetnode a = (_Exit_) ∧ kind a = (λs. False)⇩√"

begin

lemma Entry_noteq_Exit [dest]:
assumes eq:"(_Entry_) = (_Exit_)" shows "False"
proof -
from Entry_Exit_edge obtain a where "sourcenode a = (_Entry_)"
and "valid_edge a" by blast
with eq show False by simp(erule Exit_source)
qed

lemma Exit_noteq_Entry [dest]:"(_Exit_) = (_Entry_) ⟹ False"
by(rule Entry_noteq_Exit[OF sym],simp)

lemma [simp]: "valid_node (_Entry_)"
proof -
from Entry_Exit_edge obtain a where "sourcenode a = (_Entry_)"
and "valid_edge a" by blast
thus ?thesis by(fastforce simp:valid_node_def)
qed

lemma [simp]: "valid_node (_Exit_)"
proof -
from Entry_Exit_edge obtain a where "targetnode a = (_Exit_)"
and "valid_edge a" by blast
thus ?thesis by(fastforce simp:valid_node_def)
qed

definition inner_node :: "'node ⇒ bool"
where inner_node_def:
"inner_node n ≡ valid_node n ∧ n ≠ (_Entry_) ∧ n ≠ (_Exit_)"

lemma inner_is_valid:
"inner_node n ⟹ valid_node n"

lemma [dest]:
"inner_node (_Entry_) ⟹ False"

lemma [dest]:
"inner_node (_Exit_) ⟹ False"

lemma [simp]:"⟦valid_edge a; targetnode a ≠ (_Exit_)⟧
⟹ inner_node (targetnode a)"

lemma [simp]:"⟦valid_edge a; sourcenode a ≠ (_Entry_)⟧
⟹ inner_node (sourcenode a)"

lemma valid_node_cases [consumes 1, case_names "Entry" "Exit" "inner"]:
"⟦valid_node n; n = (_Entry_) ⟹ Q; n = (_Exit_) ⟹ Q;
inner_node n ⟹ Q⟧ ⟹ Q"
apply(auto simp:valid_node_def)
apply(case_tac "sourcenode a = (_Entry_)") apply auto
apply(case_tac "targetnode a = (_Exit_)") apply auto
done

lemma path_Exit_source [dest]:
assumes "(_Exit_) -as→* n'" shows "n' = (_Exit_)" and "as = []"
using ‹(_Exit_) -as→* n'›
proof(induct n≡"(_Exit_)" as n' rule:path.induct)
case (Cons_path n'' as n' a)
from ‹sourcenode a = (_Exit_)› ‹valid_edge a› have False
by -(rule Exit_source,simp_all)
{ case 1 with ‹False› show ?case ..
next
case 2 with ‹False› show ?case ..
}
qed simp_all

lemma Exit_no_sourcenode[dest]:
assumes isin:"(_Exit_) ∈ set (sourcenodes as)" and path:"n -as→* n'"
shows False
proof -
from isin obtain ns' ns'' where "sourcenodes as = ns'@(_Exit_)#ns''"
by(auto dest:split_list simp:sourcenodes_def)
then obtain as' as'' a where "as = as'@a#as''"
and source:"sourcenode a = (_Exit_)"
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
with path have "valid_edge a" by(fastforce dest:path_split)
with source show ?thesis by -(erule Exit_source)
qed

end

end


# Theory Postdomination

section ‹Postdomination›

theory Postdomination imports CFGExit begin

subsection ‹Standard Postdomination›

locale Postdomination = CFGExit sourcenode targetnode kind valid_edge Entry Exit
for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
and kind :: "'edge ⇒ 'state edge_kind" and valid_edge :: "'edge ⇒ bool"
and Entry :: "'node" ("'('_Entry'_')") and Exit :: "'node" ("'('_Exit'_')") +
assumes Entry_path:"valid_node n ⟹ ∃as. (_Entry_) -as→* n"
and Exit_path:"valid_node n ⟹ ∃as. n -as→* (_Exit_)"

begin

definition postdominate :: "'node ⇒ 'node ⇒ bool" ("_ postdominates _" [51,0])
where postdominate_def:"n' postdominates n ≡
(valid_node n ∧ valid_node n' ∧
((∀as. n -as→* (_Exit_) ⟶ n' ∈ set (sourcenodes as))))"

lemma postdominate_implies_path:
assumes "n' postdominates n" obtains as where "n -as→* n'"
proof(atomize_elim)
from ‹n' postdominates n› have "valid_node n"
and all:"∀as. n -as→* (_Exit_) ⟶ n' ∈ set(sourcenodes as)"
by(auto simp:postdominate_def)
from ‹valid_node n› obtain as where "n -as→* (_Exit_)" by(auto dest:Exit_path)
with all have "n' ∈ set(sourcenodes as)" by simp
then obtain ns ns' where "sourcenodes as = ns@n'#ns'" by(auto dest:split_list)
then obtain as' a as'' where "sourcenodes as' = ns"
and "sourcenode a = n'" and "as = as'@a#as''"
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
from ‹n -as→* (_Exit_)› ‹as = as'@a#as''› have "n -as'→* sourcenode a"
by(fastforce dest:path_split)
with ‹sourcenode a = n'› show "∃as. n -as→* n'" by blast
qed

lemma postdominate_refl:
assumes valid:"valid_node n" and notExit:"n ≠ (_Exit_)"
shows "n postdominates n"
using valid
proof(induct rule:valid_node_cases)
case Entry
{ fix as assume path:"(_Entry_) -as→* (_Exit_)"
hence notempty:"as ≠ []"
apply - apply(erule path.cases)
by (drule sym,simp,drule Exit_noteq_Entry,auto)
with path have "hd (sourcenodes as) = (_Entry_)"
by(fastforce intro:path_sourcenode)
with notempty have "(_Entry_) ∈ set (sourcenodes as)"
by(fastforce intro:hd_in_set simp:sourcenodes_def) }
with Entry show ?thesis by(simp add:postdominate_def)
next
case Exit
with notExit have False by simp
thus ?thesis by simp
next
case inner
show ?thesis
proof(cases "∃as. n -as→* (_Exit_)")
case True
{ fix as' assume path':"n -as'→* (_Exit_)"
with inner have notempty:"as' ≠ []"
by(cases as',auto elim!:path.cases simp:inner_node_def)
with path' inner have hd:"hd (sourcenodes as') = n"
by -(rule path_sourcenode)
from notempty have "sourcenodes as' ≠ []" by(simp add:sourcenodes_def)
with hd[THEN sym] have "n ∈ set (sourcenodes as')" by simp }
hence "∀as. n -as→* (_Exit_) ⟶ n ∈ set (sourcenodes as)" by simp
with True inner show ?thesis by(simp add:postdominate_def inner_is_valid)
next
case False
with inner show ?thesis by(simp add:postdominate_def inner_is_valid)
qed
qed

lemma postdominate_trans:
assumes pd1:"n'' postdominates n" and pd2:"n' postdominates n''"
shows "n' postdominates n"
proof -
from pd1 pd2 have valid:"valid_node n" and valid':"valid_node n'"
{ fix as assume path:"n -as→* (_Exit_)"
with pd1 have "n'' ∈ set (sourcenodes as)" by(simp add:postdominate_def)
then obtain ns' ns'' where "sourcenodes as = ns'@n''#ns''"
by(auto dest:split_list)
then obtain as' as'' a
where as'':"sourcenodes as'' = ns''" and as:"as=as'@a#as''"
and source:"sourcenode a = n''"
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
from as path have "n -as'@a#as''→* (_Exit_)" by simp
with source have path':"n'' -a#as''→* (_Exit_)"
by(fastforce dest:path_split_second)
with pd2 have "n' ∈ set(sourcenodes (a#as''))"
by(auto simp:postdominate_def)
with as have "n' ∈ set(sourcenodes as)" by(auto simp:sourcenodes_def) }
with valid valid' show ?thesis by(simp add:postdominate_def)
qed

lemma postdominate_antisym:
assumes pd1:"n' postdominates n" and pd2:"n postdominates n'"
shows "n = n'"
proof -
from pd1 have valid:"valid_node n" and valid':"valid_node n'"
by(auto simp:postdominate_def)
from valid obtain as where path1:"n -as→* (_Exit_)" by(fastforce dest:Exit_path)
from valid' obtain as' where path2:"n' -as'→* (_Exit_)" by(fastforce dest:Exit_path)
from pd1 path1 have "∃nx ∈ set(sourcenodes as). nx = n'"
then obtain ns ns' where sources:"sourcenodes as = ns@n'#ns'"
and all:"∀nx ∈ set ns'. nx ≠ n'"
by(fastforce elim!: rightmost_element_property)
from sources obtain asx a asx' where ns':"ns' = sourcenodes asx'"
and as:"as = asx@a#asx'" and source:"sourcenode a = n'"
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
from path1 as have "n -asx@a#asx'→* (_Exit_)" by simp
with source have "n' -a#asx'→* (_Exit_)" by(fastforce dest:path_split_second)
with pd2 have "n ∈ set(sourcenodes (a#asx'))" by(simp add:postdominate_def)
with source have "n = n' ∨ n ∈ set(sourcenodes asx')" by(simp add:sourcenodes_def)
thus ?thesis
proof
assume "n = n'" thus ?thesis .
next
assume "n ∈ set(sourcenodes asx')"
then obtain nsx' nsx'' where "sourcenodes asx' = nsx'@n#nsx''"
by(auto dest:split_list)
then obtain asi asi' a' where asx':"asx' = asi@a'#asi'"
and source':"sourcenode a' = n"
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
with path1 as have "n -(asx@a#asi)@a'#asi'→* (_Exit_)" by simp
with source' have "n -a'#asi'→* (_Exit_)" by(fastforce dest:path_split_second)
with pd1 have "n' ∈ set(sourcenodes (a'#asi'))" by(auto simp:postdominate_def)
with source' have "n' = n ∨ n' ∈ set(sourcenodes asi')"
thus ?thesis
proof
assume "n' = n" thus ?thesis by(rule sym)
next
assume "n' ∈ set(sourcenodes asi')"
with asx' ns' have "n' ∈ set ns'" by(simp add:sourcenodes_def)
with all have False by blast
thus ?thesis by simp
qed
qed
qed

lemma postdominate_path_branch:
assumes "n -as→* n''" and "n' postdominates n''" and "¬ n' postdominates n"
obtains a as' as'' where "as = as'@a#as''" and "valid_edge a"
and "¬ n' postdominates (sourcenode a)" and "n' postdominates (targetnode a)"
proof(atomize_elim)
from assms
show "∃as' a as''. as = as'@a#as'' ∧ valid_edge a ∧
¬ n' postdominates (sourcenode a) ∧ n' postdominates (targetnode a)"
proof(induct rule:path.induct)
case (Cons_path n'' as nx a n)
note IH = ‹⟦n' postdominates nx; ¬ n' postdominates n''⟧
⟹ ∃as' a as''. as = as'@a#as'' ∧ valid_edge a ∧
¬ n' postdominates sourcenode a ∧ n' postdominates targetnode a›
show ?case
proof(cases "n' postdominates n''")
case True
with ‹¬ n' postdominates n› ‹sourcenode a = n› ‹targetnode a = n''›
‹valid_edge a›
show ?thesis by blast
next
case False
from IH[OF ‹n' postdominates nx› this] show ?thesis
by clarsimp(rule_tac x="a#as'" in exI,clarsimp)
qed
qed simp
qed

lemma Exit_no_postdominator:
"(_Exit_) postdominates n ⟹ False"
by(fastforce dest:Exit_path simp:postdominate_def)

lemma postdominate_path_targetnode:
assumes "n' postdominates n" and "n -as→* n''" and "n' ∉ set(sourcenodes as)"
shows "n' postdominates n''"
proof -
from ‹n' postdominates n› have "valid_node n" and "valid_node n'"
and all:"∀as''. n -as''→* (_Exit_) ⟶ n' ∈ set(sourcenodes as'')"
from ‹n -as→* n''› have "valid_node n''" by(fastforce dest:path_valid_node)
have "∀as''. n'' -as''→* (_Exit_) ⟶ n' ∈ set(sourcenodes as'')"
proof(rule ccontr)
assume "¬ (∀as''. n'' -as''→* (_Exit_) ⟶ n' ∈ set (sourcenodes as''))"
then obtain as'' where "n'' -as''→* (_Exit_)"
and "n' ∉ set (sourcenodes as'')" by blast
from ‹n -as→* n''› ‹n'' -as''→* (_Exit_)› have "n -as@as''→* (_Exit_)"
by(rule path_Append)
with ‹n' ∉ set(sourcenodes as)› ‹n' ∉ set (sourcenodes as'')›
have "n' ∉ set (sourcenodes (as@as''))"
with ‹n -as@as''→* (_Exit_)› ‹n' postdominates n› show False
qed
with ‹valid_node n'› ‹valid_node n''› show ?thesis by(simp add:postdominate_def)
qed

lemma not_postdominate_source_not_postdominate_target:
assumes "¬ n postdominates (sourcenode a)" and "valid_node n" and "valid_edge a"
obtains ax where "sourcenode a = sourcenode ax" and "valid_edge ax"
and "¬ n postdominates targetnode ax"
proof(atomize_elim)
show "∃ax. sourcenode a = sourcenode ax ∧ valid_edge ax ∧
¬ n postdominates targetnode ax"
proof -
from assms obtain asx
where "sourcenode a -asx→* (_Exit_)"
and "n ∉ set(sourcenodes asx)" by(auto simp:postdominate_def)
from ‹sourcenode a -asx→* (_Exit_)› ‹valid_edge a›
obtain ax asx' where [simp]:"asx = ax#asx'"
apply - apply(erule path.cases)
apply(drule_tac s="(_Exit_)" in sym)
apply simp
apply(drule Exit_source)
by simp_all
with ‹sourcenode a -asx→* (_Exit_)› have "sourcenode a -[]@ax#asx'→* (_Exit_)"
by simp
hence "valid_edge ax" and "sourcenode a = sourcenode ax"
and "targetnode ax -asx'→* (_Exit_)"
by(fastforce dest:path_split)+
with ‹n ∉ set(sourcenodes asx)› have "¬ n postdominates targetnode ax"
by(fastforce simp:postdominate_def sourcenodes_def)
with ‹sourcenode a = sourcenode ax› ‹valid_edge ax› show ?thesis by blast
qed
qed

lemma inner_node_Entry_edge:
assumes "inner_node n"
obtains a where "valid_edge a" and "inner_node (targetnode a)"
and "sourcenode a = (_Entry_)"
proof(atomize_elim)
from ‹inner_node n› have "valid_node n" by(rule inner_is_valid)
then obtain as where "(_Entry_) -as→* n" by(fastforce dest:Entry_path)
show "∃a. valid_edge a ∧ inner_node (targetnode a) ∧ sourcenode a = (_Entry_)"
proof(cases "as = []")
case True
with ‹inner_node n› ‹(_Entry_) -as→* n› have False
by(fastforce simp:inner_node_def)
thus ?thesis by simp
next
case False
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)
from ‹valid_edge a'› have "valid_node (targetnode a')" by simp
thus ?thesis
proof(cases "targetnode a'" rule:valid_node_cases)
case Entry
from ‹valid_edge a'› this have False by(rule Entry_target)
thus ?thesis by simp
next
case Exit
with ‹targetnode a' -as'→* n› ‹inner_node n›
have False by simp (drule path_Exit_source,auto simp:inner_node_def)
thus ?thesis by simp
next
case inner
with ‹valid_edge a'› ‹(_Entry_) = sourcenode a'› show ?thesis by simp blast
qed
qed
qed

lemma inner_node_Exit_edge:
assumes "inner_node n"
obtains a where "valid_edge a" and "inner_node (sourcenode a)"
and "targetnode a = (_Exit_)"
proof(atomize_elim)
from ‹inner_node n› have "valid_node n" by(rule inner_is_valid)
then obtain as where "n -as→* (_Exit_)" by(fastforce dest:Exit_path)
show "∃a. valid_edge a ∧ inner_node (sourcenode a) ∧ targetnode a = (_Exit_)"
proof(cases "as = []")
case True
with ‹inner_node n› ‹n -as→* (_Exit_)› have False by fastforce
thus ?thesis by simp
next
case False
with ‹n -as→* (_Exit_)› obtain a' as' where "as = as'@[a']"
and "n -as'→* sourcenode a'" and "valid_edge a'"
and "(_Exit_) = targetnode a'" by -(erule path_split_snoc)
from ‹valid_edge a'› have "valid_node (sourcenode a')" by simp
thus ?thesis
proof(cases "sourcenode a'" rule:valid_node_cases)
case Entry
with ‹n -as'→* sourcenode a'› ‹inner_node n›
have False by simp (drule path_Entry_target,auto simp:inner_node_def)
thus ?thesis by simp
next
case Exit
from ‹valid_edge a'› this have False by(rule Exit_source)
thus ?thesis by simp
next
case inner
with ‹valid_edge a'› ‹(_Exit_) = targetnode a'› show ?thesis by simp blast
qed
qed
qed

end

subsection ‹Strong Postdomination›

locale StrongPostdomination =
Postdomination sourcenode targetnode kind valid_edge Entry Exit
for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
and kind :: "'edge ⇒ 'state edge_kind" and valid_edge :: "'edge ⇒ bool"
and Entry :: "'node" ("'('_Entry'_')") and Exit :: "'node" ("'('_Exit'_')") +
assumes successor_set_finite: "valid_node n ⟹
finite {n'. ∃a'. valid_edge a' ∧ sourcenode a' = n ∧ targetnode a' = n'}"

begin

definition  strong_postdominate :: "'node ⇒ 'node ⇒ bool"
("_ strongly-postdominates _" [51,0])
where strong_postdominate_def:"n' strongly-postdominates n ≡
(n' postdominates n ∧
(∃k ≥ 1. ∀as nx. n -as→* nx ∧
length as ≥ k ⟶ n' ∈ set(sourcenodes as)))"

lemma strong_postdominate_prop_smaller_path:
assumes all:"∀as nx. n -as→* nx ∧ length as ≥ k ⟶ n' ∈ set(sourcenodes as)"
and "n -as→* n''" and "length as ≥ k"
obtains as' as'' where "n -as'→* n'" and "length as' < k" and "n' -as''→* n''"
and "as = as'@as''"
proof(atomize_elim)
show "∃as' as''. n -as'→* n' ∧ length as' < k ∧ n' -as''→* n'' ∧ as = as'@as''"
proof(rule ccontr)
assume "¬ (∃as' as''. n -as'→* n' ∧ length as' < k ∧ n' -as''→* n'' ∧
as = as'@as'')"
hence all':"∀as' as''. n -as'→* n' ∧ n' -as''→* n'' ∧ as = as'@as''
⟶ length as' ≥ k" by fastforce
from all ‹n -as→* n''› ‹length as ≥ k› have "∃nx ∈ set(sourcenodes as). nx = n'"
by fastforce
then obtain ns ns' where "sourcenodes as = ns@n'#ns'"
and "∀nx ∈ set ns. nx ≠ n'"
by(fastforce elim!:split_list_first_propE)
then obtain asx a asx' where [simp]:"ns = sourcenodes asx"
and [simp]:"as = asx@a#asx'" and "sourcenode a = n'"
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
from ‹n -as→* n''› have "n -asx@a#asx'→* n''" by simp
with ‹sourcenode a = n'› have "n -asx→* n'" and "valid_edge a"
and "targetnode a -asx'→* n''" by(fastforce dest:path_split)+
with ‹sourcenode a = n'› have "n' -a#asx'→* n''" by(fastforce intro:Cons_path)
with ‹n -asx→* n'› all' have "length asx ≥ k" by simp
with ‹n -asx→* n'› all have "n' ∈ set(sourcenodes asx)" by fastforce
with ‹∀nx ∈ set ns. nx ≠ n'› show False by fastforce
qed
qed

lemma strong_postdominate_refl:
assumes "valid_node n" and "n ≠ (_Exit_)"
shows "n strongly-postdominates n"
proof -
from assms have "n postdominates n" by(rule postdominate_refl)
{ fix as nx assume "n -as→* nx" and "length as ≥ 1"
then obtain a' as' where [simp]:"as = a'#as'" by(cases as) auto
with ‹n -as→* nx› have "n -[]@a'#as'→* nx" by simp
hence "n = sourcenode a'" by(fastforce dest:path_split)
hence "n ∈ set(sourcenodes as)" by(simp add:sourcenodes_def) }
hence "∀as nx. n -as→* nx ∧ length as ≥ 1 ⟶ n ∈ set(sourcenodes as)"
by auto
hence "∃k ≥ 1. ∀as nx. n -as→* nx ∧ length as ≥ k ⟶ n ∈ set(sourcenodes as)"
by blast
with ‹n postdominates n› show ?thesis by(simp add:strong_postdominate_def)
qed

lemma strong_postdominate_trans:
assumes "n'' strongly-postdominates n" and "n' strongly-postdominates n''"
shows "n' strongly-postdominates n"
proof -
from ‹n'' strongly-postdominates n› have "n'' postdominates n"
and paths1:"∃k ≥ 1. ∀as nx. n -as→* nx ∧ length as ≥ k
⟶ n'' ∈ set(sourcenodes as)"
by(auto simp only:strong_postdominate_def)
from paths1 obtain k1
where all1:"∀as nx. n -as→* nx ∧ length as ≥ k1 ⟶ n'' ∈ set(sourcenodes as)"
and "k1 ≥ 1" by blast
from ‹n' strongly-postdominates n''› have "n' postdominates n''"
and paths2:"∃k ≥ 1. ∀as nx. n'' -as→* nx ∧ length as ≥ k
⟶ n' ∈ set(sourcenodes as)"
by(auto simp only:strong_postdominate_def)
from paths2 obtain k2
where all2:"∀as nx. n'' -as→* nx ∧ length as ≥ k2 ⟶ n' ∈ set(sourcenodes as)"
and "k2 ≥ 1" by blast
from ‹n'' postdominates n› ‹n' postdominates n''›
have "n' postdominates n" by(rule postdominate_trans)
{ fix as nx assume "n -as→* nx" and "length as ≥ k1 + k2"
hence "length as ≥ k1" by fastforce
with ‹n -as→* nx› all1 obtain asx asx' where "n -asx→* n''"
and "length asx < k1" and "n'' -asx'→* nx"
and [simp]:"as = asx@asx'" by -(erule strong_postdominate_prop_smaller_path)
with ‹length as ≥ k1 + k2› have "length asx' ≥ k2" by fastforce
with ‹n'' -asx'→* nx› all2 have "n' ∈ set(sourcenodes asx')" by fastforce
hence "n' ∈ set(sourcenodes as)" by(simp add:sourcenodes_def) }
with ‹k1 ≥ 1› ‹k2 ≥ 1› have "∃k ≥ 1. ∀as nx. n -as→* nx ∧ length as ≥ k
⟶ n' ∈ set(sourcenodes as)"
by(rule_tac x="k1 + k2" in exI,auto)
with ‹n' postdominates n› show ?thesis by(simp add:strong_postdominate_def)
qed

lemma strong_postdominate_antisym:
"⟦n' strongly-postdominates n; n strongly-postdominates n'⟧ ⟹ n = n'"
by(fastforce intro:postdominate_antisym simp:strong_postdominate_def)

lemma strong_postdominate_path_branch:
assumes "n -as→* n''" and "n' strongly-postdominates n''"
and "¬ n' strongly-postdominates n"
obtains a as' as'' where "as = as'@a#as''" and "valid_edge a"
and "¬ n' strongly-postdominates (sourcenode a)"
and "n' strongly-postdominates (targetnode a)"
proof(atomize_elim)
from assms
show "∃as' a as''. as = as'@a#as'' ∧ valid_edge a ∧
¬ n' strongly-postdominates (sourcenode a) ∧
n' strongly-postdominates (targetnode a)"
proof(induct rule:path.induct)
case (Cons_path n'' as nx a n)
note IH = ‹⟦n' strongly-postdominates nx; ¬ n' strongly-postdominates n''⟧
⟹ ∃as' a as''. as = as'@a#as'' ∧ valid_edge a ∧
¬ n' strongly-postdominates sourcenode a ∧
n' strongly-postdominates targetnode a›
show ?case
proof(cases "n' strongly-postdominates n''")
case True
with ‹¬ n' strongly-postdominates n› ‹sourcenode a = n› ‹targetnode a = n''›
‹valid_edge a›
show ?thesis by blast
next
case False
from IH[OF ‹n' strongly-postdominates nx› this] show ?thesis
by clarsimp(rule_tac x="a#as'" in exI,clarsimp)
qed
qed simp
qed

lemma Exit_no_strong_postdominator:
"⟦(_Exit_) strongly-postdominates n; n -as→* (_Exit_)⟧ ⟹ False"
by(fastforce intro:Exit_no_postdominator path_valid_node simp:strong_postdominate_def)

lemma strong_postdominate_path_targetnode:
assumes "n' strongly-postdominates n" and "n -as→* n''"
and "n' ∉ set(sourcenodes as)"
shows "n' strongly-postdominates n''"
proof -
from ‹n' strongly-postdominates n› have "n' postdominates n"
and "∃k ≥ 1. ∀as nx. n -as→* nx ∧ length as ≥ k
⟶ n' ∈ set(sourcenodes as)"
by(auto simp only:strong_postdominate_def)
then obtain k where "k ≥ 1"
and paths:"∀as nx. n -as→* nx ∧ length as ≥ k
⟶ n' ∈ set(sourcenodes as)" by auto
from ‹n' postdominates n› ‹n -as→* n''› ‹n' ∉ set(sourcenodes as)›
have "n' postdominates n''"
by(rule postdominate_path_targetnode)
{ fix as' nx assume "n'' -as'→* nx" and "length as' ≥ k"
with ‹n -as→* n''› have "n -as@as'→* nx" and "length (as@as') ≥ k"
by(auto intro:path_Append)
with paths have "n' ∈ set(sourcenodes (as@as'))" by fastforce
with ‹n' ∉ set(sourcenodes as)› have "n' ∈ set(sourcenodes as')"
by(fastforce simp:sourcenodes_def) }
with ‹k ≥ 1› have "∃k ≥ 1. ∀as' nx. n'' -as'→* nx ∧ length as' ≥ k
⟶ n' ∈ set(sourcenodes as')" by auto
with ‹n' postdominates n''› show ?thesis by(simp add:strong_postdominate_def)
qed

lemma not_strong_postdominate_successor_set:
assumes "¬ n strongly-postdominates (sourcenode a)" and "valid_node n"
and "valid_edge a"
and all:"∀nx ∈ N. ∃a'. valid_edge a' ∧ sourcenode a' = sourcenode a ∧
targetnode a' = nx ∧ n strongly-postdominates nx"
obtains a' where "valid_edge a'" and "sourcenode a' =  sourcenode a"
and "targetnode a' ∉ N"
proof(atomize_elim)
show "∃a'. valid_edge a' ∧ sourcenode a' =  sourcenode a ∧ targetnode a' ∉ N"
proof(cases "n postdominates (sourcenode a)")
case False
with ‹valid_edge a› ‹valid_node n›
obtain a' where [simp]:"sourcenode a = sourcenode a'"
and "valid_edge a'" and "¬ n postdominates targetnode a'"
by -(erule not_postdominate_source_not_postdominate_target)
with all have "targetnode a' ∉ N" by(auto simp:strong_postdominate_def)
with ‹valid_edge a'› show ?thesis by simp blast
next
case True
let ?M = "{n'. ∃a'. valid_edge a' ∧ sourcenode a' =  sourcenode a ∧
targetnode a' = n'}"
let ?M' = "{n'. ∃a'. valid_edge a' ∧ sourcenode a' =  sourcenode a ∧
targetnode a' = n' ∧ n strongly-postdominates n'}"
let ?N' = "(λn'. SOME i. i ≥ 1 ∧
(∀as nx. n' -as→* nx ∧ length as ≥ i
⟶ n ∈ set(sourcenodes as)))  N"
obtain k where [simp]:"k = Max ?N'" by simp
have eq:"{x ∈ ?M. (λn'. n strongly-postdominates n') x} = ?M'" by auto
from ‹valid_edge a› have "finite ?M" by(simp add:successor_set_finite)
hence "finite {x ∈ ?M. (λn'. n strongly-postdominates n') x}" by fastforce
with eq have "finite ?M'" by simp
from all have "N ⊆ ?M'" by auto
with ‹finite ?M'› have "finite N" by(auto intro:finite_subset)
hence "finite ?N'" by fastforce
show ?thesis
proof(rule ccontr)
assume "¬ (∃a'. valid_edge a' ∧ sourcenode a' = sourcenode a ∧
targetnode a' ∉ N)"
hence allImp:"∀a'. valid_edge a' ∧ sourcenode a' = sourcenode a
⟶ targetnode a' ∈ N" by blast
from True ‹¬ n strongly-postdominates (sourcenode a)›
have allPaths:"∀k ≥ 1. ∃as nx. sourcenode a -as→* nx ∧ length as ≥ k
∧ n ∉ set(sourcenodes as)" by(auto simp:strong_postdominate_def)
then obtain as nx where "sourcenode a -as→* nx"
and "length as ≥ k + 1" and "n ∉ set(sourcenodes as)"
by (erule_tac x="k + 1" in allE) auto
then obtain ax as' where [simp]:"as = ax#as'" and "valid_edge ax"
and "sourcenode ax = sourcenode a" and "targetnode ax -as'→* nx"
by -(erule path.cases,auto)
with allImp have "targetnode ax ∈ N" by fastforce
with all have "n strongly-postdominates (targetnode ax)"
by auto
then obtain k' where k':"k' = (SOME i. i ≥ 1 ∧
(∀as nx. targetnode ax -as→* nx ∧ length as ≥ i
⟶ n ∈ set(sourcenodes as)))" by simp
with ‹n strongly-postdominates (targetnode ax)›
have "k' ≥ 1 ∧ (∀as nx. targetnode ax -as→* nx ∧ length as ≥ k'
⟶ n ∈ set(sourcenodes as))"
by(auto elim!:someI_ex simp:strong_postdominate_def)
hence "k' ≥ 1"
and spdAll:"∀as nx. targetnode ax -as→* nx ∧ length as ≥ k'
⟶ n ∈ set(sourcenodes as)"
by simp_all
from ‹targetnode ax ∈ N› k' have "k' ∈ ?N'" by blast
with ‹targetnode ax ∈ N› have "?N' ≠ {}" by auto
with ‹k' ∈ ?N'› have "k' ≤ Max ?N'" using ‹finite ?N'› by(fastforce intro:Max_ge)
hence "k' ≤ k" by simp
with ‹targetnode ax -as'→* nx› ‹length as ≥ k + 1› spdAll
have "n ∈ set(sourcenodes as')"
by fastforce
with ‹n ∉ set(sourcenodes as)› show False by(simp add:sourcenodes_def)
qed
qed
qed

lemma not_strong_postdominate_predecessor_successor:
assumes "¬ n strongly-postdominates (sourcenode a)"
and "valid_node n" and "valid_edge a"
obtains a' where "valid_edge a'" and "sourcenode a' = sourcenode a"
and "¬ n strongly-postdominates (targetnode a')"
proof(atomize_elim)
show "∃a'. valid_edge a' ∧ sourcenode a' = sourcenode a ∧
¬ n strongly-postdominates (targetnode a')"
proof(rule ccontr)
assume "¬ (∃a'. valid_edge a' ∧ sourcenode a' = sourcenode a ∧
¬ n strongly-postdominates targetnode a')"
hence all:"∀a'. valid_edge a' ∧ sourcenode a' = sourcenode a ⟶
n strongly-postdominates (targetnode a')" by auto
let ?N = "{n'. ∃a'. sourcenode a' =  sourcenode a ∧ valid_edge a' ∧
targetnode a' = n'}"
from all have "∀nx ∈ ?N. ∃a'. valid_edge a' ∧ sourcenode a' = sourcenode a ∧
targetnode a' = nx ∧ n strongly-postdominates nx"
by auto
with assms obtain a' where "valid_edge a'"
and "sourcenode a' =  sourcenode a" and "targetnode a' ∉ ?N"
by(erule not_strong_postdominate_successor_set)
thus False by auto
qed
qed

end

end


# Theory CFG_wf

section ‹CFG well-formedness›

theory CFG_wf imports CFG begin

subsection ‹Well-formedness of the abstract CFG›

locale CFG_wf = CFG sourcenode targetnode kind valid_edge Entry
for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
and kind :: "'edge ⇒ 'state edge_kind" and valid_edge :: "'edge ⇒ bool"
and Entry :: "'node" ("'('_Entry'_')") +
fixes Def::"'node ⇒ 'var set"
fixes Use::"'node ⇒ 'var set"
fixes state_val::"'state ⇒ 'var ⇒ 'val"
assumes Entry_empty:"Def (_Entry_) = {} ∧ Use (_Entry_) = {}"
and CFG_edge_no_Def_equal:
"⟦valid_edge a; V ∉ Def (sourcenode a); pred (kind a) s⟧
⟹ state_val (transfer (kind a) s) V = state_val s V"
and CFG_edge_transfer_uses_only_Use:
"⟦valid_edge a; ∀V ∈ Use (sourcenode a). state_val s V = state_val s' V;
pred (kind a) s; pred (kind a) s'⟧
⟹ ∀V ∈ Def (sourcenode a). state_val (transfer (kind a) s) V =
state_val (transfer (kind a) s') V"
and CFG_edge_Uses_pred_equal:
"⟦valid_edge a; pred (kind a) s;
∀V ∈ Use (sourcenode a). state_val s V = state_val s' V⟧
⟹ pred (kind a) s'"
and deterministic:"⟦valid_edge a; valid_edge a'; sourcenode a = sourcenode a';
targetnode a ≠ targetnode a'⟧
⟹ ∃Q Q'. kind a = (Q)⇩√ ∧ kind a' = (Q')⇩√ ∧
(∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))"

begin

lemma [dest!]: "V ∈ Use (_Entry_) ⟹ False"

lemma [dest!]: "V ∈ Def (_Entry_) ⟹ False"

lemma CFG_path_no_Def_equal:
"⟦n -as→* n'; ∀n ∈ set (sourcenodes as). V ∉ Def n; preds (kinds as) s⟧
⟹ state_val (transfers (kinds as) s) V = state_val s V"
proof(induct arbitrary:s rule:path.induct)
case (empty_path n)
next
case (Cons_path n'' as n' a n)
note IH = ‹⋀s. ⟦∀n∈set (sourcenodes as). V ∉ Def n; preds (kinds as) s⟧ ⟹
state_val (transfers (kinds as) s) V = state_val s V›
from ‹preds (kinds (a#as)) s› have "pred (kind a) s"
and "preds (kinds as) (transfer (kind a) s)" by(simp_all add:kinds_def)
from ‹∀n∈set (sourcenodes (a#as)). V ∉ Def n›
have noDef:"V ∉ Def (sourcenode a)"
and all:"∀n∈set (sourcenodes as). V ∉ Def n"
by(auto simp:sourcenodes_def)
from ‹valid_edge a› noDef ‹pred (kind a) s›
have "state_val (transfer (kind a) s) V = state_val s V"
by(rule CFG_edge_no_Def_equal)
with IH[OF all ‹preds (kinds as) (transfer (kind a) s)›] show ?case
qed

end

end


# Theory CFGExit_wf

theory CFGExit_wf imports CFGExit CFG_wf begin

subsection ‹New well-formedness lemmas using ‹(_Exit_)››

locale CFGExit_wf =
CFG_wf sourcenode targetnode kind valid_edge Entry Def Use state_val +
CFGExit sourcenode targetnode kind valid_edge Entry Exit
for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
and kind :: "'edge ⇒ 'state edge_kind" and valid_edge :: "'edge ⇒ bool"
and Entry :: "'node" ("'('_Entry'_')") and Def :: "'node ⇒ 'var set"
and Use :: "'node ⇒ 'var set" and state_val :: "'state ⇒ 'var ⇒ 'val"
and Exit :: "'node" ("'('_Exit'_')") +
assumes Exit_empty:"Def (_Exit_) = {} ∧ Use (_Exit_) = {}"

begin

lemma Exit_Use_empty [dest!]: "V ∈ Use (_Exit_) ⟹ False"

lemma Exit_Def_empty [dest!]: "V ∈ Def (_Exit_) ⟹ False"

end

end


# Theory SemanticsCFG

section ‹CFG and semantics conform›

theory SemanticsCFG imports CFG begin

locale CFG_semantics_wf = CFG sourcenode targetnode kind valid_edge Entry
for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
and kind :: "'edge ⇒ 'state edge_kind" and valid_edge :: "'edge ⇒ bool"
and Entry :: "'node" ("'('_Entry'_')") +
fixes sem::"'com ⇒ 'state ⇒ 'com ⇒ 'state ⇒ bool"
("((1⟨_,/_⟩) ⇒/ (1⟨_,/_⟩))" [0,0,0,0] 81)
fixes identifies::"'node ⇒ 'com ⇒ bool" ("_ ≜ _" [51,0] 80)
assumes fundamental_property:
"⟦n ≜ c; ⟨c,s⟩ ⇒ ⟨c',s'⟩⟧ ⟹
∃n' as. n -as→* n' ∧ transfers (kinds as) s = s' ∧ preds (kinds as) s ∧
n' ≜ c'"

end


section ‹Dynamic data dependence›

context CFG_wf begin

definition dyn_data_dependence ::
"'node ⇒ 'var ⇒ 'node ⇒ 'edge list ⇒ bool" ("_ influences _ in _ via _" [51,0,0])
where "n influences V in n' via as ≡
((V ∈ Def n) ∧ (V ∈ Use n') ∧ (n -as→* n') ∧
(∃a' as'. (as = a'#as') ∧ (∀n'' ∈ set (sourcenodes as'). V ∉ Def n'')))"

lemma dyn_influence_Cons_source:
"n influences V in n' via a#as ⟹ sourcenode a = n"

lemma dyn_influence_source_notin_tl_edges:
assumes "n influences V in n' via a#as"
shows "n ∉ set (sourcenodes as)"
proof(rule ccontr)
assume "¬ n ∉ set (sourcenodes as)"
hence "n ∈ set (sourcenodes as)" by simp
from ‹n influences V in n' via a#as› have "∀n'' ∈ set (sourcenodes as). V ∉ Def n''"
and "V ∈ Def n" by(simp_all add:dyn_data_dependence_def)
from ‹∀n'' ∈ set (sourcenodes as). V ∉ Def n''›
‹n ∈ set (sourcenodes as)› have "V ∉ Def n" by simp
with ‹V ∈ Def n› show False by simp
qed

lemma dyn_influence_only_first_edge:
assumes "n influences V in n' via a#as" and "preds (kinds (a#as)) s"
shows "state_val (transfers (kinds (a#as)) s) V =
state_val (transfer (kind a) s) V"
proof -
from ‹preds (kinds (a#as)) s› have "preds (kinds as) (transfer (kind a) s)"
from ‹n influences V in n' via a#as› have "n -a#as→* n'"
and "∀n'' ∈ set (sourcenodes as). V ∉ Def n''"
from ‹n -a#as→* n'› have "n = sourcenode a" and "targetnode a -as→* n'"
by(auto elim:path_split_Cons)
from ‹n influences V in n' via a#as› ‹n = sourcenode a›
have "sourcenode a ∉ set (sourcenodes as)"
by(fastforce intro!:dyn_influence_source_notin_tl_edges)
{ fix n'' assume "n'' ∈ set (sourcenodes as)"
with ‹sourcenode a ∉ set (sourcenodes as)› ‹n = sourcenode a›
have "n'' ≠ n" by(fastforce simp:sourcenodes_def)
with ‹∀n'' ∈ set (sourcenodes as). V ∉ Def n''› ‹n'' ∈ set (sourcenodes as)›
have "V ∉ Def n''" by(auto simp:sourcenodes_def) }
hence "∀n'' ∈ set (sourcenodes as). V ∉ Def n''" by simp
with ‹targetnode a -as→* n'› ‹preds (kinds as) (transfer (kind a) s)›
have "state_val (transfers (kinds as) (transfer (kind a) s)) V =
state_val (transfer (kind a) s) V"
by -(rule CFG_path_no_Def_equal)
thus ?thesis by(auto simp:kinds_def)
qed

end

end


# Theory DynStandardControlDependence

section ‹Dynamic Standard Control Dependence›

theory DynStandardControlDependence imports Postdomination begin

context Postdomination begin

definition
dyn_standard_control_dependence :: "'node ⇒ 'node ⇒ 'edge list ⇒ bool"
("_ controls⇩s _ via _" [51,0,0])
where dyn_standard_control_dependence_def:"n controls⇩s n' via as ≡
(∃a a' as'. (as = a#as') ∧ (n' ∉ set(sourcenodes as)) ∧ (n -as→* n') ∧
(n' postdominates (targetnode a)) ∧
(valid_edge a') ∧ (sourcenode a' = n) ∧
(¬ n' postdominates (targetnode a')))"

lemma Exit_not_dyn_standard_control_dependent:
assumes control:"n controls⇩s (_Exit_) via as" shows "False"
proof -
from control obtain a as' where path:"n -as→* (_Exit_)" and as:"as = a#as'"
and pd:"(_Exit_) postdominates (targetnode a)"
by(auto simp:dyn_standard_control_dependence_def)
from path as have "n -[]@a#as'→* (_Exit_)" by simp
hence "valid_edge a" by(fastforce dest:path_split)
with pd show False by -(rule Exit_no_postdominator,auto)
qed

lemma dyn_standard_control_dependence_def_variant:
"n controls⇩s n' via as = ((n -as→* n') ∧ (n ≠ n') ∧
(¬ n' postdominates n) ∧ (n' ∉ set(sourcenodes as)) ∧
(∀n'' ∈ set(targetnodes as). n' postdominates n''))"
proof
assume "(n -as→* n') ∧ (n ≠ n') ∧ (¬ n' postdominates n) ∧
(n' ∉ set(sourcenodes as)) ∧
(∀n''∈set (targetnodes as). n' postdominates n'')"
hence path:"n -as→* n'" and noteq:"n ≠ n'"
and not_pd:"¬ n' postdominates n"
and notin:"n' ∉ set(sourcenodes as)"
and all:"∀n''∈set (targetnodes as). n' postdominates n''"
by auto
have notExit:"n ≠ (_Exit_)"
proof
assume "n = (_Exit_)"
with path have "n = n'" by(fastforce dest:path_Exit_source)
with noteq show False by simp
qed
from path have valid:"valid_node n" and valid':"valid_node n'"
by(auto dest:path_valid_node)
show "n controls⇩s n' via as"
proof(cases as)
case Nil
with path valid not_pd notExit have False
by(fastforce elim:path.cases dest:postdominate_refl)
thus ?thesis by simp
next
case (Cons ax asx)
with all have pd:"n' postdominates targetnode ax"
by(auto simp:targetnodes_def)
from path Cons have source:"n = sourcenode ax"
and path2:"targetnode ax -asx→* n'"
by(auto intro:path_split_Cons)
show ?thesis
proof(cases "∃as'. n -as'→* (_Exit_)")
case True
with not_pd valid valid' obtain as' where path':"n -as'→* (_Exit_)"
and not_isin:"n' ∉ set (sourcenodes as')"
by(auto simp:postdominate_def)
have "as' ≠ []"
proof
assume "as' = []"
with path' have "n = (_Exit_)" by(auto elim:path.cases)
with notExit show False by simp
qed
then obtain a' as'' where as':"as' = a'#as''"
by(cases as',auto elim:path.cases)
with path' have "n -[]@a'#as''→* (_Exit_)" by simp
hence source':"n = sourcenode a'"
and valid_edge:"valid_edge a'"
and path2':"targetnode a' -as''→* (_Exit_)"
by(fastforce dest:path_split)+
from path2' not_isin as' valid'
have "¬ n' postdominates (targetnode a')"
by(auto simp:postdominate_def sourcenodes_def)
with pd path Cons source source' notin valid_edge show ?thesis
by(auto simp:dyn_standard_control_dependence_def)
next
case False
with valid valid' have "n' postdominates n"
by(auto simp:postdominate_def)
with not_pd have False by simp
thus ?thesis by simp
qed
qed
next
assume "n controls⇩s n' via as"
then obtain a nx a' nx' as' where notin:"n' ∉ set(sourcenodes as)"
and path:"n -as→* n'" and as:"as = a#as'" and valid_edge:"valid_edge a'"
and pd:"n' postdominates (targetnode a)"
and source':"sourcenode a' = n"
and not_pd:"¬ n' postdominates (targetnode a')"
by(auto simp:dyn_standard_control_dependence_def)
from path as have source:"sourcenode a = n" by(auto elim:path.cases)
from path as have notExit:"n ≠ (_Exit_)" by(auto elim:path.cases)
from path have valid:"valid_node n" and valid':"valid_node n'"
by(auto dest:path_valid_node)
from notin as source have noteq:"n ≠ n'"
by(fastforce simp:sourcenodes_def)
from valid_edge have valid_target':"valid_node (targetnode a')"
by(fastforce simp:valid_node_def)
{ assume pd':"n' postdominates n"
hence all:"∀as. n -as→* (_Exit_) ⟶ n' ∈ set (sourcenodes as)"
by(auto simp:postdominate_def)
from not_pd valid' valid_target' obtain as'
where "targetnode a' -as'→* (_Exit_)"
by(auto simp:postdominate_def)
with source' valid_edge have path':"n -a'#as'→* (_Exit_)"
by(fastforce intro:Cons_path)
with all have "n' ∈ set (sourcenodes (a'#as'))" by blast
with source' have "n' = n ∨ n' ∈ set (sourcenodes as')"
by(fastforce simp:sourcenodes_def)
hence False
proof
assume "n' = n"
with noteq show ?thesis by simp
next
assume isin:"n' ∈ set (sourcenodes as')"
from path' have path2:"targetnode a' -as'→* (_Exit_)"
by(fastforce elim:path_split_Cons)
thus ?thesis
proof(cases "as' = []")
case True
with path2 have "targetnode a' = (_Exit_)" by(auto elim:path.cases)
with valid_edge all source' have "n' = n"
by(fastforce dest:path_edge simp:sourcenodes_def)
with noteq show ?thesis by simp
next
case False
from path2 not_pd valid' valid_edge obtain as''
where path'':"targetnode a' -as''→* (_Exit_)"
and notin:"n' ∉ set (sourcenodes as'')"
by(auto simp:postdominate_def)
from valid_edge path'' have "sourcenode a' -a'#as''→* (_Exit_)"
by(fastforce intro:Cons_path)
with all source' have "n' ∈ set (sourcenodes ([a']@as''))" by simp
with source' have "n' = n ∨ n' ∈ set (sourcenodes as'')"
by(auto simp:sourcenodes_def)
thus ?thesis
proof
assume "n' = n"
with noteq show ?thesis by simp
next
assume "n' ∈ set (sourcenodes as'')"
with notin show ?thesis by simp
qed
qed
qed }
hence not_pd':"¬ n' postdominates n" by blast
{ fix n'' assume "n'' ∈ set (targetnodes as)"
with as source have "n'' = targetnode a ∨ n'' ∈ set (targetnodes as')"
by(auto simp:targetnodes_def)
hence "n' postdominates n''"
proof
assume "n'' = targetnode a"
with pd show ?thesis by simp
next
assume isin:"n'' ∈ set (targetnodes as')"
hence "∃ni ∈ set (targetnodes as'). ni = n''" by simp
then obtain ns ns' where targets:"targetnodes as' = ns@n''#ns'"
and all_noteq:"∀ni ∈ set ns'. ni ≠ n''"
by(fastforce elim!:rightmost_element_property)
from targets obtain xs ax ys where ys:"ns' = targetnodes ys"
and as':"as' = xs@ax#ys" and target'':"targetnode ax = n''"
by(fastforce elim:map_append_append_maps simp:targetnodes_def)
from all_noteq ys have notin_target:"n'' ∉ set(targetnodes ys)"
by auto
from path as have "n -[]@a#as'→* n'" by simp
hence "targetnode a -as'→* n'"
by(fastforce dest:path_split)
with isin have path':"targetnode a -as'→* n'"
by(fastforce split:if_split_asm simp:targetnodes_def)
with as' target'' have path1:"targetnode a -xs→* sourcenode ax"
and valid_edge':"valid_edge ax"
and path2:"n'' -ys→* n'"
by(auto intro:path_split)
from valid_edge' have "sourcenode ax -[ax]→* targetnode ax" by(rule path_edge)
with path1 target'' have path_n'':"targetnode a -xs@[ax]→* n''"
by(fastforce intro:path_Append)
from notin as as' have notin':"n'∉ set (sourcenodes (xs@[ax]))"
show ?thesis
proof(rule ccontr)
assume "¬ n' postdominates n''"
with valid' target'' valid_edge' obtain asx'
where Exit_path:"n'' -asx'→* (_Exit_)"
and notin'':"n' ∉ set(sourcenodes asx')" by(auto simp:postdominate_def)
from path_n'' Exit_path
have Exit_path':"targetnode a -(xs@[ax])@asx'→* (_Exit_)"
by(fastforce intro:path_Append)
from notin' notin'' have "n' ∉ set(sourcenodes (xs@ax#asx'))"
with pd Exit_path' show False by(simp add:postdominate_def)
qed
qed }
with path not_pd' notin noteq show "(n -as→* n') ∧ (n ≠ n') ∧
(¬ n' postdominates n) ∧ (n' ∉ set(sourcenodes as)) ∧
(∀n'' ∈ set(targetnodes as). n' postdominates n'')" by blast
qed

lemma which_node_dyn_standard_control_dependence_source:
assumes path:"(_Entry_) -as@a#as'→* n"
and Exit_path:"n -as''→* (_Exit_)" and source:"sourcenode a = n'"
and source':"sourcenode a' = n'"
and no_source:"n ∉ set(sourcenodes (a#as'))" and valid_edge':"valid_edge a'"
and inner_node:"inner_node n" and not_pd:"¬ n postdominates (targetnode a')"
and last:"∀ax ax'. ax ∈ set as' ∧ sourcenode ax = sourcenode ax' ∧
valid_edge ax' ⟶ n postdominates targetnode ax'"
shows "n' controls⇩s n via a#as'"
proof -
from path source have path_n'n:"n' -a#as'→* n" by(fastforce dest:path_split_second)
from path have valid_edge:"valid_edge a" by(fastforce intro:path_split)
show ?thesis
proof(cases "n postdominates (targetnode a)")
case True
with path_n'n not_pd no_source source source' valid_edge' show ?thesis
by(auto simp:dyn_standard_control_dependence_def)
next
case False
hence not_pd':"¬ n postdominates (targetnode a)" .
show ?thesis
proof(cases "as' = []")
case True
with path_n'n have "targetnode a = n" by(fastforce elim:path.cases)
with inner_node have "n postdominates (targetnode a)"
by(cases "n = (_Exit_)",auto intro:postdominate_refl simp:inner_node_def)
with not_pd path_n'n no_source source source' valid_edge' show ?thesis
by(fastforce simp:dyn_standard_control_dependence_def)
next
case False
hence notempty':"as' ≠ []" .
with path have path_nxn:"targetnode a -as'→* n"
by(fastforce dest:path_split)
from Exit_path path_nxn have "∃as. targetnode a -as→* (_Exit_)"
by(fastforce dest:path_Append)
with not_pd' inner_node valid_edge obtain asx
where path_Exit:"targetnode a -asx→* (_Exit_)"
and notin:"n ∉ set (sourcenodes asx)"
by(auto simp:postdominate_def inner_is_valid)
show ?thesis
proof(cases "∃asx'. asx = as'@asx'")
case True
then obtain asx' where asx:"asx = as'@asx'" by blast
from path notempty' have "targetnode a -as'→* n"
by(fastforce dest:path_split)
with path_Exit inner_node asx notempty'
obtain a'' as'' where "asx' = a''#as'' ∧ sourcenode a'' = n"
apply(cases asx')
apply(fastforce dest:path_det)
by(fastforce dest:path_split path_det)
with asx have "n ∈ set(sourcenodes asx)" by(simp add:sourcenodes_def)
with notin have False by simp
thus ?thesis by simp
next
case False
hence all:"∀asx'. asx ≠ as'@asx'" by simp
then obtain j asx' where asx:"asx = (take j as')@asx'"
and length:"j < length as'"
and not_more:"∀k > j. ∀asx''. asx ≠ (take k as')@asx''"
by(auto elim:path_split_general)
from asx length have "∃as'1 as'2. asx = as'1@asx' ∧
as' = as'1@as'2 ∧ as'2 ≠ [] ∧ as'1 = take j as'"
by simp(rule_tac x= "drop j as'" in exI,simp)
then obtain as'1 as'' where asx:"asx = as'1@asx'"
and take:"as'1 = take j as'"
and x:"as' = as'1@as''" and x':"as'' ≠ []" by blast
from x x' obtain a1 as'2 where as':"as' = as'1@a1#as'2" and "as'' = a1#as'2"
by(cases as'') auto
have notempty_x':"asx' ≠ []"
proof(cases "asx' = []")
case True
with asx as' have "as' = asx@a1#as'2" by simp
with path_n'n have "n' -(a#asx)@a1#as'2→* n"
by simp
hence "n' -a#asx→* sourcenode a1"
and valid_edge1:"valid_edge a1" by(fastforce elim:path_split)+
hence "targetnode a -asx→* sourcenode a1"
by(fastforce intro:path_split_Cons)
with path_Exit have "(_Exit_) = sourcenode a1" by(rule path_det)
from this[THEN sym] valid_edge1 have False by -(rule Exit_source,simp_all)
thus ?thesis by simp
qed simp
with asx obtain a2 asx'1
where asx:"asx = as'1@a2#asx'1"
and asx':"asx' = a2#asx'1" by(cases asx') auto
from path_n'n as' have "n' -(a#as'1)@a1#as'2→* n" by simp
hence "n' -a#as'1→* sourcenode a1" and valid_edge1:"valid_edge a1"
by(fastforce elim:path_split)+
hence path1:"targetnode a -as'1→* sourcenode a1"
by(fastforce intro:path_split_Cons)
from path_Exit asx
have "targetnode a -as'1→* sourcenode a2"
and valid_edge2:"valid_edge a2"
and path2:"targetnode a2 -asx'1→* (_Exit_)"
by(auto intro:path_split)
with path1 have eq12:"sourcenode a1 = sourcenode a2"
by(cases as'1,auto dest:path_det)
from asx notin have "n ∉ set (sourcenodes asx'1)"
with path2 have not_pd'2:"¬ n postdominates targetnode a2"
by(cases "asx'1 = []",auto simp:postdominate_def)
from as' have "a1 ∈ set as'" by simp
with eq12 last valid_edge2 have "n postdominates targetnode a2" by blast
with not_pd'2 have False by simp
thus ?thesis by simp
qed
qed
qed
qed

lemma inner_node_dyn_standard_control_dependence_predecessor:
assumes inner_node:"inner_node n"
obtains n' as where "n' controls⇩s n via as"
proof(atomize_elim)
from inner_node obtain as' where pathExit:"n -as'→* (_Exit_)"
by(fastforce dest:inner_is_valid Exit_path)
from inner_node obtain as where pathEntry:"(_Entry_) -as→* n"
by(fastforce dest:inner_is_valid Entry_path)
with inner_node have notEmpty:"as ≠ []"
by(auto elim:path.cases simp:inner_node_def)
have "∃a asx. (_Entry_) -a#asx→* n ∧ n ∉ set (sourcenodes (a#asx))"
proof(cases "n ∈ set (sourcenodes as)")
case True
hence "∃n'' ∈ set(sourcenodes as). n = n''" by simp
then obtain ns' ns'' where nodes:"sourcenodes as = ns'@n#ns''"
and notin:"∀n'' ∈ set ns'. n ≠ n''"
by(fastforce elim!:split_list_first_propE)
from nodes obtain xs ys a'
where xs:"sourcenodes xs = ns'" and as:"as = xs@a'#ys"
and source:"sourcenode a' = n"
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
from pathEntry as have "(_Entry_) -xs@a'#ys→* n" by simp
hence path2:"(_Entry_) -xs→* sourcenode a'"
by(fastforce dest:path_split)
show ?thesis
proof(cases "xs = []")
case True
with path2 have "(_Entry_) = sourcenode a'" by(auto elim:path.cases)
with pathEntry source notEmpty have "(_Entry_) -as→* (_Entry_) ∧ as ≠ []"
by(auto elim:path.cases)
hence False by(fastforce dest:path_Entry_target)
thus ?thesis by simp
next
case False
then obtain n a'' xs' where "xs = a''#xs'" by(cases xs) auto
with False path2 notin xs source show ?thesis by simp blast
qed
next
case False
from notEmpty obtain a as' where "as = a#as'" by (cases as) auto
with False pathEntry show ?thesis by auto
qed
then obtain a asx where pathEntry':"(_Entry_) -a#asx→* n"
and notin:"n ∉ set (sourcenodes (a#asx))" by blast
show "∃n' as. n' controls⇩s n via as"
proof(cases "∀a' a''. a' ∈ set asx ∧ sourcenode a' = sourcenode a'' ∧
valid_edge a'' ⟶ n postdominates targetnode a''")
case True
from inner_node have not_pd:"¬ n postdominates (_Exit_)"
by(fastforce intro:empty_path simp:postdominate_def sourcenodes_def)
from pathEntry' have path':"(_Entry_) -[]@a#asx→* n" by simp
hence eq:"sourcenode a = (_Entry_)"
by(fastforce dest:path_split elim:path.cases)
from Entry_Exit_edge obtain a' where "sourcenode a' = (_Entry_)"
and "targetnode a' = (_Exit_)" and "valid_edge a'" by auto
with path' inner_node not_pd True eq notin pathExit
have "sourcenode a controls⇩s n via a#asx"
by -(erule which_node_dyn_standard_control_dependence_source,auto)
thus ?thesis by blast
next
case False
hence "∃a' ∈ set asx. ∃a''. sourcenode a' = sourcenode a'' ∧ valid_edge a'' ∧
¬ n postdominates targetnode a''"
by fastforce
then obtain ax asx' asx'' where "asx = asx'@ax#asx'' ∧
(∃a''. sourcenode ax = sourcenode a'' ∧ valid_edge a'' ∧
¬ n postdominates targetnode a'') ∧
(∀z ∈ set asx''. ¬ (∃a''. sourcenode z = sourcenode a'' ∧ valid_edge a'' ∧
¬ n postdominates targetnode a''))"
by(blast elim!:rightmost_element_property)
then obtain a'' where as':"asx = asx'@ax#asx''"
and eq:"sourcenode ax = sourcenode a''"
and valid_edge:"valid_edge a''"
and not_pd:"¬ n postdominates targetnode a''"
and last:"∀z ∈ set asx''. ¬ (∃a''. sourcenode z = sourcenode a'' ∧
valid_edge a'' ∧ ¬ n postdominates targetnode a'')"
by blast
from notin as' have notin':"n ∉ set (sourcenodes (ax#asx''))"
by(auto simp:sourcenodes_def)
from as' pathEntry' have "(_Entry_) -(a#asx')@ax#asx''→* n" by simp
with inner_node not_pd notin' eq last pathExit valid_edge
have "sourcenode ax controls⇩s n via ax#asx''"
by(fastforce elim!:which_node_dyn_standard_control_dependence_source)
thus ?thesis by blast
qed
qed

end

end


# Theory DynWeakControlDependence

section ‹Dynamic Weak Control Dependence›

theory DynWeakControlDependence imports Postdomination begin

context StrongPostdomination begin

definition
dyn_weak_control_dependence :: "'node ⇒ 'node ⇒ 'edge list ⇒ bool"
("_ weakly controls _ via _" [51,0,0])
where dyn_weak_control_dependence_def:"n weakly controls n' via as ≡
(∃a a' as'. (as = a#as') ∧ (n' ∉ set(sourcenodes as)) ∧ (n -as→* n') ∧
(n' strongly-postdominates (targetnode a)) ∧
(valid_edge a') ∧ (sourcenode a' = n) ∧
(¬ n' strongly-postdominates (targetnode a')))"

lemma Exit_not_dyn_weak_control_dependent:
assumes control:"n weakly controls (_Exit_) via as" shows "False"
proof -
from control obtain as a as' where path:"n -as→* (_Exit_)" and as:"as = a#as'"
and pd:"(_Exit_) postdominates (targetnode a)"
by(auto simp:dyn_weak_control_dependence_def strong_postdominate_def)
from path as have "n -[]@a#as'→* (_Exit_)" by simp
hence "valid_edge a" by(fastforce dest:path_split)
with pd show False by -(rule Exit_no_postdominator,auto)
qed

end

end


# Theory DynPDG

chapter ‹Dynamic Slicing›

section ‹Dynamic Program Dependence Graph›

theory DynPDG imports
"../Basic/CFGExit_wf"
"../Basic/DynStandardControlDependence"
"../Basic/DynWeakControlDependence"
begin

subsection ‹The dynamic PDG›

locale DynPDG =
CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use state_val Exit
for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
and kind :: "'edge ⇒ 'state edge_kind" and valid_edge :: "'edge ⇒ bool"
and Entry :: "'node" ("'('_Entry'_')") and Def :: "'node ⇒ 'var set"
and Use :: "'node ⇒ 'var set" and state_val :: "'state ⇒ 'var ⇒ 'val"
and Exit :: "'node" ("'('_Exit'_')") +
fixes dyn_control_dependence :: "'node ⇒ 'node ⇒ 'edge list ⇒ bool"
("_ controls _ via _" [51,0,0])
assumes Exit_not_dyn_control_dependent:"n controls n' via as ⟹ n' ≠ (_Exit_)"
assumes dyn_control_dependence_path:
"n controls n' via as  ⟹ n -as→* n' ∧ as ≠ []"

begin

inductive cdep_edge :: "'node ⇒ 'edge list ⇒ 'node ⇒ bool"
("_ -_→⇩c⇩d _" [51,0,0] 80)
and ddep_edge :: "'node ⇒ 'var ⇒ 'edge list ⇒ 'node ⇒ bool"
("_ -'{_'}_→⇩d⇩d _" [51,0,0,0] 80)
and DynPDG_edge :: "'node ⇒ 'var option ⇒ 'edge list ⇒ 'node ⇒ bool"

where
― ‹Syntax›
"n -as→⇩c⇩d n' == DynPDG_edge n None as n'"
| "n -{V}as→⇩d⇩d n' == DynPDG_edge n (Some V) as n'"

― ‹Rules›
| DynPDG_cdep_edge:
"n controls n' via as ⟹ n -as→⇩c⇩d n'"

| DynPDG_ddep_edge:
"n influences V in n' via as ⟹ n -{V}as→⇩d⇩d n'"

inductive DynPDG_path :: "'node ⇒ 'edge list ⇒ 'node ⇒ bool"
("_ -_→⇩d* _" [51,0,0] 80)

where DynPDG_path_Nil:
"valid_node n ⟹ n -[]→⇩d* n"

| DynPDG_path_Append_cdep:
"⟦n -as→⇩d* n''; n'' -as'→⇩c⇩d n'⟧ ⟹ n -as@as'→⇩d* n'"

| DynPDG_path_Append_ddep:
"⟦n -as→⇩d* n''; n'' -{V}as'→⇩d⇩d n'⟧ ⟹ n -as@as'→⇩d* n'"

lemma DynPDG_empty_path_eq_nodes:"n -[]→⇩d* n' ⟹ n = n'"
apply - apply(erule DynPDG_path.cases)
apply simp
apply(auto elim:DynPDG_edge.cases dest:dyn_control_dependence_path)
by(auto elim:DynPDG_edge.cases simp:dyn_data_dependence_def)

lemma DynPDG_path_cdep:"n -as→⇩c⇩d n' ⟹ n -as→⇩d* n'"
apply(subgoal_tac "n -[]@as→⇩d* n'")
apply simp
apply(rule DynPDG_path_Append_cdep, rule DynPDG_path_Nil)
by(auto elim!:DynPDG_edge.cases dest:dyn_control_dependence_path path_valid_node)

lemma DynPDG_path_ddep:"n -{V}as→⇩d⇩d n' ⟹ n -as→⇩d* n'"
apply(subgoal_tac "n -[]@as→⇩d* n'")
apply simp
apply(rule DynPDG_path_Append_ddep, rule DynPDG_path_Nil)
by(auto elim!:DynPDG_edge.cases dest:path_valid_node simp:dyn_data_dependence_def)

lemma DynPDG_path_Append:
"⟦n'' -as'→⇩d* n'; n -as→⇩d* n''⟧ ⟹ n -as@as'→⇩d* n'"
apply(induct rule:DynPDG_path.induct)
apply(auto intro:DynPDG_path.intros)
apply(rotate_tac 1,drule DynPDG_path_Append_cdep,simp+)
apply(rotate_tac 1,drule DynPDG_path_Append_ddep,simp+)
done

lemma DynPDG_path_Exit:"⟦n -as→⇩d* n'; n' = (_Exit_)⟧ ⟹ n = (_Exit_)"
apply(induct rule:DynPDG_path.induct)
by(auto elim:DynPDG_edge.cases dest:Exit_not_dyn_control_dependent
simp:dyn_data_dependence_def)

lemma DynPDG_path_not_inner:
"⟦n -as→⇩d* n'; ¬ inner_node n'⟧ ⟹ n = n'"
proof(induct rule:DynPDG_path.induct)
case (DynPDG_path_Nil n)
thus ?case by simp
next
case (DynPDG_path_Append_cdep n as n'' as' n')
from ‹n'' -as'→⇩c⇩d n'› ‹¬ inner_node n'› have False
apply -
apply(erule DynPDG_edge.cases) apply(auto simp:inner_node_def)
apply(fastforce dest:dyn_control_dependence_path path_valid_node)
apply(fastforce dest:dyn_control_dependence_path path_valid_node)
by(fastforce dest:Exit_not_dyn_control_dependent)
thus ?case by simp
next
case (DynPDG_path_Append_ddep n as n'' V as' n')
from ‹n'' -{V}as'→⇩d⇩d n'› ‹¬ inner_node n'› have False
apply -
apply(erule DynPDG_edge.cases)
by(auto dest:path_valid_node simp:inner_node_def dyn_data_dependence_def)
thus ?case by simp
qed

lemma DynPDG_cdep_edge_CFG_path:
assumes "n -as→⇩c⇩d n'" shows "n -as→* n'" and "as ≠ []"
using ‹n -as→⇩c⇩d n'›
by(auto elim:DynPDG_edge.cases dest:dyn_control_dependence_path)

lemma DynPDG_ddep_edge_CFG_path:
assumes "n -{V}as→⇩d⇩d n'" shows "n -as→* n'" and "as ≠ []"
using ‹n -{V}as→⇩d⇩d n'›
by(auto elim:DynPDG_edge.cases simp:dyn_data_dependence_def)

lemma DynPDG_path_CFG_path:
"n -as→⇩d* n' ⟹ n -as→* n'"
proof(induct rule:DynPDG_path.induct)
case DynPDG_path_Nil thus ?case by(rule empty_path)
next
case (DynPDG_path_Append_cdep n as n'' as' n')
from ‹n'' -as'→⇩c⇩d n'› have "n'' -as'→* n'"
by(rule DynPDG_cdep_edge_CFG_path(1))
with ‹n -as→* n''› show ?case by(rule path_Append)
next
case (DynPDG_path_Append_ddep n as n'' V as' n')
from ‹n'' -{V}as'→⇩d⇩d n'› have "n'' -as'→* n'"
by(rule DynPDG_ddep_edge_CFG_path(1))
with ‹n -as→* n''› show ?case by(rule path_Append)
qed

lemma DynPDG_path_split:
"n -as→⇩d* n' ⟹
(as = [] ∧ n = n') ∨
(∃n'' asx asx'. (n -asx→⇩c⇩d n'') ∧ (n'' -asx'→⇩d* n') ∧
(as = asx@asx')) ∨
(∃n'' V asx asx'. (n -{V}asx→⇩d⇩d n'') ∧ (n'' -asx'→⇩d* n') ∧
(as = asx@asx'))"
proof(induct rule:DynPDG_path.induct)
case (DynPDG_path_Nil n) thus ?case by auto
next
case (DynPDG_path_Append_cdep n as n'' as' n')
note IH = ‹as = [] ∧ n = n'' ∨
(∃nx asx asx'. n -asx→⇩c⇩d nx ∧ nx -asx'→⇩d* n'' ∧ as = asx@asx') ∨
(∃nx V asx asx'. n -{V}asx→⇩d⇩d nx ∧ nx -asx'→⇩d* n'' ∧ as = asx@asx')›
from IH show ?case
proof
assume "as = [] ∧ n = n''"
with ‹n'' -as'→⇩c⇩d n'› have "valid_node n'"
by(fastforce intro:path_valid_node(2) DynPDG_path_CFG_path
DynPDG_path_cdep)
with ‹as = [] ∧ n = n''› ‹n'' -as'→⇩c⇩d n'›
have "∃n'' asx asx'. n -asx→⇩c⇩d n'' ∧ n'' -asx'→⇩d* n' ∧ as@as' = asx@asx'"
by(auto intro:DynPDG_path_Nil)
thus ?thesis by simp
next
assume "(∃nx asx asx'. n -asx→⇩c⇩d nx ∧ nx -asx'→⇩d* n'' ∧ as = asx@asx') ∨
(∃nx V asx asx'. n -{V}asx→⇩d⇩d nx ∧ nx -asx'→⇩d* n'' ∧ as = asx@asx')"
thus ?thesis
proof
assume "∃nx asx asx'. n -asx→⇩c⇩d nx ∧ nx -asx'→⇩d* n'' ∧ as = asx@asx'"
then obtain nx asx asx' where "n -asx→⇩c⇩d nx" and "nx -asx'→⇩d* n''"
and "as = asx@asx'" by auto
from ‹n'' -as'→⇩c⇩d n'› have "n'' -as'→⇩d* n'" by(rule DynPDG_path_cdep)
with ‹nx -asx'→⇩d* n''› have "nx -asx'@as'→⇩d* n'"
by(fastforce intro:DynPDG_path_Append)
with ‹n -asx→⇩c⇩d nx› ‹as = asx@asx'›
have "∃n'' asx asx'. n -asx→⇩c⇩d n'' ∧ n'' -asx'→⇩d* n' ∧ as@as' = asx@asx'"
by auto
thus ?thesis by simp
next
assume "∃nx V asx asx'. n -{V}asx→⇩d⇩d nx ∧ nx -asx'→⇩d* n'' ∧ as = asx@asx'"
then obtain nx V asx asx' where "n -{V}asx→⇩d⇩d nx" and "nx -asx'→⇩d* n''"
and "as = asx@asx'" by auto
from ‹n'' -as'→⇩c⇩d n'› have "n'' -as'→⇩d* n'" by(rule DynPDG_path_cdep)
with ‹nx -asx'→⇩d* n''› have "nx -asx'@as'→⇩d* n'"
by(fastforce intro:DynPDG_path_Append)
with ‹n -{V}asx→⇩d⇩d nx› ‹as = asx@asx'›
have "∃n'' V asx asx'. n -{V}asx→⇩d⇩d n'' ∧ n'' -asx'→⇩d* n' ∧ as@as' = asx@asx'"
by auto
thus ?thesis by simp
qed
qed
next
case (DynPDG_path_Append_ddep n as n'' V as' n')
note IH = ‹as = [] ∧ n = n'' ∨
(∃nx asx asx'. n -asx→⇩c⇩d nx ∧ nx -asx'→⇩d* n'' ∧ as = asx@asx') ∨
(∃nx V asx asx'. n -{V}asx→⇩d⇩d nx ∧ nx -asx'→⇩d* n'' ∧ as = asx@asx')›
from IH show ?case
proof
assume "as = [] ∧ n = n''"
with ‹n'' -{V}as'→⇩d⇩d n'› have "valid_node n'"
by(fastforce intro:path_valid_node(2) DynPDG_path_CFG_path
DynPDG_path_ddep)
with ‹as = [] ∧ n = n''› ‹n'' -{V}as'→⇩d⇩d n'›
have "∃n'' V asx asx'. n -{V}asx→⇩d⇩d n'' ∧ n'' -asx'→⇩d* n' ∧ as@as' = asx@asx'"
by(fastforce intro:DynPDG_path_Nil)
thus ?thesis by simp
next
assume "(∃nx asx asx'. n -asx→⇩c⇩d nx ∧ nx -asx'→⇩d* n'' ∧ as = asx@asx') ∨
(∃nx V asx asx'. n -{V}asx→⇩d⇩d nx ∧ nx -asx'→⇩d* n'' ∧ as = asx@asx')"
thus ?thesis
proof
assume "∃nx asx asx'. n -asx→⇩c⇩d nx ∧ nx -asx'→⇩d* n'' ∧ as = asx@asx'"
then obtain nx asx asx' where "n -asx→⇩c⇩d nx" and "nx -asx'→⇩d* n''"
and "as = asx@asx'" by auto
from ‹n'' -{V}as'→⇩d⇩d n'› have "n'' -as'→⇩d* n'" by(rule DynPDG_path_ddep)
with ‹nx -asx'→⇩d* n''› have "nx -asx'@as'→⇩d* n'"
by(fastforce intro:DynPDG_path_Append)
with ‹n -asx→⇩c⇩d nx› ‹as = asx@asx'›
have "∃n'' asx asx'. n -asx→⇩c⇩d n'' ∧ n'' -asx'→⇩d* n' ∧ as@as' = asx@asx'"
by auto
thus ?thesis by simp
next
assume "∃nx V asx asx'. n -{V}asx→⇩d⇩d nx ∧ nx -asx'→⇩d* n'' ∧ as = asx@asx'"
then obtain nx V' asx asx' where "n -{V'}asx→⇩d⇩d nx" and "nx -asx'→⇩d* n''"
and "as = asx@asx'" by auto
from ‹n'' -{V}as'→⇩d⇩d n'› have "n'' -as'→⇩d* n'" by(rule DynPDG_path_ddep)
with ‹nx -asx'→⇩d* n''› have "nx -asx'@as'→⇩d* n'"
by(fastforce intro:DynPDG_path_Append)
with ‹n -{V'}asx→⇩d⇩d nx› ‹as = asx@asx'›
have "∃n'' V asx asx'. n -{V}asx→⇩d⇩d n'' ∧ n'' -asx'→⇩d* n' ∧ as@as' = asx@asx'"
by auto
thus ?thesis by simp
qed
qed
qed

lemma DynPDG_path_rev_cases [consumes 1,
case_names DynPDG_path_Nil DynPDG_path_cdep_Append DynPDG_path_ddep_Append]:
"⟦n -as→⇩d* n'; ⟦as = []; n = n'⟧ ⟹ Q;
⋀n'' asx asx'. ⟦n -asx→⇩c⇩d n''; n'' -asx'→⇩d* n';
as = asx@asx'⟧ ⟹ Q;
⋀V n'' asx asx'. ⟦n -{V}asx→⇩d⇩d n''; n'' -asx'→⇩d* n';
as = asx@asx'⟧ ⟹ Q⟧
⟹ Q"
by(blast dest:DynPDG_path_split)

lemma DynPDG_ddep_edge_no_shorter_ddep_edge:
assumes ddep:"n -{V}as→⇩d⇩d n'"
shows "∀as' a as''. tl as = as'@a#as'' ⟶ ¬ sourcenode a -{V}a#as''→⇩d⇩d n'"
proof -
from ddep have influence:"n influences V in n' via as"
by(auto elim!:DynPDG_edge.cases)
then obtain  a asx where as:"as = a#asx"
and notin:"n ∉ set (sourcenodes asx)"
by(auto dest:dyn_influence_source_notin_tl_edges simp:dyn_data_dependence_def)
from influence as
have imp:"∀nx ∈ set (sourcenodes asx). V ∉ Def nx"
by(auto simp:dyn_data_dependence_def)
{ fix as' a' as''
assume eq:"tl as = as'@a'#as''"
and ddep':"sourcenode a' -{V}a'#as''→⇩d⇩d n'"
from eq as notin have noteq:"sourcenode a' ≠ n" by(auto simp:sourcenodes_def)
from ddep' have "V ∈ Def (sourcenode a')"
by(auto elim!:DynPDG_edge.cases simp:dyn_data_dependence_def)
with eq as noteq imp have False by(auto simp:sourcenodes_def) }
thus ?thesis by blast
qed

lemma no_ddep_same_state:
assumes path:"n -as→* n'" and Uses:"V ∈ Use n'" and preds:"preds (kinds as) s"
and no_dep:"∀as' a as''. as = as'@a#as'' ⟶ ¬ sourcenode a -{V}a#as''→⇩d⇩d n'"
shows "state_val (transfers (kinds as) s) V = state_val s V"
proof -
{ fix n''
assume inset:"n'' ∈ set (sourcenodes as)" and Defs:"V ∈ Def n''"
hence "∃nx ∈ set (sourcenodes as). V ∈ Def nx" by auto
then obtain nx ns' ns'' where nodes:"sourcenodes as = ns'@nx#ns''"
and Defs':"V ∈ Def nx" and notDef:"∀nx' ∈ set ns''. V ∉ Def nx'"
by(fastforce elim!:rightmost_element_property)
from nodes obtain as' a as''
where as'':"sourcenodes as'' = ns''" and as:"as=as'@a#as''"
and source:"sourcenode a = nx"
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
from as path have path':"sourcenode a -a#as''→* n'"
by(fastforce dest:path_split_second)
from notDef as'' source
have "∀n'' ∈ set (sourcenodes as''). V ∉ Def n''"
by(auto simp:sourcenodes_def)
with path' Defs' Uses source
have influence:"nx influences V in n' via (a#as'')"
hence "nx ∉ set (sourcenodes as'')" by(rule dyn_influence_source_notin_tl_edges)
with influence source
have "∃asx a'. sourcenode a' -{V}a'#asx→⇩d⇩d n' ∧ sourcenode a' = nx ∧
(∃asx'. a#as'' = asx'@a'#asx)"
by(fastforce intro:DynPDG_ddep_edge)
with nodes no_dep as have False by(auto simp:sourcenodes_def) }
hence "∀n ∈ set (sourcenodes as). V ∉ Def n" by auto
with wf path preds show ?thesis by(fastforce intro:CFG_path_no_Def_equal)
qed

lemma DynPDG_ddep_edge_only_first_edge:
"⟦n -{V}a#as→⇩d⇩d n'; preds (kinds (a#as)) s⟧ ⟹
state_val (transfers (kinds (a#as)) s) V = state_val (transfer (kind a) s) V"
apply -
apply(erule DynPDG_edge.cases)
apply auto
apply(frule dyn_influence_Cons_source)
apply(frule dyn_influence_source_notin_tl_edges)
by(erule dyn_influence_only_first_edge)

lemma Use_value_change_implies_DynPDG_ddep_edge:
assumes "n -as→* n'" and "V ∈ Use n'" and "preds (kinds as) s"
and "preds (kinds as) s'" and "state_val s V = state_val s' V"
and "state_val (transfers (kinds as) s) V ≠
state_val (transfers (kinds as) s') V"
obtains as' a as'' where "as = as'@a#as''"
and "sourcenode a -{V}a#as''→⇩d⇩d n'"
and "state_val (transfers (kinds as) s) V =
state_val (transfers (kinds (as'@[a])) s) V"
and "state_val (transfers (kinds as) s') V =
state_val (transfers (kinds (as'@[a])) s') V"
proof(atomize_elim)
show "∃as' a as''. as = as'@a#as'' ∧
sourcenode a -{V}a#as''→⇩d⇩d n' ∧
state_val (transfers (kinds as) s) V =
state_val (transfers (kinds (as'@[a])) s) V ∧
state_val (transfers (kinds as) s') V =
state_val (transfers (kinds (as'@[a])) s') V"
proof(cases "∀as' a as''. as = as'@a#as'' ⟶
¬ sourcenode a -{V}a#as''→⇩d⇩d n'")
case True
with ‹n -as→* n'› ‹V ∈ Use n'› ‹preds (kinds as) s› ‹preds (kinds as) s'›
have "state_val (transfers (kinds as) s) V = state_val s V"
and "state_val (transfers (kinds as) s') V = state_val s' V"
by(auto intro:no_ddep_same_state)
with ‹state_val s V = state_val s' V›
‹state_val (transfers (kinds as) s) V ≠ state_val (transfers (kinds as) s') V›
show ?thesis by simp
next
case False
then obtain as' a as'' where [simp]:"as = as'@a#as''"
and "sourcenode a -{V}a#as''→⇩d⇩d n'" by auto
from ‹preds (kinds as) s› have "preds (kinds (a#as'')) (transfers (kinds as') s)"
with ‹sourcenode a -{V}a#as''→⇩d⇩d n'› have all:
"state_val (transfers (kinds (a#as'')) (transfers (kinds as') s)) V =
state_val (transfer (kind a) (transfers (kinds as') s)) V"
by(auto dest!:DynPDG_ddep_edge_only_first_edge)
from ‹preds (kinds as) s'›
have "preds (kinds (a#as'')) (transfers (kinds as') s')"
with ‹sourcenode a -{V}a#as''→⇩d⇩d n'› have all':
"state_val (transfers (kinds (a#as'')) (transfers (kinds as') s')) V =
state_val (transfer (kind a) (transfers (kinds as') s')) V"
by(auto dest!:DynPDG_ddep_edge_only_first_edge)
hence eq:"⋀s. transfers (kinds as) s =
transfers (kinds (a#as'')) (transfers (kinds as') s)"
with all have "state_val (transfers (kinds as) s) V =
state_val (transfers (kinds (as'@[a])) s) V"
moreover
from eq all' have "state_val (transfers (kinds as) s') V =
state_val (transfers (kinds (as'@[a])) s') V"
ultimately show ?thesis using ‹sourcenode a -{V}a#as''→⇩d⇩d n'› by simp blast
qed
qed

end

subsection ‹Instantiate dynamic PDG›

subsubsection ‹Standard control dependence›

locale DynStandardControlDependencePDG =
Postdomination sourcenode targetnode kind valid_edge Entry Exit +
CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use state_val Exit
for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
and kind :: "'edge ⇒ 'state edge_kind" and valid_edge :: "'edge ⇒ bool"
and Entry :: "'node" ("'('_Entry'_')") and Def :: "'node ⇒ 'var set"
and Use :: "'node ⇒ 'var set" and state_val :: "'state ⇒ 'var ⇒ 'val"
and Exit :: "'node" ("'('_Exit'_')")

begin

lemma DynPDG_scd:
"DynPDG sourcenode targetnode kind valid_edge (_Entry_)
Def Use state_val (_Exit_) dyn_standard_control_dependence"
proof(unfold_locales)
fix n n' as assume "n controls⇩s n' via as"
show "n' ≠ (_Exit_)"
proof
assume "n' = (_Exit_)"
with ‹n controls⇩s n' via as› show False
by(fastforce intro:Exit_not_dyn_standard_control_dependent)
qed
next
fix n n' as assume "n controls⇩s n' via as"
thus "n -as→* n' ∧ as ≠ []"
by(fastforce simp:dyn_standard_control_dependence_def)
qed

end

subsubsection ‹Weak control dependence›

locale DynWeakControlDependencePDG =
StrongPostdomination sourcenode targetnode kind valid_edge Entry Exit +
CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use state_val Exit
for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
and kind :: "'edge ⇒ 'state edge_kind" and valid_edge :: "'edge ⇒ bool"
and Entry :: "'node" ("'('_Entry'_')") and Def :: "'node ⇒ 'var set"
and Use :: "'node ⇒ 'var set" and state_val :: "'state ⇒ 'var ⇒ 'val"
and Exit :: "'node" ("'('_Exit'_')")

begin

lemma DynPDG_wcd:
"DynPDG sourcenode targetnode kind valid_edge (_Entry_)
Def Use state_val (_Exit_) dyn_weak_control_dependence"
proof(unfold_locales)
fix n n' as assume "n weakly controls n' via as"
show "n' ≠ (_Exit_)"
proof
assume "n' = (_Exit_)"
with ‹n weakly controls n' via as› show False
by(fastforce intro:Exit_not_dyn_weak_control_dependent)
qed
next
fix n n' as assume "n weakly controls n' via as"
thus "n -as→* n' ∧ as ≠ []"
by(fastforce simp:dyn_weak_control_dependence_def)
qed

end

subsection ‹Data slice›

definition (in CFG) empty_control_dependence :: "'node ⇒ 'node ⇒ 'edge list ⇒ bool"
where "empty_control_dependence n n' as ≡ False"

lemma (in CFGExit_wf) DynPDG_scd:
"DynPDG sourcenode targetnode kind valid_edge (_Entry_)
Def Use state_val  (_Exit_) empty_control_dependence"
proof(unfold_locales)
fix n n' as assume "empty_control_dependence n n' as"
thus "n' ≠ (_Exit_)" by(simp add:empty_control_dependence_def)
next
fix n n' as assume "empty_control_dependence n n' as"
thus "n -as→* n' ∧ as ≠ []" by(simp add:empty_control_dependence_def)
qed

end


# Theory DependentLiveVariables

section ‹Dependent Live Variables›

theory DependentLiveVariables imports DynPDG begin

text ‹‹dependent_live_vars› calculates variables which
can change\\ the value of the @{term Use} variables of the target node›

context DynPDG begin

inductive_set
dependent_live_vars :: "'node ⇒ ('var × 'edge list × 'edge list) set"
for n' :: "'node"
where dep_vars_Use:
"V ∈ Use n' ⟹ (V,[],[]) ∈ dependent_live_vars n'"

| dep_vars_Cons_cdep:
"⟦V ∈ Use (sourcenode a); sourcenode a -a#as'→⇩c⇩d n''; n'' -as''→⇩d* n'⟧
⟹ (V,[],a#as'@as'') ∈ dependent_live_vars n'"

| dep_vars_Cons_ddep:
"⟦(V,as',as) ∈ dependent_live_vars n'; V' ∈ Use (sourcenode a);
n' = last(targetnodes (a#as));
sourcenode a -{V}a#as'→⇩d⇩d last(targetnodes (a#as'))⟧
⟹ (V',[],a#as) ∈ dependent_live_vars n'"

| dep_vars_Cons_keep:
"⟦(V,as',as) ∈ dependent_live_vars n'; n' = last(targetnodes (a#as));
¬ sourcenode a -{V}a#as'→⇩d⇩d last(targetnodes (a#as'))⟧
⟹ (V,a#as',a#as) ∈ dependent_live_vars n'"

lemma dependent_live_vars_fst_prefix_snd:
"(V,as',as) ∈ dependent_live_vars n' ⟹ ∃as''. as'@as'' = as"
by(induct rule:dependent_live_vars.induct,simp_all)

lemma dependent_live_vars_Exit_empty [dest]:
"(V,as',as) ∈ dependent_live_vars (_Exit_) ⟹ False"
proof(induct rule:dependent_live_vars.induct)
case (dep_vars_Cons_cdep V a as' n'' as'')
from ‹n'' -as''→⇩d* (_Exit_)› have "n'' = (_Exit_)"
by(fastforce intro:DynPDG_path_Exit)
with ‹sourcenode a -a#as'→⇩c⇩d n''› have "sourcenode a -a#as'→⇩d* (_Exit_)"
by(fastforce intro:DynPDG_path_cdep)
hence "sourcenode a = (_Exit_)" by(fastforce intro:DynPDG_path_Exit)
with ‹V ∈ Use (sourcenode a)› show False by simp(erule Exit_Use_empty)
qed auto

lemma dependent_live_vars_lastnode:
"⟦(V,as',as) ∈ dependent_live_vars n'; as ≠ []⟧
⟹ n' = last(targetnodes as)"
proof(induct rule:dependent_live_vars.induct)
case (dep_vars_Cons_cdep V a as' n'' as'')
from ‹sourcenode a -a#as'→⇩c⇩d n''› have "sourcenode a -a#as'→* n''"
by(rule DynPDG_cdep_edge_CFG_path(1))
from ‹n'' -as''→⇩d* n'› have "n'' -as''→* n'" by(rule DynPDG_path_CFG_path)
show ?case
proof(cases "as'' = []")
case True
with ‹n'' -as''→* n'› have "n'' = n'" by (auto elim: DynPDG.dependent_live_vars.cases)
with ‹sourcenode a -a#as'→* n''› True
show ?thesis by(fastforce intro:path_targetnode[THEN sym])
next
case False
with ‹n'' -as''→* n'› have "n' = last(targetnodes as'')"
by(fastforce intro:path_targetnode[THEN sym])
with False show ?thesis by(fastforce simp:targetnodes_def)
qed
qed simp_all

lemma dependent_live_vars_Use_cases:
"⟦(V,as',as) ∈ dependent_live_vars n'; n -as→* n'⟧
⟹ ∃nx as''. as = as'@as'' ∧ n -as'→* nx ∧ nx -as''→⇩d* n' ∧ V ∈ Use nx ∧
(∀n'' ∈ set (sourcenodes as'). V ∉ Def n'')"
proof(induct arbitrary:n rule:dependent_live_vars.induct)
case (dep_vars_Use V)
from ‹n -[]→* n'› have "valid_node n'" by(rule path_valid_node(2))
hence "n' -[]→⇩d* n'" by(rule DynPDG_path_Nil)
with ‹V ∈ Use n'› ‹n -[]→* n'› show ?case
by(auto simp:sourcenodes_def)
next
case (dep_vars_Cons_cdep V a as' n'' as'' n)
from ‹n -a#as'@as''→* n'› have "sourcenode a = n"
by(auto elim:path.cases)
from ‹sourcenode a -a#as'→⇩c⇩d n''› have "sourcenode a -a#as'→* n''"
by(rule DynPDG_cdep_edge_CFG_path(1))
hence "valid_edge a" by(auto elim:path.cases)
hence "sourcenode a -[]→* sourcenode a" by(fastforce intro:empty_path)
from ‹sourcenode a -a#as'→⇩c⇩d n''› have "sourcenode a -a#as'→⇩d* n''"
by(rule DynPDG_path_cdep)
with ‹n'' -as''→⇩d* n'› have "sourcenode a -(a#as')@as''→⇩d* n'"
by(rule DynPDG_path_Append)
with ‹sourcenode a -[]→* sourcenode a› ‹V ∈ Use (sourcenode a)› ‹sourcenode a = n›
show ?case by(auto simp:sourcenodes_def)
next
case(dep_vars_Cons_ddep V as' as V' a n)
note ddep = ‹sourcenode a -{V}a#as'→⇩d⇩d last (targetnodes (a#as'))›
note IH = ‹⋀n. n -as→* n'
⟹ ∃nx as''. as = as'@as'' ∧ n -as'→* nx ∧ nx -as''→⇩d* n' ∧
V ∈ Use nx ∧ (∀n''∈set (sourcenodes as'). V ∉ Def n'')›
from ‹n -a#as→* n'› have "n -[]@a#as→* n'" by simp
hence "n = sourcenode a" and "targetnode a -as→* n'" and "valid_edge a"
by(fastforce dest:path_split)+
hence "n -[]→* n"
by(fastforce intro:empty_path simp:valid_node_def)
from IH[OF ‹targetnode a -as→* n'›]
have "∃nx as''. as = as'@as'' ∧ targetnode a -as'→* nx ∧ nx -as''→⇩d* n' ∧
V ∈ Use nx ∧ (∀n''∈set (sourcenodes as'). V ∉ Def n'')" .
then obtain nx'' as'' where "targetnode a -as'→* nx''"
and "nx'' -as''→⇩d* n'" and "as = as'@as''" by blast
have "last (targetnodes (a#as')) -as''→⇩d* n'"
proof(cases as')
case Nil
with ‹targetnode a -as'→* nx''› have "nx'' = targetnode a"
by(auto elim:path.cases)
with ‹nx'' -as''→⇩d* n'› Nil show ?thesis by(simp add:targetnodes_def)
next
case (Cons ax asx)
hence "last (targetnodes (a#as')) = last (targetnodes as')"
from Cons ‹targetnode a -as'→* nx''› have "last (targetnodes as') = nx''"
by(fastforce intro:path_targetnode)
with ‹last (targetnodes (a#as')) = last (targetnodes as')› ‹nx'' -as''→⇩d* n'›
show ?thesis by simp
qed
with ddep ‹as = as'@as''› have "sourcenode a -a#as→⇩d* n'"
by(fastforce dest:DynPDG_path_ddep DynPDG_path_Append)
with ‹V' ∈ Use (sourcenode a)› ‹n = sourcenode a› ‹n -[]→* n›
show ?case by(auto simp:sourcenodes_def)
next
case (dep_vars_Cons_keep V as' as a n)
note no_dep = ‹¬ sourcenode a -{V}a#as'→⇩d⇩d last (targetnodes (a#as'))›
note IH = ‹⋀n. n -as→* n'
⟹ ∃nx as''. (as = as'@as'') ∧ (n -as'→* nx) ∧ (nx -as''→⇩d* n') ∧
V ∈ Use nx ∧ (∀n''∈set (sourcenodes as'). V ∉ Def n'')›
from ‹n -a#as→* n'› have "n = sourcenode a" and "valid_edge a"
and "targetnode a -as→* n'" by(auto elim:path_split_Cons)
from IH[OF ‹targetnode a -as→* n'›]
have "∃nx as''. as = as'@as'' ∧ targetnode a -as'→* nx ∧ nx -as''→⇩d* n' ∧
V ∈ Use nx ∧ (∀n''∈set (sourcenodes as'). V ∉ Def n'')" .
then obtain nx'' as'' where "V ∈ Use nx''"
and "∀n''∈set (sourcenodes as'). V ∉ Def n''" and "targetnode a -as'→* nx''"
and "nx'' -as''→⇩d* n'" and "as = as'@as''" by blast
from ‹valid_edge a› ‹targetnode a -as'→* nx''› have "sourcenode a -a#as'→* nx''"
by(fastforce intro:Cons_path)
hence "last(targetnodes (a#as')) = nx''" by(fastforce dest:path_targetnode)
{ assume "V ∈ Def (sourcenode a)"
with ‹V ∈ Use nx''› ‹sourcenode a -a#as'→* nx''›
‹∀n''∈set (sourcenodes as'). V ∉ Def n''›
have "(sourcenode a) influences V in nx'' via a#as'"
with no_dep ‹last(targetnodes (a#as')) = nx''›
‹∀n''∈set (sourcenodes as'). V ∉ Def n''› ‹V ∈ Def (sourcenode a)›
have False by(fastforce dest:DynPDG_ddep_edge) }
with ‹∀n''∈set (sourcenodes as'). V ∉ Def n''›
have "∀n''∈set (sourcenodes (a#as')). V ∉ Def n''"
by(fastforce simp:sourcenodes_def)
with ‹V ∈ Use nx''› ‹sourcenode a -a#as'→* nx''› ‹nx'' -as''→⇩d* n'›
‹as = as'@as''› ‹n = sourcenode a› show ?case by fastforce
qed

lemma dependent_live_vars_dependent_edge:
assumes "(V,as',as) ∈ dependent_live_vars n'"
and "targetnode a -as→* n'"
and "V ∈ Def (sourcenode a)" and "valid_edge a"
obtains nx as'' where "as = as'@as''" and "sourcenode a -{V}a#as'→⇩d⇩d nx"
and "nx -as''→⇩d* n'"
proof(atomize_elim)
from ‹(V,as',as) ∈ dependent_live_vars n'› ‹targetnode a -as→* n'›
have "∃nx as''. as = as'@as'' ∧ targetnode a -as'→* nx ∧ nx -as''→⇩d* n' ∧
V ∈ Use nx ∧ (∀n'' ∈ set (sourcenodes as'). V ∉ Def n'')"
by(rule dependent_live_vars_Use_cases)
then obtain nx as'' where "V ∈ Use nx"
and "∀n''∈ set(sourcenodes as'). V ∉ Def n''"
and "targetnode a -as'→* nx" and "nx -as''→⇩d* n'"
and "as = as'@as''" by blast
from ‹targetnode a -as'→* nx› ‹valid_edge a› have "sourcenode a -a#as'→* nx"
by(fastforce intro:Cons_path)
with ‹V ∈ Def (sourcenode a)› ‹V ∈ Use nx›
‹∀n''∈ set(sourcenodes as'). V ∉ Def n''›
have "sourcenode a influences V in nx via a#as'"
by(auto simp:dyn_data_dependence_def sourcenodes_def)
hence "sourcenode a -{V}a#as'→⇩d⇩d nx" by(rule DynPDG_ddep_edge)
with ‹nx -as''→⇩d* n'› ‹as = as'@as''›
show "∃as'' nx. (as = as'@as'') ∧ (sourcenode a -{V}a#as'→⇩d⇩d nx) ∧
(nx -as''→⇩d* n')" by fastforce
qed

lemma dependent_live_vars_same_pathsI:
assumes "V ∈ Use n'"
shows "⟦∀as' a as''. as = as'@a#as'' ⟶ ¬ sourcenode a -{V}a#as''→⇩d⇩d n';
as ≠ [] ⟶ n' = last(targetnodes as)⟧
⟹ (V,as,as) ∈ dependent_live_vars n'"
proof(induct as)
case Nil
from ‹V ∈ Use n'› show ?case by(rule dep_vars_Use)
next
case (Cons ax asx)
note lastnode = ‹ax#asx ≠ [] ⟶ n' = last (targetnodes (ax#asx))›
note IH = ‹⟦∀as' a as''. asx = as'@a#as'' ⟶
¬ sourcenode a -{V}a#as''→⇩d⇩d n';
asx ≠ [] ⟶ n' = last (targetnodes asx)⟧
⟹ (V, asx, asx) ∈ dependent_live_vars n'›
from ‹∀as' a as''. ax#asx = as'@a#as'' ⟶ ¬ sourcenode a -{V}a#as''→⇩d⇩d n'›
have all':"∀as' a as''. asx = as'@a#as'' ⟶ ¬ sourcenode a -{V}a#as''→⇩d⇩d n'"
and "¬ sourcenode ax -{V}ax#asx→⇩d⇩d n'"
by simp_all
show ?case
proof(cases "asx = []")
case True
from ‹V ∈ Use n'› have "(V,[],[]) ∈ dependent_live_vars n'" by(rule dep_vars_Use)
with ‹¬ sourcenode ax -{V}ax#asx→⇩d⇩d n'› True lastnode
have "(V,[ax],[ax]) ∈ dependent_live_vars n'"
by(fastforce intro:dep_vars_Cons_keep)
with True show ?thesis by simp
next
case False
with lastnode have "asx ≠ [] ⟶ n' = last (targetnodes asx)"
from IH[OF all' this] have "(V, asx, asx) ∈ dependent_live_vars n'" .
with ‹¬ sourcenode ax -{V}ax#asx→⇩d⇩d n'› lastnode
show ?thesis by(fastforce intro:dep_vars_Cons_keep)
qed
qed

lemma dependent_live_vars_same_pathsD:
"⟦(V,as,as) ∈ dependent_live_vars n';  as ≠ [] ⟶ n' = last(targetnodes as)⟧
⟹ V ∈ Use n' ∧ (∀as' a as''. as = as'@a#as'' ⟶
¬ sourcenode a -{V}a#as''→⇩d⇩d n')"
proof(induct as)
case Nil
have "(V,[],[]) ∈ dependent_live_vars n'" by fact
thus ?case
by(fastforce elim:dependent_live_vars.cases simp:targetnodes_def sourcenodes_def)
next
case (Cons ax asx)
note IH = ‹⟦(V,asx,asx) ∈ dependent_live_vars n';
asx ≠ [] ⟶ n' = last (targetnodes asx)⟧
⟹ V ∈ Use n' ∧ (∀as' a as''. asx = as'@a#as'' ⟶
¬ sourcenode a -{V}a#as''→⇩d⇩d n')›
from ‹(V,ax#asx,ax#asx) ∈ dependent_live_vars n'›
have "(V,asx,asx) ∈ dependent_live_vars n'"
and "¬ sourcenode ax -{V}ax#asx→⇩d⇩d last(targetnodes (ax#asx))"
by(auto elim:dependent_live_vars.cases)
from ‹ax#asx ≠ [] ⟶ n' = last (targetnodes (ax#asx))›
have "n' = last (targetnodes (ax#asx))" by simp
show ?case
proof(cases "asx = []")
case True
with ‹(V,asx,asx) ∈ dependent_live_vars n'› have "V ∈ Use n'"
by(fastforce elim:dependent_live_vars.cases)
from ‹¬ sourcenode ax -{V}ax#asx→⇩d⇩d last(targetnodes (ax#asx))›
True ‹n' = last (targetnodes (ax#asx))›
have "∀as' a as''. ax#asx = as'@a#as'' ⟶ ¬ sourcenode a -{V}a#as''→⇩d⇩d n'"
by auto(case_tac as',auto)
with ‹V ∈ Use n'› show ?thesis by simp
next
case False
with ‹n' = last (targetnodes (ax#asx))›
have "asx ≠ [] ⟶ n' = last (targetnodes asx)"
from IH[OF ‹(V,asx,asx) ∈ dependent_live_vars n'› this]
have "V ∈ Use n' ∧ (∀as' a as''. asx = as'@a#as'' ⟶
¬ sourcenode a -{V}a#as''→⇩d⇩d n')" .
with ‹¬ sourcenode ax -{V}ax#asx→⇩d⇩d last(targetnodes (ax#asx))›
‹n' = last (targetnodes (ax#asx))› have "V ∈ Use n'"
and "∀as' a as''. ax#asx = as'@a#as'' ⟶
¬ sourcenode a -{V}a#as''→⇩d⇩d n'"
by auto(case_tac as',auto)
thus ?thesis by simp
qed
qed

lemma dependent_live_vars_same_paths:
"as ≠ [] ⟶ n' = last(targetnodes as) ⟹
(V,as,as) ∈ dependent_live_vars n' =
(V ∈ Use n' ∧ (∀as' a as''. as = as'@a#as'' ⟶
¬ sourcenode a -{V}a#as''→⇩d⇩d n'))"
by(fastforce intro!:dependent_live_vars_same_pathsD dependent_live_vars_same_pathsI)

lemma dependent_live_vars_cdep_empty_fst:
assumes "n'' -as→⇩c⇩d n'" and "V' ∈ Use n''"
shows "(V',[],as) ∈ dependent_live_vars n'"
proof(cases as)
case Nil
with ‹n'' -as→⇩c⇩d n'› show ?thesis
by(fastforce elim:DynPDG_edge.cases dest:dyn_control_dependence_path)
next
case (Cons ax asx)
with ‹n'' -as→⇩c⇩d n'› have "sourcenode ax = n''"
by(auto dest:DynPDG_cdep_edge_CFG_path elim:path.cases)
from ‹n'' -as→⇩c⇩d n'› have "valid_node n'"
by(fastforce intro:path_valid_node(2) DynPDG_cdep_edge_CFG_path(1))
from Cons ‹n'' -as→⇩c⇩d n'› have "last(targetnodes as) = n'"
by(fastforce intro:path_targetnode dest:DynPDG_cdep_edge_CFG_path)
with Cons ‹n'' -as→⇩c⇩d n'› ‹V' ∈ Use n''› ‹sourcenode ax = n''› ‹valid_node n'›
have "(V', [], ax#asx@[]) ∈ dependent_live_vars n'"
by(fastforce intro:dep_vars_Cons_cdep DynPDG_path_Nil)
with Cons show ?thesis by simp
qed

lemma dependent_live_vars_ddep_empty_fst:
assumes "n'' -{V}as→⇩d⇩d n'" and "V' ∈ Use n''"
shows "(V',[],as) ∈ dependent_live_vars n'"
proof(cases as)
case Nil
with ‹n'' -{V}as→⇩d⇩d n'› show ?thesis
by(fastforce elim:DynPDG_edge.cases simp:dyn_data_dependence_def)
next
case (Cons ax asx)
with ‹n'' -{V}as→⇩d⇩d n'› have "sourcenode ax = n''"
by(auto dest:DynPDG_ddep_edge_CFG_path elim:path.cases)
from Cons ‹n'' -{V}as→⇩d⇩d n'› have "last(targetnodes as) = n'"
by(fastforce intro:path_targetnode elim:DynPDG_ddep_edge_CFG_path(1))
from Cons ‹n'' -{V}as→⇩d⇩d n'› have all:"∀as' a as''. asx = as'@a#as'' ⟶
¬ sourcenode a -{V}a#as''→⇩d⇩d n'"
by(fastforce dest:DynPDG_ddep_edge_no_shorter_ddep_edge)
from ‹n'' -{V}as→⇩d⇩d n'› have "V ∈ Use n'"
by(auto elim!:DynPDG_edge.cases simp:dyn_data_dependence_def)
from Cons ‹n'' -{V}as→⇩d⇩d n'› have "as ≠ [] ⟶ n' = last(targetnodes as)"
by(fastforce dest:DynPDG_ddep_edge_CFG_path path_targetnode)
with Cons have "asx ≠ [] ⟶ n' = last(targetnodes asx)"
by(fastforce simp:targetnodes_def)
with all ‹V ∈ Use n'› have "(V,asx,asx) ∈ dependent_live_vars n'"
by -(rule dependent_live_vars_same_pathsI)
with ‹V' ∈ Use n''› ‹n'' -{V}as→⇩d⇩d n'› ‹last(targetnodes as) = n'›
Cons ‹sourcenode ax = n''› show ?thesis
by(fastforce intro:dep_vars_Cons_ddep)
qed

lemma ddep_dependent_live_vars_keep_notempty:
assumes "n -{V}a#as→⇩d⇩d n''" and "as' ≠ []"
and "(V,as'',as') ∈ dependent_live_vars n'"
shows "(V,as@as'',as@as') ∈ dependent_live_vars n'"
proof -
from ‹n -{V}a#as→⇩d⇩d n''› have "∀n'' ∈ set (sourcenodes as). V ∉ Def n''"
by(auto elim:DynPDG_edge.cases simp:dyn_data_dependence_def)
with ‹(V,as'',as') ∈ dependent_live_vars n'› show ?thesis
proof(induct as)
case Nil thus ?case by simp
next
case (Cons ax asx)
note IH = ‹⟦(V,as'',as') ∈ dependent_live_vars n';
∀n''∈set (sourcenodes asx). V ∉ Def n''⟧
⟹ (V, asx@as'',asx@as') ∈ dependent_live_vars n'›
from ‹∀n''∈set (sourcenodes (ax#asx)). V ∉ Def n''›
have "∀n''∈set (sourcenodes asx). V ∉ Def n''"
by(auto simp:sourcenodes_def)
from IH[OF ‹(V,as'',as') ∈ dependent_live_vars n'› this]
have "(V,asx@as'',asx@as') ∈ dependent_live_vars n'" .
from ‹as' ≠ []› ‹(V,as'',as') ∈ dependent_live_vars n'›
have "n' = last(targetnodes as')"
by(fastforce intro:dependent_live_vars_lastnode)
with ‹as' ≠ []› have "n' = last(targetnodes (ax#asx@as'))"
by(fastforce simp:targetnodes_def)
have "¬ sourcenode ax -{V}ax#asx@as''→⇩d⇩d last(targetnodes (ax#asx@as''))"
proof
assume "sourcenode ax -{V}ax#asx@as''→⇩d⇩d last(targetnodes (ax#asx@as''))"
hence "sourcenode ax -{V}ax#asx@as''→⇩d⇩d last(targetnodes (ax#asx@as''))"
by simp
with ‹∀n''∈set (sourcenodes (ax#asx)). V ∉ Def n''›
show False
by(fastforce elim:DynPDG_edge.cases
simp:dyn_data_dependence_def sourcenodes_def)
qed
with ‹(V,asx@as'',asx@as') ∈ dependent_live_vars n'›
‹n' = last(targetnodes (ax#asx@as'))›
show ?case by(fastforce intro:dep_vars_Cons_keep)
qed
qed

lemma dependent_live_vars_cdep_dependent_live_vars:
assumes "n'' -as''→⇩c⇩d n'" and "(V',as',as) ∈ dependent_live_vars n''"
shows "(V',as',as@as'') ∈ dependent_live_vars n'"
proof -
from ‹n'' -as''→⇩c⇩d n'› have "as'' ≠ []"
by(fastforce elim:DynPDG_edge.cases dest:dyn_control_dependence_path)
with ‹n'' -as''→⇩c⇩d n'› have "last(targetnodes as'') = n'"
by(fastforce intro:path_targetnode elim:DynPDG_cdep_edge_CFG_path(1))
from ‹(V',as',as) ∈ dependent_live_vars n''› show ?thesis
proof(induct rule:dependent_live_vars.induct)
case (dep_vars_Use V')
from ‹V' ∈ Use n''› ‹n'' -as''→⇩c⇩d n'› ‹last(targetnodes as'') = n'› show ?case
by(fastforce intro:dependent_live_vars_cdep_empty_fst simp:targetnodes_def)
next
case (dep_vars_Cons_cdep V a as' nx asx)
from ‹n'' -as''→⇩c⇩d n'› have "n'' -as''→⇩d* n'" by(rule DynPDG_path_cdep)
with ‹nx -asx→⇩d* n''› have "nx -asx@as''→⇩d* n'"
by -(rule DynPDG_path_Append)
with ‹V ∈ Use (sourcenode a)› ‹(sourcenode a) -a#as'→⇩c⇩d nx›
show ?case by(fastforce intro:dependent_live_vars.dep_vars_Cons_cdep)
next
case (dep_vars_Cons_ddep V as' as V' a)
from ‹as'' ≠ []› ‹last(targetnodes as'') = n'›
have "n' = last(targetnodes ((a#as)@as''))"
with dep_vars_Cons_ddep
show ?case by(fastforce intro:dependent_live_vars.dep_vars_Cons_ddep)
next
case (dep_vars_Cons_keep V as' as a)
from ‹as'' ≠ []› ‹last(targetnodes as'') = n'›
have "n' = last(targetnodes ((a#as)@as''))"
with dep_vars_Cons_keep
show ?case by(fastforce intro:dependent_live_vars.dep_vars_Cons_keep)
qed
qed

lemma dependent_live_vars_ddep_dependent_live_vars:
assumes "n'' -{V}as''→⇩d⇩d n'" and "(V',as',as) ∈ dependent_live_vars n''"
shows "(V',as',as@as'') ∈ dependent_live_vars n'"
proof -
from ‹n'' -{V}as''→⇩d⇩d n'› have "as'' ≠ []"
by(rule DynPDG_ddep_edge_CFG_path(2))
with ‹n'' -{V}as''→⇩d⇩d n'› have "last(targetnodes as'') = n'"
by(fastforce intro:path_targetnode elim:DynPDG_ddep_edge_CFG_path(1))
from ‹n'' -{V}as''→⇩d⇩d n'› have notExit:"n' ≠ (_Exit_)"
by(fastforce elim:DynPDG_edge.cases simp:dyn_data_dependence_def)
from ‹(V',as',as) ∈ dependent_live_vars n''› show ?thesis
proof(induct rule:dependent_live_vars.induct)
case (dep_vars_Use V')
from ‹V' ∈ Use n''› ‹n'' -{V}as''→⇩d⇩d n'› ‹last(targetnodes as'') = n'› show ?case
by(fastforce intro:dependent_live_vars_ddep_empty_fst simp:targetnodes_def)
next
case (dep_vars_Cons_cdep V' a as' nx asx)
from ‹n'' -{V}as''→⇩d⇩d n'› have "n'' -as''→⇩d* n'" by(rule DynPDG_path_ddep)
with ‹nx -asx→⇩d* n''› have "nx -asx@as''→⇩d* n'"
by -(rule DynPDG_path_Append)
with ‹V' ∈ Use (sourcenode a)› ‹sourcenode a -a#as'→⇩c⇩d nx› notExit
show ?case by(fastforce intro:dependent_live_vars.dep_vars_Cons_cdep)
next
case (dep_vars_Cons_ddep V as' as V' a)
from ‹as'' ≠ []› ‹last(targetnodes as'') = n'›
have "n' = last(targetnodes ((a#as)@as''))"
with dep_vars_Cons_ddep
show ?case by(fastforce intro:dependent_live_vars.dep_vars_Cons_ddep)
next
case (dep_vars_Cons_keep V as' as a)
from ‹as'' ≠ []› ‹last(targetnodes as'') = n'›
have "n' = last(targetnodes ((a#as)@as''))"
with dep_vars_Cons_keep
show ?case by(fastforce intro:dependent_live_vars.dep_vars_Cons_keep)
qed
qed

lemma dependent_live_vars_dep_dependent_live_vars:
"⟦n'' -as''→⇩d* n'; (V',as',as) ∈ dependent_live_vars n''⟧
⟹ (V',as',as@as'') ∈ dependent_live_vars n'"
proof(induct rule:DynPDG_path.induct)
case (DynPDG_path_Nil n) thus ?case by simp
next
case (DynPDG_path_Append_cdep n asx n'' asx' n')
note IH = ‹(V', as', as) ∈ dependent_live_vars n ⟹
(V', as', as @ asx) ∈ dependent_live_vars n''›
from IH[OF ‹(V',as',as) ∈ dependent_live_vars n›]
have "(V',as',as@asx) ∈ dependent_live_vars n''" .
with ‹n'' -asx'→⇩c⇩d n'› have "(V',as',(as@asx)@asx') ∈ dependent_live_vars n'"
by(rule dependent_live_vars_cdep_dependent_live_vars)
thus ?case by simp
next
case (DynPDG_path_Append_ddep n asx n'' V asx' n')
note IH = ‹(V', as', as) ∈ dependent_live_vars n ⟹
(V', as', as @ asx) ∈ dependent_live_vars n''›
from IH[OF ‹(V',as',as) ∈ dependent_live_vars n›]
have "(V',as',as@asx) ∈ dependent_live_vars n''" .
with ‹n'' -{V}asx'→⇩d⇩d n'› have "(V',as',(as@asx)@asx') ∈ dependent_live_vars n'"
by(rule dependent_live_vars_ddep_dependent_live_vars)
thus ?case by simp
qed

end

end


# Theory BitVector

section ‹Formalization of Bit Vectors›

theory BitVector imports Main begin

type_synonym bit_vector = "bool list"

fun bv_leqs :: "bit_vector ⇒ bit_vector ⇒ bool" ("_ ≼⇩b _" 99)
where bv_Nils:"[] ≼⇩b [] = True"
| bv_Cons:"(x#xs) ≼⇩b (y#ys) = ((x ⟶ y) ∧ xs ≼⇩b ys)"
| bv_rest:"xs ≼⇩b ys = False"

subsection ‹Some basic properties›

lemma bv_length: "xs ≼⇩b ys ⟹ length xs = length ys"
by(induct rule:bv_leqs.induct)auto

lemma [dest!]: "xs ≼⇩b [] ⟹ xs = []"
by(induct xs) auto

lemma bv_leqs_AppendI:
"⟦xs ≼⇩b ys; xs' ≼⇩b ys'⟧ ⟹ (xs@xs') ≼⇩b (ys@ys')"
by(induct xs ys rule:bv_leqs.induct,auto)

lemma bv_leqs_AppendD:
"⟦(xs@xs') ≼⇩b (ys@ys'); length xs = length ys⟧
⟹ xs ≼⇩b ys ∧ xs' ≼⇩b ys'"
by(induct xs ys rule:bv_leqs.induct,auto)

lemma bv_leqs_eq:
"xs ≼⇩b ys = ((∀i < length xs. xs ! i ⟶ ys ! i) ∧ length xs = length ys)"
proof(induct xs ys rule:bv_leqs.induct)
case (2 x xs y ys)
note eq = ‹xs ≼⇩b ys =
((∀i < length xs. xs ! i ⟶ ys ! i) ∧ length xs = length ys)›
show ?case
proof
assume leqs:"x#xs ≼⇩b y#ys"
with eq have "x ⟶ y" and "∀i < length xs. xs ! i ⟶ ys ! i"
and "length xs = length ys" by simp_all
from ‹x ⟶ y› have "(x#xs) ! 0 ⟶ (y#ys) ! 0" by simp
{ fix i assume "i > 0" and "i < length (x#xs)"
then obtain j where "i = Suc j" and "j < length xs" by(cases i) auto
with ‹∀i < length xs. xs ! i ⟶ ys ! i›
have "(x#xs) ! i ⟶ (y#ys) ! i" by auto }
hence "∀i < length (x#xs). i > 0 ⟶ (x#xs) ! i ⟶ (y#ys) ! i" by simp
with ‹(x#xs) ! 0 ⟶ (y#ys) ! 0› ‹length xs = length ys›
show "(∀i < length (x#xs). (x#xs) ! i ⟶ (y#ys) ! i) ∧
length (x#xs) = length (y#ys)"
by clarsimp(case_tac "i>0",auto)
next
assume "(∀i < length (x#xs). (x#xs) ! i ⟶ (y#ys) ! i) ∧
length (x#xs) = length (y#ys)"
hence "∀i < length (x#xs). (x#xs) ! i ⟶ (y#ys) ! i"
and "length (x#xs) = length (y#ys)" by simp_all
from ‹∀i < length (x#xs). (x#xs) ! i ⟶ (y#ys) ! i›
have "∀i < length xs. xs ! i ⟶ ys ! i"
by clarsimp(erule_tac x="Suc i" in allE,auto)
with eq ‹length (x#xs) = length (y#ys)› have "xs ≼⇩b ys" by simp
from ‹∀i < length (x#xs). (x#xs) ! i ⟶ (y#ys) ! i›
have "x ⟶ y" by(erule_tac x="0" in allE) simp
with ‹xs ≼⇩b ys› show "x#xs ≼⇩b y#ys" by simp
qed
qed simp_all

subsection ‹$\preceq_b$ is an order on bit vectors with minimal and
maximal element›

lemma minimal_element:
"replicate (length xs) False ≼⇩b xs"
by(induct xs) auto

lemma maximal_element:
"xs ≼⇩b replicate (length xs) True"
by(induct xs) auto

lemma bv_leqs_refl:"xs ≼⇩b xs"
by(induct xs) auto

lemma bv_leqs_trans:"⟦xs ≼⇩b ys; ys ≼⇩b zs⟧ ⟹ xs ≼⇩b zs"
proof(induct xs ys arbitrary:zs rule:bv_leqs.induct)
case (2 x xs y ys)
note IH = ‹⋀zs. ⟦xs ≼⇩b ys; ys ≼⇩b zs⟧ ⟹ xs ≼⇩b zs›
from ‹(x#xs) ≼⇩b (y#ys)› have "xs ≼⇩b ys" and "x ⟶ y" by simp_all
from ‹(y#ys) ≼⇩b zs› obtain z zs' where "zs = z#zs'" by(cases zs) auto
with ‹(y#ys) ≼⇩b zs› have "ys ≼⇩b zs'" and "y ⟶ z" by simp_all
from IH[OF ‹xs ≼⇩b ys› ‹ys ≼⇩b zs'›] have "xs ≼⇩b zs'" .
with ‹x ⟶ y› ‹y ⟶ z› ‹zs = z#zs'› show ?case by simp
qed simp_all

lemma bv_leqs_antisym:"⟦xs ≼⇩b ys; ys ≼⇩b xs⟧ ⟹ xs = ys"
by(induct xs ys rule:bv_leqs.induct)auto

definition bv_less :: "bit_vector ⇒ bit_vector ⇒ bool" ("_ ≺⇩b _" 99)
where "xs ≺⇩b ys ≡ xs ≼⇩b ys ∧ xs ≠ ys"

interpretation order "bv_leqs" "bv_less"
by(unfold_locales,
auto intro:bv_leqs_refl bv_leqs_trans bv_leqs_antisym simp:bv_less_def)

end


# Theory DynSlice

section ‹Dynamic Backward Slice›

theory DynSlice imports DependentLiveVariables BitVector "../Basic/SemanticsCFG" begin

subsection ‹Backward slice of paths›

context DynPDG begin

fun slice_path :: "'edge list ⇒ bit_vector"
where "slice_path [] = []"
| "slice_path (a#as) = (let n' = last(targetnodes (a#as)) in
(sourcenode a -a#as→⇩d* n')#slice_path as)"

(*<*)declare Let_def [simp](*>*)

lemma slice_path_length:
"length(slice_path as) = length as"
by(induct as) auto

lemma slice_path_right_Cons:
assumes slice:"slice_path as = x#xs"
obtains a' as' where "as = a'#as'" and "slice_path as' = xs"
proof(atomize_elim)
from slice show "∃a' as'. as = a'#as' ∧ slice_path as' = xs"
by(induct as) auto
qed

subsection ‹The proof of the fundamental property of (dynamic) slicing›

fun select_edge_kinds :: "'edge list ⇒ bit_vector ⇒ 'state edge_kind list"
where "select_edge_kinds [] [] = []"
| "select_edge_kinds (a#as) (b#bs) = (if b then kind a
else (case kind a of ⇑f ⇒ ⇑id | (Q)⇩√ ⇒ (λs. True)⇩√))#select_edge_kinds as bs"

definition slice_kinds :: "'edge list ⇒ 'state edge_kind list"
where "slice_kinds as = select_edge_kinds as (slice_path as)"

lemma select_edge_kinds_max_bv:
"select_edge_kinds as (replicate (length as) True) = kinds as"
by(induct as,auto simp:kinds_def)

lemma slice_path_leqs_information_same_Uses:
"⟦n -as→* n'; bs ≼⇩b bs'; slice_path as = bs;
select_edge_kinds as bs = es; select_edge_kinds as bs' = es';
∀V xs. (V,xs,as) ∈ dependent_live_vars n' ⟶ state_val s V = state_val s' V;
preds es' s'⟧
⟹ (∀V ∈ Use n'. state_val (transfers es s) V =
state_val (transfers es' s') V) ∧ preds es s"
proof(induct bs bs' arbitrary:as es es' n s s' rule:bv_leqs.induct)
case 1
from ‹slice_path as = []› have "as = []" by(cases as) auto
with ‹select_edge_kinds as [] = es› ‹select_edge_kinds as [] = es'›
have "es = []" and "es' = []" by simp_all
{ fix V assume "V ∈ Use n'"
hence "(V,[],[]) ∈ dependent_live_vars n'" by(rule dep_vars_Use)
with ‹∀V xs. (V,xs,as) ∈ dependent_live_vars n' ⟶
state_val s V = state_val s' V› ‹V ∈ Use n'› ‹as = []›
have "state_val s V = state_val s' V" by blast }
with ‹es = []› ‹es' = []› show ?case by simp
next
case (2 x xs y ys)
note all = ‹∀V xs. (V,xs,as) ∈ dependent_live_vars n' ⟶
state_val s V = state_val s' V›
note IH = ‹⋀as es es' n s s'. ⟦n -as→* n'; xs ≼⇩b ys; slice_path as = xs;
select_edge_kinds as xs = es; select_edge_kinds as ys = es';
∀V xs. (V,xs,as) ∈ dependent_live_vars n' ⟶
state_val s V = state_val s' V;
preds es' s'⟧
⟹ (∀V ∈ Use n'. state_val (transfers es s) V =
state_val (transfers es' s') V) ∧ preds es s›
from ‹x#xs ≼⇩b y#ys› have "x ⟶ y" and "xs ≼⇩b ys" by simp_all
from ‹slice_path as = x#xs› obtain a' as' where "as = a'#as'"
and "slice_path as' = xs" by(erule slice_path_right_Cons)
from ‹as = a'#as'› ‹select_edge_kinds as (x#xs) = es›
obtain ex esx where "es = ex#esx"
and ex:"ex = (if x then kind a'
else (case kind a' of ⇑f ⇒ ⇑id | (Q)⇩√ ⇒ (λs. True)⇩√))"
and "select_edge_kinds as' xs = esx" by auto
from ‹as = a'#as'› ‹select_edge_kinds as (y#ys) = es'› obtain ex' esx'
where "es' = ex'#esx'"
and ex':"ex' = (if y then kind a'
else (case kind a' of ⇑f ⇒ ⇑id | (Q)⇩√ ⇒ (λs. True)⇩√))"
and "select_edge_kinds as' ys = esx'" by auto
from ‹n -as→* n'› ‹as = a'#as'› have [simp]:"n = sourcenode a'"
and "valid_edge a'" and "targetnode a' -as'→* n'"
by(auto elim:path_split_Cons)
from ‹n -as→* n'› ‹as = a'#as'› have "last(targetnodes as) = n'"
by(fastforce intro:path_targetnode)
from ‹preds es' s'› ‹es' = ex'#esx'› have "pred ex' s'"
and "preds esx' (transfer ex' s')" by simp_all
show ?case
proof(cases "as' = []")
case True
hence [simp]:"as' = []" by simp
with ‹slice_path as' = xs› ‹xs ≼⇩b ys›
have [simp]:"xs = [] ∧ ys = []" by auto(cases ys,auto)+
with ‹select_edge_kinds as' xs = esx› ‹select_edge_kinds as' ys = esx'›
have [simp]:"esx = []" and [simp]:"esx' = []" by simp_all
from True ‹targetnode a' -as'→* n'›
have [simp]:"n' = targetnode a'" by(auto elim:path.cases)
show ?thesis
proof(cases x)
case True
with ‹x ⟶ y› ex ex' have [simp]:"ex = kind a' ∧ ex' = kind a'" by simp
have "pred ex s"
proof(cases ex)
case (Predicate Q)
with ex ex' True ‹x ⟶ y› have [simp]:"transfer ex s = s"
and [simp]:"transfer ex' s' = s'"
by(cases "kind a'",auto)+
show ?thesis
proof(cases "n -[a']→⇩c⇩d n'")
case True
{ fix V' assume "V' ∈ Use n"
with True ‹valid_edge a'›
have "(V',[],a'#[]@[]) ∈ dependent_live_vars n'"
by(fastforce intro:dep_vars_Cons_cdep DynPDG_path_Nil
simp:targetnodes_def)
with all ‹as = a'#as'› have "state_val s V' = state_val s' V'"
by fastforce }
with ‹pred ex' s'› ‹valid_edge a'›
show ?thesis by(fastforce elim:CFG_edge_Uses_pred_equal)
next
case False
from ex True Predicate have "kind a' = (Q)⇩√" by(auto split:if_split_asm)
from True ‹slice_path as = x#xs› ‹as = a'#as'› have "n -[a']→⇩d* n'"
by(auto simp:targetnodes_def)
thus ?thesis
proof(induct rule:DynPDG_path.cases)
case (DynPDG_path_Nil nx)
hence False by simp
thus ?case by simp
next
case (DynPDG_path_Append_cdep nx asx n'' asx' nx')
from ‹[a'] = asx@asx'›
have "(asx = [a'] ∧ asx' = []) ∨ (asx = [] ∧ asx' = [a'])"
by (cases asx) auto
hence False
proof
assume "asx = [a'] ∧ asx' = []"
with ‹n'' -asx'→⇩c⇩d nx'› show False
by(fastforce elim:DynPDG_edge.cases dest:dyn_control_dependence_path)
next
assume "asx = [] ∧ asx' = [a']"
with ‹nx -asx→⇩d* n''› have "nx = n''" and "asx' = [a']"
by(auto intro:DynPDG_empty_path_eq_nodes)
with ‹n = nx› ‹n' = nx'› ‹n'' -asx'→⇩c⇩d nx'› False
show False by simp
qed
thus ?thesis by simp
next
case (DynPDG_path_Append_ddep nx asx n'' V asx' nx')
from ‹[a'] = asx@asx'›
have "(asx = [a'] ∧ asx' = []) ∨ (asx = [] ∧ asx' = [a'])"
by (cases asx) auto
thus ?case
proof
assume "asx = [a'] ∧ asx' = []"
with ‹n'' -{V}asx'→⇩d⇩d nx'› have False
by(fastforce elim:DynPDG_edge.cases simp:dyn_data_dependence_def)
thus ?thesis by simp
next
assume "asx = [] ∧ asx' = [a']"
with ‹nx -asx→⇩d* n''› have "nx = n''"
{ fix V' assume "V' ∈ Use n"
from ‹n'' -{V}asx'→⇩d⇩d nx'› ‹asx = [] ∧ asx' = [a']› ‹n' = nx'›
have "(V,[],[]) ∈ dependent_live_vars n'"
by(fastforce intro:dep_vars_Use elim:DynPDG_edge.cases
simp:dyn_data_dependence_def)
with ‹V' ∈ Use n› ‹n'' -{V}asx'→⇩d⇩d nx'› ‹asx = [] ∧ asx' = [a']›
‹n = nx› ‹nx = n''› ‹n' = nx'›
have "(V',[],[a']) ∈ dependent_live_vars n'"
by(auto elim:dep_vars_Cons_ddep simp:targetnodes_def)
with all ‹as = a'#as'› have "state_val s V' = state_val s' V'"
by fastforce }
with ‹pred ex' s'› ‹valid_edge a'› ex ex' True ‹x ⟶ y› show ?thesis
by(fastforce elim:CFG_edge_Uses_pred_equal)
qed
qed
qed
qed simp
{ fix V assume "V ∈ Use n'"
from ‹V ∈ Use n'› have "(V,[],[]) ∈ dependent_live_vars n'"
by(rule dep_vars_Use)
have "state_val (transfer ex s) V = state_val (transfer ex' s') V"
proof(cases "n -{V}[a']→⇩d⇩d n'")
case True
hence "V ∈ Def n"
by(auto elim:DynPDG_edge.cases simp:dyn_data_dependence_def)
have "⋀V. V ∈ Use n ⟹ state_val s V = state_val s' V"
proof -
fix V' assume "V' ∈ Use n"
with ‹(V,[],[]) ∈ dependent_live_vars n'› True
have "(V',[],[a']) ∈ dependent_live_vars n'"
by(fastforce intro:dep_vars_Cons_ddep simp:targetnodes_def)
with all ‹as = a'#as'› show "state_val s V' = state_val s' V'" by auto
qed
with ‹valid_edge a'› ‹pred ex' s'› ‹pred ex s›
have "∀V ∈ Def n. state_val (transfer (kind a') s) V =
state_val (transfer (kind a') s') V"
by simp(rule CFG_edge_transfer_uses_only_Use,auto)
with ‹V ∈ Def n› have "state_val (transfer (kind a') s) V =
state_val (transfer (kind a') s') V"
by simp
thus ?thesis by fastforce
next
case False
with ‹last(targetnodes as) = n'› ‹as = a'#as'›
‹(V,[],[]) ∈ dependent_live_vars n'›
have "(V,[a'],[a']) ∈ dependent_live_vars n'"
by(fastforce intro:dep_vars_Cons_keep)
from ‹(V,[a'],[a']) ∈ dependent_live_vars n'› all ‹as = a'#as'›
have states_eq:"state_val s V = state_val s' V"
by auto
from ‹valid_edge a'› ‹V ∈ Use n'› False ‹pred ex s›
have "state_val (transfers (kinds [a']) s) V = state_val s V"
apply(auto intro!:no_ddep_same_state path_edge simp:targetnodes_def)
by(case_tac as',auto)
moreover
from ‹valid_edge a'› ‹V ∈ Use n'› False ‹pred ex' s'›
have "state_val (transfers (kinds [a']) s') V = state_val s' V"
apply(auto intro!:no_ddep_same_state path_edge simp:targetnodes_def)
by(case_tac as',auto)
ultimately show ?thesis using states_eq by(auto simp:kinds_def)
qed }
hence "∀V ∈ Use n'. state_val (transfer ex s) V =
state_val (transfer ex' s') V" by simp
with ‹pred ex s› ‹es = ex#esx› ‹es' = ex'#esx'› show ?thesis by simp
next
case False
with ex have cases_x:"ex = (case kind a' of ⇑f ⇒ ⇑id | (Q)⇩√ ⇒ (λs. True)⇩√)"
by simp
from cases_x have "pred ex s" by(cases "kind a'",auto)
show ?thesis
proof(cases y)
case True
with ex' have [simp]:"ex' = kind a'" by simp
{ fix V assume "V ∈ Use n'"
from ‹V ∈ Use n'› have "(V,[],[]) ∈ dependent_live_vars n'"
by(rule dep_vars_Use)
from ‹slice_path as = x#xs› ‹as = a'#as'› ‹¬ x›
have "¬ n -[a']→⇩d* n'" by(simp add:targetnodes_def)
hence "¬ n -{V}[a']→⇩d⇩d n'" by(fastforce dest:DynPDG_path_ddep)
with ‹last(targetnodes as) = n'› ‹as = a'#as'›
‹(V,[],[]) ∈ dependent_live_vars n'›
have "(V,[a'],[a']) ∈ dependent_live_vars n'"
by(fastforce intro:dep_vars_Cons_keep)
with all ‹as = a'#as'› have "state_val s V = state_val s' V" by auto
from ‹valid_edge a'› ‹V ∈ Use n'› ‹pred ex' s'›
‹¬ n -{V}[a']→⇩d⇩d n'› ‹last(targetnodes as) = n'› ‹as = a'#as'›
have "state_val (transfers (kinds [a']) s') V = state_val s' V"
apply(auto intro!:no_ddep_same_state path_edge)
by(case_tac as',auto)
with ‹state_val s V = state_val s' V› cases_x
have "state_val (transfer ex s) V =
state_val (transfer ex' s') V"
hence "∀V ∈ Use n'. state_val (transfer ex s) V =
state_val (transfer ex' s') V" by simp
with ‹as = a'#as'› ‹es = ex#esx› ‹es' = ex'#esx'› ‹pred ex s›
show ?thesis by simp
next
case False
with ex' have cases_y:"ex' = (case kind a' of ⇑f ⇒ ⇑id | (Q)⇩√ ⇒ (λs. True)⇩√)"
by simp
with cases_x have [simp]:"ex = ex'" by(cases "kind a'") auto
{ fix V assume "V ∈ Use n'"
from ‹V ∈ Use n'› have "(V,[],[]) ∈ dependent_live_vars n'"
by(rule dep_vars_Use)
from ‹slice_path as = x#xs› ‹as = a'#as'› ‹¬ x›
have "¬ n -[a']→⇩d* n'" by(simp add:targetnodes_def)
hence no_dep:"¬ n -{V}[a']→⇩d⇩d n'" by(fastforce dest:DynPDG_path_ddep)
with ‹last(targetnodes as) = n'› ‹as = a'#as'›
‹(V,[],[]) ∈ dependent_live_vars n'›
have "(V,[a'],[a']) ∈ dependent_live_vars n'"
by(fastforce intro:dep_vars_Cons_keep)
with all ‹as = a'#as'› have "state_val s V = state_val s' V" by auto }
with ‹as = a'#as'› cases_x ‹es = ex#esx› ‹es' = ex'#esx'› ‹pred ex s›
show ?thesis by(cases "kind a'",auto)
qed
qed
next
case False
show ?thesis
proof(cases "∀V xs. (V,xs,as') ∈ dependent_live_vars n' ⟶
state_val (transfer ex s) V = state_val (transfer ex' s') V")
case True
hence imp':"∀V xs. (V,xs,as') ∈ dependent_live_vars n' ⟶
state_val (transfer ex s) V = state_val (transfer ex' s') V" .
from IH[OF ‹targetnode a' -as'→* n'› ‹xs ≼⇩b ys› ‹slice_path as' = xs›
‹select_edge_kinds as' xs = esx› ‹select_edge_kinds as' ys = esx'›
this ‹preds esx' (transfer ex' s')›]
have all':"∀V∈Use n'. state_val (transfers esx (transfer ex s)) V =
state_val (transfers esx' (transfer ex' s')) V"
and "preds esx (transfer ex s)" by simp_all
have "pred ex s"
proof(cases ex)
case (Predicate Q)
with ‹slice_path as = x#xs› ‹as = a'#as'› ‹last(targetnodes as) = n'› ex
have "ex = (λs. True)⇩√ ∨ n -a'#as'→⇩d* n'"
by(cases "kind a'",auto split:if_split_asm)
thus ?thesis
proof
assume "ex = (λs. True)⇩√" thus ?thesis by simp
next
assume "n -a'#as'→⇩d* n'"
with ‹slice_path as = x#xs› ‹as = a'#as'› ‹last(targetnodes as) = n'› ex
have [simp]:"ex = kind a'" by clarsimp
with ‹x ⟶ y› ex ex' have [simp]:"ex' = ex" by(cases x) auto
from ‹n -a'#as'→⇩d* n'› show ?thesis
proof(induct rule:DynPDG_path_rev_cases)
case DynPDG_path_Nil
hence False by simp
thus ?thesis by simp
`