src/ZF/Cardinal.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 47101 ded5cc757bc9
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: 1401
diff changeset
     1
(*  Title:      ZF/Cardinal.thy
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     3
    Copyright   1994  University of Cambridge
13328
703de709a64b better document preparation
paulson
parents: 13269
diff changeset
     4
*)
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
     5
13328
703de709a64b better document preparation
paulson
parents: 13269
diff changeset
     6
header{*Cardinal Numbers Without the Axiom of Choice*}
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
     7
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents: 24893
diff changeset
     8
theory Cardinal imports OrderType Finite Nat_ZF Sum begin
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
     9
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 21524
diff changeset
    10
definition
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    11
  (*least ordinal operator*)
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 21524
diff changeset
    12
   Least    :: "(i=>o) => i"    (binder "LEAST " 10)  where
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    13
     "Least(P) == THE i. Ord(i) & P(i) & (\<forall>j. j<i \<longrightarrow> ~P(j))"
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    14
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 21524
diff changeset
    15
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 21524
diff changeset
    16
  eqpoll   :: "[i,i] => o"     (infixl "eqpoll" 50)  where
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
    17
    "A eqpoll B == \<exists>f. f \<in> bij(A,B)"
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    18
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 21524
diff changeset
    19
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 21524
diff changeset
    20
  lepoll   :: "[i,i] => o"     (infixl "lepoll" 50)  where
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
    21
    "A lepoll B == \<exists>f. f \<in> inj(A,B)"
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    22
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 21524
diff changeset
    23
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 21524
diff changeset
    24
  lesspoll :: "[i,i] => o"     (infixl "lesspoll" 50)  where
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    25
    "A lesspoll B == A lepoll B & ~(A eqpoll B)"
832
ad50a9e74eaf Added Krzysztof's constants lesspoll and Finite
lcp
parents: 753
diff changeset
    26
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 21524
diff changeset
    27
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 21524
diff changeset
    28
  cardinal :: "i=>i"           ("|_|")  where
46847
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
    29
    "|A| == (LEAST i. i eqpoll A)"
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    30
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 21524
diff changeset
    31
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 21524
diff changeset
    32
  Finite   :: "i=>o"  where
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    33
    "Finite(A) == \<exists>n\<in>nat. A eqpoll n"
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    34
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 21524
diff changeset
    35
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 21524
diff changeset
    36
  Card     :: "i=>o"  where
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    37
    "Card(i) == (i = |i|)"
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
    38
21524
7843e2fd14a9 updated (binder) syntax/notation;
wenzelm
parents: 16417
diff changeset
    39
notation (xsymbols)
7843e2fd14a9 updated (binder) syntax/notation;
wenzelm
parents: 16417
diff changeset
    40
  eqpoll    (infixl "\<approx>" 50) and
7843e2fd14a9 updated (binder) syntax/notation;
wenzelm
parents: 16417
diff changeset
    41
  lepoll    (infixl "\<lesssim>" 50) and
7843e2fd14a9 updated (binder) syntax/notation;
wenzelm
parents: 16417
diff changeset
    42
  lesspoll  (infixl "\<prec>" 50) and
7843e2fd14a9 updated (binder) syntax/notation;
wenzelm
parents: 16417
diff changeset
    43
  Least     (binder "\<mu>" 10)
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    44
46847
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
    45
notation (HTML)
21524
7843e2fd14a9 updated (binder) syntax/notation;
wenzelm
parents: 16417
diff changeset
    46
  eqpoll    (infixl "\<approx>" 50) and
7843e2fd14a9 updated (binder) syntax/notation;
wenzelm
parents: 16417
diff changeset
    47
  Least     (binder "\<mu>" 10)
7843e2fd14a9 updated (binder) syntax/notation;
wenzelm
parents: 16417
diff changeset
    48
14565
c6dc17aab88a use more symbols in HTML output
kleing
parents: 14153
diff changeset
    49
13357
6f54e992777e Removal of mono.thy
paulson
parents: 13356
diff changeset
    50
subsection{*The Schroeder-Bernstein Theorem*}
6f54e992777e Removal of mono.thy
paulson
parents: 13356
diff changeset
    51
text{*See Davey and Priestly, page 106*}
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    52
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    53
(** Lemma: Banach's Decomposition Theorem **)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    54
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    55
lemma decomp_bnd_mono: "bnd_mono(X, %W. X - g``(Y - f``W))"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    56
by (rule bnd_monoI, blast+)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    57
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    58
lemma Banach_last_equation:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
    59
    "g \<in> Y->X
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    60
     ==> g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) =
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    61
         X - lfp(X, %W. X - g``(Y - f``W))"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    62
apply (rule_tac P = "%u. ?v = X-u"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    63
       in decomp_bnd_mono [THEN lfp_unfold, THEN ssubst])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    64
apply (simp add: double_complement  fun_is_rel [THEN image_subset])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    65
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    66
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    67
lemma decomposition:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
    68
     "[| f \<in> X->Y;  g \<in> Y->X |] ==>
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    69
      \<exists>XA XB YA YB. (XA \<inter> XB = 0) & (XA \<union> XB = X) &
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    70
                      (YA \<inter> YB = 0) & (YA \<union> YB = Y) &
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    71
                      f``XA=YA & g``YB=XB"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    72
apply (intro exI conjI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    73
apply (rule_tac [6] Banach_last_equation)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    74
apply (rule_tac [5] refl)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    75
apply (assumption |
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    76
       rule  Diff_disjoint Diff_partition fun_is_rel image_subset lfp_subset)+
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    77
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    78
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    79
lemma schroeder_bernstein:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
    80
    "[| f \<in> inj(X,Y);  g \<in> inj(Y,X) |] ==> \<exists>h. h \<in> bij(X,Y)"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    81
apply (insert decomposition [of f X Y g])
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    82
apply (simp add: inj_is_fun)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    83
apply (blast intro!: restrict_bij bij_disjoint_Un intro: bij_converse_bij)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    84
(* The instantiation of exI to @{term"restrict(f,XA) \<union> converse(restrict(g,YB))"}
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    85
   is forced by the context!! *)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    86
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    87
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    88
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    89
(** Equipollence is an equivalence relation **)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    90
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
    91
lemma bij_imp_eqpoll: "f \<in> bij(A,B) ==> A \<approx> B"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    92
apply (unfold eqpoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    93
apply (erule exI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    94
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    95
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    96
(*A eqpoll A*)
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 39159
diff changeset
    97
lemmas eqpoll_refl = id_bij [THEN bij_imp_eqpoll, simp]
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    98
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
    99
lemma eqpoll_sym: "X \<approx> Y ==> Y \<approx> X"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   100
apply (unfold eqpoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   101
apply (blast intro: bij_converse_bij)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   102
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   103
46841
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   104
lemma eqpoll_trans [trans]:
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   105
    "[| X \<approx> Y;  Y \<approx> Z |] ==> X \<approx> Z"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   106
apply (unfold eqpoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   107
apply (blast intro: comp_bij)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   108
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   109
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   110
(** Le-pollence is a partial ordering **)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   111
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   112
lemma subset_imp_lepoll: "X<=Y ==> X \<lesssim> Y"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   113
apply (unfold lepoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   114
apply (rule exI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   115
apply (erule id_subset_inj)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   116
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   117
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 39159
diff changeset
   118
lemmas lepoll_refl = subset_refl [THEN subset_imp_lepoll, simp]
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   119
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 39159
diff changeset
   120
lemmas le_imp_lepoll = le_imp_subset [THEN subset_imp_lepoll]
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   121
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   122
lemma eqpoll_imp_lepoll: "X \<approx> Y ==> X \<lesssim> Y"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   123
by (unfold eqpoll_def bij_def lepoll_def, blast)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   124
46841
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   125
lemma lepoll_trans [trans]: "[| X \<lesssim> Y;  Y \<lesssim> Z |] ==> X \<lesssim> Z"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   126
apply (unfold lepoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   127
apply (blast intro: comp_inj)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   128
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   129
46841
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   130
lemma eq_lepoll_trans [trans]: "[| X \<approx> Y;  Y \<lesssim> Z |] ==> X \<lesssim> Z"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   131
 by (blast intro: eqpoll_imp_lepoll lepoll_trans)
46841
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   132
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   133
lemma lepoll_eq_trans [trans]: "[| X \<lesssim> Y;  Y \<approx> Z |] ==> X \<lesssim> Z"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   134
 by (blast intro: eqpoll_imp_lepoll lepoll_trans)
46841
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   135
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   136
(*Asymmetry law*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   137
lemma eqpollI: "[| X \<lesssim> Y;  Y \<lesssim> X |] ==> X \<approx> Y"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   138
apply (unfold lepoll_def eqpoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   139
apply (elim exE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   140
apply (rule schroeder_bernstein, assumption+)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   141
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   142
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   143
lemma eqpollE:
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   144
    "[| X \<approx> Y; [| X \<lesssim> Y; Y \<lesssim> X |] ==> P |] ==> P"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   145
by (blast intro: eqpoll_imp_lepoll eqpoll_sym)
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   146
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   147
lemma eqpoll_iff: "X \<approx> Y \<longleftrightarrow> X \<lesssim> Y & Y \<lesssim> X"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   148
by (blast intro: eqpollI elim!: eqpollE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   149
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   150
lemma lepoll_0_is_0: "A \<lesssim> 0 ==> A = 0"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   151
apply (unfold lepoll_def inj_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   152
apply (blast dest: apply_type)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   153
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   154
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   155
(*@{term"0 \<lesssim> Y"}*)
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 39159
diff changeset
   156
lemmas empty_lepollI = empty_subsetI [THEN subset_imp_lepoll]
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   157
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   158
lemma lepoll_0_iff: "A \<lesssim> 0 \<longleftrightarrow> A=0"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   159
by (blast intro: lepoll_0_is_0 lepoll_refl)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   160
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   161
lemma Un_lepoll_Un:
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   162
    "[| A \<lesssim> B; C \<lesssim> D; B \<inter> D = 0 |] ==> A \<union> C \<lesssim> B \<union> D"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   163
apply (unfold lepoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   164
apply (blast intro: inj_disjoint_Un)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   165
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   166
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   167
(*A eqpoll 0 ==> A=0*)
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 39159
diff changeset
   168
lemmas eqpoll_0_is_0 = eqpoll_imp_lepoll [THEN lepoll_0_is_0]
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   169
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   170
lemma eqpoll_0_iff: "A \<approx> 0 \<longleftrightarrow> A=0"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   171
by (blast intro: eqpoll_0_is_0 eqpoll_refl)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   172
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   173
lemma eqpoll_disjoint_Un:
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   174
    "[| A \<approx> B;  C \<approx> D;  A \<inter> C = 0;  B \<inter> D = 0 |]
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   175
     ==> A \<union> C \<approx> B \<union> D"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   176
apply (unfold eqpoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   177
apply (blast intro: bij_disjoint_Un)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   178
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   179
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   180
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13328
diff changeset
   181
subsection{*lesspoll: contributions by Krzysztof Grabczewski *}
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   182
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   183
lemma lesspoll_not_refl: "~ (i \<prec> i)"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   184
by (simp add: lesspoll_def)
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   185
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   186
lemma lesspoll_irrefl [elim!]: "i \<prec> i ==> P"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   187
by (simp add: lesspoll_def)
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   188
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   189
lemma lesspoll_imp_lepoll: "A \<prec> B ==> A \<lesssim> B"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   190
by (unfold lesspoll_def, blast)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   191
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   192
lemma lepoll_well_ord: "[| A \<lesssim> B; well_ord(B,r) |] ==> \<exists>s. well_ord(A,s)"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   193
apply (unfold lepoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   194
apply (blast intro: well_ord_rvimage)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   195
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   196
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   197
lemma lepoll_iff_leqpoll: "A \<lesssim> B \<longleftrightarrow> A \<prec> B | A \<approx> B"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   198
apply (unfold lesspoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   199
apply (blast intro!: eqpollI elim!: eqpollE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   200
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   201
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   202
lemma inj_not_surj_succ:
47042
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   203
  assumes fi: "f \<in> inj(A, succ(m))" and fns: "f \<notin> surj(A, succ(m))" 
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   204
  shows "\<exists>f. f \<in> inj(A,m)"
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   205
proof -
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   206
  from fi [THEN inj_is_fun] fns 
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   207
  obtain y where y: "y \<in> succ(m)" "\<And>x. x\<in>A \<Longrightarrow> f ` x \<noteq> y"
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   208
    by (auto simp add: surj_def)
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   209
  show ?thesis
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   210
    proof 
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   211
      show "(\<lambda>z\<in>A. if f`z = m then y else f`z) \<in> inj(A, m)" using y fi
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   212
        by (simp add: inj_def) 
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   213
           (auto intro!: if_type [THEN lam_type] intro: Pi_type dest: apply_funtype)
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   214
      qed
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   215
qed
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   216
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   217
(** Variations on transitivity **)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   218
46841
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   219
lemma lesspoll_trans [trans]:
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   220
      "[| X \<prec> Y; Y \<prec> Z |] ==> X \<prec> Z"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   221
apply (unfold lesspoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   222
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   223
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   224
46841
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   225
lemma lesspoll_trans1 [trans]:
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   226
      "[| X \<lesssim> Y; Y \<prec> Z |] ==> X \<prec> Z"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   227
apply (unfold lesspoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   228
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   229
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   230
46841
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   231
lemma lesspoll_trans2 [trans]:
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   232
      "[| X \<prec> Y; Y \<lesssim> Z |] ==> X \<prec> Z"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   233
apply (unfold lesspoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   234
apply (blast elim!: eqpollE intro: eqpollI lepoll_trans)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   235
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   236
46841
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   237
lemma eq_lesspoll_trans [trans]:
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   238
      "[| X \<approx> Y; Y \<prec> Z |] ==> X \<prec> Z"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   239
  by (blast intro: eqpoll_imp_lepoll lesspoll_trans1)
46841
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   240
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   241
lemma lesspoll_eq_trans [trans]:
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   242
      "[| X \<prec> Y; Y \<approx> Z |] ==> X \<prec> Z"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   243
  by (blast intro: eqpoll_imp_lepoll lesspoll_trans2)
46841
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   244
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   245
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   246
(** LEAST -- the least number operator [from HOL/Univ.ML] **)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   247
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   248
lemma Least_equality:
46847
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   249
    "[| P(i);  Ord(i);  !!x. x<i ==> ~P(x) |] ==> (\<mu> x. P(x)) = i"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   250
apply (unfold Least_def)
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   251
apply (rule the_equality, blast)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   252
apply (elim conjE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   253
apply (erule Ord_linear_lt, assumption, blast+)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   254
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   255
47016
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   256
lemma LeastI: 
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   257
  assumes P: "P(i)" and i: "Ord(i)" shows "P(\<mu> x. P(x))"
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   258
proof -
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   259
  { from i have "P(i) \<Longrightarrow> P(\<mu> x. P(x))"
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   260
      proof (induct i rule: trans_induct)
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   261
        case (step i) 
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   262
        show ?case
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   263
          proof (cases "P(\<mu> a. P(a))")
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   264
            case True thus ?thesis .
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   265
          next
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   266
            case False
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   267
            hence "\<And>x. x \<in> i \<Longrightarrow> ~P(x)" using step
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   268
              by blast
47018
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   269
            hence "(\<mu> a. P(a)) = i" using step
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   270
              by (blast intro: Least_equality ltD) 
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   271
            thus ?thesis using step.prems
47016
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   272
              by simp 
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   273
          qed
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   274
      qed
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   275
  }
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   276
  thus ?thesis using P .
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   277
qed
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   278
47018
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   279
text{*The proof is almost identical to the one above!*}
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   280
lemma Least_le: 
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   281
  assumes P: "P(i)" and i: "Ord(i)" shows "(\<mu> x. P(x)) \<le> i"
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   282
proof -
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   283
  { from i have "P(i) \<Longrightarrow> (\<mu> x. P(x)) \<le> i"
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   284
      proof (induct i rule: trans_induct)
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   285
        case (step i) 
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   286
        show ?case
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   287
          proof (cases "(\<mu> a. P(a)) \<le> i")
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   288
            case True thus ?thesis .
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   289
          next
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   290
            case False
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   291
            hence "\<And>x. x \<in> i \<Longrightarrow> ~ (\<mu> a. P(a)) \<le> i" using step
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   292
              by blast
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   293
            hence "(\<mu> a. P(a)) = i" using step
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   294
              by (blast elim: ltE intro: ltI Least_equality lt_trans1)
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   295
            thus ?thesis using step
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   296
              by simp 
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   297
          qed
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   298
      qed
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   299
  }
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   300
  thus ?thesis using P .
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   301
qed
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   302
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   303
(*LEAST really is the smallest*)
46847
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   304
lemma less_LeastE: "[| P(i);  i < (\<mu> x. P(x)) |] ==> Q"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   305
apply (rule Least_le [THEN [2] lt_trans2, THEN lt_irrefl], assumption+)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   306
apply (simp add: lt_Ord)
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   307
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   308
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   309
(*Easier to apply than LeastI: conclusion has only one occurrence of P*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   310
lemma LeastI2:
46847
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   311
    "[| P(i);  Ord(i);  !!j. P(j) ==> Q(j) |] ==> Q(\<mu> j. P(j))"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   312
by (blast intro: LeastI )
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   313
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   314
(*If there is no such P then LEAST is vacuously 0*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   315
lemma Least_0:
46847
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   316
    "[| ~ (\<exists>i. Ord(i) & P(i)) |] ==> (\<mu> x. P(x)) = 0"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   317
apply (unfold Least_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   318
apply (rule the_0, blast)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   319
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   320
46847
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   321
lemma Ord_Least [intro,simp,TC]: "Ord(\<mu> x. P(x))"
47042
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   322
proof (cases "\<exists>i. Ord(i) & P(i)")
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   323
  case True 
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   324
  then obtain i where "P(i)" "Ord(i)"  by auto
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   325
  hence " (\<mu> x. P(x)) \<le> i"  by (rule Least_le) 
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   326
  thus ?thesis
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   327
    by (elim ltE)
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   328
next
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   329
  case False
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   330
  hence "(\<mu> x. P(x)) = 0"  by (rule Least_0)
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   331
  thus ?thesis
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   332
    by auto
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   333
qed
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   334
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   335
47042
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   336
subsection{*Basic Properties of Cardinals*}
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   337
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   338
(*Not needed for simplification, but helpful below*)
46847
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   339
lemma Least_cong: "(!!y. P(y) \<longleftrightarrow> Q(y)) ==> (\<mu> x. P(x)) = (\<mu> x. Q(x))"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   340
by simp
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   341
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   342
(*Need AC to get @{term"X \<lesssim> Y ==> |X| \<le> |Y|"};  see well_ord_lepoll_imp_Card_le
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   343
  Converse also requires AC, but see well_ord_cardinal_eqE*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   344
lemma cardinal_cong: "X \<approx> Y ==> |X| = |Y|"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   345
apply (unfold eqpoll_def cardinal_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   346
apply (rule Least_cong)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   347
apply (blast intro: comp_bij bij_converse_bij)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   348
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   349
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   350
(*Under AC, the premise becomes trivial; one consequence is ||A|| = |A|*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   351
lemma well_ord_cardinal_eqpoll:
47018
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   352
  assumes r: "well_ord(A,r)" shows "|A| \<approx> A"
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   353
proof (unfold cardinal_def)
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   354
  show "(\<mu> i. i \<approx> A) \<approx> A"
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   355
    by (best intro: LeastI Ord_ordertype ordermap_bij bij_converse_bij bij_imp_eqpoll r) 
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   356
qed
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   357
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   358
(* @{term"Ord(A) ==> |A| \<approx> A"} *)
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   359
lemmas Ord_cardinal_eqpoll = well_ord_Memrel [THEN well_ord_cardinal_eqpoll]
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   360
46841
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   361
lemma Ord_cardinal_idem: "Ord(A) \<Longrightarrow> ||A|| = |A|"
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   362
 by (rule Ord_cardinal_eqpoll [THEN cardinal_cong])
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   363
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   364
lemma well_ord_cardinal_eqE:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   365
  assumes woX: "well_ord(X,r)" and woY: "well_ord(Y,s)" and eq: "|X| = |Y|"
46847
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   366
shows "X \<approx> Y"
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   367
proof -
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   368
  have "X \<approx> |X|" by (blast intro: well_ord_cardinal_eqpoll [OF woX] eqpoll_sym)
46847
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   369
  also have "... = |Y|" by (rule eq)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   370
  also have "... \<approx> Y" by (rule well_ord_cardinal_eqpoll [OF woY])
46847
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   371
  finally show ?thesis .
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   372
qed
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   373
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   374
lemma well_ord_cardinal_eqpoll_iff:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   375
     "[| well_ord(X,r);  well_ord(Y,s) |] ==> |X| = |Y| \<longleftrightarrow> X \<approx> Y"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   376
by (blast intro: cardinal_cong well_ord_cardinal_eqE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   377
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   378
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   379
(** Observations from Kunen, page 28 **)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   380
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   381
lemma Ord_cardinal_le: "Ord(i) ==> |i| \<le> i"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   382
apply (unfold cardinal_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   383
apply (erule eqpoll_refl [THEN Least_le])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   384
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   385
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   386
lemma Card_cardinal_eq: "Card(K) ==> |K| = K"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   387
apply (unfold Card_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   388
apply (erule sym)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   389
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   390
46841
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   391
(* Could replace the  @{term"~(j \<approx> i)"}  by  @{term"~(i \<preceq> j)"}. *)
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   392
lemma CardI: "[| Ord(i);  !!j. j<i ==> ~(j \<approx> i) |] ==> Card(i)"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   393
apply (unfold Card_def cardinal_def)
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   394
apply (subst Least_equality)
47018
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   395
apply (blast intro: eqpoll_refl)+
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   396
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   397
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   398
lemma Card_is_Ord: "Card(i) ==> Ord(i)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   399
apply (unfold Card_def cardinal_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   400
apply (erule ssubst)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   401
apply (rule Ord_Least)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   402
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   403
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   404
lemma Card_cardinal_le: "Card(K) ==> K \<le> |K|"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   405
apply (simp (no_asm_simp) add: Card_is_Ord Card_cardinal_eq)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   406
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   407
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   408
lemma Ord_cardinal [simp,intro!]: "Ord(|A|)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   409
apply (unfold cardinal_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   410
apply (rule Ord_Least)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   411
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   412
47018
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   413
text{*The cardinals are the initial ordinals.*}
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   414
lemma Card_iff_initial: "Card(K) \<longleftrightarrow> Ord(K) & (\<forall>j. j<K \<longrightarrow> ~ j \<approx> K)"
47018
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   415
proof -
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   416
  { fix j
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   417
    assume K: "Card(K)" "j \<approx> K"
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   418
    assume "j < K"
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   419
    also have "... = (\<mu> i. i \<approx> K)" using K
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   420
      by (simp add: Card_def cardinal_def)
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   421
    finally have "j < (\<mu> i. i \<approx> K)" .
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   422
    hence "False" using K
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   423
      by (best dest: less_LeastE) 
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   424
  }
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   425
  then show ?thesis
47042
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   426
    by (blast intro: CardI Card_is_Ord) 
47018
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   427
qed
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   428
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   429
lemma lt_Card_imp_lesspoll: "[| Card(a); i<a |] ==> i \<prec> a"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   430
apply (unfold lesspoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   431
apply (drule Card_iff_initial [THEN iffD1])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   432
apply (blast intro!: leI [THEN le_imp_lepoll])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   433
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   434
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   435
lemma Card_0: "Card(0)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   436
apply (rule Ord_0 [THEN CardI])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   437
apply (blast elim!: ltE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   438
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   439
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   440
lemma Card_Un: "[| Card(K);  Card(L) |] ==> Card(K \<union> L)"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   441
apply (rule Ord_linear_le [of K L])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   442
apply (simp_all add: subset_Un_iff [THEN iffD1]  Card_is_Ord le_imp_subset
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   443
                     subset_Un_iff2 [THEN iffD1])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   444
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   445
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   446
(*Infinite unions of cardinals?  See Devlin, Lemma 6.7, page 98*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   447
47101
ded5cc757bc9 proof tidying
paulson
parents: 47042
diff changeset
   448
lemma Card_cardinal [iff]: "Card(|A|)"
46847
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   449
proof (unfold cardinal_def)
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   450
  show "Card(\<mu> i. i \<approx> A)"
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   451
    proof (cases "\<exists>i. Ord (i) & i \<approx> A")
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   452
      case False thus ?thesis           --{*degenerate case*}
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   453
        by (simp add: Least_0 Card_0)
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   454
    next
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   455
      case True                         --{*real case: @{term A} is isomorphic to some ordinal*}
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   456
      then obtain i where i: "Ord(i)" "i \<approx> A" by blast
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   457
      show ?thesis
46847
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   458
        proof (rule CardI [OF Ord_Least], rule notI)
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   459
          fix j
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   460
          assume j: "j < (\<mu> i. i \<approx> A)"
46847
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   461
          assume "j \<approx> (\<mu> i. i \<approx> A)"
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   462
          also have "... \<approx> A" using i by (auto intro: LeastI)
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   463
          finally have "j \<approx> A" .
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   464
          thus False
46847
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   465
            by (rule less_LeastE [OF _ j])
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   466
        qed
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   467
    qed
8740cea39a4a More calculation-based cardinality proofs
paulson
parents: 46841
diff changeset
   468
qed
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   469
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   470
(*Kunen's Lemma 10.5*)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   471
lemma cardinal_eq_lemma:
46841
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   472
  assumes i:"|i| \<le> j" and j: "j \<le> i" shows "|j| = |i|"
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   473
proof (rule eqpollI [THEN cardinal_cong])
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   474
  show "j \<lesssim> i" by (rule le_imp_lepoll [OF j])
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   475
next
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   476
  have Oi: "Ord(i)" using j by (rule le_Ord2)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   477
  hence "i \<approx> |i|"
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   478
    by (blast intro: Ord_cardinal_eqpoll eqpoll_sym)
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   479
  also have "... \<lesssim> j"
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   480
    by (blast intro: le_imp_lepoll i)
46841
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   481
  finally show "i \<lesssim> j" .
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   482
qed
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   483
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   484
lemma cardinal_mono:
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   485
  assumes ij: "i \<le> j" shows "|i| \<le> |j|"
47016
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   486
using Ord_cardinal [of i] Ord_cardinal [of j]
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   487
proof (cases rule: Ord_linear_le)
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   488
  case le thus ?thesis .
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   489
next
47016
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   490
  case ge
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   491
  have i: "Ord(i)" using ij
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   492
    by (simp add: lt_Ord)
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   493
  have ci: "|i| \<le> j"
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   494
    by (blast intro: Ord_cardinal_le ij le_trans i)
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   495
  have "|i| = ||i||"
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   496
    by (auto simp add: Ord_cardinal_idem i)
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   497
  also have "... = |j|"
47016
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   498
    by (rule cardinal_eq_lemma [OF ge ci])
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   499
  finally have "|i| = |j|" .
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   500
  thus ?thesis by simp
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   501
qed
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   502
47016
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   503
text{*Since we have @{term"|succ(nat)| \<le> |nat|"}, the converse of @{text cardinal_mono} fails!*}
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   504
lemma cardinal_lt_imp_lt: "[| |i| < |j|;  Ord(i);  Ord(j) |] ==> i < j"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   505
apply (rule Ord_linear2 [of i j], assumption+)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   506
apply (erule lt_trans2 [THEN lt_irrefl])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   507
apply (erule cardinal_mono)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   508
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   509
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   510
lemma Card_lt_imp_lt: "[| |i| < K;  Ord(i);  Card(K) |] ==> i < K"
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   511
  by (simp (no_asm_simp) add: cardinal_lt_imp_lt Card_is_Ord Card_cardinal_eq)
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   512
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   513
lemma Card_lt_iff: "[| Ord(i);  Card(K) |] ==> (|i| < K) \<longleftrightarrow> (i < K)"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   514
by (blast intro: Card_lt_imp_lt Ord_cardinal_le [THEN lt_trans1])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   515
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   516
lemma Card_le_iff: "[| Ord(i);  Card(K) |] ==> (K \<le> |i|) \<longleftrightarrow> (K \<le> i)"
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13244
diff changeset
   517
by (simp add: Card_lt_iff Card_is_Ord Ord_cardinal not_lt_iff_le [THEN iff_sym])
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   518
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   519
(*Can use AC or finiteness to discharge first premise*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   520
lemma well_ord_lepoll_imp_Card_le:
46841
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   521
  assumes wB: "well_ord(B,r)" and AB: "A \<lesssim> B"
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   522
  shows "|A| \<le> |B|"
47016
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   523
using Ord_cardinal [of A] Ord_cardinal [of B]
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   524
proof (cases rule: Ord_linear_le)
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   525
  case le thus ?thesis .
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   526
next
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   527
  case ge
46841
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   528
  from lepoll_well_ord [OF AB wB]
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   529
  obtain s where s: "well_ord(A, s)" by blast
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   530
  have "B  \<approx> |B|" by (blast intro: wB eqpoll_sym well_ord_cardinal_eqpoll)
47016
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   531
  also have "... \<lesssim> |A|" by (rule le_imp_lepoll [OF ge])
46841
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   532
  also have "... \<approx> A" by (rule well_ord_cardinal_eqpoll [OF s])
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   533
  finally have "B \<lesssim> A" .
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   534
  hence "A \<approx> B" by (blast intro: eqpollI AB)
46841
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   535
  hence "|A| = |B|" by (rule cardinal_cong)
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   536
  thus ?thesis by simp
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   537
qed
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   538
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   539
lemma lepoll_cardinal_le: "[| A \<lesssim> i; Ord(i) |] ==> |A| \<le> i"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   540
apply (rule le_trans)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   541
apply (erule well_ord_Memrel [THEN well_ord_lepoll_imp_Card_le], assumption)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   542
apply (erule Ord_cardinal_le)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   543
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   544
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   545
lemma lepoll_Ord_imp_eqpoll: "[| A \<lesssim> i; Ord(i) |] ==> |A| \<approx> A"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   546
by (blast intro: lepoll_cardinal_le well_ord_Memrel well_ord_cardinal_eqpoll dest!: lepoll_well_ord)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   547
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13784
diff changeset
   548
lemma lesspoll_imp_eqpoll: "[| A \<prec> i; Ord(i) |] ==> |A| \<approx> A"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   549
apply (unfold lesspoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   550
apply (blast intro: lepoll_Ord_imp_eqpoll)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   551
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   552
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   553
lemma cardinal_subset_Ord: "[|A<=i; Ord(i)|] ==> |A| \<subseteq> i"
14046
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13784
diff changeset
   554
apply (drule subset_imp_lepoll [THEN lepoll_cardinal_le])
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13784
diff changeset
   555
apply (auto simp add: lt_def)
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13784
diff changeset
   556
apply (blast intro: Ord_trans)
6616e6c53d48 updating ZF-UNITY with Sidi's new material
paulson
parents: 13784
diff changeset
   557
done
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   558
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13328
diff changeset
   559
subsection{*The finite cardinals *}
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   560
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   561
lemma cons_lepoll_consD:
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   562
 "[| cons(u,A) \<lesssim> cons(v,B);  u\<notin>A;  v\<notin>B |] ==> A \<lesssim> B"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   563
apply (unfold lepoll_def inj_def, safe)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   564
apply (rule_tac x = "\<lambda>x\<in>A. if f`x=v then f`u else f`x" in exI)
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   565
apply (rule CollectI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   566
(*Proving it's in the function space A->B*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   567
apply (rule if_type [THEN lam_type])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   568
apply (blast dest: apply_funtype)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   569
apply (blast elim!: mem_irrefl dest: apply_funtype)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   570
(*Proving it's injective*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   571
apply (simp (no_asm_simp))
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   572
apply blast
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   573
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   574
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   575
lemma cons_eqpoll_consD: "[| cons(u,A) \<approx> cons(v,B);  u\<notin>A;  v\<notin>B |] ==> A \<approx> B"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   576
apply (simp add: eqpoll_iff)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   577
apply (blast intro: cons_lepoll_consD)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   578
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   579
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   580
(*Lemma suggested by Mike Fourman*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   581
lemma succ_lepoll_succD: "succ(m) \<lesssim> succ(n) ==> m \<lesssim> n"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   582
apply (unfold succ_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   583
apply (erule cons_lepoll_consD)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   584
apply (rule mem_not_refl)+
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   585
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   586
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   587
46935
38ecb2dc3636 structured case and induct rules
paulson
parents: 46877
diff changeset
   588
lemma nat_lepoll_imp_le:
38ecb2dc3636 structured case and induct rules
paulson
parents: 46877
diff changeset
   589
     "m \<in> nat ==> n \<in> nat \<Longrightarrow> m \<lesssim> n \<Longrightarrow> m \<le> n"
38ecb2dc3636 structured case and induct rules
paulson
parents: 46877
diff changeset
   590
proof (induct m arbitrary: n rule: nat_induct)
38ecb2dc3636 structured case and induct rules
paulson
parents: 46877
diff changeset
   591
  case 0 thus ?case by (blast intro!: nat_0_le)
38ecb2dc3636 structured case and induct rules
paulson
parents: 46877
diff changeset
   592
next
38ecb2dc3636 structured case and induct rules
paulson
parents: 46877
diff changeset
   593
  case (succ m)
38ecb2dc3636 structured case and induct rules
paulson
parents: 46877
diff changeset
   594
  show ?case  using `n \<in> nat`
38ecb2dc3636 structured case and induct rules
paulson
parents: 46877
diff changeset
   595
    proof (cases rule: natE)
38ecb2dc3636 structured case and induct rules
paulson
parents: 46877
diff changeset
   596
      case 0 thus ?thesis using succ
38ecb2dc3636 structured case and induct rules
paulson
parents: 46877
diff changeset
   597
        by (simp add: lepoll_def inj_def)
38ecb2dc3636 structured case and induct rules
paulson
parents: 46877
diff changeset
   598
    next
38ecb2dc3636 structured case and induct rules
paulson
parents: 46877
diff changeset
   599
      case (succ n') thus ?thesis using succ.hyps ` succ(m) \<lesssim> n`
38ecb2dc3636 structured case and induct rules
paulson
parents: 46877
diff changeset
   600
        by (blast intro!: succ_leI dest!: succ_lepoll_succD)
38ecb2dc3636 structured case and induct rules
paulson
parents: 46877
diff changeset
   601
    qed
38ecb2dc3636 structured case and induct rules
paulson
parents: 46877
diff changeset
   602
qed
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   603
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   604
lemma nat_eqpoll_iff: "[| m \<in> nat; n \<in> nat |] ==> m \<approx> n \<longleftrightarrow> m = n"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   605
apply (rule iffI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   606
apply (blast intro: nat_lepoll_imp_le le_anti_sym elim!: eqpollE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   607
apply (simp add: eqpoll_refl)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   608
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   609
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   610
(*The object of all this work: every natural number is a (finite) cardinal*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   611
lemma nat_into_Card:
47042
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   612
  assumes n: "n \<in> nat" shows "Card(n)"
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   613
proof (unfold Card_def cardinal_def, rule sym)
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   614
  have "Ord(n)" using n  by auto
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   615
  moreover
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   616
  { fix i
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   617
    assume "i < n" "i \<approx> n"
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   618
    hence False using n
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   619
      by (auto simp add: lt_nat_in_nat [THEN nat_eqpoll_iff])
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   620
  }
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   621
  ultimately show "(\<mu> i. i \<approx> n) = n" by (auto intro!: Least_equality) 
cb907612b59c more structured proofs
paulson
parents: 47018
diff changeset
   622
qed
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   623
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   624
lemmas cardinal_0 = nat_0I [THEN nat_into_Card, THEN Card_cardinal_eq, iff]
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   625
lemmas cardinal_1 = nat_1I [THEN nat_into_Card, THEN Card_cardinal_eq, iff]
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   626
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   627
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   628
(*Part of Kunen's Lemma 10.6*)
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   629
lemma succ_lepoll_natE: "[| succ(n) \<lesssim> n;  n \<in> nat |] ==> P"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   630
by (rule nat_lepoll_imp_le [THEN lt_irrefl], auto)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   631
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   632
lemma nat_lepoll_imp_ex_eqpoll_n:
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   633
     "[| n \<in> nat;  nat \<lesssim> X |] ==> \<exists>Y. Y \<subseteq> X & n \<approx> Y"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   634
apply (unfold lepoll_def eqpoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   635
apply (fast del: subsetI subsetCE
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   636
            intro!: subset_SIs
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   637
            dest!: Ord_nat [THEN [2] OrdmemD, THEN [2] restrict_inj]
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   638
            elim!: restrict_bij
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   639
                   inj_is_fun [THEN fun_is_rel, THEN image_subset])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   640
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   641
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   642
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   643
(** lepoll, \<prec> and natural numbers **)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   644
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   645
lemma lepoll_succ: "i \<lesssim> succ(i)"
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   646
  by (blast intro: subset_imp_lepoll)
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   647
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   648
lemma lepoll_imp_lesspoll_succ:
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   649
  assumes A: "A \<lesssim> m" and m: "m \<in> nat"
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   650
  shows "A \<prec> succ(m)"
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   651
proof -
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   652
  { assume "A \<approx> succ(m)"
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   653
    hence "succ(m) \<approx> A" by (rule eqpoll_sym)
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   654
    also have "... \<lesssim> m" by (rule A)
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   655
    finally have "succ(m) \<lesssim> m" .
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   656
    hence False by (rule succ_lepoll_natE) (rule m) }
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   657
  moreover have "A \<lesssim> succ(m)" by (blast intro: lepoll_trans A lepoll_succ)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   658
  ultimately show ?thesis by (auto simp add: lesspoll_def)
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   659
qed
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   660
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   661
lemma lesspoll_succ_imp_lepoll:
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   662
     "[| A \<prec> succ(m); m \<in> nat |] ==> A \<lesssim> m"
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   663
apply (unfold lesspoll_def lepoll_def eqpoll_def bij_def)
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   664
apply (auto dest: inj_not_surj_succ)
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   665
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   666
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   667
lemma lesspoll_succ_iff: "m \<in> nat ==> A \<prec> succ(m) \<longleftrightarrow> A \<lesssim> m"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   668
by (blast intro!: lepoll_imp_lesspoll_succ lesspoll_succ_imp_lepoll)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   669
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   670
lemma lepoll_succ_disj: "[| A \<lesssim> succ(m);  m \<in> nat |] ==> A \<lesssim> m | A \<approx> succ(m)"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   671
apply (rule disjCI)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   672
apply (rule lesspoll_succ_imp_lepoll)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   673
prefer 2 apply assumption
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   674
apply (simp (no_asm_simp) add: lesspoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   675
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   676
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   677
lemma lesspoll_cardinal_lt: "[| A \<prec> i; Ord(i) |] ==> |A| < i"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   678
apply (unfold lesspoll_def, clarify)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   679
apply (frule lepoll_cardinal_le, assumption)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   680
apply (blast intro: well_ord_Memrel well_ord_cardinal_eqpoll [THEN eqpoll_sym]
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   681
             dest: lepoll_well_ord  elim!: leE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   682
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   683
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   684
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13328
diff changeset
   685
subsection{*The first infinite cardinal: Omega, or nat *}
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   686
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   687
(*This implies Kunen's Lemma 10.6*)
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   688
lemma lt_not_lepoll:
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   689
  assumes n: "n<i" "n \<in> nat" shows "~ i \<lesssim> n"
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   690
proof -
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   691
  { assume i: "i \<lesssim> n"
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   692
    have "succ(n) \<lesssim> i" using n
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   693
      by (elim ltE, blast intro: Ord_succ_subsetI [THEN subset_imp_lepoll])
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   694
    also have "... \<lesssim> n" by (rule i)
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   695
    finally have "succ(n) \<lesssim> n" .
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   696
    hence False  by (rule succ_lepoll_natE) (rule n) }
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   697
  thus ?thesis by auto
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   698
qed
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   699
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   700
text{*A slightly weaker version of @{text nat_eqpoll_iff}*}
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   701
lemma Ord_nat_eqpoll_iff:
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   702
  assumes i: "Ord(i)" and n: "n \<in> nat" shows "i \<approx> n \<longleftrightarrow> i=n"
47016
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   703
using i nat_into_Ord [OF n]
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   704
proof (cases rule: Ord_linear_lt)
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   705
  case lt
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   706
  hence  "i \<in> nat" by (rule lt_nat_in_nat) (rule n)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   707
  thus ?thesis by (simp add: nat_eqpoll_iff n)
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   708
next
47016
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   709
  case eq
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   710
  thus ?thesis by (simp add: eqpoll_refl)
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   711
next
47016
15d33549edea more structured case and induction proofs
paulson
parents: 46953
diff changeset
   712
  case gt
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   713
  hence  "~ i \<lesssim> n" using n  by (rule lt_not_lepoll)
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   714
  hence  "~ i \<approx> n" using n  by (blast intro: eqpoll_imp_lepoll)
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   715
  moreover have "i \<noteq> n" using `n<i` by auto
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   716
  ultimately show ?thesis by blast
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   717
qed
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   718
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   719
lemma Card_nat: "Card(nat)"
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   720
proof -
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   721
  { fix i
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   722
    assume i: "i < nat" "i \<approx> nat"
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   723
    hence "~ nat \<lesssim> i"
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   724
      by (simp add: lt_def lt_not_lepoll)
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   725
    hence False using i
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   726
      by (simp add: eqpoll_iff)
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   727
  }
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   728
  hence "(\<mu> i. i \<approx> nat) = nat" by (blast intro: Least_equality eqpoll_refl)
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   729
  thus ?thesis
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   730
    by (auto simp add: Card_def cardinal_def)
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   731
qed
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   732
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   733
(*Allows showing that |i| is a limit cardinal*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   734
lemma nat_le_cardinal: "nat \<le> i ==> nat \<le> |i|"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   735
apply (rule Card_nat [THEN Card_cardinal_eq, THEN subst])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   736
apply (erule cardinal_mono)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   737
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   738
46841
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   739
lemma n_lesspoll_nat: "n \<in> nat ==> n \<prec> nat"
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   740
  by (blast intro: Ord_nat Card_nat ltI lt_Card_imp_lesspoll)
49b91b716cbe Structured and calculation-based proofs (with new trans rules!)
paulson
parents: 46821
diff changeset
   741
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   742
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13328
diff changeset
   743
subsection{*Towards Cardinal Arithmetic *}
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   744
(** Congruence laws for successor, cardinal addition and multiplication **)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   745
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   746
(*Congruence law for  cons  under equipollence*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   747
lemma cons_lepoll_cong:
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   748
    "[| A \<lesssim> B;  b \<notin> B |] ==> cons(a,A) \<lesssim> cons(b,B)"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   749
apply (unfold lepoll_def, safe)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   750
apply (rule_tac x = "\<lambda>y\<in>cons (a,A) . if y=a then b else f`y" in exI)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   751
apply (rule_tac d = "%z. if z \<in> B then converse (f) `z else a" in lam_injective)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   752
apply (safe elim!: consE')
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   753
   apply simp_all
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   754
apply (blast intro: inj_is_fun [THEN apply_type])+
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   755
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   756
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   757
lemma cons_eqpoll_cong:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   758
     "[| A \<approx> B;  a \<notin> A;  b \<notin> B |] ==> cons(a,A) \<approx> cons(b,B)"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   759
by (simp add: eqpoll_iff cons_lepoll_cong)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   760
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   761
lemma cons_lepoll_cons_iff:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   762
     "[| a \<notin> A;  b \<notin> B |] ==> cons(a,A) \<lesssim> cons(b,B)  \<longleftrightarrow>  A \<lesssim> B"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   763
by (blast intro: cons_lepoll_cong cons_lepoll_consD)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   764
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   765
lemma cons_eqpoll_cons_iff:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   766
     "[| a \<notin> A;  b \<notin> B |] ==> cons(a,A) \<approx> cons(b,B)  \<longleftrightarrow>  A \<approx> B"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   767
by (blast intro: cons_eqpoll_cong cons_eqpoll_consD)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   768
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   769
lemma singleton_eqpoll_1: "{a} \<approx> 1"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   770
apply (unfold succ_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   771
apply (blast intro!: eqpoll_refl [THEN cons_eqpoll_cong])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   772
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   773
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   774
lemma cardinal_singleton: "|{a}| = 1"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   775
apply (rule singleton_eqpoll_1 [THEN cardinal_cong, THEN trans])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   776
apply (simp (no_asm) add: nat_into_Card [THEN Card_cardinal_eq])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   777
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   778
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   779
lemma not_0_is_lepoll_1: "A \<noteq> 0 ==> 1 \<lesssim> A"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   780
apply (erule not_emptyE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   781
apply (rule_tac a = "cons (x, A-{x}) " in subst)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   782
apply (rule_tac [2] a = "cons(0,0)" and P= "%y. y \<lesssim> cons (x, A-{x})" in subst)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   783
prefer 3 apply (blast intro: cons_lepoll_cong subset_imp_lepoll, auto)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   784
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   785
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   786
(*Congruence law for  succ  under equipollence*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   787
lemma succ_eqpoll_cong: "A \<approx> B ==> succ(A) \<approx> succ(B)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   788
apply (unfold succ_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   789
apply (simp add: cons_eqpoll_cong mem_not_refl)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   790
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   791
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   792
(*Congruence law for + under equipollence*)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   793
lemma sum_eqpoll_cong: "[| A \<approx> C;  B \<approx> D |] ==> A+B \<approx> C+D"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   794
apply (unfold eqpoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   795
apply (blast intro!: sum_bij)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   796
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   797
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   798
(*Congruence law for * under equipollence*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   799
lemma prod_eqpoll_cong:
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   800
    "[| A \<approx> C;  B \<approx> D |] ==> A*B \<approx> C*D"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   801
apply (unfold eqpoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   802
apply (blast intro!: prod_bij)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   803
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   804
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   805
lemma inj_disjoint_eqpoll:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   806
    "[| f \<in> inj(A,B);  A \<inter> B = 0 |] ==> A \<union> (B - range(f)) \<approx> B"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   807
apply (unfold eqpoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   808
apply (rule exI)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   809
apply (rule_tac c = "%x. if x \<in> A then f`x else x"
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   810
            and d = "%y. if y \<in> range (f) then converse (f) `y else y"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   811
       in lam_bijective)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   812
apply (blast intro!: if_type inj_is_fun [THEN apply_type])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   813
apply (simp (no_asm_simp) add: inj_converse_fun [THEN apply_funtype])
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   814
apply (safe elim!: UnE')
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   815
   apply (simp_all add: inj_is_fun [THEN apply_rangeI])
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   816
apply (blast intro: inj_converse_fun [THEN apply_type])+
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   817
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   818
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   819
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13328
diff changeset
   820
subsection{*Lemmas by Krzysztof Grabczewski*}
c9cfe1638bf2 improved presentation markup
paulson
parents: 13328
diff changeset
   821
c9cfe1638bf2 improved presentation markup
paulson
parents: 13328
diff changeset
   822
(*New proofs using cons_lepoll_cons. Could generalise from succ to cons.*)
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   823
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   824
text{*If @{term A} has at most @{term"n+1"} elements and @{term"a \<in> A"}
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   825
      then @{term"A-{a}"} has at most @{term n}.*}
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   826
lemma Diff_sing_lepoll:
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   827
      "[| a \<in> A;  A \<lesssim> succ(n) |] ==> A - {a} \<lesssim> n"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   828
apply (unfold succ_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   829
apply (rule cons_lepoll_consD)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   830
apply (rule_tac [3] mem_not_refl)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   831
apply (erule cons_Diff [THEN ssubst], safe)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   832
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   833
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   834
text{*If @{term A} has at least @{term"n+1"} elements then @{term"A-{a}"} has at least @{term n}.*}
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   835
lemma lepoll_Diff_sing:
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   836
  assumes A: "succ(n) \<lesssim> A" shows "n \<lesssim> A - {a}"
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   837
proof -
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   838
  have "cons(n,n) \<lesssim> A" using A
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   839
    by (unfold succ_def)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   840
  also have "... \<lesssim> cons(a, A-{a})"
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   841
    by (blast intro: subset_imp_lepoll)
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   842
  finally have "cons(n,n) \<lesssim> cons(a, A-{a})" .
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   843
  thus ?thesis
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   844
    by (blast intro: cons_lepoll_consD mem_irrefl)
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   845
qed
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   846
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   847
lemma Diff_sing_eqpoll: "[| a \<in> A; A \<approx> succ(n) |] ==> A - {a} \<approx> n"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   848
by (blast intro!: eqpollI
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   849
          elim!: eqpollE
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   850
          intro: Diff_sing_lepoll lepoll_Diff_sing)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   851
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   852
lemma lepoll_1_is_sing: "[| A \<lesssim> 1; a \<in> A |] ==> A = {a}"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   853
apply (frule Diff_sing_lepoll, assumption)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   854
apply (drule lepoll_0_is_0)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   855
apply (blast elim: equalityE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   856
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   857
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   858
lemma Un_lepoll_sum: "A \<union> B \<lesssim> A+B"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   859
apply (unfold lepoll_def)
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   860
apply (rule_tac x = "\<lambda>x\<in>A \<union> B. if x\<in>A then Inl (x) else Inr (x)" in exI)
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   861
apply (rule_tac d = "%z. snd (z)" in lam_injective)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   862
apply force
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   863
apply (simp add: Inl_def Inr_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   864
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   865
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   866
lemma well_ord_Un:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   867
     "[| well_ord(X,R); well_ord(Y,S) |] ==> \<exists>T. well_ord(X \<union> Y, T)"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   868
by (erule well_ord_radd [THEN Un_lepoll_sum [THEN lepoll_well_ord]],
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   869
    assumption)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   870
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   871
(*Krzysztof Grabczewski*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   872
lemma disj_Un_eqpoll_sum: "A \<inter> B = 0 ==> A \<union> B \<approx> A + B"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   873
apply (unfold eqpoll_def)
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   874
apply (rule_tac x = "\<lambda>a\<in>A \<union> B. if a \<in> A then Inl (a) else Inr (a)" in exI)
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   875
apply (rule_tac d = "%z. case (%x. x, %x. x, z)" in lam_bijective)
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   876
apply auto
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   877
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   878
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   879
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   880
subsection {*Finite and infinite sets*}
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   881
47018
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   882
lemma eqpoll_imp_Finite_iff: "A \<approx> B ==> Finite(A) \<longleftrightarrow> Finite(B)"
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   883
apply (unfold Finite_def)
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   884
apply (blast intro: eqpoll_trans eqpoll_sym)
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   885
done
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   886
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   887
lemma Finite_0 [simp]: "Finite(0)"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   888
apply (unfold Finite_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   889
apply (blast intro!: eqpoll_refl nat_0I)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   890
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   891
47018
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   892
lemma Finite_cons: "Finite(x) ==> Finite(cons(y,x))"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   893
apply (unfold Finite_def)
47018
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   894
apply (case_tac "y \<in> x")
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   895
apply (simp add: cons_absorb)
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   896
apply (erule bexE)
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   897
apply (rule bexI)
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   898
apply (erule_tac [2] nat_succI)
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   899
apply (simp (no_asm_simp) add: succ_def cons_eqpoll_cong mem_not_refl)
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   900
done
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   901
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   902
lemma Finite_succ: "Finite(x) ==> Finite(succ(x))"
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   903
apply (unfold succ_def)
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   904
apply (erule Finite_cons)
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   905
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   906
47018
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   907
lemma lepoll_nat_imp_Finite:
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   908
  assumes A: "A \<lesssim> n" and n: "n \<in> nat" shows "Finite(A)"
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   909
proof -
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   910
  have "A \<lesssim> n \<Longrightarrow> Finite(A)" using n
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   911
    proof (induct n)
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   912
      case 0
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   913
      hence "A = 0" by (rule lepoll_0_is_0) 
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   914
      thus ?case by simp
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   915
    next
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   916
      case (succ n)
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   917
      hence "A \<lesssim> n \<or> A \<approx> succ(n)" by (blast dest: lepoll_succ_disj)
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   918
      thus ?case using succ by (auto simp add: Finite_def) 
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   919
    qed
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   920
  thus ?thesis using A .
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   921
qed
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   922
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   923
lemma lesspoll_nat_is_Finite:
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   924
     "A \<prec> nat ==> Finite(A)"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   925
apply (unfold Finite_def)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   926
apply (blast dest: ltD lesspoll_cardinal_lt
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   927
                   lesspoll_imp_eqpoll [THEN eqpoll_sym])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   928
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   929
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   930
lemma lepoll_Finite:
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   931
  assumes Y: "Y \<lesssim> X" and X: "Finite(X)" shows "Finite(Y)"
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   932
proof -
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   933
  obtain n where n: "n \<in> nat" "X \<approx> n" using X
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   934
    by (auto simp add: Finite_def)
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   935
  have "Y \<lesssim> X"         by (rule Y)
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   936
  also have "... \<approx> n"  by (rule n)
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   937
  finally have "Y \<lesssim> n" .
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   938
  thus ?thesis using n by (simp add: lepoll_nat_imp_Finite)
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
   939
qed
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   940
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 39159
diff changeset
   941
lemmas subset_Finite = subset_imp_lepoll [THEN lepoll_Finite]
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   942
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   943
lemma Finite_cons_iff [iff]: "Finite(cons(y,x)) \<longleftrightarrow> Finite(x)"
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   944
by (blast intro: Finite_cons subset_Finite)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   945
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   946
lemma Finite_succ_iff [iff]: "Finite(succ(x)) \<longleftrightarrow> Finite(x)"
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   947
by (simp add: succ_def)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   948
47018
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   949
lemma Finite_Int: "Finite(A) | Finite(B) ==> Finite(A \<inter> B)"
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   950
by (blast intro: subset_Finite)
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   951
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   952
lemmas Finite_Diff = Diff_subset [THEN subset_Finite]
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
   953
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   954
lemma nat_le_infinite_Ord:
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   955
      "[| Ord(i);  ~ Finite(i) |] ==> nat \<le> i"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   956
apply (unfold Finite_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   957
apply (erule Ord_nat [THEN [2] Ord_linear2])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   958
prefer 2 apply assumption
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   959
apply (blast intro!: eqpoll_refl elim!: ltE)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   960
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   961
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   962
lemma Finite_imp_well_ord:
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   963
    "Finite(A) ==> \<exists>r. well_ord(A,r)"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   964
apply (unfold Finite_def eqpoll_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   965
apply (blast intro: well_ord_rvimage bij_is_inj well_ord_Memrel nat_into_Ord)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   966
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
   967
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   968
lemma succ_lepoll_imp_not_empty: "succ(x) \<lesssim> y ==> y \<noteq> 0"
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   969
by (fast dest!: lepoll_0_is_0)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   970
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   971
lemma eqpoll_succ_imp_not_empty: "x \<approx> succ(n) ==> x \<noteq> 0"
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   972
by (fast elim!: eqpoll_sym [THEN eqpoll_0_is_0, THEN succ_neq_0])
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   973
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   974
lemma Finite_Fin_lemma [rule_format]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   975
     "n \<in> nat ==> \<forall>A. (A\<approx>n & A \<subseteq> X) \<longrightarrow> A \<in> Fin(X)"
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   976
apply (induct_tac n)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   977
apply (rule allI)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   978
apply (fast intro!: Fin.emptyI dest!: eqpoll_imp_lepoll [THEN lepoll_0_is_0])
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   979
apply (rule allI)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   980
apply (rule impI)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   981
apply (erule conjE)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   982
apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], assumption)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   983
apply (frule Diff_sing_eqpoll, assumption)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   984
apply (erule allE)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   985
apply (erule impE, fast)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   986
apply (drule subsetD, assumption)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   987
apply (drule Fin.consI, assumption)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   988
apply (simp add: cons_Diff)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   989
done
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   990
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   991
lemma Finite_Fin: "[| Finite(A); A \<subseteq> X |] ==> A \<in> Fin(X)"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   992
by (unfold Finite_def, blast intro: Finite_Fin_lemma)
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   993
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   994
lemma Fin_lemma [rule_format]: "n \<in> nat ==> \<forall>A. A \<approx> n \<longrightarrow> A \<in> Fin(A)"
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   995
apply (induct_tac n)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   996
apply (simp add: eqpoll_0_iff, clarify)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
   997
apply (subgoal_tac "\<exists>u. u \<in> A")
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
   998
apply (erule exE)
46471
2289a3869c88 prefer high-level elim_format;
wenzelm
parents: 45602
diff changeset
   999
apply (rule Diff_sing_eqpoll [elim_format])
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1000
prefer 2 apply assumption
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1001
apply assumption
13784
b9f6154427a4 tidying (by script)
paulson
parents: 13615
diff changeset
  1002
apply (rule_tac b = A in cons_Diff [THEN subst], assumption)
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1003
apply (rule Fin.consI, blast)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1004
apply (blast intro: subset_consI [THEN Fin_mono, THEN subsetD])
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1005
(*Now for the lemma assumed above*)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1006
apply (unfold eqpoll_def)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1007
apply (blast intro: bij_converse_bij [THEN bij_is_fun, THEN apply_type])
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1008
done
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1009
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1010
lemma Finite_into_Fin: "Finite(A) ==> A \<in> Fin(A)"
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1011
apply (unfold Finite_def)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1012
apply (blast intro: Fin_lemma)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1013
done
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1014
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1015
lemma Fin_into_Finite: "A \<in> Fin(U) ==> Finite(A)"
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1016
by (fast intro!: Finite_0 Finite_cons elim: Fin_induct)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1017
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
  1018
lemma Finite_Fin_iff: "Finite(A) \<longleftrightarrow> A \<in> Fin(A)"
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1019
by (blast intro: Finite_into_Fin Fin_into_Finite)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1020
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1021
lemma Finite_Un: "[| Finite(A); Finite(B) |] ==> Finite(A \<union> B)"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1022
by (blast intro!: Fin_into_Finite Fin_UnI
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1023
          dest!: Finite_into_Fin
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1024
          intro: Un_upper1 [THEN Fin_mono, THEN subsetD]
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1025
                 Un_upper2 [THEN Fin_mono, THEN subsetD])
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1026
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
  1027
lemma Finite_Un_iff [simp]: "Finite(A \<union> B) \<longleftrightarrow> (Finite(A) & Finite(B))"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1028
by (blast intro: subset_Finite Finite_Un)
14883
ca000a495448 Groups, Rings and supporting lemmas
paulson
parents: 14565
diff changeset
  1029
ca000a495448 Groups, Rings and supporting lemmas
paulson
parents: 14565
diff changeset
  1030
text{*The converse must hold too.*}
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1031
lemma Finite_Union: "[| \<forall>y\<in>X. Finite(y);  Finite(X) |] ==> Finite(\<Union>(X))"
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1032
apply (simp add: Finite_Fin_iff)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1033
apply (rule Fin_UnionI)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1034
apply (erule Fin_induct, simp)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1035
apply (blast intro: Fin.consI Fin_mono [THEN [2] rev_subsetD])
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1036
done
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1037
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1038
(* Induction principle for Finite(A), by Sidi Ehmety *)
13524
604d0f3622d6 *** empty log message ***
wenzelm
parents: 13357
diff changeset
  1039
lemma Finite_induct [case_names 0 cons, induct set: Finite]:
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1040
"[| Finite(A); P(0);
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1041
    !! x B.   [| Finite(B); x \<notin> B; P(B) |] ==> P(cons(x, B)) |]
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1042
 ==> P(A)"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1043
apply (erule Finite_into_Fin [THEN Fin_induct])
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1044
apply (blast intro: Fin_into_Finite)+
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1045
done
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1046
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1047
(*Sidi Ehmety.  The contrapositive says ~Finite(A) ==> ~Finite(A-{a}) *)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1048
lemma Diff_sing_Finite: "Finite(A - {a}) ==> Finite(A)"
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1049
apply (unfold Finite_def)
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
  1050
apply (case_tac "a \<in> A")
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1051
apply (subgoal_tac [2] "A-{a}=A", auto)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1052
apply (rule_tac x = "succ (n) " in bexI)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1053
apply (subgoal_tac "cons (a, A - {a}) = A & cons (n, n) = succ (n) ")
13784
b9f6154427a4 tidying (by script)
paulson
parents: 13615
diff changeset
  1054
apply (drule_tac a = a and b = n in cons_eqpoll_cong)
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1055
apply (auto dest: mem_irrefl)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1056
done
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1057
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1058
(*Sidi Ehmety.  And the contrapositive of this says
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1059
   [| ~Finite(A); Finite(B) |] ==> ~Finite(A-B) *)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1060
lemma Diff_Finite [rule_format]: "Finite(B) ==> Finite(A-B) \<longrightarrow> Finite(A)"
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1061
apply (erule Finite_induct, auto)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
  1062
apply (case_tac "x \<in> A")
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1063
 apply (subgoal_tac [2] "A-cons (x, B) = A - B")
13615
449a70d88b38 Numerous cosmetic changes, prompted by the new simplifier
paulson
parents: 13524
diff changeset
  1064
apply (subgoal_tac "A - cons (x, B) = (A - B) - {x}", simp)
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1065
apply (drule Diff_sing_Finite, auto)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1066
done
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1067
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1068
lemma Finite_RepFun: "Finite(A) ==> Finite(RepFun(A,f))"
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1069
by (erule Finite_induct, simp_all)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1070
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1071
lemma Finite_RepFun_iff_lemma [rule_format]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1072
     "[|Finite(x); !!x y. f(x)=f(y) ==> x=y|]
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1073
      ==> \<forall>A. x = RepFun(A,f) \<longrightarrow> Finite(A)"
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1074
apply (erule Finite_induct)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1075
 apply clarify
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1076
 apply (case_tac "A=0", simp)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1077
 apply (blast del: allE, clarify)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1078
apply (subgoal_tac "\<exists>z\<in>A. x = f(z)")
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1079
 prefer 2 apply (blast del: allE elim: equalityE, clarify)
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1080
apply (subgoal_tac "B = {f(u) . u \<in> A - {z}}")
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1081
 apply (blast intro: Diff_sing_Finite)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1082
apply (thin_tac "\<forall>A. ?P(A) \<longrightarrow> Finite(A)")
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1083
apply (rule equalityI)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1084
 apply (blast intro: elim: equalityE)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1085
apply (blast intro: elim: equalityCE)
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1086
done
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1087
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1088
text{*I don't know why, but if the premise is expressed using meta-connectives
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1089
then  the simplifier cannot prove it automatically in conditional rewriting.*}
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1090
lemma Finite_RepFun_iff:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
  1091
     "(\<forall>x y. f(x)=f(y) \<longrightarrow> x=y) ==> Finite(RepFun(A,f)) \<longleftrightarrow> Finite(A)"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1092
by (blast intro: Finite_RepFun Finite_RepFun_iff_lemma [of _ f])
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1093
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1094
lemma Finite_Pow: "Finite(A) ==> Finite(Pow(A))"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1095
apply (erule Finite_induct)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1096
apply (simp_all add: Pow_insert Finite_Un Finite_RepFun)
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1097
done
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1098
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1099
lemma Finite_Pow_imp_Finite: "Finite(Pow(A)) ==> Finite(A)"
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1100
apply (subgoal_tac "Finite({{x} . x \<in> A})")
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1101
 apply (simp add: Finite_RepFun_iff )
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1102
apply (blast intro: subset_Finite)
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1103
done
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1104
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
  1105
lemma Finite_Pow_iff [iff]: "Finite(Pow(A)) \<longleftrightarrow> Finite(A)"
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1106
by (blast intro: Finite_Pow Finite_Pow_imp_Finite)
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1107
47101
ded5cc757bc9 proof tidying
paulson
parents: 47042
diff changeset
  1108
lemma Finite_cardinal_iff:
ded5cc757bc9 proof tidying
paulson
parents: 47042
diff changeset
  1109
  assumes i: "Ord(i)" shows "Finite(|i|) \<longleftrightarrow> Finite(i)"
ded5cc757bc9 proof tidying
paulson
parents: 47042
diff changeset
  1110
  by (auto simp add: Finite_def) (blast intro: eqpoll_trans eqpoll_sym Ord_cardinal_eqpoll [OF i])+
13244
7b37e218f298 moving some results around
paulson
parents: 13221
diff changeset
  1111
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1112
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1113
(*Krzysztof Grabczewski's proof that the converse of a finite, well-ordered
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1114
  set is well-ordered.  Proofs simplified by lcp. *)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1115
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
  1116
lemma nat_wf_on_converse_Memrel: "n \<in> nat ==> wf[n](converse(Memrel(n)))"
47018
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
  1117
proof (induct n rule: nat_induct)
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
  1118
  case 0 thus ?case by (blast intro: wf_onI)
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
  1119
next
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
  1120
  case (succ x)
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
  1121
  hence wfx: "\<And>Z. Z = 0 \<or> (\<exists>z\<in>Z. \<forall>y. z \<in> y \<and> z \<in> x \<and> y \<in> x \<and> z \<in> x \<longrightarrow> y \<notin> Z)"
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
  1122
    by (simp add: wf_on_def wf_def)  --{*not easy to erase the duplicate @{term"z \<in> x"}!*}
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
  1123
  show ?case
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
  1124
    proof (rule wf_onI)
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
  1125
      fix Z u
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
  1126
      assume Z: "u \<in> Z" "\<forall>z\<in>Z. \<exists>y\<in>Z. \<langle>y, z\<rangle> \<in> converse(Memrel(succ(x)))"
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
  1127
      show False 
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
  1128
        proof (cases "x \<in> Z")
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
  1129
          case True thus False using Z
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
  1130
            by (blast elim: mem_irrefl mem_asym)
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
  1131
          next
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
  1132
          case False thus False using wfx [of Z] Z
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
  1133
            by blast
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
  1134
        qed
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
  1135
    qed
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
  1136
qed
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1137
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
  1138
lemma nat_well_ord_converse_Memrel: "n \<in> nat ==> well_ord(n,converse(Memrel(n)))"
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1139
apply (frule Ord_nat [THEN Ord_in_Ord, THEN well_ord_Memrel])
47018
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
  1140
apply (simp add: well_ord_def tot_ord_converse nat_wf_on_converse_Memrel) 
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1141
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1142
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1143
lemma well_ord_converse:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1144
     "[|well_ord(A,r);
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1145
        well_ord(ordertype(A,r), converse(Memrel(ordertype(A, r)))) |]
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1146
      ==> well_ord(A,converse(r))"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1147
apply (rule well_ord_Int_iff [THEN iffD1])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1148
apply (frule ordermap_bij [THEN bij_is_inj, THEN well_ord_rvimage], assumption)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1149
apply (simp add: rvimage_converse converse_Int converse_prod
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1150
                 ordertype_ord_iso [THEN ord_iso_rvimage_eq])
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1151
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1152
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1153
lemma ordertype_eq_n:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
  1154
  assumes r: "well_ord(A,r)" and A: "A \<approx> n" and n: "n \<in> nat"
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
  1155
  shows "ordertype(A,r) = n"
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
  1156
proof -
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
  1157
  have "ordertype(A,r) \<approx> A"
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
  1158
    by (blast intro: bij_imp_eqpoll bij_converse_bij ordermap_bij r)
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
  1159
  also have "... \<approx> n" by (rule A)
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
  1160
  finally have "ordertype(A,r) \<approx> n" .
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
  1161
  thus ?thesis
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
  1162
    by (simp add: Ord_nat_eqpoll_iff Ord_ordertype n r)
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
  1163
qed
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1164
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
  1165
lemma Finite_well_ord_converse:
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1166
    "[| Finite(A);  well_ord(A,r) |] ==> well_ord(A,converse(r))"
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1167
apply (unfold Finite_def)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1168
apply (rule well_ord_converse, assumption)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1169
apply (blast dest: ordertype_eq_n intro!: nat_well_ord_converse_Memrel)
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1170
done
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1171
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
  1172
lemma nat_into_Finite: "n \<in> nat ==> Finite(n)"
47018
3a2e6b8a2bb8 More structured proofs for cardinalities
paulson
parents: 47016
diff changeset
  1173
  by (auto simp add: Finite_def intro: eqpoll_refl) 
13221
e29378f347e4 conversion of Cardinal, CardinalArith
paulson
parents: 12861
diff changeset
  1174
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
  1175
lemma nat_not_Finite: "~ Finite(nat)"
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
  1176
proof -
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
  1177
  { fix n
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
  1178
    assume n: "n \<in> nat" "nat \<approx> n"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
  1179
    have "n \<in> nat"    by (rule n)
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
  1180
    also have "... = n" using n
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
  1181
      by (simp add: Ord_nat_eqpoll_iff Ord_nat)
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
  1182
    finally have "n \<in> n" .
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
  1183
    hence False
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
  1184
      by (blast elim: mem_irrefl)
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
  1185
  }
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
  1186
  thus ?thesis
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46935
diff changeset
  1187
    by (auto simp add: Finite_def)
46877
059d20d08ff1 Structured proofs in ZF
paulson
parents: 46847
diff changeset
  1188
qed
14076
5cfc8b9fb880 Conversion of AllocBase to new-style
paulson
parents: 14046
diff changeset
  1189
435
ca5356bd315a Addition of cardinals and order types, various tidying
lcp
parents:
diff changeset
  1190
end