Email Gateway (Aug 18 2022 at 17:46): Email Gateway (Aug 18 2022 at 17:46):From: Makarius <makarius@sketis.net>
Concerning the old-style addXX declarations there is a subtle point here,
that I've only realized rather late in 1998/99 when introducing the
attribute-based concept.
When you write in Isar
(fast intro: thm1 thm2)
the order of declarations is from left to right, so the later one takes
precedence: thm2 before thm1.
When you write in ML
fast_tac (cs addSIs [thm1, thm2])
the declaration order is inside out (using fold_rev internally), so you
get thm1 before thm2.
This provided some potential for actual confusion 10 years ago, but now
the old addXX declarations are so rare in practice that it is much less
significant.
Makarius
Email Gateway (Aug 18 2022 at 17:53):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,
I have a list of lemmas:
lemmas test = l1 l2 ... ln
some of the lemmas are specializations of the other lemmas, i.e. l2 =
l1[where f=id, simplified], such that
l1 matches everywhere where l2 matches, but, of course, I want to use l2
where ever possible.
now I do:
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?
How is the behavior with (auto intro: test), which lemma is tried first?
Best,
Peter
Email Gateway (Aug 18 2022 at 17:53):From: Lawrence Paulson <lp15@cam.ac.uk>
It has been a very long time since I worked on this, but I believe that indeed the order is taken under strict account. Back in the days of ML, something like
blah_cs addSIs [lemma1]
was guaranteed to give priority to lemma1 over the other theorems in blah_cs. The code that keeps track of the order in which theorems are delivered is still there.
However, even more important than the order of the theorems is the number of premises; those with the fewest premises get priority.
Larry Paulson
Email Gateway (Aug 18 2022 at 17:54):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 26 2024 at 16:20 UTC