:: Sorting by Exchanging
:: by Grzegorz Bancerek
::
:: Received October 18, 2010
:: Copyright (c) 2010-2016 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 ORDINAL6, EXCHSORT, ZFMISC_1, XBOOLE_0, RELAT_1, FUNCT_1,
ORDINAL1, ORDINAL2, ORDINAL4, FINSET_1, RELAT_2, FUNCT_4, FINSEQ_1,
AOFA_000, FUNCT_3, VALUED_0, WELLFND1, CARD_1, TARSKI, FUNCT_2, PARTFUN1,
FUNCT_7, REARRAN1, ORDINAL3, NAT_1, SUBSET_1, XXREAL_0, ARYTM_3,
AFINSQ_1, REWRITE1, NUMBERS, MSUALG_1, MEMBERED, STRUCT_0, ORDERS_2,
REAL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, RELAT_2,
RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1, FINSEQ_1, BINOP_1,
FUNCT_4, FUNCT_7, ORDINAL1, NUMBERS, MEMBERED, VALUED_0, CARD_1,
XCMPLX_0, ORDINAL2, ORDINAL3, ORDINAL4, AFINSQ_1, STRUCT_0, ORDERS_2,
WAYBEL_0, XXREAL_0, XREAL_0, NAT_1, AOFA_000, ORDINAL5, FUNCT_3,
ORDINAL6;
constructors MEMBERED, VALUED_0, CATALAN2, ORDINAL3, INT_1, FUNCT_7, ORDINAL5,
WELLORD2, RELAT_2, FACIRC_1, BINOP_1, WAYBEL_0, RELSET_1, ORDINAL6,
XTUPLE_0;
registrations MEMBERED, SUBSET_1, RELSET_1, XXREAL_0, XBOOLE_0, FINSET_1,
RELAT_1, FUNCT_1, ORDINAL1, VALUED_0, ORDINAL5, AFINSQ_1, CARD_1,
FUNCT_2, FUNCT_7, FUNCTOR1, STRUCT_0, WAYBEL_0, ORDINAL6, XCMPLX_0;
requirements NUMERALS, SUBSET, BOOLE, REAL;
begin :: Preliminaries
reserve a,a1,a2,b,c,d for Ordinal,
n,m,k for Nat,
x,y,z,t,X,Y,Z for set;
theorem :: EXCHSORT:1
x in (a+^b)\a iff ex c st x = a+^c & c in b;
theorem :: EXCHSORT:2
a in b & c in d implies
c <> a & c <> b & d <> a & d <> b or
c in a & d = a or c in a & d = b or
c = a & d in b or c = a & d = b or c = a & b in d or
a in c & d = b or c = b & b in d;
theorem :: EXCHSORT:3
x nin y implies (y\/{x})\y = {x};
theorem :: EXCHSORT:4
(succ x)\x = {x};
theorem :: EXCHSORT:5
for f being Function, r being Relation
for x being object holds x in f.:r iff
ex y,z being object st [y,z] in r & [y,z] in dom f & f.(y,z) = x;
theorem :: EXCHSORT:6
a\b <> {} implies inf(a\b) = b & sup(a\b) = a & union(a\b) = union a;
theorem :: EXCHSORT:7
a\b is non empty finite implies
ex n being Nat st a = b+^n;
begin :: Arrays
definition let f be set;
attr f is segmental means
:: EXCHSORT:def 1
ex a,b st proj1 f = a\b;
end;
reserve f,g for Function;
theorem :: EXCHSORT:8
dom f = dom g & f is segmental implies g is segmental;
theorem :: EXCHSORT:9
f is segmental implies
for a,b,c st a c= b & b c= c & a in dom f & c in dom f holds b in dom f;
registration
cluster Sequence-like -> segmental for Function;
cluster FinSequence-like -> segmental for Function;
end;
definition
let a;
let s be set;
attr s is a-based means
:: EXCHSORT:def 2
b in proj1 s implies a in proj1 s & a c= b;
attr s is a-limited means
:: EXCHSORT:def 3
a = sup proj1 s;
end;
theorem :: EXCHSORT:10
f is a-based segmental iff ex b st dom f = b\a & a c= b;
theorem :: EXCHSORT:11
f is b-limited non empty segmental iff ex a st dom f = b\a & a in b;
registration
cluster Sequence-like -> 0-based for Function;
cluster FinSequence-like -> 1-based for Function;
end;
theorem :: EXCHSORT:12
f is (inf dom f)-based;
theorem :: EXCHSORT:13
f is (sup dom f)-limited;
theorem :: EXCHSORT:14
f is b-limited & a in dom f implies a in b;
definition let f;
func base-f -> Ordinal means
:: EXCHSORT:def 4
f is it-based if ex a st a in dom f
otherwise it = 0;
func limit-f -> Ordinal means
:: EXCHSORT:def 5
f is it-limited if ex a st a in dom f
otherwise it = 0;
end;
definition
let f;
func len-f -> Ordinal equals
:: EXCHSORT:def 6
(limit-f)-^(base-f);
end;
theorem :: EXCHSORT:15
base-{} = 0 & limit-{} = 0 & len-{} = 0;
theorem :: EXCHSORT:16
limit-f = sup dom f;
theorem :: EXCHSORT:17
f is (limit-f)-limited;
theorem :: EXCHSORT:18
for A being empty set holds A is a-based;
registration let a,X,Y;
cluster Y-defined X-valued a-based segmental finite empty for Sequence;
end;
definition
mode array is segmental Function;
end;
registration
let A be array;
cluster dom A -> ordinal-membered;
end;
theorem :: EXCHSORT:19
for f being array holds f is 0-limited iff f is empty;
registration
cluster 0-based -> Sequence-like for array;
end;
definition
let X;
mode array of X is X-valued array;
end;
definition
let X be 1-sorted;
mode array of X is array of the carrier of X;
end;
definition
let a,X;
mode array of a,X is a-defined array of X;
end;
reserve A,B,C for array;
theorem :: EXCHSORT:20
base-f = inf dom f;
theorem :: EXCHSORT:21
f is (base-f)-based;
theorem :: EXCHSORT:22
dom A = (limit-A) \ (base-A);
theorem :: EXCHSORT:23
dom A = a\b & A is non empty implies base-A = b & limit-A = a;
theorem :: EXCHSORT:24
for f be Sequence holds
base-f = 0 & limit-f = dom f & len-f = dom f;
registration
let a,b,X;
cluster b-based natural-valued INT-valued real-valued complex-valued
finite for array of a,X;
end;
registration
let a,x;
cluster {[a,x]} -> segmental;
end;
registration
let a; let x be Nat;
cluster {[a,x]} -> natural-valued for array;
end;
registration
let a; let x be Real;
cluster {[a,x]} -> real-valued for array;
end;
registration
let a; let X be non empty set;
let x be Element of X;
cluster {[a,x]} -> X-valued for array;
end;
registration
let a,x;
cluster {[a,x]} -> a-based succ a-limited for array;
end;
registration
let b;
cluster non empty b-based natural-valued INT-valued real-valued
complex-valued finite for array;
let X be non empty set;
cluster non empty b-based finite X-valued for array;
end;
notation
let s be Sequence;
synonym s last for last s;
end;
definition
let A be array;
func last A -> set equals
:: EXCHSORT:def 7
A.union dom A;
end;
registration
let A be Sequence;
identify A last with last A;
end;
begin :: Descending sequence
definition
let f be Function;
attr f is descending means
:: EXCHSORT:def 8
for a,b st a in dom f & b in dom f & a in b holds f.b c< f.a;
end;
theorem :: EXCHSORT:25
for f being finite array
st for a st a in dom f & succ a in dom f holds f.succ a c< f.a
holds f is descending;
theorem :: EXCHSORT:26
for f being array st len-f = omega &
for a st a in dom f & succ a in dom f holds f.succ a c< f.a
holds f is descending;
theorem :: EXCHSORT:27
for f being Sequence st f is descending & f.0 is finite
holds f is finite;
theorem :: EXCHSORT:28
for f being Sequence st f is descending & f.0 is finite &
for a st f.a <> {} holds succ a in dom f
holds last f = {};
scheme :: EXCHSORT:sch 1
A{A() -> Sequence, F(set)->set}:
A() is finite
provided
F(A().0) is finite and
for a st succ a in dom A() & F(A().a) is finite
holds F(A().succ a) c< F(A().a);
begin :: Swap
registration
let X;
let f be X-defined Function;
let a,b be object;
cluster Swap(f,a,b) -> X-defined;
end;
registration
let X be set;
let f be X-valued Function;
let x,y be object;
cluster Swap(f,x,y) -> X-valued;
end;
theorem :: EXCHSORT:29
x in dom f & y in dom f implies Swap(f,x,y).x = f.y;
theorem :: EXCHSORT:30
for f being array of X st x in dom f & y in dom f
holds Swap(f,x,y)/.x = f/.y;
theorem :: EXCHSORT:31
x in dom f & y in dom f implies Swap(f,x,y).y = f.x;
theorem :: EXCHSORT:32
for f being array of X st x in dom f & y in dom f
holds Swap(f,x,y)/.y = f/.x;
theorem :: EXCHSORT:33
for x,y,z being object holds
z <> x & z <> y implies Swap(f,x,y).z = f.z;
theorem :: EXCHSORT:34
for f being array of X st z in dom f & z <> x & z <> y
holds Swap(f,x,y)/.z = f/.z;
theorem :: EXCHSORT:35
x in dom f & y in dom f implies Swap(f,x,y) = Swap(f,y,x);
registration
let X be non empty set;
cluster onto for X-valued non empty Function;
end;
registration
let X be non empty set;
let f be onto X-valued non empty Function;
let x,y be Element of dom f;
cluster Swap(f,x,y) -> onto;
end;
registration
let A;
let x,y;
cluster Swap(A,x,y) -> segmental;
end;
theorem :: EXCHSORT:36
x in dom A & y in dom A implies Swap(Swap(A,x,y),x,y) = A;
registration
let A be real-valued array;
let x,y;
cluster Swap(A,x,y) -> real-valued for array;
end;
begin :: Permutations
definition
let A be array;
mode permutation of A -> array means
:: EXCHSORT:def 9
ex f being Permutation of dom A st it = A*f;
end;
theorem :: EXCHSORT:37
for B being permutation of A holds dom B = dom A & rng B = rng A;
theorem :: EXCHSORT:38
A is permutation of A;
theorem :: EXCHSORT:39
A is permutation of B implies B is permutation of A;
theorem :: EXCHSORT:40
A is permutation of B & B is permutation of C implies A is permutation of C;
theorem :: EXCHSORT:41
Swap(id X,x,y) is one-to-one;
registration
let X be non empty set;
let x,y be Element of X;
cluster Swap(id X,x,y) -> one-to-one X-valued X-defined;
end;
registration
let X be non empty set;
let x,y be Element of X;
cluster Swap(id X,x,y) -> onto total;
end;
definition
let X,Y be non empty set;
let f be Function of X,Y;
let x,y be Element of X;
redefine func Swap(f,x,y) -> Function of X,Y;
end;
theorem :: EXCHSORT:42
x in X & y in X & f = Swap(id X,x,y) & X = dom A implies
Swap(A,x,y) = A*f;
theorem :: EXCHSORT:43
x in dom A & y in dom A implies
Swap(A,x,y) is permutation of A & A is permutation of Swap(A,x,y);
theorem :: EXCHSORT:44
x in dom A & y in dom A & A is permutation of B implies
Swap(A,x,y) is permutation of B & A is permutation of Swap(B,x,y);
begin :: Exchanging
definition
let O be RelStr;
let A be array of O;
attr A is ascending means
:: EXCHSORT:def 10
for a,b st a in dom A & b in dom A & a in b holds A/.a <= A/.b;
func inversions A -> set equals
:: EXCHSORT:def 11
{[a,b] where a,b is Element of dom A: a in b & not A/.a <= A/.b};
end;
registration
let O be RelStr;
cluster -> ascending for empty array of O;
let A be empty array of O;
cluster inversions A -> empty;
end;
reserve O for connected non empty Poset;
reserve R,Q for array of O;
theorem :: EXCHSORT:45
for O for x,y being Element of O holds x > y iff not x <= y;
definition
let O,R;
redefine func inversions R equals
:: EXCHSORT:def 12
{[a,b] where a,b is Element of dom R: a in b & R/.a > R/.b};
end;
theorem :: EXCHSORT:46
for x being object, y being set holds
[x,y] in inversions R iff x in dom R & y in dom R & x in y & R/.x > R/.y;
theorem :: EXCHSORT:47
inversions R c= [:dom R, dom R:];
registration
let O;
let R be finite array of O;
cluster inversions R -> finite;
end;
theorem :: EXCHSORT:48
R is ascending iff inversions R = {};
theorem :: EXCHSORT:49
[x,y] in inversions R implies [y,x] nin inversions R;
theorem :: EXCHSORT:50
[x,y] in inversions R & [y,z] in inversions R implies [x,z] in inversions R;
registration
let O,R;
cluster inversions R -> Relation-like;
end;
registration
let O,R;
cluster inversions R -> asymmetric transitive for Relation;
end;
definition
let O;
let a,b be Element of O;
redefine pred a < b;
asymmetry;
end;
theorem :: EXCHSORT:51
[x,y] in inversions R implies [x,y] nin inversions Swap(R,x,y);
theorem :: EXCHSORT:52
x in dom R & y in dom R & z <> x & z <> y & t <> x & t <> y
implies
([z,t] in inversions R iff [z,t] in inversions Swap(R,x,y));
theorem :: EXCHSORT:53
[x,y] in inversions R implies
([z,y] in inversions R & z in x iff [z,x] in inversions Swap(R,x,y));
theorem :: EXCHSORT:54
[x,y] in inversions R implies
([z,x] in inversions R iff z in x & [z,y] in inversions Swap(R,x,y));
theorem :: EXCHSORT:55
[x,y] in inversions R & z in y & [x,z] in inversions Swap(R,x,y) implies
[x,z] in inversions R;
theorem :: EXCHSORT:56
[x,y] in inversions R & x in z & [z,y] in inversions Swap(R,x,y) implies
[z,y] in inversions R;
theorem :: EXCHSORT:57
[x,y] in inversions R & y in z & [x,z] in inversions Swap(R,x,y) implies
[y,z] in inversions R;
theorem :: EXCHSORT:58
[x,y] in inversions R implies
(y in z & [x,z] in inversions R iff [y,z] in inversions Swap(R,x,y));
definition
let O,R,x,y;
func (R,x,y)incl -> Function equals
:: EXCHSORT:def 13
[:Swap(id dom R,x,y), Swap(id dom R,x,y):] +*
id([:{x},(succ y)\x:]\/[:(succ y)\x,{y}:]);
end;
theorem :: EXCHSORT:59
c in (succ b)\a iff a c= c & c c= b;
reserve T for non empty array of O;
reserve p,q,r,s for Element of dom T;
theorem :: EXCHSORT:60
(succ q)\p c= dom T;
theorem :: EXCHSORT:61
dom (T,p,q)incl = [:dom T, dom T:] & rng (T,p,q)incl c= [:dom T, dom T:];
theorem :: EXCHSORT:62
p c= r & r c= q implies
(T,p,q)incl.(p,r) = [p, r] & (T,p,q)incl.(r,q) = [r,q];
theorem :: EXCHSORT:63
r <> p & s <> q & f = Swap(id dom T,p,q)
implies (T,p,q)incl.(r,s) = [f.r,f.s];
theorem :: EXCHSORT:64
r in p & f = Swap(id dom T,p,q) implies
(T,p,q)incl.(r,q) = [f.r,f.q] & (T,p,q)incl.(r,p) = [f.r,f.p];
theorem :: EXCHSORT:65
q in r & f = Swap(id dom T,p,q) implies
(T,p,q)incl.(p,r) = [f.p,f.r] & (T,p,q)incl.(q,r) = [f.q,f.r];
theorem :: EXCHSORT:66
p in q implies (T,p,q)incl.(p,q) = [p,q];
theorem :: EXCHSORT:67
p in q & r <> p & r <> q & s <> p & s <> q implies (T,p,q)incl.(r,s) = [r,s];
theorem :: EXCHSORT:68
r in p & p in q implies (T,p,q)incl.(r,p) = [r,q] & (T,p,q)incl.(r,q) = [r,p]
;
theorem :: EXCHSORT:69
p in s & s in q implies (T,p,q)incl.(p,s) = [p,s] & (T,p,q)incl.(s,q) = [s,q]
;
theorem :: EXCHSORT:70
p in q & q in s implies (T,p,q)incl.(p,s) = [q,s] & (T,p,q)incl.(q,s) = [p,s]
;
theorem :: EXCHSORT:71
p in q implies (T,p,q)incl|(inversions Swap(T,p,q) qua set) is one-to-one;
registration
let O,R,x,y,z;
cluster (R,x,y)incl.:z -> Relation-like;
end;
begin :: Correctness of sorting by exchanging
theorem :: EXCHSORT:72
[x,y] in inversions R implies
(R,x,y)incl.:inversions Swap(R,x,y) c< inversions R;
registration
let R be finite Function;
let x,y;
cluster Swap(R,x,y) -> finite;
end;
theorem :: EXCHSORT:73
for R being array of O
st [x,y] in inversions R & inversions R is finite
holds card inversions Swap(R,x,y) in card inversions R;
theorem :: EXCHSORT:74
for R being finite array of O st [x,y] in inversions R
holds card inversions Swap(R,x,y) < card inversions R;
definition
let O,R;
mode arr_computation of R -> non empty array means
:: EXCHSORT:def 14
it.(base-it) = R & (for a st a in dom it holds it.a is array of O) &
for a st a in dom it & succ a in dom it
ex R,x,y st [x,y] in inversions R & it.a = R & it.succ a = Swap(R,x,y);
end;
theorem :: EXCHSORT:75
{[a,R]} is arr_computation of R;
registration
let O,R,a;
cluster a-based finite for arr_computation of R;
end;
registration
let O,R;
let C be arr_computation of R;
let x;
cluster C.x -> segmental Function-like Relation-like;
end;
registration
let O,R;
let C be arr_computation of R;
let x;
cluster C.x -> the carrier of O-valued;
end;
registration
let O,R;
let C be arr_computation of R;
cluster last C -> segmental Relation-like Function-like;
end;
registration
let O,R;
let C be arr_computation of R;
cluster last C -> the carrier of O-valued;
end;
definition
let O,R;
let C be arr_computation of R;
attr C is complete means
:: EXCHSORT:def 15
last C is ascending;
end;
theorem :: EXCHSORT:76
for C being 0-based arr_computation of R st R is finite array of O
holds C is finite;
theorem :: EXCHSORT:77
for C being 0-based arr_computation of R st R is finite array of O &
for a st inversions (C.a) <> {} holds succ a in dom C
holds C is complete;
theorem :: EXCHSORT:78
for C being finite arr_computation of R
holds last C is permutation of R &
for a st a in dom C holds C.a is permutation of R;
begin :: Existence of Complete Computations
theorem :: EXCHSORT:79
for A being 0-based finite array of X st A <> {} holds last A in X;
theorem :: EXCHSORT:80
last <%x%> = x;
theorem :: EXCHSORT:81
for A being 0-based finite array holds last (A^<%x%>) = x;
registration
let X be set;
cluster -> X-valued for Element of X^omega;
end;
scheme :: EXCHSORT:sch 2
A{F(set)->set, X()->non empty set, P[set,set], s()->set}:
ex f being finite 0-based non empty array, k being Element of X() st
k = last f & F(k) = {} & f.0 = s() &
for a st succ a in dom f
ex x,y being Element of X() st x = f.a & y = f.succ a & P[x,y]
provided
s() in X() and
F(s()) is finite and
for x being Element of X() st F(x) <> {}
ex y being Element of X() st P[x,y] & F(y) c< F(x);
reserve A for array, B for permutation of A;
theorem :: EXCHSORT:82
B in Funcs(dom A, rng A);
registration
let A be real-valued array;
cluster -> real-valued for permutation of A;
end;
registration
let a;
let X be non empty set;
cluster -> Sequence-like for Element of Funcs(a,X);
end;
registration
let X;
let Y be real-membered non empty set;
cluster -> real-valued for Element of Funcs(X,Y);
end;
registration
let X;
let A be array of X;
cluster -> X-valued for permutation of A;
end;
registration
let X be set;
let Z be set;
let Y be Subset of Z;
cluster -> Z-valued for Element of Funcs(X,Y);
end;
theorem :: EXCHSORT:83
for r being X-defined Y-valued Relation holds r is Relation of X,Y;
theorem :: EXCHSORT:84
for a being finite Ordinal, x st x in a
holds x = 0 or ex b st x = succ b;
theorem :: EXCHSORT:85
for A being 0-based finite non empty array of O
ex C being 0-based arr_computation of A st C is complete;
theorem :: EXCHSORT:86
for A being 0-based finite non empty array of O
ex B being permutation of A st B is ascending;
registration
let O;
let A be 0-based finite array of O;
cluster ascending for permutation of A;
end;