Theory TreewidthCompleteGraph

section ‹Treewidth of Complete Graphs›

theory TreewidthCompleteGraph
imports TreeDecomposition begin

text ‹As an application of the separator theorem ‹bags_separate›, or more precisely its
  corollary ‹bag_no_drop›, we show that a complete graph of size @{term "n :: nat"}
  (a clique) has treewidth @{term "(n::nat)-1"}.›
theorem (in Graph) treewidth_complete_graph:
  assumes "⋀v w. ⟦ v ∈ V; w ∈ V; v ≠ w ⟧ ⟹ v→w"
  shows "treewidth = card V - 1"
proof-
  {
    assume "V ≠ {}"
    obtain T bag where
      T: "TreeDecomposition G (T :: nat Graph) bag" "treewidth = TreeDecomposition.width T bag"
      using treewidth_cards_treewidth by blast
    interpret TreeDecomposition G T bag using T(1) .

    assume "¬?thesis"
    hence "width ≠ card V - 1" by (simp add: T(2))
    text ‹Let @{term s} be a bag of maximal size.›
    moreover obtain s where s: "s ∈ V⇘T⇙" "card (bag s) = max_bag_card"
      using max_bag_card_in_bag_cards ‹V ≠ {}› by fastforce
    text ‹The treewidth cannot be larger than @{term "card V - 1"}, so due to our assumption
      @{term "width ≠ card V - 1" } it must be smaller, hence @{term "card (bag s) < card V"}.›
    ultimately have "card (bag s) < card V" unfolding width_def
      using ‹V ≠ {}› empty_tree_empty_V le_eq_less_or_eq max_bag_card_upper_bound_V by presburger
    then obtain v where v: "v ∈ V" "v ∉ bag s" by (meson bag_finite card_mono not_less s(1) subsetI)

    text ‹There exists a bag containing @{term v}.  We consider the path from @{term s} to
      @{term t} and find that somewhere along this path there exists a bag containing
      @{term "insert v (bag s)"}, which is a contradiction because such a bag would be too big.›
    obtain t where t: "t ∈ V⇘T⇙" "v ∈ bag t" using bags_exist v(1) by blast
    with s have "∃t ∈ V⇘T⇙. insert v (bag s) ⊆ bag t" proof (induct "s ↝⇘T⇙ t" arbitrary: s)
      case Nil thus ?case using T.unique_connecting_path_properties(2) by fastforce
    next
      case (Cons x xs s)
      show ?case proof (cases)
        assume "v ∈ bag s" thus ?thesis using t Cons.prems(1) by blast
      next
        assume "v ∉ bag s"
        hence "s ≠ t" using t(2) by blast
        hence "xs ≠ Nil" using Cons.hyps(2) Cons.prems(1,3)
          by (metis T.unique_connecting_path_properties(3,4) last_ConsL list.sel(1))
        moreover have "x = s" using Cons.hyps(2) Cons.prems(1) t(1)
          by (metis T.unique_connecting_path_properties(3) list.sel(1))
        ultimately obtain s' xs' where s': "s # s' # xs' = s ↝⇘T⇙ t"
          using Cons.hyps(2) list.exhaust by metis
        moreover have st_path: "T.path (s ↝⇘T⇙ t)"
          by (simp add: Cons.prems(1) T.unique_connecting_path_properties(1) t(1))
        ultimately have "s' ∈ V⇘T⇙" by (metis T.edges_are_in_V(2) T.path_first_edge)
        text ‹Bags can never drop vertices because every vertex has a neighbor in @{term G} which
          has not yet been visited.›
        have s_in_s': "bag s ⊆ bag s'" proof
          fix w assume "w ∈ bag s"
          moreover have "s →⇘T⇙ s'" using s' st_path by (metis T.walk_first_edge)
          moreover have "v ∈ left_part s' s" using Cons.prems(1,4) s' t(1)
            by (metis T.left_treeI T.unique_connecting_path_rev insert_subset left_partI
                list.simps(15) set_rev subsetI)
          ultimately show "w ∈ bag s'"
            using bag_no_drop Cons.prems(1,4) ‹v ∉ bag s› assms bags_in_V v(1) by blast
        qed
        text ‹Bags can never gain vertices because we started with a bag of maximal size.›
        moreover have "card (bag s') ≤ card (bag s)" proof-
          have "card (bag s') ≤ max_bag_card" unfolding max_bag_card_def
            using Max_ge ‹s' ∈ V⇘T⇙› bag_cards_finite by blast
          thus ?thesis using Cons.prems(2) by auto
        qed
        ultimately have "bag s' = bag s" using ‹s' ∈ V⇘T⇙› bag_finite card_seteq by blast
        thus ?thesis
          using Cons.hyps Cons.prems(1,2) ‹s' ∈ V⇘T⇙› t s' st_path ‹xs ≠ []›
          by (metis T.path_from_toI T.path_tl T.unique_connecting_path_properties(4)
              T.unique_connecting_path_unique last.simps list.sel(1,3))
      qed
    qed
    hence "∃t ∈ V⇘T⇙. card (bag s) < card (bag t)" using v(2)
      by (metis bag_finite card_seteq insert_subset not_le)
    hence False using s Max.coboundedI bag_cards_finite not_le unfolding max_bag_card_def by auto
  }
  thus ?thesis using treewidth_upper_bound_V card.empty diff_diff_cancel zero_diff by fastforce
qed

end