--- a/FSet.thy	Sat Oct 24 01:33:29 2009 +0200
+++ b/FSet.thy	Sat Oct 24 08:09:40 2009 +0200
@@ -306,17 +306,17 @@
 *}
 
 ML {*
-fun LAMBDA_RES_TAC ctxt =
-  case (term_of o #concl o fst) (Subgoal.focus ctxt 1 (Isar.goal ())) of
+fun LAMBDA_RES_TAC ctxt i st =
+  (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
     (_ $ (_ $ (Abs(_,_,_))$(Abs(_,_,_)))) =>
       (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
       (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
-  | _ => fn _ => no_tac
+  | _ => fn _ => no_tac) i st
 *}
 
 
 ML {*
-fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm =
+fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm res_thms =
   (FIRST' [
     rtac @{thm FUN_QUOTIENT},
     rtac quot_thm,
@@ -325,6 +325,10 @@
     rtac trans_thm,
     LAMBDA_RES_TAC ctxt,
     res_forall_rsp_tac ctxt,
+    (
+     (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps res_thms))
+     THEN_ALL_NEW (fn _ => no_tac)
+    ),
     (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
     rtac refl,
     (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
@@ -339,7 +343,7 @@
 
 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}
+  r_mk_comb_tac ctxt @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} @{thms ho_memb_rsp ho_cons_rsp}
 *}
 
 
@@ -347,52 +351,20 @@
 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
 
-
+ML {* trm_r *}
 prove list_induct_tr: trm_r
 apply (atomize(full))
 (* APPLY_RSP_TAC *)
+ML_prf {* val ctxt = @{context} *}
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 (* LAMBDA_RES_TAC *)
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-(* MK_COMB_TAC *)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
-(* MK_COMB_TAC *)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
-(* REFL_TAC *)
-apply (simp)
-(* MK_COMB_TAC *)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
-(* MK_COMB_TAC *)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
-(* REFL_TAC *)
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-(* APPLY_RSP_TAC *)
-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 *})
-(* MK_COMB_TAC *)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
-(* MK_COMB_TAC *)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
-(* REFL_TAC *)
-apply (simp)
-(* APPLY_RSP *)
-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 (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-(* W(C (curry op THEN) (G... *)
-apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-(* CONS respects *)
-apply (rule ho_cons_rsp)
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
+prefer 2
 apply (subst FUN_REL.simps)
 apply (rule allI)
 apply (rule allI)
 apply (rule impI)
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
+apply (auto)
 done
 
 prove list_induct_t: trm
@@ -417,26 +389,6 @@
 prove m2_t_p: m2_t_g
 apply (atomize(full))
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-prefer 2
-apply (subst FUN_REL.simps)
-apply (rule allI)
-apply (rule allI)
-apply (rule impI)
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-prefer 2
-apply (subst FUN_REL.simps)
-apply (rule allI)
-apply (rule allI)
-apply (rule impI)
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (subst FUN_REL.simps)
-apply (rule allI)
-apply (rule allI)
-apply (rule impI)
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (rule ho_memb_rsp)
-apply (rule ho_cons_rsp)
-apply (rule ho_memb_rsp)
 apply (auto)
 done
 

--- a/QuotScript.thy	Sat Oct 24 01:33:29 2009 +0200
+++ b/QuotScript.thy	Sat Oct 24 08:09:40 2009 +0200
@@ -498,6 +498,9 @@
   shows "!f. All f = Ball (Respects R) ((absf ---> id) f)"
   sorry
 
+lemma ho_all_prs: "op = ===> op = ===> op = All All"
+  apply (auto)
+  done
 
 end