equal
deleted
inserted
replaced
130 (* Regularize works as follows: |
130 (* Regularize works as follows: |
131 |
131 |
132 0. preliminary simplification step according to |
132 0. preliminary simplification step according to |
133 ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range |
133 ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range |
134 |
134 |
135 1. eliminating simple Ball/Bex instances (ball_reg_right bex_reg_left) |
135 1. eliminating simple Ball/Bex/Bex1 instances (ball_reg_right bex_reg_left) |
136 |
136 |
137 2. monos |
137 2. monos |
138 |
138 |
139 3. commutation rules for ball and bex (ball_all_comm bex_ex_comm) |
139 3. commutation rules for ball and bex (ball_all_comm bex_ex_comm) |
140 |
140 |
157 addSolver equiv_solver addSolver quotient_solver |
157 addSolver equiv_solver addSolver quotient_solver |
158 val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt) |
158 val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt) |
159 in |
159 in |
160 simp_tac simpset THEN' |
160 simp_tac simpset THEN' |
161 REPEAT_ALL_NEW (CHANGED o FIRST' |
161 REPEAT_ALL_NEW (CHANGED o FIRST' |
162 [resolve_tac @{thms ball_reg_right bex_reg_left}, |
162 [resolve_tac @{thms ball_reg_right bex_reg_left bex1_bexeq_reg}, |
163 resolve_tac (Inductive.get_monos ctxt), |
163 resolve_tac (Inductive.get_monos ctxt), |
164 resolve_tac @{thms ball_all_comm bex_ex_comm}, |
164 resolve_tac @{thms ball_all_comm bex_ex_comm}, |
165 resolve_tac eq_eqvs, |
165 resolve_tac eq_eqvs, |
166 simp_tac simpset]) |
166 simp_tac simpset]) |
167 end |
167 end |