446 in |
446 in |
447 if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm |
447 if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm |
448 else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
448 else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
449 end |
449 end |
450 |
450 |
|
451 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
|
452 let |
|
453 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
454 in |
|
455 if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm |
|
456 else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
|
457 end |
|
458 |
|
459 | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
|
460 let |
|
461 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
462 in |
|
463 if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm |
|
464 else mk_bexeq $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
|
465 end |
|
466 |
451 | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, |
467 | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, |
452 Const (@{const_name "All"}, ty') $ t') => |
468 Const (@{const_name "All"}, ty') $ t') => |
453 let |
469 let |
454 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
470 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
455 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
471 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
457 if resrel <> needrel |
473 if resrel <> needrel |
458 then term_mismatch "regularize (Ball)" ctxt resrel needrel |
474 then term_mismatch "regularize (Ball)" ctxt resrel needrel |
459 else mk_ball $ (mk_resp $ resrel) $ subtrm |
475 else mk_ball $ (mk_resp $ resrel) $ subtrm |
460 end |
476 end |
461 |
477 |
462 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
|
463 let |
|
464 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
465 in |
|
466 if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm |
|
467 else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
|
468 end |
|
469 |
478 |
470 | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, |
479 | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, |
471 Const (@{const_name "Ex"}, ty') $ t') => |
480 Const (@{const_name "Ex"}, ty') $ t') => |
472 let |
481 let |
473 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
482 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
474 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
483 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
475 in |
484 in |
476 if resrel <> needrel |
485 if resrel <> needrel |
477 then term_mismatch "regularize (Bex)" ctxt resrel needrel |
486 then term_mismatch "regularize (Bex)" ctxt resrel needrel |
478 else mk_bex $ (mk_resp $ resrel) $ subtrm |
487 else mk_bex $ (mk_resp $ resrel) $ subtrm |
479 end |
|
480 |
|
481 | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
|
482 let |
|
483 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
484 in |
|
485 if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm |
|
486 else mk_bexeq $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
|
487 end |
488 end |
488 |
489 |
489 | (Const (@{const_name "Bexeq"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
490 | (Const (@{const_name "Bexeq"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
490 let |
491 let |
491 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
492 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |