Re: [isabelle] antiquotations

On Fri, 8 Feb 2008, Jeremy Dawson wrote:

> Mostly my problems are something do to with theories.  I don't know if 
> the problems I've faced today are because of theories or not, but I 
> think it is quite likely.  But I waste an enormous amount of time trying 
> to cope with things that don't work as expected.

The general advice is to let Isar take over control as much as possible, 
while avoiding raw ML accesses (in particular operations with unclear 
theory/proof context).

In particular:

  - Use ProofGeneral by default.
  - Always work within a theory body, if a theory is required.  Do not 
    rely on accidental theory states from previous use_thy etc.
  - Use ML antiquotions as much as possible, because here the context is 
    checked statically at compile time.

> The latest example is contained in the attached theory file. For some 
> reason the ML expression bool_axioms RL [fun_cong] produces an empty 
> list of results when it appears in the theory file being loaded.
> After the theory file is modified in the way shown (ie not using 
> bool_axioms RL [fun_cong]) it loads OK.  Then, after that, the 
> expression bool_axioms RL [fun_cong] returns exactly the results 
> expected.  Why does the same ML expression behave differently at 
> different points ?

This is a good example why proper contexts matter.  The bool_axioms list 
is bound at the ML toplevel in a situation *before* certain type class 
instantiations in your theory.  For the resolution to work out, these type 
arities need to be present in the theory.  Your ML code fails to produce 
any result here, because it references bool_axioms in the raw ML 
environment, without going through the Isar layer, which would have 
transferred the result as required.

Using a proper ML antiquotation makes things work as expected:

  @{thms bool_axioms} RL [fun_cong]

It is important to keep in mind that the ML environment is not the real 
thing, just a low-level view on the implementation platform.


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