# HG changeset patch
# User haftmann
# Date 1383592209 -3600
# Node ID 7d2544dd39888b7400f6a374d61db624ab40825c
# Parent  ce00f2fef556ca4412eae619d6ed1b772e1e2b3a
fact generalization and name consolidation

diff -r ce00f2fef556 -r 7d2544dd3988 NEWS
--- a/NEWS	Mon Nov 04 20:10:06 2013 +0100
+++ b/NEWS	Mon Nov 04 20:10:09 2013 +0100
@@ -24,6 +24,10 @@
 
 * Fact name consolidation:
     diff_def, diff_minus, ab_diff_minus ~> diff_conv_add_uminus
+    minus_le_self_iff ~> neg_less_eq_nonneg
+    le_minus_self_iff ~> less_eq_neg_nonpos
+    neg_less_nonneg ~> neg_less_pos
+    less_minus_self_iff ~> less_neg_neg [simp]
 INCOMPATIBILITY.
 
 * More simplification rules on unary and binary minus:
@@ -48,7 +52,6 @@
 or the brute way with
 "simp add: diff_conv_add_uminus del: add_uminus_conv_diff".
 
-
 New in Isabelle2013-1 (November 2013)
 -------------------------------------
 
diff -r ce00f2fef556 -r 7d2544dd3988 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Mon Nov 04 20:10:06 2013 +0100
+++ b/src/HOL/Groups.thy	Mon Nov 04 20:10:09 2013 +0100
@@ -1073,63 +1073,6 @@
 
 subclass linordered_cancel_ab_semigroup_add ..
 
-lemma neg_less_eq_nonneg [simp]:
-  "- a \<le> a \<longleftrightarrow> 0 \<le> a"
-proof
-  assume A: "- a \<le> a" show "0 \<le> a"
-  proof (rule classical)
-    assume "\<not> 0 \<le> a"
-    then have "a < 0" by auto
-    with A have "- a < 0" by (rule le_less_trans)
-    then show ?thesis by auto
-  qed
-next
-  assume A: "0 \<le> a" show "- a \<le> a"
-  proof (rule order_trans)
-    show "- a \<le> 0" using A by (simp add: minus_le_iff)
-  next
-    show "0 \<le> a" using A .
-  qed
-qed
-
-lemma neg_less_nonneg [simp]:
-  "- a < a \<longleftrightarrow> 0 < a"
-proof
-  assume A: "- a < a" show "0 < a"
-  proof (rule classical)
-    assume "\<not> 0 < a"
-    then have "a \<le> 0" by auto
-    with A have "- a < 0" by (rule less_le_trans)
-    then show ?thesis by auto
-  qed
-next
-  assume A: "0 < a" show "- a < a"
-  proof (rule less_trans)
-    show "- a < 0" using A by (simp add: minus_le_iff)
-  next
-    show "0 < a" using A .
-  qed
-qed
-
-lemma less_eq_neg_nonpos [simp]:
-  "a \<le> - a \<longleftrightarrow> a \<le> 0"
-proof
-  assume A: "a \<le> - a" show "a \<le> 0"
-  proof (rule classical)
-    assume "\<not> a \<le> 0"
-    then have "0 < a" by auto
-    then have "0 < - a" using A by (rule less_le_trans)
-    then show ?thesis by auto
-  qed
-next
-  assume A: "a \<le> 0" show "a \<le> - a"
-  proof (rule order_trans)
-    show "0 \<le> - a" using A by (simp add: minus_le_iff)
-  next
-    show "a \<le> 0" using A .
-  qed
-qed
-
 lemma equal_neg_zero [simp]:
   "a = - a \<longleftrightarrow> a = 0"
 proof
@@ -1151,6 +1094,37 @@
   "- a = a \<longleftrightarrow> a = 0"
   by (auto dest: sym)
 
+lemma neg_less_eq_nonneg [simp]:
+  "- a \<le> a \<longleftrightarrow> 0 \<le> a"
+proof
+  assume A: "- a \<le> a" show "0 \<le> a"
+  proof (rule classical)
+    assume "\<not> 0 \<le> a"
+    then have "a < 0" by auto
+    with A have "- a < 0" by (rule le_less_trans)
+    then show ?thesis by auto
+  qed
+next
+  assume A: "0 \<le> a" show "- a \<le> a"
+  proof (rule order_trans)
+    show "- a \<le> 0" using A by (simp add: minus_le_iff)
+  next
+    show "0 \<le> a" using A .
+  qed
+qed
+
+lemma neg_less_pos [simp]:
+  "- a < a \<longleftrightarrow> 0 < a"
+  by (auto simp add: less_le)
+
+lemma less_eq_neg_nonpos [simp]:
+  "a \<le> - a \<longleftrightarrow> a \<le> 0"
+  using neg_less_eq_nonneg [of "- a"] by simp
+
+lemma less_neg_neg [simp]:
+  "a < - a \<longleftrightarrow> a < 0"
+  using neg_less_pos [of "- a"] by simp
+
 lemma double_zero [simp]:
   "a + a = 0 \<longleftrightarrow> a = 0"
 proof
@@ -1169,7 +1143,7 @@
   assume "0 < a + a"
   then have "0 - a < a" by (simp only: diff_less_eq)
   then have "- a < a" by simp
-  then show "0 < a" by (simp only: neg_less_nonneg)
+  then show "0 < a" by simp
 next
   assume "0 < a"
   with this have "0 + 0 < a + a"
@@ -1197,14 +1171,6 @@
   then show ?thesis by simp
 qed
 
-lemma le_minus_self_iff:
-  "a \<le> - a \<longleftrightarrow> a \<le> 0"
-  by (fact less_eq_neg_nonpos)
-
-lemma minus_le_self_iff:
-  "- a \<le> a \<longleftrightarrow> 0 \<le> a"
-  by (fact neg_less_eq_nonneg)
-
 lemma minus_max_eq_min:
   "- max x y = min (-x) (-y)"
   by (auto simp add: max_def min_def)
diff -r ce00f2fef556 -r 7d2544dd3988 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Mon Nov 04 20:10:06 2013 +0100
+++ b/src/HOL/Rings.thy	Mon Nov 04 20:10:09 2013 +0100
@@ -1145,10 +1145,6 @@
   thus ?thesis by (simp add: ac cpos mult_strict_mono) 
 qed
 
-lemma less_minus_self_iff:
-  "a < - a \<longleftrightarrow> a < 0"
-  by (simp only: less_le less_eq_neg_nonpos equal_neg_zero)
-
 lemma abs_less_iff:
   "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b" 
   by (simp add: less_le abs_le_iff) (auto simp add: abs_if)