kuncar@48153
|
1 |
(* Title: HOL/Tools/Lifting/lifting_setup.ML
|
kuncar@48153
|
2 |
Author: Ondrej Kuncar
|
kuncar@48153
|
3 |
|
huffman@48210
|
4 |
Setting up the lifting infrastructure.
|
kuncar@48153
|
5 |
*)
|
kuncar@48153
|
6 |
|
kuncar@48153
|
7 |
signature LIFTING_SETUP =
|
kuncar@48153
|
8 |
sig
|
kuncar@48153
|
9 |
exception SETUP_LIFTING_INFR of string
|
kuncar@48153
|
10 |
|
kuncar@48392
|
11 |
val setup_lifting_infr: thm -> local_theory -> local_theory
|
kuncar@48392
|
12 |
|
kuncar@48392
|
13 |
val setup_by_quotient: thm -> thm option -> local_theory -> local_theory
|
kuncar@48153
|
14 |
|
kuncar@48153
|
15 |
val setup_by_typedef_thm: thm -> local_theory -> local_theory
|
kuncar@48153
|
16 |
end;
|
kuncar@48153
|
17 |
|
huffman@48205
|
18 |
structure Lifting_Setup: LIFTING_SETUP =
|
kuncar@48153
|
19 |
struct
|
kuncar@48153
|
20 |
|
kuncar@48153
|
21 |
infix 0 MRSL
|
kuncar@48153
|
22 |
|
kuncar@48153
|
23 |
fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
|
kuncar@48153
|
24 |
|
kuncar@48153
|
25 |
exception SETUP_LIFTING_INFR of string
|
kuncar@48153
|
26 |
|
kuncar@48219
|
27 |
fun define_cr_rel rep_fun lthy =
|
kuncar@48153
|
28 |
let
|
kuncar@48219
|
29 |
val (qty, rty) = (dest_funT o fastype_of) rep_fun
|
kuncar@48219
|
30 |
val rep_fun_graph = (HOLogic.eq_const rty) $ Bound 1 $ (rep_fun $ Bound 0)
|
kuncar@48219
|
31 |
val def_term = Abs ("x", rty, Abs ("y", qty, rep_fun_graph));
|
kuncar@48153
|
32 |
val qty_name = (fst o dest_Type) qty
|
kuncar@48153
|
33 |
val cr_rel_name = Binding.prefix_name "cr_" (Binding.qualified_name qty_name)
|
kuncar@48153
|
34 |
val (fixed_def_term, lthy') = yield_singleton (Variable.importT_terms) def_term lthy
|
kuncar@48153
|
35 |
val ((_, (_ , def_thm)), lthy'') =
|
kuncar@48153
|
36 |
Local_Theory.define ((cr_rel_name, NoSyn), ((Thm.def_binding cr_rel_name, []), fixed_def_term)) lthy'
|
kuncar@48153
|
37 |
in
|
kuncar@48153
|
38 |
(def_thm, lthy'')
|
kuncar@48153
|
39 |
end
|
kuncar@48153
|
40 |
|
kuncar@48153
|
41 |
fun define_abs_type quot_thm lthy =
|
kuncar@48153
|
42 |
if Lifting_Def.can_generate_code_cert quot_thm then
|
kuncar@48153
|
43 |
let
|
kuncar@48153
|
44 |
val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
|
kuncar@48153
|
45 |
val add_abstype_attribute =
|
kuncar@48153
|
46 |
Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I)
|
kuncar@48153
|
47 |
val add_abstype_attrib = Attrib.internal (K add_abstype_attribute);
|
kuncar@48153
|
48 |
in
|
kuncar@48153
|
49 |
lthy
|
kuncar@48153
|
50 |
|> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm])
|
kuncar@48153
|
51 |
end
|
kuncar@48153
|
52 |
else
|
kuncar@48153
|
53 |
lthy
|
kuncar@48153
|
54 |
|
kuncar@48237
|
55 |
fun quot_thm_sanity_check ctxt quot_thm =
|
kuncar@48237
|
56 |
let
|
kuncar@48237
|
57 |
val ((_, [quot_thm_fixed]), ctxt') = Variable.importT [quot_thm] ctxt
|
kuncar@48237
|
58 |
val (rty, qty) = Lifting_Term.quot_thm_rty_qty quot_thm_fixed
|
kuncar@48237
|
59 |
val rty_tfreesT = Term.add_tfree_namesT rty []
|
kuncar@48237
|
60 |
val qty_tfreesT = Term.add_tfree_namesT qty []
|
kuncar@48237
|
61 |
val extra_rty_tfrees =
|
kuncar@48237
|
62 |
(case subtract (op =) qty_tfreesT rty_tfreesT of
|
kuncar@48237
|
63 |
[] => []
|
kuncar@48237
|
64 |
| extras => [Pretty.block ([Pretty.str "Extra variables in the raw type:",
|
kuncar@48237
|
65 |
Pretty.brk 1] @
|
kuncar@48237
|
66 |
((Pretty.commas o map (Pretty.str o quote)) extras) @
|
kuncar@48237
|
67 |
[Pretty.str "."])])
|
kuncar@48237
|
68 |
val not_type_constr =
|
kuncar@48237
|
69 |
(case qty of
|
kuncar@48237
|
70 |
Type _ => []
|
kuncar@48237
|
71 |
| _ => [Pretty.block [Pretty.str "The quotient type ",
|
kuncar@48237
|
72 |
Pretty.quote (Syntax.pretty_typ ctxt' qty),
|
kuncar@48237
|
73 |
Pretty.brk 1,
|
kuncar@48237
|
74 |
Pretty.str "is not a type constructor."]])
|
kuncar@48237
|
75 |
val errs = extra_rty_tfrees @ not_type_constr
|
kuncar@48237
|
76 |
in
|
kuncar@48237
|
77 |
if null errs then () else error (cat_lines (["Sanity check of the quotient theorem failed:",""]
|
kuncar@48237
|
78 |
@ (map Pretty.string_of errs)))
|
kuncar@48237
|
79 |
end
|
kuncar@48237
|
80 |
|
kuncar@48392
|
81 |
fun setup_lifting_infr quot_thm lthy =
|
kuncar@48153
|
82 |
let
|
kuncar@48237
|
83 |
val _ = quot_thm_sanity_check lthy quot_thm
|
kuncar@48153
|
84 |
val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm
|
kuncar@48153
|
85 |
val qty_full_name = (fst o dest_Type) qtyp
|
kuncar@48153
|
86 |
val quotients = { quot_thm = quot_thm }
|
kuncar@48153
|
87 |
fun quot_info phi = Lifting_Info.transform_quotients phi quotients
|
kuncar@48153
|
88 |
in
|
kuncar@48153
|
89 |
lthy
|
kuncar@48153
|
90 |
|> Local_Theory.declaration {syntax = false, pervasive = true}
|
kuncar@48153
|
91 |
(fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
|
kuncar@48153
|
92 |
|> define_abs_type quot_thm
|
kuncar@48153
|
93 |
end
|
kuncar@48153
|
94 |
|
kuncar@48392
|
95 |
fun setup_by_quotient quot_thm maybe_reflp_thm lthy =
|
kuncar@48392
|
96 |
let
|
kuncar@48392
|
97 |
val transfer_attr = Attrib.internal (K Transfer.transfer_add)
|
kuncar@48392
|
98 |
val lthy' = case maybe_reflp_thm of
|
kuncar@48392
|
99 |
SOME reflp_thm => lthy
|
kuncar@48392
|
100 |
|> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
|
kuncar@48392
|
101 |
[[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}])
|
kuncar@48392
|
102 |
|> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
|
kuncar@48392
|
103 |
[[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
|
kuncar@48392
|
104 |
| NONE => lthy
|
kuncar@48392
|
105 |
in
|
kuncar@48392
|
106 |
lthy'
|
kuncar@48392
|
107 |
|> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
|
kuncar@48392
|
108 |
[quot_thm RS @{thm Quotient_right_unique}])
|
kuncar@48392
|
109 |
|> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
|
kuncar@48392
|
110 |
[quot_thm RS @{thm Quotient_right_total}])
|
kuncar@48392
|
111 |
|> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
|
kuncar@48392
|
112 |
[quot_thm RS @{thm Quotient_rel_eq_transfer}])
|
kuncar@48392
|
113 |
|> setup_lifting_infr quot_thm
|
kuncar@48392
|
114 |
end
|
kuncar@48392
|
115 |
|
kuncar@48153
|
116 |
fun setup_by_typedef_thm typedef_thm lthy =
|
kuncar@48153
|
117 |
let
|
kuncar@48392
|
118 |
val transfer_attr = Attrib.internal (K Transfer.transfer_add)
|
kuncar@48392
|
119 |
val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o prop_of) typedef_thm
|
kuncar@48392
|
120 |
val (T_def, lthy') = define_cr_rel rep_fun lthy
|
kuncar@48392
|
121 |
|
kuncar@48392
|
122 |
val quot_thm = (case typedef_set of
|
kuncar@48392
|
123 |
Const ("Orderings.top_class.top", _) =>
|
kuncar@48392
|
124 |
[typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient}
|
kuncar@48392
|
125 |
| Const (@{const_name "Collect"}, _) $ Abs (_, _, _) =>
|
kuncar@48392
|
126 |
[typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
|
kuncar@48392
|
127 |
| _ =>
|
kuncar@48392
|
128 |
[typedef_thm, T_def] MRSL @{thm typedef_to_Quotient})
|
kuncar@48153
|
129 |
|
kuncar@48392
|
130 |
val lthy'' = (case typedef_set of
|
kuncar@48392
|
131 |
Const ("Orderings.top_class.top", _) => (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
|
kuncar@48392
|
132 |
[[typedef_thm,T_def] MRSL @{thm copy_type_bi_total}]) lthy'
|
kuncar@48392
|
133 |
| _ => lthy')
|
kuncar@48153
|
134 |
in
|
kuncar@48392
|
135 |
lthy''
|
kuncar@48392
|
136 |
|> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
|
kuncar@48392
|
137 |
[[typedef_thm, T_def] MRSL @{thm typedef_bi_unique}])
|
kuncar@48392
|
138 |
|> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
|
huffman@48405
|
139 |
[[typedef_thm, T_def] MRSL @{thm typedef_right_total}])
|
kuncar@48392
|
140 |
|> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
|
huffman@48406
|
141 |
[[typedef_thm, T_def] MRSL @{thm typedef_rep_transfer}])
|
huffman@48406
|
142 |
|> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
|
kuncar@48392
|
143 |
[[typedef_thm, T_def] MRSL @{thm typedef_transfer_All}])
|
kuncar@48392
|
144 |
|> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
|
kuncar@48392
|
145 |
[[typedef_thm, T_def] MRSL @{thm typedef_transfer_Ex}])
|
kuncar@48392
|
146 |
|> (snd oo Local_Theory.note) ((Binding.empty, [transfer_attr]),
|
kuncar@48392
|
147 |
[[typedef_thm, T_def] MRSL @{thm typedef_transfer_bforall}])
|
kuncar@48392
|
148 |
|> setup_lifting_infr quot_thm
|
kuncar@48153
|
149 |
end
|
kuncar@48153
|
150 |
|
kuncar@48392
|
151 |
fun setup_lifting_cmd xthm lthy =
|
kuncar@48392
|
152 |
let
|
kuncar@48392
|
153 |
val input_thm = singleton (Attrib.eval_thms lthy) xthm
|
kuncar@48392
|
154 |
val input_term = (HOLogic.dest_Trueprop o prop_of) input_thm
|
kuncar@48392
|
155 |
in
|
kuncar@48392
|
156 |
case input_term of
|
kuncar@48392
|
157 |
(Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_lifting_infr input_thm lthy
|
kuncar@48392
|
158 |
| (Const (@{const_name type_definition}, _) $ _ $ _ $ _) => setup_by_typedef_thm input_thm lthy
|
kuncar@48392
|
159 |
| _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
|
kuncar@48392
|
160 |
end
|
kuncar@48153
|
161 |
|
kuncar@48153
|
162 |
val _ =
|
kuncar@48153
|
163 |
Outer_Syntax.local_theory @{command_spec "setup_lifting"}
|
huffman@48210
|
164 |
"Setup lifting infrastructure"
|
kuncar@48392
|
165 |
(Parse_Spec.xthm >> (fn xthm => setup_lifting_cmd xthm))
|
kuncar@48153
|
166 |
end;
|