Session Formal_SSA

Theory FormalSSA_Misc

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

section ‹Prelude›

subsection ‹Miscellaneous Lemmata›

theory FormalSSA_Misc
imports Main "HOL-Library.Sublist"
begin

lemma length_1_last_hd: "length ns = 1  last ns = hd ns"
  by (metis One_nat_def append.simps(1) append_butlast_last_id diff_Suc_Suc diff_zero length_0_conv length_butlast list.sel(1) zero_neq_one)

lemma not_in_butlast[simp]: "x  set ys; x  set (butlast ys)  x = last ys"
  apply (cases "ys = []")
   apply simp
  apply (subst(asm) append_butlast_last_id[symmetric])
  by (simp_all del:append_butlast_last_id)

lemma in_set_butlastI: "x  set xs  x  last xs  x  set (butlast xs)"
  by (metis append_butlast_last_id append_is_Nil_conv list.distinct(1) rotate1.simps(2) set_ConsD set_rotate1 split_list)

lemma butlast_strict_prefix: "xs  []  strict_prefix (butlast xs) xs"
  by (metis append_butlast_last_id strict_prefixI')

lemma set_tl: "set (tl xs)  set xs"
  by (metis set_mono_suffix suffix_tl)

lemma in_set_tlD[elim]: "x  set (tl xs)  x  set xs"
  using set_tl[of xs] by auto

lemma suffix_unsnoc:
  assumes "suffix xs ys" "xs  []"
  obtains x where "xs = butlast xs@[x]" "ys = butlast ys@[x]"
  by (metis append_butlast_last_id append_is_Nil_conv assms(1) assms(2) last_appendR suffix_def)

lemma prefix_split_first:
  assumes "x  set xs"
  obtains as where "prefix (as@[x]) xs" and "x  set as"
proof atomize_elim
  from assms obtain as bs where "xs = as@x#bs  x  set as" by (atomize_elim, rule split_list_first)
  thus "as. prefix (as@[x]) xs  x  set as" by -(rule exI[where x = as], auto)
qed

lemma in_prefix[elim]:
  assumes "prefix xs ys" and "x  set xs"
  shows "x  set ys"
using assms by (auto elim!:prefixE)

lemma strict_prefix_butlast:
  assumes "prefix xs (butlast ys)" "ys  []"
  shows "strict_prefix xs ys"
using assms unfolding append_butlast_last_id[symmetric] by (auto simp add:less_le butlast_strict_prefix prefix_order.le_less_trans)

lemma prefix_tl_subset: "prefix xs ys  set (tl xs)  set (tl ys)"
  by (metis Nil_tl prefix_bot.extremum prefix_def set_mono_prefix tl_append2)

lemma suffix_tl_subset: "suffix xs ys  set (tl xs)  set (tl ys)"
  by (metis append_Nil suffix_def set_mono_suffix suffix_tl suffix_order.order_trans tl_append2)

lemma set_tl_append': "set (tl (xs @ ys))  set (tl xs)  set ys"
  by (metis list.sel(2) order_refl set_append set_mono_suffix suffix_tl tl_append2)

lemma last_in_tl: "length xs > 1  last xs  set (tl xs)"
  by (metis One_nat_def diff_Suc_Suc last_in_set last_tl length_tl less_numeral_extra(4) list.size(3) zero_less_diff)

lemma concat_join: "xs  []  ys  []  last xs = hd ys  butlast xs@ys = xs@tl ys"
  by (induction xs, auto)

lemma fold_induct[case_names Nil Cons]: "P s  (x s. x  set xs  P s  P (f x s))  P (fold f xs s)"
by (rule fold_invariant [where Q = "λx. x  set xs"]) simp

lemma fold_union_elem:
  assumes "x  fold (∪) xss xs"
  obtains ys where "x  ys" "ys  set xss  {xs}"
using assms
by (induction rule:fold_induct) auto

lemma fold_union_elemI:
  assumes "x  ys" "ys  set xss  {xs}"
  shows "x  fold (∪) xss xs"
using assms
by (metis Sup_empty Sup_insert Sup_set_fold Un_insert_right UnionI ccpo_Sup_singleton fold_simps(2) list.simps(15))

lemma fold_union_elemI':
  assumes "x  xs  (xs  set xss. x  xs)"
  shows "x  fold (∪) xss xs"
using assms
using fold_union_elemI by fastforce

lemma fold_union_finite[intro!]:
  assumes "finite xs" "xs  set xss. finite xs"
  shows "finite (fold (∪) xss xs)"
using assms by - (rule fold_invariant, auto)

lemma in_set_zip_map:
  assumes "(x,y)  set (zip xs (map f ys))"
  obtains y' where "(x,y')  set (zip xs ys)" "f y' = y"
proof-
  from assms obtain i where "x = xs ! i" "y = map f ys ! i" "i < length xs" "i < length ys" by (auto simp:set_zip)
  thus thesis by - (rule that[of "ys ! i"], auto simp:set_zip)
qed

lemma dom_comp_subset: "g ` dom (f  g)  dom f"
by (auto simp add:dom_def)

lemma finite_dom_comp:
  assumes "finite (dom f)" "inj_on g (dom (f  g))"
  shows "finite (dom (f  g))"
proof (rule finite_imageD)
  have "g ` dom (f  g)  dom f" by auto
  with assms(1) show "finite (g ` dom (f  g))" by - (rule finite_subset)
qed (simp add:assms(2))

lemma the1_list: "∃!x  set xs. P x  (THE x. x  set xs  P x) = hd (filter P xs)"
proof (induction xs)
  case (Cons y xs)
  let ?Q = "λxs x. x  set xs  P x"
  from Cons.prems obtain x where x: "?Q (y#xs) x" by auto
  have "x = hd (filter P (y#xs))"
  proof (cases "x=y")
    case True
    with x show ?thesis by auto
  next
    case False
    with Cons.prems x have 1: "∃!x. x  set xs  P x" by auto
    hence "(THE x. x  set xs  P x) = x" using x False by - (rule the1_equality, auto)
    also from 1 have "(THE x. x  set xs  P x) = hd (filter P xs)" by (rule Cons.IH)
    finally show ?thesis using False x Cons.prems by auto
  qed
  thus ?case using x by - (rule the1_equality[OF Cons.prems], auto)
qed auto

lemma set_zip_leftI:
  assumes "length xs = length ys"
  assumes "y  set ys"
  obtains x where "(x,y)  set (zip xs ys)"
proof-
  from assms(2) obtain i where "y = ys ! i" "i < length ys" by (metis in_set_conv_nth)
  with assms(1) show thesis by - (rule that[of "xs ! i"], auto simp add:set_zip)
qed

lemma butlast_idx:
  assumes "y  set (butlast xs)"
  obtains i where "xs ! i = y" "i < length xs - 1"
apply atomize_elim
using assms proof (induction xs arbitrary:y)
  case (Cons x xs)
  from Cons.prems have[simp]: "xs  []" by (simp split:if_split_asm)
  show ?case
  proof (cases "y = x")
    case True
    show ?thesis by (rule exI[where x=0], simp_all add:True)
  next
    case False
    with Cons.prems have "y  set (butlast xs)" by simp
    from Cons.IH[OF this] obtain i where "y = xs ! i" and "i < length xs - 1" by auto
    thus ?thesis by - (rule exI[where x="Suc i"], simp)
  qed
qed simp

lemma butlast_idx':
  assumes "xs ! i = y" "i < length xs - 1" "length xs > 1"
  shows "y  set (butlast xs)"
using assms proof (induction xs arbitrary:i)
  case (Cons x xs)
  show ?case
  proof (cases i)
    case 0
    with Cons.prems(1,3) show ?thesis by simp
  next
    case (Suc j)
    with Cons.prems(1)[symmetric] Cons.prems(2,3) have "y  set (butlast xs)" by - (rule Cons.IH, auto)
    with Cons.prems(3) show ?thesis by simp
  qed
qed simp

lemma card_eq_1_singleton:
  assumes "card A = 1"
  obtains x where "A = {x}"
using assms[simplified] by - (drule card_eq_SucD, auto)

lemma set_take_two:
  assumes "card A  2"
  obtains x y where "x  A" "y  A" "x  y"
proof-
  from assms obtain k where "card A = Suc (Suc k)"
    by (auto simp: le_iff_add)
  from card_eq_SucD[OF this] obtain x B where x: "A = insert x B" "x  B" "card B = Suc k" by auto
  from card_eq_SucD[OF this(3)] obtain y where y: "y  B" by auto
  from x y show ?thesis by - (rule that[of x y], auto)
qed

lemma singleton_list_hd_last: "length xs = 1  hd xs = last xs"
  by (metis One_nat_def impossible_Cons last.simps length_0_conv less_nat_zero_code list.sel(1) nat_less_le neq_Nil_conv not_less_eq_eq)

lemma distinct_hd_tl: "distinct xs  hd xs  set (tl xs)"
  by (metis distinct.simps(2) hd_Cons_tl in_set_member list.sel(2) member_rec(2))

lemma set_mono_strict_prefix: "strict_prefix xs ys  set xs  set (butlast ys)"
  by (metis append_butlast_last_id strict_prefixE strict_prefix_simps(1) prefix_snoc set_mono_prefix)

lemma set_butlast_distinct: "distinct xs  set (butlast xs)  {last xs} = {}"
  by (metis append_butlast_last_id butlast.simps(1) distinct_append inf_bot_right inf_commute list.set(1) set_simps(2))

lemma disjoint_elem[elim]: "A  B = {}  x  A  x  B" by auto

lemma prefix_butlastD[elim]: "prefix xs (butlast ys)  prefix xs ys"
  using strict_prefix_butlast by fastforce

lemma butlast_prefix: "prefix xs ys  prefix (butlast xs) (butlast ys)"
  by (induction xs ys rule: list_induct2'; auto)

lemma hd_in_butlast: "length xs > 1  hd xs  set (butlast xs)"
  by (metis butlast.simps(2) dual_order.strict_iff_order hd_Cons_tl hd_in_set length_greater_0_conv length_tl less_le_trans list.distinct(1) list.sel(1) neq0_conv zero_less_diff)

lemma nonsimple_length_gt_1: "xs  []  hd xs  last xs  length xs > 1"
  by (metis length_0_conv less_one nat_neq_iff singleton_list_hd_last)

lemma set_hd_tl: "xs  []  set [hd xs]  set (tl xs) = set xs"
  by (metis inf_sup_aci(5) rotate1_hd_tl set_append set_rotate1)

lemma fold_update_conv:
  "fold (λn m. m(n  g n)) xs m x =
  (if (x  set xs) then Some (g x) else m x)"
  by (induction xs arbitrary: m) auto

lemmas removeAll_le = length_removeAll_less_eq

lemmas removeAll_less [intro] = length_removeAll_less

lemma removeAll_induct:
  assumes "xs. (x. x  set xs  P (removeAll x xs))  P xs"
  shows "P xs"
by (induct xs rule:length_induct, rule assms) auto

lemma The_Min: "Ex1 P  The P = Min {x. P x}"
apply (rule the_equality)
 apply (metis (mono_tags) Min.infinite Min_in Min_singleton all_not_in_conv finite_subset insert_iff mem_Collect_eq subsetI)
by (metis (erased, hide_lams) Least_Min Least_equality Set.set_insert ex_in_conv finite.emptyI finite_insert insert_iff mem_Collect_eq order_refl)

lemma The_Max: "Ex1 P  The P = Max {x. P x}"
apply (rule the_equality)
 apply (metis (mono_tags) Max.infinite Max_in Max_singleton all_not_in_conv finite_subset insert_iff mem_Collect_eq subsetI)
by (metis Max_singleton Min_singleton Nitpick.Ex1_unfold The_Min the_equality)

lemma set_sorted_list_of_set_remove [simp]:
"set (sorted_list_of_set (Set.remove x A)) = Set.remove x (set (sorted_list_of_set A))"
  unfolding Set.remove_def
by (cases "finite A"; simp)

lemma set_minus_one: "v  v'; v'  set vs  set vs - {v'}  {v}  set vs = {v'}  set vs = {v,v'}"
  by auto

lemma set_single_hd: "set vs = {v}  hd vs = v"
  by (induction vs; auto)

lemma set_double_filter_hd: " set vs = {v,v'}; v  v'   hd [v'vs . v'  v] = v'"
apply (induction vs)
 apply simp
apply auto
apply (case_tac "v  set vs")
 prefer 2
 apply (subgoal_tac "set vs = {v'}")
  prefer 2
  apply fastforce
 apply (clarsimp simp: set_single_hd)
by fastforce

lemma map_option_the: "x = map_option f y  x  None  the x = f (the y)"
  by (auto simp: map_option_case split: option.split prod.splits)

end

Theory Serial_Rel

(*  Title:      Serial_Rel.thy
    Author:     Sebastian Ullrich
*)

subsection "Serial Relations"

text ‹A serial relation on a finite carrier induces a cycle.›

theory Serial_Rel
imports Main
begin

definition "serial_on A r  (x  A. y  A. (x,y)  r)"
lemmas serial_onI = serial_on_def[THEN iffD2, rule_format]
lemmas serial_onE = serial_on_def[THEN iffD1, rule_format, THEN bexE]

fun iterated_serial_on :: "'a set  'a rel  'a  nat  'a" where
  "iterated_serial_on A r x 0 = x"
| "iterated_serial_on A r x (Suc n) = (SOME y. y  A  (iterated_serial_on A r x n,y)  r)"

lemma iterated_serial_on_linear: "iterated_serial_on A r x (n+m) = iterated_serial_on A r (iterated_serial_on A r x n) m"
by (induction m) auto

lemma iterated_serial_on_in_A:
  assumes "serial_on A r" "a  A"
  shows "iterated_serial_on A r a n  A"
proof (induct n)
  case (Suc n)
  thus ?case
    using assms(1, 2) by (subst iterated_serial_on.simps(2)) (rule someI2_ex, auto elim: serial_onE)
qed (simp add:assms(2))

lemma iterated_serial_on_in_power:
  assumes "serial_on A r" "a  A"
  shows "(a,iterated_serial_on A r a n)  r ^^ n"
proof (induct n)
  case (Suc n)
  moreover obtain b where "(iterated_serial_on A r a n,b)  r" "b  A"
    using iterated_serial_on_in_A[OF assms, of n] assms(1) by - (rule serial_onE)
  ultimately show ?case by (subst iterated_serial_on.simps(2)) (rule someI2_ex, auto)
qed simp

lemma trancl_powerI: "a  R ^^ n  n > 0  a  R+"
by (auto simp:trancl_power)

theorem serial_on_finite_cycle:
  assumes "serial_on A r" "A  {}" "finite A"
  obtains a where "a  A" "(a,a)  r+"
proof-
  from assms(2) obtain a where a: "a  A" by auto
  let ?f = "iterated_serial_on A r a"
  from a have "range ?f  A" using assms(1) by (auto intro: iterated_serial_on_in_A)
  with assms(3) have "mUNIV.¬ finite {n  UNIV. ?f n = ?f m}"
    by - (rule pigeonhole_infinite, auto simp: finite_subset)
  then obtain n m where "?f m = ?f n" and[simp]: "n < m"
    by (metis (mono_tags, lifting) finite_nat_set_iff_bounded mem_Collect_eq not_less_eq)
  hence "?f n = iterated_serial_on A r (?f n) (m-n)"
    using iterated_serial_on_linear[of A r a n "m-n"] by (auto simp:less_imp_le_nat)
  also have "(?f n,iterated_serial_on A r (?f n) (m-n))  r ^^ (m - n)"
    by (rule iterated_serial_on_in_power[OF assms(1)], rule iterated_serial_on_in_A[OF assms(1) a])
  finally show ?thesis
    by - (rule that[of "?f n"], rule iterated_serial_on_in_A[OF assms(1) a], rule trancl_powerI, auto)
qed

end

Theory Mapping_Exts

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

subsection "Mapping Extensions"

text ‹Some lifted definition on mapping and efficient implementations.›

theory Mapping_Exts
imports "HOL-Library.Mapping" FormalSSA_Misc
begin

lift_definition mapping_delete_all :: "('a  bool)  ('a,'b) mapping  ('a,'b) mapping"
  is "λP m x. if (P x) then None else m x" .
lift_definition map_keys :: "('a  'b)  ('a,'c) mapping  ('b,'c) mapping"
  is "λf m x. if f -` {x}  {} then m (THE k. f -` {x} = {k}) else None" .
lift_definition map_values :: "('a  'b  'c option)  ('a,'b) mapping  ('a,'c) mapping"
  is "λf m x. Option.bind (m x) (f x)" .
lift_definition restrict_mapping :: "('a  'b)  'a set  ('a, 'b) mapping"
  is "λf. restrict_map (Some  f)" .
lift_definition mapping_add :: "('a, 'b) mapping  ('a, 'b) mapping  ('a, 'b) mapping"
  is "(++)" .

definition "mmap = Mapping.map id"

lemma lookup_map_keys: "Mapping.lookup (map_keys f m) x = (if f -` {x}  {} then Mapping.lookup m (THE k. f -` {x} = {k}) else None)"
apply transfer ..

lemma Mapping_Mapping_lookup [simp, code_unfold]: "Mapping.Mapping (Mapping.lookup m) = m" by transfer simp
declare Mapping.lookup.abs_eq[simp]

lemma Mapping_eq_lookup: "m = m'  Mapping.lookup m = Mapping.lookup m'" by transfer simp

lemma map_of_map_if_conv:
  "map_of (map (λk. (k, f k)) xs) x = (if (x  set xs) then Some (f x) else None)"
  by (clarsimp simp: map_of_map_restrict)

lemma Mapping_lookup_map: "Mapping.lookup (Mapping.map f g m) a = map_option g (Mapping.lookup m (f a))"
  by transfer simp

lemma Mapping_lookup_map_default: "Mapping.lookup (Mapping.map_default k d f m) k' = (if k = k'
  then (Some  f) (case Mapping.lookup m k of None  d | Some x  x)
  else Mapping.lookup m k')"
  unfolding Mapping.map_default_def Mapping.default_def
  by transfer auto

lemma Mapping_lookup_mapping_add: "Mapping.lookup (mapping_add m1 m2) k =
  case_option (Mapping.lookup m1 k) Some (Mapping.lookup m2 k)"
  by transfer (simp add: map_add_def)

lemma Mapping_lookup_map_values: "Mapping.lookup (map_values f m) k =
  Option.bind (Mapping.lookup m k) (f k)"
  by transfer simp

lemma lookup_fold_update [simp]: "Mapping.lookup (fold (λn. Mapping.update n (g n)) xs m) x
  = (if (x  set xs) then Some (g x) else Mapping.lookup m x)"
  by transfer (rule fold_update_conv)

lemma mapping_eq_iff: "m1 = m2  (k. Mapping.lookup m1 k = Mapping.lookup m2 k)"
  by transfer auto

lemma lookup_delete: "Mapping.lookup (Mapping.delete k m) k' = (if k = k' then None else Mapping.lookup m k')"
  by transfer auto

lemma keys_map_values: "Mapping.keys (map_values f m) = Mapping.keys m - {kMapping.keys m. f k (the (Mapping.lookup m k)) = None}"
  by transfer (auto simp add: bind_eq_Some_conv)

lemma map_default_eq: "Mapping.map_default k v f m = m  (v. Mapping.lookup m k = Some v  f v = v)"
  apply (clarsimp simp: Mapping.map_default_def Mapping.default_def)
  by transfer' (auto simp: fun_eq_iff split: if_splits)

lemma lookup_update_cases: "Mapping.lookup (Mapping.update k v m) k' = (if k=k' then Some v else Mapping.lookup m k')"
by (cases "k=k'", simp_all add: Mapping.lookup_update Mapping.lookup_update_neq)

end

Theory RBT_Mapping_Exts

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

theory RBT_Mapping_Exts
imports
  Mapping_Exts
  "HOL-Library.RBT_Mapping"
  "HOL-Library.RBT_Set"
begin

lemma restrict_mapping_code [code]:
  "restrict_mapping f (RBT_Set.Set r) = RBT_Mapping.Mapping (RBT.map (λa _. f a) r)"
  by transfer (auto simp: RBT_Set.Set_def restrict_map_def)

lemma map_keys_code:
  assumes "inj f"
  shows "map_keys f (RBT_Mapping.Mapping t) = RBT.fold (λx v m. Mapping.update (f x) v m) t Mapping.empty"
proof-
  have[simp]: "x. {y. f y = f x} = {x}"
    using assms by (auto simp: inj_on_def)

  have[simp]: "distinct (map fst (rev (RBT.entries t)))"
  apply (subst rev_map[symmetric])
  apply (subst distinct_rev)
  apply (rule distinct_entries)
  done

  {
    fix k v
    fix xs :: "('a × 'c) list"
    assume asm: "distinct (map fst xs)"
    hence
      "(k, v)  set xs  Some v = foldr (λ(x, v) m. m(f x  v)) xs Map.empty (f k)"
      "k  fst ` set xs  None = foldr (λ(x, v) m. m(f x  v)) xs Map.empty (f k)"
      "x. x  f ` UNIV  None = foldr (λ(x, v) m. m(f x  v)) xs Map.empty x"
      by (induction xs) (auto simp: image_def dest!: injD[OF assms])
  }
  note a = this[unfolded foldr_conv_fold, where xs3="rev _", simplified]

  show ?thesis
  unfolding RBT.fold_fold
  apply (transfer fixing: t f)
  apply (rule ext)
  apply (auto simp: vimage_def)
   apply (rename_tac x)
   apply (case_tac "RBT.lookup t x")
    apply (auto simp: lookup_in_tree[symmetric] intro!: a(2))[1]
   apply (auto dest!: lookup_in_tree[THEN iffD1] intro!: a(1))[1]
  apply (rule a(3); auto)
  done
qed

lemma map_values_code [code]:
  "map_values f (RBT_Mapping.Mapping t) = RBT.fold (λx v m. case (f x v) of None  m | Some v'  Mapping.update x v' m) t Mapping.empty"
proof -
  {fix xs m
    assume "distinct (map fst (xs::('a × 'c) list))"
    hence "fold (λp m. case f (fst p) (snd p) of None  m | Some v'  m(fst p  v')) xs m
       = m ++ (λx. Option.bind (map_of xs x) (f x))"
    by (induction xs arbitrary: m) (auto intro: rev_image_eqI split: bind_split option.splits simp: map_add_def fun_eq_iff)
  }
  note bind_map_of_fold = this
  show ?thesis
  unfolding RBT.fold_fold
  apply (transfer fixing: t f)
  apply (simp add: split_def)
  apply (rule bind_map_of_fold [of "RBT.entries t" Map.empty, simplified, symmetric])
  using RBT.distinct_entries distinct_map by auto
qed

lemma [code_unfold]: "set (RBT.keys t) = RBT_Set.Set (RBT.map (λ_ _. ()) t)"
  by (auto simp: RBT_Set.Set_def RBT.keys_def_alt RBT.lookup_in_tree elim: rev_image_eqI)

lemma mmap_rbt_code [code]: "mmap f (RBT_Mapping.Mapping t) = RBT_Mapping.Mapping (RBT.map (λ_. f) t)"
  unfolding mmap_def by transfer auto

lemma mapping_add_code [code]: "mapping_add (RBT_Mapping.Mapping t1) (RBT_Mapping.Mapping t2) = RBT_Mapping.Mapping (RBT.union t1 t2)"
  by transfer (simp add: lookup_union)

end

Theory Graph_path

(*  Title:      Graph_path.thy
    Author:     Sebastian Ullrich
*)

section ‹SSA Representation›

subsection ‹Inductive Graph Paths›

text ‹We extend the Graph framework with inductively defined paths.
  We adopt the convention of separating locale definitions into assumption-less base locales.›

theory Graph_path imports
  FormalSSA_Misc
  Dijkstra_Shortest_Path.GraphSpec
  CAVA_Automata.Digraph_Basic
begin

hide_const "Omega_Words_Fun.prefix" "Omega_Words_Fun.suffix"

type_synonym ('n, 'ed) edge = "('n × 'ed × 'n)"

definition getFrom :: "('n, 'ed) edge  'n" where
  "getFrom  fst"
definition getData :: "('n, 'ed) edge  'ed" where
  "getData  fst  snd"
definition getTo :: "('n, 'ed) edge  'n" where
  "getTo  snd  snd"

lemma get_edge_simps [simp]:
  "getFrom (f,d,t) = f"
  "getData (f,d,t) = d"
  "getTo (f,d,t) = t"
  by (simp_all add: getFrom_def getData_def getTo_def)

  text ‹Predecessors of a node.›
  definition pred :: "('v,'w) graph  'v  ('v×'w) set"
    where "pred G v  {(v',w). (v',w,v)edges G}"

  lemma pred_finite[simp, intro]: "finite (edges G)  finite (pred G v)"
    unfolding pred_def
    by (rule finite_subset[where B="(λ(v,w,v'). (v,w))`edges G"]) force+

  lemma pred_empty[simp]: "pred empty v = {}" unfolding empty_def pred_def by auto

  lemma (in valid_graph) pred_subset: "pred G v  V×UNIV"
    unfolding pred_def using E_valid
    by (force)

  type_synonym ('V,'W,,'G) graph_pred_it =
    "'G  'V  ('V×'W,) set_iterator"

  locale graph_pred_it_defs =
    fixes pred_list_it :: "'G  'V  ('V×'W,('V×'W) list) set_iterator"
  begin
    definition "pred_it g v  it_to_it (pred_list_it g v)"
  end

  locale graph_pred_it = graph α invar + graph_pred_it_defs pred_list_it
    for α :: "'G  ('V,'W) graph" and invar and
    pred_list_it :: "'G  'V  ('V×'W,('V×'W) list) set_iterator" +
    assumes pred_list_it_correct:
      "invar g  set_iterator (pred_list_it g v) (pred (α g) v)"
  begin
    lemma pred_it_correct:
      "invar g  set_iterator (pred_it g v) (pred (α g) v)"
      unfolding pred_it_def
      apply (rule it_to_it_correct)
      by (rule pred_list_it_correct)

    lemma pi_pred_it[icf_proper_iteratorI]:
      "proper_it (pred_it S v) (pred_it S v)"
      unfolding pred_it_def
      by (intro icf_proper_iteratorI)

    lemma pred_it_proper[proper_it]:
      "proper_it' (λS. pred_it S v) (λS. pred_it S v)"
      apply (rule proper_it'I)
      by (rule pi_pred_it)
  end

  record ('V,'W,'G) graph_ops = "('V,'W,'G) GraphSpec.graph_ops" +
    gop_pred_list_it :: "'G  'V  ('V×'W,('V×'W) list) set_iterator"

  lemma (in graph_pred_it) pred_it_is_iterator[refine_transfer]:
    "invar g  set_iterator (pred_it g v) (pred (α g) v)"
    by (rule pred_it_correct)

locale StdGraphDefs = GraphSpec.StdGraphDefs ops
  + graph_pred_it_defs "gop_pred_list_it ops"
  for ops :: "('V,'W,'G,'m) graph_ops_scheme"
begin
  abbreviation pred_list_it  where "pred_list_it  gop_pred_list_it ops"
end

locale StdGraph = StdGraphDefs + org:StdGraph +
  graph_pred_it α invar pred_list_it

locale graph_path_base =
  graph_nodes_it_defs "λg. foldri (αn g)" +
  graph_pred_it_defs "λg n. foldri (inEdges' g n)"
for
  αe :: "'g  ('node × 'edgeD × 'node) set" and
  αn :: "'g  'node list" and
  invar :: "'g  bool" and
  inEdges' :: "'g  'node  ('node × 'edgeD) list"
begin

(*
  abbreviation αe :: "'g ⇒ ('node × 'edgeD × 'node) set"
  where "αe g ≡ graph.edges (α g)"
  definition αn :: "'g ⇒ 'node list"
  where "αn g ≡ nodes_it g (λ_. True) (#) []"
*)

  definition inEdges :: "'g  'node  ('node × 'edgeD × 'node) list"
  where "inEdges g n  map (λ(f,d). (f,d,n)) (inEdges' g n)"

  definition predecessors :: "'g  'node  'node list" where
    "predecessors g n  map getFrom (inEdges g n)"

  definition successors :: "'g  'node  'node list" where
    "successors g m  [n . n  αn g, m  set (predecessors g n)]"


  declare predecessors_def [code]

  declare [[inductive_internals]]
  inductive path :: "'g  'node list  bool"
    for g :: 'g
  where
    empty_path[intro]: "n  set (αn g); invar g  path g [n]"
    | Cons_path[intro]: "path g ns; n'  set (predecessors g (hd ns))  path g (n'#ns)"

  definition path2 :: "'g  'node  'node list  'node  bool" ("_  _-__" [51,0,0,51] 80) where
    "path2 g n ns m  path g ns  n = hd ns  m = last ns"

  abbreviation "α g  nodes = set (αn g), edges = αe g"
end

locale graph_path =
  graph_path_base αe αn invar inEdges' +
  graph α invar +
  ni: graph_nodes_it α invar "λg. foldri (αn g)" +
  pi: graph_pred_it α invar "λg n. foldri (inEdges' g n)"
for
  αe :: "'g  ('node × 'edgeD × 'node) set" and
  αn :: "'g  'node list" and
  invar :: "'g  bool" and
  inEdges' :: "'g  'node  ('node × 'edgeD) list"
begin
  lemma αn_correct: "invar g  set (αn g)  getFrom ` αe g  getTo ` αe g"
    by (frule valid) (auto dest: valid_graph.E_validD)

  lemma αn_distinct: "invar g  distinct (αn g)"
    by (frule ni.nodes_list_it_correct)
      (metis foldri_cons_id iterate_to_list_correct iterate_to_list_def)

  lemma inEdges_correct':
    assumes "invar g"
    shows "set (inEdges g n) = (λ(f,d). (f,d,n)) ` (pred (α g) n)"
  proof -
    from iterate_to_list_correct [OF pi.pred_list_it_correct [OF assms], of n]
    show ?thesis
      by (auto intro: rev_image_eqI simp: iterate_to_list_def pred_def inEdges_def)
  qed

  lemma inEdges_correct [intro!, simp]:
    "invar g  set (inEdges g n) = {(_, _, t). t = n}  αe g"
    by (auto simp: inEdges_correct' pred_def)

  lemma in_set_αnI1 [intro]: "invar g; x  getFrom ` αe g  x  set (αn g)"
    using αn_correct by blast
  lemma in_set_αnI2 [intro]: "invar g; x  getTo ` αe g  x  set (αn g)"
    using αn_correct by blast

(*

locale graph_path_base = graph_inEdges_base αe invar inEdges + graph_nodes_base αe invar αn
for
  αe :: "'g ⇒ ('node × 'edgeD × 'node) set" and
  αn :: "'g ⇒ 'node list" and
  invar :: "'g ⇒ bool" and
  inEdges :: "'g ⇒ 'node ⇒ ('node × 'edgeD × 'node) list"
begin
*)

(*
end

locale graph_path = graph_path_base αe αn invar inEdges + graph_inEdges αe invar inEdges + graph_nodes αe invar αn
for
  αe :: "'g ⇒ ('node × 'edgeD × 'node) set" and
  αn :: "'g ⇒ 'node list" and
  invar :: "'g ⇒ bool" and
  inEdges :: "'g ⇒ 'node ⇒ ('node × 'edgeD × 'node) list"
begin
*)

  lemma edge_to_node:
    assumes "invar g" and "e  αe g"
    obtains "getFrom e  set (αn g)" and "getTo e  set (αn g)"
  using assms(2) αn_correct [OF invar g]
    by (cases e) (auto 4 3 intro: rev_image_eqI)

  lemma inEdge_to_edge:
    assumes "e  set (inEdges g n)" and "invar g"
    obtains eD n' where "(n',eD,n)  αe g"
    using assms by auto

  lemma edge_to_inEdge:
    assumes "(n,eD,m)  αe g" "invar g"
    obtains "(n,eD,m)  set (inEdges g m)"
    using assms by auto

  lemma edge_to_predecessors:
    assumes "(n,eD,m)  αe g" "invar g"
    obtains "n  set (predecessors g m)"
  proof atomize_elim
    from assms have "(n,eD,m)  set (inEdges g m)" by (rule edge_to_inEdge)
    thus "n  set (predecessors g m)" unfolding predecessors_def by (metis get_edge_simps(1) image_eqI set_map)
  qed

  lemma predecessor_is_node[elim]: "n  set (predecessors g n'); invar g  n  set (αn g)"
  unfolding predecessors_def by (fastforce intro: rev_image_eqI simp: getTo_def getFrom_def)

  lemma successor_is_node[elim]: "n  set (predecessors g n'); n  set (αn g); invar g  n'  set (αn g)"
  unfolding predecessors_def by (fastforce intro: rev_image_eqI)

  lemma successors_predecessors[simp]: "n  set (αn g)  n  set (successors g m)  m  set (predecessors g n)"
  by (auto simp:successors_def predecessors_def)


  lemma path_not_Nil[simp, dest]: "path g ns  ns  []"
  by (erule path.cases) auto

  lemma path2_not_Nil[simp]: "g  n-nsm  ns  []"
  unfolding path2_def by auto

  lemma path2_not_Nil2[simp]: "¬ g  n-[]m"
  unfolding path2_def by auto

  lemma path2_not_Nil3[simp]: "g  n-nsm  length ns  1"
    by (cases ns, auto)

  lemma empty_path2[intro]: "n  set (αn g); invar g  g  n-[n]n"
  unfolding path2_def by auto

  lemma Cons_path2[intro]: "g  n-nsm; n'  set (predecessors g n)  g  n'-n'#nsm"
  unfolding path2_def by auto

  lemma path2_cases:
    assumes "g  n-nsm"
    obtains (empty_path) "ns = [n]" "m = n"
          | (Cons_path) "g  hd (tl ns)-tl nsm" "n  set (predecessors g (hd (tl ns)))"
  proof-
    from assms have 1: "path g ns" "hd ns = n" "last ns = m" by (auto simp: path2_def)
    from this(1) show thesis
    proof cases
      case (empty_path n)
      with 1 show thesis by - (rule that(1), auto)
    next
      case (Cons_path ns n')
      with 1 show thesis by - (rule that(2), auto simp: path2_def)
    qed
  qed

  lemma path2_induct[consumes 1, case_names empty_path Cons_path]:
    assumes "g  n-nsm"
    assumes empty: "invar g  P m [m] m"
    assumes Cons: "ns n' n. g  n-nsm  P n ns m  n'  set (predecessors g n)  P n' (n' # ns) m"
    shows "P n ns m"
  using assms(1)
  unfolding path2_def
  apply-
  proof (erule conjE, induction arbitrary: n rule:path.induct)
    case empty_path
    with empty show ?case by simp
  next
    case (Cons_path ns n' n'')
    hence[simp]: "n'' = n'" by simp
    from Cons_path Cons show ?case unfolding path2_def by auto
  qed

  lemma path_invar[intro]: "path g ns  invar g"
  by (induction rule:path.induct)

  lemma path_in_αn[intro]: "path g ns; n  set ns  n  set (αn g)"
  by (induct ns arbitrary: n rule:path.induct) auto

  lemma path2_in_αn[elim]: "g  n-nsm; l  set ns  l  set (αn g)"
  unfolding path2_def by auto

  lemma path2_hd_in_αn[elim]: "g  n-nsm  n  set (αn g)"
  unfolding path2_def by auto

  lemma path2_tl_in_αn[elim]: "g  n-nsm  m  set (αn g)"
  unfolding path2_def by auto

  lemma path2_forget_hd[simp]: "g  n-nsm  g  hd ns-nsm"
  unfolding path2_def by simp

  lemma path2_forget_last[simp]: "g  n-nsm  g  n-nslast ns"
  unfolding path2_def by simp

  lemma path_hd[dest]: "path g (n#ns)  path g [n]"
  by (rule empty_path, auto elim:path.cases)

  lemma path_by_tail[intro]: "path g (n#n'#ns); path g (n'#ns)  path g (n'#ms)  path g (n#n'#ms)"
  by (rule path.cases) auto

  lemma αn_in_αnE [elim]:
    assumes "(n,e,m)  αe g" and "invar g"
    obtains "n  set (αn g)" and "m  set (αn g)"
    using assms
    by (auto elim: edge_to_node)

  lemma path_split:
    assumes "path g (ns@m#ns')"
    shows "path g (ns@[m])" "path g(m#ns')"
  proof-
    from assms show "path g (ns@[m])"
    proof (induct ns)
      case (Cons n ns)
      thus ?case by (cases ns) auto
    qed auto
    from assms show "path g (m#ns')"
    proof (induct ns)
      case (Cons n ns)
      thus ?case by (auto elim:path.cases)
    qed auto
  qed

  lemma path2_split:
    assumes "g  n-ns@n'#ns'm"
    shows "g  n-ns@[n']n'" "g  n'-n'#ns'm"
  using assms unfolding path2_def by (auto intro:path_split iff:hd_append)

  lemma elem_set_implies_elem_tl_app_cons[simp]: "x  set xs  x  set (tl (ys@y#xs))"
    by (induction ys arbitrary: y; auto)

  lemma path2_split_ex:
    assumes "g  n-nsm" "x  set ns"
    obtains ns1 ns2 where "g  n-ns1x" "g  x-ns2m" "ns = ns1@tl ns2" "ns = butlast ns1@ns2"
  proof-
    from assms(2) obtain ns1 ns2 where "ns = ns1@x#ns2" by atomize_elim (rule split_list)
    with assms[simplified this] show thesis
      by - (rule that, auto dest:path2_split(1) path2_split(2) intro: suffixI)
  qed

  lemma path2_split_ex':
    assumes "g  n-nsm" "x  set ns"
    obtains ns1 ns2 where "g  n-ns1x" "g  x-ns2m" "ns = butlast ns1@ns2"
  using assms by (rule path2_split_ex)

  lemma path_snoc:
    assumes "path g (ns@[n])" "n  set (predecessors g m)"
    shows "path g (ns@[n,m])"
  using assms(1) proof (induction ns)
    case Nil
    hence 1: "n  set (αn g)" "invar g" by auto
    with assms(2) have "m  set (αn g)" by auto
    with 1 have "path g [m]" by auto
    with assms(2) show ?case by auto
  next
    case (Cons l ns)
    hence 1: "path g (ns @ [n])  l  set (predecessors g (hd (ns@[n])))" by -(cases g "(l # ns) @ [n]" rule:path.cases, auto)
    hence "path g (ns @ [n,m])" by (auto intro:Cons.IH)
    with 1 have "path g (l # ns @ [n,m])" by -(rule Cons_path, assumption, cases ns, auto)
    thus ?case by simp
  qed

  lemma path2_snoc[elim]:
    assumes "g  n-nsm" "m  set (predecessors g m')"
    shows "g  n-ns@[m']m'"
  proof-
    from assms(1) have 1: "ns  []" by auto

    have "path g ((butlast ns) @ [last ns, m'])"
    using assms unfolding path2_def by -(rule path_snoc, auto)
    hence "path g ((butlast ns @ [last ns]) @ [m'])" by simp
    with 1 have "path g (ns @ [m'])" by simp
    thus ?thesis
    using assms unfolding path2_def by auto
  qed

  lemma path_unsnoc:
    assumes "path g ns" "length ns  2"
    obtains "path g (butlast ns)  last (butlast ns)  set (predecessors g (last ns))"
  using assms
  proof (atomize_elim, induction ns)
    case (Cons_path ns n)
    show ?case
    proof (cases "2  length ns")
      case True
        hence [simp]: "hd (butlast ns) = hd ns" by (cases ns, auto)
        have 0: "n#butlast ns = butlast (n#ns)" using True by auto
        have 1: "n  set (predecessors g (hd (butlast ns)))" using Cons_path by simp
        from True have "path g (butlast ns)" using Cons_path by auto
        hence "path g (n#butlast ns)" using 1 by auto
        hence "path g (butlast (n#ns))" using 0 by simp
      moreover
        from Cons_path True have "last (butlast ns)  set (predecessors g (last ns))" by simp
        hence "last (butlast (n # ns))  set (predecessors g (last (n # ns)))"
          using True by (cases ns, auto)
      ultimately show ?thesis by auto
    next
      case False
      thus ?thesis
      proof (cases ns)
        case Nil
        thus ?thesis using Cons_path by -(rule ccontr, auto elim:path.cases)
      next
        case (Cons n' ns')
        hence [simp]: "ns = [n']" using False by (cases ns', auto)
        have "path g [n,n']" using Cons_path by auto
        thus ?thesis using Cons_path by auto
      qed
    qed
  qed auto

  lemma path2_unsnoc:
    assumes "g  n-nsm" "length ns  2"
    obtains "g  n-butlast nslast (butlast ns)" "last (butlast ns)  set (predecessors g m)"
  using assms unfolding path2_def by (metis append_butlast_last_id hd_append2 path_not_Nil path_unsnoc)

  lemma path2_rev_induct[consumes 1, case_names empty snoc]:
    assumes "g  n-nsm"
    assumes empty: "n  set (αn g)  P n [n] n"
    assumes snoc: "ns m' m. g  n-nsm'  P n ns m'  m'  set (predecessors g m)  P n (ns@[m]) m"
    shows "P n ns m"
  using assms(1) proof (induction arbitrary:m rule:length_induct)
    case (1 ns)
    show ?case
    proof (cases "length ns  2")
      case False
      thus ?thesis
      proof (cases ns)
        case Nil
        thus ?thesis using 1(2) by auto
      next
        case (Cons n' ns')
        with False have "ns' = []" by (cases ns', auto)
        with Cons 1(2) have "n' = n" "m = n" unfolding path2_def by auto
        with Cons ns' = [] 1(2) show ?thesis by (auto intro:empty)
      qed
    next
      case True
      let ?ns' = "butlast ns"
      let ?m' = "last ?ns'"
      from 1(2) have m: "m = last ns" unfolding path2_def by auto
      from True 1(2) obtain ns': "g  n-?ns'?m'" "?m'  set (predecessors g m)" by -(rule path2_unsnoc)
      with True "1.IH" have "P n ?ns' ?m'" by auto
      with ns' have "P n (?ns'@[m]) m" by (auto intro!: snoc)
      with m 1(2) show ?thesis by auto
    qed
  qed

  lemma path2_hd[elim, dest?]: "g  n-nsm  n = hd ns"
  unfolding path2_def by simp

  lemma path2_hd_in_ns[elim]: "g  n-nsm  n  set ns"
  unfolding path2_def by auto

  lemma path2_last[elim, dest?]: "g  n-nsm  m = last ns"
  unfolding path2_def by simp

  lemma path2_last_in_ns[elim]: "g  n-nsm  m  set ns"
  unfolding path2_def by auto

  lemma path_app[elim]:
    assumes "path g ns" "path g ms" "last ns = hd ms"
    shows "path g (ns@tl ms)"
  using assms by (induction ns rule:path.induct) auto

  lemma path2_app[elim]:
    assumes "g  n-nsm" "g  m-msl"
    shows "g  n-ns@tl msl"
  proof-
    have "last (ns @ tl ms) = last ms" using assms
    unfolding path2_def
    proof (cases "tl ms")
      case Nil
      hence "ms = [m]" using assms(2) unfolding path2_def by (cases ms, auto)
      thus ?thesis using assms(1) unfolding path2_def by auto
    next
      case (Cons m' ms')
      from this[symmetric] have "ms = hd ms#m'#ms'" using assms(2) by auto
      thus ?thesis using assms unfolding path2_def by auto
    qed
    with assms show ?thesis
      unfolding path2_def by auto
  qed

  lemma butlast_tl:
    assumes "last xs = hd ys" "xs  []" "ys  []"
    shows "butlast xs@ys = xs@tl ys"
    by (metis append.simps(1) append.simps(2) append_assoc append_butlast_last_id assms(1) assms(2) assms(3) list.collapse)

  lemma path2_app'[elim]:
    assumes "g  n-nsm" "g  m-msl"
    shows "g  n-butlast ns@msl"
  proof-
    have "butlast ns@ms = ns@tl ms" using assms by - (rule butlast_tl, auto dest:path2_hd path2_last)
    moreover from assms have "g  n-ns@tl msl" by (rule path2_app)
    ultimately show ?thesis by simp
  qed

  lemma path2_nontrivial[elim]:
    assumes "g  n-nsm" "n  m"
    shows "length ns  2"
  using assms
    by (metis Suc_1 le_antisym length_1_last_hd not_less_eq_eq path2_hd path2_last path2_not_Nil3)

  lemma simple_path2_aux:
    assumes "g  n-nsm"
    obtains ns' where "g  n-ns'm" "distinct ns'" "set ns'  set ns" "length ns'  length ns"
  apply atomize_elim
  using assms proof (induction rule:path2_induct)
    case empty_path
    with assms show ?case by - (rule exI[of _ "[m]"], auto)
  next
    case (Cons_path ns n n')
    then obtain ns' where ns': "g  n'-ns'm" "distinct ns'" "set ns'  set ns" "length ns'  length ns" by auto
    show ?case
    proof (cases "n  set ns'")
      case False
      with ns' Cons_path(2) show ?thesis by -(rule exI[where x="n#ns'"], auto)
    next
      case True
      with ns' obtain ns'1 ns'2 where split: "ns' = ns'1@n#ns'2" "n  set ns'2" by -(atomize_elim, rule split_list_last)
      with ns' have "g  n-n#ns'2m" by -(rule path2_split, simp)
      with split ns' show ?thesis by -(rule exI[where x="n#ns'2"], auto)
    qed
  qed

  lemma simple_path2:
    assumes "g  n-nsm"
    obtains ns' where "g  n-ns'm" "distinct ns'" "set ns'  set ns" "length ns'   length ns" "n  set (tl ns')" "m  set (butlast ns')"
  using assms
  apply (rule simple_path2_aux)
  by (metis append_butlast_last_id distinct.simps(2) distinct1_rotate hd_Cons_tl path2_hd path2_last path2_not_Nil rotate1.simps(2))

  lemma simple_path2_unsnoc:
    assumes "g  n-nsm" "n  m"
    obtains ns' where "g  n-ns'last ns'" "last ns'  set (predecessors g m)" "distinct ns'" "set ns'  set ns" "m  set ns'"
  proof-
    obtain ns' where 1: "g  n-ns'm" "distinct ns'" "set ns'  set ns" "m  set (butlast ns')" by (rule simple_path2[OF assms(1)])
    with assms(2) obtain 2: "g  n-butlast ns'last (butlast ns')" "last (butlast ns')  set (predecessors g m)" by - (rule path2_unsnoc, auto)
    show thesis
    proof (rule that[of "butlast ns'"])
      from 1(3) show "set (butlast ns')  set ns" by (metis in_set_butlastD subsetI subset_trans)
    qed (auto simp:1 2 distinct_butlast)
  qed

  lemma path2_split_first_last:
    assumes "g  n-nsm" "x  set ns"
    obtains ns1 ns3 ns2 where "ns = ns1@ns3@ns2" "prefix (ns1@[x]) ns" "suffix (x#ns2) ns"
        and "g  n-ns1@[x]x"  "x  set ns1"
        and "g  x-ns3x"
        and "g  x-x#ns2m" "x  set ns2"
  proof-
    from assms(2) obtain ns1 ns' where 1: "ns = ns1@x#ns'" "x  set ns1" by (atomize_elim, rule split_list_first)
    from assms(1)[unfolded 1(1)] have 2: "g  n-ns1@[x]x" "g  x-x#ns'm" by - (erule path2_split, erule path2_split)
    obtain ns3 ns2 where 3: "x#ns' = ns3@x#ns2" "x  set ns2" by (atomize_elim, rule split_list_last, simp)
    from 2(2)[unfolded 3(1)] have 4: "g  x-ns3@[x]x" "g  x-x#ns2m" by - (erule path2_split, erule path2_split)
    show thesis
    proof (rule that[OF _ _ _ 2(1) 1(2) 4 3(2)])
      show "ns = ns1 @ (ns3 @ [x]) @ ns2" using 1(1) 3(1) by simp
      show "prefix (ns1@[x]) ns" using 1 by auto
      show "suffix (x#ns2) ns" using 1 3 by (metis Sublist.suffix_def suffix_order.order_trans)
    qed
  qed

  lemma path2_simple_loop:
    assumes "g  n-nsn" "n'  set ns"
    obtains ns' where "g  n-ns'n" "n'  set ns'" "n  set (tl (butlast ns'))" "set ns'  set ns"
  using assms proof (induction "length ns" arbitrary: ns rule: nat_less_induct)
    case 1
    let ?ns' = "tl (butlast ns)"
    show ?case
    proof (cases "n  set ?ns'")
      case False
      with "1.prems"(2,3) show ?thesis by - (rule "1.prems"(1), auto)
    next
      case True
      hence 2: "length ns > 1" by (cases ns, auto)
      with "1.prems"(2) obtain m where m: "g  n-butlast nsm" "m  set (predecessors g n)" by - (rule path2_unsnoc, auto)
      with True obtain m' where m': "g  m'-?ns'm" "n  set (predecessors g m')" by - (erule path2_cases, auto)
      with True obtain ns1 ns2 where split: "g  m'-ns1n" "g  n-ns2m" "?ns' = ns1@tl ns2" "?ns' = butlast ns1@ns2"
        by - (rule path2_split_ex)
      have "ns = butlast ns@[n]" using 2 "1.prems"(2) by (auto simp: path2_def)
      moreover have "butlast ns = n#tl (butlast ns)" using 2 m(1) by (auto simp: path2_def)
      ultimately have split': "ns = n#ns1@tl ns2@[n]" "ns = n#butlast ns1@ns2@[n]" using split(3,4) by auto
      show ?thesis
      proof (cases "n'  set (n#ns1)")
        case True
        show ?thesis
        proof (rule "1.hyps"[rule_format, of _ "n#ns1"])
          show "length (n#ns1) < length ns" using split'(1) by auto
          show "n'  set (n#ns1)" by (rule True)
        qed (auto intro: split(1) m'(2) intro!: "1.prems"(1) simp: split'(1))
      next
        case False
        from False split'(1) "1.prems"(3) have 5: "n'  set (ns2@[n])" by auto
        show ?thesis
        proof (rule "1.hyps"[rule_format, of _ "ns2@[n]"])
          show "length (ns2@[n]) < length ns" using split'(2) by auto
          show "n'  set (ns2@[n])" by (rule 5)
          show "g  n-ns2@[n]n" using split(2) m(2) by (rule path2_snoc)
        qed (auto intro!: "1.prems"(1) simp: split'(2))
      qed
    qed
  qed

  lemma path2_split_first_prop:
    assumes "g  n-nsm" "xset ns. P x"
    obtains m' ns' where "g  n-ns'm'" "P m'" "x  set (butlast ns'). ¬P x" "prefix ns' ns"
  proof-
    obtain ns'' n' ns' where 1: "ns = ns''@n'#ns'" "P n'" "x  set ns''. ¬P x" by - (rule split_list_first_propE[OF assms(2)])
    with assms(1) have "g  n-ns''@[n']n'" by - (rule path2_split(1), auto)
    with 1 show thesis by - (rule that, auto)
  qed

  lemma path2_split_last_prop:
    assumes "g  n-nsm" "xset ns. P x"
    obtains n' ns' where "g  n'-ns'm" "P n'" "x  set (tl ns'). ¬P x" "suffix ns' ns"
  proof-
    obtain ns'' n' ns' where 1: "ns = ns''@n'#ns'" "P n'" "x  set ns'. ¬P x" by - (rule split_list_last_propE[OF assms(2)])
    with assms(1) have "g  n'-n'#ns'm" by - (rule path2_split(2), auto)
    with 1 show thesis by - (rule that, auto simp: Sublist.suffix_def)
  qed

  lemma path2_prefix[elim]:
    assumes 1: "g  n-nsm"
    assumes 2: "prefix (ns'@[m']) ns"
    shows "g  n-ns'@[m']m'"
  using assms by -(erule prefixE, rule path2_split, simp)

  lemma path2_prefix_ex:
    assumes "g  n-nsm" "m'  set ns"
    obtains ns' where "g  n-ns'm'" "prefix ns' ns" "m'  set (butlast ns')"
  proof-
    from assms(2) obtain ns' where "prefix (ns'@[m']) ns" "m'  set ns'" by (rule prefix_split_first)
    with assms(1) show thesis by - (rule that, auto)
  qed

  lemma path2_strict_prefix_ex:
    assumes "g  n-nsm" "m'  set (butlast ns)"
    obtains ns' where "g  n-ns'm'" "strict_prefix ns' ns" "m'  set (butlast ns')"
  proof-
    from assms(2) obtain ns' where ns': "prefix (ns'@[m']) (butlast ns)" "m'  set ns'" by (rule prefix_split_first)
    hence "strict_prefix (ns'@[m']) ns" using assms by - (rule strict_prefix_butlast, auto)
    with assms(1) ns'(2) show thesis by - (rule that, auto)
  qed

  lemma path2_nontriv[elim]: "g  n-nsm; n  m  length ns > 1"
    by (metis hd_Cons_tl last_appendR last_snoc length_greater_0_conv length_tl path2_def path_not_Nil zero_less_diff)

  declare path_not_Nil [simp del]
  declare path2_not_Nil [simp del]
  declare path2_not_Nil3 [simp del]
end

subsection ‹Domination›

text ‹We fix an entry node per graph and use it to define node domination.›

locale graph_Entry_base = graph_path_base αe αn invar inEdges'
for
  αe :: "'g  ('node × 'edgeD × 'node) set" and
  αn :: "'g  'node list" and
  invar :: "'g  bool" and
  inEdges' :: "'g  'node  ('node × 'edgeD) list"
+
fixes Entry :: "'g  'node"
begin
  definition dominates :: "'g  'node  'node  bool" where
    "dominates g n m  m  set (αn g)  (ns. g  Entry g-nsm  n  set ns)"

  abbreviation "strict_dom g n m  n  m  dominates g n m"
end

locale graph_Entry = graph_Entry_base αe αn invar inEdges' Entry
  + graph_path αe αn invar inEdges'
for
  αe :: "'g  ('node × 'edgeD × 'node) set" and
  αn :: "'g  'node list" and
  invar :: "'g  bool" and
  inEdges' :: "'g  'node  ('node × 'edgeD) list" and
  Entry :: "'g  'node"
+
assumes Entry_in_graph[simp]: "Entry g  set (αn g)"
assumes Entry_unreachable: "invar g  inEdges g (Entry g) = []"
assumes Entry_reaches[intro]:
  "n  set (αn g); invar g  ns. g  Entry g-nsn"
begin
  lemma Entry_dominates[simp,intro]: "invar g; n  set (αn g)  dominates g (Entry g) n"
  unfolding dominates_def by auto

  lemma Entry_iff_unreachable[simp]:
    assumes "invar g" "n  set (αn g)"
    shows "predecessors g n = []  n = Entry g"
  proof (rule, rule ccontr)
    assume "predecessors g n = []" "n  Entry g"
    with Entry_reaches[OF assms(2,1)] show False by (auto elim:simple_path2_unsnoc)
  qed (auto simp:assms Entry_unreachable predecessors_def)

  lemma Entry_loop:
    assumes "invar g" "g  Entry g-nsEntry g"
    shows "ns=[Entry g]"
  proof (cases "length ns  2")
    case True
    with assms have "last (butlast ns)  set (predecessors g (Entry g))" by - (rule path2_unsnoc)
    with Entry_unreachable[OF assms(1)] have False by (simp add:predecessors_def)
    thus ?thesis ..
  next
    case False
    with assms show ?thesis
      by (metis Suc_leI hd_Cons_tl impossible_Cons le_less length_greater_0_conv numeral_2_eq_2 path2_hd path2_not_Nil)
  qed

  lemma simple_Entry_path:
    assumes "invar g" "n  set (αn g)"
    obtains ns where "g  Entry g-nsn" and "n  set (butlast ns)"
  proof-
    from assms obtain ns where p: "g  Entry g-nsn" by -(atomize_elim, rule Entry_reaches)
    with p obtain ns' where "g  Entry g-ns'n" "n  set (butlast ns')" by -(rule path2_split_first_last, auto)
    thus ?thesis by (rule that)
  qed

  lemma dominatesI [intro]:
    "m  set (αn g); ns. g  Entry g-nsm  n  set ns  dominates g n m"
  unfolding dominates_def by simp

  lemma dominatesE:
    assumes "dominates g n m"
    obtains "m  set (αn g)" and "ns. g  Entry g-nsm  n  set ns"
    using assms unfolding dominates_def by auto

  lemma[simp]: "dominates g n m  m  set (αn g)" by (rule dominatesE)

  lemma[simp]:
    assumes "dominates g n m" and[simp]: "invar g"
    shows "n  set (αn g)"
  proof-
    from assms obtain ns where "g  Entry g-nsm" by atomize_elim (rule Entry_reaches, auto)
    with assms show ?thesis by (auto elim!:dominatesE)
  qed

  lemma strict_domE[elim]:
    assumes "strict_dom g n m"
    obtains "m  set (αn g)" and "ns. g  Entry g-nsm  n  set (butlast ns)"
  using assms by (metis dominates_def path2_def path_not_Nil rotate1.simps(2) set_ConsD set_rotate1 snoc_eq_iff_butlast)

  lemma dominates_refl[intro!]: "invar g; n  set (αn g)  dominates g n n"
  by auto

  lemma dominates_trans:
    assumes "invar g"
    assumes part1: "dominates g n n'"
    assumes part2: "dominates g n' n''"
    shows   "dominates g n n''"
  proof
    from part2 show "n''  set (αn g)" by auto

    fix ns :: "'node list"
    assume p: "g  Entry g-nsn''"
    with part2 have "n'  set ns" by - (erule dominatesE, auto)
    then obtain as where prefix: "prefix (as@[n']) ns" by (auto intro:prefix_split_first)
    with p have "g  Entry g-(as@[n'])n'" by auto
    with part1 have "n  set (as@[n'])" unfolding dominates_def by auto
    with prefix show "n  set ns" by auto
  qed

  lemma dominates_antisymm:
    assumes "invar g"
    assumes dom1: "dominates g n n'"
    assumes dom2: "dominates g n' n"
    shows "n = n'"
  proof (rule ccontr)
    assume "n  n'"
    from dom2 have "n  set (αn g)" by auto
    with invar g obtain ns where p: "g  Entry g-nsn" and "n  set (butlast ns)"
      by (rule simple_Entry_path)
    with dom2 have "n'  set ns" by - (erule dominatesE, auto)
    then obtain as where prefix: "prefix (as@[n']) ns" by (auto intro:prefix_split_first)
    with p have "g  Entry g-as@[n']n'" by (rule path2_prefix)
    with dom1 have "n  set (as@[n'])" unfolding dominates_def by auto
    with n  n' have "n  set as" by auto
    with ‹prefix (as@[n']) ns have "n  set (butlast ns)" by -(erule prefixE, auto iff:butlast_append)
    with n  set (butlast ns) show False..
  qed

  lemma dominates_unsnoc:
    assumes [simp]: "invar g" and "dominates g n m" "m'  set (predecessors g m)" "n  m"
    shows "dominates g n m'"
  proof
    show "m'  set (αn g)" using assms by auto
  next
    fix ns
    assume "g  Entry g-nsm'"
    with assms(3) have "g  Entry g-ns@[m]m" by auto
    with assms(2,4) show "n  set ns" by (auto elim!:dominatesE)
  qed

  lemma dominates_unsnoc':
    assumes [simp]: "invar g" and "dominates g n m" "g  m'-msm" "x  set (tl ms). x  n"
    shows "dominates g n m'"
  using assms(3,4) proof (induction rule:path2_induct)
    case empty_path
    show ?case by (rule assms(2))
  next
    case (Cons_path ms m'' m')
    from Cons_path(4) have "dominates g n m'"
      by (simp add: Cons_path.IH in_set_tlD)
    moreover from Cons_path(1) have "m'  set ms" by auto
    hence "m'  n" using Cons_path(4) by simp
    ultimately show ?case using Cons_path(2) by - (rule dominates_unsnoc, auto)
  qed

  lemma dominates_path:
    assumes "dominates g n m" and[simp]: "invar g"
    obtains ns where "g  n-nsm"
  proof atomize_elim
    from assms obtain ns where ns: "g  Entry g-nsm" by atomize_elim (rule Entry_reaches, auto)
    with assms have "n  set ns" by - (erule dominatesE)
    with ns show "ns. g  n-nsm" by - (rule path2_split_ex, auto)
  qed

  lemma dominates_antitrans:
    assumes[simp]: "invar g" and "dominates g n1 m" "dominates g n2 m"
    obtains (1) "dominates g n1 n2"
          | (2) "dominates g n2 n1"
  proof (cases "dominates g n1 n2")
    case False
    show thesis
    proof (rule 2, rule dominatesI)
      show "n1  set (αn g)" using assms(2) by simp
    next
      fix ns
      assume asm: "g  Entry g-nsn1"
      from assms(2) obtain ns2 where "g  n1-ns2m" by (rule dominates_path, simp)
      then obtain ns2' where ns2': "g  n1-ns2'm" "n1  set (tl ns2')" "set ns2'  set ns2" by (rule simple_path2)
      with asm have "g  Entry g-ns@tl ns2'm" by auto
      with assms(3) have "n2  set (ns@tl ns2')" by - (erule dominatesE)
      moreover have "n2  set (tl ns2')"
      proof
        assume "n2  set (tl ns2')"
        with ns2'(1,2) obtain ns3 where ns3: "g  n2-ns3m" "n1  set (tl ns3)"
          by - (erule path2_split_ex, auto simp: path2_not_Nil)
        have "dominates g n1 n2"
        proof
          show "n2  set (αn g)" using assms(3) by simp
        next
          fix ns'
          assume ns': "g  Entry g-ns'n2"
          with ns3(1) have "g  Entry g-ns'@tl ns3m" by auto
          with assms(2) have "n1  set (ns'@tl ns3)" by - (erule dominatesE)
          with ns3(2) show "n1  set ns'" by simp
        qed
        with False show False ..
      qed
      ultimately show "n2  set ns" by simp
    qed
  qed

  lemma dominates_extend:
    assumes "dominates g n m"
    assumes "g  m'-msm" "n  set (tl ms)"
    shows "dominates g n m'"
  proof (rule dominatesI)
    show "m'  set (αn g)" using assms(2) by auto
  next
    fix ms'
    assume "g  Entry g-ms'm'"
    with assms(2) have "g  Entry g-ms'@tl msm" by auto
    with assms(1) have "n  set (ms'@tl ms)" by - (erule dominatesE)
    with assms(3) show "n  set ms'" by auto
  qed

  definition dominators :: "'g  'node  'node set" where
    "dominators g n  {m  set (αn g). dominates g m n}"

  definition "isIdom g n m  strict_dom g m n  (m'  set (αn g). strict_dom g m' n  dominates g m' m)"
  definition idom :: "'g  'node  'node" where
    "idom g n  THE m. isIdom g n m"

  lemma idom_ex:
    assumes[simp]: "invar g" "n  set (αn g)" "n  Entry g"
    shows "∃!m. isIdom g n m"
  proof (rule ex_ex1I)
    let ?A = "λm. {m'  set (αn g). strict_dom g m' n  strict_dom g m m'}"

    have 1: "A m. finite A  A = ?A m  strict_dom g m n  m'. isIdom g n m'"
    proof-
      fix A m
      show "finite A  A = ?A m  strict_dom g m n  m'. isIdom g n m'"
      proof (induction arbitrary:m rule:finite_psubset_induct)
        case (psubset A m)
        show ?case
        proof (cases "A = {}")
          case True
          { fix m'
            assume asm: "strict_dom g m' n" and [simp]: "m'  set (αn g)"
            with True psubset.prems(1) have "¬(strict_dom g m m')" by auto
            hence "dominates g m' m" using dominates_antitrans[of g m' n m] asm psubset.prems(2) by fastforce
          }
          thus ?thesis using psubset.prems(2) by - (rule exI[of _ m], auto simp:isIdom_def)
        next
          case False
          then obtain m' where "m'  A" by auto
          with psubset.prems(1) have m': "m'  set (αn g)" "strict_dom g m' n" "strict_dom g m m'" by auto
          have "?A m'  ?A m"
          proof
            show "?A m'  ?A m" using m' by auto
            show "?A m'  ?A m" using m' dominates_antisymm[of g m m'] dominates_trans[of g m] by auto
          qed
          thus ?thesis by (rule psubset.IH[of _ m', simplified psubset.prems(1)], simp_all add: m')
        qed
      qed
    qed
    show "m. isIdom g n m" by (rule 1[of "?A (Entry g)"], auto)
  next
    fix m m'
    assume "isIdom g n m" "isIdom g n m'"
    thus "m = m'" by - (rule dominates_antisymm[of g], auto simp:isIdom_def)
  qed

  lemma idom: "invar g; n  set (αn g) - {Entry g}  isIdom g n (idom g n)"
  unfolding idom_def by (rule theI', rule idom_ex, auto)

  lemma dominates_mid:
    assumes "dominates g n x" "dominates g x m" "g  n-nsm" and[simp]: "invar g"
    shows "x  set ns"
  using assms
  proof (cases "n = x")
    case False
    from assms(1) obtain ns0 where ns0: "g  Entry g-ns0n" "n  set (butlast ns0)" by - (rule simple_Entry_path, auto)
    with assms(3) have "g  Entry g-butlast ns0@nsm" by auto
    with assms(2) have "x  set (butlast ns0@ns)" by (auto elim!:dominatesE)
    moreover have "x  set (butlast ns0)"
    proof
      assume asm: "x  set (butlast ns0)"
      with ns0 obtain ns0' where ns0': "g  Entry g-ns0'x" "n  set (butlast ns0')"
        by - (erule path2_split_ex, auto dest:in_set_butlastD simp: butlast_append split: if_split_asm)
      show False by (metis False assms(1) ns0' strict_domE)
    qed
    ultimately show ?thesis by simp
  qed auto

  definition shortestPath :: "'g  'node  nat" where
    "shortestPath g n  (LEAST l. ns. length ns = l  g  Entry g-nsn)"

  lemma shortestPath_ex:
    assumes "n  set (αn g)" "invar g"
    obtains ns where "g  Entry g-nsn" "distinct ns" "length ns = shortestPath g n"
  proof-
    from assms obtain ns where "g  Entry g-nsn" by - (atomize_elim, rule Entry_reaches)
    then obtain sns where sns: "length sns = shortestPath g n" "g  Entry g-snsn"
      unfolding shortestPath_def
      by -(atomize_elim, rule LeastI, auto)
    then obtain sns' where sns': "length sns'  shortestPath g n" "g  Entry g-sns'n" "distinct sns'" by - (rule simple_path2, auto)
    moreover from sns'(2) have "shortestPath g n  length sns'" unfolding shortestPath_def by - (rule Least_le, auto)
    ultimately show thesis by -(rule that, auto)
  qed

  lemma[simp]: "n  set (αn g); invar g  shortestPath g n  0"
    by (metis length_0_conv path2_not_Nil2 shortestPath_ex)

  lemma shortestPath_upper_bound:
    assumes "n  set (αn g)" "invar g"
    shows "shortestPath g n  length (αn g)"
  proof-
    from assms obtain ns where ns: "g  Entry g-nsn" "length ns = shortestPath g n" "distinct ns" by (rule shortestPath_ex)
    hence "shortestPath g n = length ns" by simp
    also have "... = card (set ns)" using ns(3) by (rule distinct_card[symmetric])
    also have "...  card (set (αn g))" using ns(1) by - (rule card_mono, auto)
    also have "...  length (αn g)" by (rule card_length)
    finally show ?thesis .
  qed

  lemma shortestPath_predecessor:
    assumes "n  set (αn g) - {Entry g}" and[simp]: "invar g"
    obtains n' where "Suc (shortestPath g n') = shortestPath g n" "n'  set (predecessors g n)"
  proof -
    from assms obtain sns where sns: "length sns = shortestPath g n" "g  Entry g-snsn"
      by - (rule shortestPath_ex, auto)
    let ?n' = "last (butlast sns)"
    from assms(1) sns(2) have 1: "length sns  2" by auto
    hence prefix: "g  Entry g-butlast snslast (butlast sns)  last (butlast sns)  set (predecessors g n)"
      using sns by -(rule path2_unsnoc, auto)
    hence "shortestPath g ?n'  length (butlast sns)"
      unfolding shortestPath_def by -(rule Least_le, rule exI[where x = "butlast sns"], simp)
    with 1 sns(1) have 2: "shortestPath g ?n' < shortestPath g n" by auto
    { assume asm: "Suc (shortestPath g ?n')  shortestPath g n"
      obtain sns' where sns': "g  Entry g-sns'?n'" "length sns' = shortestPath g ?n'"
        using prefix by - (rule shortestPath_ex, auto)
      hence[simp]: "g  Entry g-sns'@[n]n" using prefix by auto
      from asm 2 have "Suc (shortestPath g ?n') < shortestPath g n" by auto
      from this[unfolded shortestPath_def, THEN not_less_Least, folded shortestPath_def, simplified, THEN spec[of _ "sns'@[n]"]]
      have False using sns'(2) by auto
    }
    with prefix show thesis by - (rule that, auto)
  qed

  lemma successor_in_αn[simp]:
    assumes "predecessors g n  []" and[simp]: "invar g"
    shows "n  set (αn g)"
  proof-
    from assms(1) obtain m where "m  set (predecessors g n)" by (cases "predecessors g n", auto)
    with assms(1) obtain m' e where "(m',e,n)  αe g" using inEdges_correct[of g n, THEN arg_cong[where f="(`) getTo"]]
      by (auto simp: predecessors_def simp del: inEdges_correct)
    with assms(1) show ?thesis
      by (auto simp: predecessors_def)
  qed

  lemma shortestPath_single_predecessor:
    assumes "predecessors g n = [m]" and[simp]: "invar g"
    shows "shortestPath g m < shortestPath g n"
  proof-
    from assms(1) have "n  set (αn g) - {Entry g}"
      by (auto simp: predecessors_def Entry_unreachable)
    thus ?thesis by (rule shortestPath_predecessor, auto simp: assms(1))
  qed

  lemma strict_dom_shortestPath_order:
    assumes "strict_dom g n m" "m  set (αn g)" "invar g"
    shows "shortestPath g n < shortestPath g m"
  proof-
    from assms(2,3) obtain sns where sns: "g  Entry g-snsm" "length sns = shortestPath g m"
      by (rule shortestPath_ex)
    with assms(1) sns(1) obtain sns' where sns': "g  Entry g-sns'n" "prefix sns' sns" by -(erule path2_prefix_ex, auto elim:dominatesE)
    hence "shortestPath g n  length sns'"
      unfolding shortestPath_def by -(rule Least_le, auto)
    also have "length sns' < length sns"
    proof-
      from assms(1) sns(1) sns'(1) have "sns'  sns" by -(drule path2_last, drule path2_last, auto)
      with sns'(2) have "strict_prefix sns' sns" by auto
      thus ?thesis by (rule prefix_length_less)
    qed
    finally show ?thesis by (simp add:sns(2))
  qed

  lemma dominates_shortestPath_order:
    assumes "dominates g n m" "m  set (αn g)" "invar g"
    shows "shortestPath g n  shortestPath g m"
  using assms by (cases "n = m", auto intro:strict_dom_shortestPath_order[THEN less_imp_le])

  lemma strict_dom_trans:
    assumes[simp]: "invar g"
    assumes "strict_dom g n m" "strict_dom g m m'"
    shows "strict_dom g n m'"
  proof (rule, rule notI)
    assume "n = m'"
    moreover from assms(3) have "m'  set (αn g)" by auto
    ultimately have "dominates g m' n" by auto
    with assms(2) have "dominates g m' m" by - (rule dominates_trans, auto)
    with assms(3) show False by - (erule conjE, drule dominates_antisymm[OF assms(1)], auto)
  next
    from assms show "dominates g n m'" by - (rule dominates_trans, auto)
  qed

  inductive EntryPath :: "'g  'node list  bool" where
    EntryPath_triv[simp]: "EntryPath g [n]"
  | EntryPath_snoc[intro]: "EntryPath g ns  shortestPath g m = Suc (shortestPath g (last ns))  EntryPath g (ns@[m])"

  lemma[simp]:
    assumes "EntryPath g ns" "prefix ns' ns" "ns'  []"
    shows "EntryPath g ns'"
  using assms proof induction
    case (EntryPath_triv ns n)
    thus ?case by (cases ns', auto)
  qed auto

  lemma EntryPath_suffix:
    assumes "EntryPath g ns" "suffix ns' ns" "ns'  []"
    shows "EntryPath g ns'"
  using assms proof (induction arbitrary: ns')
    case EntryPath_triv
    thus ?case
      by (metis EntryPath.EntryPath_triv append_Nil append_is_Nil_conv list.sel(3) Sublist.suffix_def tl_append2)
  next
    case (EntryPath_snoc g ns m)
    from EntryPath_snoc.prems obtain ns'' where [simp]: "ns' = ns''@[m]"
      by - (erule suffix_unsnoc, auto)
    show ?case
    proof (cases "ns'' = []")
      case True
      thus ?thesis by auto
    next
      case False
      from EntryPath_snoc.prems(1) have "suffix ns'' ns" by (auto simp: Sublist.suffix_def)
      with False have "last ns'' = last ns" by (auto simp: Sublist.suffix_def)
      moreover from False have "EntryPath g ns''" using EntryPath_snoc.prems(1)
        by - (rule EntryPath_snoc.IH, auto simp: Sublist.suffix_def)
      ultimately show ?thesis using EntryPath_snoc.hyps(2)
        by - (simp, rule EntryPath.EntryPath_snoc, simp_all)
    qed
  qed

  lemma EntryPath_butlast_less_last:
    assumes "EntryPath g ns" "z  set (butlast ns)"
    shows "shortestPath g z < shortestPath g (last ns)"
  using assms proof (induction)
    case (EntryPath_snoc g ns m)
    thus ?case by (cases "z  set (butlast ns)", auto dest: not_in_butlast)
  qed simp

  lemma EntryPath_distinct:
    assumes "EntryPath g ns"
    shows "distinct ns"
  using assms
  proof (induction)
    case (EntryPath_snoc g ns m)
    from this consider (non_distinct) "m  set ns" | "distinct (ns @ [m])" by auto
    thus "distinct (ns @ [m])"
    proof (cases)
      case non_distinct
      have "EntryPath g (ns @ [m])" using EntryPath_snoc by (intro EntryPath.intros(2))
      with non_distinct
      have "False"
       using EntryPath_butlast_less_last butlast_snoc last_snoc less_not_refl by force
      thus ?thesis by simp
    qed
  qed simp

  lemma Entry_reachesE:
    assumes "n  set (αn g)" and[simp]: "invar g"
    obtains ns where "g  Entry g-nsn" "EntryPath g ns"
  using assms(1) proof (induction "shortestPath g n" arbitrary:n)
    case 0
    hence False by simp
    thus ?case..
  next
    case (Suc l)
    note Suc.prems(2)[simp]
    show ?case
    proof (cases "n = Entry g")
      case True
      thus ?thesis by - (rule Suc.prems(1), auto)
    next
      case False
      then obtain n' where n': "shortestPath g n' = l" "n'  set (predecessors g n)"
        using Suc.hyps(2)[symmetric] by - (rule shortestPath_predecessor, auto)
      moreover {
        fix ns
        assume asm: "g  Entry g-nsn'" "EntryPath g ns"
        hence thesis using n' Suc.hyps(2) path2_last[OF asm(1)]
          by - (rule Suc.prems(1)[of "ns@[n]"], auto)
      }
      ultimately show thesis by - (rule Suc.hyps(1), auto)
    qed
  qed
end

end

Theory SSA_CFG

(*  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-nsm  (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-nsm"
    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-nsm" "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 nsm" 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-nsm  (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
    show ?thesis unfolding phiUses_def by (rule UN_I[OF 1], rule UN_I[OF 2], auto simp:image_def Set.filter_def assms(3) 3)
  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 Set.filter_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-nsm" "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 nsm" 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-nsn" 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 "mset (α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-nsn"
      with m(1) have "m  set ns" by - (rule dominates_mid, auto)
      with m(2) show "nset 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-nsn" 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-nsm"
    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-nsm" "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-nsm" "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-nsn" "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-esn'"
    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-nsn" "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-nsm" "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-nsm" "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-nsdefNode 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-nsdefNode 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'2 m where ns'2: "g  defNode g p'-ns'2m" "m  set (predecessors g (defNode g p))" "defNode g p'  set (tl ns'2)" "p'  phiUses g m"
      by - (rule phiArg_path_ex', rule assms(3), auto intro: simple_path2)
    then obtain ns2 where ns2: "g  defNode g p'-ns2defNode g p" "length ns2 > 1" "ns2 = ns'2@[defNode g p]" by (atomize_elim, auto)

    show thesis
    proof (rule step.IH)
      fix ns
      assume ns: "g  defNode g q-nsdefNode g p'" "1 < length ns"
      assume IH: "nset (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 ns2"
      have ns_ns2: "g  defNode g q-?pathdefNode g p" "1 < length ?path" using ns ns2(1,2) by auto
      show thesis
      proof (rule step.prems(1)[OF ns_ns2, rule_format])
        fix n
        assume n: "n  set (butlast ?path)"
        show "p q m ns'a.
          r p q 
          g  defNode g q-ns'am 
          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 ns2 have 1: "?path = butlast ns@ns2"
            by - (rule concat_join[symmetric], auto simp: path2_def)
          from ns2(1) n False 1 have "n  set (butlast ns2)" by (auto simp: butlast_append path2_not_Nil)
          with step.hyps ns'2 ns2(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-nsn"
      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: "
g  n-nsm; 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-nsm; 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-nsm; 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-nsn"
    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-nsdefNode 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-nsn" "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-nsn" "defNode g p  set (tl ns)" "p  allUses g n"
    assumes q: "g  defNode g q-msm" "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-nsn" "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-nsn" "defNode g p  set (tl ns)" "p  allUses g n" "old.dominates g ?P y" "y  set ns"
      assume q: "g  defNode g q-msm" "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 ns2 where ns2: "g  y-ns2n" "suffix ns2 ns" by - (rule old.path2_split_first_last, auto)
      from q obtain ms1 where ms1: "g  ?Q-ms1y" "prefix ms1 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 ms1)@tl ns2"
        show "g  ?P-?pathn" using pqs ms1 ns2
          by (auto simp del:append_assoc intro:old.path2_app)
        have "?P  set (tl ns2)" using p(2) ns2(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 ms1)" using ms1(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-nsm" "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-nsm" "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-nsm" "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 nsm"
        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

Theory Minimality

(*  Title:      Minimality.thy
    Author:     Sebastian Ullrich
*)

section ‹Minimality›

text ‹We show that every reducible CFG without trivial \pf s is minimal, recreating the proof in~\cite{braun13cc}.
  The original proof is inlined as prose text.›

theory Minimality
imports SSA_CFG Serial_Rel
begin

context graph_path
begin
  text ‹Cytron's definition of path convergence›
  definition "pathsConverge g x xs y ys z  g  x-xsz  g  y-ysz  length xs > 1  length ys > 1  x  y 
    (j  {0..< length xs}. k  {0..<length ys}. xs ! j = ys ! k  j = length xs - 1  k = length ys - 1)"

  text ‹Simplified definition›
  definition "pathsConverge' g x xs y ys z  g  x-xsz  g  y-ysz  length xs > 1  length ys > 1  x  y 
    set (butlast xs)  set (butlast ys) = {}"

  lemma pathsConverge'[simp]: "pathsConverge g x xs y ys z  pathsConverge' g x xs y ys z"
  proof-
    have "(j  {0..< length xs}. k  {0..<length ys}. xs ! j = ys ! k  j = length xs - 1  k = length ys - 1)
           (x'  set (butlast xs). y'  set (butlast ys). x'  y')"
    proof
      assume 1: "j{0..<length xs}. k{0..<length ys}. xs ! j = ys ! k  j = length xs - 1  k = length ys - 1"
      show "x'set (butlast xs). y'set (butlast ys). x'  y'"
      proof (rule, rule, rule)
        fix x' y'
        assume 2: "x'  set (butlast xs)" "y'  set (butlast ys)" and[simp]: "x' = y'"
        from 2(1) obtain j where j: "xs ! j = x'" "j < length xs - 1" by (rule butlast_idx)
        moreover from j have "j < length xs" by simp
        moreover from 2(2) obtain k where k: "ys ! k = y'" "k < length ys - 1" by (rule butlast_idx)
        moreover from k have "k < length ys" by simp
        ultimately show False using 1[THEN bspec[where x=j], THEN bspec[where x=k]] by auto
      qed
    next
      assume 1: "x'set (butlast xs). y'set (butlast ys). x'  y'"
      show "j{0..<length xs}. k{0..<length ys}. xs ! j = ys ! k  j = length xs - 1  k = length ys - 1"
      proof (rule, rule, rule, simp)
        fix j k
        assume 2: "j < length xs" "k < length ys" "xs ! j = ys ! k"
        show "j = length xs - Suc 0  k = length ys - Suc 0"
        proof (rule ccontr, simp)
          assume 3: "j  length xs - Suc 0  k  length ys - Suc 0"
          let ?x' = "xs ! j"
          let ?y' = "ys ! k"
          from 2(1) 3 have "?x'  set (butlast xs)" by - (rule butlast_idx', auto)
          moreover from 2(2) 3 have "?y'  set (butlast ys)" by - (rule butlast_idx', auto)
          ultimately have "?x'  ?y'" using 1 by simp
          with 2(3) show False by simp
        qed
      qed
    qed
    thus ?thesis by (auto simp:pathsConverge_def pathsConverge'_def)
  qed

  lemma pathsConvergeI:
    assumes "g  x-xsz" "g  y-ysz" "length xs > 1" "length ys > 1" "set (butlast xs)  set (butlast ys) = {}"
    shows "pathsConverge g x xs y ys z"
  proof-
    from assms have "x  y"
      by (metis append_is_Nil_conv disjoint_iff_not_equal length_butlast list.collapse list.distinct(1) nth_Cons_0 nth_butlast nth_mem path2_def split_list zero_less_diff)
    with assms show ?thesis by (simp add:pathsConverge'_def)
  qed
end

text ‹A (control) flow graph G is reducible iff for each cycle C of G there is a node of C that dominates all other nodes in C.›
definition (in graph_Entry) "reducible g  n ns. g  n-nsn  (m  set ns. n  set ns. dominates g m n)"

context CFG_SSA_Transformed
begin
  text ‹A $\phi$ function for variable v is necessary in block Z iff two non-null paths $X \rightarrow^+ Z$ and $Y \rightarrow^+ Z$ converge at a block Z,
    such that the blocks X and Y contain assignments to v.›
  definition "necessaryPhi g v z  n ns m ms. old.pathsConverge g n ns m ms z  v  oldDefs g n  v  oldDefs g m"
  abbreviation "necessaryPhi' g val  necessaryPhi g (var g val) (defNode g val)"
  definition "unnecessaryPhi g val  phi g val  None  ¬necessaryPhi' g val"

  lemma necessaryPhiI: "old.pathsConverge g n ns m ms z  v  oldDefs g n  v  oldDefs g m  necessaryPhi g v z"
    by (auto simp: necessaryPhi_def)

  text ‹A program with only necessary $\phi$ functions is in minimal SSA form.›
  definition "cytronMinimal g  v  allVars g. phi g v  None  necessaryPhi' g v"

  text ‹Let p be a $\phi$ function in a block P. Furthermore, let q in a block Q
and r in a block R be two operands of p, such that p, q and r are pairwise distinct.
Then at least one of Q and R does not dominate P.›
  lemma 2:
    assumes "phiArg g p q" "phiArg g p r" "distinct [p, q, r]" and[simp]: "p  allVars g"
    shows "¬(def_dominates g q p  def_dominates g r p)"
  proof (rule, erule conjE)
    txt ‹Proof. Assume that Q and R dominate P, i.e., every path from the start block to P contains Q and R.›
    assume asm: "def_dominates g q p" "def_dominates g r p"

    txt ‹Since immediate dominance forms a tree, Q dominates R or R dominates Q.›
    hence "def_dominates g q r  def_dominates g r q"
      by - (rule old.dominates_antitrans[of g "defNode g q" "defNode g p" "defNode g r"], auto)
    moreover
    {
      txt ‹Without loss of generality, let Q dominate R.›
      fix q r
      assume assms: "phiArg g p q" "phiArg g p r" "distinct [p, q, r]"
      assume asm: "def_dominates g q p" "def_dominates g r p"
      assume wlog: "def_dominates g q r"

      have[simp]: "var g q = var g r" using phiArg_same_var[OF assms(1)] phiArg_same_var[OF assms(2)] by simp

      txt ‹Furthermore, let S be the corresponding predecessor block of P where p is using q.›
      obtain S where S: "q  phiUses g S" "S  set (old.predecessors g (defNode g p))" by (rule phiUses_exI'[OF assms(1)], simp)

      txt ‹Then there is a path from the start block crossing Q then R and S.›
      have "defNode g p  defNode g q" using assms(1,3)
        by - (rule phiArg_distinct_nodes, auto)
      with S have "old.dominates g (defNode g q) S"
        by - (rule allUses_dominated, auto)
      then obtain ns where ns: "g  defNode g q-nsS" "distinct ns"
        by (rule old.dominates_path, auto elim: old.simple_path2)
      moreover have "defNode g r  set (tl ns)"
      proof-
        have "defNode g r  defNode g q" using assms
          by - (rule phiArgs_def_distinct, auto)
        hence "hd ns  defNode g r" using ns by (auto simp:old.path2_def)
        moreover
        have "defNode g p  defNode g r" using assms(2,3)
          by - (rule phiArg_distinct_nodes, auto)
        with S(2) have "old.dominates g (defNode g r) S"
          by - (rule old.dominates_unsnoc[where m="defNode g p"], auto simp:wlog asm assms)
        with wlog have "defNode g r  set ns" using ns(1)
          by (rule old.dominates_mid, auto)
        ultimately
        show ?thesis by (metis append_Nil in_set_conv_decomp list.sel(1) tl_append2)
      qed

      txt ‹This violates the SSA property.›
      moreover have "q  allDefs g (defNode g q)" using assms S(1) by simp
      moreover have "r  allDefs g (defNode g r)" using assms S(1) by simp
      ultimately have "var g r  var g q" using S(1)
        by - (rule conventional, auto simp:old.path2_def distinct_hd_tl)
      hence False by simp
    }
    ultimately show False using assms asm by auto
  qed

  lemma convergence_prop:
    assumes "necessaryPhi g (var g v) n" "g  n-nsm" "v  allUses g m" "x. x  set (tl ns)  v  allDefs g x" "v  defs g n"
    shows "phis g (n,v)  None"
  proof
    from assms(2, 3) have "v  allVars g" by auto
    hence 1: "v  allDefs g (defNode g v)" by (rule defNode)

    assume "phis g (n,v) = None"
    with assms(5) have 2: "v  allDefs g n"
      by (auto simp:allDefs_def phiDefs_def)

    from assms(1) obtain a as b bs va vb where
      a: "va  defs g a" "var g va = var g v" and
      b: "vb  defs g b" "var g vb = var g v"
      and conv: "g  a-asn" "g  b-bsn" "1 < length as" "1 < length bs" "a  b" "set (butlast as)  set (butlast bs) = {}"
      by (auto simp:necessaryPhi_def old.pathsConverge'_def oldDefs_def)
    have "old.dominates g (defNode g v) m" using assms(2,3)
      by - (rule allUses_dominated, auto)
    hence dom: "old.dominates g (defNode g v) n" using assms(2,4) 1
      by - (rule old.dominates_unsnoc', auto)
    hence "old.strict_dom g (defNode g v) n" using 1 2 by auto

    {
      fix va a as vb b bs
      assume a: "va  defs g a" "var g va = var g v"
      assume as: "g  a-asn" "length as > 1"
      assume b: "vb  defs g b" "var g vb = var g v"
      assume bs: "g  b-bsn"
      assume conv: "a  b" "set (butlast as)  set (butlast bs) = {}"
      have 3: "defNode g v  a"
      proof
        assume contr: "defNode g v = a"

        have "a  set (butlast as)" using as by (auto simp:old.path2_def intro:hd_in_butlast)
        hence "a  set (butlast bs)" using conv(2) by auto
        moreover
        have "a  n" using 1 2 contr by auto
        hence "a  last bs" using bs by (auto simp:old.path2_def)
        ultimately have 4: "a  set bs"
          by - (subst append_butlast_last_id[symmetric], rule old.path2_not_Nil[OF bs], auto)

        have "v  va"
        proof
          assume asm: "v = va"
          have "v  vb"
          proof
            assume "v = vb"
            with asm[symmetric] b(1) have "va  allDefs g b" by simp
            with asm have "a = b" using as bs a(1) by - (rule allDefs_disjoint', auto)
            with conv(1) show False by simp
          qed
          obtain ebs where ebs: "g  Entry g-ebsb"
            using bs by (atomize, auto)
          hence "g  Entry g-butlast ebs@bsn" using bs by auto
          hence 5: "a  set (butlast ebs@bs)"
            by - (rule old.dominatesE[OF dom[simplified contr]])
          show False
          proof (cases "a  set (butlast ebs)")
            case True
            hence "a  set ebs" by (rule in_set_butlastD)
            with ebs obtain abs where abs: "g  a-absb" "a  set (tl abs)"
              by (rule old.path2_split_first_last, auto)
            let ?path = "(abs@tl bs)@tl ns"
            have "var g vb  var g va"
            proof (rule conventional)
              show "g  a-?pathm" using abs(1) bs assms(2)
                by - (rule old.path2_app, rule old.path2_app)
              have "a  set (tl bs)" using 4 by (auto simp:in_set_tlD)
              moreover have "a  set (tl ns)" using 1 2 contr assms(4) by auto
              ultimately show "a  set (tl ?path)" using abs conv(2)
                by - (subst tl_append2, auto simp: old.path2_not_Nil)
              show "va  allUses g m" using asm assms(3) by simp
              have "b  set (tl abs)" using abs(1) conv(1)
                by (auto simp:old.path2_def intro!:last_in_tl nonsimple_length_gt_1)
              thus "b  set (tl ?path)" using abs(1) by (simp add: old.path2_not_Nil)
            qed (simp_all add: a b)
            thus False using a b by simp
          next
            case False
            with 4 5 show False by simp
          qed
        qed
        hence "var g v  var g va" using a as 1 contr by - (rule allDefs_var_disjoint, auto)
        with a(2) show False by simp
      qed
      obtain eas where eas: "g  Entry g-easa"
        using as by (atomize, auto)
      hence "g  Entry g-eas@tl asn" using as by auto
      hence 4: "defNode g v  set (eas@tl as)" by - (rule old.dominatesE[OF dom])

      have "defNode g v  set (tl as)"
      proof (rule ccontr)
        assume asm: "defNode g v  set (tl as)"
        with 4 have "defNode g v  set eas" by simp
        then obtain eas' where eas': "g  defNode g v-defNode g v#eas'a" "defNode g v  set eas'" using eas
          by - (rule old.path2_split_first_last)
        let ?path = "((defNode g v#eas')@tl as)@tl ns"
        have "var g va  var g v"
        proof (rule conventional)
          show "g  defNode g v-?pathm" using eas' as assms(2)
            by (auto simp del:append_Cons append_assoc intro: old.path2_app)
          show "a  set (tl ?path)" using eas' 3 by (auto simp:old.path2_def)
          show "defNode g v  set (tl ?path)" using assms(4) 1 eas'(2) asm by auto
        qed (simp_all add:1 assms(3) a(1))
        with a(2) show False by simp
      qed
      moreover have "defNode g v  n" using 1 2 by auto
      ultimately have "defNode g v  set (butlast as)" using as subsetD[OF set_tl, of "defNode g v" as]
        by - (rule in_set_butlastI, auto simp:old.path2_def)
    }
    note def_in_as = this
    from def_in_as[OF a conv(1,3) b conv(2)] def_in_as[OF b conv(2,4) a conv(1)] conv(5,6) show False by auto
  qed

  lemma convergence_prop':
    assumes "necessaryPhi g v n" "g  n-nsm" "v  var g ` allUses g m" "x. x  set ns  v  oldDefs g x"
    obtains val where "var g val = v" "phis g (n,val)  None"
  using assms proof (induction "length ns" arbitrary: ns m rule: less_induct)
    case less
    from less.prems(4) obtain val where val: "var g val = v" "val  allUses g m" by auto
    show ?thesis
    proof (cases "m'  set (tl ns). v  var g ` phiDefs g m'")
      case False
      with less.prems(5) have "x. x  set (tl ns)  val  allDefs g x"
        by (auto simp: allDefs_def val(1)[symmetric] oldDefs_def dest: in_set_tlD)
      moreover from less.prems(3,5) have "val  defs g n"
        by (auto simp: oldDefs_def val(1)[symmetric] dest: old.path2_hd_in_ns)
      ultimately show ?thesis
        using less.prems
        by - (rule that[OF val(1)], rule convergence_prop, auto simp: val)
    next
      case True
      with less.prems(3) obtain ns' m' where m': "g  n-ns'm'" "v  var g ` phiDefs g m'" "prefix ns' ns"
        by - (erule old.path2_split_first_prop[where P="λm. v  var g ` phiDefs g m"], auto dest: in_set_tlD)
      show ?thesis
      proof (cases "m' = n")
        case True
        with m'(2) show ?thesis by (auto simp: phiDefs_def intro: that)
      next
        case False
        with m'(1) obtain m'' where m'': "g  n-butlast ns'm''" "m''  set (old.predecessors g m')"
          by - (rule old.path2_unsnoc, auto)
        show ?thesis
        proof (rule less.hyps[of "butlast ns'", OF _])
          show "length (butlast ns') < length ns"
            using m''(1) m'(3) by (cases "length ns'", auto dest: prefix_length_le)

          from m'(2) obtain val vs where vs: "phis g (m',val) = Some vs" "var g val = v"
            by (auto simp: phiDefs_def)
          with m'' obtain val' where "val'  phiUses g m''" "val'  set vs"
            by - (rule phiUses_exI, auto simp: phiDefs_def)
          with vs have "val'  allUses g m''" "var g val' = v" by auto
          then show "v  var g ` allUses g m''" by auto

          from m'(3) show "x. x  set (butlast ns')  v  oldDefs g x"
            by - (rule less.prems(5), auto elim: in_set_butlastD)
        qed (auto intro: less.prems(1,2) m''(1))
      qed
    qed
  qed

  lemma nontrivialE:
    assumes "¬trivial g p" "phi g p  None" and[simp]: "p  allVars g"
    obtains r s where "phiArg g p r" "phiArg g p s" "distinct [p, r, s]"
  proof-
    from assms(2) obtain vs where vs: "phi g p = Some vs" by auto
    have "card (set vs - {p})  2"
    proof-
      have "card (set vs)  0" using Entry_no_phis[of g p] phi_wf[OF vs] vs by (auto simp:phi_def invar)
      moreover have "set vs  {p}" using vs by - (rule phi_no_closed_loop, auto)
      ultimately have "card (set vs - {p})  0"
        by (metis List.finite_set card_0_eq insert_Diff_single insert_absorb removeAll_id set_removeAll)
      moreover have "card (set vs - {p})  1"
      proof
        assume "card (set vs - {p}) = 1"
        then obtain q where q: "{q} = set vs - {p}" by - (erule card_eq_1_singleton, auto)
        hence "isTrivialPhi g p q" using vs by (auto simp:isTrivialPhi_def split:option.split)
        moreover have "phiArg g p q" using q vs unfolding phiArg_def by auto
        ultimately show False using assms(1) by (auto simp:trivial_def)
      qed
      ultimately show ?thesis by arith
    qed
    then obtain r s where rs: "r  s" "r  set vs - {p}" "s  set vs - {p}" by (rule set_take_two)
    thus ?thesis using vs by - (rule that[of r s], auto simp: phiArg_def)
  qed

  lemma paths_converge_prefix:
    assumes "g  x-xsz" "g  y-ysz" "x  y" "length xs > 1" "length ys > 1" "x  set (butlast ys)" "y  set (butlast xs)"
    obtains xs' ys' z' where "old.pathsConverge g x xs' y ys' z'" "prefix xs' xs" "prefix ys' ys"
  using assms proof (induction "length xs" arbitrary:xs ys z rule:nat_less_induct)
    case 1
    from "1.prems"(3,4) have 2: "x  y" by (auto simp:old.path2_def)
    show thesis
    proof (cases "set (butlast xs)  set (butlast ys) = {}")
      case True
      with "1.prems"(2-) have "old.pathsConverge g x xs y ys z" by (auto simp add: old.pathsConverge'_def)
      thus thesis by (rule "1.prems"(1), simp_all)
    next
      case False
      then obtain xs' z' where xs': "g  x-xs'z'" "prefix xs' (butlast xs)" "z'  set (butlast ys)" "a  set (butlast xs'). a  set (butlast ys)"
        using "1.prems"(2,5) by - (rule old.path2_split_first_prop[of g x "butlast xs" _ "λa. a  set (butlast ys)"], auto elim: old.path2_unsnoc)
      from xs'(3) "1.prems"(3) obtain ys' where ys': "g  y-ys'z'" "strict_prefix ys' ys"
        by - (rule old.path2_strict_prefix_ex)
      show ?thesis
      proof (rule "1.hyps"[rule_format, OF _ _ _ xs'(1) ys'(1) assms(3)])
        show "length xs' < length xs" using xs'(2) xs'(1)
          by - (rule prefix_length_less, rule strict_prefix_butlast, auto)
        from "1.prems"(1) prefix_order.dual_order.strict_implies_order prefix_order.dual_order.trans
          prefix_butlastD xs'(2) ys'(2)
        show "xs'' ys'' z''. old.pathsConverge g x xs'' y ys'' z''  prefix xs'' xs'  prefix ys'' ys'  thesis"
          by blast
        show "length xs' > 1"
        proof-
          have "length xs'  0" using xs' by auto
          moreover {
            assume "length xs' = 1"
            with xs'(1,3) have "x  set (butlast ys)"
              by (auto simp:old.path2_def simp del:One_nat_def dest!:singleton_list_hd_last)
            with "1.prems"(7) have False ..
          }
          ultimately show ?thesis by arith
        qed

        show "length ys' > 1"
        proof-
          have "length ys'  0" using ys' by auto
          moreover {
            assume "length ys' = 1"
            with ys'(1) xs'(1,2) have "y  set (butlast xs)"
              by (auto simp:old.path2_def old.path_not_Nil simp del:One_nat_def dest!:singleton_list_hd_last)
            with "1.prems"(8) have False ..
          }
          ultimately show ?thesis by arith
        qed

        show "y  set (butlast xs')"
          using  xs'(2) "1.prems"(8)
          by (metis in_prefix in_set_butlastD)
        show "x  set (butlast ys')"
          by (metis "1.prems"(7) in_set_butlast_appendI strict_prefixE' ys'(2))
      qed simp
    qed
  qed

  lemma ununnecessaryPhis_disjoint_paths_aux:
    assumes "¬unnecessaryPhi g r" and[simp]: "r  allVars g"
    obtains n1 ns1 n2 ns2 where
      "var g r  oldDefs g n1" "g  n1-ns1defNode g r" and
      "var g r  oldDefs g n2" "g  n2-ns2defNode g r" and
      "set (butlast ns1)  set (butlast ns2) = {}"
  proof (cases "phi g r")
    case None
    thus thesis by - (rule that[of "defNode g r" _ "defNode g r"], auto intro!: oldDefsI intro: defNode_cases[of r g])
  next
    case Some
    with assms that show ?thesis by (auto simp: unnecessaryPhi_def necessaryPhi_def old.pathsConverge'_def)
  qed

  lemma ununnecessaryPhis_disjoint_paths:
    assumes "¬unnecessaryPhi g r" "¬unnecessaryPhi g s"
      (* and rs: "phiArg p r" "phiArg p s" "distinct [p, r, s]" *)
      and rs: "defNode g r  defNode g s"
      and[simp]: "r  allVars g" "s  allVars g" "var g r = V" "var g s = V"
    obtains n ns m ms where "V  oldDefs g n" "g  n-nsdefNode g r" and "V  oldDefs g m" "g  m-msdefNode g s"
        and "set ns  set ms = {}"
  proof-
    obtain n1 ns1 n2 ns2 where
      ns1: "V  oldDefs g n1" "g  n1-ns1defNode g r" "defNode g r  set (butlast ns1)" and
      ns2: "V  oldDefs g n2" "g  n2-ns2defNode g r" "defNode g r  set (butlast ns2)" and
      ns: "set (butlast ns1)  set (butlast ns2) = {}"
    proof-
      from assms obtain n1 ns1 n2 ns2 where
        ns1: "V  oldDefs g n1" "g  n1-ns1defNode g r" and
        ns2: "V  oldDefs g n2" "g  n2-ns2defNode g r" and
        ns: "set (butlast ns1)  set (butlast ns2) = {}"
      by - (rule ununnecessaryPhis_disjoint_paths_aux, auto)

      from ns1 obtain ns1' where ns1': "g  n1-ns1'defNode g r" "defNode g r  set (butlast ns1')" "distinct ns1'" "set ns1'  set ns1"
        by (auto elim: old.simple_path2)
      from ns2 obtain ns2' where ns2': "g  n2-ns2'defNode g r" "defNode g r  set (butlast ns2')" "distinct ns2'" "set ns2'  set ns2"
        by (auto elim: old.simple_path2)

      have "set (butlast ns1')  set (butlast ns2') = {}"
      proof (rule equals0I)
        fix x
        assume 1: "x  set (butlast ns1')  set (butlast ns2')"
        with set_butlast_distinct[OF ns1'(3)] ns1'(1) have 2: "x  defNode g r" by (auto simp:old.path2_def)
        with 1 ns1'(4) ns2'(4) ns1(2) ns2(2) have "x  set (butlast ns1)" "x  set (butlast ns2)"
          by - (auto intro!:in_set_butlastI elim:in_set_butlastD simp:old.path2_def)
        with ns show False by auto
      qed

      thus thesis by (rule that[OF ns1(1) ns1'(1,2) ns2(1) ns2'(1,2)])
    qed

    obtain m ms where ms: "V  oldDefs g m" "g  m-msdefNode g s" "defNode g r  set ms"
    proof-
      from assms(2) obtain m1 ms1 m2 ms2 where
        ms1: "V  oldDefs g m1" "g  m1-ms1defNode g s" and
        ms2: "V  oldDefs g