--- a/src/HOL/ex/Simult.ML Fri Apr 11 11:33:51 1997 +0200
+++ b/src/HOL/ex/Simult.ML Fri Apr 11 15:21:36 1997 +0200
@@ -29,7 +29,7 @@
goalw Simult.thy [TF_def] "TF(sexp) <= sexp";
by (rtac lfp_lowerbound 1);
-by (fast_tac (!claset addIs sexp.intrs@[sexp_In0I, sexp_In1I]
+by (blast_tac (!claset addIs sexp.intrs@[sexp_In0I, sexp_In1I]
addSEs [PartE]) 1);
qed "TF_sexp";
@@ -50,7 +50,7 @@
\ |] ==> R(FCONS M N) \
\ |] ==> R(i)";
by (rtac ([TF_def, TF_fun_mono, major] MRS def_induct) 1);
-by (fast_tac (!claset addIs (prems@[PartI])
+by (blast_tac (!claset addIs (prems@[PartI])
addEs [usumE, uprodE, PartE]) 1);
qed "TF_induct";
@@ -59,13 +59,9 @@
"!!A. ! M: TF(A). (M: Part (TF A) In0 --> P(M)) & \
\ (M: Part (TF A) In1 --> Q(M)) \
\ ==> (! M: Part (TF A) In0. P(M)) & (! M: Part (TF A) In1. Q(M))";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "TF_induct_lemma";
-AddSIs [PartI];
-AddSDs [In0_inject, In1_inject];
-AddSEs [PartE];
-
(*Could prove ~ TCONS M N : Part (TF A) In1 etc. *)
(*Induction on TF with separate predicates P, Q*)
@@ -93,12 +89,12 @@
(Tree_Forest_induct RS conjE) 1);
(*Instantiates ?A1 to range(Leaf). *)
by (fast_tac (!claset addSEs [Rep_Tree_inverse RS subst,
- Rep_Forest_inverse RS subst]
- addSIs [Rep_Tree,Rep_Forest]) 4);
+ Rep_Forest_inverse RS subst]
+ addSIs [Rep_Tree,Rep_Forest]) 4);
(*Cannot use simplifier: the rewrites work in the wrong direction!*)
by (ALLGOALS (fast_tac (!claset addSEs [Abs_Tree_inverse RS subst,
- Abs_Forest_inverse RS subst]
- addSIs prems)));
+ Abs_Forest_inverse RS subst]
+ addSIs prems)));
qed "tree_forest_induct";
@@ -135,38 +131,38 @@
AddIs [TF_I, uprodI, usum_In0I, usum_In1I];
AddSEs [Scons_inject];
-val prems = goalw Simult.thy TF_Rep_defs
- "[| a: A; M: Part (TF A) In1 |] ==> TCONS a M : Part (TF A) In0";
-by (fast_tac (!claset addIs prems) 1);
+goalw Simult.thy TF_Rep_defs
+ "!!A. [| a: A; M: Part (TF A) In1 |] ==> TCONS a M : Part (TF A) In0";
+by (Blast_tac 1);
qed "TCONS_I";
(* FNIL is a TF(A) -- this also justifies the type definition*)
goalw Simult.thy TF_Rep_defs "FNIL: Part (TF A) In1";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "FNIL_I";
-val prems = goalw Simult.thy TF_Rep_defs
- "[| M: Part (TF A) In0; N: Part (TF A) In1 |] ==> \
-\ FCONS M N : Part (TF A) In1";
-by (fast_tac (!claset addIs prems) 1);
+goalw Simult.thy TF_Rep_defs
+ "!!A. [| M: Part (TF A) In0; N: Part (TF A) In1 |] ==> \
+\ FCONS M N : Part (TF A) In1";
+by (Blast_tac 1);
qed "FCONS_I";
(** Injectiveness of TCONS and FCONS **)
goalw Simult.thy TF_Rep_defs "(TCONS K M=TCONS L N) = (K=L & M=N)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "TCONS_TCONS_eq";
bind_thm ("TCONS_inject", (TCONS_TCONS_eq RS iffD1 RS conjE));
goalw Simult.thy TF_Rep_defs "(FCONS K M=FCONS L N) = (K=L & M=N)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "FCONS_FCONS_eq";
bind_thm ("FCONS_inject", (FCONS_FCONS_eq RS iffD1 RS conjE));
(** Distinctness of TCONS, FNIL and FCONS **)
goalw Simult.thy TF_Rep_defs "TCONS M N ~= FNIL";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "TCONS_not_FNIL";
bind_thm ("FNIL_not_TCONS", (TCONS_not_FNIL RS not_sym));
@@ -174,7 +170,7 @@
val FNIL_neq_TCONS = sym RS TCONS_neq_FNIL;
goalw Simult.thy TF_Rep_defs "FCONS M N ~= FNIL";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "FCONS_not_FNIL";
bind_thm ("FNIL_not_FCONS", (FCONS_not_FNIL RS not_sym));
@@ -182,7 +178,7 @@
val FNIL_neq_FCONS = sym RS FCONS_neq_FNIL;
goalw Simult.thy TF_Rep_defs "TCONS M N ~= FCONS K L";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "TCONS_not_FCONS";
bind_thm ("FCONS_not_TCONS", (TCONS_not_FCONS RS not_sym));
@@ -206,12 +202,12 @@
Leaf_inject];
goalw Simult.thy [Tcons_def] "(Tcons x xs=Tcons y ys) = (x=y & xs=ys)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Tcons_Tcons_eq";
bind_thm ("Tcons_inject", (Tcons_Tcons_eq RS iffD1 RS conjE));
goalw Simult.thy [Fcons_def,Fnil_def] "Fcons x xs ~= Fnil";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Fcons_not_Fnil";
bind_thm ("Fcons_neq_Fnil", Fcons_not_Fnil RS notE);
@@ -221,7 +217,7 @@
(** Injectiveness of Fcons **)
goalw Simult.thy [Fcons_def] "(Fcons x xs=Fcons y ys) = (x=y & xs=ys)";
-by (Fast_tac 1);
+by (Blast_tac 1);
qed "Fcons_Fcons_eq";
bind_thm ("Fcons_inject", Fcons_Fcons_eq RS iffD1 RS conjE);