Re: [isabelle] Application order of (safe) introduction rules



On Thu, 9 Jun 2011, Lawrence Paulson wrote:

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.

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





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