92 in |
97 in |
93 (thm', lthy') |
98 (thm', lthy') |
94 end |
99 end |
95 |
100 |
96 (* main function for constructing the quotient type *) |
101 (* main function for constructing the quotient type *) |
97 fun mk_typedef_main (qty_name, mx, rel, rty, equiv_thm) lthy = |
102 fun mk_typedef_main (((qty_name, mx), (rty, rel)), equiv_thm) lthy = |
98 let |
103 let |
99 (* generates typedef *) |
104 (* generates typedef *) |
100 val ((_, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, rty) lthy |
105 val ((_, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, rty) lthy |
101 |
106 |
102 (* abs and rep functions *) |
107 (* abs and rep functions *) |
158 val (global_eqns2, lthy5) = Variable.import_terms true global_eqns lthy4; |
163 val (global_eqns2, lthy5) = Variable.import_terms true global_eqns lthy4; |
159 val global_eqns3 = map (fn t => (bindd, t)) global_eqns2; |
164 val global_eqns3 = map (fn t => (bindd, t)) global_eqns2; |
160 in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end) |
165 in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end) |
161 end |
166 end |
162 |
167 |
163 (* syntax setup *) |
168 (* interface and syntax setup *) |
164 local structure P = OuterParse in |
169 |
165 |
170 (* the ML-interface takes a list of 4-tuples consisting of *) |
166 fun mk_typedef (qty_name, mx, rty, rel_trm) lthy = |
171 (* *) |
167 let |
172 (* - the name of the quotient type *) |
168 val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
173 (* - its mixfix annotation *) |
169 val EQUIV_goal = HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel_trm) |
174 (* - the type to be quotient *) |
170 |
175 (* - the relation according to which the type is quotient *) |
|
176 |
|
177 fun mk_quotient_type quot_list lthy = |
|
178 let |
|
179 fun get_goal (rty, rel) = |
|
180 let |
|
181 val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} |
|
182 in |
|
183 (HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel), []) |
|
184 end |
|
185 |
|
186 val goals = map (get_goal o snd) quot_list |
|
187 |
171 fun after_qed thms lthy = |
188 fun after_qed thms lthy = |
172 let |
189 let |
173 val thm = the_single (flat thms) |
190 val thms' = flat thms |
174 in |
191 in |
175 mk_typedef_main (Binding.name qty_name, mx, rel_trm, rty, thm) lthy |> snd |
192 fold_map mk_typedef_main (quot_list ~~ thms') lthy |> snd |
176 end |
193 end |
177 in |
194 in |
178 Proof.theorem_i NONE after_qed [[(EQUIV_goal, [])]] lthy |
195 Proof.theorem_i NONE after_qed [goals] lthy |
179 end |
196 end |
180 |
197 |
181 (* FIXME: allow more than one type definition *) |
198 val quotspec_parser = |
182 val quottype_parser = |
199 OuterParse.and_list1 |
183 P.short_ident -- P.opt_infix -- |
200 (OuterParse.short_ident -- OuterParse.opt_infix -- |
184 (P.$$$ "=" |-- P.typ) -- |
201 (OuterParse.$$$ "=" |-- OuterParse.typ) -- |
185 (P.$$$ "/" |-- P.term) |
202 (OuterParse.$$$ "/" |-- OuterParse.term)) |
186 |
203 |
187 fun mk_typedef_cmd (((qstr, mx), rstr), rel_str) lthy = |
204 fun mk_quotient_type_cmd spec lthy = |
188 let |
205 let |
189 val rty = Syntax.parse_typ lthy rstr |
206 fun parse_spec (((qty_str, mx), rty_str), rel_str) = |
190 val rel_trm = Syntax.parse_term lthy rel_str |
207 let |
191 |> Syntax.check_term lthy |
208 val qty_name = Binding.name qty_str |
192 in |
209 val rty = Syntax.parse_typ lthy rty_str |
193 mk_typedef (qstr, mx, rty, rel_trm) lthy |
210 val rel = Syntax.parse_term lthy rel_str |
|
211 |> Syntax.check_term lthy |
|
212 in |
|
213 ((qty_name, mx), (rty, rel)) |
|
214 end |
|
215 in |
|
216 mk_quotient_type (map parse_spec spec) lthy |
194 end |
217 end |
195 |
218 |
196 val _ = OuterKeyword.keyword "/" |
219 val _ = OuterKeyword.keyword "/" |
197 |
220 |
198 val _ = |
221 val _ = |
199 OuterSyntax.local_theory_to_proof "quotient" |
222 OuterSyntax.local_theory_to_proof "quotient" |
200 "quotient type definitions (requires equivalence proofs)" |
223 "quotient type definitions (requires equivalence proofs)" |
201 OuterKeyword.thy_goal (quottype_parser >> mk_typedef_cmd) |
224 OuterKeyword.thy_goal (quotspec_parser >> mk_quotient_type_cmd) |
202 |
|
203 end; (* local *) |
|
204 |
225 |
205 end; (* structure *) |
226 end; (* structure *) |
206 |
227 |
207 open Quotient |
228 open Quotient |