*To*: Makarius <makarius at sketis.net>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] antiquotations*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Mon, 11 Feb 2008 10:23:40 +1100*In-reply-to*: <Pine.LNX.4.63.0802081405450.9643@atbroy100.informatik.tu-muenchen.de>*References*: <478AAC94.3030404@rsise.anu.edu.au> <478B2940.5020107@informatik.tu-muenchen.de> <478BEE3B.2000007@rsise.anu.edu.au> <478C8265.2010202@in.tum.de> <478D322C.7010001@rsise.anu.edu.au> <478DB7F0.7080604@in.tum.de> <478E6F17.9000100@rsise.anu.edu.au> <478E816D.9010606@in.tum.de> <478EF53A.9070809@rsise.anu.edu.au> <Pine.LNX.4.63.0801241542360.18967@atbroy100.informatik.tu-muenchen.de> <47ABC81B.3090608@rsise.anu.edu.au> <Pine.LNX.4.63.0802081405450.9643@atbroy100.informatik.tu-muenchen.de>*User-agent*: Icedove 1.5.0.14pre (X11/20071018)

Makarius wrote:

On Fri, 8 Feb 2008, Jeremy Dawson wrote:Mostly my problems are something do to with theories. I don't know ifthe problems I've faced today are because of theories or not, but Ithink it is quite likely. But I waste an enormous amount of time tryingto 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 uncleartheory/proof context).In particular: - Use ProofGeneral by default.- Always work within a theory body, if a theory is required. Do notrely on accidental theory states from previous use_thy etc.- Use ML antiquotions as much as possible, because here the context ischecked statically at compile time.The latest example is contained in the attached theory file. For somereason the ML expression bool_axioms RL [fun_cong] produces an emptylist of results when it appears in the theory file being loaded.After the theory file is modified in the way shown (ie not usingbool_axioms RL [fun_cong]) it loads OK. Then, after that, theexpression bool_axioms RL [fun_cong] returns exactly the resultsexpected. Why does the same ML expression behave differently atdifferent points ?This is a good example why proper contexts matter. The bool_axioms listis bound at the ML toplevel in a situation *before* certain type classinstantiations in your theory. For the resolution to work out, these typearities need to be present in the theory.

Makarius, Thanks for this - I think I understand this point.

Your ML code fails to produceany result here, because it references bool_axioms in the raw MLenvironment, without going through the Isar layer, which would havetransferred the result as required.

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}

from the result it gives afterwards. Why is this?

So far as I understood the previous emails,

Finally, is all this stuff documented anywhere?

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

Jeremy

**Follow-Ups**:**Re: [isabelle] antiquotations***From:*Makarius

**Re: [isabelle] antiquotations***From:*Alexander Krauss

**Re: [isabelle] antiquotations***From:*Stefan Berghofer

**References**:**Re: [isabelle] antiquotations***From:*Jeremy Dawson

**Re: [isabelle] antiquotations***From:*Makarius

- Previous by Date: [isabelle] typesetting compound subscripts
- Next by Date: Re: [isabelle] antiquotations
- Previous by Thread: Re: [isabelle] antiquotations
- Next by Thread: Re: [isabelle] antiquotations
- Cl-isabelle-users February 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list