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
