isabelle: src/HOL/Finite_Set.ML@0c4fd7529467 (annotated)

12396 2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	1
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	2	(* legacy ML bindings *)
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	3
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	4	structure Finites =
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	5	struct
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	6	val intrs = thms "Finites.intros";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	7	val elims = thms "Finites.cases";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	8	val elim = thm "Finites.cases";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	9	val induct = thm "Finites.induct";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	10	val mk_cases = InductivePackage.the_mk_cases (the_context ()) "Finite_Set.Finites";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	11	val [emptyI, insertI] = thms "Finites.intros";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	12	end;
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	13
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	14	structure cardR =
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	15	struct
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	16	val intrs = thms "cardR.intros";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	17	val elims = thms "cardR.cases";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	18	val elim = thm "cardR.cases";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	19	val induct = thm "cardR.induct";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	20	val mk_cases = InductivePackage.the_mk_cases (the_context ()) "Finite_Set.cardR";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	21	val [EmptyI, InsertI] = thms "cardR.intros";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	22	end;
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	23
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	24	structure foldSet =
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	25	struct
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	26	val intrs = thms "foldSet.intros";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	27	val elims = thms "foldSet.cases";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	28	val elim = thm "foldSet.cases";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	29	val induct = thm "foldSet.induct";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	30	val mk_cases = InductivePackage.the_mk_cases (the_context ()) "Finite_Set.foldSet";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	31	val [emptyI, insertI] = thms "foldSet.intros";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	32	end;
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	33
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	34	val Diff1_foldSet = thm "Diff1_foldSet";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	35	val bounded_nat_set_is_finite = thm "bounded_nat_set_is_finite";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	36	val cardR_SucD = thm "cardR_SucD";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	37	val cardR_determ = thm "cardR_determ";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	38	val cardR_emptyE = thm "cardR_emptyE";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	39	val cardR_imp_finite = thm "cardR_imp_finite";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	40	val cardR_insertE = thm "cardR_insertE";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	41	val card_0_eq = thm "card_0_eq";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	42	val card_Diff1_le = thm "card_Diff1_le";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	43	val card_Diff1_less = thm "card_Diff1_less";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	44	val card_Diff2_less = thm "card_Diff2_less";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	45	val card_Diff_singleton = thm "card_Diff_singleton";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	46	val card_Diff_singleton_if = thm "card_Diff_singleton_if";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	47	val card_Diff_subset = thm "card_Diff_subset";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	48	val card_Pow = thm "card_Pow";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	49	val card_Suc_Diff1 = thm "card_Suc_Diff1";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	50	val card_Un_Int = thm "card_Un_Int";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	51	val card_Un_disjoint = thm "card_Un_disjoint";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	52	val card_bij_eq = thm "card_bij_eq";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	53	val card_def = thm "card_def";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	54	val card_empty = thm "card_empty";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	55	val card_eq_setsum = thm "card_eq_setsum";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	56	val card_equality = thm "card_equality";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	57	val card_image = thm "card_image";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	58	val card_image_le = thm "card_image_le";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	59	val card_inj_on_le = thm "card_inj_on_le";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	60	val card_insert = thm "card_insert";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	61	val card_insert_disjoint = thm "card_insert_disjoint";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	62	val card_insert_if = thm "card_insert_if";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	63	val card_insert_le = thm "card_insert_le";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	64	val card_mono = thm "card_mono";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	65	val card_psubset = thm "card_psubset";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	66	val card_s_0_eq_empty = thm "card_s_0_eq_empty";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	67	val card_seteq = thm "card_seteq";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	68	val choose_deconstruct = thm "choose_deconstruct";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	69	val constr_bij = thm "constr_bij";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	70	val dvd_partition = thm "dvd_partition";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	71	val empty_foldSetE = thm "empty_foldSetE";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	72	val endo_inj_surj = thm "endo_inj_surj";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	73	val finite = thm "finite";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	74	val finiteI = thm "finiteI";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	75	val finite_Diff = thm "finite_Diff";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	76	val finite_Diff_insert = thm "finite_Diff_insert";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	77	val finite_Field = thm "finite_Field";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	78	val finite_Int = thm "finite_Int";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	79	val finite_Pow_iff = thm "finite_Pow_iff";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	80	val finite_Prod_UNIV = thm "finite_Prod_UNIV";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	81	val finite_SigmaI = thm "finite_SigmaI";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	82	val finite_UN = thm "finite_UN";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	83	val finite_UN_I = thm "finite_UN_I";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	84	val finite_Un = thm "finite_Un";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	85	val finite_UnI = thm "finite_UnI";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	86	val finite_atMost = thm "finite_atMost";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	87	val finite_converse = thm "finite_converse";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	88	val finite_empty_induct = thm "finite_empty_induct";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	89	val finite_imageD = thm "finite_imageD";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	90	val finite_imageI = thm "finite_imageI";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	91	val finite_imp_cardR = thm "finite_imp_cardR";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	92	val finite_imp_foldSet = thm "finite_imp_foldSet";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	93	val finite_induct = thm "finite_induct";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	94	val finite_insert = thm "finite_insert";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	95	val finite_lessThan = thm "finite_lessThan";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	96	val finite_range_imageI = thm "finite_range_imageI";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	97	val finite_subset = thm "finite_subset";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	98	val finite_subset_induct = thm "finite_subset_induct";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	99	val finite_trancl = thm "finite_trancl";
12693 827818b891c7 qualified exports from locales; wenzelm parents: 12396 diff changeset	100	val foldSet_determ = thm "LC.foldSet_determ";
12396 2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	101	val foldSet_imp_finite = thm "foldSet_imp_finite";
12693 827818b891c7 qualified exports from locales; wenzelm parents: 12396 diff changeset	102	val fold_Un_Int = thm "ACe.fold_Un_Int";
827818b891c7 qualified exports from locales; wenzelm parents: 12396 diff changeset	103	val fold_Un_disjoint = thm "ACe.fold_Un_disjoint";
827818b891c7 qualified exports from locales; wenzelm parents: 12396 diff changeset	104	val fold_Un_disjoint2 = thm "ACe.fold_Un_disjoint2";
827818b891c7 qualified exports from locales; wenzelm parents: 12396 diff changeset	105	val fold_commute = thm "LC.fold_commute";
12396 2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	106	val fold_def = thm "fold_def";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	107	val fold_empty = thm "fold_empty";
12693 827818b891c7 qualified exports from locales; wenzelm parents: 12396 diff changeset	108	val fold_equality = thm "LC.fold_equality";
827818b891c7 qualified exports from locales; wenzelm parents: 12396 diff changeset	109	val fold_insert = thm "LC.fold_insert";
827818b891c7 qualified exports from locales; wenzelm parents: 12396 diff changeset	110	val fold_nest_Un_Int = thm "LC.fold_nest_Un_Int";
827818b891c7 qualified exports from locales; wenzelm parents: 12396 diff changeset	111	val fold_nest_Un_disjoint = thm "LC.fold_nest_Un_disjoint";
12396 2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	112	val n_sub_lemma = thm "n_sub_lemma";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	113	val n_subsets = thm "n_subsets";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	114	val psubset_card_mono = thm "psubset_card_mono";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	115	val setsum_0 = thm "setsum_0";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	116	val setsum_SucD = thm "setsum_SucD";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	117	val setsum_UN_disjoint = thm "setsum_UN_disjoint";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	118	val setsum_Un = thm "setsum_Un";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	119	val setsum_Un_Int = thm "setsum_Un_Int";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	120	val setsum_Un_disjoint = thm "setsum_Un_disjoint";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	121	val setsum_addf = thm "setsum_addf";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	122	val setsum_cong = thm "setsum_cong";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	123	val setsum_def = thm "setsum_def";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	124	val setsum_diff1 = thm "setsum_diff1";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	125	val setsum_empty = thm "setsum_empty";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	126	val setsum_eq_0_iff = thm "setsum_eq_0_iff";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	127	val setsum_insert = thm "setsum_insert";
2298d5b8e530 renamed theory Finite to Finite_Set and converted; wenzelm parents: diff changeset	128	val trancl_subset_Field2 = thm "trancl_subset_Field2";

author	wenzelm
	Mon, 25 Feb 2002 20:48:14 +0100
changeset 12937	0c4fd7529467
parent 12693	827818b891c7
child 14485	ea2707645af8
permissions	-rw-r--r--