Relación 8

header {* R8: Árboles binarios completos *}

theory R8
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, jeshorcob, davoremar, domcadgom, carvelcab, juacorvic"
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"

-- "davoremar, carvelcab, juacorvic"
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. *)

-- "jeshorcob, domcadgom"
fun pr1 :: "arbol => nat" where
   "pr1 H       = 0"
 | "pr1 (N i d) = Suc (max (pr1 i) (pr1 d))"

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, jeshorcob, davoremar, domcadgom, carvelcab, juacorvic"
fun abc :: "nat ⇒ arbol" where
  "abc 0       = H"
| "abc (Suc n) = N (abc n) (abc n)" 

-- "jeshorcob" (* ¿Pudiera ser que esta sea más rápida? *)
fun abc1 :: "nat ⇒ arbol" where
   "abc1 0       = H"
 | "abc1 (Suc n) = (let a = abc1 n in N a a)"

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_abc1 :: "(arbol => 'a) => arbol => bool" where
  "es_abc1 f H       = True"
| "es_abc1 f (N a b) = ((f a = f b) ∧ (es_abc1 f a ∧ es_abc1 f b))"

-- "jeshorcob, davoremar, domcadgom, carvelcab"
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)"

-- "juacorvic"
fun es_abc3 :: "(arbol => 'a) => arbol => bool" where
  "es_abc3 f H       = True"
| "es_abc3 f (N i d) = ( es_abc3 f i ∧ es_abc3 f d ∧ f i = f d )"

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

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

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

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

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

(* jeshorcob: creo que tengo una demostración mas elegante tan
   sólo hace falta encontrar la relacion entre hojas y profundidad. *)

-- "jeshorcob, carvelcab"
lemma a1: 
  assumes "es_abc hojas a"
  shows "hojas a = 2^(pr1 a)"
using assms 
by (induct a, simp_all)

-- "jeshorcob, carvelcab,davoremar"
lemma cpr1_chojas: "es_abc pr1 a = es_abc hojas a"
by (induct a, auto simp add: a1)

(* mjeshorcob: esta es la detallada*)
-- "jeshorcob,caarvelcab"
lemma "es_abc pr1 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"
  have "es_abc pr1 (N i d) = 
        (pr1 i = pr1 d ∧ es_abc pr1 i ∧ es_abc pr1 d )" by simp
  also have "… = (pr1 i = pr1 d ∧ es_abc hojas i ∧ es_abc hojas d)"
    using h1 and h2 by simp
  also have "… = (hojas i = hojas d ∧ es_abc hojas i ∧ es_abc hojas d)" 
    using a1 by auto
  also have "… = es_abc hojas (N i d)" by simp
  finally show "?P (N i d)" by simp 
qed

-- "domcadgom"
lemma aux1: "es_abc profundidad a ⟹ hojas a = 2^(profundidad  a)"
by (induct a, simp_all)

lemma completo1: "es_abc (profundidad) a = es_abc (hojas) a"
proof (induct a, simp)
  fix a1 :: arbol and a2 :: arbol
  assume a1: "es_abc profundidad a1 = es_abc hojas a1"
  assume a2: "es_abc profundidad a2 = es_abc hojas a2"
  have "es_abc profundidad a2 ∧ es_abc profundidad a1 ⟶ 
        es_abc profundidad (N a1 a2) = es_abc hojas (N a1 a2)" 
    using a1 a2 by (simp add: aux1)
  thus "es_abc profundidad (N a1 a2) = es_abc hojas (N a1 a2)" 
    using a1 a2 es_abc.simps(2) by blast
qed

--"davoremar"
lemma prof_hojas:
  assumes "es_abc hojas t"
  shows "hojas t = 2^(profundidad t)"
using assms by (induct t, simp_all)

--"davoremar"
lemma profundidad_hojas: "es_abc profundidad t = es_abc hojas t"
by (induct t) (auto simp add: prof_hojas)

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

(* Javrodviv1: Bueno yo para este ejercicio he encontrado algo más
   sencillo, tan sólo hay que encontrar una relación de igualdad entre
   hojas y size, que para este caso es sencillo.*)

-- "Javrodviv1,carvelcab"
lemma hojasize_igualdad: "hojas x = size x + 1"
by (induct x, simp_all)

(* lemma "es_abc size a <-> es_abc hojas a" Son equivalentes = es lo
   mismo que ⟷ matemáticamente hablando*)

lemma "es_abc size a = es_abc hojas a"
by (induct a, simp_all add: hojasize_igualdad)

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

(* jeshorcob: aquí similar*)

-- "jeshorcob"
lemma a2: 
  assumes "es_abc size a"
  shows "hojas a = (size a) + 1"
using assms 
by (induct a, simp_all)

-- "jeshorcob"
lemma chojas_cnodos: "es_abc hojas a = es_abc size a"
by (induct a, auto simp add: a2)

-- "jeshorcob"
lemma "es_abc hojas a = es_abc size a" (is "?P a")
proof (induct a)
  show "?P H" by simp
next
  fix i d
  assume h1: "?P i"
  assume h2: "?P d"
  have "es_abc hojas (N i d) = 
        (hojas i = hojas d ∧ es_abc hojas i ∧ es_abc hojas d )" by simp
  also have "… = (hojas i = hojas d ∧ es_abc size i ∧ es_abc size d)"
    using h1 and h2 by simp
  also have "... = (size i = size d ∧ es_abc size i ∧ es_abc size d)" 
    using a2 by auto
  also have "... = es_abc size (N i d)" by simp
  finally show "?P (N i d)" by simp 
qed

--"domcadgom"

lemma aux2: "es_abc size a ⟹ (hojas a = size a + 1)"
by (induct a, simp_all)

lemma completo2: "es_abc hojas a = es_abc (size) a"
proof (induct a, simp)
 fix a1 :: arbol and a2 :: arbol
  assume a1: "es_abc hojas a1 = es_abc size a1"
  assume a2: "es_abc hojas a2 = es_abc size a2"
  hence "es_abc size a2 ∧ es_abc size a1 ⟶ 
         es_abc hojas (N a1 a2) = es_abc size (N a1 a2)" 
    using a1 by (simp add: aux2)
  thus "es_abc hojas (N a1 a2) = es_abc size (N a1 a2)" 
    using a1 a2 es_abc.simps(2) by blast
qed 

-- "juacorvic"
(* número de hojas es size + 1 *)
lemma l_hojas_size: "hojas x = size x + 1"
proof (induct x)
  show " hojas H = size H + 1" by simp
next 
  fix x1 x2
  assume h1: "hojas x1 = size x1 + 1"
  assume h2:"hojas x2 = size x2 + 1"
  have "hojas (N x1 x2) =  hojas x1 + hojas x2" by simp
  also have "... = size x1 + 1 + size x2 + 1" using h1 h2 by simp
  also have "... =  (1 + size x1 + size x2) + 1" by simp
  also have "... = size (N x1 x2) + 1" by simp
  finally show  "hojas (N x1 x2) = size (N x1 x2) + 1" by simp 
qed

-- "juacorvic"
(* usando lema anterior *)
lemma rel_size_igualdad: " es_abc size  a = es_abc hojas a"
by (induct a, simp_all add: l_hojas_size)

--"davoremar"
lemma hojas_size_igualdad: "hojas x = size x + 1"
by (induct x) simp_all

-"davoremar"
lemma size_hojas: "es_abc size a = es_abc hojas a"
by (induct a) (simp_all add: hojas_size_igualdad)

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

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

(*jeshorcob: sale directo como corolario de los anteriores*)

--"jeshorcob,carvelcab"
lemma "es_abc pr1 a = es_abc size a"
using cpr1_chojas and chojas_cnodos by simp_all

-- "domcadgom"
corollary completo3: "es_abc profundidad a = es_abc size a"
 using completo1 completo2 by simp

--"juacorvic"
(* 1.- En apartado 7 se demuestra que:
          es_abc profundidad a ⟷ es_abc hojas a
   2.- En apartado 8 se demuestra que:
          es_abc hojas a ⟷ es_abc size  a 
   3.- Luego podremos demostrar usando las anteriores:
          es_abc profundidad a ⟷ es_abc size  a 

   Nota: Aplico demostración de "domcadgom" de apartado 7, que no he
   conseguido reproducir *)  

lemma "es_abc profundidad a = es_abc size a"
using completo1 rel_size_igualdad by simp_all

--"davoremar"
lemma "es_abc hojas a = es_abc size a"
using profundidad_hojas size_hojas[symmetric] by simp_all

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

-- "Pedrosrei"
lemma " es_abc f (abc n)"
apply (induct n, auto) 
done

-- "jeshorcob, davoremar, domcadgom, carvelcab, juacorvic"
lemma "es_abc f (abc n)"
by (induct n, simp_all)

-- "jeshorcob"
lemma "es_abc f (abc n)" (is "?P n")
proof (induct n)
  show "?P 0" by simp
next
  fix n assume h: "?P n"
  have "es_abc f (abc (Suc n)) = es_abc f (N (abc n) (abc n))" by simp
  also have "... = (f (abc n) = f (abc n) ∧ 
                   es_abc f (abc n) ∧ es_abc f (abc n))" by simp
  also have "... = True" using h by simp
  finally show "?P (Suc n)" by simp
qed

-- "juacorvic"
(* Más detallada *)
lemma "es_abc f (abc n)"
proof (induct n)
  show " es_abc f (abc 0)" by simp
next
  fix n 
  assume h1: "es_abc f (abc n)"
  have "es_abc f (abc (Suc n)) = es_abc f (N (abc n) (abc n))" by simp
  also have "... = (es_abc f (abc n) ∧ es_abc f (abc n) ∧ 
                    (f (abc n) = f (abc n)))" by simp
  also have "... = (f (abc n) = f (abc n) )" using h1 by simp
  also have "... = True " by simp
  finally show "es_abc f (abc n) ⟹ es_abc f (abc (Suc n))" 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)).
  --------------------------------------------------------------------- 
*}

--"Pedrosrei:"
lemma "es_abc profundidad a ⟹ (a = abc (profundidad a))"
apply (induct a, auto) 
done

-- "jeshorcob"
lemma "es_abc pr1 a ⟹ (a = abc (pr1 a))"
by (induct a, simp_all)

--"davoremar, domcadgom"
lemma "es_abc profundidad a ⟹ (a = abc (profundidad a))"
by (induct a, simp_all)

--"juacorvic"
lemma "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).
  --------------------------------------------------------------------- 
*}

--"Pedrosrei:"
lemma "es_abc f = es_abc nodos"
quickcheck
oops

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

(* jeshorcob: usando size en lugar de nodos, se encuentra el mismo
   contraejemplo. *) 
--"jeshorcob, domcadgom"
lemma "es_abc f = es_abc size"
quickcheck
oops

(*
el contraejemplo es:

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

Evaluated terms:
es_abc f x = True
es_abc size x = False
*)

-- "davoremar"
lemma "es_abc f t = es_abc size t"
quickcheck
oops

-- "juacorvic"
fun medida :: "arbol => nat" where
  "medida H = 0"
| "medida (N i d) = 0"

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

(*Contraejemplo
value "es_abc medida (N H (N H H))" (*devuelve true*)
value "es_abc size (N H (N H H))"   (*devuelve false*)
*)

end