145 |
145 |
146 ML {* maps_lookup @{theory} "List.list" *} |
146 ML {* maps_lookup @{theory} "List.list" *} |
147 ML {* maps_lookup @{theory} "*" *} |
147 ML {* maps_lookup @{theory} "*" *} |
148 ML {* maps_lookup @{theory} "fun" *} |
148 ML {* maps_lookup @{theory} "fun" *} |
149 |
149 |
150 ML {* |
150 text {* FIXME: auxiliary function *} |
151 fun matches ty1 ty2 = |
|
152 Type.raw_instance (ty1, Logic.varifyT ty2) |
|
153 *} |
|
154 |
|
155 |
|
156 |
|
157 ML {* |
|
158 val quot_def_parser = |
|
159 (OuterParse.$$$ "(" |-- OuterParse.$$$ "with" |-- |
|
160 ((OuterParse.list1 OuterParse.typ) --| OuterParse.$$$ ")")) -- |
|
161 (OuterParse.binding -- |
|
162 Scan.option (OuterParse.$$$ "::" |-- OuterParse.typ) -- |
|
163 OuterParse.mixfix --| OuterParse.where_ -- SpecParse.spec) |
|
164 *} |
|
165 |
|
166 ML {* |
|
167 fun test (qrtys, (((bind, typstr), mx), (attr, prop))) lthy = lthy |
|
168 *} |
|
169 |
|
170 ML {* |
|
171 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants" |
|
172 OuterKeyword.thy_decl (quot_def_parser >> test) |
|
173 *} |
|
174 |
|
175 (* FIXME: auxiliary function *) |
|
176 ML {* |
151 ML {* |
177 val no_vars = Thm.rule_attribute (fn context => fn th => |
152 val no_vars = Thm.rule_attribute (fn context => fn th => |
178 let |
153 let |
179 val ctxt = Variable.set_body false (Context.proof_of context); |
154 val ctxt = Variable.set_body false (Context.proof_of context); |
180 val ((_, [th']), _) = Variable.import true [th] ctxt; |
155 val ((_, [th']), _) = Variable.import true [th] ctxt; |
224 val ftys = map (op -->) tys |
210 val ftys = map (op -->) tys |
225 in |
211 in |
226 (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty)) |
212 (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty)) |
227 end |
213 end |
228 |
214 |
229 val thy = ProofContext.theory_of lthy |
215 fun get_const flag (qty, rty) = |
230 |
216 let |
231 fun get_const absF = (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty)) |
217 val thy = ProofContext.theory_of lthy |
232 | get_const repF = (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty)) |
218 val qty_name = Long_Name.base_name (fst (dest_Type qty)) |
|
219 in |
|
220 case flag of |
|
221 absF => (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty)) |
|
222 | repF => (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty)) |
|
223 end |
233 |
224 |
234 fun mk_identity ty = Abs ("", ty, Bound 0) |
225 fun mk_identity ty = Abs ("", ty, Bound 0) |
235 |
226 |
236 in |
227 in |
237 if ty = qty |
228 if (AList.defined matches qenv ty) |
238 then (get_const flag) |
229 then (get_const flag (the (lookup_qenv qenv ty))) |
239 else (case ty of |
230 else (case ty of |
240 TFree _ => (mk_identity ty, (ty, ty)) |
231 TFree _ => (mk_identity ty, (ty, ty)) |
241 | Type (_, []) => (mk_identity ty, (ty, ty)) |
232 | Type (_, []) => (mk_identity ty, (ty, ty)) |
242 | Type ("fun" , [ty1, ty2]) => |
233 | Type ("fun" , [ty1, ty2]) => |
243 get_fun_fun [get_fun (negF flag) rty qty lthy ty1, get_fun flag rty qty lthy ty2] |
234 get_fun_fun [get_fun (negF flag) qenv lthy ty1, get_fun flag qenv lthy ty2] |
244 | Type (s, tys) => get_fun_aux s (map (get_fun flag rty qty lthy) tys) |
235 | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys) |
245 | _ => raise ERROR ("no type variables") |
236 | _ => raise ERROR ("no type variables") |
246 ) |
237 ) |
247 end |
238 end |
248 *} |
239 *} |
249 |
240 |
250 |
241 |
251 text {* produces the definition for a lifted constant *} |
242 text {* produces the definition for a lifted constant *} |
252 |
243 |
253 ML {* |
244 ML {* |
254 fun get_const_def nconst oconst rty qty lthy = |
245 fun get_const_def nconst otrm qenv lthy = |
255 let |
246 let |
256 val ty = fastype_of nconst |
247 val ty = fastype_of nconst |
257 val (arg_tys, res_ty) = strip_type ty |
248 val (arg_tys, res_ty) = strip_type ty |
258 |
249 |
259 val fresh_args = arg_tys |> map (pair "x") |
250 val rep_fns = map (fst o get_fun repF qenv lthy) arg_tys |
260 |> Variable.variant_frees lthy [nconst, oconst] |
251 val abs_fn = (fst o get_fun absF qenv lthy) res_ty |
261 |> map Free |
|
262 |
|
263 val rep_fns = map (fst o get_fun repF rty qty lthy) arg_tys |
|
264 val abs_fn = (fst o get_fun absF rty qty lthy) res_ty |
|
265 |
252 |
266 fun mk_fun_map (t1,t2) = Const (@{const_name "fun_map"}, dummyT) $ t1 $ t2 |
253 fun mk_fun_map (t1,t2) = Const (@{const_name "fun_map"}, dummyT) $ t1 $ t2 |
267 |
254 |
268 val fns = Library.foldr (mk_fun_map) (rep_fns, abs_fn) |
255 val fns = Library.foldr mk_fun_map (rep_fns, abs_fn) |
269 |> Syntax.check_term lthy |
256 |> Syntax.check_term lthy |
270 in |
257 in |
271 fns $ oconst |
258 fns $ otrm |
272 end |
259 end |
273 *} |
260 *} |
274 |
261 |
275 ML {* |
262 ML {* lookup_snd *} |
276 fun exchange_ty rty qty ty = |
263 |
277 if ty = rty |
264 ML {* |
278 then qty |
265 fun exchange_ty qenv ty = |
279 else |
266 case (lookup_snd matches qenv ty) of |
|
267 SOME qty => qty |
|
268 | NONE => |
280 (case ty of |
269 (case ty of |
281 Type (s, tys) => Type (s, map (exchange_ty rty qty) tys) |
270 Type (s, tys) => Type (s, map (exchange_ty qenv) tys) |
282 | _ => ty |
271 | _ => ty |
283 ) |
272 ) |
284 *} |
273 *} |
285 |
274 |
286 ML {* |
275 ML {* |
287 fun make_const_def nconst_bname oconst mx rty qty lthy = |
276 fun make_const_def nconst_bname otrm mx qenv lthy = |
288 let |
277 let |
289 val oconst_ty = fastype_of oconst |
278 val otrm_ty = fastype_of otrm |
290 val nconst_ty = exchange_ty rty qty oconst_ty |
279 val nconst_ty = exchange_ty qenv otrm_ty |
291 val nconst = Const (Binding.name_of nconst_bname, nconst_ty) |
280 val nconst = Const (Binding.name_of nconst_bname, nconst_ty) |
292 val def_trm = get_const_def nconst oconst rty qty lthy |
281 val def_trm = get_const_def nconst otrm qenv lthy |
293 in |
282 in |
294 define (nconst_bname, mx, def_trm) lthy |
283 define (nconst_bname, mx, def_trm) lthy |
295 end |
284 end |
|
285 *} |
|
286 |
|
287 ML {* |
|
288 fun build_qenv lthy qtys = |
|
289 let |
|
290 val qenv = map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) (quotdata_lookup lthy) |
|
291 |
|
292 fun find_assoc qty = |
|
293 case (AList.lookup matches qenv qty) of |
|
294 SOME rty => (qty, rty) |
|
295 | NONE => error (implode |
|
296 ["Quotient type ", |
|
297 quote (Syntax.string_of_typ lthy qty), |
|
298 " does not exists"]) |
|
299 in |
|
300 map find_assoc qtys |
|
301 end |
|
302 *} |
|
303 |
|
304 ML {* |
|
305 (* taken from isar_syn.ML *) |
|
306 val constdecl = |
|
307 OuterParse.binding -- |
|
308 (OuterParse.where_ >> K (NONE, NoSyn) || |
|
309 OuterParse.$$$ "::" |-- OuterParse.!!! ((OuterParse.typ >> SOME) -- |
|
310 OuterParse.opt_mixfix' --| OuterParse.where_) || |
|
311 Scan.ahead (OuterParse.$$$ "(") |-- |
|
312 OuterParse.!!! (OuterParse.mixfix' --| OuterParse.where_ >> pair NONE)) |
|
313 *} |
|
314 |
|
315 ML {* |
|
316 val qd_parser = |
|
317 (Args.parens (OuterParse.$$$ "for" |-- (Scan.repeat OuterParse.typ))) -- |
|
318 (constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop)) |
|
319 *} |
|
320 |
|
321 ML {* |
|
322 fun pair lthy (ty1, ty2) = |
|
323 "(" ^ (Syntax.string_of_typ lthy ty1) ^ "," ^ (Syntax.string_of_typ lthy ty2) ^ ")" |
|
324 *} |
|
325 |
|
326 ML {* |
|
327 fun parse_qd_spec (qtystrs, ((bind, (typstr__, mx)), (attr__, propstr))) lthy = |
|
328 let |
|
329 val qtys = map (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystrs |
|
330 val qenv = build_qenv lthy qtys |
|
331 val prop = Syntax.parse_prop lthy propstr |> Syntax.check_prop lthy |
|
332 val (lhs, rhs) = Logic.dest_equals prop |
|
333 in |
|
334 make_const_def bind rhs mx qenv lthy |> snd |
|
335 end |
|
336 *} |
|
337 |
|
338 ML {* |
|
339 val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants" |
|
340 OuterKeyword.thy_decl (qd_parser >> parse_qd_spec) |
296 *} |
341 *} |
297 |
342 |
298 section {* ATOMIZE *} |
343 section {* ATOMIZE *} |
299 |
344 |
300 text {* |
345 text {* |
585 (* Needed to have a meta-equality *) |
630 (* Needed to have a meta-equality *) |
586 lemma id_def_sym: "(\<lambda>x. x) \<equiv> id" |
631 lemma id_def_sym: "(\<lambda>x. x) \<equiv> id" |
587 by (simp add: id_def) |
632 by (simp add: id_def) |
588 |
633 |
589 ML {* |
634 ML {* |
|
635 fun old_exchange_ty rty qty ty = |
|
636 if ty = rty |
|
637 then qty |
|
638 else |
|
639 (case ty of |
|
640 Type (s, tys) => Type (s, map (old_exchange_ty rty qty) tys) |
|
641 | _ => ty |
|
642 ) |
|
643 *} |
|
644 |
|
645 ML {* |
|
646 fun old_get_fun flag rty qty lthy ty = |
|
647 get_fun flag [(qty, rty)] lthy ty |
|
648 |
|
649 fun old_make_const_def nconst_bname otrm mx rty qty lthy = |
|
650 make_const_def nconst_bname otrm mx [(qty, rty)] lthy |
|
651 *} |
|
652 |
|
653 ML {* |
590 fun build_repabs_term lthy thm constructors rty qty = |
654 fun build_repabs_term lthy thm constructors rty qty = |
591 let |
655 let |
592 fun mk_rep tm = |
656 fun mk_rep tm = |
593 let |
657 let |
594 val ty = exchange_ty rty qty (fastype_of tm) |
658 val ty = old_exchange_ty rty qty (fastype_of tm) |
595 in fst (get_fun repF rty qty lthy ty) $ tm end |
659 in fst (old_get_fun repF rty qty lthy ty) $ tm end |
596 |
660 |
597 fun mk_abs tm = |
661 fun mk_abs tm = |
598 let |
662 let |
599 val ty = exchange_ty rty qty (fastype_of tm) in |
663 val ty = old_exchange_ty rty qty (fastype_of tm) in |
600 fst (get_fun absF rty qty lthy ty) $ tm end |
664 fst (old_get_fun absF rty qty lthy ty) $ tm end |
601 |
665 |
602 fun is_constructor (Const (x, _)) = member (op =) constructors x |
666 fun is_constructor (Const (x, _)) = member (op =) constructors x |
603 | is_constructor _ = false; |
667 | is_constructor _ = false; |
604 |
668 |
605 fun build_aux lthy tm = |
669 fun build_aux lthy tm = |