equal
deleted
inserted
replaced
207 |
207 |
208 lemma nonzero_of_real_divide: |
208 lemma nonzero_of_real_divide: |
209 "y \<noteq> 0 \<Longrightarrow> of_real (x / y) = |
209 "y \<noteq> 0 \<Longrightarrow> of_real (x / y) = |
210 (of_real x / of_real y :: 'a::real_field)" |
210 (of_real x / of_real y :: 'a::real_field)" |
211 by (simp add: divide_inverse nonzero_of_real_inverse) |
211 by (simp add: divide_inverse nonzero_of_real_inverse) |
212 |
212 |
213 lemma of_real_divide: |
213 lemma of_real_divide [simp]: |
214 "of_real (x / y) = |
214 "of_real (x / y) = |
215 (of_real x / of_real y :: 'a::{real_field,division_by_zero})" |
215 (of_real x / of_real y :: 'a::{real_field,division_by_zero})" |
216 by (simp add: divide_inverse) |
216 by (simp add: divide_inverse) |
|
217 |
|
218 lemma of_real_power [simp]: |
|
219 "of_real (x ^ n) = (of_real x :: 'a::{real_algebra_1,recpower}) ^ n" |
|
220 by (induct n, simp_all add: power_Suc) |
217 |
221 |
218 lemma of_real_eq_iff [simp]: "(of_real x = of_real y) = (x = y)" |
222 lemma of_real_eq_iff [simp]: "(of_real x = of_real y) = (x = y)" |
219 by (simp add: of_real_def scaleR_cancel_right) |
223 by (simp add: of_real_def scaleR_cancel_right) |
220 |
224 |
221 lemmas of_real_eq_0_iff [simp] = of_real_eq_iff [of _ 0, simplified] |
225 lemmas of_real_eq_0_iff [simp] = of_real_eq_iff [of _ 0, simplified] |
321 fixes a b :: "'a::{real_field,division_by_zero}" |
325 fixes a b :: "'a::{real_field,division_by_zero}" |
322 shows "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a / b \<in> Reals" |
326 shows "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a / b \<in> Reals" |
323 apply (auto simp add: Reals_def) |
327 apply (auto simp add: Reals_def) |
324 apply (rule range_eqI) |
328 apply (rule range_eqI) |
325 apply (rule of_real_divide [symmetric]) |
329 apply (rule of_real_divide [symmetric]) |
|
330 done |
|
331 |
|
332 lemma Reals_power [simp]: |
|
333 fixes a :: "'a::{real_algebra_1,recpower}" |
|
334 shows "a \<in> Reals \<Longrightarrow> a ^ n \<in> Reals" |
|
335 apply (auto simp add: Reals_def) |
|
336 apply (rule range_eqI) |
|
337 apply (rule of_real_power [symmetric]) |
326 done |
338 done |
327 |
339 |
328 lemma Reals_cases [cases set: Reals]: |
340 lemma Reals_cases [cases set: Reals]: |
329 assumes "q \<in> \<real>" |
341 assumes "q \<in> \<real>" |
330 obtains (of_real) r where "q = of_real r" |
342 obtains (of_real) r where "q = of_real r" |