--- a/src/HOL/Tools/Lifting/lifting_setup.ML Fri Mar 08 11:28:20 2013 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Fri Mar 08 13:14:23 2013 +0100
@@ -8,7 +8,7 @@
sig
exception SETUP_LIFTING_INFR of string
- val setup_by_quotient: bool -> thm -> thm option -> local_theory -> local_theory
+ val setup_by_quotient: bool -> thm -> thm option -> thm option -> local_theory -> local_theory
val setup_by_typedef_thm: bool -> thm -> local_theory -> local_theory
end;
@@ -26,7 +26,7 @@
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 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
@@ -69,7 +69,7 @@
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 lhs = Library.foldl (op $) ((Free (Binding.name_of pcrel_name, relator_type)), args_fixed)
- val rhs = relcomp_op $ param_rel_fixed $ fixed_crel;
+ 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
@@ -78,16 +78,72 @@
end
handle Lifting_Term.PARAM_QUOT_THM (_, msg) => (print_define_pcrel_warning msg; (NONE, lthy))
+
+local
+ val eq_OO_meta = mk_meta_eq @{thm eq_OO}
+
+ fun print_generate_pcr_cr_eq_error ctxt term =
+ let
+ val goal = (Const ("HOL.eq", dummyT)) $ term $ Const ("HOL.eq", dummyT)
+ val error_msg = cat_lines
+ ["Generation of a pcr_cr_eq failed.",
+ (Pretty.string_of (Pretty.block
+ [Pretty.str "Reason: Cannot prove this: ", Pretty.brk 2, Syntax.pretty_term ctxt goal])),
+ "Most probably a relator_eq rule for one of the involved types is missing."]
+ in
+ error error_msg
+ end
+in
+ fun define_pcr_cr_eq lthy pcr_rel_def =
+ let
+ val lhs = (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
+ val args = (snd o strip_comb) lhs
+
+ fun make_inst var ctxt =
+ let
+ val typ = (snd o relation_types o snd o dest_Var) var
+ val sort = Type.sort_of_atyp typ
+ val (fresh_var, ctxt) = yield_singleton Variable.invent_types sort ctxt
+ val thy = Proof_Context.theory_of ctxt
+ in
+ ((cterm_of thy var, cterm_of thy (HOLogic.eq_const (TFree fresh_var))), ctxt)
+ end
+
+ val orig_lthy = lthy
+ val (args_inst, lthy) = fold_map make_inst args lthy
+ val pcr_cr_eq =
+ pcr_rel_def
+ |> Drule.cterm_instantiate args_inst
+ |> Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (bottom_rewr_conv (Transfer.get_relator_eq lthy))))
+ in
+ case (term_of o Thm.rhs_of) pcr_cr_eq of
+ Const (@{const_name "relcompp"}, _) $ Const ("HOL.eq", _) $ _ =>
+ let
+ val thm =
+ pcr_cr_eq
+ |> 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
+ in
+ (thm, lthy)
+ end
+ | Const (@{const_name "relcompp"}, _) $ t $ _ => print_generate_pcr_cr_eq_error lthy t
+ | _ => error "generate_pcr_cr_eq: implementation error"
+ end
+end
+
fun define_code_constr gen_code quot_thm lthy =
let
val abs = quot_thm_abs quot_thm
- val abs_background = Morphism.term (Local_Theory.target_morphism lthy) abs
in
- if gen_code andalso is_Const abs_background then
+ if gen_code andalso is_Const abs then
let
- val (fixed_abs_background, lthy') = yield_singleton(Variable.importT_terms) abs_background lthy
+ val (fixed_abs, lthy') = yield_singleton(Variable.importT_terms) abs lthy
in
- Local_Theory.background_theory(Code.add_datatype [dest_Const fixed_abs_background]) lthy'
+ Local_Theory.background_theory(Code.add_datatype [dest_Const fixed_abs]) lthy'
end
else
lthy
@@ -99,7 +155,7 @@
val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
val add_abstype_attribute =
Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I)
- val add_abstype_attrib = Attrib.internal (K add_abstype_attribute);
+ val add_abstype_attrib = Attrib.internal (K add_abstype_attribute)
in
lthy
|> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm])
@@ -133,15 +189,24 @@
@ (map Pretty.string_of errs)))
end
-fun setup_lifting_infr gen_code quot_thm maybe_reflp_thm lthy =
+fun setup_lifting_infr gen_code quot_thm opt_reflp_thm lthy =
let
val _ = quot_thm_sanity_check lthy quot_thm
val (_, qtyp) = quot_thm_rty_qty quot_thm
val (pcrel_def, lthy) = define_pcrel (quot_thm_crel quot_thm) lthy
- val quotients = { quot_thm = quot_thm, pcrel_def = pcrel_def }
+ (**)
+ 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)
+ | NONE => (NONE, lthy)
+ val pcrel_info = case pcrel_def of
+ SOME pcrel_def => SOME { pcrel_def = pcrel_def, pcr_cr_eq = the pcr_cr_eq }
+ | NONE => NONE
+ val quotients = { quot_thm = quot_thm, pcrel_info = pcrel_info }
val qty_full_name = (fst o dest_Type) qtyp
fun quot_info phi = Lifting_Info.transform_quotients phi quotients
- val lthy = case maybe_reflp_thm of
+ val lthy = case opt_reflp_thm of
SOME reflp_thm => lthy
|> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflexivity_rule_attrib]),
[reflp_thm])
@@ -156,51 +221,247 @@
(fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
end
+local
+ val OO_rules = [@{thm bi_total_OO}, @{thm bi_unique_OO}, @{thm right_total_OO}, @{thm right_unique_OO}]
+in
+ fun parametrize_class_constraint ctxt pcr_def constraint =
+ let
+ fun generate_transfer_rule pcr_def constraint goal ctxt =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val orig_ctxt = ctxt
+ val (fixed_goal, ctxt) = yield_singleton (Variable.import_terms true) goal ctxt
+ val init_goal = Goal.init (cterm_of thy fixed_goal)
+ val rules = Transfer.get_transfer_raw ctxt
+ val rules = constraint :: OO_rules @ rules
+ val tac = K (Local_Defs.unfold_tac ctxt [pcr_def]) THEN' REPEAT_ALL_NEW (resolve_tac rules)
+ in
+ (singleton (Variable.export ctxt orig_ctxt) o Goal.conclude) (the (SINGLE (tac 1) init_goal))
+ end
+
+ fun make_goal pcr_def constr =
+ let
+ val pred_name = (fst o dest_Const o strip_args 1 o HOLogic.dest_Trueprop o prop_of) constr
+ val arg = (fst o Logic.dest_equals o prop_of) pcr_def
+ in
+ HOLogic.mk_Trueprop ((Const (pred_name, (fastype_of arg) --> HOLogic.boolT)) $ arg)
+ end
+
+ val check_assms =
+ let
+ val right_names = ["bi_total", "bi_unique", "right_total", "right_unique"]
+
+ fun is_right_name name = member op= right_names (Long_Name.base_name name)
+
+ fun is_trivial_assm (Const (name, _) $ Var (_, _)) = is_right_name name
+ | is_trivial_assm (Const (name, _) $ Free (_, _)) = is_right_name name
+ | is_trivial_assm _ = false
+ in
+ fn thm =>
+ let
+ val prems = map HOLogic.dest_Trueprop (prems_of thm)
+ val thm_name = (Long_Name.base_name o fst o dest_Const o strip_args 1 o HOLogic.dest_Trueprop o concl_of) thm
+ val non_trivial_assms = filter_out is_trivial_assm prems
+ in
+ if null non_trivial_assms then ()
+ else
+ let
+ val pretty_msg = Pretty.block ([Pretty.str "Non-trivial assumptions in ",
+ Pretty.str thm_name,
+ Pretty.str " transfer rule found:",
+ Pretty.brk 1] @
+ ((Pretty.commas o map (Syntax.pretty_term ctxt)) non_trivial_assms) @
+ [Pretty.str "."])
+ in
+ warning (Pretty.str_of pretty_msg)
+ end
+ end
+ end
+
+ val goal = make_goal pcr_def constraint
+ val thm = generate_transfer_rule pcr_def constraint goal ctxt
+ val _ = check_assms thm
+ in
+ thm
+ end
+end
+
+local
+ val id_unfold = (Conv.rewr_conv (mk_meta_eq @{thm id_def}))
+in
+ fun generate_parametric_id lthy rty id_transfer_rule =
+ let
+ val orig_lthy = lthy
+ (* it doesn't raise an exception because it would have already raised it in define_pcrel *)
+ val (quot_thm, _, lthy) = Lifting_Term.prove_param_quot_thm lthy rty
+ val parametrized_relator = singleton (Variable.export_terms lthy orig_lthy) (quot_thm_crel quot_thm);
+ val lthy = orig_lthy
+ val id_transfer =
+ @{thm id_transfer}
+ |> Thm.incr_indexes (Term.maxidx_of_term parametrized_relator + 1)
+ |> Conv.fconv_rule(HOLogic.Trueprop_conv (Conv.arg_conv id_unfold then_conv Conv.arg1_conv id_unfold))
+ val var = Var (hd (Term.add_vars (prop_of id_transfer) []));
+ val thy = Proof_Context.theory_of lthy;
+ val inst = [(cterm_of thy var, cterm_of thy parametrized_relator)]
+ val id_par_thm = Drule.cterm_instantiate inst id_transfer;
+ in
+ Lifting_Def.generate_parametric_transfer_rule lthy id_transfer_rule id_par_thm
+ end
+ handle Lifting_Term.MERGE_TRANSFER_REL msg =>
+ let
+ val error_msg = cat_lines
+ ["Generation of a parametric transfer rule for the abs. or the rep. function failed.",
+ "A non-parametric version will be used.",
+ (Pretty.string_of (Pretty.block
+ [Pretty.str "Reason:", Pretty.brk 2, msg]))]
+ in
+ (warning error_msg; id_transfer_rule)
+ end
+end
+
+fun parametrize_quantifier lthy quant_transfer_rule =
+ Lifting_Term.parametrize_transfer_rule lthy quant_transfer_rule
+
+fun get_pcrel_info ctxt qty_full_name =
+ #pcrel_info (the (Lifting_Info.lookup_quotients ctxt qty_full_name))
+
(*
Sets up the Lifting package by a quotient theorem.
gen_code - flag if an abstract type given by quot_thm should be registred
as an abstract type in the code generator
quot_thm - a quotient theorem (Quotient R Abs Rep T)
- maybe_reflp_thm - a theorem saying that a relation from quot_thm is reflexive
+ opt_reflp_thm - a theorem saying that a relation from quot_thm is reflexive
(in the form "reflp R")
*)
-fun setup_by_quotient gen_code quot_thm maybe_reflp_thm lthy =
+fun setup_by_quotient gen_code 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 (_, qty) = quot_thm_rty_qty quot_thm
+ val (rty, qty) = quot_thm_rty_qty quot_thm
val induct_attr = Attrib.internal (K (Induct.induct_type (fst (dest_Type qty))))
- val qty_name = (Binding.name o Long_Name.base_name o fst o 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 maybe_reflp_thm of
- SOME reflp_thm => lthy
- |> (snd oo Local_Theory.note) ((qualify "bi_total", [transfer_attr]),
- [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}])
- |> (snd oo Local_Theory.note) ((qualify "id_abs_transfer", [transfer_attr]),
- [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
- |> (snd oo Local_Theory.note) ((qualify "abs_induct", [induct_attr]),
- [[quot_thm, reflp_thm] MRSL @{thm Quotient_total_abs_induct}])
- |> (snd oo Local_Theory.note) ((qualify "abs_eq_iff", []),
- [[quot_thm, reflp_thm] MRSL @{thm Quotient_total_abs_eq_iff}])
- | NONE => lthy
- |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]),
- [quot_thm RS @{thm Quotient_All_transfer}])
- |> (snd oo Local_Theory.note) ((qualify "Ex_transfer", [transfer_attr]),
- [quot_thm RS @{thm Quotient_Ex_transfer}])
- |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]),
- [quot_thm RS @{thm Quotient_forall_transfer}])
- |> (snd oo Local_Theory.note) ((qualify "abs_induct", [induct_attr]),
- [quot_thm RS @{thm Quotient_abs_induct}])
+ val lthy = 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}, [] )]
+ in
+ lthy
+ |> fold (fn (name, thm, attr) => (snd oo Local_Theory.note) ((qualify name, attr),
+ [[quot_thm, reflp_thm] MRSL thm])) thms
+ end
+ | NONE =>
+ let
+ val thms =
+ [("abs_induct", @{thm 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
+ end
+
+ fun setup_transfer_rules_nonpar lthy =
+ let
+ val lthy =
+ case opt_reflp_thm of
+ SOME reflp_thm =>
+ let
+ val thms =
+ [("id_abs_transfer",@{thm Quotient_id_abs_transfer}),
+ ("bi_total", @{thm Quotient_bi_total} )]
+ in
+ fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
+ [[quot_thm, reflp_thm] MRSL thm])) thms lthy
+ end
+ | NONE =>
+ let
+ val thms =
+ [("All_transfer", @{thm Quotient_All_transfer} ),
+ ("Ex_transfer", @{thm Quotient_Ex_transfer} ),
+ ("forall_transfer",@{thm Quotient_forall_transfer})]
+ in
+ fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
+ [quot_thm RS thm])) thms lthy
+ end
+ val thms =
+ [("rel_eq_transfer", @{thm Quotient_rel_eq_transfer}),
+ ("right_unique", @{thm Quotient_right_unique} ),
+ ("right_total", @{thm Quotient_right_total} )]
+ in
+ fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
+ [quot_thm RS thm])) thms lthy
+ end
+
+ fun generate_parametric_rel_eq lthy transfer_rule opt_param_thm =
+ option_fold transfer_rule (Lifting_Def.generate_parametric_transfer_rule lthy transfer_rule) opt_param_thm
+ handle Lifting_Term.MERGE_TRANSFER_REL msg =>
+ let
+ val error_msg = cat_lines
+ ["Generation of a parametric transfer rule for the quotient relation failed.",
+ (Pretty.string_of (Pretty.block
+ [Pretty.str "Reason:", Pretty.brk 2, msg]))]
+ in
+ error error_msg
+ end
+
+ fun setup_transfer_rules_par lthy =
+ let
+ val pcrel_def = #pcrel_def (the (get_pcrel_info lthy qty_full_name))
+ val lthy =
+ case opt_reflp_thm of
+ SOME reflp_thm =>
+ let
+ val id_abs_transfer = generate_parametric_id lthy rty
+ (Lifting_Term.parametrize_transfer_rule lthy
+ ([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}))
+ val bi_total = parametrize_class_constraint lthy pcrel_def
+ ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total})
+ val thms =
+ [("id_abs_transfer",id_abs_transfer),
+ ("bi_total", bi_total )]
+ in
+ fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
+ [thm])) thms lthy
+ end
+ | NONE =>
+ let
+ val thms =
+ [("All_transfer", @{thm Quotient_All_transfer} ),
+ ("Ex_transfer", @{thm Quotient_Ex_transfer} ),
+ ("forall_transfer",@{thm Quotient_forall_transfer})]
+ in
+ fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
+ [parametrize_quantifier lthy (quot_thm RS thm)])) thms lthy
+ end
+ val rel_eq_transfer = generate_parametric_rel_eq lthy
+ (Lifting_Term.parametrize_transfer_rule lthy (quot_thm RS @{thm Quotient_rel_eq_transfer}))
+ opt_par_thm
+ val right_unique = parametrize_class_constraint lthy pcrel_def
+ (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 )]
+ in
+ fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
+ [thm])) thms lthy
+ 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
in
lthy
- |> (snd oo Local_Theory.note) ((qualify "right_unique", [transfer_attr]),
- [quot_thm RS @{thm Quotient_right_unique}])
- |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]),
- [quot_thm RS @{thm Quotient_right_total}])
- |> (snd oo Local_Theory.note) ((qualify "rel_eq_transfer", [transfer_attr]),
- [quot_thm RS @{thm Quotient_rel_eq_transfer}])
- |> setup_lifting_infr gen_code quot_thm maybe_reflp_thm
+ |> setup_lifting_infr gen_code quot_thm opt_reflp_thm
+ |> setup_transfer_rules
end
(*
@@ -215,8 +476,10 @@
let
val transfer_attr = Attrib.internal (K Transfer.transfer_add)
val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
- val (T_def, lthy') = define_crel rep_fun lthy
-
+ val (T_def, lthy) = define_crel rep_fun lthy
+ (**)
+ val T_def = Morphism.thm (Local_Theory.target_morphism lthy) T_def
+ (**)
val quot_thm = case typedef_set of
Const ("Orderings.top_class.top", _) =>
[typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient}
@@ -224,49 +487,109 @@
[typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
| _ =>
[typedef_thm, T_def] MRSL @{thm typedef_to_Quotient}
-
- val (_, qty) = quot_thm_rty_qty quot_thm
- val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty
+ val (rty, qty) = quot_thm_rty_qty quot_thm
+ 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 simplify = Raw_Simplifier.rewrite_rule [mk_meta_eq @{thm mem_Collect_eq}]
+ val opt_reflp_thm =
+ case typedef_set of
+ Const ("Orderings.top_class.top", _) =>
+ SOME ((typedef_thm RS @{thm UNIV_typedef_to_equivp}) RS @{thm equivp_reflp2})
+ | _ => NONE
- val (maybe_reflp_thm, lthy'') = case typedef_set of
- Const ("Orderings.top_class.top", _) =>
- let
- val equivp_thm = typedef_thm RS @{thm UNIV_typedef_to_equivp}
- val reflp_thm = equivp_thm RS @{thm equivp_reflp2}
- in
- lthy'
- |> (snd oo Local_Theory.note) ((qualify "bi_total", [transfer_attr]),
- [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}])
- |> (snd oo Local_Theory.note) ((qualify "id_abs_transfer", [transfer_attr]),
- [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
- |> pair (SOME reflp_thm)
- end
- | _ => lthy'
- |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]),
- [[typedef_thm, T_def] MRSL @{thm typedef_All_transfer}])
- |> (snd oo Local_Theory.note) ((qualify "Ex_transfer", [transfer_attr]),
- [[typedef_thm, T_def] MRSL @{thm typedef_Ex_transfer}])
- |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]),
- [simplify ([typedef_thm, T_def] MRSL @{thm typedef_forall_transfer})])
- |> pair NONE
+ fun setup_transfer_rules_nonpar lthy =
+ let
+ val lthy =
+ case opt_reflp_thm of
+ SOME reflp_thm =>
+ let
+ val thms =
+ [("id_abs_transfer",@{thm Quotient_id_abs_transfer}),
+ ("bi_total", @{thm Quotient_bi_total} )]
+ in
+ fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
+ [[quot_thm, reflp_thm] MRSL thm])) thms lthy
+ end
+ | NONE =>
+ let
+ val thms =
+ [("All_transfer", @{thm typedef_All_transfer} ),
+ ("Ex_transfer", @{thm typedef_Ex_transfer} )]
+ in
+ lthy
+ |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]),
+ [simplify ([typedef_thm, T_def] MRSL @{thm typedef_forall_transfer})])
+ |> fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
+ [[typedef_thm, T_def] MRSL thm])) thms
+ end
+ val thms =
+ [("rep_transfer", @{thm typedef_rep_transfer}),
+ ("bi_unique", @{thm typedef_bi_unique} ),
+ ("right_unique", @{thm typedef_right_unique}),
+ ("right_total", @{thm typedef_right_total} )]
+ in
+ fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
+ [[typedef_thm, T_def] MRSL thm])) thms lthy
+ end
+
+ fun setup_transfer_rules_par lthy =
+ let
+ val pcrel_def = #pcrel_def (the (get_pcrel_info lthy qty_full_name))
+ val lthy =
+ case opt_reflp_thm of
+ SOME reflp_thm =>
+ let
+ val id_abs_transfer = generate_parametric_id lthy rty
+ (Lifting_Term.parametrize_transfer_rule lthy
+ ([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}))
+ val bi_total = parametrize_class_constraint lthy pcrel_def
+ ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total})
+ val thms =
+ [("id_abs_transfer",id_abs_transfer),
+ ("bi_total", bi_total )]
+ in
+ fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
+ [thm])) thms lthy
+ end
+ | NONE =>
+ let
+ val thms =
+ ("forall_transfer", simplify ([typedef_thm, T_def] MRSL @{thm typedef_forall_transfer}))
+ ::
+ (map_snd (fn thm => [typedef_thm, T_def] MRSL thm)
+ [("All_transfer", @{thm typedef_All_transfer}),
+ ("Ex_transfer", @{thm typedef_Ex_transfer} )])
+ in
+ fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
+ [parametrize_quantifier lthy thm])) thms lthy
+ 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))
+ [("bi_unique", @{thm typedef_bi_unique} ),
+ ("right_unique", @{thm typedef_right_unique}),
+ ("right_total", @{thm typedef_right_total} )])
+ in
+ fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
+ [thm])) thms lthy
+ 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
+
in
- lthy''
+ lthy
|> (snd oo Local_Theory.note) ((Binding.prefix_name "Quotient_" qty_name, []),
- [quot_thm])
- |> (snd oo Local_Theory.note) ((qualify "bi_unique", [transfer_attr]),
- [[typedef_thm, T_def] MRSL @{thm typedef_bi_unique}])
- |> (snd oo Local_Theory.note) ((qualify "rep_transfer", [transfer_attr]),
- [[typedef_thm, T_def] MRSL @{thm typedef_rep_transfer}])
- |> (snd oo Local_Theory.note) ((qualify "right_unique", [transfer_attr]),
- [[quot_thm] MRSL @{thm Quotient_right_unique}])
- |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]),
- [[quot_thm] MRSL @{thm Quotient_right_total}])
- |> setup_lifting_infr gen_code quot_thm maybe_reflp_thm
+ [quot_thm])
+ |> setup_lifting_infr gen_code quot_thm opt_reflp_thm
+ |> setup_transfer_rules
end
-fun setup_lifting_cmd gen_code xthm opt_reflp_xthm lthy =
+fun setup_lifting_cmd gen_code xthm opt_reflp_xthm opt_par_xthm lthy =
let
val input_thm = singleton (Attrib.eval_thms lthy) xthm
val input_term = (HOLogic.dest_Trueprop o prop_of) input_thm
@@ -283,15 +606,14 @@
end
fun setup_quotient () =
- case opt_reflp_xthm of
- SOME reflp_xthm =>
- let
- val reflp_thm = singleton (Attrib.eval_thms lthy) reflp_xthm
- val _ = sanity_check_reflp_thm reflp_thm
- in
- setup_by_quotient gen_code input_thm (SOME reflp_thm) lthy
- end
- | NONE => setup_by_quotient gen_code input_thm NONE lthy
+ let
+ val opt_reflp_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_reflp_xthm
+ val _ = if is_some opt_reflp_thm then sanity_check_reflp_thm (the opt_reflp_thm) else ()
+ val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm
+ in
+ setup_by_quotient gen_code input_thm opt_reflp_thm opt_par_thm lthy
+ end
+
fun setup_typedef () =
case opt_reflp_xthm of
@@ -310,6 +632,8 @@
val _ =
Outer_Syntax.local_theory @{command_spec "setup_lifting"}
"setup lifting infrastructure"
- (opt_gen_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm >>
- (fn ((gen_code, xthm), opt_reflp_xthm) => setup_lifting_cmd gen_code xthm opt_reflp_xthm))
+ (opt_gen_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm
+ -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse_Spec.xthm) >>
+ (fn (((gen_code, xthm), opt_reflp_xthm), opt_par_xthm) =>
+ setup_lifting_cmd gen_code xthm opt_reflp_xthm opt_par_xthm))
end;