--- 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 ..
--- 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
--- 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)"
--- 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)"
--- 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
--- 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
--- 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.
--- 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 => _"},