header {* T12a: Razonamiento modular. La teoría de grupos *}
theory T12a_Razonamiento_modular_Teoria_de_grupos
imports Main
begin
text {*
El objetivo de este tema es mostrar cómo se puede trabajar en
estructuras algebraicas por medio de locales. Se usará como ejemplo la
teoría de grupos. *}
text {*
Ejemplo 1. Un grupo es una estructura (G,·,𝟭,^) tal que G es un
conjunto, · es una operación binaria en G, 𝟭 es un elemento de G y ^
es una función de G en G tales que se cumplen las siguientes
propiedades:
* asociativa: ∀x y z. x ⋅ (y ⋅ z) = (x ⋅ y) ⋅ z
* neutro por la izquierda: ∀x. 𝟭 ⋅ x = x
* inverso por la izquierda: ∀x. x^ ⋅ x = 𝟭
Definir el entorno axiomático de los grupos. *}
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 inverso_i: "x^ ⋅ x = 𝟭"
text {*
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 con pulsando 2 veces en ^. *}
text {*
A continuación se crea un contexto en el que se supone la notación y
axiomas de grupos. En el contexto se demuestran propiedades de los
grupos. *}
context grupo
begin
text {*
Ejemplo 2. En los grupos, x^ también es el inverso de x por la
derecha; es decir
x ⋅ x^ = 𝟭 *}
-- "La demostración automática (obtenida con Sledgehammer) es"
lemma inverso_d:
"x ⋅ x^ = 𝟭"
by (metis asociativa inverso_i neutro_i)
-- "La demostración detallada es"
lemma inverso_d_2:
"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 .
qed
text {*
Ejemplo 2. En los grupos, 𝟭 también es el neutro por la derecha; es decir
x ⋅ 𝟭 = x *}
-- "La demostración automática es (obtenida con Sledgehammer) es"
lemma neutro_d:
"x ⋅ 𝟭 = x"
by (metis asociativa inverso_i neutro_i)
-- "La demostración detallada es"
lemma neutro_d_2:
"x ⋅ 𝟭 = x"
proof -
have "x ⋅ 𝟭 = x ⋅ (x^ ⋅ x)" by (simp only: inverso_i)
also have "… = (x ⋅ x^) ⋅ x" by (simp only: asociativa)
also have "… = 𝟭 ⋅ x" by (simp only: inverso_d)
also have "… = x" by (simp only: neutro_i)
finally show "x ⋅ 𝟭 = x" .
qed
text {*
Ejemplo 3. En los grupos, se tiene la propiedad cancelativa por la
izquierda; es decir,
x ⋅ y = x ⋅ z syss y = z *}
-- "La demostración automática es (obtenida con Sledgehammer) es"
lemma cancelativa_i:
"(x ⋅ y = x ⋅ z) = (y = z)"
by (metis asociativa inverso_i neutro_i)
-- "La demostración detallada es"
lemma cancelativa_i_2:
"(x ⋅ y = x ⋅ z) = (y = z)"
proof
assume "x ⋅ y = x ⋅ z"
hence "x^ ⋅ (x ⋅ y) = x^ ⋅ (x ⋅ z)" by simp
hence "(x^ ⋅ x) ⋅ y = (x^ ⋅ x) ⋅ z" by (simp only: asociativa)
hence "𝟭 ⋅ y = 𝟭 ⋅ z" by (simp only: inverso_i)
thus "y = z" by (simp only: neutro_i)
next
assume "y = z"
then show "x ⋅ y = x ⋅ z" by simp
qed
text {*
Ejemplo 4. En los grupos, el elemento neutro por la izquierda es
único; es decir, si e es un elemento tal que para todo x se tiene que
e ⋅ x = x, entonces e = 𝟭. *}
-- "La demostración automática es (obtenida con Sledgehammer) es"
lemma unicidad_neutro_i:
assumes "e ⋅ x = x"
shows "𝟭 = e"
using assms
by (metis asociativa inverso_i neutro_i)
-- "La demostración estructurada es"
lemma unicidad_neutro_i_2:
assumes "e ⋅ x = x"
shows "𝟭 = e"
proof -
have "𝟭 = x ⋅ x^" by (simp only: inverso_d)
also have "... = (e ⋅ x) ⋅ x^" using assms by simp
also have "... = e ⋅ (x ⋅ x^)" by (simp only: asociativa)
also have "... = e ⋅ 𝟭" by (simp only: inverso_d)
also have "... = e" by (simp only: neutro_d)
finally show ?thesis .
qed
text {*
Ejemplo 5. En los grupos, los inversos por la izquierda son únicos; es
decir, si x' es un elemento tal que x' ⋅ x = 𝟭, entonces x^ x'. *}
-- "La demostración automática es (obtenida con Sledgehammer) es"
lemma unicidad_inverso_i:
assumes "x' ⋅ x = 𝟭"
shows "x^ = x'"
using assms
by (metis asociativa inverso_i neutro_i)
-- "La demostración estructurada es"
lemma unicidad_inverso_i_2:
assumes "x' ⋅ x = 𝟭"
shows "x^ = x'"
proof -
have "x^ = 𝟭 ⋅ x^" by (simp only: neutro_i)
also have "... = (x' ⋅ x) ⋅ x^" using assms by simp
also have "... = x' ⋅ (x ⋅ x^)" by (simp only: asociativa)
also have "... = x' ⋅ 𝟭" by (simp only: inverso_d)
also have "... = x'" by (simp only: neutro_d)
finally show ?thesis .
qed
text {*
Ejemplo 6. En los grupos, es inverso de un producto es el producto de
los inversos cambiados de orden; es decir,
(x ⋅ y)^ = y^ ⋅ x^ *}
-- "La demostración automática es (obtenida con Sledgehammer) es"
lemma inversa_producto:
"(x ⋅ y)^ = y^ ⋅ x^"
by (metis asociativa inverso_i neutro_i)
-- "La demostración estructurada es"
lemma inversa_producto_2:
"(x ⋅ y)^ = y^ ⋅ x^"
proof (rule unicidad_inverso_i)
show "(y^ ⋅ x^) ⋅ (x ⋅ y) = 𝟭"
proof -
have "(y^ ⋅ x^) ⋅ (x ⋅ y) = (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_d)
also have "... = 𝟭" by (simp only: inverso_i)
finally show ?thesis .
qed
qed
text {*
Ejemplo 7. En los grupos, el inverso del inverso es el propio
elemento; es decir,
(x^)^ = x *}
-- "La demostración automática es (obtenida con Sledgehammer) es"
lemma inverso_inverso:
"(x^)^ = x"
by (metis inverso_d unicidad_inverso_i)
-- "La demostración estructurada es"
lemma inverso_inverso_2:
"(x^)^ = x"
proof (rule unicidad_inverso_i)
show "x ⋅ x^ = 𝟭" by (simp only: inverso_d)
qed
text {*
Ejemplo 8. En los grupos, la función inversa es inyectiva; es decir,
si x e y tienen los mismos inversos, entonces son iguales. *}
-- "La demostración automática es (obtenida con Sledgehammer) es"
lemma inversa_inyectiva:
assumes "x^ = y^"
shows "x = y"
using assms
by (metis inverso_inverso)
-- "La demostración automática estructurada es"
lemma inversa_inyectiva_2:
assumes "x^ = y^"
shows "x = y"
proof -
have "(x^)^ = (y^)^" using assms by simp
thus "x = y" by (simp only: inverso_inverso)
qed
end
end
