author  lcp 
Tue, 29 Nov 1994 11:51:07 +0100  
changeset 754  521a6f3ff279 
parent 683  8fe0fbd76887 
child 760  f0200e91b272 
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); 

18 
val cardinal_eqpoll = result(); 

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); 

27 
val cardinal_eqE = result(); 

28 

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

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

31 
by (eresolve_tac [well_ord_lepoll_imp_le] 1); 

32 
by (assume_tac 1); 

33 
val lepoll_imp_le = result(); 

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); 

41 
val cadd_assoc = result(); 

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); 

49 
val cmult_assoc = result(); 

50 

51 
goal Cardinal_AC.thy "!!A. InfCard(A) ==> A*A eqpoll A"; 

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

53 
by (eresolve_tac [well_ord_InfCard_square_eq] 1); 

54 
by (assume_tac 1); 

55 
val InfCard_square_eq = result(); 

56 

57 

58 
(*** Other applications of AC ***) 

59 

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

61 
by (resolve_tac [cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll RS 

62 
lepoll_trans] 1); 

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

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

65 
val le_imp_lepoll = result(); 

66 

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

68 
by (eresolve_tac [Card_cardinal_eq RS subst] 1 THEN 

69 
rtac iffI 1 THEN 

70 
DEPTH_SOLVE (eresolve_tac [le_imp_lepoll,lepoll_imp_le] 1)); 

71 
val le_Card_iff = result(); 

72 

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

74 
by (etac CollectE 1); 

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

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

77 
by (resolve_tac [exI] 1); 

78 
by (rtac f_imp_injective 1); 

79 
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

80 
by (fast_tac (ZF_cs addDs [apply_type] addDs [Pi_memberD]) 1); 
484  81 
by (fast_tac (ZF_cs addDs [apply_type] addEs [apply_equality]) 1); 
82 
val surj_implies_inj = result(); 

83 

84 
(*Kunen's Lemma 10.20*) 

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

86 
by (resolve_tac [lepoll_imp_le] 1); 

87 
by (eresolve_tac [surj_implies_inj RS exE] 1); 

88 
by (rewtac lepoll_def); 

89 
by (eresolve_tac [exI] 1); 

90 
val surj_implies_cardinal_le = result(); 

91 

92 
(*Kunen's Lemma 10.21*) 

93 
goal Cardinal_AC.thy 

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

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

96 
by (resolve_tac [lepoll_trans] 1); 

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

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

99 
by (rewrite_goals_tac [lepoll_def]); 

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

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

102 
by (resolve_tac [exI] 1); 

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

104 
by (subgoal_tac 

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

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

107 
addSEs [LeastI, Ord_in_Ord]) 2); 

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

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

110 
lam_injective 1); 

111 
(*Instantiate the lemma proved above*) 

112 
by (ALLGOALS ball_tac); 

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

114 
addDs [apply_type]) 1); 

115 
by (dresolve_tac [apply_type] 1); 

116 
by (eresolve_tac [conjunct2] 1); 

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

118 
val cardinal_UN_le = result(); 

119 

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

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

124 
by (asm_full_simp_tac 

125 
(ZF_ss addsimps [Card_lt_csucc_iff, cardinal_UN_le, 

126 
InfCard_is_Card, Card_cardinal]) 1); 

127 
val cardinal_UN_lt_csucc = result(); 

488  128 

129 
(*The same again, for a union of ordinals*) 

130 
goal Cardinal_AC.thy 

131 
"!!K. [ InfCard(K); ALL i:K. j(i) < csucc(K) ] ==> \ 

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

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

134 
by (assume_tac 1); 

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

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

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

138 
val cardinal_UN_Ord_lt_csucc = result(); 

139 

517  140 

141 
(*Saves checking Ord(j) below*) 

142 
goal Ordinal.thy "!!i j. [ i <= j; j<k; Ord(i) ] ==> i<k"; 

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

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

145 
val lt_subset_trans = result(); 

146 

754  147 
(*The same yet again, but the index set need not be a cardinal. 
148 
Surprisingly complicated proof!*) 

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

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

153 
by (asm_simp_tac 

154 
(ZF_ss addsimps [UN_0, InfCard_is_Card, Card_is_Ord RS Card_csucc, 

155 
Card_is_Ord, Ord_0_lt_csucc]) 2); 

516  156 
by (asm_full_simp_tac 
157 
(ZF_ss addsimps [InfCard_is_Card, le_Card_iff, lepoll_def]) 1); 

517  158 
by (safe_tac eq_cs); 
159 
by (eresolve_tac [notE] 1); 

160 
by (res_inst_tac [("j1", "%i. j(if(i: range(f), converse(f)`i, x))")] 

161 
(cardinal_UN_Ord_lt_csucc RSN (2,lt_subset_trans)) 1); 

516  162 
by (assume_tac 2); 
517  163 
by (resolve_tac [UN_least] 1); 
164 
by (res_inst_tac [("x1", "f`xa")] (UN_upper RSN (2,subset_trans)) 1); 

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

166 
by (asm_simp_tac 

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

168 
by (fast_tac (ZF_cs addSIs [Ord_UN] addEs [ltE]) 2); 

169 
by (asm_simp_tac (ZF_ss addsimps [inj_converse_fun RS apply_type] 

170 
setloop split_tac [expand_if]) 1); 

171 
val le_UN_Ord_lt_csucc = result(); 

516  172 