# 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:
"⟦c⇩1 ⊢ n -et→ n'; n' ≠ (_Exit_)⟧ ⟹ c⇩1;;c⇩2 ⊢ n -et→ n'"

| WCFG_SeqConnect:
"⟦c⇩1 ⊢ n -et→ (_Exit_); n ≠ (_Entry_)⟧ ⟹ c⇩1;;c⇩2 ⊢ n -et→ (_0_) ⊕ #:c⇩1"

| WCFG_SeqSecond:
"⟦c⇩2 ⊢ n -et→ n'; n ≠ (_Entry_)⟧ ⟹ c⇩1;;c⇩2 ⊢ n ⊕ #:c⇩1 -et→ n' ⊕ #:c⇩1"

| WCFG_CondTrue:
"if (b) c⇩1 else c⇩2 ⊢ (_0_) -(λs. interpret b s = Some true)⇩√→ (_0_) ⊕ 1"

| WCFG_CondFalse:
"if (b) c⇩1 else c⇩2 ⊢ (_0_) -(λs. interpret b s = Some false)⇩√→ (_0_) ⊕ (#:c⇩1 + 1)"

| WCFG_CondThen:
"⟦c⇩1 ⊢ n -et→ n'; n ≠ (_Entry_)⟧ ⟹ if (b) c⇩1 else c⇩2 ⊢ n ⊕ 1 -et→ n' ⊕ 1"

| WCFG_CondElse:
"⟦c⇩2 ⊢ n -et→ n'; n ≠ (_Entry_)⟧
⟹ if (b) c⇩1 else c⇩2 ⊢ n ⊕ (#:c⇩1 + 1) -et→ n' ⊕ (#:c⇩1 + 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 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 ⊢ 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 ⊢ (_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 c⇩1 n et n' c⇩2)
note IH = ‹c⇩1 ⊢ n -et'→ n' ⟹ et = et'›
from ‹c⇩1 ⊢ n -et→ n'› ‹n' ≠ (_Exit_)› obtain l where "n' = (_ l _)"
by (cases n') auto
with ‹c⇩1 ⊢ n -et→ n'› have "l < #:c⇩1"
by(fastforce intro:WCFG_targetlabel_less_num_nodes)
with ‹c⇩1;;c⇩2 ⊢ n -et'→ n'› ‹n' = (_ l _)› have "c⇩1 ⊢ 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 ⊢ n -et'→ (_Exit_) ⟹ et = et'›
from ‹c⇩1 ⊢ n -et→ (_Exit_)› ‹n ≠ (_Entry_)› obtain l where "n = (_ l _)"
by (cases n) auto
with ‹c⇩1 ⊢ n -et→ (_Exit_)› have "l < #:c⇩1"
by(fastforce intro:WCFG_sourcelabel_less_num_nodes)
with ‹c⇩1;;c⇩2 ⊢ n -et'→ (_ 0 _) ⊕ #:c⇩1› ‹n = (_ l _)› have "c⇩1 ⊢ 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 ⊢ n -et'→ n' ⟹ et = et'›
from ‹c⇩2 ⊢ n -et→ n'› ‹n ≠ (_Entry_)› obtain l where "n = (_ l _)"
by (cases n) auto
with ‹c⇩2 ⊢ n -et→ n'› have "l < #:c⇩2"
by(fastforce intro:WCFG_sourcelabel_less_num_nodes)
with ‹c⇩1;;c⇩2 ⊢ n ⊕ #:c⇩1 -et'→ n' ⊕ #:c⇩1› ‹n = (_ l _)› have "c⇩2 ⊢ 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 ⊢ n -et'→ n' ⟹ et = et'›
from ‹c⇩1 ⊢ n -et→ n'› ‹n ≠ (_Entry_)› obtain l where "n = (_ l _)"
by (cases n) auto
with ‹c⇩1 ⊢ n -et→ n'› have "l < #:c⇩1"
by(fastforce intro:WCFG_sourcelabel_less_num_nodes)
with ‹if (b) c⇩1 else c⇩2 ⊢ n ⊕ 1 -et'→ n' ⊕ 1› ‹n = (_ l _)›
have "c⇩1 ⊢ 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 ⊢ n -et'→ n' ⟹ et = et'›
from ‹c⇩2 ⊢ n -et→ n'› ‹n ≠ (_Entry_)› obtain l where "n = (_ l _)"
by (cases n) auto
with ‹c⇩2 ⊢ n -et→ n'› have "l < #:c⇩2"
by(fastforce intro:WCFG_sourcelabel_less_num_nodes)
with ‹if (b) c⇩1 else c⇩2 ⊢ n ⊕ (#:c⇩1 + 1) -et'→ n' ⊕ (#:c⇩1 + 1)› ‹n = (_ l _)›
have "c⇩2 ⊢ 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

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"
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 ⊢ n⇩1 -et⇩1→ n⇩1'; prog ⊢ n⇩2 -et⇩2→ n⇩2'; n⇩1 = n⇩2; n⇩1' ≠ n⇩2'⟧
⟹ ∃Q Q'. et⇩1 = (Q)⇩√ ∧ et⇩2 = (Q')⇩√ ∧ (∀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 ⊢ n⇩2 -et⇩2→ n⇩2'› ‹(_Entry_) = n⇩2› ‹(_Exit_) ≠ n⇩2'›
have "et⇩2 = (λs. True)⇩√" by(fastforce dest:WCFG_EntryD)
thus ?case by simp
next
case (WCFG_Entry prog)
from ‹prog ⊢ n⇩2 -et⇩2→ n⇩2'› ‹(_Entry_) = n⇩2› ‹(_0_) ≠ n⇩2'›
have "et⇩2 = (λs. False)⇩√" by(fastforce dest:WCFG_EntryD)
thus ?case by simp
next
case WCFG_Skip
from ‹Skip ⊢ 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 ⊢ 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 ⊢ 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 ⊢ n⇩2 -et⇩2→ n⇩2'; n = n⇩2; n' ≠ n⇩2'⟧
⟹ ∃Q Q'. et = (Q)⇩√ ∧ et⇩2 = (Q')⇩√ ∧ (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
from ‹c⇩1;;c⇩2 ⊢ n⇩2 -et⇩2→ n⇩2'› ‹c⇩1 ⊢ n -et→ n'› ‹n = n⇩2› ‹n' ≠ n⇩2'›
have "c⇩1 ⊢ n⇩2 -et⇩2→ n⇩2' ∨ (c⇩1 ⊢ n⇩2 -et⇩2→ (_Exit_) ∧ n⇩2' = (_0_) ⊕ #:c⇩1)"
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⇩1 ⊢ n⇩2 -et⇩2→ n⇩2'"
from IH[OF this ‹n = n⇩2› ‹n' ≠ n⇩2'›] show ?case .
next
assume "c⇩1 ⊢ n⇩2 -et⇩2→ (_Exit_) ∧ n⇩2' = (_0_) ⊕ #:c⇩1"
hence edge:"c⇩1 ⊢ 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 ⊢ n⇩2 -et⇩2→ n⇩2'; n = n⇩2; (_Exit_) ≠ n⇩2'⟧
⟹ ∃Q Q'. et = (Q)⇩√ ∧ et⇩2 = (Q')⇩√ ∧ (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
from ‹c⇩1;;c⇩2 ⊢ n⇩2 -et⇩2→ n⇩2'› ‹c⇩1 ⊢ n -et→ (_Exit_)› ‹n = n⇩2› ‹n ≠ (_Entry_)›
‹(_0_) ⊕ #:c⇩1 ≠ n⇩2'› have "c⇩1 ⊢ n⇩2 -et⇩2→ n⇩2' ∧ (_Exit_) ≠ n⇩2'"
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⇩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 ⊢ n⇩2 -et⇩2→ n⇩2'; n = n⇩2; n' ≠ n⇩2'⟧
⟹ ∃Q Q'. et = (Q)⇩√ ∧ et⇩2 = (Q')⇩√ ∧ (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
from ‹c⇩1;;c⇩2 ⊢ n⇩2 -et⇩2→ n⇩2'› ‹c⇩2 ⊢ n -et→ n'› ‹n ⊕ #:c⇩1 = n⇩2›
‹n' ⊕ #:c⇩1 ≠ n⇩2'› ‹n ≠ (_Entry_)›
obtain nx where "c⇩2 ⊢ 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 ⊢ 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 ⊢ 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 ⊢ 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 ⊢ n⇩2 -et⇩2→ n⇩2'; n = n⇩2; n' ≠ n⇩2'⟧
⟹ ∃Q Q'. et = (Q)⇩√ ∧ et⇩2 = (Q')⇩√ ∧ (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
from ‹if (b) c⇩1 else c⇩2 ⊢ n⇩2 -et⇩2→ n⇩2'› ‹c⇩1 ⊢ n -et→ n'› ‹n ≠ (_Entry_)›
‹n ⊕ 1 = n⇩2› ‹n' ⊕ 1 ≠ n⇩2'›
obtain nx where "c⇩1 ⊢ 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 ⊢ n⇩2 -et⇩2→ n⇩2'; n = n⇩2; n' ≠ n⇩2'⟧
⟹ ∃Q Q'. et = (Q)⇩√ ∧ et⇩2 = (Q')⇩√ ∧ (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
from ‹if (b) c⇩1 else c⇩2 ⊢ n⇩2 -et⇩2→ n⇩2'› ‹c⇩2 ⊢ n -et→ n'› ‹n ≠ (_Entry_)›
‹n ⊕ #:c⇩1 + 1 = n⇩2› ‹n' ⊕ #:c⇩1 + 1 ≠ n⇩2'›
obtain nx where "c⇩2 ⊢ 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' ⊢ 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' ⊢ 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' ⊢ 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' ⊢ n⇩2 -et⇩2→ n⇩2'; n = n⇩2; n' ≠ n⇩2'⟧
⟹ ∃Q Q'. et = (Q)⇩√ ∧ et⇩2 = (Q')⇩√ ∧ (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
from ‹while (b) c' ⊢ n⇩2 -et⇩2→ n⇩2'› ‹c' ⊢ n -et→ n'› ‹n ≠ (_Entry_)›
‹n' ≠ (_Exit_)› ‹n ⊕ 2 = n⇩2› ‹n' ⊕ 2 ≠ n⇩2'›
obtain nx where "c' ⊢ 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' ⊢ n⇩2 -et⇩2→ n⇩2'; n = n⇩2; (_Exit_) ≠ n⇩2'⟧
⟹ ∃Q Q'. et = (Q)⇩√ ∧ et⇩2 = (Q')⇩√ ∧ (∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))›
from ‹while (b) c' ⊢ n⇩2 -et⇩2→ n⇩2'› ‹c' ⊢ n -et→ (_Exit_)› ‹n ≠ (_Entry_)›
‹n ⊕ 2 = n⇩2› ‹(_0_) ≠ n⇩2'›
obtain nx where "c' ⊢ 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
```