--- a/src/HOL/Library/BigO.thy Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/BigO.thy Thu Jun 07 19:36:12 2018 +0200
@@ -188,7 +188,7 @@
apply (rule_tac x = "\<bar>c\<bar>" in exI)
apply auto
apply (drule_tac x = x in spec)+
- apply (simp add: abs_mult [symmetric])
+ apply (simp flip: abs_mult)
done
lemma bigo_bounded: "\<forall>x. 0 \<le> f x \<Longrightarrow> \<forall>x. f x \<le> g x \<Longrightarrow> f \<in> O(g)"
@@ -271,7 +271,7 @@
also have "\<dots> = O(\<lambda>x. \<bar>g x\<bar>) + O(\<lambda>x. \<bar>h x\<bar>)"
by (rule bigo_plus_eq, auto)
finally show ?thesis
- by (simp add: bigo_abs3 [symmetric])
+ by (simp flip: bigo_abs3)
qed
lemma bigo_mult [intro]: "O(f)*O(g) \<subseteq> O(f * g)"
@@ -447,7 +447,7 @@
for c :: "'a::linordered_field"
apply (simp add: bigo_def)
apply (rule_tac x = "\<bar>inverse c\<bar>" in exI)
- apply (simp add: abs_mult [symmetric])
+ apply (simp flip: abs_mult)
done
lemma bigo_const4: "c \<noteq> 0 \<Longrightarrow> O(\<lambda>x. 1) \<subseteq> O(\<lambda>x. c)"
@@ -468,7 +468,7 @@
lemma bigo_const_mult1: "(\<lambda>x. c * f x) \<in> O(f)"
apply (simp add: bigo_def)
apply (rule_tac x = "\<bar>c\<bar>" in exI)
- apply (auto simp add: abs_mult [symmetric])
+ apply (auto simp flip: abs_mult)
done
lemma bigo_const_mult2: "O(\<lambda>x. c * f x) \<subseteq> O(f)"
--- a/src/HOL/Library/Cardinality.thy Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Cardinality.thy Thu Jun 07 19:36:12 2018 +0200
@@ -62,7 +62,7 @@
by(simp add: card_UNIV_option)
lemma card_UNIV_set: "CARD('a set) = (if CARD('a) = 0 then 0 else 2 ^ CARD('a))"
-by(simp add: Pow_UNIV[symmetric] card_eq_0_iff card_Pow del: Pow_UNIV)
+by(simp add: card_eq_0_iff card_Pow flip: Pow_UNIV)
lemma card_set [simp]: "CARD('a set) = 2 ^ CARD('a::finite)"
by(simp add: card_UNIV_set)
@@ -267,7 +267,7 @@
definition "finite_UNIV = Phantom('a + 'b)
(of_phantom (finite_UNIV :: 'a finite_UNIV) \<and> of_phantom (finite_UNIV :: 'b finite_UNIV))"
instance
- by intro_classes (simp add: UNIV_Plus_UNIV[symmetric] finite_UNIV_sum_def finite_UNIV del: UNIV_Plus_UNIV)
+ by intro_classes (simp add: finite_UNIV_sum_def finite_UNIV)
end
instantiation sum :: (card_UNIV, card_UNIV) card_UNIV begin
--- a/src/HOL/Library/Countable.thy Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Countable.thy Thu Jun 07 19:36:12 2018 +0200
@@ -101,8 +101,8 @@
qualified termination
by (relation "measure id")
- (auto simp add: sum_encode_eq [symmetric] prod_encode_eq [symmetric]
- le_imp_less_Suc le_sum_encode_Inl le_sum_encode_Inr
+ (auto simp flip: sum_encode_eq prod_encode_eq
+ simp: le_imp_less_Suc le_sum_encode_Inl le_sum_encode_Inr
le_prod_encode_1 le_prod_encode_2)
lemma nth_item_covers: "finite_item x \<Longrightarrow> \<exists>n. nth_item n = x"
--- a/src/HOL/Library/Countable_Set_Type.thy Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Countable_Set_Type.thy Thu Jun 07 19:36:12 2018 +0200
@@ -125,7 +125,7 @@
proof -
have "rel_fun (pcr_cset (pcr_cset A)) (pcr_cset A) (\<lambda>A. UNION A id) (\<lambda>A. cUNION A id)"
by transfer_prover
- then show ?thesis by (simp add: cUnion_def [symmetric])
+ then show ?thesis by (simp flip: cUnion_def)
qed
lemmas cset_eqI = set_eqI[Transfer.transferred]
--- a/src/HOL/Library/Disjoint_Sets.thy Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Disjoint_Sets.thy Thu Jun 07 19:36:12 2018 +0200
@@ -55,7 +55,7 @@
moreover assume "\<forall>i\<in>I. A i \<in> F i" "\<forall>i\<in>I. B i \<in> F i"
ultimately show "(\<Inter>i\<in>I. A i) \<inter> (\<Inter>i\<in>I. B i) = {}"
using *[OF \<open>i\<in>I\<close>, THEN disjointD, of "A i" "B i"]
- by (auto simp: INT_Int_distrib[symmetric])
+ by (auto simp flip: INT_Int_distrib)
qed
subsubsection "Family of Disjoint Sets"
--- a/src/HOL/Library/Extended_Nat.thy Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Extended_Nat.thy Thu Jun 07 19:36:12 2018 +0200
@@ -321,7 +321,7 @@
by (simp add: eSuc_def split: enat.split)
lemma eSuc_minus_1 [simp]: "eSuc n - 1 = n"
- by (simp add: one_enat_def eSuc_enat[symmetric] zero_enat_def[symmetric])
+ by (simp add: one_enat_def flip: eSuc_enat zero_enat_def)
(*lemmas idiff_self_eq_0_enat = idiff_self_eq_0[unfolded zero_enat_def]*)
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Thu Jun 07 19:36:12 2018 +0200
@@ -486,10 +486,10 @@
by transfer (simp add: top_ereal_def)
lemma ennreal_top_neq_one[simp]: "top \<noteq> (1::ennreal)"
- by transfer (simp add: top_ereal_def one_ereal_def ereal_max[symmetric] del: ereal_max)
+ by transfer (simp add: top_ereal_def one_ereal_def flip: ereal_max)
lemma ennreal_one_neq_top[simp]: "1 \<noteq> (top::ennreal)"
- by transfer (simp add: top_ereal_def one_ereal_def ereal_max[symmetric] del: ereal_max)
+ by transfer (simp add: top_ereal_def one_ereal_def flip: ereal_max)
lemma ennreal_add_less_top[simp]:
fixes a b :: ennreal
@@ -636,7 +636,7 @@
apply transfer
subgoal for a b c
apply (cases a b c rule: ereal3_cases)
- apply (auto simp: ereal_max[symmetric] simp del: ereal_max)
+ apply (auto simp flip: ereal_max)
done
done
@@ -654,7 +654,7 @@
unfolding divide_ennreal_def
apply transfer
apply (subst mult.assoc)
- apply (simp add: top_ereal_def divide_ereal_def[symmetric])
+ apply (simp add: top_ereal_def flip: divide_ereal_def)
done
lemma divide_mult_eq: "a \<noteq> 0 \<Longrightarrow> a \<noteq> \<infinity> \<Longrightarrow> x * a / (b * a) = x / (b::ennreal)"
@@ -672,7 +672,7 @@
unfolding divide_ennreal_def
apply transfer
apply (subst mult.assoc)
- apply (simp add: top_ereal_def divide_ereal_def[symmetric])
+ apply (simp add: top_ereal_def flip: divide_ereal_def)
done
lemma ennreal_add_diff_cancel:
@@ -686,7 +686,7 @@
apply transfer
subgoal for a b
apply (cases a b rule: ereal2_cases)
- apply (auto simp: zero_ereal_def ereal_max[symmetric] max.absorb2 simp del: ereal_max)
+ apply (auto simp: zero_ereal_def max.absorb2 simp flip: ereal_max)
done
done
@@ -859,7 +859,7 @@
lemmas ennreal3_cases = ennreal_cases[case_product ennreal2_cases]
lemma ennreal_neq_top[simp]: "ennreal r \<noteq> top"
- by transfer (simp add: top_ereal_def zero_ereal_def ereal_max[symmetric] del: ereal_max)
+ by transfer (simp add: top_ereal_def zero_ereal_def flip: ereal_max)
lemma top_neq_ennreal[simp]: "top \<noteq> ennreal r"
using ennreal_neq_top[of r] by (auto simp del: ennreal_neq_top)
@@ -920,16 +920,13 @@
by (cases "0 \<le> y") (auto simp: ennreal_eq_0_iff ennreal_neg)
lemma ennreal_eq_1[simp]: "ennreal x = 1 \<longleftrightarrow> x = 1"
- by (cases "0 \<le> x")
- (auto simp: ennreal_neg ennreal_1[symmetric] simp del: ennreal_1)
+ by (cases "0 \<le> x") (auto simp: ennreal_neg simp flip: ennreal_1)
lemma ennreal_le_1[simp]: "ennreal x \<le> 1 \<longleftrightarrow> x \<le> 1"
- by (cases "0 \<le> x")
- (auto simp: ennreal_neg ennreal_1[symmetric] simp del: ennreal_1)
+ by (cases "0 \<le> x") (auto simp: ennreal_neg simp flip: ennreal_1)
lemma ennreal_ge_1[simp]: "ennreal x \<ge> 1 \<longleftrightarrow> x \<ge> 1"
- by (cases "0 \<le> x")
- (auto simp: ennreal_neg ennreal_1[symmetric] simp del: ennreal_1)
+ by (cases "0 \<le> x") (auto simp: ennreal_neg simp flip: ennreal_1)
lemma one_less_ennreal[simp]: "1 < ennreal x \<longleftrightarrow> 1 < x"
by transfer (auto simp: max.absorb2 less_max_iff_disj)
@@ -977,7 +974,7 @@
lemma ennreal_minus: "0 \<le> q \<Longrightarrow> ennreal r - ennreal q = ennreal (r - q)"
by transfer
- (simp add: max.absorb2 zero_ereal_def ereal_max[symmetric] del: ereal_max)
+ (simp add: max.absorb2 zero_ereal_def flip: ereal_max)
lemma ennreal_minus_top[simp]: "ennreal a - top = 0"
by (simp add: minus_top_ennreal)
@@ -1050,8 +1047,7 @@
"(\<And>e::real. y < top \<Longrightarrow> 0 < e \<Longrightarrow> x \<le> y + ennreal e) \<Longrightarrow> x \<le> y"
apply (cases y rule: ennreal_cases)
apply (cases x rule: ennreal_cases)
- apply (auto simp del: ennreal_plus simp add: top_unique ennreal_plus[symmetric]
- intro: zero_less_one field_le_epsilon)
+ apply (auto simp flip: ennreal_plus simp add: top_unique intro: zero_less_one field_le_epsilon)
done
lemma ennreal_rat_dense:
@@ -1394,7 +1390,7 @@
lemma ennreal_suminf_neq_top: "summable f \<Longrightarrow> (\<And>i. 0 \<le> f i) \<Longrightarrow> (\<Sum>i. ennreal (f i)) \<noteq> top"
using sums_ennreal[of f "suminf f"]
- by (simp add: suminf_nonneg sums_unique[symmetric] summable_sums_iff[symmetric] del: sums_ennreal)
+ by (simp add: suminf_nonneg flip: sums_unique summable_sums_iff del: sums_ennreal)
lemma suminf_ennreal_eq:
"(\<And>i. 0 \<le> f i) \<Longrightarrow> f sums x \<Longrightarrow> (\<Sum>i. ennreal (f i)) = ennreal x"
@@ -1598,7 +1594,7 @@
apply transfer
subgoal for A
using Inf_countable_INF[of A]
- apply (clarsimp simp add: decseq_def[symmetric])
+ apply (clarsimp simp flip: decseq_def)
subgoal for f
by (intro exI[of _ f]) auto
done
@@ -1794,19 +1790,17 @@
by (auto simp: top_unique)
lemma diff_diff_ennreal: fixes a b :: ennreal shows "a \<le> b \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> b - (b - a) = a"
- by (cases a b rule: ennreal2_cases)
- (auto simp: ennreal_minus top_unique)
+ by (cases a b rule: ennreal2_cases) (auto simp: ennreal_minus top_unique)
lemma ennreal_less_one_iff[simp]: "ennreal x < 1 \<longleftrightarrow> x < 1"
- by (cases "0 \<le> x")
- (auto simp: ennreal_neg ennreal_1[symmetric] ennreal_less_iff simp del: ennreal_1)
+ by (cases "0 \<le> x") (auto simp: ennreal_neg ennreal_less_iff simp flip: ennreal_1)
lemma SUP_const_minus_ennreal:
fixes f :: "'a \<Rightarrow> ennreal" shows "I \<noteq> {} \<Longrightarrow> (SUP x:I. c - f x) = c - (INF x:I. f x)"
including ennreal.lifting
by (transfer fixing: I)
- (simp add: sup_ereal_def[symmetric] SUP_sup_distrib[symmetric] SUP_ereal_minus_right
- del: sup_ereal_def)
+ (simp add: SUP_sup_distrib[symmetric] SUP_ereal_minus_right
+ flip: sup_ereal_def)
lemma zero_minus_ennreal[simp]: "0 - (a::ennreal) = 0"
including ennreal.lifting
@@ -1846,10 +1840,8 @@
lemma add_diff_le_ennreal: "a + b - c \<le> a + (b - c::ennreal)"
apply (cases a b c rule: ennreal3_cases)
subgoal for a' b' c'
- by (cases "0 \<le> b' - c'")
- (simp_all add: ennreal_minus ennreal_plus[symmetric] top_add ennreal_neg
- del: ennreal_plus)
- apply (simp_all add: top_add ennreal_plus[symmetric] del: ennreal_plus)
+ by (cases "0 \<le> b' - c'") (simp_all add: ennreal_minus top_add ennreal_neg flip: ennreal_plus)
+ apply (simp_all add: top_add flip: ennreal_plus)
done
lemma diff_eq_0_ennreal: "a < top \<Longrightarrow> a \<le> b \<Longrightarrow> a - b = (0::ennreal)"
@@ -1857,14 +1849,14 @@
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"
by (cases x; cases y; cases z)
- (auto simp add: top_add add_top minus_top_ennreal ennreal_minus ennreal_plus[symmetric] top_unique
- simp del: ennreal_plus)
+ (auto simp add: top_add add_top minus_top_ennreal ennreal_minus top_unique
+ simp flip: ennreal_plus)
lemma diff_diff_ennreal'': fixes x y z :: ennreal
shows "z \<le> y \<Longrightarrow> x - (y - z) = (if y - z \<le> x then x + z - y else 0)"
by (cases x; cases y; cases z)
- (auto simp add: top_add add_top minus_top_ennreal ennreal_minus ennreal_plus[symmetric] top_unique ennreal_neg
- simp del: ennreal_plus)
+ (auto simp add: top_add add_top minus_top_ennreal ennreal_minus top_unique ennreal_neg
+ simp flip: ennreal_plus)
lemma power_less_top_ennreal: fixes x :: ennreal shows "x ^ n < top \<longleftrightarrow> x < top \<or> n = 0"
using power_eq_top_ennreal[of x n] by (auto simp: less_top)
@@ -1880,7 +1872,7 @@
(auto simp: divide_ennreal ennreal_mult[symmetric] ennreal_less_iff field_simps ennreal_top_mult ennreal_top_divide)
lemma one_less_numeral[simp]: "1 < (numeral n::ennreal) \<longleftrightarrow> (num.One < n)"
- by (simp del: ennreal_1 ennreal_numeral add: ennreal_1[symmetric] ennreal_numeral[symmetric] ennreal_less_iff)
+ by (simp flip: ennreal_1 ennreal_numeral add: ennreal_less_iff)
lemma divide_eq_1_ennreal: "a / b = (1::ennreal) \<longleftrightarrow> (b \<noteq> top \<and> b \<noteq> 0 \<and> b = a)"
by (cases a ; cases b; cases "b = 0") (auto simp: ennreal_top_divide divide_ennreal split: if_split_asm)
@@ -1902,17 +1894,16 @@
lemma ennreal_minus_le_iff: "a - b \<le> c \<longleftrightarrow> (a \<le> b + (c::ennreal) \<and> (a = top \<and> b = top \<longrightarrow> c = top))"
by (cases a; cases b; cases c)
- (auto simp: top_unique top_add add_top ennreal_minus ennreal_plus[symmetric]
- simp del: ennreal_plus)
+ (auto simp: top_unique top_add add_top ennreal_minus simp flip: ennreal_plus)
lemma ennreal_le_minus_iff: "a \<le> b - c \<longleftrightarrow> (a + c \<le> (b::ennreal) \<or> (a = 0 \<and> b \<le> c))"
by (cases a; cases b; cases c)
- (auto simp: top_unique top_add add_top ennreal_minus ennreal_plus[symmetric] ennreal_le_iff2
- simp del: ennreal_plus)
+ (auto simp: top_unique top_add add_top ennreal_minus ennreal_le_iff2
+ simp flip: ennreal_plus)
lemma diff_add_eq_diff_diff_swap_ennreal: "x - (y + z :: ennreal) = x - y - z"
by (cases x; cases y; cases z)
- (auto simp: ennreal_plus[symmetric] ennreal_minus_if add_top top_add simp del: ennreal_plus)
+ (auto simp: ennreal_minus_if add_top top_add simp flip: ennreal_plus)
lemma diff_add_assoc2_ennreal: "b \<le> a \<Longrightarrow> (a - b + c::ennreal) = a + c - b"
by (cases a; cases b; cases c)
--- a/src/HOL/Library/Extended_Real.thy Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Extended_Real.thy Thu Jun 07 19:36:12 2018 +0200
@@ -174,7 +174,7 @@
then obtain n m where "{enat n<..} \<subseteq> A" "{enat m<..} \<subseteq> B"
by auto
then have "{enat (max n m) <..} \<subseteq> A \<inter> B"
- by (auto simp add: subset_eq Ball_def max_def enat_ord_code(1)[symmetric] simp del: enat_ord_code(1))
+ by (auto simp add: subset_eq Ball_def max_def simp flip: enat_ord_code(1))
then show ?case
by auto
next
@@ -415,7 +415,7 @@
lemma ereal_0_plus [simp]: "ereal 0 + x = x"
and plus_ereal_0 [simp]: "x + ereal 0 = x"
-by(simp_all add: zero_ereal_def[symmetric])
+by(simp_all flip: zero_ereal_def)
instance ereal :: numeral ..
@@ -939,7 +939,7 @@
lemma [simp]:
shows ereal_1_times: "ereal 1 * x = x"
and times_ereal_1: "x * ereal 1 = x"
-by(simp_all add: one_ereal_def[symmetric])
+by(simp_all flip: one_ereal_def)
lemma one_not_le_zero_ereal[simp]: "\<not> (1 \<le> (0::ereal))"
by (simp add: one_ereal_def zero_ereal_def)
@@ -2117,7 +2117,7 @@
obtain r where r: "ereal r = (SUP a:A. ereal a)" "A \<noteq> {}"
using * by (force simp: bot_ereal_def)
then show "bdd_above A" "A \<noteq> {}"
- by (auto intro!: SUP_upper bdd_aboveI[of _ r] simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
+ by (auto intro!: SUP_upper bdd_aboveI[of _ r] simp flip: ereal_less_eq)
qed (auto simp: mono_def continuous_at_imp_continuous_at_within continuous_at_ereal)
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))"
@@ -2130,7 +2130,7 @@
obtain r where r: "ereal r = (INF a:A. ereal a)" "A \<noteq> {}"
using * by (force simp: top_ereal_def)
then show "bdd_below A" "A \<noteq> {}"
- by (auto intro!: INF_lower bdd_belowI[of _ r] simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
+ by (auto intro!: INF_lower bdd_belowI[of _ r] simp flip: ereal_less_eq)
qed (auto simp: mono_def continuous_at_imp_continuous_at_within continuous_at_ereal)
lemma ereal_Inf':
@@ -2527,13 +2527,13 @@
by (cases n) auto
lemma ereal_of_enat_ge_zero_cancel_iff[simp]: "0 \<le> ereal_of_enat n \<longleftrightarrow> 0 \<le> n"
- by (cases n) (auto simp: enat_0[symmetric])
+ by (cases n) (auto simp flip: enat_0)
lemma ereal_of_enat_gt_zero_cancel_iff[simp]: "0 < ereal_of_enat n \<longleftrightarrow> 0 < n"
- by (cases n) (auto simp: enat_0[symmetric])
+ by (cases n) (auto simp flip: enat_0)
lemma ereal_of_enat_zero[simp]: "ereal_of_enat 0 = 0"
- by (auto simp: enat_0[symmetric])
+ by (auto simp flip: enat_0)
lemma ereal_of_enat_inf[simp]: "ereal_of_enat n = \<infinity> \<longleftrightarrow> n = \<infinity>"
by (cases n) auto
@@ -3639,7 +3639,7 @@
by (metis sums_ereal sums_unique summable_def)
lemma suminf_ereal_finite: "summable f \<Longrightarrow> (\<Sum>i. ereal (f i)) \<noteq> \<infinity>"
- by (auto simp: sums_ereal[symmetric] summable_def sums_unique[symmetric])
+ by (auto simp: summable_def simp flip: sums_ereal sums_unique)
lemma suminf_ereal_finite_neg:
assumes "summable f"
@@ -3779,8 +3779,8 @@
apply auto
done
also have "(\<lambda>x. inverse m * (x + -t)) -` S = (\<lambda>x. (x - t) / m) -` S"
- using m t by (auto simp: divide_ereal_def mult.commute uminus_ereal.simps[symmetric] minus_ereal_def
- simp del: uminus_ereal.simps)
+ using m t by (auto simp: divide_ereal_def mult.commute minus_ereal_def
+ simp flip: uminus_ereal.simps)
also have "(\<lambda>x. (x - t) / m) -` S = (\<lambda>x. m * x + t) ` S"
using m t
by (simp add: set_eq_iff image_iff)
@@ -4252,7 +4252,7 @@
by (cases rule: ereal2_cases[of a b]) auto
lemma minus_ereal_0 [simp]: "x - ereal 0 = x"
-by(simp add: zero_ereal_def[symmetric])
+by(simp flip: zero_ereal_def)
lemma ereal_diff_eq_0_iff: fixes a b :: ereal
shows "(\<bar>a\<bar> = \<infinity> \<Longrightarrow> \<bar>b\<bar> \<noteq> \<infinity>) \<Longrightarrow> a - b = 0 \<longleftrightarrow> a = b"
--- a/src/HOL/Library/Float.thy Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Float.thy Thu Jun 07 19:36:12 2018 +0200
@@ -82,7 +82,7 @@
if "e1 \<le> e2" for e1 m1 e2 m2 :: int
proof -
from that have "m1 * 2 powr e1 + m2 * 2 powr e2 = (m1 + m2 * 2 ^ nat (e2 - e1)) * 2 powr e1"
- by (simp add: powr_realpow[symmetric] powr_diff field_simps)
+ by (simp add: powr_diff field_simps flip: powr_realpow)
then show ?thesis
by blast
qed
@@ -132,7 +132,7 @@
apply (rename_tac m e)
apply (rule_tac x="m" in exI)
apply (rule_tac x="e - d" in exI)
- apply (simp add: powr_realpow[symmetric] field_simps powr_add[symmetric])
+ apply (simp flip: powr_realpow powr_add add: field_simps)
done
lemma div_power_2_int_float[simp]: "x \<in> float \<Longrightarrow> x / (2::int)^d \<in> float"
@@ -141,7 +141,7 @@
apply (rename_tac m e)
apply (rule_tac x="m" in exI)
apply (rule_tac x="e - d" in exI)
- apply (simp add: powr_realpow[symmetric] field_simps powr_add[symmetric])
+ apply (simp flip: powr_realpow powr_add add: field_simps)
done
lemma div_numeral_Bit0_float[simp]:
@@ -549,7 +549,7 @@
then have "2 powr (exponent f - e) = 2 powr - real_of_int (e - exponent f)"
by simp
also have "\<dots> = 1 / 2^nat (e - exponent f)"
- using pos by (simp add: powr_realpow[symmetric] powr_diff)
+ using pos by (simp flip: powr_realpow add: powr_diff)
finally have "m * 2^nat (e - exponent f) = real_of_int (mantissa f)"
using eq by simp
then have "mantissa f = m * 2^nat (e - exponent f)"
@@ -562,7 +562,7 @@
then show False using mantissa_not_dvd[OF not_0] by simp
qed
ultimately have "real_of_int m = mantissa f * 2^nat (exponent f - e)"
- by (simp add: powr_realpow[symmetric])
+ by (simp flip: powr_realpow)
with \<open>e \<le> exponent f\<close>
show "m = mantissa f * 2 ^ nat (exponent f - e)"
by linarith
@@ -662,11 +662,11 @@
lemma round_down_float[simp]: "round_down prec x \<in> float"
unfolding round_down_def
- by (auto intro!: times_float simp: of_int_minus[symmetric] simp del: of_int_minus)
+ by (auto intro!: times_float simp flip: of_int_minus)
lemma round_up_float[simp]: "round_up prec x \<in> float"
unfolding round_up_def
- by (auto intro!: times_float simp: of_int_minus[symmetric] simp del: of_int_minus)
+ by (auto intro!: times_float simp flip: of_int_minus)
lemma round_up: "x \<le> round_up prec x"
by (simp add: powr_minus_divide le_divide_eq round_up_def ceiling_correct)
@@ -686,19 +686,19 @@
by (simp add: round_up_def round_down_def field_simps)
also have "\<dots> \<le> 1 * 2 powr -prec"
by (rule mult_mono)
- (auto simp del: of_int_diff simp: of_int_diff[symmetric] ceiling_diff_floor_le_1)
+ (auto simp flip: of_int_diff simp: ceiling_diff_floor_le_1)
finally show ?thesis by simp
qed
lemma round_down_shift: "round_down p (x * 2 powr k) = 2 powr k * round_down (p + k) x"
unfolding round_down_def
by (simp add: powr_add powr_mult field_simps powr_diff)
- (simp add: powr_add[symmetric])
+ (simp flip: powr_add)
lemma round_up_shift: "round_up p (x * 2 powr k) = 2 powr k * round_up (p + k) x"
unfolding round_up_def
by (simp add: powr_add powr_mult field_simps powr_diff)
- (simp add: powr_add[symmetric])
+ (simp flip: powr_add)
lemma round_up_uminus_eq: "round_up p (-x) = - round_down p x"
and round_down_uminus_eq: "round_down p (-x) = - round_up p x"
@@ -831,7 +831,7 @@
finally show ?thesis
using \<open>p + e < 0\<close>
apply transfer
- apply (simp add: ac_simps round_down_def floor_divide_of_int_eq[symmetric])
+ apply (simp add: ac_simps round_down_def flip: floor_divide_of_int_eq)
proof - (*FIXME*)
fix pa :: int and ea :: int and ma :: int
assume a1: "2 ^ nat (- pa - ea) = 1 / (2 powr real_of_int pa * 2 powr real_of_int ea)"
@@ -871,8 +871,8 @@
proof (cases "b dvd a")
case True
then show ?thesis
- by (simp add: ceiling_def of_int_minus[symmetric] divide_minus_left[symmetric]
- floor_divide_of_int_eq dvd_neg_div del: divide_minus_left of_int_minus)
+ by (simp add: ceiling_def floor_divide_of_int_eq dvd_neg_div
+ flip: of_int_minus divide_minus_left)
next
case False
then have "a mod b \<noteq> 0"
@@ -881,7 +881,7 @@
using \<open>b \<noteq> 0\<close> by auto
have "\<lceil>real_of_int a / real_of_int b\<rceil> = \<lfloor>real_of_int a / real_of_int b\<rfloor> + 1"
apply (rule ceiling_eq)
- apply (auto simp: floor_divide_of_int_eq[symmetric])
+ apply (auto simp flip: floor_divide_of_int_eq)
proof -
have "real_of_int \<lfloor>real_of_int a / real_of_int b\<rfloor> \<le> real_of_int a / real_of_int b"
by simp
@@ -1207,7 +1207,7 @@
have "int x * 2 ^ nat l = x'"
by (simp add: x'_def)
moreover have "real x * 2 powr l = real x'"
- by (simp add: powr_realpow[symmetric] \<open>0 \<le> l\<close> x'_def)
+ by (simp flip: powr_realpow add: \<open>0 \<le> l\<close> x'_def)
ultimately show ?thesis
using ceil_divide_floor_conv[of y x'] powr_realpow[of 2 "nat l"] \<open>0 \<le> l\<close> \<open>y \<noteq> 0\<close>
l_def[symmetric, THEN meta_eq_to_obj_eq]
@@ -1223,7 +1223,7 @@
have "int y * 2 ^ nat (- l) = y'"
by (simp add: y'_def)
moreover have "real x * real_of_int (2::int) powr real_of_int l / real y = x / real y'"
- using \<open>\<not> 0 \<le> l\<close> by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps)
+ using \<open>\<not> 0 \<le> l\<close> by (simp flip: powr_realpow add: powr_minus y'_def field_simps)
ultimately show ?thesis
using ceil_divide_floor_conv[of y' x] \<open>\<not> 0 \<le> l\<close> \<open>y' \<noteq> 0\<close> \<open>y \<noteq> 0\<close>
l_def[symmetric, THEN meta_eq_to_obj_eq]
@@ -1389,7 +1389,7 @@
from that 2 have "(power_down p x (Suc n div 2)) ^ 2 \<le> (x ^ (Suc n div 2)) ^ 2"
by (auto intro: power_mono power_down_nonneg simp del: odd_Suc_div_two)
also have "\<dots> = x ^ (Suc n div 2 * 2)"
- by (simp add: power_mult[symmetric])
+ by (simp flip: power_mult)
also have "Suc n div 2 * 2 = Suc n"
using \<open>odd n\<close> by presburger
finally show ?thesis
@@ -1407,7 +1407,7 @@
from that even_Suc have "Suc n = Suc n div 2 * 2"
by presburger
then have "x ^ Suc n \<le> (x ^ (Suc n div 2))\<^sup>2"
- by (simp add: power_mult[symmetric])
+ by (simp flip: power_mult)
also from that 2 have "\<dots> \<le> (power_up p x (Suc n div 2))\<^sup>2"
by (auto intro: power_mono simp del: odd_Suc_div_two)
finally show ?thesis
@@ -1506,7 +1506,7 @@
proof cases
case 1
then show ?thesis
- by (simp add: assms(1)[symmetric] powr_add[symmetric] algebra_simps powr_mult_base)
+ by (simp flip: assms(1) powr_add add: algebra_simps powr_mult_base)
next
case 2
then have "b * 2 powr p < \<bar>b * 2 powr (p + 1)\<bar>"
@@ -1518,12 +1518,12 @@
by (simp_all add: floor_eq_iff)
have "\<lfloor>(a + b) * 2 powr q\<rfloor> = \<lfloor>(a + b) * 2 powr p * 2 powr (q - p)\<rfloor>"
- by (simp add: algebra_simps powr_realpow[symmetric] powr_add[symmetric])
+ by (simp add: algebra_simps flip: powr_realpow powr_add)
also have "\<dots> = \<lfloor>(ai + b * 2 powr p) * 2 powr (q - p)\<rfloor>"
by (simp add: assms algebra_simps)
also have "\<dots> = \<lfloor>(ai + b * 2 powr p) / real_of_int ((2::int) ^ nat (p - q))\<rfloor>"
using assms
- by (simp add: algebra_simps powr_realpow[symmetric] divide_powr_uminus powr_add[symmetric])
+ by (simp add: algebra_simps divide_powr_uminus flip: powr_realpow powr_add)
also have "\<dots> = \<lfloor>ai / real_of_int ((2::int) ^ nat (p - q))\<rfloor>"
by (simp del: of_int_power add: floor_divide_real_eq_div floor_eq)
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>" .
@@ -1534,7 +1534,7 @@
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>"
by (subst powr_diff) (simp add: field_simps)
also have "\<dots> = \<lfloor>(ai + sgn b / 2) / real_of_int ((2::int) ^ nat (p - q))\<rfloor>"
- using leqp by (simp add: powr_realpow[symmetric] powr_diff)
+ using leqp by (simp flip: powr_realpow add: powr_diff)
also have "\<dots> = \<lfloor>ai / real_of_int ((2::int) ^ nat (p - q))\<rfloor>"
by (simp del: of_int_power add: floor_divide_real_eq_div floor_eq)
finally show ?thesis .
@@ -1547,19 +1547,19 @@
by (auto simp: floor_eq_iff algebra_simps pos_divide_le_eq[symmetric] abs_if divide_powr_uminus
intro!: mult_neg_pos split: if_split_asm)
have "\<lfloor>(a + b) * 2 powr q\<rfloor> = \<lfloor>(2*a + 2*b) * 2 powr p * 2 powr (q - p - 1)\<rfloor>"
- by (simp add: algebra_simps powr_realpow[symmetric] powr_add[symmetric] powr_mult_base)
+ by (simp add: algebra_simps powr_mult_base flip: powr_realpow powr_add)
also have "\<dots> = \<lfloor>(2 * (a * 2 powr p) + 2 * b * 2 powr p) * 2 powr (q - p - 1)\<rfloor>"
by (simp add: algebra_simps)
also have "\<dots> = \<lfloor>(2 * ai + b * 2 powr (p + 1)) / 2 powr (1 - q + p)\<rfloor>"
using assms by (simp add: algebra_simps powr_mult_base divide_powr_uminus)
also have "\<dots> = \<lfloor>(2 * ai + b * 2 powr (p + 1)) / real_of_int ((2::int) ^ nat (p - q + 1))\<rfloor>"
- using assms by (simp add: algebra_simps powr_realpow[symmetric])
+ using assms by (simp add: algebra_simps flip: powr_realpow)
also have "\<dots> = \<lfloor>(2 * ai - 1) / real_of_int ((2::int) ^ nat (p - q + 1))\<rfloor>"
using \<open>b < 0\<close> assms
by (simp add: floor_divide_of_int_eq floor_eq floor_divide_real_eq_div
del: of_int_mult of_int_power of_int_diff)
also have "\<dots> = \<lfloor>(2 * ai - 1) * 2 powr (q - p - 1)\<rfloor>"
- using assms by (simp add: algebra_simps divide_powr_uminus powr_realpow[symmetric])
+ using assms by (simp add: algebra_simps divide_powr_uminus flip: powr_realpow)
finally show ?thesis
using \<open>b < 0\<close> by simp
qed
@@ -1595,7 +1595,7 @@
(metis of_int_1 of_int_add of_int_le_numeral_power_cancel_iff)
have "\<bar>ai\<bar> = 2 powr k + r"
- using \<open>k \<ge> 0\<close> by (auto simp: k_def r_def powr_realpow[symmetric])
+ using \<open>k \<ge> 0\<close> by (auto simp: k_def r_def simp flip: powr_realpow)
have pos: "\<bar>b\<bar> < 1 \<Longrightarrow> 0 < 2 powr k + (r + b)" for b :: real
using \<open>0 \<le> k\<close> \<open>ai \<noteq> 0\<close>
@@ -1664,8 +1664,7 @@
let ?e = "e1 - int k1 - 1"
have sum_eq: "?sum = (?m1 + ?m2) * 2 powr ?e"
- by (auto simp: powr_add[symmetric] powr_mult[symmetric] algebra_simps
- powr_realpow[symmetric] powr_mult_base)
+ by (auto simp flip: powr_add powr_mult powr_realpow simp: powr_mult_base algebra_simps)
have "\<bar>?m2\<bar> * 2 < 2 powr (bitlen \<bar>m2\<bar> + ?shift + 1)"
by (auto simp: field_simps powr_add powr_mult_base powr_diff abs_mult)
@@ -1753,7 +1752,7 @@
by (auto simp add: sgn_if zero_less_mult_iff simp del: powr_gt_zero)
also have "\<lfloor>(real_of_int (2 * ?m1) + real_of_int (sgn m2)) * 2 powr real_of_int (?f - - ?e - 1)\<rfloor> =
\<lfloor>Float (?m1 * 2 + sgn m2) (?e - 1) * 2 powr ?f\<rfloor>"
- by (simp add: powr_add[symmetric] algebra_simps powr_realpow[symmetric])
+ by (simp flip: powr_add powr_realpow add: algebra_simps)
finally
show "\<lfloor>(?a + ?b) * 2 powr ?f\<rfloor> = \<lfloor>real_of_float (Float (?m1 * 2 + sgn m2) (?e - 1)) * 2 powr ?f\<rfloor>" .
qed
@@ -1983,7 +1982,7 @@
have "x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor>) \<le>
x * (2 powr real (Suc prec) / (2 powr log 2 x))"
using real_of_int_floor_add_one_ge[of "log 2 x"] assms
- by (auto simp add: algebra_simps powr_diff [symmetric] intro!: mult_left_mono)
+ by (auto simp: algebra_simps simp flip: powr_diff intro!: mult_left_mono)
then show "x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor>) \<le> real_of_int ((2::int) ^ (Suc prec))"
using \<open>0 < x\<close> by (simp add: powr_realpow powr_add)
qed
@@ -2080,14 +2079,13 @@
have "x = 2 powr (log 2 \<bar>x\<bar>)" using \<open>0 < x\<close> by simp
also have "\<dots> \<le> (2 ^ (Suc prec )) * 2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor>)"
using real_of_int_floor_add_one_ge[of "log 2 \<bar>x\<bar>"] \<open>0 < x\<close>
- by (auto simp: powr_realpow[symmetric] powr_add[symmetric] algebra_simps
- powr_mult_base le_powr_iff)
+ by (auto simp flip: powr_realpow powr_add simp: algebra_simps powr_mult_base le_powr_iff)
also
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)"
using logless flogless \<open>x > 0\<close> \<open>y > 0\<close>
by (auto intro!: floor_mono)
finally show ?thesis
- by (auto simp: powr_realpow[symmetric] powr_diff assms of_nat_diff)
+ by (auto simp flip: powr_realpow simp: powr_diff assms of_nat_diff)
qed
ultimately show ?thesis
by (metis dual_order.trans truncate_down)
@@ -2170,12 +2168,12 @@
lemma compute_mantissa[code]:
"mantissa (Float m e) =
(if m = 0 then 0 else if 2 dvd m then mantissa (normfloat (Float m e)) else m)"
- by (auto simp: mantissa_float Float.abs_eq zero_float_def[symmetric])
+ by (auto simp: mantissa_float Float.abs_eq simp flip: zero_float_def)
lemma compute_exponent[code]:
"exponent (Float m e) =
(if m = 0 then 0 else if 2 dvd m then exponent (normfloat (Float m e)) else e)"
- by (auto simp: exponent_float Float.abs_eq zero_float_def[symmetric])
+ by (auto simp: exponent_float Float.abs_eq simp flip: zero_float_def)
lifting_update Float.float.lifting
lifting_forget Float.float.lifting
--- a/src/HOL/Library/Going_To_Filter.thy Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Going_To_Filter.thy Thu Jun 07 19:36:12 2018 +0200
@@ -80,7 +80,7 @@
lemma going_to_within_union [simp]:
"f going_to F within (A \<union> B) = sup (f going_to F within A) (f going_to F within B)"
- by (simp add: going_to_within_def inf_sup_distrib1 [symmetric])
+ by (simp add: going_to_within_def flip: inf_sup_distrib1)
lemma eventually_going_to_at_top_linorder:
fixes f :: "'a \<Rightarrow> 'b :: linorder"
--- a/src/HOL/Library/Infinite_Set.thy Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Infinite_Set.thy Thu Jun 07 19:36:12 2018 +0200
@@ -68,7 +68,7 @@
have "inj_on nat (abs ` A)" for A
by (rule inj_onI) auto
then show ?thesis
- by (auto simp add: image_comp [symmetric] dest: finite_image_absD finite_imageD)
+ by (auto simp flip: image_comp dest: finite_image_absD finite_imageD)
qed
proposition infinite_int_iff_unbounded_le: "infinite S \<longleftrightarrow> (\<forall>m. \<exists>n. \<bar>n\<bar> \<ge> m \<and> n \<in> S)"
@@ -161,11 +161,11 @@
lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P n) \<longleftrightarrow> (\<exists>m. \<forall>n>m. P n)"
for P :: "nat \<Rightarrow> bool"
- by (auto simp add: eventually_cofinite finite_nat_iff_bounded_le subset_eq not_le[symmetric])
+ by (auto simp add: eventually_cofinite finite_nat_iff_bounded_le subset_eq simp flip: not_le)
lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P n) \<longleftrightarrow> (\<exists>m. \<forall>n\<ge>m. P n)"
for P :: "nat \<Rightarrow> bool"
- by (auto simp add: eventually_cofinite finite_nat_iff_bounded subset_eq not_le[symmetric])
+ by (auto simp add: eventually_cofinite finite_nat_iff_bounded subset_eq simp flip: not_le)
lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P n) \<longleftrightarrow> (\<forall>m. \<exists>n>m. P n)"
for P :: "nat \<Rightarrow> bool"
@@ -286,7 +286,7 @@
apply (subst Suc)
apply (use \<open>infinite S\<close> in simp)
apply (intro arg_cong[where f = Least] ext)
- apply (auto simp: enumerate_Suc'[symmetric])
+ apply (auto simp flip: enumerate_Suc')
done
qed
--- a/src/HOL/Library/Landau_Symbols.thy Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Landau_Symbols.thy Thu Jun 07 19:36:12 2018 +0200
@@ -1524,7 +1524,7 @@
proof (cases p q rule: linorder_cases)
assume "p < q"
hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A
- by (auto intro!: smalloI_tendsto tendsto_neg_powr simp: powr_diff [symmetric] )
+ by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
with `p < q` show ?thesis by auto
next
assume "p = q"
@@ -1533,7 +1533,7 @@
next
assume "p > q"
hence "(\<lambda>x. g x powr q) \<in> O[F](\<lambda>x. g x powr p)" using assms A
- by (auto intro!: smalloI_tendsto tendsto_neg_powr landau_o.small_imp_big simp: powr_diff [symmetric] )
+ by (auto intro!: smalloI_tendsto tendsto_neg_powr landau_o.small_imp_big simp flip: powr_diff)
with B `p > q` show ?thesis by auto
qed
qed
@@ -1555,7 +1555,7 @@
proof (cases p q rule: linorder_cases)
assume "p < q"
hence "(\<lambda>x. g x powr p) \<in> o[F](\<lambda>x. g x powr q)" using assms A
- by (auto intro!: smalloI_tendsto tendsto_neg_powr simp: powr_diff [symmetric] )
+ by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
with `p < q` show ?thesis by (auto intro: landau_o.small_imp_big)
next
assume "p = q"
@@ -1564,7 +1564,7 @@
next
assume "p > q"
hence "(\<lambda>x. g x powr q) \<in> o[F](\<lambda>x. g x powr p)" using assms A
- by (auto intro!: smalloI_tendsto tendsto_neg_powr simp: powr_diff [symmetric] )
+ by (auto intro!: smalloI_tendsto tendsto_neg_powr simp flip: powr_diff)
with B `p > q` show ?thesis by (auto intro: landau_o.small_imp_big)
qed
qed
--- a/src/HOL/Library/Lattice_Algebras.thy Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Lattice_Algebras.thy Thu Jun 07 19:36:12 2018 +0200
@@ -136,7 +136,7 @@
qed
lemma prts: "a = pprt a + nprt a"
- by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric])
+ by (simp add: pprt_def nprt_def flip: add_eq_inf_sup)
lemma zero_le_pprt[simp]: "0 \<le> pprt a"
by (simp add: pprt_def)
@@ -266,7 +266,7 @@
proof -
from add_le_cancel_left [of "uminus a" "plus a a" zero]
have "a \<le> - a \<longleftrightarrow> a + a \<le> 0"
- by (simp add: add.assoc[symmetric])
+ by (simp flip: add.assoc)
then show ?thesis
by simp
qed
@@ -275,7 +275,7 @@
proof -
have "- a \<le> a \<longleftrightarrow> 0 \<le> a + a"
using add_le_cancel_left [of "uminus a" zero "plus a a"]
- by (simp add: add.assoc[symmetric])
+ by (simp flip: add.assoc)
then show ?thesis
by simp
qed
@@ -461,7 +461,7 @@
apply blast
done
have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
- by (simp add: prts[symmetric])
+ by (simp flip: prts)
show ?thesis
proof (cases "0 \<le> a * b")
case True
--- a/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy Thu Jun 07 19:36:12 2018 +0200
@@ -531,7 +531,7 @@
(auto simp: stl)
next
assume "alw (\<lambda>x. P (f x)) s" then show "alw P (f s)"
- by (coinduction arbitrary: s rule: alw_coinduct) (auto simp: stl[symmetric])
+ by (coinduction arbitrary: s rule: alw_coinduct) (auto simp flip: stl)
qed
lemma ev_inv:
@@ -542,7 +542,7 @@
by (induction "f s" arbitrary: s) (auto simp: stl)
next
assume "ev (\<lambda>x. P (f x)) s" then show "ev P (f s)"
- by induction (auto simp: stl[symmetric])
+ by induction (auto simp flip: stl)
qed
lemma alw_smap: "alw P (smap f s) \<longleftrightarrow> alw (\<lambda>x. P (smap f x)) s"
@@ -624,7 +624,7 @@
by (induction "f s" arbitrary: s) (auto simp: stl intro: suntil.intros)
next
assume "((\<lambda>x. P (f x)) suntil (\<lambda>x. Q (f x))) s" then show "(P suntil Q) (f s)"
- by induction (auto simp: stl[symmetric] intro: suntil.intros)
+ by induction (auto simp flip: stl intro: suntil.intros)
qed
lemma suntil_smap: "(P suntil Q) (smap f s) \<longleftrightarrow> ((\<lambda>x. P (smap f x)) suntil (\<lambda>x. Q (smap f x))) s"
@@ -778,7 +778,7 @@
using \<open>alw (HLD s) \<omega>\<close> by (simp add: alw_iff_sdrop HLD_iff)
from pigeonhole_infinite_rel[OF infinite_UNIV_nat \<open>finite s\<close> this]
show ?thesis
- by (simp add: HLD_iff infinite_iff_alw_ev[symmetric])
+ by (simp add: HLD_iff flip: infinite_iff_alw_ev)
qed
lemma ev_eq_suntil: "ev P \<omega> \<longleftrightarrow> (not P suntil P) \<omega>"
--- a/src/HOL/Library/Log_Nat.thy Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Log_Nat.thy Thu Jun 07 19:36:12 2018 +0200
@@ -37,7 +37,7 @@
also have "\<dots> < b powr (\<lfloor>log b x\<rfloor> + 1)"
using assms by (intro powr_less_mono) auto
also have "\<dots> = b ^ nat (\<lfloor>log b (real_of_int x)\<rfloor> + 1)"
- using assms by (simp add: powr_realpow[symmetric])
+ using assms by (simp flip: powr_realpow)
finally
have "x < b ^ nat (\<lfloor>log b (int x)\<rfloor> + 1)"
by (rule of_nat_less_imp_less)
@@ -182,7 +182,7 @@
by (auto simp: )
then have "?l \<le> b powr log (real b) (real x)"
using \<open>b > 1\<close>
- by (auto simp add: powr_realpow[symmetric] intro!: powr_mono of_nat_floor)
+ by (auto simp flip: powr_realpow intro!: powr_mono of_nat_floor)
also have "\<dots> = x" using \<open>b > 1\<close> \<open>0 < x\<close>
by auto
finally show ?thesis
@@ -269,7 +269,7 @@
lemma bitlen_ge_iff_power: "w \<le> bitlen x \<longleftrightarrow> w \<le> 0 \<or> 2 ^ (nat w - 1) \<le> x"
unfolding bitlen_def
- by (auto simp: nat_le_iff[symmetric] intro: floorlog_geI dest: floorlog_geD)
+ by (auto simp flip: nat_le_iff intro: floorlog_geI dest: floorlog_geD)
lemma bitlen_twopow_add_eq: "bitlen (2 ^ w + b) = w + 1" if "0 \<le> b" "b < 2 ^ w"
by (auto simp: that nat_add_distrib bitlen_le_iff_power bitlen_ge_iff_power intro!: antisym)
--- a/src/HOL/Library/Multiset.thy Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Multiset.thy Thu Jun 07 19:36:12 2018 +0200
@@ -101,7 +101,7 @@
lemma add_mset_in_multiset:
assumes M: \<open>M \<in> multiset\<close>
shows \<open>(\<lambda>b. if b = a then Suc (M b) else M b) \<in> multiset\<close>
- using assms by (simp add: multiset_def insert_Collect[symmetric])
+ using assms by (simp add: multiset_def flip: insert_Collect)
lift_definition add_mset :: "'a \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is
"\<lambda>a M b. if b = a then Suc (M b) else M b"
@@ -244,8 +244,7 @@
using count [of M] by (simp add: multiset_def)
lemma set_mset_add_mset_insert [simp]: \<open>set_mset (add_mset a A) = insert a (set_mset A)\<close>
- by (auto simp del: count_greater_eq_Suc_zero_iff
- simp: count_greater_eq_Suc_zero_iff[symmetric] split: if_splits)
+ by (auto simp flip: count_greater_eq_Suc_zero_iff split: if_splits)
lemma multiset_nonemptyE [elim]:
assumes "A \<noteq> {#}"
@@ -1216,8 +1215,8 @@
using that by (auto simp: subseteq_mset_def algebra_simps not_in_iff)
hence "Sup A \<subseteq># Sup A - {#x#}" by (intro subset_mset.cSup_least nonempty)
with \<open>x \<in># Sup A\<close> show False
- by (auto simp: subseteq_mset_def count_greater_zero_iff [symmetric]
- simp del: count_greater_zero_iff dest!: spec[of _ x])
+ by (auto simp: subseteq_mset_def simp flip: count_greater_zero_iff
+ dest!: spec[of _ x])
qed
next
fix x X assume "x \<in> set_mset X" "X \<in> A"
@@ -2158,7 +2157,7 @@
lemma replicate_mset_msubseteq_iff:
"replicate_mset m a \<subseteq># replicate_mset n b \<longleftrightarrow> m = 0 \<or> a = b \<and> m \<le> n"
by (cases m)
- (auto simp add: insert_subset_eq_iff count_le_replicate_mset_subset_eq [symmetric])
+ (auto simp: insert_subset_eq_iff simp flip: count_le_replicate_mset_subset_eq)
lemma msubseteq_replicate_msetE:
assumes "A \<subseteq># replicate_mset n a"
@@ -2991,7 +2990,7 @@
assumes "trans s" and "irrefl s"
shows "(X, Y) \<in> mult s \<longleftrightarrow> (X - X \<inter># Y, Y - X \<inter># Y) \<in> mult s" (is "?L \<longleftrightarrow> ?R")
proof -
- have "X - X \<inter># Y + X \<inter># Y = X" "Y - X \<inter># Y + X \<inter># Y = Y" by (auto simp: count_inject[symmetric])
+ have "X - X \<inter># Y + X \<inter># Y = X" "Y - X \<inter># Y + X \<inter># Y = Y" by (auto simp flip: count_inject)
thus ?thesis using mult_cancel[OF assms, of "X - X \<inter># Y" "X \<inter># Y" "Y - X \<inter># Y"] by auto
qed
@@ -3020,7 +3019,7 @@
shows "multp P N M \<longleftrightarrow> (N, M) \<in> mult R" (is "?L \<longleftrightarrow> ?R")
proof -
have *: "M \<inter># N + (N - M \<inter># N) = N" "M \<inter># N + (M - M \<inter># N) = M"
- "(M - M \<inter># N) \<inter># (N - M \<inter># N) = {#}" by (auto simp: count_inject[symmetric])
+ "(M - M \<inter># N) \<inter># (N - M \<inter># N) = {#}" by (auto simp flip: count_inject)
show ?thesis
proof
assume ?L thus ?R
@@ -3041,9 +3040,9 @@
shows "multeqp P N M \<longleftrightarrow> (N, M) \<in> (mult R)\<^sup>="
proof -
{ assume "N \<noteq> M" "M - M \<inter># N = {#}"
- then obtain y where "count N y \<noteq> count M y" by (auto simp: count_inject[symmetric])
+ then obtain y where "count N y \<noteq> count M y" by (auto simp flip: count_inject)
then have "\<exists>y. count M y < count N y" using \<open>M - M \<inter># N = {#}\<close>
- by (auto simp: count_inject[symmetric] dest!: le_neq_implies_less fun_cong[of _ _ y])
+ by (auto simp flip: count_inject dest!: le_neq_implies_less fun_cong[of _ _ y])
}
then have "multeqp P N M \<longleftrightarrow> multp P N M \<or> N = M"
by (auto simp: multeqp_def multp_def Let_def in_diff_count)
@@ -3695,7 +3694,7 @@
apply (rule ext)+
apply safe
apply (rule_tac x = "mset (zip xs ys)" in exI;
- auto simp: in_set_zip list_all2_iff mset_map[symmetric])
+ auto simp: in_set_zip list_all2_iff simp flip: mset_map)
apply (rename_tac XY)
apply (cut_tac X = XY in ex_mset)
apply (erule exE)
@@ -3894,7 +3893,7 @@
using arg_cong[OF insert_DiffM, of _ _ size] by simp
lemma size_Diff_singleton: "x \<in># M \<Longrightarrow> size (M - {#x#}) = size M - 1"
- by (simp add: size_Suc_Diff1 [symmetric])
+ by (simp flip: size_Suc_Diff1)
lemma size_Diff_singleton_if: "size (A - {#x#}) = (if x \<in># A then size A - 1 else size A)"
by (simp add: diff_single_trivial size_Diff_singleton)
--- a/src/HOL/Library/Multiset_Permutations.thy Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Multiset_Permutations.thy Thu Jun 07 19:36:12 2018 +0200
@@ -216,7 +216,7 @@
theorem card_permutations_of_multiset:
"card (permutations_of_multiset A) = fact (size A) div (\<Prod>x\<in>set_mset A. fact (count A x))"
"(\<Prod>x\<in>set_mset A. fact (count A x) :: nat) dvd fact (size A)"
- by (simp_all add: card_permutations_of_multiset_aux[of A, symmetric])
+ by (simp_all flip: card_permutations_of_multiset_aux[of A])
lemma card_permutations_of_multiset_insert_aux:
"card (permutations_of_multiset (A + {#x#})) * (count A x + 1) =
--- a/src/HOL/Library/Periodic_Fun.thy Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Periodic_Fun.thy Thu Jun 07 19:36:12 2018 +0200
@@ -54,7 +54,7 @@
by (subst of_nat_numeral[symmetric], subst minus_of_nat) (rule refl)
lemma minus_1: "f (gn1 x) = f x"
- using minus_of_nat[of x 1] by (simp add: minus_1_eq minus_eq[symmetric])
+ using minus_of_nat[of x 1] by (simp flip: minus_1_eq minus_eq)
lemmas periodic_simps = plus_of_nat minus_of_nat plus_of_int minus_of_int
plus_numeral minus_numeral plus_1 minus_1
--- a/src/HOL/Library/Perm.thy Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Perm.thy Thu Jun 07 19:36:12 2018 +0200
@@ -79,7 +79,7 @@
then obtain a where *: "affected f = {a}"
by (rule card_1_singletonE)
then have **: "f \<langle>$\<rangle> a \<noteq> a"
- by (simp add: in_affected [symmetric])
+ by (simp flip: in_affected)
with * have "f \<langle>$\<rangle> a \<notin> affected f"
by simp
then have "f \<langle>$\<rangle> (f \<langle>$\<rangle> a) = f \<langle>$\<rangle> a"
@@ -545,7 +545,7 @@
have "(f ^ n) \<langle>$\<rangle> a = (f ^ (n mod order f a + order f a * (n div order f a))) \<langle>$\<rangle> a"
by simp
also have "\<dots> = (f ^ (n mod order f a) * f ^ (order f a * (n div order f a))) \<langle>$\<rangle> a"
- by (simp add: power_add [symmetric])
+ by (simp flip: power_add)
finally show ?thesis
by (simp add: apply_times)
qed
--- a/src/HOL/Library/Stirling.thy Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Stirling.thy Thu Jun 07 19:36:12 2018 +0200
@@ -195,7 +195,7 @@
by (subst sum_atMost_Suc_shift) (simp add: sum.distrib ring_distribs)
also have "\<dots> = pochhammer x (Suc n)"
by (subst sum_atMost_Suc_shift [symmetric])
- (simp add: algebra_simps sum.distrib sum_distrib_left pochhammer_Suc Suc [symmetric])
+ (simp add: algebra_simps sum.distrib sum_distrib_left pochhammer_Suc flip: Suc)
finally show ?case .
qed
@@ -262,7 +262,7 @@
also have "zip_with_prev f y ys = map (\<lambda>i. f (xs ! i) (xs ! (i + 1))) [0..<length xs - 1]"
unfolding Cons
by (induct ys arbitrary: y)
- (simp_all add: zip_with_prev_def upt_conv_Cons map_Suc_upt [symmetric] del: upt_Suc)
+ (simp_all add: zip_with_prev_def upt_conv_Cons flip: map_Suc_upt del: upt_Suc)
finally show ?thesis
using Cons by simp
qed
--- a/src/HOL/Library/Stream.thy Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Stream.thy Thu Jun 07 19:36:12 2018 +0200
@@ -430,8 +430,8 @@
lemma stream_smap_fromN: "s = smap (\<lambda>j. let i = j - n in s !! i) (fromN n)"
by (coinduction arbitrary: s n)
- (force simp: neq_Nil_conv Let_def snth.simps(2)[symmetric] Suc_diff_Suc
- intro: stream.map_cong split: if_splits simp del: snth.simps(2))
+ (force simp: neq_Nil_conv Let_def Suc_diff_Suc simp flip: snth.simps(2)
+ intro: stream.map_cong split: if_splits)
lemma stream_smap_nats: "s = smap (snth s) nats"
using stream_smap_fromN[where n = 0] by simp
--- a/src/HOL/Library/Sublist.thy Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Sublist.thy Thu Jun 07 19:36:12 2018 +0200
@@ -105,7 +105,7 @@
"prefix xs (ys @ zs) = (prefix xs ys \<or> (\<exists>us. xs = ys @ us \<and> prefix us zs))"
apply (induct zs rule: rev_induct)
apply force
- apply (simp del: append_assoc add: append_assoc [symmetric])
+ apply (simp flip: append_assoc)
apply (metis append_eq_appendI)
done
--- a/src/HOL/Library/Uprod.thy Thu Jun 07 15:08:18 2018 +0200
+++ b/src/HOL/Library/Uprod.thy Thu Jun 07 19:36:12 2018 +0200
@@ -129,7 +129,7 @@
show "card_order natLeq" by(rule natLeq_card_order)
show "BNF_Cardinal_Arithmetic.cinfinite natLeq" by(rule natLeq_cinfinite)
show "ordLeq3 (card_of (set_uprod x)) natLeq" for x :: "'a uprod"
- by (auto simp: finite_iff_ordLess_natLeq[symmetric] intro: ordLess_imp_ordLeq)
+ by (auto simp flip: finite_iff_ordLess_natLeq intro: ordLess_imp_ordLeq)
show "rel_uprod R OO rel_uprod S \<le> rel_uprod (R OO S)"
for R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool" by(rule predicate2I)(transfer; auto)
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)"