Email Gateway (Aug 18 2022 at 10:27): Email Gateway (Aug 18 2022 at 10:27):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,
I want to use the isabelle 2005 code generator to get code for a
function that picks an arbitrary element with some property P from a
finite set S, i.e. something like:
pick :: "('a => bool) => 'a set => 'a option"
with
(pick P S = Some e) ==> (e \in S \and P e) and
(\exists e\in S. P e) ==> pick P S \noteq None
I have tried the following:
Using ExecutableSet.thy to get representation of sets as lists
Using a definition of pick involving SOME, i.e. pick P S == if \exists
e\in S. P e then Some (SOME e. e\in S \and P e) else None.
This does not work, I get an error from the code generator that it
cannot generate code for SOME.
Using fold to define pick. This also does not work, I get an error
from the code generator that it cannot handle THE (used in the
definition of fold)
What is the best way to implement such a function ?
Thanks in advance for any hints
Peter Lammich
Email Gateway (Aug 18 2022 at 10:27):From: Stefan Berghofer <berghofe@in.tum.de>
Peter Lammich wrote:
Hi Peter,
if everything else fails, you can always provide an ad-hoc ML implementation
of your function, e.g.
consts_code
"pick" ("\<module>pick")
attach {*
fun pick P [] = error "pick"
| pick P (x :: xs) = if P x then x else pick P xs;
*}
A similar trick is used in HOL/MicroJava/BV/BVExample.thy for implementing
the function some_elem, which selects an arbitrary element from a set.
Greetings,
Stefan
Email Gateway (Aug 18 2022 at 10:27):From: Tobias Nipkow <nipkow@in.tum.de>
I strongly suspect it cannot be done in the logic. Go for Stefan's solution.
Tobias
Peter Lammich schrieb:
Last updated: May 03 2024 at 08:18 UTC