--- a/src/HOL/Analysis/Bochner_Integration.thy Fri Apr 27 12:38:30 2018 +0100
+++ b/src/HOL/Analysis/Bochner_Integration.thy Fri Apr 27 12:43:05 2018 +0100
@@ -474,8 +474,8 @@
by (subst simple_bochner_integral_partition[OF f(1), where g="\<lambda>x. ennreal (f x)" and v=enn2real])
(auto intro: f simple_function_compose1 elim: simple_bochner_integrable.cases
intro!: sum.cong ennreal_cong_mult
- simp: sum_ennreal[symmetric] ac_simps ennreal_mult
- simp del: sum_ennreal)
+ simp: ac_simps ennreal_mult
+ reorient: sum_ennreal)
also have "\<dots> = (\<integral>\<^sup>+x. f x \<partial>M)"
using f
by (intro nn_integral_eq_simple_integral[symmetric])
@@ -503,7 +503,7 @@
using simple_bochner_integrable_compose2[of "\<lambda>x y. norm (x - y)" M "s" "t"] s t
by (auto intro!: simple_bochner_integral_eq_nn_integral)
also have "\<dots> \<le> (\<integral>\<^sup>+x. ennreal (norm (f x - s x)) + ennreal (norm (f x - t x)) \<partial>M)"
- by (auto intro!: nn_integral_mono simp: ennreal_plus[symmetric] simp del: ennreal_plus)
+ by (auto intro!: nn_integral_mono reorient: ennreal_plus)
(metis (erased, hide_lams) add_diff_cancel_left add_diff_eq diff_add_eq order_trans
norm_minus_commute norm_triangle_ineq4 order_refl)
also have "\<dots> = ?S + ?T"
@@ -593,7 +593,7 @@
proof (intro always_eventually allI)
fix i have "?f i \<le> (\<integral>\<^sup>+ x. (norm (f x - sf i x)) + ennreal (norm (g x - sg i x)) \<partial>M)"
by (auto intro!: nn_integral_mono norm_diff_triangle_ineq
- simp del: ennreal_plus simp add: ennreal_plus[symmetric])
+ reorient: ennreal_plus)
also have "\<dots> = ?g i"
by (intro nn_integral_add) auto
finally show "?f i \<le> ?g i" .
@@ -746,7 +746,7 @@
finally have s_fin: "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) < \<infinity>" .
have "(\<integral>\<^sup>+ x. norm (f x) \<partial>M) \<le> (\<integral>\<^sup>+ x. ennreal (norm (f x - s i x)) + ennreal (norm (s i x)) \<partial>M)"
- by (auto intro!: nn_integral_mono simp del: ennreal_plus simp add: ennreal_plus[symmetric])
+ by (auto intro!: nn_integral_mono reorient: ennreal_plus)
(metis add.commute norm_triangle_sub)
also have "\<dots> = (\<integral>\<^sup>+x. norm (f x - s i x) \<partial>M) + (\<integral>\<^sup>+x. norm (s i x) \<partial>M)"
by (rule nn_integral_add) auto
@@ -782,7 +782,7 @@
by (intro simple_bochner_integral_eq_nn_integral)
(auto intro: s simple_bochner_integrable_compose2)
also have "\<dots> \<le> (\<integral>\<^sup>+x. ennreal (norm (f x - s n x)) + norm (f x) \<partial>M)"
- by (auto intro!: nn_integral_mono simp del: ennreal_plus simp add: ennreal_plus[symmetric])
+ by (auto intro!: nn_integral_mono reorient: ennreal_plus)
(metis add.commute norm_minus_commute norm_triangle_sub)
also have "\<dots> = ?t n"
by (rule nn_integral_add) auto
@@ -827,7 +827,7 @@
using tendsto_add[OF \<open>?S \<longlonglongrightarrow> 0\<close> \<open>?T \<longlonglongrightarrow> 0\<close>] by simp
qed
then have "(\<lambda>i. norm (?s i - ?t i)) \<longlonglongrightarrow> 0"
- by (simp add: ennreal_0[symmetric] del: ennreal_0)
+ by (simp reorient: ennreal_0)
ultimately have "norm (x - y) = 0"
by (rule LIMSEQ_unique)
then show "x = y" by simp
@@ -1173,7 +1173,7 @@
by (intro simple_bochner_integral_bounded s f)
also have "\<dots> < ennreal (e / 2) + e / 2"
by (intro add_strict_mono M n m)
- also have "\<dots> = e" using \<open>0<e\<close> by (simp del: ennreal_plus add: ennreal_plus[symmetric])
+ also have "\<dots> = e" using \<open>0<e\<close> by (simp reorient: ennreal_plus)
finally show "dist (?s n) (?s m) < e"
using \<open>0<e\<close> by (simp add: dist_norm ennreal_less_iff)
qed
@@ -1218,7 +1218,7 @@
fix x assume "(\<lambda>i. u i x) \<longlonglongrightarrow> u' x"
from tendsto_diff[OF tendsto_const[of "u' x"] this]
show "(\<lambda>i. ennreal (norm (u' x - u i x))) \<longlonglongrightarrow> 0"
- by (simp add: tendsto_norm_zero_iff ennreal_0[symmetric] del: ennreal_0)
+ by (simp add: tendsto_norm_zero_iff reorient: ennreal_0)
qed
qed (insert bnd w_nonneg, auto)
then show ?thesis by simp
@@ -2116,7 +2116,7 @@
by auto
qed
then have "((\<lambda>n. norm((\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M))) \<longlongrightarrow> 0) F"
- by (simp add: ennreal_0[symmetric] del: ennreal_0)
+ by (simp reorient: ennreal_0)
then have "((\<lambda>n. ((\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M))) \<longlongrightarrow> 0) F" using tendsto_norm_zero_iff by blast
then show ?thesis using Lim_null by auto
qed
@@ -2214,7 +2214,7 @@
ultimately have "(\<lambda>n. ennreal (norm(u (r n) x))) \<longlonglongrightarrow> 0"
using tendsto_Limsup[of sequentially "\<lambda>n. ennreal (norm(u (r n) x))"] by auto
then have "(\<lambda>n. norm(u (r n) x)) \<longlonglongrightarrow> 0"
- by (simp add: ennreal_0[symmetric] del: ennreal_0)
+ by (simp reorient: ennreal_0)
then have "(\<lambda>n. u (r n) x) \<longlonglongrightarrow> 0"
by (simp add: tendsto_norm_zero_iff)
}
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Fri Apr 27 12:38:30 2018 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Fri Apr 27 12:43:05 2018 +0100
@@ -4130,7 +4130,7 @@
have "winding_number \<gamma> y \<in> \<int>" "winding_number \<gamma> z \<in> \<int>"
using that integer_winding_number [OF \<gamma> loop] sg \<open>y \<in> S\<close> by auto
with ne show ?thesis
- by (auto simp: Ints_def of_int_diff [symmetric] simp del: of_int_diff)
+ by (auto simp: Ints_def reorient: of_int_diff)
qed
have cont: "continuous_on S (\<lambda>w. winding_number \<gamma> w)"
using continuous_on_winding_number [OF \<gamma>] sg
@@ -6663,7 +6663,7 @@
by (rule derivative_eq_intros | simp)+
have y_le: "\<lbrakk>cmod (z - y) * 2 < r - cmod z\<rbrakk> \<Longrightarrow> cmod y \<le> cmod (of_real r + of_real (cmod z)) / 2" for z y
using \<open>r > 0\<close>
- apply (auto simp: algebra_simps norm_mult norm_divide norm_power of_real_add [symmetric] simp del: of_real_add)
+ apply (auto simp: algebra_simps norm_mult norm_divide norm_power reorient: of_real_add)
using norm_triangle_ineq2 [of y z]
apply (simp only: diff_le_eq norm_minus_commute mult_2)
done
@@ -6671,7 +6671,7 @@
using assms \<open>r > 0\<close> by simp
moreover have "\<And>z. cmod z < r \<Longrightarrow> cmod ((of_real r + of_real (cmod z)) / 2) < cmod (of_real r)"
using \<open>r > 0\<close>
- by (simp add: of_real_add [symmetric] del: of_real_add)
+ by (simp reorient: of_real_add)
ultimately have sum: "\<And>z. cmod z < r \<Longrightarrow> summable (\<lambda>n. of_real (cmod (a n)) * ((of_real r + complex_of_real (cmod z)) / 2) ^ n)"
by (rule power_series_conv_imp_absconv_weak)
have "\<exists>g g'. \<forall>z \<in> ball 0 r. (\<lambda>n. (a n) * z ^ n) sums g z \<and>
@@ -6719,7 +6719,7 @@
then have "0 \<le> r"
by (meson less_eq_real_def norm_ge_zero order_trans)
show ?thesis
- using w by (simp add: dist_norm \<open>0\<le>r\<close> of_real_add [symmetric] del: of_real_add)
+ using w by (simp add: dist_norm \<open>0\<le>r\<close> reorient: of_real_add)
qed
have sum: "summable (\<lambda>n. a n * of_real (((cmod (z - w) + r) / 2) ^ n))"
using assms [OF inb] by (force simp add: summable_def dist_norm)
--- a/src/HOL/Analysis/Change_Of_Vars.thy Fri Apr 27 12:38:30 2018 +0100
+++ b/src/HOL/Analysis/Change_Of_Vars.thy Fri Apr 27 12:43:05 2018 +0100
@@ -1273,8 +1273,7 @@
proof (rule add_mono)
have "(\<Sum>k\<le>n. real k * e * ?\<mu> (T k)) = (\<Sum>k\<le>n. integral (T k) (\<lambda>x. k * e))"
by (simp add: lmeasure_integral [OF meas_t]
- integral_mult_right [symmetric] integral_mult_left [symmetric]
- del: integral_mult_right integral_mult_left)
+ reorient: integral_mult_right integral_mult_left)
also have "\<dots> \<le> (\<Sum>k\<le>n. integral (T k) (\<lambda>x. (abs (det (matrix (f' x))))))"
proof (rule sum_mono)
fix k
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Fri Apr 27 12:38:30 2018 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Fri Apr 27 12:43:05 2018 +0100
@@ -2579,19 +2579,18 @@
also have "\<dots> = u * v1 + v * v2"
by simp
finally have **:"1 - (u * u1 + v * u2) = u * v1 + v * v2" by auto
- have "0 \<le> u * v1 + v * v2" "0 \<le> u * v1" "0 \<le> u * v1 + v * v2" "0 \<le> v * v2"
+ let ?b = "((u * v1) / (u * v1 + v * v2)) *\<^sub>R b1 + ((v * v2) / (u * v1 + v * v2)) *\<^sub>R b2"
+ have zeroes: "0 \<le> u * v1 + v * v2" "0 \<le> u * v1" "0 \<le> u * v1 + v * v2" "0 \<le> v * v2"
using as(1,2) obt1(1,2) obt2(1,2) by auto
- then show ?thesis
- unfolding xeq yeq * **
- using False
- apply (rule_tac
- x = "((u * v1) / (u * v1 + v * v2)) *\<^sub>R b1 + ((v * v2) / (u * v1 + v * v2)) *\<^sub>R b2" in bexI)
- defer
- apply (rule convexD [OF convex_convex_hull])
- using obt1(4) obt2(4)
- unfolding add_divide_distrib[symmetric] and zero_le_divide_iff
- apply (auto simp: scaleR_left_distrib scaleR_right_distrib)
- done
+ show ?thesis
+ proof
+ show "u *\<^sub>R x + v *\<^sub>R y = (u * u1) *\<^sub>R a + (v * u2) *\<^sub>R a + (?b - (u * u1) *\<^sub>R ?b - (v * u2) *\<^sub>R ?b)"
+ unfolding xeq yeq * **
+ using False by (auto simp: scaleR_left_distrib scaleR_right_distrib)
+ show "?b \<in> convex hull S"
+ using False zeroes obt1(4) obt2(4)
+ by (auto simp: convexD [OF convex_convex_hull] scaleR_left_distrib scaleR_right_distrib add_divide_distrib[symmetric] zero_le_divide_iff)
+ qed
qed
then obtain b where b: "b \<in> convex hull S"
"u *\<^sub>R x + v *\<^sub>R y = (u * u1) *\<^sub>R a + (v * u2) *\<^sub>R a + (b - (u * u1) *\<^sub>R b - (v * u2) *\<^sub>R b)" ..
@@ -2629,143 +2628,80 @@
subsubsection%unimportant \<open>Explicit expression for convex hull\<close>
proposition%important convex_hull_indexed:
- fixes s :: "'a::real_vector set"
- shows "convex hull s =
- {y. \<exists>k u x.
- (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> s) \<and>
- (sum u {1..k} = 1) \<and> (sum (\<lambda>i. u i *\<^sub>R x i) {1..k} = y)}"
- (is "?xyz = ?hull")
- apply%unimportant (rule hull_unique)
- apply rule
- defer
- apply (rule convexI)
-proof -
- fix x
- assume "x\<in>s"
- then show "x \<in> ?hull"
- unfolding mem_Collect_eq
- apply (rule_tac x=1 in exI, rule_tac x="\<lambda>x. 1" in exI, auto)
- done
+ fixes S :: "'a::real_vector set"
+ shows "convex hull S =
+ {y. \<exists>k u x. (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> S) \<and>
+ (sum u {1..k} = 1) \<and> (\<Sum>i = 1..k. u i *\<^sub>R x i) = y}"
+ (is "?xyz = ?hull")
+proof (rule hull_unique [OF _ convexI])
+ show "S \<subseteq> ?hull"
+ by (clarsimp, rule_tac x=1 in exI, rule_tac x="\<lambda>x. 1" in exI, auto)
next
- fix t
- assume as: "s \<subseteq> t" "convex t"
- show "?hull \<subseteq> t"
- apply rule
- unfolding mem_Collect_eq
- apply (elim exE conjE)
- proof -
- fix x k u y
- assume assm:
- "\<forall>i\<in>{1::nat..k}. 0 \<le> u i \<and> y i \<in> s"
- "sum u {1..k} = 1" "(\<Sum>i = 1..k. u i *\<^sub>R y i) = x"
- show "x\<in>t"
- unfolding assm(3) [symmetric]
- apply (rule as(2)[unfolded convex, rule_format])
- using assm(1,2) as(1) apply auto
- done
- qed
+ fix T
+ assume "S \<subseteq> T" "convex T"
+ then show "?hull \<subseteq> T"
+ by (blast intro: convex_sum)
next
fix x y u v
assume uv: "0 \<le> u" "0 \<le> v" "u + v = (1::real)"
assume xy: "x \<in> ?hull" "y \<in> ?hull"
from xy obtain k1 u1 x1 where
- x: "\<forall>i\<in>{1::nat..k1}. 0\<le>u1 i \<and> x1 i \<in> s" "sum u1 {Suc 0..k1} = 1" "(\<Sum>i = Suc 0..k1. u1 i *\<^sub>R x1 i) = x"
+ x [rule_format]: "\<forall>i\<in>{1::nat..k1}. 0\<le>u1 i \<and> x1 i \<in> S"
+ "sum u1 {Suc 0..k1} = 1" "(\<Sum>i = Suc 0..k1. u1 i *\<^sub>R x1 i) = x"
by auto
from xy obtain k2 u2 x2 where
- y: "\<forall>i\<in>{1::nat..k2}. 0\<le>u2 i \<and> x2 i \<in> s" "sum u2 {Suc 0..k2} = 1" "(\<Sum>i = Suc 0..k2. u2 i *\<^sub>R x2 i) = y"
+ y [rule_format]: "\<forall>i\<in>{1::nat..k2}. 0\<le>u2 i \<and> x2 i \<in> S"
+ "sum u2 {Suc 0..k2} = 1" "(\<Sum>i = Suc 0..k2. u2 i *\<^sub>R x2 i) = y"
by auto
- have *: "\<And>P (x1::'a) x2 s1 s2 i.
- (if P i then s1 else s2) *\<^sub>R (if P i then x1 else x2) = (if P i then s1 *\<^sub>R x1 else s2 *\<^sub>R x2)"
- "{1..k1 + k2} \<inter> {1..k1} = {1..k1}" "{1..k1 + k2} \<inter> - {1..k1} = (\<lambda>i. i + k1) ` {1..k2}"
- prefer 3
- apply (rule, rule)
- unfolding image_iff
- apply (rule_tac x = "x - k1" in bexI)
- apply (auto simp: not_le)
- done
+ have *: "\<And>P (x::'a) y s t i. (if P i then s else t) *\<^sub>R (if P i then x else y) = (if P i then s *\<^sub>R x else t *\<^sub>R y)"
+ "{1..k1 + k2} \<inter> {1..k1} = {1..k1}" "{1..k1 + k2} \<inter> - {1..k1} = (\<lambda>i. i + k1) ` {1..k2}"
+ by auto
have inj: "inj_on (\<lambda>i. i + k1) {1..k2}"
unfolding inj_on_def by auto
+ let ?uu = "\<lambda>i. if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)"
+ let ?xx = "\<lambda>i. if i \<in> {1..k1} then x1 i else x2 (i - k1)"
show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull"
- apply rule
- apply (rule_tac x="k1 + k2" in exI)
- apply (rule_tac x="\<lambda>i. if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)" in exI)
- apply (rule_tac x="\<lambda>i. if i \<in> {1..k1} then x1 i else x2 (i - k1)" in exI)
- apply (rule, rule)
- defer
- apply rule
- unfolding * and sum.If_cases[OF finite_atLeastAtMost[of 1 "k1 + k2"]] and
- sum.reindex[OF inj] and o_def Collect_mem_eq
- unfolding scaleR_scaleR[symmetric] scaleR_right.sum [symmetric] sum_distrib_left[symmetric]
- proof -
- fix i
- assume i: "i \<in> {1..k1+k2}"
- show "0 \<le> (if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)) \<and>
- (if i \<in> {1..k1} then x1 i else x2 (i - k1)) \<in> s"
- proof (cases "i\<in>{1..k1}")
- case True
- then show ?thesis
- using uv(1) x(1)[THEN bspec[where x=i]] by auto
- next
- case False
- define j where "j = i - k1"
- from i False have "j \<in> {1..k2}"
- unfolding j_def by auto
- then show ?thesis
- using False uv(2) y(1)[THEN bspec[where x=j]]
- by (auto simp: j_def[symmetric])
- qed
- qed (auto simp: not_le x(2,3) y(2,3) uv(3))
+ proof (intro CollectI exI conjI ballI)
+ show "0 \<le> ?uu i" "?xx i \<in> S" if "i \<in> {1..k1+k2}" for i
+ using that by (auto simp add: le_diff_conv uv(1) x(1) uv(2) y(1))
+ show "(\<Sum>i = 1..k1 + k2. ?uu i) = 1" "(\<Sum>i = 1..k1 + k2. ?uu i *\<^sub>R ?xx i) = u *\<^sub>R x + v *\<^sub>R y"
+ unfolding * sum.If_cases[OF finite_atLeastAtMost[of 1 "k1 + k2"]]
+ sum.reindex[OF inj] Collect_mem_eq o_def
+ unfolding scaleR_scaleR[symmetric] scaleR_right.sum [symmetric] sum_distrib_left[symmetric]
+ by (simp_all add: sum_distrib_left[symmetric] x(2,3) y(2,3) uv(3))
+ qed
qed
lemma convex_hull_finite:
- fixes s :: "'a::real_vector set"
- assumes "finite s"
- shows "convex hull s = {y. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and>
- sum u s = 1 \<and> sum (\<lambda>x. u x *\<^sub>R x) s = y}"
- (is "?HULL = ?set")
-proof (rule hull_unique, auto simp: convex_def[of ?set])
+ fixes S :: "'a::real_vector set"
+ assumes "finite S"
+ shows "convex hull S = {y. \<exists>u. (\<forall>x\<in>S. 0 \<le> u x) \<and> sum u S = 1 \<and> sum (\<lambda>x. u x *\<^sub>R x) S = y}"
+ (is "?HULL = _")
+proof (rule hull_unique [OF _ convexI]; clarify)
fix x
- assume "x \<in> s"
- then show "\<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> sum u s = 1 \<and> (\<Sum>x\<in>s. u x *\<^sub>R x) = x"
- apply (rule_tac x="\<lambda>y. if x=y then 1 else 0" in exI, auto)
- unfolding sum.delta'[OF assms] and sum_delta''[OF assms]
- apply auto
- done
+ assume "x \<in> S"
+ then show "\<exists>u. (\<forall>x\<in>S. 0 \<le> u x) \<and> sum u S = 1 \<and> (\<Sum>x\<in>S. u x *\<^sub>R x) = x"
+ by (rule_tac x="\<lambda>y. if x=y then 1 else 0" in exI) (auto simp: sum.delta'[OF assms] sum_delta''[OF assms])
next
fix u v :: real
assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
- fix ux assume ux: "\<forall>x\<in>s. 0 \<le> ux x" "sum ux s = (1::real)"
- fix uy assume uy: "\<forall>x\<in>s. 0 \<le> uy x" "sum uy s = (1::real)"
- {
- fix x
- assume "x\<in>s"
- then have "0 \<le> u * ux x + v * uy x"
- using ux(1)[THEN bspec[where x=x]] uy(1)[THEN bspec[where x=x]] and uv(1,2)
- by auto
- }
+ fix ux assume ux [rule_format]: "\<forall>x\<in>S. 0 \<le> ux x" "sum ux S = (1::real)"
+ fix uy assume uy [rule_format]: "\<forall>x\<in>S. 0 \<le> uy x" "sum uy S = (1::real)"
+ have "0 \<le> u * ux x + v * uy x" if "x\<in>S" for x
+ by (simp add: that uv ux(1) uy(1))
moreover
- have "(\<Sum>x\<in>s. u * ux x + v * uy x) = 1"
- unfolding sum.distrib and sum_distrib_left[symmetric] and ux(2) uy(2)
+ have "(\<Sum>x\<in>S. u * ux x + v * uy x) = 1"
+ unfolding sum.distrib and sum_distrib_left[symmetric] ux(2) uy(2)
using uv(3) by auto
moreover
- have "(\<Sum>x\<in>s. (u * ux x + v * uy x) *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>s. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>s. uy x *\<^sub>R x)"
- unfolding scaleR_left_distrib and sum.distrib and scaleR_scaleR[symmetric]
- and scaleR_right.sum [symmetric]
+ have "(\<Sum>x\<in>S. (u * ux x + v * uy x) *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>S. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>S. uy x *\<^sub>R x)"
+ unfolding scaleR_left_distrib sum.distrib scaleR_scaleR[symmetric] scaleR_right.sum [symmetric]
by auto
ultimately
- show "\<exists>uc. (\<forall>x\<in>s. 0 \<le> uc x) \<and> sum uc s = 1 \<and>
- (\<Sum>x\<in>s. uc x *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>s. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>s. uy x *\<^sub>R x)"
- apply (rule_tac x="\<lambda>x. u * ux x + v * uy x" in exI, auto)
- done
-next
- fix t
- assume t: "s \<subseteq> t" "convex t"
- fix u
- assume u: "\<forall>x\<in>s. 0 \<le> u x" "sum u s = (1::real)"
- then show "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> t"
- using t(2)[unfolded convex_explicit, THEN spec[where x=s], THEN spec[where x=u]]
- using assms and t(1) by auto
-qed
+ show "\<exists>uc. (\<forall>x\<in>S. 0 \<le> uc x) \<and> sum uc S = 1 \<and>
+ (\<Sum>x\<in>S. uc x *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>S. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>S. uy x *\<^sub>R x)"
+ by (rule_tac x="\<lambda>x. u * ux x + v * uy x" in exI, auto)
+qed (use assms in \<open>auto simp: convex_explicit\<close>)
subsubsection%unimportant \<open>Another formulation from Lars Schewe\<close>
@@ -2773,7 +2709,7 @@
lemma convex_hull_explicit:
fixes p :: "'a::real_vector set"
shows "convex hull p =
- {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> sum u s = 1 \<and> sum (\<lambda>v. u v *\<^sub>R v) s = y}"
+ {y. \<exists>S u. finite S \<and> S \<subseteq> p \<and> (\<forall>x\<in>S. 0 \<le> u x) \<and> sum u S = 1 \<and> sum (\<lambda>v. u v *\<^sub>R v) S = y}"
(is "?lhs = ?rhs")
proof -
{
@@ -2803,7 +2739,7 @@
using sum_image_gen[OF fin, of "\<lambda>i. u i *\<^sub>R y i" y, symmetric]
unfolding scaleR_left.sum using obt(3) by auto
ultimately
- have "\<exists>s u. finite s \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> sum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x"
+ have "\<exists>S u. finite S \<and> S \<subseteq> p \<and> (\<forall>x\<in>S. 0 \<le> u x) \<and> sum u S = 1 \<and> (\<Sum>v\<in>S. u v *\<^sub>R v) = x"
apply (rule_tac x="y ` {1..k}" in exI)
apply (rule_tac x="\<lambda>v. sum u {i\<in>{1..k}. y i = v}" in exI, auto)
done
@@ -2813,50 +2749,48 @@
{
fix y
assume "y\<in>?rhs"
- then obtain s u where
- obt: "finite s" "s \<subseteq> p" "\<forall>x\<in>s. 0 \<le> u x" "sum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = y"
+ then obtain S u where
+ obt: "finite S" "S \<subseteq> p" "\<forall>x\<in>S. 0 \<le> u x" "sum u S = 1" "(\<Sum>v\<in>S. u v *\<^sub>R v) = y"
by auto
- obtain f where f: "inj_on f {1..card s}" "f ` {1..card s} = s"
+ obtain f where f: "inj_on f {1..card S}" "f ` {1..card S} = S"
using ex_bij_betw_nat_finite_1[OF obt(1)] unfolding bij_betw_def by auto
{
fix i :: nat
- assume "i\<in>{1..card s}"
- then have "f i \<in> s"
- apply (subst f(2)[symmetric])
- apply auto
- done
+ assume "i\<in>{1..card S}"
+ then have "f i \<in> S"
+ using f(2) by blast
then have "0 \<le> u (f i)" "f i \<in> p" using obt(2,3) by auto
}
- moreover have *: "finite {1..card s}" by auto
+ moreover have *: "finite {1..card S}" by auto
{
fix y
- assume "y\<in>s"
- then obtain i where "i\<in>{1..card s}" "f i = y"
- using f using image_iff[of y f "{1..card s}"]
+ assume "y\<in>S"
+ then obtain i where "i\<in>{1..card S}" "f i = y"
+ using f using image_iff[of y f "{1..card S}"]
by auto
- then have "{x. Suc 0 \<le> x \<and> x \<le> card s \<and> f x = y} = {i}"
+ then have "{x. Suc 0 \<le> x \<and> x \<le> card S \<and> f x = y} = {i}"
apply auto
using f(1)[unfolded inj_on_def]
by (metis One_nat_def atLeastAtMost_iff)
- then have "card {x. Suc 0 \<le> x \<and> x \<le> card s \<and> f x = y} = 1" by auto
- then have "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x)) = u y"
- "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *\<^sub>R f x) = u y *\<^sub>R y"
+ then have "card {x. Suc 0 \<le> x \<and> x \<le> card S \<and> f x = y} = 1" by auto
+ then have "(\<Sum>x\<in>{x \<in> {1..card S}. f x = y}. u (f x)) = u y"
+ "(\<Sum>x\<in>{x \<in> {1..card S}. f x = y}. u (f x) *\<^sub>R f x) = u y *\<^sub>R y"
by (auto simp: sum_constant_scaleR)
}
- then have "(\<Sum>x = 1..card s. u (f x)) = 1" "(\<Sum>i = 1..card s. u (f i) *\<^sub>R f i) = y"
+ then have "(\<Sum>x = 1..card S. u (f x)) = 1" "(\<Sum>i = 1..card S. u (f i) *\<^sub>R f i) = y"
unfolding sum_image_gen[OF *(1), of "\<lambda>x. u (f x) *\<^sub>R f x" f]
and sum_image_gen[OF *(1), of "\<lambda>x. u (f x)" f]
unfolding f
- using sum.cong [of s s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *\<^sub>R f x)" "\<lambda>v. u v *\<^sub>R v"]
- using sum.cong [of s s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x))" u]
+ using sum.cong [of S S "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card S}. f x = y}. u (f x) *\<^sub>R f x)" "\<lambda>v. u v *\<^sub>R v"]
+ using sum.cong [of S S "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card S}. f x = y}. u (f x))" u]
unfolding obt(4,5)
by auto
ultimately
have "\<exists>k u x. (\<forall>i\<in>{1..k}. 0 \<le> u i \<and> x i \<in> p) \<and> sum u {1..k} = 1 \<and>
(\<Sum>i::nat = 1..k. u i *\<^sub>R x i) = y"
- apply (rule_tac x="card s" in exI)
+ apply (rule_tac x="card S" in exI)
apply (rule_tac x="u \<circ> f" in exI)
apply (rule_tac x=f in exI, fastforce)
done
@@ -2871,62 +2805,57 @@
subsubsection%unimportant \<open>A stepping theorem for that expansion\<close>
lemma convex_hull_finite_step:
- fixes s :: "'a::real_vector set"
- assumes "finite s"
+ fixes S :: "'a::real_vector set"
+ assumes "finite S"
shows
- "(\<exists>u. (\<forall>x\<in>insert a s. 0 \<le> u x) \<and> sum u (insert a s) = w \<and> sum (\<lambda>x. u x *\<^sub>R x) (insert a s) = y)
- \<longleftrightarrow> (\<exists>v\<ge>0. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> sum u s = w - v \<and> sum (\<lambda>x. u x *\<^sub>R x) s = y - v *\<^sub>R a)"
+ "(\<exists>u. (\<forall>x\<in>insert a S. 0 \<le> u x) \<and> sum u (insert a S) = w \<and> sum (\<lambda>x. u x *\<^sub>R x) (insert a S) = y)
+ \<longleftrightarrow> (\<exists>v\<ge>0. \<exists>u. (\<forall>x\<in>S. 0 \<le> u x) \<and> sum u S = w - v \<and> sum (\<lambda>x. u x *\<^sub>R x) S = y - v *\<^sub>R a)"
(is "?lhs = ?rhs")
-proof (rule, case_tac[!] "a\<in>s")
- assume "a \<in> s"
- then have *: "insert a s = s" by auto
+proof (rule, case_tac[!] "a\<in>S")
+ assume "a \<in> S"
+ then have *: "insert a S = S" by auto
assume ?lhs
then show ?rhs
- unfolding *
- apply (rule_tac x=0 in exI, auto)
- done
+ unfolding * by (rule_tac x=0 in exI, auto)
next
assume ?lhs
then obtain u where
- u: "\<forall>x\<in>insert a s. 0 \<le> u x" "sum u (insert a s) = w" "(\<Sum>x\<in>insert a s. u x *\<^sub>R x) = y"
+ u: "\<forall>x\<in>insert a S. 0 \<le> u x" "sum u (insert a S) = w" "(\<Sum>x\<in>insert a S. u x *\<^sub>R x) = y"
by auto
- assume "a \<notin> s"
+ assume "a \<notin> S"
then show ?rhs
apply (rule_tac x="u a" in exI)
using u(1)[THEN bspec[where x=a]]
apply simp
apply (rule_tac x=u in exI)
- using u[unfolded sum_clauses(2)[OF assms]] and \<open>a\<notin>s\<close>
+ using u[unfolded sum_clauses(2)[OF assms]] and \<open>a\<notin>S\<close>
apply auto
done
next
- assume "a \<in> s"
- then have *: "insert a s = s" by auto
- have fin: "finite (insert a s)" using assms by auto
+ assume "a \<in> S"
+ then have *: "insert a S = S" by auto
+ have fin: "finite (insert a S)" using assms by auto
assume ?rhs
- then obtain v u where uv: "v\<ge>0" "\<forall>x\<in>s. 0 \<le> u x" "sum u s = w - v" "(\<Sum>x\<in>s. u x *\<^sub>R x) = y - v *\<^sub>R a"
+ then obtain v u where uv: "v\<ge>0" "\<forall>x\<in>S. 0 \<le> u x" "sum u S = w - v" "(\<Sum>x\<in>S. u x *\<^sub>R x) = y - v *\<^sub>R a"
by auto
show ?lhs
apply (rule_tac x = "\<lambda>x. (if a = x then v else 0) + u x" in exI)
unfolding scaleR_left_distrib and sum.distrib and sum_delta''[OF fin] and sum.delta'[OF fin]
unfolding sum_clauses(2)[OF assms]
- using uv and uv(2)[THEN bspec[where x=a]] and \<open>a\<in>s\<close>
+ using uv and uv(2)[THEN bspec[where x=a]] and \<open>a\<in>S\<close>
apply auto
done
next
assume ?rhs
- then obtain v u where uv: "v\<ge>0" "\<forall>x\<in>s. 0 \<le> u x" "sum u s = w - v" "(\<Sum>x\<in>s. u x *\<^sub>R x) = y - v *\<^sub>R a"
+ then obtain v u where uv: "v\<ge>0" "\<forall>x\<in>S. 0 \<le> u x" "sum u S = w - v" "(\<Sum>x\<in>S. u x *\<^sub>R x) = y - v *\<^sub>R a"
by auto
- moreover assume "a \<notin> s"
+ moreover assume "a \<notin> S"
moreover
- have "(\<Sum>x\<in>s. if a = x then v else u x) = sum u s" "(\<Sum>x\<in>s. (if a = x then v else u x) *\<^sub>R x) = (\<Sum>x\<in>s. u x *\<^sub>R x)"
- using \<open>a \<notin> s\<close>
+ have "(\<Sum>x\<in>S. if a = x then v else u x) = sum u S" "(\<Sum>x\<in>S. (if a = x then v else u x) *\<^sub>R x) = (\<Sum>x\<in>S. u x *\<^sub>R x)"
+ using \<open>a \<notin> S\<close>
by (auto simp: intro!: sum.cong)
ultimately show ?lhs
- apply (rule_tac x="\<lambda>x. if a = x then v else u x" in exI)
- unfolding sum_clauses(2)[OF assms]
- apply auto
- done
+ by (rule_tac x="\<lambda>x. if a = x then v else u x" in exI) (auto simp: sum_clauses(2)[OF assms])
qed
@@ -3050,23 +2979,12 @@
apply auto
done
have "(\<Sum>x\<in>insert a t. if x = a then - (\<Sum>x\<in>t. u (x - a)) else u (x - a)) = 0"
- unfolding sum_clauses(2)[OF fin]
- using \<open>a\<notin>s\<close> \<open>t\<subseteq>s\<close>
- apply auto
- unfolding *
- apply auto
- done
+ unfolding sum_clauses(2)[OF fin] * using \<open>a\<notin>s\<close> \<open>t\<subseteq>s\<close> by auto
moreover have "\<exists>v\<in>insert a t. (if v = a then - (\<Sum>x\<in>t. u (x - a)) else u (v - a)) \<noteq> 0"
- apply (rule_tac x="v + a" in bexI)
- using obt(3,4) and \<open>0\<notin>S\<close>
- unfolding t_def
- apply auto
- done
+ using obt(3,4) \<open>0\<notin>S\<close>
+ by (rule_tac x="v + a" in bexI) (auto simp: t_def)
moreover have *: "\<And>P Q. (\<Sum>x\<in>t. (if x = a then P x else Q x) *\<^sub>R x) = (\<Sum>x\<in>t. Q x *\<^sub>R x)"
- apply (rule sum.cong)
- using \<open>a\<notin>s\<close> \<open>t\<subseteq>s\<close>
- apply auto
- done
+ using \<open>a\<notin>s\<close> \<open>t\<subseteq>s\<close> by (auto intro!: sum.cong)
have "(\<Sum>x\<in>t. u (x - a)) *\<^sub>R a = (\<Sum>v\<in>t. u (v - a) *\<^sub>R v)"
unfolding scaleR_left.sum
unfolding t_def and sum.reindex[OF inj] and o_def
@@ -3113,11 +3031,7 @@
have *: "{x - a |x. x \<in> s - {a}} = (\<lambda>x. x - a) ` (s - {a})"
by auto
have "card {x - a |x. x \<in> s - {a}} = card (s - {a})"
- unfolding *
- apply (rule card_image)
- unfolding inj_on_def
- apply auto
- done
+ unfolding * by (simp add: card_image inj_on_def)
also have "\<dots> > DIM('a)" using assms(2)
unfolding card_Diff_singleton[OF assms(1) \<open>a\<in>s\<close>] by auto
finally show ?thesis
@@ -3128,33 +3042,25 @@
qed
lemma affine_dependent_biggerset_general:
- assumes "finite (s :: 'a::euclidean_space set)"
- and "card s \<ge> dim s + 2"
- shows "affine_dependent s"
-proof -
- from assms(2) have "s \<noteq> {}" by auto
- then obtain a where "a\<in>s" by auto
- have *: "{x - a |x. x \<in> s - {a}} = (\<lambda>x. x - a) ` (s - {a})"
+ assumes "finite (S :: 'a::euclidean_space set)"
+ and "card S \<ge> dim S + 2"
+ shows "affine_dependent S"
+proof -
+ from assms(2) have "S \<noteq> {}" by auto
+ then obtain a where "a\<in>S" by auto
+ have *: "{x - a |x. x \<in> S - {a}} = (\<lambda>x. x - a) ` (S - {a})"
by auto
- have **: "card {x - a |x. x \<in> s - {a}} = card (s - {a})"
- unfolding *
- apply (rule card_image)
- unfolding inj_on_def
- apply auto
- done
- have "dim {x - a |x. x \<in> s - {a}} \<le> dim s"
- apply (rule subset_le_dim)
- unfolding subset_eq
- using \<open>a\<in>s\<close>
- apply (auto simp:span_superset span_diff)
- done
- also have "\<dots> < dim s + 1" by auto
- also have "\<dots> \<le> card (s - {a})"
+ have **: "card {x - a |x. x \<in> S - {a}} = card (S - {a})"
+ by (metis (no_types, lifting) "*" card_image diff_add_cancel inj_on_def)
+ have "dim {x - a |x. x \<in> S - {a}} \<le> dim S"
+ using \<open>a\<in>S\<close> by (auto simp: span_superset span_diff intro: subset_le_dim)
+ also have "\<dots> < dim S + 1" by auto
+ also have "\<dots> \<le> card (S - {a})"
using assms
- using card_Diff_singleton[OF assms(1) \<open>a\<in>s\<close>]
+ using card_Diff_singleton[OF assms(1) \<open>a\<in>S\<close>]
by auto
finally show ?thesis
- apply (subst insert_Diff[OF \<open>a\<in>s\<close>, symmetric])
+ apply (subst insert_Diff[OF \<open>a\<in>S\<close>, symmetric])
apply (rule dependent_imp_affine_dependent)
apply (rule dependent_biggerset_general)
unfolding **
@@ -3590,22 +3496,10 @@
by auto
let ?t = "{x::'a::euclidean_space. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0}"
have "\<exists>f. linear f \<and> f ` B = d \<and> f ` span B = ?t \<and> inj_on f (span B)"
- apply (rule basis_to_basis_subspace_isomorphism[of "span B" ?t B "d"])
- apply (rule subspace_span)
- apply (rule subspace_substandard)
- defer
- apply (rule span_inc)
- apply (rule assms)
- defer
- unfolding dim_span[of B]
- apply(rule B)
- unfolding span_substd_basis[OF d, symmetric]
- apply (rule span_inc)
- apply (rule independent_substdbasis[OF d], rule)
- apply assumption
- unfolding t[symmetric] span_substd_basis[OF d] dim_substandard[OF d]
- apply auto
- done
+ proof (intro basis_to_basis_subspace_isomorphism subspace_span subspace_substandard span_inc)
+ show "d \<subseteq> {x. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0}"
+ using d inner_not_same_Basis by blast
+ qed (auto simp: span_substd_basis independent_substdbasis dim_substandard d t B assms)
with t \<open>card B = dim B\<close> d show ?thesis by auto
qed
@@ -7081,29 +6975,17 @@
done
then have k: "\<forall>y\<in>convex hull c. f y \<le> k"
apply (rule_tac convex_on_convex_hull_bound, assumption)
- unfolding k_def
- apply (rule, rule Max_ge)
- using c(1)
- apply auto
- done
- have "d \<le> e"
- unfolding d_def
- apply (rule mult_imp_div_pos_le)
- using \<open>e > 0\<close>
- unfolding mult_le_cancel_left1
- apply (auto simp: real_of_nat_ge_one_iff Suc_le_eq DIM_positive)
- done
+ by (simp add: k_def c)
+ have "e \<le> e * real DIM('a)"
+ using e(2) real_of_nat_ge_one_iff by auto
+ then have "d \<le> e"
+ by (simp add: d_def divide_simps)
then have dsube: "cball x d \<subseteq> cball x e"
by (rule subset_cball)
have conv: "convex_on (cball x d) f"
using \<open>convex_on (convex hull c) f\<close> c2 convex_on_subset by blast
then have "\<forall>y\<in>cball x d. \<bar>f y\<bar> \<le> k + 2 * \<bar>f x\<bar>"
- apply (rule convex_bounds_lemma)
- apply (rule ballI)
- apply (rule k [rule_format])
- apply (erule rev_subsetD)
- apply (rule c2)
- done
+ by (rule convex_bounds_lemma) (use c2 k in blast)
then have "continuous_on (ball x d) f"
apply (rule_tac convex_on_bounded_continuous)
apply (rule open_ball, rule convex_on_subset[OF conv])
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Apr 27 12:38:30 2018 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Apr 27 12:43:05 2018 +0100
@@ -244,7 +244,7 @@
finally have "?\<mu> E - 2*e \<le> ?\<mu> (E - (E \<inter> \<Union>(snd`(p - s))))"
using \<open>0 < e\<close> \<open>E \<in> sets ?L\<close> tagged_division_ofD(1)[OF p(1)]
by (subst emeasure_Diff)
- (auto simp: ennreal_plus[symmetric] top_unique simp del: ennreal_plus
+ (auto simp: top_unique reorient: ennreal_plus
intro!: sets.Int sets.finite_UN ennreal_mono_minus intro: p_in_L)
also have "\<dots> \<le> ?\<mu> (\<Union>x\<in>p \<inter> s. snd x)"
proof (safe intro!: emeasure_mono subsetI)
@@ -481,7 +481,7 @@
by (simp add: nn_integral_add)
with add obtain a b where "0 \<le> a" "0 \<le> b" "(\<integral>\<^sup>+ x. h x \<partial>lborel) = ennreal a" "(\<integral>\<^sup>+ x. g x \<partial>lborel) = ennreal b" "r = a + b"
by (cases "\<integral>\<^sup>+ x. h x \<partial>lborel" "\<integral>\<^sup>+ x. g x \<partial>lborel" rule: ennreal2_cases)
- (auto simp: add_top nn_integral_add top_add ennreal_plus[symmetric] simp del: ennreal_plus)
+ (auto simp: add_top nn_integral_add top_add reorient: ennreal_plus)
with add show ?case
by (auto intro!: has_integral_add)
next
--- a/src/HOL/Analysis/FPS_Convergence.thy Fri Apr 27 12:38:30 2018 +0100
+++ b/src/HOL/Analysis/FPS_Convergence.thy Fri Apr 27 12:43:05 2018 +0100
@@ -271,7 +271,7 @@
lemma fps_conv_radius_uminus [simp]:
"fps_conv_radius (-f) = fps_conv_radius f"
using fps_conv_radius_cmult_left[of "-1" f]
- by (simp add: fps_const_neg [symmetric] del: fps_const_neg)
+ by (simp reorient: fps_const_neg)
lemma fps_conv_radius_add: "fps_conv_radius (f + g) \<ge> min (fps_conv_radius f) (fps_conv_radius g)"
unfolding fps_conv_radius_def using conv_radius_add_ge[of "fps_nth f" "fps_nth g"]
--- a/src/HOL/Analysis/Gamma_Function.thy Fri Apr 27 12:38:30 2018 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy Fri Apr 27 12:43:05 2018 +0100
@@ -1149,7 +1149,7 @@
lemma Gamma_fact: "Gamma (1 + of_nat n) = fact n"
by (simp add: pochhammer_fact pochhammer_Gamma of_nat_in_nonpos_Ints_iff
- of_nat_Suc [symmetric] del: of_nat_Suc)
+ reorient: of_nat_Suc)
lemma Gamma_numeral: "Gamma (numeral n) = fact (pred_numeral n)"
by (subst of_nat_numeral[symmetric], subst numeral_eq_Suc,
@@ -2430,7 +2430,7 @@
inverse ((- 1) ^ n * fact n :: 'a)"
by (intro tendsto_intros rGamma_zeros) simp_all
also have "inverse ((- 1) ^ n * fact n) = ?c"
- by (simp_all add: field_simps power_mult_distrib [symmetric] del: power_mult_distrib)
+ by (simp_all add: field_simps reorient: power_mult_distrib)
finally show "(\<lambda>z. inverse (rGamma z / (z + of_nat n))) \<midarrow> (- of_nat n) \<rightarrow> ?c" .
qed
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Apr 27 12:38:30 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Apr 27 12:43:05 2018 +0100
@@ -784,13 +784,13 @@
fixes f :: "_ \<Rightarrow> 'b :: real_normed_field"
assumes "f integrable_on s"
shows "(\<lambda>x. f x / of_real c) integrable_on s"
-by (simp add: integrable_on_cmult_right divide_inverse assms of_real_inverse [symmetric] del: of_real_inverse)
+by (simp add: integrable_on_cmult_right divide_inverse assms reorient: of_real_inverse)
lemma integrable_on_cdivide_iff [simp]:
fixes f :: "_ \<Rightarrow> 'b :: real_normed_field"
assumes "c \<noteq> 0"
shows "(\<lambda>x. f x / of_real c) integrable_on s \<longleftrightarrow> f integrable_on s"
-by (simp add: divide_inverse assms of_real_inverse [symmetric] del: of_real_inverse)
+by (simp add: divide_inverse assms reorient: of_real_inverse)
lemma has_integral_null [intro]: "content(cbox a b) = 0 \<Longrightarrow> (f has_integral 0) (cbox a b)"
unfolding has_integral_cbox
@@ -3431,7 +3431,7 @@
by (simp add: inner_simps field_simps)
ultimately show ?thesis using False
by (simp add: image_affinity_cbox content_cbox'
- prod.distrib[symmetric] prod_constant[symmetric] inner_diff_left del: prod_constant)
+ prod.distrib[symmetric] inner_diff_left reorient: prod_constant)
qed
qed
--- a/src/HOL/Analysis/Interval_Integral.thy Fri Apr 27 12:38:30 2018 +0100
+++ b/src/HOL/Analysis/Interval_Integral.thy Fri Apr 27 12:43:05 2018 +0100
@@ -109,8 +109,7 @@
from ereal_incseq_approx[OF this] guess X .
then show thesis
apply (intro that[of "\<lambda>i. - X i"])
- apply (auto simp add: uminus_ereal.simps[symmetric] decseq_def incseq_def
- simp del: uminus_ereal.simps)
+ apply (auto simp add: decseq_def incseq_def reorient: uminus_ereal.simps)
apply (metis ereal_minus_less_minus ereal_uminus_uminus ereal_Lim_uminus)+
done
qed
@@ -143,7 +142,7 @@
fix x i assume "l i \<le> x" "x \<le> u i"
with \<open>a < ereal (l i)\<close> \<open>ereal (u i) < b\<close>
show "a < ereal x" "ereal x < b"
- by (auto simp del: ereal_less_eq(3) simp add: ereal_less_eq(3)[symmetric])
+ by (auto reorient: ereal_less_eq(3))
qed
show thesis
by (intro that) fact+
@@ -304,8 +303,8 @@
have "LBINT x:{x. - x \<in> einterval a b}. f (- x) = LBINT x:einterval (- b) (- a). f (- x)"
unfolding interval_lebesgue_integrable_def set_lebesgue_integral_def
apply (rule Bochner_Integration.integral_cong [OF refl])
- by (auto simp: einterval_iff ereal_uminus_le_reorder ereal_uminus_less_reorder not_less uminus_ereal.simps[symmetric]
- simp del: uminus_ereal.simps
+ by (auto simp: einterval_iff ereal_uminus_le_reorder ereal_uminus_less_reorder not_less
+ reorient: uminus_ereal.simps
split: split_indicator)
then show ?case
unfolding interval_lebesgue_integral_def
@@ -676,7 +675,7 @@
fix i show "set_integrable lborel {l i .. u i} f"
using \<open>a < l i\<close> \<open>u i < b\<close> unfolding set_integrable_def
by (intro borel_integrable_compact f continuous_at_imp_continuous_on compact_Icc ballI)
- (auto simp del: ereal_less_eq simp add: ereal_less_eq(3)[symmetric])
+ (auto reorient: ereal_less_eq)
qed
have 2: "set_borel_measurable lborel (einterval a b) f"
unfolding set_borel_measurable_def
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Fri Apr 27 12:38:30 2018 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Fri Apr 27 12:43:05 2018 +0100
@@ -283,7 +283,7 @@
also have "... \<le> (\<Sum>i\<le>n. F (r i) - F (l i)) + epsilon"
using finS Sbound Sprop by (auto intro!: add_right_mono sum_mono2)
finally have "ennreal (F b - F a) \<le> (\<Sum>i\<le>n. ennreal (F (r i) - F (l i))) + epsilon"
- using egt0 by (simp add: ennreal_plus[symmetric] sum_nonneg del: ennreal_plus)
+ using egt0 by (simp add: sum_nonneg reorient: ennreal_plus)
then show "ennreal (F b - F a) \<le> (\<Sum>i. ennreal (F (r i) - F (l i))) + (epsilon :: real)"
by (rule order_trans) (auto intro!: add_mono sum_le_suminf simp del: sum_ennreal)
qed
--- a/src/HOL/Analysis/Measure_Space.thy Fri Apr 27 12:38:30 2018 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy Fri Apr 27 12:43:05 2018 +0100
@@ -1622,7 +1622,7 @@
using emeasure_subadditive[OF measurable] fin
apply simp
apply (subst (asm) (2 3 4) emeasure_eq_ennreal_measure)
- apply (auto simp add: ennreal_plus[symmetric] simp del: ennreal_plus)
+ apply (auto reorient: ennreal_plus)
done
qed
--- a/src/HOL/Analysis/Regularity.thy Fri Apr 27 12:38:30 2018 +0100
+++ b/src/HOL/Analysis/Regularity.thy Fri Apr 27 12:43:05 2018 +0100
@@ -107,7 +107,7 @@
finally have "measure M (space M) \<le> measure M K + e"
using \<open>0 < e\<close> by simp
hence "emeasure M (space M) \<le> emeasure M K + e"
- using \<open>0 < e\<close> by (simp add: emeasure_eq_measure measure_nonneg ennreal_plus[symmetric] del: ennreal_plus)
+ using \<open>0 < e\<close> by (simp add: emeasure_eq_measure reorient: ennreal_plus)
moreover have "compact K"
unfolding compact_eq_totally_bounded
proof safe
@@ -139,9 +139,9 @@
also have "\<dots> \<le> measure M (space M) - measure M K"
by (simp add: emeasure_eq_measure sU sb finite_measure_mono)
also have "\<dots> \<le> e"
- using K \<open>0 < e\<close> by (simp add: emeasure_eq_measure ennreal_plus[symmetric] measure_nonneg del: ennreal_plus)
+ using K \<open>0 < e\<close> by (simp add: emeasure_eq_measure reorient: ennreal_plus)
finally have "emeasure M A \<le> emeasure M (A \<inter> K) + ennreal e"
- using \<open>0<e\<close> by (simp add: emeasure_eq_measure algebra_simps ennreal_plus[symmetric] measure_nonneg del: ennreal_plus)
+ using \<open>0<e\<close> by (simp add: emeasure_eq_measure algebra_simps reorient: ennreal_plus)
moreover have "A \<inter> K \<subseteq> A" "compact (A \<inter> K)" using \<open>closed A\<close> \<open>compact K\<close> by auto
ultimately show "\<exists>K \<subseteq> A. compact K \<and> emeasure M A \<le> emeasure M K + ennreal e"
by blast
@@ -301,7 +301,7 @@
have "measure M (\<Union>i. D i) < (\<Sum>i<n0. measure M (D i)) + e/2" using n0 by simp
also have "(\<Sum>i<n0. measure M (D i)) \<le> (\<Sum>i<n0. measure M (K i) + e/(2*Suc n0))"
using K \<open>0 < e\<close>
- by (auto intro: sum_mono simp: emeasure_eq_measure measure_nonneg ennreal_plus[symmetric] simp del: ennreal_plus)
+ by (auto intro: sum_mono simp: emeasure_eq_measure reorient: ennreal_plus)
also have "\<dots> = (\<Sum>i<n0. measure M (K i)) + (\<Sum>i<n0. e/(2*Suc n0))"
by (simp add: sum.distrib)
also have "\<dots> \<le> (\<Sum>i<n0. measure M (K i)) + e / 2" using \<open>0 < e\<close>
@@ -310,7 +310,7 @@
have "measure M (\<Union>i. D i) < (\<Sum>i<n0. measure M (K i)) + e / 2 + e / 2"
by auto
hence "M (\<Union>i. D i) < M ?K + e"
- using \<open>0<e\<close> by (auto simp: mK emeasure_eq_measure measure_nonneg sum_nonneg ennreal_less_iff ennreal_plus[symmetric] simp del: ennreal_plus)
+ using \<open>0<e\<close> by (auto simp: mK emeasure_eq_measure sum_nonneg ennreal_less_iff reorient: ennreal_plus)
moreover
have "?K \<subseteq> (\<Union>i. D i)" using K by auto
moreover
@@ -332,9 +332,9 @@
from INF_approx_ennreal[OF \<open>0 < e/(2 powr Suc i)\<close> this]
show "\<exists>U. D i \<subseteq> U \<and> open U \<and> e/(2 powr Suc i) > emeasure M U - emeasure M (D i)"
using \<open>0<e\<close>
- by (auto simp: emeasure_eq_measure measure_nonneg sum_nonneg ennreal_less_iff ennreal_plus[symmetric] ennreal_minus
+ by (auto simp: emeasure_eq_measure sum_nonneg ennreal_less_iff ennreal_minus
finite_measure_mono sb
- simp del: ennreal_plus)
+ reorient: ennreal_plus)
qed
then obtain U where U: "\<And>i. D i \<subseteq> U i" "\<And>i. open (U i)"
"\<And>i. e/(2 powr Suc i) > emeasure M (U i) - emeasure M (D i)"
@@ -367,7 +367,7 @@
also have "\<dots> = ennreal e"
by (subst suminf_ennreal_eq[OF zero_le_power power_half_series]) auto
finally have "emeasure M ?U \<le> emeasure M (\<Union>i. D i) + ennreal e"
- using \<open>0<e\<close> by (simp add: emeasure_eq_measure ennreal_plus[symmetric] measure_nonneg del: ennreal_plus)
+ using \<open>0<e\<close> by (simp add: emeasure_eq_measure reorient: ennreal_plus)
moreover
have "(\<Union>i. D i) \<subseteq> ?U" using U by auto
moreover
--- a/src/HOL/Analysis/Set_Integral.thy Fri Apr 27 12:38:30 2018 +0100
+++ b/src/HOL/Analysis/Set_Integral.thy Fri Apr 27 12:43:05 2018 +0100
@@ -869,7 +869,7 @@
2 * (\<integral>\<^sup>+x. norm(f x) \<partial>M)" by simp
have le: "ennreal (norm (F n x - f x)) \<le> ennreal (norm (f x)) + ennreal (norm (F n x))" for n x
- by (simp add: norm_minus_commute norm_triangle_ineq4 ennreal_plus[symmetric] ennreal_minus del: ennreal_plus)
+ by (simp add: norm_minus_commute norm_triangle_ineq4 ennreal_minus reorient: ennreal_plus)
then have le2: "(\<integral>\<^sup>+ x. ennreal (norm (F n x - f x)) \<partial>M) \<le> (\<integral>\<^sup>+ x. ennreal (norm (f x)) + ennreal (norm (F n x)) \<partial>M)" for n
by (rule nn_integral_mono)
@@ -882,7 +882,7 @@
proof (intro arg_cong[where f=liminf] ext)
fix n
have "\<And>x. ennreal(G n x) = ennreal(norm(f x)) + ennreal(norm(F n x)) - ennreal(norm(F n x - f x))"
- unfolding G_def by (simp add: ennreal_plus[symmetric] ennreal_minus del: ennreal_plus)
+ unfolding G_def by (simp add: ennreal_minus reorient: ennreal_plus)
moreover have "(\<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) - ennreal(norm(F n x - f x)) \<partial>M)
= (\<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \<partial>M) - (\<integral>\<^sup>+x. norm(F n x - f x) \<partial>M)"
proof (rule nn_integral_diff)
--- a/src/HOL/Analysis/Sigma_Algebra.thy Fri Apr 27 12:38:30 2018 +0100
+++ b/src/HOL/Analysis/Sigma_Algebra.thy Fri Apr 27 12:43:05 2018 +0100
@@ -2085,7 +2085,7 @@
have "(\<lambda>x. g (f x)) \<in> X \<rightarrow> space M" "\<And>A. A \<inter> f -` Y \<inter> X = A \<inter> X"
using * by auto
with * show "sets ?VV = sets ?V"
- by (simp add: sets_vimage_algebra2 ex_simps[symmetric] vimage_comp comp_def del: ex_simps)
+ by (simp add: sets_vimage_algebra2 vimage_comp comp_def reorient: ex_simps)
qed (simp add: vimage_algebra_def emeasure_sigma)
subsubsection \<open>Restricted Space Sigma Algebra\<close>
--- a/src/Pure/raw_simplifier.ML Fri Apr 27 12:38:30 2018 +0100
+++ b/src/Pure/raw_simplifier.ML Fri Apr 27 12:43:05 2018 +0100
@@ -90,6 +90,7 @@
val prems_of: Proof.context -> thm list
val add_simp: thm -> Proof.context -> Proof.context
val del_simp: thm -> Proof.context -> Proof.context
+ val reorient_simp: thm -> Proof.context -> Proof.context
val init_simpset: thm list -> Proof.context -> Proof.context
val add_eqcong: thm -> Proof.context -> Proof.context
val del_eqcong: thm -> Proof.context -> Proof.context
@@ -560,16 +561,21 @@
else rrule_eq_True ctxt thm name lhs elhs rhs thm
end;
-fun extract_rews ctxt thms =
- let val Simpset (_, {mk_rews = {mk, ...}, ...}) = simpset_of ctxt
- in maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk ctxt thm)) thms end;
+fun extract_rews ctxt sym thms =
+ let
+ val Simpset (_, {mk_rews = {mk, ...}, ...}) = simpset_of ctxt;
+ val mk =
+ if sym then fn ctxt => fn th => (mk ctxt th) RL [Drule.symmetric_thm]
+ else mk
+ in maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk ctxt thm)) thms
+ end;
fun extract_safe_rrules ctxt thm =
- maps (orient_rrule ctxt) (extract_rews ctxt [thm]);
+ maps (orient_rrule ctxt) (extract_rews ctxt false [thm]);
fun mk_rrules ctxt thms =
let
- val rews = extract_rews ctxt thms
+ val rews = extract_rews ctxt false thms
val raw_rrules = flat (map (mk_rrule ctxt) rews)
in map mk_rrule2 raw_rrules end
@@ -578,20 +584,24 @@
local
-fun comb_simps ctxt comb mk_rrule thms =
- let val rews = extract_rews ctxt (map (Thm.transfer' ctxt) thms);
+fun comb_simps ctxt comb mk_rrule sym thms =
+ let val rews = extract_rews ctxt sym (map (Thm.transfer' ctxt) thms);
in fold (fold comb o mk_rrule) rews ctxt end;
in
fun ctxt addsimps thms =
- comb_simps ctxt insert_rrule (mk_rrule ctxt) thms;
+ comb_simps ctxt insert_rrule (mk_rrule ctxt) false thms;
+
+fun addsymsimps ctxt thms =
+ comb_simps ctxt insert_rrule (mk_rrule ctxt) true thms;
fun ctxt delsimps thms =
- comb_simps ctxt del_rrule (map mk_rrule2 o mk_rrule ctxt) thms;
+ comb_simps ctxt del_rrule (map mk_rrule2 o mk_rrule ctxt) false thms;
fun add_simp thm ctxt = ctxt addsimps [thm];
fun del_simp thm ctxt = ctxt delsimps [thm];
+fun reorient_simp thm ctxt = addsymsimps (ctxt delsimps [thm]) [thm];
end;
--- a/src/Pure/simplifier.ML Fri Apr 27 12:38:30 2018 +0100
+++ b/src/Pure/simplifier.ML Fri Apr 27 12:43:05 2018 +0100
@@ -32,6 +32,7 @@
val attrib: (thm -> Proof.context -> Proof.context) -> attribute
val simp_add: attribute
val simp_del: attribute
+ val simp_reorient: attribute
val cong_add: attribute
val cong_del: attribute
val check_simproc: Proof.context -> xstring * Position.T -> string
@@ -89,6 +90,7 @@
val simp_add = attrib add_simp;
val simp_del = attrib del_simp;
+val simp_reorient = attrib reorient_simp;
val cong_add = attrib add_cong;
val cong_del = attrib del_cong;
@@ -267,6 +269,7 @@
(* add / del *)
val simpN = "simp";
+val reorientN = "reorient"
val congN = "cong";
val onlyN = "only";
val no_asmN = "no_asm";
@@ -340,6 +343,7 @@
[Args.$$$ simpN -- Args.colon >> K (Method.modifier simp_add \<^here>),
Args.$$$ simpN -- Args.add -- Args.colon >> K (Method.modifier simp_add \<^here>),
Args.$$$ simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del \<^here>),
+ Args.$$$ reorientN -- Args.colon >> K (Method.modifier simp_reorient \<^here>),
Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >>
K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = \<^here>}]
@ cong_modifiers;
@@ -347,6 +351,7 @@
val simp_modifiers' =
[Args.add -- Args.colon >> K (Method.modifier simp_add \<^here>),
Args.del -- Args.colon >> K (Method.modifier simp_del \<^here>),
+ Args.$$$ reorientN -- Args.colon >> K (Method.modifier simp_reorient \<^here>),
Args.$$$ onlyN -- Args.colon >>
K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = \<^here>}]
@ cong_modifiers;