# HG changeset patch
# User huffman
# Date 1321506107 -3600
# Node ID 74b17a0881b3852243a47f129f98931be71d8e63
# Parent  528bad46f29e4a1b9a72b97508a7963a57de79a9
Int.thy: remove duplicate lemmas double_less_0_iff and odd_less_0, use {even,odd}_less_0_iff instead

diff -r 528bad46f29e -r 74b17a0881b3 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu Nov 17 05:27:45 2011 +0100
+++ b/src/HOL/Int.thy	Thu Nov 17 06:01:47 2011 +0100
@@ -1173,32 +1173,6 @@
 (* iszero_number_of_Pls would never normally be used
    because its lhs simplifies to "iszero 0" *)
 
-subsubsection {* The Less-Than Relation *}
-
-lemma double_less_0_iff:
-  "(a + a < 0) = (a < (0::'a::linordered_idom))"
-proof -
-  have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
-  also have "... = (a < 0)"
-    by (simp add: mult_less_0_iff zero_less_two 
-                  order_less_not_sym [OF zero_less_two]) 
-  finally show ?thesis .
-qed
-
-lemma odd_less_0:
-  "(1 + z + z < 0) = (z < (0::int))"
-proof (cases z)
-  case (nonneg n)
-  then show ?thesis
-    by (simp add: linorder_not_less add_assoc add_increasing
-      le_imp_0_less [THEN order_less_imp_le])
-next
-  case (neg n)
-  then show ?thesis
-    by (simp del: of_nat_Suc of_nat_add of_nat_1
-      add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
-qed
-
 text {* Less-Than or Equals *}
 
 text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}
@@ -1416,7 +1390,7 @@
   then obtain z where a: "a = of_int z" ..
   hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
     by (simp add: a)
-  also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
+  also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0_iff)
   also have "... = (a < 0)" by (simp add: a)
   finally show ?thesis .
 qed
diff -r 528bad46f29e -r 74b17a0881b3 src/HOL/Metis_Examples/Big_O.thy
--- a/src/HOL/Metis_Examples/Big_O.thy	Thu Nov 17 05:27:45 2011 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy	Thu Nov 17 06:01:47 2011 +0100
@@ -215,7 +215,7 @@
   apply (rule mult_left_mono)
   apply (rule abs_triangle_ineq)
   apply (simp add: order_less_le)
-apply (metis abs_not_less_zero double_less_0_iff less_not_permute linorder_not_less mult_less_0_iff)
+apply (metis abs_not_less_zero even_less_0_iff less_not_permute linorder_not_less mult_less_0_iff)
 done
 
 lemma bigo_plus_subset2 [intro]: "A <= O(f) ==> B <= O(f) ==> A \<oplus> B <= O(f)"