--- a/src/HOL/Real/RealPow.ML Fri Dec 15 12:32:35 2000 +0100
+++ b/src/HOL/Real/RealPow.ML Fri Dec 15 17:41:38 2000 +0100
@@ -6,7 +6,7 @@
*)
Goal "(#0::real) ^ (Suc n) = #0";
-by (Auto_tac);
+by Auto_tac;
qed "realpow_zero";
Addsimps [realpow_zero];
@@ -87,7 +87,7 @@
Goal "#1 ^ n = (#1::real)";
by (induct_tac "n" 1);
-by (Auto_tac);
+by Auto_tac;
qed "realpow_eq_one";
Addsimps [realpow_eq_one];
@@ -97,18 +97,13 @@
qed "abs_minus_realpow_one";
Addsimps [abs_minus_realpow_one];
-Goal "abs((-#1) ^ n) = (#1::real)";
+Goal "abs((#-1) ^ n) = (#1::real)";
by (induct_tac "n" 1);
by (auto_tac (claset(),simpset() addsimps [abs_mult,
abs_minus_cancel,abs_one]));
qed "abs_realpow_minus_one";
Addsimps [abs_realpow_minus_one];
-Goal "abs((#-1) ^ n) = (#1::real)";
-by (rtac (simplify (simpset()) abs_realpow_minus_one) 1);
-qed "abs_realpow_minus_one2";
-Addsimps [abs_realpow_minus_one2];
-
Goal "((r::real) * s) ^ n = (r ^ n) * (s ^ n)";
by (induct_tac "n" 1);
by (auto_tac (claset(),simpset() addsimps real_mult_ac));
@@ -200,33 +195,25 @@
qed "two_realpow_gt";
Addsimps [two_realpow_gt,two_realpow_ge_one];
-Goal "(-#1) ^ (2*n) = (#1::real)";
+Goal "(#-1) ^ (#2*n) = (#1::real)";
by (induct_tac "n" 1);
-by (Auto_tac);
+by Auto_tac;
qed "realpow_minus_one";
Addsimps [realpow_minus_one];
-Goal "(-#1) ^ (n + n) = (#1::real)";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed "realpow_minus_one2";
-Addsimps [realpow_minus_one2];
-
-Goal "(-#1) ^ Suc (n + n) = -(#1::real)";
-by (induct_tac "n" 1);
-by (Auto_tac);
+Goal "(#-1) ^ Suc (#2*n) = -(#1::real)";
+by Auto_tac;
qed "realpow_minus_one_odd";
Addsimps [realpow_minus_one_odd];
-Goal "(-#1) ^ Suc (Suc (n + n)) = (#1::real)";
-by (induct_tac "n" 1);
-by (Auto_tac);
+Goal "(#-1) ^ Suc (Suc (#2*n)) = (#1::real)";
+by Auto_tac;
qed "realpow_minus_one_even";
Addsimps [realpow_minus_one_even];
Goal "(#0::real) < r & r < (#1::real) --> r ^ Suc n < r ^ n";
by (induct_tac "n" 1);
-by (Auto_tac);
+by Auto_tac;
qed_spec_mp "realpow_Suc_less";
Goal "#0 <= r & r < (#1::real) --> r ^ Suc n <= r ^ n";
@@ -237,7 +224,7 @@
Goal "(#0::real) <= #0 ^ n";
by (case_tac "n" 1);
-by (Auto_tac);
+by Auto_tac;
qed "realpow_zero_le";
Addsimps [realpow_zero_le];
@@ -249,12 +236,12 @@
Goal "[| #0 <= r; r < (#1::real) |] ==> r ^ Suc n <= r ^ n";
by (etac (real_le_imp_less_or_eq RS disjE) 1);
by (rtac realpow_Suc_le2 1);
-by (Auto_tac);
+by Auto_tac;
qed "realpow_Suc_le3";
Goal "#0 <= r & r < (#1::real) & n < N --> r ^ N <= r ^ n";
by (induct_tac "N" 1);
-by (Auto_tac);
+by Auto_tac;
by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_zero2));
by (ALLGOALS(dtac (rename_numerals real_mult_le_mono3)));
by (REPEAT(assume_tac 1));
@@ -272,7 +259,7 @@
Goal "[| #0 < r; r < (#1::real) |] ==> r ^ Suc n <= r";
by (dres_inst_tac [("n","1"),("N","Suc n")]
(real_less_imp_le RS realpow_le_le) 1);
-by (Auto_tac);
+by Auto_tac;
qed "realpow_Suc_le_self";
Goal "[| #0 < r; r < (#1::real) |] ==> r ^ Suc n < #1";
@@ -297,7 +284,7 @@
Goal "(#1::real) < r & n < N --> r ^ n <= r ^ N";
by (induct_tac "N" 1);
-by (Auto_tac);
+by Auto_tac;
by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one));
by (ALLGOALS(dtac (rename_numerals real_mult_self_le)));
by (assume_tac 1);
@@ -308,7 +295,7 @@
Goal "(#1::real) <= r & n < N --> r ^ n <= r ^ N";
by (induct_tac "N" 1);
-by (Auto_tac);
+by Auto_tac;
by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one2));
by (ALLGOALS(dtac (rename_numerals real_mult_self_le2)));
by (assume_tac 1);
@@ -330,13 +317,13 @@
Goal "(#1::real) < r ==> r <= r ^ Suc n";
by (dres_inst_tac [("n","1"),("N","Suc n")]
realpow_ge_ge 1);
-by (Auto_tac);
+by Auto_tac;
qed_spec_mp "realpow_Suc_ge_self";
Goal "(#1::real) <= r ==> r <= r ^ Suc n";
by (dres_inst_tac [("n","1"),("N","Suc n")]
realpow_ge_ge2 1);
-by (Auto_tac);
+by Auto_tac;
qed_spec_mp "realpow_Suc_ge_self2";
Goal "[| (#1::real) < r; 0 < n |] ==> r <= r ^ n";