equal
deleted
inserted
replaced
498 |
498 |
499 |
499 |
500 (* Cleaning consists of: |
500 (* Cleaning consists of: |
501 |
501 |
502 1. folding of definitions and preservation lemmas; |
502 1. folding of definitions and preservation lemmas; |
503 and simplification with babs_prs all_prs ex_prs |
503 and simplification with babs_prs all_prs ex_prs ex1_prs |
504 |
504 |
505 2. unfolding of ---> in front of everything, except |
505 2. unfolding of ---> in front of everything, except |
506 bound variables |
506 bound variables |
507 (this prevents lambda_prs from becoming stuck) |
507 (this prevents lambda_prs from becoming stuck) |
508 |
508 |
509 3. simplification with lambda_prs |
509 3. simplification with lambda_prs |
510 |
510 |
511 4. simplification with Quotient_abs_rep Quotient_rel_rep id_simps |
511 4. simplification with Quotient_abs_rep Quotient_rel_rep id_simps |
|
512 and ex1_prs (since it may need lambdas to be folded). |
512 |
513 |
513 5. test for refl |
514 5. test for refl |
514 *) |
515 *) |
515 fun clean_tac lthy = |
516 fun clean_tac lthy = |
516 let |
517 let |
518 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
519 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
519 val prs = prs_rules_get lthy |
520 val prs = prs_rules_get lthy |
520 val ids = id_simps_get lthy |
521 val ids = id_simps_get lthy |
521 |
522 |
522 fun mk_simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
523 fun mk_simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
523 val ss1 = mk_simps (defs @ prs @ @{thms babs_prs all_prs ex_prs}) |
524 val ss1 = mk_simps (defs @ prs @ @{thms babs_prs all_prs ex_prs ex1_prs}) |
524 val ss2 = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep} @ ids) |
525 val ss2 = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep ex1_prs} @ ids) |
525 in |
526 in |
526 EVERY' [simp_tac ss1, |
527 EVERY' [simp_tac ss1, |
527 fun_map_tac lthy, |
528 fun_map_tac lthy, |
528 lambda_prs_tac lthy, |
529 lambda_prs_tac lthy, |
529 simp_tac ss2, |
530 simp_tac ss2, |