equal
deleted
inserted
replaced
156 val thy = ProofContext.theory_of ctxt |
156 val thy = ProofContext.theory_of ctxt |
157 val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"} |
157 val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"} |
158 val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"} |
158 val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"} |
159 val simproc = Simplifier.simproc_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc)) |
159 val simproc = Simplifier.simproc_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc)) |
160 val simpset = (mk_minimal_ss ctxt) |
160 val simpset = (mk_minimal_ss ctxt) |
161 addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} @ (id_simps_get ctxt) |
161 addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} |
162 addsimprocs [simproc] |
162 addsimprocs [simproc] |
163 addSolver equiv_solver addSolver quotient_solver |
163 addSolver equiv_solver addSolver quotient_solver |
164 val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt) |
164 val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt) |
165 in |
165 in |
166 simp_tac simpset THEN' |
166 simp_tac simpset THEN' |
402 |
402 |
403 fun injection_tac ctxt = |
403 fun injection_tac ctxt = |
404 let |
404 let |
405 val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt) |
405 val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt) |
406 in |
406 in |
407 simp_tac ((mk_minimal_ss ctxt) addsimps (id_simps_get ctxt)) (* HACK? *) |
407 injection_step_tac ctxt rel_refl |
408 THEN' injection_step_tac ctxt rel_refl |
|
409 end |
408 end |
410 |
409 |
411 fun all_injection_tac ctxt = |
410 fun all_injection_tac ctxt = |
412 REPEAT_ALL_NEW (injection_tac ctxt) |
411 REPEAT_ALL_NEW (injection_tac ctxt) |
413 |
412 |
509 (* 4. simplification with *) |
508 (* 4. simplification with *) |
510 (* thm Quotient_abs_rep Quotient_rel_rep id_simps *) |
509 (* thm Quotient_abs_rep Quotient_rel_rep id_simps *) |
511 (* *) |
510 (* *) |
512 (* 5. test for refl *) |
511 (* 5. test for refl *) |
513 |
512 |
514 fun clean_tac_aux lthy = |
513 fun clean_tac lthy = |
515 let |
514 let |
516 (* FIXME/TODO produce defs with lthy, like prs and ids *) |
515 (* FIXME/TODO produce defs with lthy, like prs and ids *) |
517 val thy = ProofContext.theory_of lthy; |
516 val thy = ProofContext.theory_of lthy; |
518 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
517 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
519 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
518 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
528 fun_map_tac lthy, |
527 fun_map_tac lthy, |
529 lambda_prs_tac lthy, |
528 lambda_prs_tac lthy, |
530 simp_tac ss2, |
529 simp_tac ss2, |
531 TRY o rtac refl] |
530 TRY o rtac refl] |
532 end |
531 end |
533 |
|
534 fun clean_tac lthy = REPEAT o CHANGED o (clean_tac_aux lthy) (* HACK?? *) |
|
535 |
532 |
536 |
533 |
537 (****************************************************) |
534 (****************************************************) |
538 (* Tactic for Generalising Free Variables in a Goal *) |
535 (* Tactic for Generalising Free Variables in a Goal *) |
539 (****************************************************) |
536 (****************************************************) |