equal
deleted
inserted
replaced
433 end |
433 end |
434 |
434 |
435 | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "All"}, ty') $ t') => |
435 | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "All"}, ty') $ t') => |
436 let |
436 let |
437 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
437 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
438 in |
438 val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) |
439 if resrel <> Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) |
439 in |
440 then term_mismatch "regularize(ball)" ctxt rtrm qtrm |
440 if resrel <> needrel |
|
441 then term_mismatch "regularize(ball)" ctxt resrel needrel |
441 else mk_ball $ (mk_resp $ resrel) $ subtrm |
442 else mk_ball $ (mk_resp $ resrel) $ subtrm |
442 end |
443 end |
443 |
444 |
444 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
445 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
445 let |
446 let |
450 end |
451 end |
451 |
452 |
452 | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
453 | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
453 let |
454 let |
454 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
455 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
455 in |
456 val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) |
456 if resrel <> Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) |
457 in |
457 then term_mismatch "regularize(bex)" ctxt rtrm qtrm |
458 if resrel <> needrel |
|
459 then term_mismatch "regularize(bex)" ctxt resrel needrel |
458 else mk_bex $ (mk_resp $ resrel) $ subtrm |
460 else mk_bex $ (mk_resp $ resrel) $ subtrm |
459 end |
461 end |
460 |
462 |
461 | (* equalities need to be replaced by appropriate equivalence relations *) |
463 | (* equalities need to be replaced by appropriate equivalence relations *) |
462 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
464 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |