The Mizar abstract of PNPROC

Journal of Formalized Mathematics
Volume 14, 2002
University of Bialystok
Copyright (c) 2002 Association of Mizar Users
The abstract of the Mizar article:: Processes in Petri nets
by
Grzegorz Bancerek,
Mitsuru Aoki,
Akio Matsumoto, and
Yasunari Shidama
Received December 20, 2002
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;
The abstract of the Mizar article:

Processes in Petri nets
