eliminated fact duplicates
authorhaftmann
Wed Feb 18 22:46:48 2015 +0100 (2015-02-18)
changeset 5955505573e5504a9
parent 59554 4044f53326c9
child 59556 aa2deef7cf47
eliminated fact duplicates
NEWS
src/HOL/Library/Fundamental_Theorem_Algebra.thy
src/HOL/Multivariate_Analysis/Fashoda.thy
src/HOL/Rings.thy
     1.1 --- a/NEWS	Wed Feb 18 22:46:47 2015 +0100
     1.2 +++ b/NEWS	Wed Feb 18 22:46:48 2015 +0100
     1.3 @@ -68,6 +68,11 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Eliminated fact duplicates:
     1.8 +  mult_less_imp_less_right ~> mult_right_less_imp_less
     1.9 +  mult_less_imp_less_left ~> mult_left_less_imp_less
    1.10 +Minor INCOMPATIBILITY.
    1.11 +
    1.12  * Fact consolidation: even_less_0_iff is subsumed by
    1.13  double_add_less_zero_iff_single_add_less_zero (simp by default anyway).
    1.14  
     2.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed Feb 18 22:46:47 2015 +0100
     2.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed Feb 18 22:46:48 2015 +0100
     2.3 @@ -217,7 +217,7 @@
     2.4        using b v
     2.5        apply (simp add: th2)
     2.6        done
     2.7 -    from mult_less_imp_less_left[OF th4 th3]
     2.8 +    from mult_left_less_imp_less[OF th4 th3]
     2.9      have "?P ?w n" unfolding th1 .
    2.10      then have "\<exists>z. ?P z n" ..
    2.11    }
     3.1 --- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Wed Feb 18 22:46:47 2015 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Wed Feb 18 22:46:48 2015 +0100
     3.3 @@ -590,7 +590,7 @@
     3.4        then have "(1 - u) * b > (1 - u) * a"
     3.5          by (auto simp add:field_simps)
     3.6        then have "b \<ge> a"
     3.7 -        apply (drule_tac mult_less_imp_less_left)
     3.8 +        apply (drule_tac mult_left_less_imp_less)
     3.9          using u
    3.10          apply auto
    3.11          done
    3.12 @@ -607,7 +607,7 @@
    3.13        then have "(1 - u) * a \<le> (1 - u) * b"
    3.14          apply -
    3.15          apply (rule mult_left_mono)
    3.16 -        apply (drule mult_less_imp_less_left)
    3.17 +        apply (drule mult_left_less_imp_less)
    3.18          using u
    3.19          apply auto
    3.20          done
    3.21 @@ -671,7 +671,7 @@
    3.22        then have "(1 - u) * b > (1 - u) * a"
    3.23          by (auto simp add: field_simps)
    3.24        then have "b \<ge> a"
    3.25 -        apply (drule_tac mult_less_imp_less_left)
    3.26 +        apply (drule_tac mult_left_less_imp_less)
    3.27          using u
    3.28          apply auto
    3.29          done
    3.30 @@ -688,7 +688,7 @@
    3.31        then have "(1 - u) * a \<le> (1 - u) * b"
    3.32          apply -
    3.33          apply (rule mult_left_mono)
    3.34 -        apply (drule mult_less_imp_less_left)
    3.35 +        apply (drule mult_left_less_imp_less)
    3.36          using u
    3.37          apply auto
    3.38          done
     4.1 --- a/src/HOL/Rings.thy	Wed Feb 18 22:46:47 2015 +0100
     4.2 +++ b/src/HOL/Rings.thy	Wed Feb 18 22:46:48 2015 +0100
     4.3 @@ -718,16 +718,6 @@
     4.4    apply simp
     4.5    done
     4.6  
     4.7 -lemma mult_less_imp_less_left:
     4.8 -  assumes "c * a < c * b" and "0 \<le> c"
     4.9 -  shows "a < b"
    4.10 -  using assms by (fact mult_left_less_imp_less)
    4.11 -
    4.12 -lemma mult_less_imp_less_right:
    4.13 -  assumes less: "a * c < b * c" and nonneg: "0 \<le> c"
    4.14 -  shows "a < b"
    4.15 -  using assms by (fact mult_right_less_imp_less)
    4.16 -
    4.17  end
    4.18  
    4.19  class linordered_semiring_1_strict = linordered_semiring_strict + semiring_1