0

1 
(* Title: ZF/sum


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1992 University of Cambridge


5 


6 
Disjoint sums in ZermeloFraenkel Set Theory


7 
*)


8 


9 
open Sum;


10 


11 
val sum_defs = [sum_def,Inl_def,Inr_def,case_def];


12 


13 
(** Introduction rules for the injections **)


14 


15 
goalw Sum.thy sum_defs "!!a A B. a : A ==> Inl(a) : A+B";


16 
by (REPEAT (ares_tac [UnI1,SigmaI,singletonI] 1));


17 
val InlI = result();


18 


19 
goalw Sum.thy sum_defs "!!b A B. b : B ==> Inr(b) : A+B";


20 
by (REPEAT (ares_tac [UnI2,SigmaI,singletonI] 1));


21 
val InrI = result();


22 


23 
(** Elimination rules **)


24 


25 
val major::prems = goalw Sum.thy sum_defs


26 
"[ u: A+B; \


27 
\ !!x. [ x:A; u=Inl(x) ] ==> P; \


28 
\ !!y. [ y:B; u=Inr(y) ] ==> P \


29 
\ ] ==> P";


30 
by (rtac (major RS UnE) 1);


31 
by (REPEAT (rtac refl 1


32 
ORELSE eresolve_tac (prems@[SigmaE,singletonE,ssubst]) 1));


33 
val sumE = result();


34 


35 
(** Injection and freeness rules **)


36 


37 
val [major] = goalw Sum.thy sum_defs "Inl(a)=Inl(b) ==> a=b";


38 
by (EVERY1 [rtac (major RS Pair_inject), assume_tac]);


39 
val Inl_inject = result();


40 


41 
val [major] = goalw Sum.thy sum_defs "Inr(a)=Inr(b) ==> a=b";


42 
by (EVERY1 [rtac (major RS Pair_inject), assume_tac]);


43 
val Inr_inject = result();


44 


45 
val [major] = goalw Sum.thy sum_defs "Inl(a)=Inr(b) ==> P";


46 
by (rtac (major RS Pair_inject) 1);


47 
by (etac (sym RS one_neq_0) 1);


48 
val Inl_neq_Inr = result();


49 


50 
val Inr_neq_Inl = sym RS Inl_neq_Inr;


51 


52 
(** Injection and freeness equivalences, for rewriting **)


53 


54 
goal Sum.thy "Inl(a)=Inl(b) <> a=b";


55 
by (rtac iffI 1);


56 
by (REPEAT (eresolve_tac [Inl_inject,subst_context] 1));


57 
val Inl_iff = result();


58 


59 
goal Sum.thy "Inr(a)=Inr(b) <> a=b";


60 
by (rtac iffI 1);


61 
by (REPEAT (eresolve_tac [Inr_inject,subst_context] 1));


62 
val Inr_iff = result();


63 


64 
goal Sum.thy "Inl(a)=Inr(b) <> False";


65 
by (rtac iffI 1);


66 
by (REPEAT (eresolve_tac [Inl_neq_Inr,FalseE] 1));


67 
val Inl_Inr_iff = result();


68 


69 
goal Sum.thy "Inr(b)=Inl(a) <> False";


70 
by (rtac iffI 1);


71 
by (REPEAT (eresolve_tac [Inr_neq_Inl,FalseE] 1));


72 
val Inr_Inl_iff = result();


73 


74 
val sum_cs = ZF_cs addIs [InlI,InrI] addSEs [sumE,Inl_neq_Inr,Inr_neq_Inl]


75 
addSDs [Inl_inject,Inr_inject];


76 


77 
goal Sum.thy "u: A+B <> (EX x. x:A & u=Inl(x))  (EX y. y:B & u=Inr(y))";


78 
by (fast_tac sum_cs 1);


79 
val sum_iff = result();


80 


81 
goal Sum.thy "A+B <= C+D <> A<=C & B<=D";


82 
by (fast_tac sum_cs 1);


83 
val sum_subset_iff = result();


84 


85 
goal Sum.thy "A+B = C+D <> A=C & B=D";


86 
by (SIMP_TAC (ZF_ss addrews [extension,sum_subset_iff]) 1);


87 
by (fast_tac ZF_cs 1);


88 
val sum_equal_iff = result();


89 


90 
(*** Eliminator  case ***)


91 


92 
goalw Sum.thy sum_defs "case(c, d, Inl(a)) = c(a)";


93 
by (rtac (split RS trans) 1);


94 
by (rtac cond_0 1);


95 
val case_Inl = result();


96 


97 
goalw Sum.thy sum_defs "case(c, d, Inr(b)) = d(b)";


98 
by (rtac (split RS trans) 1);


99 
by (rtac cond_1 1);


100 
val case_Inr = result();


101 


102 
val prems = goalw Sum.thy [case_def]


103 
"[ u=u'; !!x. c(x)=c'(x); !!y. d(y)=d'(y) ] ==> \


104 
\ case(c,d,u)=case(c',d',u')";


105 
by (REPEAT (resolve_tac ([refl,split_cong,cond_cong] @ prems) 1));


106 
val case_cong = result();


107 


108 
val major::prems = goal Sum.thy


109 
"[ u: A+B; \


110 
\ !!x. x: A ==> c(x): C(Inl(x)); \


111 
\ !!y. y: B ==> d(y): C(Inr(y)) \


112 
\ ] ==> case(c,d,u) : C(u)";


113 
by (rtac (major RS sumE) 1);


114 
by (ALLGOALS (etac ssubst));


115 
by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews


116 
(prems@[case_Inl,case_Inr]))));


117 
val case_type = result();


118 


119 
(** Rules for the Part primitive **)


120 


121 
goalw Sum.thy [Part_def]


122 
"!!a b A h. [ a : A; a=h(b) ] ==> a : Part(A,h)";


123 
by (REPEAT (ares_tac [exI,CollectI] 1));


124 
val Part_eqI = result();


125 


126 
val PartI = refl RSN (2,Part_eqI);


127 


128 
val major::prems = goalw Sum.thy [Part_def]


129 
"[ a : Part(A,h); !!z. [ a : A; a=h(z) ] ==> P \


130 
\ ] ==> P";


131 
by (rtac (major RS CollectE) 1);


132 
by (etac exE 1);


133 
by (REPEAT (ares_tac prems 1));


134 
val PartE = result();


135 


136 
goalw Sum.thy [Part_def] "Part(A,h) <= A";


137 
by (rtac Collect_subset 1);


138 
val Part_subset = result();


139 


140 
goal Sum.thy "!!A B h. A<=B ==> Part(A,h)<=Part(B,h)";


141 
by (fast_tac (ZF_cs addIs [PartI] addSEs [PartE]) 1);


142 
val Part_mono = result();


143 


144 
goal Sum.thy "Part(A+B,Inl) = {Inl(x). x: A}";


145 
by (fast_tac (sum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);


146 
val Part_Inl = result();


147 


148 
goal Sum.thy "Part(A+B,Inr) = {Inr(y). y: B}";


149 
by (fast_tac (sum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);


150 
val Part_Inr = result();


151 


152 
goalw Sum.thy [Part_def] "!!a. a : Part(A,h) ==> a : A";


153 
by (etac CollectD1 1);


154 
val PartD1 = result();


155 


156 
goal Sum.thy "Part(A,%x.x) = A";


157 
by (fast_tac (ZF_cs addIs [PartI,equalityI] addSEs [PartE]) 1);


158 
val Part_id = result();


159 


160 
goal Sum.thy "Part(A+B, %x.Inr(h(x))) = {Inr(y). y: Part(B,h)}";


161 
by (fast_tac (sum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);


162 
val Part_Inr2 = result();


163 


164 
goal Sum.thy "!!A B C. C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C";


165 
by (rtac equalityI 1);


166 
by (rtac Un_least 1);


167 
by (rtac Part_subset 1);


168 
by (rtac Part_subset 1);


169 
by (fast_tac (ZF_cs addIs [PartI] addSEs [sumE]) 1);


170 
val Part_sum_equality = result();
