Up to index of Isabelle/HOL/Jinja/Slicing
theory AdditionalLemmasheader {* \isaheader{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"
("_ \<turnstile> _ -_->* _")
where "prog \<turnstile> 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 \<turnstile> n -as->* (_ l _) ==> prog;;c⇣2 \<turnstile> 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 \<turnstile> n'' -as->* (_ l _)`
from `prog \<turnstile> n'' -as->* (_ l _)` have "n'' ≠ (_Exit_)"
by fastforce
with `valid_edge prog a` `sourcenode a = n` `targetnode a = n''`
have "prog;;c⇣2 \<turnstile> n -kind a-> n''" by(simp add:valid_edge_def WCFG_SeqFirst)
with IH `prog;;c⇣2 \<turnstile> 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 \<turnstile> n -as->* n'; n ≠ (_Entry_); as ≠ []|]
==> c⇣1;;prog \<turnstile> 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 \<turnstile> 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 \<turnstile> 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 \<turnstile> n'' -as->* n'` have [simp]:"n'' = n'" by(auto elim:While_CFG.cases)
with `c⇣1;;prog \<turnstile> n ⊕ #:c⇣1 -kind a-> n'' ⊕ #:c⇣1`
have "c⇣1;;prog \<turnstile> 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 \<turnstile> n'' ⊕ #:c⇣1 -as ⊕s #:c⇣1->* n' ⊕ #:c⇣1" .
with `c⇣1;;prog \<turnstile> 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 \<turnstile> (_ l _) -as->* n'
==> if (b) prog else c⇣2 \<turnstile> (_ 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 \<turnstile> (_ 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 \<turnstile> (_ 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 \<turnstile> (_ l' _) ⊕ 1 -as ⊕s 1->* n' ⊕ 1" .
with `if (b) prog else c⇣2 \<turnstile> (_ l _) ⊕ 1 -kind a-> n'' ⊕ 1` Node
have "if (b) prog else c⇣2 \<turnstile> (_ 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 \<turnstile> (_ 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 \<turnstile> n'' -as->* n'` have "n' = (_Exit_)" and "as = []"
by(auto dest:While_CFGExit.path_Exit_source)
from `if (b) prog else c⇣2 \<turnstile> (_ l _) ⊕ 1 -kind a-> n'' ⊕ 1`
have "if (b) prog else c⇣2 \<turnstile> (_ 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 \<turnstile> (_ l _) -as->* n'
==> if (b) c⇣1 else prog \<turnstile> (_ 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 \<turnstile> (_ 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 \<turnstile> (_ 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 \<turnstile> (_ l' _) ⊕ (#:c⇣1 + 1)
-as ⊕s (#:c⇣1 + 1)->* n' ⊕ (#:c⇣1 + 1)" .
with `if (b) c⇣1 else prog \<turnstile> (_ l _) ⊕ (#:c⇣1 + 1) -kind a-> n'' ⊕ (#:c⇣1 + 1)` Node
have "if (b) c⇣1 else prog \<turnstile> (_ 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 \<turnstile> (_ 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 \<turnstile> n'' -as->* n'` have "n' = (_Exit_)" and "as = []"
by(auto dest:While_CFGExit.path_Exit_source)
from `if (b) c⇣1 else prog \<turnstile> (_ l _) ⊕ (#:c⇣1 + 1) -kind a-> n'' ⊕ (#:c⇣1 + 1)`
have "if (b) c⇣1 else prog \<turnstile> (_ 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 \<turnstile> (_ l _) -as->* (_ l' _)
==> while (b) prog \<turnstile> (_ 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 \<turnstile> (_ 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 \<turnstile> (_ l _) ⊕ 2 -kind a-> n'' ⊕ 2"
by -(rule WCFG_WhileBody,simp_all add:valid_edge_def)
from IH[OF Node]
have "while (b) prog \<turnstile> (_ l'' _) ⊕ 2 -as ⊕s 2->* (_ l' _) ⊕ 2" .
with `while (b) prog \<turnstile> (_ l _) ⊕ 2 -kind a-> n'' ⊕ 2` Node
have "while (b) prog \<turnstile> (_ 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 \<turnstile> 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 \<turnstile> (_ l _) -as->* (_Exit_)) ∧
(∃as. prog \<turnstile> (_Entry_) -as->* (_ l _))"
proof(induct prog arbitrary:l)
case Skip
from `l < #:Skip` have [simp]:"l = 0" by simp
hence "Skip \<turnstile> (_ l _) -\<Up>id-> (_Exit_)" by(simp add:WCFG_Skip)
hence "Skip \<turnstile> (_ l _) -[((_ l _),\<Up>id,(_Exit_))]->* (_Exit_)"
by (fastforce intro: While_CFG.path.intros simp: valid_edge_def)
have "Skip \<turnstile> (_Entry_) -(λs. True)⇣\<surd>-> (_ l _)" by(simp add:WCFG_Entry)
hence "Skip \<turnstile> (_Entry_) -[((_Entry_),(λs. True)⇣\<surd>,(_ l _))]->* (_ l _)"
by(fastforce intro:While_CFG.path.intros simp:valid_edge_def While_CFG.valid_node_def)
with `Skip \<turnstile> (_ l _) -[((_ l _),\<Up>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 \<turnstile> (_Entry_) -(λs. True)⇣\<surd>-> (_ l _)" by(simp add:WCFG_Entry)
hence "V:=e \<turnstile> (_Entry_) -[((_Entry_),(λs. True)⇣\<surd>,(_ l _))]->* (_ l _)"
by(fastforce intro:While_CFG.path.intros simp:valid_edge_def While_CFG.valid_node_def)
have "V:=e \<turnstile> (_1_) -\<Up>id-> (_Exit_)" by(rule WCFG_LAssSkip)
hence "V:=e \<turnstile> (_1_) -[((_1_),\<Up>id,(_Exit_))]->* (_Exit_)"
by(fastforce intro:While_CFG.path.intros simp:valid_edge_def)
with WCFG_LAss have "V:=e \<turnstile> (_ l _) -
[((_ l _),\<Up>(λs. s(V:=(interpret e s))),(_1_)),((_1_),\<Up>id,(_Exit_))]->*
(_Exit_)"
by(fastforce intro:While_CFG.path.intros simp:valid_edge_def)
with `V:=e \<turnstile> (_Entry_) -[((_Entry_),(λs. True)⇣\<surd>,(_ l _))]->* (_ l _)`
show ?case by fastforce
next
assume [simp]:"l = 1"
hence "V:=e \<turnstile> (_ l _) -\<Up>id-> (_Exit_)" by(simp add:WCFG_LAssSkip)
hence "V:=e \<turnstile> (_ l _) -[((_ l _),\<Up>id,(_Exit_))]->* (_Exit_)"
by(fastforce intro:While_CFG.path.intros simp:valid_edge_def)
have "V:=e \<turnstile> (_0_) -\<Up>(λs. s(V:=(interpret e s)))-> (_ l _)"
by(simp add:WCFG_LAss)
hence "V:=e \<turnstile> (_0_) -[((_0_),\<Up>(λ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 \<turnstile> (_Entry_) -[((_Entry_),(λs. True)⇣\<surd>,(_0_))
,((_0_),\<Up>(λs. s(V:=(interpret e s))),(_ l _))]->* (_ l _)"
by(fastforce intro:While_CFG.path.intros simp:valid_edge_def)
with `V:=e \<turnstile> (_ l _) -[((_ l _),\<Up>id,(_Exit_))]->* (_Exit_)` show ?case by fastforce
qed
next
case (Seq prog1 prog2)
note IH1 = `!!l. l < #:prog1 ==>
(∃as. prog1 \<turnstile> (_ l _) -as->* (_Exit_)) ∧ (∃as. prog1 \<turnstile> (_Entry_) -as->* (_ l _))`
note IH2 = `!!l. l < #:prog2 ==>
(∃as. prog2 \<turnstile> (_ l _) -as->* (_Exit_)) ∧ (∃as. prog2 \<turnstile> (_Entry_) -as->* (_ l _))`
show ?case
proof(cases "l < #:prog1")
case True
from IH1[OF True] obtain as as' where "prog1 \<turnstile> (_ l _) -as->* (_Exit_)"
and "prog1 \<turnstile> (_Entry_) -as'->* (_ l _)" by blast
from `prog1 \<turnstile> (_Entry_) -as'->* (_ l _)`
have "prog1;;prog2 \<turnstile> (_Entry_) -as'->* (_ l _)"
by(fastforce intro:path_SeqFirst)
from `prog1 \<turnstile> (_ l _) -as->* (_Exit_)`
obtain asx ax where "prog1 \<turnstile> (_ l _) -asx@[ax]->* (_Exit_)"
by(induct rule:rev_induct,auto elim:While_CFG.path.cases)
hence "prog1 \<turnstile> (_ l _) -asx->* sourcenode ax"
and "valid_edge prog1 ax" and "(_Exit_) = targetnode ax"
by(auto intro:While_CFG.path_split_snoc)
from `prog1 \<turnstile> (_ l _) -asx->* sourcenode ax` `valid_edge prog1 ax`
obtain lx where [simp]:"sourcenode ax = (_ lx _)"
by(cases "sourcenode ax") auto
with `prog1 \<turnstile> (_ l _) -asx->* sourcenode ax`
have "prog1;;prog2 \<turnstile> (_ l _) -asx->* sourcenode ax"
by(fastforce intro:path_SeqFirst)
from `valid_edge prog1 ax` `(_Exit_) = targetnode ax`
have "prog1;;prog2 \<turnstile> sourcenode ax -kind ax-> (_0_) ⊕ #:prog1"
by(fastforce intro:WCFG_SeqConnect simp:valid_edge_def)
hence "prog1;;prog2 \<turnstile> 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 \<turnstile> (_ l _) -asx->* sourcenode ax`
have "prog1;;prog2 \<turnstile> (_ 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 \<turnstile> (_ 0 _) -as''->* (_Exit_)" by blast
hence "prog1;;prog2 \<turnstile> (_0_) ⊕ #:prog1 -as'' ⊕s #:prog1->* (_Exit_) ⊕ #:prog1"
by(fastforce intro!:path_SeqSecond elim:While_CFG.path.cases)
hence "prog1;;prog2 \<turnstile> (_0_) ⊕ #:prog1 -as'' ⊕s #:prog1->* (_Exit_)"
by simp
with `prog1;;prog2 \<turnstile> (_ l _) -asx@[(sourcenode ax,kind ax,(_0_) ⊕ #:prog1)]->*
(_0_) ⊕ #:prog1`
have "prog1;;prog2 \<turnstile> (_ l _) -(asx@[(sourcenode ax,kind ax,(_0_) ⊕ #:prog1)])@
(as'' ⊕s #:prog1)->* (_Exit_)"
by(fastforce intro:While_CFG.path_Append)
with `prog1;;prog2 \<turnstile> (_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 \<turnstile> (_ l' _) -as->* (_Exit_)"
and "prog2 \<turnstile> (_Entry_) -as'->* (_ l' _)" by blast
from `prog2 \<turnstile> (_ l' _) -as->* (_Exit_)`
have "prog1;;prog2 \<turnstile> (_ l' _) ⊕ #:prog1 -as ⊕s #:prog1->* (_Exit_) ⊕ #:prog1"
by(fastforce intro!:path_SeqSecond elim:While_CFG.path.cases)
hence "prog1;;prog2 \<turnstile> (_ l _) -as ⊕s #:prog1->* (_Exit_)"
by simp
from IH1[of 0] obtain as'' where "prog1 \<turnstile> (_0_) -as''->* (_Exit_)" by blast
then obtain ax asx where "prog1 \<turnstile> (_0_) -asx@[ax]->* (_Exit_)"
by(induct rule:rev_induct,auto elim:While_CFG.path.cases)
hence "prog1 \<turnstile> (_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 \<turnstile> (_0_) -asx->* sourcenode ax`
have "prog1 \<turnstile> (_Entry_) -((_Entry_),(λs. True)⇣\<surd>,(_0_))#asx->* sourcenode ax"
by(fastforce intro:While_CFG.Cons_path simp:valid_edge_def valid_node_def)
from `prog1 \<turnstile> (_0_) -asx->* sourcenode ax` `valid_edge prog1 ax`
obtain lx where [simp]:"sourcenode ax = (_ lx _)"
by(cases "sourcenode ax") auto
with `prog1 \<turnstile> (_Entry_) -((_Entry_),(λs. True)⇣\<surd>,(_0_))#asx->* sourcenode ax`
have "prog1;;prog2 \<turnstile> (_Entry_) -((_Entry_),(λs. True)⇣\<surd>,(_0_))#asx->*
sourcenode ax"
by(fastforce intro:path_SeqFirst)
from `prog2 \<turnstile> (_Entry_) -as'->* (_ l' _)` obtain ax' asx'
where "prog2 \<turnstile> (_Entry_) -ax'#asx'->* (_ l' _)"
by(cases as',auto elim:While_CFG.path.cases)
hence "(_Entry_) = sourcenode ax'" and "valid_edge prog2 ax'"
and "prog2 \<turnstile> 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 \<turnstile> sourcenode ax -kind ax-> (_0_) ⊕ #:prog1"
by(fastforce intro:WCFG_SeqConnect simp:valid_edge_def)
have "∃as. prog1;;prog2 \<turnstile> sourcenode ax -as->* (_ l _)"
proof(cases "asx' = []")
case True
with `prog2 \<turnstile> targetnode ax' -asx'->* (_ l' _)` `targetnode ax' = (_0_)`
have "l' = 0" by(auto elim:While_CFG.path.cases)
with `prog1;;prog2 \<turnstile> sourcenode ax -kind ax-> (_0_) ⊕ #:prog1`
have "prog1;;prog2 \<turnstile> 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 \<turnstile> targetnode ax' -asx'->* (_ l' _)` `targetnode ax' = (_0_)`
have "prog1;;prog2 \<turnstile> (_0_) ⊕ #:prog1 -asx' ⊕s #:prog1->* (_ l' _) ⊕ #:prog1"
by(fastforce intro:path_SeqSecond)
hence "prog1;;prog2 \<turnstile> (_0_) ⊕ #:prog1 -asx' ⊕s #:prog1->* (_ l _)" by simp
with `prog1;;prog2 \<turnstile> sourcenode ax -kind ax-> (_0_) ⊕ #:prog1`
have "prog1;;prog2 \<turnstile> 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 \<turnstile> sourcenode ax -asx''->* (_ l _)" by blast
with `prog1;;prog2 \<turnstile> (_Entry_) -((_Entry_),(λs. True)⇣\<surd>,(_0_))#asx->*
sourcenode ax`
have "prog1;;prog2 \<turnstile> (_Entry_) -(((_Entry_),(λs. True)⇣\<surd>,(_0_))#asx)@asx''->*
(_ l _)"
by(rule While_CFG.path_Append)
with `prog1;;prog2 \<turnstile> (_ l _) -as ⊕s #:prog1->* (_Exit_)`
show ?thesis by blast
qed
next
case (Cond b prog1 prog2)
note IH1 = `!!l. l < #:prog1 ==>
(∃as. prog1 \<turnstile> (_ l _) -as->* (_Exit_)) ∧ (∃as. prog1 \<turnstile> (_Entry_) -as->* (_ l _))`
note IH2 = `!!l. l < #:prog2 ==>
(∃as. prog2 \<turnstile> (_ l _) -as->* (_Exit_)) ∧ (∃as. prog2 \<turnstile> (_Entry_) -as->* (_ l _))`
show ?case
proof(cases "l = 0")
case True
from IH1[of 0] obtain as where "prog1 \<turnstile> (_0_) -as->* (_Exit_)" by blast
hence "if (b) prog1 else prog2 \<turnstile> (_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 \<turnstile>
(_0_) -((_0_),(λs. interpret b s = Some true)⇣\<surd>,(_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 \<turnstile>
(_ l _) -((_0_),(λs. interpret b s = Some true)⇣\<surd>,(_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 \<turnstile> (_Entry_) -[((_Entry_),(λs. True)⇣\<surd>,(_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 \<turnstile> (_ l' _) -as->* (_Exit_)"
and "prog1 \<turnstile> (_Entry_) -as'->* (_ l' _)" by blast
from `prog1 \<turnstile> (_ l' _) -as->* (_Exit_)`
have "if (b) prog1 else prog2 \<turnstile> (_ l' _) ⊕ 1 -as ⊕s 1->* (_Exit_) ⊕ 1"
by(fastforce intro:path_CondTrue)
hence "if (b) prog1 else prog2 \<turnstile> (_ l _) -as ⊕s 1->* (_Exit_)"
by simp
from `prog1 \<turnstile> (_Entry_) -as'->* (_ l' _)` obtain ax asx
where "prog1 \<turnstile> (_Entry_) -ax#asx->* (_ l' _)"
by(cases as',auto elim:While_CFG.cases)
hence "(_Entry_) = sourcenode ax" and "valid_edge prog1 ax"
and "prog1 \<turnstile> 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 \<turnstile> targetnode ax -asx->* (_ l' _)`
have "if (b) prog1 else prog2 \<turnstile> (_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 \<turnstile> (_0_)
-((_0_),(λs. interpret b s = Some true)⇣\<surd>,(_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 \<turnstile> (_Entry_) -((_Entry_),(λs. True)⇣\<surd>,(_0_))#
((_0_),(λs. interpret b s = Some true)⇣\<surd>,(_0_) ⊕ 1)#(asx ⊕s 1)->*
(_ l' _) ⊕ 1"
by(fastforce intro:While_CFG.Cons_path simp:valid_edge_def)
with `if (b) prog1 else prog2 \<turnstile> (_ 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 \<turnstile> (_ l'' _) -as->* (_Exit_)"
and "prog2 \<turnstile> (_Entry_) -as'->* (_ l'' _)" by blast
from `prog2 \<turnstile> (_ l'' _) -as->* (_Exit_)`
have "if (b) prog1 else prog2 \<turnstile> (_ l'' _) ⊕ (#:prog1 + 1)
-as ⊕s (#:prog1 + 1)->* (_Exit_) ⊕ (#:prog1 + 1)"
by(fastforce intro:path_CondFalse)
hence "if (b) prog1 else prog2 \<turnstile> (_ l _) -as ⊕s (#:prog1 + 1)->* (_Exit_)"
by(simp add:nat_add_assoc)
from `prog2 \<turnstile> (_Entry_) -as'->* (_ l'' _)` obtain ax asx
where "prog2 \<turnstile> (_Entry_) -ax#asx->* (_ l'' _)"
by(cases as',auto elim:While_CFG.cases)
hence "(_Entry_) = sourcenode ax" and "valid_edge prog2 ax"
and "prog2 \<turnstile> 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 \<turnstile> targetnode ax -asx->* (_ l'' _)`
have "if (b) prog1 else prog2 \<turnstile> (_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 \<turnstile> (_0_)
-((_0_),(λs. interpret b s = Some false)⇣\<surd>,(_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 \<turnstile> (_Entry_) -((_Entry_),(λs. True)⇣\<surd>,(_0_))#
((_0_),(λs. interpret b s = Some false)⇣\<surd>,(_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 \<turnstile> (_ l _) -as ⊕s (#:prog1 + 1)->* (_Exit_)`
show ?thesis by(simp add:nat_add_assoc,blast)
qed
qed
next
case (While b prog')
note IH = `!!l. l < #:prog' ==>
(∃as. prog' \<turnstile> (_ l _) -as->* (_Exit_)) ∧ (∃as. prog' \<turnstile> (_Entry_) -as->* (_ l _))`
show ?case
proof(cases "l < 1")
case True
from WCFG_Entry[of "while (b) prog'"]
have "while (b) prog' \<turnstile> (_Entry_) -[((_Entry_),(λs. True)⇣\<surd>,(_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' \<turnstile> (_1_) -[((_1_),\<Up>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' \<turnstile> (_0_) -((_0_),(λs. interpret b s = Some false)⇣\<surd>,(_1_))#
[((_1_),\<Up>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' \<turnstile> (_Entry_) -[((_Entry_),(λs. True)⇣\<surd>,(_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' \<turnstile> (_1_) -[((_1_),\<Up>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' \<turnstile> (_0_)
-[((_0_),(λs. interpret b s = Some false)⇣\<surd>,(_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' \<turnstile> (_Entry_) -((_Entry_),(λs. True)⇣\<surd>,(_0_))#
[((_0_),(λs. interpret b s = Some false)⇣\<surd>,(_1_))]->* (_1_)"
by(fastforce intro:While_CFG.Cons_path simp:valid_node_def valid_edge_def)
with `while (b) prog' \<turnstile> (_1_) -[((_1_),\<Up>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' \<turnstile> (_ l' _) -as->* (_Exit_)"
and "prog' \<turnstile> (_Entry_) -as'->* (_ l' _)" by blast
from `prog' \<turnstile> (_ l' _) -as->* (_Exit_)` obtain ax asx where
"prog' \<turnstile> (_ l' _) -asx@[ax]->* (_Exit_)"
by(induct as rule:rev_induct,auto elim:While_CFG.cases)
hence "prog' \<turnstile> (_ 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' \<turnstile> (_ l' _) -asx->* sourcenode ax`
have "while (b) prog' \<turnstile> (_ 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' \<turnstile> (_1_) -[((_1_),\<Up>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' \<turnstile> (_0_) -((_0_),(λs. interpret b s = Some false)⇣\<surd>,(_1_))#
[((_1_),\<Up>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' \<turnstile> sourcenode ax ⊕ 2 -(sourcenode ax ⊕ 2,kind ax,(_0_))#
((_0_),(λs. interpret b s = Some false)⇣\<surd>,(_1_))#
[((_1_),\<Up>id,(_Exit_))]->* (_Exit_)"
by(fastforce intro:While_CFG.Cons_path dest:WCFG_WhileBodyExit
simp:valid_node_def valid_edge_def)
with `while (b) prog' \<turnstile> (_ l' _) ⊕ 2 -asx ⊕s 2->* sourcenode ax ⊕ 2`
have path:"while (b) prog' \<turnstile> (_ l' _) ⊕ 2 -(asx ⊕s 2)@
((sourcenode ax ⊕ 2,kind ax,(_0_))#
((_0_),(λs. interpret b s = Some false)⇣\<surd>,(_1_))#
[((_1_),\<Up>id,(_Exit_))])->* (_Exit_)"
by(rule While_CFG.path_Append)
from `prog' \<turnstile> (_Entry_) -as'->* (_ l' _)` obtain ax' asx'
where "prog' \<turnstile> (_Entry_) -ax'#asx'->* (_ l' _)"
by(cases as',auto elim:While_CFG.cases)
hence "(_Entry_) = sourcenode ax'" and "valid_edge prog' ax'"
and "prog' \<turnstile> 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' \<turnstile> targetnode ax' -asx'->* (_ l' _)`
have "while (b) prog' \<turnstile> (_0_) ⊕ 2 -asx' ⊕s 2->* (_ l' _) ⊕ 2"
by(fastforce intro:path_While)
with WCFG_WhileTrue[of b prog']
have "while (b) prog' \<turnstile> (_0_)
-((_0_),(λs. interpret b s = Some true)⇣\<surd>,(_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' \<turnstile> (_Entry_) -((_Entry_),(λs. True)⇣\<surd>,(_0_))#
((_0_),(λs. interpret b s = Some true)⇣\<surd>,(_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 \<turnstile> 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 \<turnstile> (_Entry_) -[((_Entry_),(λs. False)⇣\<surd>,(_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 \<turnstile> 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 \<turnstile> (_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 \<turnstile> (_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 \<turnstile> (_Entry_) -[((_Entry_),(λs. False)⇣\<surd>,(_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 \<turnstile> 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 \<turnstile> n -et-> n'}"
by(auto intro:finite_subset finite_imageI finite_labels)
have "{n'. ∃n et. prog \<turnstile> 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 \<turnstile> n -et-> n'}"
by(auto intro:finite_subset finite_imageI finite_labels)
have "{n. ∃nx et nx'. prog \<turnstile> nx -et-> nx' ∧ (n = nx ∨ n = nx')} =
{n. ∃n' et. prog \<turnstile> n -et-> n'} Un {n'. ∃n et. prog \<turnstile> n -et-> n'}" by blast
with `finite {n. ∃n' et. prog \<turnstile> n -et-> n'}` `finite {n'. ∃n et. prog \<turnstile> n -et-> n'}`
have "finite {n. ∃nx et nx'. prog \<turnstile> 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