Re: [isabelle] rule Unifies With Chained Facts?
On Sun, 3 Apr 2011, Jun Inoue wrote:
I was trying "by (-, rule foo)", but now I see why that was no good.
For the record, if anyone reads this in the archives: "by - (rule foo)"
performs two separate method calls, a no-op and (rule foo), which
automatically induces a "stick assumptions into the premises" step in
between, whereas "by (-, rule foo)" performs one call to a single,
composite method which does nothing special in between the no-op and
Yes, the initial proof method of 'by' is just one big expressen, where
every participant receives the same facts. You often see this mistake in
by (method1, method2)
where it really should be
by method1 method2
by cases auto
It is also a bit inconvenient that there is no single method that has
the "insert chained facts, then apply a rule" behavior; but at least
there is an easy workaround with "-" followed by "rule".
Isar is about structure, but here it would get lost in the dark goal
state. You can use rule_tac as workaround, but then you are really
stepping outside proper Isar.
but if the authors of the Isabelle Tutorial ever see this, please
consider making a little note of this behavior of "rule" in Section 5.7
(or maybe in the "Structured Proofs in Isar/HOL" document). Clearly
pointing out the general difference between assumptions and premises
could be even better...
The manuals are not really up to date. I hope to be able to work again on
a proper Isar tutorial for structured proofs.
I did not understand what you mean by "general difference between
assumptions and premises".
Probably there is again a confusion by taking the printed goal state too
seriously -- which is very confusion indeed.
This archive was generated by a fusion of
Pipermail (Mailman edition) and