Re: [isabelle] Order of facts to be used



On Mon, 26 Apr 2010, Steve W wrote:

I was wondering how Isabelle determines the ordering of facts to be used.
For example:

lemma lem: "c > 0"
using ax1 ax2 ax3
by auto

How does Isabelle decide the ordering needed to solve the proof goal?

The Isar proof language always observes the order given in the text. This means ax1 ax2 ax3 are passed like that to the 'by' step. An Isar goal always consists of a list of facts plus a pending problem. It is up to the proof method to make as much sense out of it as possible. The "auto" method is an automated tool of the "simple method" category, which means it first pushes the facts into the goal, in the given order, and then does some kind of magic. What happens in the latter step is not so obvious, and there can be almost arbitrary prover plugins in the context, too.


	Makarius






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