968 (* A faster version *)

   969 

   970 ML {*

   971 fun inj_repabs_tac_fast ctxt quot_thms trans2 = SUBGOAL (fn (goal, i) =>

   972 (case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of

   973   ((Const (@{const_name FUN_REL}, _) $ _ $ _) $ (Abs _) $ (Abs _))

   974       => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam

   975 | (Const (@{const_name "op ="},_) $

   976     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $

   977     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))

   978       => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}

   979 | (Const (@{const_name FUN_REL}, _) $ _ $ _) $

   980     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $

   981     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)

   982       => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam

   983 | Const (@{const_name "op ="},_) $

   984     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $

   985     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)

   986       => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}

   987 | (Const (@{const_name FUN_REL}, _) $ _ $ _) $

   988     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $

   989     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)

   990       => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam

   991 | Const (@{const_name "op ="},_) $ _ $ _ => 

   992     rtac @{thm refl} ORELSE'

   993     (resolve_tac trans2 THEN' RANGE [

   994       quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])

   995 | _ $ _ $ _ =>

   996     instantiate_tac @{thm REP_ABS_RSP} ctxt THEN' RANGE [SOLVES' (quotient_tac ctxt quot_thms)]

   997 ) i)

   998 *}

   999 

  1000 ML {*

  1001 fun inj_repabs_tac' ctxt quot_thms rel_refl trans2 =

  1002   (FIRST' [

  1003     inj_repabs_tac_fast ctxt quot_thms trans2,

  1004     NDT ctxt "A" (APPLY_RSP_TAC ctxt THEN'

  1005                 (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms),

  1006                         quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),

  1007     NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN'

  1008                 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),

  1009     NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam),

  1010     NDT ctxt "E" (atac),

  1011     NDT ctxt "D" (resolve_tac rel_refl),

  1012     NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)),

  1013     NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))])

  1014 *}

  1015 

  1016 ML {*

  1017 fun all_inj_repabs_tac' ctxt quot_thms rel_refl trans2 =

  1018   REPEAT_ALL_NEW (inj_repabs_tac' ctxt quot_thms rel_refl trans2)

  1019 *}

  1020 

  1021 

  1022