364 *) |
364 *) |
365 |
365 |
366 val mk_babs = Const (@{const_name Babs}, dummyT) |
366 val mk_babs = Const (@{const_name Babs}, dummyT) |
367 val mk_ball = Const (@{const_name Ball}, dummyT) |
367 val mk_ball = Const (@{const_name Ball}, dummyT) |
368 val mk_bex = Const (@{const_name Bex}, dummyT) |
368 val mk_bex = Const (@{const_name Bex}, dummyT) |
|
369 val mk_bex1 = Const (@{const_name Bex1}, dummyT) |
369 val mk_resp = Const (@{const_name Respects}, dummyT) |
370 val mk_resp = Const (@{const_name Respects}, dummyT) |
370 |
371 |
371 (* - applies f to the subterm of an abstraction, |
372 (* - applies f to the subterm of an abstraction, |
372 otherwise to the given term, |
373 otherwise to the given term, |
373 - used by regularize, therefore abstracted |
374 - used by regularize, therefore abstracted |
458 if resrel <> needrel |
459 if resrel <> needrel |
459 then term_mismatch "regularize(bex)" ctxt resrel needrel |
460 then term_mismatch "regularize(bex)" ctxt resrel needrel |
460 else mk_bex $ (mk_resp $ resrel) $ subtrm |
461 else mk_bex $ (mk_resp $ resrel) $ subtrm |
461 end |
462 end |
462 |
463 |
|
464 | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
|
465 let |
|
466 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
467 in |
|
468 if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm |
|
469 else mk_bex1 $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
|
470 end |
|
471 |
|
472 | (Const (@{const_name "Bex1"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
|
473 let |
|
474 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
475 val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) |
|
476 in |
|
477 if resrel <> needrel |
|
478 then term_mismatch "regularize(bex1)" ctxt resrel needrel |
|
479 else mk_bex1 $ (mk_resp $ resrel) $ subtrm |
|
480 end |
|
481 |
463 | (* equalities need to be replaced by appropriate equivalence relations *) |
482 | (* equalities need to be replaced by appropriate equivalence relations *) |
464 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
483 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
465 if ty = ty' then rtrm |
484 if ty = ty' then rtrm |
466 else equiv_relation ctxt (domain_type ty, domain_type ty') |
485 else equiv_relation ctxt (domain_type ty, domain_type ty') |
467 |
486 |