src/HOL/Divides.thy
changeset 21408 fff1731da03b
parent 21191 c00161fbf990
child 21911 e29bcab0c81c
     1.1 --- a/src/HOL/Divides.thy	Sat Nov 18 00:20:13 2006 +0100
     1.2 +++ b/src/HOL/Divides.thy	Sat Nov 18 00:20:15 2006 +0100
     1.3 @@ -7,40 +7,50 @@
     1.4  header {* The division operators div, mod and the divides relation "dvd" *}
     1.5  
     1.6  theory Divides
     1.7 -imports Datatype
     1.8 +imports Datatype Power
     1.9  begin
    1.10  
    1.11  (*We use the same class for div and mod;
    1.12    moreover, dvd is defined whenever multiplication is*)
    1.13 -axclass
    1.14 -  div < type
    1.15 +class div =
    1.16 +  fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.17 +  fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.18 +begin
    1.19 +
    1.20 +notation
    1.21 +  div (infixl "\<^loc>div" 70)
    1.22 +
    1.23 +notation
    1.24 +  mod (infixl "\<^loc>mod" 70)
    1.25 +
    1.26 +end
    1.27  
    1.28 -instance  nat :: div ..
    1.29 +notation
    1.30 +  div (infixl "div" 70)
    1.31 +
    1.32 +notation
    1.33 +  mod (infixl "mod" 70)
    1.34 +
    1.35 +instance nat :: "Divides.div"
    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 +  div_def:   "m div n == wfrec (trancl pred_nat) 
    1.39 +                          (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m" ..
    1.40 +
    1.41 +definition
    1.42 +  (*The definition of dvd is polymorphic!*)
    1.43 +  dvd  :: "'a::times \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd" 50) where
    1.44 +  dvd_def: "m dvd n \<longleftrightarrow> (\<exists>k. n = m*k)"
    1.45  
    1.46  consts
    1.47 -  div  :: "'a::div \<Rightarrow> 'a \<Rightarrow> 'a"          (infixl 70)
    1.48 -  mod  :: "'a::div \<Rightarrow> 'a \<Rightarrow> 'a"          (infixl 70)
    1.49 -  dvd  :: "'a::times \<Rightarrow> 'a \<Rightarrow> bool"      (infixl 50)
    1.50 -
    1.51 +  quorem :: "(nat*nat) * (nat*nat) => bool"
    1.52  
    1.53  defs
    1.54 -
    1.55 -  mod_def:   "m mod n == wfrec (trancl pred_nat)
    1.56 -                          (%f j. if j<n | n=0 then j else f (j-n)) m"
    1.57 -
    1.58 -  div_def:   "m div n == wfrec (trancl pred_nat) 
    1.59 -                          (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m"
    1.60 -
    1.61 -(*The definition of dvd is polymorphic!*)
    1.62 -  dvd_def:   "m dvd n == \<exists>k. n = m*k"
    1.63 -
    1.64 -(*This definition helps prove the harder properties of div and mod.
    1.65 -  It is copied from IntDiv.thy; should it be overloaded?*)
    1.66 -constdefs
    1.67 -  quorem :: "(nat*nat) * (nat*nat) => bool"
    1.68 -    "quorem == %((a,b), (q,r)).
    1.69 -                      a = b*q + r &
    1.70 -                      (if 0<b then 0\<le>r & r<b else b<r & r \<le>0)"
    1.71 +  (*This definition helps prove the harder properties of div and mod.
    1.72 +    It is copied from IntDiv.thy; should it be overloaded?*)
    1.73 +  quorem_def: "quorem \<equiv> (%((a,b), (q,r)).
    1.74 +                    a = b*q + r &
    1.75 +                    (if 0<b then 0\<le>r & r<b else b<r & r \<le>0))"
    1.76  
    1.77  
    1.78  
    1.79 @@ -187,8 +197,8 @@
    1.80  structure CancelDivModData =
    1.81  struct
    1.82  
    1.83 -val div_name = "Divides.op div";
    1.84 -val mod_name = "Divides.op mod";
    1.85 +val div_name = "Divides.div";
    1.86 +val mod_name = "Divides.mod";
    1.87  val mk_binop = HOLogic.mk_binop;
    1.88  val mk_sum = NatArithUtils.mk_sum;
    1.89  val dest_sum = NatArithUtils.dest_sum;
    1.90 @@ -266,7 +276,7 @@
    1.91  done
    1.92  
    1.93  lemma quorem_div_mod: "0 < b ==> quorem ((a, b), (a div b, a mod b))"
    1.94 -by (auto simp add: quorem_def)
    1.95 +  unfolding quorem_def by simp 
    1.96  
    1.97  lemma quorem_div: "[| quorem((a,b),(q,r));  0 < b |] ==> a div b = q"
    1.98  by (simp add: quorem_div_mod [THEN unique_quotient])
    1.99 @@ -651,6 +661,26 @@
   1.100  apply (simp only: dvd_eq_mod_eq_0)
   1.101  done
   1.102  
   1.103 +lemma le_imp_power_dvd: "!!i::nat. m \<le> n ==> i^m dvd i^n"
   1.104 +apply (unfold dvd_def)
   1.105 +apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
   1.106 +apply (simp add: power_add)
   1.107 +done
   1.108 +
   1.109 +lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)"
   1.110 +by (induct "n", auto)
   1.111 +
   1.112 +lemma power_le_dvd [rule_format]: "k^j dvd n --> i\<le>j --> k^i dvd (n::nat)"
   1.113 +apply (induct "j")
   1.114 +apply (simp_all add: le_Suc_eq)
   1.115 +apply (blast dest!: dvd_mult_right)
   1.116 +done
   1.117 +
   1.118 +lemma power_dvd_imp_le: "[|i^m dvd i^n;  (1::nat) < i|] ==> m \<le> n"
   1.119 +apply (rule power_le_imp_le_exp, assumption)
   1.120 +apply (erule dvd_imp_le, simp)
   1.121 +done
   1.122 +
   1.123  lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
   1.124  by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
   1.125