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

2020-07-06T12:32:54Z

Protegió «Examen 1C» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Mjoseh: Página creada con « text ‹Examen de Lógica Matemática y Fundamentos (2-julio-2020)› theory examen_2_jul imports Main begin text ‹ Apellidos: Nombre:…»

2020-07-06T12:32:42Z

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

Página nueva

<source lang = "isabelle">
text ‹Examen de Lógica Matemática y Fundamentos (2-julio-2020)›

theory examen_2_jul
imports Main
begin

text ‹
Apellidos:
Nombre:
›

text ‹Sustituye la palabra examen_2_jul 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 9:30 a 11:30.›

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 examen, 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 ‹------------------------------------------------------------------
Ejercicio 1. Demostrar detalladamente con Isabelle, sin usar métodos
automáticos (como simp, auto, ...) sino sólo las reglas básicas,
que el siguiente argumento es correcto
Si todas las medicinas están contaminadas, entonces todos los
técnicos negligentes son unos bribones. Si hay medicinas
contaminadas, entonces todas las medicinas están contaminadas y son
peligrosas. Todos los germicidas son medicinas. Sólo los
negligentes son distraídos. Por tanto, si cualquier técnico es
distraído y si algunos germicidas están contaminados, los técnicos
son bribones.
Usar la siguiente simbología:
M(x): x es medicina, C(x): x está contaminada,
T(x): x es técnico, N(x): x es un negligente,
B(x): x es un bribón, G(x): x es germicida,
D(x): x es distraído, P(x): x es peligrosa.
---------------------------------------------------------------------›

text ‹------------------------------------------------------------------
Ejercicio 2. Se consideran las definiciones de las siguientes
funciones (que se dan a continuación)
estaEn :: 'a ⇒ 'a list ⇒ bool
sublista :: "'a list ⇒ 'a list ⇒ bool
elimina :: nat ⇒ 'a list ⇒ 'a list
tales 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
+ (sublista xs ys) se verifica si todos los elementos de la lista xs
están en la lista ys. Por ejemplo,
sublista [(1::nat),2,3] [3,2,1,2] = True
sublista [(1::nat),2,3] [2,1,2] = False
+ (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]

Demostrar detalladamente que
sublista (elimina n xs) xs
---------------------------------------------------------------------›

fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
"estaEn x [] = False"
| "estaEn x (a#xs) = (a=x ∨ estaEn x xs)"

fun sublista :: "'a list ⇒ 'a list ⇒ bool" where
"sublista [] ys = True"
| "sublista (x#xs) ys = (estaEn x ys ∧ sublista xs ys )"

fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina n [] = []"
| "elimina 0 xs = xs"
| "elimina (Suc n) (x#xs) = elimina n xs"

lemma eliminaSublista: "sublista (elimina n xs) xs"
oops

text ‹------------------------------------------------------------------
Ejercicio 3. Sea G un grupo. Demostrar que las siguientes condiciones
son equivalentes:
(+) G es commutativo, es decir, ∀x y. (x ⋅ y = y ⋅ x)
(+) ∀x y. (((y^ ⋅ x^) ⋅ y) ⋅ x = 𝟭)

Nota: No usar ninguno de los métodos automáticos: auto, blast, force,
fast, arith o metis
------------------------------------------------------------------ ›

locale grupo =
fixes prod :: "['a, 'a] ⇒ 'a" (infixl "⋅" 70)
and neutro ("𝟭")
and inverso ("_^" [100] 100)
assumes asociativa: "(x ⋅ y) ⋅ z = x ⋅ (y ⋅ z)"
and neutro_i: "𝟭 ⋅ x = x"
and neutro_d: "x ⋅ 𝟭 = x"
and inverso_i: "x^ ⋅ x = 𝟭"

(* Notas sobre notación:
* El producto es ⋅ y se escribe con \ cdot (sin espacio entre ellos).
* El neutro es 𝟭 y se escribe con \ y one (sin espacio entre ellos).
* El inverso de x es x^ y se escribe pulsando 2 veces en ^. *)

context grupo
begin

lemma
assumes "((y^ ⋅ x^) ⋅ y) ⋅ x = 𝟭"
shows "x ⋅ y = y ⋅ x"
oops

lemma
assumes "x ⋅ y = y ⋅ x"
shows "((y^ ⋅ x^) ⋅ y) ⋅ x = 𝟭"
oops

end

text ‹------------------------------------------------------------------
Ejercicio 4. Se define la clausura reflexiva, simétrica y transitiva
de una relación binaria r como sigue:
inductive rst :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool"
for r where
refl1: "rst r x x"
| trans1: "r x y ⟹ rst r y z ⟹ rst r x z"
| trans2: "r y x ⟹ rst r y z ⟹ rst r x z"

Demostrar detalladamente que la relación (rst es r) simétrica.
---------------------------------------------------------------------›

inductive rst :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool"
for r where
refl1: "rst r x x"
| trans1: "r x y ⟹ rst r y z ⟹ rst r x z"
| trans2: "r y x ⟹ rst r y z ⟹ rst r x z"

lemma rst_es_simetrica : "rst r x y ⟹ rst r y x"
oops

end

</source>

← Revisión anterior	Revisión del 12:32 6 jul 2020
(Sin diferencias)

Examen 1C - Historial de revisiones

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

Mjoseh: Página creada con « text ‹Examen de Lógica Matemática y Fundamentos (2-julio-2020)› theory examen_2_jul imports Main begin text ‹ Apellidos: Nombre:…»