src/HOL/Univ.ML

 
 
 (*** Introduction rules for Node ***)
 
 goalw Univ.thy [Node_def] "(%k. 0,a) : Node";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Node_K0_I";
 
 goalw Univ.thy [Node_def,Push_def]
     "!!p. p: Node ==> apfst (Push i) p : Node";
-by (fast_tac (!claset addSIs [apfst_conv, nat_case_Suc RS trans]) 1);
+by (blast_tac (!claset addSIs [apfst_conv, nat_case_Suc RS trans]) 1);
 qed "Node_Push_I";
 
 
 (*** Distinctness of constructors ***)
 

 (*** Injectiveness ***)
 
 (** Atomic nodes **)
 
 goalw Univ.thy [Atom_def, inj_def] "inj(Atom)";
-by (fast_tac (!claset addSIs [Node_K0_I] addSDs [Abs_Node_inject]) 1);
+by (blast_tac (!claset addSIs [Node_K0_I] addSDs [Abs_Node_inject]) 1);
 qed "inj_Atom";
 val Atom_inject = inj_Atom RS injD;
 
 goal Univ.thy "(Atom(a)=Atom(b)) = (a=b)";
-by (fast_tac (!claset addSEs [Atom_inject]) 1);
+by (blast_tac (!claset addSDs [Atom_inject]) 1);
 qed "Atom_Atom_eq";
 AddIffs [Atom_Atom_eq];
 
 goalw Univ.thy [Leaf_def,o_def] "inj(Leaf)";
 by (rtac injI 1);

 qed "Push_Node_inject";
 
 
 (** Injectiveness of Scons **)
 
-val [major] = goalw Univ.thy [Scons_def] "M$N <= M'$N' ==> M<=M'";
-by (cut_facts_tac [major] 1);
-by (fast_tac (!claset addSEs [Push_Node_inject]) 1);
+goalw Univ.thy [Scons_def] "!!M. M$N <= M'$N' ==> M<=M'";
+by (blast_tac (!claset addSDs [Push_Node_inject]) 1);
 qed "Scons_inject_lemma1";
 
-val [major] = goalw Univ.thy [Scons_def] "M$N <= M'$N' ==> N<=N'";
-by (cut_facts_tac [major] 1);
-by (fast_tac (!claset addSEs [Push_Node_inject]) 1);
+goalw Univ.thy [Scons_def] "!!M. M$N <= M'$N' ==> N<=N'";
+by (fast_tac (!claset addSDs [Push_Node_inject]) 1);
 qed "Scons_inject_lemma2";
 
 val [major] = goal Univ.thy "M$N = M'$N' ==> M=M'";
 by (rtac (major RS equalityE) 1);
 by (REPEAT (ares_tac [equalityI, Scons_inject_lemma1] 1));

 qed "Scons_inject";
 
 AddSDs [Scons_inject];
 
 goal Univ.thy "(M$N = M'$N') = (M=M' & N=N')";
-by (fast_tac (!claset addSEs [Scons_inject]) 1);
+by (blast_tac (!claset addSEs [Scons_inject]) 1);
 qed "Scons_Scons_eq";
 
 (*** Distinctness involving Leaf and Numb ***)
 
 (** Scons vs Leaf **)

 
 
 (*** ntrunc applied to the various node sets ***)
 
 goalw Univ.thy [ntrunc_def] "ntrunc 0 M = {}";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "ntrunc_0";
 
 goalw Univ.thy [Atom_def,ntrunc_def] "ntrunc (Suc k) (Atom a) = Atom(a)";
 by (fast_tac (!claset addss (!simpset addsimps [ndepth_K0])) 1);
 qed "ntrunc_Atom";

 by (rtac ntrunc_Atom 1);
 qed "ntrunc_Numb";
 
 goalw Univ.thy [Scons_def,ntrunc_def]
     "ntrunc (Suc k) (M$N) = ntrunc k M $ ntrunc k N";
-by (safe_tac ((claset_of "Fun") addSIs [equalityI,imageI]));
+by (safe_tac (!claset addSIs [equalityI, imageI]));
 by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3));
 by (REPEAT (rtac Suc_less_SucD 1 THEN 
             rtac (ndepth_Push_Node RS subst) 1 THEN 
             assume_tac 1));
 qed "ntrunc_Scons";

 (** Injection nodes **)
 
 goalw Univ.thy [In0_def] "ntrunc (Suc 0) (In0 M) = {}";
 by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_0]) 1);
 by (rewtac Scons_def);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "ntrunc_one_In0";
 
 goalw Univ.thy [In0_def]
     "ntrunc (Suc (Suc k)) (In0 M) = In0 (ntrunc (Suc k) M)";
 by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_Numb]) 1);
 qed "ntrunc_In0";
 
 goalw Univ.thy [In1_def] "ntrunc (Suc 0) (In1 M) = {}";
 by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_0]) 1);
 by (rewtac Scons_def);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "ntrunc_one_In1";
 
 goalw Univ.thy [In1_def]
     "ntrunc (Suc (Suc k)) (In1 M) = In1 (ntrunc (Suc k) M)";
 by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_Numb]) 1);

 
 
 (*** Disjoint Sum ***)
 
 goalw Univ.thy [usum_def] "!!M. M:A ==> In0(M) : A<+>B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "usum_In0I";
 
 goalw Univ.thy [usum_def] "!!N. N:B ==> In1(N) : A<+>B";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "usum_In1I";
 
 val major::prems = goalw Univ.thy [usum_def]
     "[| u : A<+>B;  \
 \       !!x. [| x:A;  u=In0(x) |] ==> P; \

 AddSDs [In0_inject, In1_inject];
 
 (*** proving equality of sets and functions using ntrunc ***)
 
 goalw Univ.thy [ntrunc_def] "ntrunc k M <= M";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "ntrunc_subsetI";
 
 val [major] = goalw Univ.thy [ntrunc_def]
     "(!!k. ntrunc k M <= N) ==> M<=N";
-by (fast_tac (!claset addIs [less_add_Suc1, less_add_Suc2, 
+by (blast_tac (!claset addIs [less_add_Suc1, less_add_Suc2, 
                             major RS subsetD]) 1);
 qed "ntrunc_subsetD";
 
 (*A generalized form of the take-lemma*)
 val [major] = goal Univ.thy "(!!k. ntrunc k M = ntrunc k N) ==> M=N";

 qed "ntrunc_o_equality";
 
 (*** Monotonicity ***)
 
 goalw Univ.thy [uprod_def] "!!A B. [| A<=A';  B<=B' |] ==> A<*>B <= A'<*>B'";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "uprod_mono";
 
 goalw Univ.thy [usum_def] "!!A B. [| A<=A';  B<=B' |] ==> A<+>B <= A'<+>B'";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "usum_mono";
 
 goalw Univ.thy [Scons_def] "!!M N. [| M<=M';  N<=N' |] ==> M$N <= M'$N'";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Scons_mono";
 
 goalw Univ.thy [In0_def] "!!M N. M<=N ==> In0(M) <= In0(N)";
 by (REPEAT (ares_tac [subset_refl,Scons_mono] 1));
 qed "In0_mono";

 
 
 (*** Split and Case ***)
 
 goalw Univ.thy [Split_def] "Split c (M$N) = c M N";
-by (fast_tac (!claset addIs [select_equality]) 1);
+by (blast_tac (!claset addIs [select_equality]) 1);
 qed "Split";
 
 goalw Univ.thy [Case_def] "Case c d (In0 M) = c(M)";
-by (fast_tac (!claset addIs [select_equality]) 1);
+by (blast_tac (!claset addIs [select_equality]) 1);
 qed "Case_In0";
 
 goalw Univ.thy [Case_def] "Case c d (In1 N) = d(N)";
-by (fast_tac (!claset addIs [select_equality]) 1);
+by (blast_tac (!claset addIs [select_equality]) 1);
 qed "Case_In1";
 
 (**** UN x. B(x) rules ****)
 
 goalw Univ.thy [ntrunc_def] "ntrunc k (UN x.f(x)) = (UN x. ntrunc k (f x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "ntrunc_UN1";
 
 goalw Univ.thy [Scons_def] "(UN x.f(x)) $ M = (UN x. f(x) $ M)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Scons_UN1_x";
 
 goalw Univ.thy [Scons_def] "M $ (UN x.f(x)) = (UN x. M $ f(x))";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "Scons_UN1_y";
 
 goalw Univ.thy [In0_def] "In0(UN x.f(x)) = (UN x. In0(f(x)))";
 by (rtac Scons_UN1_y 1);
 qed "In0_UN1";

 
 
 (*** Equality : the diagonal relation ***)
 
 goalw Univ.thy [diag_def] "!!a A. [| a=b;  a:A |] ==> (a,b) : diag(A)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "diag_eqI";
 
 val diagI = refl RS diag_eqI |> standard;
 
 (*The general elimination rule*)

 
 (*** Equality for Cartesian Product ***)
 
 goalw Univ.thy [dprod_def]
     "!!r s. [| (M,M'):r;  (N,N'):s |] ==> (M$N, M'$N') : r<**>s";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "dprodI";
 
 (*The general elimination rule*)
 val major::prems = goalw Univ.thy [dprod_def]
     "[| c : r<**>s;  \

 
 
 (*** Equality for Disjoint Sum ***)
 
 goalw Univ.thy [dsum_def]  "!!r. (M,M'):r ==> (In0(M), In0(M')) : r<++>s";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "dsum_In0I";
 
 goalw Univ.thy [dsum_def]  "!!r. (N,N'):s ==> (In1(N), In1(N')) : r<++>s";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "dsum_In1I";
 
 val major::prems = goalw Univ.thy [dsum_def]
     "[| w : r<++>s;  \
 \       !!x x'. [| (x,x') : r;  w = (In0(x), In0(x')) |] ==> P; \

 AddSEs [diagE, uprodE, dprodE, usumE, dsumE];
 
 (*** Monotonicity ***)
 
 goal Univ.thy "!!r s. [| r<=r';  s<=s' |] ==> r<**>s <= r'<**>s'";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "dprod_mono";
 
 goal Univ.thy "!!r s. [| r<=r';  s<=s' |] ==> r<++>s <= r'<++>s'";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "dsum_mono";
 
 
 (*** Bounding theorems ***)
 
 goal Univ.thy "diag(A) <= A Times A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "diag_subset_Sigma";
 
 goal Univ.thy "((A Times B) <**> (C Times D)) <= (A<*>C) Times (B<*>D)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "dprod_Sigma";
 
 val dprod_subset_Sigma = [dprod_mono, dprod_Sigma] MRS subset_trans |>standard;
 
 (*Dependent version*)
 goal Univ.thy
     "(Sigma A B <**> Sigma C D) <= Sigma (A<*>C) (Split(%x y. B(x)<*>D(y)))";
 by (safe_tac (!claset));
 by (stac Split 1);
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "dprod_subset_Sigma2";
 
 goal Univ.thy "(A Times B <++> C Times D) <= (A<+>C) Times (B<+>D)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "dsum_Sigma";
 
 val dsum_subset_Sigma = [dsum_mono, dsum_Sigma] MRS subset_trans |> standard;
 
 
 (*** Domain ***)
 
 goal Univ.thy "fst `` diag(A) = A";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "fst_image_diag";
 
 goal Univ.thy "fst `` (r<**>s) = (fst``r) <*> (fst``s)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "fst_image_dprod";
 
 goal Univ.thy "fst `` (r<++>s) = (fst``r) <+> (fst``s)";
-by (Fast_tac 1);
+by (Blast_tac 1);
 qed "fst_image_dsum";
 
 Addsimps [fst_image_diag, fst_image_dprod, fst_image_dsum];