src/HOL/Real/RComplete.ML
changeset 5588 a3ab526bb891
parent 5521 7970832271cc
child 7077 60b098bb8b8a
     1.1 --- a/src/HOL/Real/RComplete.ML	Tue Sep 29 18:13:05 1998 +0200
     1.2 +++ b/src/HOL/Real/RComplete.ML	Thu Oct 01 18:18:01 1998 +0200
     1.3 @@ -31,12 +31,12 @@
     1.4  \                 EX u. isUb (UNIV::real set) S u \
     1.5  \              |] ==> EX t. isLub (UNIV::real set) S t";
     1.6  by (res_inst_tac [("x","%#psup({w. %#w : S})")] exI 1);
     1.7 -by (auto_tac (claset(),simpset() addsimps [isLub_def,leastP_def,isUb_def]));
     1.8 +by (auto_tac (claset(), simpset() addsimps [isLub_def,leastP_def,isUb_def]));
     1.9  by (auto_tac (claset() addSIs [setleI,setgeI] 
    1.10 -    addSDs [real_gt_zero_preal_Ex RS iffD1],simpset()));
    1.11 +	               addSDs [real_gt_zero_preal_Ex RS iffD1],simpset()));
    1.12  by (forw_inst_tac [("x","y")] bspec 1 THEN assume_tac 1);
    1.13  by (dtac (real_gt_zero_preal_Ex RS iffD1) 1);
    1.14 -by (auto_tac (claset(),simpset() addsimps [real_preal_le_iff]));
    1.15 +by (auto_tac (claset(), simpset() addsimps [real_preal_le_iff]));
    1.16  by (rtac preal_psup_leI2a 1);
    1.17  by (forw_inst_tac [("y","%#ya")] setleD 1 THEN assume_tac 1);
    1.18  by (forward_tac  [real_ge_preal_preal_Ex] 1);
    1.19 @@ -46,73 +46,48 @@
    1.20  by (forw_inst_tac [("x","x")] bspec 1 THEN assume_tac 1);
    1.21  by (forward_tac [isUbD2] 1);
    1.22  by (dtac (real_gt_zero_preal_Ex RS iffD1) 1);
    1.23 -by (auto_tac (claset() addSDs [isUbD,
    1.24 -    real_ge_preal_preal_Ex],simpset() addsimps [real_preal_le_iff]));
    1.25 -by (blast_tac (claset() addSDs [setleD] addSIs 
    1.26 -    [psup_le_ub1] addIs [real_preal_le_iff RS iffD1]) 1);
    1.27 +by (auto_tac (claset() addSDs [isUbD, real_ge_preal_preal_Ex],
    1.28 +	      simpset() addsimps [real_preal_le_iff]));
    1.29 +by (blast_tac (claset() addSDs [setleD] addSIs [psup_le_ub1] 
    1.30 +	                addIs [real_preal_le_iff RS iffD1]) 1);
    1.31  qed "posreals_complete";
    1.32  
    1.33  
    1.34  (*-------------------------------
    1.35      Lemmas
    1.36   -------------------------------*)
    1.37 -Goal "! y : {z. ? x: P. z = x + %~xa + 1r} Int {x. 0r < x}. 0r < y";
    1.38 +Goal "! y : {z. ? x: P. z = x + -xa + 1r} Int {x. 0r < x}. 0r < y";
    1.39  by Auto_tac;
    1.40  qed "real_sup_lemma3";
    1.41   
    1.42 -(* lemmas re-arranging the terms *)
    1.43 -Goal "(S <= Y + %~X + Z) = (S + X + %~Z <= Y)";
    1.44 -by (Step_tac 1);
    1.45 -by (dres_inst_tac [("x","%~Z")] real_add_le_mono1 1);
    1.46 -by (dres_inst_tac [("x","Z")] real_add_le_mono1 2);
    1.47 -by (auto_tac (claset(),simpset() addsimps [real_add_assoc,
    1.48 -    real_add_minus,real_add_zero_right,real_add_minus_left]));
    1.49 -by (dres_inst_tac [("x","X")] real_add_le_mono1 1);
    1.50 -by (dres_inst_tac [("x","%~X")] real_add_le_mono1 2);
    1.51 -by (auto_tac (claset(),simpset() addsimps [real_add_assoc,
    1.52 -    real_add_minus,real_add_zero_right,real_add_minus_left]));
    1.53 -by (auto_tac (claset(),simpset() addsimps [real_add_commute]));
    1.54 -qed "lemma_le_swap";
    1.55 -
    1.56 -Goal "(xa <= S + X + %~Z) = (xa + %~X + Z <= S)";
    1.57 -by (Step_tac 1);
    1.58 -by (dres_inst_tac [("x","Z")] real_add_le_mono1 1);
    1.59 -by (dres_inst_tac [("x","%~Z")] real_add_le_mono1 2);
    1.60 -by (auto_tac (claset(),simpset() addsimps [real_add_assoc,
    1.61 -    real_add_minus,real_add_zero_right,real_add_minus_left]));
    1.62 -by (dres_inst_tac [("x","%~X")] real_add_le_mono1 1);
    1.63 -by (dres_inst_tac [("x","X")] real_add_le_mono1 2);
    1.64 -by (auto_tac (claset(),simpset() addsimps [real_add_assoc,
    1.65 -    real_add_minus,real_add_zero_right,real_add_minus_left]));
    1.66 -by (auto_tac (claset(),simpset() addsimps [real_add_commute]));
    1.67 +Goal "(xa <= S + X + -Z) = (xa + -X + Z <= (S::real))";
    1.68 +by (simp_tac (simpset() addsimps [real_diff_def, real_diff_le_eq RS sym] @
    1.69 +	                         real_add_ac) 1);
    1.70  qed "lemma_le_swap2";
    1.71  
    1.72 -Goal "[| 0r < x + %~X + 1r; x < xa |] ==> 0r < xa + %~X + 1r";
    1.73 +Goal "[| 0r < x + -X + 1r; x < xa |] ==> 0r < xa + -X + 1r";
    1.74  by (dtac real_add_less_mono 1);
    1.75  by (assume_tac 1);
    1.76 -by (dres_inst_tac [("C","%~x"),("A","0r + x")] real_add_less_mono2 1);
    1.77 +by (dres_inst_tac [("C","-x"),("A","0r + x")] real_add_less_mono2 1);
    1.78  by (asm_full_simp_tac (simpset() addsimps [real_add_zero_right,
    1.79      real_add_assoc RS sym,real_add_minus_left,real_add_zero_left]) 1);
    1.80  by (asm_full_simp_tac (simpset() addsimps real_add_ac) 1);
    1.81  qed "lemma_real_complete1";
    1.82  
    1.83 -Goal "!!x. [| x + %~X + 1r <= S; xa < x |] ==> xa + %~X + 1r <= S";
    1.84 +Goal "!!x. [| x + -X + 1r <= S; xa < x |] ==> xa + -X + 1r <= S";
    1.85  by (dtac real_less_imp_le 1);
    1.86  by (dtac real_add_le_mono 1);
    1.87  by (assume_tac 1);
    1.88  by (asm_full_simp_tac (simpset() addsimps real_add_ac) 1);
    1.89 -by (dres_inst_tac [("x","%~x"),("q2.0","x + S")] real_add_left_le_mono1 1);
    1.90 -by (asm_full_simp_tac (simpset() addsimps [real_add_assoc RS sym,
    1.91 -        real_add_minus_left,real_add_zero_left]) 1);
    1.92  qed "lemma_real_complete2";
    1.93  
    1.94 -Goal "[| x + %~X + 1r <= S; xa < x |] ==> xa <= S + X + %~1r"; (**)
    1.95 +Goal "[| x + -X + 1r <= S; xa < x |] ==> xa <= S + X + -1r"; (**)
    1.96  by (rtac (lemma_le_swap2 RS iffD2) 1);
    1.97  by (etac lemma_real_complete2 1);
    1.98  by (assume_tac 1);
    1.99  qed "lemma_real_complete2a";
   1.100  
   1.101 -Goal "[| x + %~X + 1r <= S; xa <= x |] ==> xa <= S + X + %~1r";
   1.102 +Goal "[| x + -X + 1r <= S; xa <= x |] ==> xa <= S + X + -1r";
   1.103  by (rotate_tac 1 1);
   1.104  by (etac (real_le_imp_less_or_eq RS disjE) 1);
   1.105  by (blast_tac (claset() addIs [lemma_real_complete2a]) 1);
   1.106 @@ -126,20 +101,22 @@
   1.107  \                             EX Y. isUb (UNIV::real set) S Y \
   1.108  \                          |] ==> EX t. isLub (UNIV :: real set) S t";
   1.109  by (Step_tac 1);
   1.110 -by (subgoal_tac "? u. u: {z. ? x: S. z = x + %~X + 1r} \
   1.111 +by (subgoal_tac "? u. u: {z. ? x: S. z = x + -X + 1r} \
   1.112  \                Int {x. 0r < x}" 1);
   1.113 -by (subgoal_tac "isUb (UNIV::real set) ({z. ? x: S. z = x + %~X + 1r} \
   1.114 -\                Int {x. 0r < x})  (Y + %~X + 1r)" 1); 
   1.115 +by (subgoal_tac "isUb (UNIV::real set) ({z. ? x: S. z = x + -X + 1r} \
   1.116 +\                Int {x. 0r < x})  (Y + -X + 1r)" 1); 
   1.117  by (cut_inst_tac [("P","S"),("xa","X")] real_sup_lemma3 1);
   1.118  by (EVERY1[forward_tac [exI RSN (3,posreals_complete)], Blast_tac, Blast_tac, Step_tac]);
   1.119 -by (res_inst_tac [("x","t + X + %~1r")] exI 1);
   1.120 +by (res_inst_tac [("x","t + X + -1r")] exI 1);
   1.121  by (rtac isLubI2 1);
   1.122  by (rtac setgeI 2 THEN Step_tac 2);
   1.123 -by (subgoal_tac "isUb (UNIV:: real set) ({z. ? x: S. z = x + %~X + 1r} \
   1.124 -\                Int {x. 0r < x})  (y + %~X + 1r)" 2); 
   1.125 -by (dres_inst_tac [("y","(y + %~ X + 1r)")] isLub_le_isUb 2 
   1.126 +by (subgoal_tac "isUb (UNIV:: real set) ({z. ? x: S. z = x + -X + 1r} \
   1.127 +\                Int {x. 0r < x})  (y + -X + 1r)" 2); 
   1.128 +by (dres_inst_tac [("y","(y + - X + 1r)")] isLub_le_isUb 2 
   1.129        THEN assume_tac 2);
   1.130 -by (etac (lemma_le_swap RS subst) 2);
   1.131 +by (full_simp_tac
   1.132 +    (simpset() addsimps [real_diff_def, real_diff_le_eq RS sym] @
   1.133 +                        real_add_ac) 2);
   1.134  by (rtac (setleI RS isUbI) 1);
   1.135  by (Step_tac 1);
   1.136  by (res_inst_tac [("R1.0","x"),("R2.0","y")] real_linear_less2 1);
   1.137 @@ -154,27 +131,20 @@
   1.138  by (rtac lemma_real_complete2b 1);
   1.139  by (etac real_less_imp_le 2);
   1.140  by (blast_tac (claset() addSIs [isLubD2]) 1 THEN Step_tac 1);
   1.141 -by (blast_tac (claset() addDs [isUbD] addSIs [(setleI RS isUbI)]
   1.142 -    addIs [real_add_le_mono1,real_add_assoc RS ssubst]) 1);
   1.143 -by (blast_tac (claset() addDs [isUbD] addSIs [(setleI RS isUbI)]
   1.144 -    addIs [real_add_le_mono1,real_add_assoc RS ssubst]) 1);
   1.145 -by (auto_tac (claset(),simpset() addsimps [real_add_assoc RS sym,
   1.146 -     real_add_minus,real_add_zero_left,real_zero_less_one]));
   1.147 +by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
   1.148 +by (blast_tac (claset() addDs [isUbD] addSIs [setleI RS isUbI]
   1.149 +                        addIs [real_add_le_mono1]) 1);
   1.150 +by (blast_tac (claset() addDs [isUbD] addSIs [setleI RS isUbI]
   1.151 +                        addIs [real_add_le_mono1]) 1);
   1.152 +by (auto_tac (claset(),
   1.153 +	      simpset() addsimps [real_add_assoc RS sym,
   1.154 +				  real_zero_less_one]));
   1.155  qed "reals_complete";
   1.156  
   1.157  (*----------------------------------------------------------------
   1.158          Related property: Archimedean property of reals
   1.159   ----------------------------------------------------------------*)
   1.160  
   1.161 -Goal "(ALL m. x*%%#m + x <= t) = (ALL m. x*%%#m <= t + %~x)";
   1.162 -by Auto_tac;
   1.163 -by (ALLGOALS(dres_inst_tac [("x","m")] spec));
   1.164 -by (dres_inst_tac [("x","%~x")] real_add_le_mono1 1);
   1.165 -by (dres_inst_tac [("x","x")] real_add_le_mono1 2);
   1.166 -by (auto_tac (claset(),simpset() addsimps [real_add_assoc,
   1.167 -      real_add_minus,real_add_minus_left,real_add_zero_right]));
   1.168 -qed "lemma_arch";
   1.169 -
   1.170  Goal "0r < x ==> EX n. rinv(%%#n) < x";
   1.171  by (stac real_nat_rinv_Ex_iff 1);
   1.172  by (EVERY1[rtac ccontr, Asm_full_simp_tac]);
   1.173 @@ -187,15 +157,15 @@
   1.174  by (asm_full_simp_tac (simpset() addsimps 
   1.175     [real_nat_Suc,real_add_mult_distrib2]) 1);
   1.176  by (blast_tac (claset() addIs [isLubD2]) 2);
   1.177 -by (asm_full_simp_tac (simpset() addsimps [lemma_arch]) 1);
   1.178 -by (subgoal_tac "isUb (UNIV::real set) {z. EX n. z = x*%%#n} (t + %~x)" 1);
   1.179 +by (asm_full_simp_tac
   1.180 +    (simpset() addsimps [real_le_diff_eq RS sym, real_diff_def]) 1);
   1.181 +by (subgoal_tac "isUb (UNIV::real set) {z. EX n. z = x*%%#n} (t + -x)" 1);
   1.182  by (blast_tac (claset() addSIs [isUbI,setleI]) 2);
   1.183 -by (dres_inst_tac [("y","t+%~x")] isLub_le_isUb 1);
   1.184 -by (dres_inst_tac [("x","%~t")] real_add_left_le_mono1 2);
   1.185 +by (dres_inst_tac [("y","t+-x")] isLub_le_isUb 1);
   1.186 +by (dres_inst_tac [("x","-t")] real_add_left_le_mono1 2);
   1.187  by (auto_tac (claset() addDs [real_le_less_trans,
   1.188 -    (real_minus_zero_less_iff2 RS iffD2)], simpset() 
   1.189 -    addsimps [real_less_not_refl,real_add_assoc RS sym,
   1.190 -    real_add_minus_left,real_add_zero_left]));
   1.191 +			      (real_minus_zero_less_iff2 RS iffD2)], 
   1.192 +	      simpset() addsimps [real_less_not_refl,real_add_assoc RS sym]));
   1.193  qed "reals_Archimedean";
   1.194  
   1.195  Goal "EX n. (x::real) < %%#n";
   1.196 @@ -203,15 +173,17 @@
   1.197  by (res_inst_tac [("x","0")] exI 1);
   1.198  by (res_inst_tac [("x","0")] exI 2);
   1.199  by (auto_tac (claset() addEs [real_less_trans],
   1.200 -    simpset() addsimps [real_nat_one,real_zero_less_one]));
   1.201 +	      simpset() addsimps [real_nat_one,real_zero_less_one]));
   1.202  by (forward_tac [(real_rinv_gt_zero RS reals_Archimedean)] 1);
   1.203  by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1);
   1.204  by (forw_inst_tac [("y","rinv x")] real_mult_less_mono1 1);
   1.205  by (auto_tac (claset(),simpset() addsimps [real_not_refl2 RS not_sym]));
   1.206  by (dres_inst_tac [("n1","n"),("y","1r")] 
   1.207       (real_nat_less_zero RS real_mult_less_mono2)  1);
   1.208 -by (auto_tac (claset(),simpset() addsimps [real_nat_less_zero,
   1.209 -    real_not_refl2 RS not_sym,real_mult_assoc RS sym]));
   1.210 +by (auto_tac (claset(),
   1.211 +	      simpset() addsimps [real_nat_less_zero,
   1.212 +				  real_not_refl2 RS not_sym,
   1.213 +				  real_mult_assoc RS sym]));
   1.214  qed "reals_Archimedean2";
   1.215  
   1.216