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