471 in |
471 in |
472 if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm |
472 if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm |
473 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 |
474 end |
474 end |
475 |
475 |
476 | (Const (@{const_name "Ex1"}, ty) $ |
476 | (Const (@{const_name "Ex1"}, ty) $ (Abs (_, _, |
477 (Abs (n, _, |
477 (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op :"}, _) $ _ $ |
478 (Const (@{const_name "op &"}, _) $ |
478 (Const (@{const_name "Respects"}, _) $ resrel)) $ (t $ _)))), |
479 (Const (@{const_name "op :"}, _) $ _ $ (Const (@{const_name "Respects"}, _) $ resrel)) $ |
479 Const (@{const_name "Ex1"}, ty') $ t') => |
480 (t $ _) |
480 let |
481 ) |
481 val t_ = incr_boundvars (~1) t |
482 )), Const (@{const_name "Ex1"}, ty') $ t') => |
482 val subtrm = apply_subt (regularize_trm ctxt) (t_, 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') |
483 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
487 val _ = tracing "bla" |
|
488 in |
484 in |
489 if resrel <> needrel |
485 if resrel <> needrel |
490 then term_mismatch "regularize (Bex1)" ctxt resrel needrel |
486 then term_mismatch "regularize (Bex1)" ctxt resrel needrel |
491 else mk_bex1_rel $ resrel $ subtrm |
487 else mk_bex1_rel $ resrel $ subtrm |
492 end |
488 end |
687 |
683 |
688 fun inj_repabs_trm_chk ctxt (rtrm, qtrm) = |
684 fun inj_repabs_trm_chk ctxt (rtrm, qtrm) = |
689 inj_repabs_trm ctxt (rtrm, qtrm) |
685 inj_repabs_trm ctxt (rtrm, qtrm) |
690 |> Syntax.check_term ctxt |
686 |> Syntax.check_term ctxt |
691 |
687 |
692 (*** Translating the goal automatically |
688 |
693 |
689 |
|
690 (*** Wrapper for transforming an rthm into a qthm ***) |
|
691 |
|
692 (* |
694 Finds subterms of a term that can be lifted and: |
693 Finds subterms of a term that can be lifted and: |
|
694 |
695 * replaces subterms matching lifted constants by the lifted constants |
695 * replaces subterms matching lifted constants by the lifted constants |
|
696 |
696 * replaces equivalence relations by equalities |
697 * replaces equivalence relations by equalities |
|
698 |
697 * In constants, frees and schematic variables replaces |
699 * In constants, frees and schematic variables replaces |
698 subtypes matching lifted types by those types *) |
700 subtypes matching lifted types by those types |
|
701 *) |
699 |
702 |
700 fun subst_ty thy ty (rty, qty) r = |
703 fun subst_ty thy ty (rty, qty) r = |
701 if r <> NONE then r else |
704 if r <> NONE then r else |
702 case try (Sign.typ_match thy (ty, rty)) Vartab.empty of |
705 case try (Sign.typ_match thy (ty, rty)) Vartab.empty of |
703 SOME inst => SOME (Envir.subst_type inst qty) |
706 SOME inst => SOME (Envir.subst_type inst qty) |
704 | NONE => NONE |
707 | NONE => NONE |
|
708 |
705 fun subst_tys thy substs ty = |
709 fun subst_tys thy substs ty = |
706 case fold (subst_ty thy ty) substs NONE of |
710 case fold (subst_ty thy ty) substs NONE of |
707 SOME ty => ty |
711 SOME ty => ty |
708 | NONE => |
712 | NONE => |
709 (case ty of |
713 (case ty of |
713 fun subst_trm thy t (rt, qt) s = |
717 fun subst_trm thy t (rt, qt) s = |
714 if s <> NONE then s else |
718 if s <> NONE then s else |
715 case try (Pattern.match thy (t, rt)) (Vartab.empty, Vartab.empty) of |
719 case try (Pattern.match thy (t, rt)) (Vartab.empty, Vartab.empty) of |
716 SOME inst => SOME (Envir.subst_term inst qt) |
720 SOME inst => SOME (Envir.subst_term inst qt) |
717 | NONE => NONE; |
721 | NONE => NONE; |
|
722 |
718 fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE |
723 fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE |
719 |
724 |
720 fun get_ty_trm_substs ctxt = |
725 fun get_ty_trm_substs ctxt = |
721 let |
726 let |
722 val thy = ProofContext.theory_of ctxt |
727 val thy = ProofContext.theory_of ctxt |
725 val const_infos = Quotient_Info.qconsts_dest ctxt |
730 val const_infos = Quotient_Info.qconsts_dest ctxt |
726 val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos |
731 val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos |
727 fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel))) |
732 fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel))) |
728 val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos |
733 val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos |
729 in |
734 in |
730 (ty_substs, (const_substs @ rel_substs)) |
735 (ty_substs, const_substs @ rel_substs) |
731 end |
736 end |
732 |
737 |
733 fun quotient_lift_all ctxt t = |
738 fun quotient_lift_all ctxt t = |
734 let |
739 let |
735 val thy = ProofContext.theory_of ctxt |
740 val thy = ProofContext.theory_of ctxt |
743 | Abs(a, ty, s) => |
748 | Abs(a, ty, s) => |
744 let |
749 let |
745 val (y, s') = Term.dest_abs (a, ty, s) |
750 val (y, s') = Term.dest_abs (a, ty, s) |
746 val nty = subst_tys thy ty_substs ty |
751 val nty = subst_tys thy ty_substs ty |
747 in |
752 in |
748 Abs(y, nty, abstract_over (Free (y, nty), (lift_aux s'))) |
753 Abs(y, nty, abstract_over (Free (y, nty), lift_aux s')) |
749 end |
754 end |
750 | Free(n, ty) => Free(n, subst_tys thy ty_substs ty) |
755 | Free(n, ty) => Free(n, subst_tys thy ty_substs ty) |
751 | Var(n, ty) => Var(n, subst_tys thy ty_substs ty) |
756 | Var(n, ty) => Var(n, subst_tys thy ty_substs ty) |
752 | Bound i => Bound i |
757 | Bound i => Bound i |
753 | Const(s, ty) => Const(s, subst_tys thy ty_substs ty)) |
758 | Const(s, ty) => Const(s, subst_tys thy ty_substs ty)) |