[isabelle-dev] simplifier trace (and jedit)

[Makarius]

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