equal
deleted
inserted
replaced
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_all: Proof.context -> term -> term |
30 val quotient_lift_all: Proof.context -> term -> term |
30 end; |
31 end; |
31 |
32 |
32 structure Quotient_Term: QUOTIENT_TERM = |
33 structure Quotient_Term: QUOTIENT_TERM = |
33 struct |
34 struct |
730 val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos |
731 val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos |
731 in |
732 in |
732 (ty_substs, const_substs @ rel_substs) |
733 (ty_substs, const_substs @ rel_substs) |
733 end |
734 end |
734 |
735 |
|
736 fun quotient_lift_const (b, t) ctxt = |
|
737 let |
|
738 val thy = ProofContext.theory_of ctxt |
|
739 val (ty_substs, _) = get_ty_trm_substs ctxt; |
|
740 val (_, ty) = dest_Const t; |
|
741 val nty = subst_tys thy ty_substs ty; |
|
742 in |
|
743 Free(b, nty) |
|
744 end |
735 |
745 |
736 (* |
746 (* |
737 Takes a term and |
747 Takes a term and |
738 |
748 |
739 * replaces raw constants by the quotient constants |
749 * replaces raw constants by the quotient constants |