# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260334789 -3600
# Node ID c86a47d4966e6d756bcd4dea07f9e384afbe9858
# Parent  5ededdde9e9f30d668a8d84de8de18b339296349
Temporarily repeated fun_map_tac 4 times. Cleaning for all examples work.

diff -r 5ededdde9e9f -r c86a47d4966e Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Wed Dec 09 00:54:46 2009 +0100
+++ b/Quot/Examples/FSet.thy	Wed Dec 09 05:59:49 2009 +0100
@@ -384,9 +384,6 @@
 apply(simp)
 apply(rule allI)
 apply(rule list_eq_refl)
-apply(cleaning)
-apply(simp add: fun_map.simps expand_fun_eq)
-apply(cleaning)
 done
 
 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))"
@@ -396,24 +393,12 @@
 (* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *)
 sorry
 
-(* Always safe to apply, but not too helpful *)
-lemma app_prs2:
-  assumes q1: "Quotient R1 abs1 rep1"
-  and     q2: "Quotient R2 abs2 rep2"
-  shows  "((abs1 ---> rep2) ((rep1 ---> abs2) f) (rep1 x)) = rep2 (((rep1 ---> abs2) f) x)"
-unfolding expand_fun_eq
-using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
-by simp
-
 lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))"
 sorry
 
 (* PROBLEM *)
 lemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))"
-apply(lifting_setup hard)
-defer
-apply(injection)
-apply(cleaning)
+apply(lifting hard)
 sorry
 
 end
diff -r 5ededdde9e9f -r c86a47d4966e Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Wed Dec 09 00:54:46 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Wed Dec 09 05:59:49 2009 +0100
@@ -321,7 +321,6 @@
 
 lemma "map (\<lambda>x. PLUS x ZERO) l = l"
 apply(lifting lam_tst4)
-apply(cleaning)
-sorry
+done
 
 end
diff -r 5ededdde9e9f -r c86a47d4966e Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Wed Dec 09 00:54:46 2009 +0100
+++ b/Quot/QuotMain.thy	Wed Dec 09 05:59:49 2009 +0100
@@ -1058,13 +1058,15 @@
     val thy = ProofContext.theory_of lthy;
     val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
       (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)
-    val thms1 = defs @ (prs_rules_get lthy)
-    val thms2 = @{thms fun_map.simps Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs} 
-                @ (id_simps_get lthy)
+    val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs}
+    val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy)
     fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
   in
     EVERY' [simp_tac (simps thms1),
             fun_map_tac lthy,
+            fun_map_tac lthy,
+            fun_map_tac lthy,
+            fun_map_tac lthy,
             lambda_prs_tac lthy,
             simp_tac (simps thms2),
             TRY o rtac refl]
diff -r 5ededdde9e9f -r c86a47d4966e Quot/QuotScript.thy
--- a/Quot/QuotScript.thy	Wed Dec 09 00:54:46 2009 +0100
+++ b/Quot/QuotScript.thy	Wed Dec 09 05:59:49 2009 +0100
@@ -389,6 +389,16 @@
 (******************************************)
 (* REST OF THE FILE IS UNUSED (until now) *)
 (******************************************)
+
+(* Always safe to apply, but not too helpful *)
+lemma app_prs2:
+  assumes q1: "Quotient R1 abs1 rep1"
+  and     q2: "Quotient R2 abs2 rep2"
+  shows  "((abs1 ---> rep2) ((rep1 ---> abs2) f) (rep1 x)) = rep2 (((rep1 ---> abs2) f) x)"
+unfolding expand_fun_eq
+using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
+by simp
+
 lemma Quotient_rel_abs:
   assumes a: "Quotient E Abs Rep"
   shows "E r s \<Longrightarrow> Abs r = Abs s"