author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 1611  35e0fd1b1775 
permissions  rwrr 
1461  1 
(* Title: ZF/Sum 
0  2 
ID: $Id$ 
1461  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1992 University of Cambridge 
5 

6 
Disjoint sums in ZermeloFraenkel Set Theory 

7 
*) 

8 

9 
open Sum; 

10 

744  11 
(*** Rules for the Part primitive ***) 
12 

13 
goalw Sum.thy [Part_def] 

14 
"a : Part(A,h) <> a:A & (EX y. a=h(y))"; 

15 
by (rtac separation 1); 

760  16 
qed "Part_iff"; 
744  17 

18 
goalw Sum.thy [Part_def] 

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

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

760  21 
qed "Part_eqI"; 
744  22 

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

24 

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

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

27 
\ ] ==> P"; 

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

29 
by (etac exE 1); 

30 
by (REPEAT (ares_tac prems 1)); 

760  31 
qed "PartE"; 
744  32 

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

34 
by (rtac Collect_subset 1); 

760  35 
qed "Part_subset"; 
744  36 

37 

38 
(*** Rules for Disjoint Sums ***) 

39 

0  40 
val sum_defs = [sum_def,Inl_def,Inr_def,case_def]; 
41 

521  42 
goalw Sum.thy (bool_def::sum_defs) "Sigma(bool,C) = C(0) + C(1)"; 
43 
by (fast_tac eq_cs 1); 

760  44 
qed "Sigma_bool"; 
521  45 

0  46 
(** Introduction rules for the injections **) 
47 

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

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

760  50 
qed "InlI"; 
0  51 

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

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

760  54 
qed "InrI"; 
0  55 

56 
(** Elimination rules **) 

57 

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

59 
"[ u: A+B; \ 

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

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

62 
\ ] ==> P"; 

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

64 
by (REPEAT (rtac refl 1 

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

760  66 
qed "sumE"; 
0  67 

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

69 

55  70 
goalw Sum.thy sum_defs "Inl(a)=Inl(b) <> a=b"; 
435  71 
by (simp_tac ZF_ss 1); 
760  72 
qed "Inl_iff"; 
0  73 

55  74 
goalw Sum.thy sum_defs "Inr(a)=Inr(b) <> a=b"; 
435  75 
by (simp_tac ZF_ss 1); 
760  76 
qed "Inr_iff"; 
0  77 

55  78 
goalw Sum.thy sum_defs "Inl(a)=Inr(b) <> False"; 
435  79 
by (simp_tac (ZF_ss addsimps [one_not_0 RS not_sym]) 1); 
760  80 
qed "Inl_Inr_iff"; 
0  81 

55  82 
goalw Sum.thy sum_defs "Inr(b)=Inl(a) <> False"; 
435  83 
by (simp_tac (ZF_ss addsimps [one_not_0]) 1); 
760  84 
qed "Inr_Inl_iff"; 
0  85 

55  86 
(*Injection and freeness rules*) 
87 

782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
773
diff
changeset

88 
bind_thm ("Inl_inject", (Inl_iff RS iffD1)); 
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
773
diff
changeset

89 
bind_thm ("Inr_inject", (Inr_iff RS iffD1)); 
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
773
diff
changeset

90 
bind_thm ("Inl_neq_Inr", (Inl_Inr_iff RS iffD1 RS FalseE)); 
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
773
diff
changeset

91 
bind_thm ("Inr_neq_Inl", (Inr_Inl_iff RS iffD1 RS FalseE)); 
55  92 

744  93 
val sum_cs = ZF_cs addSIs [PartI, InlI, InrI] 
94 
addSEs [PartE, sumE, Inl_neq_Inr, Inr_neq_Inl] 

95 
addSDs [Inl_inject, Inr_inject]; 

0  96 

55  97 
goal Sum.thy "!!A B. Inl(a): A+B ==> a: A"; 
98 
by (fast_tac sum_cs 1); 

760  99 
qed "InlD"; 
55  100 

101 
goal Sum.thy "!!A B. Inr(b): A+B ==> b: B"; 

102 
by (fast_tac sum_cs 1); 

760  103 
qed "InrD"; 
55  104 

0  105 
goal Sum.thy "u: A+B <> (EX x. x:A & u=Inl(x))  (EX y. y:B & u=Inr(y))"; 
106 
by (fast_tac sum_cs 1); 

760  107 
qed "sum_iff"; 
0  108 

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

110 
by (fast_tac sum_cs 1); 

760  111 
qed "sum_subset_iff"; 
0  112 

113 
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

114 
by (simp_tac (ZF_ss addsimps [extension,sum_subset_iff]) 1); 
0  115 
by (fast_tac ZF_cs 1); 
760  116 
qed "sum_equal_iff"; 
0  117 

521  118 

0  119 
(*** Eliminator  case ***) 
120 

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

1107  122 
by (simp_tac (ZF_ss addsimps [cond_0]) 1); 
760  123 
qed "case_Inl"; 
0  124 

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

1107  126 
by (simp_tac (ZF_ss addsimps [cond_1]) 1); 
760  127 
qed "case_Inr"; 
0  128 

129 
val major::prems = goal Sum.thy 

130 
"[ u: A+B; \ 

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

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

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

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

135 
by (ALLGOALS (etac ssubst)); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

136 
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps 
1461  137 
(prems@[case_Inl,case_Inr])))); 
760  138 
qed "case_type"; 
0  139 

435  140 
goal Sum.thy 
141 
"!!u. u: A+B ==> \ 

142 
\ R(case(c,d,u)) <> \ 

143 
\ ((ALL x:A. u = Inl(x) > R(c(x))) & \ 

144 
\ (ALL y:B. u = Inr(y) > R(d(y))))"; 

145 
by (etac sumE 1); 

146 
by (asm_simp_tac (ZF_ss addsimps [case_Inl]) 1); 

147 
by (fast_tac sum_cs 1); 

148 
by (asm_simp_tac (ZF_ss addsimps [case_Inr]) 1); 

149 
by (fast_tac sum_cs 1); 

760  150 
qed "expand_case"; 
435  151 

858  152 
val major::prems = goal Sum.thy 
1461  153 
"[ z: A+B; \ 
154 
\ !!x. x:A ==> c(x)=c'(x); \ 

155 
\ !!y. y:B ==> d(y)=d'(y) \ 

858  156 
\ ] ==> case(c,d,z) = case(c',d',z)"; 
157 
by (resolve_tac [major RS sumE] 1); 

158 
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps ([case_Inl, case_Inr] @ prems)))); 

159 
qed "case_cong"; 

160 

161 
val [major] = goal Sum.thy 

1461  162 
"z: A+B ==> \ 
858  163 
\ case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) = \ 
164 
\ case(%x. c(c'(x)), %y. d(d'(y)), z)"; 

165 
by (resolve_tac [major RS sumE] 1); 

166 
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps [case_Inl, case_Inr]))); 

167 
qed "case_case"; 

168 

773
9f8bcf1a4cff
sum_ss: moved down and added the rewrite rules for "case"
lcp
parents:
760
diff
changeset

169 
val sum_ss = ZF_ss addsimps [InlI, InrI, Inl_iff, Inr_iff, 
1461  170 
Inl_Inr_iff, Inr_Inl_iff, 
171 
case_Inl, case_Inr]; 

773
9f8bcf1a4cff
sum_ss: moved down and added the rewrite rules for "case"
lcp
parents:
760
diff
changeset

172 

9f8bcf1a4cff
sum_ss: moved down and added the rewrite rules for "case"
lcp
parents:
760
diff
changeset

173 
(*** More rules for Part(A,h) ***) 
9f8bcf1a4cff
sum_ss: moved down and added the rewrite rules for "case"
lcp
parents:
760
diff
changeset

174 

0  175 
goal Sum.thy "!!A B h. A<=B ==> Part(A,h)<=Part(B,h)"; 
744  176 
by (fast_tac sum_cs 1); 
760  177 
qed "Part_mono"; 
0  178 

744  179 
goal Sum.thy "Part(Collect(A,P), h) = Collect(Part(A,h), P)"; 
180 
by (fast_tac (sum_cs addSIs [equalityI]) 1); 

760  181 
qed "Part_Collect"; 
744  182 

803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
782
diff
changeset

183 
bind_thm ("Part_CollectE", Part_Collect RS equalityD1 RS subsetD RS CollectE); 
744  184 

0  185 
goal Sum.thy "Part(A+B,Inl) = {Inl(x). x: A}"; 
744  186 
by (fast_tac (sum_cs addIs [equalityI]) 1); 
760  187 
qed "Part_Inl"; 
0  188 

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

744  190 
by (fast_tac (sum_cs addIs [equalityI]) 1); 
760  191 
qed "Part_Inr"; 
0  192 

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

194 
by (etac CollectD1 1); 

760  195 
qed "PartD1"; 
0  196 

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

744  198 
by (fast_tac (sum_cs addIs [equalityI]) 1); 
760  199 
qed "Part_id"; 
0  200 

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

744  202 
by (fast_tac (sum_cs addIs [equalityI]) 1); 
760  203 
qed "Part_Inr2"; 
0  204 

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

744  206 
by (fast_tac (sum_cs addIs [equalityI]) 1); 
760  207 
qed "Part_sum_equality"; 