1647 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
1647 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
1648 end |
1648 end |
1649 *} |
1649 *} |
1650 |
1650 |
1651 ML {* |
1651 ML {* |
1652 fun lambda_prs_tac lthy quot = |
1652 fun lambda_prs_conv1 ctxt quot ctrm = |
1653 (EqSubst.eqsubst_tac lthy [0] @{thms LAMBDA_PRS} |
1653 case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) => |
1654 THEN' (RANGE [quotient_tac quot, quotient_tac quot])); |
1654 let |
|
1655 val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1); |
|
1656 val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2); |
|
1657 val thy = ProofContext.theory_of ctxt; |
|
1658 val [cty_a, cty_b, cty_c, cty_d] = map (ctyp_of thy) [ty_a, ty_b, ty_c, ty_d] |
|
1659 val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d]; |
|
1660 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
|
1661 val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS}; |
|
1662 val tac = |
|
1663 (compose_tac (false, lpi, 2)) THEN_ALL_NEW |
|
1664 (quotient_tac quot); |
|
1665 val gc = Drule.strip_imp_concl (cprop_of lpi); |
|
1666 val t = Goal.prove_internal [] gc (fn _ => tac 1) |
|
1667 val te = @{thm eq_reflection} OF [t] |
|
1668 val ts = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] te |
|
1669 val tl = Thm.lhs_of ts |
|
1670 (* val _ = tracing (Syntax.string_of_term @{context} (term_of ctrm));*) |
|
1671 (* val _ = tracing (Syntax.string_of_term @{context} (term_of tl));*) |
|
1672 val insts = matching_prs (ProofContext.theory_of ctxt) (term_of tl) (term_of ctrm); |
|
1673 val ti = Drule.eta_contraction_rule (Drule.instantiate insts ts); |
|
1674 (* val _ = tracing (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*) |
|
1675 in |
|
1676 Conv.rewr_conv ti ctrm |
|
1677 end |
|
1678 |
|
1679 *} |
|
1680 ML {* |
|
1681 fun lambda_prs_conv ctxt quot ctrm = |
|
1682 case (term_of ctrm) of |
|
1683 (Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs (_, _, x)) => |
|
1684 (Conv.arg_conv (Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt) |
|
1685 then_conv (lambda_prs_conv1 ctxt quot)) ctrm |
|
1686 | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm |
|
1687 | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm |
|
1688 | _ => Conv.all_conv ctrm |
|
1689 *} |
|
1690 |
|
1691 ML {* |
|
1692 fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) => |
|
1693 CONVERSION |
|
1694 (Conv.params_conv ~1 (fn ctxt => |
|
1695 (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv |
|
1696 Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) |
1655 *} |
1697 *} |
1656 |
1698 |
1657 ML {* |
1699 ML {* |
1658 fun TRY' tac = fn i => TRY (tac i) |
1700 fun TRY' tac = fn i => TRY (tac i) |
1659 *} |
1701 *} |
1662 fun clean_tac lthy quot defs reps_same = |
1704 fun clean_tac lthy quot defs reps_same = |
1663 let |
1705 let |
1664 val lower = flat (map (add_lower_defs lthy) defs) |
1706 val lower = flat (map (add_lower_defs lthy) defs) |
1665 in |
1707 in |
1666 TRY' (REPEAT_ALL_NEW (allex_prs_tac lthy quot)) THEN' |
1708 TRY' (REPEAT_ALL_NEW (allex_prs_tac lthy quot)) THEN' |
1667 TRY' (REPEAT_ALL_NEW (lambda_prs_tac lthy quot)) THEN' |
1709 TRY' (lambda_prs_tac lthy quot) THEN' |
1668 TRY' (REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower)) THEN' |
1710 TRY' (REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower)) THEN' |
1669 simp_tac (HOL_ss addsimps [reps_same]) |
1711 simp_tac (HOL_ss addsimps [reps_same]) |
1670 end |
1712 end |
1671 *} |
1713 *} |
1672 |
1714 |