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 josgarsan fracorjim1 *)
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
   manmorjim1 juacabsou lucnovdos dancorgar bowma *)
(* 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
   dancorgar *) 
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 ferrenseg josgarsan juacabsou lucnovdos bowma *)
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 profundidad3 :: "arbol => nat" where
  "profundidad3 H       = 0"
| "profundidad3 (N i d) = 1 + maximo (profundidad3 i, profundidad3 d)"

(* ivamenjim: llamando a la función anterior profundidad3 *)
lemma "profundidad a = profundidad3 a"
by (induct a) auto

(* ivamenjim manmorjim1 fracorjim1 *)
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 ferrenseg josgarsan
   manmorjim1 juacabsou fracorjim1 lucnovdos dancorgar bowma *)
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 ferrenseg juacabsou josgarsan fracorjim1 lucnovdos bowma *)
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 manmorjim1
   dancorgar *) 
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
   fracorjim1 josgarsan lucnovdos bowma *) 
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 paupeddeg juacabsou *)
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 paupeddeg
   juacabsou bowma *) 
(* 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

(* ferrenseg *)
lemma [simp]: "es_abc profundidad a ⟶ hojas a = 2 ^ (profundidad a)"
by (induct a) auto

(* Comentario: Uso de la declaración simp *)

theorem es_abc_profundidad_hojas: 
  "es_abc profundidad a = es_abc hojas a"
by (induct a) auto

(* Comentario: Dependencia de la declaración simp. *)

(* dancorgar *)
lemma rel_hojas_prof: "es_abc hojas a ∧ es_abc profundidad a
      ⟹ hojas a = 2 ^ profundidad a"
by (induct a) (auto)

theorem "es_abc hojas a = es_abc profundidad a"
by (induct a) (auto simp add: rel_hojas_prof)

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 josgarsan lucnovdos bowma *) 
lemma abc_hojas_num_nodos:
  assumes "es_abc hojas a"
  shows   "Suc (size a) = hojas a"
using assms
by (induct a) auto

(* Comentario sobre orientación de igualdades. *)

(* Otra forma de escribir lo mismo *)
(* anaprarod crigomgom paupeddeg juacabsou rubgonmar *)
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])

(* Comentario sobre orientación de igualdades. *)

(* anaprarod crigomgom paupeddeg juacabsou rubgonmar *)
(* 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 lej8b: "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

(* ferrenseg *)
lemma [simp]: "hojas a = size a + 1"
by (induct a) auto
 
theorem es_abc_hojas_size: "es_abc hojas a = es_abc size a"
by (induct a) auto

(* fracorjim1 *)
lemma aux10 : "hojas (a::arbol) = Suc(size a)"
apply (induct a)
apply auto
done
    
lemma es_abc_hojas_size_10 : "es_abc hojas (a::arbol) = es_abc size a"
apply (induct a)
apply (auto simp add: aux10)
done

(* dancorgar *)
lemma rel_hojas_size: "es_abc hojas a ∧ es_abc size a
      ⟹ hojas a = (size a) + 1"
by (induct a) (auto)

theorem "es_abc hojas a = es_abc size a"
by (induct a) (auto simp add: rel_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.
  --------------------------------------------------------------------- 
*}

(* fraortmoy marpoldia1 migtermor anaprarod  wilmorort pablucoto 
   serrodcal crigomgom rubgonmar danrodcha ivamenjim marcarmor13
   paupeddeg juacabsou josgarsan bowma lucnovdos *)
lemma lej9:  "es_abc profundidad a = es_abc size a"
by (simp add: lej7 lej8)

(* ferrenseg *)
corollary es_abc_size_profundidad: "es_abc size a = es_abc profundidad a"
by (simp add: es_abc_profundidad_hojas es_abc_hojas_size)

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

(* fraortmoy marpoldia1 migtermor wilmorort pablucoto serrodcal
   crigomgom marcarmor13 paupeddeg juacabsou dancorgar lucnovdos *)
lemma lej10: "es_abc profundidad (abc n)"
by (induct n) auto

(* anaprarod rubgonmar danrodcha ferrenseg ivamenjim paupeddeg juacabsou bowma*)
(* 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

(* ivamenjim *)
(* Igual que el anterior pero usando auto *)
lemma lej10b: "es_abc f (abc n)"
by (induct n) auto

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 ferrenseg ivamenjim paupeddeg juacabsou
   dancorgar bowma lucnovdos *) 
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
   ferrenseg ivamenjim paupeddeg juacabsou rubgonmar bowma lucnovdos *) 
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

(* dancorgar *)
fun medida :: "arbol => bool" where
  "medida H       = True"
| "medida (N i d) = ((profundidad i) = (size d))"

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

end