named interpretations

--- a/src/HOL/Lifting.thy	Fri Sep 05 00:41:00 2014 +0200
+++ b/src/HOL/Lifting.thy	Fri Sep 05 00:41:01 2014 +0200
@@ -28,7 +28,7 @@
 
 definition
   "Quotient R Abs Rep T \<longleftrightarrow>
-     (\<forall>a. Abs (Rep a) = a) \<and> 
+     (\<forall>a. Abs (Rep a) = a) \<and>
      (\<forall>a. R (Rep a) (Rep a)) \<and>
      (\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s) \<and>
      T = (\<lambda>x y. R x x \<and> Abs x = y)"
@@ -83,8 +83,8 @@
   using a unfolding Quotient_def
   by blast
 
-lemma Quotient_rep_abs_fold_unmap: 
-  assumes "x' \<equiv> Abs x" and "R x x" and "Rep x' \<equiv> Rep' x'" 
+lemma Quotient_rep_abs_fold_unmap:
+  assumes "x' \<equiv> Abs x" and "R x x" and "Rep x' \<equiv> Rep' x'"
   shows "R (Rep' x') x"
 proof -
   have "R (Rep x') x" using assms(1-2) Quotient_rep_abs by auto
@@ -92,7 +92,7 @@
 qed
 
 lemma Quotient_Rep_eq:
-  assumes "x' \<equiv> Abs x" 
+  assumes "x' \<equiv> Abs x"
   shows "Rep x' \<equiv> Rep x'"
 by simp
 
@@ -120,7 +120,7 @@
 end
 
 lemma identity_quotient: "Quotient (op =) id id (op =)"
-unfolding Quotient_def by simp 
+unfolding Quotient_def by simp
 
 text {* TODO: Use one of these alternatives as the real definition. *}
 
@@ -221,7 +221,7 @@
   shows "Quotient (op =) Abs Rep T"
 proof -
   interpret type_definition Rep Abs UNIV by fact
-  from Abs_inject Rep_inverse Abs_inverse T_def show ?thesis 
+  from Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
     by (fastforce intro!: QuotientI fun_eq_iff)
 qed
 
@@ -330,11 +330,11 @@
 (* the following two theorems are here only for convinience *)
 
 lemma typedef_right_unique: "right_unique T"
-  using T_def type Quotient_right_unique typedef_to_Quotient 
+  using T_def type Quotient_right_unique typedef_to_Quotient
   by blast
 
 lemma typedef_right_total: "right_total T"
-  using T_def type Quotient_right_total typedef_to_Quotient 
+  using T_def type Quotient_right_total typedef_to_Quotient
   by blast
 
 lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep"
@@ -503,7 +503,7 @@
   assumes "(A ===> op=) P' P"
   shows "Domainp (A OO B) = P'"
 using assms
-unfolding Domainp_iff[abs_def] OO_def bi_unique_def left_total_def rel_fun_def 
+unfolding Domainp_iff[abs_def] OO_def bi_unique_def left_total_def rel_fun_def
 by (fast intro: fun_eq_iff)
 
 lemma pcr_Domainp_par:
@@ -526,12 +526,12 @@
   assumes "left_total B"
   assumes "Domainp A = P"
   shows "Domainp (A OO B) = P"
-using assms unfolding left_total_def 
+using assms unfolding left_total_def
 by fast
 
 lemma Quotient_to_Domainp:
   assumes "Quotient R Abs Rep T"
-  shows "Domainp T = (\<lambda>x. R x x)"  
+  shows "Domainp T = (\<lambda>x. R x x)"
 by (simp add: Domainp_iff[abs_def] Quotient_cr_rel[OF assms])
 
 lemma eq_onp_to_Domainp:
@@ -559,7 +559,7 @@
 ML_file "Tools/Lifting/lifting_term.ML"
 ML_file "Tools/Lifting/lifting_def.ML"
 ML_file "Tools/Lifting/lifting_setup.ML"
-                           
+
 hide_const (open) POS NEG
 
 end

--- a/src/HOL/Tools/BNF/bnf_def.ML	Fri Sep 05 00:41:00 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -17,8 +17,8 @@
   val transfer_bnf: theory -> bnf -> bnf
   val bnf_of: Proof.context -> string -> bnf option
   val bnf_of_global: theory -> string -> bnf option
-  val bnf_interpretation: (bnf -> theory -> theory) -> (bnf -> local_theory -> local_theory) ->
-    theory -> theory
+  val bnf_interpretation: string -> (bnf -> theory -> theory) ->
+    (bnf -> local_theory -> local_theory) -> theory -> theory
   val interpret_bnf: bnf -> local_theory -> local_theory
   val register_bnf_raw: string -> bnf -> local_theory -> local_theory
   val register_bnf: string -> bnf -> local_theory -> local_theory
@@ -1523,7 +1523,9 @@
 
 fun with_transfer_bnf g bnf thy = g (transfer_bnf thy bnf) thy;
 
-val bnf_interpretation = BNF_Interpretation.interpretation o with_transfer_bnf;
+fun bnf_interpretation name =
+  BNF_Interpretation.interpretation name o with_transfer_bnf;
+
 val interpret_bnf = BNF_Interpretation.data;
 
 fun register_bnf_raw key bnf =

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Sep 05 00:41:00 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -39,7 +39,7 @@
   val fp_sugar_of_global: theory -> string -> fp_sugar option
   val fp_sugars_of: Proof.context -> fp_sugar list
   val fp_sugars_of_global: theory -> fp_sugar list
-  val fp_sugar_interpretation: (fp_sugar list -> theory -> theory) ->
+  val fp_sugars_interpretation: string -> (fp_sugar list -> theory -> theory) ->
     (fp_sugar list -> local_theory -> local_theory)-> theory -> theory
   val interpret_fp_sugars: fp_sugar list -> local_theory -> local_theory
   val register_fp_sugars_raw: fp_sugar list -> local_theory -> local_theory
@@ -223,9 +223,11 @@
   val eq: T * T -> bool = op = o pairself (map #T);
 );
 
-fun with_transfer_fp_sugar g fp_sugars thy = g (map (transfer_fp_sugar thy) fp_sugars) thy;
+fun with_transfer_fp_sugars g fp_sugars thy = g (map (transfer_fp_sugar thy) fp_sugars) thy;
 
-val fp_sugar_interpretation = FP_Sugar_Interpretation.interpretation o with_transfer_fp_sugar;
+fun fp_sugars_interpretation name =
+  FP_Sugar_Interpretation.interpretation name o with_transfer_fp_sugars;
+
 val interpret_fp_sugars = FP_Sugar_Interpretation.data;
 
 fun register_fp_sugars_raw fp_sugars =

--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Fri Sep 05 00:41:00 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -20,7 +20,7 @@
     Old_Datatype_Aux.descr * (string * sort) list * string list * string
     * (string list * string list) * (typ list * typ list)
   val get_constrs: theory -> string -> (string * typ) list option
-  val interpretation: nesting_preference ->
+  val interpretation: string -> nesting_preference ->
     (Old_Datatype_Aux.config -> string list -> theory -> theory) -> theory -> theory
   val datatype_compat: string list -> local_theory -> local_theory
   val datatype_compat_global: string list -> theory -> theory
@@ -280,10 +280,10 @@
       thy
   end;
 
-fun interpretation nesting_pref f =
+fun interpretation name nesting_pref f =
   let val new_f = new_interpretation_of nesting_pref f in
     Old_Datatype_Data.interpretation (old_interpretation_of nesting_pref f)
-    #> fp_sugar_interpretation new_f (Local_Theory.background_theory o new_f)
+    #> fp_sugars_interpretation name new_f (Local_Theory.background_theory o new_f)
   end;
 
 val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: @{attributes [nitpick_simp, simp]};

--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Fri Sep 05 00:41:00 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -7,6 +7,7 @@
 
 signature BNF_LFP_SIZE =
 sig
+  val size_interpretation: string
   val register_size: string -> string -> thm list -> thm list -> local_theory -> local_theory
   val register_size_global: string -> string -> thm list -> thm list -> theory -> theory
   val size_of: Proof.context -> string -> (string * (thm list * thm list)) option
@@ -21,6 +22,8 @@
 open BNF_Def
 open BNF_FP_Def_Sugar
 
+val size_interpretation = "size"
+
 val size_N = "size_"
 
 val rec_o_mapN = "rec_o_map"
@@ -373,7 +376,7 @@
     end
   | generate_datatype_size _ lthy = lthy;
 
-val _ = Theory.setup (fp_sugar_interpretation (map_local_theory o generate_datatype_size)
-  generate_datatype_size);
+val _ = Theory.setup (fp_sugars_interpretation size_interpretation
+  (map_local_theory o generate_datatype_size) generate_datatype_size);
 
 end;

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Sep 05 00:41:00 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -43,7 +43,7 @@
   val ctr_sugars_of_global: theory -> ctr_sugar list
   val ctr_sugar_of_case: Proof.context -> string -> ctr_sugar option
   val ctr_sugar_of_case_global: theory -> string -> ctr_sugar option
-  val ctr_sugar_interpretation: (ctr_sugar -> theory -> theory) ->
+  val ctr_sugar_interpretation: string -> (ctr_sugar -> theory -> theory) ->
     (ctr_sugar -> local_theory -> local_theory) -> theory -> theory
   val register_ctr_sugar: string -> ctr_sugar -> local_theory -> local_theory
   val default_register_ctr_sugar_global: string -> ctr_sugar -> theory -> theory
@@ -179,7 +179,8 @@
 
 fun with_transfer_ctr_sugar g ctr_sugar thy = g (transfer_ctr_sugar thy ctr_sugar) thy;
 
-val ctr_sugar_interpretation = Ctr_Sugar_Interpretation.interpretation o with_transfer_ctr_sugar;
+fun ctr_sugar_interpretation name =
+  Ctr_Sugar_Interpretation.interpretation name o with_transfer_ctr_sugar;
 
 fun register_ctr_sugar key ctr_sugar =
   Local_Theory.declaration {syntax = false, pervasive = true}

--- a/src/HOL/Tools/Ctr_Sugar/local_interpretation.ML	Fri Sep 05 00:41:00 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/local_interpretation.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -11,8 +11,8 @@
 sig
   type T
   val result: theory -> T list
-  val interpretation: (T -> theory -> theory) -> (T -> local_theory -> local_theory) -> theory ->
-    theory
+  val interpretation: string -> (T -> theory -> theory) -> (T -> local_theory -> local_theory) ->
+    theory -> theory
   val data: T -> local_theory -> local_theory
   val data_global: T -> theory -> theory
   val init: theory -> theory
@@ -27,7 +27,7 @@
 (
   type T =
     (Name_Space.naming * T) list
-    * ((((T -> theory -> theory) * (T -> local_theory -> local_theory)) * stamp)
+    * ((((T -> theory -> theory) * (T -> local_theory -> local_theory)) * (string * stamp))
        * (Name_Space.naming * T) list) list;
   val empty = ([], []);
   val extend = I;
@@ -61,8 +61,8 @@
   consolidate_common (fn (f, _) => fn (naming, x) => fn thy =>
     thy |> Sign.map_naming (K naming) |> f x |> Sign.restore_naming thy) I thy thy;
 
-fun interpretation g f =
-  Interp.map (apsnd (cons (((g, f), stamp ()), []))) #> perhaps consolidate_global;
+fun interpretation name g f =
+  Interp.map (apsnd (cons (((g, f), (name, stamp ())), []))) #> perhaps consolidate_global;
 
 fun data x =
   Local_Theory.background_theory (fn thy => Interp.map (apfst (cons (Sign.naming_of thy, x))) thy)

--- a/src/HOL/Tools/Lifting/lifting_bnf.ML	Fri Sep 05 00:41:00 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -6,6 +6,7 @@
 
 signature LIFTING_BNF =
 sig
+  val lifting_interpretation: string
 end
 
 structure Lifting_BNF : LIFTING_BNF =
@@ -15,6 +16,8 @@
 open BNF_Def
 open Transfer_BNF
 
+val lifting_interpretation = "lifting"
+
 (* Quotient map theorem *)
 
 fun Quotient_tac bnf ctxt i =
@@ -115,8 +118,8 @@
       snd (Local_Theory.notes notes lthy)
     end
 
-val _ = Theory.setup (bnf_interpretation
-  (bnf_only_type_ctr (map_local_theory o lifting_bnf_interpretation))
+val _ = Theory.setup (bnf_interpretation lifting_interpretation
+  (bnf_only_type_ctr (BNF_Util.map_local_theory o lifting_bnf_interpretation))
   (bnf_only_type_ctr lifting_bnf_interpretation))
 
 end

--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Sep 05 00:41:00 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -6,6 +6,10 @@
 
 signature EXHAUSTIVE_GENERATORS =
 sig
+  val exhaustive_interpretation: string
+  val bounded_forall_interpretation: string
+  val full_exhaustive_interpretation: string
+
   val compile_generator_expr:
     Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option
   val compile_generator_exprs: Proof.context -> term list -> (int -> term list option) list
@@ -35,6 +39,11 @@
 
 (* basics *)
 
+val exhaustive_interpretation = "exhaustive"
+val bounded_forall_interpretation = "bounded_forall"
+val full_exhaustive_interpretation = "full_exhaustive"
+
+
 (** dynamic options **)
 
 val smart_quantifier = Attrib.setup_config_bool @{binding quickcheck_smart_quantifier} (K true)
@@ -534,17 +543,20 @@
 (* setup *)
 
 val setup_exhaustive_datatype_interpretation =
-  Quickcheck_Common.datatype_interpretation (@{sort exhaustive}, instantiate_exhaustive_datatype)
+  Quickcheck_Common.datatype_interpretation exhaustive_interpretation
+    (@{sort exhaustive}, instantiate_exhaustive_datatype)
 
 val setup_bounded_forall_datatype_interpretation =
-  BNF_LFP_Compat.interpretation BNF_LFP_Compat.Keep_Nesting (Quickcheck_Common.ensure_sort
-    (((@{sort type}, @{sort type}), @{sort bounded_forall}),
-    (fn thy => BNF_LFP_Compat.the_descr thy BNF_LFP_Compat.Keep_Nesting, instantiate_bounded_forall_datatype)))
+  BNF_LFP_Compat.interpretation bounded_forall_interpretation BNF_LFP_Compat.Keep_Nesting
+    (Quickcheck_Common.ensure_sort
+       (((@{sort type}, @{sort type}), @{sort bounded_forall}),
+       (fn thy => BNF_LFP_Compat.the_descr thy BNF_LFP_Compat.Keep_Nesting, instantiate_bounded_forall_datatype)))
 
 val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true);
 
 val setup =
-  Quickcheck_Common.datatype_interpretation (@{sort full_exhaustive}, instantiate_full_exhaustive_datatype)
+  Quickcheck_Common.datatype_interpretation full_exhaustive_interpretation
+    (@{sort full_exhaustive}, instantiate_full_exhaustive_datatype)
   #> Context.theory_map (Quickcheck.add_tester ("exhaustive", (active, test_goals)))
   #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
   #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs));

--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Sep 05 00:41:00 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -6,6 +6,7 @@
 
 signature NARROWING_GENERATORS =
 sig
+  val narrowing_interpretation: string
   val allow_existentials : bool Config.T
   val finite_functions : bool Config.T
   val overlord : bool Config.T
@@ -22,6 +23,8 @@
 structure Narrowing_Generators : NARROWING_GENERATORS =
 struct
 
+val narrowing_interpretation = "narrowing"
+
 (* configurations *)
 
 val allow_existentials = Attrib.setup_config_bool @{binding quickcheck_allow_existentials} (K true)
@@ -525,7 +528,8 @@
 val setup =
   Code.datatype_interpretation ensure_partial_term_of
   #> Code.datatype_interpretation ensure_partial_term_of_code
-  #> Quickcheck_Common.datatype_interpretation (@{sort narrowing}, instantiate_narrowing_datatype)
+  #> Quickcheck_Common.datatype_interpretation narrowing_interpretation
+    (@{sort narrowing}, instantiate_narrowing_datatype)
   #> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals)))
     
 end;

--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Fri Sep 05 00:41:00 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -32,7 +32,7 @@
     -> Old_Datatype_Aux.config -> string list -> theory -> theory
   val ensure_common_sort_datatype :
     (sort * instantiation) -> Old_Datatype_Aux.config -> string list -> theory -> theory
-  val datatype_interpretation : (sort * instantiation) -> theory -> theory
+  val datatype_interpretation : string -> sort * instantiation -> theory -> theory
   val gen_mk_parametric_generator_expr :
    (((Proof.context -> term * term list -> term) * term) * typ)
      -> Proof.context -> (term * term list) list -> term
@@ -422,8 +422,8 @@
   ensure_sort (((@{sort typerep}, @{sort term_of}), sort),
     (fn thy => BNF_LFP_Compat.the_descr thy BNF_LFP_Compat.Keep_Nesting, instantiate))
 
-val datatype_interpretation =
-  BNF_LFP_Compat.interpretation BNF_LFP_Compat.Keep_Nesting o ensure_common_sort_datatype
+fun datatype_interpretation name =
+  BNF_LFP_Compat.interpretation name BNF_LFP_Compat.Keep_Nesting o ensure_common_sort_datatype
   
 (** generic parametric compilation **)
 

--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Sep 05 00:41:00 2014 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -7,6 +7,7 @@
 signature RANDOM_GENERATORS =
 sig
   type seed = Random_Engine.seed
+  val random_interpretation: string
   val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term)
     -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
     -> seed -> (('a -> 'b) * (unit -> term)) * seed
@@ -24,6 +25,8 @@
 structure Random_Generators : RANDOM_GENERATORS =
 struct
 
+val random_interpretation = "random";
+
 (** abstract syntax **)
 
 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"})
@@ -471,7 +474,8 @@
 val active = Attrib.setup_config_bool @{binding quickcheck_random_active} (K false);
 
 val setup =
-  Quickcheck_Common.datatype_interpretation (@{sort random}, instantiate_random_datatype)
+  Quickcheck_Common.datatype_interpretation random_interpretation
+    (@{sort random}, instantiate_random_datatype)
   #> Context.theory_map (Quickcheck.add_tester ("random", (active, test_goals)));
 
 end;

--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Fri Sep 05 00:41:00 2014 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -6,10 +6,10 @@
 
 signature TRANSFER_BNF =
 sig
+  val transfer_interpretation: string
   val base_name_of_bnf: BNF_Def.bnf -> binding
   val type_name_of_bnf: BNF_Def.bnf -> string
   val lookup_defined_pred_data: Proof.context -> string -> Transfer.pred_data
-  val map_local_theory: (local_theory -> local_theory) -> theory -> theory
   val bnf_only_type_ctr: (BNF_Def.bnf -> 'a -> 'a) -> BNF_Def.bnf -> 'a -> 'a
 end
 
@@ -21,6 +21,8 @@
 open BNF_FP_Util
 open BNF_FP_Def_Sugar
 
+val transfer_interpretation = "transfer"
+
 (* util functions *)
 
 fun base_name_of_bnf bnf = Binding.name (Binding.name_of (name_of_bnf bnf))
@@ -59,8 +61,6 @@
 fun is_Type (Type _) = true
   | is_Type _ = false
 
-fun map_local_theory f = Named_Target.theory_init #> f #> Local_Theory.exit_global
-
 fun bnf_only_type_ctr f bnf = if is_Type (T_of_bnf bnf) then f bnf else I
 
 fun bnf_of_fp_sugar (fp_sugar:fp_sugar) = nth (#bnfs (#fp_res fp_sugar)) (#fp_res_index fp_sugar)
@@ -290,8 +290,8 @@
     snd (Local_Theory.notes (constr_notes @ relator_eq_notes @ pred_notes) lthy)
   end
 
-val _ = Theory.setup (bnf_interpretation
-  (bnf_only_type_ctr (map_local_theory o transfer_bnf_interpretation))
+val _ = Theory.setup (bnf_interpretation transfer_interpretation
+  (bnf_only_type_ctr (BNF_Util.map_local_theory o transfer_bnf_interpretation))
   (bnf_only_type_ctr (transfer_bnf_interpretation)))
 
 (* simplification rules for the predicator *)
@@ -351,7 +351,7 @@
 
 (* fp_sugar interpretation *)
 
-fun transfer_fp_sugar_interpretation fp_sugar lthy =
+fun transfer_fp_sugars_interpretation fp_sugar lthy =
   let
     val pred_injects = prove_pred_inject lthy fp_sugar
     fun qualify defname suffix = Binding.qualified true suffix defname
@@ -361,8 +361,8 @@
     snd (Local_Theory.note ((pred_inject_thm_name, simp_attrs), pred_injects) lthy)
   end
 
-val _ = Theory.setup (fp_sugar_interpretation
-  (fp_sugar_only_type_ctr (map_local_theory o fold transfer_fp_sugar_interpretation))
-  (fp_sugar_only_type_ctr (fold transfer_fp_sugar_interpretation)))
+val _ = Theory.setup (fp_sugars_interpretation transfer_interpretation
+  (fp_sugar_only_type_ctr (map_local_theory o fold transfer_fp_sugars_interpretation))
+  (fp_sugar_only_type_ctr (fold transfer_fp_sugars_interpretation)))
 
 end