Journal of Formalized Mathematics
Volume 14, 2002
University of Bialystok
Copyright (c) 2002 Association of Mizar Users

### Processes in Petri nets

by
Grzegorz Bancerek,
Mitsuru Aoki,
Akio Matsumoto, and
Yasunari Shidama

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

```environ

vocabulary PNPROC_1, TARSKI, RELAT_1, FUNCT_1, BOOLE, MCART_1, ARYTM_1, NET_1,
FINSEQ_1, FUNCT_2, FUNCT_7, FUNCOP_1, PRALG_1, FINSEQ_4, CARD_1,
FINSET_1, PETRI, RELOC, INT_1;
notation TARSKI, XBOOLE_0, DOMAIN_1, RELAT_1, FUNCT_1, SUBSET_1, FINSET_1,
CARD_1, FINSEQ_1, FUNCT_2, FUNCOP_1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1,
BINARITH, MCART_1, FINSEQ_2, FINSEQ_4, LANG1, PRALG_1, FUNCT_7, INT_1,
GRAPH_2;
constructors WELLORD2, DOMAIN_1, INT_1, FINSEQ_4, FUNCT_7, BINARITH, GRAPH_2,
MEMBERED;
clusters RELAT_1, RELSET_1, FUNCT_1, FUNCT_7, FUNCOP_1, SUBSET_1, FINSEQ_1,
HEYTING2, PRELAMB, INT_1, MEMBERED, NUMBERS, ORDINAL2;
requirements BOOLE, SUBSET, REAL, NUMERALS, ARITHM;

begin :: Preliminaries

reserve i,j,k,l for Nat,
x,x1,x2,y1,y2 for set;

theorem :: PNPROC_1:1
i > 0 implies {[i,x]} is FinSubsequence;

theorem :: PNPROC_1:2
for q being FinSubsequence holds q = {} iff Seq q = {};

theorem :: PNPROC_1:3
for q being FinSubsequence st q = {[i,x]} holds Seq q = <*x*>;

definition
cluster -> finite FinSubsequence;
end;

theorem :: PNPROC_1:4
for q being FinSubsequence st Seq q = <*x*>
ex i st q = {[i,x]};

theorem :: PNPROC_1:5
{[x1,y1], [x2,y2]} is FinSequence implies
x1 = 1 & x2 = 1 & y1 = y2 or
x1 = 1 & x2 = 2 or
x1 = 2 & x2 = 1;

theorem :: PNPROC_1:6
<*x1,x2*> = {[1,x1], [2,x2]};

theorem :: PNPROC_1:7
for p being FinSubsequence holds Card p = len Seq p;

theorem :: PNPROC_1:8
for P,R being Relation st dom P misses dom R holds P misses R;

theorem :: PNPROC_1:9
for X,Y being set, P,R being Relation st X misses Y holds P|X misses R|Y;

theorem :: PNPROC_1:10
for f,g,h being Function st
f c= h & g c= h & f misses g holds dom f misses dom g;

theorem :: PNPROC_1:11
for Y being set, R being Relation holds Y|R c= R|(R"Y);

theorem :: PNPROC_1:12
for Y being set, f being Function holds Y|f = f|(f"Y);

begin :: Markings on Petri nets

definition let P be set;
mode marking of P -> Function means
:: PNPROC_1:def 1
dom it = P & rng it c= NAT;
end;

reserve P,p,x,y,x1,x2,y1,y2 for set,
m1,m2,m3,m4,m for marking of P,
i,j,j1,j2,k,k1,k2,l,l1,l2 for Nat;

definition
let P be set;
let m be marking of P;
let p be set;
redefine func m.p -> Nat;
synonym m multitude_of p;
end;

scheme MarkingLambda { P() -> set, F(set) -> Nat }:
ex m being marking of P() st
for p st p in P() holds m multitude_of p = F(p);

definition let P,m1,m2;
redefine pred m1 = m2 means
:: PNPROC_1:def 2
for p st p in P holds m1 multitude_of p = m2 multitude_of p;
end;

definition let P;
func {\$} P -> marking of P equals
:: PNPROC_1:def 3
P --> 0;
end;

definition
let P be set;
let m1, m2 be marking of P;
pred m1 c= m2 means
:: PNPROC_1:def 4
for p being set st p in P holds
m1 multitude_of p <= m2 multitude_of p;
reflexivity;
end;

theorem :: PNPROC_1:13
{\$}P c= m;

theorem :: PNPROC_1:14
m1 c= m2 & m2 c= m3 implies m1 c= m3;

definition
let P be set;
let m1, m2 be marking of P;
func m1 + m2 -> marking of P means
:: PNPROC_1:def 5
for p being set st p in P holds
it multitude_of p = (m1 multitude_of p)+(m2 multitude_of p);
commutativity;
end;

theorem :: PNPROC_1:15
m + {\$}P = m;

definition
let P be set;
let m1, m2 be marking of P such that
m2 c= m1;
func m1 - m2 -> marking of P means
:: PNPROC_1:def 6
for p being set st p in P holds
it multitude_of p = (m1 multitude_of p)-(m2 multitude_of p);
end;

theorem :: PNPROC_1:16
m1 c= m1 + m2;

theorem :: PNPROC_1:17
m - {\$}P = m;

theorem :: PNPROC_1:18
m1 c= m2 & m2 c= m3 implies m3 - m2 c= m3 - m1;

theorem :: PNPROC_1:19
(m1 + m2) - m2 = m1;

theorem :: PNPROC_1:20
m c= m1 & m1 c= m2 implies m1 - m c= m2 - m;

theorem :: PNPROC_1:21
m1 c= m2 implies m2 + m3 -m1 = m2 - m1 + m3;

theorem :: PNPROC_1:22
m1 c= m2 & m2 c= m1 implies m1 = m2;

theorem :: PNPROC_1:23
(m1 + m2) + m3 = m1 + (m2 + m3);

theorem :: PNPROC_1:24
m1 c= m2 & m3 c= m4 implies m1 + m3 c= m2 + m4;

theorem :: PNPROC_1:25
m1 c= m2 implies m2 - m1 c= m2;

theorem :: PNPROC_1:26
m1 c= m2 & m3 c= m4 & m4 c= m1 implies m1 - m4 c= m2 - m3;

::  a1 c= a2 & a2 c= a3 implies a3 - a2 c= a3 - a1 by T6';
::  a c= a1 & a1 c= a2 implies a1 - a c= a2 -a by T6';

theorem :: PNPROC_1:27
m1 c= m2 implies m2 = (m2 - m1) + m1;

theorem :: PNPROC_1:28
(m1 + m2) - m1 = m2;

theorem :: PNPROC_1:29
m2 + m3 c= m1 implies (m1 - m2) - m3 = m1 - (m2 + m3);

theorem :: PNPROC_1:30
m3 c= m2 & m2 c= m1 implies m1 - (m2 - m3) = (m1 - m2) + m3;

theorem :: PNPROC_1:31
m in Funcs(P, NAT);

theorem :: PNPROC_1:32
x in Funcs(P, NAT) implies x is marking of P;

begin :: Transitions and firing

definition let P;
mode transition of P means
:: PNPROC_1:def 7
ex m1,m2 st it=[m1,m2];
end;

reserve t,t1,t2 for transition of P;

definition
let P,t;
redefine func t`1 -> marking of P;
synonym Pre t;
func t`2 -> marking of P;
synonym Post t;
end;

definition
let P, m, t;
func fire(t,m) -> marking of P equals
:: PNPROC_1:def 8
(m - Pre t) + Post t if Pre t c= m
otherwise m;
end;

theorem :: PNPROC_1:33
(Pre t1) + (Pre t2) c= m implies
fire(t2, fire(t1,m)) = (m - (Pre t1) - Pre t2) + (Post t1) + (Post t2);

definition
let P, t;
func fire t -> Function means
:: PNPROC_1:def 9
dom it = Funcs(P, NAT) &
for m being marking of P holds it.m = fire(t,m);
end;

theorem :: PNPROC_1:34
rng fire t c= Funcs(P, NAT);

theorem :: PNPROC_1:35
fire(t2, fire(t1,m)) = ((fire t2)*(fire t1)).m;

definition
let P;
mode Petri_net of P -> non empty set means
:: PNPROC_1:def 10
for x being set st x in it holds x is transition of P;
end;

reserve N for Petri_net of P;

definition let P, N;
redefine mode Element of N -> transition of P;
end;

reserve e, e1,e2 for Element of N;

begin :: Firing sequences of transitions

definition let P, N;
mode firing-sequence of N is Element of N*;
end;

reserve C,C1,C2,C3,fs,fs1,fs2 for firing-sequence of N;

definition
let P, N, C;
func fire C -> Function means
:: PNPROC_1:def 11
ex F being Function-yielding FinSequence st
it = compose(F, Funcs(P, NAT)) &
len F = len C &
for i being Nat st i in dom C holds F.i = fire (C /. i qua Element of N);
end;

:: Firing of empty firing-sequence <*>N
theorem :: PNPROC_1:36
fire(<*>N) = id Funcs(P, NAT);

:: Firing of firing-sequence with one translation <*e*>
theorem :: PNPROC_1:37
fire <*e*> = fire e;

theorem :: PNPROC_1:38
(fire e)*id Funcs(P, NAT) = fire e;

:: Firing of firing-sequence with two translations <*e1,e2*>
theorem :: PNPROC_1:39
fire <*e1,e2*> = (fire e2)*(fire e1);

theorem :: PNPROC_1:40
dom fire C = Funcs(P, NAT) & rng fire C c= Funcs(P, NAT);

:: Firing of compound firing-sequence
theorem :: PNPROC_1:41
fire (C1^C2) = (fire C2)*(fire C1);

theorem :: PNPROC_1:42
fire (C^<*e*>) = (fire e)*(fire C);

definition
let P, N, C, m;
func fire(C, m) -> marking of P equals
:: PNPROC_1:def 12
(fire C).m;
end;

begin :: Sequential composition

definition let P, N;
mode process of N is Subset of N*;
end;

reserve R, R1, R2, R3, P1, P2 for process of N;

definition
cluster FinSequence-like -> FinSubsequence-like Function;
end;

definition
let P, N, R1, R2;
func R1 before R2 -> process of N equals
:: PNPROC_1:def 13
{C1^C2: C1 in R1 & C2 in R2};
end;

definition
let P, N;
let R1, R2 be non empty process of N;
cluster R1 before R2 -> non empty;
end;

theorem :: PNPROC_1:43
(R1 \/ R2) before R = (R1 before R) \/ (R2 before R);

theorem :: PNPROC_1:44
R before (R1 \/ R2) = (R before R1) \/ (R before R2);

theorem :: PNPROC_1:45
{C1} before {C2} = {C1^C2};

theorem :: PNPROC_1:46
{C1,C2} before {C} = {C1^C, C2^C};

theorem :: PNPROC_1:47
{C} before {C1,C2} = {C^C1, C^C2};

begin :: Concurrent composition

definition
let P, N, R1, R2;
func R1 concur R2 -> process of N equals
:: PNPROC_1:def 14
{C: ex q1,q2 being FinSubsequence st C = q1 \/ q2 & q1 misses q2 &
Seq q1 in R1 & Seq q2 in R2};
commutativity;
end;

theorem :: PNPROC_1:48
(R1 \/ R2) concur R = (R1 concur R) \/ (R2 concur R);

theorem :: PNPROC_1:49
{<*e1*>} concur {<*e2*>} = {<*e1,e2*>, <*e2,e1*>};

theorem :: PNPROC_1:50
{<*e1*>,<*e2*>} concur {<*e*>} = {<*e1,e*>, <*e2,e*>, <*e,e1*>, <*e,e2*>};

theorem :: PNPROC_1:51
(R1 before R2) before R3 = R1 before (R2 before R3);

definition
let p be FinSubsequence;
let i be Nat;
func i Shift p -> FinSubsequence means
:: PNPROC_1:def 15

dom it = {i+k where k is Nat: k in dom p} &
for j being Nat st j in dom p holds it.(i+j) = p.j;
end;

reserve q,q1,q2,q3,q4 for FinSubsequence;

theorem :: PNPROC_1:52
0 Shift q = q;

theorem :: PNPROC_1:53
(i+j) Shift q = i Shift (j Shift q);

theorem :: PNPROC_1:54
for p being FinSequence st p <> {} holds
dom (i Shift p) = {j1: i+1 <= j1 & j1 <= i+(len p)};

theorem :: PNPROC_1:55
for q being FinSubsequence holds q = {} iff i Shift q = {};

theorem :: PNPROC_1:56
for q being FinSubsequence ex ss being FinSubsequence st
dom ss = dom q & rng ss = dom (i Shift q) &
(for k st k in dom q holds ss.k = i+k) & ss is one-to-one;

theorem :: PNPROC_1:57
for q being FinSubsequence holds Card q = Card (i Shift q);

theorem :: PNPROC_1:58
for p being FinSequence holds dom p = dom Seq (i Shift p);

theorem :: PNPROC_1:59
for p being FinSequence st k in dom p holds (Sgm dom (i Shift p)).k = i + k;

theorem :: PNPROC_1:60
for p being FinSequence st k in dom p holds (Seq (i Shift p)).k = p.k;

theorem :: PNPROC_1:61
for p being FinSequence holds Seq (i Shift p) = p;

reserve p1,p2 for FinSequence;

theorem :: PNPROC_1:62
dom (p1 \/ ((len p1) Shift p2)) = Seg (len p1 + len p2);

theorem :: PNPROC_1:63
for p1 being FinSequence, p2 being FinSubsequence st len p1 <= i holds
dom p1 misses dom (i Shift p2);

theorem :: PNPROC_1:64
for p1,p2 being FinSequence holds p1^p2 = p1 \/ ((len p1) Shift p2);

theorem :: PNPROC_1:65
for p1 being FinSequence, p2 being FinSubsequence st i >= len p1
holds p1 misses i Shift p2;

theorem :: PNPROC_1:66
(R1 concur R2) concur R3 = R1 concur (R2 concur R3);

theorem :: PNPROC_1:67
R1 before R2 c= R1 concur R2;

theorem :: PNPROC_1:68
R1 c= P1 & R2 c= P2 implies R1 before R2 c= P1 before P2;

theorem :: PNPROC_1:69
R1 c= P1 & R2 c= P2 implies R1 concur R2 c= P1 concur P2;

theorem :: PNPROC_1:70
for p,q being FinSubsequence st q c= p holds
i Shift q c= i Shift p;

theorem :: PNPROC_1:71
for p1,p2 being FinSequence holds len p1 Shift p2 c= p1^p2;

theorem :: PNPROC_1:72
dom q1 misses dom q2 implies dom (i Shift q1) misses dom (i Shift q2);

theorem :: PNPROC_1:73
for q,q1,q2 being FinSubsequence st q = q1 \/ q2 & q1 misses q2 holds
(i Shift q1) \/ (i Shift q2) = i Shift q;

theorem :: PNPROC_1:74
for q being FinSubsequence holds dom Seq q = dom Seq (i Shift q);

theorem :: PNPROC_1:75
for q being FinSubsequence st k in dom Seq q
ex j st j = (Sgm dom q).k & (Sgm dom (i Shift q)).k = i + j;

theorem :: PNPROC_1:76
for q being FinSubsequence st
k in dom Seq q holds (Seq (i Shift q)).k = (Seq q).k;

theorem :: PNPROC_1:77
for q being FinSubsequence holds Seq q = Seq (i Shift q);

theorem :: PNPROC_1:78
for q being FinSubsequence st
dom q c= Seg k holds dom (i Shift q) c= Seg (i+k);

theorem :: PNPROC_1:79
for p being FinSequence, q1,q2 being FinSubsequence st q1 c= p
ex ss being FinSubsequence st ss = q1 \/ (len p Shift q2);

theorem :: PNPROC_1:80
for p1,p2 being FinSequence, q1,q2 being FinSubsequence st q1 c= p1 & q2 c= p2
ex ss being FinSubsequence st ss = q1 \/ (len p1 Shift q2) &
dom Seq ss = Seg (len Seq q1 + len Seq q2);

theorem :: PNPROC_1:81
for p1,p2 being FinSequence, q1,q2 being FinSubsequence st q1 c= p1 & q2 c= p2
ex ss being FinSubsequence st ss = q1 \/ (len p1 Shift q2) &
dom Seq ss = Seg (len Seq q1 + len Seq q2) &
Seq ss = Seq q1 \/ (len Seq q1 Shift Seq q2);

theorem :: PNPROC_1:82
for p1,p2 being FinSequence, q1,q2 being FinSubsequence st q1 c= p1 & q2 c= p2
ex ss being FinSubsequence st
ss = q1 \/ (len p1 Shift q2) & (Seq q1)^(Seq q2) = Seq ss;

theorem :: PNPROC_1:83
(R1 concur R2) before (P1 concur P2) c= (R1 before P1) concur (R2 before P2
);

definition
let P, N;
let R1, R2 be non empty process of N;
cluster R1 concur R2 -> non empty;
end;

begin  :: Neutral process

definition let P;
let N be Petri_net of P;
func NeutralProcess(N) -> non empty process of N equals
:: PNPROC_1:def 16
{<*>N};
end;

definition
let P;
let N be Petri_net of P;
let t be Element of N;
func ElementaryProcess(t) -> non empty process of N equals
:: PNPROC_1:def 17
{<*t*>};
end;

theorem :: PNPROC_1:84
NeutralProcess(N) before R = R;

theorem :: PNPROC_1:85
R before NeutralProcess(N) = R;

theorem :: PNPROC_1:86
NeutralProcess(N) concur R = R;
```