Theory Slicing.WCFG

section ‹CFG›

theory WCFG imports Com "../Basic/BasicDefs" begin

subsection‹CFG nodes›

datatype w_node = Node nat ("'('_ _ '_')")
  | Entry ("'('_Entry'_')")
  | Exit ("'('_Exit'_')") 

fun label_incr :: "w_node  nat  w_node" ("_  _" 60)
where "(_ l _)  i = (_ l + i _)"
  | "(_Entry_)  i = (_Entry_)"
  | "(_Exit_)  i  = (_Exit_)"


lemma Exit_label_incr [dest]: "(_Exit_) = n  i  n = (_Exit_)"
  by(cases n,auto)

lemma label_incr_Exit [dest]: "n  i = (_Exit_)  n = (_Exit_)"
  by(cases n,auto)

lemma Entry_label_incr [dest]: "(_Entry_) = n  i  n = (_Entry_)"
  by(cases n,auto)

lemma label_incr_Entry [dest]: "n  i = (_Entry_)  n = (_Entry_)"
  by(cases n,auto)

lemma label_incr_inj:
  "n  c = n'  c  n = n'"
by(cases n)(cases n',auto)+

lemma label_incr_simp:"n  i = m  (i + j)  n = m  j"
by(cases n,auto,cases m,auto)

lemma label_incr_simp_rev:"m  (j + i) = n  i  m  j = n"
by(cases n,auto,cases m,auto)

lemma label_incr_start_Node_smaller:
  "(_ l _) = n  i  n = (_(l - i)_)"
by(cases n,auto)

lemma label_incr_ge:"(_ l _) = n  i  l  i"
by(cases n) auto

lemma label_incr_0 [dest]:
  "(_0_) = n  i; i > 0  False" 
by(cases n) auto

lemma label_incr_0_rev [dest]:
  "n  i = (_0_); i > 0  False" 
by(cases n) auto

subsection‹CFG edges›

type_synonym w_edge = "(w_node × state edge_kind × w_node)"

inductive While_CFG :: "cmd  w_node  state edge_kind  w_node  bool"
  ("_  _ -_ _")
where

WCFG_Entry_Exit:
  "prog  (_Entry_) -(λs. False) (_Exit_)"

| WCFG_Entry:
  "prog  (_Entry_) -(λs. True) (_0_)"

| WCFG_Skip: 
  "Skip  (_0_) -id (_Exit_)"

| WCFG_LAss: 
  "V:=e  (_0_) -(λs. s(V:=(interpret e s))) (_1_)"

| WCFG_LAssSkip:
  "V:=e  (_1_) -id (_Exit_)"

| WCFG_SeqFirst:
  "c1  n -et n'; n'  (_Exit_)  c1;;c2  n -et n'"

| WCFG_SeqConnect: 
  "c1  n -et (_Exit_); n  (_Entry_)  c1;;c2  n -et (_0_)  #:c1"

| WCFG_SeqSecond: 
  "c2  n -et n'; n  (_Entry_)  c1;;c2  n  #:c1 -et n'  #:c1"

| WCFG_CondTrue:
    "if (b) c1 else c2  (_0_) -(λs. interpret b s = Some true) (_0_)  1"

| WCFG_CondFalse:
    "if (b) c1 else c2  (_0_) -(λs. interpret b s = Some false) (_0_)  (#:c1 + 1)"

| WCFG_CondThen:
  "c1  n -et n'; n  (_Entry_)  if (b) c1 else c2  n  1 -et n'  1"

| WCFG_CondElse:
  "c2  n -et n'; n  (_Entry_) 
   if (b) c1 else c2  n  (#:c1 + 1) -et n'  (#:c1 + 1)"

| WCFG_WhileTrue:
    "while (b) c'  (_0_) -(λs. interpret b s = Some true) (_0_)  2"

| WCFG_WhileFalse:
    "while (b) c'  (_0_) -(λs. interpret b s = Some false) (_1_)"

| WCFG_WhileFalseSkip:
  "while (b) c'  (_1_) -id (_Exit_)"

| WCFG_WhileBody:
  "c'  n -et n'; n  (_Entry_); n'  (_Exit_) 
   while (b) c'  n  2 -et n'  2"

| WCFG_WhileBodyExit:
  "c'  n -et (_Exit_); n  (_Entry_)  while (b) c'  n  2 -et (_0_)"

lemmas WCFG_intros = While_CFG.intros[split_format (complete)]
lemmas WCFG_elims = While_CFG.cases[split_format (complete)]
lemmas WCFG_induct = While_CFG.induct[split_format (complete)]


subsection ‹Some lemmas about the CFG›

lemma WCFG_Exit_no_sourcenode [dest]:
  "prog  (_Exit_) -et n'  False"
by(induct prog n"(_Exit_)" et n' rule:WCFG_induct,auto)


lemma WCFG_Entry_no_targetnode [dest]:
  "prog  n -et (_Entry_)  False"
by(induct prog n et n'"(_Entry_)" rule:WCFG_induct,auto)


lemma WCFG_sourcelabel_less_num_nodes:
  "prog  (_ l _) -et n'  l < #:prog"
proof(induct prog "(_ l _)" et n' arbitrary:l rule:WCFG_induct)
  case (WCFG_SeqFirst c1 et n' c2)
  from l < #:c1 show ?case by simp
next
  case (WCFG_SeqConnect c1 et c2)
  from l < #:c1 show ?case by simp
next
  case (WCFG_SeqSecond c2 n et n' c1)
  note IH = l. n = (_ l _)  l < #:c2
  from n  #:c1 = (_ l _) obtain l' where "n = (_ l' _)" by(cases n) auto
  from IH[OF this] have "l' < #:c2" .
  with n  #:c1 = (_ l _) n = (_ l' _) show ?case by simp
next
  case (WCFG_CondThen c1 n et n' b c2)
  note IH = l. n = (_ l _)  l < #:c1
  from n  1 = (_ l _) obtain l' where "n = (_ l' _)" by(cases n) auto
  from IH[OF this] have "l' < #:c1" .
  with n  1 = (_ l _) n = (_ l' _) show ?case by simp
next
  case (WCFG_CondElse c2 n et n' b c1)
  note IH = l. n = (_ l _)  l < #:c2
  from n  (#:c1 + 1) = (_ l _) obtain l' where "n = (_ l' _)" by(cases n) auto
  from IH[OF this] have "l' < #:c2" .
  with n  (#:c1 + 1) = (_ l _) n = (_ l' _) show ?case by simp
next
  case (WCFG_WhileBody c' n et n' b)
  note IH = l. n = (_ l _)  l < #:c'
  from n  2 = (_ l _) obtain l' where "n = (_ l' _)" by(cases n) auto
  from IH[OF this] have "l' < #:c'" .
  with n  2 = (_ l _) n = (_ l' _) show ?case by simp
next
  case (WCFG_WhileBodyExit c' n et b)
  note IH = l. n = (_ l _)  l < #:c'
  from n  2 = (_ l _) obtain l' where "n = (_ l' _)" by(cases n) auto
  from IH[OF this] have "l' < #:c'" .
  with n  2 = (_ l _) n = (_ l' _) show ?case by simp
qed (auto simp:num_inner_nodes_gr_0)


lemma WCFG_targetlabel_less_num_nodes:
  "prog  n -et (_ l _)  l < #:prog"
proof(induct prog n et "(_ l _)" arbitrary:l rule:WCFG_induct)
  case (WCFG_SeqFirst c1 n et c2)
  from l < #:c1 show ?case by simp
next
  case (WCFG_SeqSecond c2 n et n' c1)
  note IH = l. n' = (_ l _)  l < #:c2
  from n'  #:c1 = (_ l _) obtain l' where "n' = (_ l' _)" by(cases n') auto
  from IH[OF this] have "l' < #:c2" .
  with n'  #:c1 = (_ l _) n' = (_ l' _) show ?case by simp
next
  case (WCFG_CondThen c1 n et n' b c2)
  note IH = l. n' = (_ l _)  l < #:c1
  from n'  1 = (_ l _) obtain l' where "n' = (_ l' _)" by(cases n') auto
  from IH[OF this] have "l' < #:c1" .
  with n'  1 = (_ l _) n' = (_ l' _) show ?case by simp
next
  case (WCFG_CondElse c2 n et n' b c1)
  note IH = l. n' = (_ l _)  l < #:c2
  from n'  (#:c1 + 1) = (_ l _) obtain l' where "n' = (_ l' _)" by(cases n') auto
  from IH[OF this] have "l' < #:c2" .
  with n'  (#:c1 + 1) = (_ l _) n' = (_ l' _) show ?case by simp
next
  case (WCFG_WhileBody c' n et n' b)
  note IH = l. n' = (_ l _)  l < #:c'
  from n'  2 = (_ l _) obtain l' where "n' = (_ l' _)" by(cases n') auto
  from IH[OF this] have "l' < #:c'" .
  with n'  2 = (_ l _) n' = (_ l' _) show ?case by simp
qed (auto simp:num_inner_nodes_gr_0)


lemma WCFG_EntryD:
  "prog  (_Entry_) -et n'
   (n' = (_Exit_)  et = (λs. False))  (n' = (_0_)  et = (λs. True))"
by(induct prog n"(_Entry_)" et n' rule:WCFG_induct,auto)


(*<*)declare One_nat_def [simp del] add_2_eq_Suc' [simp del](*>*)

lemma WCFG_edge_det:
  "prog  n -et n'; prog  n -et' n'  et = et'"
proof(induct rule:WCFG_induct)
  case WCFG_Entry_Exit thus ?case by(fastforce dest:WCFG_EntryD)
next
  case WCFG_Entry thus ?case by(fastforce dest:WCFG_EntryD)
next
  case WCFG_Skip thus ?case by(fastforce elim:WCFG_elims)
next
  case WCFG_LAss thus ?case by(fastforce elim:WCFG_elims)
next
  case WCFG_LAssSkip thus ?case by(fastforce elim:WCFG_elims)
next
  case (WCFG_SeqFirst c1 n et n' c2)
  note IH = c1  n -et' n'  et = et'
  from c1  n -et n' n'  (_Exit_) obtain l where "n' = (_ l _)"
    by (cases n') auto
  with c1  n -et n' have "l < #:c1" 
    by(fastforce intro:WCFG_targetlabel_less_num_nodes)
  with c1;;c2  n -et' n' n' = (_ l _) have "c1  n -et' n'"
    by(fastforce elim:WCFG_elims intro:WCFG_intros dest:label_incr_ge)
  from IH[OF this] show ?case .
next
  case (WCFG_SeqConnect c1 n et c2)
  note IH = c1  n -et' (_Exit_)  et = et'
  from c1  n -et (_Exit_) n  (_Entry_) obtain l where "n = (_ l _)"
    by (cases n) auto
  with c1  n -et (_Exit_) have "l < #:c1"
    by(fastforce intro:WCFG_sourcelabel_less_num_nodes)
  with c1;;c2  n -et' (_ 0 _)  #:c1 n = (_ l _) have "c1  n -et' (_Exit_)"
    by(fastforce elim:WCFG_elims dest:WCFG_targetlabel_less_num_nodes label_incr_ge)
  from IH[OF this] show ?case .
next
  case (WCFG_SeqSecond c2 n et n' c1)
  note IH = c2  n -et' n'  et = et'
  from c2  n -et n' n  (_Entry_) obtain l where "n = (_ l _)"
    by (cases n) auto
  with c2  n -et n' have "l < #:c2"
    by(fastforce intro:WCFG_sourcelabel_less_num_nodes)
  with c1;;c2  n  #:c1 -et' n'  #:c1 n = (_ l _) have "c2  n -et' n'"
    by -(erule WCFG_elims,(fastforce dest:WCFG_sourcelabel_less_num_nodes label_incr_ge
                                    dest!:label_incr_inj)+)
  from IH[OF this] show ?case .
next
  case WCFG_CondTrue thus ?case by(fastforce elim:WCFG_elims)
next
  case WCFG_CondFalse thus ?case by(fastforce elim:WCFG_elims)
next
  case (WCFG_CondThen c1 n et n' b c2)
  note IH = c1  n -et' n'  et = et'
  from c1  n -et n' n  (_Entry_) obtain l where "n = (_ l _)"
    by (cases n) auto
  with c1  n -et n' have "l < #:c1"
    by(fastforce intro:WCFG_sourcelabel_less_num_nodes)
  with if (b) c1 else c2  n  1 -et' n'  1 n = (_ l _)
  have "c1  n -et' n'"
    by -(erule WCFG_elims,(fastforce dest:label_incr_ge label_incr_inj)+)
  from IH[OF this] show ?case .
next
  case (WCFG_CondElse c2 n et n' b c1)
  note IH = c2  n -et' n'  et = et'
  from c2  n -et n' n  (_Entry_) obtain l where "n = (_ l _)"
    by (cases n) auto
  with c2  n -et n' have "l < #:c2"
    by(fastforce intro:WCFG_sourcelabel_less_num_nodes)
  with if (b) c1 else c2  n  (#:c1 + 1) -et' n'  (#:c1 + 1) n = (_ l _)
  have "c2  n -et' n'"
    by -(erule WCFG_elims,(fastforce dest:WCFG_sourcelabel_less_num_nodes 
                             label_incr_inj label_incr_ge label_incr_simp_rev)+)
  from IH[OF this] show ?case .
next
  case WCFG_WhileTrue thus ?case by(fastforce elim:WCFG_elims)
next
  case WCFG_WhileFalse thus ?case by(fastforce elim:WCFG_elims)
next
  case WCFG_WhileFalseSkip thus ?case by(fastforce elim:WCFG_elims)
next
  case (WCFG_WhileBody c' n et n' b)
  note IH = c'  n -et' n'  et = et'
  from c'  n -et n' n  (_Entry_) obtain l where "n = (_ l _)"
    by (cases n) auto
  moreover
  with c'  n -et n' have "l < #:c'"
    by(fastforce intro:WCFG_sourcelabel_less_num_nodes)
  moreover
  from c'  n -et n' n'  (_Exit_) obtain l' where "n' = (_ l' _)"
    by (cases n') auto
  moreover
  with c'  n -et n' have "l' < #:c'"
    by(fastforce intro:WCFG_targetlabel_less_num_nodes)
  ultimately have "c'  n -et' n'" using while (b) c'  n  2 -et' n'  2
    by(fastforce elim:WCFG_elims dest:label_incr_start_Node_smaller)
  from IH[OF this] show ?case .
next
  case (WCFG_WhileBodyExit c' n et b)
  note IH = c'  n -et' (_Exit_)  et = et'
  from c'  n -et (_Exit_) n  (_Entry_) obtain l where "n = (_ l _)"
    by (cases n) auto
  with c'  n -et (_Exit_) have "l < #:c'"
    by(fastforce intro:WCFG_sourcelabel_less_num_nodes)
  with while (b) c'  n  2 -et' (_0_) n = (_ l _)
  have "c'  n -et' (_Exit_)"
    by -(erule WCFG_elims,auto dest:label_incr_start_Node_smaller)
  from IH[OF this] show ?case .
qed

(*<*)declare One_nat_def [simp] add_2_eq_Suc' [simp](*>*)

lemma less_num_nodes_edge_Exit:
  obtains l et where "l < #:prog" and "prog  (_ l _) -et (_Exit_)"
proof -
  have "l et. l < #:prog  prog  (_ l _) -et (_Exit_)"
  proof(induct prog)
    case Skip
    have "0 < #:Skip" by simp
    moreover have "Skip  (_0_) -id (_Exit_)" by(rule WCFG_Skip)
    ultimately show ?case by blast
  next
    case (LAss V e)
    have "1 < #:(V:=e)" by simp
    moreover have "V:=e  (_1_) -id (_Exit_)" by(rule WCFG_LAssSkip)
    ultimately show ?case by blast
  next
    case (Seq prog1 prog2)
    from l et. l < #:prog2  prog2  (_ l _) -et (_Exit_)
    obtain l et where "l < #:prog2" and "prog2  (_ l _) -et (_Exit_)"
      by blast
    from prog2  (_ l _) -et (_Exit_) 
    have "prog1;;prog2  (_ l _)  #:prog1 -et (_Exit_)  #:prog1"
      by(fastforce intro:WCFG_SeqSecond)
    with l < #:prog2 show ?case by(rule_tac x="l + #:prog1" in exI,auto)
  next
    case (Cond b prog1 prog2)
    from l et. l < #:prog1  prog1  (_ l _) -et (_Exit_)
    obtain l et where "l < #:prog1" and "prog1  (_ l _) -et (_Exit_)"
      by blast
    from prog1  (_ l _) -et (_Exit_)
    have "if (b) prog1 else prog2  (_ l _)  1 -et (_Exit_)  1"
      by(fastforce intro:WCFG_CondThen)
    with l < #:prog1 show ?case by(rule_tac x="l + 1" in exI,auto)
  next
    case (While b prog')
    have "1 < #:(while (b) prog')" by simp
    moreover have "while (b) prog'  (_1_) -id (_Exit_)"
      by(rule WCFG_WhileFalseSkip)
    ultimately show ?case by blast
  qed
  with that show ?thesis by blast
qed


lemma less_num_nodes_edge:
  "l < #:prog  n et. prog  n -et (_ l _)  prog  (_ l _) -et n"
proof(induct prog arbitrary:l)
  case Skip
  from l < #:Skip have "l = 0" by simp
  hence "Skip  (_ l _) -id (_Exit_)" by(fastforce intro:WCFG_Skip)
  thus ?case by blast
next
  case (LAss V e)
  from l < #:V:=e have "l = 0  l = 1" by auto
  thus ?case
  proof
    assume "l = 0"
    hence "V:=e  (_Entry_) -(λs. True) (_ l _)" by(fastforce intro:WCFG_Entry)
    thus ?thesis by blast
  next
    assume "l = 1"
    hence "V:=e  (_ l _) -id (_Exit_)" by(fastforce intro:WCFG_LAssSkip)
    thus ?thesis by blast
  qed
next
  case (Seq prog1 prog2)
  note IH1 = l. l < #:prog1  
              n et. prog1  n -et (_ l _)  prog1  (_ l _) -et n
  note IH2 = l. l < #:prog2  
              n et. prog2  n -et (_ l _)  prog2  (_ l _) -et n
  show ?case
  proof(cases "l < #:prog1")
    case True
    from IH1[OF this] obtain n et 
      where "prog1  n -et (_ l _)  prog1  (_ l _) -et n" by blast
    thus ?thesis
    proof
      assume "prog1  n -et (_ l _)"
      hence "prog1;; prog2  n -et (_ l _)" by(fastforce intro:WCFG_SeqFirst)
      thus ?thesis by blast
    next
      assume edge:"prog1  (_ l _) -et n"
      show ?thesis
      proof(cases "n = (_Exit_)")
        case True
        with edge have "prog1;; prog2  (_ l _) -et (_0_)  #:prog1"
          by(fastforce intro:WCFG_SeqConnect)
        thus ?thesis by blast
      next
        case False
        with edge have "prog1;; prog2  (_ l _) -et n"
          by(fastforce intro:WCFG_SeqFirst)
        thus ?thesis by blast
      qed
    qed
  next
    case False
    hence "#:prog1  l" by simp
    then obtain l' where "l = l' + #:prog1" and "l' = l - #:prog1" by simp
    from l = l' + #:prog1 l < #:prog1;; prog2 have "l' < #:prog2" by simp
    from IH2[OF this] obtain n et
      where "prog2  n -et (_ l' _)  prog2  (_ l' _) -et n" by blast
    thus ?thesis
    proof
      assume "prog2  n -et (_ l' _)"
      show ?thesis
      proof(cases "n = (_Entry_)")
        case True
        with prog2  n -et (_ l' _) have "l' = 0" by(auto dest:WCFG_EntryD)
        obtain l'' et'' where "l'' < #:prog1" 
          and "prog1  (_ l'' _) -et'' (_Exit_)"
          by(erule less_num_nodes_edge_Exit)
        hence "prog1;;prog2  (_ l'' _) -et'' (_0_)  #:prog1"
          by(fastforce intro:WCFG_SeqConnect)
        with l' = 0 l = l' + #:prog1 show ?thesis by simp blast
      next
        case False
        with prog2  n -et (_ l' _)
        have "prog1;;prog2  n  #:prog1 -et (_ l' _)  #:prog1"
          by(fastforce intro:WCFG_SeqSecond)
        with l = l' + #:prog1 show ?thesis  by simp blast
      qed
    next
      assume "prog2  (_ l' _) -et n"
      hence "prog1;;prog2  (_ l' _)  #:prog1 -et n  #:prog1"
        by(fastforce intro:WCFG_SeqSecond)
      with l = l' + #:prog1 show ?thesis  by simp blast
    qed
  qed
next
  case (Cond b prog1 prog2)
  note IH1 = l. l < #:prog1  
              n et. prog1  n -et (_ l _)  prog1  (_ l _) -et n
  note IH2 = l. l < #:prog2  
              n et. prog2  n -et (_ l _)  prog2  (_ l _) -et n
  show ?case
  proof(cases "l = 0")
    case True
    have "if (b) prog1 else prog2  (_Entry_) -(λs. True) (_0_)"
      by(rule WCFG_Entry)
    with True show ?thesis by simp blast
  next
    case False
    hence "0 < l" by simp
    then obtain l' where "l = l' + 1" and "l' = l - 1" by simp
    thus ?thesis
    proof(cases "l' < #:prog1")
      case True
      from IH1[OF this] obtain n et 
        where "prog1  n -et (_ l' _)  prog1  (_ l' _) -et n" by blast
      thus ?thesis
      proof
        assume edge:"prog1  n -et (_ l' _)"
        show ?thesis
        proof(cases "n = (_Entry_)")
          case True
          with edge have "l' = 0" by(auto dest:WCFG_EntryD)
          have "if (b) prog1 else prog2  (_0_) -(λs. interpret b s = Some true) 
                                          (_0_)  1"
            by(rule WCFG_CondTrue)
          with l' = 0 l = l' + 1 show ?thesis by simp blast
        next
          case False
          with edge have "if (b) prog1 else prog2  n  1 -et (_ l' _)  1"
            by(fastforce intro:WCFG_CondThen)
          with l = l' + 1 show ?thesis by simp blast
        qed
      next
        assume "prog1  (_ l' _) -et n"
        hence "if (b) prog1 else prog2  (_ l' _)  1 -et n  1"
          by(fastforce intro:WCFG_CondThen)
        with l = l' + 1 show ?thesis by simp blast
      qed
    next
      case False
      hence "#:prog1  l'" by simp
      then obtain l'' where "l' = l'' + #:prog1" and "l'' = l' - #:prog1"
        by simp
      from l' = l'' + #:prog1 l = l' + 1 l < #:(if (b) prog1 else prog2)
      have "l'' < #:prog2" by simp
      from IH2[OF this] obtain n et 
        where "prog2  n -et (_ l'' _)  prog2  (_ l'' _) -et n" by blast
      thus ?thesis
      proof
        assume "prog2  n -et (_ l'' _)"
        show ?thesis
        proof(cases "n = (_Entry_)")
          case True
          with prog2  n -et (_ l'' _) have "l'' = 0" by(auto dest:WCFG_EntryD)
          have "if (b) prog1 else prog2  (_0_) -(λs. interpret b s = Some false) 
                                          (_0_)  (#:prog1 + 1)"
            by(rule WCFG_CondFalse)
          with l'' = 0 l' = l'' + #:prog1 l = l' + 1 show ?thesis by simp blast
        next
          case False
          with prog2  n -et (_ l'' _)
          have "if (b) prog1 else prog2  n  (#:prog1 + 1) -et 
                                          (_ l'' _)  (#:prog1 + 1)"
            by(fastforce intro:WCFG_CondElse)
          with l = l' + 1 l' = l'' + #:prog1 show ?thesis by simp blast
        qed
      next
        assume "prog2  (_ l'' _) -et n"
        hence "if (b) prog1 else prog2  (_ l'' _)  (#:prog1 + 1) -et 
                                         n  (#:prog1 + 1)"
          by(fastforce intro:WCFG_CondElse)
        with l = l' + 1 l' = l'' + #:prog1 show ?thesis by simp blast
      qed
    qed
  qed
next
  case (While b prog')
  note IH = l. l < #:prog' 
              n et. prog'  n -et (_ l _)  prog'  (_ l _) -et n
  show ?case
  proof(cases "l < 1")
    case True
    have "while (b) prog'  (_Entry_) -(λs. True) (_0_)" by(rule WCFG_Entry)
    with 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 "l = 1" by simp
      have "while (b) prog'  (_0_) -(λs. interpret b s = Some false) (_1_)"
        by(rule WCFG_WhileFalse)
      with l = 1 show ?thesis by simp blast
    next
      case False
      with 1  l have "2  l" by simp
      then obtain l' where "l = l' + 2" and "l' = l - 2" 
        by(simp del:add_2_eq_Suc')
      from l = l' + 2 l < #:while (b) prog' have "l' < #:prog'" by simp
      from IH[OF this] obtain n et 
        where "prog'  n -et (_ l' _)  prog'  (_ l' _) -et n" by blast
      thus ?thesis
      proof
        assume "prog'  n -et (_ l' _)"
        show ?thesis
        proof(cases "n = (_Entry_)")
          case True
          with prog'  n -et (_ l' _) have "l' = 0" by(auto dest:WCFG_EntryD)
          have "while (b) prog'  (_0_) -(λs. interpret b s = Some true) 
                                  (_0_)  2"
            by(rule WCFG_WhileTrue)
          with l' = 0 l = l' + 2 show ?thesis by simp blast
        next
          case False
          with prog'  n -et (_ l' _)
          have "while (b) prog'  n  2 -et (_ l' _)  2"
            by(fastforce intro:WCFG_WhileBody)
          with l = l' + 2 show ?thesis by simp blast
        qed
      next
        assume "prog'  (_ l' _) -et n"
        show ?thesis
        proof(cases "n = (_Exit_)")
          case True
          with prog'  (_ l' _) -et n
          have "while (b) prog'  (_ l' _)  2 -et (_0_)"
            by(fastforce intro:WCFG_WhileBodyExit)
          with l = l' + 2 show ?thesis by simp blast
        next
          case False
          with prog'  (_ l' _) -et n
          have "while (b) prog'  (_ l' _)  2 -et n  2"
            by(fastforce intro:WCFG_WhileBody)
          with l = l' + 2 show ?thesis by simp blast
        qed
      qed
    qed
  qed
qed


(*<*)declare One_nat_def [simp del](*>*)

lemma WCFG_deterministic:
  "prog  n1 -et1 n1'; prog  n2 -et2 n2'; n1 = n2; n1'  n2'
   Q Q'. et1 = (Q)  et2 = (Q')  (s. (Q s  ¬ Q' s)  (Q' s  ¬ Q s))"
proof(induct arbitrary:n2 n2' rule:WCFG_induct)
  case (WCFG_Entry_Exit prog)
  from prog  n2 -et2 n2' (_Entry_) = n2 (_Exit_)  n2'
  have "et2 = (λs. True)" by(fastforce dest:WCFG_EntryD)
  thus ?case by simp
next
  case (WCFG_Entry prog)
  from prog  n2 -et2 n2' (_Entry_) = n2 (_0_)  n2'
  have "et2 = (λs. False)" by(fastforce dest:WCFG_EntryD)
  thus ?case by simp
next
  case WCFG_Skip
  from Skip  n2 -et2 n2' (_0_) = n2 (_Exit_)  n2'
  have False by(fastforce elim:WCFG.While_CFG.cases)
  thus ?case by simp
next
  case (WCFG_LAss V e)
  from V:=e  n2 -et2 n2' (_0_) = n2 (_1_)  n2'
  have False by -(erule WCFG.While_CFG.cases,auto)
  thus ?case by simp
next
  case (WCFG_LAssSkip V e)
  from V:=e  n2 -et2 n2' (_1_) = n2 (_Exit_)  n2'
  have False by -(erule WCFG.While_CFG.cases,auto)
  thus ?case by simp
next
  case (WCFG_SeqFirst c1 n et n' c2)
  note IH = n2 n2'. c1  n2 -et2 n2'; n = n2; n'  n2'
   Q Q'. et = (Q)  et2 = (Q')  (s. (Q s  ¬ Q' s)  (Q' s  ¬ Q s))
  from c1;;c2  n2 -et2 n2' c1  n -et n' n = n2 n'  n2'
  have "c1  n2 -et2 n2'  (c1  n2 -et2 (_Exit_)  n2' = (_0_)  #:c1)"
    apply hypsubst_thin apply(erule WCFG.While_CFG.cases)
    apply(auto intro:WCFG.While_CFG.intros)
    by(case_tac n,auto dest:WCFG_sourcelabel_less_num_nodes)+
  thus ?case
  proof
    assume "c1  n2 -et2 n2'"
    from IH[OF this n = n2 n'  n2'] show ?case .
  next
    assume "c1  n2 -et2 (_Exit_)  n2' = (_0_)  #:c1"
    hence edge:"c1  n2 -et2 (_Exit_)" and n2':"n2' = (_0_)  #:c1" by simp_all
    from IH[OF edge n = n2 n'  (_Exit_)] show ?case .
  qed
next
  case (WCFG_SeqConnect c1 n et c2)
  note IH = n2 n2'. c1  n2 -et2 n2'; n = n2; (_Exit_)  n2'
   Q Q'. et = (Q)  et2 = (Q')  (s. (Q s  ¬ Q' s)  (Q' s  ¬ Q s))
  from c1;;c2  n2 -et2 n2' c1  n -et (_Exit_) n = n2 n  (_Entry_)
    (_0_)  #:c1  n2' have "c1  n2 -et2 n2'  (_Exit_)  n2'"
    apply hypsubst_thin apply(erule WCFG.While_CFG.cases)
    apply(auto intro:WCFG.While_CFG.intros)
    by(case_tac n,auto dest:WCFG_sourcelabel_less_num_nodes)+
  from IH[OF this[THEN conjunct1] n = n2 this[THEN conjunct2]]
  show ?case .
next
  case (WCFG_SeqSecond c2 n et n' c1)
  note IH = n2 n2'. c2  n2 -et2 n2'; n = n2; n'  n2'
   Q Q'. et = (Q)  et2 = (Q')  (s. (Q s  ¬ Q' s)  (Q' s  ¬ Q s))
  from c1;;c2  n2 -et2 n2' c2  n -et n' n  #:c1 = n2
    n'  #:c1  n2' n  (_Entry_)
  obtain nx where "c2  n -et2 nx  nx  #:c1 = n2'"
    apply - apply(erule WCFG.While_CFG.cases)
    apply(auto intro:WCFG.While_CFG.intros)
      apply(cases n,auto dest:WCFG_sourcelabel_less_num_nodes)
     apply(cases n,auto dest:WCFG_sourcelabel_less_num_nodes)
    by(fastforce dest:label_incr_inj)
  with n'  #:c1  n2' have edge:"c2  n -et2 nx" and neq:"n'  nx"
    by auto
  from IH[OF edge _ neq] show ?case by simp
next
  case (WCFG_CondTrue b c1 c2)
  from if (b) c1 else c2  n2 -et2 n2' (_0_) = n2 (_0_)  1  n2'
  show ?case by -(erule WCFG.While_CFG.cases,auto)
next
  case (WCFG_CondFalse b c1 c2)
  from if (b) c1 else c2  n2 -et2 n2' (_0_) = n2 (_0_)  #:c1 + 1  n2'
  show ?case by -(erule WCFG.While_CFG.cases,auto)
next
  case (WCFG_CondThen c1 n et n' b c2)
  note IH = n2 n2'. c1  n2 -et2 n2'; n = n2; n'  n2'
     Q Q'. et = (Q)  et2 = (Q')  (s. (Q s  ¬ Q' s)  (Q' s  ¬ Q s))
  from if (b) c1 else c2  n2 -et2 n2' c1  n -et n' n  (_Entry_) 
    n  1 = n2 n'  1  n2'
  obtain nx where "c1  n -et2 nx  n'  nx"
    apply - apply(erule WCFG.While_CFG.cases)
    apply(auto intro:WCFG.While_CFG.intros)
     apply(drule label_incr_inj) apply auto
    apply(drule label_incr_simp_rev[OF sym])
    by(case_tac na,auto dest:WCFG_sourcelabel_less_num_nodes)
  from IH[OF this[THEN conjunct1] _ this[THEN conjunct2]] show ?case by simp
next
  case (WCFG_CondElse c2 n et n' b c1)
  note IH = n2 n2'. c2  n2 -et2 n2'; n = n2; n'  n2'
     Q Q'. et = (Q)  et2 = (Q')  (s. (Q s  ¬ Q' s)  (Q' s  ¬ Q s))
  from if (b) c1 else c2  n2 -et2 n2' c2  n -et n' n  (_Entry_) 
    n  #:c1 + 1 = n2 n'  #:c1 + 1  n2'
  obtain nx where "c2  n -et2 nx  n'  nx"
    apply - apply(erule WCFG.While_CFG.cases)
    apply(auto intro:WCFG.While_CFG.intros)
     apply(drule label_incr_simp_rev)
     apply(case_tac na,auto,cases n,auto dest:WCFG_sourcelabel_less_num_nodes)
    by(fastforce dest:label_incr_inj)
  from IH[OF this[THEN conjunct1] _ this[THEN conjunct2]] show ?case by simp
next
  case (WCFG_WhileTrue b c')
  from while (b) c'  n2 -et2 n2' (_0_) = n2 (_0_)  2  n2'
  show ?case by -(erule WCFG.While_CFG.cases,auto)
next
  case (WCFG_WhileFalse b c')
  from while (b) c'  n2 -et2 n2' (_0_) = n2 (_1_)  n2'
  show ?case by -(erule WCFG.While_CFG.cases,auto)
next
  case (WCFG_WhileFalseSkip b c')
  from while (b) c'  n2 -et2 n2' (_1_) = n2 (_Exit_)  n2'
  show ?case by -(erule WCFG.While_CFG.cases,auto dest:label_incr_ge)
next
  case (WCFG_WhileBody c' n et n' b)
  note IH = n2 n2'. c'  n2 -et2 n2'; n = n2; n'  n2'
     Q Q'. et = (Q)  et2 = (Q')  (s. (Q s  ¬ Q' s)  (Q' s  ¬ Q s))
  from while (b) c'  n2 -et2 n2' c'  n -et n' n  (_Entry_)
    n'  (_Exit_) n  2 = n2 n'  2  n2'
  obtain nx where "c'  n -et2 nx  n'  nx"
    apply - apply(erule WCFG.While_CFG.cases)
    apply(auto intro:WCFG.While_CFG.intros)
      apply(fastforce dest:label_incr_ge[OF sym])
     apply(fastforce dest:label_incr_inj)
    by(fastforce dest:label_incr_inj)
  from IH[OF this[THEN conjunct1] _ this[THEN conjunct2]] show ?case by simp
next
  case (WCFG_WhileBodyExit c' n et b)
  note IH = n2 n2'. c'  n2 -et2 n2'; n = n2; (_Exit_)  n2'
     Q Q'. et = (Q)  et2 = (Q')  (s. (Q s  ¬ Q' s)  (Q' s  ¬ Q s))
  from while (b) c'  n2 -et2 n2' c'  n -et (_Exit_) n  (_Entry_)
    n  2 = n2 (_0_)  n2'
  obtain nx where "c'  n -et2 nx  (_Exit_)  nx"
    apply - apply(erule WCFG.While_CFG.cases)
    apply(auto intro:WCFG.While_CFG.intros)
     apply(fastforce dest:label_incr_ge[OF sym])
    by(fastforce dest:label_incr_inj)
  from IH[OF this[THEN conjunct1] _ this[THEN conjunct2]] show ?case by simp
qed

(*<*)declare One_nat_def [simp](*>*)

end