author haftmann Fri Jul 11 09:02:22 2008 +0200 (2008-07-11) changeset 27540 dc38e79f5a1c parent 27539 115d3a8bc6a6 child 27541 9e585e99b494
separate class dvd for divisibility predicate
 src/HOL/Algebra/poly/UnivPoly2.thy file | annotate | diff | revisions src/HOL/Divides.thy file | annotate | diff | revisions src/HOL/Presburger.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Jul 11 00:35:19 2008 +0200
1.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Jul 11 09:02:22 2008 +0200
1.3 @@ -140,17 +140,7 @@
1.4
1.5  end
1.6
1.7 -instantiation up :: ("{times, one, comm_monoid_add, uminus, minus}") Divides.div
1.8 -begin
1.9 -
1.10 -definition "a div (b \<Colon> 'a up) = undefined a b"
1.11 -
1.12 -definition "a mod (b \<Colon> 'a up) = a - (a div b) * b"
1.13 -
1.14 -instance ..
1.15 -
1.16 -end
1.17 -
1.18 +instance up :: ("{times, comm_monoid_add}") Divides.dvd ..
1.19
1.20  instantiation up :: ("{times, one, comm_monoid_add, uminus, minus}") inverse
1.21  begin
1.22 @@ -366,9 +356,9 @@
1.23    show "p / q = p * inverse q"
1.25    fix n
1.26 -  show "p ^ n = nat_rec 1 (%u b. b * p) n"
1.27 -    by (induct n) simp_all
1.28 -  qed
1.29 +  show "p ^ 0 = 1" by simp
1.30 +  show "p ^ Suc n = p ^ n * p" by simp
1.31 +qed
1.32
1.33  (* Further properties of monom *)
1.34
```
```     2.1 --- a/src/HOL/Divides.thy	Fri Jul 11 00:35:19 2008 +0200
2.2 +++ b/src/HOL/Divides.thy	Fri Jul 11 09:02:22 2008 +0200
2.3 @@ -4,7 +4,7 @@
2.4      Copyright   1999  University of Cambridge
2.5  *)
2.6
2.7 -header {* The division operators div,  mod and the divides relation dvd *}
2.8 +header {* The division operators div, mod and the divides relation dvd *}
2.9
2.10  theory Divides
2.11  imports Nat Power Product_Type
2.12 @@ -13,9 +13,7 @@
2.13
2.14  subsection {* Syntactic division operations *}
2.15
2.16 -class div = times +
2.17 -  fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70)
2.18 -  fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)
2.19 +class dvd = times
2.20  begin
2.21
2.22  definition
2.23 @@ -25,9 +23,14 @@
2.24
2.25  end
2.26
2.27 +class div = times +
2.28 +  fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70)
2.29 +  fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)
2.30 +
2.31 +
2.32  subsection {* Abstract divisibility in commutative semirings. *}
2.33
2.34 -class semiring_div = comm_semiring_1_cancel + div +
2.35 +class semiring_div = comm_semiring_1_cancel + dvd + div +
2.36    assumes mod_div_equality: "a div b * b + a mod b = a"
2.37      and div_by_0: "a div 0 = 0"
2.38      and mult_div: "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
```
```     3.1 --- a/src/HOL/Presburger.thy	Fri Jul 11 00:35:19 2008 +0200
3.2 +++ b/src/HOL/Presburger.thy	Fri Jul 11 09:02:22 2008 +0200
3.3 @@ -31,8 +31,8 @@
3.4    "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<le> t) = True"
3.5    "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x > t) = False"
3.6    "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<ge> t) = False"
3.7 -  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.div})<z. (d dvd x + s) = (d dvd x + s)"
3.8 -  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.div})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
3.9 +  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.dvd})<z. (d dvd x + s) = (d dvd x + s)"
3.10 +  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.dvd})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
3.11    "\<exists>z.\<forall>x<z. F = F"
3.12    by ((erule exE, erule exE,rule_tac x="min z za" in exI,simp)+, (rule_tac x="t" in exI,fastsimp)+) simp_all
3.13
3.14 @@ -47,8 +47,8 @@
3.15    "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<le> t) = False"
3.16    "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x > t) = True"
3.17    "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<ge> t) = True"
3.18 -  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.div})>z. (d dvd x + s) = (d dvd x + s)"
3.19 -  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.div})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
3.20 +  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.dvd})>z. (d dvd x + s) = (d dvd x + s)"
3.21 +  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.dvd})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
3.22    "\<exists>z.\<forall>x>z. F = F"
3.23    by ((erule exE, erule exE,rule_tac x="max z za" in exI,simp)+,(rule_tac x="t" in exI,fastsimp)+) simp_all
3.24
3.25 @@ -57,8 +57,8 @@
3.26      \<Longrightarrow> \<forall>x k. (P x \<and> Q x) = (P (x - k*D) \<and> Q (x - k*D))"
3.27    "\<lbrakk>\<forall>x k. P x = P (x - k*D); \<forall>x k. Q x = Q (x - k*D)\<rbrakk>
3.28      \<Longrightarrow> \<forall>x k. (P x \<or> Q x) = (P (x - k*D) \<or> Q (x - k*D))"
3.29 -  "(d::'a::{comm_ring,Divides.div}) dvd D \<Longrightarrow> \<forall>x k. (d dvd x + t) = (d dvd (x - k*D) + t)"
3.30 -  "(d::'a::{comm_ring,Divides.div}) dvd D \<Longrightarrow> \<forall>x k. (\<not>d dvd x + t) = (\<not>d dvd (x - k*D) + t)"
3.31 +  "(d::'a::{comm_ring,Divides.dvd}) dvd D \<Longrightarrow> \<forall>x k. (d dvd x + t) = (d dvd (x - k*D) + t)"
3.32 +  "(d::'a::{comm_ring,Divides.dvd}) dvd D \<Longrightarrow> \<forall>x k. (\<not>d dvd x + t) = (\<not>d dvd (x - k*D) + t)"
3.33    "\<forall>x k. F = F"
3.34  by simp_all
3.35    (clarsimp simp add: dvd_def, rule iffI, clarsimp,rule_tac x = "kb - ka*k" in exI,
3.36 @@ -360,7 +360,7 @@
3.37  apply(fastsimp)
3.38  done
3.39
3.40 -theorem unity_coeff_ex: "(\<exists>(x::'a::{semiring_0,Divides.div}). P (l * x)) \<equiv> (\<exists>x. l dvd (x + 0) \<and> P x)"
3.41 +theorem unity_coeff_ex: "(\<exists>(x::'a::{semiring_0,Divides.dvd}). P (l * x)) \<equiv> (\<exists>x. l dvd (x + 0) \<and> P x)"
3.42    apply (rule eq_reflection[symmetric])
3.43    apply (rule iffI)
3.44    defer
```