:: Sorting Operators for Finite Sequences
::  by Yatsuka Nakamura
::
:: Received October 17, 2003
:: Copyright (c) 2003-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 NUMBERS, FINSEQ_1, CARD_1, XXREAL_0, RELAT_1, REAL_1, FUNCT_1,
      ARYTM_3, FUNCOP_1, ARYTM_1, RFINSEQ, CLASSES1, FUNCT_2, XBOOLE_0,
      VALUED_0, ORDINAL4, NAT_1, RFINSEQ2;
 notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XXREAL_0,
      RELAT_1, XCMPLX_0, XREAL_0, FUNCT_1, FUNCT_2, FINSEQ_1, REAL_1, NAT_1,
      RVSUM_1, FUNCOP_1, CLASSES1, RFINSEQ, INTEGRA2;
 constructors FUNCOP_1, REAL_1, NAT_1, BINOP_2, SEQM_3, RFINSEQ, INTEGRA2,
      RVSUM_1, CLASSES1, RELSET_1;
 registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, XXREAL_0, NAT_1, MEMBERED,
      FINSEQ_1, VALUED_0, FINSET_1, CARD_1, XREAL_0, ORDINAL1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin

reserve n,m for Nat;

definition
  let f be FinSequence of REAL;
  func max_p f -> Nat means
:: RFINSEQ2:def 1

  (len f=0 implies it=0) &
  (len f>0 implies it in dom f &
   (for i being Nat, r1,r2 being Real
     st i in dom f & r1=f.i & r2=f.it holds r1<=r2) &
    for j being Nat st j in dom f & f.j=f.it holds it<=j );
end;

definition
  let f be FinSequence of REAL;
  func min_p f -> Nat means
:: RFINSEQ2:def 2

  (len f=0 implies it=0) & (len f>
  0 implies it in dom f &
  (for i being Nat,r1,r2 being Real st i in
dom f & r1=f.i & r2=f.it holds r1>=r2) & for j being Nat st j in dom
  f & f.j=f.it holds it<=j );
end;

definition
  let f be FinSequence of REAL;
  func max f -> Real equals
:: RFINSEQ2:def 3
  f.(max_p f);
  func min f -> Real equals
:: RFINSEQ2:def 4
  f.(min_p f);
end;

theorem :: RFINSEQ2:1
  for f being FinSequence of REAL,i being Nat st 1<=i &
  i<=len f holds f.i<=f.(max_p f) & f.i<=max f;

theorem :: RFINSEQ2:2
  for f being FinSequence of REAL,i being Nat st 1<=i &
  i<=len f holds f.i>=f.(min_p f) & f.i>=min f;

theorem :: RFINSEQ2:3
  for f being FinSequence of REAL,r being Real st f=<*r*> holds max_p f=
  1 & max f=r;

theorem :: RFINSEQ2:4
  for f being FinSequence of REAL,r being Real st f=<*r*> holds min_p f=
  1 & min f=r;

theorem :: RFINSEQ2:5
  for f being FinSequence of REAL,r1,r2 being Real st f=<*r1,r2*> holds
  max f=max(r1,r2) & max_p f=IFEQ(r1,max(r1,r2),1,2);

theorem :: RFINSEQ2:6
  for f being FinSequence of REAL,r1,r2 being Real st f=<*r1,r2*> holds
  min f=min(r1,r2) & min_p f=IFEQ(r1,min(r1,r2),1,2);

theorem :: RFINSEQ2:7
  for f1,f2 being FinSequence of REAL st len f1=len f2 & len f1>0 holds
  max (f1+f2)<=(max f1) +(max f2);

theorem :: RFINSEQ2:8
  for f1,f2 being FinSequence of REAL st len f1=len f2 & len f1>0 holds
  min (f1+f2)>=(min f1) +(min f2);

theorem :: RFINSEQ2:9
  for f being FinSequence of REAL, a being Real st len f>0 & a>0 holds
  max (a*f)=a*(max f) & max_p (a*f)=max_p f;

theorem :: RFINSEQ2:10
  for f being FinSequence of REAL, a being Real st len f>0 & a>0 holds
  min (a*f)=a*(min f) & min_p (a*f)=min_p f;

theorem :: RFINSEQ2:11
  for f being FinSequence of REAL st len f>0 holds max (-f)=-(min f) &
  max_p (-f)=min_p f;

theorem :: RFINSEQ2:12
  for f being FinSequence of REAL st len f>0 holds min (-f)=-(max f) &
  min_p (-f)=max_p f;

theorem :: RFINSEQ2:13
  for f being FinSequence of REAL,n being Nat st n<len f
  holds max (f/^n)<= max f & min (f/^n)>= min f;

theorem :: RFINSEQ2:14
  for f,g being FinSequence of REAL st f,g
  are_fiberwise_equipotent holds max f=max g;

theorem :: RFINSEQ2:15
  for f,g being FinSequence of REAL st f,g
  are_fiberwise_equipotent holds min f=min g;

definition
  let f be FinSequence of REAL;
  func sort_d f -> non-increasing FinSequence of REAL means
:: RFINSEQ2:def 5
  ::Descend Sorting or Rearrangement of FinSequences

  f,it are_fiberwise_equipotent;
 projectivity;
end;

theorem :: RFINSEQ2:16
  for R be FinSequence of REAL st len R = 0 or len R = 1 holds R
  is non-decreasing;

theorem :: RFINSEQ2:17
  for R be FinSequence of REAL holds R is non-decreasing iff for n
  ,m be Nat st n in dom R & m in dom R & n<m holds R.n<=R.m;

theorem :: RFINSEQ2:18
  for R be non-decreasing FinSequence of REAL, n be Nat
  holds R|n is non-decreasing FinSequence of REAL;

theorem :: RFINSEQ2:19
  for R1,R2 be non-decreasing FinSequence of REAL st R1,R2
  are_fiberwise_equipotent holds R1 = R2;

definition
  let f be FinSequence of REAL;
  func sort_a f -> non-decreasing FinSequence of REAL means
:: RFINSEQ2:def 6
  ::Ascend Sorting or Rearrangement of FinSequences

  f,it are_fiberwise_equipotent;
 projectivity;
end;

theorem :: RFINSEQ2:20
  for f being non-increasing FinSequence of REAL holds sort_d f=f;

theorem :: RFINSEQ2:21
  for f being non-decreasing FinSequence of REAL holds sort_a f=f;

::$CT 2

theorem :: RFINSEQ2:24
  for f being FinSequence of REAL st f is non-increasing holds -f
  is non-decreasing;

theorem :: RFINSEQ2:25
  for f being FinSequence of REAL st f is non-decreasing holds -f
  is non-increasing;

theorem :: RFINSEQ2:26
  for f,g being FinSequence of REAL,P being Permutation of dom g
  st f = g*P & len g>=1 holds -f=(-g)*P;

theorem :: RFINSEQ2:27
  for f,g being FinSequence of REAL st f,g
  are_fiberwise_equipotent holds -f,-g are_fiberwise_equipotent;

theorem :: RFINSEQ2:28
  for f being FinSequence of REAL holds sort_d (-f) = - (sort_a f);

theorem :: RFINSEQ2:29
  for f being FinSequence of REAL holds sort_a (-f) = - (sort_d f);

theorem :: RFINSEQ2:30
  for f being FinSequence of REAL holds dom (sort_d f)=dom f & len
  (sort_d f)=len f;

theorem :: RFINSEQ2:31
  for f being FinSequence of REAL holds dom (sort_a f)=dom f & len
  (sort_a f)=len f;

theorem :: RFINSEQ2:32
  for f being FinSequence of REAL st len f >=1 holds max_p(sort_d f)=1 &
  min_p(sort_a f)=1 & (sort_d f).1=max f & (sort_a f).1=min f;