src/HOL/Univ.ML

 
 
 (*** Introduction rules for Node ***)
 
 goalw Univ.thy [Node_def] "(%k. 0,a) : Node";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "Node_K0_I";
 
 goalw Univ.thy [Node_def,Push_def]
     "!!p. p: Node ==> apfst (Push i) p : Node";
-by (fast_tac (set_cs addSIs [apfst_conv, nat_case_Suc RS trans]) 1);
+by (fast_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 (prod_cs addSIs [Node_K0_I] addSDs [Abs_Node_inject]) 1);
+by (fast_tac (!claset addSIs [Node_K0_I] addSDs [Abs_Node_inject]) 1);
 qed "inj_Atom";
 val Atom_inject = inj_Atom RS injD;
 
 goalw Univ.thy [Leaf_def,o_def] "inj(Leaf)";
 by (rtac injI 1);

 
 (** 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 (set_cs addSDs [Suc_inject]
+by (fast_tac (!claset addSDs [Suc_inject]
                      addSEs [Push_Node_inject, Zero_neq_Suc]) 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 (set_cs addSDs [Suc_inject]
+by (fast_tac (!claset addSDs [Suc_inject]
                      addSEs [Push_Node_inject, Suc_neq_Zero]) 1);
 qed "Scons_inject_lemma2";
 
 val [major] = goal Univ.thy "M$N = M'$N' ==> M=M'";
 by (rtac (major RS equalityE) 1);

 by (rtac ((major RS Scons_inject2) RS ((major RS Scons_inject1) RS minor)) 1);
 qed "Scons_inject";
 
 (*rewrite rules*)
 goal Univ.thy "(Atom(a)=Atom(b)) = (a=b)";
-by (fast_tac (HOL_cs addSEs [Atom_inject]) 1);
+by (fast_tac (!claset addSEs [Atom_inject]) 1);
 qed "Atom_Atom_eq";
 
 goal Univ.thy "(M$N = M'$N') = (M=M' & N=N')";
-by (fast_tac (HOL_cs addSEs [Scons_inject]) 1);
+by (fast_tac (!claset addSEs [Scons_inject]) 1);
 qed "Scons_Scons_eq";
 
 (*** Distinctness involving Leaf and Numb ***)
 
 (** Scons vs Leaf **)

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

 
 
 (*** proving equality of sets and functions using ntrunc ***)
 
 goalw Univ.thy [ntrunc_def] "ntrunc k M <= M";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "ntrunc_subsetI";
 
 val [major] = goalw Univ.thy [ntrunc_def]
     "(!!k. ntrunc k M <= N) ==> M<=N";
-by (fast_tac (set_cs addIs [less_add_Suc1, less_add_Suc2, 
+by (fast_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 set_cs 1);
+by (Fast_tac 1);
 qed "uprod_mono";
 
 goalw Univ.thy [usum_def] "!!A B. [| A<=A';  B<=B' |] ==> A<+>B <= A'<+>B'";
-by (fast_tac set_cs 1);
+by (Fast_tac 1);
 qed "usum_mono";
 
 goalw Univ.thy [Scons_def] "!!M N. [| M<=M';  N<=N' |] ==> M$N <= M'$N'";
-by (fast_tac set_cs 1);
+by (Fast_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 (set_cs addIs [select_equality] addEs [Scons_inject]) 1);
+by (fast_tac (!claset addIs [select_equality] addEs [Scons_inject]) 1);
 qed "Split";
 
 goalw Univ.thy [Case_def] "Case c d (In0 M) = c(M)";
-by (fast_tac (set_cs addIs [select_equality] 
+by (fast_tac (!claset addIs [select_equality] 
                      addEs [make_elim In0_inject, In0_neq_In1]) 1);
 qed "Case_In0";
 
 goalw Univ.thy [Case_def] "Case c d (In1 N) = d(N)";
-by (fast_tac (set_cs addIs [select_equality] 
+by (fast_tac (!claset addIs [select_equality] 
                      addEs [make_elim In1_inject, In1_neq_In0]) 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 (set_cs addIs [equalityI]) 1);
+by (fast_tac (!claset addIs [equalityI]) 1);
 qed "ntrunc_UN1";
 
 goalw Univ.thy [Scons_def] "(UN x.f(x)) $ M = (UN x. f(x) $ M)";
-by (fast_tac (set_cs addIs [equalityI]) 1);
+by (fast_tac (!claset addIs [equalityI]) 1);
 qed "Scons_UN1_x";
 
 goalw Univ.thy [Scons_def] "M $ (UN x.f(x)) = (UN x. M $ f(x))";
-by (fast_tac (set_cs addIs [equalityI]) 1);
+by (fast_tac (!claset addIs [equalityI]) 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 set_cs 1);
+by (Fast_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 prod_cs 1);
+by (Fast_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 prod_cs 1);
+by (Fast_tac 1);
 qed "dsum_In0I";
 
 goalw Univ.thy [dsum_def]  "!!r. (N,N'):s ==> (In1(N), In1(N')) : r<++>s";
-by (fast_tac prod_cs 1);
+by (Fast_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; \

 val univ_cs =
     prod_cs addSIs [diagI, uprodI, dprodI]
             addIs  [usum_In0I, usum_In1I, dsum_In0I, dsum_In1I]
             addSEs [diagE, uprodE, dprodE, usumE, dsumE];
 
+AddSIs [diagI, uprodI, dprodI];
+AddIs  [usum_In0I, usum_In1I, dsum_In0I, dsum_In1I];
+AddSEs [diagE, uprodE, dprodE, usumE, dsumE];
 
 (*** Monotonicity ***)
 
 goal Univ.thy "!!r s. [| r<=r';  s<=s' |] ==> r<**>s <= r'<**>s'";
-by (fast_tac univ_cs 1);
+by (Fast_tac 1);
 qed "dprod_mono";
 
 goal Univ.thy "!!r s. [| r<=r';  s<=s' |] ==> r<++>s <= r'<++>s'";
-by (fast_tac univ_cs 1);
+by (Fast_tac 1);
 qed "dsum_mono";
 
 
 (*** Bounding theorems ***)
 
 goal Univ.thy "diag(A) <= A Times A";
-by (fast_tac univ_cs 1);
+by (Fast_tac 1);
 qed "diag_subset_Sigma";
 
 goal Univ.thy "((A Times B) <**> (C Times D)) <= (A<*>C) Times (B<*>D)";
-by (fast_tac univ_cs 1);
+by (Fast_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 univ_cs);
 by (stac Split 1);
-by (fast_tac univ_cs 1);
+by (Fast_tac 1);
 qed "dprod_subset_Sigma2";
 
 goal Univ.thy "(A Times B <++> C Times D) <= (A<+>C) Times (B<+>D)";
-by (fast_tac univ_cs 1);
+by (Fast_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 (prod_cs addIs [equalityI, diagI] addSEs [diagE]) 1);
+by (fast_tac (!claset addIs [equalityI, diagI] addSEs [diagE]) 1);
 qed "fst_image_diag";
 
 goal Univ.thy "fst `` (r<**>s) = (fst``r) <*> (fst``s)";
-by (fast_tac (prod_cs addIs [equalityI, uprodI, dprodI]
+by (fast_tac (!claset addIs [equalityI, uprodI, dprodI]
                      addSEs [uprodE, dprodE]) 1);
 qed "fst_image_dprod";
 
 goal Univ.thy "fst `` (r<++>s) = (fst``r) <+> (fst``s)";
-by (fast_tac (prod_cs addIs [equalityI, usum_In0I, usum_In1I, 
+by (fast_tac (!claset addIs [equalityI, usum_In0I, usum_In1I, 
                              dsum_In0I, dsum_In1I]
                      addSEs [usumE, dsumE]) 1);
 qed "fst_image_dsum";
 
 Addsimps [fst_image_diag, fst_image_dprod, fst_image_dsum];