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