replaced monomorphic abs definitions by abs_if
authorpaulson
Thu Jun 24 17:52:02 2004 +0200 (2004-06-24)
changeset 150036145dd7538d7
parent 15002 bc050f23c3f8
child 15004 44ac09ba7213
replaced monomorphic abs definitions by abs_if
src/HOL/Complex/Complex.thy
src/HOL/Complex/NSComplex.thy
src/HOL/Hyperreal/HyperArith.thy
src/HOL/Hyperreal/HyperPow.thy
src/HOL/Hyperreal/Lim.thy
src/HOL/Hyperreal/NSA.thy
src/HOL/Hyperreal/Series.thy
src/HOL/Hyperreal/Star.thy
src/HOL/Import/HOL4Compat.thy
src/HOL/Integ/IntArith.thy
src/HOL/Integ/IntDef.thy
src/HOL/Integ/IntDiv.thy
src/HOL/Integ/NatBin.thy
src/HOL/Integ/Parity.thy
src/HOL/NumberTheory/EulerFermat.thy
src/HOL/NumberTheory/Fib.thy
src/HOL/NumberTheory/IntPrimes.thy
src/HOL/Real/RealDef.thy
src/HOL/Real/RealPow.thy
src/HOL/Real/real_arith.ML
     1.1 --- a/src/HOL/Complex/Complex.thy	Thu Jun 24 17:51:28 2004 +0200
     1.2 +++ b/src/HOL/Complex/Complex.thy	Thu Jun 24 17:52:02 2004 +0200
     1.3 @@ -455,7 +455,7 @@
     1.4  
     1.5  lemma complex_mod_mult_cnj: "cmod(z * cnj(z)) = cmod(z) ^ 2"
     1.6  apply (induct z, simp add: complex_mod complex_cnj complex_mult)
     1.7 -apply (simp add: power2_eq_square real_abs_def)
     1.8 +apply (simp add: power2_eq_square abs_if linorder_not_less)
     1.9  done
    1.10  
    1.11  lemma complex_mod_squared: "cmod(Complex x y) ^ 2 = x ^ 2 + y ^ 2"
    1.12 @@ -571,7 +571,7 @@
    1.13       complexpow_Suc: "z ^ (Suc n) = (z::complex) * (z ^ n)"
    1.14  
    1.15  
    1.16 -instance complex :: ringpower
    1.17 +instance complex :: recpower
    1.18  proof
    1.19    fix z :: complex
    1.20    fix n :: nat
    1.21 @@ -947,7 +947,7 @@
    1.22  test "(a*(b*c)) / ((b::complex)) = (uu::complex)";
    1.23  test "(a*(b*c)) / (d*(b::complex)*(x*a)) = (uu::complex)";
    1.24  
    1.25 -(*FIXME: what do we do about this?*)
    1.26 +FIXME: what do we do about this?
    1.27  test "a*(b*c)/(y*z) = d*(b::complex)*(x*a)/z";
    1.28  *)
    1.29  
     2.1 --- a/src/HOL/Complex/NSComplex.thy	Thu Jun 24 17:51:28 2004 +0200
     2.2 +++ b/src/HOL/Complex/NSComplex.thy	Thu Jun 24 17:52:02 2004 +0200
     2.3 @@ -864,7 +864,7 @@
     2.4       hcomplexpow_0:   "z ^ 0       = 1"
     2.5       hcomplexpow_Suc: "z ^ (Suc n) = (z::hcomplex) * (z ^ n)"
     2.6  
     2.7 -instance hcomplex :: ringpower
     2.8 +instance hcomplex :: recpower
     2.9  proof
    2.10    fix z :: hcomplex
    2.11    fix n :: nat
     3.1 --- a/src/HOL/Hyperreal/HyperArith.thy	Thu Jun 24 17:51:28 2004 +0200
     3.2 +++ b/src/HOL/Hyperreal/HyperArith.thy	Thu Jun 24 17:52:02 2004 +0200
     3.3 @@ -86,21 +86,20 @@
     3.4  
     3.5  declare abs_mult [simp]
     3.6  
     3.7 -lemma hrabs_add_less: "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)"
     3.8 -apply (unfold hrabs_def)
     3.9 -apply (simp split add: split_if_asm)
    3.10 -done
    3.11 +lemma hrabs_add_less:
    3.12 +     "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)"
    3.13 +by (simp add: abs_if split: split_if_asm)
    3.14  
    3.15  text{*used once in NSA*}
    3.16  lemma hrabs_less_gt_zero: "abs x < r ==> (0::hypreal) < r"
    3.17  by (blast intro!: order_le_less_trans abs_ge_zero)
    3.18  
    3.19  lemma hrabs_disj: "abs x = (x::hypreal) | abs x = -x"
    3.20 -by (simp add: hrabs_def)
    3.21 +by (simp add: abs_if)
    3.22  
    3.23  (* Needed in Geom.ML *)
    3.24  lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y"
    3.25 -by (simp add: hrabs_def split add: split_if_asm)
    3.26 +by (simp add: abs_if split add: split_if_asm)
    3.27  
    3.28  lemma hypreal_of_real_hrabs:
    3.29      "abs (hypreal_of_real r) = hypreal_of_real (abs r)"
     4.1 --- a/src/HOL/Hyperreal/HyperPow.thy	Thu Jun 24 17:51:28 2004 +0200
     4.2 +++ b/src/HOL/Hyperreal/HyperPow.thy	Thu Jun 24 17:52:02 2004 +0200
     4.3 @@ -16,7 +16,7 @@
     4.4     hpowr_Suc: "r ^ (Suc n) = (r::hypreal) * (r ^ n)"
     4.5  
     4.6  
     4.7 -instance hypreal :: ringpower
     4.8 +instance hypreal :: recpower
     4.9  proof
    4.10    fix z :: hypreal
    4.11    fix n :: nat
    4.12 @@ -39,25 +39,21 @@
    4.13  lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r"
    4.14  by simp
    4.15  
    4.16 -lemma hrealpow_two_le: "(0::hypreal) \<le> r ^ Suc (Suc 0)"
    4.17 +lemma hrealpow_two_le [simp]: "(0::hypreal) \<le> r ^ Suc (Suc 0)"
    4.18  by (auto simp add: zero_le_mult_iff)
    4.19 -declare hrealpow_two_le [simp]
    4.20  
    4.21 -lemma hrealpow_two_le_add_order:
    4.22 +lemma hrealpow_two_le_add_order [simp]:
    4.23       "(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0)"
    4.24  by (simp only: hrealpow_two_le hypreal_le_add_order)
    4.25 -declare hrealpow_two_le_add_order [simp]
    4.26  
    4.27 -lemma hrealpow_two_le_add_order2:
    4.28 +lemma hrealpow_two_le_add_order2 [simp]:
    4.29       "(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0) + w ^ Suc (Suc 0)"
    4.30 -apply (simp only: hrealpow_two_le hypreal_le_add_order)
    4.31 -done
    4.32 -declare hrealpow_two_le_add_order2 [simp]
    4.33 +by (simp only: hrealpow_two_le hypreal_le_add_order)
    4.34  
    4.35  lemma hypreal_add_nonneg_eq_0_iff:
    4.36       "[| 0 \<le> x; 0 \<le> y |] ==> (x+y = 0) = (x = 0 & y = (0::hypreal))"
    4.37 -apply arith
    4.38 -done
    4.39 +by arith
    4.40 +
    4.41  
    4.42  text{*FIXME: DELETE THESE*}
    4.43  lemma hypreal_three_squares_add_zero_iff:
    4.44 @@ -78,12 +74,11 @@
    4.45  lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \<le> 2 ^ n"
    4.46  by (insert power_increasing [of 0 n "2::hypreal"], simp)
    4.47  
    4.48 -lemma two_hrealpow_gt: "hypreal_of_nat n < 2 ^ n"
    4.49 +lemma two_hrealpow_gt [simp]: "hypreal_of_nat n < 2 ^ n"
    4.50  apply (induct_tac "n")
    4.51  apply (auto simp add: hypreal_of_nat_Suc left_distrib)
    4.52  apply (cut_tac n = n in two_hrealpow_ge_one, arith)
    4.53  done
    4.54 -declare two_hrealpow_gt [simp] 
    4.55  
    4.56  lemma hrealpow:
    4.57      "Abs_hypreal(hyprel``{%n. X n}) ^ m = Abs_hypreal(hyprel``{%n. (X n) ^ m})"
    4.58 @@ -99,11 +94,9 @@
    4.59  
    4.60  subsection{*Literal Arithmetic Involving Powers and Type @{typ hypreal}*}
    4.61  
    4.62 -lemma hypreal_of_real_power: "hypreal_of_real (x ^ n) = hypreal_of_real x ^ n"
    4.63 -apply (induct_tac "n")
    4.64 -apply (simp_all add: nat_mult_distrib)
    4.65 -done
    4.66 -declare hypreal_of_real_power [simp]
    4.67 +lemma hypreal_of_real_power [simp]:
    4.68 +     "hypreal_of_real (x ^ n) = hypreal_of_real x ^ n"
    4.69 +by (induct_tac "n", simp_all add: nat_mult_distrib)
    4.70  
    4.71  lemma power_hypreal_of_real_number_of:
    4.72       "(number_of v :: hypreal) ^ n = hypreal_of_real ((number_of v) ^ n)"
    4.73 @@ -169,11 +162,10 @@
    4.74  apply (auto simp add: hyperpow hypnat_add hypreal_mult power_add)
    4.75  done
    4.76  
    4.77 -lemma hyperpow_one: "r pow (1::hypnat) = r"
    4.78 +lemma hyperpow_one [simp]: "r pow (1::hypnat) = r"
    4.79  apply (unfold hypnat_one_def, cases r)
    4.80  apply (auto simp add: hyperpow)
    4.81  done
    4.82 -declare hyperpow_one [simp]
    4.83  
    4.84  lemma hyperpow_two:
    4.85       "r pow ((1::hypnat) + (1::hypnat)) = r * r"
    4.86 @@ -200,57 +192,48 @@
    4.87  apply (auto intro: power_mono)
    4.88  done
    4.89  
    4.90 -lemma hyperpow_eq_one: "1 pow n = (1::hypreal)"
    4.91 +lemma hyperpow_eq_one [simp]: "1 pow n = (1::hypreal)"
    4.92  apply (cases n)
    4.93  apply (auto simp add: hypreal_one_def hyperpow)
    4.94  done
    4.95 -declare hyperpow_eq_one [simp]
    4.96  
    4.97 -lemma hrabs_hyperpow_minus_one: "abs(-1 pow n) = (1::hypreal)"
    4.98 +lemma hrabs_hyperpow_minus_one [simp]: "abs(-1 pow n) = (1::hypreal)"
    4.99  apply (subgoal_tac "abs ((- (1::hypreal)) pow n) = (1::hypreal) ")
   4.100  apply simp
   4.101  apply (cases n)
   4.102  apply (auto simp add: hypreal_one_def hyperpow hypreal_minus hypreal_hrabs)
   4.103  done
   4.104 -declare hrabs_hyperpow_minus_one [simp]
   4.105  
   4.106  lemma hyperpow_mult: "(r * s) pow n = (r pow n) * (s pow n)"
   4.107  apply (cases n, cases r, cases s)
   4.108  apply (auto simp add: hyperpow hypreal_mult power_mult_distrib)
   4.109  done
   4.110  
   4.111 -lemma hyperpow_two_le: "(0::hypreal) \<le> r pow ((1::hypnat) + (1::hypnat))"
   4.112 +lemma hyperpow_two_le [simp]: "0 \<le> r pow (1 + 1)"
   4.113  by (auto simp add: hyperpow_two zero_le_mult_iff)
   4.114 -declare hyperpow_two_le [simp]
   4.115  
   4.116  lemma hrabs_hyperpow_two [simp]: "abs(x pow (1 + 1)) = x pow (1 + 1)"
   4.117 -by (simp add: hrabs_def hyperpow_two_le)
   4.118 +by (simp add: abs_if hyperpow_two_le linorder_not_less)
   4.119  
   4.120 -lemma hyperpow_two_hrabs:
   4.121 -     "abs(x) pow (1 + 1)  = x pow (1 + 1)"
   4.122 -apply (simp add: hyperpow_hrabs)
   4.123 -done
   4.124 -declare hyperpow_two_hrabs [simp]
   4.125 +lemma hyperpow_two_hrabs [simp]: "abs(x) pow (1 + 1)  = x pow (1 + 1)"
   4.126 +by (simp add: hyperpow_hrabs)
   4.127  
   4.128 -lemma hyperpow_two_gt_one:
   4.129 -     "(1::hypreal) < r ==> 1 < r pow (1 + 1)"
   4.130 +lemma hyperpow_two_gt_one: "1 < r ==> 1 < r pow (1 + 1)"
   4.131  apply (auto simp add: hyperpow_two)
   4.132  apply (rule_tac y = "1*1" in order_le_less_trans)
   4.133  apply (rule_tac [2] hypreal_mult_less_mono, auto)
   4.134  done
   4.135  
   4.136  lemma hyperpow_two_ge_one:
   4.137 -     "(1::hypreal) \<le> r ==> 1 \<le> r pow (1 + 1)"
   4.138 -apply (auto dest!: order_le_imp_less_or_eq intro: hyperpow_two_gt_one order_less_imp_le)
   4.139 -done
   4.140 +     "1 \<le> r ==> 1 \<le> r pow (1 + 1)"
   4.141 +by (auto dest!: order_le_imp_less_or_eq intro: hyperpow_two_gt_one order_less_imp_le)
   4.142  
   4.143 -lemma two_hyperpow_ge_one: "(1::hypreal) \<le> 2 pow n"
   4.144 +lemma two_hyperpow_ge_one [simp]: "(1::hypreal) \<le> 2 pow n"
   4.145  apply (rule_tac y = "1 pow n" in order_trans)
   4.146  apply (rule_tac [2] hyperpow_le, auto)
   4.147  done
   4.148 -declare two_hyperpow_ge_one [simp]
   4.149  
   4.150 -lemma hyperpow_minus_one2:
   4.151 +lemma hyperpow_minus_one2 [simp]:
   4.152       "-1 pow ((1 + 1)*n) = (1::hypreal)"
   4.153  apply (subgoal_tac " (- ((1::hypreal))) pow ((1 + 1)*n) = (1::hypreal) ")
   4.154  apply simp
   4.155 @@ -258,7 +241,6 @@
   4.156  apply (auto simp add: nat_mult_2 [symmetric] hyperpow hypnat_add hypreal_minus
   4.157                        left_distrib)
   4.158  done
   4.159 -declare hyperpow_minus_one2 [simp]
   4.160  
   4.161  lemma hyperpow_less_le:
   4.162       "[|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
   4.163 @@ -277,18 +259,16 @@
   4.164  
   4.165  lemma hyperpow_realpow:
   4.166        "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"
   4.167 -apply (simp add: hypreal_of_real_def hypnat_of_nat_eq hyperpow)
   4.168 -done
   4.169 +by (simp add: hypreal_of_real_def hypnat_of_nat_eq hyperpow)
   4.170  
   4.171 -lemma hyperpow_SReal: "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals"
   4.172 -apply (unfold SReal_def)
   4.173 -apply (simp (no_asm) del: hypreal_of_real_power add: hyperpow_realpow)
   4.174 -done
   4.175 -declare hyperpow_SReal [simp]
   4.176 +lemma hyperpow_SReal [simp]:
   4.177 +     "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals"
   4.178 +by (simp del: hypreal_of_real_power add: hyperpow_realpow SReal_def)
   4.179  
   4.180 -lemma hyperpow_zero_HNatInfinite: "N \<in> HNatInfinite ==> (0::hypreal) pow N = 0"
   4.181 +
   4.182 +lemma hyperpow_zero_HNatInfinite [simp]:
   4.183 +     "N \<in> HNatInfinite ==> (0::hypreal) pow N = 0"
   4.184  by (drule HNatInfinite_is_Suc, auto)
   4.185 -declare hyperpow_zero_HNatInfinite [simp]
   4.186  
   4.187  lemma hyperpow_le_le:
   4.188       "[| (0::hypreal) \<le> r; r \<le> 1; n \<le> N |] ==> r pow N \<le> r pow n"
     5.1 --- a/src/HOL/Hyperreal/Lim.thy	Thu Jun 24 17:51:28 2004 +0200
     5.2 +++ b/src/HOL/Hyperreal/Lim.thy	Thu Jun 24 17:52:02 2004 +0200
     5.3 @@ -1328,7 +1328,7 @@
     5.4  apply (drule_tac P = "%na. no\<le>na --> ?Q na" and x = "no + n" in spec, auto)
     5.5  apply (subgoal_tac "lim f \<le> f (no + n) ")
     5.6  apply (induct_tac [2] "no")
     5.7 -apply (auto intro: order_trans simp add: diff_minus real_abs_def)
     5.8 +apply (auto intro: order_trans simp add: diff_minus abs_if)
     5.9  apply (drule_tac no=no and m=n in lemma_f_mono_add)
    5.10  apply (auto simp add: add_commute)
    5.11  done
    5.12 @@ -1660,22 +1660,38 @@
    5.13  apply (rule_tac [4] x = xb in exI, simp_all)
    5.14  done
    5.15  
    5.16 -(*----------------------------------------------------------------------------*)
    5.17 -(* If f'(x) > 0 then x is locally strictly increasing at the right            *)
    5.18 -(*----------------------------------------------------------------------------*)
    5.19 +
    5.20 +subsection{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*}
    5.21  
    5.22  lemma DERIV_left_inc:
    5.23 -    "[| DERIV f x :> l;  0 < l |]
    5.24 -     ==> \<exists>d. 0 < d & (\<forall>h. 0 < h & h < d --> f(x) < f(x + h))"
    5.25 -apply (simp add: deriv_def LIM_def)
    5.26 -apply (drule spec, auto)
    5.27 -apply (rule_tac x = s in exI, auto)
    5.28 -apply (subgoal_tac "0 < l*h")
    5.29 - prefer 2 apply (simp add: zero_less_mult_iff)
    5.30 -apply (drule_tac x = h in spec)
    5.31 -apply (simp add: real_abs_def pos_le_divide_eq pos_less_divide_eq 
    5.32 -            split add: split_if_asm)
    5.33 -done
    5.34 +  assumes der: "DERIV f x :> l"
    5.35 +      and l:   "0 < l"
    5.36 +  shows "\<exists>d. 0 < d & (\<forall>h. 0 < h & h < d --> f(x) < f(x + h))"
    5.37 +proof -
    5.38 +  from l der [THEN DERIV_D, THEN LIM_D [where r = "l"]]
    5.39 +  have "\<exists>s. 0 < s \<and>
    5.40 +              (\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < l)"
    5.41 +    by (simp add: diff_minus)
    5.42 +  then obtain s
    5.43 +        where s:   "0 < s" 
    5.44 +          and all: "!!z. z \<noteq> 0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>(f(x+z) - f x) / z - l\<bar> < l"
    5.45 +    by auto
    5.46 +  thus ?thesis
    5.47 +  proof (intro exI conjI strip)
    5.48 +    show "0<s" .
    5.49 +    fix h::real
    5.50 +    assume "0 < h \<and> h < s"
    5.51 +    with all [of h] show "f x < f (x+h)" 
    5.52 +    proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric] 
    5.53 +		split add: split_if_asm)
    5.54 +      assume "~ (f (x+h) - f x) / h < l" and h: "0 < h" 
    5.55 +      with l 
    5.56 +      have "0 < (f (x+h) - f x) / h" by arith
    5.57 +      thus "f x < f (x+h)"
    5.58 +	by (simp add: pos_less_divide_eq h)
    5.59 +    qed
    5.60 +  qed
    5.61 +qed
    5.62  
    5.63  lemma DERIV_left_dec:
    5.64    assumes der: "DERIV f x :> l"
    5.65 @@ -1696,9 +1712,9 @@
    5.66      fix h::real
    5.67      assume "0 < h \<and> h < s"
    5.68      with all [of "-h"] show "f x < f (x-h)" 
    5.69 -    proof (simp add: real_abs_def pos_less_divide_eq diff_minus [symmetric] 
    5.70 +    proof (simp add: abs_if pos_less_divide_eq diff_minus [symmetric] 
    5.71  		split add: split_if_asm)
    5.72 -      assume "~ l \<le> - ((f (x-h) - f x) / h)" and h: "0 < h" 
    5.73 +      assume " - ((f (x-h) - f x) / h) < l" and h: "0 < h" 
    5.74        with l 
    5.75        have "0 < (f (x-h) - f x) / h" by arith
    5.76        thus "f x < f (x-h)"
     6.1 --- a/src/HOL/Hyperreal/NSA.thy	Thu Jun 24 17:51:28 2004 +0200
     6.2 +++ b/src/HOL/Hyperreal/NSA.thy	Thu Jun 24 17:52:02 2004 +0200
     6.3 @@ -405,7 +405,7 @@
     6.4  by auto
     6.5  
     6.6  lemma Infinitesimal_hrabs_iff: "(abs x \<in> Infinitesimal) = (x \<in> Infinitesimal)"
     6.7 -by (auto simp add: hrabs_def)
     6.8 +by (auto simp add: abs_if)
     6.9  declare Infinitesimal_hrabs_iff [iff]
    6.10  
    6.11  lemma HFinite_diff_Infinitesimal_hrabs:
    6.12 @@ -845,7 +845,7 @@
    6.13  lemma SReal_not_Infinitesimal:
    6.14       "[| 0 < y;  y \<in> Reals|] ==> y \<notin> Infinitesimal"
    6.15  apply (simp add: Infinitesimal_def)
    6.16 -apply (auto simp add: hrabs_def)
    6.17 +apply (auto simp add: abs_if)
    6.18  done
    6.19  
    6.20  lemma SReal_minus_not_Infinitesimal:
    6.21 @@ -1324,7 +1324,7 @@
    6.22  by (auto simp add: hypreal_mult_commute HInfinite_HFinite_not_Infinitesimal_mult)
    6.23  
    6.24  lemma HInfinite_gt_SReal: "[| x \<in> HInfinite; 0 < x; y \<in> Reals |] ==> y < x"
    6.25 -by (auto dest!: bspec simp add: HInfinite_def hrabs_def order_less_imp_le)
    6.26 +by (auto dest!: bspec simp add: HInfinite_def abs_if order_less_imp_le)
    6.27  
    6.28  lemma HInfinite_gt_zero_gt_one: "[| x \<in> HInfinite; 0 < x |] ==> 1 < x"
    6.29  by (auto intro: HInfinite_gt_SReal)
     7.1 --- a/src/HOL/Hyperreal/Series.thy	Thu Jun 24 17:51:28 2004 +0200
     7.2 +++ b/src/HOL/Hyperreal/Series.thy	Thu Jun 24 17:52:02 2004 +0200
     7.3 @@ -506,7 +506,7 @@
     7.4  apply (rule_tac x = "abs (f N) * (1/ (1 - c)) / (c ^ N) " in exI)
     7.5  apply (rule sums_divide)
     7.6  apply (rule sums_mult)
     7.7 -apply (auto intro!: sums_mult geometric_sums simp add: real_abs_def)
     7.8 +apply (auto intro!: sums_mult geometric_sums simp add: abs_if)
     7.9  done
    7.10  
    7.11  
     8.1 --- a/src/HOL/Hyperreal/Star.thy	Thu Jun 24 17:51:28 2004 +0200
     8.2 +++ b/src/HOL/Hyperreal/Star.thy	Thu Jun 24 17:52:02 2004 +0200
     8.3 @@ -169,14 +169,11 @@
     8.4  
     8.5  
     8.6  (*
     8.7 -   Prove that hrabs is a nonstandard extension of rabs without
     8.8 +   Prove that abs for hypreal is a nonstandard extension of abs for real w/o
     8.9     use of congruence property (proved after this for general
    8.10 -   nonstandard extensions of real valued functions). This makes
    8.11 -   proof much longer- see comments at end of HREALABS.thy where
    8.12 -   we proved a congruence theorem for hrabs.
    8.13 +   nonstandard extensions of real valued functions). 
    8.14  
    8.15 -   NEW!!! No need to prove all the lemmas anymore. Use the ultrafilter
    8.16 -   tactic!
    8.17 +   Proof now Uses the ultrafilter tactic!
    8.18  *)
    8.19  
    8.20  lemma hrabs_is_starext_rabs: "is_starext abs abs"
    8.21 @@ -185,7 +182,9 @@
    8.22  apply (rule_tac z = y in eq_Abs_hypreal, auto)
    8.23  apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
    8.24  apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
    8.25 -apply (auto dest!: spec simp add: hypreal_minus hrabs_def hypreal_zero_def hypreal_le_def hypreal_less_def)
    8.26 +apply (auto dest!: spec 
    8.27 +            simp add: hypreal_minus abs_if hypreal_zero_def
    8.28 +                  hypreal_le hypreal_less)
    8.29  apply (arith | ultra)+
    8.30  done
    8.31  
    8.32 @@ -224,6 +223,7 @@
    8.33   ------------------------------------------*)
    8.34  lemma starfun_mult: "( *f* f) xa * ( *f* g) xa = ( *f* (%x. f x * g x)) xa"
    8.35  by (cases xa, simp add: starfun hypreal_mult)
    8.36 +
    8.37  declare starfun_mult [symmetric, simp]
    8.38  
    8.39  (*---------------------------------------
     9.1 --- a/src/HOL/Import/HOL4Compat.thy	Thu Jun 24 17:51:28 2004 +0200
     9.2 +++ b/src/HOL/Import/HOL4Compat.thy	Thu Jun 24 17:52:02 2004 +0200
     9.3 @@ -510,10 +510,10 @@
     9.4    by (simp add: real_of_nat_Suc)
     9.5  
     9.6  lemma abs: "abs (x::real) = (if 0 <= x then x else -x)"
     9.7 -  by (simp add: real_abs_def)
     9.8 +  by (simp add: abs_if)
     9.9  
    9.10  lemma pow: "(!x::real. x ^ 0 = 1) & (!x::real. ALL n. x ^ (Suc n) = x * x ^ n)"
    9.11 -  by simp;
    9.12 +  by simp
    9.13  
    9.14  constdefs
    9.15    real_gt :: "real => real => bool" 
    10.1 --- a/src/HOL/Integ/IntArith.thy	Thu Jun 24 17:51:28 2004 +0200
    10.2 +++ b/src/HOL/Integ/IntArith.thy	Thu Jun 24 17:52:02 2004 +0200
    10.3 @@ -130,7 +130,7 @@
    10.4  by (simp add: abs_if)
    10.5  
    10.6  lemma abs_power_minus_one [simp]:
    10.7 -     "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring,ringpower})"
    10.8 +     "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring,recpower})"
    10.9  by (simp add: power_abs)
   10.10  
   10.11  lemma of_int_number_of_eq:
   10.12 @@ -227,7 +227,7 @@
   10.13  
   10.14  lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
   10.15  apply (case_tac "z=0 | w=0")
   10.16 -apply (auto simp add: zabs_def nat_mult_distrib [symmetric] 
   10.17 +apply (auto simp add: abs_if nat_mult_distrib [symmetric] 
   10.18                        nat_mult_distrib_neg [symmetric] mult_less_0_iff)
   10.19  done
   10.20  
   10.21 @@ -318,7 +318,7 @@
   10.22  apply (case_tac "k = f (n+1) ")
   10.23   apply force
   10.24  apply (erule impE)
   10.25 - apply (simp add: zabs_def split add: split_if_asm)
   10.26 + apply (simp add: abs_if split add: split_if_asm)
   10.27  apply (blast intro: le_SucI)
   10.28  done
   10.29  
    11.1 --- a/src/HOL/Integ/IntDef.thy	Thu Jun 24 17:51:28 2004 +0200
    11.2 +++ b/src/HOL/Integ/IntDef.thy	Thu Jun 24 17:52:02 2004 +0200
    11.3 @@ -503,7 +503,7 @@
    11.4  done
    11.5  
    11.6  lemma abs_int_eq [simp]: "abs (int m) = int m"
    11.7 -by (simp add: zabs_def)
    11.8 +by (simp add: abs_if)
    11.9  
   11.10  text{*This version is proved for all ordered rings, not just integers!
   11.11        It is proved here because attribute @{text arith_split} is not available
    12.1 --- a/src/HOL/Integ/IntDiv.thy	Thu Jun 24 17:51:28 2004 +0200
    12.2 +++ b/src/HOL/Integ/IntDiv.thy	Thu Jun 24 17:52:02 2004 +0200
    12.3 @@ -1126,7 +1126,7 @@
    12.4    done
    12.5  
    12.6  lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
    12.7 -  apply (auto simp add: dvd_def zabs_def zmult_int [symmetric])
    12.8 +  apply (auto simp add: dvd_def abs_if zmult_int [symmetric])
    12.9      apply (rule_tac [3] x = "nat k" in exI)
   12.10      apply (rule_tac [2] x = "-(int k)" in exI)
   12.11      apply (rule_tac x = "nat (-k)" in exI)
   12.12 @@ -1172,7 +1172,7 @@
   12.13    "p ^ (Suc n) = (p::int) * (p ^ n)"
   12.14  
   12.15  
   12.16 -instance int :: ringpower
   12.17 +instance int :: recpower
   12.18  proof
   12.19    fix z :: int
   12.20    fix n :: nat
    13.1 --- a/src/HOL/Integ/NatBin.thy	Thu Jun 24 17:51:28 2004 +0200
    13.2 +++ b/src/HOL/Integ/NatBin.thy	Thu Jun 24 17:52:02 2004 +0200
    13.3 @@ -256,58 +256,58 @@
    13.4  We cannot prove general results about the numeral @{term "-1"}, so we have to
    13.5  use @{term "- 1"} instead.*}
    13.6  
    13.7 -lemma power2_eq_square: "(a::'a::{comm_semiring_1_cancel,ringpower})\<twosuperior> = a * a"
    13.8 +lemma power2_eq_square: "(a::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = a * a"
    13.9    by (simp add: numeral_2_eq_2 Power.power_Suc)
   13.10  
   13.11 -lemma [simp]: "(0::'a::{comm_semiring_1_cancel,ringpower})\<twosuperior> = 0"
   13.12 +lemma [simp]: "(0::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 0"
   13.13    by (simp add: power2_eq_square)
   13.14  
   13.15 -lemma [simp]: "(1::'a::{comm_semiring_1_cancel,ringpower})\<twosuperior> = 1"
   13.16 +lemma [simp]: "(1::'a::{comm_semiring_1_cancel,recpower})\<twosuperior> = 1"
   13.17    by (simp add: power2_eq_square)
   13.18  
   13.19  text{*Squares of literal numerals will be evaluated.*}
   13.20  declare power2_eq_square [of "number_of w", standard, simp]
   13.21  
   13.22 -lemma zero_le_power2 [simp]: "0 \<le> (a\<twosuperior>::'a::{ordered_idom,ringpower})"
   13.23 +lemma zero_le_power2 [simp]: "0 \<le> (a\<twosuperior>::'a::{ordered_idom,recpower})"
   13.24    by (simp add: power2_eq_square zero_le_square)
   13.25  
   13.26  lemma zero_less_power2 [simp]:
   13.27 -     "(0 < a\<twosuperior>) = (a \<noteq> (0::'a::{ordered_idom,ringpower}))"
   13.28 +     "(0 < a\<twosuperior>) = (a \<noteq> (0::'a::{ordered_idom,recpower}))"
   13.29    by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
   13.30  
   13.31  lemma zero_eq_power2 [simp]:
   13.32 -     "(a\<twosuperior> = 0) = (a = (0::'a::{ordered_idom,ringpower}))"
   13.33 +     "(a\<twosuperior> = 0) = (a = (0::'a::{ordered_idom,recpower}))"
   13.34    by (force simp add: power2_eq_square mult_eq_0_iff)
   13.35  
   13.36  lemma abs_power2 [simp]:
   13.37 -     "abs(a\<twosuperior>) = (a\<twosuperior>::'a::{ordered_idom,ringpower})"
   13.38 +     "abs(a\<twosuperior>) = (a\<twosuperior>::'a::{ordered_idom,recpower})"
   13.39    by (simp add: power2_eq_square abs_mult abs_mult_self)
   13.40  
   13.41  lemma power2_abs [simp]:
   13.42 -     "(abs a)\<twosuperior> = (a\<twosuperior>::'a::{ordered_idom,ringpower})"
   13.43 +     "(abs a)\<twosuperior> = (a\<twosuperior>::'a::{ordered_idom,recpower})"
   13.44    by (simp add: power2_eq_square abs_mult_self)
   13.45  
   13.46  lemma power2_minus [simp]:
   13.47 -     "(- a)\<twosuperior> = (a\<twosuperior>::'a::{comm_ring_1,ringpower})"
   13.48 +     "(- a)\<twosuperior> = (a\<twosuperior>::'a::{comm_ring_1,recpower})"
   13.49    by (simp add: power2_eq_square)
   13.50  
   13.51 -lemma power_minus1_even: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,ringpower})"
   13.52 +lemma power_minus1_even: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})"
   13.53  apply (induct_tac "n")
   13.54  apply (auto simp add: power_Suc power_add)
   13.55  done
   13.56  
   13.57 -lemma power_even_eq: "(a::'a::ringpower) ^ (2*n) = (a^n)^2"
   13.58 +lemma power_even_eq: "(a::'a::recpower) ^ (2*n) = (a^n)^2"
   13.59  by (simp add: power_mult power_mult_distrib power2_eq_square)
   13.60  
   13.61  lemma power_odd_eq: "(a::int) ^ Suc(2*n) = a * (a^n)^2"
   13.62  by (simp add: power_even_eq) 
   13.63  
   13.64  lemma power_minus_even [simp]:
   13.65 -     "(-a) ^ (2*n) = (a::'a::{comm_ring_1,ringpower}) ^ (2*n)"
   13.66 +     "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)"
   13.67  by (simp add: power_minus1_even power_minus [of a]) 
   13.68  
   13.69  lemma zero_le_even_power:
   13.70 -     "0 \<le> (a::'a::{ordered_idom,ringpower}) ^ (2*n)"
   13.71 +     "0 \<le> (a::'a::{ordered_idom,recpower}) ^ (2*n)"
   13.72  proof (induct "n")
   13.73    case 0
   13.74      show ?case by (simp add: zero_le_one)
   13.75 @@ -320,7 +320,7 @@
   13.76  qed
   13.77  
   13.78  lemma odd_power_less_zero:
   13.79 -     "(a::'a::{ordered_idom,ringpower}) < 0 ==> a ^ Suc(2*n) < 0"
   13.80 +     "(a::'a::{ordered_idom,recpower}) < 0 ==> a ^ Suc(2*n) < 0"
   13.81  proof (induct "n")
   13.82    case 0
   13.83      show ?case by (simp add: Power.power_Suc)
   13.84 @@ -333,7 +333,7 @@
   13.85  qed
   13.86  
   13.87  lemma odd_0_le_power_imp_0_le:
   13.88 -     "0 \<le> a  ^ Suc(2*n) ==> 0 \<le> (a::'a::{ordered_idom,ringpower})"
   13.89 +     "0 \<le> a  ^ Suc(2*n) ==> 0 \<le> (a::'a::{ordered_idom,recpower})"
   13.90  apply (insert odd_power_less_zero [of a n]) 
   13.91  apply (force simp add: linorder_not_less [symmetric]) 
   13.92  done
   13.93 @@ -606,10 +606,10 @@
   13.94  lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
   13.95    by (simp add: Let_def)
   13.96  
   13.97 -lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring,ringpower})"
   13.98 +lemma power_m1_even: "(-1) ^ (2*n) = (1::'a::{number_ring,recpower})"
   13.99  by (simp add: power_mult); 
  13.100  
  13.101 -lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring,ringpower})"
  13.102 +lemma power_m1_odd: "(-1) ^ Suc(2*n) = (-1::'a::{number_ring,recpower})"
  13.103  by (simp add: power_mult power_Suc); 
  13.104  
  13.105  
    14.1 --- a/src/HOL/Integ/Parity.thy	Thu Jun 24 17:51:28 2004 +0200
    14.2 +++ b/src/HOL/Integ/Parity.thy	Thu Jun 24 17:52:02 2004 +0200
    14.3 @@ -233,22 +233,22 @@
    14.4  subsection {* Powers of negative one *}
    14.5  
    14.6  lemma neg_one_even_odd_power:
    14.7 -     "(even x --> (-1::'a::{number_ring,ringpower})^x = 1) & 
    14.8 +     "(even x --> (-1::'a::{number_ring,recpower})^x = 1) & 
    14.9        (odd x --> (-1::'a)^x = -1)"
   14.10    apply (induct_tac x)
   14.11    apply (simp, simp add: power_Suc)
   14.12    done
   14.13  
   14.14  lemma neg_one_even_power [simp]:
   14.15 -     "even x ==> (-1::'a::{number_ring,ringpower})^x = 1"
   14.16 +     "even x ==> (-1::'a::{number_ring,recpower})^x = 1"
   14.17    by (rule neg_one_even_odd_power [THEN conjunct1, THEN mp], assumption)
   14.18  
   14.19  lemma neg_one_odd_power [simp]:
   14.20 -     "odd x ==> (-1::'a::{number_ring,ringpower})^x = -1"
   14.21 +     "odd x ==> (-1::'a::{number_ring,recpower})^x = -1"
   14.22    by (rule neg_one_even_odd_power [THEN conjunct2, THEN mp], assumption)
   14.23  
   14.24  lemma neg_power_if:
   14.25 -     "(-x::'a::{comm_ring_1,ringpower}) ^ n = 
   14.26 +     "(-x::'a::{comm_ring_1,recpower}) ^ n = 
   14.27        (if even n then (x ^ n) else -(x ^ n))"
   14.28    by (induct n, simp_all split: split_if_asm add: power_Suc) 
   14.29  
   14.30 @@ -256,13 +256,13 @@
   14.31  subsection {* An Equivalence for @{term "0 \<le> a^n"} *}
   14.32  
   14.33  lemma even_power_le_0_imp_0:
   14.34 -     "a ^ (2*k) \<le> (0::'a::{ordered_idom,ringpower}) ==> a=0"
   14.35 +     "a ^ (2*k) \<le> (0::'a::{ordered_idom,recpower}) ==> a=0"
   14.36  apply (induct k) 
   14.37  apply (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc)  
   14.38  done
   14.39  
   14.40  lemma zero_le_power_iff:
   14.41 -     "(0 \<le> a^n) = (0 \<le> (a::'a::{ordered_idom,ringpower}) | even n)"
   14.42 +     "(0 \<le> a^n) = (0 \<le> (a::'a::{ordered_idom,recpower}) | even n)"
   14.43        (is "?P n")
   14.44  proof cases
   14.45    assume even: "even n"
    15.1 --- a/src/HOL/NumberTheory/EulerFermat.thy	Thu Jun 24 17:51:28 2004 +0200
    15.2 +++ b/src/HOL/NumberTheory/EulerFermat.thy	Thu Jun 24 17:52:02 2004 +0200
    15.3 @@ -60,7 +60,7 @@
    15.4  
    15.5  lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)"
    15.6    -- {* LCP: not sure why this lemma is needed now *}
    15.7 -by (auto simp add: zabs_def)
    15.8 +by (auto simp add: abs_if)
    15.9  
   15.10  
   15.11  text {* \medskip @{text norRRset} *}
    16.1 --- a/src/HOL/NumberTheory/Fib.thy	Thu Jun 24 17:51:28 2004 +0200
    16.2 +++ b/src/HOL/NumberTheory/Fib.thy	Thu Jun 24 17:52:02 2004 +0200
    16.3 @@ -66,7 +66,8 @@
    16.4    much easier to prove using integers!
    16.5  *}
    16.6  
    16.7 -lemma fib_Cassini: "int (fib (Suc (Suc n)) * fib n) =
    16.8 +lemma fib_Cassini:
    16.9 + "int (fib (Suc (Suc n)) * fib n) =
   16.10    (if n mod 2 = 0 then int (fib (Suc n) * fib (Suc n)) - 1
   16.11     else int (fib (Suc n) * fib (Suc n)) + 1)"
   16.12    apply (induct n rule: fib.induct)
    17.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Thu Jun 24 17:51:28 2004 +0200
    17.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Thu Jun 24 17:52:02 2004 +0200
    17.3 @@ -65,10 +65,10 @@
    17.4  subsection {* Euclid's Algorithm and GCD *}
    17.5  
    17.6  lemma zgcd_0 [simp]: "zgcd (m, 0) = abs m"
    17.7 -  by (simp add: zgcd_def zabs_def)
    17.8 +  by (simp add: zgcd_def abs_if)
    17.9  
   17.10  lemma zgcd_0_left [simp]: "zgcd (0, m) = abs m"
   17.11 -  by (simp add: zgcd_def zabs_def)
   17.12 +  by (simp add: zgcd_def abs_if)
   17.13  
   17.14  lemma zgcd_zminus [simp]: "zgcd (-m, n) = zgcd (m, n)"
   17.15    by (simp add: zgcd_def)
   17.16 @@ -78,7 +78,7 @@
   17.17  
   17.18  lemma zgcd_non_0: "0 < n ==> zgcd (m, n) = zgcd (n, m mod n)"
   17.19    apply (frule_tac b = n and a = m in pos_mod_sign)
   17.20 -  apply (simp del: pos_mod_sign add: zgcd_def zabs_def nat_mod_distrib)
   17.21 +  apply (simp del: pos_mod_sign add: zgcd_def abs_if nat_mod_distrib)
   17.22    apply (auto simp add: gcd_non_0 nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
   17.23    apply (frule_tac a = m in pos_mod_bound)
   17.24    apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2 nat_le_eq_zle)
   17.25 @@ -91,19 +91,19 @@
   17.26    done
   17.27  
   17.28  lemma zgcd_1 [simp]: "zgcd (m, 1) = 1"
   17.29 -  by (simp add: zgcd_def zabs_def)
   17.30 +  by (simp add: zgcd_def abs_if)
   17.31  
   17.32  lemma zgcd_0_1_iff [simp]: "(zgcd (0, m) = 1) = (abs m = 1)"
   17.33 -  by (simp add: zgcd_def zabs_def)
   17.34 +  by (simp add: zgcd_def abs_if)
   17.35  
   17.36  lemma zgcd_zdvd1 [iff]: "zgcd (m, n) dvd m"
   17.37 -  by (simp add: zgcd_def zabs_def int_dvd_iff)
   17.38 +  by (simp add: zgcd_def abs_if int_dvd_iff)
   17.39  
   17.40  lemma zgcd_zdvd2 [iff]: "zgcd (m, n) dvd n"
   17.41 -  by (simp add: zgcd_def zabs_def int_dvd_iff)
   17.42 +  by (simp add: zgcd_def abs_if int_dvd_iff)
   17.43  
   17.44  lemma zgcd_greatest_iff: "k dvd zgcd (m, n) = (k dvd m \<and> k dvd n)"
   17.45 -  by (simp add: zgcd_def zabs_def int_dvd_iff dvd_int_iff nat_dvd_iff)
   17.46 +  by (simp add: zgcd_def abs_if int_dvd_iff dvd_int_iff nat_dvd_iff)
   17.47  
   17.48  lemma zgcd_commute: "zgcd (m, n) = zgcd (n, m)"
   17.49    by (simp add: zgcd_def gcd_commute)
   17.50 @@ -125,11 +125,11 @@
   17.51  
   17.52  lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd (m, n) = zgcd (k * m, k * n)"
   17.53    by (simp del: minus_mult_right [symmetric]
   17.54 -      add: minus_mult_right nat_mult_distrib zgcd_def zabs_def
   17.55 +      add: minus_mult_right nat_mult_distrib zgcd_def abs_if
   17.56            mult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric])
   17.57  
   17.58  lemma zgcd_zmult_distrib2_abs: "zgcd (k * m, k * n) = abs k * zgcd (m, n)"
   17.59 -  by (simp add: zabs_def zgcd_zmult_distrib2)
   17.60 +  by (simp add: abs_if zgcd_zmult_distrib2)
   17.61  
   17.62  lemma zgcd_self [simp]: "0 \<le> m ==> zgcd (m, m) = m"
   17.63    by (cut_tac k = m and m = 1 and n = 1 in zgcd_zmult_distrib2, simp_all)
   17.64 @@ -465,7 +465,7 @@
   17.65    apply (rule exI)
   17.66    apply (rule exI)
   17.67    apply (subst xzgcda.simps, auto)
   17.68 -  apply (simp add: zabs_def)
   17.69 +  apply (simp add: abs_if)
   17.70    done
   17.71  
   17.72  lemma xzgcd_correct_aux2:
   17.73 @@ -481,7 +481,7 @@
   17.74     apply (frule_tac a = "r'" in pos_mod_sign, auto)
   17.75    apply (erule_tac P = "xzgcda ?u = ?v" in rev_mp)
   17.76    apply (subst xzgcda.simps, auto)
   17.77 -  apply (simp add: zabs_def)
   17.78 +  apply (simp add: abs_if)
   17.79    done
   17.80  
   17.81  lemma xzgcd_correct:
    18.1 --- a/src/HOL/Real/RealDef.thy	Thu Jun 24 17:51:28 2004 +0200
    18.2 +++ b/src/HOL/Real/RealDef.thy	Thu Jun 24 17:52:02 2004 +0200
    18.3 @@ -830,16 +830,16 @@
    18.4  
    18.5  text{*FIXME: these should go!*}
    18.6  lemma abs_eqI1: "(0::real)\<le>x ==> abs x = x"
    18.7 -by (simp add: real_abs_def)
    18.8 +by (simp add: abs_if)
    18.9  
   18.10  lemma abs_eqI2: "(0::real) < x ==> abs x = x"
   18.11 -by (simp add: real_abs_def)
   18.12 +by (simp add: abs_if)
   18.13  
   18.14  lemma abs_minus_eqI2: "x < (0::real) ==> abs x = -x"
   18.15 -by (simp add: real_abs_def linorder_not_less [symmetric])
   18.16 +by (simp add: abs_if linorder_not_less [symmetric])
   18.17  
   18.18  lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))"
   18.19 -by (simp add: real_abs_def)
   18.20 +by (simp add: abs_if)
   18.21  
   18.22  lemma abs_interval_iff: "(abs x < r) = (-r < x & x < (r::real))"
   18.23  by (force simp add: Ring_and_Field.abs_less_iff)
   18.24 @@ -849,7 +849,7 @@
   18.25  
   18.26  (*FIXME: used only once, in SEQ.ML*)
   18.27  lemma abs_add_one_gt_zero [simp]: "(0::real) < 1 + abs(x)"
   18.28 -by (simp add: real_abs_def)
   18.29 +by (simp add: abs_if)
   18.30  
   18.31  lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)"
   18.32  by (auto intro: abs_eqI1 simp add: real_of_nat_ge_zero)
    19.1 --- a/src/HOL/Real/RealPow.thy	Thu Jun 24 17:51:28 2004 +0200
    19.2 +++ b/src/HOL/Real/RealPow.thy	Thu Jun 24 17:52:02 2004 +0200
    19.3 @@ -17,7 +17,7 @@
    19.4       realpow_Suc: "r ^ (Suc n) = (r::real) * (r ^ n)"
    19.5  
    19.6  
    19.7 -instance real :: ringpower
    19.8 +instance real :: recpower
    19.9  proof
   19.10    fix z :: real
   19.11    fix n :: nat
    20.1 --- a/src/HOL/Real/real_arith.ML	Thu Jun 24 17:51:28 2004 +0200
    20.2 +++ b/src/HOL/Real/real_arith.ML	Thu Jun 24 17:52:02 2004 +0200
    20.3 @@ -12,8 +12,6 @@
    20.4  val real_mult_left_mono =
    20.5      read_instantiate_sg(sign_of (the_context())) [("a","?a::real")] mult_left_mono;
    20.6  
    20.7 -val real_abs_def = thm "real_abs_def";
    20.8 -
    20.9  val real_le_def = thm "real_le_def";
   20.10  val real_diff_def = thm "real_diff_def";
   20.11  val real_divide_def = thm "real_divide_def";