Re: [isabelle] Isabelle2013-RC2 available for testing
On Wed, 6 Feb 2013, Yannick wrote:
Note that method "rule" is dynamically rebound in HOL to include rules
stemming from the classical reasoner, too. Cf. print_claset.
I'm not sure to understand what it implies, but will learn
“print_claset”, as you mention it.
It means that the "rule" method in HOL has additional rules available: the
ones of Pure (print_rules) and the ones of the classical reasoner context
(print_claset). It is wired up in a way that you normally get what you
expect in the first place.
Before I came to Isabelle, at the time I didn't knew any prover system,
I tried to imagine such things, and in my mind, this was always coming
with this: “if it automate some proof or proof step, the user should be
able to learn what the steps was, it should be visible in some way”.
That's important, as the matter, I feel, is not only about the prover
understanding a proof, but also about the human author and human reader,
understanding it too.
Yes, this implicit use of single-step rules from the context according to
the structure of your problem, is an important aspect of Isar -- the
"Intellegible semi-automated reasoning" so to say. Fully automated
reasoning is used in different spots.
Until proper IDE feedback for "rule" steps arrives you can use rule_trace
as crude approximation:
have "A ∧ B"
proof -- trace
show A sorry
show B sorry
from `A ∧ B` obtain A and B ..-- trace
This gives you the unfiltered uninstantiated candiates that the method
guesses from the situation.
(In Isabelle2012 the trace output needs to be enabled by the check-box in
the output panel; in Isabelle2013 it is always there.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and