src/HOL/Set.thy
 changeset 16773 33c4d8fe6f78 parent 16636 1ed737a98198 child 17002 fb9261990ffe
```     1.1 --- a/src/HOL/Set.thy	Tue Jul 12 11:55:33 2005 +0200
1.2 +++ b/src/HOL/Set.thy	Tue Jul 12 12:49:00 2005 +0200
1.3 @@ -1110,10 +1110,10 @@
1.4  text {* \medskip Monotonicity. *}
1.5
1.6  lemma mono_Un: "mono f ==> f A \<union> f B \<subseteq> f (A \<union> B)"
1.7 -  by (blast dest: monoD)
1.8 +  by (auto simp add: mono_def)
1.9
1.10  lemma mono_Int: "mono f ==> f (A \<inter> B) \<subseteq> f A \<inter> f B"
1.11 -  by (blast dest: monoD)
1.12 +  by (auto simp add: mono_def)
1.13
1.14  subsubsection {* Equalities involving union, intersection, inclusion, etc. *}
1.15
1.16 @@ -1199,12 +1199,12 @@
1.17  lemma insert_disjoint[simp]:
1.18   "(insert a A \<inter> B = {}) = (a \<notin> B \<and> A \<inter> B = {})"
1.19   "({} = insert a A \<inter> B) = (a \<notin> B \<and> {} = A \<inter> B)"
1.20 -by auto
1.21 +  by auto
1.22
1.23  lemma disjoint_insert[simp]:
1.24   "(B \<inter> insert a A = {}) = (a \<notin> B \<and> B \<inter> A = {})"
1.25   "({} = A \<inter> insert b B) = (b \<notin> A \<and> {} = A \<inter> B)"
1.26 -by auto
1.27 +  by auto
1.28
1.29  text {* \medskip @{text image}. *}
1.30
1.31 @@ -1215,7 +1215,7 @@
1.32    by blast
1.33
1.34  lemma image_constant: "x \<in> A ==> (\<lambda>x. c) ` A = {c}"
1.35 -  by blast
1.36 +  by auto
1.37
1.38  lemma image_image: "f ` (g ` A) = (\<lambda>x. f (g x)) ` A"
1.39    by blast
1.40 @@ -1226,10 +1226,11 @@
1.41  lemma image_is_empty [iff]: "(f`A = {}) = (A = {})"
1.42    by blast
1.43
1.44 +
1.45  lemma image_Collect: "f ` {x. P x} = {f x | x. P x}"
1.46 -  -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS, *}
1.47 -  -- {* with its implicit quantifier and conjunction.  Also image enjoys better *}
1.48 -  -- {* equational properties than does the RHS. *}
1.49 +  -- {* NOT suitable as a default simprule: the RHS isn't simpler than the LHS,
1.50 +      with its implicit quantifier and conjunction.  Also image enjoys better
1.51 +      equational properties than does the RHS. *}
1.52    by blast
1.53
1.54  lemma if_image_distrib [simp]:
```