Re: [isabelle] counter example checking from ML



On Wed, 16 Sep 2009, Lucas Dixon wrote:

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)

The context merely maintains arbitrary data of certain modules. You can only print certain aspects of whatever might be there, using operations that the corresponding modules offer. E.g. you can print the important data provided by Variable/Assumption using print facitlities of ProofContext, say like this:

  ML_command "set ProofContext.debug"

potentially also this:

  ML_command "set ProofContext.verbose"

Then the ML pretty printer for type Proof.context (in stable Poly/ML 5.2.1) should show you fixes/assumes and some more. E.g.

  ML_val {* @{context} *}


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

For testing it is most convenient to have Isar do it for you, e.g. like this:

  lemma fixes x y :: nat assumes "x = y" shows "y = x"
    ML_prf {* val my_ctxt = @{context} *}


my first guess was to use Variable.focus - but that seems to ignore free vars and types

Focus is very special, to look under !! binders of rules and goals. To get the outermost entities (free variables) into the context, you merely need Variable.declare_term, or the slightly stronger version Variable.auto_fixes.

Explicit Variable.add_fixes is also quite common, although the type constraints need to be introduced separately, either via Variable.declare_term or the weaker version Variable.declare_constraints.

Chapter 4 of the "implementation" manual provides some further clues how things work, and which are the main operations.


	Makarius





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