Re: [isabelle] making local definitions programmatically



Hi Michael,

> Ah yes.  If I call LocalTheory.restore, I guess I still have to later
> call LocalTheory.exit.  Is that right?

> And another thing: a while back Makarius said that we should avoid all
> functions that implicitly manipulate references because these are
> unsafe in the presence of threads.  Yet it is clear that Context.>>>
> must be doing this.  Is this function an exception to the general rule?

It is helpful to recall the local theory sandwich:

	hypothetical proof context (ctxt)
	---------------------------------
        local theory               (lthy)
        ---------------------------------
        background theory          (thy)

An lthy is "put on top" of a thy e.g. by means of LocalTheory.init.
LocalTheory.define etc. than accumulate hypothetical entities, resulting
in the hypothetical context ctxt.  If necessary, you can "switch back"
to lthy by LocalTheory.restore.  Since LocalTheory.define etc. extend
thy, linearity has to be ensured - Local.Theory.exit re-exposed the
"backbone" theory thy.

So much to say about this part of the story.

Now concerning Context.>>(>).  These are the *only* remaining facilities
which update a context destructively;  in a certain fashion they are the
sinbin where the (rare) cases when a destructive update is unaviodable
are focused.  The runtime framework asserts that concurrent threads do
not interfere here.  Of course the best thing is to adhere to explicit
pure updates, but for bootstrap, legacy or explorative issues this
facility is helpful.

Hope this helps

	Florian
begin:vcard
fn:Florian Haftmann
n:Haftmann;Florian
org;quoted-printable;quoted-printable:Technische Universit=C3=A4t M=C3=BCnchen ;Institut f=C3=BCr Informatik, Lehrstuhl Software and Systems Engineering
adr;quoted-printable;quoted-printable:;;Boltzmannstra=C3=9Fe 3;M=C3=BCnchen;Bayern;85748;Deutschland
email;internet:florian.haftmann at informatik.tu-muenchen.de
title:M. Sc.
tel;work:(++49 89) 289 - 17300
note;quoted-printable:PGP available: =
	=0D=0A=
	http://www4.informatik.tu-muenchen.de/~haftmann/pgp/florian_haftmann_at_i=
	nformatik_tu_muenchen_de.pgp=0D=0A=
	
x-mozilla-html:FALSE
url:http://isabelle.in.tum.de/~haftmann
version:2.1
end:vcard

Attachment: signature.asc
Description: OpenPGP digital signature



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