101 OuterSyntax.improper_command "print_quotients" "print out all quotients" |
101 OuterSyntax.improper_command "print_quotients" "print out all quotients" |
102 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotdata o Toplevel.context_of))) |
102 OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotdata o Toplevel.context_of))) |
103 |
103 |
104 |
104 |
105 |
105 |
106 (* wrappers for define, note and theorem_i*) |
106 (* wrappers for define, note and theorem_i *) |
107 fun define (name, mx, rhs) lthy = |
107 fun define (name, mx, rhs) lthy = |
108 let |
108 let |
109 val ((rhs, (_ , thm)), lthy') = |
109 val ((rhs, (_ , thm)), lthy') = |
110 LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, rhs)) lthy |
110 LocalTheory.define Thm.internalK ((name, mx), (Attrib.empty_binding, rhs)) lthy |
111 in |
111 in |
161 end |
161 end |
162 |
162 |
163 (* tactic to prove the QUOT_TYPE theorem for the new type *) |
163 (* tactic to prove the QUOT_TYPE theorem for the new type *) |
164 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
164 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
165 let |
165 let |
166 val unfold_mem = MetaSimplifier.rewrite_rule @{thms mem_def} |
166 val unfold_mem = MetaSimplifier.rewrite_rule [@{thm mem_def}] |
167 val rep_thm = #Rep typedef_info |> unfold_mem |
167 val rep_thm = #Rep typedef_info |> unfold_mem |
168 val rep_inv = #Rep_inverse typedef_info |
168 val rep_inv = #Rep_inverse typedef_info |
169 val abs_inv = #Abs_inverse typedef_info |> unfold_mem |
169 val abs_inv = #Abs_inverse typedef_info |> unfold_mem |
170 val rep_inj = #Rep_inject typedef_info |
170 val rep_inj = #Rep_inject typedef_info |
171 in |
171 in |
298 fun after_qed thms lthy = |
298 fun after_qed thms lthy = |
299 fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd |
299 fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd |
300 in |
300 in |
301 theorem after_qed goals lthy |
301 theorem after_qed goals lthy |
302 end |
302 end |
|
303 |
|
304 fun mk_quotient_type_cmd spec lthy = |
|
305 let |
|
306 fun parse_spec (((qty_str, mx), rty_str), rel_str) = |
|
307 let |
|
308 val qty_name = Binding.name qty_str |
|
309 val rty = Syntax.parse_typ lthy rty_str |> Syntax.check_typ lthy |
|
310 val rel = Syntax.parse_term lthy rel_str |> Syntax.check_term lthy |
|
311 in |
|
312 ((qty_name, mx), (rty, rel)) |
|
313 end |
|
314 in |
|
315 mk_quotient_type (map parse_spec spec) lthy |
|
316 end |
303 |
317 |
304 val quotspec_parser = |
318 val quotspec_parser = |
305 OuterParse.and_list1 |
319 OuterParse.and_list1 |
306 (OuterParse.short_ident -- OuterParse.opt_infix -- |
320 (OuterParse.short_ident -- OuterParse.opt_infix -- |
307 (OuterParse.$$$ "=" |-- OuterParse.typ) -- |
321 (OuterParse.$$$ "=" |-- OuterParse.typ) -- |
308 (OuterParse.$$$ "/" |-- OuterParse.term)) |
322 (OuterParse.$$$ "/" |-- OuterParse.term)) |
309 |
|
310 fun mk_quotient_type_cmd spec lthy = |
|
311 let |
|
312 fun parse_spec (((qty_str, mx), rty_str), rel_str) = |
|
313 let |
|
314 val qty_name = Binding.name qty_str |
|
315 val rty = Syntax.parse_typ lthy rty_str |
|
316 val rel = Syntax.parse_term lthy rel_str |
|
317 |> Syntax.check_term lthy |
|
318 in |
|
319 ((qty_name, mx), (rty, rel)) |
|
320 end |
|
321 in |
|
322 mk_quotient_type (map parse_spec spec) lthy |
|
323 end |
|
324 |
323 |
325 val _ = OuterKeyword.keyword "/" |
324 val _ = OuterKeyword.keyword "/" |
326 |
325 |
327 val _ = |
326 val _ = |
328 OuterSyntax.local_theory_to_proof "quotient" |
327 OuterSyntax.local_theory_to_proof "quotient" |