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.