diff -r b4bef5ed8153 -r 53277fbb2dba QuotMain.thy
--- a/QuotMain.thy	Thu Oct 22 10:45:33 2009 +0200
+++ b/QuotMain.thy	Thu Oct 22 11:43:12 2009 +0200
@@ -1018,9 +1018,32 @@
   val insts = Thm.match (pat, concl)
 in
   rtac (Drule.instantiate insts thm) 1
-end)
+end
+handle _ => no_tac
+)
 *}
 
+ML {*
+fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm =
+  (FIRST' [
+    rtac @{thm FUN_QUOTIENT},
+    rtac quot_thm,
+    rtac @{thm IDENTITY_QUOTIENT},
+    rtac @{thm card1_rsp},
+      rtac @{thm ext},
+      rtac trans_thm,
+      instantiate_tac @{thm REP_ABS_RSP(1)} ctxt,
+      instantiate_tac @{thm APPLY_RSP} ctxt,
+      rtac reflex_thm,
+      Cong_Tac.cong_tac @{thm cong},
+      atac
+    ])
+*}
+
+ML {*
+fun r_mk_comb_tac_fset ctxt =
+  r_mk_comb_tac ctxt @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
+*}
 
 
 ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *}
@@ -1031,21 +1054,12 @@
 apply (atomize(full))
 apply (simp only: id_def[symmetric])
 (* APPLY_RSP_TAC *)
-apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *})
-apply (rule FUN_QUOTIENT)
-apply (rule FUN_QUOTIENT)
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
-apply (rule IDENTITY_QUOTIENT)
-apply (rule IDENTITY_QUOTIENT)
+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
-(* ABS_REP_RSP_TAC *)
-apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *})
-apply (rule FUN_QUOTIENT)
-apply (rule FUN_QUOTIENT)
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
-apply (rule IDENTITY_QUOTIENT)
+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)
@@ -1064,30 +1078,19 @@
 (* REFL_TAC *)
 apply (simp)
 (* APPLY_RSP_TAC *)
-apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *})
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
-apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *})
-apply (rule FUN_QUOTIENT)
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
+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 (simp only: FUN_REL.simps)
-apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *})
-apply (rule QUOTIENT_fset)
-(* MINE *)
-apply (rule list_eq_refl )
-apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *})
-apply (rule FUN_QUOTIENT)
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
-apply (rule IDENTITY_QUOTIENT)
+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 *})
 (* TODO don't know how to handle ho_respects *)
 prefer 2
 (* ABS_REP_RSP *)
-apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *})
-apply (rule FUN_QUOTIENT)
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 (* LAMBDA_RSP *)
 apply (simp only: FUN_REL.simps)
 apply (rule allI)
@@ -1100,45 +1103,32 @@
 (* REFL_TAC *)
 apply (simp)
 (* APPLY_RSP *)
-apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *})
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
-apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *})
-apply (rule FUN_QUOTIENT)
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
+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 *})
 (* MINE *)
 apply (simp only: FUN_REL.simps)
-apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *})
-apply (rule QUOTIENT_fset)
-(* FIRST_ASSUM MATCH_ACCEPT_TAC *)
-apply (assumption)
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 (* MK_COMB_TAC *)
 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
 (* REFL_TAC *)
 apply (simp)
 (* W(C (curry op THEN) (G... *)
-apply (rule ext)
-(* APPLY_RSP *)
-apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *})
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
-apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *})
-apply (rule FUN_QUOTIENT)
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
+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 {* 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 {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *})
-apply (rule QUOTIENT_fset)
-(* APPLY_RSP *)
-apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *})
-apply (rule QUOTIENT_fset)
-apply (rule QUOTIENT_fset)
-apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *})
-apply (rule IDENTITY_QUOTIENT)
-apply (rule FUN_QUOTIENT)
-apply (rule QUOTIENT_fset)
-apply (rule QUOTIENT_fset)
+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)
@@ -1148,35 +1138,23 @@
 apply (rule cons_preserves)
 apply (assumption)
 apply (simp)
-apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *})
-apply (rule QUOTIENT_fset)
-apply (assumption)
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 prefer 2
-apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *})
-apply (rule FUN_QUOTIENT)
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
-apply (rule IDENTITY_QUOTIENT)
+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 (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *})
-apply (rule FUN_QUOTIENT)
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
+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 APPLY_RSP} @{context} 1 *})
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
-apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *})
-apply (rule FUN_QUOTIENT)
-apply (rule QUOTIENT_fset)
-apply (rule IDENTITY_QUOTIENT)
+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 (simp add: FUN_REL.simps)
-apply (tactic {* instantiate_tac @{thm REP_ABS_RSP(1)} @{context} 1 *})
-apply (rule QUOTIENT_fset)
-apply (assumption)
+apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 sorry
 
 prove list_induct_t: trm