The abstract of the Mizar article:

Definitions of Petri Net. Part II

by

Waldemar Korczynski

Received January 31, 1992

MML identifier: E_SIEC

[ Mizar article, MML identifier index ]

environ

 vocabulary RELAT_1, BOOLE, SYSREL, E_SIEC, FUNCT_1, S_SIEC;
 notation TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, SYSREL, STRUCT_0;
 constructors SYSREL, STRUCT_0, XBOOLE_0;
 clusters RELAT_1, SYSREL, ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

 reserve x,y,z,X,Y for set;

:: D E F I N I T I O N S

definition
 struct (1-sorted) G_Net (# carrier -> set,
                           entrance, escape -> Relation #);
end;

definition let N be 1-sorted;
 func echaos N -> set equals
:: E_SIEC:def 1
 (the carrier of N) \/ {the carrier of N};
end;

definition let IT be G_Net;
 attr IT is GG means
:: E_SIEC:def 2
  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;

definition
 cluster GG 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 3
 (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;

definition
 cluster EE G_Net;
end;

definition
 cluster strict GG EE 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;

canceled 3;

theorem :: E_SIEC:8
   G_Net (# X, id(X \ Y), id(X \ Y) #) is e_net;

theorem :: E_SIEC:9
   echaos N <> {};

definition
 func empty_e_net -> strict e_net equals
:: E_SIEC:def 4
    G_Net (# {}, {}, {} #);
end;

definition let X;
 func Tempty_e_net X -> strict e_net equals
:: E_SIEC:def 5
  G_Net (# X, id X, id X #);
 func Pempty_e_net(X) -> strict e_net equals
:: E_SIEC:def 6
  G_Net (# X, {}, {} #);
end;

canceled;

theorem :: E_SIEC:11
   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:12
   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 7
  G_Net (#{x}, id{x}, id{x}#);
 func Tsingle_e_net(x) -> strict e_net equals
:: E_SIEC:def 8
  G_Net (# {x}, {}, {} #);
end;

theorem :: E_SIEC:13
   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:14
   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:15
 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 9
     G_Net (#X \/ Y, id(X), id(X)#);
end;

theorem :: E_SIEC:16
 (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:17
CL(the entrance of N) = CL(the escape of N);

theorem :: E_SIEC:18
 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:19
 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:20
 (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:21
   ((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 10
 rng (the entrance of N);
end;

definition let N;
 func e_Transitions(N) -> set equals
:: E_SIEC:def 11
  (the carrier of N) \ e_Places(N);
end;

theorem :: E_SIEC:22
   e_Places(N) misses e_Transitions(N);

theorem :: E_SIEC:23
([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:24
(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 12
   ((the entrance of N)~ \/ (the escape of N)) \ id(the carrier of N);
 end;

theorem :: E_SIEC:25
   e_Flow N c= [:e_Places(N) , e_Transitions(N):] \/
                         [:e_Transitions(N) , e_Places(N):];

definition let N;
 redefine func e_Places(N);
  synonym e_places(N);
 redefine func e_Transitions(N);
  synonym e_transitions(N);
end;

 definition let N;
 canceled 2;

  func e_pre(N) -> Relation equals
:: E_SIEC:def 15
   (the entrance of N) \ id(the carrier of N);
  func e_post(N) -> Relation equals
:: E_SIEC:def 16
   (the escape of N) \ id(the carrier of N);
 end;

canceled 2;

theorem :: E_SIEC:28
   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 17
   the carrier of N;
  func e_prox(N) -> Relation equals
:: E_SIEC:def 18
   ((the entrance of N) \/ (the escape of N))~;
  func e_flow(N) -> Relation equals
:: E_SIEC:def 19
   ((the entrance of N)~ \/ (the escape of N)) \/
                                            id(the carrier of N);
 end;

theorem :: E_SIEC:29
   e_prox(N) c= [:e_shore(N),e_shore(N):] &
         e_flow(N) c= [:e_shore(N),e_shore(N):];

theorem :: E_SIEC:30
   (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:31
 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:32
((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:33
((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:34
   ((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:35
((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:36
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;
  redefine func e_shore(N);
   synonym e_support(N);
 end;

 definition let N;
 canceled;

  func e_entrance(N) -> Relation equals
:: E_SIEC:def 21
   (((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 22
   (((the entrance of N) \ id(the carrier of N))~) \/
                id((the carrier of N) \ rng(the entrance of N));
 end;

theorem :: E_SIEC:37
   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:38
   e_entrance(N) * (e_entrance(N) \ id(e_support(N))) = {} &
      e_escape(N) * (e_escape(N) \ id(e_support(N))) = {};

 definition let N;
  redefine func e_shore(N);
   synonym e_stanchion(N);
 end;

 definition let N;
 canceled;

  func e_adjac(N) -> Relation equals
:: E_SIEC:def 24
   (((the entrance of N) \/ (the escape of N)) \
              id(the carrier of N)) \/
               id((the carrier of N) \ rng(the entrance of N));

  redefine func e_flow(N);
   synonym e_circulation(N);
 end;

theorem :: E_SIEC:39
   e_adjac(N) c= [:e_stanchion(N),e_stanchion(N):] &
         e_circulation(N) c= [:e_stanchion(N),e_stanchion(N):];

theorem :: E_SIEC:40
   (e_adjac(N)) * (e_adjac(N)) = e_adjac(N) &
  (e_adjac(N) \ id(e_stanchion(N))) * e_adjac(N) = {} &
   (e_adjac(N) \/ (e_adjac(N))~) \/ id(e_stanchion(N)) =
     e_circulation(N) \/ (e_circulation(N))~;

definition let N be e_net;
 redefine func e_Places N;
  synonym s_transitions N;
 redefine func e_Transitions N;
  synonym s_places N;
 redefine func e_shore N;
  synonym s_carrier N;
 redefine func e_entrance N;
  synonym s_enter N;
 redefine func e_escape N;
  synonym s_exit N;
 redefine func e_adjac N;
  synonym s_prox N;
end;

 reserve N for e_net;

theorem :: E_SIEC:41
((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 25
   ((the escape of N) \ id(the carrier of N))~;
  func s_post(N) -> Relation equals
:: E_SIEC:def 26
   ((the entrance of N) \ id(the carrier of N))~;
 end;

theorem :: E_SIEC:42
   s_post(N) c= [:s_transitions(N),s_places(N):] &
         s_pre(N) c= [:s_transitions(N),s_places(N):];