coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: Wellordering types

From: Larry Paulson <Larry.Paulson AT cl.cam.ac.uk>
To: casteran AT labri.fr
Cc: coq-club AT pauillac.inria.fr, isabelle-users AT cl.cam.ac.uk, Larry.Paulson AT cl.cam.ac.uk
Subject: [Coq-Club] Re: Wellordering types
Date: Thu, 25 Nov 2004 11:31:47 +0000
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Organization: Computer Laboratory, University of Cambridge, England

> I am looking for proofs that some (D,<) is well founded by
> using some mapping from D into some wellordering type W(A,B)
> ( (WO A B) in Coq Standard Library.)
>
> Is there some methodology for working on these types (i.e.
> building A and B from D and <)?

For Isabelle/HOL, look in the file Wellfounded_Relations.ML for the inverse
image construction. There are theorems for composing well-foundedness
properties.

There is a simmilar development for Isabelle/ZF.
--
Larry Paulson

[Coq-Club] Wellordering types, casteran
- [Coq-Club] Re: Wellordering types, Larry Paulson