# HG changeset patch
# User huffman
# Date 1313731939 25200
# Node ID 453803d28c4b003d4b1080ef1b3d1c3dda6d00c8
# Parent  dbd9965745fdb4b5858d039b447c69aab74462c7# Parent  dd203341fd2bb8e5227dc192a4966e51e1c1f34c
merged

diff -r dd203341fd2b -r 453803d28c4b src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Fri Aug 19 10:23:16 2011 +0900
+++ b/src/HOL/Complex.thy	Thu Aug 18 22:32:19 2011 -0700
@@ -339,11 +339,22 @@
 
 subsection {* Completeness of the Complexes *}
 
-interpretation Re: bounded_linear "Re"
+lemma bounded_linear_Re: "bounded_linear Re"
+  by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def)
+
+lemma bounded_linear_Im: "bounded_linear Im"
   by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def)
 
-interpretation Im: bounded_linear "Im"
-  by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def)
+lemmas tendsto_Re [tendsto_intros] =
+  bounded_linear.tendsto [OF bounded_linear_Re]
+
+lemmas tendsto_Im [tendsto_intros] =
+  bounded_linear.tendsto [OF bounded_linear_Im]
+
+lemmas isCont_Re [simp] = bounded_linear.isCont [OF bounded_linear_Re]
+lemmas isCont_Im [simp] = bounded_linear.isCont [OF bounded_linear_Im]
+lemmas Cauchy_Re = bounded_linear.Cauchy [OF bounded_linear_Re]
+lemmas Cauchy_Im = bounded_linear.Cauchy [OF bounded_linear_Im]
 
 lemma tendsto_Complex [tendsto_intros]:
   assumes "(f ---> a) net" and "(g ---> b) net"
@@ -370,9 +381,9 @@
 proof
   fix X :: "nat \<Rightarrow> complex"
   assume X: "Cauchy X"
-  from Re.Cauchy [OF X] have 1: "(\<lambda>n. Re (X n)) ----> lim (\<lambda>n. Re (X n))"
+  from Cauchy_Re [OF X] have 1: "(\<lambda>n. Re (X n)) ----> lim (\<lambda>n. Re (X n))"
     by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
-  from Im.Cauchy [OF X] have 2: "(\<lambda>n. Im (X n)) ----> lim (\<lambda>n. Im (X n))"
+  from Cauchy_Im [OF X] have 2: "(\<lambda>n. Im (X n)) ----> lim (\<lambda>n. Im (X n))"
     by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
   have "X ----> Complex (lim (\<lambda>n. Re (X n))) (lim (\<lambda>n. Im (X n)))"
     using LIMSEQ_Complex [OF 1 2] by simp
@@ -511,10 +522,16 @@
 lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<twosuperior>"
 by (simp add: norm_mult power2_eq_square)
 
-interpretation cnj: bounded_linear "cnj"
+lemma bounded_linear_cnj: "bounded_linear cnj"
   using complex_cnj_add complex_cnj_scaleR
   by (rule bounded_linear_intro [where K=1], simp)
 
+lemmas tendsto_cnj [tendsto_intros] =
+  bounded_linear.tendsto [OF bounded_linear_cnj]
+
+lemmas isCont_cnj [simp] =
+  bounded_linear.isCont [OF bounded_linear_cnj]
+
 
 subsection{*The Functions @{term sgn} and @{term arg}*}
 
@@ -586,10 +603,42 @@
   rcis :: "[real, real] => complex" where
   "rcis r a = complex_of_real r * cis a"
 
-definition
-  (* e ^ (x + iy) *)
-  expi :: "complex => complex" where
-  "expi z = complex_of_real(exp (Re z)) * cis (Im z)"
+abbreviation expi :: "complex \<Rightarrow> complex"
+  where "expi \<equiv> exp"
+
+lemma cos_coeff_Suc: "cos_coeff (Suc n) = - sin_coeff n / real (Suc n)"
+  unfolding cos_coeff_def sin_coeff_def
+  by (simp del: mult_Suc, auto simp add: odd_Suc_mult_two_ex)
+
+lemma sin_coeff_Suc: "sin_coeff (Suc n) = cos_coeff n / real (Suc n)"
+  unfolding cos_coeff_def sin_coeff_def
+  by (simp del: mult_Suc)
+
+lemma expi_imaginary: "expi (Complex 0 b) = cis b"
+proof (rule complex_eqI)
+  { fix n have "Complex 0 b ^ n =
+    real (fact n) *\<^sub>R Complex (cos_coeff n * b ^ n) (sin_coeff n * b ^ n)"
+      apply (induct n)
+      apply (simp add: cos_coeff_def sin_coeff_def)
+      apply (simp add: sin_coeff_Suc cos_coeff_Suc del: mult_Suc)
+      done } note * = this
+  show "Re (exp (Complex 0 b)) = Re (cis b)"
+    unfolding exp_def cis_def cos_def
+    by (subst bounded_linear.suminf[OF bounded_linear_Re summable_exp_generic],
+      simp add: * mult_assoc [symmetric])
+  show "Im (exp (Complex 0 b)) = Im (cis b)"
+    unfolding exp_def cis_def sin_def
+    by (subst bounded_linear.suminf[OF bounded_linear_Im summable_exp_generic],
+      simp add: * mult_assoc [symmetric])
+qed
+
+lemma expi_def: "expi z = complex_of_real (exp (Re z)) * cis (Im z)"
+proof -
+  have "expi z = expi (complex_of_real (Re z) + Complex 0 (Im z))"
+    by simp
+  thus ?thesis
+    unfolding exp_add exp_of_real expi_imaginary .
+qed
 
 lemma complex_split_polar:
      "\<exists>r a. z = complex_of_real r * (Complex (cos a) (sin a))"
@@ -696,10 +745,10 @@
 by (auto simp add: DeMoivre)
 
 lemma expi_add: "expi(a + b) = expi(a) * expi(b)"
-by (simp add: expi_def exp_add cis_mult [symmetric] mult_ac)
+  by (rule exp_add) (* FIXME: redundant *)
 
-lemma expi_zero [simp]: "expi (0::complex) = 1"
-by (simp add: expi_def)
+lemma expi_zero: "expi (0::complex) = 1"
+  by (rule exp_zero) (* FIXME: redundant *)
 
 lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a"
 apply (insert rcis_Ex [of z])
diff -r dd203341fd2b -r 453803d28c4b src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Aug 19 10:23:16 2011 +0900
+++ b/src/HOL/IsaMakefile	Thu Aug 18 22:32:19 2011 -0700
@@ -1183,6 +1183,7 @@
   Multivariate_Analysis/Integration.certs				\
   Multivariate_Analysis/Integration.thy					\
   Multivariate_Analysis/L2_Norm.thy					\
+  Multivariate_Analysis/Linear_Algebra.thy				\
   Multivariate_Analysis/Multivariate_Analysis.thy			\
   Multivariate_Analysis/Operator_Norm.thy				\
   Multivariate_Analysis/Path_Connected.thy				\
@@ -1194,7 +1195,7 @@
   Library/Extended_Real.thy Library/Indicator_Function.thy		\
   Library/Inner_Product.thy Library/Numeral_Type.thy Library/Convex.thy	\
   Library/FrechetDeriv.thy Library/Product_Vector.thy			\
-  Library/Product_plus.thy
+  Library/Product_plus.thy Library/Sum_of_Squares.thy
 	@cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Multivariate_Analysis
 
 
diff -r dd203341fd2b -r 453803d28c4b src/HOL/Ln.thy
--- a/src/HOL/Ln.thy	Fri Aug 19 10:23:16 2011 +0900
+++ b/src/HOL/Ln.thy	Thu Aug 18 22:32:19 2011 -0700
@@ -18,7 +18,7 @@
       inverse(fact(n+2)) * (x ^ (n+2)))" (is "_ = ?a + _")
     by (rule suminf_split_initial_segment)
   also have "?a = 1 + x"
-    by (simp add: numerals)
+    by (simp add: numeral_2_eq_2)
   finally show ?thesis .
 qed
 
@@ -70,13 +70,7 @@
       finally show ?thesis .
     qed
     moreover have "x ^ (Suc n + 2) <= x ^ (n + 2)"
-      apply (simp add: mult_compare_simps)
-      apply (simp add: assms)
-      apply (subgoal_tac "0 <= x * (x * x^n)")
-      apply force
-      apply (rule mult_nonneg_nonneg, rule a)+
-      apply (rule zero_le_power, rule a)
-      done
+      by (simp add: mult_left_le_one_le mult_nonneg_nonneg a b)
     ultimately have "inverse (fact (Suc n + 2)) *  x ^ (Suc n + 2) <=
         (1 / 2 * inverse (fact (n + 2))) * x ^ (n + 2)"
       apply (rule mult_mono)
@@ -162,7 +156,7 @@
     apply auto
     done
   also from a have "... <= 1 + x"
-    by (simp add: field_simps zero_compare_simps)
+    by (simp add: field_simps add_strict_increasing zero_le_mult_iff)
   finally show ?thesis .
 qed
 
@@ -344,24 +338,17 @@
 lemma ln_x_over_x_mono: "exp 1 <= x ==> x <= y ==> (ln y / y) <= (ln x / x)"  
 proof -
   assume x: "exp 1 <= x" "x <= y"
-  have a: "0 < x" and b: "0 < y"
-    apply (insert x)
-    apply (subgoal_tac "0 < exp (1::real)")
-    apply arith
-    apply auto
-    apply (subgoal_tac "0 < exp (1::real)")
-    apply arith
-    apply auto
-    done
+  moreover have "0 < exp (1::real)" by simp
+  ultimately have a: "0 < x" and b: "0 < y"
+    by (fast intro: less_le_trans order_trans)+
   have "x * ln y - x * ln x = x * (ln y - ln x)"
     by (simp add: algebra_simps)
   also have "... = x * ln(y / x)"
-    apply (subst ln_div)
-    apply (rule b, rule a, rule refl)
-    done
+    by (simp only: ln_div a b)
   also have "y / x = (x + (y - x)) / x"
     by simp
-  also have "... = 1 + (y - x) / x" using x a by (simp add: field_simps)
+  also have "... = 1 + (y - x) / x"
+    using x a by (simp add: field_simps)
   also have "x * ln(1 + (y - x) / x) <= x * ((y - x) / x)"
     apply (rule mult_left_mono)
     apply (rule ln_add_one_self_le_self)
@@ -373,7 +360,7 @@
   also have "... <= (y - x) * ln x"
     apply (rule mult_left_mono)
     apply (subst ln_le_cancel_iff)
-    apply force
+    apply fact
     apply (rule a)
     apply (rule x)
     using x apply simp
diff -r dd203341fd2b -r 453803d28c4b src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Fri Aug 19 10:23:16 2011 +0900
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Aug 18 22:32:19 2011 -0700
@@ -126,7 +126,7 @@
 lemmas isCont_euclidean_component [simp] =
   bounded_linear.isCont [OF bounded_linear_euclidean_component]
 
-lemma euclidean_component_zero: "0 $$ i = 0"
+lemma euclidean_component_zero [simp]: "0 $$ i = 0"
   unfolding euclidean_component_def by (rule inner_zero_right)
 
 lemma euclidean_component_add: "(x + y) $$ i = x $$ i + y $$ i"
diff -r dd203341fd2b -r 453803d28c4b src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Aug 19 10:23:16 2011 +0900
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Aug 18 22:32:19 2011 -0700
@@ -10,8 +10,8 @@
   "~~/src/HOL/Library/Infinite_Set"
   L2_Norm
   "~~/src/HOL/Library/Convex"
+  "~~/src/HOL/Library/Sum_of_Squares"
 uses
-  "~~/src/HOL/Library/positivstellensatz.ML"  (* FIXME duplicate use!? *)
   ("normarith.ML")
 begin
 
@@ -1756,7 +1756,7 @@
   have Kp: "?K > 0" by arith
     { assume C: "B < 0"
       have "((\<chi>\<chi> i. 1)::'a) \<noteq> 0" unfolding euclidean_eq[where 'a='a]
-        by(auto intro!:exI[where x=0] simp add:euclidean_component_zero)
+        by(auto intro!:exI[where x=0])
       hence "norm ((\<chi>\<chi> i. 1)::'a) > 0" by auto
       with C have "B * norm ((\<chi>\<chi> i. 1)::'a) < 0"
         by (simp add: mult_less_0_iff)
diff -r dd203341fd2b -r 453803d28c4b src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Aug 19 10:23:16 2011 +0900
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 18 22:32:19 2011 -0700
@@ -5570,9 +5570,6 @@
 
 subsection {* Some properties of a canonical subspace *}
 
-(** move **)
-declare euclidean_component_zero[simp]
-
 lemma subspace_substandard:
   "subspace {x::'a::euclidean_space. (\<forall>i<DIM('a). P i \<longrightarrow> x$$i = 0)}"
   unfolding subspace_def by(auto simp add: euclidean_simps) (* FIXME: duplicate rewrite rule *)
diff -r dd203341fd2b -r 453803d28c4b src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Fri Aug 19 10:23:16 2011 +0900
+++ b/src/HOL/NthRoot.thy	Thu Aug 18 22:32:19 2011 -0700
@@ -29,7 +29,7 @@
       using n1 by (rule power_increasing, simp)
     finally show "a \<le> max 1 a ^ n" .
     show "\<forall>r. 0 \<le> r \<and> r \<le> max 1 a \<longrightarrow> isCont (\<lambda>x. x ^ n) r"
-      by (simp add: isCont_power)
+      by simp
   qed
   then obtain r where r: "0 \<le> r \<and> r ^ n = a" by fast
   with n a have "r \<noteq> 0" by (auto simp add: power_0_left)
@@ -310,7 +310,7 @@
     show "\<forall>z. \<bar>z - root n x\<bar> \<le> root n x \<longrightarrow> root n (z ^ n) = z"
       by (simp add: abs_le_iff real_root_power_cancel n)
     show "\<forall>z. \<bar>z - root n x\<bar> \<le> root n x \<longrightarrow> isCont (\<lambda>a. a ^ n) z"
-      by (simp add: isCont_power)
+      by simp
   qed
   thus ?thesis using n x by simp
 qed
@@ -320,7 +320,7 @@
 apply (subgoal_tac "isCont (\<lambda>x. - root n (- x)) x")
 apply (simp add: real_root_minus)
 apply (rule isCont_o2 [OF isCont_minus [OF isCont_ident]])
-apply (simp add: isCont_minus isCont_root_pos)
+apply (simp add: isCont_root_pos)
 done
 
 lemma isCont_root_zero:
diff -r dd203341fd2b -r 453803d28c4b src/HOL/Series.thy
--- a/src/HOL/Series.thy	Fri Aug 19 10:23:16 2011 +0900
+++ b/src/HOL/Series.thy	Thu Aug 18 22:32:19 2011 -0700
@@ -26,10 +26,7 @@
    suminf   :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> 'a" where
    "suminf f = (THE s. f sums s)"
 
-syntax
-  "_suminf" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a" ("\<Sum>_. _" [0, 10] 10)
-translations
-  "\<Sum>i. b" == "CONST suminf (%i. b)"
+notation suminf (binder "\<Sum>" 10)
 
 
 lemma [trans]: "f=g ==> g sums z ==> f sums z"
@@ -560,7 +557,7 @@
   moreover have "summable ?g" by (rule summable_zero)
   moreover from sm have "summable f" .
   ultimately have "suminf ?g \<le> suminf f" by (rule summable_le)
-  then show "0 \<le> suminf f" by (simp add: suminf_zero)
+  then show "0 \<le> suminf f" by simp
 qed
 
 
diff -r dd203341fd2b -r 453803d28c4b src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Fri Aug 19 10:23:16 2011 +0900
+++ b/src/HOL/Transcendental.thy	Thu Aug 18 22:32:19 2011 -0700
@@ -881,7 +881,7 @@
 by (simp add: diffs_def)
 
 lemma lemma_exp_ext: "exp = (\<lambda>x. \<Sum>n. x ^ n /\<^sub>R real (fact n))"
-by (auto intro!: ext simp add: exp_def)
+by (auto simp add: exp_def)
 
 lemma DERIV_exp [simp]: "DERIV exp x :> exp(x)"
 apply (simp add: exp_def)
@@ -1248,7 +1248,7 @@
       by (rule DERIV_diff)
     thus "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> 0" by auto
   qed (auto simp add: assms)
-  thus ?thesis by (auto simp add: suminf_zero)
+  thus ?thesis by auto
 qed
 
 subsection {* Sine and Cosine *}
@@ -1337,10 +1337,10 @@
 by (auto intro!: sums_unique sums_minus sin_converges)
 
 lemma lemma_sin_ext: "sin = (\<lambda>x. \<Sum>n. sin_coeff n * x ^ n)"
-by (auto intro!: ext simp add: sin_def)
+  by (auto simp add: sin_def)
 
 lemma lemma_cos_ext: "cos = (\<lambda>x. \<Sum>n. cos_coeff n * x ^ n)"
-by (auto intro!: ext simp add: cos_def)
+  by (auto simp add: cos_def)
 
 lemma DERIV_sin [simp]: "DERIV sin x :> cos(x)"
 apply (simp add: cos_def)