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

```Here is how you would go about it if you wanted to make "ALL i<=n"
executable directly. You define your own recursive function all_upto,
prove that it behaves the same as ALL, and make that a code lemma that
replaces such bounded quantifiers by all_upto:

primrec all_upto :: "(nat  bool)  nat  bool" where
"all_upto P 0 = P 0" |
"all_upto P (Suc n) = (P(Suc n) & all_upto P n)"

lemma all_Suc: "(ALL i<=Suc n. P i) = (P(Suc n) & (ALL i<=n. P i))"
by (auto simp:le_Suc_eq)

lemma [code unfold]: "(ALL i<=n. P i) = all_upto P n"

Now you don't need Executable_Set (and need to change m_cond only a little).

Regards
Tobias

PS If you want to extract efficient code, import Efficient_Nat: it
implements nat by int.

> 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.