author | kuncar |
Wed, 04 Apr 2012 17:51:12 +0200 | |
changeset 47361 | 87c0eaf04bad |
parent 47352 | e0bff2ae939f |
child 47379 | 075d22b3a32f |
permissions | -rw-r--r-- |
47308 | 1 |
(* Title: HOL/Tools/Lifting/lifting_setup.ML |
2 |
Author: Ondrej Kuncar |
|
3 |
||
47352 | 4 |
Setting up the lifting infrastructure. |
47308 | 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 |
||
47334 | 16 |
structure Lifting_Setup: LIFTING_SETUP = |
47308 | 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 |
||
47361
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47352
diff
changeset
|
25 |
fun define_cr_rel rep_fun lthy = |
47308 | 26 |
let |
47361
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47352
diff
changeset
|
27 |
val (qty, rty) = (dest_funT o fastype_of) rep_fun |
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47352
diff
changeset
|
28 |
val rep_fun_graph = (HOLogic.eq_const rty) $ Bound 1 $ (rep_fun $ Bound 0) |
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47352
diff
changeset
|
29 |
val def_term = Abs ("x", rty, Abs ("y", qty, rep_fun_graph)); |
47308 | 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' |
|
35 |
in |
|
36 |
(def_thm, lthy'') |
|
37 |
end |
|
38 |
||
39 |
fun define_abs_type quot_thm lthy = |
|
40 |
if Lifting_Def.can_generate_code_cert quot_thm then |
|
41 |
let |
|
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); |
|
46 |
in |
|
47 |
lthy |
|
48 |
|> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm]) |
|
49 |
end |
|
50 |
else |
|
51 |
lthy |
|
52 |
||
53 |
fun setup_lifting_infr quot_thm equiv_thm lthy = |
|
54 |
let |
|
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 |
|
59 |
in |
|
60 |
lthy |
|
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 |
|
64 |
end |
|
65 |
||
66 |
fun setup_by_typedef_thm typedef_thm lthy = |
|
67 |
let |
|
68 |
fun derive_quot_and_equiv_thm to_quot_thm to_equiv_thm typedef_thm lthy = |
|
69 |
let |
|
47361
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47352
diff
changeset
|
70 |
val (_ $ rep_fun $ _ $ _) = (HOLogic.dest_Trueprop o prop_of) typedef_thm |
47308 | 71 |
val equiv_thm = typedef_thm RS to_equiv_thm |
47361
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47352
diff
changeset
|
72 |
val (T_def, lthy') = define_cr_rel rep_fun lthy |
47308 | 73 |
val quot_thm = [typedef_thm, T_def] MRSL to_quot_thm |
74 |
in |
|
75 |
(quot_thm, equiv_thm, lthy') |
|
76 |
end |
|
77 |
||
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", _) => |
|
47361
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47352
diff
changeset
|
81 |
derive_quot_and_equiv_thm @{thm UNIV_typedef_to_Quotient} @{thm UNIV_typedef_to_equivp} |
47308 | 82 |
typedef_thm lthy |
83 |
| Const (@{const_name "Collect"}, _) $ Abs (_, _, _) => |
|
47361
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47352
diff
changeset
|
84 |
derive_quot_and_equiv_thm @{thm open_typedef_to_Quotient} @{thm open_typedef_to_part_equivp} |
47308 | 85 |
typedef_thm lthy |
47361
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47352
diff
changeset
|
86 |
| _ => derive_quot_and_equiv_thm @{thm typedef_to_Quotient} @{thm typedef_to_part_equivp} |
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47352
diff
changeset
|
87 |
typedef_thm lthy) |
47308 | 88 |
in |
89 |
setup_lifting_infr quot_thm equiv_thm lthy' |
|
90 |
end |
|
91 |
||
92 |
fun setup_by_typedef_thm_aux xthm lthy = setup_by_typedef_thm (singleton (Attrib.eval_thms lthy) xthm) lthy |
|
93 |
||
94 |
val _ = |
|
95 |
Outer_Syntax.local_theory @{command_spec "setup_lifting"} |
|
47352 | 96 |
"Setup lifting infrastructure" |
47308 | 97 |
(Parse_Spec.xthm >> (fn xthm => setup_by_typedef_thm_aux xthm)) |
98 |
end; |