:: On Multiset Ordering
::  by Grzegorz Bancerek
:: 
:: Received December 31, 2015
:: Copyright (c) 2015-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 TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELAT_2, FINSET_1, ARYTM_1,
      ARYTM_3, FUNCT_1, PARTFUN1, BINOP_1, XXREAL_0, VALUED_0, NUMBERS, CARD_1,
      MESFUNC1, STRUCT_0, ALGSTR_0, MONOID_1, ORDERS_2, PRE_POLY, BAGORD_2,
      ZFMISC_1, NAT_1, FUNCOP_1, ORDERS_1, REWRITE1, FINSEQ_1, ORDINAL4,
      GROEB_1, CARD_3, INTERVA1, MIDSP_1, GRAPH_2, MCART_1, BAGORDER;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1, RELAT_2,
      ORDINAL1, RELSET_1, NECKLACE, FUNCT_1, PARTFUN1, BINOP_1, CARD_1,
      FINSEQ_1, FINSEQ_2, FINSET_1, VALUED_0, NUMBERS, FUNCT_2, XXREAL_0,
      XCMPLX_0, NAT_1, NAT_D, REWRITE1, GRAPH_2, STRUCT_0, ALGSTR_0, MONOID_1,
      ORDERS_2, WAYBEL_4, PRE_POLY, FINSEQ_6;
 constructors DOMAIN_1, RELSET_1, NECKLACE, BINOP_2, WAYBEL_4, REWRITE1,
      GRAPH_2, NAT_D, MONOID_1, FINSEQ_6, PRE_POLY;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, ORDINAL1, XREAL_0, VALUED_0,
      STRUCT_0, ORDERS_2, MONOID_0, CARD_1, PRE_POLY, FINSEQ_1, FINSET_1,
      REWRITE1, NAT_1, RELAT_1, XTUPLE_0, FUNCT_2;
 requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;


begin

theorem :: BAGORD_2:1
  for m,n being Nat holds n = (m-'(m-'n))+(n-'m);

theorem :: BAGORD_2:2
  for n,m being Nat holds m-'n >= m-n;

theorem :: BAGORD_2:3
  for m,n,x,y being Nat st n = (m-'x)+y holds m-'n <= x & n-'m <= y;

theorem :: BAGORD_2:4
  for m,n,x,y being Nat st x <= m & n = (m-'x)+y holds x-'(m-'n) = y-'(n-'m);

theorem :: BAGORD_2:5
  for k,x1,x2,y1,y2 being Nat st x2 <= k & x1 <= (k-'x2)+y2
  holds x2+(x1-'y2) <= k &
  (((k-'x2)+y2)-'x1)+y1 = (k-'(x2+(x1-'y2)))+((y2-'x1)+y1);

::$CT

reserve a,b for object, I,J for set;

registration
  cluster asymmetric transitive non empty for RelStr;
end;

registration
  let I;
  cluster asymmetric transitive for Relation of I;
end;

registration
  let R be asymmetric RelStr;
  cluster the InternalRel of R -> asymmetric;
end;

registration
  let I;
  let p,q be I-valued FinSequence;
  cluster p^q -> I-valued;
end;

theorem :: BAGORD_2:7
  for p,q being FinSequence st p^q is I-valued
  holds p is I-valued & q is I-valued;

registration
  let I;
  let f be I-valued FinSequence;
  let n be Nat;
  cluster f|n -> I-valued;
end;

theorem :: BAGORD_2:8
  for p being FinSequence st a in rng p
  ex q,r being FinSequence st p = q^<*a*>^r;

theorem :: BAGORD_2:9
  for p,q being FinSequence holds p c< q iff len p < len q &
  for i being Nat st i in dom p holds p.i = q.i;

theorem :: BAGORD_2:10
  for p,q,r being FinSequence holds r^p c< r^q iff p c< q;

definition
  let R be asymmetric non empty RelStr;
  let x,y be Element of R;
  redefine pred x <= y;
  asymmetry;
end;

theorem :: BAGORD_2:11
  for R being asymmetric non empty RelStr
  for x,y being Element of R holds x <= y iff x < y;

begin

definition
  let I;
  mode multiset of I is Element of finite-MultiSet_over I;
end;

registration
  let I;
  cluster -> I-defined natural-valued for multiset of I;
end;

registration
  let I;
  cluster -> total for multiset of I;
end;

definition
  let m be natural-valued Function;
  redefine func support m equals
:: BAGORD_2:def 1
  m"(NAT\{0});
end;

registration
  let I;
  cluster -> finite-support for multiset of I;
end;

theorem :: BAGORD_2:12
  a is multiset of I iff a is bag of I;

theorem :: BAGORD_2:13
  1.finite-MultiSet_over I = EmptyBag I;

definition
  let R be RelStr;
  let x,y be Element of R;
  pred x ## y means
:: BAGORD_2:def 2
not x <= y & not y <= x;
  symmetry;
end;

definition
  struct(multMagma,RelStr) RelMultMagma (#
    carrier -> set,
    multF -> BinOp of the carrier,
    InternalRel -> Relation of the carrier
  #);
end;

definition
  struct(multLoopStr,RelStr) RelMonoid (#
    carrier -> set,
    multF -> BinOp of the carrier,
    OneF -> Element of the carrier,
    InternalRel -> Relation of the carrier
  #);
end;

definition
  let M be multLoopStr;
  mode RelExtension of M -> RelMonoid means
:: BAGORD_2:def 3
  the multLoopStr of it = the multLoopStr of M;
end;

registration
  let M be non empty multLoopStr;
  cluster -> non empty for RelExtension of M;
end;

registration
  let M be multLoopStr;
  cluster strict for RelExtension of M;
end;

theorem :: BAGORD_2:14
  for N being multLoopStr, M being RelExtension of N holds
  a is Element of M iff a is Element of N;

theorem :: BAGORD_2:15
  for N being multLoopStr, M being RelExtension of N holds 1.N = 1.M;

registration
  let I;
  let M be RelExtension of finite-MultiSet_over I;
  cluster -> Function-like Relation-like for Element of M;
end;

registration
  let I;
  let M be RelExtension of finite-MultiSet_over I;
  cluster -> I-defined natural-valued finite-support for Element of M;
end;

registration
  let I;
  let M be RelExtension of finite-MultiSet_over I;
  cluster -> total for Element of M;
end;

theorem :: BAGORD_2:16
  for M being RelExtension of finite-MultiSet_over I holds
  the carrier of M = Bags I;

scheme :: BAGORD_2:sch 1
 RelEx{M() -> non empty multLoopStr, R[object,object]}:
  ex N being strict RelExtension of M() st
  for x,y being Element of N holds x <= y iff R[x,y];

theorem :: BAGORD_2:17
  for N being multLoopStr, M1,M2 being strict RelExtension of N
  st for m,n being Element of M1 for x,y being Element of M2 st m = x & n = y
     holds m <= n iff x <= y
  holds M1 = M2;

begin

definition
  let R be non empty RelStr;
  func DershowitzMannaOrder R -> strict RelExtension of
    finite-MultiSet_over the carrier of R means
:: BAGORD_2:def 4
  for m,n being Element of it holds m <= n iff ex x,y being Element of it st
  1.it <> x divides n & m = (n -' x) + y &
  for b being Element of R st y.b > 0
  ex a being Element of R st x.a > 0 & b <= a;
end;

theorem :: BAGORD_2:18
  for m,n being bag of I holds n = (m-'(m-'n))+(n-'m);

theorem :: BAGORD_2:19
  for m,n,x,y being bag of I st n = (m-'x)+y holds m-'n divides x &
  n-'m divides y;

theorem :: BAGORD_2:20
  for m,n,x,y being bag of I st x divides m & n = (m-'x)+y holds
  x-'(m-'n) = y-'(n-'m);

theorem :: BAGORD_2:21
  for m,x,y being bag of I st x divides m & x <> y holds m <> (m-'x)+y;

theorem :: BAGORD_2:22
  for I being non empty set, R being Relation of I
  for r being RedSequence of R
  st len r > 1 holds r.len r in I;

theorem :: BAGORD_2:23
  for R being asymmetric transitive Relation of I
  for r being RedSequence of R holds r is one-to-one;

theorem :: BAGORD_2:24
  for R being asymmetric transitive non empty RelStr
  for X being set st X is finite & ex x being Element of R st x in X
  ex x being Element of R st x is_maximal_in X;

theorem :: BAGORD_2:25
  for m,n being bag of I holds m-'n divides m;

registration
  let I;
  cluster -> Function-like Relation-like for Element of Bags I;
end;

theorem :: BAGORD_2:26
  for m,n being bag of I holds
  m-'n <> EmptyBag I or m = n or n-'m <> EmptyBag I;

definition
  let R being asymmetric transitive non empty RelStr;
  redefine func DershowitzMannaOrder R means
:: BAGORD_2:def 5
  for m,n being Element of it holds m <= n iff m <> n &
  for a being Element of R st m.a > n.a
  ex b being Element of R st a <= b & m.b < n.b;
end;

theorem :: BAGORD_2:27
  for k,x1,x2,y1,y2 being bag of I st x2 divides k & x1 divides (k-'x2)+y2
  holds x2+(x1-'y2) divides k &
  (((k-'x2)+y2)-'x1)+y1 = (k-'(x2+(x1-'y2)))+((y2-'x1)+y1);

registration
  let R be asymmetric transitive non empty RelStr;
  cluster DershowitzMannaOrder R -> asymmetric transitive;
end;

definition
  let I;
  func DivOrder I -> Relation of Bags I means
:: BAGORD_2:def 6
  for b1,b2 being bag of I holds [b1,b2] in it iff b1 <> b2 & b1 divides b2;
end;

theorem :: BAGORD_2:28
  for a,b,c being bag of I st a divides b divides c holds a divides c;

registration
  let I;
  cluster DivOrder I -> asymmetric transitive;
end;

theorem :: BAGORD_2:29
  for R being asymmetric transitive non empty RelStr holds
  DivOrder the carrier of R c= the InternalRel of DershowitzMannaOrder R;

theorem :: BAGORD_2:30
  for R being asymmetric transitive non empty RelStr
  st the InternalRel of R is empty
  holds the InternalRel of DershowitzMannaOrder R = DivOrder the carrier of R;

theorem :: BAGORD_2:31
  for R1,R2 being asymmetric transitive non empty RelStr
  st the carrier of R1 = the carrier of R2 &
  the InternalRel of R1 c= the InternalRel of R2
  holds the InternalRel of DershowitzMannaOrder R1
  c= the InternalRel of DershowitzMannaOrder R2;

begin

definition
  let I;
  let f be (Bags I)-valued FinSequence;
  func Sum f -> bag of I means
:: BAGORD_2:def 7
    ex F being Function of NAT, Bags I st
       it = F.len f &
       F.0 = EmptyBag I &
       for i being Nat
       for b being bag of I
           st i < len f & b = f.(i + 1)
        holds F.(i + 1) = F.i + b;
end;

theorem :: BAGORD_2:32
  Sum (<*>Bags I) = EmptyBag I;

registration
  let I;
  let b be bag of I;
  cluster <*b*> -> Bags I-valued for FinSequence;
end;

theorem :: BAGORD_2:33
  for p being Bags I-valued FinSequence, b being bag of I holds
  Sum (p^<*b*>) = Sum p + b;

reserve b for bag of I;

theorem :: BAGORD_2:34
  Sum <*b*> = b;

theorem :: BAGORD_2:35
  for p,q being Bags I-valued FinSequence holds
  Sum (p^q) = Sum p + Sum q;

theorem :: BAGORD_2:36
  for p being Bags I-valued FinSequence holds Sum (<*b*>^p) = b + Sum p;

theorem :: BAGORD_2:37
  for p being Bags I-valued FinSequence st b in rng p holds b divides Sum p;

theorem :: BAGORD_2:38
  for p being Bags I-valued FinSequence, i being object st i in support Sum p
  ex b st b in rng p & i in support b;

definition
  let I,b;
  mode partition of b -> Bags I-valued FinSequence means
:: BAGORD_2:def 8
  b = Sum it;
end;

definition
  let I,b;
  redefine func <*b*> -> partition of b;
end;

definition
  let R be RelStr;
  let M be RelExtension of finite-MultiSet_over the carrier of R;
  let b be Element of M;
  let p be partition of b;
  attr p is co-ordered means
:: BAGORD_2:def 9
  for i being Nat st i in dom p & i+1 in dom p
  for b1,b2 being Element of M st b1 = p.i & b2 = p.(i+1) holds b2 <= b1;
end;

definition
  let R be non empty RelStr;
  let b be bag of the carrier of R;
  let p be partition of b;
  attr p is ordered means
:: BAGORD_2:def 10
  (for m being bag of the carrier of R st m in rng p
  for x being Element of R st m.x > 0 holds m.x = b.x) &
  (for m being bag of the carrier of R st m in rng p
  for x,y being Element of R st m.x > 0 & m.y > 0 & x <> y
  holds x ## y) &
  (for m being bag of the carrier of R st m in rng p
  holds m <> EmptyBag the carrier of R) &
  (for i being Nat st i in dom p & i+1 in dom p
  for x being Element of R st (p/.(i+1)).x > 0
  ex y being Element of R st (p/.i).y > 0 & x <= y);
end;

reserve R for asymmetric transitive non empty RelStr,
  a,b,c for bag of the carrier of R,
  x,y,z for Element of R;

theorem :: BAGORD_2:39
  <*a*> is ordered iff a <> EmptyBag the carrier of R &
  for x,y st a.x > 0 & a.y > 0 & x <> y holds x ## y;

theorem :: BAGORD_2:40
  for p being Bags I-valued FinSequence
  for a,b being bag of I holds
  <*a*>^p is partition of b iff a divides b & p is partition of b-'a;

reserve p for partition of b-'a, q for partition of b;

theorem :: BAGORD_2:41
  q = <*a*>^p & q is ordered implies p is ordered;

definition
  let I;
  let m be bag of I;
  let J be set;
  func m|J -> bag of I means
:: BAGORD_2:def 11
  for i being object st i in I holds (i in J implies it.i = m.i) &
  (not i in J implies it.i = 0);
end;

reserve J for set, m for bag of I;

theorem :: BAGORD_2:42
  support (m|J) = J /\ support m;

theorem :: BAGORD_2:43
  (m|J)+(m|(I\J)) = m;

theorem :: BAGORD_2:44
  m|J divides m;

theorem :: BAGORD_2:45
  support m c= J implies m|J = m;

theorem :: BAGORD_2:46
  support(m-'(m|J)) = (support m)\J;

theorem :: BAGORD_2:47
  q is ordered & q = <*a*>^p & a.x > 0 implies a.x = b.x;

theorem :: BAGORD_2:48
  q is ordered & q = <*a*>^p & a.x > 0 & a.y > 0 & x <> y implies x ## y;

theorem :: BAGORD_2:49
  q is ordered & q = <*a*>^p implies a <> EmptyBag the carrier of R;

theorem :: BAGORD_2:50
  for c being bag of the carrier of R,
  r being Bags the carrier of R-valued FinSequence
  st q is ordered & q = <*a,c*>^r & c.y > 0
  ex x st a.x > 0 & y <= x;

theorem :: BAGORD_2:51
  x in I & (for y st y in I & y <> x holds x ## y) implies x is_maximal_in I;

theorem :: BAGORD_2:52
  q is ordered & q = <*a*>^p & c in rng p & c.x > 0 implies
  ex y st a.y > 0 & x <= y;

theorem :: BAGORD_2:53
  q is ordered & q = <*a*>^p implies (x is_maximal_in support b iff a.x > 0);

theorem :: BAGORD_2:54
  q is ordered & q = <*a*>^p implies a = b|{x:x is_maximal_in support b};

theorem :: BAGORD_2:55
  for p being Bags I-valued FinSequence st Sum p = EmptyBag I &
  for a being bag of I st a in rng p holds a <> EmptyBag I
  holds p = {};

theorem :: BAGORD_2:56
  for a,b being bag of I st a <> EmptyBag I holds a+b <> EmptyBag I;

theorem :: BAGORD_2:57
  for p,q being partition of b st p is ordered & q is ordered holds p = q;

definition
  let I;
  let a,b be bag of I;
  redefine func [a,b] -> Element of [:Bags I,Bags I:];
end;

theorem :: BAGORD_2:58
  a <> EmptyBag the carrier of R implies {x:x is_maximal_in support a} <> {};

definition
  let R,b;
  func OrderedPartition b -> Bags the carrier of R-valued FinSequence means
:: BAGORD_2:def 12

  ex F,G being Function of NAT, Bags the carrier of R st F.0 = b &
  G.0 = EmptyBag the carrier of R &
  (for i being Nat holds G.(i+1) = (F.i)|{x:x is_maximal_in support (F.i)} &
  F.(i+1) = (F.i)-'(G.(i+1))) &
  ex i being Nat st F.i = EmptyBag the carrier of R & it = G|Seg i &
  for j being Nat st j < i holds F.j <> EmptyBag the carrier of R;
end;

definition
  let R,b;
  redefine func OrderedPartition b -> partition of b;
end;

registration
  let R,b;
  cluster OrderedPartition b -> ordered for partition of b;
end;

theorem :: BAGORD_2:59
  b = EmptyBag the carrier of R iff OrderedPartition b = {};

definition
  let R;
  func PrecM R -> strict RelExtension of finite-MultiSet_over the carrier of R
  means
:: BAGORD_2:def 13
  for m,n being Element of it holds m <= n iff m <> n &
  for x st m.x > 0 holds m.x < n.x or ex y st n.y > 0 & x <= y;
end;

registration
  let R;
  cluster PrecM R -> asymmetric transitive;
end;

definition
  let I;
  let R be Relation of I,I;
  func LexOrder(I,R) -> Relation of I* means
:: BAGORD_2:def 14
  for p,q being I-valued FinSequence holds [p,q] in it iff p c< q or
  ex k being Nat st k in dom p & k in dom q & [p.k,q.k] in R &
  for n being Nat st 1 <= n < k holds p.n = q.n;
end;

registration
  let I;
  let R be transitive Relation of I;
  cluster LexOrder(I,R) -> transitive;
end;

registration
  let I;
  let R be asymmetric Relation of I;
  cluster LexOrder(I,R) -> asymmetric;
end;

theorem :: BAGORD_2:60
  for R being asymmetric Relation of I
  for p,q,r being I-valued FinSequence holds
  [p,q] in LexOrder(I,R) iff [r^p,r^q] in LexOrder(I,R);

definition
  let R;
  func PrecPrecM R -> strict RelExtension of
  finite-MultiSet_over the carrier of R means
:: BAGORD_2:def 15
  for m,n being Element of it holds m <= n iff
  [OrderedPartition m, OrderedPartition n] in
  LexOrder(the carrier of PrecM R, the InternalRel of PrecM R);
end;

registration
  let R;
  cluster PrecPrecM R -> asymmetric transitive;
end;

theorem :: BAGORD_2:61
  for a,b being Element of DershowitzMannaOrder R st a <= b
  holds b <> EmptyBag the carrier of R;

theorem :: BAGORD_2:62
  for a,b,c,d being Element of DershowitzMannaOrder R
  for e being bag of the carrier of R st a <= b & e divides a & e divides b
  holds c = a-'e & d = b-'e implies c <= d;

theorem :: BAGORD_2:63
  for p being Bags I-valued FinSequence, x being object
  st x in I & (Sum p).x > 0
  ex i being Nat st i in dom p & (p/.i).x > 0;

theorem :: BAGORD_2:64
  q is ordered & (q/.1).x = 0 & b.x > 0 implies
  ex y st (q/.1).y > 0 & x <= y;