Re: [isabelle] Mixing recursion and corecursion



>>  Thanks for tolerating my Isabelle-naivety...


Not at all. I am glad to see a heavy formalizer like yourself looking into Isabelle.  :-)


Best,

  Andrei


________________________________
From: Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
Sent: 02 November 2016 20:23
To: Andrei Popescu
Cc: Manuel Eberl; Dmitriy Traytel; cl-isabelle-users at lists.cam.ac.uk; alexander.krauss at qaware.de
Subject: Re: [isabelle] Mixing recursion and corecursion

Yes, I realised I missed termination when I saw Dmitriy's answer (and also I was thinking "why don't I need to prove a congruence rule?" when I was doing mine - my thought was "maybe Isabelle is smarter than I realised" :)) I totally support the idea of a reminder in the user interface that termination is still missing. Thanks for tolerating my Isabelle-naivety...

On 2 November 2016 at 13:56, Andrei Popescu <A.Popescu at mdx.ac.uk<mailto:A.Popescu at mdx.ac.uk>> wrote:

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<mailto:cl-isabelle-users-bounces at lists.cam.ac.uk> <cl-isabelle-users-bounces at lists.cam.ac.uk<mailto:cl-isabelle-users-bounces at lists.cam.ac.uk>> on behalf of Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk<mailto: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<mailto: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<mailto: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.