utilize 'flip'
authornipkow
Thu Jun 07 19:36:12 2018 +0200 (11 months ago)
changeset 684066beb45f6cf67
parent 68405 6a0852b8e5a8
child 68408 9a2453622596
utilize 'flip'
src/HOL/Library/BigO.thy
src/HOL/Library/Cardinality.thy
src/HOL/Library/Countable.thy
src/HOL/Library/Countable_Set_Type.thy
src/HOL/Library/Disjoint_Sets.thy
src/HOL/Library/Extended_Nat.thy
src/HOL/Library/Extended_Nonnegative_Real.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Float.thy
src/HOL/Library/Going_To_Filter.thy
src/HOL/Library/Infinite_Set.thy
src/HOL/Library/Landau_Symbols.thy
src/HOL/Library/Lattice_Algebras.thy
src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy
src/HOL/Library/Log_Nat.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Multiset_Permutations.thy
src/HOL/Library/Periodic_Fun.thy
src/HOL/Library/Perm.thy
src/HOL/Library/Stirling.thy
src/HOL/Library/Stream.thy
src/HOL/Library/Sublist.thy
src/HOL/Library/Uprod.thy
     1.1 --- a/src/HOL/Library/BigO.thy	Thu Jun 07 15:08:18 2018 +0200
     1.2 +++ b/src/HOL/Library/BigO.thy	Thu Jun 07 19:36:12 2018 +0200
     1.3 @@ -188,7 +188,7 @@
     1.4    apply (rule_tac x = "\<bar>c\<bar>" in exI)
     1.5    apply auto
     1.6    apply (drule_tac x = x in spec)+
     1.7 -  apply (simp add: abs_mult [symmetric])
     1.8 +  apply (simp flip: abs_mult)
     1.9    done
    1.10  
    1.11  lemma bigo_bounded: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. f x \<le> g x \<Longrightarrow> f \<in> O(g)"
    1.12 @@ -271,7 +271,7 @@
    1.13    also have "\<dots> = O(\<lambda>x. \<bar>g x\<bar>) + O(\<lambda>x. \<bar>h x\<bar>)"
    1.14      by (rule bigo_plus_eq, auto)
    1.15    finally show ?thesis
    1.16 -    by (simp add: bigo_abs3 [symmetric])
    1.17 +    by (simp flip: bigo_abs3)
    1.18  qed
    1.19  
    1.20  lemma bigo_mult [intro]: "O(f)*O(g) \<subseteq> O(f * g)"
    1.21 @@ -447,7 +447,7 @@
    1.22    for c :: "'a::linordered_field"
    1.23    apply (simp add: bigo_def)
    1.24    apply (rule_tac x = "\<bar>inverse c\<bar>" in exI)
    1.25 -  apply (simp add: abs_mult [symmetric])
    1.26 +  apply (simp flip: abs_mult)
    1.27    done
    1.28  
    1.29  lemma bigo_const4: "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. 1) \<subseteq> O(\<lambda>x. c)"
    1.30 @@ -468,7 +468,7 @@
    1.31  lemma bigo_const_mult1: "(\<lambda>x. c * f x) \<in> O(f)"
    1.32    apply (simp add: bigo_def)
    1.33    apply (rule_tac x = "\<bar>c\<bar>" in exI)
    1.34 -  apply (auto simp add: abs_mult [symmetric])
    1.35 +  apply (auto simp flip: abs_mult)
    1.36    done
    1.37  
    1.38  lemma bigo_const_mult2: "O(\<lambda>x. c * f x) \<subseteq> O(f)"
     2.1 --- a/src/HOL/Library/Cardinality.thy	Thu Jun 07 15:08:18 2018 +0200
     2.2 +++ b/src/HOL/Library/Cardinality.thy	Thu Jun 07 19:36:12 2018 +0200
     2.3 @@ -62,7 +62,7 @@
     2.4  by(simp add: card_UNIV_option)
     2.5  
     2.6  lemma card_UNIV_set: "CARD('a set) = (if CARD('a) = 0 then 0 else 2 ^ CARD('a))"
     2.7 -by(simp add: Pow_UNIV[symmetric] card_eq_0_iff card_Pow del: Pow_UNIV)
     2.8 +by(simp add: card_eq_0_iff card_Pow flip: Pow_UNIV)
     2.9  
    2.10  lemma card_set [simp]: "CARD('a set) = 2 ^ CARD('a::finite)"
    2.11  by(simp add: card_UNIV_set)
    2.12 @@ -267,7 +267,7 @@
    2.13  definition "finite_UNIV = Phantom('a + 'b)
    2.14    (of_phantom (finite_UNIV :: 'a finite_UNIV) \<and> of_phantom (finite_UNIV :: 'b finite_UNIV))"
    2.15  instance
    2.16 -  by intro_classes (simp add: UNIV_Plus_UNIV[symmetric] finite_UNIV_sum_def finite_UNIV del: UNIV_Plus_UNIV)
    2.17 +  by intro_classes (simp add: finite_UNIV_sum_def finite_UNIV)
    2.18  end
    2.19  
    2.20  instantiation sum :: (card_UNIV, card_UNIV) card_UNIV begin
     3.1 --- a/src/HOL/Library/Countable.thy	Thu Jun 07 15:08:18 2018 +0200
     3.2 +++ b/src/HOL/Library/Countable.thy	Thu Jun 07 19:36:12 2018 +0200
     3.3 @@ -101,8 +101,8 @@
     3.4  
     3.5  qualified termination
     3.6  by (relation "measure id")
     3.7 -  (auto simp add: sum_encode_eq [symmetric] prod_encode_eq [symmetric]
     3.8 -    le_imp_less_Suc le_sum_encode_Inl le_sum_encode_Inr
     3.9 +  (auto simp flip: sum_encode_eq prod_encode_eq
    3.10 +    simp: le_imp_less_Suc le_sum_encode_Inl le_sum_encode_Inr
    3.11      le_prod_encode_1 le_prod_encode_2)
    3.12  
    3.13  lemma nth_item_covers: "finite_item x \<Longrightarrow> \<exists>n. nth_item n = x"
     4.1 --- a/src/HOL/Library/Countable_Set_Type.thy	Thu Jun 07 15:08:18 2018 +0200
     4.2 +++ b/src/HOL/Library/Countable_Set_Type.thy	Thu Jun 07 19:36:12 2018 +0200
     4.3 @@ -125,7 +125,7 @@
     4.4  proof -
     4.5    have "rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) (\<lambda>A. UNION A id) (\<lambda>A. cUNION A id)"
     4.6      by transfer_prover
     4.7 -  then show ?thesis by (simp add: cUnion_def [symmetric])
     4.8 +  then show ?thesis by (simp flip: cUnion_def)
     4.9  qed
    4.10  
    4.11  lemmas cset_eqI = set_eqI[Transfer.transferred]
     5.1 --- a/src/HOL/Library/Disjoint_Sets.thy	Thu Jun 07 15:08:18 2018 +0200
     5.2 +++ b/src/HOL/Library/Disjoint_Sets.thy	Thu Jun 07 19:36:12 2018 +0200
     5.3 @@ -55,7 +55,7 @@
     5.4    moreover assume "\<forall>i\<in>I. A i \<in> F i" "\<forall>i\<in>I. B i \<in> F i"
     5.5    ultimately show "(\<Inter>i\<in>I. A i) \<inter> (\<Inter>i\<in>I. B i) = {}"
     5.6      using *[OF \<open>i\<in>I\<close>, THEN disjointD, of "A i" "B i"]
     5.7 -    by (auto simp: INT_Int_distrib[symmetric])
     5.8 +    by (auto simp flip: INT_Int_distrib)
     5.9  qed
    5.10  
    5.11  subsubsection "Family of Disjoint Sets"
     6.1 --- a/src/HOL/Library/Extended_Nat.thy	Thu Jun 07 15:08:18 2018 +0200
     6.2 +++ b/src/HOL/Library/Extended_Nat.thy	Thu Jun 07 19:36:12 2018 +0200
     6.3 @@ -321,7 +321,7 @@
     6.4    by (simp add: eSuc_def split: enat.split)
     6.5  
     6.6  lemma eSuc_minus_1 [simp]: "eSuc n - 1 = n"
     6.7 -  by (simp add: one_enat_def eSuc_enat[symmetric] zero_enat_def[symmetric])
     6.8 +  by (simp add: one_enat_def flip: eSuc_enat zero_enat_def)
     6.9  
    6.10  (*lemmas idiff_self_eq_0_enat = idiff_self_eq_0[unfolded zero_enat_def]*)
    6.11  
     7.1 --- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Thu Jun 07 15:08:18 2018 +0200
     7.2 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Thu Jun 07 19:36:12 2018 +0200
     7.3 @@ -486,10 +486,10 @@
     7.4    by transfer (simp add: top_ereal_def)
     7.5  
     7.6  lemma ennreal_top_neq_one[simp]: "top \<noteq> (1::ennreal)"
     7.7 -  by transfer (simp add: top_ereal_def one_ereal_def ereal_max[symmetric] del: ereal_max)
     7.8 +  by transfer (simp add: top_ereal_def one_ereal_def flip: ereal_max)
     7.9  
    7.10  lemma ennreal_one_neq_top[simp]: "1 \<noteq> (top::ennreal)"
    7.11 -  by transfer (simp add: top_ereal_def one_ereal_def ereal_max[symmetric] del: ereal_max)
    7.12 +  by transfer (simp add: top_ereal_def one_ereal_def flip: ereal_max)
    7.13  
    7.14  lemma ennreal_add_less_top[simp]:
    7.15    fixes a b :: ennreal
    7.16 @@ -636,7 +636,7 @@
    7.17    apply transfer
    7.18    subgoal for a b c
    7.19      apply (cases a b c rule: ereal3_cases)
    7.20 -    apply (auto simp: ereal_max[symmetric] simp del: ereal_max)
    7.21 +    apply (auto simp flip: ereal_max)
    7.22      done
    7.23    done
    7.24  
    7.25 @@ -654,7 +654,7 @@
    7.26    unfolding divide_ennreal_def
    7.27    apply transfer
    7.28    apply (subst mult.assoc)
    7.29 -  apply (simp add: top_ereal_def divide_ereal_def[symmetric])
    7.30 +  apply (simp add: top_ereal_def flip: divide_ereal_def)
    7.31    done
    7.32  
    7.33  lemma divide_mult_eq: "a \<noteq> 0 \<Longrightarrow> a \<noteq> \<infinity> \<Longrightarrow> x * a / (b * a) = x / (b::ennreal)"
    7.34 @@ -672,7 +672,7 @@
    7.35    unfolding divide_ennreal_def
    7.36    apply transfer
    7.37    apply (subst mult.assoc)
    7.38 -  apply (simp add: top_ereal_def divide_ereal_def[symmetric])
    7.39 +  apply (simp add: top_ereal_def flip: divide_ereal_def)
    7.40    done
    7.41  
    7.42  lemma ennreal_add_diff_cancel:
    7.43 @@ -686,7 +686,7 @@
    7.44    apply transfer
    7.45    subgoal for a b
    7.46      apply (cases a b rule: ereal2_cases)
    7.47 -    apply (auto simp: zero_ereal_def ereal_max[symmetric] max.absorb2 simp del: ereal_max)
    7.48 +    apply (auto simp: zero_ereal_def max.absorb2 simp flip: ereal_max)
    7.49      done
    7.50    done
    7.51  
    7.52 @@ -859,7 +859,7 @@
    7.53  lemmas ennreal3_cases = ennreal_cases[case_product ennreal2_cases]
    7.54  
    7.55  lemma ennreal_neq_top[simp]: "ennreal r \<noteq> top"
    7.56 -  by transfer (simp add: top_ereal_def zero_ereal_def ereal_max[symmetric] del: ereal_max)
    7.57 +  by transfer (simp add: top_ereal_def zero_ereal_def flip: ereal_max)
    7.58  
    7.59  lemma top_neq_ennreal[simp]: "top \<noteq> ennreal r"
    7.60    using ennreal_neq_top[of r] by (auto simp del: ennreal_neq_top)
    7.61 @@ -920,16 +920,13 @@
    7.62    by (cases "0 \<le> y") (auto simp: ennreal_eq_0_iff ennreal_neg)
    7.63  
    7.64  lemma ennreal_eq_1[simp]: "ennreal x = 1 \<longleftrightarrow> x = 1"
    7.65 -  by (cases "0 \<le> x")
    7.66 -     (auto simp: ennreal_neg ennreal_1[symmetric] simp del: ennreal_1)
    7.67 +  by (cases "0 \<le> x") (auto simp: ennreal_neg simp flip: ennreal_1)
    7.68  
    7.69  lemma ennreal_le_1[simp]: "ennreal x \<le> 1 \<longleftrightarrow> x \<le> 1"
    7.70 -  by (cases "0 \<le> x")
    7.71 -     (auto simp: ennreal_neg ennreal_1[symmetric] simp del: ennreal_1)
    7.72 +  by (cases "0 \<le> x") (auto simp: ennreal_neg simp flip: ennreal_1)
    7.73  
    7.74  lemma ennreal_ge_1[simp]: "ennreal x \<ge> 1 \<longleftrightarrow> x \<ge> 1"
    7.75 -  by (cases "0 \<le> x")
    7.76 -     (auto simp: ennreal_neg ennreal_1[symmetric] simp del: ennreal_1)
    7.77 +  by (cases "0 \<le> x") (auto simp: ennreal_neg simp flip: ennreal_1)
    7.78  
    7.79  lemma one_less_ennreal[simp]: "1 < ennreal x \<longleftrightarrow> 1 < x"
    7.80    by transfer (auto simp: max.absorb2 less_max_iff_disj)
    7.81 @@ -977,7 +974,7 @@
    7.82  
    7.83  lemma ennreal_minus: "0 \<le> q \<Longrightarrow> ennreal r - ennreal q = ennreal (r - q)"
    7.84    by transfer
    7.85 -     (simp add: max.absorb2 zero_ereal_def ereal_max[symmetric] del: ereal_max)
    7.86 +     (simp add: max.absorb2 zero_ereal_def flip: ereal_max)
    7.87  
    7.88  lemma ennreal_minus_top[simp]: "ennreal a - top = 0"
    7.89    by (simp add: minus_top_ennreal)
    7.90 @@ -1050,8 +1047,7 @@
    7.91    "(\<And>e::real. y < top \<Longrightarrow> 0 < e \<Longrightarrow> x \<le> y + ennreal e) \<Longrightarrow> x \<le> y"
    7.92    apply (cases y rule: ennreal_cases)
    7.93    apply (cases x rule: ennreal_cases)
    7.94 -  apply (auto simp del: ennreal_plus simp add: top_unique ennreal_plus[symmetric]
    7.95 -    intro: zero_less_one field_le_epsilon)
    7.96 +  apply (auto simp flip: ennreal_plus simp add: top_unique intro: zero_less_one field_le_epsilon)
    7.97    done
    7.98  
    7.99  lemma ennreal_rat_dense:
   7.100 @@ -1394,7 +1390,7 @@
   7.101  
   7.102  lemma ennreal_suminf_neq_top: "summable f \<Longrightarrow> (\<And>i. 0 \<le> f i) \<Longrightarrow> (\<Sum>i. ennreal (f i)) \<noteq> top"
   7.103    using sums_ennreal[of f "suminf f"]
   7.104 -  by (simp add: suminf_nonneg sums_unique[symmetric] summable_sums_iff[symmetric] del: sums_ennreal)
   7.105 +  by (simp add: suminf_nonneg flip: sums_unique summable_sums_iff del: sums_ennreal)
   7.106  
   7.107  lemma suminf_ennreal_eq:
   7.108    "(\<And>i. 0 \<le> f i) \<Longrightarrow> f sums x \<Longrightarrow> (\<Sum>i. ennreal (f i)) = ennreal x"
   7.109 @@ -1598,7 +1594,7 @@
   7.110    apply transfer
   7.111    subgoal for A
   7.112      using Inf_countable_INF[of A]
   7.113 -    apply (clarsimp simp add: decseq_def[symmetric])
   7.114 +    apply (clarsimp simp flip: decseq_def)
   7.115      subgoal for f
   7.116        by (intro exI[of _ f]) auto
   7.117      done
   7.118 @@ -1794,19 +1790,17 @@
   7.119  by (auto simp: top_unique)
   7.120  
   7.121  lemma diff_diff_ennreal: fixes a b :: ennreal shows "a \<le> b \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> b - (b - a) = a"
   7.122 -  by (cases a b rule: ennreal2_cases)
   7.123 -     (auto simp: ennreal_minus top_unique)
   7.124 +  by (cases a b rule: ennreal2_cases) (auto simp: ennreal_minus top_unique)
   7.125  
   7.126  lemma ennreal_less_one_iff[simp]: "ennreal x < 1 \<longleftrightarrow> x < 1"
   7.127 -  by (cases "0 \<le> x")
   7.128 -     (auto simp: ennreal_neg ennreal_1[symmetric] ennreal_less_iff simp del: ennreal_1)
   7.129 +  by (cases "0 \<le> x") (auto simp: ennreal_neg ennreal_less_iff simp flip: ennreal_1)
   7.130  
   7.131  lemma SUP_const_minus_ennreal:
   7.132    fixes f :: "'a \<Rightarrow> ennreal" shows "I \<noteq> {} \<Longrightarrow> (SUP x:I. c - f x) = c - (INF x:I. f x)"
   7.133    including ennreal.lifting
   7.134    by (transfer fixing: I)
   7.135 -     (simp add: sup_ereal_def[symmetric] SUP_sup_distrib[symmetric] SUP_ereal_minus_right
   7.136 -           del: sup_ereal_def)
   7.137 +     (simp add: SUP_sup_distrib[symmetric] SUP_ereal_minus_right
   7.138 +           flip: sup_ereal_def)
   7.139  
   7.140  lemma zero_minus_ennreal[simp]: "0 - (a::ennreal) = 0"
   7.141    including ennreal.lifting
   7.142 @@ -1846,10 +1840,8 @@
   7.143  lemma add_diff_le_ennreal: "a + b - c \<le> a + (b - c::ennreal)"
   7.144    apply (cases a b c rule: ennreal3_cases)
   7.145    subgoal for a' b' c'
   7.146 -    by (cases "0 \<le> b' - c'")
   7.147 -       (simp_all add: ennreal_minus ennreal_plus[symmetric] top_add ennreal_neg
   7.148 -                 del: ennreal_plus)
   7.149 -  apply (simp_all add: top_add ennreal_plus[symmetric] del: ennreal_plus)
   7.150 +    by (cases "0 \<le> b' - c'") (simp_all add: ennreal_minus top_add ennreal_neg flip: ennreal_plus)
   7.151 +  apply (simp_all add: top_add flip: ennreal_plus)
   7.152    done
   7.153  
   7.154  lemma diff_eq_0_ennreal: "a < top \<Longrightarrow> a \<le> b \<Longrightarrow> a - b = (0::ennreal)"
   7.155 @@ -1857,14 +1849,14 @@
   7.156  
   7.157  lemma diff_diff_ennreal': fixes x y z :: ennreal shows "z \<le> y \<Longrightarrow> y - z \<le> x \<Longrightarrow> x - (y - z) = x + z - y"
   7.158    by (cases x; cases y; cases z)
   7.159 -     (auto simp add: top_add add_top minus_top_ennreal ennreal_minus ennreal_plus[symmetric] top_unique
   7.160 -           simp del: ennreal_plus)
   7.161 +     (auto simp add: top_add add_top minus_top_ennreal ennreal_minus top_unique
   7.162 +           simp flip: ennreal_plus)
   7.163  
   7.164  lemma diff_diff_ennreal'': fixes x y z :: ennreal
   7.165    shows "z \<le> y \<Longrightarrow> x - (y - z) = (if y - z \<le> x then x + z - y else 0)"
   7.166    by (cases x; cases y; cases z)
   7.167 -     (auto simp add: top_add add_top minus_top_ennreal ennreal_minus ennreal_plus[symmetric] top_unique ennreal_neg
   7.168 -           simp del: ennreal_plus)
   7.169 +     (auto simp add: top_add add_top minus_top_ennreal ennreal_minus top_unique ennreal_neg
   7.170 +           simp flip: ennreal_plus)
   7.171  
   7.172  lemma power_less_top_ennreal: fixes x :: ennreal shows "x ^ n < top \<longleftrightarrow> x < top \<or> n = 0"
   7.173    using power_eq_top_ennreal[of x n] by (auto simp: less_top)
   7.174 @@ -1880,7 +1872,7 @@
   7.175       (auto simp: divide_ennreal ennreal_mult[symmetric] ennreal_less_iff field_simps ennreal_top_mult ennreal_top_divide)
   7.176  
   7.177  lemma one_less_numeral[simp]: "1 < (numeral n::ennreal) \<longleftrightarrow> (num.One < n)"
   7.178 -  by (simp del: ennreal_1 ennreal_numeral add: ennreal_1[symmetric] ennreal_numeral[symmetric] ennreal_less_iff)
   7.179 +  by (simp flip: ennreal_1 ennreal_numeral add: ennreal_less_iff)
   7.180  
   7.181  lemma divide_eq_1_ennreal: "a / b = (1::ennreal) \<longleftrightarrow> (b \<noteq> top \<and> b \<noteq> 0 \<and> b = a)"
   7.182    by (cases a ; cases b; cases "b = 0") (auto simp: ennreal_top_divide divide_ennreal split: if_split_asm)
   7.183 @@ -1902,17 +1894,16 @@
   7.184  
   7.185  lemma ennreal_minus_le_iff: "a - b \<le> c \<longleftrightarrow> (a \<le> b + (c::ennreal) \<and> (a = top \<and> b = top \<longrightarrow> c = top))"
   7.186    by (cases a; cases b; cases c)
   7.187 -     (auto simp: top_unique top_add add_top ennreal_minus ennreal_plus[symmetric]
   7.188 -           simp del: ennreal_plus)
   7.189 +     (auto simp: top_unique top_add add_top ennreal_minus simp flip: ennreal_plus)
   7.190  
   7.191  lemma ennreal_le_minus_iff: "a \<le> b - c \<longleftrightarrow> (a + c \<le> (b::ennreal) \<or> (a = 0 \<and> b \<le> c))"
   7.192    by (cases a; cases b; cases c)
   7.193 -     (auto simp: top_unique top_add add_top ennreal_minus ennreal_plus[symmetric] ennreal_le_iff2
   7.194 -           simp del: ennreal_plus)
   7.195 +     (auto simp: top_unique top_add add_top ennreal_minus ennreal_le_iff2
   7.196 +           simp flip: ennreal_plus)
   7.197  
   7.198  lemma diff_add_eq_diff_diff_swap_ennreal: "x - (y + z :: ennreal) = x - y - z"
   7.199    by (cases x; cases y; cases z)
   7.200 -     (auto simp: ennreal_plus[symmetric] ennreal_minus_if add_top top_add simp del: ennreal_plus)
   7.201 +     (auto simp: ennreal_minus_if add_top top_add simp flip: ennreal_plus)
   7.202  
   7.203  lemma diff_add_assoc2_ennreal: "b \<le> a \<Longrightarrow> (a - b + c::ennreal) = a + c - b"
   7.204    by (cases a; cases b; cases c)
     8.1 --- a/src/HOL/Library/Extended_Real.thy	Thu Jun 07 15:08:18 2018 +0200
     8.2 +++ b/src/HOL/Library/Extended_Real.thy	Thu Jun 07 19:36:12 2018 +0200
     8.3 @@ -174,7 +174,7 @@
     8.4      then obtain n m where "{enat n<..} \<subseteq> A" "{enat m<..} \<subseteq> B"
     8.5        by auto
     8.6      then have "{enat (max n m) <..} \<subseteq> A \<inter> B"
     8.7 -      by (auto simp add: subset_eq Ball_def max_def enat_ord_code(1)[symmetric] simp del: enat_ord_code(1))
     8.8 +      by (auto simp add: subset_eq Ball_def max_def simp flip: enat_ord_code(1))
     8.9      then show ?case
    8.10        by auto
    8.11    next
    8.12 @@ -415,7 +415,7 @@
    8.13  
    8.14  lemma ereal_0_plus [simp]: "ereal 0 + x = x"
    8.15    and plus_ereal_0 [simp]: "x + ereal 0 = x"
    8.16 -by(simp_all add: zero_ereal_def[symmetric])
    8.17 +by(simp_all flip: zero_ereal_def)
    8.18  
    8.19  instance ereal :: numeral ..
    8.20  
    8.21 @@ -939,7 +939,7 @@
    8.22  lemma [simp]:
    8.23    shows ereal_1_times: "ereal 1 * x = x"
    8.24    and times_ereal_1: "x * ereal 1 = x"
    8.25 -by(simp_all add: one_ereal_def[symmetric])
    8.26 +by(simp_all flip: one_ereal_def)
    8.27  
    8.28  lemma one_not_le_zero_ereal[simp]: "\<not> (1 \<le> (0::ereal))"
    8.29    by (simp add: one_ereal_def zero_ereal_def)
    8.30 @@ -2117,7 +2117,7 @@
    8.31    obtain r where r: "ereal r = (SUP a:A. ereal a)" "A \<noteq> {}"
    8.32      using * by (force simp: bot_ereal_def)
    8.33    then show "bdd_above A" "A \<noteq> {}"
    8.34 -    by (auto intro!: SUP_upper bdd_aboveI[of _ r] simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
    8.35 +    by (auto intro!: SUP_upper bdd_aboveI[of _ r] simp flip: ereal_less_eq)
    8.36  qed (auto simp: mono_def continuous_at_imp_continuous_at_within continuous_at_ereal)
    8.37  
    8.38  lemma ereal_SUP: "\<bar>SUP a:A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (SUP a:A. f a) = (SUP a:A. ereal (f a))"
    8.39 @@ -2130,7 +2130,7 @@
    8.40    obtain r where r: "ereal r = (INF a:A. ereal a)" "A \<noteq> {}"
    8.41      using * by (force simp: top_ereal_def)
    8.42    then show "bdd_below A" "A \<noteq> {}"
    8.43 -    by (auto intro!: INF_lower bdd_belowI[of _ r] simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
    8.44 +    by (auto intro!: INF_lower bdd_belowI[of _ r] simp flip: ereal_less_eq)
    8.45  qed (auto simp: mono_def continuous_at_imp_continuous_at_within continuous_at_ereal)
    8.46  
    8.47  lemma ereal_Inf':
    8.48 @@ -2527,13 +2527,13 @@
    8.49    by (cases n) auto
    8.50  
    8.51  lemma ereal_of_enat_ge_zero_cancel_iff[simp]: "0 \<le> ereal_of_enat n \<longleftrightarrow> 0 \<le> n"
    8.52 -  by (cases n) (auto simp: enat_0[symmetric])
    8.53 +  by (cases n) (auto simp flip: enat_0)
    8.54  
    8.55  lemma ereal_of_enat_gt_zero_cancel_iff[simp]: "0 < ereal_of_enat n \<longleftrightarrow> 0 < n"
    8.56 -  by (cases n) (auto simp: enat_0[symmetric])
    8.57 +  by (cases n) (auto simp flip: enat_0)
    8.58  
    8.59  lemma ereal_of_enat_zero[simp]: "ereal_of_enat 0 = 0"
    8.60 -  by (auto simp: enat_0[symmetric])
    8.61 +  by (auto simp flip: enat_0)
    8.62  
    8.63  lemma ereal_of_enat_inf[simp]: "ereal_of_enat n = \<infinity> \<longleftrightarrow> n = \<infinity>"
    8.64    by (cases n) auto
    8.65 @@ -3639,7 +3639,7 @@
    8.66    by (metis sums_ereal sums_unique summable_def)
    8.67  
    8.68  lemma suminf_ereal_finite: "summable f \<Longrightarrow> (\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
    8.69 -  by (auto simp: sums_ereal[symmetric] summable_def sums_unique[symmetric])
    8.70 +  by (auto simp: summable_def simp flip: sums_ereal sums_unique)
    8.71  
    8.72  lemma suminf_ereal_finite_neg:
    8.73    assumes "summable f"
    8.74 @@ -3779,8 +3779,8 @@
    8.75      apply auto
    8.76      done
    8.77    also have "(\<lambda>x. inverse m * (x + -t)) -` S = (\<lambda>x. (x - t) / m) -` S"
    8.78 -    using m t by (auto simp: divide_ereal_def mult.commute uminus_ereal.simps[symmetric] minus_ereal_def
    8.79 -                       simp del: uminus_ereal.simps)
    8.80 +    using m t by (auto simp: divide_ereal_def mult.commute minus_ereal_def
    8.81 +                       simp flip: uminus_ereal.simps)
    8.82    also have "(\<lambda>x. (x - t) / m) -` S = (\<lambda>x. m * x + t) ` S"
    8.83      using m t
    8.84      by (simp add: set_eq_iff image_iff)
    8.85 @@ -4252,7 +4252,7 @@
    8.86    by (cases rule: ereal2_cases[of a b]) auto
    8.87  
    8.88  lemma minus_ereal_0 [simp]: "x - ereal 0 = x"
    8.89 -by(simp add: zero_ereal_def[symmetric])
    8.90 +by(simp flip: zero_ereal_def)
    8.91  
    8.92  lemma ereal_diff_eq_0_iff: fixes a b :: ereal
    8.93    shows "(\<bar>a\<bar> = \<infinity> \<Longrightarrow> \<bar>b\<bar> \<noteq> \<infinity>) \<Longrightarrow> a - b = 0 \<longleftrightarrow> a = b"
     9.1 --- a/src/HOL/Library/Float.thy	Thu Jun 07 15:08:18 2018 +0200
     9.2 +++ b/src/HOL/Library/Float.thy	Thu Jun 07 19:36:12 2018 +0200
     9.3 @@ -82,7 +82,7 @@
     9.4      if "e1 \<le> e2" for e1 m1 e2 m2 :: int
     9.5    proof -
     9.6      from that have "m1 * 2 powr e1 + m2 * 2 powr e2 = (m1 + m2 * 2 ^ nat (e2 - e1)) * 2 powr e1"
     9.7 -      by (simp add: powr_realpow[symmetric] powr_diff field_simps)
     9.8 +      by (simp add: powr_diff field_simps flip: powr_realpow)
     9.9      then show ?thesis
    9.10        by blast
    9.11    qed
    9.12 @@ -132,7 +132,7 @@
    9.13    apply (rename_tac m e)
    9.14    apply (rule_tac x="m" in exI)
    9.15    apply (rule_tac x="e - d" in exI)
    9.16 -  apply (simp add: powr_realpow[symmetric] field_simps powr_add[symmetric])
    9.17 +  apply (simp flip: powr_realpow powr_add add: field_simps)
    9.18    done
    9.19  
    9.20  lemma div_power_2_int_float[simp]: "x \<in> float \<Longrightarrow> x / (2::int)^d \<in> float"
    9.21 @@ -141,7 +141,7 @@
    9.22    apply (rename_tac m e)
    9.23    apply (rule_tac x="m" in exI)
    9.24    apply (rule_tac x="e - d" in exI)
    9.25 -  apply (simp add: powr_realpow[symmetric] field_simps powr_add[symmetric])
    9.26 +  apply (simp flip: powr_realpow powr_add add: field_simps)
    9.27    done
    9.28  
    9.29  lemma div_numeral_Bit0_float[simp]:
    9.30 @@ -549,7 +549,7 @@
    9.31      then have "2 powr (exponent f - e) = 2 powr - real_of_int (e - exponent f)"
    9.32        by simp
    9.33      also have "\<dots> = 1 / 2^nat (e - exponent f)"
    9.34 -      using pos by (simp add: powr_realpow[symmetric] powr_diff)
    9.35 +      using pos by (simp flip: powr_realpow add: powr_diff)
    9.36      finally have "m * 2^nat (e - exponent f) = real_of_int (mantissa f)"
    9.37        using eq by simp
    9.38      then have "mantissa f = m * 2^nat (e - exponent f)"
    9.39 @@ -562,7 +562,7 @@
    9.40      then show False using mantissa_not_dvd[OF not_0] by simp
    9.41    qed
    9.42    ultimately have "real_of_int m = mantissa f * 2^nat (exponent f - e)"
    9.43 -    by (simp add: powr_realpow[symmetric])
    9.44 +    by (simp flip: powr_realpow)
    9.45    with \<open>e \<le> exponent f\<close>
    9.46    show "m = mantissa f * 2 ^ nat (exponent f - e)"
    9.47      by linarith
    9.48 @@ -662,11 +662,11 @@
    9.49  
    9.50  lemma round_down_float[simp]: "round_down prec x \<in> float"
    9.51    unfolding round_down_def
    9.52 -  by (auto intro!: times_float simp: of_int_minus[symmetric] simp del: of_int_minus)
    9.53 +  by (auto intro!: times_float simp flip: of_int_minus)
    9.54  
    9.55  lemma round_up_float[simp]: "round_up prec x \<in> float"
    9.56    unfolding round_up_def
    9.57 -  by (auto intro!: times_float simp: of_int_minus[symmetric] simp del: of_int_minus)
    9.58 +  by (auto intro!: times_float simp flip: of_int_minus)
    9.59  
    9.60  lemma round_up: "x \<le> round_up prec x"
    9.61    by (simp add: powr_minus_divide le_divide_eq round_up_def ceiling_correct)
    9.62 @@ -686,19 +686,19 @@
    9.63      by (simp add: round_up_def round_down_def field_simps)
    9.64    also have "\<dots> \<le> 1 * 2 powr -prec"
    9.65      by (rule mult_mono)
    9.66 -      (auto simp del: of_int_diff simp: of_int_diff[symmetric] ceiling_diff_floor_le_1)
    9.67 +      (auto simp flip: of_int_diff simp: ceiling_diff_floor_le_1)
    9.68    finally show ?thesis by simp
    9.69  qed
    9.70  
    9.71  lemma round_down_shift: "round_down p (x * 2 powr k) = 2 powr k * round_down (p + k) x"
    9.72    unfolding round_down_def
    9.73    by (simp add: powr_add powr_mult field_simps powr_diff)
    9.74 -    (simp add: powr_add[symmetric])
    9.75 +    (simp flip: powr_add)
    9.76  
    9.77  lemma round_up_shift: "round_up p (x * 2 powr k) = 2 powr k * round_up (p + k) x"
    9.78    unfolding round_up_def
    9.79    by (simp add: powr_add powr_mult field_simps powr_diff)
    9.80 -    (simp add: powr_add[symmetric])
    9.81 +    (simp flip: powr_add)
    9.82  
    9.83  lemma round_up_uminus_eq: "round_up p (-x) = - round_down p x"
    9.84    and round_down_uminus_eq: "round_down p (-x) = - round_up p x"
    9.85 @@ -831,7 +831,7 @@
    9.86    finally show ?thesis
    9.87      using \<open>p + e < 0\<close>
    9.88      apply transfer
    9.89 -    apply (simp add: ac_simps round_down_def floor_divide_of_int_eq[symmetric])
    9.90 +    apply (simp add: ac_simps round_down_def flip: floor_divide_of_int_eq)
    9.91      proof - (*FIXME*)
    9.92        fix pa :: int and ea :: int and ma :: int
    9.93        assume a1: "2 ^ nat (- pa - ea) = 1 / (2 powr real_of_int pa * 2 powr real_of_int ea)"
    9.94 @@ -871,8 +871,8 @@
    9.95  proof (cases "b dvd a")
    9.96    case True
    9.97    then show ?thesis
    9.98 -    by (simp add: ceiling_def of_int_minus[symmetric] divide_minus_left[symmetric]
    9.99 -      floor_divide_of_int_eq dvd_neg_div del: divide_minus_left of_int_minus)
   9.100 +    by (simp add: ceiling_def floor_divide_of_int_eq dvd_neg_div
   9.101 +             flip: of_int_minus divide_minus_left)
   9.102  next
   9.103    case False
   9.104    then have "a mod b \<noteq> 0"
   9.105 @@ -881,7 +881,7 @@
   9.106      using \<open>b \<noteq> 0\<close> by auto
   9.107    have "\<lceil>real_of_int a / real_of_int b\<rceil> = \<lfloor>real_of_int a / real_of_int b\<rfloor> + 1"
   9.108      apply (rule ceiling_eq)
   9.109 -    apply (auto simp: floor_divide_of_int_eq[symmetric])
   9.110 +    apply (auto simp flip: floor_divide_of_int_eq)
   9.111    proof -
   9.112      have "real_of_int \<lfloor>real_of_int a / real_of_int b\<rfloor> \<le> real_of_int a / real_of_int b"
   9.113        by simp
   9.114 @@ -1207,7 +1207,7 @@
   9.115      have "int x * 2 ^ nat l = x'"
   9.116        by (simp add: x'_def)
   9.117      moreover have "real x * 2 powr l = real x'"
   9.118 -      by (simp add: powr_realpow[symmetric] \<open>0 \<le> l\<close> x'_def)
   9.119 +      by (simp flip: powr_realpow add: \<open>0 \<le> l\<close> x'_def)
   9.120      ultimately show ?thesis
   9.121        using ceil_divide_floor_conv[of y x'] powr_realpow[of 2 "nat l"] \<open>0 \<le> l\<close> \<open>y \<noteq> 0\<close>
   9.122          l_def[symmetric, THEN meta_eq_to_obj_eq]
   9.123 @@ -1223,7 +1223,7 @@
   9.124      have "int y * 2 ^ nat (- l) = y'"
   9.125        by (simp add: y'_def)
   9.126      moreover have "real x * real_of_int (2::int) powr real_of_int l / real y = x / real y'"
   9.127 -      using \<open>\<not> 0 \<le> l\<close> by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps)
   9.128 +      using \<open>\<not> 0 \<le> l\<close> by (simp flip: powr_realpow add: powr_minus y'_def field_simps)
   9.129      ultimately show ?thesis
   9.130        using ceil_divide_floor_conv[of y' x] \<open>\<not> 0 \<le> l\<close> \<open>y' \<noteq> 0\<close> \<open>y \<noteq> 0\<close>
   9.131          l_def[symmetric, THEN meta_eq_to_obj_eq]
   9.132 @@ -1389,7 +1389,7 @@
   9.133      from that 2 have "(power_down p x (Suc n div 2)) ^ 2 \<le> (x ^ (Suc n div 2)) ^ 2"
   9.134        by (auto intro: power_mono power_down_nonneg simp del: odd_Suc_div_two)
   9.135      also have "\<dots> = x ^ (Suc n div 2 * 2)"
   9.136 -      by (simp add: power_mult[symmetric])
   9.137 +      by (simp flip: power_mult)
   9.138      also have "Suc n div 2 * 2 = Suc n"
   9.139        using \<open>odd n\<close> by presburger
   9.140      finally show ?thesis
   9.141 @@ -1407,7 +1407,7 @@
   9.142      from that even_Suc have "Suc n = Suc n div 2 * 2"
   9.143        by presburger
   9.144      then have "x ^ Suc n \<le> (x ^ (Suc n div 2))\<^sup>2"
   9.145 -      by (simp add: power_mult[symmetric])
   9.146 +      by (simp flip: power_mult)
   9.147      also from that 2 have "\<dots> \<le> (power_up p x (Suc n div 2))\<^sup>2"
   9.148        by (auto intro: power_mono simp del: odd_Suc_div_two)
   9.149      finally show ?thesis
   9.150 @@ -1506,7 +1506,7 @@
   9.151    proof cases
   9.152      case 1
   9.153      then show ?thesis
   9.154 -      by (simp add: assms(1)[symmetric] powr_add[symmetric] algebra_simps powr_mult_base)
   9.155 +      by (simp flip: assms(1) powr_add add: algebra_simps powr_mult_base)
   9.156    next
   9.157      case 2
   9.158      then have "b * 2 powr p < \<bar>b * 2 powr (p + 1)\<bar>"
   9.159 @@ -1518,12 +1518,12 @@
   9.160        by (simp_all add: floor_eq_iff)
   9.161  
   9.162      have "\<lfloor>(a + b) * 2 powr q\<rfloor> = \<lfloor>(a + b) * 2 powr p * 2 powr (q - p)\<rfloor>"
   9.163 -      by (simp add: algebra_simps powr_realpow[symmetric] powr_add[symmetric])
   9.164 +      by (simp add: algebra_simps flip: powr_realpow powr_add)
   9.165      also have "\<dots> = \<lfloor>(ai + b * 2 powr p) * 2 powr (q - p)\<rfloor>"
   9.166        by (simp add: assms algebra_simps)
   9.167      also have "\<dots> = \<lfloor>(ai + b * 2 powr p) / real_of_int ((2::int) ^ nat (p - q))\<rfloor>"
   9.168        using assms
   9.169 -      by (simp add: algebra_simps powr_realpow[symmetric] divide_powr_uminus powr_add[symmetric])
   9.170 +      by (simp add: algebra_simps divide_powr_uminus flip: powr_realpow powr_add)
   9.171      also have "\<dots> = \<lfloor>ai / real_of_int ((2::int) ^ nat (p - q))\<rfloor>"
   9.172        by (simp del: of_int_power add: floor_divide_real_eq_div floor_eq)
   9.173      finally have "\<lfloor>(a + b) * 2 powr real_of_int q\<rfloor> = \<lfloor>real_of_int ai / real_of_int ((2::int) ^ nat (p - q))\<rfloor>" .
   9.174 @@ -1534,7 +1534,7 @@
   9.175        have "\<lfloor>(2 * ai + sgn b) * 2 powr (real_of_int (q - p) - 1)\<rfloor> = \<lfloor>(ai + sgn b / 2) * 2 powr (q - p)\<rfloor>"
   9.176          by (subst powr_diff) (simp add: field_simps)
   9.177        also have "\<dots> = \<lfloor>(ai + sgn b / 2) / real_of_int ((2::int) ^ nat (p - q))\<rfloor>"
   9.178 -        using leqp by (simp add: powr_realpow[symmetric] powr_diff)
   9.179 +        using leqp by (simp flip: powr_realpow add: powr_diff)
   9.180        also have "\<dots> = \<lfloor>ai / real_of_int ((2::int) ^ nat (p - q))\<rfloor>"
   9.181          by (simp del: of_int_power add: floor_divide_real_eq_div floor_eq)
   9.182        finally show ?thesis .
   9.183 @@ -1547,19 +1547,19 @@
   9.184        by (auto simp: floor_eq_iff algebra_simps pos_divide_le_eq[symmetric] abs_if divide_powr_uminus
   9.185          intro!: mult_neg_pos split: if_split_asm)
   9.186      have "\<lfloor>(a + b) * 2 powr q\<rfloor> = \<lfloor>(2*a + 2*b) * 2 powr p * 2 powr (q - p - 1)\<rfloor>"
   9.187 -      by (simp add: algebra_simps powr_realpow[symmetric] powr_add[symmetric] powr_mult_base)
   9.188 +      by (simp add: algebra_simps powr_mult_base flip: powr_realpow powr_add)
   9.189      also have "\<dots> = \<lfloor>(2 * (a * 2 powr p) + 2 * b * 2 powr p) * 2 powr (q - p - 1)\<rfloor>"
   9.190        by (simp add: algebra_simps)
   9.191      also have "\<dots> = \<lfloor>(2 * ai + b * 2 powr (p + 1)) / 2 powr (1 - q + p)\<rfloor>"
   9.192        using assms by (simp add: algebra_simps powr_mult_base divide_powr_uminus)
   9.193      also have "\<dots> = \<lfloor>(2 * ai + b * 2 powr (p + 1)) / real_of_int ((2::int) ^ nat (p - q + 1))\<rfloor>"
   9.194 -      using assms by (simp add: algebra_simps powr_realpow[symmetric])
   9.195 +      using assms by (simp add: algebra_simps flip: powr_realpow)
   9.196      also have "\<dots> = \<lfloor>(2 * ai - 1) / real_of_int ((2::int) ^ nat (p - q + 1))\<rfloor>"
   9.197        using \<open>b < 0\<close> assms
   9.198        by (simp add: floor_divide_of_int_eq floor_eq floor_divide_real_eq_div
   9.199          del: of_int_mult of_int_power of_int_diff)
   9.200      also have "\<dots> = \<lfloor>(2 * ai - 1) * 2 powr (q - p - 1)\<rfloor>"
   9.201 -      using assms by (simp add: algebra_simps divide_powr_uminus powr_realpow[symmetric])
   9.202 +      using assms by (simp add: algebra_simps divide_powr_uminus flip: powr_realpow)
   9.203      finally show ?thesis
   9.204        using \<open>b < 0\<close> by simp
   9.205    qed
   9.206 @@ -1595,7 +1595,7 @@
   9.207        (metis of_int_1 of_int_add of_int_le_numeral_power_cancel_iff)
   9.208  
   9.209    have "\<bar>ai\<bar> = 2 powr k + r"
   9.210 -    using \<open>k \<ge> 0\<close> by (auto simp: k_def r_def powr_realpow[symmetric])
   9.211 +    using \<open>k \<ge> 0\<close> by (auto simp: k_def r_def simp flip: powr_realpow)
   9.212  
   9.213    have pos: "\<bar>b\<bar> < 1 \<Longrightarrow> 0 < 2 powr k + (r + b)" for b :: real
   9.214      using \<open>0 \<le> k\<close> \<open>ai \<noteq> 0\<close>
   9.215 @@ -1664,8 +1664,7 @@
   9.216    let ?e = "e1 - int k1 - 1"
   9.217  
   9.218    have sum_eq: "?sum = (?m1 + ?m2) * 2 powr ?e"
   9.219 -    by (auto simp: powr_add[symmetric] powr_mult[symmetric] algebra_simps
   9.220 -      powr_realpow[symmetric] powr_mult_base)
   9.221 +    by (auto simp flip: powr_add powr_mult powr_realpow simp: powr_mult_base algebra_simps)
   9.222  
   9.223    have "\<bar>?m2\<bar> * 2 < 2 powr (bitlen \<bar>m2\<bar> + ?shift + 1)"
   9.224      by (auto simp: field_simps powr_add powr_mult_base powr_diff abs_mult)
   9.225 @@ -1753,7 +1752,7 @@
   9.226        by (auto simp add: sgn_if zero_less_mult_iff simp del: powr_gt_zero)
   9.227      also have "\<lfloor>(real_of_int (2 * ?m1) + real_of_int (sgn m2)) * 2 powr real_of_int (?f - - ?e - 1)\<rfloor> =
   9.228          \<lfloor>Float (?m1 * 2 + sgn m2) (?e - 1) * 2 powr ?f\<rfloor>"
   9.229 -      by (simp add: powr_add[symmetric] algebra_simps powr_realpow[symmetric])
   9.230 +      by (simp flip: powr_add powr_realpow add: algebra_simps)
   9.231      finally
   9.232      show "\<lfloor>(?a + ?b) * 2 powr ?f\<rfloor> = \<lfloor>real_of_float (Float (?m1 * 2 + sgn m2) (?e - 1)) * 2 powr ?f\<rfloor>" .
   9.233    qed
   9.234 @@ -1983,7 +1982,7 @@
   9.235        have "x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor>) \<le>
   9.236          x * (2 powr real (Suc prec) / (2 powr log 2 x))"
   9.237          using real_of_int_floor_add_one_ge[of "log 2 x"] assms
   9.238 -        by (auto simp add: algebra_simps powr_diff [symmetric]  intro!: mult_left_mono)
   9.239 +        by (auto simp: algebra_simps simp flip: powr_diff intro!: mult_left_mono)
   9.240        then show "x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor>) \<le> real_of_int ((2::int) ^ (Suc prec))"
   9.241          using \<open>0 < x\<close> by (simp add: powr_realpow powr_add)
   9.242      qed
   9.243 @@ -2080,14 +2079,13 @@
   9.244        have "x = 2 powr (log 2 \<bar>x\<bar>)" using \<open>0 < x\<close> by simp
   9.245        also have "\<dots> \<le> (2 ^ (Suc prec )) * 2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor>)"
   9.246          using real_of_int_floor_add_one_ge[of "log 2 \<bar>x\<bar>"] \<open>0 < x\<close>
   9.247 -        by (auto simp: powr_realpow[symmetric] powr_add[symmetric] algebra_simps
   9.248 -          powr_mult_base le_powr_iff)
   9.249 +        by (auto simp flip: powr_realpow powr_add simp: algebra_simps powr_mult_base le_powr_iff)
   9.250        also
   9.251        have "2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor>) \<le> 2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor> + 1)"
   9.252          using logless flogless \<open>x > 0\<close> \<open>y > 0\<close>
   9.253          by (auto intro!: floor_mono)
   9.254        finally show ?thesis
   9.255 -        by (auto simp: powr_realpow[symmetric] powr_diff assms of_nat_diff)
   9.256 +        by (auto simp flip: powr_realpow simp: powr_diff assms of_nat_diff)
   9.257      qed
   9.258      ultimately show ?thesis
   9.259        by (metis dual_order.trans truncate_down)
   9.260 @@ -2170,12 +2168,12 @@
   9.261  lemma compute_mantissa[code]:
   9.262    "mantissa (Float m e) =
   9.263      (if m = 0 then 0 else if 2 dvd m then mantissa (normfloat (Float m e)) else m)"
   9.264 -  by (auto simp: mantissa_float Float.abs_eq zero_float_def[symmetric])
   9.265 +  by (auto simp: mantissa_float Float.abs_eq simp flip: zero_float_def)
   9.266  
   9.267  lemma compute_exponent[code]:
   9.268    "exponent (Float m e) =
   9.269      (if m = 0 then 0 else if 2 dvd m then exponent (normfloat (Float m e)) else e)"
   9.270 -  by (auto simp: exponent_float Float.abs_eq zero_float_def[symmetric])
   9.271 +  by (auto simp: exponent_float Float.abs_eq simp flip: zero_float_def)
   9.272  
   9.273  lifting_update Float.float.lifting
   9.274  lifting_forget Float.float.lifting
    10.1 --- a/src/HOL/Library/Going_To_Filter.thy	Thu Jun 07 15:08:18 2018 +0200
    10.2 +++ b/src/HOL/Library/Going_To_Filter.thy	Thu Jun 07 19:36:12 2018 +0200
    10.3 @@ -80,7 +80,7 @@
    10.4  
    10.5  lemma going_to_within_union [simp]: 
    10.6    "f going_to F within (A \<union> B) = sup (f going_to F within A) (f going_to F within B)"
    10.7 -  by (simp add: going_to_within_def inf_sup_distrib1 [symmetric])
    10.8 +  by (simp add: going_to_within_def flip: inf_sup_distrib1)
    10.9  
   10.10  lemma eventually_going_to_at_top_linorder:
   10.11    fixes f :: "'a \<Rightarrow> 'b :: linorder"
    11.1 --- a/src/HOL/Library/Infinite_Set.thy	Thu Jun 07 15:08:18 2018 +0200
    11.2 +++ b/src/HOL/Library/Infinite_Set.thy	Thu Jun 07 19:36:12 2018 +0200
    11.3 @@ -68,7 +68,7 @@
    11.4    have "inj_on nat (abs ` A)" for A
    11.5      by (rule inj_onI) auto
    11.6    then show ?thesis
    11.7 -    by (auto simp add: image_comp [symmetric] dest: finite_image_absD finite_imageD)
    11.8 +    by (auto simp flip: image_comp dest: finite_image_absD finite_imageD)
    11.9  qed
   11.10  
   11.11  proposition infinite_int_iff_unbounded_le: "infinite S \<longleftrightarrow> (\<forall>m. \<exists>n. \<bar>n\<bar> \<ge> m \<and> n \<in> S)"
   11.12 @@ -161,11 +161,11 @@
   11.13  
   11.14  lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P n) \<longleftrightarrow> (\<exists>m. \<forall>n>m. P n)"
   11.15    for P :: "nat \<Rightarrow> bool"
   11.16 -  by (auto simp add: eventually_cofinite finite_nat_iff_bounded_le subset_eq not_le[symmetric])
   11.17 +  by (auto simp add: eventually_cofinite finite_nat_iff_bounded_le subset_eq simp flip: not_le)
   11.18  
   11.19  lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P n) \<longleftrightarrow> (\<exists>m. \<forall>n\<ge>m. P n)"
   11.20    for P :: "nat \<Rightarrow> bool"
   11.21 -  by (auto simp add: eventually_cofinite finite_nat_iff_bounded subset_eq not_le[symmetric])
   11.22 +  by (auto simp add: eventually_cofinite finite_nat_iff_bounded subset_eq simp flip: not_le)
   11.23  
   11.24  lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P n) \<longleftrightarrow> (\<forall>m. \<exists>n>m. P n)"
   11.25    for P :: "nat \<Rightarrow> bool"
   11.26 @@ -286,7 +286,7 @@
   11.27      apply (subst Suc)
   11.28       apply (use \<open>infinite S\<close> in simp)
   11.29      apply (intro arg_cong[where f = Least] ext)
   11.30 -    apply (auto simp: enumerate_Suc'[symmetric])
   11.31 +    apply (auto simp flip: enumerate_Suc')
   11.32      done
   11.33  qed
   11.34  
    12.1 --- a/src/HOL/Library/Landau_Symbols.thy	Thu Jun 07 15:08:18 2018 +0200
    12.2 +++ b/src/HOL/Library/Landau_Symbols.thy	Thu Jun 07 19:36:12 2018 +0200
    12.3 @@ -1524,7 +1524,7 @@
    12.4    proof (cases p q rule: linorder_cases)
    12.5      assume "p < q"
    12.6      hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A
    12.7 -      by (auto intro!: smalloI_tendsto tendsto_neg_powr simp: powr_diff [symmetric] )
    12.8 +      by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
    12.9      with `p < q` show ?thesis by auto
   12.10    next
   12.11      assume "p = q"
   12.12 @@ -1533,7 +1533,7 @@
   12.13    next
   12.14      assume "p > q"
   12.15      hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" using assms A
   12.16 -      by (auto intro!: smalloI_tendsto tendsto_neg_powr landau_o.small_imp_big simp: powr_diff [symmetric] )
   12.17 +      by (auto intro!: smalloI_tendsto tendsto_neg_powr landau_o.small_imp_big simp flip: powr_diff)
   12.18      with B `p > q` show ?thesis by auto
   12.19    qed
   12.20  qed
   12.21 @@ -1555,7 +1555,7 @@
   12.22    proof (cases p q rule: linorder_cases)
   12.23      assume "p < q"
   12.24      hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A
   12.25 -      by (auto intro!: smalloI_tendsto tendsto_neg_powr simp: powr_diff [symmetric] )
   12.26 +      by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
   12.27      with `p < q` show ?thesis by (auto intro: landau_o.small_imp_big)
   12.28    next
   12.29      assume "p = q"
   12.30 @@ -1564,7 +1564,7 @@
   12.31    next
   12.32      assume "p > q"
   12.33      hence "(\<lambda>x. g x powr q) \<in> o[F](\<lambda>x. g x powr p)" using assms A
   12.34 -      by (auto intro!: smalloI_tendsto tendsto_neg_powr simp: powr_diff [symmetric] )
   12.35 +      by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
   12.36      with B `p > q` show ?thesis by (auto intro: landau_o.small_imp_big)
   12.37    qed
   12.38  qed
    13.1 --- a/src/HOL/Library/Lattice_Algebras.thy	Thu Jun 07 15:08:18 2018 +0200
    13.2 +++ b/src/HOL/Library/Lattice_Algebras.thy	Thu Jun 07 19:36:12 2018 +0200
    13.3 @@ -136,7 +136,7 @@
    13.4  qed
    13.5  
    13.6  lemma prts: "a = pprt a + nprt a"
    13.7 -  by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric])
    13.8 +  by (simp add: pprt_def nprt_def flip: add_eq_inf_sup)
    13.9  
   13.10  lemma zero_le_pprt[simp]: "0 \<le> pprt a"
   13.11    by (simp add: pprt_def)
   13.12 @@ -266,7 +266,7 @@
   13.13  proof -
   13.14    from add_le_cancel_left [of "uminus a" "plus a a" zero]
   13.15    have "a \<le> - a \<longleftrightarrow> a + a \<le> 0"
   13.16 -    by (simp add: add.assoc[symmetric])
   13.17 +    by (simp flip: add.assoc)
   13.18    then show ?thesis
   13.19      by simp
   13.20  qed
   13.21 @@ -275,7 +275,7 @@
   13.22  proof -
   13.23    have "- a \<le> a \<longleftrightarrow> 0 \<le> a + a"
   13.24      using add_le_cancel_left [of "uminus a" zero "plus a a"]
   13.25 -    by (simp add: add.assoc[symmetric])
   13.26 +    by (simp flip: add.assoc)
   13.27    then show ?thesis
   13.28      by simp
   13.29  qed
   13.30 @@ -461,7 +461,7 @@
   13.31        apply blast
   13.32        done
   13.33      have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
   13.34 -      by (simp add: prts[symmetric])
   13.35 +      by (simp flip: prts)
   13.36      show ?thesis
   13.37      proof (cases "0 \<le> a * b")
   13.38        case True
    14.1 --- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Thu Jun 07 15:08:18 2018 +0200
    14.2 +++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy	Thu Jun 07 19:36:12 2018 +0200
    14.3 @@ -531,7 +531,7 @@
    14.4         (auto simp: stl)
    14.5  next
    14.6    assume "alw (\<lambda>x. P (f x)) s" then show "alw P (f s)"
    14.7 -    by (coinduction arbitrary: s rule: alw_coinduct) (auto simp: stl[symmetric])
    14.8 +    by (coinduction arbitrary: s rule: alw_coinduct) (auto simp flip: stl)
    14.9  qed
   14.10  
   14.11  lemma ev_inv:
   14.12 @@ -542,7 +542,7 @@
   14.13      by (induction "f s" arbitrary: s) (auto simp: stl)
   14.14  next
   14.15    assume "ev (\<lambda>x. P (f x)) s" then show "ev P (f s)"
   14.16 -    by induction (auto simp: stl[symmetric])
   14.17 +    by induction (auto simp flip: stl)
   14.18  qed
   14.19  
   14.20  lemma alw_smap: "alw P (smap f s) \<longleftrightarrow> alw (\<lambda>x. P (smap f x)) s"
   14.21 @@ -624,7 +624,7 @@
   14.22      by (induction "f s" arbitrary: s) (auto simp: stl intro: suntil.intros)
   14.23  next
   14.24    assume "((\<lambda>x. P (f x)) suntil (\<lambda>x. Q (f x))) s" then show "(P suntil Q) (f s)"
   14.25 -    by induction (auto simp: stl[symmetric] intro: suntil.intros)
   14.26 +    by induction (auto simp flip: stl intro: suntil.intros)
   14.27  qed
   14.28  
   14.29  lemma suntil_smap: "(P suntil Q) (smap f s) \<longleftrightarrow> ((\<lambda>x. P (smap f x)) suntil (\<lambda>x. Q (smap f x))) s"
   14.30 @@ -778,7 +778,7 @@
   14.31      using \<open>alw (HLD s) \<omega>\<close> by (simp add: alw_iff_sdrop HLD_iff)
   14.32    from pigeonhole_infinite_rel[OF infinite_UNIV_nat \<open>finite s\<close> this]
   14.33    show ?thesis
   14.34 -    by (simp add: HLD_iff infinite_iff_alw_ev[symmetric])
   14.35 +    by (simp add: HLD_iff flip: infinite_iff_alw_ev)
   14.36  qed
   14.37  
   14.38  lemma ev_eq_suntil: "ev P \<omega> \<longleftrightarrow> (not P suntil P) \<omega>"
    15.1 --- a/src/HOL/Library/Log_Nat.thy	Thu Jun 07 15:08:18 2018 +0200
    15.2 +++ b/src/HOL/Library/Log_Nat.thy	Thu Jun 07 19:36:12 2018 +0200
    15.3 @@ -37,7 +37,7 @@
    15.4      also have "\<dots> < b powr (\<lfloor>log b x\<rfloor> + 1)"
    15.5        using assms by (intro powr_less_mono) auto
    15.6      also have "\<dots> = b ^ nat (\<lfloor>log b (real_of_int x)\<rfloor> + 1)"
    15.7 -      using assms by (simp add: powr_realpow[symmetric])
    15.8 +      using assms by (simp flip: powr_realpow)
    15.9      finally
   15.10      have "x < b ^ nat (\<lfloor>log b (int x)\<rfloor> + 1)"
   15.11        by (rule of_nat_less_imp_less)
   15.12 @@ -182,7 +182,7 @@
   15.13        by (auto simp: )
   15.14      then have "?l \<le> b powr log (real b) (real x)"
   15.15        using \<open>b > 1\<close>
   15.16 -      by (auto simp add: powr_realpow[symmetric] intro!: powr_mono of_nat_floor)
   15.17 +      by (auto simp flip: powr_realpow intro!: powr_mono of_nat_floor)
   15.18      also have "\<dots> = x" using \<open>b > 1\<close> \<open>0 < x\<close>
   15.19        by auto
   15.20      finally show ?thesis
   15.21 @@ -269,7 +269,7 @@
   15.22  
   15.23  lemma bitlen_ge_iff_power: "w \<le> bitlen x \<longleftrightarrow> w \<le> 0 \<or> 2 ^ (nat w - 1) \<le> x"
   15.24    unfolding bitlen_def
   15.25 -  by (auto simp: nat_le_iff[symmetric] intro: floorlog_geI dest: floorlog_geD)
   15.26 +  by (auto simp flip: nat_le_iff intro: floorlog_geI dest: floorlog_geD)
   15.27  
   15.28  lemma bitlen_twopow_add_eq: "bitlen (2 ^ w + b) = w + 1" if "0 \<le> b" "b < 2 ^ w"
   15.29    by (auto simp: that nat_add_distrib bitlen_le_iff_power bitlen_ge_iff_power intro!: antisym)
    16.1 --- a/src/HOL/Library/Multiset.thy	Thu Jun 07 15:08:18 2018 +0200
    16.2 +++ b/src/HOL/Library/Multiset.thy	Thu Jun 07 19:36:12 2018 +0200
    16.3 @@ -101,7 +101,7 @@
    16.4  lemma add_mset_in_multiset:
    16.5    assumes M: \<open>M \<in> multiset\<close>
    16.6    shows \<open>(\<lambda>b. if b = a then Suc (M b) else M b) \<in> multiset\<close>
    16.7 -  using assms by (simp add: multiset_def insert_Collect[symmetric])
    16.8 +  using assms by (simp add: multiset_def flip: insert_Collect)
    16.9  
   16.10  lift_definition add_mset :: "'a \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is
   16.11    "\<lambda>a M b. if b = a then Suc (M b) else M b"
   16.12 @@ -244,8 +244,7 @@
   16.13    using count [of M] by (simp add: multiset_def)
   16.14  
   16.15  lemma set_mset_add_mset_insert [simp]: \<open>set_mset (add_mset a A) = insert a (set_mset A)\<close>
   16.16 -  by (auto simp del: count_greater_eq_Suc_zero_iff
   16.17 -      simp: count_greater_eq_Suc_zero_iff[symmetric] split: if_splits)
   16.18 +  by (auto simp flip: count_greater_eq_Suc_zero_iff split: if_splits)
   16.19  
   16.20  lemma multiset_nonemptyE [elim]:
   16.21    assumes "A \<noteq> {#}"
   16.22 @@ -1216,8 +1215,8 @@
   16.23        using that by (auto simp: subseteq_mset_def algebra_simps not_in_iff)
   16.24      hence "Sup A \<subseteq># Sup A - {#x#}" by (intro subset_mset.cSup_least nonempty)
   16.25      with \<open>x \<in># Sup A\<close> show False
   16.26 -      by (auto simp: subseteq_mset_def count_greater_zero_iff [symmetric]
   16.27 -               simp del: count_greater_zero_iff dest!: spec[of _ x])
   16.28 +      by (auto simp: subseteq_mset_def simp flip: count_greater_zero_iff
   16.29 +               dest!: spec[of _ x])
   16.30    qed
   16.31  next
   16.32    fix x X assume "x \<in> set_mset X" "X \<in> A"
   16.33 @@ -2158,7 +2157,7 @@
   16.34  lemma replicate_mset_msubseteq_iff:
   16.35    "replicate_mset m a \<subseteq># replicate_mset n b \<longleftrightarrow> m = 0 \<or> a = b \<and> m \<le> n"
   16.36    by (cases m)
   16.37 -    (auto simp add: insert_subset_eq_iff count_le_replicate_mset_subset_eq [symmetric])
   16.38 +    (auto simp: insert_subset_eq_iff simp flip: count_le_replicate_mset_subset_eq)
   16.39  
   16.40  lemma msubseteq_replicate_msetE:
   16.41    assumes "A \<subseteq># replicate_mset n a"
   16.42 @@ -2991,7 +2990,7 @@
   16.43    assumes "trans s" and "irrefl s"
   16.44    shows "(X, Y) \<in> mult s \<longleftrightarrow> (X - X \<inter># Y, Y - X \<inter># Y) \<in> mult s" (is "?L \<longleftrightarrow> ?R")
   16.45  proof -
   16.46 -  have "X - X \<inter># Y + X \<inter># Y = X" "Y - X \<inter># Y + X \<inter># Y = Y" by (auto simp: count_inject[symmetric])
   16.47 +  have "X - X \<inter># Y + X \<inter># Y = X" "Y - X \<inter># Y + X \<inter># Y = Y" by (auto simp flip: count_inject)
   16.48    thus ?thesis using mult_cancel[OF assms, of "X - X \<inter># Y"  "X \<inter># Y" "Y - X \<inter># Y"] by auto
   16.49  qed
   16.50  
   16.51 @@ -3020,7 +3019,7 @@
   16.52    shows "multp P N M \<longleftrightarrow> (N, M) \<in> mult R" (is "?L \<longleftrightarrow> ?R")
   16.53  proof -
   16.54    have *: "M \<inter># N + (N - M \<inter># N) = N" "M \<inter># N + (M - M \<inter># N) = M"
   16.55 -    "(M - M \<inter># N) \<inter># (N - M \<inter># N) = {#}" by (auto simp: count_inject[symmetric])
   16.56 +    "(M - M \<inter># N) \<inter># (N - M \<inter># N) = {#}" by (auto simp flip: count_inject)
   16.57    show ?thesis
   16.58    proof
   16.59      assume ?L thus ?R
   16.60 @@ -3041,9 +3040,9 @@
   16.61    shows "multeqp P N M \<longleftrightarrow> (N, M) \<in> (mult R)\<^sup>="
   16.62  proof -
   16.63    { assume "N \<noteq> M" "M - M \<inter># N = {#}"
   16.64 -    then obtain y where "count N y \<noteq> count M y" by (auto simp: count_inject[symmetric])
   16.65 +    then obtain y where "count N y \<noteq> count M y" by (auto simp flip: count_inject)
   16.66      then have "\<exists>y. count M y < count N y" using \<open>M - M \<inter># N = {#}\<close>
   16.67 -      by (auto simp: count_inject[symmetric] dest!: le_neq_implies_less fun_cong[of _ _ y])
   16.68 +      by (auto simp flip: count_inject dest!: le_neq_implies_less fun_cong[of _ _ y])
   16.69    }
   16.70    then have "multeqp P N M \<longleftrightarrow> multp P N M \<or> N = M"
   16.71      by (auto simp: multeqp_def multp_def Let_def in_diff_count)
   16.72 @@ -3695,7 +3694,7 @@
   16.73      apply (rule ext)+
   16.74      apply safe
   16.75       apply (rule_tac x = "mset (zip xs ys)" in exI;
   16.76 -       auto simp: in_set_zip list_all2_iff mset_map[symmetric])
   16.77 +       auto simp: in_set_zip list_all2_iff simp flip: mset_map)
   16.78      apply (rename_tac XY)
   16.79      apply (cut_tac X = XY in ex_mset)
   16.80      apply (erule exE)
   16.81 @@ -3894,7 +3893,7 @@
   16.82    using arg_cong[OF insert_DiffM, of _ _ size] by simp
   16.83  
   16.84  lemma size_Diff_singleton: "x \<in># M \<Longrightarrow> size (M - {#x#}) = size M - 1"
   16.85 -  by (simp add: size_Suc_Diff1 [symmetric])
   16.86 +  by (simp flip: size_Suc_Diff1)
   16.87  
   16.88  lemma size_Diff_singleton_if: "size (A - {#x#}) = (if x \<in># A then size A - 1 else size A)"
   16.89    by (simp add: diff_single_trivial size_Diff_singleton)
    17.1 --- a/src/HOL/Library/Multiset_Permutations.thy	Thu Jun 07 15:08:18 2018 +0200
    17.2 +++ b/src/HOL/Library/Multiset_Permutations.thy	Thu Jun 07 19:36:12 2018 +0200
    17.3 @@ -216,7 +216,7 @@
    17.4  theorem card_permutations_of_multiset:
    17.5    "card (permutations_of_multiset A) = fact (size A) div (\<Prod>x\<in>set_mset A. fact (count A x))"
    17.6    "(\<Prod>x\<in>set_mset A. fact (count A x) :: nat) dvd fact (size A)"
    17.7 -  by (simp_all add: card_permutations_of_multiset_aux[of A, symmetric])
    17.8 +  by (simp_all flip: card_permutations_of_multiset_aux[of A])
    17.9  
   17.10  lemma card_permutations_of_multiset_insert_aux:
   17.11    "card (permutations_of_multiset (A + {#x#})) * (count A x + 1) = 
    18.1 --- a/src/HOL/Library/Periodic_Fun.thy	Thu Jun 07 15:08:18 2018 +0200
    18.2 +++ b/src/HOL/Library/Periodic_Fun.thy	Thu Jun 07 19:36:12 2018 +0200
    18.3 @@ -54,7 +54,7 @@
    18.4    by (subst of_nat_numeral[symmetric], subst minus_of_nat) (rule refl)
    18.5  
    18.6  lemma minus_1: "f (gn1 x) = f x"
    18.7 -  using minus_of_nat[of x 1] by (simp add: minus_1_eq minus_eq[symmetric])
    18.8 +  using minus_of_nat[of x 1] by (simp flip: minus_1_eq minus_eq)
    18.9  
   18.10  lemmas periodic_simps = plus_of_nat minus_of_nat plus_of_int minus_of_int 
   18.11                          plus_numeral minus_numeral plus_1 minus_1
    19.1 --- a/src/HOL/Library/Perm.thy	Thu Jun 07 15:08:18 2018 +0200
    19.2 +++ b/src/HOL/Library/Perm.thy	Thu Jun 07 19:36:12 2018 +0200
    19.3 @@ -79,7 +79,7 @@
    19.4    then obtain a where *: "affected f = {a}"
    19.5      by (rule card_1_singletonE)
    19.6    then have **: "f \<langle>$\<rangle> a \<noteq> a"
    19.7 -    by (simp add: in_affected [symmetric])
    19.8 +    by (simp flip: in_affected)
    19.9    with * have "f \<langle>$\<rangle> a \<notin> affected f"
   19.10      by simp
   19.11    then have "f \<langle>$\<rangle> (f \<langle>$\<rangle> a) = f \<langle>$\<rangle> a"
   19.12 @@ -545,7 +545,7 @@
   19.13    have "(f ^ n) \<langle>$\<rangle> a = (f ^ (n mod order f a + order f a * (n div order f a))) \<langle>$\<rangle> a"
   19.14      by simp
   19.15    also have "\<dots> = (f ^ (n mod order f a) * f ^ (order f a * (n div order f a))) \<langle>$\<rangle> a"
   19.16 -    by (simp add: power_add [symmetric])
   19.17 +    by (simp flip: power_add)
   19.18    finally show ?thesis
   19.19      by (simp add: apply_times)
   19.20  qed  
    20.1 --- a/src/HOL/Library/Stirling.thy	Thu Jun 07 15:08:18 2018 +0200
    20.2 +++ b/src/HOL/Library/Stirling.thy	Thu Jun 07 19:36:12 2018 +0200
    20.3 @@ -195,7 +195,7 @@
    20.4      by (subst sum_atMost_Suc_shift) (simp add: sum.distrib ring_distribs)
    20.5    also have "\<dots> = pochhammer x (Suc n)"
    20.6      by (subst sum_atMost_Suc_shift [symmetric])
    20.7 -      (simp add: algebra_simps sum.distrib sum_distrib_left pochhammer_Suc Suc [symmetric])
    20.8 +      (simp add: algebra_simps sum.distrib sum_distrib_left pochhammer_Suc flip: Suc)
    20.9    finally show ?case .
   20.10  qed
   20.11  
   20.12 @@ -262,7 +262,7 @@
   20.13    also have "zip_with_prev f y ys = map (\<lambda>i. f (xs ! i) (xs ! (i + 1))) [0..<length xs - 1]"
   20.14      unfolding Cons
   20.15      by (induct ys arbitrary: y)
   20.16 -      (simp_all add: zip_with_prev_def upt_conv_Cons map_Suc_upt [symmetric] del: upt_Suc)
   20.17 +      (simp_all add: zip_with_prev_def upt_conv_Cons flip: map_Suc_upt del: upt_Suc)
   20.18    finally show ?thesis
   20.19      using Cons by simp
   20.20  qed
    21.1 --- a/src/HOL/Library/Stream.thy	Thu Jun 07 15:08:18 2018 +0200
    21.2 +++ b/src/HOL/Library/Stream.thy	Thu Jun 07 19:36:12 2018 +0200
    21.3 @@ -430,8 +430,8 @@
    21.4  
    21.5  lemma stream_smap_fromN: "s = smap (\<lambda>j. let i = j - n in s !! i) (fromN n)"
    21.6    by (coinduction arbitrary: s n)
    21.7 -    (force simp: neq_Nil_conv Let_def snth.simps(2)[symmetric] Suc_diff_Suc
    21.8 -      intro: stream.map_cong split: if_splits simp del: snth.simps(2))
    21.9 +    (force simp: neq_Nil_conv Let_def Suc_diff_Suc simp flip: snth.simps(2)
   21.10 +      intro: stream.map_cong split: if_splits)
   21.11  
   21.12  lemma stream_smap_nats: "s = smap (snth s) nats"
   21.13    using stream_smap_fromN[where n = 0] by simp
    22.1 --- a/src/HOL/Library/Sublist.thy	Thu Jun 07 15:08:18 2018 +0200
    22.2 +++ b/src/HOL/Library/Sublist.thy	Thu Jun 07 19:36:12 2018 +0200
    22.3 @@ -105,7 +105,7 @@
    22.4    "prefix xs (ys @ zs) = (prefix xs ys \<or> (\<exists>us. xs = ys @ us \<and> prefix us zs))"
    22.5    apply (induct zs rule: rev_induct)
    22.6     apply force
    22.7 -  apply (simp del: append_assoc add: append_assoc [symmetric])
    22.8 +  apply (simp flip: append_assoc)
    22.9    apply (metis append_eq_appendI)
   22.10    done
   22.11  
    23.1 --- a/src/HOL/Library/Uprod.thy	Thu Jun 07 15:08:18 2018 +0200
    23.2 +++ b/src/HOL/Library/Uprod.thy	Thu Jun 07 19:36:12 2018 +0200
    23.3 @@ -129,7 +129,7 @@
    23.4    show "card_order natLeq" by(rule natLeq_card_order)
    23.5    show "BNF_Cardinal_Arithmetic.cinfinite natLeq" by(rule natLeq_cinfinite)
    23.6    show "ordLeq3 (card_of (set_uprod x)) natLeq" for x :: "'a uprod"
    23.7 -    by (auto simp: finite_iff_ordLess_natLeq[symmetric] intro: ordLess_imp_ordLeq)
    23.8 +    by (auto simp flip: finite_iff_ordLess_natLeq intro: ordLess_imp_ordLeq)
    23.9    show "rel_uprod R OO rel_uprod S \<le> rel_uprod (R OO S)"
   23.10      for R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool" by(rule predicate2I)(transfer; auto)
   23.11    show "rel_uprod R = (\<lambda>x y. \<exists>z. set_uprod z \<subseteq> {(x, y). R x y} \<and> map_uprod fst z = x \<and> map_uprod snd z = y)"