# Theory WellFormed

```section ‹General well-formedness of While CFG›

theory WellFormed imports
Interpretation
Labels
"../Basic/CFGExit_wf"
"../StaticIntra/CDepInstantiations"
begin

subsection ‹Definition of some functions›

fun lhs :: "cmd ⇒ vname set"
where
"lhs Skip                = {}"
| "lhs (V:=e)              = {V}"
| "lhs (c⇩1;;c⇩2)            = lhs c⇩1"
| "lhs (if (b) c⇩1 else c⇩2) = {}"
| "lhs (while (b) c)       = {}"

fun rhs_aux :: "expr ⇒ vname set"
where
"rhs_aux (Val v)       = {}"
| "rhs_aux (Var V)       = {V}"
| "rhs_aux (e1 «bop» e2) = (rhs_aux e1 ∪ rhs_aux e2)"

fun rhs :: "cmd ⇒ vname set"
where
"rhs Skip                = {}"
| "rhs (V:=e)              = rhs_aux e"
| "rhs (c⇩1;;c⇩2)            = rhs c⇩1"
| "rhs (if (b) c⇩1 else c⇩2) = rhs_aux b"
| "rhs (while (b) c)       = rhs_aux b"

lemma rhs_interpret_eq:
"⟦interpret b s = Some v'; ∀V ∈ rhs_aux b. s V = s' V⟧
⟹ interpret b s' = Some v'"
proof(induct b arbitrary:v')
case (Val v)
from ‹interpret (Val v) s = Some v'› have "v' = v" by(fastforce elim:interpret.cases)
thus ?case by simp
next
case (Var V)
hence "s' V = Some v'" by(fastforce elim:interpret.cases)
thus ?case by simp
next
case (BinOp b1 bop b2)
note IH1 = ‹⋀v'. ⟦interpret b1 s = Some v'; ∀V ∈ rhs_aux b1. s V = s' V⟧
⟹ interpret b1 s' = Some v'›
note IH2 = ‹⋀v'. ⟦interpret b2 s = Some v'; ∀V ∈ rhs_aux b2. s V = s' V⟧
⟹ interpret b2 s' = Some v'›
from ‹interpret (b1 «bop» b2) s = Some v'›
have "∃v⇩1 v⇩2. interpret b1 s = Some v⇩1 ∧ interpret b2 s = Some v⇩2 ∧
binop bop v⇩1 v⇩2 = Some v'"
apply(cases "interpret b1 s",simp)
apply(cases "interpret b2 s",simp)
by(case_tac "binop bop a aa",simp+)
then obtain v⇩1 v⇩2 where "interpret b1 s = Some v⇩1"
and "interpret b2 s = Some v⇩2" and "binop bop v⇩1 v⇩2 = Some v'" by blast
from ‹∀V ∈ rhs_aux (b1 «bop» b2). s V = s' V› have "∀V ∈ rhs_aux b1. s V = s' V"
by simp
from IH1[OF ‹interpret b1 s = Some v⇩1› this] have "interpret b1 s' = Some v⇩1" .
from ‹∀V ∈ rhs_aux (b1 «bop» b2). s V = s' V› have "∀V ∈ rhs_aux b2. s V = s' V"
by simp
from IH2[OF ‹interpret b2 s = Some v⇩2› this] have "interpret b2 s' = Some v⇩2" .
with ‹interpret b1 s' = Some v⇩1› ‹binop bop v⇩1 v⇩2 = Some v'› show ?case by simp
qed

fun Defs :: "cmd ⇒ w_node ⇒ vname set"
where "Defs prog n = {V. ∃l c.  n = (_ l _) ∧ labels prog l c ∧ V ∈ lhs c}"

fun Uses :: "cmd ⇒ w_node ⇒ vname set"
where "Uses prog n = {V. ∃l c.  n = (_ l _) ∧ labels prog l c ∧ V ∈ rhs c}"

subsection ‹Lemmas about @{term "prog ⊢ n -et→ n'"} to show well-formed
properties›

lemma WCFG_edge_no_Defs_equal:
"⟦prog ⊢ n -et→ n'; V ∉ Defs prog n⟧ ⟹ (transfer et s) V = s V"
proof(induct rule:WCFG_induct)
case (WCFG_LAss V' e)
have label:"labels (V':=e) 0 (V':=e)" and lhs:"V' ∈ lhs (V':=e)"
by(auto intro:Labels_Base)
hence "V' ∈ Defs (V':=e) (_0_)" by fastforce
with ‹V ∉ Defs (V':=e) (_0_)› show ?case by auto
next
case (WCFG_SeqFirst c⇩1 n et n' c⇩2)
note IH = ‹V ∉ Defs c⇩1 n ⟹ transfer et s V = s V›
have "V ∉ Defs c⇩1 n"
proof
assume "V ∈ Defs c⇩1 n"
then obtain c l where [simp]:"n = (_ l _)" and "labels c⇩1 l c"
and "V ∈ lhs c" by fastforce
from ‹labels c⇩1 l c› have "labels (c⇩1;;c⇩2) l (c;;c⇩2)"
by(fastforce intro:Labels_Seq1)
from ‹V ∈ lhs c› have "V ∈ lhs (c;;c⇩2)" by simp
with ‹labels (c⇩1;;c⇩2) l (c;;c⇩2)› have "V ∈ Defs (c⇩1;;c⇩2) n" by fastforce
with ‹V ∉ Defs (c⇩1;;c⇩2) n› show False by fastforce
qed
from IH[OF this] show ?case .
next
case (WCFG_SeqConnect c⇩1 n et c⇩2)
note IH = ‹V ∉ Defs c⇩1 n ⟹ transfer et s V = s V›
have "V ∉ Defs c⇩1 n"
proof
assume "V ∈ Defs c⇩1 n"
then obtain c l where [simp]:"n = (_ l _)" and "labels c⇩1 l c"
and "V ∈ lhs c" by fastforce
from ‹labels c⇩1 l c› have "labels (c⇩1;;c⇩2) l (c;;c⇩2)"
by(fastforce intro:Labels_Seq1)
from ‹V ∈ lhs c› have "V ∈ lhs (c;;c⇩2)" by simp
with ‹labels (c⇩1;;c⇩2) l (c;;c⇩2)› have "V ∈ Defs (c⇩1;;c⇩2) n" by fastforce
with ‹V ∉ Defs (c⇩1;;c⇩2) n› show False by fastforce
qed
from IH[OF this] show ?case .
next
case (WCFG_SeqSecond c⇩2 n et n' c⇩1)
note IH = ‹V ∉ Defs c⇩2 n ⟹ transfer et s V = s V›
have "V ∉ Defs c⇩2 n"
proof
assume "V ∈ Defs c⇩2 n"
then obtain c l where [simp]:"n = (_ l _)" and "labels c⇩2 l c"
and "V ∈ lhs c" by fastforce
from ‹labels c⇩2 l c› have "labels (c⇩1;;c⇩2) (l + #:c⇩1) c"
by(fastforce intro:Labels_Seq2)
with ‹V ∈ lhs c› have "V ∈ Defs (c⇩1;;c⇩2) (n ⊕ #:c⇩1)" by fastforce
with ‹V ∉ Defs (c⇩1;;c⇩2) (n ⊕ #:c⇩1)› show False by fastforce
qed
from IH[OF this] show ?case .
next
case (WCFG_CondThen c⇩1 n et n' b c⇩2)
note IH = ‹V ∉ Defs c⇩1 n ⟹ transfer et s V = s V›
have "V ∉ Defs c⇩1 n"
proof
assume "V ∈ Defs c⇩1 n"
then obtain c l where [simp]:"n = (_ l _)" and "labels c⇩1 l c"
and "V ∈ lhs c" by fastforce
from ‹labels c⇩1 l c› have "labels (if (b) c⇩1 else c⇩2) (l + 1) c"
by(fastforce intro:Labels_CondTrue)
with ‹V ∈ lhs c› have "V ∈ Defs (if (b) c⇩1 else c⇩2) (n ⊕ 1)" by fastforce
with ‹V ∉ Defs (if (b) c⇩1 else c⇩2) (n ⊕ 1)› show False by fastforce
qed
from IH[OF this] show ?case .
next
case (WCFG_CondElse c⇩2 n et n' b c⇩1)
note IH = ‹V ∉ Defs c⇩2 n ⟹ transfer et s V = s V›
have "V ∉ Defs c⇩2 n"
proof
assume "V ∈ Defs c⇩2 n"
then obtain c l where [simp]:"n = (_ l _)" and "labels c⇩2 l c"
and "V ∈ lhs c" by fastforce
from ‹labels c⇩2 l c› have "labels (if (b) c⇩1 else c⇩2) (l + #:c⇩1 + 1) c"
by(fastforce intro:Labels_CondFalse)
with ‹V ∈ lhs c› have "V ∈ Defs (if (b) c⇩1 else c⇩2) (n ⊕ #:c⇩1 + 1)"
with ‹V ∉ Defs (if (b) c⇩1 else c⇩2) (n ⊕ #:c⇩1 + 1)› show False by fastforce
qed
from IH[OF this] show ?case .
next
case (WCFG_WhileBody c' n et n' b)
note IH = ‹V ∉ Defs c' n ⟹ transfer et s V = s V›
have "V ∉ Defs c' n"
proof
assume "V ∈ Defs c' n"
then obtain c l where [simp]:"n = (_ l _)" and "labels c' l c"
and "V ∈ lhs c" by fastforce
from ‹labels c' l c› have "labels (while (b) c') (l + 2) (c;;while (b) c')"
by(fastforce intro:Labels_WhileBody)
from ‹V ∈ lhs c› have "V ∈ lhs (c;;while (b) c')" by fastforce
with ‹labels (while (b) c') (l + 2) (c;;while (b) c')›
have "V ∈ Defs (while (b) c') (n ⊕ 2)" by fastforce
with ‹V ∉ Defs (while (b) c') (n ⊕ 2)› show False by fastforce
qed
from IH[OF this] show ?case .
next
case (WCFG_WhileBodyExit c' n et b)
note IH = ‹V ∉ Defs c' n ⟹ transfer et s V = s V›
have "V ∉ Defs c' n"
proof
assume "V ∈ Defs c' n"
then obtain c l where [simp]:"n = (_ l _)" and "labels c' l c"
and "V ∈ lhs c" by fastforce
from ‹labels c' l c› have "labels (while (b) c') (l + 2) (c;;while (b) c')"
by(fastforce intro:Labels_WhileBody)
from ‹V ∈ lhs c› have "V ∈ lhs (c;;while (b) c')" by fastforce
with ‹labels (while (b) c') (l + 2) (c;;while (b) c')›
have "V ∈ Defs (while (b) c') (n ⊕ 2)" by fastforce
with ‹V ∉ Defs (while (b) c') (n ⊕ 2)› show False by fastforce
qed
from IH[OF this] show ?case .
qed auto

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

lemma WCFG_edge_transfer_uses_only_Uses:
"⟦prog ⊢ n -et→ n'; ∀V ∈ Uses prog n. s V = s' V⟧
⟹ ∀V ∈ Defs prog n. (transfer et s) V = (transfer et s') V"
proof(induct rule:WCFG_induct)
case (WCFG_LAss V e)
have "Uses (V:=e) (_0_) = {V. V ∈ rhs_aux e}"
by(fastforce elim:labels.cases intro:Labels_Base)
with ‹∀V'∈Uses (V:=e) (_0_). s V' = s' V'›
have "∀V'∈rhs_aux e. s V' = s' V'" by blast
have "Defs (V:=e) (_0_) = {V}"
by(fastforce elim:labels.cases intro:Labels_Base)
have "transfer ⇑λs. s(V := interpret e s) s V =
transfer ⇑λs. s(V := interpret e s) s' V"
proof(cases "interpret e s")
case None
{ fix v assume "interpret e s' = Some v"
with ‹∀V'∈rhs_aux e. s V' = s' V'› have "interpret e s = Some v"
by(fastforce intro:rhs_interpret_eq)
with None have False by(fastforce split:if_split_asm) }
with None show ?thesis by fastforce
next
case (Some v)
hence "interpret e s = Some v" by(fastforce split:if_split_asm)
with ‹∀V'∈rhs_aux e. s V' = s' V'›
have "interpret e s' = Some v" by(fastforce intro:rhs_interpret_eq)
with Some show ?thesis by simp
qed
with ‹Defs (V:=e) (_0_) = {V}› show ?case by simp
next
case (WCFG_SeqFirst c⇩1 n et n' c⇩2)
note IH = ‹∀V∈Uses c⇩1 n. s V = s' V
⟹ ∀V∈Defs c⇩1 n. transfer et s V = transfer et s' V›
from ‹∀V∈Uses (c⇩1;;c⇩2) n. s V = s' V› have "∀V∈Uses c⇩1 n. s V = s' V"
by auto(drule Labels_Seq1[of _ _ _ c⇩2],erule_tac x="V" in allE,auto)
from IH[OF this] have "∀V∈Defs c⇩1 n. transfer et s V = transfer et s' V" .
with ‹c⇩1 ⊢ n -et→ n'› show ?case using Labels_Base
apply clarsimp
apply(erule labels.cases,auto dest:WCFG_sourcelabel_less_num_nodes)
by(erule_tac x="V" in allE,fastforce)
next
case (WCFG_SeqConnect c⇩1 n et c⇩2)
note IH = ‹∀V∈Uses c⇩1 n. s V = s' V
⟹ ∀V∈Defs c⇩1 n. transfer et s V = transfer et s' V›
from ‹∀V∈Uses (c⇩1;;c⇩2) n. s V = s' V› have "∀V∈Uses c⇩1 n. s V = s' V"
by auto(drule Labels_Seq1[of _ _ _ c⇩2],erule_tac x="V" in allE,auto)
from IH[OF this] have "∀V∈Defs c⇩1 n. transfer et s V = transfer et s' V" .
with ‹c⇩1 ⊢ n -et→ (_Exit_)› show ?case using Labels_Base
apply clarsimp
apply(erule labels.cases,auto dest:WCFG_sourcelabel_less_num_nodes)
by(erule_tac x="V" in allE,fastforce)
next
case (WCFG_SeqSecond c⇩2 n et n' c⇩1)
note IH = ‹∀V∈Uses c⇩2 n. s V = s' V
⟹ ∀V∈Defs c⇩2 n. transfer et s V = transfer et s' V›
from ‹∀V∈Uses (c⇩1;;c⇩2) (n ⊕ #:c⇩1). s V = s' V› have "∀V∈Uses c⇩2 n. s V = s' V"
by(auto,blast dest:Labels_Seq2)
from IH[OF this] have "∀V∈Defs c⇩2 n. transfer et s V = transfer et s' V" .
with num_inner_nodes_gr_0[of "c⇩1"] show ?case
apply clarsimp
apply(erule labels.cases,auto)
by(cases n,auto dest:label_less_num_inner_nodes)+
next
case (WCFG_CondThen c⇩1 n et n' b c⇩2)
note IH = ‹∀V∈Uses c⇩1 n. s V = s' V
⟹ ∀V∈Defs c⇩1 n. transfer et s V = transfer et s' V›
from ‹∀V∈Uses (if (b) c⇩1 else c⇩2) (n ⊕ 1). s V = s' V›
have "∀V∈Uses c⇩1 n. s V = s' V" by(auto,blast dest:Labels_CondTrue)
from IH[OF this] have "∀V∈Defs c⇩1 n. transfer et s V = transfer et s' V" .
with ‹c⇩1 ⊢ n -et→ n'› show ?case
apply clarsimp
apply(erule labels.cases,auto)
apply(cases n,auto dest:label_less_num_inner_nodes)
by(cases n,auto dest:WCFG_sourcelabel_less_num_nodes)
next
case (WCFG_CondElse c⇩2 n et n' b c⇩1)
note IH = ‹∀V∈Uses c⇩2 n. s V = s' V
⟹ ∀V∈Defs c⇩2 n. transfer et s V = transfer et s' V›
from ‹∀V∈Uses (if (b) c⇩1 else c⇩2) (n ⊕ #:c⇩1 + 1). s V = s' V›
have "∀V∈Uses c⇩2 n. s V = s' V"
by auto(drule Labels_CondFalse[of _ _ _ b c⇩1],erule_tac x="V" in allE,
from IH[OF this] have "∀V∈Defs c⇩2 n. transfer et s V = transfer et s' V" .
with ‹c⇩2 ⊢ n -et→ n'› show ?case
apply clarsimp
apply(erule labels.cases,auto)
apply(cases n,auto dest:label_less_num_inner_nodes)
by(cases n,auto dest:WCFG_sourcelabel_less_num_nodes)
next
case (WCFG_WhileBody c' n et n' b)
note IH = ‹∀V∈Uses c' n. s V = s' V
⟹ ∀V∈Defs c' n. transfer et s V = transfer et s' V›
from ‹∀V∈Uses (while (b) c') (n ⊕ 2). s V = s' V› have "∀V∈Uses c' n. s V = s' V"
by auto(drule Labels_WhileBody[of _ _ _ b],erule_tac x="V" in allE,auto)
from IH[OF this] have "∀V∈Defs c' n. transfer et s V = transfer et s' V" .
thus ?case
apply clarsimp
apply(erule labels.cases,auto)
by(cases n,auto dest:label_less_num_inner_nodes)
next
case (WCFG_WhileBodyExit c' n et b)
note IH = ‹∀V∈Uses c' n. s V = s' V
⟹ ∀V∈Defs c' n. transfer et s V = transfer et s' V›
from ‹∀V∈Uses (while (b) c') (n ⊕ 2). s V = s' V› have "∀V∈Uses c' n. s V = s' V"
by auto(drule Labels_WhileBody[of _ _ _ b],erule_tac x="V" in allE,auto)
from IH[OF this] have "∀V∈Defs c' n. transfer et s V = transfer et s' V" .
thus ?case
apply clarsimp
apply(erule labels.cases,auto)
by(cases n,auto dest:label_less_num_inner_nodes)
qed (fastforce elim:labels.cases)+

lemma WCFG_edge_Uses_pred_eq:
"⟦prog ⊢ n -et→ n'; ∀V ∈ Uses prog n. s V = s' V; pred et s⟧
⟹ pred et s'"
proof(induct rule:WCFG_induct)
case (WCFG_SeqFirst c⇩1 n et n' c⇩2)
note IH = ‹⟦∀V∈Uses c⇩1 n. s V = s' V; pred et s⟧ ⟹ pred et s'›
from ‹∀V∈Uses (c⇩1;; c⇩2) n. s V = s' V› have "∀V∈Uses c⇩1 n. s V = s' V"
by auto(drule Labels_Seq1[of _ _ _ c⇩2],erule_tac x="V" in allE,auto)
from IH[OF this ‹pred et s›] show ?case .
next
case (WCFG_SeqConnect c⇩1 n et c⇩2)
note IH = ‹⟦∀V∈Uses c⇩1 n. s V = s' V; pred et s⟧ ⟹ pred et s'›
from ‹∀V∈Uses (c⇩1;; c⇩2) n. s V = s' V› have "∀V∈Uses c⇩1 n. s V = s' V"
by auto(drule Labels_Seq1[of _ _ _ c⇩2],erule_tac x="V" in allE,auto)
from IH[OF this ‹pred et s›] show ?case .
next
case (WCFG_SeqSecond c⇩2 n et n' c⇩1)
note IH = ‹⟦∀V∈Uses c⇩2 n. s V = s' V; pred et s⟧ ⟹ pred et s'›
from ‹∀V∈Uses (c⇩1;; c⇩2) (n ⊕ #:c⇩1). s V = s' V›
have "∀V∈Uses c⇩2 n. s V = s' V" by(auto,blast dest:Labels_Seq2)
from IH[OF this ‹pred et s›] show ?case .
next
case (WCFG_CondTrue b c⇩1 c⇩2)
from ‹∀V∈Uses (if (b) c⇩1 else c⇩2) (_0_). s V = s' V›
have all:"∀V. labels (if (b) c⇩1 else c⇩2) 0 (if (b) c⇩1 else c⇩2) ∧
V ∈ rhs (if (b) c⇩1 else c⇩2) ⟶ (s V = s' V)"
by fastforce
obtain v' where [simp]:"v' = true" by simp
with ‹pred (λs. interpret b s = Some true)⇩√ s›
have "interpret b s = Some v'" by simp
have "labels (if (b) c⇩1 else c⇩2) 0 (if (b) c⇩1 else c⇩2)" by(rule Labels_Base)
with all have "∀V ∈ rhs_aux b. s V = s' V" by simp
with ‹interpret b s = Some v'› have "interpret b s' = Some v'"
by(rule rhs_interpret_eq)
thus ?case by simp
next
case (WCFG_CondFalse b c⇩1 c⇩2)
from ‹∀V∈Uses (if (b) c⇩1 else c⇩2) (_0_). s V = s' V›
have all:"∀V. labels (if (b) c⇩1 else c⇩2) 0 (if (b) c⇩1 else c⇩2) ∧
V ∈ rhs (if (b) c⇩1 else c⇩2) ⟶ (s V = s' V)"
by fastforce
obtain v' where [simp]:"v' = false" by simp
with ‹pred (λs. interpret b s = Some false)⇩√ s›
have "interpret b s = Some v'" by simp
have "labels (if (b) c⇩1 else c⇩2) 0 (if (b) c⇩1 else c⇩2)" by(rule Labels_Base)
with all have "∀V ∈ rhs_aux b. s V = s' V" by simp
with ‹interpret b s = Some v'› have "interpret b s' = Some v'"
by(rule rhs_interpret_eq)
thus ?case by simp
next
case (WCFG_CondThen c⇩1 n et n' b c⇩2)
note IH = ‹⟦∀V∈Uses c⇩1 n. s V = s' V; pred et s⟧ ⟹ pred et s'›
from ‹∀V∈Uses (if (b) c⇩1 else c⇩2) (n ⊕ 1). s V = s' V›
have "∀V∈Uses c⇩1 n. s V = s' V" by(auto,blast dest:Labels_CondTrue)
from IH[OF this ‹pred et s›] show ?case .
next
case (WCFG_CondElse c⇩2 n et n' b c⇩1)
note IH = ‹⟦∀V∈Uses c⇩2 n. s V = s' V; pred et s⟧ ⟹ pred et s'›
from ‹∀V∈Uses (if (b) c⇩1 else c⇩2) (n ⊕ #:c⇩1 + 1). s V = s' V›
have "∀V∈Uses c⇩2 n. s V = s' V"
by auto(drule Labels_CondFalse[of _ _ _ b c⇩1],erule_tac x="V" in allE,
from IH[OF this ‹pred et s›] show ?case .
next
case (WCFG_WhileTrue b c')
from ‹∀V∈Uses (while (b) c') (_0_). s V = s' V›
have all:"∀V. labels (while (b) c') 0 (while (b) c') ∧
V ∈ rhs (while (b) c') ⟶ (s V = s' V)"
by fastforce
obtain v' where [simp]:"v' = true" by simp
with ‹pred (λs. interpret b s = Some true)⇩√ s›
have "interpret b s = Some v'" by simp
have "labels (while (b) c') 0 (while (b) c')" by(rule Labels_Base)
with all have "∀V ∈ rhs_aux b. s V = s' V" by simp
with ‹interpret b s = Some v'› have "interpret b s' = Some v'"
by(rule rhs_interpret_eq)
thus ?case by simp
next
case (WCFG_WhileFalse b c')
from ‹∀V∈Uses (while (b) c') (_0_). s V = s' V›
have all:"∀V. labels (while (b) c') 0 (while (b) c') ∧
V ∈ rhs (while (b) c') ⟶ (s V = s' V)"
by fastforce
obtain v' where [simp]:"v' = false" by simp
with ‹pred (λs. interpret b s = Some false)⇩√ s›
have "interpret b s = Some v'" by simp
have "labels (while (b) c') 0 (while (b) c')" by(rule Labels_Base)
with all have "∀V ∈ rhs_aux b. s V = s' V" by simp
with ‹interpret b s = Some v'› have "interpret b s' = Some v'"
by(rule rhs_interpret_eq)
thus ?case by simp
next
case (WCFG_WhileBody c' n et n' b)
note IH = ‹⟦∀V∈Uses c' n. s V = s' V; pred et s⟧ ⟹ pred et s'›
from ‹∀V∈Uses (while (b) c') (n ⊕ 2). s V = s' V› have "∀V∈Uses c' n. s V = s' V"
by auto(drule Labels_WhileBody[of _ _ _ b],erule_tac x="V" in allE,auto)
from IH[OF this ‹pred et s›] show ?case .
next
case (WCFG_WhileBodyExit c' n et b)
note IH = ‹⟦∀V∈Uses c' n. s V = s' V; pred et s⟧ ⟹ pred et s'›
from ‹∀V∈Uses (while (b) c') (n ⊕ 2). s V = s' V› have "∀V∈Uses c' n. s V = s' V"
by auto(drule Labels_WhileBody[of _ _ _ b],erule_tac x="V" in allE,auto)
from IH[OF this ‹pred et s›] show ?case .
qed simp_all

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

interpretation While_CFG_wf: CFG_wf sourcenode targetnode kind
"valid_edge prog" Entry "Defs prog" "Uses prog" id
for prog
proof(unfold_locales)
show "Defs prog (_Entry_) = {} ∧ Uses prog (_Entry_) = {}"
next
fix a V s
assume "valid_edge prog a" and "V ∉ Defs prog (sourcenode a)"
obtain nx et nx' where [simp]:"a = (nx,et,nx')" by(cases a) auto
with ‹valid_edge prog a› have "prog ⊢ nx -et→ nx'" by(simp add:valid_edge_def)
with ‹V ∉ Defs prog (sourcenode a)› show "id (transfer (kind a) s) V = id s V"
by(fastforce intro:WCFG_edge_no_Defs_equal)
next
fix a fix s s'::state
assume "valid_edge prog a"
and "∀V∈Uses prog (sourcenode a). id s V = id s' V"
obtain nx et nx' where [simp]:"a = (nx,et,nx')" by(cases a) auto
with ‹valid_edge prog a› have "prog ⊢ nx -et→ nx'" by(simp add:valid_edge_def)
with ‹∀V∈Uses prog (sourcenode a). id s V = id s' V›
show "∀V∈Defs prog (sourcenode a).
id (transfer (kind a) s) V = id (transfer (kind a) s') V"
by -(drule WCFG_edge_transfer_uses_only_Uses,simp+)
next
fix a s s'
assume pred:"pred (kind a) s" and valid:"valid_edge prog a"
and all:"∀V∈Uses prog (sourcenode a). id s V = id s' V"
obtain nx et nx' where [simp]:"a = (nx,et,nx')" by(cases a) auto
with ‹valid_edge prog a› have "prog ⊢ nx -et→ nx'" by(simp add:valid_edge_def)
with ‹pred (kind a) s› ‹∀V∈Uses prog (sourcenode a). id s V = id s' V›
show "pred (kind a) s'" by -(drule WCFG_edge_Uses_pred_eq,simp+)
next
fix a a'
assume "valid_edge prog a" and "valid_edge prog a'"
and "sourcenode a = sourcenode a'" and "targetnode a ≠ targetnode a'"
thus "∃Q Q'. kind a = (Q)⇩√ ∧ kind a' = (Q')⇩√ ∧
(∀s. (Q s ⟶ ¬ Q' s) ∧ (Q' s ⟶ ¬ Q s))"
by(fastforce intro!:WCFG_deterministic simp:valid_edge_def)
qed

lemma While_CFGExit_wf_aux:"CFGExit_wf sourcenode targetnode kind
(valid_edge prog) Entry (Defs prog) (Uses prog) id Exit"
proof(unfold_locales)
show "Defs prog (_Exit_) = {} ∧ Uses prog (_Exit_) = {}"