official fact collection sign_simps
authorhaftmann
Fri Jun 14 08:34:28 2019 +0000 (2 days ago)
changeset 70347e5cd5471c18a
parent 70346 408e15cbd2a6
child 70348 bde161c740ca
official fact collection sign_simps
NEWS
src/HOL/Analysis/Conformal_Mappings.thy
src/HOL/Decision_Procs/Approximation_Bounds.thy
src/HOL/Groups.thy
src/HOL/Library/Float.thy
src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
src/HOL/Rat.thy
src/HOL/Rings.thy
src/HOL/ex/Ballot.thy
     1.1 --- a/NEWS	Fri Jun 14 08:34:28 2019 +0000
     1.2 +++ b/NEWS	Fri Jun 14 08:34:28 2019 +0000
     1.3 @@ -18,6 +18,11 @@
     1.4  Z2 (0 / 1): theory HOL/Library/Bit.thy has been renamed accordingly.
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Fact collection sign_simps contains only simplification rules
     1.8 +for products being less / greater / equal to zero; combine with
     1.9 +existing collections algebra_simps or field_simps to obtain
    1.10 +reasonable simplification.  INCOMPATIBILITY.
    1.11 +
    1.12  
    1.13  New in Isabelle2019 (June 2019)
    1.14  -------------------------------
     2.1 --- a/src/HOL/Analysis/Conformal_Mappings.thy	Fri Jun 14 08:34:28 2019 +0000
     2.2 +++ b/src/HOL/Analysis/Conformal_Mappings.thy	Fri Jun 14 08:34:28 2019 +0000
     2.3 @@ -1878,9 +1878,9 @@
     2.4          apply (simp add: power2_eq_square divide_simps C_def norm_mult)
     2.5          proof -
     2.6            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)"
     2.7 -            by (simp add: sign_simps)
     2.8 +            by (simp add: algebra_simps)
     2.9            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)"
    2.10 -            by (simp add: sign_simps)
    2.11 +            by (simp add: algebra_simps)
    2.12          qed
    2.13      qed
    2.14      have sq201 [simp]: "0 < (1 - sqrt 2 / 2)" "(1 - sqrt 2 / 2)  < 1"
     3.1 --- a/src/HOL/Decision_Procs/Approximation_Bounds.thy	Fri Jun 14 08:34:28 2019 +0000
     3.2 +++ b/src/HOL/Decision_Procs/Approximation_Bounds.thy	Fri Jun 14 08:34:28 2019 +0000
     3.3 @@ -1588,7 +1588,7 @@
     3.4      by (cases "k = 0")
     3.5        (auto intro!: add_mono
     3.6          simp add: k [symmetric] uminus_add_conv_diff [symmetric]
     3.7 -        simp del: float_of_numeral uminus_add_conv_diff)
     3.8 +        simp del: uminus_add_conv_diff)
     3.9    hence "?lx \<le> x - k * (2 * pi) \<and> x - k * (2 * pi) \<le> ?ux"
    3.10      by (auto intro!: float_plus_down_le float_plus_up_le)
    3.11    note lx = this[THEN conjunct1] and ux = this[THEN conjunct2]
     4.1 --- a/src/HOL/Groups.thy	Fri Jun 14 08:34:28 2019 +0000
     4.2 +++ b/src/HOL/Groups.thy	Fri Jun 14 08:34:28 2019 +0000
     4.3 @@ -15,8 +15,9 @@
     4.4  subsection \<open>Dynamic facts\<close>
     4.5  
     4.6  named_theorems ac_simps "associativity and commutativity simplification rules"
     4.7 -  and algebra_simps "algebra simplification rules"
     4.8 +  and algebra_simps "algebra simplification rules for rings"
     4.9    and field_simps "algebra simplification rules for fields"
    4.10 +  and sign_simps "algebra simplification rules for comparision with zero"
    4.11  
    4.12  text \<open>
    4.13    The rewrites accumulated in \<open>algebra_simps\<close> deal with the classical
    4.14 @@ -32,6 +33,10 @@
    4.15    can be proved to be non-zero (for equations) or positive/negative (for
    4.16    inequalities). Can be too aggressive and is therefore separate from the more
    4.17    benign \<open>algebra_simps\<close>.
    4.18 +
    4.19 +  Lemmas \<open>sign_simps\<close> is a first attempt to automate proofs
    4.20 +  of positivity/negativity needed for \<open>field_simps\<close>. Have not added \<open>sign_simps\<close> to \<open>field_simps\<close>
    4.21 +  because the former can lead to case explosions.
    4.22  \<close>
    4.23  
    4.24  
     5.1 --- a/src/HOL/Library/Float.thy	Fri Jun 14 08:34:28 2019 +0000
     5.2 +++ b/src/HOL/Library/Float.thy	Fri Jun 14 08:34:28 2019 +0000
     5.3 @@ -495,10 +495,10 @@
     5.4    by (auto simp: mantissa_exponent sign_simps)
     5.5  
     5.6  lemma mantissa_nonneg_iff: "0 \<le> mantissa x \<longleftrightarrow> 0 \<le> x"
     5.7 -  by (auto simp: mantissa_exponent sign_simps zero_le_mult_iff)
     5.8 +  by (auto simp: mantissa_exponent sign_simps)
     5.9  
    5.10  lemma mantissa_neg_iff: "0 > mantissa x \<longleftrightarrow> 0 > x"
    5.11 -  by (auto simp: mantissa_exponent sign_simps zero_le_mult_iff)
    5.12 +  by (auto simp: mantissa_exponent sign_simps)
    5.13  
    5.14  lemma
    5.15    fixes m e :: int
    5.16 @@ -1788,8 +1788,8 @@
    5.17    using truncate_down_uminus_eq[of p "x + y"]
    5.18    by transfer (simp add: plus_down_def plus_up_def ac_simps)
    5.19  
    5.20 -lemma mantissa_zero[simp]: "mantissa 0 = 0"
    5.21 -  by (metis mantissa_0 zero_float.abs_eq)
    5.22 +lemma mantissa_zero: "mantissa 0 = 0"
    5.23 +  by (fact mantissa_0)
    5.24  
    5.25  qualified lemma compute_float_less[code]: "a < b \<longleftrightarrow> is_float_pos (float_plus_down 0 b (- a))"
    5.26    using truncate_down[of 0 "b - a"] truncate_down_pos[of "b - a" 0]
    5.27 @@ -1972,8 +1972,10 @@
    5.28      from assms \<open>0 < x\<close> have "log 2 x \<le> log 2 y"
    5.29        by auto
    5.30      with \<open>\<lfloor>log 2 x\<rfloor> \<noteq> \<lfloor>log 2 y\<rfloor>\<close>
    5.31 -    have logless: "log 2 x < log 2 y" and flogless: "\<lfloor>log 2 x\<rfloor> < \<lfloor>log 2 y\<rfloor>"
    5.32 -      by (metis floor_less_cancel linorder_cases not_le)+
    5.33 +    have logless: "log 2 x < log 2 y"
    5.34 +      by linarith
    5.35 +    have flogless: "\<lfloor>log 2 x\<rfloor> < \<lfloor>log 2 y\<rfloor>"
    5.36 +      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
    5.37      have "truncate_up prec x =
    5.38        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>)"
    5.39        using assms by (simp add: truncate_up_def round_up_def)
     6.1 --- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Fri Jun 14 08:34:28 2019 +0000
     6.2 +++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Fri Jun 14 08:34:28 2019 +0000
     6.3 @@ -80,9 +80,6 @@
     6.4    qed
     6.5  qed simp
     6.6  
     6.7 -lemma zero_notin_Suc_image[simp]: "0 \<notin> Suc ` A"
     6.8 -  by auto
     6.9 -
    6.10  lemma prod_sum_distrib_lists:
    6.11    fixes P and S :: "'a set" and f :: "'a \<Rightarrow> _::semiring_0" assumes "finite S"
    6.12    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)) =
    6.13 @@ -99,7 +96,7 @@
    6.14      by force+
    6.15    show ?case unfolding *
    6.16      using Suc[of "\<lambda>i. P (Suc i)"]
    6.17 -    by (simp add: sum.reindex split_conv sum_cartesian_product'
    6.18 +    by (simp add: sum.reindex sum_cartesian_product'
    6.19        lessThan_Suc_eq_insert_0 prod.reindex sum_distrib_right[symmetric] sum_distrib_left[symmetric])
    6.20  qed
    6.21  
    6.22 @@ -464,7 +461,7 @@
    6.23      unfolding ce_OB_eq_ce_t
    6.24      by (rule mutual_information_eq_entropy_conditional_entropy simple_function_finite)+
    6.25    also have "\<dots> = \<H>(t\<circ>OB) - \<H>(t\<circ>OB | fst)"
    6.26 -    unfolding entropy_chain_rule[symmetric, OF simple_function_finite simple_function_finite] sign_simps
    6.27 +    unfolding entropy_chain_rule[symmetric, OF simple_function_finite simple_function_finite] algebra_simps
    6.28      by (subst entropy_commute) simp
    6.29    also have "\<dots> \<le> \<H>(t\<circ>OB)"
    6.30      using conditional_entropy_nonneg[of "t\<circ>OB" fst] by simp
     7.1 --- a/src/HOL/Rat.thy	Fri Jun 14 08:34:28 2019 +0000
     7.2 +++ b/src/HOL/Rat.thy	Fri Jun 14 08:34:28 2019 +0000
     7.3 @@ -529,14 +529,6 @@
     7.4  
     7.5  end
     7.6  
     7.7 -text\<open>Lemmas \<open>sign_simps\<close> is a first attempt to automate proofs
     7.8 -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
     7.9 -explosions.\<close>
    7.10 -
    7.11 -lemmas (in linordered_field) sign_simps [no_atp] = algebra_simps zero_less_mult_iff mult_less_0_iff
    7.12 -lemmas sign_simps [no_atp] = algebra_simps zero_less_mult_iff mult_less_0_iff
    7.13 -
    7.14 -
    7.15  instantiation rat :: distrib_lattice
    7.16  begin
    7.17  
     8.1 --- a/src/HOL/Rings.thy	Fri Jun 14 08:34:28 2019 +0000
     8.2 +++ b/src/HOL/Rings.thy	Fri Jun 14 08:34:28 2019 +0000
     8.3 @@ -16,8 +16,8 @@
     8.4  subsection \<open>Semirings and rings\<close>
     8.5  
     8.6  class semiring = ab_semigroup_add + semigroup_mult +
     8.7 -  assumes distrib_right[algebra_simps]: "(a + b) * c = a * c + b * c"
     8.8 -  assumes distrib_left[algebra_simps]: "a * (b + c) = a * b + a * c"
     8.9 +  assumes distrib_right [algebra_simps]: "(a + b) * c = a * c + b * c"
    8.10 +  assumes distrib_left [algebra_simps]: "a * (b + c) = a * b + a * c"
    8.11  begin
    8.12  
    8.13  text \<open>For the \<open>combine_numerals\<close> simproc\<close>
    8.14 @@ -2176,17 +2176,17 @@
    8.15      by (simp add: neq_iff)
    8.16  qed
    8.17  
    8.18 -lemma zero_less_mult_iff: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
    8.19 +lemma zero_less_mult_iff [sign_simps]: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
    8.20    by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
    8.21       (auto simp add: mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2)
    8.22  
    8.23 -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"
    8.24 +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"
    8.25    by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
    8.26  
    8.27 -lemma mult_less_0_iff: "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
    8.28 +lemma mult_less_0_iff [sign_simps]: "a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
    8.29    using zero_less_mult_iff [of "- a" b] by auto
    8.30  
    8.31 -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"
    8.32 +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"
    8.33    using zero_le_mult_iff [of "- a" b] by auto
    8.34  
    8.35  text \<open>
     9.1 --- a/src/HOL/ex/Ballot.thy	Fri Jun 14 08:34:28 2019 +0000
     9.2 +++ b/src/HOL/ex/Ballot.thy	Fri Jun 14 08:34:28 2019 +0000
     9.3 @@ -223,13 +223,13 @@
     9.4  
     9.5        have "Suc a * (a - Suc b) + (Suc a - b) * Suc b =
     9.6          (Suc a * a - Suc a * Suc b) + (Suc a * Suc b - Suc b * b)"
     9.7 -        by (simp add: sign_simps)
     9.8 +        by (simp add: algebra_simps)
     9.9        also have "\<dots> = (Suc a * a + (Suc a * Suc b - Suc b * b)) - Suc a * Suc b"
    9.10          using \<open>b<a\<close> by (intro add_diff_assoc2 mult_mono) auto
    9.11        also have "\<dots> = (Suc a * a + Suc a * Suc b) - Suc b * b - Suc a * Suc b"
    9.12          using \<open>b<a\<close> by (intro arg_cong2[where f="(-)"] add_diff_assoc mult_mono) auto
    9.13        also have "\<dots> = (Suc a * Suc (a + b)) - (Suc b * Suc (a + b))"
    9.14 -        by (simp add: sign_simps)
    9.15 +        by (simp add: algebra_simps)
    9.16        finally have rearrange: "Suc a * (a - Suc b) + (Suc a - b) * Suc b = (Suc a - Suc b) * Suc (a + b)"
    9.17          unfolding diff_mult_distrib by simp
    9.18