[isabelle] On Recursion Induction



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
Description: PNG image

Attachment: t1201201.thy
Description: Binary data



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.