--- a/NEWS Thu Sep 15 17:06:00 2011 +0200
+++ b/NEWS Thu Sep 15 12:40:08 2011 -0400
@@ -115,7 +115,7 @@
Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary,
INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter,
-INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union,
+INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, INF_subset,
UNION_eq_Union_image, Union_def, UN_singleton, UN_eq have been
discarded.
--- a/src/HOL/Big_Operators.thy Thu Sep 15 17:06:00 2011 +0200
+++ b/src/HOL/Big_Operators.thy Thu Sep 15 12:40:08 2011 -0400
@@ -312,14 +312,14 @@
text{*No need to assume that @{term C} is finite. If infinite, the rhs is
directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
lemma setsum_Union_disjoint:
- "[| (ALL A:C. finite A);
- (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
- ==> setsum f (Union C) = setsum (setsum f) C"
-apply (cases "finite C")
- prefer 2 apply (force dest: finite_UnionD simp add: setsum_def)
- apply (frule setsum_UN_disjoint [of C id f])
- apply (unfold Union_def id_def, assumption+)
-done
+ assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}"
+ shows "setsum f (Union C) = setsum (setsum f) C"
+proof cases
+ assume "finite C"
+ from setsum_UN_disjoint[OF this assms]
+ show ?thesis
+ by (simp add: SUP_def)
+qed (force dest: finite_UnionD simp add: setsum_def)
(*But we can't get rid of finite A. If infinite, although the lhs is 0,
the rhs need not be, since SIGMA A B could still be finite.*)
@@ -801,7 +801,7 @@
(ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {})
==> card (Union C) = setsum card C"
apply (frule card_UN_disjoint [of C id])
-apply (unfold Union_def id_def, assumption+)
+apply (simp_all add: SUP_def id_def)
done
text{*The image of a finite set can be expressed using @{term fold_image}.*}
@@ -996,14 +996,14 @@
by (simp add: setprod_def fold_image_UN_disjoint)
lemma setprod_Union_disjoint:
- "[| (ALL A:C. finite A);
- (ALL A:C. ALL B:C. A \<noteq> B --> A Int B = {}) |]
- ==> setprod f (Union C) = setprod (setprod f) C"
-apply (cases "finite C")
- prefer 2 apply (force dest: finite_UnionD simp add: setprod_def)
- apply (frule setprod_UN_disjoint [of C id f])
- apply (unfold Union_def id_def, assumption+)
-done
+ assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}"
+ shows "setprod f (Union C) = setprod (setprod f) C"
+proof cases
+ assume "finite C"
+ from setprod_UN_disjoint[OF this assms]
+ show ?thesis
+ by (simp add: SUP_def)
+qed (force dest: finite_UnionD simp add: setprod_def)
lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
(\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
--- a/src/HOL/Complete_Lattices.thy Thu Sep 15 17:06:00 2011 +0200
+++ b/src/HOL/Complete_Lattices.thy Thu Sep 15 12:40:08 2011 -0400
@@ -1131,7 +1131,6 @@
"\<And>A B f. (\<Inter>a\<in>A. B (f a)) = (\<Inter>x\<in>f`A. B x)"
by auto
-
text {* Legacy names *}
lemma (in complete_lattice) Inf_singleton [simp]:
@@ -1142,68 +1141,9 @@
"\<Squnion>{a} = a"
by simp
-lemma (in complete_lattice) Inf_binary:
- "\<Sqinter>{a, b} = a \<sqinter> b"
- by simp
-
-lemma (in complete_lattice) Sup_binary:
- "\<Squnion>{a, b} = a \<squnion> b"
- by simp
-
-text {* Grep and put to news from here *}
-
-lemma (in complete_lattice) INF_eq:
- "(\<Sqinter>x\<in>A. B x) = \<Sqinter>({Y. \<exists>x\<in>A. Y = B x})"
- by (simp add: INF_def image_def)
-
-lemma (in complete_lattice) SUP_eq:
- "(\<Squnion>x\<in>A. B x) = \<Squnion>({Y. \<exists>x\<in>A. Y = B x})"
- by (simp add: SUP_def image_def)
-
-lemma (in complete_lattice) INF_subset:
- "B \<subseteq> A \<Longrightarrow> INFI A f \<sqsubseteq> INFI B f"
- by (rule INF_superset_mono) auto
-
-lemma (in complete_lattice) INF_UNIV_range:
- "(\<Sqinter>x. f x) = \<Sqinter>range f"
- by (fact INF_def)
-
-lemma (in complete_lattice) SUP_UNIV_range:
- "(\<Squnion>x. f x) = \<Squnion>range f"
- by (fact SUP_def)
-
-lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
- by simp
-
-lemma INTER_eq_Inter_image:
- "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
- by (fact INF_def)
-
-lemma Inter_def:
- "\<Inter>S = (\<Inter>x\<in>S. x)"
- by (simp add: INTER_eq_Inter_image image_def)
-
-lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})"
- by (fact INF_eq)
-
-lemma Un_eq_Union: "A \<union> B = \<Union>{A, B}"
- by blast
-
-lemma UNION_eq_Union_image:
- "(\<Union>x\<in>A. B x) = \<Union>(B ` A)"
- by (fact SUP_def)
-
-lemma Union_def:
- "\<Union>S = (\<Union>x\<in>S. x)"
- by (simp add: UNION_eq_Union_image image_def)
-
lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
by blast
-lemma UN_eq: "(\<Union>x\<in>A. B x) = \<Union>({Y. \<exists>x\<in>A. Y = B x})"
- by (fact SUP_eq)
-
-
text {* Finally *}
no_notation
--- a/src/HOL/Probability/Lebesgue_Integration.thy Thu Sep 15 17:06:00 2011 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Thu Sep 15 12:40:08 2011 -0400
@@ -1419,7 +1419,7 @@
(SUP n. \<integral>\<^isup>+ x. (INF i:{n..}. u i x) \<partial>M)"
unfolding liminf_SUPR_INFI using pos u
by (intro positive_integral_monotone_convergence_SUP_AE)
- (elim AE_mp, auto intro!: AE_I2 intro: INF_greatest INF_subset)
+ (elim AE_mp, auto intro!: AE_I2 intro: INF_greatest INF_superset_mono)
also have "\<dots> \<le> liminf (\<lambda>n. integral\<^isup>P M (u n))"
unfolding liminf_SUPR_INFI
by (auto intro!: SUP_mono exI INF_greatest positive_integral_mono INF_lower)
--- a/src/HOL/RealVector.thy Thu Sep 15 17:06:00 2011 +0200
+++ b/src/HOL/RealVector.thy Thu Sep 15 12:40:08 2011 -0400
@@ -452,13 +452,13 @@
using open_Union [of "{S, T}"] by simp
lemma open_UN [intro]: "\<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Union>x\<in>A. B x)"
- unfolding UN_eq by (rule open_Union) auto
+ unfolding SUP_def by (rule open_Union) auto
+
+lemma open_Inter [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)"
+ by (induct set: finite) auto
lemma open_INT [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)"
- by (induct set: finite) auto
-
-lemma open_Inter [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)"
- unfolding Inter_def by (rule open_INT)
+ unfolding INF_def by (rule open_Inter) auto
lemma closed_empty [intro, simp]: "closed {}"
unfolding closed_def by simp
@@ -466,9 +466,6 @@
lemma closed_Un [intro]: "closed S \<Longrightarrow> closed T \<Longrightarrow> closed (S \<union> T)"
unfolding closed_def by auto
-lemma closed_Inter [intro]: "\<forall>S\<in>K. closed S \<Longrightarrow> closed (\<Inter> K)"
- unfolding closed_def Inter_def by auto
-
lemma closed_UNIV [intro, simp]: "closed UNIV"
unfolding closed_def by simp
@@ -478,11 +475,14 @@
lemma closed_INT [intro]: "\<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Inter>x\<in>A. B x)"
unfolding closed_def by auto
-lemma closed_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Union>x\<in>A. B x)"
+lemma closed_Inter [intro]: "\<forall>S\<in>K. closed S \<Longrightarrow> closed (\<Inter> K)"
+ unfolding closed_def uminus_Inf by auto
+
+lemma closed_Union [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. closed T \<Longrightarrow> closed (\<Union>S)"
by (induct set: finite) auto
-lemma closed_Union [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. closed T \<Longrightarrow> closed (\<Union>S)"
- unfolding Union_def by (rule closed_UN)
+lemma closed_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Union>x\<in>A. B x)"
+ unfolding SUP_def by (rule closed_Union) auto
lemma open_closed: "open S \<longleftrightarrow> closed (- S)"
unfolding closed_def by simp
--- a/src/HOL/Wellfounded.thy Thu Sep 15 17:06:00 2011 +0200
+++ b/src/HOL/Wellfounded.thy Thu Sep 15 12:40:08 2011 -0400
@@ -305,9 +305,7 @@
"[| ALL r:R. wf r;
ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {}
|] ==> wf(Union R)"
-apply (simp add: Union_def)
-apply (blast intro: wf_UN)
-done
+ using wf_UN[of R "\<lambda>i. i"] by (simp add: SUP_def)
(*Intuition: we find an (R u S)-min element of a nonempty subset A
by case distinction.