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 |
