src/ZF/Cardinal_AC.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 47071 2884ee1ffbf0
child 58871 c399ae4b836f
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
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
2b8c2a7547ab expanded tabs
clasohm
parents: 484
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     3
    Copyright   1994  University of Cambridge
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     4
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
     5
These results help justify infinite-branching datatypes
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     6
*)
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     7
13328
703de709a64b better document preparation
paulson
parents: 13269
diff changeset
     8
header{*Cardinal Arithmetic Using AC*}
703de709a64b better document preparation
paulson
parents: 13269
diff changeset
     9
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14046
diff changeset
    10
theory Cardinal_AC imports CardinalArith Zorn begin
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    11
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13328
diff changeset
    12
subsection{*Strengthened Forms of Existing Theorems on Cardinals*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    13
46954
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
    14
lemma cardinal_eqpoll: "|A| \<approx> A"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    15
apply (rule AC_well_ord [THEN exE])
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    16
apply (erule well_ord_cardinal_eqpoll)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    17
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    18
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13784
diff changeset
    19
text{*The theorem @{term "||A|| = |A|"} *}
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 39159
diff changeset
    20
lemmas cardinal_idem = cardinal_eqpoll [THEN cardinal_cong, simp]
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    21
46954
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
    22
lemma cardinal_eqE: "|X| = |Y| ==> X \<approx> Y"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    23
apply (rule AC_well_ord [THEN exE])
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    24
apply (rule AC_well_ord [THEN exE])
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13134
diff changeset
    25
apply (rule well_ord_cardinal_eqE, assumption+)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    26
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    27
46954
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
    28
lemma cardinal_eqpoll_iff: "|X| = |Y| \<longleftrightarrow> X \<approx> Y"
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13134
diff changeset
    29
by (blast intro: cardinal_cong cardinal_eqE)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    30
13615
449a70d88b38 Numerous cosmetic changes, prompted by the new simplifier
paulson
parents: 13356
diff changeset
    31
lemma cardinal_disjoint_Un:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    32
     "[| |A|=|B|;  |C|=|D|;  A \<inter> C = 0;  B \<inter> D = 0 |]
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    33
      ==> |A \<union> C| = |B \<union> D|"
13615
449a70d88b38 Numerous cosmetic changes, prompted by the new simplifier
paulson
parents: 13356
diff changeset
    34
by (simp add: cardinal_eqpoll_iff eqpoll_disjoint_Un)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    35
46954
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
    36
lemma lepoll_imp_Card_le: "A \<lesssim> B ==> |A| \<le> |B|"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    37
apply (rule AC_well_ord [THEN exE])
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13134
diff changeset
    38
apply (erule well_ord_lepoll_imp_Card_le, assumption)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    39
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    40
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
    41
lemma cadd_assoc: "(i \<oplus> j) \<oplus> k = i \<oplus> (j \<oplus> k)"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    42
apply (rule AC_well_ord [THEN exE])
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])
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13134
diff changeset
    45
apply (rule well_ord_cadd_assoc, assumption+)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    46
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    47
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
    48
lemma cmult_assoc: "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    49
apply (rule AC_well_ord [THEN exE])
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])
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13134
diff changeset
    52
apply (rule well_ord_cmult_assoc, assumption+)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    53
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    54
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
    55
lemma cadd_cmult_distrib: "(i \<oplus> j) \<otimes> k = (i \<otimes> k) \<oplus> (j \<otimes> k)"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    56
apply (rule AC_well_ord [THEN exE])
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])
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13134
diff changeset
    59
apply (rule well_ord_cadd_cmult_distrib, assumption+)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    60
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    61
46954
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
    62
lemma InfCard_square_eq: "InfCard(|A|) ==> A*A \<approx> A"
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    63
apply (rule AC_well_ord [THEN exE])
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13134
diff changeset
    64
apply (erule well_ord_InfCard_square_eq, assumption)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    65
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    66
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    67
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13784
diff changeset
    68
subsection {*The relationship between cardinality and le-pollence*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    69
46954
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
    70
lemma Card_le_imp_lepoll:
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
    71
  assumes "|A| \<le> |B|" shows "A \<lesssim> B"
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
    72
proof -
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
    73
  have "A \<approx> |A|" 
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
    74
    by (rule cardinal_eqpoll [THEN eqpoll_sym])
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
    75
  also have "... \<lesssim> |B|"
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
    76
    by (rule le_imp_subset [THEN subset_imp_lepoll]) (rule assms)
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
    77
  also have "... \<approx> B" 
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
    78
    by (rule cardinal_eqpoll)
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
    79
  finally show ?thesis .
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
    80
qed
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    81
46954
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
    82
lemma le_Card_iff: "Card(K) ==> |A| \<le> K \<longleftrightarrow> A \<lesssim> K"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    83
apply (erule Card_cardinal_eq [THEN subst], rule iffI,
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13134
diff changeset
    84
       erule Card_le_imp_lepoll)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    85
apply (erule lepoll_imp_Card_le)
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    86
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
    87
46954
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
    88
lemma cardinal_0_iff_0 [simp]: "|A| = 0 \<longleftrightarrow> A = 0"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    89
apply auto
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13784
diff changeset
    90
apply (drule cardinal_0 [THEN ssubst])
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13784
diff changeset
    91
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
    92
done
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13784
diff changeset
    93
46954
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
    94
lemma cardinal_lt_iff_lesspoll:
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
    95
  assumes i: "Ord(i)" shows "i < |A| \<longleftrightarrow> i \<prec> A"
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
    96
proof
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
    97
  assume "i < |A|"
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
    98
  hence  "i \<prec> |A|" 
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
    99
    by (blast intro: lt_Card_imp_lesspoll Card_cardinal) 
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
   100
  also have "...  \<approx> A" 
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
   101
    by (rule cardinal_eqpoll)
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
   102
  finally show "i \<prec> A" .
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
   103
next
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
   104
  assume "i \<prec> A"
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
   105
  also have "...  \<approx> |A|" 
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
   106
    by (blast intro: cardinal_eqpoll eqpoll_sym) 
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
   107
  finally have "i \<prec> |A|" .
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
   108
  thus  "i < |A|" using i
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
   109
    by (force intro: cardinal_lt_imp_lt lesspoll_cardinal_lt)
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
   110
qed
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13784
diff changeset
   111
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13784
diff changeset
   112
lemma cardinal_le_imp_lepoll: " i \<le> |A| ==> i \<lesssim> A"
46954
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
   113
  by (blast intro: lt_Ord Card_le_imp_lepoll Ord_cardinal_le le_trans)
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13784
diff changeset
   114
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13784
diff changeset
   115
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13784
diff changeset
   116
subsection{*Other Applications of AC*}
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13784
diff changeset
   117
47052
e4ee21290dca proof tidying
paulson
parents: 46963
diff changeset
   118
lemma surj_implies_inj:
e4ee21290dca proof tidying
paulson
parents: 46963
diff changeset
   119
  assumes f: "f \<in> surj(X,Y)" shows "\<exists>g. g \<in> inj(Y,X)"
e4ee21290dca proof tidying
paulson
parents: 46963
diff changeset
   120
proof -
e4ee21290dca proof tidying
paulson
parents: 46963
diff changeset
   121
  from f AC_Pi [of Y "%y. f-``{y}"]
e4ee21290dca proof tidying
paulson
parents: 46963
diff changeset
   122
  obtain z where z: "z \<in> (\<Pi> y\<in>Y. f -`` {y})"  
e4ee21290dca proof tidying
paulson
parents: 46963
diff changeset
   123
    by (auto simp add: surj_def) (fast dest: apply_Pair)
e4ee21290dca proof tidying
paulson
parents: 46963
diff changeset
   124
  show ?thesis
e4ee21290dca proof tidying
paulson
parents: 46963
diff changeset
   125
    proof
e4ee21290dca proof tidying
paulson
parents: 46963
diff changeset
   126
      show "z \<in> inj(Y, X)" using z surj_is_fun [OF f]
e4ee21290dca proof tidying
paulson
parents: 46963
diff changeset
   127
        by (blast dest: apply_type Pi_memberD
e4ee21290dca proof tidying
paulson
parents: 46963
diff changeset
   128
                  intro: apply_equality Pi_type f_imp_injective)
e4ee21290dca proof tidying
paulson
parents: 46963
diff changeset
   129
    qed
e4ee21290dca proof tidying
paulson
parents: 46963
diff changeset
   130
qed
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
   131
47052
e4ee21290dca proof tidying
paulson
parents: 46963
diff changeset
   132
text{*Kunen's Lemma 10.20*}
e4ee21290dca proof tidying
paulson
parents: 46963
diff changeset
   133
lemma surj_implies_cardinal_le: 
e4ee21290dca proof tidying
paulson
parents: 46963
diff changeset
   134
  assumes f: "f \<in> surj(X,Y)" shows "|Y| \<le> |X|"
e4ee21290dca proof tidying
paulson
parents: 46963
diff changeset
   135
proof (rule lepoll_imp_Card_le)
e4ee21290dca proof tidying
paulson
parents: 46963
diff changeset
   136
  from f [THEN surj_implies_inj] obtain g where "g \<in> inj(Y,X)" ..
e4ee21290dca proof tidying
paulson
parents: 46963
diff changeset
   137
  thus "Y \<lesssim> X"
e4ee21290dca proof tidying
paulson
parents: 46963
diff changeset
   138
    by (auto simp add: lepoll_def)
e4ee21290dca proof tidying
paulson
parents: 46963
diff changeset
   139
qed
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
   140
47052
e4ee21290dca proof tidying
paulson
parents: 46963
diff changeset
   141
text{*Kunen's Lemma 10.21*}
13615
449a70d88b38 Numerous cosmetic changes, prompted by the new simplifier
paulson
parents: 13356
diff changeset
   142
lemma cardinal_UN_le:
46963
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   143
  assumes K: "InfCard(K)" 
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   144
  shows "(!!i. i\<in>K ==> |X(i)| \<le> K) ==> |\<Union>i\<in>K. X(i)| \<le> K"
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   145
proof (simp add: K InfCard_is_Card le_Card_iff)
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   146
  have [intro]: "Ord(K)" by (blast intro: InfCard_is_Card Card_is_Ord K) 
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   147
  assume "!!i. i\<in>K ==> X(i) \<lesssim> K"
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   148
  hence "!!i. i\<in>K ==> \<exists>f. f \<in> inj(X(i), K)" by (simp add: lepoll_def) 
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   149
  with AC_Pi obtain f where f: "f \<in> (\<Pi> i\<in>K. inj(X(i), K))"
47052
e4ee21290dca proof tidying
paulson
parents: 46963
diff changeset
   150
    by force 
46963
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   151
  { fix z
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   152
    assume z: "z \<in> (\<Union>i\<in>K. X(i))"
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   153
    then obtain i where i: "i \<in> K" "Ord(i)" "z \<in> X(i)"
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   154
      by (blast intro: Ord_in_Ord [of K]) 
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   155
    hence "(LEAST i. z \<in> X(i)) \<le> i" by (fast intro: Least_le) 
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   156
    hence "(LEAST i. z \<in> X(i)) < K" by (best intro: lt_trans1 ltI i) 
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   157
    hence "(LEAST i. z \<in> X(i)) \<in> K" and "z \<in> X(LEAST i. z \<in> X(i))"  
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   158
      by (auto intro: LeastI ltD i) 
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   159
  } note mems = this
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   160
  have "(\<Union>i\<in>K. X(i)) \<lesssim> K \<times> K" 
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   161
    proof (unfold lepoll_def)
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   162
      show "\<exists>f. f \<in> inj(\<Union>RepFun(K, X), K \<times> K)"
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   163
        apply (rule exI) 
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   164
        apply (rule_tac c = "%z. \<langle>LEAST i. z \<in> X(i), f ` (LEAST i. z \<in> X(i)) ` z\<rangle>"
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   165
                    and d = "%\<langle>i,j\<rangle>. converse (f`i) ` j" in lam_injective) 
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   166
        apply (force intro: f inj_is_fun mems apply_type Perm.left_inverse)+
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   167
        done
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   168
    qed
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   169
  also have "... \<approx> K" 
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   170
    by (simp add: K InfCard_square_eq InfCard_is_Card Card_cardinal_eq)
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   171
  finally show "(\<Union>i\<in>K. X(i)) \<lesssim> K" .
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   172
qed
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
   173
46963
67da5904300a Structured transfinite induction proofs
paulson
parents: 46954
diff changeset
   174
text{*The same again, using @{term csucc}*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
   175
lemma cardinal_UN_lt_csucc:
47071
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   176
     "[| InfCard(K);  \<And>i. i\<in>K \<Longrightarrow> |X(i)| < csucc(K) |]
13615
449a70d88b38 Numerous cosmetic changes, prompted by the new simplifier
paulson
parents: 13356
diff changeset
   177
      ==> |\<Union>i\<in>K. X(i)| < csucc(K)"
449a70d88b38 Numerous cosmetic changes, prompted by the new simplifier
paulson
parents: 13356
diff changeset
   178
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
   179
47052
e4ee21290dca proof tidying
paulson
parents: 46963
diff changeset
   180
text{*The same again, for a union of ordinals.  In use, j(i) is a bit like rank(i),
e4ee21290dca proof tidying
paulson
parents: 46963
diff changeset
   181
  the least ordinal j such that i:Vfrom(A,j). *}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
   182
lemma cardinal_UN_Ord_lt_csucc:
47071
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   183
     "[| InfCard(K);  \<And>i. i\<in>K \<Longrightarrow> j(i) < csucc(K) |]
13615
449a70d88b38 Numerous cosmetic changes, prompted by the new simplifier
paulson
parents: 13356
diff changeset
   184
      ==> (\<Union>i\<in>K. j(i)) < csucc(K)"
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13134
diff changeset
   185
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
   186
apply (blast intro: Ord_cardinal_le [THEN lt_trans1] elim: ltE)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
   187
apply (blast intro!: Ord_UN elim: ltE)
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
   188
apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN Card_csucc])
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
   189
done
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
   190
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
   191
47071
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   192
subsection{*The Main Result for Infinite-Branching Datatypes*}
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
   193
47071
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   194
text{*As above, but the index set need not be a cardinal. Work
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   195
backwards along the injection from @{term W} into @{term K}, given
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   196
that @{term"W\<noteq>0"}.*}
46954
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
   197
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
   198
lemma inj_UN_subset:
46954
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
   199
  assumes f: "f \<in> inj(A,B)" and a: "a \<in> A"
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
   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))"
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
   201
proof (rule UN_least)
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
   202
  fix x
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
   203
  assume x: "x \<in> A"
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
   204
  hence fx: "f ` x \<in> B" by (blast intro: f inj_is_fun [THEN apply_type])
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
   205
  have "C(x) \<subseteq> C(if f ` x \<in> range(f) then converse(f) ` (f ` x) else a)" 
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
   206
    using f x by (simp add: inj_is_fun [THEN apply_rangeI])
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
   207
  also have "... \<subseteq> (\<Union>y\<in>B. C(if y \<in> range(f) then converse(f) ` y else a))"
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
   208
    by (rule UN_upper [OF fx]) 
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
   209
  finally show "C(x) \<subseteq> (\<Union>y\<in>B. C(if y \<in> range(f) then converse(f)`y else a))" .
d8b3412cdb99 beautification and structured proofs
paulson
parents: 46821
diff changeset
   210
qed
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
   211
47071
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   212
theorem le_UN_Ord_lt_csucc:
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   213
  assumes IK: "InfCard(K)" and WK: "|W| \<le> K" and j: "\<And>w. w\<in>W \<Longrightarrow> j(w) < csucc(K)"
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   214
  shows "(\<Union>w\<in>W. j(w)) < csucc(K)"
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   215
proof -
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   216
  have CK: "Card(K)" 
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   217
    by (simp add: InfCard_is_Card IK)
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   218
  then obtain f where f: "f \<in> inj(W, K)" using WK
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   219
    by(auto simp add: le_Card_iff lepoll_def)
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   220
  have OU: "Ord(\<Union>w\<in>W. j(w))" using j
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   221
    by (blast elim: ltE)
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   222
  note lt_subset_trans [OF _ _ OU, trans]
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   223
  show ?thesis
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   224
    proof (cases "W=0")
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   225
      case True  --{*solve the easy 0 case*}
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   226
      thus ?thesis by (simp add: CK Card_is_Ord Card_csucc Ord_0_lt_csucc)
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   227
    next
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   228
      case False
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   229
        then obtain x where x: "x \<in> W" by blast
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   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))"
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   231
          by (rule inj_UN_subset [OF f x]) 
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   232
        also have "... < csucc(K)" using IK
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   233
          proof (rule cardinal_UN_Ord_lt_csucc)
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   234
            fix k
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   235
            assume "k \<in> K"
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   236
            thus "j(if k \<in> range(f) then converse(f) ` k else x) < csucc(K)" using f x j
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   237
              by (simp add: inj_converse_fun [THEN apply_type])
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   238
          qed
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   239
        finally show ?thesis .
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   240
    qed
2884ee1ffbf0 More structured proofs for infinite cardinalities
paulson
parents: 47052
diff changeset
   241
qed
13134
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
   242
bf37a3049251 converted the AC branch to Isar
paulson
parents: 1478
diff changeset
   243
end