src/HOL/Sum.ML
changeset 1760 6f41a494f3b1
parent 1515 4ed79ebab64d
child 1761 29e08d527ba1
     1.1 --- a/src/HOL/Sum.ML	Wed May 22 18:32:37 1996 +0200
     1.2 +++ b/src/HOL/Sum.ML	Thu May 23 14:37:06 1996 +0200
     1.3 @@ -56,12 +56,12 @@
     1.4  
     1.5  val [major] = goalw Sum.thy [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c";
     1.6  by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
     1.7 -by (fast_tac HOL_cs 1);
     1.8 +by (Fast_tac 1);
     1.9  qed "Inl_Rep_inject";
    1.10  
    1.11  val [major] = goalw Sum.thy [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d";
    1.12  by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
    1.13 -by (fast_tac HOL_cs 1);
    1.14 +by (Fast_tac 1);
    1.15  qed "Inr_Rep_inject";
    1.16  
    1.17  goalw Sum.thy [Inl_def] "inj(Inl)";
    1.18 @@ -81,11 +81,11 @@
    1.19  val Inr_inject = inj_Inr RS injD;
    1.20  
    1.21  goal Sum.thy "(Inl(x)=Inl(y)) = (x=y)";
    1.22 -by (fast_tac (HOL_cs addSEs [Inl_inject]) 1);
    1.23 +by (fast_tac (!claset addSEs [Inl_inject]) 1);
    1.24  qed "Inl_eq";
    1.25  
    1.26  goal Sum.thy "(Inr(x)=Inr(y)) = (x=y)";
    1.27 -by (fast_tac (HOL_cs addSEs [Inr_inject]) 1);
    1.28 +by (fast_tac (!claset addSEs [Inr_inject]) 1);
    1.29  qed "Inr_eq";
    1.30  
    1.31  (*** Rules for the disjoint sum of two SETS ***)
    1.32 @@ -117,15 +117,19 @@
    1.33                      addSEs [plusE, Inl_neq_Inr, Inr_neq_Inl]
    1.34                      addSDs [Inl_inject, Inr_inject];
    1.35  
    1.36 +AddSIs [InlI, InrI]; 
    1.37 +AddSEs [plusE, Inl_neq_Inr, Inr_neq_Inl];
    1.38 +AddSDs [Inl_inject, Inr_inject];
    1.39 +
    1.40  
    1.41  (** sum_case -- the selection operator for sums **)
    1.42  
    1.43  goalw Sum.thy [sum_case_def] "sum_case f g (Inl x) = f(x)";
    1.44 -by (fast_tac (sum_cs addIs [select_equality]) 1);
    1.45 +by (fast_tac (!claset addIs [select_equality]) 1);
    1.46  qed "sum_case_Inl";
    1.47  
    1.48  goalw Sum.thy [sum_case_def] "sum_case f g (Inr x) = g(x)";
    1.49 -by (fast_tac (sum_cs addIs [select_equality]) 1);
    1.50 +by (fast_tac (!claset addIs [select_equality]) 1);
    1.51  qed "sum_case_Inr";
    1.52  
    1.53  (** Exhaustion rule for sums -- a degenerate form of induction **)
    1.54 @@ -151,10 +155,10 @@
    1.55  by (rtac sumE 1);
    1.56  by (etac ssubst 1);
    1.57  by (stac sum_case_Inl 1);
    1.58 -by (fast_tac (set_cs addSEs [make_elim Inl_inject, Inl_neq_Inr]) 1);
    1.59 +by (fast_tac (!claset addSEs [make_elim Inl_inject, Inl_neq_Inr]) 1);
    1.60  by (etac ssubst 1);
    1.61  by (stac sum_case_Inr 1);
    1.62 -by (fast_tac (set_cs addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1);
    1.63 +by (fast_tac (!claset addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1);
    1.64  qed "expand_sum_case";
    1.65  
    1.66  Addsimps [Inl_eq, Inr_eq, Inl_Inr_eq, Inr_Inl_eq,  sum_case_Inl, sum_case_Inr];
    1.67 @@ -171,7 +175,7 @@
    1.68  
    1.69  goalw Sum.thy [Part_def]
    1.70      "!!a b A h. [| a : A;  a=h(b) |] ==> a : Part A h";
    1.71 -by (fast_tac set_cs 1);
    1.72 +by (Fast_tac 1);
    1.73  qed "Part_eqI";
    1.74  
    1.75  val PartI = refl RSN (2,Part_eqI);
    1.76 @@ -190,7 +194,7 @@
    1.77  qed "Part_subset";
    1.78  
    1.79  goal Sum.thy "!!A B. A<=B ==> Part A h <= Part B h";
    1.80 -by (fast_tac (set_cs addSIs [PartI] addSEs [PartE]) 1);
    1.81 +by (fast_tac (!claset addSIs [PartI] addSEs [PartE]) 1);
    1.82  qed "Part_mono";
    1.83  
    1.84  val basic_monos = basic_monos @ [Part_mono];
    1.85 @@ -200,14 +204,14 @@
    1.86  qed "PartD1";
    1.87  
    1.88  goal Sum.thy "Part A (%x.x) = A";
    1.89 -by (fast_tac (set_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
    1.90 +by (fast_tac (!claset addIs [PartI,equalityI] addSEs [PartE]) 1);
    1.91  qed "Part_id";
    1.92  
    1.93  goal Sum.thy "Part (A Int B) h = (Part A h) Int (Part B h)";
    1.94 -by (fast_tac (set_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
    1.95 +by (fast_tac (!claset addIs [PartI,equalityI] addSEs [PartE]) 1);
    1.96  qed "Part_Int";
    1.97  
    1.98  (*For inductive definitions*)
    1.99  goal Sum.thy "Part (A Int {x.P x}) h = (Part A h) Int {x.P x}";
   1.100 -by (fast_tac (set_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
   1.101 +by (fast_tac (!claset addIs [PartI,equalityI] addSEs [PartE]) 1);
   1.102  qed "Part_Collect";