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.5  subclass linordered_cancel_ab_semigroup_add ..
     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)