# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1256225740 -7200
# Node ID 7cefc03224df4235a2e6f6812a8f7a20cbdc2ef0
# Parent  c0d13b337c665bbf2b6af52ee097dc098a8cae5d
Further developing the tactic and simplifying the proof

diff -r c0d13b337c66 -r 7cefc03224df QuotMain.thy
--- a/QuotMain.thy	Thu Oct 22 16:24:02 2009 +0200
+++ b/QuotMain.thy	Thu Oct 22 17:35:40 2009 +0200
@@ -1031,6 +1031,12 @@
   (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
 *}
 
+ML {* 
+
+((simp_tac ((Simplifier.context @{context}  HOL_ss) addsimps @{thms FUN_REL.simps})) THEN' (fn _ => no_tac))
+*}
+
+ML {* ((simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps}))  THEN_ALL_NEW (fn _ => no_tac)) *}
 
 ML {*
 fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm =
@@ -1045,7 +1051,8 @@
       instantiate_tac @{thm APPLY_RSP} ctxt,
       rtac reflex_thm,
 (*      Cong_Tac.cong_tac @{thm cong},*)
-      atac
+      atac,
+      ((simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps}))  THEN_ALL_NEW (fn _ => no_tac))
     ])
 *}
 
@@ -1091,7 +1098,6 @@
 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 (simp only: FUN_REL.simps)
 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 *})
@@ -1115,8 +1121,6 @@
 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 *})
-(* MINE *)
-apply (simp only: FUN_REL.simps)
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 (* MK_COMB_TAC *)
 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
@@ -1128,7 +1132,6 @@
 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 (simp only: FUN_REL.simps)
 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 *})
@@ -1160,7 +1163,6 @@
 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 (simp add: FUN_REL.simps)
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 done