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
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 |
header {* Isabelle como un lenguaje funcional *} theory Tema_1 imports Main Efficient_Nat begin section {* Introducción *} text {* Esta notas son una introducción a la demostración asistida utilizando el sistema Isabelle/HOL/Isar. La versión de Isabelle utilizada es la 2011. En este capítulos se presenta el lenguaje funcional que está incluido en Isabelle. El lenguaje funcional es muy parecido a Haskell. *} section {* Números naturales, enteros y booleanos *} text {* En Isabelle están definidos los número naturales con la sintaxis de Peano usando dos constructores: 0 (cero) y Suc (el sucesor). Los números como el 1 son abreviaturas de los correspondientes en la notación de Peano, en este caso "Suc 0". El tipo de los números naturales es nat. Por ejemplo, el siguiente del 0 es el 1. *} value "Suc 0" -- "= 1" text {* En Isabelle está definida la suma de los números naturales: (x + y) es la suma de x e y. Por ejemplo, la suma de los números naturales 1 y 2 es el número natural 3. *} value "(1::nat) + 2" -- "= 3" text {* La notación del par de dos puntos se usa para asignar un tipo a un término (por ejemplo, (1::nat) significa que se considera que 1 es un número natural). En Isabelle está definida el producto de los números naturales: (x * y) es el producto de x e y. Por ejemplo, el producto de los números naturales 2 y 3 es el número natural 6. *} value "(2::nat) * 3" -- "= 6" text {* En Isabelle está definida la división de números naturales: (n div m) es el cociente entero de x entre y. Por ejemplo, la división natural de 7 entre 3 es 2. *} value "(7::nat) div 3" -- "= 2" text {* En Isabelle está definida el resto de división de números naturales: (n mod m) es el resto de dividir n entre m. Por ejemplo, el resto de dividir 7 entre 3 es 1. *} value "(7::nat) mod 3" -- "= 1" text {* En Isabelle también están definidos los números enteros. El tipo de los enteros se representa por int. Por ejemplo, la suma de 1 y -2 es el número entero -1. *} value "(1::int) + -2" -- "= -1" text {* Los numerales están sobrecargados. Por ejemplo, el 1 puede ser un natural o un entero, dependiendo del contexto. Isabelle resuelve ambigüedades mediante inferencia de tipos. A veces, es necesario usar declaraciones de tipo para resolver la ambigüedad. En Isabelle están definidos los valores booleanos (True y False), las conectivas (¬, ∧, ∨, ⟶ y ↔) y los cuantificadores (∀ y ∃). El tipo de los booleanos es bool. *} text {* La conjunción de dos fórmulas verdaderas es verdadera. *} value "True ∧ True" -- "= True" text {* La conjunción de un fórmula verdadera y una falsa es falsa. *} value "True ∧ False" -- "= False" text {* La disyunción de una fórmula verdadera y una falsa es verdadera. *} value "True ∨ False" -- "= True" text {* La disyunción de dos fórmulas falsas es falsa. *} value "False ∨ False" -- "= False" text {* La negación de una fórmula verdadera es falsa. *} value "¬ True" -- "= False" text {* Una fórmula falsa implica una fórmula verdadera. *} value "False ⟶ True" -- "= True" text {* Un lema introduce una proposición seguida de una demostración. Isabelle dispone de varios procedimientos automáticos para generar demostraciones, uno de los cuales es el de simplificación (llamado simp). El procedimiento simp aplica un conjunto de reglas de reescritura que inicialmente contiene un gran número de reglas relativas a los objetos definidos. *} text {* Todo elemento es igual a sí mismo. *} lemma "∀x. x = x" by simp text {* Existe un elemento igual a 1. *} lemma "∃ x. x = 1" by simp section {* Definiciones no recursivas *} text {* La disyunción exclusiva de A y B se verifica si una es verdadera y la otra no lo es. *} definition xor :: "bool ⇒ bool ⇒ bool" where "xor A B ≡ (A ∧ ¬B) ∨ (¬A ∧ B)" text {* Prop.: La disyunción exclusiva de dos fórmulas verdaderas es falsa. Dem.: Por simplificación, usando la definición de la disyunción exclusiva. *} lemma "xor True True = False" by (simp add: xor_def) text {* Se añade la definición de la disyunción exlusiva al conjunto de reglas de simplificación automáticas. *} declare xor_def[simp] section {* Definiciones locales *} text {* Se puede asignar valores a variables locales mediante 'let' y usarlo en las expresiones dentro de 'in'. Por ejemplo, si x es el número natural 3, entonces "x*x=9". *} value "let x = 3::nat in x * x" -- "= 9" section {* Pares *} text {* Un par se representa escribiendo los elementos entre paréntesis y separados por coma. El tipo de los pares es el producto de los tipos. La función fst devuelve el primer elemento de un par y la snd el segundo. Por ejemplo, si p es el par de números naturales (2,3), entonces la suma del primer elemento de p y 1 es igual al segundo elemento de p. *} value "let p = (2,3)::nat × nat in fst p + 1 = snd p" section {* Listas *} text {* Una lista se representa escribiendo los elementos entre corchetes y separados por coma. La lista vacía se representa por []. Todos los elementos de una lista tienen que ser del mismo tipo. El tipo de las listas de elementos del tipo a es (a list). El término (x#xs) representa la lista obtenida añadiendo el elemento x al principio de la lista xs. Por ejemplo, la lista obtenida añadiendo sucesivamente a la lista vacía los elementos 3, 2 y 1 es [1,2,3]. *} value "1#(2#(3#[]))" -- "= [1,2,3]" text {* Funciones de descomposión de listas: · (hd xs) es el primer elemento de la lista xs. · (tl xs) es el resto de la lista xs. Por ejemplo, si xs es la lista de números naturales [1,2,3], entonces el primero de xs es 1 y el resto de xs es [2,3]. *} value "let l = [1,2,3]::(nat list) in hd l = 1 ∧ tl l = [2,3]" -- "= True" text {* (length xs) es la longitud de la lista xs. Por ejemplo, la longitud de la lista [1,2,3] es 3. *} value "length [1,2,3]" -- "= 3" text {* En la sesión 38 de "HOL: The basis of Higher-Order Logic" se encuentran más definiciones y propiedades de las listas. *} section {* Registros *} text {* Un registro es una colección de campos y valores. Por ejemplo, los puntos del plano pueden representarse mediante registros con dos campos, las coordenadas, con valores enteros. *} record punto = coordenada_x :: int coordenada_y :: int text {* Ejemplo, el punto pt tiene de coordenadas 3 y 7. *} definition pt :: punto where "pt ≡ (|coordenada_x = 3, coordenada_y = 7|)" text {* Ejemplo, la coordenada x del punto pt es 3. *} value "coordenada_x pt" -- "= 3" text {* Ejemplo, sea pt2 el punto obtenido a partir del punto pt cambiando el valor de su coordenada x por 4. Entonces la coordenada x del punto pt2 es 4. *} value "let pt2=pt(|coordenada_x:=4|) in coordenada_x (pt2)" -- "= 4" section {* Funciones anónimas *} text {* En Isabelle pueden definirse funciones anónimas. Por ejemplo, el valor de la función que a un número le asigna su doble aplicada a 1 es 2. *} value "(λx. x + x) 1::nat" -- "= 2" section {* Condicionales *} text {* El valor absoluto del entero x es x, si "x ≥ 0" y es -x en caso contrario. *} definition absoluto :: "int ⇒ int" where "absoluto x ≡ (if x ≥ 0 then x else -x)" text {* Ejemplo, el valor absoluto de -3 es 3. *} value "absoluto(-3)" -- "= 3" text {* Def.: Un número natural n es un sucesor si es de la forma (Suc m). *} definition es_sucesor :: "nat ⇒ bool" where "es_sucesor n ≡ (case n of 0 ⇒ False | Suc m ⇒ True)" text {* Ejemplo, el número 3 es sucesor. *} value "es_sucesor 3" -- "= True" section {* Tipos de datos y recursión primitiva *} text {* Una lista de elementos de tipo a es la lista Vacia o se obtiene añadiendo, con ConsLista, un elemento de tipo a a una lista de elementos de tipo a. *} datatype 'a Lista = Vacia | ConsLista 'a "'a Lista" text {* (conc xs ys) es la concatenación de las lista xs e ys. *} primrec conc :: "'a Lista ⇒ 'a Lista ⇒ 'a Lista" where "conc Vacia ys = ys" | "conc (ConsLista x xs) ys = ConsLista x (conc xs ys)" text {* Ejemplo, la concatenación de la lista formada por 1 y 2 con la lista formada por el 3 es la lista cuyos elementos son 1, 2 y 3. *} value "conc (ConsLista 1 (ConsLista 2 Vacia)) (ConsLista 3 Vacia) = (ConsLista 1 (ConsLista 2 (ConsLista 3 Vacia)))" -- "= True" text {* (suma n) es la suma de los primeros n números naturales. Por ejemplo, suma 3 = 6 *} primrec suma :: "nat ⇒ nat" where "suma 0 = 0" | "suma (Suc m) = (Suc m) + suma m" value "suma 3" -- "= 6" text {* (sumaImpares n)" es la suma de los n primeros números impares. Por ejemplo, sumaImpares 3 = 9 *} primrec sumaImpares :: "nat ⇒ nat" where "sumaImpares 0 = 0" | "sumaImpares (Suc n) = (2 * (Suc n) - 1) + sumaImpares n" value "sumaImpares 3" -- "= 9" text {* Prop.: La suma de los n primeros numeros impares es n\<^sup>2 Dem.: Por induccion en n. *} lemma "sumaImpares n = n * n" by (induct n) auto end |