Theory Construct_SSA_notriv_code

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

subsection ‹Code Equations for SSA Minimization›

theory Construct_SSA_notriv_code imports
  SSA_CFG_code
  Construct_SSA_notriv
  While_Combinator_Exts
begin

abbreviation (input) "const x  (λ_. x)"

context CFG_SSA_Transformed_notriv_base begin
  definition [code]: "substitution_code g next = the (the_trivial (snd next) (the (phis g next)))"
  definition [code]: "substNext_code g next  λv. if v = snd next then substitution_code g next else v"
  definition [code]: "uses'_code g next n  substNext_code g next ` uses g n"

  lemma substNext_code_alt_def:
    "substNext_code g next = id(snd next := substitution_code g next)"
    unfolding substNext_code_def by auto
end

type_synonym ('g, 'node, 'val) chooseNext_code = "('node  'val set)  ('node, 'val) phis_code  'g  ('node × 'val)"

locale CFG_SSA_Transformed_notriv_base_code =
  ssa:CFG_SSA_wf_base_code αe αn invar inEdges' Entry "defs" "uses" phis +
  CFG_SSA_Transformed_notriv_base αe αn invar inEdges' Entry oldDefs oldUses "defs" "usesOf  uses" "λg. Mapping.lookup (phis g)" var "λuses phis. chooseNext_all uses (Mapping.Mapping 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) mapping" and
  phis :: "'g  ('node, 'val) phis_code" and
  var :: "'g  'val  'var" and
  chooseNext_all :: "('g, 'node, 'val) chooseNext_code"
begin
  definition [code]: "cond_code g = ssa.redundant_code g"

  definition uses'_codem :: "'g  'node × 'val  'val  ('val, 'node set) mapping  ('node, 'val set) mapping"
  where [code]: "uses'_codem g next next' nodes_of_uses =
    fold (λn. Mapping.update n (Set.insert next' (Set.remove (snd next) (the (Mapping.lookup (uses g) n)))))
      (sorted_list_of_set (case_option {} id (Mapping.lookup nodes_of_uses (snd next))))
      (uses g)"

  definition nodes_of_uses' :: "'g  'node × 'val  'val  'val set  ('val, 'node set) mapping  ('val, 'node set) mapping"
  where [code]: "nodes_of_uses' g next next' phiVals nodes_of_uses =
    (let users = case_option {} id (Mapping.lookup nodes_of_uses (snd next))
    in
    if (next'  phiVals) then Mapping.map_default next' {} (λns. ns  users) (Mapping.delete (snd next) nodes_of_uses)
    else Mapping.delete (snd next) nodes_of_uses)"

  (* FIXME: phis'_code ist in O(n) → verwende nodes_of_uses ? *)
  definition [code]: "phis'_code g next  map_values (λ(n,v) vs. if v = snd next then None else Some (map (substNext_code g next) vs)) (phis g)"

  (* Schon besser: O(log(n)) *)
  definition [code]: "phis'_codem g next next' nodes_of_phis =
    fold (λn. Mapping.update n (List.map (id(snd next := next')) (the (Mapping.lookup (phis g) n))))
      (sorted_list_of_set (case_option {} (Set.remove next) (Mapping.lookup nodes_of_phis (snd next))))
      (Mapping.delete next (phis g))"

  definition nodes_of_phis' :: "'g  'node × 'val  'val  ('val, ('node × 'val) set) mapping  ('val, ('node × 'val) set) mapping"
  where [code]: "nodes_of_phis' g next next' nodes_of_phis =
      (let old_phis = Set.remove next (case_option {} id (Mapping.lookup nodes_of_phis (snd next)));
        nop = Mapping.delete (snd next) nodes_of_phis
      in
      Mapping.map_default next' {} (λns. (Set.remove next ns)  old_phis) nop)"

  definition [code]: "triv_phis' g next triv_phis nodes_of_phis
    = (Set.remove next triv_phis)  (Set.filter (λn. ssa.trivial_code (snd n) (the (Mapping.lookup (phis g) n))) (case_option {} (Set.remove next) (Mapping.lookup nodes_of_phis (snd next))))"

  definition [code]: "step_code g = (let next = chooseNext' g in (uses'_code g next, phis'_code g next))"
  definition [code]: "step_codem g next next' nodes_of_uses nodes_of_phis = (uses'_codem g next next' nodes_of_uses, phis'_codem g next next' nodes_of_phis)"

  definition phi_equiv_mapping :: "'g  ('val, 'a set) mapping  ('val, 'a set) mapping  bool" ("_  _ φ _" 50)
    where "g  nou1 φ nou2  v  Mapping.keys (ssa.phidefNodes g). case_option {} id (Mapping.lookup nou1 v) = case_option {} id (Mapping.lookup nou2 v)"
end

locale CFG_SSA_Transformed_notriv_linorder = CFG_SSA_Transformed_notriv_base αe αn invar inEdges' Entry oldDefs oldUses "defs" "uses" phis var chooseNext_all
   + CFG_SSA_Transformed_notriv αe αn invar inEdges' Entry oldDefs oldUses "defs" "uses" phis var chooseNext_all
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" and
  chooseNext_all :: "('node  'val set)  ('node, 'val) phis  'g  ('node × 'val)"
begin
  lemma isTrivial_the_trivial: " phi g v = Some vs; isTrivialPhi g v v'   the_trivial v vs = Some v'"
    by (subst the_trivialI [of vs v v']) (auto simp: isTrivialPhi_def)

  lemma the_trivial_THE_isTrivial: " phi g v = Some vs; trivial g v   the_trivial v vs = Some (The (isTrivialPhi g v))"
    apply (frule isTrivialPhi_det)
    apply clarsimp
    apply (frule(1) isTrivial_the_trivial)
    by (auto dest: isTrivial_the_trivial intro!: the_equality intro: sym)

  lemma substitution_code_correct:
    assumes "redundant g"
    shows "substitution g = substitution_code g (chooseNext' g)"
  proof -
    from substitution [OF assms] have "phi g (chooseNext g)  None"
      unfolding isTrivialPhi_def by (clarsimp split: option.splits)
    then obtain vs where "phi g (chooseNext g) = Some vs" by blast
    with isTrivial_the_trivial [OF this substitution [OF assms]] chooseNext'[OF assms]
    show ?thesis unfolding substitution_code_def by (auto simp: phis_phi[of g "fst (chooseNext' g)"])
  qed

  lemma substNext_code_correct:
    assumes "redundant g"
    shows "substNext g = substNext_code g (chooseNext' g)"
    unfolding substNext_def [abs_def] substNext_code_def
    by (auto simp: substitution_code_correct [OF assms])

  lemma uses'_code_correct:
    assumes "redundant g"
    shows "uses' g = uses'_code g (chooseNext' g)"
    unfolding uses'_def [abs_def] uses'_code_def [abs_def]
    by (auto simp: substNext_code_correct [OF assms])

end

context CFG_SSA_Transformed_notriv_linorder
begin
  lemma substAll_terminates: "while_option (cond g) (step g) (uses g, phis g)  None"
  apply (rule notI)
  apply (rule while_option_None_invD [where I="inst' g" and r="{(y,x). (inst' g x  cond g x)  y = step g x}"], assumption)
     apply (rule wf_if_measure[where f="λ(u,p). card (dom p)"])
     defer
     apply simp
     apply unfold_locales
    apply (case_tac s)
    apply (simp add: step_def cond_def)
    apply (rule step_preserves_inst [unfolded step_def, simplified], assumption+)
   apply (simp add: step_def cond_def)
  apply (clarsimp simp: cond_def step_def split:prod.split)
  proof-
    fix u p
    assume "CFG_SSA_Transformed_notriv αe αn invar inEdges' Entry oldDefs oldUses defs (uses(g:=u)) (phis(g:=p)) var chooseNext_all"
    then interpret i: CFG_SSA_Transformed_notriv αe αn invar inEdges' Entry oldDefs oldUses "defs" "uses(g:=u)" "phis(g:=p)" var chooseNext_all .
    assume "i.redundant g"
    thus "card (dom (i.phis' g)) < card (dom p)" by (rule i.substAll_wf[of g, simplified])
  qed
end

locale CFG_SSA_Transformed_notriv_linorder_code =
  CFG_SSA_Transformed_code αe αn invar inEdges' Entry oldDefs oldUses "defs" "uses" phis var
+ CFG_SSA_Transformed_notriv_base_code αe αn invar inEdges' Entry oldDefs oldUses "defs" "uses" phis var chooseNext_all
+ CFG_SSA_Transformed_notriv_linorder αe αn invar inEdges' Entry oldDefs oldUses "defs" "usesOf  uses" "λg. Mapping.lookup (phis g)" var
  "λuses phis. chooseNext_all uses (Mapping.Mapping 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) mapping" and
  phis :: "'g  ('node, 'val) phis_code" and
  var :: "'g  'val  'var" and
  chooseNext_all :: "('g, 'node, 'val) chooseNext_code"
+
assumes chooseNext_all_code:
  "CFG_SSA_Transformed_code αe αn invar inEdges' Entry oldDefs oldUses defs u p var 
  CFG_SSA_wf_base_code.redundant_code p g 
  chooseNext_all (usesOf (u g)) (p g) g = Max (CFG_SSA_wf_base_code.trivial_phis p g)"

locale CFG_SSA_step_code =
  step_code: CFG_SSA_Transformed_notriv_linorder_code αe αn invar inEdges' Entry oldDefs oldUses "defs" "uses" phis var chooseNext_all
+
  CFG_SSA_step αe αn invar inEdges' Entry oldDefs oldUses "defs" "usesOf  uses" "λg. Mapping.lookup (phis g)" var "λuses phis. chooseNext_all uses (Mapping.Mapping phis)" g
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) mapping" and
  phis :: "'g  ('node, 'val) phis_code" and
  var :: "'g  'val  'var" and
  chooseNext_all :: "('g, 'node, 'val) chooseNext_code" and
  g :: 'g

context CFG_SSA_Transformed_notriv_linorder_code
begin
  abbreviation "u_g g u  uses(g:=u)"
  abbreviation "p_g g p  phis(g:=p)"
  abbreviation "cN  (λuses phis. chooseNext_all uses (Mapping.Mapping phis))"

  interpretation uninst_code: CFG_SSA_Transformed_notriv_base_code αe αn invar inEdges' Entry oldDefs oldUses "defs" u p var chooseNext_all
    for u p
  by unfold_locales

  interpretation uninst: CFG_SSA_Transformed_notriv_base αe αn invar inEdges' Entry oldDefs oldUses "defs" u p var cN
    for u p
  by unfold_locales

  lemma phis'_code_correct:
    assumes "ssa.redundant g"
    shows "phis' g = Mapping.lookup (phis'_code g (chooseNext' g))"
  unfolding phis'_def [abs_def] phis'_code_def [abs_def]
  by (auto simp: Mapping_lookup_map_values substNext_code_correct [OF assms] split: if_split Option.bind_split)

  lemma redundant_ign[simp]: "uninst_code.ssa.redundant_code (const p) g = uninst_code.ssa.redundant_code (phis(g:=p)) g"
  unfolding uninst_code.ssa.redundant_code_def uninst_code.ssa.trivial_code_def[abs_def] CFG_SSA_wf_base.CFG_SSA_wf_defs uninst_code.ssa.trivial_phis_def
  unfolding fun_upd_same
  ..

  lemma uses'_ign[simp]: "uninst_code.uses'_codem (const u) g = uninst_code.uses'_codem (u_g g u) g"
  unfolding uninst_code.uses'_codem_def[abs_def] uninst.substNext_code_def uninst.substitution_code_def uninst_code.ssa.trivial_code_def[abs_def] CFG_SSA_wf_base.CFG_SSA_wf_defs
    uninst.uses'_code_def[abs_def]
  by simp

  lemma phis'_ign[simp]: "uninst_code.phis'_code (const p) g = uninst_code.phis'_code (phis(g:=p)) g"
  unfolding uninst_code.phis'_code_def[abs_def] uninst.substNext_code_def uninst.substitution_code_def uninst_code.ssa.trivial_code_def[abs_def] CFG_SSA_wf_base.CFG_SSA_wf_defs
  unfolding fun_upd_same
  ..

  lemma phis'm_ign[simp]: "uninst_code.phis'_codem (const p) g = uninst_code.phis'_codem (phis(g:=p)) g"
  unfolding uninst_code.phis'_codem_def[abs_def] uninst.substNext_code_def uninst.substitution_code_def uninst_code.ssa.trivial_code_def[abs_def] CFG_SSA_wf_base.CFG_SSA_wf_defs
  unfolding fun_upd_same
  ..

  lemma set_sorted_list_of_set_phis_dom [simp]:
  "set (sorted_list_of_set {x  dom (Mapping.lookup (phis g)). P x}) = {x  dom (Mapping.lookup (phis g)). P x}"
  apply (subst set_sorted_list_of_set)
  by (rule finite_subset [OF _ ssa.phis_finite [of g]]) auto

  lemma phis'_codem_correct:
    assumes "g  nodes_of_phis φ (ssa.phiNodes_of g)" and "next  Mapping.keys (phis g)"
    shows "phis'_codem g next (substitution_code g next) nodes_of_phis = phis'_code g next"
  proof -
    from assms
    have "phis'_code g next = mmap (map (substNext_code g next)) (Mapping.delete next (phis g))"
      unfolding phis'_code_def mmap_def phi_equiv_mapping_def
    apply (subst mapping_eq_iff)
    by (auto simp: Mapping_lookup_map_values Mapping_lookup_map Option.bind_def map_option_case lookup_delete keys_dom_lookup
      dest: ssa.phis_disj [where n="fst next" and v="snd next", simplified] split: option.splits)

    also from assms have "... = phis'_codem g next (substitution_code g next) nodes_of_phis"
      unfolding phis'_codem_def mmap_def ssa.lookup_phiNodes_of [OF ssa.phis_finite] phi_equiv_mapping_def
    apply (subst mapping_eq_iff)
    apply (simp add: Mapping_lookup_map lookup_delete map_option_case)
    by (erule_tac x="next" in ballE)
    (force intro!: map_idI
      simp: substNext_code_def keys_dom_lookup fun_upd_apply
      split: option.splits if_splits)+
    finally show ?thesis ..
  qed

  lemma uses_transfer [transfer_rule]: "(rel_fun (=) (pcr_mapping (=) (=))) (λg n. Mapping.lookup (uses g) n) uses"
    by (auto simp: mapping.pcr_cr_eq cr_mapping_def Mapping.lookup.rep_eq)

  lemma uses'_codem_correct:
  assumes "g  nodes_of_uses φ ssa.useNodes_of g" and "next  Mapping.keys (phis g)"
  shows "usesOf (uses'_codem g next (substitution_code g next) nodes_of_uses) = uses'_code g next"
  using dom_uses_in_graph [of g] assms
  unfolding uses'_codem_def uses'_code_def [abs_def]
  apply (clarsimp simp: mmap_def Mapping.replace_def [abs_def] phi_equiv_mapping_def intro!: ext)
  apply (transfer' fixing: g)
  apply (subgoal_tac "b. finite
             {n. (y. Mapping.lookup (uses g) n = Some y) 
                 (x2. Mapping.lookup (uses g) n = Some x2  n  set (αn g)  b  x2)}")
   prefer 2
   apply (rule finite_subset [where B="set (αn g)"])
    apply (clarsimp simp: Mapping.keys_dom_lookup)
   apply simp
  by (auto simp: map_of_map_restrict restrict_map_def substNext_code_def fold_update_conv Mapping.keys_dom_lookup
    split: option.splits)

  lemma step_ign[simp]: "uninst_code.step_codem (const u) (const p) g = uninst_code.step_codem (u_g g u) (phis(g:=p)) g"
  by (rule ext)+ (simp add: uninst_code.step_codem_def Let_def)

  lemma cN_transfer [transfer_rule]: "(rel_fun (=) (rel_fun (pcr_mapping (=) (=)) (=))) cN chooseNext_all"
    by (auto simp: rel_fun_def mapping.pcr_cr_eq cr_mapping_def mapping.rep_inverse)

  lemma usesOf_transfer [transfer_rule]: "(rel_fun (pcr_mapping (=) (=)) (=)) (λm x. case_option {} id (m x))  usesOf"
    by (auto simp: rel_fun_def mapping.pcr_cr_eq cr_mapping_def Mapping.lookup.rep_eq)

  lemma dom_phis'_codem:
  assumes "ns. Mapping.lookup nodes_of_phis (snd next) = Some ns  finite ns"
  shows "dom (Mapping.lookup (phis'_codem g next next' nodes_of_phis)) = dom (Mapping.lookup (phis g))  (case_option {} id (Mapping.lookup nodes_of_phis (snd next))) - {next}"
    using assms unfolding phis'_codem_def
    by (auto split: if_splits option.splits  simp: lookup_delete)

  lemma dom_phis'_code [simp]:
  shows "dom (Mapping.lookup (phis'_code g next)) = dom (Mapping.lookup (phis g)) - {v. snd v = snd next}"
    by (auto simp: phis'_code_def Mapping_lookup_map_values bind_eq_Some_conv)

  lemma nodes_of_phis_finite [simplified]:
  assumes "g  nodes_of_phis φ ssa.phiNodes_of g" and "Mapping.lookup nodes_of_phis v = Some ns" and "v  Mapping.keys (ssa.phidefNodes g)"
  shows "finite ns"
  using assms unfolding phi_equiv_mapping_def
    by (erule_tac x=v in ballE) (auto intro: finite_subset [OF _ ssa.phis_finite [of g]])

  lemma lookup_phis'_codem_next:
  assumes "ns. Mapping.lookup nodes_of_phis (snd next) = Some ns  finite ns"
  shows "Mapping.lookup (phis'_codem g next next' nodes_of_phis) next = None"
    using assms unfolding phis'_codem_def
    by (auto simp: Set.remove_def lookup_delete split: option.splits)

  lemma lookup_phis'_codem_other:
  assumes "g  nodes_of_phis φ (ssa.phiNodes_of g)"
  and "next  Mapping.keys (phis g)" and "next  φ"
  shows "Mapping.lookup (phis'_codem g next (substitution_code g next) nodes_of_phis) φ =
    map_option (map (substNext_code g next)) (Mapping.lookup (phis g) φ)"
  proof (cases "snd next  snd φ")
    case True
    with assms(1,2) show ?thesis
      unfolding phis'_codem_correct [OF assms(1,2)] phis'_code_def
      using assms(3)
      by (auto intro!: map_idI [symmetric] simp: Mapping_lookup_map_values substNext_code_def lookup_delete map_option_case split: option.splits prod.splits)
  next
    case False
    hence "snd next = snd φ" by simp
    with assms(3) have "fst next  fst φ" by (cases "next", cases φ) auto
    with assms(2) False have [simp]: "Mapping.lookup (phis g) φ = None"
      by (cases φ, cases "next") (fastforce simp: keys_dom_lookup dest: ssa.phis_disj)
    from fst next  fst φ snd next = snd φ show ?thesis
    unfolding phis'_codem_correct [OF assms(1,2)] phis'_code_def
      by (auto simp: Mapping_lookup_map_values lookup_delete map_option_case substNext_code_def split: option.splits)
  qed

  lemma lookup_nodes_of_phis'_subst [simp]:
  "Mapping.lookup (nodes_of_phis' g next (substitution_code g next) nodes_of_phis) (substitution_code g next) =
    Some ((case_option {} (Set.remove next) (Mapping.lookup nodes_of_phis (substitution_code g next)))  (case_option {} (Set.remove next) (Mapping.lookup nodes_of_phis (snd next))))"
  unfolding nodes_of_phis'_def
    by (clarsimp simp: Mapping_lookup_map_default Set.remove_def lookup_delete split: option.splits)

  lemma lookup_nodes_of_phis'_not_subst:
  "v  substitution_code g next 
  Mapping.lookup (nodes_of_phis' g next (substitution_code g next) nodes_of_phis) v = (if v = snd next then None else Mapping.lookup nodes_of_phis v)"
  unfolding nodes_of_phis'_def
    by (clarsimp simp: Mapping_lookup_map_default lookup_delete)

  lemma lookup_phis'_code:
  "Mapping.lookup (phis'_code g next) v = (if snd v = snd next then None else map_option (map (substNext_code g next)) (Mapping.lookup (phis g) v))"
    unfolding phis'_code_def
    by (auto simp: Mapping_lookup_map_values bind_eq_None_conv map_conv_bind_option comp_def split: prod.splits)

  lemma phi_equiv_mappingE':
    assumes "g  m1 φ ssa.phiNodes_of g"
    and "Mapping.lookup (phis g) x = Some vs" and "b  set vs" and "b  snd ` Mapping.keys (phis g)"
    obtains "Mapping.lookup m1 b = Some {n  Mapping.keys (phis g). b  set (the (Mapping.lookup (phis g) n))}"
    using assms unfolding phi_equiv_mapping_def
    apply (auto split: option.splits if_splits)
    apply (clarsimp simp: keys_dom_lookup)
    apply (rename_tac n φ_args)
    apply (erule_tac x="(n,b)" in ballE)
     prefer 2 apply auto[1]
    by (cases x) force

  lemma phi_equiv_mappingE:
    assumes "g  m1 φ ssa.phiNodes_of g" and "b  Mapping.keys (phis g)"
    and "Mapping.lookup (phis g) x = Some vs" and "snd b  set vs"
    obtains ns where "Mapping.lookup m1 (snd b) = Some {n  Mapping.keys (phis g). snd b  set (the (Mapping.lookup (phis g) n))}"
  proof -
    from assms(2) have "snd b  snd ` Mapping.keys (phis g)" by simp
    with assms(1,3,4) show ?thesis
    by (rule phi_equiv_mappingE') (rule that)
  qed

  lemma phi_equiv_mappingE2':
    assumes "g  m1 φ ssa.phiNodes_of g"
    and "b  snd ` Mapping.keys (phis g)"
    and "φ  Mapping.keys (phis g). b  set (the (Mapping.lookup (phis g) φ))"
    shows "Mapping.lookup m1 b = None  Mapping.lookup m1 b = Some {}"
    using assms unfolding phi_equiv_mapping_def
    apply (auto split: option.splits if_splits)
    apply (clarsimp simp: keys_dom_lookup)
    apply (rename_tac n φ_args)
    apply (erule_tac x="(n,b)" in ballE)
     prefer 2 apply auto[1]
    by (cases "Mapping.lookup m1 b"; auto)

  lemma keys_phis'_codem [simp]: "Mapping.keys (phis'_codem g next next' (ssa.phiNodes_of g)) = Mapping.keys (phis g) - {next}"
    unfolding phis'_codem_def
  by (auto simp: keys_dom_lookup fun_upd_apply lookup_delete split: option.splits if_splits)

  lemma keys_phis'_codem':
    assumes "g  nodes_of_phis φ ssa.phiNodes_of g" and "next  Mapping.keys (phis g)"
    shows "Mapping.keys (phis'_codem g next next' nodes_of_phis) = Mapping.keys (phis g) - {next}"
    using assms unfolding phis'_codem_def phi_equiv_mapping_def ssa.keys_phidefNodes [OF ssa.phis_finite]
  by (force split: option.splits if_splits simp: fold_update_conv fun_upd_apply keys_dom_lookup lookup_delete)

  lemma triv_phis'_correct:
    assumes "g  nodes_of_phis φ ssa.phiNodes_of g" and "next  Mapping.keys (phis g)" and "ssa.trivial g (snd next)"
    shows "uninst_code.triv_phis' (const (phis'_codem g next (substitution_code g next) nodes_of_phis)) g next (ssa.trivial_phis g) nodes_of_phis = uninst_code.ssa.trivial_phis (const (phis'_codem g next (substitution_code g next) nodes_of_phis)) g"
  proof (rule set_eqI)
    note keys_phis'_codem' [OF assms(1,2), simp]
    fix φ

    from assms(2,3) ssa.phis_in_αn [of g "fst next" "snd next"]
    have "ssa.redundant g"
      unfolding ssa.redundant_def ssa.allVars_def ssa.allDefs_def ssa.phiDefs_def
      by (cases "next") (auto simp: keys_dom_lookup)

    then interpret step: CFG_SSA_step_code αe αn invar inEdges' Entry oldDefs oldUses "defs" "uses" phis var chooseNext_all
      by unfold_locales

    let ?u_g = "λg. Mapping.Mapping (λn. if step.u_g g n = {} then None else Some (step.u_g g n))"
    let ?p_g = "λg. Mapping.Mapping (step.p_g g)"

    have u_g_is_u_g: "usesOf  ?u_g = step.u_g"
      by (subst usesOf_def [abs_def]) (intro ext; auto)
    have p_g_is_p_g: "(λg. Mapping.lookup (?p_g g)) = step.p_g" by simp

    interpret step: CFG_SSA_wf_code αe αn invar inEdges' Entry "defs" "λg. Mapping.Mapping (λn. if step.u_g g n = {} then None else Some (step.u_g g n))" "λg. Mapping.Mapping (step.p_g g)"
      apply (intro CFG_SSA_wf_code.intro CFG_SSA_code.intro)
      unfolding u_g_is_u_g p_g_is_p_g by intro_locales

    show "φ  uninst_code.triv_phis' (const (phis'_codem g next (substitution_code g next) nodes_of_phis)) g next (ssa.trivial_phis g) nodes_of_phis  φ  uninst_code.ssa.trivial_phis (const (phis'_codem g next (substitution_code g next) nodes_of_phis)) g"
    proof (cases "φ = next")
      case True
      hence "φ  uninst_code.triv_phis' (const (phis'_codem g next (substitution_code g next) nodes_of_phis)) g next (ssa.trivial_phis g) nodes_of_phis"
        unfolding uninst_code.triv_phis'_def by (auto split: option.splits)
      moreover
      from True have "φ  Mapping.keys (phis'_codem g next (substitution_code g next) nodes_of_phis)"
        unfolding phis'_codem_def
        by (transfer fixing: nodes_of_phis "next") (auto simp: fold_update_conv split: if_splits option.splits)
      hence "φ  uninst_code.ssa.trivial_phis (const (phis'_codem g next (substitution_code g next) nodes_of_phis)) g"
        unfolding uninst_code.ssa.trivial_phis_def by simp
      ultimately show ?thesis by simp
    next
      case False
      show ?thesis
      proof (cases "Mapping.lookup nodes_of_phis (snd next)")
        case None
        hence "uninst_code.triv_phis' (const (phis'_codem g next (substitution_code g next) nodes_of_phis)) g next (ssa.trivial_phis g) nodes_of_phis = ssa.trivial_phis g - {next}"
          unfolding uninst_code.triv_phis'_def by auto
        moreover from None
        have "uninst_code.ssa.trivial_phis (const (phis'_codem g next (substitution_code g next) nodes_of_phis)) g = ssa.trivial_phis g - {next}"
          unfolding phis'_codem_def uninst_code.ssa.trivial_phis_def by (auto simp: lookup_delete)
        ultimately show ?thesis by simp
      next
        case [simp]: (Some nodes)
        from assms(2) have "snd next  snd ` dom (Mapping.lookup (phis g))" by (auto simp: keys_dom_lookup)
        with assms(1) Some have "finite nodes" by (rule nodes_of_phis_finite)
        hence [simp]: "set (sorted_list_of_set nodes) = nodes" by simp
        obtain φ_node φ_val where [simp]: "φ = (φ_node, φ_val)" by (cases φ) auto
        show ?thesis
        proof (cases "φ  nodes")
          case False
          with φ  next have "φ  uninst_code.triv_phis' (const (phis'_codem g next (substitution_code g next) nodes_of_phis)) g next (ssa.trivial_phis g) nodes_of_phis  φ  ssa.trivial_phis g"
            unfolding uninst_code.triv_phis'_def by simp
          moreover

          from False φ  next have "...  φ  uninst_code.ssa.trivial_phis (const (phis'_codem g next (substitution_code g next) nodes_of_phis)) g"
            unfolding phis'_codem_def uninst_code.ssa.trivial_phis_def
            by (auto simp add: keys_dom_lookup dom_def lookup_delete)
          ultimately show ?thesis by simp
        next
          case True
          with assms(1,2) have "φ  Mapping.keys (phis g)"
            unfolding phi_equiv_mapping_def apply clarsimp
            apply (clarsimp simp: keys_dom_lookup)
            by (erule_tac x="next" in ballE) (auto split: option.splits if_splits)

          then obtain φ_args where [simp]: "Mapping.lookup (phis g) (φ_node, φ_val) = Some φ_args"
            unfolding keys_dom_lookup by auto
          hence [simp]: "ssa.phi g φ_val = Some φ_args"
            by (rule ssa.phis_phi)

          from True φ  next have "φ  uninst_code.triv_phis' (const (phis'_codem g next (substitution_code g next) nodes_of_phis)) g next (ssa.trivial_phis g) nodes_of_phis 
            φ  ssa.trivial_phis g  ssa.trivial_code (snd φ) (the (Mapping.lookup (phis'_codem g next (substitution_code g next) nodes_of_phis) φ))"
            unfolding uninst_code.triv_phis'_def by simp
          moreover

          from φ  next φ  Mapping.keys (phis g) next  Mapping.keys (phis g)
          have [simp]: "φ_val  snd next"
            unfolding keys_dom_lookup
            by (cases "next", cases φ) (auto dest: ssa.phis_disj)

          show ?thesis
          proof (cases "φ  ssa.trivial_phis g")
            case True
            hence "ssa.trivial_code φ_val φ_args"
              unfolding ssa.trivial_phis_def by clarsimp
            hence "ssa.trivial_code φ_val (map (substNext_code g next) φ_args)"
              apply (rule ssa.trivial_code_mapI)
               prefer 2
               apply (clarsimp simp: substNext_code_def)
              apply (clarsimp simp: substNext_code_def substitution_code_def)
              apply (erule_tac c="φ_val" in equalityCE)
               prefer 2 apply simp
              apply clarsimp
              apply (subgoal_tac "ssa.isTrivialPhi g φ_val (snd next)")
               apply (subgoal_tac "ssa.isTrivialPhi g (snd next) φ_val")
                apply (blast dest: isTrivialPhi_asymmetric)
               using assms(3) next  Mapping.keys (phis g)
               apply (clarsimp simp: ssa.trivial_def keys_dom_lookup)
               apply (frule isTrivial_the_trivial [rotated 1, where v="snd next"])
                apply -
                apply (rule ssa.phis_phi [where n="fst next"])
                apply simp
               apply simp
              apply (thin_tac "φ_val = v" for v)
              using ssa.trivial_code φ_val φ_args
              apply (clarsimp simp: ssa.trivial_code_def)
              by (erule the_trivial_SomeE) (auto simp: ssa.isTrivialPhi_def)
            with calculation True φ  next φ  nodes show ?thesis
              unfolding uninst_code.ssa.trivial_phis_def phis'_codem_def
              by (clarsimp simp: keys_dom_lookup substNext_code_alt_def)
          next
            case False
            with calculation φ  next φ  Mapping.keys (phis g) True show ?thesis
              unfolding phis'_codem_def uninst_code.ssa.trivial_phis_def
              by (auto simp: keys_dom_lookup triv_phis'_def ssa.trivial_code_def)
          qed
        qed
      qed
    qed
  qed

  lemma nodes_of_phis'_correct:
  assumes "g  nodes_of_phis φ ssa.phiNodes_of g"
    and "next  Mapping.keys (phis g)" and "ssa.trivial g (snd next)"
  shows "g  (nodes_of_phis' g next (substitution_code g next) nodes_of_phis) φ (uninst_code.ssa.phiNodes_of (const (phis'_codem g next (substitution_code g next) nodes_of_phis)) g)"
  proof -
    from assms(2) obtain next_args where lookup_next [simp]: "Mapping.lookup (phis g) next = Some next_args"
      unfolding keys_dom_lookup by auto
    hence phi_next [simp]: "ssa.phi g (snd next) = Some next_args"
      by -(rule ssa.phis_phi [where n="fst next"], simp)
    from assms(3) have in_next_args: "v. v  set next_args  v = snd next  v = substitution_code g next"
      unfolding ssa.trivial_def substitution_code_def
      apply clarsimp
      apply (subst(asm) isTrivial_the_trivial)
        apply (rule ssa.phis_phi [where g=g and n="fst next"])
        apply simp
       apply assumption
      by (auto simp: ssa.isTrivialPhi_def split: option.splits)
    from assms(2) have [dest!]: "x vs. Mapping.lookup (phis g) (x, snd next) = Some vs  x = fst next  vs = next_args"
      by (auto simp add: keys_dom_lookup dest: ssa.phis_disj [where n'="fst next"])
    show ?thesis
    apply (simp only: phi_equiv_mapping_def)
    apply (subgoal_tac "finite (dom (Mapping.lookup (phis'_codem g next (substitution_code g next) nodes_of_phis)))")
     prefer 2
     apply (subst dom_phis'_codem)
      apply (rule nodes_of_phis_finite [OF assms(1)], assumption)
      using assms(2) [simplified keys_dom_lookup]
      apply clarsimp
     apply (clarsimp simp: ssa.phis_finite split: option.splits)
     apply (rule nodes_of_phis_finite [OF assms(1)], assumption)
     using assms(2) [simplified keys_dom_lookup]
     apply clarsimp
    apply (simp_all only: phis'_codem_correct [OF assms(1,2)])
    apply (intro ballI)
    apply (rename_tac v)
    apply (subst(asm) ssa.keys_phidefNodes [OF ssa.phis_finite])
    apply (subst uninst_code.ssa.lookup_phiNodes_of, assumption)
    apply (subst lookup_phis'_code)+
    apply (subst substNext_code_def)+
    apply (subst dom_phis'_code)+
    apply (cases "φ  Mapping.keys (phis g). snd next  set (the (Mapping.lookup (phis g) φ))")
     apply (erule bexE)
     apply (subst(asm) keys_dom_lookup)
     apply (drule domD)
     apply (erule exE)
     apply (rule phi_equiv_mappingE [OF assms(1,2)], assumption)
      apply clarsimp
     apply (cases "substitution_code g next  snd ` Mapping.keys (phis g)")
      apply (cases "φ'  Mapping.keys (phis g). substitution_code g next  set (the (Mapping.lookup (phis g) φ'))")
       apply (erule bexE)
       apply (subst(asm) keys_dom_lookup)+
       apply (drule domD)
       apply (erule exE)
       apply (rule_tac x="φ'" in phi_equiv_mappingE' [OF assms(1)], assumption)
         apply simp
        apply (simp add: keys_dom_lookup)
       apply (case_tac "v = substitution_code g next")
        apply (simp only:)
        apply (subst lookup_nodes_of_phis'_subst)
        apply (simp add: lookup_phis'_code)
        apply (auto 4 4 intro: rev_image_eqI
          simp: keys_dom_lookup map_option_case substNext_code_def split: option.splits)[1]
       apply (subst lookup_nodes_of_phis'_not_subst, assumption)
       apply (case_tac "φv  Mapping.keys (phis g). v  set (the (Mapping.lookup (phis g) φv))")
        apply (erule bexE)
        apply (simp add: keys_dom_lookup)
        apply (drule domD)
        apply (erule exE)
        apply (rule_tac x="φv" in phi_equiv_mappingE' [OF assms(1)], assumption)
          apply simp
         apply (clarsimp simp: keys_dom_lookup)
        apply (clarsimp simp: keys_dom_lookup)
        apply (rename_tac n v φ_args n' v' n'' φ_args' φ_args'')
        apply (auto dest: in_next_args)[1]
        apply (erule_tac x="(n,v)" in ballE)
         prefer 2 apply (auto dest: in_next_args)[1]
        apply auto[1]
       using phi_equiv_mappingE2' [OF assms(1), rotated 1]
       apply (erule_tac x=v in meta_allE)
       apply (erule meta_impE)
        apply clarsimp
       apply (auto simp: keys_dom_lookup)[1]
        apply force
       apply force
      using phi_equiv_mappingE2' [OF assms(1), rotated 1]
      apply (erule_tac x="substitution_code g next" in meta_allE)
      apply (erule meta_impE)
       apply clarsimp
      apply (erule meta_impE)
       apply assumption
      apply (case_tac "v = substitution_code g next")
       apply (auto simp: keys_dom_lookup)[1]
            apply force
           apply force
          apply force
         apply force
        apply force
       apply force
      apply (subst lookup_nodes_of_phis'_not_subst, assumption)
      apply (case_tac "φv  Mapping.keys (phis g). v  set (the (Mapping.lookup (phis g) φv))")
       apply (erule bexE)
       apply (simp add: keys_dom_lookup)
       apply (drule domD)
       apply (erule exE)
       apply (rule_tac x="φv" in phi_equiv_mappingE' [OF assms(1)], assumption)
         apply simp
        apply (clarsimp simp: keys_dom_lookup)
       apply (auto simp: keys_dom_lookup dest: in_next_args)[1]
        apply (force dest: in_next_args)[1]
       apply (force dest: in_next_args)[1]
      using phi_equiv_mappingE2' [OF assms(1), rotated 1]
      apply (erule_tac x=v in meta_allE)
      apply (erule meta_impE)
       apply clarsimp
      apply (auto simp: keys_dom_lookup)[1]
         apply force
        apply force
       apply force
      apply force
     apply (case_tac "v = substitution_code g next")
      apply (auto simp: keys_dom_lookup)[1]
     apply (subst lookup_nodes_of_phis'_not_subst, assumption)
     apply (case_tac "φv  Mapping.keys (phis g). v  set (the (Mapping.lookup (phis g) φv))")
      apply (erule bexE)
      apply (simp add: keys_dom_lookup)
      apply (drule domD)
      apply (erule exE)
      apply (rule_tac x="φv" in phi_equiv_mappingE' [OF assms(1)], assumption)
        apply simp
       apply (clarsimp simp: keys_dom_lookup)
      apply (auto simp: keys_dom_lookup dest: in_next_args)[1]
      apply (force dest: in_next_args)[1]
     using phi_equiv_mappingE2' [OF assms(1), rotated 1]
     apply (erule_tac x="v" in meta_allE)
     apply (erule meta_impE)
      apply clarsimp
     apply (auto simp: keys_dom_lookup)[1]
      apply force
     apply force
    using phi_equiv_mappingE2' [OF assms(1), rotated 1]
    apply (erule_tac x="snd next" in meta_allE)
    apply (erule meta_impE)
     apply clarsimp
    apply (erule meta_impE)
     using assms(2)
     apply clarsimp
    apply (subgoal_tac "{n  Mapping.keys (phis g). snd next  set (the (Mapping.lookup (phis g) n))} = {}")
     prefer 2
     apply auto[1]
    apply (cases "substitution_code g next  snd ` Mapping.keys (phis g)")
     apply (cases "φ'  Mapping.keys (phis g). substitution_code g next  set (the (Mapping.lookup (phis g) φ'))")
      apply (erule bexE)
      apply (subst(asm) keys_dom_lookup)+
      apply (drule domD)
      apply (erule exE)
      apply (rule_tac x="φ'" in phi_equiv_mappingE' [OF assms(1)], assumption)
        apply simp
       apply (simp add: keys_dom_lookup)
      apply (case_tac "v = substitution_code g next")
       apply (auto simp: keys_dom_lookup; force)[1]
      apply (subst lookup_nodes_of_phis'_not_subst, assumption)
      apply (case_tac "φv  Mapping.keys (phis g). v  set (the (Mapping.lookup (phis g) φv))")
       apply (erule bexE)
       apply (simp add: keys_dom_lookup)
       apply (drule domD)
       apply (erule exE)
       apply (rule_tac x="φv" in phi_equiv_mappingE' [OF assms(1)], assumption)
         apply simp
        apply (clarsimp simp: keys_dom_lookup)
       apply (auto simp: keys_dom_lookup dest: in_next_args)[1]
        apply (force dest: in_next_args)[1]
       apply (force dest: in_next_args)[1]
      using phi_equiv_mappingE2' [OF assms(1), rotated 1]
      apply (erule_tac x=v in meta_allE)
      apply (erule meta_impE)
       apply clarsimp
      apply (auto simp: keys_dom_lookup; force)[1]
     using phi_equiv_mappingE2' [OF assms(1), rotated 1]
     apply (erule_tac x="substitution_code g next" in meta_allE)
     apply (erule meta_impE)
      apply clarsimp
     apply (erule meta_impE)
      apply assumption
     apply (case_tac "v = substitution_code g next")
      apply (auto simp: keys_dom_lookup; force)[1]
     apply (subst lookup_nodes_of_phis'_not_subst, assumption)
     apply (case_tac "φv  Mapping.keys (phis g). v  set (the (Mapping.lookup (phis g) φv))")
      apply (erule bexE)
      apply (simp add: keys_dom_lookup)
      apply (drule domD)
      apply (erule exE)
      apply (rule_tac x="φv" in phi_equiv_mappingE' [OF assms(1)], assumption)
        apply simp
       apply (clarsimp simp: keys_dom_lookup)
      apply (auto simp: keys_dom_lookup dest: in_next_args; force dest: in_next_args)[1]
     using phi_equiv_mappingE2' [OF assms(1), rotated 1]
     apply (erule_tac x="v" in meta_allE)
     apply (erule meta_impE)
      apply clarsimp
     apply (erule meta_impE)
      apply (clarsimp simp: keys_dom_lookup)
     apply (auto simp: keys_dom_lookup; force)[1]
    apply (case_tac "v = substitution_code g next")
     apply (auto simp: keys_dom_lookup)[1]
    apply (subst lookup_nodes_of_phis'_not_subst, assumption)
    apply (case_tac "φv  Mapping.keys (phis g). v  set (the (Mapping.lookup (phis g) φv))")
     apply (erule bexE)
     apply (simp add: keys_dom_lookup)
     apply (drule domD)
     apply (erule exE)
     apply (rule_tac x="φv" in phi_equiv_mappingE' [OF assms(1)], assumption)
       apply simp
      apply (clarsimp simp: keys_dom_lookup)
     apply (auto simp: keys_dom_lookup dest: in_next_args; force dest: in_next_args)[1]
    using phi_equiv_mappingE2' [OF assms(1), rotated 1]
    apply (erule_tac x=v in meta_allE)
    apply (erule meta_impE)
     apply clarsimp
    apply (erule meta_impE)
     apply (clarsimp simp: keys_dom_lookup)
    apply (auto simp: keys_dom_lookup; force)[1]
    done
  qed

  lemma nodes_of_uses'_correct:
  assumes "g  nodes_of_uses φ ssa.useNodes_of g"
    and "next  Mapping.keys (phis g)" and "ssa.trivial g (snd next)"
  shows "g  (nodes_of_uses' g next (substitution_code g next) (Mapping.keys (ssa.phidefNodes g)) nodes_of_uses) φ (uninst_code.ssa.useNodes_of (const (uses'_codem g next (substitution_code g next) nodes_of_uses)) g)"
  proof -
    from assms(2,3) ssa.phis_in_αn [of g "fst next" "snd next"]
    have "ssa.redundant g"
      unfolding ssa.redundant_def ssa.allVars_def ssa.allDefs_def ssa.phiDefs_def
      by (cases "next") (auto simp: keys_dom_lookup)

    then interpret step: CFG_SSA_step_code αe αn invar inEdges' Entry oldDefs oldUses "defs" "uses" phis var chooseNext_all
      by unfold_locales


    from assms(2,3) obtain next_args v where lookup_next [simp]: "Mapping.lookup (phis g) next = Some next_args"
      and "ssa.isTrivialPhi g (snd next) v"
      unfolding keys_dom_lookup ssa.trivial_def by auto
    hence phi_next [simp]: "ssa.phi g (snd next) = Some next_args"
      by -(rule ssa.phis_phi [where n="fst next"], simp)
    hence the_trivial_next_args [simp]: "the_trivial (snd next) next_args = Some v" using ssa.isTrivialPhi g (snd next) v
      by (rule isTrivial_the_trivial)

    from assms(3) have in_next_args: "v. v  set next_args  v = snd next  v = substitution_code g next"
      unfolding ssa.trivial_def substitution_code_def
      apply (clarsimp simp del: the_trivial_next_args)
      apply (subst(asm) isTrivial_the_trivial)
        apply (rule ssa.phis_phi [where g=g and n="fst next"])
        apply simp
       apply assumption
      by (auto simp: ssa.isTrivialPhi_def split: option.splits)

    from ssa.isTrivialPhi g (snd next) v
    have triv_phi_is_v [dest!]: "v'. ssa.isTrivialPhi g (snd next) v'  v' = v"
      using isTrivialPhi_det [OF assms(3)] by auto

    from ssa.isTrivialPhi g (snd next) v have [simp]: "v  snd next" unfolding ssa.isTrivialPhi_def by simp

    from assms(2) have [dest!]: "x vs. Mapping.lookup (phis g) (x, snd next) = Some vs  x = fst next  vs = next_args"
      by (auto simp add: keys_dom_lookup dest: ssa.phis_disj [where n'="fst next"])

    have [simp]: "(CFG_base.useNodes_of αn
              (const
                (CFG_SSA_Transformed_notriv_base.uses' αn defs (usesOf  uses)
                  (λg. Mapping.lookup (phis g)) cN g))
              g)
     = (CFG_base.useNodes_of αn
     ((usesOf  uses)
      (g := CFG_SSA_Transformed_notriv_base.uses' αn defs (usesOf  uses)
             (λg. Mapping.lookup (phis g)) cN g)) g)"
     unfolding uninst.useNodes_of_def uninst.addN_def [abs_def]
      by auto

    have substNext_idem [simp]: "v. substNext g (substNext g v) = substNext g v"
      unfolding substNext_def by (auto split: if_splits)

    from assms(1)
    have nodes_of_uses_eq_NoneD [elim_format, elim]: "v n args. Mapping.lookup nodes_of_uses v = None; Mapping.lookup (phis g) (n,v) = Some args 
       (n  set (αn g). vs. Mapping.lookup (uses g) n = Some vs  v  vs)"
       unfolding phi_equiv_mapping_def
     apply (clarsimp simp: ssa.lookup_useNodes_of split: option.splits if_splits)
     by (erule_tac x="(n,v)" in ballE) auto

    from assms(1)
    have nodes_of_uses_eq_SomeD [elim_format, elim]: "v nodes n args.  Mapping.lookup nodes_of_uses v = Some nodes; Mapping.lookup (phis g) (n,v) = Some args
       nodes = {n  set (αn g). vs. Mapping.lookup (uses g) n = Some vs  v  vs}"
      unfolding phi_equiv_mapping_def
    apply (clarsimp simp: ssa.lookup_useNodes_of split: option.splits if_splits)
    by (erule_tac x="(n,v)" in ballE) auto

    show ?thesis
    unfolding phi_equiv_mapping_def nodes_of_uses'_def substitution_code_def Let_def ssa.keys_phidefNodes [OF ssa.phis_finite]
    apply (subst o_def [where g="const g" for g])
    apply (subst uses'_codem_correct [OF assms(1,2), unfolded substitution_code_def])
    apply (subst uninst.lookup_useNodes_of')
     apply (clarsimp simp: uses'_code_def split: option.splits)
     apply (rule finite_imageI)
     using ssa.uses_finite [of g]
     apply (fastforce split: option.splits)[1]
    apply (cases "v  snd ` dom (Mapping.lookup (phis g))")
     prefer 2
     apply (force intro: rev_image_eqI simp: lookup_delete uninst_code.uses'_code_def substNext_code_def substitution_code_def split: option.splits)[1]
    apply (clarsimp simp: Mapping_lookup_map_default lookup_delete uses'_code_def substNext_code_def substitution_code_def)
    apply (rename_tac n n' v' phi_args phi_args')
    apply safe
                         apply (auto elim: nodes_of_uses_eq_SomeD [where n="fst next"]
                           nodes_of_uses_eq_NoneD [where n="fst next"] simp: phi_equiv_mapping_def split: option.splits)[13]

            using assms(1)
            apply (simp add: phi_equiv_mapping_def)
            apply (erule_tac x="(n,v)" in ballE)
             prefer 2 apply auto[1]
            apply (auto simp: ssa.lookup_useNodes_of split: option.splits)[1]

           apply (auto elim: nodes_of_uses_eq_SomeD [where n="fst next"]
             nodes_of_uses_eq_NoneD [where n="fst next"] split: option.splits)[1]

          using assms(1)
          apply (simp add: phi_equiv_mapping_def)
          apply (erule_tac x="(n,v)" in ballE)
           prefer 2 apply auto[1]
          apply (auto simp: ssa.lookup_useNodes_of split: option.splits)[1]

         apply (auto 4 3 elim: nodes_of_uses_eq_SomeD [where n="fst next"] split: option.splits)[4]

     using assms(1)
     apply (simp add: phi_equiv_mapping_def)
     apply (erule_tac x="(n',v')" in ballE)
      prefer 2 apply auto[1]
     apply (auto simp: ssa.lookup_useNodes_of split: option.splits)[1]

    by (auto split: option.splits)[1]
  qed

  definition[code]: "substAll_efficient g 
    let phiVals = Mapping.keys (ssa.phidefNodes g);
        u = uses g;
        p = phis g;
        tp = ssa.trivial_phis g;
        nou = ssa.useNodes_of g;
        nop = ssa.phiNodes_of g
    in
    while
    (λ((u,p),triv_phis,nodes_of_uses,nodes_of_phis). ¬ Set.is_empty triv_phis)
    (λ((u,p),triv_phis,nodes_of_uses,nodes_of_phis). let
        next = Max triv_phis;
        next' = uninst_code.substitution_code (const p) g next;
        (u',p') = uninst_code.step_codem (const u) (const p) g next next' nodes_of_uses nodes_of_phis;
        tp' = uninst_code.triv_phis' (const p') g next triv_phis nodes_of_phis;
        nou' = uninst_code.nodes_of_uses' g next next' phiVals nodes_of_uses;
        nop' = uninst_code.nodes_of_phis' g next next' nodes_of_phis
      in ((u', p'), tp', nou', nop'))
    ((u, p), tp, nou, nop)"

  abbreviation "u_c x  const (usesOf (fst x))"
  abbreviation "p_c x  const (Mapping.lookup (snd x))"
  abbreviation "u g x  u_g g (fst x)"
  abbreviation "p g x  p_g g (snd x)"

  lemma usesOf_upd [simp]: "(usesOf  u g s1)(g := usesOf us) = usesOf  u_g g us"
    by (auto simp: fun_upd_apply usesOf_def [abs_def] split: option.splits if_splits)

  lemma keys_uses'_codem [simp]: "Mapping.keys (uses'_codem g next (substitution_code g next) (ssa.useNodes_of g)) = Mapping.keys (uses g)"
    unfolding uses'_codem_def
  apply (transfer fixing: g)
  apply (auto split: option.splits if_splits simp: fold_update_conv)
  by (subst(asm) sorted_list_of_set) (auto intro: finite_subset [OF _ finite_set])

  lemma keys_uses'_codem': " g  nodes_of_uses φ ssa.useNodes_of g; next  Mapping.keys (phis g) 
     Mapping.keys (uses'_codem g next (substitution_code g next) nodes_of_uses) = Mapping.keys (uses g)"
    unfolding uses'_codem_def
  apply (clarsimp simp: keys_dom_lookup split: if_splits option.splits)
  apply (auto simp: phi_equiv_mapping_def)
  by (erule_tac x="next" in ballE) (auto simp: ssa.lookup_useNodes_of split: if_splits option.splits)

  lemma triv_phis_base [simp]: "uninst_code.ssa.trivial_phis (const (phis g)) g = ssa.trivial_phis g"
    unfolding uninst_code.ssa.trivial_phis_def ..
  lemma useNodes_of_base [simp]: "uninst_code.ssa.useNodes_of (const (uses g)) g = ssa.useNodes_of g"
    unfolding uninst_code.ssa.useNodes_of_def uninst_code.ssa.addN_def [abs_def] mmap_def Mapping.map_default_def [abs_def] Mapping.default_def
    unfolding usesOf_def [abs_def]
    by transfer auto

  lemma phiNodes_of_base [simp]: "uninst_code.ssa.phiNodes_of (const (phis g)) g = ssa.phiNodes_of g"
    unfolding uninst_code.ssa.phiNodes_of_def uninst_code.ssa.phis_addN_def [abs_def] mmap_def Mapping.map_default_def [abs_def] Mapping.default_def
    by transfer auto

  lemma phi_equiv_mapping_refl [simp]: "uninst_code.phi_equiv_mapping ph g m m"
    unfolding uninst_code.phi_equiv_mapping_def by simp

  lemma substAll_efficient_code [code]:
    "substAll g = map_prod usesOf Mapping.lookup (fst (substAll_efficient g))"
    unfolding substAll_efficient_def while_def substAll_def Let_def
  apply -
  apply (rule map_option_the [OF _ substAll_terminates])
  proof (rule while_option_sim [where
      R="λx y. y = map_option (λa. map_prod usesOf Mapping.lookup (fst (f a))) x" and
      I="λ((u,p),triv_phis,nodes_of_uses, phis_of_nodes). Mapping.keys u  set (αn g)  Mapping.keys p  Mapping.keys (phis g)
         CFG_SSA_Transformed_notriv_linorder_code αe αn invar inEdges' Entry oldDefs oldUses defs (uses(g:=u)) (phis(g:=p)) var chooseNext_all
         triv_phis = uninst_code.ssa.trivial_phis (const p) g
         uninst_code.phi_equiv_mapping (const p) g nodes_of_uses (uninst_code.ssa.useNodes_of (const u) g)
         uninst_code.phi_equiv_mapping (const p) g phis_of_nodes (uninst_code.ssa.phiNodes_of (const p) g)"
      for f
      , simplified], simp_all add: split_def dom_uses_in_graph Set.is_empty_def)
    show "CFG_SSA_Transformed_notriv_linorder_code αe αn invar inEdges' Entry oldDefs oldUses defs uses phis var
     chooseNext_all"
      by unfold_locales
  next
    fix s1
    assume "Mapping.keys (fst (fst s1))  set (αn g)  Mapping.keys (snd (fst s1))  Mapping.keys (phis g)
       CFG_SSA_Transformed_notriv_linorder_code αe αn invar inEdges' Entry oldDefs oldUses defs (u g (fst s1)) (p g (fst s1)) var chooseNext_all
       fst (snd s1) = uninst_code.ssa.trivial_phis (const (snd (fst s1))) g
       uninst_code.phi_equiv_mapping (const (snd (fst s1))) g (fst (snd (snd s1))) (uninst_code.ssa.useNodes_of (const (fst (fst s1))) g)
       uninst_code.phi_equiv_mapping (const (snd (fst s1))) g (snd (snd (snd s1))) (uninst_code.ssa.phiNodes_of (const (snd (fst s1))) g)"
    then obtain s1_uses s1_phis s1_triv_phis s1_nodes_of_uses s1_phi_nodes_of where
      [simp]: "s1 = ((s1_uses, s1_phis), s1_triv_phis, s1_nodes_of_uses, s1_phi_nodes_of)"
      and "Mapping.keys s1_uses  set (αn g)"
      and "Mapping.keys s1_phis  Mapping.keys (phis g)"
      and "CFG_SSA_Transformed_notriv_linorder_code αe αn invar inEdges' Entry oldDefs oldUses defs (u_g g s1_uses) (p_g g s1_phis) var chooseNext_all"
      and [simp]: "s1_triv_phis = uninst_code.ssa.trivial_phis (const s1_phis) g"
      and nou_equiv: "uninst_code.phi_equiv_mapping (const s1_phis) g s1_nodes_of_uses (uninst_code.ssa.useNodes_of (const s1_uses) g)"
      and pno_equiv: "uninst_code.phi_equiv_mapping (const s1_phis) g s1_phi_nodes_of (uninst_code.ssa.phiNodes_of (const s1_phis) g)"
      by (cases s1; auto)
    from this(4) interpret i: CFG_SSA_Transformed_notriv_linorder_code αe αn invar inEdges' Entry oldDefs oldUses "defs" "u_g g s1_uses" "p_g g s1_phis" var chooseNext_all .
    let ?s2 = "map_prod usesOf Mapping.lookup (fst s1)"
    have [simp]: "uninst_code.ssa.trivial_phis (const s1_phis) g  {}  cond g ?s2"
      unfolding uninst_code.ssa.redundant_code_def [symmetric]
      by (clarsimp simp add: cond_def i.ssa.redundant_code [simplified, symmetric] CFG_SSA_wf_base.CFG_SSA_wf_defs)
    thus "uninst_code.ssa.trivial_phis (const (snd (fst s1))) g  {}  cond g ?s2"
      by simp
    {
      assume "uninst_code.ssa.trivial_phis (const (snd (fst s1))) g  {}"
      hence red: "uninst.redundant (usesOf  u_g g s1_uses) (λg'. Mapping.lookup (p_g g s1_phis g')) g"
        by (simp add: cond_def uninst.CFG_SSA_wf_defs)
      then interpret step: CFG_SSA_step_code αe αn invar inEdges' Entry oldDefs oldUses "defs"
        "u_g g s1_uses" "p_g g s1_phis" var chooseNext_all g
        by unfold_locales simp
      from step.step_CFG_SSA_Transformed_notriv[simplified]
      interpret step_step: CFG_SSA_Transformed_notriv αe αn invar inEdges' Entry oldDefs oldUses "defs"
      "(usesOf  u_g g s1_uses)(g := uninst.uses' (usesOf  u_g g s1_uses) (λg'. Mapping.lookup (p_g g s1_phis g')) g)"
      "(λg'. Mapping.lookup (p_g g s1_phis g'))(g := uninst.phis' (usesOf  u_g g s1_uses) (λg'. Mapping.lookup (p_g g s1_phis g')) g)"
      var i.cN .

      interpret step_step: CFG_SSA_ext αe αn invar inEdges' Entry "defs"
      "(usesOf  u_g g s1_uses)(g := uninst.uses' (usesOf  (u_g g s1_uses)) (λg'. Mapping.lookup (p_g g s1_phis g')) g)"
      "(λg'. Mapping.lookup (p_g g s1_phis g'))(g := uninst.phis' (usesOf  u_g g s1_uses) (λg'. Mapping.lookup (p_g g s1_phis g')) g)"
      ..

      from Mapping.keys s1_uses  set (αn g)
      have keys_u_g: "Mapping.keys (u_g g s1_uses g)  set (αn g)"
        by clarsimp

      have "Max (CFG_SSA_wf_base_code.trivial_phis (p_g g s1_phis) g) = chooseNext_all (usesOf (u_g g s1_uses g)) (p_g g s1_phis g) g"
      apply (rule chooseNext_all_code [where u="u_g g s1_uses", symmetric])
      by unfold_locales (simp add: i.ssa.redundant_code [symmetric])

      hence [simp]: "Max (CFG_SSA_wf_base_code.trivial_phis (const s1_phis) g) = chooseNext_all (usesOf s1_uses) s1_phis g"
        by (simp add: uninst_code.ssa.trivial_phis_def)

      have [simp]: "chooseNext_all (usesOf s1_uses) s1_phis g  Mapping.keys s1_phis"
        using i.chooseNext' [of g]
        by (clarsimp simp: Mapping.keys_dom_lookup)

      have [simp]: "uninst_code.ssa.useNodes_of (const s1_uses) g = uninst_code.ssa.useNodes_of (u_g g s1_uses) g"
        unfolding uninst_code.ssa.useNodes_of_def
        unfolding uninst_code.ssa.addN_def [abs_def]
        by simp

      have [simp]: "uninst_code.ssa.phiNodes_of (const s1_phis) g = uninst_code.ssa.phiNodes_of (p_g g s1_phis) g"
        unfolding uninst_code.ssa.phiNodes_of_def
        unfolding uninst_code.ssa.phis_addN_def [abs_def]
        by simp

      from Mapping.keys s1_phis  Mapping.keys (phis g)
      have "finite (Mapping.keys s1_phis)"
      by (rule finite_subset) (auto simp: keys_dom_lookup intro: ssa.phis_finite)

      hence [simp]: "uninst_code.phi_equiv_mapping (const s1_phis) g = uninst_code.phi_equiv_mapping (p_g g s1_phis) g"
        apply (intro ext)
        apply (clarsimp simp: uninst_code.phi_equiv_mapping_def)
        apply (subst uninst.keys_phidefNodes)
         apply (simp add: keys_dom_lookup)
        by clarsimp

      have uses_conv: "(usesOf 
          u_g g
           (CFG_SSA_Transformed_notriv_base_code.uses'_codem (u_g g s1_uses)
             g (chooseNext_all (usesOf s1_uses) s1_phis g)
             (uninst_code.substitution_code (p_g g s1_phis) g (chooseNext_all (usesOf s1_uses) s1_phis g))
             s1_nodes_of_uses))
                  = ((usesOf  u_g g s1_uses)
       (g := CFG_SSA_Transformed_notriv_base.uses' αn defs (usesOf  u_g g s1_uses) (λga. Mapping.lookup (p_g g s1_phis ga))
              i.cN g))"
       unfolding i.uses'_code_correct [OF red]
       apply (subst i.uses'_codem_correct [symmetric, where nodes_of_uses=s1_nodes_of_uses])
         apply (rule nou_equiv [simplified])
        apply auto[1]
       by (auto simp: fun_upd_apply)

      have phis_conv: "(λga. Mapping.lookup
                (p_g g (CFG_SSA_Transformed_notriv_base_code.phis'_codem (p_g g s1_phis) g
                         (chooseNext_all (usesOf s1_uses) s1_phis g)
                         (uninst_code.substitution_code (p_g g s1_phis) g (chooseNext_all (usesOf s1_uses) s1_phis g))
                         (CFG_SSA_base.phiNodes_of (λga. Mapping.lookup (p_g g s1_phis ga)) g))
                  ga)) =
       (λga. Mapping.lookup (p_g g s1_phis ga))
       (g := CFG_SSA_Transformed_notriv_base.phis' αn defs (usesOf  u_g g s1_uses) (λga. Mapping.lookup (p_g g s1_phis ga))
              i.cN g)"
       apply (subst i.phis'_code_correct [OF red])
       apply (subst i.phis'_codem_correct [symmetric])
       by (auto simp: fun_upd_apply)

      have [simp]: "uninst_code.substitution_code (const s1_phis) g = uninst_code.substitution_code (p_g g s1_phis) g"
        by (intro ext) (clarsimp simp: uninst_code.substitution_code_def)

      let ?next = "Max (uninst_code.ssa.trivial_phis (const (snd (fst s1))) g)"
      let ?u' = "fst (uninst_code.step_codem (u g (fst s1)) (p g (fst s1)) g ?next (uninst_code.substitution_code (const (snd (fst s1))) g ?next) (fst (snd (snd s1))) (snd (snd (snd s1))))"
      let ?p' = "snd (uninst_code.step_codem (u g (fst s1)) (p g (fst s1)) g ?next (uninst_code.substitution_code (const (snd (fst s1))) g ?next) (fst (snd (snd s1))) (snd (snd (snd s1))))"

      show step_s2: "step g ?s2 = map_prod usesOf Mapping.lookup (uninst_code.step_codem (u g (fst s1)) (p g (fst s1)) g
        ?next (uninst_code.substitution_code (const (snd (fst s1))) g ?next)
        (fst (snd (snd s1))) (snd (snd (snd s1))))"
        unfolding uninst_code.step_codem_def uninst.step_def split_def map_prod_def Let_def
      apply (auto simp: map_prod_def Let_def step_step.usesOf_cache[of g, simplified]
        i.phis'_codem_correct [OF pno_equiv [simplified]]
        i.phis'_code_correct[simplified, OF red, simplified, symmetric]
        i.uses'_codem_correct [OF nou_equiv [simplified]]
        i.uses'_code_correct [OF red, symmetric, simplified])
       apply (subst uninst.uses'_def [abs_def])+
       apply (clarsimp simp: uninst.substNext_def uninst.substitution_def CFG_SSA_wf_base.CFG_SSA_wf_defs)
      apply (subst uninst.phis'_def [abs_def])+
      by (clarsimp simp: uninst.substNext_def [abs_def] uninst.substitution_def CFG_SSA_wf_base.CFG_SSA_wf_defs cong: if_cong option.case_cong)

      have [simplified, simp]:
        "uninst_code.phis'_codem (p g (fst s1)) g ?next (uninst_code.substitution_code (const (snd (fst s1))) g ?next) s1_phi_nodes_of
          = uninst_code.phis'_codem (p g (fst s1)) g ?next (uninst_code.substitution_code (const (snd (fst s1))) g ?next) (uninst_code.ssa.phiNodes_of (const (snd (fst s1))) g)"
        by (auto simp: i.phis'_codem_correct [OF phi_equiv_mapping_refl] i.phis'_codem_correct [OF pno_equiv [simplified]])

      have [simplified, simp]:
        "usesOf (uninst_code.uses'_codem (u g (fst s1)) g ?next (uninst_code.substitution_code (const (snd (fst s1))) g ?next) s1_nodes_of_uses)
          = usesOf (uninst_code.uses'_codem (u g (fst s1)) g ?next (uninst_code.substitution_code (const (snd (fst s1))) g ?next) (uninst_code.ssa.useNodes_of (const (fst (fst s1))) g))"
        by (auto simp: i.uses'_codem_correct [OF phi_equiv_mapping_refl] i.uses'_codem_correct [OF nou_equiv [simplified]])

      from step_s2[symmetric] step.step_CFG_SSA_Transformed_notriv Mapping.keys s1_uses  set (αn g)
        Mapping.keys s1_phis  Mapping.keys (phis g)
      have "Mapping.keys ?u'  set (αn g) 
          Mapping.keys ?p'  Mapping.keys (phis g) 
          CFG_SSA_Transformed_notriv_linorder_code αe αn invar inEdges' Entry oldDefs oldUses defs
           (u g (uninst_code.step_codem (u g (fst s1)) (p g (fst s1)) g ?next (uninst_code.substitution_code (const (snd (fst s1))) g ?next) s1_nodes_of_uses s1_phi_nodes_of))
           (p g (uninst_code.step_codem (u g (fst s1)) (p g (fst s1)) g ?next (uninst_code.substitution_code (const (snd (fst s1))) g ?next) s1_nodes_of_uses s1_phi_nodes_of))
           var chooseNext_all"
      unfolding CFG_SSA_Transformed_notriv_linorder_code_def
        CFG_SSA_Transformed_notriv_linorder_def
        CFG_SSA_Transformed_code_def
        CFG_SSA_wf_code_def CFG_SSA_code_def
      apply (clarsimp simp: map_prod_def split_def uninst_code.step_codem_def Let_def uses_conv phis_conv)
      apply (rule conjI)
       prefer 2
       apply (rule conjI)
        prefer 2
        apply auto[1]
        apply unfold_locales
        apply (rename_tac g')
        apply (case_tac "g  g'")
        by (auto intro!: dom_uses_in_graph chooseNext_all_code
          simp: fun_upd_apply
            i.keys_phis'_codem' [OF pno_equiv [simplified], of ?next, simplified fun_upd_apply, simplified]
            i.keys_uses'_codem' [OF nou_equiv [simplified], of ?next, simplified fun_upd_apply, simplified])
      moreover

      have [simp]: "uninst_code.ssa.trivial_phis (p_g g s1_phis) g = uninst_code.ssa.trivial_phis (const s1_phis) g"
        unfolding uninst_code.ssa.trivial_phis_def uninst_code.ssa.trivial_code_def
        by clarsimp

      from i.triv_phis'_correct [of g "snd (snd (snd s1))" ?next] i.chooseNext' [of g]
      have "uninst_code.triv_phis' (const ?p') g ?next s1_triv_phis (snd (snd (snd s1)))
        = uninst_code.ssa.trivial_phis (const ?p') g"
        by (auto intro: pno_equiv [simplified] simp: uninst_code.step_codem_def)
      moreover

      from Mapping.keys s1_phis  Mapping.keys (phis g) ssa.phis_finite
      have "finite (dom (Mapping.lookup s1_phis))"
        by (auto intro: finite_subset simp: keys_dom_lookup)
      hence phi_equiv_mapping_p'I [simplified]:
      "m1 m2. uninst_code.phi_equiv_mapping (const s1_phis) g m1 m2  uninst_code.phi_equiv_mapping (const ?p') g m1 m2"
        unfolding uninst_code.phi_equiv_mapping_def
        apply clarsimp
        apply (subst(asm) uninst.keys_phidefNodes)
         apply simp
        apply (subst(asm) uninst.keys_phidefNodes)
         apply (simp add: uninst_code.step_codem_def keys_dom_lookup [symmetric])
        by (clarsimp simp: uninst_code.step_codem_def keys_dom_lookup [symmetric]) fastforce

      have "?next  Mapping.keys s1_phis" by auto
      with Mapping.keys s1_phis  Mapping.keys (phis g) nou_equiv i.chooseNext' [of g]
      have "uninst_code.nodes_of_uses' g ?next (uninst_code.substitution_code (const (snd (fst s1))) g ?next) (snd ` dom (Mapping.lookup (phis g))) (fst (snd (snd s1)))
        = uninst_code.nodes_of_uses' g ?next (uninst_code.substitution_code (const (snd (fst s1))) g ?next) (snd ` dom (Mapping.lookup s1_phis)) (fst (snd (snd s1)))"
        unfolding uninst_code.nodes_of_uses'_def
        apply -
        apply (erule meta_impE)
         apply auto[1]
        apply (auto simp: Let_def uninst_code.substitution_code_def keys_dom_lookup uninst_code.ssa.trivial_def)
        apply (drule i.isTrivial_the_trivial [rotated 1])
         apply (rule i.ssa.phis_phi [where n="fst ?next"])
         apply simp
        apply clarsimp
        apply (drule i.ssa.allVars_in_allDefs)
        apply clarsimp
        apply (drule ssa.phis_phi)
        apply clarsimp
        apply (clarsimp simp: uninst_code.ssa.allVars_def uninst_code.ssa.allDefs_def uninst_code.ssa.allUses_def uninst_code.ssa.phiDefs_def)
        apply (erule disjE)
         apply (drule(1) ssa.simpleDef_not_phi)
         apply simp
        by (auto intro: rev_image_eqI)

      ultimately
      show "Mapping.keys ?u'  set (αn g) 
          Mapping.keys ?p'  Mapping.keys (phis g) 
          CFG_SSA_Transformed_notriv_linorder_code αe αn invar inEdges' Entry oldDefs oldUses defs
           (u g (uninst_code.step_codem (u g (fst s1)) (p g (fst s1)) g (Max (uninst_code.ssa.trivial_phis (const (snd (fst s1))) g)) (uninst_code.substitution_code (const (snd (fst s1))) g ?next) (fst (snd (snd s1))) (snd (snd (snd s1)))))
           (p g (uninst_code.step_codem (u g (fst s1)) (p g (fst s1)) g (Max (uninst_code.ssa.trivial_phis (const (snd (fst s1))) g)) (uninst_code.substitution_code (const (snd (fst s1))) g ?next) (fst (snd (snd s1))) (snd (snd (snd s1)))))
           var chooseNext_all 
          uninst_code.triv_phis' (const ?p') g ?next (uninst_code.ssa.trivial_phis (const (snd (fst s1))) g) (snd (snd (snd s1)))
            = uninst_code.ssa.trivial_phis (const ?p') g 
          uninst_code.phi_equiv_mapping (const ?p') g (uninst_code.nodes_of_uses' g ?next (uninst_code.substitution_code (const (snd (fst s1))) g ?next) (snd ` dom (Mapping.lookup (phis g))) (fst (snd (snd s1)))) (uninst_code.ssa.useNodes_of (const ?u') g) 
          uninst_code.phi_equiv_mapping (const ?p') g (uninst_code.nodes_of_phis' g ?next (uninst_code.substitution_code (const (snd (fst s1))) g ?next) (snd (snd (snd s1)))) (uninst_code.ssa.phiNodes_of (const ?p') g)"
      using i.nodes_of_uses'_correct [of g s1_nodes_of_uses ?next, OF nou_equiv [simplified]]
        i.chooseNext' [of g]
        i.nodes_of_phis'_correct [of g s1_phi_nodes_of ?next, OF pno_equiv [simplified]]
        apply simp
        apply (rule conjI)
         apply (rule phi_equiv_mapping_p'I)
         apply (clarsimp simp: uninst_code.step_codem_def)
        apply (rule phi_equiv_mapping_p'I)
        by (clarsimp simp: uninst_code.step_codem_def)
    }
  qed

end

end