*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] On Recursion Induction*From*: Christian Sternagel <c-sterna at jaist.ac.jp>*Date*: Tue, 08 May 2012 14:13:46 +0900*In-reply-to*: <CAAPnxw37MiOfcZv7xV2YR6UrhcA-_Vg2W6+k+ajdZA77L2RN8w@mail.gmail.com>*References*: <CAAPnxw37MiOfcZv7xV2YR6UrhcA-_Vg2W6+k+ajdZA77L2RN8w@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:12.0) Gecko/20120430 Thunderbird/12.0.1

Dear Alfio, On 05/08/2012 01:03 PM, Alfio Martini wrote:

1) In the proof of the theorem, below in the file (and in the image), I use recursion induction together with "induct_tac" (as taught in the tutorial) and everything works as expected. However, If I try to use apply (induction b rule: NNF.induct) as suggested by the new tutorial from Tobias Nipkow (e.g., section 2.3, page 15) , I get the following error message: ill-typed instantiation: b :; 'a. Why this is so?

theorem "∀b. ∀e. valbool b e = valbool (NNF b) e"

theorem "valbool b e = valbool (NNF b) e" by (induction b rule: NNF.induct) auto which is short for theorem "valbool b e = valbool (NNF b) e" apply (induction b rule: NNF.induct) apply (auto) done

hope this helps chris

**Follow-Ups**:**Re: [isabelle] On Recursion Induction***From:*Brian Huffman

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

**References**:**[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