src/HOL/Finite_Set.ML
author wenzelm
Tue Sep 06 16:59:48 2005 +0200 (2005-09-06)
changeset 17274 746bb4c56800
parent 16733 236dfafbeb63
child 21019 650c48711c7b
permissions -rw-r--r--
axclass: name space prefix is now "c_class" instead of just "c";
wenzelm@12396
     1
wenzelm@12396
     2
(* legacy ML bindings *)
wenzelm@12396
     3
wenzelm@12396
     4
structure Finites =
wenzelm@12396
     5
struct
wenzelm@12396
     6
  val intrs = thms "Finites.intros";
wenzelm@12396
     7
  val elims = thms "Finites.cases";
wenzelm@12396
     8
  val elim = thm "Finites.cases";
wenzelm@12396
     9
  val induct = thm "Finites.induct";
wenzelm@12396
    10
  val mk_cases = InductivePackage.the_mk_cases (the_context ()) "Finite_Set.Finites";
wenzelm@12396
    11
  val [emptyI, insertI] = thms "Finites.intros";
wenzelm@12396
    12
end;
wenzelm@12396
    13
wenzelm@12396
    14
structure foldSet =
wenzelm@12396
    15
struct
wenzelm@12396
    16
  val intrs = thms "foldSet.intros";
wenzelm@12396
    17
  val elims = thms "foldSet.cases";
wenzelm@12396
    18
  val elim = thm "foldSet.cases";
wenzelm@12396
    19
  val induct = thm "foldSet.induct";
wenzelm@12396
    20
  val mk_cases = InductivePackage.the_mk_cases (the_context ()) "Finite_Set.foldSet";
wenzelm@12396
    21
  val [emptyI, insertI] = thms "foldSet.intros";
wenzelm@12396
    22
end;
wenzelm@12396
    23
wenzelm@12396
    24
val card_0_eq = thm "card_0_eq";
wenzelm@12396
    25
val card_Diff1_le = thm "card_Diff1_le";
wenzelm@12396
    26
val card_Diff1_less = thm "card_Diff1_less";
wenzelm@12396
    27
val card_Diff2_less = thm "card_Diff2_less";
wenzelm@12396
    28
val card_Diff_singleton = thm "card_Diff_singleton";
wenzelm@12396
    29
val card_Diff_singleton_if = thm "card_Diff_singleton_if";
wenzelm@12396
    30
val card_Diff_subset = thm "card_Diff_subset";
wenzelm@12396
    31
val card_Pow = thm "card_Pow";
wenzelm@12396
    32
val card_Suc_Diff1 = thm "card_Suc_Diff1";
wenzelm@12396
    33
val card_Un_Int = thm "card_Un_Int";
wenzelm@12396
    34
val card_Un_disjoint = thm "card_Un_disjoint";
wenzelm@12396
    35
val card_bij_eq = thm "card_bij_eq";
wenzelm@12396
    36
val card_def = thm "card_def";
wenzelm@12396
    37
val card_empty = thm "card_empty";
wenzelm@12396
    38
val card_eq_setsum = thm "card_eq_setsum";
wenzelm@12396
    39
val card_image = thm "card_image";
wenzelm@12396
    40
val card_image_le = thm "card_image_le";
wenzelm@12396
    41
val card_inj_on_le = thm "card_inj_on_le";
wenzelm@12396
    42
val card_insert = thm "card_insert";
wenzelm@12396
    43
val card_insert_disjoint = thm "card_insert_disjoint";
wenzelm@12396
    44
val card_insert_if = thm "card_insert_if";
wenzelm@12396
    45
val card_insert_le = thm "card_insert_le";
wenzelm@12396
    46
val card_mono = thm "card_mono";
wenzelm@12396
    47
val card_psubset = thm "card_psubset";
wenzelm@12396
    48
val card_seteq = thm "card_seteq";
nipkow@15392
    49
val Diff1_foldSet = thm "Diff1_foldSet";
wenzelm@12396
    50
val dvd_partition = thm "dvd_partition";
wenzelm@12396
    51
val empty_foldSetE = thm "empty_foldSetE";
wenzelm@12396
    52
val endo_inj_surj = thm "endo_inj_surj";
wenzelm@12396
    53
val finite = thm "finite";
wenzelm@12396
    54
val finite_Diff = thm "finite_Diff";
wenzelm@12396
    55
val finite_Diff_insert = thm "finite_Diff_insert";
wenzelm@12396
    56
val finite_Field = thm "finite_Field";
nipkow@15392
    57
val finite_imp_foldSet = thm "finite_imp_foldSet";
wenzelm@12396
    58
val finite_Int = thm "finite_Int";
wenzelm@12396
    59
val finite_Pow_iff = thm "finite_Pow_iff";
wenzelm@12396
    60
val finite_Prod_UNIV = thm "finite_Prod_UNIV";
wenzelm@12396
    61
val finite_SigmaI = thm "finite_SigmaI";
wenzelm@12396
    62
val finite_UN = thm "finite_UN";
wenzelm@12396
    63
val finite_UN_I = thm "finite_UN_I";
wenzelm@12396
    64
val finite_Un = thm "finite_Un";
wenzelm@12396
    65
val finite_UnI = thm "finite_UnI";
wenzelm@12396
    66
val finite_converse = thm "finite_converse";
wenzelm@12396
    67
val finite_empty_induct = thm "finite_empty_induct";
wenzelm@12396
    68
val finite_imageD = thm "finite_imageD";
wenzelm@12396
    69
val finite_imageI = thm "finite_imageI";
wenzelm@12396
    70
val finite_induct = thm "finite_induct";
wenzelm@12396
    71
val finite_insert = thm "finite_insert";
wenzelm@12396
    72
val finite_range_imageI = thm "finite_range_imageI";
wenzelm@12396
    73
val finite_subset = thm "finite_subset";
wenzelm@12396
    74
val finite_subset_induct = thm "finite_subset_induct";
wenzelm@12396
    75
val finite_trancl = thm "finite_trancl";
nipkow@15392
    76
val foldSet_determ = thm "ACf.foldSet_determ";
wenzelm@12396
    77
val foldSet_imp_finite = thm "foldSet_imp_finite";
wenzelm@12693
    78
val fold_Un_Int = thm "ACe.fold_Un_Int";
wenzelm@12693
    79
val fold_Un_disjoint = thm "ACe.fold_Un_disjoint";
nipkow@15392
    80
val fold_Un_disjoint2 = thm "ACe.fold_Un_disjoint";
nipkow@15392
    81
val fold_commute = thm "ACf.fold_commute";
wenzelm@12396
    82
val fold_def = thm "fold_def";
wenzelm@12396
    83
val fold_empty = thm "fold_empty";
nipkow@15392
    84
val fold_equality = thm "ACf.fold_equality";
nipkow@15392
    85
val fold_insert = thm "ACf.fold_insert";
nipkow@15392
    86
val fold_nest_Un_Int = thm "ACf.fold_nest_Un_Int";
nipkow@15392
    87
val fold_nest_Un_disjoint = thm "ACf.fold_nest_Un_disjoint";
wenzelm@12396
    88
val psubset_card_mono = thm "psubset_card_mono";
wenzelm@12396
    89
val setsum_0 = thm "setsum_0";
wenzelm@12396
    90
val setsum_SucD = thm "setsum_SucD";
wenzelm@12396
    91
val setsum_UN_disjoint = thm "setsum_UN_disjoint";
wenzelm@12396
    92
val setsum_Un = thm "setsum_Un";
wenzelm@12396
    93
val setsum_Un_Int = thm "setsum_Un_Int";
wenzelm@12396
    94
val setsum_Un_disjoint = thm "setsum_Un_disjoint";
wenzelm@12396
    95
val setsum_addf = thm "setsum_addf";
wenzelm@12396
    96
val setsum_cong = thm "setsum_cong";
wenzelm@12396
    97
val setsum_def = thm "setsum_def";
wenzelm@12396
    98
val setsum_diff1 = thm "setsum_diff1";
wenzelm@12396
    99
val setsum_empty = thm "setsum_empty";
wenzelm@12396
   100
val setsum_eq_0_iff = thm "setsum_eq_0_iff";
wenzelm@12396
   101
val setsum_insert = thm "setsum_insert";
wenzelm@12396
   102
val trancl_subset_Field2 = thm "trancl_subset_Field2";