# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1283001445 -28800
# Node ID 749d09f52fde5df5f715f9c6a3a0694b09a96e0b
# Parent  053c69cb4a0e1406b1fcbe763dc85534f9c09792
quotient package: added a list of pre-simplification rules for Ball, Bex and mem

diff -r 053c69cb4a0e -r 749d09f52fde src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Aug 28 20:24:40 2010 +0800
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Aug 28 21:17:25 2010 +0800
@@ -618,11 +618,18 @@
 end
 
 
+(* Since we use Ball and Bex during the lifting and descending,
+   we cannot deal with lemmas containing them, unless we unfold 
+   them by default. Also mem cannot be regularized in general. *)
+
+val default_unfolds = @{thms Ball_def Bex_def mem_def}
+
+
 (** descending as tactic **)
 
 fun descend_procedure_tac ctxt simps =
 let
-  val ss = (mk_minimal_ss ctxt) addsimps simps
+  val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds)
 in
   full_simp_tac ss
   THEN' Object_Logic.full_atomize_tac
@@ -657,7 +664,7 @@
 (* the tactic leaves three subgoals to be proved *)
 fun lift_procedure_tac ctxt simps rthm =
 let
-  val ss = (mk_minimal_ss ctxt) addsimps simps
+  val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds)
 in
   full_simp_tac ss
   THEN' Object_Logic.full_atomize_tac