--- a/src/HOL/IsaMakefile Fri Feb 15 20:43:44 2002 +0100
+++ b/src/HOL/IsaMakefile Sat Feb 16 20:59:34 2002 +0100
@@ -102,8 +102,7 @@
Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \
Wellfounded_Recursion.ML Wellfounded_Recursion.thy Wellfounded_Relations.ML \
Wellfounded_Relations.thy arith_data.ML blastdata.ML cladata.ML \
- document/root.tex equalities.ML hologic.ML meson_lemmas.ML mono.ML \
- simpdata.ML subset.ML thy_syntax.ML
+ document/root.tex hologic.ML meson_lemmas.ML simpdata.ML thy_syntax.ML
@$(ISATOOL) usedir -b -g true $(OUT)/Pure HOL
--- 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";
--- a/src/HOL/Set.thy Fri Feb 15 20:43:44 2002 +0100
+++ b/src/HOL/Set.thy Sat Feb 16 20:59:34 2002 +0100
@@ -6,8 +6,7 @@
header {* Set theory for higher-order logic *}
-theory Set = HOL
-files ("subset.ML") ("equalities.ML") ("mono.ML"):
+theory Set = HOL:
text {* A set in HOL is simply a predicate. *}
@@ -339,7 +338,7 @@
subsubsection {* Subsets *}
-lemma subsetI [intro!]: "(!!x. x:A ==> x:B) ==> A <= B"
+lemma subsetI [intro!]: "(!!x. x:A ==> x:B) ==> A \<subseteq> B"
by (simp add: subset_def)
text {*
@@ -364,13 +363,13 @@
Blast.overloaded (\"image\", domain_type);
"
-lemma subsetD [elim]: "A <= B ==> c:A ==> c:B"
+lemma subsetD [elim]: "A \<subseteq> B ==> c \<in> A ==> c \<in> B"
-- {* Rule in Modus Ponens style. *}
by (unfold subset_def) blast
declare subsetD [intro?] -- FIXME
-lemma rev_subsetD: "c:A ==> A <= B ==> c:B"
+lemma rev_subsetD: "c \<in> A ==> A \<subseteq> B ==> c \<in> B"
-- {* The same, with reversed premises for use with @{text erule} --
cf @{text rev_mp}. *}
by (rule subsetD)
@@ -378,7 +377,7 @@
declare rev_subsetD [intro?] -- FIXME
text {*
- \medskip Converts @{prop "A <= B"} to @{prop "x:A ==> x:B"}.
+ \medskip Converts @{prop "A \<subseteq> B"} to @{prop "x \<in> A ==> x \<in> B"}.
*}
ML {*
@@ -386,13 +385,13 @@
in fun impOfSubs th = th RSN (2, rev_subsetD) end;
*}
-lemma subsetCE [elim]: "A <= B ==> (c~:A ==> P) ==> (c:B ==> P) ==> P"
+lemma subsetCE [elim]: "A \<subseteq> B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
-- {* Classical elimination rule. *}
by (unfold subset_def) blast
text {*
- \medskip Takes assumptions @{prop "A <= B"}; @{prop "c:A"} and
- creates the assumption @{prop "c:B"}.
+ \medskip Takes assumptions @{prop "A \<subseteq> B"}; @{prop "c \<in> A"} and
+ creates the assumption @{prop "c \<in> B"}.
*}
ML {*
@@ -400,46 +399,46 @@
in fun set_mp_tac i = etac subsetCE i THEN mp_tac i end;
*}
-lemma contra_subsetD: "A <= B ==> c ~: B ==> c ~: A"
+lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
by blast
-lemma subset_refl: "A <= (A::'a set)"
+lemma subset_refl: "A \<subseteq> A"
by fast
-lemma subset_trans: "A <= B ==> B <= C ==> A <= (C::'a set)"
+lemma subset_trans: "A \<subseteq> B ==> B \<subseteq> C ==> A \<subseteq> C"
by blast
subsubsection {* Equality *}
-lemma subset_antisym [intro!]: "A <= B ==> B <= A ==> A = (B::'a set)"
+lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
-- {* Anti-symmetry of the subset relation. *}
- by (rule set_ext) (blast intro: subsetD)
-
-lemmas equalityI = subset_antisym
+ by (rules intro: set_ext subsetD)
+
+lemmas equalityI [intro!] = subset_antisym
text {*
\medskip Equality rules from ZF set theory -- are they appropriate
here?
*}
-lemma equalityD1: "A = B ==> A <= (B::'a set)"
+lemma equalityD1: "A = B ==> A \<subseteq> B"
by (simp add: subset_refl)
-lemma equalityD2: "A = B ==> B <= (A::'a set)"
+lemma equalityD2: "A = B ==> B \<subseteq> A"
by (simp add: subset_refl)
text {*
\medskip Be careful when adding this to the claset as @{text
subset_empty} is in the simpset: @{prop "A = {}"} goes to @{prop "{}
- <= A"} and @{prop "A <= {}"} and then back to @{prop "A = {}"}!
+ \<subseteq> A"} and @{prop "A \<subseteq> {}"} and then back to @{prop "A = {}"}!
*}
-lemma equalityE: "A = B ==> (A <= B ==> B <= (A::'a set) ==> P) ==> P"
+lemma equalityE: "A = B ==> (A \<subseteq> B ==> B \<subseteq> A ==> P) ==> P"
by (simp add: subset_refl)
lemma equalityCE [elim]:
- "A = B ==> (c:A ==> c:B ==> P) ==> (c~:A ==> c~:B ==> P) ==> P"
+ "A = B ==> (c \<in> A ==> c \<in> B ==> P) ==> (c \<notin> A ==> c \<notin> B ==> P) ==> P"
by blast
text {*
@@ -466,7 +465,7 @@
lemma UNIV_witness [intro?]: "EX x. x : UNIV"
by simp
-lemma subset_UNIV: "A <= UNIV"
+lemma subset_UNIV: "A \<subseteq> UNIV"
by (rule subsetI) (rule UNIV_I)
text {*
@@ -490,14 +489,14 @@
lemma emptyE [elim!]: "a : {} ==> P"
by simp
-lemma empty_subsetI [iff]: "{} <= A"
+lemma empty_subsetI [iff]: "{} \<subseteq> A"
-- {* One effect is to delete the ASSUMPTION @{prop "{} <= A"} *}
by blast
-lemma equals0I: "(!!y. y:A ==> False) ==> A = {}"
+lemma equals0I: "(!!y. y \<in> A ==> False) ==> A = {}"
by blast
-lemma equals0D: "A={} ==> a ~: A"
+lemma equals0D: "A = {} ==> a \<notin> A"
-- {* Use for reasoning about disjointness: @{prop "A Int B = {}"} *}
by blast
@@ -513,28 +512,28 @@
subsubsection {* The Powerset operator -- Pow *}
-lemma Pow_iff [iff]: "(A : Pow B) = (A <= B)"
+lemma Pow_iff [iff]: "(A \<in> Pow B) = (A \<subseteq> B)"
by (simp add: Pow_def)
-lemma PowI: "A <= B ==> A : Pow B"
+lemma PowI: "A \<subseteq> B ==> A \<in> Pow B"
by (simp add: Pow_def)
-lemma PowD: "A : Pow B ==> A <= B"
+lemma PowD: "A \<in> Pow B ==> A \<subseteq> B"
by (simp add: Pow_def)
-lemma Pow_bottom: "{}: Pow B"
+lemma Pow_bottom: "{} \<in> Pow B"
by simp
-lemma Pow_top: "A : Pow A"
+lemma Pow_top: "A \<in> Pow A"
by (simp add: subset_refl)
subsubsection {* Set complement *}
-lemma Compl_iff [simp]: "(c : -A) = (c~:A)"
+lemma Compl_iff [simp]: "(c \<in> -A) = (c \<notin> A)"
by (unfold Compl_def) blast
-lemma ComplI [intro!]: "(c:A ==> False) ==> c : -A"
+lemma ComplI [intro!]: "(c \<in> A ==> False) ==> c \<in> -A"
by (unfold Compl_def) blast
text {*
@@ -625,7 +624,7 @@
-- {* Classical introduction rule. *}
by auto
-lemma subset_insert_iff: "(A <= insert x B) = (if x:A then A - {x} <= B else A <= B)"
+lemma subset_insert_iff: "(A \<subseteq> insert x B) = (if x:A then A - {x} \<subseteq> B else A \<subseteq> B)"
by auto
@@ -646,13 +645,13 @@
lemma singleton_inject [dest!]: "{a} = {b} ==> a = b"
by blast
-lemma singleton_insert_inj_eq [iff]: "({b} = insert a A) = (a = b & A <= {b})"
+lemma singleton_insert_inj_eq [iff]: "({b} = insert a A) = (a = b & A \<subseteq> {b})"
by blast
-lemma singleton_insert_inj_eq' [iff]: "(insert a A = {b}) = (a = b & A <= {b})"
+lemma singleton_insert_inj_eq' [iff]: "(insert a A = {b}) = (a = b & A \<subseteq> {b})"
by blast
-lemma subset_singletonD: "A <= {x} ==> A={} | A = {x}"
+lemma subset_singletonD: "A \<subseteq> {x} ==> A = {} | A = {x}"
by fast
lemma singleton_conv [simp]: "{x. x = a} = {a}"
@@ -661,7 +660,7 @@
lemma singleton_conv2 [simp]: "{x. a = x} = {a}"
by blast
-lemma diff_single_insert: "A - {x} <= B ==> x : A ==> A <= insert x B"
+lemma diff_single_insert: "A - {x} \<subseteq> B ==> x \<in> A ==> A \<subseteq> insert x B"
by blast
@@ -772,18 +771,18 @@
lemma image_iff: "(z : f`A) = (EX x:A. z = f x)"
by blast
-lemma image_subset_iff: "(f`A <= B) = (ALL x:A. f x: B)"
+lemma image_subset_iff: "(f`A \<subseteq> B) = (\<forall>x\<in>A. f x \<in> B)"
-- {* This rewrite rule would confuse users if made default. *}
by blast
-lemma subset_image_iff: "(B <= f ` A) = (EX AA. AA <= A & B = f ` AA)"
+lemma subset_image_iff: "(B \<subseteq> f`A) = (EX AA. AA \<subseteq> A & B = f`AA)"
apply safe
prefer 2 apply fast
apply (rule_tac x = "{a. a : A & f a : B}" in exI)
apply fast
done
-lemma image_subsetI: "(!!x. x:A ==> f x : B) ==> f`A <= B"
+lemma image_subsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> f`A \<subseteq> B"
-- {* Replaces the three steps @{text subsetI}, @{text imageE},
@{text hypsubst}, but breaks too many existing proofs. *}
by blast
@@ -792,13 +791,13 @@
\medskip Range of a function -- just a translation for image!
*}
-lemma range_eqI: "b = f x ==> b : range f"
+lemma range_eqI: "b = f x ==> b \<in> range f"
by simp
-lemma rangeI: "f x : range f"
+lemma rangeI: "f x \<in> range f"
by simp
-lemma rangeE [elim?]: "b : range (%x. f x) ==> (!!x. b = f x ==> P) ==> P"
+lemma rangeE [elim?]: "b \<in> range (\<lambda>x. f x) ==> (!!x. b = f x ==> P) ==> P"
by blast
@@ -852,32 +851,30 @@
subsubsection {* The ``proper subset'' relation *}
-lemma psubsetI [intro!]: "(A::'a set) <= B ==> A ~= B ==> A < B"
+lemma psubsetI [intro!]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
by (unfold psubset_def) blast
lemma psubset_insert_iff:
- "(A < insert x B) = (if x:B then A < B else if x:A then A - {x} < B else A <= B)"
- apply (simp add: psubset_def subset_insert_iff)
- apply blast
- done
-
-lemma psubset_eq: "((A::'a set) < B) = (A <= B & A ~= B)"
+ "(A \<subset> insert x B) = (if x \<in> B then A \<subset> B else if x \<in> A then A - {x} \<subset> B else A \<subseteq> B)"
+ by (auto simp add: psubset_def subset_insert_iff)
+
+lemma psubset_eq: "(A \<subset> B) = (A \<subseteq> B & A \<noteq> B)"
by (simp only: psubset_def)
-lemma psubset_imp_subset: "(A::'a set) < B ==> A <= B"
+lemma psubset_imp_subset: "A \<subset> B ==> A \<subseteq> B"
by (simp add: psubset_eq)
-lemma psubset_subset_trans: "(A::'a set) < B ==> B <= C ==> A < C"
+lemma psubset_subset_trans: "A \<subset> B ==> B \<subseteq> C ==> A \<subset> C"
by (auto simp add: psubset_eq)
-lemma subset_psubset_trans: "(A::'a set) <= B ==> B < C ==> A < C"
+lemma subset_psubset_trans: "A \<subseteq> B ==> B \<subset> C ==> A \<subset> C"
by (auto simp add: psubset_eq)
-lemma psubset_imp_ex_mem: "A < B ==> EX b. b : (B - A)"
+lemma psubset_imp_ex_mem: "A \<subset> B ==> \<exists>b. b \<in> (B - A)"
by (unfold psubset_def) blast
lemma atomize_ball:
- "(!!x. x:A ==> P x) == Trueprop (ALL x:A. P x)"
+ "(!!x. x \<in> A ==> P x) == Trueprop (\<forall>x\<in>A. P x)"
by (simp only: Ball_def atomize_all atomize_imp)
declare atomize_ball [symmetric, rulify]
@@ -885,9 +882,898 @@
subsection {* Further set-theory lemmas *}
-use "subset.ML"
-use "equalities.ML"
-use "mono.ML"
+subsubsection {* Derived rules involving subsets. *}
+
+text {* @{text insert}. *}
+
+lemma subset_insertI: "B \<subseteq> insert a B"
+ apply (rule subsetI)
+ apply (erule insertI2)
+ done
+
+lemma subset_insert: "x \<notin> A ==> (A \<subseteq> insert x B) = (A \<subseteq> B)"
+ by blast
+
+
+text {* \medskip Big Union -- least upper bound of a set. *}
+
+lemma Union_upper: "B \<in> A ==> B \<subseteq> Union A"
+ by (rules intro: subsetI UnionI)
+
+lemma Union_least: "(!!X. X \<in> A ==> X \<subseteq> C) ==> Union A \<subseteq> C"
+ by (rules intro: subsetI elim: UnionE dest: subsetD)
+
+
+text {* \medskip General union. *}
+
+lemma UN_upper: "a \<in> A ==> B a \<subseteq> (\<Union>x\<in>A. B x)"
+ by blast
+
+lemma UN_least: "(!!x. x \<in> A ==> B x \<subseteq> C) ==> (\<Union>x\<in>A. B x) \<subseteq> C"
+ by (rules intro: subsetI elim: UN_E dest: subsetD)
+
+
+text {* \medskip Big Intersection -- greatest lower bound of a set. *}
+
+lemma Inter_lower: "B \<in> A ==> Inter A \<subseteq> B"
+ by blast
+
+lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A"
+ by (rules intro: InterI subsetI dest: subsetD)
+
+lemma INT_lower: "a \<in> A ==> (\<Inter>x\<in>A. B x) \<subseteq> B a"
+ by blast
+
+lemma INT_greatest: "(!!x. x \<in> A ==> C \<subseteq> B x) ==> C \<subseteq> (\<Inter>x\<in>A. B x)"
+ by (rules intro: INT_I subsetI dest: subsetD)
+
+
+text {* \medskip Finite Union -- the least upper bound of two sets. *}
+
+lemma Un_upper1: "A \<subseteq> A \<union> B"
+ by blast
+
+lemma Un_upper2: "B \<subseteq> A \<union> B"
+ by blast
+
+lemma Un_least: "A \<subseteq> C ==> B \<subseteq> C ==> A \<union> B \<subseteq> C"
+ by blast
+
+
+text {* \medskip Finite Intersection -- the greatest lower bound of two sets. *}
+
+lemma Int_lower1: "A \<inter> B \<subseteq> A"
+ by blast
+
+lemma Int_lower2: "A \<inter> B \<subseteq> B"
+ by blast
+
+lemma Int_greatest: "C \<subseteq> A ==> C \<subseteq> B ==> C \<subseteq> A \<inter> B"
+ by blast
+
+
+text {* \medskip Set difference. *}
+
+lemma Diff_subset: "A - B \<subseteq> A"
+ by blast
+
+
+text {* \medskip Monotonicity. *}
+
+lemma mono_Un: "mono f ==> f A \<union> f B \<subseteq> f (A \<union> B)"
+ apply (rule Un_least)
+ apply (erule Un_upper1 [THEN [2] monoD])
+ apply (erule Un_upper2 [THEN [2] monoD])
+ done
+
+lemma mono_Int: "mono f ==> f (A \<inter> B) \<subseteq> f A \<inter> f B"
+ apply (rule Int_greatest)
+ apply (erule Int_lower1 [THEN [2] monoD])
+ apply (erule Int_lower2 [THEN [2] monoD])
+ done
+
+
+subsubsection {* Equalities involving union, intersection, inclusion, etc. *}
+
+text {* @{text "{}"}. *}
+
+lemma Collect_const [simp]: "{s. P} = (if P then UNIV else {})"
+ -- {* supersedes @{text "Collect_False_empty"} *}
+ by auto
+
+lemma subset_empty [simp]: "(A \<subseteq> {}) = (A = {})"
+ by blast
+
+lemma not_psubset_empty [iff]: "\<not> (A < {})"
+ by (unfold psubset_def) blast
+
+lemma Collect_empty_eq [simp]: "(Collect P = {}) = (\<forall>x. \<not> P x)"
+ by auto
+
+lemma Collect_neg_eq: "{x. \<not> P x} = - {x. P x}"
+ by blast
+
+lemma Collect_disj_eq: "{x. P x | Q x} = {x. P x} \<union> {x. Q x}"
+ by blast
+
+lemma Collect_conj_eq: "{x. P x & Q x} = {x. P x} \<inter> {x. Q x}"
+ by blast
+
+lemma Collect_all_eq: "{x. \<forall>y. P x y} = (\<Inter>y. {x. P x y})"
+ by blast
+
+lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
+ by blast
+
+lemma Collect_ex_eq: "{x. \<exists>y. P x y} = (\<Union>y. {x. P x y})"
+ by blast
+
+lemma Collect_bex_eq: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
+ by blast
+
+
+text {* \medskip @{text insert}. *}
+
+lemma insert_is_Un: "insert a A = {a} Un A"
+ -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a {}"} *}
+ by blast
+
+lemma insert_not_empty [simp]: "insert a A \<noteq> {}"
+ by blast
+
+lemmas empty_not_insert [simp] = insert_not_empty [symmetric, standard]
+
+lemma insert_absorb: "a \<in> A ==> insert a A = A"
+ -- {* @{text "[simp]"} causes recursive calls when there are nested inserts *}
+ -- {* with \emph{quadratic} running time *}
+ by blast
+
+lemma insert_absorb2 [simp]: "insert x (insert x A) = insert x A"
+ by blast
+
+lemma insert_commute: "insert x (insert y A) = insert y (insert x A)"
+ by blast
+
+lemma insert_subset [simp]: "(insert x A \<subseteq> B) = (x \<in> B & A \<subseteq> B)"
+ by blast
+
+lemma mk_disjoint_insert: "a \<in> A ==> \<exists>B. A = insert a B & a \<notin> B"
+ -- {* use new @{text B} rather than @{text "A - {a}"} to avoid infinite unfolding *}
+ apply (rule_tac x = "A - {a}" in exI)
+ apply blast
+ done
+
+lemma insert_Collect: "insert a (Collect P) = {u. u \<noteq> a --> P u}"
+ by auto
+
+lemma UN_insert_distrib: "u \<in> A ==> (\<Union>x\<in>A. insert a (B x)) = insert a (\<Union>x\<in>A. B x)"
+ by blast
+
+
+text {* \medskip @{text image}. *}
+
+lemma image_empty [simp]: "f`{} = {}"
+ by blast
+
+lemma image_insert [simp]: "f ` insert a B = insert (f a) (f`B)"
+ by blast
+
+lemma image_constant: "x \<in> A ==> (\<lambda>x. c) ` A = {c}"
+ by blast
+
+lemma image_image: "f ` (g ` A) = (\<lambda>x. f (g x)) ` A"
+ by blast
+
+lemma insert_image [simp]: "x \<in> A ==> insert (f x) (f`A) = f`A"
+ by blast
+
+lemma image_is_empty [iff]: "(f`A = {}) = (A = {})"
+ by blast
+
+lemma image_Collect: "f ` {x. P x} = {f x | x. P x}"
+ -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS, *}
+ -- {* with its implicit quantifier and conjunction. Also image enjoys better *}
+ -- {* equational properties than does the RHS. *}
+ by blast
+
+lemma if_image_distrib [simp]:
+ "(\<lambda>x. if P x then f x else g x) ` S
+ = (f ` (S \<inter> {x. P x})) \<union> (g ` (S \<inter> {x. \<not> P x}))"
+ by (auto simp add: image_def)
+
+lemma image_cong: "M = N ==> (!!x. x \<in> N ==> f x = g x) ==> f`M = g`N"
+ by (simp add: image_def)
+
+
+text {* \medskip @{text range}. *}
+
+lemma full_SetCompr_eq: "{u. \<exists>x. u = f x} = range f"
+ by auto
+
+lemma range_composition [simp]: "range (\<lambda>x. f (g x)) = f`range g"
+ apply (subst image_image)
+ apply simp
+ done
+
+
+text {* \medskip @{text Int} *}
+
+lemma Int_absorb [simp]: "A \<inter> A = A"
+ by blast
+
+lemma Int_left_absorb: "A \<inter> (A \<inter> B) = A \<inter> B"
+ by blast
+
+lemma Int_commute: "A \<inter> B = B \<inter> A"
+ by blast
+
+lemma Int_left_commute: "A \<inter> (B \<inter> C) = B \<inter> (A \<inter> C)"
+ by blast
+
+lemma Int_assoc: "(A \<inter> B) \<inter> C = A \<inter> (B \<inter> C)"
+ by blast
+
+lemmas Int_ac = Int_assoc Int_left_absorb Int_commute Int_left_commute
+ -- {* Intersection is an AC-operator *}
+
+lemma Int_absorb1: "B \<subseteq> A ==> A \<inter> B = B"
+ by blast
+
+lemma Int_absorb2: "A \<subseteq> B ==> A \<inter> B = A"
+ by blast
+
+lemma Int_empty_left [simp]: "{} \<inter> B = {}"
+ by blast
+
+lemma Int_empty_right [simp]: "A \<inter> {} = {}"
+ by blast
+
+lemma disjoint_eq_subset_Compl: "(A \<inter> B = {}) = (A \<subseteq> -B)"
+ by blast
+
+lemma disjoint_iff_not_equal: "(A \<inter> B = {}) = (\<forall>x\<in>A. \<forall>y\<in>B. x \<noteq> y)"
+ by blast
+
+lemma Int_UNIV_left [simp]: "UNIV \<inter> B = B"
+ by blast
+
+lemma Int_UNIV_right [simp]: "A \<inter> UNIV = A"
+ by blast
+
+lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
+ by blast
+
+lemma Int_Un_distrib: "A \<inter> (B \<union> C) = (A \<inter> B) \<union> (A \<inter> C)"
+ by blast
+
+lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
+ by blast
+
+lemma Int_UNIV [simp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
+ by blast
+
+lemma Int_subset_iff: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
+ by blast
+
+lemma Int_Collect: "(x \<in> A \<inter> {x. P x}) = (x \<in> A & P x)"
+ by blast
+
+
+text {* \medskip @{text Un}. *}
+
+lemma Un_absorb [simp]: "A \<union> A = A"
+ by blast
+
+lemma Un_left_absorb: "A \<union> (A \<union> B) = A \<union> B"
+ by blast
+
+lemma Un_commute: "A \<union> B = B \<union> A"
+ by blast
+
+lemma Un_left_commute: "A \<union> (B \<union> C) = B \<union> (A \<union> C)"
+ by blast
+
+lemma Un_assoc: "(A \<union> B) \<union> C = A \<union> (B \<union> C)"
+ by blast
+
+lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute
+ -- {* Union is an AC-operator *}
+
+lemma Un_absorb1: "A \<subseteq> B ==> A \<union> B = B"
+ by blast
+
+lemma Un_absorb2: "B \<subseteq> A ==> A \<union> B = A"
+ by blast
+
+lemma Un_empty_left [simp]: "{} \<union> B = B"
+ by blast
+
+lemma Un_empty_right [simp]: "A \<union> {} = A"
+ by blast
+
+lemma Un_UNIV_left [simp]: "UNIV \<union> B = UNIV"
+ by blast
+
+lemma Un_UNIV_right [simp]: "A \<union> UNIV = UNIV"
+ by blast
+
+lemma Un_eq_Union: "A \<union> B = \<Union>{A, B}"
+ by blast
+
+lemma Un_insert_left [simp]: "(insert a B) \<union> C = insert a (B \<union> C)"
+ by blast
+
+lemma Un_insert_right [simp]: "A \<union> (insert a B) = insert a (A \<union> B)"
+ by blast
+
+lemma Int_insert_left:
+ "(insert a B) Int C = (if a \<in> C then insert a (B \<inter> C) else B \<inter> C)"
+ by auto
+
+lemma Int_insert_right:
+ "A \<inter> (insert a B) = (if a \<in> A then insert a (A \<inter> B) else A \<inter> B)"
+ by auto
+
+lemma Un_Int_distrib: "A \<union> (B \<inter> C) = (A \<union> B) \<inter> (A \<union> C)"
+ by blast
+
+lemma Un_Int_distrib2: "(B \<inter> C) \<union> A = (B \<union> A) \<inter> (C \<union> A)"
+ by blast
+
+lemma Un_Int_crazy:
+ "(A \<inter> B) \<union> (B \<inter> C) \<union> (C \<inter> A) = (A \<union> B) \<inter> (B \<union> C) \<inter> (C \<union> A)"
+ by blast
+
+lemma subset_Un_eq: "(A \<subseteq> B) = (A \<union> B = B)"
+ by blast
+
+lemma Un_empty [iff]: "(A \<union> B = {}) = (A = {} & B = {})"
+ by blast
+
+lemma Un_subset_iff: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
+ by blast
+
+lemma Un_Diff_Int: "(A - B) \<union> (A \<inter> B) = A"
+ by blast
+
+
+text {* \medskip Set complement *}
+
+lemma Compl_disjoint [simp]: "A \<inter> -A = {}"
+ by blast
+
+lemma Compl_disjoint2 [simp]: "-A \<inter> A = {}"
+ by blast
+
+lemma Compl_partition: "A \<union> (-A) = UNIV"
+ by blast
+
+lemma double_complement [simp]: "- (-A) = (A::'a set)"
+ by blast
+
+lemma Compl_Un [simp]: "-(A \<union> B) = (-A) \<inter> (-B)"
+ by blast
+
+lemma Compl_Int [simp]: "-(A \<inter> B) = (-A) \<union> (-B)"
+ by blast
+
+lemma Compl_UN [simp]: "-(\<Union>x\<in>A. B x) = (\<Inter>x\<in>A. -B x)"
+ by blast
+
+lemma Compl_INT [simp]: "-(\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)"
+ by blast
+
+lemma subset_Compl_self_eq: "(A \<subseteq> -A) = (A = {})"
+ by blast
+
+lemma Un_Int_assoc_eq: "((A \<inter> B) \<union> C = A \<inter> (B \<union> C)) = (C \<subseteq> A)"
+ -- {* Halmos, Naive Set Theory, page 16. *}
+ by blast
+
+lemma Compl_UNIV_eq [simp]: "-UNIV = {}"
+ by blast
+
+lemma Compl_empty_eq [simp]: "-{} = UNIV"
+ by blast
+
+lemma Compl_subset_Compl_iff [iff]: "(-A \<subseteq> -B) = (B \<subseteq> A)"
+ by blast
+
+lemma Compl_eq_Compl_iff [iff]: "(-A = -B) = (A = (B::'a set))"
+ by blast
+
+
+text {* \medskip @{text Union}. *}
+
+lemma Union_empty [simp]: "Union({}) = {}"
+ by blast
+
+lemma Union_UNIV [simp]: "Union UNIV = UNIV"
+ by blast
+
+lemma Union_insert [simp]: "Union (insert a B) = a \<union> \<Union>B"
+ by blast
+
+lemma Union_Un_distrib [simp]: "\<Union>(A Un B) = \<Union>A \<union> \<Union>B"
+ by blast
+
+lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"
+ by blast
+
+lemma Union_empty_conv [iff]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
+ by auto
+
+lemma Union_disjoint: "(\<Union>C \<inter> A = {}) = (\<forall>B\<in>C. B \<inter> A = {})"
+ by blast
+
+
+text {* \medskip @{text Inter}. *}
+
+lemma Inter_empty [simp]: "\<Inter>{} = UNIV"
+ by blast
+
+lemma Inter_UNIV [simp]: "\<Inter>UNIV = {}"
+ by blast
+
+lemma Inter_insert [simp]: "\<Inter>(insert a B) = a \<inter> \<Inter>B"
+ by blast
+
+lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)"
+ by blast
+
+lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
+ by blast
+
+
+text {*
+ \medskip @{text UN} and @{text INT}.
+
+ Basic identities: *}
+
+lemma UN_empty [simp]: "(\<Union>x\<in>{}. B x) = {}"
+ by blast
+
+lemma UN_empty2 [simp]: "(\<Union>x\<in>A. {}) = {}"
+ by blast
+
+lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
+ by blast
+
+lemma UN_absorb: "k \<in> I ==> A k \<union> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. A i)"
+ by blast
+
+lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV"
+ by blast
+
+lemma INT_absorb: "k \<in> I ==> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)"
+ by blast
+
+lemma UN_insert [simp]: "(\<Union>x\<in>insert a A. B x) = B a \<union> UNION A B"
+ by blast
+
+lemma UN_Un: "(\<Union>i \<in> A \<union> B. M i) = (\<Union>i\<in>A. M i) \<union> (\<Union>i\<in>B. M i)"
+ by blast
+
+lemma UN_UN_flatten: "(\<Union>x \<in> (\<Union>y\<in>A. B y). C x) = (\<Union>y\<in>A. \<Union>x\<in>B y. C x)"
+ by blast
+
+lemma UN_subset_iff: "((\<Union>i\<in>I. A i) \<subseteq> B) = (\<forall>i\<in>I. A i \<subseteq> B)"
+ by blast
+
+lemma INT_subset_iff: "(B \<subseteq> (\<Inter>i\<in>I. A i)) = (\<forall>i\<in>I. B \<subseteq> A i)"
+ by blast
+
+lemma INT_insert [simp]: "(\<Inter>x \<in> insert a A. B x) = B a \<inter> INTER A B"
+ by blast
+
+lemma INT_Un: "(\<Inter>i \<in> A \<union> B. M i) = (\<Inter>i \<in> A. M i) \<inter> (\<Inter>i\<in>B. M i)"
+ by blast
+
+lemma INT_insert_distrib:
+ "u \<in> A ==> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
+ by blast
+
+lemma Union_image_eq [simp]: "\<Union>(B`A) = (\<Union>x\<in>A. B x)"
+ by blast
+
+lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)"
+ by blast
+
+lemma Inter_image_eq [simp]: "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
+ by blast
+
+lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A = {} then {} else c)"
+ by auto
+
+lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A = {} then UNIV else c)"
+ by auto
+
+lemma UN_eq: "(\<Union>x\<in>A. B x) = \<Union>({Y. \<exists>x\<in>A. Y = B x})"
+ by blast
+
+lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})"
+ -- {* Look: it has an \emph{existential} quantifier *}
+ by blast
+
+lemma UN_empty3 [iff]: "(UNION A B = {}) = (\<forall>x\<in>A. B x = {})"
+ by auto
+
+
+text {* \medskip Distributive laws: *}
+
+lemma Int_Union: "A \<inter> \<Union>B = (\<Union>C\<in>B. A \<inter> C)"
+ by blast
+
+lemma Int_Union2: "\<Union>B \<inter> A = (\<Union>C\<in>B. C \<inter> A)"
+ by blast
+
+lemma Un_Union_image: "(\<Union>x\<in>C. A x \<union> B x) = \<Union>(A`C) \<union> \<Union>(B`C)"
+ -- {* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: *}
+ -- {* Union of a family of unions *}
+ by blast
+
+lemma UN_Un_distrib: "(\<Union>i\<in>I. A i \<union> B i) = (\<Union>i\<in>I. A i) \<union> (\<Union>i\<in>I. B i)"
+ -- {* Equivalent version *}
+ by blast
+
+lemma Un_Inter: "A \<union> \<Inter>B = (\<Inter>C\<in>B. A \<union> C)"
+ by blast
+
+lemma Int_Inter_image: "(\<Inter>x\<in>C. A x \<inter> B x) = \<Inter>(A`C) \<inter> \<Inter>(B`C)"
+ by blast
+
+lemma INT_Int_distrib: "(\<Inter>i\<in>I. A i \<inter> B i) = (\<Inter>i\<in>I. A i) \<inter> (\<Inter>i\<in>I. B i)"
+ -- {* Equivalent version *}
+ by blast
+
+lemma Int_UN_distrib: "B \<inter> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. B \<inter> A i)"
+ -- {* Halmos, Naive Set Theory, page 35. *}
+ by blast
+
+lemma Un_INT_distrib: "B \<union> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. B \<union> A i)"
+ by blast
+
+lemma Int_UN_distrib2: "(\<Union>i\<in>I. A i) \<inter> (\<Union>j\<in>J. B j) = (\<Union>i\<in>I. \<Union>j\<in>J. A i \<inter> B j)"
+ by blast
+
+lemma Un_INT_distrib2: "(\<Inter>i\<in>I. A i) \<union> (\<Inter>j\<in>J. B j) = (\<Inter>i\<in>I. \<Inter>j\<in>J. A i \<union> B j)"
+ by blast
+
+
+text {* \medskip Bounded quantifiers.
+
+ The following are not added to the default simpset because
+ (a) they duplicate the body and (b) there are no similar rules for @{text Int}. *}
+
+lemma ball_Un: "(\<forall>x \<in> A \<union> B. P x) = ((\<forall>x\<in>A. P x) & (\<forall>x\<in>B. P x))"
+ by blast
+
+lemma bex_Un: "(\<exists>x \<in> A \<union> B. P x) = ((\<exists>x\<in>A. P x) | (\<exists>x\<in>B. P x))"
+ by blast
+
+lemma ball_UN: "(\<forall>z \<in> UNION A B. P z) = (\<forall>x\<in>A. \<forall>z \<in> B x. P z)"
+ by blast
+
+lemma bex_UN: "(\<exists>z \<in> UNION A B. P z) = (\<exists>x\<in>A. \<exists>z\<in>B x. P z)"
+ by blast
+
+
+text {* \medskip Set difference. *}
+
+lemma Diff_eq: "A - B = A \<inter> (-B)"
+ by blast
+
+lemma Diff_eq_empty_iff [simp]: "(A - B = {}) = (A \<subseteq> B)"
+ by blast
+
+lemma Diff_cancel [simp]: "A - A = {}"
+ by blast
+
+lemma Diff_triv: "A \<inter> B = {} ==> A - B = A"
+ by (blast elim: equalityE)
+
+lemma empty_Diff [simp]: "{} - A = {}"
+ by blast
+
+lemma Diff_empty [simp]: "A - {} = A"
+ by blast
+
+lemma Diff_UNIV [simp]: "A - UNIV = {}"
+ by blast
+
+lemma Diff_insert0 [simp]: "x \<notin> A ==> A - insert x B = A - B"
+ by blast
+
+lemma Diff_insert: "A - insert a B = A - B - {a}"
+ -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"} *}
+ by blast
+
+lemma Diff_insert2: "A - insert a B = A - {a} - B"
+ -- {* NOT SUITABLE FOR REWRITING since @{text "{a} == insert a 0"} *}
+ by blast
+
+lemma insert_Diff_if: "insert x A - B = (if x \<in> B then A - B else insert x (A - B))"
+ by auto
+
+lemma insert_Diff1 [simp]: "x \<in> B ==> insert x A - B = A - B"
+ by blast
+
+lemma insert_Diff: "a \<in> A ==> insert a (A - {a}) = A"
+ by blast
+
+lemma Diff_insert_absorb: "x \<notin> A ==> (insert x A) - {x} = A"
+ by auto
+
+lemma Diff_disjoint [simp]: "A \<inter> (B - A) = {}"
+ by blast
+
+lemma Diff_partition: "A \<subseteq> B ==> A \<union> (B - A) = B"
+ by blast
+
+lemma double_diff: "A \<subseteq> B ==> B \<subseteq> C ==> B - (C - A) = A"
+ by blast
+
+lemma Un_Diff_cancel [simp]: "A \<union> (B - A) = A \<union> B"
+ by blast
+
+lemma Un_Diff_cancel2 [simp]: "(B - A) \<union> A = B \<union> A"
+ by blast
+
+lemma Diff_Un: "A - (B \<union> C) = (A - B) \<inter> (A - C)"
+ by blast
+
+lemma Diff_Int: "A - (B \<inter> C) = (A - B) \<union> (A - C)"
+ by blast
+
+lemma Un_Diff: "(A \<union> B) - C = (A - C) \<union> (B - C)"
+ by blast
+
+lemma Int_Diff: "(A \<inter> B) - C = A \<inter> (B - C)"
+ by blast
+
+lemma Diff_Int_distrib: "C \<inter> (A - B) = (C \<inter> A) - (C \<inter> B)"
+ by blast
+
+lemma Diff_Int_distrib2: "(A - B) \<inter> C = (A \<inter> C) - (B \<inter> C)"
+ by blast
+
+lemma Diff_Compl [simp]: "A - (- B) = A \<inter> B"
+ by auto
+
+lemma Compl_Diff_eq [simp]: "- (A - B) = -A \<union> B"
+ by blast
+
+
+text {* \medskip Quantification over type @{typ bool}. *}
+
+lemma all_bool_eq: "(\<forall>b::bool. P b) = (P True & P False)"
+ apply auto
+ apply (tactic {* case_tac "b" 1 *})
+ apply auto
+ done
+
+lemma bool_induct: "P True \<Longrightarrow> P False \<Longrightarrow> P x"
+ by (rule conjI [THEN all_bool_eq [THEN iffD2], THEN spec])
+
+lemma ex_bool_eq: "(\<exists>b::bool. P b) = (P True | P False)"
+ apply auto
+ apply (tactic {* case_tac "b" 1 *})
+ apply auto
+ done
+
+lemma Un_eq_UN: "A \<union> B = (\<Union>b. if b then A else B)"
+ by (auto simp add: split_if_mem2)
+
+lemma UN_bool_eq: "(\<Union>b::bool. A b) = (A True \<union> A False)"
+ apply auto
+ apply (tactic {* case_tac "b" 1 *})
+ apply auto
+ done
+
+lemma INT_bool_eq: "(\<Inter>b::bool. A b) = (A True \<inter> A False)"
+ apply auto
+ apply (tactic {* case_tac "b" 1 *})
+ apply auto
+ done
+
+
+text {* \medskip @{text Pow} *}
+
+lemma Pow_empty [simp]: "Pow {} = {{}}"
+ by (auto simp add: Pow_def)
+
+lemma Pow_insert: "Pow (insert a A) = Pow A \<union> (insert a ` Pow A)"
+ by (blast intro: image_eqI [where ?x = "u - {a}", standard])
+
+lemma Pow_Compl: "Pow (- A) = {-B | B. A \<in> Pow B}"
+ by (blast intro: exI [where ?x = "- u", standard])
+
+lemma Pow_UNIV [simp]: "Pow UNIV = UNIV"
+ by blast
+
+lemma Un_Pow_subset: "Pow A \<union> Pow B \<subseteq> Pow (A \<union> B)"
+ by blast
+
+lemma UN_Pow_subset: "(\<Union>x\<in>A. Pow (B x)) \<subseteq> Pow (\<Union>x\<in>A. B x)"
+ by blast
+
+lemma subset_Pow_Union: "A \<subseteq> Pow (\<Union>A)"
+ by blast
+
+lemma Union_Pow_eq [simp]: "\<Union>(Pow A) = A"
+ by blast
+
+lemma Pow_Int_eq [simp]: "Pow (A \<inter> B) = Pow A \<inter> Pow B"
+ by blast
+
+lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))"
+ by blast
+
+
+text {* \medskip Miscellany. *}
+
+lemma set_eq_subset: "(A = B) = (A \<subseteq> B & B \<subseteq> A)"
+ by blast
+
+lemma subset_iff: "(A \<subseteq> B) = (\<forall>t. t \<in> A --> t \<in> B)"
+ by blast
+
+lemma subset_iff_psubset_eq: "(A \<subseteq> B) = ((A \<subset> B) | (A = B))"
+ by (unfold psubset_def) blast
+
+lemma all_not_in_conv [iff]: "(\<forall>x. x \<notin> A) = (A = {})"
+ by blast
+
+lemma distinct_lemma: "f x \<noteq> f y ==> x \<noteq> y"
+ by rules
+
+
+text {* \medskip Miniscoping: pushing in big Unions and Intersections. *}
+
+lemma UN_simps [simp]:
+ "!!a B C. (UN x:C. insert a (B x)) = (if C={} then {} else insert a (UN x:C. B x))"
+ "!!A B C. (UN x:C. A x Un B) = ((if C={} then {} else (UN x:C. A x) Un B))"
+ "!!A B C. (UN x:C. A Un B x) = ((if C={} then {} else A Un (UN x:C. B x)))"
+ "!!A B C. (UN x:C. A x Int B) = ((UN x:C. A x) Int B)"
+ "!!A B C. (UN x:C. A Int B x) = (A Int (UN x:C. B x))"
+ "!!A B C. (UN x:C. A x - B) = ((UN x:C. A x) - B)"
+ "!!A B C. (UN x:C. A - B x) = (A - (INT x:C. B x))"
+ "!!A B. (UN x: Union A. B x) = (UN y:A. UN x:y. B x)"
+ "!!A B C. (UN z: UNION A B. C z) = (UN x:A. UN z: B(x). C z)"
+ "!!A B f. (UN x:f`A. B x) = (UN a:A. B (f a))"
+ by auto
+
+lemma INT_simps [simp]:
+ "!!A B C. (INT x:C. A x Int B) = (if C={} then UNIV else (INT x:C. A x) Int B)"
+ "!!A B C. (INT x:C. A Int B x) = (if C={} then UNIV else A Int (INT x:C. B x))"
+ "!!A B C. (INT x:C. A x - B) = (if C={} then UNIV else (INT x:C. A x) - B)"
+ "!!A B C. (INT x:C. A - B x) = (if C={} then UNIV else A - (UN x:C. B x))"
+ "!!a B C. (INT x:C. insert a (B x)) = insert a (INT x:C. B x)"
+ "!!A B C. (INT x:C. A x Un B) = ((INT x:C. A x) Un B)"
+ "!!A B C. (INT x:C. A Un B x) = (A Un (INT x:C. B x))"
+ "!!A B. (INT x: Union A. B x) = (INT y:A. INT x:y. B x)"
+ "!!A B C. (INT z: UNION A B. C z) = (INT x:A. INT z: B(x). C z)"
+ "!!A B f. (INT x:f`A. B x) = (INT a:A. B (f a))"
+ by auto
+
+lemma ball_simps [simp]:
+ "!!A P Q. (ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)"
+ "!!A P Q. (ALL x:A. P | Q x) = (P | (ALL x:A. Q x))"
+ "!!A P Q. (ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))"
+ "!!A P Q. (ALL x:A. P x --> Q) = ((EX x:A. P x) --> Q)"
+ "!!P. (ALL x:{}. P x) = True"
+ "!!P. (ALL x:UNIV. P x) = (ALL x. P x)"
+ "!!a B P. (ALL x:insert a B. P x) = (P a & (ALL x:B. P x))"
+ "!!A P. (ALL x:Union A. P x) = (ALL y:A. ALL x:y. P x)"
+ "!!A B P. (ALL x: UNION A B. P x) = (ALL a:A. ALL x: B a. P x)"
+ "!!P Q. (ALL x:Collect Q. P x) = (ALL x. Q x --> P x)"
+ "!!A P f. (ALL x:f`A. P x) = (ALL x:A. P (f x))"
+ "!!A P. (~(ALL x:A. P x)) = (EX x:A. ~P x)"
+ by auto
+
+lemma bex_simps [simp]:
+ "!!A P Q. (EX x:A. P x & Q) = ((EX x:A. P x) & Q)"
+ "!!A P Q. (EX x:A. P & Q x) = (P & (EX x:A. Q x))"
+ "!!P. (EX x:{}. P x) = False"
+ "!!P. (EX x:UNIV. P x) = (EX x. P x)"
+ "!!a B P. (EX x:insert a B. P x) = (P(a) | (EX x:B. P x))"
+ "!!A P. (EX x:Union A. P x) = (EX y:A. EX x:y. P x)"
+ "!!A B P. (EX x: UNION A B. P x) = (EX a:A. EX x:B a. P x)"
+ "!!P Q. (EX x:Collect Q. P x) = (EX x. Q x & P x)"
+ "!!A P f. (EX x:f`A. P x) = (EX x:A. P (f x))"
+ "!!A P. (~(EX x:A. P x)) = (ALL x:A. ~P x)"
+ by auto
+
+lemma ball_conj_distrib:
+ "(ALL x:A. P x & Q x) = ((ALL x:A. P x) & (ALL x:A. Q x))"
+ by blast
+
+lemma bex_disj_distrib:
+ "(EX x:A. P x | Q x) = ((EX x:A. P x) | (EX x:A. Q x))"
+ by blast
+
+
+subsubsection {* Monotonicity of various operations *}
+
+lemma image_mono: "A \<subseteq> B ==> f`A \<subseteq> f`B"
+ by blast
+
+lemma Pow_mono: "A \<subseteq> B ==> Pow A \<subseteq> Pow B"
+ by blast
+
+lemma Union_mono: "A \<subseteq> B ==> \<Union>A \<subseteq> \<Union>B"
+ by blast
+
+lemma Inter_anti_mono: "B \<subseteq> A ==> \<Inter>A \<subseteq> \<Inter>B"
+ by blast
+
+lemma UN_mono:
+ "A \<subseteq> B ==> (!!x. x \<in> A ==> f x \<subseteq> g x) ==>
+ (\<Union>x\<in>A. f x) \<subseteq> (\<Union>x\<in>B. g x)"
+ by (blast dest: subsetD)
+
+lemma INT_anti_mono:
+ "B \<subseteq> A ==> (!!x. x \<in> A ==> f x \<subseteq> g x) ==>
+ (\<Inter>x\<in>A. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
+ -- {* The last inclusion is POSITIVE! *}
+ by (blast dest: subsetD)
+
+lemma insert_mono: "C \<subseteq> D ==> insert a C \<subseteq> insert a D"
+ by blast
+
+lemma Un_mono: "A \<subseteq> C ==> B \<subseteq> D ==> A \<union> B \<subseteq> C \<union> D"
+ by blast
+
+lemma Int_mono: "A \<subseteq> C ==> B \<subseteq> D ==> A \<inter> B \<subseteq> C \<inter> D"
+ by blast
+
+lemma Diff_mono: "A \<subseteq> C ==> D \<subseteq> B ==> A - B \<subseteq> C - D"
+ by blast
+
+lemma Compl_anti_mono: "A \<subseteq> B ==> -B \<subseteq> -A"
+ by blast
+
+text {* \medskip Monotonicity of implications. *}
+
+lemma in_mono: "A \<subseteq> B ==> x \<in> A --> x \<in> B"
+ apply (rule impI)
+ apply (erule subsetD)
+ apply assumption
+ done
+
+lemma conj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 & P2) --> (Q1 & Q2)"
+ by rules
+
+lemma disj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 | P2) --> (Q1 | Q2)"
+ by rules
+
+lemma imp_mono: "Q1 --> P1 ==> P2 --> Q2 ==> (P1 --> P2) --> (Q1 --> Q2)"
+ by rules
+
+lemma imp_refl: "P --> P" ..
+
+lemma ex_mono: "(!!x. P x --> Q x) ==> (EX x. P x) --> (EX x. Q x)"
+ by rules
+
+lemma all_mono: "(!!x. P x --> Q x) ==> (ALL x. P x) --> (ALL x. Q x)"
+ by rules
+
+lemma Collect_mono: "(!!x. P x --> Q x) ==> Collect P \<subseteq> Collect Q"
+ by blast
+
+lemma Int_Collect_mono:
+ "A \<subseteq> B ==> (!!x. x \<in> A ==> P x --> Q x) ==> A \<inter> Collect P \<subseteq> B \<inter> Collect Q"
+ by blast
+
+lemmas basic_monos =
+ subset_refl imp_refl disj_mono conj_mono
+ ex_mono Collect_mono in_mono
+
+lemma eq_to_mono: "a = b ==> c = d ==> b --> d ==> a --> c"
+ by rules
+
+lemma eq_to_mono2: "a = b ==> c = d ==> ~ b --> ~ d ==> ~ a --> ~ c"
+ by rules
lemma Least_mono:
"mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
@@ -972,7 +1858,7 @@
-- {* NOT suitable for rewriting *}
by blast
-lemma vimage_mono: "A <= B ==> f -` A <= f -` B"
+lemma vimage_mono: "A \<subseteq> B ==> f -` A \<subseteq> f -` B"
-- {* monotonicity *}
by blast
@@ -985,10 +1871,10 @@
lemma back_subst: "P a ==> a = b ==> P b"
by (rule subst)
-lemma set_rev_mp: "x:A ==> A <= B ==> x:B"
+lemma set_rev_mp: "x:A ==> A \<subseteq> B ==> x:B"
by (rule subsetD)
-lemma set_mp: "A <= B ==> x:A ==> x:B"
+lemma set_mp: "A \<subseteq> B ==> x:A ==> x:B"
by (rule subsetD)
lemma order_neq_le_trans: "a ~= b ==> (a::'a::order) <= b ==> a < b"
--- a/src/HOL/equalities.ML Fri Feb 15 20:43:44 2002 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,982 +0,0 @@
-(* Title: HOL/equalities.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Equalities involving union, intersection, inclusion, etc.
-*)
-
-AddSIs [equalityI];
-
-section "{}";
-
-(*supersedes Collect_False_empty*)
-Goal "{s. P} = (if P then UNIV else {})";
-by (Force_tac 1);
-qed "Collect_const";
-Addsimps [Collect_const];
-
-Goal "(A <= {}) = (A = {})";
-by (Blast_tac 1);
-qed "subset_empty";
-Addsimps[subset_empty];
-
-Goalw [psubset_def] "~ (A < {})";
-by (Blast_tac 1);
-qed "not_psubset_empty";
-AddIffs [not_psubset_empty];
-
-Goal "(Collect P = {}) = (ALL x. ~ P x)";
-by Auto_tac;
-qed "Collect_empty_eq";
-Addsimps[Collect_empty_eq];
-
-Goal "{x. ~ (P x)} = - {x. P x}";
-by (Blast_tac 1);
-qed "Collect_neg_eq";
-
-Goal "{x. P x | Q x} = {x. P x} Un {x. Q x}";
-by (Blast_tac 1);
-qed "Collect_disj_eq";
-
-Goal "{x. P x & Q x} = {x. P x} Int {x. Q x}";
-by (Blast_tac 1);
-qed "Collect_conj_eq";
-
-Goal "{x. ALL y. P x y} = (INT y. {x. P x y})";
-by (Blast_tac 1);
-qed "Collect_all_eq";
-
-Goal "{x. ALL y: A. P x y} = (INT y: A. {x. P x y})";
-by (Blast_tac 1);
-qed "Collect_ball_eq";
-
-Goal "{x. EX y. P x y} = (UN y. {x. P x y})";
-by (Blast_tac 1);
-qed "Collect_ex_eq";
-
-Goal "{x. EX y: A. P x y} = (UN y: A. {x. P x y})";
-by (Blast_tac 1);
-qed "Collect_bex_eq";
-
-
-section "insert";
-
-(*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)
-Goal "insert a A = {a} Un A";
-by (Blast_tac 1);
-qed "insert_is_Un";
-
-Goal "insert a A ~= {}";
-by (Blast_tac 1);
-qed"insert_not_empty";
-Addsimps[insert_not_empty];
-
-bind_thm("empty_not_insert",insert_not_empty RS not_sym);
-Addsimps[empty_not_insert];
-
-Goal "a:A ==> insert a A = A";
-by (Blast_tac 1);
-qed "insert_absorb";
-(* Addsimps [insert_absorb] causes recursive calls
- when there are nested inserts, with QUADRATIC running time
-*)
-
-Goal "insert x (insert x A) = insert x A";
-by (Blast_tac 1);
-qed "insert_absorb2";
-Addsimps [insert_absorb2];
-
-Goal "insert x (insert y A) = insert y (insert x A)";
-by (Blast_tac 1);
-qed "insert_commute";
-
-Goal "(insert x A <= B) = (x:B & A <= B)";
-by (Blast_tac 1);
-qed "insert_subset";
-Addsimps[insert_subset];
-
-(* use new B rather than (A-{a}) to avoid infinite unfolding *)
-Goal "a:A ==> EX B. A = insert a B & a ~: B";
-by (res_inst_tac [("x","A-{a}")] exI 1);
-by (Blast_tac 1);
-qed "mk_disjoint_insert";
-
-Goal "insert a (Collect P) = {u. u ~= a --> P u}";
-by Auto_tac;
-qed "insert_Collect";
-
-Goal "u: A ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
-by (Blast_tac 1);
-qed "UN_insert_distrib";
-
-section "`";
-
-Goal "f`{} = {}";
-by (Blast_tac 1);
-qed "image_empty";
-Addsimps[image_empty];
-
-Goal "f`insert a B = insert (f a) (f`B)";
-by (Blast_tac 1);
-qed "image_insert";
-Addsimps[image_insert];
-
-Goal "x:A ==> (%x. c) ` A = {c}";
-by (Blast_tac 1);
-qed "image_constant";
-
-Goal "f`(g`A) = (%x. f (g x)) ` A";
-by (Blast_tac 1);
-qed "image_image";
-
-Goal "x:A ==> insert (f x) (f`A) = f`A";
-by (Blast_tac 1);
-qed "insert_image";
-Addsimps [insert_image];
-
-Goal "(f`A = {}) = (A = {})";
-by (Blast_tac 1);
-qed "image_is_empty";
-AddIffs [image_is_empty];
-
-(*NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
- with its implicit quantifier and conjunction. Also image enjoys better
- equational properties than does the RHS.*)
-Goal "f ` {x. P x} = {f x | x. P x}";
-by (Blast_tac 1);
-qed "image_Collect";
-
-Goalw [image_def] "(%x. if P x then f x else g x) ` S \
-\ = (f ` (S Int {x. P x})) Un (g ` (S Int {x. ~(P x)}))";
-by (Simp_tac 1);
-by (Blast_tac 1);
-qed "if_image_distrib";
-Addsimps[if_image_distrib];
-
-val prems = Goal "[|M = N; !!x. x:N ==> f x = g x|] ==> f`M = g`N";
-by (simp_tac (simpset() addsimps image_def::prems) 1);
-qed "image_cong";
-
-
-section "range";
-
-Goal "{u. EX x. u = f x} = range f";
-by Auto_tac;
-qed "full_SetCompr_eq";
-
-Goal "range (%x. f (g x)) = f`range g";
-by (stac image_image 1);
-by (Simp_tac 1);
-qed "range_composition";
-Addsimps[range_composition];
-
-section "Int";
-
-Goal "A Int A = A";
-by (Blast_tac 1);
-qed "Int_absorb";
-Addsimps[Int_absorb];
-
-Goal "A Int (A Int B) = A Int B";
-by (Blast_tac 1);
-qed "Int_left_absorb";
-
-Goal "A Int B = B Int A";
-by (Blast_tac 1);
-qed "Int_commute";
-
-Goal "A Int (B Int C) = B Int (A Int C)";
-by (Blast_tac 1);
-qed "Int_left_commute";
-
-Goal "(A Int B) Int C = A Int (B Int C)";
-by (Blast_tac 1);
-qed "Int_assoc";
-
-(*Intersection is an AC-operator*)
-bind_thms ("Int_ac", [Int_assoc, Int_left_absorb, Int_commute, Int_left_commute]);
-
-Goal "B<=A ==> A Int B = B";
-by (Blast_tac 1);
-qed "Int_absorb1";
-
-Goal "A<=B ==> A Int B = A";
-by (Blast_tac 1);
-qed "Int_absorb2";
-
-Goal "{} Int B = {}";
-by (Blast_tac 1);
-qed "Int_empty_left";
-Addsimps[Int_empty_left];
-
-Goal "A Int {} = {}";
-by (Blast_tac 1);
-qed "Int_empty_right";
-Addsimps[Int_empty_right];
-
-Goal "(A Int B = {}) = (A <= -B)";
-by (Blast_tac 1);
-qed "disjoint_eq_subset_Compl";
-
-Goal "(A Int B = {}) = (ALL x:A. ALL y:B. x ~= y)";
-by (Blast_tac 1);
-qed "disjoint_iff_not_equal";
-
-Goal "UNIV Int B = B";
-by (Blast_tac 1);
-qed "Int_UNIV_left";
-Addsimps[Int_UNIV_left];
-
-Goal "A Int UNIV = A";
-by (Blast_tac 1);
-qed "Int_UNIV_right";
-Addsimps[Int_UNIV_right];
-
-Goal "A Int B = Inter{A,B}";
-by (Blast_tac 1);
-qed "Int_eq_Inter";
-
-Goal "A Int (B Un C) = (A Int B) Un (A Int C)";
-by (Blast_tac 1);
-qed "Int_Un_distrib";
-
-Goal "(B Un C) Int A = (B Int A) Un (C Int A)";
-by (Blast_tac 1);
-qed "Int_Un_distrib2";
-
-Goal "(A Int B = UNIV) = (A = UNIV & B = UNIV)";
-by (Blast_tac 1);
-qed "Int_UNIV";
-Addsimps[Int_UNIV];
-
-Goal "(C <= A Int B) = (C <= A & C <= B)";
-by (Blast_tac 1);
-qed "Int_subset_iff";
-
-Goal "(x : A Int {x. P x}) = (x : A & P x)";
-by (Blast_tac 1);
-qed "Int_Collect";
-
-section "Un";
-
-Goal "A Un A = A";
-by (Blast_tac 1);
-qed "Un_absorb";
-Addsimps[Un_absorb];
-
-Goal "A Un (A Un B) = A Un B";
-by (Blast_tac 1);
-qed "Un_left_absorb";
-
-Goal "A Un B = B Un A";
-by (Blast_tac 1);
-qed "Un_commute";
-
-Goal "A Un (B Un C) = B Un (A Un C)";
-by (Blast_tac 1);
-qed "Un_left_commute";
-
-Goal "(A Un B) Un C = A Un (B Un C)";
-by (Blast_tac 1);
-qed "Un_assoc";
-
-(*Union is an AC-operator*)
-bind_thms ("Un_ac", [Un_assoc, Un_left_absorb, Un_commute, Un_left_commute]);
-
-Goal "A<=B ==> A Un B = B";
-by (Blast_tac 1);
-qed "Un_absorb1";
-
-Goal "B<=A ==> A Un B = A";
-by (Blast_tac 1);
-qed "Un_absorb2";
-
-Goal "{} Un B = B";
-by (Blast_tac 1);
-qed "Un_empty_left";
-Addsimps[Un_empty_left];
-
-Goal "A Un {} = A";
-by (Blast_tac 1);
-qed "Un_empty_right";
-Addsimps[Un_empty_right];
-
-Goal "UNIV Un B = UNIV";
-by (Blast_tac 1);
-qed "Un_UNIV_left";
-Addsimps[Un_UNIV_left];
-
-Goal "A Un UNIV = UNIV";
-by (Blast_tac 1);
-qed "Un_UNIV_right";
-Addsimps[Un_UNIV_right];
-
-Goal "A Un B = Union{A,B}";
-by (Blast_tac 1);
-qed "Un_eq_Union";
-
-Goal "(insert a B) Un C = insert a (B Un C)";
-by (Blast_tac 1);
-qed "Un_insert_left";
-Addsimps[Un_insert_left];
-
-Goal "A Un (insert a B) = insert a (A Un B)";
-by (Blast_tac 1);
-qed "Un_insert_right";
-Addsimps[Un_insert_right];
-
-Goal "(insert a B) Int C = (if a:C then insert a (B Int C) \
-\ else B Int C)";
-by (Simp_tac 1);
-by (Blast_tac 1);
-qed "Int_insert_left";
-
-Goal "A Int (insert a B) = (if a:A then insert a (A Int B) \
-\ else A Int B)";
-by (Simp_tac 1);
-by (Blast_tac 1);
-qed "Int_insert_right";
-
-Goal "A Un (B Int C) = (A Un B) Int (A Un C)";
-by (Blast_tac 1);
-qed "Un_Int_distrib";
-
-Goal "(B Int C) Un A = (B Un A) Int (C Un A)";
-by (Blast_tac 1);
-qed "Un_Int_distrib2";
-
-Goal "(A Int B) Un (B Int C) Un (C Int A) = \
-\ (A Un B) Int (B Un C) Int (C Un A)";
-by (Blast_tac 1);
-qed "Un_Int_crazy";
-
-Goal "(A<=B) = (A Un B = B)";
-by (Blast_tac 1);
-qed "subset_Un_eq";
-
-Goal "(A Un B = {}) = (A = {} & B = {})";
-by (Blast_tac 1);
-qed "Un_empty";
-AddIffs[Un_empty];
-
-Goal "(A Un B <= C) = (A <= C & B <= C)";
-by (Blast_tac 1);
-qed "Un_subset_iff";
-
-Goal "(A - B) Un (A Int B) = A";
-by (Blast_tac 1);
-qed "Un_Diff_Int";
-
-
-section "Set complement";
-
-Goal "A Int -A = {}";
-by (Blast_tac 1);
-qed "Compl_disjoint";
-
-Goal "-A Int A = {}";
-by (Blast_tac 1);
-qed "Compl_disjoint2";
-Addsimps[Compl_disjoint, Compl_disjoint2];
-
-Goal "A Un (-A) = UNIV";
-by (Blast_tac 1);
-qed "Compl_partition";
-
-Goal "- (-A) = (A:: 'a set)";
-by (Blast_tac 1);
-qed "double_complement";
-Addsimps[double_complement];
-
-Goal "-(A Un B) = (-A) Int (-B)";
-by (Blast_tac 1);
-qed "Compl_Un";
-
-Goal "-(A Int B) = (-A) Un (-B)";
-by (Blast_tac 1);
-qed "Compl_Int";
-
-Goal "-(UN x:A. B(x)) = (INT x:A. -B(x))";
-by (Blast_tac 1);
-qed "Compl_UN";
-
-Goal "-(INT x:A. B(x)) = (UN x:A. -B(x))";
-by (Blast_tac 1);
-qed "Compl_INT";
-
-Addsimps [Compl_Un, Compl_Int, Compl_UN, Compl_INT];
-
-Goal "(A <= -A) = (A = {})";
-by (Blast_tac 1);
-qed "subset_Compl_self_eq";
-
-(*Halmos, Naive Set Theory, page 16.*)
-Goal "((A Int B) Un C = A Int (B Un C)) = (C<=A)";
-by (Blast_tac 1);
-qed "Un_Int_assoc_eq";
-
-Goal "-UNIV = {}";
-by (Blast_tac 1);
-qed "Compl_UNIV_eq";
-
-Goal "-{} = UNIV";
-by (Blast_tac 1);
-qed "Compl_empty_eq";
-
-Addsimps [Compl_UNIV_eq, Compl_empty_eq];
-
-Goal "(-A <= -B) = (B <= (A::'a set))";
-by (Blast_tac 1);
-qed "Compl_subset_Compl_iff";
-AddIffs [Compl_subset_Compl_iff];
-
-Goal "(-A = -B) = (A = (B::'a set))";
-by (Blast_tac 1);
-qed "Compl_eq_Compl_iff";
-AddIffs [Compl_eq_Compl_iff];
-
-
-section "Union";
-
-Goal "Union({}) = {}";
-by (Blast_tac 1);
-qed "Union_empty";
-Addsimps[Union_empty];
-
-Goal "Union(UNIV) = UNIV";
-by (Blast_tac 1);
-qed "Union_UNIV";
-Addsimps[Union_UNIV];
-
-Goal "Union(insert a B) = a Un Union(B)";
-by (Blast_tac 1);
-qed "Union_insert";
-Addsimps[Union_insert];
-
-Goal "Union(A Un B) = Union(A) Un Union(B)";
-by (Blast_tac 1);
-qed "Union_Un_distrib";
-Addsimps[Union_Un_distrib];
-
-Goal "Union(A Int B) <= Union(A) Int Union(B)";
-by (Blast_tac 1);
-qed "Union_Int_subset";
-
-Goal "(Union A = {}) = (ALL x:A. x={})";
-by Auto_tac;
-qed "Union_empty_conv";
-AddIffs [Union_empty_conv];
-
-Goal "(Union(C) Int A = {}) = (ALL B:C. B Int A = {})";
-by (Blast_tac 1);
-qed "Union_disjoint";
-
-section "Inter";
-
-Goal "Inter({}) = UNIV";
-by (Blast_tac 1);
-qed "Inter_empty";
-Addsimps[Inter_empty];
-
-Goal "Inter(UNIV) = {}";
-by (Blast_tac 1);
-qed "Inter_UNIV";
-Addsimps[Inter_UNIV];
-
-Goal "Inter(insert a B) = a Int Inter(B)";
-by (Blast_tac 1);
-qed "Inter_insert";
-Addsimps[Inter_insert];
-
-Goal "Inter(A) Un Inter(B) <= Inter(A Int B)";
-by (Blast_tac 1);
-qed "Inter_Un_subset";
-
-Goal "Inter(A Un B) = Inter(A) Int Inter(B)";
-by (Blast_tac 1);
-qed "Inter_Un_distrib";
-
-section "UN and INT";
-
-(*Basic identities*)
-
-Goal "(UN x:{}. B x) = {}";
-by (Blast_tac 1);
-qed "UN_empty";
-Addsimps[UN_empty];
-
-Goal "(UN x:A. {}) = {}";
-by (Blast_tac 1);
-qed "UN_empty2";
-Addsimps[UN_empty2];
-
-Goal "(UN x:A. {x}) = A";
-by (Blast_tac 1);
-qed "UN_singleton";
-Addsimps [UN_singleton];
-
-Goal "k:I ==> A k Un (UN i:I. A i) = (UN i:I. A i)";
-by (Blast_tac 1);
-qed "UN_absorb";
-
-Goal "(INT x:{}. B x) = UNIV";
-by (Blast_tac 1);
-qed "INT_empty";
-Addsimps[INT_empty];
-
-Goal "k:I ==> A k Int (INT i:I. A i) = (INT i:I. A i)";
-by (Blast_tac 1);
-qed "INT_absorb";
-
-Goal "(UN x:insert a A. B x) = B a Un UNION A B";
-by (Blast_tac 1);
-qed "UN_insert";
-Addsimps[UN_insert];
-
-Goal "(UN i: A Un B. M i) = (UN i: A. M i) Un (UN i:B. M i)";
-by (Blast_tac 1);
-qed "UN_Un";
-
-Goal "(UN x : (UN y:A. B y). C x) = (UN y:A. UN x: B y. C x)";
-by (Blast_tac 1);
-qed "UN_UN_flatten";
-
-Goal "((UN i:I. A i) <= B) = (ALL i:I. A i <= B)";
-by (Blast_tac 1);
-qed "UN_subset_iff";
-
-Goal "(B <= (INT i:I. A i)) = (ALL i:I. B <= A i)";
-by (Blast_tac 1);
-qed "INT_subset_iff";
-
-Goal "(INT x:insert a A. B x) = B a Int INTER A B";
-by (Blast_tac 1);
-qed "INT_insert";
-Addsimps[INT_insert];
-
-Goal "(INT i: A Un B. M i) = (INT i: A. M i) Int (INT i:B. M i)";
-by (Blast_tac 1);
-qed "INT_Un";
-
-Goal "u: A ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)";
-by (Blast_tac 1);
-qed "INT_insert_distrib";
-
-Goal "Union(B`A) = (UN x:A. B(x))";
-by (Blast_tac 1);
-qed "Union_image_eq";
-Addsimps [Union_image_eq];
-
-Goal "f ` Union S = (UN x:S. f ` x)";
-by (Blast_tac 1);
-qed "image_Union";
-
-Goal "Inter(B`A) = (INT x:A. B(x))";
-by (Blast_tac 1);
-qed "Inter_image_eq";
-Addsimps [Inter_image_eq];
-
-Goal "(UN y:A. c) = (if A={} then {} else c)";
-by Auto_tac;
-qed "UN_constant";
-Addsimps[UN_constant];
-
-Goal "(INT y:A. c) = (if A={} then UNIV else c)";
-by Auto_tac;
-qed "INT_constant";
-Addsimps[INT_constant];
-
-Goal "(UN x:A. B(x)) = Union({Y. EX x:A. Y=B(x)})";
-by (Blast_tac 1);
-qed "UN_eq";
-
-(*Look: it has an EXISTENTIAL quantifier*)
-Goal "(INT x:A. B(x)) = Inter({Y. EX x:A. Y=B(x)})";
-by (Blast_tac 1);
-qed "INT_eq";
-
-Goal "(UNION A B = {}) = (ALL x:A. B x = {})";
-by Auto_tac;
-qed "UN_empty3";
-AddIffs [UN_empty3];
-
-
-(*Distributive laws...*)
-
-Goal "A Int Union(B) = (UN C:B. A Int C)";
-by (Blast_tac 1);
-qed "Int_Union";
-
-Goal "Union(B) Int A = (UN C:B. C Int A)";
-by (Blast_tac 1);
-qed "Int_Union2";
-
-(* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5:
- Union of a family of unions **)
-Goal "(UN x:C. A(x) Un B(x)) = Union(A`C) Un Union(B`C)";
-by (Blast_tac 1);
-qed "Un_Union_image";
-
-(*Equivalent version*)
-Goal "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i)) Un (UN i:I. B(i))";
-by (Blast_tac 1);
-qed "UN_Un_distrib";
-
-Goal "A Un Inter(B) = (INT C:B. A Un C)";
-by (Blast_tac 1);
-qed "Un_Inter";
-
-Goal "(INT x:C. A(x) Int B(x)) = Inter(A`C) Int Inter(B`C)";
-by (Blast_tac 1);
-qed "Int_Inter_image";
-
-(*Equivalent version*)
-Goal "(INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
-by (Blast_tac 1);
-qed "INT_Int_distrib";
-
-(*Halmos, Naive Set Theory, page 35.*)
-Goal "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
-by (Blast_tac 1);
-qed "Int_UN_distrib";
-
-Goal "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
-by (Blast_tac 1);
-qed "Un_INT_distrib";
-
-Goal "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
-by (Blast_tac 1);
-qed "Int_UN_distrib2";
-
-Goal "(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
-by (Blast_tac 1);
-qed "Un_INT_distrib2";
-
-
-section"Bounded quantifiers";
-
-(** The following are not added to the default simpset because
- (a) they duplicate the body and (b) there are no similar rules for Int. **)
-
-Goal "(ALL x:A Un B. P x) = ((ALL x:A. P x) & (ALL x:B. P x))";
-by (Blast_tac 1);
-qed "ball_Un";
-
-Goal "(EX x:A Un B. P x) = ((EX x:A. P x) | (EX x:B. P x))";
-by (Blast_tac 1);
-qed "bex_Un";
-
-Goal "(ALL z: UNION A B. P z) = (ALL x:A. ALL z:B x. P z)";
-by (Blast_tac 1);
-qed "ball_UN";
-
-Goal "(EX z: UNION A B. P z) = (EX x:A. EX z:B x. P z)";
-by (Blast_tac 1);
-qed "bex_UN";
-
-
-section "-";
-
-Goal "A-B = A Int (-B)";
-by (Blast_tac 1);
-qed "Diff_eq";
-
-Goal "(A-B = {}) = (A<=B)";
-by (Blast_tac 1);
-qed "Diff_eq_empty_iff";
-Addsimps[Diff_eq_empty_iff];
-
-Goal "A-A = {}";
-by (Blast_tac 1);
-qed "Diff_cancel";
-Addsimps[Diff_cancel];
-
-Goal "A Int B = {} ==> A-B = A";
-by (blast_tac (claset() addEs [equalityE]) 1);
-qed "Diff_triv";
-
-Goal "{}-A = {}";
-by (Blast_tac 1);
-qed "empty_Diff";
-Addsimps[empty_Diff];
-
-Goal "A-{} = A";
-by (Blast_tac 1);
-qed "Diff_empty";
-Addsimps[Diff_empty];
-
-Goal "A-UNIV = {}";
-by (Blast_tac 1);
-qed "Diff_UNIV";
-Addsimps[Diff_UNIV];
-
-Goal "x~:A ==> A - insert x B = A-B";
-by (Blast_tac 1);
-qed "Diff_insert0";
-Addsimps [Diff_insert0];
-
-(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
-Goal "A - insert a B = A - B - {a}";
-by (Blast_tac 1);
-qed "Diff_insert";
-
-(*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
-Goal "A - insert a B = A - {a} - B";
-by (Blast_tac 1);
-qed "Diff_insert2";
-
-Goal "insert x A - B = (if x:B then A-B else insert x (A-B))";
-by (Simp_tac 1);
-by (Blast_tac 1);
-qed "insert_Diff_if";
-
-Goal "x:B ==> insert x A - B = A-B";
-by (Blast_tac 1);
-qed "insert_Diff1";
-Addsimps [insert_Diff1];
-
-Goal "a:A ==> insert a (A-{a}) = A";
-by (Blast_tac 1);
-qed "insert_Diff";
-
-Goal "x ~: A ==> (insert x A) - {x} = A";
-by Auto_tac;
-qed "Diff_insert_absorb";
-
-Goal "A Int (B-A) = {}";
-by (Blast_tac 1);
-qed "Diff_disjoint";
-Addsimps[Diff_disjoint];
-
-Goal "A<=B ==> A Un (B-A) = B";
-by (Blast_tac 1);
-qed "Diff_partition";
-
-Goal "[| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
-by (Blast_tac 1);
-qed "double_diff";
-
-Goal "A Un (B-A) = A Un B";
-by (Blast_tac 1);
-qed "Un_Diff_cancel";
-
-Goal "(B-A) Un A = B Un A";
-by (Blast_tac 1);
-qed "Un_Diff_cancel2";
-
-Addsimps [Un_Diff_cancel, Un_Diff_cancel2];
-
-Goal "A - (B Un C) = (A-B) Int (A-C)";
-by (Blast_tac 1);
-qed "Diff_Un";
-
-Goal "A - (B Int C) = (A-B) Un (A-C)";
-by (Blast_tac 1);
-qed "Diff_Int";
-
-Goal "(A Un B) - C = (A - C) Un (B - C)";
-by (Blast_tac 1);
-qed "Un_Diff";
-
-Goal "(A Int B) - C = A Int (B - C)";
-by (Blast_tac 1);
-qed "Int_Diff";
-
-Goal "C Int (A-B) = (C Int A) - (C Int B)";
-by (Blast_tac 1);
-qed "Diff_Int_distrib";
-
-Goal "(A-B) Int C = (A Int C) - (B Int C)";
-by (Blast_tac 1);
-qed "Diff_Int_distrib2";
-
-Goal "A - (- B) = A Int B";
-by Auto_tac;
-qed "Diff_Compl";
-Addsimps [Diff_Compl];
-
-Goal "- (A-B) = -A Un B";
-by (blast_tac (claset() addIs []) 1);
-qed "Compl_Diff_eq";
-Addsimps [Compl_Diff_eq];
-
-
-section "Quantification over type \"bool\"";
-
-Goal "(ALL b::bool. P b) = (P True & P False)";
-by Auto_tac;
-by (case_tac "b" 1);
-by Auto_tac;
-qed "all_bool_eq";
-
-bind_thm ("bool_induct", conjI RS (all_bool_eq RS iffD2) RS spec);
-
-Goal "(EX b::bool. P b) = (P True | P False)";
-by Auto_tac;
-by (case_tac "b" 1);
-by Auto_tac;
-qed "ex_bool_eq";
-
-Goal "A Un B = (UN b. if b then A else B)";
-by (auto_tac(claset(), simpset() addsimps [split_if_mem2]));
-qed "Un_eq_UN";
-
-Goal "(UN b::bool. A b) = (A True Un A False)";
-by Auto_tac;
-by (case_tac "b" 1);
-by Auto_tac;
-qed "UN_bool_eq";
-
-Goal "(INT b::bool. A b) = (A True Int A False)";
-by Auto_tac;
-by (case_tac "b" 1);
-by Auto_tac;
-qed "INT_bool_eq";
-
-
-section "Pow";
-
-Goalw [Pow_def] "Pow {} = {{}}";
-by Auto_tac;
-qed "Pow_empty";
-Addsimps [Pow_empty];
-
-Goal "Pow (insert a A) = Pow A Un (insert a ` Pow A)";
-by (blast_tac (claset() addIs [inst "x" "?u-{a}" image_eqI]) 1);
-qed "Pow_insert";
-
-Goal "Pow (- A) = {-B |B. A: Pow B}";
-by (blast_tac (claset() addIs [inst "x" "- ?u" exI]) 1);
-qed "Pow_Compl";
-
-Goal "Pow UNIV = UNIV";
-by (Blast_tac 1);
-qed "Pow_UNIV";
-Addsimps [Pow_UNIV];
-
-Goal "Pow(A) Un Pow(B) <= Pow(A Un B)";
-by (Blast_tac 1);
-qed "Un_Pow_subset";
-
-Goal "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))";
-by (Blast_tac 1);
-qed "UN_Pow_subset";
-
-Goal "A <= Pow(Union(A))";
-by (Blast_tac 1);
-qed "subset_Pow_Union";
-
-Goal "Union(Pow(A)) = A";
-by (Blast_tac 1);
-qed "Union_Pow_eq";
-
-Goal "Pow(A Int B) = Pow(A) Int Pow(B)";
-by (Blast_tac 1);
-qed "Pow_Int_eq";
-
-Goal "Pow(INT x:A. B(x)) = (INT x:A. Pow(B(x)))";
-by (Blast_tac 1);
-qed "Pow_INT_eq";
-
-Addsimps [Union_Pow_eq, Pow_Int_eq];
-
-
-section "Miscellany";
-
-Goal "(A = B) = ((A <= (B::'a set)) & (B<=A))";
-by (Blast_tac 1);
-qed "set_eq_subset";
-
-Goal "(A <= B) = (ALL t. t:A --> t:B)";
-by (Blast_tac 1);
-qed "subset_iff";
-
-Goalw [psubset_def] "((A::'a set) <= B) = ((A < B) | (A=B))";
-by (Blast_tac 1);
-qed "subset_iff_psubset_eq";
-
-Goal "(ALL x. x ~: A) = (A={})";
-by (Blast_tac 1);
-qed "all_not_in_conv";
-AddIffs [all_not_in_conv];
-
-
-(** for datatypes **)
-Goal "f x ~= f y ==> x ~= y";
-by (Fast_tac 1);
-qed "distinct_lemma";
-
-
-(** Miniscoping: pushing in big Unions and Intersections **)
-local
- fun prover s = prove_goal (the_context ()) s
- (fn _ => [Simp_tac 1, ALLGOALS Blast_tac])
-in
-val UN_simps = map prover
- ["(UN x:C. insert a (B x)) = (if C={} then {} else insert a (UN x:C. B x))",
- "(UN x:C. A x Un B) = ((if C={} then {} else (UN x:C. A x) Un B))",
- "(UN x:C. A Un B x) = ((if C={} then {} else A Un (UN x:C. B x)))",
- "(UN x:C. A x Int B) = ((UN x:C. A x) Int B)",
- "(UN x:C. A Int B x) = (A Int (UN x:C. B x))",
- "(UN x:C. A x - B) = ((UN x:C. A x) - B)",
- "(UN x:C. A - B x) = (A - (INT x:C. B x))",
- "(UN x: Union A. B x) = (UN y:A. UN x:y. B x)",
- "(UN z: UNION A B. C z) = (UN x:A. UN z: B(x). C z)",
- "(UN x:f`A. B x) = (UN a:A. B(f a))"];
-
-val INT_simps = map prover
- ["(INT x:C. A x Int B) = (if C={} then UNIV else (INT x:C. A x) Int B)",
- "(INT x:C. A Int B x) = (if C={} then UNIV else A Int (INT x:C. B x))",
- "(INT x:C. A x - B) = (if C={} then UNIV else (INT x:C. A x) - B)",
- "(INT x:C. A - B x) = (if C={} then UNIV else A - (UN x:C. B x))",
- "(INT x:C. insert a (B x)) = insert a (INT x:C. B x)",
- "(INT x:C. A x Un B) = ((INT x:C. A x) Un B)",
- "(INT x:C. A Un B x) = (A Un (INT x:C. B x))",
- "(INT x: Union A. B x) = (INT y:A. INT x:y. B x)",
- "(INT z: UNION A B. C z) = (INT x:A. INT z: B(x). C z)",
- "(INT x:f`A. B x) = (INT a:A. B(f a))"];
-
-
-val ball_simps = map prover
- ["(ALL x:A. P x | Q) = ((ALL x:A. P x) | Q)",
- "(ALL x:A. P | Q x) = (P | (ALL x:A. Q x))",
- "(ALL x:A. P --> Q x) = (P --> (ALL x:A. Q x))",
- "(ALL x:A. P x --> Q) = ((EX x:A. P x) --> Q)",
- "(ALL x:{}. P x) = True",
- "(ALL x:UNIV. P x) = (ALL x. P x)",
- "(ALL x:insert a B. P x) = (P(a) & (ALL x:B. P x))",
- "(ALL x:Union(A). P x) = (ALL y:A. ALL x:y. P x)",
- "(ALL x: UNION A B. P x) = (ALL a:A. ALL x: B a. P x)",
- "(ALL x:Collect Q. P x) = (ALL x. Q x --> P x)",
- "(ALL x:f`A. P x) = (ALL x:A. P(f x))",
- "(~(ALL x:A. P x)) = (EX x:A. ~P x)"];
-
-val ball_conj_distrib =
- prover "(ALL x:A. P x & Q x) = ((ALL x:A. P x) & (ALL x:A. Q x))";
-
-val bex_simps = map prover
- ["(EX x:A. P x & Q) = ((EX x:A. P x) & Q)",
- "(EX x:A. P & Q x) = (P & (EX x:A. Q x))",
- "(EX x:{}. P x) = False",
- "(EX x:UNIV. P x) = (EX x. P x)",
- "(EX x:insert a B. P x) = (P(a) | (EX x:B. P x))",
- "(EX x:Union(A). P x) = (EX y:A. EX x:y. P x)",
- "(EX x: UNION A B. P x) = (EX a:A. EX x: B a. P x)",
- "(EX x:Collect Q. P x) = (EX x. Q x & P x)",
- "(EX x:f`A. P x) = (EX x:A. P(f x))",
- "(~(EX x:A. P x)) = (ALL x:A. ~P x)"];
-
-val bex_disj_distrib =
- prover "(EX x:A. P x | Q x) = ((EX x:A. P x) | (EX x:A. Q x))";
-
-end;
-
-bind_thms ("UN_simps", UN_simps);
-bind_thms ("INT_simps", INT_simps);
-bind_thms ("ball_simps", ball_simps);
-bind_thms ("bex_simps", bex_simps);
-bind_thm ("ball_conj_distrib", ball_conj_distrib);
-bind_thm ("bex_disj_distrib", bex_disj_distrib);
-
-Addsimps (UN_simps @ INT_simps @ ball_simps @ bex_simps);
--- a/src/HOL/mono.ML Fri Feb 15 20:43:44 2002 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,113 +0,0 @@
-(* Title: HOL/mono.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
-
-Monotonicity of various operations
-*)
-
-Goal "A<=B ==> f`A <= f`B";
-by (Blast_tac 1);
-qed "image_mono";
-
-Goal "A<=B ==> Pow(A) <= Pow(B)";
-by (Blast_tac 1);
-qed "Pow_mono";
-
-Goal "A<=B ==> Union(A) <= Union(B)";
-by (Blast_tac 1);
-qed "Union_mono";
-
-Goal "B<=A ==> Inter(A) <= Inter(B)";
-by (Blast_tac 1);
-qed "Inter_anti_mono";
-
-val prems = Goal
- "[| A<=B; !!x. x:A ==> f(x)<=g(x) |] ==> \
-\ (UN x:A. f(x)) <= (UN x:B. g(x))";
-by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
-qed "UN_mono";
-
-(*The last inclusion is POSITIVE! *)
-val prems = Goal
- "[| B<=A; !!x. x:A ==> f(x)<=g(x) |] ==> \
-\ (INT x:A. f(x)) <= (INT x:A. g(x))";
-by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
-qed "INT_anti_mono";
-
-Goal "C<=D ==> insert a C <= insert a D";
-by (Blast_tac 1);
-qed "insert_mono";
-
-Goal "[| A<=C; B<=D |] ==> A Un B <= C Un D";
-by (Blast_tac 1);
-qed "Un_mono";
-
-Goal "[| A<=C; B<=D |] ==> A Int B <= C Int D";
-by (Blast_tac 1);
-qed "Int_mono";
-
-Goal "!!A::'a set. [| A<=C; D<=B |] ==> A-B <= C-D";
-by (Blast_tac 1);
-qed "Diff_mono";
-
-Goal "!!A::'a set. A <= B ==> -B <= -A";
-by (Blast_tac 1);
-qed "Compl_anti_mono";
-
-(** Monotonicity of implications. For inductive definitions **)
-
-Goal "A<=B ==> x:A --> x:B";
-by (rtac impI 1);
-by (etac subsetD 1);
-by (assume_tac 1);
-qed "in_mono";
-
-Goal "[| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)";
-by (Blast_tac 1);
-qed "conj_mono";
-
-Goal "[| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)";
-by (Blast_tac 1);
-qed "disj_mono";
-
-Goal "[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)";
-by (Blast_tac 1);
-qed "imp_mono";
-
-Goal "P-->P";
-by (rtac impI 1);
-by (assume_tac 1);
-qed "imp_refl";
-
-val [PQimp] = Goal
- "[| !!x. P(x) --> Q(x) |] ==> (EX x. P(x)) --> (EX x. Q(x))";
-by (blast_tac (claset() addIs [PQimp RS mp]) 1);
-qed "ex_mono";
-
-val [PQimp] = Goal
- "[| !!x. P(x) --> Q(x) |] ==> (ALL x. P(x)) --> (ALL x. Q(x))";
-by (blast_tac (claset() addIs [PQimp RS mp]) 1);
-qed "all_mono";
-
-val [PQimp] = Goal
- "[| !!x. P(x) --> Q(x) |] ==> Collect(P) <= Collect(Q)";
-by (blast_tac (claset() addIs [PQimp RS mp]) 1);
-qed "Collect_mono";
-
-val [subs,PQimp] = Goal
- "[| A<=B; !!x. x:A ==> P(x) --> Q(x) \
-\ |] ==> A Int Collect(P) <= B Int Collect(Q)";
-by (blast_tac (claset() addIs [subs RS subsetD, PQimp RS mp]) 1);
-qed "Int_Collect_mono";
-
-val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono,
- ex_mono, Collect_mono, in_mono];
-
-Goal "[| a = b; c = d; b --> d |] ==> a --> c";
-by (Fast_tac 1);
-qed "eq_to_mono";
-
-Goal "[| a = b; c = d; ~ b --> ~ d |] ==> ~ a --> ~ c";
-by (Fast_tac 1);
-qed "eq_to_mono2";
--- a/src/HOL/subset.ML Fri Feb 15 20:43:44 2002 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,267 +0,0 @@
-(* Title: HOL/subset.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
-
-Derived rules involving subsets. Union and Intersection as lattice
-operations.
-*)
-
-(* legacy ML bindings *)
-
-val Ball_def = thm "Ball_def";
-val Bex_def = thm "Bex_def";
-val Collect_mem_eq = thm "Collect_mem_eq";
-val Compl_def = thm "Compl_def";
-val INTER_def = thm "INTER_def";
-val Int_def = thm "Int_def";
-val Inter_def = thm "Inter_def";
-val Pow_def = thm "Pow_def";
-val UNION_def = thm "UNION_def";
-val UNIV_def = thm "UNIV_def";
-val Un_def = thm "Un_def";
-val Union_def = thm "Union_def";
-val empty_def = thm "empty_def";
-val image_def = thm "image_def";
-val insert_def = thm "insert_def";
-val mem_Collect_eq = thm "mem_Collect_eq";
-val psubset_def = thm "psubset_def";
-val set_diff_def = thm "set_diff_def";
-val subset_def = thm "subset_def";
-val CollectI = thm "CollectI";
-val CollectD = thm "CollectD";
-val set_ext = thm "set_ext";
-val Collect_cong = thm "Collect_cong";
-val CollectE = thm "CollectE";
-val ballI = thm "ballI";
-val strip = thms "strip";
-val bspec = thm "bspec";
-val ballE = thm "ballE";
-val bexI = thm "bexI";
-val rev_bexI = thm "rev_bexI";
-val bexCI = thm "bexCI";
-val bexE = thm "bexE";
-val ball_triv = thm "ball_triv";
-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 bex_one_point1 = thm "bex_one_point1";
-val bex_one_point2 = thm "bex_one_point2";
-val ball_one_point1 = thm "ball_one_point1";
-val ball_one_point2 = thm "ball_one_point2";
-val ball_cong = thm "ball_cong";
-val bex_cong = thm "bex_cong";
-val subsetI = thm "subsetI";
-val subsetD = thm "subsetD";
-val rev_subsetD = thm "rev_subsetD";
-val subsetCE = thm "subsetCE";
-val contra_subsetD = thm "contra_subsetD";
-val subset_refl = thm "subset_refl";
-val subset_trans = thm "subset_trans";
-val subset_antisym = thm "subset_antisym";
-val equalityI = thm "equalityI";
-val equalityD1 = thm "equalityD1";
-val equalityD2 = thm "equalityD2";
-val equalityE = thm "equalityE";
-val equalityCE = thm "equalityCE";
-val setup_induction = thm "setup_induction";
-val eqset_imp_iff = thm "eqset_imp_iff";
-val UNIV_I = thm "UNIV_I";
-val UNIV_witness = thm "UNIV_witness";
-val subset_UNIV = thm "subset_UNIV";
-val ball_UNIV = thm "ball_UNIV";
-val bex_UNIV = thm "bex_UNIV";
-val empty_iff = thm "empty_iff";
-val emptyE = thm "emptyE";
-val empty_subsetI = thm "empty_subsetI";
-val equals0I = thm "equals0I";
-val equals0D = thm "equals0D";
-val ball_empty = thm "ball_empty";
-val bex_empty = thm "bex_empty";
-val UNIV_not_empty = thm "UNIV_not_empty";
-val Pow_iff = thm "Pow_iff";
-val PowI = thm "PowI";
-val PowD = thm "PowD";
-val Pow_bottom = thm "Pow_bottom";
-val Pow_top = thm "Pow_top";
-val Compl_iff = thm "Compl_iff";
-val ComplI = thm "ComplI";
-val ComplD = thm "ComplD";
-val ComplE = thm "ComplE";
-val Un_iff = thm "Un_iff";
-val UnI1 = thm "UnI1";
-val UnI2 = thm "UnI2";
-val UnCI = thm "UnCI";
-val UnE = thm "UnE";
-val Int_iff = thm "Int_iff";
-val IntI = thm "IntI";
-val IntD1 = thm "IntD1";
-val IntD2 = thm "IntD2";
-val IntE = thm "IntE";
-val Diff_iff = thm "Diff_iff";
-val DiffI = thm "DiffI";
-val DiffD1 = thm "DiffD1";
-val DiffD2 = thm "DiffD2";
-val DiffE = thm "DiffE";
-val insert_iff = thm "insert_iff";
-val insertI1 = thm "insertI1";
-val insertI2 = thm "insertI2";
-val insertE = thm "insertE";
-val insertCI = thm "insertCI";
-val subset_insert_iff = thm "subset_insert_iff";
-val singletonI = thm "singletonI";
-val singletonD = thm "singletonD";
-val singletonE = thm "singletonE";
-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 subset_singletonD = thm "subset_singletonD";
-val singleton_conv = thm "singleton_conv";
-val singleton_conv2 = thm "singleton_conv2";
-val diff_single_insert = thm "diff_single_insert";
-val UN_iff = thm "UN_iff";
-val UN_I = thm "UN_I";
-val UN_E = thm "UN_E";
-val UN_cong = thm "UN_cong";
-val INT_iff = thm "INT_iff";
-val INT_I = thm "INT_I";
-val INT_D = thm "INT_D";
-val INT_E = thm "INT_E";
-val INT_cong = thm "INT_cong";
-val Union_iff = thm "Union_iff";
-val UnionI = thm "UnionI";
-val UnionE = thm "UnionE";
-val Inter_iff = thm "Inter_iff";
-val InterI = thm "InterI";
-val InterD = thm "InterD";
-val InterE = thm "InterE";
-val image_eqI = thm "image_eqI";
-val imageI = thm "imageI";
-val rev_image_eqI = thm "rev_image_eqI";
-val imageE = thm "imageE";
-val image_Un = thm "image_Un";
-val image_iff = thm "image_iff";
-val image_subset_iff = thm "image_subset_iff";
-val subset_image_iff = thm "subset_image_iff";
-val image_subsetI = thm "image_subsetI";
-val range_eqI = thm "range_eqI";
-val rangeI = thm "rangeI";
-val rangeE = thm "rangeE";
-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 mem_simps = thms "mem_simps";
-val psubsetI = thm "psubsetI";
-val psubset_insert_iff = thm "psubset_insert_iff";
-val psubset_eq = thm "psubset_eq";
-val psubset_imp_subset = thm "psubset_imp_subset";
-val psubset_subset_trans = thm "psubset_subset_trans";
-val subset_psubset_trans = thm "subset_psubset_trans";
-val psubset_imp_ex_mem = thm "psubset_imp_ex_mem";
-val atomize_ball = thm "atomize_ball";
-
-
-(*** insert ***)
-
-Goal "B <= insert a B";
-by (rtac subsetI 1);
-by (etac insertI2 1) ;
-qed "subset_insertI";
-
-Goal "x ~: A ==> (A <= insert x B) = (A <= B)";
-by (Blast_tac 1);
-qed "subset_insert";
-
-(*** Big Union -- least upper bound of a set ***)
-
-Goal "B:A ==> B <= Union(A)";
-by (REPEAT (ares_tac [subsetI,UnionI] 1));
-qed "Union_upper";
-
-val [prem] = Goal "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C";
-by (rtac subsetI 1);
-by (REPEAT (eresolve_tac [asm_rl, UnionE, prem RS subsetD] 1));
-qed "Union_least";
-
-(** General union **)
-
-Goal "a:A ==> B(a) <= (UN x:A. B(x))";
-by (Blast_tac 1);
-qed "UN_upper";
-
-val [prem] = Goal "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C";
-by (rtac subsetI 1);
-by (REPEAT (eresolve_tac [asm_rl, UN_E, prem RS subsetD] 1));
-qed "UN_least";
-
-
-(*** Big Intersection -- greatest lower bound of a set ***)
-
-Goal "B:A ==> Inter(A) <= B";
-by (Blast_tac 1);
-qed "Inter_lower";
-
-val [prem] = Goal "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)";
-by (rtac (InterI RS subsetI) 1);
-by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1));
-qed "Inter_greatest";
-
-Goal "a:A ==> (INT x:A. B(x)) <= B(a)";
-by (Blast_tac 1);
-qed "INT_lower";
-
-val [prem] = Goal "[| !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))";
-by (rtac (INT_I RS subsetI) 1);
-by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1));
-qed "INT_greatest";
-
-(*** Finite Union -- the least upper bound of 2 sets ***)
-
-Goal "A <= A Un B";
-by (Blast_tac 1);
-qed "Un_upper1";
-
-Goal "B <= A Un B";
-by (Blast_tac 1);
-qed "Un_upper2";
-
-Goal "[| A<=C; B<=C |] ==> A Un B <= C";
-by (Blast_tac 1);
-qed "Un_least";
-
-(*** Finite Intersection -- the greatest lower bound of 2 sets *)
-
-Goal "A Int B <= A";
-by (Blast_tac 1);
-qed "Int_lower1";
-
-Goal "A Int B <= B";
-by (Blast_tac 1);
-qed "Int_lower2";
-
-Goal "[| C<=A; C<=B |] ==> C <= A Int B";
-by (Blast_tac 1);
-qed "Int_greatest";
-
-(*** Set difference ***)
-
-Goal "A-B <= (A::'a set)";
-by (Blast_tac 1) ;
-qed "Diff_subset";
-
-(*** Monotonicity ***)
-
-Goal "mono(f) ==> f(A) Un f(B) <= f(A Un B)";
-by (rtac Un_least 1);
-by (etac (Un_upper1 RSN (2,monoD)) 1);
-by (etac (Un_upper2 RSN (2,monoD)) 1);
-qed "mono_Un";
-
-Goal "mono(f) ==> f(A Int B) <= f(A) Int f(B)";
-by (rtac Int_greatest 1);
-by (etac (Int_lower1 RSN (2,monoD)) 1);
-by (etac (Int_lower2 RSN (2,monoD)) 1);
-qed "mono_Int";