# HG changeset patch # User blanchet # Date 1409870461 -7200 # Node ID a6c3962ea9074b19f212ff8ab983fdee10cf2e8f # Parent e6e3b20340be59d585fed6bd10f354698889b66d named interpretations diff -r e6e3b20340be -r a6c3962ea907 src/HOL/Lifting.thy --- 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 \ - (\a. Abs (Rep a) = a) \ + (\a. Abs (Rep a) = a) \ (\a. R (Rep a) (Rep a)) \ (\r s. R r s \ R r r \ R s s \ Abs r = Abs s) \ T = (\x y. R x x \ Abs x = y)" @@ -83,8 +83,8 @@ using a unfolding Quotient_def by blast -lemma Quotient_rep_abs_fold_unmap: - assumes "x' \ Abs x" and "R x x" and "Rep x' \ Rep' x'" +lemma Quotient_rep_abs_fold_unmap: + assumes "x' \ Abs x" and "R x x" and "Rep x' \ 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' \ Abs x" + assumes "x' \ Abs x" shows "Rep x' \ 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 =) (\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 = (\x. R x x)" + shows "Domainp T = (\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 diff -r e6e3b20340be -r a6c3962ea907 src/HOL/Tools/BNF/bnf_def.ML --- 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 = diff -r e6e3b20340be -r a6c3962ea907 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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 = diff -r e6e3b20340be -r a6c3962ea907 src/HOL/Tools/BNF/bnf_lfp_compat.ML --- 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]}; diff -r e6e3b20340be -r a6c3962ea907 src/HOL/Tools/BNF/bnf_lfp_size.ML --- 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; diff -r e6e3b20340be -r a6c3962ea907 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- 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} diff -r e6e3b20340be -r a6c3962ea907 src/HOL/Tools/Ctr_Sugar/local_interpretation.ML --- 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) diff -r e6e3b20340be -r a6c3962ea907 src/HOL/Tools/Lifting/lifting_bnf.ML --- 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 diff -r e6e3b20340be -r a6c3962ea907 src/HOL/Tools/Quickcheck/exhaustive_generators.ML --- 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)); diff -r e6e3b20340be -r a6c3962ea907 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- 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; diff -r e6e3b20340be -r a6c3962ea907 src/HOL/Tools/Quickcheck/quickcheck_common.ML --- 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 **) diff -r e6e3b20340be -r a6c3962ea907 src/HOL/Tools/Quickcheck/random_generators.ML --- 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; diff -r e6e3b20340be -r a6c3962ea907 src/HOL/Tools/Transfer/transfer_bnf.ML --- 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