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



Many thanks - this is very good to know. I got over some hurdles, but soon
ran into existential quantifiers. My attempts to get these executable
failed, so I'd like to ask:

  - What can be said in the case of making a 'SOME' executable?

  - Suppose one has a lemma which proves a unique integer exists satisfiying
    some properties, given some preconditions. How could one add an
    appropriate "code lemma"? (To get, say, the function which returns the
    unique integer when the preconditions are met and zero otherwise.)

Thanks again,

	Duraid

	
On Tue, Nov 04, 2008 at 11:47:24AM +0100, Tobias Nipkow wrote:
> 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.