T5-1 sol

theory ej_2_jun_sol
imports Main 
begin

lemma notnotI: "P ⟹ ¬¬ P"
  by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

text ‹-----------------------------------------------------------------
  Ejercicio 1. Consideremos el árbol binario definido por
     datatype 'a arbol = H  
                       | N "'a" "'a arbol" "'a arbol"
  
  Por ejemplo, el árbol
          e
         / \
        /   \
       c     g
      / \   / \
             
  se representa por "N e (N c H H) (N g H H)".

  Se define las funciones
    fun nHojas :: "'a arbol ⇒ nat" where
      "nHojas H         = 1"
    | "nHojas (N x i d) = nHojas i + nHojas d"

    fun nHojasAaux :: "'a arbol ⇒ nat ⇒ nat" where
      "nHojasAaux H         n = n + 1"
    | "nHojasAaux (N x i d) n = nHojasAaux i (nHojasAaux d n)"

    definition nHojasA :: "'a arbol ⇒ nat" where
      "nHojasA a ≡ nHojasAaux a 0"
  tales que
  + (nHojas a) es el número de hojas del árbol a. Por ejemplo, 
       nHojas (N e (N c H H) (N g H H)) = 4
  + (nHojasAA a) es el número de hojas del árbol a, calculado 
    con la función auxiliar nHojasAaux que el el segundo argumento va
    acumulando el resultado. Por ejemplo, 
       nHojasA (N e (N c H H) (N g H H)) = 4
 
  Demostrar detalladamente que las funciones nHojas y nHojasA son
  equivalentes; es decir,
     nHojasA a = nHojas a

  Nota: Los únicos métodos que se pueden usar son induct y simp. 
  -------------------------------------------------------------------›

section ‹Definiciones›

datatype 'a arbol = H  
                  | N "'a" "'a arbol" "'a arbol"

fun nHojas :: "'a arbol ⇒ nat" where
  "nHojas H         = 1"
| "nHojas (N x i d) = nHojas i + nHojas d"

fun nHojasAaux :: "'a arbol ⇒ nat ⇒ nat" where
  "nHojasAaux H         n = n + 1"
| "nHojasAaux (N x i d) n = nHojasAaux i (nHojasAaux d n)"

definition nHojasA :: "'a arbol ⇒ nat" where
  "nHojasA a ≡ nHojasAaux a 0"

value "nHojas (N e (N c H H) (N g H H)) = 4"
value "nHojasA (N e (N c H H) (N g H H)) = 4"

section ‹Demostraciones del lema auxiliar nHojasAux›

subsection ‹Demostración estructurada de nHojasAux›

lemma nHojasAuxE:
  "nHojasAaux a n = nHojas a + n"
proof (induct a arbitrary: n)
  case H
  then show ?case by simp
next
  case (N x1 a1 a2)
  then show ?case by simp
qed

subsection ‹Demostración automática de nHojasAux›

lemma nHojasAuxA:
  "nHojasAaux a n = nHojas a + n"
  by (induct a arbitrary: n) simp_all

subsection ‹Demostración declarativa detallada de nHojasAux›

lemma nHojasAux:
  "nHojasAaux a n = (nHojas a) + n"
proof (induct a arbitrary: n)
  fix n
  have "nHojasAaux H n = n + 1" 
    by (simp only: nHojasAaux.simps(1))
  also have "… = nHojas H + n" 
    by (simp only:nHojas.simps(1))
  finally show "nHojasAaux H n = nHojas H + n" 
    by this
next
  fix x :: 'a and i d :: "'a arbol" and n :: nat
  assume HI1: "⋀n. nHojasAaux i n = nHojas i + n"
    and HI2: "⋀n. nHojasAaux d n = nHojas d + n"
  have "nHojasAaux (N x i d) n = nHojasAaux i (nHojasAaux d n)" 
    by (simp only: nHojasAaux.simps(2))
  also have "… = nHojasAaux i (nHojas d + n)" 
    by (simp only: HI2)
  also have "… = nHojas i + (nHojas d + n)" 
    by (simp only: HI1)
  also have "… = (nHojas i + nHojas d) + n"
    by (simp only: add.commute)
  also have "… = nHojas (N x i d) + n" 
    by (simp only: nHojas.simps(2))
  finally show "nHojasAaux (N x i d) n = nHojas (N x i d) + n"  
    by this
qed

section ‹Demostraciones del teorema nHojasA›

subsection ‹Demostración automática de nHojasA›

theorem nHojasA_A:
  "nHojasA a = nHojas a"
  by (simp add: nHojasA_def nHojasAux)

subsection "Demostración declarativa detallada de nHojasA"

theorem nHojasA:
  "nHojasA a = nHojas a"
proof -
  have "nHojasA a = nHojasAaux a 0" 
    by (simp only: nHojasA_def)
  also have "… = nHojas a + 0"
    by (simp only: nHojasAux)
  also have "... = nHojas a"
    by (simp only: add_0_right)
  finally show "nHojasA a = nHojas a"
    by this
qed

text ‹------------------------------------------------------------------
  Ejercicio 2. Sea G un grupo. Demostrar detalladamente lo siguiente:
     x = y^ ⋅ z si y sólo si z = y ⋅ x

  Nota: No usar ninguno de los métodos automáticos: auto, blast, force,
  fast, arith o metis 
  ------------------------------------------------------------------ ›

locale grupo =
  fixes prod :: "['a, 'a] ⇒ 'a" (infixl "⋅" 70)
    and neutro ("𝟭") 
    and inverso ("_^" [100] 100)
  assumes asociativa: "(x ⋅ y) ⋅ z = x ⋅ (y ⋅ z)"
      and neutro_i:   "𝟭 ⋅ x = x"
      and neutro_d:   "x ⋅ 𝟭 = x"
      and inverso_i:  "x^ ⋅ x = 𝟭"

(* Notas sobre notación:
   * El producto es ⋅ y se escribe con \ cdot (sin espacio entre ellos). 
   * El neutro es 𝟭 y se escribe con \ y one (sin espacio entre ellos).
   * El inverso de x es x^ y se escribe pulsando 2 veces en ^. *)

context grupo
begin

section ‹Demostraciones de inverso_d›

subsection ‹Demostración automática de inverso_d›

lemma inverso_d_A:
  "x ⋅ x^ = 𝟭"
  by (metis asociativa neutro_i inverso_i)

subsection ‹Demostración declarativa detallada de inverso_d›

lemma inverso_d:
  "x ⋅ x^ = 𝟭"
proof -
  have "x ⋅ x^ = 𝟭 ⋅ (x ⋅ x^)" 
    by (simp only: neutro_i)
  also have "… = (𝟭 ⋅ x) ⋅ x^" 
    by (simp only: asociativa)
  also have "… = (((x^)^ ⋅ x^) ⋅ x) ⋅ x^" 
    by (simp only: inverso_i)
  also have "… = ((x^)^ ⋅ (x^ ⋅ x)) ⋅ x^" 
    by (simp only: asociativa)
  also have "… = ((x^)^ ⋅ 𝟭) ⋅ x^" 
    by (simp only: inverso_i)
  also have "… = (x^)^ ⋅ (𝟭 ⋅ x^)" 
    by (simp only: asociativa)
  also have "… = (x^)^ ⋅ x^" 
    by (simp only: neutro_i)
  also have "… = 𝟭" 
    by (simp only: inverso_i)
  finally show ?thesis 
    by this
qed

section ‹Demostraciones de condicion_necesaria›

subsection ‹Demostración automática de condicion_necesaria›

lemma condicion_necesaria_A:
  assumes "x = y^ ⋅ z" 
  shows   "z = y  ⋅ x" 
  using assms
  by (metis asociativa neutro_i inverso_d)

subsection ‹Demostración declarativa detallada de condicion_necesaria›

lemma condicion_necesaria:
  assumes "x = y^ ⋅ z" 
  shows   "z = y  ⋅ x" 
proof -
  have "y ⋅ x = y ⋅ (y^ ⋅ z)" 
    using assms(1)
    by (rule arg_cong)
  also have "… = (y ⋅ y^) ⋅ z" 
    by (simp only: asociativa)
  also have "… = 𝟭 ⋅ z" 
    by (simp only: inverso_d)
  also have "… = z" 
    by (simp only: neutro_i)
  finally have "y ⋅ x = z" 
    by this
  then show "z = y ⋅ x" 
    by (rule sym)
  qed

section ‹Demostraciones de condicion_suficiente›

subsection ‹Demostración automática de condicion_suficiente›

lemma condicion_suficiente_A:
  assumes "z = y  ⋅ x" 
  shows   "x = y^ ⋅ z" 
  using assms(1)
  by (metis asociativa neutro_i inverso_i)

subsection ‹Demostración declarativa detallada de condicion_suficiente›

lemma condicion_suficiente:
  assumes "z = y  ⋅ x" 
  shows   "x = y^ ⋅ z" 
proof -
  have  "y^ ⋅ z = y^ ⋅ (y ⋅ x)"
    using assms(1)
    by (rule arg_cong)
  also have "… =  (y^ ⋅ y) ⋅ x" 
    by (simp only: asociativa)
  also have "… = 𝟭 ⋅ x" 
    by (simp only: inverso_i)
  also have "… = x" 
    by (simp only: neutro_i)
  finally have "y^ ⋅ z = x" 
    by this
  then show  "x = y^ ⋅ z" 
    by (rule sym)
qed   

section ‹Demostraciones del teorema›

section ‹Demostraciones automática del teorema›

theorem condicion_necesaria_y_suficiente_A:
  "x = y^ ⋅ z ⟷ z = y  ⋅ x" 
  using condicion_necesaria  
        condicion_suficiente 
  by auto

section ‹Demostraciones declarativa detallada del teorema›

theorem condicion_necesaria_y_suficiente:
  "x = y^ ⋅ z ⟷ z = y  ⋅ x" 
proof (rule iffI)
  assume "x = y^ ⋅ z"
  then show "z = y ⋅ x"
    by (rule condicion_necesaria)
next
  assume "z = y ⋅ x"
  then show "x = y^ ⋅ z"
    by (rule condicion_suficiente)
qed

end

end