The abstract of the Mizar article:

The Underlying Principle of Dijkstra's Shortest Path Algorithm

by

Jing-Chao Chen, and

Yatsuka Nakamura

Received January 7, 2003

MML identifier: GRAPH_5

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, BOOLE, RELAT_1, FINSET_1, ORDERS_1, FINSEQ_1, CARD_1,
      GRAPH_1, GRAPH_5, RLVECT_1, GRAPH_4, FINSEQ_4, FINSEQ_2, PROB_1, ARYTM_1,
      MSAFREE2;
 notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XREAL_0, RELAT_1, FUNCT_1,
      FINSEQ_1, FINSEQ_2, FINSEQ_4, CARD_1, FINSET_1, REAL_1, NAT_1, GRAPH_1,
      BINARITH, FUNCT_2, GRAPH_4, PROB_1, RVSUM_1, GOBOARD1, GRAPH_3;
 constructors REAL_1, BINARITH, FINSEQ_4, GRAPH_4, PROB_1, GOBOARD1, SEQ_2,
      MEMBERED;
 clusters FINSEQ_1, GRAPH_1, GRAPH_2, RELSET_1, SUBSET_1, GRAPH_4, FINSET_1,
      PRELAMB, NAT_1, XREAL_0, MEMBERED;
 requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM;


begin :: Preliminaries

reserve n,m,i,j,k for Nat,
        x,y,e,y1,y2,X,V,U for set,
        W,f,g for Function;

theorem :: GRAPH_5:1
  for f being finite Function holds card rng f <= card dom f;

theorem :: GRAPH_5:2
  rng f c= rng g & x in dom f implies ex y st y in dom g & f.x = g.y;

scheme LambdaAB { A, B()->set, F(Element of B())->set } :
  ex f being Function st dom f = A() & for x being Element of B() st
     x in A() holds f.x = F(x);

theorem :: GRAPH_5:3
  for D being finite set, n being 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:4
  for D being finite set, n being Nat, X being set
  st X = {x where x is Element of D* : len x <= n } holds X is finite;

theorem :: GRAPH_5:5
  for D being finite set holds card D <> 0 iff D <> {};

theorem :: GRAPH_5:6
  for D being finite set, k being Nat st card D = k+1 holds
  ex x being Element of D,C being Subset of D st D = C \/ { x } & card C = k;

theorem :: GRAPH_5:7
  for D being finite set st card D = 1 holds ex x being Element of D st D={x};

scheme MinValue { D() -> non empty finite set, F(Element of D())-> Real}:
  ex x being Element of D() st for y being Element of D() holds F(x) <= F(y);

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:8
  p <> {} iff len p >= 1;

theorem :: GRAPH_5:9
  (for n,m st 1<=n & n<m & m<=len p holds p.n <> p.m) iff p is one-to-one;

theorem :: GRAPH_5:10
  (for n,m st 1<=n & n<m & m<=len p holds p.n <> p.m) iff card rng p = len p;

reserve G for Graph,
        pe,qe for FinSequence of the Edges of G;

theorem :: GRAPH_5:11
  i in dom pe implies (the Source of G).(pe.i) in the Vertices of G
   & (the Target of G).(pe.i) in the Vertices of G;

theorem :: GRAPH_5:12
  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:13
  p^q is Chain of G implies p is Chain of G & q is Chain of G;

theorem :: GRAPH_5:14
  p^q is oriented Chain of G implies p is oriented Chain of G &
  q is oriented Chain of G;

theorem :: GRAPH_5:15
  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:16
  {} is Simple (oriented Chain of G);

theorem :: GRAPH_5:17
  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:18
  len pe = 1 implies pe is Simple (oriented Chain of G);

theorem :: GRAPH_5:19
  for p being Simple (oriented Chain of G), q being FinSequence of
  the Edges 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:20
  for p being Simple (oriented Chain of G) holds p is one-to-one;

begin :: The Set of the Vertices On a Path or an Edge

definition let G be Graph, e be Element of the Edges of G;
  func vertices e 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 Vertices 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:21
  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:22
  vertices pe c= V iff for i st i in dom pe holds vertices(pe/.i) c= V;

theorem :: GRAPH_5:23
  not vertices pe c= V implies ex i being Nat, q,r being FinSequence
  of the Edges 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:24
  rng qe c= rng pe implies vertices qe c= vertices pe;

theorem :: GRAPH_5:25
  rng qe c= rng pe & vertices(pe) \ X c= V implies vertices(qe) \ X c= V;

theorem :: GRAPH_5:26
  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 the Vertices of G;

theorem :: GRAPH_5:27
  for e being Element of the Edges of G st
  v=(the Source of G).e or v=(the Target of G).e holds v in vertices(e);

theorem :: GRAPH_5:28
  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:29
  len pe = 1 implies vertices(pe) = vertices(pe/.1);

theorem :: GRAPH_5:30
  vertices pe c= vertices(pe^qe) & vertices qe c= vertices(pe^qe);

reserve p,q for oriented Chain of G;

theorem :: GRAPH_5:31
  p = q^pe & len q >= 1 & len pe = 1 implies vertices(p) = vertices(q) \/
  {(the Target of G).(pe.1)};

theorem :: GRAPH_5:32
  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 the Vertices of G;
  func OrientedPaths(v1,v2) -> Subset of ((the Edges 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:33
  p is_orientedpath_of v1,v2 implies v1 in vertices p & v2 in vertices p;

theorem :: GRAPH_5:34
    x in OrientedPaths(v1,v2) iff ex p st p=x & p is_orientedpath_of v1,v2;

theorem :: GRAPH_5:35
  p is_orientedpath_of v1,v2,V & v1 <> v2 implies v1 in V;

theorem :: GRAPH_5:36
  p is_orientedpath_of v1,v2,V & V c= U implies p is_orientedpath_of v1,v2,U;

theorem :: GRAPH_5:37
  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:38
  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 the Vertices 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
           the Vertices 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 the Vertices of G;
  func AcyclicPaths(v1,v2) -> Subset of ((the Edges 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 the Vertices of G,V be set;
  func AcyclicPaths(v1,v2,V) -> Subset of ((the Edges 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 Edges 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 Edges of G)* equals
:: GRAPH_5:def 11
    {q where q is Simple (oriented Chain of G) : not contradiction};
end;

theorem :: GRAPH_5:39
    p={} implies not p is_acyclicpath_of v1,v2;

theorem :: GRAPH_5:40
   p is_acyclicpath_of v1,v2 implies p is_orientedpath_of v1,v2;

theorem :: GRAPH_5:41
    AcyclicPaths(v1,v2) c= OrientedPaths(v1,v2);

theorem :: GRAPH_5:42
  AcyclicPaths(p) c= AcyclicPaths(G);

theorem :: GRAPH_5:43
  AcyclicPaths(v1,v2) c= AcyclicPaths(G);

theorem :: GRAPH_5:44
  p is_orientedpath_of v1,v2 implies AcyclicPaths(p) c= AcyclicPaths(v1,v2);

theorem :: GRAPH_5:45
  p is_orientedpath_of v1,v2,V implies
  AcyclicPaths(p) c= AcyclicPaths(v1,v2,V);

theorem :: GRAPH_5:46
    q in AcyclicPaths(p) implies len q <= len p;

theorem :: GRAPH_5:47
  p is_orientedpath_of v1,v2 implies AcyclicPaths(p) <> {} &
  AcyclicPaths(v1,v2) <> {};

theorem :: GRAPH_5:48
  p is_orientedpath_of v1,v2,V implies AcyclicPaths(p) <> {} &
  AcyclicPaths(v1,v2,V) <> {};

theorem :: GRAPH_5:49
  AcyclicPaths(v1,v2,V) c= AcyclicPaths(G);

begin :: Weight Graphs and Their Basic Properties

definition
  func Real>=0 -> Subset of REAL equals
:: GRAPH_5:def 12
  { r where r is Real : r >=0 };
end;

definition
 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 Edges 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 Edges of G), REAL;
end;

definition
  let G be Graph, p be FinSequence of the Edges 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 Edges of G,W be Function;
  func cost(p,W) -> Real equals
:: GRAPH_5:def 16
    Sum RealSequence(p,W);
end;

theorem :: GRAPH_5:50
  W is_weight>=0of G implies W is_weight_of G;

theorem :: GRAPH_5:51
  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:52
  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:53
    len qe = 1 & rng qe c= rng pe & W is_weight>=0of G implies
  cost(qe,W) <= cost(pe,W);

theorem :: GRAPH_5:54
  W is_weight>=0of G implies cost(pe,W) >= 0;

theorem :: GRAPH_5:55
  pe = {} & W is_weight_of G implies cost(pe,W) = 0;

theorem :: GRAPH_5:56
  for D being non empty finite Subset of (the Edges 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:57
  for D being non empty finite Subset of (the Edges 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:58
  W is_weight_of G implies cost(pe^qe,W) = cost(pe,W) + cost(qe,W);

theorem :: GRAPH_5:59
  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:60
  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 Vertices

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 the Vertices of G,
        pe,qe for FinSequence of the Edges of G;

theorem :: GRAPH_5:61
    len ps <= VerticesCount G;

theorem :: GRAPH_5:62
  len ps <= EdgesCount G;

definition let G;
  cluster AcyclicPaths G -> finite;
end;

definition let G, P;
  cluster AcyclicPaths P -> finite;
end;

definition let G, v1, v2;
  cluster AcyclicPaths(v1,v2) -> finite;
end;

definition let G, v1, v2, V;
  cluster AcyclicPaths(v1,v2,V) -> finite;
end;

theorem :: GRAPH_5:63
   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:64
   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:65
    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:66
  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:67
  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:68
    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 Edges 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;

theorem :: GRAPH_5:69
    for G being finite oriented Graph,
        P,Q,R being oriented Chain of G,
        v1,v2,v3 being Element of the Vertices of G st
  e in the Edges 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);