Lots of new material on complex-valued functions. Modified simplification of (x/n)^k

--- a/src/HOL/Complex.thy	Tue Mar 17 17:45:03 2015 +0000
+++ b/src/HOL/Complex.thy	Wed Mar 18 14:13:27 2015 +0000
@@ -215,6 +215,18 @@
 lemma i_even_power [simp]: "\<i> ^ (n * 2) = (-1) ^ n"
   by (metis mult.commute power2_i power_mult)
 
+lemma Re_ii_times [simp]: "Re (ii*z) = - Im z"
+  by simp
+
+lemma Im_ii_times [simp]: "Im (ii*z) = Re z"
+  by simp
+
+lemma ii_times_eq_iff: "ii*w = z \<longleftrightarrow> w = -(ii*z)"
+  by auto
+
+lemma divide_numeral_i [simp]: "z / (numeral n * ii) = -(ii*z) / numeral n"
+  by (metis divide_divide_eq_left divide_i mult.commute mult_minus_right)
+
 subsection {* Vector Norm *}
 
 instantiation complex :: real_normed_field
@@ -309,6 +321,9 @@
   apply (simp_all add: power2_sum add.commute sum_squares_bound real_sqrt_mult [symmetric])
   done
 
+lemma complex_unit_circle: "z \<noteq> 0 \<Longrightarrow> (Re z / cmod z)\<^sup>2 + (Im z / cmod z)\<^sup>2 = 1"
+  by (simp add: norm_complex_def divide_simps complex_eq_iff)
+
 
 text {* Properties of complex signum. *}
 
@@ -508,10 +523,10 @@
    (auto simp: complex_eq_iff norm_complex_def power2_eq_square[symmetric] of_real_power[symmetric]
          simp del: of_real_power)
 
-lemma re_complex_div_eq_0: "Re (a / b) = 0 \<longleftrightarrow> Re (a * cnj b) = 0"
+lemma Re_complex_div_eq_0: "Re (a / b) = 0 \<longleftrightarrow> Re (a * cnj b) = 0"
   by (auto simp add: Re_divide)
 
-lemma im_complex_div_eq_0: "Im (a / b) = 0 \<longleftrightarrow> Im (a * cnj b) = 0"
+lemma Im_complex_div_eq_0: "Im (a / b) = 0 \<longleftrightarrow> Im (a * cnj b) = 0"
   by (auto simp add: Im_divide)
 
 lemma complex_div_gt_0:
@@ -526,27 +541,27 @@
     by (simp add: Re_divide Im_divide zero_less_divide_iff)
 qed
 
-lemma re_complex_div_gt_0: "Re (a / b) > 0 \<longleftrightarrow> Re (a * cnj b) > 0"
-  and im_complex_div_gt_0: "Im (a / b) > 0 \<longleftrightarrow> Im (a * cnj b) > 0"
+lemma Re_complex_div_gt_0: "Re (a / b) > 0 \<longleftrightarrow> Re (a * cnj b) > 0"
+  and Im_complex_div_gt_0: "Im (a / b) > 0 \<longleftrightarrow> Im (a * cnj b) > 0"
   using complex_div_gt_0 by auto
 
-lemma re_complex_div_ge_0: "Re(a / b) \<ge> 0 \<longleftrightarrow> Re(a * cnj b) \<ge> 0"
-  by (metis le_less re_complex_div_eq_0 re_complex_div_gt_0)
+lemma Re_complex_div_ge_0: "Re(a / b) \<ge> 0 \<longleftrightarrow> Re(a * cnj b) \<ge> 0"
+  by (metis le_less Re_complex_div_eq_0 Re_complex_div_gt_0)
 
-lemma im_complex_div_ge_0: "Im(a / b) \<ge> 0 \<longleftrightarrow> Im(a * cnj b) \<ge> 0"
-  by (metis im_complex_div_eq_0 im_complex_div_gt_0 le_less)
+lemma Im_complex_div_ge_0: "Im(a / b) \<ge> 0 \<longleftrightarrow> Im(a * cnj b) \<ge> 0"
+  by (metis Im_complex_div_eq_0 Im_complex_div_gt_0 le_less)
 
-lemma re_complex_div_lt_0: "Re(a / b) < 0 \<longleftrightarrow> Re(a * cnj b) < 0"
-  by (metis less_asym neq_iff re_complex_div_eq_0 re_complex_div_gt_0)
+lemma Re_complex_div_lt_0: "Re(a / b) < 0 \<longleftrightarrow> Re(a * cnj b) < 0"
+  by (metis less_asym neq_iff Re_complex_div_eq_0 Re_complex_div_gt_0)
 
-lemma im_complex_div_lt_0: "Im(a / b) < 0 \<longleftrightarrow> Im(a * cnj b) < 0"
-  by (metis im_complex_div_eq_0 im_complex_div_gt_0 less_asym neq_iff)
+lemma Im_complex_div_lt_0: "Im(a / b) < 0 \<longleftrightarrow> Im(a * cnj b) < 0"
+  by (metis Im_complex_div_eq_0 Im_complex_div_gt_0 less_asym neq_iff)
 
-lemma re_complex_div_le_0: "Re(a / b) \<le> 0 \<longleftrightarrow> Re(a * cnj b) \<le> 0"
-  by (metis not_le re_complex_div_gt_0)
+lemma Re_complex_div_le_0: "Re(a / b) \<le> 0 \<longleftrightarrow> Re(a * cnj b) \<le> 0"
+  by (metis not_le Re_complex_div_gt_0)
 
-lemma im_complex_div_le_0: "Im(a / b) \<le> 0 \<longleftrightarrow> Im(a * cnj b) \<le> 0"
-  by (metis im_complex_div_gt_0 not_le)
+lemma Im_complex_div_le_0: "Im(a / b) \<le> 0 \<longleftrightarrow> Im(a * cnj b) \<le> 0"
+  by (metis Im_complex_div_gt_0 not_le)
 
 lemma Re_setsum[simp]: "Re (setsum f s) = (\<Sum>x\<in>s. Re (f x))"
   by (induct s rule: infinite_finite_induct) auto
@@ -807,7 +822,7 @@
 lemma csqrt_ii [simp]: "csqrt \<i> = (1 + \<i>) / sqrt 2"
   by (simp add: complex_eq_iff Re_divide Im_divide real_sqrt_divide real_div_sqrt)
 
-lemma power2_csqrt[algebra]: "(csqrt z)\<^sup>2 = z"
+lemma power2_csqrt[simp,algebra]: "(csqrt z)\<^sup>2 = z"
 proof cases
   assume "Im z = 0" then show ?thesis
     using real_sqrt_pow2[of "Re z"] real_sqrt_pow2[of "- Re z"]

--- a/src/HOL/Decision_Procs/Approximation.thy	Tue Mar 17 17:45:03 2015 +0000
+++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Mar 18 14:13:27 2015 +0000
@@ -1718,8 +1718,10 @@
           by (auto simp: real_power_down_fl intro!: power_down_le)
       next
         case True
-        have "power_down_fl prec (Float 1 (- 2))  ?num \<le> real (Float 1 (- 2)) ^ ?num"
-          by (auto simp: real_power_down_fl power_down)
+        have "power_down_fl prec (Float 1 (- 2))  ?num \<le> (Float 1 (- 2)) ^ ?num"
+          by (metis Float_le_zero_iff less_imp_le linorder_not_less not_numeral_le_zero numeral_One power_down_fl)
+        then have "power_down_fl prec (Float 1 (- 2))  ?num \<le> real (Float 1 (- 2)) ^ ?num"
+          by simp
         also
         have "real (floor_fl x) \<noteq> 0" and "real (floor_fl x) \<le> 0" using `real (floor_fl x) < 0` by auto
         from divide_right_mono_neg[OF floor_fl[of x] `real (floor_fl x) \<le> 0`, unfolded divide_self[OF `real (floor_fl x) \<noteq> 0`]]
@@ -1727,7 +1729,7 @@
         from order_trans[OF exp_m1_ge_quarter this[unfolded exp_le_cancel_iff[where x="- 1", symmetric]]]
         have "Float 1 (- 2) \<le> exp (x / (- floor_fl x))" unfolding Float_num .
         hence "real (Float 1 (- 2)) ^ ?num \<le> exp (x / (- floor_fl x)) ^ ?num"
-          by (auto intro!: power_mono)
+          by (metis Float_num(5) power_mono zero_le_divide_1_iff zero_le_numeral)
         also have "\<dots> = exp x" unfolding num_eq fl_eq exp_real_of_nat_mult[symmetric] using `real (floor_fl x) \<noteq> 0` by auto
         finally show ?thesis
           unfolding lb_exp.simps if_not_P[OF `\<not> 0 < x`] if_P[OF `x < - 1`] int_floor_fl_def Let_def if_P[OF True] real_of_float_power

--- a/src/HOL/Library/Formal_Power_Series.thy	Tue Mar 17 17:45:03 2015 +0000
+++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Mar 18 14:13:27 2015 +0000
@@ -8,8 +8,6 @@
 imports Complex_Main
 begin
 
-lemmas fact_Suc = fact.simps(2)
-
 subsection {* The type of formal power series*}
 
 typedef 'a fps = "{f :: nat \<Rightarrow> 'a. True}"
@@ -594,7 +592,7 @@
       fix n :: nat
       assume nn0: "n \<ge> n0"
       then have thnn0: "(1/2)^n \<le> (1/2 :: real)^n0"
-        by (auto intro: power_decreasing)
+        by (simp add: divide_simps)
       {
         assume "?s n = a"
         then have "dist (?s n) a < r"
@@ -612,9 +610,9 @@
           by (auto simp: fps_sum_rep_nth not_le k_def fps_eq_iff
               split: split_if_asm intro: LeastI2_ex)
         then have "dist (?s n) a < (1/2)^n"
-          unfolding dth by (auto intro: power_strict_decreasing)
+          unfolding dth by (simp add: divide_simps)
         also have "\<dots> \<le> (1/2)^n0"
-          using nn0 by (auto intro: power_decreasing)
+          using nn0 by (simp add: divide_simps)
         also have "\<dots> < r"
           using n0 by simp
         finally have "dist (?s n) a < r" .

--- a/src/HOL/NthRoot.thy	Tue Mar 17 17:45:03 2015 +0000
+++ b/src/HOL/NthRoot.thy	Wed Mar 18 14:13:27 2015 +0000
@@ -626,19 +626,24 @@
 apply (simp add: zero_less_divide_iff)
 done
 
+lemma sqrt2_less_2: "sqrt 2 < (2::real)"
+  by (metis not_less not_less_iff_gr_or_eq numeral_less_iff real_sqrt_four real_sqrt_le_iff semiring_norm(75) semiring_norm(78) semiring_norm(85))
+
+
 text{*Needed for the infinitely close relation over the nonstandard
     complex numbers*}
 lemma lemma_sqrt_hcomplex_capprox:
      "[| 0 < u; x < u/2; y < u/2; 0 \<le> x; 0 \<le> y |] ==> sqrt (x\<^sup>2 + y\<^sup>2) < u"
-apply (rule_tac y = "u/sqrt 2" in order_le_less_trans)
-apply (erule_tac [2] lemma_real_divide_sqrt_less)
-apply (rule power2_le_imp_le)
-apply (auto simp add: zero_le_divide_iff power_divide)
-apply (rule_tac t = "u\<^sup>2" in real_sum_of_halves [THEN subst])
-apply (rule add_mono)
-apply (auto simp add: four_x_squared intro: power_mono)
-done
-
+  apply (rule real_sqrt_sum_squares_less)
+  apply (auto simp add: abs_if field_simps)
+  apply (rule le_less_trans [where y = "x*2"])
+  using less_eq_real_def sqrt2_less_2 apply force
+  apply assumption
+  apply (rule le_less_trans [where y = "y*2"])
+  using less_eq_real_def sqrt2_less_2 mult_le_cancel_left 
+  apply auto 
+  done
+  
 text "Legacy theorem names:"
 lemmas real_root_pos2 = real_root_power_cancel
 lemmas real_root_pos_pos = real_root_gt_zero [THEN order_less_imp_le]

--- a/src/HOL/Power.thy	Tue Mar 17 17:45:03 2015 +0000
+++ b/src/HOL/Power.thy	Wed Mar 18 14:13:27 2015 +0000
@@ -51,6 +51,10 @@
   "a ^ 1 = a"
   by simp
 
+lemma power_Suc0_right [simp]:
+  "a ^ Suc 0 = a"
+  by simp
+
 lemma power_commutes:
   "a ^ n * a = a * a ^ n"
   by (induct n) (simp_all add: mult.assoc)
@@ -127,6 +131,9 @@
 
 end
 
+declare power_mult_distrib [where a = "numeral w" for w, simp]
+declare power_mult_distrib [where b = "numeral w" for w, simp]
+
 context semiring_numeral
 begin
 
@@ -301,6 +308,8 @@
   "b \<noteq> 0 \<Longrightarrow> (a / b) ^ n = a ^ n / b ^ n"
   by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
 
+declare nonzero_power_divide [where b = "numeral w" for w, simp]
+
 end
 
 

--- a/src/HOL/Probability/Lebesgue_Measure.thy	Tue Mar 17 17:45:03 2015 +0000
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Wed Mar 18 14:13:27 2015 +0000
@@ -502,13 +502,26 @@
 end
 
 lemma emeasure_lborel_UNIV: "emeasure lborel (UNIV::'a::euclidean_space set) = \<infinity>"
-  unfolding UN_box_eq_UNIV[symmetric]
-  apply (subst SUP_emeasure_incseq[symmetric])
-  apply (auto simp: incseq_def subset_box inner_add_left setprod_constant intro!: SUP_PInfty)
-  apply (rule_tac x="Suc n" in exI)
-  apply (rule order_trans[OF _ self_le_power])
-  apply (auto simp: card_gt_0_iff real_of_nat_Suc)
-  done
+proof -
+  { fix n::nat
+    let ?Ba = "Basis :: 'a set"
+    have "real n \<le> (2::real) ^ card ?Ba * real n"
+      by (simp add: mult_le_cancel_right1)
+    also 
+    have "... \<le> (2::real) ^ card ?Ba * real (Suc n) ^ card ?Ba"
+      apply (rule mult_left_mono)
+      apply (metis DIM_positive One_nat_def less_eq_Suc_le less_imp_le real_of_nat_le_iff real_of_nat_power self_le_power zero_less_Suc)
+      apply (simp add: DIM_positive)
+      done
+    finally have "real n \<le> (2::real) ^ card ?Ba * real (Suc n) ^ card ?Ba" .
+  } note [intro!] = this
+  show ?thesis
+    unfolding UN_box_eq_UNIV[symmetric]
+    apply (subst SUP_emeasure_incseq[symmetric])
+    apply (auto simp: incseq_def subset_box inner_add_left setprod_constant 
+               intro!: SUP_PInfty)
+    done 
+qed
 
 lemma emeasure_lborel_singleton[simp]: "emeasure lborel {x} = 0"
   using emeasure_lborel_cbox[of x x] nonempty_Basis

--- a/src/HOL/ROOT	Tue Mar 17 17:45:03 2015 +0000
+++ b/src/HOL/ROOT	Wed Mar 18 14:13:27 2015 +0000
@@ -688,6 +688,7 @@
     Determinants
     PolyRoots
     Complex_Analysis_Basics
+    Complex_Transcendental
   document_files
     "root.tex"
 

--- a/src/HOL/Real_Vector_Spaces.thy	Tue Mar 17 17:45:03 2015 +0000
+++ b/src/HOL/Real_Vector_Spaces.thy	Wed Mar 18 14:13:27 2015 +0000
@@ -444,7 +444,8 @@
   then show thesis ..
 qed
 
-lemma setsum_in_Reals: assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setsum f s \<in> \<real>"
+lemma setsum_in_Reals [intro,simp]:
+  assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setsum f s \<in> \<real>"
 proof (cases "finite s")
   case True then show ?thesis using assms
     by (induct s rule: finite_induct) auto
@@ -453,7 +454,8 @@
     by (metis Reals_0 setsum.infinite)
 qed
 
-lemma setprod_in_Reals: assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setprod f s \<in> \<real>"
+lemma setprod_in_Reals [intro,simp]: 
+  assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setprod f s \<in> \<real>"
 proof (cases "finite s")
   case True then show ?thesis using assms
     by (induct s rule: finite_induct) auto

--- a/src/HOL/Series.thy	Tue Mar 17 17:45:03 2015 +0000
+++ b/src/HOL/Series.thy	Wed Mar 18 14:13:27 2015 +0000
@@ -434,7 +434,7 @@
   have 2: "(\<lambda>n. (1/2::real)^n) sums 2" using geometric_sums [of "1/2::real"]
     by auto
   have "(\<lambda>n. (1/2::real)^Suc n) = (\<lambda>n. (1 / 2) ^ n / 2)"
-    by simp
+    by (simp add: mult.commute)
   thus ?thesis using sums_divide [OF 2, of 2]
     by simp
 qed

--- a/src/HOL/Transcendental.thy	Tue Mar 17 17:45:03 2015 +0000
+++ b/src/HOL/Transcendental.thy	Wed Mar 18 14:13:27 2015 +0000
@@ -1512,6 +1512,10 @@
   using exp_bound [of "1/2"]
   by (simp add: field_simps)
 
+corollary exp_le: "exp 1 \<le> (3::real)"
+  using exp_bound [of 1]
+  by (simp add: field_simps)
+
 lemma exp_bound_half: "norm(z) \<le> 1/2 \<Longrightarrow> norm(exp z) \<le> 2"
   by (blast intro: order_trans intro!: exp_half_le2 norm_exp)
 
@@ -3071,6 +3075,84 @@
 lemma sin_two_pi [simp]: "sin (2*pi) = 0"
   by (simp add: sin_double)
 
+
+lemma sin_times_sin:
+  fixes w :: "'a::{real_normed_field,banach}"
+  shows "sin(w) * sin(z) = (cos(w - z) - cos(w + z)) / 2"
+  by (simp add: cos_diff cos_add)
+
+lemma sin_times_cos:
+  fixes w :: "'a::{real_normed_field,banach}"
+  shows "sin(w) * cos(z) = (sin(w + z) + sin(w - z)) / 2"
+  by (simp add: sin_diff sin_add)
+
+lemma cos_times_sin:
+  fixes w :: "'a::{real_normed_field,banach}"
+  shows "cos(w) * sin(z) = (sin(w + z) - sin(w - z)) / 2"
+  by (simp add: sin_diff sin_add)
+
+lemma cos_times_cos:
+  fixes w :: "'a::{real_normed_field,banach}"
+  shows "cos(w) * cos(z) = (cos(w - z) + cos(w + z)) / 2"
+  by (simp add: cos_diff cos_add)
+
+lemma sin_plus_sin:  (*FIXME field_inverse_zero should not be necessary*)
+  fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}"
+  shows "sin(w) + sin(z) = 2 * sin((w + z) / 2) * cos((w - z) / 2)"
+  apply (simp add: mult.assoc sin_times_cos)
+  apply (simp add: field_simps)
+  done
+
+lemma sin_diff_sin: 
+  fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}"
+  shows "sin(w) - sin(z) = 2 * sin((w - z) / 2) * cos((w + z) / 2)"
+  apply (simp add: mult.assoc sin_times_cos)
+  apply (simp add: field_simps)
+  done
+
+lemma cos_plus_cos: 
+  fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}"
+  shows "cos(w) + cos(z) = 2 * cos((w + z) / 2) * cos((w - z) / 2)"
+  apply (simp add: mult.assoc cos_times_cos)
+  apply (simp add: field_simps)
+  done
+
+lemma cos_diff_cos: 
+  fixes w :: "'a::{real_normed_field,banach,field_inverse_zero}"
+  shows "cos(w) - cos(z) = 2 * sin((w + z) / 2) * sin((z - w) / 2)"
+  apply (simp add: mult.assoc sin_times_sin)
+  apply (simp add: field_simps)
+  done
+
+lemma cos_double_cos: 
+  fixes z :: "'a::{real_normed_field,banach}"
+  shows "cos(2 * z) = 2 * cos z ^ 2 - 1"
+by (simp add: cos_double sin_squared_eq)
+
+lemma cos_double_sin: 
+  fixes z :: "'a::{real_normed_field,banach}"
+  shows "cos(2 * z) = 1 - 2 * sin z ^ 2"
+by (simp add: cos_double sin_squared_eq)
+
+lemma sin_pi_minus [simp]: "sin (pi - x) = sin x"
+  by (metis sin_minus sin_periodic_pi minus_minus uminus_add_conv_diff)
+
+lemma cos_pi_minus [simp]: "cos (pi - x) = -(cos x)"
+  by (metis cos_minus cos_periodic_pi uminus_add_conv_diff)
+
+lemma sin_minus_pi [simp]: "sin (x - pi) = - (sin x)"
+  by (simp add: sin_diff)
+
+lemma cos_minus_pi [simp]: "cos (x - pi) = -(cos x)"
+  by (simp add: cos_diff)
+
+lemma sin_2pi_minus [simp]: "sin (2*pi - x) = -(sin x)"
+  by (metis sin_periodic_pi2 add_diff_eq mult_2 sin_pi_minus)
+
+lemma cos_2pi_minus [simp]: "cos (2*pi - x) = cos x"
+  by (metis (no_types, hide_lams) cos_add cos_minus cos_two_pi sin_minus sin_two_pi 
+           diff_0_right minus_diff_eq mult_1 mult_zero_left uminus_add_conv_diff)
+
 lemma sin_gt_zero2: "\<lbrakk>0 < x; x < pi/2\<rbrakk> \<Longrightarrow> 0 < sin x"
   by (metis sin_gt_zero_02 order_less_trans pi_half_less_two)