T4

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

theory uvus
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, incluida su
   entrega en la PEV, es de 15:30 a 16:30.› 

text ‹Nota 2: El segundo ejercicio se realizará de 16:00 a 17:00,
  estando disponible desde la PEV a partir de las 17:00 .› 

text ‹Nota 3: 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 4: 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 ‹------------------------------------------------------------------
  Ejercicio. Demostrar que 
     length (elimina n xs) ≤ length xs
  ---------------------------------------------------------------------›

― ‹Demostración en lenguaje natural

›

― ‹Demostración detallada›

lemma  "length (elimina n xs) ≤ length xs"
oops


text ‹------------------------------------------------------------------ 
  Ejercicio 2. Demostrar que si se verifica 
     ∀x. (P x ⟶ (∃y. Q y))
  entonces se verifica 
     ∀x. ∃y. (P x ⟶ Q y)

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

― ‹Demostración detallada›

lemma 
  fixes P Q :: "'b ⇒ bool" 
  assumes "∀x. (P x ⟶ (∃y. Q y))"
  shows   "∀x. ∃y. (P x ⟶ Q y)"
  oops

end