502 (* *) |
502 (* *) |
503 (* 5. test for refl *) |
503 (* 5. test for refl *) |
504 |
504 |
505 fun clean_tac_aux lthy = |
505 fun clean_tac_aux lthy = |
506 let |
506 let |
|
507 (*FIXME produce defs with lthy, like prs and ids *) |
507 val thy = ProofContext.theory_of lthy; |
508 val thy = ProofContext.theory_of lthy; |
508 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
509 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
509 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
510 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
510 |
511 val prs = prs_rules_get lthy |
511 val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs} |
512 val ids = id_simps_get lthy |
512 val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy) |
513 |
513 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
514 fun mk_simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
514 in |
515 val ss1 = mk_simps (defs @ prs @ @{thms babs_prs all_prs ex_prs}) |
515 EVERY' [simp_tac (simps thms1), |
516 val ss2 = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep} @ ids) |
|
517 in |
|
518 EVERY' [simp_tac ss1, |
516 fun_map_tac lthy, |
519 fun_map_tac lthy, |
517 lambda_prs_tac lthy, |
520 lambda_prs_tac lthy, |
518 simp_tac (simps thms2), |
521 simp_tac ss2, |
519 TRY o rtac refl] |
522 TRY o rtac refl] |
520 end |
523 end |
521 |
524 |
522 fun clean_tac lthy = REPEAT o CHANGED o (clean_tac_aux lthy) (* HACK?? *) |
525 fun clean_tac lthy = REPEAT o CHANGED o (clean_tac_aux lthy) (* HACK?? *) |
523 |
526 |