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
    ― ‹Every vertex appears somewhere›
    bags_union: " { bag t | t. t  VT} = V"
     ― ‹Every edge is covered›
    and bags_edges: "vw  t  VT. v  bag t  w  bag t"
    ― ‹Every vertex appearing in @{term s} and @{term u} also appears in every bag on the path
        connecting @{term s} and @{term u}
    and bags_continuous: " s  VT; u  VT; t  set (s Tu)   bag s  bag u  bag t"
begin
text ‹
  Following the usual literature, we will call elements of @{term V} vertices and
  elements of @{term "VT⇙"} 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  VT}"
definition "max_bag_card  Max bag_cards"
text ‹We need a special case for @{term "VT= {}"} because in this case @{const max_bag_card}
  is not well-defined.›
definition "width  if VT= {} then 0 else max_bag_card - 1"

lemma bags_in_V: "t  VT bag t  V" using bags_union Sup_upper mem_Collect_eq by blast
lemma bag_finite: "t  VT finite (bag t)" using bags_in_V finite_subset finite_vertex_set by blast
lemma bag_bound_V: "t  VT card (bag t)  card V" by (simp add: bags_in_V card_mono finite_vertex_set)
lemma bag_bound_V_empty: " V = {}; t  VT  card (bag t) = 0" using bag_bound_V by auto
lemma empty_tree_empty_V: "VT= {}  V = {}" using bags_union by simp
lemma bags_exist: "v  V  t  VT. 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  VT 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  VT. 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 "VT= {}") 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 "vw"
  shows "width  1"
proof-
  obtain t where t: "t  VT⇙" "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 ― ‹locale TreeDecomposition›

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  VT w  VT 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: "vw  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 ― ‹locale Graph›

subsection ‹Separations›

context TreeDecomposition begin

text ‹
  Every edge @{term "sTt"} 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 Tt"}.
›
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  VT. v  bag t }"
lemma vertex_subtreeI [intro]: " t  VT; 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 xsTt"
  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 Tt)" 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  VT⇙" 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 Tt)  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 Tt" 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 Tu')" 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 Tu')" 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 Tt"} 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 Tt" 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 "vhd xs" using Cons.prems(1,3) xs  Nil walk_first_edge' by auto
          then obtain u' where u': "u'  VT⇙" "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 Tt" and vw: "vw" 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 ― ‹locale TreeDecomposition›
end