24 val regularize_trm_chk: Proof.context -> term * term -> term |
24 val regularize_trm_chk: Proof.context -> term * term -> term |
25 |
25 |
26 val inj_repabs_trm: Proof.context -> term * term -> term |
26 val inj_repabs_trm: Proof.context -> term * term -> term |
27 val inj_repabs_trm_chk: Proof.context -> term * term -> term |
27 val inj_repabs_trm_chk: Proof.context -> term * term -> term |
28 |
28 |
29 val quotient_lift_const: string * term -> local_theory -> term |
29 val quotient_lift_const: typ list -> string * term -> local_theory -> term |
30 val quotient_lift_all: Proof.context -> term -> term |
30 val quotient_lift_all: typ list -> Proof.context -> term -> term |
31 end; |
31 end; |
32 |
32 |
33 structure Quotient_Term: QUOTIENT_TERM = |
33 structure Quotient_Term: QUOTIENT_TERM = |
34 struct |
34 struct |
35 |
35 |
718 fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE |
718 fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE |
719 |
719 |
720 (* prepares type and term substitution pairs to be used by above |
720 (* prepares type and term substitution pairs to be used by above |
721 functions that let replace all raw constructs by appropriate |
721 functions that let replace all raw constructs by appropriate |
722 lifted counterparts. *) |
722 lifted counterparts. *) |
723 fun get_ty_trm_substs ctxt = |
723 fun get_ty_trm_substs qtys ctxt = |
724 let |
724 let |
725 val thy = ProofContext.theory_of ctxt |
725 val thy = ProofContext.theory_of ctxt |
726 val quot_infos = Quotient_Info.quotdata_dest ctxt |
726 val quot_infos = Quotient_Info.quotdata_dest ctxt |
727 val const_infos = Quotient_Info.qconsts_dest ctxt |
727 val const_infos = Quotient_Info.qconsts_dest ctxt |
728 val ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos |
728 val all_ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos |
|
729 val ty_substs = |
|
730 if qtys = [] then all_ty_substs else |
|
731 filter (fn (_, qty) => qty mem qtys) all_ty_substs |
729 val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos |
732 val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos |
730 fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel))) |
733 fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel))) |
731 val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos |
734 val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos |
732 in |
735 fun valid_trm_subst (rt, qt) = (subst_tys thy ty_substs (fastype_of rt) = fastype_of qt) |
733 (ty_substs, const_substs @ rel_substs) |
736 val all_trm_substs = const_substs @ rel_substs |
734 end |
737 in |
735 |
738 (ty_substs, filter valid_trm_subst all_trm_substs) |
736 fun quotient_lift_const (b, t) ctxt = |
739 end |
737 let |
740 |
738 val thy = ProofContext.theory_of ctxt |
741 fun quotient_lift_const qtys (b, t) ctxt = |
739 val (ty_substs, _) = get_ty_trm_substs ctxt; |
742 let |
|
743 val thy = ProofContext.theory_of ctxt |
|
744 val (ty_substs, _) = get_ty_trm_substs qtys ctxt; |
740 val (_, ty) = dest_Const t; |
745 val (_, ty) = dest_Const t; |
741 val nty = subst_tys thy ty_substs ty; |
746 val nty = subst_tys thy ty_substs ty; |
742 in |
747 in |
743 Free(b, nty) |
748 Free(b, nty) |
744 end |
749 end |
752 |
757 |
753 * replaces raw types by the quotient types |
758 * replaces raw types by the quotient types |
754 |
759 |
755 *) |
760 *) |
756 |
761 |
757 fun quotient_lift_all ctxt t = |
762 fun quotient_lift_all qtys ctxt t = |
758 let |
763 let |
759 val thy = ProofContext.theory_of ctxt |
764 val thy = ProofContext.theory_of ctxt |
760 val (ty_substs, substs) = get_ty_trm_substs ctxt |
765 val (ty_substs, substs) = get_ty_trm_substs qtys ctxt |
761 fun lift_aux t = |
766 fun lift_aux t = |
762 case subst_trms thy substs t of |
767 case subst_trms thy substs t of |
763 SOME x => x |
768 SOME x => x |
764 | NONE => |
769 | NONE => |
765 (case t of |
770 (case t of |