:: The Formalisation of Simple Graphs :: by Yozo Toda :: :: Received September 8, 1994 :: Copyright (c) 1994-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, FINSEQ_1, XXREAL_0, CARD_1, XBOOLE_0, ARYTM_3, TARSKI, FINSET_1, ZFMISC_1, STRUCT_0, FUNCT_1, FUNCT_2, FINSUB_1, SETWISEO, MCART_1, RELAT_1, ORDINAL4, SGRAPH1, NAT_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, XTUPLE_0, MCART_1, STRUCT_0, FUNCT_1, FUNCT_2, FINSEQ_1, FINSET_1, FINSEQ_2, FINSUB_1, SETWISEO, XXREAL_0; constructors WELLORD2, SETWISEO, NAT_1, FINSEQ_2, STRUCT_0, XTUPLE_0, NUMBERS; registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, FINSUB_1, XXREAL_0, NAT_1, FINSEQ_1, CARD_1, XTUPLE_0; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin :: interval is defined as subset of reals in measure5. :: so we use a symbol nat_interval here. :: following the definition of Seg, I add an assumption 1 <= m. :: but it is unnatural, I think. :: I changed the proof of existence :: so that the assumption (1 <= m) is not necessary. :: now nat_interval has the very natural definition, I think (-: definition let m,n be Nat; func nat_interval(m,n) -> Subset of NAT equals :: SGRAPH1:def 1 {i where i is Nat: m<=i & i<=n}; end; notation let m,n be Nat; synonym Seg (m,n) for nat_interval (m,n); end; registration let m,n be Nat; cluster nat_interval(m,n) -> finite; end; theorem :: SGRAPH1:1 for m,n being Nat, e being set holds e in nat_interval(m,n) iff ex i being Nat st e=i & m<=i & i<=n; theorem :: SGRAPH1:2 for m,n,k being Nat holds k in nat_interval(m,n) iff m<=k & k<=n; theorem :: SGRAPH1:3 for n being Nat holds nat_interval (1,n) = Seg n; theorem :: SGRAPH1:4 for m,n being Nat st 1 <= m holds nat_interval(m,n) c= Seg n; theorem :: SGRAPH1:5 for k,m,n being Nat st k set equals :: SGRAPH1:def 2 {z where z is Subset of A : card z = 2}; end; theorem :: SGRAPH1:7 for A, e be set holds e in TWOELEMENTSETS(A) iff ex z being Subset of A st e = z & card z = 2; theorem :: SGRAPH1:8 for A, e be set holds (e in TWOELEMENTSETS(A) iff (e is finite Subset of A & ex x,y being object st x in A & y in A & x<>y & e = {x,y} )); theorem :: SGRAPH1:9 for A being set holds TWOELEMENTSETS(A) c= bool A; theorem :: SGRAPH1:10 for A being set, e1,e2 being set st {e1,e2} in TWOELEMENTSETS(A) holds e1 in A & e2 in A & e1<>e2; theorem :: SGRAPH1:11 TWOELEMENTSETS {} = {}; registration cluster TWOELEMENTSETS {} -> empty; end; theorem :: SGRAPH1:12 for t,u being set st t c= u holds TWOELEMENTSETS(t) c= TWOELEMENTSETS(u); ::$CT 3 registration let A be finite set; cluster TWOELEMENTSETS A -> finite; end; registration let A be non trivial set; cluster TWOELEMENTSETS A -> non empty; end; registration let a be set; cluster TWOELEMENTSETS {a} -> empty; end; reserve X for set; begin :: SECTION 1: SIMPLEGRAPHS. :: graph is defined as a pair of two sets, of vertices and of edges. :: we treat only simple graphs; :: edges are non-directed, there is no loop, :: between two vertices is at most one edge. :: we define the set of all graphs SIMPLEGRAPHS, :: and later define some operations on graphs :: (contraction, deletion, minor, etc.) as relations on SIMPLEGRAPHS. :: Vertices and Edges are used in GRAPH_1. so we must use different names. :: we restrict simple graphs as finite ones :: to treat degree as a cardinal of a set of edges. definition struct (1-sorted) SimpleGraphStruct (# carrier -> set, SEdges -> Subset of TWOELEMENTSETS (the carrier) #); end; :: SIMPLEGRAPHS is the set of all (simple) graphs, :: which is the smallest set satisfying following three conditions: :: (1) it contains , :: (2) if is an element of SIMPLEGRAPHS and n is not a vertex of , :: then <(V U {n}),E> is also an element of SIMPLEGRAPHS, :: (3) if is an element of SIMPLEGRAPHS, :: v1,v2 are different vertices of , :: and {v1,v2} is not an edge of , :: then is also an element of SIMPLEGRAPHS. definition let X be set; func SIMPLEGRAPHS(X) -> set equals :: SGRAPH1:def 3 the set of all SimpleGraphStruct (# v,e #) where v is finite Subset of X, e is finite Subset of TWOELEMENTSETS(v); end; theorem :: SGRAPH1:16 SimpleGraphStruct (#{},{}TWOELEMENTSETS{}#) in SIMPLEGRAPHS(X); registration let X be set; cluster SIMPLEGRAPHS(X) -> non empty; end; definition let X be set; mode SimpleGraph of X -> strict SimpleGraphStruct means :: SGRAPH1:def 4 it is Element of SIMPLEGRAPHS(X); end; theorem :: SGRAPH1:17 for g being object holds (g in SIMPLEGRAPHS(X) iff ex v being finite Subset of X, e being finite Subset of TWOELEMENTSETS(v) st g = SimpleGraphStruct (#v,e#)); begin :: SECTION 2: destructors for SimpleGraphStruct. theorem :: SGRAPH1:18 for g being SimpleGraph of X holds the carrier of g c= X & the SEdges of g c= TWOELEMENTSETS (the carrier of g); theorem :: SGRAPH1:19 for g being SimpleGraph of X, e being set st e in the SEdges of g ex v1,v2 being object st v1 in the carrier of g & v2 in the carrier of g & v1 <> v2 & e={v1,v2}; theorem :: SGRAPH1:20 for g being SimpleGraph of X, v1,v2 being set st {v1,v2} in the SEdges of g holds v1 in the carrier of g & v2 in the carrier of g & v1 <> v2; theorem :: SGRAPH1:21 for g being SimpleGraph of X holds (the carrier of g) is finite Subset of X & (the SEdges of g) is finite Subset of TWOELEMENTSETS(the carrier of g); :: SECTION 3: equality relation on SIMPLEGRAPHS. :: two graphs are said to be "isomorphic" if :: (1) there is bijective function (i.e. set-theoretic isomorphism) :: between two sets of vertices, :: (2) this iso. respects the correspondence of edges. definition let X; let G,G9 be SimpleGraph of X; pred G is_isomorphic_to G9 means :: SGRAPH1:def 5 ex Fv being Function of the carrier of G, the carrier of G9 st Fv is bijective & for v1,v2 being Element of G holds ({v1,v2} in (the SEdges of G) iff {Fv.v1, Fv.v2} in the SEdges of G); end; begin :: SECTION 4: properties of SIMPLEGRAPHS. :: here is the induction principle on SIMPLEGRAPHS(X). scheme :: SGRAPH1:sch 1 IndSimpleGraphs0 { X()-> set, P[set] } : for G being set st G in SIMPLEGRAPHS(X()) holds P[G] provided P[SimpleGraphStruct (#{},{}TWOELEMENTSETS{}#)] and for g being SimpleGraph of X(), v being set st g in SIMPLEGRAPHS(X() ) & P[g] & v in X() & not v in (the carrier of g) holds P[SimpleGraphStruct (#( the carrier of g)\/{v}, {}TWOELEMENTSETS((the carrier of g)\/{v})#)] and for g being SimpleGraph of X(), e being set st P[g] & e in TWOELEMENTSETS(the carrier of g) & not e in (the SEdges of g) holds ex sege being Subset of TWOELEMENTSETS(the carrier of g) st sege=((the SEdges of g)\/{e }) & P[SimpleGraphStruct (#(the carrier of g),sege#)]; :: Now we give a theorem characterising SIMPLEGRAPHS as :: an inductively defined set. We need some lemmas. theorem :: SGRAPH1:22 for g being SimpleGraph of X holds (g=SimpleGraphStruct (#{},{}TWOELEMENTSETS{}#) or ex v being set, e being Subset of TWOELEMENTSETS(v) st v is non empty & g=SimpleGraphStruct (#v,e#) ); theorem :: SGRAPH1:23 for V being Subset of X, E being Subset of TWOELEMENTSETS(V), n being set, Evn being finite Subset of TWOELEMENTSETS(V \/ {n}) st SimpleGraphStruct (#V,E#) in SIMPLEGRAPHS(X) & n in X holds SimpleGraphStruct (#(V \/ {n}),Evn#) in SIMPLEGRAPHS(X); theorem :: SGRAPH1:24 for V being Subset of X, E being Subset of TWOELEMENTSETS(V), v1,v2 being set st v1 in V & v2 in V & v1<>v2 & SimpleGraphStruct (#V,E#) in SIMPLEGRAPHS(X) holds ex v1v2 being finite Subset of TWOELEMENTSETS(V) st v1v2 = (E \/ {{v1,v2}}) & SimpleGraphStruct (#V,v1v2#) in SIMPLEGRAPHS(X); :: next we define a predicate :: which describe how SIMPLEGRAPHS are generated inductively. :: *** QUESTION *** :: conditions (not n in V) and (not {v1,v2} in E) are redundant? definition let X be set, GG be set; pred GG is_SetOfSimpleGraphs_of X means :: SGRAPH1:def 6 SimpleGraphStruct (#{},{}TWOELEMENTSETS{}#) in GG & (for V being Subset of X, E being Subset of TWOELEMENTSETS(V), n being set, Evn being finite Subset of TWOELEMENTSETS(V \/ {n}) st (SimpleGraphStruct (#V,E#) in GG & n in X & not n in V) holds SimpleGraphStruct (#(V \/ {n}),Evn#) in GG) & for V being Subset of X, E being Subset of TWOELEMENTSETS(V), v1,v2 being set st SimpleGraphStruct (#V,E#) in GG & v1 in V & v2 in V & v1<>v2 & (not {v1,v2} in E) holds ex v1v2 being finite Subset of TWOELEMENTSETS(V) st v1v2 = (E \/ {{v1,v2}}) & SimpleGraphStruct (#V,v1v2#) in GG; end; theorem :: SGRAPH1:25 SIMPLEGRAPHS(X) is_SetOfSimpleGraphs_of X; theorem :: SGRAPH1:26 for A being set st A is_SetOfSimpleGraphs_of X holds SIMPLEGRAPHS(X) c= A; theorem :: SGRAPH1:27 SIMPLEGRAPHS(X) is_SetOfSimpleGraphs_of X & for A being set st A is_SetOfSimpleGraphs_of X holds SIMPLEGRAPHS(X) c= A; begin :: SECTION 5: SubGraphs. :: graph G is a subgraph of graph G' if :: (1) the set of vertices of G is a subset of the set of vertices of G', :: (2) the set of edges of G is a subset of the set of edges of G', :: where two endpoints of each edge of G must be the vertices of G. :: (of course G must be a graph!) :: now no lemma is proved )-: definition let X be set, G be SimpleGraph of X; mode SubGraph of G -> SimpleGraph of X means :: SGRAPH1:def 7 the carrier of it c= the carrier of G & the SEdges of it c= the SEdges of G; end; begin :: SECTION 6: degree of vertices. :: the degree of a vertex means the number of edges connected to that vertex. :: in the case of simple graphs, we can prove that :: the degree is equal to the number of adjacent vertices. :: (if loop is allowed, :: the number of edges and the number of adjacent vertices are different.) :: at first we defined degree(v), :: where v was Element of the SEdges of(G) and G was an implicit argument. :: but now we have changed the type of v to set, :: and G must be an explicit argument :: or we get an error "Inaccessible locus". definition let X be set, G be SimpleGraph of X; let v be set; func degree (G,v) -> Element of NAT means :: SGRAPH1:def 8 ex X being finite set st ( for z being set holds (z in X iff z in (the SEdges of G) & v in z)) & it = card X; end; theorem :: SGRAPH1:28 for X being non empty set, G being SimpleGraph of X, v being set holds ex ww being finite set st ww = {w where w is Element of X : w in the carrier of G & {v,w} in the SEdges of G} & degree(G,v) = card ww; theorem :: SGRAPH1:29 for X being non empty set,g being SimpleGraph of X, v being set st v in the carrier of g holds ex VV being finite set st VV=(the carrier of g) & degree(g,v)<(card VV); theorem :: SGRAPH1:30 for g being SimpleGraph of X, v,e being set st e in the SEdges of g & degree (g,v)=0 holds not v in e; theorem :: SGRAPH1:31 for g being SimpleGraph of X, v being set, vg being finite set st vg=( the carrier of g) & v in vg & 1+degree(g,v)=(card vg) holds for w being Element of vg st v<>w holds ex e being set st e in (the SEdges of g) & e={v,w}; begin :: SECTION 7: path, cycle :: path is coded as a sequence of vertices, :: any two of them contained are different each other. :: but the head and the tail may be equal (which is cycle). definition let X be set, g be SimpleGraph of X, v1,v2 be Element of g, p be FinSequence of the carrier of g; pred p is_path_of v1,v2 means :: SGRAPH1:def 9 p.1 = v1 & (p.(len p))=v2 & (for i being Element of NAT st 1<=i & i p.j & {p.i,p.(i+1)}<>{p.j,p.(j+1)}; end; definition let X be set, g be SimpleGraph of X, v1,v2 be Element of the carrier of g; func PATHS(v1,v2) -> Subset of ((the carrier of g)*) equals :: SGRAPH1:def 10 {ss where ss is Element of (the carrier of g)* : ss is_path_of v1,v2}; end; theorem :: SGRAPH1:32 for g being SimpleGraph of X, v1,v2 being Element of the carrier of g, e being set holds (e in PATHS(v1,v2) iff ex ss being Element of (the carrier of g)* st e=ss & ss is_path_of v1,v2 ); theorem :: SGRAPH1:33 for g being SimpleGraph of X, v1,v2 being Element of (the carrier of g ), e being Element of (the carrier of g)* st e is_path_of v1,v2 holds e in PATHS(v1,v2); ::definition :: is_cycle :: let g be SimpleGraph of X, :: v1,v2 be Element of (the carrier of g), :: p be Element of PATHS(v1,v2); :: pred p is_cycle means :cycleDef: :: v1=v2 & ex q being Element of ((the carrier of g)*) st (q=p & 3<=(len q)); ::end; definition let X be set, g be SimpleGraph of X, p be set; pred p is_cycle_of g means :: SGRAPH1:def 11 ex v being Element of the carrier of g st p in PATHS(v,v); end; :: cycle(v) = {v1,...,vn : {vi,v(i+1)} in EdgesOf g, 3 <= n} begin :: SECTION 8: some famous graphs. :: K_{3,3} = {{1,2,3,4,5,6}, :: {{1,4},{1,5},{1,6},{2,4},{2,5},{2,6},{3,4},{3,5},{3,6}}}. :: K_5 = {{1,2,3,4,5}, :: {{1,2},{1,3},{1,4},{1,5},{2,3},{2,4},{2,5},{3,4},{3,5},{4,5}}}. :: for the proof of Kuratowski's theorem, we need only K_{3,3} and K_5. :: here we define complete (and complete bipartate) graphs in general. definition let n,m be Element of NAT; func K_(m,n) -> SimpleGraph of NAT means :: SGRAPH1:def 12 ex ee being Subset of TWOELEMENTSETS(Seg (m+n)) st ee = {{i,j} where i,j is Element of NAT : i in Seg m & j in (nat_interval(m+1,m+n))} & it = SimpleGraphStruct (# (Seg (m+n)),ee#); end; definition let n be Element of NAT; func K_(n) -> SimpleGraph of NAT means :: SGRAPH1:def 13 ex ee being finite Subset of TWOELEMENTSETS(Seg n) st ee = {{i,j} where i,j is Element of NAT : i in (Seg n) & j in (Seg n) & i<>j} & it = SimpleGraphStruct (# (Seg n), ee #); end; :: TriangleGraph will be used in the definition of planegraphs. definition func TriangleGraph -> SimpleGraph of NAT equals :: SGRAPH1:def 14 K_(3); end; theorem :: SGRAPH1:34 ex ee being Subset of TWOELEMENTSETS(Seg 3) st ee = {.{.1,2.},{.2,3.},{.3,1.}.} & TriangleGraph = SimpleGraphStruct (#(Seg 3),ee#); theorem :: SGRAPH1:35 (the carrier of TriangleGraph)=(Seg 3) & (the SEdges of TriangleGraph) = {.{.1,2.},{.2,3.},{.3,1.}.}; theorem :: SGRAPH1:36 {1,2} in (the SEdges of TriangleGraph) & {2,3} in (the SEdges of TriangleGraph) & {3,1} in (the SEdges of TriangleGraph); theorem :: SGRAPH1:37 <*1*>^<*2*>^<*3*>^<*1*> is_cycle_of TriangleGraph;