author | paulson |
Fri, 11 Aug 2000 13:26:40 +0200 | |
changeset 9577 | 9e66e8ed8237 |
parent 55 | 331d93292ee0 |
permissions | -rw-r--r-- |
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 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 |
||
55 | 37 |
goalw Sum.thy sum_defs "Inl(a)=Inl(b) <-> a=b"; |
38 |
by (simp_tac (ZF_ss addsimps [Pair_iff]) 1); |
|
0 | 39 |
val Inl_iff = result(); |
40 |
||
55 | 41 |
goalw Sum.thy sum_defs "Inr(a)=Inr(b) <-> a=b"; |
42 |
by (simp_tac (ZF_ss addsimps [Pair_iff]) 1); |
|
0 | 43 |
val Inr_iff = result(); |
44 |
||
55 | 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); |
|
0 | 47 |
val Inl_Inr_iff = result(); |
48 |
||
55 | 49 |
goalw Sum.thy sum_defs "Inr(b)=Inl(a) <-> False"; |
50 |
by (simp_tac (ZF_ss addsimps [Pair_iff, one_not_0]) 1); |
|
0 | 51 |
val Inr_Inl_iff = result(); |
52 |
||
55 | 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] |
|
0 | 61 |
addSDs [Inl_inject,Inr_inject]; |
62 |
||
55 | 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 |
||
0 | 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"; |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
80 |
by (simp_tac (ZF_ss addsimps [extension,sum_subset_iff]) 1); |
0 | 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)); |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
103 |
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps |
0 | 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(); |