Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Jing-Chao Chen
- Received March 17, 2003
- MML identifier: GRAPHSP
- [
Mizar article,
MML identifier index
]
environ
vocabulary ARYTM_1, INT_1, RELAT_1, SCM_1, RLVECT_1, AMI_3, GRAPHSP, FUNCT_1,
BOOLE, FINSET_1, ORDERS_1, FINSEQ_1, CARD_1, FUNCT_2, GRAPH_1, FINSEQ_4,
GRAPH_5, GRAPH_4, MSAFREE2, FUNCT_4;
notation XREAL_0, REAL_1, NAT_1, INT_1, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1,
FUNCT_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, CARD_1, FINSET_1, GRAPH_1,
PARTFUN1, FUNCT_2, GRAPH_4, GRAPH_3, GRAPH_5, BINARITH, DOMAIN_1,
RVSUM_1, GOBOARD1, NUMBERS, FUNCT_7;
constructors REAL_1, INT_1, FINSEQ_4, GRAPH_5, GRAPH_4, DOMAIN_1, BINARITH,
GOBOARD1, FUNCT_7, MEMBERED, RELAT_2;
clusters FRAENKEL, INT_1, GRAPH_5, FINSEQ_1, FINSET_1, RELSET_1, GRAPH_1,
FUNCT_2, GRAPH_4, XREAL_0, MEMBERED, PARTFUN1, NUMBERS, ORDINAL2;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
begin :: Preliminaries
reserve x,y,X for set,
i,j,k,m,n for Nat,
p for FinSequence of X,
ii for Integer;
theorem :: GRAPHSP:1
for p being FinSequence,x being set holds not x in rng p & p is one-to-one
iff p^<*x*> is one-to-one;
theorem :: GRAPHSP:2
1 <= ii & ii <= len p implies p.ii in X;
theorem :: GRAPHSP:3
1 <= ii & ii <= len p implies p/.ii = p.ii;
reserve G for Graph,
pe,qe for FinSequence of the Edges of G,
p,q for oriented Chain of G,
W for Function,
U,V,e,ee for set,
v1,v2,v3,v4 for Vertex of G;
theorem :: GRAPHSP:4
W is_weight_of G & len pe = 1 implies cost(pe,W) = W.(pe.1);
theorem :: GRAPHSP:5
e in the Edges of G implies <*e*> is Simple (oriented Chain of G);
theorem :: GRAPHSP:6
for p being Simple (oriented Chain of G) st p=pe^qe & len pe >= 1 &
len qe >= 1 holds
(the Target of G).(p.len p) <> (the Target of G).(pe.len pe) &
(the Source of G).(p.1) <> (the Source of G).(qe.1);
begin :: The fundamental properties of directed paths and shortest paths
theorem :: GRAPHSP:7
p is_orientedpath_of v1,v2,V iff p is_orientedpath_of v1,v2,V \/ {v2};
theorem :: GRAPHSP:8
p is_shortestpath_of v1,v2,V,W iff p is_shortestpath_of v1,v2,V \/{v2},W;
theorem :: GRAPHSP:9
p is_shortestpath_of v1,v2,V,W & q is_shortestpath_of v1,v2,V,W implies
cost(p,W)=cost(q,W);
theorem :: GRAPHSP:10
for G being oriented Graph,v1,v2 be Vertex of G,e1,e2 be set
st e1 in the Edges of G & e2 in the Edges of G &
e1 orientedly_joins v1,v2 & e2 orientedly_joins v1,v2 holds e1=e2;
theorem :: GRAPHSP:11
the Vertices of G= U \/ V & v1 in U & v2 in V & (for v3,v4 st v3 in U &
v4 in V holds not (ex e st e in the Edges of G & e orientedly_joins v3,v4))
implies not ex p st p is_orientedpath_of v1,v2;
theorem :: GRAPHSP:12
the Vertices of G= U \/ V & v1 in U & (for v3,v4 st v3 in U &
v4 in V holds not (ex e st e in the Edges of G & e orientedly_joins v3,v4)) &
p is_orientedpath_of v1,v2 implies p is_orientedpath_of v1,v2,U;
begin :: The basic theorems for Dijkstra's shortest path algorithm (continue)
reserve G for finite Graph,
P,Q for oriented Chain of G,
v1,v2,v3 for Vertex of G;
theorem :: GRAPHSP:13
W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & v1 <> v3 &
Q is_shortestpath_of v1,v3,V,W & not (ex e st e in the Edges of G &
e orientedly_joins v2,v3) & P islongestInShortestpath V,v1,W implies
Q is_shortestpath_of v1,v3,V \/{v2},W;
reserve G for finite oriented Graph,
P,Q for oriented Chain of G,
W for Function of (the Edges of G), Real>=0,
v1,v2,v3,v4 for Vertex of G;
theorem :: GRAPHSP:14
e in the Edges of G & v1 <> v2 & P=<*e*> & e orientedly_joins v1,v2
implies P is_shortestpath_of v1,v2,{v1},W;
theorem :: GRAPHSP:15
e in the Edges of G & P is_shortestpath_of v1,v2,V,W & v1 <> v3 & Q=P^<*e*> &
e orientedly_joins v2,v3 & v1 in V & (for v4 st v4 in V holds
not (ex ee st ee in the Edges of G & ee orientedly_joins v4,v3)) implies
Q is_shortestpath_of v1,v3,V \/{v2},W;
theorem :: GRAPHSP:16
the Vertices of G= U \/ V & v1 in U & (for v3,v4 st v3 in U &
v4 in V holds not (ex e st e in the Edges of G & e orientedly_joins v3,v4))
implies (P is_shortestpath_of v1,v2,U,W iff P is_shortestpath_of v1,v2,W);
begin :: The definition of assignment statement
definition let f be Function, i, x be set;
redefine func f+*(i,x);
synonym (f,i):=x;
end;
theorem :: GRAPHSP:17
for x,y being set, f being Function holds rng (f,x):=y c= rng f \/ {y};
definition let f be FinSequence of REAL, x be set, r be Real;
redefine func (f, x):=r -> FinSequence of REAL;
end;
definition let i,k be Nat,f be FinSequence of REAL,r be Real;
func (f,i):=(k,r) -> FinSequence of REAL equals
:: GRAPHSP:def 1
((f,i):=k,k):=r;
end;
reserve f,g,h for Element of REAL*,
r for Real;
theorem :: GRAPHSP:18
i <> k & i in dom f implies ((f,i):=(k,r)).i = k;
theorem :: GRAPHSP:19
m <> i & m <> k & m in dom f implies ((f,i):=(k,r)).m = f.m;
theorem :: GRAPHSP:20
k in dom f implies ((f,i):=(k,r)).k = r;
theorem :: GRAPHSP:21
dom ((f,i):=(k,r)) = dom f;
begin :: The definition of Pascal-like while-do statement
definition let X be set;
redefine func id X -> Element of Funcs(X,X);
end;
definition let X be set,f,g be Function of X,X;
redefine func g*f -> Function of X,X;
end;
definition let X be set,f,g be Element of Funcs(X,X);
redefine func g*f -> Element of Funcs(X,X);
end;
definition let X be set,f be Element of Funcs(X,X),g be Element of X;
redefine func f.g -> Element of X;
end;
definition let X be set, f be Element of Funcs(X,X);
func repeat(f) -> Function of NAT,Funcs(X,X) means
:: GRAPHSP:def 2
it.0 = id X & for i being Nat holds it.(i+1)=f*(it.i);
end;
theorem :: GRAPHSP:22
for F being Element of Funcs(REAL*,REAL*),f being Element of REAL*,n,i be Nat
holds (repeat F).0 .f = f;
theorem :: GRAPHSP:23
for F,G being Element of Funcs(REAL*,REAL*),f being Element of REAL*,
i be Nat holds (repeat (F*G)).(i+1).f = F.(G.((repeat (F*G)).i.f));
definition let g be Element of Funcs(REAL*,REAL*),f be Element of REAL*;
redefine func g.f -> Element of REAL*;
end;
definition let f be Element of REAL*, n be Nat;
func OuterVx(f,n) -> Subset of NAT equals
:: GRAPHSP:def 3
{i: i in dom f & 1 <= i & i <= n & f.i <> -1 & f.(n+i) <> -1};
end;
definition let f be Element of Funcs(REAL*,REAL*),g be Element of REAL*,
n be Nat;
assume ex i st OuterVx((repeat f).i.g,n) = {};
func LifeSpan(f,g,n) -> Nat means
:: GRAPHSP:def 4
OuterVx((repeat f).it.g,n) = {} &
for k being Nat st OuterVx((repeat f).k.g,n) = {} holds it <= k;
end;
definition let f be Element of Funcs(REAL*,REAL*), n be Nat;
func while_do(f,n) -> Element of Funcs(REAL*,REAL*) means
:: GRAPHSP:def 5
dom it=REAL* & for h being Element of REAL* holds
it.h=(repeat f).LifeSpan(f,h,n).h;
end;
begin :: Defining a weight function for an oriented graph
definition
let G be oriented Graph,v1,v2 be Vertex of G;
assume ex e be set st e in the Edges of G & e orientedly_joins v1,v2;
func Edge(v1,v2) means
:: GRAPHSP:def 6
ex e be set st it = e & e in the Edges of G & e orientedly_joins v1,v2;
end;
definition
let G be oriented Graph,v1,v2 be Vertex of G, W be Function;
func Weight(v1,v2,W) equals
:: GRAPHSP:def 7
W.Edge(v1,v2) if ex e be set st e in the Edges of G &
e orientedly_joins v1,v2 otherwise -1;
end;
definition
let G be oriented Graph,v1,v2 be Vertex of G,
W be Function of (the Edges of G), Real>=0;
redefine func Weight(v1,v2,W) -> Real;
end;
reserve G for oriented Graph,
v1,v2 for Vertex of G,
W for Function of (the Edges of G), Real>=0;
theorem :: GRAPHSP:24
Weight(v1,v2,W) >= 0 iff ex e be set st e in the Edges of G &
e orientedly_joins v1,v2;
theorem :: GRAPHSP:25
Weight(v1,v2,W) = -1 iff not ex e be set st e in the Edges of G &
e orientedly_joins v1,v2;
theorem :: GRAPHSP:26
e in the Edges of G & e orientedly_joins v1,v2 implies Weight(v1,v2,W)=W.e;
begin :: Basic operations for Dijkstra's shortest path algorithm
definition let f be Element of REAL*, n be Nat;
func UnusedVx(f,n) -> Subset of NAT equals
:: GRAPHSP:def 8
{i: i in dom f & 1 <= i & i <= n & f.i <> -1};
end;
definition let f be Element of REAL*, n be Nat;
func UsedVx(f,n) -> Subset of NAT equals
:: GRAPHSP:def 9
{i: i in dom f & 1 <= i & i <= n & f.i = -1};
end;
theorem :: GRAPHSP:27
UnusedVx(f,n) c= Seg n;
definition let f be Element of REAL*, n be Nat;
cluster UnusedVx(f,n) -> finite;
end;
theorem :: GRAPHSP:28
OuterVx(f,n) c= UnusedVx(f,n);
theorem :: GRAPHSP:29
OuterVx(f,n) c= Seg n;
definition let f be Element of REAL*, n be Nat;
cluster OuterVx(f,n) -> finite;
end;
definition let X be finite Subset of NAT,f be Element of REAL*,n;
func Argmin(X,f,n) -> Nat means
:: GRAPHSP:def 10
(X<>{} implies ex i st i=it & i in X &
(for k st k in X holds f/.(2*n+i) <= f/.(2*n+k)) &
(for k st k in X & f/.(2*n+i) = f/.(2*n+k) holds i <= k)) &
(X={} implies it=0);
end;
theorem :: GRAPHSP:30
OuterVx(f,n) <> {} & j=Argmin(OuterVx(f,n),f,n) implies j in dom f & 1<=j &
j<=n & f.j <> -1 & f.(n+j) <> -1;
theorem :: GRAPHSP:31
Argmin(OuterVx(f,n),f,n) <= n;
definition let n be Nat;
func findmin(n) -> Element of Funcs(REAL*,REAL*) means
:: GRAPHSP:def 11
dom it = REAL* & for f be Element of REAL* holds it.f=
(f,n*n+3*n+1) := (Argmin(OuterVx(f,n),f,n),-1);
end;
theorem :: GRAPHSP:32
i in dom f & i > n & i <> n*n+3*n+1 implies (findmin n).f.i=f.i;
theorem :: GRAPHSP:33
i in dom f & f.i=-1 & i <> n*n+3*n+1 implies (findmin n).f.i=-1;
theorem :: GRAPHSP:34
dom ((findmin n).f) = dom f;
theorem :: GRAPHSP:35
OuterVx(f,n) <> {} implies ex j st j in OuterVx(f,n) & 1 <= j & j <= n &
(findmin n).f.j=-1;
definition let f be Element of REAL*,n,k be Nat;
func newpathcost(f,n,k) -> Real equals
:: GRAPHSP:def 12
f/.(2*n+f/.(n*n+3*n+1))+ f/.(2*n+n*(f/.(n*n+3*n+1))+k);
end;
definition let n,k be Nat,f be Element of REAL*;
pred f hasBetterPathAt n,k means
:: GRAPHSP:def 13
(f.(n+k)=-1 or f/.(2*n+k) > newpathcost(f,n,k)) &
f/.(2*n+n*(f/.(n*n+3*n+1))+k) >= 0 & f.k <> -1;
end;
definition let f be Element of REAL*,n be Nat;
func Relax(f,n) -> Element of REAL* means
:: GRAPHSP:def 14
dom it = dom f & for k be Nat st k in dom f holds
(n<k & k <= 2*n implies (f hasBetterPathAt n,(k-'n)
implies it.k=f/.(n*n+3*n+1)) & (not f hasBetterPathAt n,(k-'n)
implies it.k=f.k)) &
(2*n <k & k <=3*n implies (f hasBetterPathAt n,(k-'2*n)
implies it.k=newpathcost(f,n,k-'2*n)) & (not f hasBetterPathAt n,(k-'2*n)
implies it.k=f.k)) &
(k<=n or k > 3*n implies it.k=f.k);
end;
definition let n be Nat;
func Relax(n) -> Element of Funcs(REAL*,REAL*) means
:: GRAPHSP:def 15
dom it = REAL* & for f be Element of REAL* holds
it.f=Relax(f,n);
end;
theorem :: GRAPHSP:36
dom ((Relax n).f) = dom f;
theorem :: GRAPHSP:37
(i <= n or i > 3*n) & i in dom f implies (Relax n).f.i=f.i;
theorem :: GRAPHSP:38
dom ((repeat(Relax(n)*findmin(n))).i.f) =
dom ((repeat(Relax(n)*findmin(n))).(i+1).f);
theorem :: GRAPHSP:39
OuterVx((repeat(Relax(n)*findmin(n))).i.f,n) <> {} implies
UnusedVx((repeat(Relax(n)*findmin(n))).(i+1).f,n) c<
UnusedVx((repeat(Relax(n)*findmin(n))).i.f,n);
theorem :: GRAPHSP:40
g=(repeat(Relax(n)*findmin(n))).i.f &
h=(repeat(Relax(n)*findmin(n))).(i+1).f &
k=Argmin(OuterVx(g,n),g,n) & OuterVx(g,n) <> {} implies
UsedVx(h,n)=UsedVx(g,n) \/ {k} & not k in UsedVx(g,n);
theorem :: GRAPHSP:41
ex i st i<=n & OuterVx((repeat(Relax(n)*findmin(n))).i.f,n) = {};
theorem :: GRAPHSP:42
dom f = dom ((repeat(Relax(n)*findmin(n))).i.f);
definition
let f,g be Element of REAL*,m,n;
pred f,g equal_at m,n means
:: GRAPHSP:def 16
dom f = dom g & for k st k in dom f & m <=k & k <= n holds f.k=g.k;
end;
theorem :: GRAPHSP:43
f,f equal_at m,n;
theorem :: GRAPHSP:44
f,g equal_at m,n & g,h equal_at m,n implies f,h equal_at m,n;
theorem :: GRAPHSP:45
(repeat(Relax(n)*findmin(n))).i.f, (repeat(Relax(n)*findmin(n))).(i+1).f
equal_at 3*n+1,n*n+3*n;
theorem :: GRAPHSP:46
for F being Element of Funcs(REAL*,REAL*),f being Element of REAL*,n,i be Nat
st i < LifeSpan(F,f,n) holds OuterVx((repeat F).i.f,n) <> {};
theorem :: GRAPHSP:47
f, (repeat(Relax(n)*findmin(n))).i.f equal_at 3*n+1,n*n+3*n;
theorem :: GRAPHSP:48
1<=n & 1 in dom f & f.(n+1) <> -1 & (for i st 1<=i & i<=n holds f.i=1) &
(for i st 2<=i & i<=n holds f.(n+i)=-1) implies 1 = Argmin(OuterVx(f,n),f,n) &
UsedVx(f,n)={} & {1} = UsedVx((repeat(Relax(n)*findmin(n))).1.f,n);
theorem :: GRAPHSP:49
g=(repeat(Relax(n)*findmin(n))).1.f & h=(repeat(Relax(n)*findmin(n))).i.f
& 1<=i & i <= LifeSpan(Relax(n)*findmin(n),f,n) & m in UsedVx(g,n)
implies m in UsedVx(h,n);
definition
let p be FinSequence of NAT,f be Element of REAL*,i,n be Nat;
pred p is_vertex_seq_at f,i,n means
:: GRAPHSP:def 17
p.(len p)=i & for k st 1<=k & k < len p holds
p.(len p-k)=f.(n+p/.(len p-k+1));
end;
definition
let p be FinSequence of NAT,f be Element of REAL*,i,n be Nat;
pred p is_simple_vertex_seq_at f,i,n means
:: GRAPHSP:def 18
(p.1=1 & len p > 1 & p is_vertex_seq_at f,i,n) & p is one-to-one;
end;
theorem :: GRAPHSP:50
for p,q being FinSequence of NAT,f be Element of REAL*,i,n be Nat
st p is_simple_vertex_seq_at f,i,n & q is_simple_vertex_seq_at f,i,n
holds p = q;
definition
let G be Graph,p be FinSequence of the Edges of G,vs be FinSequence;
pred p is_oriented_edge_seq_of vs means
:: GRAPHSP:def 19
len vs = len p + 1 &
for n st 1<=n & n<=len p holds (the Source of G).(p.n) = vs.n
& (the Target of G).(p.n) = vs.(n+1);
end;
theorem :: GRAPHSP:51
for G being oriented Graph,vs be FinSequence,p,q being oriented Chain of G st
p is_oriented_edge_seq_of vs & q is_oriented_edge_seq_of vs holds p=q;
theorem :: GRAPHSP:52
for G being Graph,vs1,vs2 be FinSequence,p being oriented Chain of G st p
is_oriented_edge_seq_of vs1 & p is_oriented_edge_seq_of vs2 & len p >= 1
holds vs1=vs2;
begin :: Data structure for Dijkstra's shortest path algorithm
:: address possible value init. value comment
:: 1 1 or -1 1 -1 if node v1 is used
:: 2 1 or -1 1 -1 if node v2 is used
:: : : : :
:: n 1 or -1 1 -1 if node vn is used
:: n+1 0 0 preceding-node of v1 toward v1
:: n+2 -1 or Node No. -1 preceding-node of v2 toward v1
:: : : : :
:: 2*n -1 or Node No. -1 preceding-node of vn toward v1
:: 2*n+1 0 0 cost from v1 to v1
:: 2*n+2 >=0 0 minimum cost from v2 to v1
:: : : : :
:: 3*n >=0 0 minimum cost from vn to v1
:: 3*n+1 weight(v1,v1) the weight of edge(v1,v1)
:: 3*n+2 weight(v1,v2) the weight of edge(v1,v2)
:: : : :
:: 4*n weight(v1,vn) the weight of edge(v1,vn)
:: : : :
:: n*n+3*n weight(vn,vn) the weight of edge(vn,vn)
:: n*n+3n+1 Node No. current node with the shortest path
definition
let f be Element of REAL*,G be oriented Graph,n be Nat,
W be Function of (the Edges of G), Real>=0;
pred f is_Input_of_Dijkstra_Alg G,n,W means
:: GRAPHSP:def 20
len f=n*n+3*n+1 & Seg n=the Vertices of G &
(for i st 1 <= i & i <= n holds f.i=1 & f.(2*n+i)=0) &
f.(n+1)=0 & (for i st 2 <= i & i <= n holds f.(n+i)=-1) &
(for i,j being Vertex of G,k,m st k=i & m=j holds
f.(2*n+n*k+m)=Weight(i,j,W));
end;
begin :: The definition of Dijkstra's shortest path algorithm
definition let n be Nat;
func DijkstraAlgorithm n -> Element of Funcs(REAL*,REAL*) equals
:: GRAPHSP:def 21
while_do(Relax(n)*findmin(n),n);
end;
begin :: Justifying the correctness of Dijkstra's shortest path algorithm
reserve p,q for FinSequence of NAT,
G for finite oriented Graph,
P,Q,R for oriented Chain of G,
W for Function of (the Edges of G), Real>=0,
v1,v2,v3,v4 for Vertex of G;
theorem :: GRAPHSP:53
f is_Input_of_Dijkstra_Alg G,n,W & v1=1 & 1 <> v2 & v2=i & n >= 1 &
g=(DijkstraAlgorithm(n)).f implies the Vertices of G = UsedVx(g,n) \/
UnusedVx(g,n) & (v2 in UsedVx(g,n) implies ex p,P st
p is_simple_vertex_seq_at g,i,n & P is_oriented_edge_seq_of p &
P is_shortestpath_of v1,v2,W & cost(P,W)=g.(2*n+i)) &
(v2 in UnusedVx(g,n) implies not ex Q st Q is_orientedpath_of v1,v2);
Back to top