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.16 -instance  nat :: plus_ac0 (add_commute,add_assoc,add_0)
    1.17 +instance  nat :: div ..
    1.18 +instance  nat :: plus_ac0
    1.19 +proof qed (rule add_commute add_assoc add_0)+
    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"
    1.95 +    thus "P j" using m P by(simp add:add_ac mult_ac)
    1.96 +  qed
    1.97 +next
    1.98 +  assume Q: ?Q
    1.99 +  from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]
   1.100 +  show ?P by(simp add:mod_div_equality2)
   1.101 +qed
   1.102 +
   1.103  end