# HG changeset patch
# User cek@localhost.localdomain
# Date 1256364549 -7200
# Node ID 3300260b63a13919eef136d65ef7de9987a34357
# Parent  4f00ca4f5ef487766386347e821cce2a632878be
Better tactic and simplified the proof further

diff -r 4f00ca4f5ef4 -r 3300260b63a1 FSet.thy
--- a/FSet.thy	Fri Oct 23 18:20:06 2009 +0200
+++ b/FSet.thy	Sat Oct 24 08:09:09 2009 +0200
@@ -263,17 +263,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,
@@ -282,6 +282,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])),
@@ -296,7 +300,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}
 *}
 
 
@@ -304,52 +308,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
@@ -374,26 +346,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
 
diff -r 4f00ca4f5ef4 -r 3300260b63a1 QuotScript.thy
--- a/QuotScript.thy	Fri Oct 23 18:20:06 2009 +0200
+++ b/QuotScript.thy	Sat Oct 24 08:09:09 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