RA2010: Isabelle como un lenguaje funcional
En la clase de hoy del curso de Razonamiento automático se ha visto cómo se puede en Isabelle/HOL
- calcular con los números naturales, los números enteros y los booleanos,
- definir funciones mediante composición, condicionales, casos e inducción,
- demostrar propiedades mediante simplificación,
- definir tipos de datos recursivos,
- definir y modificar registros y
- refutar propiedades con QuickCheck.
Los apuntes usados en la clase son
GDE Error: Error al recuperar el fichero. Si es necesario, desactiva la comprobación de errores (404:Not Found)
El código correspondiente es Cap_1.thy.