Re: [isabelle] antiquotations

Makarius wrote:
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.

Thanks for this - I think I understand this point.
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.

However I don't understand this - as I said in my earlier email, exactly the same ML code _does_ produce the desired result later on. So why does the _same_ ML expression behave _differently_ at different points ? Both the points where the ML expression bool_axioms RL [fun_cong] is used occur _after_ the point where fun is shown to be in the
axclass boolean_class  (I understand that this is what the problem was).
Using a proper ML antiquotation makes things work as expected:

  @{thms bool_axioms} RL [fun_cong]

I gather your point is that

@{thms bool_axioms}

transfers bool_axioms to the current theory. But this is exactly what I don't want! My complaint is that the _same_ ML expression bool_axioms RL [fun_cong] behaves differently between (a) where I put it in the theory file, where it doesn't work, and (b) when I use it later, in trying to debug the problem. I want the same expression to have the same meaning when I am trying to debug it as the meaning it has when it fails to work! Incidentally, some years ago I discovered that thms "bool_axioms" retrieves the theorems bool_axioms, after transferring them to the current theory. I asked how to retrieve named theorem(s) without transferring them to the current theory - no one then seemed to know. Does anyone know how to do this?

Further questions from my previous email, whose answers would, I hope, help me to understand the complexities of theories in Isar:

theory_of_thm (hd bool_axioms); produces a different result inside the Isar file
from the result it gives afterwards.  Why is this?

If I understand correctly the_context () returns the current theory as at the point where it is executed. Is that correct? The difficulty in using Isar seems to be that the current theory keeps on changing, much more than with typical .ML proof files. Is this correct?
So far as I understood the previous emails,
ML {* XXX the_context () *} and ML {* XXX at {theory} *} would only return a different result if the code represented by XXX actually changed the current theory. Is that correct?

A further question from a previous email (the answer given then was to use a different function) : bind_thm(s) seems to sometimes work (in the sense of storing a theorem in the database so that it can be effectively retrieved later). Why is this? What is the difference between bind_thm and the function I was told to use (ie, PureThy.add_thmss)?

Finally, is all this stuff documented anywhere?

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.

I'm not sure what this means, but it is the language in which enormous amounts of Isabelle proofs are and have been written - and it is still the only language for doing lots of things (including some fairly mundane things, as my theory file showed) in Isabelle.


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