split class abs from class minus
authorhaftmann
Fri Jul 20 14:28:01 2007 +0200 (2007-07-20)
changeset 238794776af8be741
parent 23878 bd651ecd4b8a
child 23880 64b9806e160b
split class abs from class minus
src/HOL/Hyperreal/StarClasses.thy
src/HOL/IntDef.thy
src/HOL/Matrix/Matrix.thy
src/HOL/OrderedGroup.thy
src/HOL/Real/Rational.thy
src/HOL/Real/RealDef.thy
src/HOL/Ring_and_Field.thy
src/HOL/Tools/Qelim/cooper_data.ML
     1.1 --- a/src/HOL/Hyperreal/StarClasses.thy	Fri Jul 20 14:27:56 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/StarClasses.thy	Fri Jul 20 14:28:01 2007 +0200
     1.3 @@ -25,7 +25,9 @@
     1.4  
     1.5  instance star :: (minus) minus
     1.6    star_minus_def:   "uminus \<equiv> *f* uminus"
     1.7 -  star_diff_def:    "(op -) \<equiv> *f2* (op -)"
     1.8 +  star_diff_def:    "(op -) \<equiv> *f2* (op -)" ..
     1.9 +
    1.10 +instance star :: (abs) abs
    1.11    star_abs_def:     "abs \<equiv> *f* abs" ..
    1.12  
    1.13  instance star :: (inverse) inverse
    1.14 @@ -398,7 +400,7 @@
    1.15  done
    1.16  
    1.17  instance star :: (pordered_comm_semiring) pordered_comm_semiring
    1.18 -by (intro_classes, transfer, rule mult_mono1_class.times_zero_less_eq_less.mult_mono)
    1.19 +by (intro_classes, transfer, rule mult_mono1_class.less_eq_less_times_zero.mult_mono)
    1.20  
    1.21  instance star :: (pordered_cancel_comm_semiring) pordered_cancel_comm_semiring ..
    1.22  
     2.1 --- a/src/HOL/IntDef.thy	Fri Jul 20 14:27:56 2007 +0200
     2.2 +++ b/src/HOL/IntDef.thy	Fri Jul 20 14:28:01 2007 +0200
     2.3 @@ -218,7 +218,7 @@
     2.4  apply (auto simp add: zmult_zless_mono2_lemma)
     2.5  done
     2.6  
     2.7 -instance int :: minus
     2.8 +instance int :: abs
     2.9    zabs_def: "\<bar>i\<Colon>int\<bar> \<equiv> if i < 0 then - i else i" ..
    2.10  
    2.11  instance int :: distrib_lattice
     3.1 --- a/src/HOL/Matrix/Matrix.thy	Fri Jul 20 14:27:56 2007 +0200
     3.2 +++ b/src/HOL/Matrix/Matrix.thy	Fri Jul 20 14:28:01 2007 +0200
     3.3 @@ -22,8 +22,10 @@
     3.4  instance matrix :: ("{plus, times, zero}") times
     3.5    times_matrix_def: "A * B \<equiv> mult_matrix (op *) (op +) A B" ..
     3.6  
     3.7 +instance matrix :: (lordered_ab_group) abs
     3.8 +  abs_matrix_def: "abs A \<equiv> sup A (- A)" ..
     3.9 +
    3.10  instance matrix :: (lordered_ab_group) lordered_ab_group_meet
    3.11 -  abs_matrix_def: "abs (A::('a::lordered_ab_group) matrix) == sup A (- A)"
    3.12  proof 
    3.13    fix A B C :: "('a::lordered_ab_group) matrix"
    3.14    show "A + B + C = A + (B + C)"    
     4.1 --- a/src/HOL/OrderedGroup.thy	Fri Jul 20 14:27:56 2007 +0200
     4.2 +++ b/src/HOL/OrderedGroup.thy	Fri Jul 20 14:28:01 2007 +0200
     4.3 @@ -783,7 +783,7 @@
     4.4    with a show ?thesis by simp 
     4.5  qed
     4.6  
     4.7 -class lordered_ab_group_abs = lordered_ab_group +
     4.8 +class lordered_ab_group_abs = lordered_ab_group + abs +
     4.9    assumes abs_lattice: "abs x = sup x (uminus x)"
    4.10  
    4.11  lemma abs_zero[simp]: "abs 0 = (0::'a::lordered_ab_group_abs)"
     5.1 --- a/src/HOL/Real/Rational.thy	Fri Jul 20 14:27:56 2007 +0200
     5.2 +++ b/src/HOL/Real/Rational.thy	Fri Jul 20 14:28:01 2007 +0200
     5.3 @@ -159,52 +159,56 @@
     5.4  
     5.5  subsubsection {* Standard operations on rational numbers *}
     5.6  
     5.7 -instance rat :: "{ord, zero, one, plus, times, minus, inverse, power}" ..
     5.8 +instance rat :: zero
     5.9 +  Zero_rat_def: "0 == Fract 0 1" ..
    5.10  
    5.11 -defs (overloaded)
    5.12 -  Zero_rat_def:  "0 == Fract 0 1"
    5.13 -  One_rat_def:   "1 == Fract 1 1"
    5.14 +instance rat :: one
    5.15 +  One_rat_def: "1 == Fract 1 1" ..
    5.16  
    5.17 +instance rat :: plus
    5.18    add_rat_def:
    5.19     "q + r ==
    5.20         Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
    5.21 -           ratrel``{(fst x * snd y + fst y * snd x, snd x * snd y)})"
    5.22 +           ratrel``{(fst x * snd y + fst y * snd x, snd x * snd y)})" ..
    5.23 +lemmas [code func del] = add_rat_def
    5.24  
    5.25 +instance rat :: minus
    5.26    minus_rat_def:
    5.27      "- q == Abs_Rat (\<Union>x \<in> Rep_Rat q. ratrel``{(- fst x, snd x)})"
    5.28 +  diff_rat_def:  "q - r == q + - (r::rat)" ..
    5.29 +lemmas [code func del] = minus_rat_def
    5.30  
    5.31 -  diff_rat_def:  "q - r == q + - (r::rat)"
    5.32 -
    5.33 +instance rat :: times
    5.34    mult_rat_def:
    5.35     "q * r ==
    5.36         Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
    5.37 -           ratrel``{(fst x * fst y, snd x * snd y)})"
    5.38 +           ratrel``{(fst x * fst y, snd x * snd y)})" ..
    5.39 +lemmas [code func del] = mult_rat_def
    5.40  
    5.41 +instance rat :: inverse
    5.42    inverse_rat_def:
    5.43      "inverse q ==
    5.44          Abs_Rat (\<Union>x \<in> Rep_Rat q.
    5.45              ratrel``{if fst x=0 then (0,1) else (snd x, fst x)})"
    5.46 +  divide_rat_def:  "q / r == q * inverse (r::rat)" ..
    5.47 +lemmas [code func del] = inverse_rat_def
    5.48  
    5.49 -  divide_rat_def:  "q / r == q * inverse (r::rat)"
    5.50 -
    5.51 +instance rat :: ord
    5.52    le_rat_def:
    5.53     "q \<le> r == contents (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
    5.54        {(fst x * snd y)*(snd x * snd y) \<le> (fst y * snd x)*(snd x * snd y)})"
    5.55 +  less_rat_def: "(z < (w::rat)) == (z \<le> w & z \<noteq> w)" ..
    5.56 +lemmas [code func del] = le_rat_def less_rat_def
    5.57  
    5.58 -  less_rat_def: "(z < (w::rat)) == (z \<le> w & z \<noteq> w)"
    5.59 +instance rat :: abs
    5.60 +  abs_rat_def: "\<bar>q\<bar> == if q < 0 then -q else (q::rat)" ..
    5.61  
    5.62 -  abs_rat_def: "\<bar>q\<bar> == if q < 0 then -q else (q::rat)"
    5.63 +instance rat :: power ..
    5.64  
    5.65  primrec (rat)
    5.66    rat_power_0:   "q ^ 0       = 1"
    5.67    rat_power_Suc: "q ^ (Suc n) = (q::rat) * (q ^ n)"
    5.68  
    5.69 -lemma zero_rat: "0 = Fract 0 1"
    5.70 -by (simp add: Zero_rat_def)
    5.71 -
    5.72 -lemma one_rat: "1 = Fract 1 1"
    5.73 -by (simp add: One_rat_def)
    5.74 -
    5.75  theorem eq_rat: "b \<noteq> 0 ==> d \<noteq> 0 ==>
    5.76    (Fract a b = Fract c d) = (a * d = c * b)"
    5.77  by (simp add: Fract_def)
    5.78 @@ -241,7 +245,7 @@
    5.79  by (simp add: less_rat_def le_rat eq_rat order_less_le)
    5.80  
    5.81  theorem abs_rat: "b \<noteq> 0 ==> \<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>"
    5.82 -  by (simp add: abs_rat_def minus_rat zero_rat less_rat eq_rat)
    5.83 +  by (simp add: abs_rat_def minus_rat Zero_rat_def less_rat eq_rat)
    5.84       (auto simp add: mult_less_0_iff zero_less_mult_iff order_le_less
    5.85                  split: abs_split)
    5.86  
    5.87 @@ -257,9 +261,9 @@
    5.88    show "q + r = r + q"
    5.89      by (induct q, induct r) (simp add: add_rat add_ac mult_ac)
    5.90    show "0 + q = q"
    5.91 -    by (induct q) (simp add: zero_rat add_rat)
    5.92 +    by (induct q) (simp add: Zero_rat_def add_rat)
    5.93    show "(-q) + q = 0"
    5.94 -    by (induct q) (simp add: zero_rat minus_rat add_rat eq_rat)
    5.95 +    by (induct q) (simp add: Zero_rat_def minus_rat add_rat eq_rat)
    5.96    show "q - r = q + (-r)"
    5.97      by (induct q, induct r) (simp add: add_rat minus_rat diff_rat)
    5.98    show "(q * r) * s = q * (r * s)"
    5.99 @@ -267,16 +271,16 @@
   5.100    show "q * r = r * q"
   5.101      by (induct q, induct r) (simp add: mult_rat mult_ac)
   5.102    show "1 * q = q"
   5.103 -    by (induct q) (simp add: one_rat mult_rat)
   5.104 +    by (induct q) (simp add: One_rat_def mult_rat)
   5.105    show "(q + r) * s = q * s + r * s"
   5.106      by (induct q, induct r, induct s)
   5.107         (simp add: add_rat mult_rat eq_rat int_distrib)
   5.108    show "q \<noteq> 0 ==> inverse q * q = 1"
   5.109 -    by (induct q) (simp add: inverse_rat mult_rat one_rat zero_rat eq_rat)
   5.110 +    by (induct q) (simp add: inverse_rat mult_rat One_rat_def Zero_rat_def eq_rat)
   5.111    show "q / r = q * inverse r"
   5.112      by (simp add: divide_rat_def)
   5.113    show "0 \<noteq> (1::rat)"
   5.114 -    by (simp add: zero_rat one_rat eq_rat)
   5.115 +    by (simp add: Zero_rat_def One_rat_def eq_rat)
   5.116  qed
   5.117  
   5.118  instance rat :: linorder
   5.119 @@ -382,7 +386,7 @@
   5.120      proof -
   5.121        let ?E = "e * f" and ?F = "f * f"
   5.122        from neq gt have "0 < ?E"
   5.123 -        by (auto simp add: zero_rat less_rat le_rat order_less_le eq_rat)
   5.124 +        by (auto simp add: Zero_rat_def less_rat le_rat order_less_le eq_rat)
   5.125        moreover from neq have "0 < ?F"
   5.126          by (auto simp add: zero_less_mult_iff)
   5.127        moreover from neq le have "(a * d) * (b * d) < (c * b) * (b * d)"
   5.128 @@ -400,7 +404,7 @@
   5.129  instance rat :: division_by_zero
   5.130  proof
   5.131    show "inverse 0 = (0::rat)"
   5.132 -    by (simp add: zero_rat Fract_def inverse_rat_def
   5.133 +    by (simp add: Zero_rat_def Fract_def inverse_rat_def
   5.134                    inverse_congruent UN_ratrel)
   5.135  qed
   5.136  
   5.137 @@ -436,15 +440,15 @@
   5.138  
   5.139  lemma zero_less_Fract_iff:
   5.140       "0 < b ==> (0 < Fract a b) = (0 < a)"
   5.141 -by (simp add: zero_rat less_rat order_less_imp_not_eq2 zero_less_mult_iff)
   5.142 +by (simp add: Zero_rat_def less_rat order_less_imp_not_eq2 zero_less_mult_iff)
   5.143  
   5.144  lemma Fract_add_one: "n \<noteq> 0 ==> Fract (m + n) n = Fract m n + 1"
   5.145  apply (insert add_rat [of concl: m n 1 1])
   5.146 -apply (simp add: one_rat  [symmetric])
   5.147 +apply (simp add: One_rat_def [symmetric])
   5.148  done
   5.149  
   5.150  lemma of_nat_rat: "of_nat k = Fract (of_nat k) 1"
   5.151 -by (induct k) (simp_all add: zero_rat one_rat add_rat)
   5.152 +by (induct k) (simp_all add: Zero_rat_def One_rat_def add_rat)
   5.153  
   5.154  lemma of_int_rat: "of_int k = Fract k 1"
   5.155  by (cases k rule: int_diff_cases, simp add: of_nat_rat diff_rat)
   5.156 @@ -563,4 +567,7 @@
   5.157    "of_rat (number_of w) = (number_of w :: 'a::{number_ring,field_char_0})"
   5.158  by (simp add: number_of_eq)
   5.159  
   5.160 +lemmas zero_rat = Zero_rat_def
   5.161 +lemmas one_rat = One_rat_def
   5.162 +
   5.163  end
     6.1 --- a/src/HOL/Real/RealDef.thy	Fri Jul 20 14:27:56 2007 +0200
     6.2 +++ b/src/HOL/Real/RealDef.thy	Fri Jul 20 14:28:01 2007 +0200
     6.3 @@ -20,12 +20,8 @@
     6.4  typedef (Real)  real = "UNIV//realrel"
     6.5    by (auto simp add: quotient_def)
     6.6  
     6.7 -instance real :: "{ord, zero, one, plus, times, minus, inverse}" ..
     6.8 -
     6.9  definition
    6.10 -
    6.11    (** these don't use the overloaded "real" function: users don't see them **)
    6.12 -
    6.13    real_of_preal :: "preal => real" where
    6.14    "real_of_preal m = Abs_Real(realrel``{(m + 1, 1)})"
    6.15  
    6.16 @@ -33,44 +29,38 @@
    6.17     (*overloaded constant for injecting other types into "real"*)
    6.18     real :: "'a => real"
    6.19  
    6.20 -
    6.21 -defs (overloaded)
    6.22 +instance real :: zero
    6.23 +  real_zero_def: "0 == Abs_Real(realrel``{(1, 1)})" ..
    6.24  
    6.25 -  real_zero_def:
    6.26 -  "0 == Abs_Real(realrel``{(1, 1)})"
    6.27 -
    6.28 -  real_one_def:
    6.29 -  "1 == Abs_Real(realrel``{(1 + 1, 1)})"
    6.30 +instance real :: one
    6.31 +  real_one_def: "1 == Abs_Real(realrel``{(1 + 1, 1)})" ..
    6.32  
    6.33 -  real_minus_def:
    6.34 -  "- r ==  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
    6.35 -
    6.36 -  real_add_def:
    6.37 -   "z + w ==
    6.38 +instance real :: plus
    6.39 +  real_add_def: "z + w ==
    6.40         contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
    6.41 -		 { Abs_Real(realrel``{(x+u, y+v)}) })"
    6.42 +		 { Abs_Real(realrel``{(x+u, y+v)}) })" ..
    6.43  
    6.44 -  real_diff_def:
    6.45 -   "r - (s::real) == r + - s"
    6.46 +instance real :: minus
    6.47 +  real_minus_def: "- r ==  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
    6.48 +  real_diff_def: "r - (s::real) == r + - s" ..
    6.49  
    6.50 +instance real :: times
    6.51    real_mult_def:
    6.52      "z * w ==
    6.53         contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
    6.54 -		 { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
    6.55 +		 { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })" ..
    6.56  
    6.57 -  real_inverse_def:
    6.58 -  "inverse (R::real) == (THE S. (R = 0 & S = 0) | S * R = 1)"
    6.59 -
    6.60 -  real_divide_def:
    6.61 -  "R / (S::real) == R * inverse S"
    6.62 +instance real :: inverse
    6.63 +  real_inverse_def: "inverse (R::real) == (THE S. (R = 0 & S = 0) | S * R = 1)"
    6.64 +  real_divide_def: "R / (S::real) == R * inverse S" ..
    6.65  
    6.66 -  real_le_def:
    6.67 -   "z \<le> (w::real) == 
    6.68 +instance real :: ord
    6.69 +  real_le_def: "z \<le> (w::real) == 
    6.70      \<exists>x y u v. x+v \<le> u+y & (x,y) \<in> Rep_Real z & (u,v) \<in> Rep_Real w"
    6.71 +  real_less_def: "(x < (y::real)) == (x \<le> y & x \<noteq> y)" ..
    6.72  
    6.73 -  real_less_def: "(x < (y::real)) == (x \<le> y & x \<noteq> y)"
    6.74 -
    6.75 -  real_abs_def:  "abs (r::real) == (if r < 0 then - r else r)"
    6.76 +instance real :: abs
    6.77 +  real_abs_def:  "abs (r::real) == (if r < 0 then - r else r)" ..
    6.78  
    6.79  
    6.80  subsection {* Equivalence relation over positive reals *}
    6.81 @@ -946,12 +936,11 @@
    6.82    "op * :: real \<Rightarrow> real \<Rightarrow> real" ("Rat.mult")
    6.83    "inverse :: real \<Rightarrow> real" ("Rat.inv")
    6.84    "op \<le> :: real \<Rightarrow> real \<Rightarrow> bool" ("Rat.le")
    6.85 -  "op < :: real \<Rightarrow> real \<Rightarrow> bool" ("(Rat.ord (_, _) = LESS)")
    6.86 +  "op < :: real \<Rightarrow> real \<Rightarrow> bool" ("Rat.lt")
    6.87    "op = :: real \<Rightarrow> real \<Rightarrow> bool" ("curry Rat.eq")
    6.88    "real :: int \<Rightarrow> real" ("Rat.rat'_of'_int")
    6.89    "real :: nat \<Rightarrow> real" ("(Rat.rat'_of'_int o {*int*})")
    6.90  
    6.91 -
    6.92  lemma [code, code unfold]:
    6.93    "number_of k = real (number_of k :: int)"
    6.94    by simp
     7.1 --- a/src/HOL/Ring_and_Field.thy	Fri Jul 20 14:27:56 2007 +0200
     7.2 +++ b/src/HOL/Ring_and_Field.thy	Fri Jul 20 14:28:01 2007 +0200
     7.3 @@ -296,7 +296,7 @@
     7.4  
     7.5  instance lordered_ring \<subseteq> lordered_ab_group_join ..
     7.6  
     7.7 -class abs_if = minus + ord + zero +
     7.8 +class abs_if = minus + ord + zero + abs +
     7.9    assumes abs_if: "abs a = (if a \<sqsubset> 0 then (uminus a) else a)"
    7.10  
    7.11  (* The "strict" suffix can be seen as describing the combination of ordered_ring and no_zero_divisors.
     8.1 --- a/src/HOL/Tools/Qelim/cooper_data.ML	Fri Jul 20 14:27:56 2007 +0200
     8.2 +++ b/src/HOL/Tools/Qelim/cooper_data.ML	Fri Jul 20 14:28:01 2007 +0200
     8.3 @@ -30,7 +30,7 @@
     8.4     @{term "op < :: int => _"}, @{term "op < :: nat => _"},
     8.5     @{term "op <= :: int => _"}, @{term "op <= :: nat => _"},
     8.6     @{term "op dvd :: int => _"}, @{term "op dvd :: nat => _"}, 
     8.7 -   @{term "abs :: int => _"},  @{term "abs :: nat => _"}, 
     8.8 +   @{term "abs :: int => _"},  (*@ {term "abs :: nat => _"}, *)
     8.9     @{term "max :: int => _"},  @{term "max :: nat => _"}, 
    8.10     @{term "min :: int => _"},  @{term "min :: nat => _"}, 
    8.11     @{term "HOL.uminus :: int => _"}, @{term "HOL.uminus :: nat => _"},