Re: [isabelle] counter example checking from ML

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

Lucas Dixon schrieb:

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

val _ = (Codegen.test_term
  @{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

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:

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?




PGP available:

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