Re: [isabelle] parametric typedef?



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?

HOL typedef can (and will) be "localized", but the rhs must not depend on term parameters of the local context, otherwise HOL would magically acquire a form of dependent types. (Dependency on assumptions is no problem.)


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 about myType is sound. But with this approach I will never be able to instantiate the constant N.

In principle such underspecified global constants can instantiated later by theory interpretation, in the style of the AWE tool from Bremen.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.