Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] parametric typedef?

Email Gateway (Aug 18 2022 at 14:11):

From: Randy Pollack <rpollack@inf.ed.ac.uk>
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 about
myType is sound. But with this approach I will never be able to
instantiate the constant N.

Randy

Email Gateway (Aug 18 2022 at 14:11):

From: Makarius <makarius@sketis.net>
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

Last updated: May 06 2024 at 12:29 UTC