Theory TreewidthTree

section ‹Treewidth of Trees›

theory TreewidthTree
imports TreeDecomposition begin

text ‹The treewidth of a tree is 1 if the tree has at least one edge, otherwise it is 0.

  For simplicity and without loss of generality, we assume that the vertex set of the tree is a
  subset of the natural numbers because this is what we use in the definition of
  @{const Graph.treewidth}.

  While it would be nice to lift this restriction, removing it would entail defining isomorphisms
  between graphs in order to map the tree decomposition to a tree decomposition over the natural
  numbers.  This is outside the scope of this theory and probably not terribly interesting by
  itself.›
theorem treewidth_tree:
  fixes G :: "nat Graph" (structure)
  assumes "Tree G"
  shows "Graph.treewidth G ≤ 1"
proof-
  interpret Tree G using assms .
  {
    assume "V ≠ {}"
    then obtain root where root: "root ∈ V" by blast
    then interpret RootedTree G root by unfold_locales
    define bag where "bag v = (if v = root then {v} else {v, parent v})" for v
    have v_in_bag: "⋀v. v ∈ bag v" unfolding bag_def by simp
    have bag_in_V: "⋀v. v ∈ V ⟹ bag v ⊆ V" unfolding bag_def
      using parent_in_V empty_subsetI insert_subset by auto
    have "TreeDecomposition G G bag" proof
      show "⋃{bag t | t. t ∈ V} = V" using bag_in_V v_in_bag by blast
    next
      fix v w assume "v→w"
      moreover have "⋀v' w'. ⟦ v'→w'; v' ≠ root ⟧ ⟹ w' ∈ bag v' ∨ v' ∈ bag w'" unfolding bag_def
        by (metis insertI2 parent_edge_cases parent_edge_root singletonI)
      ultimately have "v ∈ bag w ∨ w ∈ bag v" using no_loops undirected by blast
      thus "∃t∈V. v ∈ bag t ∧ w ∈ bag t" using ‹v→w› edges_are_in_V v_in_bag by blast
    next
      fix s u t assume s: "s ∈ V" and u: "u ∈ V" and t: "t ∈ set (s↝u)"
      have "t ∈ V" using t by (meson s subsetCE u unique_connecting_path_properties(1) walk_in_V)
      hence "s = u ⟹ t = s" using left_tree_initial' s t by blast
      moreover have "s→u ⟹ t = s ∨ t = u" using s t u ‹t ∈ V›
        by (metis insertE left_treeI left_tree_initial' list.exhaust_sel list.simps(15)
            undirected unique_connecting_path_properties(2,3) unique_connecting_path_set(2)
            unique_connecting_path_tl)
      moreover {
        assume *: "s ≠ u" "¬s→u"
        have "s = root ⟹ bag s ∩ bag u = {}" unfolding bag_def
          using *(1,2) parent_edge u undirected by fastforce
        moreover have "u = root ⟹ bag s ∩ bag u = {}" unfolding bag_def
          using *(1,2) parent_edge s by fastforce
        moreover have "⟦ s ≠ root; u ≠ root; parent s ≠ parent u ⟧ ⟹ bag s ∩ bag u = {}"
          unfolding bag_def using *(2) parent_edge s u undirected by fastforce
        moreover {
          assume **: "s ≠ root" "u ≠ root" "parent s = parent u" "t ≠ s" "t ≠ u"
          have "bag s ∩ bag u = { parent s }" unfolding bag_def using *(1) **(1-3)
            Int_insert_left inf.orderE insertE insert_absorb subset_insertI by auto
          moreover have "t = parent s"
            using sibling_path[OF s **(1) u **(2) *(1) **(3)] t **(4,5) by auto
          ultimately have "bag s ∩ bag u ⊆ bag t" by (simp add: v_in_bag)
        }
        ultimately have "bag s ∩ bag u ⊆ bag t" by blast
      }
      ultimately show "bag s ∩ bag u ⊆ bag t" by blast
    qed
    then interpret TreeDecomposition G G bag .
    {
      fix v
      have "card { v, parent v } ≤ 2"
        by (metis card.insert card.empty finite.emptyI finite_insert insert_absorb insert_not_empty
            lessI less_or_eq_imp_le numerals(2))
      hence "card (bag v) ≤ 2" unfolding bag_def by simp
    }
    hence "max_bag_card ≤ 2" using ‹V ≠ {}› max_bag_card_in_bag_cards by auto
    hence "width ≤ 1" unfolding width_def by (simp add: ‹V ≠ {}›)
    hence "∃bag. TreeDecomposition G G bag ∧ TreeDecomposition.width G bag ≤ 1"
      using TreeDecomposition_axioms by blast
  }
  thus ?thesis by (metis TreeDecomposition.width_V_empty le_0_eq linear
    treewidth_cards_treewidth treewidth_upper_bound_ex)
qed

text ‹If the tree is non-trivial, that is, if it contains more than one vertex, then its
  treewidth is exactly 1.›
corollary treewidth_tree_exact:
  fixes G :: "nat Graph" (structure)
  assumes "Tree G" "card V⇘G⇙ > 1"
  shows "Graph.treewidth G = 1"
  using assms Graph.treewidth_lower_bound_1 Tree.tree_has_edge Tree_def treewidth_tree
  by fastforce

end