src/ZF/Cardinal_AC.ML
author lcp
Fri, 12 Aug 1994 18:45:33 +0200
changeset 517 a9f93400f307
parent 516 1957113f0d7d
child 683 8fe0fbd76887
permissions -rw-r--r--
for infinite datatypes with arbitrary index sets
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
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);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    17
by (eresolve_tac [well_ord_cardinal_eqpoll] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    18
val cardinal_eqpoll = result();
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);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    25
by (resolve_tac [well_ord_cardinal_eqE] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    26
by (REPEAT_SOME assume_tac);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    27
val cardinal_eqE = result();
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);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    31
by (eresolve_tac [well_ord_lepoll_imp_le] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    32
by (assume_tac 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    33
val lepoll_imp_le = result();
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);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    39
by (resolve_tac [well_ord_cadd_assoc] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    40
by (REPEAT_SOME assume_tac);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    41
val cadd_assoc = result();
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);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    47
by (resolve_tac [well_ord_cmult_assoc] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    48
by (REPEAT_SOME assume_tac);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    49
val cmult_assoc = result();
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    50
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    51
goal Cardinal_AC.thy "!!A. InfCard(|A|) ==> A*A eqpoll A";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    52
by (resolve_tac [AC_well_ord RS exE] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    53
by (eresolve_tac [well_ord_InfCard_square_eq] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    54
by (assume_tac 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    55
val InfCard_square_eq = result();
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    56
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    57
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    58
(*** Other applications of AC ***)
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    59
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    60
goal Cardinal_AC.thy "!!A B. |A| le |B| ==> A lepoll B";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    61
by (resolve_tac [cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll RS 
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    62
		 lepoll_trans] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    63
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
    64
by (resolve_tac [cardinal_eqpoll RS eqpoll_imp_lepoll] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    65
val le_imp_lepoll = result();
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    66
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    67
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
    68
by (eresolve_tac [Card_cardinal_eq RS subst] 1 THEN
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    69
    rtac iffI 1 THEN
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    70
    DEPTH_SOLVE (eresolve_tac [le_imp_lepoll,lepoll_imp_le] 1));
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    71
val le_Card_iff = result();
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    72
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    73
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
    74
by (etac CollectE 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    75
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
    76
by (fast_tac (ZF_cs addSEs [apply_Pair]) 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    77
by (resolve_tac [exI] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    78
by (rtac f_imp_injective 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    79
by (resolve_tac [Pi_type] 1 THEN assume_tac 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    80
by (fast_tac (ZF_cs addDs [apply_type] addEs [memberPiE]) 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    81
by (fast_tac (ZF_cs addDs [apply_type] addEs [apply_equality]) 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    82
val surj_implies_inj = result();
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    83
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    84
(*Kunen's Lemma 10.20*)
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    85
goal Cardinal_AC.thy "!!f. f: surj(X,Y) ==> |Y| le |X|";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    86
by (resolve_tac [lepoll_imp_le] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    87
by (eresolve_tac [surj_implies_inj RS exE] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    88
by (rewtac lepoll_def);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    89
by (eresolve_tac [exI] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    90
val surj_implies_cardinal_le = result();
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.21*)
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    93
goal Cardinal_AC.thy
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    94
    "!!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
    95
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
    96
by (resolve_tac [lepoll_trans] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    97
by (resolve_tac [InfCard_square_eq RS eqpoll_imp_lepoll] 2);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
    98
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
    99
by (rewrite_goals_tac [lepoll_def]);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   100
by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   101
by (etac (AC_ball_Pi RS exE) 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   102
by (resolve_tac [exI] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   103
(*Lemma needed in both subgoals, for a fixed z*)
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   104
by (subgoal_tac
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   105
    "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
   106
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
   107
                    addSEs [LeastI, Ord_in_Ord]) 2);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   108
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
   109
		  ("d", "split(%i j. converse(f`i) ` j)")] 
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   110
	lam_injective 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   111
(*Instantiate the lemma proved above*)
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   112
by (ALLGOALS ball_tac);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   113
by (fast_tac (ZF_cs addEs [inj_is_fun RS apply_type]
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   114
                    addDs [apply_type]) 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   115
by (dresolve_tac [apply_type] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   116
by (eresolve_tac [conjunct2] 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   117
by (asm_simp_tac (ZF_ss addsimps [left_inverse]) 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   118
val cardinal_UN_le = result();
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   119
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
   120
(*The same again, using csucc*)
484
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   121
goal Cardinal_AC.thy
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   122
    "!!K. [| InfCard(K);  ALL i:K. |X(i)| < csucc(K) |] ==> \
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   123
\         |UN i:K. X(i)| < csucc(K)";
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   124
by (asm_full_simp_tac 
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   125
    (ZF_ss addsimps [Card_lt_csucc_iff, cardinal_UN_le, 
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   126
		     InfCard_is_Card, Card_cardinal]) 1);
70b789956bd3 Axiom of choice, cardinality results, etc.
lcp
parents:
diff changeset
   127
val cardinal_UN_lt_csucc = result();
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
   128
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
   129
(*The same again, for a union of ordinals*)
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
   130
goal Cardinal_AC.thy
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
   131
    "!!K. [| InfCard(K);  ALL i:K. j(i) < csucc(K) |] ==> \
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
   132
\         (UN i:K. j(i)) < csucc(K)";
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
   133
by (resolve_tac [cardinal_UN_lt_csucc RS Card_lt_imp_lt] 1);
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
   134
by (assume_tac 1);
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
   135
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
   136
by (fast_tac (ZF_cs addSIs [Ord_UN] addEs [ltE]) 1);
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
   137
by (eresolve_tac [InfCard_is_Card RS Card_is_Ord RS Card_csucc] 1);
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
   138
val cardinal_UN_Ord_lt_csucc = result();
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 484
diff changeset
   139
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   140
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   141
(*Saves checking Ord(j) below*)
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   142
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
   143
by (resolve_tac [subset_imp_le RS lt_trans1] 1);
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   144
by (REPEAT (eresolve_tac [asm_rl, ltE] 1));
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   145
val lt_subset_trans = result();
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   146
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   147
goal Cardinal_AC.thy
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   148
    "!!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
   149
\         (UN w:W. j(w)) < csucc(K)";
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   150
by (excluded_middle_tac "W=0" 1);
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   151
by (asm_simp_tac
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   152
    (ZF_ss addsimps [UN_0, InfCard_is_Card, Card_is_Ord RS Card_csucc, 
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   153
		     Card_is_Ord, Ord_0_lt_csucc]) 2);
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   154
by (asm_full_simp_tac
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   155
    (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
   156
by (safe_tac eq_cs);
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   157
by (eresolve_tac [notE] 1);
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   158
by (res_inst_tac [("j1", "%i. j(if(i: range(f), converse(f)`i, x))")]
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   159
    (cardinal_UN_Ord_lt_csucc RSN (2,lt_subset_trans)) 1);
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   160
by (assume_tac 2);
517
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   161
by (resolve_tac [UN_least] 1);
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   162
by (res_inst_tac [("x1", "f`xa")] (UN_upper RSN (2,subset_trans)) 1);
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   163
by (eresolve_tac [inj_is_fun RS apply_type] 2 THEN assume_tac 2);
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   164
by (asm_simp_tac 
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   165
    (ZF_ss addsimps [inj_is_fun RS apply_rangeI, left_inverse]) 1);
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   166
by (fast_tac (ZF_cs addSIs [Ord_UN] addEs [ltE]) 2);
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   167
by (asm_simp_tac (ZF_ss addsimps [inj_converse_fun RS apply_type]
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   168
		        setloop split_tac [expand_if]) 1);
a9f93400f307 for infinite datatypes with arbitrary index sets
lcp
parents: 516
diff changeset
   169
val le_UN_Ord_lt_csucc = result();
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 488
diff changeset
   170