RA2013: Razonamiento sobre árboles binarios con Isabelle/HOL
En la segunda parte de la clase de hoy del curso de Razonamiento automático se ha estudiado cómo definir árboles binarios en Isabelle/HOL y cómo demostrar sus propiedades.
La correspondiente teoría Isabelle/HOL 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 |
theory C12D imports Main begin text {* Ejemplo de definición de tipos recursivos: Definir un tipo de dato para los árboles binarios. *} datatype 'a arbolB = Hoja "'a" | Nodo "'a" "'a arbolB" "'a arbolB" text {* Ejemplo de definición sobre árboles binarios: Definir la función "espejo" que aplicada a un árbol devuelve su imagen especular. *} fun espejo :: "'a arbolB ⇒ 'a arbolB" where "espejo (Hoja x) = (Hoja x)" | "espejo (Nodo x i d) = (Nodo x (espejo d) (espejo i))" value "espejo (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e))" -- "= Nodo a (Hoja e) (Nodo b (Hoja d) (Hoja c))" text {* Ejemplo de demostración sobre árboles binarios: Demostrar que la función "espejo" es involutiva; es decir, para cualquier árbol a, se tiene que espejo(espejo(a)) = a. *} -- "La demostración estructurada es" lemma espejo_involutiva: fixes a :: "'b arbolB" shows "espejo (espejo a) = a" (is "?P a") proof (induct a) fix x show "?P (Hoja x)" by simp next fix x fix i assume h1: "?P i" fix d assume h2: "?P d" show "?P (Nodo x i d)" proof - have "espejo(espejo(Nodo x i d)) = espejo(Nodo x (espejo d) (espejo i))" by simp also have "… = Nodo x (espejo (espejo i)) (espejo (espejo d))" by simp also have "… = Nodo x i d" using h1 h2 by simp finally show ?thesis . qed qed text {* Comentarios sobre la demostración anterior: · (fixes a :: "'b arbolB") es una abreviatura de "sea a1 un árbol binario cuyos elementos son de tipo b". · (induct a) indica que el método de demostración es por inducción en el árbol binario a. · Se generan dos casos: 1. ⋀a. espejo (espejo (Hoja a)) = Hoja a 2. ⋀a1 a2 a3. ⟦espejo (espejo a2) = a2; espejo (espejo a3) = a3⟧ ⟹ espejo (espejo (Nodo a1 a2 a3)) = Nodo a1 a2 a3 *} -- "La demostración automática es" lemma espejo_involutiva_1: "espejo (espejo a ) = a" by (induct a) auto end |
Como tarea para la próxima clase se propuso la resolución de los ejercicios de la relación 6.