*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] On Recursion Induction*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Wed, 09 May 2012 09:54:48 +0200*In-reply-to*: <CAAPnxw1OQXEw7TaWg8Ft2G9q5=SEp-8FeYCGeS_Oiz2RZFn_2Q@mail.gmail.com>*References*: <CAAPnxw37MiOfcZv7xV2YR6UrhcA-_Vg2W6+k+ajdZA77L2RN8w@mail.gmail.com> <4FA8AB8A.9000705@jaist.ac.jp> <CAAPnxw1OQXEw7TaWg8Ft2G9q5=SEp-8FeYCGeS_Oiz2RZFn_2Q@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:8.0) Gecko/20120104 Icedove/8.0

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?

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.

-- Lars

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

**Re: [isabelle] On Recursion Induction***From:*Tobias Nipkow

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

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

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

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