NET_1: Some Elementary Notions of the Theory of Petri Nets

:: Some Elementary Notions of the Theory of Petri Nets
:: by Waldemar Korczy\'nski
::
:: Received August 10, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users

definition

let P be PT_net_Str ;

func Flow P -> set equals :: NET_1:def 1
the S-T_Arcs of P \/ the T-S_Arcs of P;

end;

:: deftheorem defines Flow NET_1:def 1 :

registration

let P be PT_net_Str ;

cluster Flow P -> Relation-like ;

end;

definition

let N be PT_net_Str ;

attr N is Petri means :Def2: :: NET_1:def 2
( 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:] );

end;

:: deftheorem Def2 defines Petri NET_1:def 2 :

:: A Petri net is defined as a triple of the form
:: 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.

definition

let N be PT_net_Str ;

func Elements N -> set equals :: NET_1:def 3
the carrier of N \/ the carrier' of N;

end;

:: deftheorem defines Elements NET_1:def 3 :

theorem :: NET_1:1

for x being set
for N being PT_net_Str holds
( not Elements N <> {} or not x is Element of Elements N or x is Element of the carrier of N or x is Element of the carrier' of N ) by XBOOLE_0:def 3;

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;

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;

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

proof end;

registration

cluster PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) -> Petri ;

coherence by Lm1;

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).

registration

cluster strict Petri for PT_net_Str ;

proof end;

end;

definition

mode Pnet is Petri PT_net_Str ;

end;

:: The above definition defines a Petri net as a TYPE of the structure
:: PT_net_Str. The type is not empty.

theorem Th4: :: NET_1:4

for x being set
for N being Pnet holds
( not x in the carrier of N or not x in the carrier' of N ) by Def2, XBOOLE_0:3;

:: 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.)

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

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

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

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

proof end;

definition

let N be Pnet;
let x, y be set ;

pred pre N,x,y means :: NET_1:def 4
( [y,x] in Flow N & x in the carrier' of N );

pred post N,x,y means :: NET_1:def 5
( [x,y] in Flow N & x in the carrier' of N );

end;

:: deftheorem defines pre NET_1:def 4 :

:: deftheorem defines post NET_1:def 5 :

definition

let N be PT_net_Str ;
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 ) );

proof end;

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 ) );

proof end;

proof end;

end;

:: deftheorem Def6 defines Pre NET_1:def 6 :

:: deftheorem Def7 defines Post NET_1:def 7 :

theorem Th9: :: NET_1:9

for N being Pnet
for x being Element of Elements N holds Pre (N,x) c= Elements N

proof end;

theorem :: NET_1:10

for N being Pnet
for x being Element of Elements N holds Pre (N,x) c= Elements N by Th9;

theorem Th11: :: NET_1:11

for N being Pnet
for x being Element of Elements N holds Post (N,x) c= Elements N

proof end;

theorem :: NET_1:12

for N being Pnet
for x being Element of Elements N holds Post (N,x) c= Elements N by Th11;

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 )

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 )

proof end;

definition

let N be Pnet;
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) ) );

proof end;

uniqueness by A1, XBOOLE_0:def 3;

end;

:: deftheorem Def8 defines enter NET_1:def 8 :

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) )

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

proof end;

theorem :: NET_1:17

for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
enter (N,x) c= Elements N by Th16;

definition

let N be Pnet;
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) ) );

proof end;

uniqueness by A1, XBOOLE_0:def 3;

end;

:: deftheorem Def9 defines exit NET_1:def 9 :

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) )

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

proof end;

theorem :: NET_1:20

for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
exit (N,x) c= Elements N by Th19;

definition

let N be Pnet;
let x be Element of Elements N;

func field (N,x) -> set equals :: NET_1:def 10
(enter (N,x)) \/ (exit (N,x));

end;

:: deftheorem defines field NET_1:def 10 :

definition

let N be PT_net_Str ;
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 ) );

proof end;

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 ) );

proof end;

proof end;

end;

:: deftheorem defines Prec NET_1:def 11 :

:: deftheorem defines Postc NET_1:def 12 :

definition

let N be Pnet;
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) ) ) );

proof end;

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) ) ) );

proof end;

proof end;

end;

:: deftheorem Def13 defines Entr NET_1:def 13 :

:: deftheorem Def14 defines Ext NET_1:def 14 :

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)

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)

proof end;

definition

let N be Pnet;
let X be set ;

func Input (N,X) -> set equals :: NET_1:def 15
union (Entr (N,X));

func Output (N,X) -> set equals :: NET_1:def 16
union (Ext (N,X));

end;

:: deftheorem defines Input NET_1:def 15 :

:: deftheorem defines Output NET_1:def 16 :

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) ) )

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) ) )

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 ) ) )

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 ) ) )

proof end;