T5-2 sol

theory ej_2jun_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 preOrden :: "'a arbol ⇒ 'a list" where
       "preOrden H         = []"
     | "preOrden (N x i d) = x#(preOrden i)@(preOrden d)"

     fun preOrdenAaux :: "'a arbol ⇒ 'a list ⇒ 'a list" where
       "preOrdenAaux H         xs = xs"
     | "preOrdenAaux (N x i d) xs = (preOrdenAaux d (preOrdenAaux i (xs@[x])))"

     definition preOrdenA :: "'a arbol ⇒ 'a list" where
       "preOrdenA a ≡ preOrdenAaux a []"
  tales que 
  + (preOrden a) es el recorrido post orden del árbol a. Por
    ejemplo, 
       preOrden (N e (N c H H) (N g H H)) = [c, g, e]
  + (preOrdenA a) es el recorrido post orden del árbol a, calculado 
    con la función auxiliar preOrdenAaux que usa un acumulador. Por 
    ejemplo, 
       preOrdenA (N e (N c H H) (N g H H)) = [c, g, e]
 
  Demostrar detalladamente que las funciones postOrden y postOrdenA son
  equivalentes; es decir,
     preOrdenA a = preOrden 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 preOrden :: "'a arbol ⇒ 'a list" where
  "preOrden H         = []"
| "preOrden (N x i d) = x#(preOrden i)@(preOrden d)"

fun preOrdenAaux :: "'a arbol ⇒ 'a list ⇒ 'a list" where
  "preOrdenAaux H         xs = xs"
| "preOrdenAaux (N x i d) xs = (preOrdenAaux d (preOrdenAaux i (xs@[x])))"

definition preOrdenA :: "'a arbol ⇒ 'a list" where
  "preOrdenA a ≡ preOrdenAaux a []"

section ‹Demostraciones del lema preOrdenAux›

subsection ‹Demostración estructurada de preOrdenAux›

lemma preOrdenAuxE:
  "preOrdenAaux a xs = xs @ preOrden a"
proof (induct a arbitrary: xs)
  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 preOrdenAux›

lemma preOrdenAuxA:
  "preOrdenAaux a xs = xs @ preOrden a"
  by (induct a arbitrary: xs) simp_all

subsection ‹Demostración declarativa detallada de preOrdenAux›

lemma append_unitaria:
  "[x] @ ys = x # ys" 
proof -
  have "[x] @ ys = x # ([] @ ys)"
    by (simp only: append.simps(2))
  also have "… = x # ys"
    by (simp only: append.simps(1))
  finally show "[x] @ ys = x # ys"
    by this
qed

lemma preOrdenAux:
  "preOrdenAaux a xs = xs @ preOrden a"
proof (induct a arbitrary: xs) 
  fix xs :: "'a list"
  have "preOrdenAaux H xs = xs" 
    by (simp only: preOrdenAaux.simps(1))
  also have "… = xs @ []"
    by (simp only: append_Nil2)
  also have "… = xs @ preOrden H" 
    by (simp only: preOrden.simps(1))
  finally show "preOrdenAaux H xs = xs @ preOrden H" 
    by this 
next  
  fix x :: "'a" and i d :: "'a arbol" and xs :: "'a list"
  assume HI1: "⋀xs. preOrdenAaux i xs = xs @ preOrden i" 
    and  HI2: "⋀xs. preOrdenAaux d xs = xs @ preOrden d"
  have "preOrdenAaux (N x i d) xs = 
        preOrdenAaux d (preOrdenAaux i (xs @ [x]))" 
    by (simp only: preOrdenAaux.simps(2))
  also have "… = preOrdenAaux d ((xs @ [x]) @ (preOrden i))" 
    by (simp only: HI1)      
  also have "… = ((xs @ [x]) @ (preOrden i)) @ (preOrden d)"
    by (simp only: HI2) 
  also have "… = xs @ ([x] @ preOrden i @ preOrden d)"
    by (simp only: append.assoc)       
  also have "… = xs @ (x # preOrden i @ preOrden d)"
    by (simp only: append_unitaria)
  also have "… = xs @ (preOrden (N x i d))"
    by (simp only: preOrden.simps(2))
  finally show "preOrdenAaux (N x i d) xs = 
                xs @ preOrden (N x i d)" 
    by this
qed

section ‹Demostraciones de preOrdenA›

subsection ‹Demostración automática de preOrdenA›

theorem preOrdenA_A:
  "preOrdenA a = preOrden a"
  by (simp add: preOrdenA_def preOrdenAux)

subsection ‹Demostración declarativa detallada de preOrdenA›

theorem preOrdenA:
  "preOrdenA a = preOrden a"
proof -
  have "preOrdenA a = preOrdenAaux a []" 
    by (simp only: preOrdenA_def)
  also have "… = [] @ (preOrden a)"
    by (simp only: preOrdenAux)
  also have "... = preOrden a"
    by (simp only: append.simps(1))
  finally show "preOrdenA a = preOrden a"
    by this
    qed

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

  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

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

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

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

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

end
    
end