src/HOL/Divides.thy
changeset 60429 d3d1e185cd63
parent 60353 838025c6e278
child 60516 0826b7025d07
     1.1 --- a/src/HOL/Divides.thy	Thu Jun 11 21:41:55 2015 +0100
     1.2 +++ b/src/HOL/Divides.thy	Fri Jun 12 08:53:23 2015 +0200
     1.3 @@ -9,19 +9,10 @@
     1.4  imports Parity
     1.5  begin
     1.6  
     1.7 -subsection {* Syntactic division operations *}
     1.8 +subsection {* Abstract division in commutative semirings. *}
     1.9  
    1.10  class div = dvd + divide +
    1.11    fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "mod" 70)
    1.12 -begin
    1.13 -
    1.14 -abbreviation div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "div" 70)
    1.15 -where
    1.16 -  "op div \<equiv> divide"
    1.17 -
    1.18 -end
    1.19 -
    1.20 -subsection {* Abstract division in commutative semirings. *}
    1.21  
    1.22  class semiring_div = semidom + div +
    1.23    assumes mod_div_equality: "a div b * b + a mod b = a"
    1.24 @@ -47,7 +38,7 @@
    1.25    "n \<noteq> 0 \<Longrightarrow> a ^ n = 0 \<longleftrightarrow> a = 0"
    1.26    using power_not_zero [of a n] by (auto simp add: zero_power)
    1.27  
    1.28 -text {* @{const div} and @{const mod} *}
    1.29 +text {* @{const divide} and @{const mod} *}
    1.30  
    1.31  lemma mod_div_equality2: "b * (a div b) + a mod b = a"
    1.32    unfolding mult.commute [of b]
    1.33 @@ -874,7 +865,7 @@
    1.34  subsection {* Division on @{typ nat} *}
    1.35  
    1.36  text {*
    1.37 -  We define @{const div} and @{const mod} on @{typ nat} by means
    1.38 +  We define @{const divide} and @{const mod} on @{typ nat} by means
    1.39    of a characteristic relation with two input arguments
    1.40    @{term "m\<Colon>nat"}, @{term "n\<Colon>nat"} and two output arguments
    1.41    @{term "q\<Colon>nat"}(uotient) and @{term "r\<Colon>nat"}(emainder).
    1.42 @@ -964,21 +955,14 @@
    1.43    shows "divmod_nat m n = qr"
    1.44    using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
    1.45  
    1.46 -instantiation nat :: "Divides.div"
    1.47 +instantiation nat :: semiring_div
    1.48  begin
    1.49  
    1.50  definition divide_nat where
    1.51 -  div_nat_def: "divide m n = fst (divmod_nat m n)"
    1.52 +  div_nat_def: "m div n = fst (divmod_nat m n)"
    1.53  
    1.54  definition mod_nat where
    1.55    "m mod n = snd (divmod_nat m n)"
    1.56 -  
    1.57 -instance ..
    1.58 -
    1.59 -end
    1.60 -
    1.61 -instantiation nat :: semiring_div
    1.62 -begin
    1.63  
    1.64  lemma fst_divmod_nat [simp]:
    1.65    "fst (divmod_nat m n) = m div n"
    1.66 @@ -1024,7 +1008,7 @@
    1.67      unfolding divmod_nat_rel_def using assms by auto
    1.68  qed
    1.69  
    1.70 -text {* The ''recursion'' equations for @{const div} and @{const mod} *}
    1.71 +text {* The ''recursion'' equations for @{const divide} and @{const mod} *}
    1.72  
    1.73  lemma div_less [simp]:
    1.74    fixes m n :: nat
    1.75 @@ -1082,7 +1066,7 @@
    1.76    let (q, r) = divmod_nat (m - n) n in (Suc q, r))"
    1.77    by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
    1.78  
    1.79 -text {* Simproc for cancelling @{const div} and @{const mod} *}
    1.80 +text {* Simproc for cancelling @{const divide} and @{const mod} *}
    1.81  
    1.82  ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
    1.83  
    1.84 @@ -1699,19 +1683,15 @@
    1.85                    if 0 < b then negDivAlg a b
    1.86                    else apsnd uminus (posDivAlg (-a) (-b)))"
    1.87  
    1.88 -instantiation int :: Divides.div
    1.89 +instantiation int :: ring_div
    1.90  begin
    1.91  
    1.92  definition divide_int where
    1.93 -  div_int_def: "divide a b = fst (divmod_int a b)"
    1.94 +  div_int_def: "a div b = fst (divmod_int a b)"
    1.95  
    1.96  definition mod_int where
    1.97    "a mod b = snd (divmod_int a b)"
    1.98  
    1.99 -instance ..
   1.100 -
   1.101 -end
   1.102 -
   1.103  lemma fst_divmod_int [simp]:
   1.104    "fst (divmod_int a b) = a div b"
   1.105    by (simp add: div_int_def)
   1.106 @@ -1897,7 +1877,7 @@
   1.107  lemma mod_int_unique: "divmod_int_rel a b (q, r) \<Longrightarrow> a mod b = r"
   1.108    by (simp add: divmod_int_rel_div_mod [THEN unique_remainder])
   1.109  
   1.110 -instance int :: ring_div
   1.111 +instance
   1.112  proof
   1.113    fix a b :: int
   1.114    show "a div b * b + a mod b = a"
   1.115 @@ -1932,6 +1912,8 @@
   1.116      by (rule div_int_unique, auto simp add: divmod_int_rel_def)
   1.117  qed
   1.118  
   1.119 +end
   1.120 +
   1.121  text{*Basic laws about division and remainder*}
   1.122  
   1.123  lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
   1.124 @@ -2479,7 +2461,7 @@
   1.125                        split_neg_lemma [of concl: "%x y. P y"])
   1.126  done
   1.127  
   1.128 -text {* Enable (lin)arith to deal with @{const div} and @{const mod}
   1.129 +text {* Enable (lin)arith to deal with @{const divide} and @{const mod}
   1.130    when these are applied to some constant that is of the form
   1.131    @{term "numeral k"}: *}
   1.132  declare split_zdiv [of _ _ "numeral k", arith_split] for k