Re: [isabelle] antiquotations

Jeremy Dawson wrote:
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).

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"])]),

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.


Dr. Stefan Berghofer               E-Mail: berghofe at
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  

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