185 ML {*

   186 fun ball_reg_eqv_simproc rel_eqvs ss redex =

   187   let

   188     val ctxt = Simplifier.the_context ss

   189     val thy = ProofContext.theory_of ctxt

   190   in

   191   case redex of

   192       (ogl as ((Const (@{const_name "Ball"}, _)) $

   193         ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>

   194       (let

   195         val gl = Const (@{const_name "EQUIV"}, dummyT) $ R;

   196         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);

   197         val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);

   198         val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv} OF [eqv]]);

   199 (*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)

   200       in

   201         SOME thm

   202       end

   203       handle _ => NONE

   204       )

   205   | _ => NONE

   206   end

   207 *}

   208 

   209 ML {*

   210 fun ball_reg_eqv_range_simproc rel_eqvs ss redex =

   211   let

   212     val ctxt = Simplifier.the_context ss

   213     val thy = ProofContext.theory_of ctxt

   214   in

   215   case redex of

   216       (ogl as ((Const (@{const_name "Ball"}, _)) $

   217         ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) =>

   218       (let

   219         val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2;

   220         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);

   221         val _ = tracing (Syntax.string_of_term ctxt glc);

   222         val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);

   223         val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv_range} OF [eqv]]);

   224         val R1c = cterm_of thy R1;

   225         val thmi = Drule.instantiate' [] [SOME R1c] thm;

   226 (*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *)

   227         val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl

   228         val _ = tracing "AAA";

   229         val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);

   230         val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2));

   231       in

   232         SOME thm2

   233       end

   234       handle _ => NONE

   235 

   236       )

   237   | _ => NONE

   238   end

   239 *}

   240 

   241 ML {*

   242 fun regularize_tac ctxt rel_eqvs =

   243   let

   244     val pat1 = [@{term "Ball (Respects R) P"}];

   245     val pat2 = [@{term "Ball (Respects (R1 ===> R2)) P"}];

   246     val thy = ProofContext.theory_of ctxt

   247     val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc rel_eqvs))

   248     val simproc2 = Simplifier.simproc_i thy "" pat2 (K (ball_reg_eqv_range_simproc rel_eqvs))

   249     val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2]

   250   in 

   251   ObjectLogic.full_atomize_tac THEN'

   252   simp_tac simp_ctxt THEN'

   253   REPEAT_ALL_NEW (FIRST' [

   254     rtac @{thm ball_reg_right},

   255     rtac @{thm bex_reg_left},

   256     resolve_tac (Inductive.get_monos ctxt),

   257     rtac @{thm move_forall},

   258     rtac @{thm move_exists},

   259     simp_tac simp_ctxt

   260   ])

   261   end

   262 *}