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 


6 
Cardinal Arithmetic WITH the Axiom of Choice

13134

7 


8 
These results help justify infinitebranching datatypes

484

9 
*)


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


25 
apply (rule well_ord_cardinal_eqE)


26 
apply assumption+


27 
done


28 


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


30 
apply (blast intro: cardinal_cong cardinal_eqE)


31 
done


32 


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


34 
A Un C = B Un D"


35 
apply (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un)


36 
done


37 


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


39 
apply (rule AC_well_ord [THEN exE])


40 
apply (erule well_ord_lepoll_imp_Card_le)


41 
apply assumption


42 
done


43 


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


45 
apply (rule AC_well_ord [THEN exE])


46 
apply (rule AC_well_ord [THEN exE])


47 
apply (rule AC_well_ord [THEN exE])


48 
apply (rule well_ord_cadd_assoc)


49 
apply assumption+


50 
done


51 


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


53 
apply (rule AC_well_ord [THEN exE])


54 
apply (rule AC_well_ord [THEN exE])


55 
apply (rule AC_well_ord [THEN exE])


56 
apply (rule well_ord_cmult_assoc)


57 
apply assumption+


58 
done


59 


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


61 
apply (rule AC_well_ord [THEN exE])


62 
apply (rule AC_well_ord [THEN exE])


63 
apply (rule AC_well_ord [THEN exE])


64 
apply (rule well_ord_cadd_cmult_distrib)


65 
apply assumption+


66 
done


67 


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


69 
apply (rule AC_well_ord [THEN exE])


70 
apply (erule well_ord_InfCard_square_eq)


71 
apply assumption


72 
done


73 


74 


75 
(*** Other applications of AC ***)


76 


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


78 
apply (rule cardinal_eqpoll


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


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


81 
apply (rule cardinal_eqpoll [THEN eqpoll_imp_lepoll])


82 
done


83 


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


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


86 
erule Card_le_imp_lepoll);


87 
apply (erule lepoll_imp_Card_le)


88 
done


89 


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


91 
apply (unfold surj_def)


92 
apply (erule CollectE)


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


94 
apply (fast elim!: apply_Pair)


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


96 
done


97 


98 
(*Kunen's Lemma 10.20*)


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


100 
apply (rule lepoll_imp_Card_le)


101 
apply (erule surj_implies_inj [THEN exE])


102 
apply (unfold lepoll_def)


103 
apply (erule exI)


104 
done


105 


106 
(*Kunen's Lemma 10.21*)


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


108 
apply (simp add: InfCard_is_Card le_Card_iff)


109 
apply (rule lepoll_trans)


110 
prefer 2


111 
apply (rule InfCard_square_eq [THEN eqpoll_imp_lepoll])


112 
apply (simp add: InfCard_is_Card Card_cardinal_eq)


113 
apply (unfold lepoll_def)


114 
apply (frule InfCard_is_Card [THEN Card_is_Ord])


115 
apply (erule AC_ball_Pi [THEN exE])


116 
apply (rule exI)


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


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


119 
prefer 2


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


121 
elim!: LeastI Ord_in_Ord)


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


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


124 
(*Instantiate the lemma proved above*)


125 
apply (blast intro: inj_is_fun [THEN apply_type] dest: apply_type)


126 
apply (force );


127 
done


128 


129 


130 
(*The same again, using csucc*)


131 
lemma cardinal_UN_lt_csucc:


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


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


134 
apply (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal)


135 
done


136 


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). *)


139 
lemma cardinal_UN_Ord_lt_csucc:


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


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


142 
apply (rule cardinal_UN_lt_csucc [THEN Card_lt_imp_lt])


143 
apply assumption


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


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


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


147 
done


148 


149 


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


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


152 
**)


153 


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


155 
lemma inj_UN_subset:


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


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


158 
apply (rule UN_least)


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


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


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


162 
done


163 


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


165 
be weaker.*)


166 
lemma le_UN_Ord_lt_csucc:


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


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


169 
apply (case_tac "W=0")


170 
(*solve the easy 0 case*)


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


172 
Card_is_Ord Ord_0_lt_csucc)


173 
apply (simp add: InfCard_is_Card le_Card_iff lepoll_def)


174 
apply (safe intro!: equalityI)


175 
apply (erule swap);


176 
apply (rule lt_subset_trans [OF inj_UN_subset cardinal_UN_Ord_lt_csucc])


177 
apply assumption+


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


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


180 
done


181 


182 
end


183 
