*To*: Brian Huffman <brianh at csee.ogi.edu>*Subject*: Re: [isabelle] mutual recdefs*From*: Peter Sewell <Peter.Sewell at cl.cam.ac.uk>*Date*: Fri, 17 Mar 2006 12:37:08 +0000*Cc*: isabelle-users at cl.cam.ac.uk, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: Message from Brian Huffman <brianh@csee.ogi.edu> of "Sat, 11 Mar 2006 11:52:45 PST." <200603111152.46122.brianh@csee.ogi.edu>

Brian Huffman writes: >You could actually define these functions together using primrec: Since >recursive calls are only made on subterms, you don't really need the full >power of recdef. that's true in this case, indeed. >However, using primrec is complicated by the fact that you have used product >types as arguments to your constructors. This is actually an instance of >indirect recursion, which means you would be required to additionally define >several extra constants which take the product types as arguments. If you >change your datatype definitions so that the constructors have two separate >arguments instead of a pair, then primrec should work just fine. But that seems not to be. As far as I can tell it's impossible to define multiple mutually-recursive functions over the same types, eg the is_val :: "exp => bool" is_exp :: "exp => bool" in the example below, using either primrec or recdef. Is that really the case? Clearly I could encode, with something like is_val_is_exp :: "exp => (bool * bool) " and Tom Ridge points out that I can then prove lemmas characterising the projections of that that look like my original definition. But I don't want to do that encoding unless I have to... thanks, Peter (* here is_val and is_exp define two sub-grammars of the free exp *) theory Out = Main: types ident = "string" datatype exp = Exp_ident "ident" | Exp_unit | Exp_pair "exp" "exp" | Exp_fun "ident" "exp" | Exp_app "exp" "exp" | Exp_foo "exp" consts is_val :: "exp => bool" is_exp :: "exp => bool" primrec "is_val ((Exp_ident x)) = (True)" "is_val (Exp_unit) = (True)" "is_val ((Exp_pair exp exp')) = (((is_val exp) & (is_val exp')))" "is_val ((Exp_fun x exp)) = (((is_exp exp)))" "is_val ((Exp_app exp exp')) = False" "is_val ((Exp_foo val)) = False" "is_exp ((Exp_ident x)) = (True)" "is_exp (Exp_unit) = (True)" "is_exp ((Exp_pair exp exp')) = (((is_exp exp) & (is_exp exp')))" "is_exp ((Exp_fun x exp)) = (((is_exp exp)))" "is_exp ((Exp_app exp exp')) = (((is_exp exp) & (is_exp exp')))" "is_exp ((Exp_foo val)) = (((is_val val)))"

**Follow-Ups**:**Re: [isabelle] mutual recdefs***From:*nipkow

**References**:**Re: [isabelle] mutual recdefs***From:*Brian Huffman

- Previous by Date: Re: [isabelle] How to unify the premises with my rule?
- Next by Date: Re: [isabelle] Help with simplification loops.
- Previous by Thread: Re: [isabelle] mutual recdefs
- Next by Thread: Re: [isabelle] mutual recdefs
- Cl-isabelle-users March 2006 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