well_fnd Theory
Defines predicate saying that a binary relation over some type
is well-founded.
Well-foundedness is phrased in terms of a `course of values'
induction principle, since this is more useful constructively
than alternative formulations (e.g. saying that there are
no infinite descending chains, or saying that every non-empty
subset has a minimal element). NB: constructively, these
alternative formulations are not equivalent.
Lemmas and tactics are introduced for induction on the rank of
an expression (`inverse image induction'). One deficiency of Nuprl's
type theory is that in some situations (notably when proving well-formedness
goals) lemmas are unusable, and instead one must resort to using
tactics that reproduce equivalent sequences of primitive rules.
The theorem `inv_image_ind_tp' provides a template for such a tactic
that mirrors the `inv_image_ind_a' lemma.
Summary of Definitions
Typed Definitions
-
wellfounded
*1
-
Main Theorems
-
inv_image_ind_a
*13
-
-
inv_image_ind_tp
*92
-
-
inv_image_ind
*1
-
-
wellfounded_functionality_wrt_iff
*14
-
-
wellfounded_functionality_wrt_implies
*8
-
Listing
Last modified February 24th, 1995
Paul Jackson /
jackson@cs.cornell.edu