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"
```