author  lcp 
Wed, 11 Jan 1995 18:42:06 +0100  
changeset 847  e50a32a4f669 
parent 785  c2ef808dc938 
child 1092  fdaf39a47a2b 
permissions  rwrr 
484  1 
(* Title: ZF/Cardinal_AC.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1994 University of Cambridge 

5 

6 
Cardinal arithmetic WITH the Axiom of Choice 

517  7 

8 
These results help justify infinitebranching datatypes 

484  9 
*) 
10 

11 
open Cardinal_AC; 

12 

13 
(*** Strengthened versions of existing theorems about cardinals ***) 

14 

15 
goal Cardinal_AC.thy "A eqpoll A"; 

16 
by (resolve_tac [AC_well_ord RS exE] 1); 

17 
by (eresolve_tac [well_ord_cardinal_eqpoll] 1); 

760  18 
qed "cardinal_eqpoll"; 
484  19 

20 
val cardinal_idem = cardinal_eqpoll RS cardinal_cong; 

21 

22 
goal Cardinal_AC.thy "!!X Y. X = Y ==> X eqpoll Y"; 

23 
by (resolve_tac [AC_well_ord RS exE] 1); 

24 
by (resolve_tac [AC_well_ord RS exE] 1); 

25 
by (resolve_tac [well_ord_cardinal_eqE] 1); 

26 
by (REPEAT_SOME assume_tac); 

760  27 
qed "cardinal_eqE"; 
484  28 

29 
goal Cardinal_AC.thy "!!A B. A lepoll B ==> A le B"; 

30 
by (resolve_tac [AC_well_ord RS exE] 1); 

766  31 
by (eresolve_tac [well_ord_lepoll_imp_Card_le] 1); 
484  32 
by (assume_tac 1); 
766  33 
qed "lepoll_imp_Card_le"; 
484  34 

35 
goal Cardinal_AC.thy "(i + j) + k = i + (j + k)"; 

36 
by (resolve_tac [AC_well_ord RS exE] 1); 

37 
by (resolve_tac [AC_well_ord RS exE] 1); 

38 
by (resolve_tac [AC_well_ord RS exE] 1); 

39 
by (resolve_tac [well_ord_cadd_assoc] 1); 

40 
by (REPEAT_SOME assume_tac); 

760  41 
qed "cadd_assoc"; 
484  42 

43 
goal Cardinal_AC.thy "(i * j) * k = i * (j * k)"; 

44 
by (resolve_tac [AC_well_ord RS exE] 1); 

45 
by (resolve_tac [AC_well_ord RS exE] 1); 

46 
by (resolve_tac [AC_well_ord RS exE] 1); 

47 
by (resolve_tac [well_ord_cmult_assoc] 1); 

48 
by (REPEAT_SOME assume_tac); 

760  49 
qed "cmult_assoc"; 
484  50 

847  51 
goal Cardinal_AC.thy "(i + j) * k = (i * k) + (j * k)"; 
52 
by (resolve_tac [AC_well_ord RS exE] 1); 

53 
by (resolve_tac [AC_well_ord RS exE] 1); 

54 
by (resolve_tac [AC_well_ord RS exE] 1); 

55 
by (resolve_tac [well_ord_cadd_cmult_distrib] 1); 

56 
by (REPEAT_SOME assume_tac); 

57 
qed "cadd_cmult_distrib"; 

58 

484  59 
goal Cardinal_AC.thy "!!A. InfCard(A) ==> A*A eqpoll A"; 
60 
by (resolve_tac [AC_well_ord RS exE] 1); 

61 
by (eresolve_tac [well_ord_InfCard_square_eq] 1); 

62 
by (assume_tac 1); 

760  63 
qed "InfCard_square_eq"; 
484  64 

65 

66 
(*** Other applications of AC ***) 

67 

68 
goal Cardinal_AC.thy "!!A B. A le B ==> A lepoll B"; 

69 
by (resolve_tac [cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll RS 

70 
lepoll_trans] 1); 

71 
by (eresolve_tac [le_imp_subset RS subset_imp_lepoll RS lepoll_trans] 1); 

72 
by (resolve_tac [cardinal_eqpoll RS eqpoll_imp_lepoll] 1); 

766  73 
qed "Card_le_imp_lepoll"; 
484  74 

75 
goal Cardinal_AC.thy "!!A K. Card(K) ==> A le K <> A lepoll K"; 

76 
by (eresolve_tac [Card_cardinal_eq RS subst] 1 THEN 

77 
rtac iffI 1 THEN 

766  78 
DEPTH_SOLVE (eresolve_tac [Card_le_imp_lepoll,lepoll_imp_Card_le] 1)); 
760  79 
qed "le_Card_iff"; 
484  80 

81 
goalw Cardinal_AC.thy [surj_def] "!!f. f: surj(X,Y) ==> EX g. g: inj(Y,X)"; 

82 
by (etac CollectE 1); 

83 
by (res_inst_tac [("A1", "Y"), ("B1", "%y. f``{y}")] (AC_Pi RS exE) 1); 

84 
by (fast_tac (ZF_cs addSEs [apply_Pair]) 1); 

85 
by (resolve_tac [exI] 1); 

86 
by (rtac f_imp_injective 1); 

87 
by (resolve_tac [Pi_type] 1 THEN assume_tac 1); 

683
8fe0fbd76887
Cardinal_AC/surj_implies_inj: uses Pi_memberD instead of memberPiE
lcp
parents:
517
diff
changeset

88 
by (fast_tac (ZF_cs addDs [apply_type] addDs [Pi_memberD]) 1); 
484  89 
by (fast_tac (ZF_cs addDs [apply_type] addEs [apply_equality]) 1); 
760  90 
qed "surj_implies_inj"; 
484  91 

92 
(*Kunen's Lemma 10.20*) 

93 
goal Cardinal_AC.thy "!!f. f: surj(X,Y) ==> Y le X"; 

766  94 
by (resolve_tac [lepoll_imp_Card_le] 1); 
484  95 
by (eresolve_tac [surj_implies_inj RS exE] 1); 
96 
by (rewtac lepoll_def); 

97 
by (eresolve_tac [exI] 1); 

760  98 
qed "surj_implies_cardinal_le"; 
484  99 

100 
(*Kunen's Lemma 10.21*) 

101 
goal Cardinal_AC.thy 

102 
"!!K. [ InfCard(K); ALL i:K. X(i) le K ] ==> UN i:K. X(i) le K"; 

103 
by (asm_full_simp_tac (ZF_ss addsimps [InfCard_is_Card, le_Card_iff]) 1); 

104 
by (resolve_tac [lepoll_trans] 1); 

105 
by (resolve_tac [InfCard_square_eq RS eqpoll_imp_lepoll] 2); 

106 
by (asm_simp_tac (ZF_ss addsimps [InfCard_is_Card, Card_cardinal_eq]) 2); 

107 
by (rewrite_goals_tac [lepoll_def]); 

108 
by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1); 

109 
by (etac (AC_ball_Pi RS exE) 1); 

110 
by (resolve_tac [exI] 1); 

111 
(*Lemma needed in both subgoals, for a fixed z*) 

112 
by (subgoal_tac 

113 
"ALL z: (UN i:K. X(i)). z: X(LEAST i. z:X(i)) & (LEAST i. z:X(i)) : K" 1); 

114 
by (fast_tac (ZF_cs addSIs [Least_le RS lt_trans1 RS ltD, ltI] 

115 
addSEs [LeastI, Ord_in_Ord]) 2); 

116 
by (res_inst_tac [("c", "%z. <LEAST i. z:X(i), f ` (LEAST i. z:X(i)) ` z>"), 

117 
("d", "split(%i j. converse(f`i) ` j)")] 

118 
lam_injective 1); 

119 
(*Instantiate the lemma proved above*) 

120 
by (ALLGOALS ball_tac); 

121 
by (fast_tac (ZF_cs addEs [inj_is_fun RS apply_type] 

122 
addDs [apply_type]) 1); 

123 
by (dresolve_tac [apply_type] 1); 

124 
by (eresolve_tac [conjunct2] 1); 

125 
by (asm_simp_tac (ZF_ss addsimps [left_inverse]) 1); 

760  126 
qed "cardinal_UN_le"; 
484  127 

488  128 
(*The same again, using csucc*) 
484  129 
goal Cardinal_AC.thy 
130 
"!!K. [ InfCard(K); ALL i:K. X(i) < csucc(K) ] ==> \ 

131 
\ UN i:K. X(i) < csucc(K)"; 

132 
by (asm_full_simp_tac 

133 
(ZF_ss addsimps [Card_lt_csucc_iff, cardinal_UN_le, 

134 
InfCard_is_Card, Card_cardinal]) 1); 

760  135 
qed "cardinal_UN_lt_csucc"; 
488  136 

785  137 
(*The same again, for a union of ordinals. In use, j(i) is a bit like rank(i), 
138 
the least ordinal j such that i:Vfrom(A,j). *) 

488  139 
goal Cardinal_AC.thy 
140 
"!!K. [ InfCard(K); ALL i:K. j(i) < csucc(K) ] ==> \ 

141 
\ (UN i:K. j(i)) < csucc(K)"; 

142 
by (resolve_tac [cardinal_UN_lt_csucc RS Card_lt_imp_lt] 1); 

143 
by (assume_tac 1); 

144 
by (fast_tac (ZF_cs addIs [Ord_cardinal_le RS lt_trans1] addEs [ltE]) 1); 

145 
by (fast_tac (ZF_cs addSIs [Ord_UN] addEs [ltE]) 1); 

146 
by (eresolve_tac [InfCard_is_Card RS Card_is_Ord RS Card_csucc] 1); 

760  147 
qed "cardinal_UN_Ord_lt_csucc"; 
488  148 

517  149 

785  150 
(** Main result for infinitebranching datatypes. As above, but the index 
151 
set need not be a cardinal. Surprisingly complicated proof! 

152 
**) 

153 

517  154 
(*Saves checking Ord(j) below*) 
155 
goal Ordinal.thy "!!i j. [ i <= j; j<k; Ord(i) ] ==> i<k"; 

156 
by (resolve_tac [subset_imp_le RS lt_trans1] 1); 

157 
by (REPEAT (eresolve_tac [asm_rl, ltE] 1)); 

760  158 
qed "lt_subset_trans"; 
517  159 

785  160 
(*Work backwards along the injection from W into K, given that W~=0.*) 
161 
goal Perm.thy 

162 
"!!A. [ f: inj(A,B); a:A ] ==> \ 

163 
\ (UN x:A. C(x)) <= (UN y:B. C(if(y: range(f), converse(f)`y, a)))"; 

164 
by (resolve_tac [UN_least] 1); 

165 
by (res_inst_tac [("x1", "f`x")] (UN_upper RSN (2,subset_trans)) 1); 

166 
by (eresolve_tac [inj_is_fun RS apply_type] 2 THEN assume_tac 2); 

167 
by (asm_simp_tac 

168 
(ZF_ss addsimps [inj_is_fun RS apply_rangeI, left_inverse]) 1); 

169 
val inj_UN_subset = result(); 

170 

171 
(*Simpler to require W=K; we'd have a bijection; but the theorem would 

172 
be weaker.*) 

516  173 
goal Cardinal_AC.thy 
517  174 
"!!K. [ InfCard(K); W le K; ALL w:W. j(w) < csucc(K) ] ==> \ 
175 
\ (UN w:W. j(w)) < csucc(K)"; 

176 
by (excluded_middle_tac "W=0" 1); 

785  177 
by (asm_simp_tac (*solve the easy 0 case*) 
517  178 
(ZF_ss addsimps [UN_0, InfCard_is_Card, Card_is_Ord RS Card_csucc, 
179 
Card_is_Ord, Ord_0_lt_csucc]) 2); 

516  180 
by (asm_full_simp_tac 
181 
(ZF_ss addsimps [InfCard_is_Card, le_Card_iff, lepoll_def]) 1); 

517  182 
by (safe_tac eq_cs); 
785  183 
by (swap_res_tac [[inj_UN_subset, cardinal_UN_Ord_lt_csucc] 
184 
MRS lt_subset_trans] 1); 

185 
by (REPEAT (assume_tac 1)); 

517  186 
by (fast_tac (ZF_cs addSIs [Ord_UN] addEs [ltE]) 2); 
187 
by (asm_simp_tac (ZF_ss addsimps [inj_converse_fun RS apply_type] 

188 
setloop split_tac [expand_if]) 1); 

760  189 
qed "le_UN_Ord_lt_csucc"; 
516  190 