src/HOL/Rings.thy
changeset 60429 d3d1e185cd63
parent 60353 838025c6e278
child 60516 0826b7025d07
     1.1 --- a/src/HOL/Rings.thy	Thu Jun 11 21:41:55 2015 +0100
     1.2 +++ b/src/HOL/Rings.thy	Fri Jun 12 08:53:23 2015 +0200
     1.3 @@ -559,7 +559,7 @@
     1.4  *}
     1.5  
     1.6  class divide =
     1.7 -  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
     1.8 +  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "div" 70)
     1.9  
    1.10  setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
    1.11  
    1.12 @@ -567,8 +567,8 @@
    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 +  shows distrib_left_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
    1.19 +    and distrib_right_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
    1.20    by (rule distrib_left distrib_right)+
    1.21  
    1.22  end
    1.23 @@ -577,8 +577,8 @@
    1.24  begin
    1.25  
    1.26  lemma [field_simps]:
    1.27 -  shows left_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
    1.28 -    and right_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
    1.29 +  shows left_diff_distrib_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
    1.30 +    and right_diff_distrib_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
    1.31    by (rule left_diff_distrib right_diff_distrib)+
    1.32  
    1.33  end
    1.34 @@ -586,12 +586,12 @@
    1.35  setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
    1.36  
    1.37  class semidom_divide = semidom + divide +
    1.38 -  assumes nonzero_mult_divide_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> divide (a * b) b = a"
    1.39 -  assumes divide_zero [simp]: "divide a 0 = 0"
    1.40 +  assumes nonzero_mult_divide_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> (a * b) div b = a"
    1.41 +  assumes divide_zero [simp]: "a div 0 = 0"
    1.42  begin
    1.43  
    1.44  lemma nonzero_mult_divide_cancel_left [simp]:
    1.45 -  "a \<noteq> 0 \<Longrightarrow> divide (a * b) a = b"
    1.46 +  "a \<noteq> 0 \<Longrightarrow> (a * b) div a = b"
    1.47    using nonzero_mult_divide_cancel_right [of a b] by (simp add: ac_simps)
    1.48  
    1.49  end