Re: [isabelle] On Recursion Induction



On Wed, 9 May 2012, Jasmin Blanchette wrote:

Am 09.05.2012 um 09:54 schrieb Lars Noschinski:

On 08.05.2012 21:40, Alfio Martini wrote:
I looked at section 9.2.3 in the reference manual and did not find
"induct_tac" in the list of improper proof methods. But assuming it
is, I think that the tutorial, for instance, Chapter 2, should be updated,
shouldn´t it?

This tutorial is a bit dated (but still very useful). I think Tobias Nipkow is working on a newer version.

But at the "playing level" I prefer to proceed like in a hand-made proof,
first stripping off all the quantifiers and then applying induction. In this
kind of exercise I can use this theorem further by applying rule allE and
so on. So, I assume that this kind of approach can be only done
with Isar and the fix command, as pointed out by Brian, which I usually
do.

If you really want to do step-by-step application of natural deduction rules, you might want to use the old-style rule_tac and erule_tac methods, because they allow you to instantiate meta-quantified variable (syntax is "rule_tac x=... in exI").

... both of which are definitely in the list of "harmful" proof methods of section 9.2.3.

It would seem to me that the use of tactic emulation proof methods (i.e. methods whose name end with "_tac") in one place and the warnings against their use in another place reflects more the inclinations of the respective authors of these documents than the date at which these were written.

It is probably both the inclination and the date.

Many years ago, Larry Paulson invented a very nice natural deduction rule framework called Isabelle/Pure with one main composition principle called "RS" (now visible in Isar as "rule" method or "OF" attribute). For various technical reasons he also added erule/drule/frule variants, and some means for explicit instantiations under a local quantifier erule_tac/drule_tac/frule_tac.

10 years later I came up with a natural deduction proof framework called Isabelle/Isar. It worked out just with the original Pure principles, the add-on zoo was not required. The isar-ref manual explains this Pure style of structured natural deduction in chapter 1 and 2.

Later I also re-integrated all the old stuff into the Isabelle/Isar infrastructure, so that existing material could be converted to Isar syntax in a superficial sense, without rewriting things deeply. Someone (not me) invented the name "apply style" for this guest mode of Isabelle/Isar. This is the class of "improper language elements" within proper Isar turned out quite succesful, so that its guest status is occasionally forgotten.


Concerning rule_tac in particular: it is already mostly obsolete in ML because the FOCUS combinators address the the demand for working under local quantifiers more directly. It is a re-use of Isar proof contexts for ML tactic programming.


	Makarius


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