Defining the type class "ringpower" and deleting superseded theorems for
types nat, int, real, hypreal
--- a/src/HOL/Complex/CLim.ML Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/Complex/CLim.ML Fri Jan 09 10:46:18 2004 +0100
@@ -852,13 +852,10 @@
Goal "NSCDERIV f x :> D ==> NSCDERIV (%x. c * f x) x :> c*D";
by (asm_full_simp_tac
- (simpset() addsimps [complex_times_divide1_eq RS sym, NSCDERIV_NSCLIM_iff,
- complex_minus_mult_eq2, complex_add_mult_distrib2 RS sym,
+ (simpset() addsimps [times_divide_eq_right RS sym, NSCDERIV_NSCLIM_iff,
+ minus_mult_right, complex_add_mult_distrib2 RS sym,
complex_diff_def]
- delsimps [complex_times_divide1_eq, complex_minus_mult_eq2 RS sym]
- delsimps [times_divide_eq_right, minus_mult_right RS sym]
-
-) 1);
+ delsimps [times_divide_eq_right, minus_mult_right RS sym]) 1);
by (etac (NSCLIM_const RS NSCLIM_mult) 1);
qed "NSCDERIV_cmult";
--- a/src/HOL/Complex/Complex.thy Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/Complex/Complex.thy Fri Jan 09 10:46:18 2004 +0100
@@ -577,119 +577,8 @@
qed
-lemma complex_mult_minus_one: "-(1::complex) * z = -z"
-apply (simp (no_asm))
-done
-declare complex_mult_minus_one [simp]
-
-lemma complex_mult_minus_one_right: "z * -(1::complex) = -z"
-apply (subst complex_mult_commute)
-apply (simp (no_asm))
-done
-declare complex_mult_minus_one_right [simp]
-
-lemma complex_minus_mult_cancel: "-x * -y = x * (y::complex)"
-apply (simp (no_asm))
-done
-declare complex_minus_mult_cancel [simp]
-
lemma complex_minus_mult_commute: "-x * y = x * -(y::complex)"
-apply (simp (no_asm))
-done
-
-
-lemma complex_mult_left_cancel: "(c::complex) ~= 0 ==> (c*a=c*b) = (a=b)"
-apply auto
-apply (drule_tac f = "%x. x*inverse c" in arg_cong)
-apply (simp add: complex_mult_ac)
-done
-
-lemma complex_mult_right_cancel: "(c::complex) ~= 0 ==> (a*c=b*c) = (a=b)"
-apply safe
-apply (drule_tac f = "%x. x*inverse c" in arg_cong)
-apply (simp add: complex_mult_ac)
-done
-
-lemma complex_inverse_not_zero: "z ~= 0 ==> inverse(z::complex) ~= 0"
-apply safe
-apply (frule complex_mult_right_cancel [THEN iffD2])
-apply (erule_tac [2] V = "inverse z = 0" in thin_rl)
-apply (assumption, auto)
-done
-declare complex_inverse_not_zero [simp]
-
-lemma complex_mult_not_zero: "!!x. [| x ~= 0; y ~= (0::complex) |] ==> x * y ~= 0"
-apply safe
-apply (drule_tac f = "%z. inverse x*z" in arg_cong)
-apply (simp add: complex_mult_assoc [symmetric])
-done
-
-lemmas complex_mult_not_zeroE = complex_mult_not_zero [THEN notE, standard]
-
-lemma complex_inverse_inverse: "inverse(inverse (x::complex)) = x"
-apply (case_tac "x = 0", simp add: COMPLEX_INVERSE_ZERO)
-apply (rule_tac c1 = "inverse x" in complex_mult_right_cancel [THEN iffD1])
-apply (erule complex_inverse_not_zero)
-apply (auto dest: complex_inverse_not_zero)
-done
-declare complex_inverse_inverse [simp]
-
-lemma complex_inverse_one: "inverse(1::complex) = 1"
-apply (unfold complex_one_def)
-apply (simp (no_asm) add: complex_inverse)
-done
-declare complex_inverse_one [simp]
-
-lemma complex_minus_inverse: "inverse(-x) = -inverse(x::complex)"
-apply (case_tac "x = 0", simp add: COMPLEX_INVERSE_ZERO)
-apply (rule_tac c1 = "-x" in complex_mult_right_cancel [THEN iffD1], force)
-apply (subst complex_mult_inv_left, auto)
-done
-
-lemma complex_inverse_distrib: "inverse(x*y) = inverse x * inverse (y::complex)"
-apply (rule inverse_mult_distrib)
-done
-
-
-subsection{*Division*}
-
-(*adding some of these theorems to simpset as for reals:
- not 100% convinced for some*)
-
-lemma complex_times_divide1_eq: "(x::complex) * (y/z) = (x*y)/z"
-apply (simp (no_asm) add: complex_divide_def complex_mult_assoc)
-done
-
-lemma complex_times_divide2_eq: "(y/z) * (x::complex) = (y*x)/z"
-apply (simp (no_asm) add: complex_divide_def complex_mult_ac)
-done
-
-declare complex_times_divide1_eq [simp] complex_times_divide2_eq [simp]
-
-lemma complex_divide_divide1_eq: "(x::complex) / (y/z) = (x*z)/y"
-apply (simp (no_asm) add: complex_divide_def complex_inverse_distrib complex_mult_ac)
-done
-
-lemma complex_divide_divide2_eq: "((x::complex) / y) / z = x/(y*z)"
-apply (simp (no_asm) add: complex_divide_def complex_inverse_distrib complex_mult_assoc)
-done
-
-declare complex_divide_divide1_eq [simp] complex_divide_divide2_eq [simp]
-
-(** As with multiplication, pull minus signs OUT of the / operator **)
-
-lemma complex_minus_divide_eq: "(-x) / (y::complex) = - (x/y)"
-apply (simp (no_asm) add: complex_divide_def)
-done
-declare complex_minus_divide_eq [simp]
-
-lemma complex_divide_minus_eq: "(x / -(y::complex)) = - (x/y)"
-apply (simp (no_asm) add: complex_divide_def complex_minus_inverse)
-done
-declare complex_divide_minus_eq [simp]
-
-lemma complex_add_divide_distrib: "(x+y)/(z::complex) = x/z + y/z"
-apply (simp (no_asm) add: complex_divide_def complex_add_mult_distrib)
+apply (simp)
done
subsection{*Embedding Properties for @{term complex_of_real} Map*}
@@ -713,7 +602,8 @@
done
declare complex_of_real_zero [simp]
-lemma complex_of_real_eq_iff: "(complex_of_real x = complex_of_real y) = (x = y)"
+lemma complex_of_real_eq_iff:
+ "(complex_of_real x = complex_of_real y) = (x = y)"
by (auto dest: inj_complex_of_real [THEN injD])
declare complex_of_real_eq_iff [iff]
@@ -721,22 +611,25 @@
apply (simp (no_asm) add: complex_of_real_def complex_minus)
done
-lemma complex_of_real_inverse: "complex_of_real(inverse x) = inverse(complex_of_real x)"
-apply (case_tac "x=0")
-apply (simp add: DIVISION_BY_ZERO COMPLEX_INVERSE_ZERO)
+lemma complex_of_real_inverse:
+ "complex_of_real(inverse x) = inverse(complex_of_real x)"
+apply (case_tac "x=0", simp)
apply (simp add: complex_inverse complex_of_real_def real_divide_def
inverse_mult_distrib real_power_two)
done
-lemma complex_of_real_add: "complex_of_real x + complex_of_real y = complex_of_real (x + y)"
+lemma complex_of_real_add:
+ "complex_of_real x + complex_of_real y = complex_of_real (x + y)"
apply (simp (no_asm) add: complex_add complex_of_real_def)
done
-lemma complex_of_real_diff: "complex_of_real x - complex_of_real y = complex_of_real (x - y)"
+lemma complex_of_real_diff:
+ "complex_of_real x - complex_of_real y = complex_of_real (x - y)"
apply (simp (no_asm) add: complex_of_real_minus [symmetric] complex_diff_def complex_of_real_add)
done
-lemma complex_of_real_mult: "complex_of_real x * complex_of_real y = complex_of_real (x * y)"
+lemma complex_of_real_mult:
+ "complex_of_real x * complex_of_real y = complex_of_real (x * y)"
apply (simp (no_asm) add: complex_mult complex_of_real_def)
done
@@ -764,19 +657,18 @@
done
declare complex_mod_zero [simp]
-lemma complex_mod_one: "cmod(1) = 1"
-by (unfold cmod_def, simp)
-declare complex_mod_one [simp]
+lemma complex_mod_one [simp]: "cmod(1) = 1"
+by (simp add: cmod_def real_power_two)
lemma complex_mod_complex_of_real: "cmod(complex_of_real x) = abs x"
-apply (unfold complex_of_real_def)
-apply (simp (no_asm) add: complex_mod)
+apply (simp add: complex_of_real_def real_power_two complex_mod)
done
declare complex_mod_complex_of_real [simp]
-lemma complex_of_real_abs: "complex_of_real (abs x) = complex_of_real(cmod(complex_of_real x))"
-apply (simp (no_asm))
-done
+lemma complex_of_real_abs:
+ "complex_of_real (abs x) = complex_of_real(cmod(complex_of_real x))"
+by (simp)
+
subsection{*Conjugation is an Automorphism*}
@@ -801,7 +693,8 @@
done
declare complex_cnj_cnj [simp]
-lemma complex_cnj_complex_of_real: "cnj (complex_of_real x) = complex_of_real x"
+lemma complex_cnj_complex_of_real:
+ "cnj (complex_of_real x) = complex_of_real x"
apply (unfold complex_of_real_def)
apply (simp (no_asm) add: complex_cnj)
done
@@ -884,12 +777,6 @@
subsection{*Algebra*}
-lemma complex_mult_zero_iff: "(x*y = (0::complex)) = (x = 0 | y = 0)"
-apply auto
-apply (auto intro: ccontr dest: complex_mult_not_zero)
-done
-declare complex_mult_zero_iff [iff]
-
lemma complex_add_left_cancel_zero: "(x + y = x) = (y = (0::complex))"
apply (unfold complex_zero_def)
apply (rule_tac z = x in eq_Abs_complex)
@@ -913,13 +800,6 @@
subsection{*Modulus*}
-(*
-Goal "[| sqrt(x) = 0; 0 <= x |] ==> x = 0"
-by (auto_tac (claset() addIs [real_sqrt_eq_zero_cancel],
- simpset()));
-qed "real_sqrt_eq_zero_cancel2";
-*)
-
lemma complex_mod_eq_zero_cancel: "(cmod x = 0) = (x = 0)"
apply (rule_tac z = x in eq_Abs_complex)
apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 simp add: complex_mod complex_zero_def real_power_two)
@@ -960,7 +840,7 @@
apply (rule_tac z = x in eq_Abs_complex)
apply (rule_tac z = y in eq_Abs_complex)
apply (auto simp add: complex_mult complex_mod real_sqrt_mult_distrib2 [symmetric] simp del: realpow_Suc)
-apply (rule_tac n = 1 in realpow_Suc_cancel_eq)
+apply (rule_tac n = 1 in power_inject_base)
apply (auto simp add: real_power_two [symmetric] simp del: realpow_Suc)
apply (auto simp add: real_diff_def real_power_two right_distrib left_distrib add_ac mult_ac)
done
@@ -1087,7 +967,7 @@
lemma complex_inverse_divide:
"inverse(x/y) = y/(x::complex)"
apply (unfold complex_divide_def)
-apply (auto simp add: complex_inverse_distrib complex_mult_commute)
+apply (auto simp add: inverse_mult_distrib complex_mult_commute)
done
declare complex_inverse_divide [simp]
@@ -1105,7 +985,7 @@
lemma complexpow_not_zero [rule_format (no_asm)]: "r ~= (0::complex) --> r ^ n ~= 0"
apply (induct_tac "n")
-apply (auto simp add: complex_mult_not_zero)
+apply (auto simp add: )
done
declare complexpow_not_zero [simp]
declare complexpow_not_zero [intro]
@@ -1135,7 +1015,7 @@
lemma complexpow_inverse: "inverse ((r::complex) ^ n) = (inverse r) ^ n"
apply (induct_tac "n")
-apply (auto simp add: complex_inverse_distrib)
+apply (auto simp add: inverse_mult_distrib)
done
(*---------------------------------------------------------------------------*)
@@ -1383,21 +1263,22 @@
by (unfold rcis_def cis_def, auto)
declare Re_rcis [simp]
-lemma Im_complex_polar: "Im(complex_of_real r *
- (complex_of_real(cos a) + ii * complex_of_real(sin a))) = r * sin a"
-apply (auto simp add: complex_add_mult_distrib2 complex_of_real_mult complex_mult_ac)
-done
-declare Im_complex_polar [simp]
+lemma Im_complex_polar [simp]:
+ "Im(complex_of_real r *
+ (complex_of_real(cos a) + ii * complex_of_real(sin a))) =
+ r * sin a"
+by (auto simp add: complex_add_mult_distrib2 complex_of_real_mult mult_ac)
-lemma Im_rcis: "Im(rcis r a) = r * sin a"
+lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a"
by (unfold rcis_def cis_def, auto)
-declare Im_rcis [simp]
-lemma complex_mod_complex_polar: "cmod (complex_of_real r *
- (complex_of_real(cos a) + ii * complex_of_real(sin a))) = abs r"
-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)
-done
-declare complex_mod_complex_polar [simp]
+lemma complex_mod_complex_polar [simp]:
+ "cmod (complex_of_real r *
+ (complex_of_real(cos a) + ii * complex_of_real(sin a))) =
+ abs r"
+by (auto simp add: complex_add_mult_distrib2 cmod_i complex_of_real_mult
+ right_distrib [symmetric] power_mult_distrib mult_ac
+ simp del: realpow_Suc)
lemma complex_mod_rcis: "cmod(rcis r a) = abs r"
by (unfold rcis_def cis_def, auto)
@@ -1728,9 +1609,6 @@
val complex_divide_zero = thm"complex_divide_zero";
val complex_minus_mult_eq1 = thm"complex_minus_mult_eq1";
val complex_minus_mult_eq2 = thm"complex_minus_mult_eq2";
-val complex_mult_minus_one = thm"complex_mult_minus_one";
-val complex_mult_minus_one_right = thm"complex_mult_minus_one_right";
-val complex_minus_mult_cancel = thm"complex_minus_mult_cancel";
val complex_minus_mult_commute = thm"complex_minus_mult_commute";
val complex_add_mult_distrib = thm"complex_add_mult_distrib";
val complex_add_mult_distrib2 = thm"complex_add_mult_distrib2";
@@ -1740,21 +1618,6 @@
val COMPLEX_DIVISION_BY_ZERO = thm"COMPLEX_DIVISION_BY_ZERO";
val complex_mult_inv_left = thm"complex_mult_inv_left";
val complex_mult_inv_right = thm"complex_mult_inv_right";
-val complex_mult_left_cancel = thm"complex_mult_left_cancel";
-val complex_mult_right_cancel = thm"complex_mult_right_cancel";
-val complex_inverse_not_zero = thm"complex_inverse_not_zero";
-val complex_mult_not_zero = thm"complex_mult_not_zero";
-val complex_inverse_inverse = thm"complex_inverse_inverse";
-val complex_inverse_one = thm"complex_inverse_one";
-val complex_minus_inverse = thm"complex_minus_inverse";
-val complex_inverse_distrib = thm"complex_inverse_distrib";
-val complex_times_divide1_eq = thm"complex_times_divide1_eq";
-val complex_times_divide2_eq = thm"complex_times_divide2_eq";
-val complex_divide_divide1_eq = thm"complex_divide_divide1_eq";
-val complex_divide_divide2_eq = thm"complex_divide_divide2_eq";
-val complex_minus_divide_eq = thm"complex_minus_divide_eq";
-val complex_divide_minus_eq = thm"complex_divide_minus_eq";
-val complex_add_divide_distrib = thm"complex_add_divide_distrib";
val inj_complex_of_real = thm"inj_complex_of_real";
val complex_of_real_one = thm"complex_of_real_one";
val complex_of_real_zero = thm"complex_of_real_zero";
@@ -1790,7 +1653,6 @@
val complex_cnj_zero = thm"complex_cnj_zero";
val complex_cnj_zero_iff = thm"complex_cnj_zero_iff";
val complex_mult_cnj = thm"complex_mult_cnj";
-val complex_mult_zero_iff = thm"complex_mult_zero_iff";
val complex_add_left_cancel_zero = thm"complex_add_left_cancel_zero";
val complex_diff_mult_distrib = thm"complex_diff_mult_distrib";
val complex_diff_mult_distrib2 = thm"complex_diff_mult_distrib2";
--- a/src/HOL/Complex/ComplexArith0.ML Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/Complex/ComplexArith0.ML Fri Jan 09 10:46:18 2004 +0100
@@ -168,7 +168,7 @@
Addsimps [complex_divide_minus1];
Goal "-1/(x::complex) = - (1/x)";
-by (simp_tac (simpset() addsimps [complex_divide_def, complex_minus_inverse]) 1);
+by (simp_tac (simpset() addsimps [complex_divide_def, inverse_minus_eq]) 1);
qed "complex_minus1_divide";
Addsimps [complex_minus1_divide];
--- a/src/HOL/Hyperreal/HTranscendental.ML Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/Hyperreal/HTranscendental.ML Fri Jan 09 10:46:18 2004 +0100
@@ -4,6 +4,8 @@
Description : Nonstandard extensions of transcendental functions
*)
+val hpowr_Suc= thm"hpowr_Suc";
+
(*-------------------------------------------------------------------------*)
(* NS extension of square root function *)
(*-------------------------------------------------------------------------*)
@@ -44,8 +46,7 @@
qed "hypreal_sqrt_not_zero";
Goal "0 < x ==> inverse (( *f* sqrt)(x)) ^ 2 = inverse x";
-by (forward_tac [hypreal_sqrt_not_zero] 1);
-by (dres_inst_tac [("n1","2"),("r1","( *f* sqrt) x")] (hrealpow_inverse RS sym) 1);
+by (cut_inst_tac [("n1","2"),("a1","( *f* sqrt) x")] (power_inverse RS sym) 1);
by (auto_tac (claset() addDs [hypreal_sqrt_gt_zero_pow2],simpset()));
qed "hypreal_inverse_sqrt_pow2";
@@ -81,14 +82,14 @@
Goal "(( *f* sqrt)(x*x + y*y + z*z) @= 0) = (x*x + y*y + z*z @= 0)";
by (rtac hypreal_sqrt_approx_zero2 1);
by (REPEAT(rtac hypreal_le_add_order 1));
-by Auto_tac;
+by (auto_tac (claset(), simpset() addsimps [zero_le_square]));
qed "hypreal_sqrt_sum_squares";
Addsimps [hypreal_sqrt_sum_squares];
Goal "(( *f* sqrt)(x*x + y*y) @= 0) = (x*x + y*y @= 0)";
by (rtac hypreal_sqrt_approx_zero2 1);
by (rtac hypreal_le_add_order 1);
-by Auto_tac;
+by (auto_tac (claset(), simpset() addsimps [zero_le_square]));
qed "hypreal_sqrt_sum_squares2";
Addsimps [hypreal_sqrt_sum_squares2];
@@ -126,15 +127,15 @@
Addsimps [hypreal_sqrt_hyperpow_hrabs];
Goal "[| x: HFinite; 0 <= x |] ==> st(( *f* sqrt) x) = ( *f* sqrt)(st x)";
-by (res_inst_tac [("n","1")] hrealpow_Suc_cancel_eq 1);
+by (res_inst_tac [("n","1")] power_inject_base 1);
by (auto_tac (claset() addSIs [st_zero_le,hypreal_sqrt_ge_zero],simpset()));
-by (rtac (st_mult RS subst) 2);
-by (rtac (hypreal_sqrt_mult_distrib2 RS subst) 4);
-by (rtac (hypreal_sqrt_mult_distrib2 RS subst) 6);
+by (rtac (st_mult RS subst) 1);
+by (rtac (hypreal_sqrt_mult_distrib2 RS subst) 3);
+by (rtac (hypreal_sqrt_mult_distrib2 RS subst) 5);
by (auto_tac (claset(), simpset() addsimps [st_hrabs,st_zero_le]));
by (ALLGOALS(rtac (HFinite_square_iff RS iffD1)));
-by (auto_tac (claset(),simpset() addsimps
- [hypreal_sqrt_mult_distrib2 RS sym]
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_sqrt_mult_distrib2 RS sym]
delsimps [HFinite_square_iff]));
qed "st_hypreal_sqrt";
@@ -169,7 +170,7 @@
Goal "(( *f* sqrt)(x*x + y*y) : HFinite) = (x*x + y*y : HFinite)";
by (rtac HFinite_hypreal_sqrt_iff 1);
by (rtac hypreal_le_add_order 1);
-by Auto_tac;
+by (auto_tac (claset(), simpset() addsimps [zero_le_square]));
qed "HFinite_sqrt_sum_squares";
Addsimps [HFinite_sqrt_sum_squares];
@@ -197,7 +198,7 @@
Goal "(( *f* sqrt)(x*x + y*y) : Infinitesimal) = (x*x + y*y : Infinitesimal)";
by (rtac Infinitesimal_hypreal_sqrt_iff 1);
by (rtac hypreal_le_add_order 1);
-by Auto_tac;
+by (auto_tac (claset(), simpset() addsimps [zero_le_square]));
qed "Infinitesimal_sqrt_sum_squares";
Addsimps [Infinitesimal_sqrt_sum_squares];
@@ -225,7 +226,7 @@
Goal "(( *f* sqrt)(x*x + y*y) : HInfinite) = (x*x + y*y : HInfinite)";
by (rtac HInfinite_hypreal_sqrt_iff 1);
by (rtac hypreal_le_add_order 1);
-by Auto_tac;
+by (auto_tac (claset(), simpset() addsimps [zero_le_square]));
qed "HInfinite_sqrt_sum_squares";
Addsimps [HInfinite_sqrt_sum_squares];
--- a/src/HOL/Hyperreal/HyperDef.thy Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy Fri Jan 09 10:46:18 2004 +0100
@@ -697,8 +697,12 @@
instance hypreal :: ordered_field
proof
fix x y z :: hypreal
- show "x \<le> y ==> z + x \<le> z + y" by (rule hypreal_add_left_le_mono1)
- show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: hypreal_mult_less_mono2)
+ show "0 < (1::hypreal)"
+ by (unfold hypreal_one_def hypreal_zero_def hypreal_less_def, force)
+ show "x \<le> y ==> z + x \<le> z + y"
+ by (rule hypreal_add_left_le_mono1)
+ show "x < y ==> 0 < z ==> z * x < z * y"
+ by (simp add: hypreal_mult_less_mono2)
show "\<bar>x\<bar> = (if x < 0 then -x else x)"
by (auto dest: order_le_less_trans simp add: hrabs_def linorder_not_le)
qed
--- a/src/HOL/Hyperreal/HyperPow.ML Fri Jan 09 01:28:24 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,547 +0,0 @@
-(* Title : HyperPow.ML
- Author : Jacques D. Fleuriot
- Copyright : 1998 University of Cambridge
- Description : Natural Powers of hyperreals theory
-
-Exponentials on the hyperreals
-*)
-
-Goal "(0::hypreal) ^ (Suc n) = 0";
-by Auto_tac;
-qed "hrealpow_zero";
-Addsimps [hrealpow_zero];
-
-Goal "r ~= (0::hypreal) --> r ^ n ~= 0";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed_spec_mp "hrealpow_not_zero";
-
-Goal "r ~= (0::hypreal) --> inverse(r ^ n) = (inverse r) ^ n";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed_spec_mp "hrealpow_inverse";
-
-Goal "abs (r::hypreal) ^ n = abs (r ^ n)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "hrealpow_hrabs";
-
-Goal "(r::hypreal) ^ (n + m) = (r ^ n) * (r ^ m)";
-by (induct_tac "n" 1);
-by (auto_tac (claset(), simpset() addsimps mult_ac));
-qed "hrealpow_add";
-
-Goal "(r::hypreal) ^ Suc 0 = r";
-by (Simp_tac 1);
-qed "hrealpow_one";
-Addsimps [hrealpow_one];
-
-Goal "(r::hypreal) ^ Suc (Suc 0) = r * r";
-by (Simp_tac 1);
-qed "hrealpow_two";
-
-Goal "(0::hypreal) <= r --> 0 <= r ^ n";
-by (induct_tac "n" 1);
-by (auto_tac (claset(), simpset() addsimps [zero_le_mult_iff]));
-qed_spec_mp "hrealpow_ge_zero";
-
-Goal "(0::hypreal) < r --> 0 < r ^ n";
-by (induct_tac "n" 1);
-by (auto_tac (claset(), simpset() addsimps [zero_less_mult_iff]));
-qed_spec_mp "hrealpow_gt_zero";
-
-Goal "x <= y & (0::hypreal) < x --> x ^ n <= y ^ n";
-by (induct_tac "n" 1);
-by (auto_tac (claset() addSIs [mult_mono], simpset()));
-by (asm_simp_tac (simpset() addsimps [hrealpow_ge_zero]) 1);
-qed_spec_mp "hrealpow_le";
-
-Goal "x < y & (0::hypreal) < x & 0 < n --> x ^ n < y ^ n";
-by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [hypreal_mult_less_mono,gr0I],
- simpset() addsimps [hrealpow_gt_zero]));
-qed "hrealpow_less";
-
-Goal "1 ^ n = (1::hypreal)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "hrealpow_eq_one";
-Addsimps [hrealpow_eq_one];
-
-Goal "abs(-(1 ^ n)) = (1::hypreal)";
-by Auto_tac;
-qed "hrabs_minus_hrealpow_one";
-Addsimps [hrabs_minus_hrealpow_one];
-
-Goal "abs(-1 ^ n) = (1::hypreal)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "hrabs_hrealpow_minus_one";
-Addsimps [hrabs_hrealpow_minus_one];
-
-Goal "((r::hypreal) * s) ^ n = (r ^ n) * (s ^ n)";
-by (induct_tac "n" 1);
-by (auto_tac (claset(), simpset() addsimps mult_ac));
-qed "hrealpow_mult";
-
-Goal "(0::hypreal) <= r ^ Suc (Suc 0)";
-by (auto_tac (claset(), simpset() addsimps [zero_le_mult_iff]));
-qed "hrealpow_two_le";
-Addsimps [hrealpow_two_le];
-
-Goal "(0::hypreal) <= u ^ Suc (Suc 0) + v ^ Suc (Suc 0)";
-by (simp_tac (HOL_ss addsimps [hrealpow_two_le, hypreal_le_add_order]) 1);
-qed "hrealpow_two_le_add_order";
-Addsimps [hrealpow_two_le_add_order];
-
-Goal "(0::hypreal) <= u ^ Suc (Suc 0) + v ^ Suc (Suc 0) + w ^ Suc (Suc 0)";
-by (simp_tac (HOL_ss addsimps [hrealpow_two_le, hypreal_le_add_order]) 1);
-qed "hrealpow_two_le_add_order2";
-Addsimps [hrealpow_two_le_add_order2];
-
-Goal "[| 0 <= x; 0 <= y |] ==> (x+y = 0) = (x = 0 & y = (0::hypreal))";
-by (auto_tac (claset() addIs [order_antisym], simpset()));
-qed "hypreal_add_nonneg_eq_0_iff";
-
-Goal "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))";
-by (simp_tac (HOL_ss addsimps [zero_le_square, hypreal_le_add_order,
- hypreal_add_nonneg_eq_0_iff]) 1);
-by Auto_tac;
-qed "hypreal_three_squares_add_zero_iff";
-
-Goal "(x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = (0::hypreal)) = (x = 0 & y = 0 & z = 0)";
-by (simp_tac (HOL_ss addsimps
- [hypreal_three_squares_add_zero_iff, hrealpow_two]) 1);
-qed "hrealpow_three_squares_add_zero_iff";
-Addsimps [hrealpow_three_squares_add_zero_iff];
-
-Goal "abs(x ^ Suc (Suc 0)) = (x::hypreal) ^ Suc (Suc 0)";
-by (auto_tac (claset(),
- simpset() addsimps [hrabs_def, zero_le_mult_iff]));
-qed "hrabs_hrealpow_two";
-Addsimps [hrabs_hrealpow_two];
-
-Goal "abs(x) ^ Suc (Suc 0) = (x::hypreal) ^ Suc (Suc 0)";
-by (simp_tac (simpset() addsimps [hrealpow_hrabs, hrabs_eqI1]
- delsimps [hpowr_Suc]) 1);
-qed "hrealpow_two_hrabs";
-Addsimps [hrealpow_two_hrabs];
-
-Goal "(1::hypreal) < r ==> 1 < r ^ Suc (Suc 0)";
-by (auto_tac (claset(), simpset() addsimps [hrealpow_two]));
-by (res_inst_tac [("y","1*1")] order_le_less_trans 1);
-by (rtac hypreal_mult_less_mono 2);
-by Auto_tac;
-qed "hrealpow_two_gt_one";
-
-Goal "(1::hypreal) <= r ==> 1 <= r ^ Suc (Suc 0)";
-by (etac (order_le_imp_less_or_eq RS disjE) 1);
-by (etac (hrealpow_two_gt_one RS order_less_imp_le) 1);
-by Auto_tac;
-qed "hrealpow_two_ge_one";
-
-Goal "(1::hypreal) <= 2 ^ n";
-by (res_inst_tac [("y","1 ^ n")] order_trans 1);
-by (rtac hrealpow_le 2);
-by Auto_tac;
-qed "two_hrealpow_ge_one";
-
-Goal "hypreal_of_nat n < 2 ^ n";
-by (induct_tac "n" 1);
-by (auto_tac (claset(),
- simpset() addsimps [hypreal_of_nat_Suc, left_distrib]));
-by (cut_inst_tac [("n","n")] two_hrealpow_ge_one 1);
-by (arith_tac 1);
-qed "two_hrealpow_gt";
-Addsimps [two_hrealpow_gt,two_hrealpow_ge_one];
-
-Goal "-1 ^ (2*n) = (1::hypreal)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "hrealpow_minus_one";
-
-Goal "n+n = (2*n::nat)";
-by Auto_tac;
-qed "double_lemma";
-
-(*ugh: need to get rid fo the n+n*)
-Goal "-1 ^ (n + n) = (1::hypreal)";
-by (auto_tac (claset(),
- simpset() addsimps [double_lemma, hrealpow_minus_one]));
-qed "hrealpow_minus_one2";
-Addsimps [hrealpow_minus_one2];
-
-Goal "(-(x::hypreal)) ^ Suc (Suc 0) = x ^ Suc (Suc 0)";
-by Auto_tac;
-qed "hrealpow_minus_two";
-Addsimps [hrealpow_minus_two];
-
-Goal "(0::hypreal) < r & r < 1 --> r ^ Suc n < r ^ n";
-by (induct_tac "n" 1);
-by (auto_tac (claset(),
- simpset() addsimps [hypreal_mult_less_mono2]));
-qed_spec_mp "hrealpow_Suc_less";
-
-Goal "(0::hypreal) <= r & r < 1 --> r ^ Suc n <= r ^ n";
-by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [order_less_imp_le]
- addSDs [order_le_imp_less_or_eq,hrealpow_Suc_less],
- simpset() addsimps [hypreal_mult_less_mono2]));
-qed_spec_mp "hrealpow_Suc_le";
-
-Goal "Abs_hypreal(hyprel``{%n. X n}) ^ m = Abs_hypreal(hyprel``{%n. (X n) ^ m})";
-by (induct_tac "m" 1);
-by (auto_tac (claset(),
- simpset() addsimps [hypreal_one_def, hypreal_mult]));
-qed "hrealpow";
-
-Goal "(x + (y::hypreal)) ^ Suc (Suc 0) = \
-\ x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0)))*x*y";
-by (simp_tac (simpset() addsimps
- [right_distrib, left_distrib,
- hypreal_of_nat_zero, hypreal_of_nat_Suc]) 1);
-qed "hrealpow_sum_square_expand";
-
-
-(*** Literal arithmetic involving powers, type hypreal ***)
-
-Goal "hypreal_of_real (x ^ n) = hypreal_of_real x ^ n";
-by (induct_tac "n" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [nat_mult_distrib])));
-qed "hypreal_of_real_power";
-Addsimps [hypreal_of_real_power];
-
-Goal "(number_of v :: hypreal) ^ n = hypreal_of_real ((number_of v) ^ n)";
-by (simp_tac (HOL_ss addsimps [hypreal_number_of_def,
- hypreal_of_real_power]) 1);
-qed "power_hypreal_of_real_number_of";
-
-Addsimps [inst "n" "number_of ?w" power_hypreal_of_real_number_of];
-
-(*---------------------------------------------------------------
- we'll prove the following theorem by going down to the
- level of the ultrafilter and relying on the analogous
- property for the real rather than prove it directly
- using induction: proof is much simpler this way!
- ---------------------------------------------------------------*)
-Goal "[|(0::hypreal) <= x; 0 <= y;x ^ Suc n <= y ^ Suc n |] ==> x <= y";
-by (full_simp_tac (simpset() addsimps [hypreal_zero_def]) 1);
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),
- simpset() addsimps [hrealpow,hypreal_le,hypreal_mult]));
-by (ultra_tac (claset() addIs [realpow_increasing], simpset()) 1);
-qed "hrealpow_increasing";
-
-(*By antisymmetry with the above we conclude x=y, replacing the deleted
- theorem hrealpow_Suc_cancel_eq*)
-
-Goal "x : HFinite --> x ^ n : HFinite";
-by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [HFinite_mult], simpset()));
-qed_spec_mp "hrealpow_HFinite";
-
-(*---------------------------------------------------------------
- Hypernaturals Powers
- --------------------------------------------------------------*)
-Goalw [congruent_def]
- "congruent hyprel \
-\ (%X Y. hyprel``{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})";
-by (auto_tac (claset() addSIs [ext], simpset()));
-by (ALLGOALS(Fuf_tac));
-qed "hyperpow_congruent";
-
-Goalw [hyperpow_def]
- "Abs_hypreal(hyprel``{%n. X n}) pow Abs_hypnat(hypnatrel``{%n. Y n}) = \
-\ Abs_hypreal(hyprel``{%n. X n ^ Y n})";
-by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
-by (auto_tac (claset() addSIs [lemma_hyprel_refl,bexI],
- simpset() addsimps [hyprel_in_hypreal RS
- Abs_hypreal_inverse,equiv_hyprel,hyperpow_congruent]));
-by (Fuf_tac 1);
-qed "hyperpow";
-
-Goalw [hypnat_one_def] "(0::hypreal) pow (n + (1::hypnat)) = 0";
-by (simp_tac (simpset() addsimps [hypreal_zero_def]) 1);
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(), simpset() addsimps [hyperpow,hypnat_add]));
-qed "hyperpow_zero";
-Addsimps [hyperpow_zero];
-
-Goal "r ~= (0::hypreal) --> r pow n ~= 0";
-by (simp_tac (simpset() addsimps [hypreal_zero_def]) 1);
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset(), simpset() addsimps [hyperpow]));
-by (dtac FreeUltrafilterNat_Compl_mem 1);
-by (fuf_empty_tac (claset() addIs [realpow_not_zero RS notE],
- simpset()) 1);
-qed_spec_mp "hyperpow_not_zero";
-
-Goal "r ~= (0::hypreal) --> inverse(r pow n) = (inverse r) pow n";
-by (simp_tac (simpset() addsimps [hypreal_zero_def]) 1);
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset() addSDs [FreeUltrafilterNat_Compl_mem],
- simpset() addsimps [hypreal_inverse,hyperpow]));
-by (rtac FreeUltrafilterNat_subset 1);
-by (auto_tac (claset() addDs [realpow_not_zero]
- addIs [realpow_inverse],
- simpset()));
-qed "hyperpow_inverse";
-
-Goal "abs r pow n = abs (r pow n)";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),
- simpset() addsimps [hypreal_hrabs, hyperpow,realpow_abs RS sym]));
-qed "hyperpow_hrabs";
-
-Goal "r pow (n + m) = (r pow n) * (r pow m)";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),
- simpset() addsimps [hyperpow,hypnat_add, hypreal_mult,realpow_add]));
-qed "hyperpow_add";
-
-Goalw [hypnat_one_def] "r pow (1::hypnat) = r";
-by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset(), simpset() addsimps [hyperpow]));
-qed "hyperpow_one";
-Addsimps [hyperpow_one];
-
-Goalw [hypnat_one_def]
- "r pow ((1::hypnat) + (1::hypnat)) = r * r";
-by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),
- simpset() addsimps [hyperpow,hypnat_add, hypreal_mult]));
-qed "hyperpow_two";
-
-Goal "(0::hypreal) < r --> 0 < r pow n";
-by (simp_tac (simpset() addsimps [hypreal_zero_def]) 1);
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset, realpow_gt_zero],
- simpset() addsimps [hyperpow,hypreal_less, hypreal_le]));
-qed_spec_mp "hyperpow_gt_zero";
-
-Goal "(0::hypreal) <= r --> 0 <= r pow n";
-by (simp_tac (simpset() addsimps [hypreal_zero_def]) 1);
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset() addSEs [FreeUltrafilterNat_subset, realpow_ge_zero],
- simpset() addsimps [hyperpow,hypreal_le]));
-qed "hyperpow_ge_zero";
-
-Goal "(0::hypreal) < x & x <= y --> x pow n <= y pow n";
-by (full_simp_tac (simpset() addsimps [hypreal_zero_def]) 1);
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),
- simpset() addsimps [hyperpow,hypreal_le,hypreal_less]));
-by (etac (FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset) 1
- THEN assume_tac 1);
-by (auto_tac (claset() addIs [realpow_le], simpset()));
-qed_spec_mp "hyperpow_le";
-
-Goal "1 pow n = (1::hypreal)";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(), simpset() addsimps [hypreal_one_def, hyperpow]));
-qed "hyperpow_eq_one";
-Addsimps [hyperpow_eq_one];
-
-Goal "abs(-(1 pow n)) = (1::hypreal)";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),
- simpset() addsimps [hyperpow, hypreal_hrabs, hypreal_one_def]));
-qed "hrabs_minus_hyperpow_one";
-Addsimps [hrabs_minus_hyperpow_one];
-
-Goal "abs(-1 pow n) = (1::hypreal)";
-by (subgoal_tac "abs((- (1::hypreal)) pow n) = (1::hypreal)" 1);
-by (Asm_full_simp_tac 1);
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),
- simpset() addsimps [hypreal_one_def, hyperpow,hypreal_minus,
- hypreal_hrabs]));
-qed "hrabs_hyperpow_minus_one";
-Addsimps [hrabs_hyperpow_minus_one];
-
-Goal "(r * s) pow n = (r pow n) * (s pow n)";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","s")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),
- simpset() addsimps [hyperpow, hypreal_mult,realpow_mult]));
-qed "hyperpow_mult";
-
-Goal "(0::hypreal) <= r pow ((1::hypnat) + (1::hypnat))";
-by (auto_tac (claset(),
- simpset() addsimps [hyperpow_two, zero_le_mult_iff]));
-qed "hyperpow_two_le";
-Addsimps [hyperpow_two_le];
-
-Goal "abs(x pow ((1::hypnat) + (1::hypnat))) = x pow ((1::hypnat) + (1::hypnat))";
-by (simp_tac (simpset() addsimps [hrabs_eqI1]) 1);
-qed "hrabs_hyperpow_two";
-Addsimps [hrabs_hyperpow_two];
-
-Goal "abs(x) pow ((1::hypnat) + (1::hypnat)) = x pow ((1::hypnat) + (1::hypnat))";
-by (simp_tac (simpset() addsimps [hyperpow_hrabs,hrabs_eqI1]) 1);
-qed "hyperpow_two_hrabs";
-Addsimps [hyperpow_two_hrabs];
-
-(*? very similar to hrealpow_two_gt_one *)
-Goal "(1::hypreal) < r ==> 1 < r pow ((1::hypnat) + (1::hypnat))";
-by (auto_tac (claset(), simpset() addsimps [hyperpow_two]));
-by (res_inst_tac [("y","1*1")] order_le_less_trans 1);
-by (rtac hypreal_mult_less_mono 2);
-by Auto_tac;
-qed "hyperpow_two_gt_one";
-
-Goal "(1::hypreal) <= r ==> 1 <= r pow ((1::hypnat) + (1::hypnat))";
-by (auto_tac (claset() addSDs [order_le_imp_less_or_eq]
- addIs [hyperpow_two_gt_one,order_less_imp_le],
- simpset()));
-qed "hyperpow_two_ge_one";
-
-Goal "(1::hypreal) <= 2 pow n";
-by (res_inst_tac [("y","1 pow n")] order_trans 1);
-by (rtac hyperpow_le 2);
-by Auto_tac;
-qed "two_hyperpow_ge_one";
-Addsimps [two_hyperpow_ge_one];
-
-Addsimps [simplify (simpset()) realpow_minus_one];
-
-Goal "-1 pow (((1::hypnat) + (1::hypnat))*n) = (1::hypreal)";
-by (subgoal_tac "(-((1::hypreal))) pow (((1::hypnat) + (1::hypnat))*n) = (1::hypreal)" 1);
-by (Asm_full_simp_tac 1);
-by (simp_tac (HOL_ss addsimps [hypreal_one_def]) 1);
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),
- simpset() addsimps [double_lemma, hyperpow, hypnat_add,
- hypreal_minus]));
-qed "hyperpow_minus_one2";
-Addsimps [hyperpow_minus_one2];
-
-Goalw [hypnat_one_def]
- "(0::hypreal) < r & r < 1 --> r pow (n + (1::hypnat)) < r pow n";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset() addSDs [conjI RS realpow_Suc_less]
- addEs [FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset],
- simpset() addsimps [hypreal_zero_def, hypreal_one_def,
- hyperpow, hypreal_less, hypnat_add]));
-qed_spec_mp "hyperpow_Suc_less";
-
-Goalw [hypnat_one_def]
- "0 <= r & r < (1::hypreal) --> r pow (n + (1::hypnat)) <= r pow n";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset() addSDs [conjI RS realpow_Suc_le]
- addEs [FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset],
- simpset() addsimps [hypreal_zero_def, hypreal_one_def, hyperpow,
- hypreal_le,hypnat_add, hypreal_less]));
-qed_spec_mp "hyperpow_Suc_le";
-
-Goalw [hypnat_one_def]
- "(0::hypreal) <= r & r < 1 & n < N --> r pow N <= r pow n";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","r")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),
- simpset() addsimps [hyperpow, hypreal_le,hypreal_less,
- hypnat_less, hypreal_zero_def, hypreal_one_def]));
-by (etac (FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset) 1);
-by (etac FreeUltrafilterNat_Int 1);
-by (auto_tac (claset() addSDs [conjI RS realpow_less_le], simpset()));
-qed_spec_mp "hyperpow_less_le";
-
-Goal "[| (0::hypreal) <= r; r < 1 |] \
-\ ==> ALL N n. n < N --> r pow N <= r pow n";
-by (blast_tac (claset() addSIs [hyperpow_less_le]) 1);
-qed "hyperpow_less_le2";
-
-Goal "[| 0 <= r; r < (1::hypreal); N : HNatInfinite |] \
-\ ==> ALL n: Nats. r pow N <= r pow n";
-by (auto_tac (claset() addSIs [hyperpow_less_le],
- simpset() addsimps [HNatInfinite_iff]));
-qed "hyperpow_SHNat_le";
-
-Goalw [hypreal_of_real_def,hypnat_of_nat_def]
- "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)";
-by (auto_tac (claset(), simpset() addsimps [hyperpow]));
-qed "hyperpow_realpow";
-
-Goalw [SReal_def] "(hypreal_of_real r) pow (hypnat_of_nat n) : Reals";
-by (simp_tac (simpset() delsimps [hypreal_of_real_power]
- addsimps [hyperpow_realpow]) 1);
-qed "hyperpow_SReal";
-Addsimps [hyperpow_SReal];
-
-Goal "N : HNatInfinite ==> (0::hypreal) pow N = 0";
-by (dtac HNatInfinite_is_Suc 1);
-by Auto_tac;
-qed "hyperpow_zero_HNatInfinite";
-Addsimps [hyperpow_zero_HNatInfinite];
-
-Goal "[| (0::hypreal) <= r; r < 1; n <= N |] ==> r pow N <= r pow n";
-by (dres_inst_tac [("y","N")] hypnat_le_imp_less_or_eq 1);
-by (auto_tac (claset() addIs [hyperpow_less_le], simpset()));
-qed "hyperpow_le_le";
-
-Goal "[| (0::hypreal) < r; r < 1 |] ==> r pow (n + (1::hypnat)) <= r";
-by (dres_inst_tac [("n","(1::hypnat)")] (order_less_imp_le RS hyperpow_le_le) 1);
-by Auto_tac;
-qed "hyperpow_Suc_le_self";
-
-Goal "[| (0::hypreal) <= r; r < 1 |] ==> r pow (n + (1::hypnat)) <= r";
-by (dres_inst_tac [("n","(1::hypnat)")] hyperpow_le_le 1);
-by Auto_tac;
-qed "hyperpow_Suc_le_self2";
-
-Goalw [Infinitesimal_def]
- "[| x : Infinitesimal; 0 < N |] ==> abs (x pow N) <= abs x";
-by (auto_tac (claset() addSIs [hyperpow_Suc_le_self2],
- simpset() addsimps [hyperpow_hrabs RS sym,
- hypnat_gt_zero_iff2, abs_ge_zero]));
-qed "lemma_Infinitesimal_hyperpow";
-
-Goal "[| x : Infinitesimal; 0 < N |] ==> x pow N : Infinitesimal";
-by (rtac hrabs_le_Infinitesimal 1);
-by (rtac lemma_Infinitesimal_hyperpow 2);
-by Auto_tac;
-qed "Infinitesimal_hyperpow";
-
-Goalw [hypnat_of_nat_def]
- "(x ^ n : Infinitesimal) = (x pow (hypnat_of_nat n) : Infinitesimal)";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (auto_tac (claset(), simpset() addsimps [hrealpow, hyperpow]));
-qed "hrealpow_hyperpow_Infinitesimal_iff";
-
-Goal "[| x : Infinitesimal; 0 < n |] ==> x ^ n : Infinitesimal";
-by (auto_tac (claset() addSIs [Infinitesimal_hyperpow],
- simpset() addsimps [hrealpow_hyperpow_Infinitesimal_iff,
- hypnat_of_nat_less_iff,hypnat_of_nat_zero]
- delsimps [hypnat_of_nat_less_iff RS sym]));
-qed "Infinitesimal_hrealpow";
-
-(* MOVE UP *)
-Goal "(0::hypreal) <= x * x";
-by (auto_tac (claset(),simpset() addsimps
- [zero_le_mult_iff]));
-qed "hypreal_mult_self_ge_zero";
-Addsimps [hypreal_mult_self_ge_zero];
-
-Goal "[|(0::hypreal) <= x; 0 <= y; x ^ Suc n = y ^ Suc n |] ==> x = y";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps
- [hrealpow,hypreal_mult,hypreal_le,hypreal_zero_num]));
-by (ultra_tac (claset() addIs [realpow_Suc_cancel_eq],
- simpset()) 1);
-qed "hrealpow_Suc_cancel_eq";
-
--- a/src/HOL/Hyperreal/HyperPow.thy Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/Hyperreal/HyperPow.thy Fri Jan 09 10:46:18 2004 +0100
@@ -4,33 +4,459 @@
Description : Powers theory for hyperreals
*)
-HyperPow = HRealAbs + HyperNat + RealPow +
+header{*Exponentials on the Hyperreals*}
+
+theory HyperPow = HRealAbs + HyperNat + RealPow:
-(** First: hypnat is linearly ordered **)
+instance hypnat :: order
+ by (intro_classes,
+ (assumption |
+ rule hypnat_le_refl hypnat_le_trans hypnat_le_anti_sym hypnat_less_le)+)
-instance hypnat :: order (hypnat_le_refl,hypnat_le_trans,hypnat_le_anti_sym,
- hypnat_less_le)
-instance hypnat :: linorder (hypnat_le_linear)
+
+text{*Type @{typ hypnat} is linearly ordered*}
+instance hypnat :: linorder
+ by (intro_classes, rule hypnat_le_linear)
-instance hypnat :: plus_ac0(hypnat_add_commute,hypnat_add_assoc,
- hypnat_add_zero_left)
+instance hypnat :: plus_ac0
+ by (intro_classes,
+ (assumption |
+ rule hypnat_add_commute hypnat_add_assoc hypnat_add_zero_left)+)
-instance hypreal :: {power}
+instance hypreal :: power ..
consts hpowr :: "[hypreal,nat] => hypreal"
primrec
- hpowr_0 "r ^ 0 = (1::hypreal)"
- hpowr_Suc "r ^ (Suc n) = (r::hypreal) * (r ^ n)"
+ hpowr_0: "r ^ 0 = (1::hypreal)"
+ hpowr_Suc: "r ^ (Suc n) = (r::hypreal) * (r ^ n)"
+
+
+instance hypreal :: ringpower
+proof
+ fix z :: hypreal
+ fix n :: nat
+ show "z^0 = 1" by simp
+ show "z^(Suc n) = z * (z^n)" by simp
+qed
+
consts
- "pow" :: [hypreal,hypnat] => hypreal (infixr 80)
+ "pow" :: "[hypreal,hypnat] => hypreal" (infixr 80)
defs
(* hypernatural powers of hyperreals *)
- hyperpow_def
- "(R::hypreal) pow (N::hypnat)
- == Abs_hypreal(UN X:Rep_hypreal(R). UN Y: Rep_hypnat(N).
- hyprel``{%n::nat. (X n) ^ (Y n)})"
+ hyperpow_def:
+ "(R::hypreal) pow (N::hypnat) ==
+ Abs_hypreal(\<Union>X \<in> Rep_hypreal(R). \<Union>Y \<in> Rep_hypnat(N).
+ hyprel``{%n::nat. (X n) ^ (Y n)})"
+
+lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r"
+apply (simp (no_asm))
+done
+
+lemma hrabs_hrealpow_minus_one [simp]: "abs(-1 ^ n) = (1::hypreal)"
+apply (simp add: power_abs);
+done
+
+lemma hrealpow_two_le: "(0::hypreal) \<le> r ^ Suc (Suc 0)"
+apply (auto simp add: zero_le_mult_iff)
+done
+declare hrealpow_two_le [simp]
+
+lemma hrealpow_two_le_add_order:
+ "(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0)"
+apply (simp only: hrealpow_two_le hypreal_le_add_order)
+done
+declare hrealpow_two_le_add_order [simp]
+
+lemma hrealpow_two_le_add_order2:
+ "(0::hypreal) \<le> u ^ Suc (Suc 0) + v ^ Suc (Suc 0) + w ^ Suc (Suc 0)"
+apply (simp only: hrealpow_two_le hypreal_le_add_order)
+done
+declare hrealpow_two_le_add_order2 [simp]
+
+lemma hypreal_add_nonneg_eq_0_iff:
+ "[| 0 \<le> x; 0 \<le> y |] ==> (x+y = 0) = (x = 0 & y = (0::hypreal))"
+apply arith
+done
+
+text{*FIXME: DELETE THESE*}
+lemma hypreal_three_squares_add_zero_iff:
+ "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))"
+apply (simp only: zero_le_square hypreal_le_add_order hypreal_add_nonneg_eq_0_iff)
+apply auto
+done
+
+lemma hrealpow_three_squares_add_zero_iff [simp]:
+ "(x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + z ^ Suc (Suc 0) = (0::hypreal)) =
+ (x = 0 & y = 0 & z = 0)"
+by (simp only: hypreal_three_squares_add_zero_iff hrealpow_two)
+
+
+lemma hrabs_hrealpow_two [simp]:
+ "abs(x ^ Suc (Suc 0)) = (x::hypreal) ^ Suc (Suc 0)"
+by (simp add: abs_mult)
+
+lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \<le> 2 ^ n"
+by (insert power_increasing [of 0 n "2::hypreal"], simp)
+
+lemma two_hrealpow_gt: "hypreal_of_nat n < 2 ^ n"
+apply (induct_tac "n")
+apply (auto simp add: hypreal_of_nat_Suc left_distrib)
+apply (cut_tac n = "n" in two_hrealpow_ge_one)
+apply arith
+done
+declare two_hrealpow_gt [simp]
+
+lemma hrealpow_minus_one: "-1 ^ (2*n) = (1::hypreal)"
+apply (induct_tac "n")
+apply auto
+done
+
+lemma double_lemma: "n+n = (2*n::nat)"
+apply auto
+done
+
+(*ugh: need to get rid fo the n+n*)
+lemma hrealpow_minus_one2: "-1 ^ (n + n) = (1::hypreal)"
+apply (auto simp add: double_lemma hrealpow_minus_one)
+done
+declare hrealpow_minus_one2 [simp]
+
+lemma hrealpow:
+ "Abs_hypreal(hyprel``{%n. X n}) ^ m = Abs_hypreal(hyprel``{%n. (X n) ^ m})"
+apply (induct_tac "m")
+apply (auto simp add: hypreal_one_def hypreal_mult)
+done
+
+lemma hrealpow_sum_square_expand:
+ "(x + (y::hypreal)) ^ Suc (Suc 0) =
+ x ^ Suc (Suc 0) + y ^ Suc (Suc 0) + (hypreal_of_nat (Suc (Suc 0)))*x*y"
+by (simp add: right_distrib left_distrib hypreal_of_nat_Suc)
+
+
+subsection{*Literal Arithmetic Involving Powers and Type @{typ hypreal}*}
+
+lemma hypreal_of_real_power: "hypreal_of_real (x ^ n) = hypreal_of_real x ^ n"
+apply (induct_tac "n")
+apply (simp_all add: nat_mult_distrib)
+done
+declare hypreal_of_real_power [simp]
+
+lemma power_hypreal_of_real_number_of:
+ "(number_of v :: hypreal) ^ n = hypreal_of_real ((number_of v) ^ n)"
+by (simp only: hypreal_number_of_def hypreal_of_real_power)
+
+declare power_hypreal_of_real_number_of [of _ "number_of w", standard, simp]
+
+lemma hrealpow_HFinite: "x \<in> HFinite ==> x ^ n \<in> HFinite"
+apply (induct_tac "n")
+apply (auto intro: HFinite_mult)
+done
+
+
+subsection{*Powers with Hypernatural Exponents*}
+
+lemma hyperpow_congruent:
+ "congruent hyprel
+ (%X Y. hyprel``{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})"
+apply (unfold congruent_def)
+apply (auto intro!: ext)
+apply fuf+
+done
+
+lemma hyperpow:
+ "Abs_hypreal(hyprel``{%n. X n}) pow Abs_hypnat(hypnatrel``{%n. Y n}) =
+ Abs_hypreal(hyprel``{%n. X n ^ Y n})"
+apply (unfold hyperpow_def)
+apply (rule_tac f = "Abs_hypreal" in arg_cong)
+apply (auto intro!: lemma_hyprel_refl bexI
+ simp add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] equiv_hyprel
+ hyperpow_congruent)
+apply fuf
+done
+
+lemma hyperpow_zero: "(0::hypreal) pow (n + (1::hypnat)) = 0"
+apply (unfold hypnat_one_def)
+apply (simp (no_asm) add: hypreal_zero_def)
+apply (rule_tac z = "n" in eq_Abs_hypnat)
+apply (auto simp add: hyperpow hypnat_add)
+done
+declare hyperpow_zero [simp]
+
+lemma hyperpow_not_zero [rule_format (no_asm)]:
+ "r \<noteq> (0::hypreal) --> r pow n \<noteq> 0"
+apply (simp (no_asm) add: hypreal_zero_def)
+apply (rule_tac z = "n" in eq_Abs_hypnat)
+apply (rule_tac z = "r" in eq_Abs_hypreal)
+apply (auto simp add: hyperpow)
+apply (drule FreeUltrafilterNat_Compl_mem)
+apply ultra
+done
+
+lemma hyperpow_inverse:
+ "r \<noteq> (0::hypreal) --> inverse(r pow n) = (inverse r) pow n"
+apply (simp (no_asm) add: hypreal_zero_def)
+apply (rule_tac z = "n" in eq_Abs_hypnat)
+apply (rule_tac z = "r" in eq_Abs_hypreal)
+apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: hypreal_inverse hyperpow)
+apply (rule FreeUltrafilterNat_subset)
+apply (auto dest: realpow_not_zero intro: power_inverse)
+done
+
+lemma hyperpow_hrabs: "abs r pow n = abs (r pow n)"
+apply (rule_tac z = "n" in eq_Abs_hypnat)
+apply (rule_tac z = "r" in eq_Abs_hypreal)
+apply (auto simp add: hypreal_hrabs hyperpow power_abs [symmetric])
+done
+
+lemma hyperpow_add: "r pow (n + m) = (r pow n) * (r pow m)"
+apply (rule_tac z = "n" in eq_Abs_hypnat)
+apply (rule_tac z = "m" in eq_Abs_hypnat)
+apply (rule_tac z = "r" in eq_Abs_hypreal)
+apply (auto simp add: hyperpow hypnat_add hypreal_mult power_add)
+done
+
+lemma hyperpow_one: "r pow (1::hypnat) = r"
+apply (unfold hypnat_one_def)
+apply (rule_tac z = "r" in eq_Abs_hypreal)
+apply (auto simp add: hyperpow)
+done
+declare hyperpow_one [simp]
+
+lemma hyperpow_two:
+ "r pow ((1::hypnat) + (1::hypnat)) = r * r"
+apply (unfold hypnat_one_def)
+apply (rule_tac z = "r" in eq_Abs_hypreal)
+apply (auto simp add: hyperpow hypnat_add hypreal_mult)
+done
+
+lemma hyperpow_gt_zero: "(0::hypreal) < r ==> 0 < r pow n"
+apply (simp add: hypreal_zero_def)
+apply (rule_tac z = "n" in eq_Abs_hypnat)
+apply (rule_tac z = "r" in eq_Abs_hypreal)
+apply (auto elim!: FreeUltrafilterNat_subset zero_less_power
+ simp add: hyperpow hypreal_less hypreal_le)
+done
+
+lemma hyperpow_ge_zero: "(0::hypreal) \<le> r ==> 0 \<le> r pow n"
+apply (simp add: hypreal_zero_def)
+apply (rule_tac z = "n" in eq_Abs_hypnat)
+apply (rule_tac z = "r" in eq_Abs_hypreal)
+apply (auto elim!: FreeUltrafilterNat_subset zero_le_power
+ simp add: hyperpow hypreal_le)
+done
+
+lemma hyperpow_le: "[|(0::hypreal) < x; x \<le> y|] ==> x pow n \<le> y pow n"
+apply (simp add: hypreal_zero_def)
+apply (rule_tac z = "n" in eq_Abs_hypnat)
+apply (rule_tac z = "x" in eq_Abs_hypreal)
+apply (rule_tac z = "y" in eq_Abs_hypreal)
+apply (auto simp add: hyperpow hypreal_le hypreal_less)
+apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset] , assumption)
+apply (auto intro: power_mono)
+done
+
+lemma hyperpow_eq_one: "1 pow n = (1::hypreal)"
+apply (rule_tac z = "n" in eq_Abs_hypnat)
+apply (auto simp add: hypreal_one_def hyperpow)
+done
+declare hyperpow_eq_one [simp]
+
+lemma hrabs_hyperpow_minus_one: "abs(-1 pow n) = (1::hypreal)"
+apply (subgoal_tac "abs ((- (1::hypreal)) pow n) = (1::hypreal) ")
+apply simp
+apply (rule_tac z = "n" in eq_Abs_hypnat)
+apply (auto simp add: hypreal_one_def hyperpow hypreal_minus hypreal_hrabs)
+done
+declare hrabs_hyperpow_minus_one [simp]
+
+lemma hyperpow_mult: "(r * s) pow n = (r pow n) * (s pow n)"
+apply (rule_tac z = "n" in eq_Abs_hypnat)
+apply (rule_tac z = "r" in eq_Abs_hypreal)
+apply (rule_tac z = "s" in eq_Abs_hypreal)
+apply (auto simp add: hyperpow hypreal_mult power_mult_distrib)
+done
+
+lemma hyperpow_two_le: "(0::hypreal) \<le> r pow ((1::hypnat) + (1::hypnat))"
+apply (auto simp add: hyperpow_two zero_le_mult_iff)
+done
+declare hyperpow_two_le [simp]
+
+lemma hrabs_hyperpow_two:
+ "abs(x pow (1 + 1)) = x pow (1 + 1)"
+apply (simp (no_asm) add: hrabs_eqI1)
+done
+declare hrabs_hyperpow_two [simp]
+
+lemma hyperpow_two_hrabs:
+ "abs(x) pow (1 + 1) = x pow (1 + 1)"
+apply (simp add: hyperpow_hrabs)
+done
+declare hyperpow_two_hrabs [simp]
+
+lemma hyperpow_two_gt_one:
+ "(1::hypreal) < r ==> 1 < r pow (1 + 1)"
+apply (auto simp add: hyperpow_two)
+apply (rule_tac y = "1*1" in order_le_less_trans)
+apply (rule_tac [2] hypreal_mult_less_mono)
+apply auto
+done
+
+lemma hyperpow_two_ge_one:
+ "(1::hypreal) \<le> r ==> 1 \<le> r pow (1 + 1)"
+apply (auto dest!: order_le_imp_less_or_eq intro: hyperpow_two_gt_one order_less_imp_le)
+done
+
+lemma two_hyperpow_ge_one: "(1::hypreal) \<le> 2 pow n"
+apply (rule_tac y = "1 pow n" in order_trans)
+apply (rule_tac [2] hyperpow_le)
+apply auto
+done
+declare two_hyperpow_ge_one [simp]
+
+lemma hyperpow_minus_one2:
+ "-1 pow ((1 + 1)*n) = (1::hypreal)"
+apply (subgoal_tac " (- ((1::hypreal))) pow ((1 + 1)*n) = (1::hypreal) ")
+apply simp
+apply (simp only: hypreal_one_def)
+apply (rule_tac z = "n" in eq_Abs_hypnat)
+apply (auto simp add: double_lemma hyperpow hypnat_add hypreal_minus)
+done
+declare hyperpow_minus_one2 [simp]
+
+lemma hyperpow_less_le:
+ "[|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
+apply (rule_tac z = "n" in eq_Abs_hypnat)
+apply (rule_tac z = "N" in eq_Abs_hypnat)
+apply (rule_tac z = "r" in eq_Abs_hypreal)
+apply (auto simp add: hyperpow hypreal_le hypreal_less hypnat_less
+ hypreal_zero_def hypreal_one_def)
+apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
+apply (erule FreeUltrafilterNat_Int)
+apply assumption;
+apply (auto intro: power_decreasing)
+done
+
+lemma hyperpow_SHNat_le:
+ "[| 0 \<le> r; r \<le> (1::hypreal); N \<in> HNatInfinite |]
+ ==> ALL n: Nats. r pow N \<le> r pow n"
+by (auto intro!: hyperpow_less_le simp add: HNatInfinite_iff)
+
+lemma hyperpow_realpow:
+ "(hypreal_of_real r) pow (hypnat_of_nat n) = hypreal_of_real (r ^ n)"
+apply (unfold hypreal_of_real_def hypnat_of_nat_def)
+apply (auto simp add: hyperpow)
+done
+
+lemma hyperpow_SReal: "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals"
+apply (unfold SReal_def)
+apply (simp (no_asm) del: hypreal_of_real_power add: hyperpow_realpow)
+done
+declare hyperpow_SReal [simp]
+
+lemma hyperpow_zero_HNatInfinite: "N \<in> HNatInfinite ==> (0::hypreal) pow N = 0"
+apply (drule HNatInfinite_is_Suc)
+apply auto
+done
+declare hyperpow_zero_HNatInfinite [simp]
+
+lemma hyperpow_le_le:
+ "[| (0::hypreal) \<le> r; r \<le> 1; n \<le> N |] ==> r pow N \<le> r pow n"
+apply (drule_tac y = "N" in hypnat_le_imp_less_or_eq)
+apply (auto intro: hyperpow_less_le)
+done
+
+lemma hyperpow_Suc_le_self2:
+ "[| (0::hypreal) \<le> r; r < 1 |] ==> r pow (n + (1::hypnat)) \<le> r"
+apply (drule_tac n = " (1::hypnat) " in hyperpow_le_le)
+apply auto
+done
+
+lemma lemma_Infinitesimal_hyperpow:
+ "[| x \<in> Infinitesimal; 0 < N |] ==> abs (x pow N) \<le> abs x"
+apply (unfold Infinitesimal_def)
+apply (auto intro!: hyperpow_Suc_le_self2
+ simp add: hyperpow_hrabs [symmetric] hypnat_gt_zero_iff2 abs_ge_zero)
+done
+
+lemma Infinitesimal_hyperpow:
+ "[| x \<in> Infinitesimal; 0 < N |] ==> x pow N \<in> Infinitesimal"
+apply (rule hrabs_le_Infinitesimal)
+apply (rule_tac [2] lemma_Infinitesimal_hyperpow)
+apply auto
+done
+
+lemma hrealpow_hyperpow_Infinitesimal_iff:
+ "(x ^ n \<in> Infinitesimal) = (x pow (hypnat_of_nat n) \<in> Infinitesimal)"
+apply (unfold hypnat_of_nat_def)
+apply (rule_tac z = "x" in eq_Abs_hypreal)
+apply (auto simp add: hrealpow hyperpow)
+done
+
+lemma Infinitesimal_hrealpow:
+ "[| x \<in> Infinitesimal; 0 < n |] ==> x ^ n \<in> Infinitesimal"
+by (force intro!: Infinitesimal_hyperpow
+ simp add: hrealpow_hyperpow_Infinitesimal_iff
+ hypnat_of_nat_less_iff hypnat_of_nat_zero
+ simp del: hypnat_of_nat_less_iff [symmetric])
+
+ML
+{*
+val hrealpow_two = thm "hrealpow_two";
+val hrabs_hrealpow_minus_one = thm "hrabs_hrealpow_minus_one";
+val hrealpow_two_le = thm "hrealpow_two_le";
+val hrealpow_two_le_add_order = thm "hrealpow_two_le_add_order";
+val hrealpow_two_le_add_order2 = thm "hrealpow_two_le_add_order2";
+val hypreal_add_nonneg_eq_0_iff = thm "hypreal_add_nonneg_eq_0_iff";
+val hypreal_three_squares_add_zero_iff = thm "hypreal_three_squares_add_zero_iff";
+val hrealpow_three_squares_add_zero_iff = thm "hrealpow_three_squares_add_zero_iff";
+val hrabs_hrealpow_two = thm "hrabs_hrealpow_two";
+val two_hrealpow_ge_one = thm "two_hrealpow_ge_one";
+val two_hrealpow_gt = thm "two_hrealpow_gt";
+val hrealpow_minus_one = thm "hrealpow_minus_one";
+val double_lemma = thm "double_lemma";
+val hrealpow_minus_one2 = thm "hrealpow_minus_one2";
+val hrealpow = thm "hrealpow";
+val hrealpow_sum_square_expand = thm "hrealpow_sum_square_expand";
+val hypreal_of_real_power = thm "hypreal_of_real_power";
+val power_hypreal_of_real_number_of = thm "power_hypreal_of_real_number_of";
+val hrealpow_HFinite = thm "hrealpow_HFinite";
+val hyperpow_congruent = thm "hyperpow_congruent";
+val hyperpow = thm "hyperpow";
+val hyperpow_zero = thm "hyperpow_zero";
+val hyperpow_not_zero = thm "hyperpow_not_zero";
+val hyperpow_inverse = thm "hyperpow_inverse";
+val hyperpow_hrabs = thm "hyperpow_hrabs";
+val hyperpow_add = thm "hyperpow_add";
+val hyperpow_one = thm "hyperpow_one";
+val hyperpow_two = thm "hyperpow_two";
+val hyperpow_gt_zero = thm "hyperpow_gt_zero";
+val hyperpow_ge_zero = thm "hyperpow_ge_zero";
+val hyperpow_le = thm "hyperpow_le";
+val hyperpow_eq_one = thm "hyperpow_eq_one";
+val hrabs_hyperpow_minus_one = thm "hrabs_hyperpow_minus_one";
+val hyperpow_mult = thm "hyperpow_mult";
+val hyperpow_two_le = thm "hyperpow_two_le";
+val hrabs_hyperpow_two = thm "hrabs_hyperpow_two";
+val hyperpow_two_hrabs = thm "hyperpow_two_hrabs";
+val hyperpow_two_gt_one = thm "hyperpow_two_gt_one";
+val hyperpow_two_ge_one = thm "hyperpow_two_ge_one";
+val two_hyperpow_ge_one = thm "two_hyperpow_ge_one";
+val hyperpow_minus_one2 = thm "hyperpow_minus_one2";
+val hyperpow_less_le = thm "hyperpow_less_le";
+val hyperpow_SHNat_le = thm "hyperpow_SHNat_le";
+val hyperpow_realpow = thm "hyperpow_realpow";
+val hyperpow_SReal = thm "hyperpow_SReal";
+val hyperpow_zero_HNatInfinite = thm "hyperpow_zero_HNatInfinite";
+val hyperpow_le_le = thm "hyperpow_le_le";
+val hyperpow_Suc_le_self2 = thm "hyperpow_Suc_le_self2";
+val lemma_Infinitesimal_hyperpow = thm "lemma_Infinitesimal_hyperpow";
+val Infinitesimal_hyperpow = thm "Infinitesimal_hyperpow";
+val hrealpow_hyperpow_Infinitesimal_iff = thm "hrealpow_hyperpow_Infinitesimal_iff";
+val Infinitesimal_hrealpow = thm "Infinitesimal_hrealpow";
+*}
+
end
--- a/src/HOL/Hyperreal/Lim.ML Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/Hyperreal/Lim.ML Fri Jan 09 10:46:18 2004 +0100
@@ -1348,7 +1348,7 @@
Goal "[| DERIV f x :> d; f(x) \\<noteq> 0 |] \
\ ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))";
by (rtac (real_mult_commute RS subst) 1);
-by (asm_simp_tac (HOL_ss addsimps [minus_mult_left, realpow_inverse]) 1);
+by (asm_simp_tac (HOL_ss addsimps [minus_mult_left, power_inverse]) 1);
by (fold_goals_tac [o_def]);
by (blast_tac (claset() addSIs [DERIV_chain,DERIV_inverse]) 1);
qed "DERIV_inverse_fun";
@@ -1369,7 +1369,7 @@
by (REPEAT(assume_tac 1));
by (asm_full_simp_tac
(simpset() addsimps [real_divide_def, right_distrib,
- realpow_inverse,minus_mult_left] @ mult_ac
+ power_inverse,minus_mult_left] @ mult_ac
delsimps [realpow_Suc, minus_mult_right RS sym, minus_mult_left RS sym]) 1);
qed "DERIV_quotient";
--- a/src/HOL/Hyperreal/MacLaurin.ML Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/Hyperreal/MacLaurin.ML Fri Jan 09 10:46:18 2004 +0100
@@ -65,8 +65,8 @@
delsimps [realpow_Suc]) 2);
by (stac real_mult_inv_left 2);
by (stac real_mult_inv_left 3);
-by (dtac (realpow_gt_zero RS real_not_refl2 RS not_sym) 2);
-by (assume_tac 2);
+by (rtac (real_not_refl2 RS not_sym) 2);
+by (etac zero_less_power 2);
by (rtac real_of_nat_fact_not_zero 2);
by (Simp_tac 2);
by (etac exE 1);
@@ -281,7 +281,7 @@
by (Asm_full_simp_tac 1);
by (auto_tac (claset(),simpset() addsimps [real_divide_def,
CLAIM "((a * b) * c) * d = (b * c) * (a * (d::real))",
- realpow_mult RS sym]));
+ power_mult_distrib RS sym]));
qed "Maclaurin_minus";
Goal "(h < 0 & 0 < n & diff 0 = f & \
@@ -490,7 +490,7 @@
by (dtac lemma_odd_mod_4_div_2 1);
by (asm_full_simp_tac (simpset() addsimps [numeral_2_eq_2, real_divide_def]) 1);
by (auto_tac (claset() addSIs [real_mult_le_lemma,mult_right_mono],
- simpset() addsimps [real_divide_def,abs_mult,abs_inverse,realpow_abs RS
+ simpset() addsimps [real_divide_def,abs_mult,abs_inverse,power_abs RS
sym]));
qed "Maclaurin_sin_bound";
@@ -520,7 +520,7 @@
by (cut_inst_tac [("f","sin"),("n","n"),("x","x"),
("diff","%n x. sin(x + 1/2*real (n)*pi)")]
Maclaurin_all_lt_objl 1);
-by (Step_tac 1);
+by (Safe_tac);
by (Simp_tac 1);
by (Simp_tac 1);
by (case_tac "n" 1);
--- a/src/HOL/Hyperreal/NthRoot.thy Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/Hyperreal/NthRoot.thy Fri Jan 09 10:46:18 2004 +0100
@@ -20,9 +20,14 @@
apply (rule_tac x = "1" in exI)
apply (drule_tac [2] linorder_not_le [THEN iffD1])
apply (drule_tac [2] less_not_refl2 [THEN not0_implies_Suc])
-apply (auto intro!: realpow_Suc_le_self simp add: zero_less_one)
+apply (simp add: );
+apply (force intro!: realpow_Suc_le_self simp del: realpow_Suc)
done
+text{*Used only just below*}
+lemma realpow_ge_self2: "[| (1::real) \<le> r; 0 < n |] ==> r \<le> r ^ n"
+by (insert power_increasing [of 1 n r], simp)
+
lemma lemma_nth_realpow_isUb_ex:
"[| (0::real) < a; 0 < n |]
==> \<exists>u. isUb (UNIV::real set) {x. x ^ n <= a & 0 < x} u"
@@ -129,10 +134,10 @@
apply (rule_tac n = "k" in real_mult_less_self)
apply (blast intro: lemma_nth_realpow_isLub_gt_zero)
apply (safe)
-apply (drule_tac n = "k" in lemma_nth_realpow_isLub_gt_zero [THEN real_mult_add_one_minus_ge_zero])
-apply (drule_tac [3] conjI [THEN realpow_le2])
-apply (rule_tac [3] order_less_imp_le)
-apply (auto intro: order_trans)
+apply (drule_tac n = "k" in
+ lemma_nth_realpow_isLub_gt_zero [THEN real_mult_add_one_minus_ge_zero])
+apply assumption+
+apply (blast intro: order_trans order_less_imp_le power_mono)
done
text{*Second result we want*}
@@ -141,11 +146,12 @@
isLub (UNIV::real set)
{x. x ^ n <= a & 0 < x} u |] ==> u ^ n <= a"
apply (frule lemma_nth_realpow_isLub_le , safe)
-apply (rule LIMSEQ_inverse_real_of_nat_add_minus_mult [THEN LIMSEQ_pow, THEN LIMSEQ_le_const2])
+apply (rule LIMSEQ_inverse_real_of_nat_add_minus_mult
+ [THEN LIMSEQ_pow, THEN LIMSEQ_le_const2])
apply (auto simp add: real_of_nat_def)
done
-(*----------- The theorem at last! -----------*)
+text{*The theorem at last!*}
lemma realpow_nth: "[| (0::real) < a; 0 < n |] ==> \<exists>r. r ^ n = a"
apply (frule nth_realpow_isLub_ex , auto)
apply (auto intro: realpow_nth_le realpow_nth_ge real_le_anti_sym)
--- a/src/HOL/Hyperreal/Poly.ML Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/Hyperreal/Poly.ML Fri Jan 09 10:46:18 2004 +0100
@@ -1002,7 +1002,7 @@
by (dtac (poly_mult_left_cancel RS iffD1) 1);
by (Asm_full_simp_tac 1);
by (asm_full_simp_tac (simpset() addsimps [fun_eq,poly_mult,poly_add,poly_cmult,
- poly_minus] delsimps [pmult_Cons, thm"mult_cancel_left"]) 1);
+ poly_minus] delsimps [pmult_Cons, mult_cancel_left, field_mult_cancel_left]) 1);
by (Step_tac 1);
by (res_inst_tac [("c1","real (Suc n)")] (real_mult_left_cancel
RS iffD1) 1);
--- a/src/HOL/Hyperreal/SEQ.ML Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/Hyperreal/SEQ.ML Fri Jan 09 10:46:18 2004 +0100
@@ -1216,22 +1216,25 @@
qed "LIMSEQ_pow";
(*----------------------------------------------------------------
- 0 <= x < 1 ==> (x ^ n ----> 0)
+ 0 <= x <= 1 ==> (x ^ n ----> 0)
Proof will use (NS) Cauchy equivalence for convergence and
also fact that bounded and monotonic sequence converges.
---------------------------------------------------------------*)
-Goalw [Bseq_def] "[| 0 <= x; x < 1 |] ==> Bseq (%n. x ^ n)";
+Goalw [Bseq_def] "[| 0 <= x; x <= 1 |] ==> Bseq (%n. x ^ n)";
by (res_inst_tac [("x","1")] exI 1);
-by (auto_tac (claset() addDs [conjI RS realpow_le]
+by (asm_full_simp_tac (simpset() addsimps [power_abs]) 1);
+by (auto_tac (claset() addDs [power_mono]
addIs [order_less_imp_le],
- simpset() addsimps [abs_eqI1, realpow_abs] ));
+ simpset() addsimps [abs_if] ));
qed "Bseq_realpow";
-Goal "[| 0 <= x; x < 1 |] ==> monoseq (%n. x ^ n)";
-by (blast_tac (claset() addSIs [mono_SucI2,realpow_Suc_le3]) 1);
+Goal "[| 0 <= x; x <= 1 |] ==> monoseq (%n. x ^ n)";
+by (clarify_tac (claset() addSIs [mono_SucI2]) 1);
+by (cut_inst_tac [("n","n"),("N","Suc n"),("a","x")] power_decreasing 1);
+by Auto_tac;
qed "monoseq_realpow";
-Goal "[| 0 <= x; x < 1 |] ==> convergent (%n. x ^ n)";
+Goal "[| 0 <= x; x <= 1 |] ==> convergent (%n. x ^ n)";
by (blast_tac (claset() addSIs [Bseq_monoseq_convergent,
Bseq_realpow,monoseq_realpow]) 1);
qed "convergent_realpow";
@@ -1269,7 +1272,7 @@
by (cut_inst_tac [("a","a"),("x1","inverse x")]
([LIMSEQ_const, LIMSEQ_realpow_zero] MRS LIMSEQ_mult) 1);
by (auto_tac (claset(),
- simpset() addsimps [real_divide_def, realpow_inverse]));
+ simpset() addsimps [real_divide_def, power_inverse]));
by (asm_simp_tac (simpset() addsimps [inverse_eq_divide,
pos_divide_less_eq]) 1);
qed "LIMSEQ_divide_realpow_zero";
@@ -1289,7 +1292,7 @@
Goal "abs(c) < 1 ==> (%n. c ^ n) ----> 0";
by (rtac (LIMSEQ_rabs_zero RS iffD1) 1);
by (auto_tac (claset() addIs [LIMSEQ_rabs_realpow_zero],
- simpset() addsimps [realpow_abs]));
+ simpset() addsimps [power_abs]));
qed "LIMSEQ_rabs_realpow_zero2";
Goal "abs(c) < 1 ==> (%n. c ^ n) ----NS> 0";
--- a/src/HOL/Hyperreal/Series.ML Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/Hyperreal/Series.ML Fri Jan 09 10:46:18 2004 +0100
@@ -575,7 +575,7 @@
summable_comparison_test 1);
by (res_inst_tac [("x","N")] exI 1 THEN Step_tac 1);
by (dtac (le_Suc_ex_iff RS iffD1) 1);
-by (auto_tac (claset(),simpset() addsimps [realpow_add, realpow_not_zero]));
+by (auto_tac (claset(),simpset() addsimps [power_add, realpow_not_zero]));
by (induct_tac "na" 1 THEN Auto_tac);
by (res_inst_tac [("y","c*abs(f(N + n))")] order_trans 1);
by (auto_tac (claset() addIs [mult_right_mono],
--- a/src/HOL/Hyperreal/Transcendental.ML Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/Hyperreal/Transcendental.ML Fri Jan 09 10:46:18 2004 +0100
@@ -15,7 +15,7 @@
val mult_less_cancel_left = thm"mult_less_cancel_left";
Goalw [root_def] "root (Suc n) 0 = 0";
-by (safe_tac (claset() addSIs [some_equality,realpow_zero]
+by (safe_tac (claset() addSIs [some_equality,power_0_Suc]
addSEs [realpow_zero_zero]));
qed "real_root_zero";
Addsimps [real_root_zero];
@@ -34,7 +34,7 @@
Goalw [root_def]
"0 < x ==> root(Suc n) (x ^ (Suc n)) = x";
by (rtac some_equality 1);
-by (forw_inst_tac [("n","n")] realpow_gt_zero 2);
+by (forw_inst_tac [("n","n")] zero_less_power 2);
by (auto_tac (claset(),simpset() addsimps [zero_less_mult_iff]));
by (res_inst_tac [("R1.0","u"),("R2.0","x")] real_linear_less2 1);
by (dres_inst_tac [("n1","n"),("x","u")] (zero_less_Suc RSN (3, realpow_less)) 1);
@@ -52,7 +52,7 @@
by (dres_inst_tac [("n","n")] realpow_pos_nth2 1);
by (Safe_tac THEN rtac someI2 1);
by (auto_tac (claset() addSIs [order_less_imp_le]
- addDs [realpow_gt_zero],simpset() addsimps [zero_less_mult_iff]));
+ addDs [zero_less_power],simpset() addsimps [zero_less_mult_iff]));
qed "real_root_pos_pos";
Goal "0 <= x ==> 0 <= root(Suc n) x";
@@ -66,7 +66,7 @@
by (rtac ccontr 1);
by (res_inst_tac [("R1.0","u"),("R2.0","1")] real_linear_less2 1);
by (dres_inst_tac [("n","n")] realpow_Suc_less_one 1);
-by (dres_inst_tac [("n","n")] realpow_Suc_gt_one 4);
+by (dres_inst_tac [("n","n")] power_gt1_lemma 4);
by (auto_tac (claset(),simpset() addsimps [real_less_not_refl]));
qed "real_root_one";
Addsimps [real_root_one];
@@ -171,8 +171,8 @@
by (Asm_full_simp_tac 1 THEN Asm_full_simp_tac 1);
by (res_inst_tac [("a","xa * x")] someI2 1);
by (auto_tac (claset() addEs [real_less_asym],
- simpset() addsimps mult_ac@[realpow_mult RS sym,realpow_two_disj,
- realpow_gt_zero, real_mult_order] delsimps [realpow_Suc]));
+ simpset() addsimps mult_ac@[power_mult_distrib RS sym,realpow_two_disj,
+ zero_less_power, real_mult_order] delsimps [realpow_Suc]));
qed "real_sqrt_mult_distrib";
Goal "[|0<=x; 0<=y |] ==> sqrt(x*y) = sqrt(x) * sqrt(y)";
@@ -240,8 +240,7 @@
qed "real_sqrt_not_eq_zero";
Goal "0 < x ==> inverse (sqrt(x)) ^ 2 = inverse x";
-by (ftac real_sqrt_not_eq_zero 1);
-by (cut_inst_tac [("n1","2"),("r1","sqrt x")] (realpow_inverse RS sym) 1);
+by (cut_inst_tac [("n1","2"),("a1","sqrt x")] (power_inverse RS sym) 1);
by (auto_tac (claset() addDs [real_sqrt_gt_zero_pow2],simpset()));
qed "real_inv_sqrt_pow2";
@@ -320,7 +319,7 @@
summable_comparison_test 1);
by (rtac summable_exp 2);
by (res_inst_tac [("x","0")] exI 1);
-by (auto_tac (claset(), simpset() addsimps [realpow_abs RS sym,
+by (auto_tac (claset(), simpset() addsimps [power_abs RS sym,
abs_mult,zero_le_mult_iff]));
by (auto_tac (claset() addIs [mult_right_mono],
simpset() addsimps [positive_imp_inverse_positive,abs_eqI2]));
@@ -334,7 +333,7 @@
summable_comparison_test 1);
by (rtac summable_exp 2);
by (res_inst_tac [("x","0")] exI 1);
-by (auto_tac (claset(), simpset() addsimps [realpow_abs RS sym,abs_mult,
+by (auto_tac (claset(), simpset() addsimps [power_abs RS sym,abs_mult,
zero_le_mult_iff]));
by (auto_tac (claset() addSIs [mult_right_mono],
simpset() addsimps [positive_imp_inverse_positive,abs_eqI2]));
@@ -426,7 +425,7 @@
\ sumr 0 (Suc n) (%p. (x ^ (n - p)) * (y ^ p))";
by (case_tac "x = y" 1);
by (auto_tac (claset(),simpset() addsimps [real_mult_commute,
- realpow_add RS sym] delsimps [sumr_Suc]));
+ power_add RS sym] delsimps [sumr_Suc]));
by (res_inst_tac [("c1","x - y")] (real_mult_left_cancel RS iffD1) 1);
by (rtac (minus_minus RS subst) 2);
by (stac minus_mult_left 2);
@@ -454,26 +453,26 @@
by (res_inst_tac [("z","abs (x ^ n)")] (CLAIM_SIMP
"[| (0::real) <z; x*z<=y*z |] ==> x<=y" [mult_le_cancel_left]) 1);
by (auto_tac (claset(),
- simpset() addsimps [mult_assoc,realpow_abs]));
+ simpset() addsimps [mult_assoc,power_abs]));
by (dres_inst_tac [("x","0")] spec 2 THEN Force_tac 2);
-by (auto_tac (claset(),simpset() addsimps [abs_mult,realpow_abs] @ mult_ac));
+by (auto_tac (claset(),simpset() addsimps [abs_mult,power_abs] @ mult_ac));
by (res_inst_tac [("a2","z ^ n")] (abs_ge_zero RS real_le_imp_less_or_eq
RS disjE) 1 THEN dtac sym 2);
by (auto_tac (claset() addSIs [mult_right_mono],
- simpset() addsimps [mult_assoc RS sym, realpow_abs,summable_def]));
+ simpset() addsimps [mult_assoc RS sym, power_abs,summable_def, power_0_left]));
by (res_inst_tac [("x","K * inverse(1 - (abs(z) * inverse(abs x)))")] exI 1);
by (auto_tac (claset() addSIs [sums_mult],simpset() addsimps [mult_assoc]));
by (subgoal_tac
"abs(z ^ n) * inverse(abs x ^ n) = (abs(z) * inverse(abs x)) ^ n" 1);
-by (auto_tac (claset(),simpset() addsimps [realpow_abs RS sym]));
+by (auto_tac (claset(),simpset() addsimps [power_abs RS sym]));
by (subgoal_tac "x ~= 0" 1);
by (subgoal_tac "x ~= 0" 3);
by (auto_tac (claset(),
simpset() delsimps [abs_inverse, abs_mult]
addsimps [abs_inverse RS sym, realpow_not_zero, abs_mult RS sym,
- realpow_inverse, realpow_mult RS sym]));
+ power_inverse, power_mult_distrib RS sym]));
by (auto_tac (claset() addSIs [geometric_sums],
- simpset() addsimps [realpow_abs, inverse_eq_divide]));
+ simpset() addsimps [power_abs, inverse_eq_divide]));
by (res_inst_tac [("z","abs(x)")] (CLAIM_SIMP
"[|(0::real)<z; x*z<y*z |] ==> x<y" [mult_less_cancel_left]) 1);
by (auto_tac (claset(),simpset() addsimps [abs_mult RS sym,mult_assoc]));
@@ -483,7 +482,7 @@
\ ==> summable (%n. f(n) * (z ^ n))";
by (dres_inst_tac [("z","abs z")] powser_insidea 1);
by (auto_tac (claset() addIs [summable_rabs_cancel],
- simpset() addsimps [realpow_abs RS sym]));
+ simpset() addsimps [power_abs RS sym]));
qed "powser_inside";
(* ------------------------------------------------------------------------ *)
@@ -538,7 +537,7 @@
\ (((z + h) ^ (m - p)) - (z ^ (m - p))))";
by (rtac sumr_subst 1);
by (auto_tac (claset(),simpset() addsimps [right_distrib,
- real_diff_def,realpow_add RS sym]
+ real_diff_def,power_add RS sym]
@ mult_ac));
qed "lemma_termdiff1";
@@ -588,23 +587,23 @@
by (auto_tac (claset() addSIs [sumr_bound2],simpset() addsimps [abs_mult]));
by (case_tac "n" 1 THEN Auto_tac);
by (dtac less_add_one 1);
-by (auto_tac (claset(),simpset() addsimps [realpow_add,real_add_assoc RS sym,
+by (auto_tac (claset(),simpset() addsimps [power_add,real_add_assoc RS sym,
CLAIM_SIMP "(a * b) * c = a * (c * (b::real))" mult_ac]
delsimps [sumr_Suc]));
by (auto_tac (claset() addSIs [mult_mono],simpset()delsimps [sumr_Suc]));
-by (auto_tac (claset() addSIs [realpow_le2],simpset() addsimps
- [realpow_abs] delsimps [sumr_Suc] ));
+by (auto_tac (claset() addSIs [power_mono],
+ simpset() addsimps [power_abs] delsimps [sumr_Suc] ));
by (res_inst_tac [("j","real (Suc d) * (K ^ d)")] real_le_trans 1);
by (subgoal_tac "0 <= K" 2);
by (arith_tac 3);
-by (dres_inst_tac [("n","d")] realpow_ge_zero2 2);
+by (dres_inst_tac [("n","d")] zero_le_power 2);
by (auto_tac (claset(),simpset() delsimps [sumr_Suc] ));
by (rtac (sumr_rabs RS real_le_trans) 1);
by (rtac sumr_bound2 1 THEN
auto_tac (claset() addSDs [less_add_one]
- addSIs [mult_mono], simpset() addsimps [abs_mult, realpow_add]));
-by (auto_tac (claset() addSIs [realpow_le2,realpow_ge_zero],simpset() addsimps
- [realpow_abs]));
+ addSIs [mult_mono], simpset() addsimps [abs_mult, power_add]));
+by (auto_tac (claset() addSIs [power_mono,zero_le_power],
+ simpset() addsimps [power_abs]));
by (ALLGOALS(arith_tac));
qed "lemma_termdiff3";
@@ -956,8 +955,8 @@
by (rtac real_le_trans 1);
by (res_inst_tac [("n","2"),("f","(%n. inverse (real (fact n)) * x ^ n)")]
series_pos_le 2);
-by (auto_tac (claset() addIs [summable_exp],simpset()
- addsimps [numeral_2_eq_2,realpow_ge_zero,zero_le_mult_iff]));
+by (auto_tac (claset() addIs [summable_exp],simpset()
+ addsimps [numeral_2_eq_2,zero_le_power,zero_le_mult_iff]));
qed "exp_ge_add_one_self";
Addsimps [exp_ge_add_one_self];
@@ -1233,8 +1232,8 @@
(* ------------------------------------------------------------------------ *)
Goalw [sin_def] "sin 0 = 0";
-by (auto_tac (claset() addSIs [(sums_unique RS sym),
- LIMSEQ_const],simpset() addsimps [sums_def]));
+by (auto_tac (claset() addSIs [sums_unique RS sym, LIMSEQ_const],
+ simpset() addsimps [sums_def] delsimps [power_0_left]));
qed "sin_zero";
Addsimps [sin_zero];
@@ -1361,7 +1360,7 @@
Goalw [real_le_def] "abs(sin x) <= 1";
by (rtac notI 1);
-by (dtac realpow_two_gt_one 1);
+by (dres_inst_tac [("n","Suc 0")] power_gt1 1);
by (auto_tac (claset(),simpset() delsimps [realpow_Suc]));
by (dres_inst_tac [("r1","cos x")] (realpow_two_le RSN
(2, real_gt_one_ge_zero_add_less)) 1);
@@ -1389,7 +1388,7 @@
Goalw [real_le_def] "abs(cos x) <= 1";
by (rtac notI 1);
-by (dtac realpow_two_gt_one 1);
+by (dres_inst_tac [("n","Suc 0")] power_gt1 1);
by (auto_tac (claset(),simpset() delsimps [realpow_Suc]));
by (dres_inst_tac [("r1","sin x")] (realpow_two_le RSN
(2, real_gt_one_ge_zero_add_less)) 1);
@@ -1606,7 +1605,7 @@
CLAIM "x * (x * x ^ (4*m)) = (x ^ (4*m)) * (x * (x::real))"]
delsimps [fact_Suc]));
by (subgoal_tac "0 < x ^ (4 * m)" 1);
-by (asm_simp_tac (simpset() addsimps [realpow_gt_zero]) 2);
+by (asm_simp_tac (simpset() addsimps [zero_less_power]) 2);
by (asm_simp_tac (simpset() addsimps [mult_less_cancel_left]) 1);
by (rtac real_mult_less_mono 1); (*mult_strict_mono would be stronger*)
by (ALLGOALS(Asm_simp_tac));
@@ -1624,7 +1623,7 @@
by (auto_tac (claset(),
simpset() addsimps [cos_squared_eq,
minus_add_distrib RS sym, neg_less_0_iff_less,sin_gt_zero1,
- real_add_order,realpow_gt_zero,cos_double]
+ real_add_order,zero_less_power,cos_double]
delsimps [realpow_Suc,minus_add_distrib]));
qed "cos_double_less_one";
@@ -1635,7 +1634,7 @@
by (auto_tac (claset(),simpset() addsimps mult_ac@[cos_def]));
qed "cos_paired";
-Addsimps [realpow_gt_zero];
+Addsimps [zero_less_power];
Goal "cos (2) < 0";
by (cut_inst_tac [("x","2")] cos_paired 1);
@@ -2376,11 +2375,11 @@
Addsimps [cos_arctan_not_zero];
Goal "cos x ~= 0 ==> 1 + tan(x) ^ 2 = inverse(cos x) ^ 2";
-by (rtac (realpow_inverse RS subst) 1);
+by (rtac (power_inverse RS subst) 1);
by (res_inst_tac [("c1","cos(x) ^ 2")] (real_mult_right_cancel RS iffD1) 1);
by (auto_tac (claset() addDs [realpow_not_zero], simpset() addsimps
- [realpow_mult,left_distrib,realpow_divide,
- tan_def,real_mult_assoc,realpow_inverse RS sym]
+ [power_mult_distrib,left_distrib,realpow_divide,
+ tan_def,real_mult_assoc,power_inverse RS sym]
delsimps [realpow_Suc]));
qed "tan_sec";
@@ -2430,7 +2429,7 @@
Goal "cos (2 * real (n::nat) * pi) = 1";
by (auto_tac (claset(),simpset() addsimps [cos_double,
- real_mult_assoc,realpow_add RS sym,numeral_2_eq_2]));
+ real_mult_assoc,power_add RS sym,numeral_2_eq_2]));
(*FIXME: just needs x^n for literals!*)
qed "cos_2npi";
Addsimps [cos_2npi];
@@ -2584,14 +2583,14 @@
\ ==> root(Suc n) (x * y) = root(Suc n) x * root(Suc n) y";
by (rtac real_root_pos_unique 1);
by (auto_tac (claset() addSIs [real_root_pos_pos_le],simpset()
- addsimps [realpow_mult,zero_le_mult_iff,
+ addsimps [power_mult_distrib,zero_le_mult_iff,
real_root_pow_pos2] delsimps [realpow_Suc]));
qed "real_root_mult";
Goal "0 <= x ==> (root(Suc n) (inverse x) = inverse(root(Suc n) x))";
by (rtac real_root_pos_unique 1);
by (auto_tac (claset() addIs [real_root_pos_pos_le],simpset()
- addsimps [realpow_inverse RS sym,real_root_pow_pos2]
+ addsimps [power_inverse RS sym,real_root_pow_pos2]
delsimps [realpow_Suc]));
qed "real_root_inverse";
@@ -3035,8 +3034,8 @@
by (rtac add_mono 1);
by (auto_tac (claset(),simpset() delsimps [realpow_Suc]));
by (ALLGOALS(rtac ((CLAIM "(2::real) ^ 2 = 4") RS subst)));
-by (ALLGOALS(rtac (realpow_mult RS subst)));
-by (ALLGOALS(rtac realpow_le));
+by (ALLGOALS(rtac (power_mult_distrib RS subst)));
+by (ALLGOALS(rtac power_mono));
by Auto_tac;
qed "lemma_sqrt_hcomplex_capprox";
--- a/src/HOL/Integ/Int.thy Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/Integ/Int.thy Fri Jan 09 10:46:18 2004 +0100
@@ -148,6 +148,7 @@
instance int :: ordered_ring
proof
fix i j k :: int
+ show "0 < (1::int)" by (rule int_0_less_1)
show "i \<le> j ==> k + i \<le> k + j" by simp
show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: zmult_zless_mono2)
show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
--- a/src/HOL/Integ/IntDef.thy Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/Integ/IntDef.thy Fri Jan 09 10:46:18 2004 +0100
@@ -344,7 +344,8 @@
show "i * j = j * i" by (rule zmult_commute)
show "1 * i = i" by simp
show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
- show "0 \<noteq> (1::int)" by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq)
+ show "0 \<noteq> (1::int)"
+ by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq)
assume eq: "k+i = k+j"
hence "(-k + k) + i = (-k + k) + j" by (simp only: eq zadd_assoc)
thus "i = j" by simp
--- a/src/HOL/Integ/IntPower.thy Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/Integ/IntPower.thy Fri Jan 09 10:46:18 2004 +0100
@@ -15,6 +15,15 @@
power_Suc: "p ^ (Suc n) = (p::int) * (p ^ n)"
+instance int :: ringpower
+proof
+ fix z :: int
+ fix n :: nat
+ show "z^0 = 1" by simp
+ show "z^(Suc n) = z * (z^n)" by simp
+qed
+
+
lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
apply (induct_tac "y", auto)
apply (rule zmod_zmult1_eq [THEN trans])
@@ -22,27 +31,11 @@
apply (rule zmod_zmult_distrib [symmetric])
done
-lemma zpower_1 [simp]: "1^y = (1::int)"
-by (induct_tac "y", auto)
-
-lemma zpower_zmult_distrib: "(x*z)^y = ((x^y)*(z^y)::int)"
-by (induct_tac "y", auto)
-
lemma zpower_zadd_distrib: "x^(y+z) = ((x^y)*(x^z)::int)"
-by (induct_tac "y", auto)
+ by (rule Power.power_add)
lemma zpower_zpower: "(x^y)^z = (x^(y*z)::int)"
-apply (induct_tac "y", auto)
-apply (subst zpower_zmult_distrib)
-apply (subst zpower_zadd_distrib)
-apply (simp (no_asm_simp))
-done
-
-
-(*** Logical equivalences for inequalities ***)
-
-lemma zpower_eq_0_iff [simp]: "(x^n = 0) = (x = (0::int) & 0<n)"
-by (induct_tac "n", auto)
+ by (rule Power.power_mult [symmetric])
lemma zero_less_zpower_abs_iff [simp]:
"(0 < (abs x)^n) = (x \<noteq> (0::int) | n=0)"
@@ -58,11 +51,8 @@
ML
{*
val zpower_zmod = thm "zpower_zmod";
-val zpower_1 = thm "zpower_1";
-val zpower_zmult_distrib = thm "zpower_zmult_distrib";
val zpower_zadd_distrib = thm "zpower_zadd_distrib";
val zpower_zpower = thm "zpower_zpower";
-val zpower_eq_0_iff = thm "zpower_eq_0_iff";
val zero_less_zpower_abs_iff = thm "zero_less_zpower_abs_iff";
val zero_le_zpower_abs = thm "zero_le_zpower_abs";
*}
--- a/src/HOL/IsaMakefile Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/IsaMakefile Fri Jan 09 10:46:18 2004 +0100
@@ -93,7 +93,7 @@
Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy Nat.ML \
Nat.thy NatArith.ML NatArith.thy Numeral.thy \
- Power.ML Power.thy PreList.thy Product_Type.ML Product_Type.thy ROOT.ML \
+ Power.thy PreList.thy Product_Type.ML Product_Type.thy ROOT.ML \
Recdef.thy Record.thy Relation.ML Relation.thy Relation_Power.ML \
Relation_Power.thy Ring_and_Field.thy\
Set.ML Set.thy SetInterval.ML SetInterval.thy \
@@ -152,8 +152,7 @@
Hyperreal/HyperArith0.thy Hyperreal/HyperArith.thy\
Hyperreal/HyperBin.ML Hyperreal/HyperBin.thy \
Hyperreal/HyperDef.thy Hyperreal/HyperNat.ML Hyperreal/HyperNat.thy\
- Hyperreal/HyperOrd.thy Hyperreal/HyperPow.ML\
- Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\
+ Hyperreal/HyperOrd.thy Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\
Hyperreal/Lim.ML Hyperreal/Lim.thy Hyperreal/Log.ML Hyperreal/Log.thy\
Hyperreal/MacLaurin.ML Hyperreal/MacLaurin.thy\
Hyperreal/NatStar.ML Hyperreal/NatStar.thy\
--- a/src/HOL/Library/Rational_Numbers.thy Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/Library/Rational_Numbers.thy Fri Jan 09 10:46:18 2004 +0100
@@ -514,8 +514,7 @@
by (induct q, induct r)
(simp add: mult_rat divide_rat inverse_rat zero_rat eq_rat)
show "0 \<noteq> (1::rat)"
- by (simp add: zero_rat_def one_rat_def rat_of_equality
- zero_fraction_def one_fraction_def)
+ by (simp add: zero_rat one_rat eq_rat)
assume eq: "s+q = s+r"
hence "(-s + s) + q = (-s + s) + r" by (simp only: eq rat_add_assoc)
thus "q = r" by (simp add: rat_left_minus rat_add_0)
@@ -592,6 +591,8 @@
instance rat :: ordered_field
proof
fix q r s :: rat
+ show "0 < (1::rat)"
+ by (simp add: zero_rat one_rat less_rat)
show "q \<le> r ==> s + q \<le> s + r"
proof (induct q, induct r, induct s)
fix a b c d e f :: int
--- a/src/HOL/Nat.thy Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/Nat.thy Fri Jan 09 10:46:18 2004 +0100
@@ -771,6 +771,7 @@
instance nat :: ordered_semiring
proof
fix i j k :: nat
+ show "0 < (1::nat)" by simp
show "i \<le> j ==> k + i \<le> k + j" by simp
show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2)
qed
--- a/src/HOL/NumberTheory/EvenOdd.thy Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/NumberTheory/EvenOdd.thy Fri Jan 09 10:46:18 2004 +0100
@@ -173,7 +173,7 @@
also have "(-1::int)^2 = 1";
by auto
finally; show ?thesis;
- by (auto simp add: zpower_1)
+ by auto
qed;
qed;
@@ -199,7 +199,7 @@
also have "(-1::int)^2 = 1";
by auto
finally; show ?thesis;
- by (auto simp add: zpower_1)
+ by auto
qed;
qed;
--- a/src/HOL/Power.ML Fri Jan 09 01:28:24 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,191 +0,0 @@
-(* Title: HOL/Power.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
-
-The (overloaded) exponentiation operator, ^ :: [nat,nat]=>nat
-Also binomial coefficents
-*)
-
-(*** Simple laws about Power ***)
-
-Goal "!!i::nat. i ^ (j+k) = (i^j) * (i^k)";
-by (induct_tac "k" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps mult_ac)));
-qed "power_add";
-
-Goal "!!i::nat. i ^ (j*k) = (i^j) ^ k";
-by (induct_tac "k" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [power_add])));
-qed "power_mult";
-
-Goal "!!i::nat. 0 < i ==> 0 < i^n";
-by (induct_tac "n" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "zero_less_power";
-Addsimps [zero_less_power];
-
-Goal "i^n = 0 ==> i = (0::nat)";
-by (etac contrapos_pp 1);
-by Auto_tac;
-qed "power_eq_0D";
-
-Goal "!!i::nat. 1 <= i ==> Suc 0 <= i^n";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "one_le_power";
-Addsimps [one_le_power];
-
-Goal "!!i::nat. 1 < i ==> !m. (i^n = i^m) = (n=m)";
-by (induct_tac "n" 1);
-by Auto_tac;
-by (ALLGOALS (case_tac "m"));
-by (Simp_tac 1);
-by Auto_tac;
-qed_spec_mp "power_inject";
-Addsimps [power_inject];
-
-Goalw [dvd_def] "!!i::nat. m<=n ==> i^m dvd i^n";
-by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
-by (asm_simp_tac (simpset() addsimps [power_add]) 1);
-qed "le_imp_power_dvd";
-
-Goal "(1::nat) < i ==> \\<forall>n. i ^ m <= i ^ n --> m <= n";
-by (induct_tac "m" 1);
-by Auto_tac;
-by (case_tac "na" 1);
-by Auto_tac;
-by (subgoal_tac "Suc 1 * 1 <= i * i^n" 1);
-by (Asm_full_simp_tac 1);
-by (rtac mult_le_mono 1);
-by Auto_tac;
-qed_spec_mp "power_le_imp_le";
-
-Goal "!!i::nat. [| 0 < i; i^m < i^n |] ==> m < n";
-by (rtac ccontr 1);
-by (dtac (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1);
-by (etac zero_less_power 1);
-by (contr_tac 1);
-qed "power_less_imp_less";
-
-Goal "k^j dvd n --> i<=j --> k^i dvd (n::nat)";
-by (induct_tac "j" 1);
-by (ALLGOALS (simp_tac (simpset() addsimps [le_Suc_eq])));
-by (blast_tac (claset() addSDs [dvd_mult_right]) 1);
-qed_spec_mp "power_le_dvd";
-
-Goal "[|i^m dvd i^n; (1::nat) < i|] ==> m <= n";
-by (rtac power_le_imp_le 1);
-by (assume_tac 1);
-by (etac dvd_imp_le 1);
-by (Asm_full_simp_tac 1);
-qed "power_dvd_imp_le";
-
-
-(*** Logical equivalences for inequalities ***)
-
-Goal "(x^n = 0) = (x = (0::nat) & 0<n)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "power_eq_0_iff";
-Addsimps [power_eq_0_iff];
-
-Goal "(0 < x^n) = (x ~= (0::nat) | n=0)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "zero_less_power_iff";
-Addsimps [zero_less_power_iff];
-
-Goal "(0::nat) <= x^n";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "zero_le_power";
-Addsimps [zero_le_power];
-
-
-(**** Binomial Coefficients, following Andy Gordon and Florian Kammueller ****)
-
-Goal "(n choose 0) = 1";
-by (case_tac "n" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "binomial_n_0";
-
-Goal "(0 choose Suc k) = 0";
-by (Simp_tac 1);
-qed "binomial_0_Suc";
-
-Goal "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)";
-by (Simp_tac 1);
-qed "binomial_Suc_Suc";
-
-Goal "ALL k. n < k --> (n choose k) = 0";
-by (induct_tac "n" 1);
-by Auto_tac;
-by (etac allE 1);
-by (etac mp 1);
-by (arith_tac 1);
-qed_spec_mp "binomial_eq_0";
-
-Addsimps [binomial_n_0, binomial_0_Suc, binomial_Suc_Suc];
-Delsimps [binomial_0, binomial_Suc];
-
-Goal "(n choose n) = 1";
-by (induct_tac "n" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [binomial_eq_0])));
-qed "binomial_n_n";
-Addsimps [binomial_n_n];
-
-Goal "(Suc n choose n) = Suc n";
-by (induct_tac "n" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "binomial_Suc_n";
-Addsimps [binomial_Suc_n];
-
-Goal "(n choose Suc 0) = n";
-by (induct_tac "n" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "binomial_1";
-Addsimps [binomial_1];
-
-Goal "k <= n --> 0 < (n choose k)";
-by (res_inst_tac [("m","n"),("n","k")] diff_induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed_spec_mp "zero_less_binomial";
-
-Goal "(n choose k = 0) = (n<k)";
-by (safe_tac (claset() addSIs [binomial_eq_0]));
-by (etac contrapos_pp 1);
-by (asm_full_simp_tac (simpset() addsimps [zero_less_binomial]) 1);
-qed "binomial_eq_0_iff";
-
-Goal "(0 < n choose k) = (k<=n)";
-by (simp_tac (simpset() addsimps [linorder_not_less RS sym,
- binomial_eq_0_iff RS sym]) 1);
-qed "zero_less_binomial_iff";
-
-(*Might be more useful if re-oriented*)
-Goal "ALL k. k <= n --> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k";
-by (induct_tac "n" 1);
-by (simp_tac (simpset() addsimps [binomial_0]) 1);
-by (Clarify_tac 1);
-by (case_tac "k" 1);
-by (auto_tac (claset(),
- simpset() addsimps [add_mult_distrib, add_mult_distrib2,
- le_Suc_eq, binomial_eq_0]));
-qed_spec_mp "Suc_times_binomial_eq";
-
-(*This is the well-known version, but it's harder to use because of the
- need to reason about division.*)
-Goal "k <= n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k";
-by (asm_simp_tac (simpset()
- addsimps [Suc_times_binomial_eq, div_mult_self_is_m, zero_less_Suc]
- delsimps [mult_Suc, mult_Suc_right]) 1);
-qed "binomial_Suc_Suc_eq_times";
-
-(*Another version, with -1 instead of Suc.*)
-Goal "[|k <= n; 0<k|] ==> (n choose k) * k = n * ((n - 1) choose (k - 1))";
-by (cut_inst_tac [("n","n - 1"),("k","k - 1")] Suc_times_binomial_eq 1);
-by (asm_full_simp_tac (simpset() addsplits [nat_diff_split]) 1);
-by Auto_tac;
-qed "times_binomial_minus1_eq";
-
--- a/src/HOL/Power.thy Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/Power.thy Fri Jan 09 10:46:18 2004 +0100
@@ -3,23 +3,451 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1997 University of Cambridge
-The (overloaded) exponentiation operator, ^ :: [nat,nat]=>nat
-Also binomial coefficents
*)
-Power = Divides +
-consts
- binomial :: "[nat,nat] => nat" (infixl "choose" 65)
+header{*Exponentiation and Binomial Coefficients*}
+
+theory Power = Divides:
+
+subsection{*Powers for Arbitrary (Semi)Rings*}
+
+axclass ringpower \<subseteq> semiring, power
+ power_0 [simp]: "a ^ 0 = 1"
+ power_Suc: "a ^ (Suc n) = a * (a ^ n)"
+
+lemma power_0_Suc [simp]: "(0::'a::ringpower) ^ (Suc n) = 0"
+by (simp add: power_Suc)
+
+text{*It looks plausible as a simprule, but its effect can be strange.*}
+lemma power_0_left: "0^n = (if n=0 then 1 else (0::'a::ringpower))"
+by (induct_tac "n", auto)
+
+lemma power_one [simp]: "1^n = (1::'a::ringpower)"
+apply (induct_tac "n")
+apply (auto simp add: power_Suc)
+done
+
+lemma power_one_right [simp]: "(a::'a::ringpower) ^ 1 = a"
+by (simp add: power_Suc)
+
+lemma power_add: "(a::'a::ringpower) ^ (m+n) = (a^m) * (a^n)"
+apply (induct_tac "n")
+apply (simp_all add: power_Suc mult_ac)
+done
+
+lemma power_mult: "(a::'a::ringpower) ^ (m*n) = (a^m) ^ n"
+apply (induct_tac "n")
+apply (simp_all add: power_Suc power_add)
+done
+
+lemma power_mult_distrib: "((a::'a::ringpower) * b) ^ n = (a^n) * (b^n)"
+apply (induct_tac "n")
+apply (auto simp add: power_Suc mult_ac)
+done
+
+lemma zero_less_power:
+ "0 < (a::'a::{ordered_semiring,ringpower}) ==> 0 < a^n"
+apply (induct_tac "n")
+apply (simp_all add: power_Suc zero_less_one mult_pos)
+done
+
+lemma zero_le_power:
+ "0 \<le> (a::'a::{ordered_semiring,ringpower}) ==> 0 \<le> a^n"
+apply (simp add: order_le_less)
+apply (erule disjE)
+apply (simp_all add: zero_less_power zero_less_one power_0_left)
+done
+
+lemma one_le_power:
+ "1 \<le> (a::'a::{ordered_semiring,ringpower}) ==> 1 \<le> a^n"
+apply (induct_tac "n")
+apply (simp_all add: power_Suc)
+apply (rule order_trans [OF _ mult_mono [of 1 _ 1]])
+apply (simp_all add: zero_le_one order_trans [OF zero_le_one])
+done
+
+lemma gt1_imp_ge0: "1 < a ==> 0 \<le> (a::'a::ordered_semiring)"
+ by (simp add: order_trans [OF zero_le_one order_less_imp_le])
+
+lemma power_gt1_lemma:
+ assumes gt1: "1 < (a::'a::{ordered_semiring,ringpower})"
+ shows "1 < a * a^n"
+proof -
+ have "1*1 < a * a^n"
+ proof (rule order_less_le_trans)
+ show "1*1 < a*1" by (simp add: gt1)
+ show "a*1 \<le> a * a^n"
+ by (simp only: mult_mono gt1 gt1_imp_ge0 one_le_power order_less_imp_le
+ zero_le_one order_refl)
+ qed
+ thus ?thesis by simp
+qed
+
+lemma power_gt1:
+ "1 < (a::'a::{ordered_semiring,ringpower}) ==> 1 < a ^ (Suc n)"
+by (simp add: power_gt1_lemma power_Suc)
+
+lemma power_le_imp_le_exp:
+ assumes gt1: "(1::'a::{ringpower,ordered_semiring}) < a"
+ shows "!!n. a^m \<le> a^n ==> m \<le> n"
+proof (induct "m")
+ case 0
+ show ?case by simp
+next
+ case (Suc m)
+ show ?case
+ proof (cases n)
+ case 0
+ from prems have "a * a^m \<le> 1" by (simp add: power_Suc)
+ with gt1 show ?thesis
+ by (force simp only: power_gt1_lemma
+ linorder_not_less [symmetric])
+ next
+ case (Suc n)
+ from prems show ?thesis
+ by (force dest: mult_left_le_imp_le
+ simp add: power_Suc order_less_trans [OF zero_less_one gt1])
+ qed
+qed
+
+text{*Surely we can strengthen this? It holds for 0<a<1 too.*}
+lemma power_inject_exp [simp]:
+ "1 < (a::'a::{ordered_semiring,ringpower}) ==> (a^m = a^n) = (m=n)"
+ by (force simp add: order_antisym power_le_imp_le_exp)
+
+text{*Can relax the first premise to @{term "0<a"} in the case of the
+natural numbers.*}
+lemma power_less_imp_less_exp:
+ "[| (1::'a::{ringpower,ordered_semiring}) < a; a^m < a^n |] ==> m < n"
+by (simp add: order_less_le [of m n] order_less_le [of "a^m" "a^n"]
+ power_le_imp_le_exp)
+
+
+lemma power_mono:
+ "[|a \<le> b; (0::'a::{ringpower,ordered_semiring}) \<le> a|] ==> a^n \<le> b^n"
+apply (induct_tac "n")
+apply (simp_all add: power_Suc)
+apply (auto intro: mult_mono zero_le_power order_trans [of 0 a b])
+done
+
+lemma power_strict_mono [rule_format]:
+ "[|a < b; (0::'a::{ringpower,ordered_semiring}) \<le> a|]
+ ==> 0 < n --> a^n < b^n"
+apply (induct_tac "n")
+apply (auto simp add: mult_strict_mono zero_le_power power_Suc
+ order_le_less_trans [of 0 a b])
+done
+
+lemma power_eq_0_iff [simp]:
+ "(a^n = 0) = (a = (0::'a::{ordered_ring,ringpower}) & 0<n)"
+apply (induct_tac "n")
+apply (auto simp add: power_Suc zero_neq_one [THEN not_sym])
+done
+
+lemma field_power_eq_0_iff [simp]:
+ "(a^n = 0) = (a = (0::'a::{field,ringpower}) & 0<n)"
+apply (induct_tac "n")
+apply (auto simp add: power_Suc field_mult_eq_0_iff zero_neq_one[THEN not_sym])
+done
+
+lemma field_power_not_zero: "a \<noteq> (0::'a::{field,ringpower}) ==> a^n \<noteq> 0"
+by force
+
+text{*Perhaps these should be simprules.*}
+lemma power_inverse:
+ "inverse ((a::'a::{field,division_by_zero,ringpower}) ^ n) = (inverse a) ^ n"
+apply (induct_tac "n")
+apply (auto simp add: power_Suc inverse_mult_distrib)
+done
+
+lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_field,ringpower}) ^ n"
+apply (induct_tac "n")
+apply (auto simp add: power_Suc abs_mult)
+done
+
+lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{ring,ringpower}) ^ n"
+proof -
+ have "-a = (- 1) * a" by (simp add: minus_mult_left [symmetric])
+ thus ?thesis by (simp only: power_mult_distrib)
+qed
+
+text{*Lemma for @{text power_strict_decreasing}*}
+lemma power_Suc_less:
+ "[|(0::'a::{ordered_semiring,ringpower}) < a; a < 1|]
+ ==> a * a^n < a^n"
+apply (induct_tac n)
+apply (auto simp add: power_Suc mult_strict_left_mono)
+done
+
+lemma power_strict_decreasing:
+ "[|n < N; 0 < a; a < (1::'a::{ordered_semiring,ringpower})|]
+ ==> a^N < a^n"
+apply (erule rev_mp)
+apply (induct_tac "N")
+apply (auto simp add: power_Suc power_Suc_less less_Suc_eq)
+apply (rename_tac m)
+apply (subgoal_tac "a * a^m < 1 * a^n", simp)
+apply (rule mult_strict_mono)
+apply (auto simp add: zero_le_power zero_less_one order_less_imp_le)
+done
+
+text{*Proof resembles that of @{text power_strict_decreasing}*}
+lemma power_decreasing:
+ "[|n \<le> N; 0 \<le> a; a \<le> (1::'a::{ordered_semiring,ringpower})|]
+ ==> a^N \<le> a^n"
+apply (erule rev_mp)
+apply (induct_tac "N")
+apply (auto simp add: power_Suc le_Suc_eq)
+apply (rename_tac m)
+apply (subgoal_tac "a * a^m \<le> 1 * a^n", simp)
+apply (rule mult_mono)
+apply (auto simp add: zero_le_power zero_le_one)
+done
+
+lemma power_Suc_less_one:
+ "[| 0 < a; a < (1::'a::{ordered_semiring,ringpower}) |] ==> a ^ Suc n < 1"
+apply (insert power_strict_decreasing [of 0 "Suc n" a], simp)
+done
+
+text{*Proof again resembles that of @{text power_strict_decreasing}*}
+lemma power_increasing:
+ "[|n \<le> N; (1::'a::{ordered_semiring,ringpower}) \<le> a|] ==> a^n \<le> a^N"
+apply (erule rev_mp)
+apply (induct_tac "N")
+apply (auto simp add: power_Suc le_Suc_eq)
+apply (rename_tac m)
+apply (subgoal_tac "1 * a^n \<le> a * a^m", simp)
+apply (rule mult_mono)
+apply (auto simp add: order_trans [OF zero_le_one] zero_le_power)
+done
+
+text{*Lemma for @{text power_strict_increasing}*}
+lemma power_less_power_Suc:
+ "(1::'a::{ordered_semiring,ringpower}) < a ==> a^n < a * a^n"
+apply (induct_tac n)
+apply (auto simp add: power_Suc mult_strict_left_mono order_less_trans [OF zero_less_one])
+done
+
+lemma power_strict_increasing:
+ "[|n < N; (1::'a::{ordered_semiring,ringpower}) < a|] ==> a^n < a^N"
+apply (erule rev_mp)
+apply (induct_tac "N")
+apply (auto simp add: power_less_power_Suc power_Suc less_Suc_eq)
+apply (rename_tac m)
+apply (subgoal_tac "1 * a^n < a * a^m", simp)
+apply (rule mult_strict_mono)
+apply (auto simp add: order_less_trans [OF zero_less_one] zero_le_power
+ order_less_imp_le)
+done
+
+lemma power_le_imp_le_base:
+ assumes le: "a ^ Suc n \<le> b ^ Suc n"
+ and xnonneg: "(0::'a::{ordered_semiring,ringpower}) \<le> a"
+ and ynonneg: "0 \<le> b"
+ shows "a \<le> b"
+ proof (rule ccontr)
+ assume "~ a \<le> b"
+ then have "b < a" by (simp only: linorder_not_le)
+ then have "b ^ Suc n < a ^ Suc n"
+ by (simp only: prems power_strict_mono)
+ from le and this show "False"
+ by (simp add: linorder_not_less [symmetric])
+ qed
+
+lemma power_inject_base:
+ "[| a ^ Suc n = b ^ Suc n; 0 \<le> a; 0 \<le> b |]
+ ==> a = (b::'a::{ordered_semiring,ringpower})"
+by (blast intro: power_le_imp_le_base order_antisym order_eq_refl sym)
+
+
+subsection{*Exponentiation for the Natural Numbers*}
primrec (power)
"p ^ 0 = 1"
"p ^ (Suc n) = (p::nat) * (p ^ n)"
+instance nat :: ringpower
+proof
+ fix z :: nat
+ fix n :: nat
+ show "z^0 = 1" by simp
+ show "z^(Suc n) = z * (z^n)" by simp
+qed
+
+lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n"
+by (insert one_le_power [of i n], simp)
+
+lemma le_imp_power_dvd: "!!i::nat. m \<le> n ==> i^m dvd i^n"
+apply (unfold dvd_def)
+apply (erule not_less_iff_le [THEN iffD2, THEN add_diff_inverse, THEN subst])
+apply (simp add: power_add)
+done
+
+text{*Valid for the naturals, but what if @{text"0<i<1"}?
+Premises cannot be weakened: consider the case where @{term "i=0"},
+@{term "m=1"} and @{term "n=0"}.*}
+lemma nat_power_less_imp_less: "!!i::nat. [| 0 < i; i^m < i^n |] ==> m < n"
+apply (rule ccontr)
+apply (drule leI [THEN le_imp_power_dvd, THEN dvd_imp_le, THEN leD])
+apply (erule zero_less_power, auto)
+done
+
+lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)"
+by (induct_tac "n", auto)
+
+lemma power_le_dvd [rule_format]: "k^j dvd n --> i\<le>j --> k^i dvd (n::nat)"
+apply (induct_tac "j")
+apply (simp_all add: le_Suc_eq)
+apply (blast dest!: dvd_mult_right)
+done
+
+lemma power_dvd_imp_le: "[|i^m dvd i^n; (1::nat) < i|] ==> m \<le> n"
+apply (rule power_le_imp_le_exp, assumption)
+apply (erule dvd_imp_le, simp)
+done
+
+
+subsection{*Binomial Coefficients*}
+
+text{*This development is based on the work of Andy Gordon and
+Florian Kammueller*}
+
+consts
+ binomial :: "[nat,nat] => nat" (infixl "choose" 65)
+
primrec
- binomial_0 "(0 choose k) = (if k = 0 then 1 else 0)"
+ binomial_0: "(0 choose k) = (if k = 0 then 1 else 0)"
+
+ binomial_Suc: "(Suc n choose k) =
+ (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
+
+lemma binomial_n_0 [simp]: "(n choose 0) = 1"
+by (case_tac "n", simp_all)
+
+lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0"
+by simp
+
+lemma binomial_Suc_Suc [simp]:
+ "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)"
+by simp
+
+lemma binomial_eq_0 [rule_format]: "\<forall>k. n < k --> (n choose k) = 0"
+apply (induct_tac "n", auto)
+apply (erule allE)
+apply (erule mp, arith)
+done
+
+declare binomial_0 [simp del] binomial_Suc [simp del]
+
+lemma binomial_n_n [simp]: "(n choose n) = 1"
+apply (induct_tac "n")
+apply (simp_all add: binomial_eq_0)
+done
+
+lemma binomial_Suc_n [simp]: "(Suc n choose n) = Suc n"
+by (induct_tac "n", simp_all)
+
+lemma binomial_1 [simp]: "(n choose Suc 0) = n"
+by (induct_tac "n", simp_all)
+
+lemma zero_less_binomial [rule_format]: "k \<le> n --> 0 < (n choose k)"
+by (rule_tac m = n and n = k in diff_induct, simp_all)
- binomial_Suc "(Suc n choose k) =
- (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
+lemma binomial_eq_0_iff: "(n choose k = 0) = (n<k)"
+apply (safe intro!: binomial_eq_0)
+apply (erule contrapos_pp)
+apply (simp add: zero_less_binomial)
+done
+
+lemma zero_less_binomial_iff: "(0 < n choose k) = (k\<le>n)"
+by (simp add: linorder_not_less [symmetric] binomial_eq_0_iff [symmetric])
+
+(*Might be more useful if re-oriented*)
+lemma Suc_times_binomial_eq [rule_format]:
+ "\<forall>k. k \<le> n --> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
+apply (induct_tac "n")
+apply (simp add: binomial_0, clarify)
+apply (case_tac "k")
+apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq
+ binomial_eq_0)
+done
+
+text{*This is the well-known version, but it's harder to use because of the
+ need to reason about division.*}
+lemma binomial_Suc_Suc_eq_times:
+ "k \<le> n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"
+by (simp add: Suc_times_binomial_eq div_mult_self_is_m zero_less_Suc
+ del: mult_Suc mult_Suc_right)
+
+text{*Another version, with -1 instead of Suc.*}
+lemma times_binomial_minus1_eq:
+ "[|k \<le> n; 0<k|] ==> (n choose k) * k = n * ((n - 1) choose (k - 1))"
+apply (cut_tac n = "n - 1" and k = "k - 1" in Suc_times_binomial_eq)
+apply (simp split add: nat_diff_split, auto)
+done
+
+text{*ML bindings for the general exponentiation theorems*}
+ML
+{*
+val power_0 = thm"power_0";
+val power_Suc = thm"power_Suc";
+val power_0_Suc = thm"power_0_Suc";
+val power_0_left = thm"power_0_left";
+val power_one = thm"power_one";
+val power_one_right = thm"power_one_right";
+val power_add = thm"power_add";
+val power_mult = thm"power_mult";
+val power_mult_distrib = thm"power_mult_distrib";
+val zero_less_power = thm"zero_less_power";
+val zero_le_power = thm"zero_le_power";
+val one_le_power = thm"one_le_power";
+val gt1_imp_ge0 = thm"gt1_imp_ge0";
+val power_gt1_lemma = thm"power_gt1_lemma";
+val power_gt1 = thm"power_gt1";
+val power_le_imp_le_exp = thm"power_le_imp_le_exp";
+val power_inject_exp = thm"power_inject_exp";
+val power_less_imp_less_exp = thm"power_less_imp_less_exp";
+val power_mono = thm"power_mono";
+val power_strict_mono = thm"power_strict_mono";
+val power_eq_0_iff = thm"power_eq_0_iff";
+val field_power_eq_0_iff = thm"field_power_eq_0_iff";
+val field_power_not_zero = thm"field_power_not_zero";
+val power_inverse = thm"power_inverse";
+val power_abs = thm"power_abs";
+val power_minus = thm"power_minus";
+val power_Suc_less = thm"power_Suc_less";
+val power_strict_decreasing = thm"power_strict_decreasing";
+val power_decreasing = thm"power_decreasing";
+val power_Suc_less_one = thm"power_Suc_less_one";
+val power_increasing = thm"power_increasing";
+val power_strict_increasing = thm"power_strict_increasing";
+val power_le_imp_le_base = thm"power_le_imp_le_base";
+val power_inject_base = thm"power_inject_base";
+*}
+
+text{*ML bindings for the remaining theorems*}
+ML
+{*
+val nat_one_le_power = thm"nat_one_le_power";
+val le_imp_power_dvd = thm"le_imp_power_dvd";
+val nat_power_less_imp_less = thm"nat_power_less_imp_less";
+val nat_zero_less_power_iff = thm"nat_zero_less_power_iff";
+val power_le_dvd = thm"power_le_dvd";
+val power_dvd_imp_le = thm"power_dvd_imp_le";
+val binomial_n_0 = thm"binomial_n_0";
+val binomial_0_Suc = thm"binomial_0_Suc";
+val binomial_Suc_Suc = thm"binomial_Suc_Suc";
+val binomial_eq_0 = thm"binomial_eq_0";
+val binomial_n_n = thm"binomial_n_n";
+val binomial_Suc_n = thm"binomial_Suc_n";
+val binomial_1 = thm"binomial_1";
+val zero_less_binomial = thm"zero_less_binomial";
+val binomial_eq_0_iff = thm"binomial_eq_0_iff";
+val zero_less_binomial_iff = thm"zero_less_binomial_iff";
+val Suc_times_binomial_eq = thm"Suc_times_binomial_eq";
+val binomial_Suc_Suc_eq_times = thm"binomial_Suc_Suc_eq_times";
+val times_binomial_minus1_eq = thm"times_binomial_minus1_eq";
+*}
end
--- a/src/HOL/Real/RealDef.thy Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/Real/RealDef.thy Fri Jan 09 10:46:18 2004 +0100
@@ -825,6 +825,9 @@
instance real :: ordered_field
proof
fix x y z :: real
+ show "0 < (1::real)"
+ by (force intro: real_gt_zero_preal_Ex [THEN iffD2]
+ simp add: real_one_def real_of_preal_def)
show "x \<le> y ==> z + x \<le> z + y" by (rule real_add_left_mono)
show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: real_mult_less_mono2)
show "\<bar>x\<bar> = (if x < 0 then -x else x)"
--- a/src/HOL/Real/RealPow.thy Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/Real/RealPow.thy Fri Jan 09 10:46:18 2004 +0100
@@ -8,6 +8,8 @@
theory RealPow = RealArith:
+declare abs_mult_self [simp]
+
instance real :: power ..
primrec (realpow)
@@ -15,118 +17,45 @@
realpow_Suc: "r ^ (Suc n) = (r::real) * (r ^ n)"
-lemma realpow_zero [simp]: "(0::real) ^ (Suc n) = 0"
-by auto
+instance real :: ringpower
+proof
+ fix z :: real
+ fix n :: nat
+ show "z^0 = 1" by simp
+ show "z^(Suc n) = z * (z^n)" by simp
+qed
-lemma realpow_not_zero [rule_format]: "r \<noteq> (0::real) --> r ^ n \<noteq> 0"
-by (induct_tac "n", auto)
+
+lemma realpow_not_zero: "r \<noteq> (0::real) ==> r ^ n \<noteq> 0"
+ by (rule field_power_not_zero)
lemma realpow_zero_zero: "r ^ n = (0::real) ==> r = 0"
-apply (rule ccontr)
-apply (auto dest: realpow_not_zero)
-done
-
-lemma realpow_inverse: "inverse ((r::real) ^ n) = (inverse r) ^ n"
-apply (induct_tac "n")
-apply (auto simp add: inverse_mult_distrib)
-done
-
-lemma realpow_abs: "abs(r ^ n) = abs(r::real) ^ n"
-apply (induct_tac "n")
-apply (auto simp add: abs_mult)
-done
-
-lemma realpow_add: "(r::real) ^ (n + m) = (r ^ n) * (r ^ m)"
-apply (induct_tac "n")
-apply (auto simp add: mult_ac)
-done
-
-lemma realpow_one [simp]: "(r::real) ^ 1 = r"
by simp
lemma realpow_two: "(r::real)^ (Suc (Suc 0)) = r * r"
by simp
-lemma realpow_gt_zero [rule_format]: "(0::real) < r --> 0 < r ^ n"
-apply (induct_tac "n")
-apply (auto intro: real_mult_order simp add: zero_less_one)
-done
-
-lemma realpow_ge_zero [rule_format]: "(0::real) \<le> r --> 0 \<le> r ^ n"
-apply (induct_tac "n")
-apply (auto simp add: zero_le_mult_iff)
-done
-
-lemma realpow_le [rule_format]: "(0::real) \<le> x & x \<le> y --> x ^ n \<le> y ^ n"
-apply (induct_tac "n")
-apply (auto intro!: mult_mono)
-apply (simp (no_asm_simp) add: realpow_ge_zero)
-done
-
-lemma realpow_0_left [rule_format, simp]:
- "0 < n --> 0 ^ n = (0::real)"
-apply (induct_tac "n", auto)
+text{*Legacy: weaker version of the theorem @{text power_strict_mono},
+used 6 times in NthRoot and Transcendental*}
+lemma realpow_less:
+ "[|(0::real) < x; x < y; 0 < n|] ==> x ^ n < y ^ n"
+apply (rule power_strict_mono, auto)
done
-lemma realpow_less' [rule_format]:
- "[|(0::real) \<le> x; x < y |] ==> 0 < n --> x ^ n < y ^ n"
-apply (induct n)
-apply (auto simp add: real_mult_less_mono' realpow_ge_zero)
-done
-
-text{*Legacy: weaker version of the theorem above*}
-lemma realpow_less:
- "[|(0::real) < x; x < y; 0 < n|] ==> x ^ n < y ^ n"
-apply (rule realpow_less', auto)
-done
-
-lemma realpow_eq_one [simp]: "1 ^ n = (1::real)"
-by (induct_tac "n", auto)
-
lemma abs_realpow_minus_one [simp]: "abs((-1) ^ n) = (1::real)"
-apply (induct_tac "n")
-apply (auto simp add: abs_mult)
-done
-
-lemma realpow_mult: "((r::real) * s) ^ n = (r ^ n) * (s ^ n)"
-apply (induct_tac "n")
-apply (auto simp add: mult_ac)
-done
+by (simp add: power_abs)
lemma realpow_two_le [simp]: "(0::real) \<le> r^ Suc (Suc 0)"
by (simp add: real_le_square)
lemma abs_realpow_two [simp]: "abs((x::real)^Suc (Suc 0)) = x^Suc (Suc 0)"
-by (simp add: abs_eqI1 real_le_square)
+by (simp add: abs_mult)
lemma realpow_two_abs [simp]: "abs(x::real)^Suc (Suc 0) = x^Suc (Suc 0)"
-by (simp add: realpow_abs [symmetric] abs_eqI1 del: realpow_Suc)
-
-lemma realpow_two_gt_one: "(1::real) < r ==> 1 < r^ (Suc (Suc 0))"
-apply auto
-apply (cut_tac real_zero_less_one)
-apply (frule_tac x = 0 in order_less_trans, assumption)
-apply (frule_tac c = r and a = 1 in mult_strict_right_mono)
-apply assumption;
-apply (simp add: );
-done
-
-lemma realpow_ge_one [rule_format]: "(1::real) < r --> 1 \<le> r ^ n"
-apply (induct_tac "n", auto)
-apply (subgoal_tac "1*1 \<le> r * r^n")
-apply (rule_tac [2] mult_mono, auto)
-done
-
-lemma realpow_ge_one2: "(1::real) \<le> r ==> 1 \<le> r ^ n"
-apply (drule order_le_imp_less_or_eq)
-apply (auto dest: realpow_ge_one)
-done
+by (simp add: power_abs [symmetric] abs_eqI1 del: realpow_Suc)
lemma two_realpow_ge_one [simp]: "(1::real) \<le> 2 ^ n"
-apply (rule_tac y = "1 ^ n" in order_trans)
-apply (rule_tac [2] realpow_le)
-apply (auto intro: order_less_imp_le)
-done
+by (insert power_increasing [of 0 n "2::real"], simp)
lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n"
apply (induct_tac "n")
@@ -145,111 +74,38 @@
lemma realpow_minus_one_even [simp]: "(-1) ^ Suc (Suc (2*n)) = (1::real)"
by auto
-lemma realpow_Suc_less [rule_format]:
- "(0::real) < r & r < (1::real) --> r ^ Suc n < r ^ n"
- by (induct_tac "n", auto simp add: mult_less_cancel_left)
-
-lemma realpow_Suc_le [rule_format]:
- "0 \<le> r & r < (1::real) --> r ^ Suc n \<le> r ^ n"
-apply (induct_tac "n")
-apply (auto intro: order_less_imp_le dest!: order_le_imp_less_or_eq)
-done
-
-lemma realpow_zero_le [simp]: "(0::real) \<le> 0 ^ n"
-by (case_tac "n", auto)
-
-lemma realpow_Suc_le2 [rule_format]: "0 < r & r < (1::real) --> r ^ Suc n \<le> r ^ n"
-by (blast intro!: order_less_imp_le realpow_Suc_less)
+lemma realpow_Suc_le_self: "[| 0 \<le> r; r \<le> (1::real) |] ==> r ^ Suc n \<le> r"
+by (insert power_decreasing [of 1 "Suc n" r], simp)
-lemma realpow_Suc_le3: "[| 0 \<le> r; r < (1::real) |] ==> r ^ Suc n \<le> r ^ n"
-apply (erule order_le_imp_less_or_eq [THEN disjE])
-apply (rule realpow_Suc_le2, auto)
-done
+text{*Used ONCE in Transcendental*}
+lemma realpow_Suc_less_one: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n < 1"
+by (insert power_strict_decreasing [of 0 "Suc n" r], simp)
-lemma realpow_less_le [rule_format]: "0 \<le> r & r < (1::real) & n < N --> r ^ N \<le> r ^ n"
-apply (induct_tac "N")
-apply (simp_all (no_asm_simp))
-apply clarify
-apply (subgoal_tac "r * r ^ na \<le> 1 * r ^ n", simp)
-apply (rule mult_mono)
-apply (auto simp add: realpow_ge_zero less_Suc_eq)
-done
-
-lemma realpow_le_le: "[| 0 \<le> r; r < (1::real); n \<le> N |] ==> r ^ N \<le> r ^ n"
-apply (drule_tac n = N in le_imp_less_or_eq)
-apply (auto intro: realpow_less_le)
+text{*Used ONCE in Lim.ML*}
+lemma realpow_minus_mult [rule_format]:
+ "0 < n --> (x::real) ^ (n - 1) * x = x ^ n"
+apply (simp split add: nat_diff_split)
done
-lemma realpow_Suc_le_self: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n \<le> r"
-by (drule_tac n = 1 and N = "Suc n" in order_less_imp_le [THEN realpow_le_le], auto)
-
-lemma realpow_Suc_less_one: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n < 1"
-by (blast intro: realpow_Suc_le_self order_le_less_trans)
-
-lemma realpow_le_Suc [rule_format]: "(1::real) \<le> r --> r ^ n \<le> r ^ Suc n"
-by (induct_tac "n", auto)
-
-lemma realpow_less_Suc [rule_format]: "(1::real) < r --> r ^ n < r ^ Suc n"
-by (induct_tac "n", auto simp add: mult_less_cancel_left)
-
-lemma realpow_le_Suc2 [rule_format]: "(1::real) < r --> r ^ n \<le> r ^ Suc n"
-by (blast intro!: order_less_imp_le realpow_less_Suc)
-
-(*One use in RealPow.thy*)
-lemma real_mult_self_le2: "[| (1::real) \<le> r; (1::real) \<le> x |] ==> x \<le> r * x"
-apply (subgoal_tac "1 * x \<le> r * x", simp)
-apply (rule mult_right_mono, auto)
-done
-
-lemma realpow_gt_ge2 [rule_format]: "(1::real) \<le> r & n < N --> r ^ n \<le> r ^ N"
-apply (induct_tac "N", auto)
-apply (frule_tac [!] n = na in realpow_ge_one2)
-apply (drule_tac [!] real_mult_self_le2, assumption)
-prefer 2 apply assumption
-apply (auto intro: order_trans simp add: less_Suc_eq)
-done
-
-lemma realpow_ge_ge2: "[| (1::real) \<le> r; n \<le> N |] ==> r ^ n \<le> r ^ N"
-apply (drule_tac n = N in le_imp_less_or_eq)
-apply (auto intro: realpow_gt_ge2)
-done
-
-lemma realpow_Suc_ge_self2: "(1::real) \<le> r ==> r \<le> r ^ Suc n"
-by (drule_tac n = 1 and N = "Suc n" in realpow_ge_ge2, auto)
-
-(*Used ONCE in Hyperreal/NthRoot.ML*)
-lemma realpow_ge_self2: "[| (1::real) \<le> r; 0 < n |] ==> r \<le> r ^ n"
-apply (drule less_not_refl2 [THEN not0_implies_Suc])
-apply (auto intro!: realpow_Suc_ge_self2)
-done
-
-lemma realpow_minus_mult [rule_format, simp]:
- "0 < n --> (x::real) ^ (n - 1) * x = x ^ n"
-apply (induct_tac "n")
-apply (auto simp add: real_mult_commute)
-done
-
-lemma realpow_two_mult_inverse [simp]: "r \<noteq> 0 ==> r * inverse r ^Suc (Suc 0) = inverse (r::real)"
+lemma realpow_two_mult_inverse [simp]:
+ "r \<noteq> 0 ==> r * inverse r ^Suc (Suc 0) = inverse (r::real)"
by (simp add: realpow_two real_mult_assoc [symmetric])
-(* 05/00 *)
lemma realpow_two_minus [simp]: "(-x)^Suc (Suc 0) = (x::real)^Suc (Suc 0)"
by simp
-lemma realpow_two_diff: "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
+lemma realpow_two_diff:
+ "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
apply (unfold real_diff_def)
apply (simp add: right_distrib left_distrib mult_ac)
done
-lemma realpow_two_disj: "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)"
+lemma realpow_two_disj:
+ "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)"
apply (cut_tac x = x and y = y in realpow_two_diff)
apply (auto simp del: realpow_Suc)
done
-(* used in Transc *)
-lemma realpow_diff: "[|(x::real) \<noteq> 0; m \<le> n |] ==> x ^ (n - m) = x ^ n * inverse (x ^ m)"
-by (auto simp add: le_eq_less_or_eq less_iff_Suc_add realpow_add realpow_not_zero mult_ac)
-
lemma realpow_real_of_nat: "real (m::nat) ^ n = real (m ^ n)"
apply (induct_tac "n")
apply (auto simp add: real_of_nat_one real_of_nat_mult)
@@ -261,29 +117,12 @@
done
lemma realpow_increasing:
- assumes xnonneg: "(0::real) \<le> x"
- and ynonneg: "0 \<le> y"
- and le: "x ^ Suc n \<le> y ^ Suc n"
- shows "x \<le> y"
- proof (rule ccontr)
- assume "~ x \<le> y"
- then have "y<x" by simp
- then have "y ^ Suc n < x ^ Suc n"
- by (simp only: prems realpow_less')
- from le and this show "False"
- by simp
- qed
-
-lemma realpow_Suc_cancel_eq: "[| (0::real) \<le> x; 0 \<le> y; x ^ Suc n = y ^ Suc n |] ==> x = y"
-by (blast intro: realpow_increasing order_antisym order_eq_refl sym)
+ "[|(0::real) \<le> x; 0 \<le> y; x ^ Suc n \<le> y ^ Suc n|] ==> x \<le> y"
+ by (rule power_le_imp_le_base)
-(*** Logical equivalences for inequalities ***)
-
-lemma realpow_eq_0_iff [simp]: "(x^n = 0) = (x = (0::real) & 0<n)"
-by (induct_tac "n", auto)
-
-lemma zero_less_realpow_abs_iff [simp]: "(0 < (abs x)^n) = (x \<noteq> (0::real) | n=0)"
+lemma zero_less_realpow_abs_iff [simp]:
+ "(0 < (abs x)^n) = (x \<noteq> (0::real) | n=0)"
apply (induct_tac "n")
apply (auto simp add: zero_less_mult_iff)
done
@@ -294,7 +133,7 @@
done
-(*** Literal arithmetic involving powers, type real ***)
+subsection{*Literal Arithmetic Involving Powers, Type @{typ real}*}
lemma real_of_int_power: "real (x::int) ^ n = real (x ^ n)"
apply (induct_tac "n")
@@ -302,7 +141,8 @@
done
declare real_of_int_power [symmetric, simp]
-lemma power_real_number_of: "(number_of v :: real) ^ n = real ((number_of v :: int) ^ n)"
+lemma power_real_number_of:
+ "(number_of v :: real) ^ n = real ((number_of v :: int) ^ n)"
by (simp only: real_number_of_def real_of_int_power)
declare power_real_number_of [of _ "number_of w", standard, simp]
@@ -311,20 +151,6 @@
lemma real_power_two: "(r::real)\<twosuperior> = r * r"
by (simp add: numeral_2_eq_2)
-lemma real_sqr_ge_zero [iff]: "0 \<le> (r::real)\<twosuperior>"
- by (simp add: real_power_two)
-
-lemma real_sqr_gt_zero: "(r::real) \<noteq> 0 ==> 0 < r\<twosuperior>"
-proof -
- assume "r \<noteq> 0"
- hence "0 \<noteq> r\<twosuperior>" by simp
- also have "0 \<le> r\<twosuperior>" by (simp add: real_sqr_ge_zero)
- finally show ?thesis .
-qed
-
-lemma real_sqr_not_zero: "r \<noteq> 0 ==> (r::real)\<twosuperior> \<noteq> 0"
- by simp
-
subsection{*Various Other Theorems*}
@@ -333,25 +159,19 @@
by (auto intro: real_sum_squares_cancel)
lemma real_squared_diff_one_factored: "x*x - (1::real) = (x + 1)*(x - 1)"
-apply (auto simp add: left_distrib right_distrib real_diff_def)
-done
+by (auto simp add: left_distrib right_distrib real_diff_def)
-lemma real_mult_is_one: "(x*x = (1::real)) = (x = 1 | x = - 1)"
+lemma real_mult_is_one [simp]: "(x*x = (1::real)) = (x = 1 | x = - 1)"
apply auto
apply (drule right_minus_eq [THEN iffD2])
apply (auto simp add: real_squared_diff_one_factored)
done
-declare real_mult_is_one [iff]
lemma real_le_add_half_cancel: "(x + y/2 \<le> (y::real)) = (x \<le> y /2)"
-apply auto
-done
-declare real_le_add_half_cancel [simp]
+by auto
-lemma real_minus_half_eq: "(x::real) - x/2 = x/2"
-apply auto
-done
-declare real_minus_half_eq [simp]
+lemma real_minus_half_eq [simp]: "(x::real) - x/2 = x/2"
+by auto
lemma real_mult_inverse_cancel:
"[|(0::real) < x; 0 < x1; x1 * y < x * u |]
@@ -364,34 +184,22 @@
done
text{*Used once: in Hyperreal/Transcendental.ML*}
-lemma real_mult_inverse_cancel2: "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
+lemma real_mult_inverse_cancel2:
+ "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
apply (auto dest: real_mult_inverse_cancel simp add: mult_ac)
done
-lemma inverse_real_of_nat_gt_zero: "0 < inverse (real (Suc n))"
-apply auto
-done
-declare inverse_real_of_nat_gt_zero [simp]
+lemma inverse_real_of_nat_gt_zero [simp]: "0 < inverse (real (Suc n))"
+by auto
-lemma inverse_real_of_nat_ge_zero: "0 \<le> inverse (real (Suc n))"
-apply auto
-done
-declare inverse_real_of_nat_ge_zero [simp]
+lemma inverse_real_of_nat_ge_zero [simp]: "0 \<le> inverse (real (Suc n))"
+by auto
lemma real_sum_squares_not_zero: "x ~= 0 ==> x * x + y * y ~= (0::real)"
-apply (blast dest!: real_sum_squares_cancel)
-done
+by (blast dest!: real_sum_squares_cancel)
lemma real_sum_squares_not_zero2: "y ~= 0 ==> x * x + y * y ~= (0::real)"
-apply (blast dest!: real_sum_squares_cancel2)
-done
-
-(* nice theorem *)
-lemma abs_mult_abs: "abs x * abs x = x * (x::real)"
-apply (insert linorder_less_linear [of x 0])
-apply (auto simp add: abs_eqI2 abs_minus_eqI2)
-done
-declare abs_mult_abs [simp]
+by (blast dest!: real_sum_squares_cancel2)
subsection {*Various Other Theorems*}
@@ -399,50 +207,29 @@
lemma realpow_divide:
"(x/y) ^ n = ((x::real) ^ n/ y ^ n)"
apply (unfold real_divide_def)
-apply (auto simp add: realpow_mult realpow_inverse)
-done
-
-lemma realpow_ge_zero2 [rule_format (no_asm)]: "(0::real) \<le> r --> 0 \<le> r ^ n"
-apply (induct_tac "n")
-apply (auto simp add: zero_le_mult_iff)
+apply (auto simp add: power_mult_distrib power_inverse)
done
-lemma realpow_le2 [rule_format (no_asm)]: "(0::real) \<le> x & x \<le> y --> x ^ n \<le> y ^ n"
-apply (induct_tac "n")
-apply (auto intro!: mult_mono simp add: realpow_ge_zero2)
-done
-
-lemma realpow_Suc_gt_one: "(1::real) < r ==> 1 < r ^ (Suc n)"
-apply (frule_tac n = "n" in realpow_ge_one)
-apply (drule real_le_imp_less_or_eq, safe)
-apply (frule zero_less_one [THEN real_less_trans])
-apply (drule_tac y = "r ^ n" in real_mult_less_mono2)
-apply assumption
-apply (auto dest: real_less_trans)
+lemma realpow_two_sum_zero_iff [simp]:
+ "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
+apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2
+ simp add: real_power_two)
done
-lemma realpow_two_sum_zero_iff: "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
-apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 simp add: numeral_2_eq_2)
-done
-declare realpow_two_sum_zero_iff [simp]
-
-lemma realpow_two_le_add_order: "(0::real) \<le> u ^ 2 + v ^ 2"
+lemma realpow_two_le_add_order [simp]: "(0::real) \<le> u ^ 2 + v ^ 2"
apply (rule real_le_add_order)
-apply (auto simp add: numeral_2_eq_2)
+apply (auto simp add: real_power_two)
done
-declare realpow_two_le_add_order [simp]
-lemma realpow_two_le_add_order2: "(0::real) \<le> u ^ 2 + v ^ 2 + w ^ 2"
+lemma realpow_two_le_add_order2 [simp]: "(0::real) \<le> u ^ 2 + v ^ 2 + w ^ 2"
apply (rule real_le_add_order)+
-apply (auto simp add: numeral_2_eq_2)
+apply (auto simp add: real_power_two)
done
-declare realpow_two_le_add_order2 [simp]
lemma real_sum_square_gt_zero: "x ~= 0 ==> (0::real) < x * x + y * y"
-apply (cut_tac x = "x" and y = "y" in real_mult_self_sum_ge_zero)
+apply (cut_tac x = x and y = y in real_mult_self_sum_ge_zero)
apply (drule real_le_imp_less_or_eq)
-apply (drule_tac y = "y" in real_sum_squares_not_zero)
-apply auto
+apply (drule_tac y = y in real_sum_squares_not_zero, auto)
done
lemma real_sum_square_gt_zero2: "y ~= 0 ==> (0::real) < x * x + y * y"
@@ -450,48 +237,29 @@
apply (erule real_sum_square_gt_zero)
done
-lemma real_minus_mult_self_le: "-(u * u) \<le> (x * (x::real))"
-apply (rule_tac j = "0" in real_le_trans)
-apply auto
-done
-declare real_minus_mult_self_le [simp]
+lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))"
+by (rule_tac j = 0 in real_le_trans, auto)
-lemma realpow_square_minus_le: "-(u ^ 2) \<le> (x::real) ^ 2"
-apply (auto simp add: numeral_2_eq_2)
-done
-declare realpow_square_minus_le [simp]
+lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2"
+by (auto simp add: real_power_two)
lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
-apply (case_tac "n")
-apply auto
-done
+by (case_tac "n", auto)
-lemma real_num_zero_less_two_pow: "0 < (2::real) ^ (4*d)"
+lemma real_num_zero_less_two_pow [simp]: "0 < (2::real) ^ (4*d)"
apply (induct_tac "d")
apply (auto simp add: realpow_num_eq_if)
done
-declare real_num_zero_less_two_pow [simp]
-lemma lemma_realpow_num_two_mono: "x * (4::real) < y ==> x * (2 ^ 8) < y * (2 ^ 6)"
+lemma lemma_realpow_num_two_mono:
+ "x * (4::real) < y ==> x * (2 ^ 8) < y * (2 ^ 6)"
apply (subgoal_tac " (2::real) ^ 8 = 4 * (2 ^ 6) ")
apply (simp (no_asm_simp) add: real_mult_assoc [symmetric])
apply (auto simp add: realpow_num_eq_if)
done
-lemma lemma_realpow_4: "2 ^ 2 = (4::real)"
-apply (simp (no_asm) add: realpow_num_eq_if)
-done
-declare lemma_realpow_4 [simp]
-
-lemma lemma_realpow_16: "2 ^ 4 = (16::real)"
-apply (simp (no_asm) add: realpow_num_eq_if)
-done
-declare lemma_realpow_16 [simp]
-
-lemma zero_le_x_squared: "(0::real) \<le> x^2"
-apply (simp add: numeral_2_eq_2)
-done
-declare zero_le_x_squared [simp]
+lemma zero_le_x_squared [simp]: "(0::real) \<le> x^2"
+by (simp add: real_power_two)
@@ -500,67 +268,33 @@
val realpow_0 = thm "realpow_0";
val realpow_Suc = thm "realpow_Suc";
-val realpow_zero = thm "realpow_zero";
val realpow_not_zero = thm "realpow_not_zero";
val realpow_zero_zero = thm "realpow_zero_zero";
-val realpow_inverse = thm "realpow_inverse";
-val realpow_abs = thm "realpow_abs";
-val realpow_add = thm "realpow_add";
-val realpow_one = thm "realpow_one";
val realpow_two = thm "realpow_two";
-val realpow_gt_zero = thm "realpow_gt_zero";
-val realpow_ge_zero = thm "realpow_ge_zero";
-val realpow_le = thm "realpow_le";
-val realpow_0_left = thm "realpow_0_left";
val realpow_less = thm "realpow_less";
-val realpow_eq_one = thm "realpow_eq_one";
val abs_realpow_minus_one = thm "abs_realpow_minus_one";
-val realpow_mult = thm "realpow_mult";
val realpow_two_le = thm "realpow_two_le";
val abs_realpow_two = thm "abs_realpow_two";
val realpow_two_abs = thm "realpow_two_abs";
-val realpow_two_gt_one = thm "realpow_two_gt_one";
-val realpow_ge_one = thm "realpow_ge_one";
-val realpow_ge_one2 = thm "realpow_ge_one2";
val two_realpow_ge_one = thm "two_realpow_ge_one";
val two_realpow_gt = thm "two_realpow_gt";
val realpow_minus_one = thm "realpow_minus_one";
val realpow_minus_one_odd = thm "realpow_minus_one_odd";
val realpow_minus_one_even = thm "realpow_minus_one_even";
-val realpow_Suc_less = thm "realpow_Suc_less";
-val realpow_Suc_le = thm "realpow_Suc_le";
-val realpow_zero_le = thm "realpow_zero_le";
-val realpow_Suc_le2 = thm "realpow_Suc_le2";
-val realpow_Suc_le3 = thm "realpow_Suc_le3";
-val realpow_less_le = thm "realpow_less_le";
-val realpow_le_le = thm "realpow_le_le";
val realpow_Suc_le_self = thm "realpow_Suc_le_self";
val realpow_Suc_less_one = thm "realpow_Suc_less_one";
-val realpow_le_Suc = thm "realpow_le_Suc";
-val realpow_less_Suc = thm "realpow_less_Suc";
-val realpow_le_Suc2 = thm "realpow_le_Suc2";
-val realpow_gt_ge2 = thm "realpow_gt_ge2";
-val realpow_ge_ge2 = thm "realpow_ge_ge2";
-val realpow_Suc_ge_self2 = thm "realpow_Suc_ge_self2";
-val realpow_ge_self2 = thm "realpow_ge_self2";
val realpow_minus_mult = thm "realpow_minus_mult";
val realpow_two_mult_inverse = thm "realpow_two_mult_inverse";
val realpow_two_minus = thm "realpow_two_minus";
val realpow_two_disj = thm "realpow_two_disj";
-val realpow_diff = thm "realpow_diff";
val realpow_real_of_nat = thm "realpow_real_of_nat";
val realpow_real_of_nat_two_pos = thm "realpow_real_of_nat_two_pos";
val realpow_increasing = thm "realpow_increasing";
-val realpow_Suc_cancel_eq = thm "realpow_Suc_cancel_eq";
-val realpow_eq_0_iff = thm "realpow_eq_0_iff";
val zero_less_realpow_abs_iff = thm "zero_less_realpow_abs_iff";
val zero_le_realpow_abs = thm "zero_le_realpow_abs";
val real_of_int_power = thm "real_of_int_power";
val power_real_number_of = thm "power_real_number_of";
val real_power_two = thm "real_power_two";
-val real_sqr_ge_zero = thm "real_sqr_ge_zero";
-val real_sqr_gt_zero = thm "real_sqr_gt_zero";
-val real_sqr_not_zero = thm "real_sqr_not_zero";
val real_sum_squares_cancel_a = thm "real_sum_squares_cancel_a";
val real_mult_inverse_cancel2 = thm "real_mult_inverse_cancel2";
val real_squared_diff_one_factored = thm "real_squared_diff_one_factored";
@@ -573,12 +307,8 @@
val inverse_real_of_nat_ge_zero = thm "inverse_real_of_nat_ge_zero";
val real_sum_squares_not_zero = thm "real_sum_squares_not_zero";
val real_sum_squares_not_zero2 = thm "real_sum_squares_not_zero2";
-val abs_mult_abs = thm "abs_mult_abs";
val realpow_divide = thm "realpow_divide";
-val realpow_ge_zero2 = thm "realpow_ge_zero2";
-val realpow_le2 = thm "realpow_le2";
-val realpow_Suc_gt_one = thm "realpow_Suc_gt_one";
val realpow_two_sum_zero_iff = thm "realpow_two_sum_zero_iff";
val realpow_two_le_add_order = thm "realpow_two_le_add_order";
val realpow_two_le_add_order2 = thm "realpow_two_le_add_order2";
@@ -589,8 +319,6 @@
val realpow_num_eq_if = thm "realpow_num_eq_if";
val real_num_zero_less_two_pow = thm "real_num_zero_less_two_pow";
val lemma_realpow_num_two_mono = thm "lemma_realpow_num_two_mono";
-val lemma_realpow_4 = thm "lemma_realpow_4";
-val lemma_realpow_16 = thm "lemma_realpow_16";
val zero_le_x_squared = thm "zero_le_x_squared";
*}
--- a/src/HOL/Ring_and_Field.thy Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/Ring_and_Field.thy Fri Jan 09 10:46:18 2004 +0100
@@ -38,6 +38,7 @@
diff_minus: "a - b = a + (-b)"
axclass ordered_semiring \<subseteq> semiring, linorder
+ zero_less_one: "0 < 1" --{*This axiom too is needed for semirings only.*}
add_left_mono: "a \<le> b ==> c + a \<le> c + b"
mult_strict_left_mono: "a < b ==> 0 < c ==> c * a < c * b"
@@ -484,6 +485,22 @@
"[|a \<le> b; 0 \<le> c|] ==> a*c \<le> b * (c::'a::ordered_semiring)"
by (simp add: mult_left_mono mult_commute [of _ c])
+lemma mult_left_le_imp_le:
+ "[|c*a \<le> c*b; 0 < c|] ==> a \<le> (b::'a::ordered_semiring)"
+ by (force simp add: mult_strict_left_mono linorder_not_less [symmetric])
+
+lemma mult_right_le_imp_le:
+ "[|a*c \<le> b*c; 0 < c|] ==> a \<le> (b::'a::ordered_semiring)"
+ by (force simp add: mult_strict_right_mono linorder_not_less [symmetric])
+
+lemma mult_left_less_imp_less:
+ "[|c*a < c*b; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)"
+ by (force simp add: mult_left_mono linorder_not_le [symmetric])
+
+lemma mult_right_less_imp_less:
+ "[|a*c < b*c; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)"
+ by (force simp add: mult_right_mono linorder_not_le [symmetric])
+
lemma mult_strict_left_mono_neg:
"[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring)"
apply (drule mult_strict_left_mono [of _ _ "-c"])
@@ -552,12 +569,7 @@
lemma zero_le_square: "(0::'a::ordered_ring) \<le> a*a"
by (simp add: zero_le_mult_iff linorder_linear)
-lemma zero_less_one: "(0::'a::ordered_ring) < 1"
-apply (insert zero_le_square [of 1])
-apply (simp add: order_less_le)
-done
-
-lemma zero_le_one: "(0::'a::ordered_ring) \<le> 1"
+lemma zero_le_one: "(0::'a::ordered_semiring) \<le> 1"
by (rule zero_less_one [THEN order_less_imp_le])
@@ -708,7 +720,7 @@
text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement
of an ordering.*}
-lemma field_mult_eq_0_iff: "(a*b = (0::'a::field)) = (a = 0 | b = 0)"
+lemma field_mult_eq_0_iff [simp]: "(a*b = (0::'a::field)) = (a = 0 | b = 0)"
proof cases
assume "a=0" thus ?thesis by simp
next
@@ -733,7 +745,7 @@
by (simp add: mult_assoc cnz)
qed
-lemma field_mult_cancel_right:
+lemma field_mult_cancel_right [simp]:
"(a*c = b*c) = (c = (0::'a::field) | a=b)"
proof cases
assume "c=0" thus ?thesis by simp
@@ -742,7 +754,7 @@
thus ?thesis by (force dest: field_mult_cancel_right_lemma)
qed
-lemma field_mult_cancel_left:
+lemma field_mult_cancel_left [simp]:
"(c*a = c*b) = (c = (0::'a::field) | a=b)"
by (simp add: mult_commute [of c] field_mult_cancel_right)
@@ -1401,6 +1413,10 @@
minus_mult_left [symmetric] minus_mult_right [symmetric])
done
+
+lemma abs_mult_self: "abs a * abs a = a * (a::'a::ordered_ring)"
+by (simp add: abs_if)
+
lemma abs_eq_0 [simp]: "(abs a = 0) = (a = (0::'a::ordered_ring))"
by (simp add: abs_if)
@@ -1617,6 +1633,10 @@
val mult_strict_right_mono = thm"mult_strict_right_mono";
val mult_left_mono = thm"mult_left_mono";
val mult_right_mono = thm"mult_right_mono";
+val mult_left_le_imp_le = thm"mult_left_le_imp_le";
+val mult_right_le_imp_le = thm"mult_right_le_imp_le";
+val mult_left_less_imp_less = thm"mult_left_less_imp_less";
+val mult_right_less_imp_less = thm"mult_right_less_imp_less";
val mult_strict_left_mono_neg = thm"mult_strict_left_mono_neg";
val mult_strict_right_mono_neg = thm"mult_strict_right_mono_neg";
val mult_pos = thm"mult_pos";
@@ -1744,6 +1764,7 @@
val abs_zero = thm"abs_zero";
val abs_one = thm"abs_one";
val abs_mult = thm"abs_mult";
+val abs_mult_self = thm"abs_mult_self";
val abs_eq_0 = thm"abs_eq_0";
val zero_less_abs_iff = thm"zero_less_abs_iff";
val abs_not_less_zero = thm"abs_not_less_zero";