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
Conj "form" "form"
Disj "form" "form"
and for another
Compound = neg "form"
| Impl "form" "form"
so the datatype would be
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and