Stream: General

Topic: What’s the difference between `rewrite at` and `rewrite in`?

Wolfgang Jeltsch (Aug 15 2023 at 18:18):

HOL-Example.Rewrite_Examples contains applications of both rewrite at and rewrite in. Unfortunately, from the examples I cannot tell what the difference between the two is. Could anyone tell me?

Mathias Fleury (Aug 15 2023 at 19:18):

For rewrite at you give the exact position where the rewriting should happen and for rewrite in any subterm of the position works

Wolfgang Jeltsch (Aug 15 2023 at 20:41):

This is what I had expected, but it is not what I experience: It seems that also with at subterms are considered as well. For example, in the following code snippet rewriting is successful and the proof is accepted:

lemma "1 = Suc 0"
  by (rewrite at "⌑" One_nat_def) (fact refl)

Last updated: May 02 2024 at 12:29 UTC