Desarrollo de teorías formalizadas con Isabelle/HOL

chapter {* 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 (auto simp: 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 menor_def lineal antisim  
  by blast

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 blast
next
  fix P Q R show "P ⟶ Q ⟹ Q ⟶ R ⟹ P ⟶ R" by blast
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" using dvd_refl by simp
next
  fix x y z :: nat
  show "⟦x dvd y; y dvd z⟧ ⟹ x dvd z" using dvd_trans by auto
next
  fix x y :: nat
  show "⟦x dvd y; y dvd x⟧ ⟹ x = y" using dvd_antisym by simp
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