# HG changeset patch
# User haftmann
# Date 1215759742 -7200
# Node ID dc38e79f5a1c6dd10856f715cf2da6e26140b648
# Parent  115d3a8bc6a6f7eef85a5977fbdac8dd318de6ae
separate class dvd for divisibility predicate

diff -r 115d3a8bc6a6 -r dc38e79f5a1c src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Jul 11 00:35:19 2008 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Jul 11 09:02:22 2008 +0200
@@ -140,17 +140,7 @@
 
 end
 
-instantiation up :: ("{times, one, comm_monoid_add, uminus, minus}") Divides.div
-begin
-
-definition "a div (b \<Colon> 'a up) = undefined a b"
-
-definition "a mod (b \<Colon> 'a up) = a - (a div b) * b"
-
-instance ..
-
-end
-
+instance up :: ("{times, comm_monoid_add}") Divides.dvd ..
 
 instantiation up :: ("{times, one, comm_monoid_add, uminus, minus}") inverse
 begin
@@ -366,9 +356,9 @@
   show "p / q = p * inverse q"
     by (simp add: up_divide_def)
   fix n
-  show "p ^ n = nat_rec 1 (%u b. b * p) n"
-    by (induct n) simp_all
-  qed
+  show "p ^ 0 = 1" by simp
+  show "p ^ Suc n = p ^ n * p" by simp
+qed
 
 (* Further properties of monom *)
 
diff -r 115d3a8bc6a6 -r dc38e79f5a1c src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Fri Jul 11 00:35:19 2008 +0200
+++ b/src/HOL/Divides.thy	Fri Jul 11 09:02:22 2008 +0200
@@ -4,7 +4,7 @@
     Copyright   1999  University of Cambridge
 *)
 
-header {* The division operators div,  mod and the divides relation dvd *}
+header {* The division operators div, mod and the divides relation dvd *}
 
 theory Divides
 imports Nat Power Product_Type
@@ -13,9 +13,7 @@
 
 subsection {* Syntactic division operations *}
 
-class div = times +
-  fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70)
-  fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)
+class dvd = times
 begin
 
 definition
@@ -25,9 +23,14 @@
 
 end
 
+class div = times +
+  fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70)
+  fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)
+
+
 subsection {* Abstract divisibility in commutative semirings. *}
 
-class semiring_div = comm_semiring_1_cancel + div + 
+class semiring_div = comm_semiring_1_cancel + dvd + div + 
   assumes mod_div_equality: "a div b * b + a mod b = a"
     and div_by_0: "a div 0 = 0"
     and mult_div: "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
diff -r 115d3a8bc6a6 -r dc38e79f5a1c src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Fri Jul 11 00:35:19 2008 +0200
+++ b/src/HOL/Presburger.thy	Fri Jul 11 09:02:22 2008 +0200
@@ -31,8 +31,8 @@
   "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<le> t) = True"
   "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x > t) = False"
   "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<ge> t) = False"
-  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.div})<z. (d dvd x + s) = (d dvd x + s)"
-  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.div})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
+  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.dvd})<z. (d dvd x + s) = (d dvd x + s)"
+  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.dvd})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
   "\<exists>z.\<forall>x<z. F = F"
   by ((erule exE, erule exE,rule_tac x="min z za" in exI,simp)+, (rule_tac x="t" in exI,fastsimp)+) simp_all
 
@@ -47,8 +47,8 @@
   "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<le> t) = False"
   "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x > t) = True"
   "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<ge> t) = True"
-  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.div})>z. (d dvd x + s) = (d dvd x + s)"
-  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.div})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
+  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.dvd})>z. (d dvd x + s) = (d dvd x + s)"
+  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.dvd})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
   "\<exists>z.\<forall>x>z. F = F"
   by ((erule exE, erule exE,rule_tac x="max z za" in exI,simp)+,(rule_tac x="t" in exI,fastsimp)+) simp_all
 
@@ -57,8 +57,8 @@
     \<Longrightarrow> \<forall>x k. (P x \<and> Q x) = (P (x - k*D) \<and> Q (x - k*D))"
   "\<lbrakk>\<forall>x k. P x = P (x - k*D); \<forall>x k. Q x = Q (x - k*D)\<rbrakk> 
     \<Longrightarrow> \<forall>x k. (P x \<or> Q x) = (P (x - k*D) \<or> Q (x - k*D))"
-  "(d::'a::{comm_ring,Divides.div}) dvd D \<Longrightarrow> \<forall>x k. (d dvd x + t) = (d dvd (x - k*D) + t)"
-  "(d::'a::{comm_ring,Divides.div}) dvd D \<Longrightarrow> \<forall>x k. (\<not>d dvd x + t) = (\<not>d dvd (x - k*D) + t)"
+  "(d::'a::{comm_ring,Divides.dvd}) dvd D \<Longrightarrow> \<forall>x k. (d dvd x + t) = (d dvd (x - k*D) + t)"
+  "(d::'a::{comm_ring,Divides.dvd}) dvd D \<Longrightarrow> \<forall>x k. (\<not>d dvd x + t) = (\<not>d dvd (x - k*D) + t)"
   "\<forall>x k. F = F"
 by simp_all
   (clarsimp simp add: dvd_def, rule iffI, clarsimp,rule_tac x = "kb - ka*k" in exI,
@@ -360,7 +360,7 @@
 apply(fastsimp)
 done
 
-theorem unity_coeff_ex: "(\<exists>(x::'a::{semiring_0,Divides.div}). P (l * x)) \<equiv> (\<exists>x. l dvd (x + 0) \<and> P x)"
+theorem unity_coeff_ex: "(\<exists>(x::'a::{semiring_0,Divides.dvd}). P (l * x)) \<equiv> (\<exists>x. l dvd (x + 0) \<and> P x)"
   apply (rule eq_reflection[symmetric])
   apply (rule iffI)
   defer