215 (* - the name of the quotient type *) |
215 (* - the name of the quotient type *) |
216 (* - its free type variables (first argument) *) |
216 (* - its free type variables (first argument) *) |
217 (* - its mixfix annotation *) |
217 (* - its mixfix annotation *) |
218 (* - the type to be quotient *) |
218 (* - the type to be quotient *) |
219 (* - the relation according to which the type is quotient *) |
219 (* - the relation according to which the type is quotient *) |
|
220 (* *) |
|
221 (* opens a proof-state in which one has to show that the *) |
|
222 (* relation is an equivalence relation *) |
220 |
223 |
221 fun quotient_type quot_list lthy = |
224 fun quotient_type quot_list lthy = |
222 let |
225 let |
|
226 (* sanity check *) |
|
227 val _ = map sanity_check quot_list |
|
228 |
223 fun mk_goal (rty, rel) = |
229 fun mk_goal (rty, rel) = |
224 let |
230 let |
225 val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
231 val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
226 in |
232 in |
227 HOLogic.mk_Trueprop (Const (@{const_name equivp}, equivp_ty) $ rel) |
233 HOLogic.mk_Trueprop (Const (@{const_name equivp}, equivp_ty) $ rel) |
229 |
235 |
230 val goals = map (mk_goal o snd) quot_list |
236 val goals = map (mk_goal o snd) quot_list |
231 |
237 |
232 fun after_qed thms lthy = |
238 fun after_qed thms lthy = |
233 fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd |
239 fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd |
234 |
|
235 (* sanity check *) |
|
236 val _ = map sanity_check quot_list |
|
237 in |
240 in |
238 theorem after_qed goals lthy |
241 theorem after_qed goals lthy |
239 end |
242 end |
240 |
243 |
241 fun quotient_type_cmd spec lthy = |
244 fun quotient_type_cmd specs lthy = |
242 let |
245 let |
243 fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) = |
246 fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) = |
244 let |
247 let |
245 val rty = Syntax.read_typ lthy rty_str |
248 val rty = Syntax.read_typ lthy rty_str |
246 val rel = Syntax.read_term lthy rel_str |
249 val rel = Syntax.read_term lthy rel_str |
247 in |
250 in |
248 ((vs, qty_name, mx), (rty, rel)) |
251 ((vs, qty_name, mx), (rty, rel)) |
249 end |
252 end |
250 in |
253 in |
251 quotient_type (map parse_spec spec) lthy |
254 quotient_type (map parse_spec specs) lthy |
252 end |
255 end |
253 |
256 |
254 val quotspec_parser = |
257 val quotspec_parser = |
255 OuterParse.and_list1 |
258 OuterParse.and_list1 |
256 ((OuterParse.type_args -- OuterParse.binding) -- |
259 ((OuterParse.type_args -- OuterParse.binding) -- |