# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264068682 -3600
# Node ID b91782991dc864339aeda5d64fb61e6625e1d4e1
# Parent  3e7a6ec549d1646d3d7a6071985605c8530766eb
Automatic cleaning of Bexeq<->Ex1 theorems.

diff -r 3e7a6ec549d1 -r b91782991dc8 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Thu Jan 21 10:55:09 2010 +0100
+++ b/Quot/Examples/IntEx.thy	Thu Jan 21 11:11:22 2010 +0100
@@ -195,9 +195,6 @@
 apply injection
 apply (rule quot_respect(9))
 apply (rule Quotient_my_int)
-
-apply(cleaning)
-apply (simp add: ex1_prs[OF Quotient_my_int])
 done
 
 lemma ho_tst: "foldl my_plus x [] = x"
diff -r 3e7a6ec549d1 -r b91782991dc8 Quot/QuotScript.thy
--- a/Quot/QuotScript.thy	Thu Jan 21 10:55:09 2010 +0100
+++ b/Quot/QuotScript.thy	Thu Jan 21 11:11:22 2010 +0100
@@ -468,7 +468,8 @@
 
 lemma ex1_prs:
   assumes a: "Quotient R absf repf"
-  shows "Bexeq R ((absf ---> id) f) = Ex1 f"
+  shows "((absf ---> id) ---> id) (Bexeq R) f = Ex1 f"
+apply simp
 apply (subst Bexeq_def)
 apply (subst Bex_def)
 apply (subst Ex1_def)
diff -r 3e7a6ec549d1 -r b91782991dc8 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Thu Jan 21 10:55:09 2010 +0100
+++ b/Quot/quotient_tacs.ML	Thu Jan 21 11:11:22 2010 +0100
@@ -500,7 +500,7 @@
 (* Cleaning consists of:
 
   1. folding of definitions and preservation lemmas;
-     and simplification with babs_prs all_prs ex_prs
+     and simplification with babs_prs all_prs ex_prs ex1_prs
 
   2. unfolding of ---> in front of everything, except
      bound variables
@@ -509,6 +509,7 @@
   3. 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).
 
   5. test for refl 
 *)
@@ -520,8 +521,8 @@
   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})
-  val ss2 = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep} @ ids)
+  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)
 in
   EVERY' [simp_tac ss1,
           fun_map_tac lthy,