src/HOL/Set.ML

--- a/src/HOL/Set.ML	Fri Feb 15 20:43:44 2002 +0100
+++ b/src/HOL/Set.ML	Sat Feb 16 20:59:34 2002 +0100
@@ -1,6 +1,415 @@
 
 (* legacy ML bindings *)
 
+val Ball_def = thm "Ball_def";
+val Bex_def = thm "Bex_def";
+val CollectD = thm "CollectD";
+val CollectE = thm "CollectE";
+val CollectI = thm "CollectI";
+val Collect_all_eq = thm "Collect_all_eq";
+val Collect_ball_eq = thm "Collect_ball_eq";
+val Collect_bex_eq = thm "Collect_bex_eq";
+val Collect_cong = thm "Collect_cong";
+val Collect_conj_eq = thm "Collect_conj_eq";
+val Collect_const = thm "Collect_const";
+val Collect_disj_eq = thm "Collect_disj_eq";
+val Collect_empty_eq = thm "Collect_empty_eq";
+val Collect_ex_eq = thm "Collect_ex_eq";
+val Collect_mem_eq = thm "Collect_mem_eq";
+val Collect_mono = thm "Collect_mono";
+val Collect_neg_eq = thm "Collect_neg_eq";
+val ComplD = thm "ComplD";
+val ComplE = thm "ComplE";
+val ComplI = thm "ComplI";
+val Compl_Diff_eq = thm "Compl_Diff_eq";
+val Compl_INT = thm "Compl_INT";
+val Compl_Int = thm "Compl_Int";
+val Compl_UN = thm "Compl_UN";
+val Compl_UNIV_eq = thm "Compl_UNIV_eq";
+val Compl_Un = thm "Compl_Un";
+val Compl_anti_mono = thm "Compl_anti_mono";
+val Compl_def = thm "Compl_def";
+val Compl_disjoint = thm "Compl_disjoint";
+val Compl_disjoint2 = thm "Compl_disjoint2";
+val Compl_empty_eq = thm "Compl_empty_eq";
+val Compl_eq_Compl_iff = thm "Compl_eq_Compl_iff";
+val Compl_iff = thm "Compl_iff";
+val Compl_partition = thm "Compl_partition";
+val Compl_subset_Compl_iff = thm "Compl_subset_Compl_iff";
+val DiffD1 = thm "DiffD1";
+val DiffD2 = thm "DiffD2";
+val DiffE = thm "DiffE";
+val DiffI = thm "DiffI";
+val Diff_Compl = thm "Diff_Compl";
+val Diff_Int = thm "Diff_Int";
+val Diff_Int_distrib = thm "Diff_Int_distrib";
+val Diff_Int_distrib2 = thm "Diff_Int_distrib2";
+val Diff_UNIV = thm "Diff_UNIV";
+val Diff_Un = thm "Diff_Un";
+val Diff_cancel = thm "Diff_cancel";
+val Diff_disjoint = thm "Diff_disjoint";
+val Diff_empty = thm "Diff_empty";
+val Diff_eq = thm "Diff_eq";
+val Diff_eq_empty_iff = thm "Diff_eq_empty_iff";
+val Diff_iff = thm "Diff_iff";
+val Diff_insert = thm "Diff_insert";
+val Diff_insert0 = thm "Diff_insert0";
+val Diff_insert2 = thm "Diff_insert2";
+val Diff_insert_absorb = thm "Diff_insert_absorb";
+val Diff_mono = thm "Diff_mono";
+val Diff_partition = thm "Diff_partition";
+val Diff_subset = thm "Diff_subset";
+val Diff_triv = thm "Diff_triv";
+val INTER_def = thm "INTER_def";
+val INT_D = thm "INT_D";
+val INT_E = thm "INT_E";
+val INT_I = thm "INT_I";
+val INT_Int_distrib = thm "INT_Int_distrib";
+val INT_Un = thm "INT_Un";
+val INT_absorb = thm "INT_absorb";
+val INT_anti_mono = thm "INT_anti_mono";
+val INT_bool_eq = thm "INT_bool_eq";
+val INT_cong = thm "INT_cong";
+val INT_constant = thm "INT_constant";
+val INT_empty = thm "INT_empty";
+val INT_eq = thm "INT_eq";
+val INT_greatest = thm "INT_greatest";
+val INT_iff = thm "INT_iff";
+val INT_insert = thm "INT_insert";
+val INT_insert_distrib = thm "INT_insert_distrib";
+val INT_lower = thm "INT_lower";
+val INT_simps = thms "INT_simps";
+val INT_subset_iff = thm "INT_subset_iff";
+val IntD1 = thm "IntD1";
+val IntD2 = thm "IntD2";
+val IntE = thm "IntE";
+val IntI = thm "IntI";
+val Int_Collect = thm "Int_Collect";
+val Int_Collect_mono = thm "Int_Collect_mono";
+val Int_Diff = thm "Int_Diff";
+val Int_Inter_image = thm "Int_Inter_image";
+val Int_UNIV = thm "Int_UNIV";
+val Int_UNIV_left = thm "Int_UNIV_left";
+val Int_UNIV_right = thm "Int_UNIV_right";
+val Int_UN_distrib = thm "Int_UN_distrib";
+val Int_UN_distrib2 = thm "Int_UN_distrib2";
+val Int_Un_distrib = thm "Int_Un_distrib";
+val Int_Un_distrib2 = thm "Int_Un_distrib2";
+val Int_Union = thm "Int_Union";
+val Int_Union2 = thm "Int_Union2";
+val Int_absorb = thm "Int_absorb";
+val Int_absorb1 = thm "Int_absorb1";
+val Int_absorb2 = thm "Int_absorb2";
+val Int_ac = thms "Int_ac";
+val Int_assoc = thm "Int_assoc";
+val Int_commute = thm "Int_commute";
+val Int_def = thm "Int_def";
+val Int_empty_left = thm "Int_empty_left";
+val Int_empty_right = thm "Int_empty_right";
+val Int_eq_Inter = thm "Int_eq_Inter";
+val Int_greatest = thm "Int_greatest";
+val Int_iff = thm "Int_iff";
+val Int_insert_left = thm "Int_insert_left";
+val Int_insert_right = thm "Int_insert_right";
+val Int_left_absorb = thm "Int_left_absorb";
+val Int_left_commute = thm "Int_left_commute";
+val Int_lower1 = thm "Int_lower1";
+val Int_lower2 = thm "Int_lower2";
+val Int_mono = thm "Int_mono";
+val Int_subset_iff = thm "Int_subset_iff";
+val InterD = thm "InterD";
+val InterE = thm "InterE";
+val InterI = thm "InterI";
+val Inter_UNIV = thm "Inter_UNIV";
+val Inter_Un_distrib = thm "Inter_Un_distrib";
+val Inter_Un_subset = thm "Inter_Un_subset";
+val Inter_anti_mono = thm "Inter_anti_mono";
+val Inter_def = thm "Inter_def";
+val Inter_empty = thm "Inter_empty";
+val Inter_greatest = thm "Inter_greatest";
+val Inter_iff = thm "Inter_iff";
+val Inter_image_eq = thm "Inter_image_eq";
+val Inter_insert = thm "Inter_insert";
+val Inter_lower = thm "Inter_lower";
+val PowD = thm "PowD";
+val PowI = thm "PowI";
+val Pow_Compl = thm "Pow_Compl";
+val Pow_INT_eq = thm "Pow_INT_eq";
+val Pow_Int_eq = thm "Pow_Int_eq";
+val Pow_UNIV = thm "Pow_UNIV";
+val Pow_bottom = thm "Pow_bottom";
+val Pow_def = thm "Pow_def";
+val Pow_empty = thm "Pow_empty";
+val Pow_iff = thm "Pow_iff";
+val Pow_insert = thm "Pow_insert";
+val Pow_mono = thm "Pow_mono";
+val Pow_top = thm "Pow_top";
+val UNION_def = thm "UNION_def";
+val UNIV_I = thm "UNIV_I";
+val UNIV_def = thm "UNIV_def";
+val UNIV_not_empty = thm "UNIV_not_empty";
+val UNIV_witness = thm "UNIV_witness";
+val UN_E = thm "UN_E";
+val UN_I = thm "UN_I";
+val UN_Pow_subset = thm "UN_Pow_subset";
+val UN_UN_flatten = thm "UN_UN_flatten";
+val UN_Un = thm "UN_Un";
+val UN_Un_distrib = thm "UN_Un_distrib";
+val UN_absorb = thm "UN_absorb";
+val UN_bool_eq = thm "UN_bool_eq";
+val UN_cong = thm "UN_cong";
+val UN_constant = thm "UN_constant";
+val UN_empty = thm "UN_empty";
+val UN_empty2 = thm "UN_empty2";
+val UN_empty3 = thm "UN_empty3";
+val UN_eq = thm "UN_eq";
+val UN_iff = thm "UN_iff";
+val UN_insert = thm "UN_insert";
+val UN_insert_distrib = thm "UN_insert_distrib";
+val UN_least = thm "UN_least";
+val UN_mono = thm "UN_mono";
+val UN_simps = thms "UN_simps";
+val UN_singleton = thm "UN_singleton";
+val UN_subset_iff = thm "UN_subset_iff";
+val UN_upper = thm "UN_upper";
+val UnCI = thm "UnCI";
+val UnE = thm "UnE";
+val UnI1 = thm "UnI1";
+val UnI2 = thm "UnI2";
+val Un_Diff = thm "Un_Diff";
+val Un_Diff_Int = thm "Un_Diff_Int";
+val Un_Diff_cancel = thm "Un_Diff_cancel";
+val Un_Diff_cancel2 = thm "Un_Diff_cancel2";
+val Un_INT_distrib = thm "Un_INT_distrib";
+val Un_INT_distrib2 = thm "Un_INT_distrib2";
+val Un_Int_assoc_eq = thm "Un_Int_assoc_eq";
+val Un_Int_crazy = thm "Un_Int_crazy";
+val Un_Int_distrib = thm "Un_Int_distrib";
+val Un_Int_distrib2 = thm "Un_Int_distrib2";
+val Un_Inter = thm "Un_Inter";
+val Un_Pow_subset = thm "Un_Pow_subset";
+val Un_UNIV_left = thm "Un_UNIV_left";
+val Un_UNIV_right = thm "Un_UNIV_right";
+val Un_Union_image = thm "Un_Union_image";
+val Un_absorb = thm "Un_absorb";
+val Un_absorb1 = thm "Un_absorb1";
+val Un_absorb2 = thm "Un_absorb2";
+val Un_ac = thms "Un_ac";
+val Un_assoc = thm "Un_assoc";
+val Un_commute = thm "Un_commute";
+val Un_def = thm "Un_def";
+val Un_empty = thm "Un_empty";
+val Un_empty_left = thm "Un_empty_left";
+val Un_empty_right = thm "Un_empty_right";
+val Un_eq_UN = thm "Un_eq_UN";
+val Un_eq_Union = thm "Un_eq_Union";
+val Un_iff = thm "Un_iff";
+val Un_insert_left = thm "Un_insert_left";
+val Un_insert_right = thm "Un_insert_right";
+val Un_least = thm "Un_least";
+val Un_left_absorb = thm "Un_left_absorb";
+val Un_left_commute = thm "Un_left_commute";
+val Un_mono = thm "Un_mono";
+val Un_subset_iff = thm "Un_subset_iff";
+val Un_upper1 = thm "Un_upper1";
+val Un_upper2 = thm "Un_upper2";
+val UnionE = thm "UnionE";
+val UnionI = thm "UnionI";
+val Union_Int_subset = thm "Union_Int_subset";
+val Union_Pow_eq = thm "Union_Pow_eq";
+val Union_UNIV = thm "Union_UNIV";
+val Union_Un_distrib = thm "Union_Un_distrib";
+val Union_def = thm "Union_def";
+val Union_disjoint = thm "Union_disjoint";
+val Union_empty = thm "Union_empty";
+val Union_empty_conv = thm "Union_empty_conv";
+val Union_iff = thm "Union_iff";
+val Union_image_eq = thm "Union_image_eq";
+val Union_insert = thm "Union_insert";
+val Union_least = thm "Union_least";
+val Union_mono = thm "Union_mono";
+val Union_upper = thm "Union_upper";
+val all_bool_eq = thm "all_bool_eq";
+val all_mono = thm "all_mono";
+val all_not_in_conv = thm "all_not_in_conv";
+val atomize_ball = thm "atomize_ball";
+val ballE = thm "ballE";
+val ballI = thm "ballI";
+val ball_UN = thm "ball_UN";
+val ball_UNIV = thm "ball_UNIV";
+val ball_Un = thm "ball_Un";
+val ball_cong = thm "ball_cong";
+val ball_conj_distrib = thm "ball_conj_distrib";
+val ball_empty = thm "ball_empty";
+val ball_one_point1 = thm "ball_one_point1";
+val ball_one_point2 = thm "ball_one_point2";
+val ball_simps = thms "ball_simps";
+val ball_triv = thm "ball_triv";
+val basic_monos = thms "basic_monos";
+val bexCI = thm "bexCI";
+val bexE = thm "bexE";
+val bexI = thm "bexI";
+val bex_UN = thm "bex_UN";
+val bex_UNIV = thm "bex_UNIV";
+val bex_Un = thm "bex_Un";
+val bex_cong = thm "bex_cong";
+val bex_disj_distrib = thm "bex_disj_distrib";
+val bex_empty = thm "bex_empty";
+val bex_one_point1 = thm "bex_one_point1";
+val bex_one_point2 = thm "bex_one_point2";
+val bex_simps = thms "bex_simps";
+val bex_triv = thm "bex_triv";
+val bex_triv_one_point1 = thm "bex_triv_one_point1";
+val bex_triv_one_point2 = thm "bex_triv_one_point2";
+val bool_induct = thm "bool_induct";
+val bspec = thm "bspec";
+val conj_mono = thm "conj_mono";
+val contra_subsetD = thm "contra_subsetD";
+val diff_single_insert = thm "diff_single_insert";
+val disj_mono = thm "disj_mono";
+val disjoint_eq_subset_Compl = thm "disjoint_eq_subset_Compl";
+val disjoint_iff_not_equal = thm "disjoint_iff_not_equal";
+val distinct_lemma = thm "distinct_lemma";
+val double_complement = thm "double_complement";
+val double_diff = thm "double_diff";
+val emptyE = thm "emptyE";
+val empty_Diff = thm "empty_Diff";
+val empty_def = thm "empty_def";
+val empty_iff = thm "empty_iff";
+val empty_subsetI = thm "empty_subsetI";
+val eq_to_mono = thm "eq_to_mono";
+val eq_to_mono2 = thm "eq_to_mono2";
+val eqset_imp_iff = thm "eqset_imp_iff";
+val equalityCE = thm "equalityCE";
+val equalityD1 = thm "equalityD1";
+val equalityD2 = thm "equalityD2";
+val equalityE = thm "equalityE";
+val equalityI = thm "equalityI";
+val equals0D = thm "equals0D";
+val equals0I = thm "equals0I";
+val ex_bool_eq = thm "ex_bool_eq";
+val ex_mono = thm "ex_mono";
+val full_SetCompr_eq = thm "full_SetCompr_eq";
+val if_image_distrib = thm "if_image_distrib";
+val imageE = thm "imageE";
+val imageI = thm "imageI";
+val image_Collect = thm "image_Collect";
+val image_Un = thm "image_Un";
+val image_Union = thm "image_Union";
+val image_cong = thm "image_cong";
+val image_constant = thm "image_constant";
+val image_def = thm "image_def";
+val image_empty = thm "image_empty";
+val image_eqI = thm "image_eqI";
+val image_iff = thm "image_iff";
+val image_image = thm "image_image";
+val image_insert = thm "image_insert";
+val image_is_empty = thm "image_is_empty";
+val image_mono = thm "image_mono";
+val image_subsetI = thm "image_subsetI";
+val image_subset_iff = thm "image_subset_iff";
+val imp_mono = thm "imp_mono";
+val imp_refl = thm "imp_refl";
+val in_mono = thm "in_mono";
+val insertCI = thm "insertCI";
+val insertE = thm "insertE";
+val insertI1 = thm "insertI1";
+val insertI2 = thm "insertI2";
+val insert_Collect = thm "insert_Collect";
+val insert_Diff = thm "insert_Diff";
+val insert_Diff1 = thm "insert_Diff1";
+val insert_Diff_if = thm "insert_Diff_if";
+val insert_absorb = thm "insert_absorb";
+val insert_absorb2 = thm "insert_absorb2";
+val insert_commute = thm "insert_commute";
+val insert_def = thm "insert_def";
+val insert_iff = thm "insert_iff";
+val insert_image = thm "insert_image";
+val insert_is_Un = thm "insert_is_Un";
+val insert_mono = thm "insert_mono";
+val insert_not_empty = thm "insert_not_empty";
+val insert_subset = thm "insert_subset";
+val mem_Collect_eq = thm "mem_Collect_eq";
+val mem_simps = thms "mem_simps";
+val mk_disjoint_insert = thm "mk_disjoint_insert";
+val mono_Int = thm "mono_Int";
+val mono_Un = thm "mono_Un";
+val not_psubset_empty = thm "not_psubset_empty";
+val psubsetI = thm "psubsetI";
+val psubset_def = thm "psubset_def";
+val psubset_eq = thm "psubset_eq";
+val psubset_imp_ex_mem = thm "psubset_imp_ex_mem";
+val psubset_imp_subset = thm "psubset_imp_subset";
+val psubset_insert_iff = thm "psubset_insert_iff";
+val psubset_subset_trans = thm "psubset_subset_trans";
+val rangeE = thm "rangeE";
+val rangeI = thm "rangeI";
+val range_composition = thm "range_composition";
+val range_eqI = thm "range_eqI";
+val rev_bexI = thm "rev_bexI";
+val rev_image_eqI = thm "rev_image_eqI";
+val rev_subsetD = thm "rev_subsetD";
+val set_diff_def = thm "set_diff_def";
+val set_eq_subset = thm "set_eq_subset";
+val set_ext = thm "set_ext";
+val setup_induction = thm "setup_induction";
+val singletonD = thm "singletonD";
+val singletonE = thm "singletonE";
+val singletonI = thm "singletonI";
+val singleton_conv = thm "singleton_conv";
+val singleton_conv2 = thm "singleton_conv2";
+val singleton_iff = thm "singleton_iff";
+val singleton_inject = thm "singleton_inject";
+val singleton_insert_inj_eq = thm "singleton_insert_inj_eq";
+val singleton_insert_inj_eq' = thm "singleton_insert_inj_eq'";
+val split_if_eq1 = thm "split_if_eq1";
+val split_if_eq2 = thm "split_if_eq2";
+val split_if_mem1 = thm "split_if_mem1";
+val split_if_mem2 = thm "split_if_mem2";
+val split_ifs = thms "split_ifs";
+val strip = thms "strip";
+val subsetCE = thm "subsetCE";
+val subsetD = thm "subsetD";
+val subsetI = thm "subsetI";
+val subset_Compl_self_eq = thm "subset_Compl_self_eq";
+val subset_Pow_Union = thm "subset_Pow_Union";
+val subset_UNIV = thm "subset_UNIV";
+val subset_Un_eq = thm "subset_Un_eq";
+val subset_antisym = thm "subset_antisym";
+val subset_def = thm "subset_def";
+val subset_empty = thm "subset_empty";
+val subset_iff = thm "subset_iff";
+val subset_iff_psubset_eq = thm "subset_iff_psubset_eq";
+val subset_image_iff = thm "subset_image_iff";
+val subset_insert = thm "subset_insert";
+val subset_insertI = thm "subset_insertI";
+val subset_insert_iff = thm "subset_insert_iff";
+val subset_psubset_trans = thm "subset_psubset_trans";
+val subset_refl = thm "subset_refl";
+val subset_singletonD = thm "subset_singletonD";
+val subset_trans = thm "subset_trans";
+val vimageD = thm "vimageD";
+val vimageE = thm "vimageE";
+val vimageI = thm "vimageI";
+val vimageI2 = thm "vimageI2";
+val vimage_Collect = thm "vimage_Collect";
+val vimage_Collect_eq = thm "vimage_Collect_eq";
+val vimage_Compl = thm "vimage_Compl";
+val vimage_Diff = thm "vimage_Diff";
+val vimage_INT = thm "vimage_INT";
+val vimage_Int = thm "vimage_Int";
+val vimage_UN = thm "vimage_UN";
+val vimage_UNIV = thm "vimage_UNIV";
+val vimage_Un = thm "vimage_Un";
+val vimage_Union = thm "vimage_Union";
+val vimage_def = thm "vimage_def";
+val vimage_empty = thm "vimage_empty";
+val vimage_eq = thm "vimage_eq";
+val vimage_eq_UN = thm "vimage_eq_UN";
+val vimage_insert = thm "vimage_insert";
+val vimage_mono = thm "vimage_mono";
+val vimage_singleton_eq = thm "vimage_singleton_eq";
+
 structure Set =
 struct
   val thy = the_context ();
@@ -24,25 +433,3 @@
   val set_diff_def = set_diff_def;
   val subset_def = subset_def;
 end;
-
-val vimageD = thm "vimageD";
-val vimageE = thm "vimageE";
-val vimageI = thm "vimageI";
-val vimageI2 = thm "vimageI2";
-val vimage_Collect = thm "vimage_Collect";
-val vimage_Collect_eq = thm "vimage_Collect_eq";
-val vimage_Compl = thm "vimage_Compl";
-val vimage_Diff = thm "vimage_Diff";
-val vimage_INT = thm "vimage_INT";
-val vimage_Int = thm "vimage_Int";
-val vimage_UN = thm "vimage_UN";
-val vimage_UNIV = thm "vimage_UNIV";
-val vimage_Un = thm "vimage_Un";
-val vimage_Union = thm "vimage_Union";
-val vimage_def = thm "vimage_def";
-val vimage_empty = thm "vimage_empty";
-val vimage_eq = thm "vimage_eq";
-val vimage_eq_UN = thm "vimage_eq_UN";
-val vimage_insert = thm "vimage_insert";
-val vimage_mono = thm "vimage_mono";
-val vimage_singleton_eq = thm "vimage_singleton_eq";