387 *) |
387 *) |
388 |
388 |
389 val mk_babs = Const (@{const_name Babs}, dummyT) |
389 val mk_babs = Const (@{const_name Babs}, dummyT) |
390 val mk_ball = Const (@{const_name Ball}, dummyT) |
390 val mk_ball = Const (@{const_name Ball}, dummyT) |
391 val mk_bex = Const (@{const_name Bex}, dummyT) |
391 val mk_bex = Const (@{const_name Bex}, dummyT) |
392 val mk_bex1 = Const (@{const_name Bex1}, dummyT) |
|
393 val mk_bex1_rel = Const (@{const_name Bex1_rel}, dummyT) |
392 val mk_bex1_rel = Const (@{const_name Bex1_rel}, dummyT) |
394 val mk_resp = Const (@{const_name Respects}, dummyT) |
393 val mk_resp = Const (@{const_name Respects}, dummyT) |
395 |
394 |
396 (* - applies f to the subterm of an abstraction, |
395 (* - applies f to the subterm of an abstraction, |
397 otherwise to the given term, |
396 otherwise to the given term, |
472 in |
471 in |
473 if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm |
472 if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm |
474 else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
473 else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
475 end |
474 end |
476 |
475 |
|
476 | (Const (@{const_name "Ex1"}, ty) $ |
|
477 (Abs (n, _, |
|
478 (Const (@{const_name "op &"}, _) $ |
|
479 (Const (@{const_name "op :"}, _) $ _ $ (Const (@{const_name "Respects"}, _) $ resrel)) $ |
|
480 (t $ _) |
|
481 ) |
|
482 )), Const (@{const_name "Ex1"}, ty') $ t') => |
|
483 let |
|
484 val t = incr_boundvars (~1) t |
|
485 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
486 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
|
487 val _ = tracing "bla" |
|
488 in |
|
489 if resrel <> needrel |
|
490 then term_mismatch "regularize (Bex1)" ctxt resrel needrel |
|
491 else mk_bex1_rel $ resrel $ subtrm |
|
492 end |
|
493 |
477 | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
494 | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
478 let |
495 let |
479 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
496 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
480 in |
497 in |
481 if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm |
498 if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm |
509 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
526 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
510 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
527 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
511 in |
528 in |
512 if resrel <> needrel |
529 if resrel <> needrel |
513 then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel |
530 then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel |
514 else mk_bex1_rel $ resrel $ subtrm |
|
515 end |
|
516 |
|
517 | (Const (@{const_name "Bex1"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, |
|
518 Const (@{const_name "Ex1"}, ty') $ t') => |
|
519 let |
|
520 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
521 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
|
522 in |
|
523 if resrel <> needrel |
|
524 then term_mismatch "regularize (Bex1)" ctxt resrel needrel |
|
525 else mk_bex1_rel $ resrel $ subtrm |
531 else mk_bex1_rel $ resrel $ subtrm |
526 end |
532 end |
527 |
533 |
528 | (* equalities need to be replaced by appropriate equivalence relations *) |
534 | (* equalities need to be replaced by appropriate equivalence relations *) |
529 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
535 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |