Examen 2 - Historial de revisiones

Jalonso en 15:08 26 jun 2019

2019-06-26T15:08:46Z

Jalonso en 15:35 13 jun 2019

2019-06-13T15:35:53Z

Jalonso en 17:42 12 jun 2019

2019-06-12T17:42:22Z

Jalonso en 15:20 12 jun 2019

2019-06-12T15:20:57Z

Página nueva

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

@@ Línea 366: / Línea 366: @@
    qed
 qed
 end

@@ Línea 1: / Línea 1: @@
 <source lang="isabelle">
 chapter {* Examen de Lógica Matemática y Fundamentos (6 junio 2019) *}
 text {*
@@ Línea 262: / Línea 275: @@
    show "?P H" by (simp only: nHojas.simps(1) nNodos.simps(1))
 next
-   fix x i d
+   fix x :: 'a and
-  assume HI1: "?P i"
+      i :: "'a arbol" and
    assume HI2: "?P d"
    show "?P (N x i d)"

@@ Línea 1: / Línea 1: @@
 <source lang="isabelle">
-chapter {* Examen de Lógica Matemática y Fundamentos (6-junio-2919) *}
+chapter {* Examen de Lógica Matemática y Fundamentos (6 junio 2019) *}
-theory examen_2_06_jun_sol
+text {*
-imports Main
+  Nota: En las demostraciones se pueden  las reglas básicas de deducción
-begin
+  natural de la lógica proposicional, de los cuantificadores y de la
 text {* ---------------------------------------------------------------
@@ Línea 15: / Línea 59: @@
    ------------------------------------------------------------------ *}
-lemma ej1:
+(* La demostración declarativa es *)
-  shows "(p ⟶ q) ⟶ ((¬p ⟶ q) ⟶ q)"
+lemma "(p ⟶ q) ⟶ ((¬p ⟶ q) ⟶ q)"
 proof
    assume "p ⟶ q"
@@ Línea 33: / Línea 77: @@
    qed
 qed
 text {* ---------------------------------------------------------------
@@ Línea 175: / Línea 258: @@
 (* Demostración declarativa *)
-lemma ej3:
+lemma "nHojas a = (nNodos a) + 1" (is "?P a")
 proof (induct a)
    show "?P H" by (simp only: nHojas.simps(1) nNodos.simps(1))
@@ Línea 196: / Línea 278: @@
 (* Demostración aplicativa *)
-lemma ej3_b:
+lemma "nHojas a = (nNodos a) + 1"
    apply (induct a)
       (* 1. nHojas H = nNodos H + 1
@@ Línea 249: / Línea 330: @@
 begin
-lemma ej5:
+(* Una demostración declarativa es *)
-  shows "∀x. ∀y. x = y^ ⟶ y = x^"
+lemma "∀x. ∀y. x = y^ ⟶ y = x^"
 proof (rule allI)+
    fix a b
@@ Línea 263: / Línea 344: @@
      then have "b = a^ ⋅ 𝟭" by (simp only: inverso_i)
      then show "b = a^ " by (simp only: neutro_d)
    qed
 qed