-
Notifications
You must be signed in to change notification settings - Fork 0
/
Potencias_de_potencias_en_monoides.thy
97 lines (82 loc) · 2.7 KB
/
Potencias_de_potencias_en_monoides.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
(* Potencias_de_potencias_en_monoides.thy
-- Si M es un monoide, a \<in> M y m, n \<in> \<nat>, entonces a^(m\<sqdot>n) = (a^m)^n
-- José A. Alonso Jiménez <https://jaalonso.github.io>
-- Sevilla, 17-mayo-2024
-- ------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
-- En los [monoides](https://en.wikipedia.org/wiki/Monoid) se define la
-- potencia con exponentes naturales. En Lean4, la potencia x^n se
-- se caracteriza por los siguientes lemas:
-- power_0 : x ^ 0 = 1
-- power_Suc : x ^ (Suc n) x = x * x ^ n
--
-- Demostrar que si M es un monoide, a \<in> M y m, n \<in> \<nat>, entonces
-- a^(m * n) = (a^m)^n
--
-- Indicación: Se puede usar el lema
-- power_add : a^(m + n) = a^m * a^n
-- ------------------------------------------------------------------ *)
theory Potencias_de_potencias_en_monoides
imports Main
begin
context monoid_mult
begin
(* 1\<ordfeminine> demostración *)
lemma "a^(m * n) = (a^m)^n"
proof (induct n)
have "a ^ (m * 0) = a ^ 0"
by (simp only: mult_0_right)
also have "\<dots> = 1"
by (simp only: power_0)
also have "\<dots> = (a ^ m) ^ 0"
by (simp only: power_0)
finally show "a ^ (m * 0) = (a ^ m) ^ 0"
by this
next
fix n
assume HI : "a ^ (m * n) = (a ^ m) ^ n"
have "a ^ (m * Suc n) = a ^ (m + m * n)"
by (simp only: mult_Suc_right)
also have "\<dots> = a ^ m * a ^ (m * n)"
by (simp only: power_add)
also have "\<dots> = a ^ m * (a ^ m) ^ n"
by (simp only: HI)
also have "\<dots> = (a ^ m) ^ Suc n"
by (simp only: power_Suc)
finally show "a ^ (m * Suc n) = (a ^ m) ^ Suc n"
by this
qed
(* 2\<ordfeminine> demostración *)
lemma "a^(m * n) = (a^m)^n"
proof (induct n)
have "a ^ (m * 0) = a ^ 0" by simp
also have "\<dots> = 1" by simp
also have "\<dots> = (a ^ m) ^ 0" by simp
finally show "a ^ (m * 0) = (a ^ m) ^ 0" .
next
fix n
assume HI : "a ^ (m * n) = (a ^ m) ^ n"
have "a ^ (m * Suc n) = a ^ (m + m * n)" by simp
also have "\<dots> = a ^ m * a ^ (m * n)" by (simp add: power_add)
also have "\<dots> = a ^ m * (a ^ m) ^ n" using HI by simp
also have "\<dots> = (a ^ m) ^ Suc n" by simp
finally show "a ^ (m * Suc n) =
(a ^ m) ^ Suc n" .
qed
(* 3\<ordfeminine> demostración *)
lemma "a^(m * n) = (a^m)^n"
proof (induct n)
case 0
then show ?case by simp
next
case (Suc n)
then show ?case by (simp add: power_add)
qed
(* 4\<ordfeminine> demostración *)
lemma "a^(m * n) = (a^m)^n"
by (induct n) (simp_all add: power_add)
(* 5\<ordfeminine> demostración *)
lemma "a^(m * n) = (a^m)^n"
by (simp only: power_mult)
end
end