The abstract of the Mizar article:

Some Elementary Notions of the Theory of Petri Nets

by

Waldemar Korczynski

Received August 10, 1990

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