src/ZF/Sum.ML

--- a/src/ZF/Sum.ML	Fri Jan 03 10:48:28 1997 +0100
+++ b/src/ZF/Sum.ML	Fri Jan 03 15:01:55 1997 +0100
@@ -17,7 +17,7 @@
 
 goalw Sum.thy [Part_def]
     "!!a b A h. [| a : A;  a=h(b) |] ==> a : Part(A,h)";
-by (REPEAT (ares_tac [exI,CollectI] 1));
+by (Fast_tac 1);
 qed "Part_eqI";
 
 val PartI = refl RSN (2,Part_eqI);
@@ -30,6 +30,9 @@
 by (REPEAT (ares_tac prems 1));
 qed "PartE";
 
+AddSIs [PartI];
+AddSEs [PartE];
+
 goalw Sum.thy [Part_def] "Part(A,h) <= A";
 by (rtac Collect_subset 1);
 qed "Part_subset";
@@ -46,11 +49,11 @@
 (** Introduction rules for the injections **)
 
 goalw Sum.thy sum_defs "!!a A B. a : A ==> Inl(a) : A+B";
-by (REPEAT (ares_tac [UnI1,SigmaI,singletonI] 1));
+by (Fast_tac 1);
 qed "InlI";
 
 goalw Sum.thy sum_defs "!!b A B. b : B ==> Inr(b) : A+B";
-by (REPEAT (ares_tac [UnI2,SigmaI,singletonI] 1));
+by (Fast_tac 1);
 qed "InrI";
 
 (** Elimination rules **)
@@ -68,21 +71,25 @@
 (** Injection and freeness equivalences, for rewriting **)
 
 goalw Sum.thy sum_defs "Inl(a)=Inl(b) <-> a=b";
-by (simp_tac ZF_ss 1);
+by (Simp_tac 1);
 qed "Inl_iff";
 
 goalw Sum.thy sum_defs "Inr(a)=Inr(b) <-> a=b";
-by (simp_tac ZF_ss 1);
+by (Simp_tac 1);
 qed "Inr_iff";
 
 goalw Sum.thy sum_defs "Inl(a)=Inr(b) <-> False";
-by (simp_tac (ZF_ss addsimps [one_not_0 RS not_sym]) 1);
+by (Simp_tac 1);
 qed "Inl_Inr_iff";
 
 goalw Sum.thy sum_defs "Inr(b)=Inl(a) <-> False";
-by (simp_tac (ZF_ss addsimps [one_not_0]) 1);
+by (Simp_tac 1);
 qed "Inr_Inl_iff";
 
+goalw Sum.thy sum_defs "0+0 = 0";
+by (Simp_tac 1);
+qed "sum_empty";
+
 (*Injection and freeness rules*)
 
 bind_thm ("Inl_inject", (Inl_iff RS iffD1));
@@ -90,29 +97,33 @@
 bind_thm ("Inl_neq_Inr", (Inl_Inr_iff RS iffD1 RS FalseE));
 bind_thm ("Inr_neq_Inl", (Inr_Inl_iff RS iffD1 RS FalseE));
 
-val sum_cs = ZF_cs addSIs [PartI, InlI, InrI] 
-                   addSEs [PartE, sumE, Inl_neq_Inr, Inr_neq_Inl]
-                   addSDs [Inl_inject, Inr_inject];
+AddSIs [InlI, InrI];
+AddSEs [sumE, Inl_neq_Inr, Inr_neq_Inl];
+AddSDs [Inl_inject, Inr_inject];
+
+Addsimps [InlI, InrI, Inl_iff, Inr_iff, Inl_Inr_iff, Inr_Inl_iff, sum_empty];
+
+val sum_cs = !claset;
 
 goal Sum.thy "!!A B. Inl(a): A+B ==> a: A";
-by (fast_tac sum_cs 1);
+by (Fast_tac 1);
 qed "InlD";
 
 goal Sum.thy "!!A B. Inr(b): A+B ==> b: B";
-by (fast_tac sum_cs 1);
+by (Fast_tac 1);
 qed "InrD";
 
 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);
+by (Fast_tac 1);
 qed "sum_iff";
 
 goal Sum.thy "A+B <= C+D <-> A<=C & B<=D";
-by (fast_tac sum_cs 1);
+by (Fast_tac 1);
 qed "sum_subset_iff";
 
 goal Sum.thy "A+B = C+D <-> A=C & B=D";
-by (simp_tac (ZF_ss addsimps [extension,sum_subset_iff]) 1);
-by (fast_tac ZF_cs 1);
+by (simp_tac (!simpset addsimps [extension,sum_subset_iff]) 1);
+by (Fast_tac 1);
 qed "sum_equal_iff";
 
 goalw Sum.thy [sum_def] "A+A = 2*A";
@@ -123,13 +134,17 @@
 (*** Eliminator -- case ***)
 
 goalw Sum.thy sum_defs "case(c, d, Inl(a)) = c(a)";
-by (simp_tac (ZF_ss addsimps [cond_0]) 1);
+by (simp_tac (!simpset addsimps [cond_0]) 1);
 qed "case_Inl";
 
 goalw Sum.thy sum_defs "case(c, d, Inr(b)) = d(b)";
-by (simp_tac (ZF_ss addsimps [cond_1]) 1);
+by (simp_tac (!simpset addsimps [cond_1]) 1);
 qed "case_Inr";
 
+Addsimps [case_Inl, case_Inr];
+
+val sum_ss = !simpset;
+
 val major::prems = goal Sum.thy
     "[| u: A+B; \
 \       !!x. x: A ==> c(x): C(Inl(x));   \
@@ -137,8 +152,7 @@
 \    |] ==> case(c,d,u) : C(u)";
 by (rtac (major RS sumE) 1);
 by (ALLGOALS (etac ssubst));
-by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
-                            (prems@[case_Inl,case_Inr]))));
+by (ALLGOALS (asm_simp_tac (!simpset addsimps prems)));
 qed "case_type";
 
 goal Sum.thy
@@ -146,11 +160,7 @@
 \       R(case(c,d,u)) <-> \
 \       ((ALL x:A. u = Inl(x) --> R(c(x))) & \
 \       (ALL y:B. u = Inr(y) --> R(d(y))))";
-by (etac sumE 1);
-by (asm_simp_tac (ZF_ss addsimps [case_Inl]) 1);
-by (fast_tac sum_cs 1);
-by (asm_simp_tac (ZF_ss addsimps [case_Inr]) 1);
-by (fast_tac sum_cs 1);
+by (Auto_tac());
 qed "expand_case";
 
 val major::prems = goal Sum.thy
@@ -159,39 +169,35 @@
 \     !!y. y:B ==> d(y)=d'(y)   \
 \  |] ==> case(c,d,z) = case(c',d',z)";
 by (resolve_tac [major RS sumE] 1);
-by (ALLGOALS (asm_simp_tac (ZF_ss addsimps ([case_Inl, case_Inr] @ prems))));
+by (ALLGOALS (asm_simp_tac (!simpset addsimps prems)));
 qed "case_cong";
 
-val [major] = goal Sum.thy
-  "z: A+B ==>   \
-\  case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) = \
-\  case(%x. c(c'(x)), %y. d(d'(y)), z)";
-by (resolve_tac [major RS sumE] 1);
-by (ALLGOALS (asm_simp_tac (ZF_ss addsimps [case_Inl, case_Inr])));
+goal Sum.thy
+  "!!z. z: A+B ==>   \
+\       case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) = \
+\       case(%x. c(c'(x)), %y. d(d'(y)), z)";
+by (Auto_tac());
 qed "case_case";
 
-val sum_ss = ZF_ss addsimps [InlI, InrI, Inl_iff, Inr_iff, 
-                             Inl_Inr_iff, Inr_Inl_iff,
-                             case_Inl, case_Inr];
 
 (*** More rules for Part(A,h) ***)
 
 goal Sum.thy "!!A B h. A<=B ==> Part(A,h)<=Part(B,h)";
-by (fast_tac sum_cs 1);
+by (Fast_tac 1);
 qed "Part_mono";
 
 goal Sum.thy "Part(Collect(A,P), h) = Collect(Part(A,h), P)";
-by (fast_tac (sum_cs addSIs [equalityI]) 1);
+by (fast_tac (!claset addSIs [equalityI]) 1);
 qed "Part_Collect";
 
 bind_thm ("Part_CollectE", Part_Collect RS equalityD1 RS subsetD RS CollectE);
 
 goal Sum.thy "Part(A+B,Inl) = {Inl(x). x: A}";
-by (fast_tac (sum_cs addIs [equalityI]) 1);
+by (fast_tac (!claset addIs [equalityI]) 1);
 qed "Part_Inl";
 
 goal Sum.thy "Part(A+B,Inr) = {Inr(y). y: B}";
-by (fast_tac (sum_cs addIs [equalityI]) 1);
+by (fast_tac (!claset addIs [equalityI]) 1);
 qed "Part_Inr";
 
 goalw Sum.thy [Part_def] "!!a. a : Part(A,h) ==> a : A";
@@ -199,13 +205,13 @@
 qed "PartD1";
 
 goal Sum.thy "Part(A,%x.x) = A";
-by (fast_tac (sum_cs addIs [equalityI]) 1);
+by (fast_tac (!claset addIs [equalityI]) 1);
 qed "Part_id";
 
 goal Sum.thy "Part(A+B, %x.Inr(h(x))) = {Inr(y). y: Part(B,h)}";
-by (fast_tac (sum_cs addIs [equalityI]) 1);
+by (fast_tac (!claset addIs [equalityI]) 1);
 qed "Part_Inr2";
 
 goal Sum.thy "!!A B C. C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C";
-by (fast_tac (sum_cs addIs [equalityI]) 1);
+by (fast_tac (!claset addIs [equalityI]) 1);
 qed "Part_sum_equality";