197 apply (subgoal_tac "real(Suc n) = real n + 1") |
197 apply (subgoal_tac "real(Suc n) = real n + 1") |
198 apply (erule ssubst) |
198 apply (erule ssubst) |
199 apply (subst powr_add, simp, simp) |
199 apply (subst powr_add, simp, simp) |
200 done |
200 done |
201 |
201 |
202 lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0 |
202 lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0 else x powr (real n))" |
203 else x powr (real n))" |
|
204 apply (case_tac "x = 0", simp, simp) |
203 apply (case_tac "x = 0", simp, simp) |
205 apply (rule powr_realpow [THEN sym], simp) |
204 apply (rule powr_realpow [THEN sym], simp) |
206 done |
205 done |
|
206 |
|
207 lemma powr_int: |
|
208 assumes "x > 0" |
|
209 shows "x powr i = (if i \<ge> 0 then x ^ nat i else 1 / x ^ nat (-i))" |
|
210 proof cases |
|
211 assume "i < 0" |
|
212 have r: "x powr i = 1 / x powr (-i)" by (simp add: powr_minus field_simps) |
|
213 show ?thesis using `i < 0` `x > 0` by (simp add: r field_simps powr_realpow[symmetric]) |
|
214 qed (simp add: assms powr_realpow[symmetric]) |
|
215 |
|
216 lemma powr_numeral: "0 < x \<Longrightarrow> x powr numeral n = x^numeral n" |
|
217 using powr_realpow[of x "numeral n"] by simp |
|
218 |
|
219 lemma powr_neg_numeral: "0 < x \<Longrightarrow> x powr neg_numeral n = 1 / x^numeral n" |
|
220 using powr_int[of x "neg_numeral n"] by simp |
207 |
221 |
208 lemma root_powr_inverse: |
222 lemma root_powr_inverse: |
209 "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)" |
223 "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)" |
210 by (auto simp: root_def powr_realpow[symmetric] powr_powr) |
224 by (auto simp: root_def powr_realpow[symmetric] powr_powr) |
211 |
225 |