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

2020-05-28T09:39:28Z

Protegió «T3 sol» ([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_sol imports Main begin text ‹ Apellidos: Nombr…»

2020-05-28T09:39:19Z

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

Página nueva

<source lang = "isabelle">

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

theory uvus_3_sol
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"

value "elimina 2 [a,c,d,b,e] = [d,b,e]"

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 1: 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 declarativa detallada›

lemma
"estaEn x (elimina n xs) ⟶ estaEn x xs"
proof (induct rule: elimina.induct)
fix n
show "estaEn x (elimina n []) ⟶ estaEn x []"
proof (rule impI)
assume "estaEn x (elimina n [])"
then show "estaEn x []"
by (simp only: elimina.simps(1))
qed
next
fix y ys
show "estaEn x (elimina 0 (y # ys)) ⟶ estaEn x (y # ys)"
proof (rule impI)
assume "estaEn x (elimina 0 (y # ys))"
then show "estaEn x (y # ys)"
by (simp only: elimina.simps(2))
qed
next
fix n y ys
assume 1: "estaEn x (elimina n ys) ⟶ estaEn x ys"
show "estaEn x (elimina (Suc n) (y # ys)) ⟶ estaEn x (y # ys)"
proof (rule impI)
assume "estaEn x (elimina (Suc n) (y # ys))"
then have "estaEn x (elimina n ys)"
by (simp only: elimina.simps(3))
with 1 have "estaEn x ys"
by (rule mp)
then have "y = x ∨ estaEn x ys"
by (rule disjI2)
then show "estaEn x (y # ys)"
by (simp only: estaEn.simps(2))
qed
qed

― ‹Demostración aplicativa detallada (1)›
lemma eliminaEsta:
"estaEn x (elimina n xs) ⟹ estaEn x xs"
apply (induct rule: elimina.induct)
apply (simp only: elimina.simps(1))
apply (simp only: elimina.simps(2) estaEn.simps(1))
apply (simp only: elimina.simps(3))
apply (simp only: estaEn.simps(2))
apply (rule disjI2)
apply (simp only: implies_True_equals)
done

lemma
"estaEn x (elimina n xs) ⟶ estaEn x xs"
apply (rule impI)
apply (simp only: eliminaEsta)
done

― ‹Demostración aplicativa detallada (2)›
lemma
"estaEn x (elimina n xs) ⟶ estaEn x xs"
apply (induct rule: elimina.induct)
apply (simp only: elimina.simps(1) estaEn.simps(1))
apply (rule impI, assumption)
apply (simp only: elimina.simps(2) estaEn.simps(1))
apply (rule impI, assumption)
apply (simp only: elimina.simps(3))
apply (simp only: estaEn.simps(2))
apply (rule impI)
apply (rule disjI2)
apply (erule mp, assumption)
done

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)))
--------------------------------------------------------------------›

― ‹Demostración declarativa detallada›
lemma
"(∃y z. ((∀x. ¬R(x, y)) ∨ (∀x. ¬R(x, z))))
⟶ ¬ (∀y z. ∃x. (R(x,y) ∧ R(x,z)))"
proof (rule impI)
assume 0: "∃y z. ((∀x. ¬R(x, y)) ∨ (∀x. ¬R(x, z)))"
show "¬ (∀y z. ∃x. (R(x,y) ∧ R(x,z)))"
proof (rule notI)
assume 1: "∀y. ∀z. ∃x. (R(x,y) ∧ R(x,z))"
obtain b where "∃z. ((∀x. ¬R(x, b)) ∨ (∀x. ¬R(x, z)))"
using 0 by (rule exE)
then obtain c where 2: "((∀x. ¬R(x, b)) ∨ (∀x. ¬R(x, c)))"
by (rule exE)
have "∀z. ∃x. (R(x,b) ∧ R(x,z))"
using 1 by (rule allE)
then have "∃x. (R(x,b) ∧ R(x,c))"
by (rule allE)
then obtain a where 3 :"R(a,b) ∧ R(a,c)"
by (rule exE)
show False
using 2
proof (rule disjE)
assume "∀x. ¬ R (x, b)"
then have "¬R(a,b)"
by (rule allE)
have "R(a,b)"
using 3 by (rule conjunct1)
with `¬R(a,b)` show False
by (rule notE)
next
assume "∀x. ¬ R (x, c)"
then have "¬R(a,c)"
by (rule allE)
have "R(a,c)"
using 3 by (rule conjunct2)
with `¬R(a,c)` show False
by (rule notE)
qed
qed
qed

― ‹Demostración aplicativa detallada›
lemma
"(∃y z. ((∀x. ¬R(x,y)) ∨ (∀x. ¬R(x,z))))
⟶ ¬( ∀y z. ∃x. (R(x,y) ∧ R(x,z)))"
apply (rule impI)
apply (rule notI)
apply (erule exE)+
apply (erule_tac x = y in allE)
apply (erule_tac x = z in allE)
apply (erule disjE)
apply (erule exE)
apply (erule_tac x = x in allE)
apply (erule notE)
apply (erule conjunct1)
apply (erule exE)
apply (erule_tac x = x in allE)
apply (erule notE)
apply (erule conjunct2)
done

end
</source>

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

T3 sol - Historial de revisiones

Mjoseh: Protegió «T3 sol» ([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_sol imports Main begin text ‹ Apellidos: Nombr…»