:: The Semantics of MML Query -- Ordering
:: by Grzegorz Bancerek
::
:: Received December 1, 2012
:: Copyright (c) 2012-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 MMLQUER2, RELAT_1, XBOOLE_0, SUBSET_1, AOFA_000, RELAT_2, TARSKI,
FUNCT_1, NUMBERS, MMLQUERY, ARYTM_3, ORDINAL1, PARTFUN1, ORDERS_1,
ORDINAL4, ZFMISC_1, XXREAL_0, FINSEQ_1, FINSEQ_4, SETFAM_1, CARD_1,
NAT_1, FUNCT_7, WELLORD1, REWRITE1, FINSET_1, PEPIN, AFINSQ_1, WELLORD2,
ORDINAL2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, AOFA_000,
RELAT_2, FUNCT_1, FINSET_1, FINSEQ_1, CARD_1, NAT_1, MEMBERED, ORDERS_1,
ORDINAL1, NUMBERS, PARTFUN1, FUNCT_2, MMLQUERY, ORDINAL2, ORDINAL4,
AFINSQ_1, XXREAL_0, XCMPLX_0, WELLORD1, FUNCT_7, RELSET_1, REWRITE1,
WELLORD2, TOLER_1;
constructors TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELAT_2, MMLQUERY, XXREAL_0,
ORDINAL1, VALUED_0, ORDERS_1, FINSEQ_4, XCMPLX_0, FUNCT_1, FUNCT_7,
ZFMISC_1, WELLORD2, PARTFUN1, FUNCT_2, NUMBERS, NAT_1, REWRITE1,
MEMBERED, RELSET_1, WELLORD1, TOLER_1, ORDINAL2, ORDINAL3, ORDINAL4;
registrations RELAT_1, RELSET_1, ARMSTRNG, VALUED_0, ARROW, FINSEQ_1,
XXREAL_0, CARD_1, SUBSET_1, XCMPLX_0, ORDINAL1, NAT_1, FUNCT_7, MEMBERED,
FINSET_1, XBOOLE_0, AFINSQ_1;
requirements BOOLE, SUBSET, NUMERALS;
begin :: Preliminaries
reserve X for set, R,R1,R2 for Relation;
reserve x,y,z for set;
reserve n,m,k for Nat;
theorem :: MMLQUER2:1
for R being Relation of X holds field R c= X;
theorem :: MMLQUER2:2
for R being Relation of X st x,y in R holds x in X & y in X;
theorem :: MMLQUER2:3
for X,Y being set holds (id X).:Y = X /\ Y;
theorem :: MMLQUER2:4
[x,y] in R |_2 X iff x in X & y in X & [x,y] in R;
theorem :: MMLQUER2:5
dom(X|`R) c= dom R;
theorem :: MMLQUER2:6
for R being total reflexive Relation of X
for S being Subset of X holds
R |_2 S is total reflexive Relation of S;
theorem :: MMLQUER2:7 ::: AFINSQ_1:26 generalized
for f,g being Sequence holds rng(f^g) = rng f \/ rng g;
definition
let R;
redefine attr R is transitive means
:: MMLQUER2:def 1
x,y in R & y,z in R implies x,z in R;
redefine attr R is antisymmetric means
:: MMLQUER2:def 2
x,y in R & y,x in R implies x = y;
end;
theorem :: MMLQUER2:8
for X being non empty set
for R being total connected Relation of X
for x,y being Element of X st x <> y holds x,y in R or y,x in R;
begin :: Composition of orders
definition
let R1,R2 be Relation;
func R1\,R2 -> Relation equals
:: MMLQUER2:def 3
R1 \/ (R2 \ R1~);
end;
theorem :: MMLQUER2:9
x,y in R1\,R2 iff x,y in R1 or y,x nin R1 & x,y in R2;
theorem :: MMLQUER2:10
field (R1\,R2) = field R1 \/ field R2;
theorem :: MMLQUER2:11
R1\,R2 c= R1 \/ R2;
definition
let X be set;
let R1,R2 be Relation of X;
redefine func R1\,R2 -> Relation of X;
end;
registration
let R1,R2 be reflexive Relation;
cluster R1\,R2 -> reflexive;
end;
registration
let R1,R2 be antisymmetric Relation;
cluster R1\,R2 -> antisymmetric;
end;
definition
let X be set;
let R be Relation of X;
attr R is beta-transitive means
:: MMLQUER2:def 4
for x,y being Element of X st x,y nin R
for z being Element of X holds (x,z in R implies y,z in R);
end;
registration
let X be set;
cluster connected total transitive -> beta-transitive for Relation of X;
end;
registration
let X be set;
cluster connected for Order of X;
end;
registration
let X be set;
let R1 be beta-transitive transitive Relation of X;
let R2 be transitive Relation of X;
cluster R1\,R2 -> transitive;
end;
registration
let X be set;
let R1 be Relation of X;
let R2 be total reflexive Relation of X;
cluster R1\,R2 -> total reflexive for Relation of X;
end;
registration
let X be set;
let R1 be Relation of X;
let R2 be total connected reflexive Relation of X;
cluster R1\,R2 -> connected;
end;
theorem :: MMLQUER2:12
(R\,R1)\,R2 = R\,(R1\,R2);
theorem :: MMLQUER2:13
for R being connected reflexive total Relation of X
for R2 being Relation of X holds R\,R2 = R;
begin :: "number of" ordering
definition
let X be set;
let f be Function of X,NAT;
func value_of(f) -> Relation of X means
:: MMLQUER2:def 5
x,y in it iff x in X & y in X & f.x < f.y;
end;
registration
let X be set;
let f be Function of X,NAT;
cluster value_of f -> antisymmetric transitive beta-transitive;
end;
definition
let X be finite set;
let O be Operation of X;
func number_of O -> Function of X,NAT means
:: MMLQUER2:def 6
for x being Element of X holds it.x = card (x.O);
end;
theorem :: MMLQUER2:14
for X being finite set
for O being Operation of X, x,y being Element of X holds
x,y in value_of number_of O iff card(x.O) < card(y.O);
definition
let X;
let O be Operation of X;
func first O -> Relation of X means
:: MMLQUER2:def 7
for x,y being Element of X holds x,y in it iff x.O <> {} & y.O = {};
end;
registration
let X;
let O be Operation of X;
cluster first O -> antisymmetric transitive beta-transitive;
end;
begin :: Ordering by resources
definition
let A be FinSequence;
let x be object;
func A <- x -> set equals
:: MMLQUER2:def 8
meet (A"{x});
end;
registration
let A be FinSequence;
let x;
cluster A <- x -> natural;
end;
theorem :: MMLQUER2:15
for A being FinSequence st x nin rng A holds A <- x = 0;
theorem :: MMLQUER2:16
for A being FinSequence st x in rng A holds A <- x in dom A & x = A.(A <- x);
theorem :: MMLQUER2:17
for A being FinSequence st A <- x = 0 holds x nin rng A;
definition
let X;
let A be FinSequence;
let f be Function;
func resource(X,A,f) -> Relation of X means
:: MMLQUER2:def 9
x,y in it iff x in X & y in X &
A <- (f.x) <> 0 & (A <- (f.x) < A <- (f.y) or A <- (f.y) = 0);
end;
registration
let X;
let A be FinSequence;
let f be Function;
cluster resource(X,A,f) -> antisymmetric transitive beta-transitive;
end;
begin :: Ordering by number of iteration
definition
let X;
let R be Relation of X;
let n be Nat;
redefine func iter(R,n) -> Relation of X;
end;
theorem :: MMLQUER2:18
iter(R,n).:X = {} & m >= n implies iter(R,m).:X = {};
theorem :: MMLQUER2:19
(for n holds iter(R,n).:X <> {}) & X is finite implies ex x st x in X &
for n holds Im(iter(R,n),x) <> {};
theorem :: MMLQUER2:20
R is co-well_founded irreflexive & X is finite & R is finite
implies ex n st iter(R,n).:X = {};
definition
let X;
let O be Operation of X such that
O is co-well_founded irreflexive finite;
func iteration_of O -> Relation of X means
:: MMLQUER2:def 10
ex f being Function of X,NAT st it = value_of f &
for x being Element of X st x in X
ex n st f.x = n & (x.iter(O,n) <> {} or n = 0 & x.iter(O,n) = {}) &
x.iter(O,n+1) = {};
end;
registration
cluster empty -> irreflexive co-well_founded for Relation;
end;
registration
let X;
cluster empty for Operation of X;
end;
registration
let X;
let O be co-well_founded irreflexive finite Operation of X;
cluster iteration_of O -> antisymmetric transitive beta-transitive;
end;
begin :: "value of" ordering
registration
let X be finite set;
cluster -> well_founded for Order of X;
end;
registration
let X be finite set;
cluster -> well-ordering for connected Order of X;
end;
definition
let X;
let R be connected Order of X;
let S be finite Subset of X;
func order(S,R) -> XFinSequence of X means
:: MMLQUER2:def 11
rng it = S & it is one-to-one &
for i,j being Nat st i in dom it & j in dom it holds
i <= j iff it.i,it.j in R;
end;
theorem :: MMLQUER2:21
for S1,S2 being finite Subset of X
for R being connected Order of X holds
order(S1 \/ S2,R) = order(S1,R)^order(S2,R) iff
for x,y st x in S1 & y in S2 holds x <> y & x,y in R;
definition
let X be finite set;
let O be Operation of X;
let R be connected Order of X;
func value_of(O,R) -> Relation of X means
:: MMLQUER2:def 12
for x,y being Element of X holds
x,y in it iff x.O <> {} & (y.O = {} or
y.O <> {} & order(x.O,R)/.0, order(y.O,R)/.0 in R &
order(x.O,R)/.0 <> order(y.O,R)/.0);
end;
registration
let X be finite set;
let O be Operation of X;
let R1 be connected Order of X;
cluster value_of(O,R1) -> antisymmetric transitive beta-transitive;
end;