% pointwise orders on functions whose domain is finite
% their strict part preserves well-founded orders
%
% Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace
% Date: Dec 2004

finite_pointwise_orders[D, R: TYPE]: THEORY

BEGIN

ASSUMING

  domain_finiteness: ASSUMPTION is_finite_type[D]

ENDASSUMING

  IMPORTING
    numbers_infinite,         % to discharge a TCC of infinite_pigeonhole
    pointwise_orders[D, R],
    well_foundedness,
    infinite_pigeonhole[nat, D],
    integer_enumerations[nat]

  d: VAR D
  r: VAR R
  n: VAR nat
  rel: VAR (transitive?[R])
  seq: VAR [nat -> [D -> R]]
  g: VAR (preserves[nat, nat](<, <))  % enumerates the subsequence indices

  % an infinite sequence of elements from the finite type D must contain
  % a mono-chromatic subsequence
  infinite_pigeonhole: LEMMA
    FORALL (f: [nat -> D]): EXISTS d, g: FORALL n: f(g(n)) = d

  descending_exists: LEMMA
    descending?(strictly_pointwise(rel))(seq) =>
      EXISTS d: rel(seq(n + 1)(d), seq(n)(d))

  descending_reflexive_closure: LEMMA
    descending?(strictly_pointwise(rel))(seq) =>
      descending?[R](reflexive_closure[R](rel))(LAMBDA n: seq(n)(d))

  pointwise_pigeonhole: LEMMA
    descending?(strictly_pointwise(rel))(seq) =>
      EXISTS d, g: descending?(rel)(LAMBDA n: seq(g(n))(d))

  strictly_pointwise_well_founded_order: JUDGEMENT
    strictly_pointwise(rel: (well_founded_order?[R])) HAS_TYPE
      (well_founded_order?[[D -> R]])

END finite_pointwise_orders