The abstract of the Mizar article:

Euler Circuits and Paths

by

Yatsuka Nakamura, and

Piotr Rudnicki

Received July 29, 1997

MML identifier: GRAPH_3

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSEQ_2, FINSEQ_1, MATRIX_2, INT_1, ARYTM_1, RELAT_1, GRAPH_2,
      FUNCT_1, BOOLE, GRAPH_1, MSAFREE2, ORDERS_1, RELAT_2, PARTFUN1, FINSET_1,
      CARD_1, FUNCT_4, CAT_1, FUNCOP_1, TARSKI, FINSEQ_6, NEWTON, SQUARE_1,
      GRAPH_3, FINSEQ_4;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0,
      RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, CQC_LANG, FUNCT_4, NAT_1, INT_1,
      FINSET_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, CARD_1, GRAPH_1, GRAPH_2,
      MSSCYC_1, PRE_CIRC, ABIAN;
 constructors GRAPH_2, MSSCYC_1, WELLORD2, BINARITH, CQC_LANG, PRE_CIRC, ABIAN,
      WELLFND1, FINSEQ_4, INT_1;
 clusters SUBSET_1, GRAPH_2, RELSET_1, FINSET_1, FINSEQ_5, CARD_1, MSSCYC_1,
      INT_1, ABIAN, CQC_LANG, FINSEQ_1, NAT_1, XREAL_0, MEMBERED, NUMBERS,
      ORDINAL2;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin :: Preliminaries

definition let D be set, T be FinSequence-DOMAIN of D,
               S be non empty Subset of T;
 redefine mode Element of S -> FinSequence of D;
end;

definition
 let i, j be even Integer;
 cluster i-j -> even;
end;

theorem :: GRAPH_3:1
for i, j being Integer holds (i is even iff j is even) iff (i-j) is even;

theorem :: GRAPH_3:2
 for p being FinSequence, m, n, a being Nat
  st a in dom (m, n)-cut p
  ex k being Nat st
   k in dom p & p.k = ((m,n)-cut p).a & k+1 = m+a & m <= k & k <= n;

definition
 let G be Graph;
 mode Vertex of G is Element of the Vertices of G;
end;

 reserve G for Graph,
         v, v1, v2 for Vertex of G,
         c for Chain of G,
         p, p1, p2 for Path of G,
         vs, vs1, vs2 for FinSequence of the Vertices of G,
         e, X for set,
         n, m for Nat;

theorem :: GRAPH_3:3
 vs is_vertex_seq_of c implies vs is non empty;

canceled 3;

theorem :: GRAPH_3:7
 e in the Edges of G implies <*e*> is Path of G;

theorem :: GRAPH_3:8
 (m,n)-cut p is Path of G;

theorem :: GRAPH_3:9
 rng p1 misses rng p2 &
 vs1 is_vertex_seq_of p1 & vs2 is_vertex_seq_of p2 & vs1.len vs1 = vs2.1
  implies p1^p2 is Path of G;

canceled 2;

theorem :: GRAPH_3:12
 c = {} implies c is cyclic;

definition let G be Graph;
 cluster cyclic Path of G;
end;

theorem :: GRAPH_3:13
 for p being cyclic Path of G
  holds ((m+1,len p)-cut p)^(1,m)-cut p is cyclic Path of G;

theorem :: GRAPH_3:14
 m+1 in dom p implies
    len (((m+1,len p)-cut p)^(1,m)-cut p) = len p &
    rng (((m+1,len p)-cut p)^(1,m)-cut p) = rng p &
   (((m+1,len p)-cut p)^(1,m)-cut p).1 = p.(m+1);

theorem :: GRAPH_3:15
for p being cyclic Path of G
  st n in dom p
   ex p' being cyclic Path of G
    st p'.1 = p.n & len p' = len p & rng p' = rng p;

theorem :: GRAPH_3:16  :: see MSSCYC_1:4
  for s, t being Vertex of G
    st s = (the Source of G).e & t = (the Target of G).e
     holds <*t, s*> is_vertex_seq_of <*e*>;

theorem :: GRAPH_3:17
  e in the Edges of G & vs is_vertex_seq_of c &
  vs.len vs = (the Source of G).e
 implies
  c^<*e*> is Chain of G &
  ex vs' being FinSequence of the Vertices of G
   st vs' = vs^'<*(the Source of G).e, (the Target of G).e*> &
      vs' is_vertex_seq_of c^<*e*> & vs'.1 = vs.1 &
      vs'.len vs' = (the Target of G).e;

theorem :: GRAPH_3:18
  e in the Edges of G & vs is_vertex_seq_of c &
  vs.len vs = (the Target of G).e
 implies
  c^<*e*> is Chain of G &
  ex vs' being FinSequence of the Vertices of G
   st vs' = vs^'<*(the Target of G).e, (the Source of G).e*> &
      vs' is_vertex_seq_of c^<*e*> & vs'.1 = vs.1 &
      vs'.len vs' = (the Source of G).e;

theorem :: GRAPH_3:19
   vs is_vertex_seq_of c implies
  for n being Nat st n in dom c holds
      (vs.n = (the Target of G).(c.n) & vs.(n+1) = (the Source of G).(c.n) or
       vs.n = (the Source of G).(c.n) & vs.(n+1) = (the Target of G).(c.n));

theorem :: GRAPH_3:20
vs is_vertex_seq_of c & e in rng c implies
  (the Target of G).e in rng vs & (the Source of G).e in rng vs;

definition let G be Graph, X be set;
 redefine func G-VSet X -> Subset of the Vertices of G;
end;

theorem :: GRAPH_3:21
G-VSet {} = {};

theorem :: GRAPH_3:22
e in the Edges of G & e in X implies G-VSet X is non empty;

theorem :: GRAPH_3:23
 G is connected iff
  for v1, v2 st v1 <> v2 ex c, vs st c is non empty & vs is_vertex_seq_of c &
                                     vs.1 = v1 & vs.len vs = v2;

theorem :: GRAPH_3:24
 for G being connected Graph, X being set, v being Vertex of G
  st X meets the Edges of G & not v in G-VSet X
   ex v' being Vertex of G, e being Element of the Edges of G st
      v' in G-VSet X & not e in X &
      (v' = (the Target of G).e or v' = (the Source of G).e);

begin :: Degree of a vertex

definition let G be Graph, v be Vertex of G, X be set;
 func Edges_In(v, X) -> Subset of the Edges of G means
:: GRAPH_3:def 1
 for e being set holds
          e in it iff e in the Edges of G &
                        e in X & (the Target of G).e = v;

 func Edges_Out(v, X) -> Subset of the Edges of G means
:: GRAPH_3:def 2
 for e being set holds
          e in it iff e in the Edges of G &
                        e in X & (the Source of G).e = v;
end;

definition let G be Graph, v be Vertex of G, X be set;
 func Edges_At(v, X) -> Subset of the Edges of G equals
:: GRAPH_3:def 3
 Edges_In(v, X) \/ Edges_Out(v, X);
end;

definition let G be finite Graph, v be Vertex of G, X be set;
 cluster Edges_In(v, X) -> finite;
 cluster Edges_Out(v, X) -> finite;
 cluster Edges_At(v, X) -> finite;
end;

definition let G be Graph, v be Vertex of G, X be empty set;
 cluster Edges_In(v, X) -> empty;
 cluster Edges_Out(v, X) -> empty;
 cluster Edges_At(v, X) -> empty;
end;

definition let G be Graph, v be Vertex of G;
 func Edges_In v -> Subset of the Edges of G equals
:: GRAPH_3:def 4
 Edges_In(v, the Edges of G);

 func Edges_Out v -> Subset of the Edges of G equals
:: GRAPH_3:def 5
 Edges_Out(v, the Edges of G);
end;

theorem :: GRAPH_3:25
 Edges_In(v, X) c= Edges_In v;

theorem :: GRAPH_3:26
 Edges_Out(v, X) c= Edges_Out v;

definition let G be finite Graph, v be Vertex of G;
 cluster Edges_In v -> finite;
 cluster Edges_Out v -> finite;
end;

  reserve G for finite Graph,
          v for Vertex of G,
          c for Chain of G,
          vs for FinSequence of the Vertices of G,
          X1, X2 for set;

theorem :: GRAPH_3:27
 card Edges_In v = EdgesIn v;

theorem :: GRAPH_3:28
 card Edges_Out v = EdgesOut v;

definition let G be finite Graph, v be Vertex of G, X be set;
 func Degree(v, X) -> Nat equals
:: GRAPH_3:def 6
 card Edges_In(v, X) + card Edges_Out(v, X);
end;

theorem :: GRAPH_3:29
 Degree v = Degree(v, the Edges of G);

theorem :: GRAPH_3:30
 Degree(v, X) <> 0 implies Edges_At(v, X) is non empty;

theorem :: GRAPH_3:31
 e in the Edges of G & not e in X &
 (v = (the Target of G).e or v = (the Source of G).e)
  implies Degree v <> Degree(v, X);

theorem :: GRAPH_3:32
 X2 c= X1 implies
 card Edges_In(v, X1\X2) = card Edges_In(v, X1) - card Edges_In(v, X2);

theorem :: GRAPH_3:33
 X2 c= X1 implies
 card Edges_Out(v, X1\X2) = card Edges_Out(v, X1) - card Edges_Out(v, X2);

theorem :: GRAPH_3:34
 X2 c= X1 implies Degree(v, X1 \ X2) = Degree(v, X1) - Degree(v, X2);

theorem :: GRAPH_3:35
 Edges_In(v, X) = Edges_In(v, X/\the Edges of G) &
 Edges_Out(v, X) = Edges_Out(v, X/\the Edges of G);

theorem :: GRAPH_3:36
 Degree(v, X) = Degree(v, X/\the Edges of G);

theorem :: GRAPH_3:37
 c is non empty & vs is_vertex_seq_of c
  implies (v in rng vs iff Degree(v, rng c) <> 0);

theorem :: GRAPH_3:38
for G being non empty finite connected Graph, v being Vertex of G
 holds Degree v <> 0;

begin :: Adding an edge to a graph

definition let G be Graph, v1, v2 be Vertex of G;
 func AddNewEdge(v1, v2) -> strict Graph means
:: GRAPH_3:def 7
 the Vertices of it = the Vertices of G &
       the Edges of it = (the Edges of G) \/ {the Edges of G} &
       the Source of it = (the Source of G) +* ((the Edges of G) .--> v1) &
       the Target of it = (the Target of G) +* ((the Edges of G) .--> v2);
end;

definition let G be finite Graph, v1, v2 be Vertex of G;
 cluster AddNewEdge(v1, v2) -> finite;
end;

 reserve G for Graph,
         v, v1, v2 for Vertex of G,
         c for Chain of G,
         p for Path of G,
         vs for FinSequence of the Vertices of G,
         v' for Vertex of AddNewEdge(v1, v2),
         p' for Path of AddNewEdge(v1, v2),
         vs' for FinSequence of the Vertices of AddNewEdge(v1, v2);

theorem :: GRAPH_3:39
 (the Edges of G) in the Edges of AddNewEdge(v1, v2) &
 the Edges of G = (the Edges of AddNewEdge(v1, v2)) \ {the Edges of G} &
 (the Source of AddNewEdge(v1, v2)).(the Edges of G) = v1 &
 (the Target of AddNewEdge(v1, v2)).(the Edges of G) = v2;

theorem :: GRAPH_3:40
 e in the Edges of G
  implies (the Source of AddNewEdge(v1, v2)).e = (the Source of G).e &
          (the Target of AddNewEdge(v1, v2)).e = (the Target of G).e;

theorem :: GRAPH_3:41
 vs' = vs & vs is_vertex_seq_of c implies vs' is_vertex_seq_of c;

theorem :: GRAPH_3:42
  c is Chain of AddNewEdge(v1, v2);

theorem :: GRAPH_3:43
  p is Path of AddNewEdge(v1, v2);

theorem :: GRAPH_3:44
 v' = v1 & v1 <> v2 implies Edges_In(v', X) = Edges_In(v1, X);

theorem :: GRAPH_3:45
 v' = v2 & v1 <> v2 implies Edges_Out(v', X) = Edges_Out(v2, X);

theorem :: GRAPH_3:46
 v' = v1 & v1 <> v2 & (the Edges of G) in X
  implies Edges_Out(v', X) = Edges_Out(v1, X) \/ {the Edges of G} &
          Edges_Out(v1, X) misses {the Edges of G};

theorem :: GRAPH_3:47
 v' = v2 & v1 <> v2 & (the Edges of G) in X
  implies Edges_In(v', X) = Edges_In(v2, X) \/ {the Edges of G} &
          Edges_In(v2, X) misses {the Edges of G};

theorem :: GRAPH_3:48
 v' = v & v <> v1 & v <> v2 implies Edges_In(v', X) = Edges_In(v, X);

theorem :: GRAPH_3:49
 v' = v & v <> v1 & v <> v2 implies Edges_Out(v', X) = Edges_Out(v, X);

theorem :: GRAPH_3:50
 not (the Edges of G) in rng p' implies p' is Path of G;

theorem :: GRAPH_3:51
 not (the Edges of G) in rng p' & vs = vs' & vs' is_vertex_seq_of p'
   implies vs is_vertex_seq_of p';

definition let G be connected Graph, v1, v2 be Vertex of G;
 cluster AddNewEdge(v1, v2) -> connected;
end;

 reserve G for finite Graph,
         v, v1, v2 for Vertex of G,
         vs for FinSequence of the Vertices of G,
         v' for Vertex of AddNewEdge(v1, v2);

theorem :: GRAPH_3:52
 v' = v & v1 <> v2 & (v = v1 or v = v2) & (the Edges of G) in X
   implies Degree(v', X) = Degree(v, X) +1;

theorem :: GRAPH_3:53
 v' = v & v <> v1 & v <> v2 implies Degree(v', X) = Degree(v, X);

begin

theorem :: GRAPH_3:54  :: CycVerDeg1
for c being cyclic Path of G holds Degree(v, rng c) is even;

theorem :: GRAPH_3:55  :: CycVerDeg2
 for c being Path of G st c is non cyclic & vs is_vertex_seq_of c
   holds Degree(v, rng c) is even iff v <> vs.1 & v <> vs.len vs;

 reserve G for Graph,
         v for Vertex of G,
         vs for FinSequence of the Vertices of G;

definition let G be Graph;
 func G-CycleSet -> FinSequence-DOMAIN of the Edges of G means
:: GRAPH_3:def 8

 for x being set holds
  x in it iff x is cyclic Path of G;
end;

theorem :: GRAPH_3:56
 {} is Element of G-CycleSet;

theorem :: GRAPH_3:57
 for c being Element of G-CycleSet
  st v in G-VSet rng c holds
   { c' where c' is Element of G-CycleSet :
               rng c' = rng c &
               ex vs st vs is_vertex_seq_of c' & vs.1 = v}
     is non empty Subset of G-CycleSet;

definition let G, v; let c be Element of G-CycleSet;
   assume
 v in G-VSet rng c;
 func Rotate(c, v) -> Element of G-CycleSet equals
:: GRAPH_3:def 9
 choose
   { c' where c' is Element of G-CycleSet :
               rng c' = rng c &
               ex vs st vs is_vertex_seq_of c' & vs.1 = v };
end;

definition let G be Graph, c1, c2 be Element of G-CycleSet;
   assume that
 G-VSet rng c1 meets G-VSet rng c2 and
 rng c1 misses rng c2;
  func CatCycles(c1, c2) -> Element of G-CycleSet means
:: GRAPH_3:def 10

 ex v being Vertex of G
  st v = choose ((G-VSet rng c1) /\ (G-VSet rng c2)) &
     it = Rotate(c1, v)^Rotate(c2, v);
end;

theorem :: GRAPH_3:58
 for G being Graph, c1, c2 be Element of G-CycleSet
  st G-VSet rng c1 meets G-VSet rng c2 & rng c1 misses rng c2 &
     (c1 <> {} or c2 <> {})
   holds CatCycles(c1, c2) is non empty;

 reserve G for finite Graph,
         v for Vertex of G,
         vs for FinSequence of the Vertices of G;

definition let G, v; let X be set;
   assume that
 Degree(v, X) <> 0;
  func X-PathSet v -> FinSequence-DOMAIN of the Edges of G equals
:: GRAPH_3:def 11

  { c where c is Element of X* : c is Path of G & c is non empty &
             ex vs st vs is_vertex_seq_of c & vs.1 = v };
end;

theorem :: GRAPH_3:59
 for p being Element of X-PathSet v, Y being finite set
  st Y = the Edges of G & Degree(v, X) <> 0 holds len p <= card Y;

definition let G, v; let X be set;
   assume that
 for v being Vertex of G holds Degree(v, X) is even and
 Degree(v, X) <> 0;
  func X-CycleSet v -> non empty Subset of G-CycleSet equals
:: GRAPH_3:def 12

   { c where c is Element of G-CycleSet :
             rng c c= X & c is non empty &
             ex vs st vs is_vertex_seq_of c & vs.1 = v };
end;

theorem :: GRAPH_3:60
   Degree(v, X) <> 0 & (for v holds Degree(v, X) is even)
 implies
  for c being Element of X-CycleSet v
   holds c is non empty & rng c c= X & v in G-VSet rng c;

theorem :: GRAPH_3:61
 for G be finite connected Graph, c be Element of G-CycleSet
  st rng c <> the Edges of G & c is non empty
   holds {v' where v' is Vertex of G :
                   v' in G-VSet rng c & Degree v' <> Degree(v', rng c)}
           is non empty Subset of the Vertices of G;

definition let G be finite connected Graph,
               c be Element of G-CycleSet;
   assume that
 rng c <> the Edges of G and
 c is non empty;
 func ExtendCycle c -> Element of G-CycleSet means
:: GRAPH_3:def 13

 ex c' being Element of G-CycleSet, v being Vertex of G
  st v = choose {v' where v' is Vertex of G :
                    v' in G-VSet rng c & Degree v' <> Degree(v', rng c)} &
     c' = choose (((the Edges of G) \ rng c)-CycleSet v) &
     it = CatCycles(c, c');
end;

theorem :: GRAPH_3:62
 for G being finite connected Graph, c being Element of G-CycleSet
  st rng c <> the Edges of G & c is non empty &
     for v being Vertex of G holds Degree v is even
   holds ExtendCycle c is non empty &
         card rng c < card rng ExtendCycle c;

begin :: Euler paths

definition let G be Graph; let p be Path of G;
  attr p is Eulerian means
:: GRAPH_3:def 14
 rng p = the Edges of G;
end;

theorem :: GRAPH_3:63
for G being connected Graph, p being Path of G,
    vs being FinSequence of the Vertices of G
 st p is Eulerian & vs is_vertex_seq_of p
  holds rng vs = the Vertices of G;

theorem :: GRAPH_3:64  :: Cyclic Euler paths
for G being finite connected Graph holds
    (ex p being cyclic Path of G st p is Eulerian)
 iff
    (for v being Vertex of G holds Degree v is even);

theorem :: GRAPH_3:65 :: Non-cyclic Euler paths
  for G being finite connected Graph holds
    (ex p being Path of G st p is non cyclic & p is Eulerian)
 iff
    (ex v1, v2 being Vertex of G st v1 <> v2 &
      for v being Vertex of G holds Degree v is even iff v<>v1 & v <> v2);