Email Gateway (Aug 22 2022 at 14:27): Email Gateway (Aug 22 2022 at 14:27):From: Ramana Kumar <Ramana.Kumar@cl.cam.ac.uk>
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...
Email Gateway (Aug 22 2022 at 14:29):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Thanks for tolerating my Isabelle-naivety...
Not at all. I am glad to see a heavy formalizer like yourself looking into Isabelle. :-)
Best,
Andrei
Email Gateway (Aug 22 2022 at 14:31):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
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"
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))"
How can I define a function like that? The mutual recursion combined
with corecursion seems to make it pretty difficult.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 14:34):From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Manuel,
this is nested recursion through a codatatype. To define your function you will need two steps, first the auxiliary function by primitive corecursion on llist (made higher-order to account for the recursive call) and then the actual function ms_add.
The attached theory file contains the definition. To prove the function terminating, size won’t work (nat is not a good fit for codatatypes). Instead I define the well founded subterm relation inductively and use it as the decreasing measure. Moreover, a congruence rule for the auxiliary function is needed—pardon my ugly (auto; sledgehammer) proof for this.
Cheers,
Dmitriy
Scratch.thy
Email Gateway (Aug 22 2022 at 14:38):From: Ramana Kumar <Ramana.Kumar@cl.cam.ac.uk>
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
Email Gateway (Aug 22 2022 at 14:39):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
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
Last updated: Apr 25 2024 at 08:20 UTC