Minor tidying to use Clarify_tac, etc.
--- 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)";
--- 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);
--- 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));
--- 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";
--- 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);
--- 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
--- 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";
--- 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)) ]);
--- 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);
--- 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);
--- 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);