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



I strongly suspect it cannot be done in the logic. Go for Stefan's solution.

Tobias

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





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