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
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
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
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:
using foo_def by simp -- "unreliable in the presence of polymorphism"
by (simp add: foo_def) -- "canonical use of arbitrary rewrite rule"
unfolding foo_def by simp
Maybe that is what you experience, but you did not show any concrete
This archive was generated by a fusion of
Pipermail (Mailman edition) and