full_rename_numerals -> rename_numerals; tidied
authorpaulson
Wed Jun 14 17:47:18 2000 +0200 (2000-06-14)
changeset 906515f82c9aa331
parent 9064 eacebbcafe57
child 9066 b1e874e38dab
full_rename_numerals -> rename_numerals; tidied
src/HOL/Real/RComplete.ML
src/HOL/Real/RealAbs.ML
     1.1 --- a/src/HOL/Real/RComplete.ML	Wed Jun 14 17:46:10 2000 +0200
     1.2 +++ b/src/HOL/Real/RComplete.ML	Wed Jun 14 17:47:18 2000 +0200
     1.3 @@ -17,16 +17,16 @@
     1.4  Goal "ALL x:P. #0 < x ==> \ 
     1.5  \       ((EX x:P. y < x) = (EX X. real_of_preal X : P & \
     1.6  \                          y < real_of_preal X))";
     1.7 -by (blast_tac (claset() addSDs [bspec,rename_numerals thy
     1.8 -				real_gt_zero_preal_Ex RS iffD1]) 1);
     1.9 +by (blast_tac (claset() addSDs [bspec, 
    1.10 +		    rename_numerals thy real_gt_zero_preal_Ex RS iffD1]) 1);
    1.11  qed "real_sup_lemma1";
    1.12  
    1.13  Goal "[| ALL x:P. #0 < x; EX x. x: P; EX y. ALL x: P. x < y |] \
    1.14  \         ==> (EX X. X: {w. real_of_preal w : P}) & \
    1.15  \             (EX Y. ALL X: {w. real_of_preal w : P}. X < Y)";
    1.16  by (rtac conjI 1);
    1.17 -by (blast_tac (claset() addDs [bspec, rename_numerals thy 
    1.18 -    real_gt_zero_preal_Ex RS iffD1]) 1);
    1.19 +by (blast_tac (claset() addDs [bspec, 
    1.20 +                rename_numerals thy real_gt_zero_preal_Ex RS iffD1]) 1);
    1.21  by Auto_tac;
    1.22  by (dtac bspec 1 THEN assume_tac 1);
    1.23  by (ftac bspec 1  THEN assume_tac 1);
    1.24 @@ -57,7 +57,7 @@
    1.25  by (ftac real_sup_lemma2 1 THEN Auto_tac);
    1.26  by (case_tac "#0 < ya" 1);
    1.27  by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1);
    1.28 -by (dtac (full_rename_numerals thy real_less_all_real2) 2);
    1.29 +by (dtac (rename_numerals thy real_less_all_real2) 2);
    1.30  by Auto_tac;
    1.31  by (rtac (preal_complete RS spec RS iffD1) 1);
    1.32  by Auto_tac;
    1.33 @@ -66,9 +66,10 @@
    1.34  (* second part *)
    1.35  by (rtac (real_sup_lemma1 RS iffD2) 1 THEN assume_tac 1);
    1.36  by (case_tac "#0 < ya" 1);
    1.37 -by (auto_tac (claset() addSDs (map (full_rename_numerals 
    1.38 -    thy) [real_less_all_real2,real_gt_zero_preal_Ex RS iffD1]),
    1.39 -    simpset()));
    1.40 +by (auto_tac (claset() addSDs (map (rename_numerals thy) 
    1.41 +			       [real_less_all_real2,
    1.42 +				real_gt_zero_preal_Ex RS iffD1]),
    1.43 +	      simpset()));
    1.44  by (ftac real_sup_lemma2 2 THEN Auto_tac);
    1.45  by (ftac real_sup_lemma2 1 THEN Auto_tac);
    1.46  by (rtac (preal_complete RS spec RS iffD2 RS bexE) 1);
    1.47 @@ -104,8 +105,8 @@
    1.48  by (auto_tac (claset(), simpset() addsimps 
    1.49      [isLub_def,leastP_def,isUb_def]));
    1.50  by (auto_tac (claset() addSIs [setleI,setgeI] 
    1.51 -     addSDs [(rename_numerals thy real_gt_zero_preal_Ex)
    1.52 -     RS iffD1],simpset()));
    1.53 +	         addSDs [(rename_numerals thy real_gt_zero_preal_Ex) RS iffD1],
    1.54 +	      simpset()));
    1.55  by (forw_inst_tac [("x","y")] bspec 1 THEN assume_tac 1);
    1.56  by (dtac ((rename_numerals thy real_gt_zero_preal_Ex) RS iffD1) 1);
    1.57  by (auto_tac (claset(), simpset() addsimps [real_of_preal_le_iff]));
    1.58 @@ -232,17 +233,15 @@
    1.59  by (res_inst_tac [("x","0")] exI 2);
    1.60  by (auto_tac (claset() addEs [real_less_trans],
    1.61  	      simpset() addsimps [real_of_posnat_one,real_zero_less_one]));
    1.62 -by (forward_tac [((full_rename_numerals thy real_rinv_gt_zero)
    1.63 -     RS reals_Archimedean)] 1);
    1.64 +by (ftac ((rename_numerals thy real_rinv_gt_zero) RS reals_Archimedean) 1);
    1.65  by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1);
    1.66 -by (forw_inst_tac [("y","rinv x")] 
    1.67 -    (full_rename_numerals thy real_mult_less_mono1) 1);
    1.68 +by (forw_inst_tac [("y","rinv x")]
    1.69 +    (rename_numerals thy real_mult_less_mono1) 1);
    1.70  by (auto_tac (claset(),simpset() addsimps [real_not_refl2 RS not_sym]));
    1.71  by (dres_inst_tac [("n1","n"),("y","#1")] 
    1.72       (real_of_posnat_less_zero RS real_mult_less_mono2)  1);
    1.73  by (auto_tac (claset(),
    1.74 -	      simpset() addsimps [rename_numerals thy 
    1.75 -                                  real_of_posnat_less_zero,
    1.76 +	      simpset() addsimps [rename_numerals thy real_of_posnat_less_zero,
    1.77  				  real_not_refl2 RS not_sym,
    1.78  				  real_mult_assoc RS sym]));
    1.79  qed "reals_Archimedean2";
     2.1 --- a/src/HOL/Real/RealAbs.ML	Wed Jun 14 17:46:10 2000 +0200
     2.2 +++ b/src/HOL/Real/RealAbs.ML	Wed Jun 14 17:47:18 2000 +0200
     2.3 @@ -88,15 +88,14 @@
     2.4  
     2.5  Goalw [abs_real_def] "abs (x * y) = abs x * abs (y::real)";
     2.6  by (auto_tac (claset() addSDs [order_antisym],
     2.7 -	      simpset() addsimps [real_0_le_times_iff]));
     2.8 +	      simpset() addsimps [real_0_le_mult_iff]));
     2.9  qed "abs_mult";
    2.10  
    2.11  Goalw [abs_real_def] "x~= (#0::real) ==> abs(rinv(x)) = rinv(abs(x))";
    2.12  by (auto_tac (claset(), 
    2.13                simpset() addsimps [real_le_less] @ 
    2.14 -    (map (full_rename_numerals thy) [real_minus_rinv, real_rinv_gt_zero])));
    2.15 -by (etac (full_rename_numerals thy (real_rinv_less_zero 
    2.16 -    RSN (2,real_less_asym))) 1);
    2.17 +	    (map (rename_numerals thy) [real_minus_rinv, real_rinv_gt_zero])));
    2.18 +by (etac (rename_numerals thy (real_rinv_less_zero RSN (2,real_less_asym))) 1);
    2.19  by (arith_tac 1);
    2.20  qed "abs_rinv";
    2.21  
    2.22 @@ -139,8 +138,8 @@
    2.23  qed "real_mult_0_less";
    2.24  
    2.25  Goal "[| (#0::real)<y; x<r; y*r<t*s |] ==> y*x<t*s";
    2.26 -by (blast_tac (claset() addSIs [full_rename_numerals thy 
    2.27 -    real_mult_less_mono2] addIs  [real_less_trans]) 1);
    2.28 +by (blast_tac (claset() addSIs [rename_numerals thy real_mult_less_mono2] 
    2.29 +                        addIs  [real_less_trans]) 1);
    2.30  qed "real_mult_less_trans";
    2.31  
    2.32  Goal "[| (#0::real)<=y; x<r; y*r<t*s; #0<t*s|] ==> y*x<t*s";
    2.33 @@ -154,7 +153,7 @@
    2.34  by (rtac real_mult_le_less_trans 1);
    2.35  by (rtac abs_ge_zero 1);
    2.36  by (assume_tac 1);
    2.37 -by (rtac (full_rename_numerals thy real_mult_order) 2);
    2.38 +by (rtac (rename_numerals thy real_mult_order) 2);
    2.39  by (auto_tac (claset() addSIs [real_mult_less_mono1,
    2.40      abs_ge_zero] addIs [real_le_less_trans],simpset()));
    2.41  qed "abs_mult_less";
    2.42 @@ -168,8 +167,8 @@
    2.43  by (cut_inst_tac [("x1","y")] (abs_ge_zero RS real_le_imp_less_or_eq) 1);
    2.44  by (EVERY1[etac disjE,rtac real_less_imp_le]);
    2.45  by (dres_inst_tac [("W","#1")]  real_less_sum_gt_zero 1);
    2.46 -by (forw_inst_tac [("y","abs x + (-#1)")] (full_rename_numerals thy
    2.47 -    real_mult_order) 1);
    2.48 +by (forw_inst_tac [("y","abs x + (-#1)")] 
    2.49 +    (rename_numerals thy real_mult_order) 1);
    2.50  by (rtac real_sum_gt_zero_less 2);
    2.51  by (asm_full_simp_tac (simpset() 
    2.52      addsimps [real_add_mult_distrib2,