clasohm@0: (*  Title: 	ZF/sum
clasohm@0:     ID:         $Id$
clasohm@0:     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0:     Copyright   1992  University of Cambridge
clasohm@0: 
clasohm@0: Disjoint sums in Zermelo-Fraenkel Set Theory 
clasohm@0: *)
clasohm@0: 
clasohm@0: open Sum;
clasohm@0: 
clasohm@0: val sum_defs = [sum_def,Inl_def,Inr_def,case_def];
clasohm@0: 
clasohm@0: (** Introduction rules for the injections **)
clasohm@0: 
clasohm@0: goalw Sum.thy sum_defs "!!a A B. a : A ==> Inl(a) : A+B";
clasohm@0: by (REPEAT (ares_tac [UnI1,SigmaI,singletonI] 1));
clasohm@0: val InlI = result();
clasohm@0: 
clasohm@0: goalw Sum.thy sum_defs "!!b A B. b : B ==> Inr(b) : A+B";
clasohm@0: by (REPEAT (ares_tac [UnI2,SigmaI,singletonI] 1));
clasohm@0: val InrI = result();
clasohm@0: 
clasohm@0: (** Elimination rules **)
clasohm@0: 
clasohm@0: val major::prems = goalw Sum.thy sum_defs
clasohm@0:     "[| u: A+B;  \
clasohm@0: \       !!x. [| x:A;  u=Inl(x) |] ==> P; \
clasohm@0: \       !!y. [| y:B;  u=Inr(y) |] ==> P \
clasohm@0: \    |] ==> P";
clasohm@0: by (rtac (major RS UnE) 1);
clasohm@0: by (REPEAT (rtac refl 1
clasohm@0:      ORELSE eresolve_tac (prems@[SigmaE,singletonE,ssubst]) 1));
clasohm@0: val sumE = result();
clasohm@0: 
clasohm@0: (** Injection and freeness rules **)
clasohm@0: 
clasohm@0: val [major] = goalw Sum.thy sum_defs "Inl(a)=Inl(b) ==> a=b";
clasohm@0: by (EVERY1 [rtac (major RS Pair_inject), assume_tac]);
clasohm@0: val Inl_inject = result();
clasohm@0: 
clasohm@0: val [major] = goalw Sum.thy sum_defs "Inr(a)=Inr(b) ==> a=b";
clasohm@0: by (EVERY1 [rtac (major RS Pair_inject), assume_tac]);
clasohm@0: val Inr_inject = result();
clasohm@0: 
clasohm@0: val [major] = goalw Sum.thy sum_defs "Inl(a)=Inr(b) ==> P";
clasohm@0: by (rtac (major RS Pair_inject) 1);
clasohm@0: by (etac (sym RS one_neq_0) 1);
clasohm@0: val Inl_neq_Inr = result();
clasohm@0: 
clasohm@0: val Inr_neq_Inl = sym RS Inl_neq_Inr;
clasohm@0: 
clasohm@0: (** Injection and freeness equivalences, for rewriting **)
clasohm@0: 
clasohm@0: goal Sum.thy "Inl(a)=Inl(b) <-> a=b";
clasohm@0: by (rtac iffI 1);
clasohm@0: by (REPEAT (eresolve_tac [Inl_inject,subst_context] 1));
clasohm@0: val Inl_iff = result();
clasohm@0: 
clasohm@0: goal Sum.thy "Inr(a)=Inr(b) <-> a=b";
clasohm@0: by (rtac iffI 1);
clasohm@0: by (REPEAT (eresolve_tac [Inr_inject,subst_context] 1));
clasohm@0: val Inr_iff = result();
clasohm@0: 
clasohm@0: goal Sum.thy "Inl(a)=Inr(b) <-> False";
clasohm@0: by (rtac iffI 1);
clasohm@0: by (REPEAT (eresolve_tac [Inl_neq_Inr,FalseE] 1));
clasohm@0: val Inl_Inr_iff = result();
clasohm@0: 
clasohm@0: goal Sum.thy "Inr(b)=Inl(a) <-> False";
clasohm@0: by (rtac iffI 1);
clasohm@0: by (REPEAT (eresolve_tac [Inr_neq_Inl,FalseE] 1));
clasohm@0: val Inr_Inl_iff = result();
clasohm@0: 
clasohm@0: val sum_cs = ZF_cs addIs [InlI,InrI] addSEs [sumE,Inl_neq_Inr,Inr_neq_Inl]
clasohm@0:                    addSDs [Inl_inject,Inr_inject];
clasohm@0: 
clasohm@0: goal Sum.thy "u: A+B <-> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))";
clasohm@0: by (fast_tac sum_cs 1);
clasohm@0: val sum_iff = result();
clasohm@0: 
clasohm@0: goal Sum.thy "A+B <= C+D <-> A<=C & B<=D";
clasohm@0: by (fast_tac sum_cs 1);
clasohm@0: val sum_subset_iff = result();
clasohm@0: 
clasohm@0: goal Sum.thy "A+B = C+D <-> A=C & B=D";
clasohm@0: by (SIMP_TAC (ZF_ss addrews [extension,sum_subset_iff]) 1);
clasohm@0: by (fast_tac ZF_cs 1);
clasohm@0: val sum_equal_iff = result();
clasohm@0: 
clasohm@0: (*** Eliminator -- case ***)
clasohm@0: 
clasohm@0: goalw Sum.thy sum_defs "case(c, d, Inl(a)) = c(a)";
clasohm@0: by (rtac (split RS trans) 1);
clasohm@0: by (rtac cond_0 1);
clasohm@0: val case_Inl = result();
clasohm@0: 
clasohm@0: goalw Sum.thy sum_defs "case(c, d, Inr(b)) = d(b)";
clasohm@0: by (rtac (split RS trans) 1);
clasohm@0: by (rtac cond_1 1);
clasohm@0: val case_Inr = result();
clasohm@0: 
clasohm@0: val prems = goalw Sum.thy [case_def]
clasohm@0:     "[| u=u'; !!x. c(x)=c'(x);  !!y. d(y)=d'(y) |] ==>    \
clasohm@0: \    case(c,d,u)=case(c',d',u')";
clasohm@0: by (REPEAT (resolve_tac ([refl,split_cong,cond_cong] @ prems) 1));
clasohm@0: val case_cong = result();
clasohm@0: 
clasohm@0: val major::prems = goal Sum.thy
clasohm@0:     "[| u: A+B; \
clasohm@0: \       !!x. x: A ==> c(x): C(Inl(x));   \
clasohm@0: \       !!y. y: B ==> d(y): C(Inr(y)) \
clasohm@0: \    |] ==> case(c,d,u) : C(u)";
clasohm@0: by (rtac (major RS sumE) 1);
clasohm@0: by (ALLGOALS (etac ssubst));
clasohm@0: by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
clasohm@0: 			    (prems@[case_Inl,case_Inr]))));
clasohm@0: val case_type = result();
clasohm@0: 
clasohm@0: (** Rules for the Part primitive **)
clasohm@0: 
clasohm@0: goalw Sum.thy [Part_def]
clasohm@0:     "!!a b A h. [| a : A;  a=h(b) |] ==> a : Part(A,h)";
clasohm@0: by (REPEAT (ares_tac [exI,CollectI] 1));
clasohm@0: val Part_eqI = result();
clasohm@0: 
clasohm@0: val PartI = refl RSN (2,Part_eqI);
clasohm@0: 
clasohm@0: val major::prems = goalw Sum.thy [Part_def]
clasohm@0:     "[| a : Part(A,h);  !!z. [| a : A;  a=h(z) |] ==> P  \
clasohm@0: \    |] ==> P";
clasohm@0: by (rtac (major RS CollectE) 1);
clasohm@0: by (etac exE 1);
clasohm@0: by (REPEAT (ares_tac prems 1));
clasohm@0: val PartE = result();
clasohm@0: 
clasohm@0: goalw Sum.thy [Part_def] "Part(A,h) <= A";
clasohm@0: by (rtac Collect_subset 1);
clasohm@0: val Part_subset = result();
clasohm@0: 
clasohm@0: goal Sum.thy "!!A B h. A<=B ==> Part(A,h)<=Part(B,h)";
clasohm@0: by (fast_tac (ZF_cs addIs [PartI] addSEs [PartE]) 1);
clasohm@0: val Part_mono = result();
clasohm@0: 
clasohm@0: goal Sum.thy "Part(A+B,Inl) = {Inl(x). x: A}";
clasohm@0: by (fast_tac (sum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
clasohm@0: val Part_Inl = result();
clasohm@0: 
clasohm@0: goal Sum.thy "Part(A+B,Inr) = {Inr(y). y: B}";
clasohm@0: by (fast_tac (sum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
clasohm@0: val Part_Inr = result();
clasohm@0: 
clasohm@0: goalw Sum.thy [Part_def] "!!a. a : Part(A,h) ==> a : A";
clasohm@0: by (etac CollectD1 1);
clasohm@0: val PartD1 = result();
clasohm@0: 
clasohm@0: goal Sum.thy "Part(A,%x.x) = A";
clasohm@0: by (fast_tac (ZF_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
clasohm@0: val Part_id = result();
clasohm@0: 
clasohm@0: goal Sum.thy "Part(A+B, %x.Inr(h(x))) = {Inr(y). y: Part(B,h)}";
clasohm@0: by (fast_tac (sum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
clasohm@0: val Part_Inr2 = result();
clasohm@0: 
clasohm@0: goal Sum.thy "!!A B C. C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C";
clasohm@0: by (rtac equalityI 1);
clasohm@0: by (rtac Un_least 1);
clasohm@0: by (rtac Part_subset 1);
clasohm@0: by (rtac Part_subset 1);
clasohm@0: by (fast_tac (ZF_cs addIs [PartI] addSEs [sumE]) 1);
clasohm@0: val Part_sum_equality = result();