separate class dvd for divisibility predicate
authorhaftmann
Fri Jul 11 09:02:22 2008 +0200 (2008-07-11)
changeset 27540dc38e79f5a1c
parent 27539 115d3a8bc6a6
child 27541 9e585e99b494
separate class dvd for divisibility predicate
src/HOL/Algebra/poly/UnivPoly2.thy
src/HOL/Divides.thy
src/HOL/Presburger.thy
     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.24      by (simp add: up_divide_def)
    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