merged
authornipkow
Wed Jun 06 18:20:03 2018 +0200 (11 months ago)
changeset 6840405605481935d
parent 68402 76edba1c428c
parent 68403 223172b97d0b
child 68405 6a0852b8e5a8
merged
NEWS
     1.1 --- a/NEWS	Wed Jun 06 17:18:48 2018 +0200
     1.2 +++ b/NEWS	Wed Jun 06 18:20:03 2018 +0200
     1.3 @@ -202,6 +202,12 @@
     1.4  locale instances where the qualifier's sole purpose is avoiding
     1.5  duplicate constant declarations.
     1.6  
     1.7 +* Proof method 'simp' now supports a new modifier 'flip:' followed by a list
     1.8 +of theorems. Each of these theorems is removed from the simpset
     1.9 +(without warning if it is not there) and the symmetric version of the theorem
    1.10 +(i.e. lhs and rhs exchanged) is added to the simpset.
    1.11 +For 'auto' and friends the modifier is "simp flip:".
    1.12 +
    1.13  
    1.14  *** Pure ***
    1.15  
     2.1 --- a/src/Doc/Isar_Ref/Generic.thy	Wed Jun 06 17:18:48 2018 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Generic.thy	Wed Jun 06 18:20:03 2018 +0200
     2.3 @@ -275,8 +275,9 @@
     2.4  
     2.5      opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'
     2.6      ;
     2.7 -    @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'split' (() | '!' | 'del') |
     2.8 -      'cong' (() | 'add' | 'del')) ':' @{syntax thms}
     2.9 +    @{syntax_def simpmod}: ('add' | 'del' | 'flip' | 'only' |
    2.10 +      'split' (() | '!' | 'del') | 'cong' (() | 'add' | 'del'))
    2.11 +    ':' @{syntax thms}
    2.12    \<close>}
    2.13  
    2.14    \<^descr> @{method simp} invokes the Simplifier on the first subgoal, after
    2.15 @@ -292,6 +293,11 @@
    2.16    situations to perform the intended simplification step!
    2.17  
    2.18    \<^medskip>
    2.19 +Modifier \<open>flip\<close> deletes the following theorems from the simpset and adds
    2.20 +their symmetric version (i.e.\ lhs and rhs exchanged). No warning is shown
    2.21 +if the original theorem was not present.
    2.22 +
    2.23 +  \<^medskip>
    2.24    The \<open>only\<close> modifier first removes all other rewrite rules, looper tactics
    2.25    (including split rules), congruence rules, and then behaves like \<open>add\<close>.
    2.26    Implicit solvers remain, which means that trivial rules like reflexivity or
     3.1 --- a/src/HOL/Analysis/Bochner_Integration.thy	Wed Jun 06 17:18:48 2018 +0200
     3.2 +++ b/src/HOL/Analysis/Bochner_Integration.thy	Wed Jun 06 18:20:03 2018 +0200
     3.3 @@ -476,7 +476,7 @@
     3.4         (auto intro: f simple_function_compose1 elim: simple_bochner_integrable.cases
     3.5               intro!: sum.cong ennreal_cong_mult
     3.6               simp: ac_simps ennreal_mult
     3.7 -             reorient: sum_ennreal)
     3.8 +             simp flip: sum_ennreal)
     3.9    also have "\<dots> = (\<integral>\<^sup>+x. f x \<partial>M)"
    3.10      using f
    3.11      by (intro nn_integral_eq_simple_integral[symmetric])
    3.12 @@ -504,7 +504,7 @@
    3.13      using simple_bochner_integrable_compose2[of "\<lambda>x y. norm (x - y)" M "s" "t"] s t
    3.14      by (auto intro!: simple_bochner_integral_eq_nn_integral)
    3.15    also have "\<dots> \<le> (\<integral>\<^sup>+x. ennreal (norm (f x - s x)) + ennreal (norm (f x - t x)) \<partial>M)"
    3.16 -    by (auto intro!: nn_integral_mono reorient: ennreal_plus)
    3.17 +    by (auto intro!: nn_integral_mono simp flip: ennreal_plus)
    3.18         (metis (erased, hide_lams) add_diff_cancel_left add_diff_eq diff_add_eq order_trans
    3.19                norm_minus_commute norm_triangle_ineq4 order_refl)
    3.20    also have "\<dots> = ?S + ?T"
    3.21 @@ -594,7 +594,7 @@
    3.22      proof (intro always_eventually allI)
    3.23        fix i have "?f i \<le> (\<integral>\<^sup>+ x. (norm (f x - sf i x)) + ennreal (norm (g x - sg i x)) \<partial>M)"
    3.24          by (auto intro!: nn_integral_mono norm_diff_triangle_ineq
    3.25 -                 reorient: ennreal_plus)
    3.26 +                 simp flip: ennreal_plus)
    3.27        also have "\<dots> = ?g i"
    3.28          by (intro nn_integral_add) auto
    3.29        finally show "?f i \<le> ?g i" .
    3.30 @@ -747,7 +747,7 @@
    3.31    finally have s_fin: "(\<integral>\<^sup>+x. norm (s i x) \<partial>M) < \<infinity>" .
    3.32  
    3.33    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)"
    3.34 -    by (auto intro!: nn_integral_mono reorient: ennreal_plus)
    3.35 +    by (auto intro!: nn_integral_mono simp flip: ennreal_plus)
    3.36         (metis add.commute norm_triangle_sub)
    3.37    also have "\<dots> = (\<integral>\<^sup>+x. norm (f x - s i x) \<partial>M) + (\<integral>\<^sup>+x. norm (s i x) \<partial>M)"
    3.38      by (rule nn_integral_add) auto
    3.39 @@ -783,7 +783,7 @@
    3.40          by (intro simple_bochner_integral_eq_nn_integral)
    3.41             (auto intro: s simple_bochner_integrable_compose2)
    3.42        also have "\<dots> \<le> (\<integral>\<^sup>+x. ennreal (norm (f x - s n x)) + norm (f x) \<partial>M)"
    3.43 -        by (auto intro!: nn_integral_mono reorient: ennreal_plus)
    3.44 +        by (auto intro!: nn_integral_mono simp flip: ennreal_plus)
    3.45             (metis add.commute norm_minus_commute norm_triangle_sub)
    3.46        also have "\<dots> = ?t n"
    3.47          by (rule nn_integral_add) auto
    3.48 @@ -828,7 +828,7 @@
    3.49        using tendsto_add[OF \<open>?S \<longlonglongrightarrow> 0\<close> \<open>?T \<longlonglongrightarrow> 0\<close>] by simp
    3.50    qed
    3.51    then have "(\<lambda>i. norm (?s i - ?t i)) \<longlonglongrightarrow> 0"
    3.52 -    by (simp reorient: ennreal_0)
    3.53 +    by (simp flip: ennreal_0)
    3.54    ultimately have "norm (x - y) = 0"
    3.55      by (rule LIMSEQ_unique)
    3.56    then show "x = y" by simp
    3.57 @@ -1174,7 +1174,7 @@
    3.58          by (intro simple_bochner_integral_bounded s f)
    3.59        also have "\<dots> < ennreal (e / 2) + e / 2"
    3.60          by (intro add_strict_mono M n m)
    3.61 -      also have "\<dots> = e" using \<open>0<e\<close> by (simp reorient: ennreal_plus)
    3.62 +      also have "\<dots> = e" using \<open>0<e\<close> by (simp flip: ennreal_plus)
    3.63        finally show "dist (?s n) (?s m) < e"
    3.64          using \<open>0<e\<close> by (simp add: dist_norm ennreal_less_iff)
    3.65      qed
    3.66 @@ -1219,7 +1219,7 @@
    3.67        fix x assume "(\<lambda>i. u i x) \<longlonglongrightarrow> u' x"
    3.68        from tendsto_diff[OF tendsto_const[of "u' x"] this]
    3.69        show "(\<lambda>i. ennreal (norm (u' x - u i x))) \<longlonglongrightarrow> 0"
    3.70 -        by (simp add: tendsto_norm_zero_iff reorient: ennreal_0)
    3.71 +        by (simp add: tendsto_norm_zero_iff flip: ennreal_0)
    3.72      qed
    3.73    qed (insert bnd w_nonneg, auto)
    3.74    then show ?thesis by simp
    3.75 @@ -2117,7 +2117,7 @@
    3.76        by auto
    3.77    qed
    3.78    then have "((\<lambda>n. norm((\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M))) \<longlongrightarrow> 0) F"
    3.79 -    by (simp reorient: ennreal_0)
    3.80 +    by (simp flip: ennreal_0)
    3.81    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
    3.82    then show ?thesis using Lim_null by auto
    3.83  qed
    3.84 @@ -2215,7 +2215,7 @@
    3.85      ultimately have "(\<lambda>n. ennreal (norm(u (r n) x))) \<longlonglongrightarrow> 0"
    3.86        using tendsto_Limsup[of sequentially "\<lambda>n. ennreal (norm(u (r n) x))"] by auto
    3.87      then have "(\<lambda>n. norm(u (r n) x)) \<longlonglongrightarrow> 0"
    3.88 -      by (simp reorient: ennreal_0)
    3.89 +      by (simp flip: ennreal_0)
    3.90      then have "(\<lambda>n. u (r n) x) \<longlonglongrightarrow> 0"
    3.91        by (simp add: tendsto_norm_zero_iff)
    3.92    }
     4.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Wed Jun 06 17:18:48 2018 +0200
     4.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Wed Jun 06 18:20:03 2018 +0200
     4.3 @@ -4145,7 +4145,7 @@
     4.4      have "winding_number \<gamma> y \<in> \<int>"  "winding_number \<gamma> z \<in>  \<int>"
     4.5        using that integer_winding_number [OF \<gamma> loop] sg \<open>y \<in> S\<close> by auto
     4.6      with ne show ?thesis
     4.7 -      by (auto simp: Ints_def reorient: of_int_diff)
     4.8 +      by (auto simp: Ints_def simp flip: of_int_diff)
     4.9    qed
    4.10    have cont: "continuous_on S (\<lambda>w. winding_number \<gamma> w)"
    4.11      using continuous_on_winding_number [OF \<gamma>] sg
    4.12 @@ -6667,7 +6667,7 @@
    4.13        by (rule derivative_eq_intros | simp)+
    4.14      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
    4.15        using \<open>r > 0\<close>
    4.16 -      apply (auto simp: algebra_simps norm_mult norm_divide norm_power reorient: of_real_add)
    4.17 +      apply (auto simp: algebra_simps norm_mult norm_divide norm_power simp flip: of_real_add)
    4.18        using norm_triangle_ineq2 [of y z]
    4.19        apply (simp only: diff_le_eq norm_minus_commute mult_2)
    4.20        done
    4.21 @@ -6675,7 +6675,7 @@
    4.22        using assms \<open>r > 0\<close> by simp
    4.23      moreover have "\<And>z. cmod z < r \<Longrightarrow> cmod ((of_real r + of_real (cmod z)) / 2) < cmod (of_real r)"
    4.24        using \<open>r > 0\<close>
    4.25 -      by (simp reorient: of_real_add)
    4.26 +      by (simp flip: of_real_add)
    4.27      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)"
    4.28        by (rule power_series_conv_imp_absconv_weak)
    4.29      have "\<exists>g g'. \<forall>z \<in> ball 0 r. (\<lambda>n.  (a n) * z ^ n) sums g z \<and>
    4.30 @@ -6723,7 +6723,7 @@
    4.31        then have "0 \<le> r"
    4.32          by (meson less_eq_real_def norm_ge_zero order_trans)
    4.33        show ?thesis
    4.34 -        using w by (simp add: dist_norm \<open>0\<le>r\<close> reorient: of_real_add)
    4.35 +        using w by (simp add: dist_norm \<open>0\<le>r\<close> flip: of_real_add)
    4.36      qed
    4.37      have sum: "summable (\<lambda>n. a n * of_real (((cmod (z - w) + r) / 2) ^ n))"
    4.38        using assms [OF inb] by (force simp: summable_def dist_norm)
     5.1 --- a/src/HOL/Analysis/Change_Of_Vars.thy	Wed Jun 06 17:18:48 2018 +0200
     5.2 +++ b/src/HOL/Analysis/Change_Of_Vars.thy	Wed Jun 06 18:20:03 2018 +0200
     5.3 @@ -1280,7 +1280,7 @@
     5.4        proof (rule add_mono)
     5.5          have "(\<Sum>k\<le>n. real k * e * ?\<mu> (T k)) = (\<Sum>k\<le>n. integral (T k) (\<lambda>x. k * e))"
     5.6            by (simp add: lmeasure_integral [OF meas_t]
     5.7 -                   reorient: integral_mult_right integral_mult_left)
     5.8 +                   flip: integral_mult_right integral_mult_left)
     5.9          also have "\<dots> \<le> (\<Sum>k\<le>n. integral (T k) (\<lambda>x.  (abs (det (matrix (f' x))))))"
    5.10          proof (rule sum_mono)
    5.11            fix k
     6.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Wed Jun 06 17:18:48 2018 +0200
     6.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Wed Jun 06 18:20:03 2018 +0200
     6.3 @@ -244,7 +244,7 @@
     6.4        finally have "?\<mu> E - 2*e \<le> ?\<mu> (E - (E \<inter> \<Union>(snd`(p - s))))"
     6.5          using \<open>0 < e\<close> \<open>E \<in> sets ?L\<close> tagged_division_ofD(1)[OF p(1)]
     6.6          by (subst emeasure_Diff)
     6.7 -           (auto simp: top_unique reorient: ennreal_plus
     6.8 +           (auto simp: top_unique simp flip: ennreal_plus
     6.9                   intro!: sets.Int sets.finite_UN ennreal_mono_minus intro: p_in_L)
    6.10        also have "\<dots> \<le> ?\<mu> (\<Union>x\<in>p \<inter> s. snd x)"
    6.11        proof (safe intro!: emeasure_mono subsetI)
    6.12 @@ -481,7 +481,7 @@
    6.13      by (simp add: nn_integral_add)
    6.14    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"
    6.15      by (cases "\<integral>\<^sup>+ x. h x \<partial>lborel" "\<integral>\<^sup>+ x. g x \<partial>lborel" rule: ennreal2_cases)
    6.16 -       (auto simp: add_top nn_integral_add top_add reorient: ennreal_plus)
    6.17 +       (auto simp: add_top nn_integral_add top_add simp flip: ennreal_plus)
    6.18    with add show ?case
    6.19      by (auto intro!: has_integral_add)
    6.20  next
     7.1 --- a/src/HOL/Analysis/FPS_Convergence.thy	Wed Jun 06 17:18:48 2018 +0200
     7.2 +++ b/src/HOL/Analysis/FPS_Convergence.thy	Wed Jun 06 18:20:03 2018 +0200
     7.3 @@ -271,7 +271,7 @@
     7.4  lemma fps_conv_radius_uminus [simp]:
     7.5    "fps_conv_radius (-f) = fps_conv_radius f"
     7.6    using fps_conv_radius_cmult_left[of "-1" f]
     7.7 -  by (simp reorient: fps_const_neg)
     7.8 +  by (simp flip: fps_const_neg)
     7.9  
    7.10  lemma fps_conv_radius_add: "fps_conv_radius (f + g) \<ge> min (fps_conv_radius f) (fps_conv_radius g)"
    7.11    unfolding fps_conv_radius_def using conv_radius_add_ge[of "fps_nth f" "fps_nth g"]
     8.1 --- a/src/HOL/Analysis/Gamma_Function.thy	Wed Jun 06 17:18:48 2018 +0200
     8.2 +++ b/src/HOL/Analysis/Gamma_Function.thy	Wed Jun 06 18:20:03 2018 +0200
     8.3 @@ -1148,8 +1148,7 @@
     8.4  lemma Gamma_1 [simp]: "Gamma 1 = 1" unfolding Gamma_def by simp
     8.5  
     8.6  lemma Gamma_fact: "Gamma (1 + of_nat n) = fact n"
     8.7 -  by (simp add: pochhammer_fact pochhammer_Gamma of_nat_in_nonpos_Ints_iff
     8.8 -        reorient: of_nat_Suc)
     8.9 +  by (simp add: pochhammer_fact pochhammer_Gamma of_nat_in_nonpos_Ints_iff flip: of_nat_Suc)
    8.10  
    8.11  lemma Gamma_numeral: "Gamma (numeral n) = fact (pred_numeral n)"
    8.12    by (subst of_nat_numeral[symmetric], subst numeral_eq_Suc,
    8.13 @@ -2430,7 +2429,7 @@
    8.14            inverse ((- 1) ^ n * fact n :: 'a)"
    8.15      by (intro tendsto_intros rGamma_zeros) simp_all
    8.16    also have "inverse ((- 1) ^ n * fact n) = ?c"
    8.17 -    by (simp_all add: field_simps reorient: power_mult_distrib)
    8.18 +    by (simp_all add: field_simps flip: power_mult_distrib)
    8.19    finally show "(\<lambda>z. inverse (rGamma z / (z + of_nat n))) \<midarrow> (- of_nat n) \<rightarrow> ?c" .
    8.20  qed
    8.21  
     9.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Jun 06 17:18:48 2018 +0200
     9.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Jun 06 18:20:03 2018 +0200
     9.3 @@ -772,13 +772,13 @@
     9.4    fixes f :: "_ \<Rightarrow> 'b :: real_normed_field"
     9.5    assumes "f integrable_on s"
     9.6    shows "(\<lambda>x. f x / of_real c) integrable_on s"
     9.7 -by (simp add: integrable_on_cmult_right divide_inverse assms reorient: of_real_inverse)
     9.8 +by (simp add: integrable_on_cmult_right divide_inverse assms flip: of_real_inverse)
     9.9  
    9.10  lemma integrable_on_cdivide_iff [simp]:
    9.11    fixes f :: "_ \<Rightarrow> 'b :: real_normed_field"
    9.12    assumes "c \<noteq> 0"
    9.13    shows "(\<lambda>x. f x / of_real c) integrable_on s \<longleftrightarrow> f integrable_on s"
    9.14 -by (simp add: divide_inverse assms reorient: of_real_inverse)
    9.15 +by (simp add: divide_inverse assms flip: of_real_inverse)
    9.16  
    9.17  lemma has_integral_null [intro]: "content(cbox a b) = 0 \<Longrightarrow> (f has_integral 0) (cbox a b)"
    9.18    unfolding has_integral_cbox
    9.19 @@ -3410,7 +3410,7 @@
    9.20        by (simp add: inner_simps field_simps)
    9.21      ultimately show ?thesis using False
    9.22        by (simp add: image_affinity_cbox content_cbox'
    9.23 -        prod.distrib[symmetric] inner_diff_left reorient: prod_constant)
    9.24 +        prod.distrib[symmetric] inner_diff_left flip: prod_constant)
    9.25    qed
    9.26  qed
    9.27  
    10.1 --- a/src/HOL/Analysis/Interval_Integral.thy	Wed Jun 06 17:18:48 2018 +0200
    10.2 +++ b/src/HOL/Analysis/Interval_Integral.thy	Wed Jun 06 18:20:03 2018 +0200
    10.3 @@ -88,7 +88,7 @@
    10.4    from ereal_incseq_approx[OF this] guess X .
    10.5    then show thesis
    10.6      apply (intro that[of "\<lambda>i. - X i"])
    10.7 -    apply (auto simp: decseq_def incseq_def reorient: uminus_ereal.simps)
    10.8 +    apply (auto simp: decseq_def incseq_def simp flip: uminus_ereal.simps)
    10.9      apply (metis ereal_minus_less_minus ereal_uminus_uminus ereal_Lim_uminus)+
   10.10      done
   10.11  qed
   10.12 @@ -121,7 +121,7 @@
   10.13      fix x i assume "l i \<le> x" "x \<le> u i"
   10.14      with \<open>a < ereal (l i)\<close> \<open>ereal (u i) < b\<close>
   10.15      show "a < ereal x" "ereal x < b"
   10.16 -      by (auto reorient: ereal_less_eq(3))
   10.17 +      by (auto simp flip: ereal_less_eq(3))
   10.18    qed
   10.19    show thesis
   10.20      by (intro that) fact+
   10.21 @@ -283,7 +283,7 @@
   10.22      unfolding interval_lebesgue_integrable_def set_lebesgue_integral_def
   10.23      apply (rule Bochner_Integration.integral_cong [OF refl])
   10.24      by (auto simp: einterval_iff ereal_uminus_le_reorder ereal_uminus_less_reorder not_less
   10.25 -             reorient: uminus_ereal.simps
   10.26 +             simp flip: uminus_ereal.simps
   10.27               split: split_indicator)
   10.28    then show ?case
   10.29      unfolding interval_lebesgue_integral_def 
   10.30 @@ -649,7 +649,7 @@
   10.31      fix i show "set_integrable lborel {l i .. u i} f"
   10.32        using \<open>a < l i\<close> \<open>u i < b\<close> unfolding set_integrable_def
   10.33        by (intro borel_integrable_compact f continuous_at_imp_continuous_on compact_Icc ballI)
   10.34 -         (auto reorient: ereal_less_eq)
   10.35 +         (auto simp flip: ereal_less_eq)
   10.36    qed
   10.37    have 2: "set_borel_measurable lborel (einterval a b) f"
   10.38      unfolding set_borel_measurable_def
    11.1 --- a/src/HOL/Analysis/Lebesgue_Measure.thy	Wed Jun 06 17:18:48 2018 +0200
    11.2 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Wed Jun 06 18:20:03 2018 +0200
    11.3 @@ -283,7 +283,7 @@
    11.4      also have "... \<le> (\<Sum>i\<le>n. F (r i) - F (l i)) + epsilon"
    11.5        using finS Sbound Sprop by (auto intro!: add_right_mono sum_mono2)
    11.6      finally have "ennreal (F b - F a) \<le> (\<Sum>i\<le>n. ennreal (F (r i) - F (l i))) + epsilon"
    11.7 -      using egt0 by (simp add: sum_nonneg reorient: ennreal_plus)
    11.8 +      using egt0 by (simp add: sum_nonneg flip: ennreal_plus)
    11.9      then show "ennreal (F b - F a) \<le> (\<Sum>i. ennreal (F (r i) - F (l i))) + (epsilon :: real)"
   11.10        by (rule order_trans) (auto intro!: add_mono sum_le_suminf simp del: sum_ennreal)
   11.11    qed
    12.1 --- a/src/HOL/Analysis/Measure_Space.thy	Wed Jun 06 17:18:48 2018 +0200
    12.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Wed Jun 06 18:20:03 2018 +0200
    12.3 @@ -1622,7 +1622,7 @@
    12.4      using emeasure_subadditive[OF measurable] fin
    12.5      apply simp
    12.6      apply (subst (asm) (2 3 4) emeasure_eq_ennreal_measure)
    12.7 -    apply (auto reorient: ennreal_plus)
    12.8 +    apply (auto simp flip: ennreal_plus)
    12.9      done
   12.10  qed
   12.11  
    13.1 --- a/src/HOL/Analysis/Regularity.thy	Wed Jun 06 17:18:48 2018 +0200
    13.2 +++ b/src/HOL/Analysis/Regularity.thy	Wed Jun 06 18:20:03 2018 +0200
    13.3 @@ -107,7 +107,7 @@
    13.4      finally have "measure M (space M) \<le> measure M K + e"
    13.5        using \<open>0 < e\<close> by simp
    13.6      hence "emeasure M (space M) \<le> emeasure M K + e"
    13.7 -      using \<open>0 < e\<close> by (simp add: emeasure_eq_measure reorient: ennreal_plus)
    13.8 +      using \<open>0 < e\<close> by (simp add: emeasure_eq_measure flip: ennreal_plus)
    13.9      moreover have "compact K"
   13.10        unfolding compact_eq_totally_bounded
   13.11      proof safe
   13.12 @@ -139,9 +139,9 @@
   13.13        also have "\<dots> \<le> measure M (space M) - measure M K"
   13.14          by (simp add: emeasure_eq_measure sU sb finite_measure_mono)
   13.15        also have "\<dots> \<le> e"
   13.16 -        using K \<open>0 < e\<close> by (simp add: emeasure_eq_measure reorient: ennreal_plus)
   13.17 +        using K \<open>0 < e\<close> by (simp add: emeasure_eq_measure flip: ennreal_plus)
   13.18        finally have "emeasure M A \<le> emeasure M (A \<inter> K) + ennreal e"
   13.19 -        using \<open>0<e\<close> by (simp add: emeasure_eq_measure algebra_simps reorient: ennreal_plus)
   13.20 +        using \<open>0<e\<close> by (simp add: emeasure_eq_measure algebra_simps flip: ennreal_plus)
   13.21        moreover have "A \<inter> K \<subseteq> A" "compact (A \<inter> K)" using \<open>closed A\<close> \<open>compact K\<close> by auto
   13.22        ultimately show "\<exists>K \<subseteq> A. compact K \<and> emeasure M A \<le> emeasure M K + ennreal e"
   13.23          by blast
   13.24 @@ -301,7 +301,7 @@
   13.25        have "measure M (\<Union>i. D i) < (\<Sum>i<n0. measure M (D i)) + e/2" using n0 by simp
   13.26        also have "(\<Sum>i<n0. measure M (D i)) \<le> (\<Sum>i<n0. measure M (K i) + e/(2*Suc n0))"
   13.27          using K \<open>0 < e\<close>
   13.28 -        by (auto intro: sum_mono simp: emeasure_eq_measure reorient: ennreal_plus)
   13.29 +        by (auto intro: sum_mono simp: emeasure_eq_measure simp flip: ennreal_plus)
   13.30        also have "\<dots> = (\<Sum>i<n0. measure M (K i)) + (\<Sum>i<n0. e/(2*Suc n0))"
   13.31          by (simp add: sum.distrib)
   13.32        also have "\<dots> \<le> (\<Sum>i<n0. measure M (K i)) +  e / 2" using \<open>0 < e\<close>
   13.33 @@ -310,7 +310,7 @@
   13.34        have "measure M (\<Union>i. D i) < (\<Sum>i<n0. measure M (K i)) + e / 2 + e / 2"
   13.35          by auto
   13.36        hence "M (\<Union>i. D i) < M ?K + e"
   13.37 -        using \<open>0<e\<close> by (auto simp: mK emeasure_eq_measure sum_nonneg ennreal_less_iff reorient: ennreal_plus)
   13.38 +        using \<open>0<e\<close> by (auto simp: mK emeasure_eq_measure sum_nonneg ennreal_less_iff simp flip: ennreal_plus)
   13.39        moreover
   13.40        have "?K \<subseteq> (\<Union>i. D i)" using K by auto
   13.41        moreover
   13.42 @@ -334,7 +334,7 @@
   13.43            using \<open>0<e\<close>
   13.44            by (auto simp: emeasure_eq_measure sum_nonneg ennreal_less_iff ennreal_minus
   13.45                           finite_measure_mono sb
   13.46 -                   reorient: ennreal_plus)
   13.47 +                   simp flip: ennreal_plus)
   13.48        qed
   13.49        then obtain U where U: "\<And>i. D i \<subseteq> U i" "\<And>i. open (U i)"
   13.50          "\<And>i. e/(2 powr Suc i) > emeasure M (U i) - emeasure M (D i)"
   13.51 @@ -367,7 +367,7 @@
   13.52        also have "\<dots> = ennreal e"
   13.53          by (subst suminf_ennreal_eq[OF zero_le_power power_half_series]) auto
   13.54        finally have "emeasure M ?U \<le> emeasure M (\<Union>i. D i) + ennreal e"
   13.55 -        using \<open>0<e\<close> by (simp add: emeasure_eq_measure reorient: ennreal_plus)
   13.56 +        using \<open>0<e\<close> by (simp add: emeasure_eq_measure flip: ennreal_plus)
   13.57        moreover
   13.58        have "(\<Union>i. D i) \<subseteq> ?U" using U by auto
   13.59        moreover
    14.1 --- a/src/HOL/Analysis/Set_Integral.thy	Wed Jun 06 17:18:48 2018 +0200
    14.2 +++ b/src/HOL/Analysis/Set_Integral.thy	Wed Jun 06 18:20:03 2018 +0200
    14.3 @@ -869,7 +869,7 @@
    14.4      2 * (\<integral>\<^sup>+x. norm(f x) \<partial>M)" by simp
    14.5  
    14.6    have le: "ennreal (norm (F n x - f x)) \<le> ennreal (norm (f x)) + ennreal (norm (F n x))" for n x
    14.7 -    by (simp add: norm_minus_commute norm_triangle_ineq4 ennreal_minus reorient: ennreal_plus)
    14.8 +    by (simp add: norm_minus_commute norm_triangle_ineq4 ennreal_minus flip: ennreal_plus)
    14.9    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
   14.10      by (rule nn_integral_mono)
   14.11  
   14.12 @@ -882,7 +882,7 @@
   14.13    proof (intro arg_cong[where f=liminf] ext)
   14.14      fix n
   14.15      have "\<And>x. ennreal(G n x) = ennreal(norm(f x)) + ennreal(norm(F n x)) - ennreal(norm(F n x - f x))"
   14.16 -      unfolding G_def by (simp add: ennreal_minus reorient: ennreal_plus)
   14.17 +      unfolding G_def by (simp add: ennreal_minus flip: ennreal_plus)
   14.18      moreover have "(\<integral>\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) - ennreal(norm(F n x - f x)) \<partial>M)
   14.19              = (\<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)"
   14.20      proof (rule nn_integral_diff)
    15.1 --- a/src/HOL/Analysis/Sigma_Algebra.thy	Wed Jun 06 17:18:48 2018 +0200
    15.2 +++ b/src/HOL/Analysis/Sigma_Algebra.thy	Wed Jun 06 18:20:03 2018 +0200
    15.3 @@ -2085,7 +2085,7 @@
    15.4    have "(\<lambda>x. g (f x)) \<in> X \<rightarrow> space M" "\<And>A. A \<inter> f -` Y \<inter> X = A \<inter> X"
    15.5      using * by auto
    15.6    with * show "sets ?VV = sets ?V"
    15.7 -    by (simp add: sets_vimage_algebra2 vimage_comp comp_def reorient: ex_simps)
    15.8 +    by (simp add: sets_vimage_algebra2 vimage_comp comp_def flip: ex_simps)
    15.9  qed (simp add: vimage_algebra_def emeasure_sigma)
   15.10  
   15.11  subsubsection \<open>Restricted Space Sigma Algebra\<close>
    16.1 --- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Wed Jun 06 17:18:48 2018 +0200
    16.2 +++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Wed Jun 06 18:20:03 2018 +0200
    16.3 @@ -104,7 +104,7 @@
    16.4          by (simp add: algebra_simps power2_eq_square)
    16.5        have "(\<Sum>k\<le>n. (k - n * x)\<^sup>2 * Bernstein n k x) = n * x * (1 - x)"
    16.6          apply (simp add: * sum.distrib)
    16.7 -        apply (simp add: sum_distrib_left [symmetric] mult.assoc)
    16.8 +        apply (simp flip: sum_distrib_left add: mult.assoc)
    16.9          apply (simp add: algebra_simps power2_eq_square)
   16.10          done
   16.11        then have "(\<Sum>k\<le>n. (k - n * x)\<^sup>2 * Bernstein n k x)/n^2 = x * (1 - x) / n"
   16.12 @@ -383,7 +383,7 @@
   16.13        done
   16.14      also have "... = (1/(k * (p t))^n) * (1 - p t ^ (2*n)) ^ (k^n)"
   16.15        using pt_pos [OF t] \<open>k>0\<close>
   16.16 -      by (simp add: algebra_simps power_mult power2_eq_square power_mult_distrib [symmetric])
   16.17 +      by (simp add: algebra_simps power_mult power2_eq_square flip: power_mult_distrib)
   16.18      also have "... \<le> (1/(k * (p t))^n) * 1"
   16.19        apply (rule mult_left_mono [OF power_le_one])
   16.20        using pt_pos \<open>k>0\<close> p01 power_le_one t apply auto
   16.21 @@ -550,7 +550,7 @@
   16.22      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)"
   16.23  proof (cases "A \<noteq> {} \<and> B \<noteq> {}")
   16.24    case True then show ?thesis
   16.25 -    apply (simp add: ex_in_conv [symmetric])
   16.26 +    apply (simp flip: ex_in_conv)
   16.27      using assms
   16.28      apply safe
   16.29      apply (force simp add: intro!: two_special)
   16.30 @@ -657,7 +657,7 @@
   16.31        using xf01 t by force
   16.32      have "g t = e * (\<Sum>i<j. xf i t) + e * (\<Sum>i=j..n. xf i t)"
   16.33        using j1 jn e
   16.34 -      apply (simp add: g_def distrib_left [symmetric])
   16.35 +      apply (simp add: g_def flip: distrib_left)
   16.36        apply (subst sum.union_disjoint [symmetric])
   16.37        apply (auto simp: ivl_disj_un)
   16.38        done
   16.39 @@ -1147,7 +1147,7 @@
   16.40    show ?thesis
   16.41      apply (subst euclidean_representation_sum_fun [of f, symmetric])
   16.42      apply (rule_tac x="\<lambda>x. \<Sum>b\<in>Basis. pf b x *\<^sub>R b" in exI)
   16.43 -    apply (auto simp: sum_subtractf [symmetric])
   16.44 +    apply (auto simp flip: sum_subtractf)
   16.45      done
   16.46  qed
   16.47  
    17.1 --- a/src/Pure/raw_simplifier.ML	Wed Jun 06 17:18:48 2018 +0200
    17.2 +++ b/src/Pure/raw_simplifier.ML	Wed Jun 06 18:20:03 2018 +0200
    17.3 @@ -90,7 +90,7 @@
    17.4    val prems_of: Proof.context -> thm list
    17.5    val add_simp: thm -> Proof.context -> Proof.context
    17.6    val del_simp: thm -> Proof.context -> Proof.context
    17.7 -  val reorient_simp: thm -> Proof.context -> Proof.context
    17.8 +  val flip_simp: thm -> Proof.context -> Proof.context
    17.9    val init_simpset: thm list -> Proof.context -> Proof.context
   17.10    val add_eqcong: thm -> Proof.context -> Proof.context
   17.11    val del_eqcong: thm -> Proof.context -> Proof.context
   17.12 @@ -463,11 +463,14 @@
   17.13  
   17.14  (* maintain simp rules *)
   17.15  
   17.16 -fun del_rrule (rrule as {thm, elhs, ...}) ctxt =
   17.17 +fun del_rrule loud (rrule as {thm, elhs, ...}) ctxt =
   17.18    ctxt |> map_simpset1 (fn (rules, prems, depth) =>
   17.19      (Net.delete_term eq_rrule (Thm.term_of elhs, rrule) rules, prems, depth))
   17.20    handle Net.DELETE =>
   17.21 -    (cond_warning ctxt (fn () => print_thm ctxt "Rewrite rule not in simpset:" ("", thm)); ctxt);
   17.22 +    (if not loud then ()
   17.23 +     else cond_warning ctxt
   17.24 +            (fn () => print_thm ctxt "Rewrite rule not in simpset:" ("", thm));
   17.25 +     ctxt);
   17.26  
   17.27  fun insert_rrule (rrule as {thm, name, ...}) ctxt =
   17.28   (cond_tracing ctxt (fn () => print_thm ctxt "Adding rewrite rule" (name, thm));
   17.29 @@ -597,11 +600,14 @@
   17.30    comb_simps ctxt insert_rrule (mk_rrule ctxt) true thms;
   17.31  
   17.32  fun ctxt delsimps thms =
   17.33 -  comb_simps ctxt del_rrule (map mk_rrule2 o mk_rrule ctxt) false thms;
   17.34 +  comb_simps ctxt (del_rrule true) (map mk_rrule2 o mk_rrule ctxt) false thms;
   17.35 +
   17.36 +fun delsimps_quiet ctxt thms =
   17.37 +  comb_simps ctxt (del_rrule false) (map mk_rrule2 o mk_rrule ctxt) false thms;
   17.38  
   17.39  fun add_simp thm ctxt = ctxt addsimps [thm];
   17.40  fun del_simp thm ctxt = ctxt delsimps [thm];
   17.41 -fun reorient_simp thm ctxt = addsymsimps (ctxt delsimps [thm]) [thm];
   17.42 +fun flip_simp thm ctxt = addsymsimps (delsimps_quiet ctxt [thm]) [thm];
   17.43  
   17.44  end;
   17.45  
    18.1 --- a/src/Pure/simplifier.ML	Wed Jun 06 17:18:48 2018 +0200
    18.2 +++ b/src/Pure/simplifier.ML	Wed Jun 06 18:20:03 2018 +0200
    18.3 @@ -32,7 +32,7 @@
    18.4    val attrib: (thm -> Proof.context -> Proof.context) -> attribute
    18.5    val simp_add: attribute
    18.6    val simp_del: attribute
    18.7 -  val simp_reorient: attribute
    18.8 +  val simp_flip: attribute
    18.9    val cong_add: attribute
   18.10    val cong_del: attribute
   18.11    val check_simproc: Proof.context -> xstring * Position.T -> string
   18.12 @@ -90,7 +90,7 @@
   18.13  
   18.14  val simp_add = attrib add_simp;
   18.15  val simp_del = attrib del_simp;
   18.16 -val simp_reorient = attrib reorient_simp;
   18.17 +val simp_flip = attrib flip_simp;
   18.18  val cong_add = attrib add_cong;
   18.19  val cong_del = attrib del_cong;
   18.20  
   18.21 @@ -269,7 +269,7 @@
   18.22  (* add / del *)
   18.23  
   18.24  val simpN = "simp";
   18.25 -val reorientN = "reorient"
   18.26 +val flipN = "flip"
   18.27  val congN = "cong";
   18.28  val onlyN = "only";
   18.29  val no_asmN = "no_asm";
   18.30 @@ -343,7 +343,7 @@
   18.31   [Args.$$$ simpN -- Args.colon >> K (Method.modifier simp_add \<^here>),
   18.32    Args.$$$ simpN -- Args.add -- Args.colon >> K (Method.modifier simp_add \<^here>),
   18.33    Args.$$$ simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del \<^here>),
   18.34 -  Args.$$$ reorientN -- Args.colon >> K (Method.modifier simp_reorient \<^here>),
   18.35 +  Args.$$$ simpN -- Args.$$$ flipN -- Args.colon >> K (Method.modifier simp_flip \<^here>),
   18.36    Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >>
   18.37      K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = \<^here>}]
   18.38     @ cong_modifiers;
   18.39 @@ -351,7 +351,7 @@
   18.40  val simp_modifiers' =
   18.41   [Args.add -- Args.colon >> K (Method.modifier simp_add \<^here>),
   18.42    Args.del -- Args.colon >> K (Method.modifier simp_del \<^here>),
   18.43 -  Args.$$$ reorientN -- Args.colon >> K (Method.modifier simp_reorient \<^here>),
   18.44 +  Args.$$$ flipN -- Args.colon >> K (Method.modifier simp_flip \<^here>),
   18.45    Args.$$$ onlyN -- Args.colon >>
   18.46      K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = \<^here>}]
   18.47     @ cong_modifiers;