207 |
207 |
208 for more complicated types of A and B |
208 for more complicated types of A and B |
209 *) |
209 *) |
210 |
210 |
211 (* instantiates TVars so that the term is of type ty *) |
211 (* instantiates TVars so that the term is of type ty *) |
212 fun force_typ thy trm ty = |
212 fun force_typ ctxt trm ty = |
213 let |
213 let |
|
214 val thy = ProofContext.theory_of ctxt |
214 val trm_ty = fastype_of trm |
215 val trm_ty = fastype_of trm |
215 val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty |
216 val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty |
216 in |
217 in |
217 map_types (Envir.subst_type ty_inst) trm |
218 map_types (Envir.subst_type ty_inst) trm |
218 end |
219 end |
219 |
220 |
|
221 fun get_relmap ctxt s = |
|
222 let |
|
223 val thy = ProofContext.theory_of ctxt |
|
224 val exc = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")") |
|
225 val relmap = #relmap (maps_lookup thy s) handle NotFound => raise exc |
|
226 in |
|
227 Const (relmap, dummyT) |
|
228 end |
|
229 |
|
230 fun get_equiv_rel ctxt s = |
|
231 let |
|
232 val thy = ProofContext.theory_of ctxt |
|
233 val exc = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")") |
|
234 in |
|
235 #equiv_rel (quotdata_lookup thy s) handle NotFound => raise exc |
|
236 end |
|
237 |
220 (* builds the aggregate equivalence relation *) |
238 (* builds the aggregate equivalence relation *) |
221 (* that will be the argument of Respects *) |
239 (* that will be the argument of Respects *) |
|
240 |
|
241 (* FIXME: check that the types correspond to each other? *) |
222 fun mk_resp_arg ctxt (rty, qty) = |
242 fun mk_resp_arg ctxt (rty, qty) = |
223 let |
|
224 val thy = ProofContext.theory_of ctxt |
|
225 in |
|
226 if rty = qty |
243 if rty = qty |
227 then HOLogic.eq_const rty |
244 then HOLogic.eq_const rty |
228 else |
245 else |
229 case (rty, qty) of |
246 case (rty, qty) of |
230 (Type (s, tys), Type (s', tys')) => |
247 (Type (s, tys), Type (s', tys')) => |
231 if s = s' |
248 if s = s' |
232 then |
249 then |
233 let |
250 let |
234 val exc = LIFT_MATCH ("mk_resp_arg (no relation map function found for type " ^ s ^ ")") |
|
235 val relmap = #relmap (maps_lookup thy s) handle NotFound => raise exc |
|
236 val args = map (mk_resp_arg ctxt) (tys ~~ tys') |
251 val args = map (mk_resp_arg ctxt) (tys ~~ tys') |
237 in |
252 in |
238 list_comb (Const (relmap, dummyT), args) |
253 list_comb (get_relmap ctxt s, args) |
239 end |
254 end |
240 else |
255 else |
241 let |
256 let |
242 val exc = LIFT_MATCH ("mk_resp_arg (no quotient found for type " ^ s ^ ")") |
257 val eqv_rel = get_equiv_rel ctxt s' |
243 val equiv_rel = #equiv_rel (quotdata_lookup thy s') handle NotFound => raise exc |
|
244 (* FIXME: check in this case that the rty and qty *) |
|
245 (* FIXME: correspond to each other *) |
|
246 |
|
247 (* we need to instantiate the TVars in the relation *) |
|
248 val thy = ProofContext.theory_of ctxt |
|
249 val forced_equiv_rel = force_typ thy equiv_rel (rty --> rty --> @{typ bool}) |
|
250 in |
258 in |
251 forced_equiv_rel |
259 force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) |
252 end |
260 end |
253 | _ => HOLogic.eq_const rty |
261 | _ => HOLogic.eq_const rty |
254 (* FIXME: check that the types correspond to each other? *) |
262 |
255 end |
|
256 |
|
257 val mk_babs = Const (@{const_name Babs}, dummyT) |
263 val mk_babs = Const (@{const_name Babs}, dummyT) |
258 val mk_ball = Const (@{const_name Ball}, dummyT) |
264 val mk_ball = Const (@{const_name Ball}, dummyT) |
259 val mk_bex = Const (@{const_name Bex}, dummyT) |
265 val mk_bex = Const (@{const_name Bex}, dummyT) |
260 val mk_resp = Const (@{const_name Respects}, dummyT) |
266 val mk_resp = Const (@{const_name Respects}, dummyT) |
261 |
267 |