![Lógica matemática y fundamentos [Curso 2019-20]](/~jalonso/imagenes/logoUS.jpg)
Diferencia entre revisiones de «T4»
De Lógica matemática y fundamentos [Curso 2019-20]
(Página creada con «<source lang = "isabelle"> theory T4_sol imports Main begin lemma notnotI: "P ⟹ ¬¬ P" by auto lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F" by auto text ‹-----------…») |
m (Protegió «T4» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))) |
||
| (No se muestran 2 ediciones intermedias del mismo usuario) | |||
| Línea 1: | Línea 1: | ||
<source lang = "isabelle"> | <source lang = "isabelle"> | ||
| − | theory | + | text ‹Ejercicio 4 de Lógica Matemática y Fundamentos (26-mayo-2020)› |
| + | |||
| + | theory uvus | ||
imports Main | imports Main | ||
begin | 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" | lemma notnotI: "P ⟹ ¬¬ P" | ||
| Línea 10: | Línea 35: | ||
by auto | by auto | ||
| − | text ‹----------------------------------------------------------------- | + | text ‹------------------------------------------------------------------ |
Se define la función | Se define la función | ||
elimina :: nat ⇒ 'a list ⇒ 'a list | elimina :: nat ⇒ 'a list ⇒ 'a list | ||
| Línea 25: | Línea 50: | ||
text ‹------------------------------------------------------------------ | text ‹------------------------------------------------------------------ | ||
Ejercicio. Demostrar que | Ejercicio. Demostrar que | ||
| − | length (elimina n xs) ≤ length xs | + | length (elimina n xs) ≤ length xs |
---------------------------------------------------------------------› | ---------------------------------------------------------------------› | ||
| − | ― | + | ― ‹Demostración en lenguaje natural |
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | + | › | |
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | ― | + | ― ‹Demostración detallada› |
lemma "length (elimina n xs) ≤ length xs" | lemma "length (elimina n xs) ≤ length xs" | ||
| − | + | oops | |
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
text ‹------------------------------------------------------------------ | text ‹------------------------------------------------------------------ | ||
Ejercicio 2. Demostrar que si se verifica | Ejercicio 2. Demostrar que si se verifica | ||
| Línea 250: | Línea 73: | ||
--------------------------------------------------------------------› | --------------------------------------------------------------------› | ||
| − | ― ‹Demostración | + | ― ‹Demostración detallada› |
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
lemma | lemma | ||
| − | + | fixes P Q :: "'b ⇒ bool" | |
| − | + | assumes "∀x. (P x ⟶ (∃y. Q y))" | |
| − | + | shows "∀x. ∃y. (P x ⟶ Q y)" | |
| − | + | oops | |
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | |||
| − | end | + | end |
| − | </ | + | </source> |
Revisión actual del 11:33 1 jun 2020
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