# [isabelle] Partial definitions of datatypes

Hi

`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
Peter

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