Theory AdditionalLemmas
section ‹Lemmas for the control dependences›
theory AdditionalLemmas imports WellFormed
begin
subsection ‹Paths to @{term "(_Exit_)"} and from @{term "(_Entry_)"} exist›
abbreviation path :: "cmd ⇒ w_node ⇒ w_edge list ⇒ w_node ⇒ bool"
("_ ⊢ _ -_→* _")
where "prog ⊢ n -as→* n' ≡ CFG.path sourcenode targetnode (valid_edge prog)
n as n'"
definition label_incrs :: "w_edge list ⇒ nat ⇒ w_edge list" ("_ ⊕s _" 60)
where "as ⊕s i ≡ map (λ(n,et,n'). (n ⊕ i,et,n' ⊕ i)) as"
lemma path_SeqFirst:
"prog ⊢ n -as→* (_ l _) ⟹ prog;;c⇩2 ⊢ n -as→* (_ l _)"
proof(induct n as "(_ l _)" arbitrary:l rule:While_CFG.path.induct)
case empty_path
from ‹CFG.valid_node sourcenode targetnode (valid_edge prog) (_ l _)›
show ?case
apply -
apply(rule While_CFG.empty_path)
apply(auto simp:While_CFG.valid_node_def valid_edge_def)
by(case_tac b,auto dest:WCFG_SeqFirst WCFG_SeqConnect)
next
case (Cons_path n'' as a n)
note IH = ‹prog;; c⇩2 ⊢ n'' -as→* (_ l _)›
from ‹prog ⊢ n'' -as→* (_ l _)› have "n'' ≠ (_Exit_)"
by fastforce
with ‹valid_edge prog a› ‹sourcenode a = n› ‹targetnode a = n''›
have "prog;;c⇩2 ⊢ n -kind a→ n''" by(simp add:valid_edge_def WCFG_SeqFirst)
with IH ‹prog;;c⇩2 ⊢ n -kind a→ n''› ‹sourcenode a = n› ‹targetnode a = n''› show ?case
by(fastforce intro:While_CFG.Cons_path simp:valid_edge_def)
qed
lemma path_SeqSecond:
"⟦prog ⊢ n -as→* n'; n ≠ (_Entry_); as ≠ []⟧
⟹ c⇩1;;prog ⊢ n ⊕ #:c⇩1 -as ⊕s #:c⇩1→* n' ⊕ #:c⇩1"
proof(induct rule:While_CFG.path.induct)
case (Cons_path n'' as n' a n)
note IH = ‹ ⟦n'' ≠ (_Entry_); as ≠ []⟧
⟹ c⇩1;;prog ⊢ n'' ⊕ #:c⇩1 -as ⊕s #:c⇩1→* n' ⊕ #:c⇩1›
from ‹valid_edge prog a› ‹sourcenode a = n› ‹targetnode a = n''› ‹n ≠ (_Entry_)›
have "c⇩1;;prog ⊢ n ⊕ #:c⇩1 -kind a→ n'' ⊕ #:c⇩1"
by(simp add:valid_edge_def WCFG_SeqSecond)
from ‹sourcenode a = n› ‹targetnode a = n''› ‹valid_edge prog a›
have "[(n,kind a,n'')] ⊕s #:c⇩1 = [a] ⊕s #:c⇩1"
by(cases a,simp add:label_incrs_def valid_edge_def)
show ?case
proof(cases "as = []")
case True
with ‹prog ⊢ n'' -as→* n'› have [simp]:"n'' = n'" by(auto elim:While_CFG.cases)
with ‹c⇩1;;prog ⊢ n ⊕ #:c⇩1 -kind a→ n'' ⊕ #:c⇩1›
have "c⇩1;;prog ⊢ n ⊕ #:c⇩1 -[(n,kind a,n')] ⊕s #:c⇩1→* n' ⊕ #:c⇩1"
by(fastforce intro:While_CFG.Cons_path While_CFG.empty_path
simp:label_incrs_def While_CFG.valid_node_def valid_edge_def)
with True ‹[(n,kind a,n'')] ⊕s #:c⇩1 = [a] ⊕s #:c⇩1› show ?thesis by simp
next
case False
from ‹valid_edge prog a› ‹targetnode a = n''› have "n'' ≠ (_Entry_)"
by(cases n'',auto simp:valid_edge_def)
from IH[OF this False]
have "c⇩1;;prog ⊢ n'' ⊕ #:c⇩1 -as ⊕s #:c⇩1→* n' ⊕ #:c⇩1" .
with ‹c⇩1;;prog ⊢ n ⊕ #:c⇩1 -kind a→ n'' ⊕ #:c⇩1› ‹sourcenode a = n›
‹targetnode a = n''› ‹[(n,kind a,n'')] ⊕s #:c⇩1 = [a] ⊕s #:c⇩1› show ?thesis
apply(cases a)
apply(simp add:label_incrs_def)
by(fastforce intro:While_CFG.Cons_path simp:valid_edge_def)
qed
qed simp
lemma path_CondTrue:
"prog ⊢ (_ l _) -as→* n'
⟹ if (b) prog else c⇩2 ⊢ (_ l _) ⊕ 1 -as ⊕s 1→* n' ⊕ 1"
proof(induct "(_ l _)" as n' arbitrary:l rule:While_CFG.path.induct)
case empty_path
from ‹CFG.valid_node sourcenode targetnode (valid_edge prog) (_ l _)›
WCFG_CondTrue[of b prog c⇩2]
have "CFG.valid_node sourcenode targetnode (valid_edge (if (b) prog else c⇩2))
((_ l _) ⊕ 1)"
apply(auto simp:While_CFG.valid_node_def valid_edge_def)
apply(rotate_tac 1,drule WCFG_CondThen,simp,fastforce)
apply(case_tac a) apply auto
apply(rotate_tac 1,drule WCFG_CondThen,simp,fastforce)
by(rotate_tac 1,drule WCFG_EntryD,auto)
then show ?case
by(fastforce intro:While_CFG.empty_path simp:label_incrs_def)
next
case (Cons_path n'' as n' a)
note IH = ‹⋀l. n'' = (_ l _)
⟹ if (b) prog else c⇩2 ⊢ (_ l _) ⊕ 1 -as ⊕s 1→* n' ⊕ 1›
from ‹valid_edge prog a› ‹sourcenode a = (_ l _)› ‹targetnode a = n''›
have "if (b) prog else c⇩2 ⊢ (_ l _) ⊕ 1 -kind a→ n'' ⊕ 1"
by -(rule WCFG_CondThen,simp_all add:valid_edge_def)
from ‹sourcenode a = (_ l _)› ‹targetnode a = n''› ‹valid_edge prog a›
have "[((_ l _),kind a,n'')] ⊕s 1 = [a] ⊕s 1"
by(cases a,simp add:label_incrs_def valid_edge_def)
show ?case
proof(cases n'')
case (Node l')
from IH[OF this] have "if (b) prog else c⇩2 ⊢ (_ l' _) ⊕ 1 -as ⊕s 1→* n' ⊕ 1" .
with ‹if (b) prog else c⇩2 ⊢ (_ l _) ⊕ 1 -kind a→ n'' ⊕ 1› Node
have "if (b) prog else c⇩2 ⊢ (_ l _) ⊕ 1 -((_ l _) ⊕ 1,kind a,n'' ⊕ 1)#(as ⊕s 1)→* n' ⊕ 1"
by(fastforce intro:While_CFG.Cons_path simp:valid_edge_def valid_node_def)
with ‹[((_ l _),kind a,n'')] ⊕s 1 = [a] ⊕s 1›
have "if (b) prog else c⇩2 ⊢ (_ l _) ⊕ 1 -a#as ⊕s 1→* n' ⊕ 1"
by(simp add:label_incrs_def)
thus ?thesis by simp
next
case Entry
with ‹valid_edge prog a› ‹targetnode a = n''› have False by fastforce
thus ?thesis by simp
next
case Exit
with ‹prog ⊢ n'' -as→* n'› have "n' = (_Exit_)" and "as = []"
by(auto dest:While_CFGExit.path_Exit_source)
from ‹if (b) prog else c⇩2 ⊢ (_ l _) ⊕ 1 -kind a→ n'' ⊕ 1›
have "if (b) prog else c⇩2 ⊢ (_ l _) ⊕ 1 -[((_ l _) ⊕ 1,kind a,n'' ⊕ 1)]→* n'' ⊕ 1"
by(fastforce intro:While_CFG.Cons_path While_CFG.empty_path
simp:While_CFG.valid_node_def valid_edge_def)
with Exit ‹[((_ l _),kind a,n'')] ⊕s 1 = [a] ⊕s 1› ‹n' = (_Exit_)› ‹as = []›
show ?thesis by(fastforce simp:label_incrs_def)
qed
qed
lemma path_CondFalse:
"prog ⊢ (_ l _) -as→* n'
⟹ if (b) c⇩1 else prog ⊢ (_ l _) ⊕ (#:c⇩1 + 1) -as ⊕s (#:c⇩1 + 1)→* n' ⊕ (#:c⇩1 + 1)"
proof(induct "(_ l _)" as n' arbitrary:l rule:While_CFG.path.induct)
case empty_path
from ‹CFG.valid_node sourcenode targetnode (valid_edge prog) (_ l _)›
WCFG_CondFalse[of b c⇩1 prog]
have "CFG.valid_node sourcenode targetnode (valid_edge (if (b) c⇩1 else prog))
((_ l _) ⊕ #:c⇩1 + 1)"
apply(auto simp:While_CFG.valid_node_def valid_edge_def)
apply(rotate_tac 1,drule WCFG_CondElse,simp,fastforce)
apply(case_tac a) apply auto
apply(rotate_tac 1,drule WCFG_CondElse,simp,fastforce)
by(rotate_tac 1,drule WCFG_EntryD,auto)
thus ?case by(fastforce intro:While_CFG.empty_path simp:label_incrs_def)
next
case (Cons_path n'' as n' a)
note IH = ‹⋀l. n'' = (_ l _) ⟹ if (b) c⇩1 else prog ⊢ (_ l _) ⊕ (#:c⇩1 + 1)
-as ⊕s (#:c⇩1 + 1)→* n' ⊕ (#:c⇩1 + 1)›
from ‹valid_edge prog a› ‹sourcenode a = (_ l _)› ‹targetnode a = n''›
have "if (b) c⇩1 else prog ⊢ (_ l _) ⊕ (#:c⇩1 + 1) -kind a→ n'' ⊕ (#:c⇩1 + 1)"
by -(rule WCFG_CondElse,simp_all add:valid_edge_def)
from ‹sourcenode a = (_ l _)› ‹targetnode a = n''› ‹valid_edge prog a›
have "[((_ l _),kind a,n'')] ⊕s (#:c⇩1 + 1) = [a] ⊕s (#:c⇩1 + 1)"
by(cases a,simp add:label_incrs_def valid_edge_def)
show ?case
proof(cases n'')
case (Node l')
from IH[OF this] have "if (b) c⇩1 else prog ⊢ (_ l' _) ⊕ (#:c⇩1 + 1)
-as ⊕s (#:c⇩1 + 1)→* n' ⊕ (#:c⇩1 + 1)" .
with ‹if (b) c⇩1 else prog ⊢ (_ l _) ⊕ (#:c⇩1 + 1) -kind a→ n'' ⊕ (#:c⇩1 + 1)› Node
have "if (b) c⇩1 else prog ⊢ (_ l _) ⊕ (#:c⇩1 + 1)
-((_ l _) ⊕ (#:c⇩1 + 1),kind a,n'' ⊕ (#:c⇩1 + 1))#(as ⊕s (#:c⇩1 + 1))→*
n' ⊕ (#:c⇩1 + 1)"
by(fastforce intro:While_CFG.Cons_path simp:valid_edge_def valid_node_def)
with ‹[((_ l _),kind a,n'')] ⊕s (#:c⇩1 + 1) = [a] ⊕s (#:c⇩1 + 1)› Node
have "if (b) c⇩1 else prog ⊢ (_ l _) ⊕ (#:c⇩1 + 1) -a#as ⊕s (#:c⇩1 + 1)→*
n' ⊕ (#:c⇩1 + 1)"
by(simp add:label_incrs_def)
thus ?thesis by simp
next
case Entry
with ‹valid_edge prog a› ‹targetnode a = n''› have False by fastforce
thus ?thesis by simp
next
case Exit
with ‹prog ⊢ n'' -as→* n'› have "n' = (_Exit_)" and "as = []"
by(auto dest:While_CFGExit.path_Exit_source)
from ‹if (b) c⇩1 else prog ⊢ (_ l _) ⊕ (#:c⇩1 + 1) -kind a→ n'' ⊕ (#:c⇩1 + 1)›
have "if (b) c⇩1 else prog ⊢ (_ l _) ⊕ (#:c⇩1 + 1)
-[((_ l _) ⊕ (#:c⇩1 + 1),kind a,n'' ⊕ (#:c⇩1 + 1))]→* n'' ⊕ (#:c⇩1 + 1)"
by(fastforce intro:While_CFG.Cons_path While_CFG.empty_path
simp:While_CFG.valid_node_def valid_edge_def)
with Exit ‹[((_ l _),kind a,n'')] ⊕s (#:c⇩1 + 1) = [a] ⊕s (#:c⇩1 + 1)› ‹n' = (_Exit_)›
‹as = []›
show ?thesis by(fastforce simp:label_incrs_def)
qed
qed
declare add_2_eq_Suc' [simp del] One_nat_def [simp del]
lemma path_While:
"prog ⊢ (_ l _) -as→* (_ l' _)
⟹ while (b) prog ⊢ (_ l _) ⊕ 2 -as ⊕s 2→* (_ l' _) ⊕ 2"
proof(induct "(_ l _)" as "(_ l' _)" arbitrary:l l' rule:While_CFG.path.induct)
case empty_path
from ‹CFG.valid_node sourcenode targetnode (valid_edge prog) (_ l _)›
WCFG_WhileTrue[of b prog]
have "CFG.valid_node sourcenode targetnode (valid_edge (while (b) prog)) ((_ l _) ⊕ 2)"
apply(auto simp:While_CFG.valid_node_def valid_edge_def)
apply(case_tac ba) apply auto
apply(rotate_tac 1,drule WCFG_WhileBody,auto)
apply(rotate_tac 1,drule WCFG_WhileBodyExit,auto)
apply(case_tac a) apply auto
apply(rotate_tac 1,drule WCFG_WhileBody,auto)
by(rotate_tac 1,drule WCFG_EntryD,auto)
thus ?case by(fastforce intro:While_CFG.empty_path simp:label_incrs_def)
next
case (Cons_path n'' as a)
note IH = ‹⋀l. n'' = (_ l _)
⟹ while (b) prog ⊢ (_ l _) ⊕ 2 -as ⊕s 2→* (_ l' _) ⊕ 2›
from ‹sourcenode a = (_ l _)› ‹targetnode a = n''› ‹valid_edge prog a›
have "[((_ l _),kind a,n'')] ⊕s 2 = [a] ⊕s 2"
by(cases a,simp add:label_incrs_def valid_edge_def)
show ?case
proof(cases n'')
case (Node l'')
with ‹valid_edge prog a› ‹sourcenode a = (_ l _)› ‹targetnode a = n''›
have "while (b) prog ⊢ (_ l _) ⊕ 2 -kind a→ n'' ⊕ 2"
by -(rule WCFG_WhileBody,simp_all add:valid_edge_def)
from IH[OF Node]
have "while (b) prog ⊢ (_ l'' _) ⊕ 2 -as ⊕s 2→* (_ l' _) ⊕ 2" .
with ‹while (b) prog ⊢ (_ l _) ⊕ 2 -kind a→ n'' ⊕ 2› Node
have "while (b) prog ⊢ (_ l _) ⊕ 2 -((_ l _) ⊕ 2,kind a,n'' ⊕ 2)#(as ⊕s 2)→* (_ l' _) ⊕ 2"
by(fastforce intro:While_CFG.Cons_path simp:valid_edge_def)
with ‹[((_ l _),kind a,n'')] ⊕s 2 = [a] ⊕s 2› show ?thesis by(simp add:label_incrs_def)
next
case Entry
with ‹valid_edge prog a› ‹targetnode a = n''› have False by fastforce
thus ?thesis by simp
next
case Exit
with ‹prog ⊢ n'' -as→* (_ l' _)› have "(_ l' _) = (_Exit_)" and "as = []"
by(auto dest:While_CFGExit.path_Exit_source)
then have False by simp
thus ?thesis by simp
qed
qed
lemma inner_node_Entry_Exit_path:
"l < #:prog ⟹ (∃as. prog ⊢ (_ l _) -as→* (_Exit_)) ∧
(∃as. prog ⊢ (_Entry_) -as→* (_ l _))"
proof(induct prog arbitrary:l)
case Skip
from ‹l < #:Skip› have [simp]:"l = 0" by simp
hence "Skip ⊢ (_ l _) -⇑id→ (_Exit_)" by(simp add:WCFG_Skip)
hence "Skip ⊢ (_ l _) -[((_ l _),⇑id,(_Exit_))]→* (_Exit_)"
by (fastforce intro: While_CFG.path.intros simp: valid_edge_def)
have "Skip ⊢ (_Entry_) -(λs. True)⇩√→ (_ l _)" by(simp add:WCFG_Entry)
hence "Skip ⊢ (_Entry_) -[((_Entry_),(λs. True)⇩√,(_ l _))]→* (_ l _)"
by(fastforce intro:While_CFG.path.intros simp:valid_edge_def While_CFG.valid_node_def)
with ‹Skip ⊢ (_ l _) -[((_ l _),⇑id,(_Exit_))]→* (_Exit_)› show ?case by fastforce
next
case (LAss V e)
from ‹l < #:V:=e› have "l = 0 ∨ l = 1" by auto
thus ?case
proof
assume [simp]:"l = 0"
hence "V:=e ⊢ (_Entry_) -(λs. True)⇩√→ (_ l _)" by(simp add:WCFG_Entry)
hence "V:=e ⊢ (_Entry_) -[((_Entry_),(λs. True)⇩√,(_ l _))]→* (_ l _)"
by(fastforce intro:While_CFG.path.intros simp:valid_edge_def While_CFG.valid_node_def)
have "V:=e ⊢ (_1_) -⇑id→ (_Exit_)" by(rule WCFG_LAssSkip)
hence "V:=e ⊢ (_1_) -[((_1_),⇑id,(_Exit_))]→* (_Exit_)"
by(fastforce intro:While_CFG.path.intros simp:valid_edge_def)
with WCFG_LAss have "V:=e ⊢ (_ l _) -
[((_ l _),⇑(λs. s(V:=(interpret e s))),(_1_)),((_1_),⇑id,(_Exit_))]→*
(_Exit_)"
by(fastforce intro:While_CFG.path.intros simp:valid_edge_def)
with ‹V:=e ⊢ (_Entry_) -[((_Entry_),(λs. True)⇩√,(_ l _))]→* (_ l _)›
show ?case by fastforce
next
assume [simp]:"l = 1"
hence "V:=e ⊢ (_ l _) -⇑id→ (_Exit_)" by(simp add:WCFG_LAssSkip)
hence "V:=e ⊢ (_ l _) -[((_ l _),⇑id,(_Exit_))]→* (_Exit_)"
by(fastforce intro:While_CFG.path.intros simp:valid_edge_def)
have "V:=e ⊢ (_0_) -⇑(λs. s(V:=(interpret e s)))→ (_ l _)"
by(simp add:WCFG_LAss)
hence "V:=e ⊢ (_0_) -[((_0_),⇑(λs. s(V:=(interpret e s))),(_ l _))]→* (_ l _)"
by(fastforce intro:While_CFG.path.intros simp:valid_edge_def While_CFG.valid_node_def)
with WCFG_Entry[of "V:=e"] have "V:=e ⊢ (_Entry_) -[((_Entry_),(λs. True)⇩√,(_0_))
,((_0_),⇑(λs. s(V:=(interpret e s))),(_ l _))]→* (_ l _)"
by(fastforce intro:While_CFG.path.intros simp:valid_edge_def)
with ‹V:=e ⊢ (_ l _) -[((_ l _),⇑id,(_Exit_))]→* (_Exit_)› show ?case by fastforce
qed
next
case (Seq prog1 prog2)
note IH1 = ‹⋀l. l < #:prog1 ⟹
(∃as. prog1 ⊢ (_ l _) -as→* (_Exit_)) ∧ (∃as. prog1 ⊢ (_Entry_) -as→* (_ l _))›
note IH2 = ‹⋀l. l < #:prog2 ⟹
(∃as. prog2 ⊢ (_ l _) -as→* (_Exit_)) ∧ (∃as. prog2 ⊢ (_Entry_) -as→* (_ l _))›
show ?case
proof(cases "l < #:prog1")
case True
from IH1[OF True] obtain as as' where "prog1 ⊢ (_ l _) -as→* (_Exit_)"
and "prog1 ⊢ (_Entry_) -as'→* (_ l _)" by blast
from ‹prog1 ⊢ (_Entry_) -as'→* (_ l _)›
have "prog1;;prog2 ⊢ (_Entry_) -as'→* (_ l _)"
by(fastforce intro:path_SeqFirst)
from ‹prog1 ⊢ (_ l _) -as→* (_Exit_)›
obtain asx ax where "prog1 ⊢ (_ l _) -asx@[ax]→* (_Exit_)"
by(induct rule:rev_induct,auto elim:While_CFG.path.cases)
hence "prog1 ⊢ (_ l _) -asx→* sourcenode ax"
and "valid_edge prog1 ax" and "(_Exit_) = targetnode ax"
by(auto intro:While_CFG.path_split_snoc)
from ‹prog1 ⊢ (_ l _) -asx→* sourcenode ax› ‹valid_edge prog1 ax›
obtain lx where [simp]:"sourcenode ax = (_ lx _)"
by(cases "sourcenode ax") auto
with ‹prog1 ⊢ (_ l _) -asx→* sourcenode ax›
have "prog1;;prog2 ⊢ (_ l _) -asx→* sourcenode ax"
by(fastforce intro:path_SeqFirst)
from ‹valid_edge prog1 ax› ‹(_Exit_) = targetnode ax›
have "prog1;;prog2 ⊢ sourcenode ax -kind ax→ (_0_) ⊕ #:prog1"
by(fastforce intro:WCFG_SeqConnect simp:valid_edge_def)
hence "prog1;;prog2 ⊢ sourcenode ax -[(sourcenode ax,kind ax,(_0_) ⊕ #:prog1)]→*
(_0_) ⊕ #:prog1"
by(fastforce intro:While_CFG.Cons_path While_CFG.empty_path
simp:While_CFG.valid_node_def valid_edge_def)
with ‹prog1;;prog2 ⊢ (_ l _) -asx→* sourcenode ax›
have "prog1;;prog2 ⊢ (_ l _) -asx@[(sourcenode ax,kind ax,(_0_) ⊕ #:prog1)]→*
(_0_) ⊕ #:prog1"
by(fastforce intro:While_CFG.path_Append)
from IH2[of "0"] obtain as'' where "prog2 ⊢ (_ 0 _) -as''→* (_Exit_)" by blast
hence "prog1;;prog2 ⊢ (_0_) ⊕ #:prog1 -as'' ⊕s #:prog1→* (_Exit_) ⊕ #:prog1"
by(fastforce intro!:path_SeqSecond elim:While_CFG.path.cases)
hence "prog1;;prog2 ⊢ (_0_) ⊕ #:prog1 -as'' ⊕s #:prog1→* (_Exit_)"
by simp
with ‹prog1;;prog2 ⊢ (_ l _) -asx@[(sourcenode ax,kind ax,(_0_) ⊕ #:prog1)]→*
(_0_) ⊕ #:prog1›
have "prog1;;prog2 ⊢ (_ l _) -(asx@[(sourcenode ax,kind ax,(_0_) ⊕ #:prog1)])@
(as'' ⊕s #:prog1)→* (_Exit_)"
by(fastforce intro:While_CFG.path_Append)
with ‹prog1;;prog2 ⊢ (_Entry_) -as'→* (_ l _)› show ?thesis by blast
next
case False
hence "#:prog1 ≤ l" by simp
then obtain l' where [simp]:"l = l' + #:prog1" and "l' = l - #:prog1" by simp
from ‹l < #:prog1;; prog2› have "l' < #:prog2" by simp
from IH2[OF this] obtain as as' where "prog2 ⊢ (_ l' _) -as→* (_Exit_)"
and "prog2 ⊢ (_Entry_) -as'→* (_ l' _)" by blast
from ‹prog2 ⊢ (_ l' _) -as→* (_Exit_)›
have "prog1;;prog2 ⊢ (_ l' _) ⊕ #:prog1 -as ⊕s #:prog1→* (_Exit_) ⊕ #:prog1"
by(fastforce intro!:path_SeqSecond elim:While_CFG.path.cases)
hence "prog1;;prog2 ⊢ (_ l _) -as ⊕s #:prog1→* (_Exit_)"
by simp
from IH1[of 0] obtain as'' where "prog1 ⊢ (_0_) -as''→* (_Exit_)" by blast
then obtain ax asx where "prog1 ⊢ (_0_) -asx@[ax]→* (_Exit_)"
by(induct rule:rev_induct,auto elim:While_CFG.path.cases)
hence "prog1 ⊢ (_0_) -asx→* sourcenode ax" and "valid_edge prog1 ax"
and "(_Exit_) = targetnode ax" by(auto intro:While_CFG.path_split_snoc)
from WCFG_Entry ‹prog1 ⊢ (_0_) -asx→* sourcenode ax›
have "prog1 ⊢ (_Entry_) -((_Entry_),(λs. True)⇩√,(_0_))#asx→* sourcenode ax"
by(fastforce intro:While_CFG.Cons_path simp:valid_edge_def valid_node_def)
from ‹prog1 ⊢ (_0_) -asx→* sourcenode ax› ‹valid_edge prog1 ax›
obtain lx where [simp]:"sourcenode ax = (_ lx _)"
by(cases "sourcenode ax") auto
with ‹prog1 ⊢ (_Entry_) -((_Entry_),(λs. True)⇩√,(_0_))#asx→* sourcenode ax›
have "prog1;;prog2 ⊢ (_Entry_) -((_Entry_),(λs. True)⇩√,(_0_))#asx→*
sourcenode ax"
by(fastforce intro:path_SeqFirst)
from ‹prog2 ⊢ (_Entry_) -as'→* (_ l' _)› obtain ax' asx'
where "prog2 ⊢ (_Entry_) -ax'#asx'→* (_ l' _)"
by(cases as',auto elim:While_CFG.path.cases)
hence "(_Entry_) = sourcenode ax'" and "valid_edge prog2 ax'"
and "prog2 ⊢ targetnode ax' -asx'→* (_ l' _)"
by(auto intro:While_CFG.path_split_Cons)
hence "targetnode ax' = (_0_)" by(fastforce dest:WCFG_EntryD simp:valid_edge_def)
from ‹valid_edge prog1 ax› ‹(_Exit_) = targetnode ax›
have "prog1;;prog2 ⊢ sourcenode ax -kind ax→ (_0_) ⊕ #:prog1"
by(fastforce intro:WCFG_SeqConnect simp:valid_edge_def)
have "∃as. prog1;;prog2 ⊢ sourcenode ax -as→* (_ l _)"
proof(cases "asx' = []")
case True
with ‹prog2 ⊢ targetnode ax' -asx'→* (_ l' _)› ‹targetnode ax' = (_0_)›
have "l' = 0" by(auto elim:While_CFG.path.cases)
with ‹prog1;;prog2 ⊢ sourcenode ax -kind ax→ (_0_) ⊕ #:prog1›
have "prog1;;prog2 ⊢ sourcenode ax -[(sourcenode ax,kind ax,(_ l _))]→*
(_ l _)"
by(auto intro!:While_CFG.path.intros
simp:While_CFG.valid_node_def valid_edge_def,blast)
thus ?thesis by blast
next
case False
with ‹prog2 ⊢ targetnode ax' -asx'→* (_ l' _)› ‹targetnode ax' = (_0_)›
have "prog1;;prog2 ⊢ (_0_) ⊕ #:prog1 -asx' ⊕s #:prog1→* (_ l' _) ⊕ #:prog1"
by(fastforce intro:path_SeqSecond)
hence "prog1;;prog2 ⊢ (_0_) ⊕ #:prog1 -asx' ⊕s #:prog1→* (_ l _)" by simp
with ‹prog1;;prog2 ⊢ sourcenode ax -kind ax→ (_0_) ⊕ #:prog1›
have "prog1;;prog2 ⊢ sourcenode ax -(sourcenode ax,kind ax,(_0_) ⊕ #:prog1)#
(asx' ⊕s #:prog1)→* (_ l _)"
by(fastforce intro: While_CFG.Cons_path simp:valid_node_def valid_edge_def)
thus ?thesis by blast
qed
then obtain asx'' where "prog1;;prog2 ⊢ sourcenode ax -asx''→* (_ l _)" by blast
with ‹prog1;;prog2 ⊢ (_Entry_) -((_Entry_),(λs. True)⇩√,(_0_))#asx→*
sourcenode ax›
have "prog1;;prog2 ⊢ (_Entry_) -(((_Entry_),(λs. True)⇩√,(_0_))#asx)@asx''→*
(_ l _)"
by(rule While_CFG.path_Append)
with ‹prog1;;prog2 ⊢ (_ l _) -as ⊕s #:prog1→* (_Exit_)›
show ?thesis by blast
qed
next
case (Cond b prog1 prog2)
note IH1 = ‹⋀l. l < #:prog1 ⟹
(∃as. prog1 ⊢ (_ l _) -as→* (_Exit_)) ∧ (∃as. prog1 ⊢ (_Entry_) -as→* (_ l _))›
note IH2 = ‹⋀l. l < #:prog2 ⟹
(∃as. prog2 ⊢ (_ l _) -as→* (_Exit_)) ∧ (∃as. prog2 ⊢ (_Entry_) -as→* (_ l _))›
show ?case
proof(cases "l = 0")
case True
from IH1[of 0] obtain as where "prog1 ⊢ (_0_) -as→* (_Exit_)" by blast
hence "if (b) prog1 else prog2 ⊢ (_0_) ⊕ 1 -as ⊕s 1→* (_Exit_) ⊕ 1"
by(fastforce intro:path_CondTrue)
with WCFG_CondTrue[of b prog1 prog2] have "if (b) prog1 else prog2 ⊢
(_0_) -((_0_),(λs. interpret b s = Some true)⇩√,(_0_) ⊕ 1)#(as ⊕s 1)→*
(_Exit_) ⊕ 1"
by(fastforce intro:While_CFG.Cons_path simp:valid_edge_def valid_node_def)
with True have "if (b) prog1 else prog2 ⊢
(_ l _) -((_0_),(λs. interpret b s = Some true)⇩√,(_0_) ⊕ 1)#(as ⊕s 1)→*
(_Exit_)" by simp
moreover
from WCFG_Entry[of "if (b) prog1 else prog2"] True
have "if (b) prog1 else prog2 ⊢ (_Entry_) -[((_Entry_),(λs. True)⇩√,(_0_))]→*
(_ l _)"
by(fastforce intro:While_CFG.Cons_path While_CFG.empty_path
simp:While_CFG.valid_node_def valid_edge_def)
ultimately show ?thesis by blast
next
case False
hence "0 < l" by simp
then obtain l' where [simp]:"l = l' + 1" and "l' = l - 1" by simp
show ?thesis
proof(cases "l' < #:prog1")
case True
from IH1[OF this] obtain as as' where "prog1 ⊢ (_ l' _) -as→* (_Exit_)"
and "prog1 ⊢ (_Entry_) -as'→* (_ l' _)" by blast
from ‹prog1 ⊢ (_ l' _) -as→* (_Exit_)›
have "if (b) prog1 else prog2 ⊢ (_ l' _) ⊕ 1 -as ⊕s 1→* (_Exit_) ⊕ 1"
by(fastforce intro:path_CondTrue)
hence "if (b) prog1 else prog2 ⊢ (_ l _) -as ⊕s 1→* (_Exit_)"
by simp
from ‹prog1 ⊢ (_Entry_) -as'→* (_ l' _)› obtain ax asx
where "prog1 ⊢ (_Entry_) -ax#asx→* (_ l' _)"
by(cases as',auto elim:While_CFG.cases)
hence "(_Entry_) = sourcenode ax" and "valid_edge prog1 ax"
and "prog1 ⊢ targetnode ax -asx→* (_ l' _)"
by(auto intro:While_CFG.path_split_Cons)
hence "targetnode ax = (_0_)" by(fastforce dest:WCFG_EntryD simp:valid_edge_def)
with ‹prog1 ⊢ targetnode ax -asx→* (_ l' _)›
have "if (b) prog1 else prog2 ⊢ (_0_) ⊕ 1 -asx ⊕s 1→* (_ l' _) ⊕ 1"
by(fastforce intro:path_CondTrue)
with WCFG_CondTrue[of b prog1 prog2]
have "if (b) prog1 else prog2 ⊢ (_0_)
-((_0_),(λs. interpret b s = Some true)⇩√,(_0_) ⊕ 1)#(asx ⊕s 1)→*
(_ l' _) ⊕ 1"
by(fastforce intro:While_CFG.Cons_path simp:valid_edge_def)
with WCFG_Entry[of "if (b) prog1 else prog2"]
have "if (b) prog1 else prog2 ⊢ (_Entry_) -((_Entry_),(λs. True)⇩√,(_0_))#
((_0_),(λs. interpret b s = Some true)⇩√,(_0_) ⊕ 1)#(asx ⊕s 1)→*
(_ l' _) ⊕ 1"
by(fastforce intro:While_CFG.Cons_path simp:valid_edge_def)
with ‹if (b) prog1 else prog2 ⊢ (_ l _) -as ⊕s 1→* (_Exit_)›
show ?thesis by simp blast
next
case False
hence "#:prog1 ≤ l'" by simp
then obtain l'' where [simp]:"l' = l'' + #:prog1" and "l'' = l' - #:prog1"
by simp
from ‹l < #:(if (b) prog1 else prog2)›
have "l'' < #:prog2" by simp
from IH2[OF this] obtain as as' where "prog2 ⊢ (_ l'' _) -as→* (_Exit_)"
and "prog2 ⊢ (_Entry_) -as'→* (_ l'' _)" by blast
from ‹prog2 ⊢ (_ l'' _) -as→* (_Exit_)›
have "if (b) prog1 else prog2 ⊢ (_ l'' _) ⊕ (#:prog1 + 1)
-as ⊕s (#:prog1 + 1)→* (_Exit_) ⊕ (#:prog1 + 1)"
by(fastforce intro:path_CondFalse)
hence "if (b) prog1 else prog2 ⊢ (_ l _) -as ⊕s (#:prog1 + 1)→* (_Exit_)"
by(simp add:add.assoc)
from ‹prog2 ⊢ (_Entry_) -as'→* (_ l'' _)› obtain ax asx
where "prog2 ⊢ (_Entry_) -ax#asx→* (_ l'' _)"
by(cases as',auto elim:While_CFG.cases)
hence "(_Entry_) = sourcenode ax" and "valid_edge prog2 ax"
and "prog2 ⊢ targetnode ax -asx→* (_ l'' _)"
by(auto intro:While_CFG.path_split_Cons)
hence "targetnode ax = (_0_)" by(fastforce dest:WCFG_EntryD simp:valid_edge_def)
with ‹prog2 ⊢ targetnode ax -asx→* (_ l'' _)›
have "if (b) prog1 else prog2 ⊢ (_0_) ⊕ (#:prog1 + 1) -asx ⊕s (#:prog1 + 1)→*
(_ l'' _) ⊕ (#:prog1 + 1)"
by(fastforce intro:path_CondFalse)
with WCFG_CondFalse[of b prog1 prog2]
have "if (b) prog1 else prog2 ⊢ (_0_)
-((_0_),(λs. interpret b s = Some false)⇩√,(_0_) ⊕ (#:prog1 + 1))#
(asx ⊕s (#:prog1 + 1))→* (_ l'' _) ⊕ (#:prog1 + 1)"
by(fastforce intro:While_CFG.Cons_path simp:valid_edge_def)
with WCFG_Entry[of "if (b) prog1 else prog2"]
have "if (b) prog1 else prog2 ⊢ (_Entry_) -((_Entry_),(λs. True)⇩√,(_0_))#
((_0_),(λs. interpret b s = Some false)⇩√,(_0_) ⊕ (#:prog1 + 1))#
(asx ⊕s (#:prog1 + 1))→* (_ l'' _) ⊕ (#:prog1 + 1)"
by(fastforce intro:While_CFG.Cons_path simp:valid_edge_def)
with
‹if (b) prog1 else prog2 ⊢ (_ l _) -as ⊕s (#:prog1 + 1)→* (_Exit_)›
show ?thesis by(simp add:add.assoc,blast)
qed
qed
next
case (While b prog')
note IH = ‹⋀l. l < #:prog' ⟹
(∃as. prog' ⊢ (_ l _) -as→* (_Exit_)) ∧ (∃as. prog' ⊢ (_Entry_) -as→* (_ l _))›
show ?case
proof(cases "l < 1")
case True
from WCFG_Entry[of "while (b) prog'"]
have "while (b) prog' ⊢ (_Entry_) -[((_Entry_),(λs. True)⇩√,(_0_))]→* (_0_)"
by(fastforce intro:While_CFG.Cons_path While_CFG.empty_path
simp:While_CFG.valid_node_def valid_edge_def)
from WCFG_WhileFalseSkip[of b prog']
have "while (b) prog' ⊢ (_1_) -[((_1_),⇑id,(_Exit_))]→* (_Exit_)"
by(fastforce intro:While_CFG.Cons_path While_CFG.empty_path
simp:valid_node_def valid_edge_def)
with WCFG_WhileFalse[of b prog']
have "while (b) prog' ⊢ (_0_) -((_0_),(λs. interpret b s = Some false)⇩√,(_1_))#
[((_1_),⇑id,(_Exit_))]→* (_Exit_)"
by(fastforce intro:While_CFG.Cons_path While_CFG.empty_path
simp:valid_node_def valid_edge_def)
with ‹while (b) prog' ⊢ (_Entry_) -[((_Entry_),(λs. True)⇩√,(_0_))]→* (_0_)› True
show ?thesis by simp blast
next
case False
hence "1 ≤ l" by simp
thus ?thesis
proof(cases "l < 2")
case True
with ‹1 ≤ l› have [simp]:"l = 1" by simp
from WCFG_WhileFalseSkip[of b prog']
have "while (b) prog' ⊢ (_1_) -[((_1_),⇑id,(_Exit_))]→* (_Exit_)"
by(fastforce intro:While_CFG.Cons_path While_CFG.empty_path
simp:valid_node_def valid_edge_def)
from WCFG_WhileFalse[of b prog']
have "while (b) prog' ⊢ (_0_)
-[((_0_),(λs. interpret b s = Some false)⇩√,(_1_))]→* (_1_)"
by(fastforce intro:While_CFG.Cons_path While_CFG.empty_path
simp:While_CFG.valid_node_def valid_edge_def)
with WCFG_Entry[of "while (b) prog'"]
have "while (b) prog' ⊢ (_Entry_) -((_Entry_),(λs. True)⇩√,(_0_))#
[((_0_),(λs. interpret b s = Some false)⇩√,(_1_))]→* (_1_)"
by(fastforce intro:While_CFG.Cons_path simp:valid_node_def valid_edge_def)
with ‹while (b) prog' ⊢ (_1_) -[((_1_),⇑id,(_Exit_))]→* (_Exit_)›
show ?thesis by simp blast
next
case False
with ‹1 ≤ l› have "2 ≤ l" by simp
then obtain l' where [simp]:"l = l' + 2" and "l' = l - 2"
by(simp del:add_2_eq_Suc')
from ‹l < #:while (b) prog'› have "l' < #:prog'" by simp
from IH[OF this] obtain as as' where "prog' ⊢ (_ l' _) -as→* (_Exit_)"
and "prog' ⊢ (_Entry_) -as'→* (_ l' _)" by blast
from ‹prog' ⊢ (_ l' _) -as→* (_Exit_)› obtain ax asx where
"prog' ⊢ (_ l' _) -asx@[ax]→* (_Exit_)"
by(induct as rule:rev_induct,auto elim:While_CFG.cases)
hence "prog' ⊢ (_ l' _) -asx→* sourcenode ax" and "valid_edge prog' ax"
and "(_Exit_) = targetnode ax"
by(auto intro:While_CFG.path_split_snoc)
then obtain lx where "sourcenode ax = (_ lx _)"
by(cases "sourcenode ax") auto
with ‹prog' ⊢ (_ l' _) -asx→* sourcenode ax›
have "while (b) prog' ⊢ (_ l' _) ⊕ 2 -asx ⊕s 2→* sourcenode ax ⊕ 2"
by(fastforce intro:path_While simp del:label_incr.simps)
from WCFG_WhileFalseSkip[of b prog']
have "while (b) prog' ⊢ (_1_) -[((_1_),⇑id,(_Exit_))]→* (_Exit_)"
by(fastforce intro:While_CFG.Cons_path While_CFG.empty_path
simp:valid_node_def valid_edge_def)
with WCFG_WhileFalse[of b prog']
have "while (b) prog' ⊢ (_0_) -((_0_),(λs. interpret b s = Some false)⇩√,(_1_))#
[((_1_),⇑id,(_Exit_))]→* (_Exit_)"
by(fastforce intro:While_CFG.Cons_path simp:valid_node_def valid_edge_def)
with ‹valid_edge prog' ax› ‹(_Exit_) = targetnode ax› ‹sourcenode ax = (_ lx _)›
have "while (b) prog' ⊢ sourcenode ax ⊕ 2 -(sourcenode ax ⊕ 2,kind ax,(_0_))#
((_0_),(λs. interpret b s = Some false)⇩√,(_1_))#
[((_1_),⇑id,(_Exit_))]→* (_Exit_)"
by(fastforce intro:While_CFG.Cons_path dest:WCFG_WhileBodyExit
simp:valid_node_def valid_edge_def)
with ‹while (b) prog' ⊢ (_ l' _) ⊕ 2 -asx ⊕s 2→* sourcenode ax ⊕ 2›
have path:"while (b) prog' ⊢ (_ l' _) ⊕ 2 -(asx ⊕s 2)@
((sourcenode ax ⊕ 2,kind ax,(_0_))#
((_0_),(λs. interpret b s = Some false)⇩√,(_1_))#
[((_1_),⇑id,(_Exit_))])→* (_Exit_)"
by(rule While_CFG.path_Append)
from ‹prog' ⊢ (_Entry_) -as'→* (_ l' _)› obtain ax' asx'
where "prog' ⊢ (_Entry_) -ax'#asx'→* (_ l' _)"
by(cases as',auto elim:While_CFG.cases)
hence "(_Entry_) = sourcenode ax'" and "valid_edge prog' ax'"
and "prog' ⊢ targetnode ax' -asx'→* (_ l' _)"
by(auto intro:While_CFG.path_split_Cons)
hence "targetnode ax' = (_0_)" by(fastforce dest:WCFG_EntryD simp:valid_edge_def)
with ‹prog' ⊢ targetnode ax' -asx'→* (_ l' _)›
have "while (b) prog' ⊢ (_0_) ⊕ 2 -asx' ⊕s 2→* (_ l' _) ⊕ 2"
by(fastforce intro:path_While)
with WCFG_WhileTrue[of b prog']
have "while (b) prog' ⊢ (_0_)
-((_0_),(λs. interpret b s = Some true)⇩√,(_0_) ⊕ 2)#(asx' ⊕s 2)→*
(_ l' _) ⊕ 2"
by(fastforce intro:While_CFG.Cons_path simp:valid_node_def valid_edge_def)
with WCFG_Entry[of "while (b) prog'"]
have "while (b) prog' ⊢ (_Entry_) -((_Entry_),(λs. True)⇩√,(_0_))#
((_0_),(λs. interpret b s = Some true)⇩√,(_0_) ⊕ 2)#(asx' ⊕s 2)→*
(_ l' _) ⊕ 2"
by(fastforce intro:While_CFG.Cons_path simp:valid_node_def valid_edge_def)
with path show ?thesis by simp blast
qed
qed
qed
declare add_2_eq_Suc' [simp] One_nat_def [simp]
lemma valid_node_Exit_path:
assumes "valid_node prog n" shows "∃as. prog ⊢ n -as→* (_Exit_)"
proof(cases n)
case (Node l)
with ‹valid_node prog n› have "l < #:prog"
by(fastforce dest:WCFG_sourcelabel_less_num_nodes WCFG_targetlabel_less_num_nodes
simp:valid_node_def valid_edge_def)
with Node show ?thesis by(fastforce dest:inner_node_Entry_Exit_path)
next
case Entry
from WCFG_Entry_Exit[of prog]
have "prog ⊢ (_Entry_) -[((_Entry_),(λs. False)⇩√,(_Exit_))]→* (_Exit_)"
by(fastforce intro:While_CFG.Cons_path While_CFG.empty_path
simp:valid_node_def valid_edge_def)
with Entry show ?thesis by blast
next
case Exit
with WCFG_Entry_Exit[of prog]
have "prog ⊢ n -[]→* (_Exit_)"
by(fastforce intro:While_CFG.empty_path simp:valid_node_def valid_edge_def)
thus ?thesis by blast
qed
lemma valid_node_Entry_path:
assumes "valid_node prog n" shows "∃as. prog ⊢ (_Entry_) -as→* n"
proof(cases n)
case (Node l)
with ‹valid_node prog n› have "l < #:prog"
by(fastforce dest:WCFG_sourcelabel_less_num_nodes WCFG_targetlabel_less_num_nodes
simp:valid_node_def valid_edge_def)
with Node show ?thesis by(fastforce dest:inner_node_Entry_Exit_path)
next
case Entry
with WCFG_Entry_Exit[of prog]
have "prog ⊢ (_Entry_) -[]→* n"
by(fastforce intro:While_CFG.empty_path simp:valid_node_def valid_edge_def)
thus ?thesis by blast
next
case Exit
from WCFG_Entry_Exit[of prog]
have "prog ⊢ (_Entry_) -[((_Entry_),(λs. False)⇩√,(_Exit_))]→* (_Exit_)"
by(fastforce intro:While_CFG.Cons_path While_CFG.empty_path
simp:valid_node_def valid_edge_def)
with Exit show ?thesis by blast
qed
subsection ‹Some finiteness considerations›
lemma finite_labels:"finite {l. ∃c. labels prog l c}"
proof -
have "finite {l::nat. l < #:prog}" by(fastforce intro:nat_seg_image_imp_finite)
moreover have "{l. ∃c. labels prog l c} ⊆ {l::nat. l < #:prog}"
by(fastforce intro:label_less_num_inner_nodes)
ultimately show ?thesis by(auto intro:finite_subset)
qed
lemma finite_valid_nodes:"finite {n. valid_node prog n}"
proof -
have "{n. ∃n' et. prog ⊢ n -et→ n'} ⊆
insert (_Entry_) ((λl'. (_ l' _)) ` {l. ∃c. labels prog l c})"
apply clarsimp
apply(case_tac x,auto)
by(fastforce dest:WCFG_sourcelabel_less_num_nodes less_num_inner_nodes_label)
hence "finite {n. ∃n' et. prog ⊢ n -et→ n'}"
by(auto intro:finite_subset finite_imageI finite_labels)
have "{n'. ∃n et. prog ⊢ n -et→ n'} ⊆
insert (_Exit_) ((λl'. (_ l' _)) ` {l. ∃c. labels prog l c})"
apply clarsimp
apply(case_tac x,auto)
by(fastforce dest:WCFG_targetlabel_less_num_nodes less_num_inner_nodes_label)
hence "finite {n'. ∃n et. prog ⊢ n -et→ n'}"
by(auto intro:finite_subset finite_imageI finite_labels)
have "{n. ∃nx et nx'. prog ⊢ nx -et→ nx' ∧ (n = nx ∨ n = nx')} =
{n. ∃n' et. prog ⊢ n -et→ n'} Un {n'. ∃n et. prog ⊢ n -et→ n'}" by blast
with ‹finite {n. ∃n' et. prog ⊢ n -et→ n'}› ‹finite {n'. ∃n et. prog ⊢ n -et→ n'}›
have "finite {n. ∃nx et nx'. prog ⊢ nx -et→ nx' ∧ (n = nx ∨ n = nx')}"
by fastforce
thus ?thesis by(simp add:valid_node_def valid_edge_def)
qed
lemma finite_successors:
"finite {n'. ∃a'. valid_edge prog a' ∧ sourcenode a' = n ∧
targetnode a' = n'}"
proof -
have "{n'. ∃a'. valid_edge prog a' ∧ sourcenode a' = n ∧
targetnode a' = n'} ⊆ {n. valid_node prog n}"
by(auto simp:valid_edge_def valid_node_def)
thus ?thesis by(fastforce elim:finite_subset intro:finite_valid_nodes)
qed
end