:: The Formalisation of Simple Graphs
:: by Yozo Toda
::
:: Received September 8, 1994
:: Copyright (c) 1994-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, 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, XCMPLX_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 finite Subset of A : card
z = 2};
end;
theorem :: SGRAPH1:7
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:8
for A be set, 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 {} = {};
theorem :: SGRAPH1:12
for t,u being set st t c= u holds TWOELEMENTSETS(t) c= TWOELEMENTSETS( u);
theorem :: SGRAPH1:13
for A being finite set holds TWOELEMENTSETS(A) is finite;
theorem :: SGRAPH1:14
for A being non trivial set holds TWOELEMENTSETS(A) is non empty;
theorem :: SGRAPH1:15
for a being set holds TWOELEMENTSETS {a} = {};
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 OTHER being set st OTHER is_SetOfSimpleGraphs_of X holds
SIMPLEGRAPHS(X) c= OTHER;
theorem :: SGRAPH1:27
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 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<(len p)) holds {p.i, p.(i+1)} in (the SEdges
of g)) & for i,j being Element of NAT st 1<=i & i<(len 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 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;