*To*: Christian Sternagel <c-sterna at jaist.ac.jp>, Alfio Martini <alfio.martini at acm.org>*Subject*: Re: [isabelle] On Recursion Induction*From*: Brian Huffman <huffman at in.tum.de>*Date*: Tue, 8 May 2012 07:21:22 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4FA8AB8A.9000705@jaist.ac.jp>*References*: <CAAPnxw37MiOfcZv7xV2YR6UrhcA-_Vg2W6+k+ajdZA77L2RN8w@mail.gmail.com> <4FA8AB8A.9000705@jaist.ac.jp>

On Tue, May 8, 2012 at 7:13 AM, Christian Sternagel <c-sterna at jaist.ac.jp> wrote: > 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? > > "induct"/"induction" is not the same as "induct_tac" (all methods with a > "_tac" suffix are emulations for traditional tactics (as used in apply-style > proofs) and are considered "improper" by isar-ref p. 173. One difference is > that with traditional tactics case-analysis (case_tac) and induction > (induct_tac) is possible over meta-bound variables, for "induct"/"induction" > however, you need free variables (I guess in reality the difference is more > subtle, so please Isabelle-gurus, correct me). Moreover your statement > > theorem "∀b. ∀e. valbool b e = valbool (NNF b) e" > > is a bit strange since by-default all variables are (meta-)all-quantified > after a successful proof. With proper methods you can proof the statement as > follows: > > theorem "valbool b e = valbool (NNF b) e" > by (induction b rule: NNF.induct) auto I was about to suggest the same thing. Another standard idiom is to use "fix" to introduce a new free variable, which can then be used with "induct": theorem "\<forall>b. \<forall>e. valbool b e = valbool (NNF b) e" proof (rule allI) fix b show "\<forall>e. valbool b e = valbool (NNF b) e" by (induction b rule:NNF.induct) auto qed (Note that simply "proof", which applies a default intro rule, would also work in place of "proof (rule allI)".) - Brian

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

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

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

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