:: Cell Petri Net Concepts
::  by Mitsuru Jitsukawa, Pauline N. Kawamoto, Yasunari Shidama,
::   and Yatsuka Nakamura
::
:: Received October 14, 2008
:: Copyright (c) 2008-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 PETRI, FUNCT_1, XBOOLE_0, TARSKI, SUBSET_1, FUNCT_2, RELAT_1,
      FUNCOP_1, FUNCT_4, FINSET_1, SETFAM_1, ZFMISC_1, PARTFUN1, ARYTM_3,
      CARD_1, PETRI_2, STRUCT_0;
 notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ZFMISC_1, SETFAM_1, RELAT_1,
      RELSET_1, DOMAIN_1, PETRI, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, RELSET_2,
      FINSET_1, FUNCOP_1, ORDINAL1, CARD_1, PARTIT_2, STRUCT_0;
 constructors RELSET_1, DOMAIN_1, PETRI, RELSET_2, FUNCT_4, PARTIT_2, FUNCOP_1;
 registrations SUBSET_1, RELAT_1, PARTFUN1, RELSET_1, XBOOLE_0, FUNCT_2,
      FINSET_1, STRUCT_0, FUNCT_1, PETRI, ZFMISC_1;
 requirements SUBSET, BOOLE;


begin :: Preliminaries: thin cylinder, locus

definition
  let A be non empty set, B be set;
  let Bo be set, yo be Function of Bo,A;
  assume
 Bo c= B;
  func cylinder0(A,B,Bo,yo) -> non empty Subset of Funcs(B,A) equals
:: PETRI_2:def 1

  { y where y is Function of B,A : y|Bo = yo };
end;

definition
  let A be non empty set, B be set;
  mode thin_cylinder of A,B -> non empty Subset of Funcs(B,A) means
:: PETRI_2:def 2

    ex
Bo being Subset of B,yo being Function of Bo,A st Bo is finite & it = cylinder0
    (A,B,Bo,yo);
end;

theorem :: PETRI_2:1
  for A be non empty set, B be set, D be thin_cylinder of A,B holds
  ex Bo being Subset of B,yo being Function of Bo,A st Bo is finite & D = { y
  where y is Function of B,A : y|Bo = yo };

theorem :: PETRI_2:2
  for A1,A2 be non empty set, B be set, D1 be thin_cylinder of A1,B st
  A1 c= A2 ex D2 be thin_cylinder of A2,B st D1 c= D2;

definition
  let A be non empty set, B be set;
  func thin_cylinders(A,B) -> non empty Subset-Family of Funcs(B,A) equals
:: PETRI_2:def 3
  {D
  where D is Subset of Funcs(B,A) : D is thin_cylinder of A,B};
end;

theorem :: PETRI_2:3
  for A be non trivial set, B be set, Bo1 be set, yo1 being
Function of Bo1,A, Bo2 be set, yo2 being Function of Bo2,A st Bo1 c= B & Bo2 c=
  B & cylinder0(A,B,Bo1,yo1) = cylinder0(A,B,Bo2,yo2) holds Bo1=Bo2 & yo1=yo2;

theorem :: PETRI_2:4
  for A1,A2 be non empty set, B1,B2 be set st A1 c= A2 & B1 c= B2
  ex F be Function of thin_cylinders(A1,B1), thin_cylinders(A2,B2) st for x be
set st x in thin_cylinders(A1,B1) ex Bo being Subset of B1, yo1 being Function
of Bo,A1, yo2 being Function of Bo,A2 st Bo is finite & yo1=yo2 & x=cylinder0(
  A1,B1,Bo,yo1) & F.x=cylinder0(A2,B2,Bo,yo2);

theorem :: PETRI_2:5
  for A1,A2 be non empty set, B1,B2 be set ex G be Function of
  thin_cylinders(A2,B2), thin_cylinders(A1,B1) st for x be set st x in
  thin_cylinders(A2,B2) ex Bo2 being Subset of B2,Bo1 being Subset of B1, yo1
  being Function of Bo1,A1, yo2 being Function of Bo2,A2 st Bo1 is finite & Bo2
is finite & Bo1=B1 /\ Bo2 /\ (yo2"A1) & yo1=yo2 | Bo1 & x= cylinder0(A2,B2,Bo2,
  yo2) & G.x =cylinder0(A1,B1,Bo1,yo1);

definition
  let A1,A2 be non trivial set, B1,B2 be set;
  assume that
 A1 c= A2 and
 B1 c= B2;
  func Extcylinders(A1,B1,A2,B2) -> Function of thin_cylinders(A1,B1),
  thin_cylinders(A2,B2) means
:: PETRI_2:def 4
  for x be set st x in thin_cylinders(A1,B1) ex Bo
being Subset of B1, yo1 being Function of Bo,A1, yo2 being Function of Bo,A2 st
  Bo is finite & yo1=yo2 & x=cylinder0(A1,B1,Bo,yo1) & it.x=cylinder0(A2,B2,Bo,
  yo2);
end;

definition
  let A1 be non empty set, A2 be non trivial set, B1,B2 be set;
  func Ristcylinders(A1,B1,A2,B2) -> Function of thin_cylinders(A2,B2),
  thin_cylinders(A1,B1) means
:: PETRI_2:def 5
  for x be set st x in thin_cylinders(A2,B2) ex Bo2
  being Subset of B2,Bo1 being Subset of B1, yo1 being Function of Bo1,A1, yo2
being Function of Bo2,A2 st Bo1 is finite & Bo2 is finite & Bo1=B1 /\ Bo2 /\ (
yo2"A1) & yo1=yo2 | Bo1 & x = cylinder0(A2,B2,Bo2,yo2) & it.x =cylinder0(A1,B1,
  Bo1,yo1);
end;

definition
  let A be non trivial set,B be set;
  let D be thin_cylinder of A,B;
  func loc(D) -> finite Subset of B means
:: PETRI_2:def 6
  ex Bo being Subset of B,yo being
Function of Bo,A st Bo is finite & D = { y where y is Function of B,A : y|Bo =
  yo } & it = Bo;
end;

begin :: Colored Petri nets

definition
  let A1,A2 be non trivial set, B1,B2 be set;
  let C1,C2 be non trivial set, D1,D2 be set;
  let F be Function of thin_cylinders(A1,B1), thin_cylinders(C1,D1);
  func CylinderFunc(A1,B1,A2,B2,C1,D1,C2,D2,F) -> Function of thin_cylinders(
  A2,B2), thin_cylinders(C2,D2) equals
:: PETRI_2:def 7
  Extcylinders(C1,D1,C2,D2)*F*Ristcylinders(
  A1,B1,A2,B2);
end;

definition
  struct (PT_net_Str) Colored_PT_net_Str (# carrier, carrier' ->
set, S-T_Arcs ->  Relation of the carrier,the carrier', T-S_Arcs ->
     Relation of the carrier', the carrier, ColoredSet -> non empty
    finite set, firing-rule -> Function #);
end;

definition
 func TrivialColoredPetriNet -> Colored_PT_net_Str equals
:: PETRI_2:def 8
  Colored_PT_net_Str (# {{}}, {{}}, [#]({{}},{{}}), [#]({{}},
       {{}}), {{}}, {} #);
end;

registration
 cluster TrivialColoredPetriNet
  -> with_S-T_arc with_T-S_arc non empty non void;
end;

registration
 cluster non empty non void with_S-T_arc with_T-S_arc for Colored_PT_net_Str;
end;

definition
 mode Colored_Petri_net
  is non empty non void with_S-T_arc with_T-S_arc Colored_PT_net_Str;
end;

definition
  let CPNT be Colored_Petri_net;
  let t0 be transition of CPNT;
  attr t0 is outbound means
:: PETRI_2:def 9

  {t0}*' = {};
end;

definition
  let CPNT1 be Colored_Petri_net;
  func Outbds(CPNT1) -> Subset of the carrier' of CPNT1 equals
:: PETRI_2:def 10
  {x where x
  is transition of CPNT1 : x is outbound };
end;

definition
  let CPNT be Colored_Petri_net;
  attr CPNT is Colored-PT-net-like means
:: PETRI_2:def 11

  dom (the firing-rule of CPNT)
c= (the carrier' of CPNT) \ Outbds(CPNT) & for t being transition of CPNT st
  t in dom (the firing-rule of CPNT) holds ex CS be non empty Subset of the
  ColoredSet of CPNT, I be Subset of *'{t}, O be Subset of {t}*' st (the
firing-rule of CPNT ).t is Function of thin_cylinders(CS,I), thin_cylinders(CS,
  O);
end;

theorem :: PETRI_2:6
  for CPNT be Colored_Petri_net, t being transition of CPNT st CPNT is
  Colored-PT-net-like & t in dom (the firing-rule of CPNT) holds ex CS be non
empty Subset of the ColoredSet of CPNT, I be Subset of *'{t}, O be Subset of {t
  }*' st (the firing-rule of CPNT ).t is Function of thin_cylinders(CS,I),
  thin_cylinders(CS,O);

theorem :: PETRI_2:7
  for CPNT1,CPNT2 be Colored_Petri_net, t1 be transition of CPNT1,
  t2 be transition of CPNT2 st the carrier of CPNT1 c= the carrier of CPNT2
   & the
  S-T_Arcs of CPNT1 c= the S-T_Arcs of CPNT2 & the T-S_Arcs of CPNT1 c= the
  T-S_Arcs of CPNT2 & t1=t2 holds *'{t1} c= *'{t2} & {t1}*' c= {t2}*';

registration
  cluster strict Colored-PT-net-like for Colored_Petri_net;
end;

definition
  mode Colored-PT-net is Colored-PT-net-like Colored_Petri_net;
end;

begin :: Outbound transitions of CPNT

definition
  let CPNT1, CPNT2 be Colored_Petri_net;
  pred CPNT1 misses CPNT2 means
:: PETRI_2:def 12

  (the carrier of CPNT1) /\ (the carrier
of CPNT2 ) = {} & (the carrier' of CPNT1) /\ (the carrier' of CPNT2) = {};
  symmetry;
end;

begin :: Connecting mapping for CPNT1,CPNT2

definition
  let CPNT1 be Colored_Petri_net;
  let CPNT2 be Colored_Petri_net;
  mode connecting-mapping of CPNT1,CPNT2 -> set means
:: PETRI_2:def 13

    ex O12 be Function of
    Outbds(CPNT1), the carrier of CPNT2, O21 be Function of Outbds(CPNT2), the
    carrier of CPNT1 st it=[O12,O21];
end;

begin :: Connecting firing rule for CPNT1,CPNT2

definition
  let CPNT1, CPNT2 be Colored-PT-net;
  let O be connecting-mapping of CPNT1,CPNT2;
  mode connecting-firing-rule of CPNT1,CPNT2,O -> set means
:: PETRI_2:def 14

    ex q12,q21 be
    Function, O12 be Function of Outbds(CPNT1), the carrier of CPNT2, O21 be
Function of Outbds(CPNT2), the carrier of CPNT1 st O=[O12,O21] &
 dom q12=Outbds(
    CPNT1) & dom q21=Outbds(CPNT2) & ( for t01 be transition of CPNT1 st t01 is
outbound holds q12.t01 is Function of thin_cylinders ( the ColoredSet of CPNT1,
*'{t01}), thin_cylinders ( the ColoredSet of CPNT1, Im(O12,t01) ) ) & ( for t02
    be transition of CPNT2 st t02 is outbound holds q21.t02 is Function of
    thin_cylinders (the ColoredSet of CPNT2, *'{t02}), thin_cylinders (the
    ColoredSet of CPNT2, Im(O21,t02) ) ) & it=[q12,q21];
end;

begin :: Synthesis of CPNT1,CPNT2

definition
  let CPNT1, CPNT2 be Colored-PT-net;
  let O be connecting-mapping of CPNT1,CPNT2;
  let q be connecting-firing-rule of CPNT1,CPNT2,O;
  assume
 CPNT1 misses CPNT2;
  func synthesis(CPNT1, CPNT2,O,q) -> strict Colored-PT-net means
:: PETRI_2:def 15
  ex q12,q21
  be Function, O12 be Function of Outbds(CPNT1), the carrier of CPNT2, O21 be
Function of Outbds(CPNT2), the carrier of CPNT1 st O=[O12,O21] &
 dom q12=Outbds(
  CPNT1) & dom q21=Outbds(CPNT2) & ( for t01 be transition of CPNT1 st t01 is
outbound holds q12.t01 is Function of thin_cylinders ( the ColoredSet of CPNT1,
*'{t01}), thin_cylinders ( the ColoredSet of CPNT1, Im(O12,t01) ) ) & ( for t02
  be transition of CPNT2 st t02 is outbound holds q21.t02 is Function of
  thin_cylinders ( the ColoredSet of CPNT2, *'{t02}), thin_cylinders ( the
  ColoredSet of CPNT2, Im(O21,t02) ) ) & q=[q12,q21] & the carrier of it = (the
  carrier of CPNT1) \/ (the carrier of CPNT2) & the carrier' of it = (the
carrier' of CPNT1) \/ (the carrier' of CPNT2) & the S-T_Arcs of it = (the
  S-T_Arcs of CPNT1) \/ (the S-T_Arcs of CPNT2) & the T-S_Arcs of it = (the
T-S_Arcs of CPNT1) \/ (the T-S_Arcs of CPNT2) \/ O12 \/ O21 & the ColoredSet of
  it = (the ColoredSet of CPNT1) \/ (the ColoredSet of CPNT2) & the firing-rule
of it = (the firing-rule of CPNT1) +* (the firing-rule of CPNT2) +* q12 +* q21;
end;