[isabelle-dev] [isabelle] counter example checking from ML

[Lucas Dixon]

Hi following this up a bit,

I've noticed that, for the examples I've been looking at, the 
counter-example finder is now much less successful than it used to be. I 
need to crank up the iterations a lot.

I was previously able to use it with an input of up to size 5, with 5 
iterations on over 40,000 cases without any false conjectures slipping 
through. I thought this was great, but perhaps it was a feature of the 
domain I was looking at (equations over datatypes and simple recursive 
functions on them).

So, I'm now wondering if there is there a way to provide a deterministic 
  instance generator rather than the random one currently being used (is 
this what happened before?) My feeling is that the first few cases for 
each variable is what I'm after.

Also, to make programatic changes to the configuration of tools, we need 
to have the contextual data available, so if its OK, I'll export that 
also in the signature.

best,
lucas

Florian Haftmann wrote:
> Hi Lucas,
> 
> note that the convention on the Codegen.test_term interface has changed:
> 
> ML {* Codegen.test_term @{context} @{term "%n. n = Suc n"} 2 *}
> 
> The proposition is now given as an abstraction containing *no* free 
> variables.
> 
> Hope this helps
>     Florian
> 
> Lucas Dixon schrieb:
>> Hello,
>>
>> I have questions about using isabelle quickcheck/code generation.
>> I used to quite happily use it for various things but it seems that the
>> input is now stricter than it used to be (in 2008) - extra dependencies
>> between the input term and context - and I've not yet been able to
>> figure it out.
>>
>> (Using Isabelle 32575:bf6c78d9f94c)
>>
>> I'm trying to use
>> "Codegen.test_term : Proof.context -> term -> int -> term list option"
>> (is this the best ML function to be using? do tell me of a better higher
>> level one)
>>
>> Trying to do what I used to do in ML...
>>
>> ML{*
>> val _ = (Codegen.test_term
>>   @{context}
>>   @{term "(b :: int) + a = b"});
>> *}
>> ;
>>
>> Produces the error:
>>
>> *** Error (line 19):
>> *** Value or constructor (b) has not been declared
>> *** Error (line 19):
>> *** Value or constructor (a) has not been declared
>> *** Error (line 19):
>> *** Value or constructor (b) has not been declared
>> *** Exception- ERROR of "Static Errors" raised
>> *** val ctxt2 = <context> : Context.proof
>> *** Exception- TOPLEVEL_ERROR raised
>> *** At command "ML" (line 11 of
>> "/afs/inf.ed.ac.uk/user/l/ldixon/Scratch.thy").
>>
>> My first guess was that all terms are now implicitly dependent on the
>> context they live in, so perhaps I need to add the free variables to the
>> context, - the types should already be there. The quick undisciplined
>> way, I think, is:
>>
>> ML{*
>> val (_,ctxt2) = @{context} |> Variable.add_fixes ["b", "a"];
>> val _ = (Codegen.test_term ctxt2 @{term "(b :: int) + a = b"});
>> *}
>> ;
>>
>> I can do some term manipulation and properly pull out the names of the
>> frees from the term - but I would expect the above to work... but it
>> also gives the same error.
>>
>> This gives rise to further questions:
>>
>> - how to I inspect the context? (I remember this from the Isabelle dev
>> workshop, but couldn't find it in the online example theories)
>>
>> - what's the right way to quickly make the context that would get from a
>> statement like "lemma ..."? i.e. the context of a term, automatically
>> putting in the types and frees? (my first guess was to use
>> Variable.focus - but that seems to ignore free vars and types)
>>
>> - how can I use quickcheck (or nitpick) from the ML level? and I would
>> love this to be in the Isabelle cookbook (shall I write an entry, once I
>> find out how to use it?)
>>
>> - What is the hidden implicit dependency between the term given to
>> Codegen.text_term, and the context?
>>
>> thanks,
>> lucas
>>
> 


-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.