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"
by (induct n) (simp_all add:all_Suc)

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


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

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.