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.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")