Theory TreeDecomposition
section ‹Tree Decompositions›
theory TreeDecomposition
imports Tree begin
text ‹A tree decomposition of a graph.›
locale TreeDecomposition = Graph G + T: Tree T
for G :: "('a, 'b) Graph_scheme" (structure) and T :: "('c,'d) Graph_scheme" +
fixes bag :: "'c ⇒ 'a set"
assumes
bags_union: "⋃ { bag t | t. t ∈ V⇘T⇙ } = V"
and bags_edges: "v→w ⟹ ∃t ∈ V⇘T⇙. v ∈ bag t ∧ w ∈ bag t"
and bags_continuous: "⟦ s ∈ V⇘T⇙; u ∈ V⇘T⇙; t ∈ set (s ↝⇘T⇙ u) ⟧ ⟹ bag s ∩ bag u ⊆ bag t"
begin
text ‹
Following the usual literature, we will call elements of @{term V} vertices and
elements of @{term "V⇘T⇙"} bags (or nodes) from now on.›
subsection ‹Width of a Tree Decomposition›
text ‹We define the width of this tree decomposition as the size of the largest bag minus 1.›
abbreviation "bag_cards ≡ { card (bag t) | t. t ∈ V⇘T⇙ }"
definition "max_bag_card ≡ Max bag_cards"
text ‹We need a special case for @{term "V⇘T⇙ = {}"} because in this case @{const max_bag_card}
is not well-defined.›
definition "width ≡ if V⇘T⇙ = {} then 0 else max_bag_card - 1"
lemma bags_in_V: "t ∈ V⇘T⇙ ⟹ bag t ⊆ V" using bags_union Sup_upper mem_Collect_eq by blast
lemma bag_finite: "t ∈ V⇘T⇙ ⟹ finite (bag t)" using bags_in_V finite_subset finite_vertex_set by blast
lemma bag_bound_V: "t ∈ V⇘T⇙ ⟹ card (bag t) ≤ card V" by (simp add: bags_in_V card_mono finite_vertex_set)
lemma bag_bound_V_empty: "⟦ V = {}; t ∈ V⇘T⇙ ⟧ ⟹ card (bag t) = 0" using bag_bound_V by auto
lemma empty_tree_empty_V: "V⇘T⇙ = {} ⟹ V = {}" using bags_union by simp
lemma bags_exist: "v ∈ V ⟹ ∃t ∈ V⇘T⇙. v ∈ bag t" using bags_union using UnionE mem_Collect_eq by auto
text ‹
The width is never larger than the number of vertices, and if there is at least one vertex
in the graph, then it is always smaller. This is trivially true because a bag contains at most
all of @{term V}. However, the proof is not fully trivial because we also need to show that
@{const width} is well-defined.›
lemma bag_cards_finite: "finite bag_cards" using T.finite_vertex_set by simp
lemma bag_cards_nonempty: "V ≠ {} ⟹ bag_cards ≠ {}"
using bag_cards_finite empty_tree_empty_V empty_Collect_eq ex_in_conv by blast
lemma max_bag_card_in_bag_cards: "V ≠ {} ⟹ max_bag_card ∈ bag_cards" unfolding max_bag_card_def
using Max_in bag_cards_finite bag_cards_nonempty by auto
lemma max_bag_card_lower_bound_bag: "t ∈ V⇘T⇙ ⟹ max_bag_card ≥ card (bag t)"
by (metis (mono_tags, lifting) Max_ge bag_cards_finite max_bag_card_def mem_Collect_eq)
lemma max_bag_card_lower_bound_1: assumes "V ≠ {}" shows "max_bag_card > 0" proof-
have "∃v ∈ V. ∃t ∈ V⇘T⇙. v ∈ bag t" using ‹V ≠ {}› bags_union by blast
thus "max_bag_card > 0" unfolding max_bag_card_def using bag_finite
card_gt_0_iff emptyE Max_gr_iff[OF bag_cards_finite bag_cards_nonempty[OF assms]] by auto
qed
lemma max_bag_card_upper_bound_V: "V ≠ {} ⟹ max_bag_card ≤ card V" unfolding max_bag_card_def
using Max_le_iff[OF bag_cards_finite bag_cards_nonempty] bag_bound_V by blast
lemma width_upper_bound_V: "V ≠ {} ⟹ width < card V" unfolding width_def
using max_bag_card_upper_bound_V max_bag_card_lower_bound_1
diff_less empty_tree_empty_V le_neq_implies_less less_imp_diff_less zero_less_one by presburger
lemma width_V_empty: "V = {} ⟹ width = 0" unfolding width_def max_bag_card_def
using bag_bound_V_empty T.finite_vertex_set by (cases "V⇘T⇙ = {}") auto
lemma width_bound_V_le: "width ≤ card V - 1"
using width_upper_bound_V width_V_empty by (cases "V = {}") auto
lemma width_lower_bound_1:
assumes "v→w"
shows "width ≥ 1"
proof-
obtain t where t: "t ∈ V⇘T⇙" "v ∈ bag t" "w ∈ bag t" using bags_edges assms by blast
have "card (bag t) ≠ 0" using t(1,2) bag_finite card_0_eq empty_iff by blast
moreover have "card (bag t) ≠ 1" using t(2,3) assms no_loops
by (metis One_nat_def card_Suc_eq empty_iff insertE)
ultimately have "card (bag t) ≥ 2" by simp
hence "max_bag_card > 1" using t(1) max_bag_card_lower_bound_bag by fastforce
thus ?thesis unfolding width_def using t(1) by fastforce
qed
end
subsection ‹Treewidth of a Graph›
context Graph begin
text ‹The treewidth of a graph is the minimum treewidth over all its tree decompositions.
Here we assume without loss of generality that the universe of the vertices of the tree
is @{type nat}. Because trees are finite, @{type nat} always contains enough elements.›
abbreviation treewidth_cards :: "nat set" where "treewidth_cards ≡
{ TreeDecomposition.width T bag | (T :: nat Graph) bag. TreeDecomposition G T bag }"
definition treewidth :: "nat" where "treewidth ≡ Min treewidth_cards"
text ‹Every graph has a trivial tree decomposition consisting of a single bag containing all of
@{term V}.›
proposition tree_decomposition_exists: "∃(T :: 'c Graph) bag. TreeDecomposition G T bag" proof-
obtain x where "x ∈ (UNIV :: 'c set)" by blast
define T where [simp]: "T = ⦇ verts = {x}, arcs = {} ⦈"
define bag where [simp]: "bag = (λ_ :: 'c. V)"
have "Graph T" by unfold_locales simp_all
then interpret T: Graph T .
have "⋀xs. ¬T.cycle xs" using T.cycleE by auto
moreover have "⋀v w. v ∈ V⇘T⇙ ⟹ w ∈ V⇘T⇙ ⟹ T.connected v w" using T.connected_refl by auto
ultimately have "Tree T" by unfold_locales
then interpret T: Tree T .
have "TreeDecomposition G T bag" by unfold_locales (simp_all add: edges_are_in_V)
thus ?thesis by blast
qed
corollary treewidth_cards_upper_bound_V: "n ∈ treewidth_cards ⟹ n ≤ card V - 1"
using TreeDecomposition.width_bound_V_le by blast
corollary treewidth_cards_finite: "finite treewidth_cards"
using treewidth_cards_upper_bound_V finite_nat_set_iff_bounded_le by auto
corollary treewidth_cards_nonempty: "treewidth_cards ≠ {}" by (simp add: tree_decomposition_exists)
lemma treewidth_cards_treewidth:
"∃(T :: nat Graph) bag. TreeDecomposition G T bag ∧ treewidth = TreeDecomposition.width T bag"
using Min_in treewidth_cards_finite treewidth_cards_nonempty treewidth_def by fastforce
corollary treewidth_upper_bound_V: "treewidth ≤ card V - 1" unfolding treewidth_def
using treewidth_cards_nonempty Min_in treewidth_cards_finite treewidth_cards_upper_bound_V by auto
corollary treewidth_upper_bound_0: "V = {} ⟹ treewidth = 0" using treewidth_upper_bound_V by simp
corollary treewidth_upper_bound_1: "card V = 1 ⟹ treewidth = 0" using treewidth_upper_bound_V by simp
corollary treewidth_lower_bound_1: "v→w ⟹ treewidth ≥ 1"
using TreeDecomposition.width_lower_bound_1 treewidth_cards_treewidth by fastforce
lemma treewidth_upper_bound_ex:
"⟦ TreeDecomposition G (T :: nat Graph) bag; TreeDecomposition.width T bag ≤ n ⟧ ⟹ treewidth ≤ n"
unfolding treewidth_def
by (metis (mono_tags, lifting) Min_le dual_order.trans mem_Collect_eq treewidth_cards_finite)
end
subsection ‹Separations›
context TreeDecomposition begin
text ‹
Every edge @{term "s→⇘T⇙ t"} in @{term T} separates @{term T}. In a tree decomposition,
this edge also separates @{term G}. Proving this is our goal. First, let us define the set of
vertices appearing in the left subtree when separating the tree at @{term "s →⇘T⇙ t"}.
›
definition left_part :: "'c ⇒ 'c ⇒ 'a set" where
"left_part s t ≡ ⋃{ bag u | u. u ∈ T.left_tree s t }"
lemma left_partI [intro]: "⟦ v ∈ bag u; u ∈ T.left_tree s t ⟧ ⟹ v ∈ left_part s t"
unfolding left_part_def by blast
lemma left_part_in_V: "left_part s t ⊆ V" unfolding left_part_def
using T.left_tree_in_V bags_in_V by blast
text ‹Let us define the subgraph of @{term T} induced by a vertex of @{term G}.›
definition vertex_subtree :: "'a ⇒ 'c set" where
"vertex_subtree v ≡ { t ∈ V⇘T⇙. v ∈ bag t }"
lemma vertex_subtreeI [intro]: "⟦ t ∈ V⇘T⇙; v ∈ bag t ⟧ ⟹ t ∈ vertex_subtree v"
unfolding vertex_subtree_def by blast
text ‹
The suggestive name @{const vertex_subtree} is correct: Because @{term T} is a tree
decomposition, @{term "vertex_subtree v"} is a subtree (it is connected).›
lemma vertex_subtree_connected:
assumes v: "v ∈ V" and s: "s ∈ vertex_subtree v" and t: "t ∈ vertex_subtree v"
and xs: "s ↝xs↝⇘T⇙ t"
shows "set xs ⊆ vertex_subtree v"
using assms proof (induct xs arbitrary: s)
case (Cons x xs)
show ?case proof (cases)
assume "xs = []" thus ?thesis using Cons.prems(3,4) by auto
next
assume "xs ≠ []"
moreover hence "last xs = t" using Cons.prems(4) last.simps by auto
moreover have "T.path xs" using Cons.prems(4) T.walk_tl by fastforce
moreover have "hd xs ∈ vertex_subtree v" proof
have "hd xs ∈ set (s ↝⇘T⇙ t)" using T.unique_connecting_path_unique
using Cons.prems(4) ‹xs ≠ []› by auto
hence "bag s ∩ bag t ⊆ bag (hd xs)"
using bags_continuous Cons.prems(4) T.connected_in_V by blast
thus "v ∈ bag (hd xs)" using Cons.prems(2,3) unfolding vertex_subtree_def by blast
show "hd xs ∈ V⇘T⇙" using T.connected_in_V(1) ‹xs ≠ []› ‹T.path xs› by blast
qed
ultimately have "set xs ⊆ vertex_subtree v" using Cons.hyps Cons.prems(1,3) by blast
thus ?thesis using Cons.prems(2,4) by auto
qed
qed simp
corollary vertex_subtree_unique_path_connected:
assumes "v ∈ V" "s ∈ vertex_subtree v" "t ∈ vertex_subtree v"
shows "set (s ↝⇘T⇙ t) ⊆ vertex_subtree v"
using assms vertex_subtree_connected T.unique_connecting_path_properties
by (metis (no_types, lifting) T.unique_connecting_path T.unique_connecting_path_unique
mem_Collect_eq vertex_subtree_def)
text ‹
In order to prove that edges in @{term T} are separations in @{term G}, we need one key lemma.
If a vertex appears on both sides of a separation, then it also appears in the separation.
›
lemma vertex_in_separator:
assumes st: "s →⇘T⇙ t" and v: "v ∈ left_part s t" "v ∈ left_part t s"
shows "v ∈ bag s" "v ∈ bag t"
proof-
obtain u u' where u: "v ∈ bag u" "u ∈ T.left_tree s t" "v ∈ bag u'" "u' ∈ T.left_tree t s"
using v unfolding left_part_def by blast
have "s ∈ set (u ↝⇘T⇙ u')" using T.left_tree_separates st u by blast
thus "v ∈ bag s" using bags_continuous u by (meson IntI T.left_treeE subsetCE)
have "t ∈ set (u ↝⇘T⇙ u')" using T.left_tree_separates' st u by blast
thus "v ∈ bag t" using bags_continuous u by (meson IntI T.left_treeE subsetCE)
qed
text ‹Now we can show the main theorem: For every edge @{term "s →⇘T⇙ t"} in @{term T}, the
set @{term "bag s ∩ bag t"} is a separator of @{term G}. That is, every path from the left part
to the right part goes through @{term "bag s ∩ bag t"}.›
theorem bags_separate:
assumes st: "s →⇘T⇙ t" and v: "v ∈ left_part s t" and w: "w ∈ left_part t s" and xs: "v ↝xs↝ w"
shows "set xs ∩ bag s ∩ bag t ≠ {}"
proof (rule ccontr)
assume "¬?thesis"
{
fix u assume "u ∈ set xs"
with xs v ‹¬?thesis› have "vertex_subtree u ⊆ T.left_tree s t"
proof (induct xs arbitrary: v)
case (Cons x xs v)
hence contra: "v ∉ bag s ∨ v ∉ bag t" by (metis path_from_toE IntI empty_iff hd_in_set)
{
assume "x = u" "¬vertex_subtree u ⊆ T.left_tree s t"
then obtain z where z: "z ∈ vertex_subtree u" "z ∉ T.left_tree s t" by blast
hence "z ∈ vertex_subtree v" using Cons.prems(1,3) ‹x = u›
by (metis list.sel(1) path_from_to_def)
hence "v ∈ left_part t s" unfolding vertex_subtree_def
using T.left_tree_union_V z st by auto
hence False using vertex_in_separator contra st Cons.prems(2) by blast
}
moreover {
assume "x ≠ u"
hence "u ∈ set xs" using Cons.prems(4) by auto
moreover hence "xs ≠ Nil" using empty_iff list.set(1) by auto
moreover hence "last xs = w" using Cons.prems(1) by auto
moreover have "path xs" using Cons.prems(1) walk_tl by force
moreover have "hd xs ∈ left_part s t" proof-
have "v→hd xs" using Cons.prems(1,3) ‹xs ≠ Nil› walk_first_edge' by auto
then obtain u' where u': "u' ∈ V⇘T⇙" "v ∈ bag u'" "hd xs ∈ bag u'"
using bags_edges by blast
hence "u' ∈ T.left_tree s t"
using contra vertex_in_separator st T.left_tree_union_V Cons.prems(2) by blast
thus ?thesis using u'(3) unfolding left_part_def by blast
qed
moreover have "¬set xs ∩ bag s ∩ bag t ≠ {}" using Cons.prems(3)
IntI disjoint_iff_not_equal inf_le1 inf_le2 set_subset_Cons subsetCE by auto
ultimately have "vertex_subtree u ⊆ T.left_tree s t" using Cons.hyps by blast
}
ultimately show ?case by blast
qed simp
}
hence "vertex_subtree w ⊆ T.left_tree s t" using xs last_in_set by blast
moreover have "vertex_subtree w ∩ T.left_tree t s ≠ {}" using w
unfolding left_part_def T.left_tree_def by blast
ultimately show False using T.left_tree_disjoint st by blast
qed
text ‹It follows that vertices cannot be dropped from a bag if they have a neighbor that has
not been visited yet (that is, a neighbor that is strictly in the right part of the separation).›
corollary bag_no_drop:
assumes st: "s →⇘T⇙ t" and vw: "v→w" and v: "v ∈ bag s" and w: "w ∉ bag s" "w ∈ left_part t s"
shows "v ∈ bag t"
proof-
have "v ↝[v,w]↝ w" using v vw w(1) by auto
hence "set [v,w] ∩ bag s ∩ bag t ≠ {}" using st v w(2)
by (meson T.edges_are_in_V T.left_tree_initial bags_separate left_partI)
thus ?thesis using w(1) by auto
qed
end
end