well-formed asym rules; misc. tidying

--- a/src/HOL/Real/PNat.ML	Thu Sep 10 17:28:36 1998 +0200
+++ b/src/HOL/Real/PNat.ML	Thu Sep 10 17:29:56 1998 +0200
@@ -246,8 +246,8 @@
 by (etac less_not_sym 1);
 qed "pnat_less_not_sym";
 
-(* [| x < y; y < x |] ==> P *)
-bind_thm ("pnat_less_asym",pnat_less_not_sym RS notE);
+(* [| x < y;  ~P ==> y < x |] ==> P *)
+bind_thm ("pnat_less_asym", pnat_less_not_sym RS swap);
 
 Goalw [pnat_less_def] "~ y < (y::pnat)";
 by Auto_tac;

--- a/src/HOL/Real/PRat.ML	Thu Sep 10 17:28:36 1998 +0200
+++ b/src/HOL/Real/PRat.ML	Thu Sep 10 17:29:56 1998 +0200
@@ -395,14 +395,14 @@
 (*** y < y ==> P ***)
 bind_thm("prat_less_irrefl",prat_less_not_refl RS notE);
 
-Goal "!! (q1::prat). [| q1 < q2; q2 < q1 |] ==> P";
+Goal "!! (q1::prat). q1 < q2 ==> ~ q2 < q1";
+by (rtac notI 1);
 by (dtac prat_less_trans 1 THEN assume_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [prat_less_not_refl]) 1);
-qed "prat_less_asym";
+qed "prat_less_not_sym";
 
-Goal "!! (q1::prat). q1 < q2 ==> ~ q2 < q1";
-by (auto_tac (claset() addSDs [prat_less_asym],simpset()));
-qed "prat_less_not_sym";
+(* [| x < y;  ~P ==> y < x |] ==> P *)
+bind_thm ("prat_less_asym", prat_less_not_sym RS swap);
 
 (* half of positive fraction exists- Gleason p. 120- Proposition 9-2.6(i)*)
 Goal "!(q::prat). ? x. x + x = q";

--- a/src/HOL/Real/PReal.ML	Thu Sep 10 17:28:36 1998 +0200
+++ b/src/HOL/Real/PReal.ML	Thu Sep 10 17:29:56 1998 +0200
@@ -137,10 +137,10 @@
 by Auto_tac;
 by (dtac prat_dense 1 THEN etac exE 1);
 by (eres_inst_tac [("c","xa")] equalityCE 1);
-by (auto_tac (claset() addDs [prat_less_asym],simpset()));
+by (auto_tac (claset() addDs [prat_less_not_sym],simpset()));
 by (dtac prat_dense 1 THEN etac exE 1);
 by (eres_inst_tac [("c","xa")] equalityCE 1);
-by (auto_tac (claset() addDs [prat_less_asym],simpset()));
+by (auto_tac (claset() addDs [prat_less_not_sym],simpset()));
 qed "lemma_prat_set_eq";
 
 Goal "inj(preal_prat)";
@@ -203,10 +203,14 @@
               simpset() addsimps [psubset_def]));
 qed "preal_less_trans";
 
-Goal "!! (q1::preal). [| q1 < q2; q2 < q1 |] ==> P";
+Goal "!! (q1::preal). q1 < q2 ==> ~ q2 < q1";
+by (rtac notI 1);
 by (dtac preal_less_trans 1 THEN assume_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [preal_less_not_refl]) 1);
-qed "preal_less_asym";
+qed "preal_less_not_sym";
+
+(* [| x < y;  ~P ==> y < x |] ==> P *)
+bind_thm ("preal_less_asym", preal_less_not_sym RS swap);
 
 Goalw [preal_less_def] 
       "(r1::preal) < r2 | r1 = r2 | r2 < r1";
@@ -217,9 +221,8 @@
 by (fast_tac (claset() addDs [not_in_preal_ub]) 1);
 qed "preal_linear";
 
-Goal
-    "!!(r1::preal). [| r1 < r2 ==> P;  r1 = r2 ==> P; \
-\          r2 < r1 ==> P |] ==> P";
+Goal "!!(r1::preal). [| r1 < r2 ==> P;  r1 = r2 ==> P; \
+\                       r2 < r1 ==> P |] ==> P";
 by (cut_inst_tac [("r1.0","r1"),("r2.0","r2")] preal_linear 1);
 by Auto_tac;
 qed "preal_linear_less2";

--- a/src/HOL/Real/Real.ML	Thu Sep 10 17:28:36 1998 +0200
+++ b/src/HOL/Real/Real.ML	Thu Sep 10 17:29:56 1998 +0200
@@ -4,8 +4,6 @@
     Description : The reals
 *)
 
-open Real;
-
 (*** Proving that realrel is an equivalence relation ***)
 
 Goal "[| (x1::preal) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] \
@@ -22,18 +20,18 @@
 
 Goalw [realrel_def]
     "(((x1,y1),(x2,y2)): realrel) = (x1 + y2 = x2 + y1)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "realrel_iff";
 
 Goalw [realrel_def]
     "[| x1 + y2 = x2 + y1 |] ==> ((x1,y1),(x2,y2)): realrel";
-by (Fast_tac  1);
+by (Blast_tac  1);
 qed "realrelI";
 
 Goalw [realrel_def]
   "p: realrel --> (EX x1 y1 x2 y2. \
 \                  p = ((x1,y1),(x2,y2)) & x1 + y2 = x2 + y1)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "realrelE_lemma";
 
 val [major,minor] = goal thy
@@ -90,7 +88,7 @@
 by (REPEAT (rtac realrel_in_real 1));
 by (dtac eq_equiv_class 1);
 by (rtac equiv_realrel 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 by Safe_tac;
 by (Asm_full_simp_tac 1);
 qed "inj_real_preal";
@@ -219,7 +217,7 @@
 qed "real_add_minus_left";
 
 Goal "? y. (x::real) + y = 0r";
-by (fast_tac (claset() addIs [real_add_minus]) 1);
+by (blast_tac (claset() addIs [real_add_minus]) 1);
 qed "real_minus_ex";
 
 Goal "?! y. (x::real) + y = 0r";
@@ -247,7 +245,7 @@
 Goal "? y. x = %~y";
 by (cut_inst_tac [("x","x")] real_minus_ex 1);
 by (etac exE 1 THEN dtac real_add_minus_eq_minus 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "real_as_add_inverse_ex";
 
 (* real_minus_add_distrib *)
@@ -499,13 +497,13 @@
  "P < (Q::real) = (EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & \
 \                                  (x1,y1::preal):Rep_real(P) & \
 \                                  (x2,y2):Rep_real(Q))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "real_less_iff";
 
 Goalw [real_less_def]
  "[| x1 + y2 < x2 + y1; (x1,y1::preal):Rep_real(P); \
 \         (x2,y2):Rep_real(Q) |] ==> P < (Q::real)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "real_lessI";
 
 Goalw [real_less_def]
@@ -521,7 +519,7 @@
  "R1 < (R2::real) ==> (EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & \
 \                                  (x1,y1::preal):Rep_real(R1) & \
 \                                  (x2,y2):Rep_real(R2))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "real_lessD";
 
 (* real_less is a strong order i.e nonreflexive and transitive *)
@@ -621,7 +619,7 @@
 qed "real_preal_ExD";
 
 Goal "(? m. Abs_real (realrel ^^ {(x,y)}) = %#m) = (y < x)";
-by (fast_tac (claset() addSIs [real_preal_ExI,real_preal_ExD]) 1);
+by (blast_tac (claset() addSIs [real_preal_ExI,real_preal_ExD]) 1);
 qed "real_preal_iff";
 
 (*** Gleason prop 9-4.4 p 127 ***)
@@ -654,13 +652,13 @@
     real_preal_def,real_less_def]));
 by (REPEAT(rtac exI 1));
 by (EVERY[rtac conjI 1, rtac conjI 2]);
-by (REPEAT(Fast_tac 2));
+by (REPEAT(Blast_tac 2));
 by (simp_tac (simpset() addsimps [preal_self_less_add_left] 
     delsimps [preal_add_less_iff2]) 1);
 qed "real_preal_lessI";
 
 Goal "(%#m1 < %#m2) = (m1 < m2)";
-by (fast_tac (claset() addIs [real_preal_lessI,real_preal_lessD]) 1);
+by (blast_tac (claset() addIs [real_preal_lessI,real_preal_lessD]) 1);
 qed "real_preal_less_iff1";
 
 Addsimps [real_preal_less_iff1];
@@ -670,7 +668,7 @@
     [real_preal_def,real_less_def,real_minus]));
 by (REPEAT(rtac exI 1));
 by (EVERY[rtac conjI 1, rtac conjI 2]);
-by (REPEAT(Fast_tac 2));
+by (REPEAT(Blast_tac 2));
 by (full_simp_tac (simpset() addsimps preal_add_ac) 1);
 by (full_simp_tac (simpset() addsimps [preal_self_less_add_right,
     preal_add_assoc RS sym]) 1);
@@ -681,15 +679,15 @@
     [real_preal_def,real_less_def,real_minus]));
 by (REPEAT(rtac exI 1));
 by (EVERY[rtac conjI 1, rtac conjI 2]);
-by (REPEAT(Fast_tac 2));
+by (REPEAT(Blast_tac 2));
 by (full_simp_tac (simpset() addsimps 
   [preal_self_less_add_right] @ preal_add_ac) 1);
 qed "real_preal_minus_less_zero";
 
 Goal "~ 0r < %~ %#m";
 by (cut_facts_tac [real_preal_minus_less_zero] 1);
-by (fast_tac (claset() addDs [real_less_trans] 
-               addEs [real_less_irrefl]) 1);
+by (blast_tac (claset() addDs [real_less_trans] 
+                        addEs [real_less_irrefl]) 1);
 qed "real_preal_not_minus_gt_zero";
 
 Goalw [real_zero_def] " 0r < %#m";
@@ -697,14 +695,14 @@
     [real_preal_def,real_less_def,real_minus]));
 by (REPEAT(rtac exI 1));
 by (EVERY[rtac conjI 1, rtac conjI 2]);
-by (REPEAT(Fast_tac 2));
+by (REPEAT(Blast_tac 2));
 by (full_simp_tac (simpset() addsimps 
   [preal_self_less_add_right] @ preal_add_ac) 1);
 qed "real_preal_zero_less";
 
 Goal "~ %#m < 0r";
 by (cut_facts_tac [real_preal_zero_less] 1);
-by (fast_tac (claset() addDs [real_less_trans] 
+by (blast_tac (claset() addDs [real_less_trans] 
                addEs [real_less_irrefl]) 1);
 qed "real_preal_not_less_zero";
 
@@ -719,7 +717,7 @@
     [real_preal_def,real_less_def,real_add]));
 by (REPEAT(rtac exI 1));
 by (EVERY[rtac conjI 1, rtac conjI 2]);
-by (REPEAT(Fast_tac 2));
+by (REPEAT(Blast_tac 2));
 by (full_simp_tac (simpset() addsimps preal_add_ac) 1);
 by (full_simp_tac (simpset() addsimps [preal_self_less_add_right,
     preal_add_assoc RS sym]) 1);
@@ -730,7 +728,7 @@
     [real_preal_def,real_less_def,real_minus]));
 by (REPEAT(rtac exI 1));
 by (EVERY[rtac conjI 1, rtac conjI 2]);
-by (REPEAT(Fast_tac 2));
+by (REPEAT(Blast_tac 2));
 by (full_simp_tac (simpset() addsimps preal_add_ac) 1);
 by (full_simp_tac (simpset() addsimps [preal_self_less_add_right,
     preal_add_assoc RS sym]) 1);
@@ -738,7 +736,7 @@
 
 Goal "~ %#m < %~ %#m1";
 by (cut_facts_tac [real_preal_minus_less_all] 1);
-by (fast_tac (claset() addDs [real_less_trans] 
+by (blast_tac (claset() addDs [real_less_trans] 
                addEs [real_less_irrefl]) 1);
 qed "real_preal_not_minus_gt_all";
 
@@ -747,7 +745,7 @@
     [real_preal_def,real_less_def,real_minus]));
 by (REPEAT(rtac exI 1));
 by (EVERY[rtac conjI 1, rtac conjI 2]);
-by (REPEAT(Fast_tac 2));
+by (REPEAT(Blast_tac 2));
 by (auto_tac (claset(),simpset() addsimps preal_add_ac));
 by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
 by (auto_tac (claset(),simpset() addsimps preal_add_ac));
@@ -758,7 +756,7 @@
     [real_preal_def,real_less_def,real_minus]));
 by (REPEAT(rtac exI 1));
 by (EVERY[rtac conjI 1, rtac conjI 2]);
-by (REPEAT(Fast_tac 2));
+by (REPEAT(Blast_tac 2));
 by (auto_tac (claset(),simpset() addsimps preal_add_ac));
 by (asm_full_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
 by (auto_tac (claset(),simpset() addsimps preal_add_ac));
@@ -799,25 +797,25 @@
 val real_leE = make_elim real_leD;
 
 Goal "(~(w < z)) = (z <= (w::real))";
-by (fast_tac (claset() addSIs [real_leI,real_leD]) 1);
+by (blast_tac (claset() addSIs [real_leI,real_leD]) 1);
 qed "real_less_le_iff";
 
 Goalw [real_le_def] "~ z <= w ==> w<(z::real)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "not_real_leE";
 
 Goalw [real_le_def] "z < w ==> z <= (w::real)";
-by (fast_tac (claset() addEs [real_less_asym]) 1);
+by (blast_tac (claset() addEs [real_less_asym]) 1);
 qed "real_less_imp_le";
 
 Goalw [real_le_def] "!!(x::real). x <= y ==> x < y | x = y";
 by (cut_facts_tac [real_linear] 1);
-by (fast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1);
+by (blast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1);
 qed "real_le_imp_less_or_eq";
 
 Goalw [real_le_def] "z<w | z=w ==> z <=(w::real)";
 by (cut_facts_tac [real_linear] 1);
-by (fast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1);
+by (blast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1);
 qed "real_less_or_eq_imp_le";
 
 Goal "(x <= (y::real)) = (x < y | x=y)";
@@ -830,27 +828,27 @@
 
 val prems = goal Real.thy "!!i. [| i <= j; j < k |] ==> i < (k::real)";
 by (dtac real_le_imp_less_or_eq 1);
-by (fast_tac (claset() addIs [real_less_trans]) 1);
+by (blast_tac (claset() addIs [real_less_trans]) 1);
 qed "real_le_less_trans";
 
 Goal "!! (i::real). [| i < j; j <= k |] ==> i < k";
 by (dtac real_le_imp_less_or_eq 1);
-by (fast_tac (claset() addIs [real_less_trans]) 1);
+by (blast_tac (claset() addIs [real_less_trans]) 1);
 qed "real_less_le_trans";
 
 Goal "[| i <= j; j <= k |] ==> i <= (k::real)";
 by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq,
-            rtac real_less_or_eq_imp_le, fast_tac (claset() addIs [real_less_trans])]);
+            rtac real_less_or_eq_imp_le, blast_tac (claset() addIs [real_less_trans])]);
 qed "real_le_trans";
 
 Goal "[| z <= w; w <= z |] ==> z = (w::real)";
 by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq,
-            fast_tac (claset() addEs [real_less_irrefl,real_less_asym])]);
+            blast_tac (claset() addEs [real_less_irrefl,real_less_asym])]);
 qed "real_le_anti_sym";
 
 Goal "[| ~ y < x; y ~= x |] ==> x < (y::real)";
 by (rtac not_real_leE 1);
-by (fast_tac (claset() addDs [real_le_imp_less_or_eq]) 1);
+by (blast_tac (claset() addDs [real_le_imp_less_or_eq]) 1);
 qed "not_less_not_eq_real_less";
 
 Goal "(0r < %~R) = (R < 0r)";
@@ -964,7 +962,7 @@
 qed "real_sum_gt_zero_less";
 
 Goal "(0r < S + %~W) = (W < S)";
-by (fast_tac (claset() addIs [real_less_sum_gt_zero,
+by (blast_tac (claset() addIs [real_less_sum_gt_zero,
     real_sum_gt_zero_less]) 1);
 qed "real_less_sum_gt_0_iff";
 
@@ -986,17 +984,17 @@
 
 (*** alternative definition for real_less ***)
 Goal "!!(R::real). (? T. 0r < T & R + T = S) = (R < S)";
-by (fast_tac (claset() addSIs [real_less_add_positive_left_Ex,
+by (blast_tac (claset() addSIs [real_less_add_positive_left_Ex,
     real_ex_add_positive_left_less]) 1);
 qed "real_less_iffdef";
 
 Goal "(0r < x) = (%~x < x)";
-by (Step_tac 1);
+by Safe_tac;
 by (rtac ccontr 2 THEN forward_tac 
     [real_leI RS real_le_imp_less_or_eq] 2);
 by (Step_tac 2);
 by (dtac (real_minus_zero_less_iff RS iffD2) 2);
-by (fast_tac (claset() addDs [real_less_trans]) 2);
+by (blast_tac (claset() addIs [real_less_trans]) 2);
 by (auto_tac (claset(),simpset() addsimps 
     [real_gt_zero_preal_Ex,real_preal_minus_less_self]));
 qed "real_gt_zero_iff";
@@ -1120,9 +1118,9 @@
 by (forward_tac [real_sup_lemma2] 2 THEN Auto_tac);
 by (forward_tac [real_sup_lemma2] 1 THEN Auto_tac);
 by (rtac (preal_complete RS spec RS iffD2 RS bexE) 1);
-by (Fast_tac 3);
-by (Fast_tac 1);
-by (Fast_tac 1);
+by (Blast_tac 3);
+by (Blast_tac 1);
+by (Blast_tac 1);
 by (Blast_tac 1);
 qed "posreal_complete";
 

--- a/src/HOL/Real/RealAbs.ML	Thu Sep 10 17:28:36 1998 +0200
+++ b/src/HOL/Real/RealAbs.ML	Thu Sep 10 17:29:56 1998 +0200
@@ -11,7 +11,7 @@
        (adapted version of previously proved theorems about abs)
  ----------------------------------------------------------------------------*)
 Goalw [rabs_def] "rabs r = (if 0r<=r then r else %~r)";
-by (Step_tac 1);
+by Auto_tac;
 qed "rabs_iff";
 
 Goalw [rabs_def] "rabs 0r = 0r";
@@ -39,7 +39,7 @@
 
 Goal "x<=0r ==> rabs x = %~x";
 by (dtac real_le_imp_less_or_eq 1);
-by (fast_tac (HOL_cs addIs [rabs_minus_zero,rabs_minus_eqI2]) 1);
+by (blast_tac (HOL_cs addIs [rabs_minus_zero,rabs_minus_eqI2]) 1);
 qed "rabs_minus_eqI1";
 
 Goalw [rabs_def,real_le_def] "0r<= rabs x";
@@ -154,13 +154,14 @@
 qed "real_mult_0_less";
 
 Goal "[| 0r<y; x<r; y*r<t*s |] ==> y*x<t*s";
-(*why PROOF FAILED for this*)
-by (best_tac (claset() addIs [real_mult_less_mono2, real_less_trans]) 1);
+by (blast_tac (claset() addSIs [real_mult_less_mono2]
+	                addIs  [real_less_trans]) 1);
 qed "real_mult_less_trans";
 
 Goal "!!(x::real) y.[| 0r<=y; x<r; y*r<t*s; 0r<t*s|] ==> y*x<t*s";
 by (dtac real_le_imp_less_or_eq 1);
-by (fast_tac (HOL_cs addEs [(real_mult_0_less RS iffD2),real_mult_less_trans]) 1);
+by (fast_tac (HOL_cs addEs [real_mult_0_less RS iffD2,
+			    real_mult_less_trans]) 1);
 qed "real_mult_le_less_trans";
 
 (* proofs lifted from previous older version *)
@@ -195,7 +196,7 @@
 qed "rabs_mult_le";
 
 Goal "[| 1r < rabs x; r < rabs y|] ==> r < rabs(x*y)";
-by (fast_tac (HOL_cs addIs [rabs_mult_le, real_less_le_trans]) 1);
+by (blast_tac (HOL_cs addIs [rabs_mult_le, real_less_le_trans]) 1);
 qed "rabs_mult_gt";
 
 Goal "rabs(x)<r ==> 0r<r";
@@ -213,7 +214,7 @@
 
 Goal "rabs x =x | rabs x = %~x";
 by (cut_inst_tac [("R1.0","0r"),("R2.0","x")] real_linear 1);
-by (fast_tac (claset() addIs [rabs_eqI2,rabs_minus_eqI2,
+by (blast_tac (claset() addIs [rabs_eqI2,rabs_minus_eqI2,
                             rabs_zero,rabs_minus_zero]) 1);
 qed "rabs_disj";
 
@@ -225,7 +226,7 @@
 qed "rabs_eq_disj";
 
 Goal "(rabs x < r) = (%~r<x & x<r)";
-by (Step_tac 1);
+by Safe_tac;
 by (rtac (real_less_swap_iff RS iffD2) 1);
 by (asm_simp_tac (simpset() addsimps [(rabs_ge_minus_self 
     RS real_le_less_trans)]) 1);