161 |
161 |
162 (* name equivalence theorem *) |
162 (* name equivalence theorem *) |
163 val equiv_thm_name = Binding.suffix_name "_equivp" qty_name |
163 val equiv_thm_name = Binding.suffix_name "_equivp" qty_name |
164 |
164 |
165 (* storing the quot-info *) |
165 (* storing the quot-info *) |
166 (* FIXME: VarifyT should not be used - at the moment it allows matching against the types. *) |
|
167 fun qinfo phi = transform_quotdata phi |
166 fun qinfo phi = transform_quotdata phi |
168 {qtyp = Logic.varifyT Abs_ty, rtyp = Logic.varifyT rty, |
167 {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm} |
169 equiv_rel = map_types Logic.varifyT rel, equiv_thm = equiv_thm} |
|
170 val lthy4 = Local_Theory.declaration true |
168 val lthy4 = Local_Theory.declaration true |
171 (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) lthy3 |
169 (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) lthy3 |
172 in |
170 in |
173 lthy4 |
171 lthy4 |
174 |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) |
172 |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) |
271 theorem after_qed goals lthy |
269 theorem after_qed goals lthy |
272 end |
270 end |
273 |
271 |
274 fun quotient_type_cmd specs lthy = |
272 fun quotient_type_cmd specs lthy = |
275 let |
273 let |
276 fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) = |
274 fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) lthy = |
277 let |
275 let |
278 (*val rty = Syntax.read_typ lthy rty_str*) |
276 (* new parsing with proper declaration *) |
279 |
|
280 val rty = Syntax.read_typ lthy rty_str |
277 val rty = Syntax.read_typ lthy rty_str |
281 val rel = Syntax.read_term lthy rel_str |
278 val lthy1 = Variable.declare_typ rty lthy |
|
279 val pre_rel = Syntax.parse_term lthy1 rel_str |
|
280 val pre_rel' = Syntax.type_constraint (rty --> rty --> @{typ bool}) pre_rel |
|
281 val rel = Syntax.check_term lthy1 pre_rel' |
|
282 val lthy2 = Variable.declare_term rel lthy1 |
|
283 |
|
284 (* old parsing *) |
|
285 (* val rty = Syntax.read_typ lthy rty_str |
|
286 val rel = Syntax.read_term lthy rel_str *) |
282 in |
287 in |
283 ((vs, qty_name, mx), (rty, rel)) |
288 (((vs, qty_name, mx), (rty, rel)), lthy2) |
284 end |
289 end |
285 in |
290 |
286 quotient_type (map parse_spec specs) lthy |
291 val (spec', lthy') = fold_map parse_spec specs lthy |
|
292 in |
|
293 quotient_type spec' lthy' |
287 end |
294 end |
288 |
295 |
289 val quotspec_parser = |
296 val quotspec_parser = |
290 OuterParse.and_list1 |
297 OuterParse.and_list1 |
291 ((OuterParse.type_args -- OuterParse.binding) -- |
298 ((OuterParse.type_args -- OuterParse.binding) -- |