Examen 2
De Lógica matemática y fundamentos (2018-19)
Revisión del 17:20 12 jun 2019 de Jalonso (discusión | contribuciones)
chapter {* Examen de Lógica Matemática y Fundamentos (6-junio-2919) *}
theory examen_2_06_jun_sol
imports Main
begin
text {* ---------------------------------------------------------------
Ejercicio 1. (2.5 puntos) Demostrar detalladamente que la siguiente
fórmula es una tautología:
(p ⟶ q) ⟶((¬p ⟶ q) ⟶ q)
Nota: No usar ninguno de los métodos automáticos: simp, simp_all,
auto, blast, force, fast, arith o metis
------------------------------------------------------------------ *}
lemma ej1:
shows "(p ⟶ q) ⟶ ((¬p ⟶ q) ⟶ q)"
proof
assume "p ⟶ q"
show "(¬p ⟶ q) ⟶ q"
proof
assume "¬p ⟶ q"
have "¬p ∨ p" by (rule excluded_middle)
then show "q"
proof (rule disjE)
assume "¬p"
with `¬p ⟶ q` show q by (rule mp)
next
assume "p"
with `p ⟶ q` show q by (rule mp)
qed
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 2. (2.5 puntos) Demostrar detalladamente que si R es una
relación irreflexiva y transitiva, entonces R es antisimétrica.
{ ∀x. ¬R(x,x),
∀x. ∀y. ∀z. (R(x,y) ∧ R(y,z) ⟶ R(x,z)) }
⊢ ∀x. ∀y. (R(x,y) ⟶ ¬R(y,x))
Nota: No usar ninguno de los métodos automáticos: simp, simp_all,
auto, blast, force, fast, arith o metis
------------------------------------------------------------------ *}
(* La demostración declarativa es *)
lemma
assumes "∀x. ¬R(x,x)"
"∀x. ∀y. ∀z. (R(x,y) ∧ R(y,z) ⟶ R(x,z))"
shows "∀x. ∀y. (R(x,y) ⟶ ¬ R(y,x))"
proof
fix a
show "∀y. (R(a,y) ⟶ ¬R(y,a))"
proof
fix b
show "R(a,b) ⟶ ¬R(b,a)"
proof
assume "R(a,b)"
show "¬ R(b,a)"
proof
assume "R(b,a)"
then have "R(b,a) ∧ R(a,b)" using `R(a,b)` by (rule conjI)
have "∀y. ∀z.(R(b,y) ∧ R(y,z) ⟶ R(b,z))"
using assms(2) by (rule allE)
then have "∀z.(R(b,a) ∧ R(a,z) ⟶ R(b,z))" by (rule allE)
then have "R(b,a) ∧ R(a,b) ⟶ R(b,b)" by (rule allE)
then have "R(b,b)" using `R(b,a) ∧ R(a,b)` by (rule mp)
have "¬R(b,b)" using assms(1) by (rule allE)
then show False using `R(b,b)` by (rule notE)
qed
qed
qed
qed
(* La demostración aplicativa es *)
lemma
"⟦ ∀x. ¬R(x,x);
∀x. ∀y. ∀z. (R(x,y) ∧ R(y,z) ⟶ R(x,z))⟧
⟹ ∀x. ∀y. (R(x,y) ⟶ ¬ R(y,x))"
apply (rule allI)+
(* ⋀x y. ⟦ ∀x. ¬ R (x, x);
∀x y z. R (x, y) ∧ R (y, z) ⟶ R (x, z)⟧
⟹ R (x, y) ⟶ ¬ R (y, x)*)
apply (rule impI)
(* ⋀x y. ⟦ ∀x. ¬ R (x, x);
∀x y z. R (x, y) ∧ R (y, z) ⟶ R (x, z);
R (x, y)⟧
⟹ ¬ R (y, x) *)
apply (rule notI)
(* ⋀x y. ⟦ ∀x. ¬ R (x, x);
∀x y z. R (x, y) ∧ R (y, z) ⟶ R (x, z);
R (x, y);
R (y, x)⟧
⟹ False *)
apply (erule_tac x=x in allE)
(* ⋀x y. ⟦ ∀x y z. R (x, y) ∧ R (y, z) ⟶ R (x, z);
R (x, y);
R (y, x);
¬ R (x, x)⟧
⟹ False *)
apply (erule_tac x=x in allE)
(* ⋀x y. ⟦ R (x, y);
R (y, x);
¬ R (x, x);
∀y z. R (x, y) ∧ R (y, z) ⟶ R (x, z)⟧
⟹ False *)
apply (erule_tac x=y in allE)
(* ⋀x y. ⟦ R (x, y);
R (y, x);
¬ R (x, x);
∀z. R (x, y) ∧ R (y, z) ⟶ R (x, z)⟧
⟹ False *)
apply (erule_tac x=x in allE)
(* ⋀x y. ⟦ R (x, y);
R (y, x);
¬ R (x, x);
R (x, y) ∧ R (y, x) ⟶ R (x, x)⟧
⟹ False *)
apply (erule notE)
(* ⋀x y. ⟦ R (x, y);
R (y, x);
R (x, y) ∧ R (y, x) ⟶ R (x, x)⟧
⟹ R (x, x) *)
apply (drule mp)
(* 1. ⋀x y. ⟦R (x, y); R (y, x)⟧ ⟹ R (x, y) ∧ R (y, x)
2. ⋀x y. ⟦R (x, y); R (y, x); R (x, x)⟧ ⟹ R (x, x) *)
apply (rule conjI)
(* 1. ⋀x y. ⟦R (x, y); R (y, x)⟧ ⟹ R (x, y)
2. ⋀x y. ⟦R (x, y); R (y, x)⟧ ⟹ R (y, x)
3. ⋀x y. ⟦R (x, y); R (y, x); R (x, x)⟧ ⟹ R (x, x)*)
apply assumption+
(* *)
done
text {*
---------------------------------------------------------------------
Ejercicio 3 (2.5 puntos) Consideremos el árbol binario definido por
datatype 'a arbol = H | N "'a" "'a arbol" "'a arbol"
Por ejemplo, el árbol
e
/ \
/ \
c g
/ \ / \
se representa por "N e (N c H H) (N g H H)".
Definir las funciones
nNodos :: "'a arbol ⇒ nat"
nHojas :: "'a arbol ⇒ nat"
tales que
+ (nNodos a) es el número de nodos de a. Por ejemplo,
nNodos (N e (N c H H) (N g H H)) = 3
+ (nHojas a) es el número de hojas de a. Por ejemplo,
nHojas (N e (N c H H) (N g H H)) = 4
Demostrar detalladamente que el número de hojas de un árbol es igual
al número de nodos más 1.
Nota: Los únicos métodos que se pueden usar son induct,
(simp only: ...) o this.
------------------------------------------------------------------- *}
datatype 'a arbol = H | N "'a" "'a arbol" "'a arbol"
fun nNodos :: "'a arbol ⇒ nat" where
"nNodos H = 0"
| "nNodos (N x i d) = 1 + (nNodos i) + (nNodos d)"
fun nHojas :: "'a arbol ⇒ nat" where
"nHojas H = 1"
| "nHojas (N x i d) = (nHojas i) + (nHojas d)"
(* Demostración declarativa *)
lemma ej3:
"nHojas a = (nNodos a) + 1" (is "?P a")
proof (induct a)
show "?P H" by (simp only: nHojas.simps(1) nNodos.simps(1))
next
fix x i d
assume HI1: "?P i"
assume HI2: "?P d"
show "?P (N x i d)"
proof -
have "nHojas (N x i d) = (nHojas i) + (nHojas d)"
by (simp only: nHojas.simps(2))
also have "... = (nNodos i + 1) + (nNodos d + 1)"
by (simp only: HI1 HI2)
also have "... = (nNodos (N x i d)) + 1"
by (simp only: nNodos.simps(2))
finally show "?P (N x i d)" by this
qed
qed
(* Demostración aplicativa *)
lemma ej3_b:
"nHojas a = (nNodos a) + 1"
apply (induct a)
(* 1. nHojas H = nNodos H + 1
2. ⋀x1 a1 a2. ⟦ nHojas a1 = nNodos a1 + 1;
nHojas a2 = nNodos a2 + 1⟧
⟹ nHojas (N x1 a1 a2) =
nNodos (N x1 a1 a2) + 1 *)
apply (simp only: nHojas.simps(1))
(* 1. 1 = nNodos H + 1
2. ⋀x1 a1 a2. ⟦ nHojas a1 = nNodos a1 + 1;
nHojas a2 = nNodos a2 + 1⟧
⟹ nHojas (N x1 a1 a2) = nNodos (N x1 a1 a2) + 1 *)
apply (simp only: nNodos.simps(1))
(* ⋀x1 a1 a2. ⟦ nHojas a1 = nNodos a1 + 1;
nHojas a2 = nNodos a2 + 1⟧
⟹ nHojas (N x1 a1 a2) =
nNodos (N x1 a1 a2) + 1 *)
apply (simp only: nHojas.simps(2))
(* ⋀x1 a1 a2. ⟦ nHojas a1 = nNodos a1 + 1;
nHojas a2 = nNodos a2 + 1⟧
⟹ nNodos a1 + 1 + (nNodos a2 + 1) =
nNodos (N x1 a1 a2) + 1 *)
apply (simp only: nNodos.simps(2))
(* *)
done
text {* ---------------------------------------------------------------
Ejercicio 4. (2.5 puntos) Sea G un grupo. Domostrar detalladamente que
para todo par de elementos x e y de G, si x es el inverso de y,
entonces y es el inverso de 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 ej5:
shows "∀x. ∀y. x = y^ ⟶ y = x^"
proof (rule allI)+
fix a b
show "a = b^ ⟶ b = a^"
proof
assume "a = b^"
then have "a^ ⋅ a = a^ ⋅ b^" by simp
then have "𝟭 = a^ ⋅ b^" by (simp only: inverso_i)
then have "𝟭 ⋅ b = (a^ ⋅ b^) ⋅ b" by simp
then have "b = (a^ ⋅ b^) ⋅ b" by (simp only: neutro_i)
then have "b = a^ ⋅ (b^ ⋅ b)" by (simp only: asociativa)
then have "b = a^ ⋅ 𝟭" by (simp only: inverso_i)
then show "b = a^ " by (simp only: neutro_d)
qed
qed
end
end