<html>
<head>
<meta content="text/html; charset=UTF-8" http-equiv="Content-Type">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<div class="moz-cite-prefix">Hi Makarius,<br>
<br>
thanks, this is the hint I was looking for a long time now.<br>
<br>
I will do the replacement in the BNF package, but I don't think
that I will have time for it before the approaching release.<br>
<br>
Dmitriy<br>
<br>
On 07.04.2015 17:47, Makarius wrote:<br>
</div>
<blockquote
cite="mid:alpine.LNX.2.00.1504071729590.46505@lxbroy10.informatik.tu-muenchen.de"
type="cite">Just a short note on Local_Theory.open_target (for
Isabelle/83071f4c8ae6)
<br>
versus old uses of Local_Theory.restore.
<br>
<br>
Local_Theory.open_target is the internal version of "context
begin", where Local_Theory.close_target is "end". The ML
signature is now a bit more concise form than before. It has
already been used successfully in Eisbach, to lay out a local
situation for the internal construction.
<br>
<br>
<br>
Here is a quick example that shows how to get polymorphic
constants out of local theory specifications, with such official
context nesting:
<br>
<br>
context fixes x :: 'a
<br>
begin
<br>
<br>
declare [[show_types]]
<br>
ML_val ‹
<br>
val lthy = @{context};
<br>
val (_, lthy1) = lthy |> Local_Theory.open_target;
<br>
val ((t, (_, th)), lthy2) = lthy1
<br>
|> Local_Theory.define ((@{binding c}, NoSyn),
(Attrib.empty_binding, @{term "λy. x"}));
<br>
val lthy3 = lthy2 |> Local_Theory.close_target;
<br>
val thy_ctxt = Proof_Context.init_global
(Proof_Context.theory_of lthy3);
<br>
<br>
val th' = th |> singleton (Proof_Context.export lthy2 lthy3);
<br>
val th'' = th' |> singleton (Proof_Context.export lthy3
thy_ctxt);
<br>
<br>
writeln (Display.string_of_thm lthy2 th); (*monomorphic*)
<br>
writeln (Display.string_of_thm lthy3 th'); (*partly
polymorphic*)
<br>
writeln (Display.string_of_thm thy_ctxt th''); (*fully
polymorphic*)
<br>
›
<br>
<br>
Thus the brute-force Local_Theory.restore is avoided, which only
works properly at the boundary of local theory command
transactions anyway.
<br>
<br>
<br>
Eliminating Local_Theory.restore is one of these continuous reform
projects that can be done now or later. Note that it would also
achieve better results for "private datatype", because
Local_Theory.restore disrupts the continuity of the naming policy.
<br>
<br>
It is up to the BNF guys to say if they intend to do something for
the Isabelle2015 release, or just leave the status quo. It is
unlikely that anybody will notice fine points of private datatype
definitions before the next release after Isabelle2015.
<br>
<br>
<br>
Makarius
<br>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
<br>
</body>
</html>