header {* \isaheader{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
by(simp add:sourcenodes_def targetnodes_def)
next
case False
from IH[OF `targetnode a' -as'->* n'` this]
have "sourcenodes as' = targetnode a' # butlast (targetnodes as')" .
with `n = sourcenode a'` False show ?thesis
by(simp add:sourcenodes_def targetnodes_def)
qed
qed
lemma targetnodes_is_tl_sourcenodes_App_n':
"[|n -as->* n'; as ≠ []|] ==>
targetnodes as = (tl (sourcenodes as))@[n']"
proof(induct as arbitrary:n' rule:rev_induct)
case Nil thus ?case by simp
next
case (snoc a' as')
note IH = `!!n'. [|n -as'->* n'; as' ≠ []|]
==> targetnodes as' = tl (sourcenodes as') @ [n']`
from `n -as'@[a']->* n'` have "n -as'->* sourcenode a'" and "n' = targetnode a'"
by(auto elim:path_split_snoc)
show ?case
proof(cases "as' = []")
case True
with `n -as'->* sourcenode a'` have "n = sourcenode a'" by fast
with True `n' = targetnode a'` show ?thesis
by(simp add:sourcenodes_def targetnodes_def)
next
case False
from IH[OF `n -as'->* sourcenode a'` this]
have "targetnodes as' = tl (sourcenodes as')@[sourcenode a']" .
with `n' = targetnode a'` False show ?thesis
by(simp add:sourcenodes_def targetnodes_def)
qed
qed
lemma Entry_sourcenode_hd:
assumes "n -as->* n'" and "(_Entry_) ∈ set (sourcenodes as)"
shows "n = (_Entry_)" and "(_Entry_) ∉ set (sourcenodes (tl as))"
using `n -as->* n'` `(_Entry_) ∈ set (sourcenodes as)`
proof(induct rule:path.induct)
case (empty_path n) case 1
thus ?case by(simp add:sourcenodes_def)
next
case (empty_path n) case 2
thus ?case by(simp add:sourcenodes_def)
next
case (Cons_path n'' as n' a n)
note IH1 = `(_Entry_) ∈ set(sourcenodes as) ==> n'' = (_Entry_)`
note IH2 = `(_Entry_) ∈ set(sourcenodes as) ==> (_Entry_) ∉ set(sourcenodes(tl as))`
have "(_Entry_) ∉ set (sourcenodes(tl(a#as)))"
proof
assume "(_Entry_) ∈ set (sourcenodes (tl (a#as)))"
hence "(_Entry_) ∈ set (sourcenodes as)" by simp
from IH1[OF this] have "n'' = (_Entry_)" by simp
with `targetnode a = n''` `valid_edge a` show False by -(erule Entry_target,simp)
qed
hence "(_Entry_) ∉ set (sourcenodes(tl(a#as)))" by fastforce
{ case 1
with `(_Entry_) ∉ set (sourcenodes(tl(a#as)))` `sourcenode a = n`
show ?case by(simp add:sourcenodes_def)
next
case 2
with `(_Entry_) ∉ set (sourcenodes(tl(a#as)))` `sourcenode a = n`
show ?case by(simp add:sourcenodes_def)
}
qed
end
end