*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] fun termination, mutual-recursive datatype*From*: John Wickerson <jpw48 at cam.ac.uk>*Date*: Thu, 17 May 2012 22:53:53 +0100*In-reply-to*: <CAAMXsibenvGAqnR=v4wuuX+NCuxsjbNkc1Fuj77hY3TzeCHKVw@mail.gmail.com>*References*: <D2147C6C-3081-4A59-A1F1-0AD7A5CACC5A@cam.ac.uk> <CAAMXsibenvGAqnR=v4wuuX+NCuxsjbNkc1Fuj77hY3TzeCHKVw@mail.gmail.com>

Why must the definition of \<circ> be unfolded? I mean, why does primrec throw an "Unknown variable foo_jack" otherwise? (I'm finding this problem with several of my other primrec definitions.) Thanks, john On 17 May 2012, at 16:19, Brian Huffman wrote: > On Thu, May 17, 2012 at 4:46 PM, John Wickerson <jpw48 at cam.ac.uk> wrote: >> Dear Isabelle, >> >> I am using a groovy mutually-recursive datatype a bit like the following one: >> >>> datatype jack = A "int" | B "jill" >>> and jill = C "int => jack" "int list" >> >> I would like to write a (mutually-recursive) function over my datatype, something like this: >> >>> datatype jack = A "int" | B "jill" >>> and jill = C "int => jack" "int list" >>> >>> fun >>> foo_jack :: "jack => int" and >>> foo_jill :: "jill => int" >>> where >>> "foo_jack (A n) = n" >>> | "foo_jack (B j) = foo_jill j" >>> | "foo_jill (C f ns) = listsum (map (foo_jack \<circ> f) ns)" >> >> But the <fun> command says: "Could not find lexicographic termination order." Does anybody know how one might prove that such a function terminates? > > If you unfold the function composition operator \<circ>, then the > definition works with primrec: > > primrec > foo_jack :: "jack => int" and > foo_jill :: "jill => int" > where > "foo_jack (A n) = n" > | "foo_jack (B j) = foo_jill j" > | "foo_jill (C f ns) = listsum (map (\<lambda>n. foo_jack (f n)) ns)" > > Infinitely-branching datatypes are one area where primrec still holds > a lead over the function package. > > - Brian

**References**:**[isabelle] fun termination, mutual-recursive datatype***From:*John Wickerson

**Re: [isabelle] fun termination, mutual-recursive datatype***From:*Brian Huffman

- Previous by Date: Re: [isabelle] "isabelle make" in windows-RC2
- Next by Date: [isabelle] Dark jEdit color themes
- Previous by Thread: Re: [isabelle] fun termination, mutual-recursive datatype
- Next by Thread: [isabelle] Isabelle2012-RC3 available for testing
- Cl-isabelle-users May 2012 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