:: Graphs
:: by Krzysztof Hryniewiecki
::
:: Received December 5, 1990
:: Copyright (c) 1990-2016 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, SUBSET_1, STRUCT_0, FUNCT_1, GLIB_000, XBOOLE_0,
FUNCT_5, RELAT_1, PARTFUN1, RELAT_2, FINSET_1, TREES_2, FINSEQ_1,
XXREAL_0, ARYTM_3, TARSKI, CARD_1, FUNCT_2, ZFMISC_1, GRAPH_1, RECDEF_2,
NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
FUNCT_2, FUNCT_5, FINSEQ_1, FINSET_1, PARTFUN1, CARD_1, ORDINAL1,
NUMBERS, XCMPLX_0, NAT_1, XTUPLE_0, MCART_1, XXREAL_0, STRUCT_0;
constructors PARTFUN1, FUNCT_2, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0,
FUNCT_5, RELSET_1, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FINSET_1,
XREAL_0, FINSEQ_1, ORDINAL1, STRUCT_0, CARD_1, FUNCT_2, RELSET_1, NAT_1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
begin
reserve x, y, z, v for set,
n, m, k for Nat;
definition
struct(2-sorted) MultiGraphStruct (# carrier, carrier' -> set,
Source, Target -> Function of the carrier', the carrier #);
end;
definition
let G be MultiGraphStruct;
mode Vertex of G is Element of G;
mode Edge of G is Element of the carrier' of G;
end;
registration
cluster strict non empty non void for MultiGraphStruct;
end;
definition
mode Graph is non empty MultiGraphStruct;
end;
reserve G, G1, G2, G3 for Graph;
:: from CAT_1, 2008.07.02, A.T.
definition
let C be MultiGraphStruct, f be Edge of C;
func dom f -> Vertex of C equals
:: GRAPH_1:def 1
(the Source of C).f if C is non void non empty
otherwise the Vertex of C;
func cod f -> Vertex of C equals
:: GRAPH_1:def 2
(the Target of C).f if C is non void non empty
otherwise the Vertex of C;
end;
definition
let C be non void non empty MultiGraphStruct, f be Edge of C;
redefine func dom f -> Vertex of C equals
:: GRAPH_1:def 3
(the Source of C).f;
redefine func cod f -> Vertex of C equals
:: GRAPH_1:def 4
(the Target of C).f;
end;
definition
let G1, G2;
assume that
(the Source of G1) tolerates (the Source of G2) and
(the Target of G1) tolerates (the Target of G2);
func G1 \/ G2 -> strict Graph means
:: GRAPH_1:def 5
the carrier of it = (the carrier of G1) \/ (the carrier of G2) &
the carrier' of it = (the carrier' of G1) \/ (the carrier' of G2) &
(for v st v in the carrier' of G1 holds
(the Source of it).v = (the Source of G1).v &
(the Target of it).v = (the Target of G1).v) &
for v st v in the carrier' of G2 holds
(the Source of it).v = (the Source of G2).v &
(the Target of it).v = (the Target of G2).v;
end;
definition
let G, G1, G2 be Graph;
pred G is_sum_of G1, G2 means
:: GRAPH_1:def 6
(the Target of G1) tolerates (the Target of G2) &
(the Source of G1) tolerates (the Source of G2) &
the MultiGraphStruct of G = G1 \/ G2;
end;
definition
let IT be Graph;
attr IT is oriented means
:: GRAPH_1:def 7
for x,y st x in the carrier' of IT & y in the carrier' of IT &
(the Source of IT).x = (the Source of IT).y &
(the Target of IT).x = (the Target of IT).y holds x = y;
attr IT is non-multi means
:: GRAPH_1:def 8
for x,y st x in the carrier' of IT & y in the carrier' of IT &
( (the Source of IT).x = (the Source of IT).y &
(the Target of IT).x = (the Target of IT).y or
(the Source of IT).x = (the Target of IT).y &
(the Source of IT).y = (the Target of IT).x ) holds x = y;
attr IT is simple means
:: GRAPH_1:def 9
not ex x st x in the carrier' of IT &
(the Source of IT).x = (the Target of IT).x;
attr IT is connected means
:: GRAPH_1:def 10
not ex G1, G2 being Graph st
the carrier of G1 misses the carrier of G2 & IT is_sum_of G1, G2;
end;
definition
let IT be MultiGraphStruct;
attr IT is finite means
:: GRAPH_1:def 11
the carrier of IT is finite & the carrier' of IT is finite;
end;
registration
cluster finite for MultiGraphStruct;
cluster finite non-multi oriented simple connected for Graph;
end;
registration
let G be finite MultiGraphStruct;
cluster the carrier of G -> finite;
cluster the carrier' of G -> finite;
end;
reserve x, y for Element of (the carrier of G);
definition
let G;
let x, y;
let v;
pred v joins x, y means
:: GRAPH_1:def 12
(the Source of G).v = x & (the Target of G).v = y or
(the Source of G).v = y & (the Target of G).v = x;
end;
definition
let G;
let x,y be Element of (the carrier of G);
pred x,y are_incident means
:: GRAPH_1:def 13
ex v being set st v in the carrier' of G & v joins x, y;
end;
definition
let G be Graph;
mode Chain of G -> FinSequence means
:: GRAPH_1:def 14
(for n st 1 <= n & n <= len it holds it.n in the carrier' of G) &
ex p being FinSequence st len p = len it + 1 &
(for n st 1 <= n & n <= len p holds p.n in the carrier of G) &
for n st 1 <= n & n <= len it
ex x9, y9 being Vertex of G st
x9 = p.n & y9 = p.(n+1) & it.n joins x9, y9;
end;
definition
let G be Graph;
redefine mode Chain of G -> FinSequence of the carrier' of G;
end;
definition
let G be Graph;
let IT be Chain of G;
attr IT is oriented means
:: GRAPH_1:def 15
for n st 1 <= n & n < len IT holds
(the Source of G).(IT.(n+1)) = (the Target of G).(IT.n);
end;
registration
let G be Graph;
cluster empty for Chain of G;
end;
registration
let G be Graph;
cluster empty -> oriented for Chain of G;
end;
definition
let G be Graph;
let IT be Chain of G;
redefine attr IT is one-to-one means
:: GRAPH_1:def 16
for n, m st 1 <= n & n < m & m <= len IT holds IT.n <> IT.m;
end;
definition
let G be Graph;
mode Path of G is one-to-one Chain of G;
end;
definition
let G be Graph;
mode OrientedPath of G is one-to-one oriented Chain of G;
end;
definition
let G be Graph;
let IT be Path of G;
attr IT is cyclic means
:: GRAPH_1:def 17
ex p being FinSequence st len p = len IT + 1 &
(for n st 1 <= n & n <= len p holds p.n in the carrier of G) &
(for n st 1 <= n & n <= len IT
ex x9, y9 being Vertex of G st
x9 = p.n & y9 = p.(n+1) & IT.n joins x9, y9) & p.1 = p.(len p);
end;
registration
let G be Graph;
cluster empty -> cyclic for Path of G;
end;
definition
let G be Graph;
mode Cycle of G is cyclic Path of G;
end;
definition
let G be Graph;
mode OrientedCycle of G is cyclic OrientedPath of G;
end;
definition
let G be Graph;
mode Subgraph of G -> Graph means
:: GRAPH_1:def 18
the carrier of it c= the carrier of G &
the carrier' of it c= the carrier' of G &
for v st v in the carrier' of it holds
(the Source of it).v = (the Source of G).v &
(the Target of it).v = (the Target of G).v &
(the Source of G).v in the carrier of it &
(the Target of G).v in the carrier of it;
end;
registration
let G be Graph;
cluster strict for Subgraph of G;
end;
definition
let G be finite Graph;
func VerticesCount G -> Element of NAT means
:: GRAPH_1:def 19
ex B being finite set st B = the carrier of G & it = card B;
func EdgesCount G -> Element of NAT means
:: GRAPH_1:def 20
ex B being finite set st B = the carrier' of G & it = card B;
end;
definition
let G be finite Graph;
let x be Vertex of G;
func EdgesIn x -> Element of NAT means
:: GRAPH_1:def 21
ex X being finite set st (for z being set holds
z in X iff z in the carrier' of G & (the Target of G).z = x) & it = card(X);
func EdgesOut x -> Element of NAT means
:: GRAPH_1:def 22
ex X being finite set st (for z being set holds
z in X iff z in the carrier' of G & (the Source of G).z = x) & it = card(X);
end;
definition
let G be finite Graph;
let x be Vertex of G;
func Degree x -> Element of NAT equals
:: GRAPH_1:def 23
EdgesIn(x) + EdgesOut(x);
end;
definition
let G1, G2 be Graph;
pred G1 c= G2 means
:: GRAPH_1:def 24
G1 is Subgraph of G2;
reflexivity;
end;
definition
let G be Graph;
func bool G -> set means
:: GRAPH_1:def 25
for x being object holds x in it iff x is strict Subgraph of G;
end;
scheme :: GRAPH_1:sch 1
GraphSeparation{G() -> Graph, P[object]}:
ex X being set st
for x being set holds x in X iff x is strict Subgraph of G() & P[x];
:: Properties of graphs ::
theorem :: GRAPH_1:1
for G being Graph holds dom(the Source of G) = the carrier' of G &
dom(the Target of G) = the carrier' of G;
theorem :: GRAPH_1:2
for x being Vertex of G holds x in the carrier of G;
theorem :: GRAPH_1:3
for v being set holds v in the carrier' of G implies
(the Source of G).v in the carrier of G &
(the Target of G).v in the carrier of G;
:: Chain ::
theorem :: GRAPH_1:4
for p being Chain of G holds p|Seg(n) is Chain of G;
:: Sum of two graphs ::
theorem :: GRAPH_1:5
G1 c= G implies (the Source of G1) c= (the Source of G) &
(the Target of G1) c= (the Target of G);
theorem :: GRAPH_1:6
(the Source of G1) tolerates (the Source of G2) &
(the Target of G1) tolerates (the Target of G2) implies
(the Source of (G1 \/ G2)) = (the Source of G1) \/ (the Source of G2) &
(the Target of (G1 \/ G2)) = (the Target of G1) \/ (the Target of G2);
theorem :: GRAPH_1:7
for G being strict Graph holds G = G \/ G;
theorem :: GRAPH_1:8
(the Source of G1) tolerates (the Source of G2) &
(the Target of G1) tolerates (the Target of G2) implies G1 \/ G2 = G2 \/ G1;
theorem :: GRAPH_1:9
(the Source of G1) tolerates (the Source of G2) &
(the Target of G1) tolerates (the Target of G2) &
(the Source of G1) tolerates (the Source of G3) &
(the Target of G1) tolerates (the Target of G3) &
(the Source of G2) tolerates (the Source of G3) &
(the Target of G2) tolerates (the Target of G3) implies
(G1 \/ G2) \/ G3 = G1 \/ (G2 \/ G3);
theorem :: GRAPH_1:10
G is_sum_of G1, G2 implies G is_sum_of G2, G1;
theorem :: GRAPH_1:11
for G being strict Graph holds G is_sum_of G, G;
:: Graphs' inclusion ::
theorem :: GRAPH_1:12
(ex G st G1 c= G & G2 c= G) implies G1 \/ G2 = G2 \/ G1;
theorem :: GRAPH_1:13
(ex G st G1 c= G & G2 c= G & G3 c= G) implies (G1 \/ G2) \/ G3 = G1 \/ ( G2
\/ G3);
theorem :: GRAPH_1:14
{} is Chain of G;
theorem :: GRAPH_1:15
for H1, H2 being strict Subgraph of G st
the carrier of H1 = the carrier of H2 &
the carrier' of H1 = the carrier' of H2
holds H1 = H2;
theorem :: GRAPH_1:16
for G1,G2 being strict Graph holds G1 c= G2 & G2 c= G1 implies G1 = G2;
theorem :: GRAPH_1:17
G1 c= G2 & G2 c= G3 implies G1 c= G3;
theorem :: GRAPH_1:18
G is_sum_of G1, G2 implies G1 c= G & G2 c= G;
theorem :: GRAPH_1:19
(the Source of G1) tolerates (the Source of G2) &
(the Target of G1) tolerates (the Target of G2) implies
G1 c= G1 \/ G2 & G2 c= G1 \/ G2;
theorem :: GRAPH_1:20
(ex G st G1 c= G & G2 c= G) implies G1 c= G1 \/ G2 & G2 c= G1 \/ G2;
theorem :: GRAPH_1:21
G1 c= G3 & G2 c= G3 & G is_sum_of G1, G2 implies G c= G3;
theorem :: GRAPH_1:22
G1 c= G & G2 c= G implies (G1 \/ G2) c= G;
theorem :: GRAPH_1:23
for G1,G2 being strict Graph holds
G1 c= G2 implies G1 \/ G2 = G2 & G2 \/ G1 = G2;
theorem :: GRAPH_1:24
(the Source of G1) tolerates (the Source of G2) &
(the Target of G1) tolerates (the Target of G2) &
(G1 \/ G2 = G2 or G2 \/ G1 = G2) implies G1 c= G2;
theorem :: GRAPH_1:25
for G being oriented Graph st G1 c= G holds G1 is oriented;
theorem :: GRAPH_1:26
for G being non-multi Graph st G1 c= G holds G1 is non-multi;
theorem :: GRAPH_1:27
for G being simple Graph st G1 c= G holds G1 is simple;
:: Set of all subgraphs ::
theorem :: GRAPH_1:28
for G1 being strict Graph holds G1 in bool G iff G1 c= G;
theorem :: GRAPH_1:29
for G being strict Graph holds G in bool G;
theorem :: GRAPH_1:30
for G1 being strict Graph holds G1 c= G2 iff bool G1 c= bool G2;
theorem :: GRAPH_1:31
for G being strict Graph holds { G } c= bool G;
theorem :: GRAPH_1:32
for G1,G2 being strict Graph holds
(the Source of G1) tolerates (the Source of G2) &
(the Target of G1) tolerates (the Target of G2) &
bool (G1 \/ G2) c= (bool G1) \/ (bool G2) implies G1 c= G2 or G2 c= G1;
theorem :: GRAPH_1:33
(the Source of G1) tolerates (the Source of G2) &
(the Target of G1) tolerates (the Target of G2) implies
bool G1 \/ bool G2 c= bool (G1 \/ G2);
theorem :: GRAPH_1:34
G1 in bool G & G2 in bool G implies (G1 \/ G2) in bool G;