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 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^ = 𝟭"
  (* sledgehammer *)
  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 
    by this
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" 
    by this
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"
  then have "x^ ⋅ (x ⋅ y) = x^ ⋅ (x ⋅ z)"
    by (simp only: arg_cong [of "x ⋅ y" "x ⋅ z"])
  then have "(x^ ⋅ x) ⋅ y = (x^ ⋅ x) ⋅ z" 
    by (simp only: asociativa)
  then have "𝟭 ⋅ 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 only: arg_cong [of "y" "z"])
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 [THEN sym] 
    by (rule arg_cong [of "x" "e ⋅ x" "λy. y ⋅ x^"])
  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 
    by this
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 [THEN sym] 
    by (simp only: arg_cong [of "𝟭" "x' ⋅ x"])
  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 
    by this
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 
      by this
  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 only: arg_cong [of "x^" "y^"])
  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 es menos o igual 
  que x.›

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

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 
fun 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"
  then have "x⇧-⇧1 ⊗ (x ⊗ y) = x⇧-⇧1 ⊗ (x ⊗ z)" 
    by simp 
  then have "(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" 
    by this
  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