Relación 7

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

(* fraortmoy marcarmor13*)
fun hojas :: "arbol => nat" where
  "hojas H = Suc 0"
| "hojas (N a b) = hojas a + hojas b"

value "hojas (N (N H H) (N H H)) = 4"

(* marpoldia1 anaprarod paupeddeg migtermor wilmorort pablucoto 
    ivamenjim serrodcal crigomgom rubgonmar  danrodcha ferrenseg *)
(* Es muy parecida a la definición anterior *)
fun hojas2 :: "arbol => nat" where
  "hojas2 H = 1" |
  "hojas2 (N i d) = hojas2 i + hojas2 d"
 
value "hojas2 (N (N H H) (N H H)) = 4"


(* anaprarod *)
(* Equivalencia de las definiciones *)
lemma "hojas a = hojas2 a"
by (induct a) simp_all

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

(* fraortmoy marpoldia1 anaprarod migtermor wilmorort marcarmor13*)
fun profundidad :: "arbol => nat" where
  "profundidad H = 0"
| "profundidad (N a b) = (if profundidad a > profundidad b
                          then 1 + profundidad a 
                          else 1 + profundidad b)"

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

(* anaprarod wilmorort pablucoto ivamenjim serrodcal crigomgom rubgonmar 
    danrodcha *)
fun profundidad2 :: "arbol => nat" where
  "profundidad2 H = 0"
 |"profundidad2 (N i d) = 1 + (max (profundidad2 i) (profundidad2 d))"

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

(* anaprarod *)
(* Equivalencia de las definiciones *)
lemma "profundidad a= profundidad2 a"
by (induct a) auto


(* paupeddeg *)
fun maximo :: "nat ×  nat => nat" where
  "maximo (a,b) = (if a > b 
                    then a else b)"

fun profundidad :: "arbol => nat" where
  "profundidad H = 0"
| "profundidad (N i d) = 1 + maximo(profundidad i, profundidad d)"


(* ivamenjim: llamando a la función anterior profundidad3 *)

lemma "profundidad a = profundidad3 a"
by (induct a) auto


(* ivamenjim *)
fun profundidad4 :: "arbol => nat" where
  "profundidad4 H = 0"
| "profundidad4 (N i d) = Suc (max (profundidad4 i)(profundidad4 d))"

lemma "profundidad a = profundidad4 a"
by (induct a) auto

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))
  --------------------------------------------------------------------- 
*}
(* fraortmoy marpoldia1 anaprarod paupeddeg migtermor  wilmorort 
    serrodcal crigomgom rubgonmar danrodcha *)
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))"

(* ivamenjim pablucoto marcarmor13*)
fun abc2 :: "nat ⇒ arbol" where
  "abc2 0 = H"
| "abc2 t = N (abc2 (t-1)) (abc2 (t-1))"

value "abc2 3 = N (N (N H H) (N H H)) (N (N H H) (N H H))"

(* ivamenjim: Metaejercicio de demostración *)
lemma "abc t = abc2 t"
by (induct t) auto

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

(* fraortmoy anaprarod migtermor serrodcal crigomgom rubgonmar 
    danrodcha *)
fun es_abc :: "(arbol => 'a) => arbol => bool" where
  "es_abc _ H = True"
| "es_abc f (N a b) = (es_abc f a ∧ es_abc f b ∧ (f a = f b))"


(* marpoldia1 paupeddeg ivamenjim pablucoto marcarmor13*)
fun es_abc2 :: "(arbol => 'a) => arbol => bool" where
  "es_abc2 f H = True" |
  "es_abc2 f (N i d) = ((f i = f d) ∧ (es_abc2 f i) ∧ (es_abc2 f d))"

(* anaprarod *)
(* Equivalencia de las definiciones *)
lemma "es_abc f a = es_abc2 f a"
by (induct a) auto

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

(* fraortmoy marpoldia1 migtermor wilmorort pablucoto serrodcal *)

lemma abc_prof_num_hojas:
  assumes "es_abc profundidad a"
  shows "hojas a = 2^(profundidad a)"
using assms
by (induct a) auto

(* Otra forma de escribir lo mismo *)
(* anaprarod crigomgom ivamenjim *)
lemma AUX7: "es_abc profundidad a ⟶ (hojas a = 2^(profundidad a))"
by (induct a) simp_all

(* Otra forma de escribir lo mismo *)
(* danrodcha *)
lemma aux1: "es_abc profundidad (a::arbol) ⟹ (hojas a = 2^ (profundidad a))"
by (induct a) simp_all

(* fraortmoy marpoldia1 migtermor anaprarod wilmorort serrodcal crigomgom 
    rubgonmar ivamenjim danrodcha marcarmor13 *)
(* También funciona con AUX7 *)

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

(* danrodcha *)
lemma 7: "es_abc profundidad a = es_abc hojas a"
apply (induct a) 
apply simp
apply (auto simp add: aux1)
done


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

(* fraortmoy marpoldia1 migtermor wilmorort pablucoto serrodcal marcarmor13*)

lemma abc_hojas_num_nodos:
  assumes "es_abc hojas a"
  shows "Suc(size a) = hojas a"
using assms
by (induct a) auto


(* Otra forma de escribir lo mismo *)
(* anaprarod crigomgom*)
lemma AUX8: "es_abc hojas a ⟶ (hojas a = (Suc (size a)))"
by (induct a) auto


(* fraortmoy marpoldia1 migtermor anaprarod wilmorort pablucoto serrodcal *)

lemma lej8: "es_abc hojas a = es_abc size a"
by (induct a) (auto simp add:abc_hojas_num_nodos [symmetric])

(* anaprarod crigomgom*)
(* Usando AUX8 *)
lemma L8: "es_abc hojas a= es_abc size a"
by (induct a) (auto simp add: AUX8)


(* ivamenjim *)
(* Teorema auxiliar *)
lemma auxEj8: "hojas a = size a + 1"
by (induct a) auto

(* ivamenjim *)
lemma lej8: "es_abc hojas a = es_abc size a"
by (induct a) (auto simp add: auxEj8)

(* danrodcha *)
lemma aux3: "es_abc hojas a ⟹ (hojas a = 1 + size a)"
by (induct a) simp_all

(* danrodcha *)
lemma 8: "es_abc hojas a = es_abc size a"
apply (induct a) 
apply simp
apply (auto simp add: aux3)
done

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

(* fraortmoy marpoldia1 migtermor anaprarod  wilmorort pablucoto 
    serrodcal crigomgom rubgonmar danrodcha ivamenjim marcarmor13
*)

lemma lej9:  "es_abc profundidad a = es_abc size a"
by (simp add: lej7 lej8)

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

(* fraortmoy marpoldia1 migtermor wilmorort pablucoto serrodcal crigomgom marcarmor13*)

lemma lej10: "es_abc profundidad (abc n)"
by (induct n) auto


(* anaprarod rubgonmar danrodcha *)
(* con un demostrador más débil *)
(* y en general para cualquier medida *)
lemma L10:  "es_abc f (abc a)"
by (induct a) simp_all

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

(* fraortmoy marpoldia1 migtermor wilmorort pablucoto serrodcal marcarmor13 *)

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


(* Otra forma de escribir lo mismo *)
(* anaprarod crigomgom rubgonmar *)
lemma "es_abc profundidad a ⟶ (a = (abc (profundidad a)))"
by (induct a) auto

(* danrodcha*)
lemma 11:"es_abc profundidad a ⟹ (a = (abc (profundidad a)))"
by (induct a) simp_all

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

(* migtermor *)
fun medida_nula :: "arbol => nat" where
 "medida_nula H = 0"
| "medida_nula (N i d) = 0"

lemma "es_abc medida_nula a = es_abc size a"
quickcheck
oops
(* Quickcheck encuentra el siguiente contraejemplo:
  a= N H (N H H) 
  Tras evaluar:
  es_abc medida_nula a = True
  es_abc size a = False*)


(* anaprarod  wilmorort pablucoto serrodcal  danrodcha marcarmor13*)
lemma "es_abc f a =  es_abc size a"
quickcheck
(* Quickcheck found a counterexample:
  f = λx. a⇩1   
  a = N H (N H H)
Evaluated terms:
  es_abc f a = True
  es_abc size a = False *)
oops
(* el contraejemplo que encuentra es la medida constante a1 *)

(*crigomgom *)
(* Como en la primera de las soluciones he usado la función constante 0 pero he usado una expresión lambda*)
lemma "es_abc (λx. 0::nat) a = es_abc size a"
quickcheck
oops


end