--- 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
--- 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))
--- 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))
--- 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;
--- 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)
--- 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 *)
--- 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 =
--- 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';
--- 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;
--- 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 *)
--- 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 *)
--- 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;