Re: [isabelle] Change in behavior of "simp" from Isabelle 2014 to Isabelle2015

On Sat, 30 May 2015, Eugene W. Stark wrote:

With Isabelle2015, I have so far experienced a number of times the situation in which I enter "using foobar_def", then invoke "try" and am told "Try this: by (simp add: foobar_def)". Previously in Isabelle2014 it generally seemed to be enough to say "using foobar_def by simp", but now in Isabelle2015 it is often necessary to explicitly add foobar_def as a simplification. The point is, I already know that foobar_def is going to be needed in the proof, but I don't necessarily know that it will have to be used as a simplification. Also, as far as I know, the "using" clause does not provide a way to indicate which of the facts being used are to be used as simplifications, as opposed to ordinary lemmas.

Was this change in behavior intentional? Is there a workaround? If necessary, I will try to get a standalone example, but I don't have one just now.

The intention is always to get things more right and more clear than before. In the long run (of almost 30 years) this has usually worked out, but sometimes there are set-backs.

Concerning this particular detail, their might be some re-adjustments in the 'try' command that Jasmin Blanchette could explain.

As a general principle, 'using' does not say anything specific yet. It merely hands over certain facts as primary agument to subsequent proof method. The automated methods (simp, blast, auto, etc.) all work the same in this respect: the facts are inserted (using the "insert" method internally), and then they do their normal business on the augmented goal state.

The latter poses a logical problem, because the logic (and thus the core goal state) cannot handle schematic types as truly general types -- there is no type-quantifier in Isabelle/Pure nor Isabelle/HOL. This means, facts inserted into a goal state are instantiated 0 or at most 1 times.

This makes a technical difference for the following:

  have something
    using foo_def by simp   -- "unreliable in the presence of polymorphism"


  have something
    by (simp add: foo_def)  -- "canonical use of arbitrary rewrite rule"

  have something
    unfolding foo_def by simp

Maybe that is what you experience, but you did not show any concrete examples.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.