Theory Tree_Graph

section ‹Graphs and Trees›

theory Tree_Graph
  imports Undirected_Graph_Theory.Undirected_Graphs_Root
begin

subsection ‹Miscellaneous›

definition (in ulgraph) loops :: "'a edge set" where
  "loops = {e∈E. is_loop e}"

definition (in ulgraph) sedges :: "'a edge set" where
  "sedges = {e∈E. is_sedge e}"

lemma (in ulgraph) union_loops_sedges: "loops ∪ sedges = E"
  unfolding loops_def sedges_def is_loop_def is_sedge_def using alt_edge_size by blast

lemma (in ulgraph) disjnt_loops_sedges: "disjnt loops sedges"
  unfolding disjnt_def loops_def sedges_def is_loop_def is_sedge_def by auto

lemma (in fin_ulgraph) finite_loops: "finite loops"
  unfolding loops_def using fin_edges by auto

lemma (in fin_ulgraph) finite_sedges: "finite sedges"
  unfolding sedges_def using fin_edges by auto

lemma (in ulgraph) edge_incident_vert: "e ∈ E ⟹ ∃v∈V. vincident v e"
  using edge_size wellformed by (metis empty_not_edge equals0I vincident_def incident_edge_in_wf)

lemma (in ulgraph) Union_incident_edges: "(⋃v∈V. incident_edges v) = E"
  unfolding incident_edges_def using edge_incident_vert by auto


lemma (in ulgraph) induced_edges_mono: "V⇩1 ⊆ V⇩2 ⟹ induced_edges V⇩1 ⊆ induced_edges V⇩2"
  using induced_edges_def by auto

definition (in graph_system) remove_vertex :: "'a ⇒ 'a pregraph" where
  "remove_vertex v = (V - {v}, {e∈E. ¬ vincident v e})"

lemma (in ulgraph) ex_neighbor_degree_not_0:
  assumes degree_non_0: "degree v ≠ 0"
    shows "∃u∈V. vert_adj v u"
proof-
  have "∃e∈E. v ∈ e" using degree_non_0 elem_exists_non_empty_set
    unfolding degree_def incident_sedges_def incident_loops_def vincident_def by auto
  then show ?thesis
    by (metis degree_non_0 in_mono is_isolated_vertex_def is_isolated_vertex_degree0 vert_adj_sym wellformed)
qed

lemma (in ulgraph) ex1_neighbor_degree_1:
  assumes degree_1: "degree v = 1"
  shows "∃!u. vert_adj v u"
proof-
  have "card (incident_loops v) = 0" using degree_1 unfolding degree_def by auto
  then have incident_loops: "incident_loops v = {}" by (simp add: finite_incident_loops)
  then have card_incident_sedges: "card (incident_sedges v) = 1" using degree_1 unfolding degree_def by simp
  obtain u where vert_adj: "vert_adj v u" using degree_1 ex_neighbor_degree_not_0 by force
  then have "u ≠ v" using incident_loops unfolding incident_loops_def vert_adj_def by blast
  then have u_incident: "{v,u} ∈ incident_sedges v" using vert_adj unfolding incident_sedges_def vert_adj_def vincident_def by simp
  then have incident_sedges: "incident_sedges v = {{v,u}}" using card_incident_sedges
    by (simp add: comp_sgraph.card1_incident_imp_vert comp_sgraph.vincident_def)
  have "vert_adj v u' ⟹ u' = u" for u'
  proof-
    assume v_u'_adj: "vert_adj v u'"
    then have "u' ≠ v" using incident_loops unfolding incident_loops_def vert_adj_def by blast
    then have "{v,u'} ∈ incident_sedges v" using v_u'_adj unfolding incident_sedges_def vert_adj_def vincident_def by simp
    then show "u' = u" using incident_sedges by force
  qed
  then show ?thesis using vert_adj by blast
qed

lemma (in ulgraph) degree_1_edge_partition:
  assumes degree_1: "degree v = 1"
  shows "E = {{THE u. vert_adj v u, v}} ∪ {e ∈ E. v ∉ e}"
proof-
  have "card (incident_loops v) = 0" using degree_1 unfolding degree_def by auto
  then have incident_loops: "incident_loops v = {}" by (simp add: finite_incident_loops)
  then have "card (incident_sedges v) = 1" using degree_1 unfolding degree_def by simp
  then have card_incident_edges: "card (incident_edges v) = 1" using incident_loops incident_edges_union by simp
  obtain u where vert_adj: "vert_adj v u" using ex1_neighbor_degree_1 degree_1 by blast
  then have "{v, u} ∈ {e ∈ E. v ∈ e}" unfolding vert_adj_def by blast
  then have edges_incident_v: "{e ∈ E. v ∈ e} = {{v, u}}" using card_incident_edges card_1_singletonE singletonD
    unfolding incident_edges_def vincident_def by metis
  have u: "u = (THE u. vert_adj v u)" using vert_adj ex1_neighbor_degree_1 degree_1
    by (simp add: the1_equality)
  show ?thesis using edges_incident_v u by blast
qed

lemma (in sgraph) vert_adj_not_eq: "vert_adj u v ⟹ u ≠ v"
  unfolding vert_adj_def using edge_vertices_not_equal by blast

subsection ‹Degree›

lemma (in ulgraph) empty_E_degree_0: "E = {} ⟹ degree v = 0"
  using incident_edges_empty degree0_inc_edges_empt_iff unfolding incident_edges_def by simp

lemma (in fin_ulgraph) handshaking: "(∑v∈V. degree v) = 2 * card E"
  using fin_edges fin_ulgraph_axioms
proof (induction E)
  case empty
  then interpret g: fin_ulgraph V "{}" .
  show ?case using g.empty_E_degree_0 by simp
next
  case (insert e E')
  then interpret g': fin_ulgraph V "insert e E'" by blast
  interpret g: fin_ulgraph V E' using g'.wellformed g'.edge_size finV by (unfold_locales, auto)
  show ?case
  proof (cases "is_loop e")
    case True
    then obtain u where e: "e = {u}" using card_1_singletonE is_loop_def by blast
    then have inc_sedges: "⋀v. g'.incident_sedges v = g.incident_sedges v" unfolding g'.incident_sedges_def g.incident_sedges_def by auto
    have "⋀v. v ≠ u ⟹ g'.incident_loops v = g.incident_loops v" unfolding g'.incident_loops_def g.incident_loops_def using e by auto
    then have degree_not_u: "⋀v. v ≠ u ⟹ g'.degree v = g.degree v" using inc_sedges unfolding g'.degree_def g.degree_def by auto
    have "g'.incident_loops u = g.incident_loops u ∪ {e}" unfolding g'.incident_loops_def g.incident_loops_def using e by auto
    then have degree_u: "g'.degree u = g.degree u + 2" using inc_sedges insert(2) g.finite_incident_loops g.incident_loops_def unfolding g'.degree_def g.degree_def by auto
    have "u ∈ V" using e g'.wellformed by blast
    then have "(∑v∈V. g'.degree v) = g'.degree u + (∑v∈V-{u}. g'.degree v)"
      by (simp add: finV sum.remove)
    also have "… = (∑v∈V. g.degree v) + 2" using degree_not_u degree_u sum.remove[OF finV ‹u∈V›, of g.degree] by auto
    also have "… = 2 * card (insert e E')" using insert g.fin_ulgraph_axioms by auto
    finally show ?thesis .
  next
    case False
    obtain u w where e: "e = {u,w}" using g'.obtain_edge_pair_adj by fastforce
    then have card_e: "card e = 2" using False g'.alt_edge_size is_loop_def by auto
    then have "u ≠ w" using card_2_iff using e by fastforce
    have inc_loops: "⋀v. g'.incident_loops v = g.incident_loops v"
      unfolding g'.incident_loops_alt g.incident_loops_alt using False is_loop_def by auto
    have "⋀v. v ≠ u ⟹ v ≠ w ⟹ g'.incident_sedges v = g.incident_sedges v"
      unfolding g'.incident_sedges_def g.incident_sedges_def g.vincident_def using e by auto
    then have degree_not_u_w: "⋀v. v ≠ u ⟹ v ≠ w ⟹ g'.degree v = g.degree v"
      unfolding g'.degree_def g.degree_def using inc_loops by auto
    have "g'.incident_sedges u = g.incident_sedges u ∪ {e}"
      unfolding g'.incident_sedges_def g.incident_sedges_def g.vincident_def using e card_e by auto
    then have degree_u: "g'.degree u = g.degree u + 1"
      using inc_loops insert(2) g.fin_edges g.finite_inc_sedges g.incident_sedges_def
      unfolding g'.degree_def g.degree_def by auto
    have "g'.incident_sedges w = g.incident_sedges w ∪ {e}"
      unfolding g'.incident_sedges_def g.incident_sedges_def g.vincident_def using e card_e by auto
    then have degree_w: "g'.degree w = g.degree w + 1"
      using inc_loops insert(2) g.fin_edges g.finite_inc_sedges g.incident_sedges_def
      unfolding g'.degree_def g.degree_def by auto
    have inV: "u ∈ V" "w ∈ V-{u}" using e g'.wellformed ‹u≠w› by auto
    then have "(∑v∈V. g'.degree v) = g'.degree u + g'.degree w + (∑v∈V-{u}-{w}. g'.degree v)"
      using sum.remove finV by (metis add.assoc finite_Diff)
    also have "… = g.degree u + g.degree w + (∑v∈V-{u}-{w}. g.degree v) + 2"
      using degree_not_u_w degree_u degree_w by simp
    also have "… = (∑v∈V. g.degree v) + 2" using sum.remove finV inV by (metis add.assoc finite_Diff)
    also have "… = 2 * card (insert e E')" using insert g.fin_ulgraph_axioms by auto
    finally show ?thesis .
  qed
qed

lemma (in fin_ulgraph) degree_remove_adj_ne_vert:
  assumes "u ≠ v"
    and vert_adj: "vert_adj u v"
    and remove_vertex: "remove_vertex u = (V',E')"
  shows "ulgraph.degree E' v = degree v - 1"
proof-
  interpret G': fin_ulgraph V' E' using remove_vertex wellformed edge_size finV unfolding remove_vertex_def vincident_def
    by (unfold_locales, auto)
  have E': "E' = {e ∈ E. u ∉ e}" using remove_vertex unfolding remove_vertex_def vincident_def by simp
  have incident_loops': "G'.incident_loops v = incident_loops v" unfolding incident_loops_def
    using ‹u≠v› E' G'.incident_loops_def by auto
  have uv_incident: "{u,v} ∈ incident_sedges v" using vert_adj ‹u≠v› unfolding vert_adj_def incident_sedges_def vincident_def by simp
  have uv_incident': "{u, v} ∉ G'.incident_sedges v" unfolding G'.incident_sedges_def vincident_def using E' by blast
  have "e ∈ E ⟹ u ∈ e ⟹ v ∈ e ⟹ card e = 2 ⟹ e = {u,v}" for e
    using ‹u≠v› obtain_edge_pair_adj by blast
  then have "{e ∈ E. u ∈ e ∧ v ∈ e ∧ card e = 2} = {{u,v}}" using uv_incident unfolding incident_sedges_def by blast
  then have "incident_sedges v = G'.incident_sedges v ∪ {{u,v}}" unfolding G'.incident_sedges_def incident_sedges_def vincident_def using E' by blast
  then show ?thesis unfolding G'.degree_def degree_def using incident_loops' uv_incident' G'.finite_inc_sedges G'.fin_edges by auto
qed

lemma (in ulgraph) degree_remove_non_adj_vert:
  assumes "u ≠ v"
    and vert_non_adj: "¬ vert_adj u v"
    and remove_vertex: "remove_vertex u = (V', E')"
  shows "ulgraph.degree E' v = degree v"
proof-
  interpret G': ulgraph V' E' using remove_vertex wellformed edge_size unfolding remove_vertex_def vincident_def
    by (unfold_locales, auto)
  have E': "E' = {e ∈ E. u ∉ e}" using remove_vertex unfolding remove_vertex_def vincident_def by simp
  have incident_loops': "G'.incident_loops v = incident_loops v" unfolding incident_loops_def
    using ‹u≠v› E' G'.incident_loops_def by auto
  have "G'.incident_sedges v = incident_sedges v" unfolding G'.incident_sedges_def incident_sedges_def vincident_def
    using E' ‹u≠v› vincident_def vert_adj_edge_iff2 vert_non_adj by auto
  then show ?thesis using incident_loops' unfolding G'.degree_def degree_def by simp
qed

subsection ‹Walks›

lemma (in ulgraph) walk_edges_induced_edges: "is_walk p ⟹ set (walk_edges p) ⊆ induced_edges (set p)"
  unfolding induced_edges_def is_walk_def by (induction p rule: walk_edges.induct) auto

lemma (in ulgraph) walk_edges_in_verts: "e ∈ set (walk_edges xs) ⟹ e ⊆ set xs"
  by (induction xs rule: walk_edges.induct) auto

lemma (in ulgraph) is_walk_prefix: "is_walk (xs@ys) ⟹ xs ≠ [] ⟹ is_walk xs"
  unfolding is_walk_def using walk_edges_append_ss2 by fastforce

lemma (in ulgraph) split_walk_edge: "{x,y} ∈ set (walk_edges p) ⟹
  ∃xs ys. p = xs @ x # y # ys ∨ p = xs @ y # x # ys"
  by (induction p rule: walk_edges.induct) (auto, metis append_Nil doubleton_eq_iff, (metis append_Cons)+)

subsection ‹Paths›

lemma (in ulgraph) is_gen_path_wf: "is_gen_path p ⟹ set p ⊆ V"
  unfolding is_gen_path_def using is_walk_wf by auto

lemma (in ulgraph) path_wf: "is_path p ⟹ set p ⊆ V"
  by (simp add: is_path_walk is_walk_wf)

lemma (in fin_ulgraph) length_gen_path_card_V: "is_gen_path p ⟹ walk_length p ≤ card V"
  by (metis card_mono distinct_card distinct_tl finV is_gen_path_def is_walk_def length_tl
      list.exhaust_sel order_trans set_subset_Cons walk_length_conv)

lemma (in fin_ulgraph) length_path_card_V: "is_path p ⟹ length p ≤ card V"
  by (metis path_wf card_mono distinct_card finV is_path_def)

lemma (in ulgraph) is_gen_path_prefix: "is_gen_path (xs@ys) ⟹ xs ≠ [] ⟹ is_gen_path (xs)"
  unfolding is_gen_path_def using is_walk_prefix
  by (auto, metis Int_iff distinct.simps(2) emptyE last_appendL last_appendR last_in_set list.collapse)

lemma (in ulgraph) connecting_path_append: "connecting_path u w (xs@ys) ⟹ xs ≠ [] ⟹ connecting_path u (last xs) xs"
  unfolding connecting_path_def using is_gen_path_prefix by auto

lemma (in ulgraph) connecting_path_tl: "connecting_path u v (u # w # xs) ⟹ connecting_path w v (w # xs)"
  unfolding connecting_path_def is_gen_path_def using is_walk_drop_hd distinct_tl by auto

lemma (in fin_ulgraph) obtain_longest_path:
  assumes "e ∈ E"
    and sedge: "is_sedge e"
  obtains p where "is_path p" "∀s. is_path s ⟶ length s ≤ length p"
proof-
  let ?longest_path = "ARG_MAX length p. is_path p"
  obtain u v where e: "u ≠ v" "e = {u,v}" using sedge card_2_iff unfolding is_sedge_def by metis
  then have inV: "u ∈ V" "v ∈ V" using ‹e∈E› wellformed by auto
  then have path_ex: "is_path [u,v]" using e ‹e∈E› unfolding is_path_def is_open_walk_def is_walk_def by simp
  obtain p where p_is_path: "is_path p" and p_longest_path: "∀s. is_path s ⟶ length s ≤ length p"
    using path_ex length_path_card_V ex_has_greatest_nat[of is_path "[u,v]" length gorder] by force
  then show ?thesis ..
qed

subsection ‹Cycles›

context ulgraph
begin

definition is_cycle2 :: "'a list ⇒ bool" where
  "is_cycle2 xs ⟷ is_cycle xs ∧ distinct (walk_edges xs)"

lemma loop_is_cycle2: "{v} ∈ E ⟹ is_cycle2 [v, v]"
  unfolding is_cycle2_def is_cycle_alt is_walk_def using wellformed walk_length_conv by auto

end

lemma (in sgraph) cycle2_min_length:
  assumes cycle: "is_cycle2 c"
  shows "walk_length c ≥ 3"
proof-
  consider "c = []" | "∃v1. c = [v1]" | "∃v1 v2. c = [v1, v2]" | "∃v1 v2 v3. c = [v1, v2, v3]" | "∃v1 v2 v3 v4 vs. c = v1#v2#v3#v4#vs"
    by (metis list.exhaust_sel)
  then show ?thesis using cycle walk_length_conv singleton_not_edge unfolding is_cycle2_def is_cycle_alt is_walk_def by (cases, auto)
qed

lemma (in fin_ulgraph) length_cycle_card_V: "is_cycle c ⟹ walk_length c ≤ Suc (card V)"
  using length_gen_path_card_V unfolding is_gen_path_def is_cycle_alt by fastforce

lemma (in ulgraph) is_cycle_connecting_path: "is_cycle (u#v#xs) ⟹ connecting_path v u (v#xs)"
  unfolding is_cycle_def connecting_path_def is_closed_walk_def is_gen_path_def using is_walk_drop_hd by auto

lemma (in ulgraph) cycle_edges_notin_tl: "is_cycle2 (u#v#xs) ⟹ {u,v} ∉ set (walk_edges (v#xs))"
  unfolding is_cycle2_def by simp

subsection ‹Subgraphs›

locale ulsubgraph = subgraph V⇩H E⇩H V⇩G E⇩G +
  G: ulgraph V⇩G E⇩G for V⇩H E⇩H V⇩G E⇩G
begin

interpretation H: ulgraph V⇩H E⇩H
  using is_subgraph_ulgraph G.ulgraph_axioms by auto

lemma is_walk: "H.is_walk xs ⟹ G.is_walk xs"
  unfolding H.is_walk_def G.is_walk_def using verts_ss edges_ss by blast

lemma is_closed_walk: "H.is_closed_walk xs ⟹ G.is_closed_walk xs"
  unfolding H.is_closed_walk_def G.is_closed_walk_def using is_walk by blast

lemma is_gen_path: "H.is_gen_path p ⟹ G.is_gen_path p"
  unfolding H.is_gen_path_def G.is_gen_path_def using is_walk by blast

lemma connecting_path: "H.connecting_path u v p ⟹ G.connecting_path u v p"
  unfolding H.connecting_path_def G.connecting_path_def using is_gen_path by blast

lemma is_cycle: "H.is_cycle c ⟹ G.is_cycle c"
  unfolding H.is_cycle_def G.is_cycle_def using is_closed_walk by blast

lemma is_cycle2: "H.is_cycle2 c ⟹ G.is_cycle2 c"
  unfolding H.is_cycle2_def G.is_cycle2_def using is_cycle by blast

lemma vert_connected: "H.vert_connected u v ⟹ G.vert_connected u v"
  unfolding H.vert_connected_def G.vert_connected_def using connecting_path by blast

lemma is_connected_set: "H.is_connected_set V' ⟹ G.is_connected_set V'"
  unfolding H.is_connected_set_def G.is_connected_set_def using vert_connected by blast

end

lemma (in graph_system) subgraph_remove_vertex: "remove_vertex v = (V', E') ⟹ subgraph V' E' V E"
  using wellformed unfolding remove_vertex_def vincident_def by (unfold_locales, auto)

subsection ‹Connectivity›

lemma (in ulgraph) connecting_path_connected_set:
  assumes conn_path: "connecting_path u v p"
  shows "is_connected_set (set p)"
proof-
  have "∀w∈set p. vert_connected u w"
  proof
    fix w assume "w ∈ set p"
    then obtain xs ys where "p = xs@[w]@ys" using split_list by fastforce
    then have "connecting_path u w (xs@[w])" using conn_path unfolding connecting_path_def using is_gen_path_prefix by (auto simp: hd_append)
    then show "vert_connected u w" unfolding vert_connected_def by blast
  qed
  then show ?thesis using vert_connected_rev vert_connected_trans unfolding is_connected_set_def by blast
qed

lemma (in ulgraph) vert_connected_neighbors:
  assumes "{v,u} ∈ E"
  shows "vert_connected v u"
proof-
  have "connecting_path v u [v,u]" unfolding connecting_path_def is_gen_path_def is_walk_def using assms wellformed by auto
  then show ?thesis unfolding vert_connected_def by auto
qed

lemma (in ulgraph) connected_empty_E:
  assumes empty: "E = {}"
    and connected: "vert_connected u v"
  shows "u = v"
proof (rule ccontr)
  assume "u ≠ v"
  then obtain p where conn_path: "connecting_path u v p" using connected unfolding vert_connected_def by blast
  then obtain e where "e ∈ set (walk_edges p)" using ‹u≠v› connecting_path_length_bound unfolding walk_length_def by fastforce
  then have "e ∈ E" using conn_path unfolding connecting_path_def is_gen_path_def is_walk_def by blast
  then show False using empty by blast
qed

lemma (in fin_ulgraph) degree_0_not_connected:
  assumes degree_0: "degree v = 0"
    and "u ≠ v"
  shows "¬ vert_connected v u"
proof
  assume connected: "vert_connected v u"
  then obtain p where conn_path: "connecting_path v u p" unfolding vert_connected_def by blast
  then have "walk_length p ≥ 1" using ‹u≠v› connecting_path_length_bound by metis
  then have "length p ≥ 2" using walk_length_conv by simp
  then obtain w p' where "p = v#w#p'" using walk_length_conv conn_path unfolding connecting_path_def
    by (metis assms(2) is_gen_path_def is_walk_not_empty2 last_ConsL list.collapse)
  then have inE: "{v,w} ∈ E" using conn_path unfolding connecting_path_def is_gen_path_def is_walk_def by simp
  then have "{v,w} ∈ incident_edges v" unfolding incident_edges_def vincident_def by simp
  then show False using degree0_inc_edges_empt_iff fin_edges degree_0 by blast
qed

lemma (in fin_connected_ulgraph) degree_not_0:
  assumes "card V ≥ 2"
    and inV: "v ∈ V"
  shows "degree v ≠ 0"
proof-
  obtain u where "u ∈ V" and "u ≠ v" using assms
    by (metis card_eq_0_iff card_le_Suc0_iff_eq less_eq_Suc_le nat_less_le not_less_eq_eq numeral_2_eq_2)
  then show ?thesis using degree_0_not_connected inV vertices_connected by blast
qed

lemma (in connected_ulgraph) V_E_empty: "E = {} ⟹ ∃v. V = {v}"
  using connected_empty_E connected not_empty unfolding is_connected_set_def
  by (metis ex_in_conv insert_iff mk_disjoint_insert)

lemma (in connected_ulgraph) vert_connected_remove_edge:
  assumes e: "{u,v} ∈ E"
  shows "∀w∈V. ulgraph.vert_connected V (E - {{u,v}}) w u ∨ ulgraph.vert_connected V (E - {{u,v}}) w v"
proof
  fix w assume "w∈V"
  interpret g': ulgraph V "E - {{u,v}}" using wellformed edge_size by (unfold_locales, auto)
  have inV: "u ∈ V" "v ∈ V" using e wellformed by auto
  obtain p where conn_path: "connecting_path w v p" using connected inV ‹w∈V› unfolding is_connected_set_def vert_connected_def by blast
  then show "g'.vert_connected w u ∨ g'.vert_connected w v"
  proof (cases "{u,v} ∈ set (walk_edges p)")
    case True
    assume walk_edge: "{u,v} ∈ set (walk_edges p)"
    then show ?thesis
    proof (cases "w = v")
      case True
      then show ?thesis using inV g'.vert_connected_id by blast
    next
      case False
      then have distinct: "distinct p" using conn_path by (simp add: connecting_path_def is_gen_path_distinct)
      have "u ∈ set p" using walk_edge walk_edges_in_verts by blast
      obtain xs ys where p_split: "p = xs @ u # v # ys ∨ p = xs @ v # u # ys" using split_walk_edge[OF walk_edge] by blast
      have v_notin_ys: "v ∉ set ys" using distinct p_split by auto
      have "last p = v" using conn_path unfolding connecting_path_def by simp
      then have p: "p = (xs@[u]) @ [v]" using v_notin_ys p_split last_in_set last_appendR
        by (metis append.assoc append_Cons last.simps list.discI self_append_conv2)
      then have conn_path_u: "connecting_path w u (xs@[u])" using connecting_path_append conn_path by fastforce
      have "v ∉ set (xs@[u])" using p distinct by auto
      then have "{u,v} ∉ set (walk_edges (xs@[u]))" using walk_edges_in_verts by blast
      then have "g'.connecting_path w u (xs@[u])" using conn_path_u
        unfolding g'.connecting_path_def connecting_path_def g'.is_gen_path_def is_gen_path_def g'.is_walk_def is_walk_def by blast
      then show ?thesis unfolding g'.vert_connected_def by blast
    qed
  next
    case False
    then have "g'.connecting_path w v p" using conn_path
      unfolding g'.connecting_path_def connecting_path_def g'.is_gen_path_def is_gen_path_def g'.is_walk_def is_walk_def by blast
    then show ?thesis unfolding g'.vert_connected_def by blast
  qed
qed

lemma (in ulgraph) vert_connected_remove_cycle_edge:
  assumes cycle: "is_cycle2 (u#v#xs)"
    shows "ulgraph.vert_connected V (E - {{u,v}}) u v"
proof-
  interpret g': ulgraph V "E - {{u,v}}" using wellformed edge_size by (unfold_locales, auto)
  have conn_path: "connecting_path v u (v#xs)" using cycle is_cycle_connecting_path unfolding is_cycle2_def by blast
  have "{u,v} ∉ set (walk_edges (v#xs))" using cycle unfolding is_cycle2_def by simp
  then have "g'.connecting_path v u (v#xs)" using conn_path
    unfolding g'.connecting_path_def connecting_path_def g'.is_gen_path_def is_gen_path_def g'.is_walk_def is_walk_def by blast
  then show ?thesis using g'.vert_connected_rev unfolding g'.vert_connected_def by blast
qed

lemma (in connected_ulgraph) connected_remove_cycle_edges:
  assumes cycle: "is_cycle2 (u#v#xs)"
  shows "connected_ulgraph V (E - {{u,v}})"
proof-
  interpret g': ulgraph V "E - {{u,v}}" using wellformed edge_size by (unfold_locales, auto)
  have "g'.vert_connected x y" if inV: "x ∈ V" "y ∈ V" for x y
  proof-
    have e: "{u,v} ∈ E" using cycle unfolding is_cycle2_def is_cycle_alt is_walk_def by auto
    show ?thesis using vert_connected_remove_cycle_edge[OF cycle] vert_connected_remove_edge[OF e] g'.vert_connected_trans g'.vert_connected_rev inV by metis
  qed
  then show ?thesis using not_empty by (unfold_locales, auto simp: g'.is_connected_set_def)
qed

lemma (in connected_ulgraph) connected_remove_leaf:
  assumes degree: "degree l = 1"
    and remove_vertex: "remove_vertex l = (V', E')"
  shows "ulgraph.is_connected_set V' E' V'"
proof-
  interpret g': ulgraph V' E' using remove_vertex wellformed edge_size
    unfolding remove_vertex_def vincident_def by (unfold_locales, auto)
  have V': "V' = V - {l}" using remove_vertex unfolding remove_vertex_def by simp
  have E': "E' = {e∈E. l ∉ e}" using remove_vertex unfolding remove_vertex_def vincident_def by simp
  have "u ∈ V' ⟹ v ∈ V' ⟹ g'.vert_connected u v" for u v
  proof-
    assume inV': "u ∈ V'" "v ∈ V'"
    then have inV: "u ∈ V" "v ∈ V" using remove_vertex unfolding remove_vertex_def by auto
    then obtain p where conn_path: "connecting_path u v p" using vertices_connected_path by blast
    show ?thesis
    proof (cases "u = v")
      case True
      then show ?thesis using g'.vert_connected_id inV' by simp
    next
      case False
      then have distinct: "distinct p" using conn_path unfolding connecting_path_def is_gen_path_def by blast
      have l_notin_p: "l ∉ set p"
      proof
        assume l_in_p: "l ∈ set p"
        then obtain xs ys where p: "p = xs @ l # ys" by (meson split_list)
        have "l ≠ u" "l ≠ v" using inV' remove_vertex unfolding remove_vertex_def by auto
        then have "xs ≠ []" using p conn_path unfolding connecting_path_def by fastforce
        then obtain x where last_xs: "last xs = x" by simp
        then have "x ≠ l" using distinct p ‹xs≠[]› by auto
        have "{x,l} ∈ set (walk_edges p)" using walk_edges_append_union ‹xs≠[]› unfolding p
          by (simp add: walk_edges_append_union last_xs)
        then have xl_incident: "{x,l} ∈ incident_sedges l" using conn_path ‹x≠l›
          unfolding connecting_path_def is_gen_path_def is_walk_def incident_sedges_def vincident_def by auto

        have "ys ≠ []" using ‹l≠v› p conn_path unfolding connecting_path_def by fastforce
        then obtain y ys' where ys: "ys = y # ys'" by (meson list.exhaust)
        then have "y ≠ l" using distinct p by auto
        then have "{y,l} ∈ set (walk_edges p)" using p ys conn_path walk_edges_append_ss1 by fastforce
        then have yl_incident: "{y,l} ∈ incident_sedges l" using conn_path ‹y≠l›
          unfolding connecting_path_def is_gen_path_def is_walk_def incident_sedges_def vincident_def by auto

        have card_loops: "card (incident_loops l) = 0" using degree unfolding degree_def by auto
        have "x ≠ y" using distinct last_xs ‹xs≠[]› unfolding p ys by fastforce
        then have "{x,l} ≠ {y,l}" by (metis doubleton_eq_iff)
        then have "card (incident_sedges l) ≠ 1" using xl_incident yl_incident
          by (metis card_1_singletonE singletonD)
        then have "degree l ≠ 1" using card_loops unfolding degree_def by simp
        then show False using degree ..
      qed
      then have "set (walk_edges p) ⊆ E'" using walk_edges_in_verts conn_path E' unfolding connecting_path_def is_gen_path_def is_walk_def by blast
      then have "g'.connecting_path u v p" using conn_path V' l_notin_p
        unfolding g'.connecting_path_def connecting_path_def g'.is_gen_path_def is_gen_path_def g'.is_walk_def is_walk_def by blast
      then show ?thesis unfolding g'.vert_connected_def by blast
    qed
  qed
  then show ?thesis unfolding g'.is_connected_set_def by blast
qed

lemma (in connected_sgraph) connected_two_graph_edges:
  assumes "u ≠ v"
    and V: "V = {u,v}"
  shows "E = {{u,v}}"
proof-
  obtain p where conn_path: "connecting_path u v p" using V vertices_connected_path by blast
  then obtain p' where p: "p = u # p' @ [v]" using ‹u≠v› unfolding connecting_path_def is_gen_path_def 
    by (metis append_Nil is_walk_not_empty2 list.exhaust_sel list.sel(1) snoc_eq_iff_butlast tl_append2)
  have "distinct p" using conn_path ‹u≠v› unfolding connecting_path_def is_gen_path_def by auto
  then have "p' = []" using V conn_path is_gen_path_wf append_is_Nil_conv last_in_set self_append_conv2
    unfolding connecting_path_def p by fastforce
  then have edge_in_E: "{u,v} ∈ E" using ‹u≠v› conn_path
    unfolding p connecting_path_def is_gen_path_def is_walk_def by simp
  have "E ⊆ {{}, {u}, {v}, {u,v}}" using wellformed V by blast
  then show ?thesis using two_edges edge_in_E by fastforce
qed

subsection "Connected components"

context ulgraph
begin

abbreviation "vert_connected_rel ≡ {(u,v). vert_connected u v}"

definition connected_components :: "'a set set" where
  "connected_components = V // vert_connected_rel"

definition connected_component_of :: "'a ⇒ 'a set" where
  "connected_component_of v = vert_connected_rel `` {v}"

lemma vert_connected_rel_on_V: "vert_connected_rel ⊆ V × V"
  using vert_connected_wf by auto

lemma vert_connected_rel_refl: "refl_on V vert_connected_rel"
  unfolding refl_on_def using vert_connected_rel_on_V vert_connected_id by simp

lemma vert_connected_rel_sym: "sym vert_connected_rel"
  unfolding sym_def using vert_connected_rev by simp

lemma vert_connected_rel_trans: "trans vert_connected_rel"
  unfolding trans_def using vert_connected_trans by blast

lemma equiv_vert_connected: "equiv V vert_connected_rel"
  unfolding equiv_def using vert_connected_rel_refl vert_connected_rel_sym vert_connected_rel_trans by blast

lemma connected_component_non_empty: "V' ∈ connected_components ⟹ V' ≠ {}"
  unfolding connected_components_def using equiv_vert_connected in_quotient_imp_non_empty by auto

lemma connected_component_connected: "V' ∈ connected_components ⟹ is_connected_set V'"
  unfolding connected_components_def is_connected_set_def using quotient_eq_iff[OF equiv_vert_connected, of V' V'] by simp

lemma connected_component_wf: "V' ∈ connected_components ⟹ V' ⊆ V"
  by (simp add: connected_component_connected is_connected_set_wf)

lemma connected_component_of_self: "v ∈ V ⟹ v ∈ connected_component_of v"
  unfolding connected_component_of_def using vert_connected_id by blast

lemma conn_comp_of_conn_comps: "v ∈ V ⟹ connected_component_of v ∈ connected_components"
  unfolding connected_components_def quotient_def connected_component_of_def by blast

lemma Un_connected_components: "connected_components = connected_component_of ` V"
  unfolding connected_components_def connected_component_of_def quotient_def by blast

lemma connected_component_subgraph: "V' ∈ connected_components ⟹ subgraph V' (induced_edges V') V E"
  using induced_is_subgraph connected_component_wf by simp

lemma connected_components_connected2:
  assumes conn_comp: "V' ∈ connected_components"
  shows "ulgraph.is_connected_set V' (induced_edges V') V'"
proof-
  interpret subg: subgraph V' "induced_edges V'" V E using connected_component_subgraph conn_comp by simp
  interpret g': ulgraph V' "induced_edges V'" using subg.is_subgraph_ulgraph ulgraph_axioms by simp
  have "⋀u v. u ∈ V' ⟹ v ∈ V' ⟹ g'.vert_connected u v"
  proof-
    fix u v assume "u ∈ V'" "v ∈ V'"
    then obtain p where conn_path: "connecting_path u v p" using connected_component_connected conn_comp unfolding is_connected_set_def vert_connected_def by blast
    then have u_in_p: "u ∈ set p" unfolding connecting_path_def is_gen_path_def is_walk_def by force
    then have set_p: "set p ⊆ V'" using connecting_path_connected_set[OF conn_path]
        in_quotient_imp_closed[OF equiv_vert_connected] conn_comp ‹u ∈ V'›
      unfolding is_connected_set_def connected_components_def by blast
    then have "set (g'.walk_edges p) ⊆ induced_edges V'"
      using walk_edges_induced_edges induced_edges_mono conn_path unfolding connecting_path_def is_gen_path_def by blast
    then have "g'.connecting_path u v p"
      using set_p conn_path
      unfolding g'.connecting_path_def g'.connecting_path_def g'.is_gen_path_def g'.is_walk_def
      unfolding connecting_path_def connecting_path_def is_gen_path_def is_walk_def by auto
    then show "g'.vert_connected u v" unfolding g'.vert_connected_def by blast
  qed
  then show ?thesis unfolding g'.is_connected_set_def by blast
qed

lemma vert_connected_connected_component: "C ∈ connected_components ⟹ u ∈ C ⟹ vert_connected u v ⟹ v ∈ C"
  unfolding connected_components_def using equiv_vert_connected in_quotient_imp_closed by fastforce

lemma connected_components_connected_ulgraphs:
  assumes conn_comp: "V' ∈ connected_components"
  shows "connected_ulgraph V' (induced_edges V')"
proof-
  interpret subg: subgraph V' "induced_edges V'" V E using connected_component_subgraph conn_comp by simp
  interpret g': ulgraph V' "induced_edges V'" using subg.is_subgraph_ulgraph ulgraph_axioms by simp
  show ?thesis using conn_comp connected_component_non_empty connected_components_connected2 by (unfold_locales, auto)
qed

lemma connected_components_partition_on_V: "partition_on V connected_components"
  using partition_on_quotient equiv_vert_connected unfolding connected_components_def by blast

lemma Union_connected_components: "⋃connected_components = V"
  using connected_components_partition_on_V unfolding partition_on_def by blast

lemma disjoint_connected_components: "disjoint connected_components"
  using connected_components_partition_on_V unfolding partition_on_def by blast

lemma Union_induced_edges_connected_components: "⋃(induced_edges ` connected_components) = E"
proof-
  have "∃C∈connected_components. e ∈ induced_edges C" if "e ∈ E" for e
  proof-
    obtain u v where e: "e = {u,v}" by (meson ‹e ∈ E› obtain_edge_pair_adj)
    then have "vert_connected u v" using that vert_connected_neighbors by blast
    then have "v ∈ connected_component_of u" unfolding connected_component_of_def by simp
    then have "e ∈ induced_edges (connected_component_of u)" using connected_component_of_self wellformed ‹e∈E› unfolding e induced_edges_def by auto
    then show ?thesis using conn_comp_of_conn_comps e wellformed ‹e∈E› by auto
  qed 
  then show ?thesis using connected_component_wf induced_edges_ss by blast
qed

lemma connected_components_empty_E:
  assumes empty: "E = {}"
  shows "connected_components = {{v} | v. v∈V}"
proof-
  have "∀v∈V. vert_connected_rel``{v} = {v}" using vert_connected_id connected_empty_E empty by auto
  then show ?thesis unfolding connected_components_def quotient_def by auto
qed

lemma connected_iff_connected_components:
  assumes non_empty: "V ≠ {}"
    shows "is_connected_set V ⟷ connected_components = {V}"
proof
  assume "is_connected_set V"
  then have "∀v∈V. connected_component_of v = V" unfolding connected_component_of_def is_connected_set_def using vert_connected_wf by blast
  then show "connected_components = {V}" unfolding quotient_def connected_component_of_def connected_components_def using non_empty by auto
next
  show "connected_components = {V} ⟹ is_connected_set V"
    using connected_component_connected unfolding connected_components_def is_connected_set_def by auto
qed

end

lemma (in connected_ulgraph) connected_components[simp]: "connected_components = {V}"
  using connected connected_iff_connected_components not_empty by simp

lemma (in fin_ulgraph) finite_connected_components: "finite connected_components"
  unfolding connected_components_def using finV vert_connected_rel_on_V finite_quotient by blast

lemma (in fin_ulgraph) finite_connected_component: "C ∈ connected_components ⟹ finite C"
  using connected_component_wf finV finite_subset by blast

lemma (in connected_ulgraph) connected_components_remove_edges:
  assumes edge: "{u,v} ∈ E"
  shows "ulgraph.connected_components V (E - {{u,v}}) =
    {ulgraph.connected_component_of V (E - {{u,v}}) u, ulgraph.connected_component_of V (E - {{u,v}}) v}"
proof-
  interpret g': ulgraph V "E - {{u,v}}" using wellformed edge_size by (unfold_locales, auto)
  have inV: "u ∈ V" "v ∈ V" using edge wellformed by auto
  have "∀w∈V. g'.connected_component_of w = g'.connected_component_of u ∨ g'.connected_component_of w = g'.connected_component_of v"
    using vert_connected_remove_edge[OF edge] g'.equiv_vert_connected equiv_class_eq unfolding g'.connected_component_of_def by fast
  then show ?thesis unfolding g'.connected_components_def quotient_def g'.connected_component_of_def using inV by auto
qed

lemma (in ulgraph) connected_set_connected_component:
  assumes conn_set: "is_connected_set C"
    and non_empty: "C ≠ {}"
    and "⋀u v. {u,v} ∈ E ⟹ u ∈ C ⟹ v ∈ C"
  shows "C ∈ connected_components"
proof-
  have walk_subset_C: "is_walk xs ⟹  hd xs ∈ C ⟹ set xs ⊆ C" for xs
  proof (induction xs rule: rev_induct)
    case Nil
    then show ?case by auto
  next
    case (snoc x xs)
    then show ?case
    proof (cases xs rule: rev_exhaust)
      case Nil
      then show ?thesis using snoc by auto
    next
      fix ys y assume xs: "xs = ys @ [y]"
      then have "is_walk xs" using is_walk_prefix snoc(2) by blast
      then have set_xs_C: "set xs ⊆ C" using snoc xs is_walk_not_empty2 hd_append2 by metis
      have yx_E: "{y,x} ∈ E" using snoc(2) walk_edges_app unfolding xs is_walk_def by simp
      have "x ∈ C" using assms(3)[OF yx_E] set_xs_C unfolding xs by simp
      then show ?thesis using set_xs_C by simp
    qed
  qed
  obtain u where "u ∈ C" using non_empty by blast
  then have "u ∈ V" using conn_set is_connected_set_wf by blast
  have "v ∈ C" if vert_connected: "vert_connected u v" for v
  proof-
    obtain p where "connecting_path u v p" using vert_connected unfolding vert_connected_def by blast
    then show ?thesis using walk_subset_C[of p] ‹u∈C› is_walk_def last_in_set unfolding connecting_path_def is_gen_path_def by auto
  qed
  then have "connected_component_of u = C" using assms ‹u∈C› unfolding connected_component_of_def is_connected_set_def by auto
  then show ?thesis using conn_comp_of_conn_comps ‹u∈V› by blast
qed

lemma (in ulgraph) subset_conn_comps_if_Union:
  assumes A_subset_conn_comps: "A ⊆ connected_components"
    and Un_A: "⋃A = V"
  shows "A = connected_components"
proof (rule ccontr)
  assume "A ≠ connected_components"
  then obtain C where C_conn_comp: "C ∈ connected_components " "C ∉ A" using A_subset_conn_comps by blast
  then obtain v where "v ∈ C" using connected_component_non_empty by blast
  then have "v ∉ V" using A_subset_conn_comps Un_A connected_components_partition_on_V C_conn_comp
    using partition_onD4 by fastforce
  then show False using C_conn_comp connected_component_wf ‹v∈C› by auto
qed

lemma (in connected_ulgraph) exists_adj_vert_removed:
  assumes "v ∈ V"
    and remove_vertex: "remove_vertex v = (V',E')"
    and conn_component: "C ∈ ulgraph.connected_components V' E'"
  shows "∃u∈C. vert_adj v u"
proof-
  have V': "V' = V - {v}" and E': "E' = {e∈E. v ∉ e}" using remove_vertex unfolding remove_vertex_def vincident_def by auto
  interpret subg: subgraph "V - {v}" "{e∈E. v ∉ e}" V E using subgraph_remove_vertex remove_vertex V' E' by metis
  interpret g': ulgraph "V - {v}" "{e∈E. v ∉ e}" using subg.is_subgraph_ulgraph ulgraph_axioms by blast
  obtain c where "c ∈ C" using g'.connected_component_non_empty conn_component V' E' by blast
  then have "c ∈ V'" using g'.connected_component_wf conn_component V' E' by blast
  then have "c ∈ V" using subg.verts_ss V' by blast
  then obtain p where conn_path: "connecting_path v c p" using ‹v∈V› vertices_connected_path by blast  
  have "v ≠ c" using ‹c∈V'› remove_vertex unfolding remove_vertex_def by blast
  then obtain u p' where p: "p = v # u # p'" using conn_path
    by (metis connecting_path_def is_gen_path_def is_walk_def last.simps list.exhaust_sel)
  then have conn_path_uc: "connecting_path u c (u#p')" using conn_path connecting_path_tl unfolding p by blast
  have v_notin_p': "v ∉ set (u#p')" using conn_path ‹v≠c› unfolding p connecting_path_def is_gen_path_def by auto
  then have "g'.connecting_path u c (u#p')" using conn_path_uc v_notin_p' walk_edges_in_verts
    unfolding g'.connecting_path_def connecting_path_def g'.is_gen_path_def is_gen_path_def g'.is_walk_def is_walk_def
    by blast 
  then have "g'.vert_connected u c" unfolding g'.vert_connected_def by blast
  then have "u ∈ C" using ‹c∈C› conn_component g'.vert_connected_connected_component g'.vert_connected_rev unfolding V' E' by blast
  have "vert_adj v u" using conn_path unfolding p connecting_path_def is_gen_path_def is_walk_def vert_adj_def by auto
  then show ?thesis using ‹u∈C› by blast
qed

subsection ‹Trees›

locale tree = fin_connected_ulgraph +
  assumes no_cycles: "¬ is_cycle2 c"
begin

sublocale fin_connected_sgraph
  using alt_edge_size no_cycles loop_is_cycle2 card_1_singletonE connected
  by (unfold_locales, metis, simp)

end

locale spanning_tree = ulgraph V E + T: tree V T for V E T +
  assumes subgraph: "T ⊆ E"

lemma (in fin_connected_ulgraph) has_spanning_tree: "∃T. spanning_tree V E T"
  using fin_connected_ulgraph_axioms
proof (induction "card E" arbitrary: E)
  case 0
  then interpret g: fin_connected_ulgraph V edges by blast
  have edges: "edges = {}" using g.fin_edges 0 by simp
  then obtain v where V: "V = {v}" using g.V_E_empty by blast
  interpret g': fin_connected_sgraph V edges using g.connected edges by (unfold_locales, auto)
  interpret t: tree V edges using g.length_cycle_card_V g'.cycle2_min_length g.is_cycle2_def V by (unfold_locales, fastforce)
  have "spanning_tree V edges edges" by (unfold_locales, auto) 
  then show ?case by blast
next
  case (Suc m)
  then interpret g: fin_connected_ulgraph V edges by blast
  show ?case
  proof (cases "∀c. ¬g.is_cycle2 c")
    case True
    then have "spanning_tree V edges edges" by (unfold_locales, auto)
    then show ?thesis by blast
  next
    case False
    then obtain c where cycle: "g.is_cycle2 c" by blast
    then have "length c ≥ 2" unfolding g.is_cycle2_def g.is_cycle_alt walk_length_conv by auto
    then obtain u v xs where c: "c = u#v#xs" by (metis Suc_le_length_iff numeral_2_eq_2)
    then have g': "fin_connected_ulgraph V (edges - {{u,v}})" using finV g.connected_remove_cycle_edges
      by (metis connected_ulgraph_def cycle fin_connected_ulgraph_def fin_graph_system.intro fin_graph_system_axioms.intro fin_ulgraph.intro ulgraph_def)
    have "{u,v} ∈ edges" using cycle unfolding c g.is_cycle2_def g.is_cycle_alt g.is_walk_def by auto
    then obtain T where "spanning_tree V (edges - {{u,v}}) T" using Suc card_Diff_singleton g' by fastforce
    then have "spanning_tree V edges T" unfolding spanning_tree_def spanning_tree_axioms_def using g.ulgraph_axioms by blast
    then show ?thesis by blast
  qed
qed

context tree
begin

definition leaf :: "'a ⇒ bool" where
  "leaf v ⟷ degree v = 1"

definition leaves :: "'a set" where
  "leaves = {v. leaf v}"

definition non_trivial :: "bool" where
  "non_trivial ⟷ card V ≥ 2"

lemma obtain_2_verts:
  assumes "non_trivial"
  obtains u v where "u ∈ V" "v ∈ V" "u ≠ v"
  using assms unfolding non_trivial_def
  by (meson diameter_obtains_path_vertices)

lemma leaf_in_V: "leaf v ⟹ v ∈ V"
  unfolding leaf_def using degree_none by force

lemma exists_leaf:
  assumes "non_trivial"
  shows "∃v∈V. leaf v"
proof-
  obtain p where is_path: "is_path p" and longest_path: "∀s. is_path s ⟶ length s ≤ length p"
    using obtain_longest_path 
    by (metis One_nat_def assms connected connected_sgraph_axioms connected_sgraph_def degree_0_not_connected
        is_connected_setD is_edge_or_loop is_isolated_vertex_def is_isolated_vertex_degree0 is_loop_def
        n_not_Suc_n numeral_2_eq_2 obtain_2_verts sgraph.two_edges vert_adj_def)
  then obtain l v xs where p: "p = l#v#xs"
    by (metis is_open_walk_def is_path_def is_walk_not_empty2 last_ConsL list.exhaust_sel)
  then have lv_incident: "{l,v} ∈ incident_edges l" using is_path
    unfolding incident_edges_def vincident_def is_path_def is_open_walk_def is_walk_def by simp
  have "⋀e. e∈E ⟹ e ≠ {l,v} ⟹ e ∉ incident_edges l"
  proof
    fix e
    assume e_in_E: "e ∈ E"
      and not_lv: "e ≠ {l,v}"
      and incident: "e ∈ incident_edges l"
    obtain u where e: "e = {l,u}" using e_in_E obtain_edge_pair_adj incident
      unfolding incident_edges_def vincident_def by auto
    then have "u ≠ l" using e_in_E edge_vertices_not_equal by blast
    have "u ≠ v" using e not_lv by auto
    have u_in_V: "u ∈ V" using e_in_E e wellformed by blast
    then show False
    proof (cases "u ∈ set p")
      case True
      then have "u ∈ set xs" using ‹u≠l› ‹u≠v› p by simp
      then obtain ys zs where "xs = ys@u#zs" by (meson split_list)
      then have "is_cycle2 (u#l#v#ys@[u])"
        using is_path ‹u≠l› ‹u≠v› e_in_E distinct_edgesI walk_edges_append_ss2 walk_edges_in_verts
        unfolding is_cycle2_def is_cycle_def p is_path_def is_closed_walk_def is_open_walk_def is_walk_def e walk_length_conv
        by (auto, metis insert_commute, fastforce+)
      then show ?thesis using no_cycles by blast
    next
      case False
      then have "is_path (u#p)" using is_path u_in_V e_in_E
        unfolding is_path_def is_open_walk_def is_walk_def e p by (auto, (metis insert_commute)+)
      then show False using longest_path by auto
    qed
  qed
  then have "incident_edges l = {{l,v}}" using lv_incident unfolding incident_edges_def by blast
  then have leaf: "leaf l" unfolding leaf_def alt_degree_def by simp
  then show ?thesis using leaf_in_V by blast
qed

lemma tree_remove_leaf:
  assumes leaf: "leaf l"
    and remove_vertex: "remove_vertex l = (V',E')"
  shows "tree V' E'"
proof-
  interpret g': ulgraph V' E' using remove_vertex wellformed edge_size unfolding remove_vertex_def vincident_def
    by (unfold_locales, auto)
  interpret subg: ulsubgraph V' E' V E using subgraph_remove_vertex ulgraph_axioms remove_vertex
    unfolding ulsubgraph_def by blast
  have V': "V' = V - {l}" using remove_vertex unfolding remove_vertex_def by blast
  have E': "E' = {e∈E. l ∉ e}" using remove_vertex unfolding remove_vertex_def vincident_def by blast
  have "∃v∈V. v ≠ l" using leaf unfolding leaf_def
    by (metis One_nat_def is_independent_alt is_isolated_vertex_def is_isolated_vertex_degree0
        n_not_Suc_n radius_obtains singletonI singleton_independent_set)
  then have "V' ≠ {}" using remove_vertex unfolding remove_vertex_def vincident_def by blast
  then have "g'.is_connected_set V'" using connected_remove_leaf leaf remove_vertex unfolding leaf_def by blast
  then show ?thesis using ‹V'≠{}› finV subg.is_cycle2 V' E' no_cycles by (unfold_locales, auto)
qed

end

lemma tree_induct [case_names singolton insert, induct set: tree]:
  assumes tree: "tree V E"
    and trivial: "⋀v. tree {v} {} ⟹ P {v} {}"
    and insert: "⋀l v V E. tree V E ⟹ P V E ⟹ l ∉ V ⟹ v ∈ V ⟹ {l,v} ∉ E ⟹ tree.leaf (insert {l,v} E) l ⟹ P (insert l V) (insert {l,v} E)"
  shows "P V E"
  using tree
proof (induction "card V" arbitrary: V E)
  case 0
  then interpret tree V E by simp
  have "V = {}" using finV 0(1) by simp
  then show ?case using not_empty by blast
next
  case (Suc n)
  then interpret t: tree V E by simp
  show ?case
  proof (cases "card V = 1")
    case True
    then obtain v where V: "V = {v}" using card_1_singletonE by blast
    then have "E = {}"
      using True subset_antisym t.edge_incident_vert t.vincident_def t.singleton_not_edge t.wellformed
      by fastforce
    then show ?thesis using trivial t.tree_axioms V by simp
  next
    case False
    then have card_V: "card V ≥ 2" using Suc by simp
    then obtain l where leaf: "t.leaf l" using t.exists_leaf t.non_trivial_def by blast
    then obtain e where inc_edges: "t.incident_edges l = {e}"
      unfolding t.leaf_def t.alt_degree_def using card_1_singletonE by blast
    then have e_in_E: "e ∈ E" unfolding t.incident_edges_def by blast
    then obtain u where e: "e = {l,u}" using t.two_edges card_2_iff inc_edges unfolding t.incident_edges_def t.vincident_def
      by (metis (no_types, lifting) empty_iff insert_commute insert_iff mem_Collect_eq)
    then have "l ≠ u" using e_in_E t.edge_vertices_not_equal by blast
    have "u ∈ V" using e e_in_E t.wellformed by blast
    let ?V' = "V - {l}"
    let ?E' = "E - {{l,u}}"
    have remove_vertex: "t.remove_vertex l = (?V', ?E')"
      using inc_edges e unfolding t.remove_vertex_def t.incident_edges_def by blast
    then have t': "tree ?V' ?E'" using t.tree_remove_leaf leaf by blast
    have "l ∈ V" using leaf t.leaf_in_V by blast
    then have P': "P ?V' ?E'" using Suc t' by auto
    show ?thesis using insert[OF t' P'] Suc leaf ‹u∈V› ‹l≠u› ‹l ∈ V› e e_in_E by (auto, metis insert_Diff)
  qed
qed

context tree
begin

lemma card_V_card_E: "card V = Suc (card E)"
  using tree_axioms
proof (induction V E)
  case (singolton v)
  then show ?case by auto
next
  case (insert l v V' E')
  then interpret t': tree V' E' by simp
  show ?case using t'.finV t'.fin_edges insert by simp
qed

end

lemma card_E_treeI:
  assumes fin_conn_sgraph: "fin_connected_ulgraph V E"
    and card_V_E: "card V = Suc (card E)"
  shows "tree V E"
proof-
  interpret G: fin_connected_ulgraph V E using fin_conn_sgraph .
  obtain T where T: "spanning_tree V E T" using G.has_spanning_tree by blast
  show ?thesis
  proof (cases "E = T")
    case True
    then show ?thesis using T unfolding spanning_tree_def by blast
  next
    case False
    then have "card E > card T" using T G.fin_edges unfolding spanning_tree_def spanning_tree_axioms_def
      by (simp add: psubsetI psubset_card_mono)
    then show ?thesis using tree.card_V_card_E T card_V_E unfolding spanning_tree_def by fastforce
  qed
qed

context tree
begin

lemma add_vertex_tree:
  assumes "v ∉ V"
    and  "w ∈ V"
  shows "tree (insert v V) (insert {v,w} E)"
proof -
  let ?V' = "insert v V" and ?E' = "insert {v,w} E"

  have cardV: "card {v,w} = 2" using card_2_iff assms by auto
  then interpret t': ulgraph ?V' ?E'
    using wellformed assms two_edges by (unfold_locales, auto)

  interpret subg: ulsubgraph V E ?V' ?E' by (unfold_locales, auto)

  have connected: "t'.is_connected_set ?V'"
    unfolding t'.is_connected_set_def
    using subg.vert_connected t'.vert_connected_neighbors t'.vert_connected_trans
      t'.vert_connected_id vertices_connected t'.ulgraph_axioms ulgraph_axioms assms t'.vert_connected_rev
    by simp metis

  then have fin_connected_ulgraph: "fin_connected_ulgraph ?V' ?E'" using finV by (unfold_locales, auto)

  from assms have "{v,w} ∉ E" using wellformed_alt_fst by auto
  then have "card ?E' = Suc (card E)" using fin_edges card_insert_if by auto
  then have "card ?V' = Suc (card ?E')" using card_V_card_E assms wellformed_alt_fst finV card_insert_if by auto

  then show ?thesis using card_E_treeI fin_connected_ulgraph by auto
qed

lemma tree_connected_set:
  assumes non_empty: "V' ≠ {}"
    and subg: "V' ⊆ V"
    and connected_V': "ulgraph.is_connected_set V' (induced_edges V') V'"
  shows "tree V' (induced_edges V')"
proof-
  interpret subg: subgraph V' "induced_edges V'" V E using induced_is_subgraph subg by simp
  interpret g': ulgraph V' "induced_edges V'" using subg.is_subgraph_ulgraph ulgraph_axioms by blast
  interpret subg: ulsubgraph V' "induced_edges V'" V E by unfold_locales
  show ?thesis using connected_V' subg.is_cycle2 no_cycles finV subg non_empty rev_finite_subset by (unfold_locales) (auto, blast)
qed

lemma unique_adj_vert_removed:
  assumes "v ∈ V"
    and remove_vertex: "remove_vertex v = (V',E')"
    and conn_component: "C ∈ ulgraph.connected_components V' E'"
  shows "∃!u∈C. vert_adj v u"
proof-
  interpret subg: ulsubgraph V' E' V E using remove_vertex subgraph_remove_vertex ulgraph_axioms ulsubgraph.intro by metis
  interpret g': ulgraph V' E' using subg.is_subgraph_ulgraph ulgraph_axioms by simp
  obtain u where "u ∈ C" and adj_vu: "vert_adj v u" using exists_adj_vert_removed using assms by blast
  have "w = u" if "w ∈ C" and adj_vw: "vert_adj v w" for w
  proof (rule ccontr)
    assume "w ≠ u"
    obtain p where g'_conn_path: "g'.connecting_path w u p" using ‹u∈C› ‹w∈C› conn_component
        g'.connected_component_connected g'.is_connected_setD g'.vert_connected_def by blast
    then have v_notin_p: "v ∉ set p" using remove_vertex unfolding g'.connecting_path_def g'.is_gen_path_def g'.is_walk_def remove_vertex_def by blast
    have conn_path: "connecting_path w u p" using g'_conn_path subg.connecting_path by simp
    then obtain p' where p: "p = w # p' @ [u]" unfolding connecting_path_def using ‹w≠u›
      by (metis hd_Cons_tl last.simps last_rev rev_is_Nil_conv snoc_eq_iff_butlast)
    then have "walk_edges (v#p@[v]) = {v,w} # walk_edges ((w # p') @ [u,v])" by simp
    also have "… = {v,w} # walk_edges p @ [{u,v}]" unfolding p using walk_edges_app by (metis Cons_eq_appendI)
    finally have walk_edges: "walk_edges (v#p@[v]) = {v,w} # walk_edges p @ [{v,u}]" by (simp add: insert_commute)
    then have "is_cycle (v#p@[v])" using conn_path adj_vu adj_vw ‹w≠u› ‹v∈V› g'.walk_length_conv singleton_not_edge v_notin_p
      unfolding connecting_path_def is_cycle_def is_gen_path_def is_closed_walk_def is_walk_def p vert_adj_def by auto
    then have "is_cycle2 (v#p@[v])" using ‹w≠u› v_notin_p walk_edges_in_verts unfolding is_cycle2_def walk_edges
      by (auto simp: doubleton_eq_iff is_cycle_alt distinct_edgesI)
    then show False using no_cycles by blast
  qed
  then show ?thesis using ‹u∈C› adj_vu by blast
qed

lemma non_trivial_card_E: "non_trivial ⟹ card E ≥ 1"
  using card_V_card_E unfolding non_trivial_def by simp

lemma V_Union_E: "non_trivial ⟹ V = ⋃E"
  using tree_axioms
proof (induction V E)
  case (singolton v) 
  then interpret t: tree "{v}" "{}" by simp
  show ?case using singolton unfolding t.non_trivial_def by simp
next
  case (insert l v V' E')
  then interpret t: tree V' E' by simp
  show ?case
  proof (cases "card V' = 1")
    case True
    then have V: "V' = {v}" using insert(3) card_1_singletonE by blast
    then have E: "E' = {}" using t.fin_edges t.card_V_card_E by fastforce
    then show ?thesis unfolding E V by simp
  next
    case False
    then have "t.non_trivial" using t.card_V_card_E unfolding t.non_trivial_def by simp
    then show ?thesis using insert by blast
  qed
qed

end

lemma singleton_tree: "tree {v} {}"
proof-
  interpret g: fin_ulgraph "{v}" "{}" by (unfold_locales, auto)
  show ?thesis using g.is_walk_def g.walk_length_def by (unfold_locales, auto simp: g.is_connected_set_singleton g.is_cycle2_def g.is_cycle_alt)
qed

lemma tree2:
  assumes "u ≠ v"
    shows "tree {u,v} {{u,v}}"
proof-
  interpret ulgraph "{u,v}" "{{u,v}}" using ‹u≠v› by unfold_locales auto
  have "fin_connected_ulgraph {u,v} {{u,v}}" by unfold_locales
    (auto simp: is_connected_set_def vert_connected_id vert_connected_neighbors vert_connected_rev)
  then show ?thesis using card_E_treeI ‹u≠v› by fastforce
qed

subsection ‹Graph Isomorphism›

locale graph_isomorphism =
  G: graph_system V⇩G E⇩G for V⇩G E⇩G +
  fixes V⇩H E⇩H f
  assumes bij_f: "bij_betw f V⇩G V⇩H"
  and edge_preserving: "((`) f) ` E⇩G = E⇩H"
begin

lemma inj_f: "inj_on f V⇩G"
  using bij_f unfolding bij_betw_def by blast

lemma V⇩H_def: "V⇩H = f ` V⇩G"
  using bij_f unfolding bij_betw_def by blast

definition "inv_iso ≡ the_inv_into V⇩G f"

lemma graph_system_H: "graph_system V⇩H E⇩H"
  using G.wellformed edge_preserving bij_f bij_betw_imp_surj_on by unfold_locales blast

interpretation H: graph_system V⇩H E⇩H using graph_system_H .

lemma graph_isomorphism_inv: "graph_isomorphism V⇩H E⇩H V⇩G E⇩G inv_iso"
proof (unfold_locales)
  show "bij_betw inv_iso V⇩H V⇩G" unfolding inv_iso_def using bij_betw_the_inv_into bij_f by blast
next
  have "∀v∈V⇩G. the_inv_into V⇩G f (f v) = v" using bij_f by (simp add: bij_betw_imp_inj_on the_inv_into_f_f)
  then have "∀e∈E⇩G. (λv. the_inv_into V⇩G f (f v)) ` e = e" using G.wellformed
    by (simp add: subset_iff)
  then show "((`) inv_iso)` E⇩H = E⇩G" unfolding inv_iso_def by (simp add: edge_preserving[symmetric] image_comp)
qed

interpretation inv_iso: graph_isomorphism V⇩H E⇩H V⇩G E⇩G inv_iso using graph_isomorphism_inv .

end

fun graph_isomorph :: "'a pregraph ⇒ 'b pregraph ⇒ bool" (infix ‹≃› 50) where
  "(V⇩G,E⇩G) ≃ (V⇩H,E⇩H) ⟷ (∃f. graph_isomorphism V⇩G E⇩G V⇩H E⇩H f)"

lemma (in graph_system) graph_isomorphism_id: "graph_isomorphism V E V E id"
  by unfold_locales auto

lemma (in graph_system) graph_isomorph_refl: "(V,E) ≃ (V,E)"
  using graph_isomorphism_id by auto

lemma graph_isomorph_sym: "symp (≃)"
  using graph_isomorphism.graph_isomorphism_inv unfolding symp_def by fastforce

lemma graph_isomorphism_trans: "graph_isomorphism V⇩G E⇩G V⇩H E⇩H f ⟹ graph_isomorphism V⇩H E⇩H V⇩F E⇩F g ⟹ graph_isomorphism V⇩G E⇩G V⇩F E⇩F (g o f)"
  unfolding graph_isomorphism_def graph_isomorphism_axioms_def using bij_betw_trans by (auto, blast)

lemma graph_isomorph_trans: "transp (≃)"
  using graph_isomorphism_trans unfolding transp_def by fastforce

end