5 |
5 |
6 *) |
6 *) |
7 |
7 |
8 signature QUOTIENT_TYPE = |
8 signature QUOTIENT_TYPE = |
9 sig |
9 sig |
|
10 val add_quotient_type: ((string list * binding * mixfix) * (typ * term)) * thm |
|
11 -> Proof.context -> (thm * thm) * local_theory |
|
12 |
10 val quotient_type: ((string list * binding * mixfix) * (typ * term)) list |
13 val quotient_type: ((string list * binding * mixfix) * (typ * term)) list |
11 -> Proof.context -> Proof.state |
14 -> Proof.context -> Proof.state |
12 |
15 |
13 val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * string) list |
16 val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * string) list |
14 -> Proof.context -> Proof.state |
17 -> Proof.context -> Proof.state |
67 |
70 |
68 (* makes the new type definitions and proves non-emptyness *) |
71 (* makes the new type definitions and proves non-emptyness *) |
69 fun typedef_make (vs, qty_name, mx, rel, rty) lthy = |
72 fun typedef_make (vs, qty_name, mx, rel, rty) lthy = |
70 let |
73 let |
71 val typedef_tac = |
74 val typedef_tac = |
72 EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}]) |
75 EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}]) |
73 in |
76 in |
74 Typedef.add_typedef false NONE |
77 Local_Theory.theory_result |
75 (qty_name, vs, mx) |
78 (Typedef.add_typedef_global false NONE |
76 (typedef_term rel rty lthy) |
79 (qty_name, vs, mx) |
77 NONE typedef_tac lthy |
80 (typedef_term rel rty lthy) |
|
81 NONE typedef_tac) lthy |
78 end |
82 end |
79 |
83 |
80 |
84 |
81 (* tactic to prove the quot_type theorem for the new type *) |
85 (* tactic to prove the quot_type theorem for the new type *) |
82 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
86 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
125 (K typedef_quotient_thm_tac) |
129 (K typedef_quotient_thm_tac) |
126 end |
130 end |
127 |
131 |
128 |
132 |
129 (* main function for constructing a quotient type *) |
133 (* main function for constructing a quotient type *) |
130 fun mk_quotient_type (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy = |
134 fun add_quotient_type (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy = |
131 let |
135 let |
132 (* generates the typedef *) |
136 (* generates the typedef *) |
133 val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) lthy |
137 val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) lthy |
134 |
138 |
135 (* abs and rep functions from the typedef *) |
139 (* abs and rep functions from the typedef *) |
261 end |
265 end |
262 |
266 |
263 val goals = map (mk_goal o snd) quot_list |
267 val goals = map (mk_goal o snd) quot_list |
264 |
268 |
265 fun after_qed thms lthy = |
269 fun after_qed thms lthy = |
266 fold_map mk_quotient_type (quot_list ~~ thms) lthy |> snd |
270 fold_map add_quotient_type (quot_list ~~ thms) lthy |> snd |
267 in |
271 in |
268 theorem after_qed goals lthy |
272 theorem after_qed goals lthy |
269 end |
273 end |
270 |
274 |
271 fun quotient_type_cmd specs lthy = |
275 fun quotient_type_cmd specs lthy = |
272 let |
276 let |
273 fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) lthy = |
277 fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) lthy = |
274 let |
278 let |
275 (* new parsing with proper declaration *) |
|
276 val rty = Syntax.read_typ lthy rty_str |
279 val rty = Syntax.read_typ lthy rty_str |
277 val lthy1 = Variable.declare_typ rty lthy |
280 val lthy1 = Variable.declare_typ rty lthy |
278 val rel = |
281 val rel = |
279 Syntax.parse_term lthy1 rel_str |
282 Syntax.parse_term lthy1 rel_str |
280 |> Syntax.type_constraint (rty --> rty --> @{typ bool}) |
283 |> Syntax.type_constraint (rty --> rty --> @{typ bool}) |
281 |> Syntax.check_term lthy1 |
284 |> Syntax.check_term lthy1 |
282 val lthy2 = Variable.declare_term rel lthy1 |
285 val lthy2 = Variable.declare_term rel lthy1 |
283 in |
286 in |
284 (((vs, qty_name, mx), (rty, rel)), lthy2) |
287 (((vs, qty_name, mx), (rty, rel)), lthy2) |
285 end |
288 end |
286 |
289 |
287 val (spec', lthy') = fold_map parse_spec specs lthy |
290 val (spec', lthy') = fold_map parse_spec specs lthy |
288 in |
291 in |
289 quotient_type spec' lthy' |
292 quotient_type spec' lthy' |
290 end |
293 end |
291 |
294 |
292 local |
|
293 structure P = OuterParse; |
|
294 in |
|
295 |
|
296 val quotspec_parser = |
295 val quotspec_parser = |
297 P.and_list1 ((P.type_args -- P.binding) -- P.opt_infix -- |
296 OuterParse.and_list1 |
298 (P.$$$ "=" |-- P.typ) -- (P.$$$ "/" |-- P.term)) |
297 ((OuterParse.type_args -- OuterParse.binding) -- |
299 end |
298 OuterParse.opt_mixfix -- (OuterParse.$$$ "=" |-- OuterParse.typ) -- |
|
299 (OuterParse.$$$ "/" |-- OuterParse.term)) |
300 |
300 |
301 val _ = OuterKeyword.keyword "/" |
301 val _ = OuterKeyword.keyword "/" |
302 |
302 |
303 val _ = |
303 val _ = |
304 OuterSyntax.local_theory_to_proof "quotient_type" |
304 OuterSyntax.local_theory_to_proof "quotient_type" |
305 "quotient type definitions (require equivalence proofs)" |
305 "quotient type definitions (require equivalence proofs)" |
306 OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd) |
306 OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd) |
307 |
307 |
308 end; (* structure *) |
308 end; (* structure *) |