--- a/NEWS Fri Jun 14 08:34:28 2019 +0000
+++ b/NEWS Fri Jun 14 08:34:28 2019 +0000
@@ -18,6 +18,11 @@
Z2 (0 / 1): theory HOL/Library/Bit.thy has been renamed accordingly.
INCOMPATIBILITY.
+* Fact collection sign_simps contains only simplification rules
+for products being less / greater / equal to zero; combine with
+existing collections algebra_simps or field_simps to obtain
+reasonable simplification. INCOMPATIBILITY.
+
New in Isabelle2019 (June 2019)
-------------------------------
--- a/src/HOL/Analysis/Conformal_Mappings.thy Fri Jun 14 08:34:28 2019 +0000
+++ b/src/HOL/Analysis/Conformal_Mappings.thy Fri Jun 14 08:34:28 2019 +0000
@@ -1878,9 +1878,9 @@
apply (simp add: power2_eq_square divide_simps C_def norm_mult)
proof -
have "norm z * (norm (deriv f 0) * (r - norm z - norm z)) \<le> norm z * (norm (deriv f 0) * (r - norm z) - norm (deriv f 0) * norm z)"
- by (simp add: sign_simps)
+ by (simp add: algebra_simps)
then show "(norm z * (r - norm z) - norm z * norm z) * norm (deriv f 0) \<le> norm (deriv f 0) * norm z * (r - norm z) - norm z * norm z * norm (deriv f 0)"
- by (simp add: sign_simps)
+ by (simp add: algebra_simps)
qed
qed
have sq201 [simp]: "0 < (1 - sqrt 2 / 2)" "(1 - sqrt 2 / 2) < 1"
--- a/src/HOL/Decision_Procs/Approximation_Bounds.thy Fri Jun 14 08:34:28 2019 +0000
+++ b/src/HOL/Decision_Procs/Approximation_Bounds.thy Fri Jun 14 08:34:28 2019 +0000
@@ -1588,7 +1588,7 @@
by (cases "k = 0")
(auto intro!: add_mono
simp add: k [symmetric] uminus_add_conv_diff [symmetric]
- simp del: float_of_numeral uminus_add_conv_diff)
+ simp del: uminus_add_conv_diff)
hence "?lx \<le> x - k * (2 * pi) \<and> x - k * (2 * pi) \<le> ?ux"
by (auto intro!: float_plus_down_le float_plus_up_le)
note lx = this[THEN conjunct1] and ux = this[THEN conjunct2]
--- a/src/HOL/Groups.thy Fri Jun 14 08:34:28 2019 +0000
+++ b/src/HOL/Groups.thy Fri Jun 14 08:34:28 2019 +0000
@@ -15,8 +15,9 @@
subsection \<open>Dynamic facts\<close>
named_theorems ac_simps "associativity and commutativity simplification rules"
- and algebra_simps "algebra simplification rules"
+ and algebra_simps "algebra simplification rules for rings"
and field_simps "algebra simplification rules for fields"
+ and sign_simps "algebra simplification rules for comparision with zero"
text \<open>
The rewrites accumulated in \<open>algebra_simps\<close> deal with the classical
@@ -32,6 +33,10 @@
can be proved to be non-zero (for equations) or positive/negative (for
inequalities). Can be too aggressive and is therefore separate from the more
benign \<open>algebra_simps\<close>.
+
+ Lemmas \<open>sign_simps\<close> is a first attempt to automate proofs
+ of positivity/negativity needed for \<open>field_simps\<close>. Have not added \<open>sign_simps\<close> to \<open>field_simps\<close>
+ because the former can lead to case explosions.
\<close>
--- a/src/HOL/Library/Float.thy Fri Jun 14 08:34:28 2019 +0000
+++ b/src/HOL/Library/Float.thy Fri Jun 14 08:34:28 2019 +0000
@@ -495,10 +495,10 @@
by (auto simp: mantissa_exponent sign_simps)
lemma mantissa_nonneg_iff: "0 \<le> mantissa x \<longleftrightarrow> 0 \<le> x"
- by (auto simp: mantissa_exponent sign_simps zero_le_mult_iff)
+ by (auto simp: mantissa_exponent sign_simps)
lemma mantissa_neg_iff: "0 > mantissa x \<longleftrightarrow> 0 > x"
- by (auto simp: mantissa_exponent sign_simps zero_le_mult_iff)
+ by (auto simp: mantissa_exponent sign_simps)
lemma
fixes m e :: int
@@ -1788,8 +1788,8 @@
using truncate_down_uminus_eq[of p "x + y"]
by transfer (simp add: plus_down_def plus_up_def ac_simps)
-lemma mantissa_zero[simp]: "mantissa 0 = 0"
- by (metis mantissa_0 zero_float.abs_eq)
+lemma mantissa_zero: "mantissa 0 = 0"
+ by (fact mantissa_0)
qualified lemma compute_float_less[code]: "a < b \<longleftrightarrow> is_float_pos (float_plus_down 0 b (- a))"
using truncate_down[of 0 "b - a"] truncate_down_pos[of "b - a" 0]
@@ -1972,8 +1972,10 @@
from assms \<open>0 < x\<close> have "log 2 x \<le> log 2 y"
by auto
with \<open>\<lfloor>log 2 x\<rfloor> \<noteq> \<lfloor>log 2 y\<rfloor>\<close>
- have logless: "log 2 x < log 2 y" and flogless: "\<lfloor>log 2 x\<rfloor> < \<lfloor>log 2 y\<rfloor>"
- by (metis floor_less_cancel linorder_cases not_le)+
+ have logless: "log 2 x < log 2 y"
+ by linarith
+ have flogless: "\<lfloor>log 2 x\<rfloor> < \<lfloor>log 2 y\<rfloor>"
+ using \<open>\<lfloor>log 2 x\<rfloor> \<noteq> \<lfloor>log 2 y\<rfloor>\<close> \<open>log 2 x \<le> log 2 y\<close> by linarith
have "truncate_up prec x =
real_of_int \<lceil>x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor> )\<rceil> * 2 powr - real_of_int (int prec - \<lfloor>log 2 x\<rfloor>)"
using assms by (simp add: truncate_up_def round_up_def)
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Fri Jun 14 08:34:28 2019 +0000
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Fri Jun 14 08:34:28 2019 +0000
@@ -80,9 +80,6 @@
qed
qed simp
-lemma zero_notin_Suc_image[simp]: "0 \<notin> Suc ` A"
- by auto
-
lemma prod_sum_distrib_lists:
fixes P and S :: "'a set" and f :: "'a \<Rightarrow> _::semiring_0" assumes "finite S"
shows "(\<Sum>ms\<in>{ms. set ms \<subseteq> S \<and> length ms = n \<and> (\<forall>i<n. P i (ms!i))}. \<Prod>x<n. f (ms ! x)) =
@@ -99,7 +96,7 @@
by force+
show ?case unfolding *
using Suc[of "\<lambda>i. P (Suc i)"]
- by (simp add: sum.reindex split_conv sum_cartesian_product'
+ by (simp add: sum.reindex sum_cartesian_product'
lessThan_Suc_eq_insert_0 prod.reindex sum_distrib_right[symmetric] sum_distrib_left[symmetric])
qed
@@ -464,7 +461,7 @@
unfolding ce_OB_eq_ce_t
by (rule mutual_information_eq_entropy_conditional_entropy simple_function_finite)+
also have "\<dots> = \<H>(t\<circ>OB) - \<H>(t\<circ>OB | fst)"
- unfolding entropy_chain_rule[symmetric, OF simple_function_finite simple_function_finite] sign_simps
+ unfolding entropy_chain_rule[symmetric, OF simple_function_finite simple_function_finite] algebra_simps
by (subst entropy_commute) simp
also have "\<dots> \<le> \<H>(t\<circ>OB)"
using conditional_entropy_nonneg[of "t\<circ>OB" fst] by simp
--- a/src/HOL/Rat.thy Fri Jun 14 08:34:28 2019 +0000
+++ b/src/HOL/Rat.thy Fri Jun 14 08:34:28 2019 +0000
@@ -529,14 +529,6 @@
end
-text\<open>Lemmas \<open>sign_simps\<close> is a first attempt to automate proofs
-of positivity/negativity needed for \<open>field_simps\<close>. Have not added \<open>sign_simps\<close> to \<open>field_simps\<close> because the former can lead to case
-explosions.\<close>
-
-lemmas (in linordered_field) sign_simps [no_atp] = algebra_simps zero_less_mult_iff mult_less_0_iff
-lemmas sign_simps [no_atp] = algebra_simps zero_less_mult_iff mult_less_0_iff
-
-
instantiation rat :: distrib_lattice
begin
--- a/src/HOL/Rings.thy Fri Jun 14 08:34:28 2019 +0000
+++ b/src/HOL/Rings.thy Fri Jun 14 08:34:28 2019 +0000
@@ -16,8 +16,8 @@
subsection \<open>Semirings and rings\<close>
class semiring = ab_semigroup_add + semigroup_mult +
- assumes distrib_right[algebra_simps]: "(a + b) * c = a * c + b * c"
- assumes distrib_left[algebra_simps]: "a * (b + c) = a * b + a * c"
+ assumes distrib_right [algebra_simps]: "(a + b) * c = a * c + b * c"
+ assumes distrib_left [algebra_simps]: "a * (b + c) = a * b + a * c"
begin
text \<open>For the \<open>combine_numerals\<close> simproc\<close>
@@ -2176,17 +2176,17 @@
by (simp add: neq_iff)
qed
-lemma zero_less_mult_iff: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
+lemma zero_less_mult_iff [sign_simps]: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
(auto simp add: mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2)
-lemma zero_le_mult_iff: "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
+lemma zero_le_mult_iff [sign_simps]: "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
-lemma mult_less_0_iff: "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
+lemma mult_less_0_iff [sign_simps]: "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
using zero_less_mult_iff [of "- a" b] by auto
-lemma mult_le_0_iff: "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
+lemma mult_le_0_iff [sign_simps]: "a * b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
using zero_le_mult_iff [of "- a" b] by auto
text \<open>
--- a/src/HOL/ex/Ballot.thy Fri Jun 14 08:34:28 2019 +0000
+++ b/src/HOL/ex/Ballot.thy Fri Jun 14 08:34:28 2019 +0000
@@ -223,13 +223,13 @@
have "Suc a * (a - Suc b) + (Suc a - b) * Suc b =
(Suc a * a - Suc a * Suc b) + (Suc a * Suc b - Suc b * b)"
- by (simp add: sign_simps)
+ by (simp add: algebra_simps)
also have "\<dots> = (Suc a * a + (Suc a * Suc b - Suc b * b)) - Suc a * Suc b"
using \<open>b<a\<close> by (intro add_diff_assoc2 mult_mono) auto
also have "\<dots> = (Suc a * a + Suc a * Suc b) - Suc b * b - Suc a * Suc b"
using \<open>b<a\<close> by (intro arg_cong2[where f="(-)"] add_diff_assoc mult_mono) auto
also have "\<dots> = (Suc a * Suc (a + b)) - (Suc b * Suc (a + b))"
- by (simp add: sign_simps)
+ by (simp add: algebra_simps)
finally have rearrange: "Suc a * (a - Suc b) + (Suc a - b) * Suc b = (Suc a - Suc b) * Suc (a + b)"
unfolding diff_mult_distrib by simp