The abstract of the Mizar article:

Sorting Operators for Finite Sequences

by

Yatsuka Nakamura

Received October 17, 2003

MML identifier: RFINSEQ2

[ Mizar article, MML identifier index ]

environ

 vocabulary RELAT_1, CARD_1, FUNCT_1, BOOLE, FUNCT_2, FINSEQ_1, ARYTM_1,
      SQUARE_1, PROB_1, RFINSEQ, RFINSEQ2, CQC_LANG;
 notation TARSKI, XBOOLE_0, NUMBERS, XREAL_0, RELAT_1, FUNCT_1, FUNCT_2,
      FINSEQ_1, CARD_1, REAL_1, NAT_1, SQUARE_1, SEQ_1, RVSUM_1, TOPREAL1,
      CQC_LANG, RFINSEQ, INTEGRA2;
 constructors REAL_1, NAT_1, SQUARE_1, TOPREAL1, SEQ_1, CQC_LANG, RFINSEQ,
      INTEGRA2;
 clusters NUMBERS, FUNCT_1, RELSET_1, FINSEQ_1, XREAL_0, FUNCT_2, REAL_1,
      NAT_1, RFINSEQ, INTEGRA2;
 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
 1<=n & 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;
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;
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;

theorem :: RFINSEQ2:22
for f being FinSequence of REAL
 holds sort_d (sort_d f)=sort_d f;

theorem :: RFINSEQ2:23
for f being FinSequence of REAL
 holds sort_a (sort_a f)=sort_a f;

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;