Diferencia entre revisiones de «Razonamiento sobre árboles y bosques»
De Lógica matemática y fundamentos (2018-19)
m |
|||
(No se muestran 3 ediciones intermedias del mismo usuario) | |||
Línea 1: | Línea 1: | ||
<source lang="isabelle"> | <source lang="isabelle"> | ||
− | chapter | + | chapter ‹Tema 8: Razonamiento sobre árboles› |
theory T8_Razonamiento_sobre_arboles | theory T8_Razonamiento_sobre_arboles | ||
− | imports Main | + | imports Main |
begin | begin | ||
− | text | + | text ‹En este tema se estudia razonamiento sobre otras estructuras |
− | |||
recursivas como árboles binarios, árboles generales y bosques. | recursivas como árboles binarios, árboles generales y bosques. | ||
También se muestra cómo definir tipos de datos por recursión cruzada y | También se muestra cómo definir tipos de datos por recursión cruzada y | ||
− | la demostración de sus propiedades por inducción. | + | la demostración de sus propiedades por inducción.› |
− | |||
− | section | + | section ‹Razonamiento sobre árboles binarios› |
− | text | + | text ‹Ejemplo de definición de tipos recursivos: |
− | + | Definir un tipo de dato para los árboles binarios.› | |
− | Definir un tipo de dato para los árboles binarios. | ||
− | |||
datatype 'a arbolB = Hoja "'a" | datatype 'a arbolB = Hoja "'a" | ||
| Nodo "'a" "'a arbolB" "'a arbolB" | | Nodo "'a" "'a arbolB" "'a arbolB" | ||
− | text | + | text ‹Regla de inducción correspondiente a los árboles binarios: |
− | + | La regla de inducción sobre árboles binarios es arbol.induct: | |
+ | ⟦ ⋀x. P (Hoja x); | ||
+ | ⋀x i d. ⟦P i; P d⟧ ⟹ P (Nodo x i d)⟧ | ||
+ | ⟹ P a | ||
+ | › | ||
+ | |||
+ | thm arbolB.induct | ||
+ | |||
+ | text ‹Ejemplo de definición sobre árboles binarios: | ||
Definir la función "espejo" que aplicada a un árbol devuelve su imagen | Definir la función "espejo" que aplicada a un árbol devuelve su imagen | ||
− | especular. | + | especular.› |
− | |||
fun espejo :: "'a arbolB ⇒ 'a arbolB" where | fun espejo :: "'a arbolB ⇒ 'a arbolB" where | ||
− | "espejo (Hoja x) = | + | "espejo (Hoja x) = Hoja x" |
− | | "espejo (Nodo x i d) = | + | | "espejo (Nodo x i d) = Nodo x (espejo d) (espejo i)" |
value "espejo (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e)) = | value "espejo (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e)) = | ||
Nodo a (Hoja e) (Nodo b (Hoja d) (Hoja c))" | Nodo a (Hoja e) (Nodo b (Hoja d) (Hoja c))" | ||
− | text | + | text ‹Ejemplo de demostración sobre árboles binarios: |
− | |||
Demostrar que la función "espejo" es involutiva; es decir, para | Demostrar que la función "espejo" es involutiva; es decir, para | ||
cualquier árbol a, se tiene que | cualquier árbol a, se tiene que | ||
− | espejo (espejo a) = a. | + | espejo (espejo a) = a.› |
− | |||
− | ― ‹La demostración | + | ― ‹La demostración declarativa es› |
− | lemma | + | lemma |
fixes a :: "'b arbolB" | fixes a :: "'b arbolB" | ||
shows "espejo (espejo a) = a" (is "?P a") | shows "espejo (espejo a) = a" (is "?P a") | ||
proof (induct a) | proof (induct a) | ||
fix x | fix x | ||
− | show "?P (Hoja x)" by simp | + | show "?P (Hoja x)" by simp |
next | next | ||
fix x | fix x | ||
Línea 61: | Línea 62: | ||
also have "… = Nodo x (espejo (espejo i)) (espejo (espejo d))" | also have "… = Nodo x (espejo (espejo i)) (espejo (espejo d))" | ||
by simp | by simp | ||
− | also have "… = Nodo x i d" using h1 h2 by simp | + | also have "… = Nodo x i d" |
+ | using h1 h2 by simp | ||
finally show ?thesis . | finally show ?thesis . | ||
− | qed | + | qed |
+ | qed | ||
+ | |||
+ | ― ‹La demostración declarativa detallada es› | ||
+ | lemma | ||
+ | fixes a :: "'b arbolB" | ||
+ | shows "espejo (espejo a) = a" (is "?P a") | ||
+ | proof (induct a) | ||
+ | fix x | ||
+ | show "?P (Hoja x)" | ||
+ | by (simp only: espejo.simps(1)) | ||
+ | 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 only: espejo.simps(2)) | ||
+ | also have "… = Nodo x (espejo (espejo i)) (espejo (espejo d))" | ||
+ | by (simp only: espejo.simps(2)) | ||
+ | also have "… = Nodo x i d" | ||
+ | by (simp only: h1 h2) | ||
+ | finally show ?thesis | ||
+ | by this | ||
+ | qed | ||
qed | qed | ||
− | text | + | text ‹Comentarios sobre la demostración anterior: |
− | |||
· (fixes a :: "'b arbolB") es una abreviatura de "sea a1 un árbol binario | · (fixes a :: "'b arbolB") es una abreviatura de "sea a1 un árbol binario | ||
cuyos elementos son de tipo b". | cuyos elementos son de tipo b". | ||
Línea 76: | Línea 103: | ||
2. ⋀a1 a2 a3. ⟦espejo (espejo a2) = a2; | 2. ⋀a1 a2 a3. ⟦espejo (espejo a2) = a2; | ||
espejo (espejo a3) = a3⟧ | espejo (espejo a3) = a3⟧ | ||
− | ⟹ espejo (espejo (Nodo a1 a2 a3)) = Nodo a1 a2 | + | ⟹ espejo (espejo (Nodo a1 a2 a3)) = Nodo a1 a2 a3› |
− | + | ||
+ | ― ‹La demostración aplicativa es› | ||
+ | lemma | ||
+ | "espejo (espejo a) = a" | ||
+ | apply (induct a) | ||
+ | apply simp | ||
+ | apply simp | ||
+ | done | ||
+ | |||
+ | ― ‹La demostración aplicativa detallada es› | ||
+ | lemma | ||
+ | "espejo (espejo a) = a" | ||
+ | apply (induct a) | ||
+ | apply (simp only: espejo.simps(1)) | ||
+ | apply (simp only: espejo.simps(2)) | ||
+ | done | ||
― ‹La demostración automática es› | ― ‹La demostración automática es› | ||
− | lemma | + | lemma |
− | "espejo (espejo a ) = a" | + | "espejo (espejo a) = a" |
− | by (induct a) | + | by (induct a) simp+ |
− | + | ― ‹La demostración automática detallada es› | |
− | + | lemma | |
+ | "espejo (espejo a) = a" | ||
+ | by (induct a) (simp only: espejo.simps)+ | ||
+ | |||
+ | text ‹Ejemplo. [Aplanamiento de árboles] | ||
Definir la función "aplana" que aplane los árboles recorriéndolos en | Definir la función "aplana" que aplane los árboles recorriéndolos en | ||
− | orden infijo. | + | orden infijo.› |
− | |||
fun aplana :: "'a arbolB ⇒ 'a list" where | fun aplana :: "'a arbolB ⇒ 'a list" where | ||
"aplana (Hoja x) = [x]" | "aplana (Hoja x) = [x]" | ||
− | | "aplana (Nodo x i d) = | + | | "aplana (Nodo x i d) = aplana i @ [x] @ aplana d" |
value "aplana (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e)) = | value "aplana (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e)) = | ||
[c, b, d, a, e]" | [c, b, d, a, e]" | ||
− | text | + | text ‹Ejemplo. [Aplanamiento de la imagen especular] Demostrar que |
− | + | aplana (espejo a) = rev (aplana a)› | |
− | aplana (espejo a) = rev (aplana a) | ||
− | |||
− | ― ‹La demostración | + | ― ‹La demostración declarativa es› |
lemma | lemma | ||
fixes a :: "'b arbolB" | fixes a :: "'b arbolB" | ||
Línea 108: | Línea 151: | ||
proof (induct a) | proof (induct a) | ||
fix x | fix x | ||
− | show "?P (Hoja x)" by simp | + | show "?P (Hoja x)" |
+ | by simp | ||
next | next | ||
fix x | fix x | ||
Línea 116: | Línea 160: | ||
proof - | proof - | ||
have "aplana (espejo (Nodo x i d)) = | have "aplana (espejo (Nodo x i d)) = | ||
− | aplana (Nodo x (espejo d) (espejo i))" by simp | + | aplana (Nodo x (espejo d) (espejo i))" |
+ | by simp | ||
also have "… = (aplana (espejo d)) @ [x] @ (aplana (espejo i))" | also have "… = (aplana (espejo d)) @ [x] @ (aplana (espejo i))" | ||
by simp | by simp | ||
also have "… = (rev (aplana d)) @ [x] @ (rev (aplana i))" | also have "… = (rev (aplana d)) @ [x] @ (rev (aplana i))" | ||
using h1 h2 by simp | using h1 h2 by simp | ||
− | also have "… = rev ((aplana i) @ [x] @ (aplana d))" by simp | + | also have "… = rev ((aplana i) @ [x] @ (aplana d))" |
− | also have "… = rev (aplana (Nodo x i d))" by simp | + | by simp |
+ | also have "… = rev (aplana (Nodo x i d))" | ||
+ | by simp | ||
finally show ?thesis . | finally show ?thesis . | ||
− | + | qed | |
+ | qed | ||
+ | |||
+ | ― ‹Lema auxiliar para la demostración declarativa detallada› | ||
+ | lemma rev_unit: "rev [x] = [x]" | ||
+ | proof - | ||
+ | have "rev [x] = rev [] @ [x]" | ||
+ | by (simp only: rev.simps(2)) | ||
+ | also have "… = [] @ [x]" | ||
+ | by (simp only: rev.simps(1)) | ||
+ | also have "… = [x]" | ||
+ | by (simp only: append.simps(1)) | ||
+ | finally show ?thesis | ||
+ | by this | ||
+ | qed | ||
+ | |||
+ | ― ‹La demostración estructurada y detallada es› | ||
+ | lemma | ||
+ | fixes a :: "'b arbolB" | ||
+ | shows "aplana (espejo a) = rev (aplana a)" (is "?P a") | ||
+ | proof (induct a) | ||
+ | fix x :: 'b | ||
+ | have "aplana (espejo (Hoja x)) = aplana (Hoja x)" | ||
+ | by (simp only: espejo.simps(1)) | ||
+ | also have "… = [x]" | ||
+ | by (simp only: aplana.simps(1)) | ||
+ | also have "… = rev [x]" | ||
+ | by (simp only: rev_unit) | ||
+ | also have "… = rev (aplana (Hoja x))" | ||
+ | by (simp only: aplana.simps(1)) | ||
+ | finally show "?P (Hoja x)" | ||
+ | by this | ||
+ | next | ||
+ | fix x :: 'b | ||
+ | fix i assume h1: "?P i" | ||
+ | fix d assume h2: "?P d" | ||
+ | show "?P (Nodo x i d)" | ||
+ | proof - | ||
+ | have "aplana (espejo (Nodo x i d)) = | ||
+ | aplana (Nodo x (espejo d) (espejo i))" | ||
+ | by (simp only: espejo.simps(2)) | ||
+ | also have "… = (aplana (espejo d)) @ [x] @ (aplana (espejo i))" | ||
+ | by (simp only: aplana.simps(2)) | ||
+ | also have "… = (rev (aplana d)) @ [x] @ (rev (aplana i))" | ||
+ | by (simp only: h1 h2) | ||
+ | also have "… = rev ((aplana i) @ [x] @ (aplana d))" | ||
+ | by (simp only: rev_append rev_unit append_assoc) | ||
+ | also have "… = rev (aplana (Nodo x i d))" | ||
+ | by (simp only: aplana.simps(2)) | ||
+ | finally show ?thesis | ||
+ | by this | ||
+ | qed | ||
qed | qed | ||
+ | |||
+ | ― ‹La demostración aplicativa es› | ||
+ | lemma "aplana (espejo a) = rev (aplana a)" | ||
+ | apply (induct a) | ||
+ | apply simp | ||
+ | apply simp | ||
+ | done | ||
+ | |||
+ | ― ‹La demostración aplicativa detallada es› | ||
+ | lemma "aplana (espejo a) = rev (aplana a)" | ||
+ | apply (induct a) | ||
+ | apply (simp only: espejo.simps(1) aplana.simps(1)) | ||
+ | apply (simp only: rev_unit) | ||
+ | apply (simp only: espejo.simps(2) aplana.simps(2)) | ||
+ | apply (simp only: rev_append) | ||
+ | apply (simp only: rev_unit) | ||
+ | apply (simp only: append_assoc) | ||
+ | done | ||
+ | |||
+ | ― ‹La demostración aplicativa detallada compacta es› | ||
+ | lemma "aplana (espejo a) = rev (aplana a)" | ||
+ | apply (induct a) | ||
+ | apply (simp only: | ||
+ | espejo.simps(1) | ||
+ | aplana.simps(1) | ||
+ | rev_unit | ||
+ | espejo.simps(2) | ||
+ | aplana.simps(2) | ||
+ | rev_append | ||
+ | append_assoc)+ | ||
+ | done | ||
+ | |||
+ | ― ‹La demostración aplicativa detallada más compacta es› | ||
+ | lemma "aplana (espejo a) = rev (aplana a)" | ||
+ | apply (induct a) | ||
+ | apply (simp only: | ||
+ | espejo.simps | ||
+ | aplana.simps | ||
+ | rev_unit | ||
+ | rev_append | ||
+ | append_assoc)+ | ||
+ | done | ||
― ‹La demostración automática es› | ― ‹La demostración automática es› | ||
lemma "aplana (espejo a) = rev (aplana a)" | lemma "aplana (espejo a) = rev (aplana a)" | ||
− | by (induct a) | + | by (induct a) simp_all |
− | + | ― ‹La demostración automática detallada es› | |
+ | lemma "aplana (espejo a) = rev (aplana a)" | ||
+ | by (induct a) | ||
+ | (simp only: | ||
+ | espejo.simps | ||
+ | aplana.simps | ||
+ | rev_unit | ||
+ | rev_append | ||
+ | append_assoc)+ | ||
− | text | + | section ‹Árboles y bosques. Recursión mutua e inducción› |
− | + | ||
+ | text ‹Nota. [Ejemplo de definición de tipos mediante recursión cruzada] | ||
· Un árbol de tipo a es una hoja o un nodo de tipo a junto con un | · Un árbol de tipo a es una hoja o un nodo de tipo a junto con un | ||
bosque de tipo a. | bosque de tipo a. | ||
· Un bosque de tipo a es el boque vacío o un bosque contruido añadiendo | · Un bosque de tipo a es el boque vacío o un bosque contruido añadiendo | ||
− | un árbol de tipo a a un bosque de tipo a. | + | un árbol de tipo a a un bosque de tipo a.› |
− | |||
− | datatype 'a arbol = | + | datatype 'a arbol = Nodo "'a" "'a bosque" |
and 'a bosque = Vacio | ConsB "'a arbol" "'a bosque" | and 'a bosque = Vacio | ConsB "'a arbol" "'a bosque" | ||
− | text | + | text ‹Regla de inducción correspondiente a la recursión cruzada: |
− | |||
La regla de inducción sobre árboles y bosques es arbol_bosque.induct: | La regla de inducción sobre árboles y bosques es arbol_bosque.induct: | ||
− | + | ⟦⋀x b. P2 b ⟹ P1 (Nodo x b); | |
− | |||
P2 Vacio; | P2 Vacio; | ||
⋀a b. ⟦P1 a; P2 b⟧ ⟹ P2 (ConsB a b)⟧ | ⋀a b. ⟦P1 a; P2 b⟧ ⟹ P2 (ConsB a b)⟧ | ||
− | ⟹ P1 a ∧ P2 | + | ⟹ P1 a ∧ P2 b› |
− | |||
− | text | + | thm arbol_bosque.induct |
− | + | ||
+ | text ‹Ejemplos de definición por recursión cruzada: | ||
· aplana_arbol a) es la lista obtenida aplanando el árbol a. | · aplana_arbol a) es la lista obtenida aplanando el árbol a. | ||
· (aplana_bosque b) es la lista obtenida aplanando el bosque b. | · (aplana_bosque b) es la lista obtenida aplanando el bosque b. | ||
Línea 161: | Línea 307: | ||
todos los nodos del árbol a. | todos los nodos del árbol a. | ||
· (map_bosque f b) es el bosque obtenido aplicando la función f a | · (map_bosque f b) es el bosque obtenido aplicando la función f a | ||
− | todos los nodos del bosque b. | + | todos los nodos del bosque b. › |
− | |||
fun aplana_arbol :: "'a arbol ⇒ 'a list" and | fun aplana_arbol :: "'a arbol ⇒ 'a list" and | ||
aplana_bosque :: "'a bosque ⇒ 'a list" where | aplana_bosque :: "'a bosque ⇒ 'a list" where | ||
− | + | "aplana_arbol (Nodo x b) = x # (aplana_bosque b)" | |
− | |||
| "aplana_bosque Vacio = []" | | "aplana_bosque Vacio = []" | ||
| "aplana_bosque (ConsB a b) = (aplana_arbol a) @ (aplana_bosque b)" | | "aplana_bosque (ConsB a b) = (aplana_arbol a) @ (aplana_bosque b)" | ||
Línea 173: | Línea 317: | ||
fun map_arbol :: "('a ⇒ 'b) ⇒ 'a arbol ⇒ 'b arbol" and | fun map_arbol :: "('a ⇒ 'b) ⇒ 'a arbol ⇒ 'b arbol" and | ||
map_bosque :: "('a ⇒ 'b) ⇒ 'a bosque ⇒ 'b bosque" where | map_bosque :: "('a ⇒ 'b) ⇒ 'a bosque ⇒ 'b bosque" where | ||
− | + | "map_arbol f (Nodo x b) = Nodo (f x) (map_bosque f b)" | |
− | |||
| "map_bosque f Vacio = Vacio" | | "map_bosque f Vacio = Vacio" | ||
| "map_bosque f (ConsB a b) = ConsB (map_arbol f a) (map_bosque f b)" | | "map_bosque f (ConsB a b) = ConsB (map_arbol f a) (map_bosque f b)" | ||
− | text | + | text ‹Ejemplo de demostración por inducción cruzada: |
− | |||
Demostrar que: | Demostrar que: | ||
· aplana_arbol (map_arbol f a) = map f (aplana_arbol a) | · aplana_arbol (map_arbol f a) = map f (aplana_arbol a) | ||
− | · aplana_bosque (map_bosque f b) = map f (aplana_bosque b) | + | · aplana_bosque (map_bosque f b) = map f (aplana_bosque b)› |
− | |||
− | declare [[names_short]] | + | declare [[names_short]] |
− | ― ‹La demostración | + | ― ‹La demostración declarativa es› |
lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a) | lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a) | ||
∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" | ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" | ||
proof (induct_tac a and b) | proof (induct_tac a and b) | ||
− | |||
− | |||
− | |||
fix x b | fix x b | ||
assume HI: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" | assume HI: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" | ||
have "aplana_arbol (map_arbol f (Nodo x b)) = | have "aplana_arbol (map_arbol f (Nodo x b)) = | ||
− | aplana_arbol (Nodo (f x) (map_bosque f b))" by simp | + | aplana_arbol (Nodo (f x) (map_bosque f b))" |
− | also have "… = (f x) # (aplana_bosque (map_bosque f b))" by simp | + | by simp |
− | also have "… = (f x) # (map f (aplana_bosque b))" using HI by simp | + | also have "… = (f x) # (aplana_bosque (map_bosque f b))" |
− | also have "… = map f (aplana_arbol (Nodo x b))" by simp | + | by simp |
− | finally show "aplana_arbol (map_arbol f (Nodo x b)) | + | also have "… = (f x) # (map f (aplana_bosque b))" |
− | + | using HI by simp | |
+ | also have "… = map f (aplana_arbol (Nodo x b))" | ||
+ | by simp | ||
+ | finally show "aplana_arbol (map_arbol f (Nodo x b)) = | ||
+ | map f (aplana_arbol (Nodo x b))" | ||
+ | by this | ||
next | next | ||
show "aplana_bosque (map_bosque f Vacio) = map f (aplana_bosque Vacio)" | show "aplana_bosque (map_bosque f Vacio) = map f (aplana_bosque Vacio)" | ||
Línea 218: | Línea 361: | ||
using HI1 HI2 by simp | using HI1 HI2 by simp | ||
also have "… = map f (aplana_bosque (ConsB a b))" by simp | also have "… = map f (aplana_bosque (ConsB a b))" by simp | ||
− | finally show "aplana_bosque (map_bosque f (ConsB a b)) | + | finally show "aplana_bosque (map_bosque f (ConsB a b)) = |
− | = map f (aplana_bosque (ConsB a b))" by simp | + | map f (aplana_bosque (ConsB a b))" |
+ | by this | ||
+ | qed | ||
+ | |||
+ | ― ‹La demostración declarativa detallada es› | ||
+ | lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a) | ||
+ | ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" | ||
+ | proof (induct_tac a and b) | ||
+ | fix x b | ||
+ | assume HI: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" | ||
+ | have "aplana_arbol (map_arbol f (Nodo x b)) = | ||
+ | aplana_arbol (Nodo (f x) (map_bosque f b))" | ||
+ | by (simp only: map_arbol.simps(1)) | ||
+ | also have "… = (f x) # (aplana_bosque (map_bosque f b))" | ||
+ | by (simp only: aplana_arbol.simps(1)) | ||
+ | also have "… = (f x) # (map f (aplana_bosque b))" | ||
+ | by (simp only: HI) | ||
+ | also have "… = map f (aplana_arbol (Nodo x b))" | ||
+ | by (simp only: list.map aplana_arbol.simps(1)) | ||
+ | finally show "aplana_arbol (map_arbol f (Nodo x b)) = | ||
+ | map f (aplana_arbol (Nodo x b))" | ||
+ | by this | ||
+ | next | ||
+ | show "aplana_bosque (map_bosque f Vacio) = map f (aplana_bosque Vacio)" | ||
+ | by (simp only: aplana_bosque.simps(1) | ||
+ | map_bosque.simps(1) | ||
+ | list.map) | ||
+ | next | ||
+ | fix a b | ||
+ | assume HI1: "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)" | ||
+ | and HI2: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" | ||
+ | have "aplana_bosque (map_bosque f (ConsB a b)) = | ||
+ | aplana_bosque (ConsB (map_arbol f a) (map_bosque f b))" | ||
+ | by (simp only: map_bosque.simps(2)) | ||
+ | also have "… = aplana_arbol (map_arbol f a) @ | ||
+ | aplana_bosque (map_bosque f b)" | ||
+ | by (simp only: aplana_bosque.simps(2)) | ||
+ | also have "… = (map f (aplana_arbol a)) @ (map f (aplana_bosque b))" | ||
+ | by (simp only: HI1 HI2) | ||
+ | also have "… = map f (aplana_arbol a @ aplana_bosque b)" | ||
+ | by (simp only: map_append) | ||
+ | also have "… = map f (aplana_bosque (ConsB a b))" | ||
+ | by (simp only: aplana_bosque.simps(2)) | ||
+ | finally show "aplana_bosque (map_bosque f (ConsB a b)) = | ||
+ | map f (aplana_bosque (ConsB a b))" | ||
+ | by this | ||
qed | qed | ||
− | text | + | text ‹Comentarios sobre la demostración anterior: |
− | |||
· (induct_tac a and b) indica que el método de demostración es por | · (induct_tac a and b) indica que el método de demostración es por | ||
inducción cruzada sobre a y b. | inducción cruzada sobre a y b. | ||
− | · Se generan | + | · Se generan 3 casos: |
− | 1 | + | 1. ⋀a bosque. |
− | |||
aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque) ⟹ | aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque) ⟹ | ||
aplana_arbol (map_arbol (arbol.Nodo a bosque) h) = | aplana_arbol (map_arbol (arbol.Nodo a bosque) h) = | ||
map h (aplana_arbol (arbol.Nodo a bosque)) | map h (aplana_arbol (arbol.Nodo a bosque)) | ||
− | + | 2. aplana_bosque (map_bosque Vacio h) = map h (aplana_bosque Vacio) | |
− | + | 3. ⋀arbol bosque. | |
⟦aplana_arbol (map_arbol arbol h) = map h (aplana_arbol arbol); | ⟦aplana_arbol (map_arbol arbol h) = map h (aplana_arbol arbol); | ||
aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque)⟧ | aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque)⟧ | ||
⟹ aplana_bosque (map_bosque (ConsB arbol bosque) h) = | ⟹ aplana_bosque (map_bosque (ConsB arbol bosque) h) = | ||
− | map h (aplana_bosque (ConsB arbol bosque)) | + | map h (aplana_bosque (ConsB arbol bosque))› |
− | + | ||
+ | ― ‹La demostración aplicativa es› | ||
+ | lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a) | ||
+ | ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" | ||
+ | apply (induct_tac a and b) | ||
+ | apply simp | ||
+ | apply simp | ||
+ | apply simp | ||
+ | done | ||
+ | |||
+ | ― ‹La demostración aplicativa detallada es› | ||
+ | lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a) | ||
+ | ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" | ||
+ | apply (induct_tac a and b) | ||
+ | apply (simp only: map_arbol.simps aplana_arbol.simps) | ||
+ | apply (simp only: list.map(2)) | ||
+ | apply (simp only: map_bosque.simps(1) aplana_bosque.simps(1)) | ||
+ | apply (simp only: list.map(1)) | ||
+ | apply (simp only: map_bosque.simps(2) aplana_bosque.simps(2)) | ||
+ | apply (simp only: map_append) | ||
+ | done | ||
+ | |||
+ | ― ‹La demostración aplicativa detallada compacta es› | ||
+ | lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a) | ||
+ | ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" | ||
+ | apply (induct_tac a and b) | ||
+ | apply (simp only: | ||
+ | map_arbol.simps | ||
+ | aplana_arbol.simps | ||
+ | list.map(2) | ||
+ | map_bosque.simps(1) | ||
+ | aplana_bosque.simps(1) | ||
+ | list.map(1) | ||
+ | map_bosque.simps(2) | ||
+ | aplana_bosque.simps(2) | ||
+ | map_append)+ | ||
+ | done | ||
+ | |||
+ | ― ‹La demostración aplicativa detallada más compacta es› | ||
+ | lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a) | ||
+ | ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" | ||
+ | apply (induct_tac a and b) | ||
+ | apply (simp only: | ||
+ | map_arbol.simps | ||
+ | map_bosque.simps | ||
+ | aplana_arbol.simps | ||
+ | aplana_bosque.simps | ||
+ | list.map | ||
+ | map_append)+ | ||
+ | done | ||
― ‹La demostración automática es› | ― ‹La demostración automática es› | ||
lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a) | lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a) | ||
∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" | ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" | ||
− | by (induct_tac a and b) | + | by (induct_tac a and b) simp_all |
+ | ― ‹La demostración automática detallada es› | ||
+ | lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a) | ||
+ | ∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)" | ||
+ | by (induct_tac a and b) | ||
+ | (simp only: | ||
+ | map_arbol.simps | ||
+ | map_bosque.simps | ||
+ | aplana_arbol.simps | ||
+ | aplana_bosque.simps | ||
+ | list.map | ||
+ | map_append)+ | ||
end | end | ||
</source> | </source> |
Revisión actual del 08:02 14 may 2020
chapter ‹Tema 8: Razonamiento sobre árboles›
theory T8_Razonamiento_sobre_arboles
imports Main
begin
text ‹En este tema se estudia razonamiento sobre otras estructuras
recursivas como árboles binarios, árboles generales y bosques.
También se muestra cómo definir tipos de datos por recursión cruzada y
la demostración de sus propiedades por inducción.›
section ‹Razonamiento sobre árboles binarios›
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 ‹Regla de inducción correspondiente a los árboles binarios:
La regla de inducción sobre árboles binarios es arbol.induct:
⟦ ⋀x. P (Hoja x);
⋀x i d. ⟦P i; P d⟧ ⟹ P (Nodo x i d)⟧
⟹ P a
›
thm arbolB.induct
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 declarativa es›
lemma
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
― ‹La demostración declarativa detallada es›
lemma
fixes a :: "'b arbolB"
shows "espejo (espejo a) = a" (is "?P a")
proof (induct a)
fix x
show "?P (Hoja x)"
by (simp only: espejo.simps(1))
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 only: espejo.simps(2))
also have "… = Nodo x (espejo (espejo i)) (espejo (espejo d))"
by (simp only: espejo.simps(2))
also have "… = Nodo x i d"
by (simp only: h1 h2)
finally show ?thesis
by this
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 aplicativa es›
lemma
"espejo (espejo a) = a"
apply (induct a)
apply simp
apply simp
done
― ‹La demostración aplicativa detallada es›
lemma
"espejo (espejo a) = a"
apply (induct a)
apply (simp only: espejo.simps(1))
apply (simp only: espejo.simps(2))
done
― ‹La demostración automática es›
lemma
"espejo (espejo a) = a"
by (induct a) simp+
― ‹La demostración automática detallada es›
lemma
"espejo (espejo a) = a"
by (induct a) (simp only: espejo.simps)+
text ‹Ejemplo. [Aplanamiento de árboles]
Definir la función "aplana" que aplane los árboles recorriéndolos en
orden infijo.›
fun aplana :: "'a arbolB ⇒ 'a list" where
"aplana (Hoja x) = [x]"
| "aplana (Nodo x i d) = aplana i @ [x] @ aplana d"
value "aplana (Nodo a (Nodo b (Hoja c) (Hoja d)) (Hoja e)) =
[c, b, d, a, e]"
text ‹Ejemplo. [Aplanamiento de la imagen especular] Demostrar que
aplana (espejo a) = rev (aplana a)›
― ‹La demostración declarativa es›
lemma
fixes a :: "'b arbolB"
shows "aplana (espejo a) = rev (aplana 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 "aplana (espejo (Nodo x i d)) =
aplana (Nodo x (espejo d) (espejo i))"
by simp
also have "… = (aplana (espejo d)) @ [x] @ (aplana (espejo i))"
by simp
also have "… = (rev (aplana d)) @ [x] @ (rev (aplana i))"
using h1 h2 by simp
also have "… = rev ((aplana i) @ [x] @ (aplana d))"
by simp
also have "… = rev (aplana (Nodo x i d))"
by simp
finally show ?thesis .
qed
qed
― ‹Lema auxiliar para la demostración declarativa detallada›
lemma rev_unit: "rev [x] = [x]"
proof -
have "rev [x] = rev [] @ [x]"
by (simp only: rev.simps(2))
also have "… = [] @ [x]"
by (simp only: rev.simps(1))
also have "… = [x]"
by (simp only: append.simps(1))
finally show ?thesis
by this
qed
― ‹La demostración estructurada y detallada es›
lemma
fixes a :: "'b arbolB"
shows "aplana (espejo a) = rev (aplana a)" (is "?P a")
proof (induct a)
fix x :: 'b
have "aplana (espejo (Hoja x)) = aplana (Hoja x)"
by (simp only: espejo.simps(1))
also have "… = [x]"
by (simp only: aplana.simps(1))
also have "… = rev [x]"
by (simp only: rev_unit)
also have "… = rev (aplana (Hoja x))"
by (simp only: aplana.simps(1))
finally show "?P (Hoja x)"
by this
next
fix x :: 'b
fix i assume h1: "?P i"
fix d assume h2: "?P d"
show "?P (Nodo x i d)"
proof -
have "aplana (espejo (Nodo x i d)) =
aplana (Nodo x (espejo d) (espejo i))"
by (simp only: espejo.simps(2))
also have "… = (aplana (espejo d)) @ [x] @ (aplana (espejo i))"
by (simp only: aplana.simps(2))
also have "… = (rev (aplana d)) @ [x] @ (rev (aplana i))"
by (simp only: h1 h2)
also have "… = rev ((aplana i) @ [x] @ (aplana d))"
by (simp only: rev_append rev_unit append_assoc)
also have "… = rev (aplana (Nodo x i d))"
by (simp only: aplana.simps(2))
finally show ?thesis
by this
qed
qed
― ‹La demostración aplicativa es›
lemma "aplana (espejo a) = rev (aplana a)"
apply (induct a)
apply simp
apply simp
done
― ‹La demostración aplicativa detallada es›
lemma "aplana (espejo a) = rev (aplana a)"
apply (induct a)
apply (simp only: espejo.simps(1) aplana.simps(1))
apply (simp only: rev_unit)
apply (simp only: espejo.simps(2) aplana.simps(2))
apply (simp only: rev_append)
apply (simp only: rev_unit)
apply (simp only: append_assoc)
done
― ‹La demostración aplicativa detallada compacta es›
lemma "aplana (espejo a) = rev (aplana a)"
apply (induct a)
apply (simp only:
espejo.simps(1)
aplana.simps(1)
rev_unit
espejo.simps(2)
aplana.simps(2)
rev_append
append_assoc)+
done
― ‹La demostración aplicativa detallada más compacta es›
lemma "aplana (espejo a) = rev (aplana a)"
apply (induct a)
apply (simp only:
espejo.simps
aplana.simps
rev_unit
rev_append
append_assoc)+
done
― ‹La demostración automática es›
lemma "aplana (espejo a) = rev (aplana a)"
by (induct a) simp_all
― ‹La demostración automática detallada es›
lemma "aplana (espejo a) = rev (aplana a)"
by (induct a)
(simp only:
espejo.simps
aplana.simps
rev_unit
rev_append
append_assoc)+
section ‹Árboles y bosques. Recursión mutua e inducción›
text ‹Nota. [Ejemplo de definición de tipos mediante recursión cruzada]
· Un árbol de tipo a es una hoja o un nodo de tipo a junto con un
bosque de tipo a.
· Un bosque de tipo a es el boque vacío o un bosque contruido añadiendo
un árbol de tipo a a un bosque de tipo a.›
datatype 'a arbol = Nodo "'a" "'a bosque"
and 'a bosque = Vacio | ConsB "'a arbol" "'a bosque"
text ‹Regla de inducción correspondiente a la recursión cruzada:
La regla de inducción sobre árboles y bosques es arbol_bosque.induct:
⟦⋀x b. P2 b ⟹ P1 (Nodo x b);
P2 Vacio;
⋀a b. ⟦P1 a; P2 b⟧ ⟹ P2 (ConsB a b)⟧
⟹ P1 a ∧ P2 b›
thm arbol_bosque.induct
text ‹Ejemplos de definición por recursión cruzada:
· aplana_arbol a) es la lista obtenida aplanando el árbol a.
· (aplana_bosque b) es la lista obtenida aplanando el bosque b.
· (map_arbol f a) es el árbol obtenido aplicando la función f a
todos los nodos del árbol a.
· (map_bosque f b) es el bosque obtenido aplicando la función f a
todos los nodos del bosque b. ›
fun aplana_arbol :: "'a arbol ⇒ 'a list" and
aplana_bosque :: "'a bosque ⇒ 'a list" where
"aplana_arbol (Nodo x b) = x # (aplana_bosque b)"
| "aplana_bosque Vacio = []"
| "aplana_bosque (ConsB a b) = (aplana_arbol a) @ (aplana_bosque b)"
fun map_arbol :: "('a ⇒ 'b) ⇒ 'a arbol ⇒ 'b arbol" and
map_bosque :: "('a ⇒ 'b) ⇒ 'a bosque ⇒ 'b bosque" where
"map_arbol f (Nodo x b) = Nodo (f x) (map_bosque f b)"
| "map_bosque f Vacio = Vacio"
| "map_bosque f (ConsB a b) = ConsB (map_arbol f a) (map_bosque f b)"
text ‹Ejemplo de demostración por inducción cruzada:
Demostrar que:
· aplana_arbol (map_arbol f a) = map f (aplana_arbol a)
· aplana_bosque (map_bosque f b) = map f (aplana_bosque b)›
declare [[names_short]]
― ‹La demostración declarativa es›
lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)
∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
proof (induct_tac a and b)
fix x b
assume HI: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
have "aplana_arbol (map_arbol f (Nodo x b)) =
aplana_arbol (Nodo (f x) (map_bosque f b))"
by simp
also have "… = (f x) # (aplana_bosque (map_bosque f b))"
by simp
also have "… = (f x) # (map f (aplana_bosque b))"
using HI by simp
also have "… = map f (aplana_arbol (Nodo x b))"
by simp
finally show "aplana_arbol (map_arbol f (Nodo x b)) =
map f (aplana_arbol (Nodo x b))"
by this
next
show "aplana_bosque (map_bosque f Vacio) = map f (aplana_bosque Vacio)"
by simp
next
fix a b
assume HI1: "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)"
and HI2: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
have "aplana_bosque (map_bosque f (ConsB a b)) =
aplana_bosque (ConsB (map_arbol f a) (map_bosque f b))" by simp
also have "… = aplana_arbol (map_arbol f a) @
aplana_bosque (map_bosque f b)"
by simp
also have "… = (map f (aplana_arbol a)) @ (map f (aplana_bosque b))"
using HI1 HI2 by simp
also have "… = map f (aplana_bosque (ConsB a b))" by simp
finally show "aplana_bosque (map_bosque f (ConsB a b)) =
map f (aplana_bosque (ConsB a b))"
by this
qed
― ‹La demostración declarativa detallada es›
lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)
∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
proof (induct_tac a and b)
fix x b
assume HI: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
have "aplana_arbol (map_arbol f (Nodo x b)) =
aplana_arbol (Nodo (f x) (map_bosque f b))"
by (simp only: map_arbol.simps(1))
also have "… = (f x) # (aplana_bosque (map_bosque f b))"
by (simp only: aplana_arbol.simps(1))
also have "… = (f x) # (map f (aplana_bosque b))"
by (simp only: HI)
also have "… = map f (aplana_arbol (Nodo x b))"
by (simp only: list.map aplana_arbol.simps(1))
finally show "aplana_arbol (map_arbol f (Nodo x b)) =
map f (aplana_arbol (Nodo x b))"
by this
next
show "aplana_bosque (map_bosque f Vacio) = map f (aplana_bosque Vacio)"
by (simp only: aplana_bosque.simps(1)
map_bosque.simps(1)
list.map)
next
fix a b
assume HI1: "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)"
and HI2: "aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
have "aplana_bosque (map_bosque f (ConsB a b)) =
aplana_bosque (ConsB (map_arbol f a) (map_bosque f b))"
by (simp only: map_bosque.simps(2))
also have "… = aplana_arbol (map_arbol f a) @
aplana_bosque (map_bosque f b)"
by (simp only: aplana_bosque.simps(2))
also have "… = (map f (aplana_arbol a)) @ (map f (aplana_bosque b))"
by (simp only: HI1 HI2)
also have "… = map f (aplana_arbol a @ aplana_bosque b)"
by (simp only: map_append)
also have "… = map f (aplana_bosque (ConsB a b))"
by (simp only: aplana_bosque.simps(2))
finally show "aplana_bosque (map_bosque f (ConsB a b)) =
map f (aplana_bosque (ConsB a b))"
by this
qed
text ‹Comentarios sobre la demostración anterior:
· (induct_tac a and b) indica que el método de demostración es por
inducción cruzada sobre a y b.
· Se generan 3 casos:
1. ⋀a bosque.
aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque) ⟹
aplana_arbol (map_arbol (arbol.Nodo a bosque) h) =
map h (aplana_arbol (arbol.Nodo a bosque))
2. aplana_bosque (map_bosque Vacio h) = map h (aplana_bosque Vacio)
3. ⋀arbol bosque.
⟦aplana_arbol (map_arbol arbol h) = map h (aplana_arbol arbol);
aplana_bosque (map_bosque bosque h) = map h (aplana_bosque bosque)⟧
⟹ aplana_bosque (map_bosque (ConsB arbol bosque) h) =
map h (aplana_bosque (ConsB arbol bosque))›
― ‹La demostración aplicativa es›
lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)
∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
apply (induct_tac a and b)
apply simp
apply simp
apply simp
done
― ‹La demostración aplicativa detallada es›
lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)
∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
apply (induct_tac a and b)
apply (simp only: map_arbol.simps aplana_arbol.simps)
apply (simp only: list.map(2))
apply (simp only: map_bosque.simps(1) aplana_bosque.simps(1))
apply (simp only: list.map(1))
apply (simp only: map_bosque.simps(2) aplana_bosque.simps(2))
apply (simp only: map_append)
done
― ‹La demostración aplicativa detallada compacta es›
lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)
∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
apply (induct_tac a and b)
apply (simp only:
map_arbol.simps
aplana_arbol.simps
list.map(2)
map_bosque.simps(1)
aplana_bosque.simps(1)
list.map(1)
map_bosque.simps(2)
aplana_bosque.simps(2)
map_append)+
done
― ‹La demostración aplicativa detallada más compacta es›
lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)
∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
apply (induct_tac a and b)
apply (simp only:
map_arbol.simps
map_bosque.simps
aplana_arbol.simps
aplana_bosque.simps
list.map
map_append)+
done
― ‹La demostración automática es›
lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)
∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
by (induct_tac a and b) simp_all
― ‹La demostración automática detallada es›
lemma "aplana_arbol (map_arbol f a) = map f (aplana_arbol a)
∧ aplana_bosque (map_bosque f b) = map f (aplana_bosque b)"
by (induct_tac a and b)
(simp only:
map_arbol.simps
map_bosque.simps
aplana_arbol.simps
aplana_bosque.simps
list.map
map_append)+
end