Relación 8
De Razonamiento automático (2013-14)
Revisión del 11:35 16 ene 2014 de Marescpla (discusión | contribuciones)
header {* R8: Árboles binarios completos *}
theory R8_Arboles_binarios_completos
imports Main
begin
text {*
---------------------------------------------------------------------
Ejercicio 1. Definir el tipo de datos arbol para representar los
árboles binarios que no tienen información ni en los nodos y ni en las
hojas. Por ejemplo, el árbol
·
/ \
/ \
· ·
/ \ / \
· · · ·
se representa por "N (N H H) (N H H)".
---------------------------------------------------------------------
*}
datatype arbol = H | N arbol arbol
value "N (N H H) (N H H)"
value "(N (N H H) (N (N H H) H))" --"Este tambien es un arbol segun la definicion del tipo. Sin embargo no es completo."
text {*
---------------------------------------------------------------------
Ejercicio 2. Definir la función
hojas :: "arbol => nat"
tal que (hojas a) es el número de hojas del árbol a. Por ejemplo,
hojas (N (N H H) (N H H)) = 4
---------------------------------------------------------------------
*}
--"diecabmen1 irealetei juaruipav domlloriv marescpla"
fun hojas :: "arbol => nat" where
"hojas H = Suc 0"
| "hojas (N i d) = hojas i + hojas d"
--"julrobrel maresccas4"
fun hojas_jrr :: "arbol => nat" where
"hojas_jrr H = 1" --"julrobrel: minima diferencia con la anterior"
|"hojas_jrr (N i d) = (hojas_jrr i) + (hojas_jrr d)"
value "hojas_jrr (N (N H H) (N H H))" -- "= 4"
value "hojas (N (N H H) (N H H))" -- "= 4"
value "hojas (N (N H H) (N (N H H) H))" --"= 5" --"julrobrel: la funcion tambien funciona sobre arboles binarios no completos"
text {*
---------------------------------------------------------------------
Ejercicio 4. Definir la función
profundidad :: "arbol => nat"
tal que (profundidad a) es la profundidad del árbol a. Por ejemplo,
profundidad (N (N H H) (N H H)) = 2
---------------------------------------------------------------------
*}
--"diecabmen1 juaruipav"
fun profundidad :: "arbol => nat" where
"profundidad H = 0"
| "profundidad (N i d) = (if profundidad i > profundidad d then Suc (profundidad i) else Suc (profundidad d))"
--"julrobrel"
fun maximo :: "nat => nat => nat" where
"maximo a b = (if a < b then b else a)"
value "maximo 3 4" -- "=4"
--"julrobrel"
fun profundidad_jrr :: "arbol => nat" where
"profundidad_jrr H = 0"
|"profundidad_jrr (N i d) = Suc (maximo (profundidad_jrr i) (profundidad_jrr d))" --"julrobrel: En realidad al ser arboles completos no deberia hacer falta el maximo"
value "profundidad (N (N H H) (N H H))" -- "= 2"
value "profundidad (N (N H H) (N (N H H) H))" -- "= 3" --"julrobrel: profundidad tambien funciona sobre arboles binarios no completos"
value "profundidad_jrr (N (N H H) (N H H))" -- "= 2"
value "profundidad_jrr (N (N H H) (N (N H H) H))" -- "= 3" --"julrobrel: profundidad tambien funciona sobre arboles binarios no completos"
--"irealetei maresccas4 domlloriv marescpla"
--"marescpla: yo he puesto un Suc en vez de un 1+"
fun profundidad3 :: "arbol => nat" where
"profundidad3 (H) = 0"
| "profundidad3 (N ai ad) = 1 + (if (profundidad3 ai > profundidad3 ad) then profundidad3 ai else profundidad3 ad)"
value "profundidad3 (N (N H H) (N H (N H (N H H))))" -- "= 4"
text {*
---------------------------------------------------------------------
Ejercicio 5. Definir la función
abc :: "nat ⇒ arbol"
tal que (abc n) es el árbol binario completo de profundidad n. Por
ejemplo,
abc 3 = N (N (N H H) (N H H)) (N (N H H) (N H H))
---------------------------------------------------------------------
*}
--"diecabmen1, julrobrel irealetei juaruipav maresccas4 domlloriv marescpla"
fun abc :: "nat ⇒ arbol" where
"abc 0 = H"
| "abc (Suc n) = (N (abc n) (abc n))"
value "abc 3" -- "= N (N (N H H) (N H H)) (N (N H H) (N H H))"
text {*
---------------------------------------------------------------------
Ejercicio 6. Un árbol binario a es completo respecto de la medida f si
a es una hoja o bien a es de la forma (N i d) y se cumple que tanto i
como d son árboles binarios completos respecto de f y, además,
f(i) = f(r).
Definir la función
es_abc :: "(arbol => 'a) => arbol => bool
tal que (es_abc f a) se verifica si a es un árbol binario completo
respecto de f.
---------------------------------------------------------------------
*}
--"diecabmen1 irealetei juaruipav maresccas4 domlloriv marescpla"
fun es_abc :: "(arbol => 'a) => arbol => bool" where
"es_abc f H = True"
| "es_abc f (N i d) = ((es_abc f i) ∧ (es_abc f d) ∧ (f i = f d))"
value "es_abc profundidad ( N (N (N H H) (N H H)) (N (N H H) (N H H)))" -- "true"
value "es_abc profundidad ( N (N (N H H) (N H H)) (N H (N H H)))" -- "false"
value "es_abc profundidad ( N (N (N H H) (N H H)) (N (N H H) H))" -- "false"
value "es_abc profundidad ( N (N H (N H H)) (N H (N H H)))" -- "false"
--"julrobrel"
fun es_abc_jrr:: "nat => arbol => bool" where
"es_abc_jrr 0 H = True"
|"es_abc_jrr (Suc f) H = False"
|"es_abc_jrr 0 (N i d) = False"
|"es_abc_jrr (Suc f) (N i d) = (((es_abc_jrr f i) ∧ (es_abc_jrr f d)) ∧ ((profundidad_jrr i) = (profundidad_jrr d)) ∧ ((profundidad_jrr i) = f))"
value "es_abc_jrr 2 (N (N H H) (N H H))"
value "es_abc_jrr 0 (N (N H H) (N (N H H) H))" --"=False" --"julrobrel: No es un arbol binario completo"
value "es_abc_jrr 1 (N (N H H) (N (N H H) H))" --"=False" --"julrobrel: No es un arbol binario completo"
value "es_abc_jrr 2 (N (N H H) (N (N H H) H))" --"=False" --"julrobrel: No es un arbol binario completo"
value "es_abc_jrr 3 (N (N H H) (N (N H H) H))" --"=False" --"julrobrel: No es un arbol binario completo"
text {*
---------------------------------------------------------------------
Nota. (size a) es el número de nodos del árbol a. Por ejemplo,
size (N (N H H) (N H H)) = 3
---------------------------------------------------------------------
*}
value "size (N (N H H) (N H H))"
value "size (N (N (N H H) (N H H)) (N (N H H) (N H H)))"
value "size (N (N H H) (N (N H H) H))" --"julrobrel: No es un arbol binario completo"
text {*
---------------------------------------------------------------------
Nota. Tenemos 3 funciones de medida sobre los árboles: número de
hojas, número de nodos y profundidad. A cada una le corresponde un
concepto de completitud. En los siguientes ejercicios demostraremos
que los tres conceptos de completitud son iguales.
---------------------------------------------------------------------
*}
text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar que un árbol binario a es completo respecto de
la profundidad syss es completo respecto del número de hojas.
---------------------------------------------------------------------
*}
--"julrobrel: en un arbol binario completo la profundidad y las hojas estan relacionadas por la siguiente igualdad (hojas = 2^profundidad)"
lemma "(hojas (abc n))=2^(profundidad (abc n))"
by (induct n) auto
--"irealetei, diecabmen1, maresccas4"
(*irealetei: casi me estalla el cerebro con esta demo, gracias a Marco que me dio una pista hace un par de días sobre que el había usado el assumes. La automática se me queda a medias.*)
lemma 00:
assumes "es_abc profundidad a"
shows "hojas a = 2^(profundidad a)"
using assms
by (induct a) auto
lemma profundidad_hojas_completo: "es_abc hojas a = es_abc profundidad a"
by (induct a) (auto simp add: 00)
-- "maresccas4: no he sido capaz de terminar la demostración manual"
theorem "es_abc profundidad a = es_abc hojas a" (is "?P a")
proof (induct a)
show "?P H" by simp
next
fix i d
assume H1: "?P i"
assume H2: "?P d"
show "?P (N i d)"
proof (cases)
assume H: "es_abc profundidad (N i d)"
then have "es_abc profundidad (N i d) = (es_abc profundidad i ∧ es_abc profundidad d ∧ profundidad i = profundidad d)" by simp
also have "... = (es_abc hojas i ∧ es_abc hojas d ∧ profundidad i = profundidad d)" using H1 H2 by simp
also have "... = (es_abc hojas i ∧ es_abc hojas d ∧ hojas i = hojas d)" using H by (simp add: 00)
also have "... = es_abc hojas (N i d)" by simp
finally show ?thesis .
next
assume H: "¬ es_abc profundidad (N i d)"
show "?P (N i d)"
proof (cases)
assume I: "(es_abc profundidad i ∧ es_abc profundidad d)"
then have "es_abc profundidad (N i d) = (es_abc profundidad i ∧ es_abc profundidad d ∧ profundidad i = profundidad d)" by simp
also have "...= (profundidad i = profundidad d)" using H I by simp
oops
text {*
---------------------------------------------------------------------
Ejercicio 8. Demostrar que un árbol binario a es completo respecto del
número de hojas syss es completo respecto del número de nodos
---------------------------------------------------------------------
*}
--"julrobrel: la relacion entre hojas y nodos la da la siguiente ecuacion (nodos = hojas -1) o lo que es lo mismo (nodos+1=hojas)"
lemma "Suc(size (abc n))=hojas (abc n)"
by (induct n) auto
-- "irealetei maresccas4 diecabmen1 domlloriv"
(*he conseguido hacer uno!! bieeeeeeeen!!"*)
lemma relaccion_hojas_nodo:"hojas (a) = size (a) + 1"
by (induct a) auto
lemma hojas_size_completo: "es_abc hojas a = es_abc size a"
by (induct a) (auto simp add: relaccion_hojas_nodo)
lemma "es_abc hojas a = es_abc size a"
proof (induct a)
show "es_abc hojas H = es_abc size H" by simp
next
fix i d
assume HI1:"es_abc hojas i = es_abc size i"
assume HI2:"es_abc hojas d = es_abc size d"
show " es_abc hojas (N i d) = es_abc size (N i d)"
proof -
have "es_abc hojas (N i d) = (es_abc hojas i ∧ es_abc hojas d ∧ hojas i = hojas d)" by simp
also have "... = (es_abc size i ∧ es_abc size d ∧ hojas i = hojas d)" using HI1 HI2 by simp
also have "... = (es_abc size i ∧ es_abc size d ∧ size i = size d)" by (simp add:relaccion_hojas_nodo)
also have "... = es_abc size (N i d)" by simp
finally show ?thesis by simp
qed
qed
text {*
---------------------------------------------------------------------
Ejercicio 9. Demostrar que un árbol binario a es completo respecto de
la profundidad syss es completo respecto del número de nodos
---------------------------------------------------------------------
*}
--"julrobrel: la relacion entre la profundidad y el numero de nodos es (nodos+1=2^profundidad)"
lemma "Suc(size (abc n))=2^(profundidad (abc n))"
by (induct n) auto
-- "irealetei: suponía que sería como el 7 pero no sale... por mucho que me pongo a definir lemas. De todos modos dejo donde me he quedado"
lemma 02:
assumes "es_abc size a"
shows "size a + 1 = 2^(profundidad a)"
using assms
by (induct a) auto
lemma 03:
assumes "es_abc hojas a"
shows "Suc(size a) = hojas a"
using assms
by (induct a) auto
lemma "es_abc profundidad a = es_abc size a"
by (induct a) (auto simp add:00 02 03) --"He puesto todas la teorías aunque suponía que con 02 sería suficiente"
-- "maresccas4"
(*irealetei: como me he complicado la existencia...*)
theorem "es_abc profundidad a = es_abc size a"
proof -
have "(es_abc profundidad a = es_abc hojas a)" by (simp add: profundidad_hojas_completo)
also have "...= es_abc size a" by (simp add: hojas_size_completo)
finally show ?thesis.
qed
text {*
---------------------------------------------------------------------
Ejercicio 10. Demostrar que (abc n) es un árbol binario completo.
---------------------------------------------------------------------
*}
--"julrobrel: para todo lo anterior nos hemos basado en que (abc n) siempre devuelve un arbol binario completo. Habra que demostrarlo..."
lemma profundidad_lemma: "profundidad_jrr (abc n) = n"
by (induct n) auto
lemma "es_abc_jrr n (abc n)"
by (induct n) (auto simp add:profundidad_lemma)
-- "irealetei"
lemma "es_abc profundidad (abc n)" by (induct n) auto
(* irealetei: es raro, hay que hacerlo por induct aunque parece que no usa la HI... pero por cases no se lo traga.
Creo que está mejor la solución de marco, pero la dejo para comentarla.*)
lemma "es_abc profundidad (abc n)"
proof (induct n)
show "es_abc profundidad (abc 0)" by simp
next
fix n
assume " es_abc profundidad (abc n)"
then have "es_abc profundidad (abc (Suc n))= es_abc profundidad (N (abc n) (abc n))" by simp
also have "... = es_abc profundidad (abc n)" by simp
finally show "es_abc profundidad (abc n) ⟹ es_abc profundidad (abc (Suc n))" by simp
qed
-- "maresccas4"
lemma "es_abc profundidad (abc n)"
proof (induct n)
show "es_abc profundidad (abc 0)" by simp
next
fix n
assume HI: "es_abc profundidad (abc n)"
then have "es_abc profundidad (abc (Suc n))= es_abc profundidad (N (abc n) (abc n))" by simp
also have "...= (es_abc profundidad (abc n) ∧ es_abc profundidad (abc n) ∧ profundidad (abc n) = profundidad (abc n))" by simp
finally show "es_abc profundidad (abc (Suc n))" using HI by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 11. Demostrar que si a es un árbolo binario completo
respecto de la profundidad, entonces a es (abc (profundidad a)).
---------------------------------------------------------------------
*}
lemma "(es_abc_jrr (profundidad_jrr a) a) ⟶ a = abc (profundidad_jrr a)"
by (induct a) auto
--"irealetei maresccas4 domlloriv"
lemma "es_abc profundidad a ⟹ a = abc (profundidad a)" by (induct a) auto
text {*
---------------------------------------------------------------------
Ejercicio 12. Encontrar una medida f tal que (es_abc f) es distinto de
(es_abc size).
---------------------------------------------------------------------
*}
--"julrobrel"
lemma "es_abc_jrr f t = es_abc_jrr (size t) t"
quickcheck
oops
--"julrobrel: El arbol que es una hoja..."
(*
Quickcheck found a counterexample:
f = Suc 0
t = H
Evaluated terms:
es_abc f t = False
es_abc (size t) t = True
*)
-- "irealetei maresccas4 domlloriv"
lemma "es_abc f a = es_abc size a"
quickcheck
oops
(*f = λx. a
a = N H (N H H)*)
end