# Re: [isabelle] fun termination, mutual-recursive datatype

```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

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.