src/HOL/Rings.thy
changeset 63950 cdc1e59aa513
parent 63947 559f0882d6a6
child 64164 38c407446400
     1.1 --- a/src/HOL/Rings.thy	Mon Sep 26 07:56:54 2016 +0200
     1.2 +++ b/src/HOL/Rings.thy	Mon Sep 26 07:56:54 2016 +0200
     1.3 @@ -542,6 +542,8 @@
     1.4      \<^item> \<^emph>\<open>Algebra I\<close> by van der Waerden, Springer
     1.5  \<close>
     1.6  
     1.7 +text \<open>Syntactic division operator\<close>
     1.8 +
     1.9  class divide =
    1.10    fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "div" 70)
    1.11  
    1.12 @@ -569,6 +571,13 @@
    1.13  
    1.14  setup \<open>Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"})\<close>
    1.15  
    1.16 +text \<open>Syntactic division remainder operator\<close>
    1.17 +
    1.18 +class modulo = dvd + divide +
    1.19 +  fixes modulo :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "mod" 70)
    1.20 +
    1.21 +text \<open>Algebraic classes with division\<close>
    1.22 +  
    1.23  class semidom_divide = semidom + divide +
    1.24    assumes nonzero_mult_divide_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> (a * b) div b = a"
    1.25    assumes divide_zero [simp]: "a div 0 = 0"