47308
|
1 |
(* Title: HOL/Tools/Lifting/lifting_setup.ML
|
|
2 |
Author: Ondrej Kuncar
|
|
3 |
|
|
4 |
Setting the lifting infranstructure up.
|
|
5 |
*)
|
|
6 |
|
|
7 |
signature LIFTING_SETUP =
|
|
8 |
sig
|
|
9 |
exception SETUP_LIFTING_INFR of string
|
|
10 |
|
|
11 |
val setup_lifting_infr: thm -> thm -> local_theory -> local_theory
|
|
12 |
|
|
13 |
val setup_by_typedef_thm: thm -> local_theory -> local_theory
|
|
14 |
end;
|
|
15 |
|
|
16 |
structure Lifting_Seup: LIFTING_SETUP =
|
|
17 |
struct
|
|
18 |
|
|
19 |
infix 0 MRSL
|
|
20 |
|
|
21 |
fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
|
|
22 |
|
|
23 |
exception SETUP_LIFTING_INFR of string
|
|
24 |
|
|
25 |
fun define_cr_rel equiv_thm abs_fun lthy =
|
|
26 |
let
|
|
27 |
fun force_type_of_rel rel forced_ty =
|
|
28 |
let
|
|
29 |
val thy = Proof_Context.theory_of lthy
|
|
30 |
val rel_ty = (domain_type o fastype_of) rel
|
|
31 |
val ty_inst = Sign.typ_match thy (rel_ty, forced_ty) Vartab.empty
|
|
32 |
in
|
|
33 |
Envir.subst_term_types ty_inst rel
|
|
34 |
end
|
|
35 |
|
|
36 |
val (rty, qty) = (dest_funT o fastype_of) abs_fun
|
|
37 |
val abs_fun_graph = HOLogic.mk_eq(abs_fun $ Bound 1, Bound 0)
|
|
38 |
val Abs_body = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of
|
|
39 |
Const (@{const_name equivp}, _) $ _ => abs_fun_graph
|
|
40 |
| Const (@{const_name part_equivp}, _) $ rel =>
|
|
41 |
HOLogic.mk_conj (force_type_of_rel rel rty $ Bound 1 $ Bound 1, abs_fun_graph)
|
|
42 |
| _ => raise SETUP_LIFTING_INFR "unsopported equivalence theorem"
|
|
43 |
)
|
|
44 |
val def_term = Abs ("x", rty, Abs ("y", qty, Abs_body));
|
|
45 |
val qty_name = (fst o dest_Type) qty
|
|
46 |
val cr_rel_name = Binding.prefix_name "cr_" (Binding.qualified_name qty_name)
|
|
47 |
val (fixed_def_term, lthy') = yield_singleton (Variable.importT_terms) def_term lthy
|
|
48 |
val ((_, (_ , def_thm)), lthy'') =
|
|
49 |
Local_Theory.define ((cr_rel_name, NoSyn), ((Thm.def_binding cr_rel_name, []), fixed_def_term)) lthy'
|
|
50 |
in
|
|
51 |
(def_thm, lthy'')
|
|
52 |
end
|
|
53 |
|
|
54 |
fun define_abs_type quot_thm lthy =
|
|
55 |
if Lifting_Def.can_generate_code_cert quot_thm then
|
|
56 |
let
|
|
57 |
val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
|
|
58 |
val add_abstype_attribute =
|
|
59 |
Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I)
|
|
60 |
val add_abstype_attrib = Attrib.internal (K add_abstype_attribute);
|
|
61 |
in
|
|
62 |
lthy
|
|
63 |
|> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm])
|
|
64 |
end
|
|
65 |
else
|
|
66 |
lthy
|
|
67 |
|
|
68 |
fun setup_lifting_infr quot_thm equiv_thm lthy =
|
|
69 |
let
|
|
70 |
val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm
|
|
71 |
val qty_full_name = (fst o dest_Type) qtyp
|
|
72 |
val quotients = { quot_thm = quot_thm }
|
|
73 |
fun quot_info phi = Lifting_Info.transform_quotients phi quotients
|
|
74 |
in
|
|
75 |
lthy
|
|
76 |
|> Local_Theory.declaration {syntax = false, pervasive = true}
|
|
77 |
(fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
|
|
78 |
|> define_abs_type quot_thm
|
|
79 |
end
|
|
80 |
|
|
81 |
fun setup_by_typedef_thm typedef_thm lthy =
|
|
82 |
let
|
|
83 |
fun derive_quot_and_equiv_thm to_quot_thm to_equiv_thm typedef_thm lthy =
|
|
84 |
let
|
|
85 |
val (_ $ _ $ abs_fun $ _) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
|
|
86 |
val equiv_thm = typedef_thm RS to_equiv_thm
|
|
87 |
val (T_def, lthy') = define_cr_rel equiv_thm abs_fun lthy
|
|
88 |
val quot_thm = [typedef_thm, T_def] MRSL to_quot_thm
|
|
89 |
in
|
|
90 |
(quot_thm, equiv_thm, lthy')
|
|
91 |
end
|
|
92 |
|
|
93 |
val typedef_set = (snd o dest_comb o HOLogic.dest_Trueprop o prop_of) typedef_thm
|
|
94 |
val (quot_thm, equiv_thm, lthy') = (case typedef_set of
|
|
95 |
Const ("Orderings.top_class.top", _) =>
|
|
96 |
derive_quot_and_equiv_thm @{thm copy_type_to_Quotient} @{thm copy_type_to_equivp}
|
|
97 |
typedef_thm lthy
|
|
98 |
| Const (@{const_name "Collect"}, _) $ Abs (_, _, _) =>
|
|
99 |
derive_quot_and_equiv_thm @{thm invariant_type_to_Quotient} @{thm invariant_type_to_part_equivp}
|
|
100 |
typedef_thm lthy
|
|
101 |
| _ => raise SETUP_LIFTING_INFR "unsupported typedef theorem")
|
|
102 |
in
|
|
103 |
setup_lifting_infr quot_thm equiv_thm lthy'
|
|
104 |
end
|
|
105 |
|
|
106 |
fun setup_by_typedef_thm_aux xthm lthy = setup_by_typedef_thm (singleton (Attrib.eval_thms lthy) xthm) lthy
|
|
107 |
|
|
108 |
val _ =
|
|
109 |
Outer_Syntax.local_theory @{command_spec "setup_lifting"}
|
|
110 |
"Setup lifting infrastracture"
|
|
111 |
(Parse_Spec.xthm >> (fn xthm => setup_by_typedef_thm_aux xthm))
|
|
112 |
|
|
113 |
end;
|