*To*: René Thiemann <rene.thiemann at uibk.ac.at>*Subject*: Re: [isabelle] Problems with datatype definition*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Fri, 22 May 2009 17:54:15 -0700*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <5FE2643D-07FD-4C36-B25E-BF0C0C0315E6@uibk.ac.at>*References*: <5FE2643D-07FD-4C36-B25E-BF0C0C0315E6@uibk.ac.at>*Sender*: huffman.brian.c at gmail.com

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

**Follow-Ups**:**Re: [isabelle] Problems with datatype definition***From:*Tobias Nipkow

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

- Previous by Date: Re: [isabelle] problem with opening proof
- Next by Date: Re: [isabelle] problem with opening proof
- Previous by Thread: [isabelle] Problems with datatype definition
- Next by Thread: Re: [isabelle] Problems with datatype definition
- 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