Volume 6, 1994

University of Bialystok

Copyright (c) 1994 Association of Mizar Users

### The abstract of the Mizar article:

### The Formalization of Simple Graphs

**by****Yozo Toda**- Received September 8, 1994
- MML identifier: SGRAPH1

- [ Mizar article, MML identifier index ]

environ vocabulary FINSEQ_1, BOOLE, FINSET_1, FUNCT_1, CARD_1, REALSET1, SETWISEO, FINSUB_1, TARSKI, MCART_1, SGRAPH1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, NAT_1, MCART_1, CARD_1, STRUCT_0, REALSET1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSET_1, FINSEQ_2, FINSUB_1, SETWISEO; constructors MCART_1, WELLORD2, REALSET1, NAT_1, SETWISEO, FINSEQ_2, XREAL_0, MEMBERED, XBOOLE_0; clusters SUBSET_1, FINSET_1, FINSUB_1, REALSET1, RELSET_1, FINSEQ_1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2; 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; definition let m,n be Nat; cluster nat_interval(m,n) -> finite; end; canceled; theorem :: SGRAPH1:2 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:3 for m,n,k being Nat holds k in nat_interval(m,n) iff (m<=k & k<=n); theorem :: SGRAPH1:4 for n being Nat holds nat_interval (1,n) = Seg n; theorem :: SGRAPH1:5 for m,n being Nat st 1 <= m holds nat_interval(m,n) c= Seg n; theorem :: SGRAPH1:6 for k,m,n being Nat st k<m holds Seg k misses nat_interval(m,n); theorem :: SGRAPH1:7 for m,n being Nat st n<m holds nat_interval(m,n)={}; definition let A be set; canceled 2; func TWOELEMENTSETS(A) -> set equals :: SGRAPH1:def 4 {z where z is finite Element of bool A : card z = 2}; end; canceled; theorem :: SGRAPH1:9 for A be set, e be set holds (e in TWOELEMENTSETS(A) iff ex z being finite Subset of A st (e = z & (card z)=2)); theorem :: SGRAPH1:10 for A be set, e be set holds (e in TWOELEMENTSETS(A) iff (e is finite Subset of A & ex x,y being set st (x in A & y in A & x<>y & e = {x,y}))); theorem :: SGRAPH1:11 for A being set holds TWOELEMENTSETS(A) c= (bool A); theorem :: SGRAPH1:12 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:13 TWOELEMENTSETS {} = {}; theorem :: SGRAPH1:14 for t,u being set st t c= u holds TWOELEMENTSETS(t) c= TWOELEMENTSETS(u); theorem :: SGRAPH1:15 for A being finite set holds TWOELEMENTSETS(A) is finite; theorem :: SGRAPH1:16 for A being non trivial set holds TWOELEMENTSETS(A) is non empty; theorem :: SGRAPH1:17 for a being set holds TWOELEMENTSETS {a} = {}; definition let X be empty set; cluster -> empty Subset of X; 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 <Empty,Empty>, :: (2) if <V,E> is an element of SIMPLEGRAPHS and n is not a vertex of <V,E>, :: then <(V U {n}),E> is also an element of SIMPLEGRAPHS, :: (3) if <V,E> is an element of SIMPLEGRAPHS, :: v1,v2 are different vertices of <V,E>, :: and {v1,v2} is not an edge of <V,E>, :: then <V,(E U {v1,v2})> is also an element of SIMPLEGRAPHS. definition let X be set; canceled; func SIMPLEGRAPHS(X) -> set equals :: SGRAPH1:def 6 {SimpleGraphStruct (# v,e #) where v is finite Subset of X, e is finite Subset of TWOELEMENTSETS(v) : not contradiction}; end; canceled; theorem :: SGRAPH1:19 SimpleGraphStruct (#{},{}TWOELEMENTSETS{}#) in SIMPLEGRAPHS(X); definition let X be set; cluster SIMPLEGRAPHS(X) -> non empty; end; definition let X be set; mode SimpleGraph of X -> strict SimpleGraphStruct means :: SGRAPH1:def 7 it is Element of SIMPLEGRAPHS(X); end; canceled; theorem :: SGRAPH1:21 for g being set 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. canceled; theorem :: SGRAPH1:23 for g being SimpleGraph of X holds (the carrier of g) c= X & (the SEdges of g) c= TWOELEMENTSETS (the carrier of g); canceled; theorem :: SGRAPH1:25 for g being SimpleGraph of X, e being set st e in the SEdges of g holds ex v1,v2 being set st (v1 in the carrier of g & v2 in the carrier of g & v1 <> v2 & e={v1,v2}); theorem :: SGRAPH1:26 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:27 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,G' be SimpleGraph of X; pred G is_isomorphic_to G' means :: SGRAPH1:def 8 ex Fv being Function of the carrier of G, the carrier of G' 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 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:28 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#))); canceled; theorem :: SGRAPH1:30 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 & not n in V) holds SimpleGraphStruct (#(V \/ {n}),Evn#) in SIMPLEGRAPHS(X); theorem :: SGRAPH1:31 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 9 (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; canceled 3; theorem :: SGRAPH1:35 SIMPLEGRAPHS(X) is_SetOfSimpleGraphs_of X; theorem :: SGRAPH1:36 for OTHER being set st OTHER is_SetOfSimpleGraphs_of X holds SIMPLEGRAPHS(X) c= OTHER; theorem :: SGRAPH1:37 SIMPLEGRAPHS(X) is_SetOfSimpleGraphs_of X & for OTHER being set st OTHER is_SetOfSimpleGraphs_of X holds SIMPLEGRAPHS(X) c= OTHER; 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 10 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) -> Nat means :: SGRAPH1:def 11 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; canceled; theorem :: SGRAPH1:39 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:40 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:41 for g being SimpleGraph of X, v,e being set st v in the carrier of g & e in the SEdges of g & degree (g,v)=0 holds not v in e; theorem :: SGRAPH1:42 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 12 (p.1)=v1 & (p.(len p))=v2 & (for i being Nat st (1<=i & i<(len p)) holds {p.i, p.(i+1)} in (the SEdges of g)) & (for i,j being Nat st 1<=i & i<(len p) & i<j & j<(len p) holds p.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 13 {ss where ss is Element of (the carrier of g)* : ss is_path_of v1,v2}; end; canceled; theorem :: SGRAPH1:44 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:45 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 14 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 Nat; canceled; func K_(m,n) -> SimpleGraph of NAT means :: SGRAPH1:def 16 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 Nat; func K_(n) -> SimpleGraph of NAT means :: SGRAPH1:def 17 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 18 K_(3); end; theorem :: SGRAPH1:46 ex ee being Subset of TWOELEMENTSETS(Seg 3) st ee = {{1,2},{2,3},{3,1}} & TriangleGraph = SimpleGraphStruct (#(Seg 3),ee#); theorem :: SGRAPH1:47 (the carrier of TriangleGraph)=(Seg 3) & (the SEdges of TriangleGraph) = {{1,2},{2,3},{3,1}}; theorem :: SGRAPH1:48 {1,2} in (the SEdges of TriangleGraph) & {2,3} in (the SEdges of TriangleGraph) & {3,1} in (the SEdges of TriangleGraph); theorem :: SGRAPH1:49 <*1*>^<*2*>^<*3*>^<*1*> is_cycle_of TriangleGraph;

Back to top