src/HOL/Groups.thy
changeset 62378 85ed00c1fe7c
parent 62377 ace69956d018
child 62379 340738057c8c
     1.1 --- a/src/HOL/Groups.thy	Fri Feb 12 16:09:07 2016 +0100
     1.2 +++ b/src/HOL/Groups.thy	Fri Feb 19 13:40:50 2016 +0100
     1.3 @@ -753,6 +753,13 @@
     1.4  end
     1.5  
     1.6  class strict_ordered_comm_monoid_add = comm_monoid_add + strict_ordered_ab_semigroup_add
     1.7 +begin
     1.8 +
     1.9 +lemma pos_add_strict:
    1.10 +  shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
    1.11 +  using add_strict_mono [of 0 a b c] by simp
    1.12 +
    1.13 +end
    1.14  
    1.15  class ordered_cancel_comm_monoid_add = ordered_comm_monoid_add + cancel_ab_semigroup_add
    1.16  begin
    1.17 @@ -1311,15 +1318,37 @@
    1.18    assumes le_iff_add: "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)"
    1.19  begin
    1.20  
    1.21 -lemma zero_le: "0 \<le> x"
    1.22 +lemma zero_le[simp]: "0 \<le> x"
    1.23    by (auto simp: le_iff_add)
    1.24  
    1.25 +lemma le_zero_eq[simp]: "n \<le> 0 \<longleftrightarrow> n = 0"
    1.26 +  by (auto intro: antisym)
    1.27 +
    1.28 +lemma not_less_zero[simp]: "\<not> n < 0"
    1.29 +  by (auto simp: less_le)
    1.30 +
    1.31 +lemma zero_less_iff_neq_zero: "(0 < n) \<longleftrightarrow> (n \<noteq> 0)"
    1.32 +  by (auto simp: less_le)
    1.33 +
    1.34 +text \<open>This theorem is useful with \<open>blast\<close>\<close>
    1.35 +lemma gr_zeroI: "(n = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < n"
    1.36 +  by (rule zero_less_iff_neq_zero[THEN iffD2]) iprover
    1.37 +
    1.38 +lemma not_gr_zero[simp]: "(\<not> (0 < n)) \<longleftrightarrow> (n = 0)"
    1.39 +  by (simp add: zero_less_iff_neq_zero)
    1.40 +
    1.41  subclass ordered_comm_monoid_add
    1.42    proof qed (auto simp: le_iff_add add_ac)
    1.43  
    1.44  lemma add_eq_0_iff_both_eq_0: "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
    1.45    by (intro add_nonneg_eq_0_iff zero_le)
    1.46  
    1.47 +lemma gr_implies_not_zero: "m < n \<Longrightarrow> n \<noteq> 0"
    1.48 +  using add_eq_0_iff_both_eq_0[of m] by (auto simp: le_iff_add less_le)
    1.49 +
    1.50 +lemmas zero_order = zero_le le_zero_eq not_less_zero zero_less_iff_neq_zero not_gr_zero
    1.51 +  -- \<open>This should be attributed with \<open>[iff]\<close>, but then \<open>blast\<close> fails in \<open>Set\<close>.\<close>
    1.52 +
    1.53  end
    1.54  
    1.55  class ordered_cancel_comm_monoid_diff =