:: A Theory of Boolean Valued Functions and Quantifiers with
:: Respect to Partitions
:: by Shunichi Kobayashi and Yatsuka Nakamura
::
:: Received December 21, 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 XBOOLE_0, SUBSET_1, PARTIT1, EQREL_1, TARSKI, ZFMISC_1, FUNCT_1,
SETFAM_1, RELAT_1, PARTFUN1, MARGREL1, BVFUNC_1, XBOOLEAN, BVFUNC_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XBOOLEAN, MARGREL1, RELAT_1,
FUNCT_1, SETFAM_1, RELSET_1, PARTFUN1, FUNCT_2, EQREL_1, PARTIT1,
BVFUNC_1;
constructors SETFAM_1, PARTIT1, BVFUNC_1, RELSET_1, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELSET_1, XBOOLEAN, EQREL_1, MARGREL1,
PARTIT1;
requirements SUBSET, BOOLE, NUMERALS;
begin :: Chap. 1 Preliminaries
reserve Y for non empty set,
G for Subset of PARTITIONS(Y);
definition
let X be set;
redefine func PARTITIONS X -> Part-Family of X;
end;
definition
let X be set;
let F be non empty Part-Family of X;
redefine mode Element of F -> a_partition of X;
end;
theorem :: BVFUNC_2:1
for y being Element of Y ex X being Subset of Y st y in X & ex h
being Function, F being Subset-Family of Y st dom h=G & rng h = F & (for d
being set st d in G holds h.d in d) & X=Intersect F & X<>{};
definition
let Y;
let G be Subset of PARTITIONS(Y);
func '/\' G -> a_partition of Y means
:: BVFUNC_2:def 1
for x being set holds x in it
iff ex h being Function, F being Subset-Family of Y st dom h=G & rng h = F & (
for d being set st d in G holds h.d in d) & x=Intersect F & x<>{};
end;
definition
let Y;
let G be Subset of PARTITIONS(Y),b be set;
pred b is_upper_min_depend_of G means
:: BVFUNC_2:def 2
(for d being a_partition of Y
st d in G holds b is_a_dependent_set_of d) & for e being set st e c= b & (for d
being a_partition of Y st d in G holds e is_a_dependent_set_of d) holds e=b;
end;
theorem :: BVFUNC_2:2
for y being Element of Y st G<>{} holds ex X being Subset of Y st
y in X & X is_upper_min_depend_of G;
definition
let Y;
let G be Subset of PARTITIONS(Y);
func '\/' G -> a_partition of Y means
:: BVFUNC_2:def 3
for x being set holds x in it
iff x is_upper_min_depend_of G if G<>{} otherwise it = %I(Y);
end;
theorem :: BVFUNC_2:3
for G being Subset of PARTITIONS(Y),PA being a_partition of Y st PA in
G holds PA '>' ('/\' G);
theorem :: BVFUNC_2:4
for G being Subset of PARTITIONS(Y),PA being a_partition of Y st PA in
G holds PA '<' ('\/' G);
begin :: Chap. 2 Coordinate and Quantifiers
definition
let Y;
let G be Subset of PARTITIONS(Y);
attr G is generating means
:: BVFUNC_2:def 4
('/\' G) = %I(Y);
end;
definition
let Y;
let G be Subset of PARTITIONS(Y);
attr G is independent means
:: BVFUNC_2:def 5
for h being Function, F being Subset-Family of Y
st dom h=G & rng h=F & (for d being set st d in G holds h.d in d) holds (
Intersect F)<>{};
end;
definition
let Y;
let G be Subset of PARTITIONS(Y);
pred G is_a_coordinate means
:: BVFUNC_2:def 6
G is independent generating;
end;
definition
let Y;
let PA be a_partition of Y;
redefine func {PA} -> Subset of PARTITIONS(Y);
end;
definition
let Y;
let PA be a_partition of Y;
let G be Subset of PARTITIONS(Y);
func CompF(PA,G) -> a_partition of Y equals
:: BVFUNC_2:def 7
'/\' (G \ {PA});
end;
definition
let Y;
let a be Function of Y,BOOLEAN;
let G be Subset of PARTITIONS(Y),PA be a_partition of Y;
pred a is_independent_of PA,G means
:: BVFUNC_2:def 8
a is_dependent_of CompF(PA,G);
end;
definition
let Y;
let a be Function of Y,BOOLEAN, G be Subset of PARTITIONS(Y), PA be
a_partition of Y;
func All(a,PA,G) -> Function of Y,BOOLEAN equals
:: BVFUNC_2:def 9
B_INF(a,CompF(PA,G));
end;
definition
let Y;
let a be Function of Y,BOOLEAN, G be Subset of PARTITIONS(Y), PA be
a_partition of Y;
func Ex(a,PA,G) -> Function of Y,BOOLEAN equals
:: BVFUNC_2:def 10
B_SUP(a,CompF(PA,G));
end;
theorem :: BVFUNC_2:5
for a being Function of Y,BOOLEAN, PA being a_partition of Y
holds All(a,PA,G) is_dependent_of CompF(PA,G);
theorem :: BVFUNC_2:6
for a being Function of Y,BOOLEAN, PA being a_partition of Y
holds Ex(a,PA,G) is_dependent_of CompF(PA,G);
theorem :: BVFUNC_2:7
for a being Function of Y,BOOLEAN, PA being a_partition of Y
holds All(I_el(Y),PA,G) = I_el(Y);
theorem :: BVFUNC_2:8
for a being Function of Y,BOOLEAN, PA being a_partition of Y
holds Ex(I_el(Y),PA,G) = I_el(Y);
theorem :: BVFUNC_2:9
for a being Function of Y,BOOLEAN, PA being a_partition of Y
holds All(O_el(Y),PA,G) = O_el(Y);
theorem :: BVFUNC_2:10
for a being Function of Y,BOOLEAN, PA being a_partition of Y
holds Ex(O_el(Y),PA,G) = O_el(Y);
theorem :: BVFUNC_2:11
for a being Function of Y,BOOLEAN, PA being a_partition of Y
holds All(a,PA,G) '<' a;
theorem :: BVFUNC_2:12
for a being Function of Y,BOOLEAN, PA being a_partition of Y
holds a '<' Ex(a,PA,G);
theorem :: BVFUNC_2:13
for a,b being Function of Y,BOOLEAN, PA being a_partition of Y
holds All(a,PA,G) 'or' All(b,PA,G) '<' All(a 'or' b,PA,G);
theorem :: BVFUNC_2:14
for a,b being Function of Y,BOOLEAN, PA being a_partition of Y
holds All(a 'imp' b,PA,G) '<' All(a,PA,G) 'imp' All(b,PA,G);
theorem :: BVFUNC_2:15
for a,b being Function of Y,BOOLEAN,G being Subset of PARTITIONS
(Y) , PA being a_partition of Y holds Ex(a '&' b,PA,G) '<' Ex(a,PA,G) '&' Ex(b,
PA,G);
theorem :: BVFUNC_2:16
for a,b being Function of Y,BOOLEAN, PA being a_partition of Y
holds Ex(a,PA,G) 'xor' Ex(b,PA,G) '<' Ex(a 'xor' b,PA,G);
theorem :: BVFUNC_2:17
for a,b being Function of Y,BOOLEAN, PA being a_partition of Y
holds Ex(a,PA,G) 'imp' Ex(b,PA,G) '<' Ex(a 'imp' b,PA,G);
reserve a, u for Function of Y,BOOLEAN;
theorem :: BVFUNC_2:18 :: De'Morgan's Law
for PA being a_partition of Y holds 'not' All(a,PA,G) = Ex('not' a,PA, G);
theorem :: BVFUNC_2:19 :: De'Morgan's Law
for PA being a_partition of Y holds 'not' Ex(a,PA,G) = All('not' a,PA, G);
theorem :: BVFUNC_2:20
for PA being a_partition of Y st u is_independent_of PA,G holds All(u
'imp' a,PA,G) = u 'imp' All(a,PA,G);
theorem :: BVFUNC_2:21
for PA being a_partition of Y st u is_independent_of PA,G holds All(a
'imp' u,PA,G) = Ex(a,PA,G) 'imp' u;
theorem :: BVFUNC_2:22
for PA being a_partition of Y st u is_independent_of PA,G holds
All(u 'or' a,PA,G) = u 'or' All(a,PA,G);
theorem :: BVFUNC_2:23
for PA being a_partition of Y st u is_independent_of PA,G holds All(a
'or' u,PA,G) = All(a,PA,G) 'or' u;
theorem :: BVFUNC_2:24
for PA being a_partition of Y st u is_independent_of PA,G holds All(a
'or' u,PA,G) '<' Ex(a,PA,G) 'or' u;
theorem :: BVFUNC_2:25
for PA being a_partition of Y st u is_independent_of PA,G holds
All(u '&' a,PA,G) = u '&' All(a,PA,G);
theorem :: BVFUNC_2:26
for PA being a_partition of Y st u is_independent_of PA,G holds All(a
'&' u,PA,G) = All(a,PA,G) '&' u;
theorem :: BVFUNC_2:27
for PA being a_partition of Y holds All(a '&' u,PA,G) '<' Ex(a,PA,G) '&' u;
theorem :: BVFUNC_2:28
for PA being a_partition of Y st u is_independent_of PA,G holds
All(u 'xor' a,PA,G) '<' u 'xor' All(a,PA,G);
theorem :: BVFUNC_2:29
for PA being a_partition of Y st u is_independent_of PA,G holds All(a
'xor' u,PA,G) '<' All(a,PA,G) 'xor' u;
theorem :: BVFUNC_2:30
for PA being a_partition of Y st u is_independent_of PA,G holds
All(u 'eqv' a,PA,G) '<' u 'eqv' All(a,PA,G);
theorem :: BVFUNC_2:31
for PA being a_partition of Y st u is_independent_of PA,G holds All(a
'eqv' u,PA,G) '<' All(a,PA,G) 'eqv' u;
theorem :: BVFUNC_2:32
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex(u 'or' a,PA,G) = u 'or' Ex(a,PA,G);
theorem :: BVFUNC_2:33
for PA being a_partition of Y st u is_independent_of PA,G holds Ex(a
'or' u,PA,G) = Ex(a,PA,G) 'or' u;
theorem :: BVFUNC_2:34
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex(u '&' a,PA,G) = u '&' Ex(a,PA,G);
theorem :: BVFUNC_2:35
for PA being a_partition of Y st u is_independent_of PA,G holds Ex(a
'&' u,PA,G) = Ex(a,PA,G) '&' u;
theorem :: BVFUNC_2:36
for PA being a_partition of Y holds u 'imp' Ex(a,PA,G) '<' Ex(u 'imp' a,PA,G)
;
theorem :: BVFUNC_2:37
for PA being a_partition of Y holds Ex(a,PA,G) 'imp' u '<' Ex(a 'imp' u,PA,G)
;
theorem :: BVFUNC_2:38
for PA being a_partition of Y st u is_independent_of PA,G holds
u 'xor' Ex(a,PA,G) '<' Ex(u 'xor' a,PA,G);
theorem :: BVFUNC_2:39
for PA being a_partition of Y st u is_independent_of PA,G holds Ex(a,
PA,G) 'xor' u '<' Ex(a 'xor' u,PA,G);