*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] Partial definitions of datatypes*From*: Thomas Arthur Leck Sewell <tsewell at cse.unsw.EDU.AU>*Date*: Wed, 24 Sep 2008 11:56:02 +1000 (EST)*Cc*: isabelle-users at cl.cam.ac.uk, Peter Chapman <pc at cs.st-and.ac.uk>*In-reply-to*: <48D8BE49.2010808@in.tum.de>*References*: <BDAEC597-9CC3-4968-801D-01A6D24DE61D@cs.st-and.ac.uk> <48D8BE49.2010808@in.tum.de>

There is a simple, if clunky, alternative.

Yours, Thomas. On Tue, 23 Sep 2008, Tobias Nipkow wrote:

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

**References**:**[isabelle] Partial definitions of datatypes***From:*Peter Chapman

**Re: [isabelle] Partial definitions of datatypes***From:*Tobias Nipkow

- Previous by Date: [isabelle] [Fwd: Re: Help with let expressions]
- Next by Date: Re: [isabelle] Syntax for theory definitions
- Previous by Thread: Re: [isabelle] Partial definitions of datatypes
- Next by Thread: [isabelle] Help with let expressions
- Cl-isabelle-users September 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list