Ver el código de «Tema 13: Razonamiento modular (I): Teoría de grupos.» - Demostración automática de teoremas (2014-15)

<source lang = "isabelle">
header {* T13: Razonamiento modular (I). La teoría de grupos *}

theory T13
imports Main
begin

text {*
  El objetivo de este tema es mostrar cómo se puede trabajar en
  estructuras algebraicas por medio de contextos 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, el 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

</source>