Mjoseh: Protegió «T3» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

2020-05-28T09:38:36Z

Protegió «T3» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Mjoseh: Página creada con « text ‹Ejercicio 3 de Lógica Matemática y Fundamentos (19-mayo-2020)› theory uvus_3 imports Main begin text ‹ Apellidos: Nombre:…»

2020-05-28T09:38:25Z

Página creada con «<source lang = "isabelle"> text ‹Ejercicio 3 de Lógica Matemática y Fundamentos (19-mayo-2020)› theory uvus_3 imports Main begin text ‹ Apellidos: Nombre:…»

Página nueva

<source lang = "isabelle">
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
</source>

← Revisión anterior	Revisión del 09:38 28 may 2020
(Sin diferencias)

T3 - Historial de revisiones

Mjoseh: Protegió «T3» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Mjoseh: Página creada con « text ‹Ejercicio 3 de Lógica Matemática y Fundamentos (19-mayo-2020)› theory uvus_3 imports Main begin text ‹ Apellidos: Nombre:…»