Menu Close

Autor: José A. Alonso

I1M2018: Razonamiento sobre programas

En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado cómo demostrar propiedades de programas Haskell.

Los tipos de razonamiento estudiado son

  • Razonamiento ecuacional sin variables.
  • Razonamiento ecuacional con variables.
  • Razonamiento ecuacional con análisis de casos
  • Razonamiento por inducción sobre los naturales
  • Razonamiento por inducción sobre listas.

En las demostraciones por inducción se ha destacado la elección de variables, las demostraciones anidadas y la generalización de propiedades para su prueba por inducción.

Los apuntes correspondientes a la clase son los del tema 8

Además, se ha mostrado cómo automatizar las demostraciones usando Isabelle/HOL.

I1M2018: Programación dinámica: Apilamiento de barriles

En la segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se han resuelto ejercicios de la relación 46, en el que se comparan distintas soluciones del problema del apilamiento de barriles. Se ha mostrado como transformar las definiciones recursivas en definiciones con programación dinámica. Además, se han comparado experimentalmente la eficiencia de las distintas definiciones.

Los ejercicios, y sus soluciones, se muestran a continuación.

I1M2018: El problema de las fichas mediante búsqueda en espacio de estado

En la segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticasse han resuelto ejercicios de la relación 44 en el que se aplican los patrones de busqueda en profundidad, en anchura, primero el mejor y en escalada para resolver el provlema de las fichas y comparar las soluciones obtenidas.

Los ejercicios y su solución se muestran a continuación

I1M2018: Búsquedas heurísticas en Haskell

En la la primera parte de la clase de hoy de del curso Informática de 1º del Grado en Matemáticas hemos estudiado la técnica de resolución de problemas mediante búsqueda en espacios de estados con heurísticas.

En primer lugar se estudió la búsqueda por primero el mejor, se implementó el patrón de búsqueda por primero el mejor y se aplicó el patrón para resolver el problema del 8 puzzle.

En segundó lugar se estudió la búsqueda en escalada, se implementó el patrón de búsqueda en escalada y se aplicó el patrón para resolver el el problema del cambio de monedas por escalada.

Finalmente, se estudió el algoritmo de Prim del árbol de expansión mínimo como un caso particular de búsqueda en escalada.

Los apuntes correspondientes a la clase son las secciones 3 y 4 del tema 23

LMF2018: Desarrollo de teorías formalizadas con Isabelle/HOL

En la clase de hoy del curso de Lógica matemática y fundamentos se ha estudiado cómo definir desarrollar en Isabelle/HOL teorías axiomáticas como las de monoides, semigrupos, grupos, órdenes y órdenes lineales.

La clase se ha basado en la siguiente teoría Isabelle

chapter {* T11: Desarrollo de teorías formalizadas *}
 
theory T11_Desarrollo_de_teorias_formalizadas
imports Main
begin
 
section {* Desarrollo de la teoría de grupos*}
 
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 "x ⋅ x^ = 𝟭"
  by (metis asociativa inverso_i neutro_i)
 
― ‹La demostración detallada es›
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 .
qed
 
text {*
  Ejemplo 2. En los grupos, 𝟭 también es el neutro por la derecha; es decir 
     x ⋅ 𝟭 = x   *}
 
― ‹La demostración automática (obtenida con Sledgehammer) es›
lemma "x ⋅ 𝟭 = x"
  by (metis asociativa inverso_i neutro_i)
 
― ‹La demostración detallada es›
lemma neutro_d: 
  "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 (obtenida con Sledgehammer) es›
lemma "(x ⋅ y = x ⋅ z) = (y = z)"
  by (metis asociativa inverso_i neutro_i)
 
― ‹La demostración detallada es›
lemma cancelativa_i: 
  "(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 
  assumes "e ⋅ x = x"
  shows "𝟭 = e"
  using assms
  by (metis asociativa inverso_d neutro_d)
 
― ‹La demostración estructurada es›
lemma unicidad_neutro_i:
  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 (obtenida con Sledgehammer) es›
lemma 
  assumes "x' ⋅ x = 𝟭"
  shows "x^ = x'"
  using assms
  by (metis asociativa inverso_i neutro_i)
 
― ‹La demostración estructurada es›
lemma unicidad_inverso_i:
  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 (obtenida con Sledgehammer) es›
lemma "(x ⋅ y)^ = y^ ⋅ x^"
  by (metis asociativa inverso_d neutro_d)
 
― ‹La demostración detallada es›
lemma inversa_producto:
  "(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 (obtenida con Sledgehammer) es›
lemma "(x^)^ = x"
  using inverso_d unicidad_inverso_i by blast
 
― ‹La demostración estructurada es›
lemma inverso_inverso: 
  "(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 
  assumes "x^ = y^"
  shows "x = y"
  using assms
  by (metis inverso_inverso)
 
― ‹La demostración automática estructurada es›
lemma inversa_inyectiva:
  assumes "x^ = y^"
  shows "x = y"
proof -
  have "(x^)^ = (y^)^" using assms by simp
  thus "x = y" by (simp only: inverso_inverso)
qed
 
end
 
section {* Teorías de órdenes mediante clases *}
 
text {*
  El tutorial sobre clases está en la teoría Clases.thy.
 
  La clase de los órdenes es la colección de los tipos que poseen una
  relación ≼ verificando las siguientes propiedades
  · reflexiva: x ≼ x
  · transitiva: ⟦x ≼ y; y ≼ z⟧ ⟹ x ≼ z
  · antisimétrica: ⟦x ≼ y; y ≼ x⟧ ⟹ x = y
*}
 
class orden = 
  fixes menor_ig :: "'a ⇒ 'a ⇒ bool"  (infix "≼" 50)
  assumes refl: "x ≼ x"
      and trans: "⟦x ≼ y; y ≼ z⟧ ⟹ x ≼ z"
      and antisim: "⟦x ≼ y; y ≼ x⟧ ⟹ x = y"
 
text {*
  Ha generado los teoremas correspondientes a los axiomas. Pueden 
  consultarse mediante thm como se muestra a continuación.
*}
 
thm trans
 
text {*
  Se inicia el contexto orden en el que se van a realizar definiciones y
  demostraciones. 
*}
 
context orden
begin
 
text {*
  x es menor que y si x es menor o igual que y y no son iguales.
*}
 
definition menor :: "'a ⇒ 'a ⇒ bool"  (infix "≺" 50)
  where "x ≺ y ⟷ x ≼ y ∧ ¬ y ≼ x"
 
text {*
    La relación menor es irreflexiva.
*}
 
lemma irrefl: "¬ x ≺ x"
  by (auto simp: menor_def)
 
text {*
  La relación menor es transitiva.
*}
 
(* Demostración aplicativa *)
lemma "⟦x ≺ y; y ≺ z⟧ ⟹ x ≺ z"
  apply (unfold menor_def)
    (* ⟦x ≼ y ∧ ¬ y ≼ x; y ≼ z ∧ ¬ z ≼ y⟧ ⟹ x ≼ z ∧ ¬ z ≼ x *)
  apply (auto intro: trans)
    (* *)
  done
 
(* Demostración automática *)
lemma menor_trans: "⟦x ≺ y; y ≺ z⟧ ⟹ x ≺ z"
  by (auto simp: menor_def intro: trans)
 
text {*
  La relación menor es asimétrica; es decir, si x ≺ y e y ≺ x, entonces
  se verifica cualquier propiedad P. 
*}
 
lemma asimetrica: "x ≺ y ⟹ y ≺ x ⟹ P"
  by (simp add: menor_def)
 
end
 
subsection {* Subclase *}
 
text {*
  Un orden lineal es un orden en que cada par de elementos son comparables.
*}
 
class ordenLineal = orden +
  assumes lineal: "x ≼ y ∨ y ≼ x"
begin
 
text {*
  En los órdenes lineales se tiene que x ≺ y ∨ x = y ∨ y ≺ x.
*}
 
(* Demostración aplicativa *)
lemma "x ≺ y ∨ x = y ∨ y ≺ x"
  apply (unfold menor_def)
      (* (x ≼ y ∧ ¬ y ≼ x) ∨ x = y ∨ (y ≼ x ∧ ¬ x ≼ y) *)
  apply auto
      (*  1. ⟦x ≠ y; ¬ x ≼ y⟧ ⟹ y ≼ x
          2. ⟦x ≠ y; y ≼ x; x ≼ y⟧ ⟹ False *)
   apply (cut_tac x=x and y=y in lineal)
      (* 1. ⟦x ≠ y; ¬ x ≼ y; x ≼ y ∨ y ≼ x⟧ ⟹ y ≼ x
         2. ⟦x ≠ y; y ≼ x; x ≼ y⟧ ⟹ False *)
   apply (erule disjE)
      (* 1. ⟦x ≠ y; ¬ x ≼ y; x ≼ y⟧ ⟹ y ≼ x
         2. ⟦x ≠ y; ¬ x ≼ y; y ≼ x⟧ ⟹ y ≼ x
         3. ⟦x ≠ y; y ≼ x; x ≼ y⟧ ⟹ False *)
    apply (erule_tac P="x ≼ y" in notE)
      (* 1. ⟦x ≠ y; x ≼ y⟧ ⟹ x ≼ y
         2. ⟦x ≠ y; ¬ x ≼ y; y ≼ x⟧ ⟹ y ≼ x
         3. ⟦x ≠ y; y ≼ x; x ≼ y⟧ ⟹ False *)
    apply assumption
      (* 1. ⟦x ≠ y; ¬ x ≼ y; y ≼ x⟧ ⟹ y ≼ x
         2. ⟦x ≠ y; y ≼ x; x ≼ y⟧ ⟹ False *)
   apply assumption
      (* 1. ⟦x ≠ y; y ≼ x; x ≼ y⟧ ⟹ False *)
  apply (drule antisim)
      (* 1. ⟦x ≠ y; x ≼ y⟧ ⟹ x ≼ y
         2. ⟦x ≠ y; x ≼ y; y = x⟧ ⟹ False *)
   apply assumption
      (* 1. ⟦x ≠ y; x ≼ y; y = x⟧ ⟹ False *)
  apply (erule notE)
      (* 1. ⟦x ≼ y; y = x⟧ ⟹ x = y *)
  apply (erule sym)
      (* *)
  done
 
(* Demostración automática *)
lemma "x ≺ y ∨ x = y ∨ y ≺ x"
  using antisim lineal menor_def by auto
 
end
 
section {* Teoría de órdenes mediante ámbitos ("Locales") *}
 
text {*
  Un orden es una estructura con una relación reflexiva, transitiva y
  antisimétrica. 
*}
 
locale Orden =
  fixes menor_ig :: "'a ⇒ 'a ⇒ bool"  (infix "⊑" 50)
  assumes refl:    "x ⊑ x"
      and trans:   "⟦x ⊑ y; y ⊑ z⟧ ⟹ x ⊑ z"
      and antisim: "⟦x ⊑ y; y ⊑ x⟧ ⟹ x = y"
 
text {*
    Los teoremas se diferencian por el nombre y el ámbito. Por ejemplo,
    refl: ?x ≼ ?x
    Orden.refl: Orden ?menor_ig ⟹ ?menor_ig ?x ?x
    Orden_def: Orden ?menor_ig ≡
               (∀x. ?menor_ig x x) ∧
               (∀x y z. ?menor_ig x y ⟶ ?menor_ig y z ⟶ ?menor_ig x z) ∧
               (∀x y. ?menor_ig x y ⟶ ?menor_ig y x ⟶ x = y)
*}
 
thm refl
thm Orden.refl
thm Orden_def
 
text {*
  Un orden lineal es un orden en el que todos los pares de elementos son 
  comparables. 
*}
 
locale OrdenLineal = Orden +
  assumes lineal: "x ⊑ y ∨ y ⊑ x"
 
text {*
  Los boooleanos está ordenados con el condicional.
*}
 
interpretation Orden_imp: Orden "λx y. x ⟶ y"
proof
  fix P show "P ⟶ P" by simp
next
  fix P Q R show "P ⟶ Q ⟹ Q ⟶ R ⟹ P ⟶ R" by simp
next
  fix P Q show "P ⟶ Q ⟹ Q ⟶ P ⟹ P = Q" by blast
qed
 
text {*
  Los naturales con la relación de divisibilidad es un conjunto ordenado.
*}
 
interpretation Orden_dvd: Orden "(dvd) :: nat ⇒ nat ⇒ bool"
proof 
  fix x :: nat
  show "x dvd x" by simp
next
  fix x y z :: nat
  show "⟦x dvd y; y dvd z⟧ ⟹ x dvd z" by auto 
next
  fix x y :: nat
  show "⟦x dvd y; y dvd x⟧ ⟹ x = y" by auto
qed
 
text {*
  Ámbito de las funciones monótonas (ver la página 12 del tutorial de
  locales). 
*}
 
locale Mono =
  le1: Orden le1 +
  le2: Orden le2 
    for le1 (infix "⊑⇩1" 50) and le2 (infix "⊑⇩2" 50) +
  fixes f :: "'a ⇒ 'b"
  assumes mono: "x ⊑⇩1 y ⟹ f(x) ⊑⇩2 f(y)"
 
text {*
  Si f es monótona, x ⊑_1 y e y ⊑_1 z, entonces f(x) ⊑_2 f(z).
*}
 
lemma (in Mono) mono_trans: 
  assumes "x ⊑⇩1 y" and "y ⊑⇩1 z" 
  shows "f(x) ⊑⇩2 f(z)"
proof -
  have "x ⊑⇩1 z" using assms and le1.trans by blast
  then show "f(x) ⊑⇩2 f(z)" using mono by simp
qed
 
text {*
  El teorema generado se llama Mono.mono_trans.
*}
 
thm Mono.mono_trans
 
text {*
  En el contexto Mono el nombre es mono_trans.
*}
 
context Mono 
begin 
thm mono_trans 
end
 
text {*
  El predicado `ser par' es un operador monótono entre los naturales con la
  relación de divisibilidad y los booleanos con el condicional; es decir, 
     x dvd y ⟹ even x ⟶ even y
*}
 
interpretation Mono "(dvd)" "(⟶)" "λn::nat. 2 dvd n"
proof
  fix x y :: nat 
  show "x dvd y ⟹ even x ⟶ even y"
    proof 
      assume "x dvd y" and "even x"
      then show "even y" 
        using  Rings.comm_monoid_mult_class.dvd_trans by auto
    qed
qed
 
section {* Semigrupos, monoides y grupos *}
 
subsection {* Definición de clases *}
 
text {*
  Un semigrupo es una estructura compuesta por un conjunto A y una
  operación binaria en A.
*}
 
class semigrupo =
  fixes mult :: "'a ⇒ 'a ⇒ 'a" (infixl "⊗" 70) 
  assumes asoc: "(x ⊗ y) ⊗ z = x ⊗ (y ⊗ z )"
 
subsection {* Instanciación de clases *}
 
text {*
  Los enteros con la suma forman un semigrupo.
*}
 
instantiation int :: semigrupo 
begin 
definition 
  mult_int_def: "i ⊗ j = i + (j ::int)" 
 
instance proof 
  fix i j k :: "int" 
  have "(i + j ) + k = i + (j + k)" by simp 
  then show "(i ⊗ j ) ⊗ k = i ⊗ (j ⊗ k)" unfolding mult_int_def . 
qed 
end 
 
text {*
  Los naturales con la suma forman un semigrupo.
*}
 
instantiation nat :: semigrupo 
begin 
primrec mult_nat where 
  "(0::nat) ⊗ n = n" 
| "Suc m ⊗ n = Suc (m ⊗ n)" 
 
instance proof 
  fix m n q :: "nat" 
  show "m ⊗ n ⊗ q = m ⊗ (n ⊗ q)" 
    by (induct m) auto
qed 
end
 
subsection {* Instancias recursivas *}
 
text {*
  Si (A,⊗) y (B,⊗) son semigrupos, entonces ((A×B,⊗), donde el producto
  se define por 
     (x,y)⊗(x',y') = (x⊗x',y⊗y'),
  es un semigrupo.
*}
 
instantiation prod :: (semigrupo, semigrupo) semigrupo 
begin 
 
definition 
  mult_prod_def : "p1 ⊗ p2 = (fst p1 ⊗ fst p2, snd p1 ⊗ snd p2)" 
 
instance proof 
  fix p1 p2 p3 :: "'a::semigrupo × 'b::semigrupo" 
  show "(p1 ⊗ p2) ⊗ p3 = p1 ⊗ (p2 ⊗ p3)" 
    unfolding mult_prod_def by (simp add: asoc) 
qed 
end
 
subsection {* Subclases *}
 
text {*
  Un monoide izquierdo es un semigrupo con elemento neutro por la izquierda. 
*}
 
class monoideI = semigrupo + 
  fixes neutro :: "'a" ("𝟭") 
  assumes neutroI: "𝟭 ⊗ x = x"
 
text {*
  Los naturales y los enteros con la suma forman monoides por la izquierda.
*}
 
instantiation nat and int :: monoideI 
begin 
 
definition 
  neutro_nat_def : "𝟭 = (0::nat)" 
 
definition 
  neutro_int_def : "𝟭 = (0::int)" 
 
instance proof 
  fix n :: nat 
  show "𝟭 ⊗ n = n" unfolding neutro_nat_def by simp
next 
  fix k :: int 
  show "𝟭 ⊗ k = k" unfolding neutro_int_def mult_int_def by simp 
qed 
end
 
text {*
  El producto de dos monoides por la izquierda es un monoide por la
  izquierda, donde el neutro es el par formado por los elementos neutros.
*}
 
instantiation prod :: (monoideI , monoideI) monoideI 
begin 
 
definition 
  neutro_prod_def : "𝟭 = (𝟭, 𝟭)" 
 
instance proof 
  fix p :: "'a::monoideI × 'b::monoideI" 
  show "𝟭 ⊗ p = p" 
    unfolding neutro_prod_def mult_prod_def by (simp add: neutroI) 
qed 
end
 
text {*
  Un monoide es un monoide por la izquierda cuyo elemento neutro por la
  izquierda lo es también por la derecha.
*}
 
class monoide = monoideI + 
  assumes neutro: "x ⊗ 𝟭 = x" 
 
text {*
  Los naturales y los enteros con la suma son monoides.
*}
 
instantiation nat and int :: monoide 
begin 
 
instance proof 
  fix n :: nat 
  show "n ⊗ 𝟭 = n" 
    unfolding neutro_nat_def by (induct n) simp_all 
next 
  fix k :: int 
  show "k ⊗ 𝟭 = k" 
    unfolding neutro_int_def mult_int_def by simp 
qed
end
 
text {*
  El producto de dos monoides es un monoide.
*}
 
instantiation prod :: (monoide, monoide) monoide 
begin 
 
instance proof 
  fix p :: "'a::monoide × 'b::monoide" 
  show "p ⊗ 𝟭 = p" 
    unfolding neutro_prod_def mult_prod_def by (simp add: neutro) 
qed 
end
 
text {*
  Un grupo es un monoide por la izquierda tal que todo elemento posee un
  inverso por la izquierda.
*}
 
class grupo2 = monoideI + 
  fixes inverso :: "'a ⇒ 'a" ("(_⇧-⇧1)" [1000] 999)
  assumes inversoI: "x⇧-⇧1 ⊗ x = 𝟭" 
 
text {*
  Los enteros con la suma forman un grupo.
*}
 
instantiation int :: grupo2 
begin 
 
definition
  inverso_int_def: "i⇧-⇧1 = -(i::int)"
 
instance proof 
  fix i :: "int" 
  have "-i + i = 0" by simp 
  then show "i⇧-⇧1 ⊗ i = 𝟭" 
    unfolding mult_int_def neutro_int_def inverso_int_def . 
qed 
end
 
subsection {* Razonamiento abstracto *}
 
text {*
  En los grupos se verifica la propiedad cancelativa por la izquierda, i.e.
     x ⊗ y = x ⊗ z ⟷ y = z
*}
 
lemma (in grupo2) cancelativa_izq: "x ⊗ y = x ⊗ z ⟷ y = z" 
proof 
  assume "x ⊗ y = x ⊗ z"
  hence "x⇧-⇧1 ⊗ (x ⊗ y) = x⇧-⇧1 ⊗ (x ⊗ z)" by simp 
  hence "(x⇧-⇧1 ⊗ x) ⊗ y = (x⇧-⇧1 ⊗ x) ⊗ z" using asoc by simp 
  then show "y = z" using neutroI and inversoI by simp
next 
  assume "y = z" 
  then show "x ⊗ y = x ⊗ z" by simp
qed
 
thm grupo2.cancelativa_izq
 
text {*
  Se genera el teorema grupo.cancelativa_izq
     class.grupo2 ?mult ?neutro ?inverso ⟹ 
     (?mult ?x ?y = ?mult ?x ?z) = (?y = ?z)
 
  El teorema se aplica automáticamente a todas las instancias de la clase
  grupo. Por ejemplo, a los enteros.
*}
 
subsection {* Definiciones derivadas *}
 
text {*
  En los monoides se define la potencia natural por
  · x^0     = 1
  · x^{n+1} = x*x^n
*}
 
fun (in monoide) potencia_nat :: "nat ⇒ 'a ⇒ 'a" where 
  "potencia_nat 0 x       = 𝟭"  
| "potencia_nat (Suc n) x = x ⊗ potencia_nat n x"
 
subsection {* Analogía entre clases y functores *}
 
text {*
  Las listas con la operación de concatenación y la lista vacía como elemento
  neutro forman un monoide.
*}
 
interpretation list_monoide: monoide "append" "[]"
proof 
  show "⋀x y z. (x @ y) @ z = x @ (y @ z)" by simp
next
  show "⋀x. [] @ x = x" by simp
next
  show "⋀x. x @ [] = x" by simp
qed
 
text {*
  Se pueden aplicar propiedades de los monides a las listas. Por ejemplo,
*}
 
lemma "append [] xs = xs"
  by simp
 
text {*
  (repite n xs) es la lista obtenida concatenando n veces la lista xs. 
*}
 
fun repite :: "nat ⇒ 'a list ⇒ 'a list" where 
  "repite 0 _        = []"
| "repite (Suc n) xs = xs @ repite n xs"
 
text {*
  Las listas con la operación de concatenación y la lista vacía como elemento
  neutro forman un monoide. Además, la potencia natural se intepreta como
  repite. 
*}
 
interpretation list_monoide: monoide "append" "[]" rewrites
  "monoide.potencia_nat append [] = repite" 
proof -
  interpret monoide "append" "[]" .. 
  show "monoide.potencia_nat append [] = repite" 
  proof 
    fix n 
    show "monoide.potencia_nat append [] n = repite n"
      by (induct n) auto 
  qed 
qed intro_locales
 
subsection {* Relaciones de subclase adicionales *}
 
text {*
  Los grupos son monoides.
*}
 
subclass (in grupo2) monoide 
proof 
  fix x 
  have "x⇧-⇧1 ⊗ (x ⊗ 𝟭) = x⇧-⇧1 ⊗ (x ⊗ (x⇧-⇧1 ⊗ x))" using inversoI by simp
  also have "… = (x⇧-⇧1 ⊗ x) ⊗ (x⇧-⇧1 ⊗ x)" using asoc [symmetric] by simp
  also have "… = 𝟭 ⊗ (x⇧-⇧1 ⊗ x)" using inversoI by simp
  also have "… = x⇧-⇧1 ⊗ x" using neutroI by simp
  finally have "x⇧-⇧1 ⊗ (x ⊗ 𝟭) = x⇧-⇧1 ⊗ x" . 
  then show "x ⊗ 𝟭 = x" using cancelativa_izq by simp
qed
 
text {*
  La potencia entera en los grupos se define a partir de la potencia natural
  como sigue:
  · x^k = x^k si k ≥ 0
  · x^k = (x^{-k})^{-1}, en caso contrario.
*}
 
definition (in grupo2) potencia_entera :: "int ⇒ 'a ⇒ 'a" where 
  "potencia_entera k x = 
   (if k >= 0 
    then potencia_nat (nat k) x 
    else (potencia_nat (nat (- k)) x)⇧-⇧1)"
 
section {* Bibliografía *}
text {* 
  + "Haskell-style type classes with Isabelle/Isar" ~ F. Haftmann.
    http://bit.ly/2E55pAJ
  + "Tutorial to locales and locale interpretation" ~ C. Ballarin.
    http://bit.ly/2E3ozXB  
*}
 
end