Theory Tree
section ‹Trees›
theory Tree
imports Graph begin
text ‹A tree is a connected graph without cycles.›
locale Tree = Graph +
assumes connected: "⟦ v ∈ V; w ∈ V ⟧ ⟹ v →⇧* w" and no_cycles: "¬cycle xs"
begin
subsection ‹Unique Connecting Path›
text ‹For every pair of vertices in a tree, there exists a unique path connecting these two
vertices.
›
lemma unique_connecting_path: "⟦ v ∈ V; w ∈ V ⟧ ⟹ ∃!xs. v ↝xs↝ w"
using connected no_cycles no_cycles_implies_unique_paths by blast
text ‹Let us define a function mapping pair of vertices to their unique connecting path.›
end
definition unique_connecting_path :: "('a, 'b) Graph_scheme ⇒ 'a ⇒ 'a ⇒ 'a Walk"
(infix "↝ı" 71) where "unique_connecting_path G v w ≡ THE xs. v ↝xs↝⇘G⇙ w"
text ‹We defined this outside the locale in order to be able to use the index in the shorthand
syntax @{term "v ↝ı w"}.›
context Tree begin
lemma unique_connecting_path_set:
assumes "v ∈ V" "w ∈ V"
shows "v ∈ set (v ↝ w)" "w ∈ set (v ↝ w)"
using theI'[OF unique_connecting_path[OF assms], folded unique_connecting_path_def]
hd_in_set last_in_set by fastforce+
lemma unique_connecting_path_properties:
assumes "v ∈ V" "w ∈ V"
shows "path (v ↝ w)" "v ↝ w ≠ Nil" "hd (v ↝ w) = v" "last (v ↝ w) = w"
using theI'[OF unique_connecting_path[OF assms], folded unique_connecting_path_def] by blast+
lemma unique_connecting_path_unique:
assumes "v ↝xs↝ w"
shows "xs = v ↝ w"
proof-
have "v ∈ V" "w ∈ V" using assms connected_in_V by blast+
with unique_connecting_path_properties[OF this] show ?thesis
using assms unique_connecting_path by blast
qed
corollary unique_connecting_path_connects: "⟦ v ∈ V; w ∈ V ⟧ ⟹ v ↝(v↝w) ↝ w"
using unique_connecting_path unique_connecting_path_unique by blast
lemma unique_connecting_path_rev:
assumes "v ∈ V" "w ∈ V"
shows "v ↝ w = rev (w ↝ v)"
proof-
have "v ↝(rev (w ↝ v))↝ w" using assms
by (simp add: unique_connecting_path_properties walk_rev hd_rev last_rev path_from_toI)
thus ?thesis using unique_connecting_path_unique by simp
qed
lemma unique_connecting_path_decomp:
assumes "v ∈ V" "w ∈ V" "v ↝ w = ps @ u # ps'"
shows "ps @ [u] = v ↝ u" "u # ps' = u ↝ w"
proof-
have "hd (ps @ [u]) = v"
by (metis append_Nil assms hd_append2 list.sel(1) unique_connecting_path_properties(3))
moreover have "path (ps @ [u])" using unique_connecting_path_properties(1)[OF assms(1,2)]
unfolding assms(3)
by (metis distinct.simps(2) distinct1_rotate list.sel(1) list.simps(3) not_distinct_conv_prefix
path_decomp(1) rev.simps(2) rotate1.simps(2) walk_comp walk_decomp(2) walk_last_edge walk_rev)
moreover have "last (ps @ [u]) = u" "ps @ [u] ≠ Nil" by simp_all
ultimately show "ps @ [u] = v ↝ u" using unique_connecting_path_unique by blast
next
have "last (u # ps') = w"
using assms unique_connecting_path_properties(4) by fastforce
moreover have "path (u # ps')" using unique_connecting_path_properties(1)[OF assms(1,2)]
unfolding assms(3) using path_decomp(2) by blast
moreover have "hd (u # ps') = u" "u # ps' ≠ Nil" by simp_all
ultimately show "u # ps' = u ↝ w" using unique_connecting_path_unique by blast
qed
lemma unique_connecting_path_tl:
assumes "v ∈ V" "u ∈ set (w ↝ v)" "u→w"
shows "tl (w ↝ v) = u ↝ v"
proof (rule ccontr)
assume contra: "¬?thesis"
from assms(2) obtain ps ps' where
ps: "w ↝ v = ps @ u # ps'" by (meson split_list)
have "cycle (ps @ [u])" proof
show "path (ps @ [u])" using unique_connecting_path_decomp assms(1,3) ps
by (metis edges_are_in_V unique_connecting_path_properties(1))
show "length (ps @ [u]) > 2" proof (rule ccontr)
assume "¬?thesis"
moreover have "u ≠ w" using assms(3) no_loops by blast
ultimately have "length (ps @ [u]) = 2"
by (metis edges_are_in_V(2) assms(1,3) hd_append length_0_conv length_append_singleton
less_2_cases linorder_neqE_nat list.sel(1) nat.simps(1) ps snoc_eq_iff_butlast
unique_connecting_path_properties(3))
hence "tl (w ↝ v) = u # ps'"
by (metis One_nat_def Suc_1 append_Nil diff_Suc_1 length_0_conv length_Cons
length_append_singleton list.collapse nat.simps(3) ps tl_append2)
moreover have "u # ps' = u ↝ v"
using unique_connecting_path_decomp assms(1,3) edges_are_in_V(2) ps by blast
ultimately show False using contra by simp
qed
show "last (ps @ [u]) → hd (ps @ [u])" using assms(3)
by (metis edges_are_in_V(2) unique_connecting_path_properties(3)
assms(1) hd_append list.sel(1) ps snoc_eq_iff_butlast)
qed
thus False using no_cycles by auto
qed
text ‹Every tree with at least two vertices contains an edge.›
lemma tree_has_edge:
assumes "card V > 1"
shows "∃v w. v→w"
proof-
obtain v where v: "v ∈ V" using assms
by (metis List.finite_set One_nat_def card.empty card_mono empty_set less_le_trans linear
not_less subsetI zero_less_Suc)
then obtain w where "w ∈ V" "v ≠ w" using assms
by (metis (no_types, lifting) One_nat_def card.empty card.insert distinct.simps(2) empty_set
finite.intros(1) finite_distinct_list finite_vertex_set hd_in_set last.simps last_in_set
less_or_eq_imp_le list.exhaust_sel list.simps(15) not_less path_singleton)
hence "v → hd (tl (v↝w))" using v
by (metis unique_connecting_path_properties last.simps list.exhaust_sel walk_first_edge')
thus ?thesis by blast
qed
subsection ‹Separations›
text ‹
Removing a single edge always splits a tree into two subtrees. Here we define the set of vertices
of the left subtree. The definition may not be obvious at first glance, but we will soon prove
that it behaves as expected. We say that a vertex @{term u} is in the left subtree if and only
if the unique path from @{term u} to @{term t} visits @{term s}.
›
definition left_tree :: "'a ⇒ 'a ⇒ 'a set" where
"left_tree s t ≡ { u ∈ V. s ∈ set (u ↝ t) }"
lemma left_treeI [intro]: "⟦ u ∈ V; s ∈ set (u ↝ t) ⟧ ⟹ u ∈ left_tree s t"
unfolding left_tree_def by blast
lemma left_treeE: "u ∈ left_tree s t ⟹ u ∈ V ∧ s ∈ set (u ↝ t)"
unfolding left_tree_def by blast
lemma left_tree_in_V: "left_tree s t ⊆ V" unfolding left_tree_def by blast
lemma left_tree_initial: "⟦ s ∈ V; t ∈ V ⟧ ⟹ s ∈ left_tree s t"
unfolding left_tree_def by (simp add: unique_connecting_path_set(1))
lemma left_tree_initial': "⟦ s ∈ V; t ∈ V; s ≠ t ⟧ ⟹ t ∉ left_tree s t"
by (metis distinct.simps(2) last.simps left_treeE list.discI list.sel(1) path_from_toI
path_singleton set_ConsD unique_connecting_path_unique)
lemma left_tree_initial_edge: "s→t ⟹ t ∉ left_tree s t"
using edges_are_in_V(1) left_tree_initial' no_loops undirected by blast
text ‹The union of the left and right subtree is @{term V}.›
lemma left_tree_union_V:
assumes "s→t"
shows "left_tree s t ∪ left_tree t s = V"
proof
show "left_tree s t ∪ left_tree t s ⊆ V" using left_tree_in_V by auto
{
have s: "s ∈ V" and t: "t ∈ V" using assms using edges_are_in_V by blast+
text ‹Assume to the contrary that @{term "u ∈ V"} is in neither part.›
fix u assume u: "u ∈ V" "u ∉ left_tree s t" "u ∉ left_tree t s"
text ‹Then we can construct two different paths from @{term s} to @{term u}, which, in a
tree, is a contradiction. First, we get paths from @{term s} to @{term u} and from
@{term t} to @{term u}.›
let ?xs = "s ↝ u"
let ?ys = "t ↝ u"
have "t ∉ set ?xs" using u(1,3) unfolding left_tree_def
by (metis (no_types, lifting) unique_connecting_path_rev mem_Collect_eq s set_rev)
have "s ∉ set ?ys" using u(1,2) unfolding left_tree_def
by (metis (no_types, lifting) unique_connecting_path_rev mem_Collect_eq set_rev t)
text ‹Now we can define two different paths from @{term s} to @{term u}.›
define xs' where [simp]: "xs' = ?xs"
define ys' where [simp]: "ys' = s # ?ys"
have "path ys'" using path_cons ‹s ∉ set ?ys› assms
by (simp add: unique_connecting_path_properties(1-3) t u(1))
moreover have "path xs'" "xs' ≠ []" "ys' ≠ []" "hd xs' = s" "last xs' = u"
by (simp_all add: unique_connecting_path_properties s u(1))
moreover have "hd ys' = s" "last ys' = u"
by simp (simp add: unique_connecting_path_properties(2,4) t u(1))
moreover have "xs' ≠ ys'" using unique_connecting_path_set(1) ‹t ∉ set ?xs› t u(1) by auto
text ‹The existence of two different paths is a contradiction.›
ultimately have False using unique_connecting_path_unique by blast
}
thus "V ⊆ left_tree s t ∪ left_tree t s" by blast
qed
text ‹The left and right subtrees are disjoint.›
lemma left_tree_disjoint:
assumes "s→t"
shows "left_tree s t ∩ left_tree t s = {}"
proof (rule ccontr)
assume "¬?thesis"
then obtain u where u: "u ∈ V" "s ∈ set (u ↝ t)" "t ∈ set (u ↝ s)" using left_treeE by blast
have s: "s ∈ V" and t: "t ∈ V" using assms edges_are_in_V by blast+
obtain ps ps' where ps: "u ↝ t = ps @ s # ps'" by (meson split_list u(2))
hence "ps' ≠ Nil"
using assms last_snoc no_loops unique_connecting_path_properties(4)[OF u(1) t] by auto
hence *: "length (ps @ [s]) < length (u ↝ t)" by (simp add: ps)
have ps': "ps @ [s] = u ↝ s" using ps unique_connecting_path_decomp t u(1) by blast
then obtain qs qs' where qs: "ps @ [s] = qs @ t # qs'" using split_list[OF u(3)] by auto
hence "qs' ≠ Nil" using assms last_snoc no_loops by auto
hence **: "length (qs @ [t]) < length (ps @ [s])" by (simp add: qs)
have "qs @ [t] = u ↝ t" using qs ps' unique_connecting_path_decomp s u(1) by metis
thus False using less_trans[OF ** *] by simp
qed
text ‹
The path from a vertex in the left subtree to a vertex in the right subtree goes through @{term s}.
In other words, an edge @{term "s→t"} is a separator in a tree.
›
theorem left_tree_separates:
assumes st: "s→t" and u: "u ∈ left_tree s t" and u': "u' ∈ left_tree t s"
shows "s ∈ set (u ↝ u')"
proof (rule ccontr)
assume "¬?thesis"
with assms have "set (u ↝ u') ⊆ left_tree s t"
proof(induct "u ↝ u'" arbitrary: u u')
case Nil thus ?case using unique_connecting_path_properties(2) by auto
next
case (Cons x xs u u')
have "x = u" using Cons.hyps(2) Cons.prems(2,3)
by (metis left_treeE list.sel(1) unique_connecting_path_properties(3))
hence "u→hd xs" using Cons.hyps(2) Cons.prems(2,3) st
by (metis IntI left_tree_disjoint distinct.simps(2) last.simps left_treeE list.set(1)
unique_connecting_path_properties(1,4) walk_first_edge')
hence "u ∈ V" "hd xs ∈ V" using edges_are_in_V by blast+
have *: "xs = hd xs ↝ u'"
by (metis Cons.hyps(2) Cons.prems(2,3) IntI left_tree_disjoint distinct.simps(2) last.simps
left_treeE list.sel(1,3) list.set(1) path_from_toI st
unique_connecting_path_properties(1,3,4) unique_connecting_path_unique walk_tl)
moreover hence "s ∉ set (hd xs ↝ u')" using Cons.hyps(2) Cons.prems(4)
by (metis list.set_intros(2))
moreover have "hd xs ∈ left_tree s t" proof (rule ccontr)
assume "¬?thesis"
hence "hd xs ∈ left_tree t s" using ‹hd xs ∈ V› st left_tree_union_V by fastforce
hence "t ∈ set (hd xs ↝ s)" using left_treeE by blast
let ?ys' = "hd xs ↝ s"
let ?ys = "u # ?ys'"
have "u ∉ set ?ys'" proof
assume "u ∈ set ?ys'"
hence "tl ?ys' = u ↝ s"
using unique_connecting_path_tl ‹u→hd xs› edges_are_in_V(1) st by auto
moreover have "t ≠ hd xs" proof
let ?ys = "[u, hd xs]"
have "t ≠ u" using Cons.prems(2) left_tree_initial_edge st by blast
assume "t = hd xs"
hence "?ys = u ↝ t"
using unique_connecting_path_unique[of u ?ys "hd xs"] ‹u→hd xs› ‹t ≠ u›
by (simp add: path_from_toI)
hence "s ∉ set (u ↝ t)"
by (metis Cons.hyps(2) Cons.prems(4) ‹t = hd xs› ‹x = u› distinct.simps(2)
distinct_singleton list.set_intros(1) no_loops set_ConsD st)
thus False using Cons.prems(2) left_treeE by blast
qed
ultimately have "t ∈ set (u ↝ s)" using ‹t ∈ set ?ys'› ‹hd xs ∈ V› st
by (metis edges_are_in_V(1) unique_connecting_path_properties(2,3) list.collapse set_ConsD)
thus False using Cons.prems(2) st ‹u ∈ V›
by (meson left_tree_disjoint disjoint_iff_not_equal left_treeI)
qed
hence "path ?ys" using path_cons ‹u→hd xs›
by (metis unique_connecting_path_properties(1-3) edges_are_in_V st)
moreover have "?ys ≠ Nil" "hd ?ys = u" by simp_all
moreover have "last ?ys = s" using st unique_connecting_path_properties(2,4) ‹hd xs ∈ V›
by (simp add: edges_are_in_V(1))
ultimately have "?ys = u ↝ s" using unique_connecting_path_unique by blast
hence "t ∈ set (u ↝ s)" by (metis ‹t ∈ set ?ys'› list.set_intros(2))
thus False using Cons.prems(2) ‹u ∈ V› st
by (meson left_tree_disjoint disjoint_iff_not_equal left_treeI)
qed
ultimately have "set (hd xs ↝ u') ⊆ left_tree s t"
using Cons.hyps(1) st Cons.prems(3) by blast
hence "set xs ⊆ left_tree s t" using * by simp
thus ?case using Cons.hyps(2) Cons.prems(2,3)
by (metis insert_subset left_treeE list.sel(1) list.set(2) unique_connecting_path_properties(3))
qed
hence "u' ∈ left_tree s t" using left_treeE u u' unique_connecting_path_set(2) by auto
thus False by (meson left_tree_disjoint disjoint_iff_not_equal st u')
qed
text ‹By symmetry, the path also visits @{term t}.›
corollary left_tree_separates':
assumes "s→t" "u ∈ left_tree s t" "u' ∈ left_tree t s"
shows "t ∈ set (u ↝ u')"
using assms left_tree_separates by (metis left_treeE set_rev undirected unique_connecting_path_rev)
end
subsection ‹Rooted Trees›
text ‹A rooted tree is a tree with a distinguished vertex called root.›
locale RootedTree = Tree +
fixes root :: 'a
assumes root_in_V: "root ∈ V"
begin
text ‹In a rooted tree, we can define the parent relation.›
definition parent :: "'a ⇒ 'a" where
"parent v ≡ hd (tl (v ↝ root))"
lemma parent_edge: "⟦ v ∈ V; v ≠ root ⟧ ⟹ v→parent v" unfolding parent_def
by (metis last.simps list.exhaust_sel root_in_V unique_connecting_path_properties walk_first_edge')
lemma parent_edge_root: "v→root ⟹ parent v = root" unfolding parent_def
by (metis edges_are_in_V(1) path_from_toE undirected unique_connecting_path
unique_connecting_path_set(2) unique_connecting_path_tl unique_connecting_path_unique)
lemma parent_in_V: "⟦ v ∈ V; v ≠ root ⟧ ⟹ parent v ∈ V"
using parent_edge edges_are_in_V(2) by blast
lemma parent_edge_cases: "v→w ⟹ w = parent v ∨ v = parent w" unfolding parent_def
by (metis Un_iff edges_are_in_V(1) left_tree_initial left_tree_separates' left_tree_union_V
root_in_V undirected unique_connecting_path_properties(3) unique_connecting_path_tl)
lemma sibling_path:
assumes v: "v ∈ V" "v ≠ root" and w: "w ∈ V" "w ≠ root" and vw: "v ≠ w" "parent v = parent w"
shows "v↝w = [v,parent v,w]" (is "_ = ?xs")
proof-
have "path ?xs" using v w vw
by (metis distinct_length_2_or_more distinct_singleton no_loops parent_edge undirected
walk.Cons walk_2)
thus ?thesis using unique_connecting_path_unique by fastforce
qed
end
end