213 val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty |
213 val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty |
214 in |
214 in |
215 map_types (Envir.subst_type ty_inst) trm |
215 map_types (Envir.subst_type ty_inst) trm |
216 end |
216 end |
217 |
217 |
218 fun mk_rel_compose (trm1, trm2) = |
218 fun mk_rel_compose (trm1, trm2) = |
219 Const (@{const_name "pred_comp"}, dummyT) $ trm1 $ trm2 |
219 Const (@{const_name "pred_comp"}, dummyT) $ trm1 $ |
|
220 (Const (@{const_name "pred_comp"}, dummyT) $ trm2 $ trm1) |
220 |
221 |
221 fun get_relmap ctxt s = |
222 fun get_relmap ctxt s = |
222 let |
223 let |
223 val thy = ProofContext.theory_of ctxt |
224 val thy = ProofContext.theory_of ctxt |
224 val exc = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")") |
225 val exc = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")") |
286 val rel_map = mk_relmap ctxt vs rty_pat |
287 val rel_map = mk_relmap ctxt vs rty_pat |
287 val result = list_comb (rel_map, args) |
288 val result = list_comb (rel_map, args) |
288 val eqv_rel = get_equiv_rel ctxt s' |
289 val eqv_rel = get_equiv_rel ctxt s' |
289 val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) |
290 val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) |
290 in |
291 in |
291 mk_rel_compose (eqv_rel', result) |
292 mk_rel_compose (result, eqv_rel') |
292 end |
293 end |
293 | _ => HOLogic.eq_const rty |
294 | _ => HOLogic.eq_const rty |
294 |
295 |
295 fun new_equiv_relation_chk ctxt (rty, qty) = |
296 fun new_equiv_relation_chk ctxt (rty, qty) = |
296 new_equiv_relation ctxt (rty, qty) |
297 new_equiv_relation ctxt (rty, qty) |
383 (Abs (x, ty, t), Abs (_, ty', t')) => |
384 (Abs (x, ty, t), Abs (_, ty', t')) => |
384 let |
385 let |
385 val subtrm = Abs(x, ty, regularize_trm ctxt (t, t')) |
386 val subtrm = Abs(x, ty, regularize_trm ctxt (t, t')) |
386 in |
387 in |
387 if ty = ty' then subtrm |
388 if ty = ty' then subtrm |
388 else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm |
389 else mk_babs $ (mk_resp $ new_equiv_relation ctxt (ty, ty')) $ subtrm |
389 end |
390 end |
390 |
391 |
391 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
392 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
392 let |
393 let |
393 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
394 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
394 in |
395 in |
395 if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm |
396 if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm |
396 else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
397 else mk_ball $ (mk_resp $ new_equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
397 end |
398 end |
398 |
399 |
399 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
400 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
400 let |
401 let |
401 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
402 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
402 in |
403 in |
403 if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm |
404 if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm |
404 else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
405 else mk_bex $ (mk_resp $ new_equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
405 end |
406 end |
406 |
407 |
407 | (* equalities need to be replaced by appropriate equivalence relations *) |
408 | (* equalities need to be replaced by appropriate equivalence relations *) |
408 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
409 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
409 if ty = ty' then rtrm |
410 if ty = ty' then rtrm |
410 else equiv_relation ctxt (domain_type ty, domain_type ty') |
411 else new_equiv_relation ctxt (domain_type ty, domain_type ty') |
411 |
412 |
412 | (* in this case we just check whether the given equivalence relation is correct *) |
413 | (* in this case we just check whether the given equivalence relation is correct *) |
413 (rel, Const (@{const_name "op ="}, ty')) => |
414 (rel, Const (@{const_name "op ="}, ty')) => |
414 let |
415 let |
415 val exc = LIFT_MATCH "regularise (relation mismatch)" |
416 val exc = LIFT_MATCH "regularise (relation mismatch)" |
416 val rel_ty = fastype_of rel |
417 val rel_ty = fastype_of rel |
417 val rel' = equiv_relation ctxt (domain_type rel_ty, domain_type ty') |
418 val rel' = new_equiv_relation ctxt (domain_type rel_ty, domain_type ty') |
418 in |
419 in |
419 if rel' aconv rel then rtrm else raise exc |
420 if rel' aconv rel then rtrm else raise exc |
420 end |
421 end |
421 |
422 |
422 | (_, Const _) => |
423 | (_, Const _) => |