The abstract of the Mizar article:

A Theory of Boolean Valued Functions and Partitions

by

Shunichi Kobayashi, and

Kui Jia

Received October 22, 1998

MML identifier: BVFUNC_1

[ Mizar article, MML identifier index ]

environ

 vocabulary MARGREL1, ZF_LANG, BINARITH, ORDINAL2, PARTIT1, FUNCT_2, FRAENKEL,
      VALUAT_1, RELAT_1, FUNCT_1, BOOLE, SEQM_3, EQREL_1, T_1TOPSP, SETFAM_1,
      TARSKI, BVFUNC_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL2, XREAL_0, MARGREL1,
      VALUAT_1, RELAT_1, FUNCT_1, FUNCT_2, SETFAM_1, FRAENKEL, BINARITH,
      EQREL_1, T_1TOPSP, PARTIT1, SEQM_3;
 constructors BINARITH, T_1TOPSP, PARTIT1, SEQM_3, PUA2MSS1, VALUAT_1, XREAL_0,
      MEMBERED;
 clusters SUBSET_1, MARGREL1, PARTIT1, XREAL_0, ARYTM_3, VALUAT_1, BINARITH,
      FRAENKEL;
 requirements NUMERALS, REAL, SUBSET, BOOLE;


begin :: Chap. 1  Boolean Operations

reserve Y for set;

definition let k,l be boolean set;
 func k 'imp' l equals
:: BVFUNC_1:def 1
  'not' k 'or' l;

 func k 'eqv' l equals
:: BVFUNC_1:def 2
  'not' (k 'xor' l);
 commutativity;
end;

definition let k,l be boolean set;
 cluster k 'imp' l -> boolean;
 cluster k 'eqv' l -> boolean;
end;

definition
 cluster boolean -> natural set;
end;

definition let k,l be boolean set;
 redefine
 pred k <= l means
:: BVFUNC_1:def 3
  k 'imp' l = TRUE;
 synonym k '<' l;
end;

begin :: Chap.2   Boolean Valued Functions

definition let Y;
  func BVF(Y) equals
:: BVFUNC_1:def 4
  Funcs(Y,BOOLEAN);
end;

definition let Y be set;
 cluster BVF(Y) -> functional non empty;
end;

definition let Y be set;
 cluster -> boolean-valued Element of BVF Y;
end;

reserve Y for non empty set;
reserve B for Subset of Y;

definition let a be boolean-valued Function, x be set;
 redefine
 func a.x;
 synonym Pj(a,x);
end;

definition let Y;let a be Element of BVF(Y);
 redefine
 func 'not' a ->Element of BVF(Y);
 let b be Element of BVF(Y);
 func a '&' b ->Element of BVF(Y);
end;

definition
 let p,q be boolean-valued Function;
  func p 'or' q -> Function means
:: BVFUNC_1:def 5
 dom it = dom p /\ dom q &
  for x being set st x in dom it holds it.x = (p.x) 'or' (q.x);
 commutativity;
  func p 'xor' q -> Function means
:: BVFUNC_1:def 6
 dom it = dom p /\ dom q &
  for x being set st x in dom it holds it.x = (p.x) 'xor' (q.x);
 commutativity;
end;

definition
 let p,q be boolean-valued Function;
  cluster p 'or' q -> boolean-valued;
  cluster p 'xor' q -> boolean-valued;
end;

definition let A be non empty set;
 redefine
 let p,q be Element of Funcs(A,BOOLEAN);
  func p 'or' q -> Element of Funcs(A,BOOLEAN) means
:: BVFUNC_1:def 7
 for x being Element of A holds it.x = (p.x) 'or' (q.x);
  func p 'xor' q -> Element of Funcs(A,BOOLEAN) means
:: BVFUNC_1:def 8
   for x being Element of A holds it.x = (p.x) 'xor' (q.x);
end;

definition let Y;let a,b be Element of BVF(Y);
 redefine
 func a 'or' b ->Element of BVF(Y);
 func a 'xor' b ->Element of BVF(Y);
end;

definition
 let p,q be boolean-valued Function;
  func p 'imp' q -> Function means
:: BVFUNC_1:def 9
 dom it = dom p /\ dom q &
  for x being set st x in dom it holds it.x = (p.x) 'imp' (q.x);
  func p 'eqv' q -> Function means
:: BVFUNC_1:def 10
 dom it = dom p /\ dom q &
  for x being set st x in dom it holds it.x = (p.x) 'eqv' (q.x);
 commutativity;
end;

definition
 let p,q be boolean-valued Function;
  cluster p 'imp' q -> boolean-valued;
  cluster p 'eqv' q -> boolean-valued;
end;

definition let A be non empty set;
 redefine
 let p,q be Element of Funcs(A,BOOLEAN);
  func p 'imp' q -> Element of Funcs(A,BOOLEAN) means
:: BVFUNC_1:def 11
 for x being Element of A holds it.x = ('not' Pj(p,x)) 'or' Pj(q,x);
  func p 'eqv' q -> Element of Funcs(A,BOOLEAN) means
:: BVFUNC_1:def 12
 for x being Element of A holds it.x = 'not' (Pj(p,x) 'xor' Pj(q,x));
end;

definition let Y;let a,b be Element of BVF(Y);
 redefine
 func a 'imp' b ->Element of BVF(Y);
 func a 'eqv' b ->Element of BVF(Y);
end;

definition let Y;
 func O_el(Y) ->Element of Funcs(Y,BOOLEAN) means
:: BVFUNC_1:def 13
 for x being Element of Y holds Pj(it,x)= FALSE;
end;

definition let Y;
 func I_el(Y) ->Element of Funcs(Y,BOOLEAN) means
:: BVFUNC_1:def 14
 for x being Element of Y holds Pj(it,x)= TRUE;
end;

canceled 3;

theorem :: BVFUNC_1:4
 for a being boolean-valued Function holds 'not' 'not' a=a;

theorem :: BVFUNC_1:5
 for a being Element of Funcs(Y,BOOLEAN) holds
 'not' I_el(Y)=O_el(Y) & 'not' O_el(Y)=I_el(Y);

theorem :: BVFUNC_1:6
for a,b being Element of Funcs(Y,BOOLEAN) holds
 a '&' a=a;

theorem :: BVFUNC_1:7
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
 a '&' b '&' c = a '&' (b '&' c);

theorem :: BVFUNC_1:8
for a being Element of Funcs(Y,BOOLEAN) holds
 a '&' O_el(Y)=O_el(Y);

theorem :: BVFUNC_1:9
for a being Element of Funcs(Y,BOOLEAN) holds
 a '&' I_el(Y)=a;

theorem :: BVFUNC_1:10
for a being Element of Funcs(Y,BOOLEAN) holds
 a 'or' a=a;

theorem :: BVFUNC_1:11
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
 a 'or' b 'or' c = a 'or' (b 'or' c);

theorem :: BVFUNC_1:12
for a being Element of Funcs(Y,BOOLEAN) holds
 a 'or' O_el(Y)=a;

theorem :: BVFUNC_1:13
for a being Element of Funcs(Y,BOOLEAN) holds
 a 'or' I_el(Y)=I_el(Y);

theorem :: BVFUNC_1:14  ::Distributive
   for a,b,c being Element of Funcs(Y,BOOLEAN) holds
 (a '&' b) 'or' c = (a 'or' c) '&' (b 'or' c);

theorem :: BVFUNC_1:15  ::Distributive
   for a,b,c being Element of Funcs(Y,BOOLEAN) holds
 (a 'or' b) '&' c = (a '&' c) 'or' (b '&' c);

theorem :: BVFUNC_1:16  ::De'Morgan
   for a,b being Element of Funcs(Y,BOOLEAN) holds
 'not' (a 'or' b)=('not' a) '&' ('not' b);

theorem :: BVFUNC_1:17  ::De'Morgan
   for a,b being Element of Funcs(Y,BOOLEAN) holds
  'not' (a '&' b)=('not' a) 'or' ('not' b);

definition let Y;let a,b be Element of Funcs(Y,BOOLEAN);
 pred a '<' b means
:: BVFUNC_1:def 15
 for x being Element of Y st Pj(a,x)= TRUE holds Pj(b,x)=TRUE;
reflexivity;
end;

theorem :: BVFUNC_1:18
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
((a '<' b) & (b '<' a) implies a=b)&
((a '<' b) & (b '<' c) implies a '<' c);

theorem :: BVFUNC_1:19
for a,b being Element of Funcs(Y,BOOLEAN) holds
 (a 'imp' b)=I_el(Y) iff a '<' b;

theorem :: BVFUNC_1:20
for a,b being Element of Funcs(Y,BOOLEAN) holds
(a 'eqv' b)=I_el(Y) iff a = b;

theorem :: BVFUNC_1:21
for a being Element of Funcs(Y,BOOLEAN) holds
 O_el(Y) '<' a & a '<' I_el(Y);

begin :: Chap. 3  Infimum and Supremum

definition let Y;let a be Element of Funcs(Y,BOOLEAN);
 func B_INF(a) ->Element of Funcs(Y,BOOLEAN) means
:: BVFUNC_1:def 16
  it = I_el(Y) if (for x being Element of Y holds Pj(a,x)=TRUE)
   otherwise it = O_el(Y);

 func B_SUP(a) ->Element of Funcs(Y,BOOLEAN) means
:: BVFUNC_1:def 17
  it = O_el(Y) if (for x being Element of Y holds Pj(a,x)=FALSE)
   otherwise it = I_el(Y);
end;

theorem :: BVFUNC_1:22
for a being Element of Funcs(Y,BOOLEAN) holds
     'not' B_INF(a) = B_SUP('not' a) & 'not' B_SUP(a)=B_INF('not' a);

theorem :: BVFUNC_1:23
       B_INF(O_el(Y)) = O_el(Y) & B_INF(I_el(Y))=I_el(Y) &
     B_SUP(O_el(Y)) = O_el(Y) & B_SUP(I_el(Y))=I_el(Y);

definition let Y;
 cluster O_el(Y) -> constant;
end;

definition let Y;
 cluster I_el(Y) -> constant;
end;

definition
 let Y be non empty set;
 cluster constant Element of Funcs(Y,BOOLEAN);
end;

theorem :: BVFUNC_1:24
for a being constant Element of Funcs(Y,BOOLEAN) holds
 a=O_el(Y) or a=I_el(Y);

theorem :: BVFUNC_1:25
for d being constant Element of Funcs(Y,BOOLEAN) holds
  B_INF(d) = d & B_SUP(d) = d;

theorem :: BVFUNC_1:26
for a,b being Element of Funcs(Y,BOOLEAN) holds
     B_INF(a '&' b) = B_INF(a) '&' B_INF(b) &
     B_SUP(a 'or' b) = B_SUP(a) 'or' B_SUP(b);

theorem :: BVFUNC_1:27
for a being Element of Funcs(Y,BOOLEAN),
                   d being constant Element of Funcs(Y,BOOLEAN) holds
     B_INF(d 'imp' a) = d 'imp' B_INF(a) &
     B_INF(a 'imp' d) = B_SUP(a) 'imp' d;

theorem :: BVFUNC_1:28
for a being Element of Funcs(Y,BOOLEAN),
                   d being constant Element of Funcs(Y,BOOLEAN) holds
     B_INF(d 'or' a) = d 'or' B_INF(a) &
     B_SUP(d '&' a) = d '&' B_SUP(a) &
     B_SUP(a '&' d) = B_SUP(a) '&' d;

theorem :: BVFUNC_1:29
for a being Element of Funcs(Y,BOOLEAN),x being Element of Y holds
     Pj(B_INF(a),x) '<' Pj(a,x);

theorem :: BVFUNC_1:30
for a being Element of Funcs(Y,BOOLEAN),x being Element of Y holds
     Pj(a,x) '<' Pj(B_SUP(a),x);

begin :: Chap. 4  Boolean Valued Functions and Partitions

definition let Y;let a be Element of Funcs(Y,BOOLEAN),PA be a_partition of Y;
pred a is_dependent_of PA means
:: BVFUNC_1:def 18
 for F being set st F in PA
  for x1,x2 being set st x1 in F & x2 in F holds a.x1=a.x2;
end;

theorem :: BVFUNC_1:31
for a being Element of Funcs(Y,BOOLEAN) holds
  a is_dependent_of %I(Y);

theorem :: BVFUNC_1:32
for a being constant Element of Funcs(Y,BOOLEAN) holds
  a is_dependent_of %O(Y);

definition let Y;let PA be a_partition of Y;
 redefine mode Element of PA -> Subset of Y;
end;

definition let Y;let x be Element of Y;let PA be a_partition of Y;
 redefine func EqClass(x,PA) -> Element of PA;
 synonym Lift(x,PA);
end;

definition let Y;let a be Element of Funcs(Y,BOOLEAN),PA be a_partition of Y;
 func B_INF(a,PA) -> Element of Funcs(Y,BOOLEAN) means
:: BVFUNC_1:def 19
  for y being Element of Y holds
   ( (for x being Element of Y st x in EqClass(y,PA) holds Pj(a,x)=TRUE)
         implies Pj(it,y) = TRUE ) &
   (not (for x being Element of Y st x in EqClass(y,PA) holds Pj(a,x)=TRUE)
         implies Pj(it,y) = FALSE);
end;

definition let Y;let a be Element of Funcs(Y,BOOLEAN),PA be a_partition of Y;
 func B_SUP(a,PA) -> Element of Funcs(Y,BOOLEAN) means
:: BVFUNC_1:def 20
  for y being Element of Y holds
   ( (ex x being Element of Y st x in EqClass(y,PA) & Pj(a,x)=TRUE)
         implies Pj(it,y) = TRUE ) &
   (not (ex x being Element of Y st x in EqClass(y,PA) & Pj(a,x)=TRUE)
         implies Pj(it,y) = FALSE);
end;

theorem :: BVFUNC_1:33
for a being Element of Funcs(Y,BOOLEAN),PA being a_partition of Y
holds
  B_INF(a,PA) is_dependent_of PA;

theorem :: BVFUNC_1:34
for a being Element of Funcs(Y,BOOLEAN),PA being a_partition of Y
holds
  B_SUP(a,PA) is_dependent_of PA;

theorem :: BVFUNC_1:35
for a being Element of Funcs(Y,BOOLEAN),PA being a_partition of Y
holds
   B_INF(a,PA) '<' a;

theorem :: BVFUNC_1:36
for a being Element of Funcs(Y,BOOLEAN),PA being a_partition of Y
holds
   a '<' B_SUP(a,PA);

theorem :: BVFUNC_1:37
for a being Element of Funcs(Y,BOOLEAN),PA being a_partition of Y
holds
   'not' B_INF(a,PA) = B_SUP('not' a,PA);

theorem :: BVFUNC_1:38
for a being Element of Funcs(Y,BOOLEAN) holds
  B_INF(a,%O(Y))=B_INF(a);

theorem :: BVFUNC_1:39
for a being Element of Funcs(Y,BOOLEAN) holds
  B_SUP(a,%O(Y))=B_SUP(a);

theorem :: BVFUNC_1:40
for a being Element of Funcs(Y,BOOLEAN) holds
  B_INF(a,%I(Y))=a;

theorem :: BVFUNC_1:41
for a being Element of Funcs(Y,BOOLEAN) holds
  B_SUP(a,%I(Y))=a;

theorem :: BVFUNC_1:42
for a,b being Element of Funcs(Y,BOOLEAN),PA being a_partition of Y
  holds B_INF(a '&' b,PA)=B_INF(a,PA) '&' B_INF(b,PA);

theorem :: BVFUNC_1:43
for a,b being Element of Funcs(Y,BOOLEAN),PA being a_partition of Y
 holds B_SUP(a 'or' b,PA)=B_SUP(a,PA) 'or' B_SUP(b,PA);

definition let Y;let f be Element of Funcs(Y,BOOLEAN);
 func GPart(f) -> a_partition of Y equals
:: BVFUNC_1:def 21
   {{x where x is Element of Y:f.x = TRUE },
    {x' where x' is Element of Y:f.x' = FALSE}} \ {{}};
end;

theorem :: BVFUNC_1:44
for a being Element of Funcs(Y,BOOLEAN) holds
  a is_dependent_of GPart(a);

theorem :: BVFUNC_1:45
for a being Element of Funcs(Y,BOOLEAN),PA being a_partition of Y
  st a is_dependent_of PA holds PA is_finer_than GPart(a);