Re: [isabelle] Partial definitions of datatypes

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:
> 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.