--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Wed Sep 09 14:47:41 2015 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Wed Sep 09 20:57:21 2015 +0200
@@ -102,13 +102,13 @@
(case try (Thm.instantiate' ty_inst trm_inst) ball_bex_thm of
NONE => NONE
| SOME thm' =>
- (case try (get_match_inst thy (get_lhs thm')) redex of
+ (case try (get_match_inst thy (get_lhs thm')) (Thm.term_of redex) of
NONE => NONE
| SOME inst2 => try (Drule.instantiate_normalize inst2) thm'))
end
fun ball_bex_range_simproc ctxt redex =
- case redex of
+ (case Thm.term_of redex of
(Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $
(Const (@{const_name "rel_fun"}, _) $ R1 $ R2)) $ _) =>
calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
@@ -117,7 +117,7 @@
(Const (@{const_name "rel_fun"}, _) $ R1 $ R2)) $ _) =>
calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
- | _ => NONE
+ | _ => NONE)
(* Regularize works as follows:
@@ -147,17 +147,19 @@
fun eq_imp_rel_get ctxt =
map (OF1 eq_imp_rel) (rev (Named_Theorems.get ctxt @{named_theorems quot_equiv}))
+val regularize_simproc =
+ Simplifier.make_simproc @{context} "regularize"
+ {lhss = [@{term "Ball (Respects (R1 ===> R2)) P"}, @{term "Bex (Respects (R1 ===> R2)) P"}],
+ proc = K ball_bex_range_simproc,
+ identifier = []};
+
fun regularize_tac ctxt =
let
val thy = Proof_Context.theory_of ctxt
- val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"}
- val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"}
- val simproc =
- Simplifier.simproc_global_i thy "" [ball_pat, bex_pat] ball_bex_range_simproc
val simpset =
mk_minimal_simpset ctxt
addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
- addsimprocs [simproc]
+ addsimprocs [regularize_simproc]
addSolver equiv_solver addSolver quotient_solver
val eq_eqvs = eq_imp_rel_get ctxt
in