BVFUNC_1: A Theory of Boolean Valued Functions and Partitions

:: A Theory of Boolean Valued Functions and Partitions
:: by Shunichi Kobayashi and Kui Jia
::
:: Received October 22, 1998
:: Copyright (c) 1998-2011 Association of Mizar Users

begin

definition

let k, l be boolean set ;
canceled;
canceled;
redefine pred k <= l means :Def3: :: BVFUNC_1:def 3
k => l = TRUE ;
compatibility

proof end;

end;

:: deftheorem BVFUNC_1:def 1 :

:: deftheorem BVFUNC_1:def 2 :

:: deftheorem Def3 defines <= BVFUNC_1:def 3 :

begin

scheme :: BVFUNC_1:sch 1
BVFUniq1{ F₁() -> non empty set , F₂( set ) -> set } :

for f1, f2 being Element of Funcs (F₁(),BOOLEAN) st ( for x being Element of F₁() holds f1 . x = F₂(x) ) & ( for x being Element of F₁() holds f2 . x = F₂(x) ) holds
f1 = f2

proof end;

definition

canceled;
let Y be non empty set ;
let a be Element of Funcs (Y,BOOLEAN);
:: original: 'not'
redefine func 'not' a -> Element of Funcs (Y,BOOLEAN);
coherence

proof end;

let b be Element of Funcs (Y,BOOLEAN);
:: original: '&'
redefine func a '&' b -> Element of Funcs (Y,BOOLEAN);
coherence

proof end;

end;

:: deftheorem BVFUNC_1:def 4 :

definition

let p, q be boolean-valued Function;
func p 'or' q -> boolean-valued Function means :Def5: :: 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) ) );
existence

proof end;

uniqueness

proof end;

commutativity ;
idempotence ;
func p 'xor' q -> Function means :Def6: :: 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) ) );
existence

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def5 defines 'or' BVFUNC_1:def 5 :

:: deftheorem Def6 defines 'xor' BVFUNC_1:def 6 :

registration

let p, q be boolean-valued Function;
cluster p 'xor' q -> boolean-valued ;
coherence

proof end;

end;

definition

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

proof end;

compatibility

proof end;

:: original: 'xor'
redefine 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);
coherence

proof end;

compatibility

proof end;

end;

:: deftheorem Def7 defines 'or' BVFUNC_1:def 7 :

:: deftheorem defines 'xor' BVFUNC_1:def 8 :

definition

let Y be non empty set ;
let a, b be Element of Funcs (Y,BOOLEAN);
:: original: 'or'
redefine func a 'or' b -> Element of Funcs (Y,BOOLEAN);
coherence

proof end;

:: original: 'xor'
redefine func a 'xor' b -> Element of Funcs (Y,BOOLEAN);
coherence

proof end;

end;

definition

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

proof end;

uniqueness

proof end;

func p 'eqv' q -> Function means :Def10: :: BVFUNC_1:def 10
( dom it = (dom p) /\ (dom q) & ( for x being set st x in dom it holds
it . x = (p . x) <=> (q . x) ) );
existence

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def9 defines 'imp' BVFUNC_1:def 9 :

:: deftheorem Def10 defines 'eqv' BVFUNC_1:def 10 :

registration

let p, q be boolean-valued Function;
cluster p 'imp' q -> boolean-valued ;
coherence

proof end;

cluster p 'eqv' q -> boolean-valued ;
coherence

proof end;

end;

definition

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

proof end;

compatibility

proof end;

:: original: 'eqv'
redefine func p 'eqv' q -> Element of Funcs (A,BOOLEAN) means :Def12: :: BVFUNC_1:def 12
for x being Element of A holds it . x = 'not' ((p . x) 'xor' (q . x));
coherence

proof end;

compatibility

proof end;

end;

:: deftheorem Def11 defines 'imp' BVFUNC_1:def 11 :

:: deftheorem Def12 defines 'eqv' BVFUNC_1:def 12 :

definition

let Y be non empty set ;
let a, b be Element of Funcs (Y,BOOLEAN);
:: original: 'imp'
redefine func a 'imp' b -> Element of Funcs (Y,BOOLEAN);
coherence

proof end;

:: original: 'eqv'
redefine func a 'eqv' b -> Element of Funcs (Y,BOOLEAN);
coherence

proof end;

end;

definition

let Y be non empty set ;
func O_el Y -> Element of Funcs (Y,BOOLEAN) means :Def13: :: BVFUNC_1:def 13
for x being Element of Y holds it . x = FALSE ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines O_el BVFUNC_1:def 13 :

definition

let Y be non empty set ;
func I_el Y -> Element of Funcs (Y,BOOLEAN) means :Def14: :: BVFUNC_1:def 14
for x being Element of Y holds it . x = TRUE ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines I_el BVFUNC_1:def 14 :

theorem :: BVFUNC_1:1

canceled;

theorem :: BVFUNC_1:2

canceled;

theorem :: BVFUNC_1:3

canceled;

theorem :: BVFUNC_1:4

for a being boolean-valued Function holds 'not' ('not' a) = a ;

theorem Th5: :: BVFUNC_1:5

for Y being non empty set holds
( 'not' (I_el Y) = O_el Y & 'not' (O_el Y) = I_el Y )

proof end;

theorem :: BVFUNC_1:6

for Y being non empty set
for a, b being Element of Funcs (Y,BOOLEAN) holds a '&' a = a ;

theorem :: BVFUNC_1:7

for Y being non empty set
for a, b, c being Element of Funcs (Y,BOOLEAN) holds (a '&' b) '&' c = a '&' (b '&' c)

proof end;

theorem Th8: :: BVFUNC_1:8

for Y being non empty set
for a being Element of Funcs (Y,BOOLEAN) holds a '&' (O_el Y) = O_el Y

proof end;

theorem Th9: :: BVFUNC_1:9

for Y being non empty set
for a being Element of Funcs (Y,BOOLEAN) holds a '&' (I_el Y) = a

proof end;

theorem :: BVFUNC_1:10

for Y being non empty set
for a being Element of Funcs (Y,BOOLEAN) holds a 'or' a = a ;

theorem :: BVFUNC_1:11

for Y being non empty set
for a, b, c being Element of Funcs (Y,BOOLEAN) holds (a 'or' b) 'or' c = a 'or' (b 'or' c)

proof end;

theorem Th12: :: BVFUNC_1:12

for Y being non empty set
for a being Element of Funcs (Y,BOOLEAN) holds a 'or' (O_el Y) = a

proof end;

theorem Th13: :: BVFUNC_1:13

for Y being non empty set
for a being Element of Funcs (Y,BOOLEAN) holds a 'or' (I_el Y) = I_el Y

proof end;

theorem :: BVFUNC_1:14

for Y being non empty set
for a, b, c being Element of Funcs (Y,BOOLEAN) holds (a '&' b) 'or' c = (a 'or' c) '&' (b 'or' c)

proof end;

theorem :: BVFUNC_1:15

for Y being non empty set
for a, b, c being Element of Funcs (Y,BOOLEAN) holds (a 'or' b) '&' c = (a '&' c) 'or' (b '&' c)

proof end;

theorem :: BVFUNC_1:16

for Y being non empty set
for a, b being Element of Funcs (Y,BOOLEAN) holds 'not' (a 'or' b) = ('not' a) '&' ('not' b)

proof end;

theorem :: BVFUNC_1:17

for Y being non empty set
for a, b being Element of Funcs (Y,BOOLEAN) holds 'not' (a '&' b) = ('not' a) 'or' ('not' b)

proof end;

definition

let Y be non empty set ;
let a, b be Element of Funcs (Y,BOOLEAN);
pred a '<' b means :Def15: :: BVFUNC_1:def 15
for x being Element of Y st a . x = TRUE holds
b . x = TRUE ;
reflexivity ;

end;

:: deftheorem Def15 defines '<' BVFUNC_1:def 15 :

theorem :: BVFUNC_1:18

for Y being non empty set
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 ) )

proof end;

theorem Th19: :: BVFUNC_1:19

for Y being non empty set
for a, b being Element of Funcs (Y,BOOLEAN) holds
( a 'imp' b = I_el Y iff a '<' b )

proof end;

theorem :: BVFUNC_1:20

for Y being non empty set
for a, b being Element of Funcs (Y,BOOLEAN) holds
( a 'eqv' b = I_el Y iff a = b )

proof end;

theorem :: BVFUNC_1:21

for Y being non empty set
for a being Element of Funcs (Y,BOOLEAN) holds
( O_el Y '<' a & a '<' I_el Y )

proof end;

begin

definition

let Y be non empty set ;
let a be Element of Funcs (Y,BOOLEAN);
func B_INF a -> Element of Funcs (Y,BOOLEAN) equals :Def16: :: BVFUNC_1:def 16
I_el Y if for x being Element of Y holds a . x = TRUE
otherwise O_el Y;
correctness ;
func B_SUP a -> Element of Funcs (Y,BOOLEAN) equals :Def17: :: BVFUNC_1:def 17
O_el Y if for x being Element of Y holds a . x = FALSE
otherwise I_el Y;
correctness ;

end;

:: deftheorem Def16 defines B_INF BVFUNC_1:def 16 :

:: deftheorem Def17 defines B_SUP BVFUNC_1:def 17 :

theorem Th22: :: BVFUNC_1:22

for Y being non empty set
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) )

proof end;

theorem :: BVFUNC_1:23

for Y being non empty set holds
( 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 )

proof end;

registration

let Y be non empty set ;
cluster O_el Y -> constant ;
coherence

proof end;

end;

registration

let Y be non empty set ;
cluster I_el Y -> constant ;
coherence

proof end;

end;

registration

let Y be non empty set ;
cluster Relation-like Function-like constant V21(Y) quasi_total boolean-valued Element of Funcs (Y,BOOLEAN);
existence

proof end;

end;

theorem Th24: :: BVFUNC_1:24

for Y being non empty set
for a being constant Element of Funcs (Y,BOOLEAN) holds
( a = O_el Y or a = I_el Y )

proof end;

theorem Th25: :: BVFUNC_1:25

for Y being non empty set
for d being constant Element of Funcs (Y,BOOLEAN) holds
( B_INF d = d & B_SUP d = d )

proof end;

theorem :: BVFUNC_1:26

for Y being non empty set
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) )

proof end;

theorem :: BVFUNC_1:27

for Y being non empty set
for a being Element of Funcs (Y,BOOLEAN)
for 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 )

proof end;

theorem :: BVFUNC_1:28

for Y being non empty set
for a being Element of Funcs (Y,BOOLEAN)
for 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 )

proof end;

theorem :: BVFUNC_1:29

for Y being non empty set
for a being Element of Funcs (Y,BOOLEAN)
for x being Element of Y holds (B_INF a) . x <= a . x

proof end;

theorem :: BVFUNC_1:30

for Y being non empty set
for a being Element of Funcs (Y,BOOLEAN)
for x being Element of Y holds a . x <= (B_SUP a) . x

proof end;

begin

definition

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

end;

:: deftheorem Def18 defines is_dependent_of BVFUNC_1:def 18 :

theorem :: BVFUNC_1:31

for Y being non empty set
for a being Element of Funcs (Y,BOOLEAN) holds a is_dependent_of %I Y

proof end;

theorem :: BVFUNC_1:32

for Y being non empty set
for a being constant Element of Funcs (Y,BOOLEAN) holds a is_dependent_of %O Y

proof end;

definition

let Y be non empty set ;
let PA be a_partition of Y;
:: original: Element
redefine mode Element of PA -> Subset of Y;
coherence

proof end;

end;

definition

let Y be non empty set ;
let x be Element of Y;
let PA be a_partition of Y;
:: original: EqClass
redefine func EqClass (x,PA) -> Element of PA;
coherence by EQREL_1:def 8;

end;

definition

let Y be non empty set ;
let a be Element of Funcs (Y,BOOLEAN);
let PA be a_partition of Y;
func B_INF (a,PA) -> Element of Funcs (Y,BOOLEAN) means :Def19: :: BVFUNC_1:def 19
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 ) & ( ex x being Element of Y st
( x in EqClass (y,PA) & not a . x = TRUE ) implies it . y = FALSE ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines B_INF BVFUNC_1:def 19 :

definition

let Y be non empty set ;
let a be Element of Funcs (Y,BOOLEAN);
let PA be a_partition of Y;
func B_SUP (a,PA) -> Element of Funcs (Y,BOOLEAN) means :Def20: :: BVFUNC_1:def 20
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 ) & ( ( for x being Element of Y holds
( not x in EqClass (y,PA) or not a . x = TRUE ) ) implies it . y = FALSE ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines B_SUP BVFUNC_1:def 20 :

theorem :: BVFUNC_1:33

for Y being non empty set
for a being Element of Funcs (Y,BOOLEAN)
for PA being a_partition of Y holds B_INF (a,PA) is_dependent_of PA

proof end;

theorem :: BVFUNC_1:34

for Y being non empty set
for a being Element of Funcs (Y,BOOLEAN)
for PA being a_partition of Y holds B_SUP (a,PA) is_dependent_of PA

proof end;

theorem :: BVFUNC_1:35

for Y being non empty set
for a being Element of Funcs (Y,BOOLEAN)
for PA being a_partition of Y holds B_INF (a,PA) '<' a

proof end;

theorem :: BVFUNC_1:36

for Y being non empty set
for a being Element of Funcs (Y,BOOLEAN)
for PA being a_partition of Y holds a '<' B_SUP (a,PA)

proof end;

theorem :: BVFUNC_1:37

for Y being non empty set
for a being Element of Funcs (Y,BOOLEAN)
for PA being a_partition of Y holds 'not' (B_INF (a,PA)) = B_SUP (('not' a),PA)

proof end;

theorem :: BVFUNC_1:38

for Y being non empty set
for a being Element of Funcs (Y,BOOLEAN) holds B_INF (a,(%O Y)) = B_INF a

proof end;

theorem :: BVFUNC_1:39

for Y being non empty set
for a being Element of Funcs (Y,BOOLEAN) holds B_SUP (a,(%O Y)) = B_SUP a

proof end;

theorem :: BVFUNC_1:40

for Y being non empty set
for a being Element of Funcs (Y,BOOLEAN) holds B_INF (a,(%I Y)) = a

proof end;

theorem :: BVFUNC_1:41

for Y being non empty set
for a being Element of Funcs (Y,BOOLEAN) holds B_SUP (a,(%I Y)) = a

proof end;

theorem :: BVFUNC_1:42

for Y being non empty set
for a, b being Element of Funcs (Y,BOOLEAN)
for PA being a_partition of Y holds B_INF ((a '&' b),PA) = (B_INF (a,PA)) '&' (B_INF (b,PA))

proof end;

theorem :: BVFUNC_1:43

for Y being non empty set
for a, b being Element of Funcs (Y,BOOLEAN)
for PA being a_partition of Y holds B_SUP ((a 'or' b),PA) = (B_SUP (a,PA)) 'or' (B_SUP (b,PA))

proof end;

definition

let Y be non empty set ;
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 } , { x9 where x9 is Element of Y : f . x9 = FALSE } } \ {{}};
correctness

proof end;

end;

:: deftheorem defines GPart BVFUNC_1:def 21 :

theorem :: BVFUNC_1:44

for Y being non empty set
for a being Element of Funcs (Y,BOOLEAN) holds a is_dependent_of GPart a

proof end;

theorem :: BVFUNC_1:45

for Y being non empty set
for a being Element of Funcs (Y,BOOLEAN)
for PA being a_partition of Y st a is_dependent_of PA holds
PA is_finer_than GPart a

proof end;

begin

definition

let x, y be Element of BOOLEAN ;
:: original: 'nand'
redefine func x 'nand' y -> Element of BOOLEAN ;
correctness

proof end;

end;

definition

let x, y be Element of BOOLEAN ;
:: original: 'nor'
redefine func x 'nor' y -> Element of BOOLEAN ;
correctness

proof end;

end;

definition

let x, y be boolean set ;
redefine func x <=> y equals :: BVFUNC_1:def 22
'not' (x 'xor' y);
correctness ;

end;

:: deftheorem defines <=> BVFUNC_1:def 22 :

definition

let x, y be Element of BOOLEAN ;
:: original: <=>
redefine func x <=> y -> Element of BOOLEAN ;
correctness

proof end;

end;

theorem :: BVFUNC_1:46

for x being boolean set holds TRUE 'nand' x = 'not' x ;

theorem :: BVFUNC_1:47

for x being boolean set holds FALSE 'nand' x = TRUE ;

theorem :: BVFUNC_1:48

for x being boolean set holds
( x 'nand' x = 'not' x & 'not' (x 'nand' x) = x ) ;

theorem :: BVFUNC_1:49

for x, y being boolean set holds 'not' (x 'nand' y) = x '&' y ;

theorem :: BVFUNC_1:50

for x being boolean set holds
( x 'nand' ('not' x) = TRUE & 'not' (x 'nand' ('not' x)) = FALSE ) by XBOOLEAN:135, XBOOLEAN:138;

theorem :: BVFUNC_1:51

for x, y, z being boolean set holds x 'nand' (y '&' z) = 'not' ((x '&' y) '&' z) ;

theorem :: BVFUNC_1:52

for x, y, z being boolean set holds x 'nand' (y '&' z) = (x '&' y) 'nand' z ;

theorem :: BVFUNC_1:53

for x being boolean set holds TRUE 'nor' x = FALSE ;

theorem :: BVFUNC_1:54

for x being boolean set holds FALSE 'nor' x = 'not' x ;

theorem :: BVFUNC_1:55

for x being boolean set holds
( x 'nor' x = 'not' x & 'not' (x 'nor' x) = x ) ;

theorem :: BVFUNC_1:56

for x, y being boolean set holds 'not' (x 'nor' y) = x 'or' y ;

theorem :: BVFUNC_1:57

for x being boolean set holds
( x 'nor' ('not' x) = FALSE & 'not' (x 'nor' ('not' x)) = TRUE ) by XBOOLEAN:134, XBOOLEAN:138;

theorem :: BVFUNC_1:58

for x, y, z being boolean set holds x 'nor' (y 'or' z) = 'not' ((x 'or' y) 'or' z) ;

theorem :: BVFUNC_1:59

for x being boolean set holds TRUE <=> x = x ;

theorem :: BVFUNC_1:60

for x being boolean set holds FALSE <=> x = 'not' x ;

theorem :: BVFUNC_1:61

for x being boolean set holds
( x <=> x = TRUE & 'not' (x <=> x) = FALSE ) by XBOOLEAN:125, XBOOLEAN:143;

theorem :: BVFUNC_1:62

for x, y being boolean set holds 'not' (x <=> y) = x 'xor' y ;

theorem :: BVFUNC_1:63

for x being boolean set holds
( x <=> ('not' x) = FALSE & 'not' (x <=> ('not' x)) = TRUE ) by XBOOLEAN:129, XBOOLEAN:142;

theorem :: BVFUNC_1:64

for x, y, z being boolean set holds
( x <= y => z iff x '&' y <= z )

proof end;

theorem :: BVFUNC_1:65

for x, y being boolean set holds x <=> y = (x => y) '&' (y => x) ;

theorem :: BVFUNC_1:66

for x, y being boolean set holds x => y = ('not' y) => ('not' x) ;

theorem :: BVFUNC_1:67

for x, y being boolean set holds x <=> y = ('not' x) <=> ('not' y) ;

theorem :: BVFUNC_1:68

for x, y being boolean set st x = TRUE & x => y = TRUE holds
y = TRUE ;

theorem :: BVFUNC_1:69

for y, x being boolean set st y = TRUE holds
x => y = TRUE ;

theorem :: BVFUNC_1:70

for x, y being boolean set st 'not' x = TRUE holds
x => y = TRUE ;

theorem :: BVFUNC_1:71

for z, y, x being boolean set st z => (y => x) = TRUE holds
y => (z => x) = TRUE ;

theorem :: BVFUNC_1:72

for z, y, x being boolean set st z => (y => x) = TRUE & y = TRUE holds
z => x = TRUE ;

theorem :: BVFUNC_1:73

for z, y, x being boolean set st z => (y => x) = TRUE & y = TRUE & z = TRUE holds
x = TRUE ;