# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1282453083 -28800
# Node ID b97bd93fb9e20a89ea776be9a2844c4c0d4fad5d
# Parent  9bb0016f7e60714e9d1c1c565274d7562e4edf7a
allow for pre-simplification of lifted theorems

diff -r 9bb0016f7e60 -r b97bd93fb9e2 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sun Aug 22 10:45:53 2010 +0800
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sun Aug 22 12:58:03 2010 +0800
@@ -18,7 +18,7 @@
   val lift_procedure_tac: Proof.context -> thm -> int -> tactic
   val lift_tac: Proof.context -> thm list -> int -> tactic
 
-  val lifted: Proof.context -> typ list -> thm -> thm
+  val lifted: Proof.context -> typ list -> thm list -> thm -> thm
   val lifted_attrib: attribute
 end;
 
@@ -647,7 +647,7 @@
 end
 
 
-(** lifting as tactic **)
+(** lifting as a tactic **)
 
 (* the tactic leaves three subgoals to be proved *)
 fun lift_procedure_tac ctxt rthm =
@@ -661,39 +661,47 @@
       (rtac rule THEN' rtac rthm') i
     end)
 
+
+fun lift_single_tac ctxt rthm = 
+  lift_procedure_tac ctxt rthm
+  THEN' RANGE
+    [ regularize_tac ctxt,
+      all_injection_tac ctxt,
+      clean_tac ctxt ]
+
 fun lift_tac ctxt rthms =
+  Goal.conjunction_tac 
+  THEN' RANGE (map (lift_single_tac ctxt) rthms)
+
+
+(* automated lifting with pre-simplification of the theorems;
+   for internal usage *)
+fun lifted ctxt qtys simps rthm =
 let
-  fun mk_tac rthm =
-    lift_procedure_tac ctxt rthm
-    THEN' RANGE
-      [ regularize_tac ctxt,
-        all_injection_tac ctxt,
-        clean_tac ctxt ]
+  (* When the theorem is atomized, eta redexes are contracted,
+     so we do it both in the original theorem *)
+  val rthm' =
+    rthm 
+    |> asm_full_simplify (HOL_basic_ss addsimps simps)
+    |> Drule.eta_contraction_rule 
+  val ((_, [rthm'']), ctxt') = Variable.import false [rthm'] ctxt
+  val goal = derive_qtrm ctxt qtys (prop_of rthm'')
 in
-  Goal.conjunction_tac THEN' RANGE (map mk_tac rthms)
+  Goal.prove ctxt' [] [] goal 
+    (K ((asm_full_simp_tac (HOL_basic_ss addsimps simps)
+         THEN' lift_single_tac ctxt' rthm') 1))
+  |> singleton (ProofContext.export ctxt' ctxt)
 end
 
 
-(** lifting as an attribute **)
-
-fun lifted ctxt qtys thm =
-let
-  (* When the theorem is atomized, eta redexes are contracted,
-     so we do it both in the original theorem *)
-  val thm' = Drule.eta_contraction_rule thm
-  val ((_, [thm'']), ctxt') = Variable.import false [thm'] ctxt
-  val goal = derive_qtrm ctxt qtys (prop_of thm'')
-in
-  Goal.prove ctxt' [] [] goal (K (lift_tac ctxt' [thm'] 1))
-  |> singleton (ProofContext.export ctxt' ctxt)
-end;
+(* lifting as an attribute *)
 
 val lifted_attrib = Thm.rule_attribute (fn context => 
   let
     val ctxt = Context.proof_of context
     val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
   in
-    lifted ctxt qtys
+    lifted ctxt qtys []
   end)
 
 end; (* structure *)