ZF/ind-syntax/refl_thin: new
ZF/intr-elim: added Pair_neq_0, succ_neq_0, refl_thin to simplify case rules

ZF/sum/Inl_iff, etc.: tidied and proved using simp_tac
ZF/qpair/QInl_iff, etc.: tidied and proved using simp_tac

ZF/datatype,intr_elim: replaced the undirectional use of sum_univ RS subsetD
by dresolve_tac InlD,InrD and etac PartE

--- a/src/ZF/Datatype.ML	Fri Oct 15 10:04:30 1993 +0100
+++ b/src/ZF/Datatype.ML	Fri Oct 15 10:21:01 1993 +0100
@@ -55,12 +55,16 @@
 val data_typechecks = 
     [SigmaI, InlI, InrI,
      Pair_in_univ, Inl_in_univ, Inr_in_univ, 
-     zero_in_univ, A_into_univ, nat_into_univ, sum_univ RS subsetD];
+     zero_in_univ, A_into_univ, nat_into_univ, UnCI];
 
+(*Needed for mutual recursion*)
+val data_elims = [make_elim InlD, make_elim InrD];
 
 (*For most co-datatypes involving quniv*)
 val co_data_typechecks = 
     [QSigmaI, QInlI, QInrI,
      QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
-     zero_in_quniv, A_into_quniv, nat_into_quniv, qsum_quniv RS subsetD];
+     zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
 
+val co_data_elims = [make_elim QInlD, make_elim QInrD];
+

--- a/src/ZF/List.ML	Fri Oct 15 10:04:30 1993 +0100
+++ b/src/ZF/List.ML	Fri Oct 15 10:21:01 1993 +0100
@@ -52,8 +52,7 @@
 			    Pair_in_univ]) 1);
 val list_univ = result();
 
-val list_subset_univ = standard
-    (list_mono RS (list_univ RSN (2,subset_trans)));
+val list_subset_univ = standard ([list_mono, list_univ] MRS subset_trans);
 
 val major::prems = goal List.thy
     "[| l: list(A);    \

--- a/src/ZF/QPair.ML	Fri Oct 15 10:04:30 1993 +0100
+++ b/src/ZF/QPair.ML	Fri Oct 15 10:21:01 1993 +0100
@@ -182,49 +182,43 @@
      ORELSE eresolve_tac (prems@[QSigmaE,singletonE,ssubst]) 1));
 val qsumE = result();
 
-(** QInjection and freeness rules **)
-
-val [major] = goalw QPair.thy qsum_defs "QInl(a)=QInl(b) ==> a=b";
-by (EVERY1 [rtac (major RS QPair_inject), assume_tac]);
-val QInl_inject = result();
-
-val [major] = goalw QPair.thy qsum_defs "QInr(a)=QInr(b) ==> a=b";
-by (EVERY1 [rtac (major RS QPair_inject), assume_tac]);
-val QInr_inject = result();
-
-val [major] = goalw QPair.thy qsum_defs "QInl(a)=QInr(b) ==> P";
-by (rtac (major RS QPair_inject) 1);
-by (etac (sym RS one_neq_0) 1);
-val QInl_neq_QInr = result();
-
-val QInr_neq_QInl = sym RS QInl_neq_QInr;
-
 (** Injection and freeness equivalences, for rewriting **)
 
-goal QPair.thy "QInl(a)=QInl(b) <-> a=b";
-by (rtac iffI 1);
-by (REPEAT (eresolve_tac [QInl_inject,subst_context] 1));
+goalw QPair.thy qsum_defs "QInl(a)=QInl(b) <-> a=b";
+by (simp_tac (ZF_ss addsimps [QPair_iff]) 1);
 val QInl_iff = result();
 
-goal QPair.thy "QInr(a)=QInr(b) <-> a=b";
-by (rtac iffI 1);
-by (REPEAT (eresolve_tac [QInr_inject,subst_context] 1));
+goalw QPair.thy qsum_defs "QInr(a)=QInr(b) <-> a=b";
+by (simp_tac (ZF_ss addsimps [QPair_iff]) 1);
 val QInr_iff = result();
 
-goal QPair.thy "QInl(a)=QInr(b) <-> False";
-by (rtac iffI 1);
-by (REPEAT (eresolve_tac [QInl_neq_QInr,FalseE] 1));
+goalw QPair.thy qsum_defs "QInl(a)=QInr(b) <-> False";
+by (simp_tac (ZF_ss addsimps [QPair_iff, one_not_0 RS not_sym]) 1);
 val QInl_QInr_iff = result();
 
-goal QPair.thy "QInr(b)=QInl(a) <-> False";
-by (rtac iffI 1);
-by (REPEAT (eresolve_tac [QInr_neq_QInl,FalseE] 1));
+goalw QPair.thy qsum_defs "QInr(b)=QInl(a) <-> False";
+by (simp_tac (ZF_ss addsimps [QPair_iff, one_not_0]) 1);
 val QInr_QInl_iff = result();
 
+(*Injection and freeness rules*)
+
+val QInl_inject = standard (QInl_iff RS iffD1);
+val QInr_inject = standard (QInr_iff RS iffD1);
+val QInl_neq_QInr = standard (QInl_QInr_iff RS iffD1 RS FalseE);
+val QInr_neq_QInl = standard (QInr_QInl_iff RS iffD1 RS FalseE);
+
 val qsum_cs = 
     ZF_cs addIs [QInlI,QInrI] addSEs [qsumE,QInl_neq_QInr,QInr_neq_QInl]
           addSDs [QInl_inject,QInr_inject];
 
+goal QPair.thy "!!A B. QInl(a): A<+>B ==> a: A";
+by (fast_tac qsum_cs 1);
+val QInlD = result();
+
+goal QPair.thy "!!A B. QInr(b): A<+>B ==> b: B";
+by (fast_tac qsum_cs 1);
+val QInrD = result();
+
 (** <+> is itself injective... who cares?? **)
 
 goal QPair.thy

--- a/src/ZF/Sum.ML	Fri Oct 15 10:04:30 1993 +0100
+++ b/src/ZF/Sum.ML	Fri Oct 15 10:21:01 1993 +0100
@@ -32,48 +32,42 @@
      ORELSE eresolve_tac (prems@[SigmaE,singletonE,ssubst]) 1));
 val sumE = result();
 
-(** Injection and freeness rules **)
-
-val [major] = goalw Sum.thy sum_defs "Inl(a)=Inl(b) ==> a=b";
-by (EVERY1 [rtac (major RS Pair_inject), assume_tac]);
-val Inl_inject = result();
-
-val [major] = goalw Sum.thy sum_defs "Inr(a)=Inr(b) ==> a=b";
-by (EVERY1 [rtac (major RS Pair_inject), assume_tac]);
-val Inr_inject = result();
-
-val [major] = goalw Sum.thy sum_defs "Inl(a)=Inr(b) ==> P";
-by (rtac (major RS Pair_inject) 1);
-by (etac (sym RS one_neq_0) 1);
-val Inl_neq_Inr = result();
-
-val Inr_neq_Inl = sym RS Inl_neq_Inr;
-
 (** Injection and freeness equivalences, for rewriting **)
 
-goal Sum.thy "Inl(a)=Inl(b) <-> a=b";
-by (rtac iffI 1);
-by (REPEAT (eresolve_tac [Inl_inject,subst_context] 1));
+goalw Sum.thy sum_defs "Inl(a)=Inl(b) <-> a=b";
+by (simp_tac (ZF_ss addsimps [Pair_iff]) 1);
 val Inl_iff = result();
 
-goal Sum.thy "Inr(a)=Inr(b) <-> a=b";
-by (rtac iffI 1);
-by (REPEAT (eresolve_tac [Inr_inject,subst_context] 1));
+goalw Sum.thy sum_defs "Inr(a)=Inr(b) <-> a=b";
+by (simp_tac (ZF_ss addsimps [Pair_iff]) 1);
 val Inr_iff = result();
 
-goal Sum.thy "Inl(a)=Inr(b) <-> False";
-by (rtac iffI 1);
-by (REPEAT (eresolve_tac [Inl_neq_Inr,FalseE] 1));
+goalw Sum.thy sum_defs "Inl(a)=Inr(b) <-> False";
+by (simp_tac (ZF_ss addsimps [Pair_iff, one_not_0 RS not_sym]) 1);
 val Inl_Inr_iff = result();
 
-goal Sum.thy "Inr(b)=Inl(a) <-> False";
-by (rtac iffI 1);
-by (REPEAT (eresolve_tac [Inr_neq_Inl,FalseE] 1));
+goalw Sum.thy sum_defs "Inr(b)=Inl(a) <-> False";
+by (simp_tac (ZF_ss addsimps [Pair_iff, one_not_0]) 1);
 val Inr_Inl_iff = result();
 
-val sum_cs = ZF_cs addIs [InlI,InrI] addSEs [sumE,Inl_neq_Inr,Inr_neq_Inl]
+(*Injection and freeness rules*)
+
+val Inl_inject = standard (Inl_iff RS iffD1);
+val Inr_inject = standard (Inr_iff RS iffD1);
+val Inl_neq_Inr = standard (Inl_Inr_iff RS iffD1 RS FalseE);
+val Inr_neq_Inl = standard (Inr_Inl_iff RS iffD1 RS FalseE);
+
+val sum_cs = ZF_cs addSIs [InlI,InrI] addSEs [sumE,Inl_neq_Inr,Inr_neq_Inl]
                    addSDs [Inl_inject,Inr_inject];
 
+goal Sum.thy "!!A B. Inl(a): A+B ==> a: A";
+by (fast_tac sum_cs 1);
+val InlD = result();
+
+goal Sum.thy "!!A B. Inr(b): A+B ==> b: B";
+by (fast_tac sum_cs 1);
+val InrD = result();
+
 goal Sum.thy "u: A+B <-> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))";
 by (fast_tac sum_cs 1);
 val sum_iff = result();

--- a/src/ZF/datatype.ML	Fri Oct 15 10:04:30 1993 +0100
+++ b/src/ZF/datatype.ML	Fri Oct 15 10:21:01 1993 +0100
@@ -55,12 +55,16 @@
 val data_typechecks = 
     [SigmaI, InlI, InrI,
      Pair_in_univ, Inl_in_univ, Inr_in_univ, 
-     zero_in_univ, A_into_univ, nat_into_univ, sum_univ RS subsetD];
+     zero_in_univ, A_into_univ, nat_into_univ, UnCI];
 
+(*Needed for mutual recursion*)
+val data_elims = [make_elim InlD, make_elim InrD];
 
 (*For most co-datatypes involving quniv*)
 val co_data_typechecks = 
     [QSigmaI, QInlI, QInrI,
      QPair_in_quniv, QInl_in_quniv, QInr_in_quniv, 
-     zero_in_quniv, A_into_quniv, nat_into_quniv, qsum_quniv RS subsetD];
+     zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
 
+val co_data_elims = [make_elim QInlD, make_elim QInrD];
+

--- a/src/ZF/fin.ML	Fri Oct 15 10:04:30 1993 +0100
+++ b/src/ZF/fin.ML	Fri Oct 15 10:21:01 1993 +0100
@@ -57,29 +57,30 @@
 (** Simplification for Fin **)
 val Fin_ss = arith_ss addsimps Fin.intrs;
 
-(*The union of two finite sets is fin*)
+(*The union of two finite sets is finite.*)
 val major::prems = goal Fin.thy
     "[| b: Fin(A);  c: Fin(A) |] ==> b Un c : Fin(A)";
 by (rtac (major RS Fin_induct) 1);
 by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_0, Un_cons]))));
 val Fin_UnI = result();
 
-(*The union of a set of finite sets is fin*)
+(*The union of a set of finite sets is finite.*)
 val [major] = goal Fin.thy "C : Fin(Fin(A)) ==> Union(C) : Fin(A)";
 by (rtac (major RS Fin_induct) 1);
 by (ALLGOALS (asm_simp_tac (Fin_ss addsimps [Union_0, Union_cons, Fin_UnI])));
 val Fin_UnionI = result();
 
-(*Every subset of a finite set is fin*)
-val [subs,fin] = goal Fin.thy "[| c<=b;  b: Fin(A) |] ==> c: Fin(A)";
-by (EVERY1 [subgoal_tac "(ALL z. z<=b --> z: Fin(A))",
-	    etac (spec RS mp),
-	    rtac subs]);
-by (rtac (fin RS Fin_induct) 1);
+(*Every subset of a finite set is finite.*)
+goal Fin.thy "!!b A. b: Fin(A) ==> ALL z. z<=b --> z: Fin(A)";
+be Fin_induct 1;
 by (simp_tac (Fin_ss addsimps [subset_empty_iff]) 1);
 by (safe_tac (ZF_cs addSDs [subset_cons_iff RS iffD1]));
 by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 2);
 by (ALLGOALS (asm_simp_tac Fin_ss));
+val Fin_subset_lemma = result();
+
+goal Fin.thy "!!c b A. [| c<=b;  b: Fin(A) |] ==> c: Fin(A)";
+by (REPEAT (ares_tac [Fin_subset_lemma RS spec RS mp] 1));
 val Fin_subset = result();
 
 val major::prems = goal Fin.thy 

--- a/src/ZF/ind-syntax.ML	Fri Oct 15 10:04:30 1993 +0100
+++ b/src/ZF/ind-syntax.ML	Fri Oct 15 10:21:01 1993 +0100
@@ -172,4 +172,7 @@
 val def_trans = prove_goal IFOL.thy "[| f==g;  g(a)=b |] ==> f(a)=b"
   (fn [rew,prem] => [ rewtac rew, rtac prem 1 ]);
 
+(*Delete needless equality assumptions*)
+val refl_thin = prove_goal IFOL.thy "!!P. [| a=a;  P |] ==> P"
+     (fn _ => [assume_tac 1]);
 

--- a/src/ZF/ind_syntax.ML	Fri Oct 15 10:04:30 1993 +0100
+++ b/src/ZF/ind_syntax.ML	Fri Oct 15 10:21:01 1993 +0100
@@ -172,4 +172,7 @@
 val def_trans = prove_goal IFOL.thy "[| f==g;  g(a)=b |] ==> f(a)=b"
   (fn [rew,prem] => [ rewtac rew, rtac prem 1 ]);
 
+(*Delete needless equality assumptions*)
+val refl_thin = prove_goal IFOL.thy "!!P. [| a=a;  P |] ==> P"
+     (fn _ => [assume_tac 1]);
 

--- a/src/ZF/intr-elim.ML	Fri Oct 15 10:04:30 1993 +0100
+++ b/src/ZF/intr-elim.ML	Fri Oct 15 10:21:01 1993 +0100
@@ -235,7 +235,7 @@
   disjIn selects the correct disjunct after unfolding*)
 fun intro_tacsf disjIn prems = 
   [(*insert prems and underlying sets*)
-   cut_facts_tac (prems @ (prems RL [PartD1])) 1,
+   cut_facts_tac prems 1,
    rtac (unfold RS ssubst) 1,
    REPEAT (resolve_tac [Part_eqI,CollectI] 1),
    (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
@@ -244,9 +244,10 @@
    rewrite_goals_tac con_defs,
    (*Now can solve the trivial equation*)
    REPEAT (rtac refl 2),
-   REPEAT (FIRSTGOAL (eresolve_tac (asm_rl::type_elims)
+   REPEAT (FIRSTGOAL (eresolve_tac (asm_rl::PartE::type_elims)
+		      ORELSE' hyp_subst_tac
 		      ORELSE' dresolve_tac rec_typechecks)),
-   DEPTH_SOLVE (ares_tac type_intrs 1)];
+   DEPTH_SOLVE (swap_res_tac type_intrs 1)];
 
 (*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
 val mk_disj_rls = 
@@ -260,7 +261,10 @@
 (********)
 val dummy = writeln "Proving the elimination rule...";
 
-val elim_rls = [asm_rl, FalseE, conjE, exE, disjE];
+(*Includes rules for succ and Pair since they are common constructions*)
+val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, 
+		Pair_neq_0, sym RS Pair_neq_0, succ_inject, refl_thin,
+		conjE, exE, disjE];
 
 val sumprod_free_SEs = 
     map (gen_make_elim [conjE,FalseE])

--- a/src/ZF/intr_elim.ML	Fri Oct 15 10:04:30 1993 +0100
+++ b/src/ZF/intr_elim.ML	Fri Oct 15 10:21:01 1993 +0100
@@ -235,7 +235,7 @@
   disjIn selects the correct disjunct after unfolding*)
 fun intro_tacsf disjIn prems = 
   [(*insert prems and underlying sets*)
-   cut_facts_tac (prems @ (prems RL [PartD1])) 1,
+   cut_facts_tac prems 1,
    rtac (unfold RS ssubst) 1,
    REPEAT (resolve_tac [Part_eqI,CollectI] 1),
    (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
@@ -244,9 +244,10 @@
    rewrite_goals_tac con_defs,
    (*Now can solve the trivial equation*)
    REPEAT (rtac refl 2),
-   REPEAT (FIRSTGOAL (eresolve_tac (asm_rl::type_elims)
+   REPEAT (FIRSTGOAL (eresolve_tac (asm_rl::PartE::type_elims)
+		      ORELSE' hyp_subst_tac
 		      ORELSE' dresolve_tac rec_typechecks)),
-   DEPTH_SOLVE (ares_tac type_intrs 1)];
+   DEPTH_SOLVE (swap_res_tac type_intrs 1)];
 
 (*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
 val mk_disj_rls = 
@@ -260,7 +261,10 @@
 (********)
 val dummy = writeln "Proving the elimination rule...";
 
-val elim_rls = [asm_rl, FalseE, conjE, exE, disjE];
+(*Includes rules for succ and Pair since they are common constructions*)
+val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, 
+		Pair_neq_0, sym RS Pair_neq_0, succ_inject, refl_thin,
+		conjE, exE, disjE];
 
 val sumprod_free_SEs = 
     map (gen_make_elim [conjE,FalseE])

--- a/src/ZF/list.ML	Fri Oct 15 10:04:30 1993 +0100
+++ b/src/ZF/list.ML	Fri Oct 15 10:21:01 1993 +0100
@@ -52,8 +52,7 @@
 			    Pair_in_univ]) 1);
 val list_univ = result();
 
-val list_subset_univ = standard
-    (list_mono RS (list_univ RSN (2,subset_trans)));
+val list_subset_univ = standard ([list_mono, list_univ] MRS subset_trans);
 
 val major::prems = goal List.thy
     "[| l: list(A);    \

--- a/src/ZF/qpair.ML	Fri Oct 15 10:04:30 1993 +0100
+++ b/src/ZF/qpair.ML	Fri Oct 15 10:21:01 1993 +0100
@@ -182,49 +182,43 @@
      ORELSE eresolve_tac (prems@[QSigmaE,singletonE,ssubst]) 1));
 val qsumE = result();
 
-(** QInjection and freeness rules **)
-
-val [major] = goalw QPair.thy qsum_defs "QInl(a)=QInl(b) ==> a=b";
-by (EVERY1 [rtac (major RS QPair_inject), assume_tac]);
-val QInl_inject = result();
-
-val [major] = goalw QPair.thy qsum_defs "QInr(a)=QInr(b) ==> a=b";
-by (EVERY1 [rtac (major RS QPair_inject), assume_tac]);
-val QInr_inject = result();
-
-val [major] = goalw QPair.thy qsum_defs "QInl(a)=QInr(b) ==> P";
-by (rtac (major RS QPair_inject) 1);
-by (etac (sym RS one_neq_0) 1);
-val QInl_neq_QInr = result();
-
-val QInr_neq_QInl = sym RS QInl_neq_QInr;
-
 (** Injection and freeness equivalences, for rewriting **)
 
-goal QPair.thy "QInl(a)=QInl(b) <-> a=b";
-by (rtac iffI 1);
-by (REPEAT (eresolve_tac [QInl_inject,subst_context] 1));
+goalw QPair.thy qsum_defs "QInl(a)=QInl(b) <-> a=b";
+by (simp_tac (ZF_ss addsimps [QPair_iff]) 1);
 val QInl_iff = result();
 
-goal QPair.thy "QInr(a)=QInr(b) <-> a=b";
-by (rtac iffI 1);
-by (REPEAT (eresolve_tac [QInr_inject,subst_context] 1));
+goalw QPair.thy qsum_defs "QInr(a)=QInr(b) <-> a=b";
+by (simp_tac (ZF_ss addsimps [QPair_iff]) 1);
 val QInr_iff = result();
 
-goal QPair.thy "QInl(a)=QInr(b) <-> False";
-by (rtac iffI 1);
-by (REPEAT (eresolve_tac [QInl_neq_QInr,FalseE] 1));
+goalw QPair.thy qsum_defs "QInl(a)=QInr(b) <-> False";
+by (simp_tac (ZF_ss addsimps [QPair_iff, one_not_0 RS not_sym]) 1);
 val QInl_QInr_iff = result();
 
-goal QPair.thy "QInr(b)=QInl(a) <-> False";
-by (rtac iffI 1);
-by (REPEAT (eresolve_tac [QInr_neq_QInl,FalseE] 1));
+goalw QPair.thy qsum_defs "QInr(b)=QInl(a) <-> False";
+by (simp_tac (ZF_ss addsimps [QPair_iff, one_not_0]) 1);
 val QInr_QInl_iff = result();
 
+(*Injection and freeness rules*)
+
+val QInl_inject = standard (QInl_iff RS iffD1);
+val QInr_inject = standard (QInr_iff RS iffD1);
+val QInl_neq_QInr = standard (QInl_QInr_iff RS iffD1 RS FalseE);
+val QInr_neq_QInl = standard (QInr_QInl_iff RS iffD1 RS FalseE);
+
 val qsum_cs = 
     ZF_cs addIs [QInlI,QInrI] addSEs [qsumE,QInl_neq_QInr,QInr_neq_QInl]
           addSDs [QInl_inject,QInr_inject];
 
+goal QPair.thy "!!A B. QInl(a): A<+>B ==> a: A";
+by (fast_tac qsum_cs 1);
+val QInlD = result();
+
+goal QPair.thy "!!A B. QInr(b): A<+>B ==> b: B";
+by (fast_tac qsum_cs 1);
+val QInrD = result();
+
 (** <+> is itself injective... who cares?? **)
 
 goal QPair.thy

--- a/src/ZF/sum.ML	Fri Oct 15 10:04:30 1993 +0100
+++ b/src/ZF/sum.ML	Fri Oct 15 10:21:01 1993 +0100
@@ -32,48 +32,42 @@
      ORELSE eresolve_tac (prems@[SigmaE,singletonE,ssubst]) 1));
 val sumE = result();
 
-(** Injection and freeness rules **)
-
-val [major] = goalw Sum.thy sum_defs "Inl(a)=Inl(b) ==> a=b";
-by (EVERY1 [rtac (major RS Pair_inject), assume_tac]);
-val Inl_inject = result();
-
-val [major] = goalw Sum.thy sum_defs "Inr(a)=Inr(b) ==> a=b";
-by (EVERY1 [rtac (major RS Pair_inject), assume_tac]);
-val Inr_inject = result();
-
-val [major] = goalw Sum.thy sum_defs "Inl(a)=Inr(b) ==> P";
-by (rtac (major RS Pair_inject) 1);
-by (etac (sym RS one_neq_0) 1);
-val Inl_neq_Inr = result();
-
-val Inr_neq_Inl = sym RS Inl_neq_Inr;
-
 (** Injection and freeness equivalences, for rewriting **)
 
-goal Sum.thy "Inl(a)=Inl(b) <-> a=b";
-by (rtac iffI 1);
-by (REPEAT (eresolve_tac [Inl_inject,subst_context] 1));
+goalw Sum.thy sum_defs "Inl(a)=Inl(b) <-> a=b";
+by (simp_tac (ZF_ss addsimps [Pair_iff]) 1);
 val Inl_iff = result();
 
-goal Sum.thy "Inr(a)=Inr(b) <-> a=b";
-by (rtac iffI 1);
-by (REPEAT (eresolve_tac [Inr_inject,subst_context] 1));
+goalw Sum.thy sum_defs "Inr(a)=Inr(b) <-> a=b";
+by (simp_tac (ZF_ss addsimps [Pair_iff]) 1);
 val Inr_iff = result();
 
-goal Sum.thy "Inl(a)=Inr(b) <-> False";
-by (rtac iffI 1);
-by (REPEAT (eresolve_tac [Inl_neq_Inr,FalseE] 1));
+goalw Sum.thy sum_defs "Inl(a)=Inr(b) <-> False";
+by (simp_tac (ZF_ss addsimps [Pair_iff, one_not_0 RS not_sym]) 1);
 val Inl_Inr_iff = result();
 
-goal Sum.thy "Inr(b)=Inl(a) <-> False";
-by (rtac iffI 1);
-by (REPEAT (eresolve_tac [Inr_neq_Inl,FalseE] 1));
+goalw Sum.thy sum_defs "Inr(b)=Inl(a) <-> False";
+by (simp_tac (ZF_ss addsimps [Pair_iff, one_not_0]) 1);
 val Inr_Inl_iff = result();
 
-val sum_cs = ZF_cs addIs [InlI,InrI] addSEs [sumE,Inl_neq_Inr,Inr_neq_Inl]
+(*Injection and freeness rules*)
+
+val Inl_inject = standard (Inl_iff RS iffD1);
+val Inr_inject = standard (Inr_iff RS iffD1);
+val Inl_neq_Inr = standard (Inl_Inr_iff RS iffD1 RS FalseE);
+val Inr_neq_Inl = standard (Inr_Inl_iff RS iffD1 RS FalseE);
+
+val sum_cs = ZF_cs addSIs [InlI,InrI] addSEs [sumE,Inl_neq_Inr,Inr_neq_Inl]
                    addSDs [Inl_inject,Inr_inject];
 
+goal Sum.thy "!!A B. Inl(a): A+B ==> a: A";
+by (fast_tac sum_cs 1);
+val InlD = result();
+
+goal Sum.thy "!!A B. Inr(b): A+B ==> b: B";
+by (fast_tac sum_cs 1);
+val InrD = result();
+
 goal Sum.thy "u: A+B <-> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))";
 by (fast_tac sum_cs 1);
 val sum_iff = result();