src/ZF/Cardinal_AC.ML
author clasohm
Tue, 30 Jan 1996 13:42:57 +0100
changeset 1461 6bcb44e4d6e5
parent 1092 fdaf39a47a2b
child 1609 5324067d993f
permissions -rw-r--r--
expanded tabs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
     1
(*  Title:      ZF/Cardinal_AC.ML
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     5
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     6
Cardinal arithmetic WITH the Axiom of Choice
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
     7
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
     8
These results help justify infinite-branching datatypes
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     9
*)
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    10
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    11
open Cardinal_AC;
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    12
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    13
(*** Strengthened versions of existing theorems about cardinals ***)
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    14
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    15
goal Cardinal_AC.thy "|A| eqpoll A";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    16
by (resolve_tac [AC_well_ord RS exE] 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
    17
by (etac well_ord_cardinal_eqpoll 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 754
diff changeset
    18
qed "cardinal_eqpoll";
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    19
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    20
val cardinal_idem = cardinal_eqpoll RS cardinal_cong;
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    21
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    22
goal Cardinal_AC.thy "!!X Y. |X| = |Y| ==> X eqpoll Y";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    23
by (resolve_tac [AC_well_ord RS exE] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    24
by (resolve_tac [AC_well_ord RS exE] 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
    25
by (rtac well_ord_cardinal_eqE 1);
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    26
by (REPEAT_SOME assume_tac);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 754
diff changeset
    27
qed "cardinal_eqE";
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    28
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    29
goal Cardinal_AC.thy "!!A B. A lepoll B ==> |A| le |B|";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    30
by (resolve_tac [AC_well_ord RS exE] 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
    31
by (etac well_ord_lepoll_imp_Card_le 1);
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    32
by (assume_tac 1);
766
f811d04fa4dd le_imp_lepoll: renamed to Card_le_imp_lepoll
lcp
parents: 760
diff changeset
    33
qed "lepoll_imp_Card_le";
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    34
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    35
goal Cardinal_AC.thy "(i |+| j) |+| k = i |+| (j |+| k)";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    36
by (resolve_tac [AC_well_ord RS exE] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    37
by (resolve_tac [AC_well_ord RS exE] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    38
by (resolve_tac [AC_well_ord RS exE] 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
    39
by (rtac well_ord_cadd_assoc 1);
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    40
by (REPEAT_SOME assume_tac);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 754
diff changeset
    41
qed "cadd_assoc";
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    42
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    43
goal Cardinal_AC.thy "(i |*| j) |*| k = i |*| (j |*| k)";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    44
by (resolve_tac [AC_well_ord RS exE] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    45
by (resolve_tac [AC_well_ord RS exE] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    46
by (resolve_tac [AC_well_ord RS exE] 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
    47
by (rtac well_ord_cmult_assoc 1);
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    48
by (REPEAT_SOME assume_tac);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 754
diff changeset
    49
qed "cmult_assoc";
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    50
847
e50a32a4f669 Proved cadd_cmult_distrib.
lcp
parents: 785
diff changeset
    51
goal Cardinal_AC.thy "(i |+| j) |*| k = (i |*| k) |+| (j |*| k)";
e50a32a4f669 Proved cadd_cmult_distrib.
lcp
parents: 785
diff changeset
    52
by (resolve_tac [AC_well_ord RS exE] 1);
e50a32a4f669 Proved cadd_cmult_distrib.
lcp
parents: 785
diff changeset
    53
by (resolve_tac [AC_well_ord RS exE] 1);
e50a32a4f669 Proved cadd_cmult_distrib.
lcp
parents: 785
diff changeset
    54
by (resolve_tac [AC_well_ord RS exE] 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
    55
by (rtac well_ord_cadd_cmult_distrib 1);
847
e50a32a4f669 Proved cadd_cmult_distrib.
lcp
parents: 785
diff changeset
    56
by (REPEAT_SOME assume_tac);
e50a32a4f669 Proved cadd_cmult_distrib.
lcp
parents: 785
diff changeset
    57
qed "cadd_cmult_distrib";
e50a32a4f669 Proved cadd_cmult_distrib.
lcp
parents: 785
diff changeset
    58
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    59
goal Cardinal_AC.thy "!!A. InfCard(|A|) ==> A*A eqpoll A";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    60
by (resolve_tac [AC_well_ord RS exE] 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
    61
by (etac well_ord_InfCard_square_eq 1);
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    62
by (assume_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 754
diff changeset
    63
qed "InfCard_square_eq";
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    64
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    65
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    66
(*** Other applications of AC ***)
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    67
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    68
goal Cardinal_AC.thy "!!A B. |A| le |B| ==> A lepoll B";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    69
by (resolve_tac [cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll RS 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
    70
                 lepoll_trans] 1);
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    71
by (eresolve_tac [le_imp_subset RS subset_imp_lepoll RS lepoll_trans] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    72
by (resolve_tac [cardinal_eqpoll RS eqpoll_imp_lepoll] 1);
766
f811d04fa4dd le_imp_lepoll: renamed to Card_le_imp_lepoll
lcp
parents: 760
diff changeset
    73
qed "Card_le_imp_lepoll";
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    74
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    75
goal Cardinal_AC.thy "!!A K. Card(K) ==> |A| le K <-> A lepoll K";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    76
by (eresolve_tac [Card_cardinal_eq RS subst] 1 THEN
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    77
    rtac iffI 1 THEN
766
f811d04fa4dd le_imp_lepoll: renamed to Card_le_imp_lepoll
lcp
parents: 760
diff changeset
    78
    DEPTH_SOLVE (eresolve_tac [Card_le_imp_lepoll,lepoll_imp_Card_le] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 754
diff changeset
    79
qed "le_Card_iff";
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    80
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    81
goalw Cardinal_AC.thy [surj_def] "!!f. f: surj(X,Y) ==> EX g. g: inj(Y,X)";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    82
by (etac CollectE 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    83
by (res_inst_tac [("A1", "Y"), ("B1", "%y. f-``{y}")] (AC_Pi RS exE) 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    84
by (fast_tac (ZF_cs addSEs [apply_Pair]) 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
    85
by (rtac exI 1);
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    86
by (rtac f_imp_injective 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
    87
by (rtac Pi_type 1 THEN assume_tac 1);
683
8fe0fbd76887 Cardinal_AC/surj_implies_inj: uses Pi_memberD instead of memberPiE
lcp
parents: 517
diff changeset
    88
by (fast_tac (ZF_cs addDs [apply_type] addDs [Pi_memberD]) 1);
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    89
by (fast_tac (ZF_cs addDs [apply_type] addEs [apply_equality]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 754
diff changeset
    90
qed "surj_implies_inj";
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    91
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    92
(*Kunen's Lemma 10.20*)
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    93
goal Cardinal_AC.thy "!!f. f: surj(X,Y) ==> |Y| le |X|";
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
    94
by (rtac lepoll_imp_Card_le 1);
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    95
by (eresolve_tac [surj_implies_inj RS exE] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    96
by (rewtac lepoll_def);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
    97
by (etac exI 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 754
diff changeset
    98
qed "surj_implies_cardinal_le";
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    99
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   100
(*Kunen's Lemma 10.21*)
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   101
goal Cardinal_AC.thy
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   102
    "!!K. [| InfCard(K);  ALL i:K. |X(i)| le K |] ==> |UN i:K. X(i)| le K";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   103
by (asm_full_simp_tac (ZF_ss addsimps [InfCard_is_Card, le_Card_iff]) 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
   104
by (rtac lepoll_trans 1);
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   105
by (resolve_tac [InfCard_square_eq RS eqpoll_imp_lepoll] 2);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   106
by (asm_simp_tac (ZF_ss addsimps [InfCard_is_Card, Card_cardinal_eq]) 2);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
   107
by (rewtac lepoll_def);
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   108
by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   109
by (etac (AC_ball_Pi RS exE) 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
   110
by (rtac exI 1);
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   111
(*Lemma needed in both subgoals, for a fixed z*)
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   112
by (subgoal_tac
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   113
    "ALL z: (UN i:K. X(i)). z: X(LEAST i. z:X(i)) & (LEAST i. z:X(i)) : K" 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   114
by (fast_tac (ZF_cs addSIs [Least_le RS lt_trans1 RS ltD, ltI]
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   115
                    addSEs [LeastI, Ord_in_Ord]) 2);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   116
by (res_inst_tac [("c", "%z. <LEAST i. z:X(i), f ` (LEAST i. z:X(i)) ` z>"),
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
   117
                  ("d", "%<i,j>. converse(f`i) ` j")] 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
   118
        lam_injective 1);
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   119
(*Instantiate the lemma proved above*)
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   120
by (ALLGOALS ball_tac);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   121
by (fast_tac (ZF_cs addEs [inj_is_fun RS apply_type]
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   122
                    addDs [apply_type]) 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
   123
by (dtac apply_type 1);
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
   124
by (etac conjunct2 1);
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   125
by (asm_simp_tac (ZF_ss addsimps [left_inverse]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 754
diff changeset
   126
qed "cardinal_UN_le";
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   127
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
   128
(*The same again, using csucc*)
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   129
goal Cardinal_AC.thy
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   130
    "!!K. [| InfCard(K);  ALL i:K. |X(i)| < csucc(K) |] ==> \
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   131
\         |UN i:K. X(i)| < csucc(K)";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   132
by (asm_full_simp_tac 
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   133
    (ZF_ss addsimps [Card_lt_csucc_iff, cardinal_UN_le, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
   134
                     InfCard_is_Card, Card_cardinal]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 754
diff changeset
   135
qed "cardinal_UN_lt_csucc";
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
   136
785
c2ef808dc938 cardinal_UN_Ord_lt_csucc: added comment
lcp
parents: 766
diff changeset
   137
(*The same again, for a union of ordinals.  In use, j(i) is a bit like rank(i),
c2ef808dc938 cardinal_UN_Ord_lt_csucc: added comment
lcp
parents: 766
diff changeset
   138
  the least ordinal j such that i:Vfrom(A,j). *)
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
   139
goal Cardinal_AC.thy
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
   140
    "!!K. [| InfCard(K);  ALL i:K. j(i) < csucc(K) |] ==> \
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
   141
\         (UN i:K. j(i)) < csucc(K)";
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
   142
by (resolve_tac [cardinal_UN_lt_csucc RS Card_lt_imp_lt] 1);
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
   143
by (assume_tac 1);
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
   144
by (fast_tac (ZF_cs addIs [Ord_cardinal_le RS lt_trans1] addEs [ltE]) 1);
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
   145
by (fast_tac (ZF_cs addSIs [Ord_UN] addEs [ltE]) 1);
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
   146
by (eresolve_tac [InfCard_is_Card RS Card_is_Ord RS Card_csucc] 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 754
diff changeset
   147
qed "cardinal_UN_Ord_lt_csucc";
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
   148
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   149
785
c2ef808dc938 cardinal_UN_Ord_lt_csucc: added comment
lcp
parents: 766
diff changeset
   150
(** Main result for infinite-branching datatypes.  As above, but the index
c2ef808dc938 cardinal_UN_Ord_lt_csucc: added comment
lcp
parents: 766
diff changeset
   151
    set need not be a cardinal.  Surprisingly complicated proof!
c2ef808dc938 cardinal_UN_Ord_lt_csucc: added comment
lcp
parents: 766
diff changeset
   152
**)
c2ef808dc938 cardinal_UN_Ord_lt_csucc: added comment
lcp
parents: 766
diff changeset
   153
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   154
(*Saves checking Ord(j) below*)
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   155
goal Ordinal.thy "!!i j. [| i <= j;  j<k;  Ord(i) |] ==> i<k";
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   156
by (resolve_tac [subset_imp_le RS lt_trans1] 1);
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   157
by (REPEAT (eresolve_tac [asm_rl, ltE] 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 754
diff changeset
   158
qed "lt_subset_trans";
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   159
785
c2ef808dc938 cardinal_UN_Ord_lt_csucc: added comment
lcp
parents: 766
diff changeset
   160
(*Work backwards along the injection from W into K, given that W~=0.*)
c2ef808dc938 cardinal_UN_Ord_lt_csucc: added comment
lcp
parents: 766
diff changeset
   161
goal Perm.thy 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
   162
    "!!A. [| f: inj(A,B);  a:A |] ==>           \
785
c2ef808dc938 cardinal_UN_Ord_lt_csucc: added comment
lcp
parents: 766
diff changeset
   163
\         (UN x:A. C(x)) <= (UN y:B. C(if(y: range(f), converse(f)`y, a)))";
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
   164
by (rtac UN_least 1);
785
c2ef808dc938 cardinal_UN_Ord_lt_csucc: added comment
lcp
parents: 766
diff changeset
   165
by (res_inst_tac [("x1", "f`x")] (UN_upper RSN (2,subset_trans)) 1);
c2ef808dc938 cardinal_UN_Ord_lt_csucc: added comment
lcp
parents: 766
diff changeset
   166
by (eresolve_tac [inj_is_fun RS apply_type] 2 THEN assume_tac 2);
c2ef808dc938 cardinal_UN_Ord_lt_csucc: added comment
lcp
parents: 766
diff changeset
   167
by (asm_simp_tac 
c2ef808dc938 cardinal_UN_Ord_lt_csucc: added comment
lcp
parents: 766
diff changeset
   168
    (ZF_ss addsimps [inj_is_fun RS apply_rangeI, left_inverse]) 1);
c2ef808dc938 cardinal_UN_Ord_lt_csucc: added comment
lcp
parents: 766
diff changeset
   169
val inj_UN_subset = result();
c2ef808dc938 cardinal_UN_Ord_lt_csucc: added comment
lcp
parents: 766
diff changeset
   170
c2ef808dc938 cardinal_UN_Ord_lt_csucc: added comment
lcp
parents: 766
diff changeset
   171
(*Simpler to require |W|=K; we'd have a bijection; but the theorem would
c2ef808dc938 cardinal_UN_Ord_lt_csucc: added comment
lcp
parents: 766
diff changeset
   172
  be weaker.*)
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   173
goal Cardinal_AC.thy
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   174
    "!!K. [| InfCard(K);  |W| le K;  ALL w:W. j(w) < csucc(K) |] ==> \
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   175
\         (UN w:W. j(w)) < csucc(K)";
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   176
by (excluded_middle_tac "W=0" 1);
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
   177
by (asm_simp_tac        (*solve the easy 0 case*)
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   178
    (ZF_ss addsimps [UN_0, InfCard_is_Card, Card_is_Ord RS Card_csucc, 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
   179
                     Card_is_Ord, Ord_0_lt_csucc]) 2);
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   180
by (asm_full_simp_tac
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   181
    (ZF_ss addsimps [InfCard_is_Card, le_Card_iff, lepoll_def]) 1);
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   182
by (safe_tac eq_cs);
785
c2ef808dc938 cardinal_UN_Ord_lt_csucc: added comment
lcp
parents: 766
diff changeset
   183
by (swap_res_tac [[inj_UN_subset, cardinal_UN_Ord_lt_csucc] 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
   184
                  MRS lt_subset_trans] 1);
785
c2ef808dc938 cardinal_UN_Ord_lt_csucc: added comment
lcp
parents: 766
diff changeset
   185
by (REPEAT (assume_tac 1));
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   186
by (fast_tac (ZF_cs addSIs [Ord_UN] addEs [ltE]) 2);
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   187
by (asm_simp_tac (ZF_ss addsimps [inj_converse_fun RS apply_type]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1092
diff changeset
   188
                        setloop split_tac [expand_if]) 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 754
diff changeset
   189
qed "le_UN_Ord_lt_csucc";
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   190