:: The Semantics of MML Query -- Ordering
::  by Grzegorz Bancerek
::
:: Received December 1, 2012
:: Copyright (c) 2012-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 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, XXREAL_0, CARD_1,
      SUBSET_1, XCMPLX_0, ORDINAL1, NAT_1, 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;

::$CT

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;

::$CT


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;