Theory WCFG

header {* \isaheader{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"
  ("_ \<turnstile> _ -_-> _")
where

WCFG_Entry_Exit:
  "prog \<turnstile> (_Entry_) -(λs. False)⇣\<surd>-> (_Exit_)"

| WCFG_Entry:
  "prog \<turnstile> (_Entry_) -(λs. True)⇣\<surd>-> (_0_)"

| WCFG_Skip: 
  "Skip \<turnstile> (_0_) -\<Up>id-> (_Exit_)"

| WCFG_LAss: 
  "V:=e \<turnstile> (_0_) -\<Up>(λs. s(V:=(interpret e s)))-> (_1_)"

| WCFG_LAssSkip:
  "V:=e \<turnstile> (_1_) -\<Up>id-> (_Exit_)"

| WCFG_SeqFirst:
  "[|c⇣1 \<turnstile> n -et-> n'; n' ≠ (_Exit_)|] ==> c⇣1;;c⇣2 \<turnstile> n -et-> n'"

| WCFG_SeqConnect: 
  "[|c⇣1 \<turnstile> n -et-> (_Exit_); n ≠ (_Entry_)|] ==> c⇣1;;c⇣2 \<turnstile> n -et-> (_0_) ⊕ #:c⇣1"

| WCFG_SeqSecond: 
  "[|c⇣2 \<turnstile> n -et-> n'; n ≠ (_Entry_)|] ==> c⇣1;;c⇣2 \<turnstile> n ⊕ #:c⇣1 -et-> n' ⊕ #:c⇣1"

| WCFG_CondTrue:
    "if (b) c⇣1 else c⇣2 \<turnstile> (_0_) -(λs. interpret b s = Some true)⇣\<surd>-> (_0_) ⊕ 1"

| WCFG_CondFalse:
    "if (b) c⇣1 else c⇣2 \<turnstile> (_0_) -(λs. interpret b s = Some false)⇣\<surd>-> (_0_) ⊕ (#:c⇣1 + 1)"

| WCFG_CondThen:
  "[|c⇣1 \<turnstile> n -et-> n'; n ≠ (_Entry_)|] ==> if (b) c⇣1 else c⇣2 \<turnstile> n ⊕ 1 -et-> n' ⊕ 1"

| WCFG_CondElse:
  "[|c⇣2 \<turnstile> n -et-> n'; n ≠ (_Entry_)|] 
  ==> if (b) c⇣1 else c⇣2 \<turnstile> n ⊕ (#:c⇣1 + 1) -et-> n' ⊕ (#:c⇣1 + 1)"

| WCFG_WhileTrue:
    "while (b) c' \<turnstile> (_0_) -(λs. interpret b s = Some true)⇣\<surd>-> (_0_) ⊕ 2"

| WCFG_WhileFalse:
    "while (b) c' \<turnstile> (_0_) -(λs. interpret b s = Some false)⇣\<surd>-> (_1_)"

| WCFG_WhileFalseSkip:
  "while (b) c' \<turnstile> (_1_) -\<Up>id-> (_Exit_)"

| WCFG_WhileBody:
  "[|c' \<turnstile> n -et-> n'; n ≠ (_Entry_); n' ≠ (_Exit_)|] 
  ==> while (b) c' \<turnstile> n ⊕ 2 -et-> n' ⊕ 2"

| WCFG_WhileBodyExit:
  "[|c' \<turnstile> n -et-> (_Exit_); n ≠ (_Entry_)|] ==> while (b) c' \<turnstile> 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 \<turnstile> (_Exit_) -et-> n' ==> False"
by(induct prog n≡"(_Exit_)" et n' rule:WCFG_induct,auto)


lemma WCFG_Entry_no_targetnode [dest]:
  "prog \<turnstile> n -et-> (_Entry_) ==> False"
by(induct prog n et n'≡"(_Entry_)" rule:WCFG_induct,auto)


lemma WCFG_sourcelabel_less_num_nodes:
  "prog \<turnstile> (_ l _) -et-> n' ==> l < #:prog"
proof(induct prog "(_ l _)" et n' arbitrary:l rule:WCFG_induct)
  case (WCFG_SeqFirst c⇣1 et n' c⇣2)
  from `l < #:c⇣1` show ?case by simp
next
  case (WCFG_SeqConnect c⇣1 et c⇣2)
  from `l < #:c⇣1` show ?case by simp
next
  case (WCFG_SeqSecond c⇣2 n et n' c⇣1)
  note IH = `!!l. n = (_ l _) ==> l < #:c⇣2`
  from `n ⊕ #:c⇣1 = (_ l _)` obtain l' where "n = (_ l' _)" by(cases n) auto
  from IH[OF this] have "l' < #:c⇣2" .
  with `n ⊕ #:c⇣1 = (_ l _)` `n = (_ l' _)` show ?case by simp
next
  case (WCFG_CondThen c⇣1 n et n' b c⇣2)
  note IH = `!!l. n = (_ l _) ==> l < #:c⇣1`
  from `n ⊕ 1 = (_ l _)` obtain l' where "n = (_ l' _)" by(cases n) auto
  from IH[OF this] have "l' < #:c⇣1" .
  with `n ⊕ 1 = (_ l _)` `n = (_ l' _)` show ?case by simp
next
  case (WCFG_CondElse c⇣2 n et n' b c⇣1)
  note IH = `!!l. n = (_ l _) ==> l < #:c⇣2`
  from `n ⊕ (#:c⇣1 + 1) = (_ l _)` obtain l' where "n = (_ l' _)" by(cases n) auto
  from IH[OF this] have "l' < #:c⇣2" .
  with `n ⊕ (#:c⇣1 + 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 \<turnstile> n -et-> (_ l _) ==> l < #:prog"
proof(induct prog n et "(_ l _)" arbitrary:l rule:WCFG_induct)
  case (WCFG_SeqFirst c⇣1 n et c⇣2)
  from `l < #:c⇣1` show ?case by simp
next
  case (WCFG_SeqSecond c⇣2 n et n' c⇣1)
  note IH = `!!l. n' = (_ l _) ==> l < #:c⇣2`
  from `n' ⊕ #:c⇣1 = (_ l _)` obtain l' where "n' = (_ l' _)" by(cases n') auto
  from IH[OF this] have "l' < #:c⇣2" .
  with `n' ⊕ #:c⇣1 = (_ l _)` `n' = (_ l' _)` show ?case by simp
next
  case (WCFG_CondThen c⇣1 n et n' b c⇣2)
  note IH = `!!l. n' = (_ l _) ==> l < #:c⇣1`
  from `n' ⊕ 1 = (_ l _)` obtain l' where "n' = (_ l' _)" by(cases n') auto
  from IH[OF this] have "l' < #:c⇣1" .
  with `n' ⊕ 1 = (_ l _)` `n' = (_ l' _)` show ?case by simp
next
  case (WCFG_CondElse c⇣2 n et n' b c⇣1)
  note IH = `!!l. n' = (_ l _) ==> l < #:c⇣2`
  from `n' ⊕ (#:c⇣1 + 1) = (_ l _)` obtain l' where "n' = (_ l' _)" by(cases n') auto
  from IH[OF this] have "l' < #:c⇣2" .
  with `n' ⊕ (#:c⇣1 + 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 \<turnstile> (_Entry_) -et-> n'
  ==> (n' = (_Exit_) ∧ et = (λs. False)⇣\<surd>) ∨ (n' = (_0_) ∧ et = (λs. True)⇣\<surd>)"
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 \<turnstile> n -et-> n'; prog \<turnstile> 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 c⇣1 n et n' c⇣2)
  note IH = `c⇣1 \<turnstile> n -et'-> n' ==> et = et'`
  from `c⇣1 \<turnstile> n -et-> n'` `n' ≠ (_Exit_)` obtain l where "n' = (_ l _)"
    by (cases n') auto
  with `c⇣1 \<turnstile> n -et-> n'` have "l < #:c⇣1" 
    by(fastforce intro:WCFG_targetlabel_less_num_nodes)
  with `c⇣1;;c⇣2 \<turnstile> n -et'-> n'` `n' = (_ l _)` have "c⇣1 \<turnstile> 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 c⇣1 n et c⇣2)
  note IH = `c⇣1 \<turnstile> n -et'-> (_Exit_) ==> et = et'`
  from `c⇣1 \<turnstile> n -et-> (_Exit_)` `n ≠ (_Entry_)` obtain l where "n = (_ l _)"
    by (cases n) auto
  with `c⇣1 \<turnstile> n -et-> (_Exit_)` have "l < #:c⇣1"
    by(fastforce intro:WCFG_sourcelabel_less_num_nodes)
  with `c⇣1;;c⇣2 \<turnstile> n -et'-> (_ 0 _) ⊕ #:c⇣1` `n = (_ l _)` have "c⇣1 \<turnstile> 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 c⇣2 n et n' c⇣1)
  note IH = `c⇣2 \<turnstile> n -et'-> n' ==> et = et'`
  from `c⇣2 \<turnstile> n -et-> n'` `n ≠ (_Entry_)` obtain l where "n = (_ l _)"
    by (cases n) auto
  with `c⇣2 \<turnstile> n -et-> n'` have "l < #:c⇣2"
    by(fastforce intro:WCFG_sourcelabel_less_num_nodes)
  with `c⇣1;;c⇣2 \<turnstile> n ⊕ #:c⇣1 -et'-> n' ⊕ #:c⇣1` `n = (_ l _)` have "c⇣2 \<turnstile> 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 c⇣1 n et n' b c⇣2)
  note IH = `c⇣1 \<turnstile> n -et'-> n' ==> et = et'`
  from `c⇣1 \<turnstile> n -et-> n'` `n ≠ (_Entry_)` obtain l where "n = (_ l _)"
    by (cases n) auto
  with `c⇣1 \<turnstile> n -et-> n'` have "l < #:c⇣1"
    by(fastforce intro:WCFG_sourcelabel_less_num_nodes)
  with `if (b) c⇣1 else c⇣2 \<turnstile> n ⊕ 1 -et'-> n' ⊕ 1` `n = (_ l _)`
  have "c⇣1 \<turnstile> 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 c⇣2 n et n' b c⇣1)
  note IH = `c⇣2 \<turnstile> n -et'-> n' ==> et = et'`
  from `c⇣2 \<turnstile> n -et-> n'` `n ≠ (_Entry_)` obtain l where "n = (_ l _)"
    by (cases n) auto
  with `c⇣2 \<turnstile> n -et-> n'` have "l < #:c⇣2"
    by(fastforce intro:WCFG_sourcelabel_less_num_nodes)
  with `if (b) c⇣1 else c⇣2 \<turnstile> n ⊕ (#:c⇣1 + 1) -et'-> n' ⊕ (#:c⇣1 + 1)` `n = (_ l _)`
  have "c⇣2 \<turnstile> 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' \<turnstile> n -et'-> n' ==> et = et'`
  from `c' \<turnstile> n -et-> n'` `n ≠ (_Entry_)` obtain l where "n = (_ l _)"
    by (cases n) auto
  moreover
  with `c' \<turnstile> n -et-> n'` have "l < #:c'"
    by(fastforce intro:WCFG_sourcelabel_less_num_nodes)
  moreover
  from `c' \<turnstile> n -et-> n'` `n' ≠ (_Exit_)` obtain l' where "n' = (_ l' _)"
    by (cases n') auto
  moreover
  with `c' \<turnstile> n -et-> n'` have "l' < #:c'"
    by(fastforce intro:WCFG_targetlabel_less_num_nodes)
  ultimately have "c' \<turnstile> n -et'-> n'" using `while (b) c' \<turnstile> 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' \<turnstile> n -et'-> (_Exit_) ==> et = et'`
  from `c' \<turnstile> n -et-> (_Exit_)` `n ≠ (_Entry_)` obtain l where "n = (_ l _)"
    by (cases n) auto
  with `c' \<turnstile> n -et-> (_Exit_)` have "l < #:c'"
    by(fastforce intro:WCFG_sourcelabel_less_num_nodes)
  with `while (b) c' \<turnstile> n ⊕ 2 -et'-> (_0_)` `n = (_ l _)`
  have "c' \<turnstile> 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 \<turnstile> (_ l _) -et-> (_Exit_)"
proof -
  have "∃l et. l < #:prog ∧ prog \<turnstile> (_ l _) -et-> (_Exit_)"
  proof(induct prog)
    case Skip
    have "0 < #:Skip" by simp
    moreover have "Skip \<turnstile> (_0_) -\<Up>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 \<turnstile> (_1_) -\<Up>id-> (_Exit_)" by(rule WCFG_LAssSkip)
    ultimately show ?case by blast
  next
    case (Seq prog1 prog2)
    from `∃l et. l < #:prog2 ∧ prog2 \<turnstile> (_ l _) -et-> (_Exit_)`
    obtain l et where "l < #:prog2" and "prog2 \<turnstile> (_ l _) -et-> (_Exit_)"
      by blast
    from `prog2 \<turnstile> (_ l _) -et-> (_Exit_)` 
    have "prog1;;prog2 \<turnstile> (_ 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 \<turnstile> (_ l _) -et-> (_Exit_)`
    obtain l et where "l < #:prog1" and "prog1 \<turnstile> (_ l _) -et-> (_Exit_)"
      by blast
    from `prog1 \<turnstile> (_ l _) -et-> (_Exit_)`
    have "if (b) prog1 else prog2 \<turnstile> (_ 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' \<turnstile> (_1_) -\<Up>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 \<turnstile> n -et-> (_ l _) ∨ prog \<turnstile> (_ l _) -et-> n"
proof(induct prog arbitrary:l)
  case Skip
  from `l < #:Skip` have "l = 0" by simp
  hence "Skip \<turnstile> (_ l _) -\<Up>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 \<turnstile> (_Entry_) -(λs. True)⇣\<surd>-> (_ l _)" by(fastforce intro:WCFG_Entry)
    thus ?thesis by blast
  next
    assume "l = 1"
    hence "V:=e \<turnstile> (_ l _) -\<Up>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 \<turnstile> n -et-> (_ l _) ∨ prog1 \<turnstile> (_ l _) -et-> n`
  note IH2 = `!!l. l < #:prog2 ==> 
              ∃n et. prog2 \<turnstile> n -et-> (_ l _) ∨ prog2 \<turnstile> (_ l _) -et-> n`
  show ?case
  proof(cases "l < #:prog1")
    case True
    from IH1[OF this] obtain n et 
      where "prog1 \<turnstile> n -et-> (_ l _) ∨ prog1 \<turnstile> (_ l _) -et-> n" by blast
    thus ?thesis
    proof
      assume "prog1 \<turnstile> n -et-> (_ l _)"
      hence "prog1;; prog2 \<turnstile> n -et-> (_ l _)" by(fastforce intro:WCFG_SeqFirst)
      thus ?thesis by blast
    next
      assume edge:"prog1 \<turnstile> (_ l _) -et-> n"
      show ?thesis
      proof(cases "n = (_Exit_)")
        case True
        with edge have "prog1;; prog2 \<turnstile> (_ l _) -et-> (_0_) ⊕ #:prog1"
          by(fastforce intro:WCFG_SeqConnect)
        thus ?thesis by blast
      next
        case False
        with edge have "prog1;; prog2 \<turnstile> (_ 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 \<turnstile> n -et-> (_ l' _) ∨ prog2 \<turnstile> (_ l' _) -et-> n" by blast
    thus ?thesis
    proof
      assume "prog2 \<turnstile> n -et-> (_ l' _)"
      show ?thesis
      proof(cases "n = (_Entry_)")
        case True
        with `prog2 \<turnstile> n -et-> (_ l' _)` have "l' = 0" by(auto dest:WCFG_EntryD)
        obtain l'' et'' where "l'' < #:prog1" 
          and "prog1 \<turnstile> (_ l'' _) -et''-> (_Exit_)"
          by(erule less_num_nodes_edge_Exit)
        hence "prog1;;prog2 \<turnstile> (_ 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 \<turnstile> n -et-> (_ l' _)`
        have "prog1;;prog2 \<turnstile> n ⊕ #:prog1 -et-> (_ l' _) ⊕ #:prog1"
          by(fastforce intro:WCFG_SeqSecond)
        with `l = l' + #:prog1` show ?thesis  by simp blast
      qed
    next
      assume "prog2 \<turnstile> (_ l' _) -et-> n"
      hence "prog1;;prog2 \<turnstile> (_ 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 \<turnstile> n -et-> (_ l _) ∨ prog1 \<turnstile> (_ l _) -et-> n`
  note IH2 = `!!l. l < #:prog2 ==> 
              ∃n et. prog2 \<turnstile> n -et-> (_ l _) ∨ prog2 \<turnstile> (_ l _) -et-> n`
  show ?case
  proof(cases "l = 0")
    case True
    have "if (b) prog1 else prog2 \<turnstile> (_Entry_) -(λs. True)⇣\<surd>-> (_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 \<turnstile> n -et-> (_ l' _) ∨ prog1 \<turnstile> (_ l' _) -et-> n" by blast
      thus ?thesis
      proof
        assume edge:"prog1 \<turnstile> 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 \<turnstile> (_0_) -(λs. interpret b s = Some true)⇣\<surd>-> 
                                          (_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 \<turnstile> n ⊕ 1 -et-> (_ l' _) ⊕ 1"
            by(fastforce intro:WCFG_CondThen)
          with `l = l' + 1` show ?thesis by simp blast
        qed
      next
        assume "prog1 \<turnstile> (_ l' _) -et-> n"
        hence "if (b) prog1 else prog2 \<turnstile> (_ 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 \<turnstile> n -et-> (_ l'' _) ∨ prog2 \<turnstile> (_ l'' _) -et-> n" by blast
      thus ?thesis
      proof
        assume "prog2 \<turnstile> n -et-> (_ l'' _)"
        show ?thesis
        proof(cases "n = (_Entry_)")
          case True
          with `prog2 \<turnstile> n -et-> (_ l'' _)` have "l'' = 0" by(auto dest:WCFG_EntryD)
          have "if (b) prog1 else prog2 \<turnstile> (_0_) -(λs. interpret b s = Some false)⇣\<surd>-> 
                                          (_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 \<turnstile> n -et-> (_ l'' _)`
          have "if (b) prog1 else prog2 \<turnstile> 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 \<turnstile> (_ l'' _) -et-> n"
        hence "if (b) prog1 else prog2 \<turnstile> (_ 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' \<turnstile> n -et-> (_ l _) ∨ prog' \<turnstile> (_ l _) -et-> n`
  show ?case
  proof(cases "l < 1")
    case True
    have "while (b) prog' \<turnstile> (_Entry_) -(λs. True)⇣\<surd>-> (_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' \<turnstile> (_0_) -(λs. interpret b s = Some false)⇣\<surd>-> (_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' \<turnstile> n -et-> (_ l' _) ∨ prog' \<turnstile> (_ l' _) -et-> n" by blast
      thus ?thesis
      proof
        assume "prog' \<turnstile> n -et-> (_ l' _)"
        show ?thesis
        proof(cases "n = (_Entry_)")
          case True
          with `prog' \<turnstile> n -et-> (_ l' _)` have "l' = 0" by(auto dest:WCFG_EntryD)
          have "while (b) prog' \<turnstile> (_0_) -(λs. interpret b s = Some true)⇣\<surd>-> 
                                  (_0_) ⊕ 2"
            by(rule WCFG_WhileTrue)
          with `l' = 0` `l = l' + 2` show ?thesis by simp blast
        next
          case False
          with `prog' \<turnstile> n -et-> (_ l' _)`
          have "while (b) prog' \<turnstile> n ⊕ 2 -et-> (_ l' _) ⊕ 2"
            by(fastforce intro:WCFG_WhileBody)
          with `l = l' + 2` show ?thesis by simp blast
        qed
      next
        assume "prog' \<turnstile> (_ l' _) -et-> n"
        show ?thesis
        proof(cases "n = (_Exit_)")
          case True
          with `prog' \<turnstile> (_ l' _) -et-> n`
          have "while (b) prog' \<turnstile> (_ l' _) ⊕ 2 -et-> (_0_)"
            by(fastforce intro:WCFG_WhileBodyExit)
          with `l = l' + 2` show ?thesis by simp blast
        next
          case False
          with `prog' \<turnstile> (_ l' _) -et-> n`
          have "while (b) prog' \<turnstile> (_ 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 \<turnstile> n⇣1 -et⇣1-> n⇣1'; prog \<turnstile> n⇣2 -et⇣2-> n⇣2'; n⇣1 = n⇣2; n⇣1' ≠ n⇣2'|]
  ==> ∃Q Q'. et⇣1 = (Q)⇣\<surd> ∧ et⇣2 = (Q')⇣\<surd> ∧ (∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s))"
proof(induct arbitrary:n⇣2 n⇣2' rule:WCFG_induct)
  case (WCFG_Entry_Exit prog)
  from `prog \<turnstile> n⇣2 -et⇣2-> n⇣2'` `(_Entry_) = n⇣2` `(_Exit_) ≠ n⇣2'`
  have "et⇣2 = (λs. True)⇣\<surd>" by(fastforce dest:WCFG_EntryD)
  thus ?case by simp
next
  case (WCFG_Entry prog)
  from `prog \<turnstile> n⇣2 -et⇣2-> n⇣2'` `(_Entry_) = n⇣2` `(_0_) ≠ n⇣2'`
  have "et⇣2 = (λs. False)⇣\<surd>" by(fastforce dest:WCFG_EntryD)
  thus ?case by simp
next
  case WCFG_Skip
  from `Skip \<turnstile> n⇣2 -et⇣2-> n⇣2'` `(_0_) = n⇣2` `(_Exit_) ≠ n⇣2'`
  have False by(fastforce elim:WCFG.While_CFG.cases)
  thus ?case by simp
next
  case (WCFG_LAss V e)
  from `V:=e \<turnstile> n⇣2 -et⇣2-> n⇣2'` `(_0_) = n⇣2` `(_1_) ≠ n⇣2'`
  have False by -(erule WCFG.While_CFG.cases,auto)
  thus ?case by simp
next
  case (WCFG_LAssSkip V e)
  from `V:=e \<turnstile> n⇣2 -et⇣2-> n⇣2'` `(_1_) = n⇣2` `(_Exit_) ≠ n⇣2'`
  have False by -(erule WCFG.While_CFG.cases,auto)
  thus ?case by simp
next
  case (WCFG_SeqFirst c⇣1 n et n' c⇣2)
  note IH = `!!n⇣2 n⇣2'. [|c⇣1 \<turnstile> n⇣2 -et⇣2-> n⇣2'; n = n⇣2; n' ≠ n⇣2'|]
  ==> ∃Q Q'. et = (Q)⇣\<surd> ∧ et⇣2 = (Q')⇣\<surd> ∧ (∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s))`
  from `c⇣1;;c⇣2 \<turnstile> n⇣2 -et⇣2-> n⇣2'` `c⇣1 \<turnstile> n -et-> n'` `n = n⇣2` `n' ≠ n⇣2'`
  have "c⇣1 \<turnstile> n⇣2 -et⇣2-> n⇣2' ∨ (c⇣1 \<turnstile> n⇣2 -et⇣2-> (_Exit_) ∧ n⇣2' = (_0_) ⊕ #:c⇣1)"
    apply - 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 "c⇣1 \<turnstile> n⇣2 -et⇣2-> n⇣2'"
    from IH[OF this `n = n⇣2` `n' ≠ n⇣2'`] show ?case .
  next
    assume "c⇣1 \<turnstile> n⇣2 -et⇣2-> (_Exit_) ∧ n⇣2' = (_0_) ⊕ #:c⇣1"
    hence edge:"c⇣1 \<turnstile> n⇣2 -et⇣2-> (_Exit_)" and n2':"n⇣2' = (_0_) ⊕ #:c⇣1" by simp_all
    from IH[OF edge `n = n⇣2` `n' ≠ (_Exit_)`] show ?case .
  qed
next
  case (WCFG_SeqConnect c⇣1 n et c⇣2)
  note IH = `!!n⇣2 n⇣2'. [|c⇣1 \<turnstile> n⇣2 -et⇣2-> n⇣2'; n = n⇣2; (_Exit_) ≠ n⇣2'|]
  ==> ∃Q Q'. et = (Q)⇣\<surd> ∧ et⇣2 = (Q')⇣\<surd> ∧ (∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s))`
  from `c⇣1;;c⇣2 \<turnstile> n⇣2 -et⇣2-> n⇣2'` `c⇣1 \<turnstile> n -et-> (_Exit_)` `n = n⇣2` `n ≠ (_Entry_)`
    `(_0_) ⊕ #:c⇣1 ≠ n⇣2'` have "c⇣1 \<turnstile> n⇣2 -et⇣2-> n⇣2' ∧ (_Exit_) ≠ n⇣2'"
    apply - 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 = n⇣2` this[THEN conjunct2]]
  show ?case .
next
  case (WCFG_SeqSecond c⇣2 n et n' c⇣1)
  note IH = `!!n⇣2 n⇣2'. [|c⇣2 \<turnstile> n⇣2 -et⇣2-> n⇣2'; n = n⇣2; n' ≠ n⇣2'|]
  ==> ∃Q Q'. et = (Q)⇣\<surd> ∧ et⇣2 = (Q')⇣\<surd> ∧ (∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s))`
  from `c⇣1;;c⇣2 \<turnstile> n⇣2 -et⇣2-> n⇣2'` `c⇣2 \<turnstile> n -et-> n'` `n ⊕ #:c⇣1 = n⇣2`
    `n' ⊕ #:c⇣1 ≠ n⇣2'` `n ≠ (_Entry_)`
  obtain nx where "c⇣2 \<turnstile> n -et⇣2-> nx ∧ nx ⊕ #:c⇣1 = n⇣2'"
    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' ⊕ #:c⇣1 ≠ n⇣2'` have edge:"c⇣2 \<turnstile> n -et⇣2-> nx" and neq:"n' ≠ nx"
    by auto
  from IH[OF edge _ neq] show ?case by simp
next
  case (WCFG_CondTrue b c⇣1 c⇣2)
  from `if (b) c⇣1 else c⇣2 \<turnstile> n⇣2 -et⇣2-> n⇣2'` `(_0_) = n⇣2` `(_0_) ⊕ 1 ≠ n⇣2'`
  show ?case by -(erule WCFG.While_CFG.cases,auto)
next
  case (WCFG_CondFalse b c⇣1 c⇣2)
  from `if (b) c⇣1 else c⇣2 \<turnstile> n⇣2 -et⇣2-> n⇣2'` `(_0_) = n⇣2` `(_0_) ⊕ #:c⇣1 + 1 ≠ n⇣2'`
  show ?case by -(erule WCFG.While_CFG.cases,auto)
next
  case (WCFG_CondThen c⇣1 n et n' b c⇣2)
  note IH = `!!n⇣2 n⇣2'. [|c⇣1 \<turnstile> n⇣2 -et⇣2-> n⇣2'; n = n⇣2; n' ≠ n⇣2'|]
    ==> ∃Q Q'. et = (Q)⇣\<surd> ∧ et⇣2 = (Q')⇣\<surd> ∧ (∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s))`
  from `if (b) c⇣1 else c⇣2 \<turnstile> n⇣2 -et⇣2-> n⇣2'` `c⇣1 \<turnstile> n -et-> n'` `n ≠ (_Entry_)` 
    `n ⊕ 1 = n⇣2` `n' ⊕ 1 ≠ n⇣2'`
  obtain nx where "c⇣1 \<turnstile> n -et⇣2-> 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 c⇣2 n et n' b c⇣1)
  note IH = `!!n⇣2 n⇣2'. [|c⇣2 \<turnstile> n⇣2 -et⇣2-> n⇣2'; n = n⇣2; n' ≠ n⇣2'|]
    ==> ∃Q Q'. et = (Q)⇣\<surd> ∧ et⇣2 = (Q')⇣\<surd> ∧ (∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s))`
  from `if (b) c⇣1 else c⇣2 \<turnstile> n⇣2 -et⇣2-> n⇣2'` `c⇣2 \<turnstile> n -et-> n'` `n ≠ (_Entry_)` 
    `n ⊕ #:c⇣1 + 1 = n⇣2` `n' ⊕ #:c⇣1 + 1 ≠ n⇣2'`
  obtain nx where "c⇣2 \<turnstile> n -et⇣2-> 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' \<turnstile> n⇣2 -et⇣2-> n⇣2'` `(_0_) = n⇣2` `(_0_) ⊕ 2 ≠ n⇣2'`
  show ?case by -(erule WCFG.While_CFG.cases,auto)
next
  case (WCFG_WhileFalse b c')
  from `while (b) c' \<turnstile> n⇣2 -et⇣2-> n⇣2'` `(_0_) = n⇣2` `(_1_) ≠ n⇣2'`
  show ?case by -(erule WCFG.While_CFG.cases,auto)
next
  case (WCFG_WhileFalseSkip b c')
  from `while (b) c' \<turnstile> n⇣2 -et⇣2-> n⇣2'` `(_1_) = n⇣2` `(_Exit_) ≠ n⇣2'`
  show ?case by -(erule WCFG.While_CFG.cases,auto dest:label_incr_ge)
next
  case (WCFG_WhileBody c' n et n' b)
  note IH = `!!n⇣2 n⇣2'. [|c' \<turnstile> n⇣2 -et⇣2-> n⇣2'; n = n⇣2; n' ≠ n⇣2'|]
    ==> ∃Q Q'. et = (Q)⇣\<surd> ∧ et⇣2 = (Q')⇣\<surd> ∧ (∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s))`
  from `while (b) c' \<turnstile> n⇣2 -et⇣2-> n⇣2'` `c' \<turnstile> n -et-> n'` `n ≠ (_Entry_)`
    `n' ≠ (_Exit_)` `n ⊕ 2 = n⇣2` `n' ⊕ 2 ≠ n⇣2'`
  obtain nx where "c' \<turnstile> n -et⇣2-> 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 = `!!n⇣2 n⇣2'. [|c' \<turnstile> n⇣2 -et⇣2-> n⇣2'; n = n⇣2; (_Exit_) ≠ n⇣2'|]
    ==> ∃Q Q'. et = (Q)⇣\<surd> ∧ et⇣2 = (Q')⇣\<surd> ∧ (∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s))`
  from `while (b) c' \<turnstile> n⇣2 -et⇣2-> n⇣2'` `c' \<turnstile> n -et-> (_Exit_)` `n ≠ (_Entry_)`
    `n ⊕ 2 = n⇣2` `(_0_) ≠ n⇣2'`
  obtain nx where "c' \<turnstile> n -et⇣2-> 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