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