Re: [isabelle] Application order of (safe) introduction rules
On Thu, 9 Jun 2011, Peter Lammich wrote:
apply (auto intro!: test)
the result of the proof seems to depend on the order of the lemmas in
the list. To me, it seems that intro! applies the *last* matching lemma
Is this the documented (reliable on) behavior, or is this behavior just
In general, declarations are passed through the many layers of the system
with some care, to preserve the order given by the user in the text. It
is up to the specific tools what to make out of that. The classical
reasoner has always been quite keen on maintaining a standard order, which
means that later rules have precedence.
And yes, this is documented behaviour. Quite a few of non-trivial
applications depend on it. Just last week I have reworked the traditional
documentation from the old ref manual, and moved the material to the
current isar-ref manual.
How is the behavior with (auto intro: test), which lemma is tried first?
In the ordering safe/unsafe rules should be exactly the same, but there
can be a difference how they get applied (also wrt. backtracking). This
touches very delicate parts of the Classical reasoner and its combination
with the Simplifier in auto.
This archive was generated by a fusion of
Pipermail (Mailman edition) and