--- a/src/HOL/Real/RComplete.ML Thu Nov 01 21:12:13 2001 +0100
+++ b/src/HOL/Real/RComplete.ML Fri Nov 02 17:55:24 2001 +0100
@@ -6,8 +6,6 @@
Completeness theorems for positive reals and reals.
*)
-claset_ref() := claset() delWrapper "bspec";
-
Goal "x/2 + x/2 = (x::real)";
by (Simp_tac 1);
qed "real_sum_of_halves";
@@ -18,29 +16,25 @@
previously in Real.ML.
---------------------------------------------------------*)
(*a few lemmas*)
-Goal "ALL x:P. Numeral0 < x ==> \
+Goal "ALL x:P. 0 < x ==> \
\ ((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 real_gt_zero_preal_Ex RS iffD1]) 1);
+ real_gt_zero_preal_Ex RS iffD1]) 1);
qed "real_sup_lemma1";
-Goal "[| ALL x:P. Numeral0 < x; EX x. x: P; EX y. ALL x: P. x < y |] \
+Goal "[| ALL x:P. 0 < x; a: P; ALL x: P. x < y |] \
\ ==> (EX X. X: {w. real_of_preal w : P}) & \
\ (EX Y. ALL X: {w. real_of_preal w : P}. X < Y)";
by (rtac conjI 1);
by (blast_tac (claset() addDs [bspec,
- rename_numerals real_gt_zero_preal_Ex RS iffD1]) 1);
+ 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 order_less_trans 1 THEN assume_tac 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;
-by (dres_inst_tac [("x","real_of_preal X")] bspec 1 THEN assume_tac 1);
-by (etac real_of_preal_lessD 1);
+by (dtac order_less_trans 1 THEN assume_tac 1);
+by (dtac (real_gt_zero_preal_Ex RS iffD1) 1);
+by (Force_tac 1);
qed "real_sup_lemma2";
(*-------------------------------------------------------------
@@ -49,33 +43,33 @@
(**
Supremum property for the set of positive reals
- FIXME: long proof - should be improved - need
- only have one case split
+ FIXME: long proof - should be improved
**)
-Goal "[| ALL x:P. (Numeral0::real) < x; EX x. x: P; EX y. ALL x: P. x < y |] \
-\ ==> (EX S. ALL y. (EX x: P. y < x) = (y < S))";
+(*Let P be a non-empty set of positive reals, with an upper bound y.
+ Then P has a least upper bound (written S).*)
+Goal "[| ALL x:P. (0::real) < x; EX x. x: P; EX y. ALL x: P. x<y |] \
+\ ==> (EX S. ALL y. (EX x: P. y < x) = (y < S))";
by (res_inst_tac
[("x","real_of_preal (psup({w. real_of_preal w : P}))")] exI 1);
-by Auto_tac;
-by (ftac real_sup_lemma2 1 THEN Auto_tac);
-by (case_tac "Numeral0 < ya" 1);
-by (dtac ((rename_numerals real_gt_zero_preal_Ex) RS iffD1) 1);
-by (dtac (rename_numerals real_less_all_real2) 2);
+by (Clarify_tac 1);
+by (case_tac "0 < ya" 1);
+by Auto_tac;
+by (ftac real_sup_lemma2 1 THEN REPEAT (assume_tac 1));
+by (dtac (real_gt_zero_preal_Ex RS iffD1) 1);
+by (dtac (real_less_all_real2) 3);
by Auto_tac;
by (rtac (preal_complete RS spec RS iffD1) 1);
by Auto_tac;
by (ftac real_gt_preal_preal_Ex 1);
-by Auto_tac;
+by (Force_tac 1);
(* second part *)
by (rtac (real_sup_lemma1 RS iffD2) 1 THEN assume_tac 1);
-by (case_tac "Numeral0 < ya" 1);
-by (auto_tac (claset() addSDs (map rename_numerals
- [real_less_all_real2,
- real_gt_zero_preal_Ex RS iffD1]),
+by (auto_tac (claset() addSDs [real_less_all_real2,
+ real_gt_zero_preal_Ex RS iffD1],
simpset()));
-by (ftac real_sup_lemma2 2 THEN Auto_tac);
-by (ftac real_sup_lemma2 1 THEN Auto_tac);
+by (ftac real_sup_lemma2 2 THEN REPEAT (assume_tac 1));
+by (ftac real_sup_lemma2 1 THEN REPEAT (assume_tac 1));
by (rtac (preal_complete RS spec RS iffD2 RS bexE) 1);
by (Blast_tac 3);
by (ALLGOALS(Blast_tac));
@@ -100,7 +94,7 @@
Completeness theorem for the positive reals(again)
----------------------------------------------------------------*)
-Goal "[| ALL x: S. Numeral0 < x; \
+Goal "[| ALL x: S. 0 < x; \
\ EX x. x: S; \
\ EX u. isUb (UNIV::real set) S u \
\ |] ==> EX t. isLub (UNIV::real set) S t";
@@ -109,10 +103,10 @@
by (auto_tac (claset(), simpset() addsimps
[isLub_def,leastP_def,isUb_def]));
by (auto_tac (claset() addSIs [setleI,setgeI]
- addSDs [(rename_numerals real_gt_zero_preal_Ex) RS iffD1],
+ addSDs [(real_gt_zero_preal_Ex) RS iffD1],
simpset()));
by (forw_inst_tac [("x","y")] bspec 1 THEN assume_tac 1);
-by (dtac ((rename_numerals real_gt_zero_preal_Ex) RS iffD1) 1);
+by (dtac ((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);
@@ -122,7 +116,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 real_gt_zero_preal_Ex) RS iffD1) 1);
+by (dtac ((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]
@@ -133,16 +127,17 @@
(*-------------------------------
Lemmas
-------------------------------*)
-Goal "ALL y : {z. EX x: P. z = x + (-xa) + Numeral1} Int {x. Numeral0 < x}. Numeral0 < y";
+Goal "ALL y : {z. EX x: P. z = x + (-xa) + 1} Int {x. 0 < x}. 0 < y";
by Auto_tac;
qed "real_sup_lemma3";
Goal "(xa <= S + X + (-Z)) = (xa + (-X) + Z <= (S::real))";
-by (Auto_tac);
+by Auto_tac;
qed "lemma_le_swap2";
-Goal "[| (x::real) + (-X) + Numeral1 <= S; xa <= x |] ==> xa <= S + X + (-Numeral1)";
-by (Auto_tac);
+Goal "[| (x::real) + (-X) + 1 <= S; xa <= x |] ==> xa <= S + X + (- 1)";
+by (arith_tac 1);
+by Auto_tac;
qed "lemma_real_complete2b";
(*----------------------------------------------------------
@@ -151,19 +146,19 @@
Goal "[| EX X. X: S; EX Y. isUb (UNIV::real set) S Y |] \
\ ==> EX t. isLub (UNIV :: real set) S t";
by (Step_tac 1);
-by (subgoal_tac "EX u. u: {z. EX x: S. z = x + (-X) + Numeral1} \
-\ Int {x. Numeral0 < x}" 1);
-by (subgoal_tac "isUb (UNIV::real set) ({z. EX x: S. z = x + (-X) + Numeral1} \
-\ Int {x. Numeral0 < x}) (Y + (-X) + Numeral1)" 1);
+by (subgoal_tac "EX u. u: {z. EX x: S. z = x + (-X) + 1} \
+\ Int {x. 0 < x}" 1);
+by (subgoal_tac "isUb (UNIV::real set) ({z. EX x: S. z = x + (-X) + 1} \
+\ Int {x. 0 < x}) (Y + (-X) + 1)" 1);
by (cut_inst_tac [("P","S"),("xa","X")] real_sup_lemma3 1);
by (EVERY1[forward_tac [exI RSN (3,posreals_complete)], Blast_tac, Blast_tac,
Step_tac]);
-by (res_inst_tac [("x","t + X + (-Numeral1)")] exI 1);
+by (res_inst_tac [("x","t + X + (- 1)")] exI 1);
by (rtac isLubI2 1);
by (rtac setgeI 2 THEN Step_tac 2);
-by (subgoal_tac "isUb (UNIV:: real set) ({z. EX x: S. z = x + (-X) + Numeral1} \
-\ Int {x. Numeral0 < x}) (y + (-X) + Numeral1)" 2);
-by (dres_inst_tac [("y","(y + (- X) + Numeral1)")] isLub_le_isUb 2
+by (subgoal_tac "isUb (UNIV:: real set) ({z. EX x: S. z = x + (-X) + 1} \
+\ Int {x. 0 < x}) (y + (-X) + 1)" 2);
+by (dres_inst_tac [("y","(y + (- X) + 1)")] isLub_le_isUb 2
THEN assume_tac 2);
by (full_simp_tac
(simpset() addsimps [real_diff_def, real_diff_le_eq RS sym] @
@@ -194,15 +189,15 @@
Related: Archimedean property of reals
----------------------------------------------------------------*)
-Goal "Numeral0 < real (Suc n)";
+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 (rtac (real_of_nat_ge_zero) 1);
by (simp_tac (simpset() addsimps [real_of_nat_Suc]) 1);
qed "real_of_nat_Suc_gt_zero";
-Goal "Numeral0 < x ==> EX n. inverse (real(Suc n)) < x";
+Goal "0 < x ==> EX n. inverse (real(Suc n)) < x";
by (rtac ccontr 1);
-by (subgoal_tac "ALL n. x * real (Suc n) <= Numeral1" 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);
@@ -213,7 +208,7 @@
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 (Suc n))} Numeral1" 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()));
@@ -234,17 +229,16 @@
(*There must be other proofs, e.g. Suc of the largest integer in the
cut representing x*)
Goal "EX n. (x::real) < real (n::nat)";
-by (res_inst_tac [("R1.0","x"),("R2.0","Numeral0")] real_linear_less2 1);
+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);
by (auto_tac (claset() addEs [order_less_trans],
simpset() addsimps [real_of_nat_one]));
-by (ftac ((rename_numerals real_inverse_gt_zero) RS reals_Archimedean) 1);
+by (ftac (real_inverse_gt_0 RS reals_Archimedean) 1);
by (Step_tac 1 THEN res_inst_tac [("x","Suc n")] exI 1);
-by (forw_inst_tac [("y","inverse x")]
- (rename_numerals real_mult_less_mono1) 1);
+by (forw_inst_tac [("y","inverse x")] real_mult_less_mono1 1);
by Auto_tac;
-by (dres_inst_tac [("y","Numeral1"),("z","real (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,