371 fun apply_subt f (trm1, trm2) = |
371 fun apply_subt f (trm1, trm2) = |
372 case (trm1, trm2) of |
372 case (trm1, trm2) of |
373 (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t')) |
373 (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t')) |
374 | _ => f (trm1, trm2) |
374 | _ => f (trm1, trm2) |
375 |
375 |
|
376 fun relation_error ctxt r1 r2 = |
|
377 let |
|
378 val r1s = Syntax.string_of_term ctxt r1 |
|
379 val r2s = Syntax.string_of_term ctxt r2 |
|
380 val r1t = Syntax.string_of_typ ctxt (fastype_of r1) |
|
381 val r2t = Syntax.string_of_typ ctxt (fastype_of r2) |
|
382 in |
|
383 raise LIFT_MATCH ("regularise (relation mismatch)\n[" ^ |
|
384 r1s ^ " :: " ^ r1t ^ "]\n[" ^ r2s ^ " :: " ^ r2t ^ "]") |
|
385 end |
|
386 |
376 (* the major type of All and Ex quantifiers *) |
387 (* the major type of All and Ex quantifiers *) |
377 fun qnt_typ ty = domain_type (domain_type ty) |
388 fun qnt_typ ty = domain_type (domain_type ty) |
378 |
389 |
379 (* produces a regularized version of rtrm |
390 (* produces a regularized version of rtrm |
380 |
391 |
414 if ty = ty' then rtrm |
425 if ty = ty' then rtrm |
415 else equiv_relation ctxt (domain_type ty, domain_type ty') |
426 else equiv_relation ctxt (domain_type ty, domain_type ty') |
416 |
427 |
417 | (* in this case we just check whether the given equivalence relation is correct *) |
428 | (* in this case we just check whether the given equivalence relation is correct *) |
418 (rel, Const (@{const_name "op ="}, ty')) => |
429 (rel, Const (@{const_name "op ="}, ty')) => |
419 let |
430 let |
420 (* FIXME: better exception handling *) |
|
421 fun exc rel rel' = LIFT_MATCH ("regularise (relation mismatch)\n[" ^ |
|
422 Syntax.string_of_term ctxt rel ^ " :: " ^ |
|
423 Syntax.string_of_typ ctxt (fastype_of rel) ^ "]\n[" ^ |
|
424 Syntax.string_of_term ctxt rel' ^ " :: " ^ |
|
425 Syntax.string_of_typ ctxt (fastype_of rel') ^ "]") |
|
426 val rel_ty = fastype_of rel |
431 val rel_ty = fastype_of rel |
427 val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') |
432 val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') |
428 in |
433 in |
429 if rel' aconv rel then rtrm else raise (exc rel rel') |
434 if rel' aconv rel then rtrm else relation_error ctxt rel rel' |
430 end |
435 end |
431 |
436 |
432 | (_, Const _) => |
437 | (_, Const _) => |
433 let |
438 let |
434 val thy = ProofContext.theory_of ctxt |
439 val thy = ProofContext.theory_of ctxt |
435 fun matches_typ T T' = |
440 fun matches_typ T T' = |