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
etc.
* (simp mainly: ...) is like the current (simp only: ...) for
applications that really mean to keep non-trivial tools in the
simplifier.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
