|
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";
|
|
|
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 cardR_SucD = thm "cardR_SucD";
|
|
|
36 |
val cardR_determ = thm "cardR_determ";
|
|
|
37 |
val cardR_emptyE = thm "cardR_emptyE";
|
|
|
38 |
val cardR_imp_finite = thm "cardR_imp_finite";
|
|
|
39 |
val cardR_insertE = thm "cardR_insertE";
|
|
|
40 |
val card_0_eq = thm "card_0_eq";
|
|
|
41 |
val card_Diff1_le = thm "card_Diff1_le";
|
|
|
42 |
val card_Diff1_less = thm "card_Diff1_less";
|
|
|
43 |
val card_Diff2_less = thm "card_Diff2_less";
|
|
|
44 |
val card_Diff_singleton = thm "card_Diff_singleton";
|
|
|
45 |
val card_Diff_singleton_if = thm "card_Diff_singleton_if";
|
|
|
46 |
val card_Diff_subset = thm "card_Diff_subset";
|
|
|
47 |
val card_Pow = thm "card_Pow";
|
|
|
48 |
val card_Suc_Diff1 = thm "card_Suc_Diff1";
|
|
|
49 |
val card_Un_Int = thm "card_Un_Int";
|
|
|
50 |
val card_Un_disjoint = thm "card_Un_disjoint";
|
|
|
51 |
val card_bij_eq = thm "card_bij_eq";
|
|
|
52 |
val card_def = thm "card_def";
|
|
|
53 |
val card_empty = thm "card_empty";
|
|
|
54 |
val card_eq_setsum = thm "card_eq_setsum";
|
|
|
55 |
val card_equality = thm "card_equality";
|
|
|
56 |
val card_image = thm "card_image";
|
|
|
57 |
val card_image_le = thm "card_image_le";
|
|
|
58 |
val card_inj_on_le = thm "card_inj_on_le";
|
|
|
59 |
val card_insert = thm "card_insert";
|
|
|
60 |
val card_insert_disjoint = thm "card_insert_disjoint";
|
|
|
61 |
val card_insert_if = thm "card_insert_if";
|
|
|
62 |
val card_insert_le = thm "card_insert_le";
|
|
|
63 |
val card_mono = thm "card_mono";
|
|
|
64 |
val card_psubset = thm "card_psubset";
|
|
|
65 |
val card_s_0_eq_empty = thm "card_s_0_eq_empty";
|
|
|
66 |
val card_seteq = thm "card_seteq";
|
|
|
67 |
val choose_deconstruct = thm "choose_deconstruct";
|
|
|
68 |
val constr_bij = thm "constr_bij";
|
|
|
69 |
val dvd_partition = thm "dvd_partition";
|
|
|
70 |
val empty_foldSetE = thm "empty_foldSetE";
|
|
|
71 |
val endo_inj_surj = thm "endo_inj_surj";
|
|
|
72 |
val finite = thm "finite";
|
|
|
73 |
val finiteI = thm "finiteI";
|
|
|
74 |
val finite_Diff = thm "finite_Diff";
|
|
|
75 |
val finite_Diff_insert = thm "finite_Diff_insert";
|
|
|
76 |
val finite_Field = thm "finite_Field";
|
|
|
77 |
val finite_Int = thm "finite_Int";
|
|
|
78 |
val finite_Pow_iff = thm "finite_Pow_iff";
|
|
|
79 |
val finite_Prod_UNIV = thm "finite_Prod_UNIV";
|
|
|
80 |
val finite_SigmaI = thm "finite_SigmaI";
|
|
|
81 |
val finite_UN = thm "finite_UN";
|
|
|
82 |
val finite_UN_I = thm "finite_UN_I";
|
|
|
83 |
val finite_Un = thm "finite_Un";
|
|
|
84 |
val finite_UnI = thm "finite_UnI";
|
|
|
85 |
val finite_converse = thm "finite_converse";
|
|
|
86 |
val finite_empty_induct = thm "finite_empty_induct";
|
|
|
87 |
val finite_imageD = thm "finite_imageD";
|
|
|
88 |
val finite_imageI = thm "finite_imageI";
|
|
|
89 |
val finite_imp_cardR = thm "finite_imp_cardR";
|
|
|
90 |
val finite_imp_foldSet = thm "finite_imp_foldSet";
|
|
|
91 |
val finite_induct = thm "finite_induct";
|
|
|
92 |
val finite_insert = thm "finite_insert";
|
|
|
93 |
val finite_range_imageI = thm "finite_range_imageI";
|
|
|
94 |
val finite_subset = thm "finite_subset";
|
|
|
95 |
val finite_subset_induct = thm "finite_subset_induct";
|
|
|
96 |
val finite_trancl = thm "finite_trancl";
|
|
12693
|
97 |
val foldSet_determ = thm "LC.foldSet_determ";
|
|
12396
|
98 |
val foldSet_imp_finite = thm "foldSet_imp_finite";
|
|
12693
|
99 |
val fold_Un_Int = thm "ACe.fold_Un_Int";
|
|
|
100 |
val fold_Un_disjoint = thm "ACe.fold_Un_disjoint";
|
|
|
101 |
val fold_Un_disjoint2 = thm "ACe.fold_Un_disjoint2";
|
|
|
102 |
val fold_commute = thm "LC.fold_commute";
|
|
12396
|
103 |
val fold_def = thm "fold_def";
|
|
|
104 |
val fold_empty = thm "fold_empty";
|
|
12693
|
105 |
val fold_equality = thm "LC.fold_equality";
|
|
|
106 |
val fold_insert = thm "LC.fold_insert";
|
|
|
107 |
val fold_nest_Un_Int = thm "LC.fold_nest_Un_Int";
|
|
|
108 |
val fold_nest_Un_disjoint = thm "LC.fold_nest_Un_disjoint";
|
|
12396
|
109 |
val n_sub_lemma = thm "n_sub_lemma";
|
|
|
110 |
val n_subsets = thm "n_subsets";
|
|
|
111 |
val psubset_card_mono = thm "psubset_card_mono";
|
|
|
112 |
val setsum_0 = thm "setsum_0";
|
|
|
113 |
val setsum_SucD = thm "setsum_SucD";
|
|
|
114 |
val setsum_UN_disjoint = thm "setsum_UN_disjoint";
|
|
|
115 |
val setsum_Un = thm "setsum_Un";
|
|
|
116 |
val setsum_Un_Int = thm "setsum_Un_Int";
|
|
|
117 |
val setsum_Un_disjoint = thm "setsum_Un_disjoint";
|
|
|
118 |
val setsum_addf = thm "setsum_addf";
|
|
|
119 |
val setsum_cong = thm "setsum_cong";
|
|
|
120 |
val setsum_def = thm "setsum_def";
|
|
|
121 |
val setsum_diff1 = thm "setsum_diff1";
|
|
|
122 |
val setsum_empty = thm "setsum_empty";
|
|
|
123 |
val setsum_eq_0_iff = thm "setsum_eq_0_iff";
|
|
|
124 |
val setsum_insert = thm "setsum_insert";
|
|
|
125 |
val trancl_subset_Field2 = thm "trancl_subset_Field2";
|