686 (* Finds subterms of a term that are lifted to constants and replaces |
686 (* Finds subterms of a term that are lifted to constants and replaces |
687 those as well as occurrences of the equivalence relation and replaces |
687 those as well as occurrences of the equivalence relation and replaces |
688 those by equality. |
688 those by equality. |
689 Currently types are not checked so because of the dummyTs it may |
689 Currently types are not checked so because of the dummyTs it may |
690 not be complete *) |
690 not be complete *) |
|
691 fun subst_ty thy ty (rty, qty) r = |
|
692 if r <> NONE then r else |
|
693 case try (Sign.typ_match thy (ty, rty)) Vartab.empty of |
|
694 SOME inst => SOME (Envir.subst_type inst qty) |
|
695 | NONE => NONE |
|
696 fun subst_tys thy substs ty = |
|
697 case fold (subst_ty thy ty) substs NONE of |
|
698 SOME ty => ty |
|
699 | NONE => |
|
700 (case ty of |
|
701 Type (s, tys) => Type (s, map (subst_tys thy substs) tys) |
|
702 | x => x) |
|
703 |
|
704 fun get_ty_trm_substs ctxt = |
|
705 let |
|
706 val thy = ProofContext.theory_of ctxt |
|
707 val quot_infos = Quotient_Info.quotdata_dest ctxt |
|
708 val ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos |
|
709 val const_infos = Quotient_Info.qconsts_dest ctxt |
|
710 val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos |
|
711 fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel))) |
|
712 val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos |
|
713 in |
|
714 (ty_substs, (const_substs @ rel_substs)) |
|
715 end |
|
716 |
691 fun quotient_lift_all ctxt t = |
717 fun quotient_lift_all ctxt t = |
692 let |
718 let |
693 val thy = ProofContext.theory_of ctxt |
719 val thy = ProofContext.theory_of ctxt |
694 val const_infos = Quotient_Info.qconsts_dest ctxt |
720 val (ty_substs, substs) = get_ty_trm_substs ctxt |
695 val rel_infos = Quotient_Info.quotdata_dest ctxt |
721 fun treat_subst t (rt, qt) s = |
696 fun treat_const_info t qc_info s = |
|
697 if s <> NONE then s else |
722 if s <> NONE then s else |
698 case try (Pattern.match thy (t, #rconst qc_info)) (Vartab.empty, Vartab.empty) of |
723 case try (Pattern.match thy (t, rt)) (Vartab.empty, Vartab.empty) of |
699 SOME inst => SOME (Envir.subst_term inst (#qconst qc_info)) |
724 SOME inst => SOME (Envir.subst_term inst qt) |
700 | NONE => NONE; |
725 | NONE => NONE; |
701 fun treat_const t = fold (treat_const_info t) const_infos NONE |
726 fun treat_substs t = fold (treat_subst t) substs NONE |
702 fun treat_rel_info t rel_info s = |
|
703 if s <> NONE then s else |
|
704 if Pattern.matches thy (t, #equiv_rel rel_info) then SOME (Const ("op =", dummyT)) |
|
705 else NONE |
|
706 fun treat_rel t = fold (treat_rel_info t) rel_infos NONE |
|
707 fun lift_aux t = |
727 fun lift_aux t = |
708 case treat_const t of |
728 case treat_substs t of |
709 SOME x => x |
729 SOME x => x |
710 | NONE => |
730 | NONE => |
711 (case treat_rel t of |
731 (case t of |
712 SOME x => x |
732 a $ b => lift_aux a $ lift_aux b |
713 | NONE => |
733 | Abs(a, T, s) => |
714 (case t of |
734 let val (y, s') = Term.dest_abs (a, T, s) in |
715 a $ b => lift_aux a $ lift_aux b |
735 Abs(y, dummyT, abstract_over (Free (y, dummyT), (lift_aux s'))) |
716 | Abs(a, T, s) => |
736 end |
717 let val (y, s') = Term.dest_abs (a, T, s) in |
737 | Free(n, _) => Free(n, dummyT) |
718 Abs(y, dummyT, abstract_over (Free (y, dummyT), (lift_aux s'))) |
738 | Var(n, _) => Var(n, dummyT) |
719 end |
739 | Bound i => Bound i |
720 | Free(n, _) => Free(n, dummyT) |
740 | Const(s, _) => Const(s, dummyT)) |
721 | Var(n, _) => Var(n, dummyT) |
|
722 | Bound i => Bound i |
|
723 | Const(s, _) => Const(s, dummyT))) |
|
724 in |
741 in |
725 lift_aux t |
742 lift_aux t |
726 end |
743 end |
727 |
744 |
|
745 |
728 end; (* structure *) |
746 end; (* structure *) |
729 |
747 |
730 |
748 |
731 |
749 |