equal
deleted
inserted
replaced
699 | NONE => |
699 | NONE => |
700 (case ty of |
700 (case ty of |
701 Type (s, tys) => Type (s, map (subst_tys thy substs) tys) |
701 Type (s, tys) => Type (s, map (subst_tys thy substs) tys) |
702 | x => x) |
702 | x => x) |
703 |
703 |
|
704 fun subst_trm thy t (rt, qt) s = |
|
705 if s <> NONE then s else |
|
706 case try (Pattern.match thy (t, rt)) (Vartab.empty, Vartab.empty) of |
|
707 SOME inst => SOME (Envir.subst_term inst qt) |
|
708 | NONE => NONE; |
|
709 fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE |
|
710 |
704 fun get_ty_trm_substs ctxt = |
711 fun get_ty_trm_substs ctxt = |
705 let |
712 let |
706 val thy = ProofContext.theory_of ctxt |
713 val thy = ProofContext.theory_of ctxt |
707 val quot_infos = Quotient_Info.quotdata_dest ctxt |
714 val quot_infos = Quotient_Info.quotdata_dest ctxt |
708 val ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos |
715 val ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos |
712 val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos |
719 val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos |
713 in |
720 in |
714 (ty_substs, (const_substs @ rel_substs)) |
721 (ty_substs, (const_substs @ rel_substs)) |
715 end |
722 end |
716 |
723 |
|
724 |
717 fun quotient_lift_all ctxt t = |
725 fun quotient_lift_all ctxt t = |
718 let |
726 let |
719 val thy = ProofContext.theory_of ctxt |
727 val thy = ProofContext.theory_of ctxt |
720 val (ty_substs, substs) = get_ty_trm_substs ctxt |
728 val (ty_substs, substs) = get_ty_trm_substs ctxt |
721 fun treat_subst t (rt, qt) s = |
|
722 if s <> NONE then s else |
|
723 case try (Pattern.match thy (t, rt)) (Vartab.empty, Vartab.empty) of |
|
724 SOME inst => SOME (Envir.subst_term inst qt) |
|
725 | NONE => NONE; |
|
726 fun treat_substs t = fold (treat_subst t) substs NONE |
|
727 fun lift_aux t = |
729 fun lift_aux t = |
728 case treat_substs t of |
730 case subst_trms thy substs t of |
729 SOME x => x |
731 SOME x => x |
730 | NONE => |
732 | NONE => |
731 (case t of |
733 (case t of |
732 a $ b => lift_aux a $ lift_aux b |
734 a $ b => lift_aux a $ lift_aux b |
733 | Abs(a, T, s) => |
735 | Abs(a, T, s) => |