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
> 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and