Razonamiento sobre árboles y bosques - Historial de revisiones

Jalonso en 06:02 14 may 2020

2020-05-14T06:02:22Z

Jalonso en 06:00 14 may 2020

2020-05-14T06:00:37Z

Jalonso en 17:46 13 may 2020

2020-05-13T17:46:33Z

Mostrar los cambios

Jalonso en 07:00 4 may 2019

2019-05-04T07:00:19Z

Jalonso en 11:14 7 feb 2019

2019-02-07T11:14:23Z

Jalonso en 11:08 7 feb 2019

2019-02-07T11:08:04Z

Jalonso en 11:07 7 feb 2019

2019-02-07T11:07:41Z

Página nueva

<source lang="haskell">
chapter {* Tema 8: Razonamiento sobre árboles *}

theory T8_Razonamiento_sobre_arboles
imports Main HOL.Parity
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 {*
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

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 estructurada 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

― ‹La demostración automática es›
lemma "aplana (espejo a) = rev (aplana a)"
by (induct a) auto

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 = Hoja | 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:
⟦P1 Hoja;
⋀x b. P2 b ⟹ P1 (Nodo x b);
P2 Vacio;
⋀a b. ⟦P1 a; P2 b⟧ ⟹ P2 (ConsB a b)⟧
⟹ P1 a ∧ P2 b
*}

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 Hoja = []"
| "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 Hoja = Hoja"
| "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 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)
show "aplana_arbol (map_arbol f Hoja ) = map f (aplana_arbol Hoja)"
by simp
next
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))" .
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 simp
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 4 casos:
1. aplana_arbol (map_arbol arbol.Hoja h) = map h (aplana_arbol arbol.Hoja)
2. ⋀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))
3. aplana_bosque (map_bosque Vacio h) = map h (aplana_bosque Vacio)
4. ⋀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 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) auto

end
</source>

@@ Línea 104: / Línea 104: @@
                     espejo (espejo a3) = a3⟧
                    ⟹ espejo (espejo (Nodo a1 a2 a3)) = Nodo a1 a2 a3›
 ― ‹La demostración automática es›
 lemma
    "espejo (espejo a) = a"
-   by (induct a) simp_all
+   by (induct a) simp+
 text ‹Ejemplo. [Aplanamiento de árboles]
@@ Línea 203: / Línea 224: @@
    qed
 qed
 ― ‹La demostración automática es›
 lemma "aplana (espejo a) = rev (aplana a)"
    by (induct a) simp_all
 section ‹Árboles y bosques. Recursión mutua e inducción›
@@ Línea 351: / Línea 424: @@
            ⟹ aplana_bosque (map_bosque (ConsB arbol bosque) h) =
               map h (aplana_bosque (ConsB arbol bosque))›
 ― ‹La demostración automática es›
@@ Línea 357: / Línea 480: @@
    by (induct_tac a and b) simp_all
 end
 </source>

← Revisión anterior		Revisión del 11:08 7 feb 2019
Línea 1:		Línea 1:
−	<source lang="~~haskell~~">	+	<source lang="isabelle">
	chapter {* Tema 8: Razonamiento sobre árboles *}		chapter {* Tema 8: Razonamiento sobre árboles *}

@@ Línea 3: / Línea 3: @@
 theory T8_Razonamiento_sobre_arboles
-imports Main HOL.Parity
+imports Main
 begin

@@ Línea 43: / Línea 43: @@
       espejo (espejo a) = a.
 *}
 ― ‹La demostración estructurada es›
-lemma espejo_involutiva:
+lemma espejo_involutiva_3:
    fixes a :: "'b arbolB"
    shows "espejo (espejo a) = a" (is "?P a")
@@ Línea 78: / Línea 96: @@
                    ⟹ espejo (espejo (Nodo a1 a2 a3)) = Nodo a1 a2 a3
 *}
 text {*
@@ Línea 101: / Línea 114: @@
       aplana (espejo a) = rev (aplana a)
 *}
 ― ‹La demostración estructurada es›
@@ Línea 126: / Línea 156: @@
   qed
 qed
 section {* Árboles y bosques. Recursión mutua e inducción *}
@@ Línea 186: / Línea 212: @@
 declare [[names_short]]
 ― ‹La demostración detallada es›
@@ Línea 239: / Línea 292: @@
               map h (aplana_bosque (ConsB arbol bosque))
 *}
 end
 </source>

← Revisión anterior	Revisión del 11:14 7 feb 2019
(Sin diferencias)