# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1256282505 -7200
# Node ID 6b475324cef7e6cb4137702dd51a04ff669bbf00
# Parent  7cefc03224df4235a2e6f6812a8f7a20cbdc2ef0
Using RANGE tactical allows getting rid of the quotients immediately.

diff -r 7cefc03224df -r 6b475324cef7 QuotMain.thy
--- a/QuotMain.thy	Thu Oct 22 17:35:40 2009 +0200
+++ b/QuotMain.thy	Fri Oct 23 09:21:45 2009 +0200
@@ -1037,6 +1037,16 @@
 *}
 
 ML {* ((simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps}))  THEN_ALL_NEW (fn _ => no_tac)) *}
+ML {* RANGE *}
+
+ML {*
+fun quotient_tac quot_thm =
+  REPEAT_ALL_NEW (FIRST' [
+    rtac @{thm FUN_QUOTIENT},
+    rtac quot_thm,
+    rtac @{thm IDENTITY_QUOTIENT}
+  ])
+*}
 
 ML {*
 fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm =
@@ -1047,10 +1057,9 @@
     rtac @{thm ext},
     rtac trans_thm,
     res_forall_rsp_tac ctxt,
-      instantiate_tac @{thm REP_ABS_RSP(1)} ctxt,
-      instantiate_tac @{thm APPLY_RSP} ctxt,
+    (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
+    (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
       rtac reflex_thm,
-(*      Cong_Tac.cong_tac @{thm cong},*)
       atac,
       ((simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps}))  THEN_ALL_NEW (fn _ => no_tac))
     ])
@@ -1071,11 +1080,8 @@
 apply (simp only: id_def[symmetric])
 (* APPLY_RSP_TAC *)
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 (* LAMBDA_RES_TAC *)
 apply (simp only: FUN_REL.simps)
 apply (rule allI)
@@ -1096,16 +1102,8 @@
 (* APPLY_RSP_TAC *)
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-(* ABS_REP_RSP *)
-apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-(* LAMBDA_RSP *)
 apply (simp only: FUN_REL.simps)
 apply (rule allI)
 apply (rule allI)
@@ -1119,8 +1117,6 @@
 (* APPLY_RSP *)
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 (* MK_COMB_TAC *)
 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
@@ -1131,15 +1127,8 @@
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 (* CONS respects *)
 apply (simp add: FUN_REL.simps)
 apply (rule allI)
@@ -1153,16 +1142,10 @@
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (simp only: FUN_REL.simps)
 apply (rule allI)
 apply (rule allI)
 apply (rule impI)
-apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 done