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 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 means :Def16: :: BVFUNC_1:def 16
it = I_el Y if for x being Element of Y holds a . x = TRUE
otherwise it = O_el Y;
correctness ;
func B_SUP a -> Element of Funcs Y,BOOLEAN means :Def17: :: BVFUNC_1:def 17
it = O_el Y if for x being Element of Y holds a . x = FALSE
otherwise it = 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;