Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Some Elementary Notions of the Theory of Petri Nets

by
Waldemar Korczynski

MML identifier: NET_1
[ Mizar article, MML identifier index ]

```environ

vocabulary RELAT_1, BOOLE, TARSKI, NET_1, SETFAM_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1;
constructors REAL_1, SETFAM_1, XBOOLE_0;
clusters RELAT_1, ZFMISC_1, XBOOLE_0;
requirements SUBSET, BOOLE;

begin

definition
struct Net (# Places, Transitions -> set, Flow -> Relation #);
end;

::The above definition describes a "structure  of a Petri net" which
::is a kind of relational system.

reserve x,y for set;
reserve N for Net;

definition
let N be Net;
attr N is Petri means
:: NET_1:def 1
the Places of N misses the Transitions of N &
(the Flow of N) c= [:the Places of N, the Transitions of N:] \/
[:the Transitions of N, the Places of N:];
synonym N is_Petri_net;
end;

:: A Petri net is defined as a triple of the form
::        N = (Places, Transitions, Flow)
:: with Places and Transitions being disjoint sets and
::   Flow c= (Transitions x Places) U (Places x Transitions)
:: It is allowed that both sets Places and Transitions are empty.
:: A Petri net is here described as a predicate defined in the set
:: (on the mode) Net.

definition
let N be Net;
func Elements(N) equals
:: NET_1:def 2
(the Places of N) \/ (the Transitions of N);
end;

:: The set Elements(N) of so called "elements of a Petri net is defined
:: as the union of its Places and Transitions. Here a function assigning
:: to a Petri net such a set is defined.

canceled 3;

theorem :: NET_1:4
(the Places of N) c= Elements(N);

theorem :: NET_1:5
(the Transitions of N) c= Elements(N);

:: The above definition describes the set of elements of a Petri net
:: as a (parametrized) TYPE ("mode" in Mizar) which is sometimes
:: "technically" (because of the Mizar -writing  technology) more
:: convenient.

theorem :: NET_1:6
x in Elements(N) iff
x in the Places of N or x in the Transitions of N;

theorem :: NET_1:7
Elements(N) <> {} implies
(x is Element of Elements(N) implies
x is Element of the Places of N or
x is Element of the Transitions of N);

theorem :: NET_1:8
x is Element of the Places of N &
the Places of N <> {} implies x is Element of Elements(N);

theorem :: NET_1:9
x is Element of the Transitions of N &
the Transitions of N <> {} implies x is Element of Elements(N);

definition
cluster Net (#{}, {}, {}#) -> Petri;
end;

:: This lemma is of rather "technical" nature. It allows a definition
:: of a "subtype" of the type Net. (see the following definition of the
:: type Pnet).

definition
cluster strict Petri Net;
end;

definition
mode Pnet is Petri Net;
end;

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

canceled;

theorem :: NET_1:11
for N being Pnet holds
not (x in the Places of N & x in the Transitions of N);

:: 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 :: NET_1:12
for N being Pnet holds
([x,y] in the Flow of N & x in the Transitions of N)
implies y in the Places of N;

theorem :: NET_1:13
for N being Pnet holds
([x,y] in the Flow of N & y in the Transitions of N)
implies x in the Places of N;

theorem :: NET_1:14
for N being Pnet holds
([x,y] in the Flow of N & x in the Places of N)
implies y in the Transitions of N;

theorem :: NET_1:15
for N being Pnet holds
([x,y] in the Flow of N & y in the Places of N)
implies x in the Transitions of N;

definition
let N be Pnet;
let x,y;
canceled 2;

pred pre N,x,y means
:: NET_1:def 5
[y,x] in the Flow of N & x in the Transitions of N;

pred post N,x,y means
:: NET_1:def 6
[x,y] in the Flow of N & x in the Transitions of N;
end;

definition
let N be Net;
let x be Element of Elements(N);
func Pre(N,x) means
:: NET_1:def 7
y in it iff y in Elements(N) & [y,x] in the Flow of N;

func Post(N,x) means
:: NET_1:def 8
y in it iff y in Elements(N) & [x,y] in the Flow of N;
end;

theorem :: NET_1:16
for N being Pnet
for x being Element of Elements(N) holds Pre(N,x) c= Elements(N);

theorem :: NET_1:17
for N being Pnet
for x being Element of Elements N holds Pre(N,x) c= Elements N;

theorem :: NET_1:18
for N being Pnet
for x being Element of Elements(N) holds Post(N,x) c= Elements(N);

theorem :: NET_1:19
for N being Pnet
for x being Element of Elements N holds Post(N,x) c= Elements N;

theorem :: NET_1:20
for N being Pnet
for y being Element of Elements(N) holds
y in the Transitions of N implies (x in Pre(N,y) iff pre N,y,x);

theorem :: NET_1:21
for N being Pnet
for y being Element of Elements(N) holds
y in the Transitions of N implies (x in Post(N,y) iff post N,y,x);

definition
let N be Pnet;
let x be Element of Elements(N);
assume  Elements(N) <> {};
func enter(N,x) means
:: NET_1:def 9
(x in the Places of N implies it = {x}) &
(x in the Transitions of N implies it = Pre(N,x));
end;

theorem :: NET_1:22
for N being Pnet for x being Element of Elements(N) holds
Elements(N) <> {} implies enter(N,x) ={x} or enter(N,x) = Pre(N,x);

theorem :: NET_1:23
for N being Pnet for x being Element of Elements(N) holds
Elements(N) <> {} implies enter(N,x) c= Elements(N);

theorem :: NET_1:24
for N being Pnet
for x being Element of Elements N holds
Elements N <> {} implies enter(N,x) c= Elements N;

definition
let N be Pnet;
let x be Element of Elements(N);
assume  Elements(N) <> {};
func exit(N,x) -> set means
:: NET_1:def 10
(x in the Places of N implies it = {x}) &
(x in the Transitions of N implies it = Post(N,x));
end;

theorem :: NET_1:25
for N being Pnet for x being Element of Elements(N) holds
Elements(N) <> {} implies exit(N,x) ={x} or
exit(N,x) = Post(N,x);

theorem :: NET_1:26
for N being Pnet for x being Element of Elements(N) holds
Elements(N) <> {} implies exit(N,x) c= Elements(N);

theorem :: NET_1:27
for N being Pnet
for x being Element of Elements N holds
Elements N <> {} implies exit(N,x) c= Elements N;

definition
let N be Pnet;
let x be Element of Elements(N);
func field(N,x) equals
:: NET_1:def 11
enter(N,x) \/ exit(N,x);
end;

definition
let N be Net;
let x be Element of the Transitions of N;
func Prec(N,x) means
:: NET_1:def 12
y in it iff y in the Places of N &
[y,x] in the Flow of N;

func Postc(N,x) means
:: NET_1:def 13
y in it iff y in the Places of N & [x,y] in the Flow of N;
end;

definition
let N be Pnet;
let X be set;
func Entr(N,X) means
:: NET_1:def 14
x in it iff x c= Elements N &
ex y being Element of Elements N st y in X & x = enter(N,y);

func Ext(N,X) means
:: NET_1:def 15
x in it iff x c= Elements N &
ex y being Element of Elements N st y in X & x = exit(N,y);
end;

theorem :: NET_1:28
for N being Pnet
for x being Element of Elements(N)
for X being set holds
Elements(N) <> {} & X c= Elements(N) & x in X implies
enter(N,x) in Entr(N,X);

theorem :: NET_1:29
for N being Pnet
for x being Element of Elements(N)
for X being set holds
Elements(N) <> {} & X c= Elements(N) & x in X implies
exit(N,x) in Ext(N,X);

definition
let N be Pnet;
let X be set;
func Input(N,X) equals
:: NET_1:def 16
union Entr(N,X);

func Output(N,X) equals
:: NET_1:def 17
union Ext(N,X);
end;

theorem :: NET_1:30
for N being Pnet for x for X being set holds
Elements(N) <> {} & X c= Elements(N) implies
(x in Input(N,X) iff
ex y being Element of Elements(N) st y in X & x in enter(N,y));

theorem :: NET_1:31
for N being Pnet for x for X being set holds
Elements(N) <> {} & X c= Elements(N) implies
(x in Output(N,X) iff
ex y being Element of Elements(N) st
y in X & x in exit(N,y));

theorem :: NET_1:32
for N being Pnet
for X being Subset of Elements(N)
for x being Element of Elements(N) holds
Elements(N) <> {} implies
(x in Input(N,X) iff
(x in X & x in the Places of N or
ex y being Element of Elements(N) st y in X &
y in the Transitions of N & pre N,y,x));

theorem :: NET_1:33
for N being Pnet
for X being Subset of Elements(N)
for x being Element of Elements(N) holds
Elements(N) <> {} implies
(x in Output(N,X) iff
(x in X & x in the Places of N or
ex y being Element of Elements(N) st y in X &
y in the Transitions of N & post N,y,x));
```