# 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"

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)

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)"
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)

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 "∃m∈UNIV.¬ 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

case_option (Mapping.lookup m1 k) Some (Mapping.lookup m2 k)"

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 - {k∈Mapping.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 (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)"

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-ns→m ⟹ 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-ns→m ⟹ 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-ns→m; n' ∈ set (predecessors g n)⟧ ⟹ g ⊢ n'-n'#ns→m"
unfolding path2_def by auto

lemma path2_cases:
assumes "g ⊢ n-ns→m"
obtains (empty_path) "ns = [n]" "m = n"
| (Cons_path) "g ⊢ hd (tl ns)-tl ns→m" "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-ns→m"
assumes empty: "invar g ⟹ P m [m] m"
assumes Cons: "⋀ns n' n. g ⊢ n-ns→m ⟹ 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-ns→m; l ∈ set ns⟧ ⟹ l ∈ set (αn g)"
unfolding path2_def by auto

lemma path2_hd_in_αn[elim]: "g ⊢ n-ns→m ⟹ n ∈ set (αn g)"
unfolding path2_def by auto

lemma path2_tl_in_αn[elim]: "g ⊢ n-ns→m ⟹ m ∈ set (αn g)"
unfolding path2_def by auto

lemma path2_forget_hd[simp]: "g ⊢ n-ns→m ⟹ g ⊢ hd ns-ns→m"
unfolding path2_def by simp

lemma path2_forget_last[simp]: "g ⊢ n-ns→m ⟹ g ⊢ n-ns→last 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-ns→m" "x ∈ set ns"
obtains ns⇩1 ns⇩2 where "g ⊢ n-ns⇩1→x" "g ⊢ x-ns⇩2→m" "ns = ns⇩1@tl ns⇩2" "ns = butlast ns⇩1@ns⇩2"
proof-
from assms(2) obtain ns⇩1 ns⇩2 where "ns = ns⇩1@x#ns⇩2" 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-ns→m" "x ∈ set ns"
obtains ns⇩1 ns⇩2 where "g ⊢ n-ns⇩1→x" "g ⊢ x-ns⇩2→m" "ns = butlast ns⇩1@ns⇩2"
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-ns→m" "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-ns→m" "length ns ≥ 2"
obtains "g ⊢ n-butlast ns→last (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-ns→m"
assumes empty: "n ∈ set (αn g) ⟹ P n [n] n"
assumes snoc: "⋀ns m' m. g ⊢ n-ns→m' ⟹ 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-ns→m ⟹ n = hd ns"
unfolding path2_def by simp

lemma path2_hd_in_ns[elim]: "g ⊢ n-ns→m ⟹ n ∈ set ns"
unfolding path2_def by auto

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

lemma path2_last_in_ns[elim]: "g ⊢ n-ns→m ⟹ 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-ns→m" "g ⊢ m-ms→l"
shows "g ⊢ n-ns@tl ms→l"
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-ns→m" "g ⊢ m-ms→l"
shows "g ⊢ n-butlast ns@ms→l"
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 ms→l" by (rule path2_app)
ultimately show ?thesis by simp
qed

lemma path2_nontrivial[elim]:
assumes "g ⊢ n-ns→m" "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-ns→m"
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'⇩2→m" 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-ns→m"
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-ns→m" "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-ns→m" "x ∈ set ns"
obtains ns⇩1 ns⇩3 ns⇩2 where "ns = ns⇩1@ns⇩3@ns⇩2" "prefix (ns⇩1@[x]) ns" "suffix (x#ns⇩2) ns"
and "g ⊢ n-ns⇩1@[x]→x"  "x ∉ set ns⇩1"
and "g ⊢ x-ns⇩3→x"
and "g ⊢ x-x#ns⇩2→m" "x ∉ set ns⇩2"
proof-
from assms(2) obtain ns⇩1 ns' where 1: "ns = ns⇩1@x#ns'" "x ∉ set ns⇩1" by (atomize_elim, rule split_list_first)
from assms(1)[unfolded 1(1)] have 2: "g ⊢ n-ns⇩1@[x]→x" "g ⊢ x-x#ns'→m" by - (erule path2_split, erule path2_split)
obtain ns⇩3 ns⇩2 where 3: "x#ns' = ns⇩3@x#ns⇩2" "x ∉ set ns⇩2" by (atomize_elim, rule split_list_last, simp)
from 2(2)[unfolded 3(1)] have 4: "g ⊢ x-ns⇩3@[x]→x" "g ⊢ x-x#ns⇩2→m" by - (erule path2_split, erule path2_split)
show thesis
proof (rule that[OF _ _ _ 2(1) 1(2) 4 3(2)])
show "ns = ns⇩1 @ (ns⇩3 @ [x]) @ ns⇩2" using 1(1) 3(1) by simp
show "prefix (ns⇩1@[x]) ns" using 1 by auto
show "suffix (x#ns⇩2) ns" using 1 3 by (metis Sublist.suffix_def suffix_order.order_trans)
qed
qed

lemma path2_simple_loop:
assumes "g ⊢ n-ns→n" "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 ns→m" "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 ns⇩1 ns⇩2 where split: "g ⊢ m'-ns⇩1→n" "g ⊢ n-ns⇩2→m" "?ns' = ns⇩1@tl ns⇩2" "?ns' = butlast ns⇩1@ns⇩2"
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#ns⇩1@tl ns⇩2@[n]" "ns = n#butlast ns⇩1@ns⇩2@[n]" using split(3,4) by auto
show ?thesis
proof (cases "n' ∈ set (n#ns⇩1)")
case True
show ?thesis
proof (rule "1.hyps"[rule_format, of _ "n#ns⇩1"])
show "length (n#ns⇩1) < length ns" using split'(1) by auto
show "n' ∈ set (n#ns⇩1)" 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 (ns⇩2@[n])" by auto
show ?thesis
proof (rule "1.hyps"[rule_format, of _ "ns⇩2@[n]"])
show "length (ns⇩2@[n]) < length ns" using split'(2) by auto
show "n' ∈ set (ns⇩2@[n])" by (rule 5)
show "g ⊢ n-ns⇩2@[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-ns→m" "∃x∈set 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-ns→m" "∃x∈set 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-ns→m"
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-ns→m" "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-ns→m" "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-ns→m; 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-ns→m ⟶ 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-ns→n"
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-ns→Entry 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-ns→n" and "n ∉ set (butlast ns)"
proof-
from assms obtain ns where p: "g ⊢ Entry g-ns→n" 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-ns→m⟧ ⟹ 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-ns→m ⟹ 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-ns→m" 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-ns→m ⟹ 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-ns→n''"
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-ns→n" 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-ns→m'"
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'-ms→m" "∀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'"
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-ns→m"
proof atomize_elim
from assms obtain ns where ns: "g ⊢ Entry g-ns→m" by atomize_elim (rule Entry_reaches, auto)
with assms have "n ∈ set ns" by - (erule dominatesE)
with ns show "∃ns. g ⊢ n-ns→m" by - (rule path2_split_ex, auto)
qed

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

lemma dominates_extend:
assumes "dominates g n m"
assumes "g ⊢ m'-ms→m" "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 ms→m" 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-ns→m" and[simp]: "invar g"
shows "x ∈ set ns"
using assms
proof (cases "n = x")
case False
from assms(1) obtain ns⇩0 where ns⇩0: "g ⊢ Entry g-ns⇩0→n" "n ∉ set (butlast ns⇩0)" by - (rule simple_Entry_path, auto)
with assms(3) have "g ⊢ Entry g-butlast ns⇩0@ns→m" by auto
with assms(2) have "x ∈ set (butlast ns⇩0@ns)" by (auto elim!:dominatesE)
moreover have "x ∉ set (butlast ns⇩0)"
proof
assume asm: "x ∈ set (butlast ns⇩0)"
with ns⇩0 obtain ns⇩0' where ns⇩0': "g ⊢ Entry g-ns⇩0'→x" "n ∉ set (butlast ns⇩0')"
by - (erule path2_split_ex, auto dest:in_set_butlastD simp: butlast_append split: if_split_asm)
show False by (metis False assms(1) ns⇩0' 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-ns→n)"

lemma shortestPath_ex:
assumes "n ∈ set (αn g)" "invar g"
obtains ns where "g ⊢ Entry g-ns→n" "distinct ns" "length ns = shortestPath g n"
proof-
from assms obtain ns where "g ⊢ Entry g-ns→n" by - (atomize_elim, rule Entry_reaches)
then obtain sns where sns: "length sns = shortestPath g n" "g ⊢ Entry g-sns→n"
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-ns→n" "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-sns→n"
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 sns→last (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-sns→m" "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-ns→n" "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-ns→n'" "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-ns→m ⟶ (∃n ∈ set ns. v ∈ defs g n))"

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

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

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

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

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

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

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

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

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

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

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

subsection ‹SSA CFG›

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

declare in_set_zipE[elim]
declare zip_same[simp]

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

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

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

lemmas CFG_SSA_defs = phiDefs_def allDefs_def phiUses_def allUses_def allVars_def defAss_def
end

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

lemma allDefs_disjoint': "⟦n ∈ set (αn g); m ∈ set (αn g); v ∈ allDefs g n; v ∈ allDefs g m⟧ ⟹ n = m"
using allDefs_disjoint by auto

lemma phiUsesI:
assumes "n' ∈ set (αn g)" "phis g (n',v') = Some vs" "(n,v) ∈ set (zip (predecessors g n') vs)"
shows "v ∈ phiUses g n"
proof-
from assms(3) have "n ∈ set (predecessors g n')" by auto
hence 1: "n' ∈ set (successors g n)" using assms(1) by simp
from assms(2) have 2: "v' ∈ phiDefs g n'" by (auto simp add:phiDefs_def)
from assms(2) have 3: "the (phis g (n',v')) = vs" by simp
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-ns→m" "∀n ∈ set (tl ns). v ∉ allDefs g n"
shows "defAss g n v"
unfolding defAss_def proof (rule allI, rule impI)
fix ns'
assume "g ⊢ Entry g-ns'→n"
with assms(2) have "g ⊢ Entry g-ns'@tl ns→m" by auto
with assms(1) obtain n' where n': "n' ∈ set (ns'@tl ns)" "v ∈ allDefs g n'" by (auto dest:defAssD)
with assms(3) have "n' ∉ set (tl ns)" by auto
with n' show "∃n ∈ set ns'. v ∈ allDefs g n" by auto
qed

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma phi_Entry_empty[simp]: "defNode g v = Entry g ⟹ phi g v = None"

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

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

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

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

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

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

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

lemma phi_wf: "phi g v = Some vs ⟹ length (predecessors g (defNode g v)) = length vs"

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

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

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

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

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

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

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

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

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

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

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

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

show ?case
proof (rule base.prems(1)[OF ns, rule_format], rule exI, rule exI, rule exI, rule exI)
fix n
assume "n ∈ set (butlast (ns' @ [defNode g p]))"
with base.hyps ns'
show "r p q ∧
g ⊢ defNode g q-ns'→m ∧
defNode g q ∉ set (tl ns') ∧
q ∈ phiUses g m ∧
m ∈ set (predecessors g (defNode g p)) ∧ n ∈ set ns' ∧ set ns' ⊆ set (ns' @ [defNode g p]) ∧ defNode g p ∈ set (ns' @ [defNode g p])"
by auto
qed
next
case (step p p')
from step.prems(2) step.hyps(1) obtain ns'⇩2 m where ns'⇩2: "g ⊢ defNode g p'-ns'⇩2→m" "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 ns⇩2 where ns⇩2: "g ⊢ defNode g p'-ns⇩2→defNode g p" "length ns⇩2 > 1" "ns⇩2 = ns'⇩2@[defNode g p]" by (atomize_elim, auto)

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

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

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

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

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

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

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

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

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

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

declare phiArg_def [simp del]
end

subsection ‹Bundling of CFG and Equivalent SSA CFG›

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma oldDefsI: "v ∈ defs g n ⟹ var g v ∈ oldDefs g n" by (simp add: oldDefs_def)

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

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

end


# 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-xs→z ∧ g ⊢ y-ys→z ∧ 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-xs→z ∧ g ⊢ y-ys→z ∧ 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-xs→z" "g ⊢ y-ys→z" "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-ns→n ⟶ (∃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-ns→S" "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-ns→m" "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 v⇩a v⇩b where
a: "v⇩a ∈ defs g a" "var g v⇩a = var g v" and
b: "v⇩b ∈ defs g b" "var g v⇩b = var g v"
and conv: "g ⊢ a-as→n" "g ⊢ b-bs→n" "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 v⇩a a as v⇩b b bs
assume a: "v⇩a ∈ defs g a" "var g v⇩a = var g v"
assume as: "g ⊢ a-as→n" "length as > 1"
assume b: "v⇩b ∈ defs g b" "var g v⇩b = var g v"
assume bs: "g ⊢ b-bs→n"
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 ≠ v⇩a"
proof
assume asm: "v = v⇩a"
have "v ≠ v⇩b"
proof
assume "v = v⇩b"
with asm[symmetric] b(1) have "v⇩a ∈ 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-ebs→b"
using bs by (atomize, auto)
hence "g ⊢ Entry g-butlast ebs@bs→n" 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-abs→b" "a ∉ set (tl abs)"
by (rule old.path2_split_first_last, auto)
let ?path = "(abs@tl bs)@tl ns"
have "var g v⇩b ≠ var g v⇩a"
proof (rule conventional)
show "g ⊢ a-?path→m" 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 "v⇩a ∈ 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)
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 v⇩a" 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-eas→a"
using as by (atomize, auto)
hence "g ⊢ Entry g-eas@tl as→n" 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 v⇩a ≠ var g v"
proof (rule conventional)
show "g ⊢ defNode g v-?path→m" 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
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-ns→m" "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-xs→z" "g ⊢ y-ys→z" "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 n⇩1 ns⇩1 n⇩2 ns⇩2 where
"var g r ∈ oldDefs g n⇩1" "g ⊢ n⇩1-ns⇩1→defNode g r" and
"var g r ∈ oldDefs g n⇩2" "g ⊢ n⇩2-ns⇩2→defNode g r" and
"set (butlast ns⇩1) ∩ set (butlast ns⇩2) = {}"
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-ns→defNode g r" and "V ∈ oldDefs g m" "g ⊢ m-ms→defNode g s"
and "set ns ∩ set ms = {}"
proof-
obtain n⇩1 ns⇩1 n⇩2 ns⇩2 where
ns⇩1: "V ∈ oldDefs g n⇩1" "g ⊢ n⇩1-ns⇩1→defNode g r" "defNode g r ∉ set (butlast ns⇩1)" and
ns⇩2: "V ∈ oldDefs g n⇩2" "g ⊢ n⇩2-ns⇩2→defNode g r" "defNode g r ∉ set (butlast ns⇩2)" and
ns: "set (butlast ns⇩1) ∩ set (butlast ns⇩2) = {}"
proof-
from assms obtain n⇩1 ns⇩1 n⇩2 ns⇩2 where
ns⇩1: "V ∈ oldDefs g n⇩1" "g ⊢ n⇩1-ns⇩1→defNode g r" and
ns⇩2: "V ∈ oldDefs g n⇩2" "g ⊢ n⇩2-ns⇩2→defNode g r" and
ns: "set (butlast ns⇩1) ∩ set (butlast ns⇩2) = {}"
by - (rule ununnecessaryPhis_disjoint_paths_aux, auto)

from ns⇩1 obtain ns⇩1' where ns⇩1': "g ⊢ n⇩1-ns⇩1'→defNode g r" "defNode g r ∉ set (butlast ns⇩1')" "distinct ns⇩1'" "set ns⇩1' ⊆ set ns⇩1"
by (auto elim: old.simple_path2)
from ns⇩2 obtain ns⇩2' where ns⇩2': "g ⊢ n⇩2-ns⇩2'→defNode g r" "defNode g r ∉ set (butlast ns⇩2')" "distinct ns⇩2'" "set ns⇩2' ⊆ set ns⇩2"
by (auto elim: old.simple_path2)

have "set (butlast ns⇩1') ∩ set (butlast ns⇩2') = {}"
proof (rule equals0I)
fix x
assume 1: "x ∈ set (butlast ns⇩1') ∩ set (butlast ns⇩2')"
with set_butlast_distinct[OF ns⇩1'(3)] ns⇩1'(1) have 2: "x ≠ defNode g r" by (auto simp:old.path2_def)
with 1 ns⇩1'(4) ns⇩2'(4) ns⇩1(2) ns⇩2(2) have "x ∈ set (butlast ns⇩1)" "x ∈ set (butlast ns⇩2)"
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 ns⇩1(1) ns⇩1'(1,2) ns⇩2(1) ns⇩2'(1,2)])
qed

obtain m ms where ms: "V ∈ oldDefs g m" "g ⊢ m-ms→defNode g s" "defNode g r ∉ set ms"
proof-
from assms(2) obtain m⇩1 ms⇩1 m⇩2 ms⇩2 where
ms⇩1: "V ∈ oldDefs g m⇩1" "g ⊢ m⇩1-ms⇩1→defNode g s" and
ms⇩2: "V ∈ oldDefs g `