| author | wenzelm |
| Tue, 07 Nov 2006 19:40:56 +0100 | |
| changeset 21234 | fb84ab52f23b |
| parent 21019 | 650c48711c7b |
| permissions | -rw-r--r-- |
| 12396 | 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"; |
|
|
21019
650c48711c7b
Legacy ML bindings now refer to old inductive definition package.
berghofe
parents:
17274
diff
changeset
|
10 |
val mk_cases = OldInductivePackage.the_mk_cases (the_context ()) "Finite_Set.Finites"; |
| 12396 | 11 |
val [emptyI, insertI] = thms "Finites.intros"; |
12 |
end; |
|
13 |
||
14 |
structure foldSet = |
|
15 |
struct |
|
16 |
val intrs = thms "foldSet.intros"; |
|
17 |
val elims = thms "foldSet.cases"; |
|
18 |
val elim = thm "foldSet.cases"; |
|
19 |
val induct = thm "foldSet.induct"; |
|
|
21019
650c48711c7b
Legacy ML bindings now refer to old inductive definition package.
berghofe
parents:
17274
diff
changeset
|
20 |
val mk_cases = OldInductivePackage.the_mk_cases (the_context ()) "Finite_Set.foldSet"; |
| 12396 | 21 |
val [emptyI, insertI] = thms "foldSet.intros"; |
22 |
end; |
|
23 |
||
24 |
val card_0_eq = thm "card_0_eq"; |
|
25 |
val card_Diff1_le = thm "card_Diff1_le"; |
|
26 |
val card_Diff1_less = thm "card_Diff1_less"; |
|
27 |
val card_Diff2_less = thm "card_Diff2_less"; |
|
28 |
val card_Diff_singleton = thm "card_Diff_singleton"; |
|
29 |
val card_Diff_singleton_if = thm "card_Diff_singleton_if"; |
|
30 |
val card_Diff_subset = thm "card_Diff_subset"; |
|
31 |
val card_Pow = thm "card_Pow"; |
|
32 |
val card_Suc_Diff1 = thm "card_Suc_Diff1"; |
|
33 |
val card_Un_Int = thm "card_Un_Int"; |
|
34 |
val card_Un_disjoint = thm "card_Un_disjoint"; |
|
35 |
val card_bij_eq = thm "card_bij_eq"; |
|
36 |
val card_def = thm "card_def"; |
|
37 |
val card_empty = thm "card_empty"; |
|
38 |
val card_eq_setsum = thm "card_eq_setsum"; |
|
39 |
val card_image = thm "card_image"; |
|
40 |
val card_image_le = thm "card_image_le"; |
|
41 |
val card_inj_on_le = thm "card_inj_on_le"; |
|
42 |
val card_insert = thm "card_insert"; |
|
43 |
val card_insert_disjoint = thm "card_insert_disjoint"; |
|
44 |
val card_insert_if = thm "card_insert_if"; |
|
45 |
val card_insert_le = thm "card_insert_le"; |
|
46 |
val card_mono = thm "card_mono"; |
|
47 |
val card_psubset = thm "card_psubset"; |
|
48 |
val card_seteq = thm "card_seteq"; |
|
| 15392 | 49 |
val Diff1_foldSet = thm "Diff1_foldSet"; |
| 12396 | 50 |
val dvd_partition = thm "dvd_partition"; |
51 |
val empty_foldSetE = thm "empty_foldSetE"; |
|
52 |
val endo_inj_surj = thm "endo_inj_surj"; |
|
53 |
val finite = thm "finite"; |
|
54 |
val finite_Diff = thm "finite_Diff"; |
|
55 |
val finite_Diff_insert = thm "finite_Diff_insert"; |
|
56 |
val finite_Field = thm "finite_Field"; |
|
| 15392 | 57 |
val finite_imp_foldSet = thm "finite_imp_foldSet"; |
| 12396 | 58 |
val finite_Int = thm "finite_Int"; |
59 |
val finite_Pow_iff = thm "finite_Pow_iff"; |
|
60 |
val finite_Prod_UNIV = thm "finite_Prod_UNIV"; |
|
61 |
val finite_SigmaI = thm "finite_SigmaI"; |
|
62 |
val finite_UN = thm "finite_UN"; |
|
63 |
val finite_UN_I = thm "finite_UN_I"; |
|
64 |
val finite_Un = thm "finite_Un"; |
|
65 |
val finite_UnI = thm "finite_UnI"; |
|
66 |
val finite_converse = thm "finite_converse"; |
|
67 |
val finite_empty_induct = thm "finite_empty_induct"; |
|
68 |
val finite_imageD = thm "finite_imageD"; |
|
69 |
val finite_imageI = thm "finite_imageI"; |
|
70 |
val finite_induct = thm "finite_induct"; |
|
71 |
val finite_insert = thm "finite_insert"; |
|
72 |
val finite_range_imageI = thm "finite_range_imageI"; |
|
73 |
val finite_subset = thm "finite_subset"; |
|
74 |
val finite_subset_induct = thm "finite_subset_induct"; |
|
75 |
val finite_trancl = thm "finite_trancl"; |
|
| 15392 | 76 |
val foldSet_determ = thm "ACf.foldSet_determ"; |
| 12396 | 77 |
val foldSet_imp_finite = thm "foldSet_imp_finite"; |
| 12693 | 78 |
val fold_Un_Int = thm "ACe.fold_Un_Int"; |
79 |
val fold_Un_disjoint = thm "ACe.fold_Un_disjoint"; |
|
| 15392 | 80 |
val fold_Un_disjoint2 = thm "ACe.fold_Un_disjoint"; |
81 |
val fold_commute = thm "ACf.fold_commute"; |
|
| 12396 | 82 |
val fold_def = thm "fold_def"; |
83 |
val fold_empty = thm "fold_empty"; |
|
| 15392 | 84 |
val fold_equality = thm "ACf.fold_equality"; |
85 |
val fold_insert = thm "ACf.fold_insert"; |
|
86 |
val fold_nest_Un_Int = thm "ACf.fold_nest_Un_Int"; |
|
87 |
val fold_nest_Un_disjoint = thm "ACf.fold_nest_Un_disjoint"; |
|
| 12396 | 88 |
val psubset_card_mono = thm "psubset_card_mono"; |
89 |
val setsum_0 = thm "setsum_0"; |
|
90 |
val setsum_SucD = thm "setsum_SucD"; |
|
91 |
val setsum_UN_disjoint = thm "setsum_UN_disjoint"; |
|
92 |
val setsum_Un = thm "setsum_Un"; |
|
93 |
val setsum_Un_Int = thm "setsum_Un_Int"; |
|
94 |
val setsum_Un_disjoint = thm "setsum_Un_disjoint"; |
|
95 |
val setsum_addf = thm "setsum_addf"; |
|
96 |
val setsum_cong = thm "setsum_cong"; |
|
97 |
val setsum_def = thm "setsum_def"; |
|
98 |
val setsum_diff1 = thm "setsum_diff1"; |
|
99 |
val setsum_empty = thm "setsum_empty"; |
|
100 |
val setsum_eq_0_iff = thm "setsum_eq_0_iff"; |
|
101 |
val setsum_insert = thm "setsum_insert"; |
|
102 |
val trancl_subset_Field2 = thm "trancl_subset_Field2"; |