Relación 8

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

--"julrobrel maresccas4 jaisalmen zoiruicha"
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 pabflomar"
fun maximo :: "nat => nat => nat" where
  "maximo a b = (if a < b then b else a)"

-- "pabflomar"
fun profundidad_pfm :: "arbol => nat" where
  "profundidad_pfm H = 0"
| "profundidad_pfm (N i d) = 1 + maximo (profundidad_pfm i) (profundidad_pfm d)" 

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"

--"jaisalmen zoiruicha"
fun profundidad :: "arbol => nat" where
  "profundidad H = 0"
| "profundidad (N i d) = 1 + (if profundidad i > profundidad d then (profundidad i) else (profundidad d) )"


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 pabflomar jaisalmen zoiruicha"
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 pabflomar jaisalmem zoiruicha"
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)"
--"jaisalmen zoiruicha: el número de hojas es igual a 2 elevado a la profundidad"
lemma "(hojas (abc n))=2^(profundidad (abc n))"
by (induct n) auto

--"irealetei, diecabmen1, maresccas4 domlloriv"
(*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



-- "pabflomar"

lemma "(hojas (abc n))= 2^(profundidad_pfm (abc n))"
proof (induct n)
  show " hojas (abc 0) = 2 ^ profundidad_pfm (abc 0)" by simp
next
  fix n
  assume HI: " hojas (abc n) = 2 ^ profundidad_pfm (abc n)"
  then have " hojas (abc (Suc n)) = 2 * hojas (abc n)" by simp
  also have "... = 2 * (2 ^ profundidad_pfm (abc n))" using HI by simp
  finally show "hojas (abc (Suc n)) = 2 ^ profundidad_pfm (abc (Suc n))" 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
  --------------------------------------------------------------------- 
*}
--"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

-- "jaisalmen zoiruicha"
-- "cambios mínimos respecto al anterior, solo los ( )"
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

--"jaisalmen zoiruicha"
lemma "1 +  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

--"jaisalmen zoiruicha"
lemma "profundidad (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 marescpla jaisalmen zoiruicha"
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 jaisalmen zoiruicha"
lemma "es_abc f a = es_abc size a"
quickcheck
oops

(*f = λx. a
a = N H (N H H)*)

--"marescpla"

fun contraejemplo :: "arbol => nat" where
  "contraejemplo H = Suc(0)"|
  "contraejemplo (N i d)= Suc 0"
  
value "es_abc contraejemplo (N (N H H) H)"
value "es_abc size (N (N H H) H)"

end