434 in |
434 in |
435 if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm |
435 if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm |
436 else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
436 else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
437 end |
437 end |
438 |
438 |
|
439 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
|
440 let |
|
441 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
442 in |
|
443 if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm |
|
444 else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
|
445 end |
|
446 |
|
447 | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
|
448 let |
|
449 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
450 in |
|
451 if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm |
|
452 else mk_bexeq $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
|
453 end |
|
454 |
439 | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, |
455 | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, |
440 Const (@{const_name "All"}, ty') $ t') => |
456 Const (@{const_name "All"}, ty') $ t') => |
441 let |
457 let |
442 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
458 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
443 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
459 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
445 if resrel <> needrel |
461 if resrel <> needrel |
446 then term_mismatch "regularize (Ball)" ctxt resrel needrel |
462 then term_mismatch "regularize (Ball)" ctxt resrel needrel |
447 else mk_ball $ (mk_resp $ resrel) $ subtrm |
463 else mk_ball $ (mk_resp $ resrel) $ subtrm |
448 end |
464 end |
449 |
465 |
450 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
|
451 let |
|
452 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
453 in |
|
454 if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm |
|
455 else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
|
456 end |
|
457 |
466 |
458 | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, |
467 | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, |
459 Const (@{const_name "Ex"}, ty') $ t') => |
468 Const (@{const_name "Ex"}, ty') $ t') => |
460 let |
469 let |
461 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
470 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
462 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') |
463 in |
472 in |
464 if resrel <> needrel |
473 if resrel <> needrel |
465 then term_mismatch "regularize (Bex)" ctxt resrel needrel |
474 then term_mismatch "regularize (Bex)" ctxt resrel needrel |
466 else mk_bex $ (mk_resp $ resrel) $ subtrm |
475 else mk_bex $ (mk_resp $ resrel) $ subtrm |
467 end |
|
468 |
|
469 | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
|
470 let |
|
471 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
472 in |
|
473 if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm |
|
474 else mk_bexeq $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
|
475 end |
476 end |
476 |
477 |
477 | (Const (@{const_name "Bexeq"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
478 | (Const (@{const_name "Bexeq"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
478 let |
479 let |
479 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
480 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |