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



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


On 9 Jun 2011, at 11:49, Peter Lammich wrote:

> 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?






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