# HG changeset patch
# User hoelzl
# Date 1316104808 14400
# Node ID 22c0857b8aab48518427dd8314192efa5a21002f
# Parent  e1139e612b5551c39b3d957d58352d8fff4fe1ec
removed further legacy rules from Complete_Lattices

diff -r e1139e612b55 -r 22c0857b8aab NEWS
--- 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.
 
diff -r e1139e612b55 -r 22c0857b8aab src/HOL/Big_Operators.thy
--- 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)) =
diff -r e1139e612b55 -r 22c0857b8aab src/HOL/Complete_Lattices.thy
--- 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
diff -r e1139e612b55 -r 22c0857b8aab src/HOL/Probability/Lebesgue_Integration.thy
--- 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)
diff -r e1139e612b55 -r 22c0857b8aab src/HOL/RealVector.thy
--- 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
diff -r e1139e612b55 -r 22c0857b8aab src/HOL/Wellfounded.thy
--- 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.