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