# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269697726 -3600
# Node ID 5ceedb86aa9d7462391aebc229abef57ec7be74c
# Parent  27e2fa7d4ce7fa3366a58f2cacb8516631782f79
Automated lifting can be restricted to specific quotient types

diff -r 27e2fa7d4ce7 -r 5ceedb86aa9d src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Sat Mar 27 02:10:00 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Sat Mar 27 14:48:46 2010 +0100
@@ -12,7 +12,8 @@
   val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) ->
     local_theory -> (term * thm) * local_theory
 
-  val quotient_lift_const: string * term -> local_theory -> (term * thm) * local_theory
+  val quotient_lift_const: typ list -> string * term -> local_theory ->
+    (term * thm) * local_theory
 end;
 
 structure Quotient_Def: QUOTIENT_DEF =
@@ -86,9 +87,9 @@
   quotient_def (decl, (attr, (lhs, rhs))) lthy''
 end
 
-fun quotient_lift_const (b, t) ctxt =
+fun quotient_lift_const qtys (b, t) ctxt =
   quotient_def ((NONE, NoSyn), (Attrib.empty_binding,
-    (Quotient_Term.quotient_lift_const (b, t) ctxt, t))) ctxt
+    (Quotient_Term.quotient_lift_const qtys (b, t) ctxt, t))) ctxt
 
 local
   structure P = OuterParse;
diff -r 27e2fa7d4ce7 -r 5ceedb86aa9d src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Mar 27 02:10:00 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Mar 27 14:48:46 2010 +0100
@@ -15,6 +15,7 @@
   val lift_tac: Proof.context -> thm list -> int -> tactic
   val quotient_tac: Proof.context -> int -> tactic
   val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic
+  val lifted: typ list -> Proof.context -> thm -> thm
   val lifted_attrib: attribute
 end;
 
@@ -650,17 +651,16 @@
   THEN' RANGE (map mk_tac rthms)
 end
 
-(* An Attribute which automatically constructs the qthm *)
-fun lifted_attrib_aux context thm =
+fun lifted qtys ctxt thm =
 let
-  val ctxt = Context.proof_of context
   val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt
-  val goal = (quotient_lift_all ctxt' o prop_of) thm'
+  val goal = (quotient_lift_all qtys ctxt' o prop_of) thm'
 in
   Goal.prove ctxt' [] [] goal (K (lift_tac ctxt' [thm] 1))
   |> singleton (ProofContext.export ctxt' ctxt)
 end;
 
-val lifted_attrib = Thm.rule_attribute lifted_attrib_aux
+(* An Attribute which automatically constructs the qthm *)
+val lifted_attrib = Thm.rule_attribute (fn ctxt => lifted [] (Context.proof_of ctxt))
 
 end; (* structure *)
diff -r 27e2fa7d4ce7 -r 5ceedb86aa9d src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Sat Mar 27 02:10:00 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Sat Mar 27 14:48:46 2010 +0100
@@ -26,8 +26,8 @@
   val inj_repabs_trm: Proof.context -> term * term -> term
   val inj_repabs_trm_chk: Proof.context -> term * term -> term
 
-  val quotient_lift_const: string * term -> local_theory -> term
-  val quotient_lift_all: Proof.context -> term -> term
+  val quotient_lift_const: typ list -> string * term -> local_theory -> term
+  val quotient_lift_all: typ list -> Proof.context -> term -> term
 end;
 
 structure Quotient_Term: QUOTIENT_TERM =
@@ -720,23 +720,28 @@
 (* prepares type and term substitution pairs to be used by above
    functions that let replace all raw constructs by appropriate
    lifted counterparts. *)
-fun get_ty_trm_substs ctxt =
+fun get_ty_trm_substs qtys ctxt =
 let
   val thy = ProofContext.theory_of ctxt
   val quot_infos  = Quotient_Info.quotdata_dest ctxt
   val const_infos = Quotient_Info.qconsts_dest ctxt
-  val ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos
+  val all_ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos
+  val ty_substs =
+    if qtys = [] then all_ty_substs else
+    filter (fn (_, qty) => qty mem qtys) all_ty_substs
   val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos
   fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel)))
   val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos
+  fun valid_trm_subst (rt, qt) = (subst_tys thy ty_substs (fastype_of rt) = fastype_of qt)
+  val all_trm_substs = const_substs @ rel_substs
 in
-  (ty_substs, const_substs @ rel_substs)
+  (ty_substs, filter valid_trm_subst all_trm_substs)
 end
 
-fun quotient_lift_const (b, t) ctxt =
+fun quotient_lift_const qtys (b, t) ctxt =
 let
   val thy = ProofContext.theory_of ctxt
-  val (ty_substs, _) = get_ty_trm_substs ctxt;
+  val (ty_substs, _) = get_ty_trm_substs qtys ctxt;
   val (_, ty) = dest_Const t;
   val nty = subst_tys thy ty_substs ty;
 in
@@ -754,10 +759,10 @@
 
 *)
 
-fun quotient_lift_all ctxt t =
+fun quotient_lift_all qtys ctxt t =
 let
   val thy = ProofContext.theory_of ctxt
-  val (ty_substs, substs) = get_ty_trm_substs ctxt
+  val (ty_substs, substs) = get_ty_trm_substs qtys ctxt
   fun lift_aux t =
     case subst_trms thy substs t of
       SOME x => x