src/ZF/Cardinal_AC.thy
author wenzelm
Mon Sep 06 19:13:10 2010 +0200 (2010-09-06)
changeset 39159 0dec18004e75
parent 35762 af3ff2ba4c54
child 45602 2a858377c3d2
permissions -rw-r--r--
more antiquotations;
clasohm@1478
     1
(*  Title:      ZF/Cardinal_AC.thy
clasohm@1478
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@484
     3
    Copyright   1994  University of Cambridge
lcp@484
     4
paulson@13134
     5
These results help justify infinite-branching datatypes
lcp@484
     6
*)
lcp@484
     7
paulson@13328
     8
header{*Cardinal Arithmetic Using AC*}
paulson@13328
     9
haftmann@16417
    10
theory Cardinal_AC imports CardinalArith Zorn begin
paulson@13134
    11
paulson@13356
    12
subsection{*Strengthened Forms of Existing Theorems on Cardinals*}
paulson@13134
    13
paulson@13134
    14
lemma cardinal_eqpoll: "|A| eqpoll A"
paulson@13134
    15
apply (rule AC_well_ord [THEN exE])
paulson@13134
    16
apply (erule well_ord_cardinal_eqpoll)
paulson@13134
    17
done
paulson@13134
    18
paulson@14046
    19
text{*The theorem @{term "||A|| = |A|"} *}
paulson@14046
    20
lemmas cardinal_idem = cardinal_eqpoll [THEN cardinal_cong, standard, simp]
paulson@13134
    21
paulson@13134
    22
lemma cardinal_eqE: "|X| = |Y| ==> X eqpoll Y"
paulson@13134
    23
apply (rule AC_well_ord [THEN exE])
paulson@13134
    24
apply (rule AC_well_ord [THEN exE])
paulson@13269
    25
apply (rule well_ord_cardinal_eqE, assumption+)
paulson@13134
    26
done
paulson@13134
    27
paulson@13134
    28
lemma cardinal_eqpoll_iff: "|X| = |Y| <-> X eqpoll Y"
paulson@13269
    29
by (blast intro: cardinal_cong cardinal_eqE)
paulson@13134
    30
paulson@13615
    31
lemma cardinal_disjoint_Un:
paulson@13615
    32
     "[| |A|=|B|;  |C|=|D|;  A Int C = 0;  B Int D = 0 |] 
paulson@13615
    33
      ==> |A Un C| = |B Un D|"
paulson@13615
    34
by (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un)
paulson@13134
    35
paulson@13134
    36
lemma lepoll_imp_Card_le: "A lepoll B ==> |A| le |B|"
paulson@13134
    37
apply (rule AC_well_ord [THEN exE])
paulson@13269
    38
apply (erule well_ord_lepoll_imp_Card_le, assumption)
paulson@13134
    39
done
paulson@13134
    40
paulson@13134
    41
lemma cadd_assoc: "(i |+| j) |+| k = i |+| (j |+| k)"
paulson@13134
    42
apply (rule AC_well_ord [THEN exE])
paulson@13134
    43
apply (rule AC_well_ord [THEN exE])
paulson@13134
    44
apply (rule AC_well_ord [THEN exE])
paulson@13269
    45
apply (rule well_ord_cadd_assoc, assumption+)
paulson@13134
    46
done
paulson@13134
    47
paulson@13134
    48
lemma cmult_assoc: "(i |*| j) |*| k = i |*| (j |*| k)"
paulson@13134
    49
apply (rule AC_well_ord [THEN exE])
paulson@13134
    50
apply (rule AC_well_ord [THEN exE])
paulson@13134
    51
apply (rule AC_well_ord [THEN exE])
paulson@13269
    52
apply (rule well_ord_cmult_assoc, assumption+)
paulson@13134
    53
done
paulson@13134
    54
paulson@13134
    55
lemma cadd_cmult_distrib: "(i |+| j) |*| k = (i |*| k) |+| (j |*| k)"
paulson@13134
    56
apply (rule AC_well_ord [THEN exE])
paulson@13134
    57
apply (rule AC_well_ord [THEN exE])
paulson@13134
    58
apply (rule AC_well_ord [THEN exE])
paulson@13269
    59
apply (rule well_ord_cadd_cmult_distrib, assumption+)
paulson@13134
    60
done
paulson@13134
    61
paulson@13134
    62
lemma InfCard_square_eq: "InfCard(|A|) ==> A*A eqpoll A"
paulson@13134
    63
apply (rule AC_well_ord [THEN exE])
paulson@13269
    64
apply (erule well_ord_InfCard_square_eq, assumption)
paulson@13134
    65
done
paulson@13134
    66
paulson@13134
    67
paulson@14046
    68
subsection {*The relationship between cardinality and le-pollence*}
paulson@13134
    69
paulson@13134
    70
lemma Card_le_imp_lepoll: "|A| le |B| ==> A lepoll B"
paulson@13134
    71
apply (rule cardinal_eqpoll
paulson@13134
    72
              [THEN eqpoll_sym, THEN eqpoll_imp_lepoll, THEN lepoll_trans])
paulson@13134
    73
apply (erule le_imp_subset [THEN subset_imp_lepoll, THEN lepoll_trans])
paulson@13134
    74
apply (rule cardinal_eqpoll [THEN eqpoll_imp_lepoll])
paulson@13134
    75
done
paulson@13134
    76
paulson@13134
    77
lemma le_Card_iff: "Card(K) ==> |A| le K <-> A lepoll K"
paulson@13134
    78
apply (erule Card_cardinal_eq [THEN subst], rule iffI, 
paulson@13269
    79
       erule Card_le_imp_lepoll)
paulson@13134
    80
apply (erule lepoll_imp_Card_le) 
paulson@13134
    81
done
paulson@13134
    82
paulson@14046
    83
lemma cardinal_0_iff_0 [simp]: "|A| = 0 <-> A = 0";
paulson@14046
    84
apply auto 
paulson@14046
    85
apply (drule cardinal_0 [THEN ssubst])
paulson@14046
    86
apply (blast intro: eqpoll_0_iff [THEN iffD1] cardinal_eqpoll_iff [THEN iffD1])
paulson@14046
    87
done
paulson@14046
    88
paulson@14046
    89
lemma cardinal_lt_iff_lesspoll: "Ord(i) ==> i < |A| <-> i lesspoll A"
paulson@14046
    90
apply (cut_tac A = "A" in cardinal_eqpoll)
paulson@14046
    91
apply (auto simp add: eqpoll_iff)
paulson@14046
    92
apply (blast intro: lesspoll_trans2 lt_Card_imp_lesspoll Card_cardinal)
paulson@14046
    93
apply (force intro: cardinal_lt_imp_lt lesspoll_cardinal_lt lesspoll_trans2 
paulson@14046
    94
             simp add: cardinal_idem)
paulson@14046
    95
done
paulson@14046
    96
paulson@14046
    97
lemma cardinal_le_imp_lepoll: " i \<le> |A| ==> i \<lesssim> A"
paulson@14046
    98
apply (blast intro: lt_Ord Card_le_imp_lepoll Ord_cardinal_le le_trans)
paulson@14046
    99
done
paulson@14046
   100
paulson@14046
   101
paulson@14046
   102
subsection{*Other Applications of AC*}
paulson@14046
   103
paulson@13134
   104
lemma surj_implies_inj: "f: surj(X,Y) ==> EX g. g: inj(Y,X)"
paulson@13134
   105
apply (unfold surj_def)
paulson@13134
   106
apply (erule CollectE)
paulson@13784
   107
apply (rule_tac A1 = Y and B1 = "%y. f-``{y}" in AC_Pi [THEN exE])
paulson@13134
   108
apply (fast elim!: apply_Pair)
paulson@13615
   109
apply (blast dest: apply_type Pi_memberD 
paulson@13615
   110
             intro: apply_equality Pi_type f_imp_injective)
paulson@13134
   111
done
paulson@13134
   112
paulson@13134
   113
(*Kunen's Lemma 10.20*)
paulson@13134
   114
lemma surj_implies_cardinal_le: "f: surj(X,Y) ==> |Y| le |X|"
paulson@13134
   115
apply (rule lepoll_imp_Card_le)
paulson@13134
   116
apply (erule surj_implies_inj [THEN exE])
paulson@13134
   117
apply (unfold lepoll_def)
paulson@13134
   118
apply (erule exI)
paulson@13134
   119
done
paulson@13134
   120
paulson@13134
   121
(*Kunen's Lemma 10.21*)
paulson@13615
   122
lemma cardinal_UN_le:
paulson@13615
   123
     "[| InfCard(K);  ALL i:K. |X(i)| le K |] ==> |\<Union>i\<in>K. X(i)| le K"
paulson@13134
   124
apply (simp add: InfCard_is_Card le_Card_iff)
paulson@13134
   125
apply (rule lepoll_trans)
paulson@13134
   126
 prefer 2
paulson@13134
   127
 apply (rule InfCard_square_eq [THEN eqpoll_imp_lepoll])
paulson@13134
   128
 apply (simp add: InfCard_is_Card Card_cardinal_eq)
paulson@13134
   129
apply (unfold lepoll_def)
paulson@13134
   130
apply (frule InfCard_is_Card [THEN Card_is_Ord])
paulson@13134
   131
apply (erule AC_ball_Pi [THEN exE])
paulson@13134
   132
apply (rule exI)
paulson@13134
   133
(*Lemma needed in both subgoals, for a fixed z*)
paulson@13615
   134
apply (subgoal_tac "ALL z: (\<Union>i\<in>K. X (i)). z: X (LEAST i. z:X (i)) & 
paulson@13615
   135
                    (LEAST i. z:X (i)) : K")
paulson@13134
   136
 prefer 2
paulson@13134
   137
 apply (fast intro!: Least_le [THEN lt_trans1, THEN ltD] ltI
paulson@13134
   138
             elim!: LeastI Ord_in_Ord)
paulson@13269
   139
apply (rule_tac c = "%z. <LEAST i. z:X (i), f ` (LEAST i. z:X (i)) ` z>" 
paulson@13134
   140
            and d = "%<i,j>. converse (f`i) ` j" in lam_injective)
paulson@13134
   141
(*Instantiate the lemma proved above*)
paulson@13269
   142
by (blast intro: inj_is_fun [THEN apply_type] dest: apply_type, force)
paulson@13134
   143
paulson@13134
   144
paulson@13134
   145
(*The same again, using csucc*)
paulson@13134
   146
lemma cardinal_UN_lt_csucc:
paulson@13134
   147
     "[| InfCard(K);  ALL i:K. |X(i)| < csucc(K) |]
paulson@13615
   148
      ==> |\<Union>i\<in>K. X(i)| < csucc(K)"
paulson@13615
   149
by (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal)
paulson@13134
   150
paulson@13134
   151
(*The same again, for a union of ordinals.  In use, j(i) is a bit like rank(i),
paulson@13134
   152
  the least ordinal j such that i:Vfrom(A,j). *)
paulson@13134
   153
lemma cardinal_UN_Ord_lt_csucc:
paulson@13134
   154
     "[| InfCard(K);  ALL i:K. j(i) < csucc(K) |]
paulson@13615
   155
      ==> (\<Union>i\<in>K. j(i)) < csucc(K)"
paulson@13269
   156
apply (rule cardinal_UN_lt_csucc [THEN Card_lt_imp_lt], assumption)
paulson@13134
   157
apply (blast intro: Ord_cardinal_le [THEN lt_trans1] elim: ltE)
paulson@13134
   158
apply (blast intro!: Ord_UN elim: ltE)
paulson@13134
   159
apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN Card_csucc])
paulson@13134
   160
done
paulson@13134
   161
paulson@13134
   162
paulson@13134
   163
(** Main result for infinite-branching datatypes.  As above, but the index
paulson@13134
   164
    set need not be a cardinal.  Surprisingly complicated proof!
paulson@13134
   165
**)
paulson@13134
   166
paulson@13134
   167
(*Work backwards along the injection from W into K, given that W~=0.*)
paulson@13134
   168
lemma inj_UN_subset:
paulson@13134
   169
     "[| f: inj(A,B);  a:A |] ==>            
paulson@13615
   170
      (\<Union>x\<in>A. C(x)) <= (\<Union>y\<in>B. C(if y: range(f) then converse(f)`y else a))"
paulson@13134
   171
apply (rule UN_least)
paulson@13134
   172
apply (rule_tac x1= "f`x" in subset_trans [OF _ UN_upper])
paulson@13134
   173
 apply (simp add: inj_is_fun [THEN apply_rangeI])
paulson@13134
   174
apply (blast intro: inj_is_fun [THEN apply_type])
paulson@13134
   175
done
paulson@13134
   176
paulson@13134
   177
(*Simpler to require |W|=K; we'd have a bijection; but the theorem would
paulson@13134
   178
  be weaker.*)
paulson@13134
   179
lemma le_UN_Ord_lt_csucc:
paulson@13134
   180
     "[| InfCard(K);  |W| le K;  ALL w:W. j(w) < csucc(K) |]
paulson@13615
   181
      ==> (\<Union>w\<in>W. j(w)) < csucc(K)"
paulson@13134
   182
apply (case_tac "W=0")
paulson@13134
   183
(*solve the easy 0 case*)
paulson@13134
   184
 apply (simp add: InfCard_is_Card Card_is_Ord [THEN Card_csucc] 
paulson@13134
   185
                  Card_is_Ord Ord_0_lt_csucc)
paulson@13134
   186
apply (simp add: InfCard_is_Card le_Card_iff lepoll_def)
paulson@13134
   187
apply (safe intro!: equalityI)
paulson@13269
   188
apply (erule swap) 
paulson@13269
   189
apply (rule lt_subset_trans [OF inj_UN_subset cardinal_UN_Ord_lt_csucc], assumption+)
paulson@13134
   190
 apply (simp add: inj_converse_fun [THEN apply_type])
paulson@13134
   191
apply (blast intro!: Ord_UN elim: ltE)
paulson@13134
   192
done
paulson@13134
   193
paulson@14046
   194
ML
paulson@14046
   195
{*
wenzelm@39159
   196
val cardinal_0_iff_0 = @{thm cardinal_0_iff_0};
wenzelm@39159
   197
val cardinal_lt_iff_lesspoll = @{thm cardinal_lt_iff_lesspoll};
paulson@14046
   198
*}
paulson@14046
   199
paulson@13134
   200
end