begin
Lm1:
for F being Function
for x, y being set holds dom (F +* (x .--> y)) = (dom F) \/ {x}
Lm2:
for F being Function
for x, y, z being set st z in dom (F +* (x .--> y)) & not z in dom F holds
x = z
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
for
A being
set for
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
for
A being
set for
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
for
A1,
A2 being
set for
b1 being
Rbag of
A1 for
b2 being
Rbag of
A2 st
b1 = b2 holds
Sum b1 = Sum b2
theorem Th8:
theorem
begin
:: deftheorem Def1 defines is_mincost_DTree_rooted_at GLIB_004:def 1 :
for G1 being real-weighted WGraph
for G2 being WSubgraph of G1
for v being set holds
( G2 is_mincost_DTree_rooted_at v iff ( G2 is Tree-like & ( for x being Vertex of G2 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() ) ) ) ) );
:: deftheorem Def2 defines is_mincost_DPath_from GLIB_004:def 2 :
for G being real-weighted WGraph
for W being DPath of G
for x, y being set holds
( W is_mincost_DPath_from x,y iff ( W is_Walk_from x,y & ( for W2 being DPath of G st W2 is_Walk_from x,y holds
W .cost() <= W2 .cost() ) ) );
definition
let G be
finite real-weighted WGraph;
let x,
y be
set ;
func G .min_DPath_cost (
x,
y)
-> Real means :
Def3:
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 ;
existence
( ( ex W being DWalk of G st W is_Walk_from x,y implies ex b1 being Real ex W being DPath of G st
( W is_mincost_DPath_from x,y & b1 = W .cost() ) ) & ( ( for W being DWalk of G holds not W is_Walk_from x,y ) implies ex b1 being Real st b1 = 0 ) )
uniqueness
for b1, b2 being Real holds
( ( ex W being DWalk of G st W is_Walk_from x,y & ex W being DPath of G st
( W is_mincost_DPath_from x,y & b1 = W .cost() ) & ex W being DPath of G st
( W is_mincost_DPath_from x,y & b2 = W .cost() ) implies b1 = b2 ) & ( ( for W being DWalk of G holds not W is_Walk_from x,y ) & b1 = 0 & b2 = 0 implies b1 = b2 ) )
consistency
for b1 being Real holds verum
;
end;
:: deftheorem Def3 defines .min_DPath_cost GLIB_004:def 3 :
for G being finite real-weighted WGraph
for x, y being set
for b4 being Real holds
( ( ex W being DWalk of G st W is_Walk_from x,y implies ( b4 = G .min_DPath_cost (x,y) iff ex W being DPath of G st
( W is_mincost_DPath_from x,y & b4 = W .cost() ) ) ) & ( ( for W being DWalk of G holds not W is_Walk_from x,y ) implies ( b4 = G .min_DPath_cost (x,y) iff b4 = 0 ) ) );
:: deftheorem defines WGraphSelectors GLIB_004:def 4 :
WGraphSelectors = {VertexSelector,EdgeSelector,SourceSelector,TargetSelector,WeightSelector};
Lm3:
for G being WGraph holds WGraphSelectors c= dom G
Lm4:
for G being WGraph holds
( G == G | WGraphSelectors & the_Weight_of G = the_Weight_of (G | WGraphSelectors) )
Lm5:
for G being WGraph holds dom (G | WGraphSelectors) = WGraphSelectors
:: deftheorem Def5 defines .allWSubgraphs() GLIB_004:def 5 :
for G being WGraph
for b2 being non empty set holds
( b2 = G .allWSubgraphs() iff for x being set holds
( x in b2 iff ex G2 being WSubgraph of G st
( x = G2 & dom G2 = WGraphSelectors ) ) );
:: deftheorem defines .cost() GLIB_004:def 6 :
for G being finite real-weighted WGraph holds G .cost() = Sum (the_Weight_of G);
theorem Th10:
theorem Th11:
theorem Th12:
theorem
theorem Th14:
begin
definition
let G be
real-weighted WGraph;
let L be
DIJK:Labeling of
G;
func DIJK:NextBestEdges L -> Subset of
(the_Edges_of G) means :
Def7:
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) ) ) );
existence
ex b1 being Subset of (the_Edges_of G) st
for e1 being set holds
( e1 in b1 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) ) ) )
uniqueness
for b1, b2 being Subset of (the_Edges_of G) st ( for e1 being set holds
( e1 in b1 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) ) ) ) ) & ( for e1 being set holds
( e1 in b2 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) ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def7 defines DIJK:NextBestEdges GLIB_004:def 7 :
for G being real-weighted WGraph
for L being DIJK:Labeling of G
for b3 being Subset of (the_Edges_of G) holds
( b3 = DIJK:NextBestEdges L iff for e1 being set holds
( e1 in b3 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) ) ) ) );
:: deftheorem Def8 defines DIJK:Step GLIB_004:def 8 :
for G being real-weighted WGraph
for L being DIJK:Labeling of G holds
( ( DIJK:NextBestEdges L = {} implies DIJK:Step L = L ) & ( not DIJK:NextBestEdges L = {} implies DIJK:Step L = [((L `1) +* (((the_Target_of G) . (choose (DIJK:NextBestEdges L))) .--> (((L `1) . ((the_Source_of G) . (choose (DIJK:NextBestEdges L)))) + ((the_Weight_of G) . (choose (DIJK:NextBestEdges L)))))),((L `2) \/ {(choose (DIJK:NextBestEdges L))})] ) );
:: deftheorem defines DIJK:Init GLIB_004:def 9 :
for G being real-weighted WGraph
for src being Vertex of G holds DIJK:Init src = [(src .--> 0),{}];
:: deftheorem Def10 defines DIJK:LabelingSeq GLIB_004:def 10 :
for G being real-weighted WGraph
for b2 being ManySortedSet of NAT holds
( b2 is DIJK:LabelingSeq of G iff for n being Nat holds b2 . n is DIJK:Labeling of G );
:: deftheorem Def11 defines DIJK:CompSeq GLIB_004:def 11 :
for G being real-weighted WGraph
for src being Vertex of G
for b3 being DIJK:LabelingSeq of G holds
( b3 = DIJK:CompSeq src iff ( b3 . 0 = DIJK:Init src & ( for n being Nat holds b3 . (n + 1) = DIJK:Step (b3 . n) ) ) );
:: deftheorem defines DIJK:SSSP GLIB_004:def 12 :
for G being real-weighted WGraph
for src being Vertex of G holds DIJK:SSSP (G,src) = (DIJK:CompSeq src) .Result() ;
begin
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem
begin
definition
let G be
real-weighted WGraph;
let L be
PRIM:Labeling of
G;
func PRIM:NextBestEdges L -> Subset of
(the_Edges_of G) means :
Def13:
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 ) ) );
existence
ex b1 being Subset of (the_Edges_of G) st
for e1 being set holds
( e1 in b1 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 ) ) )
uniqueness
for b1, b2 being Subset of (the_Edges_of G) st ( for e1 being set holds
( e1 in b1 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 ) ) ) ) & ( for e1 being set holds
( e1 in b2 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 ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def13 defines PRIM:NextBestEdges GLIB_004:def 13 :
for G being real-weighted WGraph
for L being PRIM:Labeling of G
for b3 being Subset of (the_Edges_of G) holds
( b3 = PRIM:NextBestEdges L iff for e1 being set holds
( e1 in b3 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 ) ) ) );
:: deftheorem defines PRIM:Init GLIB_004:def 14 :
for G being real-weighted WGraph holds PRIM:Init G = [{(choose (the_Vertices_of G))},{}];
:: deftheorem Def15 defines PRIM:Step GLIB_004:def 15 :
for G being real-weighted WGraph
for L being PRIM:Labeling of G holds
( ( PRIM:NextBestEdges L = {} implies PRIM:Step L = L ) & ( PRIM:NextBestEdges L <> {} & (the_Source_of G) . (choose (PRIM:NextBestEdges L)) in L `1 implies PRIM:Step L = [((L `1) \/ {((the_Target_of G) . (choose (PRIM:NextBestEdges L)))}),((L `2) \/ {(choose (PRIM:NextBestEdges L))})] ) & ( not PRIM:NextBestEdges L = {} & ( not PRIM:NextBestEdges L <> {} or not (the_Source_of G) . (choose (PRIM:NextBestEdges L)) in L `1 ) implies PRIM:Step L = [((L `1) \/ {((the_Source_of G) . (choose (PRIM:NextBestEdges L)))}),((L `2) \/ {(choose (PRIM:NextBestEdges L))})] ) );
:: deftheorem Def16 defines PRIM:LabelingSeq GLIB_004:def 16 :
for G being real-weighted WGraph
for b2 being ManySortedSet of NAT holds
( b2 is PRIM:LabelingSeq of G iff for n being Nat holds b2 . n is PRIM:Labeling of G );
:: deftheorem Def17 defines PRIM:CompSeq GLIB_004:def 17 :
for G being real-weighted WGraph
for b2 being PRIM:LabelingSeq of G holds
( b2 = PRIM:CompSeq G iff ( b2 . 0 = PRIM:Init G & ( for n being Nat holds b2 . (n + 1) = PRIM:Step (b2 . n) ) ) );
:: deftheorem defines PRIM:MST GLIB_004:def 18 :
for G being real-weighted WGraph holds PRIM:MST G = (PRIM:CompSeq G) .Result() ;
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
:: deftheorem Def19 defines min-cost GLIB_004:def 19 :
for G1 being finite connected real-weighted WGraph
for G2 being spanning Tree-like WSubgraph of G1 holds
( G2 is min-cost iff for G3 being spanning Tree-like WSubgraph of G1 holds G2 .cost() <= G3 .cost() );
begin
theorem
theorem Th41:
theorem Th42:
theorem