--- a/src/HOL/Analysis/Bochner_Integration.thy Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Bochner_Integration.thy Thu Apr 26 19:51:32 2018 +0200
@@ -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 Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Thu Apr 26 19:51:32 2018 +0200
@@ -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 Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Change_Of_Vars.thy Thu Apr 26 19:51:32 2018 +0200
@@ -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/Equivalence_Lebesgue_Henstock_Integration.thy Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Apr 26 19:51:32 2018 +0200
@@ -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 Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/FPS_Convergence.thy Thu Apr 26 19:51:32 2018 +0200
@@ -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 Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy Thu Apr 26 19:51:32 2018 +0200
@@ -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 Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Apr 26 19:51:32 2018 +0200
@@ -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 Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Interval_Integral.thy Thu Apr 26 19:51:32 2018 +0200
@@ -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 Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Thu Apr 26 19:51:32 2018 +0200
@@ -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 Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy Thu Apr 26 19:51:32 2018 +0200
@@ -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 Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Regularity.thy Thu Apr 26 19:51:32 2018 +0200
@@ -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 Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Set_Integral.thy Thu Apr 26 19:51:32 2018 +0200
@@ -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 Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Sigma_Algebra.thy Thu Apr 26 19:51:32 2018 +0200
@@ -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 Wed Apr 25 21:29:02 2018 +0100
+++ b/src/Pure/raw_simplifier.ML Thu Apr 26 19:51:32 2018 +0200
@@ -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 Wed Apr 25 21:29:02 2018 +0100
+++ b/src/Pure/simplifier.ML Thu Apr 26 19:51:32 2018 +0200
@@ -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;