RA2010: Funciones recursivas generales en Isabelle
En la clase de hoy del curso de Razonamiento automático se ha estudiado cómo definir funciones recursivas generales en Isabelle y cómo demostrar por inducción propiedades sobre las mismas. En concreto, se ha estudiado:
- cómo definir funciones recursivas que no son primitivas recursivas (por ejemplo, la función de Ackermann) usando fun,
- cómo obtener el esquema de inducción correpondiente a las definiciones anteriores,
- cómo demostrar propiedades de las funciones antereiores con el esquema de inducción correspondiente,
- cómo definir tipos de datos recursivos cruzados,
- cómo obtener el esquema de inducción correpondiente a las definiciones anteriores,
- cómo definr funciones con recursión cruzada,
- cómo demostrar propiedades por inducción cruzada.
En la clase se ha presentado el tema 5 (desde la página 43 a la 47).
El código correspondiente se encuentra en Cap_5.thy .