src/HOL/Sum.ML
changeset 1985 84cf16192e03
parent 1761 29e08d527ba1
child 2212 bd705e9de196
     1.1 --- a/src/HOL/Sum.ML	Thu Sep 12 10:36:51 1996 +0200
     1.2 +++ b/src/HOL/Sum.ML	Thu Sep 12 10:40:05 1996 +0200
     1.3 @@ -40,16 +40,13 @@
     1.4  by (rtac Inr_RepI 1);
     1.5  qed "Inl_not_Inr";
     1.6  
     1.7 -bind_thm ("Inl_neq_Inr", (Inl_not_Inr RS notE));
     1.8 -val Inr_neq_Inl = sym RS Inl_neq_Inr;
     1.9 +bind_thm ("Inr_not_Inl", Inl_not_Inr RS not_sym);
    1.10 +
    1.11 +AddIffs [Inl_not_Inr, Inr_not_Inl];
    1.12  
    1.13 -goal Sum.thy "(Inl(a)=Inr(b)) = False";
    1.14 -by (simp_tac (!simpset addsimps [Inl_not_Inr]) 1);
    1.15 -qed "Inl_Inr_eq";
    1.16 +bind_thm ("Inl_neq_Inr", Inl_not_Inr RS notE);
    1.17  
    1.18 -goal Sum.thy "(Inr(b)=Inl(a))  =  False";
    1.19 -by (simp_tac (!simpset addsimps [Inl_not_Inr RS not_sym]) 1);
    1.20 -qed "Inr_Inl_eq";
    1.21 +val Inr_neq_Inl = sym RS Inl_neq_Inr;
    1.22  
    1.23  
    1.24  (** Injectiveness of Inl and Inr **)
    1.25 @@ -88,16 +85,18 @@
    1.26  by (fast_tac (!claset addSEs [Inr_inject]) 1);
    1.27  qed "Inr_eq";
    1.28  
    1.29 +AddIffs [Inl_eq, Inr_eq];
    1.30 +
    1.31  (*** Rules for the disjoint sum of two SETS ***)
    1.32  
    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 (REPEAT (ares_tac [UnI1,imageI] 1));
    1.37 +by (Fast_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 (REPEAT (ares_tac [UnI2,imageI] 1));
    1.42 +by (Fast_tac 1);
    1.43  qed "InrI";
    1.44  
    1.45  (** Elimination rules **)
    1.46 @@ -113,13 +112,8 @@
    1.47  qed "plusE";
    1.48  
    1.49  
    1.50 -val sum_cs = set_cs addSIs [InlI, InrI] 
    1.51 -                    addSEs [plusE, Inl_neq_Inr, Inr_neq_Inl]
    1.52 -                    addSDs [Inl_inject, Inr_inject];
    1.53 -
    1.54  AddSIs [InlI, InrI]; 
    1.55 -AddSEs [plusE, Inl_neq_Inr, Inr_neq_Inl];
    1.56 -AddSDs [Inl_inject, Inr_inject];
    1.57 +AddSEs [plusE];
    1.58  
    1.59  
    1.60  (** sum_case -- the selection operator for sums **)
    1.61 @@ -132,6 +126,8 @@
    1.62  by (fast_tac (!claset addIs [select_equality]) 1);
    1.63  qed "sum_case_Inr";
    1.64  
    1.65 +Addsimps [sum_case_Inl, sum_case_Inr];
    1.66 +
    1.67  (** Exhaustion rule for sums -- a degenerate form of induction **)
    1.68  
    1.69  val prems = goalw Sum.thy [Inl_def,Inr_def]
    1.70 @@ -152,17 +148,10 @@
    1.71  
    1.72  goal Sum.thy "R(sum_case f g s) = \
    1.73  \             ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))";
    1.74 -by (rtac sumE 1);
    1.75 -by (etac ssubst 1);
    1.76 -by (stac sum_case_Inl 1);
    1.77 -by (fast_tac (!claset addSEs [make_elim Inl_inject, Inl_neq_Inr]) 1);
    1.78 -by (etac ssubst 1);
    1.79 -by (stac sum_case_Inr 1);
    1.80 -by (fast_tac (!claset addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1);
    1.81 +by (res_inst_tac [("s","s")] sumE 1);
    1.82 +by (Auto_tac());
    1.83  qed "expand_sum_case";
    1.84  
    1.85 -Addsimps [Inl_eq, Inr_eq, Inl_Inr_eq, Inr_Inl_eq,  sum_case_Inl, sum_case_Inr];
    1.86 -
    1.87  (*Prevents simplification of f and g: much faster*)
    1.88  qed_goal "sum_case_weak_cong" Sum.thy
    1.89    "s=t ==> sum_case f g s = sum_case f g t"
    1.90 @@ -170,7 +159,6 @@
    1.91  
    1.92  
    1.93  
    1.94 -
    1.95  (** Rules for the Part primitive **)
    1.96  
    1.97  goalw Sum.thy [Part_def]