Re: [isabelle] rule Unifies With Chained Facts?




On 03/04/11 09:28, Jun Inoue wrote:
Hi Brian, thanks for the tip!  I was trying "by (-, rule foo)", but now
I see why that was no good.  :)
[...]
It is a bit confusing how "rule" treats chained facts in a special
way, when nearly all other methods start by adding any chained facts
into the goal as premises before continuing with their normal
behavior. 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".
[...]
PS.  Not to be too nosy here, 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...

I agree. At the very least, this is non-obvious. I still get caught by this occasionally. I've trained myself that rule/erule/drule and assumption require the use of - first, while auto and (clar)simp do not. I still remain surprised whenever I have to replace "by blast" with "by - blast". As for fastsimp, force and metis... I just don't remember.

While I suppose I could just go around using auto and metis everywhere, I don't think that's necessarily a good idea, as it miscommunicates to the reader/maintainer how involved the proof step is. I will use assumption when that's all that's needed, blast when there's no simplification needed, and prefer simp over auto.

Anyway, my proposal would be to add an implicit "-" to blast and any official tactic that can finish a proof, and document in the tutorial and reference the fact that rule/erule/drule (and whatever else) don't do this, like Jun suggested.

Sincerely,

Rafal Kolanski.





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