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 ― ‹locale Tree›
definition unique_connecting_path :: "('a, 'b) Graph_scheme  'a  'a  'a Walk"
  (infix "ı" 71) where "unique_connecting_path G v w  THE xs. v xsGw"
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 (vw)  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)" "uw"
  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. vw"
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 (vw))" 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: "st  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 "st"
  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 "st"
  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 "st"} is a separator in a tree.
›
theorem left_tree_separates:
  assumes st: "st" 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 "uhd 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 uhd 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"] uhd 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 uhd 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 "st" "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 ― ‹locale Tree›

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   vparent 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: "vroot  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: "vw  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 "vw = [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 ― ‹locale RootedTree›

end