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.
Peter Lammich schrieb:
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"
(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
This archive was generated by a fusion of
Pipermail (Mailman edition) and