# HG changeset patch # User kuncar # Date 1417785276 -3600 # Node ID eb4e322734bfc382960b66add39406f494d9e773 # Parent e759afe46a8cef848809fd3e98c184b4a80b2107 note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional diff -r e759afe46a8c -r eb4e322734bf src/HOL/Tools/Lifting/lifting_def.ML --- a/src/HOL/Tools/Lifting/lifting_def.ML Tue Nov 18 16:19:57 2014 +0100 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Fri Dec 05 14:14:36 2014 +0100 @@ -20,14 +20,18 @@ val inst_of_lift_def: Proof.context -> typ -> lift_def -> lift_def val mk_lift_const_of_lift_def: typ -> lift_def -> term + type config = { notes: bool } + val default_config: config + val generate_parametric_transfer_rule: Proof.context -> thm -> thm -> thm - val add_lift_def: - binding * mixfix -> typ -> term -> thm -> thm list -> local_theory -> lift_def * local_theory + val add_lift_def: + config -> binding * mixfix -> typ -> term -> thm -> thm list -> local_theory -> + lift_def * local_theory val lift_def: - binding * mixfix -> typ -> term -> (Proof.context -> tactic) -> thm list -> + config -> binding * mixfix -> typ -> term -> (Proof.context -> tactic) -> thm list -> local_theory -> lift_def * local_theory val lift_def_cmd: @@ -98,6 +102,11 @@ fun inst_of_lift_def ctxt qty lift_def = mk_inst_of_lift_def qty lift_def |> instT_morphism ctxt |> (fn phi => morph_lift_def phi lift_def) +(* Config *) + +type config = { notes: bool }; +val default_config = { notes = true }; + (* Reflexivity prover *) fun mono_eq_prover ctxt prop = @@ -518,7 +527,7 @@ par_thms - a parametricity theorem for rhs *) -fun add_lift_def var qty rhs rsp_thm par_thms lthy = +fun add_lift_def config var qty rhs rsp_thm par_thms lthy = let val rty = fastype_of rhs val quot_thm = Lifting_Term.prove_quot_thm lthy (rty, qty) @@ -529,33 +538,41 @@ val prop = Logic.mk_equals (lhs, absrep_trm $ forced_rhs) val (_, prop') = Local_Defs.cert_def lthy prop val (_, newrhs) = Local_Defs.abs_def prop' - - val ((lift_const, (_ , def_thm)), lthy') = - Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy + val var = (#notes config = false ? apfst Binding.concealed) var + val def_name = if #notes config then Thm.def_binding (#1 var) else Binding.empty + + val ((lift_const, (_ , def_thm)), lthy) = + Local_Theory.define (var, ((def_name, []), newrhs)) lthy - val transfer_rules = generate_transfer_rules lthy' quot_thm rsp_thm def_thm par_thms + val transfer_rules = generate_transfer_rules lthy quot_thm rsp_thm def_thm par_thms - val abs_eq_thm = generate_abs_eq lthy' def_thm rsp_thm quot_thm - val opt_rep_eq_thm = generate_rep_eq lthy' def_thm rsp_thm (rty_forced, qty) + val abs_eq_thm = generate_abs_eq lthy def_thm rsp_thm quot_thm + val opt_rep_eq_thm = generate_rep_eq lthy def_thm rsp_thm (rty_forced, qty) fun qualify defname suffix = Binding.qualified true suffix defname - val lhs_name = (#1 var) - val rsp_thm_name = qualify lhs_name "rsp" - val abs_eq_thm_name = qualify lhs_name "abs_eq" - val rep_eq_thm_name = qualify lhs_name "rep_eq" - val transfer_rule_name = qualify lhs_name "transfer" - val transfer_attr = Attrib.internal (K Transfer.transfer_add) + fun notes names = + let + val lhs_name = (#1 var) + val rsp_thmN = qualify lhs_name "rsp" + val abs_eq_thmN = qualify lhs_name "abs_eq" + val rep_eq_thmN = qualify lhs_name "rep_eq" + val transfer_ruleN = qualify lhs_name "transfer" + val notes = + [(rsp_thmN, [], [rsp_thm]), + (transfer_ruleN, @{attributes [transfer_rule]}, transfer_rules), + (abs_eq_thmN, [], [abs_eq_thm])] + @ (case opt_rep_eq_thm of SOME rep_eq_thm => [(rep_eq_thmN, [], [rep_eq_thm])] | NONE => []) + in + if names then map (fn (name, attrs, thms) => ((name, []), [(thms, attrs)])) notes + else map_filter (fn (_, attrs, thms) => if null attrs then NONE + else SOME ((Binding.empty, []), [(thms, attrs)])) notes + end val lift_def = mk_lift_def rty_forced qty newrhs lift_const def_thm rsp_thm abs_eq_thm - opt_rep_eq_thm transfer_rules + opt_rep_eq_thm transfer_rules in - lthy' - |> (snd oo Local_Theory.note) ((rsp_thm_name, []), [rsp_thm]) - |> (snd oo Local_Theory.note) ((transfer_rule_name, [transfer_attr]), transfer_rules) - |> (snd oo Local_Theory.note) ((abs_eq_thm_name, []), [abs_eq_thm]) - |> (case opt_rep_eq_thm of - SOME rep_eq_thm => (snd oo Local_Theory.note) ((rep_eq_thm_name, []), [rep_eq_thm]) - | NONE => I) + lthy + |> Local_Theory.notes (notes (#notes config)) |> snd |> register_code_eq abs_eq_thm opt_rep_eq_thm (rty_forced, qty) |> ` (fn lthy => morph_lift_def (Local_Theory.target_morphism lthy) lift_def) ||> Local_Theory.restore @@ -680,7 +697,7 @@ Symtab.fold (fn (_, data) => fn l => collect data l) table [] end -fun prepare_lift_def var qty rhs par_thms lthy = +fun prepare_lift_def config var qty rhs par_thms lthy = let val rsp_rel = Lifting_Term.equiv_relation lthy (fastype_of rhs, qty) val rty_forced = (domain_type o fastype_of) rsp_rel; @@ -697,7 +714,7 @@ val opt_proven_rsp_thm = try_prove_reflexivity lthy prsp_tm fun after_qed internal_rsp_thm lthy = - add_lift_def var qty rhs (internal_rsp_thm RS to_rsp) par_thms lthy + add_lift_def config var qty rhs (internal_rsp_thm RS to_rsp) par_thms lthy in case opt_proven_rsp_thm of SOME thm => (NONE, K (after_qed thm)) @@ -720,9 +737,9 @@ end end -fun lift_def var qty rhs tac par_thms lthy = +fun lift_def config var qty rhs tac par_thms lthy = let - val (goal, after_qed) = prepare_lift_def var qty rhs par_thms lthy + val (goal, after_qed) = prepare_lift_def config var qty rhs par_thms lthy in case goal of SOME goal => @@ -748,7 +765,7 @@ val var = (binding, mx) val rhs = (Syntax.check_term lthy o Syntax.parse_term lthy) rhs_raw val par_thms = Attrib.eval_thms lthy par_xthms - val (goal, after_qed) = prepare_lift_def var qty rhs par_thms lthy + val (goal, after_qed) = prepare_lift_def default_config var qty rhs par_thms lthy in Proof.theorem NONE (snd oo after_qed) [map (rpair []) (the_list goal)] lthy end diff -r e759afe46a8c -r eb4e322734bf src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Tue Nov 18 16:19:57 2014 +0100 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Fri Dec 05 14:14:36 2014 +0100 @@ -8,9 +8,13 @@ sig exception SETUP_LIFTING_INFR of string - val setup_by_quotient: thm -> thm option -> thm option -> local_theory -> local_theory + type config = { notes: bool }; + val default_config: config; - val setup_by_typedef_thm: thm -> local_theory -> local_theory + val setup_by_quotient: config -> thm -> thm option -> thm option -> local_theory -> + binding * local_theory + + val setup_by_typedef_thm: config -> thm -> local_theory -> binding * local_theory val lifting_restore: Lifting_Info.quotient -> Context.generic -> Context.generic end @@ -24,18 +28,25 @@ exception SETUP_LIFTING_INFR of string -fun define_crel rep_fun lthy = +(* Config *) + +type config = { notes: bool }; +val default_config = { notes = true }; + +fun define_crel config rep_fun lthy = let val (qty, rty) = (dest_funT o fastype_of) rep_fun val rep_fun_graph = (HOLogic.eq_const rty) $ Bound 1 $ (rep_fun $ Bound 0) val def_term = Abs ("x", rty, Abs ("y", qty, rep_fun_graph)) val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty val crel_name = Binding.prefix_name "cr_" qty_name - val (fixed_def_term, lthy') = yield_singleton (Variable.importT_terms) def_term lthy - val ((_, (_ , def_thm)), lthy'') = - Local_Theory.define ((crel_name, NoSyn), ((Thm.def_binding crel_name, []), fixed_def_term)) lthy' - in - (def_thm, lthy'') + val (fixed_def_term, lthy) = yield_singleton (Variable.importT_terms) def_term lthy + val ((_, (_ , def_thm)), lthy) = if #notes config then + Local_Theory.define ((crel_name, NoSyn), ((Thm.def_binding crel_name, []), fixed_def_term)) lthy + else + Local_Theory.define ((Binding.concealed crel_name, NoSyn), ((Binding.empty, []), fixed_def_term)) lthy + in + (def_thm, lthy) end fun print_define_pcrel_warning msg = @@ -48,7 +59,7 @@ warning warning_msg end -fun define_pcrel crel lthy = +fun define_pcrel config crel lthy = let val (fixed_crel, lthy) = yield_singleton Variable.importT_terms crel lthy val [rty', qty] = (binder_types o fastype_of) fixed_crel @@ -67,14 +78,25 @@ (rty --> rty' --> HOLogic.boolT) --> (rty' --> qty --> HOLogic.boolT) --> rty --> qty --> HOLogic.boolT) - val relator_type = foldr1 (op -->) ((map type_of args_fixed) @ [rty, qty, HOLogic.boolT]) val qty_name = (fst o dest_Type) qty val pcrel_name = Binding.prefix_name "pcr_" ((Binding.name o Long_Name.base_name) qty_name) + val relator_type = foldr1 (op -->) ((map type_of args_fixed) @ [rty, qty, HOLogic.boolT]) val lhs = Library.foldl (op $) ((Free (Binding.name_of pcrel_name, relator_type)), args_fixed) val rhs = relcomp_op $ param_rel_fixed $ fixed_crel val definition_term = Logic.mk_equals (lhs, rhs) - val ((_, (_, def_thm)), lthy) = Specification.definition ((SOME (pcrel_name, SOME relator_type, NoSyn)), - ((Binding.empty, []), definition_term)) lthy + fun note_def lthy = + Specification.definition ((SOME (pcrel_name, SOME relator_type, NoSyn)), + ((Binding.empty, []), definition_term)) lthy |>> (snd #> snd); + fun raw_def lthy = + let + val ((_, rhs), prove) = Local_Defs.derived_def lthy true definition_term; + val ((_, (_, raw_th)), lthy) = lthy + |> Local_Theory.define ((Binding.concealed pcrel_name, NoSyn), ((Binding.empty, []), rhs)); + val th = prove lthy raw_th; + in + (th, lthy) + end + val (def_thm, lthy) = if #notes config then note_def lthy else raw_def lthy in (SOME def_thm, lthy) end @@ -96,7 +118,7 @@ error error_msg end in - fun define_pcr_cr_eq lthy pcr_rel_def = + fun define_pcr_cr_eq config lthy pcr_rel_def = let val lhs = (Thm.term_of o Thm.lhs_of) pcr_rel_def val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type o List.last o binder_types o fastype_of) lhs @@ -127,8 +149,8 @@ |> Conv.fconv_rule (Conv.arg_conv (Conv.rewr_conv eq_OO_meta)) |> mk_HOL_eq |> singleton (Variable.export lthy orig_lthy) - val ((_, [thm]), lthy) = - Local_Theory.note ((Binding.qualified true "pcr_cr_eq" qty_name, []), [thm]) lthy + val lthy = (#notes config ? (Local_Theory.note + ((Binding.qualified true "pcr_cr_eq" qty_name, []), [thm]) #> snd)) lthy in (thm, lthy) end @@ -229,18 +251,19 @@ |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Lifting_Info.init_restore_data bundle_name (phi_qinfo phi)) |> Bundle.bundle ((binding, [restore_lifting_att])) [] + |> pair binding end -fun setup_lifting_infr quot_thm opt_reflp_thm lthy = +fun setup_lifting_infr config quot_thm opt_reflp_thm lthy = let val _ = quot_thm_sanity_check lthy quot_thm val (_, qty) = quot_thm_rty_qty quot_thm - val (pcrel_def, lthy) = define_pcrel (quot_thm_crel quot_thm) lthy + val (pcrel_def, lthy) = define_pcrel config (quot_thm_crel quot_thm) lthy (**) val pcrel_def = Option.map (Morphism.thm (Local_Theory.target_morphism lthy)) pcrel_def (**) val (pcr_cr_eq, lthy) = case pcrel_def of - SOME pcrel_def => apfst SOME (define_pcr_cr_eq lthy pcrel_def) + SOME pcrel_def => apfst SOME (define_pcr_cr_eq config lthy pcrel_def) | NONE => (NONE, lthy) val pcr_info = case pcrel_def of SOME pcrel_def => SOME { pcrel_def = pcrel_def, pcr_cr_eq = the pcr_cr_eq } @@ -444,10 +467,10 @@ (dom_thm RS @{thm pcr_Domainp}) |> fold_Domainp_pcrel pcrel_def val thms = - [("domain", pcr_Domainp), - ("domain_par", pcr_Domainp_par), - ("domain_par_left_total", pcr_Domainp_par_left_total), - ("domain_eq", pcr_Domainp_eq)] + [("domain", [pcr_Domainp], @{attributes [transfer_domain_rule]}), + ("domain_par", [pcr_Domainp_par], @{attributes [transfer_domain_rule]}), + ("domain_par_left_total", [pcr_Domainp_par_left_total], @{attributes [transfer_domain_rule]}), + ("domain_eq", [pcr_Domainp_eq], @{attributes [transfer_domain_rule]})] in thms end @@ -459,7 +482,7 @@ |> fold_Domainp_pcrel pcrel_def |> reduce_Domainp ctxt (Transfer.get_relator_domain ctxt) in - [("domain", thm)] + [("domain", [thm], @{attributes [transfer_domain_rule]})] end end @@ -470,6 +493,19 @@ fun get_Domainp_thm quot_thm = the (get_first (try(curry op RS quot_thm)) [@{thm eq_onp_to_Domainp}, @{thm Quotient_to_Domainp}]) +fun notes names thms = + let + val notes = + if names then map (fn (name, thms, attrs) => ((name, []), [(thms, attrs)])) thms + else map_filter (fn (_, thms, attrs) => if null attrs then NONE + else SOME ((Binding.empty, []), [(thms, attrs)])) thms + in + Local_Theory.notes notes #> snd + end + +fun map_thms map_name map_thm thms = + map (fn (name, thms, attr) => (map_name name, map map_thm thms, attr)) thms + (* Sets up the Lifting package by a quotient theorem. @@ -479,64 +515,55 @@ opt_par_thm - a parametricity theorem for R *) -fun setup_by_quotient quot_thm opt_reflp_thm opt_par_thm lthy = +fun setup_by_quotient config quot_thm opt_reflp_thm opt_par_thm lthy = let (**) val quot_thm = Morphism.thm (Local_Theory.target_morphism lthy) quot_thm (**) - val transfer_attr = Attrib.internal (K Transfer.transfer_add) - val transfer_domain_attr = Attrib.internal (K Transfer.transfer_domain_add) val (rty, qty) = quot_thm_rty_qty quot_thm val induct_attr = Attrib.internal (K (Induct.induct_type (fst (dest_Type qty)))) val qty_full_name = (fst o dest_Type) qty val qty_name = (Binding.name o Long_Name.base_name) qty_full_name fun qualify suffix = Binding.qualified true suffix qty_name - val lthy = case opt_reflp_thm of + val notes1 = case opt_reflp_thm of SOME reflp_thm => let val thms = - [("abs_induct", @{thm Quotient_total_abs_induct}, [induct_attr]), - ("abs_eq_iff", @{thm Quotient_total_abs_eq_iff}, [] )] + [("abs_induct", @{thms Quotient_total_abs_induct}, [induct_attr]), + ("abs_eq_iff", @{thms Quotient_total_abs_eq_iff}, [] )] in - lthy - |> fold (fn (name, thm, attr) => (snd oo Local_Theory.note) ((qualify name, attr), - [[quot_thm, reflp_thm] MRSL thm])) thms + map_thms qualify (fn thm => [quot_thm, reflp_thm] MRSL thm) thms end | NONE => let val thms = - [("abs_induct", @{thm Quotient_abs_induct}, [induct_attr])] + [("abs_induct", @{thms Quotient_abs_induct}, [induct_attr])] in - fold (fn (name, thm, attr) => (snd oo Local_Theory.note) ((qualify name, attr), - [quot_thm RS thm])) thms lthy + map_thms qualify (fn thm => quot_thm RS thm) thms end val dom_thm = get_Domainp_thm quot_thm - fun setup_transfer_rules_nonpar lthy = + fun setup_transfer_rules_nonpar notes = let - val lthy = + val notes1 = case opt_reflp_thm of SOME reflp_thm => let val thms = - [("id_abs_transfer",@{thm Quotient_id_abs_transfer}), - ("left_total", @{thm Quotient_left_total} ), - ("bi_total", @{thm Quotient_bi_total})] + [("id_abs_transfer",@{thms Quotient_id_abs_transfer}, @{attributes [transfer_rule]}), + ("left_total", @{thms Quotient_left_total}, @{attributes [transfer_rule]}), + ("bi_total", @{thms Quotient_bi_total}, @{attributes [transfer_rule]})] in - fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), - [[quot_thm, reflp_thm] MRSL thm])) thms lthy + map_thms qualify (fn thm => [quot_thm, reflp_thm] MRSL thm) thms end - | NONE => - lthy - |> (snd oo Local_Theory.note) ((qualify "domain", [transfer_domain_attr]), [dom_thm]) + | NONE => map_thms qualify I [("domain", [dom_thm], @{attributes [transfer_domain_rule]})] - val thms = - [("rel_eq_transfer", @{thm Quotient_rel_eq_transfer}), - ("right_unique", @{thm Quotient_right_unique} ), - ("right_total", @{thm Quotient_right_total} )] + val notes2 = map_thms qualify (fn thm => quot_thm RS thm) + [("rel_eq_transfer", @{thms Quotient_rel_eq_transfer}, @{attributes [transfer_rule]}), + ("right_unique", @{thms Quotient_right_unique}, @{attributes [transfer_rule]}), + ("right_total", @{thms Quotient_right_total}, @{attributes [transfer_rule]})] in - fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), - [quot_thm RS thm])) thms lthy + notes2 @ notes1 @ notes end fun generate_parametric_rel_eq lthy transfer_rule opt_param_thm = @@ -551,11 +578,11 @@ error error_msg end - fun setup_transfer_rules_par lthy = + fun setup_transfer_rules_par lthy notes = let val pcrel_info = (the (get_pcrel_info lthy qty_full_name)) val pcrel_def = #pcrel_def pcrel_info - val lthy = + val notes1 = case opt_reflp_thm of SOME reflp_thm => let @@ -568,22 +595,17 @@ val left_total = parametrize_class_constraint lthy pcrel_def left_total val bi_total = parametrize_class_constraint lthy pcrel_def bi_total val thms = - [("id_abs_transfer",id_abs_transfer), - ("left_total", left_total ), - ("bi_total", bi_total )] + [("id_abs_transfer", [id_abs_transfer], @{attributes [transfer_rule]}), + ("left_total", [left_total], @{attributes [transfer_rule]}), + ("bi_total", [bi_total], @{attributes [transfer_rule]})] in - lthy - |> fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), - [thm])) thms - |> fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_domain_attr]), - [thm])) domain_thms + map_thms qualify I thms @ map_thms qualify I domain_thms end | NONE => let val thms = parametrize_domain dom_thm pcrel_info lthy in - fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_domain_attr]), - [thm])) thms lthy + map_thms qualify I thms end val rel_eq_transfer = generate_parametric_rel_eq lthy @@ -593,22 +615,25 @@ (quot_thm RS @{thm Quotient_right_unique}) val right_total = parametrize_class_constraint lthy pcrel_def (quot_thm RS @{thm Quotient_right_total}) - val thms = - [("rel_eq_transfer", rel_eq_transfer), - ("right_unique", right_unique ), - ("right_total", right_total )] + val notes2 = map_thms qualify I + [("rel_eq_transfer", [rel_eq_transfer], @{attributes [transfer_rule]}), + ("right_unique", [right_unique], @{attributes [transfer_rule]}), + ("right_total", [right_total], @{attributes [transfer_rule]})] in - fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), - [thm])) thms lthy + notes2 @ notes1 @ notes end - fun setup_transfer_rules lthy = - if is_some (get_pcrel_info lthy qty_full_name) then setup_transfer_rules_par lthy - else setup_transfer_rules_nonpar lthy + fun setup_rules lthy = + let + val thms = if is_some (get_pcrel_info lthy qty_full_name) + then setup_transfer_rules_par lthy notes1 else setup_transfer_rules_nonpar notes1 + in + notes (#notes config) thms lthy + end in lthy - |> setup_lifting_infr quot_thm opt_reflp_thm - |> setup_transfer_rules + |> setup_lifting_infr config quot_thm opt_reflp_thm + ||> setup_rules end (* @@ -619,12 +644,10 @@ typedef_thm - a typedef theorem (type_definition Rep Abs S) *) -fun setup_by_typedef_thm typedef_thm lthy = +fun setup_by_typedef_thm config typedef_thm lthy = let - val transfer_attr = Attrib.internal (K Transfer.transfer_add) - val transfer_domain_attr = Attrib.internal (K Transfer.transfer_domain_add) val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o Thm.prop_of) typedef_thm - val (T_def, lthy) = define_crel rep_fun lthy + val (T_def, lthy) = define_crel config rep_fun lthy (**) val T_def = Morphism.thm (Local_Theory.target_morphism lthy) T_def (**) @@ -646,40 +669,37 @@ | _ => NONE val dom_thm = get_Domainp_thm quot_thm - fun setup_transfer_rules_nonpar lthy = + fun setup_transfer_rules_nonpar notes = let - val lthy = + val notes1 = case opt_reflp_thm of SOME reflp_thm => let val thms = - [("id_abs_transfer",@{thm Quotient_id_abs_transfer}), - ("left_total", @{thm Quotient_left_total} ), - ("bi_total", @{thm Quotient_bi_total} )] + [("id_abs_transfer",@{thms Quotient_id_abs_transfer}, @{attributes [transfer_rule]}), + ("left_total", @{thms Quotient_left_total}, @{attributes [transfer_rule]}), + ("bi_total", @{thms Quotient_bi_total}, @{attributes [transfer_rule]})] in - fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), - [[quot_thm, reflp_thm] MRSL thm])) thms lthy + map_thms qualify (fn thm => [quot_thm, reflp_thm] MRSL thm) thms end | NONE => - lthy - |> (snd oo Local_Theory.note) ((qualify "domain", [transfer_domain_attr]), [dom_thm]) + map_thms qualify I [("domain", [dom_thm], @{attributes [transfer_domain_rule]})] val thms = - [("rep_transfer", @{thm typedef_rep_transfer}), - ("left_unique", @{thm typedef_left_unique} ), - ("right_unique", @{thm typedef_right_unique}), - ("right_total", @{thm typedef_right_total} ), - ("bi_unique", @{thm typedef_bi_unique} )] - in - fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), - [[typedef_thm, T_def] MRSL thm])) thms lthy + [("rep_transfer", @{thms typedef_rep_transfer}, @{attributes [transfer_rule]}), + ("left_unique", @{thms typedef_left_unique}, @{attributes [transfer_rule]}), + ("right_unique", @{thms typedef_right_unique}, @{attributes [transfer_rule]}), + ("right_total", @{thms typedef_right_total}, @{attributes [transfer_rule]}), + ("bi_unique", @{thms typedef_bi_unique}, @{attributes [transfer_rule]})] + in + map_thms qualify (fn thm => [typedef_thm, T_def] MRSL thm) thms @ notes1 @ notes end - fun setup_transfer_rules_par lthy = + fun setup_transfer_rules_par lthy notes = let val pcrel_info = (the (get_pcrel_info lthy qty_full_name)) val pcrel_def = #pcrel_def pcrel_info - val lthy = + val notes1 = case opt_reflp_thm of SOME reflp_thm => let @@ -692,48 +712,46 @@ (Lifting_Term.parametrize_transfer_rule lthy ([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer})) val thms = - [("left_total", left_total ), - ("bi_total", bi_total ), - ("id_abs_transfer",id_abs_transfer)] + [("left_total", [left_total], @{attributes [transfer_rule]}), + ("bi_total", [bi_total], @{attributes [transfer_rule]}), + ("id_abs_transfer",[id_abs_transfer], @{attributes [transfer_rule]})] in - lthy - |> fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), - [thm])) thms - |> fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_domain_attr]), - [thm])) domain_thms + map_thms qualify I thms @ map_thms qualify I domain_thms end | NONE => let val thms = parametrize_domain dom_thm pcrel_info lthy in - fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_domain_attr]), - [thm])) thms lthy + map_thms qualify I thms end - val thms = - ("rep_transfer", generate_parametric_id lthy rty - (Lifting_Term.parametrize_transfer_rule lthy ([typedef_thm, T_def] MRSL @{thm typedef_rep_transfer}))) - :: - (map_snd (fn thm => parametrize_class_constraint lthy pcrel_def ([typedef_thm, T_def] MRSL thm)) - [("left_unique", @{thm typedef_left_unique} ), - ("right_unique", @{thm typedef_right_unique}), - ("bi_unique", @{thm typedef_bi_unique} ), - ("right_total", @{thm typedef_right_total} )]) + val notes2 = map_thms qualify (fn thm => generate_parametric_id lthy rty + (Lifting_Term.parametrize_transfer_rule lthy ([typedef_thm, T_def] MRSL thm))) + [("rep_transfer", @{thms typedef_rep_transfer}, @{attributes [transfer_rule]})]; + val notes3 = + map_thms qualify + (fn thm => parametrize_class_constraint lthy pcrel_def ([typedef_thm, T_def] MRSL thm)) + [("left_unique", @{thms typedef_left_unique}, @{attributes [transfer_rule]}), + ("right_unique", @{thms typedef_right_unique},@{attributes [transfer_rule]}), + ("bi_unique", @{thms typedef_bi_unique}, @{attributes [transfer_rule]}), + ("right_total", @{thms typedef_right_total}, @{attributes [transfer_rule]})] in - fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]), - [thm])) thms lthy + notes3 @ notes2 @ notes1 @ notes end - fun setup_transfer_rules lthy = - if is_some (get_pcrel_info lthy qty_full_name) then setup_transfer_rules_par lthy - else setup_transfer_rules_nonpar lthy + val notes1 = [(Binding.prefix_name "Quotient_" qty_name, [quot_thm], [])] + fun setup_rules lthy = + let + val thms = if is_some (get_pcrel_info lthy qty_full_name) + then setup_transfer_rules_par lthy notes1 else setup_transfer_rules_nonpar notes1 + in + notes (#notes config) thms lthy + end in lthy - |> (snd oo Local_Theory.note) ((Binding.prefix_name "Quotient_" qty_name, []), - [quot_thm]) - |> setup_lifting_infr quot_thm opt_reflp_thm - |> setup_transfer_rules + |> setup_lifting_infr config quot_thm opt_reflp_thm + ||> setup_rules end fun setup_lifting_cmd xthm opt_reflp_xthm opt_par_xthm lthy = @@ -755,7 +773,8 @@ fun check_qty qty = if not (is_Type qty) then error "The abstract type must be a type constructor." else () - + val config = { notes = true } + fun setup_quotient () = let val opt_reflp_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_reflp_xthm @@ -763,7 +782,7 @@ val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm val _ = check_qty (snd (quot_thm_rty_qty input_thm)) in - setup_by_quotient input_thm opt_reflp_thm opt_par_thm lthy + setup_by_quotient config input_thm opt_reflp_thm opt_par_thm lthy |> snd end fun setup_typedef () = @@ -776,7 +795,7 @@ | NONE => ( case opt_par_xthm of SOME _ => error "The parametricity theorem cannot be specified if the type_definition theorem is used." - | NONE => setup_by_typedef_thm input_thm lthy + | NONE => setup_by_typedef_thm config input_thm lthy |> snd ) end in diff -r e759afe46a8c -r eb4e322734bf src/HOL/Tools/Quotient/quotient_type.ML --- a/src/HOL/Tools/Quotient/quotient_type.ML Tue Nov 18 16:19:57 2014 +0100 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Fri Dec 05 14:14:36 2014 +0100 @@ -125,9 +125,11 @@ | Const (@{const_name part_equivp}, _) $ _ => (NONE, [quot3_thm, T_def] MRSL @{thm Quotient3_to_Quotient}) | _ => error "unsupported equivalence theorem") + val config = { notes = true } in lthy' - |> Lifting_Setup.setup_by_quotient quot_thm reflp_thm opt_par_thm + |> Lifting_Setup.setup_by_quotient config quot_thm reflp_thm opt_par_thm + |> snd |> (snd oo Local_Theory.note) ((quotient_thm_name, []), [quot_thm]) end