# Re: [isabelle] Unable to generate code for ?P = (%x. True)

```Many thanks - this is very good to know. I got over some hurdles, but soon
ran into existential quantifiers. My attempts to get these executable
failed, so I'd like to ask:

- What can be said in the case of making a 'SOME' executable?

- Suppose one has a lemma which proves a unique integer exists satisfiying
some properties, given some preconditions. How could one add an
appropriate "code lemma"? (To get, say, the function which returns the
unique integer when the preconditions are met and zero otherwise.)

Thanks again,

Duraid

On Tue, Nov 04, 2008 at 11:47:24AM +0100, Tobias Nipkow wrote:
> Universal quantifiers are not executable. The only exception are bounded
> quantifiers of the form "Q x : A" where A is one of two kinds of sets:
> either a set interval, eg {0..n::nat}, or a set coming from a list, eg
> "set xs". Formulas "ALL x. x < n --> ..." are not recognized as
> executable. You have to rewrite them into the set interval form:
>
> definition
>   m_cond :: "nat => (nat => nat) => bool" where
>   "m_cond n mf =
>     ((ALL i : {0..n}. 0 < mf i) &
>      (ALL i : {0..n}. ALL j : {0..n}. i ~= j
>    --> gcd (mf i, mf j) = 1))"
>
> Now
>
> value "m_cond 1 (%x. 3)"
>
> returns "false".
>
> Note: you must import the theory "Executable_Set" for this to work!
>
> Regards
> Tobias
>
> > I was expecting a bool from the following, but instead got the error in the subject:
> >
> > ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
> > theory odd imports Primes begin
> >
> > definition
> >   m_cond :: "nat => (nat => nat) => bool" where
> >   "m_cond n mf =
> >     ((ALL i. i <= n --> 0 < mf i) &
> >      (ALL i j. i <= n & j <= n & i ~= j
> >    --> gcd (mf i, mf j) = 1))"
> >
> > value "m_cond 1 (%x. 3)"
> > ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
> >
> > Am I doing something evil here?
> >
> > 	Duraid
> >

```

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