src/ZF/Cardinal_AC.thy
author wenzelm
Mon Dec 04 22:54:31 2017 +0100 (20 months ago)
changeset 67131 85d10959c2e4
parent 61980 6b780867d426
child 67443 3abf6a722518
permissions -rw-r--r--
tuned signature;
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
wenzelm@60770
     8
section\<open>Cardinal Arithmetic Using AC\<close>
paulson@13328
     9
haftmann@16417
    10
theory Cardinal_AC imports CardinalArith Zorn begin
paulson@13134
    11
wenzelm@60770
    12
subsection\<open>Strengthened Forms of Existing Theorems on Cardinals\<close>
paulson@13134
    13
paulson@46954
    14
lemma cardinal_eqpoll: "|A| \<approx> 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
wenzelm@60770
    19
text\<open>The theorem @{term "||A|| = |A|"}\<close>
wenzelm@45602
    20
lemmas cardinal_idem = cardinal_eqpoll [THEN cardinal_cong, simp]
paulson@13134
    21
paulson@46954
    22
lemma cardinal_eqE: "|X| = |Y| ==> X \<approx> 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@46954
    28
lemma cardinal_eqpoll_iff: "|X| = |Y| \<longleftrightarrow> X \<approx> Y"
paulson@13269
    29
by (blast intro: cardinal_cong cardinal_eqE)
paulson@13134
    30
paulson@13615
    31
lemma cardinal_disjoint_Un:
paulson@46820
    32
     "[| |A|=|B|;  |C|=|D|;  A \<inter> C = 0;  B \<inter> D = 0 |]
paulson@46820
    33
      ==> |A \<union> C| = |B \<union> D|"
paulson@13615
    34
by (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un)
paulson@13134
    35
paulson@46954
    36
lemma lepoll_imp_Card_le: "A \<lesssim> 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@46821
    41
lemma cadd_assoc: "(i \<oplus> j) \<oplus> k = i \<oplus> (j \<oplus> 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@46821
    48
lemma cmult_assoc: "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> 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@46821
    55
lemma cadd_cmult_distrib: "(i \<oplus> j) \<otimes> k = (i \<otimes> k) \<oplus> (j \<otimes> 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@46954
    62
lemma InfCard_square_eq: "InfCard(|A|) ==> A*A \<approx> 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
wenzelm@60770
    68
subsection \<open>The relationship between cardinality and le-pollence\<close>
paulson@13134
    69
paulson@46954
    70
lemma Card_le_imp_lepoll:
paulson@46954
    71
  assumes "|A| \<le> |B|" shows "A \<lesssim> B"
paulson@46954
    72
proof -
paulson@46954
    73
  have "A \<approx> |A|" 
paulson@46954
    74
    by (rule cardinal_eqpoll [THEN eqpoll_sym])
paulson@46954
    75
  also have "... \<lesssim> |B|"
paulson@46954
    76
    by (rule le_imp_subset [THEN subset_imp_lepoll]) (rule assms)
paulson@46954
    77
  also have "... \<approx> B" 
paulson@46954
    78
    by (rule cardinal_eqpoll)
paulson@46954
    79
  finally show ?thesis .
paulson@46954
    80
qed
paulson@13134
    81
paulson@46954
    82
lemma le_Card_iff: "Card(K) ==> |A| \<le> K \<longleftrightarrow> A \<lesssim> K"
paulson@46820
    83
apply (erule Card_cardinal_eq [THEN subst], rule iffI,
paulson@13269
    84
       erule Card_le_imp_lepoll)
paulson@46820
    85
apply (erule lepoll_imp_Card_le)
paulson@13134
    86
done
paulson@13134
    87
paulson@46954
    88
lemma cardinal_0_iff_0 [simp]: "|A| = 0 \<longleftrightarrow> A = 0"
paulson@46820
    89
apply auto
paulson@14046
    90
apply (drule cardinal_0 [THEN ssubst])
paulson@14046
    91
apply (blast intro: eqpoll_0_iff [THEN iffD1] cardinal_eqpoll_iff [THEN iffD1])
paulson@14046
    92
done
paulson@14046
    93
paulson@46954
    94
lemma cardinal_lt_iff_lesspoll:
paulson@46954
    95
  assumes i: "Ord(i)" shows "i < |A| \<longleftrightarrow> i \<prec> A"
paulson@46954
    96
proof
paulson@46954
    97
  assume "i < |A|"
paulson@46954
    98
  hence  "i \<prec> |A|" 
paulson@46954
    99
    by (blast intro: lt_Card_imp_lesspoll Card_cardinal) 
paulson@46954
   100
  also have "...  \<approx> A" 
paulson@46954
   101
    by (rule cardinal_eqpoll)
paulson@46954
   102
  finally show "i \<prec> A" .
paulson@46954
   103
next
paulson@46954
   104
  assume "i \<prec> A"
paulson@46954
   105
  also have "...  \<approx> |A|" 
paulson@46954
   106
    by (blast intro: cardinal_eqpoll eqpoll_sym) 
paulson@46954
   107
  finally have "i \<prec> |A|" .
paulson@46954
   108
  thus  "i < |A|" using i
paulson@46954
   109
    by (force intro: cardinal_lt_imp_lt lesspoll_cardinal_lt)
paulson@46954
   110
qed
paulson@14046
   111
paulson@14046
   112
lemma cardinal_le_imp_lepoll: " i \<le> |A| ==> i \<lesssim> A"
paulson@46954
   113
  by (blast intro: lt_Ord Card_le_imp_lepoll Ord_cardinal_le le_trans)
paulson@14046
   114
paulson@14046
   115
wenzelm@60770
   116
subsection\<open>Other Applications of AC\<close>
paulson@14046
   117
paulson@47052
   118
lemma surj_implies_inj:
paulson@47052
   119
  assumes f: "f \<in> surj(X,Y)" shows "\<exists>g. g \<in> inj(Y,X)"
paulson@47052
   120
proof -
paulson@47052
   121
  from f AC_Pi [of Y "%y. f-``{y}"]
wenzelm@61980
   122
  obtain z where z: "z \<in> (\<Prod>y\<in>Y. f -`` {y})"  
paulson@47052
   123
    by (auto simp add: surj_def) (fast dest: apply_Pair)
paulson@47052
   124
  show ?thesis
paulson@47052
   125
    proof
paulson@47052
   126
      show "z \<in> inj(Y, X)" using z surj_is_fun [OF f]
paulson@47052
   127
        by (blast dest: apply_type Pi_memberD
paulson@47052
   128
                  intro: apply_equality Pi_type f_imp_injective)
paulson@47052
   129
    qed
paulson@47052
   130
qed
paulson@13134
   131
wenzelm@60770
   132
text\<open>Kunen's Lemma 10.20\<close>
paulson@47052
   133
lemma surj_implies_cardinal_le: 
paulson@47052
   134
  assumes f: "f \<in> surj(X,Y)" shows "|Y| \<le> |X|"
paulson@47052
   135
proof (rule lepoll_imp_Card_le)
paulson@47052
   136
  from f [THEN surj_implies_inj] obtain g where "g \<in> inj(Y,X)" ..
paulson@47052
   137
  thus "Y \<lesssim> X"
paulson@47052
   138
    by (auto simp add: lepoll_def)
paulson@47052
   139
qed
paulson@13134
   140
wenzelm@60770
   141
text\<open>Kunen's Lemma 10.21\<close>
paulson@13615
   142
lemma cardinal_UN_le:
paulson@46963
   143
  assumes K: "InfCard(K)" 
paulson@46963
   144
  shows "(!!i. i\<in>K ==> |X(i)| \<le> K) ==> |\<Union>i\<in>K. X(i)| \<le> K"
paulson@46963
   145
proof (simp add: K InfCard_is_Card le_Card_iff)
paulson@46963
   146
  have [intro]: "Ord(K)" by (blast intro: InfCard_is_Card Card_is_Ord K) 
paulson@46963
   147
  assume "!!i. i\<in>K ==> X(i) \<lesssim> K"
paulson@46963
   148
  hence "!!i. i\<in>K ==> \<exists>f. f \<in> inj(X(i), K)" by (simp add: lepoll_def) 
wenzelm@61980
   149
  with AC_Pi obtain f where f: "f \<in> (\<Prod>i\<in>K. inj(X(i), K))"
paulson@47052
   150
    by force 
paulson@46963
   151
  { fix z
paulson@46963
   152
    assume z: "z \<in> (\<Union>i\<in>K. X(i))"
paulson@46963
   153
    then obtain i where i: "i \<in> K" "Ord(i)" "z \<in> X(i)"
paulson@46963
   154
      by (blast intro: Ord_in_Ord [of K]) 
wenzelm@61394
   155
    hence "(\<mu> i. z \<in> X(i)) \<le> i" by (fast intro: Least_le) 
wenzelm@61394
   156
    hence "(\<mu> i. z \<in> X(i)) < K" by (best intro: lt_trans1 ltI i) 
wenzelm@61394
   157
    hence "(\<mu> i. z \<in> X(i)) \<in> K" and "z \<in> X(\<mu> i. z \<in> X(i))"  
paulson@46963
   158
      by (auto intro: LeastI ltD i) 
paulson@46963
   159
  } note mems = this
paulson@46963
   160
  have "(\<Union>i\<in>K. X(i)) \<lesssim> K \<times> K" 
paulson@46963
   161
    proof (unfold lepoll_def)
paulson@46963
   162
      show "\<exists>f. f \<in> inj(\<Union>RepFun(K, X), K \<times> K)"
paulson@46963
   163
        apply (rule exI) 
wenzelm@61394
   164
        apply (rule_tac c = "%z. \<langle>\<mu> i. z \<in> X(i), f ` (\<mu> i. z \<in> X(i)) ` z\<rangle>"
paulson@46963
   165
                    and d = "%\<langle>i,j\<rangle>. converse (f`i) ` j" in lam_injective) 
paulson@46963
   166
        apply (force intro: f inj_is_fun mems apply_type Perm.left_inverse)+
paulson@46963
   167
        done
paulson@46963
   168
    qed
paulson@46963
   169
  also have "... \<approx> K" 
paulson@46963
   170
    by (simp add: K InfCard_square_eq InfCard_is_Card Card_cardinal_eq)
paulson@46963
   171
  finally show "(\<Union>i\<in>K. X(i)) \<lesssim> K" .
paulson@46963
   172
qed
paulson@13134
   173
wenzelm@60770
   174
text\<open>The same again, using @{term csucc}\<close>
paulson@13134
   175
lemma cardinal_UN_lt_csucc:
paulson@47071
   176
     "[| InfCard(K);  \<And>i. i\<in>K \<Longrightarrow> |X(i)| < csucc(K) |]
paulson@13615
   177
      ==> |\<Union>i\<in>K. X(i)| < csucc(K)"
paulson@13615
   178
by (simp add: Card_lt_csucc_iff cardinal_UN_le InfCard_is_Card Card_cardinal)
paulson@13134
   179
wenzelm@60770
   180
text\<open>The same again, for a union of ordinals.  In use, j(i) is a bit like rank(i),
wenzelm@60770
   181
  the least ordinal j such that i:Vfrom(A,j).\<close>
paulson@13134
   182
lemma cardinal_UN_Ord_lt_csucc:
paulson@47071
   183
     "[| InfCard(K);  \<And>i. i\<in>K \<Longrightarrow> j(i) < csucc(K) |]
paulson@13615
   184
      ==> (\<Union>i\<in>K. j(i)) < csucc(K)"
paulson@13269
   185
apply (rule cardinal_UN_lt_csucc [THEN Card_lt_imp_lt], assumption)
paulson@13134
   186
apply (blast intro: Ord_cardinal_le [THEN lt_trans1] elim: ltE)
paulson@13134
   187
apply (blast intro!: Ord_UN elim: ltE)
paulson@13134
   188
apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN Card_csucc])
paulson@13134
   189
done
paulson@13134
   190
paulson@13134
   191
wenzelm@60770
   192
subsection\<open>The Main Result for Infinite-Branching Datatypes\<close>
paulson@13134
   193
wenzelm@60770
   194
text\<open>As above, but the index set need not be a cardinal. Work
paulson@47071
   195
backwards along the injection from @{term W} into @{term K}, given
wenzelm@60770
   196
that @{term"W\<noteq>0"}.\<close>
paulson@46954
   197
paulson@13134
   198
lemma inj_UN_subset:
paulson@46954
   199
  assumes f: "f \<in> inj(A,B)" and a: "a \<in> A"
paulson@46954
   200
  shows "(\<Union>x\<in>A. C(x)) \<subseteq> (\<Union>y\<in>B. C(if y \<in> range(f) then converse(f)`y else a))"
paulson@46954
   201
proof (rule UN_least)
paulson@46954
   202
  fix x
paulson@46954
   203
  assume x: "x \<in> A"
paulson@46954
   204
  hence fx: "f ` x \<in> B" by (blast intro: f inj_is_fun [THEN apply_type])
paulson@46954
   205
  have "C(x) \<subseteq> C(if f ` x \<in> range(f) then converse(f) ` (f ` x) else a)" 
paulson@46954
   206
    using f x by (simp add: inj_is_fun [THEN apply_rangeI])
paulson@46954
   207
  also have "... \<subseteq> (\<Union>y\<in>B. C(if y \<in> range(f) then converse(f) ` y else a))"
paulson@46954
   208
    by (rule UN_upper [OF fx]) 
paulson@46954
   209
  finally show "C(x) \<subseteq> (\<Union>y\<in>B. C(if y \<in> range(f) then converse(f)`y else a))" .
paulson@46954
   210
qed
paulson@13134
   211
paulson@47071
   212
theorem le_UN_Ord_lt_csucc:
paulson@47071
   213
  assumes IK: "InfCard(K)" and WK: "|W| \<le> K" and j: "\<And>w. w\<in>W \<Longrightarrow> j(w) < csucc(K)"
paulson@47071
   214
  shows "(\<Union>w\<in>W. j(w)) < csucc(K)"
paulson@47071
   215
proof -
paulson@47071
   216
  have CK: "Card(K)" 
paulson@47071
   217
    by (simp add: InfCard_is_Card IK)
paulson@47071
   218
  then obtain f where f: "f \<in> inj(W, K)" using WK
paulson@47071
   219
    by(auto simp add: le_Card_iff lepoll_def)
paulson@47071
   220
  have OU: "Ord(\<Union>w\<in>W. j(w))" using j
paulson@47071
   221
    by (blast elim: ltE)
paulson@47071
   222
  note lt_subset_trans [OF _ _ OU, trans]
paulson@47071
   223
  show ?thesis
paulson@47071
   224
    proof (cases "W=0")
wenzelm@61798
   225
      case True  \<comment>\<open>solve the easy 0 case\<close>
paulson@47071
   226
      thus ?thesis by (simp add: CK Card_is_Ord Card_csucc Ord_0_lt_csucc)
paulson@47071
   227
    next
paulson@47071
   228
      case False
paulson@47071
   229
        then obtain x where x: "x \<in> W" by blast
paulson@47071
   230
        have "(\<Union>x\<in>W. j(x)) \<subseteq> (\<Union>k\<in>K. j(if k \<in> range(f) then converse(f) ` k else x))"
paulson@47071
   231
          by (rule inj_UN_subset [OF f x]) 
paulson@47071
   232
        also have "... < csucc(K)" using IK
paulson@47071
   233
          proof (rule cardinal_UN_Ord_lt_csucc)
paulson@47071
   234
            fix k
paulson@47071
   235
            assume "k \<in> K"
paulson@47071
   236
            thus "j(if k \<in> range(f) then converse(f) ` k else x) < csucc(K)" using f x j
paulson@47071
   237
              by (simp add: inj_converse_fun [THEN apply_type])
paulson@47071
   238
          qed
paulson@47071
   239
        finally show ?thesis .
paulson@47071
   240
    qed
paulson@47071
   241
qed
paulson@13134
   242
paulson@13134
   243
end