summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Wed, 24 Oct 2012 17:40:56 +0200 | |

changeset 49974 | 791157a4179a |

parent 49973 | e84baadd4963 |

child 49975 | faf4afed009f |

ensured that rewr_conv rule t = "t == u" literally not just modulo beta-eta

src/Pure/conv.ML | file | annotate | diff | comparison | revisions |

--- a/src/Pure/conv.ML Mon Oct 22 22:47:14 2012 +0200 +++ b/src/Pure/conv.ML Wed Oct 24 17:40:56 2012 +0200 @@ -154,17 +154,22 @@ | _ => raise CTERM ("implies_concl_conv", [ct])); -(* single rewrite step, cf. REWR_CONV in HOL *) - +(* single rewrite step + beta-normalizes the rhs and takes care that lhs aconv ct *) fun rewr_conv rule ct = let val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule; val lhs = Thm.lhs_of rule1; val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1; - in - Drule.instantiate_normalize (Thm.match (lhs, ct)) rule2 + val rule3 = + Thm.instantiate (Thm.match (lhs, ct)) rule2 handle Pattern.MATCH => raise CTERM ("rewr_conv", [lhs, ct]) - end; + val rule4 = + if term_of(Thm.lhs_of rule3) aconv term_of ct then rule3 + else + let val ceq = Thm.dest_fun2 (Thm.cprop_of rule3) + in rule3 COMP Thm.trivial (Thm.mk_binop ceq ct (Thm.rhs_of rule3)) end + in Thm.transitive rule4 (Thm.beta_conversion true (Thm.rhs_of rule4)) end fun rewrs_conv rules = first_conv (map rewr_conv rules);