6 *) |
6 *) |
7 |
7 |
8 signature QUOTIENT_TYPE = |
8 signature QUOTIENT_TYPE = |
9 sig |
9 sig |
10 val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) * thm |
10 val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) * thm |
11 -> Proof.context -> (thm * thm) * local_theory |
11 -> Proof.context -> Quotient_Info.quotdata_info * local_theory |
12 |
12 |
13 val quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) list |
13 val quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) list |
14 -> Proof.context -> Proof.state |
14 -> Proof.context -> Proof.state |
15 |
15 |
16 val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * (bool * string)) list |
16 val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * (bool * string)) list |
30 in |
30 in |
31 ((rhs, thm), lthy') |
31 ((rhs, thm), lthy') |
32 end |
32 end |
33 |
33 |
34 fun note (name, thm, attrs) lthy = |
34 fun note (name, thm, attrs) lthy = |
35 let |
35 Local_Theory.note ((name, attrs), [thm]) lthy |> snd |
36 val ((_,[thm']), lthy') = Local_Theory.note ((name, attrs), [thm]) lthy |
36 |
37 in |
|
38 (thm', lthy') |
|
39 end |
|
40 |
37 |
41 fun intern_attr at = Attrib.internal (K at) |
38 fun intern_attr at = Attrib.internal (K at) |
42 |
39 |
43 fun theorem after_qed goals ctxt = |
40 fun theorem after_qed goals ctxt = |
44 let |
41 let |
62 [("x", rty), ("c", HOLogic.mk_setT rty)] |
59 [("x", rty), ("c", HOLogic.mk_setT rty)] |
63 |> Variable.variant_frees lthy [rel] |
60 |> Variable.variant_frees lthy [rel] |
64 |> map Free |
61 |> map Free |
65 in |
62 in |
66 lambda c (HOLogic.exists_const rty $ |
63 lambda c (HOLogic.exists_const rty $ |
67 lambda x (HOLogic.mk_conj ((rel $ x $ x), (HOLogic.mk_eq (c, (rel $ x)))))) |
64 lambda x (HOLogic.mk_conj (rel $ x $ x, HOLogic.mk_eq (c, rel $ x)))) |
68 end |
65 end |
69 |
66 |
70 |
67 |
71 (* makes the new type definitions and proves non-emptyness *) |
68 (* makes the new type definitions and proves non-emptyness *) |
72 fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy = |
69 fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy = |
137 |
134 |
138 |
135 |
139 (* main function for constructing a quotient type *) |
136 (* main function for constructing a quotient type *) |
140 fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial)), equiv_thm) lthy = |
137 fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial)), equiv_thm) lthy = |
141 let |
138 let |
142 val part_equiv = if partial then equiv_thm else equiv_thm RS @{thm equivp_implies_part_equivp} |
139 val part_equiv = |
|
140 if partial |
|
141 then equiv_thm |
|
142 else equiv_thm RS @{thm equivp_implies_part_equivp} |
143 |
143 |
144 (* generates the typedef *) |
144 (* generates the typedef *) |
145 val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy |
145 val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy |
146 |
146 |
147 (* abs and rep functions from the typedef *) |
147 (* abs and rep functions from the typedef *) |
171 val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name |
171 val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name |
172 |
172 |
173 (* name equivalence theorem *) |
173 (* name equivalence theorem *) |
174 val equiv_thm_name = Binding.suffix_name "_equivp" qty_name |
174 val equiv_thm_name = Binding.suffix_name "_equivp" qty_name |
175 |
175 |
176 (* storing the quot-info *) |
176 (* storing the quotdata *) |
177 fun qinfo phi = transform_quotdata phi |
177 val quotdata = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm} |
178 {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm} |
178 |
179 val lthy4 = Local_Theory.declaration true |
179 fun qinfo phi = transform_quotdata phi quotdata |
180 (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) lthy3 |
180 |
181 in |
181 val lthy4 = lthy3 |
182 lthy4 |
182 |> Local_Theory.declaration true (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) |
183 |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) |
183 |> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add]) |
184 ||>> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add]) |
184 |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) |
|
185 in |
|
186 (quotdata, lthy4) |
185 end |
187 end |
186 |
188 |
187 |
189 |
188 (* sanity checks for the quotient type specifications *) |
190 (* sanity checks for the quotient type specifications *) |
189 fun sanity_check ((vs, qty_name, _), (rty, rel, _)) = |
191 fun sanity_check ((vs, qty_name, _), (rty, rel, _)) = |
251 |
253 |
252 - the name of the quotient type |
254 - the name of the quotient type |
253 - its free type variables (first argument) |
255 - its free type variables (first argument) |
254 - its mixfix annotation |
256 - its mixfix annotation |
255 - the type to be quotient |
257 - the type to be quotient |
|
258 - the partial flag (a boolean) |
256 - the relation according to which the type is quotient |
259 - the relation according to which the type is quotient |
257 |
260 |
258 it opens a proof-state in which one has to show that the |
261 it opens a proof-state in which one has to show that the |
259 relations are equivalence relations |
262 relations are equivalence relations |
260 *) |
263 *) |
266 val _ = List.app (map_check lthy) quot_list |
269 val _ = List.app (map_check lthy) quot_list |
267 |
270 |
268 fun mk_goal (rty, rel, partial) = |
271 fun mk_goal (rty, rel, partial) = |
269 let |
272 let |
270 val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
273 val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
271 val const = if partial then @{const_name part_equivp} else @{const_name equivp} |
274 val const = |
|
275 if partial then @{const_name part_equivp} else @{const_name equivp} |
272 in |
276 in |
273 HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel) |
277 HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel) |
274 end |
278 end |
275 |
279 |
276 val goals = map (mk_goal o snd) quot_list |
280 val goals = map (mk_goal o snd) quot_list |