RA2011: Isabelle como un lenguaje funcional
En la clase de hoy del curso de Razonamiento automático se ha presentado
La clase se ha basado en la siguiente teoría Isabelle
|
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 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 |
header {* Tema 6: Isabelle como un lenguaje funcional *} theory Tema_6 imports Main 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. 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. El ejemplo del lema más trivial es el siguiente *} lemma elMasTrivial: "True" by simp text {* En este capítulos se presenta el lenguaje funcional que está incluido en Isabelle. El lenguaje funcional es muy parecido al ML estándard. *} 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 n" (el sucesor de n). 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. Lema [Ejemplo de simplificación de números naturales] El siguiente del 0 es el 1. *} lemma "Suc 0 = 1" by simp text {* En Isabelle están definida la suma y el producto de números naturales: · "x+y" es la suma de x e y · "x*y" es el producto de x e y Lema [Ejemplo de suma] La suma de los números naturales 1 y 2 es el número natural 3. *} lemma "1 + 2 = (3::nat)" by simp text {* La notación del par de dos puntos se usa para asignar un tipo a un término (por ejemplo, 3::nat significa que se considera que 3 es un número natural). Lema [Ejemplo de producto] El producto de los números naturales 2 y 3 es el número natural 6. *} lemma "2 * 3 = (6::nat)" by simp text {* En Isabelle está definida la división de números naturales: · "n div m" es el cociente entero de n entre "m" · "n mod m" es el resto de dividir "n" entre "m". Lema [Ejemplo de división] La división natural de 7 entre 3 es 2. *} lemma "7 div 3 = (2::nat)" by simp text {* Lema [Ejemplo de resto] El resto de dividir 7 entre 3 es 1. *} lemma "7 mod 3 = (1::nat)" by simp text {* En Isabelle también están definidos los números enteros. El tipo de los enteros se representa por int. Lema [Ejemplo de operación con enteros] La suma de 1 y -2 es el número entero -1. *} lemma "1 + -2 = (-1::int)" by simp 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, False", · las conectivas "¬, ∧, ∨, ⟶, ↔" y · los cuantificadores "∀, ∃". El tipo de los booleanos es bool. Lema [Ejemplos de evaluaciones booleanas] · La conjunción de dos fórmulas verdaderas es verdadera. · La conjunción de un fórmula verdadera y una falsa es falsa. · La disyunción de una fórmula verdadera y una falsa es verdadera. · La disyunción de dos fórmulas falsas es falsa. · La negación de una fórmula verdadera es falsa. · Una fórmula falsa implica una fórmula verdadera. · Todo elemento es igual a sí mismo. · Existe un elemento igual a 1. *} lemma "True ∧ True = True" by simp lemma "True ∧ False = False" by simp lemma "True ∨ False = True" by simp lemma "False ∨ False = False" by simp lemma "¬ True = (False::bool)" by simp lemma "False ⟶ True" by simp lemma "∀ x. x = x" by simp lemma "∃ x. x = 1" by simp section {* Definiciones no recursivas *} text {* Definición [Ejemplo de definición no recursiva] 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 {* Lema [Ejemplo de demostración con definiciones no recursivas] La disyunción exclusiva de dos fórmulas verdaderas es falsa. Demostración. 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'. Lema [Ejemplo de entorno local] Sea x el número natural 3. Entonces "x × x = 9". *} lemma "(let x = 3::nat in x * x = 9)" by simp 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. Lema [Ejemplo de uso de pares] Sea p el par de números naturales (2,3). La suma del primer elemento de p y 1 es igual al segundo elemento de p. *} lemma "let p = (2,3)::nat × nat in fst p + 1 = snd p" by simp 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 a#l representa la lista obtenida añadiendo el elemento a al principio de la lista l. Lema [Ejemplo de construcción de listas] La lista obtenida añadiendo sucesivamente a la lista vacía los elementos 3, 2 y 1 es [1,2,3]. *} lemma "1#(2#(3#[])) = [1,2,3]" by simp text {* (hd l) es el primer elemento de la lista l. (tl l) es el resto de la lista l. Lema [Ejemplo de cálculo con listas] Sea l la lista de números naturales [1,2,3]. Entonces, el primero de l es 1 y el resto de l es [2,3]. *} lemma "let l = [1,2,3]::(nat list) in hd l = 1 ∧ tl l = [2,3]" by simp text {* (length l)es la longitud de la lista l. Lema [Ejemplo de cálculo de longitud] La longitud de la lista [1,2,3] es 3. *} lemma "length [1,2,3] = 3" by simp text {* En la sesión 38 de "HOL: The basis of Higher-Order Logic" (en http://isabelle.informatik.tu-muenchen.de/library/HOL/outline.pdf) se encuentran más definiciones y propiedades de las listas. *} section {* Registros *} text {* Un registro es una colección de campos y valores. Definición [Ejemplo de definición de registro] 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 {* Definición [Ejemplo de definición de un registro] El punto pt tiene de coordenadas 3 y 7. *} definition pt :: punto where "pt ≡ (|coordenada_x = 3, coordenada_y = 7|)" text {* Lema [Ejemplo de propiedad de registro] La coordenada x del punto pt es 3. *} lemma "coordenada_x pt = 3" by (simp add: pt_def) text {* Lema [Ejemplo de actualización de un registro] 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. *} lemma "let pt2=pt(|coordenada_x:=4|) in coordenada_x (pt2) = 4" by (simp add: pt_def) section {* Funciones anónimas *} text {* En Isabelle pueden definirse funciones anónimas. Lema [Ejemplo de uso de funciones anónimas] El valor de la función que a un número le asigna su doble aplicada a 1 es 2. *} lemma "(λ x. x + x) 1 = (2::nat)" by simp section {* Condicionales *} text {* Definición [Ejemplo con el condicional if] 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 {* Lema [Ejemplo de simplificación con el condicional if] El valor absoluto de -3 es 3. *} lemma "absoluto(-3) = 3" by (simp add:absoluto_def) text {* Definición [Ejemplo con el condicional case] 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 {* Lema [Ejemplo de simplificación con el condicional case] El número 3 es sucesor. *} lemma "es_sucesor 3" by (simp add: es_sucesor_def) section {* Tipos de datos y recursión primitiva *} text {* Definición [Ejemplo de definición de tipo de dato recursivo] 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 {* Definición [Ejemplo de definición primitiva recursiva] (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 {* Lema [Ejemplo de simplificación con tipo de dato recursivo] 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. *} lemma "conc (ConsLista 1 (ConsLista 2 Vacia)) (ConsLista 3 Vacia) = (ConsLista 1 (ConsLista 2 (ConsLista 3 Vacia)))" by simp text {* Ejercicio [Ejemplo de definición primitiva recursiva sobre los naturales] Definir una función que sume los primeros n números naturales y usarla para comprobar que la suma de los 3 primeros números naturales es 6. *} primrec suma :: "nat ⇒ nat" where "suma 0 = 0" | "suma (Suc m) = (Suc m) + suma m" lemma "suma 3 = 6" by (simp add: suma_def) value "suma 3" value "2+(3::int)" end |