RA2010: Razonamiento por inducción sobre tipos recursivos

En la clase de hoy del curso de Razonamiento automático se han presentado las técnicas de demostración en Isabelle por inducción sobre tipos recursivos. En concreto se han estudiado los esquemas de inducción para las listas y para los árboles binarios.

Las transparencias usadas en clase son las páginas 31-34 del tema 3 (Distinción decasos e inducción). El código correspondiente se encuentra en Cap_3.thy.