[isabelle] Partial definitions of datatypes


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.