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-2021 Association of Mizar Users

definition

let k, l be boolean object ;

redefine pred k <= l means :: BVFUNC_1:def 1
k => l = TRUE ;

compatibility

proof end;

end;

:: deftheorem defines <= BVFUNC_1:def 1 :

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

for f1, f2 being Function of 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

let Y be non empty set ;
let a be Function of Y,BOOLEAN;
:: original: 'not'
redefine func 'not' a -> Function of Y,BOOLEAN;
coherence

proof end;

let b be Function of Y,BOOLEAN;
:: original: '&'
redefine func a '&' b -> Function of Y,BOOLEAN;
coherence

proof end;

end;

definition

let p, q be boolean-valued Function;

func p 'or' q -> boolean-valued Function means :Def2: :: 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) ) );

existence

proof end;

uniqueness

proof end;

commutativity ;
idempotence ;

func p 'xor' q -> Function means :Def3: :: 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) ) );

existence

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def2 defines 'or' BVFUNC_1:def 2 :

:: deftheorem Def3 defines 'xor' BVFUNC_1:def 3 :

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 Function of A,BOOLEAN;

:: original: 'or'
redefine func p 'or' q -> Function of A,BOOLEAN means :Def4: :: BVFUNC_1:def 4
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 -> Function of A,BOOLEAN means :: BVFUNC_1:def 5
for x being Element of A holds it . x = (p . x) 'xor' (q . x);

coherence

proof end;

compatibility

proof end;

end;

:: deftheorem Def4 defines 'or' BVFUNC_1:def 4 :

:: deftheorem defines 'xor' BVFUNC_1:def 5 :

definition

let p, q be boolean-valued Function;

func p 'imp' 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) => (q . x) ) );

existence

proof end;

uniqueness

proof end;

func p 'eqv' q -> Function means :Def7: :: 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) ) );

existence

proof end;

uniqueness

proof end;

commutativity ;

end;

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

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

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 Function of A,BOOLEAN;

:: original: 'imp'
redefine func p 'imp' q -> Function of A,BOOLEAN means :Def8: :: BVFUNC_1:def 8
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 -> Function of A,BOOLEAN means :Def9: :: BVFUNC_1:def 9
for x being Element of A holds it . x = 'not' ((p . x) 'xor' (q . x));

coherence

proof end;

compatibility

proof end;

end;

:: deftheorem Def8 defines 'imp' BVFUNC_1:def 8 :

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

definition

let Y be non empty set ;

func O_el Y -> Function of Y,BOOLEAN means :Def10: :: BVFUNC_1:def 10
for x being Element of Y holds it . x = FALSE ;

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines O_el BVFUNC_1:def 10 :

definition

let Y be non empty set ;

func I_el Y -> Function of Y,BOOLEAN means :Def11: :: BVFUNC_1:def 11
for x being Element of Y holds it . x = TRUE ;

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines I_el BVFUNC_1:def 11 :

theorem :: BVFUNC_1:1

canceled;

::$CT

theorem Th1: :: BVFUNC_1:2

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:3

for Y being non empty set
for a, b being Function of Y,BOOLEAN holds a '&' a = a ;

theorem :: BVFUNC_1:4

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

proof end;

theorem Th4: :: BVFUNC_1:5

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

proof end;

theorem Th5: :: BVFUNC_1:6

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

proof end;

theorem :: BVFUNC_1:7

for Y being non empty set
for a being Function of Y,BOOLEAN holds a 'or' a = a ;

theorem :: BVFUNC_1:8

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

proof end;

theorem Th8: :: BVFUNC_1:9

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

proof end;

theorem Th9: :: BVFUNC_1:10

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

proof end;

theorem :: BVFUNC_1:11

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

proof end;

theorem :: BVFUNC_1:12

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

proof end;

theorem :: BVFUNC_1:13

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

proof end;

theorem :: BVFUNC_1:14

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

proof end;

definition

let Y be non empty set ;
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;

:: deftheorem defines '<' BVFUNC_1:def 12 :

theorem :: BVFUNC_1:15

for Y being non empty set
for a, b, c being Function of Y,BOOLEAN holds
( ( a '<' b & b '<' a implies a = b ) & ( a '<' b & b '<' c implies a '<' c ) )

proof end;

theorem Th15: :: BVFUNC_1:16

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

proof end;

theorem :: BVFUNC_1:17

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

proof end;

theorem :: BVFUNC_1:18

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

proof end;

definition

let Y be non empty set ;
let a be Function of Y,BOOLEAN;

func B_INF a -> Function of Y,BOOLEAN equals :Def13: :: BVFUNC_1:def 13
I_el Y if for x being Element of Y holds a . x = TRUE
otherwise O_el Y;

correctness ;

func B_SUP a -> Function of Y,BOOLEAN equals :Def14: :: BVFUNC_1:def 14
O_el Y if for x being Element of Y holds a . x = FALSE
otherwise I_el Y;

correctness ;

end;

:: deftheorem Def13 defines B_INF BVFUNC_1:def 13 :

:: deftheorem Def14 defines B_SUP BVFUNC_1:def 14 :

theorem Th18: :: BVFUNC_1:19

for Y being non empty set
for a being Function of Y,BOOLEAN holds
( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) )

proof end;

theorem :: BVFUNC_1:20

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;

theorem Th20: :: BVFUNC_1:21

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

proof end;

theorem Th21: :: BVFUNC_1:22

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

proof end;

theorem :: BVFUNC_1:23

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

proof end;

theorem :: BVFUNC_1:24

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

proof end;

theorem :: BVFUNC_1:25

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

proof end;

theorem :: BVFUNC_1:26

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

proof end;

theorem :: BVFUNC_1:27

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

proof end;

definition

let Y be non empty set ;
let a be Function of Y,BOOLEAN;
let 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 holds
for x1, x2 being set st x1 in F & x2 in F holds
a . x1 = a . x2;

end;

:: deftheorem defines is_dependent_of BVFUNC_1:def 15 :

theorem :: BVFUNC_1:28

for Y being non empty set
for a being Function of Y,BOOLEAN holds a is_dependent_of %I Y

proof end;

theorem :: BVFUNC_1:29

for Y being non empty set
for a being constant Function of 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 6;

end;

definition

let Y be non empty set ;
let a be Function of Y,BOOLEAN;
let PA be a_partition of Y;

func B_INF (a,PA) -> Function of Y,BOOLEAN means :Def16: :: 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 ) & ( 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 Def16 defines B_INF BVFUNC_1:def 16 :

definition

let Y be non empty set ;
let a be Function of Y,BOOLEAN;
let PA be a_partition of Y;

func B_SUP (a,PA) -> Function of Y,BOOLEAN means :Def17: :: 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 ) & ( ( 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 Def17 defines B_SUP BVFUNC_1:def 17 :

theorem :: BVFUNC_1:30

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

proof end;

theorem :: BVFUNC_1:31

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

proof end;

theorem :: BVFUNC_1:32

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

proof end;

theorem :: BVFUNC_1:33

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

proof end;

theorem :: BVFUNC_1:34

for Y being non empty set
for a being Function of 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:35

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

proof end;

theorem :: BVFUNC_1:36

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

proof end;

theorem :: BVFUNC_1:37

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

proof end;

theorem :: BVFUNC_1:38

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

proof end;

theorem :: BVFUNC_1:39

for Y being non empty set
for a, b being Function of 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:40

for Y being non empty set
for a, b being Function of 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 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 } } \ {{}};

correctness

proof end;

end;

:: deftheorem defines GPart BVFUNC_1:def 18 :

theorem :: BVFUNC_1:41

for Y being non empty set
for a being Function of Y,BOOLEAN holds a is_dependent_of GPart a

proof end;

theorem :: BVFUNC_1:42

for Y being non empty set
for a being Function of Y,BOOLEAN
for PA being a_partition of Y st a is_dependent_of PA holds
PA is_finer_than GPart a

proof end;

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 object ;

redefine func x <=> y equals :: BVFUNC_1:def 19
'not' (x 'xor' y);

correctness ;

end;

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

definition

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

proof end;

end;

theorem :: BVFUNC_1:43

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

theorem :: BVFUNC_1:44

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

theorem :: BVFUNC_1:45

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

theorem :: BVFUNC_1:46

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

theorem :: BVFUNC_1:47

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

theorem :: BVFUNC_1:48

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

theorem :: BVFUNC_1:49

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

theorem :: BVFUNC_1:50

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

theorem :: BVFUNC_1:51

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

theorem :: BVFUNC_1:52

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

theorem :: BVFUNC_1:53

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

theorem :: BVFUNC_1:54

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

theorem :: BVFUNC_1:55

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

theorem :: BVFUNC_1:56

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

theorem :: BVFUNC_1:57

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

theorem :: BVFUNC_1:58

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

theorem :: BVFUNC_1:59

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

theorem :: BVFUNC_1:60

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

theorem :: BVFUNC_1:61

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

theorem :: BVFUNC_1:62

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

theorem :: BVFUNC_1:63

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

theorem :: BVFUNC_1:64

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

theorem :: BVFUNC_1:65

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

theorem :: BVFUNC_1:66

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

theorem :: BVFUNC_1:67

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

theorem :: BVFUNC_1:68

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

theorem :: BVFUNC_1:69

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

theorem :: BVFUNC_1:70

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