1609 |
1609 |
1610 |
1610 |
1611 (* del_simprocs *) |
1611 (* del_simprocs *) |
1612 |
1612 |
1613 fun del_simproc (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, |
1613 fun del_simproc (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, |
1614 (sign, lhs, proc, id)) = |
1614 (sign:Sign.sg, lhs, proc, id)) = |
1615 mk_mss (rules, congs, |
1615 mk_mss (rules, congs, |
1616 Net.delete_term ((lhs, (proc, id)), procs, eq_simproc) handle Net.DELETE => |
1616 Net.delete_term ((lhs, (proc, id)), procs, eq_simproc) handle Net.DELETE => |
1617 (trace_warning "simplification procedure not in simpset"; procs), |
1617 (trace_warning "simplification procedure not in simpset"; procs), |
1618 bounds, prems, mk_rews, termless); |
1618 bounds, prems, mk_rews, termless); |
1619 |
1619 |
1763 then sort rrs (rr::re1,re2) |
1763 then sort rrs (rr::re1,re2) |
1764 else sort rrs (re1,rr::re2) |
1764 else sort rrs (re1,rr::re2) |
1765 in sort rrs ([],[]) |
1765 in sort rrs ([],[]) |
1766 end |
1766 end |
1767 |
1767 |
1768 fun proc_rews [] = None |
1768 fun proc_rews _ [] = None |
1769 | proc_rews ((f, _) :: fs) = |
1769 | proc_rews eta_t ((f, _) :: fs) = |
1770 (case f signt t of |
1770 (case f signt eta_t of |
1771 None => proc_rews fs |
1771 None => proc_rews eta_t fs |
1772 | Some raw_thm => |
1772 | Some raw_thm => |
1773 (trace_thm "Proved rewrite rule: " raw_thm; |
1773 (trace_thm "Proved rewrite rule: " raw_thm; |
1774 (case rews (mk_procrule raw_thm) of |
1774 (case rews (mk_procrule raw_thm) of |
1775 None => proc_rews fs |
1775 None => proc_rews eta_t fs |
1776 | some => some))); |
1776 | some => some))); |
1777 in |
1777 in |
1778 (case t of |
1778 (case t of |
1779 Abs (_, _, body) $ u => (* FIXME bug!? (because of beta/eta overlap) *) |
1779 Abs (_, _, body) $ u => (* FIXME bug!? (because of beta/eta overlap) *) |
1780 Some (shypst, hypst, maxt, subst_bound (u, body), ders) |
1780 Some (shypst, hypst, maxt, subst_bound (u, body), ders) |
1781 | _ => |
1781 | _ => |
1782 (case rews (sort_rrules (Net.match_term rules t)) of |
1782 (case rews (sort_rrules (Net.match_term rules t)) of |
1783 None => proc_rews (Net.match_term procs t) |
1783 None => proc_rews (Pattern.eta_contract t) (Net.match_term procs t) |
1784 | some => some)) |
1784 | some => some)) |
1785 end; |
1785 end; |
1786 |
1786 |
1787 |
1787 |
1788 (* conversion to apply a congruence rule to a term *) |
1788 (* conversion to apply a congruence rule to a term *) |