--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Thu Apr 27 11:06:47 2017 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Thu Apr 27 15:59:00 2017 +0100
@@ -831,7 +831,7 @@
apply (drule has_integral_affinity01 [where m= "-1" and c=1])
apply (auto simp: reversepath_def valid_path_def piecewise_C1_differentiable_on_def)
apply (drule has_integral_neg)
- apply (rule_tac s = "(\<lambda>x. 1 - x) ` s" in has_integral_spike_finite)
+ apply (rule_tac S = "(\<lambda>x. 1 - x) ` s" in has_integral_spike_finite)
apply (auto simp: *)
done
qed
@@ -1114,7 +1114,7 @@
have "((\<lambda>x. f (shiftpath a g x) * vector_derivative (shiftpath a g) (at x))
has_integral integral {a..1} (\<lambda>x. f (g x) * vector_derivative g (at x))) {0..1 - a}"
apply (rule has_integral_spike_finite
- [where s = "{1-a} \<union> (\<lambda>x. x-a) ` s" and f = "\<lambda>x. f(g(a+x)) * vector_derivative g (at(a+x))"])
+ [where S = "{1-a} \<union> (\<lambda>x. x-a) ` s" and f = "\<lambda>x. f(g(a+x)) * vector_derivative g (at(a+x))"])
using s apply blast
using a apply (auto simp: algebra_simps vd1)
apply (force simp: shiftpath_def add.commute)
@@ -1125,7 +1125,7 @@
have "((\<lambda>x. f (shiftpath a g x) * vector_derivative (shiftpath a g) (at x))
has_integral integral {0..a} (\<lambda>x. f (g x) * vector_derivative g (at x))) {1 - a..1}"
apply (rule has_integral_spike_finite
- [where s = "{1-a} \<union> (\<lambda>x. x-a+1) ` s" and f = "\<lambda>x. f(g(a+x-1)) * vector_derivative g (at(a+x-1))"])
+ [where S = "{1-a} \<union> (\<lambda>x. x-a+1) ` s" and f = "\<lambda>x. f(g(a+x-1)) * vector_derivative g (at(a+x-1))"])
using s apply blast
using a apply (auto simp: algebra_simps vd2)
apply (force simp: shiftpath_def add.commute)
@@ -1324,7 +1324,7 @@
apply (cut_tac has_integral_cmul [OF *, where c = "v-u"])
using fs assms
apply (simp add: False subpath_def has_contour_integral)
- apply (rule_tac s = "(\<lambda>t. ((v-u) *\<^sub>R t + u)) -` s" in has_integral_spike_finite)
+ apply (rule_tac S = "(\<lambda>t. ((v-u) *\<^sub>R t + u)) -` s" in has_integral_spike_finite)
apply (auto simp: inj_on_def False finite_vimageI vd scaleR_conv_of_real)
done
qed
@@ -3543,6 +3543,63 @@
apply (force simp: algebra_simps)
done
+subsubsection\<open>Some lemmas about negating a path.\<close>
+
+lemma valid_path_negatepath: "valid_path \<gamma> \<Longrightarrow> valid_path (uminus \<circ> \<gamma>)"
+ unfolding o_def using piecewise_C1_differentiable_neg valid_path_def by blast
+
+lemma has_contour_integral_negatepath:
+ assumes \<gamma>: "valid_path \<gamma>" and cint: "((\<lambda>z. f (- z)) has_contour_integral - i) \<gamma>"
+ shows "(f has_contour_integral i) (uminus \<circ> \<gamma>)"
+proof -
+ obtain S where cont: "continuous_on {0..1} \<gamma>" and "finite S" and diff: "\<gamma> C1_differentiable_on {0..1} - S"
+ using \<gamma> by (auto simp: valid_path_def piecewise_C1_differentiable_on_def)
+ have "((\<lambda>x. - (f (- \<gamma> x) * vector_derivative \<gamma> (at x within {0..1}))) has_integral i) {0..1}"
+ using cint by (auto simp: has_contour_integral_def dest: has_integral_neg)
+ then
+ have "((\<lambda>x. f (- \<gamma> x) * vector_derivative (uminus \<circ> \<gamma>) (at x within {0..1})) has_integral i) {0..1}"
+ proof (rule rev_iffD1 [OF _ has_integral_spike_eq])
+ show "negligible S"
+ by (simp add: \<open>finite S\<close> negligible_finite)
+ show "f (- \<gamma> x) * vector_derivative (uminus \<circ> \<gamma>) (at x within {0..1}) =
+ - (f (- \<gamma> x) * vector_derivative \<gamma> (at x within {0..1}))"
+ if "x \<in> {0..1} - S" for x
+ proof -
+ have "vector_derivative (uminus \<circ> \<gamma>) (at x within cbox 0 1) = - vector_derivative \<gamma> (at x within cbox 0 1)"
+ apply (rule vector_derivative_within_closed_interval)
+ using that
+ apply (auto simp: o_def)
+ apply (rule has_vector_derivative_minus)
+ by (metis C1_differentiable_on_def diff has_vector_derivative_at_within that vector_derivative_at_within_ivl zero_less_one)
+ then show ?thesis
+ by simp
+ qed
+ qed
+ then show ?thesis by (simp add: has_contour_integral_def)
+qed
+
+lemma winding_number_negatepath:
+ assumes \<gamma>: "valid_path \<gamma>" and 0: "0 \<notin> path_image \<gamma>"
+ shows "winding_number(uminus \<circ> \<gamma>) 0 = winding_number \<gamma> 0"
+proof -
+ have "op / 1 contour_integrable_on \<gamma>"
+ using "0" \<gamma> contour_integrable_inversediff by fastforce
+ then have "((\<lambda>z. 1/z) has_contour_integral contour_integral \<gamma> (op / 1)) \<gamma>"
+ by (rule has_contour_integral_integral)
+ then have "((\<lambda>z. 1 / - z) has_contour_integral - contour_integral \<gamma> (op / 1)) \<gamma>"
+ using has_contour_integral_neg by auto
+ then show ?thesis
+ using assms
+ apply (simp add: winding_number_valid_path valid_path_negatepath image_def path_defs)
+ apply (simp add: contour_integral_unique has_contour_integral_negatepath)
+ done
+qed
+
+lemma contour_integrable_negatepath:
+ assumes \<gamma>: "valid_path \<gamma>" and pi: "(\<lambda>z. f (- z)) contour_integrable_on \<gamma>"
+ shows "f contour_integrable_on (uminus \<circ> \<gamma>)"
+ by (metis \<gamma> add.inverse_inverse contour_integrable_on_def has_contour_integral_negatepath pi)
+
(* A combined theorem deducing several things piecewise.*)
lemma winding_number_join_pos_combined:
"\<lbrakk>valid_path \<gamma>1; z \<notin> path_image \<gamma>1; 0 < Re(winding_number \<gamma>1 z);
@@ -3551,7 +3608,7 @@
by (simp add: valid_path_join path_image_join winding_number_join valid_path_imp_path)
-(* Useful sufficient conditions for the winding number to be positive etc.*)
+subsubsection\<open>Useful sufficient conditions for the winding number to be positive\<close>
lemma Re_winding_number:
"\<lbrakk>valid_path \<gamma>; z \<notin> path_image \<gamma>\<rbrakk>
@@ -5589,13 +5646,13 @@
"\<lbrakk>f holomorphic_on s; open s\<rbrakk> \<Longrightarrow> (deriv f) holomorphic_on s"
by (metis DERIV_deriv_iff_field_differentiable at_within_open derivative_is_holomorphic holomorphic_on_def)
-lemma analytic_deriv: "f analytic_on s \<Longrightarrow> (deriv f) analytic_on s"
+lemma analytic_deriv [analytic_intros]: "f analytic_on s \<Longrightarrow> (deriv f) analytic_on s"
using analytic_on_holomorphic holomorphic_deriv by auto
lemma holomorphic_higher_deriv [holomorphic_intros]: "\<lbrakk>f holomorphic_on s; open s\<rbrakk> \<Longrightarrow> (deriv ^^ n) f holomorphic_on s"
by (induction n) (auto simp: holomorphic_deriv)
-lemma analytic_higher_deriv: "f analytic_on s \<Longrightarrow> (deriv ^^ n) f analytic_on s"
+lemma analytic_higher_deriv [analytic_intros]: "f analytic_on s \<Longrightarrow> (deriv ^^ n) f analytic_on s"
unfolding analytic_on_def using holomorphic_higher_deriv by blast
lemma has_field_derivative_higher_deriv:
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Thu Apr 27 11:06:47 2017 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Thu Apr 27 15:59:00 2017 +0100
@@ -482,6 +482,8 @@
where
"f analytic_on s \<equiv> \<forall>x \<in> s. \<exists>e. 0 < e \<and> f holomorphic_on (ball x e)"
+named_theorems analytic_intros "introduction rules for proving analyticity"
+
lemma analytic_imp_holomorphic: "f analytic_on s \<Longrightarrow> f holomorphic_on s"
by (simp add: at_within_open [OF _ open_ball] analytic_on_def holomorphic_on_def)
(metis centre_in_ball field_differentiable_at_within)
@@ -531,16 +533,16 @@
finally show ?thesis .
qed
-lemma analytic_on_linear: "(op * c) analytic_on s"
- by (auto simp add: analytic_on_holomorphic holomorphic_on_linear)
+lemma analytic_on_linear [analytic_intros,simp]: "(op * c) analytic_on s"
+ by (auto simp add: analytic_on_holomorphic)
-lemma analytic_on_const: "(\<lambda>z. c) analytic_on s"
+lemma analytic_on_const [analytic_intros,simp]: "(\<lambda>z. c) analytic_on s"
by (metis analytic_on_def holomorphic_on_const zero_less_one)
-lemma analytic_on_ident: "(\<lambda>x. x) analytic_on s"
- by (simp add: analytic_on_def holomorphic_on_ident gt_ex)
+lemma analytic_on_ident [analytic_intros,simp]: "(\<lambda>x. x) analytic_on s"
+ by (simp add: analytic_on_def gt_ex)
-lemma analytic_on_id: "id analytic_on s"
+lemma analytic_on_id [analytic_intros]: "id analytic_on s"
unfolding id_def by (rule analytic_on_ident)
lemma analytic_on_compose:
@@ -572,11 +574,11 @@
\<Longrightarrow> g o f analytic_on s"
by (metis analytic_on_compose analytic_on_subset image_subset_iff)
-lemma analytic_on_neg:
+lemma analytic_on_neg [analytic_intros]:
"f analytic_on s \<Longrightarrow> (\<lambda>z. -(f z)) analytic_on s"
by (metis analytic_on_holomorphic holomorphic_on_minus)
-lemma analytic_on_add:
+lemma analytic_on_add [analytic_intros]:
assumes f: "f analytic_on s"
and g: "g analytic_on s"
shows "(\<lambda>z. f z + g z) analytic_on s"
@@ -596,7 +598,7 @@
by (metis e e' min_less_iff_conj)
qed
-lemma analytic_on_diff:
+lemma analytic_on_diff [analytic_intros]:
assumes f: "f analytic_on s"
and g: "g analytic_on s"
shows "(\<lambda>z. f z - g z) analytic_on s"
@@ -616,7 +618,7 @@
by (metis e e' min_less_iff_conj)
qed
-lemma analytic_on_mult:
+lemma analytic_on_mult [analytic_intros]:
assumes f: "f analytic_on s"
and g: "g analytic_on s"
shows "(\<lambda>z. f z * g z) analytic_on s"
@@ -636,7 +638,7 @@
by (metis e e' min_less_iff_conj)
qed
-lemma analytic_on_inverse:
+lemma analytic_on_inverse [analytic_intros]:
assumes f: "f analytic_on s"
and nz: "(\<And>z. z \<in> s \<Longrightarrow> f z \<noteq> 0)"
shows "(\<lambda>z. inverse (f z)) analytic_on s"
@@ -658,7 +660,7 @@
by (metis e e' min_less_iff_conj)
qed
-lemma analytic_on_divide:
+lemma analytic_on_divide [analytic_intros]:
assumes f: "f analytic_on s"
and g: "g analytic_on s"
and nz: "(\<And>z. z \<in> s \<Longrightarrow> g z \<noteq> 0)"
@@ -666,11 +668,11 @@
unfolding divide_inverse
by (metis analytic_on_inverse analytic_on_mult f g nz)
-lemma analytic_on_power:
+lemma analytic_on_power [analytic_intros]:
"f analytic_on s \<Longrightarrow> (\<lambda>z. (f z) ^ n) analytic_on s"
-by (induct n) (auto simp: analytic_on_const analytic_on_mult)
+by (induct n) (auto simp: analytic_on_mult)
-lemma analytic_on_sum:
+lemma analytic_on_sum [analytic_intros]:
"(\<And>i. i \<in> I \<Longrightarrow> (f i) analytic_on s) \<Longrightarrow> (\<lambda>x. sum (\<lambda>i. f i x) I) analytic_on s"
by (induct I rule: infinite_finite_induct) (auto simp: analytic_on_const analytic_on_add)
--- a/src/HOL/Analysis/Complex_Transcendental.thy Thu Apr 27 11:06:47 2017 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Thu Apr 27 15:59:00 2017 +0100
@@ -1401,7 +1401,7 @@
Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] Re_Ln_pos_le [of z]
by (simp add: Ln_times) auto
-lemma Ln_of_nat: "0 < n \<Longrightarrow> Ln (of_nat n) = of_real (ln (of_nat n))"
+lemma Ln_of_nat [simp]: "0 < n \<Longrightarrow> Ln (of_nat n) = of_real (ln (of_nat n))"
by (subst of_real_of_nat_eq[symmetric], subst Ln_of_real[symmetric]) simp_all
lemma Ln_of_nat_over_of_nat:
@@ -1936,14 +1936,13 @@
qed
lemma lim_Ln_over_n: "((\<lambda>n. Ln(of_nat n) / of_nat n) \<longlongrightarrow> 0) sequentially"
- using lim_Ln_over_power [of 1]
- by simp
-
-lemma Ln_Reals_eq: "x \<in> \<real> \<Longrightarrow> Re x > 0 \<Longrightarrow> Ln x = of_real (ln (Re x))"
+ using lim_Ln_over_power [of 1] by simp
+
+lemma Ln_Reals_eq: "\<lbrakk>x \<in> \<real>; Re x > 0\<rbrakk> \<Longrightarrow> Ln x = of_real (ln (Re x))"
using Ln_of_real by force
-lemma powr_Reals_eq: "x \<in> \<real> \<Longrightarrow> Re x > 0 \<Longrightarrow> x powr complex_of_real y = of_real (x powr y)"
- by (simp add: powr_of_real)
+lemma powr_Reals_eq: "\<lbrakk>x \<in> \<real>; y \<in> \<real>; Re x > 0\<rbrakk> \<Longrightarrow> x powr y = of_real (Re x powr Re y)"
+ by (metis linear not_le of_real_Re powr_of_real)
lemma lim_ln_over_power:
fixes s :: real
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Apr 27 11:06:47 2017 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Apr 27 15:59:00 2017 +0100
@@ -683,7 +683,7 @@
by (simp add: AE_iff_measurable)
show ?thesis
proof (rule has_integral_spike_eq[symmetric])
- show "\<forall>x\<in>\<Omega> - N. f x = g x" using N(3) by auto
+ show "\<And>x. x\<in>\<Omega> - N \<Longrightarrow> f x = g x" using N(3) by auto
show "negligible N"
unfolding negligible_def
proof (intro allI)
@@ -2246,7 +2246,7 @@
proof
show "(\<lambda>x. norm (g x)) integrable_on s"
using le norm_ge_zero[of "f _"]
- by (intro integrable_spike_finite[OF _ _ g, where s="{}"])
+ by (intro integrable_spike_finite[OF _ _ g, of "{}"])
(auto intro!: abs_of_nonneg intro: order_trans simp del: norm_ge_zero)
qed fact
show "set_borel_measurable lebesgue s f"
@@ -2266,9 +2266,9 @@
unfolding absolutely_integrable_on_def
proof
show "(\<lambda>x. norm (h x)) integrable_on s"
- proof (intro integrable_spike_finite[OF _ _ h, where s="{}"] ballI)
+ proof (intro integrable_spike_finite[OF _ _ h, of "{}"] ballI)
fix x assume "x \<in> s - {}" then show "norm (h x) = h x"
- using order_trans[OF norm_ge_zero le[THEN bspec, of x]] by auto
+ by (metis Diff_empty abs_of_nonneg bot_set_def le norm_ge_zero order_trans real_norm_def)
qed auto
qed fact
have 2: "set_borel_measurable lebesgue s (f k)" for k
--- a/src/HOL/Analysis/Gamma_Function.thy Thu Apr 27 11:06:47 2017 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy Thu Apr 27 15:59:00 2017 +0100
@@ -2785,7 +2785,7 @@
by (intro has_integral_spike_finite_eq[of "{0}"]) (simp_all add: powr_def Ln_of_real)
also have "fact n * of_nat n / pochhammer z (n+1) * exp ((z - 1) * Ln (of_nat n)) =
(of_nat n powr z * fact n / pochhammer z (n+1))"
- by (auto simp add: powr_def algebra_simps exp_diff)
+ by (auto simp add: powr_def algebra_simps exp_diff exp_of_real)
finally show ?thesis by (subst has_integral_restrict) simp_all
next
case False
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Apr 27 11:06:47 2017 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Apr 27 15:59:00 2017 +0100
@@ -2238,78 +2238,50 @@
lemma has_integral_spike:
fixes f :: "'b::euclidean_space \<Rightarrow> 'a::real_normed_vector"
- assumes "negligible s"
- and "(\<forall>x\<in>(t - s). g x = f x)"
- and "(f has_integral y) t"
- shows "(g has_integral y) t"
+ assumes "negligible S"
+ and gf: "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
+ and fint: "(f has_integral y) T"
+ shows "(g has_integral y) T"
proof -
- {
- fix a b :: 'b
- fix f g :: "'b \<Rightarrow> 'a"
- fix y :: 'a
- assume as: "\<forall>x \<in> cbox a b - s. g x = f x" "(f has_integral y) (cbox a b)"
+ have *: "(g has_integral y) (cbox a b)"
+ if "(f has_integral y) (cbox a b)" "\<forall>x \<in> cbox a b - S. g x = f x" for a b f and g:: "'b \<Rightarrow> 'a" and y
+ proof -
have "((\<lambda>x. f x + (g x - f x)) has_integral (y + 0)) (cbox a b)"
- apply (rule has_integral_add[OF as(2)])
- apply (rule has_integral_negligible[OF assms(1)])
- using as
- apply auto
- done
- then have "(g has_integral y) (cbox a b)"
+ using that by (intro has_integral_add has_integral_negligible) (auto intro!: \<open>negligible S\<close>)
+ then show ?thesis
by auto
- } note * = this
+ qed
show ?thesis
+ using fint gf
apply (subst has_integral_alt)
- using assms(2-)
- apply -
- apply (rule cond_cases)
- apply safe
- apply (rule *)
- apply assumption+
- apply (subst(asm) has_integral_alt)
- unfolding if_not_P
- apply (erule_tac x=e in allE)
- apply safe
- apply (rule_tac x=B in exI)
- apply safe
- apply (erule_tac x=a in allE)
- apply (erule_tac x=b in allE)
- apply safe
- apply (rule_tac x=z in exI)
- apply safe
- apply (rule *[where fa2="\<lambda>x. if x\<in>t then f x else 0"])
- apply auto
+ apply (subst (asm) has_integral_alt)
+ apply (simp add: split: if_split_asm)
+ apply (blast dest: *)
+ apply (elim all_forward imp_forward ex_forward)
+ apply (force dest: *[where f="\<lambda>x. if x\<in>T then f x else 0" and g="\<lambda>x. if x \<in> T then g x else 0"])+
done
qed
lemma has_integral_spike_eq:
- assumes "negligible s"
- and "\<forall>x\<in>(t - s). g x = f x"
- shows "((f has_integral y) t \<longleftrightarrow> (g has_integral y) t)"
- apply rule
- apply (rule_tac[!] has_integral_spike[OF assms(1)])
- using assms(2)
- apply auto
- done
+ assumes "negligible S"
+ and gf: "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
+ shows "(f has_integral y) T \<longleftrightarrow> (g has_integral y) T"
+ using has_integral_spike [OF \<open>negligible S\<close>] gf
+ by metis
lemma integrable_spike:
- assumes "negligible s"
- and "\<forall>x\<in>(t - s). g x = f x"
- and "f integrable_on t"
- shows "g integrable_on t"
- using assms
- unfolding integrable_on_def
- apply -
- apply (erule exE)
- apply rule
- apply (rule has_integral_spike)
- apply fastforce+
- done
+ assumes "negligible S"
+ and "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
+ and "f integrable_on T"
+ shows "g integrable_on T"
+ using assms unfolding integrable_on_def by (blast intro: has_integral_spike)
lemma integral_spike:
- assumes "negligible s"
- and "\<forall>x\<in>(t - s). g x = f x"
- shows "integral t f = integral t g"
- using has_integral_spike_eq[OF assms] by (simp add: integral_def integrable_on_def)
+ assumes "negligible S"
+ and "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
+ shows "integral T f = integral T g"
+ using has_integral_spike_eq[OF assms]
+ by (auto simp: integral_def integrable_on_def)
subsection \<open>Some other trivialities about negligible sets.\<close>
@@ -2337,7 +2309,7 @@
unfolding negligible_def
proof (safe, goal_cases)
case (1 a b)
- note assm = assms[unfolded negligible_def,rule_format,of a b]
+ note assms[unfolded negligible_def,rule_format,of a b]
then show ?case
apply (subst has_integral_spike_eq[OF assms(2)])
defer
@@ -2405,37 +2377,24 @@
subsection \<open>Finite case of the spike theorem is quite commonly needed.\<close>
lemma has_integral_spike_finite:
- assumes "finite s"
- and "\<forall>x\<in>t-s. g x = f x"
- and "(f has_integral y) t"
- shows "(g has_integral y) t"
- apply (rule has_integral_spike)
- using assms
- apply auto
- done
+ assumes "finite S"
+ and "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
+ and "(f has_integral y) T"
+ shows "(g has_integral y) T"
+ using assms has_integral_spike negligible_finite by blast
lemma has_integral_spike_finite_eq:
- assumes "finite s"
- and "\<forall>x\<in>t-s. g x = f x"
- shows "((f has_integral y) t \<longleftrightarrow> (g has_integral y) t)"
- apply rule
- apply (rule_tac[!] has_integral_spike_finite)
- using assms
- apply auto
- done
+ assumes "finite S"
+ and "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
+ shows "((f has_integral y) T \<longleftrightarrow> (g has_integral y) T)"
+ by (metis assms has_integral_spike_finite)
lemma integrable_spike_finite:
- assumes "finite s"
- and "\<forall>x\<in>t-s. g x = f x"
- and "f integrable_on t"
- shows "g integrable_on t"
- using assms
- unfolding integrable_on_def
- apply safe
- apply (rule_tac x=y in exI)
- apply (rule has_integral_spike_finite)
- apply auto
- done
+ assumes "finite S"
+ and "\<And>x. x \<in> T - S \<Longrightarrow> g x = f x"
+ and "f integrable_on T"
+ shows "g integrable_on T"
+ using assms has_integral_spike_finite by blast
subsection \<open>In particular, the boundary of an interval is negligible.\<close>
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Apr 27 11:06:47 2017 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Apr 27 15:59:00 2017 +0100
@@ -1265,6 +1265,11 @@
lemma cbox_Pair_iff [iff]: "(x, y) \<in> cbox (a, c) (b, d) \<longleftrightarrow> x \<in> cbox a b \<and> y \<in> cbox c d"
by (force simp: cbox_Pair_eq)
+lemma cbox_Complex_eq: "cbox (Complex a c) (Complex b d) = (\<lambda>(x,y). Complex x y) ` (cbox a b \<times> cbox c d)"
+ apply (auto simp: cbox_def Basis_complex_def)
+ apply (rule_tac x = "(Re x, Im x)" in image_eqI)
+ using complex_eq by auto
+
lemma cbox_Pair_eq_0: "cbox (a, c) (b, d) = {} \<longleftrightarrow> cbox a b = {} \<or> cbox c d = {}"
by (force simp: cbox_Pair_eq)
@@ -3916,19 +3921,6 @@
lemma bounded_subset_cball: "bounded S \<longleftrightarrow> (\<exists>e x. S \<subseteq> cball x e \<and> 0 \<le> e)"
unfolding bounded_def subset_eq by auto (meson order_trans zero_le_dist)
-lemma bounded_subset_ballD:
- assumes "bounded S" shows "\<exists>r. 0 < r \<and> S \<subseteq> ball x r"
-proof -
- obtain e::real and y where "S \<subseteq> cball y e" "0 \<le> e"
- using assms by (auto simp: bounded_subset_cball)
- then show ?thesis
- apply (rule_tac x="dist x y + e + 1" in exI)
- apply (simp add: add.commute add_pos_nonneg)
- apply (erule subset_trans)
- apply (clarsimp simp add: cball_def)
- by (metis add_le_cancel_right add_strict_increasing dist_commute dist_triangle_le zero_less_one)
-qed
-
lemma bounded_any_center: "bounded S \<longleftrightarrow> (\<exists>e. \<forall>y\<in>S. dist a y \<le> e)"
unfolding bounded_def
by auto (metis add.commute add_le_cancel_right dist_commute dist_triangle_le)
@@ -4014,6 +4006,22 @@
by (metis insert_is_Un bounded_Un)
qed
+lemma bounded_subset_ballI: "S \<subseteq> ball x r \<Longrightarrow> bounded S"
+ by (meson bounded_ball bounded_subset)
+
+lemma bounded_subset_ballD:
+ assumes "bounded S" shows "\<exists>r. 0 < r \<and> S \<subseteq> ball x r"
+proof -
+ obtain e::real and y where "S \<subseteq> cball y e" "0 \<le> e"
+ using assms by (auto simp: bounded_subset_cball)
+ then show ?thesis
+ apply (rule_tac x="dist x y + e + 1" in exI)
+ apply (simp add: add.commute add_pos_nonneg)
+ apply (erule subset_trans)
+ apply (clarsimp simp add: cball_def)
+ by (metis add_le_cancel_right add_strict_increasing dist_commute dist_triangle_le zero_less_one)
+qed
+
lemma finite_imp_bounded [intro]: "finite S \<Longrightarrow> bounded S"
by (induct set: finite) simp_all