137 (* Regularize works as follows: |
137 (* Regularize works as follows: |
138 |
138 |
139 0. preliminary simplification step according to |
139 0. preliminary simplification step according to |
140 ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range |
140 ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range |
141 |
141 |
142 1. eliminating simple Ball/Bex/Bex1 instances (ball_reg_right bex_reg_left) |
142 1. eliminating simple Ball/Bex instances (ball_reg_right bex_reg_left) |
143 |
143 |
144 2. monos |
144 2. monos |
145 |
145 |
146 3. commutation rules for ball and bex (ball_all_comm bex_ex_comm) |
146 3. commutation rules for ball and bex (ball_all_comm bex_ex_comm) |
147 |
147 |
352 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
352 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
353 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
353 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
354 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
354 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
355 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
355 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
356 |
356 |
357 | Const (@{const_name "op ="},_) $ |
|
358 (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
|
359 (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
|
360 => rtac @{thm bex1_rsp} THEN' dtac @{thm QT_ex1} |
|
361 |
|
362 (* TODO: Check why less _ are needed then in EX/ALL cases *) |
|
363 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
|
364 (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _)) $ |
|
365 (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _)) |
|
366 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
|
367 |
|
368 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
357 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
369 (Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _) |
358 (Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _) |
370 => rtac @{thm bexeq_rsp} THEN' quotient_tac ctxt |
359 => rtac @{thm bexeq_rsp} THEN' quotient_tac ctxt |
371 |
360 |
372 | (_ $ |
361 | (_ $ |