# HG changeset patch
# User wenzelm
# Date 964475948 -7200
# Node ID c8eb573114ded582000edea32cc461fada8254fb
# Parent  a9c60e65510721ae0140fa717fa5cbc864cf7056
rename_numerals: use implicit theory context;

diff -r a9c60e655107 -r c8eb573114de src/HOL/Real/RComplete.ML
--- a/src/HOL/Real/RComplete.ML	Mon Jul 24 23:58:49 2000 +0200
+++ b/src/HOL/Real/RComplete.ML	Mon Jul 24 23:59:08 2000 +0200
@@ -1,9 +1,9 @@
-(*  Title       : RComplete.thy
+(*  Title       : HOL/Real/RComplete.ML
     ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
-    Description : Completeness theorems for positive
-                  reals and reals 
+
+Completeness theorems for positive reals and reals.
 *) 
 
 claset_ref() := claset() delWrapper "bspec";
@@ -18,7 +18,7 @@
 \       ((EX x:P. y < x) = (EX X. real_of_preal X : P & \
 \                          y < real_of_preal X))";
 by (blast_tac (claset() addSDs [bspec, 
-		    rename_numerals thy real_gt_zero_preal_Ex RS iffD1]) 1);
+		    rename_numerals real_gt_zero_preal_Ex RS iffD1]) 1);
 qed "real_sup_lemma1";
 
 Goal "[| ALL x:P. #0 < x; EX x. x: P; EX y. ALL x: P. x < y |] \
@@ -26,12 +26,12 @@
 \             (EX Y. ALL X: {w. real_of_preal w : P}. X < Y)";
 by (rtac conjI 1);
 by (blast_tac (claset() addDs [bspec, 
-                rename_numerals thy real_gt_zero_preal_Ex RS iffD1]) 1);
+                rename_numerals real_gt_zero_preal_Ex RS iffD1]) 1);
 by Auto_tac;
 by (dtac bspec 1 THEN assume_tac 1);
 by (ftac bspec 1  THEN assume_tac 1);
 by (dtac real_less_trans 1 THEN assume_tac 1);
-by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1
+by (dtac ((rename_numerals real_gt_zero_preal_Ex) RS iffD1) 1
     THEN etac exE 1);    
 by (res_inst_tac [("x","ya")] exI 1);
 by Auto_tac;
@@ -56,8 +56,8 @@
 by Auto_tac;
 by (ftac real_sup_lemma2 1 THEN Auto_tac);
 by (case_tac "#0 < ya" 1);
-by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1);
-by (dtac (rename_numerals thy real_less_all_real2) 2);
+by (dtac ((rename_numerals real_gt_zero_preal_Ex) RS iffD1) 1);
+by (dtac (rename_numerals real_less_all_real2) 2);
 by Auto_tac;
 by (rtac (preal_complete RS spec RS iffD1) 1);
 by Auto_tac;
@@ -66,7 +66,7 @@
 (* second part *)
 by (rtac (real_sup_lemma1 RS iffD2) 1 THEN assume_tac 1);
 by (case_tac "#0 < ya" 1);
-by (auto_tac (claset() addSDs (map (rename_numerals thy) 
+by (auto_tac (claset() addSDs (map rename_numerals
 			       [real_less_all_real2,
 				real_gt_zero_preal_Ex RS iffD1]),
 	      simpset()));
@@ -105,10 +105,10 @@
 by (auto_tac (claset(), simpset() addsimps 
     [isLub_def,leastP_def,isUb_def]));
 by (auto_tac (claset() addSIs [setleI,setgeI] 
-	         addSDs [(rename_numerals thy real_gt_zero_preal_Ex) RS iffD1],
+	         addSDs [(rename_numerals real_gt_zero_preal_Ex) RS iffD1],
 	      simpset()));
 by (forw_inst_tac [("x","y")] bspec 1 THEN assume_tac 1);
-by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1);
+by (dtac ((rename_numerals real_gt_zero_preal_Ex) RS iffD1) 1);
 by (auto_tac (claset(), simpset() addsimps [real_of_preal_le_iff]));
 by (rtac preal_psup_leI2a 1);
 by (forw_inst_tac [("y","real_of_preal ya")] setleD 1 THEN assume_tac 1);
@@ -118,7 +118,7 @@
 by (blast_tac (claset() addSDs [setleD] addIs [real_of_preal_le_iff RS iffD1]) 1);
 by (forw_inst_tac [("x","x")] bspec 1 THEN assume_tac 1);
 by (ftac isUbD2 1);
-by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1);
+by (dtac ((rename_numerals real_gt_zero_preal_Ex) RS iffD1) 1);
 by (auto_tac (claset() addSDs [isUbD, real_ge_preal_preal_Ex],
 	      simpset() addsimps [real_of_preal_le_iff]));
 by (blast_tac (claset() addSDs [setleD] addSIs [psup_le_ub1] 
@@ -233,15 +233,15 @@
 by (res_inst_tac [("x","0")] exI 2);
 by (auto_tac (claset() addEs [real_less_trans],
 	      simpset() addsimps [real_of_posnat_one,real_zero_less_one]));
-by (ftac ((rename_numerals thy real_rinv_gt_zero) RS reals_Archimedean) 1);
+by (ftac ((rename_numerals real_rinv_gt_zero) RS reals_Archimedean) 1);
 by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1);
 by (forw_inst_tac [("y","rinv x")]
-    (rename_numerals thy real_mult_less_mono1) 1);
+    (rename_numerals real_mult_less_mono1) 1);
 by (auto_tac (claset(),simpset() addsimps [real_not_refl2 RS not_sym]));
 by (dres_inst_tac [("n1","n"),("y","#1")] 
      (real_of_posnat_less_zero RS real_mult_less_mono2)  1);
 by (auto_tac (claset(),
-	      simpset() addsimps [rename_numerals thy real_of_posnat_less_zero,
+	      simpset() addsimps [rename_numerals real_of_posnat_less_zero,
 				  real_not_refl2 RS not_sym,
 				  real_mult_assoc RS sym]));
 qed "reals_Archimedean2";
diff -r a9c60e655107 -r c8eb573114de src/HOL/Real/RealPow.ML
--- 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 *)