:: Simple-named complex-valued nominative data -- definition and basic
:: operations
::  by Ievgen Ivanov , Mykola Nikitchenko , Andrii Kryvolap and Artur Korni{\l}owicz
::
:: Received August 30, 2017
:: Copyright (c) 2017-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 NOMIN_1, NUMBERS, SUBSET_1, XBOOLE_0, RELAT_1, FUNCT_1, FINSEQ_1,
      XXREAL_0, NAT_1, ARYTM_3, CARD_1, PARTFUN1, TARSKI, CARD_3, FUNCOP_1,
      ORDINAL4, ZFMISC_1, FINSET_1, ARYTM_1, FUNCT_4, ORDERS_5;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, ENUMSET1,
      RELAT_1, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, FUNCOP_1,
      TURING_1, XXREAL_0, XCMPLX_0, FUNCT_4, CARD_3, FINSEQ_4, FINSET_1;
 constructors PROB_1, FINSEQ_4, RELSET_1, FUNCT_6, TURING_1;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
      FINSET_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, CARD_1, RELSET_1, INT_1;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin :: Preliminaries

reserve a,a1,a2,v,v1,v2,x for object;
reserve V,A for set;
reserve m,n for Nat;
reserve S,S1,S2 for FinSequence;

theorem :: NOMIN_1:1
  for f being FinSequence st n in dom f holds (<*x*>^f).(n+1) = f.n;

theorem :: NOMIN_1:2
  for f being Function st dom f = NAT holds f|Seg(n) is FinSequence;

theorem :: NOMIN_1:3
  for f,g being FinSequence holds dom f c= dom g or dom g c= dom f;

registration
  let f,g be FinSequence;
  cluster f+*g -> FinSequence-like;
end;

registration let f1, f2 be Function;
  cluster f2 \/ (f1|(dom(f1)\dom(f2))) -> Function-like;
end;

definition
  let f,g be Function, x,y be object;
  pred f,x =~ g,y means
:: NOMIN_1:def 1
  (x in dom f iff y in dom g) & (x in dom f implies f.x = g.y);
end;

begin :: Definition of simple-named complex-valued nominative data

definition
  let V,A;
  mode NominativeSet of V,A is PartFunc of V,A;
end;

registration
  let V,A;
  cluster finite for NominativeSet of V,A;
end;

definition
  let V,A;
  mode TypeSSNominativeData of V,A is finite NominativeSet of V,A;
end;

definition
  let V,A;
  func NDSS(V,A) -> set equals
:: NOMIN_1:def 2
  the set of all d where d is TypeSSNominativeData of V,A;
end;

registration
  let V,A;
  cluster NDSS(V,A) -> non empty;
end;

theorem :: NOMIN_1:4
  x in NDSS(V,A) implies x is TypeSSNominativeData of V,A;

theorem :: NOMIN_1:5
  NDSS(V,A) c= PFuncs(V,A);

theorem :: NOMIN_1:6
  {} in NDSS(V,A);

theorem :: NOMIN_1:7
  for A, B being set st A c= B holds NDSS(V,A) c= NDSS(V,B);

theorem :: NOMIN_1:8
  for f,g being finite Function holds
  f tolerates g & f in NDSS(V,A) & g in NDSS(V,A) implies
  f \/ g in NDSS(V,A);

definition
  let V,A;
  func FNDSC(V,A) -> Function means
:: NOMIN_1:def 3
  dom it = NAT & it.0 = A &
  for n being Nat holds it.(n+1) = NDSS(V,A\/it.n);
end;

theorem :: NOMIN_1:9
  FNDSC(V,A).1 = NDSS(V,A);

theorem :: NOMIN_1:10
  FNDSC(V,A).2 = NDSS(V,A\/NDSS(V,A));

theorem :: NOMIN_1:11
  A c= Union FNDSC(V,A);

theorem :: NOMIN_1:12
  1 <= n implies {} in FNDSC(V,A).n;

registration
  let V,A,n;
  cluster FNDSC(V,A) | Seg(n) -> FinSequence-like;
end;

theorem :: NOMIN_1:13
  m <> 0 & m <= n implies FNDSC(V,A).m c= FNDSC(V,A).n;

definition
  let V,A;
  let S be FinSequence;
  pred S IsNDRankSeq V,A means
:: NOMIN_1:def 4
  S.1 = NDSS(V,A) &
  for n being Nat st n in dom S & n+1 in dom S holds S.(n+1) = NDSS(V,A\/S.n);
end;

theorem :: NOMIN_1:14
  S IsNDRankSeq V,A implies S <> {};

theorem :: NOMIN_1:15
  S IsNDRankSeq V,A & S1 c= S & S1 <> {} implies S1 IsNDRankSeq V,A;

theorem :: NOMIN_1:16
  S IsNDRankSeq V,A & n in dom S implies S|n IsNDRankSeq V,A;

theorem :: NOMIN_1:17
  S IsNDRankSeq V,A implies S ^ <* NDSS(V,A\/S.len S) *> IsNDRankSeq V,A;

theorem :: NOMIN_1:18
  1 <= n implies FNDSC(V,A) | Seg(n) IsNDRankSeq V,A;

theorem :: NOMIN_1:19
  S IsNDRankSeq V,A & n in dom S implies S.n = FNDSC(V,A).n;

theorem :: NOMIN_1:20
  S IsNDRankSeq V,A implies S = FNDSC(V,A) | dom S;

theorem :: NOMIN_1:21
  S1 IsNDRankSeq V,A & S2 IsNDRankSeq V,A implies S1 tolerates S2;

theorem :: NOMIN_1:22
  S1 IsNDRankSeq V,A & S2 IsNDRankSeq V,A implies S1 c= S2 or S2 c= S1;

theorem :: NOMIN_1:23
  S1 IsNDRankSeq V,A & S2 IsNDRankSeq V,A implies S1+*S2 = S1 or S1+*S2 = S2;

theorem :: NOMIN_1:24
  S1 IsNDRankSeq V,A & S2 IsNDRankSeq V,A implies S1+*S2 IsNDRankSeq V,A;

theorem :: NOMIN_1:25
  S IsNDRankSeq V,A & m <= n & n in dom S implies S.m c= S.n;

theorem :: NOMIN_1:26
  for F being FinSequence st F IsNDRankSeq V,A
   ex S being FinSequence st len S = 1 + len F & S IsNDRankSeq V,A &
    for n being Nat st n in dom S holds S.n = NDSS(V,A\/(<*A*>^F).n);

theorem :: NOMIN_1:27
  <*NDSS(V,A)*> IsNDRankSeq V,A;

theorem :: NOMIN_1:28
  <*NDSS(V,A),NDSS(V,A\/NDSS(V,A))*> IsNDRankSeq V,A;

theorem :: NOMIN_1:29
  <*NDSS(V,A),NDSS(V,A\/NDSS(V,A)),NDSS(V,A\/NDSS(V,A\/NDSS(V,A)))*>
   IsNDRankSeq V,A;

definition
  let V,A;
  mode NonatomicND of V,A -> Function means
:: NOMIN_1:def 5
  ex S being FinSequence st S IsNDRankSeq V,A & it in Union S;
  sethood;
end;

reserve D,D1,D2 for NonatomicND of V,A;

theorem :: NOMIN_1:30
  {} is NonatomicND of V,A;

theorem :: NOMIN_1:31
  D in Union FNDSC(V,A);

theorem :: NOMIN_1:32
  for d being set st d c= D holds d is NonatomicND of V,A;

theorem :: NOMIN_1:33
  ex n being Nat st D is TypeSSNominativeData of V,A\/FNDSC(V,A).n;

registration
  let V,A;
  cluster -> finite for NonatomicND of V,A;
end;

theorem :: NOMIN_1:34
  D1 tolerates D2 & S IsNDRankSeq V,A & D1 in S.m & D2 in S.m
  implies D1 \/ D2 in S.m;

theorem :: NOMIN_1:35
  D1 tolerates D2 & S2 IsNDRankSeq V,A & S1 c= S2 &
   D1 in Union S1 & D2 in Union S2
  implies D1 \/ D2 in Union S2;

theorem :: NOMIN_1:36
  D1 tolerates D2 implies D1 \/ D2 is NonatomicND of V,A;

theorem :: NOMIN_1:37
  D1 tolerates D2 implies D1 +* D2 is NonatomicND of V,A;

definition
  let V,A;
  mode TypeSCNominativeData of V,A -> set means
:: NOMIN_1:def 6
  it in A or it is NonatomicND of V,A;
  sethood;
end;

registration
  let V,A;
  cluster Function-like Relation-like for TypeSCNominativeData of V,A;
end;

definition
  let V,A;
  redefine mode NonatomicND of V,A
    -> Function-like Relation-like TypeSCNominativeData of V,A;
end;

definition
  let V,A;
  func ND(V,A) -> set equals
:: NOMIN_1:def 7
  the set of all D where D is TypeSCNominativeData of V,A;
end;

registration
  let V,A;
  cluster ND(V,A) -> non empty;
end;

theorem :: NOMIN_1:38
  {} in ND(V,A);

theorem :: NOMIN_1:39
  x in ND(V,A) implies x is TypeSCNominativeData of V,A;

theorem :: NOMIN_1:40
  ND(V,A) = Union FNDSC(V,A);

theorem :: NOMIN_1:41
  D in ND(V,A);

theorem :: NOMIN_1:42
  not D in A implies D in ND(V,A) \ A;

theorem :: NOMIN_1:43
  x in ND(V,A) \ A implies x is NonatomicND of V,A;

theorem :: NOMIN_1:44
  for D being TypeSCNominativeData of V,A holds D in Union FNDSC(V,A);

begin :: Examples of simple-named complex-valued nominative data

::$N [v->a]
definition
  let v,a;
  func ND_ex_1(v,a) -> set equals
:: NOMIN_1:def 8
  v.-->a;
end;

registration
  let v,a;
  cluster ND_ex_1(v,a) -> Function-like Relation-like;
end;

theorem :: NOMIN_1:45
  v in V & a in A implies ND_ex_1(v,a) in NDSS(V,A);

theorem :: NOMIN_1:46
  v in V & a in A implies ND_ex_1(v,a) is NonatomicND of V,A;

definition
  let V,A be non empty set;
  let v be Element of V;
  let a be Element of A;
  redefine func ND_ex_1(v,a) -> NonatomicND of V,A;
end;

theorem :: NOMIN_1:47
  v in V & a in A implies ND_ex_1(v,a) is TypeSCNominativeData of V,A;

::$N [v->[v1->a]]
definition
  let v,v1,a1;
  func ND_ex_2(v,v1,a1) -> set equals
:: NOMIN_1:def 9
  v.-->(v1.-->a1);
end;

registration
  let v,v1,a1;
  cluster ND_ex_2(v,v1,a1) -> Function-like Relation-like;
end;

theorem :: NOMIN_1:48
  {v,v1} c= V & a1 in A implies ND_ex_2(v,v1,a1) in NDSS(V,A\/NDSS(V,A));

theorem :: NOMIN_1:49
  {v,v1} c= V & a1 in A implies ND_ex_2(v,v1,a1) is NonatomicND of V,A;

definition
  let V,A be non empty set;
  let v,v1 be Element of V;
  let a be Element of A;
  redefine func ND_ex_2(v,v1,a) -> NonatomicND of V,A;
end;

theorem :: NOMIN_1:50
  {v,v1} c= V & a1 in A implies
  ND_ex_2(v,v1,a1) is TypeSCNominativeData of V,A;

::$N [v->a,v1->a1]
definition
  let v,v1,a,a1;
  func ND_ex_3(v,v1,a,a1) -> set equals
:: NOMIN_1:def 10
  (v,v1)-->(a,a1);
end;

registration
  let v,v1,a,a1;
  cluster ND_ex_3(v,v1,a,a1) -> Function-like Relation-like;
end;

theorem :: NOMIN_1:51
  {v,v1} c= V & {a,a1} c= A implies ND_ex_3(v,v1,a,a1) in NDSS(V,A);

theorem :: NOMIN_1:52
  {v,v1} c= V & {a,a1} c= A implies
  ND_ex_3(v,v1,a,a1) is NonatomicND of V,A;

definition
  let V,A be non empty set;
  let v,v1 be Element of V;
  let a,a1 be Element of A;
  redefine func ND_ex_3(v,v1,a,a1) -> NonatomicND of V,A;
end;

theorem :: NOMIN_1:53
  {v,v1} c= V & {a,a1} c= A implies
  ND_ex_3(v,v1,a,a1) is TypeSCNominativeData of V,A;

::$N [v->a,v1->[v2->a1]]
definition
  let v,v1,v2,a,a1;
  func ND_ex_4(v,v1,v2,a,a1) -> set equals
:: NOMIN_1:def 11
  (v,v1)-->(a,v2.-->a1);
end;

registration
  let v,v1,v2,a,a1;
  cluster ND_ex_4(v,v1,v2,a,a1) -> Function-like Relation-like;
end;

theorem :: NOMIN_1:54
  {v,v1,v2} c= V & {a,a1} c= A implies
  ND_ex_4(v,v1,v2,a,a1) in NDSS(V,A\/NDSS(V,A));

theorem :: NOMIN_1:55
  {v,v1,v2} c= V & {a,a1} c= A implies
  ND_ex_4(v,v1,v2,a,a1) is NonatomicND of V,A;

definition
  let V,A be non empty set;
  let v,v1,v2 be Element of V;
  let a,a1 be Element of A;
  redefine func ND_ex_4(v,v1,v2,a,a1) -> NonatomicND of V,A;
end;

theorem :: NOMIN_1:56
  {v,v1,v2} c= V & {a,a1} c= A implies
  ND_ex_4(v,v1,v2,a,a1) is TypeSCNominativeData of V,A;

theorem :: NOMIN_1:57
  <*x*> is NonatomicND of {1},{x};

begin :: Operations on simple-named complex-valued nominative data

definition
  let V,A,v,D such that
 v in dom D;
  func denaming(v,D) -> TypeSCNominativeData of V,A equals
:: NOMIN_1:def 12
  D.v;
end;

definition
  let V,A;
  let v,D be object;
  assume
 D is TypeSCNominativeData of V,A;
  assume
 v in V;
  func naming(V,A,v,D) -> NonatomicND of V,A equals
:: NOMIN_1:def 13
  v .--> D;
end;

definition
  let V,A;
  let a be object;
  let f be V-valued FinSequence;
  assume
 len f > 0;
  func namingSeq(V,A,f,a) -> FinSequence means
:: NOMIN_1:def 14
  len it = len f & it.1 = naming(V,A,f.len f,a) &
   for n being Nat st 1 <= n < len it holds
    it.(n+1) = naming(V,A,f.(len f-n),it.n);
end;

theorem :: NOMIN_1:58
  for f being V-valued FinSequence holds
  1 <= n <= len f implies
  namingSeq(V,A,f,a).n is NonatomicND of V,A;

definition
  let V,A;
  let f be V-valued FinSequence;
  let a be object;
  func naming(V,A,f,a) -> set equals
:: NOMIN_1:def 15
  namingSeq(V,A,f,a).len(namingSeq(V,A,f,a));
end;

theorem :: NOMIN_1:59
  for f being V-valued FinSequence st len f > 0
  holds naming(V,A,f,a) is NonatomicND of V,A;

theorem :: NOMIN_1:60
  for V being non empty set
  for v being Element of V holds
  naming(V,A,<*v*>,a) = naming(V,A,v,a);

theorem :: NOMIN_1:61
  for V being non empty set
  for v1,v2 being Element of V st a is TypeSCNominativeData of V,A holds
  naming(V,A,<*v1,v2*>,a) = v1.-->(v2.-->a);

theorem :: NOMIN_1:62
  for D being TypeSCNominativeData of V,A holds
  v in V implies denaming(v,naming(V,A,v,D)) = D;

theorem :: NOMIN_1:63
  v in dom D implies naming(V,A,v,denaming(v,D)) = v .--> D.v;

definition
  let V,A;
  let d1,d2 be object such that
 d1 is TypeSCNominativeData of V,A and
 d2 is TypeSCNominativeData of V,A;
  func global_overlapping(V,A,d1,d2) -> TypeSCNominativeData of V,A means
:: NOMIN_1:def 16

  ex f1,f2 being Function st f1 = d1 & f2 = d2 &
  it = f2 \/ (f1|(dom(f1)\dom(f2))) if not d1 in A & not d2 in A
  otherwise it = d2;
end;

definition
  let V,A;
  let d1,d2,v be object;
  func local_overlapping(V,A,d1,d2,v) -> TypeSCNominativeData of V,A equals
:: NOMIN_1:def 17
  global_overlapping(V,A,d1,naming(V,A,v,d2));
end;

theorem :: NOMIN_1:64
  not D1 in A & not D2 in A implies
  global_overlapping(V,A,D1,D2) = D2 \/ (D1|(dom(D1)\dom(D2)));

theorem :: NOMIN_1:65
  not D1 in A & not D2 in A & dom D1 c= dom D2 implies
  global_overlapping(V,A,D1,D2) = D2;

theorem :: NOMIN_1:66
  global_overlapping(V,A,D,D) = D;

theorem :: NOMIN_1:67
  v in V & not v.-->a1 in A & not v.-->a2 in A &
  a1 is TypeSCNominativeData of V,A & a2 is TypeSCNominativeData of V,A
  implies
  global_overlapping(V,A,v.-->a1,v.-->a2) = v.-->a2;

theorem :: NOMIN_1:68
  {v1,v2} c= V & v1 <> v2 & not v1.-->a1 in A & not v2.-->a2 in A &
  a1 is TypeSCNominativeData of V,A & a2 is TypeSCNominativeData of V,A
  implies
  global_overlapping(V,A,v1.-->a1,v2.-->a2) = (v2,v1)-->(a2,a1);

theorem :: NOMIN_1:69
  {v,v1,v2} c= V & v <> v1 & a2 in A &
  not v1.-->a1 in A & not v.-->(v2.-->a2) in A &
  a1 is TypeSCNominativeData of V,A implies
  local_overlapping(V,A,v1.-->a1,v2.-->a2,v) = (v,v1)-->(v2.-->a2,a1);

definition
  let V,A,v;
  func denaming(V,A,v) -> PartFunc of ND(V,A),ND(V,A) means
:: NOMIN_1:def 18
  dom it = {d where d is NonatomicND of V,A: v in dom d} &
  for D being NonatomicND of V,A st D in dom it holds it.D = denaming(v,D);
end;

definition
  let V,A,v;
  func naming(V,A,v) -> Function of ND(V,A),ND(V,A) means
:: NOMIN_1:def 19
  for D being TypeSCNominativeData of V,A holds it.D = naming(V,A,v,D);
end;

definition
  let V,A,v;
  func local_overlapping(V,A,v) -> PartFunc of [:ND(V,A),ND(V,A):],ND(V,A)
   means
:: NOMIN_1:def 20
  dom it = [: ND(V,A) \ A , ND(V,A) :] &
  for d1 being NonatomicND of V,A
   for d2 being object st not d1 in A & d2 in ND(V,A) holds
    it. [d1,d2] = local_overlapping(V,A,d1,d2,v);
end;