Email Gateway (Aug 23 2022 at 08:21): Email Gateway (Aug 23 2022 at 08:21):From: Makarius <makarius@sketis.net>
On 03.02.20 15:47, John F. Hughes wrote:
Programming and Proving (on the second page of chapter 4) says
"A proof can either be an atomic by with a single proof method which must
finish off the statement being proved, for example auto, or it can be a
proof– qed block of multiple steps." So for instance,by auto
is apparently an allowable proof sometimes. This certainly matches my
experience.
That tutorial presents arestricted model of Isar and is not necessarily
correct in all details.
On the other hand, the Isar reference manual says (Appendix A) that a
theorem is one of several forms, which all end with a *proof, * and a
proof is...refinement ∗ proper_proof
where a "refinement" entails things like "apply" or "subgoal" or "using",
and a proper_proof is described like this:proper_proof = *proof *method? statement∗ qed method?
| done
So... is "by auto" not an Isar proof? Of is Appendix A intentionally
simplified to remove that case?Can someone explain this apparent inconsistency, please?
The isar-ref manual is the definitive source for all Isar commands
(apart from the Isabelle/ML definitions).
Appendix A.1.3 and A.1.4 provide various derived elements that are so
charecteristic for Isar. It often requires a long time to grasp the full
depth of what is going on, it is a very delicate art.
In A.1.3 you see that "by" actually has two proof method slots,
corresponding to "proof" ... "qed". That is practically important, e.g.
for "by induct auto" proofs --- please don't do "by (induct, auto)".
Makarius
Email Gateway (Aug 23 2022 at 08:27):From: "John F. Hughes" <jfh@cs.brown.edu>
Programming and Proving (on the second page of chapter 4) says
"A proof can either be an atomic by with a single proof method which must
finish off the statement being proved, for example auto, or it can be a
proof– qed block of multiple steps." So for instance,
by auto
is apparently an allowable proof sometimes. This certainly matches my
experience.
On the other hand, the Isar reference manual says (Appendix A) that a
theorem is one of several forms, which all end with a *proof, * and a
proof is...
refinement ∗ proper_proof
where a "refinement" entails things like "apply" or "subgoal" or "using",
and a proper_proof is described like this:
proper_proof = *proof *method? statement∗ qed method?
| done
So... is "by auto" not an Isar proof? Of is Appendix A intentionally
simplified to remove that case?
Can someone explain this apparent inconsistency, please?
Last updated: May 06 2024 at 12:29 UTC