Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994 Association of Mizar Users

### The Formalization of Simple Graphs

by
Yozo Toda

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) :
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;
```