Re: [isabelle] Mixing recursion and corecursion

Hi Manuel,

this is nested recursion through a codatatype. To define your function you will need two steps, first the auxiliary function by primitive corecursion on llist (made higher-order to account for the recursive call) and then the actual function ms_add.

The attached theory file contains the definition. To prove the function terminating, size wonât work (nat is not a good fit for codatatypes). Instead I define the well founded subterm relation inductively and use it as the decreasing measure. Moreover, a congruence rule for the auxiliary function is neededâpardon my ugly (auto; sledgehammer) proof for this.


Attachment: Scratch.thy
Description: Binary data

> On 1 Nov 2016, at 21:55, Manuel Eberl <eberlm at> wrote:
> Hallo,
> I have the following datatype:
> datatype ms = Const real | MS "(ms à real) llist"
> I now want to define two mutually a function ms_add that combines two
> values of type ms in the following way:
> ms_add :: "ms â ms â ms" and
> ms_add_aux :: "(ms à real) llist â (ms à real) llist â (ms à real) llist"
> where
>  "ms_add (Const x) (Const y) = Const (x + y)"
> | "ms_add (MS xs) (MS ys) = MS (ms_add_aux xs ys)"
> | "ms_add_aux LNil ys = ys"
> | "ms_add_aux xs LNil = xs"
> | "ms_add_aux (LCons x xs) (LCons y ys) =
>     (if snd x > snd y then LCons x (ms_add_aux xs (LCons y ys))
>      else if snd x < snd y then LCons y (ms_add_aux (LCons x xs) ys)
>      else LCons (ms_add (fst x) (fst y), snd x) (ms_add_aux xs ys))"
> How can I define a function like that? The mutual recursion combined
> with corecursion seems to make it pretty difficult.
> Cheers,
> Manuel

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