tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
(* Title: HOL/Tools/Lifting/lifting_setup.ML
Author: Ondrej Kuncar
Setting up the lifting infrastructure.
*)
signature LIFTING_SETUP =
sig
exception SETUP_LIFTING_INFR of string
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;
structure Lifting_Setup: LIFTING_SETUP =
struct
open Lifting_Util
infix 0 MRSL
exception SETUP_LIFTING_INFR of string
fun define_crel 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'')
end
fun print_define_pcrel_warning msg =
let
val warning_msg = cat_lines
["Generation of a parametrized correspondence relation failed.",
(Pretty.string_of (Pretty.block
[Pretty.str "Reason:", Pretty.brk 2, msg]))]
in
warning warning_msg
end
fun define_pcrel crel lthy =
let
val (fixed_crel, lthy) = yield_singleton Variable.importT_terms crel lthy
val [rty', qty] = (binder_types o fastype_of) fixed_crel
val (param_rel, args) = Lifting_Term.generate_parametrized_relator lthy rty'
val rty_raw = (domain_type o range_type o fastype_of) param_rel
val thy = Proof_Context.theory_of lthy
val tyenv_match = Sign.typ_match thy (rty_raw, rty') Vartab.empty
val param_rel_subst = Envir.subst_term (tyenv_match,Vartab.empty) param_rel
val args_subst = map (Envir.subst_term (tyenv_match,Vartab.empty)) args
val lthy = Variable.declare_names fixed_crel lthy
val (instT, lthy) = Variable.importT_inst (param_rel_subst :: args_subst) lthy
val args_fixed = (map (Term_Subst.instantiate (instT, []))) args_subst
val param_rel_fixed = Term_Subst.instantiate (instT, []) param_rel_subst
val rty = (domain_type o fastype_of) param_rel_fixed
val relcomp_op = Const (@{const_name "relcompp"},
(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 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
in
(SOME def_thm, lthy)
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
in
if gen_code andalso is_Const abs then
let
val (fixed_abs, lthy') = yield_singleton(Variable.importT_terms) abs lthy
in
Local_Theory.background_theory(Code.add_datatype [dest_Const fixed_abs]) lthy'
end
else
lthy
end
fun define_abs_type gen_code quot_thm lthy =
if gen_code andalso Lifting_Def.can_generate_code_cert quot_thm then
let
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)
in
lthy
|> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm])
end
else
lthy
fun quot_thm_sanity_check ctxt quot_thm =
let
val ((_, [quot_thm_fixed]), ctxt') = Variable.importT [quot_thm] ctxt
val (rty, qty) = quot_thm_rty_qty quot_thm_fixed
val rty_tfreesT = Term.add_tfree_namesT rty []
val qty_tfreesT = Term.add_tfree_namesT qty []
val extra_rty_tfrees =
case subtract (op =) qty_tfreesT rty_tfreesT of
[] => []
| extras => [Pretty.block ([Pretty.str "Extra variables in the raw type:",
Pretty.brk 1] @
((Pretty.commas o map (Pretty.str o quote)) extras) @
[Pretty.str "."])]
val not_type_constr =
case qty of
Type _ => []
| _ => [Pretty.block [Pretty.str "The quotient type ",
Pretty.quote (Syntax.pretty_typ ctxt' qty),
Pretty.brk 1,
Pretty.str "is not a type constructor."]]
val errs = extra_rty_tfrees @ not_type_constr
in
if null errs then () else error (cat_lines (["Sanity check of the quotient theorem failed:",""]
@ (map Pretty.string_of errs)))
end
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 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 opt_reflp_thm of
SOME reflp_thm => lthy
|> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflexivity_rule_attrib]),
[reflp_thm])
|> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflexivity_rule_attrib]),
[[quot_thm, reflp_thm] MRSL @{thm Quotient_to_left_total}])
|> define_code_constr gen_code quot_thm
| NONE => lthy
|> define_abs_type gen_code quot_thm
in
lthy
|> Local_Theory.declaration {syntax = false, pervasive = true}
(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)
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 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 (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
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
|> setup_lifting_infr gen_code quot_thm opt_reflp_thm
|> setup_transfer_rules
end
(*
Sets up the Lifting package by a typedef theorem.
gen_code - flag if an abstract type given by typedef_thm should be registred
as an abstract type in the code generator
typedef_thm - a typedef theorem (type_definition Rep Abs S)
*)
fun setup_by_typedef_thm gen_code typedef_thm lthy =
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 = 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}
| Const (@{const_name "Collect"}, _) $ Abs (_, _, _) =>
[typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
| _ =>
[typedef_thm, T_def] MRSL @{thm typedef_to_Quotient}
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
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
|> (snd oo Local_Theory.note) ((Binding.prefix_name "Quotient_" qty_name, []),
[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 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
handle TERM _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
fun sanity_check_reflp_thm reflp_thm =
let
val reflp_tm = (HOLogic.dest_Trueprop o prop_of) reflp_thm
handle TERM _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"."
in
case reflp_tm of
Const (@{const_name reflp}, _) $ _ => ()
| _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"."
end
fun setup_quotient () =
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
SOME _ => error "The reflexivity theorem cannot be specified if the type_definition theorem is used."
| NONE => setup_by_typedef_thm gen_code input_thm lthy
in
case input_term of
(Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_quotient ()
| (Const (@{const_name type_definition}, _) $ _ $ _ $ _) => setup_typedef ()
| _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
end
val opt_gen_code =
Scan.optional (@{keyword "("} |-- Parse.!!! ((Parse.reserved "no_code" >> K false) --| @{keyword ")"})) true
val _ =
Outer_Syntax.local_theory @{command_spec "setup_lifting"}
"setup lifting infrastructure"
(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;