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