Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 18 2022 at 16:53):

From: David Lazar <lazar6@illinois.edu>
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

Email Gateway (Aug 18 2022 at 16:54):

From: Lars Noschinski <noschinl@in.tum.de>
In Proof General, you can enable the "Trace Rules" which causes Isar to
list the rules it considers to do this step. Unfortunately this does not
tell you exactly which rule it chose; but in most cases it is easy to
identify which of these rules was used.

-- Lars

Last updated: Nov 21 2024 at 12:39 UTC