--- a/NEWS Wed Jun 06 17:18:48 2018 +0200
+++ b/NEWS Wed Jun 06 18:20:03 2018 +0200
@@ -202,6 +202,12 @@
locale instances where the qualifier's sole purpose is avoiding
duplicate constant declarations.
+* Proof method 'simp' now supports a new modifier 'flip:' followed by a list
+of theorems. Each of these theorems is removed from the simpset
+(without warning if it is not there) and the symmetric version of the theorem
+(i.e. lhs and rhs exchanged) is added to the simpset.
+For 'auto' and friends the modifier is "simp flip:".
+
*** Pure ***
--- a/src/Doc/Isar_Ref/Generic.thy Wed Jun 06 17:18:48 2018 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy Wed Jun 06 18:20:03 2018 +0200
@@ -275,8 +275,9 @@
opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'
;
- @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'split' (() | '!' | 'del') |
- 'cong' (() | 'add' | 'del')) ':' @{syntax thms}
+ @{syntax_def simpmod}: ('add' | 'del' | 'flip' | 'only' |
+ 'split' (() | '!' | 'del') | 'cong' (() | 'add' | 'del'))
+ ':' @{syntax thms}
\<close>}
\<^descr> @{method simp} invokes the Simplifier on the first subgoal, after
@@ -292,6 +293,11 @@
situations to perform the intended simplification step!
\<^medskip>
+Modifier \<open>flip\<close> deletes the following theorems from the simpset and adds
+their symmetric version (i.e.\ lhs and rhs exchanged). No warning is shown
+if the original theorem was not present.
+
+ \<^medskip>
The \<open>only\<close> modifier first removes all other rewrite rules, looper tactics
(including split rules), congruence rules, and then behaves like \<open>add\<close>.
Implicit solvers remain, which means that trivial rules like reflexivity or
--- a/src/HOL/Analysis/Bochner_Integration.thy Wed Jun 06 17:18:48 2018 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy Wed Jun 06 18:20:03 2018 +0200
@@ -476,7 +476,7 @@
(auto intro: f simple_function_compose1 elim: simple_bochner_integrable.cases
intro!: sum.cong ennreal_cong_mult
simp: ac_simps ennreal_mult
- reorient: sum_ennreal)
+ simp flip: sum_ennreal)
also have "\<dots> = (\<integral>\<^sup>+x. f x \<partial>M)"
using f
by (intro nn_integral_eq_simple_integral[symmetric])
@@ -504,7 +504,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 reorient: ennreal_plus)
+ by (auto intro!: nn_integral_mono simp flip: 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"
@@ -594,7 +594,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
- reorient: ennreal_plus)
+ simp flip: ennreal_plus)
also have "\<dots> = ?g i"
by (intro nn_integral_add) auto
finally show "?f i \<le> ?g i" .
@@ -747,7 +747,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 reorient: ennreal_plus)
+ by (auto intro!: nn_integral_mono simp flip: 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
@@ -783,7 +783,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 reorient: ennreal_plus)
+ by (auto intro!: nn_integral_mono simp flip: ennreal_plus)
(metis add.commute norm_minus_commute norm_triangle_sub)
also have "\<dots> = ?t n"
by (rule nn_integral_add) auto
@@ -828,7 +828,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 reorient: ennreal_0)
+ by (simp flip: ennreal_0)
ultimately have "norm (x - y) = 0"
by (rule LIMSEQ_unique)
then show "x = y" by simp
@@ -1174,7 +1174,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 reorient: ennreal_plus)
+ also have "\<dots> = e" using \<open>0<e\<close> by (simp flip: ennreal_plus)
finally show "dist (?s n) (?s m) < e"
using \<open>0<e\<close> by (simp add: dist_norm ennreal_less_iff)
qed
@@ -1219,7 +1219,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 reorient: ennreal_0)
+ by (simp add: tendsto_norm_zero_iff flip: ennreal_0)
qed
qed (insert bnd w_nonneg, auto)
then show ?thesis by simp
@@ -2117,7 +2117,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 reorient: ennreal_0)
+ by (simp flip: 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
@@ -2215,7 +2215,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 reorient: ennreal_0)
+ by (simp flip: 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 Jun 06 17:18:48 2018 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Wed Jun 06 18:20:03 2018 +0200
@@ -4145,7 +4145,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 reorient: of_int_diff)
+ by (auto simp: Ints_def simp flip: of_int_diff)
qed
have cont: "continuous_on S (\<lambda>w. winding_number \<gamma> w)"
using continuous_on_winding_number [OF \<gamma>] sg
@@ -6667,7 +6667,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 reorient: of_real_add)
+ apply (auto simp: algebra_simps norm_mult norm_divide norm_power simp flip: of_real_add)
using norm_triangle_ineq2 [of y z]
apply (simp only: diff_le_eq norm_minus_commute mult_2)
done
@@ -6675,7 +6675,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 reorient: of_real_add)
+ by (simp flip: 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>
@@ -6723,7 +6723,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> reorient: of_real_add)
+ using w by (simp add: dist_norm \<open>0\<le>r\<close> flip: 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: summable_def dist_norm)
--- a/src/HOL/Analysis/Change_Of_Vars.thy Wed Jun 06 17:18:48 2018 +0200
+++ b/src/HOL/Analysis/Change_Of_Vars.thy Wed Jun 06 18:20:03 2018 +0200
@@ -1280,7 +1280,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]
- reorient: integral_mult_right integral_mult_left)
+ flip: 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 Jun 06 17:18:48 2018 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Wed Jun 06 18:20:03 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: top_unique reorient: ennreal_plus
+ (auto simp: top_unique simp flip: 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 reorient: ennreal_plus)
+ (auto simp: add_top nn_integral_add top_add simp flip: ennreal_plus)
with add show ?case
by (auto intro!: has_integral_add)
next
--- a/src/HOL/Analysis/FPS_Convergence.thy Wed Jun 06 17:18:48 2018 +0200
+++ b/src/HOL/Analysis/FPS_Convergence.thy Wed Jun 06 18:20:03 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 reorient: fps_const_neg)
+ by (simp flip: 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 Jun 06 17:18:48 2018 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy Wed Jun 06 18:20:03 2018 +0200
@@ -1148,8 +1148,7 @@
lemma Gamma_1 [simp]: "Gamma 1 = 1" unfolding Gamma_def by simp
lemma Gamma_fact: "Gamma (1 + of_nat n) = fact n"
- by (simp add: pochhammer_fact pochhammer_Gamma of_nat_in_nonpos_Ints_iff
- reorient: of_nat_Suc)
+ by (simp add: pochhammer_fact pochhammer_Gamma of_nat_in_nonpos_Ints_iff flip: 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 +2429,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 reorient: power_mult_distrib)
+ by (simp_all add: field_simps flip: 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 Jun 06 17:18:48 2018 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Jun 06 18:20:03 2018 +0200
@@ -772,13 +772,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 reorient: of_real_inverse)
+by (simp add: integrable_on_cmult_right divide_inverse assms flip: 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 reorient: of_real_inverse)
+by (simp add: divide_inverse assms flip: 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
@@ -3410,7 +3410,7 @@
by (simp add: inner_simps field_simps)
ultimately show ?thesis using False
by (simp add: image_affinity_cbox content_cbox'
- prod.distrib[symmetric] inner_diff_left reorient: prod_constant)
+ prod.distrib[symmetric] inner_diff_left flip: prod_constant)
qed
qed
--- a/src/HOL/Analysis/Interval_Integral.thy Wed Jun 06 17:18:48 2018 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy Wed Jun 06 18:20:03 2018 +0200
@@ -88,7 +88,7 @@
from ereal_incseq_approx[OF this] guess X .
then show thesis
apply (intro that[of "\<lambda>i. - X i"])
- apply (auto simp: decseq_def incseq_def reorient: uminus_ereal.simps)
+ apply (auto simp: decseq_def incseq_def simp flip: uminus_ereal.simps)
apply (metis ereal_minus_less_minus ereal_uminus_uminus ereal_Lim_uminus)+
done
qed
@@ -121,7 +121,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 reorient: ereal_less_eq(3))
+ by (auto simp flip: ereal_less_eq(3))
qed
show thesis
by (intro that) fact+
@@ -283,7 +283,7 @@
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
- reorient: uminus_ereal.simps
+ simp flip: uminus_ereal.simps
split: split_indicator)
then show ?case
unfolding interval_lebesgue_integral_def
@@ -649,7 +649,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 reorient: ereal_less_eq)
+ (auto simp flip: 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 Jun 06 17:18:48 2018 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Wed Jun 06 18:20:03 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: sum_nonneg reorient: ennreal_plus)
+ using egt0 by (simp add: sum_nonneg flip: 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 Jun 06 17:18:48 2018 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy Wed Jun 06 18:20:03 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 reorient: ennreal_plus)
+ apply (auto simp flip: ennreal_plus)
done
qed
--- a/src/HOL/Analysis/Regularity.thy Wed Jun 06 17:18:48 2018 +0200
+++ b/src/HOL/Analysis/Regularity.thy Wed Jun 06 18:20:03 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 reorient: ennreal_plus)
+ using \<open>0 < e\<close> by (simp add: emeasure_eq_measure flip: 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 reorient: ennreal_plus)
+ using K \<open>0 < e\<close> by (simp add: emeasure_eq_measure flip: 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 reorient: ennreal_plus)
+ using \<open>0<e\<close> by (simp add: emeasure_eq_measure algebra_simps flip: 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 reorient: ennreal_plus)
+ by (auto intro: sum_mono simp: emeasure_eq_measure simp flip: 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 sum_nonneg ennreal_less_iff reorient: ennreal_plus)
+ using \<open>0<e\<close> by (auto simp: mK emeasure_eq_measure sum_nonneg ennreal_less_iff simp flip: ennreal_plus)
moreover
have "?K \<subseteq> (\<Union>i. D i)" using K by auto
moreover
@@ -334,7 +334,7 @@
using \<open>0<e\<close>
by (auto simp: emeasure_eq_measure sum_nonneg ennreal_less_iff ennreal_minus
finite_measure_mono sb
- reorient: ennreal_plus)
+ simp flip: 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 reorient: ennreal_plus)
+ using \<open>0<e\<close> by (simp add: emeasure_eq_measure flip: ennreal_plus)
moreover
have "(\<Union>i. D i) \<subseteq> ?U" using U by auto
moreover
--- a/src/HOL/Analysis/Set_Integral.thy Wed Jun 06 17:18:48 2018 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy Wed Jun 06 18:20:03 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_minus reorient: ennreal_plus)
+ by (simp add: norm_minus_commute norm_triangle_ineq4 ennreal_minus flip: 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_minus reorient: ennreal_plus)
+ unfolding G_def by (simp add: ennreal_minus flip: 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 Jun 06 17:18:48 2018 +0200
+++ b/src/HOL/Analysis/Sigma_Algebra.thy Wed Jun 06 18:20:03 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 vimage_comp comp_def reorient: ex_simps)
+ by (simp add: sets_vimage_algebra2 vimage_comp comp_def flip: ex_simps)
qed (simp add: vimage_algebra_def emeasure_sigma)
subsubsection \<open>Restricted Space Sigma Algebra\<close>
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy Wed Jun 06 17:18:48 2018 +0200
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy Wed Jun 06 18:20:03 2018 +0200
@@ -104,7 +104,7 @@
by (simp add: algebra_simps power2_eq_square)
have "(\<Sum>k\<le>n. (k - n * x)\<^sup>2 * Bernstein n k x) = n * x * (1 - x)"
apply (simp add: * sum.distrib)
- apply (simp add: sum_distrib_left [symmetric] mult.assoc)
+ apply (simp flip: sum_distrib_left add: mult.assoc)
apply (simp add: algebra_simps power2_eq_square)
done
then have "(\<Sum>k\<le>n. (k - n * x)\<^sup>2 * Bernstein n k x)/n^2 = x * (1 - x) / n"
@@ -383,7 +383,7 @@
done
also have "... = (1/(k * (p t))^n) * (1 - p t ^ (2*n)) ^ (k^n)"
using pt_pos [OF t] \<open>k>0\<close>
- by (simp add: algebra_simps power_mult power2_eq_square power_mult_distrib [symmetric])
+ by (simp add: algebra_simps power_mult power2_eq_square flip: power_mult_distrib)
also have "... \<le> (1/(k * (p t))^n) * 1"
apply (rule mult_left_mono [OF power_le_one])
using pt_pos \<open>k>0\<close> p01 power_le_one t apply auto
@@ -550,7 +550,7 @@
shows "\<exists>f \<in> R. f ` S \<subseteq> {0..1} \<and> (\<forall>x \<in> A. f x < e) \<and> (\<forall>x \<in> B. f x > 1 - e)"
proof (cases "A \<noteq> {} \<and> B \<noteq> {}")
case True then show ?thesis
- apply (simp add: ex_in_conv [symmetric])
+ apply (simp flip: ex_in_conv)
using assms
apply safe
apply (force simp add: intro!: two_special)
@@ -657,7 +657,7 @@
using xf01 t by force
have "g t = e * (\<Sum>i<j. xf i t) + e * (\<Sum>i=j..n. xf i t)"
using j1 jn e
- apply (simp add: g_def distrib_left [symmetric])
+ apply (simp add: g_def flip: distrib_left)
apply (subst sum.union_disjoint [symmetric])
apply (auto simp: ivl_disj_un)
done
@@ -1147,7 +1147,7 @@
show ?thesis
apply (subst euclidean_representation_sum_fun [of f, symmetric])
apply (rule_tac x="\<lambda>x. \<Sum>b\<in>Basis. pf b x *\<^sub>R b" in exI)
- apply (auto simp: sum_subtractf [symmetric])
+ apply (auto simp flip: sum_subtractf)
done
qed
--- a/src/Pure/raw_simplifier.ML Wed Jun 06 17:18:48 2018 +0200
+++ b/src/Pure/raw_simplifier.ML Wed Jun 06 18:20:03 2018 +0200
@@ -90,7 +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 flip_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
@@ -463,11 +463,14 @@
(* maintain simp rules *)
-fun del_rrule (rrule as {thm, elhs, ...}) ctxt =
+fun del_rrule loud (rrule as {thm, elhs, ...}) ctxt =
ctxt |> map_simpset1 (fn (rules, prems, depth) =>
(Net.delete_term eq_rrule (Thm.term_of elhs, rrule) rules, prems, depth))
handle Net.DELETE =>
- (cond_warning ctxt (fn () => print_thm ctxt "Rewrite rule not in simpset:" ("", thm)); ctxt);
+ (if not loud then ()
+ else cond_warning ctxt
+ (fn () => print_thm ctxt "Rewrite rule not in simpset:" ("", thm));
+ ctxt);
fun insert_rrule (rrule as {thm, name, ...}) ctxt =
(cond_tracing ctxt (fn () => print_thm ctxt "Adding rewrite rule" (name, thm));
@@ -597,11 +600,14 @@
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) false thms;
+ comb_simps ctxt (del_rrule true) (map mk_rrule2 o mk_rrule ctxt) false thms;
+
+fun delsimps_quiet ctxt thms =
+ comb_simps ctxt (del_rrule false) (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];
+fun flip_simp thm ctxt = addsymsimps (delsimps_quiet ctxt [thm]) [thm];
end;
--- a/src/Pure/simplifier.ML Wed Jun 06 17:18:48 2018 +0200
+++ b/src/Pure/simplifier.ML Wed Jun 06 18:20:03 2018 +0200
@@ -32,7 +32,7 @@
val attrib: (thm -> Proof.context -> Proof.context) -> attribute
val simp_add: attribute
val simp_del: attribute
- val simp_reorient: attribute
+ val simp_flip: attribute
val cong_add: attribute
val cong_del: attribute
val check_simproc: Proof.context -> xstring * Position.T -> string
@@ -90,7 +90,7 @@
val simp_add = attrib add_simp;
val simp_del = attrib del_simp;
-val simp_reorient = attrib reorient_simp;
+val simp_flip = attrib flip_simp;
val cong_add = attrib add_cong;
val cong_del = attrib del_cong;
@@ -269,7 +269,7 @@
(* add / del *)
val simpN = "simp";
-val reorientN = "reorient"
+val flipN = "flip"
val congN = "cong";
val onlyN = "only";
val no_asmN = "no_asm";
@@ -343,7 +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.$$$ flipN -- Args.colon >> K (Method.modifier simp_flip \<^here>),
Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >>
K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = \<^here>}]
@ cong_modifiers;
@@ -351,7 +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.$$$ flipN -- Args.colon >> K (Method.modifier simp_flip \<^here>),
Args.$$$ onlyN -- Args.colon >>
K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = \<^here>}]
@ cong_modifiers;