:: Proof of Dijkstra's Shortest Path Algorithm & Prim's Minimum Spanning
:: Tree Algorithm
:: by Gilbert Lee and Piotr Rudnicki
::
:: Received February 22, 2005
:: Copyright (c) 2005-2018 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, FUNCT_1, RELAT_1, FUNCT_4, FUNCOP_1, XBOOLE_0, PRE_POLY,
TARSKI, CARD_1, UPROOTS, CARD_3, ARYTM_3, FINSEQ_1, NAT_1, XXREAL_0,
FINSET_1, SUBSET_1, FINSEQ_2, ARYTM_1, GLIB_003, TREES_1, GLIB_000,
GLIB_001, REAL_1, PBOOLE, ZFMISC_1, FUNCT_2, ABIAN, PARTFUN1, MCART_1,
GLIB_002, WAYBEL_0, RELAT_2, RCOMP_1, GRAPH_1, GLIB_004;
notations TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, XTUPLE_0, XFAMILY, CARD_1,
ORDINAL1, NUMBERS, SUBSET_1, DOMAIN_1, MCART_1, XCMPLX_0, XXREAL_0,
XREAL_0, RELAT_1, RELSET_1, PARTFUN1, FUNCT_1, FINSEQ_1, FINSEQ_2,
PBOOLE, FUNCT_2, RVSUM_1, ABIAN, UPROOTS, FINSET_1, NAT_1, FUNCOP_1,
FUNCT_4, GLIB_000, GLIB_001, GLIB_002, GLIB_003, RFUNCT_3, PRE_POLY;
constructors DOMAIN_1, BINOP_2, FINSOP_1, RVSUM_1, GRAPH_2, RFUNCT_3, UPROOTS,
GLIB_002, GLIB_003, XXREAL_2, RELSET_1, XTUPLE_0, WSIERP_1, XFAMILY,
FINSEQ_6;
registrations XBOOLE_0, SUBSET_1, RELAT_1, PARTFUN1, FRAENKEL, FUNCT_1,
ORDINAL1, FUNCOP_1, FINSET_1, NUMBERS, XREAL_0, NAT_1, CARD_1, GLIB_000,
ABIAN, GLIB_001, GLIB_002, GLIB_003, VALUED_0, RELSET_1, PRE_POLY, INT_1,
FINSEQ_1, XTUPLE_0, FINSEQ_2;
requirements ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
begin
theorem :: GLIB_004:1
for f, g being Function holds support (f +* g) c= support f \/ support g;
theorem :: GLIB_004:2
for f being Function, x, y being object holds
support (f +* (x.-->y)) c= support f \/ {x};
theorem :: GLIB_004:3
for A,B being set, b being Rbag of A, b1 being Rbag of B, b2
being Rbag of A\B st b = b1 +* b2 holds Sum b = Sum b1 + Sum b2;
theorem :: GLIB_004:4
for X,x being set, b being Rbag of X st dom b = {x} holds Sum b = b.x;
theorem :: GLIB_004:5
for A being set, b1,b2 being Rbag of A st (for x being set st x
in A holds b1.x <= b2.x) holds Sum b1 <= Sum b2;
theorem :: GLIB_004:6
for A being set, b1,b2 being Rbag of A st (for x being set st x in A
holds b1.x = b2.x) holds Sum b1 = Sum b2;
theorem :: GLIB_004:7
for A1,A2 being set, b1 being Rbag of A1, b2 being Rbag of A2 st b1 =
b2 holds Sum b1 = Sum b2;
theorem :: GLIB_004:8
for X, x being set, b being Rbag of X, y being Real st b =
(EmptyBag X) +* (x.-->y) holds Sum b = y;
theorem :: GLIB_004:9
for X, x being set, b1, b2 being Rbag of X, y being Real st b2
= b1 +* (x.-->y) holds Sum b2 = Sum b1 + y - b1.x;
begin :: Graph preliminaries
definition
let G1 be real-weighted WGraph, G2 be WSubgraph of G1, v be set;
pred G2 is_mincost_DTree_rooted_at v means
:: GLIB_004:def 1
G2 is Tree-like & for x
being Vertex of G2 holds ex W2 being DPath of G2 st W2 is_Walk_from v,x & for
W1 being DPath of G1 st W1 is_Walk_from v,x holds W2.cost() <= W1.cost();
end;
definition
let G be real-weighted WGraph, W be DPath of G, x,y be set;
pred W is_mincost_DPath_from x,y means
:: GLIB_004:def 2
W is_Walk_from x,y & for W2
being DPath of G st W2 is_Walk_from x,y holds W.cost() <= W2.cost();
end;
definition
let G be finite real-weighted WGraph, x,y be set;
func G.min_DPath_cost(x,y) -> Real means
:: GLIB_004:def 3
ex W being DPath of G st W
is_mincost_DPath_from x,y & it = W.cost() if ex W being DWalk of G st W
is_Walk_from x,y otherwise it = 0;
end;
definition
func WGraphSelectors -> non empty finite Subset of NAT equals
:: GLIB_004:def 4
{
VertexSelector, EdgeSelector, SourceSelector, TargetSelector, WeightSelector};
end;
registration
let G be WGraph;
cluster G|(WGraphSelectors) -> [Graph-like] [Weighted];
end;
definition
let G be WGraph;
func G.allWSubgraphs() -> non empty set means
:: GLIB_004:def 5
for x being set holds x
in it iff ex G2 being WSubgraph of G st x = G2 & dom G2 = WGraphSelectors;
end;
registration
let G be finite WGraph;
cluster G.allWSubgraphs() -> finite;
end;
definition
let G be WGraph, X be non empty Subset of G.allWSubgraphs();
redefine mode Element of X -> WSubgraph of G;
end;
definition
let G be finite real-weighted WGraph;
func G.cost() -> Real equals
:: GLIB_004:def 6
Sum the_Weight_of G;
end;
theorem :: GLIB_004:10
for G1 being finite real-weighted WGraph, e being set, G2 being
weight-inheriting [Weighted] removeEdge of G1,e st e in the_Edges_of G1 holds
G1.cost() = G2.cost() + (the_Weight_of G1).e;
theorem :: GLIB_004:11
for G being finite real-weighted WGraph, V1 being non empty
Subset of the_Vertices_of G, E1 being Subset of G.edgesBetween(V1), G1 being
inducedWSubgraph of G,V1,E1, e being set, G2 being inducedWSubgraph of G,V1,E1
\/ {e} st not e in E1 & e in G.edgesBetween(V1) holds G1.cost() + (
the_Weight_of G).e = G2.cost();
theorem :: GLIB_004:12
for G being finite nonnegative-weighted WGraph, W being DPath of
G, x,y being set, m,n being Element of NAT st W is_mincost_DPath_from x,y holds
W.cut(m,n) is_mincost_DPath_from W.cut(m,n).first(),W.cut(m,n).last();
theorem :: GLIB_004:13
for G being finite real-weighted WGraph, W1,W2 being DPath of G, x,y
being set st W1 is_mincost_DPath_from x,y & W2 is_mincost_DPath_from x,y holds
W1.cost() = W2.cost();
theorem :: GLIB_004:14
for G being finite real-weighted WGraph, W being DPath of G, x,y
being set st W is_mincost_DPath_from x,y holds G.min_DPath_cost(x,y) = W.cost()
;
begin :: Definitions for Dijkstra's Shortest Path Algorithm
definition
let G be _Graph;
mode DIJK:Labeling of G is Element of [: PFuncs(the_Vertices_of G, REAL),
bool the_Edges_of G :];
end;
definition
let X1,X3 be set, X2 be non empty set;
let x be Element of [: PFuncs(X1,X3),X2 :];
redefine func x`1 -> Element of PFuncs(X1,X3);
end;
registration
let G be finite _Graph, L be DIJK:Labeling of G;
cluster L`1 -> finite for set;
cluster L`2 -> finite for set;
end;
definition
let G be real-weighted WGraph, L be DIJK:Labeling of G;
func DIJK:NextBestEdges(L) -> Subset of the_Edges_of G means
:: GLIB_004:def 7
for e1
being set holds e1 in it iff e1 DSJoins dom (L`1), the_Vertices_of G \ dom (L`1
), G & for e2 being set st e2 DSJoins dom (L`1), the_Vertices_of G \ dom (L`1),
G holds (L`1).((the_Source_of G).e1) + (the_Weight_of G).e1 <= (L`1).((
the_Source_of G).e2) + (the_Weight_of G).e2;
end;
definition
let G be real-weighted WGraph, L be DIJK:Labeling of G;
func DIJK:Step(L) -> DIJK:Labeling of G equals
:: GLIB_004:def 8
L if
DIJK:NextBestEdges(L) = {} otherwise [ L`1+*((the_Target_of G).
(the Element of
DIJK:NextBestEdges(L)) .--> ((L`1).((the_Source_of G).(the Element of
DIJK:NextBestEdges(L))) + (the_Weight_of G).
(the Element of DIJK:NextBestEdges(L)))), L
`2 \/ {the Element of DIJK:NextBestEdges(L)} ];
end;
definition
let G be real-weighted WGraph, src be Vertex of G;
func DIJK:Init(src) -> DIJK:Labeling of G equals
:: GLIB_004:def 9
[src .--> 0, {}];
end;
definition
let G be real-weighted WGraph;
mode DIJK:LabelingSeq of G -> ManySortedSet of NAT means
:: GLIB_004:def 10
for n being Nat holds it.n is DIJK:Labeling of G;
end;
definition
let G be real-weighted WGraph, S be DIJK:LabelingSeq of G, n be Nat;
redefine func S.n -> DIJK:Labeling of G;
end;
definition
let G be real-weighted WGraph, src be Vertex of G;
func DIJK:CompSeq(src) -> DIJK:LabelingSeq of G means
:: GLIB_004:def 11
it.0 = DIJK:Init(src) & for n being Nat holds it.(n+1) = DIJK:Step(it.n);
end;
definition
let G be real-weighted WGraph, src be Vertex of G;
func DIJK:SSSP(G,src) -> DIJK:Labeling of G equals
:: GLIB_004:def 12
DIJK:CompSeq(src)
.Result();
end;
begin :: Dijkstra's Algorithm Theorems
theorem :: GLIB_004:15
for G being finite real-weighted WGraph, L be DIJK:Labeling of G
holds (card dom (DIJK:Step(L))`1 = card dom L`1 iff DIJK:NextBestEdges(L) = {})
& (card dom (DIJK:Step(L))`1 = card dom L`1 + 1 iff DIJK:NextBestEdges(L)<>{});
theorem :: GLIB_004:16
for G being real-weighted WGraph, L be DIJK:Labeling of G holds
dom L`1 c= dom (DIJK:Step(L))`1 & L`2 c= (DIJK:Step(L))`2;
theorem :: GLIB_004:17
for G being real-weighted WGraph, src be Vertex of G holds dom (
(DIJK:Init(src))`1) = {src};
theorem :: GLIB_004:18
for G being real-weighted WGraph, src being Vertex of G, i,j
being Nat st i <= j holds dom ((DIJK:CompSeq(src).i))`1 c= dom (DIJK:CompSeq(
src).j)`1 & (DIJK:CompSeq(src).i)`2 c= (DIJK:CompSeq(src).j)`2;
theorem :: GLIB_004:19
for G being finite real-weighted WGraph, src being Vertex of G,
n being Nat holds dom (DIJK:CompSeq(src).n)`1 c= G.reachableDFrom(src);
theorem :: GLIB_004:20
for G being finite real-weighted WGraph, src being Vertex of G,
n being Nat holds DIJK:NextBestEdges(DIJK:CompSeq(src).n) = {} iff dom (
DIJK:CompSeq(src).n)`1 = G.reachableDFrom(src);
theorem :: GLIB_004:21
for G being finite real-weighted WGraph, s being Vertex of G, n
being Nat holds card dom (DIJK:CompSeq(s).n)`1 = min(n+1, card(G.reachableDFrom
(s)));
theorem :: GLIB_004:22
for G being finite real-weighted WGraph, src being Vertex of G,
n being Nat holds (DIJK:CompSeq(src).n)`2 c= G.edgesBetween(dom (DIJK:CompSeq(
src).n)`1);
theorem :: GLIB_004:23
for G being finite nonnegative-weighted WGraph, s being Vertex
of G, n being Nat, G2 being inducedWSubgraph of G, dom (DIJK:CompSeq(s).n)`1, (
DIJK:CompSeq(s).n)`2 holds G2 is_mincost_DTree_rooted_at s & for v being Vertex
of G st v in dom (DIJK:CompSeq(s).n)`1 holds G.min_DPath_cost(s,v) = (
DIJK:CompSeq(s).n)`1.v;
theorem :: GLIB_004:24
for G being finite real-weighted WGraph, s being Vertex of G
holds DIJK:CompSeq(s) is halting;
registration
let G be finite real-weighted WGraph, src be Vertex of G;
cluster DIJK:CompSeq(src) -> halting;
end;
theorem :: GLIB_004:25
for G being finite real-weighted WGraph, s being Vertex of G
holds DIJK:CompSeq(s).Lifespan() + 1 = card G.reachableDFrom(s);
theorem :: GLIB_004:26
for G being finite real-weighted WGraph, s being Vertex of G
holds dom (DIJK:SSSP(G,s))`1 = G.reachableDFrom(s);
::$N Dijkstra's shortest path algorithm
theorem :: GLIB_004:27
for G being finite nonnegative-weighted WGraph, s being Vertex of G,
G2 being inducedWSubgraph of G, dom (DIJK:SSSP(G,s))`1, DIJK:SSSP(G,s)`2 holds
G2 is_mincost_DTree_rooted_at s & for v being Vertex of G st v in G
.reachableDFrom(s) holds v in the_Vertices_of G2 & G.min_DPath_cost(s,v) = (
DIJK:SSSP(G,s))`1.v;
begin :: Prim's Algorithm definitions
definition
let G be _Graph;
mode PRIM:Labeling of G is Element of [: bool the_Vertices_of G, bool
the_Edges_of G :];
end;
registration
let G be finite _Graph, L be PRIM:Labeling of G;
cluster L`1 -> finite for set;
cluster L`2 -> finite for set;
end;
definition
let G be real-weighted WGraph, L being PRIM:Labeling of G;
func PRIM:NextBestEdges(L) -> Subset of the_Edges_of G means
:: GLIB_004:def 13
for e1
being set holds e1 in it iff e1 SJoins L`1, the_Vertices_of G \ L`1, G & for e2
being set st e2 SJoins L`1, the_Vertices_of G \ L`1, G holds (the_Weight_of G).
e1 <= (the_Weight_of G).e2;
end;
definition
let G be real-weighted WGraph;
func PRIM:Init(G) -> PRIM:Labeling of G equals
:: GLIB_004:def 14
[ {the Element of the_Vertices_of G}, {} ];
end;
definition
let G be real-weighted WGraph, L being PRIM:Labeling of G;
func PRIM:Step(L) -> PRIM:Labeling of G equals
:: GLIB_004:def 15
L if
PRIM:NextBestEdges(L) = {}, [ L`1 \/ {(the_Target_of G).(the Element of
PRIM:NextBestEdges(L))}, L`2 \/ {the Element of PRIM:NextBestEdges(L)} ] if
PRIM:NextBestEdges(L) <> {} & (the_Source_of G).
(the Element of PRIM:NextBestEdges(L))
in L`1 otherwise [ L`1 \/ {(the_Source_of G).
(the Element of PRIM:NextBestEdges(L))}, L
`2 \/ {the Element of PRIM:NextBestEdges(L)} ];
end;
definition
let G be real-weighted WGraph;
mode PRIM:LabelingSeq of G -> ManySortedSet of NAT means
:: GLIB_004:def 16
for n being Nat holds it.n is PRIM:Labeling of G;
end;
definition
let G be real-weighted WGraph, S be PRIM:LabelingSeq of G, n be Nat;
redefine func S.n -> PRIM:Labeling of G;
end;
definition
let G be real-weighted WGraph;
func PRIM:CompSeq(G) -> PRIM:LabelingSeq of G means
:: GLIB_004:def 17
it.0 = PRIM:Init (G) & for n being Nat holds it.(n+1) = PRIM:Step(it.n);
end;
definition
let G be real-weighted WGraph;
func PRIM:MST(G) -> PRIM:Labeling of G equals
:: GLIB_004:def 18
PRIM:CompSeq(G).Result();
end;
theorem :: GLIB_004:28
for G being real-weighted WGraph, L be PRIM:Labeling of G st
PRIM:NextBestEdges(L) <> {} holds ex v being Vertex of G st not v in L`1 &
PRIM:Step(L) = [ L`1 \/ {v},
L`2 \/ {the Element of PRIM:NextBestEdges(L)} ];
theorem :: GLIB_004:29
for G being real-weighted WGraph, L be PRIM:Labeling of G holds
L`1 c= (PRIM:Step(L))`1 & L`2 c= (PRIM:Step(L))`2;
theorem :: GLIB_004:30
for G being finite real-weighted WGraph, n being Nat holds (
PRIM:CompSeq(G).n)`1 is non empty Subset of the_Vertices_of G & (PRIM:CompSeq(G
).n)`2 c= G.edgesBetween((PRIM:CompSeq(G).n)`1);
theorem :: GLIB_004:31
for G1 being finite real-weighted WGraph, n being Nat, G2 being
inducedSubgraph of G1,(PRIM:CompSeq(G1).n)`1, (PRIM:CompSeq(G1).n)`2 holds G2
is connected;
theorem :: GLIB_004:32
for G1 being finite real-weighted WGraph, n being Nat, G2 being
inducedSubgraph of G1, (PRIM:CompSeq(G1).n)`1 holds G2 is connected;
registration
let G1 be finite real-weighted WGraph, n being Nat;
cluster -> connected for inducedSubgraph of G1,(PRIM:CompSeq(G1).n)`1;
end;
registration
let G1 be finite real-weighted WGraph, n being Nat;
cluster -> connected for inducedSubgraph of G1, (PRIM:CompSeq(G1).n)`1, (
PRIM:CompSeq(G1).n)`2;
end;
theorem :: GLIB_004:33
for G being finite real-weighted WGraph, n being Nat holds (
PRIM:CompSeq(G).n)`1 c= G.reachableFrom(the Element of the_Vertices_of G);
theorem :: GLIB_004:34
for G being finite real-weighted WGraph, i,j being Nat st i <= j
holds (PRIM:CompSeq(G).i)`1 c= (PRIM:CompSeq(G).j)`1 & (PRIM:CompSeq(G).i)`2 c=
(PRIM:CompSeq(G).j)`2;
theorem :: GLIB_004:35
for G being finite real-weighted WGraph, n being Nat holds
PRIM:NextBestEdges(PRIM:CompSeq(G).n) = {} iff (PRIM:CompSeq(G).n)`1 = G
.reachableFrom(the Element of the_Vertices_of G);
theorem :: GLIB_004:36
for G being finite real-weighted WGraph, n being Nat holds card
((PRIM:CompSeq(G).n)`1) = min(n+1,
card(G.reachableFrom(the Element of the_Vertices_of
G)));
theorem :: GLIB_004:37
for G being finite real-weighted WGraph holds PRIM:CompSeq(G) is
halting & PRIM:CompSeq(G).Lifespan() + 1
= card G.reachableFrom(the Element of
the_Vertices_of G);
theorem :: GLIB_004:38
for G1 being finite real-weighted WGraph, n being Nat, G2 being
inducedSubgraph of G1, (PRIM:CompSeq(G1).n)`1, (PRIM:CompSeq(G1).n)`2 holds G2
is Tree-like;
theorem :: GLIB_004:39
for G being finite connected real-weighted WGraph holds (
PRIM:MST(G))`1 = the_Vertices_of G;
registration
let G be finite connected real-weighted WGraph;
cluster spanning Tree-like for WSubgraph of G;
end;
definition
let G1 be finite connected real-weighted WGraph, G2 be spanning Tree-like
WSubgraph of G1;
attr G2 is min-cost means
:: GLIB_004:def 19
for G3 being spanning Tree-like WSubgraph of G1 holds G2.cost() <= G3.cost();
end;
registration
let G1 be finite connected real-weighted WGraph;
cluster min-cost for spanning Tree-like WSubgraph of G1;
end;
definition
let G be finite connected real-weighted WGraph;
mode minimumSpanningTree of G is min-cost spanning Tree-like WSubgraph of G;
end;
begin :: Prim's Algorithm Theorems
theorem :: GLIB_004:40
for G1,G2 being finite connected real-weighted WGraph, G3 being
WSubgraph of G1 st G3 is minimumSpanningTree of G1 & G1 == G2 & the_Weight_of
G1 = the_Weight_of G2 holds G3 is minimumSpanningTree of G2;
theorem :: GLIB_004:41
for G being finite connected real-weighted WGraph, G1 being
minimumSpanningTree of G, G2 being WGraph st G1 == G2 & the_Weight_of G1 =
the_Weight_of G2 holds G2 is minimumSpanningTree of G;
theorem :: GLIB_004:42
for G being finite connected real-weighted WGraph, n being Nat
holds (PRIM:CompSeq(G).n)`2 c= (PRIM:MST(G))`2;
::$N Prim's Minimum Spanning Tree Algorithm
theorem :: GLIB_004:43
for G1 being finite connected real-weighted WGraph, G2 being
inducedWSubgraph of G1, (PRIM:MST(G1))`1, (PRIM:MST(G1))`2 holds G2 is
minimumSpanningTree of G1;