# HG changeset patch
# User paulson
# Date 971770996 -7200
# Node ID 529c65b5dcde7dfb44bcef3a310cd71f8582a960
# Parent  178a272bceeb49e2a42db48b8e14fc73a8be6a63
restoration of "equalityI"; renaming of contrapos rules

diff -r 178a272bceeb -r 529c65b5dcde src/HOL/Real/PRat.ML
--- a/src/HOL/Real/PRat.ML	Tue Oct 17 10:21:12 2000 +0200
+++ b/src/HOL/Real/PRat.ML	Tue Oct 17 10:23:16 2000 +0200
@@ -5,8 +5,6 @@
     Description : The positive rationals
 *) 
 
-Delrules [equalityI];
-
 (*** Many theorems similar to those in theory Integ ***)
 (*** Proving that ratrel is an equivalence relation ***)
 
@@ -109,8 +107,7 @@
 (**** qinv: inverse on prat ****)
 
 Goalw [congruent_def] "congruent ratrel (%(x,y). ratrel^^{(y,x)})";
-by Safe_tac;
-by (asm_full_simp_tac (simpset() addsimps [pnat_mult_commute]) 1);
+by (auto_tac (claset(), simpset() addsimps [pnat_mult_commute]));  
 qed "qinv_congruent";
 
 Goalw [qinv_def]
@@ -150,7 +147,8 @@
 Goal "congruent2 ratrel (%p1 p2.                  \
 \        (%(x1,y1). (%(x2,y2). ratrel^^{(x1*y2 + x2*y1, y1*y2)}) p2) p1)";
 by (rtac (equiv_ratrel RS congruent2_commuteI) 1);
-by (auto_tac (claset(),simpset() addsimps [prat_add_congruent2_lemma]));
+by (auto_tac (claset() delrules [equalityI],
+              simpset() addsimps [prat_add_congruent2_lemma]));
 by (asm_simp_tac (simpset() addsimps [pnat_mult_commute,pnat_add_commute]) 1);
 qed "prat_add_congruent2";
 
@@ -193,7 +191,7 @@
     "congruent2 ratrel (%p1 p2.                  \
 \         (%(x1,y1). (%(x2,y2). ratrel^^{(x1*x2, y1*y2)}) p2) p1)";
 (*Proof via congruent2_commuteI seems longer*)
-by Safe_tac;
+by (Clarify_tac 1);
 by (asm_simp_tac (simpset() addsimps [pnat_mult_assoc]) 1);
 (*The rest should be trivial, but rearranging terms is hard*)
 by (res_inst_tac [("x1","x1a")] (pnat_mult_left_commute RS ssubst) 1);
@@ -385,7 +383,7 @@
 qed "prat_less_not_sym";
 
 (* [| x < y;  ~P ==> y < x |] ==> P *)
-bind_thm ("prat_less_asym", prat_less_not_sym RS swap);
+bind_thm ("prat_less_asym", prat_less_not_sym RS contrapos_np);
 
 (* half of positive fraction exists- Gleason p. 120- Proposition 9-2.6(i)*)
 Goal "!(q::prat). EX x. x + x = q";
diff -r 178a272bceeb -r 529c65b5dcde src/HOL/Real/PReal.ML
--- a/src/HOL/Real/PReal.ML	Tue Oct 17 10:21:12 2000 +0200
+++ b/src/HOL/Real/PReal.ML	Tue Oct 17 10:23:16 2000 +0200
@@ -108,9 +108,7 @@
 Goal "EX x. x~: Rep_preal X";
 by (cut_inst_tac [("x","X")] Rep_preal 1);
 by (dtac prealE_lemma2 1);
-by (rtac ccontr 1);
 by (auto_tac (claset(),simpset() addsimps [psubset_def]));
-by (blast_tac (claset() addIs [set_ext] addEs [swap]) 1);
 qed "not_mem_Rep_preal_Ex";
 
 (** preal_of_prat: the injection from prat to preal **)
@@ -178,7 +176,7 @@
 qed "preal_less_not_sym";
 
 (* [| x < y;  ~P ==> y < x |] ==> P *)
-bind_thm ("preal_less_asym", preal_less_not_sym RS swap);
+bind_thm ("preal_less_asym", preal_less_not_sym RS contrapos_np);
 
 Goalw [preal_less_def] 
       "(r1::preal) < r2 | r1 = r2 | r2 < r1";
@@ -812,9 +810,6 @@
 
 (* useful lemmas - proved elsewhere? *)
 Goalw [psubset_def] "A < B ==> EX x. x ~: A & x : B";
-by (etac conjE 1);
-by (etac swap 1);
-by (etac equalityI 1);
 by Auto_tac;
 qed "lemma_psubset_mem";
 
@@ -1204,7 +1199,7 @@
 by (asm_full_simp_tac (simpset() addsimps [psubset_def]) 1);
 by (dtac bspec 1 THEN assume_tac 1);
 by (REPEAT(etac conjE 1));
-by (EVERY1[rtac swap, assume_tac, rtac set_ext]);
+by (EVERY1[rtac contrapos_np, assume_tac, rtac set_ext]);
 by (auto_tac (claset() addSDs [lemma_psubset_mem],simpset()));
 by (cut_inst_tac [("r1.0","Xa"),("r2.0","Ya")] preal_linear 1);
 by (auto_tac (claset() addDs [psubsetD],simpset() addsimps [preal_less_def]));
diff -r 178a272bceeb -r 529c65b5dcde src/HOL/Real/RealDef.ML
--- a/src/HOL/Real/RealDef.ML	Tue Oct 17 10:21:12 2000 +0200
+++ b/src/HOL/Real/RealDef.ML	Tue Oct 17 10:23:16 2000 +0200
@@ -108,7 +108,7 @@
 
 Goalw [congruent_def]
   "congruent realrel (%p. (%(x,y). realrel^^{(y,x)}) p)";
-by Safe_tac;
+by (Clarify_tac 1); 
 by (asm_full_simp_tac (simpset() addsimps [preal_add_commute]) 1);
 qed "real_minus_congruent";
 
@@ -151,7 +151,7 @@
 Goalw [congruent2_def]
     "congruent2 realrel (%p1 p2.                  \
 \         (%(x1,y1). (%(x2,y2). realrel^^{(x1+x2, y1+y2)}) p2) p1)";
-by Safe_tac;
+by (Clarify_tac 1); 
 by (asm_simp_tac (simpset() addsimps [preal_add_assoc]) 1);
 by (res_inst_tac [("z1.1","x1a")] (preal_add_left_commute RS ssubst) 1);
 by (asm_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
@@ -317,7 +317,7 @@
     "congruent2 realrel (%p1 p2.                  \
 \         (%(x1,y1). (%(x2,y2). realrel^^{(x1*x2 + y1*y2, x1*y2+x2*y1)}) p2) p1)";
 by (rtac (equiv_realrel RS congruent2_commuteI) 1);
-by Safe_tac;
+by (Clarify_tac 1); 
 by (rewtac split_def);
 by (asm_simp_tac (simpset() addsimps [preal_mult_commute,preal_add_commute]) 1);
 by (auto_tac (claset(),simpset() addsimps [real_mult_congruent2_lemma]));
@@ -647,7 +647,7 @@
 qed "real_less_not_sym";
 
 (* [| x < y;  ~P ==> y < x |] ==> P *)
-bind_thm ("real_less_asym", real_less_not_sym RS swap);
+bind_thm ("real_less_asym", real_less_not_sym RS contrapos_np);
 
 Goalw [real_of_preal_def] 
      "real_of_preal ((z1::preal) + z2) = \