src/HOL/Rings.thy
changeset 60353 838025c6e278
parent 60352 d46de31a50c4
child 60429 d3d1e185cd63
     1.1 --- a/src/HOL/Rings.thy	Mon Jun 01 18:59:21 2015 +0200
     1.2 +++ b/src/HOL/Rings.thy	Mon Jun 01 18:59:22 2015 +0200
     1.3 @@ -415,33 +415,6 @@
     1.4  
     1.5  end
     1.6  
     1.7 -class divide =
     1.8 -  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
     1.9 -
    1.10 -setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
    1.11 -
    1.12 -context semiring
    1.13 -begin
    1.14 -
    1.15 -lemma [field_simps]:
    1.16 -  shows distrib_left_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
    1.17 -    and distrib_right_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
    1.18 -  by (rule distrib_left distrib_right)+
    1.19 -
    1.20 -end
    1.21 -
    1.22 -context ring
    1.23 -begin
    1.24 -
    1.25 -lemma [field_simps]:
    1.26 -  shows left_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
    1.27 -    and right_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
    1.28 -  by (rule left_diff_distrib right_diff_distrib)+
    1.29 -
    1.30 -end
    1.31 -
    1.32 -setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
    1.33 -  
    1.34  class semiring_no_zero_divisors = semiring_0 +
    1.35    assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
    1.36  begin
    1.37 @@ -585,6 +558,46 @@
    1.38    \end{itemize}
    1.39  *}
    1.40  
    1.41 +class divide =
    1.42 +  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.43 +
    1.44 +setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
    1.45 +
    1.46 +context semiring
    1.47 +begin
    1.48 +
    1.49 +lemma [field_simps]:
    1.50 +  shows distrib_left_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
    1.51 +    and distrib_right_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
    1.52 +  by (rule distrib_left distrib_right)+
    1.53 +
    1.54 +end
    1.55 +
    1.56 +context ring
    1.57 +begin
    1.58 +
    1.59 +lemma [field_simps]:
    1.60 +  shows left_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
    1.61 +    and right_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
    1.62 +  by (rule left_diff_distrib right_diff_distrib)+
    1.63 +
    1.64 +end
    1.65 +
    1.66 +setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
    1.67 +
    1.68 +class semidom_divide = semidom + divide +
    1.69 +  assumes nonzero_mult_divide_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> divide (a * b) b = a"
    1.70 +  assumes divide_zero [simp]: "divide a 0 = 0"
    1.71 +begin
    1.72 +
    1.73 +lemma nonzero_mult_divide_cancel_left [simp]:
    1.74 +  "a \<noteq> 0 \<Longrightarrow> divide (a * b) a = b"
    1.75 +  using nonzero_mult_divide_cancel_right [of a b] by (simp add: ac_simps)
    1.76 +
    1.77 +end
    1.78 +
    1.79 +class idom_divide = idom + semidom_divide
    1.80 +
    1.81  class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +
    1.82    assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
    1.83    assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"