support non-open typedefs; define cr_rel in terms of a rep function for typedefs
1 (* Title: HOL/Tools/Lifting/lifting_setup.ML
4 Setting up the lifting infrastructure.
7 signature LIFTING_SETUP =
9 exception SETUP_LIFTING_INFR of string
11 val setup_lifting_infr: thm -> thm -> local_theory -> local_theory
13 val setup_by_typedef_thm: thm -> local_theory -> local_theory
16 structure Lifting_Setup: LIFTING_SETUP =
21 fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
23 exception SETUP_LIFTING_INFR of string
25 fun define_cr_rel rep_fun lthy =
27 val (qty, rty) = (dest_funT o fastype_of) rep_fun
28 val rep_fun_graph = (HOLogic.eq_const rty) $ Bound 1 $ (rep_fun $ Bound 0)
29 val def_term = Abs ("x", rty, Abs ("y", qty, rep_fun_graph));
30 val qty_name = (fst o dest_Type) qty
31 val cr_rel_name = Binding.prefix_name "cr_" (Binding.qualified_name qty_name)
32 val (fixed_def_term, lthy') = yield_singleton (Variable.importT_terms) def_term lthy
33 val ((_, (_ , def_thm)), lthy'') =
34 Local_Theory.define ((cr_rel_name, NoSyn), ((Thm.def_binding cr_rel_name, []), fixed_def_term)) lthy'
39 fun define_abs_type quot_thm lthy =
40 if Lifting_Def.can_generate_code_cert quot_thm then
42 val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
43 val add_abstype_attribute =
44 Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I)
45 val add_abstype_attrib = Attrib.internal (K add_abstype_attribute);
48 |> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm])
53 fun setup_lifting_infr quot_thm equiv_thm lthy =
55 val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm
56 val qty_full_name = (fst o dest_Type) qtyp
57 val quotients = { quot_thm = quot_thm }
58 fun quot_info phi = Lifting_Info.transform_quotients phi quotients
61 |> Local_Theory.declaration {syntax = false, pervasive = true}
62 (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
63 |> define_abs_type quot_thm
66 fun setup_by_typedef_thm typedef_thm lthy =
68 fun derive_quot_and_equiv_thm to_quot_thm to_equiv_thm typedef_thm lthy =
70 val (_ $ rep_fun $ _ $ _) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
71 val equiv_thm = typedef_thm RS to_equiv_thm
72 val (T_def, lthy') = define_cr_rel rep_fun lthy
73 val quot_thm = [typedef_thm, T_def] MRSL to_quot_thm
75 (quot_thm, equiv_thm, lthy')
78 val typedef_set = (snd o dest_comb o HOLogic.dest_Trueprop o prop_of) typedef_thm
79 val (quot_thm, equiv_thm, lthy') = (case typedef_set of
80 Const ("Orderings.top_class.top", _) =>
81 derive_quot_and_equiv_thm @{thm UNIV_typedef_to_Quotient} @{thm UNIV_typedef_to_equivp}
83 | Const (@{const_name "Collect"}, _) $ Abs (_, _, _) =>
84 derive_quot_and_equiv_thm @{thm open_typedef_to_Quotient} @{thm open_typedef_to_part_equivp}
86 | _ => derive_quot_and_equiv_thm @{thm typedef_to_Quotient} @{thm typedef_to_part_equivp}
89 setup_lifting_infr quot_thm equiv_thm lthy'
92 fun setup_by_typedef_thm_aux xthm lthy = setup_by_typedef_thm (singleton (Attrib.eval_thms lthy) xthm) lthy
95 Outer_Syntax.local_theory @{command_spec "setup_lifting"}
96 "Setup lifting infrastructure"
97 (Parse_Spec.xthm >> (fn xthm => setup_by_typedef_thm_aux xthm))