1 signature QUOTIENT = |
1 signature QUOTIENT = |
2 sig |
2 sig |
3 val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state |
3 val quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state |
4 val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state |
4 val quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state |
5 val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory |
5 val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory |
6 val note: binding * thm -> local_theory -> thm * local_theory |
6 val note: binding * thm -> local_theory -> thm * local_theory |
7 end; |
7 end; |
8 |
8 |
9 structure Quotient: QUOTIENT = |
9 structure Quotient: QUOTIENT = |
188 (* - the name of the quotient type *) |
188 (* - the name of the quotient type *) |
189 (* - its mixfix annotation *) |
189 (* - its mixfix annotation *) |
190 (* - the type to be quotient *) |
190 (* - the type to be quotient *) |
191 (* - the relation according to which the type is quotient *) |
191 (* - the relation according to which the type is quotient *) |
192 |
192 |
193 fun mk_quotient_type quot_list lthy = |
193 fun quotient_type quot_list lthy = |
194 let |
194 let |
195 fun mk_goal (rty, rel) = |
195 fun mk_goal (rty, rel) = |
196 let |
196 let |
197 val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
197 val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
198 in |
198 in |
205 fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd |
205 fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd |
206 in |
206 in |
207 theorem after_qed goals lthy |
207 theorem after_qed goals lthy |
208 end |
208 end |
209 |
209 |
210 fun mk_quotient_type_cmd spec lthy = |
210 fun quotient_type_cmd spec lthy = |
211 let |
211 let |
212 fun parse_spec (((qty_str, mx), rty_str), rel_str) = |
212 fun parse_spec (((qty_str, mx), rty_str), rel_str) = |
213 let |
213 let |
214 val qty_name = Binding.name qty_str |
214 val qty_name = Binding.name qty_str |
215 val rty = Syntax.parse_typ lthy rty_str |> Syntax.check_typ lthy |
215 val rty = Syntax.parse_typ lthy rty_str |> Syntax.check_typ lthy |
216 val rel = Syntax.parse_term lthy rel_str |> Syntax.check_term lthy |
216 val rel = Syntax.parse_term lthy rel_str |> Syntax.check_term lthy |
217 in |
217 in |
218 ((qty_name, mx), (rty, rel)) |
218 ((qty_name, mx), (rty, rel)) |
219 end |
219 end |
220 in |
220 in |
221 mk_quotient_type (map parse_spec spec) lthy |
221 quotient_type (map parse_spec spec) lthy |
222 end |
222 end |
223 |
223 |
224 val quotspec_parser = |
224 val quotspec_parser = |
225 OuterParse.and_list1 |
225 OuterParse.and_list1 |
226 (OuterParse.short_ident -- OuterParse.opt_infix -- |
226 (OuterParse.short_ident -- OuterParse.opt_infix -- |