equal
deleted
inserted
replaced
1598 (EqSubst.eqsubst_tac lthy [0] @{thms LAMBDA_PRS} |
1598 (EqSubst.eqsubst_tac lthy [0] @{thms LAMBDA_PRS} |
1599 THEN' (RANGE [quotient_tac quot, quotient_tac quot])); |
1599 THEN' (RANGE [quotient_tac quot, quotient_tac quot])); |
1600 *} |
1600 *} |
1601 |
1601 |
1602 ML {* |
1602 ML {* |
|
1603 fun TRY' tac = fn i => TRY (tac i) |
|
1604 *} |
|
1605 |
|
1606 ML {* |
1603 fun clean_tac lthy quot defs reps_same = |
1607 fun clean_tac lthy quot defs reps_same = |
1604 let |
1608 let |
1605 val lower = flat (map (add_lower_defs lthy) defs) |
1609 val lower = flat (map (add_lower_defs lthy) defs) |
1606 in |
1610 in |
1607 (REPEAT_ALL_NEW (allex_prs_tac lthy quot)) THEN' |
1611 TRY' (REPEAT_ALL_NEW (allex_prs_tac lthy quot)) THEN' |
1608 (REPEAT_ALL_NEW (lambda_prs_tac lthy quot)) THEN' |
1612 TRY' (REPEAT_ALL_NEW (lambda_prs_tac lthy quot)) THEN' |
1609 (REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower)) THEN' |
1613 TRY' (REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower)) THEN' |
1610 (simp_tac (HOL_ss addsimps [reps_same])) |
1614 simp_tac (HOL_ss addsimps [reps_same]) |
1611 end |
1615 end |
1612 *} |
1616 *} |
|
1617 |
|
1618 ML {* |
|
1619 fun lift_tac lthy thm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs = |
|
1620 (procedure_tac thm lthy) THEN' |
|
1621 (regularize_tac lthy rel_eqv rel_refl) THEN' |
|
1622 (REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms)) THEN' |
|
1623 (clean_tac lthy quot defs reps_same) |
|
1624 *} |
|
1625 |
1613 |
1626 |
1614 |
1627 |
1615 end |
1628 end |
1616 |
1629 |
1617 |
1630 |