--- 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])
--- 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
--- 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
--- 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"
--- 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)
--- 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 *)
--- 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:
--- 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
--- 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)