Re: [isabelle] Mixing recursion and corecursion



Hi Ramana,


All good, but you also need to prove termination for ms_add, which requires some ingenuity -- see Dmitriy's answer.

Otherwise you get only partial-function behavior: the rules for ms_add would be conditioned by membership to its domain

(as shown by "find_theorems ms_add").


Btw, I think it would be a good idea if the function package reminded the user that termination has not been proved.

(CCed is Alex Krauss, the function package author -- whom I greet with this occasion.  :-)  )


Best,

  Andrei


________________________________
From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
Sent: 01 November 2016 22:00
To: Manuel Eberl
Cc: cl-isabelle-users at lists.cam.ac.uk
Subject: [SPAM: 3.500] 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.