687 |
687 |
688 |
688 |
689 |
689 |
690 (*** Wrapper for transforming an rthm into a qthm ***) |
690 (*** Wrapper for transforming an rthm into a qthm ***) |
691 |
691 |
692 (* |
692 (* subst_tys takes a list of (rty,qty) substitution pairs |
693 Finds subterms of a term that can be lifted and: |
693 and replaces all occurences of rty in the given type |
694 |
694 by appropriate qty, with substitution *) |
695 * replaces subterms matching lifted constants by the lifted constants |
|
696 |
|
697 * replaces equivalence relations by equalities |
|
698 |
|
699 * In constants, frees and schematic variables replaces |
|
700 subtypes matching lifted types by those types |
|
701 *) |
|
702 |
|
703 fun subst_ty thy ty (rty, qty) r = |
695 fun subst_ty thy ty (rty, qty) r = |
704 if r <> NONE then r else |
696 if r <> NONE then r else |
705 case try (Sign.typ_match thy (ty, rty)) Vartab.empty of |
697 case try (Sign.typ_match thy (ty, rty)) Vartab.empty of |
706 SOME inst => SOME (Envir.subst_type inst qty) |
698 SOME inst => SOME (Envir.subst_type inst qty) |
707 | NONE => NONE |
699 | NONE => NONE |
708 |
|
709 fun subst_tys thy substs ty = |
700 fun subst_tys thy substs ty = |
710 case fold (subst_ty thy ty) substs NONE of |
701 case fold (subst_ty thy ty) substs NONE of |
711 SOME ty => ty |
702 SOME ty => ty |
712 | NONE => |
703 | NONE => |
713 (case ty of |
704 (case ty of |
714 Type (s, tys) => Type (s, map (subst_tys thy substs) tys) |
705 Type (s, tys) => Type (s, map (subst_tys thy substs) tys) |
715 | x => x) |
706 | x => x) |
716 |
707 |
|
708 (* subst_trms takes a list of (rtrm,qtrm) substitution pairs |
|
709 and if the given term matches any of the raw terms it |
|
710 returns the appropriate qtrm instantiated. If none of |
|
711 them matched it returns NONE. *) |
717 fun subst_trm thy t (rtrm, qtrm) s = |
712 fun subst_trm thy t (rtrm, qtrm) s = |
718 if s <> NONE then s else |
713 if s <> NONE then s else |
719 case try (Pattern.match thy (t, rtrm)) (Vartab.empty, Vartab.empty) of |
714 case try (Pattern.match thy (t, rtrm)) (Vartab.empty, Vartab.empty) of |
720 SOME inst => SOME (Envir.subst_term inst qtrm) |
715 SOME inst => SOME (Envir.subst_term inst qtrm) |
721 | NONE => NONE; |
716 | NONE => NONE; |
722 |
|
723 fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE |
717 fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE |
724 |
718 |
|
719 (* prepares type and term substitution pairs to be used by above |
|
720 functions that let replace all raw constructs by appropriate |
|
721 lifted counterparts. *) |
725 fun get_ty_trm_substs ctxt = |
722 fun get_ty_trm_substs ctxt = |
726 let |
723 let |
727 val thy = ProofContext.theory_of ctxt |
724 val thy = ProofContext.theory_of ctxt |
728 val quot_infos = Quotient_Info.quotdata_dest ctxt |
725 val quot_infos = Quotient_Info.quotdata_dest ctxt |
729 val ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos |
726 val ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos |
732 fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel))) |
729 fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel))) |
733 val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos |
730 val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos |
734 in |
731 in |
735 (ty_substs, const_substs @ rel_substs) |
732 (ty_substs, const_substs @ rel_substs) |
736 end |
733 end |
|
734 |
|
735 |
|
736 (* |
|
737 Finds subterms of a term that can be lifted and: |
|
738 |
|
739 * replaces subterms matching lifted constants by the lifted constants |
|
740 |
|
741 * replaces equivalence relations by equalities |
|
742 |
|
743 * In constants, frees and schematic variables replaces |
|
744 subtypes matching lifted types by those types |
|
745 *) |
737 |
746 |
738 fun quotient_lift_all ctxt t = |
747 fun quotient_lift_all ctxt t = |
739 let |
748 let |
740 val thy = ProofContext.theory_of ctxt |
749 val thy = ProofContext.theory_of ctxt |
741 val (ty_substs, substs) = get_ty_trm_substs ctxt |
750 val (ty_substs, substs) = get_ty_trm_substs ctxt |