9 val induct = thm "Finites.induct"; |
9 val induct = thm "Finites.induct"; |
10 val mk_cases = InductivePackage.the_mk_cases (the_context ()) "Finite_Set.Finites"; |
10 val mk_cases = InductivePackage.the_mk_cases (the_context ()) "Finite_Set.Finites"; |
11 val [emptyI, insertI] = thms "Finites.intros"; |
11 val [emptyI, insertI] = thms "Finites.intros"; |
12 end; |
12 end; |
13 |
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 = |
14 structure foldSet = |
25 struct |
15 struct |
26 val intrs = thms "foldSet.intros"; |
16 val intrs = thms "foldSet.intros"; |
27 val elims = thms "foldSet.cases"; |
17 val elims = thms "foldSet.cases"; |
28 val elim = thm "foldSet.cases"; |
18 val elim = thm "foldSet.cases"; |
29 val induct = thm "foldSet.induct"; |
19 val induct = thm "foldSet.induct"; |
30 val mk_cases = InductivePackage.the_mk_cases (the_context ()) "Finite_Set.foldSet"; |
20 val mk_cases = InductivePackage.the_mk_cases (the_context ()) "Finite_Set.foldSet"; |
31 val [emptyI, insertI] = thms "foldSet.intros"; |
21 val [emptyI, insertI] = thms "foldSet.intros"; |
32 end; |
22 end; |
33 |
23 |
34 val cardR_SucD = thm "cardR_SucD"; |
|
35 val cardR_determ = thm "cardR_determ"; |
|
36 val cardR_emptyE = thm "cardR_emptyE"; |
|
37 val cardR_imp_finite = thm "cardR_imp_finite"; |
|
38 val cardR_insertE = thm "cardR_insertE"; |
|
39 val card_0_eq = thm "card_0_eq"; |
24 val card_0_eq = thm "card_0_eq"; |
40 val card_Diff1_le = thm "card_Diff1_le"; |
25 val card_Diff1_le = thm "card_Diff1_le"; |
41 val card_Diff1_less = thm "card_Diff1_less"; |
26 val card_Diff1_less = thm "card_Diff1_less"; |
42 val card_Diff2_less = thm "card_Diff2_less"; |
27 val card_Diff2_less = thm "card_Diff2_less"; |
43 val card_Diff_singleton = thm "card_Diff_singleton"; |
28 val card_Diff_singleton = thm "card_Diff_singleton"; |
48 val card_Un_Int = thm "card_Un_Int"; |
33 val card_Un_Int = thm "card_Un_Int"; |
49 val card_Un_disjoint = thm "card_Un_disjoint"; |
34 val card_Un_disjoint = thm "card_Un_disjoint"; |
50 val card_bij_eq = thm "card_bij_eq"; |
35 val card_bij_eq = thm "card_bij_eq"; |
51 val card_def = thm "card_def"; |
36 val card_def = thm "card_def"; |
52 val card_empty = thm "card_empty"; |
37 val card_empty = thm "card_empty"; |
53 val card_equality = thm "card_equality"; |
|
54 val card_eq_setsum = thm "card_eq_setsum"; |
38 val card_eq_setsum = thm "card_eq_setsum"; |
55 val card_image = thm "card_image"; |
39 val card_image = thm "card_image"; |
56 val card_image_le = thm "card_image_le"; |
40 val card_image_le = thm "card_image_le"; |
57 val card_inj_on_le = thm "card_inj_on_le"; |
41 val card_inj_on_le = thm "card_inj_on_le"; |
58 val card_insert = thm "card_insert"; |
42 val card_insert = thm "card_insert"; |
85 val finite_UnI = thm "finite_UnI"; |
69 val finite_UnI = thm "finite_UnI"; |
86 val finite_converse = thm "finite_converse"; |
70 val finite_converse = thm "finite_converse"; |
87 val finite_empty_induct = thm "finite_empty_induct"; |
71 val finite_empty_induct = thm "finite_empty_induct"; |
88 val finite_imageD = thm "finite_imageD"; |
72 val finite_imageD = thm "finite_imageD"; |
89 val finite_imageI = thm "finite_imageI"; |
73 val finite_imageI = thm "finite_imageI"; |
90 val finite_imp_cardR = thm "finite_imp_cardR"; |
|
91 val finite_induct = thm "finite_induct"; |
74 val finite_induct = thm "finite_induct"; |
92 val finite_insert = thm "finite_insert"; |
75 val finite_insert = thm "finite_insert"; |
93 val finite_range_imageI = thm "finite_range_imageI"; |
76 val finite_range_imageI = thm "finite_range_imageI"; |
94 val finite_subset = thm "finite_subset"; |
77 val finite_subset = thm "finite_subset"; |
95 val finite_subset_induct = thm "finite_subset_induct"; |
78 val finite_subset_induct = thm "finite_subset_induct"; |