src/HOL/Real/PReal.ML
changeset 9043 ca761fe227d8
parent 8919 d00b01ed8539
child 9108 9fff97d29837
     1.1 --- a/src/HOL/Real/PReal.ML	Wed Jun 07 12:07:07 2000 +0200
     1.2 +++ b/src/HOL/Real/PReal.ML	Wed Jun 07 12:14:18 2000 +0200
     1.3 @@ -44,7 +44,7 @@
     1.4  by (rtac (Rep_preal RS preal_psubset_empty) 1);
     1.5  qed "Rep_preal_psubset_empty";
     1.6  
     1.7 -Goal "? x. x: Rep_preal X";
     1.8 +Goal "EX x. x: Rep_preal X";
     1.9  by (cut_inst_tac [("x","X")]  Rep_preal_psubset_empty 1);
    1.10  by (auto_tac (claset() addIs [(equals0I RS sym)],
    1.11                simpset() addsimps [psubset_def]));
    1.12 @@ -52,22 +52,22 @@
    1.13  
    1.14  Goalw [preal_def] 
    1.15        "[| {} < A; A < UNIV; \
    1.16 -\              (!y: A. ((!z. z < y --> z: A) & \
    1.17 -\                        (? u: A. y < u))) |] ==> A : preal";
    1.18 +\              (ALL y: A. ((ALL z. z < y --> z: A) & \
    1.19 +\                        (EX u: A. y < u))) |] ==> A : preal";
    1.20  by (Fast_tac 1);
    1.21  qed "prealI1";
    1.22      
    1.23  Goalw [preal_def] 
    1.24        "[| {} < A; A < UNIV; \
    1.25 -\              !y: A. (!z. z < y --> z: A); \
    1.26 -\              !y: A. (? u: A. y < u) |] ==> A : preal";
    1.27 +\              ALL y: A. (ALL z. z < y --> z: A); \
    1.28 +\              ALL y: A. (EX u: A. y < u) |] ==> A : preal";
    1.29  by (Best_tac 1);
    1.30  qed "prealI2";
    1.31  
    1.32  Goalw [preal_def] 
    1.33        "A : preal ==> {} < A & A < UNIV & \
    1.34 -\                         (!y: A. ((!z. z < y --> z: A) & \
    1.35 -\                                  (? u: A. y < u)))";
    1.36 +\                         (ALL y: A. ((ALL z. z < y --> z: A) & \
    1.37 +\                                  (EX u: A. y < u)))";
    1.38  by (Fast_tac 1);
    1.39  qed "prealE_lemma";
    1.40  
    1.41 @@ -85,11 +85,11 @@
    1.42  by (Fast_tac 1);
    1.43  qed "prealE_lemma2";
    1.44  
    1.45 -Goalw [preal_def] "A : preal ==> !y: A. (!z. z < y --> z: A)";
    1.46 +Goalw [preal_def] "A : preal ==> ALL y: A. (ALL z. z < y --> z: A)";
    1.47  by (Fast_tac 1);
    1.48  qed "prealE_lemma3";
    1.49  
    1.50 -Goal "[| A : preal; y: A |] ==> (!z. z < y --> z: A)";
    1.51 +Goal "[| A : preal; y: A |] ==> (ALL z. z < y --> z: A)";
    1.52  by (fast_tac (claset() addSDs [prealE_lemma3]) 1);
    1.53  qed "prealE_lemma3a";
    1.54  
    1.55 @@ -97,15 +97,15 @@
    1.56  by (fast_tac (claset() addSDs [prealE_lemma3a]) 1);
    1.57  qed "prealE_lemma3b";
    1.58  
    1.59 -Goalw [preal_def] "A : preal ==> !y: A. (? u: A. y < u)";
    1.60 +Goalw [preal_def] "A : preal ==> ALL y: A. (EX u: A. y < u)";
    1.61  by (Fast_tac 1);
    1.62  qed "prealE_lemma4";
    1.63  
    1.64 -Goal "[| A : preal; y: A |] ==> ? u: A. y < u";
    1.65 +Goal "[| A : preal; y: A |] ==> EX u: A. y < u";
    1.66  by (fast_tac (claset() addSDs [prealE_lemma4]) 1);
    1.67  qed "prealE_lemma4a";
    1.68  
    1.69 -Goal "? x. x~: Rep_preal X";
    1.70 +Goal "EX x. x~: Rep_preal X";
    1.71  by (cut_inst_tac [("x","X")] Rep_preal 1);
    1.72  by (dtac prealE_lemma2 1);
    1.73  by (rtac ccontr 1);
    1.74 @@ -148,7 +148,7 @@
    1.75  (* A positive fraction not in a positive real is an upper bound *)
    1.76  (* Gleason p. 122 - Remark (1)                                  *)
    1.77  
    1.78 -Goal "x ~: Rep_preal(R) ==> !y: Rep_preal(R). y < x";
    1.79 +Goal "x ~: Rep_preal(R) ==> ALL y: Rep_preal(R). y < x";
    1.80  by (cut_inst_tac [("x1","R")] (Rep_preal RS prealE_lemma) 1);
    1.81  by (auto_tac (claset() addIs [not_less_not_eq_prat_less],simpset()));
    1.82  qed "not_in_preal_ub";
    1.83 @@ -207,13 +207,13 @@
    1.84  (** lemmas for proving positive reals addition set in preal **)
    1.85  
    1.86  (** Part 1 of Dedekind sections def **)
    1.87 -Goal "{} < {w. ? x: Rep_preal R. ? y:Rep_preal S. w = x + y}";
    1.88 +Goal "{} < {w. EX x: Rep_preal R. EX y:Rep_preal S. w = x + y}";
    1.89  by (cut_facts_tac [mem_Rep_preal_Ex,mem_Rep_preal_Ex] 1);
    1.90  by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
    1.91  qed "preal_add_set_not_empty";
    1.92  
    1.93  (** Part 2 of Dedekind sections def **)
    1.94 -Goal "? q. q  ~: {w. ? x: Rep_preal R. ? y:Rep_preal S. w = x + y}";
    1.95 +Goal "EX q. q  ~: {w. EX x: Rep_preal R. EX y:Rep_preal S. w = x + y}";
    1.96  by (cut_inst_tac [("X","R")] not_mem_Rep_preal_Ex 1);
    1.97  by (cut_inst_tac [("X","S")] not_mem_Rep_preal_Ex 1);
    1.98  by (REPEAT(etac exE 1));
    1.99 @@ -224,7 +224,7 @@
   1.100  by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
   1.101  qed "preal_not_mem_add_set_Ex";
   1.102  
   1.103 -Goal "{w. ? x: Rep_preal R. ? y:Rep_preal S. w = x + y} < UNIV";
   1.104 +Goal "{w. EX x: Rep_preal R. EX y:Rep_preal S. w = x + y} < UNIV";
   1.105  by (auto_tac (claset() addSIs [psubsetI],simpset()));
   1.106  by (cut_inst_tac [("R","R"),("S","S")] preal_not_mem_add_set_Ex 1);
   1.107  by (etac exE 1);
   1.108 @@ -233,8 +233,8 @@
   1.109  qed "preal_add_set_not_prat_set";
   1.110  
   1.111  (** Part 3 of Dedekind sections def **)
   1.112 -Goal "!y: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x + y}. \
   1.113 -\         !z. z < y --> z : {w. ? x:Rep_preal R. ? y:Rep_preal S. w = x + y}";
   1.114 +Goal "ALL y: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x + y}. \
   1.115 +\         ALL z. z < y --> z : {w. EX x:Rep_preal R. EX y:Rep_preal S. w = x + y}";
   1.116  by Auto_tac;
   1.117  by (ftac prat_mult_qinv_less_1 1);
   1.118  by (forw_inst_tac [("x","x"),("q2.0","prat_of_pnat (Abs_pnat 1)")] 
   1.119 @@ -250,14 +250,14 @@
   1.120       RS sym,prat_add_assoc RS sym,prat_mult_assoc]));
   1.121  qed "preal_add_set_lemma3";
   1.122  
   1.123 -Goal "!y: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x + y}. \
   1.124 -\         ? u: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x + y}. y < u";
   1.125 +Goal "ALL y: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x + y}. \
   1.126 +\         EX u: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x + y}. y < u";
   1.127  by Auto_tac;
   1.128  by (dtac (Rep_preal RS prealE_lemma4a) 1);
   1.129  by (auto_tac (claset() addIs [prat_add_less2_mono1],simpset()));
   1.130  qed "preal_add_set_lemma4";
   1.131  
   1.132 -Goal "{w. ? x: Rep_preal R. ? y: Rep_preal S. w = x + y} : preal";
   1.133 +Goal "{w. EX x: Rep_preal R. EX y: Rep_preal S. w = x + y} : preal";
   1.134  by (rtac prealI2 1);
   1.135  by (rtac preal_add_set_not_empty 1);
   1.136  by (rtac preal_add_set_not_prat_set 1);
   1.137 @@ -297,13 +297,13 @@
   1.138  (** lemmas for proving positive reals multiplication set in preal **)
   1.139  
   1.140  (** Part 1 of Dedekind sections def **)
   1.141 -Goal "{} < {w. ? x: Rep_preal R. ? y:Rep_preal S. w = x * y}";
   1.142 +Goal "{} < {w. EX x: Rep_preal R. EX y:Rep_preal S. w = x * y}";
   1.143  by (cut_facts_tac [mem_Rep_preal_Ex,mem_Rep_preal_Ex] 1);
   1.144  by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
   1.145  qed "preal_mult_set_not_empty";
   1.146  
   1.147  (** Part 2 of Dedekind sections def **)
   1.148 -Goal "? q. q  ~: {w. ? x: Rep_preal R. ? y:Rep_preal S. w = x * y}";
   1.149 +Goal "EX q. q  ~: {w. EX x: Rep_preal R. EX y:Rep_preal S. w = x * y}";
   1.150  by (cut_inst_tac [("X","R")] not_mem_Rep_preal_Ex 1);
   1.151  by (cut_inst_tac [("X","S")] not_mem_Rep_preal_Ex 1);
   1.152  by (REPEAT(etac exE 1));
   1.153 @@ -314,7 +314,7 @@
   1.154  by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
   1.155  qed "preal_not_mem_mult_set_Ex";
   1.156  
   1.157 -Goal "{w. ? x: Rep_preal R. ? y:Rep_preal S. w = x * y} < UNIV";
   1.158 +Goal "{w. EX x: Rep_preal R. EX y:Rep_preal S. w = x * y} < UNIV";
   1.159  by (auto_tac (claset() addSIs [psubsetI],simpset()));
   1.160  by (cut_inst_tac [("R","R"),("S","S")] preal_not_mem_mult_set_Ex 1);
   1.161  by (etac exE 1);
   1.162 @@ -323,8 +323,8 @@
   1.163  qed "preal_mult_set_not_prat_set";
   1.164  
   1.165  (** Part 3 of Dedekind sections def **)
   1.166 -Goal "!y: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x * y}. \
   1.167 -\         !z. z < y --> z : {w. ? x:Rep_preal R. ? y:Rep_preal S. w = x * y}";
   1.168 +Goal "ALL y: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x * y}. \
   1.169 +\         ALL z. z < y --> z : {w. EX x:Rep_preal R. EX y:Rep_preal S. w = x * y}";
   1.170  by Auto_tac;
   1.171  by (forw_inst_tac [("x","qinv(ya)"),("q1.0","z")] 
   1.172      prat_mult_left_less2_mono1 1);
   1.173 @@ -335,14 +335,14 @@
   1.174  by (auto_tac (claset(),simpset() addsimps [prat_mult_assoc]));
   1.175  qed "preal_mult_set_lemma3";
   1.176  
   1.177 -Goal "!y: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x * y}. \
   1.178 -\         ? u: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x * y}. y < u";
   1.179 +Goal "ALL y: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x * y}. \
   1.180 +\         EX u: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x * y}. y < u";
   1.181  by Auto_tac;
   1.182  by (dtac (Rep_preal RS prealE_lemma4a) 1);
   1.183  by (auto_tac (claset() addIs [prat_mult_less2_mono1],simpset()));
   1.184  qed "preal_mult_set_lemma4";
   1.185  
   1.186 -Goal "{w. ? x: Rep_preal R. ? y: Rep_preal S. w = x * y} : preal";
   1.187 +Goal "{w. EX x: Rep_preal R. EX y: Rep_preal S. w = x * y} : preal";
   1.188  by (rtac prealI2 1);
   1.189  by (rtac preal_mult_set_not_empty 1);
   1.190  by (rtac preal_mult_set_not_prat_set 1);
   1.191 @@ -410,39 +410,39 @@
   1.192   (** lemmas **)
   1.193  Goalw [preal_add_def] 
   1.194        "z: Rep_preal(R+S) ==> \
   1.195 -\           ? x: Rep_preal(R). ? y: Rep_preal(S). z = x + y";
   1.196 +\           EX x: Rep_preal(R). EX y: Rep_preal(S). z = x + y";
   1.197  by (dtac (preal_mem_add_set RS Abs_preal_inverse RS subst) 1);
   1.198  by (Fast_tac 1);
   1.199  qed "mem_Rep_preal_addD";
   1.200  
   1.201  Goalw [preal_add_def] 
   1.202 -      "? x: Rep_preal(R). ? y: Rep_preal(S). z = x + y \
   1.203 +      "EX x: Rep_preal(R). EX y: Rep_preal(S). z = x + y \
   1.204  \      ==> z: Rep_preal(R+S)";
   1.205  by (rtac (preal_mem_add_set RS Abs_preal_inverse RS ssubst) 1);
   1.206  by (Fast_tac 1);
   1.207  qed "mem_Rep_preal_addI";
   1.208  
   1.209 -Goal " z: Rep_preal(R+S) = (? x: Rep_preal(R). \
   1.210 -\                                 ? y: Rep_preal(S). z = x + y)";
   1.211 +Goal " z: Rep_preal(R+S) = (EX x: Rep_preal(R). \
   1.212 +\                                 EX y: Rep_preal(S). z = x + y)";
   1.213  by (fast_tac (claset() addSIs [mem_Rep_preal_addD,mem_Rep_preal_addI]) 1);
   1.214  qed "mem_Rep_preal_add_iff";
   1.215  
   1.216  Goalw [preal_mult_def] 
   1.217        "z: Rep_preal(R*S) ==> \
   1.218 -\           ? x: Rep_preal(R). ? y: Rep_preal(S). z = x * y";
   1.219 +\           EX x: Rep_preal(R). EX y: Rep_preal(S). z = x * y";
   1.220  by (dtac (preal_mem_mult_set RS Abs_preal_inverse RS subst) 1);
   1.221  by (Fast_tac 1);
   1.222  qed "mem_Rep_preal_multD";
   1.223  
   1.224  Goalw [preal_mult_def] 
   1.225 -      "? x: Rep_preal(R). ? y: Rep_preal(S). z = x * y \
   1.226 +      "EX x: Rep_preal(R). EX y: Rep_preal(S). z = x * y \
   1.227  \      ==> z: Rep_preal(R*S)";
   1.228  by (rtac (preal_mem_mult_set RS Abs_preal_inverse RS ssubst) 1);
   1.229  by (Fast_tac 1);
   1.230  qed "mem_Rep_preal_multI";
   1.231  
   1.232 -Goal " z: Rep_preal(R*S) = (? x: Rep_preal(R). \
   1.233 -\                                 ? y: Rep_preal(S). z = x * y)";
   1.234 +Goal " z: Rep_preal(R*S) = (EX x: Rep_preal(R). \
   1.235 +\                                 EX y: Rep_preal(S). z = x * y)";
   1.236  by (fast_tac (claset() addSIs [mem_Rep_preal_multD,mem_Rep_preal_multI]) 1);
   1.237  qed "mem_Rep_preal_mult_iff";
   1.238  
   1.239 @@ -507,13 +507,13 @@
   1.240  (*** Prove existence of inverse ***)
   1.241  (*** Inverse is a positive real ***)
   1.242  
   1.243 -Goal "? y. qinv(y) ~:  Rep_preal X";
   1.244 +Goal "EX y. qinv(y) ~:  Rep_preal X";
   1.245  by (cut_inst_tac [("X","X")] not_mem_Rep_preal_Ex 1);
   1.246  by (etac exE 1 THEN cut_inst_tac [("x","x")] prat_as_inverse_ex 1);
   1.247  by Auto_tac;
   1.248  qed "qinv_not_mem_Rep_preal_Ex";
   1.249  
   1.250 -Goal "? q. q: {x. ? y. x < y & qinv y ~:  Rep_preal A}";
   1.251 +Goal "EX q. q: {x. EX y. x < y & qinv y ~:  Rep_preal A}";
   1.252  by (cut_inst_tac [("X","A")] qinv_not_mem_Rep_preal_Ex 1);
   1.253  by Auto_tac;
   1.254  by (cut_inst_tac [("y","y")] qless_Ex 1);
   1.255 @@ -521,19 +521,19 @@
   1.256  qed "lemma_preal_mem_inv_set_ex";
   1.257  
   1.258  (** Part 1 of Dedekind sections def **)
   1.259 -Goal "{} < {x. ? y. x < y & qinv y ~:  Rep_preal A}";
   1.260 +Goal "{} < {x. EX y. x < y & qinv y ~:  Rep_preal A}";
   1.261  by (cut_facts_tac [lemma_preal_mem_inv_set_ex] 1);
   1.262  by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
   1.263  qed "preal_inv_set_not_empty";
   1.264  
   1.265  (** Part 2 of Dedekind sections def **)
   1.266 -Goal "? y. qinv(y) :  Rep_preal X";
   1.267 +Goal "EX y. qinv(y) :  Rep_preal X";
   1.268  by (cut_inst_tac [("X","X")] mem_Rep_preal_Ex 1);
   1.269  by (etac exE 1 THEN cut_inst_tac [("x","x")] prat_as_inverse_ex 1);
   1.270  by Auto_tac;
   1.271  qed "qinv_mem_Rep_preal_Ex";
   1.272  
   1.273 -Goal "? x. x ~: {x. ? y. x < y & qinv y ~:  Rep_preal A}";
   1.274 +Goal "EX x. x ~: {x. EX y. x < y & qinv y ~:  Rep_preal A}";
   1.275  by (rtac ccontr 1);
   1.276  by (cut_inst_tac [("X","A")] qinv_mem_Rep_preal_Ex 1);
   1.277  by Auto_tac;
   1.278 @@ -544,7 +544,7 @@
   1.279  by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
   1.280  qed "preal_not_mem_inv_set_Ex";
   1.281  
   1.282 -Goal "{x. ? y. x < y & qinv y ~:  Rep_preal A} < UNIV";
   1.283 +Goal "{x. EX y. x < y & qinv y ~:  Rep_preal A} < UNIV";
   1.284  by (auto_tac (claset() addSIs [psubsetI],simpset()));
   1.285  by (cut_inst_tac [("A","A")]  preal_not_mem_inv_set_Ex 1);
   1.286  by (etac exE 1);
   1.287 @@ -553,19 +553,19 @@
   1.288  qed "preal_inv_set_not_prat_set";
   1.289  
   1.290  (** Part 3 of Dedekind sections def **)
   1.291 -Goal "! y: {x. ? y. x < y & qinv y ~: Rep_preal A}. \
   1.292 - \      !z. z < y --> z : {x. ? y. x < y & qinv y ~: Rep_preal A}";
   1.293 +Goal "ALL y: {x. EX y. x < y & qinv y ~: Rep_preal A}. \
   1.294 + \      ALL z. z < y --> z : {x. EX y. x < y & qinv y ~: Rep_preal A}";
   1.295  by Auto_tac;
   1.296  by (res_inst_tac [("x","ya")] exI 1);
   1.297  by (auto_tac (claset() addIs [prat_less_trans],simpset()));
   1.298  qed "preal_inv_set_lemma3";
   1.299  
   1.300 -Goal "! y: {x. ? y. x < y & qinv y ~: Rep_preal A}. \
   1.301 -\       Bex {x. ? y. x < y & qinv y ~: Rep_preal A} (op < y)";
   1.302 +Goal "ALL y: {x. EX y. x < y & qinv y ~: Rep_preal A}. \
   1.303 +\       Bex {x. EX y. x < y & qinv y ~: Rep_preal A} (op < y)";
   1.304  by (blast_tac (claset() addDs [prat_dense]) 1);
   1.305  qed "preal_inv_set_lemma4";
   1.306  
   1.307 -Goal "{x. ? y. x < y & qinv(y) ~: Rep_preal(A)} : preal";
   1.308 +Goal "{x. EX y. x < y & qinv(y) ~: Rep_preal(A)} : preal";
   1.309  by (rtac prealI2 1);
   1.310  by (rtac preal_inv_set_not_empty 1);
   1.311  by (rtac preal_inv_set_not_prat_set 1);
   1.312 @@ -585,8 +585,8 @@
   1.313  qed "preal_mem_mult_invD";
   1.314  
   1.315  (*** Gleason's Lemma 9-3.4 p 122 ***)
   1.316 -Goal "! xa : Rep_preal(A). xa + x : Rep_preal(A) ==> \
   1.317 -\            ? xb : Rep_preal(A). xb + (prat_of_pnat p)*x : Rep_preal(A)";
   1.318 +Goal "ALL xa : Rep_preal(A). xa + x : Rep_preal(A) ==> \
   1.319 +\            EX xb : Rep_preal(A). xb + (prat_of_pnat p)*x : Rep_preal(A)";
   1.320  by (cut_facts_tac [mem_Rep_preal_Ex] 1);
   1.321  by (res_inst_tac [("n","p")] pnat_induct 1);
   1.322  by (auto_tac (claset(),simpset() addsimps [pnat_one_def,
   1.323 @@ -603,7 +603,7 @@
   1.324      simpset() addsimps [prat_mult,pre_lemma_gleason9_34b,pnat_mult_assoc]));
   1.325  qed "lemma1b_gleason9_34";
   1.326  
   1.327 -Goal "! xa : Rep_preal(A). xa + x : Rep_preal(A) ==> False";
   1.328 +Goal "ALL xa : Rep_preal(A). xa + x : Rep_preal(A) ==> False";
   1.329  by (cut_inst_tac [("X","A")] not_mem_Rep_preal_Ex 1);
   1.330  by (etac exE 1);
   1.331  by (dtac not_in_preal_ub 1);
   1.332 @@ -618,7 +618,7 @@
   1.333      simpset() addsimps [prat_of_pnat_def]));
   1.334  qed "lemma_gleason9_34a";
   1.335  
   1.336 -Goal "? r: Rep_preal(R). r + x ~: Rep_preal(R)";
   1.337 +Goal "EX r: Rep_preal(R). r + x ~: Rep_preal(R)";
   1.338  by (rtac ccontr 1);
   1.339  by (blast_tac (claset() addIs [lemma_gleason9_34a]) 1);
   1.340  qed "lemma_gleason9_34";
   1.341 @@ -639,7 +639,7 @@
   1.342  (******)
   1.343  
   1.344  (*** FIXME: long! ***)
   1.345 -Goal "prat_of_pnat 1p < x ==> ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
   1.346 +Goal "prat_of_pnat 1p < x ==> EX r: Rep_preal(A). r*x ~: Rep_preal(A)";
   1.347  by (res_inst_tac [("X1","A")] (mem_Rep_preal_Ex RS exE) 1);
   1.348  by (res_inst_tac [("Q","xa*x : Rep_preal(A)")] (excluded_middle RS disjE) 1);
   1.349  by (Fast_tac 1);
   1.350 @@ -663,7 +663,7 @@
   1.351  qed "lemma_gleason9_36";
   1.352  
   1.353  Goal "prat_of_pnat (Abs_pnat 1) < x ==> \
   1.354 -\     ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
   1.355 +\     EX r: Rep_preal(A). r*x ~: Rep_preal(A)";
   1.356  by (rtac lemma_gleason9_36 1);
   1.357  by (asm_simp_tac (simpset() addsimps [pnat_one_def]) 1);
   1.358  qed "lemma_gleason9_36a";
   1.359 @@ -813,7 +813,7 @@
   1.360  (**** Define the D required and show that it is a positive real ****)
   1.361  
   1.362  (* useful lemmas - proved elsewhere? *)
   1.363 -Goalw [psubset_def] "A < B ==> ? x. x ~: A & x : B";
   1.364 +Goalw [psubset_def] "A < B ==> EX x. x ~: A & x : B";
   1.365  by (etac conjE 1);
   1.366  by (etac swap 1);
   1.367  by (etac equalityI 1);
   1.368 @@ -843,7 +843,7 @@
   1.369  (** Part 1 of Dedekind sections def **)
   1.370  Goalw [preal_less_def]
   1.371       "A < B ==> \
   1.372 -\     ? q. q : {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
   1.373 +\     EX q. q : {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
   1.374  by (EVERY1[dtac lemma_psubset_mem, etac exE, etac conjE]);
   1.375  by (dres_inst_tac [("x1","B")] (Rep_preal RS prealE_lemma4a) 1);
   1.376  by (auto_tac (claset(),simpset() addsimps [prat_less_def]));
   1.377 @@ -851,13 +851,13 @@
   1.378  
   1.379  Goal
   1.380       "A < B ==> \
   1.381 -\       {} < {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
   1.382 +\       {} < {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
   1.383  by (dtac lemma_ex_mem_less_left_add1 1);
   1.384  by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
   1.385  qed "preal_less_set_not_empty";
   1.386  
   1.387  (** Part 2 of Dedekind sections def **)
   1.388 -Goal "? q. q ~: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
   1.389 +Goal "EX q. q ~: {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
   1.390  by (cut_inst_tac [("X","B")] not_mem_Rep_preal_Ex 1);
   1.391  by (etac exE 1);
   1.392  by (res_inst_tac [("x","x")] exI 1);
   1.393 @@ -866,7 +866,7 @@
   1.394  by (auto_tac (claset() addDs [Rep_preal RS prealE_lemma3b],simpset()));
   1.395  qed "lemma_ex_not_mem_less_left_add1";
   1.396  
   1.397 -Goal "{d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} < UNIV";
   1.398 +Goal "{d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} < UNIV";
   1.399  by (auto_tac (claset() addSIs [psubsetI],simpset()));
   1.400  by (cut_inst_tac [("A","A"),("B","B")] lemma_ex_not_mem_less_left_add1 1);
   1.401  by (etac exE 1);
   1.402 @@ -875,16 +875,16 @@
   1.403  qed "preal_less_set_not_prat_set";
   1.404  
   1.405  (** Part 3 of Dedekind sections def **)
   1.406 -Goal "A < B ==> ! y: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
   1.407 - \      !z. z < y --> z : {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
   1.408 +Goal "A < B ==> ALL y: {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
   1.409 + \      ALL z. z < y --> z : {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
   1.410  by Auto_tac;
   1.411  by (dres_inst_tac [("x","n")] prat_add_less2_mono2 1);
   1.412  by (dtac (Rep_preal RS prealE_lemma3b) 1);
   1.413  by Auto_tac;
   1.414  qed "preal_less_set_lemma3";
   1.415  
   1.416 -Goal "A < B ==> ! y: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
   1.417 -\       Bex {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} (op < y)";
   1.418 +Goal "A < B ==> ALL y: {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
   1.419 +\       Bex {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} (op < y)";
   1.420  by Auto_tac;
   1.421  by (dtac (Rep_preal RS prealE_lemma4a) 1);
   1.422  by (auto_tac (claset(),simpset() addsimps [prat_less_def,prat_add_assoc]));
   1.423 @@ -892,7 +892,7 @@
   1.424  
   1.425  Goal 
   1.426       "!! (A::preal). A < B ==> \
   1.427 -\     {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}: preal";
   1.428 +\     {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}: preal";
   1.429  by (rtac prealI2 1);
   1.430  by (rtac preal_less_set_not_empty 1);
   1.431  by (rtac preal_less_set_not_prat_set 2);
   1.432 @@ -904,7 +904,7 @@
   1.433  (** proving that A + D <= B **)
   1.434  Goalw [preal_le_def] 
   1.435         "!! (A::preal). A < B ==> \
   1.436 -\         A + Abs_preal({d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}) <= B";
   1.437 +\         A + Abs_preal({d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}) <= B";
   1.438  by (rtac subsetI 1);
   1.439  by (dtac mem_Rep_preal_addD 1);
   1.440  by (auto_tac (claset(),simpset() addsimps [
   1.441 @@ -918,14 +918,14 @@
   1.442  
   1.443  (** proving that B <= A + D  --- trickier **)
   1.444  (** lemma **)
   1.445 -Goal "x : Rep_preal(B) ==> ? e. x + e : Rep_preal(B)";
   1.446 +Goal "x : Rep_preal(B) ==> EX e. x + e : Rep_preal(B)";
   1.447  by (dtac (Rep_preal RS prealE_lemma4a) 1);
   1.448  by (auto_tac (claset(),simpset() addsimps [prat_less_def]));
   1.449  qed "lemma_sum_mem_Rep_preal_ex";
   1.450  
   1.451  Goalw [preal_le_def] 
   1.452         "!! (A::preal). A < B ==> \
   1.453 -\         B <= A + Abs_preal({d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)})";
   1.454 +\         B <= A + Abs_preal({d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)})";
   1.455  by (rtac subsetI 1);
   1.456  by (res_inst_tac [("Q","x: Rep_preal(A)")] (excluded_middle RS disjE) 1);
   1.457  by (rtac mem_Rep_preal_addI 1);
   1.458 @@ -945,12 +945,12 @@
   1.459  
   1.460  (*** required proof ***)
   1.461  Goal "!! (A::preal). A < B ==> \
   1.462 -\         A + Abs_preal({d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}) = B";
   1.463 +\         A + Abs_preal({d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}) = B";
   1.464  by (blast_tac (claset() addIs [preal_le_anti_sym,
   1.465                  preal_less_add_left_subsetI,preal_less_add_left_subsetI2]) 1);
   1.466  qed "preal_less_add_left";
   1.467  
   1.468 -Goal "!! (A::preal). A < B ==> ? D. A + D = B";
   1.469 +Goal "!! (A::preal). A < B ==> EX D. A + D = B";
   1.470  by (fast_tac (claset() addDs [preal_less_add_left]) 1);
   1.471  qed "preal_less_add_left_Ex";        
   1.472  
   1.473 @@ -1070,23 +1070,23 @@
   1.474  (*** Completeness of preal ***)
   1.475  
   1.476  (*** prove that supremum is a cut ***)
   1.477 -Goal "? (X::preal). X: P ==> \
   1.478 -\         ? q.  q: {w. ? X. X : P & w : Rep_preal X}";
   1.479 +Goal "EX (X::preal). X: P ==> \
   1.480 +\         EX q.  q: {w. EX X. X : P & w : Rep_preal X}";
   1.481  by Safe_tac;
   1.482  by (cut_inst_tac [("X","X")] mem_Rep_preal_Ex 1);
   1.483  by Auto_tac;
   1.484  qed "preal_sup_mem_Ex";
   1.485  
   1.486  (** Part 1 of Dedekind def **)
   1.487 -Goal "? (X::preal). X: P ==> \
   1.488 -\         {} < {w. ? X : P. w : Rep_preal X}";
   1.489 +Goal "EX (X::preal). X: P ==> \
   1.490 +\         {} < {w. EX X : P. w : Rep_preal X}";
   1.491  by (dtac preal_sup_mem_Ex 1);
   1.492  by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
   1.493  qed "preal_sup_set_not_empty";
   1.494  
   1.495  (** Part 2 of Dedekind sections def **) 
   1.496 -Goalw [preal_less_def] "? Y. (! X: P. X < Y)  \             
   1.497 -\         ==> ? q. q ~: {w. ? X. X: P & w: Rep_preal(X)}"; (**)
   1.498 +Goalw [preal_less_def] "EX Y. (ALL X: P. X < Y)  \             
   1.499 +\         ==> EX q. q ~: {w. EX X. X: P & w: Rep_preal(X)}"; (**)
   1.500  by (auto_tac (claset(),simpset() addsimps [psubset_def]));
   1.501  by (cut_inst_tac [("X","Y")] not_mem_Rep_preal_Ex 1);
   1.502  by (etac exE 1);
   1.503 @@ -1094,8 +1094,8 @@
   1.504  by (auto_tac (claset() addSDs [bspec],simpset()));
   1.505  qed "preal_sup_not_mem_Ex";
   1.506  
   1.507 -Goalw [preal_le_def] "? Y. (! X: P. X <= Y)  \
   1.508 -\         ==> ? q. q ~: {w. ? X. X: P & w: Rep_preal(X)}";
   1.509 +Goalw [preal_le_def] "EX Y. (ALL X: P. X <= Y)  \
   1.510 +\         ==> EX q. q ~: {w. EX X. X: P & w: Rep_preal(X)}";
   1.511  by (Step_tac 1);
   1.512  by (cut_inst_tac [("X","Y")] not_mem_Rep_preal_Ex 1);
   1.513  by (etac exE 1);
   1.514 @@ -1103,16 +1103,16 @@
   1.515  by (auto_tac (claset() addSDs [bspec],simpset()));
   1.516  qed "preal_sup_not_mem_Ex1";
   1.517  
   1.518 -Goal "? Y. (! X: P. X < Y)  \                                    
   1.519 -\         ==> {w. ? X: P. w: Rep_preal(X)} < UNIV";       (**)
   1.520 +Goal "EX Y. (ALL X: P. X < Y)  \                                    
   1.521 +\         ==> {w. EX X: P. w: Rep_preal(X)} < UNIV";       (**)
   1.522  by (dtac preal_sup_not_mem_Ex 1);
   1.523  by (auto_tac (claset() addSIs [psubsetI],simpset()));
   1.524  by (eres_inst_tac [("c","q")] equalityCE 1);
   1.525  by Auto_tac;
   1.526  qed "preal_sup_set_not_prat_set";
   1.527  
   1.528 -Goal "? Y. (! X: P. X <= Y)  \
   1.529 -\         ==> {w. ? X: P. w: Rep_preal(X)} < UNIV";
   1.530 +Goal "EX Y. (ALL X: P. X <= Y)  \
   1.531 +\         ==> {w. EX X: P. w: Rep_preal(X)} < UNIV";
   1.532  by (dtac preal_sup_not_mem_Ex1 1);
   1.533  by (auto_tac (claset() addSIs [psubsetI],simpset()));
   1.534  by (eres_inst_tac [("c","q")] equalityCE 1);
   1.535 @@ -1120,32 +1120,32 @@
   1.536  qed "preal_sup_set_not_prat_set1";
   1.537  
   1.538  (** Part 3 of Dedekind sections def **)
   1.539 -Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \              
   1.540 -\         ==> ! y: {w. ? X: P. w: Rep_preal X}. \
   1.541 -\             !z. z < y --> z: {w. ? X: P. w: Rep_preal X}";         (**)
   1.542 +Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X < Y) |] \              
   1.543 +\         ==> ALL y: {w. EX X: P. w: Rep_preal X}. \
   1.544 +\             ALL z. z < y --> z: {w. EX X: P. w: Rep_preal X}";         (**)
   1.545  by (auto_tac(claset() addEs [Rep_preal RS prealE_lemma3b],simpset()));
   1.546  qed "preal_sup_set_lemma3";
   1.547  
   1.548 -Goal "[|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
   1.549 -\         ==> ! y: {w. ? X: P. w: Rep_preal X}. \
   1.550 -\             !z. z < y --> z: {w. ? X: P. w: Rep_preal X}";
   1.551 +Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X <= Y) |] \
   1.552 +\         ==> ALL y: {w. EX X: P. w: Rep_preal X}. \
   1.553 +\             ALL z. z < y --> z: {w. EX X: P. w: Rep_preal X}";
   1.554  by (auto_tac(claset() addEs [Rep_preal RS prealE_lemma3b],simpset()));
   1.555  qed "preal_sup_set_lemma3_1";
   1.556  
   1.557 -Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \              
   1.558 -\         ==>  !y: {w. ? X: P. w: Rep_preal X}. \                        
   1.559 -\             Bex {w. ? X: P. w: Rep_preal X} (op < y)";                (**)
   1.560 +Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X < Y) |] \              
   1.561 +\         ==>  ALL y: {w. EX X: P. w: Rep_preal X}. \                        
   1.562 +\             Bex {w. EX X: P. w: Rep_preal X} (op < y)";                (**)
   1.563  by (blast_tac (claset() addDs [(Rep_preal RS prealE_lemma4a)]) 1);
   1.564  qed "preal_sup_set_lemma4";
   1.565  
   1.566 -Goal "[|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
   1.567 -\         ==>  !y: {w. ? X: P. w: Rep_preal X}. \
   1.568 -\             Bex {w. ? X: P. w: Rep_preal X} (op < y)";
   1.569 +Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X <= Y) |] \
   1.570 +\         ==>  ALL y: {w. EX X: P. w: Rep_preal X}. \
   1.571 +\             Bex {w. EX X: P. w: Rep_preal X} (op < y)";
   1.572  by (blast_tac (claset() addDs [(Rep_preal RS prealE_lemma4a)]) 1);
   1.573  qed "preal_sup_set_lemma4_1";
   1.574  
   1.575 -Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \            
   1.576 -\         ==> {w. ? X: P. w: Rep_preal(X)}: preal";                      (**)
   1.577 +Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X < Y) |] \            
   1.578 +\         ==> {w. EX X: P. w: Rep_preal(X)}: preal";                      (**)
   1.579  by (rtac prealI2 1);
   1.580  by (rtac preal_sup_set_not_empty 1);
   1.581  by (rtac preal_sup_set_not_prat_set 2);
   1.582 @@ -1154,8 +1154,8 @@
   1.583  by Auto_tac;
   1.584  qed "preal_sup";
   1.585  
   1.586 -Goal "[|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
   1.587 -\         ==> {w. ? X: P. w: Rep_preal(X)}: preal";
   1.588 +Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X <= Y) |] \
   1.589 +\         ==> {w. EX X: P. w: Rep_preal(X)}: preal";
   1.590  by (rtac prealI2 1);
   1.591  by (rtac preal_sup_set_not_empty 1);
   1.592  by (rtac preal_sup_set_not_prat_set1 2);
   1.593 @@ -1164,27 +1164,27 @@
   1.594  by Auto_tac;
   1.595  qed "preal_sup1";
   1.596  
   1.597 -Goalw [psup_def] "? Y. (! X:P. X < Y) ==> ! x: P. x <= psup P";      (**) 
   1.598 +Goalw [psup_def] "EX Y. (ALL X:P. X < Y) ==> ALL x: P. x <= psup P";      (**) 
   1.599  by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
   1.600  by (rtac (preal_sup RS Abs_preal_inverse RS ssubst) 1);
   1.601  by Auto_tac;
   1.602  qed "preal_psup_leI";
   1.603  
   1.604 -Goalw [psup_def] "? Y. (! X:P. X <= Y) ==> ! x: P. x <= psup P";
   1.605 +Goalw [psup_def] "EX Y. (ALL X:P. X <= Y) ==> ALL x: P. x <= psup P";
   1.606  by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
   1.607  by (rtac (preal_sup1 RS Abs_preal_inverse RS ssubst) 1);
   1.608  by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
   1.609  qed "preal_psup_leI2";
   1.610  
   1.611 -Goal "[| ? Y. (! X:P. X < Y); x : P |] ==> x <= psup P";              (**)
   1.612 +Goal "[| EX Y. (ALL X:P. X < Y); x : P |] ==> x <= psup P";              (**)
   1.613  by (blast_tac (claset() addSDs [preal_psup_leI]) 1);
   1.614  qed "preal_psup_leI2b";
   1.615  
   1.616 -Goal "[| ? Y. (! X:P. X <= Y); x : P |] ==> x <= psup P";
   1.617 +Goal "[| EX Y. (ALL X:P. X <= Y); x : P |] ==> x <= psup P";
   1.618  by (blast_tac (claset() addSDs [preal_psup_leI2]) 1);
   1.619  qed "preal_psup_leI2a";
   1.620  
   1.621 -Goalw [psup_def] "[| ? X. X : P; ! X:P. X < Y |] ==> psup P <= Y";   (**)
   1.622 +Goalw [psup_def] "[| EX X. X : P; ALL X:P. X < Y |] ==> psup P <= Y";   (**)
   1.623  by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
   1.624  by (dtac (([exI,exI] MRS preal_sup) RS Abs_preal_inverse RS subst) 1);
   1.625  by (rotate_tac 1 2);
   1.626 @@ -1192,7 +1192,7 @@
   1.627  by (auto_tac (claset() addSDs [bspec],simpset() addsimps [preal_less_def,psubset_def]));
   1.628  qed "psup_le_ub";
   1.629  
   1.630 -Goalw [psup_def] "[| ? X. X : P; ! X:P. X <= Y |] ==> psup P <= Y";
   1.631 +Goalw [psup_def] "[| EX X. X : P; ALL X:P. X <= Y |] ==> psup P <= Y";
   1.632  by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
   1.633  by (dtac (([exI,exI] MRS preal_sup1) RS Abs_preal_inverse RS subst) 1);
   1.634  by (rotate_tac 1 2);
   1.635 @@ -1202,8 +1202,8 @@
   1.636  qed "psup_le_ub1";
   1.637  
   1.638  (** supremum property **)
   1.639 -Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \                  
   1.640 -\         ==> (!Y. (? X: P. Y < X) = (Y < psup P))";              
   1.641 +Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X < Y) |] \                  
   1.642 +\         ==> (ALL Y. (EX X: P. Y < X) = (Y < psup P))";              
   1.643  by (forward_tac [preal_sup RS Abs_preal_inverse] 1);
   1.644  by (Fast_tac 1);
   1.645  by (auto_tac (claset() addSIs [psubsetI],simpset() addsimps [psup_def,preal_less_def]));