:: A Theory of Boolean Valued Functions and Partitions :: by Shunichi Kobayashi and Kui Jia :: :: Received October 22, 1998 :: Copyright (c) 1998-2018 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 NUMBERS, XBOOLEAN, XXREAL_0, CARD_1, XBOOLE_0, SUBSET_1, MARGREL1, FUNCT_1, RELAT_1, TARSKI, FUNCOP_1, PARTIT1, EQREL_1, ZFMISC_1, SETFAM_1, BVFUNC_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XBOOLEAN, MARGREL1, RELAT_1, FUNCT_1, FUNCT_2, SETFAM_1, EQREL_1, ORDINAL1, NUMBERS, PARTIT1, XXREAL_0, FUNCOP_1; constructors SETFAM_1, XXREAL_0, XREAL_0, PARTIT1, BINARITH, FUNCOP_1, RELSET_1, NUMBERS; registrations SUBSET_1, XREAL_0, XBOOLEAN, EQREL_1, MARGREL1, FUNCT_2, RELSET_1, FUNCOP_1; requirements REAL, SUBSET, BOOLE, ARITHM, NUMERALS; begin :: Chap. 1 Boolean Operations definition let k,l be boolean object; redefine pred k <= l means :: BVFUNC_1:def 1 k => l = TRUE; end; begin :: Chap.2 Boolean Valued Functions reserve Y for non empty set; reserve B for Subset of Y; scheme :: BVFUNC_1:sch 1 BVFUniq1 {Y() -> non empty set, F(set) -> set}: for f1,f2 being Function of Y(),BOOLEAN st (for x being Element of Y() holds f1.x = F(x)) & (for x being Element of Y() holds f2.x = F(x)) holds f1 = f2; definition let Y; let a be Function of Y,BOOLEAN; redefine func 'not' a -> Function of Y,BOOLEAN; let b be Function of Y,BOOLEAN; redefine func a '&' b -> Function of Y,BOOLEAN; end; definition let p,q be boolean-valued Function; func p 'or' q -> boolean-valued Function means :: BVFUNC_1:def 2 dom it = dom p /\ dom q & for x being object st x in dom it holds it.x = (p.x) 'or' (q.x); commutativity; idempotence; func p 'xor' q -> Function means :: BVFUNC_1:def 3 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; registration let p,q be boolean-valued Function; cluster p 'xor' q -> boolean-valued; end; definition let A be non empty set; let p,q be Function of A,BOOLEAN; redefine func p 'or' q -> Function of A,BOOLEAN means :: BVFUNC_1:def 4 for x being Element of A holds it.x = (p.x) 'or' (q.x); redefine func p 'xor' q -> Function of A,BOOLEAN means :: BVFUNC_1:def 5 for x being Element of A holds it.x = (p.x) 'xor' (q.x); end; definition let p,q be boolean-valued Function; func p 'imp' 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) => (q.x); func p 'eqv' q -> Function means :: BVFUNC_1:def 7 dom it = dom p /\ dom q & for x being set st x in dom it holds it.x = (p.x) <=> (q.x); commutativity; end; registration 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; let p,q be Function of A,BOOLEAN; redefine func p 'imp' q -> Function of A,BOOLEAN means :: BVFUNC_1:def 8 for x being Element of A holds it.x = 'not' p.x 'or' q.x; redefine func p 'eqv' q -> Function of A,BOOLEAN means :: BVFUNC_1:def 9 for x being Element of A holds it.x = 'not' (p.x 'xor' q.x); end; definition let Y; func O_el(Y) ->Function of Y,BOOLEAN means :: BVFUNC_1:def 10 for x being Element of Y holds it.x= FALSE; end; definition let Y; func I_el(Y) ->Function of Y,BOOLEAN means :: BVFUNC_1:def 11 for x being Element of Y holds it.x= TRUE; end; ::\$CT theorem :: BVFUNC_1:2 'not' I_el(Y)=O_el(Y) & 'not' O_el(Y)=I_el(Y); theorem :: BVFUNC_1:3 for a,b being Function of Y,BOOLEAN holds a '&' a=a; theorem :: BVFUNC_1:4 for a,b,c being Function of Y,BOOLEAN holds a '&' b '&' c = a '&' (b '&' c); theorem :: BVFUNC_1:5 for a being Function of Y,BOOLEAN holds a '&' O_el(Y)=O_el( Y); theorem :: BVFUNC_1:6 for a being Function of Y,BOOLEAN holds a '&' I_el(Y)=a; theorem :: BVFUNC_1:7 for a being Function of Y,BOOLEAN holds a 'or' a=a; theorem :: BVFUNC_1:8 for a,b,c being Function of Y,BOOLEAN holds a 'or' b 'or' c = a 'or' (b 'or' c); theorem :: BVFUNC_1:9 for a being Function of Y,BOOLEAN holds a 'or' O_el(Y)=a; theorem :: BVFUNC_1:10 for a being Function of Y,BOOLEAN holds a 'or' I_el(Y)= I_el(Y); theorem :: BVFUNC_1:11 ::Distributive for a,b,c being Function of Y,BOOLEAN holds (a '&' b) 'or' c = (a 'or' c) '&' (b 'or' c); theorem :: BVFUNC_1:12 ::Distributive for a,b,c being Function of Y,BOOLEAN holds (a 'or' b) '&' c = (a '&' c) 'or' (b '&' c); theorem :: BVFUNC_1:13 ::De'Morgan for a,b being Function of Y,BOOLEAN holds 'not' (a 'or' b)=('not' a) '&' ('not' b); theorem :: BVFUNC_1:14 ::De'Morgan for a,b being Function of Y,BOOLEAN holds 'not' (a '&' b)=('not' a) 'or' ('not' b); definition let Y; let a,b be Function of Y,BOOLEAN; pred a '<' b means :: BVFUNC_1:def 12 for x being Element of Y st a.x= TRUE holds b.x= TRUE; reflexivity; end; theorem :: BVFUNC_1:15 for a,b,c being Function of Y,BOOLEAN holds ( a '<' b & b '<' a implies a=b)& ( a '<' b & b '<' c implies a '<' c); theorem :: BVFUNC_1:16 for a,b being Function of Y,BOOLEAN holds (a 'imp' b)=I_el (Y) iff a '<' b; theorem :: BVFUNC_1:17 for a,b being Function of Y,BOOLEAN holds (a 'eqv' b)=I_el(Y) iff a = b; theorem :: BVFUNC_1:18 for a being Function of Y,BOOLEAN holds O_el(Y) '<' a & a '<' I_el(Y); begin :: Chap. 3 Infimum and Supremum definition let Y; let a be Function of Y,BOOLEAN; func B_INF(a) ->Function of Y,BOOLEAN equals :: BVFUNC_1:def 13 I_el(Y) if for x being Element of Y holds a.x=TRUE otherwise O_el(Y); func B_SUP(a) ->Function of Y,BOOLEAN equals :: BVFUNC_1:def 14 O_el(Y) if for x being Element of Y holds a.x=FALSE otherwise I_el(Y); end; theorem :: BVFUNC_1:19 for a being Function of Y,BOOLEAN holds 'not' B_INF(a) = B_SUP('not' a) & 'not' B_SUP(a)=B_INF('not' a); theorem :: BVFUNC_1:20 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); registration let Y; cluster O_el(Y) -> constant; end; registration let Y; cluster I_el(Y) -> constant; end; theorem :: BVFUNC_1:21 for a being constant Function of Y,BOOLEAN holds a=O_el(Y) or a=I_el(Y); theorem :: BVFUNC_1:22 for d being constant Function of Y,BOOLEAN holds B_INF(d) = d & B_SUP(d) = d; theorem :: BVFUNC_1:23 for a,b being Function of 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:24 for a being Function of Y,BOOLEAN, d being constant Function of 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:25 for a being Function of Y,BOOLEAN, d being constant Function of 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:26 for a being Function of Y,BOOLEAN,x being Element of Y holds ( B_INF a).x <= a.x; theorem :: BVFUNC_1:27 for a being Function of Y,BOOLEAN,x being Element of Y holds a.x <= (B_SUP a).x; begin :: Chap. 4 Boolean Valued Functions and Partitions definition let Y; let a be Function of Y,BOOLEAN,PA be a_partition of Y; pred a is_dependent_of PA means :: BVFUNC_1:def 15 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:28 for a being Function of Y,BOOLEAN holds a is_dependent_of %I(Y); theorem :: BVFUNC_1:29 for a being constant Function of 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; end; definition let Y; let a be Function of Y,BOOLEAN,PA be a_partition of Y; func B_INF(a,PA) -> Function of Y,BOOLEAN means :: BVFUNC_1:def 16 for y being Element of Y holds ( (for x being Element of Y st x in EqClass(y,PA) holds a.x= TRUE) implies it.y = TRUE ) & (not (for x being Element of Y st x in EqClass(y, PA) holds a.x=TRUE) implies it.y = FALSE); end; definition let Y; let a be Function of Y,BOOLEAN,PA be a_partition of Y; func B_SUP(a,PA) -> Function of Y,BOOLEAN means :: BVFUNC_1:def 17 for y being Element of Y holds ( (ex x being Element of Y st x in EqClass(y,PA) & a.x=TRUE) implies it.y = TRUE ) & (not (ex x being Element of Y st x in EqClass(y,PA) & a .x=TRUE) implies it.y = FALSE); end; theorem :: BVFUNC_1:30 for a being Function of Y,BOOLEAN,PA being a_partition of Y holds B_INF(a,PA) is_dependent_of PA; theorem :: BVFUNC_1:31 for a being Function of Y,BOOLEAN,PA being a_partition of Y holds B_SUP(a,PA) is_dependent_of PA; theorem :: BVFUNC_1:32 for a being Function of Y,BOOLEAN,PA being a_partition of Y holds B_INF(a,PA) '<' a; theorem :: BVFUNC_1:33 for a being Function of Y,BOOLEAN,PA being a_partition of Y holds a '<' B_SUP(a,PA); theorem :: BVFUNC_1:34 for a being Function of Y,BOOLEAN,PA being a_partition of Y holds 'not' B_INF(a,PA) = B_SUP('not' a,PA); theorem :: BVFUNC_1:35 for a being Function of Y,BOOLEAN holds B_INF(a,%O(Y))=B_INF(a); theorem :: BVFUNC_1:36 for a being Function of Y,BOOLEAN holds B_SUP(a,%O(Y))=B_SUP(a); theorem :: BVFUNC_1:37 for a being Function of Y,BOOLEAN holds B_INF(a,%I(Y))=a; theorem :: BVFUNC_1:38 for a being Function of Y,BOOLEAN holds B_SUP(a,%I(Y))=a; theorem :: BVFUNC_1:39 for a,b being Function of 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:40 for a,b being Function of 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 Function of Y,BOOLEAN; func GPart(f) -> a_partition of Y equals :: BVFUNC_1:def 18 {{x where x is Element of Y:f.x = TRUE }, {x9 where x9 is Element of Y:f.x9 = FALSE}} \ {{}}; end; theorem :: BVFUNC_1:41 for a being Function of Y,BOOLEAN holds a is_dependent_of GPart( a); theorem :: BVFUNC_1:42 for a being Function of Y,BOOLEAN,PA being a_partition of Y st a is_dependent_of PA holds PA is_finer_than GPart(a); begin :: BINARI_5 definition let x, y be Element of BOOLEAN; redefine func x 'nand' y -> Element of BOOLEAN; end; definition let x, y be Element of BOOLEAN; redefine func x 'nor' y -> Element of BOOLEAN; end; definition let x, y be boolean object; redefine func x <=> y equals :: BVFUNC_1:def 19 'not' (x 'xor' y); end; definition let x, y be Element of BOOLEAN; redefine func x <=> y -> Element of BOOLEAN; end; reserve x,y,z for boolean object; theorem :: BVFUNC_1:43 TRUE 'nand' x = 'not' x; theorem :: BVFUNC_1:44 FALSE 'nand' x = TRUE; theorem :: BVFUNC_1:45 x 'nand' x = 'not' x & 'not' (x 'nand' x) = x; theorem :: BVFUNC_1:46 'not' (x 'nand' y) = x '&' y; theorem :: BVFUNC_1:47 x 'nand' 'not' x = TRUE & 'not' (x 'nand' 'not' x) = FALSE; theorem :: BVFUNC_1:48 x 'nand' (y '&' z) = 'not' (x '&' y '&' z); theorem :: BVFUNC_1:49 x 'nand' (y '&' z) = (x '&' y) 'nand' z; theorem :: BVFUNC_1:50 TRUE 'nor' x = FALSE; theorem :: BVFUNC_1:51 FALSE 'nor' x = 'not' x; theorem :: BVFUNC_1:52 x 'nor' x = 'not' x & 'not' (x 'nor' x) = x; theorem :: BVFUNC_1:53 'not' (x 'nor' y) = x 'or' y; theorem :: BVFUNC_1:54 x 'nor' 'not' x = FALSE & 'not' (x 'nor' 'not' x) = TRUE; theorem :: BVFUNC_1:55 x 'nor' (y 'or' z) = 'not' (x 'or' y 'or' z); theorem :: BVFUNC_1:56 TRUE <=> x = x; theorem :: BVFUNC_1:57 FALSE <=> x = 'not' x; theorem :: BVFUNC_1:58 x <=> x = TRUE & 'not' (x <=> x) = FALSE; theorem :: BVFUNC_1:59 'not' (x <=> y) = x 'xor' y; theorem :: BVFUNC_1:60 x <=> 'not' x = FALSE & 'not' (x <=> 'not' x) = TRUE; theorem :: BVFUNC_1:61 x <= (y => z) iff x '&' y <= z; theorem :: BVFUNC_1:62 x <=> y = (x => y) '&' (y => x); theorem :: BVFUNC_1:63 x => y = 'not' y => 'not' x; theorem :: BVFUNC_1:64 x <=> y = 'not' x <=> 'not' y; theorem :: BVFUNC_1:65 x=TRUE & (x => y)=TRUE implies y=TRUE; theorem :: BVFUNC_1:66 y=TRUE implies (x => y)=TRUE; theorem :: BVFUNC_1:67 ('not' x)=TRUE implies (x => y)=TRUE; theorem :: BVFUNC_1:68 z => (y => x)=TRUE implies y => (z => x)=TRUE; theorem :: BVFUNC_1:69 z => (y => x)=TRUE & y=TRUE implies z => x=TRUE; theorem :: BVFUNC_1:70 z => (y => x)=TRUE & y=TRUE & z = TRUE implies x=TRUE;