:: Manysorted Sets
::  by Andrzej Trybulec
::
:: Received July 7, 1993
:: Copyright (c) 1993-2012 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 FUNCT_1, RELAT_1, SETFAM_1, XBOOLE_0, SUBSET_1, PARTFUN1,
      FUNCOP_1, TARSKI, FUNCT_2, ZFMISC_1, MEMBER_1, FUNCT_4, PBOOLE, NAT_1;
 notations TARSKI, ZFMISC_1, XBOOLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
      ORDINAL1, PARTFUN1, FUNCT_2, FUNCT_4, FUNCOP_1;
 constructors SETFAM_1, FUNCOP_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_4;
 registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1, FUNCT_4;
 requirements BOOLE, SUBSET;


begin

reserve i,j,e,u for set;

theorem :: PBOOLE:1
  for f being Function st f is non-empty holds rng f is
  with_non-empty_elements;

theorem :: PBOOLE:2
  for f being Function holds f is empty-yielding iff f = {} or rng f = {
  {} };

reserve I for set; :: of indices

registration
  let I;
  cluster total for I-defined Function;
end;

definition
  let I;
  mode ManySortedSet of I is total I-defined Function;
end;

reserve x,X,Y,Z,V for ManySortedSet of I;

scheme :: PBOOLE:sch 1

  KuratowskiFunction{A()-> set, F(set) -> set}:
 ex f being ManySortedSet of A() st for e st e in A() holds f.e in F(e)
provided
 for e st e in A() holds F(e) <> {};

definition
  let I,X,Y;
  pred X in Y means
:: PBOOLE:def 1

  for i st i in I holds X.i in Y.i;
  pred X c= Y means
:: PBOOLE:def 2

  for i st i in I holds X.i c= Y.i;
  reflexivity;
end;

definition
  let I be non empty set,X,Y be ManySortedSet of I;
  redefine pred X in Y;
  asymmetry;
end;

scheme :: PBOOLE:sch 2

  PSeparation { I()-> set, A() -> ManySortedSet of I(), P[set,set] } : ex X
being ManySortedSet of I() st for i being set st i in I() for e holds e in X.i
  iff e in A().i & P[i,e];

theorem :: PBOOLE:3
  (for i st i in I holds X.i = Y.i) implies X = Y;

definition
  let I;
  func [[0]]I -> ManySortedSet of I equals
:: PBOOLE:def 3
  I --> {};
  let X,Y;
  func X \/ Y -> ManySortedSet of I means
:: PBOOLE:def 4

  for i st i in I holds it.i = X.i \/ Y.i;
  commutativity;
  idempotence;
  func X /\ Y -> ManySortedSet of I means
:: PBOOLE:def 5

  for i st i in I holds it.i = X.i /\ Y.i;
  commutativity;
  idempotence;
  func X \ Y -> ManySortedSet of I means
:: PBOOLE:def 6

  for i st i in I holds it.i = X.i \ Y.i;
  pred X overlaps Y means
:: PBOOLE:def 7

  for i st i in I holds X.i meets Y.i;
  symmetry;
  pred X misses Y means
:: PBOOLE:def 8

  for i st i in I holds X.i misses Y.i;
  symmetry;
end;

notation
  let I;
  let X,Y;
  antonym X meets Y for X misses Y;
end;

definition
  let I,X,Y;
  func X \+\ Y -> ManySortedSet of I equals
:: PBOOLE:def 9
  (X \ Y) \/ (Y \ X);
  commutativity;
end;

theorem :: PBOOLE:4
  for i st i in I holds (X \+\ Y).i = X.i \+\ Y.i;

theorem :: PBOOLE:5
  [[0]]I.i = {};

theorem :: PBOOLE:6
  (for i st i in I holds X.i = {}) implies X = [[0]]I;

theorem :: PBOOLE:7
  x in X or x in Y implies x in X \/ Y;

theorem :: PBOOLE:8
  x in X /\ Y iff x in X & x in Y;

theorem :: PBOOLE:9
  x in X & X c= Y implies x in Y;

theorem :: PBOOLE:10
  x in X & x in Y implies X overlaps Y;

theorem :: PBOOLE:11
  X overlaps Y implies ex x st x in X & x in Y;

theorem :: PBOOLE:12
  x in X \ Y implies x in X;

begin

definition
  let I,X,Y;
  redefine pred X = Y means
:: PBOOLE:def 10
  for i st i in I holds X.i = Y.i;
end;

theorem :: PBOOLE:13
  X c= Y & Y c= Z implies X c= Z;

theorem :: PBOOLE:14
  X c= X \/ Y;

theorem :: PBOOLE:15
  X /\ Y c= X;

theorem :: PBOOLE:16
  X c= Z & Y c= Z implies X \/ Y c= Z;

theorem :: PBOOLE:17
  Z c= X & Z c= Y implies Z c= X /\ Y;

theorem :: PBOOLE:18
  X c= Y implies X \/ Z c= Y \/ Z;

theorem :: PBOOLE:19
  X c= Y implies X /\ Z c= Y /\ Z;

theorem :: PBOOLE:20
  X c= Y & Z c= V implies X \/ Z c= Y \/ V;

theorem :: PBOOLE:21
  X c= Y & Z c= V implies X /\ Z c= Y /\ V;

theorem :: PBOOLE:22
  X c= Y implies X \/ Y = Y;

theorem :: PBOOLE:23
  X c= Y implies X /\ Y = X;

theorem :: PBOOLE:24
  X /\ Y c= X \/ Z;

theorem :: PBOOLE:25
  X c= Z implies X \/ Y /\ Z = (X \/ Y) /\ Z;

theorem :: PBOOLE:26
  X = Y \/ Z iff Y c= X & Z c= X & for V st Y c= V & Z c= V holds X c= V;

theorem :: PBOOLE:27
  X = Y /\ Z iff X c= Y & X c= Z & for V st V c= Y & V c= Z holds V c= X;

theorem :: PBOOLE:28
  (X \/ Y) \/ Z = X \/ (Y \/ Z);

theorem :: PBOOLE:29
  (X /\ Y) /\ Z = X /\ (Y /\ Z);

theorem :: PBOOLE:30
  X /\ (X \/ Y) = X;

theorem :: PBOOLE:31
  X \/ (X /\ Y) = X;

theorem :: PBOOLE:32
  X /\ (Y \/ Z) = X /\ Y \/ X /\ Z;

theorem :: PBOOLE:33
  X \/ Y /\ Z = (X \/ Y) /\ (X \/ Z);

theorem :: PBOOLE:34
  (X /\ Y) \/ (X /\ Z) = X implies X c= Y \/ Z;

theorem :: PBOOLE:35
  (X \/ Y) /\ (X \/ Z) = X implies Y /\ Z c= X;

theorem :: PBOOLE:36
  (X /\ Y) \/ (Y /\ Z) \/ (Z /\ X) = (X \/ Y) /\ (Y \/ Z) /\ (Z \/ X);

theorem :: PBOOLE:37
  X \/ Y c= Z implies X c= Z;

theorem :: PBOOLE:38
  X c= Y /\ Z implies X c= Y;

theorem :: PBOOLE:39
  X \/ Y \/ Z = (X \/ Z) \/ (Y \/ Z);

theorem :: PBOOLE:40
  X /\ Y /\ Z = (X /\ Z) /\ (Y /\ Z);

theorem :: PBOOLE:41
  X \/ (X \/ Y) = X \/ Y;

theorem :: PBOOLE:42
  X /\ (X /\ Y) = X /\ Y;

begin :: ManySortedSet with empty components

theorem :: PBOOLE:43
  [[0]]I c= X;

theorem :: PBOOLE:44
  X c= [[0]]I implies X = [[0]]I;

theorem :: PBOOLE:45
  X c= Y & X c= Z & Y /\ Z = [[0]]I implies X = [[0]]I;

theorem :: PBOOLE:46
  X c= Y & Y /\ Z = [[0]]I implies X /\ Z = [[0]]I;

theorem :: PBOOLE:47
  X \/ [[0]]I = X & [[0]]I \/ X = X;

theorem :: PBOOLE:48
  X \/ Y = [[0]]I implies X = [[0]]I;

theorem :: PBOOLE:49
  X /\ [[0]]I = [[0]]I;

theorem :: PBOOLE:50
  X c= (Y \/ Z) & X /\ Z = [[0]]I implies X c= Y;

theorem :: PBOOLE:51
  Y c= X & X /\ Y = [[0]]I implies Y = [[0]]I;

begin :: Difference and symmetric difference

theorem :: PBOOLE:52
  X \ Y = [[0]]I iff X c= Y;

theorem :: PBOOLE:53
  X c= Y implies X \ Z c= Y \ Z;

theorem :: PBOOLE:54
  X c= Y implies Z \ Y c= Z \ X;

theorem :: PBOOLE:55
  X c= Y & Z c= V implies X \ V c= Y \ Z;

theorem :: PBOOLE:56
  X \ Y c= X;

theorem :: PBOOLE:57
  X c= Y \ X implies X = [[0]]I;

theorem :: PBOOLE:58
  X \ X = [[0]]I;

theorem :: PBOOLE:59
  X \ [[0]]I = X;

theorem :: PBOOLE:60
  [[0]]I \ X = [[0]]I;

theorem :: PBOOLE:61
  X \ (X \/ Y) = [[0]]I;

theorem :: PBOOLE:62
  X /\ (Y \ Z) = (X /\ Y) \ Z;

theorem :: PBOOLE:63
  (X \ Y) /\ Y = [[0]]I;

theorem :: PBOOLE:64
  X \ (Y \ Z) = (X \ Y) \/ X /\ Z;

theorem :: PBOOLE:65
  (X \ Y) \/ X /\ Y = X;

theorem :: PBOOLE:66
  X c= Y implies Y = X \/ (Y \ X);

theorem :: PBOOLE:67
  X \/ (Y \ X) = X \/ Y;

theorem :: PBOOLE:68
  X \ (X \ Y) = X /\ Y;

theorem :: PBOOLE:69
  X \ (Y /\ Z) = (X \ Y) \/ (X \ Z);

theorem :: PBOOLE:70
  X \ X /\ Y = X \ Y;

theorem :: PBOOLE:71
  X /\ Y = [[0]]I iff X \ Y = X;

theorem :: PBOOLE:72
  (X \/ Y) \ Z = (X \ Z) \/ (Y \ Z);

theorem :: PBOOLE:73
  (X \ Y) \ Z = X \ (Y \/ Z);

theorem :: PBOOLE:74
  (X /\ Y) \ Z = (X \ Z) /\ (Y \ Z);

theorem :: PBOOLE:75
  (X \/ Y) \ Y = X \ Y;

theorem :: PBOOLE:76
  X c= Y \/ Z implies X \ Y c= Z & X \ Z c= Y;

theorem :: PBOOLE:77
  (X \/ Y) \ (X /\ Y) = (X \ Y) \/ (Y \ X);

theorem :: PBOOLE:78
  (X \ Y) \ Y = X \ Y;

theorem :: PBOOLE:79
  X \ (Y \/ Z) = (X \ Y) /\ (X \ Z);

theorem :: PBOOLE:80
  X \ Y = Y \ X implies X = Y;

theorem :: PBOOLE:81
  X /\ (Y \ Z) = X /\ Y \ X /\ Z;

theorem :: PBOOLE:82
  X \ Y c= Z implies X c= Y \/ Z;

theorem :: PBOOLE:83
  X \ Y c= X \+\ Y;

theorem :: PBOOLE:84
  X \+\ [[0]]I = X;

theorem :: PBOOLE:85
  X \+\ X = [[0]]I;

theorem :: PBOOLE:86
  X \/ Y = (X \+\ Y) \/ X /\ Y;

theorem :: PBOOLE:87
  X \+\ Y = (X \/ Y) \ X /\ Y;

theorem :: PBOOLE:88
  (X \+\ Y) \ Z = (X \ (Y \/ Z)) \/ (Y \ (X \/ Z));

theorem :: PBOOLE:89
  X \ (Y \+\ Z) = X \ (Y \/ Z) \/ X /\ Y /\ Z;

theorem :: PBOOLE:90
  (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z);

theorem :: PBOOLE:91
  X \ Y c= Z & Y \ X c= Z implies X \+\ Y c= Z;

theorem :: PBOOLE:92
  X \/ Y = X \+\ (Y \ X);

theorem :: PBOOLE:93
  X /\ Y = X \+\ (X \ Y);

theorem :: PBOOLE:94
  X \ Y = X \+\ (X /\ Y);

theorem :: PBOOLE:95
  Y \ X = X \+\ (X \/ Y);

theorem :: PBOOLE:96
  X \/ Y = X \+\ Y \+\ X /\ Y;

theorem :: PBOOLE:97
  X /\ Y = X \+\ Y \+\ (X \/ Y);

begin :: Meeting and overlap(p?)ing

theorem :: PBOOLE:98
  X overlaps Y or X overlaps Z implies X overlaps Y \/ Z;

theorem :: PBOOLE:99
  X overlaps Y & Y c= Z implies X overlaps Z;

theorem :: PBOOLE:100
  X overlaps Y & X c= Z implies Z overlaps Y;

theorem :: PBOOLE:101
  X c= Y & Z c= V & X overlaps Z implies Y overlaps V;

theorem :: PBOOLE:102
  X overlaps Y /\ Z implies X overlaps Y & X overlaps Z;

theorem :: PBOOLE:103
  X overlaps Z & X c= V implies X overlaps Z /\ V;

theorem :: PBOOLE:104
  X overlaps Y \ Z implies X overlaps Y;

theorem :: PBOOLE:105
  Y does not overlap Z implies X /\ Y does not overlap X /\ Z;

theorem :: PBOOLE:106
  X overlaps Y \ Z implies Y overlaps X \ Z;

theorem :: PBOOLE:107
  X meets Y & Y c= Z implies X meets Z;

theorem :: PBOOLE:108
  Y misses X \ Y;

theorem :: PBOOLE:109
  X /\ Y misses X \ Y;

theorem :: PBOOLE:110
  X /\ Y misses X \+\ Y;

theorem :: PBOOLE:111
  X misses Y implies X /\ Y = [[0]]I;

theorem :: PBOOLE:112
  X <> [[0]]I implies X meets X;

theorem :: PBOOLE:113
  X c= Y & X c= Z & Y misses Z implies X = [[0]]I;

theorem :: PBOOLE:114
  Z \/ V = X \/ Y & X misses Z & Y misses V implies X = V & Y = Z;

theorem :: PBOOLE:115
  X misses Y implies X \ Y = X;

theorem :: PBOOLE:116
  X misses Y implies (X \/ Y) \ Y = X;

theorem :: PBOOLE:117
  X \ Y = X implies X misses Y;

theorem :: PBOOLE:118
  X \ Y misses Y \ X;

begin :: Roughly speaking

definition
  let I,X,Y;
  pred X [= Y means
:: PBOOLE:def 11

  for x st x in X holds x in Y;
  reflexivity;
end;

theorem :: PBOOLE:119
  X c= Y implies X [= Y;

theorem :: PBOOLE:120
  X [= Y & Y [= Z implies X [= Z;

begin :: Non empty set of sorts

theorem :: PBOOLE:121
  [[0]]{} in [[0]]{};

theorem :: PBOOLE:122
  for X being ManySortedSet of {} holds X = {};

reserve I for non empty set,
  x,X,Y for ManySortedSet of I;

theorem :: PBOOLE:123
  X overlaps Y implies X meets Y;

theorem :: PBOOLE:124
  not ex x st x in [[0]]I;

theorem :: PBOOLE:125
  x in X & x in Y implies X /\ Y <> [[0]]I;

theorem :: PBOOLE:126
  X does not overlap [[0]]I;

theorem :: PBOOLE:127
  X /\ Y = [[0]]I implies X does not overlap Y;

theorem :: PBOOLE:128
  X overlaps X implies X <> [[0]]I;

begin :: Empty and non-empty ManySortedSets

reserve I for set,
  x,X,Y,Z for ManySortedSet of I;

definition
  let I be set;
  let X be ManySortedSet of I;
  redefine attr X is empty-yielding means
:: PBOOLE:def 12

  for i st i in I holds X.i is
  empty;
  redefine attr X is non-empty means
:: PBOOLE:def 13

  for i st i in I holds X.i is non empty;
end;

registration
  let I be set;
  cluster empty-yielding for ManySortedSet of I;
  cluster non-empty for ManySortedSet of I;
end;

registration
  let I be non empty set;
  cluster non-empty -> non empty-yielding for ManySortedSet of I;
  cluster empty-yielding -> non non-empty for ManySortedSet of I;
end;

theorem :: PBOOLE:129
  X is empty-yielding iff X = [[0]]I;

theorem :: PBOOLE:130
  Y is empty-yielding & X c= Y implies X is empty-yielding;

theorem :: PBOOLE:131
  X is non-empty & X c= Y implies Y is non-empty;

theorem :: PBOOLE:132
  X is non-empty & X [= Y implies X c= Y;

theorem :: PBOOLE:133
  X is non-empty & X [= Y implies Y is non-empty;

reserve X for non-empty ManySortedSet of I;

theorem :: PBOOLE:134
  ex x st x in X;

theorem :: PBOOLE:135
  (for x holds x in X iff x in Y) implies X = Y;

theorem :: PBOOLE:136
  (for x holds x in X iff x in Y & x in Z) implies X = Y /\ Z;

begin :: Addenda

scheme :: PBOOLE:sch 3

  MSSEx { I() -> set, P[set,set] }: ex f being ManySortedSet of I() st for i
  st i in I() holds P[i,f.i]
provided
 for i st i in I() ex j st P[i,j];

scheme :: PBOOLE:sch 4

  MSSLambda { I() -> set, F(set) -> set }: ex f being ManySortedSet of I() st
  for i st i in I() holds f.i = F(i);

registration
  let I be set;
  cluster Function-yielding for ManySortedSet of I;
end;

definition
  let I be set;
  mode ManySortedFunction of I is Function-yielding ManySortedSet of I;
end;

theorem :: PBOOLE:137
  not ex M being non-empty ManySortedSet of I st {} in rng M;

definition
  let I be set;
  let M be ManySortedSet of I;
  mode Component of M is Element of rng M;
end;

theorem :: PBOOLE:138
  for I being non empty set for M being ManySortedSet of I, A being
  Component of M ex i st i in I & A = M.i;

theorem :: PBOOLE:139
  for M being ManySortedSet of I, i st i in I holds M.i is Component of M;

definition
  let I;
  let B be ManySortedSet of I;
  mode Element of B -> ManySortedSet of I means
:: PBOOLE:def 14
    for i st i in I holds it.i is
    Element of B.i;
end;

begin :: Many Sorted Functions

definition
  let I;
  let A be ManySortedSet of I, B be ManySortedSet of I;
  mode ManySortedFunction of A,B -> ManySortedSet of I means
:: PBOOLE:def 15
 for i st i in I holds it.i is Function of A.i, B.i;
end;

registration
  let I;
  let A be ManySortedSet of I, B be ManySortedSet of I;
  cluster ->Function-yielding for ManySortedFunction of A,B;
end;

registration
  let I be set;
  let J be non empty set;
  let O be Function of I,J;
  let F be ManySortedSet of J;
  cluster F*O -> total for I-defined Function;
end;

reserve D for non empty set,
  n for Nat;

scheme :: PBOOLE:sch 5

  LambdaDMS {D()->non empty set, F(set)->set}: ex X be ManySortedSet of D() st
  for d be Element of D() holds X.d = F(d);

registration
  let J be non empty set, B be non-empty ManySortedSet of J, j be Element of J;
  cluster B.j -> non empty;
end;

reserve X,Y for ManySortedSet of I;

definition
  let I, X,Y;
  func [|X,Y|] -> ManySortedSet of I means
:: PBOOLE:def 16
  for i st i in I holds it.i = [:X.i,Y.i:];
end;

definition
  let I, X, Y;
  func (Funcs) (X,Y) -> ManySortedSet of I means
:: PBOOLE:def 17
  for i be set st i in I holds it.i = Funcs(X.i,Y.i);
end;

definition
  let I be set, M be ManySortedSet of I;
  mode ManySortedSubset of M -> ManySortedSet of I means
:: PBOOLE:def 18

  it c= M;
end;

registration
  let I be set, M be non-empty ManySortedSet of I;
  cluster non-empty for ManySortedSubset of M;
end;

definition
  let F,G be Function-yielding Function;
  func G**F -> Function means
:: PBOOLE:def 19

  dom it = (dom F) /\ (dom G) &
  for i be set st i in dom it holds it.i = (G.i)*(F.i);
end;

registration
  let F,G be Function-yielding Function;
  cluster G**F -> Function-yielding;
end;

definition
  let I be set, A be ManySortedSet of I, F be ManySortedFunction of I;
  func F.:.:A -> ManySortedSet of I means
:: PBOOLE:def 20
  for i be set st i in I holds it.i = (F.i).:(A.i);
end;

registration
  let I;
  cluster [[0]]I -> empty-yielding;
end;

scheme :: PBOOLE:sch 6

  MSSExD { I() -> non empty set, P[set,set] }: ex f being ManySortedSet of I()
  st for i being Element of I() holds P[i,f.i]
provided
 for i being Element of I() ex j being set st P[i,j];

registration
  let A be non empty set;
  cluster non-empty -> non empty-yielding for ManySortedSet of A;
end;

registration
  let X be non empty set;
  cluster -> non empty for ManySortedSet of X;
end;

theorem :: PBOOLE:140
  for F, G, H be Function-yielding Function holds
  (H ** G) ** F = H ** (G ** F);

registration
 let I be set, f be non-empty ManySortedSet of I;
 cluster total for I-defined f-compatible Function;
end;

theorem :: PBOOLE:141
 for I being set, f being non-empty ManySortedSet of I
 for p being f-compatible I-defined Function
  ex s being f-compatible ManySortedSet of I st p c= s;

theorem :: PBOOLE:142
  for I,A be set
  for s,ss being ManySortedSet of I
  holds (ss +* s | A) | A = s | A;

registration
 let X be non empty set, Y be set;
 cluster X-valued for ManySortedSet of Y;
end;

theorem :: PBOOLE:143
  for I,Y being non empty set, M be Y-valued ManySortedSet of I,
     x be Element of I
  holds M.x = M/.x;

theorem :: PBOOLE:144
 for f being Function, M being ManySortedSet of I
   holds (f+*M)|I = M;

theorem :: PBOOLE:145
 for I being set, Y being non empty set
 for p being Y-valued I-defined Function
  ex s being Y-valued ManySortedSet of I st p c= s;

theorem :: PBOOLE:146
 X c= Y & Y c= X implies X = Y;

definition let I be non empty set, A,B be ManySortedSet of I;
 redefine pred A = B means
:: PBOOLE:def 21
  for i being Element of I holds A.i = B.i;
end;