[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 MHonArc.