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

2020-09-10T08:18:50Z

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

Mjoseh: Página creada con « text ‹Examen de Lógica Matemática y Fundamentos (9-septiembre-2020)› theory examen_9_sep imports Main begin text ‹ Apellidos: Nomb…»

2020-09-10T08:18:36Z

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

Página nueva

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

theory examen_9_sep
imports Main
begin

text ‹
Apellidos:
Nombre:
›

text ‹Sustituye la palabra examen_9_sep 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.›

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

text ‹------------------------------------------------------------------
Ejercicio 1. (2.5 puntos) 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:
Ningún individuo que sea candidato será derrotado si hace una
buena campaña. Todo individuo que se postula es un candidato. Cualquier
candidato que no sea derrotado, será elegido. Todo individuo que sea
elegido hace una buena campaña. Por tanto, todo individuo que se
postula será elegido si y sólo si hace una buena campaña.

Simbología: I(x): x es individuo, C(x): x es candidato,
D(x): x es derrotado, B(x): x hace una buena campaña,
P(x): x se postula, E(x): x es elegido.
---------------------------------------------------------------------›

text ‹ -----------------------------------------------------------------
Ejercicio 2. (2.5 puntos) Consideramos la función
menores :: int ⇒ int list ⇒ bool
tal que (menores a xs) es la lista de los elementos de la lista xs que
son menores que a. Por ejemplo,
value "menores 2 [3,0,1] = [0,1]"
value "menores 2 [3,0,5] = [0]"

fun menores :: "int ⇒ int list ⇒ int list" where
"menores a [] = []"
| "menores a (x#xs) = (if x < a then x # (menores a xs)
else (menores a xs))"

Demostrar que la longitud de la lista de elementos menores que uno
dado es menor o igual que la longitud de la lista original.
-----------------------------------------------------------------------›

fun menores :: "int ⇒ int list ⇒ int list" where
"menores a [] = []"
| "menores a (x#xs) = (if x < a then x # (menores a xs)
else (menores a xs))"

value "menores 2 [3,0,1] = [0,1]"
value "menores 2 [3,0,5] = [0]"

lemma menores_menor:
"length (menores x xs) < 1 + (length xs)"
oops

text ‹------------------------------------------------------------------
Ejercicio 3. (2.5 puntos) Sea G un grupo. Demostrar que si se verifica
∀x y. (((y^ ⋅ x^) ⋅ y) ⋅ x = 𝟭), entonces también se verifica
∀x. ∀y. ∀z. x ⋅ y = z ⋅ x ⟶ y = z

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_d: "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 = z ⋅ x ⟶ y = z"
oops

end

text ‹-----------------------------------------------------------------
Ejercicio 4. (2.5 puntos) El conjunto de los conjuntos finitos
se define inductivamente por
inductive_set Finito :: "'a set set"
where
vacioI: "{} ∈ Finito" |
insertaI: "A ∈ Finito ⟹ insert a A ∈ Finito"

Demostrar detalladamente que la unión de dos conjuntos finitos es
finito; es decir.
⟦ A ∈ Finito; B ∈ Finito ⟧ ⟹ A ∪ B ∈ Finito

Nota: Los únicos métodos que se pueden usar son induct y
(simp only: ...).
---------------------------------------------------------------------›

inductive_set Finito :: "'a set set"
where
vacioI: "{} ∈ Finito" |
insertaI: "A ∈ Finito ⟹ insert a A ∈ Finito"

lemma "⟦ A ∈ Finito; B ∈ Finito ⟧ ⟹ A ∪ B ∈ Finito"
oops

end

</source>

← Revisión anterior	Revisión del 08:18 10 sep 2020
(Sin diferencias)

Examen 2C - Historial de revisiones

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

Mjoseh: Página creada con « text ‹Examen de Lógica Matemática y Fundamentos (9-septiembre-2020)› theory examen_9_sep imports Main begin text ‹ Apellidos: Nomb…»