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.

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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.