T5-1

text ‹Ejercicio 5 de Lógica Matemática y Fundamentos (2-junio-2020)›

theory ej_2_jun
imports Main 
begin

text ‹
  Apellidos:
  Nombre: 
› 

text ‹Sustituye la palabra ej_2_jun por tu usuario de la Universidad de
  Sevilla y graba el fichero con dicho usuario.thy› 

text ‹Nota 1: El tiempo de realización del ejercicio, incluida su
   entrega en la PEV, es de 15:30 a 17:30.› 

text ‹Nota 2: Además de las reglas básicas de deducción natural de la 
  lógica proposicional y de primer orden, también se pueden usar las 
  reglas notnotI y mt que demostramos a  continuación.›

text ‹Nota 3: En el proceso de corrección del ejercicio, y antes de la
  publicación de las calificaciones del mismo, se podrá requerir
  aclaraciones sobre su respuesta. Estas aclaraciones se harán por 
  alguno de los procedimientos virtuales previstos en la PEV. ›

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
  -------------------------------------------------------------------›

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"

― ‹Lema nHojasAux›

― ‹Demostración en lenguaje natural›

― ‹Demostración detallada de nHojasAux›

lemma nHojasAux:
  "nHojasAaux a n = (nHojas a) + n"
  oops

― ‹Demostraciones de nHojasA›

― ‹Demostración en lenguaje natural›

― ‹Demostración detallada›

theorem nHojasA:
  "nHojasA a = nHojas a"
  oops

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

― ‹Demostración detallada›

lemma
  "x = y^ ⋅ z ⟷ z = y  ⋅ x" 
  oops

end

end