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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
