# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264509522 -3600
# Node ID a792bfc1be2b75112e27a5fa309e45dcec4e3f8c
# Parent  ce774af6b9648c930567c489707cde5b3714b92b
Combined the simpsets in clean_tac and updated the comment. Now cleaning of splits does work.

diff -r ce774af6b964 -r a792bfc1be2b Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Tue Jan 26 12:24:23 2010 +0100
+++ b/Quot/Examples/FSet.thy	Tue Jan 26 13:38:42 2010 +0100
@@ -382,10 +382,6 @@
 
 lemma  "All (\<lambda>(x::'a fset, y). x = y)"
 apply(lifting test)
-apply(cleaning)
-thm all_prs
-apply(rule all_prs)
-apply(tactic {* Quotient_Tacs.quotient_tac @{context} 1*})
 done
 
 lemma test2: "Ex (\<lambda>(x::'a list, y). x = y)"
@@ -393,14 +389,6 @@
 
 lemma  "Ex (\<lambda>(x::'a fset, y). x = y)"
 apply(lifting test2)
-apply(cleaning)
-apply(rule ex_prs)
-apply(tactic {* Quotient_Tacs.quotient_tac @{context} 1*})
 done
 
-ML {* @{term "Ex (\<lambda>(x::'a fset, y). x = y)"} *}
-
-
-
-
 end
diff -r ce774af6b964 -r a792bfc1be2b Quot/Examples/SigmaEx.thy
--- a/Quot/Examples/SigmaEx.thy	Tue Jan 26 12:24:23 2010 +0100
+++ b/Quot/Examples/SigmaEx.thy	Tue Jan 26 13:38:42 2010 +0100
@@ -144,11 +144,6 @@
 apply (lifting tolift)
 apply (regularize)
 apply (simp)
-prefer 2
-apply cleaning
-apply (subst ex_prs)
-apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
-apply (rule refl)
 sorry
 
 lemma tolift':
diff -r ce774af6b964 -r a792bfc1be2b Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Tue Jan 26 12:24:23 2010 +0100
+++ b/Quot/quotient_tacs.ML	Tue Jan 26 13:38:42 2010 +0100
@@ -503,19 +503,17 @@
 
 (* Cleaning consists of:
 
-  1. folding of definitions and preservation lemmas;
-     and simplification with babs_prs all_prs ex_prs ex1_prs
-
-  2. unfolding of ---> in front of everything, except
+  1. unfolding of ---> in front of everything, except
      bound variables
      (this prevents lambda_prs from becoming stuck)
 
-  3. simplification with lambda_prs
+  2. simplification with lambda_prs
 
-  4. simplification with Quotient_abs_rep Quotient_rel_rep id_simps
-     and ex1_prs (since it may need lambdas to be folded).
+  3. simplification with Quotient_abs_rep Quotient_rel_rep id_simps
+     folding of definitions and preservation lemmas;
+     and simplification with babs_prs all_prs ex_prs ex1_prs
 
-  5. test for refl 
+  4. test for refl
 *)
 fun clean_tac lthy =
 let
@@ -525,13 +523,11 @@
   val ids = id_simps_get lthy
 
   fun mk_simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
-  val ss1 = mk_simps (defs @ prs @ @{thms babs_prs all_prs ex_prs ex1_prs})
-  val ss2 = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep ex1_prs} @ ids)
+  val ss = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs)
 in
-  EVERY' [simp_tac ss1,
-          fun_map_tac lthy,
+  EVERY' [fun_map_tac lthy,
           lambda_prs_tac lthy,
-          simp_tac ss2,
+          simp_tac ss,
           TRY o rtac refl]
 end