:: A Theory of Boolean Valued Functions and Partitions
:: by Shunichi Kobayashi and Kui Jia
::
:: Received October 22, 1998
:: Copyright (c) 1998-2016 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;