685 inj_repabs_trm ctxt (rtrm, qtrm) |
685 inj_repabs_trm ctxt (rtrm, qtrm) |
686 |> Syntax.check_term ctxt |
686 |> Syntax.check_term ctxt |
687 |
687 |
688 |
688 |
689 |
689 |
690 (*** Wrapper for transforming an rthm into a qthm ***) |
690 (*** Wrapper for automatically transforming an rthm into a qthm ***) |
691 |
691 |
692 (* subst_tys takes a list of (rty,qty) substitution pairs |
692 (* subst_tys takes a list of (rty, qty) substitution pairs |
693 and replaces all occurences of rty in the given type |
693 and replaces all occurences of rty in the given type |
694 by appropriate qty, with substitution *) |
694 by appropriate qty, with substitution *) |
695 fun subst_ty thy ty (rty, qty) r = |
695 fun subst_ty thy ty (rty, qty) r = |
696 if r <> NONE then r else |
696 if r <> NONE then r else |
697 case try (Sign.typ_match thy (rty, ty)) Vartab.empty of |
697 case try (Sign.typ_match thy (rty, ty)) Vartab.empty of |
703 | NONE => |
703 | NONE => |
704 (case ty of |
704 (case ty of |
705 Type (s, tys) => Type (s, map (subst_tys thy substs) tys) |
705 Type (s, tys) => Type (s, map (subst_tys thy substs) tys) |
706 | x => x) |
706 | x => x) |
707 |
707 |
708 (* subst_trms takes a list of (rtrm,qtrm) substitution pairs |
708 (* subst_trms takes a list of (rtrm, qtrm) substitution pairs |
709 and if the given term matches any of the raw terms it |
709 and if the given term matches any of the raw terms it |
710 returns the appropriate qtrm instantiated. If none of |
710 returns the appropriate qtrm instantiated. If none of |
711 them matched it returns NONE. *) |
711 them matched it returns NONE. *) |
712 fun subst_trm thy t (rtrm, qtrm) s = |
712 fun subst_trm thy t (rtrm, qtrm) s = |
713 if s <> NONE then s else |
713 if s <> NONE then s else |
720 functions that let replace all raw constructs by appropriate |
720 functions that let replace all raw constructs by appropriate |
721 lifted counterparts. *) |
721 lifted counterparts. *) |
722 fun get_ty_trm_substs ctxt = |
722 fun get_ty_trm_substs ctxt = |
723 let |
723 let |
724 val thy = ProofContext.theory_of ctxt |
724 val thy = ProofContext.theory_of ctxt |
725 val quot_infos = Quotient_Info.quotdata_dest ctxt |
725 val quot_infos = Quotient_Info.quotdata_dest ctxt |
|
726 val const_infos = Quotient_Info.qconsts_dest ctxt |
726 val ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos |
727 val ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos |
727 val const_infos = Quotient_Info.qconsts_dest ctxt |
|
728 val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos |
728 val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos |
729 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))) |
730 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 |
731 in |
731 in |
732 (ty_substs, const_substs @ rel_substs) |
732 (ty_substs, const_substs @ rel_substs) |
733 end |
733 end |
734 |
734 |
735 |
735 |
736 (* |
736 (* |
737 Finds subterms of a term that can be lifted and: |
737 Takes a term and |
738 |
738 |
739 * replaces subterms matching lifted constants by the lifted constants |
739 * replaces raw constants by the quotient constants |
740 |
740 |
741 * replaces equivalence relations by equalities |
741 * replaces equivalence relations by equalities |
742 |
742 |
743 * In constants, frees and schematic variables replaces |
743 * replaces raw types by the quotient types |
744 subtypes matching lifted types by those types |
744 |
745 *) |
745 *) |
746 |
746 |
747 fun quotient_lift_all ctxt t = |
747 fun quotient_lift_all ctxt t = |
748 let |
748 let |
749 val thy = ProofContext.theory_of ctxt |
749 val thy = ProofContext.theory_of ctxt |