src/HOL/Groups.thy
 changeset 54250 7d2544dd3988 parent 54230 b1d955791529 child 54703 499f92dc6e45
```     1.1 --- a/src/HOL/Groups.thy	Mon Nov 04 20:10:06 2013 +0100
1.2 +++ b/src/HOL/Groups.thy	Mon Nov 04 20:10:09 2013 +0100
1.3 @@ -1073,63 +1073,6 @@
1.4
1.6
1.7 -lemma neg_less_eq_nonneg [simp]:
1.8 -  "- a \<le> a \<longleftrightarrow> 0 \<le> a"
1.9 -proof
1.10 -  assume A: "- a \<le> a" show "0 \<le> a"
1.11 -  proof (rule classical)
1.12 -    assume "\<not> 0 \<le> a"
1.13 -    then have "a < 0" by auto
1.14 -    with A have "- a < 0" by (rule le_less_trans)
1.15 -    then show ?thesis by auto
1.16 -  qed
1.17 -next
1.18 -  assume A: "0 \<le> a" show "- a \<le> a"
1.19 -  proof (rule order_trans)
1.20 -    show "- a \<le> 0" using A by (simp add: minus_le_iff)
1.21 -  next
1.22 -    show "0 \<le> a" using A .
1.23 -  qed
1.24 -qed
1.25 -
1.26 -lemma neg_less_nonneg [simp]:
1.27 -  "- a < a \<longleftrightarrow> 0 < a"
1.28 -proof
1.29 -  assume A: "- a < a" show "0 < a"
1.30 -  proof (rule classical)
1.31 -    assume "\<not> 0 < a"
1.32 -    then have "a \<le> 0" by auto
1.33 -    with A have "- a < 0" by (rule less_le_trans)
1.34 -    then show ?thesis by auto
1.35 -  qed
1.36 -next
1.37 -  assume A: "0 < a" show "- a < a"
1.38 -  proof (rule less_trans)
1.39 -    show "- a < 0" using A by (simp add: minus_le_iff)
1.40 -  next
1.41 -    show "0 < a" using A .
1.42 -  qed
1.43 -qed
1.44 -
1.45 -lemma less_eq_neg_nonpos [simp]:
1.46 -  "a \<le> - a \<longleftrightarrow> a \<le> 0"
1.47 -proof
1.48 -  assume A: "a \<le> - a" show "a \<le> 0"
1.49 -  proof (rule classical)
1.50 -    assume "\<not> a \<le> 0"
1.51 -    then have "0 < a" by auto
1.52 -    then have "0 < - a" using A by (rule less_le_trans)
1.53 -    then show ?thesis by auto
1.54 -  qed
1.55 -next
1.56 -  assume A: "a \<le> 0" show "a \<le> - a"
1.57 -  proof (rule order_trans)
1.58 -    show "0 \<le> - a" using A by (simp add: minus_le_iff)
1.59 -  next
1.60 -    show "a \<le> 0" using A .
1.61 -  qed
1.62 -qed
1.63 -
1.64  lemma equal_neg_zero [simp]:
1.65    "a = - a \<longleftrightarrow> a = 0"
1.66  proof
1.67 @@ -1151,6 +1094,37 @@
1.68    "- a = a \<longleftrightarrow> a = 0"
1.69    by (auto dest: sym)
1.70
1.71 +lemma neg_less_eq_nonneg [simp]:
1.72 +  "- a \<le> a \<longleftrightarrow> 0 \<le> a"
1.73 +proof
1.74 +  assume A: "- a \<le> a" show "0 \<le> a"
1.75 +  proof (rule classical)
1.76 +    assume "\<not> 0 \<le> a"
1.77 +    then have "a < 0" by auto
1.78 +    with A have "- a < 0" by (rule le_less_trans)
1.79 +    then show ?thesis by auto
1.80 +  qed
1.81 +next
1.82 +  assume A: "0 \<le> a" show "- a \<le> a"
1.83 +  proof (rule order_trans)
1.84 +    show "- a \<le> 0" using A by (simp add: minus_le_iff)
1.85 +  next
1.86 +    show "0 \<le> a" using A .
1.87 +  qed
1.88 +qed
1.89 +
1.90 +lemma neg_less_pos [simp]:
1.91 +  "- a < a \<longleftrightarrow> 0 < a"
1.92 +  by (auto simp add: less_le)
1.93 +
1.94 +lemma less_eq_neg_nonpos [simp]:
1.95 +  "a \<le> - a \<longleftrightarrow> a \<le> 0"
1.96 +  using neg_less_eq_nonneg [of "- a"] by simp
1.97 +
1.98 +lemma less_neg_neg [simp]:
1.99 +  "a < - a \<longleftrightarrow> a < 0"
1.100 +  using neg_less_pos [of "- a"] by simp
1.101 +
1.102  lemma double_zero [simp]:
1.103    "a + a = 0 \<longleftrightarrow> a = 0"
1.104  proof
1.105 @@ -1169,7 +1143,7 @@
1.106    assume "0 < a + a"
1.107    then have "0 - a < a" by (simp only: diff_less_eq)
1.108    then have "- a < a" by simp
1.109 -  then show "0 < a" by (simp only: neg_less_nonneg)
1.110 +  then show "0 < a" by simp
1.111  next
1.112    assume "0 < a"
1.113    with this have "0 + 0 < a + a"
1.114 @@ -1197,14 +1171,6 @@
1.115    then show ?thesis by simp
1.116  qed
1.117
1.118 -lemma le_minus_self_iff:
1.119 -  "a \<le> - a \<longleftrightarrow> a \<le> 0"
1.120 -  by (fact less_eq_neg_nonpos)
1.121 -
1.122 -lemma minus_le_self_iff:
1.123 -  "- a \<le> a \<longleftrightarrow> 0 \<le> a"
1.124 -  by (fact neg_less_eq_nonneg)
1.125 -
1.126  lemma minus_max_eq_min:
1.127    "- max x y = min (-x) (-y)"
1.128    by (auto simp add: max_def min_def)
```