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 bounded_nat_set_is_finite = thm "bounded_nat_set_is_finite";


36 
val cardR_SucD = thm "cardR_SucD";


37 
val cardR_determ = thm "cardR_determ";


38 
val cardR_emptyE = thm "cardR_emptyE";


39 
val cardR_imp_finite = thm "cardR_imp_finite";


40 
val cardR_insertE = thm "cardR_insertE";


41 
val card_0_eq = thm "card_0_eq";


42 
val card_Diff1_le = thm "card_Diff1_le";


43 
val card_Diff1_less = thm "card_Diff1_less";


44 
val card_Diff2_less = thm "card_Diff2_less";


45 
val card_Diff_singleton = thm "card_Diff_singleton";


46 
val card_Diff_singleton_if = thm "card_Diff_singleton_if";


47 
val card_Diff_subset = thm "card_Diff_subset";


48 
val card_Pow = thm "card_Pow";


49 
val card_Suc_Diff1 = thm "card_Suc_Diff1";


50 
val card_Un_Int = thm "card_Un_Int";


51 
val card_Un_disjoint = thm "card_Un_disjoint";


52 
val card_bij_eq = thm "card_bij_eq";


53 
val card_def = thm "card_def";


54 
val card_empty = thm "card_empty";


55 
val card_eq_setsum = thm "card_eq_setsum";


56 
val card_equality = thm "card_equality";


57 
val card_image = thm "card_image";


58 
val card_image_le = thm "card_image_le";


59 
val card_inj_on_le = thm "card_inj_on_le";


60 
val card_insert = thm "card_insert";


61 
val card_insert_disjoint = thm "card_insert_disjoint";


62 
val card_insert_if = thm "card_insert_if";


63 
val card_insert_le = thm "card_insert_le";


64 
val card_mono = thm "card_mono";


65 
val card_psubset = thm "card_psubset";


66 
val card_s_0_eq_empty = thm "card_s_0_eq_empty";


67 
val card_seteq = thm "card_seteq";


68 
val choose_deconstruct = thm "choose_deconstruct";


69 
val constr_bij = thm "constr_bij";


70 
val dvd_partition = thm "dvd_partition";


71 
val empty_foldSetE = thm "empty_foldSetE";


72 
val endo_inj_surj = thm "endo_inj_surj";


73 
val finite = thm "finite";


74 
val finiteI = thm "finiteI";


75 
val finite_Diff = thm "finite_Diff";


76 
val finite_Diff_insert = thm "finite_Diff_insert";


77 
val finite_Field = thm "finite_Field";


78 
val finite_Int = thm "finite_Int";


79 
val finite_Pow_iff = thm "finite_Pow_iff";


80 
val finite_Prod_UNIV = thm "finite_Prod_UNIV";


81 
val finite_SigmaI = thm "finite_SigmaI";


82 
val finite_UN = thm "finite_UN";


83 
val finite_UN_I = thm "finite_UN_I";


84 
val finite_Un = thm "finite_Un";


85 
val finite_UnI = thm "finite_UnI";


86 
val finite_atMost = thm "finite_atMost";


87 
val finite_converse = thm "finite_converse";


88 
val finite_empty_induct = thm "finite_empty_induct";


89 
val finite_imageD = thm "finite_imageD";


90 
val finite_imageI = thm "finite_imageI";


91 
val finite_imp_cardR = thm "finite_imp_cardR";


92 
val finite_imp_foldSet = thm "finite_imp_foldSet";


93 
val finite_induct = thm "finite_induct";


94 
val finite_insert = thm "finite_insert";


95 
val finite_lessThan = thm "finite_lessThan";


96 
val finite_range_imageI = thm "finite_range_imageI";


97 
val finite_subset = thm "finite_subset";


98 
val finite_subset_induct = thm "finite_subset_induct";


99 
val finite_trancl = thm "finite_trancl";


100 
val foldSet_determ = thm "foldSet_determ";


101 
val foldSet_imp_finite = thm "foldSet_imp_finite";


102 
val fold_Un_Int = thm "fold_Un_Int";


103 
val fold_Un_disjoint = thm "fold_Un_disjoint";


104 
val fold_Un_disjoint2 = thm "fold_Un_disjoint2";


105 
val fold_commute = thm "fold_commute";


106 
val fold_def = thm "fold_def";


107 
val fold_empty = thm "fold_empty";


108 
val fold_equality = thm "fold_equality";


109 
val fold_insert = thm "fold_insert";


110 
val fold_nest_Un_Int = thm "fold_nest_Un_Int";


111 
val fold_nest_Un_disjoint = thm "fold_nest_Un_disjoint";


112 
val n_sub_lemma = thm "n_sub_lemma";


113 
val n_subsets = thm "n_subsets";


114 
val psubset_card_mono = thm "psubset_card_mono";


115 
val setsum_0 = thm "setsum_0";


116 
val setsum_SucD = thm "setsum_SucD";


117 
val setsum_UN_disjoint = thm "setsum_UN_disjoint";


118 
val setsum_Un = thm "setsum_Un";


119 
val setsum_Un_Int = thm "setsum_Un_Int";


120 
val setsum_Un_disjoint = thm "setsum_Un_disjoint";


121 
val setsum_addf = thm "setsum_addf";


122 
val setsum_cong = thm "setsum_cong";


123 
val setsum_def = thm "setsum_def";


124 
val setsum_diff1 = thm "setsum_diff1";


125 
val setsum_empty = thm "setsum_empty";


126 
val setsum_eq_0_iff = thm "setsum_eq_0_iff";


127 
val setsum_insert = thm "setsum_insert";


128 
val trancl_subset_Field2 = thm "trancl_subset_Field2";
