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