507 in |
507 in |
508 if ty = ty' then subtrm |
508 if ty = ty' then subtrm |
509 else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm |
509 else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm |
510 end |
510 end |
511 |
511 |
512 | (Const (@{const_name Babs}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) => |
512 | (Const (\<^const_name>\<open>Babs\<close>, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) => |
513 let |
513 let |
514 val subtrm = regularize_trm ctxt (t, t') |
514 val subtrm = regularize_trm ctxt (t, t') |
515 val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty') |
515 val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty') |
516 in |
516 in |
517 if resrel <> needres |
517 if resrel <> needres |
518 then term_mismatch "regularize (Babs)" ctxt resrel needres |
518 then term_mismatch "regularize (Babs)" ctxt resrel needres |
519 else mk_babs $ resrel $ subtrm |
519 else mk_babs $ resrel $ subtrm |
520 end |
520 end |
521 |
521 |
522 | (Const (@{const_name All}, ty) $ t, Const (@{const_name All}, ty') $ t') => |
522 | (Const (\<^const_name>\<open>All\<close>, ty) $ t, Const (\<^const_name>\<open>All\<close>, ty') $ t') => |
523 let |
523 let |
524 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
524 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
525 in |
525 in |
526 if ty = ty' then Const (@{const_name All}, ty) $ subtrm |
526 if ty = ty' then Const (\<^const_name>\<open>All\<close>, ty) $ subtrm |
527 else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
527 else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
528 end |
528 end |
529 |
529 |
530 | (Const (@{const_name Ex}, ty) $ t, Const (@{const_name Ex}, ty') $ t') => |
530 | (Const (\<^const_name>\<open>Ex\<close>, ty) $ t, Const (\<^const_name>\<open>Ex\<close>, ty') $ t') => |
531 let |
531 let |
532 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
532 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
533 in |
533 in |
534 if ty = ty' then Const (@{const_name Ex}, ty) $ subtrm |
534 if ty = ty' then Const (\<^const_name>\<open>Ex\<close>, ty) $ subtrm |
535 else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
535 else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
536 end |
536 end |
537 |
537 |
538 | (Const (@{const_name Ex1}, ty) $ (Abs (_, _, |
538 | (Const (\<^const_name>\<open>Ex1\<close>, ty) $ (Abs (_, _, |
539 (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name Set.member}, _) $ _ $ |
539 (Const (\<^const_name>\<open>HOL.conj\<close>, _) $ (Const (\<^const_name>\<open>Set.member\<close>, _) $ _ $ |
540 (Const (@{const_name Respects}, _) $ resrel)) $ (t $ _)))), |
540 (Const (\<^const_name>\<open>Respects\<close>, _) $ resrel)) $ (t $ _)))), |
541 Const (@{const_name Ex1}, ty') $ t') => |
541 Const (\<^const_name>\<open>Ex1\<close>, ty') $ t') => |
542 let |
542 let |
543 val t_ = incr_boundvars (~1) t |
543 val t_ = incr_boundvars (~1) t |
544 val subtrm = apply_subt (regularize_trm ctxt) (t_, t') |
544 val subtrm = apply_subt (regularize_trm ctxt) (t_, t') |
545 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
545 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
546 in |
546 in |
547 if resrel <> needrel |
547 if resrel <> needrel |
548 then term_mismatch "regularize (Bex1)" ctxt resrel needrel |
548 then term_mismatch "regularize (Bex1)" ctxt resrel needrel |
549 else mk_bex1_rel $ resrel $ subtrm |
549 else mk_bex1_rel $ resrel $ subtrm |
550 end |
550 end |
551 |
551 |
552 | (Const (@{const_name Ex1}, ty) $ t, Const (@{const_name Ex1}, ty') $ t') => |
552 | (Const (\<^const_name>\<open>Ex1\<close>, ty) $ t, Const (\<^const_name>\<open>Ex1\<close>, ty') $ t') => |
553 let |
553 let |
554 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
554 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
555 in |
555 in |
556 if ty = ty' then Const (@{const_name Ex1}, ty) $ subtrm |
556 if ty = ty' then Const (\<^const_name>\<open>Ex1\<close>, ty) $ subtrm |
557 else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
557 else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
558 end |
558 end |
559 |
559 |
560 | (Const (@{const_name Ball}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t, |
560 | (Const (\<^const_name>\<open>Ball\<close>, ty) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ resrel) $ t, |
561 Const (@{const_name All}, ty') $ t') => |
561 Const (\<^const_name>\<open>All\<close>, ty') $ t') => |
562 let |
562 let |
563 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
563 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
564 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
564 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
565 in |
565 in |
566 if resrel <> needrel |
566 if resrel <> needrel |
567 then term_mismatch "regularize (Ball)" ctxt resrel needrel |
567 then term_mismatch "regularize (Ball)" ctxt resrel needrel |
568 else mk_ball $ (mk_resp $ resrel) $ subtrm |
568 else mk_ball $ (mk_resp $ resrel) $ subtrm |
569 end |
569 end |
570 |
570 |
571 | (Const (@{const_name Bex}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t, |
571 | (Const (\<^const_name>\<open>Bex\<close>, ty) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ resrel) $ t, |
572 Const (@{const_name Ex}, ty') $ t') => |
572 Const (\<^const_name>\<open>Ex\<close>, ty') $ t') => |
573 let |
573 let |
574 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
574 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
575 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
575 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
576 in |
576 in |
577 if resrel <> needrel |
577 if resrel <> needrel |
578 then term_mismatch "regularize (Bex)" ctxt resrel needrel |
578 then term_mismatch "regularize (Bex)" ctxt resrel needrel |
579 else mk_bex $ (mk_resp $ resrel) $ subtrm |
579 else mk_bex $ (mk_resp $ resrel) $ subtrm |
580 end |
580 end |
581 |
581 |
582 | (Const (@{const_name Bex1_rel}, ty) $ resrel $ t, Const (@{const_name Ex1}, ty') $ t') => |
582 | (Const (\<^const_name>\<open>Bex1_rel\<close>, ty) $ resrel $ t, Const (\<^const_name>\<open>Ex1\<close>, ty') $ t') => |
583 let |
583 let |
584 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
584 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
585 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
585 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
586 in |
586 in |
587 if resrel <> needrel |
587 if resrel <> needrel |
588 then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel |
588 then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel |
589 else mk_bex1_rel $ resrel $ subtrm |
589 else mk_bex1_rel $ resrel $ subtrm |
590 end |
590 end |
591 |
591 |
592 | (* equalities need to be replaced by appropriate equivalence relations *) |
592 | (* equalities need to be replaced by appropriate equivalence relations *) |
593 (Const (@{const_name HOL.eq}, ty), Const (@{const_name HOL.eq}, ty')) => |
593 (Const (\<^const_name>\<open>HOL.eq\<close>, ty), Const (\<^const_name>\<open>HOL.eq\<close>, ty')) => |
594 if ty = ty' then rtrm |
594 if ty = ty' then rtrm |
595 else equiv_relation ctxt (domain_type ty, domain_type ty') |
595 else equiv_relation ctxt (domain_type ty, domain_type ty') |
596 |
596 |
597 | (* in this case we just check whether the given equivalence relation is correct *) |
597 | (* in this case we just check whether the given equivalence relation is correct *) |
598 (rel, Const (@{const_name HOL.eq}, ty')) => |
598 (rel, Const (\<^const_name>\<open>HOL.eq\<close>, ty')) => |
599 let |
599 let |
600 val rel_ty = fastype_of rel |
600 val rel_ty = fastype_of rel |
601 val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') |
601 val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') |
602 in |
602 in |
603 if rel' aconv rel then rtrm |
603 if rel' aconv rel then rtrm |
621 if Pattern.matches thy (rtrm', rtrm) |
621 if Pattern.matches thy (rtrm', rtrm) |
622 then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm |
622 then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm |
623 end |
623 end |
624 end |
624 end |
625 |
625 |
626 | (((t1 as Const (@{const_name case_prod}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))), |
626 | (((t1 as Const (\<^const_name>\<open>case_prod\<close>, _)) $ Abs (v1, ty, Abs(v1', ty', s1))), |
627 ((t2 as Const (@{const_name case_prod}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) => |
627 ((t2 as Const (\<^const_name>\<open>case_prod\<close>, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) => |
628 regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2))) |
628 regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2))) |
629 |
629 |
630 | (((t1 as Const (@{const_name case_prod}, _)) $ Abs (v1, ty, s1)), |
630 | (((t1 as Const (\<^const_name>\<open>case_prod\<close>, _)) $ Abs (v1, ty, s1)), |
631 ((t2 as Const (@{const_name case_prod}, _)) $ Abs (v2, _ , s2))) => |
631 ((t2 as Const (\<^const_name>\<open>case_prod\<close>, _)) $ Abs (v2, _ , s2))) => |
632 regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2)) |
632 regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2)) |
633 |
633 |
634 | (t1 $ t2, t1' $ t2') => |
634 | (t1 $ t2, t1' $ t2') => |
635 regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2') |
635 regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2') |
636 |
636 |
697 |
697 |
698 (* bound variables need to be treated properly, |
698 (* bound variables need to be treated properly, |
699 as the type of subterms needs to be calculated *) |
699 as the type of subterms needs to be calculated *) |
700 fun inj_repabs_trm ctxt (rtrm, qtrm) = |
700 fun inj_repabs_trm ctxt (rtrm, qtrm) = |
701 case (rtrm, qtrm) of |
701 case (rtrm, qtrm) of |
702 (Const (@{const_name Ball}, T) $ r $ t, Const (@{const_name All}, _) $ t') => |
702 (Const (\<^const_name>\<open>Ball\<close>, T) $ r $ t, Const (\<^const_name>\<open>All\<close>, _) $ t') => |
703 Const (@{const_name Ball}, T) $ r $ (inj_repabs_trm ctxt (t, t')) |
703 Const (\<^const_name>\<open>Ball\<close>, T) $ r $ (inj_repabs_trm ctxt (t, t')) |
704 |
704 |
705 | (Const (@{const_name Bex}, T) $ r $ t, Const (@{const_name Ex}, _) $ t') => |
705 | (Const (\<^const_name>\<open>Bex\<close>, T) $ r $ t, Const (\<^const_name>\<open>Ex\<close>, _) $ t') => |
706 Const (@{const_name Bex}, T) $ r $ (inj_repabs_trm ctxt (t, t')) |
706 Const (\<^const_name>\<open>Bex\<close>, T) $ r $ (inj_repabs_trm ctxt (t, t')) |
707 |
707 |
708 | (Const (@{const_name Babs}, T) $ r $ t, t' as (Abs _)) => |
708 | (Const (\<^const_name>\<open>Babs\<close>, T) $ r $ t, t' as (Abs _)) => |
709 let |
709 let |
710 val rty = fastype_of rtrm |
710 val rty = fastype_of rtrm |
711 val qty = fastype_of qtrm |
711 val qty = fastype_of qtrm |
712 in |
712 in |
713 mk_repabs ctxt (rty, qty) (Const (@{const_name Babs}, T) $ r $ (inj_repabs_trm ctxt (t, t'))) |
713 mk_repabs ctxt (rty, qty) (Const (\<^const_name>\<open>Babs\<close>, T) $ r $ (inj_repabs_trm ctxt (t, t'))) |
714 end |
714 end |
715 |
715 |
716 | (Abs (x, T, t), Abs (x', T', t')) => |
716 | (Abs (x, T, t), Abs (x', T', t')) => |
717 let |
717 let |
718 val rty = fastype_of rtrm |
718 val rty = fastype_of rtrm |