src/HOL/Rings.thy
changeset 64164 38c407446400
parent 63950 cdc1e59aa513
child 64239 de5cd9217d4c
     1.1 --- a/src/HOL/Rings.thy	Tue Oct 11 16:44:13 2016 +0200
     1.2 +++ b/src/HOL/Rings.thy	Wed Oct 12 20:38:47 2016 +0200
     1.3 @@ -571,11 +571,6 @@
     1.4  
     1.5  setup \<open>Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"})\<close>
     1.6  
     1.7 -text \<open>Syntactic division remainder operator\<close>
     1.8 -
     1.9 -class modulo = dvd + divide +
    1.10 -  fixes modulo :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "mod" 70)
    1.11 -
    1.12  text \<open>Algebraic classes with division\<close>
    1.13    
    1.14  class semidom_divide = semidom + divide +
    1.15 @@ -1286,6 +1281,53 @@
    1.16  
    1.17  end
    1.18  
    1.19 +
    1.20 +text \<open>Syntactic division remainder operator\<close>
    1.21 +
    1.22 +class modulo = dvd + divide +
    1.23 +  fixes modulo :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "mod" 70)
    1.24 +
    1.25 +text \<open>Arbitrary quotient and remainder partitions\<close>
    1.26 +
    1.27 +class semiring_modulo = comm_semiring_1_cancel + divide + modulo +
    1.28 +  assumes mod_div_equality: "a div b * b + a mod b = a"
    1.29 +begin
    1.30 +
    1.31 +lemma mod_div_decomp:
    1.32 +  fixes a b
    1.33 +  obtains q r where "q = a div b" and "r = a mod b"
    1.34 +    and "a = q * b + r"
    1.35 +proof -
    1.36 +  from mod_div_equality have "a = a div b * b + a mod b" by simp
    1.37 +  moreover have "a div b = a div b" ..
    1.38 +  moreover have "a mod b = a mod b" ..
    1.39 +  note that ultimately show thesis by blast
    1.40 +qed
    1.41 +
    1.42 +lemma mod_div_equality2: "b * (a div b) + a mod b = a"
    1.43 +  using mod_div_equality [of a b] by (simp add: ac_simps)
    1.44 +
    1.45 +lemma mod_div_equality3: "a mod b + a div b * b = a"
    1.46 +  using mod_div_equality [of a b] by (simp add: ac_simps)
    1.47 +
    1.48 +lemma mod_div_equality4: "a mod b + b * (a div b) = a"
    1.49 +  using mod_div_equality [of a b] by (simp add: ac_simps)
    1.50 +
    1.51 +lemma minus_div_eq_mod: "a - a div b * b = a mod b"
    1.52 +  by (rule add_implies_diff [symmetric]) (fact mod_div_equality3)
    1.53 +
    1.54 +lemma minus_div_eq_mod2: "a - b * (a div b) = a mod b"
    1.55 +  by (rule add_implies_diff [symmetric]) (fact mod_div_equality4)
    1.56 +
    1.57 +lemma minus_mod_eq_div: "a - a mod b = a div b * b"
    1.58 +  by (rule add_implies_diff [symmetric]) (fact mod_div_equality)
    1.59 +
    1.60 +lemma minus_mod_eq_div2: "a - a mod b = b * (a div b)"
    1.61 +  by (rule add_implies_diff [symmetric]) (fact mod_div_equality2)
    1.62 +
    1.63 +end
    1.64 +  
    1.65 +
    1.66  class ordered_semiring = semiring + ordered_comm_monoid_add +
    1.67    assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
    1.68    assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"