:: 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-2021 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);