Defining the type class "ringpower" and deleting superseded theorems for
authorpaulson
Fri Jan 09 10:46:18 2004 +0100 (2004-01-09)
changeset 14348744c868ee0b7
parent 14347 1fff56703e29
child 14349 8d92e426eb38
Defining the type class "ringpower" and deleting superseded theorems for
types nat, int, real, hypreal
src/HOL/Complex/CLim.ML
src/HOL/Complex/Complex.thy
src/HOL/Complex/ComplexArith0.ML
src/HOL/Hyperreal/HTranscendental.ML
src/HOL/Hyperreal/HyperDef.thy
src/HOL/Hyperreal/HyperPow.ML
src/HOL/Hyperreal/HyperPow.thy
src/HOL/Hyperreal/Lim.ML
src/HOL/Hyperreal/MacLaurin.ML
src/HOL/Hyperreal/NthRoot.thy
src/HOL/Hyperreal/Poly.ML
src/HOL/Hyperreal/SEQ.ML
src/HOL/Hyperreal/Series.ML
src/HOL/Hyperreal/Transcendental.ML
src/HOL/Integ/Int.thy
src/HOL/Integ/IntDef.thy
src/HOL/Integ/IntPower.thy
src/HOL/IsaMakefile
src/HOL/Library/Rational_Numbers.thy
src/HOL/Nat.thy
src/HOL/NumberTheory/EvenOdd.thy
src/HOL/Power.ML
src/HOL/Power.thy
src/HOL/Real/RealDef.thy
src/HOL/Real/RealPow.thy
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Complex/CLim.ML	Fri Jan 09 01:28:24 2004 +0100
     1.2 +++ b/src/HOL/Complex/CLim.ML	Fri Jan 09 10:46:18 2004 +0100
     1.3 @@ -852,13 +852,10 @@
     1.4  
     1.5  Goal "NSCDERIV f x :> D ==> NSCDERIV (%x. c * f x) x :> c*D";
     1.6  by (asm_full_simp_tac 
     1.7 -    (simpset() addsimps [complex_times_divide1_eq RS sym, NSCDERIV_NSCLIM_iff,
     1.8 -                         complex_minus_mult_eq2, complex_add_mult_distrib2 RS sym,
     1.9 +    (simpset() addsimps [times_divide_eq_right RS sym, NSCDERIV_NSCLIM_iff,
    1.10 +                         minus_mult_right, complex_add_mult_distrib2 RS sym,
    1.11                           complex_diff_def] 
    1.12 -             delsimps [complex_times_divide1_eq, complex_minus_mult_eq2 RS sym]
    1.13 -             delsimps [times_divide_eq_right, minus_mult_right RS sym]
    1.14 -
    1.15 -) 1);
    1.16 +             delsimps [times_divide_eq_right, minus_mult_right RS sym]) 1);
    1.17  by (etac (NSCLIM_const RS NSCLIM_mult) 1);
    1.18  qed "NSCDERIV_cmult";
    1.19  
     2.1 --- a/src/HOL/Complex/Complex.thy	Fri Jan 09 01:28:24 2004 +0100
     2.2 +++ b/src/HOL/Complex/Complex.thy	Fri Jan 09 10:46:18 2004 +0100
     2.3 @@ -577,119 +577,8 @@
     2.4  qed
     2.5  
     2.6  
     2.7 -lemma complex_mult_minus_one: "-(1::complex) * z = -z"
     2.8 -apply (simp (no_asm))
     2.9 -done
    2.10 -declare complex_mult_minus_one [simp]
    2.11 -
    2.12 -lemma complex_mult_minus_one_right: "z * -(1::complex) = -z"
    2.13 -apply (subst complex_mult_commute)
    2.14 -apply (simp (no_asm))
    2.15 -done
    2.16 -declare complex_mult_minus_one_right [simp]
    2.17 -
    2.18 -lemma complex_minus_mult_cancel: "-x * -y = x * (y::complex)"
    2.19 -apply (simp (no_asm))
    2.20 -done
    2.21 -declare complex_minus_mult_cancel [simp]
    2.22 -
    2.23  lemma complex_minus_mult_commute: "-x * y = x * -(y::complex)"
    2.24 -apply (simp (no_asm))
    2.25 -done
    2.26 -
    2.27 -
    2.28 -lemma complex_mult_left_cancel: "(c::complex) ~= 0 ==> (c*a=c*b) = (a=b)"
    2.29 -apply auto
    2.30 -apply (drule_tac f = "%x. x*inverse c" in arg_cong)
    2.31 -apply (simp add: complex_mult_ac)
    2.32 -done
    2.33 -
    2.34 -lemma complex_mult_right_cancel: "(c::complex) ~= 0 ==> (a*c=b*c) = (a=b)"
    2.35 -apply safe
    2.36 -apply (drule_tac f = "%x. x*inverse c" in arg_cong)
    2.37 -apply (simp add: complex_mult_ac)
    2.38 -done
    2.39 -
    2.40 -lemma complex_inverse_not_zero: "z ~= 0 ==> inverse(z::complex) ~= 0"
    2.41 -apply safe
    2.42 -apply (frule complex_mult_right_cancel [THEN iffD2])
    2.43 -apply (erule_tac [2] V = "inverse z = 0" in thin_rl)
    2.44 -apply (assumption, auto)
    2.45 -done
    2.46 -declare complex_inverse_not_zero [simp]
    2.47 -
    2.48 -lemma complex_mult_not_zero: "!!x. [| x ~= 0; y ~= (0::complex) |] ==> x * y ~= 0"
    2.49 -apply safe
    2.50 -apply (drule_tac f = "%z. inverse x*z" in arg_cong)
    2.51 -apply (simp add: complex_mult_assoc [symmetric])
    2.52 -done
    2.53 -
    2.54 -lemmas complex_mult_not_zeroE = complex_mult_not_zero [THEN notE, standard]
    2.55 -
    2.56 -lemma complex_inverse_inverse: "inverse(inverse (x::complex)) = x"
    2.57 -apply (case_tac "x = 0", simp add: COMPLEX_INVERSE_ZERO)
    2.58 -apply (rule_tac c1 = "inverse x" in complex_mult_right_cancel [THEN iffD1])
    2.59 -apply (erule complex_inverse_not_zero)
    2.60 -apply (auto dest: complex_inverse_not_zero)
    2.61 -done
    2.62 -declare complex_inverse_inverse [simp]
    2.63 -
    2.64 -lemma complex_inverse_one: "inverse(1::complex) = 1"
    2.65 -apply (unfold complex_one_def)
    2.66 -apply (simp (no_asm) add: complex_inverse)
    2.67 -done
    2.68 -declare complex_inverse_one [simp]
    2.69 -
    2.70 -lemma complex_minus_inverse: "inverse(-x) = -inverse(x::complex)"
    2.71 -apply (case_tac "x = 0", simp add: COMPLEX_INVERSE_ZERO)
    2.72 -apply (rule_tac c1 = "-x" in complex_mult_right_cancel [THEN iffD1], force)
    2.73 -apply (subst complex_mult_inv_left, auto)
    2.74 -done
    2.75 -
    2.76 -lemma complex_inverse_distrib: "inverse(x*y) = inverse x * inverse (y::complex)"
    2.77 -apply (rule inverse_mult_distrib) 
    2.78 -done
    2.79 -
    2.80 -
    2.81 -subsection{*Division*}
    2.82 -
    2.83 -(*adding some of these theorems to simpset as for reals:
    2.84 -  not 100% convinced for some*)
    2.85 -
    2.86 -lemma complex_times_divide1_eq: "(x::complex) * (y/z) = (x*y)/z"
    2.87 -apply (simp (no_asm) add: complex_divide_def complex_mult_assoc)
    2.88 -done
    2.89 -
    2.90 -lemma complex_times_divide2_eq: "(y/z) * (x::complex) = (y*x)/z"
    2.91 -apply (simp (no_asm) add: complex_divide_def complex_mult_ac)
    2.92 -done
    2.93 -
    2.94 -declare complex_times_divide1_eq [simp] complex_times_divide2_eq [simp]
    2.95 -
    2.96 -lemma complex_divide_divide1_eq: "(x::complex) / (y/z) = (x*z)/y"
    2.97 -apply (simp (no_asm) add: complex_divide_def complex_inverse_distrib complex_mult_ac)
    2.98 -done
    2.99 -
   2.100 -lemma complex_divide_divide2_eq: "((x::complex) / y) / z = x/(y*z)"
   2.101 -apply (simp (no_asm) add: complex_divide_def complex_inverse_distrib complex_mult_assoc)
   2.102 -done
   2.103 -
   2.104 -declare complex_divide_divide1_eq [simp] complex_divide_divide2_eq [simp]
   2.105 -
   2.106 -(** As with multiplication, pull minus signs OUT of the / operator **)
   2.107 -
   2.108 -lemma complex_minus_divide_eq: "(-x) / (y::complex) = - (x/y)"
   2.109 -apply (simp (no_asm) add: complex_divide_def)
   2.110 -done
   2.111 -declare complex_minus_divide_eq [simp]
   2.112 -
   2.113 -lemma complex_divide_minus_eq: "(x / -(y::complex)) = - (x/y)"
   2.114 -apply (simp (no_asm) add: complex_divide_def complex_minus_inverse)
   2.115 -done
   2.116 -declare complex_divide_minus_eq [simp]
   2.117 -
   2.118 -lemma complex_add_divide_distrib: "(x+y)/(z::complex) = x/z + y/z"
   2.119 -apply (simp (no_asm) add: complex_divide_def complex_add_mult_distrib)
   2.120 +apply (simp)
   2.121  done
   2.122  
   2.123  subsection{*Embedding Properties for @{term complex_of_real} Map*}
   2.124 @@ -713,7 +602,8 @@
   2.125  done
   2.126  declare complex_of_real_zero [simp]
   2.127  
   2.128 -lemma complex_of_real_eq_iff: "(complex_of_real x = complex_of_real y) = (x = y)"
   2.129 +lemma complex_of_real_eq_iff:
   2.130 +     "(complex_of_real x = complex_of_real y) = (x = y)"
   2.131  by (auto dest: inj_complex_of_real [THEN injD])
   2.132  declare complex_of_real_eq_iff [iff]
   2.133  
   2.134 @@ -721,22 +611,25 @@
   2.135  apply (simp (no_asm) add: complex_of_real_def complex_minus)
   2.136  done
   2.137  
   2.138 -lemma complex_of_real_inverse: "complex_of_real(inverse x) = inverse(complex_of_real x)"
   2.139 -apply (case_tac "x=0")
   2.140 -apply (simp add: DIVISION_BY_ZERO COMPLEX_INVERSE_ZERO)
   2.141 +lemma complex_of_real_inverse:
   2.142 + "complex_of_real(inverse x) = inverse(complex_of_real x)"
   2.143 +apply (case_tac "x=0", simp)
   2.144  apply (simp add: complex_inverse complex_of_real_def real_divide_def 
   2.145                   inverse_mult_distrib real_power_two)
   2.146  done
   2.147  
   2.148 -lemma complex_of_real_add: "complex_of_real x + complex_of_real y = complex_of_real (x + y)"
   2.149 +lemma complex_of_real_add:
   2.150 + "complex_of_real x + complex_of_real y = complex_of_real (x + y)"
   2.151  apply (simp (no_asm) add: complex_add complex_of_real_def)
   2.152  done
   2.153  
   2.154 -lemma complex_of_real_diff: "complex_of_real x - complex_of_real y = complex_of_real (x - y)"
   2.155 +lemma complex_of_real_diff:
   2.156 + "complex_of_real x - complex_of_real y = complex_of_real (x - y)"
   2.157  apply (simp (no_asm) add: complex_of_real_minus [symmetric] complex_diff_def complex_of_real_add)
   2.158  done
   2.159  
   2.160 -lemma complex_of_real_mult: "complex_of_real x * complex_of_real y = complex_of_real (x * y)"
   2.161 +lemma complex_of_real_mult:
   2.162 + "complex_of_real x * complex_of_real y = complex_of_real (x * y)"
   2.163  apply (simp (no_asm) add: complex_mult complex_of_real_def)
   2.164  done
   2.165  
   2.166 @@ -764,19 +657,18 @@
   2.167  done
   2.168  declare complex_mod_zero [simp]
   2.169  
   2.170 -lemma complex_mod_one: "cmod(1) = 1"
   2.171 -by (unfold cmod_def, simp)
   2.172 -declare complex_mod_one [simp]
   2.173 +lemma complex_mod_one [simp]: "cmod(1) = 1"
   2.174 +by (simp add: cmod_def real_power_two)
   2.175  
   2.176  lemma complex_mod_complex_of_real: "cmod(complex_of_real x) = abs x"
   2.177 -apply (unfold complex_of_real_def)
   2.178 -apply (simp (no_asm) add: complex_mod)
   2.179 +apply (simp add: complex_of_real_def real_power_two complex_mod)
   2.180  done
   2.181  declare complex_mod_complex_of_real [simp]
   2.182  
   2.183 -lemma complex_of_real_abs: "complex_of_real (abs x) = complex_of_real(cmod(complex_of_real x))"
   2.184 -apply (simp (no_asm))
   2.185 -done
   2.186 +lemma complex_of_real_abs:
   2.187 +     "complex_of_real (abs x) = complex_of_real(cmod(complex_of_real x))"
   2.188 +by (simp)
   2.189 +
   2.190  
   2.191  
   2.192  subsection{*Conjugation is an Automorphism*}
   2.193 @@ -801,7 +693,8 @@
   2.194  done
   2.195  declare complex_cnj_cnj [simp]
   2.196  
   2.197 -lemma complex_cnj_complex_of_real: "cnj (complex_of_real x) = complex_of_real x"
   2.198 +lemma complex_cnj_complex_of_real:
   2.199 + "cnj (complex_of_real x) = complex_of_real x"
   2.200  apply (unfold complex_of_real_def)
   2.201  apply (simp (no_asm) add: complex_cnj)
   2.202  done
   2.203 @@ -884,12 +777,6 @@
   2.204  
   2.205  subsection{*Algebra*}
   2.206  
   2.207 -lemma complex_mult_zero_iff: "(x*y = (0::complex)) = (x = 0 | y = 0)"
   2.208 -apply auto
   2.209 -apply (auto intro: ccontr dest: complex_mult_not_zero)
   2.210 -done
   2.211 -declare complex_mult_zero_iff [iff]
   2.212 -
   2.213  lemma complex_add_left_cancel_zero: "(x + y = x) = (y = (0::complex))"
   2.214  apply (unfold complex_zero_def)
   2.215  apply (rule_tac z = x in eq_Abs_complex)
   2.216 @@ -913,13 +800,6 @@
   2.217  
   2.218  subsection{*Modulus*}
   2.219  
   2.220 -(*
   2.221 -Goal "[| sqrt(x) = 0; 0 <= x |] ==> x = 0"
   2.222 -by (auto_tac (claset() addIs [real_sqrt_eq_zero_cancel],
   2.223 -    simpset()));
   2.224 -qed "real_sqrt_eq_zero_cancel2";
   2.225 -*)
   2.226 -
   2.227  lemma complex_mod_eq_zero_cancel: "(cmod x = 0) = (x = 0)"
   2.228  apply (rule_tac z = x in eq_Abs_complex)
   2.229  apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 simp add: complex_mod complex_zero_def real_power_two)
   2.230 @@ -960,7 +840,7 @@
   2.231  apply (rule_tac z = x in eq_Abs_complex)
   2.232  apply (rule_tac z = y in eq_Abs_complex)
   2.233  apply (auto simp add: complex_mult complex_mod real_sqrt_mult_distrib2 [symmetric] simp del: realpow_Suc)
   2.234 -apply (rule_tac n = 1 in realpow_Suc_cancel_eq)
   2.235 +apply (rule_tac n = 1 in power_inject_base)
   2.236  apply (auto simp add: real_power_two [symmetric] simp del: realpow_Suc)
   2.237  apply (auto simp add: real_diff_def real_power_two right_distrib left_distrib add_ac mult_ac)
   2.238  done
   2.239 @@ -1087,7 +967,7 @@
   2.240  lemma complex_inverse_divide:
   2.241        "inverse(x/y) = y/(x::complex)"
   2.242  apply (unfold complex_divide_def)
   2.243 -apply (auto simp add: complex_inverse_distrib complex_mult_commute)
   2.244 +apply (auto simp add: inverse_mult_distrib complex_mult_commute)
   2.245  done
   2.246  declare complex_inverse_divide [simp]
   2.247  
   2.248 @@ -1105,7 +985,7 @@
   2.249  
   2.250  lemma complexpow_not_zero [rule_format (no_asm)]: "r ~= (0::complex) --> r ^ n ~= 0"
   2.251  apply (induct_tac "n")
   2.252 -apply (auto simp add: complex_mult_not_zero)
   2.253 +apply (auto simp add: )
   2.254  done
   2.255  declare complexpow_not_zero [simp]
   2.256  declare complexpow_not_zero [intro]
   2.257 @@ -1135,7 +1015,7 @@
   2.258  
   2.259  lemma complexpow_inverse: "inverse ((r::complex) ^ n) = (inverse r) ^ n"
   2.260  apply (induct_tac "n")
   2.261 -apply (auto simp add: complex_inverse_distrib)
   2.262 +apply (auto simp add: inverse_mult_distrib)
   2.263  done
   2.264  
   2.265  (*---------------------------------------------------------------------------*)
   2.266 @@ -1383,21 +1263,22 @@
   2.267  by (unfold rcis_def cis_def, auto)
   2.268  declare Re_rcis [simp]
   2.269  
   2.270 -lemma Im_complex_polar: "Im(complex_of_real r *
   2.271 -      (complex_of_real(cos a) + ii * complex_of_real(sin a))) = r * sin a"
   2.272 -apply (auto simp add: complex_add_mult_distrib2 complex_of_real_mult complex_mult_ac)
   2.273 -done
   2.274 -declare Im_complex_polar [simp]
   2.275 +lemma Im_complex_polar [simp]:
   2.276 +     "Im(complex_of_real r * 
   2.277 +         (complex_of_real(cos a) + ii * complex_of_real(sin a))) = 
   2.278 +      r * sin a"
   2.279 +by (auto simp add: complex_add_mult_distrib2 complex_of_real_mult mult_ac)
   2.280  
   2.281 -lemma Im_rcis: "Im(rcis r a) = r * sin a"
   2.282 +lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a"
   2.283  by (unfold rcis_def cis_def, auto)
   2.284 -declare Im_rcis [simp]
   2.285  
   2.286 -lemma complex_mod_complex_polar: "cmod (complex_of_real r *
   2.287 -      (complex_of_real(cos a) + ii * complex_of_real(sin a))) = abs r"
   2.288 -apply (auto simp add: complex_add_mult_distrib2 cmod_i complex_of_real_mult right_distrib [symmetric] realpow_mult complex_mult_ac mult_ac simp del: realpow_Suc)
   2.289 -done
   2.290 -declare complex_mod_complex_polar [simp]
   2.291 +lemma complex_mod_complex_polar [simp]:
   2.292 +     "cmod (complex_of_real r * 
   2.293 +            (complex_of_real(cos a) + ii * complex_of_real(sin a))) = 
   2.294 +      abs r"
   2.295 +by (auto simp add: complex_add_mult_distrib2 cmod_i complex_of_real_mult
   2.296 +                      right_distrib [symmetric] power_mult_distrib mult_ac 
   2.297 +         simp del: realpow_Suc)
   2.298  
   2.299  lemma complex_mod_rcis: "cmod(rcis r a) = abs r"
   2.300  by (unfold rcis_def cis_def, auto)
   2.301 @@ -1728,9 +1609,6 @@
   2.302  val complex_divide_zero = thm"complex_divide_zero";
   2.303  val complex_minus_mult_eq1 = thm"complex_minus_mult_eq1";
   2.304  val complex_minus_mult_eq2 = thm"complex_minus_mult_eq2";
   2.305 -val complex_mult_minus_one = thm"complex_mult_minus_one";
   2.306 -val complex_mult_minus_one_right = thm"complex_mult_minus_one_right";
   2.307 -val complex_minus_mult_cancel = thm"complex_minus_mult_cancel";
   2.308  val complex_minus_mult_commute = thm"complex_minus_mult_commute";
   2.309  val complex_add_mult_distrib = thm"complex_add_mult_distrib";
   2.310  val complex_add_mult_distrib2 = thm"complex_add_mult_distrib2";
   2.311 @@ -1740,21 +1618,6 @@
   2.312  val COMPLEX_DIVISION_BY_ZERO = thm"COMPLEX_DIVISION_BY_ZERO";
   2.313  val complex_mult_inv_left = thm"complex_mult_inv_left";
   2.314  val complex_mult_inv_right = thm"complex_mult_inv_right";
   2.315 -val complex_mult_left_cancel = thm"complex_mult_left_cancel";
   2.316 -val complex_mult_right_cancel = thm"complex_mult_right_cancel";
   2.317 -val complex_inverse_not_zero = thm"complex_inverse_not_zero";
   2.318 -val complex_mult_not_zero = thm"complex_mult_not_zero";
   2.319 -val complex_inverse_inverse = thm"complex_inverse_inverse";
   2.320 -val complex_inverse_one = thm"complex_inverse_one";
   2.321 -val complex_minus_inverse = thm"complex_minus_inverse";
   2.322 -val complex_inverse_distrib = thm"complex_inverse_distrib";
   2.323 -val complex_times_divide1_eq = thm"complex_times_divide1_eq";
   2.324 -val complex_times_divide2_eq = thm"complex_times_divide2_eq";
   2.325 -val complex_divide_divide1_eq = thm"complex_divide_divide1_eq";
   2.326 -val complex_divide_divide2_eq = thm"complex_divide_divide2_eq";
   2.327 -val complex_minus_divide_eq = thm"complex_minus_divide_eq";
   2.328 -val complex_divide_minus_eq = thm"complex_divide_minus_eq";
   2.329 -val complex_add_divide_distrib = thm"complex_add_divide_distrib";
   2.330  val inj_complex_of_real = thm"inj_complex_of_real";
   2.331  val complex_of_real_one = thm"complex_of_real_one";
   2.332  val complex_of_real_zero = thm"complex_of_real_zero";
   2.333 @@ -1790,7 +1653,6 @@
   2.334  val complex_cnj_zero = thm"complex_cnj_zero";
   2.335  val complex_cnj_zero_iff = thm"complex_cnj_zero_iff";
   2.336  val complex_mult_cnj = thm"complex_mult_cnj";
   2.337 -val complex_mult_zero_iff = thm"complex_mult_zero_iff";
   2.338  val complex_add_left_cancel_zero = thm"complex_add_left_cancel_zero";
   2.339  val complex_diff_mult_distrib = thm"complex_diff_mult_distrib";
   2.340  val complex_diff_mult_distrib2 = thm"complex_diff_mult_distrib2";
     3.1 --- a/src/HOL/Complex/ComplexArith0.ML	Fri Jan 09 01:28:24 2004 +0100
     3.2 +++ b/src/HOL/Complex/ComplexArith0.ML	Fri Jan 09 10:46:18 2004 +0100
     3.3 @@ -168,7 +168,7 @@
     3.4  Addsimps [complex_divide_minus1];
     3.5  
     3.6  Goal "-1/(x::complex) = - (1/x)";
     3.7 -by (simp_tac (simpset() addsimps [complex_divide_def, complex_minus_inverse]) 1); 
     3.8 +by (simp_tac (simpset() addsimps [complex_divide_def, inverse_minus_eq]) 1); 
     3.9  qed "complex_minus1_divide";
    3.10  Addsimps [complex_minus1_divide];
    3.11  
     4.1 --- a/src/HOL/Hyperreal/HTranscendental.ML	Fri Jan 09 01:28:24 2004 +0100
     4.2 +++ b/src/HOL/Hyperreal/HTranscendental.ML	Fri Jan 09 10:46:18 2004 +0100
     4.3 @@ -4,6 +4,8 @@
     4.4      Description : Nonstandard extensions of transcendental functions
     4.5  *)
     4.6  
     4.7 +val hpowr_Suc= thm"hpowr_Suc";
     4.8 +
     4.9  (*-------------------------------------------------------------------------*)
    4.10  (* NS extension of square root function                                    *)
    4.11  (*-------------------------------------------------------------------------*)
    4.12 @@ -44,8 +46,7 @@
    4.13  qed "hypreal_sqrt_not_zero";
    4.14  
    4.15  Goal "0 < x ==> inverse (( *f* sqrt)(x)) ^ 2 = inverse x";
    4.16 -by (forward_tac [hypreal_sqrt_not_zero] 1);
    4.17 -by (dres_inst_tac [("n1","2"),("r1","( *f* sqrt) x")] (hrealpow_inverse RS sym) 1);
    4.18 +by (cut_inst_tac [("n1","2"),("a1","( *f* sqrt) x")] (power_inverse RS sym) 1);
    4.19  by (auto_tac (claset() addDs [hypreal_sqrt_gt_zero_pow2],simpset()));
    4.20  qed "hypreal_inverse_sqrt_pow2";
    4.21  
    4.22 @@ -81,14 +82,14 @@
    4.23  Goal "(( *f* sqrt)(x*x + y*y + z*z) @= 0) = (x*x + y*y + z*z @= 0)";
    4.24  by (rtac hypreal_sqrt_approx_zero2 1);
    4.25  by (REPEAT(rtac hypreal_le_add_order 1));
    4.26 -by Auto_tac;
    4.27 +by (auto_tac (claset(), simpset() addsimps [zero_le_square]));
    4.28  qed "hypreal_sqrt_sum_squares";
    4.29  Addsimps [hypreal_sqrt_sum_squares];
    4.30  
    4.31  Goal  "(( *f* sqrt)(x*x + y*y) @= 0) = (x*x + y*y @= 0)";
    4.32  by (rtac hypreal_sqrt_approx_zero2 1);
    4.33  by (rtac hypreal_le_add_order 1);
    4.34 -by Auto_tac;
    4.35 +by (auto_tac (claset(), simpset() addsimps [zero_le_square]));
    4.36  qed "hypreal_sqrt_sum_squares2";
    4.37  Addsimps [hypreal_sqrt_sum_squares2];
    4.38  
    4.39 @@ -126,15 +127,15 @@
    4.40  Addsimps [hypreal_sqrt_hyperpow_hrabs];
    4.41  
    4.42  Goal "[| x: HFinite; 0 <= x |] ==> st(( *f* sqrt) x) = ( *f* sqrt)(st x)";
    4.43 -by (res_inst_tac [("n","1")] hrealpow_Suc_cancel_eq 1);
    4.44 +by (res_inst_tac [("n","1")] power_inject_base 1);
    4.45  by (auto_tac (claset() addSIs [st_zero_le,hypreal_sqrt_ge_zero],simpset()));
    4.46 -by (rtac (st_mult RS subst) 2);
    4.47 -by (rtac (hypreal_sqrt_mult_distrib2 RS subst) 4);
    4.48 -by (rtac (hypreal_sqrt_mult_distrib2 RS subst) 6);
    4.49 +by (rtac (st_mult RS subst) 1);
    4.50 +by (rtac (hypreal_sqrt_mult_distrib2 RS subst) 3);
    4.51 +by (rtac (hypreal_sqrt_mult_distrib2 RS subst) 5);
    4.52  by (auto_tac (claset(), simpset() addsimps [st_hrabs,st_zero_le]));
    4.53  by (ALLGOALS(rtac (HFinite_square_iff RS iffD1)));
    4.54 -by (auto_tac (claset(),simpset() addsimps 
    4.55 -    [hypreal_sqrt_mult_distrib2 RS sym] 
    4.56 +by (auto_tac (claset(),
    4.57 +     simpset() addsimps [hypreal_sqrt_mult_distrib2 RS sym] 
    4.58      delsimps [HFinite_square_iff]));
    4.59  qed "st_hypreal_sqrt";
    4.60  
    4.61 @@ -169,7 +170,7 @@
    4.62  Goal  "(( *f* sqrt)(x*x + y*y) : HFinite) = (x*x + y*y : HFinite)";
    4.63  by (rtac HFinite_hypreal_sqrt_iff 1);
    4.64  by (rtac  hypreal_le_add_order 1);
    4.65 -by Auto_tac;
    4.66 +by (auto_tac (claset(), simpset() addsimps [zero_le_square]));
    4.67  qed "HFinite_sqrt_sum_squares";
    4.68  Addsimps [HFinite_sqrt_sum_squares];
    4.69  
    4.70 @@ -197,7 +198,7 @@
    4.71  Goal  "(( *f* sqrt)(x*x + y*y) : Infinitesimal) = (x*x + y*y : Infinitesimal)";
    4.72  by (rtac Infinitesimal_hypreal_sqrt_iff 1);
    4.73  by (rtac hypreal_le_add_order 1);
    4.74 -by Auto_tac;
    4.75 +by (auto_tac (claset(), simpset() addsimps [zero_le_square]));
    4.76  qed "Infinitesimal_sqrt_sum_squares";
    4.77  Addsimps [Infinitesimal_sqrt_sum_squares];
    4.78  
    4.79 @@ -225,7 +226,7 @@
    4.80  Goal  "(( *f* sqrt)(x*x + y*y) : HInfinite) = (x*x + y*y : HInfinite)";
    4.81  by (rtac HInfinite_hypreal_sqrt_iff 1);
    4.82  by (rtac hypreal_le_add_order 1);
    4.83 -by Auto_tac;
    4.84 +by (auto_tac (claset(), simpset() addsimps [zero_le_square]));
    4.85  qed "HInfinite_sqrt_sum_squares";
    4.86  Addsimps [HInfinite_sqrt_sum_squares];
    4.87  
     5.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Fri Jan 09 01:28:24 2004 +0100
     5.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Fri Jan 09 10:46:18 2004 +0100
     5.3 @@ -697,8 +697,12 @@
     5.4  instance hypreal :: ordered_field
     5.5  proof
     5.6    fix x y z :: hypreal
     5.7 -  show "x \<le> y ==> z + x \<le> z + y" by (rule hypreal_add_left_le_mono1)
     5.8 -  show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: hypreal_mult_less_mono2)
     5.9 +  show "0 < (1::hypreal)" 
    5.10 +    by (unfold hypreal_one_def hypreal_zero_def hypreal_less_def, force)
    5.11 +  show "x \<le> y ==> z + x \<le> z + y" 
    5.12 +    by (rule hypreal_add_left_le_mono1)
    5.13 +  show "x < y ==> 0 < z ==> z * x < z * y" 
    5.14 +    by (simp add: hypreal_mult_less_mono2)
    5.15    show "\<bar>x\<bar> = (if x < 0 then -x else x)"
    5.16      by (auto dest: order_le_less_trans simp add: hrabs_def linorder_not_le)
    5.17  qed
     6.1 --- a/src/HOL/Hyperreal/HyperPow.ML	Fri Jan 09 01:28:24 2004 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,547 +0,0 @@
     6.4 -(*  Title       : HyperPow.ML
     6.5 -    Author      : Jacques D. Fleuriot  
     6.6 -    Copyright   : 1998  University of Cambridge
     6.7 -    Description : Natural Powers of hyperreals theory
     6.8 -
     6.9 -Exponentials on the hyperreals
    6.10 -*)
    6.11 -
    6.12 -Goal "(0::hypreal) ^ (Suc n) = 0";
    6.13 -by Auto_tac;
    6.14 -qed "hrealpow_zero";
    6.15 -Addsimps [hrealpow_zero];
    6.16 -
    6.17 -Goal "r ~= (0::hypreal) --> r ^ n ~= 0";
    6.18 -by (induct_tac "n" 1);
    6.19 -by Auto_tac;
    6.20 -qed_spec_mp "hrealpow_not_zero";
    6.21 -
    6.22 -Goal "r ~= (0::hypreal) --> inverse(r ^ n) = (inverse r) ^ n";
    6.23 -by (induct_tac "n" 1);
    6.24 -by Auto_tac;
    6.25 -qed_spec_mp "hrealpow_inverse";
    6.26 -
    6.27 -Goal "abs (r::hypreal) ^ n = abs (r ^ n)";
    6.28 -by (induct_tac "n" 1);
    6.29 -by Auto_tac;
    6.30 -qed "hrealpow_hrabs";
    6.31 -
    6.32 -Goal "(r::hypreal) ^ (n + m) = (r ^ n) * (r ^ m)";
    6.33 -by (induct_tac "n" 1);
    6.34 -by (auto_tac (claset(), simpset() addsimps mult_ac));
    6.35 -qed "hrealpow_add";
    6.36 -
    6.37 -Goal "(r::hypreal) ^ Suc 0 = r";
    6.38 -by (Simp_tac 1);
    6.39 -qed "hrealpow_one";
    6.40 -Addsimps [hrealpow_one];
    6.41 -
    6.42 -Goal "(r::hypreal) ^ Suc (Suc 0) = r * r";
    6.43 -by (Simp_tac 1);
    6.44 -qed "hrealpow_two";
    6.45 -
    6.46 -Goal "(0::hypreal) <= r --> 0 <= r ^ n";
    6.47 -by (induct_tac "n" 1);
    6.48 -by (auto_tac (claset(), simpset() addsimps [zero_le_mult_iff]));
    6.49 -qed_spec_mp "hrealpow_ge_zero";
    6.50 -
    6.51 -Goal "(0::hypreal) < r --> 0 < r ^ n";
    6.52 -by (induct_tac "n" 1);
    6.53 -by (auto_tac (claset(), simpset() addsimps [zero_less_mult_iff]));
    6.54 -qed_spec_mp "hrealpow_gt_zero";
    6.55 -
    6.56 -Goal "x <= y & (0::hypreal) < x --> x ^ n <= y ^ n";
    6.57 -by (induct_tac "n" 1);
    6.58 -by (auto_tac (claset() addSIs [mult_mono], simpset()));
    6.59 -by (asm_simp_tac (simpset() addsimps [hrealpow_ge_zero]) 1);
    6.60 -qed_spec_mp "hrealpow_le";
    6.61 -
    6.62 -Goal "x < y & (0::hypreal) < x & 0 < n --> x ^ n < y ^ n";
    6.63 -by (induct_tac "n" 1);
    6.64 -by (auto_tac (claset() addIs [hypreal_mult_less_mono,gr0I],
    6.65 -              simpset() addsimps [hrealpow_gt_zero]));
    6.66 -qed "hrealpow_less";
    6.67 -
    6.68 -Goal "1 ^ n = (1::hypreal)";
    6.69 -by (induct_tac "n" 1);
    6.70 -by Auto_tac;
    6.71 -qed "hrealpow_eq_one";
    6.72 -Addsimps [hrealpow_eq_one];
    6.73 -
    6.74 -Goal "abs(-(1 ^ n)) = (1::hypreal)";
    6.75 -by Auto_tac;  
    6.76 -qed "hrabs_minus_hrealpow_one";
    6.77 -Addsimps [hrabs_minus_hrealpow_one];
    6.78 -
    6.79 -Goal "abs(-1 ^ n) = (1::hypreal)";
    6.80 -by (induct_tac "n" 1);
    6.81 -by Auto_tac;  
    6.82 -qed "hrabs_hrealpow_minus_one";
    6.83 -Addsimps [hrabs_hrealpow_minus_one];
    6.84 -
    6.85 -Goal "((r::hypreal) * s) ^ n = (r ^ n) * (s ^ n)";
    6.86 -by (induct_tac "n" 1);
    6.87 -by (auto_tac (claset(), simpset() addsimps mult_ac));
    6.88 -qed "hrealpow_mult";
    6.89 -
    6.90 -Goal "(0::hypreal) <= r ^ Suc (Suc 0)";
    6.91 -by (auto_tac (claset(), simpset() addsimps [zero_le_mult_iff]));
    6.92 -qed "hrealpow_two_le";
    6.93 -Addsimps [hrealpow_two_le];
    6.94 -
    6.95 -Goal "(0::hypreal) <= u ^ Suc (Suc 0) + v ^ Suc (Suc 0)";
    6.96 -by (simp_tac (HOL_ss addsimps [hrealpow_two_le, hypreal_le_add_order]) 1); 
    6.97 -qed "hrealpow_two_le_add_order";
    6.98 -Addsimps [hrealpow_two_le_add_order];
    6.99 -
   6.100 -Goal "(0::hypreal) <= u ^ Suc (Suc 0) + v ^ Suc (Suc 0) + w ^ Suc (Suc 0)";
   6.101 -by (simp_tac (HOL_ss addsimps [hrealpow_two_le, hypreal_le_add_order]) 1); 
   6.102 -qed "hrealpow_two_le_add_order2";
   6.103 -Addsimps [hrealpow_two_le_add_order2];
   6.104 -
   6.105 -Goal "[| 0 <= x; 0 <= y |] ==> (x+y = 0) = (x = 0 & y = (0::hypreal))";
   6.106 -by (auto_tac (claset() addIs [order_antisym], simpset()));
   6.107 -qed "hypreal_add_nonneg_eq_0_iff";
   6.108 -
   6.109 -Goal "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))";
   6.110 -by (simp_tac (HOL_ss addsimps [zero_le_square, hypreal_le_add_order, 
   6.111 -                         hypreal_add_nonneg_eq_0_iff]) 1);
   6.112 -by Auto_tac;
   6.113 -qed "hypreal_three_squares_add_zero_iff";
   6.114 -
   6.115 -Goal "(x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = (0::hypreal)) = (x = 0 & y = 0 & z = 0)";
   6.116 -by (simp_tac (HOL_ss addsimps
   6.117 -               [hypreal_three_squares_add_zero_iff, hrealpow_two]) 1);
   6.118 -qed "hrealpow_three_squares_add_zero_iff";
   6.119 -Addsimps [hrealpow_three_squares_add_zero_iff];
   6.120 -
   6.121 -Goal "abs(x ^ Suc (Suc 0)) = (x::hypreal) ^ Suc (Suc 0)";
   6.122 -by (auto_tac (claset(), 
   6.123 -              simpset() addsimps [hrabs_def, zero_le_mult_iff])); 
   6.124 -qed "hrabs_hrealpow_two";
   6.125 -Addsimps [hrabs_hrealpow_two];
   6.126 -
   6.127 -Goal "abs(x) ^ Suc (Suc 0) = (x::hypreal) ^ Suc (Suc 0)";
   6.128 -by (simp_tac (simpset() addsimps [hrealpow_hrabs, hrabs_eqI1] 
   6.129 -                        delsimps [hpowr_Suc]) 1);
   6.130 -qed "hrealpow_two_hrabs";
   6.131 -Addsimps [hrealpow_two_hrabs];
   6.132 -
   6.133 -Goal "(1::hypreal) < r ==> 1 < r ^ Suc (Suc 0)";
   6.134 -by (auto_tac (claset(), simpset() addsimps [hrealpow_two]));
   6.135 -by (res_inst_tac [("y","1*1")] order_le_less_trans 1); 
   6.136 -by (rtac hypreal_mult_less_mono 2); 
   6.137 -by Auto_tac;  
   6.138 -qed "hrealpow_two_gt_one";
   6.139 -
   6.140 -Goal "(1::hypreal) <= r ==> 1 <= r ^ Suc (Suc 0)";
   6.141 -by (etac (order_le_imp_less_or_eq RS disjE) 1);
   6.142 -by (etac (hrealpow_two_gt_one RS order_less_imp_le) 1);
   6.143 -by Auto_tac;  
   6.144 -qed "hrealpow_two_ge_one";
   6.145 -
   6.146 -Goal "(1::hypreal) <= 2 ^ n";
   6.147 -by (res_inst_tac [("y","1 ^ n")] order_trans 1);
   6.148 -by (rtac hrealpow_le 2);
   6.149 -by Auto_tac;
   6.150 -qed "two_hrealpow_ge_one";
   6.151 -
   6.152 -Goal "hypreal_of_nat n < 2 ^ n";
   6.153 -by (induct_tac "n" 1);
   6.154 -by (auto_tac (claset(),
   6.155 -        simpset() addsimps [hypreal_of_nat_Suc, left_distrib]));
   6.156 -by (cut_inst_tac [("n","n")] two_hrealpow_ge_one 1);
   6.157 -by (arith_tac 1);
   6.158 -qed "two_hrealpow_gt";
   6.159 -Addsimps [two_hrealpow_gt,two_hrealpow_ge_one];
   6.160 -
   6.161 -Goal "-1 ^ (2*n) = (1::hypreal)";
   6.162 -by (induct_tac "n" 1);
   6.163 -by Auto_tac;
   6.164 -qed "hrealpow_minus_one";
   6.165 -
   6.166 -Goal "n+n = (2*n::nat)";
   6.167 -by Auto_tac; 
   6.168 -qed "double_lemma";
   6.169 -
   6.170 -(*ugh: need to get rid fo the n+n*)
   6.171 -Goal "-1 ^ (n + n) = (1::hypreal)";
   6.172 -by (auto_tac (claset(), 
   6.173 -              simpset() addsimps [double_lemma, hrealpow_minus_one]));
   6.174 -qed "hrealpow_minus_one2";
   6.175 -Addsimps [hrealpow_minus_one2];
   6.176 -
   6.177 -Goal "(-(x::hypreal)) ^ Suc (Suc 0) = x ^ Suc (Suc 0)";
   6.178 -by Auto_tac;
   6.179 -qed "hrealpow_minus_two";
   6.180 -Addsimps [hrealpow_minus_two];
   6.181 -
   6.182 -Goal "(0::hypreal) < r & r < 1 --> r ^ Suc n < r ^ n";
   6.183 -by (induct_tac "n" 1);
   6.184 -by (auto_tac (claset(),
   6.185 -              simpset() addsimps [hypreal_mult_less_mono2]));
   6.186 -qed_spec_mp "hrealpow_Suc_less";
   6.187 -
   6.188 -Goal "(0::hypreal) <= r & r < 1 --> r ^ Suc n <= r ^ n";
   6.189 -by (induct_tac "n" 1);
   6.190 -by (auto_tac (claset() addIs [order_less_imp_le]
   6.191 -                       addSDs [order_le_imp_less_or_eq,hrealpow_Suc_less],
   6.192 -              simpset() addsimps [hypreal_mult_less_mono2]));
   6.193 -qed_spec_mp "hrealpow_Suc_le";
   6.194 -
   6.195 -Goal "Abs_hypreal(hyprel``{%n. X n}) ^ m = Abs_hypreal(hyprel``{%n. (X n) ^ m})";
   6.196 -by (induct_tac "m" 1);
   6.197 -by (auto_tac (claset(),
   6.198 -              simpset() addsimps [hypreal_one_def, hypreal_mult]));
   6.199 -qed "hrealpow";
   6.200 -
   6.201 -Goal "(x + (y::hypreal)) ^ Suc (Suc 0) = \
   6.202 -\     x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0)))*x*y";
   6.203 -by (simp_tac (simpset() addsimps
   6.204 -              [right_distrib, left_distrib, 
   6.205 -               hypreal_of_nat_zero, hypreal_of_nat_Suc]) 1);
   6.206 -qed "hrealpow_sum_square_expand";
   6.207 -
   6.208 -
   6.209 -(*** Literal arithmetic involving powers, type hypreal ***)
   6.210 -
   6.211 -Goal "hypreal_of_real (x ^ n) = hypreal_of_real x ^ n";
   6.212 -by (induct_tac "n" 1); 
   6.213 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [nat_mult_distrib])));
   6.214 -qed "hypreal_of_real_power";
   6.215 -Addsimps [hypreal_of_real_power];
   6.216 -
   6.217 -Goal "(number_of v :: hypreal) ^ n = hypreal_of_real ((number_of v) ^ n)";
   6.218 -by (simp_tac (HOL_ss addsimps [hypreal_number_of_def, 
   6.219 -                               hypreal_of_real_power]) 1);
   6.220 -qed "power_hypreal_of_real_number_of";
   6.221 -
   6.222 -Addsimps [inst "n" "number_of ?w" power_hypreal_of_real_number_of];
   6.223 -
   6.224 -(*---------------------------------------------------------------
   6.225 -   we'll prove the following theorem by going down to the
   6.226 -   level of the ultrafilter and relying on the analogous
   6.227 -   property for the real rather than prove it directly 
   6.228 -   using induction: proof is much simpler this way!
   6.229 - ---------------------------------------------------------------*)
   6.230 -Goal "[|(0::hypreal) <= x; 0 <= y;x ^ Suc n <= y ^ Suc n |] ==> x <= y";
   6.231 -by (full_simp_tac (simpset() addsimps [hypreal_zero_def]) 1);
   6.232 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   6.233 -by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   6.234 -by (auto_tac (claset(),
   6.235 -              simpset() addsimps [hrealpow,hypreal_le,hypreal_mult]));
   6.236 -by (ultra_tac (claset() addIs [realpow_increasing], simpset()) 1);
   6.237 -qed "hrealpow_increasing";
   6.238 -
   6.239 -(*By antisymmetry with the above we conclude x=y, replacing the deleted 
   6.240 -  theorem hrealpow_Suc_cancel_eq*)
   6.241 -
   6.242 -Goal "x : HFinite --> x ^ n : HFinite";
   6.243 -by (induct_tac "n" 1);
   6.244 -by (auto_tac (claset() addIs [HFinite_mult], simpset()));
   6.245 -qed_spec_mp "hrealpow_HFinite";
   6.246 -
   6.247 -(*---------------------------------------------------------------
   6.248 -                  Hypernaturals Powers
   6.249 - --------------------------------------------------------------*)
   6.250 -Goalw [congruent_def]
   6.251 -     "congruent hyprel \
   6.252 -\    (%X Y. hyprel``{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})";
   6.253 -by (auto_tac (claset() addSIs [ext], simpset()));
   6.254 -by (ALLGOALS(Fuf_tac));
   6.255 -qed "hyperpow_congruent";
   6.256 -
   6.257 -Goalw [hyperpow_def]
   6.258 -  "Abs_hypreal(hyprel``{%n. X n}) pow Abs_hypnat(hypnatrel``{%n. Y n}) = \
   6.259 -\  Abs_hypreal(hyprel``{%n. X n ^ Y n})";
   6.260 -by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
   6.261 -by (auto_tac (claset() addSIs [lemma_hyprel_refl,bexI],
   6.262 -    simpset() addsimps [hyprel_in_hypreal RS 
   6.263 -    Abs_hypreal_inverse,equiv_hyprel,hyperpow_congruent]));
   6.264 -by (Fuf_tac 1);
   6.265 -qed "hyperpow";
   6.266 -
   6.267 -Goalw [hypnat_one_def] "(0::hypreal) pow (n + (1::hypnat)) = 0";
   6.268 -by (simp_tac (simpset() addsimps [hypreal_zero_def]) 1);
   6.269 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   6.270 -by (auto_tac (claset(), simpset() addsimps [hyperpow,hypnat_add]));
   6.271 -qed "hyperpow_zero";
   6.272 -Addsimps [hyperpow_zero];
   6.273 -
   6.274 -Goal "r ~= (0::hypreal) --> r pow n ~= 0";
   6.275 -by (simp_tac (simpset() addsimps [hypreal_zero_def]) 1);
   6.276 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   6.277 -by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   6.278 -by (auto_tac (claset(), simpset() addsimps [hyperpow]));
   6.279 -by (dtac FreeUltrafilterNat_Compl_mem 1);
   6.280 -by (fuf_empty_tac (claset() addIs [realpow_not_zero RS notE],
   6.281 -    simpset()) 1);
   6.282 -qed_spec_mp "hyperpow_not_zero";
   6.283 -
   6.284 -Goal "r ~= (0::hypreal) --> inverse(r pow n) = (inverse r) pow n";
   6.285 -by (simp_tac (simpset() addsimps [hypreal_zero_def]) 1);
   6.286 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   6.287 -by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   6.288 -by (auto_tac (claset() addSDs [FreeUltrafilterNat_Compl_mem],
   6.289 -              simpset() addsimps [hypreal_inverse,hyperpow]));
   6.290 -by (rtac FreeUltrafilterNat_subset 1);
   6.291 -by (auto_tac (claset() addDs [realpow_not_zero] 
   6.292 -                       addIs [realpow_inverse], 
   6.293 -              simpset()));
   6.294 -qed "hyperpow_inverse";
   6.295 -
   6.296 -Goal "abs r pow n = abs (r pow n)";
   6.297 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   6.298 -by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   6.299 -by (auto_tac (claset(),
   6.300 -              simpset() addsimps [hypreal_hrabs, hyperpow,realpow_abs RS sym]));
   6.301 -qed "hyperpow_hrabs";
   6.302 -
   6.303 -Goal "r pow (n + m) = (r pow n) * (r pow m)";
   6.304 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   6.305 -by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
   6.306 -by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   6.307 -by (auto_tac (claset(),
   6.308 -          simpset() addsimps [hyperpow,hypnat_add, hypreal_mult,realpow_add]));
   6.309 -qed "hyperpow_add";
   6.310 -
   6.311 -Goalw [hypnat_one_def] "r pow (1::hypnat) = r";
   6.312 -by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   6.313 -by (auto_tac (claset(), simpset() addsimps [hyperpow]));
   6.314 -qed "hyperpow_one";
   6.315 -Addsimps [hyperpow_one];
   6.316 -
   6.317 -Goalw [hypnat_one_def] 
   6.318 -     "r pow ((1::hypnat) + (1::hypnat)) = r * r";
   6.319 -by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   6.320 -by (auto_tac (claset(),
   6.321 -              simpset() addsimps [hyperpow,hypnat_add, hypreal_mult]));
   6.322 -qed "hyperpow_two";
   6.323 -
   6.324 -Goal "(0::hypreal) < r --> 0 < r pow n";
   6.325 -by (simp_tac (simpset() addsimps [hypreal_zero_def]) 1);
   6.326 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   6.327 -by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   6.328 -by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset, realpow_gt_zero],
   6.329 -              simpset() addsimps [hyperpow,hypreal_less, hypreal_le]));
   6.330 -qed_spec_mp "hyperpow_gt_zero";
   6.331 -
   6.332 -Goal "(0::hypreal) <= r --> 0 <= r pow n";
   6.333 -by (simp_tac (simpset() addsimps [hypreal_zero_def]) 1);
   6.334 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   6.335 -by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   6.336 -by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset, realpow_ge_zero],
   6.337 -              simpset() addsimps [hyperpow,hypreal_le]));
   6.338 -qed "hyperpow_ge_zero";
   6.339 -
   6.340 -Goal "(0::hypreal) < x & x <= y --> x pow n <= y pow n";
   6.341 -by (full_simp_tac (simpset() addsimps [hypreal_zero_def]) 1);
   6.342 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   6.343 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   6.344 -by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   6.345 -by (auto_tac (claset(),
   6.346 -              simpset() addsimps [hyperpow,hypreal_le,hypreal_less]));
   6.347 -by (etac (FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset) 1
   6.348 -    THEN assume_tac 1);
   6.349 -by (auto_tac (claset() addIs [realpow_le], simpset()));
   6.350 -qed_spec_mp "hyperpow_le";
   6.351 -
   6.352 -Goal "1 pow n = (1::hypreal)";
   6.353 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   6.354 -by (auto_tac (claset(), simpset() addsimps [hypreal_one_def, hyperpow]));
   6.355 -qed "hyperpow_eq_one";
   6.356 -Addsimps [hyperpow_eq_one];
   6.357 -
   6.358 -Goal "abs(-(1 pow n)) = (1::hypreal)";
   6.359 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   6.360 -by (auto_tac (claset(), 
   6.361 -              simpset() addsimps [hyperpow, hypreal_hrabs, hypreal_one_def]));
   6.362 -qed "hrabs_minus_hyperpow_one";
   6.363 -Addsimps [hrabs_minus_hyperpow_one];
   6.364 -
   6.365 -Goal "abs(-1 pow n) = (1::hypreal)";
   6.366 -by (subgoal_tac "abs((- (1::hypreal)) pow n) = (1::hypreal)" 1);
   6.367 -by (Asm_full_simp_tac 1); 
   6.368 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   6.369 -by (auto_tac (claset(),
   6.370 -              simpset() addsimps [hypreal_one_def, hyperpow,hypreal_minus,
   6.371 -                                  hypreal_hrabs]));
   6.372 -qed "hrabs_hyperpow_minus_one";
   6.373 -Addsimps [hrabs_hyperpow_minus_one];
   6.374 -
   6.375 -Goal "(r * s) pow n = (r pow n) * (s pow n)";
   6.376 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   6.377 -by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   6.378 -by (res_inst_tac [("z","s")] eq_Abs_hypreal 1);
   6.379 -by (auto_tac (claset(),
   6.380 -       simpset() addsimps [hyperpow, hypreal_mult,realpow_mult]));
   6.381 -qed "hyperpow_mult";
   6.382 -
   6.383 -Goal "(0::hypreal) <= r pow ((1::hypnat) + (1::hypnat))";
   6.384 -by (auto_tac (claset(), 
   6.385 -              simpset() addsimps [hyperpow_two, zero_le_mult_iff]));
   6.386 -qed "hyperpow_two_le";
   6.387 -Addsimps [hyperpow_two_le];
   6.388 -
   6.389 -Goal "abs(x pow ((1::hypnat) + (1::hypnat))) = x pow ((1::hypnat) + (1::hypnat))";
   6.390 -by (simp_tac (simpset() addsimps [hrabs_eqI1]) 1);
   6.391 -qed "hrabs_hyperpow_two";
   6.392 -Addsimps [hrabs_hyperpow_two];
   6.393 -
   6.394 -Goal "abs(x) pow ((1::hypnat) + (1::hypnat))  = x pow ((1::hypnat) + (1::hypnat))";
   6.395 -by (simp_tac (simpset() addsimps [hyperpow_hrabs,hrabs_eqI1]) 1);
   6.396 -qed "hyperpow_two_hrabs";
   6.397 -Addsimps [hyperpow_two_hrabs];
   6.398 -
   6.399 -(*? very similar to hrealpow_two_gt_one *)
   6.400 -Goal "(1::hypreal) < r ==> 1 < r pow ((1::hypnat) + (1::hypnat))";
   6.401 -by (auto_tac (claset(), simpset() addsimps [hyperpow_two]));
   6.402 -by (res_inst_tac [("y","1*1")] order_le_less_trans 1); 
   6.403 -by (rtac hypreal_mult_less_mono 2); 
   6.404 -by Auto_tac;  
   6.405 -qed "hyperpow_two_gt_one";
   6.406 -
   6.407 -Goal "(1::hypreal) <= r ==> 1 <= r pow ((1::hypnat) + (1::hypnat))";
   6.408 -by (auto_tac (claset() addSDs [order_le_imp_less_or_eq] 
   6.409 -                       addIs [hyperpow_two_gt_one,order_less_imp_le],
   6.410 -              simpset()));
   6.411 -qed "hyperpow_two_ge_one";
   6.412 -
   6.413 -Goal "(1::hypreal) <= 2 pow n";
   6.414 -by (res_inst_tac [("y","1 pow n")] order_trans 1);
   6.415 -by (rtac hyperpow_le 2);
   6.416 -by Auto_tac;
   6.417 -qed "two_hyperpow_ge_one";
   6.418 -Addsimps [two_hyperpow_ge_one];
   6.419 -
   6.420 -Addsimps [simplify (simpset()) realpow_minus_one];
   6.421 -
   6.422 -Goal "-1 pow (((1::hypnat) + (1::hypnat))*n) = (1::hypreal)";
   6.423 -by (subgoal_tac "(-((1::hypreal))) pow (((1::hypnat) + (1::hypnat))*n) = (1::hypreal)" 1);
   6.424 -by (Asm_full_simp_tac 1); 
   6.425 -by (simp_tac (HOL_ss addsimps [hypreal_one_def]) 1);
   6.426 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   6.427 -by (auto_tac (claset(),
   6.428 -              simpset() addsimps [double_lemma, hyperpow, hypnat_add,
   6.429 -                                  hypreal_minus]));
   6.430 -qed "hyperpow_minus_one2";
   6.431 -Addsimps [hyperpow_minus_one2];
   6.432 -
   6.433 -Goalw [hypnat_one_def]
   6.434 -     "(0::hypreal) < r & r < 1 --> r pow (n + (1::hypnat)) < r pow n";
   6.435 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   6.436 -by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   6.437 -by (auto_tac (claset() addSDs [conjI RS realpow_Suc_less] 
   6.438 -                  addEs [FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset],
   6.439 -              simpset() addsimps [hypreal_zero_def, hypreal_one_def, 
   6.440 -                                  hyperpow, hypreal_less, hypnat_add]));
   6.441 -qed_spec_mp "hyperpow_Suc_less";
   6.442 -
   6.443 -Goalw [hypnat_one_def]
   6.444 -     "0 <= r & r < (1::hypreal) --> r pow (n + (1::hypnat)) <= r pow n";
   6.445 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   6.446 -by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   6.447 -by (auto_tac (claset() addSDs [conjI RS realpow_Suc_le] 
   6.448 -                 addEs [FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset],
   6.449 -              simpset() addsimps [hypreal_zero_def, hypreal_one_def, hyperpow,
   6.450 -                                  hypreal_le,hypnat_add, hypreal_less]));
   6.451 -qed_spec_mp "hyperpow_Suc_le";
   6.452 -
   6.453 -Goalw [hypnat_one_def]
   6.454 -     "(0::hypreal) <= r & r < 1 & n < N --> r pow N <= r pow n";
   6.455 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   6.456 -by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
   6.457 -by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
   6.458 -by (auto_tac (claset(),
   6.459 -              simpset() addsimps [hyperpow, hypreal_le,hypreal_less,
   6.460 -                           hypnat_less, hypreal_zero_def, hypreal_one_def]));
   6.461 -by (etac (FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset) 1);
   6.462 -by (etac FreeUltrafilterNat_Int 1);
   6.463 -by (auto_tac (claset() addSDs [conjI RS realpow_less_le], simpset()));
   6.464 -qed_spec_mp "hyperpow_less_le";
   6.465 -
   6.466 -Goal "[| (0::hypreal) <= r;  r < 1 |]  \
   6.467 -\     ==> ALL N n. n < N --> r pow N <= r pow n";
   6.468 -by (blast_tac (claset() addSIs [hyperpow_less_le]) 1);
   6.469 -qed "hyperpow_less_le2";
   6.470 -
   6.471 -Goal "[| 0 <= r;  r < (1::hypreal);  N : HNatInfinite |]  \
   6.472 -\     ==> ALL n: Nats. r pow N <= r pow n";
   6.473 -by (auto_tac (claset() addSIs [hyperpow_less_le],
   6.474 -              simpset() addsimps [HNatInfinite_iff]));
   6.475 -qed "hyperpow_SHNat_le";
   6.476 -
   6.477 -Goalw [hypreal_of_real_def,hypnat_of_nat_def] 
   6.478 -      "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)";
   6.479 -by (auto_tac (claset(), simpset() addsimps [hyperpow]));
   6.480 -qed "hyperpow_realpow";
   6.481 -
   6.482 -Goalw [SReal_def] "(hypreal_of_real r) pow (hypnat_of_nat n) : Reals";
   6.483 -by (simp_tac (simpset() delsimps [hypreal_of_real_power]
   6.484 -			addsimps [hyperpow_realpow]) 1); 
   6.485 -qed "hyperpow_SReal";
   6.486 -Addsimps [hyperpow_SReal];
   6.487 -
   6.488 -Goal "N : HNatInfinite ==> (0::hypreal) pow N = 0";
   6.489 -by (dtac HNatInfinite_is_Suc 1);
   6.490 -by Auto_tac;
   6.491 -qed "hyperpow_zero_HNatInfinite";
   6.492 -Addsimps [hyperpow_zero_HNatInfinite];
   6.493 -
   6.494 -Goal "[| (0::hypreal) <= r; r < 1; n <= N |] ==> r pow N <= r pow n";
   6.495 -by (dres_inst_tac [("y","N")] hypnat_le_imp_less_or_eq 1);
   6.496 -by (auto_tac (claset() addIs [hyperpow_less_le], simpset()));
   6.497 -qed "hyperpow_le_le";
   6.498 -
   6.499 -Goal "[| (0::hypreal) < r; r < 1 |] ==> r pow (n + (1::hypnat)) <= r";
   6.500 -by (dres_inst_tac [("n","(1::hypnat)")] (order_less_imp_le RS hyperpow_le_le) 1);
   6.501 -by Auto_tac;
   6.502 -qed "hyperpow_Suc_le_self";
   6.503 -
   6.504 -Goal "[| (0::hypreal) <= r; r < 1 |] ==> r pow (n + (1::hypnat)) <= r";
   6.505 -by (dres_inst_tac [("n","(1::hypnat)")] hyperpow_le_le 1);
   6.506 -by Auto_tac;
   6.507 -qed "hyperpow_Suc_le_self2";
   6.508 -
   6.509 -Goalw [Infinitesimal_def]
   6.510 -     "[| x : Infinitesimal; 0 < N |] ==> abs (x pow N) <= abs x";
   6.511 -by (auto_tac (claset() addSIs [hyperpow_Suc_le_self2],
   6.512 -              simpset() addsimps [hyperpow_hrabs RS sym,
   6.513 -                                  hypnat_gt_zero_iff2, abs_ge_zero]));
   6.514 -qed "lemma_Infinitesimal_hyperpow";
   6.515 -
   6.516 -Goal "[| x : Infinitesimal; 0 < N |] ==> x pow N : Infinitesimal";
   6.517 -by (rtac hrabs_le_Infinitesimal 1);
   6.518 -by (rtac lemma_Infinitesimal_hyperpow 2); 
   6.519 -by Auto_tac;  
   6.520 -qed "Infinitesimal_hyperpow";
   6.521 -
   6.522 -Goalw [hypnat_of_nat_def] 
   6.523 -     "(x ^ n : Infinitesimal) = (x pow (hypnat_of_nat n) : Infinitesimal)";
   6.524 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   6.525 -by (auto_tac (claset(), simpset() addsimps [hrealpow, hyperpow]));
   6.526 -qed "hrealpow_hyperpow_Infinitesimal_iff";
   6.527 -
   6.528 -Goal "[| x : Infinitesimal; 0 < n |] ==> x ^ n : Infinitesimal";
   6.529 -by (auto_tac (claset() addSIs [Infinitesimal_hyperpow],
   6.530 -    simpset() addsimps [hrealpow_hyperpow_Infinitesimal_iff,
   6.531 -                        hypnat_of_nat_less_iff,hypnat_of_nat_zero] 
   6.532 -              delsimps [hypnat_of_nat_less_iff RS sym]));
   6.533 -qed "Infinitesimal_hrealpow";
   6.534 -
   6.535 -(* MOVE UP *)
   6.536 -Goal "(0::hypreal) <= x * x";
   6.537 -by (auto_tac (claset(),simpset() addsimps 
   6.538 -    [zero_le_mult_iff]));
   6.539 -qed "hypreal_mult_self_ge_zero";
   6.540 -Addsimps [hypreal_mult_self_ge_zero];
   6.541 -
   6.542 -Goal "[|(0::hypreal) <= x; 0 <= y; x ^ Suc n = y ^ Suc n |] ==> x = y";
   6.543 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   6.544 -by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   6.545 -by (auto_tac (claset(),simpset() addsimps 
   6.546 -    [hrealpow,hypreal_mult,hypreal_le,hypreal_zero_num]));
   6.547 -by (ultra_tac (claset() addIs [realpow_Suc_cancel_eq],
   6.548 -    simpset()) 1);
   6.549 -qed "hrealpow_Suc_cancel_eq";
   6.550 -
     7.1 --- a/src/HOL/Hyperreal/HyperPow.thy	Fri Jan 09 01:28:24 2004 +0100
     7.2 +++ b/src/HOL/Hyperreal/HyperPow.thy	Fri Jan 09 10:46:18 2004 +0100
     7.3 @@ -4,33 +4,459 @@
     7.4      Description : Powers theory for hyperreals
     7.5  *)
     7.6  
     7.7 -HyperPow = HRealAbs + HyperNat + RealPow +  
     7.8 +header{*Exponentials on the Hyperreals*}
     7.9 +
    7.10 +theory HyperPow = HRealAbs + HyperNat + RealPow:
    7.11  
    7.12 -(** First: hypnat is linearly ordered **)
    7.13 +instance hypnat :: order
    7.14 +  by (intro_classes,
    7.15 +      (assumption | 
    7.16 +       rule hypnat_le_refl hypnat_le_trans hypnat_le_anti_sym hypnat_less_le)+)
    7.17  
    7.18 -instance hypnat :: order (hypnat_le_refl,hypnat_le_trans,hypnat_le_anti_sym,
    7.19 -                          hypnat_less_le)
    7.20 -instance hypnat :: linorder (hypnat_le_linear)
    7.21 +                          
    7.22 +text{*Type @{typ hypnat} is linearly ordered*}
    7.23 +instance hypnat :: linorder 
    7.24 +  by (intro_classes, rule hypnat_le_linear)
    7.25  
    7.26 -instance hypnat :: plus_ac0(hypnat_add_commute,hypnat_add_assoc,
    7.27 -                            hypnat_add_zero_left)
    7.28 +instance hypnat :: plus_ac0
    7.29 +  by (intro_classes,
    7.30 +      (assumption | 
    7.31 +       rule hypnat_add_commute hypnat_add_assoc hypnat_add_zero_left)+)
    7.32  
    7.33  
    7.34 -instance hypreal :: {power}
    7.35 +instance hypreal :: power ..
    7.36  
    7.37  consts hpowr :: "[hypreal,nat] => hypreal"  
    7.38  primrec
    7.39 -     hpowr_0   "r ^ 0       = (1::hypreal)"
    7.40 -     hpowr_Suc "r ^ (Suc n) = (r::hypreal) * (r ^ n)"
    7.41 +   hpowr_0:   "r ^ 0       = (1::hypreal)"
    7.42 +   hpowr_Suc: "r ^ (Suc n) = (r::hypreal) * (r ^ n)"
    7.43 +
    7.44 +
    7.45 +instance hypreal :: ringpower
    7.46 +proof
    7.47 +  fix z :: hypreal
    7.48 +  fix n :: nat
    7.49 +  show "z^0 = 1" by simp
    7.50 +  show "z^(Suc n) = z * (z^n)" by simp
    7.51 +qed
    7.52 +
    7.53  
    7.54  consts
    7.55 -  "pow"  :: [hypreal,hypnat] => hypreal     (infixr 80)
    7.56 +  "pow"  :: "[hypreal,hypnat] => hypreal"     (infixr 80)
    7.57  
    7.58  defs
    7.59  
    7.60    (* hypernatural powers of hyperreals *)
    7.61 -  hyperpow_def
    7.62 -  "(R::hypreal) pow (N::hypnat) 
    7.63 -      == Abs_hypreal(UN X:Rep_hypreal(R). UN Y: Rep_hypnat(N).
    7.64 -             hyprel``{%n::nat. (X n) ^ (Y n)})"
    7.65 +  hyperpow_def:
    7.66 +  "(R::hypreal) pow (N::hypnat) ==
    7.67 +      Abs_hypreal(\<Union>X \<in> Rep_hypreal(R). \<Union>Y \<in> Rep_hypnat(N).
    7.68 +                        hyprel``{%n::nat. (X n) ^ (Y n)})"
    7.69 +
    7.70 +lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r"
    7.71 +apply (simp (no_asm))
    7.72 +done
    7.73 +
    7.74 +lemma hrabs_hrealpow_minus_one [simp]: "abs(-1 ^ n) = (1::hypreal)"
    7.75 +apply (simp add: power_abs); 
    7.76 +done
    7.77 +
    7.78 +lemma hrealpow_two_le: "(0::hypreal) \<le> r ^ Suc (Suc 0)"
    7.79 +apply (auto simp add: zero_le_mult_iff)
    7.80 +done
    7.81 +declare hrealpow_two_le [simp]
    7.82 +
    7.83 +lemma hrealpow_two_le_add_order:
    7.84 +     "(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0)"
    7.85 +apply (simp only: hrealpow_two_le hypreal_le_add_order)
    7.86 +done
    7.87 +declare hrealpow_two_le_add_order [simp]
    7.88 +
    7.89 +lemma hrealpow_two_le_add_order2:
    7.90 +     "(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0) + w ^ Suc (Suc 0)"
    7.91 +apply (simp only: hrealpow_two_le hypreal_le_add_order)
    7.92 +done
    7.93 +declare hrealpow_two_le_add_order2 [simp]
    7.94 +
    7.95 +lemma hypreal_add_nonneg_eq_0_iff:
    7.96 +     "[| 0 \<le> x; 0 \<le> y |] ==> (x+y = 0) = (x = 0 & y = (0::hypreal))"
    7.97 +apply arith
    7.98 +done
    7.99 +
   7.100 +text{*FIXME: DELETE THESE*}
   7.101 +lemma hypreal_three_squares_add_zero_iff:
   7.102 +     "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))"
   7.103 +apply (simp only: zero_le_square hypreal_le_add_order hypreal_add_nonneg_eq_0_iff)
   7.104 +apply auto
   7.105 +done
   7.106 +
   7.107 +lemma hrealpow_three_squares_add_zero_iff [simp]:
   7.108 +     "(x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = (0::hypreal)) = 
   7.109 +      (x = 0 & y = 0 & z = 0)"
   7.110 +by (simp only: hypreal_three_squares_add_zero_iff hrealpow_two)
   7.111 +
   7.112 +
   7.113 +lemma hrabs_hrealpow_two [simp]:
   7.114 +     "abs(x ^ Suc (Suc 0)) = (x::hypreal) ^ Suc (Suc 0)"
   7.115 +by (simp add: abs_mult)
   7.116 +
   7.117 +lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \<le> 2 ^ n"
   7.118 +by (insert power_increasing [of 0 n "2::hypreal"], simp)
   7.119 +
   7.120 +lemma two_hrealpow_gt: "hypreal_of_nat n < 2 ^ n"
   7.121 +apply (induct_tac "n")
   7.122 +apply (auto simp add: hypreal_of_nat_Suc left_distrib)
   7.123 +apply (cut_tac n = "n" in two_hrealpow_ge_one)
   7.124 +apply arith
   7.125 +done
   7.126 +declare two_hrealpow_gt [simp] 
   7.127 +
   7.128 +lemma hrealpow_minus_one: "-1 ^ (2*n) = (1::hypreal)"
   7.129 +apply (induct_tac "n")
   7.130 +apply auto
   7.131 +done
   7.132 +
   7.133 +lemma double_lemma: "n+n = (2*n::nat)"
   7.134 +apply auto
   7.135 +done
   7.136 +
   7.137 +(*ugh: need to get rid fo the n+n*)
   7.138 +lemma hrealpow_minus_one2: "-1 ^ (n + n) = (1::hypreal)"
   7.139 +apply (auto simp add: double_lemma hrealpow_minus_one)
   7.140 +done
   7.141 +declare hrealpow_minus_one2 [simp]
   7.142 +
   7.143 +lemma hrealpow:
   7.144 +    "Abs_hypreal(hyprel``{%n. X n}) ^ m = Abs_hypreal(hyprel``{%n. (X n) ^ m})"
   7.145 +apply (induct_tac "m")
   7.146 +apply (auto simp add: hypreal_one_def hypreal_mult)
   7.147 +done
   7.148 +
   7.149 +lemma hrealpow_sum_square_expand:
   7.150 +     "(x + (y::hypreal)) ^ Suc (Suc 0) =
   7.151 +      x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0)))*x*y"
   7.152 +by (simp add: right_distrib left_distrib hypreal_of_nat_Suc)
   7.153 +
   7.154 +
   7.155 +subsection{*Literal Arithmetic Involving Powers and Type @{typ hypreal}*}
   7.156 +
   7.157 +lemma hypreal_of_real_power: "hypreal_of_real (x ^ n) = hypreal_of_real x ^ n"
   7.158 +apply (induct_tac "n")
   7.159 +apply (simp_all add: nat_mult_distrib)
   7.160 +done
   7.161 +declare hypreal_of_real_power [simp]
   7.162 +
   7.163 +lemma power_hypreal_of_real_number_of:
   7.164 +     "(number_of v :: hypreal) ^ n = hypreal_of_real ((number_of v) ^ n)"
   7.165 +by (simp only: hypreal_number_of_def hypreal_of_real_power)
   7.166 +
   7.167 +declare power_hypreal_of_real_number_of [of _ "number_of w", standard, simp]
   7.168 +
   7.169 +lemma hrealpow_HFinite: "x \<in> HFinite ==> x ^ n \<in> HFinite"
   7.170 +apply (induct_tac "n")
   7.171 +apply (auto intro: HFinite_mult)
   7.172 +done
   7.173 +
   7.174 +
   7.175 +subsection{*Powers with Hypernatural Exponents*}
   7.176 +
   7.177 +lemma hyperpow_congruent:
   7.178 +     "congruent hyprel
   7.179 +     (%X Y. hyprel``{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})"
   7.180 +apply (unfold congruent_def)
   7.181 +apply (auto intro!: ext)
   7.182 +apply fuf+
   7.183 +done
   7.184 +
   7.185 +lemma hyperpow:
   7.186 +  "Abs_hypreal(hyprel``{%n. X n}) pow Abs_hypnat(hypnatrel``{%n. Y n}) =
   7.187 +   Abs_hypreal(hyprel``{%n. X n ^ Y n})"
   7.188 +apply (unfold hyperpow_def)
   7.189 +apply (rule_tac f = "Abs_hypreal" in arg_cong)
   7.190 +apply (auto intro!: lemma_hyprel_refl bexI 
   7.191 +           simp add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] equiv_hyprel 
   7.192 +                     hyperpow_congruent)
   7.193 +apply fuf
   7.194 +done
   7.195 +
   7.196 +lemma hyperpow_zero: "(0::hypreal) pow (n + (1::hypnat)) = 0"
   7.197 +apply (unfold hypnat_one_def)
   7.198 +apply (simp (no_asm) add: hypreal_zero_def)
   7.199 +apply (rule_tac z = "n" in eq_Abs_hypnat)
   7.200 +apply (auto simp add: hyperpow hypnat_add)
   7.201 +done
   7.202 +declare hyperpow_zero [simp]
   7.203 +
   7.204 +lemma hyperpow_not_zero [rule_format (no_asm)]:
   7.205 +     "r \<noteq> (0::hypreal) --> r pow n \<noteq> 0"
   7.206 +apply (simp (no_asm) add: hypreal_zero_def)
   7.207 +apply (rule_tac z = "n" in eq_Abs_hypnat)
   7.208 +apply (rule_tac z = "r" in eq_Abs_hypreal)
   7.209 +apply (auto simp add: hyperpow)
   7.210 +apply (drule FreeUltrafilterNat_Compl_mem)
   7.211 +apply ultra
   7.212 +done
   7.213 +
   7.214 +lemma hyperpow_inverse:
   7.215 +     "r \<noteq> (0::hypreal) --> inverse(r pow n) = (inverse r) pow n"
   7.216 +apply (simp (no_asm) add: hypreal_zero_def)
   7.217 +apply (rule_tac z = "n" in eq_Abs_hypnat)
   7.218 +apply (rule_tac z = "r" in eq_Abs_hypreal)
   7.219 +apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: hypreal_inverse hyperpow)
   7.220 +apply (rule FreeUltrafilterNat_subset)
   7.221 +apply (auto dest: realpow_not_zero intro: power_inverse)
   7.222 +done
   7.223 +
   7.224 +lemma hyperpow_hrabs: "abs r pow n = abs (r pow n)"
   7.225 +apply (rule_tac z = "n" in eq_Abs_hypnat)
   7.226 +apply (rule_tac z = "r" in eq_Abs_hypreal)
   7.227 +apply (auto simp add: hypreal_hrabs hyperpow power_abs [symmetric])
   7.228 +done
   7.229 +
   7.230 +lemma hyperpow_add: "r pow (n + m) = (r pow n) * (r pow m)"
   7.231 +apply (rule_tac z = "n" in eq_Abs_hypnat)
   7.232 +apply (rule_tac z = "m" in eq_Abs_hypnat)
   7.233 +apply (rule_tac z = "r" in eq_Abs_hypreal)
   7.234 +apply (auto simp add: hyperpow hypnat_add hypreal_mult power_add)
   7.235 +done
   7.236 +
   7.237 +lemma hyperpow_one: "r pow (1::hypnat) = r"
   7.238 +apply (unfold hypnat_one_def)
   7.239 +apply (rule_tac z = "r" in eq_Abs_hypreal)
   7.240 +apply (auto simp add: hyperpow)
   7.241 +done
   7.242 +declare hyperpow_one [simp]
   7.243 +
   7.244 +lemma hyperpow_two:
   7.245 +     "r pow ((1::hypnat) + (1::hypnat)) = r * r"
   7.246 +apply (unfold hypnat_one_def)
   7.247 +apply (rule_tac z = "r" in eq_Abs_hypreal)
   7.248 +apply (auto simp add: hyperpow hypnat_add hypreal_mult)
   7.249 +done
   7.250 +
   7.251 +lemma hyperpow_gt_zero: "(0::hypreal) < r ==> 0 < r pow n"
   7.252 +apply (simp add: hypreal_zero_def)
   7.253 +apply (rule_tac z = "n" in eq_Abs_hypnat)
   7.254 +apply (rule_tac z = "r" in eq_Abs_hypreal)
   7.255 +apply (auto elim!: FreeUltrafilterNat_subset zero_less_power
   7.256 +                   simp add: hyperpow hypreal_less hypreal_le)
   7.257 +done
   7.258 +
   7.259 +lemma hyperpow_ge_zero: "(0::hypreal) \<le> r ==> 0 \<le> r pow n"
   7.260 +apply (simp add: hypreal_zero_def)
   7.261 +apply (rule_tac z = "n" in eq_Abs_hypnat)
   7.262 +apply (rule_tac z = "r" in eq_Abs_hypreal)
   7.263 +apply (auto elim!: FreeUltrafilterNat_subset zero_le_power 
   7.264 +            simp add: hyperpow hypreal_le)
   7.265 +done
   7.266 +
   7.267 +lemma hyperpow_le: "[|(0::hypreal) < x; x \<le> y|] ==> x pow n \<le> y pow n"
   7.268 +apply (simp add: hypreal_zero_def)
   7.269 +apply (rule_tac z = "n" in eq_Abs_hypnat)
   7.270 +apply (rule_tac z = "x" in eq_Abs_hypreal)
   7.271 +apply (rule_tac z = "y" in eq_Abs_hypreal)
   7.272 +apply (auto simp add: hyperpow hypreal_le hypreal_less)
   7.273 +apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset] , assumption)
   7.274 +apply (auto intro: power_mono)
   7.275 +done
   7.276 +
   7.277 +lemma hyperpow_eq_one: "1 pow n = (1::hypreal)"
   7.278 +apply (rule_tac z = "n" in eq_Abs_hypnat)
   7.279 +apply (auto simp add: hypreal_one_def hyperpow)
   7.280 +done
   7.281 +declare hyperpow_eq_one [simp]
   7.282 +
   7.283 +lemma hrabs_hyperpow_minus_one: "abs(-1 pow n) = (1::hypreal)"
   7.284 +apply (subgoal_tac "abs ((- (1::hypreal)) pow n) = (1::hypreal) ")
   7.285 +apply simp
   7.286 +apply (rule_tac z = "n" in eq_Abs_hypnat)
   7.287 +apply (auto simp add: hypreal_one_def hyperpow hypreal_minus hypreal_hrabs)
   7.288 +done
   7.289 +declare hrabs_hyperpow_minus_one [simp]
   7.290 +
   7.291 +lemma hyperpow_mult: "(r * s) pow n = (r pow n) * (s pow n)"
   7.292 +apply (rule_tac z = "n" in eq_Abs_hypnat)
   7.293 +apply (rule_tac z = "r" in eq_Abs_hypreal)
   7.294 +apply (rule_tac z = "s" in eq_Abs_hypreal)
   7.295 +apply (auto simp add: hyperpow hypreal_mult power_mult_distrib)
   7.296 +done
   7.297 +
   7.298 +lemma hyperpow_two_le: "(0::hypreal) \<le> r pow ((1::hypnat) + (1::hypnat))"
   7.299 +apply (auto simp add: hyperpow_two zero_le_mult_iff)
   7.300 +done
   7.301 +declare hyperpow_two_le [simp]
   7.302 +
   7.303 +lemma hrabs_hyperpow_two:
   7.304 +     "abs(x pow (1 + 1)) = x pow (1 + 1)"
   7.305 +apply (simp (no_asm) add: hrabs_eqI1)
   7.306 +done
   7.307 +declare hrabs_hyperpow_two [simp]
   7.308 +
   7.309 +lemma hyperpow_two_hrabs:
   7.310 +     "abs(x) pow (1 + 1)  = x pow (1 + 1)"
   7.311 +apply (simp add: hyperpow_hrabs)
   7.312 +done
   7.313 +declare hyperpow_two_hrabs [simp]
   7.314 +
   7.315 +lemma hyperpow_two_gt_one:
   7.316 +     "(1::hypreal) < r ==> 1 < r pow (1 + 1)"
   7.317 +apply (auto simp add: hyperpow_two)
   7.318 +apply (rule_tac y = "1*1" in order_le_less_trans)
   7.319 +apply (rule_tac [2] hypreal_mult_less_mono)
   7.320 +apply auto
   7.321 +done
   7.322 +
   7.323 +lemma hyperpow_two_ge_one:
   7.324 +     "(1::hypreal) \<le> r ==> 1 \<le> r pow (1 + 1)"
   7.325 +apply (auto dest!: order_le_imp_less_or_eq intro: hyperpow_two_gt_one order_less_imp_le)
   7.326 +done
   7.327 +
   7.328 +lemma two_hyperpow_ge_one: "(1::hypreal) \<le> 2 pow n"
   7.329 +apply (rule_tac y = "1 pow n" in order_trans)
   7.330 +apply (rule_tac [2] hyperpow_le)
   7.331 +apply auto
   7.332 +done
   7.333 +declare two_hyperpow_ge_one [simp]
   7.334 +
   7.335 +lemma hyperpow_minus_one2:
   7.336 +     "-1 pow ((1 + 1)*n) = (1::hypreal)"
   7.337 +apply (subgoal_tac " (- ((1::hypreal))) pow ((1 + 1)*n) = (1::hypreal) ")
   7.338 +apply simp
   7.339 +apply (simp only: hypreal_one_def)
   7.340 +apply (rule_tac z = "n" in eq_Abs_hypnat)
   7.341 +apply (auto simp add: double_lemma hyperpow hypnat_add hypreal_minus)
   7.342 +done
   7.343 +declare hyperpow_minus_one2 [simp]
   7.344 +
   7.345 +lemma hyperpow_less_le:
   7.346 +     "[|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
   7.347 +apply (rule_tac z = "n" in eq_Abs_hypnat)
   7.348 +apply (rule_tac z = "N" in eq_Abs_hypnat)
   7.349 +apply (rule_tac z = "r" in eq_Abs_hypreal)
   7.350 +apply (auto simp add: hyperpow hypreal_le hypreal_less hypnat_less 
   7.351 +            hypreal_zero_def hypreal_one_def)
   7.352 +apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
   7.353 +apply (erule FreeUltrafilterNat_Int)
   7.354 +apply assumption; 
   7.355 +apply (auto intro: power_decreasing)
   7.356 +done
   7.357 +
   7.358 +lemma hyperpow_SHNat_le:
   7.359 +     "[| 0 \<le> r;  r \<le> (1::hypreal);  N \<in> HNatInfinite |]
   7.360 +      ==> ALL n: Nats. r pow N \<le> r pow n"
   7.361 +by (auto intro!: hyperpow_less_le simp add: HNatInfinite_iff)
   7.362 +
   7.363 +lemma hyperpow_realpow:
   7.364 +      "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"
   7.365 +apply (unfold hypreal_of_real_def hypnat_of_nat_def)
   7.366 +apply (auto simp add: hyperpow)
   7.367 +done
   7.368 +
   7.369 +lemma hyperpow_SReal: "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals"
   7.370 +apply (unfold SReal_def)
   7.371 +apply (simp (no_asm) del: hypreal_of_real_power add: hyperpow_realpow)
   7.372 +done
   7.373 +declare hyperpow_SReal [simp]
   7.374 +
   7.375 +lemma hyperpow_zero_HNatInfinite: "N \<in> HNatInfinite ==> (0::hypreal) pow N = 0"
   7.376 +apply (drule HNatInfinite_is_Suc)
   7.377 +apply auto
   7.378 +done
   7.379 +declare hyperpow_zero_HNatInfinite [simp]
   7.380 +
   7.381 +lemma hyperpow_le_le:
   7.382 +     "[| (0::hypreal) \<le> r; r \<le> 1; n \<le> N |] ==> r pow N \<le> r pow n"
   7.383 +apply (drule_tac y = "N" in hypnat_le_imp_less_or_eq)
   7.384 +apply (auto intro: hyperpow_less_le)
   7.385 +done
   7.386 +
   7.387 +lemma hyperpow_Suc_le_self2:
   7.388 +     "[| (0::hypreal) \<le> r; r < 1 |] ==> r pow (n + (1::hypnat)) \<le> r"
   7.389 +apply (drule_tac n = " (1::hypnat) " in hyperpow_le_le)
   7.390 +apply auto
   7.391 +done
   7.392 +
   7.393 +lemma lemma_Infinitesimal_hyperpow:
   7.394 +     "[| x \<in> Infinitesimal; 0 < N |] ==> abs (x pow N) \<le> abs x"
   7.395 +apply (unfold Infinitesimal_def)
   7.396 +apply (auto intro!: hyperpow_Suc_le_self2 
   7.397 +          simp add: hyperpow_hrabs [symmetric] hypnat_gt_zero_iff2 abs_ge_zero)
   7.398 +done
   7.399 +
   7.400 +lemma Infinitesimal_hyperpow:
   7.401 +     "[| x \<in> Infinitesimal; 0 < N |] ==> x pow N \<in> Infinitesimal"
   7.402 +apply (rule hrabs_le_Infinitesimal)
   7.403 +apply (rule_tac [2] lemma_Infinitesimal_hyperpow)
   7.404 +apply auto
   7.405 +done
   7.406 +
   7.407 +lemma hrealpow_hyperpow_Infinitesimal_iff:
   7.408 +     "(x ^ n \<in> Infinitesimal) = (x pow (hypnat_of_nat n) \<in> Infinitesimal)"
   7.409 +apply (unfold hypnat_of_nat_def)
   7.410 +apply (rule_tac z = "x" in eq_Abs_hypreal)
   7.411 +apply (auto simp add: hrealpow hyperpow)
   7.412 +done
   7.413 +
   7.414 +lemma Infinitesimal_hrealpow:
   7.415 +     "[| x \<in> Infinitesimal; 0 < n |] ==> x ^ n \<in> Infinitesimal"
   7.416 +by (force intro!: Infinitesimal_hyperpow
   7.417 +          simp add: hrealpow_hyperpow_Infinitesimal_iff 
   7.418 +                    hypnat_of_nat_less_iff hypnat_of_nat_zero
   7.419 +          simp del: hypnat_of_nat_less_iff [symmetric])
   7.420 +
   7.421 +ML
   7.422 +{*
   7.423 +val hrealpow_two = thm "hrealpow_two";
   7.424 +val hrabs_hrealpow_minus_one = thm "hrabs_hrealpow_minus_one";
   7.425 +val hrealpow_two_le = thm "hrealpow_two_le";
   7.426 +val hrealpow_two_le_add_order = thm "hrealpow_two_le_add_order";
   7.427 +val hrealpow_two_le_add_order2 = thm "hrealpow_two_le_add_order2";
   7.428 +val hypreal_add_nonneg_eq_0_iff = thm "hypreal_add_nonneg_eq_0_iff";
   7.429 +val hypreal_three_squares_add_zero_iff = thm "hypreal_three_squares_add_zero_iff";
   7.430 +val hrealpow_three_squares_add_zero_iff = thm "hrealpow_three_squares_add_zero_iff";
   7.431 +val hrabs_hrealpow_two = thm "hrabs_hrealpow_two";
   7.432 +val two_hrealpow_ge_one = thm "two_hrealpow_ge_one";
   7.433 +val two_hrealpow_gt = thm "two_hrealpow_gt";
   7.434 +val hrealpow_minus_one = thm "hrealpow_minus_one";
   7.435 +val double_lemma = thm "double_lemma";
   7.436 +val hrealpow_minus_one2 = thm "hrealpow_minus_one2";
   7.437 +val hrealpow = thm "hrealpow";
   7.438 +val hrealpow_sum_square_expand = thm "hrealpow_sum_square_expand";
   7.439 +val hypreal_of_real_power = thm "hypreal_of_real_power";
   7.440 +val power_hypreal_of_real_number_of = thm "power_hypreal_of_real_number_of";
   7.441 +val hrealpow_HFinite = thm "hrealpow_HFinite";
   7.442 +val hyperpow_congruent = thm "hyperpow_congruent";
   7.443 +val hyperpow = thm "hyperpow";
   7.444 +val hyperpow_zero = thm "hyperpow_zero";
   7.445 +val hyperpow_not_zero = thm "hyperpow_not_zero";
   7.446 +val hyperpow_inverse = thm "hyperpow_inverse";
   7.447 +val hyperpow_hrabs = thm "hyperpow_hrabs";
   7.448 +val hyperpow_add = thm "hyperpow_add";
   7.449 +val hyperpow_one = thm "hyperpow_one";
   7.450 +val hyperpow_two = thm "hyperpow_two";
   7.451 +val hyperpow_gt_zero = thm "hyperpow_gt_zero";
   7.452 +val hyperpow_ge_zero = thm "hyperpow_ge_zero";
   7.453 +val hyperpow_le = thm "hyperpow_le";
   7.454 +val hyperpow_eq_one = thm "hyperpow_eq_one";
   7.455 +val hrabs_hyperpow_minus_one = thm "hrabs_hyperpow_minus_one";
   7.456 +val hyperpow_mult = thm "hyperpow_mult";
   7.457 +val hyperpow_two_le = thm "hyperpow_two_le";
   7.458 +val hrabs_hyperpow_two = thm "hrabs_hyperpow_two";
   7.459 +val hyperpow_two_hrabs = thm "hyperpow_two_hrabs";
   7.460 +val hyperpow_two_gt_one = thm "hyperpow_two_gt_one";
   7.461 +val hyperpow_two_ge_one = thm "hyperpow_two_ge_one";
   7.462 +val two_hyperpow_ge_one = thm "two_hyperpow_ge_one";
   7.463 +val hyperpow_minus_one2 = thm "hyperpow_minus_one2";
   7.464 +val hyperpow_less_le = thm "hyperpow_less_le";
   7.465 +val hyperpow_SHNat_le = thm "hyperpow_SHNat_le";
   7.466 +val hyperpow_realpow = thm "hyperpow_realpow";
   7.467 +val hyperpow_SReal = thm "hyperpow_SReal";
   7.468 +val hyperpow_zero_HNatInfinite = thm "hyperpow_zero_HNatInfinite";
   7.469 +val hyperpow_le_le = thm "hyperpow_le_le";
   7.470 +val hyperpow_Suc_le_self2 = thm "hyperpow_Suc_le_self2";
   7.471 +val lemma_Infinitesimal_hyperpow = thm "lemma_Infinitesimal_hyperpow";
   7.472 +val Infinitesimal_hyperpow = thm "Infinitesimal_hyperpow";
   7.473 +val hrealpow_hyperpow_Infinitesimal_iff = thm "hrealpow_hyperpow_Infinitesimal_iff";
   7.474 +val Infinitesimal_hrealpow = thm "Infinitesimal_hrealpow";
   7.475 +*}
   7.476 +
   7.477  end
     8.1 --- a/src/HOL/Hyperreal/Lim.ML	Fri Jan 09 01:28:24 2004 +0100
     8.2 +++ b/src/HOL/Hyperreal/Lim.ML	Fri Jan 09 10:46:18 2004 +0100
     8.3 @@ -1348,7 +1348,7 @@
     8.4  Goal "[| DERIV f x :> d; f(x) \\<noteq> 0 |] \
     8.5  \     ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))";
     8.6  by (rtac (real_mult_commute RS subst) 1);
     8.7 -by (asm_simp_tac (HOL_ss addsimps [minus_mult_left, realpow_inverse]) 1);
     8.8 +by (asm_simp_tac (HOL_ss addsimps [minus_mult_left, power_inverse]) 1);
     8.9  by (fold_goals_tac [o_def]);
    8.10  by (blast_tac (claset() addSIs [DERIV_chain,DERIV_inverse]) 1);
    8.11  qed "DERIV_inverse_fun";
    8.12 @@ -1369,7 +1369,7 @@
    8.13  by (REPEAT(assume_tac 1));
    8.14  by (asm_full_simp_tac
    8.15      (simpset() addsimps [real_divide_def, right_distrib,
    8.16 -                         realpow_inverse,minus_mult_left] @ mult_ac 
    8.17 +                         power_inverse,minus_mult_left] @ mult_ac 
    8.18         delsimps [realpow_Suc, minus_mult_right RS sym, minus_mult_left RS sym]) 1);
    8.19  qed "DERIV_quotient";
    8.20  
     9.1 --- a/src/HOL/Hyperreal/MacLaurin.ML	Fri Jan 09 01:28:24 2004 +0100
     9.2 +++ b/src/HOL/Hyperreal/MacLaurin.ML	Fri Jan 09 10:46:18 2004 +0100
     9.3 @@ -65,8 +65,8 @@
     9.4       delsimps [realpow_Suc]) 2);
     9.5  by (stac real_mult_inv_left 2);
     9.6  by (stac real_mult_inv_left 3);
     9.7 -by (dtac (realpow_gt_zero RS real_not_refl2 RS not_sym) 2);
     9.8 -by (assume_tac 2);
     9.9 +by (rtac (real_not_refl2 RS not_sym) 2);
    9.10 +by (etac zero_less_power 2);
    9.11  by (rtac real_of_nat_fact_not_zero 2);
    9.12  by (Simp_tac 2);
    9.13  by (etac exE 1);
    9.14 @@ -281,7 +281,7 @@
    9.15  by (Asm_full_simp_tac 1);
    9.16  by (auto_tac (claset(),simpset() addsimps [real_divide_def,
    9.17      CLAIM "((a * b) * c) * d = (b * c) * (a * (d::real))",
    9.18 -    realpow_mult RS sym]));
    9.19 +    power_mult_distrib RS sym]));
    9.20  qed "Maclaurin_minus";
    9.21  
    9.22  Goal "(h < 0 & 0 < n & diff 0 = f & \
    9.23 @@ -490,7 +490,7 @@
    9.24  by (dtac lemma_odd_mod_4_div_2 1);
    9.25  by (asm_full_simp_tac (simpset() addsimps [numeral_2_eq_2, real_divide_def]) 1);
    9.26  by (auto_tac (claset() addSIs [real_mult_le_lemma,mult_right_mono],
    9.27 -      simpset() addsimps [real_divide_def,abs_mult,abs_inverse,realpow_abs RS
    9.28 +      simpset() addsimps [real_divide_def,abs_mult,abs_inverse,power_abs RS
    9.29  sym]));
    9.30  qed "Maclaurin_sin_bound";
    9.31  
    9.32 @@ -520,7 +520,7 @@
    9.33  by (cut_inst_tac [("f","sin"),("n","n"),("x","x"),
    9.34         ("diff","%n x. sin(x + 1/2*real (n)*pi)")] 
    9.35         Maclaurin_all_lt_objl 1);
    9.36 -by (Step_tac 1);
    9.37 +by (Safe_tac);
    9.38  by (Simp_tac 1);
    9.39  by (Simp_tac 1);
    9.40  by (case_tac "n" 1);
    10.1 --- a/src/HOL/Hyperreal/NthRoot.thy	Fri Jan 09 01:28:24 2004 +0100
    10.2 +++ b/src/HOL/Hyperreal/NthRoot.thy	Fri Jan 09 10:46:18 2004 +0100
    10.3 @@ -20,9 +20,14 @@
    10.4  apply (rule_tac x = "1" in exI)
    10.5  apply (drule_tac [2] linorder_not_le [THEN iffD1])
    10.6  apply (drule_tac [2] less_not_refl2 [THEN not0_implies_Suc])
    10.7 -apply (auto intro!: realpow_Suc_le_self simp add: zero_less_one)
    10.8 +apply (simp add: ); 
    10.9 +apply (force intro!: realpow_Suc_le_self simp del: realpow_Suc)
   10.10  done
   10.11  
   10.12 +text{*Used only just below*}
   10.13 +lemma realpow_ge_self2: "[| (1::real) \<le> r; 0 < n |] ==> r \<le> r ^ n"
   10.14 +by (insert power_increasing [of 1 n r], simp)
   10.15 +
   10.16  lemma lemma_nth_realpow_isUb_ex:
   10.17       "[| (0::real) < a; 0 < n |]  
   10.18        ==> \<exists>u. isUb (UNIV::real set) {x. x ^ n <= a & 0 < x} u"
   10.19 @@ -129,10 +134,10 @@
   10.20  apply (rule_tac n = "k" in real_mult_less_self)
   10.21  apply (blast intro: lemma_nth_realpow_isLub_gt_zero)
   10.22  apply (safe)
   10.23 -apply (drule_tac n = "k" in lemma_nth_realpow_isLub_gt_zero [THEN real_mult_add_one_minus_ge_zero])
   10.24 -apply (drule_tac [3] conjI [THEN realpow_le2])
   10.25 -apply (rule_tac [3] order_less_imp_le) 
   10.26 -apply (auto intro: order_trans)
   10.27 +apply (drule_tac n = "k" in
   10.28 +        lemma_nth_realpow_isLub_gt_zero [THEN real_mult_add_one_minus_ge_zero])
   10.29 +apply assumption+
   10.30 +apply (blast intro: order_trans order_less_imp_le power_mono) 
   10.31  done
   10.32  
   10.33  text{*Second result we want*}
   10.34 @@ -141,11 +146,12 @@
   10.35       isLub (UNIV::real set)  
   10.36       {x. x ^ n <= a & 0 < x} u |] ==> u ^ n <= a"
   10.37  apply (frule lemma_nth_realpow_isLub_le , safe)
   10.38 -apply (rule LIMSEQ_inverse_real_of_nat_add_minus_mult [THEN LIMSEQ_pow, THEN LIMSEQ_le_const2])
   10.39 +apply (rule LIMSEQ_inverse_real_of_nat_add_minus_mult
   10.40 +                [THEN LIMSEQ_pow, THEN LIMSEQ_le_const2])
   10.41  apply (auto simp add: real_of_nat_def)
   10.42  done
   10.43  
   10.44 -(*----------- The theorem at last! -----------*)
   10.45 +text{*The theorem at last!*}
   10.46  lemma realpow_nth: "[| (0::real) < a; 0 < n |] ==> \<exists>r. r ^ n = a"
   10.47  apply (frule nth_realpow_isLub_ex , auto)
   10.48  apply (auto intro: realpow_nth_le realpow_nth_ge real_le_anti_sym)
    11.1 --- a/src/HOL/Hyperreal/Poly.ML	Fri Jan 09 01:28:24 2004 +0100
    11.2 +++ b/src/HOL/Hyperreal/Poly.ML	Fri Jan 09 10:46:18 2004 +0100
    11.3 @@ -1002,7 +1002,7 @@
    11.4  by (dtac (poly_mult_left_cancel RS iffD1) 1);
    11.5  by (Asm_full_simp_tac 1);
    11.6  by (asm_full_simp_tac (simpset() addsimps [fun_eq,poly_mult,poly_add,poly_cmult,
    11.7 -    poly_minus] delsimps [pmult_Cons, thm"mult_cancel_left"]) 1);
    11.8 +    poly_minus] delsimps [pmult_Cons, mult_cancel_left, field_mult_cancel_left]) 1);
    11.9  by (Step_tac 1);
   11.10  by (res_inst_tac [("c1","real (Suc n)")] (real_mult_left_cancel 
   11.11      RS iffD1) 1);
    12.1 --- a/src/HOL/Hyperreal/SEQ.ML	Fri Jan 09 01:28:24 2004 +0100
    12.2 +++ b/src/HOL/Hyperreal/SEQ.ML	Fri Jan 09 10:46:18 2004 +0100
    12.3 @@ -1216,22 +1216,25 @@
    12.4  qed "LIMSEQ_pow";
    12.5  
    12.6  (*----------------------------------------------------------------
    12.7 -               0 <= x < 1 ==> (x ^ n ----> 0)
    12.8 +               0 <= x <= 1 ==> (x ^ n ----> 0)
    12.9    Proof will use (NS) Cauchy equivalence for convergence and
   12.10    also fact that bounded and monotonic sequence converges.  
   12.11   ---------------------------------------------------------------*)
   12.12 -Goalw [Bseq_def] "[| 0 <= x; x < 1 |] ==> Bseq (%n. x ^ n)";
   12.13 +Goalw [Bseq_def] "[| 0 <= x; x <= 1 |] ==> Bseq (%n. x ^ n)";
   12.14  by (res_inst_tac [("x","1")] exI 1);
   12.15 -by (auto_tac (claset() addDs [conjI RS realpow_le] 
   12.16 +by (asm_full_simp_tac (simpset() addsimps [power_abs]) 1);
   12.17 +by (auto_tac (claset() addDs [power_mono] 
   12.18                         addIs [order_less_imp_le], 
   12.19 -              simpset() addsimps [abs_eqI1, realpow_abs] ));
   12.20 +              simpset() addsimps [abs_if] ));
   12.21  qed "Bseq_realpow";
   12.22  
   12.23 -Goal "[| 0 <= x; x < 1 |] ==> monoseq (%n. x ^ n)";
   12.24 -by (blast_tac (claset() addSIs [mono_SucI2,realpow_Suc_le3]) 1);
   12.25 +Goal "[| 0 <= x; x <= 1 |] ==> monoseq (%n. x ^ n)";
   12.26 +by (clarify_tac (claset() addSIs [mono_SucI2]) 1);
   12.27 +by (cut_inst_tac [("n","n"),("N","Suc n"),("a","x")] power_decreasing 1);
   12.28 +by Auto_tac;
   12.29  qed "monoseq_realpow";
   12.30  
   12.31 -Goal "[| 0 <= x; x < 1 |] ==> convergent (%n. x ^ n)";
   12.32 +Goal "[| 0 <= x; x <= 1 |] ==> convergent (%n. x ^ n)";
   12.33  by (blast_tac (claset() addSIs [Bseq_monoseq_convergent,
   12.34                                  Bseq_realpow,monoseq_realpow]) 1);
   12.35  qed "convergent_realpow";
   12.36 @@ -1269,7 +1272,7 @@
   12.37  by (cut_inst_tac [("a","a"),("x1","inverse x")] 
   12.38      ([LIMSEQ_const, LIMSEQ_realpow_zero] MRS LIMSEQ_mult) 1);
   12.39  by (auto_tac (claset(), 
   12.40 -              simpset() addsimps [real_divide_def, realpow_inverse])); 
   12.41 +              simpset() addsimps [real_divide_def, power_inverse])); 
   12.42  by (asm_simp_tac (simpset() addsimps [inverse_eq_divide,
   12.43                                        pos_divide_less_eq]) 1); 
   12.44  qed "LIMSEQ_divide_realpow_zero";
   12.45 @@ -1289,7 +1292,7 @@
   12.46  Goal "abs(c) < 1 ==> (%n. c ^ n) ----> 0";
   12.47  by (rtac (LIMSEQ_rabs_zero RS iffD1) 1);
   12.48  by (auto_tac (claset() addIs [LIMSEQ_rabs_realpow_zero],
   12.49 -              simpset() addsimps [realpow_abs]));
   12.50 +              simpset() addsimps [power_abs]));
   12.51  qed "LIMSEQ_rabs_realpow_zero2";
   12.52  
   12.53  Goal "abs(c) < 1 ==> (%n. c ^ n) ----NS> 0";
    13.1 --- a/src/HOL/Hyperreal/Series.ML	Fri Jan 09 01:28:24 2004 +0100
    13.2 +++ b/src/HOL/Hyperreal/Series.ML	Fri Jan 09 10:46:18 2004 +0100
    13.3 @@ -575,7 +575,7 @@
    13.4      summable_comparison_test 1);
    13.5  by (res_inst_tac [("x","N")] exI 1 THEN Step_tac 1);
    13.6  by (dtac (le_Suc_ex_iff RS iffD1) 1);
    13.7 -by (auto_tac (claset(),simpset() addsimps [realpow_add, realpow_not_zero]));
    13.8 +by (auto_tac (claset(),simpset() addsimps [power_add, realpow_not_zero]));
    13.9  by (induct_tac "na" 1 THEN Auto_tac);
   13.10  by (res_inst_tac [("y","c*abs(f(N + n))")] order_trans 1);
   13.11  by (auto_tac (claset() addIs [mult_right_mono],
    14.1 --- a/src/HOL/Hyperreal/Transcendental.ML	Fri Jan 09 01:28:24 2004 +0100
    14.2 +++ b/src/HOL/Hyperreal/Transcendental.ML	Fri Jan 09 10:46:18 2004 +0100
    14.3 @@ -15,7 +15,7 @@
    14.4  val mult_less_cancel_left = thm"mult_less_cancel_left";
    14.5  
    14.6  Goalw [root_def] "root (Suc n) 0 = 0";
    14.7 -by (safe_tac (claset() addSIs [some_equality,realpow_zero] 
    14.8 +by (safe_tac (claset() addSIs [some_equality,power_0_Suc] 
    14.9      addSEs [realpow_zero_zero]));
   14.10  qed "real_root_zero";
   14.11  Addsimps [real_root_zero];
   14.12 @@ -34,7 +34,7 @@
   14.13  Goalw [root_def] 
   14.14       "0 < x ==> root(Suc n) (x ^ (Suc n)) = x";
   14.15  by (rtac some_equality 1);
   14.16 -by (forw_inst_tac [("n","n")] realpow_gt_zero 2);
   14.17 +by (forw_inst_tac [("n","n")] zero_less_power 2);
   14.18  by (auto_tac (claset(),simpset() addsimps [zero_less_mult_iff]));
   14.19  by (res_inst_tac [("R1.0","u"),("R2.0","x")] real_linear_less2 1);
   14.20  by (dres_inst_tac [("n1","n"),("x","u")] (zero_less_Suc RSN  (3, realpow_less)) 1);
   14.21 @@ -52,7 +52,7 @@
   14.22  by (dres_inst_tac [("n","n")] realpow_pos_nth2 1);
   14.23  by (Safe_tac THEN rtac someI2 1);
   14.24  by (auto_tac (claset() addSIs [order_less_imp_le] 
   14.25 -    addDs [realpow_gt_zero],simpset() addsimps [zero_less_mult_iff]));
   14.26 +    addDs [zero_less_power],simpset() addsimps [zero_less_mult_iff]));
   14.27  qed "real_root_pos_pos";
   14.28  
   14.29  Goal "0 <= x ==> 0 <= root(Suc n) x";
   14.30 @@ -66,7 +66,7 @@
   14.31  by (rtac ccontr 1);
   14.32  by (res_inst_tac [("R1.0","u"),("R2.0","1")] real_linear_less2 1);
   14.33  by (dres_inst_tac [("n","n")] realpow_Suc_less_one 1);
   14.34 -by (dres_inst_tac [("n","n")] realpow_Suc_gt_one 4);
   14.35 +by (dres_inst_tac [("n","n")] power_gt1_lemma 4);
   14.36  by (auto_tac (claset(),simpset() addsimps [real_less_not_refl]));
   14.37  qed "real_root_one";
   14.38  Addsimps [real_root_one];
   14.39 @@ -171,8 +171,8 @@
   14.40  by (Asm_full_simp_tac 1 THEN Asm_full_simp_tac 1);
   14.41  by (res_inst_tac [("a","xa * x")] someI2 1);
   14.42  by (auto_tac (claset() addEs [real_less_asym],
   14.43 -    simpset() addsimps mult_ac@[realpow_mult RS sym,realpow_two_disj,
   14.44 -    realpow_gt_zero, real_mult_order] delsimps [realpow_Suc]));
   14.45 +    simpset() addsimps mult_ac@[power_mult_distrib RS sym,realpow_two_disj,
   14.46 +    zero_less_power, real_mult_order] delsimps [realpow_Suc]));
   14.47  qed "real_sqrt_mult_distrib";
   14.48  
   14.49  Goal "[|0<=x; 0<=y |] ==> sqrt(x*y) =  sqrt(x) * sqrt(y)";
   14.50 @@ -240,8 +240,7 @@
   14.51  qed "real_sqrt_not_eq_zero";
   14.52  
   14.53  Goal "0 < x ==> inverse (sqrt(x)) ^ 2 = inverse x";
   14.54 -by (ftac real_sqrt_not_eq_zero 1);
   14.55 -by (cut_inst_tac [("n1","2"),("r1","sqrt x")] (realpow_inverse RS sym) 1);
   14.56 +by (cut_inst_tac [("n1","2"),("a1","sqrt x")] (power_inverse RS sym) 1);
   14.57  by (auto_tac (claset() addDs [real_sqrt_gt_zero_pow2],simpset()));
   14.58  qed "real_inv_sqrt_pow2";
   14.59  
   14.60 @@ -320,7 +319,7 @@
   14.61      summable_comparison_test 1);
   14.62  by (rtac summable_exp 2);
   14.63  by (res_inst_tac [("x","0")] exI 1);
   14.64 -by (auto_tac (claset(), simpset() addsimps [realpow_abs RS sym,
   14.65 +by (auto_tac (claset(), simpset() addsimps [power_abs RS sym,
   14.66      abs_mult,zero_le_mult_iff]));
   14.67  by (auto_tac (claset() addIs [mult_right_mono],
   14.68      simpset() addsimps [positive_imp_inverse_positive,abs_eqI2]));
   14.69 @@ -334,7 +333,7 @@
   14.70      summable_comparison_test 1);
   14.71  by (rtac summable_exp 2);
   14.72  by (res_inst_tac [("x","0")] exI 1);
   14.73 -by (auto_tac (claset(), simpset() addsimps [realpow_abs RS sym,abs_mult,
   14.74 +by (auto_tac (claset(), simpset() addsimps [power_abs RS sym,abs_mult,
   14.75      zero_le_mult_iff]));
   14.76  by (auto_tac (claset() addSIs [mult_right_mono],
   14.77      simpset() addsimps [positive_imp_inverse_positive,abs_eqI2]));
   14.78 @@ -426,7 +425,7 @@
   14.79  \     sumr 0 (Suc n) (%p. (x ^ (n - p)) * (y ^ p))";
   14.80  by (case_tac "x = y" 1);
   14.81  by (auto_tac (claset(),simpset() addsimps [real_mult_commute,
   14.82 -    realpow_add RS sym] delsimps [sumr_Suc]));
   14.83 +    power_add RS sym] delsimps [sumr_Suc]));
   14.84  by (res_inst_tac [("c1","x - y")] (real_mult_left_cancel RS iffD1) 1);
   14.85  by (rtac (minus_minus RS subst) 2);
   14.86  by (stac minus_mult_left 2);
   14.87 @@ -454,26 +453,26 @@
   14.88  by (res_inst_tac [("z","abs (x ^ n)")] (CLAIM_SIMP 
   14.89      "[| (0::real) <z; x*z<=y*z |] ==> x<=y" [mult_le_cancel_left]) 1);
   14.90  by (auto_tac (claset(),
   14.91 -    simpset() addsimps [mult_assoc,realpow_abs]));
   14.92 +    simpset() addsimps [mult_assoc,power_abs]));
   14.93  by (dres_inst_tac [("x","0")] spec 2 THEN Force_tac 2); 
   14.94 -by (auto_tac (claset(),simpset() addsimps [abs_mult,realpow_abs] @ mult_ac));
   14.95 +by (auto_tac (claset(),simpset() addsimps [abs_mult,power_abs] @ mult_ac));
   14.96  by (res_inst_tac [("a2","z ^ n")] (abs_ge_zero RS real_le_imp_less_or_eq
   14.97      RS disjE) 1 THEN dtac sym 2);
   14.98  by (auto_tac (claset() addSIs [mult_right_mono],
   14.99 -    simpset() addsimps [mult_assoc RS sym, realpow_abs,summable_def]));
  14.100 +    simpset() addsimps [mult_assoc RS sym, power_abs,summable_def, power_0_left]));
  14.101  by (res_inst_tac [("x","K * inverse(1 - (abs(z) * inverse(abs x)))")] exI 1);
  14.102  by (auto_tac (claset() addSIs [sums_mult],simpset() addsimps [mult_assoc]));
  14.103  by (subgoal_tac 
  14.104      "abs(z ^ n) * inverse(abs x ^ n) = (abs(z) * inverse(abs x)) ^ n" 1);
  14.105 -by (auto_tac (claset(),simpset() addsimps [realpow_abs RS sym]));
  14.106 +by (auto_tac (claset(),simpset() addsimps [power_abs RS sym]));
  14.107  by (subgoal_tac "x ~= 0" 1);
  14.108  by (subgoal_tac "x ~= 0" 3);
  14.109  by (auto_tac (claset(),
  14.110       simpset() delsimps [abs_inverse, abs_mult]
  14.111        addsimps [abs_inverse RS sym, realpow_not_zero, abs_mult RS sym,
  14.112 -    realpow_inverse, realpow_mult RS sym]));
  14.113 +    power_inverse, power_mult_distrib RS sym]));
  14.114  by (auto_tac (claset() addSIs [geometric_sums],
  14.115 -       simpset() addsimps [realpow_abs, inverse_eq_divide]));
  14.116 +       simpset() addsimps [power_abs, inverse_eq_divide]));
  14.117  by (res_inst_tac [("z","abs(x)")] (CLAIM_SIMP 
  14.118      "[|(0::real)<z; x*z<y*z |] ==> x<y" [mult_less_cancel_left]) 1);
  14.119  by (auto_tac (claset(),simpset() addsimps [abs_mult RS sym,mult_assoc]));
  14.120 @@ -483,7 +482,7 @@
  14.121  \     ==> summable (%n. f(n) * (z ^ n))";
  14.122  by (dres_inst_tac [("z","abs z")] powser_insidea 1);
  14.123  by (auto_tac (claset() addIs [summable_rabs_cancel],
  14.124 -    simpset() addsimps [realpow_abs RS sym]));
  14.125 +    simpset() addsimps [power_abs RS sym]));
  14.126  qed "powser_inside";
  14.127  
  14.128  (* ------------------------------------------------------------------------ *)
  14.129 @@ -538,7 +537,7 @@
  14.130  \       (((z + h) ^ (m - p)) - (z ^ (m - p))))";
  14.131  by (rtac sumr_subst 1);
  14.132  by (auto_tac (claset(),simpset() addsimps [right_distrib,
  14.133 -    real_diff_def,realpow_add RS sym] 
  14.134 +    real_diff_def,power_add RS sym] 
  14.135      @ mult_ac));
  14.136  qed "lemma_termdiff1";
  14.137  
  14.138 @@ -588,23 +587,23 @@
  14.139  by (auto_tac (claset() addSIs [sumr_bound2],simpset() addsimps [abs_mult]));
  14.140  by (case_tac "n" 1 THEN Auto_tac);
  14.141  by (dtac less_add_one 1);
  14.142 -by (auto_tac (claset(),simpset() addsimps [realpow_add,real_add_assoc RS sym,
  14.143 +by (auto_tac (claset(),simpset() addsimps [power_add,real_add_assoc RS sym,
  14.144      CLAIM_SIMP "(a * b) * c = a * (c * (b::real))" mult_ac] 
  14.145      delsimps [sumr_Suc]));
  14.146  by (auto_tac (claset() addSIs [mult_mono],simpset()delsimps [sumr_Suc])); 
  14.147 -by (auto_tac (claset() addSIs [realpow_le2],simpset() addsimps 
  14.148 -    [realpow_abs] delsimps [sumr_Suc] ));
  14.149 +by (auto_tac (claset() addSIs [power_mono],
  14.150 +            simpset() addsimps [power_abs] delsimps [sumr_Suc] ));
  14.151  by (res_inst_tac [("j","real (Suc d) * (K ^ d)")] real_le_trans 1);
  14.152  by (subgoal_tac "0 <= K" 2);
  14.153  by (arith_tac 3);
  14.154 -by (dres_inst_tac [("n","d")] realpow_ge_zero2 2);
  14.155 +by (dres_inst_tac [("n","d")] zero_le_power 2);
  14.156  by (auto_tac (claset(),simpset() delsimps [sumr_Suc] ));
  14.157  by (rtac (sumr_rabs RS real_le_trans) 1);
  14.158  by (rtac sumr_bound2 1 THEN 
  14.159      auto_tac (claset() addSDs [less_add_one]
  14.160 -    addSIs [mult_mono], simpset() addsimps [abs_mult, realpow_add]));
  14.161 -by (auto_tac (claset() addSIs [realpow_le2,realpow_ge_zero],simpset() addsimps 
  14.162 -    [realpow_abs]));
  14.163 +    addSIs [mult_mono], simpset() addsimps [abs_mult, power_add]));
  14.164 +by (auto_tac (claset() addSIs [power_mono,zero_le_power],
  14.165 +              simpset() addsimps [power_abs]));
  14.166  by (ALLGOALS(arith_tac));
  14.167  qed "lemma_termdiff3";
  14.168  
  14.169 @@ -956,8 +955,8 @@
  14.170  by (rtac real_le_trans 1);
  14.171  by (res_inst_tac [("n","2"),("f","(%n. inverse (real (fact n)) * x ^ n)")]
  14.172      series_pos_le 2);
  14.173 -by (auto_tac (claset() addIs [summable_exp],simpset() 
  14.174 -    addsimps [numeral_2_eq_2,realpow_ge_zero,zero_le_mult_iff]));
  14.175 +by (auto_tac (claset() addIs [summable_exp],simpset()
  14.176 +    addsimps [numeral_2_eq_2,zero_le_power,zero_le_mult_iff]));
  14.177  qed "exp_ge_add_one_self";
  14.178  Addsimps [exp_ge_add_one_self];
  14.179  
  14.180 @@ -1233,8 +1232,8 @@
  14.181  (* ------------------------------------------------------------------------ *)
  14.182  
  14.183  Goalw [sin_def] "sin 0 = 0";
  14.184 -by (auto_tac (claset() addSIs [(sums_unique RS sym),
  14.185 -    LIMSEQ_const],simpset() addsimps [sums_def]));
  14.186 +by (auto_tac (claset() addSIs [sums_unique RS sym, LIMSEQ_const],
  14.187 +              simpset() addsimps [sums_def] delsimps [power_0_left]));
  14.188  qed "sin_zero";
  14.189  Addsimps [sin_zero];
  14.190  
  14.191 @@ -1361,7 +1360,7 @@
  14.192  
  14.193  Goalw [real_le_def] "abs(sin x) <= 1";
  14.194  by (rtac notI 1);
  14.195 -by (dtac realpow_two_gt_one 1);
  14.196 +by (dres_inst_tac [("n","Suc 0")] power_gt1 1); 
  14.197  by (auto_tac (claset(),simpset() delsimps [realpow_Suc]));
  14.198  by (dres_inst_tac [("r1","cos x")] (realpow_two_le RSN 
  14.199      (2, real_gt_one_ge_zero_add_less)) 1);
  14.200 @@ -1389,7 +1388,7 @@
  14.201  
  14.202  Goalw [real_le_def] "abs(cos x) <= 1";
  14.203  by (rtac notI 1);
  14.204 -by (dtac realpow_two_gt_one 1);
  14.205 +by (dres_inst_tac [("n","Suc 0")] power_gt1 1); 
  14.206  by (auto_tac (claset(),simpset() delsimps [realpow_Suc]));
  14.207  by (dres_inst_tac [("r1","sin x")] (realpow_two_le RSN 
  14.208      (2, real_gt_one_ge_zero_add_less)) 1);
  14.209 @@ -1606,7 +1605,7 @@
  14.210          CLAIM "x * (x * x ^ (4*m)) = (x ^ (4*m)) * (x * (x::real))"] 
  14.211      delsimps [fact_Suc]));
  14.212  by (subgoal_tac "0 < x ^ (4 * m)" 1);
  14.213 -by (asm_simp_tac (simpset() addsimps [realpow_gt_zero]) 2); 
  14.214 +by (asm_simp_tac (simpset() addsimps [zero_less_power]) 2); 
  14.215  by (asm_simp_tac (simpset() addsimps [mult_less_cancel_left]) 1); 
  14.216  by (rtac real_mult_less_mono 1); (*mult_strict_mono would be stronger*)
  14.217  by (ALLGOALS(Asm_simp_tac));
  14.218 @@ -1624,7 +1623,7 @@
  14.219  by (auto_tac (claset(),
  14.220      simpset() addsimps [cos_squared_eq,
  14.221      minus_add_distrib RS sym, neg_less_0_iff_less,sin_gt_zero1,
  14.222 -    real_add_order,realpow_gt_zero,cos_double] 
  14.223 +    real_add_order,zero_less_power,cos_double] 
  14.224      delsimps [realpow_Suc,minus_add_distrib]));
  14.225  qed "cos_double_less_one";
  14.226  
  14.227 @@ -1635,7 +1634,7 @@
  14.228  by (auto_tac (claset(),simpset() addsimps  mult_ac@[cos_def]));
  14.229  qed "cos_paired";
  14.230  
  14.231 -Addsimps [realpow_gt_zero];
  14.232 +Addsimps [zero_less_power];
  14.233  
  14.234  Goal "cos (2) < 0";
  14.235  by (cut_inst_tac [("x","2")] cos_paired 1);
  14.236 @@ -2376,11 +2375,11 @@
  14.237  Addsimps [cos_arctan_not_zero];
  14.238  
  14.239  Goal "cos x ~= 0 ==> 1 + tan(x) ^ 2 = inverse(cos x) ^ 2";
  14.240 -by (rtac (realpow_inverse RS subst) 1);
  14.241 +by (rtac (power_inverse RS subst) 1);
  14.242  by (res_inst_tac [("c1","cos(x) ^ 2")] (real_mult_right_cancel RS iffD1) 1);
  14.243  by (auto_tac (claset() addDs [realpow_not_zero], simpset() addsimps
  14.244 -    [realpow_mult,left_distrib,realpow_divide,
  14.245 -     tan_def,real_mult_assoc,realpow_inverse RS sym] 
  14.246 +    [power_mult_distrib,left_distrib,realpow_divide,
  14.247 +     tan_def,real_mult_assoc,power_inverse RS sym] 
  14.248       delsimps [realpow_Suc]));
  14.249  qed "tan_sec";
  14.250  
  14.251 @@ -2430,7 +2429,7 @@
  14.252  
  14.253  Goal "cos (2 * real (n::nat) * pi) = 1";
  14.254  by (auto_tac (claset(),simpset() addsimps [cos_double,
  14.255 -    real_mult_assoc,realpow_add RS sym,numeral_2_eq_2]));
  14.256 +    real_mult_assoc,power_add RS sym,numeral_2_eq_2]));
  14.257    (*FIXME: just needs x^n for literals!*)
  14.258  qed "cos_2npi";
  14.259  Addsimps [cos_2npi];
  14.260 @@ -2584,14 +2583,14 @@
  14.261  \     ==> root(Suc n) (x * y) = root(Suc n) x * root(Suc n) y";
  14.262  by (rtac real_root_pos_unique 1);
  14.263  by (auto_tac (claset() addSIs [real_root_pos_pos_le],simpset() 
  14.264 -    addsimps [realpow_mult,zero_le_mult_iff,
  14.265 +    addsimps [power_mult_distrib,zero_le_mult_iff,
  14.266      real_root_pow_pos2] delsimps [realpow_Suc]));
  14.267  qed "real_root_mult";
  14.268  
  14.269  Goal "0 <= x ==> (root(Suc n) (inverse x) = inverse(root(Suc n) x))";
  14.270  by (rtac real_root_pos_unique 1);
  14.271  by (auto_tac (claset() addIs [real_root_pos_pos_le],simpset() 
  14.272 -    addsimps [realpow_inverse RS sym,real_root_pow_pos2] 
  14.273 +    addsimps [power_inverse RS sym,real_root_pow_pos2] 
  14.274      delsimps [realpow_Suc]));
  14.275  qed "real_root_inverse";
  14.276  
  14.277 @@ -3035,8 +3034,8 @@
  14.278  by (rtac add_mono 1);
  14.279  by (auto_tac (claset(),simpset() delsimps [realpow_Suc]));
  14.280  by (ALLGOALS(rtac ((CLAIM "(2::real) ^ 2 = 4") RS subst)));
  14.281 -by (ALLGOALS(rtac (realpow_mult RS subst)));
  14.282 -by (ALLGOALS(rtac realpow_le));
  14.283 +by (ALLGOALS(rtac (power_mult_distrib RS subst)));
  14.284 +by (ALLGOALS(rtac power_mono));
  14.285  by Auto_tac;
  14.286  qed "lemma_sqrt_hcomplex_capprox";
  14.287  
    15.1 --- a/src/HOL/Integ/Int.thy	Fri Jan 09 01:28:24 2004 +0100
    15.2 +++ b/src/HOL/Integ/Int.thy	Fri Jan 09 10:46:18 2004 +0100
    15.3 @@ -148,6 +148,7 @@
    15.4  instance int :: ordered_ring
    15.5  proof
    15.6    fix i j k :: int
    15.7 +  show "0 < (1::int)" by (rule int_0_less_1)
    15.8    show "i \<le> j ==> k + i \<le> k + j" by simp
    15.9    show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: zmult_zless_mono2)
   15.10    show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
    16.1 --- a/src/HOL/Integ/IntDef.thy	Fri Jan 09 01:28:24 2004 +0100
    16.2 +++ b/src/HOL/Integ/IntDef.thy	Fri Jan 09 10:46:18 2004 +0100
    16.3 @@ -344,7 +344,8 @@
    16.4    show "i * j = j * i" by (rule zmult_commute)
    16.5    show "1 * i = i" by simp
    16.6    show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
    16.7 -  show "0 \<noteq> (1::int)" by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq)
    16.8 +  show "0 \<noteq> (1::int)" 
    16.9 +    by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq)
   16.10    assume eq: "k+i = k+j" 
   16.11      hence "(-k + k) + i = (-k + k) + j" by (simp only: eq zadd_assoc)
   16.12      thus "i = j" by simp
    17.1 --- a/src/HOL/Integ/IntPower.thy	Fri Jan 09 01:28:24 2004 +0100
    17.2 +++ b/src/HOL/Integ/IntPower.thy	Fri Jan 09 10:46:18 2004 +0100
    17.3 @@ -15,6 +15,15 @@
    17.4    power_Suc: "p ^ (Suc n) = (p::int) * (p ^ n)"
    17.5  
    17.6  
    17.7 +instance int :: ringpower
    17.8 +proof
    17.9 +  fix z :: int
   17.10 +  fix n :: nat
   17.11 +  show "z^0 = 1" by simp
   17.12 +  show "z^(Suc n) = z * (z^n)" by simp
   17.13 +qed
   17.14 +
   17.15 +
   17.16  lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
   17.17  apply (induct_tac "y", auto)
   17.18  apply (rule zmod_zmult1_eq [THEN trans])
   17.19 @@ -22,27 +31,11 @@
   17.20  apply (rule zmod_zmult_distrib [symmetric])
   17.21  done
   17.22  
   17.23 -lemma zpower_1 [simp]: "1^y = (1::int)"
   17.24 -by (induct_tac "y", auto)
   17.25 -
   17.26 -lemma zpower_zmult_distrib: "(x*z)^y = ((x^y)*(z^y)::int)"
   17.27 -by (induct_tac "y", auto)
   17.28 -
   17.29  lemma zpower_zadd_distrib: "x^(y+z) = ((x^y)*(x^z)::int)"
   17.30 -by (induct_tac "y", auto)
   17.31 +  by (rule Power.power_add)
   17.32  
   17.33  lemma zpower_zpower: "(x^y)^z = (x^(y*z)::int)"
   17.34 -apply (induct_tac "y", auto)
   17.35 -apply (subst zpower_zmult_distrib)
   17.36 -apply (subst zpower_zadd_distrib)
   17.37 -apply (simp (no_asm_simp))
   17.38 -done
   17.39 -
   17.40 -
   17.41 -(*** Logical equivalences for inequalities ***)
   17.42 -
   17.43 -lemma zpower_eq_0_iff [simp]: "(x^n = 0) = (x = (0::int) & 0<n)"
   17.44 -by (induct_tac "n", auto)
   17.45 +  by (rule Power.power_mult [symmetric])
   17.46  
   17.47  lemma zero_less_zpower_abs_iff [simp]:
   17.48       "(0 < (abs x)^n) = (x \<noteq> (0::int) | n=0)"
   17.49 @@ -58,11 +51,8 @@
   17.50  ML
   17.51  {*
   17.52  val zpower_zmod = thm "zpower_zmod";
   17.53 -val zpower_1 = thm "zpower_1";
   17.54 -val zpower_zmult_distrib = thm "zpower_zmult_distrib";
   17.55  val zpower_zadd_distrib = thm "zpower_zadd_distrib";
   17.56  val zpower_zpower = thm "zpower_zpower";
   17.57 -val zpower_eq_0_iff = thm "zpower_eq_0_iff";
   17.58  val zero_less_zpower_abs_iff = thm "zero_less_zpower_abs_iff";
   17.59  val zero_le_zpower_abs = thm "zero_le_zpower_abs";
   17.60  *}
    18.1 --- a/src/HOL/IsaMakefile	Fri Jan 09 01:28:24 2004 +0100
    18.2 +++ b/src/HOL/IsaMakefile	Fri Jan 09 10:46:18 2004 +0100
    18.3 @@ -93,7 +93,7 @@
    18.4    Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
    18.5    Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy Nat.ML \
    18.6    Nat.thy NatArith.ML NatArith.thy Numeral.thy \
    18.7 -  Power.ML Power.thy PreList.thy Product_Type.ML Product_Type.thy ROOT.ML \
    18.8 +  Power.thy PreList.thy Product_Type.ML Product_Type.thy ROOT.ML \
    18.9    Recdef.thy Record.thy Relation.ML Relation.thy Relation_Power.ML \
   18.10    Relation_Power.thy Ring_and_Field.thy\
   18.11    Set.ML Set.thy SetInterval.ML SetInterval.thy \
   18.12 @@ -152,8 +152,7 @@
   18.13    Hyperreal/HyperArith0.thy Hyperreal/HyperArith.thy\
   18.14    Hyperreal/HyperBin.ML Hyperreal/HyperBin.thy \
   18.15    Hyperreal/HyperDef.thy Hyperreal/HyperNat.ML Hyperreal/HyperNat.thy\
   18.16 -  Hyperreal/HyperOrd.thy Hyperreal/HyperPow.ML\
   18.17 -  Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\
   18.18 +  Hyperreal/HyperOrd.thy Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\
   18.19    Hyperreal/Lim.ML Hyperreal/Lim.thy  Hyperreal/Log.ML Hyperreal/Log.thy\
   18.20    Hyperreal/MacLaurin.ML Hyperreal/MacLaurin.thy\
   18.21    Hyperreal/NatStar.ML Hyperreal/NatStar.thy\
    19.1 --- a/src/HOL/Library/Rational_Numbers.thy	Fri Jan 09 01:28:24 2004 +0100
    19.2 +++ b/src/HOL/Library/Rational_Numbers.thy	Fri Jan 09 10:46:18 2004 +0100
    19.3 @@ -514,8 +514,7 @@
    19.4      by (induct q, induct r)
    19.5         (simp add: mult_rat divide_rat inverse_rat zero_rat eq_rat)
    19.6    show "0 \<noteq> (1::rat)"
    19.7 -    by (simp add: zero_rat_def one_rat_def rat_of_equality 
    19.8 -                  zero_fraction_def one_fraction_def) 
    19.9 +    by (simp add: zero_rat one_rat eq_rat) 
   19.10    assume eq: "s+q = s+r" 
   19.11      hence "(-s + s) + q = (-s + s) + r" by (simp only: eq rat_add_assoc)
   19.12      thus "q = r" by (simp add: rat_left_minus rat_add_0)
   19.13 @@ -592,6 +591,8 @@
   19.14  instance rat :: ordered_field
   19.15  proof
   19.16    fix q r s :: rat
   19.17 +  show "0 < (1::rat)" 
   19.18 +    by (simp add: zero_rat one_rat less_rat) 
   19.19    show "q \<le> r ==> s + q \<le> s + r"
   19.20    proof (induct q, induct r, induct s)
   19.21      fix a b c d e f :: int
    20.1 --- a/src/HOL/Nat.thy	Fri Jan 09 01:28:24 2004 +0100
    20.2 +++ b/src/HOL/Nat.thy	Fri Jan 09 10:46:18 2004 +0100
    20.3 @@ -771,6 +771,7 @@
    20.4  instance nat :: ordered_semiring
    20.5  proof
    20.6    fix i j k :: nat
    20.7 +  show "0 < (1::nat)" by simp
    20.8    show "i \<le> j ==> k + i \<le> k + j" by simp
    20.9    show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2)
   20.10  qed
    21.1 --- a/src/HOL/NumberTheory/EvenOdd.thy	Fri Jan 09 01:28:24 2004 +0100
    21.2 +++ b/src/HOL/NumberTheory/EvenOdd.thy	Fri Jan 09 10:46:18 2004 +0100
    21.3 @@ -173,7 +173,7 @@
    21.4        also have "(-1::int)^2 = 1";
    21.5          by auto
    21.6        finally; show ?thesis;
    21.7 -        by (auto simp add: zpower_1)
    21.8 +        by auto
    21.9      qed;
   21.10  qed;
   21.11  
   21.12 @@ -199,7 +199,7 @@
   21.13        also have "(-1::int)^2 = 1";
   21.14          by auto
   21.15        finally; show ?thesis;
   21.16 -        by (auto simp add: zpower_1)
   21.17 +        by auto
   21.18      qed;
   21.19  qed;
   21.20  
    22.1 --- a/src/HOL/Power.ML	Fri Jan 09 01:28:24 2004 +0100
    22.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.3 @@ -1,191 +0,0 @@
    22.4 -(*  Title:      HOL/Power.ML
    22.5 -    ID:         $Id$
    22.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    22.7 -    Copyright   1997  University of Cambridge
    22.8 -
    22.9 -The (overloaded) exponentiation operator, ^ :: [nat,nat]=>nat
   22.10 -Also binomial coefficents
   22.11 -*)
   22.12 -
   22.13 -(*** Simple laws about Power ***)
   22.14 -
   22.15 -Goal "!!i::nat. i ^ (j+k) = (i^j) * (i^k)";
   22.16 -by (induct_tac "k" 1);
   22.17 -by (ALLGOALS (asm_simp_tac (simpset() addsimps mult_ac)));
   22.18 -qed "power_add";
   22.19 -
   22.20 -Goal "!!i::nat. i ^ (j*k) = (i^j) ^ k";
   22.21 -by (induct_tac "k" 1);
   22.22 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [power_add])));
   22.23 -qed "power_mult";
   22.24 -
   22.25 -Goal "!!i::nat. 0 < i ==> 0 < i^n";
   22.26 -by (induct_tac "n" 1);
   22.27 -by (ALLGOALS Asm_simp_tac);
   22.28 -qed "zero_less_power";
   22.29 -Addsimps [zero_less_power];
   22.30 -
   22.31 -Goal "i^n = 0 ==> i = (0::nat)";
   22.32 -by (etac contrapos_pp 1); 
   22.33 -by Auto_tac;  
   22.34 -qed "power_eq_0D";
   22.35 -
   22.36 -Goal "!!i::nat. 1 <= i ==> Suc 0 <= i^n";
   22.37 -by (induct_tac "n" 1);
   22.38 -by Auto_tac;
   22.39 -qed "one_le_power";
   22.40 -Addsimps [one_le_power];
   22.41 -
   22.42 -Goal "!!i::nat. 1 < i ==> !m. (i^n = i^m) = (n=m)";
   22.43 -by (induct_tac "n" 1);
   22.44 -by Auto_tac;
   22.45 -by (ALLGOALS (case_tac "m"));
   22.46 -by (Simp_tac 1);
   22.47 -by Auto_tac;
   22.48 -qed_spec_mp "power_inject";
   22.49 -Addsimps [power_inject];
   22.50 -
   22.51 -Goalw [dvd_def] "!!i::nat. m<=n ==> i^m dvd i^n";
   22.52 -by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
   22.53 -by (asm_simp_tac (simpset() addsimps [power_add]) 1);
   22.54 -qed "le_imp_power_dvd";
   22.55 -
   22.56 -Goal "(1::nat) < i ==> \\<forall>n. i ^ m <= i ^ n --> m <= n";
   22.57 -by (induct_tac "m" 1);
   22.58 -by Auto_tac;  
   22.59 -by (case_tac "na" 1); 
   22.60 -by Auto_tac;
   22.61 -by (subgoal_tac "Suc 1 * 1 <= i * i^n" 1);
   22.62 -by (Asm_full_simp_tac 1); 
   22.63 -by (rtac mult_le_mono 1);
   22.64 -by Auto_tac;   
   22.65 -qed_spec_mp "power_le_imp_le";
   22.66 -
   22.67 -Goal "!!i::nat. [| 0 < i; i^m < i^n |] ==> m < n";
   22.68 -by (rtac ccontr 1);
   22.69 -by (dtac (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1);
   22.70 -by (etac zero_less_power 1);
   22.71 -by (contr_tac 1);
   22.72 -qed "power_less_imp_less";
   22.73 -
   22.74 -Goal "k^j dvd n --> i<=j --> k^i dvd (n::nat)";
   22.75 -by (induct_tac "j" 1);
   22.76 -by (ALLGOALS (simp_tac (simpset() addsimps [le_Suc_eq])));
   22.77 -by (blast_tac (claset() addSDs [dvd_mult_right]) 1);
   22.78 -qed_spec_mp "power_le_dvd";
   22.79 -
   22.80 -Goal "[|i^m dvd i^n;  (1::nat) < i|] ==> m <= n";
   22.81 -by (rtac power_le_imp_le 1); 
   22.82 -by (assume_tac 1); 
   22.83 -by (etac dvd_imp_le 1); 
   22.84 -by (Asm_full_simp_tac 1); 
   22.85 -qed "power_dvd_imp_le";
   22.86 -
   22.87 -
   22.88 -(*** Logical equivalences for inequalities ***)
   22.89 -
   22.90 -Goal "(x^n = 0) = (x = (0::nat) & 0<n)";
   22.91 -by (induct_tac "n" 1);
   22.92 -by Auto_tac; 
   22.93 -qed "power_eq_0_iff";
   22.94 -Addsimps [power_eq_0_iff];
   22.95 -
   22.96 -Goal "(0 < x^n) = (x ~= (0::nat) | n=0)";
   22.97 -by (induct_tac "n" 1);
   22.98 -by Auto_tac; 
   22.99 -qed "zero_less_power_iff";
  22.100 -Addsimps [zero_less_power_iff];
  22.101 -
  22.102 -Goal "(0::nat) <= x^n";
  22.103 -by (induct_tac "n" 1);
  22.104 -by Auto_tac; 
  22.105 -qed "zero_le_power";
  22.106 -Addsimps [zero_le_power];
  22.107 -
  22.108 -
  22.109 -(**** Binomial Coefficients, following Andy Gordon and Florian Kammueller ****)
  22.110 -
  22.111 -Goal "(n choose 0) = 1";
  22.112 -by (case_tac "n" 1);
  22.113 -by (ALLGOALS Asm_simp_tac);
  22.114 -qed "binomial_n_0";
  22.115 -
  22.116 -Goal "(0 choose Suc k) = 0";
  22.117 -by (Simp_tac 1);
  22.118 -qed "binomial_0_Suc";
  22.119 -
  22.120 -Goal "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)";
  22.121 -by (Simp_tac 1);
  22.122 -qed "binomial_Suc_Suc";
  22.123 -
  22.124 -Goal "ALL k. n < k --> (n choose k) = 0";
  22.125 -by (induct_tac "n" 1);
  22.126 -by Auto_tac;
  22.127 -by (etac allE 1);
  22.128 -by (etac mp 1);
  22.129 -by (arith_tac 1);
  22.130 -qed_spec_mp "binomial_eq_0";
  22.131 -
  22.132 -Addsimps [binomial_n_0, binomial_0_Suc, binomial_Suc_Suc];
  22.133 -Delsimps [binomial_0, binomial_Suc];
  22.134 -
  22.135 -Goal "(n choose n) = 1";
  22.136 -by (induct_tac "n" 1);
  22.137 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [binomial_eq_0])));
  22.138 -qed "binomial_n_n";
  22.139 -Addsimps [binomial_n_n];
  22.140 -
  22.141 -Goal "(Suc n choose n) = Suc n";
  22.142 -by (induct_tac "n" 1);
  22.143 -by (ALLGOALS Asm_simp_tac);
  22.144 -qed "binomial_Suc_n";
  22.145 -Addsimps [binomial_Suc_n];
  22.146 -
  22.147 -Goal "(n choose Suc 0) = n";
  22.148 -by (induct_tac "n" 1);
  22.149 -by (ALLGOALS Asm_simp_tac);
  22.150 -qed "binomial_1";
  22.151 -Addsimps [binomial_1];
  22.152 -
  22.153 -Goal "k <= n --> 0 < (n choose k)";
  22.154 -by (res_inst_tac [("m","n"),("n","k")] diff_induct 1);
  22.155 -by (ALLGOALS Asm_simp_tac);
  22.156 -qed_spec_mp "zero_less_binomial";
  22.157 -
  22.158 -Goal "(n choose k = 0) = (n<k)";
  22.159 -by (safe_tac (claset() addSIs [binomial_eq_0]));
  22.160 -by (etac contrapos_pp 1);
  22.161 -by (asm_full_simp_tac (simpset() addsimps [zero_less_binomial]) 1); 
  22.162 -qed "binomial_eq_0_iff";
  22.163 -
  22.164 -Goal "(0 < n choose k) = (k<=n)";
  22.165 -by (simp_tac (simpset() addsimps [linorder_not_less RS sym, 
  22.166 -                                  binomial_eq_0_iff RS sym]) 1); 
  22.167 -qed "zero_less_binomial_iff";
  22.168 -
  22.169 -(*Might be more useful if re-oriented*)
  22.170 -Goal "ALL k. k <= n --> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k";
  22.171 -by (induct_tac "n" 1);
  22.172 -by (simp_tac (simpset() addsimps [binomial_0]) 1);
  22.173 -by (Clarify_tac 1);
  22.174 -by (case_tac "k" 1);
  22.175 -by (auto_tac (claset(),
  22.176 -	      simpset() addsimps [add_mult_distrib, add_mult_distrib2,
  22.177 -				  le_Suc_eq, binomial_eq_0]));
  22.178 -qed_spec_mp "Suc_times_binomial_eq";
  22.179 -
  22.180 -(*This is the well-known version, but it's harder to use because of the
  22.181 -  need to reason about division.*)
  22.182 -Goal "k <= n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k";
  22.183 -by (asm_simp_tac (simpset()
  22.184 -  addsimps [Suc_times_binomial_eq, div_mult_self_is_m, zero_less_Suc]
  22.185 -  delsimps [mult_Suc, mult_Suc_right]) 1);
  22.186 -qed "binomial_Suc_Suc_eq_times";
  22.187 -
  22.188 -(*Another version, with -1 instead of Suc.*)
  22.189 -Goal "[|k <= n;  0<k|] ==> (n choose k) * k = n * ((n - 1) choose (k - 1))";
  22.190 -by (cut_inst_tac [("n","n - 1"),("k","k - 1")] Suc_times_binomial_eq 1);
  22.191 -by (asm_full_simp_tac (simpset() addsplits [nat_diff_split]) 1); 
  22.192 -by Auto_tac;  
  22.193 -qed "times_binomial_minus1_eq";
  22.194 -
    23.1 --- a/src/HOL/Power.thy	Fri Jan 09 01:28:24 2004 +0100
    23.2 +++ b/src/HOL/Power.thy	Fri Jan 09 10:46:18 2004 +0100
    23.3 @@ -3,23 +3,451 @@
    23.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    23.5      Copyright   1997  University of Cambridge
    23.6  
    23.7 -The (overloaded) exponentiation operator, ^ :: [nat,nat]=>nat
    23.8 -Also binomial coefficents
    23.9  *)
   23.10  
   23.11 -Power = Divides + 
   23.12 -consts
   23.13 -  binomial :: "[nat,nat] => nat"      (infixl "choose" 65)
   23.14 +header{*Exponentiation and Binomial Coefficients*}
   23.15 +
   23.16 +theory Power = Divides:
   23.17 +
   23.18 +subsection{*Powers for Arbitrary (Semi)Rings*}
   23.19 +
   23.20 +axclass ringpower \<subseteq> semiring, power
   23.21 +  power_0 [simp]:   "a ^ 0       = 1"
   23.22 +  power_Suc: "a ^ (Suc n) = a * (a ^ n)"
   23.23 +
   23.24 +lemma power_0_Suc [simp]: "(0::'a::ringpower) ^ (Suc n) = 0"
   23.25 +by (simp add: power_Suc)
   23.26 +
   23.27 +text{*It looks plausible as a simprule, but its effect can be strange.*}
   23.28 +lemma power_0_left: "0^n = (if n=0 then 1 else (0::'a::ringpower))"
   23.29 +by (induct_tac "n", auto)
   23.30 +
   23.31 +lemma power_one [simp]: "1^n = (1::'a::ringpower)"
   23.32 +apply (induct_tac "n")
   23.33 +apply (auto simp add: power_Suc)  
   23.34 +done
   23.35 +
   23.36 +lemma power_one_right [simp]: "(a::'a::ringpower) ^ 1 = a"
   23.37 +by (simp add: power_Suc)
   23.38 +
   23.39 +lemma power_add: "(a::'a::ringpower) ^ (m+n) = (a^m) * (a^n)"
   23.40 +apply (induct_tac "n")
   23.41 +apply (simp_all add: power_Suc mult_ac)
   23.42 +done
   23.43 +
   23.44 +lemma power_mult: "(a::'a::ringpower) ^ (m*n) = (a^m) ^ n"
   23.45 +apply (induct_tac "n")
   23.46 +apply (simp_all add: power_Suc power_add)
   23.47 +done
   23.48 +
   23.49 +lemma power_mult_distrib: "((a::'a::ringpower) * b) ^ n = (a^n) * (b^n)"
   23.50 +apply (induct_tac "n") 
   23.51 +apply (auto simp add: power_Suc mult_ac)
   23.52 +done
   23.53 +
   23.54 +lemma zero_less_power:
   23.55 +     "0 < (a::'a::{ordered_semiring,ringpower}) ==> 0 < a^n"
   23.56 +apply (induct_tac "n")
   23.57 +apply (simp_all add: power_Suc zero_less_one mult_pos)
   23.58 +done
   23.59 +
   23.60 +lemma zero_le_power:
   23.61 +     "0 \<le> (a::'a::{ordered_semiring,ringpower}) ==> 0 \<le> a^n"
   23.62 +apply (simp add: order_le_less)
   23.63 +apply (erule disjE) 
   23.64 +apply (simp_all add: zero_less_power zero_less_one power_0_left)
   23.65 +done
   23.66 +
   23.67 +lemma one_le_power:
   23.68 +     "1 \<le> (a::'a::{ordered_semiring,ringpower}) ==> 1 \<le> a^n"
   23.69 +apply (induct_tac "n")
   23.70 +apply (simp_all add: power_Suc)
   23.71 +apply (rule order_trans [OF _ mult_mono [of 1 _ 1]]) 
   23.72 +apply (simp_all add: zero_le_one order_trans [OF zero_le_one]) 
   23.73 +done
   23.74 +
   23.75 +lemma gt1_imp_ge0: "1 < a ==> 0 \<le> (a::'a::ordered_semiring)"
   23.76 +  by (simp add: order_trans [OF zero_le_one order_less_imp_le])
   23.77 +
   23.78 +lemma power_gt1_lemma:
   23.79 +     assumes gt1: "1 < (a::'a::{ordered_semiring,ringpower})"
   23.80 +        shows     "1 < a * a^n"
   23.81 +proof -
   23.82 +  have "1*1 < a * a^n"
   23.83 +    proof (rule order_less_le_trans) 
   23.84 +      show "1*1 < a*1" by (simp add: gt1)
   23.85 +      show  "a*1 \<le> a * a^n"
   23.86 +   by (simp only: mult_mono gt1 gt1_imp_ge0 one_le_power order_less_imp_le 
   23.87 +                  zero_le_one order_refl)
   23.88 +    qed
   23.89 +  thus ?thesis by simp
   23.90 +qed
   23.91 +
   23.92 +lemma power_gt1:
   23.93 +     "1 < (a::'a::{ordered_semiring,ringpower}) ==> 1 < a ^ (Suc n)"
   23.94 +by (simp add: power_gt1_lemma power_Suc)
   23.95 +
   23.96 +lemma power_le_imp_le_exp:
   23.97 +     assumes gt1: "(1::'a::{ringpower,ordered_semiring}) < a"
   23.98 +       shows      "!!n. a^m \<le> a^n ==> m \<le> n"
   23.99 +proof (induct "m")
  23.100 +  case 0
  23.101 +    show ?case by simp
  23.102 +next
  23.103 +  case (Suc m)
  23.104 +    show ?case 
  23.105 +      proof (cases n)
  23.106 +        case 0
  23.107 +          from prems have "a * a^m \<le> 1" by (simp add: power_Suc)
  23.108 +          with gt1 show ?thesis
  23.109 +            by (force simp only: power_gt1_lemma 
  23.110 +                                 linorder_not_less [symmetric])
  23.111 +      next
  23.112 +        case (Suc n)
  23.113 +          from prems show ?thesis 
  23.114 +	    by (force dest: mult_left_le_imp_le
  23.115 +	          simp add: power_Suc order_less_trans [OF zero_less_one gt1]) 
  23.116 +      qed
  23.117 +qed
  23.118 +
  23.119 +text{*Surely we can strengthen this? It holds for 0<a<1 too.*}
  23.120 +lemma power_inject_exp [simp]:
  23.121 +     "1 < (a::'a::{ordered_semiring,ringpower}) ==> (a^m = a^n) = (m=n)"
  23.122 +  by (force simp add: order_antisym power_le_imp_le_exp)  
  23.123 +
  23.124 +text{*Can relax the first premise to @{term "0<a"} in the case of the
  23.125 +natural numbers.*}
  23.126 +lemma power_less_imp_less_exp:
  23.127 +     "[| (1::'a::{ringpower,ordered_semiring}) < a; a^m < a^n |] ==> m < n"
  23.128 +by (simp add: order_less_le [of m n] order_less_le [of "a^m" "a^n"] 
  23.129 +              power_le_imp_le_exp) 
  23.130 +
  23.131 +
  23.132 +lemma power_mono:
  23.133 +     "[|a \<le> b; (0::'a::{ringpower,ordered_semiring}) \<le> a|] ==> a^n \<le> b^n"
  23.134 +apply (induct_tac "n") 
  23.135 +apply (simp_all add: power_Suc)
  23.136 +apply (auto intro: mult_mono zero_le_power order_trans [of 0 a b])
  23.137 +done
  23.138 +
  23.139 +lemma power_strict_mono [rule_format]:
  23.140 +     "[|a < b; (0::'a::{ringpower,ordered_semiring}) \<le> a|] 
  23.141 +      ==> 0 < n --> a^n < b^n" 
  23.142 +apply (induct_tac "n") 
  23.143 +apply (auto simp add: mult_strict_mono zero_le_power power_Suc
  23.144 +                      order_le_less_trans [of 0 a b])
  23.145 +done
  23.146 +
  23.147 +lemma power_eq_0_iff [simp]:
  23.148 +     "(a^n = 0) = (a = (0::'a::{ordered_ring,ringpower}) & 0<n)"
  23.149 +apply (induct_tac "n")
  23.150 +apply (auto simp add: power_Suc zero_neq_one [THEN not_sym])
  23.151 +done
  23.152 +
  23.153 +lemma field_power_eq_0_iff [simp]:
  23.154 +     "(a^n = 0) = (a = (0::'a::{field,ringpower}) & 0<n)"
  23.155 +apply (induct_tac "n")
  23.156 +apply (auto simp add: power_Suc field_mult_eq_0_iff zero_neq_one[THEN not_sym])
  23.157 +done
  23.158 +
  23.159 +lemma field_power_not_zero: "a \<noteq> (0::'a::{field,ringpower}) ==> a^n \<noteq> 0"
  23.160 +by force
  23.161 +
  23.162 +text{*Perhaps these should be simprules.*}
  23.163 +lemma power_inverse:
  23.164 +  "inverse ((a::'a::{field,division_by_zero,ringpower}) ^ n) = (inverse a) ^ n"
  23.165 +apply (induct_tac "n")
  23.166 +apply (auto simp add: power_Suc inverse_mult_distrib)
  23.167 +done
  23.168 +
  23.169 +lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_field,ringpower}) ^ n"
  23.170 +apply (induct_tac "n")
  23.171 +apply (auto simp add: power_Suc abs_mult)
  23.172 +done
  23.173 +
  23.174 +lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{ring,ringpower}) ^ n"
  23.175 +proof -
  23.176 +  have "-a = (- 1) * a"  by (simp add: minus_mult_left [symmetric])
  23.177 +  thus ?thesis by (simp only: power_mult_distrib)
  23.178 +qed
  23.179 +
  23.180 +text{*Lemma for @{text power_strict_decreasing}*}
  23.181 +lemma power_Suc_less:
  23.182 +     "[|(0::'a::{ordered_semiring,ringpower}) < a; a < 1|]
  23.183 +      ==> a * a^n < a^n"
  23.184 +apply (induct_tac n) 
  23.185 +apply (auto simp add: power_Suc mult_strict_left_mono) 
  23.186 +done
  23.187 +
  23.188 +lemma power_strict_decreasing:
  23.189 +     "[|n < N; 0 < a; a < (1::'a::{ordered_semiring,ringpower})|]
  23.190 +      ==> a^N < a^n"
  23.191 +apply (erule rev_mp) 
  23.192 +apply (induct_tac "N")  
  23.193 +apply (auto simp add: power_Suc power_Suc_less less_Suc_eq) 
  23.194 +apply (rename_tac m)  
  23.195 +apply (subgoal_tac "a * a^m < 1 * a^n", simp)
  23.196 +apply (rule mult_strict_mono) 
  23.197 +apply (auto simp add: zero_le_power zero_less_one order_less_imp_le)
  23.198 +done
  23.199 +
  23.200 +text{*Proof resembles that of @{text power_strict_decreasing}*}
  23.201 +lemma power_decreasing:
  23.202 +     "[|n \<le> N; 0 \<le> a; a \<le> (1::'a::{ordered_semiring,ringpower})|]
  23.203 +      ==> a^N \<le> a^n"
  23.204 +apply (erule rev_mp) 
  23.205 +apply (induct_tac "N") 
  23.206 +apply (auto simp add: power_Suc  le_Suc_eq) 
  23.207 +apply (rename_tac m)  
  23.208 +apply (subgoal_tac "a * a^m \<le> 1 * a^n", simp)
  23.209 +apply (rule mult_mono) 
  23.210 +apply (auto simp add: zero_le_power zero_le_one)
  23.211 +done
  23.212 +
  23.213 +lemma power_Suc_less_one:
  23.214 +     "[| 0 < a; a < (1::'a::{ordered_semiring,ringpower}) |] ==> a ^ Suc n < 1"
  23.215 +apply (insert power_strict_decreasing [of 0 "Suc n" a], simp) 
  23.216 +done
  23.217 +
  23.218 +text{*Proof again resembles that of @{text power_strict_decreasing}*}
  23.219 +lemma power_increasing:
  23.220 +     "[|n \<le> N; (1::'a::{ordered_semiring,ringpower}) \<le> a|] ==> a^n \<le> a^N"
  23.221 +apply (erule rev_mp) 
  23.222 +apply (induct_tac "N") 
  23.223 +apply (auto simp add: power_Suc le_Suc_eq) 
  23.224 +apply (rename_tac m)
  23.225 +apply (subgoal_tac "1 * a^n \<le> a * a^m", simp)
  23.226 +apply (rule mult_mono) 
  23.227 +apply (auto simp add: order_trans [OF zero_le_one] zero_le_power)
  23.228 +done
  23.229 +
  23.230 +text{*Lemma for @{text power_strict_increasing}*}
  23.231 +lemma power_less_power_Suc:
  23.232 +     "(1::'a::{ordered_semiring,ringpower}) < a ==> a^n < a * a^n"
  23.233 +apply (induct_tac n) 
  23.234 +apply (auto simp add: power_Suc mult_strict_left_mono order_less_trans [OF zero_less_one]) 
  23.235 +done
  23.236 +
  23.237 +lemma power_strict_increasing:
  23.238 +     "[|n < N; (1::'a::{ordered_semiring,ringpower}) < a|] ==> a^n < a^N"
  23.239 +apply (erule rev_mp) 
  23.240 +apply (induct_tac "N")  
  23.241 +apply (auto simp add: power_less_power_Suc power_Suc less_Suc_eq) 
  23.242 +apply (rename_tac m)
  23.243 +apply (subgoal_tac "1 * a^n < a * a^m", simp)
  23.244 +apply (rule mult_strict_mono)  
  23.245 +apply (auto simp add: order_less_trans [OF zero_less_one] zero_le_power
  23.246 +                 order_less_imp_le)
  23.247 +done
  23.248 +
  23.249 +lemma power_le_imp_le_base:
  23.250 +  assumes le: "a ^ Suc n \<le> b ^ Suc n"
  23.251 +      and xnonneg: "(0::'a::{ordered_semiring,ringpower}) \<le> a"
  23.252 +      and ynonneg: "0 \<le> b"
  23.253 +  shows "a \<le> b"
  23.254 + proof (rule ccontr)
  23.255 +   assume "~ a \<le> b"
  23.256 +   then have "b < a" by (simp only: linorder_not_le)
  23.257 +   then have "b ^ Suc n < a ^ Suc n"
  23.258 +     by (simp only: prems power_strict_mono) 
  23.259 +   from le and this show "False"
  23.260 +      by (simp add: linorder_not_less [symmetric])
  23.261 + qed
  23.262 +  
  23.263 +lemma power_inject_base:
  23.264 +     "[| a ^ Suc n = b ^ Suc n; 0 \<le> a; 0 \<le> b |] 
  23.265 +      ==> a = (b::'a::{ordered_semiring,ringpower})"
  23.266 +by (blast intro: power_le_imp_le_base order_antisym order_eq_refl sym)
  23.267 +
  23.268 +
  23.269 +subsection{*Exponentiation for the Natural Numbers*}
  23.270  
  23.271  primrec (power)
  23.272    "p ^ 0 = 1"
  23.273    "p ^ (Suc n) = (p::nat) * (p ^ n)"
  23.274    
  23.275 +instance nat :: ringpower
  23.276 +proof
  23.277 +  fix z :: nat
  23.278 +  fix n :: nat
  23.279 +  show "z^0 = 1" by simp
  23.280 +  show "z^(Suc n) = z * (z^n)" by simp
  23.281 +qed
  23.282 +
  23.283 +lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n"
  23.284 +by (insert one_le_power [of i n], simp)
  23.285 +
  23.286 +lemma le_imp_power_dvd: "!!i::nat. m \<le> n ==> i^m dvd i^n"
  23.287 +apply (unfold dvd_def)
  23.288 +apply (erule not_less_iff_le [THEN iffD2, THEN add_diff_inverse, THEN subst])
  23.289 +apply (simp add: power_add)
  23.290 +done
  23.291 +
  23.292 +text{*Valid for the naturals, but what if @{text"0<i<1"}?
  23.293 +Premises cannot be weakened: consider the case where @{term "i=0"},
  23.294 +@{term "m=1"} and @{term "n=0"}.*}
  23.295 +lemma nat_power_less_imp_less: "!!i::nat. [| 0 < i; i^m < i^n |] ==> m < n"
  23.296 +apply (rule ccontr)
  23.297 +apply (drule leI [THEN le_imp_power_dvd, THEN dvd_imp_le, THEN leD])
  23.298 +apply (erule zero_less_power, auto) 
  23.299 +done
  23.300 +
  23.301 +lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)"
  23.302 +by (induct_tac "n", auto)
  23.303 +
  23.304 +lemma power_le_dvd [rule_format]: "k^j dvd n --> i\<le>j --> k^i dvd (n::nat)"
  23.305 +apply (induct_tac "j")
  23.306 +apply (simp_all add: le_Suc_eq)
  23.307 +apply (blast dest!: dvd_mult_right)
  23.308 +done
  23.309 +
  23.310 +lemma power_dvd_imp_le: "[|i^m dvd i^n;  (1::nat) < i|] ==> m \<le> n"
  23.311 +apply (rule power_le_imp_le_exp, assumption)
  23.312 +apply (erule dvd_imp_le, simp)
  23.313 +done
  23.314 +
  23.315 +
  23.316 +subsection{*Binomial Coefficients*}
  23.317 +
  23.318 +text{*This development is based on the work of Andy Gordon and 
  23.319 +Florian Kammueller*}
  23.320 +
  23.321 +consts
  23.322 +  binomial :: "[nat,nat] => nat"      (infixl "choose" 65)
  23.323 +
  23.324  primrec
  23.325 -  binomial_0   "(0     choose k) = (if k = 0 then 1 else 0)"
  23.326 +  binomial_0:   "(0     choose k) = (if k = 0 then 1 else 0)"
  23.327 +
  23.328 +  binomial_Suc: "(Suc n choose k) =
  23.329 +                 (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
  23.330 +
  23.331 +lemma binomial_n_0 [simp]: "(n choose 0) = 1"
  23.332 +by (case_tac "n", simp_all)
  23.333 +
  23.334 +lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0"
  23.335 +by simp
  23.336 +
  23.337 +lemma binomial_Suc_Suc [simp]:
  23.338 +     "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)"
  23.339 +by simp
  23.340 +
  23.341 +lemma binomial_eq_0 [rule_format]: "\<forall>k. n < k --> (n choose k) = 0"
  23.342 +apply (induct_tac "n", auto)
  23.343 +apply (erule allE)
  23.344 +apply (erule mp, arith)
  23.345 +done
  23.346 +
  23.347 +declare binomial_0 [simp del] binomial_Suc [simp del]
  23.348 +
  23.349 +lemma binomial_n_n [simp]: "(n choose n) = 1"
  23.350 +apply (induct_tac "n")
  23.351 +apply (simp_all add: binomial_eq_0)
  23.352 +done
  23.353 +
  23.354 +lemma binomial_Suc_n [simp]: "(Suc n choose n) = Suc n"
  23.355 +by (induct_tac "n", simp_all)
  23.356 +
  23.357 +lemma binomial_1 [simp]: "(n choose Suc 0) = n"
  23.358 +by (induct_tac "n", simp_all)
  23.359 +
  23.360 +lemma zero_less_binomial [rule_format]: "k \<le> n --> 0 < (n choose k)"
  23.361 +by (rule_tac m = n and n = k in diff_induct, simp_all)
  23.362  
  23.363 -  binomial_Suc "(Suc n choose k) =
  23.364 -                (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
  23.365 +lemma binomial_eq_0_iff: "(n choose k = 0) = (n<k)"
  23.366 +apply (safe intro!: binomial_eq_0)
  23.367 +apply (erule contrapos_pp)
  23.368 +apply (simp add: zero_less_binomial)
  23.369 +done
  23.370 +
  23.371 +lemma zero_less_binomial_iff: "(0 < n choose k) = (k\<le>n)"
  23.372 +by (simp add: linorder_not_less [symmetric] binomial_eq_0_iff [symmetric])
  23.373 +
  23.374 +(*Might be more useful if re-oriented*)
  23.375 +lemma Suc_times_binomial_eq [rule_format]:
  23.376 +     "\<forall>k. k \<le> n --> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
  23.377 +apply (induct_tac "n")
  23.378 +apply (simp add: binomial_0, clarify)
  23.379 +apply (case_tac "k")
  23.380 +apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq 
  23.381 +                      binomial_eq_0)
  23.382 +done
  23.383 +
  23.384 +text{*This is the well-known version, but it's harder to use because of the
  23.385 +  need to reason about division.*}
  23.386 +lemma binomial_Suc_Suc_eq_times:
  23.387 +     "k \<le> n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"
  23.388 +by (simp add: Suc_times_binomial_eq div_mult_self_is_m zero_less_Suc 
  23.389 +        del: mult_Suc mult_Suc_right)
  23.390 +
  23.391 +text{*Another version, with -1 instead of Suc.*}
  23.392 +lemma times_binomial_minus1_eq:
  23.393 +     "[|k \<le> n;  0<k|] ==> (n choose k) * k = n * ((n - 1) choose (k - 1))"
  23.394 +apply (cut_tac n = "n - 1" and k = "k - 1" in Suc_times_binomial_eq)
  23.395 +apply (simp split add: nat_diff_split, auto)
  23.396 +done
  23.397 +
  23.398 +text{*ML bindings for the general exponentiation theorems*}
  23.399 +ML
  23.400 +{*
  23.401 +val power_0 = thm"power_0";
  23.402 +val power_Suc = thm"power_Suc";
  23.403 +val power_0_Suc = thm"power_0_Suc";
  23.404 +val power_0_left = thm"power_0_left";
  23.405 +val power_one = thm"power_one";
  23.406 +val power_one_right = thm"power_one_right";
  23.407 +val power_add = thm"power_add";
  23.408 +val power_mult = thm"power_mult";
  23.409 +val power_mult_distrib = thm"power_mult_distrib";
  23.410 +val zero_less_power = thm"zero_less_power";
  23.411 +val zero_le_power = thm"zero_le_power";
  23.412 +val one_le_power = thm"one_le_power";
  23.413 +val gt1_imp_ge0 = thm"gt1_imp_ge0";
  23.414 +val power_gt1_lemma = thm"power_gt1_lemma";
  23.415 +val power_gt1 = thm"power_gt1";
  23.416 +val power_le_imp_le_exp = thm"power_le_imp_le_exp";
  23.417 +val power_inject_exp = thm"power_inject_exp";
  23.418 +val power_less_imp_less_exp = thm"power_less_imp_less_exp";
  23.419 +val power_mono = thm"power_mono";
  23.420 +val power_strict_mono = thm"power_strict_mono";
  23.421 +val power_eq_0_iff = thm"power_eq_0_iff";
  23.422 +val field_power_eq_0_iff = thm"field_power_eq_0_iff";
  23.423 +val field_power_not_zero = thm"field_power_not_zero";
  23.424 +val power_inverse = thm"power_inverse";
  23.425 +val power_abs = thm"power_abs";
  23.426 +val power_minus = thm"power_minus";
  23.427 +val power_Suc_less = thm"power_Suc_less";
  23.428 +val power_strict_decreasing = thm"power_strict_decreasing";
  23.429 +val power_decreasing = thm"power_decreasing";
  23.430 +val power_Suc_less_one = thm"power_Suc_less_one";
  23.431 +val power_increasing = thm"power_increasing";
  23.432 +val power_strict_increasing = thm"power_strict_increasing";
  23.433 +val power_le_imp_le_base = thm"power_le_imp_le_base";
  23.434 +val power_inject_base = thm"power_inject_base";
  23.435 +*}
  23.436 + 
  23.437 +text{*ML bindings for the remaining theorems*}
  23.438 +ML
  23.439 +{*
  23.440 +val nat_one_le_power = thm"nat_one_le_power";
  23.441 +val le_imp_power_dvd = thm"le_imp_power_dvd";
  23.442 +val nat_power_less_imp_less = thm"nat_power_less_imp_less";
  23.443 +val nat_zero_less_power_iff = thm"nat_zero_less_power_iff";
  23.444 +val power_le_dvd = thm"power_le_dvd";
  23.445 +val power_dvd_imp_le = thm"power_dvd_imp_le";
  23.446 +val binomial_n_0 = thm"binomial_n_0";
  23.447 +val binomial_0_Suc = thm"binomial_0_Suc";
  23.448 +val binomial_Suc_Suc = thm"binomial_Suc_Suc";
  23.449 +val binomial_eq_0 = thm"binomial_eq_0";
  23.450 +val binomial_n_n = thm"binomial_n_n";
  23.451 +val binomial_Suc_n = thm"binomial_Suc_n";
  23.452 +val binomial_1 = thm"binomial_1";
  23.453 +val zero_less_binomial = thm"zero_less_binomial";
  23.454 +val binomial_eq_0_iff = thm"binomial_eq_0_iff";
  23.455 +val zero_less_binomial_iff = thm"zero_less_binomial_iff";
  23.456 +val Suc_times_binomial_eq = thm"Suc_times_binomial_eq";
  23.457 +val binomial_Suc_Suc_eq_times = thm"binomial_Suc_Suc_eq_times";
  23.458 +val times_binomial_minus1_eq = thm"times_binomial_minus1_eq";
  23.459 +*}
  23.460  
  23.461  end
  23.462  
    24.1 --- a/src/HOL/Real/RealDef.thy	Fri Jan 09 01:28:24 2004 +0100
    24.2 +++ b/src/HOL/Real/RealDef.thy	Fri Jan 09 10:46:18 2004 +0100
    24.3 @@ -825,6 +825,9 @@
    24.4  instance real :: ordered_field
    24.5  proof
    24.6    fix x y z :: real
    24.7 +  show "0 < (1::real)" 
    24.8 +    by (force intro: real_gt_zero_preal_Ex [THEN iffD2]
    24.9 +              simp add: real_one_def real_of_preal_def)
   24.10    show "x \<le> y ==> z + x \<le> z + y" by (rule real_add_left_mono)
   24.11    show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: real_mult_less_mono2)
   24.12    show "\<bar>x\<bar> = (if x < 0 then -x else x)"
    25.1 --- a/src/HOL/Real/RealPow.thy	Fri Jan 09 01:28:24 2004 +0100
    25.2 +++ b/src/HOL/Real/RealPow.thy	Fri Jan 09 10:46:18 2004 +0100
    25.3 @@ -8,6 +8,8 @@
    25.4  
    25.5  theory RealPow = RealArith:
    25.6  
    25.7 +declare abs_mult_self [simp]
    25.8 +
    25.9  instance real :: power ..
   25.10  
   25.11  primrec (realpow)
   25.12 @@ -15,118 +17,45 @@
   25.13       realpow_Suc: "r ^ (Suc n) = (r::real) * (r ^ n)"
   25.14  
   25.15  
   25.16 -lemma realpow_zero [simp]: "(0::real) ^ (Suc n) = 0"
   25.17 -by auto
   25.18 +instance real :: ringpower
   25.19 +proof
   25.20 +  fix z :: real
   25.21 +  fix n :: nat
   25.22 +  show "z^0 = 1" by simp
   25.23 +  show "z^(Suc n) = z * (z^n)" by simp
   25.24 +qed
   25.25  
   25.26 -lemma realpow_not_zero [rule_format]: "r \<noteq> (0::real) --> r ^ n \<noteq> 0"
   25.27 -by (induct_tac "n", auto)
   25.28 +
   25.29 +lemma realpow_not_zero: "r \<noteq> (0::real) ==> r ^ n \<noteq> 0"
   25.30 +  by (rule field_power_not_zero)
   25.31  
   25.32  lemma realpow_zero_zero: "r ^ n = (0::real) ==> r = 0"
   25.33 -apply (rule ccontr)
   25.34 -apply (auto dest: realpow_not_zero)
   25.35 -done
   25.36 -
   25.37 -lemma realpow_inverse: "inverse ((r::real) ^ n) = (inverse r) ^ n"
   25.38 -apply (induct_tac "n")
   25.39 -apply (auto simp add: inverse_mult_distrib)
   25.40 -done
   25.41 -
   25.42 -lemma realpow_abs: "abs(r ^ n) = abs(r::real) ^ n"
   25.43 -apply (induct_tac "n")
   25.44 -apply (auto simp add: abs_mult)
   25.45 -done
   25.46 -
   25.47 -lemma realpow_add: "(r::real) ^ (n + m) = (r ^ n) * (r ^ m)"
   25.48 -apply (induct_tac "n")
   25.49 -apply (auto simp add: mult_ac)
   25.50 -done
   25.51 -
   25.52 -lemma realpow_one [simp]: "(r::real) ^ 1 = r"
   25.53  by simp
   25.54  
   25.55  lemma realpow_two: "(r::real)^ (Suc (Suc 0)) = r * r"
   25.56  by simp
   25.57  
   25.58 -lemma realpow_gt_zero [rule_format]: "(0::real) < r --> 0 < r ^ n"
   25.59 -apply (induct_tac "n")
   25.60 -apply (auto intro: real_mult_order simp add: zero_less_one)
   25.61 -done
   25.62 -
   25.63 -lemma realpow_ge_zero [rule_format]: "(0::real) \<le> r --> 0 \<le> r ^ n"
   25.64 -apply (induct_tac "n")
   25.65 -apply (auto simp add: zero_le_mult_iff)
   25.66 -done
   25.67 -
   25.68 -lemma realpow_le [rule_format]: "(0::real) \<le> x & x \<le> y --> x ^ n \<le> y ^ n"
   25.69 -apply (induct_tac "n")
   25.70 -apply (auto intro!: mult_mono)
   25.71 -apply (simp (no_asm_simp) add: realpow_ge_zero)
   25.72 -done
   25.73 -
   25.74 -lemma realpow_0_left [rule_format, simp]:
   25.75 -     "0 < n --> 0 ^ n = (0::real)"
   25.76 -apply (induct_tac "n", auto) 
   25.77 +text{*Legacy: weaker version of the theorem @{text power_strict_mono},
   25.78 +used 6 times in NthRoot and Transcendental*}
   25.79 +lemma realpow_less:
   25.80 +     "[|(0::real) < x; x < y; 0 < n|] ==> x ^ n < y ^ n"
   25.81 +apply (rule power_strict_mono, auto) 
   25.82  done
   25.83  
   25.84 -lemma realpow_less' [rule_format]:
   25.85 -     "[|(0::real) \<le> x; x < y |] ==> 0 < n --> x ^ n < y ^ n"
   25.86 -apply (induct n) 
   25.87 -apply (auto simp add: real_mult_less_mono' realpow_ge_zero) 
   25.88 -done
   25.89 -
   25.90 -text{*Legacy: weaker version of the theorem above*}
   25.91 -lemma realpow_less:
   25.92 -     "[|(0::real) < x; x < y; 0 < n|] ==> x ^ n < y ^ n"
   25.93 -apply (rule realpow_less', auto) 
   25.94 -done
   25.95 -
   25.96 -lemma realpow_eq_one [simp]: "1 ^ n = (1::real)"
   25.97 -by (induct_tac "n", auto)
   25.98 -
   25.99  lemma abs_realpow_minus_one [simp]: "abs((-1) ^ n) = (1::real)"
  25.100 -apply (induct_tac "n")
  25.101 -apply (auto simp add: abs_mult)
  25.102 -done
  25.103 -
  25.104 -lemma realpow_mult: "((r::real) * s) ^ n = (r ^ n) * (s ^ n)"
  25.105 -apply (induct_tac "n")
  25.106 -apply (auto simp add: mult_ac)
  25.107 -done
  25.108 +by (simp add: power_abs)
  25.109  
  25.110  lemma realpow_two_le [simp]: "(0::real) \<le> r^ Suc (Suc 0)"
  25.111  by (simp add: real_le_square)
  25.112  
  25.113  lemma abs_realpow_two [simp]: "abs((x::real)^Suc (Suc 0)) = x^Suc (Suc 0)"
  25.114 -by (simp add: abs_eqI1 real_le_square)
  25.115 +by (simp add: abs_mult)
  25.116  
  25.117  lemma realpow_two_abs [simp]: "abs(x::real)^Suc (Suc 0) = x^Suc (Suc 0)"
  25.118 -by (simp add: realpow_abs [symmetric] abs_eqI1 del: realpow_Suc)
  25.119 -
  25.120 -lemma realpow_two_gt_one: "(1::real) < r ==> 1 < r^ (Suc (Suc 0))"
  25.121 -apply auto
  25.122 -apply (cut_tac real_zero_less_one)
  25.123 -apply (frule_tac x = 0 in order_less_trans, assumption)
  25.124 -apply (frule_tac c = r and a = 1 in mult_strict_right_mono)
  25.125 -apply assumption; 
  25.126 -apply (simp add: ); 
  25.127 -done
  25.128 -
  25.129 -lemma realpow_ge_one [rule_format]: "(1::real) < r --> 1 \<le> r ^ n"
  25.130 -apply (induct_tac "n", auto)
  25.131 -apply (subgoal_tac "1*1 \<le> r * r^n")
  25.132 -apply (rule_tac [2] mult_mono, auto)
  25.133 -done
  25.134 -
  25.135 -lemma realpow_ge_one2: "(1::real) \<le> r ==> 1 \<le> r ^ n"
  25.136 -apply (drule order_le_imp_less_or_eq)
  25.137 -apply (auto dest: realpow_ge_one)
  25.138 -done
  25.139 +by (simp add: power_abs [symmetric] abs_eqI1 del: realpow_Suc)
  25.140  
  25.141  lemma two_realpow_ge_one [simp]: "(1::real) \<le> 2 ^ n"
  25.142 -apply (rule_tac y = "1 ^ n" in order_trans)
  25.143 -apply (rule_tac [2] realpow_le)
  25.144 -apply (auto intro: order_less_imp_le)
  25.145 -done
  25.146 +by (insert power_increasing [of 0 n "2::real"], simp)
  25.147  
  25.148  lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n"
  25.149  apply (induct_tac "n")
  25.150 @@ -145,111 +74,38 @@
  25.151  lemma realpow_minus_one_even [simp]: "(-1) ^ Suc (Suc (2*n)) = (1::real)"
  25.152  by auto
  25.153  
  25.154 -lemma realpow_Suc_less [rule_format]:
  25.155 -     "(0::real) < r & r < (1::real) --> r ^ Suc n < r ^ n"
  25.156 -  by (induct_tac "n", auto simp add: mult_less_cancel_left)
  25.157 -
  25.158 -lemma realpow_Suc_le [rule_format]:
  25.159 -     "0 \<le> r & r < (1::real) --> r ^ Suc n \<le> r ^ n"
  25.160 -apply (induct_tac "n")
  25.161 -apply (auto intro: order_less_imp_le dest!: order_le_imp_less_or_eq)
  25.162 -done
  25.163 -
  25.164 -lemma realpow_zero_le [simp]: "(0::real) \<le> 0 ^ n"
  25.165 -by (case_tac "n", auto)
  25.166 -
  25.167 -lemma realpow_Suc_le2 [rule_format]: "0 < r & r < (1::real) --> r ^ Suc n \<le> r ^ n"
  25.168 -by (blast intro!: order_less_imp_le realpow_Suc_less)
  25.169 +lemma realpow_Suc_le_self: "[| 0 \<le> r; r \<le> (1::real) |] ==> r ^ Suc n \<le> r"
  25.170 +by (insert power_decreasing [of 1 "Suc n" r], simp)
  25.171  
  25.172 -lemma realpow_Suc_le3: "[| 0 \<le> r; r < (1::real) |] ==> r ^ Suc n \<le> r ^ n"
  25.173 -apply (erule order_le_imp_less_or_eq [THEN disjE])
  25.174 -apply (rule realpow_Suc_le2, auto)
  25.175 -done
  25.176 +text{*Used ONCE in Transcendental*}
  25.177 +lemma realpow_Suc_less_one: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n < 1"
  25.178 +by (insert power_strict_decreasing [of 0 "Suc n" r], simp)
  25.179  
  25.180 -lemma realpow_less_le [rule_format]: "0 \<le> r & r < (1::real) & n < N --> r ^ N \<le> r ^ n"
  25.181 -apply (induct_tac "N")
  25.182 -apply (simp_all (no_asm_simp))
  25.183 -apply clarify
  25.184 -apply (subgoal_tac "r * r ^ na \<le> 1 * r ^ n", simp)
  25.185 -apply (rule mult_mono)
  25.186 -apply (auto simp add: realpow_ge_zero less_Suc_eq)
  25.187 -done
  25.188 -
  25.189 -lemma realpow_le_le: "[| 0 \<le> r; r < (1::real); n \<le> N |] ==> r ^ N \<le> r ^ n"
  25.190 -apply (drule_tac n = N in le_imp_less_or_eq)
  25.191 -apply (auto intro: realpow_less_le)
  25.192 +text{*Used ONCE in Lim.ML*}
  25.193 +lemma realpow_minus_mult [rule_format]:
  25.194 +     "0 < n --> (x::real) ^ (n - 1) * x = x ^ n" 
  25.195 +apply (simp split add: nat_diff_split)
  25.196  done
  25.197  
  25.198 -lemma realpow_Suc_le_self: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n \<le> r"
  25.199 -by (drule_tac n = 1 and N = "Suc n" in order_less_imp_le [THEN realpow_le_le], auto)
  25.200 -
  25.201 -lemma realpow_Suc_less_one: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n < 1"
  25.202 -by (blast intro: realpow_Suc_le_self order_le_less_trans)
  25.203 -
  25.204 -lemma realpow_le_Suc [rule_format]: "(1::real) \<le> r --> r ^ n \<le> r ^ Suc n"
  25.205 -by (induct_tac "n", auto)
  25.206 -
  25.207 -lemma realpow_less_Suc [rule_format]: "(1::real) < r --> r ^ n < r ^ Suc n"
  25.208 -by (induct_tac "n", auto simp add: mult_less_cancel_left)
  25.209 -
  25.210 -lemma realpow_le_Suc2 [rule_format]: "(1::real) < r --> r ^ n \<le> r ^ Suc n"
  25.211 -by (blast intro!: order_less_imp_le realpow_less_Suc)
  25.212 -
  25.213 -(*One use in RealPow.thy*)
  25.214 -lemma real_mult_self_le2: "[| (1::real) \<le> r; (1::real) \<le> x |]  ==> x \<le> r * x"
  25.215 -apply (subgoal_tac "1 * x \<le> r * x", simp) 
  25.216 -apply (rule mult_right_mono, auto) 
  25.217 -done
  25.218 -
  25.219 -lemma realpow_gt_ge2 [rule_format]: "(1::real) \<le> r & n < N --> r ^ n \<le> r ^ N"
  25.220 -apply (induct_tac "N", auto)
  25.221 -apply (frule_tac [!] n = na in realpow_ge_one2)
  25.222 -apply (drule_tac [!] real_mult_self_le2, assumption)
  25.223 -prefer 2 apply assumption
  25.224 -apply (auto intro: order_trans simp add: less_Suc_eq)
  25.225 -done
  25.226 -
  25.227 -lemma realpow_ge_ge2: "[| (1::real) \<le> r; n \<le> N |] ==> r ^ n \<le> r ^ N"
  25.228 -apply (drule_tac n = N in le_imp_less_or_eq)
  25.229 -apply (auto intro: realpow_gt_ge2)
  25.230 -done
  25.231 -
  25.232 -lemma realpow_Suc_ge_self2: "(1::real) \<le> r ==> r \<le> r ^ Suc n"
  25.233 -by (drule_tac n = 1 and N = "Suc n" in realpow_ge_ge2, auto)
  25.234 -
  25.235 -(*Used ONCE in Hyperreal/NthRoot.ML*)
  25.236 -lemma realpow_ge_self2: "[| (1::real) \<le> r; 0 < n |] ==> r \<le> r ^ n"
  25.237 -apply (drule less_not_refl2 [THEN not0_implies_Suc])
  25.238 -apply (auto intro!: realpow_Suc_ge_self2)
  25.239 -done
  25.240 -
  25.241 -lemma realpow_minus_mult [rule_format, simp]:
  25.242 -     "0 < n --> (x::real) ^ (n - 1) * x = x ^ n"
  25.243 -apply (induct_tac "n")
  25.244 -apply (auto simp add: real_mult_commute)
  25.245 -done
  25.246 -
  25.247 -lemma realpow_two_mult_inverse [simp]: "r \<noteq> 0 ==> r * inverse r ^Suc (Suc 0) = inverse (r::real)"
  25.248 +lemma realpow_two_mult_inverse [simp]:
  25.249 +     "r \<noteq> 0 ==> r * inverse r ^Suc (Suc 0) = inverse (r::real)"
  25.250  by (simp add: realpow_two real_mult_assoc [symmetric])
  25.251  
  25.252 -(* 05/00 *)
  25.253  lemma realpow_two_minus [simp]: "(-x)^Suc (Suc 0) = (x::real)^Suc (Suc 0)"
  25.254  by simp
  25.255  
  25.256 -lemma realpow_two_diff: "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
  25.257 +lemma realpow_two_diff:
  25.258 +     "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
  25.259  apply (unfold real_diff_def)
  25.260  apply (simp add: right_distrib left_distrib mult_ac)
  25.261  done
  25.262  
  25.263 -lemma realpow_two_disj: "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)"
  25.264 +lemma realpow_two_disj:
  25.265 +     "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)"
  25.266  apply (cut_tac x = x and y = y in realpow_two_diff)
  25.267  apply (auto simp del: realpow_Suc)
  25.268  done
  25.269  
  25.270 -(* used in Transc *)
  25.271 -lemma realpow_diff: "[|(x::real) \<noteq> 0; m \<le> n |] ==> x ^ (n - m) = x ^ n * inverse (x ^ m)"
  25.272 -by (auto simp add: le_eq_less_or_eq less_iff_Suc_add realpow_add realpow_not_zero mult_ac)
  25.273 -
  25.274  lemma realpow_real_of_nat: "real (m::nat) ^ n = real (m ^ n)"
  25.275  apply (induct_tac "n")
  25.276  apply (auto simp add: real_of_nat_one real_of_nat_mult)
  25.277 @@ -261,29 +117,12 @@
  25.278  done
  25.279  
  25.280  lemma realpow_increasing:
  25.281 -  assumes xnonneg: "(0::real) \<le> x"
  25.282 -      and ynonneg: "0 \<le> y"
  25.283 -      and le: "x ^ Suc n \<le> y ^ Suc n"
  25.284 -  shows "x \<le> y"
  25.285 - proof (rule ccontr)
  25.286 -   assume "~ x \<le> y"
  25.287 -   then have "y<x" by simp
  25.288 -   then have "y ^ Suc n < x ^ Suc n"
  25.289 -     by (simp only: prems realpow_less') 
  25.290 -   from le and this show "False"
  25.291 -     by simp
  25.292 - qed
  25.293 -  
  25.294 -lemma realpow_Suc_cancel_eq: "[| (0::real) \<le> x; 0 \<le> y; x ^ Suc n = y ^ Suc n |] ==> x = y"
  25.295 -by (blast intro: realpow_increasing order_antisym order_eq_refl sym)
  25.296 +     "[|(0::real) \<le> x; 0 \<le> y; x ^ Suc n \<le> y ^ Suc n|] ==> x \<le> y"
  25.297 +  by (rule power_le_imp_le_base)
  25.298  
  25.299  
  25.300 -(*** Logical equivalences for inequalities ***)
  25.301 -
  25.302 -lemma realpow_eq_0_iff [simp]: "(x^n = 0) = (x = (0::real) & 0<n)"
  25.303 -by (induct_tac "n", auto)
  25.304 -
  25.305 -lemma zero_less_realpow_abs_iff [simp]: "(0 < (abs x)^n) = (x \<noteq> (0::real) | n=0)"
  25.306 +lemma zero_less_realpow_abs_iff [simp]:
  25.307 +     "(0 < (abs x)^n) = (x \<noteq> (0::real) | n=0)" 
  25.308  apply (induct_tac "n")
  25.309  apply (auto simp add: zero_less_mult_iff)
  25.310  done
  25.311 @@ -294,7 +133,7 @@
  25.312  done
  25.313  
  25.314  
  25.315 -(*** Literal arithmetic involving powers, type real ***)
  25.316 +subsection{*Literal Arithmetic Involving Powers, Type @{typ real}*}
  25.317  
  25.318  lemma real_of_int_power: "real (x::int) ^ n = real (x ^ n)"
  25.319  apply (induct_tac "n")
  25.320 @@ -302,7 +141,8 @@
  25.321  done
  25.322  declare real_of_int_power [symmetric, simp]
  25.323  
  25.324 -lemma power_real_number_of: "(number_of v :: real) ^ n = real ((number_of v :: int) ^ n)"
  25.325 +lemma power_real_number_of:
  25.326 +     "(number_of v :: real) ^ n = real ((number_of v :: int) ^ n)"
  25.327  by (simp only: real_number_of_def real_of_int_power)
  25.328  
  25.329  declare power_real_number_of [of _ "number_of w", standard, simp]
  25.330 @@ -311,20 +151,6 @@
  25.331  lemma real_power_two: "(r::real)\<twosuperior> = r * r"
  25.332    by (simp add: numeral_2_eq_2)
  25.333  
  25.334 -lemma real_sqr_ge_zero [iff]: "0 \<le> (r::real)\<twosuperior>"
  25.335 -  by (simp add: real_power_two)
  25.336 -
  25.337 -lemma real_sqr_gt_zero: "(r::real) \<noteq> 0 ==> 0 < r\<twosuperior>"
  25.338 -proof -
  25.339 -  assume "r \<noteq> 0"
  25.340 -  hence "0 \<noteq> r\<twosuperior>" by simp
  25.341 -  also have "0 \<le> r\<twosuperior>" by (simp add: real_sqr_ge_zero)
  25.342 -  finally show ?thesis .
  25.343 -qed
  25.344 -
  25.345 -lemma real_sqr_not_zero: "r \<noteq> 0 ==> (r::real)\<twosuperior> \<noteq> 0"
  25.346 -  by simp
  25.347 -
  25.348  
  25.349  subsection{*Various Other Theorems*}
  25.350  
  25.351 @@ -333,25 +159,19 @@
  25.352    by (auto intro: real_sum_squares_cancel)
  25.353  
  25.354  lemma real_squared_diff_one_factored: "x*x - (1::real) = (x + 1)*(x - 1)"
  25.355 -apply (auto simp add: left_distrib right_distrib real_diff_def)
  25.356 -done
  25.357 +by (auto simp add: left_distrib right_distrib real_diff_def)
  25.358  
  25.359 -lemma real_mult_is_one: "(x*x = (1::real)) = (x = 1 | x = - 1)"
  25.360 +lemma real_mult_is_one [simp]: "(x*x = (1::real)) = (x = 1 | x = - 1)"
  25.361  apply auto
  25.362  apply (drule right_minus_eq [THEN iffD2]) 
  25.363  apply (auto simp add: real_squared_diff_one_factored)
  25.364  done
  25.365 -declare real_mult_is_one [iff]
  25.366  
  25.367  lemma real_le_add_half_cancel: "(x + y/2 \<le> (y::real)) = (x \<le> y /2)"
  25.368 -apply auto
  25.369 -done
  25.370 -declare real_le_add_half_cancel [simp]
  25.371 +by auto
  25.372  
  25.373 -lemma real_minus_half_eq: "(x::real) - x/2 = x/2"
  25.374 -apply auto
  25.375 -done
  25.376 -declare real_minus_half_eq [simp]
  25.377 +lemma real_minus_half_eq [simp]: "(x::real) - x/2 = x/2"
  25.378 +by auto
  25.379  
  25.380  lemma real_mult_inverse_cancel:
  25.381       "[|(0::real) < x; 0 < x1; x1 * y < x * u |] 
  25.382 @@ -364,34 +184,22 @@
  25.383  done
  25.384  
  25.385  text{*Used once: in Hyperreal/Transcendental.ML*}
  25.386 -lemma real_mult_inverse_cancel2: "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
  25.387 +lemma real_mult_inverse_cancel2:
  25.388 +     "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
  25.389  apply (auto dest: real_mult_inverse_cancel simp add: mult_ac)
  25.390  done
  25.391  
  25.392 -lemma inverse_real_of_nat_gt_zero: "0 < inverse (real (Suc n))"
  25.393 -apply auto
  25.394 -done
  25.395 -declare inverse_real_of_nat_gt_zero [simp]
  25.396 +lemma inverse_real_of_nat_gt_zero [simp]: "0 < inverse (real (Suc n))"
  25.397 +by auto
  25.398  
  25.399 -lemma inverse_real_of_nat_ge_zero: "0 \<le> inverse (real (Suc n))"
  25.400 -apply auto
  25.401 -done
  25.402 -declare inverse_real_of_nat_ge_zero [simp]
  25.403 +lemma inverse_real_of_nat_ge_zero [simp]: "0 \<le> inverse (real (Suc n))"
  25.404 +by auto
  25.405  
  25.406  lemma real_sum_squares_not_zero: "x ~= 0 ==> x * x + y * y ~= (0::real)"
  25.407 -apply (blast dest!: real_sum_squares_cancel) 
  25.408 -done
  25.409 +by (blast dest!: real_sum_squares_cancel)
  25.410  
  25.411  lemma real_sum_squares_not_zero2: "y ~= 0 ==> x * x + y * y ~= (0::real)"
  25.412 -apply (blast dest!: real_sum_squares_cancel2) 
  25.413 -done
  25.414 -
  25.415 -(* nice theorem *)
  25.416 -lemma abs_mult_abs: "abs x * abs x = x * (x::real)"
  25.417 -apply (insert linorder_less_linear [of x 0]) 
  25.418 -apply (auto simp add: abs_eqI2 abs_minus_eqI2)
  25.419 -done
  25.420 -declare abs_mult_abs [simp]
  25.421 +by (blast dest!: real_sum_squares_cancel2)
  25.422  
  25.423  
  25.424  subsection {*Various Other Theorems*}
  25.425 @@ -399,50 +207,29 @@
  25.426  lemma realpow_divide: 
  25.427      "(x/y) ^ n = ((x::real) ^ n/ y ^ n)"
  25.428  apply (unfold real_divide_def)
  25.429 -apply (auto simp add: realpow_mult realpow_inverse)
  25.430 -done
  25.431 -
  25.432 -lemma realpow_ge_zero2 [rule_format (no_asm)]: "(0::real) \<le> r --> 0 \<le> r ^ n"
  25.433 -apply (induct_tac "n")
  25.434 -apply (auto simp add: zero_le_mult_iff)
  25.435 +apply (auto simp add: power_mult_distrib power_inverse)
  25.436  done
  25.437  
  25.438 -lemma realpow_le2 [rule_format (no_asm)]: "(0::real) \<le> x & x \<le> y --> x ^ n \<le> y ^ n"
  25.439 -apply (induct_tac "n")
  25.440 -apply (auto intro!: mult_mono simp add: realpow_ge_zero2)
  25.441 -done
  25.442 -
  25.443 -lemma realpow_Suc_gt_one: "(1::real) < r ==> 1 < r ^ (Suc n)"
  25.444 -apply (frule_tac n = "n" in realpow_ge_one)
  25.445 -apply (drule real_le_imp_less_or_eq, safe)
  25.446 -apply (frule zero_less_one [THEN real_less_trans])
  25.447 -apply (drule_tac y = "r ^ n" in real_mult_less_mono2)
  25.448 -apply assumption
  25.449 -apply (auto dest: real_less_trans)
  25.450 +lemma realpow_two_sum_zero_iff [simp]:
  25.451 +     "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
  25.452 +apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 
  25.453 +                   simp add: real_power_two)
  25.454  done
  25.455  
  25.456 -lemma realpow_two_sum_zero_iff: "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
  25.457 -apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 simp add: numeral_2_eq_2)
  25.458 -done
  25.459 -declare realpow_two_sum_zero_iff [simp]
  25.460 -
  25.461 -lemma realpow_two_le_add_order: "(0::real) \<le> u ^ 2 + v ^ 2"
  25.462 +lemma realpow_two_le_add_order [simp]: "(0::real) \<le> u ^ 2 + v ^ 2"
  25.463  apply (rule real_le_add_order)
  25.464 -apply (auto simp add: numeral_2_eq_2)
  25.465 +apply (auto simp add: real_power_two)
  25.466  done
  25.467 -declare realpow_two_le_add_order [simp]
  25.468  
  25.469 -lemma realpow_two_le_add_order2: "(0::real) \<le> u ^ 2 + v ^ 2 + w ^ 2"
  25.470 +lemma realpow_two_le_add_order2 [simp]: "(0::real) \<le> u ^ 2 + v ^ 2 + w ^ 2"
  25.471  apply (rule real_le_add_order)+
  25.472 -apply (auto simp add: numeral_2_eq_2)
  25.473 +apply (auto simp add: real_power_two)
  25.474  done
  25.475 -declare realpow_two_le_add_order2 [simp]
  25.476  
  25.477  lemma real_sum_square_gt_zero: "x ~= 0 ==> (0::real) < x * x + y * y"
  25.478 -apply (cut_tac x = "x" and y = "y" in real_mult_self_sum_ge_zero)
  25.479 +apply (cut_tac x = x and y = y in real_mult_self_sum_ge_zero)
  25.480  apply (drule real_le_imp_less_or_eq)
  25.481 -apply (drule_tac y = "y" in real_sum_squares_not_zero)
  25.482 -apply auto
  25.483 +apply (drule_tac y = y in real_sum_squares_not_zero, auto)
  25.484  done
  25.485  
  25.486  lemma real_sum_square_gt_zero2: "y ~= 0 ==> (0::real) < x * x + y * y"
  25.487 @@ -450,48 +237,29 @@
  25.488  apply (erule real_sum_square_gt_zero)
  25.489  done
  25.490  
  25.491 -lemma real_minus_mult_self_le: "-(u * u) \<le> (x * (x::real))"
  25.492 -apply (rule_tac j = "0" in real_le_trans)
  25.493 -apply auto
  25.494 -done
  25.495 -declare real_minus_mult_self_le [simp]
  25.496 +lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))"
  25.497 +by (rule_tac j = 0 in real_le_trans, auto)
  25.498  
  25.499 -lemma realpow_square_minus_le: "-(u ^ 2) \<le> (x::real) ^ 2"
  25.500 -apply (auto simp add: numeral_2_eq_2)
  25.501 -done
  25.502 -declare realpow_square_minus_le [simp]
  25.503 +lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2"
  25.504 +by (auto simp add: real_power_two)
  25.505  
  25.506  lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
  25.507 -apply (case_tac "n")
  25.508 -apply auto
  25.509 -done
  25.510 +by (case_tac "n", auto)
  25.511  
  25.512 -lemma real_num_zero_less_two_pow: "0 < (2::real) ^ (4*d)"
  25.513 +lemma real_num_zero_less_two_pow [simp]: "0 < (2::real) ^ (4*d)"
  25.514  apply (induct_tac "d")
  25.515  apply (auto simp add: realpow_num_eq_if)
  25.516  done
  25.517 -declare real_num_zero_less_two_pow [simp]
  25.518  
  25.519 -lemma lemma_realpow_num_two_mono: "x * (4::real)   < y ==> x * (2 ^ 8) < y * (2 ^ 6)"
  25.520 +lemma lemma_realpow_num_two_mono:
  25.521 +     "x * (4::real)   < y ==> x * (2 ^ 8) < y * (2 ^ 6)"
  25.522  apply (subgoal_tac " (2::real) ^ 8 = 4 * (2 ^ 6) ")
  25.523  apply (simp (no_asm_simp) add: real_mult_assoc [symmetric])
  25.524  apply (auto simp add: realpow_num_eq_if)
  25.525  done
  25.526  
  25.527 -lemma lemma_realpow_4: "2 ^ 2 = (4::real)"
  25.528 -apply (simp (no_asm) add: realpow_num_eq_if)
  25.529 -done
  25.530 -declare lemma_realpow_4 [simp]
  25.531 -
  25.532 -lemma lemma_realpow_16: "2 ^ 4 = (16::real)"
  25.533 -apply (simp (no_asm) add: realpow_num_eq_if)
  25.534 -done
  25.535 -declare lemma_realpow_16 [simp]
  25.536 -
  25.537 -lemma zero_le_x_squared: "(0::real) \<le> x^2"
  25.538 -apply (simp add: numeral_2_eq_2)
  25.539 -done
  25.540 -declare zero_le_x_squared [simp]
  25.541 +lemma zero_le_x_squared [simp]: "(0::real) \<le> x^2"
  25.542 +by (simp add: real_power_two)
  25.543  
  25.544  
  25.545  
  25.546 @@ -500,67 +268,33 @@
  25.547  val realpow_0 = thm "realpow_0";
  25.548  val realpow_Suc = thm "realpow_Suc";
  25.549  
  25.550 -val realpow_zero = thm "realpow_zero";
  25.551  val realpow_not_zero = thm "realpow_not_zero";
  25.552  val realpow_zero_zero = thm "realpow_zero_zero";
  25.553 -val realpow_inverse = thm "realpow_inverse";
  25.554 -val realpow_abs = thm "realpow_abs";
  25.555 -val realpow_add = thm "realpow_add";
  25.556 -val realpow_one = thm "realpow_one";
  25.557  val realpow_two = thm "realpow_two";
  25.558 -val realpow_gt_zero = thm "realpow_gt_zero";
  25.559 -val realpow_ge_zero = thm "realpow_ge_zero";
  25.560 -val realpow_le = thm "realpow_le";
  25.561 -val realpow_0_left = thm "realpow_0_left";
  25.562  val realpow_less = thm "realpow_less";
  25.563 -val realpow_eq_one = thm "realpow_eq_one";
  25.564  val abs_realpow_minus_one = thm "abs_realpow_minus_one";
  25.565 -val realpow_mult = thm "realpow_mult";
  25.566  val realpow_two_le = thm "realpow_two_le";
  25.567  val abs_realpow_two = thm "abs_realpow_two";
  25.568  val realpow_two_abs = thm "realpow_two_abs";
  25.569 -val realpow_two_gt_one = thm "realpow_two_gt_one";
  25.570 -val realpow_ge_one = thm "realpow_ge_one";
  25.571 -val realpow_ge_one2 = thm "realpow_ge_one2";
  25.572  val two_realpow_ge_one = thm "two_realpow_ge_one";
  25.573  val two_realpow_gt = thm "two_realpow_gt";
  25.574  val realpow_minus_one = thm "realpow_minus_one";
  25.575  val realpow_minus_one_odd = thm "realpow_minus_one_odd";
  25.576  val realpow_minus_one_even = thm "realpow_minus_one_even";
  25.577 -val realpow_Suc_less = thm "realpow_Suc_less";
  25.578 -val realpow_Suc_le = thm "realpow_Suc_le";
  25.579 -val realpow_zero_le = thm "realpow_zero_le";
  25.580 -val realpow_Suc_le2 = thm "realpow_Suc_le2";
  25.581 -val realpow_Suc_le3 = thm "realpow_Suc_le3";
  25.582 -val realpow_less_le = thm "realpow_less_le";
  25.583 -val realpow_le_le = thm "realpow_le_le";
  25.584  val realpow_Suc_le_self = thm "realpow_Suc_le_self";
  25.585  val realpow_Suc_less_one = thm "realpow_Suc_less_one";
  25.586 -val realpow_le_Suc = thm "realpow_le_Suc";
  25.587 -val realpow_less_Suc = thm "realpow_less_Suc";
  25.588 -val realpow_le_Suc2 = thm "realpow_le_Suc2";
  25.589 -val realpow_gt_ge2 = thm "realpow_gt_ge2";
  25.590 -val realpow_ge_ge2 = thm "realpow_ge_ge2";
  25.591 -val realpow_Suc_ge_self2 = thm "realpow_Suc_ge_self2";
  25.592 -val realpow_ge_self2 = thm "realpow_ge_self2";
  25.593  val realpow_minus_mult = thm "realpow_minus_mult";
  25.594  val realpow_two_mult_inverse = thm "realpow_two_mult_inverse";
  25.595  val realpow_two_minus = thm "realpow_two_minus";
  25.596  val realpow_two_disj = thm "realpow_two_disj";
  25.597 -val realpow_diff = thm "realpow_diff";
  25.598  val realpow_real_of_nat = thm "realpow_real_of_nat";
  25.599  val realpow_real_of_nat_two_pos = thm "realpow_real_of_nat_two_pos";
  25.600  val realpow_increasing = thm "realpow_increasing";
  25.601 -val realpow_Suc_cancel_eq = thm "realpow_Suc_cancel_eq";
  25.602 -val realpow_eq_0_iff = thm "realpow_eq_0_iff";
  25.603  val zero_less_realpow_abs_iff = thm "zero_less_realpow_abs_iff";
  25.604  val zero_le_realpow_abs = thm "zero_le_realpow_abs";
  25.605  val real_of_int_power = thm "real_of_int_power";
  25.606  val power_real_number_of = thm "power_real_number_of";
  25.607  val real_power_two = thm "real_power_two";
  25.608 -val real_sqr_ge_zero = thm "real_sqr_ge_zero";
  25.609 -val real_sqr_gt_zero = thm "real_sqr_gt_zero";
  25.610 -val real_sqr_not_zero = thm "real_sqr_not_zero";
  25.611  val real_sum_squares_cancel_a = thm "real_sum_squares_cancel_a";
  25.612  val real_mult_inverse_cancel2 = thm "real_mult_inverse_cancel2";
  25.613  val real_squared_diff_one_factored = thm "real_squared_diff_one_factored";
  25.614 @@ -573,12 +307,8 @@
  25.615  val inverse_real_of_nat_ge_zero = thm "inverse_real_of_nat_ge_zero";
  25.616  val real_sum_squares_not_zero = thm "real_sum_squares_not_zero";
  25.617  val real_sum_squares_not_zero2 = thm "real_sum_squares_not_zero2";
  25.618 -val abs_mult_abs = thm "abs_mult_abs";
  25.619  
  25.620  val realpow_divide = thm "realpow_divide";
  25.621 -val realpow_ge_zero2 = thm "realpow_ge_zero2";
  25.622 -val realpow_le2 = thm "realpow_le2";
  25.623 -val realpow_Suc_gt_one = thm "realpow_Suc_gt_one";
  25.624  val realpow_two_sum_zero_iff = thm "realpow_two_sum_zero_iff";
  25.625  val realpow_two_le_add_order = thm "realpow_two_le_add_order";
  25.626  val realpow_two_le_add_order2 = thm "realpow_two_le_add_order2";
  25.627 @@ -589,8 +319,6 @@
  25.628  val realpow_num_eq_if = thm "realpow_num_eq_if";
  25.629  val real_num_zero_less_two_pow = thm "real_num_zero_less_two_pow";
  25.630  val lemma_realpow_num_two_mono = thm "lemma_realpow_num_two_mono";
  25.631 -val lemma_realpow_4 = thm "lemma_realpow_4";
  25.632 -val lemma_realpow_16 = thm "lemma_realpow_16";
  25.633  val zero_le_x_squared = thm "zero_le_x_squared";
  25.634  *}
  25.635  
    26.1 --- a/src/HOL/Ring_and_Field.thy	Fri Jan 09 01:28:24 2004 +0100
    26.2 +++ b/src/HOL/Ring_and_Field.thy	Fri Jan 09 10:46:18 2004 +0100
    26.3 @@ -38,6 +38,7 @@
    26.4    diff_minus: "a - b = a + (-b)"
    26.5  
    26.6  axclass ordered_semiring \<subseteq> semiring, linorder
    26.7 +  zero_less_one: "0 < 1" --{*This axiom too is needed for semirings only.*}
    26.8    add_left_mono: "a \<le> b ==> c + a \<le> c + b"
    26.9    mult_strict_left_mono: "a < b ==> 0 < c ==> c * a < c * b"
   26.10  
   26.11 @@ -484,6 +485,22 @@
   26.12       "[|a \<le> b; 0 \<le> c|] ==> a*c \<le> b * (c::'a::ordered_semiring)"
   26.13    by (simp add: mult_left_mono mult_commute [of _ c]) 
   26.14  
   26.15 +lemma mult_left_le_imp_le:
   26.16 +     "[|c*a \<le> c*b; 0 < c|] ==> a \<le> (b::'a::ordered_semiring)"
   26.17 +  by (force simp add: mult_strict_left_mono linorder_not_less [symmetric])
   26.18 + 
   26.19 +lemma mult_right_le_imp_le:
   26.20 +     "[|a*c \<le> b*c; 0 < c|] ==> a \<le> (b::'a::ordered_semiring)"
   26.21 +  by (force simp add: mult_strict_right_mono linorder_not_less [symmetric])
   26.22 +
   26.23 +lemma mult_left_less_imp_less:
   26.24 +     "[|c*a < c*b; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)"
   26.25 +  by (force simp add: mult_left_mono linorder_not_le [symmetric])
   26.26 + 
   26.27 +lemma mult_right_less_imp_less:
   26.28 +     "[|a*c < b*c; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)"
   26.29 +  by (force simp add: mult_right_mono linorder_not_le [symmetric])
   26.30 +
   26.31  lemma mult_strict_left_mono_neg:
   26.32       "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring)"
   26.33  apply (drule mult_strict_left_mono [of _ _ "-c"])
   26.34 @@ -552,12 +569,7 @@
   26.35  lemma zero_le_square: "(0::'a::ordered_ring) \<le> a*a"
   26.36  by (simp add: zero_le_mult_iff linorder_linear) 
   26.37  
   26.38 -lemma zero_less_one: "(0::'a::ordered_ring) < 1"
   26.39 -apply (insert zero_le_square [of 1]) 
   26.40 -apply (simp add: order_less_le) 
   26.41 -done
   26.42 -
   26.43 -lemma zero_le_one: "(0::'a::ordered_ring) \<le> 1"
   26.44 +lemma zero_le_one: "(0::'a::ordered_semiring) \<le> 1"
   26.45    by (rule zero_less_one [THEN order_less_imp_le]) 
   26.46  
   26.47  
   26.48 @@ -708,7 +720,7 @@
   26.49  
   26.50  text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement
   26.51        of an ordering.*}
   26.52 -lemma field_mult_eq_0_iff: "(a*b = (0::'a::field)) = (a = 0 | b = 0)"
   26.53 +lemma field_mult_eq_0_iff [simp]: "(a*b = (0::'a::field)) = (a = 0 | b = 0)"
   26.54    proof cases
   26.55      assume "a=0" thus ?thesis by simp
   26.56    next
   26.57 @@ -733,7 +745,7 @@
   26.58      by (simp add: mult_assoc cnz)
   26.59    qed
   26.60  
   26.61 -lemma field_mult_cancel_right:
   26.62 +lemma field_mult_cancel_right [simp]:
   26.63       "(a*c = b*c) = (c = (0::'a::field) | a=b)"
   26.64    proof cases
   26.65      assume "c=0" thus ?thesis by simp
   26.66 @@ -742,7 +754,7 @@
   26.67      thus ?thesis by (force dest: field_mult_cancel_right_lemma)
   26.68    qed
   26.69  
   26.70 -lemma field_mult_cancel_left:
   26.71 +lemma field_mult_cancel_left [simp]:
   26.72       "(c*a = c*b) = (c = (0::'a::field) | a=b)"
   26.73    by (simp add: mult_commute [of c] field_mult_cancel_right) 
   26.74  
   26.75 @@ -1401,6 +1413,10 @@
   26.76                    minus_mult_left [symmetric] minus_mult_right [symmetric])  
   26.77  done
   26.78  
   26.79 +
   26.80 +lemma abs_mult_self: "abs a * abs a = a * (a::'a::ordered_ring)"
   26.81 +by (simp add: abs_if) 
   26.82 +
   26.83  lemma abs_eq_0 [simp]: "(abs a = 0) = (a = (0::'a::ordered_ring))"
   26.84  by (simp add: abs_if)
   26.85  
   26.86 @@ -1617,6 +1633,10 @@
   26.87  val mult_strict_right_mono = thm"mult_strict_right_mono";
   26.88  val mult_left_mono = thm"mult_left_mono";
   26.89  val mult_right_mono = thm"mult_right_mono";
   26.90 +val mult_left_le_imp_le = thm"mult_left_le_imp_le";
   26.91 +val mult_right_le_imp_le = thm"mult_right_le_imp_le";
   26.92 +val mult_left_less_imp_less = thm"mult_left_less_imp_less";
   26.93 +val mult_right_less_imp_less = thm"mult_right_less_imp_less";
   26.94  val mult_strict_left_mono_neg = thm"mult_strict_left_mono_neg";
   26.95  val mult_strict_right_mono_neg = thm"mult_strict_right_mono_neg";
   26.96  val mult_pos = thm"mult_pos";
   26.97 @@ -1744,6 +1764,7 @@
   26.98  val abs_zero = thm"abs_zero";
   26.99  val abs_one = thm"abs_one";
  26.100  val abs_mult = thm"abs_mult";
  26.101 +val abs_mult_self = thm"abs_mult_self";
  26.102  val abs_eq_0 = thm"abs_eq_0";
  26.103  val zero_less_abs_iff = thm"zero_less_abs_iff";
  26.104  val abs_not_less_zero = thm"abs_not_less_zero";