[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
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