[isabelle-dev] Local_Theory.open_target instead of Local_Theory.restore

[Dmitriy Traytel]

Hi Makarius,

thanks, this is the hint I was looking for a long time now.

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.

Dmitriy

On 07.04.2015 17:47, Makarius wrote:
> Just a short note on Local_Theory.open_target (for Isabelle/83071f4c8ae6)
> versus old uses of Local_Theory.restore.
>
> 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.
>
>
> Here is a quick example that shows how to get polymorphic constants 
> out of local theory specifications, with such official context nesting:
>
> context fixes x :: 'a
> begin
>
> declare [[show_types]]
> ML_val ‹
>   val lthy = @{context};
>   val (_, lthy1) = lthy |> Local_Theory.open_target;
>   val ((t, (_, th)), lthy2) = lthy1
>     |> Local_Theory.define ((@{binding c}, NoSyn), 
> (Attrib.empty_binding, @{term "λy. x"}));
>   val lthy3 = lthy2 |> Local_Theory.close_target;
>   val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of 
> lthy3);
>
>   val th' = th |> singleton (Proof_Context.export lthy2 lthy3);
>   val th'' = th' |> singleton (Proof_Context.export lthy3 thy_ctxt);
>
>   writeln (Display.string_of_thm lthy2 th);  (*monomorphic*)
>   writeln (Display.string_of_thm lthy3 th');  (*partly polymorphic*)
>   writeln (Display.string_of_thm thy_ctxt th'');  (*fully polymorphic*)
> ›
>
> Thus the brute-force Local_Theory.restore is avoided, which only works 
> properly at the boundary of local theory command transactions anyway.
>
>
> 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.
>
> 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.
>
>
>     Makarius
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150407/1a758016/attachment-0002.html>