*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] Problems with datatype definition*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Sun, 24 May 2009 20:53:59 +0200*Cc*: isabelle-users at cl.cam.ac.uk, René Thiemann <rene.thiemann at uibk.ac.at>*In-reply-to*: <cc2478ab0905221754y682158f8j31af586acd6e7155@mail.gmail.com>*References*: <5FE2643D-07FD-4C36-B25E-BF0C0C0315E6@uibk.ac.at> <cc2478ab0905221754y682158f8j31af586acd6e7155@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.19 (Macintosh/20081209)

It often works to define a supertype. The example below can be encoded as datatype 'a foo = Bar 'a | Com' "'a foo" nat where "Com' f n" encodes "Com (Some(...(Some f)...))", with n nested Somes. Fine-grained constraints are expressed as propositions on this type. Tobias Brian Huffman schrieb: > 2009/5/20 René Thiemann <rene.thiemann at uibk.ac.at>: >> Dear all, >> >> the following datatype definition is not accepted in Isabelle/HOL, >> presumably since the parameter of foo has been changed to "'a option". >> >> datatype 'a foo = Bar 'a | Com "'a option foo" >> >> Is there some known workaround for this problem? > > This is an instance of "nested" or "non-regular" recursion, which is > not supported by Isabelle's datatype package. I think you can define > those kinds of datatypes in Coq, but Isabelle has a much less > sophisticated type system that makes working with nested recursive > datatypes very difficult. > > The first problem is, what would an induction rule for type 'a foo > look like? Here's a first try: > > lemma foo_induct: > assumes "ALL a. P (Bar a)" > assumes "ALL x. P x --> P (Com x)" > shows "ALL x. P x" > > But the above rule doesn't work because it is not type-correct. > Because of the nested recursion, the predicate in the inductive > hypothesis needs to have a different type than the one in the > conclusion. In Coq, I think this can work by giving P a polymorphic > type like "forall a, foo a -> Prop". But in Isabelle you can't talk > about polymorphic types in this way. > > The other (related) problem is how to define recursive functions over > a nested recursive datatype. Here's a definition you might like to be > able to write: > > primrec "size :: 'a foo => nat" where > "size (Foo a) = 0" | > "size (Com x) = Suc (size x)" > > The problem is that the recursive call to "size" on the rhs is at a > different type. This means that it is impossible to translate this > definition into a non-recursive one that uses a fixed-point > combinator; at what type would you take the fixed-point? In Coq, the > workaround would be to define a recursive value of type "forall a. foo > a -> nat", with the type parameter made explicit. > > So basically, unless Isabelle's type system is extended with rank-2 > polymorphism, these kinds of definitions will never be supported. The > only workaround I can think of would be to use something like ZF set > theory to encode everything in a single Isabelle type, allowing you to > essentially bypass Isabelle's type system altogether. > > - Brian

**References**:**[isabelle] Problems with datatype definition***From:*René Thiemann

**Re: [isabelle] Problems with datatype definition***From:*Brian Huffman

- Previous by Date: Re: [isabelle] problem with opening proof
- Next by Date: [isabelle] 2nd Cfp: PCC09
- Previous by Thread: Re: [isabelle] Problems with datatype definition
- Next by Thread: Re: [isabelle] Problem with local proof
- Cl-isabelle-users May 2009 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