src/HOL/Finite_Set.ML
author wenzelm
Thu, 06 Dec 2001 00:38:55 +0100
changeset 12396 2298d5b8e530
child 12693 827818b891c7
permissions -rw-r--r--
renamed theory Finite to Finite_Set and converted;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12396
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
     1
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
     2
(* legacy ML bindings *)
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
     3
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
     4
structure Finites =
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
     5
struct
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
     6
  val intrs = thms "Finites.intros";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
     7
  val elims = thms "Finites.cases";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
     8
  val elim = thm "Finites.cases";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
     9
  val induct = thm "Finites.induct";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    10
  val mk_cases = InductivePackage.the_mk_cases (the_context ()) "Finite_Set.Finites";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    11
  val [emptyI, insertI] = thms "Finites.intros";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    12
end;
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    13
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    14
structure cardR =
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    15
struct
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    16
  val intrs = thms "cardR.intros";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    17
  val elims = thms "cardR.cases";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    18
  val elim = thm "cardR.cases";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    19
  val induct = thm "cardR.induct";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    20
  val mk_cases = InductivePackage.the_mk_cases (the_context ()) "Finite_Set.cardR";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    21
  val [EmptyI, InsertI] = thms "cardR.intros";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    22
end;
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    23
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    24
structure foldSet =
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    25
struct
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    26
  val intrs = thms "foldSet.intros";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    27
  val elims = thms "foldSet.cases";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    28
  val elim = thm "foldSet.cases";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    29
  val induct = thm "foldSet.induct";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    30
  val mk_cases = InductivePackage.the_mk_cases (the_context ()) "Finite_Set.foldSet";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    31
  val [emptyI, insertI] = thms "foldSet.intros";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    32
end;
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    33
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    34
val Diff1_foldSet = thm "Diff1_foldSet";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    35
val bounded_nat_set_is_finite = thm "bounded_nat_set_is_finite";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    36
val cardR_SucD = thm "cardR_SucD";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    37
val cardR_determ = thm "cardR_determ";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    38
val cardR_emptyE = thm "cardR_emptyE";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    39
val cardR_imp_finite = thm "cardR_imp_finite";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    40
val cardR_insertE = thm "cardR_insertE";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    41
val card_0_eq = thm "card_0_eq";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    42
val card_Diff1_le = thm "card_Diff1_le";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    43
val card_Diff1_less = thm "card_Diff1_less";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    44
val card_Diff2_less = thm "card_Diff2_less";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    45
val card_Diff_singleton = thm "card_Diff_singleton";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    46
val card_Diff_singleton_if = thm "card_Diff_singleton_if";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    47
val card_Diff_subset = thm "card_Diff_subset";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    48
val card_Pow = thm "card_Pow";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    49
val card_Suc_Diff1 = thm "card_Suc_Diff1";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    50
val card_Un_Int = thm "card_Un_Int";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    51
val card_Un_disjoint = thm "card_Un_disjoint";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    52
val card_bij_eq = thm "card_bij_eq";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    53
val card_def = thm "card_def";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    54
val card_empty = thm "card_empty";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    55
val card_eq_setsum = thm "card_eq_setsum";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    56
val card_equality = thm "card_equality";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    57
val card_image = thm "card_image";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    58
val card_image_le = thm "card_image_le";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    59
val card_inj_on_le = thm "card_inj_on_le";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    60
val card_insert = thm "card_insert";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    61
val card_insert_disjoint = thm "card_insert_disjoint";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    62
val card_insert_if = thm "card_insert_if";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    63
val card_insert_le = thm "card_insert_le";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    64
val card_mono = thm "card_mono";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    65
val card_psubset = thm "card_psubset";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    66
val card_s_0_eq_empty = thm "card_s_0_eq_empty";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    67
val card_seteq = thm "card_seteq";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    68
val choose_deconstruct = thm "choose_deconstruct";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    69
val constr_bij = thm "constr_bij";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    70
val dvd_partition = thm "dvd_partition";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    71
val empty_foldSetE = thm "empty_foldSetE";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    72
val endo_inj_surj = thm "endo_inj_surj";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    73
val finite = thm "finite";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    74
val finiteI = thm "finiteI";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    75
val finite_Diff = thm "finite_Diff";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    76
val finite_Diff_insert = thm "finite_Diff_insert";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    77
val finite_Field = thm "finite_Field";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    78
val finite_Int = thm "finite_Int";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    79
val finite_Pow_iff = thm "finite_Pow_iff";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    80
val finite_Prod_UNIV = thm "finite_Prod_UNIV";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    81
val finite_SigmaI = thm "finite_SigmaI";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    82
val finite_UN = thm "finite_UN";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    83
val finite_UN_I = thm "finite_UN_I";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    84
val finite_Un = thm "finite_Un";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    85
val finite_UnI = thm "finite_UnI";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    86
val finite_atMost = thm "finite_atMost";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    87
val finite_converse = thm "finite_converse";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    88
val finite_empty_induct = thm "finite_empty_induct";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    89
val finite_imageD = thm "finite_imageD";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    90
val finite_imageI = thm "finite_imageI";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    91
val finite_imp_cardR = thm "finite_imp_cardR";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    92
val finite_imp_foldSet = thm "finite_imp_foldSet";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    93
val finite_induct = thm "finite_induct";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    94
val finite_insert = thm "finite_insert";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    95
val finite_lessThan = thm "finite_lessThan";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    96
val finite_range_imageI = thm "finite_range_imageI";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    97
val finite_subset = thm "finite_subset";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    98
val finite_subset_induct = thm "finite_subset_induct";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
    99
val finite_trancl = thm "finite_trancl";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   100
val foldSet_determ = thm "foldSet_determ";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   101
val foldSet_imp_finite = thm "foldSet_imp_finite";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   102
val fold_Un_Int = thm "fold_Un_Int";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   103
val fold_Un_disjoint = thm "fold_Un_disjoint";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   104
val fold_Un_disjoint2 = thm "fold_Un_disjoint2";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   105
val fold_commute = thm "fold_commute";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   106
val fold_def = thm "fold_def";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   107
val fold_empty = thm "fold_empty";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   108
val fold_equality = thm "fold_equality";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   109
val fold_insert = thm "fold_insert";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   110
val fold_nest_Un_Int = thm "fold_nest_Un_Int";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   111
val fold_nest_Un_disjoint = thm "fold_nest_Un_disjoint";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   112
val n_sub_lemma = thm "n_sub_lemma";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   113
val n_subsets = thm "n_subsets";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   114
val psubset_card_mono = thm "psubset_card_mono";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   115
val setsum_0 = thm "setsum_0";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   116
val setsum_SucD = thm "setsum_SucD";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   117
val setsum_UN_disjoint = thm "setsum_UN_disjoint";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   118
val setsum_Un = thm "setsum_Un";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   119
val setsum_Un_Int = thm "setsum_Un_Int";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   120
val setsum_Un_disjoint = thm "setsum_Un_disjoint";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   121
val setsum_addf = thm "setsum_addf";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   122
val setsum_cong = thm "setsum_cong";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   123
val setsum_def = thm "setsum_def";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   124
val setsum_diff1 = thm "setsum_diff1";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   125
val setsum_empty = thm "setsum_empty";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   126
val setsum_eq_0_iff = thm "setsum_eq_0_iff";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   127
val setsum_insert = thm "setsum_insert";
2298d5b8e530 renamed theory Finite to Finite_Set and converted;
wenzelm
parents:
diff changeset
   128
val trancl_subset_Field2 = thm "trancl_subset_Field2";