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)_\<surd>→ (_Exit_)"

| WCFG_Entry:
  "prog ⊨ (_Entry_) -(λs. True)_\<surd>→ (_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:
  "[c₁ ⊨ n -et→ n'; n' ≠ (_Exit_)] ==> c₁;;c₂ ⊨ n -et→ n'"

| WCFG_SeqConnect: 
  "[c₁ ⊨ n -et→ (_Exit_); n ≠ (_Entry_)] ==> c₁;;c₂ ⊨ n -et→ (_0_) ⊕ #:c₁"

| WCFG_SeqSecond: 
  "[c₂ ⊨ n -et→ n'; n ≠ (_Entry_)] ==> c₁;;c₂ ⊨ n ⊕ #:c₁ -et→ n' ⊕ #:c₁"

| WCFG_CondTrue:
    "if (b) c₁ else c₂ ⊨ (_0_) -(λs. interpret b s = Some true)_\<surd>→ (_0_) ⊕ 1"

| WCFG_CondFalse:
    "if (b) c₁ else c₂ ⊨ (_0_) -(λs. interpret b s = Some false)_\<surd>→ (_0_) ⊕ (#:c₁ + 1)"

| WCFG_CondThen:
  "[c₁ ⊨ n -et→ n'; n ≠ (_Entry_)] ==> if (b) c₁ else c₂ ⊨ n ⊕ 1 -et→ n' ⊕ 1"

| WCFG_CondElse:
  "[c₂ ⊨ n -et→ n'; n ≠ (_Entry_)]
  ==> if (b) c₁ else c₂ ⊨ n ⊕ (#:c₁ + 1) -et→ n' ⊕ (#:c₁ + 1)"

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

| WCFG_WhileFalse:
    "while (b) c' ⊨ (_0_) -(λs. interpret b s = Some false)_\<surd>→ (_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 c₁ et n' c₂)
  from ‹l < #:c₁› show ?case by simp
next
  case (WCFG_SeqConnect c₁ et c₂)
  from ‹l < #:c₁› show ?case by simp
next
  case (WCFG_SeqSecond c₂ n et n' c₁)
  note IH = ‹∧l. n = (_ l _) ==> l < #:c₂›
  from ‹n ⊕ #:c₁ = (_ l _)› obtain l' where "n = (_ l' _)" by(cases n) auto
  from IH[OF this] have "l' < #:c₂" .
  with ‹n ⊕ #:c₁ = (_ l _)› ‹n = (_ l' _)› show ?case by simp
next
  case (WCFG_CondThen c₁ n et n' b c₂)
  note IH = ‹∧l. n = (_ l _) ==> l < #:c₁›
  from ‹n ⊕ 1 = (_ l _)› obtain l' where "n = (_ l' _)" by(cases n) auto
  from IH[OF this] have "l' < #:c₁" .
  with ‹n ⊕ 1 = (_ l _)› ‹n = (_ l' _)› show ?case by simp
next
  case (WCFG_CondElse c₂ n et n' b c₁)
  note IH = ‹∧l. n = (_ l _) ==> l < #:c₂›
  from ‹n ⊕ (#:c₁ + 1) = (_ l _)› obtain l' where "n = (_ l' _)" by(cases n) auto
  from IH[OF this] have "l' < #:c₂" .
  with ‹n ⊕ (#:c₁ + 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 c₁ n et c₂)
  from ‹l < #:c₁› show ?case by simp
next
  case (WCFG_SeqSecond c₂ n et n' c₁)
  note IH = ‹∧l. n' = (_ l _) ==> l < #:c₂›
  from ‹n' ⊕ #:c₁ = (_ l _)› obtain l' where "n' = (_ l' _)" by(cases n') auto
  from IH[OF this] have "l' < #:c₂" .
  with ‹n' ⊕ #:c₁ = (_ l _)› ‹n' = (_ l' _)› show ?case by simp
next
  case (WCFG_CondThen c₁ n et n' b c₂)
  note IH = ‹∧l. n' = (_ l _) ==> l < #:c₁›
  from ‹n' ⊕ 1 = (_ l _)› obtain l' where "n' = (_ l' _)" by(cases n') auto
  from IH[OF this] have "l' < #:c₁" .
  with ‹n' ⊕ 1 = (_ l _)› ‹n' = (_ l' _)› show ?case by simp
next
  case (WCFG_CondElse c₂ n et n' b c₁)
  note IH = ‹∧l. n' = (_ l _) ==> l < #:c₂›
  from ‹n' ⊕ (#:c₁ + 1) = (_ l _)› obtain l' where "n' = (_ l' _)" by(cases n') auto
  from IH[OF this] have "l' < #:c₂" .
  with ‹n' ⊕ (#:c₁ + 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)_\<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 ⊨ 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 c₁ n et n' c₂)
  note IH = ‹c₁ ⊨ n -et'→ n' ==> et = et'›
  from ‹c₁ ⊨ n -et→ n'› ‹n' ≠ (_Exit_)› obtain l where "n' = (_ l _)"
    by (cases n') auto
  with ‹c₁ ⊨ n -et→ n'› have "l < #:c₁" 
    by(fastforce intro:WCFG_targetlabel_less_num_nodes)
  with ‹c₁;;c₂ ⊨ n -et'→ n'› ‹n' = (_ l _)› have "c₁ ⊨ 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₁ n et c₂)
  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 ‹c₁;;c₂ ⊨ n -et'→ (_ 0 _) ⊕ #:c₁› ‹n = (_ l _)› have "c₁ ⊨ 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₂ n et n' c₁)
  note IH = ‹c₂ ⊨ n -et'→ n' ==> et = et'›
  from ‹c₂ ⊨ n -et→ n'› ‹n ≠ (_Entry_)› obtain l where "n = (_ l _)"
    by (cases n) auto
  with ‹c₂ ⊨ n -et→ n'› have "l < #:c₂"
    by(fastforce intro:WCFG_sourcelabel_less_num_nodes)
  with ‹c₁;;c₂ ⊨ n ⊕ #:c₁ -et'→ n' ⊕ #:c₁› ‹n = (_ l _)› have "c₂ ⊨ 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₁ n et n' b c₂)
  note IH = ‹c₁ ⊨ n -et'→ n' ==> et = et'›
  from ‹c₁ ⊨ n -et→ n'› ‹n ≠ (_Entry_)› obtain l where "n = (_ l _)"
    by (cases n) auto
  with ‹c₁ ⊨ n -et→ n'› have "l < #:c₁"
    by(fastforce intro:WCFG_sourcelabel_less_num_nodes)
  with ‹if (b) c₁ else c₂ ⊨ n ⊕ 1 -et'→ n' ⊕ 1› ‹n = (_ l _)›
  have "c₁ ⊨ 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₂ n et n' b c₁)
  note IH = ‹c₂ ⊨ n -et'→ n' ==> et = et'›
  from ‹c₂ ⊨ n -et→ n'› ‹n ≠ (_Entry_)› obtain l where "n = (_ l _)"
    by (cases n) auto
  with ‹c₂ ⊨ n -et→ n'› have "l < #:c₂"
    by(fastforce intro:WCFG_sourcelabel_less_num_nodes)
  with ‹if (b) c₁ else c₂ ⊨ n ⊕ (#:c₁ + 1) -et'→ n' ⊕ (#:c₁ + 1)› ‹n = (_ l _)›
  have "c₂ ⊨ 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)_\<surd>→ (_ 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)_\<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 ⊨ 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)_\<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 ⊨ 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)_\<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 ⊨ 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)_\<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' ⊨ (_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' ⊨ 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)_\<surd>→
                                  (_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 ⊨ n₁ -et₁→ n₁'; prog ⊨ n₂ -et₂→ n₂'; n₁ = n₂; n₁' ≠ n₂']
  ==> ∃Q Q'. et₁ = (Q)_\<surd> ∧ et₂ = (Q')_\<surd> ∧ (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))"
proof(induct arbitrary:n₂ n₂' rule:WCFG_induct)
  case (WCFG_Entry_Exit prog)
  from ‹prog ⊨ n₂ -et₂→ n₂'› ‹(_Entry_) = n₂› ‹(_Exit_) ≠ n₂'›
  have "et₂ = (λs. True)_\<surd>" by(fastforce dest:WCFG_EntryD)
  thus ?case by simp
next
  case (WCFG_Entry prog)
  from ‹prog ⊨ n₂ -et₂→ n₂'› ‹(_Entry_) = n₂› ‹(_0_) ≠ n₂'›
  have "et₂ = (λs. False)_\<surd>" by(fastforce dest:WCFG_EntryD)
  thus ?case by simp
next
  case WCFG_Skip
  from ‹Skip ⊨ n₂ -et₂→ n₂'› ‹(_0_) = n₂› ‹(_Exit_) ≠ n₂'›
  have False by(fastforce elim:WCFG.While_CFG.cases)
  thus ?case by simp
next
  case (WCFG_LAss V e)
  from ‹V:=e ⊨ n₂ -et₂→ n₂'› ‹(_0_) = n₂› ‹(_1_) ≠ n₂'›
  have False by -(erule WCFG.While_CFG.cases,auto)
  thus ?case by simp
next
  case (WCFG_LAssSkip V e)
  from ‹V:=e ⊨ n₂ -et₂→ n₂'› ‹(_1_) = n₂› ‹(_Exit_) ≠ n₂'›
  have False by -(erule WCFG.While_CFG.cases,auto)
  thus ?case by simp
next
  case (WCFG_SeqFirst c₁ n et n' c₂)
  note IH = ‹∧n₂ n₂'. [c₁ ⊨ n₂ -et₂→ n₂'; n = n₂; n' ≠ n₂']
 ==> ∃Q Q'. et = (Q)_\√ ∧ et₂ = (Q')_\√ ∧ (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
  from ‹c₁;;c₂ ⊨ n₂ -et₂→ n₂'› ‹c₁ ⊨ n -et→ n'› ‹n = n₂› ‹n' ≠ n₂'›
  have "c₁ ⊨ n₂ -et₂→ n₂' ∨ (c₁ ⊨ n₂ -et₂→ (_Exit_) ∧ n₂' = (_0_) ⊕ #:c₁)"
    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 "c₁ ⊨ n₂ -et₂→ n₂'"
    from IH[OF this ‹n = n₂› ‹n' ≠ n₂'›] show ?case .
  next
    assume "c₁ ⊨ n₂ -et₂→ (_Exit_) ∧ n₂' = (_0_) ⊕ #:c₁"
    hence edge:"c₁ ⊨ n₂ -et₂→ (_Exit_)" and n2':"n₂' = (_0_) ⊕ #:c₁" by simp_all
    from IH[OF edge ‹n = n₂› ‹n' ≠ (_Exit_)›] show ?case .
  qed
next
  case (WCFG_SeqConnect c₁ n et c₂)
  note IH = ‹∧n₂ n₂'. [c₁ ⊨ n₂ -et₂→ n₂'; n = n₂; (_Exit_) ≠ n₂']
 ==> ∃Q Q'. et = (Q)_\√ ∧ et₂ = (Q')_\√ ∧ (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
  from ‹c₁;;c₂ ⊨ n₂ -et₂→ n₂'› ‹c₁ ⊨ n -et→ (_Exit_)› ‹n = n₂› ‹n ≠ (_Entry_)›
    ‹(_0_) ⊕ #:c₁ ≠ n₂'› have "c₁ ⊨ n₂ -et₂→ n₂' ∧ (_Exit_) ≠ n₂'"
    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 = n₂› this[THEN conjunct2]]
  show ?case .
next
  case (WCFG_SeqSecond c₂ n et n' c₁)
  note IH = ‹∧n₂ n₂'. [c₂ ⊨ n₂ -et₂→ n₂'; n = n₂; n' ≠ n₂']
 ==> ∃Q Q'. et = (Q)_\√ ∧ et₂ = (Q')_\√ ∧ (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
  from ‹c₁;;c₂ ⊨ n₂ -et₂→ n₂'› ‹c₂ ⊨ n -et→ n'› ‹n ⊕ #:c₁ = n₂›
    ‹n' ⊕ #:c₁ ≠ n₂'› ‹n ≠ (_Entry_)›
  obtain nx where "c₂ ⊨ n -et₂→ nx ∧ nx ⊕ #:c₁ = n₂'"
    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₁ ≠ n₂'› have edge:"c₂ ⊨ n -et₂→ nx" and neq:"n' ≠ nx"
    by auto
  from IH[OF edge _ neq] show ?case by simp
next
  case (WCFG_CondTrue b c₁ c₂)
  from ‹if (b) c₁ else c₂ ⊨ n₂ -et₂→ n₂'› ‹(_0_) = n₂› ‹(_0_) ⊕ 1 ≠ n₂'›
  show ?case by -(erule WCFG.While_CFG.cases,auto)
next
  case (WCFG_CondFalse b c₁ c₂)
  from ‹if (b) c₁ else c₂ ⊨ n₂ -et₂→ n₂'› ‹(_0_) = n₂› ‹(_0_) ⊕ #:c₁ + 1 ≠ n₂'›
  show ?case by -(erule WCFG.While_CFG.cases,auto)
next
  case (WCFG_CondThen c₁ n et n' b c₂)
  note IH = ‹∧n₂ n₂'. [c₁ ⊨ n₂ -et₂→ n₂'; n = n₂; n' ≠ n₂']
 ==> ∃Q Q'. et = (Q)_\√ ∧ et₂ = (Q')_\√ ∧ (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
  from ‹if (b) c₁ else c₂ ⊨ n₂ -et₂→ n₂'› ‹c₁ ⊨ n -et→ n'› ‹n ≠ (_Entry_)›
    ‹n ⊕ 1 = n₂› ‹n' ⊕ 1 ≠ n₂'›
  obtain nx where "c₁ ⊨ n -et₂→ 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₂ n et n' b c₁)
  note IH = ‹∧n₂ n₂'. [c₂ ⊨ n₂ -et₂→ n₂'; n = n₂; n' ≠ n₂']
 ==> ∃Q Q'. et = (Q)_\√ ∧ et₂ = (Q')_\√ ∧ (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
  from ‹if (b) c₁ else c₂ ⊨ n₂ -et₂→ n₂'› ‹c₂ ⊨ n -et→ n'› ‹n ≠ (_Entry_)›
    ‹n ⊕ #:c₁ + 1 = n₂› ‹n' ⊕ #:c₁ + 1 ≠ n₂'›
  obtain nx where "c₂ ⊨ n -et₂→ 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' ⊨ n₂ -et₂→ n₂'› ‹(_0_) = n₂› ‹(_0_) ⊕ 2 ≠ n₂'›
  show ?case by -(erule WCFG.While_CFG.cases,auto)
next
  case (WCFG_WhileFalse b c')
  from ‹while (b) c' ⊨ n₂ -et₂→ n₂'› ‹(_0_) = n₂› ‹(_1_) ≠ n₂'›
  show ?case by -(erule WCFG.While_CFG.cases,auto)
next
  case (WCFG_WhileFalseSkip b c')
  from ‹while (b) c' ⊨ n₂ -et₂→ n₂'› ‹(_1_) = n₂› ‹(_Exit_) ≠ n₂'›
  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₂ n₂'. [c' ⊨ n₂ -et₂→ n₂'; n = n₂; n' ≠ n₂']
 ==> ∃Q Q'. et = (Q)_\√ ∧ et₂ = (Q')_\√ ∧ (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
  from ‹while (b) c' ⊨ n₂ -et₂→ n₂'› ‹c' ⊨ n -et→ n'› ‹n ≠ (_Entry_)›
    ‹n' ≠ (_Exit_)› ‹n ⊕ 2 = n₂› ‹n' ⊕ 2 ≠ n₂'›
  obtain nx where "c' ⊨ n -et₂→ 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₂ n₂'. [c' ⊨ n₂ -et₂→ n₂'; n = n₂; (_Exit_) ≠ n₂']
 ==> ∃Q Q'. et = (Q)_\√ ∧ et₂ = (Q')_\√ ∧ (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
  from ‹while (b) c' ⊨ n₂ -et₂→ n₂'› ‹c' ⊨ n -et→ (_Exit_)› ‹n ≠ (_Entry_)›
    ‹n ⊕ 2 = n₂› ‹(_0_) ≠ n₂'›
  obtain nx where "c' ⊨ n -et₂→ 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