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

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;

:: Seven Bridges of Koenigsberg

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;