T3

text ‹Ejercicio 3 de Lógica Matemática y Fundamentos (19-mayo-2020)›

theory uvus_3
imports Main 
begin

text ‹
  Apellidos:
  Nombre: 
› 

text ‹Sustituye la palabra uvus 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 es de 15:30 a 17:00.
  A continuación, se dispone de 30 minutos para su entrega en la PEV.› 

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 ‹------------------------------------------------------------------
  Se define la función
     elimina :: nat ⇒ 'a list ⇒ 'a list
  tal que (elimina n xs) es la lista obtenida eliminando los n primeros
  elementos de xs. Por ejemplo, 
     elimina 2 [a,c,d,b,e] = [d,b,e]
  ---------------------------------------------------------------------›

fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
  "elimina n []             = []"
| "elimina 0 xs             = xs"
| "elimina (Suc n) (x # xs) = elimina n xs"

text ‹------------------------------------------------------------------ 
  Se define la función
     estaEn :: 'a ⇒ 'a list ⇒ bool
  tal que (estaEn x xs) se verifica si el elemento x está en la lista
  xs. Por ejemplo, 
     estaEn (2::nat) [3,2,4] = True
     estaEn (1::nat) [3,2,4] = False
  ---------------------------------------------------------------------›

fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
  "estaEn x []       = False"
| "estaEn x (a # xs) = (a = x ∨ estaEn x xs)"

text ‹------------------------------------------------------------------
  Ejercicio: Demostrar que
     estaEn x (elimina n xs) ⟶ estaEn x xs

  + En lenguaje natural
  + En Isabelle/HOL, de forma detallada. Es opcional hacerlo de forma
    declarativa o aplicativa.

  Nota: Es recomendable pasar de la demostración en lenguaje natural a la 
  demostración estructurada. Y, a continuación, detallar los pasos de 
  simplificación hasta llegar a usar sólo el método (simp only:..).
 ----------------------------------------------------------------------›

― ‹Demostración en lenguaje natural

›

― ‹Demostración detallada›

lemma 
  "estaEn x (elimina n xs) ⟶ estaEn x xs"
  oops

text ‹------------------------------------------------------------------ 
  Ejercicio 2. Demostrar que si la relación binaria R verifica la 
  siguiente condición
     ∃y z. (∀x. ¬R(x, y)) ∨ (∀x. ¬R(x, z)))
  entonces no se verifica que
    ∀y z. ∃x. (R(x,y) ∧ R(x,z)))

  Nota: Hacer la demostración de forma detallada. Es opcional hacerla 
  de forma declarativa o aplicativa.
  --------------------------------------------------------------------›

― ‹Demostración detallada›
lemma 
  "(∃y z. ((∀x. ¬R(x, y)) ∨ (∀x. ¬R(x, z))))
  ⟶ ¬ (∀y z. ∃x. (R(x,y) ∧ R(x,z)))"
  oops
end