# HG changeset patch # User nipkow # Date 1528302003 -7200 # Node ID 05605481935d99e06d7cd7ccf498a9e4e71352c5 # Parent 76edba1c428c757a5f5f2c35796e38ddfc3ccaae# Parent 223172b97d0bf3eea3918ee22648f7aa158e230c merged diff -r 76edba1c428c -r 05605481935d NEWS --- 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 *** diff -r 76edba1c428c -r 05605481935d src/Doc/Isar_Ref/Generic.thy --- 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} \} \<^descr> @{method simp} invokes the Simplifier on the first subgoal, after @@ -292,6 +293,11 @@ situations to perform the intended simplification step! \<^medskip> +Modifier \flip\ 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 \only\ modifier first removes all other rewrite rules, looper tactics (including split rules), congruence rules, and then behaves like \add\. Implicit solvers remain, which means that trivial rules like reflexivity or diff -r 76edba1c428c -r 05605481935d src/HOL/Analysis/Bochner_Integration.thy --- 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 "\ = (\\<^sup>+x. f x \M)" using f by (intro nn_integral_eq_simple_integral[symmetric]) @@ -504,7 +504,7 @@ using simple_bochner_integrable_compose2[of "\x y. norm (x - y)" M "s" "t"] s t by (auto intro!: simple_bochner_integral_eq_nn_integral) also have "\ \ (\\<^sup>+x. ennreal (norm (f x - s x)) + ennreal (norm (f x - t x)) \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 "\ = ?S + ?T" @@ -594,7 +594,7 @@ proof (intro always_eventually allI) fix i have "?f i \ (\\<^sup>+ x. (norm (f x - sf i x)) + ennreal (norm (g x - sg i x)) \M)" by (auto intro!: nn_integral_mono norm_diff_triangle_ineq - reorient: ennreal_plus) + simp flip: ennreal_plus) also have "\ = ?g i" by (intro nn_integral_add) auto finally show "?f i \ ?g i" . @@ -747,7 +747,7 @@ finally have s_fin: "(\\<^sup>+x. norm (s i x) \M) < \" . have "(\\<^sup>+ x. norm (f x) \M) \ (\\<^sup>+ x. ennreal (norm (f x - s i x)) + ennreal (norm (s i x)) \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 "\ = (\\<^sup>+x. norm (f x - s i x) \M) + (\\<^sup>+x. norm (s i x) \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 "\ \ (\\<^sup>+x. ennreal (norm (f x - s n x)) + norm (f x) \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 "\ = ?t n" by (rule nn_integral_add) auto @@ -828,7 +828,7 @@ using tendsto_add[OF \?S \ 0\ \?T \ 0\] by simp qed then have "(\i. norm (?s i - ?t i)) \ 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 "\ < ennreal (e / 2) + e / 2" by (intro add_strict_mono M n m) - also have "\ = e" using \0 by (simp reorient: ennreal_plus) + also have "\ = e" using \0 by (simp flip: ennreal_plus) finally show "dist (?s n) (?s m) < e" using \0 by (simp add: dist_norm ennreal_less_iff) qed @@ -1219,7 +1219,7 @@ fix x assume "(\i. u i x) \ u' x" from tendsto_diff[OF tendsto_const[of "u' x"] this] show "(\i. ennreal (norm (u' x - u i x))) \ 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 "((\n. norm((\x. u n x \M) - (\x. f x \M))) \ 0) F" - by (simp reorient: ennreal_0) + by (simp flip: ennreal_0) then have "((\n. ((\x. u n x \M) - (\x. f x \M))) \ 0) F" using tendsto_norm_zero_iff by blast then show ?thesis using Lim_null by auto qed @@ -2215,7 +2215,7 @@ ultimately have "(\n. ennreal (norm(u (r n) x))) \ 0" using tendsto_Limsup[of sequentially "\n. ennreal (norm(u (r n) x))"] by auto then have "(\n. norm(u (r n) x)) \ 0" - by (simp reorient: ennreal_0) + by (simp flip: ennreal_0) then have "(\n. u (r n) x) \ 0" by (simp add: tendsto_norm_zero_iff) } diff -r 76edba1c428c -r 05605481935d src/HOL/Analysis/Cauchy_Integral_Theorem.thy --- 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 \ y \ \" "winding_number \ z \ \" using that integer_winding_number [OF \ loop] sg \y \ S\ 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 (\w. winding_number \ w)" using continuous_on_winding_number [OF \] sg @@ -6667,7 +6667,7 @@ by (rule derivative_eq_intros | simp)+ have y_le: "\cmod (z - y) * 2 < r - cmod z\ \ cmod y \ cmod (of_real r + of_real (cmod z)) / 2" for z y using \r > 0\ - 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 \r > 0\ by simp moreover have "\z. cmod z < r \ cmod ((of_real r + of_real (cmod z)) / 2) < cmod (of_real r)" using \r > 0\ - by (simp reorient: of_real_add) + by (simp flip: of_real_add) ultimately have sum: "\z. cmod z < r \ summable (\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 "\g g'. \z \ ball 0 r. (\n. (a n) * z ^ n) sums g z \ @@ -6723,7 +6723,7 @@ then have "0 \ r" by (meson less_eq_real_def norm_ge_zero order_trans) show ?thesis - using w by (simp add: dist_norm \0\r\ reorient: of_real_add) + using w by (simp add: dist_norm \0\r\ flip: of_real_add) qed have sum: "summable (\n. a n * of_real (((cmod (z - w) + r) / 2) ^ n))" using assms [OF inb] by (force simp: summable_def dist_norm) diff -r 76edba1c428c -r 05605481935d src/HOL/Analysis/Change_Of_Vars.thy --- 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 "(\k\n. real k * e * ?\ (T k)) = (\k\n. integral (T k) (\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 "\ \ (\k\n. integral (T k) (\x. (abs (det (matrix (f' x))))))" proof (rule sum_mono) fix k diff -r 76edba1c428c -r 05605481935d src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy --- 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 "?\ E - 2*e \ ?\ (E - (E \ \(snd`(p - s))))" using \0 < e\ \E \ sets ?L\ 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 "\ \ ?\ (\x\p \ 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 \ a" "0 \ b" "(\\<^sup>+ x. h x \lborel) = ennreal a" "(\\<^sup>+ x. g x \lborel) = ennreal b" "r = a + b" by (cases "\\<^sup>+ x. h x \lborel" "\\<^sup>+ x. g x \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 diff -r 76edba1c428c -r 05605481935d src/HOL/Analysis/FPS_Convergence.thy --- 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) \ 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"] diff -r 76edba1c428c -r 05605481935d src/HOL/Analysis/Gamma_Function.thy --- 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 "(\z. inverse (rGamma z / (z + of_nat n))) \ (- of_nat n) \ ?c" . qed diff -r 76edba1c428c -r 05605481935d src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- 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 :: "_ \ 'b :: real_normed_field" assumes "f integrable_on s" shows "(\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 :: "_ \ 'b :: real_normed_field" assumes "c \ 0" shows "(\x. f x / of_real c) integrable_on s \ 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 \ (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 diff -r 76edba1c428c -r 05605481935d src/HOL/Analysis/Interval_Integral.thy --- 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 "\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 \ x" "x \ u i" with \a < ereal (l i)\ \ereal (u i) < b\ 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 \a < l i\ \u i < b\ 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 diff -r 76edba1c428c -r 05605481935d src/HOL/Analysis/Lebesgue_Measure.thy --- 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 "... \ (\i\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) \ (\i\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) \ (\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 diff -r 76edba1c428c -r 05605481935d src/HOL/Analysis/Measure_Space.thy --- 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 diff -r 76edba1c428c -r 05605481935d src/HOL/Analysis/Regularity.thy --- 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) \ measure M K + e" using \0 < e\ by simp hence "emeasure M (space M) \ emeasure M K + e" - using \0 < e\ by (simp add: emeasure_eq_measure reorient: ennreal_plus) + using \0 < e\ 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 "\ \ measure M (space M) - measure M K" by (simp add: emeasure_eq_measure sU sb finite_measure_mono) also have "\ \ e" - using K \0 < e\ by (simp add: emeasure_eq_measure reorient: ennreal_plus) + using K \0 < e\ by (simp add: emeasure_eq_measure flip: ennreal_plus) finally have "emeasure M A \ emeasure M (A \ K) + ennreal e" - using \0 by (simp add: emeasure_eq_measure algebra_simps reorient: ennreal_plus) + using \0 by (simp add: emeasure_eq_measure algebra_simps flip: ennreal_plus) moreover have "A \ K \ A" "compact (A \ K)" using \closed A\ \compact K\ by auto ultimately show "\K \ A. compact K \ emeasure M A \ emeasure M K + ennreal e" by blast @@ -301,7 +301,7 @@ have "measure M (\i. D i) < (\ii (\i0 < e\ - 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 "\ = (\ii \ (\i0 < e\ @@ -310,7 +310,7 @@ have "measure M (\i. D i) < (\ii. D i) < M ?K + e" - using \0 by (auto simp: mK emeasure_eq_measure sum_nonneg ennreal_less_iff reorient: ennreal_plus) + using \0 by (auto simp: mK emeasure_eq_measure sum_nonneg ennreal_less_iff simp flip: ennreal_plus) moreover have "?K \ (\i. D i)" using K by auto moreover @@ -334,7 +334,7 @@ using \0 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: "\i. D i \ U i" "\i. open (U i)" "\i. e/(2 powr Suc i) > emeasure M (U i) - emeasure M (D i)" @@ -367,7 +367,7 @@ also have "\ = ennreal e" by (subst suminf_ennreal_eq[OF zero_le_power power_half_series]) auto finally have "emeasure M ?U \ emeasure M (\i. D i) + ennreal e" - using \0 by (simp add: emeasure_eq_measure reorient: ennreal_plus) + using \0 by (simp add: emeasure_eq_measure flip: ennreal_plus) moreover have "(\i. D i) \ ?U" using U by auto moreover diff -r 76edba1c428c -r 05605481935d src/HOL/Analysis/Set_Integral.thy --- 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 * (\\<^sup>+x. norm(f x) \M)" by simp have le: "ennreal (norm (F n x - f x)) \ 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: "(\\<^sup>+ x. ennreal (norm (F n x - f x)) \M) \ (\\<^sup>+ x. ennreal (norm (f x)) + ennreal (norm (F n x)) \M)" for n by (rule nn_integral_mono) @@ -882,7 +882,7 @@ proof (intro arg_cong[where f=liminf] ext) fix n have "\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 "(\\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) - ennreal(norm(F n x - f x)) \M) = (\\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \M) - (\\<^sup>+x. norm(F n x - f x) \M)" proof (rule nn_integral_diff) diff -r 76edba1c428c -r 05605481935d src/HOL/Analysis/Sigma_Algebra.thy --- 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 "(\x. g (f x)) \ X \ space M" "\A. A \ f -` Y \ X = A \ 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 \Restricted Space Sigma Algebra\ diff -r 76edba1c428c -r 05605481935d src/HOL/Analysis/Weierstrass_Theorems.thy --- 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 "(\k\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 "(\k\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] \k>0\ - 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 "... \ (1/(k * (p t))^n) * 1" apply (rule mult_left_mono [OF power_le_one]) using pt_pos \k>0\ p01 power_le_one t apply auto @@ -550,7 +550,7 @@ shows "\f \ R. f ` S \ {0..1} \ (\x \ A. f x < e) \ (\x \ B. f x > 1 - e)" proof (cases "A \ {} \ B \ {}") 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 * (\ii=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="\x. \b\Basis. pf b x *\<^sub>R b" in exI) - apply (auto simp: sum_subtractf [symmetric]) + apply (auto simp flip: sum_subtractf) done qed diff -r 76edba1c428c -r 05605481935d src/Pure/raw_simplifier.ML --- 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; diff -r 76edba1c428c -r 05605481935d src/Pure/simplifier.ML --- 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;