Re: [isabelle] antiquotations



Makarius wrote:
Having studied the recent threads on the "effect of use_thy", "antiquotations" etc. here is a summary in my own words, together with some additional hints on how to avoid problems with old ways of doing things, and moving on towards more powerful concepts.

* The raw interactive ML toplevel is mostly obsolete. After many years of the two toplevels side-by-side, we have finally passed the turning point where everything is Isar, and ML is smoothly integrated into that. Proper context-dependent antiquotations are just one benefit from this principle, and typing additional ML {* *} should be a small price to pay in current Proof General (adding a key binding to produce that wrapping should be trivial anyway).
Unfortunately the integration isn't "smooth". In fact I'm working on a project now where it is demanded that everything is in Isar, so I have to try to work in this way. And it is incredibly frustrating, because things seem to sometimes work, and sometimes not, with no apparent reason, seemingly randomly.

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. What is a simple job when I'm doing proofs using "the raw interactive ML toplevel" becomes slow and frustrating when I try to use Isar as much as possible, while using ML for the things not available in Isar.

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 ?

Why is this?  I suspect it is to do with theories, and noted that
theory_of_thm (hd bool_axioms); produces a different result inside the Isar file
from the result it gives afterwards.  Why is this?

I waste an enormous amount of time trying to cope with things that don't work as expected. When a proof works fine at the terminal, but doesn't work when you put it into a theory file and load that theory file, debugging the situation is very difficult. (This is quite apart from the fact that debugging Isar is naturally more difficult than debugging ML, because when you load an ML proof file that fails, the theorems proved prior to the failure are there for you to use).

Something that is a simple job when I'm doing proofs solely in ML becomes slow and frustrating when I try to use Isar as much as possible (and ML for the things not available in Isar.) Often it seems to be something to do with theories. And although I've been using Isabelle for over 10 years now, it seems that these difficulties have only arisen in the last few years, and mostly to do with trying to use Isar. In short, using Isar is so much more difficult than using pure ML for proofs. (Of course, learning two languages instead of one is no doubt part of the reason also).

* ML functions that refer to the old-style (dynamic) context, such as "the_context" and "thm" are very hard to understand exactly and should be replaced more and more by proper antiquotations (which are statically scoped at compile-time).

If I understand correctly the_context () returns the current theory as at the point where it is executed. Is that correct? If so, it doesn't seem so hard to understand. But - again I may be wrong here - the difficulty in using Isar seems to be that the current theory keeps on changing, much more than with typical .ML proof files.
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?

Anyway, attached is the theory file that has taken so much of my time.
If the experts could tell me why bffcs0 is different from bffcs1-3, I'd be grateful.

Regards,

Jeremy Dawson





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