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