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

Dear Brian, Thanks for your reply! >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 That is the way I go about it when using Isar. So the question that remains is: how to prove the theorem above (with all the (two) quantifiers) using the procedural style (and without using induct_tac)? All the Best! On Tue, May 8, 2012 at 2:21 AM, Brian Huffman <huffman at in.tum.de> wrote: > 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 > -- Alfio Ricardo Martini PhD in Computer Science (TU Berlin) Associate Professor at Faculty of Informatics (PUCRS) Coordenador do Curso de Ciência da Computação Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática 90619-900 -Porto Alegre - RS - Brasil

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

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

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

- 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