src/HOL/Rings.thy
changeset 62378 85ed00c1fe7c
parent 62377 ace69956d018
child 62390 842917225d56
     1.1 --- a/src/HOL/Rings.thy	Fri Feb 12 16:09:07 2016 +0100
     1.2 +++ b/src/HOL/Rings.thy	Fri Feb 19 13:40:50 2016 +0100
     1.3 @@ -1312,7 +1312,7 @@
     1.4  lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0"
     1.5  by (drule mult_right_mono [of b 0], auto)
     1.6  
     1.7 -lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0"
     1.8 +lemma split_mult_neg_le: "(0 \<le> a \<and> b \<le> 0) \<or> (a \<le> 0 \<and> 0 \<le> b) \<Longrightarrow> a * b \<le> 0"
     1.9  by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
    1.10  
    1.11  end
    1.12 @@ -1735,17 +1735,51 @@
    1.13  
    1.14  end
    1.15  
    1.16 -class linordered_semidom = semidom + linordered_comm_semiring_strict +
    1.17 +class zero_less_one = order + zero + one +
    1.18    assumes zero_less_one [simp]: "0 < 1"
    1.19 +
    1.20 +class linordered_nonzero_semiring = ordered_comm_semiring + monoid_mult + linorder + zero_less_one
    1.21 +begin
    1.22 +
    1.23 +subclass zero_neq_one
    1.24 +  proof qed (insert zero_less_one, blast)
    1.25 +
    1.26 +subclass comm_semiring_1
    1.27 +  proof qed (rule mult_1_left)
    1.28 +
    1.29 +lemma zero_le_one [simp]: "0 \<le> 1"
    1.30 +by (rule zero_less_one [THEN less_imp_le])
    1.31 +
    1.32 +lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
    1.33 +by (simp add: not_le)
    1.34 +
    1.35 +lemma not_one_less_zero [simp]: "\<not> 1 < 0"
    1.36 +by (simp add: not_less)
    1.37 +
    1.38 +lemma mult_left_le: "c \<le> 1 \<Longrightarrow> 0 \<le> a \<Longrightarrow> a * c \<le> a"
    1.39 +  using mult_left_mono[of c 1 a] by simp
    1.40 +
    1.41 +lemma mult_le_one: "a \<le> 1 \<Longrightarrow> 0 \<le> b \<Longrightarrow> b \<le> 1 \<Longrightarrow> a * b \<le> 1"
    1.42 +  using mult_mono[of a 1 b 1] by simp
    1.43 +
    1.44 +lemma zero_less_two: "0 < 1 + 1"
    1.45 +  using add_pos_pos[OF zero_less_one zero_less_one] .
    1.46 +
    1.47 +end
    1.48 +
    1.49 +class linordered_semidom = semidom + linordered_comm_semiring_strict + zero_less_one +
    1.50    assumes le_add_diff_inverse2 [simp]: "b \<le> a \<Longrightarrow> a - b + b = a"
    1.51  begin
    1.52  
    1.53 +subclass linordered_nonzero_semiring
    1.54 +  proof qed
    1.55 +
    1.56  text \<open>Addition is the inverse of subtraction.\<close>
    1.57  
    1.58  lemma le_add_diff_inverse [simp]: "b \<le> a \<Longrightarrow> b + (a - b) = a"
    1.59    by (frule le_add_diff_inverse2) (simp add: add.commute)
    1.60  
    1.61 -lemma add_diff_inverse: "~ a<b \<Longrightarrow> b + (a - b) = a"
    1.62 +lemma add_diff_inverse: "\<not> a < b \<Longrightarrow> b + (a - b) = a"
    1.63    by simp
    1.64  
    1.65  lemma add_le_imp_le_diff:
    1.66 @@ -1771,36 +1805,14 @@
    1.67      by (simp add: add.commute diff_diff_add)
    1.68  qed
    1.69  
    1.70 -lemma pos_add_strict:
    1.71 -  shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
    1.72 -  using add_strict_mono [of 0 a b c] by simp
    1.73 -
    1.74 -lemma zero_le_one [simp]: "0 \<le> 1"
    1.75 -by (rule zero_less_one [THEN less_imp_le])
    1.76 -
    1.77 -lemma not_one_le_zero [simp]: "\<not> 1 \<le> 0"
    1.78 -by (simp add: not_le)
    1.79 -
    1.80 -lemma not_one_less_zero [simp]: "\<not> 1 < 0"
    1.81 -by (simp add: not_less)
    1.82 -
    1.83  lemma less_1_mult:
    1.84 -  assumes "1 < m" and "1 < n"
    1.85 -  shows "1 < m * n"
    1.86 -  using assms mult_strict_mono [of 1 m 1 n]
    1.87 -    by (simp add:  less_trans [OF zero_less_one])
    1.88 -
    1.89 -lemma mult_left_le: "c \<le> 1 \<Longrightarrow> 0 \<le> a \<Longrightarrow> a * c \<le> a"
    1.90 -  using mult_left_mono[of c 1 a] by simp
    1.91 -
    1.92 -lemma mult_le_one: "a \<le> 1 \<Longrightarrow> 0 \<le> b \<Longrightarrow> b \<le> 1 \<Longrightarrow> a * b \<le> 1"
    1.93 -  using mult_mono[of a 1 b 1] by simp
    1.94 +  "1 < m \<Longrightarrow> 1 < n \<Longrightarrow> 1 < m * n"
    1.95 +  using mult_strict_mono [of 1 m 1 n] by (simp add: less_trans [OF zero_less_one])
    1.96  
    1.97  end
    1.98  
    1.99 -class linordered_idom = comm_ring_1 +
   1.100 -  linordered_comm_semiring_strict + ordered_ab_group_add +
   1.101 -  abs_if + sgn_if
   1.102 +class linordered_idom =
   1.103 +  comm_ring_1 + linordered_comm_semiring_strict + ordered_ab_group_add + abs_if + sgn_if
   1.104  begin
   1.105  
   1.106  subclass linordered_semiring_1_strict ..
   1.107 @@ -1962,9 +1974,6 @@
   1.108    thus ?thesis by simp
   1.109  qed
   1.110  
   1.111 -lemma zero_less_two: "0 < 1 + 1"
   1.112 -by (blast intro: less_trans zero_less_one less_add_one)
   1.113 -
   1.114  end
   1.115  
   1.116  context linordered_idom