Relación 6

chapter {* R7: Árboles binarios completos *}

theory R7_Arboles_binarios_completos
imports Main 
begin 

text {*  
  En esta relación se piden demostraciones automáticas (lo más cortas
  posibles). Para ello, en algunos casos es necesario incluir lemas
  auxiliares (que se demuestran automáticamente) y usar ejercicios
  anteriores. 

  --------------------------------------------------------------------- 
  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) = (N (N H H) (N H H) :: arbol)"

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
  --------------------------------------------------------------------- 
*}
 (*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut davperriv rafferrod jospermon1*)
fun hojas :: "arbol => nat" where
  "hojas H = 1"
| "hojas (N x y) =hojas x + hojas y"
 
value "hojas (N (N H H) (N H H)) = 4"

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

 (*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut  davperriv rafferrod jospermon1*)
fun profundidad :: "arbol => nat" where
  "profundidad H = 0"
| "profundidad (N x y) = Suc (max (profundidad x) (profundidad y))"

value "profundidad (N (N H H) (N H H)) = 2"

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

 (*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut davperriv rafferrod jospermon1*)
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.
  --------------------------------------------------------------------- 
*}

 (*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut  davperriv rafferrod jospermon1*)
fun es_abc :: "(arbol => 'a) => arbol => bool" where
  "es_abc f H = True"
| "es_abc f (N i d) =((f i = f d) ∧ (es_abc f i) ∧ (es_abc f d))"

value "es_abc profundidad (abc 4) = True"

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)) = 3"
value "size (N (N (N H H) (N H H)) (N (N H H) (N H H))) = 7"

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.
  --------------------------------------------------------------------- 
*}


(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut  davperriv jospermon1 rafferrod*)
(* blast no funciona, ¿cómo eliminar la conjunción sin recurrir a auto? *)
lemma hojas_prof:
"es_abc profundidad a ⟶ hojas a = 2^profundidad a"
  by (induct a) auto
theorem comp_p_h: "es_abc profundidad a = es_abc hojas a" 
  by (induct a) (auto simp add: hojas_prof)

lemma abc_profundidad_hojas:
  "es_abc profundidad a ⟶ hojas a = 2 ^ profundidad a" (is "?P a")
proof (induct a)
  show "?P H" by simp
next
  fix i assume HIi: "?P i"
  fix d assume HId: "?P d"
  show "?P (N i d)" using HIi HId by simp
qed

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.
  --------------------------------------------------------------------- 
*}

(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon jescudero cesgongut  davperriv jospermon1 rafferrod*)
lemma hojas_size:
" es_abc hojas a ⟶ hojas a = Suc (size a)"
  by (induct a) auto

 theorem comp_h_s: "es_abc hojas a = es_abc size a" 
  by (induct a) (auto simp add: hojas_size )


text {*  
  --------------------------------------------------------------------- 
  Ejercicio 9. Demostrar que un árbol binario a es completo respecto de
  la profundidad syss es completo respecto del número de nodos.
  --------------------------------------------------------------------- 
*}

(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon rafferrod*)
 theorem "es_abc profundidad a = es_abc size a" 
  by (simp_all add:comp_p_h comp_h_s)

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 10. Demostrar que (abc n) es un árbol binario completo.
  --------------------------------------------------------------------- 
*}

(*anddonram luicedval oscgonesc edupalhid macmerflo diwu2 rafcabgon rafferrod*)
  theorem "es_abc f (abc n) " 
  by (induct n) auto

(* cesgongut *)
theorem "es_abc f (abc n)" (is "?P n")
proof (induct n)
  show "?P 0" by simp
next
  fix a assume HI: "?P a"
  show "?P (Suc a)" using HI by simp
qed

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 11. Demostrar que si a es un árbolo binario completo
  respecto de la profundidad, entonces a es igual a
  (abc (profundidad a)).
  --------------------------------------------------------------------- 
*}

(*anddonram luicedval oscgonesc macmerflo diwu2 rafcabgon rafferrod*)
 theorem "es_abc profundidad a =(a=abc (profundidad a)) " 
  by (induct a) auto


(* edupalhid *)
lemma  
  assumes "es_abc profundidad a"
  shows   "a = (abc (profundidad a))"
using assms
by (induct a) auto

(* cesgongut *)
theorem "es_abc profundidad a ⟶ a = (abc (profundidad a))" (is "?P a")
proof (induct a)
  show "?P H" by simp
next
  fix i assume HIi: "?P i"
  fix d assume HId: "?P d"
  show "?P (N i d)" using HIi HId by auto
qed

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 12. Encontrar una medida f tal que (es_abc f) es distinto de 
  (es_abc size).
  --------------------------------------------------------------------- 
*}

(*anddonram(mas o menos llegué a la conclusión de que f(H)=f(N i d) )  luicedval edupalhid rafcabgon cesgongut  davperriv *)
fun funcion :: "arbol => nat" where
  "funcion H = 1"
| "funcion (N x y) =  funcion x "

 theorem "es_abc size a = es_abc funcion a" 
   quickcheck
   oops

end