Some new material. SIMPRULE STATUS for sum/prod.delta rules!
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy Thu Jun 15 11:11:36 2017 +0200
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy Thu Jun 15 17:22:23 2017 +0100
@@ -387,7 +387,7 @@
have "(\<Sum>j\<in>Basis. \<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j)) *\<^sub>R j) \<bullet> b
= (\<Sum>j\<in>Basis. if j = b then (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j))) else 0)"
using b
- by (auto simp add: algebra_simps inner_sum_left inner_Basis split: if_split intro!: sum.cong)
+ by (simp add: inner_sum_left inner_Basis if_distrib cong: if_cong) (simp add: sum.commute)
also have "\<dots> = (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> b)))"
using b by (simp add: sum.delta)
also have "\<dots> = f x \<bullet> b"
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Thu Jun 15 11:11:36 2017 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Thu Jun 15 17:22:23 2017 +0100
@@ -919,7 +919,6 @@
apply (auto simp: bounded_linear_mult_right)
done
-(*Used only once, in Multivariate/cauchy.ml. *)
lemma has_complex_derivative_inverse_strong:
fixes f :: "complex \<Rightarrow> complex"
shows "DERIV f x :> f' \<Longrightarrow>
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Jun 15 11:11:36 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Jun 15 17:22:23 2017 +0100
@@ -55,7 +55,7 @@
lemma content_unit[iff]: "content (cbox 0 (One::'a::euclidean_space)) = 1"
by simp
-lemma content_pos_le[intro]: "0 \<le> content (cbox a b)"
+lemma content_pos_le [iff]: "0 \<le> content X"
by simp
corollary content_nonneg [simp]: "~ content (cbox a b) < 0"
@@ -157,20 +157,18 @@
lemma sum_content_null:
assumes "content (cbox a b) = 0"
and "p tagged_division_of (cbox a b)"
- shows "sum (\<lambda>(x,k). content k *\<^sub>R f x) p = (0::'a::real_normed_vector)"
+ shows "(\<Sum>(x,k)\<in>p. content k *\<^sub>R f x) = (0::'a::real_normed_vector)"
proof (rule sum.neutral, rule)
fix y
assume y: "y \<in> p"
obtain x k where xk: "y = (x, k)"
using surj_pair[of y] by blast
- note assm = tagged_division_ofD(3-4)[OF assms(2) y[unfolded xk]]
- from this(2) obtain c d where k: "k = cbox c d" by blast
+ then obtain c d where k: "k = cbox c d" "k \<subseteq> cbox a b"
+ by (metis assms(2) tagged_division_ofD(3) tagged_division_ofD(4) y)
have "(\<lambda>(x, k). content k *\<^sub>R f x) y = content k *\<^sub>R f x"
unfolding xk by auto
also have "\<dots> = 0"
- using content_subset[OF assm(1)[unfolded k]] content_pos_le[of c d]
- unfolding assms(1) k
- by auto
+ using assms(1) content_0_subset k(2) by auto
finally show "(\<lambda>(x, k). content k *\<^sub>R f x) y = 0" .
qed
@@ -446,6 +444,11 @@
"(f has_integral y) s \<Longrightarrow> ((\<lambda>x. f x *\<^sub>R c) has_integral (y *\<^sub>R c)) s"
using has_integral_linear[OF _ bounded_linear_scaleR_left] by (simp add: comp_def)
+lemma integrable_on_scaleR_left:
+ assumes "f integrable_on A"
+ shows "(\<lambda>x. f x *\<^sub>R y) integrable_on A"
+ using assms has_integral_scaleR_left unfolding integrable_on_def by blast
+
lemma has_integral_mult_left:
fixes c :: "_ :: real_normed_algebra"
shows "(f has_integral y) s \<Longrightarrow> ((\<lambda>x. f x * c) has_integral (y * c)) s"
@@ -670,12 +673,8 @@
by (auto intro: has_integral_sum integrable_integral)
lemma integrable_sum:
- "\<lbrakk>finite t; \<forall>a\<in>t. (f a) integrable_on s\<rbrakk> \<Longrightarrow> (\<lambda>x. sum (\<lambda>a. f a x) t) integrable_on s"
- unfolding integrable_on_def
- apply (drule bchoice)
- using has_integral_sum[of t]
- apply auto
- done
+ "\<lbrakk>finite I; \<And>a. a \<in> I \<Longrightarrow> f a integrable_on S\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Sum>a\<in>I. f a x) integrable_on S"
+ unfolding integrable_on_def using has_integral_sum[of I] by metis
lemma has_integral_eq:
assumes "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
@@ -5493,32 +5492,10 @@
apply (rule_tac[!] sum_nonneg)
apply safe
unfolding real_scaleR_def right_diff_distrib[symmetric]
- apply (rule_tac[!] mult_nonneg_nonneg)
- proof -
- fix a b
- assume ab: "(a, b) \<in> p1"
- show "0 \<le> content b"
- using *(3)[OF ab]
- apply safe
- apply (rule content_pos_le)
+ apply (rule_tac[!] mult_nonneg_nonneg)
+ apply simp_all
+ using obt(4) prems(1) prems(4) apply (blast intro: elim: dest!: bspec)+
done
- then show "0 \<le> content b" .
- show "0 \<le> f a - g a" "0 \<le> h a - f a"
- using *(1-2)[OF ab]
- using obt(4)[rule_format,of a]
- by auto
- next
- fix a b
- assume ab: "(a, b) \<in> p2"
- show "0 \<le> content b"
- using *(6)[OF ab]
- apply safe
- apply (rule content_pos_le)
- done
- then show "0 \<le> content b" .
- show "0 \<le> f a - g a" and "0 \<le> h a - f a"
- using *(4-5)[OF ab] using obt(4)[rule_format,of a] by auto
- qed
then show ?case
apply -
unfolding real_norm_def
@@ -6317,7 +6294,7 @@
proof (rule, goal_cases)
case prems: (1 x)
have "e / (4 * content (cbox a b)) > 0"
- using \<open>e>0\<close> False content_pos_le[of a b] by (simp add: less_le)
+ by (simp add: False content_lt_nz e)
from assms(3)[rule_format, OF prems, THEN LIMSEQ_D, OF this]
guess n .. note n=this
then show ?case
@@ -7094,9 +7071,10 @@
also have "\<dots> = content (cbox a b) * e * norm (x - x0)"
by simp
also have "\<dots> < e' * norm (x - x0)"
- using \<open>e' > 0\<close> content_pos_le[of a b]
- by (intro mult_strict_right_mono[OF _ \<open>0 < norm (x - x0)\<close>])
- (auto simp: divide_simps e_def simp del: measure_nonneg)
+ using \<open>e' > 0\<close>
+ apply (intro mult_strict_right_mono[OF _ \<open>0 < norm (x - x0)\<close>])
+ apply (auto simp: divide_simps e_def)
+ by (metis \<open>0 < e\<close> e_def order.asym zero_less_divide_iff)
finally have "norm (?F x - ?F x0 - ?dF (x - x0)) < e' * norm (x - x0)" .
then show ?case
by (auto simp: divide_simps)
@@ -7207,8 +7185,7 @@
define e' where "e' = e / 2"
with \<open>e > 0\<close> have "e' > 0" by simp
then have "\<forall>\<^sub>F n in F. \<forall>x\<in>cbox a b. norm (f n x - g x) < e' / content (cbox a b)"
- using u content_nonzero content_pos_le[of a b]
- by (auto simp: uniform_limit_iff dist_norm simp del: measure_nonneg)
+ using u content_nonzero by (auto simp: uniform_limit_iff dist_norm zero_less_measure_iff)
then show "\<forall>\<^sub>F n in F. dist (I n) J < e"
proof eventually_elim
case (elim n)
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Jun 15 11:11:36 2017 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Jun 15 17:22:23 2017 +0100
@@ -1665,8 +1665,8 @@
definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
(\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. ((a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i) \<or> (b\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> a\<bullet>i))) \<longrightarrow> x \<in> s)"
-lemma is_interval_cbox: "is_interval (cbox a (b::'a::euclidean_space))" (is ?th1)
- and is_interval_box: "is_interval (box a b)" (is ?th2)
+lemma is_interval_cbox [simp]: "is_interval (cbox a (b::'a::euclidean_space))" (is ?th1)
+ and is_interval_box [simp]: "is_interval (box a b)" (is ?th2)
unfolding is_interval_def mem_box Ball_def atLeastAtMost_iff
by (meson order_trans le_less_trans less_le_trans less_trans)+
@@ -1726,12 +1726,28 @@
by (simp add: box_ne_empty inner_Basis inner_sum_left sum_nonneg)
lemma box01_nonempty [simp]: "box 0 One \<noteq> {}"
- by (simp add: box_ne_empty inner_Basis inner_sum_left) (simp add: sum.remove)
+ by (simp add: box_ne_empty inner_Basis inner_sum_left)
lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)"
using nonempty_Basis box01_nonempty box_eq_empty(1) box_ne_empty(1) by blast
-
+lemma interval_subset_is_interval:
+ assumes "is_interval S"
+ shows "cbox a b \<subseteq> S \<longleftrightarrow> cbox a b = {} \<or> a \<in> S \<and> b \<in> S" (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then show ?rhs using box_ne_empty(1) mem_box(2) by fastforce
+next
+ assume ?rhs
+ have "cbox a b \<subseteq> S" if "a \<in> S" "b \<in> S"
+ using assms unfolding is_interval_def
+ apply (clarsimp simp add: mem_box)
+ using that by blast
+ with \<open>?rhs\<close> show ?lhs
+ by blast
+qed
+
+
subsection \<open>Connectedness\<close>
lemma connected_local:
@@ -5641,35 +5657,6 @@
qed
qed (metis compact_imp_complete compact_imp_seq_compact seq_compact_imp_totally_bounded)
-lemma cauchy: "Cauchy s \<longleftrightarrow> (\<forall>e>0.\<exists> N::nat. \<forall>n\<ge>N. dist(s n)(s N) < e)" (is "?lhs = ?rhs")
-proof -
- {
- assume ?rhs
- {
- fix e::real
- assume "e>0"
- with \<open>?rhs\<close> obtain N where N:"\<forall>n\<ge>N. dist (s n) (s N) < e/2"
- by (erule_tac x="e/2" in allE) auto
- {
- fix n m
- assume nm:"N \<le> m \<and> N \<le> n"
- then have "dist (s m) (s n) < e" using N
- using dist_triangle_half_l[of "s m" "s N" "e" "s n"]
- by blast
- }
- then have "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < e"
- by blast
- }
- then have ?lhs
- unfolding cauchy_def
- by blast
- }
- then show ?thesis
- unfolding cauchy_def
- using dist_triangle_half_l
- by blast
-qed
-
lemma cauchy_imp_bounded:
assumes "Cauchy s"
shows "bounded (range s)"
@@ -6978,6 +6965,11 @@
ultimately show ?thesis ..
qed
+lemma bounded_uniformly_continuous_image:
+ fixes f :: "'a :: heine_borel \<Rightarrow> 'b :: heine_borel"
+ assumes "uniformly_continuous_on S f" "bounded S"
+ shows "bounded(image f S)"
+ by (metis (no_types, lifting) assms bounded_closure_image compact_closure compact_continuous_image compact_eq_bounded_closed image_cong uniformly_continuous_imp_continuous uniformly_continuous_on_extension_on_closure)
subsection\<open>Quotient maps\<close>
@@ -9521,7 +9513,7 @@
have "\<exists>N. \<forall>n\<ge>N. norm (x n - x N) < d" if "d > 0" for d :: real
proof -
from that obtain N where N: "\<forall>n\<ge>N. norm (f (x n) - f (x N)) < e * d"
- using cf[unfolded cauchy o_def dist_norm, THEN spec[where x="e*d"]] e
+ using cf[unfolded Cauchy_def o_def dist_norm, THEN spec[where x="e*d"]] e
by auto
have "norm (x n - x N) < d" if "n \<ge> N" for n
proof -
@@ -9538,7 +9530,7 @@
then show ?thesis by auto
qed
then show ?thesis
- by (simp add: cauchy dist_norm)
+ by (simp add: Cauchy_altdef2 dist_norm)
qed
lemma complete_isometric_image:
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Thu Jun 15 11:11:36 2017 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Thu Jun 15 17:22:23 2017 +0100
@@ -923,9 +923,7 @@
lemma fps_sum_rep_nth: "(sum (\<lambda>i. fps_const(a$i)*X^i) {0..m})$n =
(if n \<le> m then a$n else 0::'a::comm_ring_1)"
- apply (auto simp add: fps_sum_nth cond_value_iff cong del: if_weak_cong)
- apply (simp add: sum.delta')
- done
+ by (auto simp add: fps_sum_nth cond_value_iff cong del: if_weak_cong)
lemma fps_notation: "(\<lambda>n. sum (\<lambda>i. fps_const(a$i) * X^i) {0..n}) \<longlonglongrightarrow> a"
(is "?s \<longlonglongrightarrow> a")
--- a/src/HOL/Groups_Big.thy Thu Jun 15 11:11:36 2017 +0200
+++ b/src/HOL/Groups_Big.thy Thu Jun 15 17:22:23 2017 +0100
@@ -332,7 +332,7 @@
by (intro reindex_bij_betw_not_neutral[OF _ _ bij]) auto
qed
-lemma delta:
+lemma delta [simp]:
assumes fS: "finite S"
shows "F (\<lambda>k. if k = a then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
proof -
@@ -355,7 +355,7 @@
qed
qed
-lemma delta':
+lemma delta' [simp]:
assumes fin: "finite S"
shows "F (\<lambda>k. if a = k then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
using delta [OF fin, of a b, symmetric] by (auto intro: cong)
--- a/src/HOL/Probability/Fin_Map.thy Thu Jun 15 11:11:36 2017 +0200
+++ b/src/HOL/Probability/Fin_Map.thy Thu Jun 15 17:22:23 2017 +0100
@@ -474,7 +474,7 @@
fix P::"nat \<Rightarrow> 'a \<Rightarrow>\<^sub>F 'b"
assume "Cauchy P"
then obtain Nd where Nd: "\<And>n. n \<ge> Nd \<Longrightarrow> dist (P n) (P Nd) < 1"
- by (force simp: cauchy)
+ by (force simp: Cauchy_altdef2)
define d where "d = domain (P Nd)"
with Nd have dim: "\<And>n. n \<ge> Nd \<Longrightarrow> domain (P n) = d" using dist_le_1_imp_domain_eq by auto
have [simp]: "finite d" unfolding d_def by simp
@@ -484,11 +484,11 @@
have q: "\<And>i. i \<in> d \<Longrightarrow> q i = Q i" by (auto simp add: Q_def Abs_fmap_inverse)
{
fix i assume "i \<in> d"
- have "Cauchy (p i)" unfolding cauchy p_def
+ have "Cauchy (p i)" unfolding Cauchy_altdef2 p_def
proof safe
fix e::real assume "0 < e"
with \<open>Cauchy P\<close> obtain N where N: "\<And>n. n\<ge>N \<Longrightarrow> dist (P n) (P N) < min e 1"
- by (force simp: cauchy min_def)
+ by (force simp: Cauchy_altdef2 min_def)
hence "\<And>n. n \<ge> N \<Longrightarrow> domain (P n) = domain (P N)" using dist_le_1_imp_domain_eq by auto
with dim have dim: "\<And>n. n \<ge> N \<Longrightarrow> domain (P n) = d" by (metis nat_le_linear)
show "\<exists>N. \<forall>n\<ge>N. dist ((P n) i) ((P N) i) < e"
--- a/src/HOL/Probability/Probability_Mass_Function.thy Thu Jun 15 11:11:36 2017 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Thu Jun 15 17:22:23 2017 +0100
@@ -2111,7 +2111,7 @@
by (rule sum.commute)
also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then
(\<Sum>x\<in>set (map fst xs). if x = fst (xs ! xa) then snd (xs ! xa) else 0) else 0)"
- by (auto intro!: sum.cong sum.neutral)
+ by (auto intro!: sum.cong sum.neutral simp del: sum.delta)
also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then snd (xs ! xa) else 0)"
by (intro sum.cong refl) (simp_all add: sum.delta)
also have "\<dots> = sum_list (map snd (filter (\<lambda>x. fst x \<in> A) xs))"
--- a/src/HOL/Real_Vector_Spaces.thy Thu Jun 15 11:11:36 2017 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Thu Jun 15 17:22:23 2017 +0100
@@ -1949,6 +1949,33 @@
qed
qed
+lemma (in metric_space) Cauchy_altdef2: "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N::nat. \<forall>n\<ge>N. dist(s n)(s N) < e)" (is "?lhs = ?rhs")
+proof
+ assume "Cauchy s"
+ then show ?rhs by (force simp add: Cauchy_def)
+next
+ assume ?rhs
+ {
+ fix e::real
+ assume "e>0"
+ with \<open>?rhs\<close> obtain N where N: "\<forall>n\<ge>N. dist (s n) (s N) < e/2"
+ by (erule_tac x="e/2" in allE) auto
+ {
+ fix n m
+ assume nm: "N \<le> m \<and> N \<le> n"
+ then have "dist (s m) (s n) < e" using N
+ using dist_triangle_half_l[of "s m" "s N" "e" "s n"]
+ by blast
+ }
+ then have "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < e"
+ by blast
+ }
+ then have ?lhs
+ unfolding Cauchy_def by blast
+ then show ?lhs
+ by blast
+qed
+
lemma (in metric_space) metric_CauchyI:
"(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
by (simp add: Cauchy_def)