Re: [isabelle] Partial definitions of datatypes

There is a simple, if clunky, alternative.

You could simply declare your new type (unfortunately, needing new names for all the constructors), then declare an injection function that maps from your new type to the subset of the old type that you are interested in representing. You could then do all your logic on injections of values in the new type.

It's the lowest-budget solution, and will probably allow you to get the job done, but I suppose it isn't pretty. There may be a way to hide the injection function and the renaming of the constructors using locales.


On Tue, 23 Sep 2008, Tobias Nipkow wrote:

Peter, this sounds rather fanciful and I don't think there is an easy
solution. You cannot add constructors to a datatype (and you even want
to remove one). The best I can think of is to make the datatype more

datatype 'a form = At "nat" | Compound 'a "'a form list"

so you can instantiate it:

datatype condis = Con | Dis
types cd_form = "condis form"

However, this yields n-ary conjunctions and disjunctions; which becomes
awkward for negation ;-) So you would need an additional predicate for
wellformed formulae of certain kinds.


Peter Chapman schrieb:

Is there a way to partially define a datatype?  Or, is there a way to
define it generally at one point, and then redefine/specialise it later on?

I have some results which only require that I define my datatype as

datatype form = At "nat"
                          | Compound "string" "form list"

i.e. that I define formulae as atomic and compound, and can distinguish
between them.  I would like to then specialise this datatype somewhat,
so for a particular application I may wish to have

Compound = Conj "form" "form"
                      | Disj "form" "form"

so then the datatype would be

At "nat"
Conj "form" "form"
Disj "form" "form"

and for another

Compound = neg "form"
                      | Impl "form" "form"

so the datatype would be

At "nat"
neg "form"
Impl "form" "form"

Obviously, I'd like the original results which I proved to hold for the
new datatype, which is a specialisation of the old one.  Essentially, I
would like to plug in a more complete version of what it means for a
formula to be compound.

I've looked at the documentation about type classes and locales, but I
don't see how that would apply here: I'm not adding new operations to a
theory, just new constructors to a datatype.

Many thanks


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