New theorems; stronger theorems; tidier theorems. Also some renaming
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Sat Jun 17 20:24:22 2017 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Mon Jun 19 16:07:47 2017 +0100
@@ -1518,7 +1518,7 @@
lemma has_contour_integral_diff:
"\<lbrakk>(f1 has_contour_integral i1) g; (f2 has_contour_integral i2) g\<rbrakk>
\<Longrightarrow> ((\<lambda>x. f1 x - f2 x) has_contour_integral (i1 - i2)) g"
- by (simp add: has_integral_sub has_contour_integral_def algebra_simps)
+ by (simp add: has_integral_diff has_contour_integral_def algebra_simps)
lemma has_contour_integral_lmul:
"(f has_contour_integral i) g \<Longrightarrow> ((\<lambda>x. c * (f x)) has_contour_integral (c*i)) g"
@@ -2486,7 +2486,7 @@
_ 0 1 ])
using ynz \<open>0 < B\<close> \<open>0 < C\<close>
apply (simp_all del: le_divide_eq_numeral1)
- apply (simp add: has_integral_sub has_contour_integral_linepath [symmetric] has_contour_integral_integral
+ apply (simp add: has_integral_diff has_contour_integral_linepath [symmetric] has_contour_integral_integral
fpi_uv f_uv contour_integrable_continuous_linepath, clarify)
apply (simp only: **)
apply (simp add: norm_triangle_le norm_mult cmod_diff_le del: le_divide_eq_numeral1)
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Sat Jun 17 20:24:22 2017 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Mon Jun 19 16:07:47 2017 +0100
@@ -385,7 +385,7 @@
moreover have "((\<lambda>x. if x \<in> A \<inter> box a b then 1 else 0) has_integral ?M A) (box a b)"
by (subst has_integral_restrict) (auto intro: compl)
ultimately have "((\<lambda>x. 1 - (if x \<in> A \<inter> box a b then 1 else 0)) has_integral ?M (box a b) - ?M A) (box a b)"
- by (rule has_integral_sub)
+ by (rule has_integral_diff)
then have "((\<lambda>x. (if x \<in> (UNIV - A) \<inter> box a b then 1 else 0)) has_integral ?M (box a b) - ?M A) (box a b)"
by (rule has_integral_cong[THEN iffD1, rotated 1]) auto
then have "((\<lambda>x. 1) has_integral ?M (box a b) - ?M A) ((UNIV - A) \<inter> box a b)"
@@ -633,7 +633,7 @@
proof
assume int: "(\<lambda>x. 1::real) integrable_on A"
then have "(indicator A::'a \<Rightarrow> real) integrable_on UNIV"
- unfolding indicator_def[abs_def] integrable_restrict_univ .
+ unfolding indicator_def[abs_def] integrable_restrict_UNIV .
then obtain r where "((indicator A::'a\<Rightarrow>real) has_integral r) UNIV"
by auto
from nn_integral_has_integral_lborel[OF _ _ this] emeasure_A show False
@@ -665,7 +665,7 @@
unfolding ennreal_max_0 by auto
then have "((\<lambda>x. max 0 (f x)) has_integral r) UNIV" "((\<lambda>x. max 0 (- f x)) has_integral q) UNIV"
using nn_integral_has_integral[OF _ _ r] nn_integral_has_integral[OF _ _ q] by auto
- note has_integral_sub[OF this]
+ note has_integral_diff[OF this]
moreover have "(\<lambda>x. max 0 (f x) - max 0 (- f x)) = f"
by auto
ultimately show ?thesis
@@ -696,7 +696,7 @@
ultimately have "(?F has_integral 0) UNIV"
using has_integral_integral_real[of ?F] by simp
then show "(indicator N has_integral (0::real)) (cbox a b)"
- unfolding has_integral_restrict_univ .
+ unfolding has_integral_restrict_UNIV .
qed
qed
qed
@@ -874,7 +874,7 @@
have "(?f has_integral LINT x : S | lborel. f x) UNIV"
by (rule has_integral_integral_lborel) fact
hence 1: "(f has_integral (set_lebesgue_integral lborel S f)) S"
- apply (subst has_integral_restrict_univ [symmetric])
+ apply (subst has_integral_restrict_UNIV [symmetric])
apply (rule has_integral_eq)
by auto
thus "f integrable_on S"
@@ -890,7 +890,7 @@
assumes f: "set_integrable lebesgue S f"
shows "(f has_integral (LINT x:S|lebesgue. f x)) S"
using has_integral_integral_lebesgue[OF f]
- by (simp_all add: indicator_def if_distrib[of "\<lambda>x. x *\<^sub>R f _"] has_integral_restrict_univ cong: if_cong)
+ by (simp_all add: indicator_def if_distrib[of "\<lambda>x. x *\<^sub>R f _"] has_integral_restrict_UNIV cong: if_cong)
lemma set_lebesgue_integral_eq_integral:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -921,7 +921,7 @@
"(\<lambda>x. norm (indicator s x *\<^sub>R f x)) = (\<lambda>x. if x \<in> s then norm (f x) else 0)"
by auto
ultimately show "f integrable_on s" "(\<lambda>x. norm (f x)) integrable_on s"
- by (simp_all add: integrable_restrict_univ)
+ by (simp_all add: integrable_restrict_UNIV)
next
assume f: "f integrable_on s" and nf: "(\<lambda>x. norm (f x)) integrable_on s"
show "f absolutely_integrable_on s"
@@ -934,21 +934,38 @@
qed
qed
-lemma absolutely_integrable_on_iff_nonneg:
- fixes f :: "'a :: euclidean_space \<Rightarrow> real"
- assumes "\<And>x. 0 \<le> f x" shows "f absolutely_integrable_on s \<longleftrightarrow> f integrable_on s"
-proof -
- from assms have "(\<lambda>x. \<bar>f x\<bar>) = f"
- by (intro ext) auto
- then show ?thesis
- unfolding absolutely_integrable_on_def by simp
-qed
+lemma absolutely_integrable_restrict_UNIV:
+ "(\<lambda>x. if x \<in> s then f x else 0) absolutely_integrable_on UNIV \<longleftrightarrow> f absolutely_integrable_on s"
+ by (intro arg_cong2[where f=integrable]) auto
lemma absolutely_integrable_onI:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
shows "f integrable_on s \<Longrightarrow> (\<lambda>x. norm (f x)) integrable_on s \<Longrightarrow> f absolutely_integrable_on s"
unfolding absolutely_integrable_on_def by auto
+lemma nonnegative_absolutely_integrable_1:
+ fixes f :: "'a :: euclidean_space \<Rightarrow> real"
+ assumes f: "f integrable_on A" and "\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x"
+ shows "f absolutely_integrable_on A"
+ apply (rule absolutely_integrable_onI [OF f])
+ using assms by (simp add: integrable_eq)
+
+lemma absolutely_integrable_on_iff_nonneg:
+ fixes f :: "'a :: euclidean_space \<Rightarrow> real"
+ assumes "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f x" shows "f absolutely_integrable_on S \<longleftrightarrow> f integrable_on S"
+proof -
+ { assume "f integrable_on S"
+ then have "(\<lambda>x. if x \<in> S then f x else 0) integrable_on UNIV"
+ by (simp add: integrable_restrict_UNIV)
+ then have "(\<lambda>x. if x \<in> S then f x else 0) absolutely_integrable_on UNIV"
+ using \<open>f integrable_on S\<close> absolutely_integrable_restrict_UNIV assms nonnegative_absolutely_integrable_1 by blast
+ then have "f absolutely_integrable_on S"
+ using absolutely_integrable_restrict_UNIV by blast
+ }
+ then show ?thesis
+ unfolding absolutely_integrable_on_def by auto
+qed
+
lemma lmeasurable_iff_integrable_on: "S \<in> lmeasurable \<longleftrightarrow> (\<lambda>x. 1::real) integrable_on S"
by (subst absolutely_integrable_on_iff_nonneg[symmetric])
(simp_all add: lmeasurable_iff_integrable)
@@ -994,7 +1011,7 @@
show "negligible S"
unfolding negligible_def
proof (safe intro!: has_integral_iff_nn_integral_lebesgue[THEN iffD2]
- has_integral_restrict_univ[where s="cbox _ _", THEN iffD1])
+ has_integral_restrict_UNIV[where s="cbox _ _", THEN iffD1])
fix a b
show "(\<lambda>x. if x \<in> cbox a b then indicator S x else 0) \<in> lebesgue \<rightarrow>\<^sub>M borel"
using S by (auto intro!: measurable_If)
@@ -2209,16 +2226,12 @@
qed
qed
-lemma absolutely_integrable_restrict_univ:
- "(\<lambda>x. if x \<in> s then f x else 0) absolutely_integrable_on UNIV \<longleftrightarrow> f absolutely_integrable_on s"
- by (intro arg_cong2[where f=integrable]) auto
-
lemma absolutely_integrable_add[intro]:
fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
shows "f absolutely_integrable_on s \<Longrightarrow> g absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. f x + g x) absolutely_integrable_on s"
by (rule set_integral_add)
-lemma absolutely_integrable_sub[intro]:
+lemma absolutely_integrable_diff[intro]:
fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
shows "f absolutely_integrable_on s \<Longrightarrow> g absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. f x - g x) absolutely_integrable_on s"
by (rule set_integral_diff)
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Sat Jun 17 20:24:22 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Mon Jun 19 16:07:47 2017 +0100
@@ -188,6 +188,12 @@
lemma property_empty_interval: "\<forall>a b. content (cbox a b) = 0 \<longrightarrow> P (cbox a b) \<Longrightarrow> P {}"
using content_empty unfolding empty_as_interval by auto
+lemma interval_bounds_nz_content [simp]:
+ assumes "content (cbox a b) \<noteq> 0"
+ shows "interval_upperbound (cbox a b) = b"
+ and "interval_lowerbound (cbox a b) = a"
+ by (metis assms content_empty interval_bounds')+
+
subsection \<open>Gauge integral\<close>
text \<open>Case distinction to define it first on compact intervals first, then use a limit. This is only
@@ -569,7 +575,7 @@
qed
qed
-lemma has_integral_sub:
+lemma has_integral_diff:
"(f has_integral k) s \<Longrightarrow> (g has_integral l) s \<Longrightarrow>
((\<lambda>x. f x - g x) has_integral (k - l)) s"
using has_integral_add[OF _ has_integral_neg, of f k s g l]
@@ -606,7 +612,7 @@
lemma integral_diff: "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow>
integral s (\<lambda>x. f x - g x) = integral s f - integral s g"
- by (rule integral_unique) (metis integrable_integral has_integral_sub)
+ by (rule integral_unique) (metis integrable_integral has_integral_diff)
lemma integrable_0: "(\<lambda>x. 0) integrable_on s"
unfolding integrable_on_def using has_integral_0 by auto
@@ -635,7 +641,7 @@
lemma integrable_diff:
"f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow> (\<lambda>x. f x - g x) integrable_on s"
- unfolding integrable_on_def by(auto intro: has_integral_sub)
+ unfolding integrable_on_def by(auto intro: has_integral_diff)
lemma integrable_linear:
"f integrable_on s \<Longrightarrow> bounded_linear h \<Longrightarrow> (h \<circ> f) integrable_on s"
@@ -680,7 +686,7 @@
assumes "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
and "(f has_integral k) s"
shows "(g has_integral k) s"
- using has_integral_sub[OF assms(2), of "\<lambda>x. f x - g x" 0]
+ using has_integral_diff[OF assms(2), of "\<lambda>x. f x - g x" 0]
using has_integral_is_0[of s "\<lambda>x. f x - g x"]
using assms(1)
by auto
@@ -774,22 +780,10 @@
shows "(f has_integral 0) (cbox a a)"
and "(f has_integral 0) {a}"
proof -
- have *: "{a} = cbox a a"
- apply (rule set_eqI)
- unfolding mem_box singleton_iff euclidean_eq_iff[where 'a='a]
- apply safe
- prefer 3
- apply (erule_tac x=b in ballE)
- apply (auto simp add: field_simps)
- done
- show "(f has_integral 0) (cbox a a)" "(f has_integral 0) {a}"
- unfolding *
- apply (rule_tac[!] has_integral_null)
- unfolding content_eq_0_interior
- unfolding interior_cbox
- using box_sing
- apply auto
- done
+ show "(f has_integral 0) (cbox a a)"
+ by (rule has_integral_null) simp
+ then show "(f has_integral 0) {a}"
+ by simp
qed
lemma integrable_on_refl[intro]: "f integrable_on cbox a a"
@@ -994,7 +988,7 @@
unfolding k1 interval_split[OF \<open>k \<in> Basis\<close>]
unfolding content_eq_0_interior
unfolding interval_split[OF \<open>k \<in> Basis\<close>, symmetric] k1[symmetric]
- by (rule tagged_division_split_left_inj[OF assms])
+ by (metis tagged_division_split_left_inj assms)
qed
lemma tagged_division_split_right_inj_content:
@@ -1008,7 +1002,7 @@
unfolding k1 interval_split[OF \<open>k \<in> Basis\<close>]
unfolding content_eq_0_interior
unfolding interval_split[OF \<open>k \<in> Basis\<close>, symmetric] k1[symmetric]
- by (rule tagged_division_split_right_inj[OF assms])
+ by (metis tagged_division_split_right_inj assms)
qed
lemma has_integral_split:
@@ -3149,7 +3143,7 @@
then have Idiff: "?I a y - ?I a x = ?I x y"
using False x by (simp add: algebra_simps integral_combine)
have fux_int: "((\<lambda>u. f u - f x) has_integral integral {x..y} f - (y - x) *\<^sub>R f x) {x..y}"
- apply (rule has_integral_sub)
+ apply (rule has_integral_diff)
using x y apply (force intro: integrable_integral [OF integrable_subinterval_real [OF f]])
using has_integral_const_real [of "f x" x y] False
apply (simp add: )
@@ -3167,7 +3161,7 @@
then have Idiff: "?I a x - ?I a y = ?I y x"
using True x y by (simp add: algebra_simps integral_combine)
have fux_int: "((\<lambda>u. f u - f x) has_integral integral {y..x} f - (x - y) *\<^sub>R f x) {y..x}"
- apply (rule has_integral_sub)
+ apply (rule has_integral_diff)
using x y apply (force intro: integrable_integral [OF integrable_subinterval_real [OF f]])
using has_integral_const_real [of "f x" y x] True
apply (simp add: )
@@ -5069,7 +5063,7 @@
done
qed
-lemma has_integral_restrict_univ:
+lemma has_integral_restrict_UNIV:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
shows "((\<lambda>x. if x \<in> s then f x else 0) has_integral i) UNIV \<longleftrightarrow> (f has_integral i) s"
by auto
@@ -5088,8 +5082,8 @@
done
then show ?thesis
using assms(3)
- apply (subst has_integral_restrict_univ[symmetric])
- apply (subst(asm) has_integral_restrict_univ[symmetric])
+ apply (subst has_integral_restrict_UNIV[symmetric])
+ apply (subst(asm) has_integral_restrict_UNIV[symmetric])
apply auto
done
qed
@@ -5108,11 +5102,11 @@
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
shows "f integrable_on s \<Longrightarrow> integral UNIV (\<lambda>x. if x \<in> s then f x else 0) = integral s f"
apply (rule integral_unique)
- unfolding has_integral_restrict_univ
+ unfolding has_integral_restrict_UNIV
apply auto
done
-lemma integrable_restrict_univ:
+lemma integrable_restrict_UNIV:
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
shows "(\<lambda>x. if x \<in> s then f x else 0) integrable_on UNIV \<longleftrightarrow> f integrable_on s"
unfolding integrable_on_def
@@ -5164,7 +5158,7 @@
fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
assumes "negligible ((s - t) \<union> (t - s))"
shows "(f has_integral y) s \<longleftrightarrow> (f has_integral y) t"
- unfolding has_integral_restrict_univ[symmetric,of f]
+ unfolding has_integral_restrict_UNIV[symmetric,of f]
apply (rule has_integral_spike_eq[OF assms])
by (auto split: if_split_asm)
@@ -5195,7 +5189,7 @@
and as: "s \<subseteq> t" "(f has_integral i) s" "(f has_integral j) t" "\<forall>x\<in>t. 0 \<le> f(x)\<bullet>k"
shows "i\<bullet>k \<le> j\<bullet>k"
proof -
- note has_integral_restrict_univ[symmetric, of f]
+ note has_integral_restrict_UNIV[symmetric, of f]
note as(2-3)[unfolded this] note * = has_integral_component_le[OF k this]
show ?thesis
apply (rule *)
@@ -5667,7 +5661,7 @@
and "negligible (s \<inter> t)"
shows "(f has_integral (i + j)) (s \<union> t)"
proof -
- note * = has_integral_restrict_univ[symmetric, of f]
+ note * = has_integral_restrict_UNIV[symmetric, of f]
show ?thesis
unfolding *
apply (rule has_integral_spike[OF assms(3)])
@@ -5700,7 +5694,7 @@
and "\<forall>s\<in>t. \<forall>s'\<in>t. s \<noteq> s' \<longrightarrow> negligible (s \<inter> s')"
shows "(f has_integral (sum i t)) (\<Union>t)"
proof -
- note * = has_integral_restrict_univ[symmetric, of f]
+ note * = has_integral_restrict_UNIV[symmetric, of f]
have **: "negligible (\<Union>((\<lambda>(a,b). a \<inter> b) ` {(a,b). a \<in> t \<and> b \<in> {y. y \<in> t \<and> a \<noteq> y}}))"
apply (rule negligible_Union)
apply (rule finite_imageI)
@@ -6541,9 +6535,9 @@
(\<lambda>x. if x \<in> t \<inter> s then f k x else 0)"
by (rule ext) auto
have int': "\<And>k a b. f k integrable_on cbox a b \<inter> s"
- apply (subst integrable_restrict_univ[symmetric])
+ apply (subst integrable_restrict_UNIV[symmetric])
apply (subst ifif[symmetric])
- apply (subst integrable_restrict_univ)
+ apply (subst integrable_restrict_UNIV)
apply (rule int)
done
have "\<And>a b. (\<lambda>x. if x \<in> s then g x else 0) integrable_on cbox a b \<and>
@@ -7237,7 +7231,7 @@
(prod (f b) (g b) - prod (f a) (g a))) {a..b}"
using deriv by (intro fundamental_theorem_of_calculus_interior_strong[OF s le])
(auto intro!: continuous_intros continuous_on has_vector_derivative)
- from has_integral_sub[OF this int] show ?thesis by (simp add: algebra_simps)
+ from has_integral_diff[OF this int] show ?thesis by (simp add: algebra_simps)
qed
lemma integration_by_parts_interior:
--- a/src/HOL/Analysis/Tagged_Division.thy Sat Jun 17 20:24:22 2017 +0200
+++ b/src/HOL/Analysis/Tagged_Division.thy Mon Jun 19 16:07:47 2017 +0100
@@ -1496,7 +1496,7 @@
apply (erule disjE)
apply (rule_tac x="(k,(interval_lowerbound l)\<bullet>k)" in exI, force simp add: *)
apply (rule_tac x="(k,(interval_upperbound l)\<bullet>k)" in exI, force simp add: *)
- done
+ done
moreover have "?D1 \<subseteq> ?D"
by (auto simp add: assms division_points_subset)
ultimately show "?D1 \<subset> ?D"
@@ -1521,47 +1521,33 @@
qed
lemma division_split_left_inj:
- fixes type :: "'a::euclidean_space"
- assumes "d division_of i"
- and "k1 \<in> d"
- and "k2 \<in> d"
- and "k1 \<noteq> k2"
- and "k1 \<inter> {x::'a. x\<bullet>k \<le> c} = k2 \<inter> {x. x\<bullet>k \<le> c}"
- and k: "k\<in>Basis"
- shows "interior (k1 \<inter> {x. x\<bullet>k \<le> c}) = {}"
+ fixes S :: "'a::euclidean_space set"
+ assumes div: "\<D> division_of S"
+ and eq: "K1 \<inter> {x::'a. x\<bullet>k \<le> c} = K2 \<inter> {x. x\<bullet>k \<le> c}"
+ and "K1 \<in> \<D>" "K2 \<in> \<D>" "K1 \<noteq> K2"
+ shows "interior (K1 \<inter> {x. x\<bullet>k \<le> c}) = {}"
proof -
- note d=division_ofD[OF assms(1)]
- guess u1 v1 using d(4)[OF assms(2)] by (elim exE) note uv1=this
- guess u2 v2 using d(4)[OF assms(3)] by (elim exE) note uv2=this
- have **: "\<And>s t u. s \<inter> t = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<subseteq> t \<Longrightarrow> u = {}"
- by auto
- show ?thesis
- unfolding uv1 uv2
- apply (rule **[OF d(5)[OF assms(2-4)]])
- apply (simp add: uv1)
- using assms(5) uv1 by auto
+ have "interior K2 \<inter> interior {a. a \<bullet> k \<le> c} = interior K1 \<inter> interior {a. a \<bullet> k \<le> c}"
+ by (metis (no_types) eq interior_Int)
+ moreover have "\<And>A. interior A \<inter> interior K2 = {} \<or> A = K2 \<or> A \<notin> \<D>"
+ by (meson div \<open>K2 \<in> \<D>\<close> division_of_def)
+ ultimately show ?thesis
+ using \<open>K1 \<in> \<D>\<close> \<open>K1 \<noteq> K2\<close> by auto
qed
lemma division_split_right_inj:
- fixes type :: "'a::euclidean_space"
- assumes "d division_of i"
- and "k1 \<in> d"
- and "k2 \<in> d"
- and "k1 \<noteq> k2"
- and "k1 \<inter> {x::'a. x\<bullet>k \<ge> c} = k2 \<inter> {x. x\<bullet>k \<ge> c}"
- and k: "k \<in> Basis"
- shows "interior (k1 \<inter> {x. x\<bullet>k \<ge> c}) = {}"
+ fixes S :: "'a::euclidean_space set"
+ assumes div: "\<D> division_of S"
+ and eq: "K1 \<inter> {x::'a. x\<bullet>k \<ge> c} = K2 \<inter> {x. x\<bullet>k \<ge> c}"
+ and "K1 \<in> \<D>" "K2 \<in> \<D>" "K1 \<noteq> K2"
+ shows "interior (K1 \<inter> {x. x\<bullet>k \<ge> c}) = {}"
proof -
- note d=division_ofD[OF assms(1)]
- guess u1 v1 using d(4)[OF assms(2)] by (elim exE) note uv1=this
- guess u2 v2 using d(4)[OF assms(3)] by (elim exE) note uv2=this
- have **: "\<And>s t u. s \<inter> t = {} \<Longrightarrow> u \<subseteq> s \<Longrightarrow> u \<subseteq> t \<Longrightarrow> u = {}"
- by auto
- show ?thesis
- unfolding uv1 uv2
- apply (rule **[OF d(5)[OF assms(2-4)]])
- apply (simp add: uv1)
- using assms(5) uv1 by auto
+ have "interior K2 \<inter> interior {a. a \<bullet> k \<ge> c} = interior K1 \<inter> interior {a. a \<bullet> k \<ge> c}"
+ by (metis (no_types) eq interior_Int)
+ moreover have "\<And>A. interior A \<inter> interior K2 = {} \<or> A = K2 \<or> A \<notin> \<D>"
+ by (meson div \<open>K2 \<in> \<D>\<close> division_of_def)
+ ultimately show ?thesis
+ using \<open>K1 \<in> \<D>\<close> \<open>K1 \<noteq> K2\<close> by auto
qed
lemma interval_doublesplit:
@@ -1912,18 +1898,30 @@
by (rule tagged_division_union_interval)
lemma tagged_division_split_left_inj:
- "d tagged_division_of i \<Longrightarrow> (x1, k1) \<in> d \<Longrightarrow> (x2, k2) \<in> d \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow>
- k1 \<inter> {x. x\<bullet>k \<le> c} = k2 \<inter> {x. x\<bullet>k \<le> c} \<Longrightarrow> k \<in> Basis \<Longrightarrow>
- interior (k1 \<inter> {x. x\<bullet>k \<le> c}) = {}"
- by (intro division_split_left_inj[of "snd`d" i k1 k2, OF division_of_tagged_division])
- (auto simp add: snd_def[abs_def] image_iff split: prod.split )
+ assumes d: "d tagged_division_of i"
+ and "k1 \<noteq> k2"
+ and tags: "(x1, k1) \<in> d" "(x2, k2) \<in> d"
+ and eq: "k1 \<inter> {x. x \<bullet> k \<le> c} = k2 \<inter> {x. x \<bullet> k \<le> c}"
+ shows "interior (k1 \<inter> {x. x\<bullet>k \<le> c}) = {}"
+proof -
+ have "interior (k1 \<inter> k2) = {} \<or> (x2, k2) = (x1, k1)"
+ using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
+ then show ?thesis
+ using eq \<open>k1 \<noteq> k2\<close> by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
+qed
lemma tagged_division_split_right_inj:
- "d tagged_division_of i \<Longrightarrow> (x1, k1) \<in> d \<Longrightarrow> (x2, k2) \<in> d \<Longrightarrow> k1 \<noteq> k2 \<Longrightarrow>
- k1 \<inter> {x. x\<bullet>k \<ge> c} = k2 \<inter> {x. x\<bullet>k \<ge> c} \<Longrightarrow> k \<in> Basis \<Longrightarrow>
- interior (k1 \<inter> {x. x\<bullet>k \<ge> c}) = {}"
- by (intro division_split_right_inj[of "snd`d" i k1 k2, OF division_of_tagged_division])
- (auto simp add: snd_def[abs_def] image_iff split: prod.split )
+ assumes d: "d tagged_division_of i"
+ and "k1 \<noteq> k2"
+ and tags: "(x1, k1) \<in> d" "(x2, k2) \<in> d"
+ and eq: "k1 \<inter> {x. x\<bullet>k \<ge> c} = k2 \<inter> {x. x\<bullet>k \<ge> c}"
+ shows "interior (k1 \<inter> {x. x\<bullet>k \<ge> c}) = {}"
+proof -
+ have "interior (k1 \<inter> k2) = {} \<or> (x2, k2) = (x1, k1)"
+ using tags d by (metis (no_types) interior_Int tagged_division_ofD(5))
+ then show ?thesis
+ using eq \<open>k1 \<noteq> k2\<close> by (metis (no_types) inf_assoc inf_bot_left inf_left_idem interior_Int old.prod.inject)
+qed
subsection \<open>Special case of additivity we need for the FTC.\<close>
@@ -1934,22 +1932,21 @@
shows "sum (\<lambda>(x,k). f(Sup k) - f(Inf k)) p = f b - f a"
proof -
let ?f = "(\<lambda>k::(real) set. if k = {} then 0 else f(interval_upperbound k) - f(interval_lowerbound k))"
- have ***: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
- using assms by auto
+ have p_td: "p tagged_division_of cbox a b"
+ using assms(2) box_real(2) by presburger
have *: "add.operative ?f"
- unfolding add.operative_1_lt box_eq_empty
- by auto
+ unfolding add.operative_1_lt box_eq_empty by auto
have **: "cbox a b \<noteq> {}"
using assms(1) by auto
- note sum.operative_tagged_division[OF * assms(2)[simplified box_real[symmetric]]]
- note * = this[unfolded if_not_P[OF **] interval_bounds[OF ***],symmetric]
- show ?thesis
- unfolding *
- apply (rule sum.cong)
- unfolding split_paired_all split_conv
- using assms(2)
- apply auto
- done
+ then have "f b - f a = (\<Sum>(x, l)\<in>p. if l = {} then 0 else f (interval_upperbound l) - f (interval_lowerbound l))"
+ proof -
+ have "(if cbox a b = {} then 0 else f (interval_upperbound (cbox a b)) - f (interval_lowerbound (cbox a b))) = f b - f a"
+ using assms by auto
+ then show ?thesis
+ using p_td assms by (simp add: "*" sum.operative_tagged_division)
+ qed
+ then show ?thesis
+ using assms by (auto intro!: sum.cong)
qed
lemma bgauge_existence_lemma: "(\<forall>x\<in>s. \<exists>d::real. 0 < d \<and> q d x) \<longleftrightarrow> (\<forall>x. \<exists>d>0. x\<in>s \<longrightarrow> q d x)"
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Sat Jun 17 20:24:22 2017 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Mon Jun 19 16:07:47 2017 +0100
@@ -1438,8 +1438,8 @@
lemma
fixes a :: "'a::euclidean_space"
- shows cbox_sing: "cbox a a = {a}"
- and box_sing: "box a a = {}"
+ shows cbox_sing [simp]: "cbox a a = {a}"
+ and box_sing [simp]: "box a a = {}"
unfolding set_eq_iff mem_box eq_iff [symmetric]
by (auto intro!: euclidean_eqI[where 'a='a])
(metis all_not_in_conv nonempty_Basis)
--- a/src/HOL/Groups_Big.thy Sat Jun 17 20:24:22 2017 +0200
+++ b/src/HOL/Groups_Big.thy Mon Jun 19 16:07:47 2017 +0100
@@ -643,8 +643,8 @@
lemma member_le_sum:
fixes f :: "_ \<Rightarrow> 'b::{semiring_1, ordered_comm_monoid_add}"
- assumes le: "\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x"
- and "i \<in> A"
+ assumes "i \<in> A"
+ and le: "\<And>x. x \<in> A - {i} \<Longrightarrow> 0 \<le> f x"
and "finite A"
shows "f i \<le> sum f A"
proof -