Diferencia entre revisiones de «Razonamiento sobre árboles y bosques»
De Lógica matemática y fundamentos (2018-19)
m |
|||
Línea 43: | Línea 43: | ||
espejo (espejo a) = a. | espejo (espejo a) = a. | ||
*} | *} | ||
+ | |||
+ | ― ‹La demostración aplicativa es› | ||
+ | lemma espejo_involutiva: | ||
+ | "espejo (espejo a ) = a" | ||
+ | apply (induct a) | ||
+ | (* 1. ⋀x. espejo (espejo (Hoja x)) = Hoja x | ||
+ | 2. ⋀x1a a1 a2. | ||
+ | ⟦espejo (espejo a1) = a1; | ||
+ | espejo (espejo a2) = a2⟧ | ||
+ | ⟹ espejo (espejo (Nodo x1a a1 a2)) = Nodo x1a a1 a2 *) | ||
+ | apply simp_all | ||
+ | (* *) | ||
+ | done | ||
+ | |||
+ | ― ‹La demostración automática es› | ||
+ | lemma espejo_involutiva_2: | ||
+ | "espejo (espejo a ) = a" | ||
+ | by (induct a) simp_all | ||
― ‹La demostración estructurada es› | ― ‹La demostración estructurada es› | ||
− | lemma | + | lemma espejo_involutiva_3: |
fixes a :: "'b arbolB" | fixes a :: "'b arbolB" | ||
shows "espejo (espejo a) = a" (is "?P a") | shows "espejo (espejo a) = a" (is "?P a") | ||
Línea 78: | Línea 96: | ||
⟹ espejo (espejo (Nodo a1 a2 a3)) = Nodo a1 a2 a3 | ⟹ espejo (espejo (Nodo a1 a2 a3)) = Nodo a1 a2 a3 | ||
*} | *} | ||
− | |||
− | |||
− | |||
− | |||
− | |||
text {* | text {* | ||
Línea 101: | Línea 114: | ||
aplana (espejo a) = rev (aplana a) | aplana (espejo a) = rev (aplana a) | ||
*} | *} | ||
+ | |||
+ | ― ‹La demostración aplicativa es› | ||
+ | lemma "aplana (espejo a) = rev (aplana a)" | ||
+ | apply (induct a) | ||
+ | (* 1. ⋀x. aplana (espejo (Hoja x)) = rev (aplana (Hoja x)) | ||
+ | 2. ⋀x1a a1 a2. | ||
+ | ⟦aplana (espejo a1) = rev (aplana a1); | ||
+ | aplana (espejo a2) = rev (aplana a2)⟧ | ||
+ | ⟹ aplana (espejo (Nodo x1a a1 a2)) = | ||
+ | rev (aplana (Nodo x1a a1 a2)) *) | ||
+ | apply simp_all | ||
+ | (* *) | ||
+ | done | ||
+ | |||
+ | ― ‹La demostración automática es› | ||
+ | lemma "aplana (espejo a) = rev (aplana a)" | ||
+ | by (induct a) simp_all | ||
― ‹La demostración estructurada es› | ― ‹La demostración estructurada es› | ||
Línea 126: | Línea 156: | ||
qed | qed | ||
qed | qed | ||
− | |||
− | |||
− | |||
− | |||
section {* Árboles y bosques. Recursión mutua e inducción *} | section {* Árboles y bosques. Recursión mutua e inducción *} | ||
Línea 186: | Línea 212: | ||
declare [[names_short]] | declare [[names_short]] | ||
+ | |||
+ | ― ‹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) | ||
+ | (* 1. aplana_arbol (map_arbol f Hoja) = | ||
+ | map f (aplana_arbol Hoja) | ||
+ | 2. ⋀x1 x2. | ||
+ | aplana_bosque (map_bosque f x2) = | ||
+ | map f (aplana_bosque x2) ⟹ | ||
+ | aplana_arbol (map_arbol f (Nodo x1 x2)) = | ||
+ | map f (aplana_arbol (Nodo x1 x2)) | ||
+ | 3. aplana_bosque (map_bosque f Vacio) = | ||
+ | map f (aplana_bosque Vacio) | ||
+ | 4. ⋀x1 x2. | ||
+ | ⟦aplana_arbol (map_arbol f x1) = map f (aplana_arbol x1); | ||
+ | aplana_bosque (map_bosque f x2) = map f (aplana_bosque x2)⟧ | ||
+ | ⟹ aplana_bosque (map_bosque f (ConsB x1 x2)) = | ||
+ | map f (aplana_bosque (ConsB x1 x2)) *) | ||
+ | apply simp_all | ||
+ | (* *) | ||
+ | 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 detallada es› | ― ‹La demostración detallada es› | ||
Línea 239: | Línea 292: | ||
map h (aplana_bosque (ConsB arbol bosque)) | map h (aplana_bosque (ConsB arbol bosque)) | ||
*} | *} | ||
− | |||
− | |||
− | |||
− | |||
− | |||
end | end | ||
</source> | </source> |
Revisión del 09:00 4 may 2019
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 aplicativa es›
lemma espejo_involutiva:
"espejo (espejo a ) = a"
apply (induct a)
(* 1. ⋀x. espejo (espejo (Hoja x)) = Hoja x
2. ⋀x1a a1 a2.
⟦espejo (espejo a1) = a1;
espejo (espejo a2) = a2⟧
⟹ espejo (espejo (Nodo x1a a1 a2)) = Nodo x1a a1 a2 *)
apply simp_all
(* *)
done
― ‹La demostración automática es›
lemma espejo_involutiva_2:
"espejo (espejo a ) = a"
by (induct a) simp_all
― ‹La demostración estructurada es›
lemma espejo_involutiva_3:
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
*}
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 aplicativa es›
lemma "aplana (espejo a) = rev (aplana a)"
apply (induct a)
(* 1. ⋀x. aplana (espejo (Hoja x)) = rev (aplana (Hoja x))
2. ⋀x1a a1 a2.
⟦aplana (espejo a1) = rev (aplana a1);
aplana (espejo a2) = rev (aplana a2)⟧
⟹ aplana (espejo (Nodo x1a a1 a2)) =
rev (aplana (Nodo x1a a1 a2)) *)
apply simp_all
(* *)
done
― ‹La demostración automática es›
lemma "aplana (espejo a) = rev (aplana a)"
by (induct a) simp_all
― ‹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
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 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)
(* 1. aplana_arbol (map_arbol f Hoja) =
map f (aplana_arbol Hoja)
2. ⋀x1 x2.
aplana_bosque (map_bosque f x2) =
map f (aplana_bosque x2) ⟹
aplana_arbol (map_arbol f (Nodo x1 x2)) =
map f (aplana_arbol (Nodo x1 x2))
3. aplana_bosque (map_bosque f Vacio) =
map f (aplana_bosque Vacio)
4. ⋀x1 x2.
⟦aplana_arbol (map_arbol f x1) = map f (aplana_arbol x1);
aplana_bosque (map_bosque f x2) = map f (aplana_bosque x2)⟧
⟹ aplana_bosque (map_bosque f (ConsB x1 x2)) =
map f (aplana_bosque (ConsB x1 x2)) *)
apply simp_all
(* *)
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 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))
*}
end