*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] mutual recdefs*From*: Brian Huffman <brianh at csee.ogi.edu>*Date*: Sat, 11 Mar 2006 11:52:45 -0800*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <E1FHlJn-0002zf-00@mta1.cl.cam.ac.uk>*References*: <E1FHlJn-0002zf-00@mta1.cl.cam.ac.uk>*User-agent*: KMail/1.8

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. 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. - Brian On Friday 10 March 2006 09:22, Peter Sewell wrote: > Another naive question: I'd like to define several mutually recursive > functions, eg (roughly) as is_val and is_exp in the example below. > Looking in the tutorial I only see single examples - how would this be > most nicely done? (Presumably I could make a new disjoint sum type > and work over that, but that seems ugly - though some plumbing of size > functions is going to be needed somewhere.) > > ta, > Peter > > > 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" > > and C = > Ctx_pairL "exp" > > | Ctx_pairR "exp" > | Ctx_appL "exp" > | Ctx_appR "exp" > > and Jop = > JO_red "exp*exp" > and judgement = > judgement_Jop "Jop" > > consts is_val :: "exp => bool" > is_C :: "C => bool" > is_Jop :: "Jop => bool" > is_exp :: "exp => bool" > recdef is_val "measure (% x . size x)" > "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" > recdef is_C "measure (% x . size x)" > "is_C (Ctx_pairL ( exp ) ) = (((is_exp exp)))" > "is_C (Ctx_pairR ( val ) ) = (((is_val val)))" > "is_C (Ctx_appL ( exp ) ) = (((is_exp exp)))" > "is_C (Ctx_appR ( val ) ) = (((is_val val)))" > recdef is_Jop "measure (% x . size x)" > "is_Jop (JO_red ( e , e' ) ) = (((is_exp e) & (is_exp e')))" > recdef is_exp "measure (% x . size x)" > "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:*Peter Sewell

**References**:**[isabelle] mutual recdefs***From:*Peter Sewell

- Previous by Date: Re: [isabelle] Sets
- Next by Date: Re: [isabelle] cardinality
- Previous by Thread: [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