376 fun apply_subt f (trm1, trm2) = |
376 fun apply_subt f (trm1, trm2) = |
377 case (trm1, trm2) of |
377 case (trm1, trm2) of |
378 (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t')) |
378 (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t')) |
379 | _ => f (trm1, trm2) |
379 | _ => f (trm1, trm2) |
380 |
380 |
381 fun relation_error ctxt r1 r2 = |
381 fun term_mismatch str ctxt t1 t2 = |
382 let |
382 let |
383 val r1_str = Syntax.string_of_term ctxt r1 |
383 val t1_str = Syntax.string_of_term ctxt t1 |
384 val r2_str = Syntax.string_of_term ctxt r2 |
384 val t2_str = Syntax.string_of_term ctxt t2 |
385 val r1_ty_str = Syntax.string_of_typ ctxt (fastype_of r1) |
385 val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1) |
386 val r2_ty_str = Syntax.string_of_typ ctxt (fastype_of r2) |
386 val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2) |
387 in |
387 in |
388 raise LIFT_MATCH |
388 raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str]) |
389 (cat_lines ["regularise (relation mismatch)", r1_str ^ "::" ^ r1_ty_str, r2_str ^ "::" ^ r2_ty_str]) |
|
390 end |
389 end |
391 |
390 |
392 (* the major type of All and Ex quantifiers *) |
391 (* the major type of All and Ex quantifiers *) |
393 fun qnt_typ ty = domain_type (domain_type ty) |
392 fun qnt_typ ty = domain_type (domain_type ty) |
394 |
393 |
431 in |
430 in |
432 if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm |
431 if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm |
433 else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
432 else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
434 end |
433 end |
435 |
434 |
|
435 | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "All"}, ty') $ t') => |
|
436 let |
|
437 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
438 in |
|
439 if resrel <> Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) |
|
440 then term_mismatch "regularize(ball)" ctxt rtrm qtrm |
|
441 else mk_ball $ (mk_resp $ resrel) $ subtrm |
|
442 end |
|
443 |
436 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
444 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
437 let |
445 let |
438 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
446 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
439 in |
447 in |
440 if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm |
448 if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm |
441 else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
449 else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
|
450 end |
|
451 |
|
452 | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
|
453 let |
|
454 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
455 in |
|
456 if resrel <> Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) |
|
457 then term_mismatch "regularize(bex)" ctxt rtrm qtrm |
|
458 else mk_bex $ (mk_resp $ resrel) $ subtrm |
442 end |
459 end |
443 |
460 |
444 | (* equalities need to be replaced by appropriate equivalence relations *) |
461 | (* equalities need to be replaced by appropriate equivalence relations *) |
445 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
462 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
446 if ty = ty' then rtrm |
463 if ty = ty' then rtrm |
450 (rel, Const (@{const_name "op ="}, ty')) => |
467 (rel, Const (@{const_name "op ="}, ty')) => |
451 let |
468 let |
452 val rel_ty = fastype_of rel |
469 val rel_ty = fastype_of rel |
453 val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') |
470 val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') |
454 in |
471 in |
455 if rel' aconv rel then rtrm else relation_error ctxt rel rel' |
472 if rel' aconv rel then rtrm else term_mismatch "regularise (relation mismatch)" ctxt rel rel' |
456 end |
473 end |
457 |
474 |
458 | (_, Const _) => |
475 | (_, Const _) => |
459 let |
476 let |
460 val thy = ProofContext.theory_of ctxt |
477 val thy = ProofContext.theory_of ctxt |
462 | same_const _ _ = false |
479 | same_const _ _ = false |
463 in |
480 in |
464 if same_const rtrm qtrm then rtrm |
481 if same_const rtrm qtrm then rtrm |
465 else |
482 else |
466 let |
483 let |
467 val qtrm_str = Syntax.string_of_term ctxt qtrm |
484 val rtrm' = #rconst (qconsts_lookup thy qtrm) |
468 val exc1 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " not found)") |
485 handle NotFound => term_mismatch "regularize(constant notfound)" ctxt rtrm qtrm |
469 val exc2 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " mismatch)") |
486 in |
470 val rtrm' = #rconst (qconsts_lookup thy qtrm) handle NotFound => raise exc1 |
487 if Pattern.matches thy (rtrm', rtrm) |
471 in |
488 then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm |
472 if Pattern.matches thy (rtrm', rtrm) |
|
473 then rtrm else raise exc2 |
|
474 end |
489 end |
475 end |
490 end |
476 |
491 |
477 | (t1 $ t2, t1' $ t2') => |
492 | (t1 $ t2, t1' $ t2') => |
478 (regularize_trm ctxt (t1, t1')) $ (regularize_trm ctxt (t2, t2')) |
493 (regularize_trm ctxt (t1, t1')) $ (regularize_trm ctxt (t2, t2')) |