Theory 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