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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and