:: 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-2021 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 be Nat; cluster -> connected for inducedSubgraph of G1,(PRIM:CompSeq(G1).n)`1; end; registration let G1 be _finite real-weighted WGraph, n be 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;