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 (c1;;c2)            = lhs c1"
  | "lhs (if (b) c1 else c2) = {}"
  | "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 (c1;;c2)            = rhs c1"
  | "rhs (if (b) c1 else c2) = 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 "∃v1 v2. interpret b1 s = Some v1 ∧ interpret b2 s = Some v2 ∧
                binop bop v1 v2 = Some v'"
    apply(cases "interpret b1 s",simp)
    apply(cases "interpret b2 s",simp)
    by(case_tac "binop bop a aa",simp+)
  then obtain v1 v2 where "interpret b1 s = Some v1"
    and "interpret b2 s = Some v2" and "binop bop v1 v2 = 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 v1› this] have "interpret b1 s' = Some v1" .
  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 v2› this] have "interpret b2 s' = Some v2" .
  with ‹interpret b1 s' = Some v1› ‹binop bop v1 v2 = 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 c1 n et n' c2)
  note IH = ‹V ∉ Defs c1 n ⟹ transfer et s V = s V›
  have "V ∉ Defs c1 n"
  proof
    assume "V ∈ Defs c1 n"
    then obtain c l where [simp]:"n = (_ l _)" and "labels c1 l c"
      and "V ∈ lhs c" by fastforce
    from ‹labels c1 l c› have "labels (c1;;c2) l (c;;c2)"
      by(fastforce intro:Labels_Seq1)
    from ‹V ∈ lhs c› have "V ∈ lhs (c;;c2)" by simp
    with ‹labels (c1;;c2) l (c;;c2)› have "V ∈ Defs (c1;;c2) n" by fastforce
    with ‹V ∉ Defs (c1;;c2) n› show False by fastforce
  qed
  from IH[OF this] show ?case .
next
  case (WCFG_SeqConnect c1 n et c2)
  note IH = ‹V ∉ Defs c1 n ⟹ transfer et s V = s V›
  have "V ∉ Defs c1 n"
  proof
    assume "V ∈ Defs c1 n"
    then obtain c l where [simp]:"n = (_ l _)" and "labels c1 l c"
      and "V ∈ lhs c" by fastforce
    from ‹labels c1 l c› have "labels (c1;;c2) l (c;;c2)"
      by(fastforce intro:Labels_Seq1)
    from ‹V ∈ lhs c› have "V ∈ lhs (c;;c2)" by simp
    with ‹labels (c1;;c2) l (c;;c2)› have "V ∈ Defs (c1;;c2) n" by fastforce
    with ‹V ∉ Defs (c1;;c2) n› show False by fastforce
  qed
  from IH[OF this] show ?case .
next
  case (WCFG_SeqSecond c2 n et n' c1)
  note IH = ‹V ∉ Defs c2 n ⟹ transfer et s V = s V›
  have "V ∉ Defs c2 n"
  proof
    assume "V ∈ Defs c2 n"
    then obtain c l where [simp]:"n = (_ l _)" and "labels c2 l c"
      and "V ∈ lhs c" by fastforce
    from ‹labels c2 l c› have "labels (c1;;c2) (l + #:c1) c"
      by(fastforce intro:Labels_Seq2)
    with ‹V ∈ lhs c› have "V ∈ Defs (c1;;c2) (n ⊕ #:c1)" by fastforce
    with ‹V ∉ Defs (c1;;c2) (n ⊕ #:c1)› show False by fastforce
  qed
  from IH[OF this] show ?case .
next
  case (WCFG_CondThen c1 n et n' b c2)
  note IH = ‹V ∉ Defs c1 n ⟹ transfer et s V = s V›
  have "V ∉ Defs c1 n"
  proof
    assume "V ∈ Defs c1 n"
    then obtain c l where [simp]:"n = (_ l _)" and "labels c1 l c"
      and "V ∈ lhs c" by fastforce
    from ‹labels c1 l c› have "labels (if (b) c1 else c2) (l + 1) c"
      by(fastforce intro:Labels_CondTrue)
    with ‹V ∈ lhs c› have "V ∈ Defs (if (b) c1 else c2) (n ⊕ 1)" by fastforce
    with ‹V ∉ Defs (if (b) c1 else c2) (n ⊕ 1)› show False by fastforce
  qed
  from IH[OF this] show ?case .
next
  case (WCFG_CondElse c2 n et n' b c1)
  note IH = ‹V ∉ Defs c2 n ⟹ transfer et s V = s V›
  have "V ∉ Defs c2 n"
  proof
    assume "V ∈ Defs c2 n"
    then obtain c l where [simp]:"n = (_ l _)" and "labels c2 l c"
      and "V ∈ lhs c" by fastforce
    from ‹labels c2 l c› have "labels (if (b) c1 else c2) (l + #:c1 + 1) c"
      by(fastforce intro:Labels_CondFalse)
    with ‹V ∈ lhs c› have "V ∈ Defs (if (b) c1 else c2) (n ⊕ #:c1 + 1)"
      by(fastforce simp:add.commute add.left_commute)
    with ‹V ∉ Defs (if (b) c1 else c2) (n ⊕ #:c1 + 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 c1 n et n' c2)
  note IH = ‹∀V∈Uses c1 n. s V = s' V 
    ⟹ ∀V∈Defs c1 n. transfer et s V = transfer et s' V›
  from ‹∀V∈Uses (c1;;c2) n. s V = s' V› have "∀V∈Uses c1 n. s V = s' V"
    by auto(drule Labels_Seq1[of _ _ _ c2],erule_tac x="V" in allE,auto)
  from IH[OF this] have "∀V∈Defs c1 n. transfer et s V = transfer et s' V" .
  with ‹c1 ⊢ 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 c1 n et c2)
  note IH = ‹∀V∈Uses c1 n. s V = s' V 
    ⟹ ∀V∈Defs c1 n. transfer et s V = transfer et s' V›
  from ‹∀V∈Uses (c1;;c2) n. s V = s' V› have "∀V∈Uses c1 n. s V = s' V"
    by auto(drule Labels_Seq1[of _ _ _ c2],erule_tac x="V" in allE,auto)
  from IH[OF this] have "∀V∈Defs c1 n. transfer et s V = transfer et s' V" .
  with ‹c1 ⊢ 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 c2 n et n' c1)
  note IH = ‹∀V∈Uses c2 n. s V = s' V 
    ⟹ ∀V∈Defs c2 n. transfer et s V = transfer et s' V›
  from ‹∀V∈Uses (c1;;c2) (n ⊕ #:c1). s V = s' V› have "∀V∈Uses c2 n. s V = s' V"
    by(auto,blast dest:Labels_Seq2)
  from IH[OF this] have "∀V∈Defs c2 n. transfer et s V = transfer et s' V" .
  with num_inner_nodes_gr_0[of "c1"] show ?case
    apply clarsimp
    apply(erule labels.cases,auto)
    by(cases n,auto dest:label_less_num_inner_nodes)+
next
  case (WCFG_CondThen c1 n et n' b c2)
  note IH = ‹∀V∈Uses c1 n. s V = s' V 
    ⟹ ∀V∈Defs c1 n. transfer et s V = transfer et s' V›
  from ‹∀V∈Uses (if (b) c1 else c2) (n ⊕ 1). s V = s' V› 
  have "∀V∈Uses c1 n. s V = s' V" by(auto,blast dest:Labels_CondTrue)
  from IH[OF this] have "∀V∈Defs c1 n. transfer et s V = transfer et s' V" .
  with ‹c1 ⊢ 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 c2 n et n' b c1)
  note IH = ‹∀V∈Uses c2 n. s V = s' V 
    ⟹ ∀V∈Defs c2 n. transfer et s V = transfer et s' V›
  from ‹∀V∈Uses (if (b) c1 else c2) (n ⊕ #:c1 + 1). s V = s' V› 
  have "∀V∈Uses c2 n. s V = s' V"
    by auto(drule Labels_CondFalse[of _ _ _ b c1],erule_tac x="V" in allE,
       auto simp:add.assoc)
  from IH[OF this] have "∀V∈Defs c2 n. transfer et s V = transfer et s' V" .
  with ‹c2 ⊢ 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 c1 n et n' c2)
  note IH = ‹⟦∀V∈Uses c1 n. s V = s' V; pred et s⟧ ⟹ pred et s'›
  from ‹∀V∈Uses (c1;; c2) n. s V = s' V› have "∀V∈Uses c1 n. s V = s' V"
    by auto(drule Labels_Seq1[of _ _ _ c2],erule_tac x="V" in allE,auto)
  from IH[OF this ‹pred et s›] show ?case .
next
  case (WCFG_SeqConnect c1 n et c2)
  note IH = ‹⟦∀V∈Uses c1 n. s V = s' V; pred et s⟧ ⟹ pred et s'›
  from ‹∀V∈Uses (c1;; c2) n. s V = s' V› have "∀V∈Uses c1 n. s V = s' V"
    by auto(drule Labels_Seq1[of _ _ _ c2],erule_tac x="V" in allE,auto)
  from IH[OF this ‹pred et s›] show ?case .
next
  case (WCFG_SeqSecond c2 n et n' c1)
  note IH = ‹⟦∀V∈Uses c2 n. s V = s' V; pred et s⟧ ⟹ pred et s'›
  from ‹∀V∈Uses (c1;; c2) (n ⊕ #:c1). s V = s' V›
  have "∀V∈Uses c2 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 c1 c2)
  from ‹∀V∈Uses (if (b) c1 else c2) (_0_). s V = s' V› 
  have all:"∀V. labels (if (b) c1 else c2) 0 (if (b) c1 else c2) ∧ 
            V ∈ rhs (if (b) c1 else c2) ⟶ (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) c1 else c2) 0 (if (b) c1 else c2)" 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 c1 c2)
  from ‹∀V∈Uses (if (b) c1 else c2) (_0_). s V = s' V›
  have all:"∀V. labels (if (b) c1 else c2) 0 (if (b) c1 else c2) ∧ 
              V ∈ rhs (if (b) c1 else c2) ⟶ (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) c1 else c2) 0 (if (b) c1 else c2)" 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 c1 n et n' b c2)
  note IH = ‹⟦∀V∈Uses c1 n. s V = s' V; pred et s⟧ ⟹ pred et s'›
  from ‹∀V∈Uses (if (b) c1 else c2) (n ⊕ 1). s V = s' V›
  have "∀V∈Uses c1 n. s V = s' V" by(auto,blast dest:Labels_CondTrue)
  from IH[OF this ‹pred et s›] show ?case .
next
  case (WCFG_CondElse c2 n et n' b c1)
  note IH = ‹⟦∀V∈Uses c2 n. s V = s' V; pred et s⟧ ⟹ pred et s'›
  from ‹∀V∈Uses (if (b) c1 else c2) (n ⊕ #:c1 + 1). s V = s' V›
  have "∀V∈Uses c2 n. s V = s' V"
    by auto(drule Labels_CondFalse[of _ _ _ b c1],erule_tac x="V" in allE,
       auto simp:add.assoc)
  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_) = {}"
    by(simp add:Defs.simps Uses.simps)
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_) = {}"
    by(simp add:Defs.simps Uses.simps)
qed

interpretation While_CFGExit_wf: CFGExit_wf sourcenode targetnode kind 
  "valid_edge prog" Entry "Defs prog" "Uses prog" id Exit
  for prog
by(rule While_CFGExit_wf_aux)


end