src/HOL/Real/PRat.ML

     ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Description : The positive rationals
 *) 
-
-Delrules [equalityI];
 
 (*** Many theorems similar to those in theory Integ ***)
 (*** Proving that ratrel is an equivalence relation ***)
 
 Goal "[| (x1::pnat) * y2 = x2 * y1; x2 * y3 = x3 * y2 |] \

 qed "eq_Abs_prat";
 
 (**** 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]
       "qinv (Abs_prat(ratrel^^{(x,y)})) = Abs_prat(ratrel ^^ {(y,x)})";
 by (simp_tac (simpset() addsimps 

 qed "prat_add_congruent2_lemma";
 
 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";
 
 Goalw [prat_add_def]
    "Abs_prat((ratrel^^{(x1,y1)})) + Abs_prat((ratrel^^{(x2,y2)})) =   \

 
 Goalw [congruent2_def]
     "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);
 by (asm_simp_tac (simpset() addsimps [pnat_mult_assoc RS sym]) 1);
 by (asm_simp_tac (simpset() addsimps pnat_mult_ac) 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_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";
 by (rtac allI 1);
 by (res_inst_tac [("z","q")] eq_Abs_prat 1);