equal
deleted
inserted
replaced
1576 (EqSubst.eqsubst_tac lthy [0] @{thms LAMBDA_PRS} |
1576 (EqSubst.eqsubst_tac lthy [0] @{thms LAMBDA_PRS} |
1577 THEN' (RANGE [quotient_tac quot, quotient_tac quot])); |
1577 THEN' (RANGE [quotient_tac quot, quotient_tac quot])); |
1578 *} |
1578 *} |
1579 |
1579 |
1580 ML {* |
1580 ML {* |
|
1581 fun TRY' tac = fn i => TRY (tac i) |
|
1582 *} |
|
1583 |
|
1584 ML {* |
1581 fun clean_tac lthy quot defs reps_same = |
1585 fun clean_tac lthy quot defs reps_same = |
1582 let |
1586 let |
1583 val lower = flat (map (add_lower_defs lthy) defs) |
1587 val lower = flat (map (add_lower_defs lthy) defs) |
1584 in |
1588 in |
1585 (REPEAT_ALL_NEW (allex_prs_tac lthy quot)) THEN' |
1589 TRY' (REPEAT_ALL_NEW (allex_prs_tac lthy quot)) THEN' |
1586 (REPEAT_ALL_NEW (lambda_prs_tac lthy quot)) THEN' |
1590 TRY' (REPEAT_ALL_NEW (lambda_prs_tac lthy quot)) THEN' |
1587 (REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower)) THEN' |
1591 TRY' (REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower)) THEN' |
1588 (simp_tac (HOL_ss addsimps [reps_same])) |
1592 simp_tac (HOL_ss addsimps [reps_same]) |
1589 end |
1593 end |
1590 *} |
1594 *} |
|
1595 |
|
1596 ML {* |
|
1597 fun lift_tac lthy thm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs = |
|
1598 (procedure_tac thm lthy) THEN' |
|
1599 (regularize_tac lthy rel_eqv rel_refl) THEN' |
|
1600 (REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms)) THEN' |
|
1601 (clean_tac lthy quot defs reps_same) |
|
1602 *} |
|
1603 |
1591 |
1604 |
1592 |
1605 |
1593 end |
1606 end |
1594 |
1607 |
1595 |
1608 |