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.
lemma lem: "c > 0"
using ax1 ax2 ax3
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and