Re: [isabelle] Destruction rule setup
On Sun, 12 Jul 2015, Larry Paulson wrote:
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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and