:: Trees: Connected, Acyclic Graphs
::  by Gilbert Lee
::
:: Received February 22, 2005
:: Copyright (c) 2005-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, FINSET_1, ARYTM_3, CARD_1, SUBSET_1, XBOOLE_0, GLIB_000,
      RELAT_2, GLIB_001, TREES_1, ZFMISC_1, FUNCT_1, FINSEQ_1, GRAPH_1, ABIAN,
      XXREAL_0, RELAT_1, RCOMP_1, FUNCOP_1, ARYTM_1, WAYBEL_0, TARSKI, PBOOLE,
      SETFAM_1, ORDINAL1, NAT_1, GLIB_002, XCMPLX_0;
 notations TARSKI, XBOOLE_0, CARD_1, ORDINAL1, NUMBERS, SUBSET_1, SETFAM_1,
      DOMAIN_1, XCMPLX_0, ABIAN, XXREAL_0, RELAT_1, FUNCT_1, PBOOLE, FUNCT_2,
      FINSEQ_1, NAT_1, FUNCOP_1, GLIB_000, GLIB_001;
 constructors DOMAIN_1, CARD_FIL, GLIB_001, VALUED_1, XXREAL_2, WELLORD2,
      RELSET_1;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
      FINSET_1, XREAL_0, INT_1, CARD_1, GLIB_000, ABIAN, GLIB_001, FUNCT_2,
      PARTFUN1;
 requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;


begin :: Definitions

definition
  let G be _Graph;
  attr G is connected means
:: GLIB_002:def 1

  for u,v being Vertex of G holds ex W being Walk of G st W is_Walk_from u,v;
end;

definition
  let G be _Graph;
  attr G is acyclic means
:: GLIB_002:def 2

  not ex W being Walk of G st W is Cycle-like;
end;

definition
  let G be _Graph;
  attr G is Tree-like means
:: GLIB_002:def 3

  G is acyclic & G is connected;
end;

registration
  cluster _trivial -> connected for _Graph;
end;

registration
  cluster _trivial loopless -> Tree-like for _Graph;
end;

registration
  cluster acyclic -> simple for _Graph;
end;

registration
  cluster Tree-like -> acyclic connected for _Graph;
end;

registration
  cluster acyclic connected -> Tree-like for _Graph;
end;

registration
  let G be _Graph, v be Vertex of G;
  cluster -> Tree-like for inducedSubgraph of G,{v},{};
end;

definition
  let G be _Graph, v be set;
  pred G is_DTree_rooted_at v means
:: GLIB_002:def 4

  G is Tree-like & for x being Vertex
  of G holds ex W being DWalk of G st W is_Walk_from v,x;
end;

registration
  cluster _trivial _finite Tree-like for _Graph;
  cluster non _trivial _finite Tree-like for _Graph;
end;

registration
  let G be _Graph;
  cluster _trivial _finite Tree-like for Subgraph of G;
end;

registration
  let G be acyclic _Graph;
  cluster -> acyclic for Subgraph of G;
end;

definition
  let G be _Graph, v be Vertex of G;
  func G.reachableFrom(v) -> non empty Subset of the_Vertices_of G means
:: GLIB_002:def 5

  for x being object
   holds x in it iff ex W being Walk of G st W is_Walk_from v,x;
end;

definition
  let G be _Graph, v be Vertex of G;
  func G.reachableDFrom(v) -> non empty Subset of the_Vertices_of G means
:: GLIB_002:def 6
 for x being object
 holds x in it iff ex W being DWalk of G st W is_Walk_from v,x;
end;

definition
  let G1 be _Graph, G2 be Subgraph of G1;
  attr G2 is Component-like means
:: GLIB_002:def 7

  G2 is connected & not ex G3 being connected Subgraph of G1 st G2 c< G3;
end;

registration
  let G be _Graph;
  cluster Component-like -> connected for Subgraph of G;
end;

registration
  let G be _Graph, v be Vertex of G;
  cluster -> Component-like for inducedSubgraph of G,G.reachableFrom(v);
end;

registration
  let G be _Graph;
  cluster Component-like for Subgraph of G;
end;

definition
  let G be _Graph;
  mode Component of G is Component-like Subgraph of G;
end;

definition
  let G be _Graph;
  func G.componentSet() -> non empty Subset-Family of the_Vertices_of G means
:: GLIB_002:def 8

  for x being set holds x in it iff ex v being Vertex of G st x = G
  .reachableFrom(v);
end;

registration
  let G be _Graph, X be Element of G.componentSet();
  cluster -> Component-like for inducedSubgraph of G,X;
end;

definition
  let G be _Graph;
  func G.numComponents() -> Cardinal equals
:: GLIB_002:def 9
  card G.componentSet();
end;

definition
  let G be _finite _Graph;
  redefine func G.numComponents() -> non zero Element of NAT;
end;

definition
  let G be _Graph, v be Vertex of G;
  attr v is cut-vertex means
:: GLIB_002:def 10

  for G2 being removeVertex of G,v holds
    G.numComponents() in G2.numComponents();
end;

definition
  let G be _finite _Graph, v be Vertex of G;
  redefine attr v is cut-vertex means
:: GLIB_002:def 11

  for G2 being removeVertex of G,v
  holds G.numComponents() < G2.numComponents();
end;

registration
  let G be non _trivial _finite connected _Graph;
  cluster non cut-vertex for Vertex of G;
end;

registration
  let G be non _trivial _finite Tree-like _Graph;
  cluster endvertex for Vertex of G;
end;

registration
  let G be non _trivial _finite Tree-like _Graph, v be endvertex Vertex of G;
  cluster -> Tree-like for removeVertex of G,v;
end;

definition
  let GF be Graph-yielding Function;
  attr GF is connected means
:: GLIB_002:def 12
  for x being object st x in dom GF
    ex G being _Graph st GF.x = G & G is connected;
  attr GF is acyclic means
:: GLIB_002:def 13
  for x being object st x in dom GF
    ex G being _Graph st GF.x = G & G is acyclic;
  attr GF is Tree-like means
:: GLIB_002:def 14
  for x being object st x in dom GF
    ex G being _Graph st GF.x = G & G is Tree-like;
end;

definition
  let GF be non empty Graph-yielding Function;
  redefine attr GF is connected means
:: GLIB_002:def 15

  for x being Element of dom GF holds GF.x is connected;
  redefine attr GF is acyclic means
:: GLIB_002:def 16

  for x being Element of dom GF holds GF.x is acyclic;
  redefine attr GF is Tree-like means
:: GLIB_002:def 17
  for x being Element of dom GF holds GF.x is Tree-like;
end;

definition
  let GSq be GraphSeq;
  redefine attr GSq is connected means
:: GLIB_002:def 18

  for n being Nat holds GSq.n is connected;
  redefine attr GSq is acyclic means
:: GLIB_002:def 19

  for n being Nat holds GSq.n is acyclic;
  redefine attr GSq is Tree-like means
:: GLIB_002:def 20

  for n being Nat holds GSq.n is Tree-like;
end;

registration
  cluster connected acyclic Tree-like non empty for Graph-yielding Function;
end;

registration
  cluster _trivial -> connected for Graph-yielding Function;
  cluster _trivial loopless -> Tree-like for Graph-yielding Function;
  cluster acyclic -> simple for Graph-yielding Function;
  cluster Tree-like -> acyclic connected for Graph-yielding Function;
  cluster acyclic connected -> Tree-like for Graph-yielding Function;
end;

registration
  cluster halting _finite Tree-like for GraphSeq;
end;

registration
  let GF be connected non empty Graph-yielding Function;
  let x be Element of dom GF;
  cluster GF.x -> connected for _Graph;
end;

registration
  let GF be acyclic non empty Graph-yielding Function;
  let x be Element of dom GF;
  cluster GF.x -> acyclic for _Graph;
end;

registration
  let GF be Tree-like non empty Graph-yielding Function;
  let x be Element of dom GF;
  cluster GF.x -> Tree-like for _Graph;
end;

registration
  let GSq be connected GraphSeq, n be Nat;
  cluster GSq.n -> connected for _Graph;
end;

registration
  let GSq be acyclic GraphSeq, n be Nat;
  cluster GSq.n -> acyclic for _Graph;
end;

registration
  let GSq be Tree-like GraphSeq, n be Nat;
  cluster GSq.n -> Tree-likefor _Graph;
end;

begin :: Theorems

reserve G,G1,G2 for _Graph;
reserve e,x,y for set;
reserve v,v1,v2 for Vertex of G;
reserve W for Walk of G;

::$CT

theorem :: GLIB_002:2
  for G being non _trivial connected _Graph, v being Vertex of G
  holds not v is isolated;

theorem :: GLIB_002:3
  for G1 being non _trivial _Graph, v being Vertex of G1, G2 being
removeVertex of G1,v st G2 is connected & ex e being set st e in v.edgesInOut()
  & not e Joins v,v,G1 holds G1 is connected;

theorem :: GLIB_002:4
  for G1 being non _trivial connected _Graph, v being Vertex of G1, G2
  being removeVertex of G1,v st v is endvertex holds G2 is connected;

theorem :: GLIB_002:5
  for G1 being connected _Graph, W being Walk of G1, e being set,
  G2 being removeEdge of G1,e st W is Cycle-like & e in W.edges() holds G2 is
  connected;

theorem :: GLIB_002:6
  (ex v1 being Vertex of G st for v2 being Vertex of G ex W being Walk
  of G st W is_Walk_from v1,v2) implies G is connected;

theorem :: GLIB_002:7
  for G being _trivial _Graph holds G is connected;

theorem :: GLIB_002:8
  G1 == G2 & G1 is connected implies G2 is connected;

theorem :: GLIB_002:9
  v in G.reachableFrom(v);

theorem :: GLIB_002:10
 for e,x,y being object holds
  x in G.reachableFrom(v1) & e Joins x,y,G implies y in G.reachableFrom(
  v1);

theorem :: GLIB_002:11
  G.edgesBetween(G.reachableFrom(v)) = G.edgesInOut(G.reachableFrom(v));

theorem :: GLIB_002:12
  v1 in G.reachableFrom(v2) implies G.reachableFrom(v1) = G
  .reachableFrom(v2);

theorem :: GLIB_002:13
  v in W.vertices() implies W.vertices() c= G.reachableFrom(v);

theorem :: GLIB_002:14
  for G1 being _Graph, G2 being Subgraph of G1, v1 being Vertex of G1,
v2 being Vertex of G2 st v1 = v2 holds G2.reachableFrom(v2) c= G1.reachableFrom
  (v1);

theorem :: GLIB_002:15
  (ex v being Vertex of G st G.reachableFrom(v) = the_Vertices_of G)
  implies G is connected;

theorem :: GLIB_002:16
  G is connected implies for v being Vertex of G holds G.reachableFrom(v
  ) = the_Vertices_of G;

theorem :: GLIB_002:17
  for v1 being Vertex of G1, v2 being Vertex of G2 st G1 == G2 & v1 = v2
  holds G1.reachableFrom(v1) = G2.reachableFrom(v2);

theorem :: GLIB_002:18
  v in G.reachableDFrom(v);

theorem :: GLIB_002:19
  x in G.reachableDFrom(v1) & e DJoins x,y,G implies y in G .reachableDFrom(v1)
;

theorem :: GLIB_002:20
  G.reachableDFrom(v) c= G.reachableFrom(v);

theorem :: GLIB_002:21
  for G1 being _Graph, G2 being Subgraph of G1, v1 being Vertex of G1,
  v2 being Vertex of G2 st v1 = v2 holds G2.reachableDFrom(v2) c= G1
  .reachableDFrom(v1);

theorem :: GLIB_002:22
  for v1 being Vertex of G1, v2 being Vertex of G2 st G1 == G2 & v1 = v2
  holds G1.reachableDFrom(v1) = G2.reachableDFrom(v2);

theorem :: GLIB_002:23
  for G1 being _Graph, G2 being connected Subgraph of G1 holds G2 is
  spanning implies G1 is connected;

theorem :: GLIB_002:24
  union G.componentSet() = the_Vertices_of G;

theorem :: GLIB_002:25
  G is connected iff G.componentSet() = {the_Vertices_of G};

theorem :: GLIB_002:26
  G1 == G2 implies G1.componentSet() = G2.componentSet();

theorem :: GLIB_002:27
  x in G.componentSet() implies x is non empty Subset of the_Vertices_of
  G;

theorem :: GLIB_002:28
  G is connected iff G.numComponents() = 1;

theorem :: GLIB_002:29
  G1 == G2 implies G1.numComponents() = G2.numComponents();

theorem :: GLIB_002:30
  G is Component of G iff G is connected;

theorem :: GLIB_002:31
  for C being Component of G holds the_Edges_of C = G.edgesBetween(
  the_Vertices_of C);

theorem :: GLIB_002:32
  for C1,C2 being Component of G holds the_Vertices_of C1 =
  the_Vertices_of C2 iff C1 == C2;

theorem :: GLIB_002:33
  for C being Component of G, v being Vertex of G holds v in
  the_Vertices_of C iff the_Vertices_of C = G.reachableFrom(v);

theorem :: GLIB_002:34
  for C1,C2 being Component of G, v being set st v in the_Vertices_of C1
  & v in the_Vertices_of C2 holds C1 == C2;

theorem :: GLIB_002:35
  for G being connected _Graph, v being Vertex of G holds v is non
  cut-vertex iff for G2 being removeVertex of G,v holds G2.numComponents() c= G
  .numComponents();

theorem :: GLIB_002:36
  for G being connected _Graph, v being Vertex of G, G2 being
  removeVertex of G,v st not v is cut-vertex holds G2 is connected;

theorem :: GLIB_002:37
  for G being non _trivial _finite connected _Graph holds ex v1,v2 being
Vertex of G st v1 <> v2 & not v1 is cut-vertex & not v2 is cut-vertex;

theorem :: GLIB_002:38
  v is cut-vertex implies G is non _trivial;

theorem :: GLIB_002:39
  for v1 being Vertex of G1, v2 being Vertex of G2 st G1 == G2 & v1 = v2
  holds v1 is cut-vertex implies v2 is cut-vertex;

theorem :: GLIB_002:40
  for G being _finite connected _Graph holds G.order() <= G.size() + 1;

theorem :: GLIB_002:41
  for G being acyclic _Graph holds G is simple;

theorem :: GLIB_002:42
  for G being acyclic _Graph, W being Path of G, e being set st not e in
W.edges() & e in W.last().edgesInOut() holds W.addEdge(e) is Path-like;

theorem :: GLIB_002:43
  for G being non _trivial _finite acyclic _Graph st the_Edges_of G <> {}
  holds ex v1,v2 being Vertex of G st v1 <> v2 & v1 is endvertex & v2 is
  endvertex & v2 in G.reachableFrom(v1);

theorem :: GLIB_002:44
  G1 == G2 & G1 is acyclic implies G2 is acyclic;

theorem :: GLIB_002:45
  for G being non _trivial _finite Tree-like _Graph holds ex v1,v2 being
  Vertex of G st v1 <> v2 & v1 is endvertex & v2 is endvertex;

theorem :: GLIB_002:46
  for G being _finite _Graph holds G is Tree-like iff G is acyclic
  & G.order() = G.size() + 1;

theorem :: GLIB_002:47
  for G being _finite _Graph holds G is Tree-like iff G is connected & G
  .order() = G.size() + 1;

theorem :: GLIB_002:48
  G1 == G2 & G1 is Tree-like implies G2 is Tree-like;

theorem :: GLIB_002:49
  G is_DTree_rooted_at x implies x is Vertex of G;

theorem :: GLIB_002:50
  G1 == G2 & G1 is_DTree_rooted_at x implies G2 is_DTree_rooted_at x;