Quelle  SSA_CFG.thy

(*  Title:      SSA_CFG.thy
    Author:     Sebastian Ullrich, Denis Lohner
*)

theory SSA_CFG
imports Graph_path "HOL-Library.Sublist"
begin

subsection ‹CFG›

locale CFG_base = graph_Entry_base αe αn invar inEdges' Entry
for
  αe :: "'g ==> ('node::linorder × 'edgeD × 'node) set" and
  αn :: "'g ==> 'node list" and
  invar :: "'g ==> bool" and
  inEdges' :: "'g ==> 'node ==> ('node × 'edgeD) list" and
  Entry :: "'g ==> 'node" +
fixes "defs" :: "'g ==> 'node ==> 'var::linorder set"
fixes "uses" :: "'g ==> 'node ==> 'var set"
begin
  definition "vars g ≡ fold (∪) (map (uses g) (αn g)) {}"
  definition defAss' :: "'g ==> 'node ==> 'var ==> bool" where
    "defAss' g m v ⟷ (∀ns. g ⊨ Entry g-ns→m ⟶ (∃n ∈ set ns. v ∈ defs g n))"

  definition defAss'Uses :: "'g ==> bool" where
    "defAss'Uses g ≡ ∀m ∈ set (αn g). ∀v ∈ uses g m. defAss' g m v"
end

locale CFG = CFG_base αe αn invar inEdges' Entry "defs" "uses"
+ graph_Entry αe αn invar inEdges' Entry
for
  αe :: "'g ==> ('node::linorder × 'edgeD × 'node) set" and
  αn :: "'g ==> 'node list" and
  invar :: "'g ==> bool" and
  inEdges' :: "'g ==> 'node ==> ('node × 'edgeD) list" and
  Entry :: "'g ==> 'node" and
  "defs" :: "'g ==> 'node ==> 'var::linorder set" and
  "uses" :: "'g ==> 'node ==> 'var set" +
assumes defs_uses_disjoint: "n ∈ set (αn g) ==> defs g n ∩ uses g n = {}"
assumes defs_finite[simp]: "finite (defs g n)"
assumes uses_in_αn: "v ∈ uses g n ==> n ∈ set (αn g)"
assumes uses_finite[simp, intro!]: "finite (uses g n)"
assumes invar[intro!]: "invar g"
begin
  lemma vars_finite[simp]: "finite (vars g)"
  by (auto simp:vars_def)

  lemma Entry_no_predecessor[simp]: "predecessors g (Entry g) = []"
  using Entry_unreachable
  by (auto simp:predecessors_def)

  lemma uses_in_vars[elim, simp]: "v ∈ uses g n ==> v ∈ vars g"
  by (auto simp add:vars_def uses_in_αn intro!: fold_union_elemI)

  lemma varsE:
    assumes "v ∈ vars g"
    obtains n where "n ∈ set (αn g)" "v ∈ uses g n"
  using assms by (auto simp:vars_def elim!:fold_union_elem)

  lemma defs_uses_disjoint'[simp]: "n ∈ set (αn g) ==> v ∈ defs g n ==> v ∈ uses g n ==> False"
  using defs_uses_disjoint by auto
end

context CFG
begin
  lemma defAss'E:
    assumes "defAss' g m v" "g ⊨ Entry g-ns→m"
    obtains n where "n ∈ set ns" "v ∈ defs g n"
  using assms unfolding defAss'_def by auto

  lemmas defAss'I = defAss'_def[THEN iffD2, rule_format]

  lemma defAss'_extend:
    assumes "defAss' g m v"
    assumes "g ⊨ n-ns→m" "∀n ∈ set (tl ns). v ∉ defs g n"
    shows "defAss' g n v"
  unfolding defAss'_def proof (rule allI, rule impI)
    fix ns'
    assume "g ⊨ Entry g-ns'→n"
    with assms(2) have "g ⊨ Entry g-ns'@tl ns→m" by auto
    with assms(1) obtain n' where n': "n' ∈ set (ns'@tl ns)" "v ∈ defs g n'" by -(erule defAss'E)
    with assms(3) have "n' ∉ set (tl ns)" by auto
    with n' show "∃n ∈ set ns'. v ∈ defs g n" by auto
  qed
end

text ‹A CFG is well-formed if it satisfies definite assignment.›

locale CFG_wf = CFG αe αn invar inEdges' Entry "defs" "uses"
for
  αe :: "'g ==> ('node::linorder × 'edgeD × 'node) set" and
  αn :: "'g ==> 'node list" and
  invar :: "'g ==> bool" and
  inEdges' :: "'g ==> 'node ==> ('node × 'edgeD) list" and
  Entry::"'g ==> 'node" and
  "defs" :: "'g ==> 'node ==> 'var::linorder set" and
  "uses" :: "'g ==> 'node ==> 'var set" +
assumes def_ass_uses: "∀m ∈ set (αn g). ∀v ∈ uses g m. defAss' g m v"

subsection ‹SSA CFG›

type_synonym ('node, 'val) phis = "'node × 'val ⇀ 'val list"

declare in_set_zipE[elim]
declare zip_same[simp]

locale CFG_SSA_base = CFG_base αe αn invar inEdges' Entry "defs" "uses"
for
  αe :: "'g ==> ('node::linorder × 'edgeD × 'node) set" and
  αn :: "'g ==> 'node list" and
  invar :: "'g ==> bool" and
  inEdges' :: "'g ==> 'node ==> ('node × 'edgeD) list" and
  Entry::"'g ==> 'node" and
  "defs" :: "'g ==> 'node ==> 'val::linorder set" and
  "uses" :: "'g ==> 'node ==> 'val set" +
fixes phis :: "'g ==> ('node, 'val) phis"
begin
  definition "phiDefs g n ≡ {v. (n,v) ∈ dom (phis g)}"
  definition[code]: "allDefs g n ≡ defs g n ∪ phiDefs g n"

  definition[code]: "phiUses g n ≡
    ∪n' ∈ set (successors g n). ∪v' ∈ phiDefs g n'. snd ` Set.filter (λ(n'',v). n'' = n) (set (zip (predecessors g n') (the (phis g (n',v')))))"
  definition[code]: "allUses g n ≡ uses g n ∪ phiUses g n"
  definition[code]: "allVars g ≡ ∪n ∈ set (αn g). allDefs g n ∪ allUses g n"

  definition defAss :: "'g ==> 'node ==> 'val ==> bool" where
    "defAss g m v ⟷ (∀ns. g ⊨ Entry g-ns→m ⟶ (∃n ∈ set ns. v ∈ allDefs g n))"

  lemmas CFG_SSA_defs = phiDefs_def allDefs_def phiUses_def allUses_def allVars_def defAss_def
end

locale CFG_SSA = CFG αe αn invar inEdges' Entry "defs" "uses" + CFG_SSA_base αe αn invar inEdges' Entry "defs" "uses" phis
for
  αe :: "'g ==> ('node::linorder × 'edgeD × 'node) set" and
  αn :: "'g ==> 'node list" and
  invar :: "'g ==> bool" and
  inEdges' :: "'g ==> 'node ==> ('node × 'edgeD) list" and
  Entry::"'g ==> 'node" and
  "defs" :: "'g ==> 'node ==> 'val::linorder set" and
  "uses" :: "'g ==> 'node ==> 'val set" and
   phis :: "'g ==> ('node, 'val) phis" +
assumes phis_finite: "finite (dom (phis g))"
assumes phis_in_αn: "phis g (n,v) = Some vs ==> n ∈ set (αn g)"
assumes phis_wf:
  "phis g (n,v) = Some args ==> length (predecessors g n) = length args"
assumes simpleDefs_phiDefs_disjoint:             
  "n ∈ set (αn g) ==> defs g n ∩ phiDefs g n = {}"
assumes allDefs_disjoint:
  "[n ∈ set (αn g); m ∈ set (αn g); n ≠ m] ==> allDefs g n ∩ allDefs g m = {}"
begin
  lemma phis_disj:
    assumes "phis g (n,v) = Some vs"
    and "phis g (n',v) = Some vs'"
    shows "n = n'" and "vs = vs'"
  proof -
    from assms have "n ∈ set (αn g)" and "n' ∈ set (αn g)"
      by (auto dest: phis_in_αn)
    from allDefs_disjoint [OF this] assms show "n = n'"
      by (auto simp: allDefs_def phiDefs_def)
    with assms show "vs = vs'" by simp
  qed

  lemma allDefs_disjoint': "[n ∈ set (αn g); m ∈ set (αn g); v ∈ allDefs g n; v ∈ allDefs g m] ==> n = m"
  using allDefs_disjoint by auto

  lemma phiUsesI:
    assumes "n' ∈ set (αn g)" "phis g (n',v') = Some vs" "(n,v) ∈ set (zip (predecessors g n') vs)"
    shows "v ∈ phiUses g n"
  proof-
    from assms(3) have "n ∈ set (predecessors g n')" by auto
    hence 1: "n' ∈ set (successors g n)" using assms(1) by simp
    from assms(2) have 2: "v' ∈ phiDefs g n'" by (auto simp add:phiDefs_def)
    from assms(2) have 3: "the (phis g (n',v')) = vs" by simp
    with assms(3) show ?thesis
      apply (simp only: phiUses_def)
      using 1 apply (rule UN_I)
      using 2 apply (rule UN_I)
      apply auto
      done
  qed

  lemma phiUsesE:
    assumes "v ∈ phiUses g n"
    obtains  n' v' vs where "n' ∈ set (successors g n)" "(n,v) ∈ set (zip (predecessors g n') vs)" "phis g (n', v') = Some vs"
  proof-
    from assms(1) obtain n' v' where "n'∈set (successors g n)" "v'∈phiDefs g n'"
      "v ∈ snd ` Set.filter (λ(n'', v). n'' = n) (set (zip (predecessors g n') (the (phis g (n', v')))))" by (auto simp:phiUses_def)
    thus ?thesis by - (rule that[of n' "the (phis g (n',v'))" v'], auto simp:phiDefs_def)
  qed

  lemma defs_in_allDefs[simp]: "v ∈ defs g n ==> v ∈ allDefs g n" by (simp add:allDefs_def)
  lemma phiDefs_in_allDefs[simp, elim]: "v ∈ phiDefs g n ==> v ∈ allDefs g n" by (simp add:allDefs_def)
  lemma uses_in_allUses[simp]: "v ∈ uses g n ==> v ∈ allUses g n" by (simp add:allUses_def)
  lemma phiUses_in_allUses[simp]: "v ∈ phiUses g n ==> v ∈ allUses g n" by (simp add:allUses_def)
  lemma allDefs_in_allVars[simp, intro]: "[v ∈ allDefs g n; n ∈ set (αn g)] ==> v ∈ allVars g" by (auto simp:allVars_def)
  lemma allUses_in_allVars[simp, intro]: "[v ∈ allUses g n; n ∈ set (αn g)] ==> v ∈ allVars g" by (auto simp:allVars_def)

  lemma phiDefs_finite[simp]: "finite (phiDefs g n)"
  unfolding phiDefs_def
  proof (rule finite_surj[where f=snd], rule phis_finite[where g=g])
    have "∧x y. phis g (n,x) = Some y ==> x ∈ snd ` dom (phis g)" by (metis domI imageI snd_conv)
    thus "{v. (n, v) ∈ dom (phis g)} ⊆ snd ` dom (phis g)" by auto
  qed

  lemma phiUses_finite[simp]:
    assumes "n ∈ set (αn g)"
    shows "finite (phiUses g n)"
    by (auto simp: phiUses_def)

  lemma allDefs_finite[simp]: "n ∈ set (αn g) ==> finite (allDefs g n)" by (auto simp add:allDefs_def)
  lemma allUses_finite[simp]: "n ∈ set (αn g) ==> finite (allUses g n)" by (auto simp add:allUses_def)
  lemma allVars_finite[simp]: "finite (allVars g)" by (auto simp add:allVars_def)

  lemmas defAssI = defAss_def[THEN iffD2, rule_format]
  lemmas defAssD = defAss_def[THEN iffD1, rule_format]

  lemma defAss_extend:
    assumes "defAss g m v"
    assumes "g ⊨ n-ns→m" "∀n ∈ set (tl ns). v ∉ allDefs g n"
    shows "defAss g n v"
  unfolding defAss_def proof (rule allI, rule impI)
    fix ns'
    assume "g ⊨ Entry g-ns'→n"
    with assms(2) have "g ⊨ Entry g-ns'@tl ns→m" by auto
    with assms(1) obtain n' where n': "n' ∈ set (ns'@tl ns)" "v ∈ allDefs g n'" by (auto dest:defAssD)
    with assms(3) have "n' ∉ set (tl ns)" by auto
    with n' show "∃n ∈ set ns'. v ∈ allDefs g n" by auto
  qed

  lemma defAss_dominating:
    assumes[simp]: "n ∈ set (αn g)"
    shows "defAss g n v ⟷ (∃m ∈ set (αn g). dominates g m n ∧ v ∈ allDefs g m)"
  proof
    assume asm: "defAss g n v"
    obtain ns where ns: "g ⊨ Entry g-ns→n" by (atomize, auto)
    from defAssD[OF asm this] obtain m where m: "m ∈ set ns" "v ∈ allDefs g m" by auto
    have "dominates g m n"
    proof
      fix ns'
      assume ns': "g ⊨ Entry g-ns'→n"
      from defAssD[OF asm this] obtain m' where m': "m' ∈ set ns'" "v ∈ allDefs g m'" by auto
      with m ns ns' have "m' = m" by - (rule allDefs_disjoint', auto)
      with m' show "m ∈ set ns'" by simp
    qed simp
    with m ns show "∃m∈set (αn g). dominates g m n ∧ v ∈ allDefs g m" by auto
  next
    assume "∃m ∈ set (αn g). dominates g m n ∧ v ∈ allDefs g m"
    then obtain m where[simp]: "m ∈ set (αn g)" and m: "dominates g m n" "v ∈ allDefs g m" by auto
    show "defAss g n v"
    proof (rule defAssI)
      fix ns
      assume "g ⊨ Entry g-ns→n"
      with m(1) have "m ∈ set ns" by - (rule dominates_mid, auto)
      with m(2) show "∃n∈set ns. v ∈ allDefs g n" by auto
    qed
  qed
end

locale CFG_SSA_wf_base = CFG_SSA_base αe αn invar inEdges' Entry "defs" "uses" phis
for
  αe :: "'g ==> ('node::linorder × 'edgeD × 'node) set" and
  αn :: "'g ==> 'node list" and
  invar :: "'g ==> bool" and
  inEdges' :: "'g ==> 'node ==> ('node × 'edgeD) list" and
  Entry::"'g ==> 'node" and
  "defs" :: "'g ==> 'node ==> 'val::linorder set" and
  "uses" :: "'g ==> 'node ==> 'val set" and
  phis :: "'g ==> ('node, 'val) phis"
begin
  text ‹Using the SSA properties, we can map every value to its unique defining node and
 remove the @{typ 'node} parameter of the @{term phis} map.›

  definition defNode :: "'g ==> 'val ==> 'node" where
    defNode_code [code]: "defNode g v ≡ hd [n ← αn g. v ∈ allDefs g n]"

  abbreviation "def_dominates g v' v ≡ dominates g (defNode g v') (defNode g v)"
  abbreviation "strict_def_dom g v' v ≡ defNode g v' ≠ defNode g v ∧ def_dominates g v' v"

  definition "phi g v = phis g (defNode g v,v)"
  definition[simp]: "phiArg g v v' ≡ ∃vs. phi g v = Some vs ∧ v' ∈ set vs"

  definition[code]: "isTrivialPhi g v v' ⟷ v' ≠ v ∧
    (case phi g v of
      Some vs ==> set vs = {v,v'} ∨ set vs = {v'}
    | None ==> False)"
  definition[code]: "trivial g v ≡ ∃v' ∈ allVars g. isTrivialPhi g v v'"
  definition[code]: "redundant g ≡ ∃v ∈ allVars g. trivial g v"

  definition "defAssUses g ≡ ∀n ∈ set (αn g). ∀v ∈ allUses g n. defAss g n v"

  text ‹'liveness' of an SSA value is defined inductively starting from simple uses so that
 a circle of \pf s is not considered live.›

  declare [[inductive_internals]]
  inductive liveVal :: "'g ==> 'val ==> bool"
    for g :: 'g
  where
    liveSimple: "[n ∈ set (αn g); val ∈ uses g n] ==> liveVal g val"
  | livePhi: "[liveVal g v; phiArg g v v'] ==> liveVal g v'"

  definition "pruned g = (∀n ∈ set (αn g). ∀val. val ∈ phiDefs g n ⟶ liveVal g val)"

  lemmas "CFG_SSA_wf_defs" = CFG_SSA_defs defNode_code phi_def isTrivialPhi_def trivial_def redundant_def liveVal_def pruned_def
end

locale CFG_SSA_wf = CFG_SSA αe αn invar inEdges' Entry "defs" "uses" phis + CFG_SSA_wf_base αe αn invar inEdges' Entry "defs" "uses" phis
for
  αe :: "'g ==> ('node::linorder × 'edgeD × 'node) set" and
  αn :: "'g ==> 'node list" and
  invar :: "'g ==> bool" and
  inEdges' :: "'g ==> 'node ==> ('node × 'edgeD) list" and
  Entry::"'g ==> 'node" and
  "defs" :: "'g ==> 'node ==> 'val::linorder set" and
  "uses" :: "'g ==> 'node ==> 'val set" and
  phis :: "'g ==> ('node, 'val) phis" +
  assumes allUses_def_ass: "[v ∈ allUses g n; n ∈ set (αn g)] ==> defAss g n v"
  assumes Entry_no_phis[simp]: "phis g (Entry g,v) = None"
begin
  lemma allVars_in_allDefs: "v ∈ allVars g ==> ∃n ∈ set (αn g). v ∈ allDefs g n"
    unfolding allVars_def
  apply auto
  apply (drule(1) allUses_def_ass)
  apply (clarsimp simp: defAss_def)
  apply (drule Entry_reaches)
   apply auto[1]
  by fastforce

  lemma phiDefs_Entry_empty[simp]: "phiDefs g (Entry g) = {}"
  by (auto simp: phiDefs_def)

  lemma phi_Entry_empty[simp]: "defNode g v = Entry g ==> phi g v = None"
    by (simp add:phi_def)

  lemma defNode_ex1:
    assumes "v ∈ allVars g"
    shows "∃!n. n ∈ set (αn g) ∧ v ∈ allDefs g n"
  proof (rule ex_ex1I)
    show "∃n. n ∈ set (αn g) ∧ v ∈ allDefs g n"
    proof-
      from assms(1) obtain n where n: "n ∈ set (αn g)" "v ∈ allDefs g n ∨ v ∈ allUses g n" by (auto simp:allVars_def)
      thus ?thesis
      proof (cases "v ∈ allUses g n")
        case True
        from n(1) obtain ns where ns: "g ⊨ Entry g-ns→n" by (atomize_elim, rule Entry_reaches, auto)
        with allUses_def_ass[OF True n(1)] obtain m where m: "m ∈ set ns" "v ∈ allDefs g m" by - (drule defAssD, auto)
        from ns this(1) have "m ∈ set (αn g)" by (rule path2_in_αn)
        with n(1) m show ?thesis by auto
      qed auto
    qed
    show "∧n m. n ∈ set (αn g) ∧ v ∈ allDefs g n ==> m ∈ set (αn g) ∧ v ∈ allDefs g m ==> n = m" using allDefs_disjoint by auto
  qed

  lemma defNode_def: "v ∈ allVars g ==> defNode g v = (THE n. n ∈ set (αn g) ∧ v ∈ allDefs g n)"
  unfolding defNode_code by (rule the1_list[symmetric], rule defNode_ex1)

  lemma defNode[simp]:
    assumes "v ∈ allVars g"
    shows  "(defNode g v) ∈ set (αn g)" "v ∈ allDefs g (defNode g v)"
  apply (atomize(full))
  unfolding defNode_def[OF assms] using assms
  by - (rule theI', rule defNode_ex1)

  lemma defNode_eq[intro]:
    assumes "n ∈ set (αn g)" "v ∈ allDefs g n"
    shows "defNode g v = n"
  apply (subst defNode_def, rule allDefs_in_allVars[OF assms(2) assms(1)])
  by (rule the1_equality, rule defNode_ex1, rule allDefs_in_allVars[where n=n], simp_all add:assms)

  lemma defNode_cases[consumes 1]:
    assumes "v ∈ allVars g"
    obtains (simpleDef) "v ∈ defs g (defNode g v)"
          | (phi)       "phi g v ≠ None"
  proof (cases "v ∈ defs g (defNode g v)")
    case True
    thus thesis by (rule simpleDef)
  next
    case False
    with assms[THEN defNode(2)] show thesis
      by - (rule phi, auto simp: allDefs_def phiDefs_def phi_def)
  qed

  lemma phi_phiDefs[simp]: "phi g v = Some vs ==> v ∈ phiDefs g (defNode g v)" by (auto simp:phiDefs_def phi_def)

  lemma simpleDef_not_phi:
    assumes "n ∈ set (αn g)" "v ∈ defs g n"
    shows "phi g v = None"
  proof-
    from assms have "defNode g v = n" by auto
    with assms show ?thesis using simpleDefs_phiDefs_disjoint by (auto simp: phi_def phiDefs_def)
  qed

  lemma phi_wf: "phi g v = Some vs ==> length (predecessors g (defNode g v)) = length vs"
  by (rule phis_wf) (simp add:phi_def)

  lemma phi_finite: "finite (dom (phi g))"
  proof-
    let ?f = "λv. (defNode g v,v)"
    have "phi g = phis g ∘ ?f" by (auto simp add:phi_def)
    moreover have "inj ?f" by (auto intro:injI)
    hence "finite (dom (phis g ∘ ?f))" by - (rule finite_dom_comp, auto simp add:phis_finite inj_on_def)
    ultimately show ?thesis by simp
  qed

  lemma phiUses_exI:
    assumes "m ∈ set (predecessors g n)" "phis g (n,v) = Some vs" "n ∈ set (αn g)"
    obtains v' where "v' ∈ phiUses g m" "v' ∈ set vs"
  proof-
    from assms(1) obtain i where i: "m = predecessors g n ! i" "i < length (predecessors g n)" by (metis in_set_conv_nth)
    with assms(2) phis_wf have[simp]: "i < length vs" by (auto simp add:phi_def)
    from i assms(2,3) have "vs ! i ∈ phiUses g m" by - (rule phiUsesI, auto simp add:phiUses_def phi_def set_zip)
    thus thesis by (rule that) (auto simp add:i(2) phis_wf)
  qed

  lemma phiArg_exI:
    assumes "m ∈ set (predecessors g (defNode g v))" "phi g v ≠ None" and[simp]: "v ∈ allVars g"
    obtains v' where "v' ∈ phiUses g m" "phiArg g v v'"
  proof-
    from assms(2) obtain vs where "phi g v = Some vs" by auto
    with assms(1) show thesis
      by - (rule phiUses_exI, auto intro!:that simp: phi_def)
  qed

  lemma phiUses_exI':
    assumes "phiArg g p q" and[simp]: "p ∈ allVars g"
    obtains m where "q ∈ phiUses g m" "m ∈ set (predecessors g (defNode g p))"
  proof-
    let ?n = "defNode g p"
    from assms(1) obtain i vs where vs: "phi g p = Some vs" and i: "q = vs ! i" "i < length vs" by (metis in_set_conv_nth phiArg_def)
    with phis_wf have[simp]: "i < length (predecessors g ?n)" by (auto simp add:phi_def)
    from vs i have "q ∈ phiUses g (predecessors g ?n ! i)" by - (rule phiUsesI, auto simp add:phiUses_def phi_def set_zip)
    thus thesis by (rule that) (auto simp add:i(2) phis_wf)
  qed

  lemma phiArg_in_allVars[simp]:
    assumes "phiArg g v v'"
    shows "v' ∈ allVars g"
  proof-
    let ?n = "defNode g v"
    from assms(1) obtain vs where vs: "phi g v = Some vs" "v' ∈ set vs" by auto
    then obtain m where m: "(m,v') ∈ set (zip (predecessors g ?n) vs)" by - (rule set_zip_leftI, rule phi_wf)
    from vs(1) have n: "?n ∈ set (αn g)" by (simp add: phi_def phis_in_αn)
    with m have[simp]: "m ∈ set (αn g)" by auto
    from n m vs have "v' ∈ phiUses g m" by - (rule phiUsesI, simp_all add:phi_def)
    thus ?thesis by - (rule allUses_in_allVars, auto simp:allUses_def)
  qed

  lemma defAss_defNode:
    assumes "defAss g m v" "v ∈ allVars g" "g ⊨ Entry g-ns→m"
    shows "defNode g v ∈ set ns"
  proof-
    from assms obtain n where n: "n ∈ set ns" "v ∈ allDefs g n" by (auto simp:defAss_def)
    with assms(3) have "n = defNode g v" by - (rule defNode_eq[symmetric], auto)
    with n show "defNode g v ∈ set ns" by (simp add:defAss_def)
  qed

  lemma defUse_path_ex:
    assumes "v ∈ allUses g m" "m ∈ set (αn g)"
    obtains ns where "g ⊨ defNode g v-ns→m" "EntryPath g ns"
  proof-
    from assms have "defAss g m v" by - (rule allUses_def_ass, auto)
    moreover from assms obtain ns where ns: "g ⊨ Entry g-ns→m" "EntryPath g ns"
      by - (atomize_elim, rule Entry_reachesE, auto)
    ultimately have "defNode g v ∈ set ns" using assms(1)
      by - (rule defAss_defNode, auto)
    with ns(1) obtain ns' where "g ⊨ defNode g v-ns'→m" "suffix ns' ns"
      by (rule path2_split_ex', auto simp: Sublist.suffix_def)
    thus thesis using ns(2)
      by - (rule that, assumption, rule EntryPath_suffix, auto)
  qed

  lemma defUse_path_dominated:
    assumes "g ⊨ defNode g v-ns→n" "defNode g v ∉ set (tl ns)" "v ∈ allUses g n" "n' ∈ set ns"
    shows "dominates g (defNode g v) n'"
  proof (rule dominatesI)
    fix es
    assume asm: "g ⊨ Entry g-es→n'"
    from assms(1,4) obtain ns' where ns': "g ⊨ n'-ns'→n" "suffix ns' ns"
      by - (rule path2_split_ex, auto simp: Sublist.suffix_def)
    from assms have "defAss g n v" by - (rule allUses_def_ass, auto)
    with asm ns'(1) assms(3) have "defNode g v ∈ set (es@tl ns')" by - (rule defAss_defNode, auto)
    with suffix_tl_subset[OF ns'(2)] assms(2) show "defNode g v ∈ set es" by auto
  next
    show "n' ∈ set (αn g)" using assms(1,4) by auto
  qed

  lemma allUses_dominated:
    assumes "v ∈ allUses g n" "n ∈ set (αn g)"
    shows "dominates g (defNode g v) n"
  proof-
    from assms obtain ns where "g ⊨ defNode g v-ns→n" "defNode g v ∉ set (tl ns)"
      by - (rule defUse_path_ex, auto elim: simple_path2)
    with assms(1) show ?thesis by - (rule defUse_path_dominated, auto)
  qed

  lemma phiArg_path_ex':
    assumes "phiArg g p q" and[simp]: "p ∈ allVars g"
    obtains ns m where "g ⊨ defNode g q-ns→m" "EntryPath g ns" "q ∈ phiUses g m" "m ∈ set (predecessors g (defNode g p))"
  proof-
    from assms obtain m where m: "q ∈ phiUses g m" "m ∈ set (predecessors g (defNode g p))"
      by (rule phiUses_exI')
    then obtain ns where "g ⊨ defNode g q-ns→m" "EntryPath g ns" by - (rule defUse_path_ex, auto)
    with m show thesis by - (rule that)
  qed

  lemma phiArg_path_ex:
    assumes "phiArg g p q" and[simp]: "p ∈ allVars g"
    obtains ns where "g ⊨ defNode g q-ns→defNode g p" "length ns > 1"
    by (rule phiArg_path_ex'[OF assms], rule, auto)

  lemma phiArg_tranclp_path_ex:
    assumes "r⁺⁺ p q" "p ∈ allVars g" and[simp]: "∧p q. r p q ==> phiArg g p q"
    obtains ns where "g ⊨ defNode g q-ns→defNode g p" "length ns > 1"
      "∀n ∈ set (butlast ns). ∃p q m ns'. r p q ∧ g ⊨ defNode g q-ns'→m ∧ (defNode g q) ∉ set (tl ns') ∧ q ∈ phiUses g m ∧ m ∈ set (predecessors g (defNode g p)) ∧ n ∈ set ns' ∧ set ns' ⊆ set ns ∧ defNode g p ∈ set ns"
  using assms(1,2) proof (induction rule: converse_tranclp_induct)
    case (base p)
    from base.hyps base.prems(2) obtain ns' m where ns': "g ⊨ defNode g q-ns'→m" "defNode g q ∉ set (tl ns')" "m ∈ set (predecessors g (defNode g p))" "q ∈ phiUses g m"
      by - (rule phiArg_path_ex', rule assms(3), auto intro: simple_path2)
    hence ns: "g ⊨ defNode g q-ns'@[defNode g p]→defNode g p" "length (ns'@[defNode g p]) > 1" by auto

    show ?case
    proof (rule base.prems(1)[OF ns, rule_format], rule exI, rule exI, rule exI, rule exI)
      fix n
      assume "n ∈ set (butlast (ns' @ [defNode g p]))"
      with base.hyps ns'
      show "r p q ∧
          g ⊨ defNode g q-ns'→m ∧
          defNode g q ∉ set (tl ns') ∧
          q ∈ phiUses g m ∧
          m ∈ set (predecessors g (defNode g p)) ∧ n ∈ set ns' ∧ set ns' ⊆ set (ns' @ [defNode g p]) ∧ defNode g p ∈ set (ns' @ [defNode g p])"
        by auto
    qed
  next
    case (step p p')
    from step.prems(2) step.hyps(1) obtain ns'₂ m where ns'₂: "g ⊨ defNode g p'-ns'₂→m" "m ∈ set (predecessors g (defNode g p))" "defNode g p' ∉ set (tl ns'₂)" "p' ∈ phiUses g m"
      by - (rule phiArg_path_ex', rule assms(3), auto intro: simple_path2)
    then obtain ns₂ where ns₂: "g ⊨ defNode g p'-ns₂→defNode g p" "length ns₂ > 1" "ns₂ = ns'₂@[defNode g p]" by (atomize_elim, auto)

    show thesis
    proof (rule step.IH)
      fix ns
      assume ns: "g ⊨ defNode g q-ns→defNode g p'" "1 < length ns"
      assume IH: "∀n∈set (butlast ns).
             ∃p q m ns'.
                r p q ∧
                g ⊨ defNode g q-ns'→m ∧
                defNode g q ∉ set (tl ns') ∧
                q ∈ phiUses g m ∧ m ∈ set (predecessors g (defNode g p)) ∧ n ∈ set ns' ∧ set ns' ⊆ set ns ∧ defNode g p ∈ set ns"

      let ?path = "ns@tl ns₂"
      have ns_ns₂: "g ⊨ defNode g q-?path→defNode g p" "1 < length ?path" using ns ns₂(1,2) by auto
      show thesis
      proof (rule step.prems(1)[OF ns_ns₂, rule_format])
        fix n
        assume n: "n ∈ set (butlast ?path)"
        show "∃p q m ns'a.
          r p q ∧
          g ⊨ defNode g q-ns'a→m ∧
          defNode g q ∉ set (tl ns'a) ∧
          q ∈ phiUses g m ∧ m ∈ set (predecessors g (defNode g p)) ∧ n ∈ set ns'a ∧ set ns'a ⊆ set ?path ∧ defNode g p ∈ set ?path"
        proof (cases "n ∈ set (butlast ns)")
          case True
          with IH obtain p q m ns' where "
                r p q ∧
                g ⊨ defNode g q-ns'→m ∧
                defNode g q ∉ set (tl ns') ∧
                q ∈ phiUses g m ∧ m ∈ set (predecessors g (defNode g p)) ∧ n ∈ set ns' ∧ set ns' ⊆ set ns ∧ defNode g p ∈ set ns" by auto
          thus ?thesis by - (rule exI, rule exI, rule exI, rule exI, auto)
        next
          case False
          from ns ns₂ have 1: "?path = butlast ns@ns₂"
            by - (rule concat_join[symmetric], auto simp: path2_def)
          from ns₂(1) n False 1 have "n ∈ set (butlast ns₂)" by (auto simp: butlast_append path2_not_Nil)
          with step.hyps ns'₂ ns₂(3) show ?thesis
            by - (subst 1, rule exI[where x=p], rule exI[where x=p'], rule exI, rule exI, auto simp: path2_not_Nil)
        qed
      qed
    next
      show "p' ∈ allVars g" using step.prems(2) step.hyps(1)[THEN assms(3)] by auto
    qed
  qed

  lemma non_dominated_predecessor:
    assumes "n ∈ set (αn g)" "n ≠ Entry g"
    obtains m where "m ∈ set (predecessors g n)" "¬dominates g n m"
  proof-
    obtain ns where "g ⊨ Entry g-ns→n"
      by (atomize_elim, rule Entry_reaches, auto simp add:assms(1))
    then obtain ns' where ns': "g ⊨ Entry g-ns'→n" "n ∉ set (butlast ns')"
      by (rule simple_path2)
    let ?m = "last (butlast ns')"
    from ns'(1) assms(2) obtain m: "g ⊨ Entry g-butlast ns'→?m" "?m ∈ set (predecessors g n)"
      by - (rule path2_unsnoc, auto)
    with m(1) ns'(2) show thesis
      by - (rule that, auto elim:dominatesE)
  qed

  lemmas dominates_trans'[trans, elim] = dominates_trans[OF invar]
  lemmas strict_dom_trans'[trans, elim] = strict_dom_trans[OF invar]
  lemmas dominates_refl'[simp] = dominates_refl[OF invar]
  lemmas dominates_antisymm'[dest] = dominates_antisymm[OF invar]

  lemma liveVal_in_allVars[simp]: "liveVal g v ==> v ∈ allVars g"
  by (induction rule: liveVal.induct, auto intro!: allUses_in_allVars)

  lemma phi_no_closed_loop:
    assumes[simp]: "p ∈ allVars g" and "phi g p = Some vs"
    shows "set vs ≠ {p}"
  proof (cases "defNode g p = Entry g")
    case True
    with assms(2) show ?thesis by auto
  next
    case False
    show ?thesis
    proof
      assume[simp]: "set vs = {p}"
      let ?n = "defNode g p"
      obtain ns where ns: "g ⊨ Entry g-ns→?n" "?n ∉ set (butlast ns)" by (rule simple_Entry_path, auto)
      let ?m = "last (butlast ns)"
      from ns False obtain m: "g ⊨ Entry g-butlast ns→?m" "?m ∈ set (predecessors g ?n)"
        by - (rule path2_unsnoc, auto)
      hence "p ∈ phiUses g ?m" using assms(2) by - (rule phiUses_exI, auto simp:phi_def)
      hence "defAss g ?m p" using m by - (rule allUses_def_ass, auto)
      then obtain l where l: "l ∈ set (butlast ns)" "p ∈ allDefs g l" using m by - (drule defAssD, auto)
      with assms(2) m have "l = ?n" by - (rule allDefs_disjoint', auto)
      with ns l m show False by auto
    qed
  qed

  lemma phis_phi: "phis g (n, v) = Some vs ==> phi g v = Some vs"
  unfolding phi_def
  apply (subst defNode_eq)
  by (auto simp: allDefs_def phi_def phiDefs_def intro: phis_in_αn)

  lemma trivial_phi: "trivial g v ==> phi g v ≠ None"
  by (auto simp: trivial_def isTrivialPhi_def split: option.splits)

  lemma trivial_finite: "finite {v. trivial g v}"
  by (rule finite_subset[OF _ phi_finite]) (auto dest: trivial_phi)

  lemma trivial_in_allVars: "trivial g v ==> v ∈ allVars g"
  by (drule trivial_phi, auto simp: allDefs_def phiDefs_def image_def phi_def intro: phis_in_αn intro!: allDefs_in_allVars)

  declare phiArg_def [simp del]
end

subsection ‹Bundling of CFG and Equivalent SSA CFG›

locale CFG_SSA_Transformed_base = old: CFG_base αe αn invar inEdges' Entry oldDefs oldUses + CFG_SSA_wf_base αe αn invar inEdges' Entry "defs" "uses" phis
for
  αe :: "'g ==> ('node::linorder × 'edgeD × 'node) set" and
  αn :: "'g ==> 'node list" and
  invar :: "'g ==> bool" and
  inEdges' :: "'g ==> 'node ==> ('node × 'edgeD) list" and
  Entry::"'g ==> 'node" and
  oldDefs :: "'g ==> 'node ==> 'var::linorder set" and
  oldUses :: "'g ==> 'node ==> 'var set" and
  "defs" :: "'g ==> 'node ==> 'val::linorder set" and
  "uses" :: "'g ==> 'node ==> 'val set" and
  phis :: "'g ==> ('node, 'val) phis" +
  fixes var :: "'g ==> 'val ==> 'var"

locale CFG_SSA_Transformed = CFG_SSA_Transformed_base αe αn invar inEdges' Entry oldDefs oldUses "defs" "uses" phis var
  + old: CFG_wf αe αn invar inEdges' Entry oldDefs oldUses + CFG_SSA_wf αe αn invar inEdges' Entry "defs" "uses" phis
for
  αe :: "'g ==> ('node::linorder × 'edgeD × 'node) set" and
  αn :: "'g ==> 'node list" and
  invar :: "'g ==> bool" and
  inEdges' :: "'g ==> 'node ==> ('node × 'edgeD) list" and
  Entry::"'g ==> 'node" and
  oldDefs :: "'g ==> 'node ==> 'var::linorder set" and
  oldUses :: "'g ==> 'node ==> 'var set" and
  "defs" :: "'g ==> 'node ==> 'val::linorder set" and
  "uses" :: "'g ==> 'node ==> 'val set" and
  phis :: "'g ==> ('node, 'val) phis" and
  var :: "'g ==> 'val ==> 'var" +
  assumes oldDefs_def: "oldDefs g n = var g ` defs g n"
  assumes oldUses_def: "n ∈ set (αn g) ==> oldUses g n = var g ` uses g n"
  assumes conventional: "
\<lbrakk>g ⊨ n-ns→m; n ∉ set (tl ns); v ∈ allDefs g n; v ∈ allUses g m; x ∈ set (tl ns); v' ∈ allDefs g x] ==> var g v' ≠ var g v"
  assumes phis_same_var[elim]: "phis g (n,v) = Some vs ==> v' ∈ set vs ==> var g v' = var g v"
  assumes allDefs_var_disjoint: "[n ∈ set (αn g); v ∈ allDefs g n; v' ∈ allDefs g n; v ≠ v'] ==> var g v' ≠ var g v"
begin
  lemma conventional': "[g ⊨ n-ns→m; n ∉ set (tl ns); v ∈ allDefs g n; v ∈ allUses g m; v' ∈ allDefs g x; var g v' = var g v] ==> x ∉ set (tl ns)"
    using conventional by auto

  lemma conventional'': "[g ⊨ defNode g v-ns→m; defNode g v ∉ set (tl ns); v ∈ allUses g m; var g v' = var g v; v ∈ allVars g; v' ∈ allVars g] ==> defNode g v' ∉ set (tl ns)"
    by (rule conventional'[where v=v and v'=v'], auto)

  lemma phiArg_same_var: "phiArg g p q ==> var g q = var g p"
    by (metis phiArg_def phi_def phis_same_var)

  lemma oldDef_defAss:
    assumes "v ∈ allUses g n" "g ⊨ Entry g-ns→n"
    obtains m where "m ∈ set ns" "var g v ∈ oldDefs g m"
  using assms proof (induction ns arbitrary: v n rule: length_induct)
    case (1 ns)
    from "1.prems"(2-) have 2: "defNode g v ∈ set ns"
      by - (rule defAss_defNode, rule allUses_def_ass, auto)
    let ?V = "defNode g v"
    from "1.prems"(2,3) have[simp]: "v ∈ allVars g" by auto
    thus ?case
    proof (cases v rule: defNode_cases)
      case simpleDef
      with 2 show thesis by - (rule "1.prems"(1), auto simp: oldDefs_def)
    next
      case phi
      then obtain vs where vs: "phi g v = Some vs" by auto
      from "1.prems"(3) 2 obtain ns' where ns': "g ⊨ Entry g-ns'→?V" "prefix ns' ns"
        by (rule old.path2_split_ex, auto)
      let ?V' = "last (butlast ns')"
      from ns' phi have nontriv: "length ns' ≥ 2"
        by - (rule old.path2_nontrivial, auto)
      hence 3: "g ⊨ Entry g-butlast ns'→?V'" "?V' ∈ set (old.predecessors g ?V)"
        using ns'(1) by (auto intro: old.path2_unsnoc)
      with phi vs obtain v' where v': "v' ∈ phiUses g ?V'" "var g v' = var g v"
        by - (rule phiArg_exI, auto simp: phi_def phis_same_var phiArg_def)
      show thesis
      proof (rule "1.IH"[rule_format])
        show "length (butlast ns') < length ns" using ns' by (cases ns', auto simp: old.path2_not_Nil2 dest: prefix_length_le)
        show "v' ∈ allUses g ?V'" using v'(1) by simp
      next
        fix n
        assume "n ∈ set (butlast ns')" "var g v' ∈ oldDefs g n"
        thus thesis
          using ns'(2)[THEN set_mono_prefix] v'(2) by - (rule "1.prems"(1)[of n], auto dest: in_set_butlastD)
      qed (rule 3(1))
    qed
  qed

  lemma allDef_path_from_simpleDef:
    assumes[simp]: "v ∈ allVars g"
    obtains n ns where "g ⊨ n-ns→defNode g v" "old.EntryPath g ns" "var g v ∈ oldDefs g n"
  proof-
    let ?V = "defNode g v"
    from assms obtain ns where ns: "g ⊨ Entry g-ns→?V" "old.EntryPath g ns"
      by - (rule old.Entry_reachesE, auto)
    from assms show thesis
    proof (cases v rule: defNode_cases)
      case simpleDef
      thus thesis by - (rule that, auto simp: oldDefs_def)
    next
      case phi
      then obtain vs where vs: "phi g v = Some vs" by auto
      let ?V' = "last (butlast ns)"
      from ns phi have nontriv: "length ns ≥ 2"
        by - (rule old.path2_nontrivial, auto)
      hence 3: "g ⊨ Entry g-butlast ns→?V'" "?V' ∈ set (old.predecessors g ?V)"
        using ns(1) by (auto intro: old.path2_unsnoc)
      with phi vs obtain v' where v': "v' ∈ phiUses g ?V'" "var g v' = var g v"
        by - (rule phiArg_exI, auto simp: phi_def phis_same_var phiArg_def)
      with 3(1) obtain n where n: "n ∈ set (butlast ns)" "var g v' ∈ oldDefs g n"
        by - (rule oldDef_defAss[of v' g], auto)
      with ns obtain ns' where "g ⊨ n-ns'→?V" "suffix ns' ns"
        by - (rule old.path2_split_ex'[OF ns(1)], auto intro: in_set_butlastD simp: Sublist.suffix_def)
      with n(2) v'(2) ns(2) show thesis
        by - (rule that, assumption, erule old.EntryPath_suffix, auto)
    qed
  qed

  lemma defNode_var_disjoint:
    assumes "p ∈ allVars g" "q ∈ allVars g" "p ≠ q" "defNode g p = defNode g q"
    shows "var g p ≠ var g q"
  proof-
    have "q ∈ allDefs g (defNode g p)" using assms(2) assms(4) by (auto)
    thus ?thesis using assms(1-3)
      by - (rule allDefs_var_disjoint[of "defNode g p" g], auto)
  qed

  lemma phiArg_distinct_nodes:
    assumes "phiArg g p q" "p ≠ q" and[simp]: "p ∈ allVars g"
    shows "defNode g p ≠ defNode g q"
  proof
    have "p ∈ allDefs g (defNode g p)" by simp
    moreover assume "defNode g p = defNode g q"
    ultimately have "var g p ≠ var g q" using assms
      by - (rule defNode_var_disjoint, auto)
    moreover
    from assms(1) have "var g q = var g p" by (rule phiArg_same_var)
    ultimately show False by simp
  qed

  lemma phiArgs_def_distinct:
    assumes "phiArg g p q" "phiArg g p r" "q ≠ r" "p ∈ allVars g"
    shows "defNode g q ≠ defNode g r"
  proof (rule)
    assume "defNode g q = defNode g r"
    hence "var g q ≠ var g r" using assms by - (rule defNode_var_disjoint, auto)
    thus False using phiArg_same_var[OF assms(1)] phiArg_same_var[OF assms(2)] by simp
  qed

  lemma defNode_not_on_defUse_path:
    assumes p: "g ⊨ defNode g p-ns→n" "defNode g p ∉ set (tl ns)" "p ∈ allUses g n"
    assumes[simp]: "q ∈ allVars g" "p ≠ q" "var g p = var g q"
    shows "defNode g q ∉ set ns"
  proof-
    let ?P = "defNode g p"
    let ?Q = "defNode g q"

    have[simp]: "p ∈ allVars g" using p(1,3) by auto
    have "?P ≠ ?Q" using defNode_var_disjoint[of p g q] by auto
    moreover have "?Q ∉ set (tl ns)" using p(2,3)
      by - (rule conventional'[OF p(1), of p q], auto)
    ultimately show ?thesis using p(1) by (cases ns, auto simp: old.path2_def)
  qed

  lemma defUse_paths_disjoint:
    assumes p: "g ⊨ defNode g p-ns→n" "defNode g p ∉ set (tl ns)" "p ∈ allUses g n"
    assumes q: "g ⊨ defNode g q-ms→m" "defNode g q ∉ set (tl ms)" "q ∈ allUses g m"
    assumes[simp]: "p ≠ q" "var g p = var g q"
    shows "set ns ∩ set ms = {}"
  proof (rule equals0I)
    fix y
    assume y: "y ∈ set ns ∩ set ms"

    {
      fix p ns n
      assume p: "g ⊨ defNode g p-ns→n" "defNode g p ∉ set (tl ns)" "p ∈ allUses g n"
      assume y: "y ∈ set ns"
      from p(1,3) have dom: "old.dominates g (defNode g p) n" by - (rule allUses_dominated, auto)
      moreover
      obtain ns' where "g ⊨ y-ns'→n" "suffix ns' ns"
        by (rule old.path2_split_first_last[OF p(1) y], auto)
      ultimately have "old.dominates g (defNode g p) y" using suffix_tl_subset[of ns' ns] p(2)
        by - (rule old.dominates_extend[where ms=ns'], auto)
    }
    with assms y have dom: "old.dominates g (defNode g p) y" "old.dominates g (defNode g q) y" by auto

    {
      fix p ns n q ms m
      let ?P = "defNode g p"
      let ?Q = "defNode g q"

      assume p: "g ⊨ defNode g p-ns→n" "defNode g p ∉ set (tl ns)" "p ∈ allUses g n" "old.dominates g ?P y" "y ∈ set ns"
      assume q: "g ⊨ defNode g q-ms→m" "defNode g q ∉ set (tl ms)" "q ∈ allUses g m" "old.dominates g ?Q y" "y ∈ set ms"
      assume[simp]: "p ≠ q" "var g p = var g q"
      assume dom: "old.dominates g ?P ?Q"
      then obtain pqs where pqs: "g ⊨ ?P-pqs→?Q" "?P ∉ set (tl pqs)" by (rule old.dominates_path, auto intro: old.simple_path2)
      from p obtain ns₂ where ns₂: "g ⊨ y-ns₂→n" "suffix ns₂ ns" by - (rule old.path2_split_first_last, auto)
      from q obtain ms₁ where ms₁: "g ⊨ ?Q-ms₁→y" "prefix ms₁ ms" by - (rule old.path2_split_first_last, auto)
      have "var g q ≠ var g p"
      proof (rule conventional[OF _ _ _ p(3)])
        let ?path = "(pqs@tl ms₁)@tl ns₂"
        show "g ⊨ ?P-?path→n" using pqs ms₁ ns₂
          by (auto simp del:append_assoc intro:old.path2_app)
        have "?P ∉ set (tl ns₂)" using p(2) ns₂(2)[THEN suffix_tl_subset, THEN subsetD] by auto
        moreover
        have[simp]: "q ∈ allVars g" "p ∈ allVars g" using p q by auto
        have "?P ∉ set (tl ms)" using q
          by - (rule conventional'[where v'=p and v=q], auto)
        hence "?P ∉ set (tl ms₁)" using ms₁(2)[simplified, THEN prefix_tl_subset] by auto
        ultimately
        show "?P ∉ set (tl ?path)" using pqs(2)
          by - (rule notI, auto dest: subsetD[OF set_tl_append'])
        show "p ∈ allDefs g (defNode g p)" by auto
        have "?P ≠ ?Q" using defNode_var_disjoint[of p g q] by auto
        hence 1: "length pqs > 1" using pqs by - (rule old.path2_nontriv)
        hence "?Q ∈ set (tl pqs)" using pqs unfolding old.path2_def by (auto intro:last_in_tl)
        moreover from 1 have "pqs ≠ []" by auto
        ultimately show "?Q ∈ set (tl ?path)" by simp
        show "q ∈ allDefs g ?Q" by simp
      qed
      hence False by simp
    }
    from this[OF p _ _ q] this[OF q _ _ p] y dom show False
      by - (rule old.dominates_antitrans[OF _ dom], auto)
  qed

  lemma oldDefsI: "v ∈ defs g n ==> var g v ∈ oldDefs g n" by (simp add: oldDefs_def)
 
  lemma simpleDefs_phiDefs_var_disjoint:
    assumes "v ∈ phiDefs g n" "n ∈ set (αn g)"
    shows "var g v ∉ oldDefs g n"
  proof
    from assms have[simp]: "v ∈ allVars g" by auto
    assume "var g v ∈ oldDefs g n"
    then obtain v'' where v'': "v'' ∈ defs g n" "var g v'' = var g v"
      by (auto simp: oldDefs_def)
    from this(1) assms have "v'' ≠ v"
      using simpleDefs_phiDefs_disjoint[of n g] by (auto simp: phiArg_def)
    with v'' assms show False
      using allDefs_var_disjoint[of n g v'' v] by auto
  qed

  lemma liveVal_use_path: 
    assumes "liveVal g v"
    obtains ns m where "g ⊨ defNode g v-ns→m" "var g v ∈ oldUses g m"
      "∧x. x ∈ set (tl ns) ==> var g v ∉ oldDefs g x"
  using assms proof (induction)
    case (liveSimple m v)
    from liveSimple.hyps have[simp]: "v ∈ allVars g"
      by - (rule allUses_in_allVars, auto)
    from liveSimple.hyps obtain ns where ns: "g ⊨ defNode g v-ns→m" "defNode g v ∉ set (tl ns)"
      by - (rule defUse_path_ex, auto intro!: uses_in_allUses elim: old.simple_path2)
    from this(1) show thesis
    proof (rule liveSimple.prems)
      show "var g v ∈ oldUses g m" using liveSimple.hyps by (auto simp: oldUses_def)
      {
        fix x
        assume asm: "x ∈ set (tl ns)" "var g v ∈ oldDefs g x"
        then obtain v' where "v' ∈ defs g x" "var g v' = var g v"
          by (auto simp: oldDefs_def)
        with asm liveSimple.hyps have False
          by - (rule conventional[OF ns, of v x v', THEN notE], auto)
      }
      thus "∧x. x ∈ set (tl ns) ==> var g v ∉ oldDefs g x" by auto
    qed
  next
    case (livePhi v v')
    from livePhi.hyps have[simp]: "v ∈ allVars g" "v' ∈ allVars g" "var g v' = var g v"
      by (auto intro: phiArg_same_var)
    show thesis
    proof (rule livePhi.IH)
      fix ns m
      assume asm: "g ⊨ defNode g v-ns→m" "var g v ∈ oldUses g m"
        "∧x. x ∈ set (tl ns) ==> var g v ∉ oldDefs g x"
      from livePhi.hyps(2) obtain ns' m' where ns': "g ⊨ defNode g v'-ns'→m'" "v' ∈ phiUses g m'"
        "m' ∈ set (old.predecessors g (defNode g v))" "defNode g v' ∉ set (tl ns')"
        by (rule phiArg_path_ex', auto elim: old.simple_path2)
      show thesis 
      proof (rule livePhi.prems)
        show "g ⊨ defNode g v'-(ns'@[defNode g v])@tl ns→m"
        apply (rule old.path2_app)
         apply (rule old.path2_snoc[OF ns'(1,3)])
        by (rule asm(1))
        show "var g v' ∈ oldUses g m" using asm(2) by simp
        {
          fix x
          assume asm: "x ∈ set (tl ns')" "var g v ∈ oldDefs g x"
          then obtain v'' where "v'' ∈ defs g x" "var g v'' = var g v"
            by (auto simp: oldDefs_def)
          with asm ns'(2) have False
            by - (rule conventional[OF ns'(1,4), of v' x v'', THEN notE], auto)
        }
        then show "∧x. x ∈ set (tl ((ns'@[defNode g v])@tl ns)) ==> var g v' ∉ oldDefs g x"
          using simpleDefs_phiDefs_var_disjoint[of v g "defNode g v"] livePhi.hyps(2)
          by (auto dest!: set_tl_append'[THEN subsetD] asm(3) simp: phiArg_def)
      qed
    qed
  qed
end

end