Theory Slicing.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;;c2  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;; c2  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;;c2  n -kind a n''" by(simp add:valid_edge_def WCFG_SeqFirst)
  with IH prog;;c2  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  [] 
   c1;;prog  n  #:c1 -as ⊕s #:c1→* n'  #:c1"
proof(induct rule:While_CFG.path.induct)
  case (Cons_path n'' as n' a n)
  note IH = n''  (_Entry_); as  [] 
     c1;;prog  n''  #:c1 -as ⊕s #:c1→* n'  #:c1
  from valid_edge prog a sourcenode a = n targetnode a = n'' n  (_Entry_)
  have "c1;;prog  n  #:c1 -kind a n''  #:c1"
    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 #:c1 = [a] ⊕s #:c1"
    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 c1;;prog  n  #:c1 -kind a n''  #:c1
    have "c1;;prog  n  #:c1 -[(n,kind a,n')] ⊕s #:c1→* n'  #:c1"
      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 #:c1 = [a] ⊕s #:c1 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 "c1;;prog  n''  #:c1 -as ⊕s #:c1→* n'  #:c1" .
    with c1;;prog  n  #:c1 -kind a n''  #:c1 sourcenode a = n
      targetnode a = n'' [(n,kind a,n'')] ⊕s #:c1 = [a] ⊕s #:c1 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 c2  (_ 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 c2]
  have "CFG.valid_node sourcenode targetnode (valid_edge (if (b) prog else c2)) 
    ((_ 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 c2  (_ l _)  1 -as ⊕s 1→* n'  1
  from valid_edge prog a sourcenode a = (_ l _)  targetnode a = n''
  have "if (b) prog else c2  (_ 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 c2  (_ l' _)  1 -as ⊕s 1→* n'  1" .
    with if (b) prog else c2  (_ l _)  1 -kind a n''  1 Node
    have "if (b) prog else c2  (_ 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 c2  (_ 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 c2  (_ l _)  1 -kind a n''  1 
    have "if (b) prog else c2  (_ 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) c1 else prog  (_ l _)  (#:c1 + 1) -as ⊕s (#:c1 + 1)→* n'  (#:c1 + 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 c1 prog]
  have "CFG.valid_node sourcenode targetnode (valid_edge (if (b) c1 else prog))
    ((_ l _)  #:c1 + 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) c1 else prog  (_ l _)  (#:c1 + 1) 
                                               -as ⊕s (#:c1 + 1)→* n'  (#:c1 + 1)
  from valid_edge prog a sourcenode a = (_ l _)  targetnode a = n''
  have "if (b) c1 else prog  (_ l _)  (#:c1 + 1) -kind a n''  (#:c1 + 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 (#:c1 + 1) = [a] ⊕s (#:c1 + 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) c1 else prog  (_ l' _)  (#:c1 + 1) 
                                             -as ⊕s (#:c1 + 1)→* n'  (#:c1 + 1)" .
    with if (b) c1 else prog  (_ l _)  (#:c1 + 1) -kind a n''  (#:c1 + 1) Node
    have "if (b) c1 else prog  (_ l _)  (#:c1 + 1) 
      -((_ l _)  (#:c1 + 1),kind a,n''  (#:c1 + 1))#(as ⊕s (#:c1 + 1))→* 
      n'  (#:c1 + 1)"
      by(fastforce intro:While_CFG.Cons_path simp:valid_edge_def valid_node_def)
    with [((_ l _),kind a,n'')] ⊕s (#:c1 + 1) = [a] ⊕s (#:c1 + 1) Node
    have "if (b) c1 else prog  (_ l _)  (#:c1 + 1) -a#as ⊕s (#:c1 + 1)→* 
                                n'  (#:c1 + 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) c1 else prog  (_ l _)  (#:c1 + 1) -kind a n''  (#:c1 + 1)
    have "if (b) c1 else prog  (_ l _)  (#:c1 + 1) 
          -[((_ l _)  (#:c1 + 1),kind a,n''  (#:c1 + 1))]→* n''  (#:c1 + 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 (#:c1 + 1) = [a] ⊕s (#:c1 + 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