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 (* FIXME: purely local typedef causes at the moment |
|
78 problems with type variables |
|
79 |
77 Typedef.add_typedef false NONE (qty_name, vs, mx) |
80 Typedef.add_typedef false NONE (qty_name, vs, mx) |
78 (typedef_term rel rty lthy) NONE typedef_tac lthy |
81 (typedef_term rel rty lthy) NONE typedef_tac lthy |
|
82 *) |
|
83 Local_Theory.theory_result |
|
84 (Typedef.add_typedef_global false NONE |
|
85 (qty_name, vs, mx) |
|
86 (typedef_term rel rty lthy) |
|
87 NONE typedef_tac) lthy |
79 end |
88 end |
80 |
89 |
81 |
90 |
82 (* tactic to prove the quot_type theorem for the new type *) |
91 (* tactic to prove the quot_type theorem for the new type *) |
83 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
92 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |