*To*: Randy Pollack <rpollack at inf.ed.ac.uk>*Subject*: Re: [isabelle] parametric typedef?*From*: Makarius <makarius at sketis.net>*Date*: Fri, 16 Oct 2009 19:39:27 +0200 (CEST)*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <19155.27260.4930.942923@locatelli.inf.ed.ac.uk>*References*: <19155.27260.4930.942923@locatelli.inf.ed.ac.uk>*User-agent*: Alpine 1.10 (LNX 962 2008-03-14)

On Mon, 12 Oct 2009, Randy Pollack wrote:

Consider the following (very simplified) example: datatype myDatatype = A | B locale fix_n = fixes n :: nat begin inductive myProperty :: "myDatatype => bool" where mPA : "myProperty A" | mPB : "even n \<Longrightarrow> myProperty B" Now I want to define a new type typedef myType = "{X::myDatatype . myProperty X}" This is not accepted: *** Illegal application of command "typedef" (...) in local theory mode Is there a way to do such a thing, or a reason why it cannot be done?

Notice that leaving locale fix_n, the following is accepted: end (** fix_n **) consts N :: nat interpretation FN:fix_n "N :: nat" done typedef myType = "{X::myDatatype . FN.myProperty X}" by (rule exI[of _ "A"], simp add: FN.mPA)So Isabelle accepts that parametric definition and reasoning aboutmyType is sound. But with this approach I will never be able toinstantiate the constant N.

Makarius

**References**:**[isabelle] parametric typedef?***From:*Randy Pollack

- Previous by Date: Re: [isabelle] Error: Pending sort hypothesis
- Next by Date: Re: [isabelle] Numerical Recipes in Isabelle
- Previous by Thread: [isabelle] parametric typedef?
- Next by Thread: [isabelle] Open research position at ETH Zurich
- Cl-isabelle-users October 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list