On Wed, 23 May 2012, Christian Sternagel wrote:

- Why does "apply (simp only: rule)" and "unfolding rule" behave differently? E.g., on the term "Suc 0 = 0" with rule "Nat.nat.distinct(2)" the former results in "False", whereas the latter does nothing. Is it important that those two commands behave differently?

There are several historical accidents here.

Unfolding plain definitions should be unfolding plain definitions, not approximative simplification, which does sometimes more sometimes less than expected. Unfortunately, there are user theories out there, that use the 'unfolding' command for genuine simplification of facts and goals.

Likewise, (simp only: ...) should use only the given rules to simplify, not arbitrary complex loopers that might be there as well. When I introduced the "only" modifiers many years ago, I convinced myself that all loopers were trivial in the sense that there are required to solve the simplification problem successfully (by rule refl, TrueI etc.). Later on quite non-trivial loopers were added, and I missed the opportunity to sort this out.

The following sketch has been in my TODO list for many years to iron out these confusions:

  * unfold/unfolding strictly unfolds equations of the form c x y = t
    in the sense of c == %x y. t

  * (simp only: ...) only keeps trivial loopers, and removes arithmetic

  * (simp mainly: ...) is like the current (simp only: ...) for
    applications that really mean to keep non-trivial tools in the

isabelle-dev mailing list

Reply via email to