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 (rule foo).

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 the sources:

  by (method1, method2)

where it really should be

  by method1 method2

e.g.

  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.


	Makarius





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