# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1256220606 -7200
# Node ID ca0b28863ca95775061e214031f8e9b0f04e7ae4
# Parent  9c74171ff78b72dc3f80e20a9ae4a5fa489d3c95
Working on the proof and the tactic.

diff -r 9c74171ff78b -r ca0b28863ca9 QuotMain.thy
--- a/QuotMain.thy	Thu Oct 22 15:45:05 2009 +0200
+++ b/QuotMain.thy	Thu Oct 22 16:10:06 2009 +0200
@@ -1029,9 +1029,8 @@
     rtac @{thm FUN_QUOTIENT},
     rtac quot_thm,
     rtac @{thm IDENTITY_QUOTIENT},
-    rtac @{thm card1_rsp},
-      rtac @{thm ext},
-      rtac trans_thm,
+    rtac @{thm ext},
+    rtac trans_thm,
       instantiate_tac @{thm REP_ABS_RSP(1)} ctxt,
       instantiate_tac @{thm APPLY_RSP} ctxt,
       rtac reflex_thm,
@@ -1057,7 +1056,12 @@
 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 *})
-prefer 2
+apply (simp only: FUN_REL.simps)
+apply (rule allI)
+apply (rule allI)
+apply (rule impI)
+apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *})
+apply (simp only: FUN_REL.simps)
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 (* LAMBDA_RES_TAC *)
@@ -1087,14 +1091,13 @@
 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 *})
-(* TODO don't know how to handle ho_respects *)
+(* ABS_REP_RSP *)
 apply (simp only: FUN_REL.simps)
 apply (rule allI)
 apply (rule allI)
 apply (rule impI)
 apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *})
 apply (simp only: FUN_REL.simps)
-(* ABS_REP_RSP *)
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 (* LAMBDA_RSP *)
 apply (simp only: FUN_REL.simps)
@@ -1164,12 +1167,6 @@
 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 *})
-apply (simp only: FUN_REL.simps)
-apply (rule allI)
-apply (rule allI)
-apply (rule impI)
-apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *})
-apply (simp only: FUN_REL.simps)
 done
 
 prove list_induct_t: trm