author | wenzelm |
Fri, 01 Jan 2016 16:40:47 +0100 | |
changeset 62028 | 2ecee4679f99 |
parent 61955 | e96292f32c3c |
child 62083 | 7582b39f51ed |
permissions | -rw-r--r-- |
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/Power.thy |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
3 |
Copyright 1997 University of Cambridge |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
4 |
*) |
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
5 |
|
60758 | 6 |
section \<open>Exponentiation\<close> |
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
7 |
|
15131 | 8 |
theory Power |
55096 | 9 |
imports Num Equiv_Relations |
15131 | 10 |
begin |
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
11 |
|
60867 | 12 |
context linordered_ring (* TODO: move *) |
13 |
begin |
|
14 |
||
15 |
lemma sum_squares_ge_zero: |
|
16 |
"0 \<le> x * x + y * y" |
|
17 |
by (intro add_nonneg_nonneg zero_le_square) |
|
18 |
||
19 |
lemma not_sum_squares_lt_zero: |
|
20 |
"\<not> x * x + y * y < 0" |
|
21 |
by (simp add: not_less sum_squares_ge_zero) |
|
22 |
||
23 |
end |
|
24 |
||
60758 | 25 |
subsection \<open>Powers for Arbitrary Monoids\<close> |
30960 | 26 |
|
30996 | 27 |
class power = one + times |
30960 | 28 |
begin |
24996 | 29 |
|
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61944
diff
changeset
|
30 |
primrec power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^" 80) |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61944
diff
changeset
|
31 |
where |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61944
diff
changeset
|
32 |
power_0: "a ^ 0 = 1" |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61944
diff
changeset
|
33 |
| power_Suc: "a ^ Suc n = a * a ^ n" |
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
34 |
|
30996 | 35 |
notation (latex output) |
36 |
power ("(_\<^bsup>_\<^esup>)" [1000] 1000) |
|
37 |
||
60758 | 38 |
text \<open>Special syntax for squares.\<close> |
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61944
diff
changeset
|
39 |
abbreviation power2 :: "'a \<Rightarrow> 'a" ("(_\<^sup>2)" [1000] 999) |
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61944
diff
changeset
|
40 |
where "x\<^sup>2 \<equiv> x ^ 2" |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
41 |
|
30960 | 42 |
end |
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
43 |
|
30996 | 44 |
context monoid_mult |
45 |
begin |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
46 |
|
39438
c5ece2a7a86e
Isar "default" step needs to fail for solved problems, for clear distinction of '.' and '..' for example -- amending lapse introduced in 9de4d64eee3b (April 2004);
wenzelm
parents:
36409
diff
changeset
|
47 |
subclass power . |
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
48 |
|
30996 | 49 |
lemma power_one [simp]: |
50 |
"1 ^ n = 1" |
|
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30242
diff
changeset
|
51 |
by (induct n) simp_all |
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
52 |
|
30996 | 53 |
lemma power_one_right [simp]: |
31001 | 54 |
"a ^ 1 = a" |
30996 | 55 |
by simp |
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
56 |
|
59741
5b762cd73a8e
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59009
diff
changeset
|
57 |
lemma power_Suc0_right [simp]: |
5b762cd73a8e
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59009
diff
changeset
|
58 |
"a ^ Suc 0 = a" |
5b762cd73a8e
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59009
diff
changeset
|
59 |
by simp |
5b762cd73a8e
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59009
diff
changeset
|
60 |
|
30996 | 61 |
lemma power_commutes: |
62 |
"a ^ n * a = a * a ^ n" |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
63 |
by (induct n) (simp_all add: mult.assoc) |
21199
2d83f93c3580
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
krauss
parents:
17149
diff
changeset
|
64 |
|
30996 | 65 |
lemma power_Suc2: |
66 |
"a ^ Suc n = a ^ n * a" |
|
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30242
diff
changeset
|
67 |
by (simp add: power_commutes) |
28131
3130d7b3149d
add lemma power_Suc2; generalize power_minus from class comm_ring_1 to ring_1
huffman
parents:
25874
diff
changeset
|
68 |
|
30996 | 69 |
lemma power_add: |
70 |
"a ^ (m + n) = a ^ m * a ^ n" |
|
71 |
by (induct m) (simp_all add: algebra_simps) |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
72 |
|
30996 | 73 |
lemma power_mult: |
74 |
"a ^ (m * n) = (a ^ m) ^ n" |
|
30273
ecd6f0ca62ea
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
huffman
parents:
30242
diff
changeset
|
75 |
by (induct n) (simp_all add: power_add) |
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
76 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset
|
77 |
lemma power2_eq_square: "a\<^sup>2 = a * a" |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
78 |
by (simp add: numeral_2_eq_2) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
79 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
80 |
lemma power3_eq_cube: "a ^ 3 = a * a * a" |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
81 |
by (simp add: numeral_3_eq_3 mult.assoc) |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
82 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
83 |
lemma power_even_eq: |
53076 | 84 |
"a ^ (2 * n) = (a ^ n)\<^sup>2" |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
85 |
by (subst mult.commute) (simp add: power_mult) |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
86 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
87 |
lemma power_odd_eq: |
53076 | 88 |
"a ^ Suc (2*n) = a * (a ^ n)\<^sup>2" |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
89 |
by (simp add: power_even_eq) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
90 |
|
47255
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset
|
91 |
lemma power_numeral_even: |
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset
|
92 |
"z ^ numeral (Num.Bit0 w) = (let w = z ^ (numeral w) in w * w)" |
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset
|
93 |
unfolding numeral_Bit0 power_add Let_def .. |
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset
|
94 |
|
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset
|
95 |
lemma power_numeral_odd: |
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset
|
96 |
"z ^ numeral (Num.Bit1 w) = (let w = z ^ (numeral w) in z * w * w)" |
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset
|
97 |
unfolding numeral_Bit1 One_nat_def add_Suc_right add_0_right |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
98 |
unfolding power_Suc power_add Let_def mult.assoc .. |
47255
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset
|
99 |
|
49824 | 100 |
lemma funpow_times_power: |
101 |
"(times x ^^ f x) = times (x ^ f x)" |
|
102 |
proof (induct "f x" arbitrary: f) |
|
103 |
case 0 then show ?case by (simp add: fun_eq_iff) |
|
104 |
next |
|
105 |
case (Suc n) |
|
106 |
def g \<equiv> "\<lambda>x. f x - 1" |
|
107 |
with Suc have "n = g x" by simp |
|
108 |
with Suc have "times x ^^ g x = times (x ^ g x)" by simp |
|
109 |
moreover from Suc g_def have "f x = g x + 1" by simp |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
110 |
ultimately show ?case by (simp add: power_add funpow_add fun_eq_iff mult.assoc) |
49824 | 111 |
qed |
112 |
||
58656 | 113 |
lemma power_commuting_commutes: |
114 |
assumes "x * y = y * x" |
|
115 |
shows "x ^ n * y = y * x ^n" |
|
116 |
proof (induct n) |
|
117 |
case (Suc n) |
|
118 |
have "x ^ Suc n * y = x ^ n * y * x" |
|
119 |
by (subst power_Suc2) (simp add: assms ac_simps) |
|
120 |
also have "\<dots> = y * x ^ Suc n" |
|
121 |
unfolding Suc power_Suc2 |
|
122 |
by (simp add: ac_simps) |
|
123 |
finally show ?case . |
|
124 |
qed simp |
|
125 |
||
30996 | 126 |
end |
127 |
||
128 |
context comm_monoid_mult |
|
129 |
begin |
|
130 |
||
56480
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
55811
diff
changeset
|
131 |
lemma power_mult_distrib [field_simps]: |
30996 | 132 |
"(a * b) ^ n = (a ^ n) * (b ^ n)" |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
133 |
by (induct n) (simp_all add: ac_simps) |
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
134 |
|
30996 | 135 |
end |
136 |
||
60758 | 137 |
text\<open>Extract constant factors from powers\<close> |
59741
5b762cd73a8e
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59009
diff
changeset
|
138 |
declare power_mult_distrib [where a = "numeral w" for w, simp] |
5b762cd73a8e
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59009
diff
changeset
|
139 |
declare power_mult_distrib [where b = "numeral w" for w, simp] |
5b762cd73a8e
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59009
diff
changeset
|
140 |
|
60155
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset
|
141 |
lemma power_add_numeral [simp]: |
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset
|
142 |
fixes a :: "'a :: monoid_mult" |
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset
|
143 |
shows "a^numeral m * a^numeral n = a^numeral (m + n)" |
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset
|
144 |
by (simp add: power_add [symmetric]) |
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset
|
145 |
|
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset
|
146 |
lemma power_add_numeral2 [simp]: |
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset
|
147 |
fixes a :: "'a :: monoid_mult" |
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset
|
148 |
shows "a^numeral m * (a^numeral n * b) = a^numeral (m + n) * b" |
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset
|
149 |
by (simp add: mult.assoc [symmetric]) |
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset
|
150 |
|
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset
|
151 |
lemma power_mult_numeral [simp]: |
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset
|
152 |
fixes a :: "'a :: monoid_mult" |
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset
|
153 |
shows"(a^numeral m)^numeral n = a^numeral (m * n)" |
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset
|
154 |
by (simp only: numeral_mult power_mult) |
91477b3a2d6b
Tidying. Improved simplification for numerals, esp in exponents.
paulson <lp15@cam.ac.uk>
parents:
59867
diff
changeset
|
155 |
|
47191 | 156 |
context semiring_numeral |
157 |
begin |
|
158 |
||
159 |
lemma numeral_sqr: "numeral (Num.sqr k) = numeral k * numeral k" |
|
160 |
by (simp only: sqr_conv_mult numeral_mult) |
|
161 |
||
162 |
lemma numeral_pow: "numeral (Num.pow k l) = numeral k ^ numeral l" |
|
163 |
by (induct l, simp_all only: numeral_class.numeral.simps pow.simps |
|
164 |
numeral_sqr numeral_mult power_add power_one_right) |
|
165 |
||
166 |
lemma power_numeral [simp]: "numeral k ^ numeral l = numeral (Num.pow k l)" |
|
167 |
by (rule numeral_pow [symmetric]) |
|
168 |
||
169 |
end |
|
170 |
||
30996 | 171 |
context semiring_1 |
172 |
begin |
|
173 |
||
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
174 |
lemma of_nat_power [simp]: |
30996 | 175 |
"of_nat (m ^ n) = of_nat m ^ n" |
176 |
by (induct n) (simp_all add: of_nat_mult) |
|
177 |
||
59009
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58889
diff
changeset
|
178 |
lemma zero_power: |
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58889
diff
changeset
|
179 |
"0 < n \<Longrightarrow> 0 ^ n = 0" |
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58889
diff
changeset
|
180 |
by (cases n) simp_all |
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58889
diff
changeset
|
181 |
|
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58889
diff
changeset
|
182 |
lemma power_zero_numeral [simp]: |
348561aa3869
generalized lemmas (particularly concerning dvd) as far as appropriate
haftmann
parents:
58889
diff
changeset
|
183 |
"0 ^ numeral k = 0" |
47209
4893907fe872
add constant pred_numeral k = numeral k - (1::nat);
huffman
parents:
47192
diff
changeset
|
184 |
by (simp add: numeral_eq_Suc) |
47191 | 185 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset
|
186 |
lemma zero_power2: "0\<^sup>2 = 0" (* delete? *) |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
187 |
by (rule power_zero_numeral) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
188 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset
|
189 |
lemma one_power2: "1\<^sup>2 = 1" (* delete? *) |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
190 |
by (rule power_one) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
191 |
|
60867 | 192 |
lemma power_0_Suc [simp]: |
193 |
"0 ^ Suc n = 0" |
|
194 |
by simp |
|
195 |
||
196 |
text\<open>It looks plausible as a simprule, but its effect can be strange.\<close> |
|
197 |
lemma power_0_left: |
|
198 |
"0 ^ n = (if n = 0 then 1 else 0)" |
|
199 |
by (cases n) simp_all |
|
200 |
||
30996 | 201 |
end |
202 |
||
203 |
context comm_semiring_1 |
|
204 |
begin |
|
205 |
||
60758 | 206 |
text \<open>The divides relation\<close> |
30996 | 207 |
|
208 |
lemma le_imp_power_dvd: |
|
209 |
assumes "m \<le> n" shows "a ^ m dvd a ^ n" |
|
210 |
proof |
|
211 |
have "a ^ n = a ^ (m + (n - m))" |
|
60758 | 212 |
using \<open>m \<le> n\<close> by simp |
30996 | 213 |
also have "\<dots> = a ^ m * a ^ (n - m)" |
214 |
by (rule power_add) |
|
215 |
finally show "a ^ n = a ^ m * a ^ (n - m)" . |
|
216 |
qed |
|
217 |
||
218 |
lemma power_le_dvd: |
|
219 |
"a ^ n dvd b \<Longrightarrow> m \<le> n \<Longrightarrow> a ^ m dvd b" |
|
220 |
by (rule dvd_trans [OF le_imp_power_dvd]) |
|
221 |
||
222 |
lemma dvd_power_same: |
|
223 |
"x dvd y \<Longrightarrow> x ^ n dvd y ^ n" |
|
224 |
by (induct n) (auto simp add: mult_dvd_mono) |
|
225 |
||
226 |
lemma dvd_power_le: |
|
227 |
"x dvd y \<Longrightarrow> m \<ge> n \<Longrightarrow> x ^ n dvd y ^ m" |
|
228 |
by (rule power_le_dvd [OF dvd_power_same]) |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
229 |
|
30996 | 230 |
lemma dvd_power [simp]: |
231 |
assumes "n > (0::nat) \<or> x = 1" |
|
232 |
shows "x dvd (x ^ n)" |
|
233 |
using assms proof |
|
234 |
assume "0 < n" |
|
235 |
then have "x ^ n = x ^ Suc (n - 1)" by simp |
|
236 |
then show "x dvd (x ^ n)" by simp |
|
237 |
next |
|
238 |
assume "x = 1" |
|
239 |
then show "x dvd (x ^ n)" by simp |
|
240 |
qed |
|
241 |
||
242 |
end |
|
243 |
||
60867 | 244 |
class semiring_1_no_zero_divisors = semiring_1 + semiring_no_zero_divisors |
245 |
begin |
|
246 |
||
247 |
subclass power . |
|
248 |
||
249 |
lemma power_eq_0_iff [simp]: |
|
250 |
"a ^ n = 0 \<longleftrightarrow> a = 0 \<and> n > 0" |
|
251 |
by (induct n) auto |
|
252 |
||
253 |
lemma power_not_zero: |
|
254 |
"a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0" |
|
255 |
by (induct n) auto |
|
256 |
||
257 |
lemma zero_eq_power2 [simp]: |
|
258 |
"a\<^sup>2 = 0 \<longleftrightarrow> a = 0" |
|
259 |
unfolding power2_eq_square by simp |
|
260 |
||
261 |
end |
|
262 |
||
263 |
context semidom |
|
264 |
begin |
|
265 |
||
266 |
subclass semiring_1_no_zero_divisors .. |
|
267 |
||
268 |
end |
|
269 |
||
30996 | 270 |
context ring_1 |
271 |
begin |
|
272 |
||
273 |
lemma power_minus: |
|
274 |
"(- a) ^ n = (- 1) ^ n * a ^ n" |
|
275 |
proof (induct n) |
|
276 |
case 0 show ?case by simp |
|
277 |
next |
|
278 |
case (Suc n) then show ?case |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
279 |
by (simp del: power_Suc add: power_Suc2 mult.assoc) |
30996 | 280 |
qed |
281 |
||
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61378
diff
changeset
|
282 |
lemma power_minus': "NO_MATCH 1 x \<Longrightarrow> (-x) ^ n = (-1)^n * x ^ n" |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61378
diff
changeset
|
283 |
by (rule power_minus) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
61378
diff
changeset
|
284 |
|
47191 | 285 |
lemma power_minus_Bit0: |
286 |
"(- x) ^ numeral (Num.Bit0 k) = x ^ numeral (Num.Bit0 k)" |
|
287 |
by (induct k, simp_all only: numeral_class.numeral.simps power_add |
|
288 |
power_one_right mult_minus_left mult_minus_right minus_minus) |
|
289 |
||
290 |
lemma power_minus_Bit1: |
|
291 |
"(- x) ^ numeral (Num.Bit1 k) = - (x ^ numeral (Num.Bit1 k))" |
|
47220
52426c62b5d0
replace lemmas eval_nat_numeral with a simpler reformulation
huffman
parents:
47209
diff
changeset
|
292 |
by (simp only: eval_nat_numeral(3) power_Suc power_minus_Bit0 mult_minus_left) |
47191 | 293 |
|
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
294 |
lemma power2_minus [simp]: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset
|
295 |
"(- a)\<^sup>2 = a\<^sup>2" |
60867 | 296 |
by (fact power_minus_Bit0) |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
297 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
298 |
lemma power_minus1_even [simp]: |
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58157
diff
changeset
|
299 |
"(- 1) ^ (2*n) = 1" |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
300 |
proof (induct n) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
301 |
case 0 show ?case by simp |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
302 |
next |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
303 |
case (Suc n) then show ?case by (simp add: power_add power2_eq_square) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
304 |
qed |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
305 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
306 |
lemma power_minus1_odd: |
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58157
diff
changeset
|
307 |
"(- 1) ^ Suc (2*n) = -1" |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
308 |
by simp |
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
309 |
|
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
310 |
lemma power_minus_even [simp]: |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
311 |
"(-a) ^ (2*n) = a ^ (2*n)" |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
312 |
by (simp add: power_minus [of a]) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
313 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
314 |
end |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
315 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
316 |
context ring_1_no_zero_divisors |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
317 |
begin |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
318 |
|
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
319 |
subclass semiring_1_no_zero_divisors .. |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
320 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
321 |
lemma power2_eq_1_iff: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset
|
322 |
"a\<^sup>2 = 1 \<longleftrightarrow> a = 1 \<or> a = - 1" |
60867 | 323 |
using square_eq_1_iff [of a] by (simp add: power2_eq_square) |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
324 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
325 |
end |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
326 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
327 |
context idom |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
328 |
begin |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
329 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset
|
330 |
lemma power2_eq_iff: "x\<^sup>2 = y\<^sup>2 \<longleftrightarrow> x = y \<or> x = - y" |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
331 |
unfolding power2_eq_square by (rule square_eq_iff) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
332 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
333 |
end |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
334 |
|
60867 | 335 |
context algebraic_semidom |
336 |
begin |
|
337 |
||
338 |
lemma div_power: |
|
339 |
assumes "b dvd a" |
|
340 |
shows "(a div b) ^ n = a ^ n div b ^ n" |
|
341 |
using assms by (induct n) (simp_all add: div_mult_div_if_dvd dvd_power_same) |
|
342 |
||
343 |
end |
|
344 |
||
60685
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60155
diff
changeset
|
345 |
context normalization_semidom |
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60155
diff
changeset
|
346 |
begin |
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60155
diff
changeset
|
347 |
|
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60155
diff
changeset
|
348 |
lemma normalize_power: |
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60155
diff
changeset
|
349 |
"normalize (a ^ n) = normalize a ^ n" |
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60155
diff
changeset
|
350 |
by (induct n) (simp_all add: normalize_mult) |
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60155
diff
changeset
|
351 |
|
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60155
diff
changeset
|
352 |
lemma unit_factor_power: |
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60155
diff
changeset
|
353 |
"unit_factor (a ^ n) = unit_factor a ^ n" |
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60155
diff
changeset
|
354 |
by (induct n) (simp_all add: unit_factor_mult) |
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60155
diff
changeset
|
355 |
|
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60155
diff
changeset
|
356 |
end |
cb21b7022b00
moved normalization and unit_factor into Main HOL corpus
haftmann
parents:
60155
diff
changeset
|
357 |
|
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
358 |
context division_ring |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
359 |
begin |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
360 |
|
60867 | 361 |
text\<open>Perhaps these should be simprules.\<close> |
362 |
lemma power_inverse [field_simps, divide_simps]: |
|
363 |
"inverse a ^ n = inverse (a ^ n)" |
|
364 |
proof (cases "a = 0") |
|
365 |
case True then show ?thesis by (simp add: power_0_left) |
|
366 |
next |
|
367 |
case False then have "inverse (a ^ n) = inverse a ^ n" |
|
368 |
by (induct n) (simp_all add: nonzero_inverse_mult_distrib power_commutes) |
|
369 |
then show ?thesis by simp |
|
370 |
qed |
|
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
371 |
|
60867 | 372 |
lemma power_one_over [field_simps, divide_simps]: |
373 |
"(1 / a) ^ n = 1 / a ^ n" |
|
374 |
using power_inverse [of a] by (simp add: divide_inverse) |
|
375 |
||
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
376 |
end |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
377 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
378 |
context field |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
379 |
begin |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
380 |
|
60867 | 381 |
lemma power_diff: |
382 |
assumes nz: "a \<noteq> 0" |
|
383 |
shows "n \<le> m \<Longrightarrow> a ^ (m - n) = a ^ m / a ^ n" |
|
384 |
by (induct m n rule: diff_induct) (simp_all add: nz power_not_zero) |
|
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
385 |
|
60867 | 386 |
lemma power_divide [field_simps, divide_simps]: |
387 |
"(a / b) ^ n = a ^ n / b ^ n" |
|
388 |
by (induct n) simp_all |
|
389 |
||
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
390 |
end |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
391 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
392 |
|
60758 | 393 |
subsection \<open>Exponentiation on ordered types\<close> |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
394 |
|
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
33364
diff
changeset
|
395 |
context linordered_semidom |
30996 | 396 |
begin |
397 |
||
398 |
lemma zero_less_power [simp]: |
|
399 |
"0 < a \<Longrightarrow> 0 < a ^ n" |
|
56544 | 400 |
by (induct n) simp_all |
30996 | 401 |
|
402 |
lemma zero_le_power [simp]: |
|
403 |
"0 \<le> a \<Longrightarrow> 0 \<le> a ^ n" |
|
56536 | 404 |
by (induct n) simp_all |
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
405 |
|
47241 | 406 |
lemma power_mono: |
407 |
"a \<le> b \<Longrightarrow> 0 \<le> a \<Longrightarrow> a ^ n \<le> b ^ n" |
|
408 |
by (induct n) (auto intro: mult_mono order_trans [of 0 a b]) |
|
409 |
||
410 |
lemma one_le_power [simp]: "1 \<le> a \<Longrightarrow> 1 \<le> a ^ n" |
|
411 |
using power_mono [of 1 a n] by simp |
|
412 |
||
413 |
lemma power_le_one: "\<lbrakk>0 \<le> a; a \<le> 1\<rbrakk> \<Longrightarrow> a ^ n \<le> 1" |
|
414 |
using power_mono [of a 1 n] by simp |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
415 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
416 |
lemma power_gt1_lemma: |
30996 | 417 |
assumes gt1: "1 < a" |
418 |
shows "1 < a * a ^ n" |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
419 |
proof - |
30996 | 420 |
from gt1 have "0 \<le> a" |
421 |
by (fact order_trans [OF zero_le_one less_imp_le]) |
|
422 |
have "1 * 1 < a * 1" using gt1 by simp |
|
423 |
also have "\<dots> \<le> a * a ^ n" using gt1 |
|
60758 | 424 |
by (simp only: mult_mono \<open>0 \<le> a\<close> one_le_power order_less_imp_le |
14577 | 425 |
zero_le_one order_refl) |
426 |
finally show ?thesis by simp |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
427 |
qed |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
428 |
|
30996 | 429 |
lemma power_gt1: |
430 |
"1 < a \<Longrightarrow> 1 < a ^ Suc n" |
|
431 |
by (simp add: power_gt1_lemma) |
|
24376 | 432 |
|
30996 | 433 |
lemma one_less_power [simp]: |
434 |
"1 < a \<Longrightarrow> 0 < n \<Longrightarrow> 1 < a ^ n" |
|
435 |
by (cases n) (simp_all add: power_gt1_lemma) |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
436 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
437 |
lemma power_le_imp_le_exp: |
30996 | 438 |
assumes gt1: "1 < a" |
439 |
shows "a ^ m \<le> a ^ n \<Longrightarrow> m \<le> n" |
|
440 |
proof (induct m arbitrary: n) |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
441 |
case 0 |
14577 | 442 |
show ?case by simp |
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
443 |
next |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
444 |
case (Suc m) |
14577 | 445 |
show ?case |
446 |
proof (cases n) |
|
447 |
case 0 |
|
30996 | 448 |
with Suc.prems Suc.hyps have "a * a ^ m \<le> 1" by simp |
14577 | 449 |
with gt1 show ?thesis |
450 |
by (force simp only: power_gt1_lemma |
|
30996 | 451 |
not_less [symmetric]) |
14577 | 452 |
next |
453 |
case (Suc n) |
|
30996 | 454 |
with Suc.prems Suc.hyps show ?thesis |
14577 | 455 |
by (force dest: mult_left_le_imp_le |
30996 | 456 |
simp add: less_trans [OF zero_less_one gt1]) |
14577 | 457 |
qed |
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
458 |
qed |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
459 |
|
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
460 |
lemma of_nat_zero_less_power_iff [simp]: |
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
461 |
"of_nat x ^ n > 0 \<longleftrightarrow> x > 0 \<or> n = 0" |
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
462 |
by (induct n) auto |
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
463 |
|
61799 | 464 |
text\<open>Surely we can strengthen this? It holds for \<open>0<a<1\<close> too.\<close> |
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
465 |
lemma power_inject_exp [simp]: |
30996 | 466 |
"1 < a \<Longrightarrow> a ^ m = a ^ n \<longleftrightarrow> m = n" |
14577 | 467 |
by (force simp add: order_antisym power_le_imp_le_exp) |
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
468 |
|
60758 | 469 |
text\<open>Can relax the first premise to @{term "0<a"} in the case of the |
470 |
natural numbers.\<close> |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
471 |
lemma power_less_imp_less_exp: |
30996 | 472 |
"1 < a \<Longrightarrow> a ^ m < a ^ n \<Longrightarrow> m < n" |
473 |
by (simp add: order_less_le [of m n] less_le [of "a^m" "a^n"] |
|
474 |
power_le_imp_le_exp) |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
475 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
476 |
lemma power_strict_mono [rule_format]: |
30996 | 477 |
"a < b \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 < n \<longrightarrow> a ^ n < b ^ n" |
478 |
by (induct n) |
|
479 |
(auto simp add: mult_strict_mono le_less_trans [of 0 a b]) |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
480 |
|
61799 | 481 |
text\<open>Lemma for \<open>power_strict_decreasing\<close>\<close> |
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
482 |
lemma power_Suc_less: |
30996 | 483 |
"0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a * a ^ n < a ^ n" |
484 |
by (induct n) |
|
485 |
(auto simp add: mult_strict_left_mono) |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
486 |
|
30996 | 487 |
lemma power_strict_decreasing [rule_format]: |
488 |
"n < N \<Longrightarrow> 0 < a \<Longrightarrow> a < 1 \<longrightarrow> a ^ N < a ^ n" |
|
489 |
proof (induct N) |
|
490 |
case 0 then show ?case by simp |
|
491 |
next |
|
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
492 |
case (Suc N) then show ?case |
30996 | 493 |
apply (auto simp add: power_Suc_less less_Suc_eq) |
494 |
apply (subgoal_tac "a * a^N < 1 * a^n") |
|
495 |
apply simp |
|
496 |
apply (rule mult_strict_mono) apply auto |
|
497 |
done |
|
498 |
qed |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
499 |
|
61799 | 500 |
text\<open>Proof resembles that of \<open>power_strict_decreasing\<close>\<close> |
30996 | 501 |
lemma power_decreasing [rule_format]: |
502 |
"n \<le> N \<Longrightarrow> 0 \<le> a \<Longrightarrow> a \<le> 1 \<longrightarrow> a ^ N \<le> a ^ n" |
|
503 |
proof (induct N) |
|
504 |
case 0 then show ?case by simp |
|
505 |
next |
|
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
506 |
case (Suc N) then show ?case |
30996 | 507 |
apply (auto simp add: le_Suc_eq) |
508 |
apply (subgoal_tac "a * a^N \<le> 1 * a^n", simp) |
|
509 |
apply (rule mult_mono) apply auto |
|
510 |
done |
|
511 |
qed |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
512 |
|
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
513 |
lemma power_Suc_less_one: |
30996 | 514 |
"0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a ^ Suc n < 1" |
515 |
using power_strict_decreasing [of 0 "Suc n" a] by simp |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
516 |
|
61799 | 517 |
text\<open>Proof again resembles that of \<open>power_strict_decreasing\<close>\<close> |
30996 | 518 |
lemma power_increasing [rule_format]: |
519 |
"n \<le> N \<Longrightarrow> 1 \<le> a \<Longrightarrow> a ^ n \<le> a ^ N" |
|
520 |
proof (induct N) |
|
521 |
case 0 then show ?case by simp |
|
522 |
next |
|
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
523 |
case (Suc N) then show ?case |
30996 | 524 |
apply (auto simp add: le_Suc_eq) |
525 |
apply (subgoal_tac "1 * a^n \<le> a * a^N", simp) |
|
526 |
apply (rule mult_mono) apply (auto simp add: order_trans [OF zero_le_one]) |
|
527 |
done |
|
528 |
qed |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
529 |
|
61799 | 530 |
text\<open>Lemma for \<open>power_strict_increasing\<close>\<close> |
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
531 |
lemma power_less_power_Suc: |
30996 | 532 |
"1 < a \<Longrightarrow> a ^ n < a * a ^ n" |
533 |
by (induct n) (auto simp add: mult_strict_left_mono less_trans [OF zero_less_one]) |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
534 |
|
30996 | 535 |
lemma power_strict_increasing [rule_format]: |
536 |
"n < N \<Longrightarrow> 1 < a \<longrightarrow> a ^ n < a ^ N" |
|
537 |
proof (induct N) |
|
538 |
case 0 then show ?case by simp |
|
539 |
next |
|
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
540 |
case (Suc N) then show ?case |
30996 | 541 |
apply (auto simp add: power_less_power_Suc less_Suc_eq) |
542 |
apply (subgoal_tac "1 * a^n < a * a^N", simp) |
|
543 |
apply (rule mult_strict_mono) apply (auto simp add: less_trans [OF zero_less_one] less_imp_le) |
|
544 |
done |
|
545 |
qed |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
546 |
|
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25062
diff
changeset
|
547 |
lemma power_increasing_iff [simp]: |
30996 | 548 |
"1 < b \<Longrightarrow> b ^ x \<le> b ^ y \<longleftrightarrow> x \<le> y" |
549 |
by (blast intro: power_le_imp_le_exp power_increasing less_imp_le) |
|
15066 | 550 |
|
551 |
lemma power_strict_increasing_iff [simp]: |
|
30996 | 552 |
"1 < b \<Longrightarrow> b ^ x < b ^ y \<longleftrightarrow> x < y" |
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
553 |
by (blast intro: power_less_imp_less_exp power_strict_increasing) |
15066 | 554 |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
555 |
lemma power_le_imp_le_base: |
30996 | 556 |
assumes le: "a ^ Suc n \<le> b ^ Suc n" |
557 |
and ynonneg: "0 \<le> b" |
|
558 |
shows "a \<le> b" |
|
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25062
diff
changeset
|
559 |
proof (rule ccontr) |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25062
diff
changeset
|
560 |
assume "~ a \<le> b" |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25062
diff
changeset
|
561 |
then have "b < a" by (simp only: linorder_not_le) |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25062
diff
changeset
|
562 |
then have "b ^ Suc n < a ^ Suc n" |
41550 | 563 |
by (simp only: assms power_strict_mono) |
30996 | 564 |
from le and this show False |
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25062
diff
changeset
|
565 |
by (simp add: linorder_not_less [symmetric]) |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25062
diff
changeset
|
566 |
qed |
14577 | 567 |
|
22853 | 568 |
lemma power_less_imp_less_base: |
569 |
assumes less: "a ^ n < b ^ n" |
|
570 |
assumes nonneg: "0 \<le> b" |
|
571 |
shows "a < b" |
|
572 |
proof (rule contrapos_pp [OF less]) |
|
573 |
assume "~ a < b" |
|
574 |
hence "b \<le> a" by (simp only: linorder_not_less) |
|
575 |
hence "b ^ n \<le> a ^ n" using nonneg by (rule power_mono) |
|
30996 | 576 |
thus "\<not> a ^ n < b ^ n" by (simp only: linorder_not_less) |
22853 | 577 |
qed |
578 |
||
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
579 |
lemma power_inject_base: |
30996 | 580 |
"a ^ Suc n = b ^ Suc n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a = b" |
581 |
by (blast intro: power_le_imp_le_base antisym eq_refl sym) |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
582 |
|
22955 | 583 |
lemma power_eq_imp_eq_base: |
30996 | 584 |
"a ^ n = b ^ n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 < n \<Longrightarrow> a = b" |
585 |
by (cases n) (simp_all del: power_Suc, rule power_inject_base) |
|
22955 | 586 |
|
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
587 |
lemma power2_le_imp_le: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset
|
588 |
"x\<^sup>2 \<le> y\<^sup>2 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y" |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
589 |
unfolding numeral_2_eq_2 by (rule power_le_imp_le_base) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
590 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
591 |
lemma power2_less_imp_less: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset
|
592 |
"x\<^sup>2 < y\<^sup>2 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x < y" |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
593 |
by (rule power_less_imp_less_base) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
594 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
595 |
lemma power2_eq_imp_eq: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset
|
596 |
"x\<^sup>2 = y\<^sup>2 \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x = y" |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
597 |
unfolding numeral_2_eq_2 by (erule (2) power_eq_imp_eq_base) simp |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
598 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
599 |
end |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
600 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
601 |
context linordered_ring_strict |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
602 |
begin |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
603 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
604 |
lemma sum_squares_eq_zero_iff: |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
605 |
"x * x + y * y = 0 \<longleftrightarrow> x = 0 \<and> y = 0" |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
606 |
by (simp add: add_nonneg_eq_0_iff) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
607 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
608 |
lemma sum_squares_le_zero_iff: |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
609 |
"x * x + y * y \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0" |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
610 |
by (simp add: le_less not_sum_squares_lt_zero sum_squares_eq_zero_iff) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
611 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
612 |
lemma sum_squares_gt_zero_iff: |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
613 |
"0 < x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0" |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
614 |
by (simp add: not_le [symmetric] sum_squares_le_zero_iff) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
615 |
|
30996 | 616 |
end |
617 |
||
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
haftmann
parents:
33364
diff
changeset
|
618 |
context linordered_idom |
30996 | 619 |
begin |
29978
33df3c4eb629
generalize le_imp_power_dvd and power_le_dvd; move from Divides to Power
huffman
parents:
29608
diff
changeset
|
620 |
|
61944 | 621 |
lemma power_abs: "\<bar>a ^ n\<bar> = \<bar>a\<bar> ^ n" |
30996 | 622 |
by (induct n) (auto simp add: abs_mult) |
623 |
||
61944 | 624 |
lemma abs_power_minus [simp]: "\<bar>(-a) ^ n\<bar> = \<bar>a ^ n\<bar>" |
35216 | 625 |
by (simp add: power_abs) |
30996 | 626 |
|
61944 | 627 |
lemma zero_less_power_abs_iff [simp]: "0 < \<bar>a\<bar> ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0" |
30996 | 628 |
proof (induct n) |
629 |
case 0 show ?case by simp |
|
630 |
next |
|
631 |
case (Suc n) show ?case by (auto simp add: Suc zero_less_mult_iff) |
|
29978
33df3c4eb629
generalize le_imp_power_dvd and power_le_dvd; move from Divides to Power
huffman
parents:
29608
diff
changeset
|
632 |
qed |
33df3c4eb629
generalize le_imp_power_dvd and power_le_dvd; move from Divides to Power
huffman
parents:
29608
diff
changeset
|
633 |
|
61944 | 634 |
lemma zero_le_power_abs [simp]: "0 \<le> \<bar>a\<bar> ^ n" |
30996 | 635 |
by (rule zero_le_power [OF abs_ge_zero]) |
636 |
||
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
637 |
lemma zero_le_power2 [simp]: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset
|
638 |
"0 \<le> a\<^sup>2" |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
639 |
by (simp add: power2_eq_square) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
640 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
641 |
lemma zero_less_power2 [simp]: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset
|
642 |
"0 < a\<^sup>2 \<longleftrightarrow> a \<noteq> 0" |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
643 |
by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
644 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
645 |
lemma power2_less_0 [simp]: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset
|
646 |
"\<not> a\<^sup>2 < 0" |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
647 |
by (force simp add: power2_eq_square mult_less_0_iff) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
648 |
|
58787 | 649 |
lemma power2_less_eq_zero_iff [simp]: |
650 |
"a\<^sup>2 \<le> 0 \<longleftrightarrow> a = 0" |
|
651 |
by (simp add: le_less) |
|
652 |
||
61944 | 653 |
lemma abs_power2 [simp]: "\<bar>a\<^sup>2\<bar> = a\<^sup>2" |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
654 |
by (simp add: power2_eq_square abs_mult abs_mult_self) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
655 |
|
61944 | 656 |
lemma power2_abs [simp]: "\<bar>a\<bar>\<^sup>2 = a\<^sup>2" |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
657 |
by (simp add: power2_eq_square abs_mult_self) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
658 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
659 |
lemma odd_power_less_zero: |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
660 |
"a < 0 \<Longrightarrow> a ^ Suc (2*n) < 0" |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
661 |
proof (induct n) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
662 |
case 0 |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
663 |
then show ?case by simp |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
664 |
next |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
665 |
case (Suc n) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
666 |
have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)" |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
667 |
by (simp add: ac_simps power_add power2_eq_square) |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
668 |
thus ?case |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
669 |
by (simp del: power_Suc add: Suc mult_less_0_iff mult_neg_neg) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
670 |
qed |
30996 | 671 |
|
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
672 |
lemma odd_0_le_power_imp_0_le: |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
673 |
"0 \<le> a ^ Suc (2*n) \<Longrightarrow> 0 \<le> a" |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
674 |
using odd_power_less_zero [of a n] |
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
675 |
by (force simp add: linorder_not_less [symmetric]) |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
676 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
677 |
lemma zero_le_even_power'[simp]: |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
678 |
"0 \<le> a ^ (2*n)" |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
679 |
proof (induct n) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
680 |
case 0 |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
681 |
show ?case by simp |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
682 |
next |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
683 |
case (Suc n) |
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
684 |
have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)" |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
685 |
by (simp add: ac_simps power_add power2_eq_square) |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
686 |
thus ?case |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
687 |
by (simp add: Suc zero_le_mult_iff) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
688 |
qed |
30996 | 689 |
|
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
690 |
lemma sum_power2_ge_zero: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset
|
691 |
"0 \<le> x\<^sup>2 + y\<^sup>2" |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
692 |
by (intro add_nonneg_nonneg zero_le_power2) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
693 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
694 |
lemma not_sum_power2_lt_zero: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset
|
695 |
"\<not> x\<^sup>2 + y\<^sup>2 < 0" |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
696 |
unfolding not_less by (rule sum_power2_ge_zero) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
697 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
698 |
lemma sum_power2_eq_zero_iff: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset
|
699 |
"x\<^sup>2 + y\<^sup>2 = 0 \<longleftrightarrow> x = 0 \<and> y = 0" |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
700 |
unfolding power2_eq_square by (simp add: add_nonneg_eq_0_iff) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
701 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
702 |
lemma sum_power2_le_zero_iff: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset
|
703 |
"x\<^sup>2 + y\<^sup>2 \<le> 0 \<longleftrightarrow> x = 0 \<and> y = 0" |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
704 |
by (simp add: le_less sum_power2_eq_zero_iff not_sum_power2_lt_zero) |
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
705 |
|
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
706 |
lemma sum_power2_gt_zero_iff: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset
|
707 |
"0 < x\<^sup>2 + y\<^sup>2 \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0" |
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
708 |
unfolding not_le [symmetric] by (simp add: sum_power2_le_zero_iff) |
30996 | 709 |
|
59865
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
710 |
lemma abs_le_square_iff: |
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
711 |
"\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> x\<^sup>2 \<le> y\<^sup>2" |
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
712 |
proof |
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
713 |
assume "\<bar>x\<bar> \<le> \<bar>y\<bar>" |
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
714 |
then have "\<bar>x\<bar>\<^sup>2 \<le> \<bar>y\<bar>\<^sup>2" by (rule power_mono, simp) |
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
715 |
then show "x\<^sup>2 \<le> y\<^sup>2" by simp |
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
716 |
next |
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
717 |
assume "x\<^sup>2 \<le> y\<^sup>2" |
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
718 |
then show "\<bar>x\<bar> \<le> \<bar>y\<bar>" |
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
719 |
by (auto intro!: power2_le_imp_le [OF _ abs_ge_zero]) |
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
720 |
qed |
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
721 |
|
61944 | 722 |
lemma abs_square_le_1:"x\<^sup>2 \<le> 1 \<longleftrightarrow> \<bar>x\<bar> \<le> 1" |
59865
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
723 |
using abs_le_square_iff [of x 1] |
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
724 |
by simp |
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
725 |
|
61944 | 726 |
lemma abs_square_eq_1: "x\<^sup>2 = 1 \<longleftrightarrow> \<bar>x\<bar> = 1" |
59865
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
727 |
by (auto simp add: abs_if power2_eq_1_iff) |
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
728 |
|
61944 | 729 |
lemma abs_square_less_1: "x\<^sup>2 < 1 \<longleftrightarrow> \<bar>x\<bar> < 1" |
59865
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
730 |
using abs_square_eq_1 [of x] abs_square_le_1 [of x] |
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
731 |
by (auto simp add: le_less) |
8a20dd967385
rationalised and generalised some theorems concerning abs and x^2.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
732 |
|
30996 | 733 |
end |
734 |
||
29978
33df3c4eb629
generalize le_imp_power_dvd and power_le_dvd; move from Divides to Power
huffman
parents:
29608
diff
changeset
|
735 |
|
60758 | 736 |
subsection \<open>Miscellaneous rules\<close> |
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
737 |
|
60867 | 738 |
lemma (in linordered_semidom) self_le_power: |
739 |
"1 \<le> a \<Longrightarrow> 0 < n \<Longrightarrow> a \<le> a ^ n" |
|
740 |
using power_increasing [of 1 n a] power_one_right [of a] by auto |
|
55718
34618f031ba9
A few lemmas about summations, etc.
paulson <lp15@cam.ac.uk>
parents:
55096
diff
changeset
|
741 |
|
60867 | 742 |
lemma (in power) power_eq_if: |
743 |
"p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))" |
|
47255
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset
|
744 |
unfolding One_nat_def by (cases m) simp_all |
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset
|
745 |
|
58787 | 746 |
lemma (in comm_semiring_1) power2_sum: |
747 |
"(x + y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 + 2 * x * y" |
|
47192
0c0501cb6da6
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
huffman
parents:
47191
diff
changeset
|
748 |
by (simp add: algebra_simps power2_eq_square mult_2_right) |
30996 | 749 |
|
58787 | 750 |
lemma (in comm_ring_1) power2_diff: |
751 |
"(x - y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 - 2 * x * y" |
|
752 |
by (simp add: algebra_simps power2_eq_square mult_2_right) |
|
30996 | 753 |
|
60974
6a6f15d8fbc4
New material and fixes related to the forthcoming Stone-Weierstrass development
paulson <lp15@cam.ac.uk>
parents:
60867
diff
changeset
|
754 |
lemma (in comm_ring_1) power2_commute: |
6a6f15d8fbc4
New material and fixes related to the forthcoming Stone-Weierstrass development
paulson <lp15@cam.ac.uk>
parents:
60867
diff
changeset
|
755 |
"(x - y)\<^sup>2 = (y - x)\<^sup>2" |
6a6f15d8fbc4
New material and fixes related to the forthcoming Stone-Weierstrass development
paulson <lp15@cam.ac.uk>
parents:
60867
diff
changeset
|
756 |
by (simp add: algebra_simps power2_eq_square) |
6a6f15d8fbc4
New material and fixes related to the forthcoming Stone-Weierstrass development
paulson <lp15@cam.ac.uk>
parents:
60867
diff
changeset
|
757 |
|
30313 | 758 |
|
60758 | 759 |
text \<open>Simprules for comparisons where common factors can be cancelled.\<close> |
47255
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset
|
760 |
|
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset
|
761 |
lemmas zero_compare_simps = |
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset
|
762 |
add_strict_increasing add_strict_increasing2 add_increasing |
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
763 |
zero_le_mult_iff zero_le_divide_iff |
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
764 |
zero_less_mult_iff zero_less_divide_iff |
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
765 |
mult_le_0_iff divide_le_0_iff |
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
766 |
mult_less_0_iff divide_less_0_iff |
47255
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset
|
767 |
zero_le_power2 power2_less_0 |
30a1692557b0
removed Nat_Numeral.thy, moving all theorems elsewhere
huffman
parents:
47241
diff
changeset
|
768 |
|
30313 | 769 |
|
60758 | 770 |
subsection \<open>Exponentiation for the Natural Numbers\<close> |
14577 | 771 |
|
30996 | 772 |
lemma nat_one_le_power [simp]: |
773 |
"Suc 0 \<le> i \<Longrightarrow> Suc 0 \<le> i ^ n" |
|
774 |
by (rule one_le_power [of i n, unfolded One_nat_def]) |
|
23305 | 775 |
|
30996 | 776 |
lemma nat_zero_less_power_iff [simp]: |
777 |
"x ^ n > 0 \<longleftrightarrow> x > (0::nat) \<or> n = 0" |
|
778 |
by (induct n) auto |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
779 |
|
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
780 |
lemma nat_power_eq_Suc_0_iff [simp]: |
30996 | 781 |
"x ^ m = Suc 0 \<longleftrightarrow> m = 0 \<or> x = Suc 0" |
782 |
by (induct m) auto |
|
30056 | 783 |
|
30996 | 784 |
lemma power_Suc_0 [simp]: |
785 |
"Suc 0 ^ n = Suc 0" |
|
786 |
by simp |
|
30056 | 787 |
|
61799 | 788 |
text\<open>Valid for the naturals, but what if \<open>0<i<1\<close>? |
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
789 |
Premises cannot be weakened: consider the case where @{term "i=0"}, |
60758 | 790 |
@{term "m=1"} and @{term "n=0"}.\<close> |
21413 | 791 |
lemma nat_power_less_imp_less: |
61076 | 792 |
assumes nonneg: "0 < (i::nat)" |
30996 | 793 |
assumes less: "i ^ m < i ^ n" |
21413 | 794 |
shows "m < n" |
795 |
proof (cases "i = 1") |
|
796 |
case True with less power_one [where 'a = nat] show ?thesis by simp |
|
797 |
next |
|
798 |
case False with nonneg have "1 < i" by auto |
|
799 |
from power_strict_increasing_iff [OF this] less show ?thesis .. |
|
800 |
qed |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
8844
diff
changeset
|
801 |
|
33274
b6ff7db522b5
moved lemmas for dvd on nat to theories Nat and Power
haftmann
parents:
31998
diff
changeset
|
802 |
lemma power_dvd_imp_le: |
b6ff7db522b5
moved lemmas for dvd on nat to theories Nat and Power
haftmann
parents:
31998
diff
changeset
|
803 |
"i ^ m dvd i ^ n \<Longrightarrow> (1::nat) < i \<Longrightarrow> m \<le> n" |
b6ff7db522b5
moved lemmas for dvd on nat to theories Nat and Power
haftmann
parents:
31998
diff
changeset
|
804 |
apply (rule power_le_imp_le_exp, assumption) |
b6ff7db522b5
moved lemmas for dvd on nat to theories Nat and Power
haftmann
parents:
31998
diff
changeset
|
805 |
apply (erule dvd_imp_le, simp) |
b6ff7db522b5
moved lemmas for dvd on nat to theories Nat and Power
haftmann
parents:
31998
diff
changeset
|
806 |
done |
b6ff7db522b5
moved lemmas for dvd on nat to theories Nat and Power
haftmann
parents:
31998
diff
changeset
|
807 |
|
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49824
diff
changeset
|
808 |
lemma power2_nat_le_eq_le: |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49824
diff
changeset
|
809 |
fixes m n :: nat |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset
|
810 |
shows "m\<^sup>2 \<le> n\<^sup>2 \<longleftrightarrow> m \<le> n" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49824
diff
changeset
|
811 |
by (auto intro: power2_le_imp_le power_mono) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49824
diff
changeset
|
812 |
|
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49824
diff
changeset
|
813 |
lemma power2_nat_le_imp_le: |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49824
diff
changeset
|
814 |
fixes m n :: nat |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52435
diff
changeset
|
815 |
assumes "m\<^sup>2 \<le> n" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49824
diff
changeset
|
816 |
shows "m \<le> n" |
54249 | 817 |
proof (cases m) |
818 |
case 0 then show ?thesis by simp |
|
819 |
next |
|
820 |
case (Suc k) |
|
821 |
show ?thesis |
|
822 |
proof (rule ccontr) |
|
823 |
assume "\<not> m \<le> n" |
|
824 |
then have "n < m" by simp |
|
825 |
with assms Suc show False |
|
60867 | 826 |
by (simp add: power2_eq_square) |
54249 | 827 |
qed |
828 |
qed |
|
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
49824
diff
changeset
|
829 |
|
60758 | 830 |
subsubsection \<open>Cardinality of the Powerset\<close> |
55096 | 831 |
|
832 |
lemma card_UNIV_bool [simp]: "card (UNIV :: bool set) = 2" |
|
833 |
unfolding UNIV_bool by simp |
|
834 |
||
835 |
lemma card_Pow: "finite A \<Longrightarrow> card (Pow A) = 2 ^ card A" |
|
836 |
proof (induct rule: finite_induct) |
|
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
837 |
case empty |
55096 | 838 |
show ?case by auto |
839 |
next |
|
840 |
case (insert x A) |
|
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
841 |
then have "inj_on (insert x) (Pow A)" |
55096 | 842 |
unfolding inj_on_def by (blast elim!: equalityE) |
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
843 |
then have "card (Pow A) + card (insert x ` Pow A) = 2 * 2 ^ card A" |
55096 | 844 |
by (simp add: mult_2 card_image Pow_insert insert.hyps) |
845 |
then show ?case using insert |
|
846 |
apply (simp add: Pow_insert) |
|
847 |
apply (subst card_Un_disjoint, auto) |
|
848 |
done |
|
849 |
qed |
|
850 |
||
57418 | 851 |
|
60758 | 852 |
subsubsection \<open>Generalized sum over a set\<close> |
57418 | 853 |
|
854 |
lemma setsum_zero_power [simp]: |
|
855 |
fixes c :: "nat \<Rightarrow> 'a::division_ring" |
|
856 |
shows "(\<Sum>i\<in>A. c i * 0^i) = (if finite A \<and> 0 \<in> A then c 0 else 0)" |
|
857 |
apply (cases "finite A") |
|
858 |
by (induction A rule: finite_induct) auto |
|
859 |
||
860 |
lemma setsum_zero_power' [simp]: |
|
861 |
fixes c :: "nat \<Rightarrow> 'a::field" |
|
862 |
shows "(\<Sum>i\<in>A. c i * 0^i / d i) = (if finite A \<and> 0 \<in> A then c 0 / d 0 else 0)" |
|
863 |
using setsum_zero_power [of "\<lambda>i. c i / d i" A] |
|
864 |
by auto |
|
865 |
||
866 |
||
60758 | 867 |
subsubsection \<open>Generalized product over a set\<close> |
55096 | 868 |
|
869 |
lemma setprod_constant: "finite A ==> (\<Prod>x\<in> A. (y::'a::{comm_monoid_mult})) = y^(card A)" |
|
870 |
apply (erule finite_induct) |
|
871 |
apply auto |
|
872 |
done |
|
873 |
||
57418 | 874 |
lemma setprod_power_distrib: |
875 |
fixes f :: "'a \<Rightarrow> 'b::comm_semiring_1" |
|
876 |
shows "setprod f A ^ n = setprod (\<lambda>x. (f x) ^ n) A" |
|
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
877 |
proof (cases "finite A") |
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
878 |
case True then show ?thesis |
57418 | 879 |
by (induct A rule: finite_induct) (auto simp add: power_mult_distrib) |
880 |
next |
|
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
881 |
case False then show ?thesis |
57418 | 882 |
by simp |
883 |
qed |
|
884 |
||
58437 | 885 |
lemma power_setsum: |
886 |
"c ^ (\<Sum>a\<in>A. f a) = (\<Prod>a\<in>A. c ^ f a)" |
|
887 |
by (induct A rule: infinite_finite_induct) (simp_all add: power_add) |
|
888 |
||
55096 | 889 |
lemma setprod_gen_delta: |
890 |
assumes fS: "finite S" |
|
891 |
shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::comm_monoid_mult) * c^ (card S - 1) else c^ card S)" |
|
892 |
proof- |
|
893 |
let ?f = "(\<lambda>k. if k=a then b k else c)" |
|
894 |
{assume a: "a \<notin> S" |
|
895 |
hence "\<forall> k\<in> S. ?f k = c" by simp |
|
896 |
hence ?thesis using a setprod_constant[OF fS, of c] by simp } |
|
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
897 |
moreover |
55096 | 898 |
{assume a: "a \<in> S" |
899 |
let ?A = "S - {a}" |
|
900 |
let ?B = "{a}" |
|
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
901 |
have eq: "S = ?A \<union> ?B" using a by blast |
55096 | 902 |
have dj: "?A \<inter> ?B = {}" by simp |
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
903 |
from fS have fAB: "finite ?A" "finite ?B" by auto |
55096 | 904 |
have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A" |
57418 | 905 |
apply (rule setprod.cong) by auto |
55096 | 906 |
have cA: "card ?A = card S - 1" using fS a by auto |
907 |
have fA1: "setprod ?f ?A = c ^ card ?A" unfolding fA0 apply (rule setprod_constant) using fS by auto |
|
908 |
have "setprod ?f ?A * setprod ?f ?B = setprod ?f S" |
|
57418 | 909 |
using setprod.union_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]] |
55096 | 910 |
by simp |
911 |
then have ?thesis using a cA |
|
57418 | 912 |
by (simp add: fA1 field_simps cong add: setprod.cong cong del: if_weak_cong)} |
55096 | 913 |
ultimately show ?thesis by blast |
914 |
qed |
|
915 |
||
60758 | 916 |
subsection \<open>Code generator tweak\<close> |
31155
92d8ff6af82c
monomorphic code generation for power operations
haftmann
parents:
31021
diff
changeset
|
917 |
|
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51263
diff
changeset
|
918 |
code_identifier |
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51263
diff
changeset
|
919 |
code_module Power \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith |
33364 | 920 |
|
3390
0c7625196d95
New theory "Power" of exponentiation (and binomial coefficients)
paulson
parents:
diff
changeset
|
921 |
end |