class div inherits from class times
authorhaftmann
Fri Oct 12 08:20:46 2007 +0200 (2007-10-12)
changeset 2499392dfacb32053
parent 24992 d33713284207
child 24994 c385c4eabb3b
class div inherits from class times
NEWS
src/HOL/Algebra/abstract/Ring2.thy
src/HOL/Algebra/poly/UnivPoly2.thy
src/HOL/Divides.thy
src/HOL/IntDiv.thy
src/HOL/Presburger.thy
     1.1 --- a/NEWS	Fri Oct 12 08:20:45 2007 +0200
     1.2 +++ b/NEWS	Fri Oct 12 08:20:46 2007 +0200
     1.3 @@ -535,6 +535,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* class "div" now inherits from class "times" rather than "type".
     1.8 +INCOMPATIBILITY.
     1.9 +
    1.10  * New "auto_quickcheck" feature tests outermost goal statements for
    1.11  potential counter-examples.  Controlled by ML references
    1.12  auto_quickcheck (default true) and auto_quickcheck_time_limit (default
    1.13 @@ -574,12 +577,12 @@
    1.14  * Library/Numeral_Type: numbers as types, e.g. TYPE(32).
    1.15  
    1.16  * Code generator library theories:
    1.17 -  - Pretty_Int represents HOL integers by big integer literals in target
    1.18 +  - Code_Integer represents HOL integers by big integer literals in target
    1.19      languages.
    1.20 -  - Pretty_Char represents HOL characters by character literals in target
    1.21 +  - Code_Char represents HOL characters by character literals in target
    1.22      languages.
    1.23 -  - Pretty_Char_chr like Pretty_Char, but also offers treatment of character
    1.24 -    codes; includes Pretty_Int.
    1.25 +  - Code_Char_chr like Code_Char, but also offers treatment of character
    1.26 +    codes; includes Code_Integer.
    1.27    - Executable_Set allows to generate code for finite sets using lists.
    1.28    - Executable_Rat implements rational numbers as triples (sign, enumerator,
    1.29      denominator).
    1.30 @@ -587,12 +590,11 @@
    1.31      representable by rational numbers.
    1.32    - Efficient_Nat implements natural numbers by integers, which in general will
    1.33      result in higher efficency; pattern matching with 0/Suc is eliminated;
    1.34 -    includes Pretty_Int.
    1.35 -  - ML_String provides an additional datatype ml_string; in the HOL default
    1.36 -    setup, strings in HOL are mapped to lists of HOL characters in SML; values
    1.37 -    of type ml_string are mapped to strings in SML.
    1.38 -  - ML_Int provides an additional datatype ml_int which is mapped to to SML
    1.39 -    built-in integers.
    1.40 +    includes Code_Integer.
    1.41 +  - Code_Index provides an additional datatype index which is mapped to
    1.42 +    target-language built-in integers.
    1.43 +  - Code_Message provides an additional datatype message_string} which is isomorphic to
    1.44 +    strings; messages are mapped to target-language strings.
    1.45  
    1.46  * New package for inductive predicates
    1.47  
    1.48 @@ -787,12 +789,6 @@
    1.49  ring_distribs.  Removed lemmas field_xyz in theory Ring_and_Field
    1.50  because they were subsumed by lemmas xyz.  INCOMPATIBILITY.
    1.51  
    1.52 -* Library/Pretty_Int.thy: maps HOL numerals on target language integer
    1.53 -literals when generating code.
    1.54 -
    1.55 -* Library/Pretty_Char.thy: maps HOL characters on target language
    1.56 -character literals when generating code.
    1.57 -
    1.58  * Library/Commutative_Ring.thy: switched from recdef to function
    1.59  package; constants add, mul, pow now curried.  Infix syntax for
    1.60  algebraic operations.
     2.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Fri Oct 12 08:20:45 2007 +0200
     2.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Fri Oct 12 08:20:46 2007 +0200
     2.3 @@ -15,15 +15,15 @@
     2.4  text {* Most constants are already declared by HOL. *}
     2.5  
     2.6  consts
     2.7 -  assoc         :: "['a::times, 'a] => bool"              (infixl "assoc" 50)
     2.8 -  irred         :: "'a::{zero, one, times} => bool"
     2.9 -  prime         :: "'a::{zero, one, times} => bool"
    2.10 +  assoc         :: "['a::Divides.div, 'a] => bool"              (infixl "assoc" 50)
    2.11 +  irred         :: "'a::{zero, one, Divides.div} => bool"
    2.12 +  prime         :: "'a::{zero, one, Divides.div} => bool"
    2.13  
    2.14  section {* Axioms *}
    2.15  
    2.16  subsection {* Ring axioms *}
    2.17  
    2.18 -axclass ring < zero, one, plus, minus, times, inverse, power
    2.19 +axclass ring < zero, one, plus, minus, times, inverse, power, Divides.div
    2.20  
    2.21    a_assoc:      "(a + b) + c = a + (b + c)"
    2.22    l_zero:       "0 + a = a"
     3.1 --- a/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Oct 12 08:20:45 2007 +0200
     3.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Oct 12 08:20:46 2007 +0200
     3.3 @@ -82,6 +82,7 @@
     3.4  instance up :: (plus) plus ..
     3.5  instance up :: (minus) minus ..
     3.6  instance up :: (times) times ..
     3.7 +instance up :: (Divides.div) Divides.div ..
     3.8  instance up :: (inverse) inverse ..
     3.9  instance up :: (power) power ..
    3.10  
    3.11 @@ -96,7 +97,7 @@
    3.12                  (* note: - 1 is different from -1; latter is of class number *)
    3.13  
    3.14    up_minus_def:   "(a::'a::{plus, minus} up) - b == a + (-b)"
    3.15 -  up_inverse_def: "inverse (a::'a::{zero, one, times, inverse} up) == 
    3.16 +  up_inverse_def: "inverse (a::'a::{zero, one, Divides.div, inverse} up) == 
    3.17                       (if a dvd 1 then THE x. a*x = 1 else 0)"
    3.18    up_divide_def:  "(a::'a::{times, inverse} up) / b == a * inverse b"
    3.19    up_power_def:   "(a::'a::{one, times, power} up) ^ n ==
     4.1 --- a/src/HOL/Divides.thy	Fri Oct 12 08:20:45 2007 +0200
     4.2 +++ b/src/HOL/Divides.thy	Fri Oct 12 08:20:46 2007 +0200
     4.3 @@ -11,9 +11,7 @@
     4.4  uses "~~/src/Provers/Arith/cancel_div_mod.ML"
     4.5  begin
     4.6  
     4.7 -(*We use the same class for div and mod;
     4.8 -  moreover, dvd is defined whenever multiplication is*)
     4.9 -class div = type +
    4.10 +class div = times +
    4.11    fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>div" 70)
    4.12    fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>mod" 70)
    4.13  
    4.14 @@ -23,12 +21,12 @@
    4.15    mod_def: "m mod n == wfrec (pred_nat^+)
    4.16                            (%f j. if j<n | n=0 then j else f (j-n)) m" ..
    4.17  
    4.18 -definition (in times)
    4.19 +definition (in div)
    4.20    dvd  :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<^loc>dvd" 50)
    4.21  where
    4.22    [code func del]: "m \<^loc>dvd n \<longleftrightarrow> (\<exists>k. n = m \<^loc>* k)"
    4.23  
    4.24 -class dvd_mod = times + div + zero + -- {* for code generation *}
    4.25 +class dvd_mod = div + zero + -- {* for code generation *}
    4.26    assumes dvd_def_mod [code func]: "x \<^loc>dvd y \<longleftrightarrow> y \<^loc>mod x = \<^loc>0"
    4.27  
    4.28  definition
    4.29 @@ -903,7 +901,7 @@
    4.30    unfolding divmod_def by simp
    4.31  
    4.32  instance nat :: dvd_mod
    4.33 -  by default (simp add: times_class.dvd [symmetric] dvd_eq_mod_eq_0)
    4.34 +  by default (simp add: dvd_eq_mod_eq_0)
    4.35  
    4.36  code_modulename SML
    4.37    Divides Nat
     5.1 --- a/src/HOL/IntDiv.thy	Fri Oct 12 08:20:45 2007 +0200
     5.2 +++ b/src/HOL/IntDiv.thy	Fri Oct 12 08:20:46 2007 +0200
     5.3 @@ -1144,7 +1144,7 @@
     5.4    by (simp add: dvd_def zmod_eq_0_iff)
     5.5  
     5.6  instance int :: dvd_mod
     5.7 -  by default (simp add: times_class.dvd [symmetric] zdvd_iff_zmod_eq_0)
     5.8 +  by default (simp add: zdvd_iff_zmod_eq_0)
     5.9  
    5.10  lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
    5.11    zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard]
     6.1 --- a/src/HOL/Presburger.thy	Fri Oct 12 08:20:45 2007 +0200
     6.2 +++ b/src/HOL/Presburger.thy	Fri Oct 12 08:20:46 2007 +0200
     6.3 @@ -30,8 +30,8 @@
     6.4    "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<le> t) = True"
     6.5    "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x > t) = False"
     6.6    "\<exists>(z ::'a::{linorder}).\<forall>x<z.(x \<ge> t) = False"
     6.7 -  "\<exists>z.\<forall>(x::'a::{linorder,plus,times})<z. (d dvd x + s) = (d dvd x + s)"
     6.8 -  "\<exists>z.\<forall>(x::'a::{linorder,plus,times})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
     6.9 +  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.div})<z. (d dvd x + s) = (d dvd x + s)"
    6.10 +  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.div})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
    6.11    "\<exists>z.\<forall>x<z. F = F"
    6.12    by ((erule exE, erule exE,rule_tac x="min z za" in exI,simp)+, (rule_tac x="t" in exI,fastsimp)+) simp_all
    6.13  
    6.14 @@ -46,8 +46,8 @@
    6.15    "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<le> t) = False"
    6.16    "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x > t) = True"
    6.17    "\<exists>(z ::'a::{linorder}).\<forall>x>z.(x \<ge> t) = True"
    6.18 -  "\<exists>z.\<forall>(x::'a::{linorder,plus,times})>z. (d dvd x + s) = (d dvd x + s)"
    6.19 -  "\<exists>z.\<forall>(x::'a::{linorder,plus,times})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
    6.20 +  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.div})>z. (d dvd x + s) = (d dvd x + s)"
    6.21 +  "\<exists>z.\<forall>(x::'a::{linorder,plus,Divides.div})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
    6.22    "\<exists>z.\<forall>x>z. F = F"
    6.23    by ((erule exE, erule exE,rule_tac x="max z za" in exI,simp)+,(rule_tac x="t" in exI,fastsimp)+) simp_all
    6.24  
    6.25 @@ -56,8 +56,8 @@
    6.26      \<Longrightarrow> \<forall>x k. (P x \<and> Q x) = (P (x - k*D) \<and> Q (x - k*D))"
    6.27    "\<lbrakk>\<forall>x k. P x = P (x - k*D); \<forall>x k. Q x = Q (x - k*D)\<rbrakk> 
    6.28      \<Longrightarrow> \<forall>x k. (P x \<or> Q x) = (P (x - k*D) \<or> Q (x - k*D))"
    6.29 -  "(d::'a::{comm_ring}) dvd D \<Longrightarrow> \<forall>x k. (d dvd x + t) = (d dvd (x - k*D) + t)"
    6.30 -  "(d::'a::{comm_ring}) dvd D \<Longrightarrow> \<forall>x k. (\<not>d dvd x + t) = (\<not>d dvd (x - k*D) + t)"
    6.31 +  "(d::'a::{comm_ring,Divides.div}) dvd D \<Longrightarrow> \<forall>x k. (d dvd x + t) = (d dvd (x - k*D) + t)"
    6.32 +  "(d::'a::{comm_ring,Divides.div}) dvd D \<Longrightarrow> \<forall>x k. (\<not>d dvd x + t) = (\<not>d dvd (x - k*D) + t)"
    6.33    "\<forall>x k. F = F"
    6.34  by simp_all
    6.35    (clarsimp simp add: dvd_def, rule iffI, clarsimp,rule_tac x = "kb - ka*k" in exI,
    6.36 @@ -359,7 +359,7 @@
    6.37  apply(fastsimp)
    6.38  done
    6.39  
    6.40 -theorem unity_coeff_ex: "(\<exists>(x::'a::{semiring_0}). P (l * x)) \<equiv> (\<exists>x. l dvd (x + 0) \<and> P x)"
    6.41 +theorem unity_coeff_ex: "(\<exists>(x::'a::{semiring_0,Divides.div}). P (l * x)) \<equiv> (\<exists>x. l dvd (x + 0) \<and> P x)"
    6.42    apply (rule eq_reflection[symmetric])
    6.43    apply (rule iffI)
    6.44    defer