*To*: Lars Noschinski <noschinl at in.tum.de>*Subject*: Re: [isabelle] On Recursion Induction*From*: Jasmin Blanchette <jasmin.blanchette at gmail.com>*Date*: Wed, 9 May 2012 10:57:20 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4FAA22C8.4090400@in.tum.de>*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>

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. Jasmin

**Follow-Ups**:**Re: [isabelle] On Recursion Induction***From:*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

- Previous by Date: Re: [isabelle] On Recursion Induction
- 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