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 Zermelo-Fraenkel 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 equivalences, for rewriting **) |
|
36 |
|
37 goalw Sum.thy sum_defs "Inl(a)=Inl(b) <-> a=b"; |
|
38 by (simp_tac (ZF_ss addsimps [Pair_iff]) 1); |
|
39 val Inl_iff = result(); |
|
40 |
|
41 goalw Sum.thy sum_defs "Inr(a)=Inr(b) <-> a=b"; |
|
42 by (simp_tac (ZF_ss addsimps [Pair_iff]) 1); |
|
43 val Inr_iff = result(); |
|
44 |
|
45 goalw Sum.thy sum_defs "Inl(a)=Inr(b) <-> False"; |
|
46 by (simp_tac (ZF_ss addsimps [Pair_iff, one_not_0 RS not_sym]) 1); |
|
47 val Inl_Inr_iff = result(); |
|
48 |
|
49 goalw Sum.thy sum_defs "Inr(b)=Inl(a) <-> False"; |
|
50 by (simp_tac (ZF_ss addsimps [Pair_iff, one_not_0]) 1); |
|
51 val Inr_Inl_iff = result(); |
|
52 |
|
53 (*Injection and freeness rules*) |
|
54 |
|
55 val Inl_inject = standard (Inl_iff RS iffD1); |
|
56 val Inr_inject = standard (Inr_iff RS iffD1); |
|
57 val Inl_neq_Inr = standard (Inl_Inr_iff RS iffD1 RS FalseE); |
|
58 val Inr_neq_Inl = standard (Inr_Inl_iff RS iffD1 RS FalseE); |
|
59 |
|
60 val sum_cs = ZF_cs addSIs [InlI,InrI] addSEs [sumE,Inl_neq_Inr,Inr_neq_Inl] |
|
61 addSDs [Inl_inject,Inr_inject]; |
|
62 |
|
63 goal Sum.thy "!!A B. Inl(a): A+B ==> a: A"; |
|
64 by (fast_tac sum_cs 1); |
|
65 val InlD = result(); |
|
66 |
|
67 goal Sum.thy "!!A B. Inr(b): A+B ==> b: B"; |
|
68 by (fast_tac sum_cs 1); |
|
69 val InrD = result(); |
|
70 |
|
71 goal Sum.thy "u: A+B <-> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))"; |
|
72 by (fast_tac sum_cs 1); |
|
73 val sum_iff = result(); |
|
74 |
|
75 goal Sum.thy "A+B <= C+D <-> A<=C & B<=D"; |
|
76 by (fast_tac sum_cs 1); |
|
77 val sum_subset_iff = result(); |
|
78 |
|
79 goal Sum.thy "A+B = C+D <-> A=C & B=D"; |
|
80 by (simp_tac (ZF_ss addsimps [extension,sum_subset_iff]) 1); |
|
81 by (fast_tac ZF_cs 1); |
|
82 val sum_equal_iff = result(); |
|
83 |
|
84 (*** Eliminator -- case ***) |
|
85 |
|
86 goalw Sum.thy sum_defs "case(c, d, Inl(a)) = c(a)"; |
|
87 by (rtac (split RS trans) 1); |
|
88 by (rtac cond_0 1); |
|
89 val case_Inl = result(); |
|
90 |
|
91 goalw Sum.thy sum_defs "case(c, d, Inr(b)) = d(b)"; |
|
92 by (rtac (split RS trans) 1); |
|
93 by (rtac cond_1 1); |
|
94 val case_Inr = result(); |
|
95 |
|
96 val major::prems = goal Sum.thy |
|
97 "[| u: A+B; \ |
|
98 \ !!x. x: A ==> c(x): C(Inl(x)); \ |
|
99 \ !!y. y: B ==> d(y): C(Inr(y)) \ |
|
100 \ |] ==> case(c,d,u) : C(u)"; |
|
101 by (rtac (major RS sumE) 1); |
|
102 by (ALLGOALS (etac ssubst)); |
|
103 by (ALLGOALS (asm_simp_tac (ZF_ss addsimps |
|
104 (prems@[case_Inl,case_Inr])))); |
|
105 val case_type = result(); |
|
106 |
|
107 (** Rules for the Part primitive **) |
|
108 |
|
109 goalw Sum.thy [Part_def] |
|
110 "!!a b A h. [| a : A; a=h(b) |] ==> a : Part(A,h)"; |
|
111 by (REPEAT (ares_tac [exI,CollectI] 1)); |
|
112 val Part_eqI = result(); |
|
113 |
|
114 val PartI = refl RSN (2,Part_eqI); |
|
115 |
|
116 val major::prems = goalw Sum.thy [Part_def] |
|
117 "[| a : Part(A,h); !!z. [| a : A; a=h(z) |] ==> P \ |
|
118 \ |] ==> P"; |
|
119 by (rtac (major RS CollectE) 1); |
|
120 by (etac exE 1); |
|
121 by (REPEAT (ares_tac prems 1)); |
|
122 val PartE = result(); |
|
123 |
|
124 goalw Sum.thy [Part_def] "Part(A,h) <= A"; |
|
125 by (rtac Collect_subset 1); |
|
126 val Part_subset = result(); |
|
127 |
|
128 goal Sum.thy "!!A B h. A<=B ==> Part(A,h)<=Part(B,h)"; |
|
129 by (fast_tac (ZF_cs addIs [PartI] addSEs [PartE]) 1); |
|
130 val Part_mono = result(); |
|
131 |
|
132 goal Sum.thy "Part(A+B,Inl) = {Inl(x). x: A}"; |
|
133 by (fast_tac (sum_cs addIs [PartI,equalityI] addSEs [PartE]) 1); |
|
134 val Part_Inl = result(); |
|
135 |
|
136 goal Sum.thy "Part(A+B,Inr) = {Inr(y). y: B}"; |
|
137 by (fast_tac (sum_cs addIs [PartI,equalityI] addSEs [PartE]) 1); |
|
138 val Part_Inr = result(); |
|
139 |
|
140 goalw Sum.thy [Part_def] "!!a. a : Part(A,h) ==> a : A"; |
|
141 by (etac CollectD1 1); |
|
142 val PartD1 = result(); |
|
143 |
|
144 goal Sum.thy "Part(A,%x.x) = A"; |
|
145 by (fast_tac (ZF_cs addIs [PartI,equalityI] addSEs [PartE]) 1); |
|
146 val Part_id = result(); |
|
147 |
|
148 goal Sum.thy "Part(A+B, %x.Inr(h(x))) = {Inr(y). y: Part(B,h)}"; |
|
149 by (fast_tac (sum_cs addIs [PartI,equalityI] addSEs [PartE]) 1); |
|
150 val Part_Inr2 = result(); |
|
151 |
|
152 goal Sum.thy "!!A B C. C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C"; |
|
153 by (rtac equalityI 1); |
|
154 by (rtac Un_least 1); |
|
155 by (rtac Part_subset 1); |
|
156 by (rtac Part_subset 1); |
|
157 by (fast_tac (ZF_cs addIs [PartI] addSEs [sumE]) 1); |
|
158 val Part_sum_equality = result(); |
|