[isabelle] Isar: making implicit intro/elim rules explicit



The paper "A Tutorial Introduction to Structured Isar Proofs" has the
following simple example:

lemma "A --> A"
proof (rule impI)
  assume a: "A"
  show "A" by (rule a)
qed

The proof can be reduced to:

lemma "A --> A"
proof
  assume a: "A"
  show "A" by (rule a)
qed

by making the proof method "(rule impI)" implicit.  As stated in the
paper, the "proof" command is short for "proof (rule elim-rules
intro-rules)", where "elim-rules" and "intro-rules" are selected by
Isar automatically based on the context.  Is there a way to see Isar's
choices for "elim-rules" and "intro-rules" (and also "." and "..")?
In other words, is there a way to turn a proof that uses implicit
proof methods into a proof where all the proof methods are explicit?

I can see how implicit proof methods make proofs easier to read and
write, but seeing these things explicitly would be very helpful in
learning Isar.

Thanks,
David





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