src/ZF/ex/Integ.ML

 
 (**** zminus: unary negation on integ ****)
 
 goalw Integ.thy [congruent_def]
     "congruent(intrel, %<x,y>. intrel``{<y,x>})";
-by (safe_tac (claset()));
+by Safe_tac;
 by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
 qed "zminus_congruent";
 
 (*Resolve th against the corresponding facts for zminus*)
 val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];

 qed "zminus_type";
 
 goalw Integ.thy [integ_def,zminus_def]
     "!!z w. [| $~z = $~w;  z: integ;  w: integ |] ==> z=w";
 by (etac (zminus_ize UN_equiv_class_inject) 1);
-by (safe_tac (claset()));
+by Safe_tac;
 (*The setloop is only needed because assumptions are in the wrong order!*)
 by (asm_full_simp_tac (simpset() addsimps add_ac
                        setloop dtac eq_intrelD) 1);
 qed "zminus_inject";
 

 
 (**** znegative: the test for negative integers ****)
 
 (*No natural number is negative!*)
 goalw Integ.thy [znegative_def, znat_def]  "~ znegative($# n)";
-by (safe_tac (claset()));
+by Safe_tac;
 by (dres_inst_tac [("psi", "?lhs=?rhs")] asm_rl 1);
 by (dres_inst_tac [("psi", "?lhs<?rhs")] asm_rl 1);
 by (fast_tac (claset() addss
               (simpset() addsimps [add_le_self2 RS le_imp_not_lt])) 1);
 qed "not_znegative_znat";

 
 (**** zmagnitude: magnitide of an integer, as a natural number ****)
 
 goalw Integ.thy [congruent_def]
     "congruent(intrel, %<x,y>. (y#-x) #+ (x#-y))";
-by (safe_tac (claset()));
+by Safe_tac;
 by (ALLGOALS Asm_simp_tac);
 by (etac rev_mp 1);
 by (res_inst_tac [("m","x1"),("n","y1")] diff_induct 1 THEN 
     REPEAT (assume_tac 1));
 by (Asm_simp_tac 3);

 goalw Integ.thy [congruent2_def]
     "congruent2(intrel, %z1 z2.                      \
 \         let <x1,y1>=z1; <x2,y2>=z2                 \
 \                           in intrel``{<x1#+x2, y1#+y2>})";
 (*Proof via congruent2_commuteI seems longer*)
-by (safe_tac (claset()));
+by Safe_tac;
 by (asm_simp_tac (simpset() addsimps [add_assoc, Let_def]) 1);
 (*The rest should be trivial, but rearranging terms is hard;
   add_ac does not help rewriting with the assumptions.*)
 by (res_inst_tac [("m1","x1a")] (add_left_commute RS ssubst) 1);
 by (res_inst_tac [("m1","x2a")] (add_left_commute RS ssubst) 3);

 goal Integ.thy 
     "congruent2(intrel, %p1 p2.                 \
 \               split(%x1 y1. split(%x2 y2.     \
 \                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))";
 by (rtac (equiv_intrel RS congruent2_commuteI) 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (ALLGOALS Asm_simp_tac);
 (*Proof that zmult is congruent in one argument*)
 by (asm_simp_tac 
     (simpset() addsimps (add_ac @ [add_mult_distrib_left RS sym])) 2);
 by (asm_simp_tac