src/ZF/Cardinal_AC.ML
author lcp
Tue, 26 Jul 1994 13:21:20 +0200
changeset 484 70b789956bd3
child 488 52f7447d4f1b
permissions -rw-r--r--
Axiom of choice, cardinality results, etc.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     1
(*  Title: 	ZF/Cardinal_AC.ML
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     2
    ID:         $Id$
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
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
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     7
*)
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     8
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
     9
open Cardinal_AC;
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    10
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    11
(*** Strengthened versions of existing theorems about cardinals ***)
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    12
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    13
goal Cardinal_AC.thy "|A| eqpoll A";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    14
by (resolve_tac [AC_well_ord RS exE] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    15
by (eresolve_tac [well_ord_cardinal_eqpoll] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    16
val cardinal_eqpoll = result();
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    17
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    18
val cardinal_idem = cardinal_eqpoll RS cardinal_cong;
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    19
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    20
goal Cardinal_AC.thy "!!X Y. |X| = |Y| ==> X eqpoll Y";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    21
by (resolve_tac [AC_well_ord RS exE] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    22
by (resolve_tac [AC_well_ord RS exE] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    23
by (resolve_tac [well_ord_cardinal_eqE] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    24
by (REPEAT_SOME assume_tac);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    25
val cardinal_eqE = result();
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    26
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    27
goal Cardinal_AC.thy "!!A B. A lepoll B ==> |A| le |B|";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    28
by (resolve_tac [AC_well_ord RS exE] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    29
by (eresolve_tac [well_ord_lepoll_imp_le] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    30
by (assume_tac 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    31
val lepoll_imp_le = result();
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    32
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    33
goal Cardinal_AC.thy "(i |+| j) |+| k = i |+| (j |+| k)";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    34
by (resolve_tac [AC_well_ord RS exE] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    35
by (resolve_tac [AC_well_ord RS exE] 1);
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 [well_ord_cadd_assoc] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    38
by (REPEAT_SOME assume_tac);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    39
val cadd_assoc = result();
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    40
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    41
goal Cardinal_AC.thy "(i |*| j) |*| k = i |*| (j |*| k)";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    42
by (resolve_tac [AC_well_ord RS exE] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    43
by (resolve_tac [AC_well_ord RS exE] 1);
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 [well_ord_cmult_assoc] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    46
by (REPEAT_SOME assume_tac);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    47
val cmult_assoc = result();
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    48
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    49
goal Cardinal_AC.thy "!!A. InfCard(|A|) ==> A*A eqpoll A";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    50
by (resolve_tac [AC_well_ord RS exE] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    51
by (eresolve_tac [well_ord_InfCard_square_eq] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    52
by (assume_tac 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    53
val InfCard_square_eq = result();
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    54
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    55
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    56
(*** Other applications of AC ***)
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    57
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    58
goal Cardinal_AC.thy "!!A B. |A| le |B| ==> A lepoll B";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    59
by (resolve_tac [cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll RS 
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    60
		 lepoll_trans] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    61
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
    62
by (resolve_tac [cardinal_eqpoll RS eqpoll_imp_lepoll] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    63
val le_imp_lepoll = result();
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    64
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    65
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
    66
by (eresolve_tac [Card_cardinal_eq RS subst] 1 THEN
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    67
    rtac iffI 1 THEN
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    68
    DEPTH_SOLVE (eresolve_tac [le_imp_lepoll,lepoll_imp_le] 1));
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    69
val le_Card_iff = result();
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    70
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    71
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
    72
by (etac CollectE 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    73
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
    74
by (fast_tac (ZF_cs addSEs [apply_Pair]) 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    75
by (resolve_tac [exI] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    76
by (rtac f_imp_injective 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    77
by (resolve_tac [Pi_type] 1 THEN assume_tac 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    78
by (fast_tac (ZF_cs addDs [apply_type] addEs [memberPiE]) 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    79
by (fast_tac (ZF_cs addDs [apply_type] addEs [apply_equality]) 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    80
val surj_implies_inj = result();
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    81
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    82
(*Kunen's Lemma 10.20*)
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    83
goal Cardinal_AC.thy "!!f. f: surj(X,Y) ==> |Y| le |X|";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    84
by (resolve_tac [lepoll_imp_le] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    85
by (eresolve_tac [surj_implies_inj RS exE] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    86
by (rewtac lepoll_def);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    87
by (eresolve_tac [exI] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    88
val surj_implies_cardinal_le = result();
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    89
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    90
(*Kunen's Lemma 10.21*)
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    91
goal Cardinal_AC.thy
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    92
    "!!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
    93
by (asm_full_simp_tac (ZF_ss addsimps [InfCard_is_Card, le_Card_iff]) 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    94
by (resolve_tac [lepoll_trans] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    95
by (resolve_tac [InfCard_square_eq RS eqpoll_imp_lepoll] 2);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    96
by (asm_simp_tac (ZF_ss addsimps [InfCard_is_Card, Card_cardinal_eq]) 2);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    97
by (rewrite_goals_tac [lepoll_def]);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    98
by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    99
by (etac (AC_ball_Pi RS exE) 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   100
by (resolve_tac [exI] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   101
(*Lemma needed in both subgoals, for a fixed z*)
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   102
by (subgoal_tac
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   103
    "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
   104
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
   105
                    addSEs [LeastI, Ord_in_Ord]) 2);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   106
by (res_inst_tac [("c", "%z. <LEAST i. z:X(i), f ` (LEAST i. z:X(i)) ` z>"),
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   107
		  ("d", "split(%i j. converse(f`i) ` j)")] 
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   108
	lam_injective 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   109
(*Instantiate the lemma proved above*)
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   110
by (ALLGOALS ball_tac);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   111
by (fast_tac (ZF_cs addEs [inj_is_fun RS apply_type]
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   112
                    addDs [apply_type]) 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   113
by (dresolve_tac [apply_type] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   114
by (eresolve_tac [conjunct2] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   115
by (asm_simp_tac (ZF_ss addsimps [left_inverse]) 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   116
val cardinal_UN_le = result();
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   117
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   118
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   119
goal Cardinal_AC.thy
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   120
    "!!K. [| InfCard(K);  ALL i:K. |X(i)| < csucc(K) |] ==> \
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   121
\         |UN i:K. X(i)| < csucc(K)";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   122
by (asm_full_simp_tac 
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   123
    (ZF_ss addsimps [Card_lt_csucc_iff, cardinal_UN_le, 
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   124
		     InfCard_is_Card, Card_cardinal]) 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   125
val cardinal_UN_lt_csucc = result();