*To*: Jasmin Blanchette <jasmin.blanchette at gmail.com>*Subject*: Re: [isabelle] On Recursion Induction*From*: Makarius <makarius at sketis.net>*Date*: Wed, 9 May 2012 16:32:30 +0200 (CEST)*Cc*: Lars Noschinski <noschinl at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <A82F2BA0-ABFE-4B33-B6DD-18D2900459DA@gmail.com>*References*: <CAAPnxw37MiOfcZv7xV2YR6UrhcA-_Vg2W6+k+ajdZA77L2RN8w@mail.gmail.com> <4FA8AB8A.9000705@jaist.ac.jp> <CAAPnxw1OQXEw7TaWg8Ft2G9q5=SEp-8FeYCGeS_Oiz2RZFn_2Q@mail.gmail.com> <4FAA22C8.4090400@in.tum.de> <A82F2BA0-ABFE-4B33-B6DD-18D2900459DA@gmail.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

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 warningsagainst their use in another place reflects more the inclinations of therespective authors of these documents than the date at which these werewritten.

It is probably both the inclination and the date.

Makarius

**References**:**[isabelle] On Recursion Induction***From:*Alfio Martini

**Re: [isabelle] On Recursion Induction***From:*Christian Sternagel

**Re: [isabelle] On Recursion Induction***From:*Alfio Martini

**Re: [isabelle] On Recursion Induction***From:*Lars Noschinski

**Re: [isabelle] On Recursion Induction***From:*Jasmin Blanchette

- Previous by Date: Re: [isabelle] Isabelle2012-RC2 available for testing
- Next by Date: Re: [isabelle] Isabelle2012-RC2 available for testing
- Previous by Thread: Re: [isabelle] On Recursion Induction
- Next by Thread: Re: [isabelle] On Recursion Induction
- Cl-isabelle-users May 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list