src/HOL/Real/RComplete.ML
changeset 10919 144ede948e58
parent 10784 27e4d90b35b5
child 11701 3d51fbf81c17
--- a/src/HOL/Real/RComplete.ML	Tue Jan 16 00:40:57 2001 +0100
+++ b/src/HOL/Real/RComplete.ML	Tue Jan 16 12:20:52 2001 +0100
@@ -194,37 +194,37 @@
         Related: Archimedean property of reals
  ----------------------------------------------------------------*)
 
-Goal "#0 < real_of_nat (Suc n)";
-by (res_inst_tac [("y","real_of_nat n")] order_le_less_trans 1); 
+Goal "#0 < real (Suc n)";
+by (res_inst_tac [("y","real n")] order_le_less_trans 1); 
 by (rtac (rename_numerals real_of_nat_ge_zero) 1);
 by (simp_tac (simpset() addsimps [real_of_nat_Suc]) 1); 
 qed "real_of_nat_Suc_gt_zero";
 
-Goal "#0 < x ==> EX n. inverse (real_of_nat(Suc n)) < x";
+Goal "#0 < x ==> EX n. inverse (real(Suc n)) < x";
 by (rtac ccontr 1);
-by (subgoal_tac "ALL n. x * real_of_nat (Suc n) <= #1" 1);
+by (subgoal_tac "ALL n. x * real (Suc n) <= #1" 1);
 by (asm_full_simp_tac
     (simpset() addsimps [linorder_not_less, real_inverse_eq_divide]) 2); 
 by (Clarify_tac 2);
 by (dres_inst_tac [("x","n")] spec 2); 
-by (dres_inst_tac [("k","real_of_nat (Suc n)")] (real_mult_le_mono1) 2); 
+by (dres_inst_tac [("k","real (Suc n)")] (real_mult_le_mono1) 2); 
 by (rtac real_of_nat_ge_zero 2);
 by (asm_full_simp_tac (simpset()  
 	 addsimps [real_of_nat_Suc_gt_zero RS real_not_refl2 RS not_sym, 
                    real_mult_commute]) 2); 
 by (subgoal_tac "isUb (UNIV::real set) \
-\                     {z. EX n. z = x*(real_of_nat (Suc n))} #1" 1);
-by (subgoal_tac "EX X. X : {z. EX n. z = x*(real_of_nat (Suc n))}" 1);
+\                     {z. EX n. z = x*(real (Suc n))} #1" 1);
+by (subgoal_tac "EX X. X : {z. EX n. z = x*(real (Suc n))}" 1);
 by (dtac reals_complete 1);
 by (auto_tac (claset() addIs [isUbI,setleI],simpset()));
-by (subgoal_tac "ALL m. x*(real_of_nat(Suc m)) <= t" 1);
+by (subgoal_tac "ALL m. x*(real(Suc m)) <= t" 1);
 by (asm_full_simp_tac (simpset() addsimps 
                        [real_of_nat_Suc, real_add_mult_distrib2]) 1);
 by (blast_tac (claset() addIs [isLubD2]) 2);
 by (asm_full_simp_tac
     (simpset() addsimps [real_le_diff_eq RS sym, real_diff_def]) 1);
 by (subgoal_tac "isUb (UNIV::real set) \
-\                  {z. EX n. z = x*(real_of_nat (Suc n))} (t + (-x))" 1);
+\                  {z. EX n. z = x*(real (Suc n))} (t + (-x))" 1);
 by (blast_tac (claset() addSIs [isUbI,setleI]) 2);
 by (dres_inst_tac [("y","t+(-x)")] isLub_le_isUb 1);
 by (auto_tac (claset(), 
@@ -233,7 +233,7 @@
 
 (*There must be other proofs, e.g. Suc of the largest integer in the
   cut representing x*)
-Goal "EX n. (x::real) < real_of_nat n";
+Goal "EX n. (x::real) < real (n::nat)";
 by (res_inst_tac [("R1.0","x"),("R2.0","#0")] real_linear_less2 1);
 by (res_inst_tac [("x","0")] exI 1);
 by (res_inst_tac [("x","1")] exI 2);
@@ -244,7 +244,7 @@
 by (forw_inst_tac [("y","inverse x")]
     (rename_numerals real_mult_less_mono1) 1);
 by Auto_tac;  
-by (dres_inst_tac [("y","#1"),("z","real_of_nat (Suc n)")]
+by (dres_inst_tac [("y","#1"),("z","real (Suc n)")]
     (rotate_prems 1 real_mult_less_mono2) 1);
 by (auto_tac (claset(),
 	      simpset() addsimps [real_of_nat_Suc_gt_zero,