src/HOL/Rings.thy
changeset 60352 d46de31a50c4
parent 59910 815de5506080
child 60353 838025c6e278
     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:21 2015 +0200
     1.3 @@ -415,6 +415,33 @@
     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