1 signature QUOTIENT_TYPE = |
1 signature QUOTIENT_TYPE = |
2 sig |
2 sig |
3 exception LIFT_MATCH of string |
3 exception LIFT_MATCH of string |
4 |
4 |
5 val quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state |
5 val quotient_type: ((string list * binding * mixfix) * (typ * term)) list |
6 val quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state |
6 -> Proof.context -> Proof.state |
7 |
7 val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * string) list |
|
8 -> Proof.context -> Proof.state |
8 end; |
9 end; |
9 |
10 |
10 structure Quotient_Type: QUOTIENT_TYPE = |
11 structure Quotient_Type: QUOTIENT_TYPE = |
11 struct |
12 struct |
12 |
13 |
58 (HOLogic.exists_const rty $ |
59 (HOLogic.exists_const rty $ |
59 lambda x (HOLogic.mk_eq (c, (rel $ x)))) |
60 lambda x (HOLogic.mk_eq (c, (rel $ x)))) |
60 end |
61 end |
61 |
62 |
62 (* makes the new type definitions and proves non-emptyness*) |
63 (* makes the new type definitions and proves non-emptyness*) |
63 fun typedef_make (qty_name, mx, rel, rty) lthy = |
64 fun typedef_make (vs, qty_name, mx, rel, rty) lthy = |
64 let |
65 let |
65 val typedef_tac = |
66 val typedef_tac = |
66 EVERY1 [rtac @{thm exI}, |
67 EVERY1 [rtac @{thm exI}, |
67 rtac mem_def2, |
68 rtac mem_def2, |
68 rtac @{thm exI}, |
69 rtac @{thm exI}, |
69 rtac @{thm refl}] |
70 rtac @{thm refl}] |
70 val tfrees = map fst (Term.add_tfreesT rty []) |
|
71 in |
71 in |
72 Local_Theory.theory_result |
72 Local_Theory.theory_result |
73 (Typedef.add_typedef false NONE |
73 (Typedef.add_typedef false NONE |
74 (qty_name, tfrees, mx) |
74 (qty_name, vs, mx) |
75 (typedef_term rel rty lthy) |
75 (typedef_term rel rty lthy) |
76 NONE typedef_tac) lthy |
76 NONE typedef_tac) lthy |
77 end |
77 end |
78 |
78 |
79 (* tactic to prove the Quot_Type theorem for the new type *) |
79 (* tactic to prove the Quot_Type theorem for the new type *) |
118 Goal.prove lthy [] [] goal |
118 Goal.prove lthy [] [] goal |
119 (K typedef_quotient_thm_tac) |
119 (K typedef_quotient_thm_tac) |
120 end |
120 end |
121 |
121 |
122 (* main function for constructing a quotient type *) |
122 (* main function for constructing a quotient type *) |
123 fun mk_typedef_main (((qty_name, mx), (rty, rel)), equiv_thm) lthy = |
123 fun mk_typedef_main (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy = |
124 let |
124 let |
125 (* generates the typedef *) |
125 (* generates the typedef *) |
126 val ((qty_full_name, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, rty) lthy |
126 val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) lthy |
127 |
127 |
128 (* abs and rep functions from the typedef *) |
128 (* abs and rep functions from the typedef *) |
129 val Abs_ty = #abs_type typedef_info |
129 val Abs_ty = #abs_type typedef_info |
130 val Rep_ty = #rep_type typedef_info |
130 val Rep_ty = #rep_type typedef_info |
131 val Abs_name = #Abs_name typedef_info |
131 val Abs_name = #Abs_name typedef_info |
194 theorem after_qed goals lthy |
194 theorem after_qed goals lthy |
195 end |
195 end |
196 |
196 |
197 fun quotient_type_cmd spec lthy = |
197 fun quotient_type_cmd spec lthy = |
198 let |
198 let |
199 fun parse_spec (((qty_str, mx), rty_str), rel_str) = |
199 fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) = |
200 let |
200 let |
201 val qty_name = Binding.name qty_str |
|
202 val rty = Syntax.read_typ lthy rty_str |
201 val rty = Syntax.read_typ lthy rty_str |
203 val rel = Syntax.read_term lthy rel_str |
202 val rel = Syntax.read_term lthy rel_str |
204 in |
203 in |
205 ((qty_name, mx), (rty, rel)) |
204 ((vs, qty_name, mx), (rty, rel)) |
206 end |
205 end |
207 in |
206 in |
208 quotient_type (map parse_spec spec) lthy |
207 quotient_type (map parse_spec spec) lthy |
209 end |
208 end |
210 |
209 |
211 val quotspec_parser = |
210 val quotspec_parser = |
212 OuterParse.and_list1 |
211 OuterParse.and_list1 |
213 (OuterParse.short_ident -- OuterParse.opt_infix -- |
212 ((OuterParse.type_args -- OuterParse.binding) -- |
214 (OuterParse.$$$ "=" |-- OuterParse.typ) -- |
213 OuterParse.opt_infix -- (OuterParse.$$$ "=" |-- OuterParse.typ) -- |
215 (OuterParse.$$$ "/" |-- OuterParse.term)) |
214 (OuterParse.$$$ "/" |-- OuterParse.term)) |
216 |
215 |
217 val _ = OuterKeyword.keyword "/" |
216 val _ = OuterKeyword.keyword "/" |
218 |
217 |
219 val _ = |
218 val _ = |