src/HOL/Divides.thy
 changeset 13152 2a54f99b44b3 parent 12338 de0f4a63baa5 child 13189 81ed5c6de890
```     1.1 --- a/src/HOL/Divides.thy	Wed May 15 11:51:20 2002 +0200
1.2 +++ b/src/HOL/Divides.thy	Wed May 15 13:49:51 2002 +0200
1.3 @@ -6,35 +6,33 @@
1.4  The division operators div, mod and the divides relation "dvd"
1.5  *)
1.6
1.7 -Divides = NatArith +
1.8 +theory Divides = NatArith files("Divides_lemmas.ML"):
1.9
1.10  (*We use the same class for div and mod;
1.11    moreover, dvd is defined whenever multiplication is*)
1.12  axclass
1.13    div < type
1.14
1.15 -instance  nat :: div
1.17 +instance  nat :: div ..
1.18 +instance  nat :: plus_ac0
1.20
1.21  consts
1.22 -  div  :: ['a::div, 'a]  => 'a          (infixl 70)
1.23 -  mod  :: ['a::div, 'a]  => 'a          (infixl 70)
1.24 -  dvd  :: ['a::times, 'a] => bool       (infixl 50)
1.25 +  div  :: "'a::div \<Rightarrow> 'a \<Rightarrow> 'a"          (infixl 70)
1.26 +  mod  :: "'a::div \<Rightarrow> 'a \<Rightarrow> 'a"          (infixl 70)
1.27 +  dvd  :: "'a::times \<Rightarrow> 'a \<Rightarrow> bool"      (infixl 50)
1.28
1.29
1.30 -(*Remainder and quotient are defined here by algorithms and later proved to
1.31 -  satisfy the traditional definition (theorem mod_div_equality)
1.32 -*)
1.33  defs
1.34
1.35 -  mod_def   "m mod n == wfrec (trancl pred_nat)
1.36 +  mod_def:   "m mod n == wfrec (trancl pred_nat)
1.37                            (%f j. if j<n | n=0 then j else f (j-n)) m"
1.38
1.39 -  div_def   "m div n == wfrec (trancl pred_nat)
1.40 +  div_def:   "m div n == wfrec (trancl pred_nat)
1.41                            (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m"
1.42
1.43  (*The definition of dvd is polymorphic!*)
1.44 -  dvd_def   "m dvd n == EX k. n = m*k"
1.45 +  dvd_def:   "m dvd n == EX k. n = m*k"
1.46
1.47  (*This definition helps prove the harder properties of div and mod.
1.48    It is copied from IntDiv.thy; should it be overloaded?*)
1.49 @@ -44,4 +42,54 @@
1.50                        a = b*q + r &
1.51                        (if 0<b then 0<=r & r<b else b<r & r <=0)"
1.52
1.53 +use "Divides_lemmas.ML"
1.54 +
1.55 +lemma mod_div_equality2: "n * (m div n) + m mod n = (m::nat)"
1.56 +apply(insert mod_div_equality[of m n])
1.57 +apply(simp only:mult_ac)
1.58 +done
1.59 +
1.60 +lemma split_div:
1.61 +assumes m: "m \<noteq> 0"
1.62 +shows "P(n div m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P i)"
1.63 +       (is "?P = ?Q")
1.64 +proof
1.65 +  assume P: ?P
1.66 +  show ?Q
1.67 +  proof (intro allI impI)
1.68 +    fix i j
1.69 +    assume n: "n = m*i + j" and j: "j < m"
1.70 +    show "P i"
1.71 +    proof (cases)
1.72 +      assume "i = 0"
1.73 +      with n j P show "P i" by simp
1.74 +    next
1.75 +      assume "i \<noteq> 0"
1.76 +      with n j P show "P i" by (simp add:add_ac div_mult_self1)
1.77 +    qed
1.78 +  qed
1.79 +next
1.80 +  assume Q: ?Q
1.81 +  from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]
1.82 +  show ?P by(simp add:mod_div_equality2)
1.83 +qed
1.84 +
1.85 +lemma split_mod:
1.86 +assumes m: "m \<noteq> 0"
1.87 +shows "P(n mod m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P j)"
1.88 +       (is "?P = ?Q")
1.89 +proof
1.90 +  assume P: ?P
1.91 +  show ?Q
1.92 +  proof (intro allI impI)
1.93 +    fix i j
1.94 +    assume "n = m*i + j" "j < m"