151 |
151 |
152 5. then simplification like 0 |
152 5. then simplification like 0 |
153 |
153 |
154 finally jump back to 1 |
154 finally jump back to 1 |
155 *) |
155 *) |
|
156 |
156 fun regularize_tac ctxt = |
157 fun regularize_tac ctxt = |
157 let |
158 let |
158 val thy = ProofContext.theory_of ctxt |
159 val thy = ProofContext.theory_of ctxt |
159 val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"} |
160 val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"} |
160 val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"} |
161 val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"} |
161 val simproc = Simplifier.simproc_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc)) |
162 val simproc = Simplifier.simproc_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc)) |
162 val simpset = (mk_minimal_ss ctxt) |
163 val simpset = (mk_minimal_ss ctxt) |
163 addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} |
164 addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} |
164 addsimprocs [simproc] |
165 addsimprocs [simproc] |
165 addSolver equiv_solver addSolver quotient_solver |
166 addSolver equiv_solver addSolver quotient_solver |
166 val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt) |
167 val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)} |
|
168 val eq_eqvs = map (OF1 eq_imp_rel) (equiv_rules_get ctxt) |
167 in |
169 in |
168 simp_tac simpset THEN' |
170 simp_tac simpset THEN' |
169 REPEAT_ALL_NEW (CHANGED o FIRST' |
171 REPEAT_ALL_NEW (CHANGED o FIRST' |
170 [resolve_tac @{thms ball_reg_right bex_reg_left bex1_bexeq_reg}, |
172 [resolve_tac @{thms ball_reg_right bex_reg_left bex1_bexeq_reg}, |
171 resolve_tac (Inductive.get_monos ctxt), |
173 resolve_tac (Inductive.get_monos ctxt), |