*To*: Duraid Madina <duraid at kinoko.c.u-tokyo.ac.jp>*Subject*: Re: [isabelle] Unable to generate code for ?P = (%x. True)*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 05 Nov 2008 09:20:48 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <20081104174313.GA55368@kinoko.c.u-tokyo.ac.jp>*References*: <20081103164348.GB50946@kinoko.c.u-tokyo.ac.jp> <4910283C.6030804@in.tum.de> <20081104174313.GA55368@kinoko.c.u-tokyo.ac.jp>*User-agent*: Thunderbird 2.0.0.16 (Macintosh/20080707)

> Many thanks - this is very good to know. I got over some hurdles, but soon > ran into existential quantifiers. EX is completely dual to ALL, also w.r.t. code generation. > - What can be said in the case of making a 'SOME' executable? Tricky. Of course in general you cannot. But even if everything inside the SOME is executable, non-uniqueness (esp for "SOME x. False") almost always rule out replacing the some by a logically equivalent term. You usually have to resort to extra-logical means. For example, in our Jinja work we implemented "%S. SOME x. x : S" by the ML function "hd" on lists: definition some_elem :: "'a set => 'a" "some_elem == (%S. SOME x. x : S)" consts_code "some_elem" ("hd") The const_code statement is outside the logic and it is your responsibility that hd is a correct implementation of some_elem! > - 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.) In that case I would avoid working with SOME in the first place. Use THE. And if you want to generate code: don't even use THE, define the function explicitly. For example, if the element can be found by a search over some interval: fun search where "search i j = (if i<j then if p i then f i else search (i+1) j else 0)" Then prove that search has the properties you want and use search where you would have used SOME. Tobias > 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

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

- Previous by Date: Re: [isabelle] interpretations and lambda terms
- Next by Date: Re: [isabelle] Unable to generate code for ?P = (%x. True)
- 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