src/ZF/Main_ZFC.ML
author nipkow
Sun, 05 Jan 2003 21:03:14 +0100
changeset 13771 6cd59cc885a1
parent 13137 b642533c7ea4
permissions -rw-r--r--
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12552
d2d2ab3f1f37 separation of the AC part of Main into Main_ZFC, plus a few new lemmas
paulson
parents:
diff changeset
     1
structure Main_ZFC =
d2d2ab3f1f37 separation of the AC part of Main into Main_ZFC, plus a few new lemmas
paulson
parents:
diff changeset
     2
struct
d2d2ab3f1f37 separation of the AC part of Main into Main_ZFC, plus a few new lemmas
paulson
parents:
diff changeset
     3
  val thy = the_context ();
d2d2ab3f1f37 separation of the AC part of Main into Main_ZFC, plus a few new lemmas
paulson
parents:
diff changeset
     4
end;
13137
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
     5
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
     6
(* legacy ML bindings *)
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
     7
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
     8
(* from AC *)
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
     9
val AC_Pi = thm "AC_Pi";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    10
val AC_ball_Pi = thm "AC_ball_Pi";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    11
val AC_Pi_Pow = thm "AC_Pi_Pow";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    12
val AC_func = thm "AC_func";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    13
val non_empty_family = thm "non_empty_family";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    14
val AC_func0 = thm "AC_func0";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    15
val AC_func_Pow = thm "AC_func_Pow";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    16
val AC_Pi0 = thm "AC_Pi0";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    17
val choice_Diff = thm "choice_Diff";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    18
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    19
(* from Zorn *)
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    20
val Union_lemma0 = thm "Union_lemma0";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    21
val Inter_lemma0 = thm "Inter_lemma0";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    22
val increasingD1 = thm "increasingD1";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    23
val increasingD2 = thm "increasingD2";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    24
val TFin_UnionI = thm "TFin_UnionI";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    25
val TFin_is_subset = thm "TFin_is_subset";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    26
val TFin_induct = thm "TFin_induct";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    27
val increasing_trans = thm "increasing_trans";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    28
val TFin_linear_lemma1 = thm "TFin_linear_lemma1";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    29
val TFin_linear_lemma2 = thm "TFin_linear_lemma2";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    30
val TFin_subsetD = thm "TFin_subsetD";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    31
val TFin_subset_linear = thm "TFin_subset_linear";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    32
val equal_next_upper = thm "equal_next_upper";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    33
val equal_next_Union = thm "equal_next_Union";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    34
val chain_subset_Pow = thm "chain_subset_Pow";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    35
val super_subset_chain = thm "super_subset_chain";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    36
val maxchain_subset_chain = thm "maxchain_subset_chain";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    37
val choice_super = thm "choice_super";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    38
val choice_not_equals = thm "choice_not_equals";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    39
val Hausdorff_next_exists = thm "Hausdorff_next_exists";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    40
val TFin_chain_lemma4 = thm "TFin_chain_lemma4";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    41
val Hausdorff = thm "Hausdorff";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    42
val chain_extend = thm "chain_extend";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    43
val Zorn = thm "Zorn";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    44
val TFin_well_lemma5 = thm "TFin_well_lemma5";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    45
val well_ord_TFin_lemma = thm "well_ord_TFin_lemma";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    46
val well_ord_TFin = thm "well_ord_TFin";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    47
val Zermelo_next_exists = thm "Zermelo_next_exists";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    48
val choice_imp_injection = thm "choice_imp_injection";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    49
val AC_well_ord = thm "AC_well_ord";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    50
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    51
(* from Cardinal_AC *)
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    52
val cardinal_eqpoll = thm "cardinal_eqpoll";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    53
val cardinal_idem = thm "cardinal_idem";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    54
val cardinal_eqE = thm "cardinal_eqE";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    55
val cardinal_eqpoll_iff = thm "cardinal_eqpoll_iff";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    56
val cardinal_disjoint_Un = thm "cardinal_disjoint_Un";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    57
val lepoll_imp_Card_le = thm "lepoll_imp_Card_le";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    58
val cadd_assoc = thm "cadd_assoc";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    59
val cmult_assoc = thm "cmult_assoc";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    60
val cadd_cmult_distrib = thm "cadd_cmult_distrib";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    61
val InfCard_square_eq = thm "InfCard_square_eq";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    62
val Card_le_imp_lepoll = thm "Card_le_imp_lepoll";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    63
val le_Card_iff = thm "le_Card_iff";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    64
val surj_implies_inj = thm "surj_implies_inj";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    65
val surj_implies_cardinal_le = thm "surj_implies_cardinal_le";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    66
val cardinal_UN_le = thm "cardinal_UN_le";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    67
val cardinal_UN_lt_csucc = thm "cardinal_UN_lt_csucc";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    68
val cardinal_UN_Ord_lt_csucc = thm "cardinal_UN_Ord_lt_csucc";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    69
val inj_UN_subset = thm "inj_UN_subset";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    70
val le_UN_Ord_lt_csucc = thm "le_UN_Ord_lt_csucc";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    71
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    72
(* from InfDatatype *)
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    73
val fun_Limit_VfromE = thm "fun_Limit_VfromE";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    74
val fun_Vcsucc_lemma = thm "fun_Vcsucc_lemma";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    75
val subset_Vcsucc = thm "subset_Vcsucc";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    76
val fun_Vcsucc = thm "fun_Vcsucc";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    77
val fun_in_Vcsucc = thm "fun_in_Vcsucc";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    78
val fun_in_Vcsucc' = thm "fun_in_Vcsucc'";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    79
val Card_fun_Vcsucc = thm "Card_fun_Vcsucc";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    80
val Card_fun_in_Vcsucc = thm "Card_fun_in_Vcsucc";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    81
val Limit_csucc = thm "Limit_csucc";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    82
val Pair_in_Vcsucc = thm "Pair_in_Vcsucc";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    83
val Inl_in_Vcsucc = thm "Inl_in_Vcsucc";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    84
val Inr_in_Vcsucc = thm "Inr_in_Vcsucc";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    85
val zero_in_Vcsucc = thm "zero_in_Vcsucc";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    86
val nat_into_Vcsucc = thm "nat_into_Vcsucc";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    87
val InfCard_nat_Un_cardinal = thm "InfCard_nat_Un_cardinal";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    88
val le_nat_Un_cardinal = thm "le_nat_Un_cardinal";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    89
val UN_upper_cardinal = thm "UN_upper_cardinal";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    90
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    91
val inf_datatype_intrs = thms "inf_datatype_intros";
b642533c7ea4 conversion of AC branch to Isar
paulson
parents: 12552
diff changeset
    92