src/HOL/Divides.thy

--- a/src/HOL/Divides.thy	Thu Jun 11 21:41:55 2015 +0100
+++ b/src/HOL/Divides.thy	Fri Jun 12 08:53:23 2015 +0200
@@ -9,19 +9,10 @@
 imports Parity
 begin
 
-subsection {* Syntactic division operations *}
+subsection {* Abstract division in commutative semirings. *}
 
 class div = dvd + divide +
   fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "mod" 70)
-begin
-
-abbreviation div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "div" 70)
-where
-  "op div \<equiv> divide"
-
-end
-
-subsection {* Abstract division in commutative semirings. *}
 
 class semiring_div = semidom + div +
   assumes mod_div_equality: "a div b * b + a mod b = a"
@@ -47,7 +38,7 @@
   "n \<noteq> 0 \<Longrightarrow> a ^ n = 0 \<longleftrightarrow> a = 0"
   using power_not_zero [of a n] by (auto simp add: zero_power)
 
-text {* @{const div} and @{const mod} *}
+text {* @{const divide} and @{const mod} *}
 
 lemma mod_div_equality2: "b * (a div b) + a mod b = a"
   unfolding mult.commute [of b]
@@ -874,7 +865,7 @@
 subsection {* Division on @{typ nat} *}
 
 text {*
-  We define @{const div} and @{const mod} on @{typ nat} by means
+  We define @{const divide} and @{const mod} on @{typ nat} by means
   of a characteristic relation with two input arguments
   @{term "m\<Colon>nat"}, @{term "n\<Colon>nat"} and two output arguments
   @{term "q\<Colon>nat"}(uotient) and @{term "r\<Colon>nat"}(emainder).
@@ -964,21 +955,14 @@
   shows "divmod_nat m n = qr"
   using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
 
-instantiation nat :: "Divides.div"
+instantiation nat :: semiring_div
 begin
 
 definition divide_nat where
-  div_nat_def: "divide m n = fst (divmod_nat m n)"
+  div_nat_def: "m div n = fst (divmod_nat m n)"
 
 definition mod_nat where
   "m mod n = snd (divmod_nat m n)"
-  
-instance ..
-
-end
-
-instantiation nat :: semiring_div
-begin
 
 lemma fst_divmod_nat [simp]:
   "fst (divmod_nat m n) = m div n"
@@ -1024,7 +1008,7 @@
     unfolding divmod_nat_rel_def using assms by auto
 qed
 
-text {* The ''recursion'' equations for @{const div} and @{const mod} *}
+text {* The ''recursion'' equations for @{const divide} and @{const mod} *}
 
 lemma div_less [simp]:
   fixes m n :: nat
@@ -1082,7 +1066,7 @@
   let (q, r) = divmod_nat (m - n) n in (Suc q, r))"
   by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
 
-text {* Simproc for cancelling @{const div} and @{const mod} *}
+text {* Simproc for cancelling @{const divide} and @{const mod} *}
 
 ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
 
@@ -1699,19 +1683,15 @@
                   if 0 < b then negDivAlg a b
                   else apsnd uminus (posDivAlg (-a) (-b)))"
 
-instantiation int :: Divides.div
+instantiation int :: ring_div
 begin
 
 definition divide_int where
-  div_int_def: "divide a b = fst (divmod_int a b)"
+  div_int_def: "a div b = fst (divmod_int a b)"
 
 definition mod_int where
   "a mod b = snd (divmod_int a b)"
 
-instance ..
-
-end
-
 lemma fst_divmod_int [simp]:
   "fst (divmod_int a b) = a div b"
   by (simp add: div_int_def)
@@ -1897,7 +1877,7 @@
 lemma mod_int_unique: "divmod_int_rel a b (q, r) \<Longrightarrow> a mod b = r"
   by (simp add: divmod_int_rel_div_mod [THEN unique_remainder])
 
-instance int :: ring_div
+instance
 proof
   fix a b :: int
   show "a div b * b + a mod b = a"
@@ -1932,6 +1912,8 @@
     by (rule div_int_unique, auto simp add: divmod_int_rel_def)
 qed
 
+end
+
 text{*Basic laws about division and remainder*}
 
 lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
@@ -2479,7 +2461,7 @@
                       split_neg_lemma [of concl: "%x y. P y"])
 done
 
-text {* Enable (lin)arith to deal with @{const div} and @{const mod}
+text {* Enable (lin)arith to deal with @{const divide} and @{const mod}
   when these are applied to some constant that is of the form
   @{term "numeral k"}: *}
 declare split_zdiv [of _ _ "numeral k", arith_split] for k