# HG changeset patch
# User haftmann
# Date 1550740507 0
# Node ID 3bfa28b3a5b24887f68754d0c1da8f8795580b1a
# Parent  74d673b7d40eff44275da56c777af555bea30255
streamlined specification interfaces

diff -r 74d673b7d40e -r 3bfa28b3a5b2 NEWS
--- a/NEWS	Thu Feb 21 09:15:06 2019 +0000
+++ b/NEWS	Thu Feb 21 09:15:07 2019 +0000
@@ -104,6 +104,10 @@
 * Slightly more conventional naming schema in structure Inductive.
 Minor INCOMPATIBILITY.
 
+* Various _global variants of specification tools have been removed.
+Minor INCOMPATIBILITY, prefer combinators Named_Target.theory_map[_result]
+to lift specifications to the global theory level.
+
 * Code generation: command 'export_code' without file keyword exports
 code as regular theory export, which can be materialized using the
 command-line tools "isabelle export" or "isabelle build -e" (with
diff -r 74d673b7d40e -r 3bfa28b3a5b2 src/HOL/HOLCF/Tools/cpodef.ML
--- a/src/HOL/HOLCF/Tools/cpodef.ML	Thu Feb 21 09:15:06 2019 +0000
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Thu Feb 21 09:15:07 2019 +0000
@@ -164,8 +164,10 @@
 fun add_podef typ set opt_bindings tac thy =
   let
     val name = #1 typ
-    val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy
-      |> Typedef.add_typedef_global {overloaded = false} typ set opt_bindings tac
+    val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) =
+      thy
+      |> Named_Target.theory_map_result (apsnd o Typedef.transform_info)
+           (Typedef.add_typedef {overloaded = false} typ set opt_bindings tac)
     val oldT = #rep_type (#1 info)
     val newT = #abs_type (#1 info)
     val lhs_tfrees = map dest_TFree (snd (dest_Type newT))
diff -r 74d673b7d40e -r 3bfa28b3a5b2 src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Thu Feb 21 09:15:06 2019 +0000
+++ b/src/HOL/Import/import_rule.ML	Thu Feb 21 09:15:07 2019 +0000
@@ -223,9 +223,10 @@
       Abs_name = Binding.name abs_name,
       type_definition_name = Binding.name ("type_definition_" ^ tycname)}
     val ((_, typedef_info), thy') =
-     Typedef.add_typedef_global {overloaded = false}
+     Named_Target.theory_map_result (apsnd o Typedef.transform_info)
+     (Typedef.add_typedef {overloaded = false}
        (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
-       (SOME typedef_bindings) (fn ctxt => resolve_tac ctxt [th2] 1) thy
+       (SOME typedef_bindings) (fn ctxt => resolve_tac ctxt [th2] 1)) thy
     val aty = #abs_type (#1 typedef_info)
     val th = freezeT thy' (#type_definition (#2 typedef_info))
     val (th_s, _) = Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th))
diff -r 74d673b7d40e -r 3bfa28b3a5b2 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Thu Feb 21 09:15:06 2019 +0000
+++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Feb 21 09:15:07 2019 +0000
@@ -535,12 +535,13 @@
     val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
       thy3
       |> Sign.concealed
-      |> Inductive.add_inductive_global
+      |> Named_Target.theory_map_result Inductive.transform_result
+         (Inductive.add_inductive
           {quiet_mode = false, verbose = false, alt_name = Binding.name big_rep_name,
            coind = false, no_elim = true, no_ind = false, skip_mono = true}
           (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
              (rep_set_names' ~~ recTs'))
-          [] (map (fn x => (Binding.empty_atts, x)) intr_ts) []
+          [] (map (fn x => (Binding.empty_atts, x)) intr_ts) [])
       ||> Sign.restore_naming thy3;
 
     (**** Prove that representing set is closed under permutation ****)
@@ -582,7 +583,8 @@
     val (typedefs, thy6) =
       thy4
       |> fold_map (fn (((name, mx), tvs), (cname, U)) => fn thy =>
-          Typedef.add_typedef_global {overloaded = false}
+          Named_Target.theory_map_result (apsnd o Typedef.transform_info)
+          (Typedef.add_typedef {overloaded = false}
             (name, map (fn (v, _) => (v, dummyS)) tvs, mx)  (* FIXME keep constraints!? *)
             (Const (\<^const_name>\<open>Collect\<close>, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
                Const (cname, U --> HOLogic.boolT)) NONE
@@ -590,7 +592,7 @@
               resolve_tac ctxt [exI] 1 THEN
               resolve_tac ctxt [CollectI] 1 THEN
               QUIET_BREADTH_FIRST (has_fewer_prems 1)
-              (resolve_tac ctxt rep_intrs 1)) thy |> (fn ((_, r), thy) =>
+              (resolve_tac ctxt rep_intrs 1))) thy |> (fn ((_, r), thy) =>
         let
           val permT = mk_permT
             (TFree (singleton (Name.variant_list (map fst tvs)) "'a", \<^sort>\<open>type\<close>));
@@ -1523,12 +1525,12 @@
     val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
       thy10
       |> Sign.concealed
-      |> Inductive.add_inductive_global
-          {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
+      |> Named_Target.theory_map_result Inductive.transform_result
+          (Inductive.add_inductive {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
            coind = false, no_elim = false, no_ind = false, skip_mono = true}
           (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
           (map dest_Free rec_fns)
-          (map (fn x => (Binding.empty_atts, x)) rec_intr_ts) []
+          (map (fn x => (Binding.empty_atts, x)) rec_intr_ts) [])
       ||> Global_Theory.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct")
       ||> Sign.restore_naming thy10;
 
diff -r 74d673b7d40e -r 3bfa28b3a5b2 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Thu Feb 21 09:15:06 2019 +0000
+++ b/src/HOL/Tools/Function/partial_function.ML	Thu Feb 21 09:15:07 2019 +0000
@@ -12,6 +12,7 @@
     Attrib.binding * term -> local_theory -> (term * thm) * local_theory
   val add_partial_function_cmd: string -> (binding * string option * mixfix) list ->
     Attrib.binding * string -> local_theory -> (term * thm) * local_theory
+  val transform_result: morphism -> term * thm -> term * thm
 end;
 
 structure Partial_Function: PARTIAL_FUNCTION =
@@ -219,6 +220,8 @@
 
 (*** partial_function definition ***)
 
+fun transform_result phi (t, thm) = (Morphism.term phi t, Morphism.thm phi thm);
+
 fun gen_add_partial_function prep mode fixes_raw eqn_raw lthy =
   let
     val setup_data = the (lookup_mode lthy mode)
diff -r 74d673b7d40e -r 3bfa28b3a5b2 src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Thu Feb 21 09:15:06 2019 +0000
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Thu Feb 21 09:15:07 2019 +0000
@@ -150,12 +150,13 @@
     val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
       thy0
       |> Sign.concealed
-      |> Inductive.add_inductive_global
+      |> Named_Target.theory_map_result Inductive.transform_result
+          (Inductive.add_inductive
           {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name',
             coind = false, no_elim = false, no_ind = true, skip_mono = true}
           (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
           (map dest_Free rec_fns)
-          (map (fn x => (Binding.empty_atts, x)) rec_intr_ts) []
+          (map (fn x => (Binding.empty_atts, x)) rec_intr_ts) [])
       ||> Sign.restore_naming thy0;
 
     (* prove uniqueness and termination of primrec combinators *)
diff -r 74d673b7d40e -r 3bfa28b3a5b2 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Thu Feb 21 09:15:06 2019 +0000
+++ b/src/HOL/Tools/inductive.ML	Thu Feb 21 09:15:07 2019 +0000
@@ -52,10 +52,6 @@
     flags -> ((binding * typ) * mixfix) list ->
     (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory ->
     result * local_theory
-  val add_inductive_global:
-    flags -> ((binding * typ) * mixfix) list ->
-    (string * typ) list -> (Attrib.binding * term) list -> thm list -> theory ->
-    result * theory
   val add_inductive_cmd: bool -> bool ->
     (binding * string option * mixfix) list ->
     (binding * string option * mixfix) list ->
@@ -1226,16 +1222,6 @@
 val add_inductive = gen_add_inductive add_ind_def;
 val add_inductive_cmd = gen_add_inductive_cmd add_ind_def;
 
-fun add_inductive_global flags cnames_syn pnames pre_intros monos thy =
-  let
-    val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
-    val ctxt' = thy
-      |> Named_Target.theory_init
-      |> add_inductive flags cnames_syn pnames pre_intros monos |> snd
-      |> Local_Theory.exit;
-    val info = #2 (the_inductive_global ctxt' name);
-  in (info, Proof_Context.theory_of ctxt') end;
-
 
 (* read off arities of inductive predicates from raw induction rule *)
 fun arities_of induct =
diff -r 74d673b7d40e -r 3bfa28b3a5b2 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Thu Feb 21 09:15:06 2019 +0000
+++ b/src/HOL/Tools/inductive_realizer.ML	Thu Feb 21 09:15:07 2019 +0000
@@ -352,13 +352,14 @@
     (** realizability predicate **)
 
     val (ind_info, thy3') = thy2 |>
-      Inductive.add_inductive_global
+      Named_Target.theory_map_result Inductive.transform_result
+      (Inductive.add_inductive
         {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
           no_elim = false, no_ind = false, skip_mono = false}
         rlzpreds rlzparams (map (fn (rintr, intr) =>
           ((Binding.name (Long_Name.base_name (name_of_thm intr)), []),
            subst_atomic rlzpreds' (Logic.unvarify_global rintr)))
-             (rintrs ~~ maps snd rss)) [] ||>
+             (rintrs ~~ maps snd rss)) []) ||>
       Sign.root_path;
     val thy3 = fold (Global_Theory.hide_fact false o name_of_thm) (#intrs ind_info) thy3';
 
diff -r 74d673b7d40e -r 3bfa28b3a5b2 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Thu Feb 21 09:15:06 2019 +0000
+++ b/src/HOL/Tools/record.ML	Thu Feb 21 09:15:07 2019 +0000
@@ -102,8 +102,9 @@
     val vs = map (Proof_Context.check_tfree ctxt) raw_vs;
   in
     thy
-    |> Typedef.add_typedef_global overloaded (raw_tyco, vs, NoSyn)
-        (HOLogic.mk_UNIV repT) NONE (fn ctxt' => resolve_tac ctxt' [UNIV_witness] 1)
+    |> Named_Target.theory_map_result (apsnd o Typedef.transform_info)
+        (Typedef.add_typedef overloaded (raw_tyco, vs, NoSyn)
+          (HOLogic.mk_UNIV repT) NONE (fn ctxt' => resolve_tac ctxt' [UNIV_witness] 1))
     |-> (fn (tyco, info) => get_typedef_info tyco vs info)
   end;
 
diff -r 74d673b7d40e -r 3bfa28b3a5b2 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Thu Feb 21 09:15:06 2019 +0000
+++ b/src/HOL/Tools/typedef.ML	Thu Feb 21 09:15:07 2019 +0000
@@ -307,9 +307,8 @@
   in typedef_result inhabited lthy' end;
 
 fun add_typedef_global overloaded typ set opt_bindings tac =
-  Named_Target.theory_init
-  #> add_typedef overloaded typ set opt_bindings tac
-  #> Local_Theory.exit_result_global (apsnd o transform_info);
+  Named_Target.theory_map_result (apsnd o transform_info)
+    (add_typedef overloaded typ set opt_bindings tac)
 
 
 (* typedef: proof interface *)
diff -r 74d673b7d40e -r 3bfa28b3a5b2 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Thu Feb 21 09:15:06 2019 +0000
+++ b/src/Pure/Isar/class.ML	Thu Feb 21 09:15:07 2019 +0000
@@ -39,6 +39,9 @@
     -> string list * (string * sort) list * sort
   val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory
   val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state
+  val theory_map_result: string list * (string * sort) list * sort
+    -> (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory)
+    -> (Proof.context -> 'b -> tactic) -> theory -> 'b * theory
 
   (*subclasses*)
   val classrel: class * class -> theory -> Proof.state
@@ -749,6 +752,11 @@
     |> pair y
   end;
 
+fun theory_map_result arities f g tac =
+  instantiation arities
+  #> g
+  #-> prove_instantiation_exit_result f tac;
+
 
 (* simplified instantiation interface with no class parameter *)
 
diff -r 74d673b7d40e -r 3bfa28b3a5b2 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Thu Feb 21 09:15:06 2019 +0000
+++ b/src/Pure/Isar/overloading.ML	Thu Feb 21 09:15:07 2019 +0000
@@ -15,6 +15,11 @@
 
   val overloading: (string * (string * typ) * bool) list -> theory -> local_theory
   val overloading_cmd: (string * string * bool) list -> theory -> local_theory
+  val theory_map: (string * (string * typ) * bool) list
+    -> (local_theory -> local_theory) -> theory -> theory
+  val theory_map_result: (string * (string * typ) * bool) list
+    -> (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory)
+    -> theory -> 'b * theory
 end;
 
 structure Overloading: OVERLOADING =
@@ -185,19 +190,19 @@
           commas_quote (map (Syntax.string_of_term lthy o Const o fst) overloading));
   in lthy end;
 
-fun gen_overloading prep_const raw_overloading thy =
+fun gen_overloading prep_const raw_overloading_spec thy =
   let
     val ctxt = Proof_Context.init_global thy;
-    val _ = if null raw_overloading then error "At least one parameter must be given" else ();
-    val overloading = raw_overloading |> map (fn (v, const, checked) =>
+    val _ = if null raw_overloading_spec then error "At least one parameter must be given" else ();
+    val overloading_spec = raw_overloading_spec |> map (fn (v, const, checked) =>
       (Term.dest_Const (prep_const ctxt const), (v, checked)));
   in
     thy
     |> Generic_Target.init
        {background_naming = Sign.naming_of thy,
         setup = Proof_Context.init_global
-          #> Data.put overloading
-          #> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
+          #> Data.put overloading_spec
+          #> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading_spec
           #> activate_improvable_syntax
           #> synchronize_syntax,
         conclude = conclude}
@@ -213,4 +218,9 @@
 val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
 val overloading_cmd = gen_overloading Syntax.read_term;
 
+fun theory_map overloading_spec g =
+  overloading overloading_spec #> g #> Local_Theory.exit_global;
+fun theory_map_result overloading_spec f g =
+  overloading overloading_spec #> g #> Local_Theory.exit_result_global f;
+
 end;