# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259925649 -3600
# Node ID 6b77cfd508e98e84c1c371aee5a35daaacaf04c0
# Parent  ebfd747b47ab07605d1881ae19348e4bd1222e0d
rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.

diff -r ebfd747b47ab -r 6b77cfd508e9 FIXME-TODO
--- a/FIXME-TODO	Fri Dec 04 11:33:58 2009 +0100
+++ b/FIXME-TODO	Fri Dec 04 12:20:49 2009 +0100
@@ -43,3 +43,6 @@
 
 
 - Integrate RSP/PRS lemmas in QuotList with the ones from IntEx etc.
+
+- Check all the places where we do "handle _"
+
diff -r ebfd747b47ab -r 6b77cfd508e9 LFex.thy
--- a/LFex.thy	Fri Dec 04 11:33:58 2009 +0100
+++ b/LFex.thy	Fri Dec 04 12:20:49 2009 +0100
@@ -219,7 +219,7 @@
 ML {*
   val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM}
   val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs}
-  val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs}
+  val trans2 = map (fn x => @{thm EQUALS_PRS} OF [x]) quot
   val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot
   val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same
 *}
diff -r ebfd747b47ab -r 6b77cfd508e9 QuotMain.thy
--- a/QuotMain.thy	Fri Dec 04 11:33:58 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 12:20:49 2009 +0100
@@ -708,7 +708,6 @@
 
 section {* RepAbs Injection Tactic *}
 
-(* TODO: check if it still works with first_order_match *)
 (* FIXME/TODO: do not handle everything *)
 ML {*
 fun instantiate_tac thm = 
@@ -1026,6 +1025,31 @@
   REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2)
 *}
 
+ML {*
+fun dest_fun_type (Type("fun", [T, S])) = (T, S)
+  | dest_fun_type _ = error "dest_fun_type"
+*}
+
+ML {*
+val rep_abs_rsp_tac =
+  Subgoal.FOCUS (fn {concl, context, ...} =>
+    case HOLogic.dest_Trueprop (term_of concl) of (rel $ lhs $ (rep $ (abs $ rhs))) =>
+    (let
+      val thy = ProofContext.theory_of context;
+      val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
+      val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
+      val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep];
+      val thm = Drule.instantiate' ty_inst t_inst @{thm REP_ABS_RSP}
+      val te = solve_quotient_assums context thm
+      val t_inst = map (SOME o (cterm_of thy)) [lhs, rhs];
+      val thm = Drule.instantiate' [] t_inst te
+    in
+      compose_tac (false, thm, 1) 1
+    end
+    handle _ => no_tac)
+  | _ => no_tac)
+*}
+
 (* A faster version *)
 
 ML {*
@@ -1054,7 +1078,8 @@
     (resolve_tac trans2 THEN' RANGE [
       quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])
 | _ $ _ $ _ =>
-    instantiate_tac @{thm REP_ABS_RSP} ctxt THEN' RANGE [SOLVES' (quotient_tac ctxt)]
+    rep_abs_rsp_tac ctxt
+| _ => error "inj_repabs_tac not a relation"
 ) i)
 *}
 
@@ -1108,12 +1133,6 @@
 *}
 
 ML {*
-fun dest_fun_type (Type("fun", [T, S])) = (T, S)
-  | dest_fun_type _ = error "dest_fun_type"
-*}
-
-
-ML {*
 fun lambda_allex_prs_simple_conv ctxt ctrm =
   case (term_of ctrm) of
     ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>