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

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

-- "javrodviv1"
fun hojas :: "arbol => nat" where
  "hojas H = 1"
| "hojas (N i d) = hojas i + hojas d"
  
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
  --------------------------------------------------------------------- 
*}

-- "javrodviv1"
fun max :: "nat ⇒ nat ⇒ nat" where
  "max a b= (if a≥ b then a else b)"

value "max 6 3" -- "= 6"

fun profundidad :: "arbol => nat" where
  "profundidad H = 0"
| "profundidad (N a b) = 1 + max (profundidad a) (profundidad b)"

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

(* Javrodviv1: Explico estas dos funciones, la que utilizo para los 
  lemas de abajo es profundidad ya que profundidad1 me encuentra
  contraejemplos y para evitar eso busque definir profundidad
  definidad de manera distinta. No obstante la que a mi me parece
  mas sensata para definir la profundidad de un árbol es la 
  profundidad1 *)

(* Javrodviv1: Fallo mio ya lo corregí*)

(*Pedrosrei: La profundidad correcta es la mayor. Si te encuentra
 contraejemplos más adelante es que te has equivocado en los
 enunciados. Las funciones máximo y mínimo vienen predefinidas
 ya sin necesidad de definirlas. *)

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

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

-- "javrodviv1"
fun es_abc :: "(arbol => 'a) => arbol => bool" where
  "es_abc f H = True"
| "es_abc f (N a b) = ((f a = f b) ∧ (es_abc f a ∧ es_abc f b))"

text {*  
  --------------------------------------------------------------------- 
  Nota. (size a) es el número de nodos del árbol a. Por ejemplo,
     size (N (N H H) (N H H)) = 3
  --------------------------------------------------------------------- 
*}

text{*Para entenderme he cambiado de función de tamaño, la demostración
es análoga pero buscando las simplificaciones de size cuando correspondan
*}

fun nodos::"arbol ⇒ nat" where
"nodos H = 0"
|"nodos (N i d) = 1+(nodos i)+(nodos d)"

lemma "size t= nodos t"
apply (induct t, auto)done

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

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

text{*Pedrosrei: Los enunciados y demostraciones que vienen a continuación 
son feos y engorrosos. Yo he optado por demostrarlo todo a través de 
una propiedad extraña a la demostración en principio. Animo encarecidamente
a que pongáis una demostración más corta y directa. Voy explicando paso
a paso qué he hecho en cada momento. Hecha esta demostración, el resto
son triviales por una cadena de resultados. 
 No existe relación de implicación en ningún sentido 
 entre hojas y profundidad, como es obvio y muestran los siguientes
 contraejemplos: *}
lemma "(((hojas(t1) = hojas(t2)))-->(profundidad(t1) = profundidad(t2)))"
quickcheck
oops
lemma "((profundidad(t1) = profundidad(t2)) -->
 ((hojas(t1) = hojas(t2))))"
quickcheck
oops
lemma "((profundidad(t1) = profundidad(t2)) <->
 ((hojas(t1) = hojas(t2))))"
quickcheck
oops
text {* Quickchecking... 
Testing conjecture with Quickcheck-exhaustive... 
Quickcheck found a counterexample:

t1 = N (N H H) (N H H)
t2 = N H (N H H)


Evaluated terms:
hojas t1 = 4
hojas t2 = 3

Ahora pongo una serie de resultados auxiliares que ayudarán en la prueba
 *}

lemma auxprof:"(es_abc profundidad t)∧(profundidad t = n)==> (t= abc n)"
apply (induct t arbitrary:n, auto)done

lemma eq_1_iff_exp_0:"Suc 0 = 2 ^ n <-> n=0"  apply (cases n, auto) done

lemma auxhojas:"(t= abc n)==> (es_abc hojas t)"
apply (induct n arbitrary: t, auto simp add: eq_1_iff_exp_0) done

lemma auxhoja:"(t= abc n)==>((hojas t = 2^n))"
apply (induct n  arbitrary: t rule: abc.induct, auto)done

text{* Pedrosrei. Y aquí viene la demostración larga y fea que os animo a mejorar.
He dejado los pasos exactamente que indica el razonador para que 
veáis qué hace en cada caso:
*}

lemma prof_eq_hoja:"es_abc profundidad t <-> es_abc hojas t" 
proof 
assume a1:"es_abc profundidad t"
have "∀t. ∃n. n = profundidad t" by auto
then obtain n where "n = profundidad t" by auto
with a1 have 1:"t= abc n" using auxprof by auto
thus "es_abc hojas t" using auxhojas by auto
next
show "es_abc hojas t ==> es_abc profundidad t" apply (induct t, auto)
  proof -
  fix t1 t2 
  assume a1:"es_abc profundidad t1"
  thus "es_abc profundidad t2 ==>
       es_abc hojas t1 ==>
       es_abc hojas t2 ==>
       hojas t1 = hojas t2 ==>
       profundidad t1 = profundidad t2" proof -
         assume a2:"es_abc profundidad t2"
         thus "es_abc hojas t1 ==>
         es_abc hojas t2 ==>
         hojas t1 = hojas t2 ==>
         profundidad t1 = profundidad t2"proof-
           assume a3:"es_abc hojas t1"
           thus "es_abc hojas t2 ==>
           hojas t1 = hojas t2 ==>
           profundidad t1 = profundidad t2"proof-
             assume a4:"es_abc hojas t2"
             thus "hojas t1 = hojas t2 ==>
             profundidad t1 = profundidad t2" proof -
               assume a5:"hojas t1 = hojas t2"
               thus "profundidad t1 = profundidad t2"
               proof-
               obtain n where 1:"profundidad t1 = n" by auto
               with a1 have 2:"t1 = abc n"using auxprof by auto
               hence 3:"es_abc hojas t1" using auxhojas by auto
               have "hojas t1 = (2::nat)^n" using 2 auxhoja by auto
               hence 3:"hojas t2 =  (2::nat)^n" using a5 by auto
               obtain m where 4:"profundidad t2 = m" by auto
               with a2 have 5:"t2 = abc m"using auxprof by auto
               hence 6:"es_abc hojas t2" using auxhojas by auto
               have "hojas t2 =  (2::nat)^m" using 5 auxhoja by auto
               with 3 have " (2::nat)^m =  (2::nat) ^n" by auto
               hence "m = n" apply (induct, auto)done
               hence "t2 = abc n" using 5 by auto
               with 2 have "t1= t2" by auto
               thus "profundidad t1 = profundidad t2" by auto
               qed
             qed
           qed
         qed
       qed
     qed
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
  --------------------------------------------------------------------- 
*}
text{* Pedrosrei. Aquí dejo esta. Es trivial debido a la demostración anterior,
sólo hace falta coger el mismo desvío. Aquí sí que podéis encontrar
una mucho más directa: *}

lemma auxnodo:"(t= abc n)==>(es_abc nodos t)∧(nodos t = (2^n - 1))"
apply (induct n  arbitrary: t rule: abc.induct, auto)done

lemma nodos_eq_hoja:"es_abc nodos t <-> es_abc hojas t" (is "?P t")
proof -
have 1:"es_abc hojas t <-> es_abc profundidad t" using prof_eq_hoja by auto
hence 2:"?P t = (es_abc profundidad t <-> es_abc nodos t)" by auto
have "(es_abc profundidad t <-> es_abc nodos t)"
proof
assume a1:"es_abc profundidad t"
have "∀t. ∃n. n = profundidad t" by auto
then obtain n where "n = profundidad t" by auto
with a1 have 1:"t= abc n" using auxprof by auto
thus "es_abc nodos t" using auxnodo by auto
next
show "es_abc nodos t ==> es_abc profundidad t" apply (induct t, auto)
  proof -
  fix t1 t2 
  assume a1:"es_abc profundidad t1"
  thus "es_abc profundidad t2 ==>
       es_abc nodos t1 ==>
       es_abc nodos t2 ==>
       nodos t1 = nodos t2 ==>
       profundidad t1 = profundidad t2" proof -
         assume a2:"es_abc profundidad t2"
         thus "es_abc nodos t1 ==>
         es_abc nodos t2 ==>
         nodos t1 = nodos t2 ==>
         profundidad t1 = profundidad t2"proof-
           assume a3:"es_abc nodos t1"
           thus "es_abc nodos t2 ==>
           nodos t1 = nodos t2 ==>
           profundidad t1 = profundidad t2"proof-
             assume a4:"es_abc nodos t2"
             thus "nodos t1 = nodos t2 ==>
             profundidad t1 = profundidad t2" proof -
               assume a5:"nodos t1 = nodos t2"
               thus "profundidad t1 = profundidad t2"
               proof-
               obtain n where 1:"profundidad t1 = n" by auto
               with a1 have 2:"t1 = abc n"using auxprof by auto
               hence 3:"es_abc nodos t1" using auxnodo by auto
               have "nodos t1 = (2::nat)^n - 1" using 2 auxnodo by auto
               hence 3:"nodos t2 =  (2::nat)^n - 1" using a5 by auto
               obtain m where 4:"profundidad t2 = m" by auto
               with a2 have 5:"t2 = abc m"using auxprof by auto
               hence 6:"es_abc nodos t2" using auxnodo by auto
               have "nodos t2 =  (2::nat)^m - 1" using 5 auxnodo by auto
               with 3 have 7:" (2::nat)^m - 1 =  (2::nat) ^n - 1" by auto
               hence "m = n" proof -
                 have " (2::nat)^m - 1 =  (2::nat) ^n - 1"using 7 by auto
                 hence "(2::nat)^m - 1 + 1 =  (2::nat) ^n" by auto
                 hence "(2::nat)^m  =  (2::nat) ^n" by auto
                 thus ?thesis apply (induct, auto)done
                 qed
               hence "t2 = abc n" using 5 by auto
               with 2 have "t1= t2" by auto
               thus "profundidad t1 = profundidad t2" by auto
               qed
             qed
           qed
         qed
       qed
     qed
qed
with 1 2 show ?thesis by auto
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
  --------------------------------------------------------------------- 
*}

text {* Pedrosrei. De hecho, esta es una parte de la anterior: *}

lemma prof_eq_nodos: "(es_abc profundidad t <-> es_abc nodos t)"
proof
assume a1:"es_abc profundidad t"
have "∀t. ∃n. n = profundidad t" by auto
then obtain n where "n = profundidad t" by auto
with a1 have 1:"t= abc n" using auxprof by auto
thus "es_abc nodos t" using auxnodo by auto
next
show "es_abc nodos t ==> es_abc profundidad t" apply (induct t, auto)
  proof -
  fix t1 t2 
  assume a1:"es_abc profundidad t1"
  thus "es_abc profundidad t2 ==>
       es_abc nodos t1 ==>
       es_abc nodos t2 ==>
       nodos t1 = nodos t2 ==>
       profundidad t1 = profundidad t2" proof -
         assume a2:"es_abc profundidad t2"
         thus "es_abc nodos t1 ==>
         es_abc nodos t2 ==>
         nodos t1 = nodos t2 ==>
         profundidad t1 = profundidad t2"proof-
           assume a3:"es_abc nodos t1"
           thus "es_abc nodos t2 ==>
           nodos t1 = nodos t2 ==>
           profundidad t1 = profundidad t2"proof-
             assume a4:"es_abc nodos t2"
             thus "nodos t1 = nodos t2 ==>
             profundidad t1 = profundidad t2" proof -
               assume a5:"nodos t1 = nodos t2"
               thus "profundidad t1 = profundidad t2"
               proof-
               obtain n where 1:"profundidad t1 = n" by auto
               with a1 have 2:"t1 = abc n"using auxprof by auto
               hence 3:"es_abc nodos t1" using auxnodo by auto
               have "nodos t1 = (2::nat)^n - 1" using 2 auxnodo by auto
               hence 3:"nodos t2 =  (2::nat)^n - 1" using a5 by auto
               obtain m where 4:"profundidad t2 = m" by auto
               with a2 have 5:"t2 = abc m"using auxprof by auto
               hence 6:"es_abc nodos t2" using auxnodo by auto
               have "nodos t2 =  (2::nat)^m - 1" using 5 auxnodo by auto
               with 3 have 7:" (2::nat)^m - 1 =  (2::nat) ^n - 1" by auto
               hence "m = n" proof -
                 have " (2::nat)^m - 1 =  (2::nat) ^n - 1"using 7 by auto
                 hence "(2::nat)^m - 1 + 1 =  (2::nat) ^n" by auto
                 hence "(2::nat)^m  =  (2::nat) ^n" by auto
                 thus ?thesis apply (induct, auto)done
                 qed
               hence "t2 = abc n" using 5 by auto
               with 2 have "t1= t2" by auto
               thus "profundidad t1 = profundidad t2" by auto
               qed
             qed
           qed
         qed
       qed
   qed
qed

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 10. Demostrar que (abc n) es un árbol binario completo.
  --------------------------------------------------------------------- 
*}
--"Pedrosrei:"
lemma " es_abc f (abc n)"
apply (induct n, auto) done


text {*  
  --------------------------------------------------------------------- 
  Ejercicio 11. Demostrar que si a es un árbolo binario completo
  respecto de la profundidad, entonces a es (abc (profundidad a)).
  --------------------------------------------------------------------- 
*}
--"Pedrosrei:"
lemma "es_abc profundidad a ==> (a= abc (profundidad a))"
apply (induct a, auto) done

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 12. Encontrar una medida f tal que (es_abc f) es distinto de 
  (es_abc size).
  --------------------------------------------------------------------- 
*}
--"Pedrosrei:"
lemma "es_abc f = es_abc nodos
quickcheck
oops
text {*
El contraejemplo no es más que una medida constante, la trivial:

Quickchecking... 
Testing conjecture with Quickcheck-exhaustive... 
Quickcheck found a counterexample:

f = λx. a⇣1
x = N H (N H H)


Evaluated terms:
es_abc f x = True
es_abc R8_Arboles_binarios_completos.size x = False
*}
end