:: Trees: Connected, Acyclic Graphs
:: by Gilbert Lee
::
:: Received February 22, 2005
:: Copyright (c) 2005-2017 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 GSq be GraphSeq;
attr GSq is connected means
:: GLIB_002:def 12
for n being Nat holds GSq.n is connected;
attr GSq is acyclic means
:: GLIB_002:def 13
for n being Nat holds GSq.n is acyclic;
attr GSq is Tree-like means
:: GLIB_002:def 14
for n being Nat holds GSq.n is Tree-like;
end;
registration
cluster trivial -> connected for GraphSeq;
cluster trivial loopless -> Tree-like for GraphSeq;
cluster acyclic -> simple for GraphSeq;
cluster Tree-like -> acyclic connected for GraphSeq;
cluster acyclic connected -> Tree-like for GraphSeq;
end;
registration
cluster halting finite Tree-like for GraphSeq;
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;