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

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
Duraid Madina wrote:
> 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.*