# HG changeset patch
# User paulson
# Date 875262074 -7200
# Node ID d78cf498a88c06787349ac2b61e86db4e53dc41d
# Parent  e285533153553a7a2bd0520d34764ffae6879e92
Minor tidying to use Clarify_tac, etc.

diff -r e28553315355 -r d78cf498a88c src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Fri Sep 26 10:12:04 1997 +0200
+++ b/src/HOL/Arith.ML	Fri Sep 26 10:21:14 1997 +0200
@@ -432,7 +432,7 @@
 
 goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";
 by (res_inst_tac [("m","k"),("n","i")] diff_induct 1);
-by (ALLGOALS (strip_tac THEN' Simp_tac THEN' TRY o Blast_tac));
+by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac));
 qed "zero_induct_lemma";
 
 val prems = goal Arith.thy "[| P(k);  !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
diff -r e28553315355 -r d78cf498a88c src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Fri Sep 26 10:12:04 1997 +0200
+++ b/src/HOL/Divides.ML	Fri Sep 26 10:21:14 1997 +0200
@@ -121,7 +121,7 @@
 (* Monotonicity of div in first argument *)
 goal thy "!!n. 0<k ==> ALL m. m <= n --> (m div k) <= (n div k)";
 by (res_inst_tac [("n","n")] less_induct 1);
-by (strip_tac 1);
+by (Clarify_tac 1);
 by (case_tac "na<k" 1);
 (* 1  case n<k *)
 by (subgoal_tac "m<k" 1);
@@ -347,7 +347,7 @@
 AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2];
 
 goalw thy [dvd_def] "!!m. [| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)";
-by (Step_tac 1);
+by (Clarify_tac 1);
 by (full_simp_tac (!simpset addsimps [zero_less_mult_iff]) 1);
 by (res_inst_tac 
     [("x", "(((k div ka)*ka + k mod ka) - ((f*k) div (f*ka)) * ka)")] 
@@ -369,7 +369,7 @@
 qed "dvd_mult_cancel";
 
 goalw thy [dvd_def] "!!i j. [| i dvd m; j dvd n|] ==> (i*j) dvd (m*n)";
-by (Step_tac 1);
+by (Clarify_tac 1);
 by (res_inst_tac [("x","k*ka")] exI 1);
 by (asm_simp_tac (!simpset addsimps mult_ac) 1);
 qed "mult_dvd_mono";
@@ -380,7 +380,7 @@
 qed "dvd_mult_left";
 
 goalw thy [dvd_def] "!!n. [| k dvd n; 0 < n |] ==> k <= n";
-by (Step_tac 1);
+by (Clarify_tac 1);
 by (ALLGOALS (full_simp_tac (!simpset addsimps [zero_less_mult_iff])));
 by (etac conjE 1);
 by (rtac le_trans 1);
diff -r e28553315355 -r d78cf498a88c src/HOL/Induct/Exp.ML
--- a/src/HOL/Induct/Exp.ML	Fri Sep 26 10:12:04 1997 +0200
+++ b/src/HOL/Induct/Exp.ML	Fri Sep 26 10:21:14 1997 +0200
@@ -80,7 +80,7 @@
 by (Blast_tac 1);
 by (blast_tac (!claset addEs [exec_WHILE_case]) 1);
 by (thin_tac "(?c,s2) -[?ev]-> s3" 1);
-by (Step_tac 1);
+by (Clarify_tac 1);
 by (etac exec_WHILE_case 1);
 by (ALLGOALS Fast_tac);         (*Blast_tac: proof fails*)
 qed "com_Unique";
@@ -197,10 +197,8 @@
 qed "valof_valof";
 
 
-
 (** Equivalence of  VALOF SKIP RESULTIS e  and  e **)
 
-
 goal thy "!!x. (e',s) -|-> (v,s') ==> \
 \              (e' = VALOF SKIP RESULTIS e) --> \
 \              (e, s) -|-> (v,s')";
@@ -218,7 +216,6 @@
 qed "valof_skip";
 
 
-
 (** Equivalence of  VALOF x:=e RESULTIS x  and  e **)
 
 goal thy "!!x. (e',s) -|-> (v,s'') ==> \
@@ -227,7 +224,7 @@
 by (etac eval_induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (thin_tac "?PP-->?QQ" 1);
-by (Step_tac 1);
+by (Clarify_tac 1);
 by (Simp_tac 1);
 by (Blast_tac 1); 
 bind_thm ("valof_assign1", refl RSN (2, result() RS mp));
diff -r e28553315355 -r d78cf498a88c src/HOL/Induct/LFilter.ML
--- a/src/HOL/Induct/LFilter.ML	Fri Sep 26 10:12:04 1997 +0200
+++ b/src/HOL/Induct/LFilter.ML	Fri Sep 26 10:21:14 1997 +0200
@@ -59,7 +59,7 @@
 
 val prems = goal thy
     "[| !!x. p x ==> q x |] ==> Domain (findRel p) <= Domain (findRel q)";
-by (Step_tac 1);
+by (Clarify_tac 1);
 by (etac findRel.induct 1);
 by (blast_tac (!claset addIs (findRel.intrs@prems)) 1);
 by (blast_tac (!claset addIs findRel.intrs) 1);
@@ -89,7 +89,7 @@
 goal thy "!!p. ~ (p x) ==> find p (LCons x l) = find p l";
 by (case_tac "LCons x l : Domain(findRel p)" 1);
 by (Asm_full_simp_tac 2);
-by (Step_tac 1);
+by (Clarify_tac 1);
 by (asm_simp_tac (!simpset addsimps [findRel_imp_find]) 1);
 by (blast_tac (!claset addIs (findRel_imp_find::findRel.intrs)) 1);
 qed "find_LCons_seek";
@@ -335,7 +335,7 @@
 by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
 by (etac Domain_findRelE 1);
 by (forward_tac [lmap_LCons_findRel] 1);
-by (Step_tac 1);
+by (Clarify_tac 1);
 by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
 by (Blast_tac 1);
 qed "lfilter_lmap";
diff -r e28553315355 -r d78cf498a88c src/HOL/Induct/Mutil.ML
--- a/src/HOL/Induct/Mutil.ML	Fri Sep 26 10:12:04 1997 +0200
+++ b/src/HOL/Induct/Mutil.ML	Fri Sep 26 10:21:14 1997 +0200
@@ -94,7 +94,8 @@
 goalw thy [evnodd_def]
     "evnodd (insert (i,j) C) b = \
 \      (if (i+j) mod 2 = b then insert (i,j) (evnodd C b) else evnodd C b)";
-by (simp_tac (!simpset setloop (split_tac [expand_if] THEN' Step_tac)) 1);
+by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (Blast_tac 1);
 qed "evnodd_insert";
 
 Addsimps [finite_evnodd, evnodd_Un, evnodd_Diff, evnodd_empty, evnodd_insert];
@@ -133,7 +134,7 @@
 by (Simp_tac 2 THEN assume_tac 1);
 by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1);
 by (Simp_tac 2 THEN assume_tac 1);
-by (Step_tac 1);
+by (Clarify_tac 1);
 by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd ta b" 1);
 by (asm_simp_tac (!simpset addsimps [tiling_domino_finite]) 1);
 by (blast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1);
diff -r e28553315355 -r d78cf498a88c src/HOL/Integ/Equiv.ML
--- a/src/HOL/Integ/Equiv.ML	Fri Sep 26 10:12:04 1997 +0200
+++ b/src/HOL/Integ/Equiv.ML	Fri Sep 26 10:21:14 1997 +0200
@@ -18,19 +18,19 @@
 
 goalw Equiv.thy [trans_def,sym_def,inverse_def]
     "!!r. [| sym(r); trans(r) |] ==> r^-1 O r <= r";
-by (fast_tac (!claset addSEs [inverseD]) 1);
+by (blast_tac (!claset addSEs [inverseD]) 1);
 qed "sym_trans_comp_subset";
 
 goalw Equiv.thy [refl_def]
     "!!A r. refl A r ==> r <= r^-1 O r";
-by (fast_tac (!claset addIs [compI]) 1);
+by (Blast_tac 1);
 qed "refl_comp_subset";
 
 goalw Equiv.thy [equiv_def]
     "!!A r. equiv A r ==> r^-1 O r = r";
+by (Clarify_tac 1);
 by (rtac equalityI 1);
-by (REPEAT (ares_tac [sym_trans_comp_subset, refl_comp_subset] 1
-     ORELSE etac conjE 1));
+by (REPEAT (ares_tac [sym_trans_comp_subset, refl_comp_subset] 1));
 qed "equiv_comp_eq";
 
 (*second half*)
@@ -38,9 +38,7 @@
     "!!A r. [| r^-1 O r = r;  Domain(r) = A |] ==> equiv A r";
 by (etac equalityE 1);
 by (subgoal_tac "ALL x y. (x,y) : r --> (y,x) : r" 1);
-by (Step_tac 1);
-by (fast_tac (!claset addIs [compI]) 3);
-by (ALLGOALS (fast_tac (!claset addIs [compI])));
+by (ALLGOALS Fast_tac);
 qed "comp_equivI";
 
 (** Equivalence classes **)
@@ -48,27 +46,24 @@
 (*Lemma for the next result*)
 goalw Equiv.thy [equiv_def,trans_def,sym_def]
     "!!A r. [| equiv A r;  (a,b): r |] ==> r^^{a} <= r^^{b}";
-by (Step_tac 1);
-by (rtac ImageI 1);
-by (Fast_tac 2);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "equiv_class_subset";
 
 goal Equiv.thy "!!A r. [| equiv A r;  (a,b): r |] ==> r^^{a} = r^^{b}";
 by (REPEAT (ares_tac [equalityI, equiv_class_subset] 1));
 by (rewrite_goals_tac [equiv_def,sym_def]);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "equiv_class_eq";
 
 goalw Equiv.thy [equiv_def,refl_def]
     "!!A r. [| equiv A r;  a: A |] ==> a: r^^{a}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "equiv_class_self";
 
 (*Lemma for the next result*)
 goalw Equiv.thy [equiv_def,refl_def]
     "!!A r. [| equiv A r;  r^^{b} <= r^^{a};  b: A |] ==> (a,b): r";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "subset_equiv_class";
 
 goal Equiv.thy
@@ -79,7 +74,7 @@
 (*thus r^^{a} = r^^{b} as well*)
 goalw Equiv.thy [equiv_def,trans_def,sym_def]
     "!!A r. [| equiv A r;  x: (r^^{a} Int r^^{b}) |] ==> (a,b): r";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "equiv_class_nondisjoint";
 
 val [major] = goalw Equiv.thy [equiv_def,refl_def]
@@ -89,23 +84,14 @@
 
 goal Equiv.thy
     "!!A r. equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)";
-by (Step_tac 1);
-by ((rtac equiv_class_eq 1) THEN (assume_tac 1) THEN (assume_tac 1));
-by ((rtac eq_equiv_class 3) THEN 
-    (assume_tac 4) THEN (assume_tac 4) THEN (assume_tac 3));
-by ((dtac equiv_type 1) THEN (dtac rev_subsetD 1) THEN
-    (assume_tac 1) THEN (dtac SigmaD1 1) THEN (assume_tac 1));
-by ((dtac equiv_type 1) THEN (dtac rev_subsetD 1) THEN
-    (assume_tac 1) THEN (dtac SigmaD2 1) THEN (assume_tac 1));
+by (blast_tac (!claset addSIs [equiv_class_eq]
+	               addDs [eq_equiv_class, equiv_type]) 1);
 qed "equiv_class_eq_iff";
 
 goal Equiv.thy
     "!!A r. [| equiv A r;  x: A;  y: A |] ==> (r^^{x} = r^^{y}) = ((x,y): r)";
-by (Step_tac 1);
-by ((rtac eq_equiv_class 1) THEN 
-    (assume_tac 1) THEN (assume_tac 1) THEN (assume_tac 1));
-by ((rtac equiv_class_eq 1) THEN 
-    (assume_tac 1) THEN (assume_tac 1));
+by (blast_tac (!claset addSIs [equiv_class_eq]
+	               addDs [eq_equiv_class, equiv_type]) 1);
 qed "eq_equiv_class_iff";
 
 (*** Quotients ***)
@@ -113,7 +99,7 @@
 (** Introduction/elimination rules -- needed? **)
 
 goalw Equiv.thy [quotient_def] "!!A. x:A ==> r^^{x}: A/r";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "quotientI";
 
 val [major,minor] = goalw Equiv.thy [quotient_def]
@@ -122,7 +108,7 @@
 by (resolve_tac [major RS UN_E] 1);
 by (rtac minor 1);
 by (assume_tac 2);
-by (Fast_tac 1);
+by (Fast_tac 1);   (*Blast_tac FAILS to prove it*)
 qed "quotientE";
 
 goalw Equiv.thy [equiv_def,refl_def,quotient_def]
@@ -157,7 +143,7 @@
 \                      ==> (UN x:r^^{a}. b(x)) = b(a)";
 by (rtac (equiv_class_self RS UN_singleton) 1 THEN REPEAT (assume_tac 1));
 by (rewrite_goals_tac [equiv_def,congruent_def,sym_def]);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "UN_equiv_class";
 
 (*type checking of  UN x:r``{a}. b(x) *)
@@ -166,7 +152,7 @@
 \       !!x.  x : A ==> b(x) : B |]             \
 \    ==> (UN x:X. b(x)) : B";
 by (cut_facts_tac prems 1);
-by (Step_tac 1);
+by (Clarify_tac 1);
 by (stac UN_equiv_class 1);
 by (REPEAT (ares_tac prems 1));
 qed "UN_equiv_class_type";
@@ -180,7 +166,7 @@
 \       !!x y. [| x:A; y:A; b(x)=b(y) |] ==> (x,y):r |]         \
 \    ==> X=Y";
 by (cut_facts_tac prems 1);
-by (Step_tac 1);
+by (Clarify_tac 1);
 by (rtac equiv_class_eq 1);
 by (REPEAT (ares_tac prems 1));
 by (etac box_equals 1);
@@ -193,18 +179,18 @@
 
 goalw Equiv.thy [congruent_def,congruent2_def,equiv_def,refl_def]
     "!!A r. [| equiv A r;  congruent2 r b;  a: A |] ==> congruent r (b a)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "congruent2_implies_congruent";
 
 goalw Equiv.thy [congruent_def]
     "!!A r. [| equiv A r;  congruent2 r b;  a: A |] ==> \
 \    congruent r (%x1. UN x2:r^^{a}. b x1 x2)";
-by (Step_tac 1);
+by (Clarify_tac 1);
 by (rtac (equiv_type RS subsetD RS SigmaE2) 1 THEN REPEAT (assume_tac 1));
 by (asm_simp_tac (!simpset addsimps [UN_equiv_class,
                                      congruent2_implies_congruent]) 1);
 by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "congruent2_implies_congruent_UN";
 
 goal Equiv.thy
@@ -222,7 +208,7 @@
 \       !!x1 x2.  [| x1: A; x2: A |] ==> b x1 x2 : B |]    \
 \    ==> (UN x1:X1. UN x2:X2. b x1 x2) : B";
 by (cut_facts_tac prems 1);
-by (Step_tac 1);
+by (Clarify_tac 1);
 by (REPEAT (ares_tac (prems@[UN_equiv_class_type,
                              congruent2_implies_congruent_UN,
                              congruent2_implies_congruent, quotientI]) 1));
@@ -237,10 +223,8 @@
 \       !! y z w. [| w: A;  (y,z) : r |] ==> b w y = b w z       \
 \    |] ==> congruent2 r b";
 by (cut_facts_tac prems 1);
-by (Step_tac 1);
-by (rtac trans 1);
-by (REPEAT (ares_tac prems 1
-     ORELSE etac (subsetD RS SigmaE2) 1 THEN assume_tac 2 THEN assume_tac 1));
+by (Clarify_tac 1);
+by (blast_tac (!claset addIs (trans::prems)) 1);
 qed "congruent2I";
 
 val [equivA,commute,congt] = goal Equiv.thy
diff -r e28553315355 -r d78cf498a88c src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Fri Sep 26 10:12:04 1997 +0200
+++ b/src/HOL/NatDef.ML	Fri Sep 26 10:21:14 1997 +0200
@@ -152,7 +152,7 @@
 qed "nat_case_Suc";
 
 goalw thy [wf_def, pred_nat_def] "wf(pred_nat)";
-by (strip_tac 1);
+by (Clarify_tac 1);
 by (nat_ind_tac "x" 1);
 by (ALLGOALS Blast_tac);
 qed "wf_pred_nat";
diff -r e28553315355 -r d78cf498a88c src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Fri Sep 26 10:12:04 1997 +0200
+++ b/src/HOL/Relation.ML	Fri Sep 26 10:21:14 1997 +0200
@@ -164,7 +164,7 @@
     "[| b: r^^A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P"
  (fn major::prems=>
   [ (rtac (major RS CollectE) 1),
-    (Step_tac 1),
+    (Clarify_tac 1),
     (rtac (hd prems) 1),
     (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);
 
diff -r e28553315355 -r d78cf498a88c src/HOL/Set.ML
--- a/src/HOL/Set.ML	Fri Sep 26 10:12:04 1997 +0200
+++ b/src/HOL/Set.ML	Fri Sep 26 10:21:14 1997 +0200
@@ -412,8 +412,8 @@
 
 (*Redundant? But unlike insertCI, it proves the subgoal immediately!*)
 AddSIs [singletonI];   
-    
 AddSDs [singleton_inject];
+AddSEs [singletonE];
 
 goal Set.thy "{x.x=a} = {a}";
 by(Blast_tac 1);
diff -r e28553315355 -r d78cf498a88c src/HOL/WF_Rel.ML
--- a/src/HOL/WF_Rel.ML	Fri Sep 26 10:12:04 1997 +0200
+++ b/src/HOL/WF_Rel.ML	Fri Sep 26 10:21:14 1997 +0200
@@ -34,7 +34,7 @@
 
 goal thy "!!r. wf(r) ==> wf(inv_image r (f::'a=>'b))"; 
 by (full_simp_tac (!simpset addsimps [inv_image_def, wf_eq_minimal]) 1);
-by (Step_tac 1);
+by (Clarify_tac 1);
 by (subgoal_tac "? (w::'b). w : {w. ? (x::'a). x: Q & (f x = w)}" 1);
 by (blast_tac (!claset delrules [allE]) 2);
 by (etac allE 1);
@@ -130,7 +130,7 @@
  by (Blast_tac 1);
 by (etac swap 1);
 by (Asm_full_simp_tac 1);
-by (Step_tac 1);
+by (Clarify_tac 1);
 by (subgoal_tac "!n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
  by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1);
  by (rtac allI 1);
diff -r e28553315355 -r d78cf498a88c src/HOL/ex/Primes.ML
--- a/src/HOL/ex/Primes.ML	Fri Sep 26 10:12:04 1997 +0200
+++ b/src/HOL/ex/Primes.ML	Fri Sep 26 10:21:14 1997 +0200
@@ -90,7 +90,7 @@
 (*This theorem leads immediately to a proof of the uniqueness of factorization.
   If p divides a product of primes then it is one of those primes.*)
 goalw thy [prime_def] "!!p. [| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n";
-by (Step_tac 1);
+by (Clarify_tac 1);
 by (subgoal_tac "m = gcd(m*p, m*n)" 1);
 by (etac ssubst 1);
 by (rtac gcd_greatest 1);