equal
deleted
inserted
replaced
1 (* Title: quotient_typ.thy |
1 (* Title: HOL/Tools/Quotient/quotient_typ.thy |
2 Author: Cezary Kaliszyk and Christian Urban |
2 Author: Cezary Kaliszyk and Christian Urban |
3 |
3 |
4 Definition of a quotient type. |
4 Definition of a quotient type. |
5 |
5 |
6 *) |
6 *) |
7 |
7 |
8 signature QUOTIENT_TYPE = |
8 signature QUOTIENT_TYPE = |
9 sig |
9 sig |
72 fun typedef_make (vs, qty_name, mx, rel, rty) lthy = |
72 fun typedef_make (vs, qty_name, mx, rel, rty) lthy = |
73 let |
73 let |
74 val typedef_tac = |
74 val typedef_tac = |
75 EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}]) |
75 EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}]) |
76 in |
76 in |
77 Local_Theory.theory_result |
77 Typedef.add_typedef false NONE (qty_name, vs, mx) |
78 (Typedef.add_typedef_global false NONE |
78 (typedef_term rel rty lthy) NONE typedef_tac lthy |
79 (qty_name, vs, mx) |
|
80 (typedef_term rel rty lthy) |
|
81 NONE typedef_tac) lthy |
|
82 end |
79 end |
83 |
80 |
84 |
81 |
85 (* tactic to prove the quot_type theorem for the new type *) |
82 (* tactic to prove the quot_type theorem for the new type *) |
86 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
83 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
280 val lthy1 = Variable.declare_typ rty lthy |
277 val lthy1 = Variable.declare_typ rty lthy |
281 val rel = |
278 val rel = |
282 Syntax.parse_term lthy1 rel_str |
279 Syntax.parse_term lthy1 rel_str |
283 |> Syntax.type_constraint (rty --> rty --> @{typ bool}) |
280 |> Syntax.type_constraint (rty --> rty --> @{typ bool}) |
284 |> Syntax.check_term lthy1 |
281 |> Syntax.check_term lthy1 |
285 val lthy2 = Variable.declare_term rel lthy1 |
282 val (newT, lthy2) = lthy1 |
|
283 |> Typedecl.typedecl_wrt [rel] (qty_name, vs, mx) |
|
284 ||> Variable.declare_term rel |
|
285 |
|
286 (*val Type (full_qty_name, type_args) = newT |
|
287 val vs' = map Term.dest_TFree type_args*) |
286 in |
288 in |
287 (((vs, qty_name, mx), (rty, rel)), lthy2) |
289 (((vs, qty_name, mx), (rty, rel)), lthy2) |
288 end |
290 end |
289 |
291 |
290 val (spec', lthy') = fold_map parse_spec specs lthy |
292 val (spec', lthy') = fold_map parse_spec specs lthy |