--- a/src/ZF/equalities.thy Sun Oct 07 15:49:25 2007 +0200
+++ b/src/ZF/equalities.thy Sun Oct 07 21:19:31 2007 +0200
@@ -971,279 +971,18 @@
Inter_greatest Int_greatest RepFun_subset
Un_upper1 Un_upper2 Int_lower1 Int_lower2
-(*First, ML bindings from the old file subset.ML*)
-ML
-{*
-val cons_subsetI = thm "cons_subsetI";
-val subset_consI = thm "subset_consI";
-val cons_subset_iff = thm "cons_subset_iff";
-val cons_subsetE = thm "cons_subsetE";
-val subset_empty_iff = thm "subset_empty_iff";
-val subset_cons_iff = thm "subset_cons_iff";
-val subset_succI = thm "subset_succI";
-val succ_subsetI = thm "succ_subsetI";
-val succ_subsetE = thm "succ_subsetE";
-val succ_subset_iff = thm "succ_subset_iff";
-val singleton_subsetI = thm "singleton_subsetI";
-val singleton_subsetD = thm "singleton_subsetD";
-val Union_subset_iff = thm "Union_subset_iff";
-val Union_upper = thm "Union_upper";
-val Union_least = thm "Union_least";
-val subset_UN_iff_eq = thm "subset_UN_iff_eq";
-val UN_subset_iff = thm "UN_subset_iff";
-val UN_upper = thm "UN_upper";
-val UN_least = thm "UN_least";
-val Inter_subset_iff = thm "Inter_subset_iff";
-val Inter_lower = thm "Inter_lower";
-val Inter_greatest = thm "Inter_greatest";
-val INT_lower = thm "INT_lower";
-val INT_greatest = thm "INT_greatest";
-val Un_subset_iff = thm "Un_subset_iff";
-val Un_upper1 = thm "Un_upper1";
-val Un_upper2 = thm "Un_upper2";
-val Un_least = thm "Un_least";
-val Int_subset_iff = thm "Int_subset_iff";
-val Int_lower1 = thm "Int_lower1";
-val Int_lower2 = thm "Int_lower2";
-val Int_greatest = thm "Int_greatest";
-val Diff_subset = thm "Diff_subset";
-val Diff_contains = thm "Diff_contains";
-val subset_Diff_cons_iff = thm "subset_Diff_cons_iff";
-val Collect_subset = thm "Collect_subset";
-val RepFun_subset = thm "RepFun_subset";
-
-val subset_SIs = thms "subset_SIs";
-
-val subset_cs = claset()
- delrules [subsetI, subsetCE]
- addSIs subset_SIs
- addIs [Union_upper, Inter_lower]
- addSEs [cons_subsetE];
+ML {*
+val subset_cs = @{claset}
+ delrules [@{thm subsetI}, @{thm subsetCE}]
+ addSIs @{thms subset_SIs}
+ addIs [@{thm Union_upper}, @{thm Inter_lower}]
+ addSEs [@{thm cons_subsetE}];
*}
(*subset_cs is a claset for subset reasoning*)
ML
{*
-val ZF_cs = claset() delrules [equalityI];
-
-val in_mono = thm "in_mono";
-val conj_mono = thm "conj_mono";
-val disj_mono = thm "disj_mono";
-val imp_mono = thm "imp_mono";
-val imp_refl = thm "imp_refl";
-val ex_mono = thm "ex_mono";
-val all_mono = thm "all_mono";
-
-val converse_iff = thm "converse_iff";
-val converseI = thm "converseI";
-val converseD = thm "converseD";
-val converseE = thm "converseE";
-val converse_converse = thm "converse_converse";
-val converse_type = thm "converse_type";
-val converse_prod = thm "converse_prod";
-val converse_empty = thm "converse_empty";
-val converse_subset_iff = thm "converse_subset_iff";
-val domain_iff = thm "domain_iff";
-val domainI = thm "domainI";
-val domainE = thm "domainE";
-val domain_subset = thm "domain_subset";
-val rangeI = thm "rangeI";
-val rangeE = thm "rangeE";
-val range_subset = thm "range_subset";
-val fieldI1 = thm "fieldI1";
-val fieldI2 = thm "fieldI2";
-val fieldCI = thm "fieldCI";
-val fieldE = thm "fieldE";
-val field_subset = thm "field_subset";
-val domain_subset_field = thm "domain_subset_field";
-val range_subset_field = thm "range_subset_field";
-val domain_times_range = thm "domain_times_range";
-val field_times_field = thm "field_times_field";
-val image_iff = thm "image_iff";
-val image_singleton_iff = thm "image_singleton_iff";
-val imageI = thm "imageI";
-val imageE = thm "imageE";
-val image_subset = thm "image_subset";
-val vimage_iff = thm "vimage_iff";
-val vimage_singleton_iff = thm "vimage_singleton_iff";
-val vimageI = thm "vimageI";
-val vimageE = thm "vimageE";
-val vimage_subset = thm "vimage_subset";
-val rel_Union = thm "rel_Union";
-val rel_Un = thm "rel_Un";
-val domain_Diff_eq = thm "domain_Diff_eq";
-val range_Diff_eq = thm "range_Diff_eq";
-val cons_eq = thm "cons_eq";
-val cons_commute = thm "cons_commute";
-val cons_absorb = thm "cons_absorb";
-val cons_Diff = thm "cons_Diff";
-val equal_singleton = thm "equal_singleton";
-val Int_cons = thm "Int_cons";
-val Int_absorb = thm "Int_absorb";
-val Int_left_absorb = thm "Int_left_absorb";
-val Int_commute = thm "Int_commute";
-val Int_left_commute = thm "Int_left_commute";
-val Int_assoc = thm "Int_assoc";
-val Int_Un_distrib = thm "Int_Un_distrib";
-val Int_Un_distrib2 = thm "Int_Un_distrib2";
-val subset_Int_iff = thm "subset_Int_iff";
-val subset_Int_iff2 = thm "subset_Int_iff2";
-val Int_Diff_eq = thm "Int_Diff_eq";
-val Int_cons_left = thm "Int_cons_left";
-val Int_cons_right = thm "Int_cons_right";
-val Un_cons = thm "Un_cons";
-val Un_absorb = thm "Un_absorb";
-val Un_left_absorb = thm "Un_left_absorb";
-val Un_commute = thm "Un_commute";
-val Un_left_commute = thm "Un_left_commute";
-val Un_assoc = thm "Un_assoc";
-val Un_Int_distrib = thm "Un_Int_distrib";
-val subset_Un_iff = thm "subset_Un_iff";
-val subset_Un_iff2 = thm "subset_Un_iff2";
-val Un_empty = thm "Un_empty";
-val Un_eq_Union = thm "Un_eq_Union";
-val Diff_cancel = thm "Diff_cancel";
-val Diff_triv = thm "Diff_triv";
-val empty_Diff = thm "empty_Diff";
-val Diff_0 = thm "Diff_0";
-val Diff_eq_0_iff = thm "Diff_eq_0_iff";
-val Diff_cons = thm "Diff_cons";
-val Diff_cons2 = thm "Diff_cons2";
-val Diff_disjoint = thm "Diff_disjoint";
-val Diff_partition = thm "Diff_partition";
-val subset_Un_Diff = thm "subset_Un_Diff";
-val double_complement = thm "double_complement";
-val double_complement_Un = thm "double_complement_Un";
-val Un_Int_crazy = thm "Un_Int_crazy";
-val Diff_Un = thm "Diff_Un";
-val Diff_Int = thm "Diff_Int";
-val Un_Diff = thm "Un_Diff";
-val Int_Diff = thm "Int_Diff";
-val Diff_Int_distrib = thm "Diff_Int_distrib";
-val Diff_Int_distrib2 = thm "Diff_Int_distrib2";
-val Un_Int_assoc_iff = thm "Un_Int_assoc_iff";
-val Union_cons = thm "Union_cons";
-val Union_Un_distrib = thm "Union_Un_distrib";
-val Union_Int_subset = thm "Union_Int_subset";
-val Union_disjoint = thm "Union_disjoint";
-val Union_empty_iff = thm "Union_empty_iff";
-val Int_Union2 = thm "Int_Union2";
-val Inter_0 = thm "Inter_0";
-val Inter_Un_subset = thm "Inter_Un_subset";
-val Inter_Un_distrib = thm "Inter_Un_distrib";
-val Union_singleton = thm "Union_singleton";
-val Inter_singleton = thm "Inter_singleton";
-val Inter_cons = thm "Inter_cons";
-val Union_eq_UN = thm "Union_eq_UN";
-val Inter_eq_INT = thm "Inter_eq_INT";
-val UN_0 = thm "UN_0";
-val UN_singleton = thm "UN_singleton";
-val UN_Un = thm "UN_Un";
-val INT_Un = thm "INT_Un";
-val UN_UN_flatten = thm "UN_UN_flatten";
-val Int_UN_distrib = thm "Int_UN_distrib";
-val Un_INT_distrib = thm "Un_INT_distrib";
-val Int_UN_distrib2 = thm "Int_UN_distrib2";
-val Un_INT_distrib2 = thm "Un_INT_distrib2";
-val UN_constant = thm "UN_constant";
-val INT_constant = thm "INT_constant";
-val UN_RepFun = thm "UN_RepFun";
-val INT_RepFun = thm "INT_RepFun";
-val INT_Union_eq = thm "INT_Union_eq";
-val INT_UN_eq = thm "INT_UN_eq";
-val UN_Un_distrib = thm "UN_Un_distrib";
-val INT_Int_distrib = thm "INT_Int_distrib";
-val UN_Int_subset = thm "UN_Int_subset";
-val Diff_UN = thm "Diff_UN";
-val Diff_INT = thm "Diff_INT";
-val Sigma_cons1 = thm "Sigma_cons1";
-val Sigma_cons2 = thm "Sigma_cons2";
-val Sigma_succ1 = thm "Sigma_succ1";
-val Sigma_succ2 = thm "Sigma_succ2";
-val SUM_UN_distrib1 = thm "SUM_UN_distrib1";
-val SUM_UN_distrib2 = thm "SUM_UN_distrib2";
-val SUM_Un_distrib1 = thm "SUM_Un_distrib1";
-val SUM_Un_distrib2 = thm "SUM_Un_distrib2";
-val prod_Un_distrib2 = thm "prod_Un_distrib2";
-val SUM_Int_distrib1 = thm "SUM_Int_distrib1";
-val SUM_Int_distrib2 = thm "SUM_Int_distrib2";
-val prod_Int_distrib2 = thm "prod_Int_distrib2";
-val SUM_eq_UN = thm "SUM_eq_UN";
-val domain_of_prod = thm "domain_of_prod";
-val domain_0 = thm "domain_0";
-val domain_cons = thm "domain_cons";
-val domain_Un_eq = thm "domain_Un_eq";
-val domain_Int_subset = thm "domain_Int_subset";
-val domain_Diff_subset = thm "domain_Diff_subset";
-val domain_converse = thm "domain_converse";
-val domain_UN = thm "domain_UN";
-val domain_Union = thm "domain_Union";
-val range_of_prod = thm "range_of_prod";
-val range_0 = thm "range_0";
-val range_cons = thm "range_cons";
-val range_Un_eq = thm "range_Un_eq";
-val range_Int_subset = thm "range_Int_subset";
-val range_Diff_subset = thm "range_Diff_subset";
-val range_converse = thm "range_converse";
-val field_of_prod = thm "field_of_prod";
-val field_0 = thm "field_0";
-val field_cons = thm "field_cons";
-val field_Un_eq = thm "field_Un_eq";
-val field_Int_subset = thm "field_Int_subset";
-val field_Diff_subset = thm "field_Diff_subset";
-val field_converse = thm "field_converse";
-val image_0 = thm "image_0";
-val image_Un = thm "image_Un";
-val image_Int_subset = thm "image_Int_subset";
-val image_Int_square_subset = thm "image_Int_square_subset";
-val image_Int_square = thm "image_Int_square";
-val image_0_left = thm "image_0_left";
-val image_Un_left = thm "image_Un_left";
-val image_Int_subset_left = thm "image_Int_subset_left";
-val vimage_0 = thm "vimage_0";
-val vimage_Un = thm "vimage_Un";
-val vimage_Int_subset = thm "vimage_Int_subset";
-val vimage_eq_UN = thm "vimage_eq_UN";
-val function_vimage_Int = thm "function_vimage_Int";
-val function_vimage_Diff = thm "function_vimage_Diff";
-val function_image_vimage = thm "function_image_vimage";
-val vimage_Int_square_subset = thm "vimage_Int_square_subset";
-val vimage_Int_square = thm "vimage_Int_square";
-val vimage_0_left = thm "vimage_0_left";
-val vimage_Un_left = thm "vimage_Un_left";
-val vimage_Int_subset_left = thm "vimage_Int_subset_left";
-val converse_Un = thm "converse_Un";
-val converse_Int = thm "converse_Int";
-val converse_Diff = thm "converse_Diff";
-val converse_UN = thm "converse_UN";
-val converse_INT = thm "converse_INT";
-val Pow_0 = thm "Pow_0";
-val Pow_insert = thm "Pow_insert";
-val Un_Pow_subset = thm "Un_Pow_subset";
-val UN_Pow_subset = thm "UN_Pow_subset";
-val subset_Pow_Union = thm "subset_Pow_Union";
-val Union_Pow_eq = thm "Union_Pow_eq";
-val Union_Pow_iff = thm "Union_Pow_iff";
-val Pow_Int_eq = thm "Pow_Int_eq";
-val Pow_INT_eq = thm "Pow_INT_eq";
-val RepFun_eq_0_iff = thm "RepFun_eq_0_iff";
-val RepFun_constant = thm "RepFun_constant";
-val Collect_Un = thm "Collect_Un";
-val Collect_Int = thm "Collect_Int";
-val Collect_Diff = thm "Collect_Diff";
-val Collect_cons = thm "Collect_cons";
-val Int_Collect_self_eq = thm "Int_Collect_self_eq";
-val Collect_Collect_eq = thm "Collect_Collect_eq";
-val Collect_Int_Collect_eq = thm "Collect_Int_Collect_eq";
-val Collect_disj_eq = thm "Collect_disj_eq";
-val Collect_conj_eq = thm "Collect_conj_eq";
-
-val Int_ac = thms "Int_ac";
-val Un_ac = thms "Un_ac";
-val Int_absorb1 = thm "Int_absorb1";
-val Int_absorb2 = thm "Int_absorb2";
-val Un_absorb1 = thm "Un_absorb1";
-val Un_absorb2 = thm "Un_absorb2";
+val ZF_cs = @{claset} delrules [@{thm equalityI}];
*}
end