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



Awesome. Many thanks Brian :)

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.