--- a/src/HOL/Real/RealPow.ML Mon Jul 24 23:58:49 2000 +0200
+++ b/src/HOL/Real/RealPow.ML Mon Jul 24 23:59:08 2000 +0200
@@ -24,7 +24,7 @@
by (induct_tac "n" 1);
by (Auto_tac);
by (forw_inst_tac [("n","n")] realpow_not_zero 1);
-by (auto_tac (claset() addDs [rename_numerals thy real_rinv_distrib],
+by (auto_tac (claset() addDs [rename_numerals real_rinv_distrib],
simpset()));
qed_spec_mp "realpow_rinv";
@@ -51,19 +51,19 @@
Goal "(#0::real) < r --> #0 <= r ^ n";
by (induct_tac "n" 1);
by (auto_tac (claset() addDs [real_less_imp_le]
- addIs [rename_numerals thy real_le_mult_order],
+ addIs [rename_numerals real_le_mult_order],
simpset()));
qed_spec_mp "realpow_ge_zero";
Goal "(#0::real) < r --> #0 < r ^ n";
by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [rename_numerals thy real_mult_order],
+by (auto_tac (claset() addIs [rename_numerals real_mult_order],
simpset() addsimps [real_zero_less_one]));
qed_spec_mp "realpow_gt_zero";
Goal "(#0::real) <= r --> #0 <= r ^ n";
by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [rename_numerals thy real_le_mult_order],
+by (auto_tac (claset() addIs [rename_numerals real_le_mult_order],
simpset()));
qed_spec_mp "realpow_ge_zero2";
@@ -83,7 +83,7 @@
Goal "(#0::real) < x & x < y & 0 < n --> x ^ n < y ^ n";
by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [rename_numerals thy real_mult_less_mono, gr0I]
+by (auto_tac (claset() addIs [rename_numerals real_mult_less_mono, gr0I]
addDs [realpow_gt_zero],
simpset()));
qed_spec_mp "realpow_less";
@@ -113,29 +113,29 @@
qed "realpow_mult";
Goal "(#0::real) <= r ^ 2";
-by (simp_tac (simpset() addsimps [rename_numerals thy real_le_square]) 1);
+by (simp_tac (simpset() addsimps [rename_numerals real_le_square]) 1);
qed "realpow_two_le";
Addsimps [realpow_two_le];
Goal "abs((x::real) ^ 2) = x ^ 2";
by (simp_tac (simpset() addsimps [abs_eqI1,
- rename_numerals thy real_le_square]) 1);
+ rename_numerals real_le_square]) 1);
qed "abs_realpow_two";
Addsimps [abs_realpow_two];
Goal "abs(x::real) ^ 2 = x ^ 2";
by (simp_tac (simpset() addsimps
- [realpow_abs,abs_eqI1] delsimps [realpow_Suc]) 1);
+ [realpow_abs,abs_eqI1] delsimps [thm "realpow_Suc"]) 1);
qed "realpow_two_abs";
Addsimps [realpow_two_abs];
Goal "(#1::real) < r ==> #1 < r ^ 2";
by Auto_tac;
-by (cut_facts_tac [rename_numerals thy real_zero_less_one] 1);
+by (cut_facts_tac [rename_numerals real_zero_less_one] 1);
by (forw_inst_tac [("R1.0","#0")] real_less_trans 1);
by (assume_tac 1);
by (dres_inst_tac [("z","r"),("x","#1")]
- (rename_numerals thy real_mult_less_mono1) 1);
+ (rename_numerals real_mult_less_mono1) 1);
by (auto_tac (claset() addIs [real_less_trans],simpset()));
qed "realpow_two_gt_one";
@@ -143,7 +143,7 @@
by (induct_tac "n" 1);
by (auto_tac (claset() addSDs [real_le_imp_less_or_eq],
simpset()));
-by (dtac (rename_numerals thy (real_zero_less_one RS real_mult_less_mono)) 1);
+by (dtac (rename_numerals (real_zero_less_one RS real_mult_less_mono)) 1);
by (dtac sym 4);
by (auto_tac (claset() addSIs [real_less_imp_le],
simpset() addsimps [real_zero_less_one]));
@@ -153,9 +153,9 @@
by (forw_inst_tac [("n","n")] realpow_ge_one 1);
by (dtac real_le_imp_less_or_eq 1 THEN Step_tac 1);
by (dtac sym 2);
-by (ftac (rename_numerals thy (real_zero_less_one RS real_less_trans)) 1);
+by (ftac (rename_numerals (real_zero_less_one RS real_less_trans)) 1);
by (dres_inst_tac [("y","r ^ n")]
- (rename_numerals thy real_mult_less_mono2) 1);
+ (rename_numerals real_mult_less_mono2) 1);
by (assume_tac 1);
by (auto_tac (claset() addDs [real_less_trans],
simpset()));
@@ -171,7 +171,7 @@
by (forw_inst_tac [("n1","n")]
((real_not_refl2 RS not_sym) RS realpow_not_zero RS not_sym) 1);
by (auto_tac (claset() addSDs [real_le_imp_less_or_eq]
- addIs [rename_numerals thy real_mult_order],
+ addIs [rename_numerals real_mult_order],
simpset()));
qed "realpow_Suc_gt_zero";
@@ -254,7 +254,7 @@
by (induct_tac "N" 1);
by (Auto_tac);
by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_zero2));
-by (ALLGOALS(dtac (rename_numerals thy real_mult_le_mono3)));
+by (ALLGOALS(dtac (rename_numerals real_mult_le_mono3)));
by (REPEAT(assume_tac 1));
by (REPEAT(assume_tac 3));
by (auto_tac (claset(),simpset() addsimps
@@ -297,7 +297,7 @@
by (induct_tac "N" 1);
by (Auto_tac);
by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one));
-by (ALLGOALS(dtac (rename_numerals thy real_mult_self_le)));
+by (ALLGOALS(dtac (rename_numerals real_mult_self_le)));
by (assume_tac 1);
by (assume_tac 2);
by (auto_tac (claset() addIs [real_le_trans],
@@ -308,7 +308,7 @@
by (induct_tac "N" 1);
by (Auto_tac);
by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one2));
-by (ALLGOALS(dtac (rename_numerals thy real_mult_self_le2)));
+by (ALLGOALS(dtac (rename_numerals real_mult_self_le2)));
by (assume_tac 1);
by (assume_tac 2);
by (auto_tac (claset() addIs [real_le_trans],
@@ -373,18 +373,18 @@
@ real_mult_ac) 1);
qed "realpow_two_add_minus";
-goalw RealPow.thy [real_diff_def]
+Goalw [real_diff_def]
"(x::real) ^ 2 - y ^ 2 = (x - y) * (x + y)";
by (simp_tac (simpset() addsimps [realpow_two_add_minus]
- delsimps [realpow_Suc]) 1);
+ delsimps [thm "realpow_Suc"]) 1);
qed "realpow_two_diff";
-goalw RealPow.thy [real_diff_def]
+Goalw [real_diff_def]
"((x::real) ^ 2 = y ^ 2) = (x = y | x = -y)";
-by (auto_tac (claset(),simpset() delsimps [realpow_Suc]));
-by (dtac (rename_numerals thy (real_eq_minus_iff RS iffD1 RS sym)) 1);
-by (auto_tac (claset() addDs [rename_numerals thy real_add_minus_eq_minus],
- simpset() addsimps [realpow_two_add_minus] delsimps [realpow_Suc]));
+by (auto_tac (claset(),simpset() delsimps [thm "realpow_Suc"]));
+by (dtac (rename_numerals (real_eq_minus_iff RS iffD1 RS sym)) 1);
+by (auto_tac (claset() addDs [rename_numerals real_add_minus_eq_minus],
+ simpset() addsimps [realpow_two_add_minus] delsimps [thm "realpow_Suc"]));
qed "realpow_two_disj";
(* used in Transc *)