# Re: [isabelle] Mixing recursion and corecursion

```How about defining them not in mutual recursion? This seems to work. (If
someone sees aspects of terrible Isabelle style, by the way, let me know
how to do it properly :))

codatatype 'a llist = LNil | LCons 'a "'a llist"
datatype ms = Const real | MS "(ms Ã real) llist"

(if snd x > snd y then LCons x (ms_add_aux ms_add xs (LCons y ys))
else if snd x < snd y then LCons y (ms_add_aux ms_add (LCons x xs) ys)
apply pat_completeness
apply auto
done

function
ms_add :: "ms â ms â ms"
where
"ms_add (Const x) (Const y) = Const (x + y)"
| "ms_add (Const x) (MS ys) = Const x"
| "ms_add (MS xs) (Const y) = Const y"
apply auto
apply (case_tac a; auto)
apply (case_tac b; auto)
apply (case_tac b; auto)
done

On 1 November 2016 at 21:55, Manuel Eberl <eberlm at in.tum.de> wrote:

> 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))"
>

```

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