First round of changes, towards installation of simprocs
authorpaulson
Wed Jun 07 12:14:18 2000 +0200 (2000-06-07)
changeset 9043ca761fe227d8
parent 9042 4d4521cbbcca
child 9044 28ee037278a6
First round of changes, towards installation of simprocs

* replacing 0r by (0::real0
* better rewriting, especially pulling out signs in (-x)*y = - (x*y), etc.
src/HOL/Real/HahnBanach/Aux.thy
src/HOL/Real/Hyperreal/HyperDef.ML
src/HOL/Real/PNat.ML
src/HOL/Real/PRat.ML
src/HOL/Real/PReal.ML
src/HOL/Real/RComplete.ML
src/HOL/Real/ROOT.ML
src/HOL/Real/RealAbs.ML
src/HOL/Real/RealBin.ML
src/HOL/Real/RealDef.ML
src/HOL/Real/RealDef.thy
src/HOL/Real/RealInt.ML
src/HOL/Real/RealOrd.ML
src/HOL/Real/RealOrd.thy
src/HOL/Real/RealPow.ML
     1.1 --- a/src/HOL/Real/HahnBanach/Aux.thy	Wed Jun 07 12:07:07 2000 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/Aux.thy	Wed Jun 07 12:14:18 2000 +0200
     1.3 @@ -109,13 +109,13 @@
     1.4    thus ?thesis by (simp only: real_mult_commute)
     1.5  qed
     1.6  
     1.7 -lemma real_rinv_gt_zero1: "#0 < x ==> #0 < rinv x"
     1.8 -proof - 
     1.9 -  assume "#0 < x"
    1.10 -  hence "0r < x" by simp
    1.11 -  hence "0r < rinv x" by (rule real_rinv_gt_zero)
    1.12 -  thus ?thesis by simp
    1.13 -qed
    1.14 +lemma real_rinv_gt_zero1: "#0 < x ==> #0 < rinv x";
    1.15 +proof -; 
    1.16 +  assume "#0 < x";
    1.17 +  have "0 < x"; by simp;
    1.18 +  hence "0 < rinv x"; by (rule real_rinv_gt_zero);
    1.19 +  thus ?thesis; by simp;
    1.20 +qed;
    1.21  
    1.22  lemma real_mult_inv_right1: "x ~= #0 ==> x*rinv(x) = #1"
    1.23     by simp
    1.24 @@ -127,7 +127,7 @@
    1.25        "[| (#0::real) <= x; #0 <= y |] ==> #0 <= x * y"
    1.26  proof -
    1.27    assume "#0 <= x" "#0 <= y"
    1.28 -    have "[|0r <= x; 0r <= y|] ==> 0r <= x * y"  
    1.29 +    have "[|0 <= x; 0 <= y|] ==> 0 <= x * y"  
    1.30        by (rule real_le_mult_order)
    1.31      thus ?thesis by (simp!)
    1.32  qed
    1.33 @@ -139,7 +139,7 @@
    1.34    also have "a * ... = a * - x + a * - y" 
    1.35      by (simp only: real_add_mult_distrib2)
    1.36    also have "... = - a * x - a * y" 
    1.37 -    by (simp add: real_minus_mult_eq2 [RS sym] real_minus_mult_eq1)
    1.38 +    by simp;
    1.39    finally show ?thesis .
    1.40  qed
    1.41  
    1.42 @@ -149,7 +149,7 @@
    1.43    also have "a * ... = a * x + a * - y" 
    1.44      by (simp only: real_add_mult_distrib2)
    1.45    also have "... = a * x - a * y"   
    1.46 -    by (simp add: real_minus_mult_eq2 [RS sym] real_minus_mult_eq1)
    1.47 +    by simp;
    1.48    finally show ?thesis .
    1.49  qed
    1.50  
     2.1 --- a/src/HOL/Real/Hyperreal/HyperDef.ML	Wed Jun 07 12:07:07 2000 +0200
     2.2 +++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Wed Jun 07 12:14:18 2000 +0200
     2.3 @@ -587,29 +587,29 @@
     2.4  Goal "-(x * y) = -x * (y::hypreal)";
     2.5  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
     2.6  by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
     2.7 -by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
     2.8 -    hypreal_mult,real_minus_mult_eq1] 
     2.9 -      @ real_mult_ac @ real_add_ac));
    2.10 +by (auto_tac (claset(),
    2.11 +	      simpset() addsimps [hypreal_minus, hypreal_mult] 
    2.12 +                                 @ real_mult_ac @ real_add_ac));
    2.13  qed "hypreal_minus_mult_eq1";
    2.14  
    2.15  Goal "-(x * y) = (x::hypreal) * -y";
    2.16  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
    2.17  by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
    2.18  by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
    2.19 -   hypreal_mult,real_minus_mult_eq2] 
    2.20 -    @ real_mult_ac @ real_add_ac));
    2.21 +					   hypreal_mult] 
    2.22 +                                           @ real_mult_ac @ real_add_ac));
    2.23  qed "hypreal_minus_mult_eq2";
    2.24  
    2.25  Goal "-x*-y = x*(y::hypreal)";
    2.26  by (full_simp_tac (simpset() addsimps [hypreal_minus_mult_eq2 RS sym,
    2.27 -    hypreal_minus_mult_eq1 RS sym]) 1);
    2.28 +				       hypreal_minus_mult_eq1 RS sym]) 1);
    2.29  qed "hypreal_minus_mult_cancel";
    2.30  
    2.31  Addsimps [hypreal_minus_mult_cancel];
    2.32  
    2.33  Goal "-x*y = (x::hypreal)*-y";
    2.34  by (full_simp_tac (simpset() addsimps [hypreal_minus_mult_eq2 RS sym,
    2.35 -    hypreal_minus_mult_eq1 RS sym]) 1);
    2.36 +				       hypreal_minus_mult_eq1 RS sym]) 1);
    2.37  qed "hypreal_minus_mult_commute";
    2.38  
    2.39  
     3.1 --- a/src/HOL/Real/PNat.ML	Wed Jun 07 12:07:07 2000 +0200
     3.2 +++ b/src/HOL/Real/PNat.ML	Wed Jun 07 12:14:18 2000 +0200
     3.3 @@ -289,7 +289,7 @@
     3.4  qed "Rep_pnat_le_one";
     3.5  
     3.6  Goalw [pnat_less_def]
     3.7 -     "!! (z1::nat). z1 < z2  ==> ? z3. z1 + Rep_pnat z3 = z2";
     3.8 +     "!! (z1::nat). z1 < z2  ==> EX z3. z1 + Rep_pnat z3 = z2";
     3.9  by (dtac less_imp_add_positive 1);
    3.10  by (force_tac (claset() addSIs [Abs_pnat_inverse],
    3.11  	       simpset() addsimps [Collect_pnat_gt_0]) 1);
    3.12 @@ -473,7 +473,7 @@
    3.13  (* ordering on positive naturals in terms of existence of sum *)
    3.14  (* could provide alternative definition -- Gleason *)
    3.15  Goalw [pnat_less_def,pnat_add_def] 
    3.16 -      "(z1::pnat) < z2 = (? z3. z1 + z3 = z2)";
    3.17 +      "(z1::pnat) < z2 = (EX z3. z1 + z3 = z2)";
    3.18  by (rtac iffI 1);
    3.19  by (res_inst_tac [("t","z2")] (Rep_pnat_inverse RS subst) 1);
    3.20  by (dtac lemma_less_ex_sum_Rep_pnat 1);
    3.21 @@ -484,8 +484,8 @@
    3.22                 Rep_pnat_gt_zero] delsimps [add_0_right]));
    3.23  qed "pnat_less_iff";
    3.24  
    3.25 -Goal "(? (x::pnat). z1 + x = z2) | z1 = z2 \
    3.26 -\          |(? x. z2 + x = z1)";
    3.27 +Goal "(EX (x::pnat). z1 + x = z2) | z1 = z2 \
    3.28 +\          |(EX x. z2 + x = z1)";
    3.29  by (cut_facts_tac [pnat_less_linear] 1);
    3.30  by (asm_full_simp_tac (simpset() addsimps [pnat_less_iff]) 1);
    3.31  qed "pnat_linear_Ex_eq";
     4.1 --- a/src/HOL/Real/PRat.ML	Wed Jun 07 12:07:07 2000 +0200
     4.2 +++ b/src/HOL/Real/PRat.ML	Wed Jun 07 12:14:18 2000 +0200
     4.3 @@ -270,11 +270,11 @@
     4.4  by (simp_tac (simpset() addsimps [prat_mult_qinv]) 1);
     4.5  qed "prat_mult_qinv_right";
     4.6  
     4.7 -Goal "? y. (x::prat) * y = prat_of_pnat (Abs_pnat 1)";
     4.8 +Goal "EX y. (x::prat) * y = prat_of_pnat (Abs_pnat 1)";
     4.9  by (fast_tac (claset() addIs [prat_mult_qinv_right]) 1);
    4.10  qed "prat_qinv_ex";
    4.11  
    4.12 -Goal "?! y. (x::prat) * y = prat_of_pnat (Abs_pnat 1)";
    4.13 +Goal "EX! y. (x::prat) * y = prat_of_pnat (Abs_pnat 1)";
    4.14  by (auto_tac (claset() addIs [prat_mult_qinv_right],simpset()));
    4.15  by (dres_inst_tac [("f","%x. ya*x")] arg_cong 1);
    4.16  by (asm_full_simp_tac (simpset() addsimps [prat_mult_assoc RS sym]) 1);
    4.17 @@ -282,7 +282,7 @@
    4.18      prat_mult_1,prat_mult_1_right]) 1);
    4.19  qed "prat_qinv_ex1";
    4.20  
    4.21 -Goal "?! y. y * (x::prat) = prat_of_pnat (Abs_pnat 1)";
    4.22 +Goal "EX! y. y * (x::prat) = prat_of_pnat (Abs_pnat 1)";
    4.23  by (auto_tac (claset() addIs [prat_mult_qinv],simpset()));
    4.24  by (dres_inst_tac [("f","%x. x*ya")] arg_cong 1);
    4.25  by (asm_full_simp_tac (simpset() addsimps [prat_mult_assoc]) 1);
    4.26 @@ -296,7 +296,7 @@
    4.27  by (Blast_tac 1);
    4.28  qed "prat_mult_inv_qinv";
    4.29  
    4.30 -Goal "? y. x = qinv y";
    4.31 +Goal "EX y. x = qinv y";
    4.32  by (cut_inst_tac [("x","x")] prat_qinv_ex 1);
    4.33  by (etac exE 1 THEN dtac prat_mult_inv_qinv 1);
    4.34  by (Fast_tac 1);
    4.35 @@ -386,7 +386,7 @@
    4.36  bind_thm ("prat_less_asym", prat_less_not_sym RS swap);
    4.37  
    4.38  (* half of positive fraction exists- Gleason p. 120- Proposition 9-2.6(i)*)
    4.39 -Goal "!(q::prat). ? x. x + x = q";
    4.40 +Goal "!(q::prat). EX x. x + x = q";
    4.41  by (rtac allI 1);
    4.42  by (res_inst_tac [("z","q")] eq_Abs_prat 1);
    4.43  by (res_inst_tac [("x","Abs_prat (ratrel ^^ {(x, y+y)})")] exI 1);
    4.44 @@ -396,7 +396,7 @@
    4.45                 pnat_add_mult_distrib2]));
    4.46  qed "lemma_prat_dense";
    4.47  
    4.48 -Goal "? (x::prat). x + x = q";
    4.49 +Goal "EX (x::prat). x + x = q";
    4.50  by (res_inst_tac [("z","q")] eq_Abs_prat 1);
    4.51  by (res_inst_tac [("x","Abs_prat (ratrel ^^ {(x, y+y)})")] exI 1);
    4.52  by (auto_tac (claset(),simpset() addsimps 
    4.53 @@ -407,7 +407,7 @@
    4.54  (* there exists a number between any two positive fractions *)
    4.55  (* Gleason p. 120- Proposition 9-2.6(iv) *)
    4.56  Goalw [prat_less_def] 
    4.57 -      "!! (q1::prat). q1 < q2 ==> ? x. q1 < x & x < q2";
    4.58 +      "!! (q1::prat). q1 < q2 ==> EX x. q1 < x & x < q2";
    4.59  by (auto_tac (claset() addIs [lemma_prat_dense],simpset()));
    4.60  by (res_inst_tac [("x","T")] (lemma_prat_dense RS allE) 1);
    4.61  by (etac exE 1);
    4.62 @@ -442,7 +442,7 @@
    4.63  qed "prat_mult_left_less2_mono1";
    4.64  
    4.65  (* there is no smallest positive fraction *)
    4.66 -Goalw [prat_less_def] "? (x::prat). x < y";
    4.67 +Goalw [prat_less_def] "EX (x::prat). x < y";
    4.68  by (cut_facts_tac [lemma_prat_dense] 1);
    4.69  by (Fast_tac 1);
    4.70  qed "qless_Ex";
    4.71 @@ -765,7 +765,7 @@
    4.72  (*** of preal type as defined using Dedekind Sections in PReal  ***)
    4.73  (*** Show that exists positive real `one' ***)
    4.74  
    4.75 -Goal "? q. q: {x::prat. x < prat_of_pnat (Abs_pnat 1)}";
    4.76 +Goal "EX q. q: {x::prat. x < prat_of_pnat (Abs_pnat 1)}";
    4.77  by (fast_tac (claset() addIs [prat_less_qinv_2_1]) 1);
    4.78  qed "lemma_prat_less_1_memEx";
    4.79  
    4.80 @@ -781,7 +781,7 @@
    4.81  qed "empty_set_psubset_lemma_prat_less_1_set";
    4.82  
    4.83  (*** exists rational not in set --- prat_of_pnat (Abs_pnat 1) itself ***)
    4.84 -Goal "? q. q ~: {x::prat. x < prat_of_pnat (Abs_pnat 1)}";
    4.85 +Goal "EX q. q ~: {x::prat. x < prat_of_pnat (Abs_pnat 1)}";
    4.86  by (res_inst_tac [("x","prat_of_pnat (Abs_pnat 1)")] exI 1);
    4.87  by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
    4.88  qed "lemma_prat_less_1_not_memEx";
    4.89 @@ -803,7 +803,7 @@
    4.90  Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} : {A. {} < A & \
    4.91  \               A < UNIV & \
    4.92  \               (!y: A. ((!z. z < y --> z: A) & \
    4.93 -\               (? u: A. y < u)))}";
    4.94 +\               (EX u: A. y < u)))}";
    4.95  by (auto_tac (claset() addDs [prat_less_trans],
    4.96      simpset() addsimps [empty_set_psubset_lemma_prat_less_1_set,
    4.97                         lemma_prat_less_1_set_psubset_rat_set]));
     5.1 --- a/src/HOL/Real/PReal.ML	Wed Jun 07 12:07:07 2000 +0200
     5.2 +++ b/src/HOL/Real/PReal.ML	Wed Jun 07 12:14:18 2000 +0200
     5.3 @@ -44,7 +44,7 @@
     5.4  by (rtac (Rep_preal RS preal_psubset_empty) 1);
     5.5  qed "Rep_preal_psubset_empty";
     5.6  
     5.7 -Goal "? x. x: Rep_preal X";
     5.8 +Goal "EX x. x: Rep_preal X";
     5.9  by (cut_inst_tac [("x","X")]  Rep_preal_psubset_empty 1);
    5.10  by (auto_tac (claset() addIs [(equals0I RS sym)],
    5.11                simpset() addsimps [psubset_def]));
    5.12 @@ -52,22 +52,22 @@
    5.13  
    5.14  Goalw [preal_def] 
    5.15        "[| {} < A; A < UNIV; \
    5.16 -\              (!y: A. ((!z. z < y --> z: A) & \
    5.17 -\                        (? u: A. y < u))) |] ==> A : preal";
    5.18 +\              (ALL y: A. ((ALL z. z < y --> z: A) & \
    5.19 +\                        (EX u: A. y < u))) |] ==> A : preal";
    5.20  by (Fast_tac 1);
    5.21  qed "prealI1";
    5.22      
    5.23  Goalw [preal_def] 
    5.24        "[| {} < A; A < UNIV; \
    5.25 -\              !y: A. (!z. z < y --> z: A); \
    5.26 -\              !y: A. (? u: A. y < u) |] ==> A : preal";
    5.27 +\              ALL y: A. (ALL z. z < y --> z: A); \
    5.28 +\              ALL y: A. (EX u: A. y < u) |] ==> A : preal";
    5.29  by (Best_tac 1);
    5.30  qed "prealI2";
    5.31  
    5.32  Goalw [preal_def] 
    5.33        "A : preal ==> {} < A & A < UNIV & \
    5.34 -\                         (!y: A. ((!z. z < y --> z: A) & \
    5.35 -\                                  (? u: A. y < u)))";
    5.36 +\                         (ALL y: A. ((ALL z. z < y --> z: A) & \
    5.37 +\                                  (EX u: A. y < u)))";
    5.38  by (Fast_tac 1);
    5.39  qed "prealE_lemma";
    5.40  
    5.41 @@ -85,11 +85,11 @@
    5.42  by (Fast_tac 1);
    5.43  qed "prealE_lemma2";
    5.44  
    5.45 -Goalw [preal_def] "A : preal ==> !y: A. (!z. z < y --> z: A)";
    5.46 +Goalw [preal_def] "A : preal ==> ALL y: A. (ALL z. z < y --> z: A)";
    5.47  by (Fast_tac 1);
    5.48  qed "prealE_lemma3";
    5.49  
    5.50 -Goal "[| A : preal; y: A |] ==> (!z. z < y --> z: A)";
    5.51 +Goal "[| A : preal; y: A |] ==> (ALL z. z < y --> z: A)";
    5.52  by (fast_tac (claset() addSDs [prealE_lemma3]) 1);
    5.53  qed "prealE_lemma3a";
    5.54  
    5.55 @@ -97,15 +97,15 @@
    5.56  by (fast_tac (claset() addSDs [prealE_lemma3a]) 1);
    5.57  qed "prealE_lemma3b";
    5.58  
    5.59 -Goalw [preal_def] "A : preal ==> !y: A. (? u: A. y < u)";
    5.60 +Goalw [preal_def] "A : preal ==> ALL y: A. (EX u: A. y < u)";
    5.61  by (Fast_tac 1);
    5.62  qed "prealE_lemma4";
    5.63  
    5.64 -Goal "[| A : preal; y: A |] ==> ? u: A. y < u";
    5.65 +Goal "[| A : preal; y: A |] ==> EX u: A. y < u";
    5.66  by (fast_tac (claset() addSDs [prealE_lemma4]) 1);
    5.67  qed "prealE_lemma4a";
    5.68  
    5.69 -Goal "? x. x~: Rep_preal X";
    5.70 +Goal "EX x. x~: Rep_preal X";
    5.71  by (cut_inst_tac [("x","X")] Rep_preal 1);
    5.72  by (dtac prealE_lemma2 1);
    5.73  by (rtac ccontr 1);
    5.74 @@ -148,7 +148,7 @@
    5.75  (* A positive fraction not in a positive real is an upper bound *)
    5.76  (* Gleason p. 122 - Remark (1)                                  *)
    5.77  
    5.78 -Goal "x ~: Rep_preal(R) ==> !y: Rep_preal(R). y < x";
    5.79 +Goal "x ~: Rep_preal(R) ==> ALL y: Rep_preal(R). y < x";
    5.80  by (cut_inst_tac [("x1","R")] (Rep_preal RS prealE_lemma) 1);
    5.81  by (auto_tac (claset() addIs [not_less_not_eq_prat_less],simpset()));
    5.82  qed "not_in_preal_ub";
    5.83 @@ -207,13 +207,13 @@
    5.84  (** lemmas for proving positive reals addition set in preal **)
    5.85  
    5.86  (** Part 1 of Dedekind sections def **)
    5.87 -Goal "{} < {w. ? x: Rep_preal R. ? y:Rep_preal S. w = x + y}";
    5.88 +Goal "{} < {w. EX x: Rep_preal R. EX y:Rep_preal S. w = x + y}";
    5.89  by (cut_facts_tac [mem_Rep_preal_Ex,mem_Rep_preal_Ex] 1);
    5.90  by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
    5.91  qed "preal_add_set_not_empty";
    5.92  
    5.93  (** Part 2 of Dedekind sections def **)
    5.94 -Goal "? q. q  ~: {w. ? x: Rep_preal R. ? y:Rep_preal S. w = x + y}";
    5.95 +Goal "EX q. q  ~: {w. EX x: Rep_preal R. EX y:Rep_preal S. w = x + y}";
    5.96  by (cut_inst_tac [("X","R")] not_mem_Rep_preal_Ex 1);
    5.97  by (cut_inst_tac [("X","S")] not_mem_Rep_preal_Ex 1);
    5.98  by (REPEAT(etac exE 1));
    5.99 @@ -224,7 +224,7 @@
   5.100  by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
   5.101  qed "preal_not_mem_add_set_Ex";
   5.102  
   5.103 -Goal "{w. ? x: Rep_preal R. ? y:Rep_preal S. w = x + y} < UNIV";
   5.104 +Goal "{w. EX x: Rep_preal R. EX y:Rep_preal S. w = x + y} < UNIV";
   5.105  by (auto_tac (claset() addSIs [psubsetI],simpset()));
   5.106  by (cut_inst_tac [("R","R"),("S","S")] preal_not_mem_add_set_Ex 1);
   5.107  by (etac exE 1);
   5.108 @@ -233,8 +233,8 @@
   5.109  qed "preal_add_set_not_prat_set";
   5.110  
   5.111  (** Part 3 of Dedekind sections def **)
   5.112 -Goal "!y: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x + y}. \
   5.113 -\         !z. z < y --> z : {w. ? x:Rep_preal R. ? y:Rep_preal S. w = x + y}";
   5.114 +Goal "ALL y: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x + y}. \
   5.115 +\         ALL z. z < y --> z : {w. EX x:Rep_preal R. EX y:Rep_preal S. w = x + y}";
   5.116  by Auto_tac;
   5.117  by (ftac prat_mult_qinv_less_1 1);
   5.118  by (forw_inst_tac [("x","x"),("q2.0","prat_of_pnat (Abs_pnat 1)")] 
   5.119 @@ -250,14 +250,14 @@
   5.120       RS sym,prat_add_assoc RS sym,prat_mult_assoc]));
   5.121  qed "preal_add_set_lemma3";
   5.122  
   5.123 -Goal "!y: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x + y}. \
   5.124 -\         ? u: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x + y}. y < u";
   5.125 +Goal "ALL y: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x + y}. \
   5.126 +\         EX u: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x + y}. y < u";
   5.127  by Auto_tac;
   5.128  by (dtac (Rep_preal RS prealE_lemma4a) 1);
   5.129  by (auto_tac (claset() addIs [prat_add_less2_mono1],simpset()));
   5.130  qed "preal_add_set_lemma4";
   5.131  
   5.132 -Goal "{w. ? x: Rep_preal R. ? y: Rep_preal S. w = x + y} : preal";
   5.133 +Goal "{w. EX x: Rep_preal R. EX y: Rep_preal S. w = x + y} : preal";
   5.134  by (rtac prealI2 1);
   5.135  by (rtac preal_add_set_not_empty 1);
   5.136  by (rtac preal_add_set_not_prat_set 1);
   5.137 @@ -297,13 +297,13 @@
   5.138  (** lemmas for proving positive reals multiplication set in preal **)
   5.139  
   5.140  (** Part 1 of Dedekind sections def **)
   5.141 -Goal "{} < {w. ? x: Rep_preal R. ? y:Rep_preal S. w = x * y}";
   5.142 +Goal "{} < {w. EX x: Rep_preal R. EX y:Rep_preal S. w = x * y}";
   5.143  by (cut_facts_tac [mem_Rep_preal_Ex,mem_Rep_preal_Ex] 1);
   5.144  by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
   5.145  qed "preal_mult_set_not_empty";
   5.146  
   5.147  (** Part 2 of Dedekind sections def **)
   5.148 -Goal "? q. q  ~: {w. ? x: Rep_preal R. ? y:Rep_preal S. w = x * y}";
   5.149 +Goal "EX q. q  ~: {w. EX x: Rep_preal R. EX y:Rep_preal S. w = x * y}";
   5.150  by (cut_inst_tac [("X","R")] not_mem_Rep_preal_Ex 1);
   5.151  by (cut_inst_tac [("X","S")] not_mem_Rep_preal_Ex 1);
   5.152  by (REPEAT(etac exE 1));
   5.153 @@ -314,7 +314,7 @@
   5.154  by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
   5.155  qed "preal_not_mem_mult_set_Ex";
   5.156  
   5.157 -Goal "{w. ? x: Rep_preal R. ? y:Rep_preal S. w = x * y} < UNIV";
   5.158 +Goal "{w. EX x: Rep_preal R. EX y:Rep_preal S. w = x * y} < UNIV";
   5.159  by (auto_tac (claset() addSIs [psubsetI],simpset()));
   5.160  by (cut_inst_tac [("R","R"),("S","S")] preal_not_mem_mult_set_Ex 1);
   5.161  by (etac exE 1);
   5.162 @@ -323,8 +323,8 @@
   5.163  qed "preal_mult_set_not_prat_set";
   5.164  
   5.165  (** Part 3 of Dedekind sections def **)
   5.166 -Goal "!y: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x * y}. \
   5.167 -\         !z. z < y --> z : {w. ? x:Rep_preal R. ? y:Rep_preal S. w = x * y}";
   5.168 +Goal "ALL y: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x * y}. \
   5.169 +\         ALL z. z < y --> z : {w. EX x:Rep_preal R. EX y:Rep_preal S. w = x * y}";
   5.170  by Auto_tac;
   5.171  by (forw_inst_tac [("x","qinv(ya)"),("q1.0","z")] 
   5.172      prat_mult_left_less2_mono1 1);
   5.173 @@ -335,14 +335,14 @@
   5.174  by (auto_tac (claset(),simpset() addsimps [prat_mult_assoc]));
   5.175  qed "preal_mult_set_lemma3";
   5.176  
   5.177 -Goal "!y: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x * y}. \
   5.178 -\         ? u: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x * y}. y < u";
   5.179 +Goal "ALL y: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x * y}. \
   5.180 +\         EX u: {w. EX x: Rep_preal R. EX y: Rep_preal S. w = x * y}. y < u";
   5.181  by Auto_tac;
   5.182  by (dtac (Rep_preal RS prealE_lemma4a) 1);
   5.183  by (auto_tac (claset() addIs [prat_mult_less2_mono1],simpset()));
   5.184  qed "preal_mult_set_lemma4";
   5.185  
   5.186 -Goal "{w. ? x: Rep_preal R. ? y: Rep_preal S. w = x * y} : preal";
   5.187 +Goal "{w. EX x: Rep_preal R. EX y: Rep_preal S. w = x * y} : preal";
   5.188  by (rtac prealI2 1);
   5.189  by (rtac preal_mult_set_not_empty 1);
   5.190  by (rtac preal_mult_set_not_prat_set 1);
   5.191 @@ -410,39 +410,39 @@
   5.192   (** lemmas **)
   5.193  Goalw [preal_add_def] 
   5.194        "z: Rep_preal(R+S) ==> \
   5.195 -\           ? x: Rep_preal(R). ? y: Rep_preal(S). z = x + y";
   5.196 +\           EX x: Rep_preal(R). EX y: Rep_preal(S). z = x + y";
   5.197  by (dtac (preal_mem_add_set RS Abs_preal_inverse RS subst) 1);
   5.198  by (Fast_tac 1);
   5.199  qed "mem_Rep_preal_addD";
   5.200  
   5.201  Goalw [preal_add_def] 
   5.202 -      "? x: Rep_preal(R). ? y: Rep_preal(S). z = x + y \
   5.203 +      "EX x: Rep_preal(R). EX y: Rep_preal(S). z = x + y \
   5.204  \      ==> z: Rep_preal(R+S)";
   5.205  by (rtac (preal_mem_add_set RS Abs_preal_inverse RS ssubst) 1);
   5.206  by (Fast_tac 1);
   5.207  qed "mem_Rep_preal_addI";
   5.208  
   5.209 -Goal " z: Rep_preal(R+S) = (? x: Rep_preal(R). \
   5.210 -\                                 ? y: Rep_preal(S). z = x + y)";
   5.211 +Goal " z: Rep_preal(R+S) = (EX x: Rep_preal(R). \
   5.212 +\                                 EX y: Rep_preal(S). z = x + y)";
   5.213  by (fast_tac (claset() addSIs [mem_Rep_preal_addD,mem_Rep_preal_addI]) 1);
   5.214  qed "mem_Rep_preal_add_iff";
   5.215  
   5.216  Goalw [preal_mult_def] 
   5.217        "z: Rep_preal(R*S) ==> \
   5.218 -\           ? x: Rep_preal(R). ? y: Rep_preal(S). z = x * y";
   5.219 +\           EX x: Rep_preal(R). EX y: Rep_preal(S). z = x * y";
   5.220  by (dtac (preal_mem_mult_set RS Abs_preal_inverse RS subst) 1);
   5.221  by (Fast_tac 1);
   5.222  qed "mem_Rep_preal_multD";
   5.223  
   5.224  Goalw [preal_mult_def] 
   5.225 -      "? x: Rep_preal(R). ? y: Rep_preal(S). z = x * y \
   5.226 +      "EX x: Rep_preal(R). EX y: Rep_preal(S). z = x * y \
   5.227  \      ==> z: Rep_preal(R*S)";
   5.228  by (rtac (preal_mem_mult_set RS Abs_preal_inverse RS ssubst) 1);
   5.229  by (Fast_tac 1);
   5.230  qed "mem_Rep_preal_multI";
   5.231  
   5.232 -Goal " z: Rep_preal(R*S) = (? x: Rep_preal(R). \
   5.233 -\                                 ? y: Rep_preal(S). z = x * y)";
   5.234 +Goal " z: Rep_preal(R*S) = (EX x: Rep_preal(R). \
   5.235 +\                                 EX y: Rep_preal(S). z = x * y)";
   5.236  by (fast_tac (claset() addSIs [mem_Rep_preal_multD,mem_Rep_preal_multI]) 1);
   5.237  qed "mem_Rep_preal_mult_iff";
   5.238  
   5.239 @@ -507,13 +507,13 @@
   5.240  (*** Prove existence of inverse ***)
   5.241  (*** Inverse is a positive real ***)
   5.242  
   5.243 -Goal "? y. qinv(y) ~:  Rep_preal X";
   5.244 +Goal "EX y. qinv(y) ~:  Rep_preal X";
   5.245  by (cut_inst_tac [("X","X")] not_mem_Rep_preal_Ex 1);
   5.246  by (etac exE 1 THEN cut_inst_tac [("x","x")] prat_as_inverse_ex 1);
   5.247  by Auto_tac;
   5.248  qed "qinv_not_mem_Rep_preal_Ex";
   5.249  
   5.250 -Goal "? q. q: {x. ? y. x < y & qinv y ~:  Rep_preal A}";
   5.251 +Goal "EX q. q: {x. EX y. x < y & qinv y ~:  Rep_preal A}";
   5.252  by (cut_inst_tac [("X","A")] qinv_not_mem_Rep_preal_Ex 1);
   5.253  by Auto_tac;
   5.254  by (cut_inst_tac [("y","y")] qless_Ex 1);
   5.255 @@ -521,19 +521,19 @@
   5.256  qed "lemma_preal_mem_inv_set_ex";
   5.257  
   5.258  (** Part 1 of Dedekind sections def **)
   5.259 -Goal "{} < {x. ? y. x < y & qinv y ~:  Rep_preal A}";
   5.260 +Goal "{} < {x. EX y. x < y & qinv y ~:  Rep_preal A}";
   5.261  by (cut_facts_tac [lemma_preal_mem_inv_set_ex] 1);
   5.262  by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
   5.263  qed "preal_inv_set_not_empty";
   5.264  
   5.265  (** Part 2 of Dedekind sections def **)
   5.266 -Goal "? y. qinv(y) :  Rep_preal X";
   5.267 +Goal "EX y. qinv(y) :  Rep_preal X";
   5.268  by (cut_inst_tac [("X","X")] mem_Rep_preal_Ex 1);
   5.269  by (etac exE 1 THEN cut_inst_tac [("x","x")] prat_as_inverse_ex 1);
   5.270  by Auto_tac;
   5.271  qed "qinv_mem_Rep_preal_Ex";
   5.272  
   5.273 -Goal "? x. x ~: {x. ? y. x < y & qinv y ~:  Rep_preal A}";
   5.274 +Goal "EX x. x ~: {x. EX y. x < y & qinv y ~:  Rep_preal A}";
   5.275  by (rtac ccontr 1);
   5.276  by (cut_inst_tac [("X","A")] qinv_mem_Rep_preal_Ex 1);
   5.277  by Auto_tac;
   5.278 @@ -544,7 +544,7 @@
   5.279  by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
   5.280  qed "preal_not_mem_inv_set_Ex";
   5.281  
   5.282 -Goal "{x. ? y. x < y & qinv y ~:  Rep_preal A} < UNIV";
   5.283 +Goal "{x. EX y. x < y & qinv y ~:  Rep_preal A} < UNIV";
   5.284  by (auto_tac (claset() addSIs [psubsetI],simpset()));
   5.285  by (cut_inst_tac [("A","A")]  preal_not_mem_inv_set_Ex 1);
   5.286  by (etac exE 1);
   5.287 @@ -553,19 +553,19 @@
   5.288  qed "preal_inv_set_not_prat_set";
   5.289  
   5.290  (** Part 3 of Dedekind sections def **)
   5.291 -Goal "! y: {x. ? y. x < y & qinv y ~: Rep_preal A}. \
   5.292 - \      !z. z < y --> z : {x. ? y. x < y & qinv y ~: Rep_preal A}";
   5.293 +Goal "ALL y: {x. EX y. x < y & qinv y ~: Rep_preal A}. \
   5.294 + \      ALL z. z < y --> z : {x. EX y. x < y & qinv y ~: Rep_preal A}";
   5.295  by Auto_tac;
   5.296  by (res_inst_tac [("x","ya")] exI 1);
   5.297  by (auto_tac (claset() addIs [prat_less_trans],simpset()));
   5.298  qed "preal_inv_set_lemma3";
   5.299  
   5.300 -Goal "! y: {x. ? y. x < y & qinv y ~: Rep_preal A}. \
   5.301 -\       Bex {x. ? y. x < y & qinv y ~: Rep_preal A} (op < y)";
   5.302 +Goal "ALL y: {x. EX y. x < y & qinv y ~: Rep_preal A}. \
   5.303 +\       Bex {x. EX y. x < y & qinv y ~: Rep_preal A} (op < y)";
   5.304  by (blast_tac (claset() addDs [prat_dense]) 1);
   5.305  qed "preal_inv_set_lemma4";
   5.306  
   5.307 -Goal "{x. ? y. x < y & qinv(y) ~: Rep_preal(A)} : preal";
   5.308 +Goal "{x. EX y. x < y & qinv(y) ~: Rep_preal(A)} : preal";
   5.309  by (rtac prealI2 1);
   5.310  by (rtac preal_inv_set_not_empty 1);
   5.311  by (rtac preal_inv_set_not_prat_set 1);
   5.312 @@ -585,8 +585,8 @@
   5.313  qed "preal_mem_mult_invD";
   5.314  
   5.315  (*** Gleason's Lemma 9-3.4 p 122 ***)
   5.316 -Goal "! xa : Rep_preal(A). xa + x : Rep_preal(A) ==> \
   5.317 -\            ? xb : Rep_preal(A). xb + (prat_of_pnat p)*x : Rep_preal(A)";
   5.318 +Goal "ALL xa : Rep_preal(A). xa + x : Rep_preal(A) ==> \
   5.319 +\            EX xb : Rep_preal(A). xb + (prat_of_pnat p)*x : Rep_preal(A)";
   5.320  by (cut_facts_tac [mem_Rep_preal_Ex] 1);
   5.321  by (res_inst_tac [("n","p")] pnat_induct 1);
   5.322  by (auto_tac (claset(),simpset() addsimps [pnat_one_def,
   5.323 @@ -603,7 +603,7 @@
   5.324      simpset() addsimps [prat_mult,pre_lemma_gleason9_34b,pnat_mult_assoc]));
   5.325  qed "lemma1b_gleason9_34";
   5.326  
   5.327 -Goal "! xa : Rep_preal(A). xa + x : Rep_preal(A) ==> False";
   5.328 +Goal "ALL xa : Rep_preal(A). xa + x : Rep_preal(A) ==> False";
   5.329  by (cut_inst_tac [("X","A")] not_mem_Rep_preal_Ex 1);
   5.330  by (etac exE 1);
   5.331  by (dtac not_in_preal_ub 1);
   5.332 @@ -618,7 +618,7 @@
   5.333      simpset() addsimps [prat_of_pnat_def]));
   5.334  qed "lemma_gleason9_34a";
   5.335  
   5.336 -Goal "? r: Rep_preal(R). r + x ~: Rep_preal(R)";
   5.337 +Goal "EX r: Rep_preal(R). r + x ~: Rep_preal(R)";
   5.338  by (rtac ccontr 1);
   5.339  by (blast_tac (claset() addIs [lemma_gleason9_34a]) 1);
   5.340  qed "lemma_gleason9_34";
   5.341 @@ -639,7 +639,7 @@
   5.342  (******)
   5.343  
   5.344  (*** FIXME: long! ***)
   5.345 -Goal "prat_of_pnat 1p < x ==> ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
   5.346 +Goal "prat_of_pnat 1p < x ==> EX r: Rep_preal(A). r*x ~: Rep_preal(A)";
   5.347  by (res_inst_tac [("X1","A")] (mem_Rep_preal_Ex RS exE) 1);
   5.348  by (res_inst_tac [("Q","xa*x : Rep_preal(A)")] (excluded_middle RS disjE) 1);
   5.349  by (Fast_tac 1);
   5.350 @@ -663,7 +663,7 @@
   5.351  qed "lemma_gleason9_36";
   5.352  
   5.353  Goal "prat_of_pnat (Abs_pnat 1) < x ==> \
   5.354 -\     ? r: Rep_preal(A). r*x ~: Rep_preal(A)";
   5.355 +\     EX r: Rep_preal(A). r*x ~: Rep_preal(A)";
   5.356  by (rtac lemma_gleason9_36 1);
   5.357  by (asm_simp_tac (simpset() addsimps [pnat_one_def]) 1);
   5.358  qed "lemma_gleason9_36a";
   5.359 @@ -813,7 +813,7 @@
   5.360  (**** Define the D required and show that it is a positive real ****)
   5.361  
   5.362  (* useful lemmas - proved elsewhere? *)
   5.363 -Goalw [psubset_def] "A < B ==> ? x. x ~: A & x : B";
   5.364 +Goalw [psubset_def] "A < B ==> EX x. x ~: A & x : B";
   5.365  by (etac conjE 1);
   5.366  by (etac swap 1);
   5.367  by (etac equalityI 1);
   5.368 @@ -843,7 +843,7 @@
   5.369  (** Part 1 of Dedekind sections def **)
   5.370  Goalw [preal_less_def]
   5.371       "A < B ==> \
   5.372 -\     ? q. q : {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
   5.373 +\     EX q. q : {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
   5.374  by (EVERY1[dtac lemma_psubset_mem, etac exE, etac conjE]);
   5.375  by (dres_inst_tac [("x1","B")] (Rep_preal RS prealE_lemma4a) 1);
   5.376  by (auto_tac (claset(),simpset() addsimps [prat_less_def]));
   5.377 @@ -851,13 +851,13 @@
   5.378  
   5.379  Goal
   5.380       "A < B ==> \
   5.381 -\       {} < {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
   5.382 +\       {} < {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
   5.383  by (dtac lemma_ex_mem_less_left_add1 1);
   5.384  by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
   5.385  qed "preal_less_set_not_empty";
   5.386  
   5.387  (** Part 2 of Dedekind sections def **)
   5.388 -Goal "? q. q ~: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
   5.389 +Goal "EX q. q ~: {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
   5.390  by (cut_inst_tac [("X","B")] not_mem_Rep_preal_Ex 1);
   5.391  by (etac exE 1);
   5.392  by (res_inst_tac [("x","x")] exI 1);
   5.393 @@ -866,7 +866,7 @@
   5.394  by (auto_tac (claset() addDs [Rep_preal RS prealE_lemma3b],simpset()));
   5.395  qed "lemma_ex_not_mem_less_left_add1";
   5.396  
   5.397 -Goal "{d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} < UNIV";
   5.398 +Goal "{d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} < UNIV";
   5.399  by (auto_tac (claset() addSIs [psubsetI],simpset()));
   5.400  by (cut_inst_tac [("A","A"),("B","B")] lemma_ex_not_mem_less_left_add1 1);
   5.401  by (etac exE 1);
   5.402 @@ -875,16 +875,16 @@
   5.403  qed "preal_less_set_not_prat_set";
   5.404  
   5.405  (** Part 3 of Dedekind sections def **)
   5.406 -Goal "A < B ==> ! y: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
   5.407 - \      !z. z < y --> z : {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
   5.408 +Goal "A < B ==> ALL y: {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
   5.409 + \      ALL z. z < y --> z : {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
   5.410  by Auto_tac;
   5.411  by (dres_inst_tac [("x","n")] prat_add_less2_mono2 1);
   5.412  by (dtac (Rep_preal RS prealE_lemma3b) 1);
   5.413  by Auto_tac;
   5.414  qed "preal_less_set_lemma3";
   5.415  
   5.416 -Goal "A < B ==> ! y: {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
   5.417 -\       Bex {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} (op < y)";
   5.418 +Goal "A < B ==> ALL y: {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
   5.419 +\       Bex {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} (op < y)";
   5.420  by Auto_tac;
   5.421  by (dtac (Rep_preal RS prealE_lemma4a) 1);
   5.422  by (auto_tac (claset(),simpset() addsimps [prat_less_def,prat_add_assoc]));
   5.423 @@ -892,7 +892,7 @@
   5.424  
   5.425  Goal 
   5.426       "!! (A::preal). A < B ==> \
   5.427 -\     {d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}: preal";
   5.428 +\     {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}: preal";
   5.429  by (rtac prealI2 1);
   5.430  by (rtac preal_less_set_not_empty 1);
   5.431  by (rtac preal_less_set_not_prat_set 2);
   5.432 @@ -904,7 +904,7 @@
   5.433  (** proving that A + D <= B **)
   5.434  Goalw [preal_le_def] 
   5.435         "!! (A::preal). A < B ==> \
   5.436 -\         A + Abs_preal({d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}) <= B";
   5.437 +\         A + Abs_preal({d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}) <= B";
   5.438  by (rtac subsetI 1);
   5.439  by (dtac mem_Rep_preal_addD 1);
   5.440  by (auto_tac (claset(),simpset() addsimps [
   5.441 @@ -918,14 +918,14 @@
   5.442  
   5.443  (** proving that B <= A + D  --- trickier **)
   5.444  (** lemma **)
   5.445 -Goal "x : Rep_preal(B) ==> ? e. x + e : Rep_preal(B)";
   5.446 +Goal "x : Rep_preal(B) ==> EX e. x + e : Rep_preal(B)";
   5.447  by (dtac (Rep_preal RS prealE_lemma4a) 1);
   5.448  by (auto_tac (claset(),simpset() addsimps [prat_less_def]));
   5.449  qed "lemma_sum_mem_Rep_preal_ex";
   5.450  
   5.451  Goalw [preal_le_def] 
   5.452         "!! (A::preal). A < B ==> \
   5.453 -\         B <= A + Abs_preal({d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)})";
   5.454 +\         B <= A + Abs_preal({d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)})";
   5.455  by (rtac subsetI 1);
   5.456  by (res_inst_tac [("Q","x: Rep_preal(A)")] (excluded_middle RS disjE) 1);
   5.457  by (rtac mem_Rep_preal_addI 1);
   5.458 @@ -945,12 +945,12 @@
   5.459  
   5.460  (*** required proof ***)
   5.461  Goal "!! (A::preal). A < B ==> \
   5.462 -\         A + Abs_preal({d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}) = B";
   5.463 +\         A + Abs_preal({d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}) = B";
   5.464  by (blast_tac (claset() addIs [preal_le_anti_sym,
   5.465                  preal_less_add_left_subsetI,preal_less_add_left_subsetI2]) 1);
   5.466  qed "preal_less_add_left";
   5.467  
   5.468 -Goal "!! (A::preal). A < B ==> ? D. A + D = B";
   5.469 +Goal "!! (A::preal). A < B ==> EX D. A + D = B";
   5.470  by (fast_tac (claset() addDs [preal_less_add_left]) 1);
   5.471  qed "preal_less_add_left_Ex";        
   5.472  
   5.473 @@ -1070,23 +1070,23 @@
   5.474  (*** Completeness of preal ***)
   5.475  
   5.476  (*** prove that supremum is a cut ***)
   5.477 -Goal "? (X::preal). X: P ==> \
   5.478 -\         ? q.  q: {w. ? X. X : P & w : Rep_preal X}";
   5.479 +Goal "EX (X::preal). X: P ==> \
   5.480 +\         EX q.  q: {w. EX X. X : P & w : Rep_preal X}";
   5.481  by Safe_tac;
   5.482  by (cut_inst_tac [("X","X")] mem_Rep_preal_Ex 1);
   5.483  by Auto_tac;
   5.484  qed "preal_sup_mem_Ex";
   5.485  
   5.486  (** Part 1 of Dedekind def **)
   5.487 -Goal "? (X::preal). X: P ==> \
   5.488 -\         {} < {w. ? X : P. w : Rep_preal X}";
   5.489 +Goal "EX (X::preal). X: P ==> \
   5.490 +\         {} < {w. EX X : P. w : Rep_preal X}";
   5.491  by (dtac preal_sup_mem_Ex 1);
   5.492  by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
   5.493  qed "preal_sup_set_not_empty";
   5.494  
   5.495  (** Part 2 of Dedekind sections def **) 
   5.496 -Goalw [preal_less_def] "? Y. (! X: P. X < Y)  \             
   5.497 -\         ==> ? q. q ~: {w. ? X. X: P & w: Rep_preal(X)}"; (**)
   5.498 +Goalw [preal_less_def] "EX Y. (ALL X: P. X < Y)  \             
   5.499 +\         ==> EX q. q ~: {w. EX X. X: P & w: Rep_preal(X)}"; (**)
   5.500  by (auto_tac (claset(),simpset() addsimps [psubset_def]));
   5.501  by (cut_inst_tac [("X","Y")] not_mem_Rep_preal_Ex 1);
   5.502  by (etac exE 1);
   5.503 @@ -1094,8 +1094,8 @@
   5.504  by (auto_tac (claset() addSDs [bspec],simpset()));
   5.505  qed "preal_sup_not_mem_Ex";
   5.506  
   5.507 -Goalw [preal_le_def] "? Y. (! X: P. X <= Y)  \
   5.508 -\         ==> ? q. q ~: {w. ? X. X: P & w: Rep_preal(X)}";
   5.509 +Goalw [preal_le_def] "EX Y. (ALL X: P. X <= Y)  \
   5.510 +\         ==> EX q. q ~: {w. EX X. X: P & w: Rep_preal(X)}";
   5.511  by (Step_tac 1);
   5.512  by (cut_inst_tac [("X","Y")] not_mem_Rep_preal_Ex 1);
   5.513  by (etac exE 1);
   5.514 @@ -1103,16 +1103,16 @@
   5.515  by (auto_tac (claset() addSDs [bspec],simpset()));
   5.516  qed "preal_sup_not_mem_Ex1";
   5.517  
   5.518 -Goal "? Y. (! X: P. X < Y)  \                                    
   5.519 -\         ==> {w. ? X: P. w: Rep_preal(X)} < UNIV";       (**)
   5.520 +Goal "EX Y. (ALL X: P. X < Y)  \                                    
   5.521 +\         ==> {w. EX X: P. w: Rep_preal(X)} < UNIV";       (**)
   5.522  by (dtac preal_sup_not_mem_Ex 1);
   5.523  by (auto_tac (claset() addSIs [psubsetI],simpset()));
   5.524  by (eres_inst_tac [("c","q")] equalityCE 1);
   5.525  by Auto_tac;
   5.526  qed "preal_sup_set_not_prat_set";
   5.527  
   5.528 -Goal "? Y. (! X: P. X <= Y)  \
   5.529 -\         ==> {w. ? X: P. w: Rep_preal(X)} < UNIV";
   5.530 +Goal "EX Y. (ALL X: P. X <= Y)  \
   5.531 +\         ==> {w. EX X: P. w: Rep_preal(X)} < UNIV";
   5.532  by (dtac preal_sup_not_mem_Ex1 1);
   5.533  by (auto_tac (claset() addSIs [psubsetI],simpset()));
   5.534  by (eres_inst_tac [("c","q")] equalityCE 1);
   5.535 @@ -1120,32 +1120,32 @@
   5.536  qed "preal_sup_set_not_prat_set1";
   5.537  
   5.538  (** Part 3 of Dedekind sections def **)
   5.539 -Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \              
   5.540 -\         ==> ! y: {w. ? X: P. w: Rep_preal X}. \
   5.541 -\             !z. z < y --> z: {w. ? X: P. w: Rep_preal X}";         (**)
   5.542 +Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X < Y) |] \              
   5.543 +\         ==> ALL y: {w. EX X: P. w: Rep_preal X}. \
   5.544 +\             ALL z. z < y --> z: {w. EX X: P. w: Rep_preal X}";         (**)
   5.545  by (auto_tac(claset() addEs [Rep_preal RS prealE_lemma3b],simpset()));
   5.546  qed "preal_sup_set_lemma3";
   5.547  
   5.548 -Goal "[|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
   5.549 -\         ==> ! y: {w. ? X: P. w: Rep_preal X}. \
   5.550 -\             !z. z < y --> z: {w. ? X: P. w: Rep_preal X}";
   5.551 +Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X <= Y) |] \
   5.552 +\         ==> ALL y: {w. EX X: P. w: Rep_preal X}. \
   5.553 +\             ALL z. z < y --> z: {w. EX X: P. w: Rep_preal X}";
   5.554  by (auto_tac(claset() addEs [Rep_preal RS prealE_lemma3b],simpset()));
   5.555  qed "preal_sup_set_lemma3_1";
   5.556  
   5.557 -Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \              
   5.558 -\         ==>  !y: {w. ? X: P. w: Rep_preal X}. \                        
   5.559 -\             Bex {w. ? X: P. w: Rep_preal X} (op < y)";                (**)
   5.560 +Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X < Y) |] \              
   5.561 +\         ==>  ALL y: {w. EX X: P. w: Rep_preal X}. \                        
   5.562 +\             Bex {w. EX X: P. w: Rep_preal X} (op < y)";                (**)
   5.563  by (blast_tac (claset() addDs [(Rep_preal RS prealE_lemma4a)]) 1);
   5.564  qed "preal_sup_set_lemma4";
   5.565  
   5.566 -Goal "[|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
   5.567 -\         ==>  !y: {w. ? X: P. w: Rep_preal X}. \
   5.568 -\             Bex {w. ? X: P. w: Rep_preal X} (op < y)";
   5.569 +Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X <= Y) |] \
   5.570 +\         ==>  ALL y: {w. EX X: P. w: Rep_preal X}. \
   5.571 +\             Bex {w. EX X: P. w: Rep_preal X} (op < y)";
   5.572  by (blast_tac (claset() addDs [(Rep_preal RS prealE_lemma4a)]) 1);
   5.573  qed "preal_sup_set_lemma4_1";
   5.574  
   5.575 -Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \            
   5.576 -\         ==> {w. ? X: P. w: Rep_preal(X)}: preal";                      (**)
   5.577 +Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X < Y) |] \            
   5.578 +\         ==> {w. EX X: P. w: Rep_preal(X)}: preal";                      (**)
   5.579  by (rtac prealI2 1);
   5.580  by (rtac preal_sup_set_not_empty 1);
   5.581  by (rtac preal_sup_set_not_prat_set 2);
   5.582 @@ -1154,8 +1154,8 @@
   5.583  by Auto_tac;
   5.584  qed "preal_sup";
   5.585  
   5.586 -Goal "[|? (X::preal). X: P; ? Y. (! X:P. X <= Y) |] \
   5.587 -\         ==> {w. ? X: P. w: Rep_preal(X)}: preal";
   5.588 +Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X <= Y) |] \
   5.589 +\         ==> {w. EX X: P. w: Rep_preal(X)}: preal";
   5.590  by (rtac prealI2 1);
   5.591  by (rtac preal_sup_set_not_empty 1);
   5.592  by (rtac preal_sup_set_not_prat_set1 2);
   5.593 @@ -1164,27 +1164,27 @@
   5.594  by Auto_tac;
   5.595  qed "preal_sup1";
   5.596  
   5.597 -Goalw [psup_def] "? Y. (! X:P. X < Y) ==> ! x: P. x <= psup P";      (**) 
   5.598 +Goalw [psup_def] "EX Y. (ALL X:P. X < Y) ==> ALL x: P. x <= psup P";      (**) 
   5.599  by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
   5.600  by (rtac (preal_sup RS Abs_preal_inverse RS ssubst) 1);
   5.601  by Auto_tac;
   5.602  qed "preal_psup_leI";
   5.603  
   5.604 -Goalw [psup_def] "? Y. (! X:P. X <= Y) ==> ! x: P. x <= psup P";
   5.605 +Goalw [psup_def] "EX Y. (ALL X:P. X <= Y) ==> ALL x: P. x <= psup P";
   5.606  by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
   5.607  by (rtac (preal_sup1 RS Abs_preal_inverse RS ssubst) 1);
   5.608  by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
   5.609  qed "preal_psup_leI2";
   5.610  
   5.611 -Goal "[| ? Y. (! X:P. X < Y); x : P |] ==> x <= psup P";              (**)
   5.612 +Goal "[| EX Y. (ALL X:P. X < Y); x : P |] ==> x <= psup P";              (**)
   5.613  by (blast_tac (claset() addSDs [preal_psup_leI]) 1);
   5.614  qed "preal_psup_leI2b";
   5.615  
   5.616 -Goal "[| ? Y. (! X:P. X <= Y); x : P |] ==> x <= psup P";
   5.617 +Goal "[| EX Y. (ALL X:P. X <= Y); x : P |] ==> x <= psup P";
   5.618  by (blast_tac (claset() addSDs [preal_psup_leI2]) 1);
   5.619  qed "preal_psup_leI2a";
   5.620  
   5.621 -Goalw [psup_def] "[| ? X. X : P; ! X:P. X < Y |] ==> psup P <= Y";   (**)
   5.622 +Goalw [psup_def] "[| EX X. X : P; ALL X:P. X < Y |] ==> psup P <= Y";   (**)
   5.623  by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
   5.624  by (dtac (([exI,exI] MRS preal_sup) RS Abs_preal_inverse RS subst) 1);
   5.625  by (rotate_tac 1 2);
   5.626 @@ -1192,7 +1192,7 @@
   5.627  by (auto_tac (claset() addSDs [bspec],simpset() addsimps [preal_less_def,psubset_def]));
   5.628  qed "psup_le_ub";
   5.629  
   5.630 -Goalw [psup_def] "[| ? X. X : P; ! X:P. X <= Y |] ==> psup P <= Y";
   5.631 +Goalw [psup_def] "[| EX X. X : P; ALL X:P. X <= Y |] ==> psup P <= Y";
   5.632  by (auto_tac (claset(),simpset() addsimps [preal_le_def]));
   5.633  by (dtac (([exI,exI] MRS preal_sup1) RS Abs_preal_inverse RS subst) 1);
   5.634  by (rotate_tac 1 2);
   5.635 @@ -1202,8 +1202,8 @@
   5.636  qed "psup_le_ub1";
   5.637  
   5.638  (** supremum property **)
   5.639 -Goal "[|? (X::preal). X: P; ? Y. (! X:P. X < Y) |] \                  
   5.640 -\         ==> (!Y. (? X: P. Y < X) = (Y < psup P))";              
   5.641 +Goal "[|EX (X::preal). X: P; EX Y. (ALL X:P. X < Y) |] \                  
   5.642 +\         ==> (ALL Y. (EX X: P. Y < X) = (Y < psup P))";              
   5.643  by (forward_tac [preal_sup RS Abs_preal_inverse] 1);
   5.644  by (Fast_tac 1);
   5.645  by (auto_tac (claset() addSIs [psubsetI],simpset() addsimps [psup_def,preal_less_def]));
     6.1 --- a/src/HOL/Real/RComplete.ML	Wed Jun 07 12:07:07 2000 +0200
     6.2 +++ b/src/HOL/Real/RComplete.ML	Wed Jun 07 12:14:18 2000 +0200
     6.3 @@ -14,16 +14,16 @@
     6.4         previously in Real.ML. 
     6.5   ---------------------------------------------------------*)
     6.6   (*a few lemmas*)
     6.7 -Goal "! x:P. #0 < x ==> \ 
     6.8 -\       ((? x:P. y < x) = (? X. real_of_preal X : P & \
     6.9 +Goal "ALL x:P. #0 < x ==> \ 
    6.10 +\       ((EX x:P. y < x) = (EX X. real_of_preal X : P & \
    6.11  \                          y < real_of_preal X))";
    6.12  by (blast_tac (claset() addSDs [bspec,rename_numerals thy
    6.13  				real_gt_zero_preal_Ex RS iffD1]) 1);
    6.14  qed "real_sup_lemma1";
    6.15  
    6.16 -Goal "[| ! x:P. #0 < x; ? x. x: P; ? y. !x: P. x < y |] \
    6.17 -\         ==> (? X. X: {w. real_of_preal w : P}) & \
    6.18 -\             (? Y. !X: {w. real_of_preal w : P}. X < Y)";
    6.19 +Goal "[| ALL x:P. #0 < x; EX x. x: P; EX y. ALL x: P. x < y |] \
    6.20 +\         ==> (EX X. X: {w. real_of_preal w : P}) & \
    6.21 +\             (EX Y. ALL X: {w. real_of_preal w : P}. X < Y)";
    6.22  by (rtac conjI 1);
    6.23  by (blast_tac (claset() addDs [bspec, rename_numerals thy 
    6.24      real_gt_zero_preal_Ex RS iffD1]) 1);
    6.25 @@ -49,8 +49,8 @@
    6.26   only have one case split 
    6.27  **)
    6.28  
    6.29 -Goal "[| ! x:P. (#0::real) < x; ? x. x: P; ? y. !x: P. x < y |] \
    6.30 -\         ==> (? S. !y. (? x: P. y < x) = (y < S))";
    6.31 +Goal "[| ALL x:P. (#0::real) < x; EX x. x: P; EX y. ALL x: P. x < y |] \
    6.32 +\         ==> (EX S. ALL y. (EX x: P. y < x) = (y < S))";
    6.33  by (res_inst_tac 
    6.34     [("x","real_of_preal (psup({w. real_of_preal w : P}))")] exI 1);
    6.35  by Auto_tac;
    6.36 @@ -128,7 +128,7 @@
    6.37  (*-------------------------------
    6.38      Lemmas
    6.39   -------------------------------*)
    6.40 -Goal "! y : {z. ? x: P. z = x + (-xa) + #1} Int {x. #0 < x}. #0 < y";
    6.41 +Goal "ALL y : {z. EX x: P. z = x + (-xa) + #1} Int {x. #0 < x}. #0 < y";
    6.42  by Auto_tac;
    6.43  qed "real_sup_lemma3";
    6.44   
    6.45 @@ -158,9 +158,9 @@
    6.46  Goal "[| EX X. X: S;  EX Y. isUb (UNIV::real set) S Y |]  \
    6.47  \     ==> EX t. isLub (UNIV :: real set) S t";
    6.48  by (Step_tac 1);
    6.49 -by (subgoal_tac "? u. u: {z. ? x: S. z = x + (-X) + #1} \
    6.50 +by (subgoal_tac "EX u. u: {z. EX x: S. z = x + (-X) + #1} \
    6.51  \                Int {x. #0 < x}" 1);
    6.52 -by (subgoal_tac "isUb (UNIV::real set) ({z. ? x: S. z = x + (-X) + #1} \
    6.53 +by (subgoal_tac "isUb (UNIV::real set) ({z. EX x: S. z = x + (-X) + #1} \
    6.54  \                Int {x. #0 < x})  (Y + (-X) + #1)" 1); 
    6.55  by (cut_inst_tac [("P","S"),("xa","X")] real_sup_lemma3 1);
    6.56  by (EVERY1[forward_tac [exI RSN (3,posreals_complete)], Blast_tac, Blast_tac, 
    6.57 @@ -168,7 +168,7 @@
    6.58  by (res_inst_tac [("x","t + X + (-#1)")] exI 1);
    6.59  by (rtac isLubI2 1);
    6.60  by (rtac setgeI 2 THEN Step_tac 2);
    6.61 -by (subgoal_tac "isUb (UNIV:: real set) ({z. ? x: S. z = x + (-X) + #1} \
    6.62 +by (subgoal_tac "isUb (UNIV:: real set) ({z. EX x: S. z = x + (-X) + #1} \
    6.63  \                Int {x. #0 < x})  (y + (-X) + #1)" 2); 
    6.64  by (dres_inst_tac [("y","(y + (- X) + #1)")] isLub_le_isUb 2 
    6.65        THEN assume_tac 2);
     7.1 --- a/src/HOL/Real/ROOT.ML	Wed Jun 07 12:07:07 2000 +0200
     7.2 +++ b/src/HOL/Real/ROOT.ML	Wed Jun 07 12:14:18 2000 +0200
     7.3 @@ -8,7 +8,5 @@
     7.4  Linear real arithmetic is installed in RealBin.ML.
     7.5  *)
     7.6  
     7.7 -time_use_thy "RealDef";
     7.8 -use          "simproc.ML";
     7.9  time_use_thy "Real";
    7.10  time_use_thy "Hyperreal/HyperDef";
     8.1 --- a/src/HOL/Real/RealAbs.ML	Wed Jun 07 12:07:07 2000 +0200
     8.2 +++ b/src/HOL/Real/RealAbs.ML	Wed Jun 07 12:14:18 2000 +0200
     8.3 @@ -86,26 +86,15 @@
     8.4  by (simp_tac (simpset() addsimps [zero_eq_numeral_0]) 1);
     8.5  qed "abs_ge_minus_self";
     8.6  
     8.7 -(* case splits nightmare *)
     8.8  Goalw [abs_real_def] "abs (x * y) = abs x * abs (y::real)";
     8.9 -by (auto_tac (claset(),
    8.10 -	      simpset() addsimps [real_minus_mult_eq1, real_minus_mult_commute,
    8.11 -				  real_minus_mult_eq2]));
    8.12 -by (blast_tac (claset() addDs [full_rename_numerals thy real_le_mult_order]) 1);
    8.13 -by (auto_tac (claset() addSDs [not_real_leE], simpset()));
    8.14 -by (EVERY1[dtac (full_rename_numerals thy real_mult_le_zero), 
    8.15 -    assume_tac, dtac real_le_anti_sym]);
    8.16 -by (EVERY[dtac (full_rename_numerals thy real_mult_le_zero) 3,
    8.17 -     assume_tac 3, dtac real_le_anti_sym 3]);
    8.18 -by (dtac (full_rename_numerals thy real_mult_less_zero1) 5 THEN assume_tac 5);
    8.19 -by (auto_tac (claset() addDs [real_less_asym,sym],
    8.20 -	      simpset() addsimps [real_minus_mult_eq2 RS sym] @real_mult_ac));
    8.21 +by (auto_tac (claset() addSDs [order_antisym],
    8.22 +	      simpset() addsimps [real_0_le_times_iff]));
    8.23  qed "abs_mult";
    8.24  
    8.25  Goalw [abs_real_def] "x~= (#0::real) ==> abs(rinv(x)) = rinv(abs(x))";
    8.26 -by (auto_tac (claset(), simpset() addsimps [real_le_less] @ 
    8.27 -    (map (full_rename_numerals thy) [real_minus_rinv,
    8.28 -    real_rinv_gt_zero])));
    8.29 +by (auto_tac (claset(), 
    8.30 +              simpset() addsimps [real_le_less] @ 
    8.31 +    (map (full_rename_numerals thy) [real_minus_rinv, real_rinv_gt_zero])));
    8.32  by (etac (full_rename_numerals thy (real_rinv_less_zero 
    8.33      RSN (2,real_less_asym))) 1);
    8.34  by (arith_tac 1);
     9.1 --- a/src/HOL/Real/RealBin.ML	Wed Jun 07 12:07:07 2000 +0200
     9.2 +++ b/src/HOL/Real/RealBin.ML	Wed Jun 07 12:14:18 2000 +0200
     9.3 @@ -13,7 +13,7 @@
     9.4  qed "real_number_of";
     9.5  Addsimps [real_number_of];
     9.6  
     9.7 -Goalw [real_number_of_def] "0r = #0";
     9.8 +Goalw [real_number_of_def] "(0::real) = #0";
     9.9  by (simp_tac (simpset() addsimps [real_of_int_zero RS sym]) 1);
    9.10  qed "zero_eq_numeral_0";
    9.11  
    9.12 @@ -109,14 +109,14 @@
    9.13  
    9.14  Addsimps [le_real_number_of_eq_not_less];
    9.15  
    9.16 -(*** New versions of existing theorems involving 0r, 1r ***)
    9.17 +(*** New versions of existing theorems involving 0, 1r ***)
    9.18  
    9.19  Goal "- #1 = (#-1::real)";
    9.20  by (Simp_tac 1);
    9.21  qed "minus_numeral_one";
    9.22  
    9.23  
    9.24 -(*Maps 0r to #0 and 1r to #1 and -1r to #-1*)
    9.25 +(*Maps 0 to #0 and 1r to #1 and -1r to #-1*)
    9.26  val real_numeral_ss = 
    9.27      HOL_ss addsimps [zero_eq_numeral_0, one_eq_numeral_1, 
    9.28  		     minus_numeral_one];
    9.29 @@ -124,7 +124,7 @@
    9.30  fun rename_numerals thy th = simplify real_numeral_ss (change_theory thy th);
    9.31  
    9.32  
    9.33 -(*Now insert some identities previously stated for 0r and 1r*)
    9.34 +(*Now insert some identities previously stated for 0 and 1r*)
    9.35  
    9.36  (** RealDef & Real **)
    9.37  
    9.38 @@ -136,6 +136,17 @@
    9.39  	   real_mult_minus_1_right, real_mult_minus_1, real_rinv_1,
    9.40  	   real_minus_zero_less_iff]);
    9.41  
    9.42 +AddIffs (map (rename_numerals thy) [real_mult_is_0, real_0_is_mult]);
    9.43 +
    9.44 +bind_thm ("real_0_less_times_iff", 
    9.45 +	  rename_numerals thy real_zero_less_times_iff);
    9.46 +bind_thm ("real_0_le_times_iff", 
    9.47 +	  rename_numerals thy real_zero_le_times_iff);
    9.48 +bind_thm ("real_times_less_0_iff", 
    9.49 +	  rename_numerals thy real_times_less_zero_iff);
    9.50 +bind_thm ("real_times_le_0_iff", 
    9.51 +	  rename_numerals thy real_times_le_zero_iff);
    9.52 +
    9.53  
    9.54  (*Perhaps add some theorems that aren't in the default simpset, as
    9.55    done in Integ/NatBin.ML*)
    9.56 @@ -201,3 +212,27 @@
    9.57      asm_full_simplify real_numeral_ss (change_theory thy th);
    9.58  
    9.59  
    9.60 +(** Simplification of arithmetic when nested to the right **)
    9.61 +
    9.62 +Goal "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::real)";
    9.63 +by Auto_tac; 
    9.64 +qed "real_add_number_of_left";
    9.65 +
    9.66 +Goal "number_of v * (number_of w * z) = (number_of(bin_mult v w) * z::real)";
    9.67 +by (simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
    9.68 +qed "real_mult_number_of_left";
    9.69 +
    9.70 +Goalw [real_diff_def]
    9.71 +    "number_of v + (number_of w - c) = number_of(bin_add v w) - (c::real)";
    9.72 +by (rtac real_add_number_of_left 1);
    9.73 +qed "real_add_number_of_diff1";
    9.74 +
    9.75 +Goal "number_of v + (c - number_of w) = \
    9.76 +\    number_of (bin_add v (bin_minus w)) + (c::real)";
    9.77 +by (stac (diff_real_number_of RS sym) 1);
    9.78 +by Auto_tac;
    9.79 +qed "real_add_number_of_diff2";
    9.80 +
    9.81 +Addsimps [real_add_number_of_left, real_mult_number_of_left,
    9.82 +	  real_add_number_of_diff1, real_add_number_of_diff2]; 
    9.83 +
    10.1 --- a/src/HOL/Real/RealDef.ML	Wed Jun 07 12:07:07 2000 +0200
    10.2 +++ b/src/HOL/Real/RealDef.ML	Wed Jun 07 12:14:18 2000 +0200
    10.3 @@ -135,13 +135,13 @@
    10.4  by (asm_full_simp_tac (simpset() addsimps [real_minus_minus]) 1);
    10.5  qed "inj_real_minus";
    10.6  
    10.7 -Goalw [real_zero_def] "-0r = 0r";
    10.8 +Goalw [real_zero_def] "-0 = (0::real)";
    10.9  by (simp_tac (simpset() addsimps [real_minus]) 1);
   10.10  qed "real_minus_zero";
   10.11  
   10.12  Addsimps [real_minus_zero];
   10.13  
   10.14 -Goal "(-x = 0r) = (x = 0r)"; 
   10.15 +Goal "(-x = 0) = (x = (0::real))"; 
   10.16  by (res_inst_tac [("z","x")] eq_Abs_real 1);
   10.17  by (auto_tac (claset(),
   10.18  	      simpset() addsimps [real_zero_def, real_minus] @ preal_add_ac));
   10.19 @@ -149,10 +149,6 @@
   10.20  
   10.21  Addsimps [real_minus_zero_iff];
   10.22  
   10.23 -Goal "(-x ~= 0r) = (x ~= 0r)"; 
   10.24 -by Auto_tac;
   10.25 -qed "real_minus_not_zero_iff";
   10.26 -
   10.27  (*** Congruence property for addition ***)
   10.28  Goalw [congruent2_def]
   10.29      "congruent2 realrel (%p1 p2.                  \
   10.30 @@ -196,25 +192,25 @@
   10.31  (* real addition is an AC operator *)
   10.32  bind_thms ("real_add_ac", [real_add_assoc,real_add_commute,real_add_left_commute]);
   10.33  
   10.34 -Goalw [real_of_preal_def,real_zero_def] "0r + z = z";
   10.35 +Goalw [real_of_preal_def,real_zero_def] "(0::real) + z = z";
   10.36  by (res_inst_tac [("z","z")] eq_Abs_real 1);
   10.37  by (asm_full_simp_tac (simpset() addsimps [real_add] @ preal_add_ac) 1);
   10.38  qed "real_add_zero_left";
   10.39  Addsimps [real_add_zero_left];
   10.40  
   10.41 -Goal "z + 0r = z";
   10.42 +Goal "z + (0::real) = z";
   10.43  by (simp_tac (simpset() addsimps [real_add_commute]) 1);
   10.44  qed "real_add_zero_right";
   10.45  Addsimps [real_add_zero_right];
   10.46  
   10.47 -Goalw [real_zero_def] "z + (-z) = 0r";
   10.48 +Goalw [real_zero_def] "z + (-z) = (0::real)";
   10.49  by (res_inst_tac [("z","z")] eq_Abs_real 1);
   10.50  by (asm_full_simp_tac (simpset() addsimps [real_minus,
   10.51          real_add, preal_add_commute]) 1);
   10.52  qed "real_add_minus";
   10.53  Addsimps [real_add_minus];
   10.54  
   10.55 -Goal "(-z) + z = 0r";
   10.56 +Goal "(-z) + z = (0::real)";
   10.57  by (simp_tac (simpset() addsimps [real_add_commute]) 1);
   10.58  qed "real_add_minus_left";
   10.59  Addsimps [real_add_minus_left];
   10.60 @@ -230,31 +226,31 @@
   10.61  
   10.62  Addsimps [real_add_minus_cancel, real_minus_add_cancel];
   10.63  
   10.64 -Goal "? y. (x::real) + y = 0r";
   10.65 +Goal "EX y. (x::real) + y = 0";
   10.66  by (blast_tac (claset() addIs [real_add_minus]) 1);
   10.67  qed "real_minus_ex";
   10.68  
   10.69 -Goal "?! y. (x::real) + y = 0r";
   10.70 +Goal "EX! y. (x::real) + y = 0";
   10.71  by (auto_tac (claset() addIs [real_add_minus],simpset()));
   10.72  by (dres_inst_tac [("f","%x. ya+x")] arg_cong 1);
   10.73  by (asm_full_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
   10.74  by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
   10.75  qed "real_minus_ex1";
   10.76  
   10.77 -Goal "?! y. y + (x::real) = 0r";
   10.78 +Goal "EX! y. y + (x::real) = 0";
   10.79  by (auto_tac (claset() addIs [real_add_minus_left],simpset()));
   10.80  by (dres_inst_tac [("f","%x. x+ya")] arg_cong 1);
   10.81  by (asm_full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
   10.82  by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
   10.83  qed "real_minus_left_ex1";
   10.84  
   10.85 -Goal "x + y = 0r ==> x = -y";
   10.86 +Goal "x + y = (0::real) ==> x = -y";
   10.87  by (cut_inst_tac [("z","y")] real_add_minus_left 1);
   10.88  by (res_inst_tac [("x1","y")] (real_minus_left_ex1 RS ex1E) 1);
   10.89  by (Blast_tac 1);
   10.90  qed "real_add_minus_eq_minus";
   10.91  
   10.92 -Goal "? (y::real). x = -y";
   10.93 +Goal "EX (y::real). x = -y";
   10.94  by (cut_inst_tac [("x","x")] real_minus_ex 1);
   10.95  by (etac exE 1 THEN dtac real_add_minus_eq_minus 1);
   10.96  by (Fast_tac 1);
   10.97 @@ -278,29 +274,29 @@
   10.98  by (simp_tac (simpset() addsimps [real_add_commute,real_add_left_cancel]) 1);
   10.99  qed "real_add_right_cancel";
  10.100  
  10.101 -Goal "((x::real) = y) = (0r = x + (- y))";
  10.102 +Goal "((x::real) = y) = (0 = x + (- y))";
  10.103  by (Step_tac 1);
  10.104  by (res_inst_tac [("x1","-y")] 
  10.105        (real_add_right_cancel RS iffD1) 2);
  10.106  by Auto_tac;
  10.107  qed "real_eq_minus_iff"; 
  10.108  
  10.109 -Goal "((x::real) = y) = (x + (- y) = 0r)";
  10.110 +Goal "((x::real) = y) = (x + (- y) = 0)";
  10.111  by (Step_tac 1);
  10.112  by (res_inst_tac [("x1","-y")] 
  10.113        (real_add_right_cancel RS iffD1) 2);
  10.114  by Auto_tac;
  10.115  qed "real_eq_minus_iff2"; 
  10.116  
  10.117 -Goal "0r - x = -x";
  10.118 +Goal "(0::real) - x = -x";
  10.119  by (simp_tac (simpset() addsimps [real_diff_def]) 1);
  10.120  qed "real_diff_0";
  10.121  
  10.122 -Goal "x - 0r = x";
  10.123 +Goal "x - (0::real) = x";
  10.124  by (simp_tac (simpset() addsimps [real_diff_def]) 1);
  10.125  qed "real_diff_0_right";
  10.126  
  10.127 -Goal "x - x = 0r";
  10.128 +Goal "x - x = (0::real)";
  10.129  by (simp_tac (simpset() addsimps [real_diff_def]) 1);
  10.130  qed "real_diff_self";
  10.131  
  10.132 @@ -355,13 +351,15 @@
  10.133                                       preal_add_ac @ preal_mult_ac) 1);
  10.134  qed "real_mult_assoc";
  10.135  
  10.136 -qed_goal "real_mult_left_commute" thy
  10.137 -    "(z1::real) * (z2 * z3) = z2 * (z1 * z3)"
  10.138 - (fn _ => [rtac (real_mult_commute RS trans) 1, rtac (real_mult_assoc RS trans) 1,
  10.139 -           rtac (real_mult_commute RS arg_cong) 1]);
  10.140 +Goal "(z1::real) * (z2 * z3) = z2 * (z1 * z3)";
  10.141 +by (rtac (real_mult_commute RS trans) 1);
  10.142 +by (rtac (real_mult_assoc RS trans) 1);
  10.143 +by (rtac (real_mult_commute RS arg_cong) 1);
  10.144 +qed "real_mult_left_commute";
  10.145  
  10.146  (* real multiplication is an AC operator *)
  10.147 -bind_thms ("real_mult_ac", [real_mult_assoc, real_mult_commute, real_mult_left_commute]);
  10.148 +bind_thms ("real_mult_ac", 
  10.149 +	   [real_mult_assoc, real_mult_commute, real_mult_left_commute]);
  10.150  
  10.151  Goalw [real_one_def,pnat_one_def] "1r * z = z";
  10.152  by (res_inst_tac [("z","z")] eq_Abs_real 1);
  10.153 @@ -379,14 +377,14 @@
  10.154  
  10.155  Addsimps [real_mult_1_right];
  10.156  
  10.157 -Goalw [real_zero_def,pnat_one_def] "0r * z = 0r";
  10.158 +Goalw [real_zero_def,pnat_one_def] "0 * z = (0::real)";
  10.159  by (res_inst_tac [("z","z")] eq_Abs_real 1);
  10.160  by (asm_full_simp_tac (simpset() addsimps [real_mult,
  10.161      preal_add_mult_distrib2,preal_mult_1_right] 
  10.162      @ preal_mult_ac @ preal_add_ac) 1);
  10.163  qed "real_mult_0";
  10.164  
  10.165 -Goal "z * 0r = 0r";
  10.166 +Goal "z * 0 = (0::real)";
  10.167  by (simp_tac (simpset() addsimps [real_mult_commute, real_mult_0]) 1);
  10.168  qed "real_mult_0_right";
  10.169  
  10.170 @@ -401,19 +399,16 @@
  10.171  qed "real_minus_mult_eq1";
  10.172  
  10.173  Goal "-(x * y) = x * (- y :: real)";
  10.174 -by (res_inst_tac [("z","x")] eq_Abs_real 1);
  10.175 -by (res_inst_tac [("z","y")] eq_Abs_real 1);
  10.176 -by (auto_tac (claset(),
  10.177 -	      simpset() addsimps [real_minus,real_mult] 
  10.178 -    @ preal_mult_ac @ preal_add_ac));
  10.179 +by (simp_tac (simpset() addsimps [inst "z" "x" real_mult_commute,
  10.180 +				  real_minus_mult_eq1]) 1);
  10.181  qed "real_minus_mult_eq2";
  10.182  
  10.183 +Addsimps [real_minus_mult_eq1 RS sym, real_minus_mult_eq2 RS sym];
  10.184 +
  10.185  Goal "(- 1r) * z = -z";
  10.186 -by (simp_tac (simpset() addsimps [real_minus_mult_eq1 RS sym]) 1);
  10.187 +by (Simp_tac 1);
  10.188  qed "real_mult_minus_1";
  10.189  
  10.190 -Addsimps [real_mult_minus_1];
  10.191 -
  10.192  Goal "z * (- 1r) = -z";
  10.193  by (stac real_mult_commute 1);
  10.194  by (Simp_tac 1);
  10.195 @@ -455,15 +450,15 @@
  10.196                          preal_add_ac @ preal_mult_ac) 1);
  10.197  qed "real_add_mult_distrib";
  10.198  
  10.199 -val real_mult_commute'= read_instantiate [("z","w")] real_mult_commute;
  10.200 +val real_mult_commute'= inst "z" "w" real_mult_commute;
  10.201  
  10.202  Goal "(w::real) * (z1 + z2) = (w * z1) + (w * z2)";
  10.203 -by (simp_tac (simpset() addsimps [real_mult_commute',real_add_mult_distrib]) 1);
  10.204 +by (simp_tac (simpset() addsimps [real_mult_commute',
  10.205 +				  real_add_mult_distrib]) 1);
  10.206  qed "real_add_mult_distrib2";
  10.207  
  10.208  Goalw [real_diff_def] "((z1::real) - z2) * w = (z1 * w) - (z2 * w)";
  10.209 -by (simp_tac (simpset() addsimps [real_add_mult_distrib, 
  10.210 -				  real_minus_mult_eq1]) 1);
  10.211 +by (simp_tac (simpset() addsimps [real_add_mult_distrib]) 1);
  10.212  qed "real_diff_mult_distrib";
  10.213  
  10.214  Goal "(w::real) * (z1 - z2) = (w * z1) - (w * z2)";
  10.215 @@ -472,19 +467,19 @@
  10.216  qed "real_diff_mult_distrib2";
  10.217  
  10.218  (*** one and zero are distinct ***)
  10.219 -Goalw [real_zero_def,real_one_def] "0r ~= 1r";
  10.220 +Goalw [real_zero_def,real_one_def] "0 ~= 1r";
  10.221  by (auto_tac (claset(),
  10.222           simpset() addsimps [preal_self_less_add_left RS preal_not_refl2]));
  10.223  qed "real_zero_not_eq_one";
  10.224  
  10.225  (*** existence of inverse ***)
  10.226 -(** lemma -- alternative definition for 0r **)
  10.227 -Goalw [real_zero_def] "0r = Abs_real (realrel ^^ {(x, x)})";
  10.228 +(** lemma -- alternative definition of 0 **)
  10.229 +Goalw [real_zero_def] "0 = Abs_real (realrel ^^ {(x, x)})";
  10.230  by (auto_tac (claset(),simpset() addsimps [preal_add_commute]));
  10.231  qed "real_zero_iff";
  10.232  
  10.233  Goalw [real_zero_def,real_one_def] 
  10.234 -          "!!(x::real). x ~= 0r ==> ? y. x*y = 1r";
  10.235 +          "!!(x::real). x ~= 0 ==> EX y. x*y = 1r";
  10.236  by (res_inst_tac [("z","x")] eq_Abs_real 1);
  10.237  by (cut_inst_tac [("r1.0","xa"),("r2.0","y")] preal_linear 1);
  10.238  by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
  10.239 @@ -502,30 +497,30 @@
  10.240      @ preal_add_ac @ preal_mult_ac));
  10.241  qed "real_mult_inv_right_ex";
  10.242  
  10.243 -Goal "!!(x::real). x ~= 0r ==> ? y. y*x = 1r";
  10.244 +Goal "!!(x::real). x ~= 0 ==> EX y. y*x = 1r";
  10.245  by (asm_simp_tac (simpset() addsimps [real_mult_commute,
  10.246  				      real_mult_inv_right_ex]) 1);
  10.247  qed "real_mult_inv_left_ex";
  10.248  
  10.249 -Goalw [rinv_def] "x ~= 0r ==> rinv(x)*x = 1r";
  10.250 +Goalw [rinv_def] "x ~= 0 ==> rinv(x)*x = 1r";
  10.251  by (ftac real_mult_inv_left_ex 1);
  10.252  by (Step_tac 1);
  10.253  by (rtac selectI2 1);
  10.254  by Auto_tac;
  10.255  qed "real_mult_inv_left";
  10.256  
  10.257 -Goal "x ~= 0r ==> x*rinv(x) = 1r";
  10.258 +Goal "x ~= 0 ==> x*rinv(x) = 1r";
  10.259  by (auto_tac (claset() addIs [real_mult_commute RS subst],
  10.260                simpset() addsimps [real_mult_inv_left]));
  10.261  qed "real_mult_inv_right";
  10.262  
  10.263 -Goal "(c::real) ~= 0r ==> (c*a=c*b) = (a=b)";
  10.264 +Goal "(c::real) ~= 0 ==> (c*a=c*b) = (a=b)";
  10.265  by Auto_tac;
  10.266  by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1);
  10.267  by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac)  1);
  10.268  qed "real_mult_left_cancel";
  10.269      
  10.270 -Goal "(c::real) ~= 0r ==> (a*c=b*c) = (a=b)";
  10.271 +Goal "(c::real) ~= 0 ==> (a*c=b*c) = (a=b)";
  10.272  by (Step_tac 1);
  10.273  by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1);
  10.274  by (asm_full_simp_tac
  10.275 @@ -540,7 +535,7 @@
  10.276  by Auto_tac;
  10.277  qed "real_mult_right_cancel_ccontr";
  10.278  
  10.279 -Goalw [rinv_def] "x ~= 0r ==> rinv(x) ~= 0r";
  10.280 +Goalw [rinv_def] "x ~= 0 ==> rinv(x) ~= 0";
  10.281  by (ftac real_mult_inv_left_ex 1);
  10.282  by (etac exE 1);
  10.283  by (rtac selectI2 1);
  10.284 @@ -551,7 +546,7 @@
  10.285  
  10.286  Addsimps [real_mult_inv_left,real_mult_inv_right];
  10.287  
  10.288 -Goal "[| x ~= 0r; y ~= 0r |] ==> x * y ~= 0r";
  10.289 +Goal "[| x ~= 0; y ~= 0 |] ==> x * y ~= (0::real)";
  10.290  by (Step_tac 1);
  10.291  by (dres_inst_tac [("f","%z. rinv x*z")] arg_cong 1);
  10.292  by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
  10.293 @@ -559,7 +554,7 @@
  10.294  
  10.295  bind_thm ("real_mult_not_zeroE",real_mult_not_zero RS notE);
  10.296  
  10.297 -Goal "x ~= 0r ==> rinv(rinv x) = x";
  10.298 +Goal "x ~= 0 ==> rinv(rinv x) = x";
  10.299  by (res_inst_tac [("c1","rinv x")] (real_mult_right_cancel RS iffD1) 1);
  10.300  by (etac rinv_not_zero 1);
  10.301  by (auto_tac (claset() addDs [rinv_not_zero],simpset()));
  10.302 @@ -567,21 +562,19 @@
  10.303  
  10.304  Goalw [rinv_def] "rinv(1r) = 1r";
  10.305  by (cut_facts_tac [real_zero_not_eq_one RS 
  10.306 -       not_sym RS real_mult_inv_left_ex] 1);
  10.307 -by (etac exE 1);
  10.308 -by (rtac selectI2 1);
  10.309 +                   not_sym RS real_mult_inv_left_ex] 1);
  10.310  by (auto_tac (claset(),
  10.311 -	      simpset() addsimps 
  10.312 -    [real_zero_not_eq_one RS not_sym]));
  10.313 +	      simpset() addsimps [real_zero_not_eq_one RS not_sym]));
  10.314  qed "real_rinv_1";
  10.315  Addsimps [real_rinv_1];
  10.316  
  10.317 -Goal "x ~= 0r ==> rinv(-x) = -rinv(x)";
  10.318 +Goal "x ~= 0 ==> rinv(-x) = -rinv(x)";
  10.319  by (res_inst_tac [("c1","-x")] (real_mult_right_cancel RS iffD1) 1);
  10.320 +by (stac real_mult_inv_left 2);
  10.321  by Auto_tac;
  10.322  qed "real_minus_rinv";
  10.323  
  10.324 -Goal "[| x ~= 0r; y ~= 0r |] ==> rinv(x*y) = rinv(x)*rinv(y)";
  10.325 +Goal "[| x ~= 0; y ~= 0 |] ==> rinv(x*y) = rinv(x)*rinv(y)";
  10.326  by (forw_inst_tac [("y","y")] real_mult_not_zero 1 THEN assume_tac 1);
  10.327  by (res_inst_tac [("c1","x")] (real_mult_left_cancel RS iffD1) 1);
  10.328  by (auto_tac (claset(),simpset() addsimps [real_mult_assoc RS sym]));
  10.329 @@ -682,13 +675,13 @@
  10.330  
  10.331  Goalw [real_of_preal_def]
  10.332        "!!(x::preal). y < x ==> \
  10.333 -\      ? m. Abs_real (realrel ^^ {(x,y)}) = real_of_preal m";
  10.334 +\      EX m. Abs_real (realrel ^^ {(x,y)}) = real_of_preal m";
  10.335  by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
  10.336      simpset() addsimps preal_add_ac));
  10.337  qed "real_of_preal_ExI";
  10.338  
  10.339  Goalw [real_of_preal_def]
  10.340 -      "!!(x::preal). ? m. Abs_real (realrel ^^ {(x,y)}) = \
  10.341 +      "!!(x::preal). EX m. Abs_real (realrel ^^ {(x,y)}) = \
  10.342  \                    real_of_preal m ==> y < x";
  10.343  by (auto_tac (claset(),
  10.344  	      simpset() addsimps 
  10.345 @@ -697,13 +690,13 @@
  10.346      [preal_add_assoc RS sym,preal_self_less_add_left]) 1);
  10.347  qed "real_of_preal_ExD";
  10.348  
  10.349 -Goal "(? m. Abs_real (realrel ^^ {(x,y)}) = real_of_preal m) = (y < x)";
  10.350 +Goal "(EX m. Abs_real (realrel ^^ {(x,y)}) = real_of_preal m) = (y < x)";
  10.351  by (blast_tac (claset() addSIs [real_of_preal_ExI,real_of_preal_ExD]) 1);
  10.352  qed "real_of_preal_iff";
  10.353  
  10.354  (*** Gleason prop 9-4.4 p 127 ***)
  10.355  Goalw [real_of_preal_def,real_zero_def] 
  10.356 -      "? m. (x::real) = real_of_preal m | x = 0r | x = -(real_of_preal m)";
  10.357 +      "EX m. (x::real) = real_of_preal m | x = 0 | x = -(real_of_preal m)";
  10.358  by (res_inst_tac [("z","x")] eq_Abs_real 1);
  10.359  by (auto_tac (claset(),simpset() addsimps [real_minus] @ preal_add_ac));
  10.360  by (cut_inst_tac [("r1.0","x"),("r2.0","y")] preal_linear 1);
  10.361 @@ -713,7 +706,7 @@
  10.362  qed "real_of_preal_trichotomy";
  10.363  
  10.364  Goal "!!P. [| !!m. x = real_of_preal m ==> P; \
  10.365 -\             x = 0r ==> P; \
  10.366 +\             x = 0 ==> P; \
  10.367  \             !!m. x = -(real_of_preal m) ==> P |] ==> P";
  10.368  by (cut_inst_tac [("x","x")] real_of_preal_trichotomy 1);
  10.369  by Auto_tac;
  10.370 @@ -756,7 +749,7 @@
  10.371      preal_add_assoc RS sym]) 1);
  10.372  qed "real_of_preal_minus_less_self";
  10.373  
  10.374 -Goalw [real_zero_def] "- real_of_preal m < 0r";
  10.375 +Goalw [real_zero_def] "- real_of_preal m < 0";
  10.376  by (auto_tac (claset(),
  10.377  	      simpset() addsimps [real_of_preal_def,
  10.378  				  real_less_def,real_minus]));
  10.379 @@ -767,13 +760,13 @@
  10.380    [preal_self_less_add_right] @ preal_add_ac) 1);
  10.381  qed "real_of_preal_minus_less_zero";
  10.382  
  10.383 -Goal "~ 0r < - real_of_preal m";
  10.384 +Goal "~ 0 < - real_of_preal m";
  10.385  by (cut_facts_tac [real_of_preal_minus_less_zero] 1);
  10.386  by (fast_tac (claset() addDs [real_less_trans] 
  10.387                          addEs [real_less_irrefl]) 1);
  10.388  qed "real_of_preal_not_minus_gt_zero";
  10.389  
  10.390 -Goalw [real_zero_def] "0r < real_of_preal m";
  10.391 +Goalw [real_zero_def] "0 < real_of_preal m";
  10.392  by (auto_tac (claset(),simpset() addsimps 
  10.393     [real_of_preal_def,real_less_def,real_minus]));
  10.394  by (REPEAT(rtac exI 1));
  10.395 @@ -783,20 +776,20 @@
  10.396  		   [preal_self_less_add_right] @ preal_add_ac) 1);
  10.397  qed "real_of_preal_zero_less";
  10.398  
  10.399 -Goal "~ real_of_preal m < 0r";
  10.400 +Goal "~ real_of_preal m < 0";
  10.401  by (cut_facts_tac [real_of_preal_zero_less] 1);
  10.402  by (blast_tac (claset() addDs [real_less_trans] 
  10.403                          addEs [real_less_irrefl]) 1);
  10.404  qed "real_of_preal_not_less_zero";
  10.405  
  10.406 -Goal "0r < - (- real_of_preal m)";
  10.407 +Goal "0 < - (- real_of_preal m)";
  10.408  by (simp_tac (simpset() addsimps 
  10.409      [real_of_preal_zero_less]) 1);
  10.410  qed "real_minus_minus_zero_less";
  10.411  
  10.412  (* another lemma *)
  10.413  Goalw [real_zero_def]
  10.414 -      "0r < real_of_preal m + real_of_preal m1";
  10.415 +      "0 < real_of_preal m + real_of_preal m1";
  10.416  by (auto_tac (claset(),
  10.417  	      simpset() addsimps [real_of_preal_def,
  10.418  				  real_less_def,real_add]));
  10.419 @@ -962,7 +955,7 @@
  10.420  by (blast_tac (claset() addSEs [real_less_asym]) 1);
  10.421  qed "real_less_le";
  10.422  
  10.423 -Goal "(0r < -R) = (R < 0r)";
  10.424 +Goal "(0 < -R) = (R < (0::real))";
  10.425  by (res_inst_tac [("x","R")]  real_of_preal_trichotomyE 1);
  10.426  by (auto_tac (claset(),
  10.427  	      simpset() addsimps [real_of_preal_not_minus_gt_zero,
  10.428 @@ -972,7 +965,7 @@
  10.429  
  10.430  Addsimps [real_minus_zero_less_iff];
  10.431  
  10.432 -Goal "(-R < 0r) = (0r < R)";
  10.433 +Goal "(-R < 0) = ((0::real) < R)";
  10.434  by (res_inst_tac [("x","R")]  real_of_preal_trichotomyE 1);
  10.435  by (auto_tac (claset(),
  10.436  	      simpset() addsimps [real_of_preal_not_minus_gt_zero,
  10.437 @@ -981,7 +974,7 @@
  10.438  qed "real_minus_zero_less_iff2";
  10.439  
  10.440  (*Alternative definition for real_less*)
  10.441 -Goal "R < S ==> ? T. 0r < T & R + T = S";
  10.442 +Goal "R < S ==> EX T::real. 0 < T & R + T = S";
  10.443  by (res_inst_tac [("x","R")]  real_of_preal_trichotomyE 1);
  10.444  by (ALLGOALS(res_inst_tac [("x","S")]  real_of_preal_trichotomyE));
  10.445  by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
  10.446 @@ -999,7 +992,7 @@
  10.447  qed "real_less_add_positive_left_Ex";
  10.448  
  10.449  (** change naff name(s)! **)
  10.450 -Goal "(W < S) ==> (0r < S + (-W))";
  10.451 +Goal "(W < S) ==> (0 < S + (-W::real))";
  10.452  by (dtac real_less_add_positive_left_Ex 1);
  10.453  by (auto_tac (claset(),
  10.454  	      simpset() addsimps [real_add_minus,
  10.455 @@ -1011,7 +1004,7 @@
  10.456  qed "real_lemma_change_eq_subj";
  10.457  
  10.458  (* FIXME: long! *)
  10.459 -Goal "(0r < S + (-W)) ==> (W < S)";
  10.460 +Goal "(0 < S + (-W::real)) ==> (W < S)";
  10.461  by (rtac ccontr 1);
  10.462  by (dtac (real_leI RS real_le_imp_less_or_eq) 1);
  10.463  by (auto_tac (claset(),
  10.464 @@ -1026,13 +1019,13 @@
  10.465  by (auto_tac (claset() addEs [real_less_asym], simpset()));
  10.466  qed "real_sum_gt_zero_less";
  10.467  
  10.468 -Goal "(0r < S + (-W)) = (W < S)";
  10.469 +Goal "(0 < S + (-W::real)) = (W < S)";
  10.470  by (blast_tac (claset() addIs [real_less_sum_gt_zero,
  10.471  			       real_sum_gt_zero_less]) 1);
  10.472  qed "real_less_sum_gt_0_iff";
  10.473  
  10.474  
  10.475 -Goalw [real_diff_def] "(x<y) = (x-y < 0r)";
  10.476 +Goalw [real_diff_def] "(x<y) = (x-y < (0::real))";
  10.477  by (stac (real_minus_zero_less_iff RS sym) 1);
  10.478  by (simp_tac (simpset() addsimps [real_add_commute,
  10.479  				  real_less_sum_gt_0_iff]) 1);
    11.1 --- a/src/HOL/Real/RealDef.thy	Wed Jun 07 12:07:07 2000 +0200
    11.2 +++ b/src/HOL/Real/RealDef.thy	Wed Jun 07 12:14:18 2000 +0200
    11.3 @@ -15,17 +15,16 @@
    11.4  
    11.5  
    11.6  instance
    11.7 -   real  :: {ord, plus, times, minus}
    11.8 +   real  :: {ord, zero, plus, times, minus}
    11.9  
   11.10  consts 
   11.11  
   11.12 -  "0r"       :: real               ("0r")   
   11.13    "1r"       :: real               ("1r")  
   11.14  
   11.15  defs
   11.16  
   11.17    real_zero_def  
   11.18 -     "0r == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p),
   11.19 +     "0 == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p),
   11.20                                  preal_of_prat(prat_of_pnat 1p))})"
   11.21    real_one_def   
   11.22       "1r == Abs_real(realrel^^{(preal_of_prat(prat_of_pnat 1p) + 
   11.23 @@ -44,7 +43,7 @@
   11.24                                 preal_of_prat(prat_of_pnat 1p))})"
   11.25  
   11.26    rinv       :: real => real
   11.27 -  "rinv(R)   == (@S. R ~= 0r & S*R = 1r)"
   11.28 +  "rinv(R)   == (@S. R ~= 0 & S*R = 1r)"
   11.29  
   11.30    real_of_posnat :: nat => real             
   11.31    "real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))"
    12.1 --- a/src/HOL/Real/RealInt.ML	Wed Jun 07 12:07:07 2000 +0200
    12.2 +++ b/src/HOL/Real/RealInt.ML	Wed Jun 07 12:14:18 2000 +0200
    12.3 @@ -37,7 +37,7 @@
    12.4       prat_of_pnat_add RS sym,pnat_of_nat_add]));
    12.5  qed "inj_real_of_int";
    12.6  
    12.7 -Goalw [int_def,real_zero_def] "real_of_int (int 0) = 0r";
    12.8 +Goalw [int_def,real_zero_def] "real_of_int (int 0) = 0";
    12.9  by (simp_tac (simpset() addsimps [real_of_int, preal_add_commute]) 1);
   12.10  qed "real_of_int_zero";
   12.11  
   12.12 @@ -97,13 +97,13 @@
   12.13  qed "real_of_nat_real_of_int";
   12.14  
   12.15  (* put with other properties of real_of_nat? *)
   12.16 -Goal "neg z ==> real_of_nat (nat z) = 0r";
   12.17 +Goal "neg z ==> real_of_nat (nat z) = 0";
   12.18  by (asm_simp_tac (simpset() addsimps [neg_nat,
   12.19      real_of_nat_zero]) 1);
   12.20  qed "real_of_nat_neg_int";
   12.21  Addsimps [real_of_nat_neg_int];
   12.22  
   12.23 -Goal "(real_of_int x = 0r) = (x = int 0)";
   12.24 +Goal "(real_of_int x = 0) = (x = int 0)";
   12.25  by (auto_tac (claset() addIs [inj_real_of_int RS injD],
   12.26      HOL_ss addsimps [real_of_int_zero]));
   12.27  qed "real_of_int_zero_cancel";
    13.1 --- a/src/HOL/Real/RealOrd.ML	Wed Jun 07 12:07:07 2000 +0200
    13.2 +++ b/src/HOL/Real/RealOrd.ML	Wed Jun 07 12:14:18 2000 +0200
    13.3 @@ -5,30 +5,89 @@
    13.4      Description: Type "real" is a linear order
    13.5  *)
    13.6  
    13.7 -Goal "(0r < x) = (? y. x = real_of_preal y)";
    13.8 +(**** The simproc abel_cancel ****)
    13.9 +
   13.10 +(*** Two lemmas needed for the simprocs ***)
   13.11 +
   13.12 +(*Deletion of other terms in the formula, seeking the -x at the front of z*)
   13.13 +Goal "((x::real) + (y + z) = y + u) = ((x + z) = u)";
   13.14 +by (stac real_add_left_commute 1);
   13.15 +by (rtac real_add_left_cancel 1);
   13.16 +qed "real_add_cancel_21";
   13.17 +
   13.18 +(*A further rule to deal with the case that
   13.19 +  everything gets cancelled on the right.*)
   13.20 +Goal "((x::real) + (y + z) = y) = (x = -z)";
   13.21 +by (stac real_add_left_commute 1);
   13.22 +by (res_inst_tac [("t", "y")] (real_add_zero_right RS subst) 1
   13.23 +    THEN stac real_add_left_cancel 1);
   13.24 +by (simp_tac (simpset() addsimps [real_eq_diff_eq RS sym]) 1);
   13.25 +qed "real_add_cancel_end";
   13.26 +
   13.27 +
   13.28 +structure Real_Cancel_Data =
   13.29 +struct
   13.30 +  val ss		= HOL_ss
   13.31 +  val eq_reflection	= eq_reflection
   13.32 +
   13.33 +  val thy		= RealDef.thy
   13.34 +  val T			= HOLogic.realT
   13.35 +  val zero		= Const ("0", T)
   13.36 +  val restrict_to_left  = restrict_to_left
   13.37 +  val add_cancel_21	= real_add_cancel_21
   13.38 +  val add_cancel_end	= real_add_cancel_end
   13.39 +  val add_left_cancel	= real_add_left_cancel
   13.40 +  val add_assoc		= real_add_assoc
   13.41 +  val add_commute	= real_add_commute
   13.42 +  val add_left_commute	= real_add_left_commute
   13.43 +  val add_0		= real_add_zero_left
   13.44 +  val add_0_right	= real_add_zero_right
   13.45 +
   13.46 +  val eq_diff_eq	= real_eq_diff_eq
   13.47 +  val eqI_rules		= [real_less_eqI, real_eq_eqI, real_le_eqI]
   13.48 +  fun dest_eqI th = 
   13.49 +      #1 (HOLogic.dest_bin "op =" HOLogic.boolT 
   13.50 +	      (HOLogic.dest_Trueprop (concl_of th)))
   13.51 +
   13.52 +  val diff_def		= real_diff_def
   13.53 +  val minus_add_distrib	= real_minus_add_distrib
   13.54 +  val minus_minus	= real_minus_minus
   13.55 +  val minus_0		= real_minus_zero
   13.56 +  val add_inverses	= [real_add_minus, real_add_minus_left];
   13.57 +  val cancel_simps	= [real_add_minus_cancel, real_minus_add_cancel]
   13.58 +end;
   13.59 +
   13.60 +structure Real_Cancel = Abel_Cancel (Real_Cancel_Data);
   13.61 +
   13.62 +Addsimprocs [Real_Cancel.sum_conv, Real_Cancel.rel_conv];
   13.63 +
   13.64 +
   13.65 +(**** Theorems about the ordering ****)
   13.66 +
   13.67 +Goal "(0 < x) = (EX y. x = real_of_preal y)";
   13.68  by (auto_tac (claset(), simpset() addsimps [real_of_preal_zero_less]));
   13.69  by (cut_inst_tac [("x","x")] real_of_preal_trichotomy 1);
   13.70  by (blast_tac (claset() addSEs [real_less_irrefl,
   13.71  				real_of_preal_not_minus_gt_zero RS notE]) 1);
   13.72  qed "real_gt_zero_preal_Ex";
   13.73  
   13.74 -Goal "real_of_preal z < x ==> ? y. x = real_of_preal y";
   13.75 +Goal "real_of_preal z < x ==> EX y. x = real_of_preal y";
   13.76  by (blast_tac (claset() addSDs [real_of_preal_zero_less RS real_less_trans]
   13.77                 addIs [real_gt_zero_preal_Ex RS iffD1]) 1);
   13.78  qed "real_gt_preal_preal_Ex";
   13.79  
   13.80 -Goal "real_of_preal z <= x ==> ? y. x = real_of_preal y";
   13.81 +Goal "real_of_preal z <= x ==> EX y. x = real_of_preal y";
   13.82  by (blast_tac (claset() addDs [real_le_imp_less_or_eq,
   13.83  			       real_gt_preal_preal_Ex]) 1);
   13.84  qed "real_ge_preal_preal_Ex";
   13.85  
   13.86 -Goal "y <= 0r ==> !x. y < real_of_preal x";
   13.87 +Goal "y <= 0 ==> ALL x. y < real_of_preal x";
   13.88  by (auto_tac (claset() addEs [real_le_imp_less_or_eq RS disjE]
   13.89                         addIs [real_of_preal_zero_less RSN(2,real_less_trans)],
   13.90                simpset() addsimps [real_of_preal_zero_less]));
   13.91  qed "real_less_all_preal";
   13.92  
   13.93 -Goal "~ 0r < y ==> !x. y < real_of_preal x";
   13.94 +Goal "~ 0 < y ==> ALL x. y < real_of_preal x";
   13.95  by (blast_tac (claset() addSIs [real_less_all_preal,real_leI]) 1);
   13.96  qed "real_less_all_real2";
   13.97  
   13.98 @@ -38,22 +97,22 @@
   13.99  by (simp_tac (simpset() addsimps [real_add_commute]) 1);
  13.100  qed "real_less_swap_iff";
  13.101  
  13.102 -Goal "[| R + L = S; 0r < L |] ==> R < S";
  13.103 +Goal "[| R + L = S;  (0::real) < L |] ==> R < S";
  13.104  by (rtac (real_less_sum_gt_0_iff RS iffD1) 1);
  13.105  by (auto_tac (claset(), simpset() addsimps real_add_ac));
  13.106  qed "real_lemma_add_positive_imp_less";
  13.107  
  13.108 -Goal "? T. 0r < T & R + T = S ==> R < S";
  13.109 +Goal "EX T::real. 0 < T & R + T = S ==> R < S";
  13.110  by (blast_tac (claset() addIs [real_lemma_add_positive_imp_less]) 1);
  13.111  qed "real_ex_add_positive_left_less";
  13.112  
  13.113  (*Alternative definition for real_less.  NOT for rewriting*)
  13.114 -Goal "(R < S) = (? T. 0r < T & R + T = S)";
  13.115 +Goal "(R < S) = (EX T::real. 0 < T & R + T = S)";
  13.116  by (blast_tac (claset() addSIs [real_less_add_positive_left_Ex,
  13.117  				real_ex_add_positive_left_less]) 1);
  13.118  qed "real_less_iff_add";
  13.119  
  13.120 -Goal "(0r < x) = (-x < x)";
  13.121 +Goal "((0::real) < x) = (-x < x)";
  13.122  by Safe_tac;
  13.123  by (rtac ccontr 2 THEN forward_tac 
  13.124      [real_leI RS real_le_imp_less_or_eq] 2);
  13.125 @@ -65,17 +124,17 @@
  13.126   	        [real_gt_zero_preal_Ex,real_of_preal_minus_less_self]));
  13.127  qed "real_gt_zero_iff";
  13.128  
  13.129 -Goal "(x < 0r) = (x < -x)";
  13.130 +Goal "(x < (0::real)) = (x < -x)";
  13.131  by (rtac (real_minus_zero_less_iff RS subst) 1);
  13.132  by (stac real_gt_zero_iff 1);
  13.133  by (Full_simp_tac 1);
  13.134  qed "real_lt_zero_iff";
  13.135  
  13.136 -Goalw [real_le_def] "(0r <= x) = (-x <= x)";
  13.137 +Goalw [real_le_def] "((0::real) <= x) = (-x <= x)";
  13.138  by (auto_tac (claset(), simpset() addsimps [real_lt_zero_iff RS sym]));
  13.139  qed "real_ge_zero_iff";
  13.140  
  13.141 -Goalw [real_le_def] "(x <= 0r) = (x <= -x)";
  13.142 +Goalw [real_le_def] "(x <= (0::real)) = (x <= -x)";
  13.143  by (auto_tac (claset(), simpset() addsimps [real_gt_zero_iff RS sym]));
  13.144  qed "real_le_zero_iff";
  13.145  
  13.146 @@ -86,31 +145,31 @@
  13.147  by (etac preal_less_irrefl 1);
  13.148  qed "real_of_preal_le_iff";
  13.149  
  13.150 -Goal "[| 0r < x; 0r < y |] ==> 0r < x * y";
  13.151 +Goal "[| 0 < x; 0 < y |] ==> (0::real) < x * y";
  13.152  by (auto_tac (claset(), simpset() addsimps [real_gt_zero_preal_Ex]));  
  13.153  by (res_inst_tac [("x","y*ya")] exI 1);
  13.154  by (full_simp_tac (simpset() addsimps [real_of_preal_mult]) 1);
  13.155  qed "real_mult_order";
  13.156  
  13.157 -Goal "[| x < 0r; y < 0r |] ==> 0r < x * y";
  13.158 +Goal "[| x < 0; y < 0 |] ==> (0::real) < x * y";
  13.159  by (REPEAT(dtac (real_minus_zero_less_iff RS iffD2) 1));
  13.160  by (dtac real_mult_order 1 THEN assume_tac 1);
  13.161  by (Asm_full_simp_tac 1);
  13.162  qed "real_mult_less_zero1";
  13.163  
  13.164 -Goal "[| 0r <= x; 0r <= y |] ==> 0r <= x * y";
  13.165 +Goal "[| 0 <= x; 0 <= y |] ==> (0::real) <= x * y";
  13.166  by (REPEAT(dtac real_le_imp_less_or_eq 1));
  13.167  by (auto_tac (claset() addIs [real_mult_order, real_less_imp_le],
  13.168  	      simpset()));
  13.169  qed "real_le_mult_order";
  13.170  
  13.171 -Goal "[| 0r < x; 0r <= y |] ==> 0r <= x * y";
  13.172 +Goal "[| 0 < x; 0 <= y |] ==> (0::real) <= x * y";
  13.173  by (dtac real_le_imp_less_or_eq 1);
  13.174  by (auto_tac (claset() addIs [real_mult_order,
  13.175  			      real_less_imp_le],simpset()));
  13.176  qed "real_less_le_mult_order";
  13.177  
  13.178 -Goal "[| x <= 0r; y <= 0r |] ==> 0r <= x * y";
  13.179 +Goal "[| x <= 0; y <= 0 |] ==> (0::real) <= x * y";
  13.180  by (rtac real_less_or_eq_imp_le 1);
  13.181  by (dtac real_le_imp_less_or_eq 1 THEN etac disjE 1);
  13.182  by Auto_tac;
  13.183 @@ -118,7 +177,7 @@
  13.184  by (auto_tac (claset() addDs [real_mult_less_zero1],simpset()));
  13.185  qed "real_mult_le_zero1";
  13.186  
  13.187 -Goal "[| 0r <= x; y < 0r |] ==> x * y <= 0r";
  13.188 +Goal "[| 0 <= x; y < 0 |] ==> x * y <= (0::real)";
  13.189  by (rtac real_less_or_eq_imp_le 1);
  13.190  by (dtac real_le_imp_less_or_eq 1 THEN etac disjE 1);
  13.191  by Auto_tac;
  13.192 @@ -128,14 +187,14 @@
  13.193  	                addIs [real_minus_mult_eq2 RS ssubst]) 1);
  13.194  qed "real_mult_le_zero";
  13.195  
  13.196 -Goal "[| 0r < x; y < 0r |] ==> x*y < 0r";
  13.197 +Goal "[| 0 < x; y < 0 |] ==> x*y < (0::real)";
  13.198  by (dtac (real_minus_zero_less_iff RS iffD2) 1);
  13.199  by (dtac real_mult_order 1 THEN assume_tac 1);
  13.200  by (rtac (real_minus_zero_less_iff RS iffD1) 1);
  13.201 -by (asm_full_simp_tac (simpset() addsimps [real_minus_mult_eq2]) 1);
  13.202 +by (Asm_full_simp_tac 1);
  13.203  qed "real_mult_less_zero";
  13.204  
  13.205 -Goalw [real_one_def] "0r < 1r";
  13.206 +Goalw [real_one_def] "0 < 1r";
  13.207  by (auto_tac (claset() addIs [real_gt_zero_preal_Ex RS iffD2],
  13.208  	      simpset() addsimps [real_of_preal_def]));
  13.209  qed "real_zero_less_one";
  13.210 @@ -198,13 +257,13 @@
  13.211  by (Full_simp_tac 1);
  13.212  qed "real_le_add_left_cancel";
  13.213  
  13.214 -Goal "[| 0r < x; 0r < y |] ==> 0r < x + y";
  13.215 +Goal "[| 0 < x; 0 < y |] ==> (0::real) < x + y";
  13.216  by (etac real_less_trans 1);
  13.217  by (dtac real_add_less_mono2 1);
  13.218  by (Full_simp_tac 1);
  13.219  qed "real_add_order";
  13.220  
  13.221 -Goal "[| 0r <= x; 0r <= y |] ==> 0r <= x + y";
  13.222 +Goal "[| 0 <= x; 0 <= y |] ==> (0::real) <= x + y";
  13.223  by (REPEAT(dtac real_le_imp_less_or_eq 1));
  13.224  by (auto_tac (claset() addIs [real_add_order, real_less_imp_le],
  13.225  	      simpset()));
  13.226 @@ -233,7 +292,7 @@
  13.227  	  simpset() addsimps [real_minus_zero_less_iff2, real_zero_less_one]));
  13.228  qed "real_less_Ex";
  13.229  
  13.230 -Goal "0r < r ==>  u + (-r) < u";
  13.231 +Goal "(0::real) < r ==>  u + (-r) < u";
  13.232  by (res_inst_tac [("C","r")] real_less_add_right_cancel 1);
  13.233  by (simp_tac (simpset() addsimps [real_add_assoc]) 1);
  13.234  qed "real_add_minus_positive_less_self";
  13.235 @@ -249,13 +308,13 @@
  13.236  qed "real_le_minus_iff";
  13.237  Addsimps [real_le_minus_iff RS sym];
  13.238            
  13.239 -Goal "0r <= 1r";
  13.240 +Goal "0 <= 1r";
  13.241  by (rtac (real_zero_less_one RS real_less_imp_le) 1);
  13.242  qed "real_zero_le_one";
  13.243  Addsimps [real_zero_le_one];
  13.244  
  13.245 -Goal "0r <= x*x";
  13.246 -by (res_inst_tac [("R2.0","0r"),("R1.0","x")] real_linear_less2 1);
  13.247 +Goal "(0::real) <= x*x";
  13.248 +by (res_inst_tac [("R2.0","0"),("R1.0","x")] real_linear_less2 1);
  13.249  by (auto_tac (claset() addIs [real_mult_order,
  13.250  			      real_mult_less_zero1,real_less_imp_le],
  13.251  	      simpset()));
  13.252 @@ -305,12 +364,12 @@
  13.253  by (etac (inj_pnat_of_nat RS injD) 1);
  13.254  qed "inj_real_of_posnat";
  13.255  
  13.256 -Goalw [real_of_posnat_def] "0r < real_of_posnat n";
  13.257 +Goalw [real_of_posnat_def] "0 < real_of_posnat n";
  13.258  by (rtac (real_gt_zero_preal_Ex RS iffD2) 1);
  13.259  by (Blast_tac 1);
  13.260  qed "real_of_posnat_less_zero";
  13.261  
  13.262 -Goal "real_of_posnat n ~= 0r";
  13.263 +Goal "real_of_posnat n ~= 0";
  13.264  by (rtac (real_of_posnat_less_zero RS real_not_refl2 RS not_sym) 1);
  13.265  qed "real_of_posnat_not_eq_zero";
  13.266  Addsimps[real_of_posnat_not_eq_zero];
  13.267 @@ -324,7 +383,7 @@
  13.268  qed "real_of_posnat_less_one";
  13.269  Addsimps [real_of_posnat_less_one];
  13.270  
  13.271 -Goal "rinv(real_of_posnat n) ~= 0r";
  13.272 +Goal "rinv(real_of_posnat n) ~= 0";
  13.273  by (rtac ((real_of_posnat_less_zero RS 
  13.274      real_not_refl2 RS not_sym) RS rinv_not_zero) 1);
  13.275  qed "real_of_posnat_rinv_not_zero";
  13.276 @@ -340,7 +399,7 @@
  13.277      real_not_refl2 RS not_sym)]) 1);
  13.278  qed "real_of_posnat_rinv_inj";
  13.279  
  13.280 -Goal "0r < x ==> 0r < rinv x";
  13.281 +Goal "0 < x ==> 0 < rinv x";
  13.282  by (EVERY1[rtac ccontr, dtac real_leI]);
  13.283  by (forward_tac [real_minus_zero_less_iff2 RS iffD2] 1);
  13.284  by (forward_tac [real_not_refl2 RS not_sym] 1);
  13.285 @@ -351,7 +410,7 @@
  13.286  	      simpset() addsimps [real_minus_mult_eq1 RS sym]));
  13.287  qed "real_rinv_gt_zero";
  13.288  
  13.289 -Goal "x < 0r ==> rinv x < 0r";
  13.290 +Goal "x < 0 ==> rinv x < 0";
  13.291  by (ftac real_not_refl2 1);
  13.292  by (dtac (real_minus_zero_less_iff RS iffD2) 1);
  13.293  by (rtac (real_minus_zero_less_iff RS iffD1) 1);
  13.294 @@ -359,14 +418,13 @@
  13.295  by (auto_tac (claset() addIs [real_rinv_gt_zero], simpset()));
  13.296  qed "real_rinv_less_zero";
  13.297  
  13.298 -Goal "0r < rinv(real_of_posnat n)";
  13.299 +Goal "0 < rinv(real_of_posnat n)";
  13.300  by (rtac (real_of_posnat_less_zero RS real_rinv_gt_zero) 1);
  13.301  qed "real_of_posnat_rinv_gt_zero";
  13.302  Addsimps [real_of_posnat_rinv_gt_zero];
  13.303  
  13.304  Goal "x+x = x*(1r+1r)";
  13.305 -by (simp_tac (simpset() addsimps 
  13.306 -              [real_add_mult_distrib2]) 1);
  13.307 +by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1);
  13.308  qed "real_add_self";
  13.309  
  13.310  Goal "x < x + 1r";
  13.311 @@ -379,12 +437,12 @@
  13.312  by (rtac real_self_less_add_one 1);
  13.313  qed "real_one_less_two";
  13.314  
  13.315 -Goal "0r < 1r + 1r";
  13.316 +Goal "0 < 1r + 1r";
  13.317  by (rtac ([real_zero_less_one,
  13.318  	   real_one_less_two] MRS real_less_trans) 1);
  13.319  qed "real_zero_less_two";
  13.320  
  13.321 -Goal "1r + 1r ~= 0r";
  13.322 +Goal "1r + 1r ~= 0";
  13.323  by (rtac (real_zero_less_two RS real_not_refl2 RS not_sym) 1);
  13.324  qed "real_two_not_zero";
  13.325  
  13.326 @@ -395,7 +453,7 @@
  13.327  by (full_simp_tac (simpset() addsimps [real_mult_assoc]) 1);
  13.328  qed "real_sum_of_halves";
  13.329  
  13.330 -Goal "[| 0r<z; x<y |] ==> x*z<y*z";       
  13.331 +Goal "[| (0::real) < z; x < y |] ==> x*z < y*z";       
  13.332  by (rotate_tac 1 1);
  13.333  by (dtac real_less_sum_gt_zero 1);
  13.334  by (rtac real_sum_gt_zero_less 1);
  13.335 @@ -404,11 +462,11 @@
  13.336      real_minus_mult_eq2 RS sym, real_mult_commute ]) 1);
  13.337  qed "real_mult_less_mono1";
  13.338  
  13.339 -Goal "[| 0r<z; x<y |] ==> z*x<z*y";       
  13.340 +Goal "[| (0::real) < z; x < y |] ==> z*x < z*y";       
  13.341  by (asm_simp_tac (simpset() addsimps [real_mult_commute,real_mult_less_mono1]) 1);
  13.342  qed "real_mult_less_mono2";
  13.343  
  13.344 -Goal "[| 0r<z; x*z<y*z |] ==> x<y";
  13.345 +Goal "[| (0::real) < z; x*z < y*z |] ==> x < y";
  13.346  by (forw_inst_tac [("x","x*z")] (real_rinv_gt_zero 
  13.347                         RS real_mult_less_mono1) 1);
  13.348  by (auto_tac (claset(),
  13.349 @@ -416,17 +474,17 @@
  13.350       [real_mult_assoc,real_not_refl2 RS not_sym]));
  13.351  qed "real_mult_less_cancel1";
  13.352  
  13.353 -Goal "[| 0r<z; z*x<z*y |] ==> x<y";
  13.354 +Goal "[| (0::real) < z; z*x < z*y |] ==> x < y";
  13.355  by (etac real_mult_less_cancel1 1);
  13.356  by (asm_full_simp_tac (simpset() addsimps [real_mult_commute]) 1);
  13.357  qed "real_mult_less_cancel2";
  13.358  
  13.359 -Goal "0r < z ==> (x*z < y*z) = (x < y)";
  13.360 +Goal "(0::real) < z ==> (x*z < y*z) = (x < y)";
  13.361  by (blast_tac (claset() addIs [real_mult_less_mono1,
  13.362      real_mult_less_cancel1]) 1);
  13.363  qed "real_mult_less_iff1";
  13.364  
  13.365 -Goal "0r < z ==> (z*x < z*y) = (x < y)";
  13.366 +Goal "(0::real) < z ==> (z*x < z*y) = (x < y)";
  13.367  by (blast_tac (claset() addIs [real_mult_less_mono2,
  13.368      real_mult_less_cancel2]) 1);
  13.369  qed "real_mult_less_iff2";
  13.370 @@ -434,60 +492,60 @@
  13.371  Addsimps [real_mult_less_iff1,real_mult_less_iff2];
  13.372  
  13.373  (* 05/00 *)
  13.374 -Goalw [real_le_def] "[| 0r<z; x*z<=y*z |] ==> x<=y";
  13.375 +Goalw [real_le_def] "[| (0::real) < z; x*z<=y*z |] ==> x<=y";
  13.376  by (Auto_tac);
  13.377  qed "real_mult_le_cancel1";
  13.378  
  13.379 -Goalw [real_le_def] "!!(x::real). [| 0r<z; z*x<=z*y |] ==> x<=y";
  13.380 +Goalw [real_le_def] "[| (0::real) < z; z*x<=z*y |] ==> x<=y";
  13.381  by (Auto_tac);
  13.382  qed "real_mult_le_cancel2";
  13.383  
  13.384 -Goalw [real_le_def] "0r < z ==> (x*z <= y*z) = (x <= y)";
  13.385 +Goalw [real_le_def] "(0::real) < z ==> (x*z <= y*z) = (x <= y)";
  13.386  by (Auto_tac);
  13.387  qed "real_mult_le_cancel_iff1";
  13.388  
  13.389 -Goalw [real_le_def] "0r < z ==> (z*x <= z*y) = (x <= y)";
  13.390 +Goalw [real_le_def] "(0::real) < z ==> (z*x <= z*y) = (x <= y)";
  13.391  by (Auto_tac);
  13.392  qed "real_mult_le_cancel_iff2";
  13.393  
  13.394  Addsimps [real_mult_le_cancel_iff1,real_mult_le_cancel_iff2];
  13.395  
  13.396  
  13.397 -Goal "[| 0r<=z; x<y |] ==> x*z<=y*z";
  13.398 +Goal "[| (0::real) <= z; x < y |] ==> x*z <= y*z";
  13.399  by (EVERY1 [rtac real_less_or_eq_imp_le, dtac real_le_imp_less_or_eq]);
  13.400  by (auto_tac (claset() addIs [real_mult_less_mono1],simpset()));
  13.401  qed "real_mult_le_less_mono1";
  13.402  
  13.403 -Goal "[| 0r<=z; x<y |] ==> z*x<=z*y";
  13.404 +Goal "[| (0::real) <= z; x < y |] ==> z*x <= z*y";
  13.405  by (asm_simp_tac (simpset() addsimps [real_mult_commute,real_mult_le_less_mono1]) 1);
  13.406  qed "real_mult_le_less_mono2";
  13.407  
  13.408 -Goal "[| 0r<=z; x<=y |] ==> z*x<=z*y";
  13.409 +Goal "[| (0::real) <= z; x <= y |] ==> z*x <= z*y";
  13.410  by (dres_inst_tac [("x","x")] real_le_imp_less_or_eq 1);
  13.411  by (auto_tac (claset() addIs [real_mult_le_less_mono2], simpset()));
  13.412  qed "real_mult_le_le_mono1";
  13.413  
  13.414 -Goal "[| 0r < r1; r1 <r2; 0r < x; x < y|] ==> r1 * x < r2 * y";
  13.415 +Goal "[| (0::real) < r1; r1 < r2; 0 < x; x < y|] ==> r1 * x < r2 * y";
  13.416  by (dres_inst_tac [("x","x")] real_mult_less_mono2 1);
  13.417 -by (dres_inst_tac [("R1.0","0r")] real_less_trans 2);
  13.418 +by (dres_inst_tac [("R1.0","0")] real_less_trans 2);
  13.419  by (dres_inst_tac [("x","r1")] real_mult_less_mono1 3);
  13.420  by Auto_tac;
  13.421  by (blast_tac (claset() addIs [real_less_trans]) 1);
  13.422  qed "real_mult_less_mono";
  13.423  
  13.424 -Goal "[| 0r < r1; r1 <r2; 0r < y|] ==> 0r < r2 * y";
  13.425 -by (dres_inst_tac [("R1.0","0r")] real_less_trans 1);
  13.426 -by (assume_tac 1);
  13.427 -by (blast_tac (claset() addIs [real_mult_order]) 1);
  13.428 +Goal "[| (0::real) < r1; r1  < r2;  0 < y|] ==> 0 < r2 * y";
  13.429 +by (rtac real_mult_order 1); 
  13.430 +by (assume_tac 2);
  13.431 +by (blast_tac (claset() addIs [real_less_trans]) 1);
  13.432  qed "real_mult_order_trans";
  13.433  
  13.434 -Goal "[| 0r < r1; r1 <r2; 0r <= x; x < y|] ==> r1 * x < r2 * y";
  13.435 +Goal "[| (0::real) < r1; r1  < r2;  0 <= x; x < y|] ==> r1 * x < r2 * y";
  13.436  by (auto_tac (claset() addSDs [real_le_imp_less_or_eq] 
  13.437  	               addIs [real_mult_less_mono,real_mult_order_trans],
  13.438                simpset()));
  13.439  qed "real_mult_less_mono3";
  13.440  
  13.441 -Goal "[| 0r <= r1; r1 <r2; 0r <= x; x < y|] ==> r1 * x < r2 * y";
  13.442 +Goal "[| (0::real) <= r1; r1  < r2;  0 <= x; x < y|] ==> r1 * x < r2 * y";
  13.443  by (auto_tac (claset() addSDs [real_le_imp_less_or_eq] 
  13.444  	               addIs [real_mult_less_mono,real_mult_order_trans,
  13.445  			      real_mult_order],
  13.446 @@ -497,7 +555,7 @@
  13.447  by (blast_tac (claset() addIs [real_mult_order]) 1);
  13.448  qed "real_mult_less_mono4";
  13.449  
  13.450 -Goal "[| 0r < r1; r1 <= r2; 0r <= x; x <= y |] ==> r1 * x <= r2 * y";
  13.451 +Goal "[| (0::real) < r1; r1 <= r2;  0 <= x; x <= y |] ==> r1 * x <= r2 * y";
  13.452  by (rtac real_less_or_eq_imp_le 1);
  13.453  by (REPEAT(dtac real_le_imp_less_or_eq 1));
  13.454  by (auto_tac (claset() addIs [real_mult_less_mono,
  13.455 @@ -505,7 +563,7 @@
  13.456  	      simpset()));
  13.457  qed "real_mult_le_mono";
  13.458  
  13.459 -Goal "[| 0r < r1; r1 < r2; 0r <= x; x <= y |] ==> r1 * x <= r2 * y";
  13.460 +Goal "[| (0::real) < r1; r1 < r2;  0 <= x; x <= y |] ==> r1 * x <= r2 * y";
  13.461  by (rtac real_less_or_eq_imp_le 1);
  13.462  by (REPEAT(dtac real_le_imp_less_or_eq 1));
  13.463  by (auto_tac (claset() addIs [real_mult_less_mono, real_mult_order_trans,
  13.464 @@ -513,20 +571,20 @@
  13.465  	      simpset()));
  13.466  qed "real_mult_le_mono2";
  13.467  
  13.468 -Goal "[| 0r <= r1; r1 < r2; 0r <= x; x <= y |] ==> r1 * x <= r2 * y";
  13.469 +Goal "[| (0::real) <= r1; r1 < r2;  0 <= x; x <= y |] ==> r1 * x <= r2 * y";
  13.470  by (dtac real_le_imp_less_or_eq 1);
  13.471  by (auto_tac (claset() addIs [real_mult_le_mono2],simpset()));
  13.472  by (dtac real_le_trans 1 THEN assume_tac 1);
  13.473  by (auto_tac (claset() addIs [real_less_le_mult_order], simpset()));
  13.474  qed "real_mult_le_mono3";
  13.475  
  13.476 -Goal "[| 0r <= r1; r1 <= r2; 0r <= x; x <= y |] ==> r1 * x <= r2 * y";
  13.477 +Goal "[| (0::real) <= r1; r1 <= r2;  0 <= x; x <= y |] ==> r1 * x <= r2 * y";
  13.478  by (dres_inst_tac [("x","r1")] real_le_imp_less_or_eq 1);
  13.479  by (auto_tac (claset() addIs [real_mult_le_mono3, real_mult_le_le_mono1],
  13.480  	      simpset()));
  13.481  qed "real_mult_le_mono4";
  13.482  
  13.483 -Goal "1r <= x ==> 0r < x";
  13.484 +Goal "1r <= x ==> 0 < x";
  13.485  by (rtac ccontr 1 THEN dtac real_leI 1);
  13.486  by (dtac real_le_trans 1 THEN assume_tac 1);
  13.487  by (auto_tac (claset() addDs [real_zero_less_one RSN (2,real_le_less_trans)],
  13.488 @@ -562,8 +620,7 @@
  13.489  qed "real_gt_half_sum";
  13.490  
  13.491  Goal "x < y ==> EX r::real. x < r & r < y";
  13.492 -by (blast_tac (claset() addSIs [real_less_half_sum,
  13.493 -				real_gt_half_sum]) 1);
  13.494 +by (blast_tac (claset() addSIs [real_less_half_sum, real_gt_half_sum]) 1);
  13.495  qed "real_dense";
  13.496  
  13.497  Goal "(EX n. rinv(real_of_posnat n) < r) = (EX n. 1r < r * real_of_posnat n)";
  13.498 @@ -603,7 +660,7 @@
  13.499  
  13.500  Addsimps [real_of_posnat_less_iff];
  13.501  
  13.502 -Goal "0r < u  ==> (u < rinv (real_of_posnat n)) = (real_of_posnat n < rinv(u))";
  13.503 +Goal "0 < u  ==> (u < rinv (real_of_posnat n)) = (real_of_posnat n < rinv(u))";
  13.504  by (Step_tac 1);
  13.505  by (res_inst_tac [("n2","n")] (real_of_posnat_less_zero RS 
  13.506      real_rinv_gt_zero RS real_mult_less_cancel1) 1);
  13.507 @@ -620,13 +677,13 @@
  13.508      real_not_refl2 RS not_sym,real_mult_assoc RS sym]));
  13.509  qed "real_of_posnat_less_rinv_iff";
  13.510  
  13.511 -Goal "0r < u ==> (u = rinv(real_of_posnat n)) = (real_of_posnat n = rinv u)";
  13.512 +Goal "0 < u ==> (u = rinv(real_of_posnat n)) = (real_of_posnat n = rinv u)";
  13.513  by (auto_tac (claset(),
  13.514  	      simpset() addsimps [real_rinv_rinv,
  13.515      real_of_posnat_less_zero,real_not_refl2 RS not_sym]));
  13.516  qed "real_of_posnat_rinv_eq_iff";
  13.517  
  13.518 -Goal "[| 0r < r; r < x |] ==> rinv x < rinv r";
  13.519 +Goal "[| 0 < r; r < x |] ==> rinv x < rinv r";
  13.520  by (ftac real_less_trans 1 THEN assume_tac 1);
  13.521  by (ftac real_rinv_gt_zero 1);
  13.522  by (forw_inst_tac [("x","x")] real_rinv_gt_zero 1);
  13.523 @@ -641,7 +698,7 @@
  13.524           not_sym RS real_mult_inv_left,real_mult_assoc RS sym]) 1);
  13.525  qed "real_rinv_less_swap";
  13.526  
  13.527 -Goal "[| 0r < r; 0r < x|] ==> (r < x) = (rinv x < rinv r)";
  13.528 +Goal "[| 0 < r; 0 < x|] ==> (r < x) = (rinv x < rinv r)";
  13.529  by (auto_tac (claset() addIs [real_rinv_less_swap],simpset()));
  13.530  by (res_inst_tac [("t","r")] (real_rinv_rinv RS subst) 1);
  13.531  by (etac (real_not_refl2 RS not_sym) 1);
  13.532 @@ -676,7 +733,7 @@
  13.533  qed "real_add_minus_rinv_real_of_posnat_le";
  13.534  Addsimps [real_add_minus_rinv_real_of_posnat_le];
  13.535  
  13.536 -Goal "0r < r ==> r*(1r + (-rinv(real_of_posnat n))) < r";
  13.537 +Goal "0 < r ==> r*(1r + (-rinv(real_of_posnat n))) < r";
  13.538  by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1);
  13.539  by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1);
  13.540  by (auto_tac (claset() addIs [real_mult_order],
  13.541 @@ -685,44 +742,43 @@
  13.542  				  real_minus_zero_less_iff2]));
  13.543  qed "real_mult_less_self";
  13.544  
  13.545 -Goal "0r <= 1r + (-rinv(real_of_posnat n))";
  13.546 +Goal "0 <= 1r + (-rinv(real_of_posnat n))";
  13.547  by (res_inst_tac [("C","rinv(real_of_posnat n)")] real_le_add_right_cancel 1);
  13.548  by (simp_tac (simpset() addsimps [real_add_assoc,
  13.549  				  real_of_posnat_rinv_le_iff]) 1);
  13.550  qed "real_add_one_minus_rinv_ge_zero";
  13.551  
  13.552 -Goal "0r < r ==> 0r <= r*(1r + (-rinv(real_of_posnat n)))";
  13.553 +Goal "0 < r ==> 0 <= r*(1r + (-rinv(real_of_posnat n)))";
  13.554  by (dtac (real_add_one_minus_rinv_ge_zero RS real_mult_le_less_mono1) 1);
  13.555  by Auto_tac;
  13.556  qed "real_mult_add_one_minus_ge_zero";
  13.557  
  13.558 -Goal "x*y = 0r ==> x = 0r | y = 0r";
  13.559 -by (auto_tac (claset() addIs [ccontr] addDs [real_mult_not_zero],
  13.560 -	      simpset()));
  13.561 -qed "real_mult_zero_disj";
  13.562 - 
  13.563 -Goal "x + x*y = x*(1r + y)";
  13.564 -by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1);
  13.565 -qed "real_add_mult_distrib_one";
  13.566 +Goal "(x*y = 0) = (x = 0 | y = (0::real))";
  13.567 +by Auto_tac;
  13.568 +by (blast_tac (claset() addIs [ccontr] addDs [real_mult_not_zero]) 1);
  13.569 +qed "real_mult_is_0";
  13.570  
  13.571 -Goal "[| x ~= 1r; y * x = y |] ==> y = 0r";
  13.572 -by (dtac (sym RS (real_eq_minus_iff RS iffD1)) 1);
  13.573 -by (dtac sym 1);
  13.574 -by (asm_full_simp_tac (simpset() addsimps [real_minus_mult_eq2,
  13.575 -    real_add_mult_distrib_one]) 1);
  13.576 -by (dtac real_mult_zero_disj 1);
  13.577 +Goal "(0 = x*y) = (0 = x | (0::real) = y)";
  13.578 +by (stac eq_commute 1 THEN stac real_mult_is_0 1);
  13.579 +by Auto_tac;
  13.580 +qed "real_0_is_mult";
  13.581 +AddIffs [real_mult_is_0, real_0_is_mult];
  13.582 +
  13.583 +Goal "[| x ~= 1r; y * x = y |] ==> y = 0";
  13.584 +by (subgoal_tac "y*(1r + -x) = 0" 1);
  13.585 +by (stac real_add_mult_distrib2 2);
  13.586  by (auto_tac (claset(),
  13.587  	      simpset() addsimps [real_eq_minus_iff2 RS sym]));
  13.588  qed "real_mult_eq_self_zero";
  13.589  Addsimps [real_mult_eq_self_zero];
  13.590  
  13.591 -Goal "[| x ~= 1r; y = y * x |] ==> y = 0r";
  13.592 +Goal "[| x ~= 1r; y = y * x |] ==> y = 0";
  13.593  by (dtac sym 1);
  13.594  by (Asm_full_simp_tac 1);
  13.595  qed "real_mult_eq_self_zero2";
  13.596  Addsimps [real_mult_eq_self_zero2];
  13.597  
  13.598 -Goal "[| 0r <= x*y; 0r < x |] ==> 0r <= y";
  13.599 +Goal "[| 0 <= x*y; 0 < x |] ==> (0::real) <= y";
  13.600  by (ftac real_rinv_gt_zero 1);
  13.601  by (dres_inst_tac [("x","rinv x")] real_less_le_mult_order 1);
  13.602  by (dtac (real_not_refl2 RS not_sym RS real_mult_inv_left) 2);
  13.603 @@ -730,7 +786,7 @@
  13.604  	      simpset() addsimps [real_mult_assoc RS sym]));
  13.605  qed "real_mult_ge_zero_cancel";
  13.606  
  13.607 -Goal "[|x ~= 0r; y ~= 0r |] ==> rinv(x) + rinv(y) = (x + y)*rinv(x*y)";
  13.608 +Goal "[|x ~= 0; y ~= 0 |] ==> rinv(x) + rinv(y) = (x + y)*rinv(x*y)";
  13.609  by (asm_full_simp_tac (simpset() addsimps 
  13.610  		       [real_rinv_distrib,real_add_mult_distrib,
  13.611  			real_mult_assoc RS sym]) 1);
  13.612 @@ -740,37 +796,74 @@
  13.613  qed "real_rinv_add";
  13.614  
  13.615  (* 05/00 *)
  13.616 -Goal "(0r <= -R) = (R <= 0r)";
  13.617 +Goal "(0 <= -R) = (R <= (0::real))";
  13.618  by (auto_tac (claset() addDs [sym],
  13.619      simpset() addsimps [real_le_less]));
  13.620  qed "real_minus_zero_le_iff";
  13.621  
  13.622 -Goal "(-R <= 0r) = (0r <= R)";
  13.623 +Goal "(-R <= 0) = ((0::real) <= R)";
  13.624  by (auto_tac (claset(),simpset() addsimps 
  13.625      [real_minus_zero_less_iff2,real_le_less]));
  13.626  qed "real_minus_zero_le_iff2";
  13.627  
  13.628 -Goal "-(x*x) <= 0r";
  13.629 +Goal "-(x*x) <= (0::real)";
  13.630  by (simp_tac (simpset() addsimps [real_minus_zero_le_iff2]) 1);
  13.631  qed "real_minus_squre_le_zero";
  13.632  Addsimps [real_minus_squre_le_zero];
  13.633  
  13.634 -Goal "x * x + y * y = 0r ==> x = 0r";
  13.635 +Goal "x * x + y * y = 0 ==> x = (0::real)";
  13.636  by (dtac real_add_minus_eq_minus 1);
  13.637  by (cut_inst_tac [("x","x")] real_le_square 1);
  13.638  by (Auto_tac THEN dtac real_le_anti_sym 1);
  13.639 -by (auto_tac (claset() addDs [real_mult_zero_disj],simpset()));
  13.640 +by Auto_tac;
  13.641  qed "real_sum_squares_cancel";
  13.642  
  13.643 -Goal "x * x + y * y = 0r ==> y = 0r";
  13.644 +Goal "x * x + y * y = 0 ==> y = (0::real)";
  13.645  by (res_inst_tac [("y","x")] real_sum_squares_cancel 1);
  13.646  by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
  13.647  qed "real_sum_squares_cancel2";
  13.648  
  13.649  (*----------------------------------------------------------------------------
  13.650 +     Some convenient biconditionals for products of signs (lcp)
  13.651 + ----------------------------------------------------------------------------*)
  13.652 +
  13.653 +Goal "((0::real) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)";
  13.654 +by (auto_tac (claset(), 
  13.655 +              simpset() addsimps [order_le_less, real_less_le_iff, 
  13.656 +                                  real_mult_order, real_mult_less_zero1]));
  13.657 +by (ALLGOALS (rtac ccontr)); 
  13.658 +by (auto_tac (claset(), simpset() addsimps [order_le_less, real_less_le_iff]));
  13.659 +by (ALLGOALS (etac rev_mp)); 
  13.660 +by (ALLGOALS (dtac real_mult_less_zero THEN' assume_tac));
  13.661 +by (auto_tac (claset() addDs [order_less_not_sym], 
  13.662 +              simpset() addsimps [real_mult_commute]));  
  13.663 +qed "real_zero_less_times_iff";
  13.664 +
  13.665 +Goal "((0::real) <= x*y) = (0 <= x & 0 <= y | x <= 0 & y <= 0)";
  13.666 +by (auto_tac (claset(), 
  13.667 +              simpset() addsimps [order_le_less, real_less_le_iff,  
  13.668 +                                  real_zero_less_times_iff]));
  13.669 +qed "real_zero_le_times_iff";
  13.670 +
  13.671 +Goal "(x*y < (0::real)) = (0 < x & y < 0 | x < 0 & 0 < y)";
  13.672 +by (auto_tac (claset(), 
  13.673 +              simpset() addsimps [real_zero_le_times_iff, 
  13.674 +                                  linorder_not_le RS sym]));
  13.675 +by (auto_tac (claset() addDs [order_less_not_sym],  
  13.676 +              simpset() addsimps [linorder_not_le]));
  13.677 +qed "real_times_less_zero_iff";
  13.678 +
  13.679 +Goal "(x*y <= (0::real)) = (0 <= x & y <= 0 | x <= 0 & 0 <= y)";
  13.680 +by (auto_tac (claset() addDs [order_less_not_sym], 
  13.681 +              simpset() addsimps [real_zero_less_times_iff, 
  13.682 +                                  linorder_not_less RS sym]));
  13.683 +qed "real_times_le_zero_iff";
  13.684 +
  13.685 +
  13.686 +(*----------------------------------------------------------------------------
  13.687       Another embedding of the naturals in the reals (see real_of_posnat)
  13.688   ----------------------------------------------------------------------------*)
  13.689 -Goalw [real_of_nat_def] "real_of_nat 0 = 0r";
  13.690 +Goalw [real_of_nat_def] "real_of_nat 0 = 0";
  13.691  by (full_simp_tac (simpset() addsimps [real_of_posnat_one]) 1);
  13.692  qed "real_of_nat_zero";
  13.693  
  13.694 @@ -801,7 +894,7 @@
  13.695  	      simpset() addsimps [real_of_nat_def,real_add_right_cancel]));
  13.696  qed "inj_real_of_nat";
  13.697  
  13.698 -Goalw [real_of_nat_def] "0r <= real_of_nat n";
  13.699 +Goalw [real_of_nat_def] "0 <= real_of_nat n";
  13.700  by (res_inst_tac [("C","1r")] real_le_add_right_cancel 1);
  13.701  by (asm_full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
  13.702  qed "real_of_nat_ge_zero";
  13.703 @@ -844,7 +937,7 @@
  13.704  by (etac real_of_nat_minus 1);
  13.705  qed "real_of_nat_diff2";
  13.706  
  13.707 -Goal "(real_of_nat n ~= 0r) = (n ~= 0)";
  13.708 +Goal "(real_of_nat n ~= 0) = (n ~= 0)";
  13.709  by (auto_tac (claset() addIs [inj_real_of_nat RS injD],
  13.710      simpset() addsimps [real_of_nat_zero RS sym] 
  13.711      delsimps [neq0_conv]));
    14.1 --- a/src/HOL/Real/RealOrd.thy	Wed Jun 07 12:07:07 2000 +0200
    14.2 +++ b/src/HOL/Real/RealOrd.thy	Wed Jun 07 12:14:18 2000 +0200
    14.3 @@ -2,7 +2,8 @@
    14.4      ID: 	 $Id$
    14.5      Author:      Jacques D. Fleuriot and Lawrence C. Paulson
    14.6      Copyright:   1998  University of Cambridge
    14.7 -    Description: Type "real" is a linear order
    14.8 +    Description: Type "real" is a linear order and also 
    14.9 +                 satisfies plus_ac0: + is an AC-operator with zero
   14.10  *)
   14.11  
   14.12  RealOrd = RealDef +
   14.13 @@ -10,4 +11,6 @@
   14.14  instance real :: order (real_le_refl,real_le_trans,real_le_anti_sym,real_less_le)
   14.15  instance real :: linorder (real_le_linear)
   14.16  
   14.17 +instance real :: plus_ac0 (real_add_commute,real_add_assoc,real_add_zero_left)
   14.18 +
   14.19  end
    15.1 --- a/src/HOL/Real/RealPow.ML	Wed Jun 07 12:07:07 2000 +0200
    15.2 +++ b/src/HOL/Real/RealPow.ML	Wed Jun 07 12:14:18 2000 +0200
    15.3 @@ -12,13 +12,12 @@
    15.4  
    15.5  Goal "r ~= (#0::real) --> r ^ n ~= #0";
    15.6  by (induct_tac "n" 1);
    15.7 -by (auto_tac (claset() addIs [real_mult_not_zeroE],
    15.8 -    simpset() addsimps [real_zero_not_eq_one RS not_sym]));
    15.9 +by Auto_tac; 
   15.10  qed_spec_mp "realpow_not_zero";
   15.11  
   15.12  Goal "r ^ n = (#0::real) ==> r = #0";
   15.13  by (rtac ccontr 1);
   15.14 -by (auto_tac (claset() addDs [realpow_not_zero],simpset()));
   15.15 +by (auto_tac (claset() addDs [realpow_not_zero], simpset()));
   15.16  qed "realpow_zero_zero";
   15.17  
   15.18  Goal "r ~= #0 --> rinv(r ^ n) = (rinv r) ^ n";
   15.19 @@ -383,65 +382,57 @@
   15.20  goalw RealPow.thy [real_diff_def] 
   15.21        "((x::real) ^ 2 = y ^ 2) = (x = y | x = -y)";
   15.22  by (auto_tac (claset(),simpset() delsimps [realpow_Suc]));
   15.23 -by (dtac (rename_numerals thy ((real_eq_minus_iff RS iffD1) 
   15.24 -    RS sym)) 1);
   15.25 -by (auto_tac (claset() addSDs [full_rename_numerals thy 
   15.26 -    real_mult_zero_disj] addDs [full_rename_numerals thy 
   15.27 -    real_add_minus_eq_minus], simpset() addsimps 
   15.28 -    [realpow_two_add_minus] delsimps [realpow_Suc]));
   15.29 +by (dtac (rename_numerals thy (real_eq_minus_iff RS iffD1 RS sym)) 1);
   15.30 +by (auto_tac (claset() addDs [full_rename_numerals thy real_add_minus_eq_minus], 
   15.31 +          simpset() addsimps [realpow_two_add_minus] delsimps [realpow_Suc]));
   15.32  qed "realpow_two_disj";
   15.33  
   15.34  (* used in Transc *)
   15.35 -Goal  "!!x. [|x ~= #0; m <= n |] ==> \
   15.36 -\      x ^ (n - m) = x ^ n * rinv(x ^ m)";
   15.37 -by (auto_tac (claset(),simpset() addsimps [le_eq_less_or_eq,
   15.38 -    less_iff_Suc_add,realpow_add,
   15.39 -    realpow_not_zero] @ real_mult_ac));
   15.40 +Goal  "[|x ~= #0; m <= n |] ==> x ^ (n - m) = x ^ n * rinv(x ^ m)";
   15.41 +by (auto_tac (claset(),
   15.42 +              simpset() addsimps [le_eq_less_or_eq,
   15.43 +                                  less_iff_Suc_add,realpow_add,
   15.44 +                                  realpow_not_zero] @ real_mult_ac));
   15.45  qed "realpow_diff";
   15.46  
   15.47  Goal "real_of_nat (m) ^ n = real_of_nat (m ^ n)";
   15.48  by (induct_tac "n" 1);
   15.49 -by (auto_tac (claset(),simpset() addsimps [real_of_nat_one,
   15.50 -    real_of_nat_mult]));
   15.51 +by (auto_tac (claset(),
   15.52 +              simpset() addsimps [real_of_nat_one, real_of_nat_mult]));
   15.53  qed "realpow_real_of_nat";
   15.54  
   15.55  Goal "#0 < real_of_nat (2 ^ n)";
   15.56  by (induct_tac "n" 1);
   15.57  by (auto_tac (claset() addSIs [full_rename_numerals thy real_mult_order],
   15.58 -    simpset() addsimps [real_of_nat_mult RS sym,real_of_nat_one]));
   15.59 +              simpset() addsimps [real_of_nat_mult RS sym,real_of_nat_one]));
   15.60  by (simp_tac (simpset() addsimps [rename_numerals thy 
   15.61 -    (real_of_nat_zero RS sym)]) 1);
   15.62 +                                  (real_of_nat_zero RS sym)]) 1);
   15.63  qed "realpow_real_of_nat_two_pos";
   15.64  Addsimps [realpow_real_of_nat_two_pos];
   15.65  
   15.66 -(* FIXME: annoyingly long proof! *)
   15.67 +
   15.68 +
   15.69 +
   15.70 +(***	REALORD.ML, AFTER real_rinv_less_iff ***)
   15.71 +Goal "[| 0 < r; 0 < x|] ==> (rinv x <= rinv r) = (r <= x)";
   15.72 +by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym, 
   15.73 +                                      real_rinv_less_iff]) 1); 
   15.74 +qed "real_rinv_le_iff";
   15.75 +
   15.76  Goal "(#0::real) <= x & #0 <= y &  x ^ Suc n <= y ^ Suc n --> x <= y";
   15.77  by (induct_tac "n" 1);
   15.78 -by (Auto_tac);
   15.79 +by Auto_tac;
   15.80  by (dtac not_real_leE 1);
   15.81 -by (auto_tac (claset() addDs [real_less_asym],
   15.82 -    simpset() addsimps [real_le_less]));
   15.83 -by (forw_inst_tac [("r","y")] 
   15.84 -    (full_rename_numerals thy real_rinv_less_swap) 1);
   15.85 -by (rtac real_linear_less2 2);
   15.86 -by (rtac real_linear_less2 5);
   15.87 -by (dtac (full_rename_numerals thy 
   15.88 -    ((real_not_refl2 RS not_sym) RS real_mult_not_zero)) 9);
   15.89 -by (Auto_tac);
   15.90 -by (forw_inst_tac [("t","#0")] (real_not_refl2 RS not_sym) 1);
   15.91 -by (forward_tac [full_rename_numerals thy real_rinv_gt_zero] 1);
   15.92 -by (forw_inst_tac [("t","#0")] (real_not_refl2 RS not_sym) 3);
   15.93 -by (dtac (full_rename_numerals thy real_rinv_gt_zero) 3);
   15.94 -by (dtac (full_rename_numerals thy real_mult_less_zero) 3);
   15.95 -by (forw_inst_tac [("x","(y * y ^ n)"),("r1.0","y")] 
   15.96 -    (full_rename_numerals thy real_mult_less_mono) 2);
   15.97 -by (dres_inst_tac [("x","x * (x * x ^ n)"),("r1.0","rinv x")] 
   15.98 -    (full_rename_numerals thy real_mult_less_mono) 1);
   15.99 -by (Auto_tac);
  15.100 -by (auto_tac (claset() addIs (map (full_rename_numerals thy ) 
  15.101 -    [real_mult_order,realpow_gt_zero]),
  15.102 -    simpset() addsimps [real_mult_assoc 
  15.103 -    RS sym,real_not_refl2 RS not_sym]));
  15.104 +by (auto_tac (claset(), 
  15.105 +              simpset() addsimps [inst "x" "#0" order_le_less,
  15.106 +                                  real_times_le_0_iff])); 
  15.107 +by (subgoal_tac "rinv x * (x * (x * x ^ n)) <= rinv y * (y * (y * y ^ n))" 1);
  15.108 +by (rtac real_mult_le_mono 2);
  15.109 +by (asm_full_simp_tac (simpset() addsimps [realpow_ge_zero, real_0_le_times_iff]) 4); 
  15.110 +by (asm_full_simp_tac (simpset() addsimps [real_rinv_le_iff]) 3);
  15.111 +by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
  15.112 +by (rtac real_rinv_gt_zero 1);  
  15.113 +by Auto_tac; 
  15.114  qed_spec_mp "realpow_increasing";
  15.115    
  15.116  Goal "(#0::real) <= x & #0 <= y &  x ^ Suc n = y ^ Suc n --> x = y";