1478

1 
(* Title: ZF/Cardinal_AC.thy

484

2 
ID: $Id$

1478

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

484

4 
Copyright 1994 University of Cambridge


5 

13134

6 
These results help justify infinitebranching datatypes

484

7 
*)


8 

13328

9 
header{*Cardinal Arithmetic Using AC*}


10 

13134

11 
theory Cardinal_AC = CardinalArith + Zorn:


12 


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


14 


15 
lemma cardinal_eqpoll: "A eqpoll A"


16 
apply (rule AC_well_ord [THEN exE])


17 
apply (erule well_ord_cardinal_eqpoll)


18 
done


19 


20 
lemmas cardinal_idem = cardinal_eqpoll [THEN cardinal_cong, standard]


21 


22 
lemma cardinal_eqE: "X = Y ==> X eqpoll Y"


23 
apply (rule AC_well_ord [THEN exE])


24 
apply (rule AC_well_ord [THEN exE])

13269

25 
apply (rule well_ord_cardinal_eqE, assumption+)

13134

26 
done


27 


28 
lemma cardinal_eqpoll_iff: "X = Y <> X eqpoll Y"

13269

29 
by (blast intro: cardinal_cong cardinal_eqE)

13134

30 


31 
lemma cardinal_disjoint_Un: "[ A=B; C=D; A Int C = 0; B Int D = 0 ] ==>


32 
A Un C = B Un D"


33 
apply (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un)


34 
done


35 


36 
lemma lepoll_imp_Card_le: "A lepoll B ==> A le B"


37 
apply (rule AC_well_ord [THEN exE])

13269

38 
apply (erule well_ord_lepoll_imp_Card_le, assumption)

13134

39 
done


40 


41 
lemma cadd_assoc: "(i + j) + k = i + (j + k)"


42 
apply (rule AC_well_ord [THEN exE])


43 
apply (rule AC_well_ord [THEN exE])


44 
apply (rule AC_well_ord [THEN exE])

13269

45 
apply (rule well_ord_cadd_assoc, assumption+)

13134

46 
done


47 


48 
lemma cmult_assoc: "(i * j) * k = i * (j * k)"


49 
apply (rule AC_well_ord [THEN exE])


50 
apply (rule AC_well_ord [THEN exE])


51 
apply (rule AC_well_ord [THEN exE])

13269

52 
apply (rule well_ord_cmult_assoc, assumption+)

13134

53 
done


54 


55 
lemma cadd_cmult_distrib: "(i + j) * k = (i * k) + (j * k)"


56 
apply (rule AC_well_ord [THEN exE])


57 
apply (rule AC_well_ord [THEN exE])


58 
apply (rule AC_well_ord [THEN exE])

13269

59 
apply (rule well_ord_cadd_cmult_distrib, assumption+)

13134

60 
done


61 


62 
lemma InfCard_square_eq: "InfCard(A) ==> A*A eqpoll A"


63 
apply (rule AC_well_ord [THEN exE])

13269

64 
apply (erule well_ord_InfCard_square_eq, assumption)

13134

65 
done


66 


67 


68 
(*** Other applications of AC ***)


69 


70 
lemma Card_le_imp_lepoll: "A le B ==> A lepoll B"


71 
apply (rule cardinal_eqpoll


72 
[THEN eqpoll_sym, THEN eqpoll_imp_lepoll, THEN lepoll_trans])


73 
apply (erule le_imp_subset [THEN subset_imp_lepoll, THEN lepoll_trans])


74 
apply (rule cardinal_eqpoll [THEN eqpoll_imp_lepoll])


75 
done


76 


77 
lemma le_Card_iff: "Card(K) ==> A le K <> A lepoll K"


78 
apply (erule Card_cardinal_eq [THEN subst], rule iffI,

13269

79 
erule Card_le_imp_lepoll)

13134

80 
apply (erule lepoll_imp_Card_le)


81 
done


82 


83 
lemma surj_implies_inj: "f: surj(X,Y) ==> EX g. g: inj(Y,X)"


84 
apply (unfold surj_def)


85 
apply (erule CollectE)


86 
apply (rule_tac A1 = "Y" and B1 = "%y. f``{y}" in AC_Pi [THEN exE])


87 
apply (fast elim!: apply_Pair)


88 
apply (blast dest: apply_type Pi_memberD intro: apply_equality Pi_type f_imp_injective)


89 
done


90 


91 
(*Kunen's Lemma 10.20*)


92 
lemma surj_implies_cardinal_le: "f: surj(X,Y) ==> Y le X"


93 
apply (rule lepoll_imp_Card_le)


94 
apply (erule surj_implies_inj [THEN exE])


95 
apply (unfold lepoll_def)


96 
apply (erule exI)


97 
done


98 


99 
(*Kunen's Lemma 10.21*)


100 
lemma cardinal_UN_le: "[ InfCard(K); ALL i:K. X(i) le K ] ==> UN i:K. X(i) le K"


101 
apply (simp add: InfCard_is_Card le_Card_iff)


102 
apply (rule lepoll_trans)


103 
prefer 2


104 
apply (rule InfCard_square_eq [THEN eqpoll_imp_lepoll])


105 
apply (simp add: InfCard_is_Card Card_cardinal_eq)


106 
apply (unfold lepoll_def)


107 
apply (frule InfCard_is_Card [THEN Card_is_Ord])


108 
apply (erule AC_ball_Pi [THEN exE])


109 
apply (rule exI)


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


111 
apply (subgoal_tac "ALL z: (UN i:K. X (i)). z: X (LEAST i. z:X (i)) & (LEAST i. z:X (i)) : K")


112 
prefer 2


113 
apply (fast intro!: Least_le [THEN lt_trans1, THEN ltD] ltI


114 
elim!: LeastI Ord_in_Ord)

13269

115 
apply (rule_tac c = "%z. <LEAST i. z:X (i), f ` (LEAST i. z:X (i)) ` z>"

13134

116 
and d = "%<i,j>. converse (f`i) ` j" in lam_injective)


117 
(*Instantiate the lemma proved above*)

13269

118 
by (blast intro: inj_is_fun [THEN apply_type] dest: apply_type, force)

13134

119 


120 


121 
(*The same again, using csucc*)


122 
lemma cardinal_UN_lt_csucc:


123 
"[ InfCard(K); ALL i:K. X(i) < csucc(K) ]


124 
==> UN i:K. X(i) < csucc(K)"


125 
apply (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal)


126 
done


127 


128 
(*The same again, for a union of ordinals. In use, j(i) is a bit like rank(i),


129 
the least ordinal j such that i:Vfrom(A,j). *)


130 
lemma cardinal_UN_Ord_lt_csucc:


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


132 
==> (UN i:K. j(i)) < csucc(K)"

13269

133 
apply (rule cardinal_UN_lt_csucc [THEN Card_lt_imp_lt], assumption)

13134

134 
apply (blast intro: Ord_cardinal_le [THEN lt_trans1] elim: ltE)


135 
apply (blast intro!: Ord_UN elim: ltE)


136 
apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN Card_csucc])


137 
done


138 


139 


140 
(** Main result for infinitebranching datatypes. As above, but the index


141 
set need not be a cardinal. Surprisingly complicated proof!


142 
**)


143 


144 
(*Work backwards along the injection from W into K, given that W~=0.*)


145 
lemma inj_UN_subset:


146 
"[ f: inj(A,B); a:A ] ==>


147 
(UN x:A. C(x)) <= (UN y:B. C(if y: range(f) then converse(f)`y else a))"


148 
apply (rule UN_least)


149 
apply (rule_tac x1= "f`x" in subset_trans [OF _ UN_upper])


150 
apply (simp add: inj_is_fun [THEN apply_rangeI])


151 
apply (blast intro: inj_is_fun [THEN apply_type])


152 
done


153 


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


155 
be weaker.*)


156 
lemma le_UN_Ord_lt_csucc:


157 
"[ InfCard(K); W le K; ALL w:W. j(w) < csucc(K) ]


158 
==> (UN w:W. j(w)) < csucc(K)"


159 
apply (case_tac "W=0")


160 
(*solve the easy 0 case*)


161 
apply (simp add: InfCard_is_Card Card_is_Ord [THEN Card_csucc]


162 
Card_is_Ord Ord_0_lt_csucc)


163 
apply (simp add: InfCard_is_Card le_Card_iff lepoll_def)


164 
apply (safe intro!: equalityI)

13269

165 
apply (erule swap)


166 
apply (rule lt_subset_trans [OF inj_UN_subset cardinal_UN_Ord_lt_csucc], assumption+)

13134

167 
apply (simp add: inj_converse_fun [THEN apply_type])


168 
apply (blast intro!: Ord_UN elim: ltE)


169 
done


170 


171 
end


172 
