:: Definitions of Petri Net - Part II
:: by Waldemar Korczy\'nski
::
:: Received January 31, 1992
:: Copyright (c) 1992-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies STRUCT_0, RELAT_1, TARSKI, ZFMISC_1, XBOOLE_0, SYSREL, E_SIEC;
notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, SYSREL, STRUCT_0;
constructors SYSREL, STRUCT_0, XTUPLE_0;
registrations XBOOLE_0, RELAT_1;
requirements SUBSET, BOOLE;
begin
reserve x,y,z for object,X,Y for set;
definition
struct (1-sorted) G_Net (# carrier -> set, entrance, escape -> Relation #);
end;
definition
let IT be G_Net;
attr IT is GG means
:: E_SIEC:def 1
the entrance of IT c= [:the carrier of IT,the carrier of IT:] &
the escape of IT c= [:the carrier of IT,the carrier of IT:] &
(the entrance of IT) * (the entrance of IT) = the entrance of IT &
(the entrance of IT) * (the escape of IT) = the entrance of IT &
(the escape of IT) * (the escape of IT) = the escape of IT &
(the escape of IT) * (the entrance of IT) = the escape of IT;
end;
registration
cluster GG for G_Net;
end;
definition
mode gg_net is GG G_Net;
end;
definition
let IT be G_Net;
attr IT is EE means
:: E_SIEC:def 2
(the entrance of IT) * ((the entrance of IT) \ id the carrier of IT) = {} &
(the escape of IT) * ((the escape of IT) \ id the carrier of IT) = {};
end;
registration
cluster EE for G_Net;
end;
registration
cluster strict GG EE for G_Net;
end;
definition
mode e_net is EE GG G_Net;
end;
reserve N for e_net;
theorem :: E_SIEC:1
for R, S being Relation holds G_Net (# X, R, S #) is e_net iff
R c= [:X,X:] & S c= [:X,X:] & R * R = R & R * S = R &
S * S = S & S * R = S & R * (R \ id X) = {} & S * (S \ id X) = {};
theorem :: E_SIEC:2
G_Net (# X, {}, {} #) is e_net;
theorem :: E_SIEC:3
G_Net (# X, id X, id X #) is e_net;
theorem :: E_SIEC:4
G_Net (# {}, {}, {} #) is e_net;
theorem :: E_SIEC:5
G_Net (# X, id(X \ Y), id(X \ Y) #) is e_net;
definition
func empty_e_net -> strict e_net equals
:: E_SIEC:def 3
G_Net (# {}, {}, {} #);
end;
definition
let X;
func Tempty_e_net X -> strict e_net equals
:: E_SIEC:def 4
G_Net (# X, id X, id X #);
func Pempty_e_net(X) -> strict e_net equals
:: E_SIEC:def 5
G_Net (# X, {}, {} #);
end;
theorem :: E_SIEC:6
the carrier of Tempty_e_net(X) = X & the entrance of Tempty_e_net(X) = id X &
the escape of Tempty_e_net(X) = id X;
theorem :: E_SIEC:7
the carrier of Pempty_e_net(X) = X & the entrance of Pempty_e_net(X) = {} &
the escape of Pempty_e_net(X) = {};
definition
let x;
func Psingle_e_net(x) -> strict e_net equals
:: E_SIEC:def 6
G_Net (#{x}, id{x}, id{x}#);
func Tsingle_e_net(x) -> strict e_net equals
:: E_SIEC:def 7
G_Net (# {x}, {}, {} #);
end;
theorem :: E_SIEC:8
the carrier of Psingle_e_net(x) = {x} &
the entrance of Psingle_e_net(x) = id{x} &
the escape of Psingle_e_net(x) = id{x};
theorem :: E_SIEC:9
the carrier of Tsingle_e_net(x) = {x} &
the entrance of Tsingle_e_net(x) = {} &
the escape of Tsingle_e_net(x) = {};
theorem :: E_SIEC:10
G_Net (# X \/ Y, id X, id X #) is e_net;
definition
let X,Y;
func PTempty_e_net(X,Y) -> strict e_net equals
:: E_SIEC:def 8
G_Net (#X \/ Y, id(X), id(X)#);
end;
theorem :: E_SIEC:11
(the entrance of N) \ id(dom(the entrance of N)) =
(the entrance of N) \ id the carrier of N &
(the escape of N) \ id(dom(the escape of N)) =
(the escape of N) \ id the carrier of N &
(the entrance of N) \ id(rng(the entrance of N)) =
(the entrance of N) \ id the carrier of N &
(the escape of N) \ id(rng(the escape of N)) =
(the escape of N) \ id the carrier of N;
theorem :: E_SIEC:12
CL the entrance of N = CL the escape of N;
theorem :: E_SIEC:13
rng (the entrance of N) = rng (CL(the entrance of N)) &
rng (the entrance of N) = dom (CL(the entrance of N)) &
rng (the escape of N) = rng (CL(the escape of N)) &
rng (the escape of N) = dom (CL(the escape of N)) &
rng the entrance of N = rng the escape of N;
theorem :: E_SIEC:14
dom (the entrance of N) c= the carrier of N & rng (the entrance
of N) c= the carrier of N & dom (the escape of N) c= the carrier of N & rng (
the escape of N) c= the carrier of N;
theorem :: E_SIEC:15
(the entrance of N) * ((the escape of N) \ id the carrier of N) = {} &
(the escape of N) * ((the entrance of N) \ id the carrier of N) = {};
theorem :: E_SIEC:16
((the entrance of N) \ id(the carrier of N)) *
((the entrance of N) \ id(the carrier of N)) = {} &
((the escape of N) \ id(the carrier of N)) *
((the escape of N) \ id(the carrier of N)) = {} &
((the entrance of N) \ id(the carrier of N)) *
((the escape of N) \ id(the carrier of N)) = {} &
((the escape of N) \ id(the carrier of N)) *
((the entrance of N) \ id(the carrier of N)) = {};
definition
let N;
func e_Places(N) -> set equals
:: E_SIEC:def 9
rng (the entrance of N);
end;
definition
let N;
func e_Transitions(N) -> set equals
:: E_SIEC:def 10
(the carrier of N) \ e_Places(N);
end;
theorem :: E_SIEC:17
([x,y] in the entrance of N or [x,y] in the escape of N) &
x <> y implies x in e_Transitions(N) & y in e_Places(N);
theorem :: E_SIEC:18
(the entrance of N) \ id(the carrier of N) c=
[:e_Transitions(N),e_Places(N):] &
(the escape of N) \ id(the carrier of N) c=
[:e_Transitions(N),e_Places(N):];
definition
let N;
func e_Flow N -> Relation equals
:: E_SIEC:def 11
((the entrance of N)~ \/ (the escape of N)) \ id N;
end;
theorem :: E_SIEC:19
e_Flow N c= [:e_Places(N), e_Transitions(N):] \/
[:e_Transitions(N), e_Places(N):];
definition
let N;
func e_pre(N) -> Relation equals
:: E_SIEC:def 12
(the entrance of N) \ id(the carrier of N);
func e_post(N) -> Relation equals
:: E_SIEC:def 13
(the escape of N) \ id(the carrier of N);
end;
theorem :: E_SIEC:20
e_pre(N) c= [:e_Transitions(N),e_Places(N):] &
e_post(N) c= [:e_Transitions(N),e_Places(N):];
definition
let N;
func e_shore(N) -> set equals
:: E_SIEC:def 14
the carrier of N;
func e_prox(N) -> Relation equals
:: E_SIEC:def 15
((the entrance of N) \/ (the escape of N))~;
func e_flow(N) -> Relation equals
:: E_SIEC:def 16
((the entrance of N)~ \/ (the escape of N)) \/ id(the carrier of N);
end;
theorem :: E_SIEC:21
e_prox(N) c= [:e_shore(N),e_shore(N):] &
e_flow(N) c= [:e_shore(N),e_shore(N):];
theorem :: E_SIEC:22
(e_prox(N)) * (e_prox(N)) = e_prox(N) &
(e_prox(N) \ id(e_shore(N))) * e_prox(N) = {} &
(e_prox(N) \/ (e_prox(N))~) \/ id(e_shore(N)) = e_flow(N) \/ (e_flow(N))~;
theorem :: E_SIEC:23
id((the carrier of N) \ rng(the escape of N)) *
((the escape of N) \ id(the carrier of N)) =
((the escape of N) \ id(the carrier of N)) &
id((the carrier of N) \ rng(the entrance of N)) *
((the entrance of N) \ id(the carrier of N)) =
((the entrance of N) \ id(the carrier of N));
theorem :: E_SIEC:24
((the escape of N) \ id the carrier of N) *
((the escape of N) \ id the carrier of N) = {} &
((the entrance of N) \ id the carrier of N) *
((the entrance of N) \ id the carrier of N) = {} &
((the escape of N) \ id(the carrier of N)) *
((the entrance of N) \ id the carrier of N) = {} &
((the entrance of N) \ id the carrier of N) *
((the escape of N) \ id the carrier of N) = {};
theorem :: E_SIEC:25
((the escape of N) \ id(the carrier of N))~ *
((the escape of N) \ id(the carrier of N))~ = {} &
((the entrance of N) \ id(the carrier of N))~ *
((the entrance of N) \ id(the carrier of N))~ = {};
theorem :: E_SIEC:26
((the escape of N) \ id(the carrier of N))~ * id((the carrier of N) \
rng(the escape of N))~ = ((the escape of N) \ id(the carrier of N))~ &
((the entrance of N) \ id(the carrier of N))~ *
id((the carrier of N) \ rng(the entrance of N))~ =
((the entrance of N) \ id(the carrier of N))~;
theorem :: E_SIEC:27
((the escape of N) \ id(the carrier of N)) *
(id((the carrier of N) \ rng(the escape of N))) = {} &
((the entrance of N) \ id(the carrier of N)) *
(id((the carrier of N) \ rng(the entrance of N))) = {};
theorem :: E_SIEC:28
id((the carrier of N) \ rng(the escape of N)) *
((the escape of N) \ id(the carrier of N))~ = {} &
id((the carrier of N) \ rng(the entrance of N)) *
((the entrance of N) \ id(the carrier of N))~ = {};
definition
let N;
func e_entrance(N) -> Relation equals
:: E_SIEC:def 17
(((the escape of N) \ id(the carrier of N))~) \/
id((the carrier of N) \ rng(the escape of N));
func e_escape(N) -> Relation equals
:: E_SIEC:def 18
(((the entrance of N) \ id(the carrier of N))~) \/
id((the carrier of N) \ rng(the entrance of N));
end;
theorem :: E_SIEC:29
e_entrance(N) * e_entrance(N) = e_entrance(N) &
e_entrance(N) * e_escape(N) = e_entrance(N) &
e_escape(N) * e_entrance(N) = e_escape(N) &
e_escape(N) * e_escape(N) = e_escape(N);
theorem :: E_SIEC:30
e_entrance(N) * (e_entrance(N) \ id(e_shore N)) = {} &
e_escape(N) * (e_escape(N) \ id(e_shore N)) = {};
definition
let N;
func e_adjac(N) -> Relation equals
:: E_SIEC:def 19
(((the entrance of N) \/ (the escape of N)) \ id(the carrier of N))
\/ id((the carrier of N) \ rng(the entrance of N));
end;
theorem :: E_SIEC:31
e_adjac(N) c= [:e_shore(N),e_shore(N):] &
e_flow(N) c= [:e_shore(N),e_shore(N):];
theorem :: E_SIEC:32
(e_adjac(N)) * (e_adjac(N)) = e_adjac(N) &
(e_adjac(N) \ id(e_shore(N))) * e_adjac(N) = {} &
(e_adjac(N) \/ (e_adjac(N))~) \/ id(e_shore(N)) = e_flow(N) \/ (e_flow(N))~;
reserve N for e_net;
theorem :: E_SIEC:33
((the entrance of N) \ id(the carrier of N))~ c=
[:e_Places(N), e_Transitions(N):] &
((the escape of N) \ id(the carrier of N))~ c=
[:e_Places(N),e_Transitions(N):];
definition
let N be G_Net;
func s_pre(N) -> Relation equals
:: E_SIEC:def 20
((the escape of N) \ id(the carrier of N))~;
func s_post(N) -> Relation equals
:: E_SIEC:def 21
((the entrance of N) \ id(the carrier of N))~;
end;
theorem :: E_SIEC:34
s_post(N) c= [:e_Places(N),e_Transitions(N):] &
s_pre(N) c= [:e_Places(N),e_Transitions(N):];