
diff -r 6cdba30c6d66 -r 8c7597b19f0e QuotMain.thy
--- a/QuotMain.thy	Thu Dec 03 14:02:05 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 09:01:13 2009 +0100
@@ -965,6 +965,61 @@
   REPEAT_ALL_NEW (inj_repabs_tac ctxt quot_thms rel_refl trans2)
 *}
 
+(* A faster version *)
+
+ML {*
+fun inj_repabs_tac_fast ctxt quot_thms trans2 = SUBGOAL (fn (goal, i) =>
+(case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
+  ((Const (@{const_name FUN_REL}, _) $ _ $ _) $ (Abs _) $ (Abs _))
+      => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam
+| (Const (@{const_name "op ="},_) $
+    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
+      => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
+| (Const (@{const_name FUN_REL}, _) $ _ $ _) $
+    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+      => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam
+| Const (@{const_name "op ="},_) $
+    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+      => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
+| (Const (@{const_name FUN_REL}, _) $ _ $ _) $
+    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+      => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam
+| Const (@{const_name "op ="},_) $ _ $ _ => 
+    rtac @{thm refl} ORELSE'
+    (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 quot_thms)]
+) i)
+*}
+
+ML {*
+fun inj_repabs_tac' ctxt quot_thms rel_refl trans2 =
+  (FIRST' [
+    inj_repabs_tac_fast ctxt quot_thms trans2,
+    NDT ctxt "A" (APPLY_RSP_TAC ctxt THEN'
+                (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms),
+                        quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
+    NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN'
+                (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
+    NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam),
+    NDT ctxt "E" (atac),
+    NDT ctxt "D" (resolve_tac rel_refl),
+    NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)),
+    NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))])
+*}
+
+ML {*
+fun all_inj_repabs_tac' ctxt quot_thms rel_refl trans2 =
+  REPEAT_ALL_NEW (inj_repabs_tac' ctxt quot_thms rel_refl trans2)
+*}
+
+
+
 section {* Cleaning of the theorem *}
 
 




