|
1 (* Title : HOL/RealPow.thy |
|
2 Author : Jacques D. Fleuriot |
|
3 Copyright : 1998 University of Cambridge |
|
4 *) |
|
5 |
|
6 header {* Natural powers theory *} |
|
7 |
|
8 theory RealPow |
|
9 imports RealDef |
|
10 uses ("Tools/float_syntax.ML") |
|
11 begin |
|
12 |
|
13 declare abs_mult_self [simp] |
|
14 |
|
15 instantiation real :: recpower |
|
16 begin |
|
17 |
|
18 primrec power_real where |
|
19 realpow_0: "r ^ 0 = (1\<Colon>real)" |
|
20 | realpow_Suc: "r ^ Suc n = (r\<Colon>real) * r ^ n" |
|
21 |
|
22 instance proof |
|
23 fix z :: real |
|
24 fix n :: nat |
|
25 show "z^0 = 1" by simp |
|
26 show "z^(Suc n) = z * (z^n)" by simp |
|
27 qed |
|
28 |
|
29 end |
|
30 |
|
31 |
|
32 lemma two_realpow_ge_one [simp]: "(1::real) \<le> 2 ^ n" |
|
33 by simp |
|
34 |
|
35 lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n" |
|
36 apply (induct "n") |
|
37 apply (auto simp add: real_of_nat_Suc) |
|
38 apply (subst mult_2) |
|
39 apply (rule add_less_le_mono) |
|
40 apply (auto simp add: two_realpow_ge_one) |
|
41 done |
|
42 |
|
43 lemma realpow_Suc_le_self: "[| 0 \<le> r; r \<le> (1::real) |] ==> r ^ Suc n \<le> r" |
|
44 by (insert power_decreasing [of 1 "Suc n" r], simp) |
|
45 |
|
46 lemma realpow_minus_mult [rule_format]: |
|
47 "0 < n --> (x::real) ^ (n - 1) * x = x ^ n" |
|
48 apply (simp split add: nat_diff_split) |
|
49 done |
|
50 |
|
51 lemma realpow_two_mult_inverse [simp]: |
|
52 "r \<noteq> 0 ==> r * inverse r ^Suc (Suc 0) = inverse (r::real)" |
|
53 by (simp add: real_mult_assoc [symmetric]) |
|
54 |
|
55 lemma realpow_two_minus [simp]: "(-x)^Suc (Suc 0) = (x::real)^Suc (Suc 0)" |
|
56 by simp |
|
57 |
|
58 lemma realpow_two_diff: |
|
59 "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)" |
|
60 apply (unfold real_diff_def) |
|
61 apply (simp add: ring_simps) |
|
62 done |
|
63 |
|
64 lemma realpow_two_disj: |
|
65 "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)" |
|
66 apply (cut_tac x = x and y = y in realpow_two_diff) |
|
67 apply (auto simp del: realpow_Suc) |
|
68 done |
|
69 |
|
70 lemma realpow_real_of_nat: "real (m::nat) ^ n = real (m ^ n)" |
|
71 apply (induct "n") |
|
72 apply (auto simp add: real_of_nat_one real_of_nat_mult) |
|
73 done |
|
74 |
|
75 lemma realpow_real_of_nat_two_pos [simp] : "0 < real (Suc (Suc 0) ^ n)" |
|
76 apply (induct "n") |
|
77 apply (auto simp add: real_of_nat_mult zero_less_mult_iff) |
|
78 done |
|
79 |
|
80 (* used by AFP Integration theory *) |
|
81 lemma realpow_increasing: |
|
82 "[|(0::real) \<le> x; 0 \<le> y; x ^ Suc n \<le> y ^ Suc n|] ==> x \<le> y" |
|
83 by (rule power_le_imp_le_base) |
|
84 |
|
85 |
|
86 subsection{*Literal Arithmetic Involving Powers, Type @{typ real}*} |
|
87 |
|
88 lemma real_of_int_power: "real (x::int) ^ n = real (x ^ n)" |
|
89 apply (induct "n") |
|
90 apply (simp_all add: nat_mult_distrib) |
|
91 done |
|
92 declare real_of_int_power [symmetric, simp] |
|
93 |
|
94 lemma power_real_number_of: |
|
95 "(number_of v :: real) ^ n = real ((number_of v :: int) ^ n)" |
|
96 by (simp only: real_number_of [symmetric] real_of_int_power) |
|
97 |
|
98 declare power_real_number_of [of _ "number_of w", standard, simp] |
|
99 |
|
100 |
|
101 subsection {* Properties of Squares *} |
|
102 |
|
103 lemma sum_squares_ge_zero: |
|
104 fixes x y :: "'a::ordered_ring_strict" |
|
105 shows "0 \<le> x * x + y * y" |
|
106 by (intro add_nonneg_nonneg zero_le_square) |
|
107 |
|
108 lemma not_sum_squares_lt_zero: |
|
109 fixes x y :: "'a::ordered_ring_strict" |
|
110 shows "\<not> x * x + y * y < 0" |
|
111 by (simp add: linorder_not_less sum_squares_ge_zero) |
|
112 |
|
113 lemma sum_nonneg_eq_zero_iff: |
|
114 fixes x y :: "'a::pordered_ab_group_add" |
|
115 assumes x: "0 \<le> x" and y: "0 \<le> y" |
|
116 shows "(x + y = 0) = (x = 0 \<and> y = 0)" |
|
117 proof (auto) |
|
118 from y have "x + 0 \<le> x + y" by (rule add_left_mono) |
|
119 also assume "x + y = 0" |
|
120 finally have "x \<le> 0" by simp |
|
121 thus "x = 0" using x by (rule order_antisym) |
|
122 next |
|
123 from x have "0 + y \<le> x + y" by (rule add_right_mono) |
|
124 also assume "x + y = 0" |
|
125 finally have "y \<le> 0" by simp |
|
126 thus "y = 0" using y by (rule order_antisym) |
|
127 qed |
|
128 |
|
129 lemma sum_squares_eq_zero_iff: |
|
130 fixes x y :: "'a::ordered_ring_strict" |
|
131 shows "(x * x + y * y = 0) = (x = 0 \<and> y = 0)" |
|
132 by (simp add: sum_nonneg_eq_zero_iff) |
|
133 |
|
134 lemma sum_squares_le_zero_iff: |
|
135 fixes x y :: "'a::ordered_ring_strict" |
|
136 shows "(x * x + y * y \<le> 0) = (x = 0 \<and> y = 0)" |
|
137 by (simp add: order_le_less not_sum_squares_lt_zero sum_squares_eq_zero_iff) |
|
138 |
|
139 lemma sum_squares_gt_zero_iff: |
|
140 fixes x y :: "'a::ordered_ring_strict" |
|
141 shows "(0 < x * x + y * y) = (x \<noteq> 0 \<or> y \<noteq> 0)" |
|
142 by (simp add: order_less_le sum_squares_ge_zero sum_squares_eq_zero_iff) |
|
143 |
|
144 lemma sum_power2_ge_zero: |
|
145 fixes x y :: "'a::{ordered_idom,recpower}" |
|
146 shows "0 \<le> x\<twosuperior> + y\<twosuperior>" |
|
147 unfolding power2_eq_square by (rule sum_squares_ge_zero) |
|
148 |
|
149 lemma not_sum_power2_lt_zero: |
|
150 fixes x y :: "'a::{ordered_idom,recpower}" |
|
151 shows "\<not> x\<twosuperior> + y\<twosuperior> < 0" |
|
152 unfolding power2_eq_square by (rule not_sum_squares_lt_zero) |
|
153 |
|
154 lemma sum_power2_eq_zero_iff: |
|
155 fixes x y :: "'a::{ordered_idom,recpower}" |
|
156 shows "(x\<twosuperior> + y\<twosuperior> = 0) = (x = 0 \<and> y = 0)" |
|
157 unfolding power2_eq_square by (rule sum_squares_eq_zero_iff) |
|
158 |
|
159 lemma sum_power2_le_zero_iff: |
|
160 fixes x y :: "'a::{ordered_idom,recpower}" |
|
161 shows "(x\<twosuperior> + y\<twosuperior> \<le> 0) = (x = 0 \<and> y = 0)" |
|
162 unfolding power2_eq_square by (rule sum_squares_le_zero_iff) |
|
163 |
|
164 lemma sum_power2_gt_zero_iff: |
|
165 fixes x y :: "'a::{ordered_idom,recpower}" |
|
166 shows "(0 < x\<twosuperior> + y\<twosuperior>) = (x \<noteq> 0 \<or> y \<noteq> 0)" |
|
167 unfolding power2_eq_square by (rule sum_squares_gt_zero_iff) |
|
168 |
|
169 |
|
170 subsection{* Squares of Reals *} |
|
171 |
|
172 lemma real_two_squares_add_zero_iff [simp]: |
|
173 "(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)" |
|
174 by (rule sum_squares_eq_zero_iff) |
|
175 |
|
176 lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)" |
|
177 by simp |
|
178 |
|
179 lemma real_sum_squares_cancel2: "x * x + y * y = 0 ==> y = (0::real)" |
|
180 by simp |
|
181 |
|
182 lemma real_mult_self_sum_ge_zero: "(0::real) \<le> x*x + y*y" |
|
183 by (rule sum_squares_ge_zero) |
|
184 |
|
185 lemma real_sum_squares_cancel_a: "x * x = -(y * y) ==> x = (0::real) & y=0" |
|
186 by (simp add: real_add_eq_0_iff [symmetric]) |
|
187 |
|
188 lemma real_squared_diff_one_factored: "x*x - (1::real) = (x + 1)*(x - 1)" |
|
189 by (simp add: left_distrib right_diff_distrib) |
|
190 |
|
191 lemma real_mult_is_one [simp]: "(x*x = (1::real)) = (x = 1 | x = - 1)" |
|
192 apply auto |
|
193 apply (drule right_minus_eq [THEN iffD2]) |
|
194 apply (auto simp add: real_squared_diff_one_factored) |
|
195 done |
|
196 |
|
197 lemma real_sum_squares_not_zero: "x ~= 0 ==> x * x + y * y ~= (0::real)" |
|
198 by simp |
|
199 |
|
200 lemma real_sum_squares_not_zero2: "y ~= 0 ==> x * x + y * y ~= (0::real)" |
|
201 by simp |
|
202 |
|
203 lemma realpow_two_sum_zero_iff [simp]: |
|
204 "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)" |
|
205 by (rule sum_power2_eq_zero_iff) |
|
206 |
|
207 lemma realpow_two_le_add_order [simp]: "(0::real) \<le> u ^ 2 + v ^ 2" |
|
208 by (rule sum_power2_ge_zero) |
|
209 |
|
210 lemma realpow_two_le_add_order2 [simp]: "(0::real) \<le> u ^ 2 + v ^ 2 + w ^ 2" |
|
211 by (intro add_nonneg_nonneg zero_le_power2) |
|
212 |
|
213 lemma real_sum_square_gt_zero: "x ~= 0 ==> (0::real) < x * x + y * y" |
|
214 by (simp add: sum_squares_gt_zero_iff) |
|
215 |
|
216 lemma real_sum_square_gt_zero2: "y ~= 0 ==> (0::real) < x * x + y * y" |
|
217 by (simp add: sum_squares_gt_zero_iff) |
|
218 |
|
219 lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))" |
|
220 by (rule_tac j = 0 in real_le_trans, auto) |
|
221 |
|
222 lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2" |
|
223 by (auto simp add: power2_eq_square) |
|
224 |
|
225 (* The following theorem is by Benjamin Porter *) |
|
226 lemma real_sq_order: |
|
227 fixes x::real |
|
228 assumes xgt0: "0 \<le> x" and ygt0: "0 \<le> y" and sq: "x^2 \<le> y^2" |
|
229 shows "x \<le> y" |
|
230 proof - |
|
231 from sq have "x ^ Suc (Suc 0) \<le> y ^ Suc (Suc 0)" |
|
232 by (simp only: numeral_2_eq_2) |
|
233 thus "x \<le> y" using ygt0 |
|
234 by (rule power_le_imp_le_base) |
|
235 qed |
|
236 |
|
237 |
|
238 subsection {*Various Other Theorems*} |
|
239 |
|
240 lemma real_le_add_half_cancel: "(x + y/2 \<le> (y::real)) = (x \<le> y /2)" |
|
241 by auto |
|
242 |
|
243 lemma real_minus_half_eq [simp]: "(x::real) - x/2 = x/2" |
|
244 by auto |
|
245 |
|
246 lemma real_mult_inverse_cancel: |
|
247 "[|(0::real) < x; 0 < x1; x1 * y < x * u |] |
|
248 ==> inverse x * y < inverse x1 * u" |
|
249 apply (rule_tac c=x in mult_less_imp_less_left) |
|
250 apply (auto simp add: real_mult_assoc [symmetric]) |
|
251 apply (simp (no_asm) add: mult_ac) |
|
252 apply (rule_tac c=x1 in mult_less_imp_less_right) |
|
253 apply (auto simp add: mult_ac) |
|
254 done |
|
255 |
|
256 lemma real_mult_inverse_cancel2: |
|
257 "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1" |
|
258 apply (auto dest: real_mult_inverse_cancel simp add: mult_ac) |
|
259 done |
|
260 |
|
261 lemma inverse_real_of_nat_gt_zero [simp]: "0 < inverse (real (Suc n))" |
|
262 by simp |
|
263 |
|
264 lemma inverse_real_of_nat_ge_zero [simp]: "0 \<le> inverse (real (Suc n))" |
|
265 by simp |
|
266 |
|
267 lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))" |
|
268 by (case_tac "n", auto) |
|
269 |
|
270 subsection{* Float syntax *} |
|
271 |
|
272 syntax "_Float" :: "float_const \<Rightarrow> 'a" ("_") |
|
273 |
|
274 use "Tools/float_syntax.ML" |
|
275 setup FloatSyntax.setup |
|
276 |
|
277 text{* Test: *} |
|
278 lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::real)" |
|
279 by simp |
|
280 |
|
281 end |