theory examen_2_jul_sol
imports Main
begin
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.
---------------------------------------------------------------------›
― ‹Formalización y demostración›
― ‹Formalización:›
lemma
assumes "(∀x. M(x) ⟶ C(x)) ⟶ (∀y. (T(y) ∧ N(y)) ⟶ B(y))"
"(∃x. M(x) ∧ C(x)) ⟶ (∀x. M(x) ⟶ C(x) ∧ P(x))"
"∀x. G(x) ⟶ M(x)"
"∀y. ¬N(y) ⟶ ¬D(y)"
shows "(∀y. T y ⟶ D y) ∧ (∃x. G x ∧ C x) ⟶ (∀z. T z ⟶ B z)"
oops
― ‹Auxiliar›
lemma previo:
assumes "∀x. M(x) ⟶ C(x) ∧ P(x)"
shows "∀x. M(x) ⟶ C(x)"
proof (rule allI)
fix a
show "M(a) ⟶ C(a)"
proof (rule impI)
assume "M(a)"
have "M(a) ⟶ C(a) ∧ P(a)" using assms by (rule allE)
then have "C(a) ∧ P(a)" using ‹M(a)› by (rule mp)
then show "C(a)" by (rule conjunct1)
qed
qed
― ‹Demostración declarativa detallada:›
lemma
assumes "(∀x. M(x) ⟶ C(x)) ⟶ (∀y. (T(y) ∧ N(y)) ⟶ B(y))"
"(∃x. M(x) ∧ C(x)) ⟶ (∀x. M(x) ⟶ C(x) ∧ P(x))"
"∀x. G(x) ⟶ M(x)"
"∀y. ¬N(y) ⟶ ¬D(y)"
shows "(∀y. T y ⟶ D y) ∧ (∃x. G x ∧ C x) ⟶ (∀z. T z ⟶ B z)"
proof (rule impI)
assume 1: "(∀y. T(y) ⟶ D(y)) ∧ (∃x. G(x) ∧ C(x))"
show "∀z. T(z) ⟶ B(z)"
proof (rule allI)
fix a
show "T(a) ⟶ B(a)"
proof (rule impI)
assume "T(a)"
show "B(a)"
proof -
have "∀y. T(y) ⟶ D(y)" using 1 by (rule conjunct1)
then have "T(a) ⟶ D(a)" by (rule allE)
then have "D(a)" using `T(a)` by (rule mp)
then have "¬¬D(a)" by (rule notnotI)
have "¬N(a)⟶¬D(a)" using assms(4) by (rule allE)
then have "¬¬N(a)" using `¬¬D(a)` by (rule mt)
then have "N(a)" by (rule notnotD)
have "∃x. G(x) ∧ C(x)" using 1 by (rule conjunct2)
then obtain b where "G(b) ∧ C(b)" by (rule exE)
then have "G(b)" by (rule conjunct1)
have "C(b)" using `G(b) ∧ C(b)` by (rule conjunct2)
have "G(b) ⟶ M(b)" using assms(3) by (rule allE)
then have "M(b)" using `G(b)` by (rule mp)
then have "M(b) ∧ C(b)" using `C(b)` by (rule conjI)
then have "∃x. M(x) ∧ C(x)" by (rule exI)
with assms(2) have "∀x. M(x) ⟶ C(x) ∧ P(x)" by (rule mp)
then have "∀x. M(x) ⟶ C(x)" by (rule previo)
with assms(1) have "∀y. (T(y) ∧ N(y)) ⟶ B(y)" by (rule mp)
then have "(T(a) ∧ N(a))⟶B(a)" by (rule allE)
have "T(a) ∧ N(a)" using `T(a)` `N(a)` by (rule conjI)
with `(T(a) ∧ N(a)) ⟶ B(a)` show "B(a)" by (rule mp)
qed
qed
qed
qed
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"
― ‹Auxiliares:›
lemma sublistaMono: "sublista xs ys ⟹ sublista xs (y#ys)"
apply (induct xs)
apply (simp only: sublista.simps(1))
apply (simp only: sublista.simps(2))
apply (rule conjI)
apply (erule conjE)
apply (simp only: estaEn.simps(2))
apply (rule disjI2)
apply (simp only: implies_True_equals)+
done
lemma estaEn1: "estaEn x (x#xs)"
apply (simp only: estaEn.simps(2))
apply (rule disjI1)
apply (rule refl)
done
lemma sublistaReflexiva: "sublista xs xs"
apply (induct xs)
apply (simp only: sublista.simps(1))
apply (simp only: sublista.simps(2))
apply (rule conjI)
apply (rule estaEn1)
apply (rule sublistaMono, assumption)
done
― ‹Demostración declarativa detallada:›
lemma eliminaSublista_dec: "sublista (elimina n xs) xs"
proof (induct rule: elimina.induct)
fix n
show "sublista (elimina n []) []"
by (simp only: elimina.simps(1) sublista.simps(1))
next
fix x :: "'a" and xs :: "'a list"
show "sublista (elimina 0 (x # xs)) (x # xs)"
by (simp only: elimina.simps(2) sublistaReflexiva)
next
fix n and x :: "'a" and xs :: "'a list"
show "sublista (elimina n xs) xs ⟹
sublista (elimina (Suc n) (x # xs)) (x # xs)"
by (simp only: elimina.simps(3) sublistaMono)
qed
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
― ‹Auxiliar para una implicación:›
lemma inverso_d:
"x ⋅ x^ = 𝟭"
proof -
have "x ⋅ x^ = 𝟭 ⋅ (x ⋅ x^)"
by (simp only: neutro_i)
also have "… = (𝟭 ⋅ x) ⋅ x^"
by (simp only: asociativa)
also have "… = (((x^)^ ⋅ x^) ⋅ x) ⋅ x^"
by (simp only: inverso_i)
also have "… = ((x^)^ ⋅ (x^ ⋅ x)) ⋅ x^"
by (simp only: asociativa)
also have "… = ((x^)^ ⋅ 𝟭) ⋅ x^"
by (simp only: inverso_i)
also have "… = (x^)^ ⋅ (𝟭 ⋅ x^)"
by (simp only: asociativa)
also have "… = (x^)^ ⋅ x^"
by (simp only: neutro_i)
also have "… = 𝟭"
by (simp only: inverso_i)
finally show ?thesis
by this
qed
lemma
assumes "((y^ ⋅ x^) ⋅ y) ⋅ x = 𝟭"
shows "x ⋅ y = y ⋅ x"
proof -
have "x ⋅ y = (x ⋅ y) ⋅ 𝟭"
by (rule neutro_d [THEN sym])
also have "… = (x ⋅ y) ⋅ (((y^ ⋅ x^) ⋅ y) ⋅ x)"
using assms by (rule arg_cong [THEN sym])
also have "… = (x ⋅ ((y ⋅ y^) ⋅ x^) ⋅ y) ⋅ x"
by (simp only: asociativa)
also have "… = ((x ⋅ (𝟭 ⋅ x^)) ⋅ y) ⋅ x"
by (simp only: inverso_d)
also have "… = (x ⋅ ((𝟭 ⋅ x^) ⋅ y)) ⋅ x "
by (simp only: asociativa)
also have "… = (x ⋅ (x^ ⋅ y)) ⋅ x"
by (simp only: neutro_i)
also have "… = ((x ⋅ x^) ⋅ y) ⋅ x"
by (simp only: asociativa)
also have "… = (𝟭 ⋅ y) ⋅ x"
by (simp only: inverso_d)
also have "… = 𝟭 ⋅ (y ⋅ x)"
by (simp only: asociativa)
also have "… = y ⋅ x"
by (simp only: neutro_i)
finally show "x ⋅ y = y ⋅ x"
by this
qed
― ‹Recíproco:›
lemma
assumes "x ⋅ y = y ⋅ x"
shows "((y^ ⋅ x^) ⋅ y) ⋅ x = 𝟭"
proof -
have "y ⋅ x = x ⋅ y" using assms by (rule sym)
then have "x^ ⋅ (y ⋅ x) = x^ ⋅ (x ⋅ y)" by (rule arg_cong)
then have "y^ ⋅ (x^ ⋅ (y ⋅ x)) =y^ ⋅ (x^ ⋅ (x ⋅ y))" by (rule arg_cong)
then have "((y^ ⋅ x^) ⋅ y) ⋅ x =y^ ⋅ ((x^ ⋅ x) ⋅ y)"
by (simp only: asociativa)
also have "... = y^ ⋅ (𝟭 ⋅ y)" by (simp only: inverso_i)
also have "... = y^ ⋅ y " by (simp only: neutro_i)
also have "... = 𝟭" by (simp only: inverso_i)
finally show "((y^ ⋅ x^) ⋅ y) ⋅ x = 𝟭" by this
qed
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"
― ‹Lemas auxiliares:›
lemma r_subset_rst: "r x y ⟹ rst r x y"
by (simp only: refl1 trans1)
lemma r_subset_rst_b: "r x y ⟹ rst r y x"
by (simp only: refl1 trans2)
lemma rst_sc1_declarativo: "rst r x y ⟹ r y z ⟹ rst r x z"
proof (induct rule:rst.induct)
case (refl1 x)
then show ?case by (rule r_subset_rst)
next
case (trans1 x y z)
then show ?case by (simp only: rst.trans1)
next
case (trans2 y x z)
then show ?case by (simp only: rst.trans2)
qed
lemma rst_sc2_declarativo: "rst r z y ⟹ r x y ⟹ rst r z x"
proof (induct rule:rst.induct)
case (refl1 x)
then show ?case by (rule r_subset_rst_b)
next
case (trans1 x y z)
then show ?case by (simp only: rst.trans1)
next
case (trans2 y x z)
then show ?case by (simp only: rst.trans2)
qed
― ‹Demostración declarativa detallada:›
lemma rstSimetrica_declarativa: "rst r x y ⟹ rst r y x"
proof (induct rule: rst.induct)
fix x
show "rst r x x" by (rule refl1)
next
fix x y z
assume "r x y" and "rst r y z" and "rst r z y"
then show "rst r z x" by (simp only: rst_sc2_declarativo)
next
fix x y z
assume "r y x" and "rst r y z" and "rst r z y"
then show "rst r z x" by (simp only: rst_sc1_declarativo)
qed
end
![Lógica matemática y fundamentos [Curso 2019-20]](/~jalonso/imagenes/logoUS.jpg)