Re: [isabelle] Destruction rules 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.

I'm afraid I must not have been making myself clear. To give an analogy: The direct effect of putting [simp] into the definition of a rule is that the Simplifier then includes that rule as one of its simprules. What is the direct effect, in that sense, of putting [dest] into the definition of a rule? (One might ask the same question, of course, about [intro] or [elim].) 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.