30 |
30 |
31 lemma SReal_hcmod_hcomplex_of_complex [simp]: |
31 lemma SReal_hcmod_hcomplex_of_complex [simp]: |
32 "hcmod (hcomplex_of_complex r) \<in> Reals" |
32 "hcmod (hcomplex_of_complex r) \<in> Reals" |
33 by (simp add: Reals_eq_Standard) |
33 by (simp add: Reals_eq_Standard) |
34 |
34 |
35 lemma SReal_hcmod_number_of [simp]: "hcmod (number_of w ::hcomplex) \<in> Reals" |
35 lemma SReal_hcmod_numeral [simp]: "hcmod (numeral w ::hcomplex) \<in> Reals" |
36 by (simp add: Reals_eq_Standard) |
36 by (simp add: Reals_eq_Standard) |
37 |
37 |
38 lemma SReal_hcmod_SComplex: "x \<in> SComplex ==> hcmod x \<in> Reals" |
38 lemma SReal_hcmod_SComplex: "x \<in> SComplex ==> hcmod x \<in> Reals" |
39 by (simp add: Reals_eq_Standard) |
39 by (simp add: Reals_eq_Standard) |
40 |
40 |
41 lemma SComplex_divide_number_of: |
41 lemma SComplex_divide_numeral: |
42 "r \<in> SComplex ==> r/(number_of w::hcomplex) \<in> SComplex" |
42 "r \<in> SComplex ==> r/(numeral w::hcomplex) \<in> SComplex" |
43 by simp |
43 by simp |
44 |
44 |
45 lemma SComplex_UNIV_complex: |
45 lemma SComplex_UNIV_complex: |
46 "{x. hcomplex_of_complex x \<in> SComplex} = (UNIV::complex set)" |
46 "{x. hcomplex_of_complex x \<in> SComplex} = (UNIV::complex set)" |
47 by simp |
47 by simp |
209 lemma hcomplex_of_complex_HFinite_diff_Infinitesimal: |
209 lemma hcomplex_of_complex_HFinite_diff_Infinitesimal: |
210 "hcomplex_of_complex x \<noteq> 0 |
210 "hcomplex_of_complex x \<noteq> 0 |
211 ==> hcomplex_of_complex x \<in> HFinite - Infinitesimal" |
211 ==> hcomplex_of_complex x \<in> HFinite - Infinitesimal" |
212 by (rule SComplex_HFinite_diff_Infinitesimal, auto) |
212 by (rule SComplex_HFinite_diff_Infinitesimal, auto) |
213 |
213 |
214 lemma number_of_not_Infinitesimal [simp]: |
214 lemma numeral_not_Infinitesimal [simp]: |
215 "number_of w \<noteq> (0::hcomplex) ==> (number_of w::hcomplex) \<notin> Infinitesimal" |
215 "numeral w \<noteq> (0::hcomplex) ==> (numeral w::hcomplex) \<notin> Infinitesimal" |
216 by (fast dest: Standard_number_of [THEN SComplex_Infinitesimal_zero]) |
216 by (fast dest: Standard_numeral [THEN SComplex_Infinitesimal_zero]) |
217 |
217 |
218 lemma approx_SComplex_not_zero: |
218 lemma approx_SComplex_not_zero: |
219 "[| y \<in> SComplex; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0" |
219 "[| y \<in> SComplex; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0" |
220 by (auto dest: SComplex_Infinitesimal_zero approx_sym [THEN mem_infmal_iff [THEN iffD2]]) |
220 by (auto dest: SComplex_Infinitesimal_zero approx_sym [THEN mem_infmal_iff [THEN iffD2]]) |
221 |
221 |
222 lemma SComplex_approx_iff: |
222 lemma SComplex_approx_iff: |
223 "[|x \<in> SComplex; y \<in> SComplex|] ==> (x @= y) = (x = y)" |
223 "[|x \<in> SComplex; y \<in> SComplex|] ==> (x @= y) = (x = y)" |
224 by (auto simp add: Standard_def) |
224 by (auto simp add: Standard_def) |
225 |
225 |
226 lemma number_of_Infinitesimal_iff [simp]: |
226 lemma numeral_Infinitesimal_iff [simp]: |
227 "((number_of w :: hcomplex) \<in> Infinitesimal) = |
227 "((numeral w :: hcomplex) \<in> Infinitesimal) = |
228 (number_of w = (0::hcomplex))" |
228 (numeral w = (0::hcomplex))" |
229 apply (rule iffI) |
229 apply (rule iffI) |
230 apply (fast dest: Standard_number_of [THEN SComplex_Infinitesimal_zero]) |
230 apply (fast dest: Standard_numeral [THEN SComplex_Infinitesimal_zero]) |
231 apply (simp (no_asm_simp)) |
231 apply (simp (no_asm_simp)) |
232 done |
232 done |
233 |
233 |
234 lemma approx_unique_complex: |
234 lemma approx_unique_complex: |
235 "[| r \<in> SComplex; s \<in> SComplex; r @= x; s @= x|] ==> r = s" |
235 "[| r \<in> SComplex; s \<in> SComplex; r @= x; s @= x|] ==> r = s" |
439 |
439 |
440 lemma stc_add: |
440 lemma stc_add: |
441 "[| x \<in> HFinite; y \<in> HFinite |] ==> stc (x + y) = stc(x) + stc(y)" |
441 "[| x \<in> HFinite; y \<in> HFinite |] ==> stc (x + y) = stc(x) + stc(y)" |
442 by (simp add: stc_unique stc_SComplex stc_approx_self approx_add) |
442 by (simp add: stc_unique stc_SComplex stc_approx_self approx_add) |
443 |
443 |
444 lemma stc_number_of [simp]: "stc (number_of w) = number_of w" |
444 lemma stc_numeral [simp]: "stc (numeral w) = numeral w" |
445 by (rule Standard_number_of [THEN stc_SComplex_eq]) |
445 by (rule Standard_numeral [THEN stc_SComplex_eq]) |
446 |
446 |
447 lemma stc_zero [simp]: "stc 0 = 0" |
447 lemma stc_zero [simp]: "stc 0 = 0" |
448 by simp |
448 by simp |
449 |
449 |
450 lemma stc_one [simp]: "stc 1 = 1" |
450 lemma stc_one [simp]: "stc 1 = 1" |