:: Euler circuits and paths
:: by Yatsuka Nakamura and Piotr Rudnicki
::
:: Received July 29, 1997
:: Copyright (c) 1997-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, FINSEQ_2, XBOOLE_0, SUBSET_1, FINSEQ_1, ABIAN, INT_1,
ARYTM_1, RELAT_1, XXREAL_0, ARYTM_3, GRAPH_2, FUNCT_1, CARD_1, GRAPH_1,
GLIB_000, STRUCT_0, TREES_2, ORDINAL4, NAT_1, PARTFUN1, TARSKI, RELAT_2,
FINSET_1, FUNCT_4, FUNCOP_1, ZFMISC_1, FINSEQ_6, GRAPH_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, FUNCT_4, INT_1,
NAT_1, FINSET_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, XXREAL_2, STRUCT_0,
GRAPH_1, GRAPH_2, MSSCYC_1, ABIAN, XXREAL_0;
constructors WELLORD2, FUNCT_4, FINSEQ_4, ABIAN, GRAPH_2, MSSCYC_1, XXREAL_2,
RELSET_1, PRE_POLY;
registrations XBOOLE_0, ORDINAL1, FUNCOP_1, FINSET_1, XXREAL_0, XREAL_0,
NAT_1, INT_1, CARD_1, MEMBERED, FINSEQ_1, ABIAN, GRAPH_2, MSSCYC_1,
RELAT_1, XXREAL_2, STRUCT_0, RELSET_1, FINSEQ_2;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin :: Preliminaries
definition
let D be set, T be non empty FinSequenceSet of D,
S be non empty Subset of T;
redefine mode Element of S -> FinSequence of D;
end;
registration
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 carrier 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 carrier 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;
theorem :: GRAPH_3:4
e in the carrier' of G implies <*e*> is Path of G;
theorem :: GRAPH_3:5
(m,n)-cut p is Path of G;
theorem :: GRAPH_3:6
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;
theorem :: GRAPH_3:7
c = {} implies c is cyclic;
registration
let G be Graph;
cluster cyclic for Path of G;
end;
theorem :: GRAPH_3:8
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:9
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:10
for p being cyclic Path of G st n in dom p ex p9 being cyclic
Path of G st p9.1 = p.n & len p9 = len p & rng p9 = rng p;
theorem :: GRAPH_3:11 :: 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:12
e in the carrier' of G & vs is_vertex_seq_of c & vs.len vs = (
the Source of G).e implies c^<*e*> is Chain of G & ex vs9 being FinSequence of
the carrier of G st vs9 = vs^'<*(the Source of G).e, (the Target of G).e*> &
vs9 is_vertex_seq_of c^<*e*> & vs9.1 = vs.1 & vs9.len vs9 = (the Target of G).e
;
theorem :: GRAPH_3:13
e in the carrier' of G & vs is_vertex_seq_of c & vs.len vs = (
the Target of G).e implies c^<*e*> is Chain of G & ex vs9 being FinSequence of
the carrier of G st vs9 = vs^'<*(the Target of G).e, (the Source of G).e*> &
vs9 is_vertex_seq_of c^<*e*> & vs9.1 = vs.1 & vs9.len vs9 = (the Source of G).e
;
theorem :: GRAPH_3:14
vs is_vertex_seq_of c implies for n being Element of 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:15
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 carrier of G;
end;
theorem :: GRAPH_3:16
G-VSet {} = {};
theorem :: GRAPH_3:17
e in the carrier' of G & e in X implies G-VSet X is non empty;
theorem :: GRAPH_3:18
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:19
for G being connected Graph, X being set, v being Vertex of G st
X meets the carrier' of G & not v in G-VSet X ex v9 being Vertex of G, e being
Element of the carrier' of G st v9 in G-VSet X & not e in X & (v9 = (the Target
of G).e or v9 = (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 carrier' of G means
:: GRAPH_3:def 1
for e being
set holds e in it iff e in the carrier' of G & e in X & (the Target of G).e = v
;
func Edges_Out(v, X) -> Subset of the carrier' of G means
:: GRAPH_3:def 2
for e being
set holds e in it iff e in the carrier' 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 carrier' of G equals
:: GRAPH_3:def 3
Edges_In(v, X) \/
Edges_Out(v, X);
end;
registration
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;
registration
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 carrier' of G equals
:: GRAPH_3:def 4
Edges_In(v, the
carrier' of G);
func Edges_Out v -> Subset of the carrier' of G equals
:: GRAPH_3:def 5
Edges_Out(v, the
carrier' of G);
end;
theorem :: GRAPH_3:20
Edges_In(v, X) c= Edges_In v;
theorem :: GRAPH_3:21
Edges_Out(v, X) c= Edges_Out v;
registration
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 carrier of G,
X1, X2 for set;
theorem :: GRAPH_3:22
card Edges_In v = EdgesIn v;
theorem :: GRAPH_3:23
card Edges_Out v = EdgesOut v;
definition
let G be finite Graph, v be Vertex of G, X be set;
func Degree(v, X) -> Element of NAT equals
:: GRAPH_3:def 6
card Edges_In(v, X) + card
Edges_Out(v, X);
end;
theorem :: GRAPH_3:24
Degree v = Degree(v, the carrier' of G);
theorem :: GRAPH_3:25
Degree(v, X) <> 0 implies Edges_At(v, X) is non empty;
theorem :: GRAPH_3:26
e in the carrier' 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:27
X2 c= X1 implies card Edges_In(v, X1\X2) = card Edges_In(v, X1)
- card Edges_In(v, X2);
theorem :: GRAPH_3:28
X2 c= X1 implies card Edges_Out(v, X1\X2) = card Edges_Out(v, X1
) - card Edges_Out(v, X2);
theorem :: GRAPH_3:29
X2 c= X1 implies Degree(v, X1 \ X2) = Degree(v, X1) - Degree(v, X2);
theorem :: GRAPH_3:30
Edges_In(v, X) = Edges_In(v, X/\the carrier' of G) & Edges_Out(v
, X) = Edges_Out(v, X/\the carrier' of G);
theorem :: GRAPH_3:31
Degree(v, X) = Degree(v, X/\the carrier' of G);
theorem :: GRAPH_3:32
c is non empty & vs is_vertex_seq_of c implies (v in rng vs iff
Degree(v, rng c) <> 0);
theorem :: GRAPH_3:33
for G being non void 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 carrier of it = the
carrier of G & the carrier' of it = (the carrier' of G) \/ {the carrier' of G}
& the Source of it = (the Source of G) +* ((the carrier' of G) .--> v1) & the
Target of it = (the Target of G) +* ((the carrier' of G) .--> v2);
end;
registration
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 carrier of G,
v9 for Vertex of AddNewEdge(v1, v2),
p9 for Path of AddNewEdge(v1, v2),
vs9 for FinSequence of the carrier of AddNewEdge(v1, v2);
theorem :: GRAPH_3:34
(the carrier' of G) in the carrier' of AddNewEdge(v1, v2) & the
carrier' of G = (the carrier' of AddNewEdge(v1, v2)) \ {the carrier' of G} & (
the Source of AddNewEdge(v1, v2)).(the carrier' of G) = v1 & (the Target of
AddNewEdge(v1, v2)).(the carrier' of G) = v2;
theorem :: GRAPH_3:35
e in the carrier' 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:36
vs9 = vs & vs is_vertex_seq_of c implies vs9 is_vertex_seq_of c;
theorem :: GRAPH_3:37
c is Chain of AddNewEdge(v1, v2);
theorem :: GRAPH_3:38
p is Path of AddNewEdge(v1, v2);
theorem :: GRAPH_3:39
v9 = v1 & v1 <> v2 implies Edges_In(v9, X) = Edges_In(v1, X);
theorem :: GRAPH_3:40
v9 = v2 & v1 <> v2 implies Edges_Out(v9, X) = Edges_Out(v2, X);
theorem :: GRAPH_3:41
v9 = v1 & (the carrier' of G) in X implies Edges_Out(v9, X) =
Edges_Out(v1, X) \/ {the carrier' of G} & Edges_Out(v1, X) misses {the carrier'
of G};
theorem :: GRAPH_3:42
v9 = v2 & (the carrier' of G) in X implies Edges_In(v9, X) =
Edges_In(v2, X) \/ {the carrier' of G} & Edges_In(v2, X) misses {the carrier'
of G};
theorem :: GRAPH_3:43
v9 = v & v <> v2 implies Edges_In(v9, X) = Edges_In(v, X);
theorem :: GRAPH_3:44
v9 = v & v <> v1 implies Edges_Out(v9, X) = Edges_Out(v, X);
theorem :: GRAPH_3:45
not (the carrier' of G) in rng p9 implies p9 is Path of G;
theorem :: GRAPH_3:46
not (the carrier' of G) in rng p9 & vs = vs9 & vs9
is_vertex_seq_of p9 implies vs is_vertex_seq_of p9;
registration
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 carrier of G,
v9 for Vertex of AddNewEdge(v1, v2);
theorem :: GRAPH_3:47
v9 = v & v1 <> v2 & (v = v1 or v = v2) & (the carrier' of G) in
X implies Degree(v9, X) = Degree(v, X) +1;
theorem :: GRAPH_3:48
v9 = v & v <> v1 & v <> v2 implies Degree(v9, X) = Degree(v, X);
begin
theorem :: GRAPH_3:49 :: CycVerDeg1
for c being cyclic Path of G holds Degree(v, rng c) is even;
theorem :: GRAPH_3:50 :: 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 carrier of G;
definition
let G be Graph;
func G-CycleSet -> FinSequenceSet of the carrier' 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:51
{} in G-CycleSet;
registration let G be Graph;
cluster G-CycleSet -> non empty;
end;
theorem :: GRAPH_3:52
for c being Element of G-CycleSet st v in G-VSet rng c holds {
c9 where c9 is Element of G-CycleSet : rng c9 = rng c & ex vs st vs
is_vertex_seq_of c9 & 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
the Element of { c9 where
c9 is Element of G-CycleSet : rng c9 = rng c & ex vs st vs is_vertex_seq_of c9
& 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 = the Element of (G-VSet rng c1) /\ (G-VSet rng c2) &
it = Rotate(c1
, v)^Rotate(c2, v);
end;
theorem :: GRAPH_3:53
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 carrier of G;
definition
let G, v;
let X be set;
assume
Degree(v, X) <> 0;
func X-PathSet v -> non empty FinSequenceSet of the carrier' 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:54
for p being Element of X-PathSet v, Y being finite set st Y =
the carrier' 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:55
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:56
for G be finite connected Graph, c be Element of G-CycleSet st
rng c <> the carrier' of G & c is non empty holds {v9 where v9 is Vertex of G :
v9 in G-VSet rng c & Degree v9 <> Degree(v9, rng c)} is non empty Subset of the
carrier of G;
definition
let G be finite connected Graph, c be Element of G-CycleSet;
assume that
rng c <> the carrier' of G and
c is non empty;
func ExtendCycle c -> Element of G-CycleSet means
:: GRAPH_3:def 13
ex c9 being
Element of G-CycleSet, v being Vertex of G st
v = the Element of {v9 where v9 is Vertex
of G : v9 in G-VSet rng c & Degree v9 <> Degree(v9, rng c)} & c9
= the Element of ((
the carrier' of G) \ rng c)-CycleSet v & it = CatCycles(c, c9);
end;
theorem :: GRAPH_3:57
for G being finite connected Graph, c being Element of G
-CycleSet st rng c <> the carrier' 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 carrier' of G;
end;
theorem :: GRAPH_3:58
for G being connected Graph, p being Path of G, vs being
FinSequence of the carrier of G st p is Eulerian & vs is_vertex_seq_of p holds
rng vs = the carrier of G;
theorem :: GRAPH_3:59 :: 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:60 :: 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;