src/HOL/Tools/Quotient/quotient_term.ML
changeset 35990 5ceedb86aa9d
parent 35843 23908b4dbc2f
child 36692 54b64d4ad524
     1.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Sat Mar 27 02:10:00 2010 +0100
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Sat Mar 27 14:48:46 2010 +0100
     1.3 @@ -26,8 +26,8 @@
     1.4    val inj_repabs_trm: Proof.context -> term * term -> term
     1.5    val inj_repabs_trm_chk: Proof.context -> term * term -> term
     1.6  
     1.7 -  val quotient_lift_const: string * term -> local_theory -> term
     1.8 -  val quotient_lift_all: Proof.context -> term -> term
     1.9 +  val quotient_lift_const: typ list -> string * term -> local_theory -> term
    1.10 +  val quotient_lift_all: typ list -> Proof.context -> term -> term
    1.11  end;
    1.12  
    1.13  structure Quotient_Term: QUOTIENT_TERM =
    1.14 @@ -720,23 +720,28 @@
    1.15  (* prepares type and term substitution pairs to be used by above
    1.16     functions that let replace all raw constructs by appropriate
    1.17     lifted counterparts. *)
    1.18 -fun get_ty_trm_substs ctxt =
    1.19 +fun get_ty_trm_substs qtys ctxt =
    1.20  let
    1.21    val thy = ProofContext.theory_of ctxt
    1.22    val quot_infos  = Quotient_Info.quotdata_dest ctxt
    1.23    val const_infos = Quotient_Info.qconsts_dest ctxt
    1.24 -  val ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos
    1.25 +  val all_ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos
    1.26 +  val ty_substs =
    1.27 +    if qtys = [] then all_ty_substs else
    1.28 +    filter (fn (_, qty) => qty mem qtys) all_ty_substs
    1.29    val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos
    1.30    fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel)))
    1.31    val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos
    1.32 +  fun valid_trm_subst (rt, qt) = (subst_tys thy ty_substs (fastype_of rt) = fastype_of qt)
    1.33 +  val all_trm_substs = const_substs @ rel_substs
    1.34  in
    1.35 -  (ty_substs, const_substs @ rel_substs)
    1.36 +  (ty_substs, filter valid_trm_subst all_trm_substs)
    1.37  end
    1.38  
    1.39 -fun quotient_lift_const (b, t) ctxt =
    1.40 +fun quotient_lift_const qtys (b, t) ctxt =
    1.41  let
    1.42    val thy = ProofContext.theory_of ctxt
    1.43 -  val (ty_substs, _) = get_ty_trm_substs ctxt;
    1.44 +  val (ty_substs, _) = get_ty_trm_substs qtys ctxt;
    1.45    val (_, ty) = dest_Const t;
    1.46    val nty = subst_tys thy ty_substs ty;
    1.47  in
    1.48 @@ -754,10 +759,10 @@
    1.49  
    1.50  *)
    1.51  
    1.52 -fun quotient_lift_all ctxt t =
    1.53 +fun quotient_lift_all qtys ctxt t =
    1.54  let
    1.55    val thy = ProofContext.theory_of ctxt
    1.56 -  val (ty_substs, substs) = get_ty_trm_substs ctxt
    1.57 +  val (ty_substs, substs) = get_ty_trm_substs qtys ctxt
    1.58    fun lift_aux t =
    1.59      case subst_trms thy substs t of
    1.60        SOME x => x