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.

Cheers,
Dmitriy

Attachment: Scratch.thy
Description: Binary data



> On 1 Nov 2016, at 21:55, Manuel Eberl <eberlm at in.tum.de> 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.