Theory CDepInstantiations

Up to index of Isabelle/HOL/Jinja/Slicing

theory CDepInstantiations
imports Slice PDG WeakOrderDependence
header {* \isaheader{Instantiate framework with control dependences} *}

theory CDepInstantiations imports
Slice
PDG
WeakOrderDependence
begin

subsection{* Standard control dependence *}

context StandardControlDependencePDG begin

lemma Exit_in_obs_slice_node:"(_Exit_) ∈ obs n' (PDG_BS S) ==> (_Exit_) ∈ S"
by(auto elim:obsE PDG_path_CFG_path simp:PDG_BS_def split:split_if_asm)


abbreviation PDG_path' :: "'node => 'node => bool" ("_ -->d* _" [51,0] 80)
where "n -->d* n' ≡ PDG.PDG_path sourcenode targetnode valid_edge Def Use
standard_control_dependence n n'"


lemma cd_closed:
"[|n' ∈ PDG_BS S; n controlss n'|] ==> n ∈ PDG_BS S"
by(simp add:PDG_BS_def)(blast dest:PDG_cdep_edge PDG_path_Append PDG_path_cdep)


lemma obs_postdominate:
assumes "n ∈ obs n' (PDG_BS S)" and "n ≠ (_Exit_)" shows "n postdominates n'"
proof(rule ccontr)
assume "¬ n postdominates n'"
from `n ∈ obs n' (PDG_BS S)` have "valid_node n" by(fastforce dest:in_obs_valid)
with `n ∈ obs n' (PDG_BS S)` `n ≠ (_Exit_)` have "n postdominates n"
by(fastforce intro:postdominate_refl)
from `n ∈ obs n' (PDG_BS S)` obtain as where "n' -as->* n"
and "∀n' ∈ set(sourcenodes as). n' ∉ (PDG_BS S)"
and "n ∈ (PDG_BS S)" by(erule obsE)
from `n postdominates n` `¬ n postdominates n'` `n' -as->* n`
obtain as' a as'' where [simp]:"as = as'@a#as''" and "valid_edge a"
and "¬ n postdominates (sourcenode a)" and "n postdominates (targetnode a)"
by -(erule postdominate_path_branch)
from `¬ n postdominates (sourcenode a)` `valid_edge a` `valid_node n`
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)
apply simp_all
by fastforce
with `sourcenode a -asx->* (_Exit_)` have "sourcenode a -[]@ax#asx'->* (_Exit_)"
by simp
hence "valid_edge ax" and [simp]:"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)
from `n ∈ obs n' (PDG_BS S)` `∀n' ∈ set(sourcenodes as). n' ∉ (PDG_BS S)`
have "n ∉ set (sourcenodes (a#as''))"
by(fastforce elim:obs.cases simp:sourcenodes_def)
from `n' -as->* n` have "sourcenode a -a#as''->* n"
by(fastforce dest:path_split_second)
with `n postdominates (targetnode a)` `¬ n postdominates targetnode ax`
`valid_edge ax` `n ∉ set (sourcenodes (a#as''))`
have "sourcenode a controlss n" by(fastforce simp:standard_control_dependence_def)
with `n ∈ obs n' (PDG_BS S)` have "sourcenode a ∈ (PDG_BS S)"
by(fastforce intro:cd_closed PDG_cdep_edge elim:obs.cases)
with `∀n' ∈ set(sourcenodes as). n' ∉ (PDG_BS S)`
show False by(simp add:sourcenodes_def)
qed


lemma obs_singleton:"(∃m. obs n (PDG_BS S) = {m}) ∨ obs n (PDG_BS S) = {}"
proof(rule ccontr)
assume "¬ ((∃m. obs n (PDG_BS S) = {m}) ∨ obs n (PDG_BS S) = {})"
hence "∃nx nx'. nx ∈ obs n (PDG_BS S) ∧ nx' ∈ obs n (PDG_BS S) ∧
nx ≠ nx'"
by auto
then obtain nx nx' where "nx ∈ obs n (PDG_BS S)" and "nx' ∈ obs n (PDG_BS S)"
and "nx ≠ nx'" by auto
from `nx ∈ obs n (PDG_BS S)` obtain as where "n -as->* nx"
and "∀n' ∈ set(sourcenodes as). n' ∉ (PDG_BS S)" and "nx ∈ (PDG_BS S)"
by(erule obsE)
from `n -as->* nx` have "valid_node nx" by(fastforce dest:path_valid_node)
with `nx ∈ (PDG_BS S)` have "obs nx (PDG_BS S) = {nx}" by -(rule n_in_obs)
with `n -as->* nx` `nx ∈ obs n (PDG_BS S)` `nx' ∈ obs n (PDG_BS S)` `nx ≠ nx'`
have "as ≠ []" by(fastforce elim:path.cases)
with `n -as->* nx` `nx ∈ obs n (PDG_BS S)` `nx' ∈ obs n (PDG_BS S)`
`nx ≠ nx'` `obs nx (PDG_BS S) = {nx}` `∀n' ∈ set(sourcenodes as). n' ∉ (PDG_BS S)`
have "∃a as' as''. n -as'->* sourcenode a ∧ targetnode a -as''->* nx ∧
valid_edge a ∧ as = as'@a#as'' ∧
obs (targetnode a) (PDG_BS S) = {nx} ∧
(¬ (∃m. obs (sourcenode a) (PDG_BS S) = {m} ∨
obs (sourcenode a) (PDG_BS S) = {}))"

proof(induct arbitrary:nx' rule:path.induct)
case (Cons_path n'' as n' a n)
note [simp] = `sourcenode a = n`[THEN sym] `targetnode a = n''`[THEN sym]
note more_than_one = `n' ∈ obs n (PDG_BS S)` `nx' ∈ obs n (PDG_BS S)` `n' ≠ nx'`
note IH = `!!nx'. [|n' ∈ obs n'' (PDG_BS S); nx' ∈ obs n'' (PDG_BS S); n' ≠ nx';
obs n' (PDG_BS S) = {n'}; ∀n'∈set (sourcenodes as). n' ∉ (PDG_BS S); as ≠ []|]
==> ∃a as' as''. n'' -as'->* sourcenode a ∧ targetnode a -as''->* n' ∧
valid_edge a ∧ as = as'@a#as'' ∧ obs (targetnode a) (PDG_BS S) = {n'} ∧
(¬ (∃m. obs (sourcenode a) (PDG_BS S) = {m} ∨
obs (sourcenode a) (PDG_BS S) = {}))`

from `∀n'∈set (sourcenodes (a#as)). n' ∉ (PDG_BS S)`
have "∀n'∈set (sourcenodes as). n' ∉ (PDG_BS S)" and "sourcenode a ∉ (PDG_BS S)"
by(simp_all add:sourcenodes_def)
show ?case
proof(cases "as = []")
case True
with `n'' -as->* n'` have [simp]:"n' = n''" by(fastforce elim:path.cases)
from more_than_one
have "¬ (∃m. obs (sourcenode a) (PDG_BS S) = {m} ∨
obs (sourcenode a) (PDG_BS S) = {})"

by auto
with `obs n' (PDG_BS S) = {n'}` True `valid_edge a` show ?thesis
apply(rule_tac x="a" in exI)
apply(rule_tac x="[]" in exI)
apply(rule_tac x="[]" in exI)
by(auto intro!:empty_path)
next
case False
hence "as ≠ []" .
from `n'' -as->* n'` `∀n'∈set (sourcenodes as). n' ∉ (PDG_BS S)`
have "obs n' (PDG_BS S) ⊆ obs n'' (PDG_BS S)" by(rule path_obs_subset)
show ?thesis
proof(cases "obs n' (PDG_BS S) = obs n'' (PDG_BS S)")
case True
with `n'' -as->* n'` `valid_edge a` `obs n' (PDG_BS S) = {n'}` more_than_one
show ?thesis
apply(rule_tac x="a" in exI)
apply(rule_tac x="[]" in exI)
apply(rule_tac x="as" in exI)
by(fastforce intro:empty_path)
next
case False
with `obs n' (PDG_BS S) ⊆ obs n'' (PDG_BS S)`
have "obs n' (PDG_BS S) ⊂ obs n'' (PDG_BS S)" by simp
with `obs n' (PDG_BS S) = {n'}` obtain ni where "n' ∈ obs n'' (PDG_BS S)"
and "ni ∈ obs n'' (PDG_BS S)" and "n' ≠ ni" by auto
from IH[OF this `obs n' (PDG_BS S) = {n'}`
`∀n'∈set (sourcenodes as). n' ∉ (PDG_BS S)` `as ≠ []`] obtain a' as' as''
where "n'' -as'->* sourcenode a'" and "targetnode a' -as''->* n'"
and "valid_edge a'" and [simp]:"as = as'@a'#as''"
and "obs (targetnode a') (PDG_BS S) = {n'}"
and more_than_one':"¬ (∃m. obs (sourcenode a') (PDG_BS S) = {m} ∨
obs (sourcenode a') (PDG_BS S) = {})"

by blast
from `n'' -as'->* sourcenode a'` `valid_edge a`
have "n -a#as'->* sourcenode a'" by(fastforce intro:path.Cons_path)
with `targetnode a' -as''->* n'` `obs (targetnode a') (PDG_BS S) = {n'}`
more_than_one' `valid_edge a'` show ?thesis
apply(rule_tac x="a'" in exI)
apply(rule_tac x="a#as'" in exI)
apply(rule_tac x="as''" in exI)
by fastforce
qed
qed
qed simp
then obtain a as' as'' where "valid_edge a"
and "obs (targetnode a) (PDG_BS S) = {nx}"
and more_than_one:"¬ (∃m. obs (sourcenode a) (PDG_BS S) = {m} ∨
obs (sourcenode a) (PDG_BS S) = {})"

by blast
have "sourcenode a ∉ (PDG_BS S)"
proof(rule ccontr)
assume "¬ sourcenode a ∉ PDG_BS S"
hence "sourcenode a ∈ PDG_BS S" by simp
with `valid_edge a` have "obs (sourcenode a) (PDG_BS S) = {sourcenode a}"
by(fastforce intro!:n_in_obs)
with more_than_one show False by simp
qed
with `valid_edge a`
have "obs (targetnode a) (PDG_BS S) ⊆ obs (sourcenode a) (PDG_BS S)"
by(rule edge_obs_subset)
with `obs (targetnode a) (PDG_BS S) = {nx}`
have "nx ∈ obs (sourcenode a) (PDG_BS S)" by simp
with more_than_one obtain m where "m ∈ obs (sourcenode a) (PDG_BS S)"
and "nx ≠ m" by auto
from `m ∈ obs (sourcenode a) (PDG_BS S)`
have "valid_node m" by(fastforce dest:in_obs_valid)
from `obs (targetnode a) (PDG_BS S) = {nx}` have "valid_node nx"
by(fastforce dest:in_obs_valid)
show False
proof(cases "m postdominates (sourcenode a)")
case True
with `nx ∈ obs (sourcenode a) (PDG_BS S)` `m ∈ obs (sourcenode a) (PDG_BS S)`
have "m postdominates nx"
by(fastforce intro:postdominate_path_targetnode elim:obs.cases)
with `nx ≠ m` have "¬ nx postdominates m" by(fastforce dest:postdominate_antisym)
have "(_Exit_) -[]->* (_Exit_)" by(fastforce intro:empty_path)
with `m postdominates nx` have "nx ≠ (_Exit_)"
by(fastforce simp:postdominate_def sourcenodes_def)
have "¬ nx postdominates (sourcenode a)"
proof(rule ccontr)
assume "¬ ¬ nx postdominates sourcenode a"
hence "nx postdominates sourcenode a" by simp
from `m ∈ obs (sourcenode a) (PDG_BS S)` `nx ∈ obs (sourcenode a) (PDG_BS S)`
obtain asx' where "sourcenode a -asx'->* m" and "nx ∉ set(sourcenodes asx')"
by(fastforce elim:obs.cases)
with `nx postdominates sourcenode a` have "nx postdominates m"
by(rule postdominate_path_targetnode)
with `¬ nx postdominates m` show False by simp
qed
with `nx ∈ obs (sourcenode a) (PDG_BS S)` `valid_node nx` `nx ≠ (_Exit_)`
show False by(fastforce dest:obs_postdominate)
next
case False
show False
proof(cases "m = Exit")
case True
from `m ∈ obs (sourcenode a) (PDG_BS S)` `nx ∈ obs (sourcenode a) (PDG_BS S)`
obtain xs where "sourcenode a -xs->* m" and "nx ∉ set(sourcenodes xs)"
by(fastforce elim:obsE)
obtain x' xs' where [simp]:"xs = x'#xs'"
proof(cases xs)
case Nil
with `sourcenode a -xs->* m` have [simp]:"sourcenode a = m" by fastforce
with `m ∈ obs (sourcenode a) (PDG_BS S)`
have "m ∈ (PDG_BS S)" by(fastforce elim:obsE)
with `valid_node m` have "obs m (PDG_BS S) = {m}"
by(rule n_in_obs)
with `nx ∈ obs (sourcenode a) (PDG_BS S)` `nx ≠ m` have False
by fastforce
thus ?thesis by simp
qed blast
from `sourcenode a -xs->* m` have "sourcenode a = sourcenode x'"
and "valid_edge x'" and "targetnode x' -xs'->* m"
by(auto elim:path_split_Cons)
from `targetnode x' -xs'->* m` `nx ∉ set(sourcenodes xs)` `valid_edge x'`
`valid_node m` True
have "¬ nx postdominates (targetnode x')"
by(fastforce simp:postdominate_def sourcenodes_def)
from `nx ≠ m` True have "nx ≠ (_Exit_)" by simp
with `obs (targetnode a) (PDG_BS S) = {nx}`
have "nx postdominates (targetnode a)"
by(fastforce intro:obs_postdominate)
from `obs (targetnode a) (PDG_BS S) = {nx}`
obtain ys where "targetnode a -ys->* nx"
and "∀nx' ∈ set(sourcenodes ys). nx' ∉ (PDG_BS S)"
and "nx ∈ (PDG_BS S)" by(fastforce elim:obsE)
hence "nx ∉ set(sourcenodes ys)"by fastforce
have "sourcenode a ≠ nx"
proof
assume "sourcenode a = nx"
from `nx ∈ obs (sourcenode a) (PDG_BS S)`
have "nx ∈ (PDG_BS S)" by -(erule obsE)
with `valid_node nx` have "obs nx (PDG_BS S) = {nx}" by -(erule n_in_obs)
with `sourcenode a = nx` `m ∈ obs (sourcenode a) (PDG_BS S)`
`nx ≠ m` show False by fastforce
qed
with `nx ∉ set(sourcenodes ys)` have "nx ∉ set(sourcenodes (a#ys))"
by(fastforce simp:sourcenodes_def)
from `valid_edge a` `targetnode a -ys->* nx`
have "sourcenode a -a#ys->* nx" by(fastforce intro:Cons_path)
from `sourcenode a -a#ys->* nx` `nx ∉ set(sourcenodes (a#ys))`
`nx postdominates (targetnode a)` `valid_edge x'`
`¬ nx postdominates (targetnode x')` `sourcenode a = sourcenode x'`
have "(sourcenode a) controlss nx"
by(fastforce simp:standard_control_dependence_def)
with `nx ∈ (PDG_BS S)` have "sourcenode a ∈ (PDG_BS S)"
by(rule cd_closed)
with `valid_edge a` have "obs (sourcenode a) (PDG_BS S) = {sourcenode a}"
by(fastforce intro!:n_in_obs)
with `m ∈ obs (sourcenode a) (PDG_BS S)`
`nx ∈ obs (sourcenode a) (PDG_BS S)` `nx ≠ m`
show False by simp
next
case False
with `m ∈ obs (sourcenode a) (PDG_BS S)` `valid_node m`
`¬ m postdominates sourcenode a`
show False by(fastforce dest:obs_postdominate)
qed
qed
qed


lemma PDGBackwardSliceCorrect:
"BackwardSlice sourcenode targetnode kind valid_edge
(_Entry_) Def Use state_val PDG_BS"

proof(unfold_locales)
fix n S assume "n ∈ PDG_BS S"
thus "valid_node n" by(rule PDG_BS_valid_node)
next
fix n S assume "valid_node n" and "n ∈ S"
thus "n ∈ PDG_BS S" by(fastforce intro:PDG_path_Nil simp:PDG_BS_def)
next
fix n' S n V
assume "n' ∈ PDG_BS S" and "n influences V in n'"
thus "n ∈ PDG_BS S"
by(auto dest:PDG.PDG_path_ddep[OF PDG_scd,OF PDG.PDG_ddep_edge[OF PDG_scd]]
dest:PDG_path_Append simp:PDG_BS_def split:split_if_asm)
next
fix n S
have "(∃m. obs n (PDG_BS S) = {m}) ∨ obs n (PDG_BS S) = {}"
by(rule obs_singleton)
thus "finite (obs n (PDG_BS S))" by fastforce
next
fix n S
have "(∃m. obs n (PDG_BS S) = {m}) ∨ obs n (PDG_BS S) = {}"
by(rule obs_singleton)
thus "card (obs n (PDG_BS S)) ≤ 1" by fastforce
qed

end


subsection{* Weak control dependence *}

context WeakControlDependencePDG begin

lemma Exit_in_obs_slice_node:"(_Exit_) ∈ obs n' (PDG_BS S) ==> (_Exit_) ∈ S"
by(auto elim:obsE PDG_path_CFG_path simp:PDG_BS_def split:split_if_asm)


lemma cd_closed:
"[|n' ∈ PDG_BS S; n weakly controls n'|] ==> n ∈ PDG_BS S"
by(simp add:PDG_BS_def)(blast dest:PDG_cdep_edge PDG_path_Append PDG_path_cdep)


lemma obs_strong_postdominate:
assumes "n ∈ obs n' (PDG_BS S)" and "n ≠ (_Exit_)"
shows "n strongly-postdominates n'"
proof(rule ccontr)
assume "¬ n strongly-postdominates n'"
from `n ∈ obs n' (PDG_BS S)` have "valid_node n" by(fastforce dest:in_obs_valid)
with `n ∈ obs n' (PDG_BS S)` `n ≠ (_Exit_)` have "n strongly-postdominates n"
by(fastforce intro:strong_postdominate_refl)
from `n ∈ obs n' (PDG_BS S)` obtain as where "n' -as->* n"
and "∀n' ∈ set(sourcenodes as). n' ∉ (PDG_BS S)"
and "n ∈ (PDG_BS S)" by(erule obsE)
from `n strongly-postdominates n` `¬ n strongly-postdominates n'` `n' -as->* n`
obtain as' a as'' where [simp]:"as = as'@a#as''" and "valid_edge a"
and "¬ n strongly-postdominates (sourcenode a)" and
"n strongly-postdominates (targetnode a)"
by -(erule strong_postdominate_path_branch)
from `n ∈ obs n' (PDG_BS S)` `∀n' ∈ set(sourcenodes as). n' ∉ (PDG_BS S)`
have "n ∉ set (sourcenodes (a#as''))"
by(fastforce elim:obs.cases simp:sourcenodes_def)
from `n' -as->* n` have "sourcenode a -a#as''->* n"
by(fastforce dest:path_split_second)
from `¬ n strongly-postdominates (sourcenode a)` `valid_edge a` `valid_node n`
obtain a' where "sourcenode a' = sourcenode a"
and "valid_edge a'" and "¬ n strongly-postdominates (targetnode a')"
by(fastforce elim:not_strong_postdominate_predecessor_successor)
with `n strongly-postdominates (targetnode a)` `n ∉ set (sourcenodes (a#as''))`
`sourcenode a -a#as''->* n`
have "sourcenode a weakly controls n"
by(fastforce simp:weak_control_dependence_def)
with `n ∈ obs n' (PDG_BS S)` have "sourcenode a ∈ (PDG_BS S)"
by(fastforce intro:cd_closed PDG_cdep_edge elim:obs.cases)
with `∀n' ∈ set(sourcenodes as). n' ∉ (PDG_BS S)`
show False by(simp add:sourcenodes_def)
qed


lemma obs_singleton:"(∃m. obs n (PDG_BS S) = {m}) ∨ obs n (PDG_BS S) = {}"
proof(rule ccontr)
assume "¬ ((∃m. obs n (PDG_BS S) = {m}) ∨ obs n (PDG_BS S) = {})"
hence "∃nx nx'. nx ∈ obs n (PDG_BS S) ∧ nx' ∈ obs n (PDG_BS S) ∧
nx ≠ nx'"
by auto
then obtain nx nx' where "nx ∈ obs n (PDG_BS S)" and "nx' ∈ obs n (PDG_BS S)"
and "nx ≠ nx'" by auto
from `nx ∈ obs n (PDG_BS S)` obtain as where "n -as->* nx"
and "∀n' ∈ set(sourcenodes as). n' ∉ (PDG_BS S)" and "nx ∈ (PDG_BS S)"
by(erule obsE)
from `n -as->* nx` have "valid_node nx" by(fastforce dest:path_valid_node)
with `nx ∈ (PDG_BS S)` have "obs nx (PDG_BS S) = {nx}" by -(rule n_in_obs)
with `n -as->* nx` `nx ∈ obs n (PDG_BS S)` `nx' ∈ obs n (PDG_BS S)` `nx ≠ nx'`
have "as ≠ []" by(fastforce elim:path.cases)
with `n -as->* nx` `nx ∈ obs n (PDG_BS S)` `nx' ∈ obs n (PDG_BS S)`
`nx ≠ nx'` `obs nx (PDG_BS S) = {nx}` `∀n' ∈ set(sourcenodes as). n' ∉ (PDG_BS S)`
have "∃a as' as''. n -as'->* sourcenode a ∧ targetnode a -as''->* nx ∧
valid_edge a ∧ as = as'@a#as'' ∧
obs (targetnode a) (PDG_BS S) = {nx} ∧
(¬ (∃m. obs (sourcenode a) (PDG_BS S) = {m} ∨
obs (sourcenode a) (PDG_BS S) = {}))"

proof(induct arbitrary:nx' rule:path.induct)
case (Cons_path n'' as n' a n)
note [simp] = `sourcenode a = n`[THEN sym] `targetnode a = n''`[THEN sym]
note more_than_one = `n' ∈ obs n (PDG_BS S)` `nx' ∈ obs n (PDG_BS S)` `n' ≠ nx'`
note IH = `!!nx'. [|n' ∈ obs n'' (PDG_BS S); nx' ∈ obs n'' (PDG_BS S); n' ≠ nx';
obs n' (PDG_BS S) = {n'}; ∀n'∈set (sourcenodes as). n' ∉ (PDG_BS S); as ≠ []|]
==> ∃a as' as''. n'' -as'->* sourcenode a ∧ targetnode a -as''->* n' ∧
valid_edge a ∧ as = as'@a#as'' ∧ obs (targetnode a) (PDG_BS S) = {n'} ∧
(¬ (∃m. obs (sourcenode a) (PDG_BS S) = {m} ∨
obs (sourcenode a) (PDG_BS S) = {}))`

from `∀n'∈set (sourcenodes (a#as)). n' ∉ (PDG_BS S)`
have "∀n'∈set (sourcenodes as). n' ∉ (PDG_BS S)" and "sourcenode a ∉ (PDG_BS S)"
by(simp_all add:sourcenodes_def)
show ?case
proof(cases "as = []")
case True
with `n'' -as->* n'` have [simp]:"n' = n''" by(fastforce elim:path.cases)
from more_than_one
have "¬ (∃m. obs (sourcenode a) (PDG_BS S) = {m} ∨
obs (sourcenode a) (PDG_BS S) = {})"

by auto
with `obs n' (PDG_BS S) = {n'}` True `valid_edge a` show ?thesis
apply(rule_tac x="a" in exI)
apply(rule_tac x="[]" in exI)
apply(rule_tac x="[]" in exI)
by(auto intro!:empty_path)
next
case False
hence "as ≠ []" .
from `n'' -as->* n'` `∀n'∈set (sourcenodes as). n' ∉ (PDG_BS S)`
have "obs n' (PDG_BS S) ⊆ obs n'' (PDG_BS S)" by(rule path_obs_subset)
show ?thesis
proof(cases "obs n' (PDG_BS S) = obs n'' (PDG_BS S)")
case True
with `n'' -as->* n'` `valid_edge a` `obs n' (PDG_BS S) = {n'}` more_than_one
show ?thesis
apply(rule_tac x="a" in exI)
apply(rule_tac x="[]" in exI)
apply(rule_tac x="as" in exI)
by(fastforce intro:empty_path)
next
case False
with `obs n' (PDG_BS S) ⊆ obs n'' (PDG_BS S)`
have "obs n' (PDG_BS S) ⊂ obs n'' (PDG_BS S)" by simp
with `obs n' (PDG_BS S) = {n'}` obtain ni where "n' ∈ obs n'' (PDG_BS S)"
and "ni ∈ obs n'' (PDG_BS S)" and "n' ≠ ni" by auto
from IH[OF this `obs n' (PDG_BS S) = {n'}`
`∀n'∈set (sourcenodes as). n' ∉ (PDG_BS S)` `as ≠ []`] obtain a' as' as''
where "n'' -as'->* sourcenode a'" and "targetnode a' -as''->* n'"
and "valid_edge a'" and [simp]:"as = as'@a'#as''"
and "obs (targetnode a') (PDG_BS S) = {n'}"
and more_than_one':"¬ (∃m. obs (sourcenode a') (PDG_BS S) = {m} ∨
obs (sourcenode a') (PDG_BS S) = {})"

by blast
from `n'' -as'->* sourcenode a'` `valid_edge a`
have "n -a#as'->* sourcenode a'" by(fastforce intro:path.Cons_path)
with `targetnode a' -as''->* n'` `obs (targetnode a') (PDG_BS S) = {n'}`
more_than_one' `valid_edge a'` show ?thesis
apply(rule_tac x="a'" in exI)
apply(rule_tac x="a#as'" in exI)
apply(rule_tac x="as''" in exI)
by fastforce
qed
qed
qed simp
then obtain a as' as'' where "valid_edge a"
and "obs (targetnode a) (PDG_BS S) = {nx}"
and more_than_one:"¬ (∃m. obs (sourcenode a) (PDG_BS S) = {m} ∨
obs (sourcenode a) (PDG_BS S) = {})"

by blast
have "sourcenode a ∉ (PDG_BS S)"
proof(rule ccontr)
assume "¬ sourcenode a ∉ PDG_BS S"
hence "sourcenode a ∈ PDG_BS S" by simp
with `valid_edge a` have "obs (sourcenode a) (PDG_BS S) = {sourcenode a}"
by(fastforce intro!:n_in_obs)
with more_than_one show False by simp
qed
with `valid_edge a`
have "obs (targetnode a) (PDG_BS S) ⊆ obs (sourcenode a) (PDG_BS S)"
by(rule edge_obs_subset)
with `obs (targetnode a) (PDG_BS S) = {nx}`
have "nx ∈ obs (sourcenode a) (PDG_BS S)" by simp
with more_than_one obtain m where "m ∈ obs (sourcenode a) (PDG_BS S)"
and "nx ≠ m" by auto
from `m ∈ obs (sourcenode a) (PDG_BS S)`
have "valid_node m" by(fastforce dest:in_obs_valid)
from `obs (targetnode a) (PDG_BS S) = {nx}` have "valid_node nx"
by(fastforce dest:in_obs_valid)
show False
proof(cases "m strongly-postdominates (sourcenode a)")
case True
with `nx ∈ obs (sourcenode a) (PDG_BS S)` `m ∈ obs (sourcenode a) (PDG_BS S)`
have "m strongly-postdominates nx"
by(fastforce intro:strong_postdominate_path_targetnode elim:obs.cases)
with `nx ≠ m` have "¬ nx strongly-postdominates m"
by(fastforce dest:strong_postdominate_antisym)
have "(_Exit_) -[]->* (_Exit_)" by(fastforce intro:empty_path)
with `m strongly-postdominates nx` have "nx ≠ (_Exit_)"
by(fastforce simp:strong_postdominate_def sourcenodes_def postdominate_def)
have "¬ nx strongly-postdominates (sourcenode a)"
proof(rule ccontr)
assume "¬ ¬ nx strongly-postdominates sourcenode a"
hence "nx strongly-postdominates sourcenode a" by simp
from `m ∈ obs (sourcenode a) (PDG_BS S)` `nx ∈ obs (sourcenode a) (PDG_BS S)`
obtain asx' where "sourcenode a -asx'->* m" and "nx ∉ set(sourcenodes asx')"
by(fastforce elim:obs.cases)
with `nx strongly-postdominates sourcenode a` have "nx strongly-postdominates m"
by(rule strong_postdominate_path_targetnode)
with `¬ nx strongly-postdominates m` show False by simp
qed
with `nx ∈ obs (sourcenode a) (PDG_BS S)` `valid_node nx` `nx ≠ (_Exit_)`
show False by(fastforce dest:obs_strong_postdominate)
next
case False
show False
proof(cases "m = Exit")
case True
from `m ∈ obs (sourcenode a) (PDG_BS S)` `nx ∈ obs (sourcenode a) (PDG_BS S)`
obtain xs where "sourcenode a -xs->* m" and "nx ∉ set(sourcenodes xs)"
by(fastforce elim:obsE)
obtain x' xs' where [simp]:"xs = x'#xs'"
proof(cases xs)
case Nil
with `sourcenode a -xs->* m` have [simp]:"sourcenode a = m" by fastforce
with `m ∈ obs (sourcenode a) (PDG_BS S)`
have "m ∈ (PDG_BS S)" by(fastforce elim:obsE)
with `valid_node m` have "obs m (PDG_BS S) = {m}"
by(rule n_in_obs)
with `nx ∈ obs (sourcenode a) (PDG_BS S)` `nx ≠ m` have False
by fastforce
thus ?thesis by simp
qed blast
from `sourcenode a -xs->* m` have "sourcenode a = sourcenode x'"
and "valid_edge x'" and "targetnode x' -xs'->* m"
by(auto elim:path_split_Cons)
from `targetnode x' -xs'->* m` `nx ∉ set(sourcenodes xs)` `valid_edge x'`
`valid_node m` True
have "¬ nx strongly-postdominates (targetnode x')"
by(fastforce simp:strong_postdominate_def postdominate_def sourcenodes_def)
from `nx ≠ m` True have "nx ≠ (_Exit_)" by simp
with `obs (targetnode a) (PDG_BS S) = {nx}`
have "nx strongly-postdominates (targetnode a)"
by(fastforce intro:obs_strong_postdominate)
from `obs (targetnode a) (PDG_BS S) = {nx}`
obtain ys where "targetnode a -ys->* nx"
and "∀nx' ∈ set(sourcenodes ys). nx' ∉ (PDG_BS S)"
and "nx ∈ (PDG_BS S)" by(fastforce elim:obsE)
hence "nx ∉ set(sourcenodes ys)"by fastforce
have "sourcenode a ≠ nx"
proof
assume "sourcenode a = nx"
from `nx ∈ obs (sourcenode a) (PDG_BS S)`
have "nx ∈ (PDG_BS S)" by -(erule obsE)
with `valid_node nx` have "obs nx (PDG_BS S) = {nx}" by -(erule n_in_obs)
with `sourcenode a = nx` `m ∈ obs (sourcenode a) (PDG_BS S)`
`nx ≠ m` show False by fastforce
qed
with `nx ∉ set(sourcenodes ys)` have "nx ∉ set(sourcenodes (a#ys))"
by(fastforce simp:sourcenodes_def)
from `valid_edge a` `targetnode a -ys->* nx`
have "sourcenode a -a#ys->* nx" by(fastforce intro:Cons_path)
from `sourcenode a -a#ys->* nx` `nx ∉ set(sourcenodes (a#ys))`
`nx strongly-postdominates (targetnode a)` `valid_edge x'`
`¬ nx strongly-postdominates (targetnode x')` `sourcenode a = sourcenode x'`
have "(sourcenode a) weakly controls nx"
by(fastforce simp:weak_control_dependence_def)
with `nx ∈ (PDG_BS S)` have "sourcenode a ∈ (PDG_BS S)"
by(rule cd_closed)
with `valid_edge a` have "obs (sourcenode a) (PDG_BS S) = {sourcenode a}"
by(fastforce intro!:n_in_obs)
with `m ∈ obs (sourcenode a) (PDG_BS S)`
`nx ∈ obs (sourcenode a) (PDG_BS S)` `nx ≠ m`
show False by simp
next
case False
with `m ∈ obs (sourcenode a) (PDG_BS S)` `valid_node m`
`¬ m strongly-postdominates sourcenode a`
show False by(fastforce dest:obs_strong_postdominate)
qed
qed
qed


lemma WeakPDGBackwardSliceCorrect:
"BackwardSlice sourcenode targetnode kind valid_edge
(_Entry_) Def Use state_val PDG_BS"

proof(unfold_locales)
fix n S assume "n ∈ PDG_BS S"
thus "valid_node n" by(rule PDG_BS_valid_node)
next
fix n S assume "valid_node n" and "n ∈ S"
thus "n ∈ PDG_BS S" by(fastforce intro:PDG_path_Nil simp:PDG_BS_def)
next
fix n' S n V assume "n' ∈ PDG_BS S" and "n influences V in n'"
thus "n ∈ PDG_BS S"
by(auto dest:PDG.PDG_path_ddep[OF PDG_wcd,OF PDG.PDG_ddep_edge[OF PDG_wcd]]
dest:PDG_path_Append simp:PDG_BS_def split:split_if_asm)
next
fix n S
have "(∃m. obs n (PDG_BS S) = {m}) ∨ obs n (PDG_BS S) = {}"
by(rule obs_singleton)
thus "finite (obs n (PDG_BS S))" by fastforce
next
fix n S
have "(∃m. obs n (PDG_BS S) = {m}) ∨ obs n (PDG_BS S) = {}"
by(rule obs_singleton)
thus "card (obs n (PDG_BS S)) ≤ 1" by fastforce
qed

end


subsection{* Weak order dependence *}

context CFG_wf begin

lemma obs_singleton:
(*assumes valid:"valid_node n"*)
shows "(∃m. obs n (wod_backward_slice S) = {m}) ∨
obs n (wod_backward_slice S) = {}"

proof(rule ccontr)
let ?WOD_BS = "wod_backward_slice S"
assume "¬ ((∃m. obs n ?WOD_BS = {m}) ∨ obs n ?WOD_BS = {})"
hence "∃nx nx'. nx ∈ obs n ?WOD_BS ∧ nx' ∈ obs n ?WOD_BS ∧
nx ≠ nx'"
by auto
then obtain nx nx' where "nx ∈ obs n ?WOD_BS" and "nx' ∈ obs n ?WOD_BS"
and "nx ≠ nx'" by auto
from `nx ∈ obs n ?WOD_BS` obtain as where "n -as->* nx"
and "∀n' ∈ set(sourcenodes as). n' ∉ ?WOD_BS" and "nx ∈ ?WOD_BS"
by(erule obsE)
from `n -as->* nx` have "valid_node nx" by(fastforce dest:path_valid_node)
with `nx ∈ ?WOD_BS` have "obs nx ?WOD_BS = {nx}" by -(rule n_in_obs)
with `n -as->* nx` `nx ∈ obs n ?WOD_BS` `nx' ∈ obs n ?WOD_BS` `nx ≠ nx'`
have "as ≠ []" by(fastforce elim:path.cases)
with `n -as->* nx` `nx ∈ obs n ?WOD_BS` `nx' ∈ obs n ?WOD_BS` `nx ≠ nx'`
`obs nx ?WOD_BS = {nx}` `∀n' ∈ set(sourcenodes as). n' ∉ ?WOD_BS`
have "∃a as' as''. n -as'->* sourcenode a ∧ targetnode a -as''->* nx ∧
valid_edge a ∧ as = as'@a#as'' ∧
obs (targetnode a) ?WOD_BS = {nx} ∧
(¬ (∃m. obs (sourcenode a) ?WOD_BS = {m} ∨
obs (sourcenode a) ?WOD_BS = {}))"

proof(induct arbitrary:nx' rule:path.induct)
case (Cons_path n'' as n' a n)
note [simp] = `sourcenode a = n`[THEN sym] `targetnode a = n''`[THEN sym]
note more_than_one = `n' ∈ obs n (?WOD_BS)` `nx' ∈ obs n (?WOD_BS)` `n' ≠ nx'`
note IH = `!!nx'. [|n' ∈ obs n'' (?WOD_BS); nx' ∈ obs n'' (?WOD_BS); n' ≠ nx';
obs n' (?WOD_BS) = {n'}; ∀n'∈set (sourcenodes as). n' ∉ (?WOD_BS); as ≠ []|]
==> ∃a as' as''. n'' -as'->* sourcenode a ∧ targetnode a -as''->* n' ∧
valid_edge a ∧ as = as'@a#as'' ∧ obs (targetnode a) (?WOD_BS) = {n'} ∧
(¬ (∃m. obs (sourcenode a) (?WOD_BS) = {m} ∨
obs (sourcenode a) (?WOD_BS) = {}))`

from `∀n'∈set (sourcenodes (a#as)). n' ∉ (?WOD_BS)`
have "∀n'∈set (sourcenodes as). n' ∉ (?WOD_BS)" and "sourcenode a ∉ (?WOD_BS)"
by(simp_all add:sourcenodes_def)
show ?case
proof(cases "as = []")
case True
with `n'' -as->* n'` have [simp]:"n' = n''" by(fastforce elim:path.cases)
from more_than_one
have "¬ (∃m. obs (sourcenode a) (?WOD_BS) = {m} ∨
obs (sourcenode a) (?WOD_BS) = {})"

by auto
with `obs n' (?WOD_BS) = {n'}` True `valid_edge a` show ?thesis
apply(rule_tac x="a" in exI)
apply(rule_tac x="[]" in exI)
apply(rule_tac x="[]" in exI)
by(auto intro!:empty_path)
next
case False
hence "as ≠ []" .
from `n'' -as->* n'` `∀n'∈set (sourcenodes as). n' ∉ (?WOD_BS)`
have "obs n' (?WOD_BS) ⊆ obs n'' (?WOD_BS)" by(rule path_obs_subset)
show ?thesis
proof(cases "obs n' (?WOD_BS) = obs n'' (?WOD_BS)")
case True
with `n'' -as->* n'` `valid_edge a` `obs n' (?WOD_BS) = {n'}` more_than_one
show ?thesis
apply(rule_tac x="a" in exI)
apply(rule_tac x="[]" in exI)
apply(rule_tac x="as" in exI)
by(fastforce intro:empty_path)
next
case False
with `obs n' (?WOD_BS) ⊆ obs n'' (?WOD_BS)`
have "obs n' (?WOD_BS) ⊂ obs n'' (?WOD_BS)" by simp
with `obs n' (?WOD_BS) = {n'}` obtain ni where "n' ∈ obs n'' (?WOD_BS)"
and "ni ∈ obs n'' (?WOD_BS)" and "n' ≠ ni" by auto
from IH[OF this `obs n' (?WOD_BS) = {n'}`
`∀n'∈set (sourcenodes as). n' ∉ (?WOD_BS)` `as ≠ []`] obtain a' as' as''
where "n'' -as'->* sourcenode a'" and "targetnode a' -as''->* n'"
and "valid_edge a'" and [simp]:"as = as'@a'#as''"
and "obs (targetnode a') (?WOD_BS) = {n'}"
and more_than_one':"¬ (∃m. obs (sourcenode a') (?WOD_BS) = {m} ∨
obs (sourcenode a') (?WOD_BS) = {})"

by blast
from `n'' -as'->* sourcenode a'` `valid_edge a`
have "n -a#as'->* sourcenode a'" by(fastforce intro:path.Cons_path)
with `targetnode a' -as''->* n'` `obs (targetnode a') (?WOD_BS) = {n'}`
more_than_one' `valid_edge a'` show ?thesis
apply(rule_tac x="a'" in exI)
apply(rule_tac x="a#as'" in exI)
apply(rule_tac x="as''" in exI)
by fastforce
qed
qed
qed simp
then obtain a as' as'' where "valid_edge a"
and "obs (targetnode a) (?WOD_BS) = {nx}"
and more_than_one:"¬ (∃m. obs (sourcenode a) (?WOD_BS) = {m} ∨
obs (sourcenode a) (?WOD_BS) = {})"

by blast
have "sourcenode a ∉ (?WOD_BS)"
proof(rule ccontr)
assume "¬ sourcenode a ∉ ?WOD_BS"
hence "sourcenode a ∈ ?WOD_BS" by simp
with `valid_edge a` have "obs (sourcenode a) (?WOD_BS) = {sourcenode a}"
by(fastforce intro!:n_in_obs)
with more_than_one show False by simp
qed
with `valid_edge a`
have "obs (targetnode a) (?WOD_BS) ⊆ obs (sourcenode a) (?WOD_BS)"
by(rule edge_obs_subset)
with `obs (targetnode a) (?WOD_BS) = {nx}`
have "nx ∈ obs (sourcenode a) (?WOD_BS)" by simp
with more_than_one obtain m where "m ∈ obs (sourcenode a) (?WOD_BS)"
and "nx ≠ m" by auto
with `nx ∈ obs (sourcenode a) (?WOD_BS)` obtain as2
where "sourcenode a -as2->* m" and "nx ∉ set(sourcenodes as2)"
by(fastforce elim:obsE)
from `nx ∈ obs (sourcenode a) (?WOD_BS)` `m ∈ obs (sourcenode a) (?WOD_BS)`
obtain as1 where "sourcenode a -as1->* nx" and "m ∉ set(sourcenodes as1)"
by(fastforce elim:obsE)
from `obs (targetnode a) (?WOD_BS) = {nx}` obtain asx
where "targetnode a -asx->* nx" by(fastforce elim:obsE)
have "∀asx'. targetnode a -asx'->* m --> nx ∈ set(sourcenodes asx')"
proof(rule ccontr)
assume "¬ (∀asx'. targetnode a -asx'->* m --> nx ∈ set (sourcenodes asx'))"
then obtain asx' where "targetnode a -asx'->* m" and "nx ∉ set (sourcenodes asx')"
by blast
show False
proof(cases "∀nx ∈ set(sourcenodes asx'). nx ∉ ?WOD_BS")
case True
with `targetnode a -asx'->* m` `m ∈ obs (sourcenode a) (?WOD_BS)`
have "m ∈ obs (targetnode a) ?WOD_BS" by(fastforce intro:obs_elem elim:obsE)
with `nx ≠ m` `obs (targetnode a) (?WOD_BS) = {nx}` show False by simp
next
case False
hence "∃nx ∈ set(sourcenodes asx'). nx ∈ ?WOD_BS" by blast
then obtain nx' ns ns' where "sourcenodes asx' = ns@nx'#ns'" and "nx' ∈ ?WOD_BS"
and "∀nx ∈ set ns. nx ∉ ?WOD_BS" by(fastforce elim!:split_list_first_propE)
from `sourcenodes asx' = ns@nx'#ns'` obtain ax ai ai'
where [simp]:"asx' = ai@ax#ai'" "ns = sourcenodes ai" "nx' = sourcenode ax"
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
from `targetnode a -asx'->* m` have "targetnode a -ai->* sourcenode ax"
by(fastforce dest:path_split)
with `nx' ∈ ?WOD_BS` `∀nx ∈ set ns. nx ∉ ?WOD_BS`
have "nx' ∈ obs (targetnode a) ?WOD_BS" by(fastforce intro:obs_elem)
with `obs (targetnode a) (?WOD_BS) = {nx}` have "nx' = nx" by simp
with `nx ∉ set (sourcenodes asx')` show False by(simp add:sourcenodes_def)
qed
qed
with `nx ≠ m` `sourcenode a -as1->* nx` `m ∉ set(sourcenodes as1)`
`sourcenode a -as2->* m` `nx ∉ set(sourcenodes as2)` `valid_edge a`
`targetnode a -asx->* nx`
have "sourcenode a -->wod nx,m" by(simp add:wod_def,blast)
with `nx ∈ obs (sourcenode a) (?WOD_BS)` `m ∈ obs (sourcenode a) (?WOD_BS)`
have "sourcenode a ∈ ?WOD_BS" by(fastforce elim:cd_closed elim:obsE)
with `sourcenode a ∉ ?WOD_BS` show False by simp
qed


lemma WODBackwardSliceCorrect:
"BackwardSlice sourcenode targetnode kind valid_edge
(_Entry_) Def Use state_val wod_backward_slice"

proof(unfold_locales)
fix n S assume "n ∈ wod_backward_slice S"
thus "valid_node n" by(rule wod_backward_slice_valid_node)
next
fix n S assume "valid_node n" and "n ∈ S"
thus "n ∈ wod_backward_slice S" by(rule refl)
next
fix n' S n V assume "n' ∈ wod_backward_slice S" "n influences V in n'"
thus "n ∈ wod_backward_slice S"
by -(rule dd_closed)
next
fix n S
have "(∃m. obs n (wod_backward_slice S) = {m}) ∨
obs n (wod_backward_slice S) = {}"

by(rule obs_singleton)
thus "finite (obs n (wod_backward_slice S))" by fastforce
next
fix n S
have "(∃m. obs n (wod_backward_slice S) = {m}) ∨ obs n (wod_backward_slice S) = {}"
by(rule obs_singleton)
thus "card (obs n (wod_backward_slice S)) ≤ 1" by fastforce
qed

end

end