Stream: General

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


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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: Jun 20 2024 at 12:31 UTC