:: A Note on the Seven Bridges of K\"onigsberg Problem
:: by Adam Naumowicz
::
:: Received June 16, 2014
:: Copyright (c) 2014-2016 Association of Mizar Users

environ

vocabularies HIDDEN, NUMBERS, XBOOLE_0, FINSEQ_1, ABIAN, 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, ZFMISC_1, GRAPH_3, FUNCT_2, GRAPH_3A;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, NUMBERS, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, CARD_1, NAT_1, FINSEQ_1, FINSEQ_4, STRUCT_0, GRAPH_1, GRAPH_2, MSSCYC_1, ABIAN, XXREAL_0, GRAPH_3;
definitions TARSKI, FUNCT_1, GRAPH_2, XBOOLE_0;
theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, NAT_1, PARTFUN1, CARD_1, CARD_2, FINSEQ_1, FINSEQ_3, XBOOLE_0, XXREAL_0, XTUPLE_0, GRAPH_3, POLYFORM, ENUMSET1;
schemes ;
registrations XBOOLE_0, FINSET_1, XREAL_0, NAT_1, CARD_1, MEMBERED, FINSEQ_1, STRUCT_0, RELSET_1, SUBSET_1;
constructors HIDDEN, FINSEQ_4, ABIAN, MSSCYC_1, RELSET_1, PRE_POLY, GRAPH_3, ENUMSET1;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities GRAPH_3, FINSEQ_1;
expansions GRAPH_1;


definition
func KVertices -> set equals :: GRAPH_3A:def 1
{0,1,2,3};
correctness
coherence
{0,1,2,3} is set ;
;
func KEdges -> set equals :: GRAPH_3A:def 2
{10,20,30,40,50,60,70};
correctness
coherence
{10,20,30,40,50,60,70} is set ;
;
end;

:: deftheorem defines KVertices GRAPH_3A:def 1 :
KVertices = {0,1,2,3};

:: deftheorem defines KEdges GRAPH_3A:def 2 :
KEdges = {10,20,30,40,50,60,70};

definition
func KSource -> Function of KEdges,KVertices equals :: GRAPH_3A:def 3
{[10,0],[20,0],[30,0],[40,1],[50,1],[60,2],[70,2]};
correctness
coherence
{[10,0],[20,0],[30,0],[40,1],[50,1],[60,2],[70,2]} is Function of KEdges,KVertices;
proof end;
func KTarget -> Function of KEdges,KVertices equals :: GRAPH_3A:def 4
{[10,1],[20,2],[30,3],[40,2],[50,2],[60,3],[70,3]};
correctness
coherence
{[10,1],[20,2],[30,3],[40,2],[50,2],[60,3],[70,3]} is Function of KEdges,KVertices;
proof end;
end;

:: deftheorem defines KSource GRAPH_3A:def 3 :
KSource = {[10,0],[20,0],[30,0],[40,1],[50,1],[60,2],[70,2]};

:: deftheorem defines KTarget GRAPH_3A:def 4 :
KTarget = {[10,1],[20,2],[30,3],[40,2],[50,2],[60,3],[70,3]};

definition
func KoenigsbergBridges -> Graph equals :: GRAPH_3A:def 5
 MultiGraphStruct(# KVertices,KEdges,KSource,KTarget #);
correctness
coherence
MultiGraphStruct(# KVertices,KEdges,KSource,KTarget #) is Graph;
;
end;

:: deftheorem defines KoenigsbergBridges GRAPH_3A:def 5 :
KoenigsbergBridges = MultiGraphStruct(# KVertices,KEdges,KSource,KTarget #);

registration
cluster KoenigsbergBridges -> connected finite ;
correctness
coherence
( KoenigsbergBridges is finite & KoenigsbergBridges is connected );
proof end;
end;

theorem d0: :: GRAPH_3A:1
for v being Vertex of KoenigsbergBridges st v = 0 holds
Degree v = 3
proof end;

theorem d1: :: GRAPH_3A:2
for v being Vertex of KoenigsbergBridges st v = 1 holds
Degree v = 3
proof end;

theorem :: GRAPH_3A:3
for v being Vertex of KoenigsbergBridges st v = 2 holds
Degree v = 5
proof end;

theorem d3: :: GRAPH_3A:4
for v being Vertex of KoenigsbergBridges st v = 3 holds
Degree v = 3
proof end;

theorem :: GRAPH_3A:5
for p being Path of KoenigsbergBridges holds
( not p is cyclic or not p is Eulerian )
proof end;

theorem :: GRAPH_3A:6
for p being Path of KoenigsbergBridges holds
( p is cyclic or not p is Eulerian )
proof end;