*To*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Subject*: Re: [isabelle] antiquotations*From*: Stefan Berghofer <berghofe at in.tum.de>*Date*: Mon, 11 Feb 2008 15:34:11 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <47AF877C.4050205@rsise.anu.edu.au>*Organization*: Technische Universität München*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> <47AF877C.4050205@rsise.anu.edu.au>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.7.13) Gecko/20060417

Jeremy Dawson wrote:

However I don't understand this - as I said in my earlier email, exactlythe same ML code _does_ produce the desired result later on. So whydoes the _same_ ML expression behave _differently_ at different points? Both the points where the ML expression bool_axioms RL [fun_cong] isused occur _after_ the point where fun is shown to be in theaxclass boolean_class (I understand that this is what the problem was).

Dear Jeremy, the reason for this effect is that each theorem contains an ML reference pointing to the theory it has been proved in (or been looked up in). The theorems contained in bool_axioms refer to some intermediate theory that does not yet contain the information that fun is in boolean_class. However, as soon as your theory has been completely processed, all theorems that have been proved in the preceeding intermediate theories are promoted to theorems that are also valid in the final theory. This is done by (imperatively!) updating the theory references contained in the theorems, which explains why the very same ML expression (denoting a data structure containing a reference) suddenly behaves in a different way. This usage of references might indeed seem a bit strange at first sight, but it seems to be the only way to achieve that definitions and proofs may be intermixed within the same theory, which was impossible with the implementation of theories we had in Isabelle more than a decade ago. An effect similar to the one that you have noticed can be produced by executing the ML command Type.of_sort (Sign.tsig_of (theory_of_thm (hd bool_axioms))) (Type ("fun", [TFree ("'a", HOLogic.typeS), TFree ("'b", ["BI.boolean_class"])]), ["BI.boolean_class"]) for checking whether a function type is a member of boolean_class. This expression returns "false" when executed inside your theory, but "true" when executed outside your theory, because the theory returned by "theory_of_thm ..." is changed when closing the theory. Greetings, Stefan -- Dr. Stefan Berghofer E-Mail: berghofe at in.tum.de Institut fuer Informatik Phone: +49 89 289 17328 Technische Universitaet Muenchen Fax: +49 89 289 17307 Boltzmannstr. 3 Room: 01.11.059 85748 Garching, GERMANY http://www.in.tum.de/~berghofe

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

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

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

- Previous by Date: Re: [isabelle] antiquotations
- Next by Date: [isabelle] IMLA'08: Call for Papers
- Previous by Thread: Re: [isabelle] antiquotations
- Next by Thread: [isabelle] TTVSI call for participation, registration, and posters
- 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