Theory Graph_path
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
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
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'"
by (simp add: Cons_path.IH in_set_tlD)
moreover from Cons_path(1) have "m' ∈ set ms" by auto
hence "m' ≠ n" using Cons_path(4) by simp
ultimately show ?case using Cons_path(2) by - (rule dominates_unsnoc, auto)
qed
lemma dominates_path:
assumes "dominates g n m" and[simp]: "invar g"
obtains ns where "g ⊢ n-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