--- a/src/HOL/Real/RealDef.ML Wed Jul 28 22:01:58 1999 +0200
+++ b/src/HOL/Real/RealDef.ML Thu Jul 29 12:44:57 1999 +0200
@@ -206,20 +206,20 @@
qed "real_add_zero_right";
Addsimps [real_add_zero_right];
-Goalw [real_zero_def] "z + -z = 0r";
+Goalw [real_zero_def] "z + (-z) = 0r";
by (res_inst_tac [("z","z")] eq_Abs_real 1);
by (asm_full_simp_tac (simpset() addsimps [real_minus,
real_add, preal_add_commute]) 1);
qed "real_add_minus";
Addsimps [real_add_minus];
-Goal "-z + z = 0r";
+Goal "(-z) + z = 0r";
by (simp_tac (simpset() addsimps [real_add_commute]) 1);
qed "real_add_minus_left";
Addsimps [real_add_minus_left];
-Goal "z + (- z + w) = (w::real)";
+Goal "z + ((- z) + w) = (w::real)";
by (simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
qed "real_add_minus_cancel";
@@ -259,7 +259,7 @@
by (Fast_tac 1);
qed "real_as_add_inverse_ex";
-Goal "-(x + y) = -x + -(y::real)";
+Goal "-(x + y) = (-x) + (- y :: real)";
by (res_inst_tac [("z","x")] eq_Abs_real 1);
by (res_inst_tac [("z","y")] eq_Abs_real 1);
by (auto_tac (claset(),simpset() addsimps [real_minus,real_add]));
@@ -269,7 +269,7 @@
Goal "((x::real) + y = x + z) = (y = z)";
by (Step_tac 1);
-by (dres_inst_tac [("f","%t.-x + t")] arg_cong 1);
+by (dres_inst_tac [("f","%t. (-x) + t")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
qed "real_add_left_cancel";
@@ -277,18 +277,18 @@
by (simp_tac (simpset() addsimps [real_add_commute,real_add_left_cancel]) 1);
qed "real_add_right_cancel";
-Goal "((x::real) = y) = (0r = x + - y)";
+Goal "((x::real) = y) = (0r = x + (- y))";
by (Step_tac 1);
by (res_inst_tac [("x1","-y")]
(real_add_right_cancel RS iffD1) 2);
-by (Auto_tac);
+by Auto_tac;
qed "real_eq_minus_iff";
-Goal "((x::real) = y) = (x + - y = 0r)";
+Goal "((x::real) = y) = (x + (- y) = 0r)";
by (Step_tac 1);
by (res_inst_tac [("x1","-y")]
(real_add_right_cancel RS iffD1) 2);
-by (Auto_tac);
+by Auto_tac;
qed "real_eq_minus_iff2";
Goal "0r - x = -x";
@@ -391,7 +391,7 @@
Addsimps [real_mult_0_right, real_mult_0];
-Goal "-(x * y) = -x * (y::real)";
+Goal "-(x * y) = (-x) * (y::real)";
by (res_inst_tac [("z","x")] eq_Abs_real 1);
by (res_inst_tac [("z","y")] eq_Abs_real 1);
by (auto_tac (claset(),
@@ -399,7 +399,7 @@
@ preal_mult_ac @ preal_add_ac));
qed "real_minus_mult_eq1";
-Goal "-(x * y) = x * -(y::real)";
+Goal "-(x * y) = x * (- y :: real)";
by (res_inst_tac [("z","x")] eq_Abs_real 1);
by (res_inst_tac [("z","y")] eq_Abs_real 1);
by (auto_tac (claset(),
@@ -407,34 +407,34 @@
@ preal_mult_ac @ preal_add_ac));
qed "real_minus_mult_eq2";
-Goal "- 1r * z = -z";
+Goal "(- 1r) * z = -z";
by (simp_tac (simpset() addsimps [real_minus_mult_eq1 RS sym]) 1);
qed "real_mult_minus_1";
Addsimps [real_mult_minus_1];
-Goal "z * - 1r = -z";
+Goal "z * (- 1r) = -z";
by (stac real_mult_commute 1);
by (Simp_tac 1);
qed "real_mult_minus_1_right";
Addsimps [real_mult_minus_1_right];
-Goal "-x * -y = x * (y::real)";
+Goal "(-x) * (-y) = x * (y::real)";
by (full_simp_tac (simpset() addsimps [real_minus_mult_eq2 RS sym,
- real_minus_mult_eq1 RS sym]) 1);
+ real_minus_mult_eq1 RS sym]) 1);
qed "real_minus_mult_cancel";
Addsimps [real_minus_mult_cancel];
-Goal "-x * y = x * -(y::real)";
+Goal "(-x) * y = x * (- y :: real)";
by (full_simp_tac (simpset() addsimps [real_minus_mult_eq2 RS sym,
- real_minus_mult_eq1 RS sym]) 1);
+ real_minus_mult_eq1 RS sym]) 1);
qed "real_minus_mult_commute";
(*-----------------------------------------------------------------------------
- -----------------------------------------------------------------------------*)
+ ----------------------------------------------------------------------------*)
(** Lemmas **)
@@ -493,17 +493,17 @@
Goal "!!(x::real). x ~= 0r ==> ? y. y*x = 1r";
by (asm_simp_tac (simpset() addsimps [real_mult_commute,
- real_mult_inv_right_ex]) 1);
+ real_mult_inv_right_ex]) 1);
qed "real_mult_inv_left_ex";
-Goalw [rinv_def] "!!(x::real). x ~= 0r ==> rinv(x)*x = 1r";
+Goalw [rinv_def] "x ~= 0r ==> rinv(x)*x = 1r";
by (forward_tac [real_mult_inv_left_ex] 1);
by (Step_tac 1);
by (rtac selectI2 1);
by Auto_tac;
qed "real_mult_inv_left";
-Goal "!!(x::real). x ~= 0r ==> x*rinv(x) = 1r";
+Goal "x ~= 0r ==> x*rinv(x) = 1r";
by (auto_tac (claset() addIs [real_mult_commute RS subst],
simpset() addsimps [real_mult_inv_left]));
qed "real_mult_inv_right";
@@ -517,15 +517,16 @@
Goal "(c::real) ~= 0r ==> (a*c=b*c) = (a=b)";
by (Step_tac 1);
by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1);
-by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac) 1);
+by (asm_full_simp_tac
+ (simpset() addsimps [real_mult_inv_right] @ real_mult_ac) 1);
qed "real_mult_right_cancel";
-Goal "!!a. c*a ~= c*b ==> a ~= b";
-by (Auto_tac);
+Goal "c*a ~= c*b ==> a ~= b";
+by Auto_tac;
qed "real_mult_left_cancel_ccontr";
-Goal "!!a. a*c ~= b*c ==> a ~= b";
-by (Auto_tac);
+Goal "a*c ~= b*c ==> a ~= b";
+by Auto_tac;
qed "real_mult_right_cancel_ccontr";
Goalw [rinv_def] "x ~= 0r ==> rinv(x) ~= 0r";
@@ -539,7 +540,7 @@
Addsimps [real_mult_inv_left,real_mult_inv_right];
-Goal "!!x. [| x ~= 0r; y ~= 0r |] ==> x * y ~= 0r";
+Goal "[| x ~= 0r; y ~= 0r |] ==> x * y ~= 0r";
by (Step_tac 1);
by (dres_inst_tac [("f","%z. rinv x*z")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
@@ -569,8 +570,7 @@
by Auto_tac;
qed "real_minus_rinv";
-Goal "!!x y. [| x ~= 0r; y ~= 0r |] \
-\ ==> rinv(x*y) = rinv(x)*rinv(y)";
+Goal "[| x ~= 0r; y ~= 0r |] ==> rinv(x*y) = rinv(x)*rinv(y)";
by (forw_inst_tac [("y","y")] real_mult_not_zero 1 THEN assume_tac 1);
by (res_inst_tac [("c1","x")] (real_mult_left_cancel RS iffD1) 1);
by (auto_tac (claset(),simpset() addsimps [real_mult_assoc RS sym]));
@@ -778,7 +778,7 @@
addEs [real_less_irrefl]) 1);
qed "real_of_preal_not_less_zero";
-Goal "0r < - - real_of_preal m";
+Goal "0r < - (- real_of_preal m)";
by (simp_tac (simpset() addsimps
[real_of_preal_zero_less]) 1);
qed "real_minus_minus_zero_less";
@@ -970,7 +970,7 @@
qed "real_minus_zero_less_iff2";
(*Alternative definition for real_less*)
-Goal "!!(R::real). R < S ==> ? T. 0r < T & R + T = S";
+Goal "R < S ==> ? T. 0r < T & R + T = S";
by (res_inst_tac [("x","R")] real_of_preal_trichotomyE 1);
by (ALLGOALS(res_inst_tac [("x","S")] real_of_preal_trichotomyE));
by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
@@ -988,19 +988,19 @@
qed "real_less_add_positive_left_Ex";
(** change naff name(s)! **)
-Goal "(W < S) ==> (0r < S + -W)";
+Goal "(W < S) ==> (0r < S + (-W))";
by (dtac real_less_add_positive_left_Ex 1);
by (auto_tac (claset(),
simpset() addsimps [real_add_minus,
real_add_zero_right] @ real_add_ac));
qed "real_less_sum_gt_zero";
-Goal "!!S::real. T = S + W ==> S = T + -W";
+Goal "!!S::real. T = S + W ==> S = T + (-W)";
by (asm_simp_tac (simpset() addsimps real_add_ac) 1);
qed "real_lemma_change_eq_subj";
(* FIXME: long! *)
-Goal "(0r < S + -W) ==> (W < S)";
+Goal "(0r < S + (-W)) ==> (W < S)";
by (rtac ccontr 1);
by (dtac (real_leI RS real_le_imp_less_or_eq) 1);
by (auto_tac (claset(),
@@ -1015,7 +1015,7 @@
by (auto_tac (claset() addEs [real_less_asym], simpset()));
qed "real_sum_gt_zero_less";
-Goal "(0r < S + -W) = (W < S)";
+Goal "(0r < S + (-W)) = (W < S)";
by (blast_tac (claset() addIs [real_less_sum_gt_zero,
real_sum_gt_zero_less]) 1);
qed "real_less_sum_gt_0_iff";