The Mizar abstract of QUANTAL1

Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994 Association of Mizar Users
The abstract of the Mizar article:: Quantales
by
Grzegorz Bancerek
Received May 9, 1994
MML identifier: QUANTAL1
[ Mizar article, MML identifier index ]
environ

 vocabulary TARSKI, BOOLE, LATTICES, VECTSP_1, FUNCT_1, LATTICE3, BINOP_1,
      PRE_TOPC, FINSET_1, FREEALG, MONOID_0, ALGSTR_2, GROUP_1, BHSP_3,
      SETWISEO, VECTSP_2, SEQM_3, GRAPH_1, FUNCT_3, RELAT_1, QUANTAL1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, VECTSP_1, RELAT_1, FUNCT_1,
      BINOP_1, SETWISEO, STRUCT_0, FINSET_1, DOMAIN_1, LATTICES, LATTICE3,
      MONOID_0, PRE_TOPC, PARTFUN1, FUNCT_2;
 constructors BINOP_1, SETWISEO, DOMAIN_1, LATTICE3, MONOID_0, PRE_TOPC,
      MEMBERED, PARTFUN1, RELAT_2, XBOOLE_0;
 clusters LATTICE3, MONOID_0, FINSET_1, STRUCT_0, GROUP_1, RELSET_1, SUBSET_1,
      LATTICES, MEMBERED, ZFMISC_1, PARTFUN1, FUNCT_2, XBOOLE_0;
 requirements BOOLE, SUBSET;


begin

definition let X be set;
 let Y be Subset of bool X;
 redefine func union Y -> Subset of X;
end;

scheme DenestFraenkel
 {A()->non empty set, B()->non empty set, F(set)->set,
  G(set)->Element of B(), P[set]}:
  {F(a) where a is Element of B(): a in {G(b) where b is Element of A(): P[b]}}
    = {F(G(a)) where a is Element of A(): P[a]};

scheme EmptyFraenkel {A() -> non empty set, f(set) -> set, P[set]}:
 {f(a) where a is Element of A(): P[a]} = {}
  provided
 not ex a being Element of A() st P[a];

theorem :: QUANTAL1:1
 for L1,L2 being non empty LattStr st the LattStr of L1 = the LattStr of L2
  for a1,b1 being Element of L1,
      a2,b2 being Element of L2, X being set st
   a1 = a2 & b1 = b2 holds
    a1"\/"b1 = a2"\/"b2 & a1"/\"b1 = a2"/\"b2 & (a1 [= b1 iff a2 [= b2);

theorem :: QUANTAL1:2
 for L1,L2 being non empty LattStr st the LattStr of L1 = the LattStr of L2
  for a being Element of L1,
      b being Element of L2, X being set st a = b
   holds (a is_less_than X iff b is_less_than X) &
    (a is_great_than X iff b is_great_than X);

definition let L be 1-sorted;
 mode UnOp of L is map of L,L;
end;

definition let L be non empty LattStr, X be Subset of L;
 attr X is directed means
:: QUANTAL1:def 1
    for Y being finite Subset of X ex x being Element of L st
   "\/"(Y, L) [= x & x in X;
end;

theorem :: QUANTAL1:3
   for L being non empty LattStr, X being Subset of L st X is directed holds
   X is non empty;

definition
  struct (LattStr, HGrStr) QuantaleStr
   (# carrier -> set,
     L_join, L_meet, mult -> BinOp of the carrier #);
end;

definition
 cluster non empty QuantaleStr;
end;

definition
  struct (QuantaleStr, multLoopStr) QuasiNetStr
   (# carrier -> set,
     L_join, L_meet, mult -> (BinOp of the carrier),
     unity -> Element of the carrier #);
end;

definition
 cluster non empty QuasiNetStr;
end;

definition let IT be non empty HGrStr;
 attr IT is with_left-zero means
:: QUANTAL1:def 2
    ex a being Element of IT st
   for b being Element of IT holds a*b = a;
 attr IT is with_right-zero means
:: QUANTAL1:def 3
    ex b being Element of IT st
   for a being Element of IT holds a*b = b;
end;

definition let IT be non empty HGrStr;
 attr IT is with_zero means
:: QUANTAL1:def 4

  IT is with_left-zero with_right-zero;
end;

definition
 cluster with_zero -> with_left-zero with_right-zero (non empty HGrStr);
 cluster with_left-zero with_right-zero -> with_zero (non empty HGrStr);
end;

definition
 cluster with_zero (non empty HGrStr);
end;

definition let IT be non empty QuantaleStr;
 attr IT is right-distributive means
:: QUANTAL1:def 5

  for a being Element of IT, X being set holds
   a [*] "\/"(X,IT) =
    "\/"({a [*] b where b is Element of IT: b in X},IT);
 attr IT is left-distributive means
:: QUANTAL1:def 6

  for a being Element of IT, X being set holds
   "\/"(X,IT) [*] a =
     "\/"({b [*] a where b is Element of IT: b in X},IT);
 attr IT is times-additive means
:: QUANTAL1:def 7
    for a,b,c being Element of IT holds
     (a"\/"b)[*]c = (a[*]c)"\/"(b[*]c) & c[*](a"\/"b) = (c[*]a)"\/"(c[*]b);
 attr IT is times-continuous means
:: QUANTAL1:def 8
    for X1, X2 being Subset of IT st X1 is directed & X2 is directed holds
   ("\/"X1)[*]("\/"X2) = "\/"({a [*] b where
      a is Element of IT, b is Element of IT:
     a in X1 & b in X2},IT);
end;

reserve x,y,z for set;

theorem :: QUANTAL1:4
 for Q being non empty QuantaleStr st the LattStr of Q = BooleLatt {}
  holds Q is associative commutative unital with_zero
   complete right-distributive left-distributive Lattice-like;

definition let A be non empty set, b1,b2,b3 be BinOp of A;
 cluster QuantaleStr(#A,b1,b2,b3#) -> non empty;
end;

definition
 cluster associative commutative unital with_zero
  left-distributive right-distributive complete Lattice-like
     (non empty QuantaleStr);
end;

scheme LUBFraenkelDistr
    {Q() -> complete Lattice-like (non empty QuantaleStr),
     f(set, set) -> Element of Q(),
     X, Y() -> set}:
  "\/"({"\/"({f(a,b) where b is Element of Q(): b in Y()},Q())
                 where a is Element of Q(): a in X()}, Q()) =
  "\/"({f(a,b) where a is Element of Q(),
                   b is Element of Q(): a in X() & b in
 Y()}, Q());

reserve
 Q for left-distributive right-distributive complete Lattice-like
     (non empty QuantaleStr),
 a, b, c, d for Element of Q;

theorem :: QUANTAL1:5
 for Q for X,Y being set holds "\/"(X,Q) [*] "\/"(Y,Q) = "\/"({a[*]
b: a in X & b in Y}, Q);

theorem :: QUANTAL1:6
 (a"\/"b) [*] c = (a [*] c) "\/" (b [*] c) & c [*] (a"\/"b) = (c [*] a) "\/"
 (c [*] b);

definition let A be non empty set, b1,b2,b3 be (BinOp of A),
  e be Element of A;
 cluster QuasiNetStr(#A,b1,b2,b3,e#) -> non empty;
end;

definition
 cluster complete Lattice-like (non empty QuasiNetStr);
end;

definition
 cluster left-distributive right-distributive -> times-continuous
  times-additive (complete Lattice-like (non empty QuasiNetStr));
end;

definition
 cluster associative commutative well-unital with_zero with_left-zero
  left-distributive right-distributive complete Lattice-like
   (non empty QuasiNetStr);
end;

definition
 mode Quantale is associative left-distributive right-distributive
      complete Lattice-like (non empty QuantaleStr);

 mode QuasiNet is well-unital associative with_left-zero times-continuous
   times-additive complete Lattice-like (non empty QuasiNetStr);
end;

definition
 mode BlikleNet is with_zero (non empty QuasiNet);
end;

theorem :: QUANTAL1:7
   for Q being well-unital (non empty QuasiNetStr) st Q is Quantale
   holds Q is BlikleNet;

reserve Q for Quantale, a,a',b,b',c,d,d1,d2,D for Element of Q;

theorem :: QUANTAL1:8
 a [= b implies a [*] c [= b [*] c & c [*] a [= c [*] b;

theorem :: QUANTAL1:9
 a [= b & c [= d implies a [*] c [= b [*] d;

definition let f be Function;
 attr f is idempotent means
:: QUANTAL1:def 9
    f * f = f;
end;

definition let L be non empty LattStr;
  let IT be UnOp of L;
 attr IT is inflationary means
:: QUANTAL1:def 10
    for p being Element of L holds p [= IT.p;

 attr IT is deflationary means
:: QUANTAL1:def 11
    for p being Element of L holds IT.p [= p;

 attr IT is monotone means
:: QUANTAL1:def 12

  for p,q being Element of L st p [= q holds IT.p [= IT.q;

 attr IT is \/-distributive means
:: QUANTAL1:def 13
    for X being Subset of L holds
   IT."\/"X [= "\/"({IT.a where a is Element of L: a in X}, L);
end;

definition
 let L be Lattice;
 cluster inflationary deflationary monotone UnOp of L;
end;

theorem :: QUANTAL1:10
 for L being complete Lattice, j being UnOp of L st j is monotone holds
  j is \/-distributive iff for X being Subset of L holds
    j."\/"X = "\/"({j.a where a is Element of L: a in X}, L);

definition let Q be non empty QuantaleStr;
   let IT be UnOp of Q;
  attr IT is times-monotone means
:: QUANTAL1:def 14
     for a,b being Element of Q holds IT.a [*] IT.b [= IT.(a [*]
 b);
end;

definition let Q be non empty QuantaleStr, a,b be Element of Q;
  func a -r> b -> Element of Q equals
:: QUANTAL1:def 15

    "\/"({ c where c is Element of Q: c [*] a [= b }, Q);

  func a -l> b -> Element of Q equals
:: QUANTAL1:def 16

    "\/"({ c where c is Element of Q: a [*] c [= b }, Q);
end;

theorem :: QUANTAL1:11
 a [*] b [= c iff b [= a -l> c;

theorem :: QUANTAL1:12
 a [*] b [= c iff a [= b -r> c;

theorem :: QUANTAL1:13
 for Q being Quantale, s,a,b being Element of Q st
   a [= b holds b-r>s [= a-r>s & b-l>s [= a-l>s;

theorem :: QUANTAL1:14
   for Q being Quantale, s being Element of Q,
     j being UnOp of Q
   st for a being Element of Q holds j.a = (a-r>s)-r>s
  holds j is monotone;

definition let Q be non empty QuantaleStr;
   let IT be Element of Q;
  attr IT is dualizing means
:: QUANTAL1:def 17

   for a being Element of Q
    holds (a-r>IT)-l>IT = a & (a-l>IT)-r>IT = a;

  attr IT is cyclic means
:: QUANTAL1:def 18

   for a being Element of Q holds a -r> IT = a -l> IT;
end;

theorem :: QUANTAL1:15
 c is cyclic iff for a,b st a [*] b [= c holds b [*] a [= c;

theorem :: QUANTAL1:16
 for Q being Quantale, s,a being Element of Q
   st s is cyclic holds
   a [= (a-r>s)-r>s & a [= (a-l>s)-l>s;

theorem :: QUANTAL1:17
   for Q being Quantale, s,a being Element of Q
   st s is cyclic holds
   a-r>s = ((a-r>s)-r>s)-r>s & a-l>s = ((a-l>s)-l>s)-l>s;

theorem :: QUANTAL1:18
   for Q being Quantale, s,a,b being Element of Q
   st s is cyclic holds
   ((a-r>s)-r>s)[*]((b-r>s)-r>s) [= ((a[*]b)-r>s)-r>s;

theorem :: QUANTAL1:19
 D is dualizing implies Q is unital &
  the_unity_wrt the mult of Q = D -r> D &
   the_unity_wrt the mult of Q = D -l> D;

theorem :: QUANTAL1:20
   a is dualizing implies
  b -r> c = (b [*] (c -l> a)) -r> a & b -l> c = ((c -r> a) [*] b) -l> a;

definition
  struct (QuasiNetStr) Girard-QuantaleStr
  (# carrier -> set,
    L_join, L_meet, mult -> (BinOp of the carrier),
    unity, absurd -> Element of the carrier #);
end;

definition
 cluster non empty Girard-QuantaleStr;
end;

definition let IT be non empty Girard-QuantaleStr;
 attr IT is cyclic means
:: QUANTAL1:def 19
   the absurd of IT is cyclic;
 attr IT is dualized means
:: QUANTAL1:def 20
   the absurd of IT is dualizing;
end;

theorem :: QUANTAL1:21
 for Q being non empty Girard-QuantaleStr st the LattStr of Q = BooleLatt {}
  holds Q is cyclic dualized;

definition let A be non empty set, b1,b2,b3 be (BinOp of A),
               e1,e2 be Element of A;
 cluster Girard-QuantaleStr(#A,b1,b2,b3,e1,e2#) -> non empty;
end;

definition
  cluster associative commutative well-unital
   left-distributive right-distributive complete Lattice-like
   cyclic dualized strict (non empty Girard-QuantaleStr);
end;

definition
  mode Girard-Quantale is associative well-unital
   left-distributive right-distributive
   complete Lattice-like cyclic dualized (non empty Girard-QuantaleStr);
end;

definition let G be Girard-QuantaleStr;
  func Bottom G -> Element of G equals
:: QUANTAL1:def 21
  the absurd of G;
end;

definition let G be non empty Girard-QuantaleStr;
  func Top G -> Element of G equals
:: QUANTAL1:def 22
   (Bottom G) -r> Bottom G;
  let a be Element of G;
  func Bottom a -> Element of G equals
:: QUANTAL1:def 23
   a -r> Bottom G;
end;

definition let G be non empty Girard-QuantaleStr;
 func Negation G -> UnOp of G means
:: QUANTAL1:def 24
     for a being Element of G holds it.a = Bottom a;
end;

definition let G be non empty Girard-QuantaleStr, u be UnOp of G;
  func Bottom u -> UnOp of G equals
:: QUANTAL1:def 25
     Negation(G)*u;
end;

definition let G be non empty Girard-QuantaleStr, o be BinOp of G;
  func Bottom o -> BinOp of G equals
:: QUANTAL1:def 26
      Negation(G)*o;
end;

reserve Q for Girard-Quantale,
        a,a1,a2,b,b1,b2,c,d for Element of Q,
 X for set;

theorem :: QUANTAL1:22
 Bottom Bottom a = a;

theorem :: QUANTAL1:23
 a [= b implies Bottom b [= Bottom a;

theorem :: QUANTAL1:24
 Bottom "\/"(X,Q) = "/\"({Bottom a: a in X}, Q);

theorem :: QUANTAL1:25
 Bottom "/\"(X,Q) = "\/"({Bottom a: a in X}, Q);

theorem :: QUANTAL1:26
 Bottom (a"\/"b) = Bottom a"/\"Bottom b & Bottom (a"/\"b) = Bottom a"\/"Bottom
b;

definition let Q,a,b;
 func a delta b -> Element of Q equals
:: QUANTAL1:def 27
   Bottom (Bottom a [*] Bottom b);
end;

theorem :: QUANTAL1:27
   a [*] "\/"(X,Q) = "\/"({a [*] b: b in X}, Q) & a delta "/\"(X,Q) =
   "/\"({a delta c: c in X}, Q);

theorem :: QUANTAL1:28
   "\/"(X,Q) [*] a = "\/"({b [*] a: b in X}, Q) & "/\"(X,Q) delta a =
   "/\"({c delta a: c in X}, Q);


theorem :: QUANTAL1:29
   a delta (b"/\"c) = (a delta b)"/\"(a delta c) &
  (b"/\"c) delta a = (b delta a)"/\"(c delta a);

theorem :: QUANTAL1:30
   a1 [= b1 & a2 [= b2 implies a1 delta a2 [= b1 delta b2;

theorem :: QUANTAL1:31
   a delta b delta c = a delta (b delta c);

theorem :: QUANTAL1:32
 a [*] Top Q = a & Top Q [*] a = a;

theorem :: QUANTAL1:33
   a delta Bottom Q = a & (Bottom Q) delta a = a;

theorem :: QUANTAL1:34
   for Q being Quantale for j being UnOp of Q st
    j is monotone idempotent \/-distributive
  ex L being complete Lattice st the carrier of L = rng j &
   for X being Subset of L holds "\/"X = j."\/"(X,Q);
The abstract of the Mizar article:

Quantales
