:: Dickson's lemma
::  by Gilbert Lee and Piotr Rudnicki
::
:: Received March 12, 2002
:: Copyright (c) 2002-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 FUNCT_1, RELAT_1, FUNCOP_1, NAT_1, TARSKI, ARYTM_3, XBOOLE_0,
      SUBSET_1, NUMBERS, XXREAL_0, FINSET_1, CARD_1, ORDERS_2, REARRAN1,
      RELAT_2, STRUCT_0, WELLORD1, WAYBEL_4, WAYBEL20, EQREL_1, ORDERS_1,
      ZFMISC_1, WELLFND1, SETFAM_1, VALUED_0, ORDINAL2, MCART_1, CAT_1,
      YELLOW_1, PBOOLE, CARD_3, RLVECT_2, YELLOW_6, WAYBEL_3, FUNCT_4,
      YELLOW_3, DICKSON, XCMPLX_0, WELLORD2, ORDINAL1, PARTFUN1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
      PBOOLE, RELSET_1, XXREAL_2, SEQ_4, PARTFUN1, FUNCT_2, CARD_3, ORDINAL1,
      XCMPLX_0, NAT_1, STRUCT_0, RELAT_2, XXREAL_0, FUNCT_4, FUNCOP_1,
      DOMAIN_1, FINSET_1, XTUPLE_0, MCART_1, WELLORD1, WELLORD2, ORDERS_2,
      ORDERS_1, EQREL_1, WELLFND1, WAYBEL_0, CARD_1, NUMBERS, WAYBEL_4,
      VALUED_0, PRALG_1, YELLOW_3, WAYBEL_1, YELLOW_1, WAYBEL_3, YELLOW_6;
 constructors WELLORD1, DOMAIN_1, PRALG_1, ORDERS_3, WAYBEL_1, YELLOW_3,
      WAYBEL_3, WAYBEL_4, WELLFND1, SEQ_4, RELSET_1, XTUPLE_0, NUMBERS;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
      FUNCOP_1, FINSET_1, XXREAL_0, NAT_1, MEMBERED, EQREL_1, PRE_CIRC,
      STRUCT_0, ORDERS_2, YELLOW_1, YELLOW_3, WAYBEL18, WAYBEL_3, VALUED_0,
      CARD_1, XXREAL_2, CARD_3, ZFMISC_1, RELSET_1, XTUPLE_0;
 requirements BOOLE, SUBSET, NUMERALS;


begin :: Preliminaries

theorem :: DICKSON:1
  for g being Function, x being set st dom g = {x} holds g = x .--> g.x;

::$CT

theorem :: DICKSON:3
  for X being infinite set ex f being sequence of  X st f is one-to-one;

definition
  let R be RelStr, f be sequence of R;
  attr f is ascending means
:: DICKSON:def 1
  for n being Element of NAT
  holds f.(n+1) <> f.n & [f.n, f.(n+1)] in the InternalRel of R;
end;

definition
  let R be RelStr, f be sequence of R;
  attr f is weakly-ascending means
:: DICKSON:def 2
  for n being Nat holds [f.n, f.(n+1)] in the InternalRel of R;
end;

theorem :: DICKSON:4
  for R being non empty transitive RelStr, f being sequence of R
  st f is weakly-ascending
  for i,j being Nat st i < j holds f.i <= f.j;

theorem :: DICKSON:5
  for R being non empty RelStr holds R is connected iff
  the InternalRel of R is_strongly_connected_in the carrier of R;

theorem :: DICKSON:6
  for L being RelStr, Y being set, a being set
  holds (the InternalRel of L)-Seg(a) misses Y & a in Y iff
  a is_minimal_wrt Y, the InternalRel of L;

theorem :: DICKSON:7
  for L being non empty transitive antisymmetric RelStr,
  x being Element of L, a, N being set
  st a is_minimal_wrt (the InternalRel of L)-Seg(x) /\ N,(the InternalRel of L)
  holds a is_minimal_wrt N, (the InternalRel of L);

begin :: Chapter 4.2

definition
  let R be RelStr; :: Def 4.19 (ix)
  attr R is quasi_ordered means
:: DICKSON:def 3
  R is reflexive transitive;
end;

definition :: Lemma 4.24.i
  let R be RelStr such that
 R is quasi_ordered;
  func EqRel R -> Equivalence_Relation of the carrier of R equals
:: DICKSON:def 4

  (the InternalRel of R) /\ (the InternalRel of R)~;
end;

theorem :: DICKSON:8
  for R being RelStr, x,y being Element of R
  st R is quasi_ordered holds x in Class(EqRel R, y) iff x <= y & y <= x;

definition :: Lemma 4.24, (the InternalRel of R) / EqRel R
  let R be RelStr;
  func <=E R -> Relation of Class EqRel R means
:: DICKSON:def 5

  for A, B being object holds [A,B] in it iff ex a, b being Element of R
  st A = Class(EqRel R, a) & B = Class(EqRel R, b) & a <= b;
end;

theorem :: DICKSON:9  :: Lemma 4.24.ii
  for R being RelStr
  st R is quasi_ordered holds <=E R partially_orders Class(EqRel R);

theorem :: DICKSON:10 ::Lemma 4.24.iii
  for R being non empty RelStr st R is quasi_ordered & R is connected
  holds <=E R linearly_orders Class(EqRel R);

definition :: "strict part" of a relation, p. 155
  let R be Relation;
  func R\~ -> Relation equals
:: DICKSON:def 6
  R \ R~;
end;

registration
  let R be Relation;
  cluster R \~ -> asymmetric;
end;

definition
  let X be set, R be Relation of X;
  redefine func R\~ -> Relation of X;
end;

definition
  let R be RelStr;
  func R\~ -> strict RelStr equals
:: DICKSON:def 7
  RelStr(# the carrier of R, (the InternalRel of R)\~ #);
end;

registration
  let R be non empty RelStr;
  cluster R\~ -> non empty;
end;

registration
  let R be transitive RelStr;
  cluster R\~ -> transitive;
end;

registration
  let R be RelStr;
  cluster R\~ -> antisymmetric;
end;

theorem :: DICKSON:11 ::Exercise 4.27:
  for R being non empty Poset, x being Element of R
  holds Class(EqRel R, x) = {x};

theorem :: DICKSON:12 :: Exercise 4.29.i
  for R being Relation holds R = R\~ iff R is asymmetric;

theorem :: DICKSON:13 :: Exercise 4.29.ii
  for R being Relation st R is transitive holds R\~ is transitive;

theorem :: DICKSON:14 :: Exercise 4.29.iii
  for R being Relation, a, b being set st R is antisymmetric
  holds [a,b] in R\~ iff [a,b] in R & a <> b;

theorem :: DICKSON:15  :: Exercise 4.29 (addition)
  for R being RelStr st R is well_founded holds R\~ is well_founded;

theorem :: DICKSON:16  :: Exercise 4.29 (addition)
  for R being RelStr
  st R\~ is well_founded & R is antisymmetric holds R is well_founded;

begin :: Chapter 4.3

theorem :: DICKSON:17  :: Def 4.30 (see WAYBEL_4:def 26)
  for L being RelStr, N being set, x being Element of L\~
  holds x is_minimal_wrt N, the InternalRel of (L\~) iff (x in N &
  for y being Element of L st y in N & [y,x] in the InternalRel of L
  holds [x,y] in the InternalRel of L);

:: Proposition 4.31 - see WELLFND1:15
:: Omitting Example 4.32, Exercise 4.33, Exercise 4.34

theorem :: DICKSON:18 ::L_4_35: :: Lemma 4.35
  for R, S being non empty RelStr, m being Function of R,S
  st R is quasi_ordered & S is antisymmetric & S\~ is well_founded &
  for a,b being Element of R holds
  (a <= b implies m.a <= m.b) & (m.a = m.b implies [a,b] in EqRel R)
  holds R\~ is well_founded;

definition :: p. 158, restricted eq classes
  let R be non empty RelStr, N be Subset of R;
  func min-classes N -> Subset-Family of R means
:: DICKSON:def 8

  for x being set holds x in it iff ex y being Element of R\~
  st y is_minimal_wrt N, the InternalRel of (R\~) & x = Class(EqRel R,y) /\ N;
end;

theorem :: DICKSON:19  :: Lemma 4.36
  for R being non empty RelStr, N being Subset of R, x being set
  st R is quasi_ordered & x in min-classes N
  holds for y being Element of R\~ st y in x
  holds y is_minimal_wrt N, the InternalRel of R\~;

theorem :: DICKSON:20
  for R being non empty RelStr holds R\~ is well_founded iff
  for N being Subset of R st N <> {}
   ex x being object st x in min-classes N;

theorem :: DICKSON:21
  for R being non empty RelStr, N being Subset of R, y being Element of R\~
  st y is_minimal_wrt N, the InternalRel of (R\~)
  holds min-classes N is non empty;

theorem :: DICKSON:22
  for R being non empty RelStr, N being Subset of R, x being set st
  x in min-classes N holds x is non empty;

theorem :: DICKSON:23  :: Lemma 4.37
  for R being non empty RelStr st R is quasi_ordered
  holds R is connected & R\~ is well_founded iff
  for N being non empty Subset of R holds card min-classes N = 1;

theorem :: DICKSON:24 :: Lemma 4.38
  for R being non empty Poset
  holds the InternalRel of R well_orders the carrier of R iff
  for N being non empty Subset of R holds card min-classes N = 1;

definition :: Def 4.39
  let R be RelStr, N be Subset of R, B be set;
  pred B is_Dickson-basis_of N,R means
:: DICKSON:def 9

  B c= N & for a being Element of R st a in N
  ex b being Element of R st b in B & b <= a;
end;

theorem :: DICKSON:25
  for R being RelStr holds {} is_Dickson-basis_of {} the carrier of R, R;

theorem :: DICKSON:26
  for R being non empty RelStr, N being non empty Subset of R, B being set
  st B is_Dickson-basis_of N,R holds B is non empty;

definition :: Def 4.39
  let R be RelStr;
  attr R is Dickson means
:: DICKSON:def 10

  for N being Subset of R
  ex B being set st B is_Dickson-basis_of N,R & B is finite;
end;

theorem :: DICKSON:27  :: Lemma 4:40
  for R being non empty RelStr
  st R\~ is well_founded & R is connected holds R is Dickson;

theorem :: DICKSON:28  :: Exercise 4.41
  for R, S being RelStr st (the InternalRel of R) c= (the InternalRel of S) &
  R is Dickson & (the carrier of R) = (the carrier of S) holds S is Dickson;

definition
  let f be Function, b be set such that
 dom f = NAT and
 b in rng f;
  func f mindex b -> Element of NAT means
:: DICKSON:def 11

  f.it = b & for i being Element of NAT st f.i = b holds it <= i;
end;

definition
  let R be non empty 1-sorted, f be sequence of R, b be set,
  m be Element of NAT;
  assume
 ex j being Element of NAT st m < j & f.j = b;
  func f mindex (b,m) -> Element of NAT means
:: DICKSON:def 12

  f.it = b & m < it & for i being Element of NAT st m < i & f.i = b
  holds it <= i;
end;

theorem :: DICKSON:29  :: Prop 4.42 (i) -> (ii)
  for R being non empty RelStr st R is Dickson
  for f being sequence of R ex i,j being Nat st i < j & f.i <= f.j;

theorem :: DICKSON:30
  for R being RelStr, N being Subset of R, x being Element of R\~
  st R is quasi_ordered & x in N &
  ((the InternalRel of R)-Seg(x)) /\ N c= Class(EqRel R,x)
  holds x is_minimal_wrt N, the InternalRel of R\~;

theorem :: DICKSON:31  :: Prop 4.42 (ii) -> (iii)
  for R being non empty RelStr st R is quasi_ordered &
  (for f being sequence of R ex i,j being Nat st i < j & f.i <= f.j)
  holds for N being non empty Subset of R
  holds min-classes N is finite & min-classes N is non empty;

theorem :: DICKSON:32  :: Prop (iii) -> (i)
  for R being non empty RelStr st R is quasi_ordered &
  (for N being non empty Subset of R
  holds min-classes N is finite & min-classes N is non empty)
  holds R is Dickson;

theorem :: DICKSON:33  :: Corollary 4.44
  for R being non empty RelStr st R is quasi_ordered & R is Dickson
  holds R\~ is well_founded;

theorem :: DICKSON:34 :: Corollary 4.43
  for R being non empty Poset, N being non empty Subset of R st R is Dickson
  holds ex B being set st B is_Dickson-basis_of N, R &
  for C being set st C is_Dickson-basis_of N, R holds B c= C;

definition
  let R be non empty RelStr, N be Subset of R such that
 R is Dickson;
  func Dickson-bases (N,R) -> non empty Subset-Family of R means
:: DICKSON:def 13

  for B being set holds B in it iff B is_Dickson-basis_of N,R;
end;

theorem :: DICKSON:35  :: Proposition 4.45
  for R being non empty RelStr, s being sequence of R st R is Dickson
  ex t being sequence of R st t is subsequence of s & t is weakly-ascending;

theorem :: DICKSON:36
  for R being RelStr st R is empty holds R is Dickson;

theorem :: DICKSON:37   :: Theorem 4.46
  for M, N be RelStr
  st M is Dickson & N is Dickson & M is quasi_ordered & N is quasi_ordered
  holds [:M,N:] is quasi_ordered & [:M,N:] is Dickson;

theorem :: DICKSON:38
for R, S being RelStr st R,S are_isomorphic & R is Dickson & R is quasi_ordered
  holds S is quasi_ordered & S is Dickson;

theorem :: DICKSON:39
  for p being RelStr-yielding ManySortedSet of {0}, z being Element of {0}
  holds p.z, product p are_isomorphic;

registration
  let X be set, p be RelStr-yielding ManySortedSet of X, Y be Subset of X;
  cluster p|Y -> RelStr-yielding;
end;

theorem :: DICKSON:40
  for n being non zero Nat, p being RelStr-yielding ManySortedSet of n
  holds product p is non empty iff p is non-Empty;

theorem :: DICKSON:41
  for n being non zero Nat,
      p being RelStr-yielding ManySortedSet of Segm(n+1),
  ns being Subset of Segm(n+1), ne being Element of Segm(n+1)
  st ns = n & ne = n holds [:product(p|ns), p.ne:], product p are_isomorphic;

theorem :: DICKSON:42  :: Corollary 4.47
  for n being non zero Nat, p being RelStr-yielding ManySortedSet of Segm n
  st for i being Element of Segm n holds p.i is Dickson & p.i is quasi_ordered
  holds product p is quasi_ordered & product p is Dickson;

registration
  let p be RelStr-yielding ManySortedSet of {};
  cluster product p -> non empty;
  cluster product p -> antisymmetric;
  cluster product p -> quasi_ordered;
::$N Dickson Lemma
  cluster product p -> Dickson;
end;

definition
  func NATOrd -> Relation of NAT equals
:: DICKSON:def 14
:::  RelIncl omega;
  {[x,y] where x, y is Element of NAT : x <= y};
end;

theorem :: DICKSON:43
  NATOrd is_reflexive_in NAT;

theorem :: DICKSON:44
  NATOrd is_antisymmetric_in NAT;

theorem :: DICKSON:45
  NATOrd is_strongly_connected_in NAT;

theorem :: DICKSON:46
  NATOrd is_transitive_in NAT;

definition
  func OrderedNAT -> non empty RelStr equals
:: DICKSON:def 15
  RelStr(# NAT, NATOrd #);
end;

registration
  cluster OrderedNAT -> connected;
  cluster OrderedNAT -> Dickson;
  cluster OrderedNAT -> quasi_ordered;
  cluster OrderedNAT -> antisymmetric;
  cluster OrderedNAT -> transitive;
  cluster OrderedNAT -> well_founded;
end;

registration :: 4.48 Dickson's Lemma
  let n be Element of NAT;
  cluster product (n --> OrderedNAT) -> non empty;
  cluster product (n --> OrderedNAT) -> Dickson;
  cluster product (n --> OrderedNAT) -> quasi_ordered;
  cluster product (n --> OrderedNAT) -> antisymmetric;
end;

theorem :: DICKSON:47
 :: Proposition 4.49, in B&W proven without axiom of choice (4.46)
  for M be RelStr st M is Dickson & M is quasi_ordered
  holds [:M,OrderedNAT:] is quasi_ordered & [:M,OrderedNAT:] is Dickson;

:: Omitting Exercise 4.50

theorem :: DICKSON:48  :: Lemma 4.51
  for R, S being non empty RelStr st R is Dickson & S is quasi_ordered &
  the InternalRel of R c= the InternalRel of S &
  (the carrier of R) = (the carrier of S) holds S\~ is well_founded;

theorem :: DICKSON:49 :: Lemma 4.52
  for R being non empty RelStr st R is quasi_ordered holds R is Dickson iff
  for S being non empty RelStr
  st S is quasi_ordered & the InternalRel of R c= the InternalRel of S &
  the carrier of R = the carrier of S holds S\~ is well_founded;

theorem :: DICKSON:50
  NATOrd = RelIncl omega;