added parentheses to cope with a possible reduction of the precedence of unary
authorpaulson
Thu Jul 29 12:44:57 1999 +0200 (1999-07-29)
changeset 712748e235179ffb
parent 7126 fdb397af4cab
child 7128 468b6c8b8dc4
added parentheses to cope with a possible reduction of the precedence of unary
minus
src/HOL/HOL.thy
src/HOL/Hoare/Arith2.ML
src/HOL/Hoare/Hoare.ML
src/HOL/Integ/IntDef.ML
src/HOL/Integ/IntDef.thy
src/HOL/Integ/IntDiv.ML
src/HOL/Integ/NatBin.ML
src/HOL/Real/Hyperreal/Filter.ML
src/HOL/Real/RComplete.ML
src/HOL/Real/Real.ML
src/HOL/Real/RealAbs.ML
src/HOL/Real/RealDef.ML
src/HOL/Real/RealDef.thy
src/HOL/UNITY/Deadlock.ML
src/HOL/equalities.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/HOL.thy	Wed Jul 28 22:01:58 1999 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu Jul 29 12:44:57 1999 +0200
     1.3 @@ -70,7 +70,7 @@
     1.4  consts
     1.5    "+"           :: ['a::plus, 'a]  => 'a            (infixl 65)
     1.6    "-"           :: ['a::minus, 'a] => 'a            (infixl 65)
     1.7 -  uminus        :: ['a::minus] => 'a                ("- _" [100] 100)
     1.8 +  uminus        :: ['a::minus] => 'a                ("- _" [71] 70)
     1.9    "*"           :: ['a::times, 'a] => 'a            (infixl 70)
    1.10    (*See Nat.thy for "^"*)
    1.11  
     2.1 --- a/src/HOL/Hoare/Arith2.ML	Wed Jul 28 22:01:58 1999 +0200
     2.2 +++ b/src/HOL/Hoare/Arith2.ML	Thu Jul 29 12:44:57 1999 +0200
     2.3 @@ -9,40 +9,26 @@
     2.4  open Arith2;
     2.5  
     2.6  
     2.7 -(*** HOL lemmas ***)
     2.8 -
     2.9 -
    2.10 -val [prem1,prem2]=goal HOL.thy "[|~P ==> ~Q; Q|] ==> P";
    2.11 -by (cut_facts_tac [prem1 COMP impI,prem2] 1);
    2.12 -by (Fast_tac 1);
    2.13 -val not_imp_swap=result();
    2.14 -
    2.15 -
    2.16 -
    2.17  (*** cd ***)
    2.18  
    2.19  
    2.20 -val prems=goalw thy [cd_def] "0<n ==> cd n n n";
    2.21 -by (cut_facts_tac prems 1);
    2.22 +Goalw [cd_def] "0<n ==> cd n n n";
    2.23  by (Asm_simp_tac 1);
    2.24  qed "cd_nnn";
    2.25  
    2.26 -val prems=goalw thy [cd_def] "[| cd x m n; 0<m; 0<n |] ==> x<=m & x<=n";
    2.27 -by (cut_facts_tac prems 1);
    2.28 +Goalw [cd_def] "[| cd x m n; 0<m; 0<n |] ==> x<=m & x<=n";
    2.29  by (blast_tac (claset() addIs [dvd_imp_le]) 1);
    2.30  qed "cd_le";
    2.31  
    2.32 -val prems=goalw thy [cd_def] "cd x m n = cd x n m";
    2.33 +Goalw [cd_def] "cd x m n = cd x n m";
    2.34  by (Fast_tac 1);
    2.35  qed "cd_swap";
    2.36  
    2.37 -val prems=goalw thy [cd_def] "n<=m ==> cd x m n = cd x (m-n) n";
    2.38 -by (cut_facts_tac prems 1);
    2.39 +Goalw [cd_def] "n<=m ==> cd x m n = cd x (m-n) n";
    2.40  by (blast_tac (claset() addIs [dvd_diff] addDs [dvd_diffD]) 1);
    2.41  qed "cd_diff_l";
    2.42  
    2.43 -val prems=goalw thy [cd_def] "m<=n ==> cd x m n = cd x m (n-m)";
    2.44 -by (cut_facts_tac prems 1);
    2.45 +Goalw [cd_def] "m<=n ==> cd x m n = cd x m (n-m)";
    2.46  by (blast_tac (claset() addIs [dvd_diff] addDs [dvd_diffD]) 1);
    2.47  qed "cd_diff_r";
    2.48  
    2.49 @@ -60,16 +46,14 @@
    2.50  by (simp_tac (simpset() addsimps [cd_swap]) 1);
    2.51  qed "gcd_swap";
    2.52  
    2.53 -val prems=goalw thy [gcd_def] "n<=m ==> gcd m n = gcd (m-n) n";
    2.54 -by (cut_facts_tac prems 1);
    2.55 +Goalw [gcd_def] "n<=m ==> gcd m n = gcd (m-n) n";
    2.56  by (subgoal_tac "n<=m ==> !x. cd x m n = cd x (m-n) n" 1);
    2.57  by (Asm_simp_tac 1);
    2.58  by (rtac allI 1);
    2.59  by (etac cd_diff_l 1);
    2.60  qed "gcd_diff_l";
    2.61  
    2.62 -val prems=goalw thy [gcd_def] "m<=n ==> gcd m n = gcd m (n-m)";
    2.63 -by (cut_facts_tac prems 1);
    2.64 +Goalw [gcd_def] "m<=n ==> gcd m n = gcd m (n-m)";
    2.65  by (subgoal_tac "m<=n ==> !x. cd x m n = cd x m (n-m)" 1);
    2.66  by (Asm_simp_tac 1);
    2.67  by (rtac allI 1);
    2.68 @@ -79,11 +63,10 @@
    2.69  
    2.70  (*** pow ***)
    2.71  
    2.72 -val prems = goal Power.thy "m mod 2 = 0 ==> ((n::nat)*n)^(m div 2) = n^m";
    2.73 +Goal "m mod 2 = 0 ==> ((n::nat)*n)^(m div 2) = n^m";
    2.74  by (subgoal_tac "n*n=n^2" 1);
    2.75 -by (etac ssubst 1);
    2.76 -by (stac (power_mult RS sym) 1);
    2.77 +by (etac ssubst 1 THEN stac (power_mult RS sym) 1);
    2.78  by (stac mult_div_cancel 1);
    2.79 -by (ALLGOALS(simp_tac (simpset() addsimps prems)));
    2.80 +by (ALLGOALS Asm_simp_tac);
    2.81  qed "sq_pow_div2";
    2.82  Addsimps [sq_pow_div2];
     3.1 --- a/src/HOL/Hoare/Hoare.ML	Wed Jul 28 22:01:58 1999 +0200
     3.2 +++ b/src/HOL/Hoare/Hoare.ML	Thu Jul 29 12:44:57 1999 +0200
     3.3 @@ -38,7 +38,7 @@
     3.4  val lemma = result() RS spec RS spec RS mp RS mp;
     3.5  
     3.6  Goalw [Valid_def]
     3.7 - "[| p <= i; Valid (i Int b) c i; (i Int -b) <= q |] \
     3.8 + "[| p <= i; Valid (i Int b) c i;  i Int (-b) <= q |] \
     3.9  \ ==> Valid p (WHILE b INV {i} DO c OD) q";
    3.10  by (Asm_simp_tac 1);
    3.11  by (Clarify_tac 1);
     4.1 --- a/src/HOL/Integ/IntDef.ML	Wed Jul 28 22:01:58 1999 +0200
     4.2 +++ b/src/HOL/Integ/IntDef.ML	Thu Jul 29 12:44:57 1999 +0200
     4.3 @@ -180,7 +180,7 @@
     4.4      (simpset() addsimps [zadd_ize UN_equiv_class2]) 1);
     4.5  qed "zadd";
     4.6  
     4.7 -Goal "- (z + w) = - z + - (w::int)";
     4.8 +Goal "- (z + w) = (- z) + (- w::int)";
     4.9  by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
    4.10  by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
    4.11  by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1);
    4.12 @@ -612,7 +612,7 @@
    4.13  
    4.14  Goal "!!w::int. (z + w' = z + w) = (w' = w)";
    4.15  by Safe_tac;
    4.16 -by (dres_inst_tac [("f", "%x. x + -z")] arg_cong 1);
    4.17 +by (dres_inst_tac [("f", "%x. x + (-z)")] arg_cong 1);
    4.18  by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
    4.19  qed "zadd_left_cancel";
    4.20  
     5.1 --- a/src/HOL/Integ/IntDef.thy	Wed Jul 28 22:01:58 1999 +0200
     5.2 +++ b/src/HOL/Integ/IntDef.thy	Thu Jul 29 12:44:57 1999 +0200
     5.3 @@ -39,7 +39,7 @@
     5.4         Abs_Integ(UN p1:Rep_Integ(z). UN p2:Rep_Integ(w).   
     5.5             split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)"
     5.6  
     5.7 -  zdiff_def "z - w == z + -(w::int)"
     5.8 +  zdiff_def "z - (w::int) == z + (-w)"
     5.9  
    5.10    zless_def "z<w == neg(z - w)"
    5.11  
     6.1 --- a/src/HOL/Integ/IntDiv.ML	Wed Jul 28 22:01:58 1999 +0200
     6.2 +++ b/src/HOL/Integ/IntDiv.ML	Thu Jul 29 12:44:57 1999 +0200
     6.3 @@ -761,7 +761,7 @@
     6.4  val lemma1 = result();
     6.5  
     6.6  Goal "[| b < (#0::int);  c ~= #0 |] ==> (c*a) div (c*b) = a div b";
     6.7 -by (subgoal_tac "(c * -a) div (c * -b) = -a div -b" 1);
     6.8 +by (subgoal_tac "(c * (-a)) div (c * (-b)) = (-a) div (-b)" 1);
     6.9  by (rtac lemma1 2);
    6.10  by (auto_tac (claset(), simpset() addsimps [zmult_zminus_right]));
    6.11  val lemma2 = result();
    6.12 @@ -789,7 +789,7 @@
    6.13  val lemma1 = result();
    6.14  
    6.15  Goal "[| b < (#0::int);  c ~= #0 |] ==> (c*a) mod (c*b) = c * (a mod b)";
    6.16 -by (subgoal_tac "(c * -a) mod (c * -b) = c * (-a mod -b)" 1);
    6.17 +by (subgoal_tac "(c * (-a)) mod (c * (-b)) = c * ((-a) mod (-b))" 1);
    6.18  by (rtac lemma1 2);
    6.19  by (auto_tac (claset(), 
    6.20  	      simpset() addsimps [zmult_zminus_right, zmod_zminus_zminus]));
    6.21 @@ -838,12 +838,11 @@
    6.22  
    6.23  
    6.24  Goal "a <= (#0::int) ==> (#1 + #2*b) div (#2*a) = (b+#1) div a";
    6.25 -by (subgoal_tac "(#1 + #2*(-b-#1)) div (#2 * -a) = (-b-#1) div (-a)" 1);
    6.26 +by (subgoal_tac "(#1 + #2*(-b-#1)) div (#2 * (-a)) = (-b-#1) div (-a)" 1);
    6.27  by (rtac pos_zdiv_times_2 2);
    6.28  by (auto_tac (claset(),
    6.29  	      simpset() addsimps [zmult_zminus_right]));
    6.30 -by Auto_tac;
    6.31 -by (subgoal_tac "(#-1 + - (#2 * b)) = - (#1 + (#2 * b))" 1);
    6.32 +by (subgoal_tac "(#-1 - (#2 * b)) = - (#1 + (#2 * b))" 1);
    6.33  by (Simp_tac 2);
    6.34  by (asm_full_simp_tac (HOL_ss
    6.35  		       addsimps [zdiv_zminus_zminus, zdiff_def,
    6.36 @@ -899,11 +898,11 @@
    6.37  
    6.38  Goal "a <= (#0::int) ==> (#1 + #2*b) mod (#2*a) = #2 * ((b+#1) mod a) - #1";
    6.39  by (subgoal_tac 
    6.40 -    "(#1 + #2*(-b-#1)) mod (#2*-a) = #1 + #2*((-b-#1) mod (-a))" 1);
    6.41 +    "(#1 + #2*(-b-#1)) mod (#2*(-a)) = #1 + #2*((-b-#1) mod (-a))" 1);
    6.42  by (rtac pos_zmod_times_2 2);
    6.43  by (auto_tac (claset(),
    6.44  	      simpset() addsimps [zmult_zminus_right]));
    6.45 -by (subgoal_tac "(#-1 + - (#2 * b)) = - (#1 + (#2 * b))" 1);
    6.46 +by (subgoal_tac "(#-1 - (#2 * b)) = - (#1 + (#2 * b))" 1);
    6.47  by (Simp_tac 2);
    6.48  by (asm_full_simp_tac (HOL_ss
    6.49  		       addsimps [zmod_zminus_zminus, zdiff_def,
    6.50 @@ -938,19 +937,19 @@
    6.51  by (rtac order_trans 1);
    6.52  by (res_inst_tac [("a'","#-1")]  zdiv_mono1 1);
    6.53  by (auto_tac (claset(), simpset() addsimps [zdiv_minus1]));
    6.54 -qed "div_neg_pos";
    6.55 +qed "div_neg_pos_less0";
    6.56  
    6.57  Goal "[| (#0::int) <= a;  b < #0 |] ==> a div b <= #0";
    6.58  by (dtac zdiv_mono1_neg 1);
    6.59  by Auto_tac;
    6.60 -qed "div_nonneg_neg";
    6.61 +qed "div_nonneg_neg_le0";
    6.62  
    6.63  Goal "(#0::int) < b ==> (#0 <= a div b) = (#0 <= a)";
    6.64  by Auto_tac;
    6.65  by (dtac zdiv_mono1 2);
    6.66  by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff]));
    6.67  by (full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
    6.68 -by (blast_tac (claset() addIs [div_neg_pos]) 1);
    6.69 +by (blast_tac (claset() addIs [div_neg_pos_less0]) 1);
    6.70  qed "pos_imp_zdiv_nonneg_iff";
    6.71  
    6.72  Goal "b < (#0::int) ==> (#0 <= a div b) = (a <= (#0::int))";
     7.1 --- a/src/HOL/Integ/NatBin.ML	Wed Jul 28 22:01:58 1999 +0200
     7.2 +++ b/src/HOL/Integ/NatBin.ML	Thu Jul 29 12:44:57 1999 +0200
     7.3 @@ -146,7 +146,7 @@
     7.4  Goal "(#0::int) <= z ==> nat z div nat z' = nat (z div z')";
     7.5  by (case_tac "#0 <= z'" 1);
     7.6  by (auto_tac (claset(), 
     7.7 -	      simpset() addsimps [div_nonneg_neg, DIVISION_BY_ZERO_DIV]));
     7.8 +	      simpset() addsimps [div_nonneg_neg_le0, DIVISION_BY_ZERO_DIV]));
     7.9  by (zdiv_undefined_case_tac "z' = #0" 1);
    7.10   by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_DIV]) 1);
    7.11  by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
     8.1 --- a/src/HOL/Real/Hyperreal/Filter.ML	Wed Jul 28 22:01:58 1999 +0200
     8.2 +++ b/src/HOL/Real/Hyperreal/Filter.ML	Thu Jul 29 12:44:57 1999 +0200
     8.3 @@ -4,9 +4,6 @@
     8.4      Description : Filters and Ultrafilter
     8.5  *) 
     8.6  
     8.7 -open Filter;
     8.8 -
     8.9 -
    8.10  (*------------------------------------------------------------------
    8.11        Properties of Filters and Freefilters - 
    8.12        rules for intro, destruction etc.
    8.13 @@ -290,7 +287,7 @@
    8.14               A few properties of freefilters
    8.15   -------------------------------------------------------------------*)
    8.16  
    8.17 -Goal "F1 Int F2 = ((F1 Int Y) Int F2) Un ((F2 Int - Y) Int F1)";
    8.18 +Goal "F1 Int F2 = ((F1 Int Y) Int F2) Un ((F2 Int (- Y)) Int F1)";
    8.19  by (Auto_tac);
    8.20  qed "lemma_Compl_cancel_eq";
    8.21  
    8.22 @@ -303,7 +300,7 @@
    8.23  qed "finite_IntI2";
    8.24  
    8.25  Goal "[| finite (F1 Int Y); \
    8.26 -\                 finite (F2 Int - Y) \
    8.27 +\                 finite (F2 Int (- Y)) \
    8.28  \              |] ==> finite (F1 Int F2)";
    8.29  by (res_inst_tac [("Y1","Y")] (lemma_Compl_cancel_eq RS ssubst) 1);
    8.30  by (rtac finite_UnI 1);
    8.31 @@ -403,7 +400,7 @@
    8.32     We prove: 1. Existence of maximal filter i.e. ultrafilter
    8.33               2. Freeness property i.e ultrafilter is free
    8.34               Use a locale to prove various lemmas and then 
    8.35 -             export main result- The Ultrafilter Theorem
    8.36 +             export main result: The Ultrafilter Theorem
    8.37   -------------------------------------------------------------------*)
    8.38  Open_locale "UFT"; 
    8.39  
    8.40 @@ -516,8 +513,9 @@
    8.41  by (res_inst_tac [("x","Union c")] bexI 1 THEN Blast_tac 1);
    8.42  by (rtac Un_chain_mem_cofinite_Filter_set 1 THEN REPEAT(assume_tac 1));
    8.43  by (res_inst_tac [("x","frechet (UNIV)")] bexI 1 THEN Blast_tac 1);
    8.44 -by (auto_tac (claset(),simpset() addsimps 
    8.45 -        [thm "superfrechet_def", thm "frechet_def"]));
    8.46 +by (auto_tac (claset(),
    8.47 +	      simpset() addsimps 
    8.48 +	      [thm "superfrechet_def", thm "frechet_def"]));
    8.49  qed "max_cofinite_Filter_Ex";
    8.50  
    8.51  Goal "EX U: superfrechet UNIV. (\
     9.1 --- a/src/HOL/Real/RComplete.ML	Wed Jul 28 22:01:58 1999 +0200
     9.2 +++ b/src/HOL/Real/RComplete.ML	Thu Jul 29 12:44:57 1999 +0200
     9.3 @@ -5,9 +5,6 @@
     9.4                    reals and reals 
     9.5  *) 
     9.6  
     9.7 -
     9.8 -open RComplete;
     9.9 -
    9.10  claset_ref() := claset() delWrapper "bspec";
    9.11  
    9.12  (*---------------------------------------------------------
    9.13 @@ -20,15 +17,14 @@
    9.14  \       ((? x:P. y < x) = (? X. real_of_preal X : P & \
    9.15  \                          y < real_of_preal X))";
    9.16  by (blast_tac (claset() addSDs [bspec,
    9.17 -    real_gt_zero_preal_Ex RS iffD1]) 1);
    9.18 +				real_gt_zero_preal_Ex RS iffD1]) 1);
    9.19  qed "real_sup_lemma1";
    9.20  
    9.21  Goal "[| ! x:P. 0r < x; ? x. x: P; ? y. !x: P. x < y |] \
    9.22  \         ==> (? X. X: {w. real_of_preal w : P}) & \
    9.23  \             (? Y. !X: {w. real_of_preal w : P}. X < Y)";
    9.24  by (rtac conjI 1);
    9.25 -by (blast_tac (claset() addDs [bspec,
    9.26 -    real_gt_zero_preal_Ex RS iffD1]) 1);
    9.27 +by (blast_tac (claset() addDs [bspec, real_gt_zero_preal_Ex RS iffD1]) 1);
    9.28  by Auto_tac;
    9.29  by (dtac bspec 1 THEN assume_tac 1);
    9.30  by (forward_tac [bspec] 1  THEN assume_tac 1);
    9.31 @@ -65,7 +61,7 @@
    9.32  by (rtac (real_sup_lemma1 RS iffD2) 1 THEN assume_tac 1);
    9.33  by (case_tac "0r < ya" 1);
    9.34  by (auto_tac (claset() addSDs [real_less_all_real2,
    9.35 -        real_gt_zero_preal_Ex RS iffD1],simpset()));
    9.36 +			       real_gt_zero_preal_Ex RS iffD1],simpset()));
    9.37  by (forward_tac [real_sup_lemma2] 2 THEN Auto_tac);
    9.38  by (forward_tac [real_sup_lemma2] 1 THEN Auto_tac);
    9.39  by (rtac (preal_complete RS spec RS iffD2 RS bexE) 1);
    9.40 @@ -79,15 +75,14 @@
    9.41     Completeness properties using isUb, isLub etc.
    9.42   -------------------------------------------------------*)
    9.43  
    9.44 -Goal "!!(x::real). [| isLub R S x; isLub R S y |] ==> x = y";
    9.45 +Goal "[| isLub R S x; isLub R S y |] ==> x = (y::real)";
    9.46  by (forward_tac [isLub_isUb] 1);
    9.47  by (forw_inst_tac [("x","y")] isLub_isUb 1);
    9.48  by (blast_tac (claset() addSIs [real_le_anti_sym]
    9.49 -                addSDs [isLub_le_isUb]) 1);
    9.50 +                        addSDs [isLub_le_isUb]) 1);
    9.51  qed "real_isLub_unique";
    9.52  
    9.53 -Goalw [setle_def,setge_def] 
    9.54 -         "!!x::real. [| x <=* S'; S <= S' |] ==> x <=* S";
    9.55 +Goalw [setle_def,setge_def] "[| (x::real) <=* S'; S <= S' |] ==> x <=* S";
    9.56  by (Blast_tac 1);
    9.57  qed "real_order_restrict";
    9.58  
    9.59 @@ -96,13 +91,14 @@
    9.60   ----------------------------------------------------------------*)
    9.61  
    9.62  Goal "[| ALL x: S. 0r < x; \
    9.63 -\                 EX x. x: S; \
    9.64 -\                 EX u. isUb (UNIV::real set) S u \
    9.65 -\              |] ==> EX t. isLub (UNIV::real set) S t";
    9.66 +\        EX x. x: S; \
    9.67 +\        EX u. isUb (UNIV::real set) S u \
    9.68 +\     |] ==> EX t. isLub (UNIV::real set) S t";
    9.69  by (res_inst_tac [("x","real_of_preal(psup({w. real_of_preal w : S}))")] exI 1);
    9.70  by (auto_tac (claset(), simpset() addsimps [isLub_def,leastP_def,isUb_def]));
    9.71  by (auto_tac (claset() addSIs [setleI,setgeI] 
    9.72 -	               addSDs [real_gt_zero_preal_Ex RS iffD1],simpset()));
    9.73 +	               addSDs [real_gt_zero_preal_Ex RS iffD1],
    9.74 +	      simpset()));
    9.75  by (forw_inst_tac [("x","y")] bspec 1 THEN assume_tac 1);
    9.76  by (dtac (real_gt_zero_preal_Ex RS iffD1) 1);
    9.77  by (auto_tac (claset(), simpset() addsimps [real_of_preal_le_iff]));
    9.78 @@ -125,38 +121,39 @@
    9.79  (*-------------------------------
    9.80      Lemmas
    9.81   -------------------------------*)
    9.82 -Goal "! y : {z. ? x: P. z = x + -xa + 1r} Int {x. 0r < x}. 0r < y";
    9.83 +Goal "! y : {z. ? x: P. z = x + (-xa) + 1r} Int {x. 0r < x}. 0r < y";
    9.84  by Auto_tac;
    9.85  qed "real_sup_lemma3";
    9.86   
    9.87 -Goal "(xa <= S + X + -Z) = (xa + -X + Z <= (S::real))";
    9.88 +Goal "(xa <= S + X + (-Z)) = (xa + (-X) + Z <= (S::real))";
    9.89  by (simp_tac (simpset() addsimps [real_diff_def, real_diff_le_eq RS sym] @
    9.90  	                         real_add_ac) 1);
    9.91  qed "lemma_le_swap2";
    9.92  
    9.93 -Goal "[| 0r < x + -X + 1r; x < xa |] ==> 0r < xa + -X + 1r";
    9.94 +Goal "[| 0r < x + (-X) + 1r; x < xa |] ==> 0r < xa + (-X) + 1r";
    9.95  by (dtac real_add_less_mono 1);
    9.96  by (assume_tac 1);
    9.97  by (dres_inst_tac [("C","-x"),("A","0r + x")] real_add_less_mono2 1);
    9.98 -by (asm_full_simp_tac (simpset() addsimps [real_add_zero_right,
    9.99 -    real_add_assoc RS sym,real_add_minus_left,real_add_zero_left]) 1);
   9.100 +by (asm_full_simp_tac
   9.101 +    (simpset() addsimps [real_add_zero_right, real_add_assoc RS sym,
   9.102 +			 real_add_minus_left,real_add_zero_left]) 1);
   9.103  by (asm_full_simp_tac (simpset() addsimps real_add_ac) 1);
   9.104  qed "lemma_real_complete1";
   9.105  
   9.106 -Goal "!!x. [| x + -X + 1r <= S; xa < x |] ==> xa + -X + 1r <= S";
   9.107 +Goal "[| x + (-X) + 1r <= S; xa < x |] ==> xa + (-X) + 1r <= S";
   9.108  by (dtac real_less_imp_le 1);
   9.109  by (dtac real_add_le_mono 1);
   9.110  by (assume_tac 1);
   9.111  by (asm_full_simp_tac (simpset() addsimps real_add_ac) 1);
   9.112  qed "lemma_real_complete2";
   9.113  
   9.114 -Goal "[| x + -X + 1r <= S; xa < x |] ==> xa <= S + X + -1r"; (**)
   9.115 +Goal "[| x + (-X) + 1r <= S; xa < x |] ==> xa <= S + X + (-1r)"; (**)
   9.116  by (rtac (lemma_le_swap2 RS iffD2) 1);
   9.117  by (etac lemma_real_complete2 1);
   9.118  by (assume_tac 1);
   9.119  qed "lemma_real_complete2a";
   9.120  
   9.121 -Goal "[| x + -X + 1r <= S; xa <= x |] ==> xa <= S + X + -1r";
   9.122 +Goal "[| x + (-X) + 1r <= S; xa <= x |] ==> xa <= S + X + (-1r)";
   9.123  by (rotate_tac 1 1);
   9.124  by (etac (real_le_imp_less_or_eq RS disjE) 1);
   9.125  by (blast_tac (claset() addIs [lemma_real_complete2a]) 1);
   9.126 @@ -166,22 +163,22 @@
   9.127  (*------------------------------------
   9.128        reals Completeness (again!)
   9.129   ------------------------------------*)
   9.130 -Goal "!!(S::real set). [| EX X. X: S; \
   9.131 -\                             EX Y. isUb (UNIV::real set) S Y \
   9.132 -\                          |] ==> EX t. isLub (UNIV :: real set) S t";
   9.133 +Goal "[| EX X. X: S;  EX Y. isUb (UNIV::real set) S Y |]  \
   9.134 +\     ==> EX t. isLub (UNIV :: real set) S t";
   9.135  by (Step_tac 1);
   9.136 -by (subgoal_tac "? u. u: {z. ? x: S. z = x + -X + 1r} \
   9.137 +by (subgoal_tac "? u. u: {z. ? x: S. z = x + (-X) + 1r} \
   9.138  \                Int {x. 0r < x}" 1);
   9.139 -by (subgoal_tac "isUb (UNIV::real set) ({z. ? x: S. z = x + -X + 1r} \
   9.140 -\                Int {x. 0r < x})  (Y + -X + 1r)" 1); 
   9.141 +by (subgoal_tac "isUb (UNIV::real set) ({z. ? x: S. z = x + (-X) + 1r} \
   9.142 +\                Int {x. 0r < x})  (Y + (-X) + 1r)" 1); 
   9.143  by (cut_inst_tac [("P","S"),("xa","X")] real_sup_lemma3 1);
   9.144 -by (EVERY1[forward_tac [exI RSN (3,posreals_complete)], Blast_tac, Blast_tac, Step_tac]);
   9.145 -by (res_inst_tac [("x","t + X + -1r")] exI 1);
   9.146 +by (EVERY1[forward_tac [exI RSN (3,posreals_complete)], Blast_tac, Blast_tac, 
   9.147 +	   Step_tac]);
   9.148 +by (res_inst_tac [("x","t + X + (-1r)")] exI 1);
   9.149  by (rtac isLubI2 1);
   9.150  by (rtac setgeI 2 THEN Step_tac 2);
   9.151 -by (subgoal_tac "isUb (UNIV:: real set) ({z. ? x: S. z = x + -X + 1r} \
   9.152 -\                Int {x. 0r < x})  (y + -X + 1r)" 2); 
   9.153 -by (dres_inst_tac [("y","(y + - X + 1r)")] isLub_le_isUb 2 
   9.154 +by (subgoal_tac "isUb (UNIV:: real set) ({z. ? x: S. z = x + (-X) + 1r} \
   9.155 +\                Int {x. 0r < x})  (y + (-X) + 1r)" 2); 
   9.156 +by (dres_inst_tac [("y","(y + (- X) + 1r)")] isLub_le_isUb 2 
   9.157        THEN assume_tac 2);
   9.158  by (full_simp_tac
   9.159      (simpset() addsimps [real_diff_def, real_diff_le_eq RS sym] @
   9.160 @@ -230,9 +227,9 @@
   9.161  by (asm_full_simp_tac
   9.162      (simpset() addsimps [real_le_diff_eq RS sym, real_diff_def]) 1);
   9.163  by (subgoal_tac "isUb (UNIV::real set) \
   9.164 -\   {z. EX n. z = x*(real_of_posnat n)} (t + -x)" 1);
   9.165 +\   {z. EX n. z = x*(real_of_posnat n)} (t + (-x))" 1);
   9.166  by (blast_tac (claset() addSIs [isUbI,setleI]) 2);
   9.167 -by (dres_inst_tac [("y","t+-x")] isLub_le_isUb 1);
   9.168 +by (dres_inst_tac [("y","t+(-x)")] isLub_le_isUb 1);
   9.169  by (dres_inst_tac [("x","-t")] real_add_left_le_mono1 2);
   9.170  by (auto_tac (claset() addDs [real_le_less_trans,
   9.171  			      (real_minus_zero_less_iff2 RS iffD2)], 
    10.1 --- a/src/HOL/Real/Real.ML	Wed Jul 28 22:01:58 1999 +0200
    10.2 +++ b/src/HOL/Real/Real.ML	Thu Jul 29 12:44:57 1999 +0200
    10.3 @@ -6,10 +6,10 @@
    10.4  *)
    10.5  
    10.6  Goal "(0r < x) = (? y. x = real_of_preal y)";
    10.7 -by (auto_tac (claset(),simpset() addsimps [real_of_preal_zero_less]));
    10.8 +by (auto_tac (claset(), simpset() addsimps [real_of_preal_zero_less]));
    10.9  by (cut_inst_tac [("x","x")] real_of_preal_trichotomy 1);
   10.10  by (blast_tac (claset() addSEs [real_less_irrefl,
   10.11 -     real_of_preal_not_minus_gt_zero RS notE]) 1);
   10.12 +				real_of_preal_not_minus_gt_zero RS notE]) 1);
   10.13  qed "real_gt_zero_preal_Ex";
   10.14  
   10.15  Goal "real_of_preal z < x ==> ? y. x = real_of_preal y";
   10.16 @@ -19,12 +19,12 @@
   10.17  
   10.18  Goal "real_of_preal z <= x ==> ? y. x = real_of_preal y";
   10.19  by (blast_tac (claset() addDs [real_le_imp_less_or_eq,
   10.20 -              real_gt_preal_preal_Ex]) 1);
   10.21 +			       real_gt_preal_preal_Ex]) 1);
   10.22  qed "real_ge_preal_preal_Ex";
   10.23  
   10.24  Goal "y <= 0r ==> !x. y < real_of_preal x";
   10.25  by (auto_tac (claset() addEs [real_le_imp_less_or_eq RS disjE]
   10.26 -              addIs [real_of_preal_zero_less RSN(2,real_less_trans)],
   10.27 +                       addIs [real_of_preal_zero_less RSN(2,real_less_trans)],
   10.28                simpset() addsimps [real_of_preal_zero_less]));
   10.29  qed "real_less_all_preal";
   10.30  
   10.31 @@ -43,12 +43,12 @@
   10.32  by (auto_tac (claset(), simpset() addsimps real_add_ac));
   10.33  qed "real_lemma_add_positive_imp_less";
   10.34  
   10.35 -Goal "!!(R::real). ? T. 0r < T & R + T = S ==> R < S";
   10.36 +Goal "? T. 0r < T & R + T = S ==> R < S";
   10.37  by (blast_tac (claset() addIs [real_lemma_add_positive_imp_less]) 1);
   10.38  qed "real_ex_add_positive_left_less";
   10.39  
   10.40  (*Alternative definition for real_less.  NOT for rewriting*)
   10.41 -Goal "!!(R::real). (R < S) = (? T. 0r < T & R + T = S)";
   10.42 +Goal "(R < S) = (? T. 0r < T & R + T = S)";
   10.43  by (blast_tac (claset() addSIs [real_less_add_positive_left_Ex,
   10.44  				real_ex_add_positive_left_less]) 1);
   10.45  qed "real_less_iff_add";
   10.46 @@ -62,7 +62,7 @@
   10.47  by (blast_tac (claset() addIs [real_less_trans]) 2);
   10.48  by (auto_tac (claset(),
   10.49  	      simpset() addsimps 
   10.50 -	      [real_gt_zero_preal_Ex,real_of_preal_minus_less_self]));
   10.51 + 	        [real_gt_zero_preal_Ex,real_of_preal_minus_less_self]));
   10.52  qed "real_gt_zero_iff";
   10.53  
   10.54  Goal "(x < 0r) = (x < -x)";
   10.55 @@ -72,11 +72,11 @@
   10.56  qed "real_lt_zero_iff";
   10.57  
   10.58  Goalw [real_le_def] "(0r <= x) = (-x <= x)";
   10.59 -by (auto_tac (claset(),simpset() addsimps [real_lt_zero_iff RS sym]));
   10.60 +by (auto_tac (claset(), simpset() addsimps [real_lt_zero_iff RS sym]));
   10.61  qed "real_ge_zero_iff";
   10.62  
   10.63  Goalw [real_le_def] "(x <= 0r) = (x <= -x)";
   10.64 -by (auto_tac (claset(),simpset() addsimps [real_gt_zero_iff RS sym]));
   10.65 +by (auto_tac (claset(), simpset() addsimps [real_gt_zero_iff RS sym]));
   10.66  qed "real_le_zero_iff";
   10.67  
   10.68  Goal "(real_of_preal m1 <= real_of_preal m2) = (m1 <= m2)";
   10.69 @@ -86,31 +86,31 @@
   10.70  by (etac preal_less_irrefl 1);
   10.71  qed "real_of_preal_le_iff";
   10.72  
   10.73 -Goal "!!(x::real). [| 0r < x; 0r < y |] ==> 0r < x * y";
   10.74 -by (auto_tac (claset(),simpset() addsimps [real_gt_zero_preal_Ex]));  
   10.75 +Goal "[| 0r < x; 0r < y |] ==> 0r < x * y";
   10.76 +by (auto_tac (claset(), simpset() addsimps [real_gt_zero_preal_Ex]));  
   10.77  by (res_inst_tac [("x","y*ya")] exI 1);
   10.78  by (full_simp_tac (simpset() addsimps [real_of_preal_mult]) 1);
   10.79  qed "real_mult_order";
   10.80  
   10.81 -Goal "!!(x::real). [| x < 0r; y < 0r |] ==> 0r < x * y";
   10.82 +Goal "[| x < 0r; y < 0r |] ==> 0r < x * y";
   10.83  by (REPEAT(dtac (real_minus_zero_less_iff RS iffD2) 1));
   10.84  by (dtac real_mult_order 1 THEN assume_tac 1);
   10.85  by (Asm_full_simp_tac 1);
   10.86  qed "real_mult_less_zero1";
   10.87  
   10.88 -Goal "!!(x::real). [| 0r <= x; 0r <= y |] ==> 0r <= x * y";
   10.89 +Goal "[| 0r <= x; 0r <= y |] ==> 0r <= x * y";
   10.90  by (REPEAT(dtac real_le_imp_less_or_eq 1));
   10.91  by (auto_tac (claset() addIs [real_mult_order, real_less_imp_le],
   10.92  	      simpset()));
   10.93  qed "real_le_mult_order";
   10.94  
   10.95 -Goal "!!(x::real). [| 0r < x; 0r <= y |] ==> 0r <= x * y";
   10.96 +Goal "[| 0r < x; 0r <= y |] ==> 0r <= x * y";
   10.97  by (dtac real_le_imp_less_or_eq 1);
   10.98  by (auto_tac (claset() addIs [real_mult_order,
   10.99 -    real_less_imp_le],simpset()));
  10.100 +			      real_less_imp_le],simpset()));
  10.101  qed "real_less_le_mult_order";
  10.102  
  10.103 -Goal "!!(x::real). [| x <= 0r; y <= 0r |] ==> 0r <= x * y";
  10.104 +Goal "[| x <= 0r; y <= 0r |] ==> 0r <= x * y";
  10.105  by (rtac real_less_or_eq_imp_le 1);
  10.106  by (dtac real_le_imp_less_or_eq 1 THEN etac disjE 1);
  10.107  by Auto_tac;
  10.108 @@ -118,17 +118,17 @@
  10.109  by (auto_tac (claset() addDs [real_mult_less_zero1],simpset()));
  10.110  qed "real_mult_le_zero1";
  10.111  
  10.112 -Goal "!!(x::real). [| 0r <= x; y < 0r |] ==> x * y <= 0r";
  10.113 +Goal "[| 0r <= x; y < 0r |] ==> x * y <= 0r";
  10.114  by (rtac real_less_or_eq_imp_le 1);
  10.115  by (dtac real_le_imp_less_or_eq 1 THEN etac disjE 1);
  10.116  by Auto_tac;
  10.117  by (dtac (real_minus_zero_less_iff RS iffD2) 1);
  10.118  by (rtac (real_minus_zero_less_iff RS subst) 1);
  10.119  by (blast_tac (claset() addDs [real_mult_order] 
  10.120 -    addIs [real_minus_mult_eq2 RS ssubst]) 1);
  10.121 +	                addIs [real_minus_mult_eq2 RS ssubst]) 1);
  10.122  qed "real_mult_le_zero";
  10.123  
  10.124 -Goal "!!(x::real). [| 0r < x; y < 0r |] ==> x*y < 0r";
  10.125 +Goal "[| 0r < x; y < 0r |] ==> x*y < 0r";
  10.126  by (dtac (real_minus_zero_less_iff RS iffD2) 1);
  10.127  by (dtac real_mult_order 1 THEN assume_tac 1);
  10.128  by (rtac (real_minus_zero_less_iff RS iffD1) 1);
  10.129 @@ -137,7 +137,7 @@
  10.130  
  10.131  Goalw [real_one_def] "0r < 1r";
  10.132  by (auto_tac (claset() addIs [real_gt_zero_preal_Ex RS iffD2],
  10.133 -    simpset() addsimps [real_of_preal_def]));
  10.134 +	      simpset() addsimps [real_of_preal_def]));
  10.135  qed "real_zero_less_one";
  10.136  
  10.137  (*** Monotonicity results ***)
  10.138 @@ -204,7 +204,7 @@
  10.139  by (Full_simp_tac 1);
  10.140  qed "real_add_order";
  10.141  
  10.142 -Goal "!!(x::real). [| 0r <= x; 0r <= y |] ==> 0r <= x + y";
  10.143 +Goal "[| 0r <= x; 0r <= y |] ==> 0r <= x + y";
  10.144  by (REPEAT(dtac real_le_imp_less_or_eq 1));
  10.145  by (auto_tac (claset() addIs [real_add_order, real_less_imp_le],
  10.146  	      simpset()));
  10.147 @@ -228,12 +228,12 @@
  10.148  
  10.149  Goal "EX (x::real). x < y";
  10.150  by (rtac (real_add_zero_right RS subst) 1);
  10.151 -by (res_inst_tac [("x","y + -1r")] exI 1);
  10.152 +by (res_inst_tac [("x","y + (-1r)")] exI 1);
  10.153  by (auto_tac (claset() addSIs [real_add_less_mono2],
  10.154  	  simpset() addsimps [real_minus_zero_less_iff2, real_zero_less_one]));
  10.155  qed "real_less_Ex";
  10.156  
  10.157 -Goal "!!(u::real). 0r < r ==>  u + -r < u";
  10.158 +Goal "0r < r ==>  u + (-r) < u";
  10.159  by (res_inst_tac [("C","r")] real_less_add_right_cancel 1);
  10.160  by (simp_tac (simpset() addsimps [real_add_assoc]) 1);
  10.161  qed "real_add_minus_positive_less_self";
  10.162 @@ -242,10 +242,10 @@
  10.163  by (Step_tac 1);
  10.164  by (dres_inst_tac [("x","-s")] real_add_left_le_mono1 1);
  10.165  by (dres_inst_tac [("x","r")] real_add_left_le_mono1 2);
  10.166 -by (Auto_tac);
  10.167 +by Auto_tac;
  10.168  by (dres_inst_tac [("z","-r")] real_add_le_mono1 1);
  10.169  by (dres_inst_tac [("z","s")] real_add_le_mono1 2);
  10.170 -by (auto_tac (claset(),simpset() addsimps [real_add_assoc]));
  10.171 +by (auto_tac (claset(), simpset() addsimps [real_add_assoc]));
  10.172  qed "real_le_minus_iff";
  10.173  Addsimps [real_le_minus_iff RS sym];
  10.174            
  10.175 @@ -257,14 +257,14 @@
  10.176  Goal "0r <= x*x";
  10.177  by (res_inst_tac [("R2.0","0r"),("R1.0","x")] real_linear_less2 1);
  10.178  by (auto_tac (claset() addIs [real_mult_order,
  10.179 -    real_mult_less_zero1,real_less_imp_le],
  10.180 -    simpset()));
  10.181 +			      real_mult_less_zero1,real_less_imp_le],
  10.182 +	      simpset()));
  10.183  qed "real_le_square";
  10.184  Addsimps [real_le_square];
  10.185  
  10.186 -(*---------------------------------------------------------------------------------
  10.187 +(*----------------------------------------------------------------------------
  10.188               An embedding of the naturals in the reals
  10.189 - ---------------------------------------------------------------------------------*)
  10.190 + ----------------------------------------------------------------------------*)
  10.191  
  10.192  Goalw [real_of_posnat_def] "real_of_posnat 0 = 1r";
  10.193  by (full_simp_tac (simpset() addsimps [pnat_one_iff RS sym,real_of_preal_def]) 1);
  10.194 @@ -324,7 +324,7 @@
  10.195  by (induct_tac "n" 1);
  10.196  by (auto_tac (claset(),
  10.197  	      simpset () addsimps [real_of_posnat_Suc,real_of_posnat_one,
  10.198 -				   real_of_posnat_less_zero, real_less_imp_le]));
  10.199 +			   real_of_posnat_less_zero, real_less_imp_le]));
  10.200  qed "real_of_posnat_less_one";
  10.201  Addsimps [real_of_posnat_less_one];
  10.202  
  10.203 @@ -352,7 +352,7 @@
  10.204  by (EVERY1[dtac real_le_imp_less_or_eq, Step_tac]); 
  10.205  by (dtac real_mult_less_zero1 1 THEN assume_tac 1);
  10.206  by (auto_tac (claset() addIs [real_zero_less_one RS real_less_asym],
  10.207 -    simpset() addsimps [real_minus_mult_eq1 RS sym]));
  10.208 +	      simpset() addsimps [real_minus_mult_eq1 RS sym]));
  10.209  qed "real_rinv_gt_zero";
  10.210  
  10.211  Goal "x < 0r ==> rinv x < 0r";
  10.212 @@ -360,8 +360,7 @@
  10.213  by (dtac (real_minus_zero_less_iff RS iffD2) 1);
  10.214  by (rtac (real_minus_zero_less_iff RS iffD1) 1);
  10.215  by (dtac (real_minus_rinv RS sym) 1);
  10.216 -by (auto_tac (claset() addIs [real_rinv_gt_zero],
  10.217 -    simpset()));
  10.218 +by (auto_tac (claset() addIs [real_rinv_gt_zero], simpset()));
  10.219  qed "real_rinv_less_zero";
  10.220  
  10.221  Goal "0r < rinv(real_of_posnat n)";
  10.222 @@ -400,7 +399,7 @@
  10.223  by (full_simp_tac (simpset() addsimps [real_mult_assoc]) 1);
  10.224  qed "real_sum_of_halves";
  10.225  
  10.226 -Goal "!!(x::real). [| 0r<z; x<y |] ==> x*z<y*z";       
  10.227 +Goal "[| 0r<z; x<y |] ==> x*z<y*z";       
  10.228  by (rotate_tac 1 1);
  10.229  by (dtac real_less_sum_gt_zero 1);
  10.230  by (rtac real_sum_gt_zero_less 1);
  10.231 @@ -409,11 +408,11 @@
  10.232      real_minus_mult_eq2 RS sym, real_mult_commute ]) 1);
  10.233  qed "real_mult_less_mono1";
  10.234  
  10.235 -Goal "!!(y::real). [| 0r<z; x<y |] ==> z*x<z*y";       
  10.236 +Goal "[| 0r<z; x<y |] ==> z*x<z*y";       
  10.237  by (asm_simp_tac (simpset() addsimps [real_mult_commute,real_mult_less_mono1]) 1);
  10.238  qed "real_mult_less_mono2";
  10.239  
  10.240 -Goal "!!(x::real). [| 0r<z; x*z<y*z |] ==> x<y";
  10.241 +Goal "[| 0r<z; x*z<y*z |] ==> x<y";
  10.242  by (forw_inst_tac [("x","x*z")] (real_rinv_gt_zero 
  10.243                         RS real_mult_less_mono1) 1);
  10.244  by (auto_tac (claset(),
  10.245 @@ -421,7 +420,7 @@
  10.246       [real_mult_assoc,real_not_refl2 RS not_sym]));
  10.247  qed "real_mult_less_cancel1";
  10.248  
  10.249 -Goal "!!(x::real). [| 0r<z; z*x<z*y |] ==> x<y";
  10.250 +Goal "[| 0r<z; z*x<z*y |] ==> x<y";
  10.251  by (etac real_mult_less_cancel1 1);
  10.252  by (asm_full_simp_tac (simpset() addsimps [real_mult_commute]) 1);
  10.253  qed "real_mult_less_cancel2";
  10.254 @@ -438,105 +437,107 @@
  10.255  
  10.256  Addsimps [real_mult_less_iff1,real_mult_less_iff2];
  10.257  
  10.258 -Goal "!!(x::real). [| 0r<=z; x<y |] ==> x*z<=y*z";
  10.259 +Goal "[| 0r<=z; x<y |] ==> x*z<=y*z";
  10.260  by (EVERY1 [rtac real_less_or_eq_imp_le, dtac real_le_imp_less_or_eq]);
  10.261  by (auto_tac (claset() addIs [real_mult_less_mono1],simpset()));
  10.262  qed "real_mult_le_less_mono1";
  10.263  
  10.264 -Goal "!!(x::real). [| 0r<=z; x<y |] ==> z*x<=z*y";
  10.265 +Goal "[| 0r<=z; x<y |] ==> z*x<=z*y";
  10.266  by (asm_simp_tac (simpset() addsimps [real_mult_commute,real_mult_le_less_mono1]) 1);
  10.267  qed "real_mult_le_less_mono2";
  10.268  
  10.269 -Goal "!!x y (z::real). [| 0r<=z; x<=y |] ==> z*x<=z*y";
  10.270 +Goal "[| 0r<=z; x<=y |] ==> z*x<=z*y";
  10.271  by (dres_inst_tac [("x","x")] real_le_imp_less_or_eq 1);
  10.272  by (auto_tac (claset() addIs [real_mult_le_less_mono2], simpset()));
  10.273  qed "real_mult_le_le_mono1";
  10.274  
  10.275 -Goal "!!(x::real). [| 0r < r1; r1 <r2; 0r < x; x < y|] \
  10.276 +Goal "[| 0r < r1; r1 <r2; 0r < x; x < y|] \
  10.277  \                  ==> r1 * x < r2 * y";
  10.278  by (dres_inst_tac [("x","x")] real_mult_less_mono2 1);
  10.279  by (dres_inst_tac [("R1.0","0r")] real_less_trans 2);
  10.280  by (dres_inst_tac [("x","r1")] real_mult_less_mono1 3);
  10.281 -by (Auto_tac);
  10.282 +by Auto_tac;
  10.283  by (blast_tac (claset() addIs [real_less_trans]) 1);
  10.284  qed "real_mult_less_mono";
  10.285  
  10.286 -Goal "!!(x::real). [| 0r < r1; r1 <r2; 0r < y|] \
  10.287 +Goal "[| 0r < r1; r1 <r2; 0r < y|] \
  10.288  \                           ==> 0r < r2 * y";
  10.289  by (dres_inst_tac [("R1.0","0r")] real_less_trans 1);
  10.290  by (assume_tac 1);
  10.291  by (blast_tac (claset() addIs [real_mult_order]) 1);
  10.292  qed "real_mult_order_trans";
  10.293  
  10.294 -Goal "!!(x::real). [| 0r < r1; r1 <r2; 0r <= x; x < y|] \
  10.295 +Goal "[| 0r < r1; r1 <r2; 0r <= x; x < y|] \
  10.296  \                  ==> r1 * x < r2 * y";
  10.297 -by (auto_tac (claset() addSDs [real_le_imp_less_or_eq] addIs
  10.298 -              [real_mult_less_mono,real_mult_order_trans],
  10.299 +by (auto_tac (claset() addSDs [real_le_imp_less_or_eq] 
  10.300 +	               addIs [real_mult_less_mono,real_mult_order_trans],
  10.301                simpset()));
  10.302  qed "real_mult_less_mono3";
  10.303  
  10.304 -Goal "!!(x::real). [| 0r <= r1; r1 <r2; 0r <= x; x < y|] \
  10.305 +Goal "[| 0r <= r1; r1 <r2; 0r <= x; x < y|] \
  10.306  \                  ==> r1 * x < r2 * y";
  10.307 -by (auto_tac (claset() addSDs [real_le_imp_less_or_eq] addIs
  10.308 -              [real_mult_less_mono,real_mult_order_trans,
  10.309 -               real_mult_order],simpset()));
  10.310 +by (auto_tac (claset() addSDs [real_le_imp_less_or_eq] 
  10.311 +	               addIs [real_mult_less_mono,real_mult_order_trans,
  10.312 +			      real_mult_order],
  10.313 +	      simpset()));
  10.314  by (dres_inst_tac [("R2.0","x")] real_less_trans 1);
  10.315  by (assume_tac 1);
  10.316  by (blast_tac (claset() addIs [real_mult_order]) 1);
  10.317  qed "real_mult_less_mono4";
  10.318  
  10.319 -Goal "!!(x::real). [| 0r < r1; r1 <= r2; 0r <= x; x <= y |] \
  10.320 -\                  ==> r1 * x <= r2 * y";
  10.321 -by (rtac real_less_or_eq_imp_le 1);
  10.322 -by (REPEAT(dtac real_le_imp_less_or_eq 1));
  10.323 -by (auto_tac (claset() addIs [real_mult_less_mono,
  10.324 -    real_mult_order_trans,real_mult_order],simpset()));
  10.325 -qed "real_mult_le_mono";
  10.326 -
  10.327 -Goal "!!(x::real). [| 0r < r1; r1 < r2; 0r <= x; x <= y |] \
  10.328 +Goal "[| 0r < r1; r1 <= r2; 0r <= x; x <= y |] \
  10.329  \                  ==> r1 * x <= r2 * y";
  10.330  by (rtac real_less_or_eq_imp_le 1);
  10.331  by (REPEAT(dtac real_le_imp_less_or_eq 1));
  10.332  by (auto_tac (claset() addIs [real_mult_less_mono,
  10.333 -    real_mult_order_trans,real_mult_order],simpset()));
  10.334 +			      real_mult_order_trans,real_mult_order],
  10.335 +	      simpset()));
  10.336 +qed "real_mult_le_mono";
  10.337 +
  10.338 +Goal "[| 0r < r1; r1 < r2; 0r <= x; x <= y |] \
  10.339 +\                  ==> r1 * x <= r2 * y";
  10.340 +by (rtac real_less_or_eq_imp_le 1);
  10.341 +by (REPEAT(dtac real_le_imp_less_or_eq 1));
  10.342 +by (auto_tac (claset() addIs [real_mult_less_mono, real_mult_order_trans,
  10.343 +			      real_mult_order],
  10.344 +	      simpset()));
  10.345  qed "real_mult_le_mono2";
  10.346  
  10.347 -Goal "!!(x::real). [| 0r <= r1; r1 < r2; 0r <= x; x <= y |] \
  10.348 +Goal "[| 0r <= r1; r1 < r2; 0r <= x; x <= y |] \
  10.349  \                  ==> r1 * x <= r2 * y";
  10.350  by (dtac real_le_imp_less_or_eq 1);
  10.351  by (auto_tac (claset() addIs [real_mult_le_mono2],simpset()));
  10.352  by (dtac real_le_trans 1 THEN assume_tac 1);
  10.353 -by (auto_tac (claset() addIs [real_less_le_mult_order],simpset()));
  10.354 +by (auto_tac (claset() addIs [real_less_le_mult_order], simpset()));
  10.355  qed "real_mult_le_mono3";
  10.356  
  10.357 -Goal "!!(x::real). [| 0r <= r1; r1 <= r2; 0r <= x; x <= y |] \
  10.358 +Goal "[| 0r <= r1; r1 <= r2; 0r <= x; x <= y |] \
  10.359  \                  ==> r1 * x <= r2 * y";
  10.360  by (dres_inst_tac [("x","r1")] real_le_imp_less_or_eq 1);
  10.361 -by (auto_tac (claset() addIs [real_mult_le_mono3,
  10.362 -    real_mult_le_le_mono1],simpset()));
  10.363 +by (auto_tac (claset() addIs [real_mult_le_mono3, real_mult_le_le_mono1],
  10.364 +	      simpset()));
  10.365  qed "real_mult_le_mono4";
  10.366  
  10.367 -Goal "!!x. 1r <= x ==> 0r < x";
  10.368 +Goal "1r <= x ==> 0r < x";
  10.369  by (rtac ccontr 1 THEN dtac real_leI 1);
  10.370  by (dtac real_le_trans 1 THEN assume_tac 1);
  10.371 -by (auto_tac (claset() addDs [real_zero_less_one 
  10.372 -    RSN (2,real_le_less_trans)],simpset() addsimps 
  10.373 -    [real_less_not_refl]));
  10.374 +by (auto_tac (claset() addDs [real_zero_less_one RSN (2,real_le_less_trans)],
  10.375 +	      simpset() addsimps [real_less_not_refl]));
  10.376  qed "real_gt_zero";
  10.377  
  10.378 -Goal "!!r. [| 1r < r; 1r <= x |]  ==> x <= r * x";
  10.379 +Goal "[| 1r < r; 1r <= x |]  ==> x <= r * x";
  10.380  by (dtac (real_gt_zero RS real_less_imp_le) 1);
  10.381  by (auto_tac (claset() addSDs [real_mult_le_less_mono1],
  10.382      simpset()));
  10.383  qed "real_mult_self_le";
  10.384  
  10.385 -Goal "!!r. [| 1r <= r; 1r <= x |]  ==> x <= r * x";
  10.386 +Goal "[| 1r <= r; 1r <= x |]  ==> x <= r * x";
  10.387  by (dtac real_le_imp_less_or_eq 1);
  10.388  by (auto_tac (claset() addIs [real_mult_self_le],
  10.389 -    simpset() addsimps [real_le_refl]));
  10.390 +	      simpset() addsimps [real_le_refl]));
  10.391  qed "real_mult_self_le2";
  10.392  
  10.393 -Goal "!!(x::real). x < y ==> x < (x + y)*rinv(1r + 1r)";
  10.394 +Goal "x < y ==> x < (x + y)*rinv(1r + 1r)";
  10.395  by (dres_inst_tac [("C","x")] real_add_less_mono2 1);
  10.396  by (dtac (real_add_self RS subst) 1);
  10.397  by (dtac (real_zero_less_two RS real_rinv_gt_zero RS 
  10.398 @@ -544,7 +545,7 @@
  10.399  by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc]) 1);
  10.400  qed "real_less_half_sum";
  10.401  
  10.402 -Goal "!!(x::real). x < y ==> (x + y)*rinv(1r + 1r) < y";
  10.403 +Goal "x < y ==> (x + y)*rinv(1r + 1r) < y";
  10.404  by (dtac real_add_less_mono1 1);
  10.405  by (dtac (real_add_self RS subst) 1);
  10.406  by (dtac (real_zero_less_two RS real_rinv_gt_zero RS 
  10.407 @@ -552,20 +553,21 @@
  10.408  by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc]) 1);
  10.409  qed "real_gt_half_sum";
  10.410  
  10.411 -Goal "!!(x::real). x < y ==> EX r. x < r & r < y";
  10.412 +Goal "x < y ==> EX r::real. x < r & r < y";
  10.413  by (blast_tac (claset() addSIs [real_less_half_sum,
  10.414 -    real_gt_half_sum]) 1);
  10.415 +				real_gt_half_sum]) 1);
  10.416  qed "real_dense";
  10.417  
  10.418  Goal "(EX n. rinv(real_of_posnat n) < r) = (EX n. 1r < r * real_of_posnat n)";
  10.419  by (Step_tac 1);
  10.420  by (dres_inst_tac [("n1","n")] (real_of_posnat_less_zero 
  10.421 -                       RS real_mult_less_mono1) 1);
  10.422 +				RS real_mult_less_mono1) 1);
  10.423  by (dres_inst_tac [("n2","n")] (real_of_posnat_less_zero RS 
  10.424 -        real_rinv_gt_zero RS real_mult_less_mono1) 2);
  10.425 +				real_rinv_gt_zero RS real_mult_less_mono1) 2);
  10.426  by (auto_tac (claset(),
  10.427  	      simpset() addsimps [(real_of_posnat_less_zero RS 
  10.428 -    real_not_refl2 RS not_sym),real_mult_assoc]));
  10.429 +				   real_not_refl2 RS not_sym),
  10.430 +				  real_mult_assoc]));
  10.431  qed "real_of_posnat_rinv_Ex_iff";
  10.432  
  10.433  Goal "(rinv(real_of_posnat n) < r) = (1r < r * real_of_posnat n)";
  10.434 @@ -573,8 +575,8 @@
  10.435  by (dres_inst_tac [("n1","n")] (real_of_posnat_less_zero 
  10.436                         RS real_mult_less_mono1) 1);
  10.437  by (dres_inst_tac [("n2","n")] (real_of_posnat_less_zero RS 
  10.438 -        real_rinv_gt_zero RS real_mult_less_mono1) 2);
  10.439 -by (auto_tac (claset(),simpset() addsimps [real_mult_assoc]));
  10.440 +				real_rinv_gt_zero RS real_mult_less_mono1) 2);
  10.441 +by (auto_tac (claset(), simpset() addsimps [real_mult_assoc]));
  10.442  qed "real_of_posnat_rinv_iff";
  10.443  
  10.444  Goal "(rinv(real_of_posnat n) <= r) = (1r <= r * real_of_posnat n)";
  10.445 @@ -584,7 +586,7 @@
  10.446  by (dres_inst_tac [("n3","n")] (real_of_posnat_less_zero RS 
  10.447          real_rinv_gt_zero RS real_less_imp_le RS 
  10.448          real_mult_le_le_mono1) 2);
  10.449 -by (auto_tac (claset(),simpset() addsimps real_mult_ac));
  10.450 +by (auto_tac (claset(), simpset() addsimps real_mult_ac));
  10.451  qed "real_of_posnat_rinv_le_iff";
  10.452  
  10.453  Goalw [real_of_posnat_def] "(real_of_posnat n < real_of_posnat m) = (n < m)";
  10.454 @@ -616,14 +618,14 @@
  10.455      real_of_posnat_less_zero,real_not_refl2 RS not_sym]));
  10.456  qed "real_of_posnat_rinv_eq_iff";
  10.457  
  10.458 -Goal "!!x. [| 0r < r; r < x |] ==> rinv x < rinv r";
  10.459 +Goal "[| 0r < r; r < x |] ==> rinv x < rinv r";
  10.460  by (forward_tac [real_less_trans] 1 THEN assume_tac 1);
  10.461  by (forward_tac [real_rinv_gt_zero] 1);
  10.462  by (forw_inst_tac [("x","x")] real_rinv_gt_zero 1);
  10.463  by (forw_inst_tac [("x","r"),("z","rinv r")] real_mult_less_mono1 1);
  10.464  by (assume_tac 1);
  10.465  by (asm_full_simp_tac (simpset() addsimps [real_not_refl2 RS 
  10.466 -         not_sym RS real_mult_inv_right]) 1);
  10.467 +					   not_sym RS real_mult_inv_right]) 1);
  10.468  by (forward_tac [real_rinv_gt_zero] 1);
  10.469  by (forw_inst_tac [("x","1r"),("z","rinv x")] real_mult_less_mono2 1);
  10.470  by (assume_tac 1);
  10.471 @@ -631,14 +633,14 @@
  10.472           not_sym RS real_mult_inv_left,real_mult_assoc RS sym]) 1);
  10.473  qed "real_rinv_less_swap";
  10.474  
  10.475 -Goal "!!x. [| 0r < r; 0r < x|] ==> (r < x) = (rinv x < rinv r)";
  10.476 +Goal "[| 0r < r; 0r < x|] ==> (r < x) = (rinv x < rinv r)";
  10.477  by (auto_tac (claset() addIs [real_rinv_less_swap],simpset()));
  10.478  by (res_inst_tac [("t","r")] (real_rinv_rinv RS subst) 1);
  10.479  by (etac (real_not_refl2 RS not_sym) 1);
  10.480  by (res_inst_tac [("t","x")] (real_rinv_rinv RS subst) 1);
  10.481  by (etac (real_not_refl2 RS not_sym) 1);
  10.482  by (auto_tac (claset() addIs [real_rinv_less_swap],
  10.483 -    simpset() addsimps [real_rinv_gt_zero]));
  10.484 +	      simpset() addsimps [real_rinv_gt_zero]));
  10.485  qed "real_rinv_less_iff";
  10.486  
  10.487  Goal "r < r + rinv(real_of_posnat n)";
  10.488 @@ -653,87 +655,85 @@
  10.489  qed "real_add_rinv_real_of_posnat_le";
  10.490  Addsimps [real_add_rinv_real_of_posnat_le];
  10.491  
  10.492 -Goal "r + -rinv(real_of_posnat n) < r";
  10.493 +Goal "r + (-rinv(real_of_posnat n)) < r";
  10.494  by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1);
  10.495  by (full_simp_tac (simpset() addsimps [real_add_assoc RS sym,
  10.496 -    real_minus_zero_less_iff2]) 1);
  10.497 +				       real_minus_zero_less_iff2]) 1);
  10.498  qed "real_add_minus_rinv_real_of_posnat_less";
  10.499  Addsimps [real_add_minus_rinv_real_of_posnat_less];
  10.500  
  10.501 -Goal "r + -rinv(real_of_posnat n) <= r";
  10.502 +Goal "r + (-rinv(real_of_posnat n)) <= r";
  10.503  by (rtac real_less_imp_le 1);
  10.504  by (Simp_tac 1);
  10.505  qed "real_add_minus_rinv_real_of_posnat_le";
  10.506  Addsimps [real_add_minus_rinv_real_of_posnat_le];
  10.507  
  10.508 -Goal "!!r. 0r < r ==> r*(1r + -rinv(real_of_posnat n)) < r";
  10.509 +Goal "0r < r ==> r*(1r + (-rinv(real_of_posnat n))) < r";
  10.510  by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1);
  10.511  by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1);
  10.512 -by (auto_tac (claset() addIs [real_mult_order],simpset() 
  10.513 -    addsimps [real_add_assoc RS sym,real_minus_mult_eq2 RS sym,
  10.514 -    real_minus_zero_less_iff2]));
  10.515 +by (auto_tac (claset() addIs [real_mult_order],
  10.516 +	      simpset() addsimps [real_add_assoc RS sym,
  10.517 +				  real_minus_mult_eq2 RS sym,
  10.518 +				  real_minus_zero_less_iff2]));
  10.519  qed "real_mult_less_self";
  10.520  
  10.521 -Goal "0r <= 1r + -rinv(real_of_posnat n)";
  10.522 +Goal "0r <= 1r + (-rinv(real_of_posnat n))";
  10.523  by (res_inst_tac [("C","rinv(real_of_posnat n)")] real_le_add_right_cancel 1);
  10.524  by (simp_tac (simpset() addsimps [real_add_assoc,
  10.525 -    real_of_posnat_rinv_le_iff]) 1);
  10.526 +				  real_of_posnat_rinv_le_iff]) 1);
  10.527  qed "real_add_one_minus_rinv_ge_zero";
  10.528  
  10.529 -Goal "!!r. 0r < r ==> 0r <= r*(1r + -rinv(real_of_posnat n))";
  10.530 -by (dtac (real_add_one_minus_rinv_ge_zero RS 
  10.531 -          real_mult_le_less_mono1) 1);
  10.532 -by (Auto_tac);
  10.533 +Goal "0r < r ==> 0r <= r*(1r + (-rinv(real_of_posnat n)))";
  10.534 +by (dtac (real_add_one_minus_rinv_ge_zero RS real_mult_le_less_mono1) 1);
  10.535 +by Auto_tac;
  10.536  qed "real_mult_add_one_minus_ge_zero";
  10.537  
  10.538 -Goal "!!x. x*y = 0r ==> x = 0r | y = 0r";
  10.539 -by (auto_tac (claset() addIs [ccontr] addDs 
  10.540 -    [real_mult_not_zero],simpset()));
  10.541 +Goal "x*y = 0r ==> x = 0r | y = 0r";
  10.542 +by (auto_tac (claset() addIs [ccontr] addDs [real_mult_not_zero],
  10.543 +	      simpset()));
  10.544  qed "real_mult_zero_disj";
  10.545   
  10.546  Goal "x + x*y = x*(1r + y)";
  10.547  by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1);
  10.548  qed "real_add_mult_distrib_one";
  10.549  
  10.550 -Goal "!!x. [| x ~= 1r; y * x = y |] ==> y = 0r";
  10.551 +Goal "[| x ~= 1r; y * x = y |] ==> y = 0r";
  10.552  by (dtac (sym RS (real_eq_minus_iff RS iffD1)) 1);
  10.553  by (dtac sym 1);
  10.554  by (asm_full_simp_tac (simpset() addsimps [real_minus_mult_eq2,
  10.555      real_add_mult_distrib_one]) 1);
  10.556  by (dtac real_mult_zero_disj 1);
  10.557 -by (auto_tac (claset(),simpset() 
  10.558 -   addsimps [real_eq_minus_iff2 RS sym]));
  10.559 +by (auto_tac (claset(),
  10.560 +	      simpset() addsimps [real_eq_minus_iff2 RS sym]));
  10.561  qed "real_mult_eq_self_zero";
  10.562  Addsimps [real_mult_eq_self_zero];
  10.563  
  10.564 -Goal "!!x. [| x ~= 1r; y = y * x |] ==> y = 0r";
  10.565 +Goal "[| x ~= 1r; y = y * x |] ==> y = 0r";
  10.566  by (dtac sym 1);
  10.567  by (Asm_full_simp_tac 1);
  10.568  qed "real_mult_eq_self_zero2";
  10.569  Addsimps [real_mult_eq_self_zero2];
  10.570  
  10.571 -Goal "!!x. [| 0r <= x*y; 0r < x |] ==> 0r <= y";
  10.572 +Goal "[| 0r <= x*y; 0r < x |] ==> 0r <= y";
  10.573  by (forward_tac [real_rinv_gt_zero] 1);
  10.574  by (dres_inst_tac [("x","rinv x")] real_less_le_mult_order 1);
  10.575  by (dtac (real_not_refl2 RS not_sym RS real_mult_inv_left) 2);
  10.576 -by (auto_tac (claset(),simpset() addsimps 
  10.577 -    [real_mult_assoc RS sym]));
  10.578 +by (auto_tac (claset(),
  10.579 +	      simpset() addsimps [real_mult_assoc RS sym]));
  10.580  qed "real_mult_ge_zero_cancel";
  10.581  
  10.582 -Goal "!!x. [|x ~= 0r; y ~= 0r |] ==> \
  10.583 -\          rinv(x) + rinv(y) = (x + y)*rinv(x*y)";
  10.584 +Goal "[|x ~= 0r; y ~= 0r |] ==> rinv(x) + rinv(y) = (x + y)*rinv(x*y)";
  10.585  by (asm_full_simp_tac (simpset() addsimps 
  10.586 -    [real_rinv_distrib,real_add_mult_distrib,
  10.587 -     real_mult_assoc RS sym]) 1);
  10.588 +		       [real_rinv_distrib,real_add_mult_distrib,
  10.589 +			real_mult_assoc RS sym]) 1);
  10.590  by (rtac (real_mult_assoc RS ssubst) 1);
  10.591  by (rtac (real_mult_left_commute RS subst) 1);
  10.592 -by (asm_full_simp_tac (simpset() addsimps 
  10.593 -    [real_add_commute]) 1);
  10.594 +by (asm_full_simp_tac (simpset() addsimps [real_add_commute]) 1);
  10.595  qed "real_rinv_add";
  10.596  
  10.597 -(*---------------------------------------------------------------------------------
  10.598 +(*----------------------------------------------------------------------------
  10.599       Another embedding of the naturals in the reals (see real_of_posnat)
  10.600 - ---------------------------------------------------------------------------------*)
  10.601 + ----------------------------------------------------------------------------*)
  10.602  Goalw [real_of_nat_def] "real_of_nat 0 = 0r";
  10.603  by (full_simp_tac (simpset() addsimps [real_of_posnat_one]) 1);
  10.604  qed "real_of_nat_zero";
  10.605 @@ -754,7 +754,7 @@
  10.606  qed "real_of_nat_Suc";
  10.607      
  10.608  Goalw [real_of_nat_def] "(n < m) = (real_of_nat n < real_of_nat m)";
  10.609 -by (Auto_tac);
  10.610 +by Auto_tac;
  10.611  qed "real_of_nat_less_iff";
  10.612  
  10.613  Addsimps [real_of_nat_less_iff RS sym];
  10.614 @@ -762,22 +762,22 @@
  10.615  Goal "inj real_of_nat";
  10.616  by (rtac injI 1);
  10.617  by (auto_tac (claset() addSIs [inj_real_of_posnat RS injD],
  10.618 -    simpset() addsimps [real_of_nat_def,real_add_right_cancel]));
  10.619 +	      simpset() addsimps [real_of_nat_def,real_add_right_cancel]));
  10.620  qed "inj_real_of_nat";
  10.621  
  10.622  Goalw [real_of_nat_def] "0r <= real_of_nat n";
  10.623  by (res_inst_tac [("C","1r")] real_le_add_right_cancel 1);
  10.624 -by (asm_full_simp_tac (simpset() addsimps 
  10.625 -        [real_add_assoc]) 1);
  10.626 +by (asm_full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
  10.627  qed "real_of_nat_ge_zero";
  10.628  Addsimps [real_of_nat_ge_zero];
  10.629  
  10.630  Goal "real_of_nat n1 * real_of_nat n2 = real_of_nat (n1 * n2)";
  10.631  by (induct_tac "n1" 1);
  10.632  by (dtac sym 2);
  10.633 -by (auto_tac (claset(),simpset() addsimps [real_of_nat_zero,
  10.634 -    real_of_nat_add RS sym,real_of_nat_Suc,real_add_mult_distrib,
  10.635 -    real_add_commute]));
  10.636 +by (auto_tac (claset(),
  10.637 +	      simpset() addsimps [real_of_nat_zero,
  10.638 +				  real_of_nat_add RS sym,real_of_nat_Suc,
  10.639 +				  real_add_mult_distrib, real_add_commute]));
  10.640  qed "real_of_nat_mult";
  10.641  
  10.642  Goal "(real_of_nat n = real_of_nat m) = (n = m)";
  10.643 @@ -788,21 +788,20 @@
  10.644  (*------- lemmas -------*)
  10.645  goal NatDef.thy "!!m. [| m < Suc n; n <= m |] ==> m = n";
  10.646  by (auto_tac (claset() addSDs [le_imp_less_or_eq] addIs [less_asym],
  10.647 -    simpset() addsimps [less_Suc_eq]));
  10.648 +	      simpset() addsimps [less_Suc_eq]));
  10.649  qed "lemma_nat_not_dense";
  10.650  
  10.651  goal NatDef.thy "!!m. [| m <= Suc n; n < m |] ==> m = Suc n";
  10.652  by (auto_tac (claset() addSDs [le_imp_less_or_eq] addIs [less_asym],
  10.653 -    simpset() addsimps [le_Suc_eq]));
  10.654 +	      simpset() addsimps [le_Suc_eq]));
  10.655  qed "lemma_nat_not_dense2";
  10.656  
  10.657  goal NatDef.thy "!!m. m < Suc n ==> ~ Suc n <= m";
  10.658 -by (blast_tac (claset() addDs 
  10.659 -     [less_le_trans] addIs [less_asym]) 1);
  10.660 +by (blast_tac (claset() addDs [less_le_trans] addIs [less_asym]) 1);
  10.661  qed "lemma_not_leI";
  10.662  
  10.663  goalw NatDef.thy [le_def] "!!m. ~ Suc n <= m ==> ~ Suc (Suc n) <= m";
  10.664 -by (Auto_tac);
  10.665 +by Auto_tac;
  10.666  qed "lemma_not_leI2";
  10.667  
  10.668  (*------- lemmas -------*)
  10.669 @@ -815,14 +814,15 @@
  10.670  (* Goalw  [real_of_nat_def] 
  10.671     "real_of_nat (n1 - n2) = real_of_nat n1 + -real_of_nat n2";*)
  10.672  
  10.673 -Goal "n2 < n1 --> real_of_nat (n1 - n2) = real_of_nat n1 + -real_of_nat n2";
  10.674 +Goal "n2 < n1 --> real_of_nat (n1 - n2) = real_of_nat n1 + (-real_of_nat n2)";
  10.675  by (induct_tac "n1" 1);
  10.676  by (Step_tac 1 THEN dtac leI 1 THEN dtac sym 2);
  10.677  by (dtac lemma_nat_not_dense 1);
  10.678 -by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc,
  10.679 -              real_of_nat_zero] @ real_add_ac));
  10.680 +by (auto_tac (claset(),
  10.681 +	      simpset() addsimps [real_of_nat_Suc, real_of_nat_zero] @ 
  10.682 +	                         real_add_ac));
  10.683  by (asm_full_simp_tac (simpset() addsimps [real_of_nat_one RS sym,
  10.684 -             real_of_nat_add,Suc_diff_n]) 1);
  10.685 +					   real_of_nat_add,Suc_diff_n]) 1);
  10.686  qed "real_of_nat_minus";
  10.687  
  10.688  
    11.1 --- a/src/HOL/Real/RealAbs.ML	Wed Jul 28 22:01:58 1999 +0200
    11.2 +++ b/src/HOL/Real/RealAbs.ML	Thu Jul 29 12:44:57 1999 +0200
    11.3 @@ -31,8 +31,8 @@
    11.4  by (simp_tac (simpset() addsimps [(prem RS real_less_imp_le),rabs_eqI1]) 1);
    11.5  qed "rabs_eqI2";
    11.6  
    11.7 -val [prem] = goalw thy [rabs_def,real_le_def] "x<0r ==> rabs x = -x";
    11.8 -by (simp_tac (simpset() addsimps [prem,if_not_P]) 1);
    11.9 +Goalw [rabs_def,real_le_def] "x<0r ==> rabs x = -x";
   11.10 +by (Asm_simp_tac 1);
   11.11  qed "rabs_minus_eqI2";
   11.12  
   11.13  Goal "x<=0r ==> rabs x = -x";
   11.14 @@ -71,39 +71,38 @@
   11.15  
   11.16  (* case splits nightmare *)
   11.17  Goalw [rabs_def] "rabs(x*y) = (rabs x)*(rabs y)";
   11.18 -by (auto_tac (claset(),simpset() addsimps [real_minus_mult_eq1,
   11.19 -   real_minus_mult_commute,real_minus_mult_eq2]));
   11.20 +by (auto_tac (claset(),
   11.21 +	      simpset() addsimps [real_minus_mult_eq1, real_minus_mult_commute,
   11.22 +				  real_minus_mult_eq2]));
   11.23  by (blast_tac (claset() addDs [real_le_mult_order]) 1);
   11.24  by (auto_tac (claset() addSDs [not_real_leE],simpset()));
   11.25  by (EVERY1[dtac real_mult_le_zero, assume_tac, dtac real_le_anti_sym]);
   11.26  by (EVERY[dtac real_mult_le_zero 3, assume_tac 3, dtac real_le_anti_sym 3]);
   11.27  by (dtac real_mult_less_zero1 5 THEN assume_tac 5);
   11.28  by (auto_tac (claset() addDs [real_less_asym,sym],
   11.29 -    simpset() addsimps [real_minus_mult_eq2 RS sym] @real_mult_ac));
   11.30 +	      simpset() addsimps [real_minus_mult_eq2 RS sym] @real_mult_ac));
   11.31  qed "rabs_mult";
   11.32  
   11.33  Goalw [rabs_def] "x~= 0r ==> rabs(rinv(x)) = rinv(rabs(x))";
   11.34 -by (auto_tac (claset(),simpset() addsimps [real_minus_rinv] 
   11.35 -   ));
   11.36 +by (auto_tac (claset(), simpset() addsimps [real_minus_rinv]));
   11.37  by (ALLGOALS(dtac not_real_leE));
   11.38  by (etac real_less_asym 1);
   11.39 -by (blast_tac (claset() addDs [real_le_imp_less_or_eq,
   11.40 -          real_rinv_gt_zero]) 1);
   11.41 +by (blast_tac (claset() addDs [real_le_imp_less_or_eq, real_rinv_gt_zero]) 1);
   11.42  by (dtac (rinv_not_zero RS not_sym) 1);
   11.43  by (rtac (real_rinv_less_zero RSN (2,real_less_asym)) 1);
   11.44  by (assume_tac 2);
   11.45  by (blast_tac (claset() addSDs [real_le_imp_less_or_eq]) 1);
   11.46  qed "rabs_rinv";
   11.47  
   11.48 -val [prem] = goal thy "y ~= 0r ==> rabs(x*rinv(y)) = rabs(x)*rinv(rabs(y))";
   11.49 +Goal "y ~= 0r ==> rabs(x*rinv(y)) = rabs(x)*rinv(rabs(y))";
   11.50  by (res_inst_tac [("c1","rabs y")] (real_mult_left_cancel RS subst) 1);
   11.51 -by (simp_tac (simpset() addsimps [(rabs_not_zero_iff RS sym), prem]) 1);
   11.52 -by (simp_tac (simpset() addsimps [(rabs_mult RS sym) ,real_mult_inv_right, 
   11.53 -    prem,rabs_not_zero_iff RS sym] @ real_mult_ac) 1);
   11.54 +by (asm_simp_tac (simpset() addsimps [rabs_not_zero_iff RS sym]) 1);
   11.55 +by (asm_simp_tac (simpset() addsimps [rabs_mult RS sym, real_mult_inv_right, 
   11.56 +				 rabs_not_zero_iff RS sym] @ real_mult_ac) 1);
   11.57  qed "rabs_mult_rinv";
   11.58  
   11.59  Goal "rabs(x+y) <= rabs x + rabs y";
   11.60 -by (EVERY1 [res_inst_tac [("Q1","0r<=x+y")] (expand_if RS ssubst), rtac conjI]);
   11.61 +by (case_tac "0r<=x+y" 1);
   11.62  by (asm_simp_tac
   11.63      (simpset() addsimps [rabs_eqI1,real_add_le_mono,rabs_ge_self]) 1);
   11.64  by (asm_simp_tac 
   11.65 @@ -113,38 +112,38 @@
   11.66  
   11.67  Goal "rabs(w + x + y + z) <= rabs(w) + rabs(x) + rabs(y) + rabs(z)";
   11.68  by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
   11.69 -by (blast_tac (claset() addSIs [(rabs_triangle_ineq RS real_le_trans),
   11.70 +by (blast_tac (claset() addSIs [rabs_triangle_ineq RS real_le_trans,
   11.71  				real_add_left_le_mono1]) 1);
   11.72  qed "rabs_triangle_ineq_four";
   11.73  
   11.74  Goalw [rabs_def] "rabs(-x)=rabs(x)";
   11.75 -by (auto_tac (claset() addSDs [not_real_leE,real_less_asym] addIs [real_le_anti_sym],
   11.76 -   simpset() addsimps [real_ge_zero_iff]));
   11.77 +by (auto_tac (claset() addSDs [not_real_leE,real_less_asym] 
   11.78 +	               addIs [real_le_anti_sym],
   11.79 +		       simpset() addsimps [real_ge_zero_iff]));
   11.80  qed "rabs_minus_cancel";
   11.81  
   11.82 -Goal "rabs(x + -y) = rabs (y + -x)";
   11.83 +Goal "rabs(x + (-y)) = rabs (y + (-x))";
   11.84  by (rtac (rabs_minus_cancel RS subst) 1);
   11.85 -by (simp_tac (simpset() addsimps 
   11.86 -    [real_add_commute]) 1);
   11.87 +by (simp_tac (simpset() addsimps [real_add_commute]) 1);
   11.88  qed "rabs_minus_add_cancel";
   11.89  
   11.90 -Goal "rabs(x + -y) <= rabs x + rabs y";
   11.91 +Goal "rabs(x + (-y)) <= rabs x + rabs y";
   11.92  by (res_inst_tac [("x1","y")] (rabs_minus_cancel RS subst) 1);
   11.93  by (rtac rabs_triangle_ineq 1);
   11.94  qed "rabs_triangle_minus_ineq";
   11.95  
   11.96 -Goal "rabs (x + y + (-l + -m)) <= rabs(x + -l) + rabs(y + -m)";
   11.97 +Goal "rabs (x + y + ((-l) + (-m))) <= rabs(x + (-l)) + rabs(y + (-m))";
   11.98  by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
   11.99  by (res_inst_tac [("x1","y")] (real_add_left_commute RS ssubst) 1);
  11.100  by (rtac (real_add_assoc RS subst) 1);
  11.101  by (rtac rabs_triangle_ineq 1);
  11.102  qed "rabs_sum_triangle_ineq";
  11.103  
  11.104 -Goal "rabs(x) <= rabs(x + -y) + rabs(y)";
  11.105 -by (res_inst_tac [("j","rabs(x + -y + y)")] real_le_trans 1);
  11.106 +Goal "rabs(x) <= rabs(x + (-y)) + rabs(y)";
  11.107 +by (res_inst_tac [("j","rabs(x + (-y) + y)")] real_le_trans 1);
  11.108  by (simp_tac (simpset() addsimps [real_add_assoc]) 1);
  11.109  by (simp_tac (simpset() addsimps [real_add_assoc RS sym,
  11.110 -              rabs_triangle_ineq]) 1);
  11.111 +				  rabs_triangle_ineq]) 1);
  11.112  qed "rabs_triangle_ineq_minus_cancel";
  11.113  
  11.114  Goal "[| rabs x < r; rabs y < s |] ==> rabs(x+y) < r+s";
  11.115 @@ -153,7 +152,7 @@
  11.116  by (REPEAT (ares_tac [real_add_less_mono] 1));
  11.117  qed "rabs_add_less";
  11.118  
  11.119 -Goal "[| rabs x < r; rabs y < s |] ==> rabs(x+ -y) < r+s";
  11.120 +Goal "[| rabs x < r; rabs y < s |] ==> rabs(x+ (-y)) < r+s";
  11.121  by (rotate_tac 1 1);
  11.122  by (dtac (rabs_minus_cancel RS ssubst) 1);
  11.123  by (asm_simp_tac (simpset() addsimps [rabs_add_less]) 1);
  11.124 @@ -169,7 +168,7 @@
  11.125  	                addIs  [real_less_trans]) 1);
  11.126  qed "real_mult_less_trans";
  11.127  
  11.128 -Goal "!!(x::real) y.[| 0r<=y; x<r; y*r<t*s; 0r<t*s|] ==> y*x<t*s";
  11.129 +Goal "[| 0r<=y; x<r; y*r<t*s; 0r<t*s|] ==> y*x<t*s";
  11.130  by (dtac real_le_imp_less_or_eq 1);
  11.131  by (fast_tac (HOL_cs addEs [real_mult_0_less RS iffD2,
  11.132  			    real_mult_less_trans]) 1);
  11.133 @@ -196,11 +195,11 @@
  11.134  by (cut_inst_tac [("x1","y")] (rabs_ge_zero RS real_le_imp_less_or_eq) 1);
  11.135  by (EVERY1[etac disjE,rtac real_less_imp_le]);
  11.136  by (dres_inst_tac [("W","1r")]  real_less_sum_gt_zero 1);
  11.137 -by (forw_inst_tac [("y","rabs x + -1r")] real_mult_order 1);
  11.138 +by (forw_inst_tac [("y","rabs x + (-1r)")] real_mult_order 1);
  11.139  by (assume_tac 1);
  11.140  by (rtac real_sum_gt_zero_less 1);
  11.141  by (asm_full_simp_tac (simpset() addsimps [real_add_mult_distrib2,
  11.142 -    real_mult_commute, rabs_mult]) 1);
  11.143 +					   real_mult_commute, rabs_mult]) 1);
  11.144  by (dtac sym 1);
  11.145  by (asm_full_simp_tac (simpset() addsimps [rabs_mult]) 1);
  11.146  qed "rabs_mult_le";
  11.147 @@ -215,7 +214,7 @@
  11.148  
  11.149  Goalw [rabs_def] "rabs 1r = 1r";
  11.150  by (auto_tac (claset() addSDs [not_real_leE RS real_less_asym],
  11.151 -   simpset() addsimps [real_zero_less_one]));
  11.152 +	      simpset() addsimps [real_zero_less_one]));
  11.153  qed "rabs_one";
  11.154  
  11.155  Goal "[| 0r < x ; x < r |] ==> rabs x < r";
  11.156 @@ -225,7 +224,7 @@
  11.157  Goal "rabs x =x | rabs x = -x";
  11.158  by (cut_inst_tac [("R1.0","0r"),("R2.0","x")] real_linear 1);
  11.159  by (blast_tac (claset() addIs [rabs_eqI2,rabs_minus_eqI2,
  11.160 -                            rabs_zero,rabs_minus_zero]) 1);
  11.161 +			       rabs_zero,rabs_minus_zero]) 1);
  11.162  qed "rabs_disj";
  11.163  
  11.164  Goal "rabs x = y ==> x = y | -x = y";
  11.165 @@ -239,9 +238,8 @@
  11.166  by Safe_tac;
  11.167  by (rtac (real_less_swap_iff RS iffD2) 1);
  11.168  by (asm_simp_tac (simpset() addsimps [(rabs_ge_minus_self 
  11.169 -    RS real_le_less_trans)]) 1);
  11.170 -by (asm_simp_tac (simpset() addsimps [(rabs_ge_self 
  11.171 -    RS real_le_less_trans)]) 1);
  11.172 +				       RS real_le_less_trans)]) 1);
  11.173 +by (asm_simp_tac (simpset() addsimps [rabs_ge_self RS real_le_less_trans]) 1);
  11.174  by (EVERY1 [dtac (real_less_swap_iff RS iffD1), rotate_tac 1, 
  11.175              dtac (real_minus_minus RS subst), 
  11.176              cut_inst_tac [("x","x")] rabs_disj, dtac disjE ]);
  11.177 @@ -252,57 +250,57 @@
  11.178  by (auto_tac (claset(),simpset() addsimps [rabs_interval_iff]));
  11.179  by (dtac (real_less_swap_iff RS iffD1) 1);
  11.180  by (dtac (real_less_swap_iff RS iffD1) 2);
  11.181 -by (Auto_tac);
  11.182 +by Auto_tac;
  11.183  qed "rabs_interval_iff2";
  11.184  
  11.185 -Goal "!!x. rabs x <= r ==> -r<=x & x<=r";
  11.186 +Goal "rabs x <= r ==> -r<=x & x<=r";
  11.187  by (dtac real_le_imp_less_or_eq 1);
  11.188  by (auto_tac (claset() addSDs [real_less_imp_le],
  11.189 -    simpset() addsimps [rabs_interval_iff,rabs_ge_self]));
  11.190 +	      simpset() addsimps [rabs_interval_iff,rabs_ge_self]));
  11.191  by (auto_tac (claset(),simpset() addsimps [real_le_def]));
  11.192  by (dtac (real_less_swap_iff RS iffD1) 1);
  11.193 -by (auto_tac (claset() addSDs [rabs_ge_minus_self 
  11.194 -    RS real_le_less_trans],simpset() addsimps [real_less_not_refl]));
  11.195 +by (auto_tac (claset() addSDs [rabs_ge_minus_self RS real_le_less_trans],
  11.196 +	      simpset() addsimps [real_less_not_refl]));
  11.197  qed "rabs_leD";
  11.198  
  11.199 -Goal "!!x. [| -r<x; x<=r |] ==> rabs x <= r";
  11.200 +Goal "[| -r<x; x<=r |] ==> rabs x <= r";
  11.201  by (dtac real_le_imp_less_or_eq 1);
  11.202  by (Step_tac 1);
  11.203  by (blast_tac (claset() addIs 
  11.204 -    [rabs_interval_iff RS iffD2 RS real_less_imp_le]) 1);
  11.205 -by (auto_tac (claset() addSDs [rabs_eqI2],simpset() addsimps 
  11.206 -    [real_le_def,real_gt_zero_iff RS sym,real_less_not_refl]));
  11.207 +	       [rabs_interval_iff RS iffD2 RS real_less_imp_le]) 1);
  11.208 +by (auto_tac (claset() addSDs [rabs_eqI2],
  11.209 +	      simpset() addsimps 
  11.210 +	        [real_le_def,real_gt_zero_iff RS sym,real_less_not_refl]));
  11.211  qed "rabs_leI1";
  11.212  
  11.213 -Goal "!!x. [| -r<=x; x<=r |] ==> rabs x <= r";
  11.214 +Goal "[| -r<=x; x<=r |] ==> rabs x <= r";
  11.215  by (REPEAT(dtac real_le_imp_less_or_eq 1));
  11.216  by (Step_tac 1);
  11.217 -by (blast_tac (claset() addIs 
  11.218 -    [rabs_interval_iff RS iffD2 RS real_less_imp_le]) 1);
  11.219 -by (auto_tac (claset() addSDs [rabs_eqI2],simpset() addsimps 
  11.220 -    [real_le_def,real_gt_zero_iff RS sym,real_less_not_refl,
  11.221 -    rabs_minus_cancel]));
  11.222 +by (blast_tac (claset() 
  11.223 +	       addIs [rabs_interval_iff RS iffD2 RS real_less_imp_le]) 1);
  11.224 +by (auto_tac (claset() addSDs [rabs_eqI2],
  11.225 +	      simpset() addsimps 
  11.226 +	      [real_le_def,real_gt_zero_iff RS sym,real_less_not_refl,
  11.227 +	       rabs_minus_cancel]));
  11.228  by (cut_inst_tac [("x","r")] rabs_disj 1);
  11.229  by (rotate_tac 1 1);
  11.230 -by (auto_tac (claset(),simpset() addsimps [real_less_not_refl]));
  11.231 +by (auto_tac (claset(), simpset() addsimps [real_less_not_refl]));
  11.232  qed "rabs_leI";
  11.233  
  11.234  Goal "(rabs x <= r) = (-r<=x & x<=r)";
  11.235  by (blast_tac (claset() addSIs [rabs_leD,rabs_leI]) 1);
  11.236  qed "rabs_le_interval_iff";
  11.237  
  11.238 -Goal 
  11.239 -     "(rabs (x + -y) < r) = (y + -r < x & x < y + r)";
  11.240 -by (auto_tac (claset(),simpset() addsimps 
  11.241 -     [rabs_interval_iff]));
  11.242 +Goal "(rabs (x + (-y)) < r) = (y + (-r) < x & x < y + r)";
  11.243 +by (auto_tac (claset(), simpset() addsimps [rabs_interval_iff]));
  11.244  by (ALLGOALS(dtac real_less_sum_gt_zero));
  11.245  by (ALLGOALS(dtac real_less_sum_gt_zero));
  11.246  by (ALLGOALS(rtac real_sum_gt_zero_less));
  11.247 -by (auto_tac (claset(),simpset() addsimps 
  11.248 -    [real_minus_add_distrib] addsimps real_add_ac));
  11.249 +by (auto_tac (claset(),
  11.250 +	      simpset() addsimps [real_minus_add_distrib] @ real_add_ac));
  11.251  qed "rabs_add_minus_interval_iff";
  11.252  
  11.253 -Goal "!!k. 0r < k ==> 0r < k + rabs(x)";
  11.254 +Goal "0r < k ==> 0r < k + rabs(x)";
  11.255  by (res_inst_tac [("t","0r")] (real_add_zero_right RS subst) 1);
  11.256  by (etac (rabs_ge_zero RSN (2,real_add_less_le_mono)) 1);
  11.257  qed "rabs_add_pos_gt_zero";
    12.1 --- a/src/HOL/Real/RealDef.ML	Wed Jul 28 22:01:58 1999 +0200
    12.2 +++ b/src/HOL/Real/RealDef.ML	Thu Jul 29 12:44:57 1999 +0200
    12.3 @@ -206,20 +206,20 @@
    12.4  qed "real_add_zero_right";
    12.5  Addsimps [real_add_zero_right];
    12.6  
    12.7 -Goalw [real_zero_def] "z + -z = 0r";
    12.8 +Goalw [real_zero_def] "z + (-z) = 0r";
    12.9  by (res_inst_tac [("z","z")] eq_Abs_real 1);
   12.10  by (asm_full_simp_tac (simpset() addsimps [real_minus,
   12.11          real_add, preal_add_commute]) 1);
   12.12  qed "real_add_minus";
   12.13  Addsimps [real_add_minus];
   12.14  
   12.15 -Goal "-z + z = 0r";
   12.16 +Goal "(-z) + z = 0r";
   12.17  by (simp_tac (simpset() addsimps [real_add_commute]) 1);
   12.18  qed "real_add_minus_left";
   12.19  Addsimps [real_add_minus_left];
   12.20  
   12.21  
   12.22 -Goal "z + (- z + w) = (w::real)";
   12.23 +Goal "z + ((- z) + w) = (w::real)";
   12.24  by (simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
   12.25  qed "real_add_minus_cancel";
   12.26  
   12.27 @@ -259,7 +259,7 @@
   12.28  by (Fast_tac 1);
   12.29  qed "real_as_add_inverse_ex";
   12.30  
   12.31 -Goal "-(x + y) = -x + -(y::real)";
   12.32 +Goal "-(x + y) = (-x) + (- y :: real)";
   12.33  by (res_inst_tac [("z","x")] eq_Abs_real 1);
   12.34  by (res_inst_tac [("z","y")] eq_Abs_real 1);
   12.35  by (auto_tac (claset(),simpset() addsimps [real_minus,real_add]));
   12.36 @@ -269,7 +269,7 @@
   12.37  
   12.38  Goal "((x::real) + y = x + z) = (y = z)";
   12.39  by (Step_tac 1);
   12.40 -by (dres_inst_tac [("f","%t.-x + t")] arg_cong 1);
   12.41 +by (dres_inst_tac [("f","%t. (-x) + t")] arg_cong 1);
   12.42  by (asm_full_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
   12.43  qed "real_add_left_cancel";
   12.44  
   12.45 @@ -277,18 +277,18 @@
   12.46  by (simp_tac (simpset() addsimps [real_add_commute,real_add_left_cancel]) 1);
   12.47  qed "real_add_right_cancel";
   12.48  
   12.49 -Goal "((x::real) = y) = (0r = x + - y)";
   12.50 +Goal "((x::real) = y) = (0r = x + (- y))";
   12.51  by (Step_tac 1);
   12.52  by (res_inst_tac [("x1","-y")] 
   12.53        (real_add_right_cancel RS iffD1) 2);
   12.54 -by (Auto_tac);
   12.55 +by Auto_tac;
   12.56  qed "real_eq_minus_iff"; 
   12.57  
   12.58 -Goal "((x::real) = y) = (x + - y = 0r)";
   12.59 +Goal "((x::real) = y) = (x + (- y) = 0r)";
   12.60  by (Step_tac 1);
   12.61  by (res_inst_tac [("x1","-y")] 
   12.62        (real_add_right_cancel RS iffD1) 2);
   12.63 -by (Auto_tac);
   12.64 +by Auto_tac;
   12.65  qed "real_eq_minus_iff2"; 
   12.66  
   12.67  Goal "0r - x = -x";
   12.68 @@ -391,7 +391,7 @@
   12.69  
   12.70  Addsimps [real_mult_0_right, real_mult_0];
   12.71  
   12.72 -Goal "-(x * y) = -x * (y::real)";
   12.73 +Goal "-(x * y) = (-x) * (y::real)";
   12.74  by (res_inst_tac [("z","x")] eq_Abs_real 1);
   12.75  by (res_inst_tac [("z","y")] eq_Abs_real 1);
   12.76  by (auto_tac (claset(),
   12.77 @@ -399,7 +399,7 @@
   12.78      @ preal_mult_ac @ preal_add_ac));
   12.79  qed "real_minus_mult_eq1";
   12.80  
   12.81 -Goal "-(x * y) = x * -(y::real)";
   12.82 +Goal "-(x * y) = x * (- y :: real)";
   12.83  by (res_inst_tac [("z","x")] eq_Abs_real 1);
   12.84  by (res_inst_tac [("z","y")] eq_Abs_real 1);
   12.85  by (auto_tac (claset(),
   12.86 @@ -407,34 +407,34 @@
   12.87      @ preal_mult_ac @ preal_add_ac));
   12.88  qed "real_minus_mult_eq2";
   12.89  
   12.90 -Goal "- 1r * z = -z";
   12.91 +Goal "(- 1r) * z = -z";
   12.92  by (simp_tac (simpset() addsimps [real_minus_mult_eq1 RS sym]) 1);
   12.93  qed "real_mult_minus_1";
   12.94  
   12.95  Addsimps [real_mult_minus_1];
   12.96  
   12.97 -Goal "z * - 1r = -z";
   12.98 +Goal "z * (- 1r) = -z";
   12.99  by (stac real_mult_commute 1);
  12.100  by (Simp_tac 1);
  12.101  qed "real_mult_minus_1_right";
  12.102  
  12.103  Addsimps [real_mult_minus_1_right];
  12.104  
  12.105 -Goal "-x * -y = x * (y::real)";
  12.106 +Goal "(-x) * (-y) = x * (y::real)";
  12.107  by (full_simp_tac (simpset() addsimps [real_minus_mult_eq2 RS sym,
  12.108 -    real_minus_mult_eq1 RS sym]) 1);
  12.109 +				       real_minus_mult_eq1 RS sym]) 1);
  12.110  qed "real_minus_mult_cancel";
  12.111  
  12.112  Addsimps [real_minus_mult_cancel];
  12.113  
  12.114 -Goal "-x * y = x * -(y::real)";
  12.115 +Goal "(-x) * y = x * (- y :: real)";
  12.116  by (full_simp_tac (simpset() addsimps [real_minus_mult_eq2 RS sym,
  12.117 -    real_minus_mult_eq1 RS sym]) 1);
  12.118 +				       real_minus_mult_eq1 RS sym]) 1);
  12.119  qed "real_minus_mult_commute";
  12.120  
  12.121  (*-----------------------------------------------------------------------------
  12.122  
  12.123 - -----------------------------------------------------------------------------*)
  12.124 + ----------------------------------------------------------------------------*)
  12.125  
  12.126  (** Lemmas **)
  12.127  
  12.128 @@ -493,17 +493,17 @@
  12.129  
  12.130  Goal "!!(x::real). x ~= 0r ==> ? y. y*x = 1r";
  12.131  by (asm_simp_tac (simpset() addsimps [real_mult_commute,
  12.132 -    real_mult_inv_right_ex]) 1);
  12.133 +				      real_mult_inv_right_ex]) 1);
  12.134  qed "real_mult_inv_left_ex";
  12.135  
  12.136 -Goalw [rinv_def] "!!(x::real). x ~= 0r ==> rinv(x)*x = 1r";
  12.137 +Goalw [rinv_def] "x ~= 0r ==> rinv(x)*x = 1r";
  12.138  by (forward_tac [real_mult_inv_left_ex] 1);
  12.139  by (Step_tac 1);
  12.140  by (rtac selectI2 1);
  12.141  by Auto_tac;
  12.142  qed "real_mult_inv_left";
  12.143  
  12.144 -Goal "!!(x::real). x ~= 0r ==> x*rinv(x) = 1r";
  12.145 +Goal "x ~= 0r ==> x*rinv(x) = 1r";
  12.146  by (auto_tac (claset() addIs [real_mult_commute RS subst],
  12.147                simpset() addsimps [real_mult_inv_left]));
  12.148  qed "real_mult_inv_right";
  12.149 @@ -517,15 +517,16 @@
  12.150  Goal "(c::real) ~= 0r ==> (a*c=b*c) = (a=b)";
  12.151  by (Step_tac 1);
  12.152  by (dres_inst_tac [("f","%x. x*rinv c")] arg_cong 1);
  12.153 -by (asm_full_simp_tac (simpset() addsimps [real_mult_inv_right] @ real_mult_ac)  1);
  12.154 +by (asm_full_simp_tac
  12.155 +    (simpset() addsimps [real_mult_inv_right] @ real_mult_ac)  1);
  12.156  qed "real_mult_right_cancel";
  12.157  
  12.158 -Goal "!!a. c*a ~= c*b ==> a ~= b";
  12.159 -by (Auto_tac);
  12.160 +Goal "c*a ~= c*b ==> a ~= b";
  12.161 +by Auto_tac;
  12.162  qed "real_mult_left_cancel_ccontr";
  12.163  
  12.164 -Goal "!!a. a*c ~= b*c ==> a ~= b";
  12.165 -by (Auto_tac);
  12.166 +Goal "a*c ~= b*c ==> a ~= b";
  12.167 +by Auto_tac;
  12.168  qed "real_mult_right_cancel_ccontr";
  12.169  
  12.170  Goalw [rinv_def] "x ~= 0r ==> rinv(x) ~= 0r";
  12.171 @@ -539,7 +540,7 @@
  12.172  
  12.173  Addsimps [real_mult_inv_left,real_mult_inv_right];
  12.174  
  12.175 -Goal "!!x. [| x ~= 0r; y ~= 0r |] ==> x * y ~= 0r";
  12.176 +Goal "[| x ~= 0r; y ~= 0r |] ==> x * y ~= 0r";
  12.177  by (Step_tac 1);
  12.178  by (dres_inst_tac [("f","%z. rinv x*z")] arg_cong 1);
  12.179  by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
  12.180 @@ -569,8 +570,7 @@
  12.181  by Auto_tac;
  12.182  qed "real_minus_rinv";
  12.183  
  12.184 -Goal "!!x y. [| x ~= 0r; y ~= 0r |] \
  12.185 -\                     ==> rinv(x*y) = rinv(x)*rinv(y)";
  12.186 +Goal "[| x ~= 0r; y ~= 0r |] ==> rinv(x*y) = rinv(x)*rinv(y)";
  12.187  by (forw_inst_tac [("y","y")] real_mult_not_zero 1 THEN assume_tac 1);
  12.188  by (res_inst_tac [("c1","x")] (real_mult_left_cancel RS iffD1) 1);
  12.189  by (auto_tac (claset(),simpset() addsimps [real_mult_assoc RS sym]));
  12.190 @@ -778,7 +778,7 @@
  12.191                 addEs [real_less_irrefl]) 1);
  12.192  qed "real_of_preal_not_less_zero";
  12.193  
  12.194 -Goal "0r < - - real_of_preal m";
  12.195 +Goal "0r < - (- real_of_preal m)";
  12.196  by (simp_tac (simpset() addsimps 
  12.197      [real_of_preal_zero_less]) 1);
  12.198  qed "real_minus_minus_zero_less";
  12.199 @@ -970,7 +970,7 @@
  12.200  qed "real_minus_zero_less_iff2";
  12.201  
  12.202  (*Alternative definition for real_less*)
  12.203 -Goal "!!(R::real). R < S ==> ? T. 0r < T & R + T = S";
  12.204 +Goal "R < S ==> ? T. 0r < T & R + T = S";
  12.205  by (res_inst_tac [("x","R")]  real_of_preal_trichotomyE 1);
  12.206  by (ALLGOALS(res_inst_tac [("x","S")]  real_of_preal_trichotomyE));
  12.207  by (auto_tac (claset() addSDs [preal_less_add_left_Ex],
  12.208 @@ -988,19 +988,19 @@
  12.209  qed "real_less_add_positive_left_Ex";
  12.210  
  12.211  (** change naff name(s)! **)
  12.212 -Goal "(W < S) ==> (0r < S + -W)";
  12.213 +Goal "(W < S) ==> (0r < S + (-W))";
  12.214  by (dtac real_less_add_positive_left_Ex 1);
  12.215  by (auto_tac (claset(),
  12.216  	      simpset() addsimps [real_add_minus,
  12.217      real_add_zero_right] @ real_add_ac));
  12.218  qed "real_less_sum_gt_zero";
  12.219  
  12.220 -Goal "!!S::real. T = S + W ==> S = T + -W";
  12.221 +Goal "!!S::real. T = S + W ==> S = T + (-W)";
  12.222  by (asm_simp_tac (simpset() addsimps real_add_ac) 1);
  12.223  qed "real_lemma_change_eq_subj";
  12.224  
  12.225  (* FIXME: long! *)
  12.226 -Goal "(0r < S + -W) ==> (W < S)";
  12.227 +Goal "(0r < S + (-W)) ==> (W < S)";
  12.228  by (rtac ccontr 1);
  12.229  by (dtac (real_leI RS real_le_imp_less_or_eq) 1);
  12.230  by (auto_tac (claset(),
  12.231 @@ -1015,7 +1015,7 @@
  12.232  by (auto_tac (claset() addEs [real_less_asym], simpset()));
  12.233  qed "real_sum_gt_zero_less";
  12.234  
  12.235 -Goal "(0r < S + -W) = (W < S)";
  12.236 +Goal "(0r < S + (-W)) = (W < S)";
  12.237  by (blast_tac (claset() addIs [real_less_sum_gt_zero,
  12.238  			       real_sum_gt_zero_less]) 1);
  12.239  qed "real_less_sum_gt_0_iff";
    13.1 --- a/src/HOL/Real/RealDef.thy	Wed Jul 28 22:01:58 1999 +0200
    13.2 +++ b/src/HOL/Real/RealDef.thy	Thu Jul 29 12:44:57 1999 +0200
    13.3 @@ -33,7 +33,7 @@
    13.4    real_minus_def
    13.5      "- R ==  Abs_real(UN (x,y):Rep_real(R). realrel^^{(y,x)})"
    13.6  
    13.7 -  real_diff_def "x - y == x + -(y::real)"
    13.8 +  real_diff_def "x - y == x + (- y :: real)"
    13.9  
   13.10  constdefs
   13.11  
   13.12 @@ -49,7 +49,7 @@
   13.13    "real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))"
   13.14  
   13.15    real_of_nat :: nat => real          
   13.16 -  "real_of_nat n    == real_of_posnat n + -1r"
   13.17 +  "real_of_nat n    == real_of_posnat n + (-1r)"
   13.18  
   13.19  defs
   13.20  
    14.1 --- a/src/HOL/UNITY/Deadlock.ML	Wed Jul 28 22:01:58 1999 +0200
    14.2 +++ b/src/HOL/UNITY/Deadlock.ML	Thu Jul 29 12:44:57 1999 +0200
    14.3 @@ -9,15 +9,13 @@
    14.4  
    14.5  (*Trivial, two-process case*)
    14.6  Goalw [constrains_def, stable_def]
    14.7 -    "[| F : (A Int B) co A;  F : (B Int A) co B |] \
    14.8 -\    ==> F : stable (A Int B)";
    14.9 +    "[| F : (A Int B) co A;  F : (B Int A) co B |] ==> F : stable (A Int B)";
   14.10  by (Blast_tac 1);
   14.11  result();
   14.12  
   14.13  
   14.14  (*a simplification step*)
   14.15 -Goal "(INT i: atMost n. A(Suc i) Int A i) = \
   14.16 -\     (INT i: atMost (Suc n). A i)";
   14.17 +Goal "(INT i: atMost n. A(Suc i) Int A i) = (INT i: atMost (Suc n). A i)";
   14.18  by (induct_tac "n" 1);
   14.19  by (ALLGOALS (asm_simp_tac (simpset() addsimps [atMost_Suc])));
   14.20  by (blast_tac (claset() addEs [le_SucE] addSEs [equalityE]) 1);
   14.21 @@ -25,8 +23,8 @@
   14.22  
   14.23  
   14.24  (*Dual of the required property.  Converse inclusion fails.*)
   14.25 -Goal "(UN i: lessThan n. A i) Int -(A n) <=  \
   14.26 -\     (UN i: lessThan n. (A i) Int -(A(Suc i)))";
   14.27 +Goal "(UN i: lessThan n. A i) Int (- A n) <=  \
   14.28 +\     (UN i: lessThan n. (A i) Int (- A (Suc i)))";
   14.29  by (induct_tac "n" 1);
   14.30  by (Asm_simp_tac 1);
   14.31  by (simp_tac (simpset() addsimps [lessThan_Suc]) 1);
   14.32 @@ -56,13 +54,12 @@
   14.33  by (induct_tac "n" 1);
   14.34  by (Asm_simp_tac 1);
   14.35  by (asm_simp_tac
   14.36 -    (simpset() addsimps Int_ac @
   14.37 -			[Int_Un_distrib, Int_Un_distrib2, lemma,
   14.38 -			 lessThan_Suc, atMost_Suc]) 1);
   14.39 +    (simpset() addsimps Int_ac @ [Int_Un_distrib, Int_Un_distrib2, lemma,
   14.40 +				  lessThan_Suc, atMost_Suc]) 1);
   14.41  qed "INT_le_equals_Int";
   14.42  
   14.43  Goal "(INT i: atMost (Suc n). A i) = \
   14.44 -\         A 0 Int (INT i: atMost n. -A i Un A(Suc i))";
   14.45 +\     A 0 Int (INT i: atMost n. -A i Un A(Suc i))";
   14.46  by (simp_tac (simpset() addsimps [lessThan_Suc_atMost, INT_le_equals_Int]) 1);
   14.47  qed "INT_le_Suc_equals_Int";
   14.48  
   14.49 @@ -73,9 +70,8 @@
   14.50  \       ALL i: atMost n. F : (A(Suc i) Int A i) co \
   14.51  \                            (-A i Un A(Suc i)) |] \
   14.52  \    ==> F : stable (INT i: atMost (Suc n). A i)";
   14.53 -
   14.54  by (rtac ([zeroprem, allprem RS ball_constrains_INT] MRS 
   14.55 -    constrains_Int RS constrains_weaken) 1);
   14.56 +	  constrains_Int RS constrains_weaken) 1);
   14.57  by (simp_tac (simpset() addsimps [Collect_le_Int_equals, 
   14.58  				  Int_assoc, INT_absorb]) 1);
   14.59  by (simp_tac (simpset() addsimps [INT_le_Suc_equals_Int]) 1);
    15.1 --- a/src/HOL/equalities.ML	Wed Jul 28 22:01:58 1999 +0200
    15.2 +++ b/src/HOL/equalities.ML	Thu Jul 29 12:44:57 1999 +0200
    15.3 @@ -338,25 +338,25 @@
    15.4  
    15.5  section "Set complement";
    15.6  
    15.7 -Goal "A Int -A = {}";
    15.8 +Goal "A Int (-A) = {}";
    15.9  by (Blast_tac 1);
   15.10  qed "Compl_disjoint";
   15.11  Addsimps[Compl_disjoint];
   15.12  
   15.13 -Goal "A Un -A = UNIV";
   15.14 +Goal "A Un (-A) = UNIV";
   15.15  by (Blast_tac 1);
   15.16  qed "Compl_partition";
   15.17  
   15.18 -Goal "- -A = (A:: 'a set)";
   15.19 +Goal "- (-A) = (A:: 'a set)";
   15.20  by (Blast_tac 1);
   15.21  qed "double_complement";
   15.22  Addsimps[double_complement];
   15.23  
   15.24 -Goal "-(A Un B) = -A Int -B";
   15.25 +Goal "-(A Un B) = (-A) Int (-B)";
   15.26  by (Blast_tac 1);
   15.27  qed "Compl_Un";
   15.28  
   15.29 -Goal "-(A Int B) = -A Un -B";
   15.30 +Goal "-(A Int B) = (-A) Un (-B)";
   15.31  by (Blast_tac 1);
   15.32  qed "Compl_Int";
   15.33  
   15.34 @@ -615,7 +615,7 @@
   15.35  
   15.36  section "-";
   15.37  
   15.38 -Goal "A-B = A Int -B";
   15.39 +Goal "A-B = A Int (-B)";
   15.40  by (Blast_tac 1);
   15.41  qed "Diff_eq";
   15.42  
   15.43 @@ -719,7 +719,7 @@
   15.44  by (Blast_tac 1);
   15.45  qed "Diff_Int_distrib2";
   15.46  
   15.47 -Goal "A - - B = A Int B";
   15.48 +Goal "A - (- B) = A Int B";
   15.49  by Auto_tac;
   15.50  qed "Diff_Compl";
   15.51  Addsimps [Diff_Compl];
    16.1 --- a/src/HOL/simpdata.ML	Wed Jul 28 22:01:58 1999 +0200
    16.2 +++ b/src/HOL/simpdata.ML	Thu Jul 29 12:44:57 1999 +0200
    16.3 @@ -285,11 +285,11 @@
    16.4  by (Blast_tac 1);
    16.5  qed "if_False";
    16.6  
    16.7 -Goalw [if_def] "!!P. P ==> (if P then x else y) = x";
    16.8 +Goalw [if_def] "P ==> (if P then x else y) = x";
    16.9  by (Blast_tac 1);
   16.10  qed "if_P";
   16.11  
   16.12 -Goalw [if_def] "!!P. ~P ==> (if P then x else y) = y";
   16.13 +Goalw [if_def] "~P ==> (if P then x else y) = y";
   16.14  by (Blast_tac 1);
   16.15  qed "if_not_P";
   16.16  
   16.17 @@ -319,8 +319,7 @@
   16.18  qed "if_eq_cancel";
   16.19  
   16.20  (*This form is useful for expanding IFs on the RIGHT of the ==> symbol*)
   16.21 -Goal
   16.22 -    "(if P then Q else R) = ((P-->Q) & (~P-->R))";
   16.23 +Goal "(if P then Q else R) = ((P-->Q) & (~P-->R))";
   16.24  by (rtac split_if 1);
   16.25  qed "if_bool_eq_conj";
   16.26  
   16.27 @@ -398,8 +397,6 @@
   16.28  val Addsplits        = Splitter.Addsplits;
   16.29  val Delsplits        = Splitter.Delsplits;
   16.30  
   16.31 -(** 'if' congruence rules: neither included by default! *)
   16.32 -
   16.33  (*In general it seems wrong to add distributive laws by default: they
   16.34    might cause exponential blow-up.  But imp_disjL has been in for a while
   16.35    and cannot be removed without affecting existing proofs.  Moreover, 
   16.36 @@ -464,7 +461,8 @@
   16.37  by (asm_simp_tac (HOL_ss addsimps prems) 1);
   16.38  qed "if_cong";
   16.39  
   16.40 -(*Prevents simplification of x and y: much faster*)
   16.41 +(*Prevents simplification of x and y: faster and allows the execution
   16.42 +  of functional programs. NOW THE DEFAULT.*)
   16.43  Goal "b=c ==> (if b then x else y) = (if c then x else y)";
   16.44  by (etac arg_cong 1);
   16.45  qed "if_weak_cong";