src/HOL/Sum.ML
changeset 2891 d8f254ad1ab9
parent 2212 bd705e9de196
child 2922 580647a879cf
     1.1 --- a/src/HOL/Sum.ML	Fri Apr 04 11:18:19 1997 +0200
     1.2 +++ b/src/HOL/Sum.ML	Fri Apr 04 11:18:52 1997 +0200
     1.3 @@ -53,12 +53,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 1);
     1.8 +by (Blast_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 1);
    1.14 +by (Blast_tac 1);
    1.15  qed "Inr_Rep_inject";
    1.16  
    1.17  goalw Sum.thy [Inl_def] "inj(Inl)";
    1.18 @@ -78,11 +78,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 (!claset addSEs [Inl_inject]) 1);
    1.23 +by (blast_tac (!claset addSDs [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 (!claset addSEs [Inr_inject]) 1);
    1.28 +by (blast_tac (!claset addSDs [Inr_inject]) 1);
    1.29  qed "Inr_eq";
    1.30  
    1.31  AddIffs [Inl_eq, Inr_eq];
    1.32 @@ -92,11 +92,11 @@
    1.33  (** Introduction rules for the injections **)
    1.34  
    1.35  goalw Sum.thy [sum_def] "!!a A B. a : A ==> Inl(a) : A Plus B";
    1.36 -by (Fast_tac 1);
    1.37 +by (Blast_tac 1);
    1.38  qed "InlI";
    1.39  
    1.40  goalw Sum.thy [sum_def] "!!b A B. b : B ==> Inr(b) : A Plus B";
    1.41 -by (Fast_tac 1);
    1.42 +by (Blast_tac 1);
    1.43  qed "InrI";
    1.44  
    1.45  (** Elimination rules **)
    1.46 @@ -119,7 +119,7 @@
    1.47  (** sum_case -- the selection operator for sums **)
    1.48  
    1.49  goalw Sum.thy [sum_case_def] "sum_case f g (Inl x) = f(x)";
    1.50 -by (fast_tac (!claset addIs [select_equality]) 1);
    1.51 +by (blast_tac (!claset addIs [select_equality]) 1);
    1.52  qed "sum_case_Inl";
    1.53  
    1.54  goalw Sum.thy [sum_case_def] "sum_case f g (Inr x) = g(x)";
    1.55 @@ -163,7 +163,7 @@
    1.56  
    1.57  goalw Sum.thy [Part_def]
    1.58      "!!a b A h. [| a : A;  a=h(b) |] ==> a : Part A h";
    1.59 -by (Fast_tac 1);
    1.60 +by (Blast_tac 1);
    1.61  qed "Part_eqI";
    1.62  
    1.63  val PartI = refl RSN (2,Part_eqI);
    1.64 @@ -177,12 +177,15 @@
    1.65  by (REPEAT (ares_tac prems 1));
    1.66  qed "PartE";
    1.67  
    1.68 +AddIs  [Part_eqI];
    1.69 +AddSEs [PartE];
    1.70 +
    1.71  goalw Sum.thy [Part_def] "Part A h <= A";
    1.72  by (rtac Int_lower1 1);
    1.73  qed "Part_subset";
    1.74  
    1.75  goal Sum.thy "!!A B. A<=B ==> Part A h <= Part B h";
    1.76 -by (fast_tac (!claset addSIs [PartI] addSEs [PartE]) 1);
    1.77 +by (Fast_tac 1);
    1.78  qed "Part_mono";
    1.79  
    1.80  val basic_monos = basic_monos @ [Part_mono];
    1.81 @@ -192,14 +195,14 @@
    1.82  qed "PartD1";
    1.83  
    1.84  goal Sum.thy "Part A (%x.x) = A";
    1.85 -by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 1);
    1.86 +by (Blast_tac 1);
    1.87  qed "Part_id";
    1.88  
    1.89  goal Sum.thy "Part (A Int B) h = (Part A h) Int (Part B h)";
    1.90 -by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 1);
    1.91 +by (Fast_tac 1);
    1.92  qed "Part_Int";
    1.93  
    1.94  (*For inductive definitions*)
    1.95  goal Sum.thy "Part (A Int {x.P x}) h = (Part A h) Int {x.P x}";
    1.96 -by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 1);
    1.97 +by (Fast_tac 1);
    1.98  qed "Part_Collect";