[isabelle] Mixing recursion and corecursion
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"
"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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and