6 |
6 |
7 signature LIFTING_SETUP = |
7 signature LIFTING_SETUP = |
8 sig |
8 sig |
9 exception SETUP_LIFTING_INFR of string |
9 exception SETUP_LIFTING_INFR of string |
10 |
10 |
11 val setup_lifting_infr: thm -> local_theory -> local_theory |
11 val setup_lifting_infr: bool -> thm -> local_theory -> local_theory |
12 |
12 |
13 val setup_by_quotient: thm -> thm option -> local_theory -> local_theory |
13 val setup_by_quotient: bool -> thm -> thm option -> local_theory -> local_theory |
14 |
14 |
15 val setup_by_typedef_thm: thm -> local_theory -> local_theory |
15 val setup_by_typedef_thm: bool -> thm -> local_theory -> local_theory |
16 end; |
16 end; |
17 |
17 |
18 structure Lifting_Setup: LIFTING_SETUP = |
18 structure Lifting_Setup: LIFTING_SETUP = |
19 struct |
19 struct |
20 |
20 |
36 Local_Theory.define ((cr_rel_name, NoSyn), ((Thm.def_binding cr_rel_name, []), fixed_def_term)) lthy' |
36 Local_Theory.define ((cr_rel_name, NoSyn), ((Thm.def_binding cr_rel_name, []), fixed_def_term)) lthy' |
37 in |
37 in |
38 (def_thm, lthy'') |
38 (def_thm, lthy'') |
39 end |
39 end |
40 |
40 |
41 fun define_abs_type quot_thm lthy = |
41 fun define_abs_type no_code quot_thm lthy = |
42 if Lifting_Def.can_generate_code_cert quot_thm then |
42 if not no_code andalso Lifting_Def.can_generate_code_cert quot_thm then |
43 let |
43 let |
44 val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep} |
44 val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep} |
45 val add_abstype_attribute = |
45 val add_abstype_attribute = |
46 Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I) |
46 Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I) |
47 val add_abstype_attrib = Attrib.internal (K add_abstype_attribute); |
47 val add_abstype_attrib = Attrib.internal (K add_abstype_attribute); |
76 in |
76 in |
77 if null errs then () else error (cat_lines (["Sanity check of the quotient theorem failed:",""] |
77 if null errs then () else error (cat_lines (["Sanity check of the quotient theorem failed:",""] |
78 @ (map Pretty.string_of errs))) |
78 @ (map Pretty.string_of errs))) |
79 end |
79 end |
80 |
80 |
81 fun setup_lifting_infr quot_thm lthy = |
81 fun setup_lifting_infr no_code quot_thm lthy = |
82 let |
82 let |
83 val _ = quot_thm_sanity_check lthy quot_thm |
83 val _ = quot_thm_sanity_check lthy quot_thm |
84 val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm |
84 val (_, qtyp) = Lifting_Term.quot_thm_rty_qty quot_thm |
85 val qty_full_name = (fst o dest_Type) qtyp |
85 val qty_full_name = (fst o dest_Type) qtyp |
86 val quotients = { quot_thm = quot_thm } |
86 val quotients = { quot_thm = quot_thm } |
87 fun quot_info phi = Lifting_Info.transform_quotients phi quotients |
87 fun quot_info phi = Lifting_Info.transform_quotients phi quotients |
88 in |
88 in |
89 lthy |
89 lthy |
90 |> Local_Theory.declaration {syntax = false, pervasive = true} |
90 |> Local_Theory.declaration {syntax = false, pervasive = true} |
91 (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi)) |
91 (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi)) |
92 |> define_abs_type quot_thm |
92 |> define_abs_type no_code quot_thm |
93 end |
93 end |
94 |
94 |
95 fun setup_by_quotient quot_thm maybe_reflp_thm lthy = |
95 fun setup_by_quotient no_code quot_thm maybe_reflp_thm lthy = |
96 let |
96 let |
97 val transfer_attr = Attrib.internal (K Transfer.transfer_add) |
97 val transfer_attr = Attrib.internal (K Transfer.transfer_add) |
98 val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm |
98 val (_, qty) = Lifting_Term.quot_thm_rty_qty quot_thm |
99 val qty_name = (Binding.name o fst o dest_Type) qty |
99 val qty_name = (Binding.name o fst o dest_Type) qty |
100 fun qualify suffix = Binding.qualified true suffix qty_name |
100 fun qualify suffix = Binding.qualified true suffix qty_name |
117 [quot_thm RS @{thm Quotient_right_unique}]) |
117 [quot_thm RS @{thm Quotient_right_unique}]) |
118 |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]), |
118 |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]), |
119 [quot_thm RS @{thm Quotient_right_total}]) |
119 [quot_thm RS @{thm Quotient_right_total}]) |
120 |> (snd oo Local_Theory.note) ((qualify "rel_eq_transfer", [transfer_attr]), |
120 |> (snd oo Local_Theory.note) ((qualify "rel_eq_transfer", [transfer_attr]), |
121 [quot_thm RS @{thm Quotient_rel_eq_transfer}]) |
121 [quot_thm RS @{thm Quotient_rel_eq_transfer}]) |
122 |> setup_lifting_infr quot_thm |
122 |> setup_lifting_infr no_code quot_thm |
123 end |
123 end |
124 |
124 |
125 fun setup_by_typedef_thm typedef_thm lthy = |
125 fun setup_by_typedef_thm no_code typedef_thm lthy = |
126 let |
126 let |
127 val transfer_attr = Attrib.internal (K Transfer.transfer_add) |
127 val transfer_attr = Attrib.internal (K Transfer.transfer_add) |
128 val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o prop_of) typedef_thm |
128 val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o prop_of) typedef_thm |
129 val (T_def, lthy') = define_cr_rel rep_fun lthy |
129 val (T_def, lthy') = define_cr_rel rep_fun lthy |
130 |
130 |
167 [[typedef_thm, T_def] MRSL @{thm typedef_rep_transfer}]) |
167 [[typedef_thm, T_def] MRSL @{thm typedef_rep_transfer}]) |
168 |> (snd oo Local_Theory.note) ((qualify "right_unique", [transfer_attr]), |
168 |> (snd oo Local_Theory.note) ((qualify "right_unique", [transfer_attr]), |
169 [[quot_thm] MRSL @{thm Quotient_right_unique}]) |
169 [[quot_thm] MRSL @{thm Quotient_right_unique}]) |
170 |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]), |
170 |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]), |
171 [[quot_thm] MRSL @{thm Quotient_right_total}]) |
171 [[quot_thm] MRSL @{thm Quotient_right_total}]) |
172 |> setup_lifting_infr quot_thm |
172 |> setup_lifting_infr no_code quot_thm |
173 end |
173 end |
174 |
174 |
175 fun setup_lifting_cmd xthm lthy = |
175 fun setup_lifting_cmd no_code xthm opt_reflp_xthm lthy = |
176 let |
176 let |
177 val input_thm = singleton (Attrib.eval_thms lthy) xthm |
177 val input_thm = singleton (Attrib.eval_thms lthy) xthm |
178 val input_term = (HOLogic.dest_Trueprop o prop_of) input_thm |
178 val input_term = (HOLogic.dest_Trueprop o prop_of) input_thm |
|
179 handle TERM _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported." |
|
180 |
|
181 fun sanity_check_reflp_thm reflp_thm = |
|
182 let |
|
183 val reflp_tm = (HOLogic.dest_Trueprop o prop_of) reflp_thm |
|
184 handle TERM _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"." |
|
185 in |
|
186 case reflp_tm of |
|
187 Const (@{const_name reflp}, _) $ _ => () |
|
188 | _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"." |
|
189 end |
|
190 |
|
191 fun setup_quotient () = |
|
192 case opt_reflp_xthm of |
|
193 SOME reflp_xthm => |
|
194 let |
|
195 val reflp_thm = singleton (Attrib.eval_thms lthy) reflp_xthm |
|
196 val _ = sanity_check_reflp_thm reflp_thm |
|
197 in |
|
198 setup_by_quotient no_code input_thm (SOME reflp_thm) lthy |
|
199 end |
|
200 | NONE => setup_by_quotient no_code input_thm NONE lthy |
|
201 |
|
202 fun setup_typedef () = |
|
203 case opt_reflp_xthm of |
|
204 SOME _ => error "The reflexivity theorem cannot be specified if the type_definition theorem is used." |
|
205 | NONE => setup_by_typedef_thm no_code input_thm lthy |
179 in |
206 in |
180 case input_term of |
207 case input_term of |
181 (Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_lifting_infr input_thm lthy |
208 (Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_quotient () |
182 | (Const (@{const_name type_definition}, _) $ _ $ _ $ _) => setup_by_typedef_thm input_thm lthy |
209 | (Const (@{const_name type_definition}, _) $ _ $ _ $ _) => setup_typedef () |
183 | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported." |
210 | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported." |
184 end |
211 end |
|
212 |
|
213 val opt_no_code = |
|
214 Scan.optional (@{keyword "("} |-- Parse.!!! ((Parse.reserved "no_code" >> K true) --| @{keyword ")"})) false |
185 |
215 |
186 val _ = |
216 val _ = |
187 Outer_Syntax.local_theory @{command_spec "setup_lifting"} |
217 Outer_Syntax.local_theory @{command_spec "setup_lifting"} |
188 "Setup lifting infrastructure" |
218 "Setup lifting infrastructure" |
189 (Parse_Spec.xthm >> (fn xthm => setup_lifting_cmd xthm)) |
219 (opt_no_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm >> |
|
220 (fn ((no_code, xthm), opt_reflp_xthm) => setup_lifting_cmd no_code xthm opt_reflp_xthm)) |
190 end; |
221 end; |