src/HOL/Complex.thy
changeset 56217 dc429a5b13c4
parent 55759 fe3d8f585c20
child 56238 5d147e1e18d1
     1.1 --- a/src/HOL/Complex.thy	Wed Mar 19 14:55:47 2014 +0000
     1.2 +++ b/src/HOL/Complex.thy	Wed Mar 19 17:06:02 2014 +0000
     1.3 @@ -634,20 +634,32 @@
     1.4  lemma im_complex_div_le_0: "Im(a / b) \<le> 0 \<longleftrightarrow> Im(a * cnj b) \<le> 0"
     1.5    by (metis im_complex_div_gt_0 not_le)
     1.6  
     1.7 -lemma Re_setsum: "finite s \<Longrightarrow> Re(setsum f s) = setsum (%x. Re(f x)) s"
     1.8 +lemma Re_setsum: "Re(setsum f s) = setsum (%x. Re(f x)) s"
     1.9 +apply (cases "finite s")
    1.10    by (induct s rule: finite_induct) auto
    1.11  
    1.12 -lemma Im_setsum: "finite s \<Longrightarrow> Im(setsum f s) = setsum (%x. Im(f x)) s"
    1.13 +lemma Im_setsum: "Im(setsum f s) = setsum (%x. Im(f x)) s"
    1.14 +apply (cases "finite s")
    1.15 +  by (induct s rule: finite_induct) auto
    1.16 +
    1.17 +lemma Complex_setsum': "setsum (%x. Complex (f x) 0) s = Complex (setsum f s) 0"
    1.18 +apply (cases "finite s")
    1.19    by (induct s rule: finite_induct) auto
    1.20  
    1.21 -lemma Complex_setsum': "finite s \<Longrightarrow> setsum (%x. Complex (f x) 0) s = Complex (setsum f s) 0"
    1.22 +lemma Complex_setsum: "Complex (setsum f s) 0 = setsum (%x. Complex (f x) 0) s"
    1.23 +  by (metis Complex_setsum')
    1.24 +
    1.25 +lemma cnj_setsum: "cnj (setsum f s) = setsum (%x. cnj (f x)) s"
    1.26 +apply (cases "finite s")
    1.27 +  by (induct s rule: finite_induct) (auto simp: complex_cnj_add)
    1.28 +
    1.29 +lemma of_real_setsum: "of_real (setsum f s) = setsum (%x. of_real(f x)) s"
    1.30 +apply (cases "finite s")
    1.31    by (induct s rule: finite_induct) auto
    1.32  
    1.33 -lemma Complex_setsum: "finite s \<Longrightarrow> Complex (setsum f s) 0 = setsum (%x. Complex (f x) 0) s"
    1.34 -  by (metis Complex_setsum')
    1.35 -
    1.36 -lemma cnj_setsum: "finite s \<Longrightarrow> cnj (setsum f s) = setsum (%x. cnj (f x)) s"
    1.37 -  by (induct s rule: finite_induct) (auto simp: complex_cnj_add)
    1.38 +lemma of_real_setprod: "of_real (setprod f s) = setprod (%x. of_real(f x)) s"
    1.39 +apply (cases "finite s")
    1.40 +  by (induct s rule: finite_induct) auto
    1.41  
    1.42  lemma Reals_cnj_iff: "z \<in> \<real> \<longleftrightarrow> cnj z = z"
    1.43  by (metis Reals_cases Reals_of_real complex.exhaust complex.inject complex_cnj