--- 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.
--- 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"
--- 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 ==
--- 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 \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>div" 70)
fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>mod" 70)
@@ -23,12 +21,12 @@
mod_def: "m mod n == wfrec (pred_nat^+)
(%f j. if j<n | n=0 then j else f (j-n)) m" ..
-definition (in times)
+definition (in div)
dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<^loc>dvd" 50)
where
[code func del]: "m \<^loc>dvd n \<longleftrightarrow> (\<exists>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 \<longleftrightarrow> 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
--- 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]
--- 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 @@
"\<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,times})<z. (d dvd x + s) = (d dvd x + s)"
- "\<exists>z.\<forall>(x::'a::{linorder,plus,times})<z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
+ "\<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<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
@@ -46,8 +46,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,times})>z. (d dvd x + s) = (d dvd x + s)"
- "\<exists>z.\<forall>(x::'a::{linorder,plus,times})>z. (\<not> d dvd x + s) = (\<not> d dvd x + s)"
+ "\<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>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 @@
\<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}) dvd D \<Longrightarrow> \<forall>x k. (d dvd x + t) = (d dvd (x - k*D) + t)"
- "(d::'a::{comm_ring}) dvd D \<Longrightarrow> \<forall>x k. (\<not>d dvd x + t) = (\<not>d dvd (x - k*D) + t)"
+ "(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)"
"\<forall>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: "(\<exists>(x::'a::{semiring_0}). P (l * x)) \<equiv> (\<exists>x. l dvd (x + 0) \<and> P x)"
+theorem unity_coeff_ex: "(\<exists>(x::'a::{semiring_0,Divides.div}). P (l * x)) \<equiv> (\<exists>x. l dvd (x + 0) \<and> P x)"
apply (rule eq_reflection[symmetric])
apply (rule iffI)
defer