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

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.

Tobias

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.