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"

function ms_add_aux where
  "ms_add_aux ms_add LNil ys = ys"
| "ms_add_aux ms_add xs LNil = xs"
| "ms_add_aux ms_add (LCons x xs) (LCons y ys) =
     (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)
      else LCons (ms_add (fst x) (fst y), snd x) (ms_add_aux ms_add 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 (MS xs) (MS ys) = MS (ms_add_aux ms_add xs ys)"
| "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.