384 (Abs (x, ty, t), Abs (_, ty', t')) => |
384 (Abs (x, ty, t), Abs (_, ty', t')) => |
385 let |
385 let |
386 val subtrm = Abs(x, ty, regularize_trm ctxt (t, t')) |
386 val subtrm = Abs(x, ty, regularize_trm ctxt (t, t')) |
387 in |
387 in |
388 if ty = ty' then subtrm |
388 if ty = ty' then subtrm |
389 else mk_babs $ (mk_resp $ new_equiv_relation ctxt (ty, ty')) $ subtrm |
389 else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm |
390 end |
390 end |
391 |
391 |
392 | (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') => |
393 let |
393 let |
394 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
394 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
395 in |
395 in |
396 if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm |
396 if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm |
397 else mk_ball $ (mk_resp $ new_equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
397 else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
398 end |
398 end |
399 |
399 |
400 | (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') => |
401 let |
401 let |
402 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
402 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
403 in |
403 in |
404 if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm |
404 if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm |
405 else mk_bex $ (mk_resp $ new_equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
405 else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
406 end |
406 end |
407 |
407 |
408 | (* equalities need to be replaced by appropriate equivalence relations *) |
408 | (* equalities need to be replaced by appropriate equivalence relations *) |
409 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
409 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
410 if ty = ty' then rtrm |
410 if ty = ty' then rtrm |
411 else new_equiv_relation ctxt (domain_type ty, domain_type ty') |
411 else equiv_relation ctxt (domain_type ty, domain_type ty') |
412 |
412 |
413 | (* 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 *) |
414 (rel, Const (@{const_name "op ="}, ty')) => |
414 (rel, Const (@{const_name "op ="}, ty')) => |
415 let |
415 let |
416 val exc = LIFT_MATCH "regularise (relation mismatch)" |
416 val exc = LIFT_MATCH "regularise (relation mismatch)" |
417 val rel_ty = fastype_of rel |
417 val rel_ty = fastype_of rel |
418 val rel' = new_equiv_relation ctxt (domain_type rel_ty, domain_type ty') |
418 val rel' = equiv_relation ctxt (domain_type rel_ty, domain_type ty') |
419 in |
419 in |
420 if rel' aconv rel then rtrm else raise exc |
420 if rel' aconv rel then rtrm else raise exc |
421 end |
421 end |
422 |
422 |
423 | (_, Const _) => |
423 | (_, Const _) => |