Demostración automática de teoremas (2014-15) Demostración automática de teoremas (2014-15)

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