:: Graphs :: by Krzysztof Hryniewiecki :: :: Received December 5, 1990 :: Copyright (c) 1990-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, 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;