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;