cancel-factor simproc allows shorter proofs

--- a/src/HOL/Hoare/Examples.ML	Tue Dec 19 15:06:59 2000 +0100
+++ b/src/HOL/Hoare/Examples.ML	Tue Dec 19 15:14:36 2000 +0100
@@ -89,11 +89,8 @@
 \ INV {fac A = b * fac a} \
 \ DO b := b*a; a := a-1 OD \
 \ {b = fac A}";
-by (hoare_tac Asm_full_simp_tac 1);
-by (Clarify_tac 1);
-by (case_tac "a" 1);
-by  (ALLGOALS (asm_simp_tac
-     (simpset() addsimps [add_mult_distrib,add_mult_distrib2,mult_assoc])));
+by (hoare_tac (asm_full_simp_tac (simpset() addsplits [nat_diff_split])) 1);
+by Auto_tac;  
 qed "factorial";
 
 (** Square root **)
@@ -199,10 +196,10 @@
 by (asm_simp_tac HOL_basic_ss 1);
 by (REPEAT (etac thin_rl 1));
 by (hoare_tac Asm_full_simp_tac 1);
-    by (SELECT_GOAL (auto_tac (claset(), simpset() addsimps [neq_Nil_conv])) 1);
+    by (force_tac (claset(), simpset() addsimps [neq_Nil_conv]) 1);
    by (blast_tac (claset() addSEs [less_SucE] addIs [Suc_leI]) 1);
   by (blast_tac (claset() addSEs [less_SucE] addIs [less_imp_diff_less]
                           addDs [pred_less_imp_le RS le_imp_less_Suc] ) 1);
- by (SELECT_GOAL (auto_tac (claset(), simpset() addsimps [nth_list_update])) 1);
-by (SELECT_GOAL (auto_tac (claset() addIs [order_antisym], simpset())) 1);
+ by (force_tac (claset(), simpset() addsimps [nth_list_update]) 1);
+by (auto_tac (claset() addIs [order_antisym], simpset()));
 qed "Partition";

--- a/src/HOL/NumberTheory/Factorization.ML	Tue Dec 19 15:06:59 2000 +0100
+++ b/src/HOL/NumberTheory/Factorization.ML	Tue Dec 19 15:14:36 2000 +0100
@@ -57,9 +57,7 @@
 qed "prime_primel";
 
 Goalw [prime_def,dvd_def] "p:prime ==> ~(p dvd 1)";
-by Auto_tac;
-by (case_tac "k" 1);
-by Auto_tac;
+by Auto_tac;  
 qed "prime_nd_one";
 
 Goalw [dvd_def] "[| prod (x#xs) = prod ys |] ==> x dvd (prod ys)";
@@ -258,8 +256,8 @@
 qed "primel_prod_less";
 
 Goal "[| primel xs; p*prod xs = p; p:prime |] ==> xs=[]";
-by (auto_tac (claset() addIs [primel_one_empty,mn_eq_m_one,prime_g_zero], 
-	      simpset()));
+by (auto_tac (claset() addIs [primel_one_empty], 
+	      simpset() addsimps [prime_def]));
 qed "prod_one_empty";
 
 Goal "[| ALL m. m < prod ys --> (ALL xs ys. primel xs & primel ys & \

--- a/src/HOL/NumberTheory/IntPrimes.ML	Tue Dec 19 15:06:59 2000 +0100
+++ b/src/HOL/NumberTheory/IntPrimes.ML	Tue Dec 19 15:14:36 2000 +0100
@@ -507,25 +507,21 @@
 qed "zcong_cancel2";
 
 Goalw [zcong_def,dvd_def]
-      "[| [a = b] (mod m); [a = b] (mod n); zgcd(m,n) = #1 |] \
+      "[| [a = b] (mod m);  [a = b] (mod n);  zgcd(m,n) = #1 |] \
 \     ==> [a=b](mod m*n)";
 by Auto_tac;
 by (subgoal_tac "m dvd (n*ka)" 1);
 by (subgoal_tac "m dvd ka" 1);
 by (case_tac "#0<=ka" 2);
 by (stac (zdvd_zminus_iff RS sym) 3);
+by (res_inst_tac [("n","n")] zrelprime_zdvd_zmult 3);
+by (asm_simp_tac (simpset() addsimps [zgcd_commute]) 3);
+by (asm_full_simp_tac (simpset() addsimps [zmult_commute,zdvd_zminus_iff]) 3);
 by (res_inst_tac [("n","n")] zrelprime_zdvd_zmult 2);
 by (asm_simp_tac (simpset() addsimps [zgcd_commute]) 2);
 by (asm_full_simp_tac (simpset() addsimps [zmult_commute]) 2);
-by (res_inst_tac [("n","n")] zrelprime_zdvd_zmult 2);
-by (asm_simp_tac (simpset() addsimps [zgcd_commute]) 2);
-by (asm_full_simp_tac (simpset() addsimps [zmult_commute,zdvd_zminus_iff]) 2);
-by (rewtac dvd_def);
-by Safe_tac;
-by (res_inst_tac [("x","kc")] exI 1);
-by (res_inst_tac [("x","k")] exI 2);
-by (simp_tac (simpset() addsimps zmult_ac) 1);
-by Auto_tac;
+by (auto_tac (claset(), simpset() addsimps [dvd_def]));  
+by (blast_tac (claset() addIs [sym]) 1); 
 qed "zcong_zgcd_zmult_zmod";
 
 Goalw [zcong_def,dvd_def]