*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] Unable to generate code for ?P = (%x. True)*From*: Duraid Madina <duraid at kinoko.c.u-tokyo.ac.jp>*Date*: Wed, 5 Nov 2008 02:43:13 +0900*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4910283C.6030804@in.tum.de>*References*: <20081103164348.GB50946@kinoko.c.u-tokyo.ac.jp> <4910283C.6030804@in.tum.de>*User-agent*: Mutt/1.4.2.1i

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

**Follow-Ups**:**Re: [isabelle] Unable to generate code for ?P = (%x. True)***From:*Tobias Nipkow

**References**:**[isabelle] Unable to generate code for ?P = (%x. True)***From:*Duraid Madina

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

- Previous by Date: Re: [isabelle] Unable to generate code for ?P = (%x. True)
- Next by Date: Re: [isabelle] interpretations and lambda terms
- Previous by Thread: Re: [isabelle] Unable to generate code for ?P = (%x. True)
- Next by Thread: Re: [isabelle] Unable to generate code for ?P = (%x. True)
- Cl-isabelle-users November 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list