Email Gateway (Aug 22 2022 at 10:51): Email Gateway (Aug 22 2022 at 10:51):From: "W. Douglas Maurer" <maurer@email.gwu.edu>
Some of the destruction rules in Isar are set up with [dest]; for example:
lemma impD [dest]: (A --> B) ==> A ==> B
lemma allD [dest]: (\forall x: B x) ==> B a
Others are not set up with [dest]; for example:
lemma not_conjD: ~(P & Q) ==> ~P | ~Q
lemma imp_to_disjD: P --> Q ==> ~P | Q
Why is this? Thanks! -WDMaurer
Email Gateway (Aug 22 2022 at 10:51):From: Larry Paulson <lp15@cam.ac.uk>
The original point of the setup was to create something that behaved like a sequent calculus. The two examples not included (not_conjD and imp_to_disjD) are redundant in this context, though for the former you’d need a detailed discussion of how negation is handled in order to see it. You could equally ask why impD is included as well as impCE, which is more general; the reason is that it handles an important special case well. It has to be admitted that there are many different ways of setting things up, and to find the best one would take a lot of experimentation. I did this in the 1990s (on largely first-order problems and set theory) but hardly at all since.
Larry Paulson
Email Gateway (Aug 22 2022 at 10:51):From: Makarius <makarius@sketis.net>
There is also a longer text by Larry from that time. Today it is section
9.4 "The Classical Reasoner" in the isar-ref manual.
Makarius
Last updated: Apr 25 2024 at 16:19 UTC