src/HOL/Complex.thy
changeset 56381 0556204bc230
parent 56369 2704ca85be98
child 56409 36489d77c484
     1.1 --- a/src/HOL/Complex.thy	Thu Apr 03 17:16:02 2014 +0200
     1.2 +++ b/src/HOL/Complex.thy	Thu Apr 03 17:56:08 2014 +0200
     1.3 @@ -374,30 +374,20 @@
     1.4  lemma bounded_linear_Im: "bounded_linear Im"
     1.5    by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def)
     1.6  
     1.7 -lemmas tendsto_Re [tendsto_intros] =
     1.8 -  bounded_linear.tendsto [OF bounded_linear_Re]
     1.9 -
    1.10 -lemmas tendsto_Im [tendsto_intros] =
    1.11 -  bounded_linear.tendsto [OF bounded_linear_Im]
    1.12 -
    1.13 -lemmas isCont_Re [simp] = bounded_linear.isCont [OF bounded_linear_Re]
    1.14 -lemmas isCont_Im [simp] = bounded_linear.isCont [OF bounded_linear_Im]
    1.15  lemmas Cauchy_Re = bounded_linear.Cauchy [OF bounded_linear_Re]
    1.16  lemmas Cauchy_Im = bounded_linear.Cauchy [OF bounded_linear_Im]
    1.17 -
    1.18 -lemma continuous_Re: "continuous_on X Re"
    1.19 -  by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Re 
    1.20 -            continuous_on_cong continuous_on_id)
    1.21 -
    1.22 -lemma continuous_Im: "continuous_on X Im"
    1.23 -  by (metis (poly_guards_query) bounded_linear.continuous_on bounded_linear_Im 
    1.24 -            continuous_on_cong continuous_on_id)
    1.25 -
    1.26 -lemma has_derivative_Re [has_derivative_intros] : "(Re has_derivative Re) F"
    1.27 -  by (auto simp add: has_derivative_def bounded_linear_Re tendsto_const)
    1.28 -
    1.29 -lemma has_derivative_Im [has_derivative_intros] : "(Im has_derivative Im) F"
    1.30 -  by (auto simp add: has_derivative_def bounded_linear_Im tendsto_const)
    1.31 +lemmas tendsto_Re [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_Re]
    1.32 +lemmas tendsto_Im [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_Im]
    1.33 +lemmas isCont_Re [simp] = bounded_linear.isCont [OF bounded_linear_Re]
    1.34 +lemmas isCont_Im [simp] = bounded_linear.isCont [OF bounded_linear_Im]
    1.35 +lemmas continuous_Re [simp] = bounded_linear.continuous [OF bounded_linear_Re]
    1.36 +lemmas continuous_Im [simp] = bounded_linear.continuous [OF bounded_linear_Im]
    1.37 +lemmas continuous_on_Re [continuous_intros] = bounded_linear.continuous_on[OF bounded_linear_Re]
    1.38 +lemmas continuous_on_Im [continuous_intros] = bounded_linear.continuous_on[OF bounded_linear_Im]
    1.39 +lemmas has_derivative_Re [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Re]
    1.40 +lemmas has_derivative_Im [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Im]
    1.41 +lemmas sums_Re = bounded_linear.sums [OF bounded_linear_Re]
    1.42 +lemmas sums_Im = bounded_linear.sums [OF bounded_linear_Im]
    1.43  
    1.44  lemma tendsto_Complex [tendsto_intros]:
    1.45    assumes "(f ---> a) F" and "(g ---> b) F"
    1.46 @@ -445,8 +435,7 @@
    1.47  qed
    1.48  
    1.49  declare
    1.50 -  DERIV_power[where 'a=complex, THEN DERIV_cong,
    1.51 -              unfolded of_nat_def[symmetric], DERIV_intros]
    1.52 +  DERIV_power[where 'a=complex, unfolded of_nat_def[symmetric], derivative_intros]
    1.53  
    1.54  
    1.55  subsection {* The Complex Number $i$ *}
    1.56 @@ -605,11 +594,11 @@
    1.57    using complex_cnj_add complex_cnj_scaleR
    1.58    by (rule bounded_linear_intro [where K=1], simp)
    1.59  
    1.60 -lemmas tendsto_cnj [tendsto_intros] =
    1.61 -  bounded_linear.tendsto [OF bounded_linear_cnj]
    1.62 -
    1.63 -lemmas isCont_cnj [simp] =
    1.64 -  bounded_linear.isCont [OF bounded_linear_cnj]
    1.65 +lemmas tendsto_cnj [tendsto_intros] = bounded_linear.tendsto [OF bounded_linear_cnj]
    1.66 +lemmas isCont_cnj [simp] = bounded_linear.isCont [OF bounded_linear_cnj]
    1.67 +lemmas continuous_cnj [simp, continuous_intros] = bounded_linear.continuous [OF bounded_linear_cnj]
    1.68 +lemmas continuous_on_cnj [simp, continuous_intros] = bounded_linear.continuous_on [OF bounded_linear_cnj]
    1.69 +lemmas has_derivative_cnj [simp, derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_cnj]
    1.70  
    1.71  lemma lim_cnj: "((\<lambda>x. cnj(f x)) ---> cnj l) F \<longleftrightarrow> (f ---> l) F"
    1.72    by (simp add: tendsto_iff dist_complex_def Complex.complex_cnj_diff [symmetric])
    1.73 @@ -704,12 +693,6 @@
    1.74  lemma sums_complex_iff: "f sums x \<longleftrightarrow> ((\<lambda>x. Re (f x)) sums Re x) \<and> ((\<lambda>x. Im (f x)) sums Im x)"
    1.75    unfolding sums_def tendsto_complex_iff Im_setsum Re_setsum ..
    1.76    
    1.77 -lemma sums_Re: "f sums a \<Longrightarrow> (\<lambda>x. Re (f x)) sums Re a"
    1.78 -  unfolding sums_complex_iff by blast
    1.79 -
    1.80 -lemma sums_Im: "f sums a \<Longrightarrow> (\<lambda>x. Im (f x)) sums Im a"
    1.81 -  unfolding sums_complex_iff by blast
    1.82 -
    1.83  lemma summable_complex_iff: "summable f \<longleftrightarrow> summable (\<lambda>x. Re (f x)) \<and>  summable (\<lambda>x. Im (f x))"
    1.84    unfolding summable_def sums_complex_iff[abs_def] by (metis Im.simps Re.simps)
    1.85  
    1.86 @@ -976,5 +959,4 @@
    1.87  lemmas complex_Re_Im_cancel_iff = complex_eq_iff
    1.88  lemmas complex_equality = complex_eqI
    1.89  
    1.90 -
    1.91  end