Email Gateway (Aug 18 2022 at 15:09): Email Gateway (Aug 18 2022 at 15:09):From: Steve W <s.wong.731@googlemail.com>
Hi,
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?
Thanks
Steve
Email Gateway (Aug 18 2022 at 15:10):From: Makarius <makarius@sketis.net>
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
Last updated: Apr 19 2024 at 16:20 UTC