:: The Underlying Principle of {D}ijkstra's Shortest Path Algorithm :: by Jingchao Chen and Yatsuka Nakamura :: :: Received January 7, 2003 :: Copyright (c) 2003-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, SUBSET_1, FUNCT_1, RELAT_1, TARSKI, CARD_1, FINSET_1, XXREAL_0, FINSEQ_1, FINSEQ_2, CARD_3, NAT_1, XBOOLE_0, ARYTM_3, ARYTM_1, ORDINAL4, GRAPH_1, STRUCT_0, TREES_2, GRAPH_4, PARTFUN1, GLIB_000, REAL_1, GRAPH_5, ARYTM_2; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSET_1, ARYTM_2, NAT_1, NAT_D, STRUCT_0, GRAPH_1, FUNCT_2, GRAPH_4, CARD_3, RVSUM_1; constructors FINSEQ_4, FINSOP_1, BINARITH, GRAPH_4, NAT_D, RVSUM_1, ARYTM_2, RELSET_1; registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, GRAPH_1, GRAPH_4, VALUED_0, CARD_1, STRUCT_0, ARYTM_2, FINSEQ_3, ORDINAL1; requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM; begin :: Preliminaries reserve n,m,i,j,k for Nat, x,y,e,X,V,U for set, W,f,g for Function; theorem :: GRAPH_5:1 rng f c= rng g & x in dom f implies ex y being object st y in dom g & f.x = g. y; theorem :: GRAPH_5:2 for D being finite set, n being Element of NAT, X being set st X = {x where x is Element of D* : 1 <= len x & len x <= n } holds X is finite; theorem :: GRAPH_5:3 for D being finite set, n being Element of NAT, X being set st X = {x where x is Element of D* : len x <= n } holds X is finite; ::$CT 2 definition let D be set, X be non empty Subset of D*; redefine mode Element of X -> FinSequence of D; end; begin :: Additional Properties of Finite Sequences reserve p,q for FinSequence; theorem :: GRAPH_5:6 (for n,m st 1<=n & n p.m) iff p is one-to-one; theorem :: GRAPH_5:7 (for n,m st 1<=n & n p.m) iff card rng p = len p; reserve G for Graph, pe,qe for FinSequence of the carrier' of G; theorem :: GRAPH_5:8 i in dom pe implies (the Source of G).(pe.i) in the carrier of G & ( the Target of G).(pe.i) in the carrier of G; theorem :: GRAPH_5:9 for x being object holds q^<*x*> is one-to-one & rng (q^<*x*>) c= rng p implies ex p1,p2 being FinSequence st p=p1^<*x*>^p2 & rng q c= rng (p1^p2); begin :: Additional Properties of Chains and Oriented Paths theorem :: GRAPH_5:10 p^q is Chain of G implies p is Chain of G & q is Chain of G; theorem :: GRAPH_5:11 p^q is oriented Chain of G implies p is oriented Chain of G & q is oriented Chain of G; theorem :: GRAPH_5:12 for p,q being oriented Chain of G st (the Target of G).(p.len p) =(the Source of G).(q.1) holds p^q is oriented Chain of G; begin :: Additional Properties of Acyclic Oriented Paths theorem :: GRAPH_5:13 {} is Simple oriented Chain of G; theorem :: GRAPH_5:14 p^q is Simple oriented Chain of G implies p is Simple oriented Chain of G & q is Simple oriented Chain of G; theorem :: GRAPH_5:15 len pe = 1 implies pe is Simple oriented Chain of G; theorem :: GRAPH_5:16 for p being Simple oriented Chain of G, q being FinSequence of the carrier' of G st len p >=1 & len q=1 & (the Source of G).(q.1)=(the Target of G).(p.(len p)) & (the Source of G).(p.1) <> (the Target of G).(p.(len p)) & not ex k st 1<=k & k <= len p & (the Target of G).(p.k) =(the Target of G).(q.1 ) holds p^q is Simple oriented Chain of G; theorem :: GRAPH_5:17 for p being Simple oriented Chain of G holds p is one-to-one; begin :: The Set of the carrier On a Path or an Edge definition let G be Graph, e be Element of the carrier' of G; func vertices e -> set equals :: GRAPH_5:def 1 {(the Source of G).e, (the Target of G).e}; end; definition let G,pe; func vertices pe -> Subset of the carrier of G equals :: GRAPH_5:def 2 {v where v is Vertex of G : ex i st i in dom pe & v in vertices(pe/.i)}; end; theorem :: GRAPH_5:18 for p being Simple oriented Chain of G st p=pe^qe & len pe >= 1 & len qe >= 1 & (the Source of G).(p.1) <> (the Target of G).(p.len p) holds not (the Source of G).(p.1) in vertices qe & not (the Target of G).(p.len p) in vertices pe; theorem :: GRAPH_5:19 vertices pe c= V iff for i be Nat st i in dom pe holds vertices( pe/.i) c= V; theorem :: GRAPH_5:20 not vertices pe c= V implies ex i being Element of NAT, q,r being FinSequence of the carrier' of G st i+1 <= len pe & not vertices(pe/.(i+1 )) c= V & len q=i & pe=q^r & vertices q c= V; theorem :: GRAPH_5:21 rng qe c= rng pe implies vertices qe c= vertices pe; theorem :: GRAPH_5:22 rng qe c= rng pe & vertices(pe) \ X c= V implies vertices(qe) \ X c= V; theorem :: GRAPH_5:23 vertices(pe^qe) \ X c= V implies vertices(pe) \ X c= V & vertices(qe) \ X c= V; reserve v,v1,v2,v3 for Element of G; theorem :: GRAPH_5:24 i in dom pe & (v=(the Source of G).(pe.i) or v=(the Target of G) .(pe.i)) implies v in vertices pe; theorem :: GRAPH_5:25 len pe = 1 implies vertices(pe) = vertices(pe/.1); theorem :: GRAPH_5:26 vertices pe c= vertices(pe^qe) & vertices qe c= vertices(pe^qe); reserve p,q for oriented Chain of G; theorem :: GRAPH_5:27 p = q^pe & len q >= 1 & len pe = 1 implies vertices(p) = vertices(q) \/ {(the Target of G).(pe.1)}; theorem :: GRAPH_5:28 v <> (the Source of G).(p.1) & v in vertices(p) implies ex i st 1<=i & i <= len p & v = (the Target of G).(p.i); begin :: Directed Paths between Two vertices definition let G, p, v1,v2; pred p is_orientedpath_of v1,v2 means :: GRAPH_5:def 3 p <> {} & (the Source of G).(p. 1) = v1 & (the Target of G).(p.(len p))= v2; end; definition let G, v1,v2, p,V; pred p is_orientedpath_of v1,v2,V means :: GRAPH_5:def 4 p is_orientedpath_of v1,v2 & vertices(p) \ {v2} c= V; end; definition let G be Graph, v1,v2 be Element of G; func OrientedPaths(v1,v2) -> Subset of ((the carrier' of G)*) equals :: GRAPH_5:def 5 {p where p is oriented Chain of G : p is_orientedpath_of v1,v2}; end; theorem :: GRAPH_5:29 p is_orientedpath_of v1,v2 implies v1 in vertices p & v2 in vertices p; theorem :: GRAPH_5:30 x in OrientedPaths(v1,v2) iff ex p st p=x & p is_orientedpath_of v1,v2; theorem :: GRAPH_5:31 p is_orientedpath_of v1,v2,V & v1 <> v2 implies v1 in V; theorem :: GRAPH_5:32 p is_orientedpath_of v1,v2,V & V c= U implies p is_orientedpath_of v1,v2,U; theorem :: GRAPH_5:33 len p >= 1 & p is_orientedpath_of v1,v2 & pe.1 orientedly_joins v2,v3 & len pe=1 implies ex q st q=p^pe & q is_orientedpath_of v1,v3; theorem :: GRAPH_5:34 q=p^pe & len p >= 1 & len pe=1 & p is_orientedpath_of v1,v2,V & pe.1 orientedly_joins v2,v3 implies q is_orientedpath_of v1,v3,V \/{v2}; begin :: Acyclic (or Simple) Paths definition let G be Graph, p be oriented Chain of G, v1,v2 be Element of G; pred p is_acyclicpath_of v1,v2 means :: GRAPH_5:def 6 p is Simple & p is_orientedpath_of v1,v2; end; definition let G be Graph, p be oriented Chain of G, v1,v2 be Element of G,V be set; pred p is_acyclicpath_of v1,v2,V means :: GRAPH_5:def 7 p is Simple & p is_orientedpath_of v1,v2,V; end; definition let G be Graph, v1,v2 be Element of G; func AcyclicPaths(v1,v2) -> Subset of ((the carrier' of G)*) equals :: GRAPH_5:def 8 {p where p is Simple oriented Chain of G: p is_acyclicpath_of v1,v2}; end; definition let G be Graph, v1,v2 be Element of G,V be set; func AcyclicPaths(v1,v2,V) -> Subset of ((the carrier' of G)*) equals :: GRAPH_5:def 9 {p where p is Simple oriented Chain of G : p is_acyclicpath_of v1,v2,V}; end; definition let G be Graph, p be oriented Chain of G; func AcyclicPaths(p) -> Subset of ((the carrier' of G)*) equals :: GRAPH_5:def 10 {q where q is Simple oriented Chain of G : q <> {} & (the Source of G).(q.1) = (the Source of G).(p.1) & (the Target of G).(q.(len q)) = (the Target of G).(p.(len p)) & rng q c= rng p}; end; definition let G be Graph; func AcyclicPaths(G) -> Subset of (the carrier' of G)* equals :: GRAPH_5:def 11 the set of all q where q is Simple oriented Chain of G ; end; theorem :: GRAPH_5:35 p={} implies not p is_acyclicpath_of v1,v2; theorem :: GRAPH_5:36 p is_acyclicpath_of v1,v2 implies p is_orientedpath_of v1,v2; theorem :: GRAPH_5:37 AcyclicPaths(v1,v2) c= OrientedPaths(v1,v2); theorem :: GRAPH_5:38 AcyclicPaths(p) c= AcyclicPaths(G); theorem :: GRAPH_5:39 AcyclicPaths(v1,v2) c= AcyclicPaths(G); theorem :: GRAPH_5:40 p is_orientedpath_of v1,v2 implies AcyclicPaths(p) c= AcyclicPaths(v1,v2); theorem :: GRAPH_5:41 p is_orientedpath_of v1,v2,V implies AcyclicPaths(p) c= AcyclicPaths(v1,v2,V) ; theorem :: GRAPH_5:42 q in AcyclicPaths(p) implies len q <= len p; theorem :: GRAPH_5:43 p is_orientedpath_of v1,v2 implies AcyclicPaths(p) <> {} & AcyclicPaths(v1,v2) <> {}; theorem :: GRAPH_5:44 p is_orientedpath_of v1,v2,V implies AcyclicPaths(p) <> {} & AcyclicPaths(v1,v2,V) <> {}; theorem :: GRAPH_5:45 AcyclicPaths(v1,v2,V) c= AcyclicPaths(G); begin :: Weight Graphs and Their Basic Properties notation synonym Real>=0 for REAL+; end; definition redefine func Real>=0 -> Subset of REAL equals :: GRAPH_5:def 12 { r where r is Real : r >=0 }; end; registration cluster Real>=0 -> non empty; end; definition let G be Graph, W be Function; pred W is_weight>=0of G means :: GRAPH_5:def 13 W is Function of the carrier' of G, Real>=0; end; definition let G be Graph, W be Function; pred W is_weight_of G means :: GRAPH_5:def 14 W is Function of (the carrier' of G), REAL; end; definition let G be Graph, p be FinSequence of the carrier' of G, W be Function; assume W is_weight_of G; func RealSequence(p,W) -> FinSequence of REAL means :: GRAPH_5:def 15 dom p = dom it & for i be Nat st i in dom p holds it.i=W.(p.i); end; definition let G be Graph, p be FinSequence of the carrier' of G,W be Function; func cost(p,W) -> Real equals :: GRAPH_5:def 16 Sum RealSequence(p,W); end; theorem :: GRAPH_5:46 W is_weight>=0of G implies W is_weight_of G; theorem :: GRAPH_5:47 for f being FinSequence of REAL st W is_weight>=0of G & f = RealSequence(pe,W) holds for i st i in dom f holds f.i >= 0; theorem :: GRAPH_5:48 rng qe c= rng pe & W is_weight_of G & i in dom qe implies ex j st j in dom pe & RealSequence(pe,W).j = RealSequence(qe,W).i; theorem :: GRAPH_5:49 len qe = 1 & rng qe c= rng pe & W is_weight>=0of G implies cost(qe,W) <= cost(pe,W); theorem :: GRAPH_5:50 W is_weight>=0of G implies cost(pe,W) >= 0; theorem :: GRAPH_5:51 pe = {} & W is_weight_of G implies cost(pe,W) = 0; theorem :: GRAPH_5:52 for D being non empty finite Subset of (the carrier' of G)* st D = AcyclicPaths(v1,v2) ex pe st pe in D & for qe st qe in D holds cost(pe,W) <= cost(qe,W); theorem :: GRAPH_5:53 for D being non empty finite Subset of (the carrier' of G)* st D = AcyclicPaths(v1,v2,V) holds ex pe st pe in D & for qe st qe in D holds cost( pe,W) <= cost(qe,W); theorem :: GRAPH_5:54 W is_weight_of G implies cost(pe^qe,W) = cost(pe,W) + cost(qe,W); theorem :: GRAPH_5:55 qe is one-to-one & rng qe c= rng pe & W is_weight>=0of G implies cost(qe,W) <= cost(pe,W); theorem :: GRAPH_5:56 pe in AcyclicPaths(p) & W is_weight>=0of G implies cost(pe,W) <= cost(p,W); begin :: Shortest Paths and Their Basic Properties definition let G be Graph, v1,v2 be Vertex of G, p be oriented Chain of G, W be Function; pred p is_shortestpath_of v1,v2,W means :: GRAPH_5:def 17 p is_orientedpath_of v1,v2 & for q being oriented Chain of G st q is_orientedpath_of v1,v2 holds cost(p,W) <= cost(q,W); end; definition let G be Graph, v1,v2 be Vertex of G, p be oriented Chain of G, V be set, W be Function; pred p is_shortestpath_of v1,v2,V,W means :: GRAPH_5:def 18 p is_orientedpath_of v1,v2 ,V & for q being oriented Chain of G st q is_orientedpath_of v1,v2,V holds cost (p,W) <= cost(q,W); end; begin :: Basic Properties of a Graph with Finite carrier reserve G for finite Graph, ps for Simple oriented Chain of G, P,Q for oriented Chain of G, v1,v2,v3 for Element of G, pe,qe for FinSequence of the carrier' of G; theorem :: GRAPH_5:57 len ps <= VerticesCount G; theorem :: GRAPH_5:58 len ps <= EdgesCount G; registration let G; cluster AcyclicPaths G -> finite; end; registration let G, P; cluster AcyclicPaths P -> finite; end; registration let G, v1, v2; cluster AcyclicPaths(v1,v2) -> finite; end; registration let G, v1, v2, V; cluster AcyclicPaths(v1,v2,V) -> finite; end; theorem :: GRAPH_5:59 AcyclicPaths(v1,v2) <> {} implies ex pe st pe in AcyclicPaths(v1,v2) & for qe st qe in AcyclicPaths(v1,v2) holds cost(pe,W) <= cost(qe,W); theorem :: GRAPH_5:60 AcyclicPaths(v1,v2,V) <> {} implies ex pe st pe in AcyclicPaths(v1,v2, V) & for qe st qe in AcyclicPaths(v1,v2,V) holds cost(pe,W) <= cost(qe,W); theorem :: GRAPH_5:61 P is_orientedpath_of v1,v2 & W is_weight>=0of G implies ex q being Simple oriented Chain of G st q is_shortestpath_of v1,v2,W; theorem :: GRAPH_5:62 P is_orientedpath_of v1,v2,V & W is_weight>=0of G implies ex q being Simple oriented Chain of G st q is_shortestpath_of v1,v2,V,W; begin :: Three Basic Theorems for Dijkstra's Shortest Path Algorithm theorem :: GRAPH_5:63 W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & (for Q, v3 st not v3 in V & Q is_shortestpath_of v1,v3,V,W holds cost(P,W) <= cost(Q,W)) implies P is_shortestpath_of v1,v2,W; theorem :: GRAPH_5:64 W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & V c= U & (for Q, v3 st not v3 in V & Q is_shortestpath_of v1,v3,V,W holds cost(P,W) <= cost(Q,W)) implies P is_shortestpath_of v1,v2,U,W; definition let G be Graph, pe be FinSequence of the carrier' of G, V be set, v1 be Vertex of G, W be Function; pred pe islongestInShortestpath V,v1,W means :: GRAPH_5:def 19 for v being Vertex of G st v in V & v <> v1 ex q being oriented Chain of G st q is_shortestpath_of v1,v ,V,W & cost(q,W) <= cost(pe,W); end; ::$N Dijkstra's shortest path algorithm theorem :: GRAPH_5:65 for G being finite oriented Graph, P,Q,R being oriented Chain of G, v1 ,v2,v3 being Element of G st e in the carrier' of G & W is_weight>=0of G & len P >= 1 & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & v1 <> v3 & R=P^<*e*> & Q is_shortestpath_of v1,v3,V,W & e orientedly_joins v2,v3 & P islongestInShortestpath V,v1,W holds (cost(Q,W) <= cost(R,W) implies Q is_shortestpath_of v1,v3,V \/{v2},W) & (cost(Q,W) >= cost(R,W) implies R is_shortestpath_of v1,v3,V \/{v2},W);