% a characterization of well-foundedness by the absence of infinitely
% descending sequences; well-founded orders.
%
% Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace
% Date: Dec 2004 / Jan 2005

well_foundedness[T: TYPE]: THEORY

BEGIN

  IMPORTING orders[T], monotone_sequences[T], skolemization, closure_ops[T]

  n: VAR nat
  x, y: VAR T
  rel: VAR pred[[T, T]]
  seq: VAR sequence[T]

  no_infinite_descending_sequence: THEOREM
    well_founded?(rel) <=> empty?[sequence[T]](descending?(rel))

  well_founded_is_irreflexive: JUDGEMENT
    (well_founded?) SUBTYPE_OF (irreflexive?[T])

  well_founded_order?(rel): bool =
    well_founded?[T](rel) & transitive?[T](rel)

  well_order_is_well_founded_order: JUDGEMENT
    (well_ordered?[T]) SUBTYPE_OF (well_founded_order?)

  well_founded_order_is_well_founded: JUDGEMENT
    (well_founded_order?) SUBTYPE_OF (well_founded?)

  well_founded_order_is_strict_order: JUDGEMENT
    (well_founded_order?) SUBTYPE_OF (strict_order?)

  transitive_closure_preserves_well_foundedness: JUDGEMENT
    transitive_closure(rel: (well_founded?[T])) HAS_TYPE (well_founded_order?)

END well_foundedness