:: by Waldemar Korczy\'nski

::

:: Received August 10, 1990

:: Copyright (c) 1990-2021 Association of Mizar Users

:: deftheorem defines Flow NET_1:def 1 :

for P being PT_net_Str holds Flow P = the S-T_Arcs of P \/ the T-S_Arcs of P;

for P being PT_net_Str holds Flow P = the S-T_Arcs of P \/ the T-S_Arcs of P;

registration
end;

:: deftheorem Def2 defines Petri NET_1:def 2 :

for N being PT_net_Str holds

( N is Petri iff ( the carrier of N misses the carrier' of N & Flow N c= [: the carrier of N, the carrier' of N:] \/ [: the carrier' of N, the carrier of N:] ) );

for N being PT_net_Str holds

( N is Petri iff ( the carrier of N misses the carrier' of N & Flow N c= [: the carrier of N, the carrier' of N:] \/ [: the carrier' of N, the carrier of N:] ) );

definition
end;

:: deftheorem defines Elements NET_1:def 3 :

for N being PT_net_Str holds Elements N = the carrier of N \/ the carrier' of N;

for N being PT_net_Str holds Elements N = the carrier of N \/ the carrier' of N;

theorem :: NET_1:1

theorem :: NET_1:2

for x being set

for N being PT_net_Str st x is Element of the carrier of N & the carrier of N <> {} holds

x is Element of Elements N by XBOOLE_1:7, TARSKI:def 3;

for N being PT_net_Str st x is Element of the carrier of N & the carrier of N <> {} holds

x is Element of Elements N by XBOOLE_1:7, TARSKI:def 3;

theorem :: NET_1:3

for x being set

for N being PT_net_Str st x is Element of the carrier' of N & the carrier' of N <> {} holds

x is Element of Elements N by XBOOLE_1:7, TARSKI:def 3;

for N being PT_net_Str st x is Element of the carrier' of N & the carrier' of N <> {} holds

x is Element of Elements N by XBOOLE_1:7, TARSKI:def 3;

Lm1: PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) is Petri

proof end;

:: This lemma is of rather "technical" nature. It allows a definition

:: of a "subtype" of the type PT_net_Str. (see the following definition of the

:: type Pnet).

:: of a "subtype" of the type PT_net_Str. (see the following definition of the

:: type Pnet).

registration
end;

:: The above definition defines a Petri net as a TYPE of the structure

:: PT_net_Str. The type is not empty.

:: PT_net_Str. The type is not empty.

:: This lemma is of rather "technical" character. It will be used in the

:: proof of the correctness of a definition of a function bellow. (See

:: the definition of the functions Enter and Exit.)

:: proof of the correctness of a definition of a function bellow. (See

:: the definition of the functions Enter and Exit.)

theorem Th5: :: NET_1:5

for x, y being set

for N being Pnet st [x,y] in Flow N & x in the carrier' of N holds

y in the carrier of N

for N being Pnet st [x,y] in Flow N & x in the carrier' of N holds

y in the carrier of N

proof end;

theorem Th6: :: NET_1:6

for x, y being set

for N being Pnet st [x,y] in Flow N & y in the carrier' of N holds

x in the carrier of N

for N being Pnet st [x,y] in Flow N & y in the carrier' of N holds

x in the carrier of N

proof end;

theorem :: NET_1:7

for x, y being set

for N being Pnet st [x,y] in Flow N & x in the carrier of N holds

y in the carrier' of N

for N being Pnet st [x,y] in Flow N & x in the carrier of N holds

y in the carrier' of N

proof end;

theorem :: NET_1:8

for x, y being set

for N being Pnet st [x,y] in Flow N & y in the carrier of N holds

x in the carrier' of N

for N being Pnet st [x,y] in Flow N & y in the carrier of N holds

x in the carrier' of N

proof end;

:: deftheorem defines pre NET_1:def 4 :

for N being Pnet

for x, y being set holds

( pre N,x,y iff ( [y,x] in Flow N & x in the carrier' of N ) );

for N being Pnet

for x, y being set holds

( pre N,x,y iff ( [y,x] in Flow N & x in the carrier' of N ) );

:: deftheorem defines post NET_1:def 5 :

for N being Pnet

for x, y being set holds

( post N,x,y iff ( [x,y] in Flow N & x in the carrier' of N ) );

for N being Pnet

for x, y being set holds

( post N,x,y iff ( [x,y] in Flow N & x in the carrier' of N ) );

definition

let N be PT_net_Str ;

let x be Element of Elements N;

ex b_{1} being set st

for y being object holds

( y in b_{1} iff ( y in Elements N & [y,x] in Flow N ) )

for b_{1}, b_{2} being set st ( for y being object holds

( y in b_{1} iff ( y in Elements N & [y,x] in Flow N ) ) ) & ( for y being object holds

( y in b_{2} iff ( y in Elements N & [y,x] in Flow N ) ) ) holds

b_{1} = b_{2}

ex b_{1} being set st

for y being object holds

( y in b_{1} iff ( y in Elements N & [x,y] in Flow N ) )

for b_{1}, b_{2} being set st ( for y being object holds

( y in b_{1} iff ( y in Elements N & [x,y] in Flow N ) ) ) & ( for y being object holds

( y in b_{2} iff ( y in Elements N & [x,y] in Flow N ) ) ) holds

b_{1} = b_{2}

end;
let x be Element of Elements N;

func Pre (N,x) -> set means :Def6: :: NET_1:def 6

for y being object holds

( y in it iff ( y in Elements N & [y,x] in Flow N ) );

existence for y being object holds

( y in it iff ( y in Elements N & [y,x] in Flow N ) );

ex b

for y being object holds

( y in b

proof end;

uniqueness for b

( y in b

( y in b

b

proof end;

func Post (N,x) -> set means :Def7: :: NET_1:def 7

for y being object holds

( y in it iff ( y in Elements N & [x,y] in Flow N ) );

existence for y being object holds

( y in it iff ( y in Elements N & [x,y] in Flow N ) );

ex b

for y being object holds

( y in b

proof end;

uniqueness for b

( y in b

( y in b

b

proof end;

:: deftheorem Def6 defines Pre NET_1:def 6 :

for N being PT_net_Str

for x being Element of Elements N

for b_{3} being set holds

( b_{3} = Pre (N,x) iff for y being object holds

( y in b_{3} iff ( y in Elements N & [y,x] in Flow N ) ) );

for N being PT_net_Str

for x being Element of Elements N

for b

( b

( y in b

:: deftheorem Def7 defines Post NET_1:def 7 :

for N being PT_net_Str

for x being Element of Elements N

for b_{3} being set holds

( b_{3} = Post (N,x) iff for y being object holds

( y in b_{3} iff ( y in Elements N & [x,y] in Flow N ) ) );

for N being PT_net_Str

for x being Element of Elements N

for b

( b

( y in b

theorem :: NET_1:10

theorem :: NET_1:12

theorem :: NET_1:13

for x being set

for N being Pnet

for y being Element of Elements N st y in the carrier' of N holds

( x in Pre (N,y) iff pre N,y,x )

for N being Pnet

for y being Element of Elements N st y in the carrier' of N holds

( x in Pre (N,y) iff pre N,y,x )

proof end;

theorem :: NET_1:14

for x being set

for N being Pnet

for y being Element of Elements N st y in the carrier' of N holds

( x in Post (N,y) iff post N,y,x )

for N being Pnet

for y being Element of Elements N st y in the carrier' of N holds

( x in Post (N,y) iff post N,y,x )

proof end;

definition

let N be Pnet;

let x be Element of Elements N;

assume A1: Elements N <> {} ;

ex b_{1} being set st

( ( x in the carrier of N implies b_{1} = {x} ) & ( x in the carrier' of N implies b_{1} = Pre (N,x) ) )

for b_{1}, b_{2} being set st ( x in the carrier of N implies b_{1} = {x} ) & ( x in the carrier' of N implies b_{1} = Pre (N,x) ) & ( x in the carrier of N implies b_{2} = {x} ) & ( x in the carrier' of N implies b_{2} = Pre (N,x) ) holds

b_{1} = b_{2}
by A1, XBOOLE_0:def 3;

end;
let x be Element of Elements N;

assume A1: Elements N <> {} ;

func enter (N,x) -> set means :Def8: :: NET_1:def 8

( ( x in the carrier of N implies it = {x} ) & ( x in the carrier' of N implies it = Pre (N,x) ) );

existence ( ( x in the carrier of N implies it = {x} ) & ( x in the carrier' of N implies it = Pre (N,x) ) );

ex b

( ( x in the carrier of N implies b

proof end;

uniqueness for b

b

:: deftheorem Def8 defines enter NET_1:def 8 :

for N being Pnet

for x being Element of Elements N st Elements N <> {} holds

for b_{3} being set holds

( b_{3} = enter (N,x) iff ( ( x in the carrier of N implies b_{3} = {x} ) & ( x in the carrier' of N implies b_{3} = Pre (N,x) ) ) );

for N being Pnet

for x being Element of Elements N st Elements N <> {} holds

for b

( b

theorem Th15: :: NET_1:15

for N being Pnet

for x being Element of Elements N holds

( not Elements N <> {} or enter (N,x) = {x} or enter (N,x) = Pre (N,x) )

for x being Element of Elements N holds

( not Elements N <> {} or enter (N,x) = {x} or enter (N,x) = Pre (N,x) )

proof end;

theorem Th16: :: NET_1:16

for N being Pnet

for x being Element of Elements N st Elements N <> {} holds

enter (N,x) c= Elements N

for x being Element of Elements N st Elements N <> {} holds

enter (N,x) c= Elements N

proof end;

theorem :: NET_1:17

definition

let N be Pnet;

let x be Element of Elements N;

assume A1: Elements N <> {} ;

ex b_{1} being set st

( ( x in the carrier of N implies b_{1} = {x} ) & ( x in the carrier' of N implies b_{1} = Post (N,x) ) )

for b_{1}, b_{2} being set st ( x in the carrier of N implies b_{1} = {x} ) & ( x in the carrier' of N implies b_{1} = Post (N,x) ) & ( x in the carrier of N implies b_{2} = {x} ) & ( x in the carrier' of N implies b_{2} = Post (N,x) ) holds

b_{1} = b_{2}
by A1, XBOOLE_0:def 3;

end;
let x be Element of Elements N;

assume A1: Elements N <> {} ;

func exit (N,x) -> set means :Def9: :: NET_1:def 9

( ( x in the carrier of N implies it = {x} ) & ( x in the carrier' of N implies it = Post (N,x) ) );

existence ( ( x in the carrier of N implies it = {x} ) & ( x in the carrier' of N implies it = Post (N,x) ) );

ex b

( ( x in the carrier of N implies b

proof end;

uniqueness for b

b

:: deftheorem Def9 defines exit NET_1:def 9 :

for N being Pnet

for x being Element of Elements N st Elements N <> {} holds

for b_{3} being set holds

( b_{3} = exit (N,x) iff ( ( x in the carrier of N implies b_{3} = {x} ) & ( x in the carrier' of N implies b_{3} = Post (N,x) ) ) );

for N being Pnet

for x being Element of Elements N st Elements N <> {} holds

for b

( b

theorem Th18: :: NET_1:18

for N being Pnet

for x being Element of Elements N holds

( not Elements N <> {} or exit (N,x) = {x} or exit (N,x) = Post (N,x) )

for x being Element of Elements N holds

( not Elements N <> {} or exit (N,x) = {x} or exit (N,x) = Post (N,x) )

proof end;

theorem Th19: :: NET_1:19

for N being Pnet

for x being Element of Elements N st Elements N <> {} holds

exit (N,x) c= Elements N

for x being Element of Elements N st Elements N <> {} holds

exit (N,x) c= Elements N

proof end;

theorem :: NET_1:20

definition

let N be Pnet;

let x be Element of Elements N;

correctness

coherence

(enter (N,x)) \/ (exit (N,x)) is set ;

;

end;
let x be Element of Elements N;

correctness

coherence

(enter (N,x)) \/ (exit (N,x)) is set ;

;

:: deftheorem defines field NET_1:def 10 :

for N being Pnet

for x being Element of Elements N holds field (N,x) = (enter (N,x)) \/ (exit (N,x));

for N being Pnet

for x being Element of Elements N holds field (N,x) = (enter (N,x)) \/ (exit (N,x));

definition

let N be PT_net_Str ;

let x be Element of the carrier' of N;

ex b_{1} being set st

for y being object holds

( y in b_{1} iff ( y in the carrier of N & [y,x] in Flow N ) )

for b_{1}, b_{2} being set st ( for y being object holds

( y in b_{1} iff ( y in the carrier of N & [y,x] in Flow N ) ) ) & ( for y being object holds

( y in b_{2} iff ( y in the carrier of N & [y,x] in Flow N ) ) ) holds

b_{1} = b_{2}

ex b_{1} being set st

for y being object holds

( y in b_{1} iff ( y in the carrier of N & [x,y] in Flow N ) )

for b_{1}, b_{2} being set st ( for y being object holds

( y in b_{1} iff ( y in the carrier of N & [x,y] in Flow N ) ) ) & ( for y being object holds

( y in b_{2} iff ( y in the carrier of N & [x,y] in Flow N ) ) ) holds

b_{1} = b_{2}

end;
let x be Element of the carrier' of N;

func Prec (N,x) -> set means :: NET_1:def 11

for y being object holds

( y in it iff ( y in the carrier of N & [y,x] in Flow N ) );

existence for y being object holds

( y in it iff ( y in the carrier of N & [y,x] in Flow N ) );

ex b

for y being object holds

( y in b

proof end;

uniqueness for b

( y in b

( y in b

b

proof end;

func Postc (N,x) -> set means :: NET_1:def 12

for y being object holds

( y in it iff ( y in the carrier of N & [x,y] in Flow N ) );

existence for y being object holds

( y in it iff ( y in the carrier of N & [x,y] in Flow N ) );

ex b

for y being object holds

( y in b

proof end;

uniqueness for b

( y in b

( y in b

b

proof end;

:: deftheorem defines Prec NET_1:def 11 :

for N being PT_net_Str

for x being Element of the carrier' of N

for b_{3} being set holds

( b_{3} = Prec (N,x) iff for y being object holds

( y in b_{3} iff ( y in the carrier of N & [y,x] in Flow N ) ) );

for N being PT_net_Str

for x being Element of the carrier' of N

for b

( b

( y in b

:: deftheorem defines Postc NET_1:def 12 :

for N being PT_net_Str

for x being Element of the carrier' of N

for b_{3} being set holds

( b_{3} = Postc (N,x) iff for y being object holds

( y in b_{3} iff ( y in the carrier of N & [x,y] in Flow N ) ) );

for N being PT_net_Str

for x being Element of the carrier' of N

for b

( b

( y in b

definition

let N be Pnet;

let X be set ;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ( x c= Elements N & ex y being Element of Elements N st

( y in X & x = enter (N,y) ) ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x c= Elements N & ex y being Element of Elements N st

( y in X & x = enter (N,y) ) ) ) ) & ( for x being set holds

( x in b_{2} iff ( x c= Elements N & ex y being Element of Elements N st

( y in X & x = enter (N,y) ) ) ) ) holds

b_{1} = b_{2}

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ( x c= Elements N & ex y being Element of Elements N st

( y in X & x = exit (N,y) ) ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x c= Elements N & ex y being Element of Elements N st

( y in X & x = exit (N,y) ) ) ) ) & ( for x being set holds

( x in b_{2} iff ( x c= Elements N & ex y being Element of Elements N st

( y in X & x = exit (N,y) ) ) ) ) holds

b_{1} = b_{2}

end;
let X be set ;

func Entr (N,X) -> set means :Def13: :: NET_1:def 13

for x being set holds

( x in it iff ( x c= Elements N & ex y being Element of Elements N st

( y in X & x = enter (N,y) ) ) );

existence for x being set holds

( x in it iff ( x c= Elements N & ex y being Element of Elements N st

( y in X & x = enter (N,y) ) ) );

ex b

for x being set holds

( x in b

( y in X & x = enter (N,y) ) ) )

proof end;

uniqueness for b

( x in b

( y in X & x = enter (N,y) ) ) ) ) & ( for x being set holds

( x in b

( y in X & x = enter (N,y) ) ) ) ) holds

b

proof end;

func Ext (N,X) -> set means :Def14: :: NET_1:def 14

for x being set holds

( x in it iff ( x c= Elements N & ex y being Element of Elements N st

( y in X & x = exit (N,y) ) ) );

existence for x being set holds

( x in it iff ( x c= Elements N & ex y being Element of Elements N st

( y in X & x = exit (N,y) ) ) );

ex b

for x being set holds

( x in b

( y in X & x = exit (N,y) ) ) )

proof end;

uniqueness for b

( x in b

( y in X & x = exit (N,y) ) ) ) ) & ( for x being set holds

( x in b

( y in X & x = exit (N,y) ) ) ) ) holds

b

proof end;

:: deftheorem Def13 defines Entr NET_1:def 13 :

for N being Pnet

for X, b_{3} being set holds

( b_{3} = Entr (N,X) iff for x being set holds

( x in b_{3} iff ( x c= Elements N & ex y being Element of Elements N st

( y in X & x = enter (N,y) ) ) ) );

for N being Pnet

for X, b

( b

( x in b

( y in X & x = enter (N,y) ) ) ) );

:: deftheorem Def14 defines Ext NET_1:def 14 :

for N being Pnet

for X, b_{3} being set holds

( b_{3} = Ext (N,X) iff for x being set holds

( x in b_{3} iff ( x c= Elements N & ex y being Element of Elements N st

( y in X & x = exit (N,y) ) ) ) );

for N being Pnet

for X, b

( b

( x in b

( y in X & x = exit (N,y) ) ) ) );

theorem Th21: :: NET_1:21

for N being Pnet

for x being Element of Elements N

for X being set st Elements N <> {} & x in X holds

enter (N,x) in Entr (N,X)

for x being Element of Elements N

for X being set st Elements N <> {} & x in X holds

enter (N,x) in Entr (N,X)

proof end;

theorem Th22: :: NET_1:22

for N being Pnet

for x being Element of Elements N

for X being set st Elements N <> {} & x in X holds

exit (N,x) in Ext (N,X)

for x being Element of Elements N

for X being set st Elements N <> {} & x in X holds

exit (N,x) in Ext (N,X)

proof end;

definition

let N be Pnet;

let X be set ;

correctness

coherence

union (Entr (N,X)) is set ;

;

correctness

coherence

union (Ext (N,X)) is set ;

;

end;
let X be set ;

correctness

coherence

union (Entr (N,X)) is set ;

;

correctness

coherence

union (Ext (N,X)) is set ;

;

:: deftheorem defines Input NET_1:def 15 :

for N being Pnet

for X being set holds Input (N,X) = union (Entr (N,X));

for N being Pnet

for X being set holds Input (N,X) = union (Entr (N,X));

:: deftheorem defines Output NET_1:def 16 :

for N being Pnet

for X being set holds Output (N,X) = union (Ext (N,X));

for N being Pnet

for X being set holds Output (N,X) = union (Ext (N,X));

theorem :: NET_1:23

for N being Pnet

for x, X being set st X c= Elements N holds

( x in Input (N,X) iff ex y being Element of Elements N st

( y in X & x in enter (N,y) ) )

for x, X being set st X c= Elements N holds

( x in Input (N,X) iff ex y being Element of Elements N st

( y in X & x in enter (N,y) ) )

proof end;

theorem :: NET_1:24

for N being Pnet

for x, X being set st X c= Elements N holds

( x in Output (N,X) iff ex y being Element of Elements N st

( y in X & x in exit (N,y) ) )

for x, X being set st X c= Elements N holds

( x in Output (N,X) iff ex y being Element of Elements N st

( y in X & x in exit (N,y) ) )

proof end;

theorem :: NET_1:25

for N being Pnet

for X being Subset of (Elements N)

for x being Element of Elements N st Elements N <> {} holds

( x in Input (N,X) iff ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st

( y in X & y in the carrier' of N & pre N,y,x ) ) )

for X being Subset of (Elements N)

for x being Element of Elements N st Elements N <> {} holds

( x in Input (N,X) iff ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st

( y in X & y in the carrier' of N & pre N,y,x ) ) )

proof end;

theorem :: NET_1:26

for N being Pnet

for X being Subset of (Elements N)

for x being Element of Elements N st Elements N <> {} holds

( x in Output (N,X) iff ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st

( y in X & y in the carrier' of N & post N,y,x ) ) )

for X being Subset of (Elements N)

for x being Element of Elements N st Elements N <> {} holds

( x in Output (N,X) iff ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st

( y in X & y in the carrier' of N & post N,y,x ) ) )

proof end;

:: N = (carrier, carrier', Flow)

:: with carrier and carrier' being disjoint sets and

:: Flow c= (carrier' x carrier) U (carrier x carrier')

:: It is allowed that both sets carrier and carrier' are empty.

:: A Petri net is here described as a predicate defined in the set

:: (on the mode) PT_net_Str.