src/HOL/Finite_Set.ML
changeset 12396 2298d5b8e530
child 12693 827818b891c7
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Finite_Set.ML	Thu Dec 06 00:38:55 2001 +0100
     1.3 @@ -0,0 +1,128 @@
     1.4 +
     1.5 +(* legacy ML bindings *)
     1.6 +
     1.7 +structure Finites =
     1.8 +struct
     1.9 +  val intrs = thms "Finites.intros";
    1.10 +  val elims = thms "Finites.cases";
    1.11 +  val elim = thm "Finites.cases";
    1.12 +  val induct = thm "Finites.induct";
    1.13 +  val mk_cases = InductivePackage.the_mk_cases (the_context ()) "Finite_Set.Finites";
    1.14 +  val [emptyI, insertI] = thms "Finites.intros";
    1.15 +end;
    1.16 +
    1.17 +structure cardR =
    1.18 +struct
    1.19 +  val intrs = thms "cardR.intros";
    1.20 +  val elims = thms "cardR.cases";
    1.21 +  val elim = thm "cardR.cases";
    1.22 +  val induct = thm "cardR.induct";
    1.23 +  val mk_cases = InductivePackage.the_mk_cases (the_context ()) "Finite_Set.cardR";
    1.24 +  val [EmptyI, InsertI] = thms "cardR.intros";
    1.25 +end;
    1.26 +
    1.27 +structure foldSet =
    1.28 +struct
    1.29 +  val intrs = thms "foldSet.intros";
    1.30 +  val elims = thms "foldSet.cases";
    1.31 +  val elim = thm "foldSet.cases";
    1.32 +  val induct = thm "foldSet.induct";
    1.33 +  val mk_cases = InductivePackage.the_mk_cases (the_context ()) "Finite_Set.foldSet";
    1.34 +  val [emptyI, insertI] = thms "foldSet.intros";
    1.35 +end;
    1.36 +
    1.37 +val Diff1_foldSet = thm "Diff1_foldSet";
    1.38 +val bounded_nat_set_is_finite = thm "bounded_nat_set_is_finite";
    1.39 +val cardR_SucD = thm "cardR_SucD";
    1.40 +val cardR_determ = thm "cardR_determ";
    1.41 +val cardR_emptyE = thm "cardR_emptyE";
    1.42 +val cardR_imp_finite = thm "cardR_imp_finite";
    1.43 +val cardR_insertE = thm "cardR_insertE";
    1.44 +val card_0_eq = thm "card_0_eq";
    1.45 +val card_Diff1_le = thm "card_Diff1_le";
    1.46 +val card_Diff1_less = thm "card_Diff1_less";
    1.47 +val card_Diff2_less = thm "card_Diff2_less";
    1.48 +val card_Diff_singleton = thm "card_Diff_singleton";
    1.49 +val card_Diff_singleton_if = thm "card_Diff_singleton_if";
    1.50 +val card_Diff_subset = thm "card_Diff_subset";
    1.51 +val card_Pow = thm "card_Pow";
    1.52 +val card_Suc_Diff1 = thm "card_Suc_Diff1";
    1.53 +val card_Un_Int = thm "card_Un_Int";
    1.54 +val card_Un_disjoint = thm "card_Un_disjoint";
    1.55 +val card_bij_eq = thm "card_bij_eq";
    1.56 +val card_def = thm "card_def";
    1.57 +val card_empty = thm "card_empty";
    1.58 +val card_eq_setsum = thm "card_eq_setsum";
    1.59 +val card_equality = thm "card_equality";
    1.60 +val card_image = thm "card_image";
    1.61 +val card_image_le = thm "card_image_le";
    1.62 +val card_inj_on_le = thm "card_inj_on_le";
    1.63 +val card_insert = thm "card_insert";
    1.64 +val card_insert_disjoint = thm "card_insert_disjoint";
    1.65 +val card_insert_if = thm "card_insert_if";
    1.66 +val card_insert_le = thm "card_insert_le";
    1.67 +val card_mono = thm "card_mono";
    1.68 +val card_psubset = thm "card_psubset";
    1.69 +val card_s_0_eq_empty = thm "card_s_0_eq_empty";
    1.70 +val card_seteq = thm "card_seteq";
    1.71 +val choose_deconstruct = thm "choose_deconstruct";
    1.72 +val constr_bij = thm "constr_bij";
    1.73 +val dvd_partition = thm "dvd_partition";
    1.74 +val empty_foldSetE = thm "empty_foldSetE";
    1.75 +val endo_inj_surj = thm "endo_inj_surj";
    1.76 +val finite = thm "finite";
    1.77 +val finiteI = thm "finiteI";
    1.78 +val finite_Diff = thm "finite_Diff";
    1.79 +val finite_Diff_insert = thm "finite_Diff_insert";
    1.80 +val finite_Field = thm "finite_Field";
    1.81 +val finite_Int = thm "finite_Int";
    1.82 +val finite_Pow_iff = thm "finite_Pow_iff";
    1.83 +val finite_Prod_UNIV = thm "finite_Prod_UNIV";
    1.84 +val finite_SigmaI = thm "finite_SigmaI";
    1.85 +val finite_UN = thm "finite_UN";
    1.86 +val finite_UN_I = thm "finite_UN_I";
    1.87 +val finite_Un = thm "finite_Un";
    1.88 +val finite_UnI = thm "finite_UnI";
    1.89 +val finite_atMost = thm "finite_atMost";
    1.90 +val finite_converse = thm "finite_converse";
    1.91 +val finite_empty_induct = thm "finite_empty_induct";
    1.92 +val finite_imageD = thm "finite_imageD";
    1.93 +val finite_imageI = thm "finite_imageI";
    1.94 +val finite_imp_cardR = thm "finite_imp_cardR";
    1.95 +val finite_imp_foldSet = thm "finite_imp_foldSet";
    1.96 +val finite_induct = thm "finite_induct";
    1.97 +val finite_insert = thm "finite_insert";
    1.98 +val finite_lessThan = thm "finite_lessThan";
    1.99 +val finite_range_imageI = thm "finite_range_imageI";
   1.100 +val finite_subset = thm "finite_subset";
   1.101 +val finite_subset_induct = thm "finite_subset_induct";
   1.102 +val finite_trancl = thm "finite_trancl";
   1.103 +val foldSet_determ = thm "foldSet_determ";
   1.104 +val foldSet_imp_finite = thm "foldSet_imp_finite";
   1.105 +val fold_Un_Int = thm "fold_Un_Int";
   1.106 +val fold_Un_disjoint = thm "fold_Un_disjoint";
   1.107 +val fold_Un_disjoint2 = thm "fold_Un_disjoint2";
   1.108 +val fold_commute = thm "fold_commute";
   1.109 +val fold_def = thm "fold_def";
   1.110 +val fold_empty = thm "fold_empty";
   1.111 +val fold_equality = thm "fold_equality";
   1.112 +val fold_insert = thm "fold_insert";
   1.113 +val fold_nest_Un_Int = thm "fold_nest_Un_Int";
   1.114 +val fold_nest_Un_disjoint = thm "fold_nest_Un_disjoint";
   1.115 +val n_sub_lemma = thm "n_sub_lemma";
   1.116 +val n_subsets = thm "n_subsets";
   1.117 +val psubset_card_mono = thm "psubset_card_mono";
   1.118 +val setsum_0 = thm "setsum_0";
   1.119 +val setsum_SucD = thm "setsum_SucD";
   1.120 +val setsum_UN_disjoint = thm "setsum_UN_disjoint";
   1.121 +val setsum_Un = thm "setsum_Un";
   1.122 +val setsum_Un_Int = thm "setsum_Un_Int";
   1.123 +val setsum_Un_disjoint = thm "setsum_Un_disjoint";
   1.124 +val setsum_addf = thm "setsum_addf";
   1.125 +val setsum_cong = thm "setsum_cong";
   1.126 +val setsum_def = thm "setsum_def";
   1.127 +val setsum_diff1 = thm "setsum_diff1";
   1.128 +val setsum_empty = thm "setsum_empty";
   1.129 +val setsum_eq_0_iff = thm "setsum_eq_0_iff";
   1.130 +val setsum_insert = thm "setsum_insert";
   1.131 +val trancl_subset_Field2 = thm "trancl_subset_Field2";