# HG changeset patch # User haftmann # Date 1192170046 -7200 # Node ID 92dfacb32053e3da17027ab84bba02cb1bbd053d # Parent d337132842073ec5066b83e740607bd488570d18 class div inherits from class times diff -r d33713284207 -r 92dfacb32053 NEWS --- a/NEWS Fri Oct 12 08:20:45 2007 +0200 +++ b/NEWS Fri Oct 12 08:20:46 2007 +0200 @@ -535,6 +535,9 @@ *** HOL *** +* class "div" now inherits from class "times" rather than "type". +INCOMPATIBILITY. + * New "auto_quickcheck" feature tests outermost goal statements for potential counter-examples. Controlled by ML references auto_quickcheck (default true) and auto_quickcheck_time_limit (default @@ -574,12 +577,12 @@ * Library/Numeral_Type: numbers as types, e.g. TYPE(32). * Code generator library theories: - - Pretty_Int represents HOL integers by big integer literals in target + - Code_Integer represents HOL integers by big integer literals in target languages. - - Pretty_Char represents HOL characters by character literals in target + - Code_Char represents HOL characters by character literals in target languages. - - Pretty_Char_chr like Pretty_Char, but also offers treatment of character - codes; includes Pretty_Int. + - Code_Char_chr like Code_Char, but also offers treatment of character + codes; includes Code_Integer. - Executable_Set allows to generate code for finite sets using lists. - Executable_Rat implements rational numbers as triples (sign, enumerator, denominator). @@ -587,12 +590,11 @@ representable by rational numbers. - Efficient_Nat implements natural numbers by integers, which in general will result in higher efficency; pattern matching with 0/Suc is eliminated; - includes Pretty_Int. - - ML_String provides an additional datatype ml_string; in the HOL default - setup, strings in HOL are mapped to lists of HOL characters in SML; values - of type ml_string are mapped to strings in SML. - - ML_Int provides an additional datatype ml_int which is mapped to to SML - built-in integers. + includes Code_Integer. + - Code_Index provides an additional datatype index which is mapped to + target-language built-in integers. + - Code_Message provides an additional datatype message_string} which is isomorphic to + strings; messages are mapped to target-language strings. * New package for inductive predicates @@ -787,12 +789,6 @@ ring_distribs. Removed lemmas field_xyz in theory Ring_and_Field because they were subsumed by lemmas xyz. INCOMPATIBILITY. -* Library/Pretty_Int.thy: maps HOL numerals on target language integer -literals when generating code. - -* Library/Pretty_Char.thy: maps HOL characters on target language -character literals when generating code. - * Library/Commutative_Ring.thy: switched from recdef to function package; constants add, mul, pow now curried. Infix syntax for algebraic operations. diff -r d33713284207 -r 92dfacb32053 src/HOL/Algebra/abstract/Ring2.thy --- a/src/HOL/Algebra/abstract/Ring2.thy Fri Oct 12 08:20:45 2007 +0200 +++ b/src/HOL/Algebra/abstract/Ring2.thy Fri Oct 12 08:20:46 2007 +0200 @@ -15,15 +15,15 @@ text {* Most constants are already declared by HOL. *} consts - assoc :: "['a::times, 'a] => bool" (infixl "assoc" 50) - irred :: "'a::{zero, one, times} => bool" - prime :: "'a::{zero, one, times} => bool" + assoc :: "['a::Divides.div, 'a] => bool" (infixl "assoc" 50) + irred :: "'a::{zero, one, Divides.div} => bool" + prime :: "'a::{zero, one, Divides.div} => bool" section {* Axioms *} subsection {* Ring axioms *} -axclass ring < zero, one, plus, minus, times, inverse, power +axclass ring < zero, one, plus, minus, times, inverse, power, Divides.div a_assoc: "(a + b) + c = a + (b + c)" l_zero: "0 + a = a" diff -r d33713284207 -r 92dfacb32053 src/HOL/Algebra/poly/UnivPoly2.thy --- a/src/HOL/Algebra/poly/UnivPoly2.thy Fri Oct 12 08:20:45 2007 +0200 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy Fri Oct 12 08:20:46 2007 +0200 @@ -82,6 +82,7 @@ instance up :: (plus) plus .. instance up :: (minus) minus .. instance up :: (times) times .. +instance up :: (Divides.div) Divides.div .. instance up :: (inverse) inverse .. instance up :: (power) power .. @@ -96,7 +97,7 @@ (* note: - 1 is different from -1; latter is of class number *) up_minus_def: "(a::'a::{plus, minus} up) - b == a + (-b)" - up_inverse_def: "inverse (a::'a::{zero, one, times, inverse} up) == + up_inverse_def: "inverse (a::'a::{zero, one, Divides.div, inverse} up) == (if a dvd 1 then THE x. a*x = 1 else 0)" up_divide_def: "(a::'a::{times, inverse} up) / b == a * inverse b" up_power_def: "(a::'a::{one, times, power} up) ^ n == diff -r d33713284207 -r 92dfacb32053 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Fri Oct 12 08:20:45 2007 +0200 +++ b/src/HOL/Divides.thy Fri Oct 12 08:20:46 2007 +0200 @@ -11,9 +11,7 @@ uses "~~/src/Provers/Arith/cancel_div_mod.ML" begin -(*We use the same class for div and mod; - moreover, dvd is defined whenever multiplication is*) -class div = type + +class div = times + fixes div :: "'a \ 'a \ 'a" (infixl "\<^loc>div" 70) fixes mod :: "'a \ 'a \ 'a" (infixl "\<^loc>mod" 70) @@ -23,12 +21,12 @@ mod_def: "m mod n == wfrec (pred_nat^+) (%f j. if j 'a \ bool" (infixl "\<^loc>dvd" 50) where [code func del]: "m \<^loc>dvd n \ (\k. n = m \<^loc>* k)" -class dvd_mod = times + div + zero + -- {* for code generation *} +class dvd_mod = div + zero + -- {* for code generation *} assumes dvd_def_mod [code func]: "x \<^loc>dvd y \ y \<^loc>mod x = \<^loc>0" definition @@ -903,7 +901,7 @@ unfolding divmod_def by simp instance nat :: dvd_mod - by default (simp add: times_class.dvd [symmetric] dvd_eq_mod_eq_0) + by default (simp add: dvd_eq_mod_eq_0) code_modulename SML Divides Nat diff -r d33713284207 -r 92dfacb32053 src/HOL/IntDiv.thy --- a/src/HOL/IntDiv.thy Fri Oct 12 08:20:45 2007 +0200 +++ b/src/HOL/IntDiv.thy Fri Oct 12 08:20:46 2007 +0200 @@ -1144,7 +1144,7 @@ by (simp add: dvd_def zmod_eq_0_iff) instance int :: dvd_mod - by default (simp add: times_class.dvd [symmetric] zdvd_iff_zmod_eq_0) + by default (simp add: zdvd_iff_zmod_eq_0) lemmas zdvd_iff_zmod_eq_0_number_of [simp] = zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard] diff -r d33713284207 -r 92dfacb32053 src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Fri Oct 12 08:20:45 2007 +0200 +++ b/src/HOL/Presburger.thy Fri Oct 12 08:20:46 2007 +0200 @@ -30,8 +30,8 @@ "\(z ::'a::{linorder}).\x t) = True" "\(z ::'a::{linorder}).\x t) = False" "\(z ::'a::{linorder}).\x t) = False" - "\z.\(x::'a::{linorder,plus,times})z.\(x::'a::{linorder,plus,times}) d dvd x + s) = (\ d dvd x + s)" + "\z.\(x::'a::{linorder,plus,Divides.div})z.\(x::'a::{linorder,plus,Divides.div}) d dvd x + s) = (\ d dvd x + s)" "\z.\x(z ::'a::{linorder}).\x>z.(x \ t) = False" "\(z ::'a::{linorder}).\x>z.(x > t) = True" "\(z ::'a::{linorder}).\x>z.(x \ t) = True" - "\z.\(x::'a::{linorder,plus,times})>z. (d dvd x + s) = (d dvd x + s)" - "\z.\(x::'a::{linorder,plus,times})>z. (\ d dvd x + s) = (\ d dvd x + s)" + "\z.\(x::'a::{linorder,plus,Divides.div})>z. (d dvd x + s) = (d dvd x + s)" + "\z.\(x::'a::{linorder,plus,Divides.div})>z. (\ d dvd x + s) = (\ d dvd x + s)" "\z.\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 @@ -56,8 +56,8 @@ \ \x k. (P x \ Q x) = (P (x - k*D) \ Q (x - k*D))" "\\x k. P x = P (x - k*D); \x k. Q x = Q (x - k*D)\ \ \x k. (P x \ Q x) = (P (x - k*D) \ Q (x - k*D))" - "(d::'a::{comm_ring}) dvd D \ \x k. (d dvd x + t) = (d dvd (x - k*D) + t)" - "(d::'a::{comm_ring}) dvd D \ \x k. (\d dvd x + t) = (\d dvd (x - k*D) + t)" + "(d::'a::{comm_ring,Divides.div}) dvd D \ \x k. (d dvd x + t) = (d dvd (x - k*D) + t)" + "(d::'a::{comm_ring,Divides.div}) dvd D \ \x k. (\d dvd x + t) = (\d dvd (x - k*D) + t)" "\x k. F = F" by simp_all (clarsimp simp add: dvd_def, rule iffI, clarsimp,rule_tac x = "kb - ka*k" in exI, @@ -359,7 +359,7 @@ apply(fastsimp) done -theorem unity_coeff_ex: "(\(x::'a::{semiring_0}). P (l * x)) \ (\x. l dvd (x + 0) \ P x)" +theorem unity_coeff_ex: "(\(x::'a::{semiring_0,Divides.div}). P (l * x)) \ (\x. l dvd (x + 0) \ P x)" apply (rule eq_reflection[symmetric]) apply (rule iffI) defer