Razonamiento automático (2013-14) Razonamiento automático (2013-14)

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"
fun hojas :: "arbol => nat" where
  "hojas H = Suc 0"
| "hojas (N i d) = hojas i + hojas d"

--"julrobrel"
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"
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"
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"
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: 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"
lemma 00:
 assumes "es_abc profundidad a"
 shows "hojas a = 2^(profundidad a)"
 using assms
by (induct a) auto

lemma "es_abc hojas a = es_abc profundidad a"
 by (induct a) (auto simp add: 00)

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"
(*he conseguido hacer uno!! bieeeeeeeen!!"*)
lemma relaccion_hojas_nodo:"hojas (a) = size (a) + 1"
by (induct a) auto


lemma "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



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*)
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

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

lemma "es_abc f a = es_abc size a"
quickcheck
oops
(*f = λx. a
a = N H (N H H)*)

end