Re: [isabelle] Why is conjE so complicated? [was: Re: intro rule for &&&]

On Thu, 20 Dec 2012, Holger Blasum wrote:

Also checked with some treatments of Natural Deduction (examples:
Van Dalen, Logic and Structure 1997 p. 36, Prawitz, Natural
Deduction 1965 p. 20, Gentzen 1934, p. 186) that conjunction
elimination is presented in the style of conjD1 and conjD2 and not
Isabelle's conjE (of course, disjunction elimination is a different beast).

Is there any deeper reason "conjE" appears overly complicated and/or
"conjD1" and "conjD2" are not aboard?

After some further acquaintance with the truely natural Natural Deduction of Isabelle/Pure and Isabelle/Isar you will consider conjD1/conjD2 as much less natural than they seem; and they are not elimination rules at all.

It might also help to ask the 'print_statement' command to print rules for you in structured Isar form.

Thus neither conjE nor disjE look like beasts anymore.


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