# HG changeset patch
# User haftmann
# Date 1184934481 -7200
# Node ID 4776af8be7413236a39e20779a44b0aa0380b3f7
# Parent  bd651ecd4b8a247897bfa3ef610e5b895802b9f2
split class abs from class minus

diff -r bd651ecd4b8a -r 4776af8be741 src/HOL/Hyperreal/StarClasses.thy
--- a/src/HOL/Hyperreal/StarClasses.thy	Fri Jul 20 14:27:56 2007 +0200
+++ b/src/HOL/Hyperreal/StarClasses.thy	Fri Jul 20 14:28:01 2007 +0200
@@ -25,7 +25,9 @@
 
 instance star :: (minus) minus
   star_minus_def:   "uminus \<equiv> *f* uminus"
-  star_diff_def:    "(op -) \<equiv> *f2* (op -)"
+  star_diff_def:    "(op -) \<equiv> *f2* (op -)" ..
+
+instance star :: (abs) abs
   star_abs_def:     "abs \<equiv> *f* abs" ..
 
 instance star :: (inverse) inverse
@@ -398,7 +400,7 @@
 done
 
 instance star :: (pordered_comm_semiring) pordered_comm_semiring
-by (intro_classes, transfer, rule mult_mono1_class.times_zero_less_eq_less.mult_mono)
+by (intro_classes, transfer, rule mult_mono1_class.less_eq_less_times_zero.mult_mono)
 
 instance star :: (pordered_cancel_comm_semiring) pordered_cancel_comm_semiring ..
 
diff -r bd651ecd4b8a -r 4776af8be741 src/HOL/IntDef.thy
--- a/src/HOL/IntDef.thy	Fri Jul 20 14:27:56 2007 +0200
+++ b/src/HOL/IntDef.thy	Fri Jul 20 14:28:01 2007 +0200
@@ -218,7 +218,7 @@
 apply (auto simp add: zmult_zless_mono2_lemma)
 done
 
-instance int :: minus
+instance int :: abs
   zabs_def: "\<bar>i\<Colon>int\<bar> \<equiv> if i < 0 then - i else i" ..
 
 instance int :: distrib_lattice
diff -r bd651ecd4b8a -r 4776af8be741 src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Fri Jul 20 14:27:56 2007 +0200
+++ b/src/HOL/Matrix/Matrix.thy	Fri Jul 20 14:28:01 2007 +0200
@@ -22,8 +22,10 @@
 instance matrix :: ("{plus, times, zero}") times
   times_matrix_def: "A * B \<equiv> mult_matrix (op *) (op +) A B" ..
 
+instance matrix :: (lordered_ab_group) abs
+  abs_matrix_def: "abs A \<equiv> sup A (- A)" ..
+
 instance matrix :: (lordered_ab_group) lordered_ab_group_meet
-  abs_matrix_def: "abs (A::('a::lordered_ab_group) matrix) == sup A (- A)"
 proof 
   fix A B C :: "('a::lordered_ab_group) matrix"
   show "A + B + C = A + (B + C)"    
diff -r bd651ecd4b8a -r 4776af8be741 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Fri Jul 20 14:27:56 2007 +0200
+++ b/src/HOL/OrderedGroup.thy	Fri Jul 20 14:28:01 2007 +0200
@@ -783,7 +783,7 @@
   with a show ?thesis by simp 
 qed
 
-class lordered_ab_group_abs = lordered_ab_group +
+class lordered_ab_group_abs = lordered_ab_group + abs +
   assumes abs_lattice: "abs x = sup x (uminus x)"
 
 lemma abs_zero[simp]: "abs 0 = (0::'a::lordered_ab_group_abs)"
diff -r bd651ecd4b8a -r 4776af8be741 src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Fri Jul 20 14:27:56 2007 +0200
+++ b/src/HOL/Real/Rational.thy	Fri Jul 20 14:28:01 2007 +0200
@@ -159,52 +159,56 @@
 
 subsubsection {* Standard operations on rational numbers *}
 
-instance rat :: "{ord, zero, one, plus, times, minus, inverse, power}" ..
+instance rat :: zero
+  Zero_rat_def: "0 == Fract 0 1" ..
 
-defs (overloaded)
-  Zero_rat_def:  "0 == Fract 0 1"
-  One_rat_def:   "1 == Fract 1 1"
+instance rat :: one
+  One_rat_def: "1 == Fract 1 1" ..
 
+instance rat :: plus
   add_rat_def:
    "q + r ==
        Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
-           ratrel``{(fst x * snd y + fst y * snd x, snd x * snd y)})"
+           ratrel``{(fst x * snd y + fst y * snd x, snd x * snd y)})" ..
+lemmas [code func del] = add_rat_def
 
+instance rat :: minus
   minus_rat_def:
     "- q == Abs_Rat (\<Union>x \<in> Rep_Rat q. ratrel``{(- fst x, snd x)})"
+  diff_rat_def:  "q - r == q + - (r::rat)" ..
+lemmas [code func del] = minus_rat_def
 
-  diff_rat_def:  "q - r == q + - (r::rat)"
-
+instance rat :: times
   mult_rat_def:
    "q * r ==
        Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
-           ratrel``{(fst x * fst y, snd x * snd y)})"
+           ratrel``{(fst x * fst y, snd x * snd y)})" ..
+lemmas [code func del] = mult_rat_def
 
+instance rat :: inverse
   inverse_rat_def:
     "inverse q ==
         Abs_Rat (\<Union>x \<in> Rep_Rat q.
             ratrel``{if fst x=0 then (0,1) else (snd x, fst x)})"
+  divide_rat_def:  "q / r == q * inverse (r::rat)" ..
+lemmas [code func del] = inverse_rat_def
 
-  divide_rat_def:  "q / r == q * inverse (r::rat)"
-
+instance rat :: ord
   le_rat_def:
    "q \<le> r == contents (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
       {(fst x * snd y)*(snd x * snd y) \<le> (fst y * snd x)*(snd x * snd y)})"
+  less_rat_def: "(z < (w::rat)) == (z \<le> w & z \<noteq> w)" ..
+lemmas [code func del] = le_rat_def less_rat_def
 
-  less_rat_def: "(z < (w::rat)) == (z \<le> w & z \<noteq> w)"
+instance rat :: abs
+  abs_rat_def: "\<bar>q\<bar> == if q < 0 then -q else (q::rat)" ..
 
-  abs_rat_def: "\<bar>q\<bar> == if q < 0 then -q else (q::rat)"
+instance rat :: power ..
 
 primrec (rat)
   rat_power_0:   "q ^ 0       = 1"
   rat_power_Suc: "q ^ (Suc n) = (q::rat) * (q ^ n)"
 
-lemma zero_rat: "0 = Fract 0 1"
-by (simp add: Zero_rat_def)
-
-lemma one_rat: "1 = Fract 1 1"
-by (simp add: One_rat_def)
-
 theorem eq_rat: "b \<noteq> 0 ==> d \<noteq> 0 ==>
   (Fract a b = Fract c d) = (a * d = c * b)"
 by (simp add: Fract_def)
@@ -241,7 +245,7 @@
 by (simp add: less_rat_def le_rat eq_rat order_less_le)
 
 theorem abs_rat: "b \<noteq> 0 ==> \<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>"
-  by (simp add: abs_rat_def minus_rat zero_rat less_rat eq_rat)
+  by (simp add: abs_rat_def minus_rat Zero_rat_def less_rat eq_rat)
      (auto simp add: mult_less_0_iff zero_less_mult_iff order_le_less
                 split: abs_split)
 
@@ -257,9 +261,9 @@
   show "q + r = r + q"
     by (induct q, induct r) (simp add: add_rat add_ac mult_ac)
   show "0 + q = q"
-    by (induct q) (simp add: zero_rat add_rat)
+    by (induct q) (simp add: Zero_rat_def add_rat)
   show "(-q) + q = 0"
-    by (induct q) (simp add: zero_rat minus_rat add_rat eq_rat)
+    by (induct q) (simp add: Zero_rat_def minus_rat add_rat eq_rat)
   show "q - r = q + (-r)"
     by (induct q, induct r) (simp add: add_rat minus_rat diff_rat)
   show "(q * r) * s = q * (r * s)"
@@ -267,16 +271,16 @@
   show "q * r = r * q"
     by (induct q, induct r) (simp add: mult_rat mult_ac)
   show "1 * q = q"
-    by (induct q) (simp add: one_rat mult_rat)
+    by (induct q) (simp add: One_rat_def mult_rat)
   show "(q + r) * s = q * s + r * s"
     by (induct q, induct r, induct s)
        (simp add: add_rat mult_rat eq_rat int_distrib)
   show "q \<noteq> 0 ==> inverse q * q = 1"
-    by (induct q) (simp add: inverse_rat mult_rat one_rat zero_rat eq_rat)
+    by (induct q) (simp add: inverse_rat mult_rat One_rat_def Zero_rat_def eq_rat)
   show "q / r = q * inverse r"
     by (simp add: divide_rat_def)
   show "0 \<noteq> (1::rat)"
-    by (simp add: zero_rat one_rat eq_rat)
+    by (simp add: Zero_rat_def One_rat_def eq_rat)
 qed
 
 instance rat :: linorder
@@ -382,7 +386,7 @@
     proof -
       let ?E = "e * f" and ?F = "f * f"
       from neq gt have "0 < ?E"
-        by (auto simp add: zero_rat less_rat le_rat order_less_le eq_rat)
+        by (auto simp add: Zero_rat_def less_rat le_rat order_less_le eq_rat)
       moreover from neq have "0 < ?F"
         by (auto simp add: zero_less_mult_iff)
       moreover from neq le have "(a * d) * (b * d) < (c * b) * (b * d)"
@@ -400,7 +404,7 @@
 instance rat :: division_by_zero
 proof
   show "inverse 0 = (0::rat)"
-    by (simp add: zero_rat Fract_def inverse_rat_def
+    by (simp add: Zero_rat_def Fract_def inverse_rat_def
                   inverse_congruent UN_ratrel)
 qed
 
@@ -436,15 +440,15 @@
 
 lemma zero_less_Fract_iff:
      "0 < b ==> (0 < Fract a b) = (0 < a)"
-by (simp add: zero_rat less_rat order_less_imp_not_eq2 zero_less_mult_iff)
+by (simp add: Zero_rat_def less_rat order_less_imp_not_eq2 zero_less_mult_iff)
 
 lemma Fract_add_one: "n \<noteq> 0 ==> Fract (m + n) n = Fract m n + 1"
 apply (insert add_rat [of concl: m n 1 1])
-apply (simp add: one_rat  [symmetric])
+apply (simp add: One_rat_def [symmetric])
 done
 
 lemma of_nat_rat: "of_nat k = Fract (of_nat k) 1"
-by (induct k) (simp_all add: zero_rat one_rat add_rat)
+by (induct k) (simp_all add: Zero_rat_def One_rat_def add_rat)
 
 lemma of_int_rat: "of_int k = Fract k 1"
 by (cases k rule: int_diff_cases, simp add: of_nat_rat diff_rat)
@@ -563,4 +567,7 @@
   "of_rat (number_of w) = (number_of w :: 'a::{number_ring,field_char_0})"
 by (simp add: number_of_eq)
 
+lemmas zero_rat = Zero_rat_def
+lemmas one_rat = One_rat_def
+
 end
diff -r bd651ecd4b8a -r 4776af8be741 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Fri Jul 20 14:27:56 2007 +0200
+++ b/src/HOL/Real/RealDef.thy	Fri Jul 20 14:28:01 2007 +0200
@@ -20,12 +20,8 @@
 typedef (Real)  real = "UNIV//realrel"
   by (auto simp add: quotient_def)
 
-instance real :: "{ord, zero, one, plus, times, minus, inverse}" ..
-
 definition
-
   (** these don't use the overloaded "real" function: users don't see them **)
-
   real_of_preal :: "preal => real" where
   "real_of_preal m = Abs_Real(realrel``{(m + 1, 1)})"
 
@@ -33,44 +29,38 @@
    (*overloaded constant for injecting other types into "real"*)
    real :: "'a => real"
 
-
-defs (overloaded)
+instance real :: zero
+  real_zero_def: "0 == Abs_Real(realrel``{(1, 1)})" ..
 
-  real_zero_def:
-  "0 == Abs_Real(realrel``{(1, 1)})"
-
-  real_one_def:
-  "1 == Abs_Real(realrel``{(1 + 1, 1)})"
+instance real :: one
+  real_one_def: "1 == Abs_Real(realrel``{(1 + 1, 1)})" ..
 
-  real_minus_def:
-  "- r ==  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
-
-  real_add_def:
-   "z + w ==
+instance real :: plus
+  real_add_def: "z + w ==
        contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
-		 { Abs_Real(realrel``{(x+u, y+v)}) })"
+		 { Abs_Real(realrel``{(x+u, y+v)}) })" ..
 
-  real_diff_def:
-   "r - (s::real) == r + - s"
+instance real :: minus
+  real_minus_def: "- r ==  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
+  real_diff_def: "r - (s::real) == r + - s" ..
 
+instance real :: times
   real_mult_def:
     "z * w ==
        contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
-		 { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
+		 { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })" ..
 
-  real_inverse_def:
-  "inverse (R::real) == (THE S. (R = 0 & S = 0) | S * R = 1)"
-
-  real_divide_def:
-  "R / (S::real) == R * inverse S"
+instance real :: inverse
+  real_inverse_def: "inverse (R::real) == (THE S. (R = 0 & S = 0) | S * R = 1)"
+  real_divide_def: "R / (S::real) == R * inverse S" ..
 
-  real_le_def:
-   "z \<le> (w::real) == 
+instance real :: ord
+  real_le_def: "z \<le> (w::real) == 
     \<exists>x y u v. x+v \<le> u+y & (x,y) \<in> Rep_Real z & (u,v) \<in> Rep_Real w"
+  real_less_def: "(x < (y::real)) == (x \<le> y & x \<noteq> y)" ..
 
-  real_less_def: "(x < (y::real)) == (x \<le> y & x \<noteq> y)"
-
-  real_abs_def:  "abs (r::real) == (if r < 0 then - r else r)"
+instance real :: abs
+  real_abs_def:  "abs (r::real) == (if r < 0 then - r else r)" ..
 
 
 subsection {* Equivalence relation over positive reals *}
@@ -946,12 +936,11 @@
   "op * :: real \<Rightarrow> real \<Rightarrow> real" ("Rat.mult")
   "inverse :: real \<Rightarrow> real" ("Rat.inv")
   "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool" ("Rat.le")
-  "op < :: real \<Rightarrow> real \<Rightarrow> bool" ("(Rat.ord (_, _) = LESS)")
+  "op < :: real \<Rightarrow> real \<Rightarrow> bool" ("Rat.lt")
   "op = :: real \<Rightarrow> real \<Rightarrow> bool" ("curry Rat.eq")
   "real :: int \<Rightarrow> real" ("Rat.rat'_of'_int")
   "real :: nat \<Rightarrow> real" ("(Rat.rat'_of'_int o {*int*})")
 
-
 lemma [code, code unfold]:
   "number_of k = real (number_of k :: int)"
   by simp
diff -r bd651ecd4b8a -r 4776af8be741 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Fri Jul 20 14:27:56 2007 +0200
+++ b/src/HOL/Ring_and_Field.thy	Fri Jul 20 14:28:01 2007 +0200
@@ -296,7 +296,7 @@
 
 instance lordered_ring \<subseteq> lordered_ab_group_join ..
 
-class abs_if = minus + ord + zero +
+class abs_if = minus + ord + zero + abs +
   assumes abs_if: "abs a = (if a \<sqsubset> 0 then (uminus a) else a)"
 
 (* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors.
diff -r bd651ecd4b8a -r 4776af8be741 src/HOL/Tools/Qelim/cooper_data.ML
--- a/src/HOL/Tools/Qelim/cooper_data.ML	Fri Jul 20 14:27:56 2007 +0200
+++ b/src/HOL/Tools/Qelim/cooper_data.ML	Fri Jul 20 14:28:01 2007 +0200
@@ -30,7 +30,7 @@
    @{term "op < :: int => _"}, @{term "op < :: nat => _"},
    @{term "op <= :: int => _"}, @{term "op <= :: nat => _"},
    @{term "op dvd :: int => _"}, @{term "op dvd :: nat => _"}, 
-   @{term "abs :: int => _"},  @{term "abs :: nat => _"}, 
+   @{term "abs :: int => _"},  (*@ {term "abs :: nat => _"}, *)
    @{term "max :: int => _"},  @{term "max :: nat => _"}, 
    @{term "min :: int => _"},  @{term "min :: nat => _"}, 
    @{term "HOL.uminus :: int => _"}, @{term "HOL.uminus :: nat => _"},