Re: [isabelle] Destruction rule setup



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


> On 11 Jul 2015, at 22:09, W. Douglas Maurer <maurer at email.gwu.edu> wrote:
> 
> 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
> 
> -- 
> Prof. W. Douglas Maurer                Washington, DC 20052, USA
> Department of Computer Science         Tel. (1-202)994-5921
> The George Washington University       Fax  (1-202)994-4875
> 





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