DAO2011: Isabelle como un lenguaje funcional
En la clase de hoy del curso de Demostración asistida por ordenador (DAO2011) se ha presentado Isabelle como un sistema de programación funcional que permite
- evaluar expresiones aritméticas y lógicas (con value),
- definir funciones no recursivas (con definition),
- definir funciones recursivas (con primrec),
- enunciar propiedades (con lemma),
- demostrar propiedades por simplificación (con simp) y
- demostrar propiedades por inducción (con induct y auto).
La teoría correspondiente a la clase es Tema_1.thy cuyo contenido se muestra a continuación
Read More “DAO2011: Isabelle como un lenguaje funcional”