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 from test.

Is this the documented (reliable on) behavior, or is this behavior just by accident?

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.


	Makarius





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