Re: [isabelle] Code generation for picking arbitrary element from finite set



Peter Lammich wrote:
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

[...]

What is the best way to implement such a function ?

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

--
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.