# HG changeset patch
# User haftmann
# Date 1560501268 0
# Node ID e5cd5471c18a0c3b9ee6c5671aa573aa56f2f988
# Parent  408e15cbd2a60eee68dde9ecd1d039b2c415378a
official fact collection sign_simps

diff -r 408e15cbd2a6 -r e5cd5471c18a NEWS
--- 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)
 -------------------------------
diff -r 408e15cbd2a6 -r e5cd5471c18a src/HOL/Analysis/Conformal_Mappings.thy
--- 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"
diff -r 408e15cbd2a6 -r e5cd5471c18a src/HOL/Decision_Procs/Approximation_Bounds.thy
--- 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]
diff -r 408e15cbd2a6 -r e5cd5471c18a src/HOL/Groups.thy
--- 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>
 
 
diff -r 408e15cbd2a6 -r e5cd5471c18a src/HOL/Library/Float.thy
--- 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)
diff -r 408e15cbd2a6 -r e5cd5471c18a src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
--- 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
diff -r 408e15cbd2a6 -r e5cd5471c18a src/HOL/Rat.thy
--- 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
 
diff -r 408e15cbd2a6 -r e5cd5471c18a src/HOL/Rings.thy
--- 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>
diff -r 408e15cbd2a6 -r e5cd5471c18a src/HOL/ex/Ballot.thy
--- 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