*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] On Recursion Induction*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Tue, 8 May 2012 01:03:09 -0300*Sender*: alfio.martini at gmail.com

Dear Users, Attached to this e-mail is an image of small theory where I adapt an example of Paulson, from the book "ML for the Working Programmer". I have two simple doubts: 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? 2) This is perhaps for Makarius: In the image one sees that I have a total of 11 subgoals, but only 10 are printed. I would expect to reach the eleventh subgoal by scrolling down in the output window, but it does not work like that. Many thanks! PS: Using Isabelle-2012-RC1-Windows -- 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

**Attachment:
Working-Paulson-NNF-exercise.PNG**

**Attachment:
t1201201.thy**

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

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

- Previous by Date: Re: [isabelle] Proof help on Cardinality and list_all2
- Next by Date: Re: [isabelle] On Recursion Induction
- Previous by Thread: Re: [isabelle] Dealing with Cases
- 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