author  paulson 
Wed, 08 May 2002 10:12:57 +0200  
changeset 13118  336b0bcbd27c 
parent 12820  02e2ff3e4d37 
child 13161  a40db0418145 
permissions  rwrr 
1478  1 
(* Title: ZF/CardinalArith.thy 
437  2 
ID: $Id$ 
1478  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
437  4 
Copyright 1994 University of Cambridge 
5 

6 
Cardinal Arithmetic 

7 
*) 

8 

12667  9 
theory CardinalArith = Cardinal + OrderArith + ArithSimp + Finite: 
467  10 

12667  11 
constdefs 
437  12 

12667  13 
InfCard :: "i=>o" 
14 
"InfCard(i) == Card(i) & nat le i" 

437  15 

12667  16 
cmult :: "[i,i]=>i" (infixl "*" 70) 
17 
"i * j == i*j" 

18 

19 
cadd :: "[i,i]=>i" (infixl "+" 65) 

20 
"i + j == i+j" 

437  21 

12667  22 
csquare_rel :: "i=>i" 
23 
"csquare_rel(K) == 

24 
rvimage(K*K, 

25 
lam <x,y>:K*K. <x Un y, x, y>, 

26 
rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))" 

437  27 

484  28 
(*This def is more complex than Kunen's but it more easily proved to 
29 
be a cardinal*) 

12667  30 
jump_cardinal :: "i=>i" 
31 
"jump_cardinal(K) == 

1155  32 
UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}" 
12667  33 

484  34 
(*needed because jump_cardinal(K) might not be the successor of K*) 
12667  35 
csucc :: "i=>i" 
36 
"csucc(K) == LEAST L. Card(L) & K<L" 

484  37 

12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
9964
diff
changeset

38 
syntax (xsymbols) 
12667  39 
"op +" :: "[i,i] => i" (infixl "\<oplus>" 65) 
40 
"op *" :: "[i,i] => i" (infixl "\<otimes>" 70) 

41 

42 

13118  43 
(*** The following really belong early in the development ***) 
44 

45 
lemma relation_converse_converse [simp]: 

46 
"relation(r) ==> converse(converse(r)) = r" 

47 
by (simp add: relation_def, blast) 

48 

49 
lemma relation_restrict [simp]: "relation(restrict(r,A))" 

50 
by (simp add: restrict_def relation_def, blast) 

51 

52 
(*** The following really belong in Order ***) 

53 

54 
lemma subset_ord_iso_Memrel: 

55 
"\<lbrakk>f: ord_iso(A,Memrel(B),C,r); A<=B\<rbrakk> \<Longrightarrow> f: ord_iso(A,Memrel(A),C,r)" 

56 
apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN fun_is_rel]) 

57 
apply (frule ord_iso_trans [OF id_ord_iso_Memrel], assumption) 

58 
apply (simp add: right_comp_id) 

59 
done 

60 

61 
lemma restrict_ord_iso: 

62 
"\<lbrakk>f \<in> ord_iso(i, Memrel(i), Order.pred(A,a,r), r); a \<in> A; j < i; 

63 
trans[A](r)\<rbrakk> 

64 
\<Longrightarrow> restrict(f,j) \<in> ord_iso(j, Memrel(j), Order.pred(A,f`j,r), r)" 

65 
apply (frule ltD) 

66 
apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption) 

67 
apply (frule ord_iso_restrict_pred, assumption) 

68 
apply (simp add: pred_iff trans_pred_pred_eq lt_pred_Memrel) 

69 
apply (blast intro!: subset_ord_iso_Memrel le_imp_subset [OF leI]) 

70 
done 

71 

72 
lemma restrict_ord_iso2: 

73 
"\<lbrakk>f \<in> ord_iso(Order.pred(A,a,r), r, i, Memrel(i)); a \<in> A; 

74 
j < i; trans[A](r)\<rbrakk> 

75 
\<Longrightarrow> converse(restrict(converse(f), j)) 

76 
\<in> ord_iso(Order.pred(A, converse(f)`j, r), r, j, Memrel(j))" 

77 
by (blast intro: restrict_ord_iso ord_iso_sym ltI) 

78 

12667  79 
(*** The following really belong in OrderType ***) 
80 

81 
lemma oadd_eq_0_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> (i ++ j) = 0 <> i=0 & j=0" 

82 
apply (erule trans_induct3 [of j]) 

83 
apply (simp_all add: oadd_Limit) 

12820  84 
apply (simp add: Union_empty_iff Limit_def lt_def, blast) 
12667  85 
done 
86 

87 
lemma oadd_eq_lt_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> 0 < (i ++ j) <> 0<i  0<j" 

88 
by (simp add: Ord_0_lt_iff [symmetric] oadd_eq_0_iff) 

89 

90 
lemma oadd_lt_self: "[ Ord(i); 0<j ] ==> i < i++j" 

91 
apply (rule lt_trans2) 

92 
apply (erule le_refl) 

93 
apply (simp only: lt_Ord2 oadd_1 [of i, symmetric]) 

94 
apply (blast intro: succ_leI oadd_le_mono) 

95 
done 

96 

97 
lemma oadd_LimitI: "\<lbrakk>Ord(i); Limit(j)\<rbrakk> \<Longrightarrow> Limit(i ++ j)" 

98 
apply (simp add: oadd_Limit) 

99 
apply (frule Limit_has_1 [THEN ltD]) 

100 
apply (rule increasing_LimitI) 

101 
apply (rule Ord_0_lt) 

102 
apply (blast intro: Ord_in_Ord [OF Limit_is_Ord]) 

103 
apply (force simp add: Union_empty_iff oadd_eq_0_iff 

12820  104 
Limit_is_Ord [of j, THEN Ord_in_Ord], auto) 
12667  105 
apply (rule_tac x="succ(x)" in bexI) 
106 
apply (simp add: ltI Limit_is_Ord [of j, THEN Ord_in_Ord]) 

107 
apply (simp add: Limit_def lt_def) 

108 
done 

109 

110 
(*** The following really belong in Cardinal ***) 

111 

112 
lemma lesspoll_not_refl: "~ (i lesspoll i)" 

113 
by (simp add: lesspoll_def) 

114 

115 
lemma lesspoll_irrefl [elim!]: "i lesspoll i ==> P" 

116 
by (simp add: lesspoll_def) 

117 

118 
lemma Card_Union [simp,intro,TC]: "(ALL x:A. Card(x)) ==> Card(Union(A))" 

119 
apply (rule CardI) 

120 
apply (simp add: Card_is_Ord) 

121 
apply (clarify dest!: ltD) 

122 
apply (drule bspec, assumption) 

123 
apply (frule lt_Card_imp_lesspoll, blast intro: ltI Card_is_Ord) 

124 
apply (drule eqpoll_sym [THEN eqpoll_imp_lepoll]) 

125 
apply (drule lesspoll_trans1, assumption) 

126 
apply (subgoal_tac "B lepoll \<Union>A") 

127 
apply (drule lesspoll_trans1, assumption, blast) 

128 
apply (blast intro: subset_imp_lepoll) 

129 
done 

130 

131 
lemma Card_UN: 

132 
"(!!x. x:A ==> Card(K(x))) ==> Card(UN x:A. K(x))" 

133 
by (blast intro: Card_Union) 

134 

135 
lemma Card_OUN [simp,intro,TC]: 

136 
"(!!x. x:A ==> Card(K(x))) ==> Card(UN x<A. K(x))" 

137 
by (simp add: OUnion_def Card_0) 

9654
9754ba005b64
Xsymbols for ordinal, cardinal, integer arithmetic
paulson
parents:
9548
diff
changeset

138 

12776  139 
lemma n_lesspoll_nat: "n \<in> nat ==> n \<prec> nat" 
140 
apply (unfold lesspoll_def) 

141 
apply (rule conjI) 

142 
apply (erule OrdmemD [THEN subset_imp_lepoll], rule Ord_nat) 

143 
apply (rule notI) 

144 
apply (erule eqpollE) 

145 
apply (rule succ_lepoll_natE) 

146 
apply (blast intro: nat_succI [THEN OrdmemD, THEN subset_imp_lepoll] 

12820  147 
lepoll_trans, assumption) 
12776  148 
done 
149 

150 
lemma in_Card_imp_lesspoll: "[ Card(K); b \<in> K ] ==> b \<prec> K" 

151 
apply (unfold lesspoll_def) 

152 
apply (simp add: Card_iff_initial) 

153 
apply (fast intro!: le_imp_lepoll ltI leI) 

154 
done 

155 

156 
lemma succ_lepoll_imp_not_empty: "succ(x) \<lesssim> y ==> y \<noteq> 0" 

157 
by (fast dest!: lepoll_0_is_0) 

158 

159 
lemma eqpoll_succ_imp_not_empty: "x \<approx> succ(n) ==> x \<noteq> 0" 

160 
by (fast elim!: eqpoll_sym [THEN eqpoll_0_is_0, THEN succ_neq_0]) 

161 

162 
lemma Finite_Fin_lemma [rule_format]: 

163 
"n \<in> nat ==> \<forall>A. (A\<approx>n & A \<subseteq> X) > A \<in> Fin(X)" 

164 
apply (induct_tac "n") 

165 
apply (rule allI) 

166 
apply (fast intro!: Fin.emptyI dest!: eqpoll_imp_lepoll [THEN lepoll_0_is_0]) 

167 
apply (rule allI) 

168 
apply (rule impI) 

169 
apply (erule conjE) 

12820  170 
apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], assumption) 
171 
apply (frule Diff_sing_eqpoll, assumption) 

12776  172 
apply (erule allE) 
173 
apply (erule impE, fast) 

12820  174 
apply (drule subsetD, assumption) 
175 
apply (drule Fin.consI, assumption) 

12776  176 
apply (simp add: cons_Diff) 
177 
done 

178 

179 
lemma Finite_Fin: "[ Finite(A); A \<subseteq> X ] ==> A \<in> Fin(X)" 

180 
by (unfold Finite_def, blast intro: Finite_Fin_lemma) 

181 

182 
lemma lesspoll_lemma: 

183 
"[ ~ A \<prec> B; C \<prec> B ] ==> A  C \<noteq> 0" 

184 
apply (unfold lesspoll_def) 

185 
apply (fast dest!: Diff_eq_0_iff [THEN iffD1, THEN subset_imp_lepoll] 

186 
intro!: eqpollI elim: notE 

187 
elim!: eqpollE lepoll_trans) 

188 
done 

189 

190 
lemma eqpoll_imp_Finite_iff: "A \<approx> B ==> Finite(A) <> Finite(B)" 

191 
apply (unfold Finite_def) 

192 
apply (blast intro: eqpoll_trans eqpoll_sym) 

193 
done 

194 

437  195 
end 