diff -r 428efffe8599 -r b50b8c0eec01 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";